michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(kernel): remove 'let'-expressions

Browse source 
We simulate it in the following way:
1- An opaque 'let'-expressions (let x : t := v in b) is encoded as
      ((fun (x : t), b) v)
   We also use a macro (let-macro) to mark this pattern.
   Thus, the pretty-printer knows how to display it correctly.

2- Transparent 'let'-expressions are eagerly expanded by the parser.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-24 16:27:23 -07:00
parent 609aeae390
commit 603dafbaf7
32 changed files with 147 additions and 355 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

50
src/frontends/lean/builtin_exprs.cpp
View file

@ -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<parameter> 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 &) {

6
src/frontends/lean/parser.cpp
View file

@ -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<expr> args;
for (unsigned i = 0; i < macro_num_args(e); i++)

5
src/kernel/abstract.h
View file

@ -61,9 +61,4 @@ template<typename T> 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)); }
}

7
src/kernel/converter.cpp
View file

@ -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<expr> 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;
}

73
src/kernel/expr.cpp
View file

@ -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<expr_cell*> & 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<expr_app*>(it)->dealloc(todo); break;
case expr_kind::Lambda:
case expr_kind::Pi: static_cast<expr_binding*>(it)->dealloc(todo); break;
case expr_kind::Let: static_cast<expr_let*>(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<expr_composite*>(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<expr_composite*>(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<expr> 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); }
}

43
src/kernel/expr.h
View file

@ -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<expr_cell*> & 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 <tt>Pi(x.{sz-1}, domain[sz-1], ..., Pi(x.{0}, domain[0], range)...)</tt> */
@ -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<expr_const*>(e); }
inline expr_app * to_app(expr_cell * e) { lean_assert(is_app(e)); return static_cast<expr_app*>(e); }
inline expr_binding * to_binding(expr_cell * e) { lean_assert(is_binding(e)); return static_cast<expr_binding*>(e); }
inline expr_let * to_let(expr_cell * e) { lean_assert(is_let(e)); return static_cast<expr_let*>(e); }
inline expr_sort * to_sort(expr_cell * e) { lean_assert(is_sort(e)); return static_cast<expr_sort*>(e); }
inline expr_mlocal * to_mlocal(expr_cell * e) { lean_assert(is_mlocal(e)); return static_cast<expr_mlocal*>(e); }
inline expr_local * to_local(expr_cell * e) { lean_assert(is_local(e)); return static_cast<expr_local*>(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<typename C> 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);
}

6
src/kernel/expr_eq_fn.cpp
View file

@ -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
}

5
src/kernel/for_each_fn.cpp
View file

@ -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;
}
}
}

54
src/kernel/formatter.cpp
View file

@ -37,13 +37,6 @@ std::pair<expr, expr> binding_body_fresh(expr const & b, bool preserve_type) {
return mk_pair(instantiate(binding_body(b), c), c);
}
std::pair<expr, expr> 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;

3
src/kernel/free_vars.cpp
View file

@ -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)) {

14
src/kernel/replace_fn.cpp
View file

@ -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)));

8
src/kernel/replace_visitor.cpp
View file

@ -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<expr> 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

1
src/kernel/replace_visitor.h
View file

@ -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); }

32
src/kernel/type_checker.cpp
View file

@ -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));

1
src/kernel/type_checker.h
View file

@ -76,7 +76,6 @@ class type_checker {
bool meta_to_telescope_core(expr const & e, buffer<expr> & telescope, buffer<optional<expr>> & 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);

1
src/library/deep_copy.cpp
View file

@ -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));
}

8
src/library/expr_lt.cpp
View file

@ -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);

78
src/library/kernel_bindings.cpp
View file

