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

Change name convention for creating Lean expressions

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-06 11:27:14 -07:00
parent 33d2dd2d8b
commit 84f4a32c0e
21 changed files with 580 additions and 514 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/kernel/abstract.cpp
View file

@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <algorithm>
#include "abstract.h"
#include "free_vars.h"
#include "replace.h"
@ -17,7 +18,7 @@ expr abstract(expr const & e, unsigned n, expr const * s) {
while (i > 0) {
--i;
if (s[i] == e)
return var(offset + n - i - 1);
return mk_var(offset + n - i - 1);
}
return e;
};
@ -32,11 +33,31 @@ expr abstract_p(expr const & e, unsigned n, expr const * s) {
while (i > 0) {
--i;
if (is_eqp(s[i], e))
return var(offset + n - i - 1);
return mk_var(offset + n - i - 1);
}
return e;
};
return replace_fn<decltype(f)>(f)(e);
}
expr Fun(std::initializer_list<std::pair<expr const &, expr const &>> const & l, expr const & b) {
expr r = b;
auto it = l.end();
while (it != l.begin()) {
--it;
auto const & p = *it;
r = Fun(p.first, p.second, r);
}
return r;
}
expr Pi(std::initializer_list<std::pair<expr const &, expr const &>> const & l, expr const & b) {
expr r = b;
auto it = l.end();
while (it != l.begin()) {
--it;
auto const & p = *it;
r = Pi(p.first, p.second, r);
}
return r;
}
}

17
src/kernel/abstract.h
View file

