feat(frontends/lean): add 'class' and 'instances' infrastructure

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

library/standard/bit.lean

@@ -1,10 +1,14 @@
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
+import logic
 namespace bit
 inductive bit : Type :=
 | b0 : bit
 | b1 : bit
 notation `'0` := b0
 notation `'1` := b1
+
+theorem inhabited_bit [instance] : inhabited bit
+:= inhabited_intro b0
 end

library/standard/logic.lean

@@ -193,13 +193,15 @@ theorem exists_unique_elim {A : Type} {p : A → Bool} {b : Bool} (H2 : ∃! x,
 inductive inhabited (A : Type) : Bool :=
 | inhabited_intro : A → inhabited A
 
+class inhabited
+
 theorem inhabited_elim {A : Type} {B : Bool} (H1 : inhabited A) (H2 : A → B) : B
 := inhabited_rec H2 H1
 
-theorem inhabited_Bool : inhabited Bool
+theorem inhabited_Bool [instance] : inhabited Bool
 := inhabited_intro true
 
-theorem inhabited_fun (A : Type) {B : Type} (H : inhabited B) : inhabited (A → B)
+theorem inhabited_fun [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A → B)
 := inhabited_elim H (take (b : B), inhabited_intro (λ a : A, b))
 
 definition cast {A B : Type} (H : A = B) (a : A) : B

library/standard/num.lean

@@ -1,6 +1,7 @@
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
+import logic
 namespace num
 -- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26.
 -- The parser will generate the terms (pos (bit1 (bit1 (bit0 one)))), zero, and (pos (bit0 (bit1 (bit1 one)))).
@@ -14,4 +15,9 @@ inductive num : Type :=
 | zero  : num
 | pos   : pos_num → num
 
+theorem inhabited_pos_num [instance] : inhabited pos_num
+:= inhabited_intro one
+
+theorem inhabited_num [instance] : inhabited num
+:= inhabited_intro zero
 end

library/standard/option.lean

@@ -7,5 +7,5 @@ inductive option (A : Type) : Type :=
 | none {} : option A
 | some    : A → option A
 
-theorem inhabited_option (A : Type) : inhabited (option A)
+theorem inhabited_option [instance] (A : Type) : inhabited (option A)
 := inhabited_intro none

library/standard/pair.lean

@@ -13,7 +13,7 @@ section
   definition fst [inline] (p : pair A B) := pair_rec (λ x y, x) p
   definition snd [inline] (p : pair A B) := pair_rec (λ x y, y) p
 
-  theorem pair_inhabited (H1 : inhabited A) (H2 : inhabited B) : inhabited (pair A B)
+  theorem pair_inhabited [instance] (H1 : inhabited A) (H2 : inhabited B) : inhabited (pair A B)
   := inhabited_elim H1 (λ a, inhabited_elim H2 (λ b, inhabited_intro (mk_pair a b)))
 
   theorem fst_mk_pair (a : A) (b : B) : fst (mk_pair a b) = a
@@ -28,4 +28,3 @@ end
 
 -- notation for n-ary tuples
 notation `(` h `,` t:(foldl `,` (e r, mk_pair r e) h) `)` := t
-

library/standard/string.lean

@@ -11,4 +11,10 @@ inductive char : Type :=
 inductive string : Type :=
 | empty : string
 | str   : char → string → string
+
+theorem inhabited_char [instance] : inhabited char
+:= inhabited_intro (ascii b0 b0 b0 b0 b0 b0 b0 b0)
+
+theorem inhabited_string [instance] : inhabited string
+:= inhabited_intro empty
 end

library/standard/unit.lean

@@ -6,5 +6,5 @@ import logic
 inductive unit : Type :=
 | tt : unit
 
-theorem inhabited_unit : inhabited unit
+theorem inhabited_unit [instance] : inhabited unit
 := inhabited_intro tt

src/emacs/lean-mode.el

@@ -24,7 +24,7 @@
 (define-generic-mode
     'lean-mode     ;; name of the mode to create
   '("--")          ;; comments start with
-  '("import" "abbreviation" "definition" "parameter" "parameters" "proof" "qed" "conjecture" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "axiom" "inductive" "with" "universe" "alias" "help" "environment" "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "builtin" "section" "set_option" "add_rewrite") ;; some keywords
+  '("import" "abbreviation" "definition" "parameter" "parameters" "proof" "qed" "conjecture" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "axiom" "inductive" "with" "universe" "alias" "help" "environment" "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "builtin" "class" "instance" "section" "set_option" "add_rewrite") ;; some keywords
   '(("\\_<\\(Bool\\|Int\\|Nat\\|Real\\|Type\\|TypeU\\|ℕ\\|ℤ\\)\\_>" . 'font-lock-type-face)
     ("\\_<\\(calc\\|have\\|show\\|by\\|in\\|let\\|forall\\|fun\\|exists\\|if\\|then\\|else\\|assume\\|take\\|obtain\\|from\\)\\_>" . font-lock-keyword-face)
     ("\"[^\"]*\"" . 'font-lock-string-face)

src/frontends/lean/CMakeLists.txt

@@ -3,6 +3,7 @@ scanner.cpp parse_table.cpp parser_config.cpp parser.cpp
 parser_pos_provider.cpp builtin_cmds.cpp builtin_exprs.cpp
 interactive.cpp notation_cmd.cpp calc.cpp
 decl_cmds.cpp util.cpp inductive_cmd.cpp elaborator.cpp
-dependencies.cpp parser_bindings.cpp proof_qed_ext.cpp)
+dependencies.cpp parser_bindings.cpp proof_qed_ext.cpp
+class.cpp)
 
 target_link_libraries(lean_frontend ${LEAN_LIBS})

