From c46ec6a548409ae69566c672b40d617009be3ca3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 1 Oct 2014 14:02:49 -0700 Subject: [PATCH] fix(frontends/lean): missing type information for INFO, fixes #218 --- src/frontends/lean/parser.cpp | 9 ++++---- src/frontends/lean/parser_bindings.cpp | 5 +++-- src/frontends/lean/util.cpp | 6 +++-- src/kernel/abstract.cpp | 12 +++++----- src/kernel/abstract.h | 16 +++++++------- tests/lean/interactive/missing.input | 3 +++ .../interactive/missing.input.expected.out | 22 +++++++++++++++++++ tests/lean/interactive/missing.lean | 16 ++++++++++++++ 8 files changed, 67 insertions(+), 22 deletions(-) create mode 100644 tests/lean/interactive/missing.input create mode 100644 tests/lean/interactive/missing.input.expected.out create mode 100644 tests/lean/interactive/missing.lean diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index ea7ab9e76d..13511a8e84 100644 --- a/src/frontends/lean/parser.cpp +++ b/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()); diff --git a/src/frontends/lean/parser_bindings.cpp b/src/frontends/lean/parser_bindings.cpp index 0a6b215834..d0e6bdbc39 100644 --- a/src/frontends/lean/parser_bindings.cpp +++ b/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; } diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index 04b018bf33..9f584cf61c 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -83,11 +83,13 @@ list locals_to_context(expr const & e, parser const & p) { } expr Fun(buffer 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 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 diff --git a/src/kernel/abstract.cpp b/src/kernel/abstract.cpp index e059ee70a6..943cb7a754 100644 --- a/src/kernel/abstract.cpp +++ b/src/kernel/abstract.cpp @@ -58,10 +58,10 @@ class mk_binding_cache { std::vector> 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 -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(num, locals, b); } -expr Fun(unsigned num, expr const * locals, expr const & b) { return mk_binding(num, locals, b); } +expr Pi(unsigned num, expr const * locals, expr const & b, bool use_cache) { return mk_binding(num, locals, b, use_cache); } +expr Fun(unsigned num, expr const * locals, expr const & b, bool use_cache) { return mk_binding(num, locals, b, use_cache); } } diff --git a/src/kernel/abstract.h b/src/kernel/abstract.h index 050c299233..988c901036 100644 --- a/src/kernel/abstract.h +++ b/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 const & locals, expr const & b) { return Fun(locals.size(), locals.begin(), b); } -template 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 const & locals, expr const & b, bool use_cache = true) { return Fun(locals.size(), locals.begin(), b, use_cache); } +template 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 const & locals, expr const & b) { return Pi(locals.size(), locals.begin(), b); } -template 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 const & locals, expr const & b, bool use_cache = true) { return Pi(locals.size(), locals.begin(), b, use_cache); } +template expr Pi(T const & locals, expr const & b, bool use_cache = true) { return Pi(locals.size(), locals.data(), b, use_cache); } } diff --git a/tests/lean/interactive/missing.input b/tests/lean/interactive/missing.input new file mode 100644 index 0000000000..93a202e2a6 --- /dev/null +++ b/tests/lean/interactive/missing.input @@ -0,0 +1,3 @@ +VISIT missing.lean +WAIT +INFO 10 \ No newline at end of file diff --git a/tests/lean/interactive/missing.input.expected.out b/tests/lean/interactive/missing.input.expected.out new file mode 100644 index 0000000000..8f5d7de11e --- /dev/null +++ b/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 diff --git a/tests/lean/interactive/missing.lean b/tests/lean/interactive/missing.lean new file mode 100644 index 0000000000..1136a21b1b --- /dev/null +++ b/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