@ -31,13 +31,18 @@ inline expr abstract_p(expr const & e, expr const & s) { return abstract_p(e, 1,
/**
\brief Create a lambda expression (lambda (x : t) b), the term b is abstracted using abstract(b, constant(x)).
*/
inline expr fun(name const & n, expr const & t, expr const & b) { return lambda(n, t, abstract(b, constant(n))); }
inline expr fun(char const * n, expr const & t, expr const & b) { return fun(name(n), t, b); }
inline expr fun(expr const & n, expr const & t, expr const & b) { return lambda(const_name(n), t, abstract(b, n)); }
inline expr Fun(name const & n, expr const & t, expr const & b) { return mk_lambda(n, t, abstract(b, mk_constant(n))); }
inline expr Fun(char const * n, expr const & t, expr const & b) { return Fun(name(n), t, b); }
inline expr Fun(expr const & n, expr const & t, expr const & b) { return mk_lambda(const_name(n), t, abstract(b, n)); }
inline expr Fun(std::pair<expr const &, expr const &> const & p, expr const & b) { return Fun(p.first, p.second, b); }
expr Fun(std::initializer_list<std::pair<expr const &, expr const &>> const & l, expr const & b);
/**
\brief Create a Pi expression (pi (x : t) b), the term b is abstracted using abstract(b, constant(x)).
*/
inline expr Fun(name const & n, expr const & t, expr const & b) { return pi(n, t, abstract(b, constant(n))); }
inline expr Fun(char const * n, expr const & t, expr const & b) { return Fun(name(n), t, b); }
inline expr Fun(expr const & n, expr const & t, expr const & b) { return pi(const_name(n), t, abstract(b, n)); }
inline expr Pi(name const & n, expr const & t, expr const & b) { return mk_pi(n, t, abstract(b, mk_constant(n))); }
inline expr Pi(char const * n, expr const & t, expr const & b) { return Pi(name(n), t, b); }
inline expr Pi(expr const & n, expr const & t, expr const & b) { return mk_pi(const_name(n), t, abstract(b, n)); }
inline expr Pi(std::pair<expr const &, expr const &> const & p, expr const & b) { return Pi(p.first, p.second, b); }
expr Pi(std::initializer_list<std::pair<expr const &, expr const &>> const & l, expr const & b);
}

47
src/kernel/arith/arith.cpp
View file

@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/
#include "builtin.h"
#include "arith.h"
#include "abstract.h"
#include "environment.h"
namespace lean {
@ -15,7 +16,7 @@ public:
static char const * g_kind;
virtual ~int_type_value() {}
char const * kind() const { return g_kind; }
virtual expr get_type() const { return type(level()); }
virtual expr get_type() const { return Type(); }
virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { return false; }
virtual bool operator==(value const & other) const { return other.kind() == kind(); }
virtual void display(std::ostream & out) const { out << "int"; }
@ -34,7 +35,7 @@ public:
int_value_value(mpz const & v):m_val(v) {}
virtual ~int_value_value() {}
char const * kind() const { return g_kind; }
virtual expr get_type() const { return int_type(); }
virtual expr get_type() const { return Int; }
virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { return false; }
virtual bool operator==(value const & other) const {
return other.kind() == kind() && m_val == static_cast<int_value_value const &>(other).m_val;
@ -47,8 +48,8 @@ public:
char const * int_value_value::g_kind = "int_num";
expr int_value(mpz const & v) {
return to_expr(*(new int_value_value(v)));
expr mk_int_value(mpz const & v) {
return mk_value(*(new int_value_value(v)));
}
bool is_int_value(expr const & e) {
@ -66,7 +67,7 @@ class int_bin_op : public value {
public:
static char const * g_kind;
int_bin_op() {
m_type = arrow(int_type(), arrow(int_type(), int_type()));
m_type = Int >> (Int >> Int);
}
virtual ~int_bin_op() {}
char const * kind() const { return g_kind; }
@ -74,7 +75,7 @@ public:
virtual bool operator==(value const & other) const { return other.kind() == kind(); }
virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
if (num_args == 3 && is_int_value(args[1]) && is_int_value(args[2])) {
r = int_value(F()(int_value_numeral(args[1]), int_value_numeral(args[2])));
r = mk_int_value(F()(int_value_numeral(args[1]), int_value_numeral(args[2])));
return true;
} else {
return false;
@ -90,37 +91,37 @@ template<char const * Name, unsigned Hash, typename F> char const * int_bin_op<N
constexpr char int_add_name[] = "+";
struct int_add_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 + v2; }; };
typedef int_bin_op<int_add_name, 43, int_add_eval> int_add_value;
MK_BUILTIN(int_add, int_add_value);
MK_BUILTIN(int_add_fn, int_add_value);
constexpr char int_sub_name[] = "-";
struct int_sub_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 - v2; }; };
typedef int_bin_op<int_sub_name, 47, int_sub_eval> int_sub_value;
MK_BUILTIN(int_sub, int_sub_value);
MK_BUILTIN(int_sub_fn, int_sub_value);
constexpr char int_mul_name[] = "*";
struct int_mul_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 * v2; }; };
typedef int_bin_op<int_mul_name, 53, int_mul_eval> int_mul_value;
MK_BUILTIN(int_mul, int_mul_value);
MK_BUILTIN(int_mul_fn, int_mul_value);
constexpr char int_div_name[] = "div";
struct int_div_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 / v2; }; };
typedef int_bin_op<int_div_name, 61, int_div_eval> int_div_value;
MK_BUILTIN(int_div, int_div_value);
MK_BUILTIN(int_div_fn, int_div_value);
class int_leq_value : public value {
class int_le_value : public value {
expr m_type;
public:
static char const * g_kind;
int_leq_value() {
m_type = arrow(int_type(), arrow(int_type(), bool_type()));
int_le_value() {
m_type = Int >> (Int >> Bool);
}
virtual ~int_leq_value() {}
virtual ~int_le_value() {}
char const * kind() const { return g_kind; }
virtual expr get_type() const { return m_type; }
virtual bool operator==(value const & other) const { return other.kind() == kind(); }
virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
if (num_args == 3 && is_int_value(args[1]) && is_int_value(args[2])) {
r = bool_value(int_value_numeral(args[1]) <= int_value_numeral(args[2]));
r = mk_bool_value(int_value_numeral(args[1]) <= int_value_numeral(args[2]));
return true;
} else {
return false;
@ -130,15 +131,17 @@ public:
virtual format pp() const { return format("<="); }
virtual unsigned hash() const { return 67; }
};
char const * int_leq_value::g_kind = "<=";
MK_BUILTIN(int_leq, int_leq_value);
char const * int_le_value::g_kind = "<=";
MK_BUILTIN(int_le_fn, int_le_value);
MK_CONSTANT(int_geq, name(name("int"), "geq"));
MK_CONSTANT(int_lt, name(name("int"), "lt"));
MK_CONSTANT(int_gt, name(name("int"), "gt"));
MK_CONSTANT(int_ge_fn, name(name("int"), "ge"));
MK_CONSTANT(int_lt_fn, name(name("int"), "lt"));
MK_CONSTANT(int_gt_fn, name(name("int"), "gt"));
void add_int_theory(environment & env) {
expr p = arrow(int_type(), arrow(int_type(), bool_type()));
env.add_definition(int_geq_name, p, lambda("x", int_type(), lambda("y", int_type(), app(int_leq(), var(0), var(1)))));
expr p = Int >> (Int >> Bool);
expr x = Const("x");
expr y = Const("y");
env.add_definition(int_ge_fn_name, p, Fun({{x, Int}, {y, Int}}, iLe(y, x)));
}
}

51
src/kernel/arith/arith.h
View file

@ -6,41 +6,54 @@ Author: Leonardo de Moura
*/
#pragma once
#include "expr.h"
#include "builtin.h"
#include "mpz.h"
#include "mpq.h"
namespace lean {
expr int_type();
expr mk_int_type();
#define Int mk_int_type()
bool is_int_type(expr const & e);
expr int_value(mpz const & v);
inline expr int_value(int v) { return int_value(mpz(v)); }
expr mk_int_value(mpz const & v);
inline expr mk_int_value(int v) { return mk_int_value(mpz(v)); }
inline expr iVal(int v) { return mk_int_value(v); }
bool is_int_value(expr const & e);
mpz const & int_value_numeral(expr const & e);
expr int_add();
bool is_int_add(expr const & e);
expr mk_int_add_fn();
bool is_int_add_fn(expr const & e);
inline expr iAdd(expr const & e1, expr const & e2) { return mk_app(mk_int_add_fn(), e1, e2); }
expr int_sub();
bool is_int_sub(expr const & e);
expr mk_int_sub_fn();
bool is_int_sub_fn(expr const & e);
inline expr iSub(expr const & e1, expr const & e2) { return mk_app(mk_int_sub_fn(), e1, e2); }
expr int_mul();
bool is_int_mul(expr const & e);
expr mk_int_mul_fn();
bool is_int_mul_fn(expr const & e);
inline expr iMul(expr const & e1, expr const & e2) { return mk_app(mk_int_mul_fn(), e1, e2); }
expr int_div();
bool is_int_div(expr const & e);
expr mk_int_div_fn();
bool is_int_div_fn(expr const & e);
inline expr iDiv(expr const & e1, expr const & e2) { return mk_app(mk_int_div_fn(), e1, e2); }
expr int_leq();
bool is_int_leq(expr const & e);
expr mk_int_le_fn();
bool is_int_le_fn(expr const & e);
inline expr iLe(expr const & e1, expr const & e2) { return mk_app(mk_int_le_fn(), e1, e2); }
expr int_geq();
bool is_int_geq(expr const & e);
expr mk_int_ge_fn();
bool is_int_ge_fn(expr const & e);
inline expr iGe(expr const & e1, expr const & e2) { return mk_app(mk_int_ge_fn(), e1, e2); }
expr int_lt();
bool is_int_lt(expr const & e);
expr mk_int_lt_fn();
bool is_int_lt_fn(expr const & e);
inline expr iLt(expr const & e1, expr const & e2) { return mk_app(mk_int_lt_fn(), e1, e2); }
expr int_gt();
bool is_int_gt(expr const & e);
expr mk_int_gt_fn();
bool is_int_gt_fn(expr const & e);
inline expr iGt(expr const & e1, expr const & e2) { return mk_app(mk_int_gt_fn(), e1, e2); }
inline expr iIf(expr const & c, expr const & t, expr const & e) { return mk_if(Int, c, t, e); }
class environment;
void add_int_theory(environment & env);

108
src/kernel/builtin.cpp
View file

@ -22,7 +22,7 @@ expr mk_bin_op(expr const & op, expr const & unit, unsigned num_args, expr const
unsigned i = num_args - 1;
while (i > 0) {
--i;
r = app(op, args[i], r);
r = mk_app({op, args[i], r});
}
return r;
}
@ -37,7 +37,7 @@ public:
static char const * g_kind;
virtual ~bool_type_value() {}
char const * kind() const { return g_kind; }
virtual expr get_type() const { return type(level()); }
virtual expr get_type() const { return Type(); }
virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { return false; }
virtual bool operator==(value const & other) const { return other.kind() == kind(); }
virtual void display(std::ostream & out) const { out << "bool"; }
@ -56,7 +56,7 @@ public:
bool_value_value(bool v):m_val(v) {}
virtual ~bool_value_value() {}
char const * kind() const { return g_kind; }
virtual expr get_type() const { return bool_type(); }
virtual expr get_type() const { return Bool; }
virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { return false; }
virtual bool operator==(value const & other) const {
return other.kind() == kind() && m_val == static_cast<bool_value_value const &>(other).m_val;
@ -69,9 +69,9 @@ public:
char const * bool_value_value::g_kind = "bool_value";
expr bool_value(bool v) {
static thread_local expr true_val = to_expr(*(new bool_value_value(true)));
static thread_local expr false_val = to_expr(*(new bool_value_value(false)));
expr mk_bool_value(bool v) {
static thread_local expr true_val = mk_value(*(new bool_value_value(true)));
static thread_local expr false_val = mk_value(*(new bool_value_value(false)));
return v ? true_val : false_val;
}
@ -95,13 +95,13 @@ bool is_false(expr const & e) {
static level m_lvl(name("m"));
static level u_lvl(name("u"));
expr m_type() {
static thread_local expr r = type(m_lvl);
expr mk_type_m() {
static thread_local expr r = Type(m_lvl);
return r;
}
expr u_type() {
static thread_local expr r = type(u_lvl);
expr mk_type_u() {
static thread_local expr r = Type(u_lvl);
return r;
}
@ -110,9 +110,9 @@ class if_fn_value : public value {
public:
static char const * g_kind;
if_fn_value() {
expr A = constant("A");
expr A = Const("A");
// Pi (A: Type), bool -> A -> A -> A
m_type = Fun("A", u_type(), arrow(bool_type(), arrow(A, arrow(A, A))));
m_type = Pi({A, TypeU}, Bool >> (A >> (A >> A)));
}
virtual ~if_fn_value() {}
char const * kind() const { return g_kind; }
@ -158,74 +158,76 @@ MK_CONSTANT(foralli_fn, name("foralli"));
MK_CONSTANT(domain_inj_fn, name("domain_inj"));
MK_CONSTANT(range_inj_fn, name("range_inj"));
void add_basic_theory(environment & env) {
env.define_uvar(uvar_name(m_lvl), level() + LEAN_DEFAULT_LEVEL_SEPARATION);
env.define_uvar(uvar_name(u_lvl), m_lvl + LEAN_DEFAULT_LEVEL_SEPARATION);
expr p1 = arrow(bool_type(), bool_type());
expr p2 = arrow(bool_type(), p1);
expr p1 = Bool >> Bool;
expr p2 = Bool >> p1;
expr A = constant("A");
expr a = constant("a");
expr b = constant("b");
expr c = constant("a");
expr H = constant("H");
expr H1 = constant("H1");
expr H2 = constant("H2");
expr B = constant("B");
expr f = constant("f");
expr g = constant("g");
expr x = constant("x");
expr y = constant("y");
expr P = constant("P");
expr A1 = constant("A1");
expr B1 = constant("B1");
expr a1 = constant("a1");
expr A = Const("A");
expr a = Const("a");
expr b = Const("b");
expr c = Const("a");
expr H = Const("H");
expr H1 = Const("H1");
expr H2 = Const("H2");
expr B = Const("B");
expr f = Const("f");
expr g = Const("g");
expr x = Const("x");
expr y = Const("y");
expr P = Const("P");
expr A1 = Const("A1");
expr B1 = Const("B1");
expr a1 = Const("a1");
// and(x, y) = (if bool x y false)
env.add_definition(and_fn_name, p2, fun(x, bool_type(), fun(y, bool_type(), mk_bool_if(x, y, bool_value(false)))));
env.add_definition(and_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, y, True)));
// or(x, y) = (if bool x true y)
env.add_definition(or_fn_name, p2, fun(x, bool_type(), fun(y, bool_type(), mk_bool_if(x, bool_value(true), y))));
env.add_definition(or_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, False, y)));
// not(x) = (if bool x false true)
env.add_definition(not_fn_name, p1, fun(x, bool_type(), mk_bool_if(x, bool_value(false), bool_value(true))));
env.add_definition(not_fn_name, p1, Fun({{x, Bool}}, bIf(x, False, True)));
// forall : Pi (A : Type u), (A -> Bool) -> Bool
expr A_pred = arrow(A, bool_type());
expr q_type = Fun(A, u_type(), arrow(A_pred, bool_type()));
expr A_pred = A >> Bool;
expr q_type = Pi({A, TypeU}, A_pred >> Bool);
env.add_var(forall_fn_name, q_type);
env.add_definition(exists_fn_name, q_type, fun(A, u_type(), fun(P, A_pred, mk_not(mk_forall(A, fun(x, A, mk_not(P(x))))))));
env.add_definition(exists_fn_name, q_type, Fun({{A,TypeU}, {P, A_pred}}, Not(Forall(A, Fun({x, A}, Not(P(x)))))));
// refl : Pi (A : Type u) (a : A), a = a
env.add_axiom(refl_fn_name, Fun(A, u_type(), Fun(a, A, eq(a, a))));
env.add_axiom(refl_fn_name, Pi({{A, TypeU}, {a, A}}, Eq(a, a)));
// subst : Pi (A : Type u) (P : A -> bool) (a b : A) (H1 : P a) (H2 : a = b), P b
env.add_axiom(subst_fn_name, Fun(A, u_type(), Fun(P, A_pred, Fun(a, A, Fun(b, A, Fun(H1, P(a), Fun(H2, eq(a, b), P(b))))))));
env.add_axiom(subst_fn_name, Pi({{A, TypeU}, {P, A_pred}, {a, A}, {b, A}, {H1, P(a)}, {H2, Eq(a,b)}}, P(b)));
// symm : Pi (A : Type u) (a b : A) (H : a = b), b = a :=
// subst A (fun x : A => x = a) a b (refl A a) H
env.add_definition(symm_fn_name, Fun(A, u_type(), Fun(a, A, Fun(b, A, Fun(H, eq(a, b), eq(b, a))))),
fun(A, u_type(), fun(a, A, fun(b, A, fun(H, eq(a, b), app(subst_fn(), A, fun(x, A, eq(x,a)), a, b, app(refl_fn(), A, a), H))))));
env.add_definition(symm_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {H, Eq(a, b)}}, Eq(b, a)),
Fun({{A, TypeU}, {a, A}, {b, A}, {H, Eq(a, b)}},
Subst(A, Fun({{x, A}}, Eq(x,a)), a, b, Refl(A, a), H)));
// trans: Pi (A: Type u) (a b c : A) (H1 : a = b) (H2 : b = c), a = c :=
// subst A (fun x : A => a = x) b c H1 H2
env.add_definition(trans_fn_name, Fun(A, u_type(), Fun(a, A, Fun(b, A, Fun(c, A, Fun(H1, eq(a, b), Fun(H2, eq(b, c), eq(a, c))))))),
fun(A, u_type(), fun(a, A, fun(b, A, fun(c, A, fun(H1, eq(a, b), fun(H2, eq(b, c), app(subst_fn(), A, fun(x, A, eq(a, x)), b, c, H1, H2))))))));
env.add_definition(trans_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)),
Fun({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a,b)}, {H2, Eq(b,c)}},
Subst(A, Fun({{x, A}}, Eq(a, x)), b, c, H1, H2)));
// congr : Pi (A : Type u) (B : A -> Type u) (f g : Pi (x : A) B x) (a b : A) (H1 : f = g) (H2 : a = b), f a = g b
expr piABx = Fun(x, A, B(x));
expr A_arrow_u = arrow(A, u_type());
env.add_axiom(congr_fn_name, Fun(A, u_type(), Fun(B, A_arrow_u, Fun(f, piABx, Fun(g, piABx, Fun(a, A, Fun(b, A, Fun(H1, eq(f, g), Fun(H2, eq(a, b), eq(f(a), g(b)))))))))));
expr piABx = Pi({x, A}, B(x));
expr A_arrow_u = A >> TypeU;
env.add_axiom(congr_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {b, A}, {H1, Eq(f, g)}, {H2, Eq(a, b)}}, Eq(f(a), g(b))));
// ext : Pi (A : Type u) (B : A -> Type u) (f g : Pi (x : A) B x) (H : Pi x : A, (f x) = (g x)), f = g
env.add_axiom(ext_fn_name, Fun(A, u_type(), Fun(B, A_arrow_u, Fun(f, piABx, Fun(g, piABx, Fun(H, Fun(x, A, eq(f(x), g(x))), eq(f, g)))))));
env.add_axiom(ext_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {H, Pi({x, A}, Eq(f(x), g(x)))}}, Eq(f, g)));
// foralle : Pi (A : Type u) (P : A -> bool) (H : (forall A P)) (a : A), P a
env.add_axiom(foralle_fn_name, Fun(A, u_type(), Fun(P, A_pred, Fun(H, mk_forall(A, P), Fun(a, A, P(a))))));
env.add_axiom(foralle_fn_name, Pi({{A, TypeU}, {P, A_pred}, {H, mk_forall(A, P)}, {a, A}}, P(a)));
// foralli : Pi (A : Type u) (P : A -> bool) (H : Pi (x : A), P x), (forall A P)
env.add_axiom(foralli_fn_name, Fun(A, u_type(), Fun(P, A_pred, Fun(H, Fun(x, A, P(x)), mk_forall(A, P)))));
env.add_axiom(foralli_fn_name, Pi({{A, TypeU}, {P, A_pred}, {H, Pi({x, A}, P(x))}}, Forall(A, P)));
// domain_inj : Pi (A A1: Type u) (B : A -> Type u) (B1 : A1 -> Type u) (H : (Pi (x : A), B x) = (Pi (x : A1), B1 x)), A = A1
expr piA1B1x = Fun(x, A1, B1(x));
env.add_axiom(domain_inj_fn_name, Fun(A, u_type(), Fun(A1, u_type(), Fun(B, A_arrow_u, Fun(B1, arrow(A1, u_type()), Fun(H, eq(piABx, piA1B1x), eq(A, A1)))))));
expr piA1B1x = Pi({x, A1}, B1(x));
expr A1_arrow_u = A1 >> TypeU;
env.add_axiom(domain_inj_fn_name, Pi({{A, TypeU}, {A1, TypeU}, {B, A_arrow_u}, {B1, A1_arrow_u}, {H, Eq(piABx, piA1B1x)}}, Eq(A, A1)));
// range_inj : Pi (A A1: Type u) (B : A -> Type u) (B1 : A1 -> Type u) (a : A) (a1 : A1) (H : (Pi (x : A), B x) = (Pi (x : A1), B1 x)), (B a) = (B1 a1)
env.add_axiom(range_inj_fn_name, Fun(A, u_type(), Fun(A1, u_type(), Fun(B, A_arrow_u, Fun(B1, arrow(A1, u_type()), Fun(a, A, Fun(a1, A1, Fun(H, eq(piABx, piA1B1x), eq(B(a), B1(a1))))))))));
env.add_axiom(range_inj_fn_name, Pi({{A, TypeU}, {A1, TypeU}, {B, A_arrow_u}, {B1, A1_arrow_u}, {a, A}, {a1, A1}, {H, Eq(piABx, piA1B1x)}}, Eq(B(a), B1(a1))));
}
}

85
src/kernel/builtin.h
View file