src/frontends/lean/builtin_cmds.cpp

@@ -21,6 +21,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/inductive_cmd.h"
 #include "frontends/lean/proof_qed_ext.h"
 #include "frontends/lean/decl_cmds.h"
+#include "frontends/lean/class.h"
 
 namespace lean {
 static name g_raw("raw");
@@ -248,6 +249,7 @@ cmd_table init_cmd_table() {
     register_notation_cmds(r);
     register_calc_cmds(r);
     register_proof_qed_cmds(r);
+    register_class_cmds(r);
     return r;
 }
 

src/frontends/lean/class.cpp

@@ -0,0 +1,125 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <string>
+#include "util/sstream.h"
+#include "library/scoped_ext.h"
+#include "library/kernel_serializer.h"
+#include "frontends/lean/parser.h"
+
+namespace lean {
+struct class_entry {
+    enum class kind { NewClass, NewInstance };
+    kind  m_kind;
+    name  m_class;
+    name  m_instance;
+    class_entry() {}
+    class_entry(name const & c):m_kind(kind::NewClass), m_class(c) {}
+    class_entry(name const & c, name const & i):m_kind(kind::NewInstance), m_class(c), m_instance(i) {}
+    bool is_new_class() const { return m_kind == kind::NewClass; }
+};
+
+struct class_state {
+    typedef rb_map<name, list<name>, name_quick_cmp> class_instances;
+    class_instances m_instances;
+    void add_class(name const & c) {
+        m_instances.insert(c, list<name>());
+    }
+    void add_instance(name const & c, name const & i) {
+        auto it = m_instances.find(c);
+        if (!it) throw exception(sstream() << "invalid instance, unknown class '" << c << "'");
+        m_instances.insert(c, cons(i, filter(*it, [&](name const & i1) { return i1 != i; })));
+    }
+};
+
+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) {
+        if (e.m_kind == class_entry::kind::NewClass)
+            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");
+        return g_class_name;
+    }
+    static std::string const & get_serialization_key() {
+        static std::string g_key("class");
+        return g_key;
+    }
+    static void  write_entry(serializer & s, entry const & e) {
+        s.write_char(static_cast<char>(e.m_kind)); // NOLINT
+        if (e.is_new_class())
+            s << e.m_class;
+        else
+            s << e.m_class << e.m_instance;
+    }
+    static entry read_entry(deserializer & d) {
+        entry e;
+        e.m_kind = static_cast<class_entry::kind>(d.read_char());
+        if (e.is_new_class())
+            d >> e.m_class;
+        else
+            d >> e.m_class >> e.m_instance;
+        return e;
+    }
+};
+
+template class scoped_ext<class_config>;
+typedef scoped_ext<class_config> class_ext;
+
+environment add_class(environment const & env, name const & n) {
+    declaration d = env.get(n);
+    if (d.is_definition() && !d.is_opaque())
+        throw exception(sstream() << "invalid class declaration, '" << n << "' is not an opaque definition");
+    class_state const & s = class_ext::get_state(env);
+    if (s.m_instances.contains(n))
+        throw exception(sstream() << "class '" << n << "' has already been declared");
+    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();
+    while (is_pi(type))
+        type = binding_body(type);
+    if (!is_constant(get_app_fn(type)))
+        throw exception(sstream() << "invalid class instance declaration '" << n << "' resultant type must be a class");
+    name const & c = const_name(get_app_fn(type));
+    return class_ext::add_entry(env, get_dummy_ios(), class_entry(c, n));
+}
+
+list<name> get_class_instances(environment const & env, name const & c) {
+    class_state const & s = class_ext::get_state(env);
+    if (auto it = s.m_instances.find(c))
+        return *it;
+    else
+        return list<name>();
+}
+
+environment add_class_cmd(parser & p) {
+    auto pos = p.pos();
+    name c   = p.check_id_next("invalid 'class' declaration, identifier expected");
+    expr e   = p.id_to_expr(c, pos);
+    if (!is_constant(e)) throw parser_error(sstream() << "invalid 'class' declaration, '" << c << "' is not a constant", pos);
+    return add_class(p.env(), const_name(e));
+}
+
+environment add_instance_cmd(parser & p) {
+    auto pos = p.pos();
+    name c   = p.check_id_next("invalid 'class instance' declaration, identifier expected");
+    expr e   = p.id_to_expr(c, pos);
+    if (!is_constant(e)) throw parser_error(sstream() << "invalid 'class instance' declaration, '" << c << "' is not a constant", pos);
+    return add_instance(p.env(), const_name(e));
+}
+
+void register_class_cmds(cmd_table & r) {
+    add_cmd(r, cmd_info("class", "add a new class", add_class_cmd));
+    add_cmd(r, cmd_info("instance", "add a new instance", add_instance_cmd));
+}
+}

