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

refactor(kernel): rename var_decl to constant_assumption

Browse source 
Motivation: it matches the notation used to declare it.
This commit is contained in:
Leonardo de Moura 2014-10-02 16:54:56 -07:00
parent 4946f55290
commit bf081ed431
48 changed files with 156 additions and 161 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/decl_cmds.cpp
View file

@ -83,7 +83,7 @@ static environment declare_var(parser & p, environment env,
env = module::add(env, check(env, mk_axiom(full_n, ls, type)));
p.add_decl_index(full_n, pos, get_axiom_tk(), type);
} else {
env = module::add(env, check(env, mk_var_decl(full_n, ls, type)));
env = module::add(env, check(env, mk_constant_assumption(full_n, ls, type)));
p.add_decl_index(full_n, pos, get_variable_tk(), type);
}
if (!ns.is_anonymous())

2
src/frontends/lean/inductive_cmd.cpp
View file

@ -473,7 +473,7 @@ struct inductive_cmd_fn {
for (auto const & d : decls) {
name d_name; expr d_type;
std::tie(d_name, d_type, std::ignore) = d;
m_env = m_env.add(check(m_env, mk_var_decl(d_name, ls, d_type)));
m_env = m_env.add(check(m_env, mk_constant_assumption(d_name, ls, d_type)));
}
m_tc = mk_type_checker(m_env, m_p.mk_ngen(), false);
}

2
src/frontends/lean/structure_cmd.cpp
View file

@ -191,7 +191,7 @@ struct structure_cmd_fn {
}
void add_tmp_record_decl() {
m_env = m_env.add(check(m_env, mk_var_decl(m_name, to_list(m_level_names.begin(), m_level_names.end()), m_type)));
m_env = m_env.add(check(m_env, mk_constant_assumption(m_name, to_list(m_level_names.begin(), m_level_names.end()), m_type)));
}
levels to_levels(buffer<name> const & lvl_names) {

10
src/kernel/declaration.cpp
View file

@ -49,10 +49,10 @@ declaration::~declaration() { if (m_ptr) m_ptr->dec_ref(); }
declaration & declaration::operator=(declaration const & s) { LEAN_COPY_REF(s); }
declaration & declaration::operator=(declaration && s) { LEAN_MOVE_REF(s); }
bool declaration::is_definition() const { return static_cast<bool>(m_ptr->m_value); }
bool declaration::is_var_decl() const { return !is_definition(); }
bool declaration::is_axiom() const { return is_var_decl() && m_ptr->m_theorem; }
bool declaration::is_theorem() const { return is_definition() && m_ptr->m_theorem; }
bool declaration::is_definition() const { return static_cast<bool>(m_ptr->m_value); }
bool declaration::is_constant_assumption() const { return !is_definition(); }
bool declaration::is_axiom() const { return is_constant_assumption() && m_ptr->m_theorem; }
bool declaration::is_theorem() const { return is_definition() && m_ptr->m_theorem; }
name const & declaration::get_name() const { return m_ptr->m_name; }
level_param_names const & declaration::get_univ_params() const { return m_ptr->m_params; }
@ -87,7 +87,7 @@ declaration mk_theorem(name const & n, level_param_names const & params, expr co
declaration mk_axiom(name const & n, level_param_names const & params, expr const & t) {
return declaration(new declaration::cell(n, params, t, true));
}
declaration mk_var_decl(name const & n, level_param_names const & params, expr const & t) {
declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t) {
return declaration(new declaration::cell(n, params, t, false));
}

6
src/kernel/declaration.h
View file

@ -57,7 +57,7 @@ public:
bool is_definition() const;
bool is_axiom() const;
bool is_theorem() const;
bool is_var_decl() const;
bool is_constant_assumption() const;
name const & get_name() const;
level_param_names const & get_univ_params() const;
@ -75,7 +75,7 @@ public:
unsigned weight, module_idx mod_idx, bool use_conv_opt);
friend declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v, module_idx mod_idx);
friend declaration mk_axiom(name const & n, level_param_names const & params, expr const & t);
friend declaration mk_var_decl(name const & n, level_param_names const & params, expr const & t);
friend declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t);
};
inline optional<declaration> none_declaration() { return optional<declaration>(); }
@ -88,7 +88,7 @@ declaration mk_definition(environment const & env, name const & n, level_param_n
bool opaque = false, module_idx mod_idx = 0, bool use_conv_opt = true);
declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v, module_idx mod_idx = 0);
declaration mk_axiom(name const & n, level_param_names const & params, expr const & t);
declaration mk_var_decl(name const & n, level_param_names const & params, expr const & t);
declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t);
void initialize_declaration();
void finalize_declaration();

6
src/kernel/inductive/inductive.cpp
View file

