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

refactor(kernel/expr): remove silly overloads

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-16 13:37:55 -07:00
parent c4f02bd16a
commit 3b6b23c921
14 changed files with 126 additions and 169 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -210,7 +210,7 @@ static expr parse_proof(parser & p, expr const & prop) {
--i; --i;
expr l = locals[i]; expr l = locals[i];
pr = p.save_pos(Fun(l, pr), using_pos); pr = p.save_pos(Fun(l, pr), using_pos);
pr = p.save_pos(pr(l), using_pos); pr = p.save_pos(mk_app(pr, l), using_pos);
} }
return pr; return pr;
} else { } else {
@ -256,7 +256,7 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> con
auto proof_pos = p.pos(); auto proof_pos = p.pos();
proof = parse_proof(p, prop); proof = parse_proof(p, prop);
proof = p.save_pos(Fun(*prev_local, proof), proof_pos); proof = p.save_pos(Fun(*prev_local, proof), proof_pos);
proof = p.save_pos(proof(*prev_local), proof_pos); proof = p.save_pos(mk_app(proof, *prev_local), proof_pos);
} else { } else {
proof = parse_proof(p, prop); proof = parse_proof(p, prop);
} }
@ -327,12 +327,12 @@ static expr parse_obtain(parser & p, unsigned, expr const *, pos_info const & po
expr a = ps[i]; expr a = ps[i];
expr H_aux = mk_local(p.mk_fresh_name(), H_name.append_after(i), mk_expr_placeholder(), mk_contextual_info(false)); expr H_aux = mk_local(p.mk_fresh_name(), H_name.append_after(i), mk_expr_placeholder(), mk_contextual_info(false));
expr H2 = Fun({a, H}, b); expr H2 = Fun({a, H}, b);
b = mk_constant(*g_exists_elim)(H_aux, H2); b = mk_app(mk_constant(*g_exists_elim), H_aux, H2);
H = H_aux; H = H_aux;
} }
expr a = ps[0]; expr a = ps[0];
expr H2 = Fun({a, H}, b); expr H2 = Fun({a, H}, b);
expr r = mk_constant(*g_exists_elim)(H1, H2); expr r = mk_app(mk_constant(*g_exists_elim), H1, H2);
return p.rec_save_pos(r, pos); return p.rec_save_pos(r, pos);
} }

51
src/kernel/expr.h
View file

@ -144,21 +144,6 @@ public:
friend expr mk_macro(macro_definition const & m, unsigned num, expr const * args, tag g); friend expr mk_macro(macro_definition const & m, unsigned num, expr const * args, tag g);
friend bool is_eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; } friend bool is_eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; }
// Overloaded operator() can be used to create applications
expr operator()(expr const & a1, tag g = nulltag) const;
expr operator()(expr const & a1, expr const & a2, tag g = nulltag) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, tag g = nulltag) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4,
tag g = nulltag) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4,
expr const & a5, tag g = nulltag) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4,
expr const & a5, expr const & a6, tag g = nulltag) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4,
expr const & a5, expr const & a6, expr const & a7, tag g = nulltag) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4,
expr const & a5, expr const & a6, expr const & a7, expr const & a8,
tag g = nulltag) const;
}; };
expr copy_tag(expr const & e, expr && new_e); expr copy_tag(expr const & e, expr && new_e);
@ -460,14 +445,14 @@ expr mk_app(unsigned num_args, expr const * args, tag g = nulltag);
inline expr mk_app(std::initializer_list<expr> const & l, tag g = nulltag) { inline expr mk_app(std::initializer_list<expr> const & l, tag g = nulltag) {
return mk_app(l.size(), l.begin(), g); return mk_app(l.size(), l.begin(), g);
} }
template<typename T> expr mk_app(T const & args, tag g = nulltag) { return mk_app(args.size(), args.data(), g); } inline expr mk_app(buffer<expr> const & args, tag g = nulltag) { return mk_app(args.size(), args.data(), g); }
template<typename T> expr mk_app(expr const & f, T const & args, tag g = nulltag) { inline expr mk_app(expr const & f, buffer<expr> const & args, tag g = nulltag) {
return mk_app(f, args.size(), args.data(), g); return mk_app(f, args.size(), args.data(), g);
} }
expr mk_rev_app(expr const & f, unsigned num_args, expr const * args, tag g = nulltag); expr mk_rev_app(expr const & f, unsigned num_args, expr const * args, tag g = nulltag);
expr mk_rev_app(unsigned num_args, expr const * args, tag g = nulltag); expr mk_rev_app(unsigned num_args, expr const * args, tag g = nulltag);
template<typename T> expr mk_rev_app(T const & args, tag g = nulltag) { return mk_rev_app(args.size(), args.data(), g); } inline expr mk_rev_app(buffer<expr> const & args, tag g = nulltag) { return mk_rev_app(args.size(), args.data(), g); }
template<typename T> expr mk_rev_app(expr const & f, T const & args, tag g = nulltag) { inline expr mk_rev_app(expr const & f, buffer<expr> const & args, tag g = nulltag) {
return mk_rev_app(f, args.size(), args.data(), g); return mk_rev_app(f, args.size(), args.data(), g);
} }
expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e,
@ -505,34 +490,6 @@ inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const
tag g = nulltag) { tag g = nulltag) {
return mk_app({e1, e2, e3, e4, e5}, g); return mk_app({e1, e2, e3, e4, e5}, g);
} }
inline expr expr::operator()(expr const & a, tag g) const {
return mk_app({*this, a}, g);
}
inline expr expr::operator()(expr const & a1, expr const & a2, tag g) const {
return mk_app({*this, a1, a2}, g);
}
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, tag g) const {
return mk_app({*this, a1, a2, a3}, g);
}
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, tag g) const {
return mk_app({*this, a1, a2, a3, a4}, g);
}
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4,
expr const & a5, tag g) const {
return mk_app({*this, a1, a2, a3, a4, a5}, g);
}
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5,
expr const & a6, tag g) const {
return mk_app({*this, a1, a2, a3, a4, a5, a6}, g);
}
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5,
expr const & a6, expr const & a7, tag g) const {
return mk_app({*this, a1, a2, a3, a4, a5, a6, a7}, g);
}
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5,
expr const & a6, expr const & a7, expr const & a8, tag g) const {
return mk_app({*this, a1, a2, a3, a4, a5, a6, a7, a8}, g);
}
/** \brief Return application (...((f x_{n-1}) x_{n-2}) ... x_0) */ /** \brief Return application (...((f x_{n-1}) x_{n-2}) ... x_0) */
expr mk_app_vars(expr const & f, unsigned n, tag g = nulltag); expr mk_app_vars(expr const & f, unsigned n, tag g = nulltag);

