fix(frontends/lean/builtin_cmds): abstract section parameters in the 'check' command

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

src/frontends/lean/builtin_cmds.cpp

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "util/sstream.h"
 #include "util/sexpr/option_declarations.h"
 #include "kernel/type_checker.h"
+#include "kernel/abstract.h"
 #include "library/io_state_stream.h"
 #include "library/scoped_ext.h"
 #include "library/aliases.h"
@@ -72,6 +73,10 @@ environment end_scoped_cmd(parser & p) {
 
 environment check_cmd(parser & p) {
     expr e   = p.parse_expr();
+    buffer<parameter> section_ps;
+    name_set locals = collect_locals(e);
+    mk_section_params(collect_locals(e), p, section_ps);
+    e = p.lambda_abstract(section_ps, e);
     level_param_names ls = to_level_param_names(collect_univ_params(e));
     e = p.elaborate(e);
     expr type = type_checker(p.env()).check(e, ls);

tests/lean/interactive/t3.input.expected.out

@@ -1,3 +1,3 @@
-A : Type.{l_1}
+fun (A : Type.{l_1}), A : Type.{l_1} -> Type.{l_1}
-A : Type.{l_1}
+fun (A : Type.{l_1}), A : Type.{l_1} -> Type.{l_1}
 done

tests/lean/run/e10.lean

@@ -0,0 +1,42 @@
+
+precedence `+`:65
+
+namespace nat
+  variable nat : Type.{1}
+  variable add : nat → nat → nat
+  infixl + := add
+end
+
+namespace int
+  using nat (nat)
+  variable int : Type.{1}
+  variable add : int → int → int
+  infixl + := add
+  variable of_nat : nat → int
+  coercion of_nat
+end
+
+section
+  using nat
+  using int
+
+  variables n m : nat
+  variables i j : int
+
+  -- 'Most recent' are always tried first
+  print raw i + n
+  -- So, in the following one int.add is tried first, and we
+  -- get int.add (int.of_nat n) (int.of_nat m)
+  check n + m
+
+
+  print ">>> Forcing nat notation"
+  -- Force natural numbers
+  check #nat n + m
+
+  -- Moving 'nat' to the 'front'
+  print ">>> Moving nat notation to the 'front'"
+  using nat
+  print raw i + n
+  check n + m
+end

tests/lean/run/e11.lean

@@ -0,0 +1,41 @@
+precedence `+`:65
+
+namespace nat
+  variable nat : Type.{1}
+  variable add : nat → nat → nat
+  infixl + := add
+end
+
+namespace int
+  using nat (nat)
+  variable int : Type.{1}
+  variable add : int → int → int
+  infixl + := add
+  variable of_nat : nat → int
+  coercion of_nat
+end
+
+section
+  -- Using "only" the notation and declarations from the namespaces nat and int
+  using [notation] nat
+  using [notation] int
+  using [decls] nat
+  using [decls] int
+
+  variables n m : nat
+  variables i j : int
+  check n + m
+  check i + j
+
+  -- The following check does not work, since we are not using the coercions
+  -- check n + i
+
+  -- Here is a possible trick for this kind of configuration
+  definition add_ni (a : nat) (b : int) := (of_nat a) + b
+  definition add_in (a : int) (b : nat) := a + (of_nat b)
+  infixl + := add_ni
+  infixl + := add_in
+
+  check i + n
+  check n + i
+end

tests/lean/t4.lean.expected.out

@@ -5,9 +5,9 @@ F.{2} : Type.{2} -> Type.{2}
 F.{u} : Type.{u} -> Type.{u}
 f : N -> N -> N
 len.{1} : Pi (A : Type) (n : N) (v : vec.{1} A n), N
-B -> B : Bool
+fun (B : Bool), (B -> B) : Bool -> Bool
-A -> A : Type.{l_1}
+fun (A : Type.{l_1}), (A -> A) : Type.{l_1} -> Type.{l_1}
-C : Type.{l_2}
+fun {C : Type.{l_2}}, C : Type.{l_2} -> Type.{l_2}
 t4.lean:25:6: error: unknown identifier 'A'
 R.{1 0} : Type -> Bool
 fun (x : N) (y : N), x : N -> N -> N