From 4e35afedcc10d18a23b9bc56a2c2f756d0f0827c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 8 May 2015 20:54:16 -0700
Subject: [PATCH] feat(frontends/lean): rename 'wait' to 'reveal'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/emacs/lean-syntax.el           |  2 +-
 src/frontends/lean/decl_cmds.cpp   | 10 +++++-----
 src/frontends/lean/parser.cpp      |  2 +-
 src/frontends/lean/parser.h        |  2 +-
 src/frontends/lean/token_table.cpp |  2 +-
 tests/lean/hott/tele_eq.hlean      |  2 +-
 tests/lean/run/calc_heq_symm.lean  |  2 +-
 tests/lean/run/class2.lean         |  2 +-
 tests/lean/run/class3.lean         |  2 +-
 tests/lean/run/class8.lean         |  2 +-
 tests/lean/run/dfun_tst.lean       |  2 +-
 tests/lean/run/local_eqns.lean     |  2 +-
 tests/lean/run/match_tac3.lean     |  2 +-
 tests/lean/run/match_tac4.lean     |  4 ++--
 tests/lean/run/revert_tac.lean     |  2 +-
 tests/lean/run/reverts_tac.lean    |  2 +-
 tests/lean/run/rewriter1.lean      |  2 +-
 tests/lean/run/rewriter2.lean      |  2 +-
 tests/lean/run/tactic21.lean       |  2 +-
 tests/lean/run/tele_eq.lean        |  2 +-
 20 files changed, 25 insertions(+), 25 deletions(-)

diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index 8fa1ffd21a..14271f2226 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -16,7 +16,7 @@
     "alias" "help" "environment" "options" "precedence" "reserve"
     "match" "infix" "infixl" "infixr" "notation" "postfix" "prefix"
     "tactic_infix" "tactic_infixl" "tactic_infixr" "tactic_notation" "tactic_postfix" "tactic_prefix"
-    "eval" "check" "coercion" "end" "wait"
+    "eval" "check" "coercion" "end" "reveal"
     "using" "namespace" "section" "fields" "find_decl"
     "attribute" "local" "set_option" "add_rewrite" "extends" "include" "omit" "classes"
     "instances" "coercions" "metaclasses" "raw" "migrate" "replacing")
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 826ab748a2..01af415dd9 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -1410,14 +1410,14 @@ environment local_attribute_cmd(parser & p) {
     return attribute_cmd_core(p, false);
 }
 
