feat(frontends/lean): add new definition command skeleton

src/frontends/lean/decl_cmds.cpp

@@ -586,9 +586,6 @@ void collect_locals(expr const & type, expr const & value, parser const & p, buf
     sort_locals(ls.get_collected(), p, ctx_ps);
 }
 
-// An Lean example is not really a definition, but we use the definition infrastructure to simulate it.
-enum def_cmd_kind { Theorem, Definition, MetaDefinition, Example, Abbreviation, LocalAbbreviation };
-
 class definition_cmd_fn {
     parser &          m_p;
     environment       m_env;
@@ -1206,7 +1203,10 @@ static environment definition_cmd(parser & p) {
     } else {
         throw parser_error("invalid definition/theorem, 'definition' or 'theorem' expected", p.pos());
     }
-    return definition_cmd_core(p, kind, is_private, is_protected, is_noncomputable);
+    if (p.use_new_elaborator())
+        return xdefinition_cmd_core(p, kind, is_private, is_protected, is_noncomputable);
+    else
+        return definition_cmd_core(p, kind, is_private, is_protected, is_noncomputable);
 }
 
 static environment include_cmd_core(parser & p, bool include) {

src/frontends/lean/decl_util.cpp

@@ -32,18 +32,23 @@ bool parse_univ_params(parser & p, buffer<name> & lp_names) {
     }
 }
 