src/frontends/lean/class.h

@@ -0,0 +1,22 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "util/name.h"
+#include "util/list.h"
+#include "kernel/environment.h"
+#include "frontends/lean/cmd_table.h"
+
+namespace lean {
+/** \brief Add a new 'class' to the environment. */
+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 the instances of the given class. */
+list<name> get_class_instances(environment const & env, name const & c);
+
+void register_class_cmds(cmd_table & r);
+}

src/frontends/lean/decl_cmds.cpp

@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "library/explicit.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/util.h"
+#include "frontends/lean/class.h"
 
 namespace lean {
 static name g_llevel_curly(".{");
@@ -23,6 +24,8 @@ static name g_colon(":");
 static name g_assign(":=");
 static name g_private("[private]");
 static name g_inline("[inline]");
+static name g_instance("[instance]");
+static name g_class("[class]");
 
 environment universe_cmd(parser & p) {
     name n = p.check_id_next("invalid universe declaration, identifier expected");
@@ -152,19 +155,38 @@ void collect_section_locals(expr const & type, expr const & value, parser const
     return mk_section_params(ls, p, section_ps);
 }
 
-static void parse_modifiers(parser & p, bool & is_private, bool & is_opaque) {
-    while (true) {
-        if (p.curr_is_token(g_private)) {
-            is_private = true;
-            p.next();
-        } else if (p.curr_is_token(g_inline)) {
-            is_opaque = false;
-            p.next();
-        } else {
-            break;
+struct decl_modifiers {
+    bool m_is_private;
+    bool m_is_opaque;
+    bool m_is_instance;
+    bool m_is_class;
+    decl_modifiers() {
+        m_is_private  = false;
+        m_is_opaque   = true;
+        m_is_instance = false;
+        m_is_class    = false;
+    }
+
+    void parse(parser & p) {
+        while (true) {
+            if (p.curr_is_token(g_private)) {
+                m_is_private = true;
+                p.next();
+            } else if (p.curr_is_token(g_inline)) {
+                m_is_opaque = false;
+                p.next();
+            } else if (p.curr_is_token(g_instance)) {
+                m_is_instance = true;
+                p.next();
+            } else if (p.curr_is_token(g_class)) {
+                m_is_class = true;
+                p.next();
+            } else {
+                break;
+            }
         }
     }
-}
+};
 
 // Return the levels in \c ls that are defined in the section
 levels collect_section_levels(level_param_names const & ls, parser & p) {
@@ -178,16 +200,17 @@ levels collect_section_levels(level_param_names const & ls, parser & p) {
     return to_list(section_ls_buffer.begin(), section_ls_buffer.end());
 }
 
-environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque) {
+environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
     name n = p.check_id_next("invalid declaration, identifier expected");
     check_atomic(n);
-    bool is_private = false;
-    parse_modifiers(p, is_private, is_opaque);
-    if (is_theorem && !is_opaque)
+    decl_modifiers modifiers;
+    modifiers.m_is_opaque = _is_opaque;
+    modifiers.parse(p);
+    if (is_theorem && !modifiers.m_is_opaque)
         throw exception("invalid theorem declaration, theorems cannot be transparent");
     environment env = p.env();
     name real_n; // real name for this declaration
-    if (is_private) {
+    if (modifiers.m_is_private) {
         auto env_n = add_private_name(env, n, optional<unsigned>(hash(p.pos().first, p.pos().second)));
         env    = env_n.first;
         real_n = env_n.second;
@@ -257,8 +280,12 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque) {
         auto type_value = p.elaborate(n, type, value);
         type  = type_value.first;
         value = type_value.second;
-        env = module::add(env, check(env, mk_definition(env, real_n, ls, type, value, is_opaque)));
+        env = module::add(env, check(env, mk_definition(env, real_n, ls, type, value, modifiers.m_is_opaque)));
     }
+    if (modifiers.m_is_class)
+        env = add_class(env, real_n);
+    if (modifiers.m_is_instance)
+        env = add_instance(env, real_n);
     return env;
 }
 environment definition_cmd(parser & p) {

src/frontends/lean/token_table.cpp

@@ -63,12 +63,12 @@ token_table init_token_table() {
          {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}};
 
     char const * commands[] = {"theorem", "axiom", "variable", "definition", "coercion",
-                               "variables", "[private]", "[inline]", "[fact]", "abbreviation",
+                               "variables", "[private]", "[inline]", "[fact]", "[instance]", "[class]", "abbreviation",
                                "evaluate", "check", "print", "end", "namespace", "section", "import",
                                "abbreviation", "inductive", "record", "structure", "module", "universe",
                                "precedence", "infixl", "infixr", "infix", "postfix", "prefix", "notation",
                                "exit", "set_option", "using", "calc_subst", "calc_refl", "calc_trans",
-                               "add_proof_qed", "reset_proof_qed", "#setline", nullptr};
+                               "add_proof_qed", "reset_proof_qed", "#setline", "class", "instance", nullptr};
 
     std::pair<char const *, char const *> aliases[] =
         {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},