From b6fde680127c86c29e299c59755fa88e69045d9d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 1 Jun 2015 15:35:28 -0700
Subject: [PATCH] feat(frontends/lean/decl_cmds): avoid funny names when
 displaying error messages for "examples"

---
 src/frontends/lean/decl_cmds.cpp                | 13 ++++++++-----
 tests/lean/571.lean.expected.out                |  2 +-
 tests/lean/abbrev_paren.hlean.expected.out      |  2 +-
 tests/lean/apply_fail.lean.expected.out         |  2 +-
 tests/lean/assert_fail.lean.expected.out        |  4 ++--
 tests/lean/constr_tac_errors.lean.expected.out  | 10 +++++-----
 tests/lean/exact_partial.lean.expected.out      |  2 +-
 tests/lean/exact_partial2.lean.expected.out     |  2 +-
 tests/lean/quasireducible.lean.expected.out     |  4 ++--
 tests/lean/red.lean.expected.out                |  2 +-
 tests/lean/revert_fail.lean.expected.out        |  6 +++---
 tests/lean/rewrite_fail.lean.expected.out       |  4 ++--
 tests/lean/show_tac.lean.expected.out           |  2 +-
 tests/lean/unsolved_proof_qed.lean.expected.out |  4 ++--
 tests/lean/user_rec_crash.lean.expected.out     |  2 +-
 15 files changed, 32 insertions(+), 29 deletions(-)

diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index b9af33442..5f12c7619 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -910,9 +910,11 @@ class definition_cmd_fn {
     buffer<name>          m_ls_buffer_checkpoint;
 
     void save_checkpoint() {
-        m_type_checkpoint      = m_type;
-        m_env_checkpoint       = m_env;
-        m_ls_buffer_checkpoint = m_ls_buffer;
+        if (m_kind != Example) {
+            m_type_checkpoint      = m_type;
+            m_env_checkpoint       = m_env;
+            m_ls_buffer_checkpoint = m_ls_buffer;
+        }
     }
 
     bool is_definition() const { return m_kind == Definition || m_kind == Abbreviation || m_kind == LocalAbbreviation; }
@@ -921,7 +923,7 @@ class definition_cmd_fn {
 
     void parse_name() {
         if (m_kind == Example)
-            m_name = m_p.mk_fresh_name();
+            m_name = name{"example"};
         else
             m_name = m_p.check_id_next("invalid declaration, identifier expected");
     }
@@ -1338,7 +1340,8 @@ static environment theorem_cmd(parser & p) {
     return definition_cmd_core(p, Theorem, false, false);
 }
 static environment example_cmd(parser & p) {
-    return definition_cmd_core(p, Example, false, false);
+    definition_cmd_core(p, Example, false, false);
+    return p.env();
 }
 static environment private_definition_cmd(parser & p) {
     def_cmd_kind kind = Definition;
diff --git a/tests/lean/571.lean.expected.out b/tests/lean/571.lean.expected.out
index 0d9564630..404d6f8f1 100644
--- a/tests/lean/571.lean.expected.out
+++ b/tests/lean/571.lean.expected.out
@@ -7,7 +7,7 @@ H : ∃ (n : ℕ), P n
 P : ℕ → Prop,
 H : ∃ (n : ℕ), P n
 ⊢ ℕ
-571.lean:7:0: error: failed to add declaration '14.1' to environment, value has metavariables
+571.lean:7:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (P : …) (H : …),
     ?M_1
diff --git a/tests/lean/abbrev_paren.hlean.expected.out b/tests/lean/abbrev_paren.hlean.expected.out
index 6a9b69f12..609b84b80 100644
--- a/tests/lean/abbrev_paren.hlean.expected.out
+++ b/tests/lean/abbrev_paren.hlean.expected.out
@@ -1,7 +1,7 @@
 abbrev_paren.hlean:5:54: error: don't know how to synthesize placeholder
 C : Precategory
 ⊢ C = Precategory.mk (carrier C) C
-abbrev_paren.hlean:5:54: error: failed to add declaration '14.0' to environment, value has metavariables
+abbrev_paren.hlean:5:54: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (C : Precategory),
     ?M_1
diff --git a/tests/lean/apply_fail.lean.expected.out b/tests/lean/apply_fail.lean.expected.out
index 5ea45ee6d..4b1292b60 100644
--- a/tests/lean/apply_fail.lean.expected.out
+++ b/tests/lean/apply_fail.lean.expected.out
@@ -8,7 +8,7 @@ a b : Prop
 apply_fail.lean:4:0: error: don't know how to synthesize placeholder
 a b : Prop
 ⊢ a ∧ b
-apply_fail.lean:4:0: error: failed to add declaration '14.0' to environment, value has metavariables
+apply_fail.lean:4:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (a b : Prop),
     ?M_1
diff --git a/tests/lean/assert_fail.lean.expected.out b/tests/lean/assert_fail.lean.expected.out
index 0e0901e43..711351872 100644
--- a/tests/lean/assert_fail.lean.expected.out
+++ b/tests/lean/assert_fail.lean.expected.out
@@ -7,7 +7,7 @@ assert_fail.lean:4:0: error: don't know how to synthesize placeholder
 a b : Prop,
 H : b ∧ a
 ⊢ a ∧ b
-assert_fail.lean:4:0: error: failed to add declaration '14.0' to environment, value has metavariables
+assert_fail.lean:4:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (a b : Prop) (H : …),
     ?M_1
@@ -18,7 +18,7 @@ assert_fail.lean:10:0: error: don't know how to synthesize placeholder
 a : Prop,
 Ha : a
 ⊢ a
-assert_fail.lean:10:0: error: failed to add declaration '14.1' to environment, value has metavariables
+assert_fail.lean:10:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (a : Prop) (Ha : a),
     ?M_1
diff --git a/tests/lean/constr_tac_errors.lean.expected.out b/tests/lean/constr_tac_errors.lean.expected.out
index fe57cf41c..11a2e0799 100644
--- a/tests/lean/constr_tac_errors.lean.expected.out
+++ b/tests/lean/constr_tac_errors.lean.expected.out
@@ -5,7 +5,7 @@ proof state:
 constr_tac_errors.lean:4:0: error: don't know how to synthesize placeholder
 
 ⊢ nat
-constr_tac_errors.lean:4:0: error: failed to add declaration '14.0' to environment, value has metavariables
+constr_tac_errors.lean:4:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   ?M_1
 constr_tac_errors.lean:12:2: error:invalid 'constructor' tactic, goal is an inductive datatype, but it does not have 2 constructor(s)
@@ -17,7 +17,7 @@ Hb : b
 constr_tac_errors.lean:13:0: error: don't know how to synthesize placeholder
 a b : Prop
 ⊢ a → b → a ∧ b
-constr_tac_errors.lean:13:0: error: failed to add declaration '14.2' to environment, value has metavariables
+constr_tac_errors.lean:13:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (a b : Prop),
     ?M_1
@@ -30,7 +30,7 @@ Hb : b
 constr_tac_errors.lean:19:0: error: don't know how to synthesize placeholder
 a b : Prop
 ⊢ a → b → a ∧ b
-constr_tac_errors.lean:19:0: error: failed to add declaration '14.3' to environment, value has metavariables
+constr_tac_errors.lean:19:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (a b : Prop),
     ?M_1
@@ -43,7 +43,7 @@ Hb : b
 constr_tac_errors.lean:32:0: error: don't know how to synthesize placeholder
 a b : Prop
 ⊢ a → b → unit
-constr_tac_errors.lean:32:0: error: failed to add declaration '14.5' to environment, value has metavariables
+constr_tac_errors.lean:32:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (a b : Prop),
     ?M_1
@@ -54,6 +54,6 @@ proof state:
 constr_tac_errors.lean:40:0: error: don't know how to synthesize placeholder
 
 ⊢ nat → nat
-constr_tac_errors.lean:40:0: error: failed to add declaration '14.7' to environment, value has metavariables
+constr_tac_errors.lean:40:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   ?M_1
diff --git a/tests/lean/exact_partial.lean.expected.out b/tests/lean/exact_partial.lean.expected.out
index ce63e3b2c..5a9eaa1a6 100644
--- a/tests/lean/exact_partial.lean.expected.out
+++ b/tests/lean/exact_partial.lean.expected.out
@@ -18,7 +18,7 @@ a_2 : b
 exact_partial.lean:5:0: error: don't know how to synthesize placeholder
 a b : Prop
 ⊢ a → b → a ∧ b
-exact_partial.lean:5:0: error: failed to add declaration '14.0' to environment, value has metavariables
+exact_partial.lean:5:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (a b : Prop),
     ?M_1
diff --git a/tests/lean/exact_partial2.lean.expected.out b/tests/lean/exact_partial2.lean.expected.out
index d470edfd8..9b253c2fd 100644
--- a/tests/lean/exact_partial2.lean.expected.out
+++ b/tests/lean/exact_partial2.lean.expected.out
@@ -15,7 +15,7 @@ a b c : nat,
 h₁ : a = b,
 h₂ : b = c
 ⊢ a = c
-exact_partial2.lean:4:0: error: failed to add declaration '14.0' to environment, value has metavariables
+exact_partial2.lean:4:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (a b c : nat) (h₁ : …) (h₂ : …),
     ?M_1
diff --git a/tests/lean/quasireducible.lean.expected.out b/tests/lean/quasireducible.lean.expected.out
index a624fd90e..76c01bdae 100644
--- a/tests/lean/quasireducible.lean.expected.out
+++ b/tests/lean/quasireducible.lean.expected.out
@@ -9,7 +9,7 @@ quasireducible.lean:11:3: error: don't know how to synthesize placeholder
 a : nat,
 H : f a = a
 ⊢ g a = a
-quasireducible.lean:11:3: error: failed to add declaration '14.1' to environment, value has metavariables
+quasireducible.lean:11:3: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (a : nat) (H : …),
     ?M_1
@@ -24,7 +24,7 @@ quasireducible.lean:16:3: error: don't know how to synthesize placeholder
 a : nat,
 H : f a = a
 ⊢ g a = a
-quasireducible.lean:16:3: error: failed to add declaration '14.2' to environment, value has metavariables
+quasireducible.lean:16:3: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (a : nat) (H : …),
     ?M_1
diff --git a/tests/lean/red.lean.expected.out b/tests/lean/red.lean.expected.out
index 4a7d5b669..2238b4df5 100644
--- a/tests/lean/red.lean.expected.out
+++ b/tests/lean/red.lean.expected.out
@@ -1,4 +1,4 @@
-red.lean:9:19: error: type mismatch at definition '14.1', has type
+red.lean:9:19: error: type mismatch at definition 'example', has type
   f = f
 but is expected to have type
   f = g
diff --git a/tests/lean/revert_fail.lean.expected.out b/tests/lean/revert_fail.lean.expected.out
index 6ac2c7c0d..eb8ff4155 100644
--- a/tests/lean/revert_fail.lean.expected.out
+++ b/tests/lean/revert_fail.lean.expected.out
@@ -9,7 +9,7 @@ A : Type,
 n : nat,
 v : vector A n
 ⊢ v = v
-revert_fail.lean:6:0: error: failed to add declaration '14.0' to environment, value has metavariables
+revert_fail.lean:6:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (A : Type) (n : nat) (v : …),
     ?M_1
@@ -19,7 +19,7 @@ no goals
 revert_fail.lean:12:0: error: don't know how to synthesize placeholder
 n : nat
 ⊢ n = n
-revert_fail.lean:12:0: error: failed to add declaration '14.1' to environment, value has metavariables
+revert_fail.lean:12:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (n : nat),
     ?M_1
@@ -30,7 +30,7 @@ n : nat
 revert_fail.lean:17:0: error: don't know how to synthesize placeholder
 n : nat
 ⊢ n = n
-revert_fail.lean:17:0: error: failed to add declaration '14.2' to environment, value has metavariables
+revert_fail.lean:17:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (n : nat),
     ?M_1
diff --git a/tests/lean/rewrite_fail.lean.expected.out b/tests/lean/rewrite_fail.lean.expected.out
index 2ecd71ab4..707c23e07 100644
--- a/tests/lean/rewrite_fail.lean.expected.out
+++ b/tests/lean/rewrite_fail.lean.expected.out
@@ -11,7 +11,7 @@ a b : ℕ,
 Ha : a = 0,
 Hb : b = 0
 ⊢ a + b = 0
-rewrite_fail.lean:6:0: error: failed to add declaration '14.0' to environment, value has metavariables
+rewrite_fail.lean:6:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (a b : ℕ) (Ha : …) (Hb : …),
     ?M_1
@@ -21,7 +21,7 @@ no goals
 rewrite_fail.lean:12:0: error: don't know how to synthesize placeholder
 a : ℕ
 ⊢ a = a
-rewrite_fail.lean:12:0: error: failed to add declaration '14.1' to environment, value has metavariables
+rewrite_fail.lean:12:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (a : ℕ),
     ?M_1
diff --git a/tests/lean/show_tac.lean.expected.out b/tests/lean/show_tac.lean.expected.out
index e823be637..a9b5fed35 100644
--- a/tests/lean/show_tac.lean.expected.out
+++ b/tests/lean/show_tac.lean.expected.out
@@ -12,7 +12,7 @@ Hab : a ∧ b,
 Ha : a,
 Hb : b
 ⊢ b ∧ a
-show_tac.lean:7:0: error: failed to add declaration '14.0' to environment, value has metavariables
+show_tac.lean:7:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (a b : Prop) (Hab : …),
     ?M_1
diff --git a/tests/lean/unsolved_proof_qed.lean.expected.out b/tests/lean/unsolved_proof_qed.lean.expected.out
index 271da0058..dbd2fbfb0 100644
--- a/tests/lean/unsolved_proof_qed.lean.expected.out
+++ b/tests/lean/unsolved_proof_qed.lean.expected.out
@@ -15,7 +15,7 @@ a b c : nat,
 H₁ : a = b,
 H₂ : b = c
 ⊢ a = c
-unsolved_proof_qed.lean:2:0: error: failed to add declaration '14.0' to environment, value has metavariables
+unsolved_proof_qed.lean:2:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (a b c : nat) (H₁ : …) (H₂ : …),
     ?M_1
@@ -36,7 +36,7 @@ a b c : nat,
 H₁ : a = b,
 H₂ : b = c
 ⊢ c = a
-unsolved_proof_qed.lean:5:0: error: failed to add declaration '14.1' to environment, value has metavariables
+unsolved_proof_qed.lean:5:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (a b c : nat) (H₁ : …) (H₂ : …),
     have aux : …, from ?M_1,
diff --git a/tests/lean/user_rec_crash.lean.expected.out b/tests/lean/user_rec_crash.lean.expected.out
index 4f945ca19..c58a7ffb0 100644
--- a/tests/lean/user_rec_crash.lean.expected.out
+++ b/tests/lean/user_rec_crash.lean.expected.out
@@ -7,7 +7,7 @@ user_rec_crash.lean:4:0: error: don't know how to synthesize placeholder
 a b : Prop,
 h : a ∧ b
 ⊢ a
-user_rec_crash.lean:4:0: error: failed to add declaration '14.0' to environment, value has metavariables
+user_rec_crash.lean:4:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (a b : Prop) (h : …),
     ?M_1