@ -16,18 +16,23 @@ expr mk_bin_op(expr const & op, expr const & unit, unsigned num_args, expr const
expr mk_bin_op(expr const & op, expr const & unit, std::initializer_list<expr> const & l);
/** \brief Return (Type m) m >= bottom + Offset */
expr m_type();
expr mk_type_m();
#define TypeM mk_type_m()
/** \brief Return (Type u) u >= m + Offset */
expr u_type();
expr mk_type_u();
#define TypeU mk_type_u()
/** \brief Return the Lean Boolean type. */
expr bool_type();
expr mk_bool_type();
#define Bool mk_bool_type()
/** \brief Return true iff \c e is the Lean Boolean type. */
bool is_bool_type(expr const & e);
/** \brief Create a Lean Boolean value (true/false) */
expr bool_value(bool v);
expr mk_bool_value(bool v);
#define True mk_bool_value(true)
#define False mk_bool_value(false)
/** \brief Return true iff \c e is a Lean Boolean value. */
bool is_bool_value(expr const & e);
/**
@ -41,74 +46,84 @@ bool is_true(expr const & e);
bool is_false(expr const & e);
/** \brief Return the Lean If-Then-Else operator. It has type: pi (A : Type), bool -> A -> A -> A */
expr if_fn();
expr mk_if_fn();
/** \brief Return true iff \c e is the Lean If-Then-Else operator */
bool is_if_fn(expr const & e);
/** \brief Return the term (if A c t e) */
inline expr mk_if(expr const & A, expr const & c, expr const & t, expr const & e) { return app(if_fn(), A, c, t, e); }
inline expr mk_if(expr const & A, expr const & c, expr const & t, expr const & e) { return mk_app(mk_if_fn(), A, c, t, e); }
inline expr If(expr const & A, expr const & c, expr const & t, expr const & e) { return mk_if(A, c, t, e); }
/** \brief Return the term (if bool c t e) */
inline expr mk_bool_if(expr const & c, expr const & t, expr const & e) { return mk_if(bool_type(), c, t, e); }
inline expr mk_bool_if(expr const & c, expr const & t, expr const & e) { return mk_if(mk_bool_type(), c, t, e); }
inline expr bIf(expr const & c, expr const & t, expr const & e) { return mk_bool_if(c, t, e); }
/** \brief Return the Lean and operator */
expr and_fn();
expr mk_and_fn();
/** \brief Return true iff \c e is the Lean and operator. */
bool is_and_fn(expr const & e);
/** \brief Return (and e1 e2) */
inline expr mk_and(expr const & e1, expr const & e2) { return app(and_fn(), e1, e2); }
inline expr mk_and(unsigned num_args, expr const * args) { return mk_bin_op(and_fn(), bool_value(true), num_args, args); }
inline expr mk_and(std::initializer_list<expr> const & l) { return mk_bin_op(and_fn(), bool_value(true), l); }
inline expr mk_and(expr const & e1, expr const & e2) { return mk_app(mk_and_fn(), e1, e2); }
inline expr mk_and(unsigned num_args, expr const * args) { return mk_bin_op(mk_and_fn(), True, num_args, args); }
inline expr And(expr const & e1, expr const & e2) { return mk_and(e1, e2); }
inline expr And(std::initializer_list<expr> const & l) { return mk_and(l.size(), l.begin()); }
/** \brief Return the Lean or operator */
expr or_fn();
expr mk_or_fn();
bool is_or_fn(expr const & e);
/** \brief Return (or e1 e2) */
inline expr mk_or(expr const & e1, expr const & e2) { return app(or_fn(), e1, e2); }
inline expr mk_or(unsigned num_args, expr const * args) { return mk_bin_op(or_fn(), bool_value(false), num_args, args); }
inline expr mk_or(std::initializer_list<expr> const & l) { return mk_bin_op(or_fn(), bool_value(false), l); }
inline expr mk_or(expr const & e1, expr const & e2) { return mk_app(mk_or_fn(), e1, e2); }
inline expr mk_or(unsigned num_args, expr const * args) { return mk_bin_op(mk_or_fn(), False, num_args, args); }
inline expr Or(expr const & e1, expr const & e2) { return mk_or(e1, e2); }
inline expr Or(std::initializer_list<expr> const & l) { return mk_or(l.size(), l.begin()); }
/** \brief Return the Lean not operator */
expr not_fn();
expr mk_not_fn();
bool is_not_fn(expr const & e);
/** \brief Return (not e) */
inline expr mk_not(expr const & e) { return app(not_fn(), e); }
inline expr mk_not(expr const & e) { return mk_app(mk_not_fn(), e); }
inline expr Not(expr const & e) { return mk_not(e); }
/** \brief Return the Lean forall operator. It has type: <tt>Pi (A : Type), (A -> bool) -> Bool<\tt> */
expr forall_fn();
expr mk_forall_fn();
/** \brief Return true iff \c e is the Lean forall operator */
bool is_forall_fn(expr const & e);
/** \brief Return the term (forall A P), where A is a type and P : A -> bool */
inline expr mk_forall(expr const & A, expr const & P) { return app(forall_fn(), A, P); }
inline expr mk_forall(expr const & A, expr const & P) { return mk_app(mk_forall_fn(), A, P); }
inline expr Forall(expr const & A, expr const & P) { return mk_forall(A, P); }
/** \brief Return the Lean exists operator. It has type: <tt>Pi (A : Type), (A -> Bool) -> Bool<\tt> */
expr exists_fn();
expr mk_exists_fn();
/** \brief Return true iff \c e is the Lean exists operator */
bool is_exists_fn(expr const & e);
/** \brief Return the term (exists A P), where A is a type and P : A -> bool */
inline expr mk_exists(expr const & A, expr const & P) { return app(exists_fn(), A, P); }
inline expr mk_exists(expr const & A, expr const & P) { return mk_app(mk_exists_fn(), A, P); }
inline expr Exists(expr const & A, expr const & P) { return mk_exists(A, P); }
expr refl_fn();
expr mk_refl_fn();
bool is_refl_fn(expr const & e);
expr subst_fn();
inline expr Refl(expr const & A, expr const & a) { return mk_app(mk_refl_fn(), A, a); }
expr mk_subst_fn();
bool is_subst_fn(expr const & e);
expr symm_fn();
inline expr Subst(expr const & A, expr const & P, expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app({mk_subst_fn(), A, P, a, b, H1, H2}); }
expr mk_symm_fn();
bool is_symm_fn(expr const & e);
expr trans_fn();
expr mk_trans_fn();
bool is_trans_fn(expr const & e);
expr congr_fn();
expr mk_congr_fn();
bool is_congr_fn(expr const & e);
expr ext_fn();
expr mk_ext_fn();
bool is_ext_fn(expr const & e);
expr foralle_fn();
expr mk_foralle_fn();
bool is_foralle_fn(expr const & e);
expr foralli_fn();
expr mk_foralli_fn();
bool is_foralli_fn(expr const & e);
expr domain_inj_fn();
expr mk_domain_inj_fn();
bool is_domain_inj_fn(expr const & e);
expr range_inj_fn();
expr mk_range_inj_fn();
bool is_range_inj_fn(expr const & e);
class environment;
@ -119,8 +134,8 @@ void add_basic_theory(environment & env);
\brief Helper macro for defining constants such as bool_type, int_type, int_add, etc.
*/
#define MK_BUILTIN(Name, ClassName) \
expr Name() { \
static thread_local expr r = to_expr(*(new ClassName())); \
expr mk_##Name() { \
static thread_local expr r = mk_value(*(new ClassName())); \
return r; \
} \
bool is_##Name(expr const & e) { \
@ -132,8 +147,8 @@ bool is_##Name(expr const & e) { \
*/
#define MK_CONSTANT(Name, NameObj) \
static name Name ## _name = NameObj; \
expr Name() { \
static thread_local expr r = constant(Name ## _name); \
expr mk_##Name() { \
static thread_local expr r = mk_constant(Name ## _name); \
return r ; \
} \
bool is_##Name(expr const & e) { \

10
src/kernel/deep_copy.cpp
View file

@ -29,13 +29,13 @@ class deep_copy_fn {
buffer<expr> new_args;
for (expr const & old_arg : args(a))
new_args.push_back(apply(old_arg));
r = app(new_args.size(), new_args.data());
r = mk_app(new_args.size(), new_args.data());
break;
}
case expr_kind::Eq: r = eq(apply(eq_lhs(a)), apply(eq_rhs(a))); break;
case expr_kind::Lambda: r = lambda(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))); break;
case expr_kind::Pi: r = pi(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))); break;
case expr_kind::Let: r = let(let_name(a), apply(let_value(a)), apply(let_body(a))); break;
case expr_kind::Eq: r = mk_eq(apply(eq_lhs(a)), apply(eq_rhs(a))); break;
case expr_kind::Lambda: r = mk_lambda(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))); break;
case expr_kind::Pi: r = mk_pi(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))); break;
case expr_kind::Let: r = mk_let(let_name(a), apply(let_value(a)), apply(let_body(a))); break;
}
if (sh)
m_cache.insert(std::make_pair(a.raw(), r));

26
src/kernel/expr.cpp
View file