@ -290,7 +290,7 @@ struct add_inductive_fn {
/** \brief Add all datatype declarations to environment. */
void declare_inductive_types() {
for (auto d : m_decls) {
m_env = m_env.add(check(m_env, mk_var_decl(inductive_decl_name(d), m_level_names, inductive_decl_type(d))));
m_env = m_env.add(check(m_env, mk_constant_assumption(inductive_decl_name(d), m_level_names, inductive_decl_type(d))));
}
inductive_env_ext ext(get_extension(m_env));
ext.add_inductive_info(m_level_names, m_num_params, m_decls);
@ -436,7 +436,7 @@ struct add_inductive_fn {
inductive_env_ext ext(get_extension(m_env));
for (auto d : m_decls) {
for (auto ir : inductive_decl_intros(d)) {
m_env = m_env.add(check(m_env, mk_var_decl(intro_rule_name(ir), m_level_names, intro_rule_type(ir))));
m_env = m_env.add(check(m_env, mk_constant_assumption(intro_rule_name(ir), m_level_names, intro_rule_type(ir))));
ext.add_intro_info(intro_rule_name(ir), inductive_decl_name(d));
}
}
@ -649,7 +649,7 @@ struct add_inductive_fn {
}
elim_ty = Pi(m_param_consts, elim_ty);
elim_ty = infer_implicit(elim_ty, true /* strict */);
m_env = m_env.add(check(m_env, mk_var_decl(get_elim_name(d), get_elim_level_param_names(), elim_ty)));
m_env = m_env.add(check(m_env, mk_constant_assumption(get_elim_name(d), get_elim_level_param_names(), elim_ty)));
}
/** \brief Declare the eliminator/recursor for each datatype. */

20
src/library/kernel_bindings.cpp
View file

@ -746,7 +746,7 @@ int push_optional_declaration(lua_State * L, optional<declaration> const & e) {
DECLARATION_PRED(is_definition)
DECLARATION_PRED(is_theorem)
DECLARATION_PRED(is_axiom)
DECLARATION_PRED(is_var_decl)
DECLARATION_PRED(is_constant_assumption)
DECLARATION_PRED(is_opaque)
DECLARATION_PRED(use_conv_opt)
static int declaration_get_name(lua_State * L) { return push_name(L, to_declaration(L, 1).get_name()); }
@ -759,12 +759,12 @@ static int declaration_get_value(lua_State * L) {
}
static int declaration_get_weight(lua_State * L) { return push_integer(L, to_declaration(L, 1).get_weight()); }
static int declaration_get_module_idx(lua_State * L) { return push_integer(L, to_declaration(L, 1).get_module_idx()); }
static int mk_var_decl(lua_State * L) {
static int mk_constant_assumption(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs == 2)
return push_declaration(L, mk_var_decl(to_name_ext(L, 1), level_param_names(), to_expr(L, 2)));
return push_declaration(L, mk_constant_assumption(to_name_ext(L, 1), level_param_names(), to_expr(L, 2)));
else
return push_declaration(L, mk_var_decl(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3)));
return push_declaration(L, mk_constant_assumption(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3)));
}
static int mk_axiom(lua_State * L) {
int nargs = lua_gettop(L);
@ -821,7 +821,7 @@ static const struct luaL_Reg declaration_m[] = {
{"is_definition", safe_function<declaration_is_definition>},
{"is_theorem", safe_function<declaration_is_theorem>},
{"is_axiom", safe_function<declaration_is_axiom>},
{"is_var_decl", safe_function<declaration_is_var_decl>},
{"is_constant_assumption", safe_function<declaration_is_constant_assumption>},
{"opaque", safe_function<declaration_is_opaque>},
{"use_conv_opt", safe_function<declaration_use_conv_opt>},
{"name", safe_function<declaration_get_name>},
@ -839,11 +839,11 @@ static void open_declaration(lua_State * L) {
lua_setfield(L, -2, "__index");
setfuncs(L, declaration_m, 0);
SET_GLOBAL_FUN(declaration_pred, "is_declaration");
SET_GLOBAL_FUN(mk_var_decl, "mk_var_decl");
SET_GLOBAL_FUN(mk_axiom, "mk_axiom");
SET_GLOBAL_FUN(mk_theorem, "mk_theorem");
SET_GLOBAL_FUN(mk_definition, "mk_definition");
SET_GLOBAL_FUN(declaration_pred, "is_declaration");
SET_GLOBAL_FUN(mk_constant_assumption, "mk_constant_assumption");
SET_GLOBAL_FUN(mk_axiom, "mk_axiom");
SET_GLOBAL_FUN(mk_theorem, "mk_theorem");
SET_GLOBAL_FUN(mk_definition, "mk_definition");
}
// Formatter

2
src/library/kernel_serializer.cpp
View file

@ -314,7 +314,7 @@ declaration read_declaration(deserializer & d, module_idx midx) {
if (is_th_ax)
return mk_axiom(n, ps, t);
else
return mk_var_decl(n, ps, t);
return mk_constant_assumption(n, ps, t);
}
}

2
src/library/level_names.cpp
View file

@ -100,7 +100,7 @@ declaration sanitize_level_params(declaration const & d) {
if (param_name_map.empty())
return d;
expr new_type = rename_param_levels(d.get_type(), param_name_map);
if (d.is_var_decl()) {
if (d.is_constant_assumption()) {
return update_declaration(d, new_ls, new_type);
} else {
expr new_value = rename_param_levels(d.get_value(), param_name_map);

2
src/library/sorry.cpp
View file

@ -36,7 +36,7 @@ environment declare_sorry(environment const & env) {
throw exception("failed to declare 'sorry', environment already has an object named 'sorry'");
return env;
} else {
return module::add(env, check(env, mk_var_decl(*g_sorry_name, list<name>(*g_l), *g_sorry_type)));
return module::add(env, check(env, mk_constant_assumption(*g_sorry_name, list<name>(*g_l), *g_sorry_type)));
}
}

4
src/library/update_declaration.cpp
View file

@ -17,13 +17,13 @@ static declaration update_declaration(declaration d, optional<level_param_names>
} else {
lean_assert(!value);
}
if (d.is_var_decl()) {
if (d.is_constant_assumption()) {
if (is_eqp(d.get_type(), _type) && is_eqp(d.get_univ_params(), _ps))
return d;
if (d.is_axiom())
return mk_axiom(d.get_name(), _ps, _type);
else
return mk_var_decl(d.get_name(), _ps, _type);
return mk_constant_assumption(d.get_name(), _ps, _type);
} else {
if (is_eqp(d.get_type(), _type) && is_eqp(d.get_value(), _value) && is_eqp(d.get_univ_params(), _ps))
return d;

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

@ -86,7 +86,7 @@ static void tst2() {
environment env;
name base("base");
expr Prop = mk_Prop();
env = add_decl(env, mk_var_decl(name(base, 0u), level_param_names(), Prop >> (Prop >> Prop)));
env = add_decl(env, mk_constant_assumption(name(base, 0u), level_param_names(), Prop >> (Prop >> Prop)));
expr x = Local("x", Prop);
expr y = Local("y", Prop);
for (unsigned i = 1; i <= 100; i++) {

3
tests/lean/t1.lean
View file

@ -1,8 +1,7 @@
(*
print("testing...")
local env = get_env()
env = add_decl(env, mk_var_decl("x", Prop))
env = add_decl(env, mk_constant_assumption("x", Prop))
assert(env:find("x"))
set_env(env)
*)

30
tests/lua/coe1.lua
View file

@ -15,19 +15,19 @@ local lst_1 = Const("lst", {1})
local l1 = param_univ("l1")
local l2 = param_univ("l2")
local m = Local("m", nat)
env = add_decl(env, mk_var_decl("nat", Type))
env = add_decl(env, mk_var_decl("real", Type))
env = add_decl(env, mk_var_decl("one", nat))
env = add_decl(env, mk_var_decl("lst", {l}, mk_arrow(Ul, Ul)))
env = add_decl(env, mk_var_decl("len", {l}, Pi(A, mk_arrow(lst_l(A), nat))))
env = add_decl(env, mk_var_decl("vec", {l}, mk_arrow(Ul, nat, Ul)))
env = add_decl(env, mk_var_decl("mat", {l}, mk_arrow(Ul, nat, nat, Ul)))
env = add_decl(env, mk_var_decl("dlst", {l1, l2}, mk_arrow(mk_sort(l1), mk_sort(l2), mk_sort(max_univ(l1, l2)))))
env = add_decl(env, mk_var_decl("vec2lst", {l}, Pi(A, n, mk_arrow(vec_l(A, n), lst_l(A)))))
env = add_decl(env, mk_var_decl("lst2vec", {l}, Pi(A, ll, vec_l(A, len_l(A, ll)))))
env = add_decl(env, mk_var_decl("vec2mat", {l}, Pi(A, n, mk_arrow(vec_l(A, n), mat_l(A, n, one)))))
env = add_decl(env, mk_var_decl("mat2dlst", {l}, Pi(A, n, m, mk_arrow(mat_l(A, n, m), Const("dlst", {l, 1})(A, nat)))))
env = add_decl(env, mk_var_decl("nat2lst", mk_arrow(nat, lst_1(nat))))
env = add_decl(env, mk_constant_assumption("nat", Type))
env = add_decl(env, mk_constant_assumption("real", Type))
env = add_decl(env, mk_constant_assumption("one", nat))
env = add_decl(env, mk_constant_assumption("lst", {l}, mk_arrow(Ul, Ul)))
env = add_decl(env, mk_constant_assumption("len", {l}, Pi(A, mk_arrow(lst_l(A), nat))))
env = add_decl(env, mk_constant_assumption("vec", {l}, mk_arrow(Ul, nat, Ul)))
env = add_decl(env, mk_constant_assumption("mat", {l}, mk_arrow(Ul, nat, nat, Ul)))
env = add_decl(env, mk_constant_assumption("dlst", {l1, l2}, mk_arrow(mk_sort(l1), mk_sort(l2), mk_sort(max_univ(l1, l2)))))
env = add_decl(env, mk_constant_assumption("vec2lst", {l}, Pi(A, n, mk_arrow(vec_l(A, n), lst_l(A)))))
env = add_decl(env, mk_constant_assumption("lst2vec", {l}, Pi(A, ll, vec_l(A, len_l(A, ll)))))
env = add_decl(env, mk_constant_assumption("vec2mat", {l}, Pi(A, n, mk_arrow(vec_l(A, n), mat_l(A, n, one)))))
env = add_decl(env, mk_constant_assumption("mat2dlst", {l}, Pi(A, n, m, mk_arrow(mat_l(A, n, m), Const("dlst", {l, 1})(A, nat)))))
env = add_decl(env, mk_constant_assumption("nat2lst", mk_arrow(nat, lst_1(nat))))
env = add_coercion(env, "lst2vec")
assert(is_coercion(env, Const("lst2vec", {l})))
assert(has_coercions_from(env, "lst"))
@ -62,7 +62,7 @@ print(get_coercions(env2, lst_nat, "dlst"):head())
assert(env2:type_check(get_coercions(env2, lst_nat, "dlst"):head()))
assert(is_coercion(env2, "vec2mat"))
assert(is_coercion(env2, "lst2vec"))
env2 = add_decl(env2, mk_var_decl("lst2vec2", {l}, Pi(A, ll, vec_l(A, len_l(A, ll)))))
env2 = add_decl(env2, mk_constant_assumption("lst2vec2", {l}, Pi(A, ll, vec_l(A, len_l(A, ll)))))
print("======")
env2 = add_coercion(env2, "lst2vec2")
print("======")
@ -70,7 +70,7 @@ print(get_coercions(env2, lst_nat, "dlst"):head())
print("---------")
for_each_coercion_user(env2, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end)
env2 = add_coercion(env2, "vec2lst")
env2 = add_decl(env2, mk_var_decl("lst2nat", {l}, Pi(A, mk_arrow(lst_l(A), nat))))
env2 = add_decl(env2, mk_constant_assumption("lst2nat", {l}, Pi(A, mk_arrow(lst_l(A), nat))))
env2 = add_coercion(env2, "lst2nat")
print("---------")
for_each_coercion_user(env2, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D)) end)

14
tests/lua/coe2.lua
View file

@ -1,21 +1,21 @@
local env = environment()
local l1 = param_univ("l1")
local l2 = param_univ("l2")
env = add_decl(env, mk_var_decl("functor", {l1, l2}, mk_arrow(mk_sort(l1), mk_sort(l2), mk_sort(imax_univ(l1, l2)))))
env = add_decl(env, mk_constant_assumption("functor", {l1, l2}, mk_arrow(mk_sort(l1), mk_sort(l2), mk_sort(imax_univ(l1, l2)))))
local A = Local("A", mk_sort(l1))
local B = Local("B", mk_sort(l2))
local functor = Const("functor", {l1, l2})
env = add_decl(env, mk_var_decl("to_fun", {l1, l2}, Pi(A, B, mk_arrow(functor(A, B), mk_arrow(A, B)))))
env = add_decl(env, mk_constant_assumption("to_fun", {l1, l2}, Pi(A, B, mk_arrow(functor(A, B), mk_arrow(A, B)))))
env = add_coercion(env, "to_fun", "functor")
for_each_coercion_fun(env, function(C, f) print(tostring(C) .. " >-> function : " .. tostring(f)) end)
env = add_decl(env, mk_var_decl("nat", Type))
env = add_decl(env, mk_var_decl("real", Type))
env = add_decl(env, mk_constant_assumption("nat", Type))
env = add_decl(env, mk_constant_assumption("real", Type))
local nat = Const("nat")
local real = Const("real")
env = add_decl(env, mk_var_decl("f1", Const("functor", {1, 1})(nat, real)))
env = add_decl(env, mk_constant_assumption("f1", Const("functor", {1, 1})(nat, real)))
print(get_coercions_to_fun(env, Const("functor", {1, 1})(nat, real)):head())
env = add_decl(env, mk_var_decl("sfunctor", {l1}, mk_arrow(mk_sort(l1), mk_sort(l1))))
env = add_decl(env, mk_var_decl("sf2f", {l1}, Pi(A, mk_arrow(Const("sfunctor", {l1})(A), Const("functor", {l1, l1})(A, A)))))
env = add_decl(env, mk_constant_assumption("sfunctor", {l1}, mk_arrow(mk_sort(l1), mk_sort(l1))))
env = add_decl(env, mk_constant_assumption("sf2f", {l1}, Pi(A, mk_arrow(Const("sfunctor", {l1})(A), Const("functor", {l1, l1})(A, A)))))
env = add_coercion(env, "sf2f")
print(get_coercions_to_fun(env, Const("sfunctor", {1})(nat)):head())
assert(env:type_check(get_coercions_to_fun(env, Const("sfunctor", {1})(nat)):head()))

8
tests/lua/coe3.lua
View file

@ -1,12 +1,12 @@
local env = environment()
local l = param_univ("l")
env = add_decl(env, mk_var_decl("group", {l}, mk_sort(l+1)))
env = add_decl(env, mk_var_decl("abelian_group", {l}, mk_sort(l+1)))
env = add_decl(env, mk_constant_assumption("group", {l}, mk_sort(l+1)))
env = add_decl(env, mk_constant_assumption("abelian_group", {l}, mk_sort(l+1)))
local group = Const("group", {l})
local ab_group = Const("abelian_group", {l})
env = add_decl(env, mk_var_decl("carrier", {l}, mk_arrow(group, mk_sort(l))))
env = add_decl(env, mk_constant_assumption("carrier", {l}, mk_arrow(group, mk_sort(l))))
env = add_coercion(env, "carrier")
env = add_decl(env, mk_var_decl("abg2g", {l}, mk_arrow(ab_group, group)))
env = add_decl(env, mk_constant_assumption("abg2g", {l}, mk_arrow(ab_group, group)))
env = add_coercion(env, "abg2g")
for_each_coercion_sort(env, function(C, f) print(tostring(C) .. " >-> sort : " .. tostring(f)) end)
print(get_coercions_to_sort(env, Const("abelian_group", {1})):head())

8
tests/lua/coe4.lua
View file

@ -3,10 +3,10 @@ local l = param_univ("l")
local Ul = mk_sort(l)
local lst_l = Const("lst", {l})
local A = Local("A", Ul)
env = add_decl(env, mk_var_decl("lst", {l}, mk_arrow(Ul, Ul)))
env = add_decl(env, mk_var_decl("lst2lst", {l}, Pi(A, mk_arrow(lst_l(A), lst_l(A)))))
env = add_decl(env, mk_var_decl("head", {l}, Pi(A, mk_arrow(lst_l(A), A))))
env = add_decl(env, mk_var_decl("id", {l}, Pi(A, mk_arrow(A, A))))
env = add_decl(env, mk_constant_assumption("lst", {l}, mk_arrow(Ul, Ul)))
env = add_decl(env, mk_constant_assumption("lst2lst", {l}, Pi(A, mk_arrow(lst_l(A), lst_l(A)))))
env = add_decl(env, mk_constant_assumption("head", {l}, Pi(A, mk_arrow(lst_l(A), A))))
env = add_decl(env, mk_constant_assumption("id", {l}, Pi(A, mk_arrow(A, A))))
function add_bad_coercion(env, c)
ok, msg = pcall(function() add_coercion(env, c) end)
assert(not ok)

18
tests/lua/coe5.lua
View file

@ -1,20 +1,20 @@
local env = environment()
local l = param_univ("l")
env = add_decl(env, mk_var_decl("group", {l}, mk_sort(l+1)))
env = add_decl(env, mk_var_decl("abelian_group", {l}, mk_sort(l+1)))
env = add_decl(env, mk_var_decl("ring", {l}, mk_sort(l+1)))
env = add_decl(env, mk_var_decl("abelian_ring", {l}, mk_sort(l+1)))
env = add_decl(env, mk_constant_assumption("group", {l}, mk_sort(l+1)))
env = add_decl(env, mk_constant_assumption("abelian_group", {l}, mk_sort(l+1)))
env = add_decl(env, mk_constant_assumption("ring", {l}, mk_sort(l+1)))
env = add_decl(env, mk_constant_assumption("abelian_ring", {l}, mk_sort(l+1)))
local group = Const("group", {l})
local ring = Const("ring", {l})
local ab_group = Const("abelian_group", {l})
local ab_ring = Const("abelian_ring", {l})
env = add_decl(env, mk_var_decl("carrier", {l}, mk_arrow(group, mk_sort(l))))
env = add_decl(env, mk_constant_assumption("carrier", {l}, mk_arrow(group, mk_sort(l))))
env = add_coercion(env, "carrier")
env = add_decl(env, mk_var_decl("ag2g", {l}, mk_arrow(ab_group, group)))
env = add_decl(env, mk_var_decl("r2g", {l}, mk_arrow(ring, group)))
env = add_decl(env, mk_var_decl("ar2r", {l}, mk_arrow(ab_ring, ring)))
env = add_decl(env, mk_var_decl("ar2ag", {l}, mk_arrow(ab_ring, ab_group)))
env = add_decl(env, mk_constant_assumption("ag2g", {l}, mk_arrow(ab_group, group)))
env = add_decl(env, mk_constant_assumption("r2g", {l}, mk_arrow(ring, group)))
env = add_decl(env, mk_constant_assumption("ar2r", {l}, mk_arrow(ab_ring, ring)))
env = add_decl(env, mk_constant_assumption("ar2ag", {l}, mk_arrow(ab_ring, ab_group)))
env = add_coercion(env, "ag2g")
env = add_coercion(env, "r2g")
env = add_coercion(env, "ar2r")

9
tests/lua/def1.lua
View file

@ -1,8 +1,8 @@
local b = mk_var_decl("bit", Type)
local b = mk_constant_assumption("bit", Type)
local l1 = mk_param_univ("l1")
local l2 = mk_param_univ("l2")
local p = mk_var_decl("tst", {"l1", "l2"}, mk_arrow(mk_sort(l1), mk_sort(l2)))
assert(p:is_var_decl())
local p = mk_constant_assumption("tst", {"l1", "l2"}, mk_arrow(mk_sort(l1), mk_sort(l2)))
assert(p:is_constant_assumption())
assert(not p:is_axiom())
assert(p:name() == name("tst"))
print(mk_arrow(mk_sort(l1), mk_sort(l2)))
@ -11,7 +11,7 @@ assert(#(p:univ_params()) == 2)
assert(p:univ_params():head() == name("l1"))
assert(p:univ_params():tail():head() == name("l2"))
local ax = mk_axiom("ax", {"l1", "l2"}, mk_arrow(mk_sort(l1), mk_sort(l2)))
assert(ax:is_var_decl())
assert(ax:is_constant_assumption())
assert(ax:is_axiom())
assert(ax:name() == name("ax"))
assert(not pcall(function() print(ax:value()) end))
@ -73,4 +73,3 @@ mk_theorem("t1", {l1, "l2"}, mk_arrow(mk_sort(l1), mk_sort(l2)), mk_lambda("x",
assert(not pcall(function() mk_definition("bit", Type) end))
local env = environment(10)
assert(not pcall(function() mk_definition(env, "bit", Type) end))

5
tests/lua/env11.lua
View file

@ -1,8 +1,8 @@
local A = Const("A")
local B = Const("B")
local env = environment()
local env1 = add_decl(env, mk_var_decl("A", Prop))
env1 = add_decl(env1, mk_var_decl("B", Prop))
local env1 = add_decl(env, mk_constant_assumption("A", Prop))
env1 = add_decl(env1, mk_constant_assumption("B", Prop))
env1 = add_decl(env1, mk_axiom("H", B))
local c1 = check(env1, mk_axiom("H1", A))
local c2 = check(env1, mk_axiom("H2", A))
@ -34,4 +34,3 @@ local c7 = check(env1b, mk_definition("H2", A, Const("H1")))
expected_error(function() env2:replace(c7) end)
local c8 = check(env1b, mk_theorem("H2", B, Const("H")))
expected_error(function() env2:replace(c8) end)

5
tests/lua/env3.lua
View file

@ -1,6 +1,6 @@
function init(env)
env = add_decl(env, mk_var_decl("A", Prop))
env = add_decl(env, mk_var_decl("And", mk_arrow(Prop, mk_arrow(Prop, Prop))))
env = add_decl(env, mk_constant_assumption("A", Prop))
env = add_decl(env, mk_constant_assumption("And", mk_arrow(Prop, mk_arrow(Prop, Prop))))
env = add_decl(env, mk_axiom("p", Const("A")))
env = add_decl(env, mk_axiom("q", Const("A")))
return env
@ -18,4 +18,3 @@ env = init(bare_environment({prop_proof_irrel=false}))
t = type_checker(env)
assert(not t:is_def_eq(p, q))
assert(not t:is_def_eq(And(p, q), And(q, p)))

2
tests/lua/env4.lua
View file

@ -1,5 +1,5 @@
local env = bare_environment()
env = add_decl(env, mk_var_decl("A", Prop))
env = add_decl(env, mk_constant_assumption("A", Prop))
local c1 = type_check(env, mk_axiom("p", Const("A")))
local c2 = type_check(env, mk_axiom("q", Const("A")))
env = env:add(c1)

2
tests/lua/env5.lua
View file

@ -46,7 +46,7 @@ print(tc2:check(tmp))
local tmp1 = tc2:check(id_u)
local tmp2 = tc2:check(tmp1)
print(tc2:check(tmp2))
env2 = add_decl(env2, mk_var_decl("a", Type))
env2 = add_decl(env2, mk_constant_assumption("a", Type))
local tc2 = type_checker(env2)
local a = Const("a")
local id_2 = Const("id", {mk_level_succ(mk_level_one())})

2
tests/lua/env6.lua
View file

@ -1,5 +1,5 @@
local env = bare_environment()
env = add_decl(env, mk_var_decl("A", Prop))
env = add_decl(env, mk_constant_assumption("A", Prop))
local A = Const("A")
local x = Local("x", Prop)
env = add_decl(env, mk_axiom("magic", Pi(x, x)))

2
tests/lua/env7.lua
View file

@ -1,5 +1,5 @@
local env1 = bare_environment()
local env2 = add_decl(env1, mk_var_decl("A", Type))
local env2 = add_decl(env1, mk_constant_assumption("A", Type))
assert(env2:is_descendant(env1))
assert(env2:is_descendant(env2))
assert(not env1:is_descendant(env2))

7
tests/lua/env9.lua
View file

@ -1,12 +1,11 @@
local env = bare_environment()
-- Trust level is set to 0 by default. Then, we must type check a
-- definition, before adding it to the environment
assert(not pcall(function() env:add(mk_var_decl("A", Prop)) end))
assert(not pcall(function() env:add(mk_constant_assumption("A", Prop)) end))
-- The function check produces a "certified declaration".
env:add(check(env, mk_var_decl("A", Prop)))
env:add(check(env, mk_constant_assumption("A", Prop)))
local env = bare_environment({trust_level = 10000000})
-- Now, env has trust_level > LEAN_BELIEVER_TRUST_LEVEL, then we can
-- add declarations without type checking them.
env:add(mk_var_decl("A", Prop))
env:add(mk_constant_assumption("A", Prop))

2
tests/lua/eta.lua
View file

@ -1,5 +1,5 @@
local env = bare_environment()
env = add_decl(env, mk_var_decl("f", mk_arrow(Prop, mk_arrow(Prop, Prop))))
env = add_decl(env, mk_constant_assumption("f", mk_arrow(Prop, mk_arrow(Prop, Prop))))
local f = Const("f")
local x = Local("x", Prop)
local y = Local("y", Prop)

2
tests/lua/goal1.lua
View file

@ -1,6 +1,6 @@
local env = environment()
local A = Local("A", Type)
env = add_decl(env, mk_var_decl("eq", Pi(A, mk_arrow(A, A, Prop))))
env = add_decl(env, mk_constant_assumption("eq", Pi(A, mk_arrow(A, A, Prop))))
local eq = Const("eq")
local a = Local("a", A)
local b = Local("b", A)

2
tests/lua/ind2.lua
View file

@ -95,7 +95,7 @@ bad_add_inductive(env,
"cons", Pi(A, mk_arrow(list_l(A), A, list_l(A))))
local A = Local("A", Type)
env = add_decl(env, mk_var_decl("eq", Pi(A, mk_arrow(A, A, Prop))))
env = add_decl(env, mk_constant_assumption("eq", Pi(A, mk_arrow(A, A, Prop))))
local eq = Const("eq")
local Nat2 = Const("nat2")
local a = Local("a", Nat2)

6
tests/lua/mod1.lua
View file

@ -1,5 +1,5 @@
local env = environment()
env = add_decl(env, mk_var_decl("A", Prop))
env = add_decl(env, mk_constant_assumption("A", Prop))
local A = Const("A")
env = add_decl(env, mk_axiom("H1", A))
local H1 = Const("H1")
@ -10,7 +10,7 @@ env:export("mod1_mod.olean")
local env2 = import_modules("mod1_mod.olean", {keep_proofs=true})
assert(env2:get("A"):type() == Prop)
assert(env2:get("A"):is_var_decl())
assert(env2:get("A"):is_constant_assumption())
assert(env2:get("H1"):type() == A)
assert(env2:get("H1"):is_axiom())
assert(env2:get("H2"):type() == A)
@ -22,7 +22,7 @@ assert(env2:get("B"):is_definition())
local env3 = import_modules("mod1_mod.olean")
assert(env3:get("A"):type() == Prop)
assert(env3:get("A"):is_var_decl())
assert(env3:get("A"):is_constant_assumption())
assert(env3:get("H1"):type() == A)
assert(env3:get("H1"):is_axiom())
assert(env3:get("H2"):type() == A)

2
tests/lua/mod3.lua
View file

@ -1,3 +1,3 @@
local env = environment()
env = add_decl(env, mk_var_decl("A", Type))
env = add_decl(env, mk_constant_assumption("A", Type))
env:export("mod3_mod.olean")

4
tests/lua/mod5.lua
View file

@ -15,8 +15,8 @@ function mk_module(midx, imports)
end
local env = import_modules(imp_names, {num_threads=NumThreads})
if #imports == 0 then
env = add_decl(env, mk_var_decl(const_name(midx), Prop))
env = add_decl(env, mk_var_decl("and", mk_arrow(Prop, Prop, Prop)))
env = add_decl(env, mk_constant_assumption(const_name(midx), Prop))
env = add_decl(env, mk_constant_assumption("and", mk_arrow(Prop, Prop, Prop)))
elseif #imports == 1 then
env = add_decl(env, mk_definition(const_name(midx), Prop, Const(const_name(imports[1]))))
else

2
tests/lua/proof_state1.lua
View file

@ -1,6 +1,6 @@
local env = environment()
local A = Local("A", Type)
env = add_decl(env, mk_var_decl("eq", Pi(A, mk_arrow(A, A, Prop))))
env = add_decl(env, mk_constant_assumption("eq", Pi(A, mk_arrow(A, A, Prop))))
local eq = Const("eq")
local a = mk_local("a", "a", A)
local b = mk_local("b", "a", A)

8
tests/lua/res1.lua
View file

@ -11,9 +11,9 @@ function init_env(env)
local c = Local("c", Prop)
local Ha = Local("Ha", a)
local Hb = Local("Hb", b)
env = add_decl(env, mk_var_decl("or", mk_arrow(Prop, Prop, Prop)))
env = add_decl(env, mk_var_decl("not", mk_arrow(Prop, Prop)))
env = add_decl(env, mk_var_decl("false", Prop))
env = add_decl(env, mk_constant_assumption("or", mk_arrow(Prop, Prop, Prop)))
env = add_decl(env, mk_constant_assumption("not", mk_arrow(Prop, Prop)))
env = add_decl(env, mk_constant_assumption("false", Prop))
env = add_decl(env, mk_axiom({"or", "elim"}, Pi(a, b, c, mk_arrow(Or(a, b), mk_arrow(a, c), mk_arrow(b, c), c))))
env = add_decl(env, mk_axiom({"or", "intro_left"}, Pi(a, Ha, b, Or(a, b))))
env = add_decl(env, mk_axiom({"or", "intro_right"}, Pi(b, a, Hb, Or(a, b))))
@ -23,7 +23,7 @@ end
function decl_bools(env, ls)
for i = 1, #ls do
env = add_decl(env, mk_var_decl(ls[i]:data(), Prop))
env = add_decl(env, mk_constant_assumption(ls[i]:data(), Prop))
end
return env
end

26
tests/lua/scope.lua
View file

@ -15,19 +15,19 @@ local lst_1 = Const("lst", {1})
local l1 = param_univ("l1")
local l2 = param_univ("l2")
local m = Local("m", nat)
env = add_decl(env, mk_var_decl("nat", Type))
env = add_decl(env, mk_var_decl("real", Type))
env = add_decl(env, mk_var_decl("one", nat))
env = add_decl(env, mk_var_decl("lst", {l}, mk_arrow(Ul, Ul)))
env = add_decl(env, mk_var_decl("len", {l}, Pi(A, mk_arrow(lst_l(A), nat))))
env = add_decl(env, mk_var_decl("vec", {l}, mk_arrow(Ul, nat, Ul)))
env = add_decl(env, mk_var_decl("mat", {l}, mk_arrow(Ul, nat, nat, Ul)))
env = add_decl(env, mk_var_decl("dlst", {l1, l2}, mk_arrow(mk_sort(l1), mk_sort(l2), mk_sort(max_univ(l1, l2)))))
env = add_decl(env, mk_var_decl("vec2lst", {l}, Pi(A, n, mk_arrow(vec_l(A, n), lst_l(A)))))
env = add_decl(env, mk_var_decl("lst2vec", {l}, Pi(A, ll, vec_l(A, len_l(A, ll)))))
env = add_decl(env, mk_var_decl("vec2mat", {l}, Pi(A, n, mk_arrow(vec_l(A, n), mat_l(A, n, one)))))
env = add_decl(env, mk_var_decl("mat2dlst", {l}, Pi(A, n, m, mk_arrow(mat_l(A, n, m), Const("dlst", {l, 1})(A, nat)))))
env = add_decl(env, mk_var_decl("nat2lst", mk_arrow(nat, lst_1(nat))))
env = add_decl(env, mk_constant_assumption("nat", Type))
env = add_decl(env, mk_constant_assumption("real", Type))
env = add_decl(env, mk_constant_assumption("one", nat))
env = add_decl(env, mk_constant_assumption("lst", {l}, mk_arrow(Ul, Ul)))
env = add_decl(env, mk_constant_assumption("len", {l}, Pi(A, mk_arrow(lst_l(A), nat))))
env = add_decl(env, mk_constant_assumption("vec", {l}, mk_arrow(Ul, nat, Ul)))
env = add_decl(env, mk_constant_assumption("mat", {l}, mk_arrow(Ul, nat, nat, Ul)))
env = add_decl(env, mk_constant_assumption("dlst", {l1, l2}, mk_arrow(mk_sort(l1), mk_sort(l2), mk_sort(max_univ(l1, l2)))))
env = add_decl(env, mk_constant_assumption("vec2lst", {l}, Pi(A, n, mk_arrow(vec_l(A, n), lst_l(A)))))
env = add_decl(env, mk_constant_assumption("lst2vec", {l}, Pi(A, ll, vec_l(A, len_l(A, ll)))))
env = add_decl(env, mk_constant_assumption("vec2mat", {l}, Pi(A, n, mk_arrow(vec_l(A, n), mat_l(A, n, one)))))
env = add_decl(env, mk_constant_assumption("mat2dlst", {l}, Pi(A, n, m, mk_arrow(mat_l(A, n, m), Const("dlst", {l, 1})(A, nat)))))
env = add_decl(env, mk_constant_assumption("nat2lst", mk_arrow(nat, lst_1(nat))))
env = add_coercion(env, "lst2vec")
env = push_scope(env, "tst")
local lst_nat = lst_1(nat)

2
tests/lua/slow/mod2.lua
View file

@ -4,7 +4,7 @@ function mk_env(prefix, sz)
local A = Local("A", mk_sort(0))
local x = Local("x", A)
env = add_decl(env, mk_definition(name(prefix, "id"), Pi(A, mk_arrow(A, A)), Fun(A, x, x), {opaque=false}))
env = add_decl(env, mk_var_decl(name(prefix, "P"), Prop))
env = add_decl(env, mk_constant_assumption(name(prefix, "P"), Prop))
local P = Const(name(prefix, "P"))
local id = Const(name(prefix, "id"))
env = add_decl(env, mk_axiom(name(prefix, "Ax"), P))

2
tests/lua/tactic1.lua
View file

@ -1,6 +1,6 @@
local env = environment()
local A = Local("A", Type)
env = add_decl(env, mk_var_decl("eq", Pi(A, mk_arrow(A, A, Prop))))
env = add_decl(env, mk_constant_assumption("eq", Pi(A, mk_arrow(A, A, Prop))))
local eq = Const("eq")
local a = Local("a", A)
local b = Local("b", A)

4
tests/lua/tc4.lua
View file

@ -1,6 +1,6 @@
local env = bare_environment()
env = add_decl(env, mk_var_decl("or", mk_arrow(Prop, Prop, Prop)))
env = add_decl(env, mk_var_decl("A", Prop))
env = add_decl(env, mk_constant_assumption("or", mk_arrow(Prop, Prop, Prop)))
env = add_decl(env, mk_constant_assumption("A", Prop))
local Or = Const("or")
local A = Const("A")
local B = Const("B")

8
tests/lua/tc5.lua
View file

@ -1,8 +1,8 @@
local env = bare_environment()
env = add_decl(env, mk_var_decl("A", Prop))
env = add_decl(env, mk_var_decl("T", Type))
env = add_decl(env, mk_constant_assumption("A", Prop))
env = add_decl(env, mk_constant_assumption("T", Type))
env = add_decl(env, mk_definition("B2", Type, Prop, {opaque=false}))
env = add_decl(env, mk_var_decl("C", Const("B2")))
env = add_decl(env, mk_constant_assumption("C", Const("B2")))
env = add_decl(env, mk_definition("BB", Type, mk_arrow(Prop, Prop), {opaque=false}))
local tc = type_checker(env)
assert(tc:is_prop(Const("A")))
@ -21,7 +21,7 @@ assert(not pcall(function()
end
))
assert(not pcall(function()
env = add_decl(env, mk_var_decl("A", mk_local("l1", Prop)))
env = add_decl(env, mk_constant_assumption("A", mk_local("l1", Prop)))
end
))
assert(not pcall(function()

2
tests/lua/tc6.lua
View file

@ -1,3 +1,3 @@
local env = environment()
local l = mk_param_univ("l")
check_error(function() env = add_decl(env, mk_var_decl("A", {l, l}, mk_sort(l))) end)
check_error(function() env = add_decl(env, mk_constant_assumption("A", {l, l}, mk_sort(l))) end)

8
tests/lua/tc7.lua
View file

@ -1,9 +1,9 @@
local env = environment()
env = add_decl(env, mk_var_decl("N", Type))
env = add_decl(env, mk_constant_assumption("N", Type))
local N = Const("N")
env = add_decl(env, mk_var_decl("f", mk_arrow(N, N)))
env = add_decl(env, mk_var_decl("g", mk_arrow(N, N)))
env = add_decl(env, mk_var_decl("a", N))
env = add_decl(env, mk_constant_assumption("f", mk_arrow(N, N)))
env = add_decl(env, mk_constant_assumption("g", mk_arrow(N, N)))
env = add_decl(env, mk_constant_assumption("a", N))
local f = Const("f")
local g = Const("g")
local x = Local("x", N)

6
tests/lua/tc8.lua
View file

@ -1,8 +1,8 @@
local env = environment()
local N = Const("N")
env = add_decl(env, mk_var_decl("N", Type))
env = add_decl(env, mk_var_decl("f", mk_arrow(N, N)))
env = add_decl(env, mk_var_decl("a", N))
env = add_decl(env, mk_constant_assumption("N", Type))
env = add_decl(env, mk_constant_assumption("f", mk_arrow(N, N)))
env = add_decl(env, mk_constant_assumption("a", N))
local f = Const("f")
local a = Const("a")
local m1 = mk_metavar("m1", mk_metavar("m2", mk_sort(mk_meta_univ("l"))))

20
tests/lua/tc_bug1.lua
View file

@ -12,16 +12,16 @@ local and_intro = Const("and_intro")
local A = Local("A", Prop)
local B = Local("B", Prop)
local C = Local("C", Prop)
env = add_decl(env, mk_var_decl("N", Type))
env = add_decl(env, mk_var_decl("p", mk_arrow(N, N, Prop)))
env = add_decl(env, mk_var_decl("q", mk_arrow(N, Prop)))
env = add_decl(env, mk_var_decl("f", mk_arrow(N, N)))
env = add_decl(env, mk_var_decl("a", N))
env = add_decl(env, mk_var_decl("b", N))
env = add_decl(env, mk_var_decl("and", mk_arrow(Prop, Prop, Prop)))
env = add_decl(env, mk_var_decl("and_intro", Pi(A, B, mk_arrow(A, B, And(A, B)))))
env = add_decl(env, mk_var_decl("foo_intro", Pi(A, B, C, mk_arrow(B, B))))
env = add_decl(env, mk_var_decl("foo_intro2", Pi(A, B, C, mk_arrow(B, B))))
env = add_decl(env, mk_constant_assumption("N", Type))
env = add_decl(env, mk_constant_assumption("p", mk_arrow(N, N, Prop)))
env = add_decl(env, mk_constant_assumption("q", mk_arrow(N, Prop)))
env = add_decl(env, mk_constant_assumption("f", mk_arrow(N, N)))
env = add_decl(env, mk_constant_assumption("a", N))
env = add_decl(env, mk_constant_assumption("b", N))
env = add_decl(env, mk_constant_assumption("and", mk_arrow(Prop, Prop, Prop)))
env = add_decl(env, mk_constant_assumption("and_intro", Pi(A, B, mk_arrow(A, B, And(A, B)))))
env = add_decl(env, mk_constant_assumption("foo_intro", Pi(A, B, C, mk_arrow(B, B))))
env = add_decl(env, mk_constant_assumption("foo_intro2", Pi(A, B, C, mk_arrow(B, B))))
env = add_decl(env, mk_axiom("Ax1", q(a)))
env = add_decl(env, mk_axiom("Ax2", q(a)))
env = add_decl(env, mk_axiom("Ax3", q(b)))

6
tests/lua/unify2.lua
View file

@ -17,10 +17,10 @@ function test_unify(env, lhs, rhs, num_s)
end
local env = environment()
env = add_decl(env, mk_var_decl("N", Type))
env = add_decl(env, mk_constant_assumption("N", Type))
local N = Const("N")
env = add_decl(env, mk_var_decl("f", mk_arrow(N, N, N)))
env = add_decl(env, mk_var_decl("a", N))
env = add_decl(env, mk_constant_assumption("f", mk_arrow(N, N, N)))
env = add_decl(env, mk_constant_assumption("a", N))
local f = Const("f")
local a = Const("a")
local l1 = mk_local("l1", "x", N)

12
tests/lua/unify3.lua
View file

@ -3,12 +3,12 @@ local group = Const("group")
local carrier = Const("carrier")
local real = Const("real")
local nat = Const("nat")
env = add_decl(env, mk_var_decl("group", mk_sort(2)))
env = add_decl(env, mk_var_decl("carrier", mk_arrow(group, Type)))
env = add_decl(env, mk_var_decl("real", Type))
env = add_decl(env, mk_var_decl("nat", Type))
env = add_decl(env, mk_var_decl("real_group", group))
env = add_decl(env, mk_var_decl("nat_group", group))
env = add_decl(env, mk_constant_assumption("group", mk_sort(2)))
env = add_decl(env, mk_constant_assumption("carrier", mk_arrow(group, Type)))
env = add_decl(env, mk_constant_assumption("real", Type))
env = add_decl(env, mk_constant_assumption("nat", Type))
env = add_decl(env, mk_constant_assumption("real_group", group))
env = add_decl(env, mk_constant_assumption("nat_group", group))
local real_group = Const("real_group")
local nat_group = Const("nat_group")
local m = mk_metavar("m", mk_metavar("m_ty", mk_sort(mk_meta_univ("u"))))

6
tests/lua/unify4.lua
View file

@ -11,10 +11,10 @@ function test_unify(env, m, lhs, rhs, num_s)
end
local env = environment()
env = add_decl(env, mk_var_decl("N", Type))
env = add_decl(env, mk_constant_assumption("N", Type))
local N = Const("N")
env = add_decl(env, mk_var_decl("f", mk_arrow(N, N, N)))
env = add_decl(env, mk_var_decl("a", N))
env = add_decl(env, mk_constant_assumption("f", mk_arrow(N, N, N)))
env = add_decl(env, mk_constant_assumption("a", N))
local f = Const("f")
local a = Const("a")
local l1 = mk_local("l1", "x", N)

8
tests/lua/unify5.lua
View file

@ -1,9 +1,9 @@
local env = environment()
env = add_decl(env, mk_var_decl("N", Type))
env = add_decl(env, mk_constant_assumption("N", Type))
local N = Const("N")
env = add_decl(env, mk_var_decl("f", mk_arrow(N, N, N)))
env = add_decl(env, mk_var_decl("a", N))
env = add_decl(env, mk_var_decl("b", N))
env = add_decl(env, mk_constant_assumption("f", mk_arrow(N, N, N)))
env = add_decl(env, mk_constant_assumption("a", N))
env = add_decl(env, mk_constant_assumption("b", N))
local f = Const("f")
local a = Const("a")
local b = Const("b")

4
tests/lua/unify7.lua
View file

@ -1,8 +1,8 @@
local env = environment()
local N = Const("N")
local P = Const("P")
env = add_decl(env, mk_var_decl("N", Type))
env = add_decl(env, mk_var_decl("P", mk_arrow(N, Prop)))
env = add_decl(env, mk_constant_assumption("N", Type))
env = add_decl(env, mk_constant_assumption("P", mk_arrow(N, Prop)))
local a = Local("a", N)
local H = Local("H", P(a))
local t = Pi(H, Prop)