feat(frontends/lean/definition_cmds): postprocessing for parameters

src/frontends/lean/decl_util.cpp

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "library/locals.h"
 #include "library/placeholder.h"
 #include "library/tactic/elaborate.h"
+#include "frontends/lean/util.h"
 #include "frontends/lean/decl_util.h"
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/parser.h"
@@ -233,4 +234,23 @@ void elaborate_params(elaborator & elab, buffer<expr> const & params, buffer<exp
         new_params.push_back(new_param);
     }
 }
+
+environment add_local_ref(parser & p, environment const & env, name const & c_name, name const & c_real_name, buffer<name> const & lp_names, buffer<expr> const & var_params) {
+    if (!p.has_params()) return env;
+    buffer<expr> params;
+    buffer<name> lps;
+    for (name const & u : lp_names) {
+        if (p.is_local_level_variable(u))
+            break;
+        lps.push_back(u);
+    }
+    for (expr const & e : var_params) {
+        if (p.is_local_variable(e))
+            break;
+        params.push_back(e);
+    }
+    if (lps.empty() && params.empty()) return env;
+    expr ref = mk_local_ref(c_real_name, param_names_to_levels(to_list(lps)), params);
+    return p.add_local_ref(env, c_name, ref);
+}
 }

src/frontends/lean/decl_util.h

@@ -59,4 +59,10 @@ void collect_implicit_locals(parser & p, buffer<name> & lp_names, buffer<expr> &
 
     \post params.size() == new_params.size() */
 void elaborate_params(elaborator & elab, buffer<expr> const & params, buffer<expr> & new_params);
+
+/** \brief Create an alias c_name --> (c_real_name.{level_params} params)
+    level_params and params are subsets of lp_names and var_params that were
+    declared using the parameter command. */
+environment add_local_ref(parser & p, environment const & env, name const & c_name, name const & c_real_name,
+                          buffer<name> const & lp_names, buffer<expr> const & var_params);
 }

src/frontends/lean/definition_cmds.cpp

@@ -280,9 +280,11 @@ static environment compile_decl(parser & p, environment const & env, def_cmd_kin
     }
 }
 
-static environment declare_definition(parser & p, def_cmd_kind kind, buffer<name> const & lp_names, name const & c_name,
-                                      expr const & type, expr const & val, bool is_private, bool is_protected, bool is_noncomputable,
-                                      decl_attributes attrs, pos_info const & pos) {
+static pair<environment, name>
+declare_definition(parser & p, def_cmd_kind kind, buffer<name> const & lp_names,
+                   name const & c_name, expr const & type, expr const & val,
+                   bool is_private, bool is_protected, bool is_noncomputable,
+                   decl_attributes attrs, pos_info const & pos) {
     auto env_n = mk_real_name(p.env(), c_name, is_private, pos);
     environment new_env = env_n.first;
     name c_real_name    = env_n.second;
@@ -309,7 +311,8 @@ static environment declare_definition(parser & p, def_cmd_kind kind, buffer<name
     }
 
     new_env = attrs.apply(new_env, p.ios(), c_real_name);
-    return compile_decl(p, new_env, kind, is_noncomputable, c_name, c_real_name, pos);
+    new_env = compile_decl(p, new_env, kind, is_noncomputable, c_name, c_real_name, pos);
+    return mk_pair(new_env, c_real_name);
 }
 
 environment xdefinition_cmd_core(parser & p, def_cmd_kind kind, bool is_private, bool is_protected, bool is_noncomputable,
@@ -329,7 +332,11 @@ environment xdefinition_cmd_core(parser & p, def_cmd_kind kind, bool is_private,
     // TODO(Leo): postprocess nested matches and equations
     finalize_definition(elab, new_params, type, val, lp_names);
     if (kind == Example) return p.env();
-    return declare_definition(p, kind, lp_names, mlocal_name(fn), type, val,
-                              is_private, is_protected, is_noncomputable, attrs, header_pos);
+    name c_name = mlocal_name(fn);
+    auto env_n  = declare_definition(p, kind, lp_names, c_name, type, val,
+                                     is_private, is_protected, is_noncomputable, attrs, header_pos);
+    environment new_env = env_n.first;
+    name c_real_name    = env_n.second;
+    return add_local_ref(p, new_env, c_name, c_real_name, lp_names, params);
 }
 }

tests/lean/def3.lean

@@ -0,0 +1,11 @@
+set_option new_elaborator true
+
+section
+  variable (A : Type)
+
+  definition f : A → A :=
+  λ x, x
+
+  check f
+
+end

tests/lean/def3.lean.expected.out

@@ -0,0 +1 @@
+f : Π A, A → A

tests/lean/def4.lean

@@ -0,0 +1,23 @@
+set_option new_elaborator true
+
+section
+  parameter (A : Type)
+
+  definition f : A → A :=
+  λ x, x
+
+  check f
+  check f (0:nat) -- error
+
+  parameter {A}
+
+  definition g : A → A :=
+  λ x, x
+
+  check g
+  check g (0:nat) -- error
+end
+
+check f
+check f _ (0:nat)
+check g 0

tests/lean/def4.lean.expected.out

@@ -0,0 +1,21 @@
+f : A → A
+def4.lean:10:8: error: type mismatch at application
+  f 0
+term
+  0
+has type
+  ℕ
+but is expected to have type
+  A
+g : A → A
+def4.lean:18:8: error: type mismatch at application
+  g 0
+term
+  0
+has type
+  ℕ
+but is expected to have type
+  A
+f : Π A, A → A
+f ℕ 0 : ℕ
+g 0 : ℕ