From be52d950f096e389f8fa737db424fee2d79b1741 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 6 Nov 2014 12:19:40 -0800
Subject: [PATCH] fix(frontends/lean): improve error message, addresses issue
 #299

---
 src/frontends/lean/pp_options.cpp             |  5 +++--
 src/util/sexpr/options.h                      |  4 ++++
 tests/lean/error_full_names.lean              | 10 ++++++++++
 tests/lean/error_full_names.lean.expected.out | 16 ++++++++++++++++
 4 files changed, 33 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/error_full_names.lean
 create mode 100644 tests/lean/error_full_names.lean.expected.out

diff --git a/src/frontends/lean/pp_options.cpp b/src/frontends/lean/pp_options.cpp
index 81b2a67f6..856cdd9ea 100644
--- a/src/frontends/lean/pp_options.cpp
+++ b/src/frontends/lean/pp_options.cpp
@@ -93,13 +93,14 @@ void initialize_pp_options() {
                          "(pretty printer) apply beta-reduction when pretty printing");
 
     options universes_true(*g_pp_universes, true);
+    options full_names_true(*g_pp_full_names, true);
     options implicit_true(*g_pp_implicit, true);
     options coercions_true(*g_pp_coercions, true);
     options notation_false(*g_pp_notation, false);
     options implicit_coercions = join(coercions_true, implicit_true);
     options implicit_notation  = join(notation_false, implicit_true);
-    options all = join(join(universes_true, implicit_true), join(coercions_true, notation_false));
-    g_distinguishing_pp_options = new list<options>({implicit_true, coercions_true, implicit_coercions,
+    options all = universes_true + implicit_true + coercions_true + notation_false + full_names_true;
+    g_distinguishing_pp_options = new list<options>({implicit_true, full_names_true, coercions_true, implicit_coercions,
                 implicit_notation, universes_true, all});
 }
 
diff --git a/src/util/sexpr/options.h b/src/util/sexpr/options.h
index 6af4d6cde..aef07f325 100644
--- a/src/util/sexpr/options.h
+++ b/src/util/sexpr/options.h
@@ -85,6 +85,10 @@ inline options read_options(deserializer & d) { return options(read_sexpr(d)); }
 inline deserializer & operator>>(deserializer & d, options & o) { o = read_options(d); return d; }
 template<typename T> options update(options const & o, name const & n, T const & v) { return o.update(n, sexpr(v)); }
 
+inline options operator+(options const & opts1, options const & opts2) {
+    return join(opts1, opts2);
+}
+
 struct mk_option_declaration {
     mk_option_declaration(name const & n, option_kind k, char const * default_value, char const * description);
 };
diff --git a/tests/lean/error_full_names.lean b/tests/lean/error_full_names.lean
new file mode 100644
index 000000000..7f9aebd18
--- /dev/null
+++ b/tests/lean/error_full_names.lean
@@ -0,0 +1,10 @@
+import data.nat
+namespace foo
+open nat
+inductive nat : Type := zero, foosucc : nat → nat
+check 0 + nat.zero --error
+end foo
+
+namespace foo
+check nat.succ nat.zero --error
+end foo
diff --git a/tests/lean/error_full_names.lean.expected.out b/tests/lean/error_full_names.lean.expected.out
new file mode 100644
index 000000000..e592afff1
--- /dev/null
+++ b/tests/lean/error_full_names.lean.expected.out
@@ -0,0 +1,16 @@
+error_full_names.lean:5:8: error: type mismatch at application
+  0 + nat.zero
+term
+  nat.zero
+has type
+  nat
+but is expected to have type
+  ℕ
+error_full_names.lean:9:6: error: type mismatch at application
+  nat.succ nat.zero
+term
+  nat.zero
+has type
+  foo.nat
+but is expected to have type
+  nat