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

Modify type checker. Now, it only accepts builtin values that have been declared in the environment. The idea is to be able to track which classes of builtin values have been used in a given environment. We want to be able to quantify the size of the trusted code base for a particular development.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-04 08:30:04 -07:00
parent 9f34f96b08
commit e955c054ca
21 changed files with 236 additions and 110 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -248,14 +248,8 @@ class parser::imp {
/** \brief Initialize \c m_builtins table with Lean builtin symbols that do not have notation associated with them. */
void init_builtins() {
m_builtins["Bool"] = Bool;
m_builtins["true"] = True;
m_builtins["false"] = False;
m_builtins["\u22A4"] = True;
m_builtins["\u22A5"] = False;
m_builtins["Nat"] = Nat;
m_builtins["Int"] = Int;
m_builtins["Real"] = Real;
}
unsigned parse_unsigned(char const * msg) {
@ -576,6 +570,8 @@ class parser::imp {
} else {
return mk_constant(obj.get_name());
}
} if (k == object_kind::Builtin) {
return obj.get_value();
} else {
throw parser_error(sstream() << "invalid object reference, object '" << id << "' is not an expression.", p);
}

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

@ -1166,6 +1166,12 @@ class pp_formatter_cell : public formatter_cell {
return r;
}
format pp_builtin_set(object const & obj, options const & opts) {
char const * kwd = obj.keyword();
name const & n = obj.get_name();
return format{highlight_command(format(kwd)), space(), format(n)};
}
format pp_definition(object const & obj, options const & opts) {
return pp_compact_definition(obj.keyword(), obj.get_name(), obj.get_type(), obj.get_value(), opts);
}
@ -1224,6 +1230,8 @@ public:
case object_kind::UVarDeclaration: return pp_uvar_decl(obj, opts);
case object_kind::Postulate: return pp_postulate(obj, opts);
case object_kind::Definition: return pp_definition(obj, opts);
case object_kind::Builtin: return pp_postulate(obj, opts);
case object_kind::BuiltinSet: return pp_builtin_set(obj, opts);
case object_kind::Neutral:
if (dynamic_cast<notation_declaration const *>(obj.cell())) {
return pp_notation_decl(obj, opts);

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

@ -353,6 +353,29 @@ void add_arith_theory(environment & env) {
expr x = Const("x");
expr y = Const("y");
env.add_builtin(Nat);
env.add_builtin_set(nVal(0));
env.add_builtin(mk_nat_add_fn());
env.add_builtin(mk_nat_mul_fn());
env.add_builtin(mk_nat_le_fn());
env.add_builtin(Int);
env.add_builtin_set(iVal(0));
env.add_builtin(mk_int_add_fn());
env.add_builtin(mk_int_mul_fn());
env.add_builtin(mk_int_div_fn());
env.add_builtin(mk_int_le_fn());
env.add_builtin(Real);
env.add_builtin_set(rVal(0));
env.add_builtin(mk_real_add_fn());
env.add_builtin(mk_real_mul_fn());
env.add_builtin(mk_real_div_fn());
env.add_builtin(mk_real_le_fn());
env.add_builtin(mk_nat_to_int_fn());
env.add_builtin(mk_int_to_real_fn());
env.add_definition(nat_ge_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, nLe(y, x)));
env.add_definition(nat_lt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(y, x))));
env.add_definition(nat_gt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(x, y))));

28
src/kernel/builtin.cpp
View file

