From e59456c19f9841b58db68330b4040fb113458ac7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 8 May 2015 16:45:13 -0700
Subject: [PATCH] feat(frontends/lean): remove 'opaque' keyword

see issue #576
---
 src/emacs/lean-syntax.el           |  2 +-
 src/frontends/lean/decl_cmds.cpp   | 45 +++++++++---------------------
 src/frontends/lean/token_table.cpp |  2 +-
 src/frontends/lean/tokens.cpp      |  4 ---
 src/frontends/lean/tokens.h        |  1 -
 5 files changed, 15 insertions(+), 39 deletions(-)

diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index 179b91387..f680bcb16 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -8,7 +8,7 @@
 (require 'rx)
 
 (defconst lean-keywords
-  '("import" "prelude" "tactic_hint" "protected" "private" "opaque" "definition" "renaming"
+  '("import" "prelude" "tactic_hint" "protected" "private" "definition" "renaming"
     "hiding" "exposing" "parameter" "parameters" "begin" "begin+" "proof" "qed" "conjecture" "constant" "constants"
     "hypothesis" "lemma" "corollary" "variable" "variables" "premise" "premises"
     "print" "theorem" "example" "abbreviation"
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 6ea141570..465ca6e88 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -858,7 +858,6 @@ class definition_cmd_fn {
     parser &          m_p;
     environment       m_env;
     def_cmd_kind      m_kind;
-    bool              m_is_opaque;
     bool              m_is_private;
     bool              m_is_protected;
     pos_info          m_pos;
@@ -1261,11 +1260,10 @@ class definition_cmd_fn {
     }
 
 public:
-    definition_cmd_fn(parser & p, def_cmd_kind kind, bool is_opaque, bool is_private, bool is_protected):
-        m_p(p), m_env(m_p.env()), m_kind(kind), m_is_opaque(is_opaque),
+    definition_cmd_fn(parser & p, def_cmd_kind kind, bool is_private, bool is_protected):
+        m_p(p), m_env(m_p.env()), m_kind(kind),
         m_is_private(is_private), m_is_protected(is_protected),
         m_pos(p.pos()), m_attributes(true, kind == Abbreviation || kind == LocalAbbreviation) {
-        lean_assert(!(!is_definition() && !m_is_opaque));
         lean_assert(!(m_is_private && m_is_protected));
     }
 
@@ -1291,36 +1289,27 @@ public:
     }
 };
 
-static environment definition_cmd_core(parser & p, def_cmd_kind kind, bool is_opaque, bool is_private, bool is_protected) {
-    return definition_cmd_fn(p, kind, is_opaque, is_private, is_protected)();
+static environment definition_cmd_core(parser & p, def_cmd_kind kind, bool is_private, bool is_protected) {
+    return definition_cmd_fn(p, kind, is_private, is_protected)();
 }
 static environment definition_cmd(parser & p) {
-    return definition_cmd_core(p, Definition, false, false, false);
+    return definition_cmd_core(p, Definition, false, false);
 }
 static environment abbreviation_cmd(parser & p) {
-    return definition_cmd_core(p, Abbreviation, false, false, false);
+    return definition_cmd_core(p, Abbreviation, false, false);
 }
 environment local_abbreviation_cmd(parser & p) {
-    return definition_cmd_core(p, LocalAbbreviation, false, true, false);
-}
-static environment opaque_definition_cmd(parser & p) {
-    p.check_token_next(get_definition_tk(), "invalid 'opaque' definition, 'definition' expected");
-    return definition_cmd_core(p, Definition, true, false, false);
+    return definition_cmd_core(p, LocalAbbreviation, true, false);
 }
 static environment theorem_cmd(parser & p) {
-    return definition_cmd_core(p, Theorem, true, false, false);
+    return definition_cmd_core(p, Theorem, false, false);
 }
 static environment example_cmd(parser & p) {
-    return definition_cmd_core(p, Example, true, false, false);
+    return definition_cmd_core(p, Example, false, false);
 }
 static environment private_definition_cmd(parser & p) {
     def_cmd_kind kind = Definition;
-    bool is_opaque  = false;
-    if (p.curr_is_token_or_id(get_opaque_tk())) {
-        is_opaque = true;
-        p.next();
-        p.check_token_next(get_definition_tk(), "invalid 'private' definition, 'definition' expected");
-    } else if (p.curr_is_token_or_id(get_definition_tk())) {
+    if (p.curr_is_token_or_id(get_definition_tk())) {
         p.next();
     } else if (p.curr_is_token_or_id(get_abbreviation_tk())) {
         kind = Abbreviation;
@@ -1328,11 +1317,10 @@ static environment private_definition_cmd(parser & p) {
     } else if (p.curr_is_token_or_id(get_theorem_tk())) {
         p.next();
         kind = Theorem;
-        is_opaque  = true;
     } else {
         throw parser_error("invalid 'private' definition/theorem, 'definition' or 'theorem' expected", p.pos());
     }
-    return definition_cmd_core(p, kind, is_opaque, true, false);
+    return definition_cmd_core(p, kind, true, false);
 }
 static environment protected_definition_cmd(parser & p) {
     if (p.curr_is_token_or_id(get_axiom_tk())) {
@@ -1349,12 +1337,7 @@ static environment protected_definition_cmd(parser & p) {
         return variables_cmd_core(p, variable_kind::Constant, true);
     } else {
         def_cmd_kind kind = Definition;
-        bool is_opaque  = false;
-        if (p.curr_is_token_or_id(get_opaque_tk())) {
-            is_opaque = true;
-            p.next();
-            p.check_token_next(get_definition_tk(), "invalid 'protected' definition, 'definition' expected");
-        } else if (p.curr_is_token_or_id(get_definition_tk())) {
+        if (p.curr_is_token_or_id(get_definition_tk())) {
             p.next();
         } else if (p.curr_is_token_or_id(get_abbreviation_tk())) {
             p.next();
@@ -1362,11 +1345,10 @@ static environment protected_definition_cmd(parser & p) {
         } else if (p.curr_is_token_or_id(get_theorem_tk())) {
             p.next();
             kind       = Theorem;
-            is_opaque  = true;
         } else {
             throw parser_error("invalid 'protected' definition/theorem, 'definition' or 'theorem' expected", p.pos());
         }
-        return definition_cmd_core(p, kind, is_opaque, false, true);
+        return definition_cmd_core(p, kind, false, true);
     }
 }
 
@@ -1438,7 +1420,6 @@ void register_decl_cmds(cmd_table & r) {
     add_cmd(r, cmd_info("axioms",       "declare new axioms", axioms_cmd));
     add_cmd(r, cmd_info("definition",   "add new definition", definition_cmd));
     add_cmd(r, cmd_info("example",      "add new example", example_cmd));
-    add_cmd(r, cmd_info("opaque",       "add new opaque definition", opaque_definition_cmd));
     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));
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 2ebb677c5..370902fd9 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", "opaque",
+        {"theorem", "axiom", "axioms", "variable", "protected", "private",
          "definition", "example", "coercion", "abbreviation",
          "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]",
          "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]", "[quasireducible]",
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index dfc972034..93355f5cc 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -101,7 +101,6 @@ static name * g_constant     = nullptr;
 static name * g_constants    = nullptr;
 static name * g_variable     = nullptr;
 static name * g_variables    = nullptr;
-static name * g_opaque       = nullptr;
 static name * g_instance     = nullptr;
 static name * g_priority     = nullptr;
 static name * g_unfold_c     = nullptr;
@@ -230,7 +229,6 @@ void initialize_tokens() {
     g_definition   = new name("definition");
     g_theorem      = new name("theorem");
     g_abbreviation = new name("abbreviation");
-    g_opaque       = new name("opaque");
     g_axiom        = new name("axiom");
     g_axioms       = new name("axioms");
     g_constant     = new name("constant");
@@ -303,7 +301,6 @@ void finalize_tokens() {
     delete g_definition;
     delete g_theorem;
     delete g_abbreviation;
-    delete g_opaque;
     delete g_axiom;
     delete g_axioms;
     delete g_constant;
@@ -509,7 +506,6 @@ name const & get_constant_tk() { return *g_constant; }
 name const & get_constants_tk() { return *g_constants; }
 name const & get_variable_tk() { return *g_variable; }
 name const & get_variables_tk() { return *g_variables; }
-name const & get_opaque_tk() { return *g_opaque; }
 name const & get_instance_tk() { return *g_instance; }
 name const & get_priority_tk() { return *g_priority; }
 name const & get_unfold_c_tk() { return *g_unfold_c; }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index 10e31db3d..975107570 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -103,7 +103,6 @@ name const & get_constant_tk();
 name const & get_constants_tk();
 name const & get_variable_tk();
 name const & get_variables_tk();
-name const & get_opaque_tk();
 name const & get_instance_tk();
 name const & get_priority_tk();
 name const & get_unfold_c_tk();