feat(frontends/lean/builtin_cmds): add definition command family

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

src/emacs/lean-mode.el

@@ -31,7 +31,7 @@
     ("\\(->\\|↔\\|/\\\\\\|==\\|\\\\/\\|[*+/<=>¬∧∨≠≤≥-]\\)" . 'font-lock-constant-face)
     ("\\(λ\\|→\\|∃\\|∀\\|:\\|:=\\)" . font-lock-constant-face)
     ("\\_<\\(\\b.*_tac\\|Cond\\|OrElse\\|T\\(?:hen\\|ry\\)\\|When\\|apply\\|b\\(?:ack\\|eta\\)\\|done\\|exact\\)\\_>" . 'font-lock-constant-face)
-    ("\\_<\\(universe\\|theorem\\|axiom\\|definition\\|variable\\|builtin\\)\\_>[ \t]*\\([^ \t\n]*\\)" (2 'font-lock-function-name-face))
+    ("\\_<\\(universe\\|theorem\\|axiom\\|definition\\|variable\\|parameter\\)\\_>}?[ \t]*\\([^ \t\n]*\\)" (2 'font-lock-function-name-face))
     ("variables[ \t]\\([^:]*\\)" (1 'font-lock-function-name-face))
     ("\\(set_opaque\\|set_option\\)[ \t]*\\([^ \t\n]*\\)" (2 'font-lock-constant-face))
     ("\\_<_\\_>" . 'font-lock-preprocessor-face)

src/frontends/lean/builtin_cmds.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "library/io_state_stream.h"
 #include "library/scoped_ext.h"
 #include "library/aliases.h"
+#include "library/private.h"
 #include "library/locals.h"
 #include "frontends/lean/parser.h"
 
@@ -18,6 +19,9 @@ static name g_raw("raw");
 static name g_llevel_curly(".{");
 static name g_rcurly("}");
 static name g_colon(":");
+static name g_assign(":=");
+static name g_private("[private]");
+static name g_inline("[inline]");
 
 static void check_atomic(name const & n) {
     if (!n.is_atomic())
@@ -138,6 +142,121 @@ environment cast_variable_cmd(parser & p) {
     return variable_cmd_core(p, false, mk_cast_binder_info());
 }
 
+// Collect local (section) constants occurring in type and value, sort them, and store in section_ps
+static void collect_section_locals(expr const & type, expr const & value, parser const & p, buffer<parameter> & section_ps) {
+    name_set ls = collect_locals(type, collect_locals(value));
+    ls.for_each([&](name const & n) {
+            section_ps.push_back(*p.get_local(n));
+        });
+    std::sort(section_ps.begin(), section_ps.end(), [&](parameter const & p1, parameter const & p2) {
+            return *p.get_local_index(mlocal_name(p1.m_local)) < *p.get_local_index(mlocal_name(p2.m_local));
+        });
+}
+
+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;
+        }
+    }
+}
+
+// Wrap \c e with the "explicit macro", the idea is to inform the elaborator
+// preprocessor, that we do not need create metavariables for implicit arguments
+static expr mark_explicit(expr const & e) {
+    // TODO(Leo)
+    return e;
+}
+
+environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque) {
+    bool is_private = false;
+    parse_modifiers(p, is_private, is_opaque);
+    if (is_theorem && !is_opaque)
+        throw exception("invalid theorem declaration, theorems cannot be transparent");
+    name n = p.check_id_next("invalid declaration, identifier expected");
+    check_atomic(n);
+    environment env = p.env();
+    name real_n; // real name for this declaration
+    if (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;
+    } else {
+        name const & ns = get_namespace(env);
+        real_n     = ns + n;
+    }
+    buffer<name> ls_buffer;
+    expr type, value;
+    level_param_names ls;
+    {
+        parser::local_scope scope(p);
+        parse_univ_params(p, ls_buffer);
+        p.set_type_use_placeholder(false);
+        buffer<parameter> ps;
+        if (!p.curr_is_token(g_colon))
+            p.parse_binders(ps);
+        p.check_token_next(g_colon, "invalid declaration, ':' expected");
+        type = p.parse_scoped_expr(ps);
+        p.check_token_next(g_assign, "invalid declaration, ':=' expected");
+        p.set_type_use_placeholder(true);
+        value = p.parse_scoped_expr(ps);
+        type = p.pi_abstract(ps, type);
+        value = p.lambda_abstract(ps, value);
+        update_parameters(ls_buffer, collect_univ_params(value, collect_univ_params(type)), p);
+        ls = to_list(ls_buffer.begin(), ls_buffer.end());
+    }
+    if (in_section(env)) {
+        buffer<parameter> section_ps;
+        collect_section_locals(type, value, p, section_ps);
+        type = p.pi_abstract(section_ps, type);
+        value = p.lambda_abstract(section_ps, value);
+        buffer<level> section_ls_buffer;
+        for (name const & l : ls) {
+            if (p.get_local_level_index(l))
+                section_ls_buffer.push_back(mk_param_univ(l));
+            else
+                break;
+        }
+        levels section_ls = to_list(section_ls_buffer.begin(), section_ls_buffer.end());
+        buffer<expr> section_args;
+        for (auto const & p : section_ps)
+            section_args.push_back(p.m_local);
+        expr ref = mk_app(mark_explicit(mk_constant(real_n, section_ls)), section_args);
+        p.add_local_expr(n, ref);
+    } else {
+        if (real_n != n)
+            env = add_alias(env, n, mk_constant(real_n));
+    }
+    if (is_theorem) {
+        // TODO(Leo): delay theorems
+        auto type_value = p.elaborate(type, value, ls);
+        type  = type_value.first;
+        value = type_value.second;
+        env = env.add(check(env, mk_theorem(real_n, ls, type, value)));
+    } else {
+        auto type_value = p.elaborate(type, value, ls);
+        type  = type_value.first;
+        value = type_value.second;
+        env = env.add(check(env, mk_definition(env, real_n, ls, type, value, is_opaque)));
+    }
+    return env;
+}
+environment definition_cmd(parser & p) {
+    return definition_cmd_core(p, false, true);
+}
+environment abbreviation_cmd(parser & p) {
+    return definition_cmd_core(p, false, false);
+}
+environment theorem_cmd(parser & p) {
+    return definition_cmd_core(p, true, true);
+}
+
 environment print_cmd(parser & p) {
     if (p.curr() == scanner::token_kind::String) {
         p.regular_stream() << p.get_str_val() << "\n";
@@ -190,6 +309,9 @@ cmd_table init_cmd_table() {
     add_cmd(r, cmd_info("[variable]",   "declare a new cast parameter", cast_variable_cmd));
     add_cmd(r, cmd_info("axiom",        "declare a new axiom", axiom_cmd));
     add_cmd(r, cmd_info("{axiom}",      "declare a new implicit axiom", implicit_axiom_cmd));
+    add_cmd(r, cmd_info("definition",   "add new definition", definition_cmd));
+    add_cmd(r, cmd_info("abbreviation", "add new abbreviation (aka transparent definition)", abbreviation_cmd));
+    add_cmd(r, cmd_info("theorem",      "add new theorem", theorem_cmd));
     add_cmd(r, cmd_info("check",        "type check given expression, and display its type", check_cmd));
     return r;
 }

src/frontends/lean/builtin_exprs.cpp

@@ -40,7 +40,7 @@ parse_table init_nud_table() {
 
 parse_table init_led_table() {
     parse_table r(false);
-    r.add({transition("->", mk_expr_action(get_arrow_prec() + 1))}, mk_arrow(Var(0), Var(2)));
+    r.add({transition("->", mk_expr_action(get_arrow_prec()-1))}, mk_arrow(Var(0), Var(2)));
     return r;
 }
 }

src/frontends/lean/parser.cpp

@@ -246,6 +246,14 @@ optional<unsigned> parser::get_local_index(name const & n) const {
         return optional<unsigned>();
 }
 
+optional<parameter> parser::get_local(name const & n) const {
+    auto it = m_local_decls.find(n);
+    if (it != m_local_decls.end())
+        return optional<parameter>(it->second.first);
+    else
+        return optional<parameter>();
+}
+
 /** \brief Parse a sequence of identifiers <tt>ID*</tt>. Store the result in \c result. */
 void parser::parse_names(buffer<std::pair<pos_info, name>> & result) {
     while (curr_is_identifier()) {
@@ -401,6 +409,10 @@ expr parser::elaborate(expr const & e, level_param_names const &) {
     return e;
 }
 
+std::pair<expr, expr> parser::elaborate(expr const & t, expr const & v, level_param_names const &) {
+    return mk_pair(t, v);
+}
+
 /** \brief Parse <tt>ID ':' expr</tt>, where the expression represents the type of the identifier. */
 parameter parser::parse_binder_core(binder_info const & bi) {
     auto p  = pos();
@@ -621,9 +633,6 @@ expr parser::parse_id() {
     // globals
     if (m_env.find(id))
         r = save_pos(mk_constant(id, ls), p);
-    // private globals
-    else if (auto prv_id = user_to_hidden_name(m_env, id))
-        r = save_pos(mk_constant(*prv_id, ls), p);
     // aliases
     auto as = get_alias_exprs(m_env, id);
     if (!is_nil(as)) {

src/frontends/lean/parser.h

@@ -195,6 +195,8 @@ public:
     optional<unsigned> get_local_level_index(name const & n) const;
     /** \brief Position of the local declaration named \c n in the sequence of local decls. */
     optional<unsigned> get_local_index(name const & n) const;
+    /** \brief Return the local parameter named \c n */
+    optional<parameter> get_local(name const & n) const;
     /**
        \brief Specify how the method mk_Type behaves. When <tt>set_type_use_placeholder(true)</tt>, then
        it returns <tt>'Type.{_}'</tt>, where '_' is placeholder that instructs the Lean elaborator to
@@ -210,6 +212,7 @@ public:
     expr mk_Type();
 
     expr elaborate(expr const & e, level_param_names const &);
+    std::pair<expr, expr> elaborate(expr const & t, expr const & v, level_param_names const &);
 
     /** parse all commands in the input stream */
     bool operator()() { return parse_commands(); }

src/frontends/lean/token_table.cpp

@@ -4,11 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <limits>
 #include <utility>
 #include "frontends/lean/token_table.h"
 
 namespace lean {
 static unsigned g_arrow_prec = 25;
+static unsigned g_max_prec   = std::numeric_limits<unsigned>::max();
+static unsigned g_plus_prec  = 65;
+static unsigned g_cup_prec   = 75;
 unsigned get_arrow_prec() { return g_arrow_prec; }
 token_table add_command_token(token_table const & s, char const * token) {
     return insert(s, token, token_info(token));
@@ -45,12 +49,16 @@ static char const * g_cup            = "\u2294";
 
 token_table init_token_table() {
     token_table t;
-    char const * builtin[] = {"fun", "Pi", "let", "in", "have", "show", "by", "from", "(", ")", "{", "}", "[", "]",
+    std::pair<char const *, unsigned> builtin[] =
-                              ".{", "Type", "...", ",", ".", ":", "calc", ":=", "--", "(*", "(--",
+        {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"have", 0}, {"show", 0}, {"by", 0},
-                              "proof", "qed", "private", "raw", "Bool", "+", g_cup, nullptr};
+         {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0},
+         {"[", g_max_prec}, {"]", 0}, {".{", 0}, {"Type", g_max_prec},
+         {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"calc", 0}, {":=", 0}, {"--", 0},
+         {"(*", 0}, {"(--", 0}, {"proof", 0}, {"qed", 0}, {"raw", 0}, {"Bool", g_max_prec},
+         {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}};
 
     char const * commands[] = {"theorem", "axiom", "variable", "definition", "{axiom}", "{variable}", "[variable]",
-                               "variables", "{variables}", "[variables]",
+                               "variables", "{variables}", "[variables]", "[private]", "[inline]", "abbreviation",
                                "evaluate", "check", "print", "end", "namespace", "section", "import",
                                "abbreviation", "inductive", "record", "structure", "module", "universe",
                                nullptr};
@@ -68,29 +76,28 @@ token_table init_token_table() {
          {nullptr, nullptr}};
 
     auto it = builtin;
-    while (*it) {
+    while (it->first) {
-        t = add_token(t, *it);
+        t = add_token(t, it->first, it->second);
         it++;
     }
-    t = add_token(t, "->", get_arrow_prec());
 
-    it = commands;
+    auto it2 = commands;
-    while (*it) {
+    while (*it2) {
-        t = add_command_token(t, *it);
+        t = add_command_token(t, *it2);
-        ++it;
+        ++it2;
     }
 
-    auto it2 = aliases;
+    auto it3 = aliases;
-    while (it2->first) {
+    while (it3->first) {
-        t = add_token(t, it2->first, it2->second);
+        t = add_token(t, it3->first, it3->second);
-        it2++;
+        it3++;
     }
     t = add_token(t, g_arrow_unicode, "->", get_arrow_prec());
 
-    it2 = cmd_aliases;
+    auto it4 = cmd_aliases;
-    while (it2->first) {
+    while (it4->first) {
-        t = add_command_token(t, it2->first, it2->second);
+        t = add_command_token(t, it4->first, it4->second);
-        ++it2;
+        ++it4;
     }
     return t;
 }

src/library/private.cpp

@@ -14,7 +14,6 @@ Author: Leonardo de Moura
 namespace lean {
 struct private_ext : public environment_extension {
     unsigned                           m_counter;
-    rb_map<name, name, name_quick_cmp> m_map;      // map: user-name   -> hidden-name
     rb_map<name, name, name_quick_cmp> m_inv_map;  // map: hidden-name -> user-name
     private_ext():m_counter(0) {}
 };
@@ -47,7 +46,6 @@ std::pair<environment, name> add_private_name(environment const & env, name cons
     if (extra_hash)
         h = hash(h, *extra_hash);
     name r = name(g_private, h) + n;
-    ext.m_map.insert(n, r);
     ext.m_inv_map.insert(r, n);
     ext.m_counter++;
     environment new_env = update(env, ext);
@@ -76,11 +74,6 @@ optional<name> hidden_to_user_name(environment const & env, name const & n) {
     return it ? optional<name>(*it) : optional<name>();
 }
 
-optional<name> user_to_hidden_name(environment const & env, name const & n) {
-    auto it = get_extension(env).m_map.find(n);
-    return it ? optional<name>(*it) : optional<name>();
-}
-
 static int add_private_name(lua_State * L) {
     int nargs = lua_gettop(L);
     optional<unsigned> h;
@@ -93,11 +86,9 @@ static int add_private_name(lua_State * L) {
 }
 
 static int hidden_to_user_name(lua_State * L) { return push_optional_name(L, hidden_to_user_name(to_environment(L, 1), to_name_ext(L, 2))); }
-static int user_to_hidden_name(lua_State * L) { return push_optional_name(L, user_to_hidden_name(to_environment(L, 1), to_name_ext(L, 2))); }
 
 void open_private(lua_State * L) {
     SET_GLOBAL_FUN(add_private_name,    "add_private_name");
     SET_GLOBAL_FUN(hidden_to_user_name, "hidden_to_user_name");
-    SET_GLOBAL_FUN(user_to_hidden_name, "user_to_hidden_name");
 }
 }

src/library/private.h

@@ -31,18 +31,5 @@ std::pair<environment, name> add_private_name(environment const & env, name cons
 */
 optional<name> hidden_to_user_name(environment const & env, name const & n);
 
-/**
-    \brief Return the hidden name associated with the user name \c n.
-
-    \remark The "user name" is the argument provided to \c add_private_name, and "hidden name" is the name returned
-    by \c add_private_name.
-
-    \remark The mapping user -> hidden name is *not* stored in .olean files.
-    In this way, users don't have "access" to the names.
-
-    \see add_private_name
-*/
-optional<name> user_to_hidden_name(environment const & env, name const & n);
-
 void open_private(lua_State * L);
 }

tests/lean/t5.lean

@@ -0,0 +1,14 @@
+variable N : Type.{1}
+variable f : N → N
+variable a : N
+definition g (a : N) : N := f a
+check g
+namespace foo
+  definition h : N := f a
+  check h
+  definition [private] q : N := f a
+  check q
+end
+check foo.h
+check q -- Error q is now hidden
+

tests/lean/t5.lean.expected.out

@@ -0,0 +1,5 @@
+g : N -> N
+foo.h : N
+private.3156207665.q : N
+foo.h : N
+t5.lean:13:6: error: unknown identifier 'q'

tests/lean/t6.lean

@@ -0,0 +1,11 @@
+section
+  {parameter} A : Type  -- Mark A as implicit parameter
+  parameter   R : A → A → Bool
+  definition  id (a : A) : A := a
+  definition  refl : Bool := forall (a : A), R a a
+  definition  symm : Bool := forall (a b : A), R a b -> R b a
+end
+check id.{2}
+check refl.{1}
+check symm.{1}
+

tests/lean/t6.lean.expected.out

@@ -0,0 +1,3 @@
+id.{2} : Pi {A : Type.{2}} (a : A), A
+refl.{1} : Pi {A : Type} (R : A -> A -> Bool), Bool
+symm.{1} : Pi {A : Type} (R : A -> A -> Bool), Bool

tests/lean/t7.lean

@@ -0,0 +1,19 @@
+variable and : Bool → Bool → Bool
+section
+  {parameter} A : Type  -- Mark A as implicit parameter
+  parameter   R : A → A → Bool
+  parameter   B : Type
+  definition  id (a : A) : A := a
+  definition [private] refl : Bool := ∀ (a : A), R a a
+  definition  symm : Bool := ∀ (a b : A), R a b → R b a
+  definition  trans : Bool := ∀ (a b c : A), R a b → R b c → R a c
+  definition  equivalence : Bool := and (and refl symm) trans
+end
+check id.{2}
+check trans.{1}
+check symm.{1}
+check equivalence.{1}
+(*
+local env = get_env()
+print(env:find("equivalence"):value())
+*)

tests/lean/t7.lean.expected.out

@@ -0,0 +1,5 @@
+id.{2} : Pi {A : Type.{2}} (a : A), A
+trans.{1} : Pi {A : Type} (R : A -> A -> Bool), Bool
+symm.{1} : Pi {A : Type} (R : A -> A -> Bool), Bool
+equivalence.{1} : Pi {A : Type} (R : A -> A -> Bool), Bool
+fun {A : Type.{l_1}} (R : A -> A -> Bool), (and (and (private.2020036202.refl.{l_1} A R) (symm.{l_1} A R)) (trans.{l_1} A R))

tests/lua/prv.lua

@@ -12,9 +12,6 @@ assert(hidden_to_user_name(env, n1))
 assert(hidden_to_user_name(env, n1) == name("foo"))
 assert(hidden_to_user_name(env, n2) == name("foo"))
 assert(hidden_to_user_name(env, n3) == name("foo", "bla"))
-print(user_to_hidden_name(env, "foo"))
-assert(user_to_hidden_name(env, "foo") == n2)
-assert(user_to_hidden_name(env, {"foo", "bla"}) == n3)
 
 
 env:export("prv_mod.olean")
@@ -22,10 +19,7 @@ local env2 = import_modules("prv_mod")
 assert(hidden_to_user_name(env2, n1) == name("foo"))
 assert(hidden_to_user_name(env2, n2) == name("foo"))
 assert(hidden_to_user_name(env2, n3) == name("foo", "bla"))
-assert(not user_to_hidden_name(env2, "foo"))
-assert(not user_to_hidden_name(env2, {"foo", "bla"}))
 env2, n4 = add_private_name(env2, "foo")
 print(n4)
 assert(n1 ~= n4)
 assert(not hidden_to_user_name(env, n4))
-assert(user_to_hidden_name(env2, "foo") == n4)