18
src/tests/kernel/environment.cpp
View file

@ -74,12 +74,12 @@ static void tst1() {
expr c = mk_local("c", Prop); expr c = mk_local("c", Prop);
expr id = Const("id"); expr id = Const("id");
type_checker checker(env3, name_generator("tmp")); type_checker checker(env3, name_generator("tmp"));
lean_assert(checker.check(id(Prop)).first == Prop >> Prop); lean_assert(checker.check(mk_app(id, Prop)).first == Prop >> Prop);
lean_assert(checker.whnf(id(Prop, c)).first == c); lean_assert(checker.whnf(mk_app(id, Prop, c)).first == c);
lean_assert(checker.whnf(id(Prop, id(Prop, id(Prop, c)))).first == c); lean_assert(checker.whnf(mk_app(id, Prop, mk_app(id, Prop, mk_app(id, Prop, c)))).first == c);
type_checker checker2(env2, name_generator("tmp")); type_checker checker2(env2, name_generator("tmp"));
lean_assert(checker2.whnf(id(Prop, id(Prop, id(Prop, c)))).first == id(Prop, id(Prop, id(Prop, c)))); lean_assert(checker2.whnf(mk_app(id, Prop, mk_app(id, Prop, mk_app(id, Prop, c)))).first == mk_app(id, Prop, mk_app(id, Prop, mk_app(id, Prop, c))));
} }
static void tst2() { static void tst2() {
@ -92,7 +92,7 @@ static void tst2() {
for (unsigned i = 1; i <= 100; i++) { for (unsigned i = 1; i <= 100; i++) {
expr prev = Const(name(base, i-1)); expr prev = Const(name(base, i-1));
env = add_decl(env, mk_definition(env, name(base, i), level_param_names(), Prop >> (Prop >> Prop), env = add_decl(env, mk_definition(env, name(base, i), level_param_names(), Prop >> (Prop >> Prop),
Fun({x, y}, prev(prev(x, y), prev(y, x))))); Fun({x, y}, mk_app(prev, mk_app(prev, x, y), mk_app(prev, y, x)))));
} }
expr Type = mk_Type(); expr Type = mk_Type();
expr A = Local("A", Type); expr A = Local("A", Type);
@ -108,10 +108,10 @@ static void tst2() {
expr c1 = mk_local("c1", Prop); expr c1 = mk_local("c1", Prop);
expr c2 = mk_local("c2", Prop); expr c2 = mk_local("c2", Prop);
expr id = Const("id"); expr id = Const("id");
std::cout << checker.whnf(f3(c1, c2)).first << "\n"; std::cout << checker.whnf(mk_app(f3, c1, c2)).first << "\n";
lean_assert_eq(env.find(name(base, 98))->get_weight(), 98); lean_assert_eq(env.find(name(base, 98))->get_weight(), 98);
lean_assert(checker.is_def_eq(f98(c1, c2), f97(f97(c1, c2), f97(c2, c1))).first); lean_assert(checker.is_def_eq(mk_app(f98, c1, c2), mk_app(f97, mk_app(f97, c1, c2), mk_app(f97, c2, c1))).first);
lean_assert(checker.is_def_eq(f98(c1, id(Prop, id(Prop, c2))), f97(f97(c1, id(Prop, c2)), f97(c2, c1))).first); lean_assert(checker.is_def_eq(mk_app(f98, c1, mk_app(id, Prop, mk_app(id, Prop, c2))), mk_app(f97, mk_app(f97, c1, mk_app(id, Prop, c2)), mk_app(f97, c2, c1))).first);
name_set s; name_set s;
s.insert(name(base, 96)); s.insert(name(base, 96));
} }
@ -152,7 +152,7 @@ static void tst3() {
expr a = Const("a"); expr a = Const("a");
expr b = Const("b"); expr b = Const("b");
type_checker checker(env, name_generator("tmp")); type_checker checker(env, name_generator("tmp"));
lean_assert_eq(checker.whnf(proj1(proj1(mk(id(A, mk(a, b)), b)))).first, a); lean_assert_eq(checker.whnf(mk_app(proj1, mk_app(proj1, mk_app(mk, mk_app(id, A, mk_app(mk, a, b)), b)))).first, a);
} }
class dummy_ext : public environment_extension {}; class dummy_ext : public environment_extension {};

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

@ -44,22 +44,22 @@ static void tst1() {
a = Const("a"); a = Const("a");
expr f; expr f;
f = Var(0); f = Var(0);
expr fa = f(a); expr fa = mk_app(f, a);
expr Type = mk_Type(); expr Type = mk_Type();
expr ty = Type; expr ty = Type;
std::cout << fa << "\n"; std::cout << fa << "\n";
std::cout << fa(a) << "\n"; std::cout << mk_app(fa, a) << "\n";
lean_assert(is_eqp(app_fn(fa), f)); lean_assert(is_eqp(app_fn(fa), f));
lean_assert(is_eqp(app_arg(fa), a)); lean_assert(is_eqp(app_arg(fa), a));
{ {
scoped_expr_caching set(false); scoped_expr_caching set(false);
lean_assert(!is_eqp(fa, f(a))); lean_assert(!is_eqp(fa, mk_app(f, a)));
} }
lean_assert(fa(a) == f(a, a)); lean_assert(mk_app(fa, a) == mk_app(f, a, a));
std::cout << fa(fa, fa) << "\n"; std::cout << mk_app(fa, fa, fa) << "\n";
std::cout << mk_lambda("x", ty, Var(0)) << "\n"; std::cout << mk_lambda("x", ty, Var(0)) << "\n";
lean_assert(f(a)(a) == f(a, a)); lean_assert(mk_app(mk_app(f, a), a) == mk_app(f, a, a));
lean_assert(f(a(a)) != f(a, a)); lean_assert(mk_app(f, mk_app(a, a)) != mk_app(f, a, a));
lean_assert(mk_lambda("x", ty, Var(0)) == mk_lambda("y", ty, Var(0))); lean_assert(mk_lambda("x", ty, Var(0)) == mk_lambda("y", ty, Var(0)));
std::cout << mk_pi("x", ty, Var(0)) << "\n"; std::cout << mk_pi("x", ty, Var(0)) << "\n";
} }
@ -69,7 +69,7 @@ static expr mk_dag(unsigned depth, bool _closed = false) {
expr a = _closed ? Const("a") : Var(0); expr a = _closed ? Const("a") : Var(0);
while (depth > 0) { while (depth > 0) {
depth--; depth--;
a = f(a, a); a = mk_app(f, a, a);
} }
return a; return a;
} }
@ -86,7 +86,7 @@ static expr mk_big(expr f, unsigned depth, unsigned val) {
if (depth == 1) if (depth == 1)
return Const(name(name("foo"), val)); return Const(name(name("foo"), val));
else else
return f(mk_big(f, depth - 1, val << 1), mk_big(f, depth - 1, (val << 1) + 1)); return mk_app(f, mk_big(f, depth - 1, val << 1), mk_big(f, depth - 1, (val << 1) + 1));
} }
static void tst3() { static void tst3() {
@ -101,7 +101,7 @@ static void tst4() {
expr f = Const("f"); expr f = Const("f");
expr a = Var(0); expr a = Var(0);
for (unsigned i = 0; i < 10000; i++) { for (unsigned i = 0; i < 10000; i++) {
a = f(a); a = mk_app(f, a);
} }
} }
@ -109,7 +109,7 @@ static expr mk_redundant_dag(expr f, unsigned depth) {
if (depth == 0) if (depth == 0)
return Var(0); return Var(0);
else else
return f(mk_redundant_dag(f, depth - 1), mk_redundant_dag(f, depth - 1)); return mk_app(f, mk_redundant_dag(f, depth - 1), mk_redundant_dag(f, depth - 1));
} }
static unsigned count_core(expr const & a, expr_set & s) { static unsigned count_core(expr const & a, expr_set & s) {
@ -170,10 +170,10 @@ static void tst7() {
scoped_expr_caching set(false); scoped_expr_caching set(false);
expr f = Const("f"); expr f = Const("f");
expr v = Var(0); expr v = Var(0);
expr a1 = max_sharing(f(v, v)); expr a1 = max_sharing(mk_app(f, v, v));
expr a2 = max_sharing(f(v, v)); expr a2 = max_sharing(mk_app(f, v, v));
lean_assert(!is_eqp(a1, a2)); lean_assert(!is_eqp(a1, a2));
expr b = max_sharing(f(a1, a2)); expr b = max_sharing(mk_app(f, a1, a2));
lean_assert(is_eqp(app_arg(app_fn(b)), app_arg(b))); lean_assert(is_eqp(app_arg(app_fn(b)), app_arg(b)));
} }
@ -188,16 +188,16 @@ static void tst8() {
lean_assert(closed(a)); lean_assert(closed(a));
lean_assert(!closed(x)); lean_assert(!closed(x));
lean_assert(closed(f)); lean_assert(closed(f));
lean_assert(!closed(f(x))); lean_assert(!closed(mk_app(f, x)));
lean_assert(closed(mk_lambda("x", p, x))); lean_assert(closed(mk_lambda("x", p, x)));
lean_assert(!closed(mk_lambda("x", x, x))); lean_assert(!closed(mk_lambda("x", x, x)));
lean_assert(!closed(mk_lambda("x", p, y))); lean_assert(!closed(mk_lambda("x", p, y)));
lean_assert(closed(f(f(f(a))))); lean_assert(closed(mk_app(f, mk_app(f, mk_app(f, a)))));
lean_assert(closed(mk_lambda("x", p, f(f(f(a)))))); lean_assert(closed(mk_lambda("x", p, mk_app(f, mk_app(f, mk_app(f, a))))));
lean_assert(closed(mk_pi("x", p, x))); lean_assert(closed(mk_pi("x", p, x)));
lean_assert(!closed(mk_pi("x", x, x))); lean_assert(!closed(mk_pi("x", x, x)));
lean_assert(!closed(mk_pi("x", p, y))); lean_assert(!closed(mk_pi("x", p, y)));
lean_assert(closed(mk_pi("x", p, f(f(f(a)))))); lean_assert(closed(mk_pi("x", p, mk_app(f, mk_app(f, mk_app(f, a))))));
lean_assert(closed(mk_lambda("y", p, mk_lambda("x", p, y)))); lean_assert(closed(mk_lambda("y", p, mk_lambda("x", p, y))));
lean_assert(closed(mk_lambda("y", p, mk_app({mk_lambda("x", p, y), Var(0)})))); lean_assert(closed(mk_lambda("y", p, mk_app({mk_lambda("x", p, y), Var(0)}))));
expr r = mk_lambda("y", p, mk_app({mk_lambda("x", p, y), Var(0)})); expr r = mk_lambda("y", p, mk_app({mk_lambda("x", p, y), Var(0)}));
@ -243,25 +243,25 @@ static void tst11() {
expr y = Var(1); expr y = Var(1);
expr Type = mk_Type(); expr Type = mk_Type();
expr t = Type; expr t = Type;
std::cout << instantiate(mk_lambda("x", t, f(f(y, b), f(x, y))), f(a)) << "\n"; std::cout << instantiate(mk_lambda("x", t, mk_app(f, mk_app(f, y, b), mk_app(f, x, y))), mk_app(f, a)) << "\n";
lean_assert(instantiate(mk_lambda("x", t, f(f(y, b), f(x, y))), f(a)) == lean_assert(instantiate(mk_lambda("x", t, mk_app(f, mk_app(f, y, b), mk_app(f, x, y))), mk_app(f, a)) ==
mk_lambda("x", t, f(f(f(a), b), f(x, f(a))))); mk_lambda("x", t, mk_app(f, mk_app(f, mk_app(f, a), b), mk_app(f, x, mk_app(f, a)))));
std::cout << abstract(mk_lambda("x", t, f(a, mk_lambda("y", t, f(b, a)))), Const("a")) << "\n"; std::cout << abstract(mk_lambda("x", t, mk_app(f, a, mk_lambda("y", t, mk_app(f, b, a)))), Const("a")) << "\n";
lean_assert(abstract(mk_lambda("x", t, f(a, mk_lambda("y", t, f(b, a)))), Const("a")) == lean_assert(abstract(mk_lambda("x", t, mk_app(f, a, mk_lambda("y", t, mk_app(f, b, a)))), Const("a")) ==
mk_lambda("x", t, f(Var(1), mk_lambda("y", t, f(b, Var(2)))))); mk_lambda("x", t, mk_app(f, Var(1), mk_lambda("y", t, mk_app(f, b, Var(2))))));
lean_assert(substitute(f(f(f(a))), f(a), b) == f(f(b))); lean_assert(substitute(mk_app(f, mk_app(f, mk_app(f, a))), mk_app(f, a), b) == mk_app(f, mk_app(f, b)));
} }
static void tst12() { static void tst12() {
scoped_expr_caching set(false); scoped_expr_caching set(false);
expr f = Const("f"); expr f = Const("f");
expr v = Var(0); expr v = Var(0);
expr a1 = max_sharing(f(v, v)); expr a1 = max_sharing(mk_app(f, v, v));
expr a2 = max_sharing(f(v, v)); expr a2 = max_sharing(mk_app(f, v, v));
lean_assert(!is_eqp(a1, a2)); lean_assert(!is_eqp(a1, a2));
lean_assert(a1 == a2); lean_assert(a1 == a2);
max_sharing_fn M; max_sharing_fn M;
lean_assert(is_eqp(M(f(v, v)), M(f(v, v)))); lean_assert(is_eqp(M(mk_app(f, v, v)), M(mk_app(f, v, v))));
lean_assert(is_eqp(M(a1), M(a2))); lean_assert(is_eqp(M(a1), M(a2)));
} }
@ -292,9 +292,9 @@ static void tst15() {
expr m = mk_metavar("m", Prop); expr m = mk_metavar("m", Prop);
check_serializer(m); check_serializer(m);
lean_assert(has_metavar(m)); lean_assert(has_metavar(m));
lean_assert(has_metavar(f(m))); lean_assert(has_metavar(mk_app(f, m)));
lean_assert(!has_metavar(f(a))); lean_assert(!has_metavar(mk_app(f, a)));
lean_assert(!has_metavar(f(x))); lean_assert(!has_metavar(mk_app(f, x)));
lean_assert(!has_metavar(Pi(a, a))); lean_assert(!has_metavar(Pi(a, a)));
lean_assert(!has_metavar(Type)); lean_assert(!has_metavar(Type));
lean_assert(!has_metavar(Fun(a, a))); lean_assert(!has_metavar(Fun(a, a)));
@ -303,9 +303,9 @@ static void tst15() {
lean_assert(has_metavar(Pi(a1, a1))); lean_assert(has_metavar(Pi(a1, a1)));
lean_assert(has_metavar(Fun(a, m))); lean_assert(has_metavar(Fun(a, m)));
lean_assert(has_metavar(Fun(a1, a))); lean_assert(has_metavar(Fun(a1, a)));
lean_assert(has_metavar(f(a, a, m))); lean_assert(has_metavar(mk_app(f, a, a, m)));
lean_assert(has_metavar(f(a, m, a, a))); lean_assert(has_metavar(mk_app(f, a, m, a, a)));
lean_assert(!has_metavar(f(a, a, a, a))); lean_assert(!has_metavar(mk_app(f, a, a, a, a)));
} }
static void check_copy(expr const & e) { static void check_copy(expr const & e) {
@ -319,7 +319,7 @@ static void check_copy(expr const & e) {
static void tst16() { static void tst16() {
expr f = Const("f"); expr f = Const("f");
expr a = Const("a"); expr a = Const("a");
check_copy(f(a)); check_copy(mk_app(f, a));
expr Prop = mk_Prop(); expr Prop = mk_Prop();
check_copy(mk_metavar("M", Prop)); check_copy(mk_metavar("M", Prop));
check_copy(mk_lambda("x", a, Var(0))); check_copy(mk_lambda("x", a, Var(0)));
@ -356,10 +356,10 @@ static void tst18() {
check_serializer(l); check_serializer(l);
lean_assert(!has_local(m)); lean_assert(!has_local(m));
lean_assert(has_local(l)); lean_assert(has_local(l));
lean_assert(!has_local(f(m))); lean_assert(!has_local(mk_app(f, m)));
lean_assert(has_local(f(l))); lean_assert(has_local(mk_app(f, l)));
lean_assert(!has_local(f(a0))); lean_assert(!has_local(mk_app(f, a0)));
lean_assert(!has_local(f(x))); lean_assert(!has_local(mk_app(f, x)));
lean_assert(!has_local(Pi(a, a))); lean_assert(!has_local(Pi(a, a)));
lean_assert(!has_local(Pi(a1, a1))); lean_assert(!has_local(Pi(a1, a1)));
lean_assert(!has_local(Type)); lean_assert(!has_local(Type));
@ -369,9 +369,9 @@ static void tst18() {
lean_assert(has_local(Pi(a2, a2))); lean_assert(has_local(Pi(a2, a2)));
lean_assert(has_local(Fun(a, l))); lean_assert(has_local(Fun(a, l)));
lean_assert(has_local(Fun(a2, a2))); lean_assert(has_local(Fun(a2, a2)));
lean_assert(has_local(f(a, a, l))); lean_assert(has_local(mk_app(f, a, a, l)));
lean_assert(has_local(f(a, l, a, a))); lean_assert(has_local(mk_app(f, a, l, a, a)));
lean_assert(!has_local(f(a0, a0, a0, a0))); lean_assert(!has_local(mk_app(f, a0, a0, a0, a0)));
} }
int main() { int main() {

28
src/tests/kernel/free_vars.cpp
View file

@ -19,16 +19,16 @@ static void tst1() {
expr x = Var(0); expr x = Var(0);
expr y = Var(1); expr y = Var(1);
expr t = Const("t"); expr t = Const("t");
expr F = mk_lambda("_", t, f(x)); expr F = mk_lambda("_", t, mk_app(f, x));
lean_assert(has_free_var(mk_lambda("_", t, f(Var(1))), 0)); lean_assert(has_free_var(mk_lambda("_", t, mk_app(f, Var(1))), 0));
lean_assert(!has_free_var(mk_lambda("_", t, f(Var(0))), 1)); lean_assert(!has_free_var(mk_lambda("_", t, mk_app(f, Var(0))), 1));
lean_assert(!has_free_var(mk_pi("_", t, mk_lambda("_", t, f(Var(1)))), 0)); lean_assert(!has_free_var(mk_pi("_", t, mk_lambda("_", t, mk_app(f, Var(1)))), 0));
lean_assert(has_free_var(f(Var(0)), 0)); lean_assert(has_free_var(mk_app(f, Var(0)), 0));
lean_assert(has_free_var(f(Var(1)), 1)); lean_assert(has_free_var(mk_app(f, Var(1)), 1));
lean_assert(!has_free_var(f(Var(1)), 0)); lean_assert(!has_free_var(mk_app(f, Var(1)), 0));
lean_assert_eq(lower_free_vars(f(Var(1)), 1), f(Var(0))); lean_assert_eq(lower_free_vars(mk_app(f, Var(1)), 1), mk_app(f, Var(0)));
lean_assert_eq(lower_free_vars(mk_lambda("_", t, f(Var(2))), 1), mk_lambda("_", t, f(Var(1)))); lean_assert_eq(lower_free_vars(mk_lambda("_", t, mk_app(f, Var(2))), 1), mk_lambda("_", t, mk_app(f, Var(1))));
lean_assert_eq(lower_free_vars(mk_lambda("_", t, f(Var(0))), 1), mk_lambda("_", t, f(Var(0)))); lean_assert_eq(lower_free_vars(mk_lambda("_", t, mk_app(f, Var(0))), 1), mk_lambda("_", t, mk_app(f, Var(0))));
} }
static void tst2() { static void tst2() {
@ -46,7 +46,7 @@ static void tst3() {
unsigned m = 10; unsigned m = 10;
expr f = Const("f"); expr f = Const("f");
expr a = Const("a"); expr a = Const("a");
expr r = f(a, Var(m)); expr r = mk_app(f, a, Var(m));
expr b = Const("Prop"); expr b = Const("Prop");
for (unsigned i = 0; i < n; i++) for (unsigned i = 0; i < n; i++)
r = mk_lambda(name(), b, r); r = mk_lambda(name(), b, r);
@ -63,11 +63,11 @@ static void tst4() {
expr B = mk_Prop(); expr B = mk_Prop();
expr x = Local("x", B); expr x = Local("x", B);
expr y = Local("y", B); expr y = Local("y", B);
expr t = f(Fun({x, y}, f(x, y))(f(Var(1), Var(2))), x); expr t = mk_app(f, mk_app(Fun({x, y}, mk_app(f, x, y)), mk_app(f, Var(1), Var(2))), x);
lean_assert_eq(lift_free_vars(t, 1, 2), lean_assert_eq(lift_free_vars(t, 1, 2),
f(Fun(x, Fun(y, f(x, y)))(f(Var(3), Var(4))), x)); mk_app(f, mk_app(Fun(x, Fun(y, mk_app(f, x, y))), mk_app(f, Var(3), Var(4))), x));
lean_assert_eq(lift_free_vars(t, 0, 3), lean_assert_eq(lift_free_vars(t, 0, 3),
f(Fun(x, Fun(y, f(x, y)))(f(Var(4), Var(5))), x)); mk_app(f, mk_app(Fun(x, Fun(y, mk_app(f, x, y))), mk_app(f, Var(4), Var(5))), x));
lean_assert_eq(lift_free_vars(t, 3, 2), t); lean_assert_eq(lift_free_vars(t, 3, 2), t);
} }

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

@ -23,16 +23,16 @@ static void tst1() {
expr b = Const("b"); expr b = Const("b");
expr c = Const("c"); expr c = Const("c");
expr d = Const("d"); expr d = Const("d");
expr F1 = Fun(x, x)(f, a); expr F1 = mk_app(Fun(x, x), f, a);
lean_assert(is_head_beta(F1)); lean_assert(is_head_beta(F1));
lean_assert_eq(head_beta_reduce(F1), f(a)); lean_assert_eq(head_beta_reduce(F1), mk_app(f, a));
expr F2 = Fun({h, y}, h(y))(f, a, b, c); expr F2 = mk_app(Fun({h, y}, mk_app(h, y)), f, a, b, c);
lean_assert(is_head_beta(F2)); lean_assert(is_head_beta(F2));
lean_assert_eq(head_beta_reduce(F2), f(a, b, c)); lean_assert_eq(head_beta_reduce(F2), mk_app(f, a, b, c));
expr F3 = Fun(x, f(Fun(y, y)(x), x))(a); expr F3 = mk_app(Fun(x, mk_app(f, mk_app(Fun(y, y), x), x)), a);
lean_assert(is_head_beta(F3)); lean_assert(is_head_beta(F3));
lean_assert(head_beta_reduce(F3) == f(Fun(y, y)(a), a)); lean_assert(head_beta_reduce(F3) == mk_app(f, mk_app(Fun(y, y), a), a));
lean_assert(beta_reduce(F3) == f(a, a)); lean_assert(beta_reduce(F3) == mk_app(f, a, a));
} }
int main() { int main() {

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

@ -24,7 +24,7 @@ static void tst1() {
expr y = Local("y", N); expr y = Local("y", N);
expr f = Const("f"); expr f = Const("f");
expr F1, F2; expr F1, F2;
F1 = f(Fun(x, f(x, x)), Fun(y, f(y, y))); F1 = mk_app(f, Fun(x, mk_app(f, x, x)), Fun(y, mk_app(f, y, y)));
lean_assert(!is_eqp(app_arg(app_fn(F1)), app_arg(F1))); lean_assert(!is_eqp(app_arg(app_fn(F1)), app_arg(F1)));
F2 = max_fn(F1); F2 = max_fn(F1);
std::cout << F2 << "\n"; std::cout << F2 << "\n";
@ -38,8 +38,8 @@ static void tst2() {
expr x = Const("x"); expr x = Const("x");
expr f = Const("f"); expr f = Const("f");
expr g = Const("g"); expr g = Const("g");
expr t1 = max_fn2(max_fn1(f(g(x)))); expr t1 = max_fn2(max_fn1(mk_app(f, mk_app(g, x))));
expr t2 = max_fn2(f(t1, g(x))); expr t2 = max_fn2(mk_app(f, t1, mk_app(g, x)));
expr arg1 = app_arg(app_arg(app_fn(t2))); expr arg1 = app_arg(app_arg(app_fn(t2)));
expr arg2 = app_arg(t2); expr arg2 = app_arg(t2);
lean_assert(is_eqp(arg1, arg2)); lean_assert(is_eqp(arg1, arg2));
@ -54,11 +54,11 @@ static void tst3() {
expr f = Const("f"); expr f = Const("f");
expr new_a1 = max_fn(a1); expr new_a1 = max_fn(a1);
lean_assert(is_eqp(new_a1, a1)); lean_assert(is_eqp(new_a1, a1));
expr t1 = max_fn(f(a2)); expr t1 = max_fn(mk_app(f, a2));
lean_assert(is_eqp(app_arg(t1), a1)); lean_assert(is_eqp(app_arg(t1), a1));
expr t2 = max_fn(f(a2)); expr t2 = max_fn(mk_app(f, a2));
lean_assert(is_eqp(t1, t2)); lean_assert(is_eqp(t1, t2));
expr t3 = max_fn(f(a3)); expr t3 = max_fn(mk_app(f, a3));
lean_assert(is_eqp(t1, t3)); lean_assert(is_eqp(t1, t3));
} }

40
src/tests/kernel/metavar.cpp
View file

@ -81,11 +81,11 @@ static void tst1() {
lean_assert(m1 != m2); lean_assert(m1 != m2);
expr f = Const("f"); expr f = Const("f");
expr a = Const("a"); expr a = Const("a");
subst.assign(m1, f(a)); subst.assign(m1, mk_app(f, a));
lean_assert(subst.is_assigned(m1)); lean_assert(subst.is_assigned(m1));
lean_assert(!subst.is_assigned(m2)); lean_assert(!subst.is_assigned(m2));
lean_assert(*subst.get_expr(m1) == f(a)); lean_assert(*subst.get_expr(m1) == mk_app(f, a));
lean_assert(subst.instantiate_metavars(f(m1)).first == f(f(a))); lean_assert(subst.instantiate_metavars(mk_app(f, m1)).first == mk_app(f, mk_app(f, a)));
std::cout << subst << "\n"; std::cout << subst << "\n";
} }
@ -98,19 +98,19 @@ static void tst2() {
expr f = Const("f"); expr f = Const("f");
expr g = Const("g"); expr g = Const("g");
expr a = Const("a"); expr a = Const("a");
s.assign(m1, f(m2), mk_assumption_justification(1)); s.assign(m1, mk_app(f, m2), mk_assumption_justification(1));
s.assign(m2, g(a), mk_assumption_justification(2)); s.assign(m2, mk_app(g, a), mk_assumption_justification(2));
lean_assert(check_assumptions(s.get_assignment(m1)->second, {1})); lean_assert(check_assumptions(s.get_assignment(m1)->second, {1}));
lean_assert(s.occurs(m1, f(m1))); lean_assert(s.occurs(m1, mk_app(f, m1)));
lean_assert(s.occurs(m2, f(m1))); lean_assert(s.occurs(m2, mk_app(f, m1)));
lean_assert(!s.occurs(m1, f(m2))); lean_assert(!s.occurs(m1, mk_app(f, m2)));
lean_assert(!s.occurs(m1, f(a))); lean_assert(!s.occurs(m1, mk_app(f, a)));
lean_assert(!s.occurs(m3, f(m1))); lean_assert(!s.occurs(m3, mk_app(f, m1)));
std::cout << s << "\n"; std::cout << s << "\n";
auto p1 = s.instantiate_metavars(g(m1)); auto p1 = s.instantiate_metavars(mk_app(g, m1));
check_assumptions(p1.second, {1, 2}); check_assumptions(p1.second, {1, 2});
lean_assert(check_assumptions(s.get_assignment(m1)->second, {1, 2})); lean_assert(check_assumptions(s.get_assignment(m1)->second, {1, 2}));
lean_assert(p1.first == g(f(g(a)))); lean_assert(p1.first == mk_app(g, mk_app(f, mk_app(g, a))));
} }
static void tst3() { static void tst3() {
@ -123,11 +123,11 @@ static void tst3() {
expr b = Const("b"); expr b = Const("b");
expr x = Local("x", Prop); expr x = Local("x", Prop);
expr y = Local("y", Prop); expr y = Local("y", Prop);
s.assign(m1, Fun({x, y}, f(y, x))); s.assign(m1, Fun({x, y}, mk_app(f, y, x)));
lean_assert_eq(s.instantiate_metavars(m1(a, b, g(a))).first, f(b, a, g(a))); lean_assert_eq(s.instantiate_metavars(mk_app(m1, a, b, mk_app(g, a))).first, mk_app(f, b, a, mk_app(g, a)));
lean_assert_eq(s.instantiate_metavars(m1(a)).first, Fun(y, f(y, a))); lean_assert_eq(s.instantiate_metavars(mk_app(m1, a)).first, Fun(y, mk_app(f, y, a)));
lean_assert_eq(s.instantiate_metavars(m1(a, b)).first, f(b, a)); lean_assert_eq(s.instantiate_metavars(mk_app(m1, a, b)).first, mk_app(f, b, a));
std::cout << s.instantiate_metavars(m1(a, b, g(a))).first << "\n"; std::cout << s.instantiate_metavars(mk_app(m1, a, b, mk_app(g, a))).first << "\n";
} }
static void tst4() { static void tst4() {
@ -143,13 +143,13 @@ static void tst4() {
expr a = Const("a"); expr a = Const("a");
expr T1 = mk_sort(l1); expr T1 = mk_sort(l1);
expr T2 = mk_sort(u); expr T2 = mk_sort(u);
expr t = f(T1, T2, m1, m2); expr t = mk_app(f, T1, T2, m1, m2);
lean_assert(s.instantiate_metavars(t).first == t); lean_assert(s.instantiate_metavars(t).first == t);
s.assign(m1, a, justification()); s.assign(m1, a, justification());
s.assign(m2, m3, justification()); s.assign(m2, m3, justification());
lean_assert(s.instantiate_metavars(t).first == f(T1, T2, a, m3)); lean_assert(s.instantiate_metavars(t).first == mk_app(f, T1, T2, a, m3));
s.assign(l1, level(), justification()); s.assign(l1, level(), justification());
lean_assert(s.instantiate_metavars(t).first == f(Prop, T2, a, m3)); lean_assert(s.instantiate_metavars(t).first == mk_app(f, Prop, T2, a, m3));
} }
int main() { int main() {

2
src/tests/kernel/replace.cpp
View file

@ -22,7 +22,7 @@ expr mk_big(expr f, unsigned depth, unsigned val) {
if (depth == 1) if (depth == 1)
return mk_constant(name(name("foo"), val)); return mk_constant(name(name("foo"), val));
else else
return f(mk_big(f, depth - 1, val << 1), mk_big(f, depth - 1, (val << 1) + 1)); return mk_app(f, mk_big(f, depth - 1, val << 1), mk_big(f, depth - 1, (val << 1) + 1));
} }
static void tst1() { static void tst1() {

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

@ -22,7 +22,7 @@ static void tst1() {
expr t = Type; expr t = Type;
expr z = Const("z"); expr z = Const("z");
expr m = mk_metavar("a", Type); expr m = mk_metavar("a", Type);
expr F = 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, mk_app(f, mk_app(f, mk_app(f, x, a), Const("10")), mk_app(f, x, m))));
expr G = deep_copy(F); expr G = deep_copy(F);
lean_assert(F == G); lean_assert(F == G);
lean_assert(!is_eqp(F, G)); lean_assert(!is_eqp(F, G));

18
src/tests/library/expr_lt.cpp
View file

@ -20,15 +20,15 @@ static void tst1() {
lt(Const("a"), Const("b"), true); lt(Const("a"), Const("b"), true);
lt(Const("a"), Const("a"), false); lt(Const("a"), Const("a"), false);
lt(Var(1), Const("a"), true); lt(Var(1), Const("a"), true);
lt(Const("f")(Var(0)), Const("f")(Var(0), Const("a")), true); lt(mk_app(Const("f"), Var(0)), mk_app(Const("f"), Var(0), Const("a")), true);
lt(Const("f")(Var(0), Const("a"), Const("b")), Const("f")(Var(0), Const("a")), false); lt(mk_app(Const("f"), Var(0), Const("a"), Const("b")), mk_app(Const("f"), Var(0), Const("a")), false);
lt(Const("f")(Var(0), Const("a")), Const("g")(Var(0), Const("a")), true); lt(mk_app(Const("f"), Var(0), Const("a")), mk_app(Const("g"), Var(0), Const("a")), true);
lt(Const("f")(Var(0), Const("a")), Const("f")(Var(1), Const("a")), true); lt(mk_app(Const("f"), Var(0), Const("a")), mk_app(Const("f"), Var(1), Const("a")), true);
lt(Const("f")(Var(0), Const("a")), Const("f")(Var(0), Const("b")), true); lt(mk_app(Const("f"), Var(0), Const("a")), mk_app(Const("f"), Var(0), Const("b")), true);
lt(Const("f")(Var(0), Const("a")), Const("f")(Var(0), Const("a")), false); lt(mk_app(Const("f"), Var(0), Const("a")), mk_app(Const("f"), Var(0), Const("a")), false);
lt(Const("g")(Var(0), Const("a")), Const("f")(Var(0), Const("a")), false); lt(mk_app(Const("g"), Var(0), Const("a")), mk_app(Const("f"), Var(0), Const("a")), false);
lt(Const("f")(Var(1), Const("a")), Const("f")(Var(0), Const("a")), false); lt(mk_app(Const("f"), Var(1), Const("a")), mk_app(Const("f"), Var(0), Const("a")), false);
lt(Const("f")(Var(0), Const("b")), Const("f")(Var(0), Const("a")), false); lt(mk_app(Const("f"), Var(0), Const("b")), mk_app(Const("f"), Var(0), Const("a")), false);
} }
int main() { int main() {

8
src/tests/library/head_map.cpp
View file

@ -21,7 +21,7 @@ static void tst1() {
expr Prop = mk_Prop(); expr Prop = mk_Prop();
expr x = Local("x", Prop); expr x = Local("x", Prop);
expr l1 = Fun(x, x); expr l1 = Fun(x, x);
expr l2 = Fun(x, f(x)); expr l2 = Fun(x, mk_app(f, x));
lean_assert(l1 != l2); lean_assert(l1 != l2);
lean_assert(map.empty()); lean_assert(map.empty());
map.insert(a, a); map.insert(a, a);
@ -52,9 +52,9 @@ static void tst1() {
map.erase(a); map.erase(a);
lean_assert(size_fn(map) == 0); lean_assert(size_fn(map) == 0);
lean_assert(map.empty()); lean_assert(map.empty());
map.insert(f(a), f(a)); map.insert(mk_app(f, a), mk_app(f, a));
map.insert(f(b), f(b)); map.insert(mk_app(f, b), mk_app(f, b));
lean_assert(length(*map.find(f(a))) == 2); lean_assert(length(*map.find(mk_app(f, a))) == 2);
} }
int main() { int main() {

6
src/tests/library/occurs.cpp
View file

@ -22,10 +22,10 @@ static void tst1() {
expr a1 = Local("a", T); expr a1 = Local("a", T);
lean_assert(occurs(f, f)); lean_assert(occurs(f, f));
lean_assert(!occurs(a, f)); lean_assert(!occurs(a, f));
lean_assert(occurs(a, f(a))); lean_assert(occurs(a, mk_app(f, a)));
lean_assert(occurs("a", f(a))); lean_assert(occurs("a", mk_app(f, a)));
lean_assert(!occurs("b", f)); lean_assert(!occurs("b", f));
lean_assert(!occurs(a, Fun(a1, f(a1)))); lean_assert(!occurs(a, Fun(a1, mk_app(f, a1))));
} }
int main() { int main() {

4
src/tests/library/unifier.cpp
View file

@ -21,8 +21,8 @@ static void tst1() {
expr a = Local("a", A); expr a = Local("a", A);
expr b = Local("b", A); expr b = Local("b", A);
expr m = mk_metavar("m", A); expr m = mk_metavar("m", A);
expr t1 = f(m, m); expr t1 = mk_app(f, m, m);
expr t2 = f(a, b); expr t2 = mk_app(f, a, b);
auto r = unify(env, t1, t2, ngen, false); auto r = unify(env, t1, t2, ngen, false);
lean_assert(!r.pull()); lean_assert(!r.pull());
} }