-pair<expr, expr> parse_single_header(parser & p, buffer<name> & lp_names, buffer<expr> & params) {
+expr parse_single_header(parser & p, buffer<name> & lp_names, buffer<expr> & params) {
     auto c_pos  = p.pos();
     name c_name = p.check_id_next("invalid declaration, identifier expected");
-    expr c      = p.save_pos(mk_local(c_name, mk_expr_placeholder()), c_pos);
     parse_univ_params(p, lp_names);
     p.parse_optional_binders(params);
     for (expr const & param : params)
         p.add_local(param);
-    p.check_token_next(get_colon_tk(), "invalid declaration, ':' expected");
-    expr type = p.parse_expr();
+    expr type;
+    if (p.curr_is_token(get_colon_tk())) {
+        p.next();
+        type = p.parse_expr();
+    } else {
+        type = p.save_pos(mk_expr_placeholder(), c_pos);
+    }
+    expr c    = p.save_pos(mk_local(c_name, type), c_pos);
     p.add_local(c);
-    return mk_pair(c, type);
+    return c;
 }
 
 void parse_mutual_header(parser & p, buffer<name> & lp_names, buffer<expr> & cs, buffer<expr> & params) {
@@ -210,6 +215,11 @@ void collect_implicit_locals(parser & p, buffer<name> & lp_names, buffer<expr> &
     update_univ_parameters(p, lp_names, lp_found);
 }
 
+void collect_implicit_locals(parser & p, buffer<name> & lp_names, buffer<expr> & params, expr const & e) {
+    buffer<expr> all_exprs; all_exprs.push_back(e);
+    collect_implicit_locals(p, lp_names, params, all_exprs);
+}
+
 void elaborate_params(elaborator & elab, buffer<expr> const & params, buffer<expr> & new_params) {
     for (unsigned i = 0; i < params.size(); i++) {
         expr const & param = params[i];

src/frontends/lean/decl_util.h

@@ -18,13 +18,13 @@ bool parse_univ_params(parser & p, buffer<name> & lp_names);
 
          c.{u_1 ... u_k} (params) : type
 
-    The result is the pair (c, type). The explicit universe level parameters are stored
+    The result is the local constant (c : type). The explicit universe level parameters are stored
     at lp_names, and the optional parameters at params.
 
     Both lp_names and params are added to the parser scope.
 
     \remark Caller is responsible for using: parser::local_scope scope2(p, env); */
-pair<expr, expr> parse_single_header(parser & p, buffer<name> & lp_names, buffer<expr> & params);
+expr parse_single_header(parser & p, buffer<name> & lp_names, buffer<expr> & params);
 /** \brief Parse the header of a mutually recursive declaration. It has the form
 
         {u_1 ... u_k} id_1, ... id_n (params)
@@ -51,6 +51,7 @@ expr parse_inner_header(parser & p, name const & c_expected);
     We also add parameters included using the command 'include'.
     lp_names and params are input/output. */
 void collect_implicit_locals(parser & p, buffer<name> & lp_names, buffer<expr> & params, buffer<expr> const & all_exprs);
+void collect_implicit_locals(parser & p, buffer<name> & lp_names, buffer<expr> & params, expr const & e);
 
 /** \brief Elaborate the types of the parameters \c params, and update the elaborator local context using them.
     Store the elaborated parameters at new_params.

src/frontends/lean/definition_cmds.cpp

@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/util.h"
 #include "frontends/lean/decl_util.h"
 #include "frontends/lean/decl_attributes.h"
+#include "frontends/lean/definition_cmds.h"
 
 namespace lean {
 expr parse_equation_lhs(parser & p, expr const & fn, buffer<expr> & locals) {
@@ -87,15 +88,13 @@ expr parse_mutual_definition(parser & p, buffer<name> & lp_names, buffer<expr> &
         eq = replace_locals(eq, pre_fns, fns);
     }
     expr r = mk_equations(p, fns, eqns, R_Rwf, header_pos);
-    buffer<expr> all_exprs; all_exprs.push_back(r);
-    collect_implicit_locals(p, lp_names, params, all_exprs);
+    collect_implicit_locals(p, lp_names, params, r);
     return r;
 }
 
 environment mutual_definition_cmd_core(parser & p, bool is_private, bool is_protected, bool is_noncomputable) {
     decl_attributes attrs;
     attrs.parse(p);
-    parser::local_scope scope(p);
     buffer<name> lp_names;
     buffer<expr> fns, params;
     expr val = parse_mutual_definition(p, lp_names, fns, params);
@@ -110,4 +109,53 @@ environment mutual_definition_cmd_core(parser & p, bool is_private, bool is_prot
 
     return p.env();
 }
+
+expr_pair parse_definition(parser & p, buffer<name> & lp_names, buffer<expr> & params) {
+    parser::local_scope scope(p);
+    auto header_pos = p.pos();
+    expr fn = parse_single_header(p, lp_names, params);
+    expr val;
+    if (p.curr_is_token(get_assign_tk())) {
+        p.next();
+        val = p.parse_expr();
+    } else if (p.curr_is_token(get_bar_tk())) {
+        buffer<expr> eqns;
+        if (p.curr_is_token(get_none_tk())) {
+            auto none_pos = p.pos();
+            p.next();
+            eqns.push_back(p.save_pos(mk_no_equation(), none_pos));
+        } else {
+            while (p.curr_is_token(get_bar_tk())) {
+                eqns.push_back(parse_equation(p, fn));
+            }
+        }
+        optional<expr_pair> R_Rwf = parse_using_well_founded(p);
+        buffer<expr> fns;
+        fns.push_back(fn);
+        val = mk_equations(p, fns, eqns, R_Rwf, header_pos);
+    } else {
+        throw parser_error("invalid definition, '|' or ':=' expected", p.pos());
+    }
+    collect_implicit_locals(p, lp_names, params, val);
+    return mk_pair(fn, val);
+}
+
+environment xdefinition_cmd_core(parser & p, def_cmd_kind kind, bool is_private, bool is_protected, bool is_noncomputable) {
+    decl_attributes attrs;
+    attrs.parse(p);
+    buffer<name> lp_names;
+    buffer<expr> params;
+    expr fn, val;
+    std::tie(fn, val) = parse_definition(p, lp_names, params);
+    elaborator elab(p.env(), p.get_options(), metavar_context(), local_context());
+    buffer<expr> new_params;
+    elaborate_params(elab, params, new_params);
+    val = replace_locals(val, params, new_params);
+
+    // TODO(Leo)
+    for (auto p : params) { tout() << ">> " << p << " : " << mlocal_type(p) << "\n"; }
+    tout() << val << "\n";
+
+    return p.env();
+}
 }

src/frontends/lean/definition_cmds.h

@@ -15,7 +15,6 @@ inline environment noncomputable_mutual_definition_cmd(parser & p) { return mutu
 inline environment private_noncomputable_mutual_definition_cmd(parser & p) { return mutual_definition_cmd_core(p, true, false, true); }
 inline environment protected_noncomputable_mutual_definition_cmd(parser & p) { return mutual_definition_cmd_core(p, false, true, true); }
 
-expr parse_equation_lhs(parser & p, expr const & fn, buffer<expr> & locals);
-expr parse_equation(parser & p, expr const & fn);
-
+enum def_cmd_kind { Theorem, Definition, MetaDefinition, Example, Abbreviation, LocalAbbreviation };
+environment xdefinition_cmd_core(parser & p, def_cmd_kind k, bool is_private, bool is_protected, bool is_noncomputable);
 }