@ -45,7 +45,6 @@ expr mk_bin_lop(expr const & op, expr const & unit, std::initializer_list<expr>
return mk_bin_lop(op, unit, l.size(), l.begin());
}
// =======================================
// Bultin universe variables m and u
static level m_lvl(name("M"));
@ -121,19 +120,19 @@ bool is_false(expr const & e) {
// =======================================
// If-then-else builtin operator
static name g_ite_name("ite");
static format g_ite_fmt(g_ite_name);
class ite_fn_value : public value {
static name g_if_name("if");
static format g_if_fmt(g_if_name);
class if_fn_value : public value {
expr m_type;
public:
ite_fn_value() {
if_fn_value() {
expr A = Const("A");
// Pi (A: Type), bool -> A -> A -> A
m_type = Pi({A, TypeU}, Bool >> (A >> (A >> A)));
}
virtual ~ite_fn_value() {}
virtual ~if_fn_value() {}
virtual expr get_type() const { return m_type; }
virtual name get_name() const { return g_ite_name; }
virtual name get_name() const { return g_if_name; }
virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
if (num_args == 5 && is_bool_value(args[2])) {
if (to_bool(args[2]))
@ -149,10 +148,9 @@ public:
}
}
};
MK_BUILTIN(ite_fn, ite_fn_value);
MK_BUILTIN(if_fn, if_fn_value);
// =======================================
MK_CONSTANT(if_fn, name("if"));
MK_CONSTANT(implies_fn, name("implies"));
MK_CONSTANT(iff_fn, name("iff"));
MK_CONSTANT(and_fn, name("and"));
@ -174,6 +172,7 @@ MK_CONSTANT(imp_antisym_fn, name("ImpAntisym"));
void add_basic_theory(environment & env) {
env.add_uvar(uvar_name(m_lvl), level() + LEAN_DEFAULT_LEVEL_SEPARATION);
env.add_uvar(uvar_name(u_lvl), m_lvl + LEAN_DEFAULT_LEVEL_SEPARATION);
expr p1 = Bool >> Bool;
expr p2 = Bool >> p1;
expr f = Const("f");
@ -191,18 +190,19 @@ void add_basic_theory(environment & env) {
expr H = Const("H");
expr H1 = Const("H1");
expr H2 = Const("H2");
expr ite = mk_ite_fn();
// if(A, x, y, z) := ite A x y z
env.add_definition(if_fn_name, to_value(ite).get_type(), ite);
env.add_builtin(mk_bool_type());
env.add_builtin(mk_bool_value(true));
env.add_builtin(mk_bool_value(false));
env.add_builtin(mk_if_fn());
// implies(x, y) := ite x y True
// implies(x, y) := if x y True
env.add_definition(implies_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, y, True)));
// iff(x, y) := x = y
env.add_definition(iff_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Eq(x, y)));
// not(x) := ite x False True
// not(x) := if x False True
env.add_definition(not_fn_name, p1, Fun({x, Bool}, bIf(x, False, True)));
// or(x, y) := Not(x) => y

24
src/kernel/environment.cpp
View file

@ -234,6 +234,22 @@ struct environment::imp {
check_type(n, t, v, env);
}
/** \brief Add a new builtin value to this environment */
void add_builtin(expr const & n, environment const & env) {
if (!is_value(n))
throw invalid_builtin_value_declaration(env, n);
check_name(to_value(n).get_name(), env);
register_named_object(mk_builtin(n));
}
/** \brief Add a new builtin value set to this environment */
void add_builtin_set(expr const & r, environment const & env) {
if (!is_value(r))
throw invalid_builtin_value_declaration(env, r);
check_name(to_value(r).get_name(), env);
register_named_object(mk_builtin_set(r));
}
/** \brief Add new definition. */
void add_definition(name const & n, expr const & t, expr const & v, bool opaque, environment const & env) {
check_new_definition(n, t, v, env);
@ -378,6 +394,14 @@ level environment::get_uvar(name const & n) const {
return m_imp->get_uvar(n, *this);
}
void environment::add_builtin(expr const & v) {
return m_imp->add_builtin(v, *this);
}
void environment::add_builtin_set(expr const & r) {
return m_imp->add_builtin_set(r, *this);
}
void environment::add_definition(name const & n, expr const & t, expr const & v, bool opaque) {
m_imp->add_definition(n, t, v, opaque, *this);
}

21
src/kernel/environment.h
View file

@ -75,6 +75,27 @@ public:
// =======================================
// Environment Objects
/**
\brief Add builtin value to the environment.
\pre is_value(v)
*/
void add_builtin(expr const & v);
/**
\brief Add a builtin value set to the environment.
The set is registered by providing a representative of the set.
Each builtin set of values is implemented by a C++ class.
The environment will only accept object of the same class of
the representative. This functionality is used to support
infinite set of builtin values such as the natural numbers.
\pre is_value(r);
*/
void add_builtin_set(expr const & r);
/**
\brief Add a new definition n : t := v.
It throws an exception if v does not have type t.

23
src/kernel/kernel_exception.h
View file

@ -170,4 +170,27 @@ public:
expr const & get_value_type() const { return m_value_type; }
virtual char const * what() const noexcept { return "definition type mismatch"; }
};
/**
\brief Invalid builtin value declaration.
*/
class invalid_builtin_value_declaration : public kernel_exception {
expr m_expr;
public:
invalid_builtin_value_declaration(environment const & env, expr const & e):kernel_exception(env), m_expr(e) {}
virtual ~invalid_builtin_value_declaration() {}
virtual char const * what() const noexcept { return "invalid builtin value declaration, expression is not a builtin value"; }
};
/**
\brief Exception used to report that a builtin value is not
declared in the environment.
*/
class invalid_builtin_value_reference : public kernel_exception {
expr m_expr;
public:
invalid_builtin_value_reference(environment const & env, expr const & e):kernel_exception(env), m_expr(e) {}
virtual ~invalid_builtin_value_reference() {}
virtual char const * what() const noexcept { return "invalid builtin value reference, this kind of builtin value was not declared in the environment"; }
};
}

88
src/kernel/object.cpp
View file

@ -9,16 +9,6 @@ Author: Leonardo de Moura
namespace lean {
neutral_object_cell::neutral_object_cell():object_cell(object_kind::Neutral) {}
neutral_object_cell::~neutral_object_cell() {}
bool neutral_object_cell::has_name() const { return false; }
name const & neutral_object_cell::get_name() const { lean_unreachable(); return name::anonymous(); }
bool neutral_object_cell::has_cnstr_level() const { return false; }
level neutral_object_cell::get_cnstr_level() const { lean_unreachable(); return level(); }
bool neutral_object_cell::has_type() const { return false; }
expr const & neutral_object_cell::get_type() const { lean_unreachable(); return expr::null(); }
bool neutral_object_cell::is_definition() const { return false; }
bool neutral_object_cell::is_opaque() const { lean_unreachable(); return false; }
expr const & neutral_object_cell::get_value() const { lean_unreachable(); return expr::null(); }
/**
\brief Named kernel objects.
@ -31,8 +21,8 @@ public:
named_object_cell(object_kind k, name const & n):object_cell(k), m_name(n) {}
virtual ~named_object_cell() {}
virtual bool has_name() const { return true; }
virtual name const & get_name() const { return m_name; }
virtual bool has_name() const { return true; }
virtual name get_name() const { return m_name; }
};
/**
@ -45,18 +35,55 @@ public:
named_object_cell(object_kind::UVarDeclaration, n), m_level(l) {}
virtual ~uvar_declaration_object_cell() {}
virtual bool has_cnstr_level() const { return true; }
virtual level get_cnstr_level() const { return m_level; }
bool has_type() const { return false; }
expr const & get_type() const { lean_unreachable(); return expr::null(); }
bool is_definition() const { return false; }
bool is_opaque() const { lean_unreachable(); return false; }
expr const & get_value() const { lean_unreachable(); return expr::null(); }
virtual bool has_cnstr_level() const { return true; }
virtual level get_cnstr_level() const { return m_level; }
virtual char const * keyword() const { return "Universe"; }
};
/**
\brief Base class for Axioms and Variable declarations.
*/
class builtin_object_cell : public object_cell {
expr m_value;
public:
builtin_object_cell(expr const & v):
object_cell(object_kind::Builtin), m_value(v) { lean_assert(is_value(v)); }
virtual ~builtin_object_cell() {}
virtual bool has_name() const { return true; }
virtual name get_name() const { return to_value(m_value).get_name(); }
virtual bool has_type() const { return true; }
virtual expr get_type() const { return to_value(m_value).get_type(); }
virtual bool is_definition() const { return true; }
virtual bool is_opaque() const { return false; }
virtual expr get_value() const { return m_value; }
virtual char const * keyword() const { return "Builtin"; }
virtual bool is_builtin() const { return true; }
};
/**
\brief Base class for capturing a set of builtin objects such as
a) the natural numbers 0, 1, 2, ...
b) the integers 0, -1, 1, -2, 2, ...
c) the reals
d) ...
This object represents an infinite set of declarations.
This is just a markup to sign that an environment depends on a
particular builtin set of values.
*/
class builtin_set_object_cell : public object_cell {
// The representative is only used to test if a builtin value
// is in the same C++ class of the representative.
expr m_representative;
public:
builtin_set_object_cell(expr const & r):object_cell(object_kind::BuiltinSet), m_representative(r) { lean_assert(is_value(r)); }
virtual ~builtin_set_object_cell() {}
virtual bool has_name() const { return true; }
virtual name get_name() const { return to_value(m_representative).get_name(); }
virtual bool is_builtin_set() const { return true; }
virtual bool in_builtin_set(expr const & v) const { return is_value(v) && typeid(to_value(v)) == typeid(to_value(m_representative)); }
virtual char const * keyword() const { return "BuiltinSet"; }
};
/**
\brief Named (and typed) kernel objects.
*/
@ -67,11 +94,8 @@ public:
named_object_cell(k, n), m_type(t) {}
virtual ~named_typed_object_cell() {}
virtual bool has_type() const { return true; }
virtual expr const & get_type() const { return m_type; }
virtual bool has_cnstr_level() const { return false; }
virtual level get_cnstr_level() const { lean_unreachable(); return level(); }
virtual bool has_type() const { return true; }
virtual expr get_type() const { return m_type; }
};
/**
@ -81,10 +105,6 @@ class postulate_object_cell : public named_typed_object_cell {
public:
postulate_object_cell(name const & n, expr const & t):
named_typed_object_cell(object_kind::Postulate, n, t) {}
bool is_definition() const { return false; }
bool is_opaque() const { lean_unreachable(); return false; }
expr const & get_value() const { lean_unreachable(); return expr::null(); }
};
/**
@ -118,9 +138,9 @@ public:
named_typed_object_cell(object_kind::Definition, n, t), m_value(v), m_opaque(opaque) {}
virtual ~definition_object_cell() {}
bool is_definition() const { return true; }
bool is_opaque() const { return m_opaque; }
expr const & get_value() const { return m_value; }
virtual bool is_definition() const { return true; }
virtual bool is_opaque() const { return m_opaque; }
virtual expr get_value() const { return m_value; }
virtual char const * keyword() const { return "Definition"; }
};
@ -140,6 +160,8 @@ object mk_definition(name const & n, expr const & t, expr const & v, bool opaque
object mk_theorem(name const & n, expr const & t, expr const & v) { return object(new theorem_object_cell(n, t, v)); }
object mk_axiom(name const & n, expr const & t) { return object(new axiom_object_cell(n, t)); }
object mk_var_decl(name const & n, expr const & t) { return object(new variable_decl_object_cell(n, t)); }
object mk_builtin(expr const & v) { return object(new builtin_object_cell(v)); }
object mk_builtin_set(expr const & r) { return object(new builtin_set_object_cell(r)); }
static object g_null_object;

51
src/kernel/object.h
View file

@ -14,7 +14,7 @@ Author: Leonardo de Moura
frontend may need to create new objects for bookkeeping.
*/
namespace lean {
enum class object_kind { UVarDeclaration, Definition, Postulate, Neutral };
enum class object_kind { UVarDeclaration, Definition, Postulate, Builtin, BuiltinSet, Neutral };
class object_cell {
void dealloc() { delete this; }
@ -33,30 +33,34 @@ public:
virtual char const * keyword() const = 0;
/** \brief Return true iff object has a name. */
virtual bool has_name() const = 0;
virtual bool has_name() const { return false; }
/** \brief Return object name. \pre has_name() */
virtual name const & get_name() const = 0;
virtual name get_name() const { lean_unreachable(); return name(); }
/** \brief Has constraint level associated with it (for universal variables). */
virtual bool has_cnstr_level() const = 0;
virtual bool has_cnstr_level() const { return false; }
/** \brief Return the constraint level associated with the object. */
virtual level get_cnstr_level() const = 0;
virtual level get_cnstr_level() const { lean_unreachable(); return level(); }
/** \brief Return true iff object has a type. */
virtual bool has_type() const = 0;
virtual bool has_type() const { return false; }
/** \brief Return object type. \pre has_type() */
virtual expr const & get_type() const = 0;
virtual expr get_type() const { lean_unreachable(); return expr(); }
/** \brief Return true iff object is a definition */
virtual bool is_definition() const = 0;
virtual bool is_definition() const { return false; }
/** \brief Return true iff the definition is opaque. \pre is_definition() */
virtual bool is_opaque() const = 0;
virtual bool is_opaque() const { lean_unreachable(); return false; }
/** \brief Return object value. \pre is_definition() */
virtual expr const & get_value() const = 0;
virtual expr get_value() const { lean_unreachable(); return expr(); }
virtual bool is_axiom() const { return false; }
virtual bool is_builtin() const { return false; }
virtual bool is_builtin_set() const { return false; }
virtual bool is_theorem() const { return false; }
virtual bool is_var_decl() const { return false; }
virtual bool in_builtin_set(expr const & v) const { return false; }
};
/**
@ -67,20 +71,6 @@ public:
class neutral_object_cell : public object_cell {
public:
neutral_object_cell();
virtual ~neutral_object_cell();
virtual bool has_name() const;
virtual name const & get_name() const;
virtual bool has_cnstr_level() const;
virtual level get_cnstr_level() const;
virtual bool has_type() const;
virtual expr const & get_type() const;
virtual bool is_definition() const;
virtual bool is_opaque() const;
virtual expr const & get_value() const;
};
/**
@ -115,25 +105,32 @@ public:
friend object mk_axiom(name const & n, expr const & t);
friend object mk_var_decl(name const & n, expr const & t);
friend object mk_neutral(neutral_object_cell * c);
friend object mk_builtin(expr const & v);
friend object mk_builtin_set(expr const & r);
char const * keyword() const { return m_ptr->keyword(); }
bool has_name() const { return m_ptr->has_name(); }
name const & get_name() const { return m_ptr->get_name(); }
name get_name() const { return m_ptr->get_name(); }
bool has_type() const { return m_ptr->has_type(); }
bool has_cnstr_level() const { return m_ptr->has_cnstr_level(); }
level get_cnstr_level() const { return m_ptr->get_cnstr_level(); }
expr const & get_type() const { return m_ptr->get_type(); }
expr get_type() const { return m_ptr->get_type(); }
bool is_definition() const { return m_ptr->is_definition(); }
bool is_opaque() const { return m_ptr->is_opaque(); }
expr const & get_value() const { return m_ptr->get_value(); }
expr get_value() const { return m_ptr->get_value(); }
bool is_axiom() const { return m_ptr->is_axiom(); }
bool is_theorem() const { return m_ptr->is_theorem(); }
bool is_var_decl() const { return m_ptr->is_var_decl(); }
bool is_builtin() const { return m_ptr->is_builtin(); }
bool is_builtin_set() const { return m_ptr->is_builtin_set(); }
bool in_builtin_set(expr const & e) const { return m_ptr->in_builtin_set(e); }
object_cell const * cell() const { return m_ptr; }
};
object mk_uvar_decl(name const & n, level const & l);
object mk_builtin(expr const & v);
object mk_builtin_set(expr const & r);
object mk_definition(name const & n, expr const & t, expr const & v, bool opaque);
object mk_theorem(name const & n, expr const & t, expr const & v);
object mk_axiom(name const & n, expr const & t);

12
src/kernel/type_checker.cpp
View file

@ -139,10 +139,18 @@ public:
}
break;
}
case expr_kind::Value:
r = to_value(e).get_type();
case expr_kind::Value: {
// Check if the builtin value (or its set) is declared in the environment.
name const & n = to_value(e).get_name();
object const & obj = m_env.get_object(n);
if (obj && ((obj.is_builtin() && obj.get_value() == e) || (obj.is_builtin_set() && obj.in_builtin_set(e)))) {
r = to_value(e).get_type();
} else {
throw invalid_builtin_value_reference(m_env, e);
}
break;
}
}
if (shared) {
m_cache.insert(e, r);

4
src/library/printer.cpp
View file

@ -184,8 +184,10 @@ std::ostream & operator<<(std::ostream & out, object const & obj) {
out << obj.get_name() << " >= " << obj.get_cnstr_level(); break;
case object_kind::Postulate:
out << obj.get_name() << " : " << obj.get_type(); break;
case object_kind::Definition:
case object_kind::Definition: case object_kind::Builtin:
out << obj.get_name() << " : " << obj.get_type() << " :=\n " << obj.get_value(); break;
case object_kind::BuiltinSet:
out << obj.get_name(); break;
case object_kind::Neutral:
break;
}

20
src/tests/frontends/lean/implicit_args.cpp
View file

@ -71,10 +71,10 @@ static void tst1() {
expr F = Const("F");
expr g = Const("g");
expr a = Const("a");
expr Nat = Const("Nat");
expr Real = Const("Real");
env.add_var("Nat", Type());
env.add_var("Real", Type());
expr Nat = Const("N");
expr Real = Const("R");
env.add_var("N", Type());
env.add_var("R", Type());
env.add_var("F", Pi({{A, Type()}, {B, Type()}, {g, A >> B}}, A));
env.add_var("f", Nat >> Real);
expr f = Const("f");
@ -109,8 +109,8 @@ static void tst2() {
static void tst3() {
frontend env;
expr Nat = Const("Nat");
env.add_var("Nat", Type());
expr Nat = Const("N");
env.add_var("N", Type());
env.add_var("vec", Nat >> Type());
expr n = Const("n");
expr vec = Const("vec");
@ -139,8 +139,8 @@ static void tst3() {
static void tst4() {
frontend env;
expr Nat = Const("Nat");
env.add_var("Nat", Type());
expr Nat = Const("N");
env.add_var("N", Type());
expr R = Const("R");
env.add_var("R", Type());
env.add_var("a", Nat);
@ -167,8 +167,8 @@ static void tst5() {
expr b = Const("b");
expr f = Const("f");
expr g = Const("g");
expr Nat = Const("Nat");
env.add_var("Nat", Type());
expr Nat = Const("N");
env.add_var("N", Type());
env.add_var("f", Pi({{A,Type()},{a,A},{b,A}}, A));
env.add_var("g", Nat >> Nat);
success(Fun({{a,_},{b,_}},g(f(_,a,b))),

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

@ -17,7 +17,7 @@ Author: Leonardo de Moura
using namespace lean;
static void tst1() {
environment env;
environment env = mk_toplevel();
expr e = mk_int_value(mpz(10));
lean_assert(is_int_value(e));
lean_assert(infer_type(e, env) == Int);
@ -25,7 +25,7 @@ static void tst1() {
}
static void tst2() {
environment env;
environment env = mk_toplevel();
expr e = iAdd(iVal(10), iVal(30));
std::cout << e << "\n";
std::cout << normalize(e, env) << "\n";
@ -41,7 +41,7 @@ static void tst2() {
}
static void tst3() {
environment env;
environment env = mk_toplevel();
expr e = iMul(iVal(10), iVal(30));
std::cout << e << "\n";
std::cout << normalize(e, env) << "\n";
@ -73,7 +73,7 @@ static void tst4() {
}
static void tst5() {
environment env;
environment env = mk_toplevel();
env.add_var(name("a"), Int);
expr e = Eq(iVal(3), iVal(4));
std::cout << e << " --> " << normalize(e, env) << "\n";

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

@ -62,7 +62,7 @@ static void tst2() {
}
static void tst3() {
environment env;
environment env = mk_toplevel();
try {
env.add_definition("a", Int, Const("a"));
lean_unreachable();
@ -123,7 +123,7 @@ static void tst4() {
}
static void tst5() {
environment env;
environment env = mk_toplevel();
env.add_definition("a", Int, iVal(1), true); // add opaque definition
try {
std::cout << infer_type(iAdd(Const("a"), Int), env) << "\n";
@ -134,7 +134,7 @@ static void tst5() {
}
static void tst6() {
environment env;
environment env = mk_toplevel();
level u = env.add_uvar("u", level() + 1);
level w = env.add_uvar("w", u + 1);
env.add_var("f", mk_arrow(Type(u), Type(u)));

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

@ -15,6 +15,7 @@ Author: Leonardo de Moura
#include "expr_sets.h"
#include "abstract.h"
#include "kernel_exception.h"
#include "toplevel.h"
#include "printer.h"
using namespace lean;
@ -185,7 +186,7 @@ static void tst2() {
}
static void tst3() {
environment env;
environment env = mk_toplevel();
env.add_var("a", Bool);
expr t1 = Const("a");
expr t2 = Const("a");
@ -212,7 +213,7 @@ static expr mk_big(unsigned depth) {
static void tst5() {
#ifndef __APPLE__
expr t = mk_big(18);
environment env;
environment env = mk_toplevel();
env.add_var("f", Bool >> (Bool >> Bool));
env.add_var("a", Bool);
normalizer proc(env);

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

@ -13,12 +13,13 @@ Author: Leonardo de Moura
#include "deep_copy.h"
#include "abstract.h"
#include "normalizer.h"
#include "toplevel.h"
#include "arith.h"
#include "test.h"
using namespace lean;
expr normalize(expr const & e) {
environment env;
environment env = mk_toplevel();
env.add_var("a", Int);
env.add_var("b", Int);
env.add_var("f", Int >> (Int >> Int));

6
src/tests/kernel/type_checker.cpp
View file

@ -73,7 +73,7 @@ static void tst2() {
}
static void tst3() {
environment env;
environment env = mk_toplevel();
expr f = Fun("a", Bool, Eq(Const("a"), True));
std::cout << infer_type(f, env) << "\n";
lean_assert(infer_type(f, env) == mk_arrow(Bool, Bool));
@ -82,7 +82,7 @@ static void tst3() {
}
static void tst4() {
environment env;
environment env = mk_toplevel();
expr a = Eq(iVal(1), iVal(2));
expr pr = mk_lambda("x", a, Var(0));
std::cout << infer_type(pr, env) << "\n";
@ -218,7 +218,7 @@ static expr mk_big(unsigned depth) {
static void tst12() {
#ifndef __APPLE__
expr t = mk_big(18);
environment env;
environment env = mk_toplevel();
env.add_var("f", Int >> (Int >> Int));
env.add_var("a", Int);
type_checker checker(env);

2
tests/lean/arith7.lean.expected.out
View file

@ -6,7 +6,7 @@
2
⊤
Assumed: y
ite Int (0 ≤ -3 + y) (-3 + y) (-1 * (-3 + y))
if Int (0 ≤ -3 + y) (-3 + y) (-1 * (-3 + y))
| x + y | > x
Set: lean::pp::notation
Int::gt (Int::abs (Int::add x y)) x

2
tests/lean/tst1.lean.expected.out
View file

@ -46,4 +46,4 @@ map normal form -->
f (v1 i H) (v2 i H)
update normal form -->
λ (A : Type) (n : N) (v : Π (i : N) (H : i < n), A) (i : N) (d : A) (j : N) (H : j < n), ite A (j = i) d (v j H)
λ (A : Type) (n : N) (v : Π (i : N) (H : i < n), A) (i : N) (d : A) (j : N) (H : j < n), if A (j = i) d (v j H)

2
tests/lean/tst10.lean.expected.out
View file

@ -15,7 +15,7 @@ a ∨ b
a ∨ a ∨ b
a ⇒ b ⇒ a
Bool
ite Bool a a ⊤
if Bool a a ⊤
a
Assumed: H1
Assumed: H2

2
tests/lean/tst17.lean.expected.out
View file

@ -5,6 +5,6 @@
∀ a b : Type, ∃ c : Type, (g a b) = (f c)
Bool
(λ a : Type,
(λ b : Type, ite Bool ((λ x : Type, ite Bool ((g a b) = (f x)) ⊥ ⊤) = (λ x : Type, ⊤)) ⊥ ⊤) =
(λ b : Type, if Bool ((λ x : Type, if Bool ((g a b) = (f x)) ⊥ ⊤) = (λ x : Type, ⊤)) ⊥ ⊤) =
(λ x : Type, ⊤)) =
(λ x : Type, ⊤)