@ -41,7 +41,7 @@ expr_app::~expr_app() {
for (unsigned i = 0; i < m_num_args; i++)
(m_args+i)->~expr();
}
expr app(unsigned n, expr const * as) {
expr mk_app(unsigned n, expr const * as) {
lean_assert(n > 1);
unsigned new_n;
unsigned n0 = 0;
@ -126,10 +126,8 @@ void expr_cell::dealloc() {
}
}
expr type() {
static thread_local expr r;
if (!r)
r = type(level());
expr mk_type() {
static thread_local expr r = mk_type(level());
return r;
}
@ -223,15 +221,15 @@ std::ostream & operator<<(std::ostream & out, expr const & a) {
expr copy(expr const & a) {
switch (a.kind()) {
case expr_kind::Var: return var(var_idx(a));
case expr_kind::Constant: return constant(const_name(a));
case expr_kind::Type: return type(ty_level(a));
case expr_kind::Value: return to_expr(static_cast<expr_value*>(a.raw())->m_val);
case expr_kind::App: return app(num_args(a), begin_args(a));
case expr_kind::Eq: return eq(eq_lhs(a), eq_rhs(a));
case expr_kind::Lambda: return lambda(abst_name(a), abst_domain(a), abst_body(a));
case expr_kind::Pi: return pi(abst_name(a), abst_domain(a), abst_body(a));
case expr_kind::Let: return let(let_name(a), let_value(a), let_body(a));
case expr_kind::Var: return mk_var(var_idx(a));
case expr_kind::Constant: return mk_constant(const_name(a));
case expr_kind::Type: return mk_type(ty_level(a));
case expr_kind::Value: return mk_value(static_cast<expr_value*>(a.raw())->m_val);
case expr_kind::App: return mk_app(num_args(a), begin_args(a));
case expr_kind::Eq: return mk_eq(eq_lhs(a), eq_rhs(a));
case expr_kind::Lambda: return mk_lambda(abst_name(a), abst_domain(a), abst_body(a));
case expr_kind::Pi: return mk_pi(abst_name(a), abst_domain(a), abst_body(a));
case expr_kind::Let: return mk_let(let_name(a), let_value(a), let_body(a));
}
lean_unreachable();
return expr();

97
src/kernel/expr.h
View file

@ -93,16 +93,15 @@ public:
operator bool() const { return m_ptr != nullptr; }
friend expr var(unsigned idx);
friend expr constant(name const & n);
friend expr to_expr(value & v);
friend expr app(unsigned num_args, expr const * args);
friend expr app(std::initializer_list<expr> const & l);
friend expr eq(expr const & l, expr const & r);
friend expr lambda(name const & n, expr const & t, expr const & e);
friend expr pi(name const & n, expr const & t, expr const & e);
friend expr type(level const & l);
friend expr let(name const & n, expr const & v, expr const & e);
friend expr mk_var(unsigned idx);
friend expr mk_constant(name const & n);
friend expr mk_value(value & v);
friend expr mk_app(unsigned num_args, expr const * args);
friend expr mk_eq(expr const & l, expr const & r);
friend expr mk_lambda(name const & n, expr const & t, expr const & e);
friend expr mk_pi(name const & n, expr const & t, expr const & e);
friend expr mk_type(level const & l);
friend expr mk_let(name const & n, expr const & v, expr const & e);
friend bool is_eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; }
@ -111,6 +110,9 @@ public:
expr operator()(expr const & a1, expr const & a2) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5, expr const & a6) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5, expr const & a6, expr const & a7) const;
};
// =======================================
@ -133,7 +135,7 @@ public:
class expr_app : public expr_cell {
unsigned m_num_args;
expr m_args[0];
friend expr app(unsigned num_args, expr const * args);
friend expr mk_app(unsigned num_args, expr const * args);
public:
expr_app(unsigned size);
~expr_app();
@ -251,36 +253,43 @@ inline bool is_abstraction(expr const & e) { return is_lambda(e) || is_pi(e); }
// =======================================
// Constructors
inline expr var(unsigned idx) { return expr(new expr_var(idx)); }
inline expr constant(name const & n) { return expr(new expr_const(n)); }
inline expr constant(char const * n) { return constant(name(n)); }
inline expr to_expr(value & v) { return expr(new expr_value(v)); }
expr app(unsigned num_args, expr const * args);
inline expr app(expr const & e1, expr const & e2) { expr args[2] = {e1, e2}; return app(2, args); }
inline expr app(expr const & e1, expr const & e2, expr const & e3) { expr args[3] = {e1, e2, e3}; return app(3, args); }
inline expr app(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { expr args[4] = {e1, e2, e3, e4}; return app(4, args); }
inline expr app(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { expr args[5] = {e1, e2, e3, e4, e5}; return app(5, args); }
inline expr app(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) {
expr args[6] = {e1, e2, e3, e4, e5, e6}; return app(6, args);
}
inline expr app(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7) {
expr args[7] = {e1, e2, e3, e4, e5, e6, e7}; return app(7, args);
}
inline expr eq(expr const & l, expr const & r) { return expr(new expr_eq(l, r)); }
inline expr lambda(name const & n, expr const & t, expr const & e) { return expr(new expr_lambda(n, t, e)); }
inline expr lambda(char const * n, expr const & t, expr const & e) { return lambda(name(n), t, e); }
inline expr pi(name const & n, expr const & t, expr const & e) { return expr(new expr_pi(n, t, e)); }
inline expr pi(char const * n, expr const & t, expr const & e) { return pi(name(n), t, e); }
inline expr arrow(expr const & t, expr const & e) { return pi(name("_"), t, e); }
inline expr let(name const & n, expr const & v, expr const & e) { return expr(new expr_let(n, v, e)); }
inline expr let(char const * n, expr const & v, expr const & e) { return let(name(n), v, e); }
inline expr type(level const & l) { return expr(new expr_type(l)); }
expr type();
inline expr mk_var(unsigned idx) { return expr(new expr_var(idx)); }
inline expr Var(unsigned idx) { return mk_var(idx); }
inline expr mk_constant(name const & n) { return expr(new expr_const(n)); }
inline expr mk_constant(char const * n) { return mk_constant(name(n)); }
inline expr Const(name const & n) { return mk_constant(n); }
inline expr Const(char const * n) { return mk_constant(n); }
inline expr mk_value(value & v) { return expr(new expr_value(v)); }
inline expr to_expr(value & v) { return mk_value(v); }
expr mk_app(unsigned num_args, expr const * args);
inline expr mk_app(std::initializer_list<expr> const & l) { return mk_app(l.size(), l.begin()); }
inline expr mk_app(expr const & e1, expr const & e2) { return mk_app({e1, e2}); }
inline expr mk_app(expr const & e1, expr const & e2, expr const & e3) { return mk_app({e1, e2, e3}); }
inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({e1, e2, e3, e4}); }
inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({e1, e2, e3, e4, e5}); }
inline expr mk_eq(expr const & l, expr const & r) { return expr(new expr_eq(l, r)); }
inline expr Eq(expr const & l, expr const & r) { return mk_eq(l, r); }
inline expr mk_lambda(name const & n, expr const & t, expr const & e) { return expr(new expr_lambda(n, t, e)); }
inline expr mk_lambda(char const * n, expr const & t, expr const & e) { return mk_lambda(name(n), t, e); }
inline expr mk_pi(name const & n, expr const & t, expr const & e) { return expr(new expr_pi(n, t, e)); }
inline expr mk_pi(char const * n, expr const & t, expr const & e) { return mk_pi(name(n), t, e); }
inline expr arrow(expr const & t, expr const & e) { return mk_pi(name("_"), t, e); }
inline expr operator>>(expr const & t, expr const & e) { return arrow(t, e); }
inline expr mk_let(name const & n, expr const & v, expr const & e) { return expr(new expr_let(n, v, e)); }
inline expr mk_let(char const * n, expr const & v, expr const & e) { return mk_let(name(n), v, e); }
inline expr Let(char const * n, expr const & v, expr const & e) { return mk_let(n, v, e); }
inline expr mk_type(level const & l) { return expr(new expr_type(l)); }
expr mk_type();
inline expr Type(level const & l) { return mk_type(l); }
inline expr Type() { return mk_type(); }
inline expr expr::operator()(expr const & a1) const { return app(*this, a1); }
inline expr expr::operator()(expr const & a1, expr const & a2) const { return app(*this, a1, a2); }
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3) const { return app(*this, a1, a2, a3); }
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const { return app(*this, a1, a2, a3, a4); }
inline expr expr::operator()(expr const & a1) const { return mk_app({*this, a1}); }
inline expr expr::operator()(expr const & a1, expr const & a2) const { return mk_app({*this, a1, a2}); }
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3) const { return mk_app({*this, a1, a2, a3}); }
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const { return mk_app({*this, a1, a2, a3, a4}); }
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const { return mk_app({*this, a1, a2, a3, a4, a5}); }
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5, expr const & a6) const { return mk_app({*this, a1, a2, a3, a4, a5, a6}); }
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) const { return mk_app({*this, a1, a2, a3, a4, a5, a6, a7}); }
// =======================================
// =======================================
@ -418,7 +427,7 @@ template<typename F> expr update_app(expr const & e, F f) {
modified = true;
}
if (modified)
return app(new_args.size(), new_args.data());
return mk_app(new_args.size(), new_args.data());
else
return e;
}
@ -431,7 +440,7 @@ template<typename F> expr update_abst(expr const & e, F f) {
std::pair<expr, expr> p = f(old_t, old_b);
if (!is_eqp(p.first, old_t) || !is_eqp(p.second, old_b)) {
name const & n = abst_name(e);
return is_pi(e) ? pi(n, p.first, p.second) : lambda(n, p.first, p.second);
return is_pi(e) ? mk_pi(n, p.first, p.second) : mk_lambda(n, p.first, p.second);
}
else {
return e;
@ -445,7 +454,7 @@ template<typename F> expr update_let(expr const & e, F f) {
expr const & old_b = let_body(e);
std::pair<expr, expr> p = f(old_v, old_b);
if (!is_eqp(p.first, old_v) || !is_eqp(p.second, old_b))
return let(let_name(e), p.first, p.second);
return mk_let(let_name(e), p.first, p.second);
else
return e;
}
@ -457,7 +466,7 @@ template<typename F> expr update_eq(expr const & e, F f) {
expr const & old_r = eq_rhs(e);
std::pair<expr, expr> p = f(old_l, old_r);
if (!is_eqp(p.first, old_l) || !is_eqp(p.second, old_r))
return eq(p.first, p.second);
return mk_eq(p.first, p.second);
else
return e;
}

4
src/kernel/free_vars.cpp
View file

@ -107,7 +107,7 @@ expr lower_free_vars(expr const & e, unsigned d) {
auto f = [=](expr const & e, unsigned offset) -> expr {
if (is_var(e) && var_idx(e) >= offset) {
lean_assert(var_idx(e) >= offset + d);
return var(var_idx(e) - d);
return mk_var(var_idx(e) - d);
}
else {
return e;
@ -121,7 +121,7 @@ expr lift_free_vars(expr const & e, unsigned d) {
return e;
auto f = [=](expr const & e, unsigned offset) -> expr {
if (is_var(e) && var_idx(e) >= offset) {
return var(var_idx(e) + d);
return mk_var(var_idx(e) + d);
}
else {
return e;

4
src/kernel/instantiate.cpp
View file

@ -19,7 +19,7 @@ expr instantiate_with_closed(expr const & e, unsigned n, expr const * s) {
if (vidx < offset + n)
return s[n - (vidx - offset) - 1];
else
return var(vidx - n);
return mk_var(vidx - n);
}
}
return e;
@ -34,7 +34,7 @@ expr instantiate(expr const & e, unsigned n, expr const * s) {
if (vidx < offset + n)
return lift_free_vars(s[n - (vidx - offset) - 1], offset);
else
return var(vidx - n);
return mk_var(vidx - n);
}
}
return e;

14
src/kernel/normalize.cpp
View file

@ -80,7 +80,7 @@ class normalize_fn {
lean_assert(is_lambda(a));
expr new_t = reify(normalize(abst_domain(a), s, k), k);
expr new_b = reify(normalize(abst_body(a), extend(s, svalue(k)), k+1), k+1);
return lambda(abst_name(a), new_t, new_b);
return mk_lambda(abst_name(a), new_t, new_b);
#if 0
// Eta-reduction + Cumulativity + Set theoretic interpretation is unsound.
// Example:
@ -119,7 +119,7 @@ class normalize_fn {
if (v.is_bounded_var()) tout << "#" << to_bvar(v); else tout << to_expr(v); tout << "\n";);
switch (v.kind()) {
case svalue_kind::Expr: return to_expr(v);
case svalue_kind::BoundedVar: return var(k - to_bvar(v) - 1);
case svalue_kind::BoundedVar: return mk_var(k - to_bvar(v) - 1);
case svalue_kind::Closure: return reify_closure(to_expr(v), stack_of(v), k);
}
lean_unreachable();
@ -169,7 +169,7 @@ class normalize_fn {
if (to_value(new_f).normalize(new_args.size(), new_args.data(), r))
return svalue(r);
}
return svalue(app(new_args.size(), new_args.data()));
return svalue(mk_app(new_args.size(), new_args.data()));
}
}
}
@ -177,11 +177,11 @@ class normalize_fn {
expr new_l = reify(normalize(eq_lhs(a), s, k), k);
expr new_r = reify(normalize(eq_rhs(a), s, k), k);
if (new_l == new_r) {
return svalue(bool_value(true));
return svalue(mk_bool_value(true));
} else if (is_value(new_l) && is_value(new_r)) {
return svalue(bool_value(false));
return svalue(mk_bool_value(false));
} else {
return svalue(eq(new_l, new_r));
return svalue(mk_eq(new_l, new_r));
}
}
case expr_kind::Lambda:
@ -189,7 +189,7 @@ class normalize_fn {
case expr_kind::Pi: {
expr new_t = reify(normalize(abst_domain(a), s, k), k);
expr new_b = reify(normalize(abst_body(a), extend(s, svalue(k)), k+1), k+1);
return svalue(pi(abst_name(a), new_t, new_b));
return svalue(mk_pi(abst_name(a), new_t, new_b));
}
case expr_kind::Let:
return normalize(let_body(a), extend(s, normalize(let_value(a), s, k)), k+1);

8
src/kernel/type_check.cpp
View file

@ -82,7 +82,7 @@ struct infer_type_fn {
case expr_kind::Constant:
return m_env.get_object(const_name(e)).get_type();
case expr_kind::Var: return lookup(ctx, var_idx(e));
case expr_kind::Type: return type(ty_level(e) + 1);
case expr_kind::Type: return mk_type(ty_level(e) + 1);
case expr_kind::App: {
expr f_t = infer_pi(arg(e, 0), ctx);
unsigned i = 1;
@ -110,16 +110,16 @@ struct infer_type_fn {
case expr_kind::Eq:
infer_type(eq_lhs(e), ctx);
infer_type(eq_rhs(e), ctx);
return bool_type();
return mk_bool_type();
case expr_kind::Lambda: {
infer_universe(abst_domain(e), ctx);
expr t = infer_type(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)));
return pi(abst_name(e), abst_domain(e), t);
return mk_pi(abst_name(e), abst_domain(e), t);
}
case expr_kind::Pi: {
level l1 = infer_universe(abst_domain(e), ctx);
level l2 = infer_universe(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)));
return type(max(l1, l2));
return mk_type(max(l1, l2));
}
case expr_kind::Let:
return infer_type(let_body(e), extend(ctx, let_name(e), infer_type(let_value(e), ctx), let_value(e)));

82
src/tests/kernel/arith.cpp
View file

@ -16,84 +16,84 @@ using namespace lean;
static void tst1() {
environment env;
expr e = int_value(mpz(10));
expr e = mk_int_value(mpz(10));
lean_assert(is_int_value(e));
lean_assert(infer_type(e, env) == int_type());
lean_assert(infer_type(e, env) == Int);
std::cout << "e: " << e << "\n";
}
static void tst2() {
environment env;
expr e = app(int_add(), int_value(10), int_value(30));
expr e = iAdd(iVal(10), iVal(30));
std::cout << e << "\n";
std::cout << normalize(e, env) << "\n";
lean_assert(normalize(e, env) == int_value(40));
std::cout << infer_type(int_add(), env) << "\n";
lean_assert(infer_type(e, env) == int_type());
lean_assert(infer_type(app(int_add(), int_value(10)), env) == arrow(int_type(), int_type()));
lean_assert(is_int_add(int_add()));
lean_assert(!is_int_add(int_mul()));
lean_assert(normalize(e, env) == iVal(40));
std::cout << infer_type(mk_int_add_fn(), env) << "\n";
lean_assert(infer_type(e, env) == Int);
lean_assert(infer_type(mk_app(mk_int_add_fn(), iVal(10)), env) == (Int >> Int));
lean_assert(is_int_add_fn(mk_int_add_fn()));
lean_assert(!is_int_add_fn(mk_int_mul_fn()));
lean_assert(is_int_value(normalize(e, env)));
expr e2 = fun("a", int_type(), app(int_add(), constant("a"), app(int_add(), int_value(10), int_value(30))));
expr e2 = Fun("a", Int, iAdd(Const("a"), iAdd(iVal(10), iVal(30))));
std::cout << e2 << " --> " << normalize(e2, env) << "\n";
lean_assert(infer_type(e2, env) == arrow(int_type(), int_type()));
lean_assert(normalize(e2, env) == fun("a", int_type(), app(int_add(), constant("a"), int_value(40))));
lean_assert(infer_type(e2, env) == arrow(Int, Int));
lean_assert(normalize(e2, env) == Fun("a", Int, iAdd(Const("a"), iVal(40))));
}
static void tst3() {
environment env;
expr e = app(int_mul(), int_value(10), int_value(30));
expr e = iMul(iVal(10), iVal(30));
std::cout << e << "\n";
std::cout << normalize(e, env) << "\n";
lean_assert(normalize(e, env) == int_value(300));
std::cout << infer_type(int_mul(), env) << "\n";
lean_assert(infer_type(e, env) == int_type());
lean_assert(infer_type(app(int_mul(), int_value(10)), env) == arrow(int_type(), int_type()));
lean_assert(is_int_mul(int_mul()));
lean_assert(!is_int_mul(int_add()));
lean_assert(normalize(e, env) == iVal(300));
std::cout << infer_type(mk_int_mul_fn(), env) << "\n";
lean_assert(infer_type(e, env) == Int);
lean_assert(infer_type(mk_app(mk_int_mul_fn(), iVal(10)), env) == arrow(Int, Int));
lean_assert(is_int_mul_fn(mk_int_mul_fn()));
lean_assert(!is_int_mul_fn(mk_int_add_fn()));
lean_assert(is_int_value(normalize(e, env)));
expr e2 = fun("a", int_type(), app(int_mul(), constant("a"), app(int_mul(), int_value(10), int_value(30))));
expr e2 = Fun("a", Int, iMul(Const("a"), iMul(iVal(10), iVal(30))));
std::cout << e2 << " --> " << normalize(e2, env) << "\n";
lean_assert(infer_type(e2, env) == arrow(int_type(), int_type()));
lean_assert(normalize(e2, env) == fun("a", int_type(), app(int_mul(), constant("a"), int_value(300))));
lean_assert(infer_type(e2, env) == (Int >> Int));
lean_assert(normalize(e2, env) == Fun("a", Int, iMul(Const("a"), iVal(300))));
}
static void tst4() {
environment env;
expr e = app(int_sub(), int_value(10), int_value(30));
expr e = iSub(iVal(10), iVal(30));
std::cout << e << "\n";
std::cout << normalize(e, env) << "\n";
lean_assert(normalize(e, env) == int_value(-20));
std::cout << infer_type(int_sub(), env) << "\n";
lean_assert(infer_type(e, env) == int_type());
lean_assert(infer_type(app(int_sub(), int_value(10)), env) == arrow(int_type(), int_type()));
lean_assert(is_int_sub(int_sub()));
lean_assert(!is_int_sub(int_add()));
lean_assert(normalize(e, env) == iVal(-20));
std::cout << infer_type(mk_int_sub_fn(), env) << "\n";
lean_assert(infer_type(e, env) == Int);
lean_assert(infer_type(mk_app(mk_int_sub_fn(), iVal(10)), env) == arrow(Int, Int));
lean_assert(is_int_sub_fn(mk_int_sub_fn()));
lean_assert(!is_int_sub_fn(mk_int_add_fn()));
lean_assert(is_int_value(normalize(e, env)));
expr e2 = fun("a", int_type(), app(int_sub(), constant("a"), app(int_sub(), int_value(10), int_value(30))));
expr e2 = Fun("a", Int, iSub(Const("a"), iSub(iVal(10), iVal(30))));
std::cout << e2 << " --> " << normalize(e2, env) << "\n";
lean_assert(infer_type(e2, env) == arrow(int_type(), int_type()));
lean_assert(normalize(e2, env) == fun("a", int_type(), app(int_sub(), constant("a"), int_value(-20))));
lean_assert(infer_type(e2, env) == (Int >> Int));
lean_assert(normalize(e2, env) == Fun("a", Int, iSub(Const("a"), iVal(-20))));
}
static void tst5() {
environment env;
env.add_var(name("a"), int_type());
expr e = eq(int_value(3), int_value(4));
env.add_var(name("a"), Int);
expr e = Eq(iVal(3), iVal(4));
std::cout << e << " --> " << normalize(e, env) << "\n";
lean_assert(normalize(e, env) == bool_value(false));
lean_assert(normalize(eq(constant("a"), int_value(3)), env) == eq(constant("a"), int_value(3)));
lean_assert(normalize(e, env) == False);
lean_assert(normalize(Eq(Const("a"), iVal(3)), env) == Eq(Const("a"), iVal(3)));
}
static void tst6() {
std::cout << "tst6\n";
std::cout << int_add().raw() << "\n";
std::cout << int_add().raw() << "\n";
std::thread t1([](){ std::cout << "t1: " << int_add().raw() << "\n"; });
std::cout << mk_int_add_fn().raw() << "\n";
std::cout << mk_int_add_fn().raw() << "\n";
std::thread t1([](){ std::cout << "t1: " << mk_int_add_fn().raw() << "\n"; });
t1.join();
std::thread t2([](){ std::cout << "t2: " << int_add().raw() << "\n"; });
std::thread t2([](){ std::cout << "t2: " << mk_int_add_fn().raw() << "\n"; });
t2.join();
std::cout << int_add().raw() << "\n";
std::cout << mk_int_add_fn().raw() << "\n";
}
int main() {

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

@ -62,44 +62,44 @@ static void tst2() {
static void tst3() {
environment env;
try {
env.add_definition("a", int_type(), constant("a"));
env.add_definition("a", Int, Const("a"));
lean_unreachable();
} catch (exception const & ex) {
std::cout << "expected error: " << ex.what() << "\n";
}
env.add_definition("a", int_type(), app(int_add(), int_value(1), int_value(2)));
expr t = app(int_add(), constant("a"), int_value(1));
env.add_definition("a", Int, iAdd(iVal(1), iVal(2)));
expr t = iAdd(Const("a"), iVal(1));
std::cout << t << " --> " << normalize(t, env) << "\n";
lean_assert(normalize(t, env) == int_value(4));
env.add_definition("b", int_type(), app(int_mul(), int_value(2), constant("a")));
std::cout << "b --> " << normalize(constant("b"), env) << "\n";
lean_assert(normalize(constant("b"), env) == int_value(6));
lean_assert(normalize(t, env) == iVal(4));
env.add_definition("b", Int, iMul(iVal(2), Const("a")));
std::cout << "b --> " << normalize(Const("b"), env) << "\n";
lean_assert(normalize(Const("b"), env) == iVal(6));
try {
env.add_definition("c", arrow(int_type(), int_type()), constant("a"));
env.add_definition("c", arrow(Int, Int), Const("a"));
lean_unreachable();
} catch (exception const & ex) {
std::cout << "expected error: " << ex.what() << "\n";
}
try {
env.add_definition("a", int_type(), int_value(10));
env.add_definition("a", Int, iVal(10));
lean_unreachable();
} catch (exception const & ex) {
std::cout << "expected error: " << ex.what() << "\n";
}
environment c_env = env.mk_child();
try {
env.add_definition("c", int_type(), constant("a"));
env.add_definition("c", Int, Const("a"));
lean_unreachable();
} catch (exception const & ex) {
std::cout << "expected error: " << ex.what() << "\n";
}
lean_assert(normalize(constant("b"), env) == int_value(6));
lean_assert(normalize(constant("b"), c_env) == int_value(6));
c_env.add_definition("c", int_type(), constant("a"));
lean_assert(normalize(constant("c"), c_env) == int_value(3));
lean_assert(normalize(Const("b"), env) == iVal(6));
lean_assert(normalize(Const("b"), c_env) == iVal(6));
c_env.add_definition("c", Int, Const("a"));
lean_assert(normalize(Const("c"), c_env) == iVal(3));
try {
expr r = normalize(constant("c"), env);
lean_assert(r == int_value(3));
expr r = normalize(Const("c"), env);
lean_assert(r == iVal(3));
lean_unreachable();
} catch (exception const & ex) {
std::cout << "expected error: " << ex.what() << std::endl;
@ -109,21 +109,21 @@ static void tst3() {
static void tst4() {
environment env;
env.add_definition("a", int_type(), int_value(1), true); // add opaque definition
expr t = app(int_add(), constant("a"), int_value(1));
env.add_definition("a", Int, iVal(1), true); // add opaque definition
expr t = iAdd(Const("a"), iVal(1));
std::cout << t << " --> " << normalize(t, env) << "\n";
lean_assert(normalize(t, env) == t);
env.add_definition("b", int_type(), app(int_add(), constant("a"), int_value(1)));
expr t2 = app(int_sub(), constant("b"), int_value(9));
env.add_definition("b", Int, iAdd(Const("a"), iVal(1)));
expr t2 = iSub(Const("b"), iVal(9));
std::cout << t2 << " --> " << normalize(t2, env) << "\n";
lean_assert(normalize(t2, env) == app(int_sub(), app(int_add(), constant("a"), int_value(1)), int_value(9)));
lean_assert(normalize(t2, env) == iSub(iAdd(Const("a"), iVal(1)), iVal(9)));
}
static void tst5() {
environment env;
env.add_definition("a", int_type(), int_value(1), true); // add opaque definition
env.add_definition("a", Int, iVal(1), true); // add opaque definition
try {
std::cout << infer_type(app(int_add(), constant("a"), int_type()), env) << "\n";
std::cout << infer_type(iAdd(Const("a"), Int), env) << "\n";
lean_unreachable();
} catch (exception const & ex) {
std::cout << "expected error: " << ex.what() << "\n";
@ -134,34 +134,34 @@ static void tst6() {
environment env;
level u = env.define_uvar("u", level() + 1);
level w = env.define_uvar("w", u + 1);
env.add_var("f", arrow(type(u), type(u)));
expr t = app(constant("f"), int_type());
env.add_var("f", arrow(Type(u), Type(u)));
expr t = Const("f")(Int);
std::cout << "type of " << t << " is " << infer_type(t, env) << "\n";
try {
infer_type(app(constant("f"), type(w)), env);
infer_type(Const("f")(Type(w)), env);
lean_unreachable();
} catch (exception const & ex) {
std::cout << "expected error: " << ex.what() << "\n";
}
try {
infer_type(app(constant("f"), type(u)), env);
infer_type(Const("f")(Type(u)), env);
lean_unreachable();
} catch (exception const & ex) {
std::cout << "expected error: " << ex.what() << "\n";
}
t = app(constant("f"), type());
t = Const("f")(Type());
std::cout << "type of " << t << " is " << infer_type(t, env) << "\n";
std::cout << infer_type(arrow(type(u), type(w)), env) << "\n";
lean_assert(infer_type(arrow(type(u), type(w)), env) == type(max(u+1, w+1)));
std::cout << infer_type(arrow(int_type(), int_type()), env) << "\n";
lean_assert(infer_type(arrow(int_type(), int_type()), env) == type());
std::cout << infer_type(arrow(Type(u), Type(w)), env) << "\n";
lean_assert(infer_type(arrow(Type(u), Type(w)), env) == Type(max(u+1, w+1)));
std::cout << infer_type(arrow(Int, Int), env) << "\n";
lean_assert(infer_type(arrow(Int, Int), env) == Type());
}
static void tst7() {
environment env = mk_toplevel();
env.add_var("a", int_type());
env.add_var("b", int_type());
expr t = app(if_fn(), int_type(), bool_value(true), constant("a"), constant("b"));
env.add_var("a", Int);
env.add_var("b", Int);
expr t = If(Int, True, Const("a"), Const("b"));
std::cout << t << " --> " << normalize(t, env) << "\n";
std::cout << infer_type(t, env) << "\n";
std::cout << "Environment\n" << env;

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

@ -18,45 +18,45 @@ using namespace lean;
void tst1() {
expr a;
a = constant("a");
a = Const("a");
expr f;
f = var(0);
f = Var(0);
expr fa = f(a);
expr ty = type(level());
expr ty = Type();
std::cout << fa << "\n";
std::cout << fa(a) << "\n";
lean_assert(is_eqp(arg(fa, 0), f));
lean_assert(is_eqp(arg(fa, 1), a));
lean_assert(!is_eqp(fa, f(a)));
lean_assert(app(fa, a) == f(a, a));
lean_assert(fa(a) == f(a, a));
std::cout << fa(fa, fa) << "\n";
std::cout << 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(f(a(a)) != f(a, a));
lean_assert(lambda("x", ty, var(0)) == lambda("y", ty, var(0)));
std::cout << pi("x", ty, var(0)) << "\n";
lean_assert(mk_lambda("x", ty, Var(0)) == mk_lambda("y", ty, Var(0)));
std::cout << mk_pi("x", ty, Var(0)) << "\n";
}
void tst1_pp() {
std::cerr << "=============== PP =====================\n";
expr a;
a = constant("a");
a = Const("a");
expr f;
f = var(0);
f = Var(0);
expr fa = f(a);
expr ty = type(level());
expr ty = Type();
pp(fa(a)); std::cout << "\n";
pp(fa(fa, fa)); std::cout << "\n";
pp(lambda("x", ty, var(0))); std::cout << "\n";
pp(pi("x", ty, var(0))); std::cout << "\n";
pp(pi("x", ty, lambda("y", ty, var(0)))); std::cout << "\n";
pp(mk_lambda("x", ty, Var(0))); std::cout << "\n";
pp(mk_pi("x", ty, Var(0))); std::cout << "\n";
pp(mk_pi("x", ty, mk_lambda("y", ty, Var(0)))); std::cout << "\n";
std::cerr << "=============== PP =====================\n";
}
expr mk_dag(unsigned depth, bool _closed = false) {
expr f = constant("f");
expr a = _closed ? constant("a") : var(0);
expr f = Const("f");
expr a = _closed ? Const("a") : Var(0);
while (depth > 0) {
depth--;
a = f(a, a);
@ -151,21 +151,21 @@ void tst2() {
expr mk_big(expr f, unsigned depth, unsigned val) {
if (depth == 1)
return constant(name(val));
return Const(name(val));
else
return f(mk_big(f, depth - 1, val << 1), mk_big(f, depth - 1, (val << 1) + 1));
}
void tst3() {
expr f = constant("f");
expr f = Const("f");
expr r1 = mk_big(f, 18, 0);
expr r2 = mk_big(f, 18, 0);
lean_assert(r1 == r2);
}
void tst4() {
expr f = constant("f");
expr a = var(0);
expr f = Const("f");
expr a = Var(0);
for (unsigned i = 0; i < 10000; i++) {
a = f(a);
}
@ -173,7 +173,7 @@ void tst4() {
expr mk_redundant_dag(expr f, unsigned depth) {
if (depth == 0)
return var(0);
return Var(0);
else
return f(mk_redundant_dag(f, depth - 1), mk_redundant_dag(f, depth - 1));
}
@ -205,7 +205,7 @@ unsigned count(expr const & a) {
}
void tst5() {
expr f = constant("f");
expr f = Const("f");
{
expr r1 = mk_redundant_dag(f, 5);
expr r2 = max_sharing(r1);
@ -227,7 +227,7 @@ void tst5() {
}
void tst6() {
expr f = constant("f");
expr f = Const("f");
expr r = mk_redundant_dag(f, 12);
for (unsigned i = 0; i < 1000; i++) {
r = max_sharing(r);
@ -239,8 +239,8 @@ void tst6() {
}
void tst7() {
expr f = constant("f");
expr v = var(0);
expr f = Const("f");
expr v = Var(0);
expr a1 = max_sharing(f(v,v));
expr a2 = max_sharing(f(v,v));
lean_assert(!is_eqp(a1, a2));
@ -249,38 +249,38 @@ void tst7() {
}
void tst8() {
expr f = constant("f");
expr x = var(0);
expr a = constant("a");
expr n = constant("n");
expr p = type(level());
expr y = var(1);
expr f = Const("f");
expr x = Var(0);
expr a = Const("a");
expr n = Const("n");
expr p = Type();
expr y = Var(1);
lean_assert(closed(a));
lean_assert(!closed(x));
lean_assert(closed(f));
lean_assert(!closed(f(x)));
lean_assert(closed(lambda("x", p, x)));
lean_assert(!closed(lambda("x", x, x)));
lean_assert(!closed(lambda("x", p, y)));
lean_assert(closed(mk_lambda("x", p, x)));
lean_assert(!closed(mk_lambda("x", x, x)));
lean_assert(!closed(mk_lambda("x", p, y)));
lean_assert(closed(f(f(f(a)))));
lean_assert(closed(lambda("x", p, f(f(f(a))))));
lean_assert(closed(pi("x", p, x)));
lean_assert(!closed(pi("x", x, x)));
lean_assert(!closed(pi("x", p, y)));
lean_assert(closed(pi("x", p, f(f(f(a))))));
lean_assert(closed(lambda("y", p, lambda("x", p, y))));
lean_assert(closed(lambda("y", p, app(lambda("x", p, y), var(0)))));
expr r = lambda("y", p, app(lambda("x", p, y), var(0)));
lean_assert(closed(mk_lambda("x", p, f(f(f(a))))));
lean_assert(closed(mk_pi("x", p, x)));
lean_assert(!closed(mk_pi("x", x, x)));
lean_assert(!closed(mk_pi("x", p, y)));
lean_assert(closed(mk_pi("x", p, f(f(f(a))))));
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)}))));
expr r = mk_lambda("y", p, mk_app({mk_lambda("x", p, y), Var(0)}));
lean_assert(closed(r));
lean_assert(closed(r));
r = lambda("y", p, app(lambda("x", p, y), var(1)));
r = mk_lambda("y", p, mk_app({mk_lambda("x", p, y), Var(1)}));
lean_assert(!closed(r));
r = lambda("y", p, app(lambda("x", p, var(0)), var(1)));
r = mk_lambda("y", p, mk_app({mk_lambda("x", p, Var(0)), Var(1)}));
lean_assert(!closed(r));
lean_assert(closed(lambda("z", p, r)));
lean_assert(closed(mk_lambda("z", p, r)));
pp(lambda("y", p, app(lambda("x", p, y), var(0)))); std::cout << std::endl;
pp(pi("x", p, f(f(f(a))))); std::cout << std::endl;
pp(mk_lambda("y", p, mk_app({mk_lambda("x", p, y), Var(0)}))); std::cout << std::endl;
pp(mk_pi("x", p, f(f(f(a))))); std::cout << std::endl;
}
@ -292,7 +292,7 @@ void tst9() {
}
void tst10() {
expr f = constant("f");
expr f = Const("f");
expr r = mk_big(f, 16, 0);
for (unsigned i = 0; i < 1000; i++) {
lean_assert(closed(r));
@ -309,34 +309,34 @@ inline expr substitute(expr const & e, expr const & s, expr const & t) {
}
void tst11() {
expr f = constant("f");
expr a = constant("a");
expr b = constant("b");
expr x = var(0);
expr y = var(1);
expr t = type(level());
std::cout << instantiate(lambda("x", t, f(f(y, b), f(x, y))), f(a)) << "\n";
lean_assert(instantiate(lambda("x", t, f(f(y, b), f(x, y))), f(a)) ==
lambda("x", t, f(f(f(a), b), f(x, f(a)))));
std::cout << abstract(lambda("x", t, f(a, lambda("y", t, f(b, a)))), constant("a")) << "\n";
lean_assert(abstract(lambda("x", t, f(a, lambda("y", t, f(b, a)))), constant("a")) ==
lambda("x", t, f(var(1), lambda("y", t, f(b, var(2))))));
std::cout << abstract_p(lambda("x", t, f(a, lambda("y", t, f(b, a)))), constant("a")) << "\n";
lean_assert(abstract_p(lambda("x", t, f(a, lambda("y", t, f(b, a)))), constant("a")) ==
lambda("x", t, f(a, lambda("y", t, f(b, a)))));
std::cout << abstract_p(lambda("x", t, f(a, lambda("y", t, f(b, a)))), a) << "\n";
lean_assert(abstract_p(lambda("x", t, f(a, lambda("y", t, f(b, a)))), a) ==
lambda("x", t, f(var(1), lambda("y", t, f(b, var(2))))));
expr f = Const("f");
expr a = Const("a");
expr b = Const("b");
expr x = Var(0);
expr y = Var(1);
expr t = Type();
std::cout << instantiate(mk_lambda("x", t, f(f(y, b), f(x, y))), f(a)) << "\n";
lean_assert(instantiate(mk_lambda("x", t, f(f(y, b), f(x, y))), f(a)) ==
mk_lambda("x", t, f(f(f(a), b), f(x, f(a)))));
std::cout << abstract(mk_lambda("x", t, f(a, mk_lambda("y", t, f(b, a)))), Const("a")) << "\n";
lean_assert(abstract(mk_lambda("x", t, f(a, mk_lambda("y", t, f(b, a)))), Const("a")) ==
mk_lambda("x", t, f(Var(1), mk_lambda("y", t, f(b, Var(2))))));
std::cout << abstract_p(mk_lambda("x", t, f(a, mk_lambda("y", t, f(b, a)))), Const("a")) << "\n";
lean_assert(abstract_p(mk_lambda("x", t, f(a, mk_lambda("y", t, f(b, a)))), Const("a")) ==
mk_lambda("x", t, f(a, mk_lambda("y", t, f(b, a)))));
std::cout << abstract_p(mk_lambda("x", t, f(a, mk_lambda("y", t, f(b, a)))), a) << "\n";
lean_assert(abstract_p(mk_lambda("x", t, f(a, mk_lambda("y", t, f(b, a)))), a) ==
mk_lambda("x", t, f(Var(1), mk_lambda("y", t, f(b, Var(2))))));
lean_assert(substitute(f(f(f(a))), f(a), b) == f(f(b)));
}
void tst12() {
expr f = constant("f");
expr a = constant("a");
expr x = var(0);
expr t = type(level());
expr F = pi("y", t, lambda("x", t, f(f(f(x,a),constant("10")),x)));
expr f = Const("f");
expr a = Const("a");
expr x = Var(0);
expr t = Type();
expr F = mk_pi("y", t, mk_lambda("x", t, f(f(f(x,a),Const("10")),x)));
expr G = deep_copy(F);
lean_assert(F == G);
lean_assert(!is_eqp(F, G));
@ -344,8 +344,8 @@ void tst12() {
}
void tst13() {
expr f = constant("f");
expr v = var(0);
expr f = Const("f");
expr v = Var(0);
expr a1 = max_sharing(f(v,v));
expr a2 = max_sharing(f(v,v));
lean_assert(!is_eqp(a1, a2));
@ -356,17 +356,17 @@ void tst13() {
}
void tst14() {
expr t0 = type(level());
expr t1 = type(level()+1);
expr t0 = Type();
expr t1 = Type(level()+1);
lean_assert(ty_level(t1) == level()+1);
lean_assert(t0 != t1);
std::cout << t0 << " " << t1 << "\n";
}
void tst15() {
expr t = eq(constant("a"), constant("b"));
expr t = Eq(Const("a"), Const("b"));
std::cout << t << "\n";
expr l = let("a", constant("b"), var(0));
expr l = mk_let("a", Const("b"), Var(0));
std::cout << l << "\n";
lean_assert(closed(l));
}

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

@ -9,24 +9,24 @@ Author: Leonardo de Moura
using namespace lean;
static void tst1() {
expr f = constant("f");
expr a = constant("a");
expr b = constant("b");
expr x = var(0);
expr y = var(1);
expr t = constant("t");
expr F = lambda("_", t, f(x));
lean_assert(has_free_var(lambda("_", t, f(var(1))), 0));
lean_assert(!has_free_var(lambda("_", t, f(var(0))), 1));
lean_assert(!has_free_var(pi("_", t, lambda("_", t, f(var(1)))), 0));
lean_assert(has_free_var(f(var(0)), 0));
lean_assert(has_free_var(f(var(1)), 1));
lean_assert(!has_free_var(f(var(1)), 0));
lean_assert(has_free_var(f(var(1)), 0, 2));
lean_assert(!has_free_var(f(var(1)), 0, 1));
lean_assert(lower_free_vars(f(var(1)), 1) == f(var(0)));
lean_assert(lower_free_vars(lambda("_", t, f(var(2))), 1) == lambda("_", t, f(var(1))));
lean_assert(lower_free_vars(lambda("_", t, f(var(0))), 1) == lambda("_", t, f(var(0))));
expr f = Const("f");
expr a = Const("a");
expr b = Const("b");
expr x = Var(0);
expr y = Var(1);
expr t = Const("t");
expr F = mk_lambda("_", t, f(x));
lean_assert(has_free_var(mk_lambda("_", t, f(Var(1))), 0));
lean_assert(!has_free_var(mk_lambda("_", t, f(Var(0))), 1));
lean_assert(!has_free_var(mk_pi("_", t, mk_lambda("_", t, f(Var(1)))), 0));
lean_assert(has_free_var(f(Var(0)), 0));
lean_assert(has_free_var(f(Var(1)), 1));
lean_assert(!has_free_var(f(Var(1)), 0));
lean_assert(has_free_var(f(Var(1)), 0, 2));
lean_assert(!has_free_var(f(Var(1)), 0, 1));
lean_assert(lower_free_vars(f(Var(1)), 1) == f(Var(0)));
lean_assert(lower_free_vars(mk_lambda("_", t, f(Var(2))), 1) == mk_lambda("_", t, f(Var(1))));
lean_assert(lower_free_vars(mk_lambda("_", t, f(Var(0))), 1) == mk_lambda("_", t, f(Var(0))));
}
int main() {

150
src/tests/kernel/normalize.cpp
View file

@ -18,10 +18,10 @@ expr normalize(expr const & e) {
}
static void eval(expr const & e, environment & env) { std::cout << e << " --> " << normalize(e, env) << "\n"; }
static expr t() { return constant("t"); }
static expr lam(expr const & e) { return lambda("_", t(), e); }
static expr lam(expr const & t, expr const & e) { return lambda("_", t, e); }
static expr v(unsigned i) { return var(i); }
static expr t() { return Const("t"); }
static expr lam(expr const & e) { return mk_lambda("_", t(), e); }
static expr lam(expr const & t, expr const & e) { return mk_lambda("_", t, e); }
static expr v(unsigned i) { return Var(i); }
static expr zero() {
// fun (t : T) (s : t -> t) (z : t) z
return lam(t(), lam(arrow(v(0), v(0)), lam(v(1), v(0))));
@ -30,16 +30,16 @@ static expr one() {
// fun (t : T) (s : t -> t) s
return lam(t(), lam(arrow(v(0), v(0)), v(0)));
}
static expr num() { return constant("num"); }
static expr num() { return Const("num"); }
static expr plus() {
// fun (m n : numeral) (A : Type 0) (f : A -> A) (x : A) => m A f (n A f x).
expr x = v(0), f = v(1), A = v(2), n = v(3), m = v(4);
expr body = m(A, f, n(A, f, x));
return lam(num(), lam(num(), lam(t(), lam(arrow(v(0), v(0)), lam(v(1), body)))));
}
static expr two() { return app(plus(), one(), one()); }
static expr three() { return app(plus(), two(), one()); }
static expr four() { return app(plus(), two(), two()); }
static expr two() { return mk_app({plus(), one(), one()}); }
static expr three() { return mk_app({plus(), two(), one()}); }
static expr four() { return mk_app({plus(), two(), two()}); }
static expr times() {
// fun (m n : numeral) (A : Type 0) (f : A -> A) (x : A) => m A (n A f) x.
expr x = v(0), f = v(1), A = v(2), n = v(3), m = v(4);
@ -80,56 +80,56 @@ unsigned count(expr const & a) {
static void tst_church_numbers() {
environment env;
env.add_var("t", type(level()));
env.add_var("N", type(level()));
env.add_var("z", constant("N"));
env.add_var("s", constant("N"));
expr N = constant("N");
expr z = constant("z");
expr s = constant("s");
std::cout << normalize(app(zero(), N, s, z), env) << "\n";
std::cout << normalize(app(one(), N, s, z), env) << "\n";
std::cout << normalize(app(two(), N, s, z), env) << "\n";
std::cout << normalize(app(four(), N, s, z), env) << "\n";
std::cout << count(normalize(app(four(), N, s, z), env)) << "\n";
lean_assert(count(normalize(app(four(), N, s, z), env)) == 4 + 2);
std::cout << normalize(app(app(times(), four(), four()), N, s, z), env) << "\n";
std::cout << normalize(app(app(power(), two(), four()), N, s, z), env) << "\n";
lean_assert(count(normalize(app(app(power(), two(), four()), N, s, z), env)) == 16 + 2);
std::cout << normalize(app(app(times(), two(), app(power(), two(), four())), N, s, z), env) << "\n";
std::cout << count(normalize(app(app(times(), two(), app(power(), two(), four())), N, s, z), env)) << "\n";
std::cout << count(normalize(app(app(times(), four(), app(power(), two(), four())), N, s, z), env)) << "\n";
lean_assert(count(normalize(app(app(times(), four(), app(power(), two(), four())), N, s, z), env)) == 64 + 2);
expr big = normalize(app(app(power(), two(), app(power(), two(), three())), N, s, z), env);
env.add_var("t", Type());
env.add_var("N", Type());
env.add_var("z", Const("N"));
env.add_var("s", Const("N"));
expr N = Const("N");
expr z = Const("z");
expr s = Const("s");
std::cout << normalize(mk_app(zero(), N, s, z), env) << "\n";
std::cout << normalize(mk_app(one(), N, s, z), env) << "\n";
std::cout << normalize(mk_app(two(), N, s, z), env) << "\n";
std::cout << normalize(mk_app(four(), N, s, z), env) << "\n";
std::cout << count(normalize(mk_app(four(), N, s, z), env)) << "\n";
lean_assert(count(normalize(mk_app(four(), N, s, z), env)) == 4 + 2);
std::cout << normalize(mk_app(mk_app(times(), four(), four()), N, s, z), env) << "\n";
std::cout << normalize(mk_app(mk_app(power(), two(), four()), N, s, z), env) << "\n";
lean_assert(count(normalize(mk_app(mk_app(power(), two(), four()), N, s, z), env)) == 16 + 2);
std::cout << normalize(mk_app(mk_app(times(), two(), mk_app(power(), two(), four())), N, s, z), env) << "\n";
std::cout << count(normalize(mk_app(mk_app(times(), two(), mk_app(power(), two(), four())), N, s, z), env)) << "\n";
std::cout << count(normalize(mk_app(mk_app(times(), four(), mk_app(power(), two(), four())), N, s, z), env)) << "\n";
lean_assert(count(normalize(mk_app(mk_app(times(), four(), mk_app(power(), two(), four())), N, s, z), env)) == 64 + 2);
expr big = normalize(mk_app(mk_app(power(), two(), mk_app(power(), two(), three())), N, s, z), env);
std::cout << count(big) << "\n";
lean_assert(count(big) == 256 + 2);
expr three = app(plus(), two(), one());
lean_assert(count(normalize(app(app(power(), three, three), N, s, z), env)) == 27 + 2);
// expr big2 = normalize(app(app(power(), two(), app(times(), app(plus(), four(), one()), four())), N, s, z), env);
expr three = mk_app(plus(), two(), one());
lean_assert(count(normalize(mk_app(mk_app(power(), three, three), N, s, z), env)) == 27 + 2);
// expr big2 = normalize(mk_app(mk_app(power(), two(), mk_app(times(), mk_app(plus(), four(), one()), four())), N, s, z), env);
// std::cout << count(big2) << "\n";
std::cout << normalize(lam(lam(app(app(times(), four(), four()), N, var(0), z))), env) << "\n";
std::cout << normalize(lam(lam(mk_app(mk_app(times(), four(), four()), N, Var(0), z))), env) << "\n";
}
static void tst1() {
environment env;
env.add_var("t", type(level()));
expr t = type(level());
env.add_var("t", Type());
expr t = Type();
env.add_var("f", arrow(t, t));
expr f = constant("f");
expr f = Const("f");
env.add_var("a", t);
expr a = constant("a");
expr a = Const("a");
env.add_var("b", t);
expr b = constant("b");
expr x = var(0);
expr y = var(1);
eval(app(lambda("x", t, x), a), env);
eval(app(lambda("x", t, x), a, b), env);
eval(lambda("x", t, f(x)), env);
eval(lambda("y", t, lambda("x", t, f(y, x))), env);
eval(app(lambda("x", t,
app(lambda("f", t,
app(var(0), b)),
lambda("g", t, f(var(1))))),
expr b = Const("b");
expr x = Var(0);
expr y = Var(1);
eval(mk_app(mk_lambda("x", t, x), a), env);
eval(mk_app(mk_lambda("x", t, x), a, b), env);
eval(mk_lambda("x", t, f(x)), env);
eval(mk_lambda("y", t, mk_lambda("x", t, f(y, x))), env);
eval(mk_app(mk_lambda("x", t,
mk_app(mk_lambda("f", t,
mk_app(Var(0), b)),
mk_lambda("g", t, f(Var(1))))),
a), env);
expr l01 = lam(v(0)(v(1)));
expr l12 = lam(lam(v(1)(v(2))));
@ -139,61 +139,61 @@ static void tst1() {
static void tst2() {
environment env;
expr t = type(level());
expr t = Type();
env.add_var("f", arrow(t, t));
expr f = constant("f");
expr f = Const("f");
env.add_var("a", t);
expr a = constant("a");
expr a = Const("a");
env.add_var("b", t);
expr b = constant("b");
expr b = Const("b");
env.add_var("h", arrow(t, t));
expr h = constant("h");
expr x = var(0);
expr y = var(1);
expr h = Const("h");
expr x = Var(0);
expr y = Var(1);
lean_assert(normalize(f(x,x), env, extend(context(), name("f"), t, f(a))) == f(f(a), f(a)));
context c1 = extend(extend(context(), name("f"), t, f(a)), name("h"), t, h(x));
expr F1 = normalize(f(x,f(x)), env, c1);
lean_assert(F1 == f(h(f(a)), f(h(f(a)))));
std::cout << F1 << "\n";
expr F2 = normalize(lambda("x", t, f(x, f(y))), env, c1);
expr F2 = normalize(mk_lambda("x", t, f(x, f(y))), env, c1);
std::cout << F2 << "\n";
lean_assert(F2 == lambda("x", t, f(x, f(h(f(a))))));
expr F3 = normalize(lambda("y", t, lambda("x", t, f(x, f(y)))), env, c1);
lean_assert(F2 == mk_lambda("x", t, f(x, f(h(f(a))))));
expr F3 = normalize(mk_lambda("y", t, mk_lambda("x", t, f(x, f(y)))), env, c1);
std::cout << F3 << "\n";
lean_assert(F3 == lambda("y", t, lambda("x", t, f(x, f(y)))));
context c2 = extend(extend(context(), name("foo"), t, lambda("x", t, f(x, a))), name("bla"), t, lambda("z", t, h(x,y)));
expr F4 = normalize(lambda("x", t, f(x, f(y))), env, c2);
lean_assert(F3 == mk_lambda("y", t, mk_lambda("x", t, f(x, f(y)))));
context c2 = extend(extend(context(), name("foo"), t, mk_lambda("x", t, f(x, a))), name("bla"), t, mk_lambda("z", t, h(x,y)));
expr F4 = normalize(mk_lambda("x", t, f(x, f(y))), env, c2);
std::cout << F4 << "\n";
lean_assert(F4 == lambda("x", t, f(x, f(lambda("z", t, h(x,lambda("x", t, f(x, a))))))));
lean_assert(F4 == mk_lambda("x", t, f(x, f(mk_lambda("z", t, h(x,mk_lambda("x", t, f(x, a))))))));
context c3 = extend(context(), name("x"), t);
expr f5 = app(lambda("f", t, lambda("z", t, var(1))), lambda("y", t, var(1)));
expr f5 = mk_app(mk_lambda("f", t, mk_lambda("z", t, Var(1))), mk_lambda("y", t, Var(1)));
expr F5 = normalize(f5, env, c3);
std::cout << f5 << "\n---->\n";
std::cout << F5 << "\n";
lean_assert(F5 == lambda("z", t, lambda("y", t, var(2))));
lean_assert(F5 == mk_lambda("z", t, mk_lambda("y", t, Var(2))));
context c4 = extend(extend(context(), name("x"), t), name("x2"), t);
expr F6 = normalize(app(lambda("f", t, lambda("z1", t, lambda("z2", t, app(var(2), constant("a"))))),
lambda("y", t, app(var(1), var(2), var(0)))), env, c4);
expr F6 = normalize(mk_app(mk_lambda("f", t, mk_lambda("z1", t, mk_lambda("z2", t, mk_app(Var(2), Const("a"))))),
mk_lambda("y", t, mk_app(Var(1), Var(2), Var(0)))), env, c4);
std::cout << F6 << "\n";
lean_assert(F6 == lambda("z1", t, lambda("z2", t, app(var(2), var(3), constant("a")))));
lean_assert(F6 == mk_lambda("z1", t, mk_lambda("z2", t, mk_app(Var(2), Var(3), Const("a")))));
}
static void tst3() {
environment env;
env.add_var("a", bool_type());
expr t1 = constant("a");
expr t2 = constant("a");
expr e = eq(t1, t2);
env.add_var("a", Bool);
expr t1 = Const("a");
expr t2 = Const("a");
expr e = Eq(t1, t2);
std::cout << e << " --> " << normalize(e, env) << "\n";
lean_assert(normalize(e, env) == bool_value(true));
lean_assert(normalize(e, env) == True);
}
static void tst4() {
environment env;
env.add_var("b", type(level()));
expr t1 = let("a", constant("b"), lambda("c", type(), var(1)(var(0))));
env.add_var("b", Type());
expr t1 = mk_let("a", Const("b"), mk_lambda("c", Type(), Var(1)(Var(0))));
std::cout << t1 << " --> " << normalize(t1, env) << "\n";
lean_assert(normalize(t1, env) == lambda("c", type(), constant("b")(var(0))));
lean_assert(normalize(t1, env) == mk_lambda("c", Type(), Const("b")(Var(0))));
}
int main() {

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

@ -14,33 +14,33 @@ using namespace lean;
expr mk_big(expr f, unsigned depth, unsigned val) {
if (depth == 1)
return constant(name(val));
return mk_constant(name(val));
else
return f(mk_big(f, depth - 1, val << 1), mk_big(f, depth - 1, (val << 1) + 1));
}
static void tst1() {
expr f = constant("f");
expr f = Const("f");
expr r = mk_big(f, 16, 0);
expr n = constant(name(0u));
expr n = Const(name(0u));
for (unsigned i = 0; i < 20; i++) {
r = abstract(r, n);
}
}
static void tst2() {
expr r = lambda("x", type(level()), app(var(0), var(1), var(2)));
std::cout << instantiate_with_closed(r, constant("a")) << std::endl;
lean_assert(instantiate_with_closed(r, constant("a")) == lambda("x", type(level()), app(var(0), constant("a"), var(1))));
lean_assert(instantiate_with_closed(instantiate_with_closed(r, constant("a")), constant("b")) ==
lambda("x", type(level()), app(var(0), constant("a"), constant("b"))));
std::cout << instantiate_with_closed(abst_body(r), constant("a")) << std::endl;
lean_assert(instantiate_with_closed(abst_body(r), constant("a")) == app(constant("a"), var(0), var(1)));
std::cout << instantiate(r, var(10)) << std::endl;
lean_assert(instantiate(r, var(10)) == lambda("x", type(level()), app(var(0), var(11), var(1))));
std::cout << pi("_", var(3), var(4)) << std::endl;
std::cout << instantiate(pi("_", var(3), var(4)), var(0)) << std::endl;
lean_assert(instantiate(pi("_", var(3), var(4)), var(0)) == pi("_", var(2), var(3)));
expr r = mk_lambda("x", Type(), mk_app({Var(0), Var(1), Var(2)}));
std::cout << instantiate_with_closed(r, Const("a")) << std::endl;
lean_assert(instantiate_with_closed(r, Const("a")) == mk_lambda("x", Type(), mk_app({Var(0), Const("a"), Var(1)})));
lean_assert(instantiate_with_closed(instantiate_with_closed(r, Const("a")), Const("b")) ==
mk_lambda("x", Type(), mk_app({Var(0), Const("a"), Const("b")})));
std::cout << instantiate_with_closed(abst_body(r), Const("a")) << std::endl;
lean_assert(instantiate_with_closed(abst_body(r), Const("a")) == mk_app({Const("a"), Var(0), Var(1)}));
std::cout << instantiate(r, Var(10)) << std::endl;
lean_assert(instantiate(r, Var(10)) == mk_lambda("x", Type(), mk_app({Var(0), Var(11), Var(1)})));
std::cout << mk_pi("_", Var(3), Var(4)) << std::endl;
std::cout << instantiate(mk_pi("_", Var(3), Var(4)), Var(0)) << std::endl;
lean_assert(instantiate(mk_pi("_", Var(3), Var(4)), Var(0)) == mk_pi("_", Var(2), Var(3)));
}
int main() {

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

@ -19,20 +19,20 @@ using namespace lean;
expr normalize(expr const & e) {
environment env;
env.add_var("a", int_type());
env.add_var("b", int_type());
env.add_var("f", arrow(int_type(), arrow(int_type(), int_type())));
env.add_var("h", arrow(int_type(), arrow(int_type(), int_type())));
env.add_var("a", Int);
env.add_var("b", Int);
env.add_var("f", Int >> (Int >> Int));
env.add_var("h", Int >> (Int >> Int));
return normalize(e, env);
}
static void mk(expr const & a) {
expr b = constant("b");
expr b = Const("b");
for (unsigned i = 0; i < 100; i++) {
expr h = constant("h");
expr h = Const("h");
h = h(a);
for (unsigned j = 0; j < 100; j++)
h = app(h, b);
h = mk_app(h, b);
h = max_sharing(h);
lean_assert(closed(h));
h = normalize(h);
@ -43,8 +43,8 @@ static void mk(expr const & a) {
}
static void tst1() {
expr a = constant("a");
expr f = constant("f");
expr a = Const("a");
expr f = Const("f");
a = f(a, a);
std::vector<std::thread> ts;

60
src/tests/kernel/type_check.cpp
View file

@ -14,49 +14,49 @@ Author: Leonardo de Moura
#include "test.h"
using namespace lean;
expr c(char const * n) { return constant(n); }
expr c(char const * n) { return mk_constant(n); }
static void tst1() {
environment env;
expr t0 = type(level());
expr t0 = Type();
std::cout << infer_type(t0, env) << "\n";
lean_assert(infer_type(t0, env) == type(level()+1));
expr f = pi("_", t0, t0);
lean_assert(infer_type(t0, env) == Type(level()+1));
expr f = mk_pi("_", t0, t0);
std::cout << infer_type(f, env) << "\n";
lean_assert(infer_type(f, env) == type(level()+1));
lean_assert(infer_type(f, env) == Type(level()+1));
level u = env.define_uvar("u", level() + 1);
level v = env.define_uvar("v", level() + 1);
expr g = pi("_", type(u), type(v));
expr g = mk_pi("_", Type(u), Type(v));
std::cout << infer_type(g, env) << "\n";
lean_assert(infer_type(g, env) == type(max(u+1, v+1)));
std::cout << infer_type(type(u), env) << "\n";
lean_assert(infer_type(type(u), env) == type(u+1));
std::cout << infer_type(lambda("x", type(u), var(0)), env) << "\n";
lean_assert(infer_type(lambda("x", type(u), var(0)), env) == pi("_", type(u), type(u)));
std::cout << infer_type(lambda("Nat", type(level()), lambda("n", var(0), var(0))), env) << "\n";
lean_assert(infer_type(g, env) == Type(max(u+1, v+1)));
std::cout << infer_type(Type(u), env) << "\n";
lean_assert(infer_type(Type(u), env) == Type(u+1));
std::cout << infer_type(mk_lambda("x", Type(u), Var(0)), env) << "\n";
lean_assert(infer_type(mk_lambda("x", Type(u), Var(0)), env) == mk_pi("_", Type(u), Type(u)));
std::cout << infer_type(mk_lambda("Nat", Type(), mk_lambda("n", Var(0), Var(0))), env) << "\n";
expr nat = c("nat");
expr T = fun("nat", type(level()),
fun("+", arrow(nat, arrow(nat, nat)),
fun("m", nat, app(c("+"), c("m"), c("m")))));
expr T = Fun("nat", Type(),
Fun("+", arrow(nat, arrow(nat, nat)),
Fun("m", nat, mk_app({c("+"), c("m"), c("m")}))));
std::cout << T << "\n";
std::cout << infer_type(T, env) << "\n";
std::cout << Fun("nat", type(level()), arrow(arrow(nat, arrow(nat, nat)), arrow(nat, nat))) << "\n";
lean_assert(infer_type(T, env) == Fun("nat", type(level()), arrow(arrow(nat, arrow(nat, nat)), arrow(nat, nat))));
std::cout << Pi("nat", Type(), arrow(arrow(nat, arrow(nat, nat)), arrow(nat, nat))) << "\n";
lean_assert(infer_type(T, env) == Pi("nat", Type(), arrow(arrow(nat, arrow(nat, nat)), arrow(nat, nat))));
}
static void tst2() {
try{
environment env;
level l1 = env.define_uvar("l1", level() + 1);
expr t0 = type(level());
expr t1 = type(l1);
expr t0 = Type();
expr t1 = Type(l1);
expr F =
fun("Nat", t0,
fun("Vec", arrow(c("Nat"), t0),
fun("n", c("Nat"),
fun("len", arrow(app(c("Vec"), c("n")), c("Nat")),
fun("v", app(c("Vec"), c("n")),
app(c("len"), c("v")))))));
Fun("Nat", t0,
Fun("Vec", arrow(c("Nat"), t0),
Fun("n", c("Nat"),
Fun("len", arrow(mk_app({c("Vec"), c("n")}), c("Nat")),
Fun("v", mk_app({c("Vec"), c("n")}),
mk_app({c("len"), c("v")}))))));
std::cout << F << "\n";
std::cout << infer_type(F, env) << "\n";
}
@ -67,17 +67,17 @@ static void tst2() {
static void tst3() {
environment env;
expr f = fun("a", bool_type(), eq(constant("a"), bool_value(true)));
expr f = Fun("a", Bool, Eq(Const("a"), True));
std::cout << infer_type(f, env) << "\n";
lean_assert(infer_type(f, env) == arrow(bool_type(), bool_type()));
expr t = let("a", bool_value(true), var(0));
lean_assert(infer_type(f, env) == arrow(Bool, Bool));
expr t = mk_let("a", True, Var(0));
std::cout << infer_type(t, env) << "\n";
}
static void tst4() {
environment env;
expr a = eq(int_value(1), int_value(2));
expr pr = lambda("x", a, var(0));
expr a = Eq(iVal(1), iVal(2));
expr pr = mk_lambda("x", a, Var(0));
std::cout << infer_type(pr, env) << "\n";
}