diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 6a900aa75..c65d631fa 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -20,6 +20,7 @@ static name g_colon(":"); static name g_assign(":="); static name g_comma(","); static name g_fact("[fact]"); +static name g_inline("[inline]"); static name g_from("from"); static name g_using("using"); static name g_then("then"); @@ -50,6 +51,25 @@ static expr parse_let_body(parser & p, pos_info const & pos) { } } +static expr mk_let(parser & p, name const & id, expr const & t, expr const & v, expr const & b, pos_info const & pos, binder_info const & bi) { + expr l = p.save_pos(mk_lambda(id, t, b, bi), pos); + return p.save_pos(mk_let_macro(p.save_pos(mk_app(l, v), pos)), pos); +} + +static void parse_let_modifiers(parser & p, bool & is_fact, bool & is_opaque) { + while (true) { + if (p.curr_is_token(g_fact)) { + is_fact = true; + p.next(); + } else if (p.curr_is_token(g_inline)) { + is_opaque = false; + p.next(); + } else { + break; + } + } +} + static expr parse_let(parser & p, pos_info const & pos) { parser::local_scope scope1(p); if (p.parse_local_notation_decl()) { @@ -57,12 +77,18 @@ static expr parse_let(parser & p, pos_info const & pos) { } else { auto pos = p.pos(); name id = p.check_id_next("invalid let declaration, identifier expected"); + bool is_opaque = true; + bool is_fact = false; expr type, value; + parse_let_modifiers(p, is_fact, is_opaque); if (p.curr_is_token(g_assign)) { p.next(); - type = p.save_pos(mk_expr_placeholder(), pos); + if (is_opaque) + type = p.save_pos(mk_expr_placeholder(), pos); value = p.parse_expr(); } else if (p.curr_is_token(g_colon)) { + if (!is_opaque) + throw parser_error("invalid let 'inline' declaration, explicit type must not be provided", p.pos()); p.next(); type = p.parse_expr(); p.check_token_next(g_assign, "invalid declaration, ':=' expected"); @@ -72,20 +98,28 @@ static expr parse_let(parser & p, pos_info const & pos) { buffer ps; auto lenv = p.parse_binders(ps); if (p.curr_is_token(g_colon)) { + if (!is_opaque) + throw parser_error("invalid let 'inline' declaration, explicit type must not be provided", p.pos()); p.next(); type = p.parse_scoped_expr(ps, lenv); - } else { + } else if (is_opaque) { type = p.save_pos(mk_expr_placeholder(), pos); } p.check_token_next(g_assign, "invalid let declaration, ':=' expected"); value = p.parse_scoped_expr(ps, lenv); - type = p.pi_abstract(ps, type); + if (is_opaque) + type = p.pi_abstract(ps, type); value = p.lambda_abstract(ps, value); } - expr l = p.save_pos(mk_local(id, type), pos); - p.add_local(l); - expr body = abstract(parse_let_body(p, pos), l); - return p.save_pos(mk_let(id, type, value, body), pos); + if (is_opaque) { + expr l = p.save_pos(mk_local(id, type), pos); + p.add_local(l); + expr body = abstract(parse_let_body(p, pos), l); + return mk_let(p, id, type, value, body, pos, mk_contextual_info(is_fact)); + } else { + p.add_local_expr(id, value, mk_contextual_info(false)); + return parse_let_body(p, pos); + } } } @@ -217,7 +251,7 @@ static expr parse_show(parser & p, unsigned, expr const *, pos_info const & pos) expr prop = p.parse_expr(); p.check_token_next(g_comma, "invalid 'show' declaration, ',' expected"); expr proof = parse_proof(p, prop); - return p.save_pos(mk_let(H_show, prop, proof, Var(0)), pos); + return mk_let(p, H_show, prop, proof, Var(0), pos, mk_contextual_info(false)); } static expr parse_calc_expr(parser & p, unsigned, expr const *, pos_info const &) { diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 0edf4afa1..ffe392fe2 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -252,12 +252,6 @@ expr parser::copy_with_new_pos(expr const & e, pos_info p) { copy_with_new_pos(binding_domain(e), p), copy_with_new_pos(binding_body(e), p)), p); - case expr_kind::Let: - return save_pos(update_let(e, - copy_with_new_pos(let_type(e), p), - copy_with_new_pos(let_value(e), p), - copy_with_new_pos(let_body(e), p)), - p); case expr_kind::Macro: { buffer args; for (unsigned i = 0; i < macro_num_args(e); i++) diff --git a/src/kernel/abstract.h b/src/kernel/abstract.h index 828dd2bd7..feb9a3b87 100644 --- a/src/kernel/abstract.h +++ b/src/kernel/abstract.h @@ -61,9 +61,4 @@ template expr Pi(T const & locals, expr const & b) { return Pi(local inline expr Pi(expr const & local, expr const & b, binder_info const & bi = binder_info()) { return Pi(local_pp_name(local), mlocal_type(local), abstract(b, local), bi); } -/** -- \brief Create a Let expression (Let x := v in b), the term b is abstracted using abstract(b, x). --*/ -inline expr Let(name const & x, expr const & t, expr const & v, expr const & b) { return mk_let(x, t, v, abstract(b, mk_constant(x))); } -inline expr Let(expr const & x, expr const & t, expr const & v, expr const & b) { return mk_let(named_expr_name(x), t, v, abstract(b, x)); } } diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp index b25351e4f..c92541983 100644 --- a/src/kernel/converter.cpp +++ b/src/kernel/converter.cpp @@ -83,7 +83,7 @@ struct default_converter : public converter { case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: case expr_kind::Pi: case expr_kind::Constant: return e; - case expr_kind::Lambda: case expr_kind::Macro: case expr_kind::Let: case expr_kind::App: + case expr_kind::Lambda: case expr_kind::Macro: case expr_kind::App: break; } @@ -109,9 +109,6 @@ struct default_converter : public converter { else r = e; break; - case expr_kind::Let: - r = whnf_core(instantiate(let_body(e), let_value(e)), c); - break; case expr_kind::App: { buffer args; expr f0 = get_app_rev_args(e, args); @@ -308,7 +305,7 @@ struct default_converter : public converter { case expr_kind::Meta: lean_unreachable(); // LCOV_EXCL_LINE case expr_kind::Var: case expr_kind::Local: case expr_kind::App: - case expr_kind::Constant: case expr_kind::Macro: case expr_kind::Let: + case expr_kind::Constant: case expr_kind::Macro: // We do not handle these cases in this method. break; } diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 15b2ef185..cc115066e 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -178,27 +178,6 @@ expr_sort::expr_sort(level const & l): } expr_sort::~expr_sort() {} -// Expr Let -expr_let::expr_let(name const & n, expr const & t, expr const & v, expr const & b): - expr_composite(expr_kind::Let, ::lean::hash(v.hash(), b.hash()), - t.has_metavar() || v.has_metavar() || b.has_metavar(), - t.has_local() || v.has_local() || b.has_local(), - t.has_param_univ() || v.has_param_univ() || b.has_param_univ(), - std::max({get_depth(t), get_depth(v), get_depth(b)}) + 1, - std::max({get_free_var_range(t), get_free_var_range(v), dec(get_free_var_range(b))})), - m_name(n), - m_type(t), - m_value(v), - m_body(b) { -} -void expr_let::dealloc(buffer & todelete) { - dec_ref(m_body, todelete); - dec_ref(m_value, todelete); - dec_ref(m_type, todelete); - delete(this); -} -expr_let::~expr_let() {} - // Macro definition bool macro_definition_cell::lt(macro_definition_cell const &) const { return false; } bool macro_definition_cell::operator==(macro_definition_cell const & other) const { return typeid(*this) == typeid(other); } @@ -297,7 +276,6 @@ expr mk_app(expr const & f, expr const & a) { return cache(expr(new expr_app(f, expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info const & i) { return cache(expr(new expr_binding(k, n, t, e, i))); } -expr mk_let(name const & n, expr const & t, expr const & v, expr const & e) { return cache(expr(new expr_let(n, t, v, e))); } expr mk_sort(level const & l) { return cache(expr(new expr_sort(l))); } // ======================================= @@ -319,7 +297,6 @@ void expr_cell::dealloc() { case expr_kind::App: static_cast(it)->dealloc(todo); break; case expr_kind::Lambda: case expr_kind::Pi: static_cast(it)->dealloc(todo); break; - case expr_kind::Let: static_cast(it)->dealloc(todo); break; } } } catch (std::bad_alloc&) { @@ -443,7 +420,7 @@ unsigned get_depth(expr const & e) { case expr_kind::Meta: case expr_kind::Local: return 1; case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Macro: - case expr_kind::App: case expr_kind::Let: + case expr_kind::App: return static_cast(e.raw())->m_depth; } lean_unreachable(); // LCOV_EXCL_LINE @@ -458,7 +435,7 @@ unsigned get_free_var_range(expr const & e) { case expr_kind::Meta: case expr_kind::Local: return get_free_var_range(mlocal_type(e)); case expr_kind::Lambda: case expr_kind::Pi: - case expr_kind::App: case expr_kind::Let: + case expr_kind::App: case expr_kind::Macro: return static_cast(e.raw())->m_free_var_range; } @@ -501,13 +478,6 @@ expr update_binding(expr const & e, expr const & new_domain, expr const & new_bo return e; } -expr update_let(expr const & e, expr const & new_type, expr const & new_val, expr const & new_body) { - if (!is_eqp(let_type(e), new_type) || !is_eqp(let_value(e), new_val) || !is_eqp(let_body(e), new_body)) - return copy_tag(e, mk_let(let_name(e), new_type, new_val, new_body)); - else - return e; -} - expr update_mlocal(expr const & e, expr const & new_type) { if (is_eqp(mlocal_type(e), new_type)) return e; @@ -551,9 +521,9 @@ bool is_atomic(expr const & e) { return true; case expr_kind::Macro: return to_macro(e)->get_num_args() == 0; - case expr_kind::App: case expr_kind::Let: - case expr_kind::Meta: case expr_kind::Local: - case expr_kind::Lambda: case expr_kind::Pi: + case expr_kind::App: case expr_kind::Meta: + case expr_kind::Local: case expr_kind::Lambda: + case expr_kind::Pi: return false; } lean_unreachable(); // LCOV_EXCL_LINE @@ -569,4 +539,37 @@ bool is_arrow(expr const & t) { return res; } } + +static name g_let("let"); +std::string const & get_let_macro_opcode() { + static std::string g_let_macro_opcode("let"); + return g_let_macro_opcode; +} + +/** + \brief We use a macro to mark expressions that denote "let"-expressions. + This marks have no real semantic meaning, but are used by Lean's pretty printer. +*/ +class let_macro_definition_cell : public macro_definition_cell { + static void check_macro(expr const & m) { + if (!is_macro(m) || macro_num_args(m) != 1) + throw exception("invalid 'let' macro"); + } +public: + virtual name get_name() const { return g_let; } + virtual expr get_type(expr const & m, expr const * arg_types, extension_context &) const { + check_macro(m); + return arg_types[0]; + } + virtual optional expand(expr const & m, extension_context &) const { + check_macro(m); + return some_expr(macro_arg(m, 0)); + } + virtual void write(serializer & s) const { s.write_string(get_let_macro_opcode()); } +}; + +static macro_definition g_let_macro_definition(new let_macro_definition_cell()); +expr mk_let_macro(expr const & e) { return mk_macro(g_let_macro_definition, 1, &e); } +bool is_let_macro(expr const & e) { return is_macro(e) && macro_def(e) == g_let_macro_definition; } +expr let_macro_arg(expr const & e) { lean_assert(is_let_macro(e)); return macro_arg(e, 0); } } diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 2dc6e4bd6..019a227bd 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -40,11 +40,10 @@ class expr; | App expr expr | Lambda name expr expr | Pi name expr expr - | Let name expr expr expr | Macro macro */ -enum class expr_kind { Var, Sort, Constant, Meta, Local, App, Lambda, Pi, Let, Macro }; +enum class expr_kind { Var, Sort, Constant, Meta, Local, App, Lambda, Pi, Macro }; class expr_cell { protected: // The bits of the following field mean: @@ -132,7 +131,6 @@ public: friend expr mk_pair(expr const & f, expr const & s, expr const & t); friend expr mk_proj(bool fst, expr const & p); friend expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info const & i); - friend expr mk_let(name const & n, expr const & t, expr const & v, expr const & e); friend expr mk_macro(macro_definition const & m, unsigned num, expr const * args); friend bool is_eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; } @@ -290,23 +288,6 @@ public: binder const & get_binder() const { return m_binder; } }; -/** \brief Let expressions */ -class expr_let : public expr_composite { - name m_name; - expr m_type; - expr m_value; - expr m_body; - friend class expr_cell; - void dealloc(buffer & todelete); -public: - expr_let(name const & n, expr const & t, expr const & v, expr const & b); - ~expr_let(); - name const & get_name() const { return m_name; } - expr const & get_type() const { return m_type; } - expr const & get_value() const { return m_value; } - expr const & get_body() const { return m_body; } -}; - /** \brief Sort */ class expr_sort : public expr_cell { level m_level; @@ -404,7 +385,6 @@ inline bool is_app(expr_cell * e) { return e->kind() == expr_kind::App; inline bool is_lambda(expr_cell * e) { return e->kind() == expr_kind::Lambda; } inline bool is_pi(expr_cell * e) { return e->kind() == expr_kind::Pi; } inline bool is_sort(expr_cell * e) { return e->kind() == expr_kind::Sort; } -inline bool is_let(expr_cell * e) { return e->kind() == expr_kind::Let; } inline bool is_binding(expr_cell * e) { return is_lambda(e) || is_pi(e); } inline bool is_mlocal(expr_cell * e) { return is_metavar(e) || is_local(e); } @@ -417,7 +397,6 @@ inline bool is_app(expr const & e) { return e.kind() == expr_kind::App; } inline bool is_lambda(expr const & e) { return e.kind() == expr_kind::Lambda; } inline bool is_pi(expr const & e) { return e.kind() == expr_kind::Pi; } inline bool is_sort(expr const & e) { return e.kind() == expr_kind::Sort; } -inline bool is_let(expr const & e) { return e.kind() == expr_kind::Let; } inline bool is_binding(expr const & e) { return is_lambda(e) || is_pi(e); } inline bool is_mlocal(expr const & e) { return is_metavar(e) || is_local(e); } @@ -455,7 +434,6 @@ inline expr mk_lambda(name const & n, expr const & t, expr const & e, binder_inf inline expr mk_pi(name const & n, expr const & t, expr const & e, binder_info const & i = binder_info()) { return mk_binding(expr_kind::Pi, n, t, e, i); } -expr mk_let(name const & n, expr const & t, expr const & v, expr const & e); expr mk_sort(level const & l); /** \brief Return Pi(x.{sz-1}, domain[sz-1], ..., Pi(x.{0}, domain[0], range)...) */ @@ -517,7 +495,6 @@ inline expr_var * to_var(expr_cell * e) { lean_assert(is_var(e)); inline expr_const * to_constant(expr_cell * e) { lean_assert(is_constant(e)); return static_cast(e); } inline expr_app * to_app(expr_cell * e) { lean_assert(is_app(e)); return static_cast(e); } inline expr_binding * to_binding(expr_cell * e) { lean_assert(is_binding(e)); return static_cast(e); } -inline expr_let * to_let(expr_cell * e) { lean_assert(is_let(e)); return static_cast(e); } inline expr_sort * to_sort(expr_cell * e) { lean_assert(is_sort(e)); return static_cast(e); } inline expr_mlocal * to_mlocal(expr_cell * e) { lean_assert(is_mlocal(e)); return static_cast(e); } inline expr_local * to_local(expr_cell * e) { lean_assert(is_local(e)); return static_cast(e); } @@ -528,7 +505,6 @@ inline expr_var * to_var(expr const & e) { return to_var(e.raw() inline expr_const * to_constant(expr const & e) { return to_constant(e.raw()); } inline expr_app * to_app(expr const & e) { return to_app(e.raw()); } inline expr_binding * to_binding(expr const & e) { return to_binding(e.raw()); } -inline expr_let * to_let(expr const & e) { return to_let(e.raw()); } inline expr_sort * to_sort(expr const & e) { return to_sort(e.raw()); } inline expr_mlocal * to_mlocal(expr const & e) { return to_mlocal(e.raw()); } inline expr_mlocal * to_metavar(expr const & e) { return to_metavar(e.raw()); } @@ -557,10 +533,6 @@ inline expr const & binding_body(expr_cell * e) { return to_binding(e inline binder_info const & binding_info(expr_cell * e) { return to_binding(e)->get_info(); } inline binder const & binding_binder(expr_cell * e) { return to_binding(e)->get_binder(); } inline level const & sort_level(expr_cell * e) { return to_sort(e)->get_level(); } -inline name const & let_name(expr_cell * e) { return to_let(e)->get_name(); } -inline expr const & let_value(expr_cell * e) { return to_let(e)->get_value(); } -inline expr const & let_type(expr_cell * e) { return to_let(e)->get_type(); } -inline expr const & let_body(expr_cell * e) { return to_let(e)->get_body(); } inline name const & mlocal_name(expr_cell * e) { return to_mlocal(e)->get_name(); } inline expr const & mlocal_type(expr_cell * e) { return to_mlocal(e)->get_type(); } @@ -582,10 +554,6 @@ inline expr const & binding_body(expr const & e) { return to_binding( inline binder_info const & binding_info(expr const & e) { return to_binding(e)->get_info(); } inline binder const & binding_binder(expr const & e) { return to_binding(e)->get_binder(); } inline level const & sort_level(expr const & e) { return to_sort(e)->get_level(); } -inline name const & let_name(expr const & e) { return to_let(e)->get_name(); } -inline expr const & let_value(expr const & e) { return to_let(e)->get_value(); } -inline expr const & let_type(expr const & e) { return to_let(e)->get_type(); } -inline expr const & let_body(expr const & e) { return to_let(e)->get_body(); } inline name const & mlocal_name(expr const & e) { return to_mlocal(e)->get_name(); } inline expr const & mlocal_type(expr const & e) { return to_mlocal(e)->get_type(); } inline name const & local_pp_name(expr const & e) { return to_local(e)->get_pp_name(); } @@ -666,12 +634,19 @@ expr update_app(expr const & e, expr const & new_fn, expr const & new_arg); expr update_rev_app(expr const & e, unsigned num, expr const * new_args); template expr update_rev_app(expr const & e, C const & c) { return update_rev_app(e, c.size(), c.data()); } expr update_binding(expr const & e, expr const & new_domain, expr const & new_body); -expr update_let(expr const & e, expr const & new_type, expr const & new_val, expr const & new_body); expr update_mlocal(expr const & e, expr const & new_type); expr update_sort(expr const & e, level const & new_level); expr update_constant(expr const & e, levels const & new_levels); expr update_macro(expr const & e, unsigned num, expr const * args); // ======================================= +// ======================================= +// Auxiliary macro for "marking" let-expressions +expr mk_let_macro(expr const & e); +bool is_let_macro(expr const & e); +expr let_macro_arg(expr const & e); +std::string const & get_let_macro_opcode(); +// ======================================= + std::ostream & operator<<(std::ostream & out, expr const & e); } diff --git a/src/kernel/expr_eq_fn.cpp b/src/kernel/expr_eq_fn.cpp index 3f067ba0c..17e5720fc 100644 --- a/src/kernel/expr_eq_fn.cpp +++ b/src/kernel/expr_eq_fn.cpp @@ -58,12 +58,6 @@ bool expr_eq_fn::apply(expr const & a, expr const & b) { return false; } return true; - case expr_kind::Let: - m_counter++; - return - apply(let_type(a), let_type(b)) && - apply(let_value(a), let_value(b)) && - apply(let_body(a), let_body(b)); } lean_unreachable(); // LCOV_EXCL_LINE } diff --git a/src/kernel/for_each_fn.cpp b/src/kernel/for_each_fn.cpp index 3583a0ad1..159989a77 100644 --- a/src/kernel/for_each_fn.cpp +++ b/src/kernel/for_each_fn.cpp @@ -64,11 +64,6 @@ void for_each_fn::apply(expr const & e, unsigned offset) { todo.emplace_back(binding_body(e), offset + 1); todo.emplace_back(binding_domain(e), offset); goto begin_loop; - case expr_kind::Let: - todo.emplace_back(let_body(e), offset + 1); - todo.emplace_back(let_value(e), offset); - todo.emplace_back(let_type(e), offset); - goto begin_loop; } } } diff --git a/src/kernel/formatter.cpp b/src/kernel/formatter.cpp index 452f81aa2..df3da5eac 100644 --- a/src/kernel/formatter.cpp +++ b/src/kernel/formatter.cpp @@ -37,13 +37,6 @@ std::pair binding_body_fresh(expr const & b, bool preserve_type) { return mk_pair(instantiate(binding_body(b), c), c); } -std::pair let_body_fresh(expr const & l, bool preserve_type) { - lean_assert(is_let(l)); - name n = pick_unused_name(let_body(l), let_name(l)); - expr c = mk_local(n, preserve_type ? let_type(l) : expr()); - return mk_pair(instantiate(let_body(l), c), c); -} - /** \brief Very basic printer for expressions. It is mainly used when debugging code. @@ -66,10 +59,35 @@ struct print_expr_fn { } } + bool print_let(expr const & a) { + if (!is_let_macro(a)) + return false; + expr l = let_macro_arg(a); + if (!is_app(l) || !is_lambda(app_fn(l))) + return false; + name n = binding_name(app_fn(l)); + expr t = binding_domain(app_fn(l)); + expr b = binding_body(app_fn(l)); + expr v = app_arg(l); + n = pick_unused_name(b, n); + expr c = mk_local(n, expr()); + b = instantiate(b, c); + out() << "let " << c; + out() << " : "; + print(t); + out() << " := "; + print(v); + out() << " in "; + print_child(b); + return true; + } + void print_macro(expr const & a) { - macro_def(a).display(out()); - for (unsigned i = 0; i < macro_num_args(a); i++) { - out() << " "; print_child(macro_arg(a, i)); + if (!print_let(a)) { + macro_def(a).display(out()); + for (unsigned i = 0; i < macro_num_args(a); i++) { + out() << " "; print_child(macro_arg(a, i)); + } } } @@ -103,19 +121,6 @@ struct print_expr_fn { return print_child(a); } - void print_let(expr const & a) { - auto p = let_body_fresh(a); - expr const & b = p.first; - expr const & n = p.second; - out() << "let " << n; - out() << " : "; - print(let_type(a)); - out() << " := "; - print(let_value(a)); - out() << " in "; - print_child(b); - } - void print_binding(char const * bname, expr e) { expr_kind k = e.kind(); out() << bname; @@ -190,9 +195,6 @@ struct print_expr_fn { print_arrow_body(lower_free_vars(binding_body(a), 1)); } break; - case expr_kind::Let: - print_let(a); - break; case expr_kind::Sort: print_sort(a); break; diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp index 5c4d47301..fc7125add 100644 --- a/src/kernel/free_vars.cpp +++ b/src/kernel/free_vars.cpp @@ -69,9 +69,6 @@ protected: case expr_kind::Lambda: case expr_kind::Pi: result = apply(binding_domain(e), offset) || apply(binding_body(e), offset + 1); break; - case expr_kind::Let: - result = apply(let_type(e), offset) || apply(let_value(e), offset) || apply(let_body(e), offset + 1); - break; case expr_kind::Macro: for (unsigned i = 0; i < macro_num_args(e); i++) { if (apply(macro_arg(e, i), offset)) { diff --git a/src/kernel/replace_fn.cpp b/src/kernel/replace_fn.cpp index 6c4769d9d..64815f26d 100644 --- a/src/kernel/replace_fn.cpp +++ b/src/kernel/replace_fn.cpp @@ -101,19 +101,11 @@ expr replace_fn::operator()(expr const & e) { r = update_binding(e, rs(-2), rs(-1)); pop_rs(2); break; - case expr_kind::Let: - if (check_index(f, 0) && !visit(let_type(e), offset)) - goto begin_loop; - if (check_index(f, 1) && !visit(let_value(e), offset)) - goto begin_loop; - if (check_index(f, 2) && !visit(let_body(e), offset + 1)) - goto begin_loop; - r = update_let(e, rs(-3), rs(-2), rs(-1)); - pop_rs(3); - break; case expr_kind::Macro: while (f.m_index < macro_num_args(e)) { - if (!visit(macro_arg(e, f.m_index), offset)) + unsigned idx = f.m_index; + f.m_index++; + if (!visit(macro_arg(e, idx), offset)) goto begin_loop; } r = update_macro(e, macro_num_args(e), &rs(-macro_num_args(e))); diff --git a/src/kernel/replace_visitor.cpp b/src/kernel/replace_visitor.cpp index 6bc203967..8ccd6e9d2 100644 --- a/src/kernel/replace_visitor.cpp +++ b/src/kernel/replace_visitor.cpp @@ -30,13 +30,6 @@ expr replace_visitor::visit_binding(expr const & e) { } expr replace_visitor::visit_lambda(expr const & e) { return visit_binding(e); } expr replace_visitor::visit_pi(expr const & e) { return visit_binding(e); } -expr replace_visitor::visit_let(expr const & e) { - lean_assert(is_let(e)); - expr new_t = visit(let_type(e)); - expr new_v = visit(let_value(e)); - expr new_b = visit(let_body(e)); - return update_let(e, new_t, new_v, new_b); -} expr replace_visitor::visit_macro(expr const & e) { lean_assert(is_macro(e)); buffer new_args; @@ -69,7 +62,6 @@ expr replace_visitor::visit(expr const & e) { case expr_kind::App: return save_result(e, visit_app(e), shared); case expr_kind::Lambda: return save_result(e, visit_lambda(e), shared); case expr_kind::Pi: return save_result(e, visit_pi(e), shared); - case expr_kind::Let: return save_result(e, visit_let(e), shared); } lean_unreachable(); // LCOV_EXCL_LINE diff --git a/src/kernel/replace_visitor.h b/src/kernel/replace_visitor.h index bf32cfe92..a0dd57608 100644 --- a/src/kernel/replace_visitor.h +++ b/src/kernel/replace_visitor.h @@ -30,7 +30,6 @@ protected: virtual expr visit_binding(expr const &); virtual expr visit_lambda(expr const &); virtual expr visit_pi(expr const &); - virtual expr visit_let(expr const &); virtual expr visit(expr const &); public: expr operator()(expr const & e) { return visit(e); } diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index bc138e975..4da46a85a 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -203,20 +203,6 @@ expr type_checker::ensure_pi_core(expr e, expr const & s) { } } -/** - \brief Create a justification for a let definition type mismatch, - \c e is the let expression, and \c val_type is the type inferred for the let value. -*/ -justification type_checker::mk_let_mismatch_jst(expr const & e, expr const & val_type) { - lean_assert(is_let(e)); - return mk_justification(e, - [=](formatter const & fmt, options const & o, substitution const & subst) { - return pp_def_type_mismatch(fmt, m_env, o, let_name(e), - subst.instantiate_metavars_wo_jst(let_type(e)), - subst.instantiate_metavars_wo_jst(val_type)); - }); -} - static constexpr char const * g_macro_error_msg = "failed to type check macro expansion"; justification type_checker::mk_macro_jst(expr const & e) { @@ -343,23 +329,7 @@ expr type_checker::infer_type_core(expr const & e, bool infer_only) { } r = instantiate(binding_body(f_type), app_arg(e)); break; - } - case expr_kind::Let: - if (!infer_only) { - ensure_sort_core(infer_type_core(let_type(e), infer_only), let_type(e)); - expr val_type = infer_type_core(let_value(e), infer_only); - simple_delayed_justification jst([=]() { return mk_let_mismatch_jst(e, val_type); }); - if (!is_def_eq(val_type, let_type(e), jst)) { - environment env = m_env; - throw_kernel_exception(env, e, - [=](formatter const & fmt, options const & o) { - return pp_def_type_mismatch(fmt, env, o, let_name(e), let_type(e), val_type); - }); - } - } - r = infer_type_core(instantiate(let_body(e), let_value(e)), infer_only); - break; - } + }} if (m_memoize) m_infer_type_cache[infer_only].insert(mk_pair(e, r)); diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index f1843f7e5..76d296536 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -76,7 +76,6 @@ class type_checker { bool meta_to_telescope_core(expr const & e, buffer & telescope, buffer> & locals); expr ensure_sort_core(expr e, expr const & s); expr ensure_pi_core(expr e, expr const & s); - justification mk_let_mismatch_jst(expr const & e, expr const & val_type); justification mk_macro_jst(expr const & e); void check_level(level const & l, expr const & s); expr infer_type_core(expr const & e, bool infer_only); diff --git a/src/library/deep_copy.cpp b/src/library/deep_copy.cpp index c0c0a1c4a..9fbd6f0f7 100644 --- a/src/library/deep_copy.cpp +++ b/src/library/deep_copy.cpp @@ -19,7 +19,6 @@ expr copy(expr const & a) { case expr_kind::App: return mk_app(app_fn(a), app_arg(a)); case expr_kind::Lambda: return mk_lambda(binding_name(a), binding_domain(a), binding_body(a), binding_info(a)); case expr_kind::Pi: return mk_pi(binding_name(a), binding_domain(a), binding_body(a), binding_info(a)); - case expr_kind::Let: return mk_let(let_name(a), let_type(a), let_value(a), let_body(a)); case expr_kind::Meta: return mk_metavar(mlocal_name(a), mlocal_type(a)); case expr_kind::Local: return mk_local(mlocal_name(a), local_pp_name(a), mlocal_type(a)); } diff --git a/src/library/expr_lt.cpp b/src/library/expr_lt.cpp index 4ae997fdb..ee45fcdde 100644 --- a/src/library/expr_lt.cpp +++ b/src/library/expr_lt.cpp @@ -40,14 +40,6 @@ bool is_lt(expr const & a, expr const & b, bool use_hash) { return is_lt(binding_body(a), binding_body(b), use_hash); case expr_kind::Sort: return is_lt(sort_level(a), sort_level(b), use_hash); - case expr_kind::Let: - if (let_type(a) != let_type(b)) { - return is_lt(let_type(a), let_type(b), use_hash); - } else if (let_value(a) != let_value(b)){ - return is_lt(let_value(a), let_value(b), use_hash); - } else { - return is_lt(let_body(a), let_body(b), use_hash); - } case expr_kind::Local: case expr_kind::Meta: if (mlocal_name(a) != mlocal_name(b)) return mlocal_name(a) < mlocal_name(b); diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 8e695b950..c2ebd3965 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -325,13 +325,6 @@ expr & to_macro_app(lua_State * L, int idx) { return r; } -expr & to_let(lua_State * L, int idx) { - expr & r = to_expr(L, idx); - if (!is_let(r)) - throw exception(sstream() << "arg #" << idx << " must be a let-expression"); - return r; -} - static int expr_tostring(lua_State * L) { std::ostringstream out; formatter fmt = get_global_formatter(L); @@ -383,16 +376,6 @@ static int expr_mk_arrow(lua_State * L) { r = mk_arrow(to_expr(L, i), r); return push_expr(L, r); } -static int expr_mk_let(lua_State * L) { return push_expr(L, mk_let(to_name_ext(L, 1), to_expr(L, 2), to_expr(L, 3), to_expr(L, 4))); } - -static expr get_expr_from_table(lua_State * L, int t, int i) { - lua_pushvalue(L, t); // push table to the top - lua_pushinteger(L, i); - lua_gettable(L, -2); - expr r = to_expr(L, -1); - lua_pop(L, 2); // remove table and value - return r; -} static void throw_invalid_binder_table(int t) { #define VALID_FORMS "local_name, {local_name, bool}, {expr, expr}, {expr, expr, bool}, or {expr, expr, binder_info}, each entry represents a binder, the first expression in each entry must be a (local) constant, the second expression is the type, the optional Boolean can be used to mark implicit arguments." @@ -519,51 +502,6 @@ static int expr_mk_local(lua_State * L) { } static int expr_get_kind(lua_State * L) { return push_integer(L, static_cast(to_expr(L, 1).kind())); } -// t is a table of pairs {{a1, b1, c1}, ..., {ak, bk, ck}} -// ai, bi and ci are expressions -static std::tuple get_expr_triple_from_table(lua_State * L, int t, int i) { - lua_pushvalue(L, t); // push table on the top - lua_pushinteger(L, i); - lua_gettable(L, -2); // now table {ai, bi, ci} is on the top - if (!lua_istable(L, -1) || objlen(L, -1) != 3) - throw exception(sstream() << "arg #" << t << " must be of the form '{{expr, expr, expr}, ...}'"); - expr ai = get_expr_from_table(L, -1, 1); - expr bi = get_expr_from_table(L, -1, 2); - expr ci = get_expr_from_table(L, -1, 3); - lua_pop(L, 2); // pop table {ai, bi, ci} and t from stack - return std::make_tuple(ai, bi, ci); -} - -static int expr_let(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs < 2) - throw exception("function must have at least 2 arguments"); - if (nargs == 2) { - if (!lua_istable(L, 1)) - throw exception("function expects arg #1 to be of the form '{{expr, expr, expr}, ...}'"); - int len = objlen(L, 1); - if (len == 0) - throw exception("function expects arg #1 to be a non-empty table"); - expr r = to_expr(L, 2); - for (int i = len; i >= 1; i--) { - auto p = get_expr_triple_from_table(L, 1, i); - r = Let(std::get<0>(p), std::get<1>(p), std::get<2>(p), r); - } - return push_expr(L, r); - } else { - if ((nargs - 1) % 3 != 0) - throw exception("function must have 3*n + 1 arguments"); - expr r = to_expr(L, nargs); - for (int i = nargs - 1; i >= 1; i-=3) { - if (is_expr(L, i - 2)) - r = Let(to_expr(L, i - 2), to_expr(L, i - 1), to_expr(L, i), r); - else - r = Let(to_name_ext(L, i - 2), to_expr(L, i - 1), to_expr(L, i), r); - } - return push_expr(L, r); - } -} - #define EXPR_PRED(P) static int expr_ ## P(lua_State * L) { check_num_args(L, 1); return push_boolean(L, P(to_expr(L, 1))); } EXPR_PRED(is_constant) @@ -572,7 +510,6 @@ EXPR_PRED(is_app) EXPR_PRED(is_lambda) EXPR_PRED(is_pi) EXPR_PRED(is_binding) -EXPR_PRED(is_let) EXPR_PRED(is_macro) EXPR_PRED(is_metavar) EXPR_PRED(is_local) @@ -600,8 +537,6 @@ static int expr_fields(lua_State * L) { case expr_kind::Lambda: case expr_kind::Pi: push_name(L, binding_name(e)); push_expr(L, binding_domain(e)); push_expr(L, binding_body(e)); push_binder_info(L, binding_info(e)); return 4; - case expr_kind::Let: - push_name(L, let_name(e)); push_expr(L, let_type(e)); push_expr(L, let_value(e)); push_expr(L, let_body(e)); return 4; case expr_kind::Meta: case expr_kind::Local: push_name(L, mlocal_name(e)); push_expr(L, mlocal_type(e)); return 2; @@ -728,11 +663,6 @@ static int binding_domain(lua_State * L) { return push_expr(L, binding_domain(to static int binding_body(lua_State * L) { return push_expr(L, binding_body(to_binding(L, 1))); } static int binding_info(lua_State * L) { return push_binder_info(L, binding_info(to_binding(L, 1))); } -static int let_name(lua_State * L) { return push_name(L, let_name(to_let(L, 1))); } -static int let_type(lua_State * L) { return push_expr(L, let_type(to_let(L, 1))); } -static int let_value(lua_State * L) { return push_expr(L, let_value(to_let(L, 1))); } -static int let_body(lua_State * L) { return push_expr(L, let_body(to_let(L, 1))); } - static int expr_occurs(lua_State * L) { return push_boolean(L, occurs(to_expr(L, 1), to_expr(L, 2))); } static int expr_is_eqp(lua_State * L) { return push_boolean(L, is_eqp(to_expr(L, 1), to_expr(L, 2))); } static int expr_hash(lua_State * L) { return push_integer(L, to_expr(L, 1).hash()); } @@ -773,7 +703,6 @@ static const struct luaL_Reg expr_m[] = { {"is_lambda", safe_function}, {"is_pi", safe_function}, {"is_binding", safe_function}, - {"is_let", safe_function}, {"is_macro", safe_function}, {"is_meta", safe_function}, {"has_free_vars", safe_function}, @@ -790,10 +719,6 @@ static const struct luaL_Reg expr_m[] = { {"binding_domain", safe_function}, {"binding_body", safe_function}, {"binding_info", safe_function}, - {"let_name", safe_function}, - {"let_type", safe_function}, - {"let_value", safe_function}, - {"let_body", safe_function}, {"macro_def", safe_function}, {"macro_num_args", safe_function}, {"macro_arg", safe_function}, @@ -832,12 +757,10 @@ static void open_expr(lua_State * L) { SET_GLOBAL_FUN(expr_mk_lambda, "mk_lambda"); SET_GLOBAL_FUN(expr_mk_pi, "mk_pi"); SET_GLOBAL_FUN(expr_mk_arrow, "mk_arrow"); - SET_GLOBAL_FUN(expr_mk_let, "mk_let"); SET_GLOBAL_FUN(expr_mk_macro, "mk_macro"); SET_GLOBAL_FUN(expr_fun, "fun"); SET_GLOBAL_FUN(expr_fun, "Fun"); SET_GLOBAL_FUN(expr_pi, "Pi"); - SET_GLOBAL_FUN(expr_let, "Let"); SET_GLOBAL_FUN(expr_mk_sort, "mk_sort"); SET_GLOBAL_FUN(expr_mk_metavar, "mk_metavar"); SET_GLOBAL_FUN(expr_mk_local, "mk_local"); @@ -861,7 +784,6 @@ static void open_expr(lua_State * L) { SET_ENUM("App", expr_kind::App); SET_ENUM("Lambda", expr_kind::Lambda); SET_ENUM("Pi", expr_kind::Pi); - SET_ENUM("Let", expr_kind::Let); SET_ENUM("Macro", expr_kind::Macro); lua_setglobal(L, "expr_kind"); } diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp index ed024ffd9..aa8f974d7 100644 --- a/src/library/kernel_serializer.cpp +++ b/src/library/kernel_serializer.cpp @@ -159,9 +159,6 @@ class expr_serializer : public object_serializer alts; lean_assert(!is_var(rhs)); // rhs can't be a free variable (this is an invariant of the approach we are using). - lean_assert(!is_let(rhs)); // rhs can't be a let, since the rhs is in whnf. // Add Projections to alts unsigned vidx = margs.size() - 1; for (expr const & marg : margs) { diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index 066b7cb6c..f78426e3d 100644 --- a/src/tests/kernel/expr.cpp +++ b/src/tests/kernel/expr.cpp @@ -117,8 +117,6 @@ static unsigned count_core(expr const & a, expr_set & s) { return count_core(app_fn(a), s) + count_core(app_arg(a), s) + 1; case expr_kind::Lambda: case expr_kind::Pi: return count_core(binding_domain(a), s) + count_core(binding_body(a), s) + 1; - case expr_kind::Let: - return count_core(let_value(a), s) + count_core(let_body(a), s) + 1; } return 0; } @@ -269,7 +267,7 @@ static void tst13() { } static void tst14() { - expr l = mk_let("a", Bool, Const("b"), Var(0)); + expr l = Const("b"); check_serializer(l); std::cout << l << "\n"; lean_assert(closed(l)); @@ -292,11 +290,6 @@ static void tst15() { lean_assert(has_metavar(Pi({a, m}, a))); lean_assert(has_metavar(Fun({a, Type}, m))); lean_assert(has_metavar(Fun({a, m}, a))); - lean_assert(!has_metavar(Let(a, Type, Bool, a))); - lean_assert(!has_metavar(mk_let(name("a"), Type, f(x), f(f(x))))); - lean_assert(has_metavar(mk_let(name("a"), m, f(x), f(f(x))))); - lean_assert(has_metavar(mk_let(name("a"), Type, f(m), f(f(x))))); - lean_assert(has_metavar(mk_let(name("a"), Type, f(x), f(f(m))))); lean_assert(has_metavar(f(a, a, m))); lean_assert(has_metavar(f(a, m, a, a))); lean_assert(!has_metavar(f(a, a, a, a))); @@ -317,7 +310,6 @@ static void tst16() { check_copy(mk_metavar("M", Bool)); check_copy(mk_lambda("x", a, Var(0))); check_copy(mk_pi("x", a, Var(0))); - check_copy(mk_let("x", Bool, a, Var(0))); } static void tst17() { @@ -358,10 +350,6 @@ static void tst18() { lean_assert(has_local(Pi({a, l}, a))); lean_assert(has_local(Fun({a, Type}, l))); lean_assert(has_local(Fun({a, l}, a))); - lean_assert(!has_local(Let(a, Type, Bool, a))); - lean_assert(has_local(mk_let(name("a"), l, f(x), f(f(x))))); - lean_assert(has_local(mk_let(name("a"), Type, f(l), f(f(x))))); - lean_assert(has_local(mk_let(name("a"), Type, f(x), f(f(l))))); lean_assert(has_local(f(a, a, l))); lean_assert(has_local(f(a, l, a, a))); lean_assert(!has_local(f(a, a, a, a))); diff --git a/src/tests/kernel/instantiate.cpp b/src/tests/kernel/instantiate.cpp index 7021c08a7..dd4d06c8c 100644 --- a/src/tests/kernel/instantiate.cpp +++ b/src/tests/kernel/instantiate.cpp @@ -31,18 +31,8 @@ static void tst1() { lean_assert(beta_reduce(F3) == f(a, a)); } -static void tst2() { - expr x = Const("x"); - expr a = Const("a"); - expr f = Const("f"); - expr N = Const("N"); - expr F1 = Let(x, N, a, f(x)); - lean_assert(head_beta_reduce(F1) == F1); -} - int main() { save_stack_info(); tst1(); - tst2(); return has_violations() ? 1 : 0; } diff --git a/src/tests/kernel/max_sharing.cpp b/src/tests/kernel/max_sharing.cpp index 36d04c600..22bf53cc1 100644 --- a/src/tests/kernel/max_sharing.cpp +++ b/src/tests/kernel/max_sharing.cpp @@ -25,11 +25,6 @@ static void tst1() { std::cout << F2 << "\n"; lean_assert(is_eqp(app_arg(app_fn(F2)), app_arg(F2))); max_fn.clear(); - F1 = f(Let(x, Type, f(a1), f(x, x)), Let(y, Type, f(a1), f(y, y))); - lean_assert(!is_eqp(app_arg(app_fn(F1)), app_arg(F1))); - F2 = max_fn(F1); - std::cout << F2 << "\n"; - lean_assert(is_eqp(app_arg(app_fn(F2)), app_arg(F2))); } static void tst2() { diff --git a/src/tests/library/deep_copy.cpp b/src/tests/library/deep_copy.cpp index 8889121ac..90ccbe741 100644 --- a/src/tests/library/deep_copy.cpp +++ b/src/tests/library/deep_copy.cpp @@ -17,7 +17,7 @@ static void tst1() { expr t = Type; expr z = Const("z"); expr m = mk_metavar("a", Type); - expr F = mk_let("z", mk_Bool(), Type, mk_pi("y", t, mk_lambda("x", t, f(f(f(x, a), Const("10")), f(x, m))))); + expr F = mk_pi("y", t, mk_lambda("x", t, f(f(f(x, a), Const("10")), f(x, m)))); expr G = deep_copy(F); lean_assert(F == G); lean_assert(!is_eqp(F, G)); diff --git a/tests/lean/let1.lean b/tests/lean/let1.lean index 86c1f325f..0359347c1 100644 --- a/tests/lean/let1.lean +++ b/tests/lean/let1.lean @@ -1,7 +1,7 @@ -- Correct version -check let bool : Type.{1} := Type.{0}, - and (p q : bool) : bool := ∀ c : bool, (p → q → c) → c, - infixl `∧` 25 := and, +check let bool [inline] := Type.{0}, + and [inline] (p q : bool) := ∀ c : bool, (p → q → c) → c, + infixl `∧` 25 := and, and_intro (p q : bool) (H1 : p) (H2 : q) : p ∧ q := λ (c : bool) (H : p → q → c), H H1 H2, and_elim_left (p q : bool) (H : p ∧ q) : p @@ -10,10 +10,10 @@ check let bool : Type.{1} := Type.{0}, := H q (λ (H1 : p) (H2 : q), H2) in and_intro -check let bool : Type.{1} := Type.{0}, - and (p q : bool) : bool := ∀ c : bool, (p → q → c) → c, - infixl `∧` 25 := and, - and_intro (p q : bool) (H1 : p) (H2 : q) : q ∧ p +check let bool [inline] := Type.{0}, + and [inline] (p q : bool) := ∀ c : bool, (p → q → c) → c, + infixl `∧` 25 := and, + and_intro [fact] (p q : bool) (H1 : p) (H2 : q) : q ∧ p := λ (c : bool) (H : p → q → c), H H1 H2, and_elim_left (p q : bool) (H : p ∧ q) : p := H p (λ (H1 : p) (H2 : q), H1), diff --git a/tests/lean/let1.lean.expected.out b/tests/lean/let1.lean.expected.out index 8116c8b37..b572d9e92 100644 --- a/tests/lean/let1.lean.expected.out +++ b/tests/lean/let1.lean.expected.out @@ -1,5 +1,7 @@ -let bool : Type := Bool in (let and : bool -> bool -> bool := fun (p : bool) (q : bool), (Pi (c : bool) (a : p -> q -> c), c) in (let and_intro : Pi (p : bool) (q : bool) (H1 : p) (H2 : q), (and p q) := fun (p : bool) (q : bool) (H1 : p) (H2 : q) (c : bool) (H : p -> q -> c), (H H1 H2) in (let and_elim_left : Pi (p : bool) (q : bool) (H : and p q), p := fun (p : bool) (q : bool) (H : and p q), (H p (fun (H1 : p) (H2 : q), H1)) in (let and_elim_right : Pi (p : bool) (q : bool) (H : and p q), q := fun (p : bool) (q : bool) (H : and p q), (H q (fun (H1 : p) (H2 : q), H2)) in and_intro)))) : Pi (p : Bool) (q : Bool) (H1 : p) (H2 : q) (c : Bool) (H : p -> q -> c), c -let1.lean:16:10: error: type mismatch at definition 'and_intro', expected type +let and_intro : Pi (p : Bool) (q : Bool) (H1 : p) (H2 : q), ((fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q) := fun (p : Bool) (q : Bool) (H1 : p) (H2 : q) (c : Bool) (H : p -> q -> c), (H H1 H2) in (let and_elim_left : Pi (p : Bool) (q : Bool) (H : (fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q), p := fun (p : Bool) (q : Bool) (H : (fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q), (H p (fun (H1 : p) (H2 : q), H1)) in (let and_elim_right : Pi (p : Bool) (q : Bool) (H : (fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q), q := fun (p : Bool) (q : Bool) (H : (fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q), (H q (fun (H1 : p) (H2 : q), H2)) in and_intro)) : Pi (p : Bool) (q : Bool) (H1 : p) (H2 : q), ((fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q) +let1.lean:17:20: error: type mismatch at application + (fun (and_intro : Pi (p : Bool) (q : Bool) (H1 : p) (H2 : q), ((fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) q p)), (let and_elim_left : Pi (p : Bool) (q : Bool) (H : (fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q), p := fun (p : Bool) (q : Bool) (H : (fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q), (H p (fun (H1 : p) (H2 : q), H1)) in (let and_elim_right : Pi (p : Bool) (q : Bool) (H : (fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q), q := fun (p : Bool) (q : Bool) (H : (fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) p q), (H q (fun (H1 : p) (H2 : q), H2)) in and_intro))) (fun (p : Bool) (q : Bool) (H1 : p) (H2 : q) (c : Bool) (H : p -> q -> c), (H H1 H2)) +expected type: Pi (p : Bool) (q : Bool) (H1 : p) (H2 : q), ((fun (p : Bool) (q : Bool), (Pi (c : Bool) (a : p -> q -> c), c)) q p) given type: Pi (p : Bool) (q : Bool) (H1 : p) (H2 : q) (c : Bool) (H : p -> q -> c), c diff --git a/tests/lua/expr3.lua b/tests/lua/expr3.lua index 8bc0a4d3d..5bcf1242c 100644 --- a/tests/lua/expr3.lua +++ b/tests/lua/expr3.lua @@ -22,7 +22,6 @@ local l2 = mk_lambda("a", Bool, Var(0), binder_info(true, false)) assert(not l1:binding_info():is_implicit()) assert(l2:binding_info():is_implicit()) -local let1 = mk_let("a", Bool, Const("true"), f(Var(0))) local b = Const("b") local pi3 = Pi({{a, Bool}, {b, Bool}}, a) diff --git a/tests/lua/expr7.lua b/tests/lua/expr7.lua index 4f9ea9966..bd5f4a796 100644 --- a/tests/lua/expr7.lua +++ b/tests/lua/expr7.lua @@ -5,6 +5,4 @@ local T = Const("T") print(Pi({{A, Type}, {a, A}, {A, vec(A)}, {a, A}}, a)) local t = mk_pi("A", Type, mk_pi("a", Var(0), mk_pi("A", vec(Var(1)), mk_pi("a", Var(0), T(Var(0), Var(2)))))) print(t) -print(Let(A, Type, Bool, Pi(a, A, Let(A, Type, A, Pi(a, A, a))))) -print(mk_let("A", Type, Bool, mk_pi("a", Var(0), mk_let("A", Type, Var(1), mk_pi("a", Var(0), T(Var(0), Var(1), Var(2))))))) -print(mk_let("A", Type, Bool, mk_pi("a", Var(0), mk_let("A", Type, Var(1), mk_pi("a", Var(0), T(Var(0), Var(1), Var(2), Var(3))))))) + diff --git a/tests/lua/let1.lua b/tests/lua/let1.lua deleted file mode 100644 index 8f9f891c4..000000000 --- a/tests/lua/let1.lua +++ /dev/null @@ -1,25 +0,0 @@ -assert(not mk_let("a", Type, Var(0), Var(0)):closed()) -local env = bare_environment() -local A = Const("A") -env = add_decl(env, mk_var_decl("A", Type)) -env = add_decl(env, mk_var_decl("g", mk_arrow(A, mk_arrow(A, A)))) -env = add_decl(env, mk_var_decl("f", mk_arrow(A, Bool))) -env = add_decl(env, mk_var_decl("a", A)) -local a = Const("a") -local b = Const("b") -local x = Const("x") -local y = Const("y") -local g = Const("g") -local f = Const("f") -local tc = type_checker(env) -print(Let(x, A, a, f(x))) -print(Let(x, A, a, y, A, f(f(x)), f(x))) -assert(Let(x, A, a, y, A, f(f(x)), f(x)) == Let({{x, A, a}, {y, A, f(f(x))}}, f(x))) -print(Let({{x, A, a}, {y, A, g(g(x), x, a)}}, f(y))) -local t = Let({{x, A, a}, {y, A, g(g(x), x, a)}}, f(y)) -assert(t:let_name() == name("x")) -assert(t:let_type() == A) -assert(t:let_value() == a) -assert(t:let_body():is_let()) -print(tc:check(Let({{x, A, a}, {y, A, g(g(x, a), x)}}, f(y)))) -