feat(frontends/lean): add 'class' command back

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/emacs/lean-syntax.el

@@ -14,7 +14,7 @@
     "axiom" "inductive" "with" "structure" "universe" "alias" "help" "environment"
     "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl"
     "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end"
-    "private" "using" "namespace" "builtin" "including" "instance" "section"
+    "private" "using" "namespace" "builtin" "including" "instance" "class" "section"
     "set_option" "add_rewrite" "extends")
   "lean keywords")
 

src/frontends/lean/class.cpp

@@ -12,15 +12,22 @@ Author: Leonardo de Moura
 
 namespace lean {
 struct class_entry {
+    bool  m_class_cmd;
     name  m_class;
-    name  m_instance;
+    name  m_instance; // only relevant if m_class_cmd == false
-    class_entry() {}
+    class_entry():m_class_cmd(false) {}
-    class_entry(name const & c, name const & i):m_class(c), m_instance(i) {}
+    explicit class_entry(name const & c):m_class_cmd(true), m_class(c) {}
+    class_entry(name const & c, name const & i):m_class_cmd(false), m_class(c), m_instance(i) {}
 };
 
 struct class_state {
     typedef rb_map<name, list<name>, name_quick_cmp> class_instances;
     class_instances m_instances;
+    void add_class(name const & c) {
+        auto it = m_instances.find(c);
+        if (!it)
+            m_instances.insert(c, list<name>());
+    }
     void add_instance(name const & c, name const & i) {
         auto it = m_instances.find(c);
         if (!it)
@@ -34,7 +41,10 @@ struct class_config {
     typedef class_state state;
     typedef class_entry entry;
     static void add_entry(environment const &, io_state const &, state & s, entry const & e) {
-        s.add_instance(e.m_class, e.m_instance);
+        if (e.m_class_cmd)
+            s.add_class(e.m_class);
+        else
+            s.add_instance(e.m_class, e.m_instance);
     }
     static name const & get_class_name() {
         static name g_class_name("class");
@@ -45,11 +55,18 @@ struct class_config {
         return g_key;
     }
     static void  write_entry(serializer & s, entry const & e) {
-        s << e.m_class << e.m_instance;
+        if (e.m_class_cmd)
+            s << true << e.m_class;
+        else
+            s << false << e.m_class << e.m_instance;
     }
     static entry read_entry(deserializer & d) {
         entry e;
-        d >> e.m_class >> e.m_instance;
+        d >> e.m_class_cmd;
+        if (e.m_class_cmd)
+            d >> e.m_class;
+        else
+            d >> e.m_class >> e.m_instance;
         return e;
     }
 };
@@ -57,16 +74,25 @@ struct class_config {
 template class scoped_ext<class_config>;
 typedef scoped_ext<class_config> class_ext;
 
+static void check_class(environment const & env, name const & c_name) {
+    declaration c_d = env.get(c_name);
+    if (c_d.is_definition() && !c_d.is_opaque())
+        throw exception(sstream() << "invalid class, '" << c_name << "' is a transparent definition");
+}
+
 name get_class_name(environment const & env, expr const & e) {
     if (!is_constant(e))
         throw exception("class expected, expression is not a constant");
     name const & c_name = const_name(e);
-    declaration c_d = env.get(c_name);
+    check_class(env, c_name);
-    if (c_d.is_definition() && !c_d.is_opaque())
-        throw exception(sstream() << "invalid class, '" << c_name << "' is a transparent definition");
     return c_name;
 }
 
+environment add_class(environment const & env, name const & n) {
+    check_class(env, n);
+    return class_ext::add_entry(env, get_dummy_ios(), class_entry(n));
+}
+
 environment add_instance(environment const & env, name const & n) {
     declaration d = env.get(n);
     expr type = d.get_type();
@@ -99,7 +125,21 @@ environment add_instance_cmd(parser & p) {
     return env;
 }
 
+environment add_class_cmd(parser & p) {
+    bool found = false;
+    environment env = p.env();
+    while (p.curr_is_identifier()) {
+        found    = true;
+        name c   = p.check_constant_next("invalid 'class' declaration, constant expected");
+        env = add_class(env, c);
+    }
+    if (!found)
+        throw parser_error("invalid 'class' declaration, at least one identifier expected", p.pos());
+    return env;
+}
+
 void register_class_cmds(cmd_table & r) {
     add_cmd(r, cmd_info("instance", "add a new instance", add_instance_cmd));
+    add_cmd(r, cmd_info("class",    "add a new class", add_class_cmd));
 }
 }

src/frontends/lean/class.h

@@ -11,6 +11,8 @@ Author: Leonardo de Moura
 #include "frontends/lean/cmd_table.h"
 
 namespace lean {
+/** \brief Add a new 'class' to the environment (if it is not already declared) */
+environment add_class(environment const & env, name const & n);
 /** \brief Add a new 'class instance' to the environment. */
 environment add_instance(environment const & env, name const & n);
 /** \brief Return true iff \c c was declared with \c add_class . */

src/frontends/lean/token_table.cpp

@@ -79,7 +79,7 @@ token_table init_token_table() {
                                "abbreviation", "inductive", "record", "renaming", "extends", "structure", "module", "universe",
                                "precedence", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
                                "exit", "set_option", "using", "calc_subst", "calc_refl", "calc_trans", "tactic_hint",
-                               "add_begin_end_tactic", "set_begin_end_tactic", "instance", "#erase_cache", nullptr};
+                               "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "#erase_cache", nullptr};
 
     pair<char const *, char const *> aliases[] =
         {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},

tests/lean/run/class11.lean

@@ -0,0 +1,9 @@
+import logic
+
+variable C {A : Type} : A → Prop
+class C
+
+variable f {A : Type} (a : A) {H : C a} : Prop
+
+definition g {A : Type} (a b : A) {H1 : C a} {H2 : C b} : Prop :=
+f a ∧ f b

tests/lean/run/indimp.lean

@@ -15,5 +15,5 @@ cons2   : A → list2 A → list2 A
 inductive and (A B : Prop) : Prop :=
 and_intro : A → B → and A B
 
-inductive class {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop) (f : T1 → T2) :=
+inductive cls {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop) (f : T1 → T2) :=
-mk : (∀x y : T1, R1 x y → R2 (f x) (f y)) → class R1 R2 f
+mk : (∀x y : T1, R1 x y → R2 (f x) (f y)) → cls R1 R2 f

tests/lean/run/rel.lean

@@ -3,17 +3,17 @@ using relation
 
 namespace is_equivalence
 
-  inductive class {T : Type} (R : T → T → Type) : Prop :=
+  inductive cls {T : Type} (R : T → T → Type) : Prop :=
-  mk : is_reflexive R → is_symmetric R → is_transitive R → class R
+  mk : is_reflexive R → is_symmetric R → is_transitive R → cls R
 
-  theorem is_reflexive {T : Type} {R : T → T → Type} {C : class R} : is_reflexive R :=
+  theorem is_reflexive {T : Type} {R : T → T → Type} {C : cls R} : is_reflexive R :=
-  class_rec (λx y z, x) C
+  cls_rec (λx y z, x) C
 
-  theorem is_symmetric {T : Type} {R : T → T → Type} {C : class R} : is_symmetric R :=
+  theorem is_symmetric {T : Type} {R : T → T → Type} {C : cls R} : is_symmetric R :=
-  class_rec (λx y z, y) C
+  cls_rec (λx y z, y) C
 
-  theorem is_transitive {T : Type} {R : T → T → Type} {C : class R} : is_transitive R :=
+  theorem is_transitive {T : Type} {R : T → T → Type} {C : cls R} : is_transitive R :=
-  class_rec (λx y z, z) C
+  cls_rec (λx y z, z) C
 
 end is_equivalence