fix(frontends/lean): missing type information for INFO, fixes #218

src/frontends/lean/parser.cpp

@@ -869,11 +869,12 @@ expr parser::parse_notation(parse_table t, expr * left) {
             break;
         case notation::action_kind::ScopedExpr: {
             expr r   = parse_scoped_expr(ps, lenv, a.rbp());
+            bool no_cache = false;
             if (is_var(a.get_rec(), 0)) {
                 if (a.use_lambda_abstraction())
-                    r = Fun(ps, r);
+                    r = Fun(ps, r, no_cache);
                 else
-                    r = Pi(ps, r);
+                    r = Pi(ps, r, no_cache);
                 r = rec_save_pos(r, binder_pos);
             } else {
                 expr rec = copy_with_new_pos(a.get_rec(), p);
@@ -882,9 +883,9 @@ expr parser::parse_notation(parse_table t, expr * left) {
                     --i;
                     expr const & l = ps[i];
                     if (a.use_lambda_abstraction())
-                        r = Fun(l, r);
+                        r = Fun(l, r, no_cache);
                     else
-                        r = Pi(l, r);
+                        r = Pi(l, r, no_cache);
                     r = save_pos(r, binder_pos);
                     args.push_back(r);
                     r = instantiate_rev(rec, args.size(), args.data());

src/frontends/lean/parser_bindings.cpp

@@ -96,10 +96,11 @@ static int lambda_abstract(lua_State * L) {
     local_scope const & s = to_local_scope(L, 1);
     expr const & e = to_expr(L, 2);
     expr r;
+    bool using_cache = false;
     if (nargs == 2)
-        r = gparser.rec_save_pos(Fun(s->second.size(), s->second.data(), e), gparser.pos_of(e));
+        r = gparser.rec_save_pos(Fun(s->second.size(), s->second.data(), e, using_cache), gparser.pos_of(e));
     else
-        r = gparser.rec_save_pos(Fun(s->second.size(), s->second.data(), e), pos_info(lua_tointeger(L, 3), lua_tointeger(L, 4)));
+        r = gparser.rec_save_pos(Fun(s->second.size(), s->second.data(), e, using_cache), pos_info(lua_tointeger(L, 3), lua_tointeger(L, 4)));
     return push_expr(L, r);
 }
 static int next(lua_State * L) { gparser.next(); return 0; }

src/frontends/lean/util.cpp

@@ -83,11 +83,13 @@ list<expr> locals_to_context(expr const & e, parser const & p) {
 }
 
 expr Fun(buffer<expr> const & locals, expr const & e, parser & p) {
-    return p.rec_save_pos(Fun(locals, e), p.pos_of(e));
+    bool use_cache = false;
+    return p.rec_save_pos(Fun(locals, e, use_cache), p.pos_of(e));
 }
 
 expr Pi(buffer<expr> const & locals, expr const & e, parser & p) {
-    return p.rec_save_pos(Pi(locals, e), p.pos_of(e));
+    bool use_cache = false;
+    return p.rec_save_pos(Pi(locals, e, use_cache), p.pos_of(e));
 }
 
 template<bool is_lambda>

src/kernel/abstract.cpp

@@ -58,10 +58,10 @@ class mk_binding_cache {
     std::vector<optional<expr>> m_abstract_types;
 public:
     mk_binding_cache() {}
-    void abstract(unsigned num, expr const * locals) {
+    void abstract(unsigned num, expr const * locals, bool use_cache) {
         m_locals.resize(num, none_expr());
         m_abstract_types.resize(num, none_expr());
-        bool matching = true;
+        bool matching = use_cache;
         for (unsigned i = 0; i < num; i++) {
             if (!(matching && m_locals[i] && *m_locals[i] == locals[i])) {
                 m_locals[i]         = locals[i];
@@ -79,10 +79,10 @@ public:
 MK_THREAD_LOCAL_GET_DEF(mk_binding_cache, get_mk_binding_cache);
 
 template<bool is_lambda>
-expr mk_binding(unsigned num, expr const * locals, expr const & b) {
+expr mk_binding(unsigned num, expr const * locals, expr const & b, bool use_cache) {
     expr r       = abstract_locals(b, num, locals);
     auto & cache = get_mk_binding_cache();
-    cache.abstract(num, locals);
+    cache.abstract(num, locals, use_cache);
     unsigned i = num;
     while (i > 0) {
         --i;
@@ -96,6 +96,6 @@ expr mk_binding(unsigned num, expr const * locals, expr const & b) {
     return r;
 }
 
-expr Pi(unsigned num, expr const * locals, expr const & b) { return mk_binding<false>(num, locals, b); }
-expr Fun(unsigned num, expr const * locals, expr const & b) { return mk_binding<true>(num, locals, b); }
+expr Pi(unsigned num, expr const * locals, expr const & b, bool use_cache) { return mk_binding<false>(num, locals, b, use_cache); }
+expr Fun(unsigned num, expr const * locals, expr const & b, bool use_cache) { return mk_binding<true>(num, locals, b, use_cache); }
 }

src/kernel/abstract.h

@@ -33,10 +33,10 @@ inline expr Fun(name const & n, expr const & t, expr const & b, binder_info cons
     return mk_lambda(n, t, abstract(b, mk_constant(n)), bi);
 }
 /** \brief Create a lambda-expression by abstracting the given local constants over b */
-expr Fun(unsigned num, expr const * locals, expr const & b);
-inline expr Fun(expr const & local, expr const & b) { return Fun(1, &local, b); }
-inline expr Fun(std::initializer_list<expr> const & locals, expr const & b) { return Fun(locals.size(), locals.begin(), b); }
-template<typename T> expr Fun(T const & locals, expr const & b) { return Fun(locals.size(), locals.data(), b); }
+expr Fun(unsigned num, expr const * locals, expr const & b, bool use_cache = true);
+inline expr Fun(expr const & local, expr const & b, bool use_cache = true) { return Fun(1, &local, b, use_cache); }
+inline expr Fun(std::initializer_list<expr> const & locals, expr const & b, bool use_cache = true) { return Fun(locals.size(), locals.begin(), b, use_cache); }
+template<typename T> expr Fun(T const & locals, expr const & b, bool use_cache = true) { return Fun(locals.size(), locals.data(), b, use_cache); }
 
 /**
    \brief Create a Pi expression (pi (x : t) b), the term b is abstracted using abstract(b, constant(x)).
@@ -45,8 +45,8 @@ inline expr Pi(name const & n, expr const & t, expr const & b, binder_info const
     return mk_pi(n, t, abstract(b, mk_constant(n)), bi);
 }
 /** \brief Create a Pi-expression by abstracting the given local constants over b */
-expr Pi(unsigned num, expr const * locals, expr const & b);
-inline expr Pi(expr const & local, expr const & b) { return Pi(1, &local, b); }
-inline expr Pi(std::initializer_list<expr> const & locals, expr const & b) { return Pi(locals.size(), locals.begin(), b); }
-template<typename T> expr Pi(T const & locals, expr const & b) { return Pi(locals.size(), locals.data(), b); }
+expr Pi(unsigned num, expr const * locals, expr const & b, bool use_cache = true);
+inline expr Pi(expr const & local, expr const & b, bool use_cache = true) { return Pi(1, &local, b, use_cache); }
+inline expr Pi(std::initializer_list<expr> const & locals, expr const & b, bool use_cache = true) { return Pi(locals.size(), locals.begin(), b, use_cache); }
+template<typename T> expr Pi(T const & locals, expr const & b, bool use_cache = true) { return Pi(locals.size(), locals.data(), b, use_cache); }
 }

tests/lean/interactive/missing.input

@@ -0,0 +1,3 @@
+VISIT missing.lean
+WAIT
+INFO 10

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

@@ -0,0 +1,22 @@
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGININFO
+-- SYMBOL|10|0
+have
+-- ACK
+-- SYMBOL|10|15
+∀
+-- ACK
+-- TYPE|10|22
+Type → Type
+-- ACK
+-- IDENTIFIER|10|22
+tree
+-- ACK
+-- TYPE|10|27
+Type
+-- ACK
+-- IDENTIFIER|10|27
+A
+-- ACK
+-- ENDINFO

tests/lean/interactive/missing.lean

@@ -0,0 +1,16 @@
+import logic
+
+inductive tree (A : Type) :=
+leaf : A → tree A,
+node : tree A → tree A → tree A
+
+namespace tree
+
+definition below_rec {A : Type} (t : tree A) {P : tree A → Type} (iH : Π (t : tree A), P t) : P t :=
+have general : ∀ (t : tree A),
+  P t, from
+  -- take t, iH t,
+  sorry,
+general t
+
+end tree