@ -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<int>(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<expr, expr, expr> 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<expr_is_lambda>},
{"is_pi", safe_function<expr_is_pi>},
{"is_binding", safe_function<expr_is_binding>},
{"is_let", safe_function<expr_is_let>},
{"is_macro", safe_function<expr_is_macro>},
{"is_meta", safe_function<expr_is_meta>},
{"has_free_vars", safe_function<expr_has_free_vars>},
@ -790,10 +719,6 @@ static const struct luaL_Reg expr_m[] = {
{"binding_domain", safe_function<binding_domain>},
{"binding_body", safe_function<binding_body>},
{"binding_info", safe_function<binding_info>},
{"let_name", safe_function<let_name>},
{"let_type", safe_function<let_type>},
{"let_value", safe_function<let_value>},
{"let_body", safe_function<let_body>},
{"macro_def", safe_function<macro_def>},
{"macro_num_args", safe_function<macro_num_args>},
{"macro_arg", safe_function<macro_arg>},
@ -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");
}

18
src/library/kernel_serializer.cpp
View file

@ -159,9 +159,6 @@ class expr_serializer : public object_serializer<expr, expr_hash_alloc, expr_eqp
case expr_kind::Lambda: case expr_kind::Pi:
s << binding_name(a) << binding_info(a); write_core(binding_domain(a)); write_core(binding_body(a));
break;
case expr_kind::Let:
s << let_name(a); write_core(let_type(a)); write_core(let_value(a)); write_core(let_body(a));
break;
case expr_kind::Meta:
s << mlocal_name(a); write_core(mlocal_type(a));
break;
@ -215,12 +212,6 @@ public:
}
case expr_kind::Lambda: case expr_kind::Pi:
return read_binding(k);
case expr_kind::Let: {
name n = read_name(d);
expr t = read();
expr v = read();
return mk_let(n, t, v, read());
}
case expr_kind::Meta: {
name n = read_name(d);
return mk_metavar(n, read());
@ -341,4 +332,13 @@ inductive_decls read_inductive_decls(deserializer & d) {
}
return inductive_decls(ps, num_params, to_list(decls.begin(), decls.end()));
}
static register_macro_deserializer_fn
let_macro_des_fn(get_let_macro_opcode(),
[](deserializer &, unsigned num, expr const * args) {
if (num != 1)
throw_corrupted_file();
return mk_let_macro(args[0]);
});
}

3
src/library/max_sharing.cpp
View file

@ -38,9 +38,6 @@ struct max_sharing_fn::imp {
case expr_kind::Lambda: case expr_kind::Pi:
res = update_binding(a, apply(binding_domain(a)), apply(binding_body(a)));
break;
case expr_kind::Let:
res = update_let(a, apply(let_type(a)), apply(let_value(a)), apply(let_body(a)));
break;
case expr_kind::Meta: case expr_kind::Local:
res = update_mlocal(a, apply(mlocal_type(a)));
break;

2
src/library/normalize.cpp
View file

@ -37,8 +37,6 @@ class normalize_fn {
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Sort:
case expr_kind::Meta: case expr_kind::Local: case expr_kind::Macro:
return e;
case expr_kind::Let:
lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::Lambda: case expr_kind::Pi:
return normalize_binding(e);
case expr_kind::App:

2
src/library/resolve_macro.cpp
View file

@ -289,7 +289,7 @@ expr mk_resolve_macro(expr const & l, expr const & H1, expr const & H2) {
return mk_macro(g_resolve_macro_definition, 3, args);
}
register_macro_deserializer_fn
static register_macro_deserializer_fn
resolve_macro_des_fn(g_resolve_opcode,
[](deserializer &, unsigned num, expr const * args) {
if (num != 3)

1
src/library/unifier.cpp
View file

@ -822,7 +822,6 @@ struct unifier_fn {
expr mtype = mlocal_type(m);
buffer<constraints> 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) {

14
src/tests/kernel/expr.cpp
View file

@ -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)));

10
src/tests/kernel/instantiate.cpp
View file

@ -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;
}

5
src/tests/kernel/max_sharing.cpp
View file

@ -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() {

2
src/tests/library/deep_copy.cpp
View file

@ -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));

14
tests/lean/let1.lean
View file

@ -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),

6
tests/lean/let1.lean.expected.out
View file

@ -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

1
tests/lua/expr3.lua
View file

@ -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)

4
tests/lua/expr7.lua
View file

@ -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)))))))

25
tests/lua/let1.lua
View file

@ -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))))