-static environment wait_cmd(parser & p) {
+static environment reveal_cmd(parser & p) {
     buffer<name> ds;
-    name d          = p.check_constant_next("invalid 'wait' command, constant expected");
+    name d          = p.check_constant_next("invalid 'reveal' command, constant expected");
     ds.push_back(d);
     while (p.curr_is_identifier()) {
-        ds.push_back(p.check_constant_next("invalid 'wait' command, constant expected"));
+        ds.push_back(p.check_constant_next("invalid 'reveal' command, constant expected"));
     }
-    return p.wait_theorems(ds);
+    return p.reveal_theorems(ds);
 }
 
 void register_decl_cmds(cmd_table & r) {
@@ -1436,7 +1436,7 @@ void register_decl_cmds(cmd_table & r) {
     add_cmd(r, cmd_info("private",      "add new private definition/theorem", private_definition_cmd));
     add_cmd(r, cmd_info("protected",    "add new protected definition/theorem", protected_definition_cmd));
     add_cmd(r, cmd_info("theorem",      "add new theorem", theorem_cmd));
-    add_cmd(r, cmd_info("wait",         "wait for theorems to be processed", wait_cmd));
+    add_cmd(r, cmd_info("reveal",       "reveal given theorems", reveal_cmd));
     add_cmd(r, cmd_info("include",      "force section parameter/variable to be included", include_cmd));
     add_cmd(r, cmd_info("attribute",    "set declaration attributes", attribute_cmd));
     add_cmd(r, cmd_info("abbreviation", "declare a new abbreviation", abbreviation_cmd));
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 2fc25e82b9..90a9f10f21 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1821,7 +1821,7 @@ void parser::add_delayed_theorem(certified_declaration const & cd) {
     m_theorem_queue.add(cd);
 }
 
-environment parser::wait_theorems(buffer<name> const & ds) {
+environment parser::reveal_theorems(buffer<name> const & ds) {
     m_theorem_queue.for_each([&](certified_declaration const & thm) {
             if (keep_new_thms()) {
                 name const & thm_name = thm.get_declaration().get_name();
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index da997c6daf..705535855f 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -301,7 +301,7 @@ public:
     unsigned num_threads() const { return m_num_threads; }
     void add_delayed_theorem(environment const & env, name const & n, level_param_names const & ls, expr const & t, expr const & v);
     void add_delayed_theorem(certified_declaration const & cd);
-    environment wait_theorems(buffer<name> const & ds);
+    environment reveal_theorems(buffer<name> const & ds);
 
     /** \brief Read the next token. */
     void scan() { m_curr = m_scanner.scan(m_env); }
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index ad23663d35..44c8defb0f 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -103,7 +103,7 @@ void init_token_table(token_table & t) {
          {"<d", g_decreasing_prec}, {"renaming", 0}, {"extends", 0}, {nullptr, 0}};
 
     char const * commands[] =
-        {"theorem", "axiom", "axioms", "variable", "protected", "private", "wait",
+        {"theorem", "axiom", "axioms", "variable", "protected", "private", "reveal",
          "definition", "example", "coercion", "abbreviation",
          "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]",
          "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]", "[quasireducible]",
diff --git a/tests/lean/hott/tele_eq.hlean b/tests/lean/hott/tele_eq.hlean
index 4be2dfbf0c..f38bf4b3d1 100644
--- a/tests/lean/hott/tele_eq.hlean
+++ b/tests/lean/hott/tele_eq.hlean
@@ -14,5 +14,5 @@ begin
   cases H₃,
   apply rfl
 end
-wait foo.eq
+reveal foo.eq
 print definition foo.eq
diff --git a/tests/lean/run/calc_heq_symm.lean b/tests/lean/run/calc_heq_symm.lean
index d185140cba..00483999fd 100644
--- a/tests/lean/run/calc_heq_symm.lean
+++ b/tests/lean/run/calc_heq_symm.lean
@@ -7,5 +7,5 @@ calc d  == c  : H₃
     ... == a₂ : H₁
     ... =  a₁ : H₀
 
-wait tst
+reveal tst
 print definition tst
diff --git a/tests/lean/run/class2.lean b/tests/lean/run/class2.lean
index d9950943f9..9768fea993 100644
--- a/tests/lean/run/class2.lean
+++ b/tests/lean/run/class2.lean
@@ -3,7 +3,7 @@ open prod nonempty inhabited
 
 theorem H {A B : Type} (H1 : inhabited A) : inhabited (Prop × A × (B → num))
 := _
-wait H
+reveal H
 (*
 print(get_env():find("H"):value())
 *)
diff --git a/tests/lean/run/class3.lean b/tests/lean/run/class3.lean
index 1aa1c14d54..2b3b0f8076 100644
--- a/tests/lean/run/class3.lean
+++ b/tests/lean/run/class3.lean
@@ -11,7 +11,7 @@ section
 
 end
 
-wait tst
+reveal tst
 (*
 print(get_env():find("tst"):value())
 *)
diff --git a/tests/lean/run/class8.lean b/tests/lean/run/class8.lean
index 5d2d72c8dc..522d42e2fb 100644
--- a/tests/lean/run/class8.lean
+++ b/tests/lean/run/class8.lean
@@ -32,7 +32,7 @@ have h1 [visible] : inh A, from inh.intro a,
 have h2 [visible] : inh C, from inh_exists H2,
 _
 
-wait T1
+reveal T1
 (*
 print(get_env():find("T1"):value())
 *)
diff --git a/tests/lean/run/dfun_tst.lean b/tests/lean/run/dfun_tst.lean
index 35308ae982..ffb5f777bd 100644
--- a/tests/lean/run/dfun_tst.lean
+++ b/tests/lean/run/dfun_tst.lean
@@ -5,7 +5,7 @@ theorem tst1 : inhabited (vector nat 2)
 
 theorem tst2 : inhabited (Prop × (Π n : nat, vector nat n))
 
-wait tst2
+reveal tst2
 (*
 print(get_env():find("tst2"):value())
 *)
diff --git a/tests/lean/run/local_eqns.lean b/tests/lean/run/local_eqns.lean
index 6cb802d9ba..ff0b07874e 100644
--- a/tests/lean/run/local_eqns.lean
+++ b/tests/lean/run/local_eqns.lean
@@ -64,5 +64,5 @@ theorem add_eq_addl : ∀ x y, x + y = x ⊕ y
     rewrite [s_add, add_eq_addl]
   end
 
-wait add_eq_addl
+reveal add_eq_addl
 print definition add_eq_addl
diff --git a/tests/lean/run/match_tac3.lean b/tests/lean/run/match_tac3.lean
index d025cba4a5..efc05ea4d1 100644
--- a/tests/lean/run/match_tac3.lean
+++ b/tests/lean/run/match_tac3.lean
@@ -10,5 +10,5 @@ begin
   end
 end
 
-wait tst
+reveal tst
 print definition tst
diff --git a/tests/lean/run/match_tac4.lean b/tests/lean/run/match_tac4.lean
index 30ea2b7530..787cc25dc3 100644
--- a/tests/lean/run/match_tac4.lean
+++ b/tests/lean/run/match_tac4.lean
@@ -22,7 +22,7 @@ begin
   end
 end
 
-wait tst
+reveal tst
 print definition tst
 
 theorem tst2 (a b c d : Prop) : a ∧ b ∧ c ∧ d ↔ d ∧ c ∧ b ∧ a :=
@@ -31,5 +31,5 @@ begin
   repeat (intro H;  repeat (cases H with [H', H] | apply and.intro | assumption))
 end
 
-wait tst2
+reveal tst2
 print definition tst2
diff --git a/tests/lean/run/revert_tac.lean b/tests/lean/run/revert_tac.lean
index 5d1be5ae4b..d06c1813aa 100644
--- a/tests/lean/run/revert_tac.lean
+++ b/tests/lean/run/revert_tac.lean
@@ -23,7 +23,7 @@ begin
   apply (eq.rec_on Heq Hp)
 end
 
-wait foo1 foo2
+reveal foo1 foo2
 
 print definition foo1
 print definition foo2
diff --git a/tests/lean/run/reverts_tac.lean b/tests/lean/run/reverts_tac.lean
index fa3ed92242..33fb4b3731 100644
--- a/tests/lean/run/reverts_tac.lean
+++ b/tests/lean/run/reverts_tac.lean
@@ -24,6 +24,6 @@ begin
   apply (eq.rec_on Heq Hp)
 end
 
-wait foo1 foo2
+reveal foo1 foo2
 print definition foo1
 print definition foo2
diff --git a/tests/lean/run/rewriter1.lean b/tests/lean/run/rewriter1.lean
index b984b70861..92c368b7bc 100644
--- a/tests/lean/run/rewriter1.lean
+++ b/tests/lean/run/rewriter1.lean
@@ -6,5 +6,5 @@ begin
   rewrite [add.assoc, {b + _}add.comm, -add.assoc]
 end
 
-wait test
+reveal test
 print definition test
diff --git a/tests/lean/run/rewriter2.lean b/tests/lean/run/rewriter2.lean
index c31743f893..8ff802d00f 100644
--- a/tests/lean/run/rewriter2.lean
+++ b/tests/lean/run/rewriter2.lean
@@ -25,7 +25,7 @@ begin
   rewrite [+mul_zero, +zero_mul, +add_zero] -- in rewrite rules, + is notation for one or more
 end
 
-wait test3
+reveal test3
 print definition test3
 
 theorem test4 {A : Type} [s : comm_ring A] (a b c : A) : a * 0 + 0 * b + c * 0 + 0 * a = 0 :=
diff --git a/tests/lean/run/tactic21.lean b/tests/lean/run/tactic21.lean
index d66a1a97e6..c4f94cd49e 100644
--- a/tests/lean/run/tactic21.lean
+++ b/tests/lean/run/tactic21.lean
@@ -7,7 +7,7 @@ theorem tst1 {A : Type} {a b c : A} {p : A → A → Prop} (H1 : p a b) (H2 : p
 theorem tst2 {A : Type} {a b c d : A} {p : A → A → Prop} (Ha : p a c) (H1 : p a b) (Hb : p b d) (H2 : p b c) : ∃ x, p a x ∧ p x c
 := by apply exists.intro; apply and.intro; eassumption; eassumption
 
-wait tst2
+reveal tst2
 (*
 print(get_env():find("tst2"):value())
 *)
diff --git a/tests/lean/run/tele_eq.lean b/tests/lean/run/tele_eq.lean
index ab00d3d54e..4c0f9886d3 100644
--- a/tests/lean/run/tele_eq.lean
+++ b/tests/lean/run/tele_eq.lean
@@ -15,5 +15,5 @@ begin
   apply rfl
 end
 
-wait foo.eq
+reveal foo.eq
 print definition foo.eq