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

refactor(kernel): store binder_infor in local constants

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-30 09:14:55 -07:00
parent c2ab31113f
commit cb000eda13
65 changed files with 526 additions and 668 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
doc/lua/lua.md
View file

@ -701,7 +701,7 @@ A local constant is essentially a pair name and expression, where the
expression represents the type of the local constant.
The API `Fun(c, b)` automatically replace the local constant `c` in `b` with
the variable 0. It does all necessary adjustments when `b` contains nested
lambda abstractions. The API also provides `Fun({c_1, ..., c_n}, b)` as
lambda abstractions. The API also provides `Fun(c_1, ..., c_n, b)` as
syntax-sugar for `Fun(c_1, ..., Fun(c_n, b)...)`.
```lua
@ -711,14 +711,14 @@ local c_1 = Local("c_1", N)
local c_2 = Local("c_2", N)
local c_3 = Local("c_3", N)
assert(Fun(c_1, f(c_1)) == mk_lambda("c_1", N, f(Var(0))))
assert(Fun({c_1, c_2}, f(c_1, c_2)) ==
assert(Fun(c_1, c_2, f(c_1, c_2)) ==
mk_lambda("c_1", N, mk_lambda("c_2", N, f(Var(1), Var(0)))))
assert(Fun({c_1, c_2}, f(c_1, Fun(c_3, f(c_2, c_3)))) ==
assert(Fun(c_1, c_2, f(c_1, Fun(c_3, f(c_2, c_3)))) ==
mk_lambda("c_1", N, mk_lambda("c_2", N,
f(Var(1), mk_lambda("c_3", N, f(Var(1), Var(0)))))))
````
Binders can be annotated with `hints` for the Lean _elaborator_.
Local constants can be annotated with `hints` for the Lean _elaborator_.
For example, we can say a binder is an _implicit argument_, and
must be inferred automatically by the elaborator.
These annotations are irrelevant from the kernel's point of view,
@ -732,13 +732,13 @@ assert(is_binder_info(b))
assert(b:is_implicit())
local N = Const("N")
local f = Const("f")
local c1 = Local("c1", N)
local c1 = Local("c1", N, b)
local c2 = Local("c2", N)
-- Create the expression
-- fun {c1 : N} (c2 : N), (f c1 c2)
-- In Lean, curly braces are used to denote
-- implicit arguments
local l = Fun({{c1, b}, c2}, f(c1, c2))
local l = Fun(c1, c2, f(c1, c2))
local x, T, B, bi = l:data()
assert(x == name("c1"))
assert(T == N)
@ -748,14 +748,3 @@ local y, T, C, bi2 = B:data()
assert(not bi2:is_implicit())
```
We can also use the `Fun` API with regular constants and the desired type.
```lua
local N = Const("N")
local f = Const("f")
local c = Const("c")
assert(Fun(c, N, f(c)) == mk_lambda("c", N, f(Var(0))))
local d = Const("d")
assert(Fun({{c, N}, {d, N}}, f(c, d)) ==
mk_lambda("c", N, mk_lambda("d", N, f(Var(1), Var(0)))))
```

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

@ -73,7 +73,7 @@ environment end_scoped_cmd(parser & p) {
environment check_cmd(parser & p) {
expr e = p.parse_expr();
buffer<parameter> section_ps;
buffer<expr> section_ps;
name_set locals = collect_locals(e);
mk_section_params(collect_locals(e), p, section_ps);
e = p.lambda_abstract(section_ps, e);

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

@ -96,7 +96,7 @@ static expr parse_let(parser & p, pos_info const & pos) {
value = p.parse_expr();
} else {
parser::local_scope scope2(p);
buffer<parameter> ps;
buffer<expr> ps;
auto lenv = p.parse_binders(ps);
if (p.curr_is_token(g_colon)) {
if (!is_opaque)
@ -118,7 +118,7 @@ static expr parse_let(parser & p, pos_info const & pos) {
expr body = abstract(parse_let_body(p, pos), l);
return mk_let(p, id, type, value, body, pos, mk_contextual_info(is_fact));
} else {
p.add_local_expr(id, value, mk_contextual_info(false));
p.add_local_expr(id, value);
return parse_let_body(p, pos);
}
}
@ -225,9 +225,9 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> con
}
p.check_token_next(g_comma, "invalid 'have' declaration, ',' expected");
parser::local_scope scope(p);
expr l = p.save_pos(mk_local(id, prop), pos);
binder_info bi = mk_contextual_info(is_fact);
p.add_local(l, bi);
expr l = p.save_pos(mk_local(id, prop, bi), pos);
p.add_local(l);
expr body;
if (p.curr_is_token(g_then)) {
auto then_pos = p.pos();

1
src/frontends/lean/cmd_table.h
View file

@ -9,6 +9,7 @@ Author: Leonardo de Moura
#include <functional>
#include "kernel/environment.h"
#include "library/tactic/tactic.h"
#include "frontends/lean/parser_pos_provider.h"
namespace lean {
class parser;

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

@ -113,7 +113,7 @@ static environment declare_var(parser & p, environment env,
name const & n, level_param_names const & ls, expr const & type,
bool is_axiom, binder_info const & bi, pos_info const & pos) {
if (in_section(p.env())) {
p.add_local_expr(n, p.save_pos(mk_local(n, type), pos), bi);
p.add_local(p.save_pos(mk_local(n, type, bi), pos));
return env;
} else {
name const & ns = get_namespace(env);
@ -143,7 +143,7 @@ environment variable_cmd_core(parser & p, bool is_axiom) {
parser::param_universe_scope scope2(p);
expr type;
if (!p.curr_is_token(g_colon)) {
buffer<parameter> ps;
buffer<expr> ps;
auto lenv = p.parse_binders(ps);
p.check_token_next(g_colon, "invalid declaration, ':' expected");
type = p.parse_scoped_expr(ps, lenv);
@ -171,17 +171,17 @@ environment axiom_cmd(parser & p) {
}
// Sort local_names by order of occurrence in the section, and copy the associated parameters to section_ps
void mk_section_params(name_set const & local_names, parser const & p, buffer<parameter> & section_ps) {
void mk_section_params(name_set const & local_names, parser const & p, buffer<expr> & section_ps) {
local_names.for_each([&](name const & n) {
section_ps.push_back(*p.get_local(n));
});
std::sort(section_ps.begin(), section_ps.end(), [&](parameter const & p1, parameter const & p2) {
return p.get_local_index(mlocal_name(p1.m_local)) < p.get_local_index(mlocal_name(p2.m_local));
std::sort(section_ps.begin(), section_ps.end(), [&](expr const & p1, expr const & p2) {
return p.get_local_index(mlocal_name(p1)) < p.get_local_index(mlocal_name(p2));
});
}
// Collect local (section) constants occurring in type and value, sort them, and store in section_ps
void collect_section_locals(expr const & type, expr const & value, parser const & p, buffer<parameter> & section_ps) {
void collect_section_locals(expr const & type, expr const & value, parser const & p, buffer<expr> & section_ps) {
name_set ls = collect_locals(type, collect_locals(value));
return mk_section_params(ls, p, section_ps);
}
@ -249,7 +249,7 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque) {
p.check_token_next(g_assign, "invalid declaration, ':=' expected");
value = p.parse_expr();
} else {
buffer<parameter> ps;
buffer<expr> ps;
optional<local_environment> lenv;
{
parser::param_universe_scope scope2(p);
@ -270,15 +270,12 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque) {
ls = to_list(ls_buffer.begin(), ls_buffer.end());
}
if (in_section(env)) {
buffer<parameter> section_ps;
buffer<expr> section_ps;
collect_section_locals(type, value, p, section_ps);
type = p.pi_abstract(section_ps, type);
value = p.lambda_abstract(section_ps, value);
levels section_ls = collect_section_levels(ls, p);
buffer<expr> section_args;
for (auto const & p : section_ps)
section_args.push_back(p.m_local);
expr ref = mk_app(mk_explicit(mk_constant(real_n, section_ls)), section_args);
expr ref = mk_app(mk_explicit(mk_constant(real_n, section_ls)), section_ps);
p.add_local_expr(n, ref);
} else {
if (real_n != n)

3
src/frontends/lean/decl_cmds.h
View file

@ -7,7 +7,6 @@ Author: Leonardo de Moura
#pragma once
#include "util/buffer.h"
#include "kernel/expr.h"
#include "frontends/lean/parameter.h"
#include "frontends/lean/cmd_table.h"
namespace lean {
class parser;
@ -26,7 +25,7 @@ void update_univ_parameters(buffer<name> & ls_buffer, name_set const & found_ls,
\brief Copy the parameters associated with the local names in \c local_names to \c section_ps.
Then sort \c section_ps (using the order in which they were declared).
*/
void mk_section_params(name_set const & local_names, parser const & p, buffer<parameter> & section_ps);
void mk_section_params(name_set const & local_names, parser const & p, buffer<expr> & section_ps);
/**
\brief Return the levels in \c ls that are defined in the section.
*/

27
src/frontends/lean/elaborator.cpp
View file

@ -24,12 +24,11 @@ Author: Leonardo de Moura
#include "library/unifier.h"
#include "library/tactic/tactic.h"
#include "library/error_handling/error_handling.h"
#include "frontends/lean/parameter.h"
#include "frontends/lean/hint_table.h"
namespace lean {
class elaborator {
typedef list<parameter> context;
typedef list<expr> context;
typedef std::vector<constraint> constraints;
environment m_env;
@ -123,8 +122,8 @@ public:
m_subst(s), m_ctx(ctx), m_pos_provider(pp) {
}
expr mk_local(name const & n, expr const & t) {
return ::lean::mk_local(m_ngen.next(), n, t);
expr mk_local(name const & n, expr const & t, binder_info const & bi) {
return ::lean::mk_local(m_ngen.next(), n, t, bi);
}
expr infer_type(expr const & e) {
@ -199,7 +198,7 @@ public:
*/
expr pi_abstract_context(expr e, tag g) {
for (auto const & p : m_ctx)
e = save_tag(Pi(p.m_local, e, p.m_bi), g);
e = save_tag(Pi(p, e), g);
return e;
}
@ -215,7 +214,7 @@ public:
expr apply_context(expr const & f, tag g) {
buffer<expr> args;
for (auto const & p : m_ctx)
args.push_back(p.m_local);
args.push_back(p);
expr r = f;
unsigned i = args.size();
while (i > 0) {
@ -505,10 +504,10 @@ public:
expr visit_pi(expr const & e) {
expr d = ensure_type(visit_expecting_type(binding_domain(e)));
expr l = mk_local(binding_name(e), d);
expr l = mk_local(binding_name(e), d, binding_info(e));
expr b = instantiate(binding_body(e), l);
if (binding_info(e).is_contextual()) {
flet<context> set(m_ctx, cons(parameter(l, binding_info(e)), m_ctx));
flet<context> set(m_ctx, cons(l, m_ctx));
b = ensure_type(visit_expecting_type(b));
} else {
b = ensure_type(visit_expecting_type(b));
@ -519,10 +518,10 @@ public:
expr visit_lambda(expr const & e) {
expr d = ensure_type(visit_expecting_type(binding_domain(e)));
expr l = mk_local(binding_name(e), d);
expr l = mk_local(binding_name(e), d, binding_info(e));
expr b = instantiate(binding_body(e), l);
if (binding_info(e).is_contextual()) {
flet<context> set(m_ctx, cons(parameter(l, binding_info(e)), m_ctx));
flet<context> set(m_ctx, cons(l, m_ctx));
b = visit(b);
} else {
b = visit(b);
@ -706,21 +705,21 @@ public:
static name g_tmp_prefix = name::mk_internal_unique_name();
expr elaborate(environment const & env, io_state const & ios, expr const & e, name_generator const & ngen,
hint_table const & htable, substitution const & s, list<parameter> const & ctx, pos_info_provider * pp) {
hint_table const & htable, substitution const & s, list<expr> const & ctx, pos_info_provider * pp) {
return elaborator(env, ios, ngen, htable, s, ctx, pp)(e);
}
expr elaborate(environment const & env, io_state const & ios, expr const & e, hint_table const & htable, pos_info_provider * pp) {
return elaborate(env, ios, e, name_generator(g_tmp_prefix), htable, substitution(), list<parameter>(), pp);
return elaborate(env, ios, e, name_generator(g_tmp_prefix), htable, substitution(), list<expr>(), pp);
}
std::pair<expr, expr> elaborate(environment const & env, io_state const & ios, name const & n, expr const & t, expr const & v,
hint_table const & htable, pos_info_provider * pp) {
return elaborator(env, ios, name_generator(g_tmp_prefix), htable, substitution(), list<parameter>(), pp)(t, v, n);
return elaborator(env, ios, name_generator(g_tmp_prefix), htable, substitution(), list<expr>(), pp)(t, v, n);
}
expr elaborate(environment const & env, io_state const & ios, expr const & e, expr const & expected_type, name_generator const & ngen,
hint_table const & htable, list<parameter> const & ctx, pos_info_provider * pp) {
hint_table const & htable, list<expr> const & ctx, pos_info_provider * pp) {
return elaborator(env, ios, ngen, htable, substitution(), ctx, pp)(e, expected_type);
}
}

4
src/frontends/lean/elaborator.h
View file

@ -15,9 +15,9 @@ Author: Leonardo de Moura
namespace lean {
expr elaborate(environment const & env, io_state const & ios, expr const & e, name_generator const & ngen,
hint_table const & htable = hint_table(), substitution const & s = substitution(),
list<parameter> const & ctx = list<parameter>(), pos_info_provider * pp = nullptr);
list<expr> const & ctx = list<expr>(), pos_info_provider * pp = nullptr);
expr elaborate(environment const & env, io_state const & ios, expr const & e, expr const & expected_type, name_generator const & ngen,
hint_table const & htable = hint_table(), list<parameter> const & ctx = list<parameter>(), pos_info_provider * pp = nullptr);
hint_table const & htable = hint_table(), list<expr> const & ctx = list<expr>(), pos_info_provider * pp = nullptr);
expr elaborate(environment const & env, io_state const & ios, expr const & e, hint_table const & htable = hint_table(),
pos_info_provider * pp = nullptr);
std::pair<expr, expr> elaborate(environment const & env, io_state const & ios, name const & n, expr const & t, expr const & v,

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

@ -39,7 +39,7 @@ using inductive::intro_rule_type;
// Make sure that every inductive datatype (in decls) occurring in \c type has
// the universe levels \c lvl_params and section parameters \c section_params
static expr fix_inductive_occs(expr const & type, buffer<inductive_decl> const & decls,
buffer<name> const & lvl_params, buffer<parameter> const & section_params) {
buffer<name> const & lvl_params, buffer<expr> const & section_params) {
return replace(type, [&](expr const & e, unsigned) {
if (!is_constant(e))
return none_expr();
@ -58,7 +58,7 @@ static expr fix_inductive_occs(expr const & type, buffer<inductive_decl> const &
}
expr r = update_constant(e, ls);
for (unsigned i = 0; i < section_params.size(); i++)
r = mk_app(r, section_params[i].m_local);
r = mk_app(r, section_params[i]);
return some_expr(r);
});
}
@ -134,7 +134,7 @@ static void accumulate_levels(type_checker & tc, expr t, unsigned num_params, le
ls.push_back(l);
}
}
t = instantiate(binding_body(t), mk_local(ngen.next(), binding_name(t), binding_domain(t)));
t = instantiate(binding_body(t), mk_local(ngen.next(), binding_name(t), binding_domain(t), binding_info(t)));
i++;
}
}
@ -196,11 +196,11 @@ static void elaborate_inductive(buffer<inductive_decl> & decls, level_param_name
}
static environment create_alias(environment const & env, name const & full_id, name const & id, levels const & section_leves,
buffer<parameter> const & section_params, parser & p) {
buffer<expr> const & section_params, parser & p) {
if (in_section(env)) {
expr r = mk_explicit(mk_constant(full_id, section_leves));
for (unsigned i = 0; i < section_params.size(); i++)
r = mk_app(r, section_params[i].m_local);
r = mk_app(r, section_params[i]);
p.add_local_expr(id, r);
return env;
} else if (full_id != id) {
@ -261,7 +261,7 @@ environment inductive_cmd(parser & p) {
// initialize param_universe_scope, we are using implicit universe levels
pu_scope.emplace(p);
}
buffer<parameter> ps;
buffer<expr> ps;
local_environment lenv = env;
auto params_pos = p.pos();
if (!p.curr_is_token(g_colon)) {
@ -329,7 +329,7 @@ environment inductive_cmd(parser & p) {
}
}
update_univ_parameters(ls_buffer, used_levels, p);
buffer<parameter> section_params;
buffer<expr> section_params;
mk_section_params(section_locals, p, section_params);
// First, add section_params to inductive types type.
// We don't update the introduction rules in the first pass, because

19
src/frontends/lean/parameter.h
View file

@ -1,19 +0,0 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "kernel/expr.h"
#include "frontends/lean/parser_pos_provider.h"
namespace lean {
struct parameter {
expr m_local;
binder_info m_bi;
parameter(expr const & l, binder_info const & bi):
m_local(l), m_bi(bi) {}
parameter() {}
};
}

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

@ -354,19 +354,10 @@ void parser::add_local_level(name const & n, level const & l) {
m_local_level_decls.insert(n, l);
}
void parser::add_local_expr(name const & n, parameter const & p) {
void parser::add_local_expr(name const & n, expr const & p) {
m_local_decls.insert(n, p);
}
void parser::add_local_expr(name const & n, expr const & e, binder_info const & bi) {
add_local_expr(n, parameter(e, bi));
}
void parser::add_local(expr const & e, binder_info const & bi) {
lean_assert(is_local(e));
add_local_expr(local_pp_name(e), e, bi);
}
unsigned parser::get_local_level_index(name const & n) const {
return m_local_level_decls.find_idx(n);
}
@ -375,13 +366,6 @@ unsigned parser::get_local_index(name const & n) const {
return m_local_decls.find_idx(n);
}
optional<parameter> parser::get_local(name const & n) const {
if (auto it = m_local_decls.find(n))
return optional<parameter>(*it);
else
return optional<parameter>();
}
/** \brief Parse a sequence of identifiers <tt>ID*</tt>. Store the result in \c result. */
void parser::parse_names(buffer<std::pair<pos_info, name>> & result) {
while (curr_is_identifier()) {
@ -539,7 +523,7 @@ expr parser::elaborate(expr const & e) {
return ::lean::elaborate(m_env, m_ios, e, m_hints, &pp);
}
expr parser::elaborate(expr const & e, name_generator const & ngen, list<parameter> const & ctx) {
expr parser::elaborate(expr const & e, name_generator const & ngen, list<expr> const & ctx) {
parser_pos_provider pp(m_pos_table, get_stream_name(), m_last_cmd_pos);
return ::lean::elaborate(m_env, m_ios, e, ngen, m_hints, substitution(), ctx, &pp);
}
@ -555,7 +539,7 @@ std::pair<expr, expr> parser::elaborate(name const & n, expr const & t, expr con
}
/** \brief Parse <tt>ID ':' expr</tt>, where the expression represents the type of the identifier. */
parameter parser::parse_binder_core(binder_info const & bi) {
expr parser::parse_binder_core(binder_info const & bi) {
auto p = pos();
if (!curr_is_identifier())
throw parser_error("invalid binder, identifier expected", p);
@ -568,10 +552,10 @@ parameter parser::parse_binder_core(binder_info const & bi) {
} else {
type = save_pos(mk_expr_placeholder(), p);
}
return parameter(save_pos(mk_local(id, type), p), bi);
return save_pos(mk_local(id, type, bi), p);
}
parameter parser::parse_binder() {
expr parser::parse_binder() {
if (curr_is_identifier()) {
return parse_binder_core(binder_info());
} else if (curr_is_token(g_lparen)) {
@ -611,7 +595,7 @@ parameter parser::parse_binder() {
\brief Parse <tt>ID ... ID ':' expr</tt>, where the expression
represents the type of the identifiers.
*/
void parser::parse_binder_block(buffer<parameter> & r, binder_info const & bi) {
void parser::parse_binder_block(buffer<expr> & r, binder_info const & bi) {
buffer<std::pair<pos_info, name>> names;
parse_names(names);
if (names.empty())
@ -623,13 +607,13 @@ void parser::parse_binder_block(buffer<parameter> & r, binder_info const & bi) {
}
for (auto p : names) {
expr arg_type = type ? *type : save_pos(mk_expr_placeholder(), p.first);
expr local = save_pos(mk_local(p.second, arg_type), p.first);
add_local_expr(p.second, parameter(local, bi));
r.push_back(parameter(local, bi));
expr local = save_pos(mk_local(p.second, arg_type, bi), p.first);
add_local(local);
r.push_back(local);
}
}
void parser::parse_binders_core(buffer<parameter> & r) {
void parser::parse_binders_core(buffer<expr> & r) {
if (curr_is_identifier()) {
parse_binder_block(r, binder_info());
} else if (curr_is_token(g_lparen)) {
@ -662,7 +646,7 @@ void parser::parse_binders_core(buffer<parameter> & r) {
parse_binders_core(r);
}
local_environment parser::parse_binders(buffer<parameter> & r) {
local_environment parser::parse_binders(buffer<expr> & r) {
flet<environment> save(m_env, m_env); // save environment
local_expr_decls::mk_scope scope(m_local_decls);
unsigned old_sz = r.size();
@ -688,8 +672,8 @@ bool parser::parse_local_notation_decl() {
expr parser::parse_notation(parse_table t, expr * left) {
lean_assert(curr() == scanner::token_kind::Keyword);
auto p = pos();
buffer<expr> args;
buffer<parameter> ps;
buffer<expr> args;
buffer<expr> ps;
local_environment lenv(m_env);
pos_info binder_pos;
if (left)
@ -752,11 +736,12 @@ expr parser::parse_notation(parse_table t, expr * left) {
unsigned i = ps.size();
while (i > 0) {
--i;
expr const & l = ps[i].m_local;
expr const & l = ps[i];
if (a.use_lambda_abstraction())
r = save_pos(Fun(l, r, ps[i].m_bi), binder_pos);
r = Fun(l, r);
else
r = save_pos(Pi(l, r, ps[i].m_bi), binder_pos);
r = Pi(l, r);
r = save_pos(r, binder_pos);
args.push_back(r);
r = instantiate_rev(a.get_rec(), args.size(), args.data());
args.pop_back();
@ -831,7 +816,7 @@ expr parser::id_to_expr(name const & id, pos_info const & p) {
}
// locals
if (auto it1 = m_local_decls.find(id))
return copy_with_new_pos(propagate_levels(it1->m_local, ls), p);
return copy_with_new_pos(propagate_levels(*it1, ls), p);
optional<expr> r;
// globals
if (m_env.find(id))
@ -921,32 +906,17 @@ expr parser::parse_expr(unsigned rbp) {
return left;
}
expr parser::parse_scoped_expr(unsigned num_params, parameter const * ps, local_environment const & lenv, unsigned rbp) {
expr parser::parse_scoped_expr(unsigned num_ps, expr const * ps, local_environment const & lenv, unsigned rbp) {
local_scope scope(*this);
m_env = lenv;
for (unsigned i = 0; i < num_params; i++)
add_local(ps[i].m_local, ps[i].m_bi);
for (unsigned i = 0; i < num_ps; i++)
add_local(ps[i]);
return parse_expr(rbp);
}
expr parser::abstract(unsigned num_params, parameter const * ps, expr const & e, bool lambda, pos_info const & p) {
buffer<expr> locals;
for (unsigned i = 0; i < num_params; i++)
locals.push_back(ps[i].m_local);
expr r = ::lean::abstract(e, locals.size(), locals.data());
unsigned i = num_params;
while (i > 0) {
--i;
expr const & l = ps[i].m_local;
name const & n = local_pp_name(l);
expr type = ::lean::abstract(mlocal_type(l), i, locals.data());
if (lambda)
r = mk_lambda(n, type, r, ps[i].m_bi);
else
r = mk_pi(n, type, r, ps[i].m_bi);
r = save_pos(r, p);
}
return r;
expr parser::abstract(unsigned num_ps, expr const * ps, expr const & e, bool lambda, pos_info const & p) {
expr r = lambda ? Fun(num_ps, ps, e) : Pi(num_ps, ps, e);
return rec_save_pos(r, p);
}
/** \brief Throw an exception if \c e contains a local constant that is not marked as contextual in \c local_decls */
@ -955,7 +925,7 @@ static void check_only_contextual_locals(expr const & e, local_expr_decls const
if (is_local(e)) {
auto it = local_decls.find(mlocal_name(e));
lean_assert(it);
if (!it->m_bi.is_contextual())
if (!local_info(*it).is_contextual())
throw parser_error(sstream() << "invalid 'apply' tactic, it references non-contextual local '"
<< local_pp_name(e) << "'", pos);
}
@ -965,10 +935,10 @@ static void check_only_contextual_locals(expr const & e, local_expr_decls const
/** \brief Return a list of all contextual parameters in local_decls */
static list<parameter> collect_contextual_parameters(local_expr_decls const & local_decls) {
buffer<parameter> tmp;
for (parameter const & p : local_decls.get_values()) {
if (p.m_bi.is_contextual() && is_local(p.m_local))
static list<expr> collect_contextual_parameters(local_expr_decls const & local_decls) {
buffer<expr> tmp;
for (expr const & p : local_decls.get_values()) {
if (is_local(p) && local_info(p).is_contextual())
tmp.push_back(p);
}
return to_list(tmp.begin(), tmp.end());
@ -978,7 +948,7 @@ tactic parser::parse_exact_apply() {
auto p = pos();
expr e = parse_expr();
check_only_contextual_locals(e, m_local_decls, p);
list<parameter> ctx = collect_contextual_parameters(m_local_decls);
list<expr> ctx = collect_contextual_parameters(m_local_decls);
return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) {
if (empty(s.get_goals()))
return none_proof_state();
@ -988,17 +958,14 @@ tactic parser::parse_exact_apply() {
auto const & s_locals = s.get_init_locals();
// Remark: the proof state initial hypotheses (s_locals) are essentially ctx "after elaboration".
// So, to process \c e, we must first replace its local constants with (s_locals).
// We should also create a new_ctx based on (s_locals), but using the binder info from ctx.
name_generator ngen = s.ngen();
lean_assert(length(s_locals) == length(ctx));
buffer<parameter> new_ctx;
buffer<expr> locals;
auto it1 = ctx;
auto it2 = s_locals;
while (!is_nil(it1) && !is_nil(it2)) {
auto const & p = head(it1);
locals.push_back(p.m_local);
new_ctx.push_back(parameter(head(it2), p.m_bi));
locals.push_back(p);
it1 = tail(it1);
it2 = tail(it2);
}
@ -1008,7 +975,7 @@ tactic parser::parse_exact_apply() {
new_e = instantiate(new_e, l);
parser_pos_provider pp(m_pos_table, get_stream_name(), m_last_cmd_pos);
new_e = ::lean::elaborate(env, ios, new_e, g.get_conclusion(), ngen.mk_child(),
m_hints, to_list(new_ctx.begin(), new_ctx.end()), &pp);
m_hints, s_locals, &pp);
proof_builder new_pb = add_proof(s.get_pb(), gname, new_e);
return some_proof_state(proof_state(s, new_gs, new_pb, ngen));
});
@ -1018,7 +985,7 @@ tactic parser::parse_apply() {
auto p = pos();
expr e = parse_expr();
check_only_contextual_locals(e, m_local_decls, p);
list<parameter> ctx = collect_contextual_parameters(m_local_decls);
list<expr> ctx = collect_contextual_parameters(m_local_decls);
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
name_generator ngen = s.ngen();
auto const & s_locals = s.get_init_locals();
@ -1026,7 +993,7 @@ tactic parser::parse_apply() {
proof_state new_s(s, ngen);
buffer<expr> tmp;
for (auto const & p : ctx)
tmp.push_back(p.m_local);
tmp.push_back(p);
std::reverse(tmp.begin(), tmp.end());
new_e = abstract_locals(new_e, tmp.size(), tmp.data());
for (auto const & l : s_locals)
@ -1224,14 +1191,14 @@ static unsigned to_rbp(lua_State * L, int idx) {
return idx < nargs ? 0 : lua_tointeger(L, idx);
}
typedef std::pair<local_environment, std::vector<parameter>> local_scope_cell;
typedef std::pair<local_environment, std::vector<expr>> local_scope_cell;
typedef std::shared_ptr<local_scope_cell> local_scope;
DECL_UDATA(local_scope);
static const struct luaL_Reg local_scope_m[] = {
{"__gc", local_scope_gc},
{0, 0}
};
int push_local_scope_ext(lua_State * L, local_environment const & lenv, buffer<parameter> const & ps) {
int push_local_scope_ext(lua_State * L, local_environment const & lenv, buffer<expr> const & ps) {
local_scope r = std::make_shared<local_scope_cell>();
r->first = lenv;
for (auto const & p : ps)
@ -1254,12 +1221,12 @@ static int parse_level(lua_State * L) { return push_level(L, gparser.parse_leve
static int parse_expr(lua_State * L) { return push_expr(L, gparser.parse_expr(to_rbp(L, 1))); }
static int parse_led(lua_State * L) { return push_expr(L, gparser.parse_led(to_expr(L, 1))); }
static int parse_binders(lua_State * L) {
buffer<parameter> ps;
buffer<expr> ps;
auto lenv = gparser.parse_binders(ps);
return push_local_scope_ext(L, lenv, ps);
}
static int parse_binder(lua_State * L) {
buffer<parameter> ps;
buffer<expr> ps;
ps.push_back(gparser.parse_binder());
return push_local_scope_ext(L, gparser.env(), ps);
}

46
src/frontends/lean/parser.h
View file

@ -19,7 +19,6 @@ Author: Leonardo de Moura
#include "library/io_state.h"
#include "library/io_state_stream.h"
#include "library/kernel_bindings.h"
#include "frontends/lean/parameter.h"
#include "frontends/lean/hint_table.h"
#include "frontends/lean/scanner.h"
#include "frontends/lean/local_decls.h"
@ -37,9 +36,9 @@ struct parser_error : public exception {
};
struct interrupt_parser {};
typedef local_decls<parameter> local_expr_decls;
typedef local_decls<level> local_level_decls;
typedef environment local_environment;
typedef local_decls<expr> local_expr_decls;
typedef local_decls<level> local_level_decls;
typedef environment local_environment;
class parser {
environment m_env;
@ -118,9 +117,9 @@ class parser {
expr parse_numeral_expr();
expr parse_decimal_expr();
expr parse_string_expr();
parameter parse_binder_core(binder_info const & bi);
void parse_binder_block(buffer<parameter> & r, binder_info const & bi);
void parse_binders_core(buffer<parameter> & r);
expr parse_binder_core(binder_info const & bi);
void parse_binder_block(buffer<expr> & r, binder_info const & bi);
void parse_binders_core(buffer<expr> & r);
tactic parse_exact_apply();
friend environment section_cmd(parser & p);
@ -204,43 +203,42 @@ public:
level parse_level(unsigned rbp = 0);
parameter parse_binder();
local_environment parse_binders(buffer<parameter> & r);
expr parse_binder();
local_environment parse_binders(buffer<expr> & r);
/** \brief Convert an identifier into an expression (constant or local constant) based on the current scope */
expr id_to_expr(name const & id, pos_info const & p);
expr parse_expr(unsigned rbp = 0);
expr parse_led(expr left);
expr parse_scoped_expr(unsigned num_params, parameter const * ps, local_environment const & lenv, unsigned rbp = 0);
expr parse_scoped_expr(buffer<parameter> & ps, local_environment const & lenv, unsigned rbp = 0) {
expr parse_scoped_expr(unsigned num_params, expr const * ps, local_environment const & lenv, unsigned rbp = 0);
expr parse_scoped_expr(buffer<expr> & ps, local_environment const & lenv, unsigned rbp = 0) {
return parse_scoped_expr(ps.size(), ps.data(), lenv, rbp);
}
expr parse_scoped_expr(unsigned num_params, parameter const * ps, unsigned rbp = 0) {
expr parse_scoped_expr(unsigned num_params, expr const * ps, unsigned rbp = 0) {
return parse_scoped_expr(num_params, ps, local_environment(m_env), rbp);
}
expr parse_scoped_expr(buffer<parameter> & ps, unsigned rbp = 0) { return parse_scoped_expr(ps.size(), ps.data(), rbp); }
expr abstract(unsigned num_params, parameter const * ps, expr const & e, bool lambda, pos_info const & p);
expr abstract(buffer<parameter> const & ps, expr const & e, bool lambda, pos_info const & p) { return abstract(ps.size(), ps.data(), e, lambda, p); }
expr lambda_abstract(buffer<parameter> const & ps, expr const & e, pos_info const & p) { return abstract(ps, e, true, p); }
expr pi_abstract(buffer<parameter> const & ps, expr const & e, pos_info const & p) { return abstract(ps, e, false, p); }
expr lambda_abstract(buffer<parameter> const & ps, expr const & e) { return lambda_abstract(ps, e, pos_of(e)); }
expr pi_abstract(buffer<parameter> const & ps, expr const & e) { return pi_abstract(ps, e, pos_of(e)); }
expr parse_scoped_expr(buffer<expr> & ps, unsigned rbp = 0) { return parse_scoped_expr(ps.size(), ps.data(), rbp); }
expr abstract(unsigned num_params, expr const * ps, expr const & e, bool lambda, pos_info const & p);
expr abstract(buffer<expr> const & ps, expr const & e, bool lambda, pos_info const & p) { return abstract(ps.size(), ps.data(), e, lambda, p); }
expr lambda_abstract(buffer<expr> const & ps, expr const & e, pos_info const & p) { return abstract(ps, e, true, p); }
expr pi_abstract(buffer<expr> const & ps, expr const & e, pos_info const & p) { return abstract(ps, e, false, p); }
expr lambda_abstract(buffer<expr> const & ps, expr const & e) { return lambda_abstract(ps, e, pos_of(e)); }
expr pi_abstract(buffer<expr> const & ps, expr const & e) { return pi_abstract(ps, e, pos_of(e)); }
tactic parse_tactic(unsigned rbp = 0);
tactic parse_apply();
struct local_scope { parser & m_p; environment m_env; local_scope(parser & p); ~local_scope(); };
void add_local_level(name const & n, level const & l);
void add_local_expr(name const & n, parameter const & p);
void add_local_expr(name const & n, expr const & e, binder_info const & bi = binder_info());
void add_local(expr const & e, binder_info const & bi = binder_info());
void add_local_expr(name const & n, expr const & p);
void add_local(expr const & p) { return add_local_expr(local_pp_name(p), p); }
/** \brief Position of the local level declaration named \c n in the sequence of local level decls. */
unsigned get_local_level_index(name const & n) const;
/** \brief Position of the local declaration named \c n in the sequence of local decls. */
unsigned get_local_index(name const & n) const;
/** \brief Return the local parameter named \c n */
optional<parameter> get_local(name const & n) const;
expr const * get_local(name const & n) const { return m_local_decls.find(n); }
/**
\brief By default, \c mk_Type returns <tt>Type.{_}</tt> where '_' is a new placeholder.
This scope object allows us to temporarily change this behavior.
@ -265,7 +263,7 @@ public:
struct no_undef_id_error_scope { parser & m_p; bool m_old; no_undef_id_error_scope(parser &); ~no_undef_id_error_scope(); };
expr elaborate(expr const & e);
expr elaborate(expr const & e, name_generator const & ngen, list<parameter> const & ctx);
expr elaborate(expr const & e, name_generator const & ngen, list<expr> const & ctx);
expr elaborate(environment const & env, expr const & e);
std::pair<expr, expr> elaborate(name const & n, expr const & t, expr const & v);

43
src/kernel/abstract.cpp
View file

@ -47,32 +47,23 @@ expr abstract_locals(expr const & e, unsigned n, expr const * subst) {
});
}
#define MkBinder(FName) \
expr FName(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 = FName(p.first, p.second, r); \
} \
return r; \
template<bool is_lambda>
expr mk_binding(unsigned num, expr const * locals, expr const & b) {
expr r = abstract_locals(b, num, locals);
unsigned i = num;
while (i > 0) {
--i;
expr const & l = locals[i];
expr t = abstract_locals(mlocal_type(l), i, locals);
if (is_lambda)
r = mk_lambda(local_pp_name(l), t, r, local_info(l));
else
r = mk_pi(local_pp_name(l), t, r, local_info(l));
}
return r;
}
MkBinder(Fun);
MkBinder(Pi);
#define MkBinder2(FName, Mk) \
expr FName(unsigned num, expr const * locals, expr const & b) { \
expr r = b; \
unsigned i = num; \
while (i > 0) { \
--i; \
r = Mk(local_pp_name(locals[i]), mlocal_type(locals[i]), abstract(r, locals[i])); \
} \
return r; \
}
MkBinder2(Fun, mk_lambda);
MkBinder2(Pi, mk_pi);
expr Pi(unsigned num, expr const * locals, expr const & b) { return mk_binding<false>(num, locals, b); }
expr Fun(unsigned num, expr const * locals, expr const & b) { return mk_binding<true>(num, locals, b); }
}

20
src/kernel/abstract.h
View file

@ -32,17 +32,11 @@ inline expr abstract_local(expr const & e, expr const & s) { return abstract_loc
inline expr Fun(name const & n, expr const & t, expr const & b, binder_info const & bi = binder_info()) {
return mk_lambda(n, t, abstract(b, mk_constant(n)), bi);
}
inline expr Fun(expr const & n, expr const & t, expr const & b, binder_info const & bi = binder_info()) {
return mk_lambda(named_expr_name(n), t, abstract(b, n), bi);
}
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 lambda-expression by abstracting the given local constants over b */
expr Fun(unsigned num, expr const * locals, expr const & b);
inline expr Fun(expr const & local, expr const & b) { return Fun(1, &local, b); }
inline expr Fun(std::initializer_list<expr> const & locals, expr const & b) { return Fun(locals.size(), locals.begin(), b); }
template<typename T> expr Fun(T const & locals, expr const & b) { return Fun(locals.size(), locals.data(), b); }
inline expr Fun(expr const & local, expr const & b, binder_info const & bi = binder_info()) {
return Fun(local_pp_name(local), mlocal_type(local), abstract(b, local), bi);
}
/**
\brief Create a Pi expression (pi (x : t) b), the term b is abstracted using abstract(b, constant(x)).
@ -50,15 +44,9 @@ inline expr Fun(expr const & local, expr const & b, binder_info const & bi = bin
inline expr Pi(name const & n, expr const & t, expr const & b, binder_info const & bi = binder_info()) {
return mk_pi(n, t, abstract(b, mk_constant(n)), bi);
}
inline expr Pi(expr const & n, expr const & t, expr const & b, binder_info const & bi = binder_info()) {
return mk_pi(named_expr_name(n), t, abstract(b, n), bi);
}
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);
/** \brief Create a Pi-expression by abstracting the given local constants over b */
expr Pi(unsigned num, expr const * locals, expr const & b);
inline expr Pi(expr const & local, expr const & b) { return Pi(1, &local, b); }
inline expr Pi(std::initializer_list<expr> const & locals, expr const & b) { return Pi(locals.size(), locals.begin(), b); }
template<typename T> expr Pi(T const & locals, expr const & b) { return Pi(locals.size(), locals.data(), b); }
inline expr Pi(expr const & local, expr const & b, binder_info const & bi = binder_info()) {
return Pi(local_pp_name(local), mlocal_type(local), abstract(b, local), bi);
}
}

2
src/kernel/converter.cpp
View file

@ -271,7 +271,7 @@ struct default_converter : public converter {
expr var_s_type = instantiate_rev(binding_domain(s), subst.size(), subst.data());
if (!is_def_eq(var_t_type, var_s_type, c, jst))
return false;
subst.push_back(mk_local(mk_fresh_name(c), binding_name(s), var_s_type));
subst.push_back(mk_local(mk_fresh_name(c), binding_name(s), var_s_type, binding_info(s)));
t = binding_body(t);
s = binding_body(s);
} while (t.kind() == k && s.kind() == k);

18
src/kernel/expr.cpp
View file

@ -115,9 +115,10 @@ void expr_mlocal::dealloc(buffer<expr_cell*> & todelete) {
delete(this);
}
expr_local::expr_local(name const & n, name const & pp_name, expr const & t):
expr_local::expr_local(name const & n, name const & pp_name, expr const & t, binder_info const & bi):
expr_mlocal(false, n, t),
m_pp_name(pp_name) {}
m_pp_name(pp_name),
m_bi(bi) {}
void expr_local::dealloc(buffer<expr_cell*> & todelete) {
dec_ref(m_type, todelete);
delete(this);
@ -275,7 +276,9 @@ expr mk_var(unsigned idx) { return cache(expr(new expr_var(idx))); }
expr mk_constant(name const & n, levels const & ls) { return cache(expr(new expr_const(n, ls))); }
expr mk_macro(macro_definition const & m, unsigned num, expr const * args) { return cache(expr(new expr_macro(m, num, args))); }
expr mk_metavar(name const & n, expr const & t) { return cache(expr(new expr_mlocal(true, n, t))); }
expr mk_local(name const & n, name const & pp_n, expr const & t) { return cache(expr(new expr_local(n, pp_n, t))); }
expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info const & bi) {
return cache(expr(new expr_local(n, pp_n, t, bi)));
}
expr mk_app(expr const & f, expr const & a) { return cache(expr(new expr_app(f, a))); }
expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info const & i) {
return cache(expr(new expr_binding(k, n, t, e, i)));
@ -502,7 +505,14 @@ expr update_mlocal(expr const & e, expr const & new_type) {
else if (is_metavar(e))
return copy_tag(e, mk_metavar(mlocal_name(e), new_type));
else
return copy_tag(e, mk_local(mlocal_name(e), local_pp_name(e), new_type));
return copy_tag(e, mk_local(mlocal_name(e), local_pp_name(e), new_type, local_info(e)));
}
expr update_local(expr const & e, expr const & new_type, binder_info const & bi) {
if (is_eqp(mlocal_type(e), new_type) && local_info(e) == bi)
return e;
else
return copy_tag(e, mk_local(mlocal_name(e), local_pp_name(e), new_type, bi));
}
expr update_sort(expr const & e, level const & new_level) {

87
src/kernel/expr.h
View file

@ -21,6 +21,7 @@ Author: Leonardo de Moura
#include "util/optional.h"
#include "util/serializer.h"
#include "util/sexpr/format.h"
#include "util/name_generator.h"
#include "kernel/level.h"
#include "kernel/extension_context.h"
@ -126,7 +127,7 @@ public:
friend expr mk_sort(level const & l);
friend expr mk_constant(name const & n, levels const & ls);
friend expr mk_metavar(name const & n, expr const & t);
friend expr mk_local(name const & n, name const & pp_n, expr const & t);
friend expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info const & bi);
friend expr mk_app(expr const & f, expr const & a);
friend expr mk_pair(expr const & f, expr const & s, expr const & t);
friend expr mk_proj(bool fst, expr const & p);
@ -200,42 +201,6 @@ public:
expr const & get_type() const { return m_type; }
};
/** \brief expr_mlocal subclass for local constants. */
class expr_local : public expr_mlocal {
// The name used in the binder that generate this local,
// it is only used for pretty printing. This field is ignored
// when comparing expressions.
name m_pp_name;
friend expr_cell;
void dealloc(buffer<expr_cell*> & todelete);
public:
expr_local(name const & n, name const & pp_name, expr const & t);
name const & get_pp_name() const { return m_pp_name; }
};
/** \brief Composite expressions */
class expr_composite : public expr_cell {
protected:
unsigned m_depth;
unsigned m_free_var_range;
friend unsigned get_depth(expr const & e);
friend unsigned get_free_var_range(expr const & e);
public:
expr_composite(expr_kind k, unsigned h, bool has_mv, bool has_local, bool has_param_univ, unsigned d, unsigned fv_range);
};
/** \brief Applications */
class expr_app : public expr_composite {
expr m_fn;
expr m_arg;
friend expr_cell;
void dealloc(buffer<expr_cell*> & todelete);
public:
expr_app(expr const & fn, expr const & arg);
expr const & get_fn() const { return m_fn; }
expr const & get_arg() const { return m_arg; }
};
/**
\brief Auxiliary annotation for binders (Lambda and Pi). This information
is only used for elaboration.
@ -262,6 +227,44 @@ inline binder_info mk_contextual_info(bool f) { return binder_info(false, false,
bool operator==(binder_info const & i1, binder_info const & i2);
inline bool operator!=(binder_info const & i1, binder_info const & i2) { return !(i1 == i2); }
/** \brief expr_mlocal subclass for local constants. */
class expr_local : public expr_mlocal {
// The name used in the binder that generate this local,
// it is only used for pretty printing. This field is ignored
// when comparing expressions.
name m_pp_name;
binder_info m_bi;
friend expr_cell;
void dealloc(buffer<expr_cell*> & todelete);
public:
expr_local(name const & n, name const & pp_name, expr const & t, binder_info const & bi);
name const & get_pp_name() const { return m_pp_name; }
binder_info const & get_info() const { return m_bi; }
};
/** \brief Composite expressions */
class expr_composite : public expr_cell {
protected:
unsigned m_depth;
unsigned m_free_var_range;
friend unsigned get_depth(expr const & e);
friend unsigned get_free_var_range(expr const & e);
public:
expr_composite(expr_kind k, unsigned h, bool has_mv, bool has_local, bool has_param_univ, unsigned d, unsigned fv_range);
};
/** \brief Applications */
class expr_app : public expr_composite {
expr m_fn;
expr m_arg;
friend expr_cell;
void dealloc(buffer<expr_cell*> & todelete);
public:
expr_app(expr const & fn, expr const & arg);
expr const & get_fn() const { return m_fn; }
expr const & get_arg() const { return m_arg; }
};
class binder {
friend class expr_binding;
name m_name;
@ -418,8 +421,10 @@ inline expr mk_constant(name const & n) { return mk_constant(n, levels()); }
inline expr Const(name const & n) { return mk_constant(n); }
expr mk_macro(macro_definition const & m, unsigned num = 0, expr const * args = nullptr);
expr mk_metavar(name const & n, expr const & t);
expr mk_local(name const & n, name const & pp_n, expr const & t);
inline expr mk_local(name const & n, expr const & t) { return mk_local(n, n, t); }
expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info const & bi);
inline expr mk_local(name const & n, expr const & t) { return mk_local(n, n, t, binder_info()); }
inline expr mk_local(name const & n, expr const & t, binder_info const & bi) { return mk_local(n, n, t, bi); }
inline expr Local(name const & n, expr const & t, binder_info const & bi = binder_info()) { return mk_local(n, t, bi); }
expr mk_app(expr const & f, expr const & a);
expr mk_app(expr const & f, unsigned num_args, expr const * args);
expr mk_app(unsigned num_args, expr const * args);
@ -483,6 +488,8 @@ inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3,
/** \brief Return application (...((f x_{n-1}) x_{n-2}) ... x_0) */
expr mk_app_vars(expr const & f, unsigned n);
expr mk_local_for(expr const & b, name_generator const & ngen);
bool enable_expr_caching(bool f);
/** \brief Helper class for temporarily enabling/disabling expression caching */
struct scoped_expr_caching {
@ -560,6 +567,7 @@ inline level const & sort_level(expr const & e) { return to_sort(e)-
inline name const & mlocal_name(expr const & e) { return to_mlocal(e)->get_name(); }
inline expr const & mlocal_type(expr const & e) { return to_mlocal(e)->get_type(); }
inline name const & local_pp_name(expr const & e) { return to_local(e)->get_pp_name(); }
inline binder_info const & local_info(expr const & e) { return to_local(e)->get_info(); }
inline bool is_constant(expr const & e, name const & n) { return is_constant(e) && const_name(e) == n; }
inline bool has_metavar(expr const & e) { return e.has_metavar(); }
@ -643,6 +651,7 @@ template<typename C> expr update_rev_app(expr const & e, C const & c) { return u
expr update_binding(expr const & e, expr const & new_domain, expr const & new_body);
expr update_binding(expr const & e, expr const & new_domain, expr const & new_body, binder_info const & bi);
expr update_mlocal(expr const & e, expr const & new_type);
expr update_local(expr const & e, expr const & new_type, binder_info const & bi);
expr update_sort(expr const & e, level const & new_level);
expr update_constant(expr const & e, levels const & new_levels);
expr update_macro(expr const & e, unsigned num, expr const * args);

7
src/kernel/expr_eq_fn.cpp
View file

@ -32,10 +32,15 @@ bool expr_eq_fn::apply(expr const & a, expr const & b) {
return
const_name(a) == const_name(b) &&
compare(const_levels(a), const_levels(b), [](level const & l1, level const & l2) { return l1 == l2; });
case expr_kind::Local: case expr_kind::Meta:
case expr_kind::Meta:
return
mlocal_name(a) == mlocal_name(b) &&
apply(mlocal_type(a), mlocal_type(b));
case expr_kind::Local:
return
mlocal_name(a) == mlocal_name(b) &&
apply(mlocal_type(a), mlocal_type(b)) &&
(!m_compare_binder_info || local_info(a) == local_info(b));
case expr_kind::App:
m_counter++;
return

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

@ -219,7 +219,7 @@ struct add_inductive_fn {
name mk_fresh_name() { return m_ngen.next(); }
/** \brief Create a local constant for the given binding. */
expr mk_local_for(expr const & b) { return mk_local(mk_fresh_name(), binding_name(b), binding_domain(b)); }
expr mk_local_for(expr const & b) { return mk_local(mk_fresh_name(), binding_name(b), binding_domain(b), binding_info(b)); }
/** \brief Return type of the i-th global parameter. */
expr get_param_type(unsigned i) { return mlocal_type(m_param_consts[i]); }
@ -523,7 +523,7 @@ struct add_inductive_fn {
}
i++;
}
info.m_major_premise = mk_local(mk_fresh_name(), "n", mk_app(mk_app(m_it_consts[d_idx], m_param_consts), info.m_indices));
info.m_major_premise = mk_local(mk_fresh_name(), "n", mk_app(mk_app(m_it_consts[d_idx], m_param_consts), info.m_indices), binder_info());
expr C_ty = mk_sort(m_elim_level);
if (m_dep_elim)
C_ty = Pi(info.m_major_premise, C_ty);
@ -531,7 +531,7 @@ struct add_inductive_fn {
name C_name("C");
if (get_num_its() > 1)
C_name = name(C_name).append_after(d_idx+1);
info.m_C = mk_local(mk_fresh_name(), C_name, C_ty);
info.m_C = mk_local(mk_fresh_name(), C_name, C_ty, binder_info());
m_elim_info.push_back(info);
d_idx++;
}
@ -583,11 +583,11 @@ struct add_inductive_fn {
C_app = mk_app(C_app, u_app);
}
expr v_i_ty = Pi(xs, C_app);
expr v_i = mk_local(mk_fresh_name(), name("v").append_after(i), v_i_ty);
expr v_i = mk_local(mk_fresh_name(), name("v").append_after(i), v_i_ty, binder_info());
v.push_back(v_i);
}
expr minor_ty = Pi(b, Pi(u, Pi(v, C_app)));
expr minor = mk_local(mk_fresh_name(), name("e").append_after(minor_idx), minor_ty);
expr minor = mk_local(mk_fresh_name(), name("e").append_after(minor_idx), minor_ty, binder_info());
m_elim_info[d_idx].m_minor_premises.push_back(minor);
minor_idx++;
}

2
src/kernel/type_checker.cpp
View file

@ -49,7 +49,7 @@ optional<expr> type_checker::expand_macro(expr const & m) {
It also returns the fresh local constant.
*/
std::pair<expr, expr> type_checker::open_binding_body(expr const & e) {
expr local = mk_local(m_gen.next(), binding_name(e), binding_domain(e));
expr local = mk_local(m_gen.next(), binding_name(e), binding_domain(e), binding_info(e));
return mk_pair(instantiate(binding_body(e), local), local);
}

2
src/library/deep_copy.cpp
View file

@ -20,7 +20,7 @@ expr copy(expr const & a) {
case expr_kind::Lambda: return mk_lambda(binding_name(a), binding_domain(a), binding_body(a), binding_info(a));
case expr_kind::Pi: return mk_pi(binding_name(a), binding_domain(a), binding_body(a), binding_info(a));
case expr_kind::Meta: return mk_metavar(mlocal_name(a), mlocal_type(a));
case expr_kind::Local: return mk_local(mlocal_name(a), local_pp_name(a), mlocal_type(a));
case expr_kind::Local: return mk_local(mlocal_name(a), local_pp_name(a), mlocal_type(a), local_info(a));
}
lean_unreachable(); // LCOV_EXCL_LINE
}

119
src/library/kernel_bindings.cpp
View file

@ -381,115 +381,24 @@ static int expr_mk_arrow(lua_State * L) {
return push_expr(L, r);
}
static void throw_invalid_binder_table(int t) {
#define VALID_FORMS "local_name, {local_name, bool}, {expr, expr}, {expr, expr, bool}, or {expr, expr, binder_info}, each entry represents a binder, the first expression in each entry must be a (local) constant, the second expression is the type, the optional Boolean can be used to mark implicit arguments."
if (t > 0)
throw exception(sstream() << "arg #" << t << " must be a table {e_1, ..., e_k} where each entry e_i is of the form: " VALID_FORMS);
else
throw exception(sstream() << "invalid binder, it must of the form: " VALID_FORMS);
}
// t is a table of tuples {{a1, b1}, ..., {ak, bk}}
// Each tuple represents a binder
static std::tuple<expr, expr, binder_info> get_binder_from_table(lua_State * L, int t, int i) {
lua_pushvalue(L, t); // push table on the top
lua_pushinteger(L, i);
lua_gettable(L, -2); // now table tuple {ai, bi} is on the top
int tuple_sz = objlen(L, -1);
if (is_expr(L, -1)) {
expr const & e = to_expr(L, -1);
if (!is_local(e))
throw_invalid_binder_table(t);
return std::make_tuple(e, mlocal_type(e), binder_info());
}
if (!lua_istable(L, -1) || (tuple_sz != 2 && tuple_sz != 3))
throw_invalid_binder_table(t);
lua_rawgeti(L, -1, 1);
if (!is_expr(L, -1))
throw_invalid_binder_table(t);
expr ai = to_expr(L, -1);
if (!is_constant(ai) && !is_local(ai))
throw_invalid_binder_table(t);
lua_pop(L, 1);
binder_info ii;
lua_rawgeti(L, -1, 2);
if (is_expr(L, -1)) {
expr bi = to_expr(L, -1);
lua_pop(L, 1);
if (tuple_sz == 3) {
lua_rawgeti(L, -1, 3);
if (lua_isboolean(L, -1))
ii = binder_info(lua_toboolean(L, -1));
else if (is_binder_info(L, -1))
ii = to_binder_info(L, -1);
else
throw_invalid_binder_table(t);
lua_pop(L, 1);
}
return std::make_tuple(ai, bi, ii);
} else {
if (!is_local(ai))
throw_invalid_binder_table(t);
if (lua_isboolean(L, -1))
ii = binder_info(lua_toboolean(L, -1));
else if (is_binder_info(L, -1))
ii = to_binder_info(L, -1);
else
throw_invalid_binder_table(t);
lua_pop(L, 1);
return std::make_tuple(ai, mlocal_type(ai), ii);
}
}
typedef expr (*MkAbst1)(expr const & n, expr const & t, expr const & b);
typedef expr (*MkAbst2)(name const & n, expr const & t, expr const & b);
template<bool pi>
static int expr_abst(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs < 2)
throw exception("function must have at least 2 arguments");
if (nargs == 2) {
if (is_expr(L, 1) && is_local(to_expr(L, 1))) {
if (pi)
return push_expr(L, Pi(to_expr(L, 1), to_expr(L, 2)));
else
return push_expr(L, Fun(to_expr(L, 1), to_expr(L, 2)));
} else if (lua_istable(L, 1)) {
int len = objlen(L, 1);
if (len == 0)
throw exception("function expects arg #1 to be a non-empty table");
expr r = to_expr(L, 2);
for (int i = len; i >= 1; i--) {
auto p = get_binder_from_table(L, 1, i);
if (pi)
r = Pi(std::get<0>(p), std::get<1>(p), r, std::get<2>(p));
else
r = Fun(std::get<0>(p), std::get<1>(p), r, std::get<2>(p));
}
return push_expr(L, r);
} else {
throw exception("function expects arg #1 to be a local constant or a table of the form '{{expr, expr}, ...}'");
}
} else {
if (nargs % 2 == 0)
throw exception("function must have an odd number of arguments");
expr r = to_expr(L, nargs);
for (int i = nargs - 1; i >= 1; i-=2) {
if (is_expr(L, i - 1)) {
if (pi)
r = Pi(to_expr(L, i - 1), to_expr(L, i), r);
else
r = Fun(to_expr(L, i - 1), to_expr(L, i), r);
} else {
if (pi)
r = Pi(to_name_ext(L, i - 1), to_expr(L, i), r);
else
r = Fun(to_name_ext(L, i - 1), to_expr(L, i), r);
}
}
return push_expr(L, r);
check_atleast_num_args(L, 2);
expr r = to_expr(L, nargs);
for (int i = nargs - 1; i >= 1; i -= 1) {
expr l = to_expr(L, i);
if (!is_local(l))
throw exception(sstream() << "arg #" << i << " must be a local constants");
if (pi)
r = Pi(l, r);
else
r = Fun(l, r);
}
return push_expr(L, r);
}
static int expr_fun(lua_State * L) { return expr_abst<false>(L); }
@ -501,8 +410,12 @@ static int expr_mk_local(lua_State * L) {
name n = to_name_ext(L, 1);
if (nargs == 2)
return push_expr(L, mk_local(n, to_expr(L, 2)));
else if (nargs == 3 && is_binder_info(L, 3))
return push_expr(L, mk_local(n, n, to_expr(L, 2), to_binder_info(L, 3)));
else if (nargs == 3)
return push_expr(L, mk_local(n, to_name_ext(L, 2), to_expr(L, 3), binder_info()));
else
return push_expr(L, mk_local(n, to_name_ext(L, 2), to_expr(L, 3)));
return push_expr(L, mk_local(n, to_name_ext(L, 2), to_expr(L, 3), to_binder_info(L, 4)));
}
static int expr_get_kind(lua_State * L) { return push_integer(L, static_cast<int>(to_expr(L, 1).kind())); }

9
src/library/kernel_serializer.cpp
View file

@ -167,7 +167,7 @@ class expr_serializer : public object_serializer<expr, expr_hash_alloc, expr_eqp
s << mlocal_name(a); write_core(mlocal_type(a));
break;
case expr_kind::Local:
s << mlocal_name(a) << local_pp_name(a); write_core(mlocal_type(a));
s << mlocal_name(a) << local_pp_name(a) << local_info(a); write_core(mlocal_type(a));
break;
}
});
@ -221,9 +221,10 @@ public:
return mk_metavar(n, read());
}
case expr_kind::Local: {
name n = read_name(d);
name pp_n = read_name(d);
return mk_local(n, pp_n, read());
name n = read_name(d);
name pp_n = read_name(d);
binder_info bi = read_binder_info(d);
return mk_local(n, pp_n, read(), bi);
}}
throw_corrupted_file(); // LCOV_EXCL_LINE
});

2
src/library/normalize.cpp
View file

@ -18,7 +18,7 @@ class normalize_fn {
expr normalize_binding(expr const & e) {
expr d = normalize(binding_domain(e));
expr l = mk_local(m_ngen.next(), binding_name(e), d);
expr l = mk_local(m_ngen.next(), binding_name(e), d, binding_info(e));
expr b = abstract(normalize(instantiate(binding_body(e), l)), l);
return update_binding(e, d, b);
}

2
src/library/tactic/proof_state.cpp
View file

@ -98,7 +98,7 @@ static proof_state to_proof_state(environment const * env, expr const & mvar, na
list<expr> init_ls;
hypotheses hs;
while (is_pi(t)) {
expr l = mk_local(ngen.next(), binding_name(t), binding_domain(t));
expr l = mk_local(ngen.next(), binding_name(t), binding_domain(t), binding_info(t));
bool c = true;
if (tc)
c = !tc->is_prop(binding_domain(t));

2
src/library/unifier.cpp
View file

@ -930,7 +930,7 @@ struct unifier_fn {
expr tmp_pi = mk_pi(binding_name(rhs), mk_app_vars(maux1, margs.size()), dontcare); // trick for "extending" the context
expr mtype2 = replace_range(mtype, tmp_pi); // trick for "extending" the context
expr maux2 = mk_aux_metavar_for(mtype2);
expr new_local = mk_local(m_ngen.next(), binding_name(rhs), binding_domain(rhs));
expr new_local = mk_local(m_ngen.next(), binding_name(rhs), binding_domain(rhs), binding_info(rhs));
cs.push_back(mk_eq_cnstr(mk_app(mk_app(maux2, margs), new_local), instantiate(binding_body(rhs), new_local), j));
expr v = update_binding(rhs, mk_app_vars(maux1, margs.size()), mk_app_vars(maux2, margs.size() + 1));
v = mk_lambda_for(mtype, v);

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

@ -55,11 +55,11 @@ static void tst1() {
} catch (kernel_exception & ex) {
std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n";
}
expr A = Const("A");
expr x = Const("x");
expr A = Local("A", Type);
expr x = Local("x", A);
auto env3 = add_decl(env2, mk_definition("id", level_param_names(),
Pi(A, mk_Type(), A >> A),
Fun({{A, mk_Type()}, {x, A}}, x)));
Pi(A, A >> A),
Fun({A, x}, x)));
expr c = mk_local("c", Bool);
expr id = Const("id");
type_checker checker(env3, name_generator("tmp"));
@ -75,17 +75,18 @@ static void tst2() {
environment env;
name base("base");
env = add_decl(env, mk_var_decl(name(base, 0u), level_param_names(), Bool >> (Bool >> Bool)));
expr x = Const("x");
expr y = Const("y");
expr x = Local("x", Bool);
expr y = Local("y", Bool);
for (unsigned i = 1; i <= 100; i++) {
expr prev = Const(name(base, i-1));
env = add_decl(env, mk_definition(env, name(base, i), level_param_names(), Bool >> (Bool >> Bool),
Fun({{x, Bool}, {y, Bool}}, prev(prev(x, y), prev(y, x)))));
Fun({x, y}, prev(prev(x, y), prev(y, x)))));
}
expr A = Const("A");
expr A = Local("A", Type);
expr a = Local("a", A);
env = add_decl(env, mk_definition("id", level_param_names(),
Pi(A, mk_Type(), A >> A),
Fun({{A, mk_Type()}, {x, A}}, x)));
Pi(A, A >> A),
Fun({A, a}, a)));
type_checker checker(env, name_generator("tmp"));
expr f96 = Const(name(base, 96));
expr f97 = Const(name(base, 97));
@ -127,12 +128,12 @@ public:
static void tst3() {
environment env(0, true, true, true, list<name>(), std::unique_ptr<normalizer_extension>(new normalizer_extension_tst()));
expr A = Const("A");
expr x = Const("x");
expr A = Local("A", Type);
expr x = Local("x", A);
expr id = Const("id");
env = add_decl(env, mk_definition("id", level_param_names(),
Pi(A, mk_Type(), A >> A),
Fun({{A, mk_Type()}, {x, A}}, x)));
Pi(A, A >> A),
Fun({A, x}, x)));
expr mk = Const("mk");
expr proj1 = Const("proj1");
expr a = Const("a");

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

@ -276,20 +276,21 @@ static void tst14() {
static void tst15() {
expr f = Const("f");
expr x = Var(0);
expr a = Const("a");
expr a = Local("a", Type);
expr m = mk_metavar("m", Bool);
check_serializer(m);
lean_assert(has_metavar(m));
lean_assert(has_metavar(f(m)));
lean_assert(!has_metavar(f(a)));
lean_assert(!has_metavar(f(x)));
lean_assert(!has_metavar(Pi({a, Type}, a)));
lean_assert(!has_metavar(Pi(a, a)));
lean_assert(!has_metavar(Type));
lean_assert(!has_metavar(Fun({a, Type}, a)));
lean_assert(has_metavar(Pi({a, Type}, m)));
lean_assert(has_metavar(Pi({a, m}, a)));
lean_assert(has_metavar(Fun({a, Type}, m)));
lean_assert(has_metavar(Fun({a, m}, a)));
lean_assert(!has_metavar(Fun(a, a)));
lean_assert(has_metavar(Pi(a, m)));
expr a1 = Local("a", m);
lean_assert(has_metavar(Pi(a1, a1)));
lean_assert(has_metavar(Fun(a, m)));
lean_assert(has_metavar(Fun(a1, a)));
lean_assert(has_metavar(f(a, a, m)));
lean_assert(has_metavar(f(a, m, a, a)));
lean_assert(!has_metavar(f(a, a, a, a)));
@ -331,28 +332,31 @@ static void tst17() {
static void tst18() {
expr f = Const("f");
expr x = Var(0);
expr a = Const("a");
expr l = mk_local("m", Bool);
expr m = mk_metavar("m", Bool);
expr a0 = Const("a");
expr a = Local("a", Type);
expr a1 = Local("a", m);
expr a2 = Local("a", l);
check_serializer(l);
lean_assert(!has_local(m));
lean_assert(has_local(l));
lean_assert(!has_local(f(m)));
lean_assert(has_local(f(l)));
lean_assert(!has_local(f(a)));
lean_assert(!has_local(f(a0)));
lean_assert(!has_local(f(x)));
lean_assert(!has_local(Pi({a, Type}, a)));
lean_assert(!has_local(Pi({a, m}, a)));
lean_assert(!has_local(Pi(a, a)));
lean_assert(!has_local(Pi(a1, a1)));
lean_assert(!has_local(Type));
lean_assert(!has_local(Pi({a, Type}, a)));
lean_assert(has_local(Pi({a, Type}, l)));
lean_assert(!has_metavar(Pi({a, Type}, l)));
lean_assert(has_local(Pi({a, l}, a)));
lean_assert(has_local(Fun({a, Type}, l)));
lean_assert(has_local(Fun({a, l}, a)));
lean_assert(!has_local(Pi(a, a)));
lean_assert(has_local(Pi(a, l)));
lean_assert(!has_metavar(Pi(a, l)));
lean_assert(has_local(Pi(a2, a2)));
lean_assert(has_local(Fun(a, l)));
lean_assert(has_local(Fun(a2, a2)));
lean_assert(has_local(f(a, a, l)));
lean_assert(has_local(f(a, l, a, a)));
lean_assert(!has_local(f(a, a, a, a)));
lean_assert(!has_local(f(a0, a0, a0, a0)));
}
int main() {

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

@ -32,10 +32,10 @@ static void tst1() {
static void tst2() {
expr f = Const("f");
expr x = Const("x");
expr y = Const("y");
expr B = Const("Bool");
expr t = Fun({x, B}, Fun({y, B}, x));
expr x = Local("x", B);
expr y = Local("y", B);
expr t = Fun({x, y}, x);
lean_assert(closed(t));
lean_assert(!closed(binding_body(t)));
}
@ -59,14 +59,14 @@ static void tst3() {
static void tst4() {
expr f = Const("f");
expr x = Const("x");
expr y = Const("y");
expr B = Bool;
expr t = f(Fun({x, B}, Fun({y, B}, f(x, y)))(f(Var(1), Var(2))), x);
expr x = Local("x", B);
expr y = Local("y", B);
expr t = f(Fun({x, y}, f(x, y))(f(Var(1), Var(2))), x);
lean_assert_eq(lift_free_vars(t, 1, 2),
f(Fun({x, B}, Fun({y, B}, f(x, y)))(f(Var(3), Var(4))), x));
f(Fun(x, Fun(y, f(x, y)))(f(Var(3), Var(4))), x));
lean_assert_eq(lift_free_vars(t, 0, 3),
f(Fun({x, B}, Fun({y, B}, f(x, y)))(f(Var(4), Var(5))), x));
f(Fun(x, Fun(y, f(x, y)))(f(Var(4), Var(5))), x));
lean_assert_eq(lift_free_vars(t, 3, 2), t);
}

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

@ -11,23 +11,23 @@ using namespace lean;
static void tst1() {
expr f = Const("f");
expr h = Const("h");
expr x = Const("x");
expr y = Const("y");
expr N = Const("N");
expr x = Local("x", N);
expr y = Local("y", N);
expr h = Local("h", N >> (N >> (N >> N)));
expr a = Const("a");
expr b = Const("b");
expr c = Const("c");
expr d = Const("d");
expr N = Const("N");
expr F1 = Fun({x, N}, x)(f, a);
expr F1 = Fun(x, x)(f, a);
lean_assert(is_head_beta(F1));
lean_assert_eq(head_beta_reduce(F1), f(a));
expr F2 = Fun({{h, N >> (N >> (N >> N))}, {y, N}}, h(y))(f, a, b, c);
expr F2 = Fun({h, y}, h(y))(f, a, b, c);
lean_assert(is_head_beta(F2));
lean_assert_eq(head_beta_reduce(F2), f(a, b, c));
expr F3 = Fun({x, N}, f(Fun({y, N}, y)(x), x))(a);
expr F3 = Fun(x, f(Fun(y, y)(x), x))(a);
lean_assert(is_head_beta(F3));
lean_assert(head_beta_reduce(F3) == f(Fun({y, N}, y)(a), a));
lean_assert(head_beta_reduce(F3) == f(Fun(y, y)(a), a));
lean_assert(beta_reduce(F3) == f(a, a));
}

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

@ -14,12 +14,12 @@ static void tst1() {
max_sharing_fn max_fn;
expr a1 = Const("a");
expr a2 = Const("a");
expr x = Const("x");
expr y = Const("y");
expr f = Const("f");
expr N = Const("N");
expr x = Local("x", N);
expr y = Local("y", N);
expr f = Const("f");
expr F1, F2;
F1 = f(Fun({x, N}, f(x, x)), Fun({y, N}, f(y, y)));
F1 = f(Fun(x, f(x, x)), Fun(y, f(y, y)));
lean_assert(!is_eqp(app_arg(app_fn(F1)), app_arg(F1)));
F2 = max_fn(F1);
std::cout << F2 << "\n";

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

@ -125,13 +125,13 @@ static void tst3() {
substitution s;
expr f = Const("f");
expr g = Const("g");
expr x = Const("x");
expr y = Const("y");
expr a = Const("a");
expr b = Const("b");
s = s.assign(m1, Fun({{x, Bool}, {y, Bool}}, f(y, x)));
expr x = Local("x", Bool);
expr y = Local("y", Bool);
s = s.assign(m1, Fun({x, y}, f(y, x)));
lean_assert_eq(s.instantiate_metavars(m1(a, b, g(a))).first, f(b, a, g(a)));
lean_assert_eq(s.instantiate_metavars(m1(a)).first, Fun({y, Bool}, f(y, a)));
lean_assert_eq(s.instantiate_metavars(m1(a)).first, Fun(y, f(y, a)));
lean_assert_eq(s.instantiate_metavars(m1(a, b)).first, f(b, a));
std::cout << s.instantiate_metavars(m1(a, b, g(a))).first << "\n";
}

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

@ -68,8 +68,6 @@ static expr arg(expr n, unsigned i) {
static void tst3() {
expr f = Const("f");
expr x = Const("x");
expr y = Const("y");
expr c = Const("c");
expr d = Const("d");
expr A = Const("A");
@ -87,12 +85,15 @@ static void tst3() {
return none_expr();
}
};
expr x = Local("x", A);
expr y = Local("y", A);
replace_fn replacer(proc, tracer(trace));
expr t = Fun({{x, A}, {y, A}}, f(x, f(f(f(x, x), f(y, d)), f(d, d))));
expr t = Fun({x, y}, f(x, f(f(f(x, x), f(y, d)), f(d, d))));
expr b = binding_body(t);
expr r = replacer(b);
std::cout << r << "\n";
lean_assert(r == Fun({y, A}, f(c, f(f(f(c, c), f(y, d)), f(d, d)))));
lean_assert(r == Fun(y, f(c, f(f(f(c, c), f(y, d)), f(d, d)))));
for (auto p : trace) {
std::cout << p.first << " --> " << p.second << "\n";
}

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

@ -14,12 +14,13 @@ static void tst1() {
expr a = Const("a");
expr b = Const("b");
expr T = Type;
expr a1 = Local("a", T);
lean_assert(occurs(f, f));
lean_assert(!occurs(a, f));
lean_assert(occurs(a, f(a)));
lean_assert(occurs("a", f(a)));
lean_assert(!occurs("b", f));
lean_assert(!occurs(a, Fun({a, T}, f(a))));
lean_assert(!occurs(a, Fun(a1, f(a1))));
}
int main() {

4
tests/lua/ac.lua
View file

@ -7,8 +7,8 @@ local Acc = Const("Acc", {l})
local x = Local("x", A)
local y = Local("y", A)
env = add_inductive(env,
"Acc", {l}, 2, Pi({A, R, x}, Bool),
"Acc_intro", Pi({A, R, x}, mk_arrow(Pi(y, mk_arrow(R(y, x), Acc(A, R, y))), Acc(A, R, x))))
"Acc", {l}, 2, Pi(A, R, x, Bool),
"Acc_intro", Pi(A, R, x, mk_arrow(Pi(y, mk_arrow(R(y, x), Acc(A, R, y))), Acc(A, R, x))))
function display_type(env, t)
print(tostring(t) .. " : " .. tostring(type_checker(env):infer(t)))

22
tests/lua/acc.lua
View file

@ -13,8 +13,8 @@ local y = Local("y", A)
local Acc = Const("Acc", {l})
env = add_inductive(env,
"Acc", {l}, 2, Pi({A, R, x}, mk_sort(l+1)),
"Acc_intro", Pi({A, R, x}, mk_arrow(Pi(y, mk_arrow(R(y, x), Acc(A, R, y))), Acc(A, R, x))))
"Acc", {l}, 2, Pi(A, R, x, mk_sort(l+1)),
"Acc_intro", Pi(A, R, x, mk_arrow(Pi(y, mk_arrow(R(y, x), Acc(A, R, y))), Acc(A, R, x))))
env = env:add_universe("u")
env = env:add_universe("v")
@ -42,21 +42,21 @@ local y = Local("y", A)
local a = Local("a", A)
local P = Local("P", mk_arrow(A, mk_sort(l2)))
local Hr = Local("Hr", Pi(y, mk_arrow(R(y, x), P(y))))
local H = Local("H", Pi({x, Hr}, P(x)))
local H = Local("H", Pi(x, Hr, P(x)))
local HR = Local("HR", R(y, x))
local HRa = Local("HRa", R(y, a))
local arg = Local("arg", Pi({y, HR}, Acc(A, R, y)))
local H_arg = Local("H_arg", Pi({y, HR}, P(y)))
local arg = Local("arg", Pi(y, HR, Acc(A, R, y)))
local H_arg = Local("H_arg", Pi(y, HR, P(y)))
local d = Local("d", Acc(A, R, x))
local Hwf = Local("R_is_wf", Pi(a, Acc(A, R, a)))
local wfi_th_type = Pi({A, R, Hwf, P, H, a}, P(a))
local wfi_th_type = Pi(A, R, Hwf, P, H, a, P(a))
print(wfi_th_type)
type_checker(env):check(wfi_th_type, {l1, l2})
local wfi_th_val = Fun({A, R, Hwf, P, H, a}, Acc_rec(A, R,
Fun({x, d}, P(x)), -- C
Fun({x, arg, H_arg}, H(x, H_arg)), -- e_1
a,
Acc_intro(A, R, a, Fun({y, HRa}, Hwf(y)))
local wfi_th_val = Fun(A, R, Hwf, P, H, a, Acc_rec(A, R,
Fun(x, d, P(x)), -- C
Fun(x, arg, H_arg, H(x, H_arg)), -- e_1
a,
Acc_intro(A, R, a, Fun(y, HRa, Hwf(y)))
))
print(env:normalize(type_checker(env):check(wfi_th_val, {l1, l2})))
env = add_decl(env, mk_definition("well_founded_induction_type", {l1, l2}, wfi_th_type, wfi_th_val))

9
tests/lua/alias1.lua
View file

@ -2,7 +2,6 @@ local env = environment()
local env = environment()
local l = mk_param_univ("l")
local A = Const("A")
local U_l = mk_sort(l)
local U_l1 = mk_sort(max_univ(l, 1)) -- Make sure U_l1 is not Bool/Prop
local nat = Const({"nat", "nat"})
@ -23,10 +22,12 @@ assert(get_alias_exprs(env, {"natural", "zero"}):head() == zero)
assert(get_alias_exprs(env, {"natural", "nat"}):head() == nat)
assert(is_aliased(env, nat) == name("natural", "nat"))
local A = Local("A", U_l)
env = add_inductive(env,
name("list", "list"), {l}, 1, Pi(A, U_l, U_l1),
name("list", "nil"), Pi({{A, U_l, true}}, list_l(A)),
name("list", "cons"), Pi({{A, U_l, true}}, mk_arrow(A, list_l(A), list_l(A))))
name("list", "list"), {l}, 1, Pi(A, U_l1),
name("list", "nil"), Pi(A, list_l(A)),
name("list", "cons"), Pi(A, mk_arrow(A, list_l(A), list_l(A))))
env = add_aliases(env, "list", "lst")
print(not get_alias_exprs(env, {"lst", "list_rec"}):is_nil())

12
tests/lua/coe1.lua
View file

@ -23,10 +23,10 @@ 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("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_coercion(env, "lst2vec")
assert(is_coercion(env, Const("lst2vec", {l})))
@ -54,7 +54,7 @@ print(get_coercion(env2, lst_nat, "dlst"))
assert(env2:type_check(get_coercion(env2, lst_nat, "dlst")))
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_var_decl("lst2vec2", {l}, Pi(A, ll, vec_l(A, len_l(A, ll)))))
print("======")
env2 = add_coercion(env2, "lst2vec2")
print("======")
@ -62,7 +62,7 @@ print(get_coercion(env2, lst_nat, "dlst"))
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_var_decl("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)

2
tests/lua/coe2.lua
View file

@ -5,7 +5,7 @@ env = add_decl(env, mk_var_decl("functor", {l1, l2}, mk_arrow(mk_sort(l1), mk_so
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_var_decl("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))

10
tests/lua/env10.lua
View file

@ -26,15 +26,15 @@ local b = Local("b", B)
local sigma_l1l2 = Const("sigma", {l1, l2})
env = add_inductive(env,
"sigma", {l1, l2}, 2, Pi({A, B}, U_l1l2),
"pair", Pi({A, B, a, b}, sigma_l1l2(A, B)))
"sigma", {l1, l2}, 2, Pi(A, B, U_l1l2),
"pair", Pi(A, B, a, b, sigma_l1l2(A, B)))
local coproduct_l1l2 = Const("coproduct", {l1, l2})
env = add_inductive(env,
"coproduct", {l1, l2}, 2, Pi({A, B}, U_l1l2),
"inl", Pi({A, B, a}, coproduct_l1l2(A, B)),
"inr", Pi({A, B, b}, coproduct_l1l2(A, B)))
"coproduct", {l1, l2}, 2, Pi(A, B, U_l1l2),
"inl", Pi(A, B, a, coproduct_l1l2(A, B)),
"inr", Pi(A, B, b, coproduct_l1l2(A, B)))
env:for_each_decl(function(d)
print(tostring(d:name()) .. " : " .. tostring(d:type()))

7
tests/lua/env5.lua
View file

@ -2,11 +2,12 @@ local env = bare_environment()
local l_name = name("l")
local l = mk_param_univ(l_name)
local U_l = mk_sort(l)
local A = Const("A")
local x = Const("x")
local A = Local("A", U_l)
local x = Local("x", A)
local A2A = mk_arrow(A, A)
local id_ty = Pi(A, U_l, mk_arrow(A, A))
local id_def = Fun(A, U_l, Fun(x, A, x))
local id_ty = Pi(A, mk_arrow(A, A))
local id_def = Fun(A, Fun(x, x))
env = add_decl(env, mk_definition(env, "id", {l_name}, id_ty, id_def, {opaque=false}))
local ok, ex = pcall(function()
env = add_decl(env, mk_definition(env, "id2", {"l2"}, id_ty, id_def, {opaque=false}))

4
tests/lua/env6.lua
View file

@ -1,8 +1,8 @@
local env = bare_environment()
env = add_decl(env, mk_var_decl("A", Bool))
local A = Const("A")
local x = Const("x")
env = add_decl(env, mk_axiom("magic", Pi(x, Bool, x)))
local x = Local("x", Bool)
env = add_decl(env, mk_axiom("magic", Pi(x, x)))
local saved_env = env
env = add_decl(env, mk_axiom("Ax", A))
env = add_decl(env, mk_definition("T1", A, Const("Ax")))

22
tests/lua/eta.lua
View file

@ -1,16 +1,16 @@
local env = bare_environment()
env = add_decl(env, mk_var_decl("f", mk_arrow(Bool, mk_arrow(Bool, Bool))))
local f = Const("f")
local x = Const("x")
local y = Const("y")
local z = Const("z")
local x = Local("x", Bool)
local y = Local("y", Bool)
local z = Local("z", Bool)
local tc = type_checker(env)
print(tc:whnf(Fun(x, Bool, f(x))))
print(tc:whnf(Fun(x, Bool, Fun(y, Bool, f(x, y)))))
print(tc:whnf(Fun(x, Bool, Fun(y, Bool, f(Const("a"), y)))))
print(tc:whnf(Fun(z, Bool, Fun(x, Bool, Fun(y, Bool, f(z, y))))))
assert(tc:is_def_eq(f, Fun(x, Bool, f(x))))
assert(tc:is_def_eq(f, Fun(x, Bool, Fun(y, Bool, f(x, y)))))
local a = Const("a")
print(tc:whnf(Fun(x, f(x))))
print(tc:whnf(Fun(x, y, f(x, y))))
print(tc:whnf(Fun(x, y, f(Const("a"), y))))
print(tc:whnf(Fun(z, x, y, f(z, y))))
assert(tc:is_def_eq(f, Fun(x, f(x))))
assert(tc:is_def_eq(f, Fun(x, y, f(x, y))))
local A = Const("A")
assert(tc:is_def_eq(Fun(a, A, a)(f), Fun(x, Bool, Fun(y, Bool, f(x, y)))))
local a = Local("a", A)
assert(tc:is_def_eq(Fun(a, a)(f), Fun(x, y, f(x, y))))

4
tests/lua/expr10.lua
View file

@ -3,6 +3,6 @@ local f = Local("f", mk_arrow(Bool, Bool, Bool))
local a = Local("a", Bool)
local b = Local("b", Bool)
local x = Local("x", Bool)
local t = Fun({f, a, b}, f(Fun(x, x)(b), a))
local t = Fun(f, a, b, f(Fun(x, x)(b), a))
print(env:normalize(t))
assert(env:normalize(t) == Fun({f, a, b}, f(b, a)))
assert(env:normalize(t) == Fun(f, a, b, f(b, a)))

10
tests/lua/expr2.lua
View file

@ -14,10 +14,12 @@ assert(mk_metavar("a", Bool):is_lt(mk_metavar("a", Type)))
assert(mk_local("a", Bool):is_lt(mk_local("b", Bool)))
assert(not mk_local("a", Bool):is_lt(mk_local("a", Bool)))
assert(Bool:is_lt(Const("a")))
assert(Fun(a, Bool, a):is_lt(Fun(a, Type, a)))
assert(Fun(a, Bool, a):is_lt(Fun(a, Bool, Var(2))))
assert(Pi(a, Bool, a):is_lt(Pi(a, Type, a)))
assert(Pi(a, Bool, a):is_lt(Pi(a, Bool, Var(2))))
local a = Local("a", Bool)
local a1 = Local("a1", Type)
assert(Fun(a, a):is_lt(Fun(a1, a1)))
assert(Fun(a, a):is_lt(Fun(a, Var(2))))
assert(Pi(a, a):is_lt(Pi(a1, a1)))
assert(Pi(a, a):is_lt(Pi(a, Var(2))))
assert(Var(0) < Var(1))
print(Const("a", {mk_level_one(), mk_level_zero()}))
assert(Const("a", {mk_level_one()}):is_lt(Const("a", {mk_level_one(), mk_level_zero()})))

12
tests/lua/expr3.lua
View file

@ -9,7 +9,8 @@ assert(t:fn() == f)
assert(t:arg() == a)
assert(not pcall(function() f:fn() end))
local pi1 = Pi(a, Bool, Type)
local a1 = Local("a", Bool)
local pi1 = Pi(a1, Type)
assert(pi1:is_pi())
assert(not pcall(function() f:binding_name() end))
local pi2 = mk_pi("a", Bool, Type, binder_info(true, true))
@ -23,14 +24,13 @@ assert(not l1:binding_info():is_implicit())
assert(l2:binding_info():is_implicit())
local b = Const("b")
local pi3 = Pi({{a, Bool}, {b, Bool}}, a)
local a = Local("a", Bool)
local b = Local("b", Bool)
local pi3 = Pi(a, b, a)
print(pi3)
assert(not pcall(function() Pi(a) end))
local pi4 = Pi(a, Bool, b, Bool, a)
local pi4 = Pi(a, b, a)
print(pi4)
assert(not pcall(function() Pi(a, Bool, b, Bool) end))
assert(not pcall(function() Pi({}, Bool) end))
assert(pi4:binding_name() == name("a"))
assert(pi4:binding_domain() == Bool)
assert(pi4:binding_body():is_pi())

21
tests/lua/expr4.lua
View file

@ -1,15 +1,8 @@
local a = Const("a")
local b = Const("b")
local f = Const("f")
local vec = Const("vec")
print(Pi({{a, Type}, {b, vec(a), true}}, vec(b)))
print(Pi({{a, Type, binder_info(true, true)}, {b, vec(a), true}}, vec(b)))
assert(not pcall(function()
print(Pi({{a, Type}, {f(b), vec(a), true}}, vec(b)))
end
))
assert(not pcall(function()
print(Pi({{a, Type, a}, {b, vec(a), true}}, vec(b)))
end
))
local a = Local("a", Type)
local b = Local("b", vec(a), binder_info(true))
local f = Const("f")
print(Pi(a, b, vec(b)))
local a = Local("a", Type, binder_info(true, true))
local b = Local("b", vec(a), binder_info(true))
print(Pi(a, b, vec(b)))

8
tests/lua/expr7.lua
View file

@ -1,8 +1,10 @@
local a = Const("a")
local A = Const("A")
local A = Local("A", Type)
local a = Local("a", A)
local vec = Const("vec")
local A1 = Local("A", vec(A))
local a1 = Local("a", a)
local T = Const("T")
print(Pi({{A, Type}, {a, A}, {A, vec(A)}, {a, A}}, a))
print(Pi(A, a, A1, a1, a1))
local t = mk_pi("A", Type, mk_pi("a", Var(0), mk_pi("A", vec(Var(1)), mk_pi("a", Var(0), T(Var(0), Var(2))))))
print(t)

10
tests/lua/expr8.lua
View file

@ -1,9 +1,7 @@
local Or = Const("or")
local A = Local("A", Type)
local a = Local("a", A)
local a = Local("a", A, binder_info(true))
local b = Local("b", A)
local H = Local("H", Or(a, b))
print(Pi({A, {a, true}, {b, Bool}, {H, binder_info(false, true)}}, Or(b, a)))
print(Pi({A, a, b, H}, Or(b, a)))
print(Fun({A, {a, true}, {b, Bool}, {H, binder_info(false, true)}}, Or(b, a)))
print(Fun({A, a, b, H}, Or(b, a)))
local H = Local("H", Or(a, b), binder_info(false, true))
print(Pi(A, a, b, H, Or(b, a)))
print(Fun(A, a, b, H, Or(b, a)))

6
tests/lua/hott1.lua
View file

@ -10,8 +10,8 @@ assert(env:cls_proof_irrel():head() == name("Id"))
assert(env:cls_proof_irrel():tail():is_nil())
local l = mk_param_univ("l")
local U_l = mk_sort(l)
local A = Const("A")
env = add_decl(env, mk_var_decl("Id", {l}, Pi(A, U_l, mk_arrow(A, A, U_l))))
local A = Local("A", U_l)
env = add_decl(env, mk_var_decl("Id", {l}, Pi(A, mk_arrow(A, A, U_l))))
local Set = mk_sort(mk_level_zero())
env = add_decl(env, mk_var_decl("N", Set))
local N = Const("N")
@ -26,7 +26,7 @@ local tc = type_checker(env)
-- H1 and H2 are definitionally equal since both have type Id.{0} N a b
-- and Id is in env:cls_proof_irrel()
assert(tc:is_def_eq(Const("H1"), Const("H2")))
env = add_decl(env, mk_var_decl("Path", {l}, Pi(A, U_l, mk_arrow(A, A, U_l))))
env = add_decl(env, mk_var_decl("Path", {l}, Pi(A, mk_arrow(A, A, U_l))))
local Path_z = Const("Path", {mk_level_zero()})
env = add_decl(env, mk_axiom("H3", Path_z(N, a, b)))
env = add_decl(env, mk_axiom("H4", Path_z(N, a, b)))

92
tests/lua/ind1.lua
View file

@ -1,7 +1,7 @@
local env = environment()
local l = mk_param_univ("l")
local A = Const("A")
local U_l = mk_sort(l)
local A = Local("A", U_l)
local U_l1 = mk_sort(max_univ(l, 1)) -- Make sure U_l1 is not Bool/Prop
local list_l = Const("list", {l}) -- list.{l}
local Nat = Const("nat")
@ -10,7 +10,7 @@ local zero = Const("zero")
local succ = Const("succ")
local forest_l = Const("forest", {l})
local tree_l = Const("tree", {l})
local n = Const("n")
local n = Local("n", Nat)
env = env:add_universe("u")
env = env:add_universe("v")
@ -29,42 +29,44 @@ env = add_inductive(env,
-- 1 is the number of parameters.
-- The Boolean true in {A, U_l, true} is marking that this argument is implicit.
env = add_inductive(env,
"list", {l}, 1, Pi(A, U_l, U_l1),
"nil", Pi({{A, U_l, true}}, list_l(A)),
"cons", Pi({{A, U_l, true}}, mk_arrow(A, list_l(A), list_l(A))))
"list", {l}, 1, Pi(A, U_l1),
"nil", Pi(A, list_l(A)),
"cons", Pi(A, mk_arrow(A, list_l(A), list_l(A))))
env = add_inductive(env,
"vec", {l}, 1, Pi({{A, U_l}, {n, Nat}}, U_l1),
"vnil", Pi({{A, U_l, true}}, vec_l(A, zero)),
"vcons", Pi({{A, U_l, true}, {n, Nat, true}}, mk_arrow(A, vec_l(A, n), vec_l(A, succ(n)))))
"vec", {l}, 1, Pi(A, n, U_l1),
"vnil", Pi(A, vec_l(A, zero)),
"vcons", Pi(A, n, mk_arrow(A, vec_l(A, n), vec_l(A, succ(n)))))
local And = Const("and")
local Or = Const("or")
local B = Const("B")
-- Datatype without introduction rules (aka constructors). It is a uninhabited type.
env = add_inductive(env, "false", Bool)
-- Datatype with a single constructor.
env = add_inductive(env, "true", Bool, "trivial", Const("true"))
local A = Local("A", Bool)
local B = Local("B", Bool)
env = add_inductive(env,
"and", 2, Pi({{A, Bool}, {B, Bool}}, Bool),
"and_intro", Pi({{A, Bool, true}, {B, Bool, true}}, mk_arrow(A, B, And(A, B))))
"and", 2, Pi(A, B, Bool),
"and_intro", Pi(A, B, mk_arrow(A, B, And(A, B))))
env = add_inductive(env,
"or", 2, Pi({{A, Bool}, {B, Bool}}, Bool),
"or_intro_left", Pi({{A, Bool, true}, {B, Bool, true}}, mk_arrow(A, Or(A, B))),
"or_intro_right", Pi({{A, Bool, true}, {B, Bool, true}}, mk_arrow(B, Or(A, B))))
local P = Const("P")
local a = Const("a")
"or", 2, Pi(A, B, Bool),
"or_intro_left", Pi(A, B, mk_arrow(A, Or(A, B))),
"or_intro_right", Pi(A, B, mk_arrow(B, Or(A, B))))
local A = Local("A", U_l)
local P = Local("P", mk_arrow(A, Bool))
local a = Local("a", A)
local exists_l = Const("exists", {l})
env = add_inductive(env,
"exists", {l}, 2, Pi({{A, U_l}, {P, mk_arrow(A, Bool)}}, Bool),
"exists_intro", Pi({{A, U_l, true}, {P, mk_arrow(A, Bool), true}, {a, A}}, mk_arrow(P(a), exists_l(A, P))))
"exists", {l}, 2, Pi(A, P, Bool),
"exists_intro", Pi(A, P, a, mk_arrow(P(a), exists_l(A, P))))
env = add_inductive(env, {l}, 1,
{"tree", Pi(A, U_l, U_l1),
"node", Pi({{A, U_l, true}}, mk_arrow(A, forest_l(A), tree_l(A)))
{"tree", Pi(A, U_l1),
"node", Pi(A, mk_arrow(A, forest_l(A), tree_l(A)))
},
{"forest", Pi(A, U_l, U_l1),
"emptyf", Pi({{A, U_l, true}}, forest_l(A)),
"consf", Pi({{A, U_l, true}}, mk_arrow(tree_l(A), forest_l(A), forest_l(A)))})
{"forest", Pi(A, U_l1),
"emptyf", Pi(A, forest_l(A)),
"consf", Pi(A, mk_arrow(tree_l(A), forest_l(A), forest_l(A)))})
local tc = type_checker(env)
display_type(env, Const("forest", {0}))
@ -76,24 +78,28 @@ display_type(env, Const("or_rec"))
local Even = Const("Even")
local Odd = Const("Odd")
local b = Const("b")
local b = Local("b", Nat)
env = add_inductive(env, {},
{"Even", mk_arrow(Nat, Bool),
"zero_is_even", Even(zero),
"succ_odd", Pi(b, Nat, mk_arrow(Odd(b), Even(succ(b))))},
"succ_odd", Pi(b, mk_arrow(Odd(b), Even(succ(b))))},
{"Odd", mk_arrow(Nat, Bool),
"succ_even", Pi(b, Nat, mk_arrow(Even(b), Odd(succ(b))))})
"succ_even", Pi(b, mk_arrow(Even(b), Odd(succ(b))))})
local flist_l = Const("flist", {l})
env = add_inductive(env,
"flist", {l}, 1, Pi(A, U_l, U_l1),
"fnil", Pi({{A, U_l, true}}, flist_l(A)),
"fcons", Pi({{A, U_l, true}}, mk_arrow(mk_arrow(Nat, A), mk_arrow(Nat, Bool, flist_l(A)), flist_l(A))))
"flist", {l}, 1, Pi(A, U_l1),
"fnil", Pi(A, flist_l(A)),
"fcons", Pi(A, mk_arrow(mk_arrow(Nat, A), mk_arrow(Nat, Bool, flist_l(A)), flist_l(A))))
local eq_l = Const("eq", {l})
local A = Local("A", U_l)
local a = Local("a", A)
local b = Local("b", A)
env = add_inductive(env,
"eq", {l}, 2, Pi({{A, U_l}, {a, A}, {b, A}}, Bool),
"refl", Pi({{A, U_l}, {a, A}}, eq_l(A, a, a)))
"eq", {l}, 2, Pi(A, a, b, Bool),
"refl", Pi(A, a, eq_l(A, a, a)))
display_type(env, Const("eq_rec", {v, u}))
display_type(env, Const("exists_rec", {u}))
display_type(env, Const("list_rec", {v, u}))
@ -103,10 +109,12 @@ display_type(env, Const("and_rec", {v}))
display_type(env, Const("vec_rec", {v, u}))
display_type(env, Const("flist_rec", {v, u}))
local n = Const("n")
local c = Const("c")
local nat_rec1 = Const("nat_rec", {1})
local add = Fun({{a, Nat}, {b, Nat}}, nat_rec1(mk_lambda("_", Nat, Nat), b, Fun({{n, Nat}, {c, Nat}}, succ(c)), a))
local a = Local("a", Nat)
local b = Local("b", Nat)
local n = Local("n", Nat)
local c = Local("c", Nat)
local add = Fun(a, b, nat_rec1(mk_lambda("_", Nat, Nat), b, Fun(n, c, succ(c)), a))
display_type(env, add)
local tc = type_checker(env)
assert(tc:is_def_eq(add(succ(succ(zero)), succ(zero)),
@ -117,10 +125,11 @@ assert(tc:is_def_eq(add(succ(succ(succ(zero))), succ(succ(zero))),
local list_nat = Const("list", {1})(Nat)
local list_nat_rec1 = Const("list_rec", {1, 1})(Nat)
display_type(env, list_nat_rec1)
local h = Const("h")
local t = Const("t")
local lst = Const("lst")
local length = Fun(lst, list_nat, list_nat_rec1(mk_lambda("_", list_nat, Nat), zero, Fun({{h, Nat}, {t, list_nat}, {c, Nat}}, succ(c)), lst))
local h = Local("h", Nat)
local t = Local("t", list_nat)
local c = Local("c", Nat)
local lst = Local("lst", list_nat)
local length = Fun(lst, list_nat_rec1(mk_lambda("_", list_nat, Nat), zero, Fun(h, t, c, succ(c)), lst))
local nil_nat = Const("nil", {1})(Nat)
local cons_nat = Const("cons", {1})(Nat)
print(tc:whnf(length(nil_nat)))
@ -138,9 +147,12 @@ assert(tc:is_def_eq(length(cons_nat(zero, cons_nat(zero, nil_nat))), succ(succ(z
-- Martin-Lof style identity type
local env = hott_environment()
local Id_l = Const("Id", {l})
local A = Local("A", U_l)
local a = Local("a", A)
local b = Local("b", A)
env = env:add_universe("u")
env = env:add_universe("v")
env = add_inductive(env,
"Id", {l}, 1, Pi({{A, U_l}, {a, A}, {b, A}}, U_l),
"Id_refl", Pi({{A, U_l, true}, {b, A}}, Id_l(A, b, b)))
"Id", {l}, 1, Pi(A, a, b, U_l),
"Id_refl", Pi(A, b, Id_l(A, b, b)))
display_type(env, Const("Id_rec", {v, u}))

52
tests/lua/ind2.lua
View file

@ -8,7 +8,6 @@ function bad_add_inductive(...)
end
local l = mk_param_univ("l")
local A = Const("A")
local U_l = mk_sort(l)
local U_l1 = mk_sort(max_univ(l, 1)) -- Make sure U_l1 is not Bool/Prop
local list_l = Const("list", {l}) -- list.{l}
@ -25,21 +24,23 @@ bad_add_inductive(env,
"zero", Bool, -- Incorrect result type
"succ", mk_arrow(Nat, Nat))
local A = Local("A", U_l)
bad_add_inductive(env, {l}, 1,
{"tree", mk_arrow(U_l, U_l1),
"node", Pi({{A, U_l, true}}, mk_arrow(A, forest_l(A), tree_l(A)))
"node", Pi(A, mk_arrow(A, forest_l(A), tree_l(A)))
},
{"forest", mk_arrow(U_l1, U_l1), -- Parameters of all inductive types must match
"emptyf", Pi({{A, U_l, true}}, forest_l(A)),
"consf", Pi({{A, U_l, true}}, mk_arrow(tree_l(A), forest_l(A), forest_l(A)))})
"emptyf", Pi(A, forest_l(A)),
"consf", Pi(A, mk_arrow(tree_l(A), forest_l(A), forest_l(A)))})
bad_add_inductive(env, {l}, 1,
{"tree", mk_arrow(U_l, U_l), -- Result may be in universe zero (e.g., l is instantiated with zero)
"node", Pi({{A, U_l, true}}, mk_arrow(A, forest_l(A), tree_l(A)))
"node", Pi(A, mk_arrow(A, forest_l(A), tree_l(A)))
},
{"forest", mk_arrow(U_l, U_l1),
"emptyf", Pi({{A, U_l, true}}, forest_l(A)),
"consf", Pi({{A, U_l, true}}, mk_arrow(tree_l(A), forest_l(A), forest_l(A)))})
"emptyf", Pi(A, forest_l(A)),
"consf", Pi(A, mk_arrow(tree_l(A), forest_l(A), forest_l(A)))})
bad_add_inductive(env,
"nat", 1, Type, -- mismatch in the number of arguments claimed
@ -53,54 +54,55 @@ env = add_inductive(env,
local Even = Const("Even")
local Odd = Const("Odd")
local b = Const("b")
local b = Local("b", Nat)
bad_add_inductive(env, {},
{"Even", mk_arrow(Nat, Type),
"zero_is_even", Even(zero),
"succ_odd", Pi(b, Nat, mk_arrow(Odd(b), Even(succ(b))))},
"succ_odd", Pi(b, mk_arrow(Odd(b), Even(succ(b))))},
{"Odd", mk_arrow(Nat, Bool), -- if one datatype lives in Bool/Prop, then all must live in Bool/Prop
"succ_even", Pi(b, Nat, mk_arrow(Even(b), Odd(succ(b))))})
"succ_even", Pi(b, mk_arrow(Even(b), Odd(succ(b))))})
bad_add_inductive(env,
"list", {l}, 1, mk_arrow(U_l, U_l1),
"nil", Pi({{A, U_l, true}}, mk_arrow(mk_arrow(list_l(A), Bool), list_l(A))), -- nonpositive occurrence of inductive datatype
"cons", Pi({{A, U_l, true}}, mk_arrow(A, list_l(A), list_l(A))))
"nil", Pi(A, mk_arrow(mk_arrow(list_l(A), Bool), list_l(A))), -- nonpositive occurrence of inductive datatype
"cons", Pi(A, mk_arrow(A, list_l(A), list_l(A))))
bad_add_inductive(env,
"list", {l}, 1, mk_arrow(U_l, U_l1),
"nil", Pi({{A, U_l, true}}, list_l(mk_arrow(A, A))),
"cons", Pi({{A, U_l, true}}, mk_arrow(A, list_l(A), list_l(A))))
"nil", Pi(A, list_l(mk_arrow(A, A))),
"cons", Pi(A, mk_arrow(A, list_l(A), list_l(A))))
local list_1 = Const("list", {mk_level_one()})
bad_add_inductive(env,
"list", {l}, 1, mk_arrow(U_l, U_l1),
"nil", Pi({{A, U_l, true}}, list_l(A)),
"cons", Pi({{A, U_l, true}}, mk_arrow(A, list_1(Nat), list_l(A)))) -- all list occurrences must be of the form list_l(A)
"nil", Pi(A, list_l(A)),
"cons", Pi(A, mk_arrow(A, list_1(Nat), list_l(A)))) -- all list occurrences must be of the form list_l(A)
bad_add_inductive(env,
"list", {l}, 1, mk_arrow(U_l, U_l1),
"nil", Pi({{A, U_l, true}}, list_l(A)),
"cons", Pi({{A, Type, true}}, mk_arrow(A, list_1(A), list_1(A))))
"nil", Pi(A, list_l(A)),
"cons", Pi(A, mk_arrow(A, list_1(A), list_1(A))))
bad_add_inductive(env,
"list", {l}, 1, mk_arrow(U_l, U_l1),
"nil", Pi({{A, U_l, true}}, mk_arrow(U_l, list_l(A))),
"cons", Pi({{A, U_l, true}}, mk_arrow(A, list_l(A), list_l(A))))
"nil", Pi(A, mk_arrow(U_l, list_l(A))),
"cons", Pi(A, mk_arrow(A, list_l(A), list_l(A))))
bad_add_inductive(env,
"list", {l}, 1, mk_arrow(U_l, U_l1),
"nil", Pi({{A, U_l, true}}, list_l(A)),
"cons", Pi({{A, U_l, true}}, mk_arrow(list_l(A), A, list_l(A))))
"nil", Pi(A, list_l(A)),
"cons", Pi(A, mk_arrow(list_l(A), A, list_l(A))))
env = add_decl(env, mk_var_decl("eq", Pi(A, Type, mk_arrow(A, A, Bool))))
local A = Local("A", Type)
env = add_decl(env, mk_var_decl("eq", Pi(A, mk_arrow(A, A, Bool))))
local eq = Const("eq")
local Nat2 = Const("nat2")
local a = Const("a")
local a = Local("a", Nat2)
bad_add_inductive(env,
"nat2", Type,
"zero2", Nat2,
"succ2", Pi(a, Nat2, mk_arrow(eq(Nat2, a, a), Nat2)))
"succ2", Pi(a, mk_arrow(eq(Nat2, a, a), Nat2)))
local env = bare_environment()
bad_add_inductive(env, -- Environment does not support inductive datatypes

10
tests/lua/ind3.lua
View file

@ -17,7 +17,7 @@ local b = Local("b", nat)
local n = Local("n", nat)
local r = Local("r", nat)
local nat_rec_nat = Const("nat_rec", {1})(Fun(a, nat))
local add = Fun({a, b}, nat_rec_nat(b, Fun({n, r}, succ(r)), a))
local add = Fun(a, b, nat_rec_nat(b, Fun(n, r, succ(r)), a))
local tc = type_checker(env)
assert(tc:is_def_eq(add(succ(succ(zero)), succ(zero)),
succ(succ(succ(zero)))))
@ -38,11 +38,11 @@ local tail = Local("tail", tree_list_l(A))
env = add_inductive(env, {l}, 1,
{"tree", Pi(A, U_l1),
"leaf", Pi(A, tree_l(A)),
"node", Pi({A, v, children}, tree_l(A))
"node", Pi(A, v, children, tree_l(A))
},
{"tree_list", Pi(A, U_l1),
"nil", Pi(A, tree_list_l(A)),
"cons", Pi({A, head, tail}, tree_list_l(A))})
"cons", Pi(A, head, tail, tree_list_l(A))})
local tree_nat = Const("tree", {1})(nat)
local tree_list_nat = Const("tree_list", {1})(nat)
@ -52,9 +52,9 @@ local tree_rec_nat = Const("tree_rec", {1, 1})(nat, Fun(t, nat), Fun(tl, nat)
local r1 = Local("r1", nat)
local r2 = Local("r2", nat)
local length_tree_nat = Fun(t, tree_rec_nat(zero,
Fun({a, tl, r}, succ(r)),
Fun(a, tl, r, succ(r)),
zero,
Fun({t, tl, r1, r2}, add(r1, r2)),
Fun(t, tl, r1, r2, add(r1, r2)),
t))
display_type(env, length_tree_nat)

2
tests/lua/ind_ex.lua
View file

@ -7,7 +7,7 @@ local a = Local("a", A)
env = add_inductive(env,
"inhabited", {l}, 1, mk_arrow(U_l, Bool),
"inhabited_intro", Pi({A, a}, inhabited(A)))
"inhabited_intro", Pi(A, a, inhabited(A)))
function display_type(env, t)
print(tostring(t) .. " : " .. tostring(type_checker(env):check(t)))

4
tests/lua/ind_tricky.lua
View file

@ -1,11 +1,11 @@
local env = environment()
local tricky = Const("tricky")
local P = Const("P")
local P = Local("P", Bool)
env = add_inductive(env,
"tricky", Bool,
"C", mk_arrow(Pi(P, Bool, mk_arrow(P, P)), tricky))
"C", mk_arrow(Pi(P, mk_arrow(P, P)), tricky))
function display_type(env, t)
print(tostring(t) .. " : " .. tostring(type_checker(env):check(t)))

2
tests/lua/proof_state1.lua
View file

@ -5,7 +5,7 @@ local eq = Const("eq")
local a = Local("a", A)
local b = Local("b", A)
local H = Local("H", eq(A, a, b))
local m = mk_metavar("m", Pi({A, a, b, H}, eq(A, a, b)))
local m = mk_metavar("m", Pi(A, a, b, H, eq(A, a, b)))
print(to_proof_state(m))
local s = to_proof_state(m)
local n, g = s:goals():head()

17
tests/lua/res1.lua
View file

@ -6,17 +6,18 @@ local False = Const("false")
function init_env(env)
-- Populate environment when declarations used by resolve_macro.
-- This is a 'fake' environment used only for testing.
local a = Const("a")
local b = Const("b")
local c = Const("c")
local H = Const("H")
local a = Local("a", Bool)
local b = Local("b", Bool)
local c = Local("c", Bool)
local Ha = Local("Ha", a)
local Hb = Local("Hb", b)
env = add_decl(env, mk_var_decl("or", mk_arrow(Bool, Bool, Bool)))
env = add_decl(env, mk_var_decl("not", mk_arrow(Bool, Bool)))
env = add_decl(env, mk_var_decl("false", Bool))
env = add_decl(env, mk_axiom("or_elim", Pi({{a, Bool}, {b, Bool}, {c, Bool}}, 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, Bool}, {H, a}, {b, Bool}}, Or(a, b))))
env = add_decl(env, mk_axiom("or_intro_right", Pi({{b, Bool}, {a, Bool}, {H, b}}, Or(a, b))))
env = add_decl(env, mk_axiom("absurd_elim", Pi({{a, Bool}, {b, Bool}}, mk_arrow(a, Not(a), b))))
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))))
env = add_decl(env, mk_axiom("absurd_elim", Pi(a, b, mk_arrow(a, Not(a), b))))
return env
end

8
tests/lua/scope.lua
View file

@ -23,10 +23,10 @@ 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("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_coercion(env, "lst2vec")
env = push_scope(env, "tst")

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

@ -3,7 +3,7 @@ function mk_env(prefix, sz)
local env = environment()
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_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"), Bool))
local P = Const(name(prefix, "P"))
local id = Const(name(prefix, "id"))

10
tests/lua/sorted.lua
View file

@ -6,7 +6,7 @@ local U_l1 = mk_sort(max_univ(l, 1)) -- Make sure U_l1 is not Bool/Prop
local list_l = Const("list", {l}) -- list.{l}
env = add_inductive(env,
"list", {l}, 1, Pi(A, U_l, U_l1),
"list", {l}, 1, Pi(A, U_l1),
"nil", Pi(A, list_l(A)),
"cons", Pi(A, mk_arrow(A, list_l(A), list_l(A))))
@ -22,10 +22,10 @@ local Hlt = Local("H", lt(a1, a2))
local Hs = Local("Hs", is_sorted_l(A, lt, cons_l(A, a2, t)))
env = add_inductive(env,
"is_sorted", {l}, 2, Pi({A, lt}, mk_arrow(list_l(A), Bool)),
"is_sorted_nil", Pi({A, lt}, is_sorted_l(A, lt, nil_l(A))),
"is_sorted_cons_nil", Pi({A, lt, a}, is_sorted_l(A, lt, cons_l(A, a, nil_l(A)))),
"is_sorted_cons_cons", Pi({A, lt, a1, a2, t, Hlt, Hs}, is_sorted_l(A, lt, cons_l(A, a1, cons_l(A, a2, t)))))
"is_sorted", {l}, 2, Pi(A, lt, mk_arrow(list_l(A), Bool)),
"is_sorted_nil", Pi(A, lt, is_sorted_l(A, lt, nil_l(A))),
"is_sorted_cons_nil", Pi(A, lt, a, is_sorted_l(A, lt, cons_l(A, a, nil_l(A)))),
"is_sorted_cons_cons", Pi(A, lt, a1, a2, t, Hlt, Hs, is_sorted_l(A, lt, cons_l(A, a1, cons_l(A, a2, t)))))
print(env:find("is_sorted_rec"):type())

2
tests/lua/tactic1.lua
View file

@ -5,7 +5,7 @@ local eq = Const("eq")
local a = Local("a", A)
local b = Local("b", A)
local H = Local("H", eq(A, a, b))
local m = mk_metavar("m", Pi({A, a, b, H}, eq(A, a, b)))
local m = mk_metavar("m", Pi(A, a, b, H, eq(A, a, b)))
print(to_proof_state(m))
local s = to_proof_state(m)
local t = Then(Append(trace_tac("tst1a"), trace_tac("tst1b")),

4
tests/lua/tag1.lua
View file

@ -1,8 +1,8 @@
local f = Const("f")
local x = Const("x")
local x = Local("x", Bool)
local a = Const("a")
local t1 = f(x, a, Var(1))
local t2 = Fun(x, Bool, t1)
local t2 = Fun(x, t1)
assert(not t2:tag())
assert(not t2:binding_body():tag())
t2:set_tag(2)

6
tests/lua/tc1.lua
View file

@ -2,8 +2,8 @@ local env = bare_environment()
local g = name_generator("tst")
local tc = type_checker(env, g)
assert(is_type_checker(tc))
local a = Const("a")
local t = Fun(a, Bool, a)
local a = Local("a", Bool)
local t = Fun(a, a)
local b = Const("b")
print(t(b))
assert(tc:whnf(t(b)) == b)
@ -13,7 +13,7 @@ local m = mk_metavar("m1", mk_metavar("m2", mk_sort(mk_meta_univ("u"))))
print(tc:infer(m))
local tc2 = type_checker(env, g)
local t2 = Fun(a, Bool, m(a))
local t2 = Fun(a, m(a))
print("---------")
print("t2: ")
print(t2)

83
tests/lua/tc2.lua
View file

@ -1,35 +1,37 @@
local env = bare_environment()
local env = environment()
local l = mk_param_univ("l")
local A = Const("A")
local a = Const("a")
local b = Const("b")
local P = Const("P")
local A = Local("A", mk_sort(l))
local a = Local("a", A)
local b = Local("b", A)
local P = Local("P", mk_arrow(A, Bool))
env = add_decl(env, mk_definition("id", {l},
Pi(A, mk_sort(l), mk_arrow(A, mk_arrow(A, Bool))),
Fun({{A, mk_sort(l)}, {a, A}, {b, A}}, Pi(P, mk_arrow(A, Bool), mk_arrow(P(a), P(b))))))
Pi(A, mk_arrow(A, mk_arrow(A, Bool))),
Fun(A, a, b, Pi(P, mk_arrow(P(a), P(b))))))
local id_l = Const("id", {l})
local H = Const("H")
local H = Local("H", P(a))
env = add_decl(env, mk_theorem("refl", {l},
Pi({{A, mk_sort(l)}, {a, A}}, id_l(A, a, a)),
Fun({{A, mk_sort(l)}, {a, A}, {P, mk_arrow(A, Bool)}, {H, P(a)}}, H)))
local H1 = Const("H1")
local H2 = Const("H2")
Pi(A, a, id_l(A, a, a)),
Fun(A, a, P, H, H)))
local H1 = Local("H1", id_l(A, a, b))
local H2 = Local("H2", P(a))
env = add_decl(env, mk_theorem("subst", {l},
Pi({{A, mk_sort(l)}, {P, mk_arrow(A, Bool)}, {a, A}, {b, A}, {H1, id_l(A, a, b)}, {H2, P(a)}}, P(b)),
Fun({{A, mk_sort(l)}, {P, mk_arrow(A, Bool)}, {a, A}, {b, A}, {H1, id_l(A, a, b)}, {H2, P(a)}},
H1(P, H2))))
Pi(A, P, a, b, H1, H2, P(b)),
Fun(A, P, a, b, H1, H2, H1(P, H2))))
local refl_l = Const("refl", {l})
local subst_l = Const("subst", {l})
local x = Const("x")
local x = Local("x", A)
local H = Local("H", id_l(A, a, b))
env = add_decl(env, mk_theorem("symm", {l},
Pi({{A, mk_sort(l)}, {a, A}, {b, A}, {H, id_l(A, a, b)}}, id_l(A, b, a)),
Fun({{A, mk_sort(l)}, {a, A}, {b, A}, {H, id_l(A, a, b)}},
subst_l(A, Fun(x, A, id_l(A, x, a)), a, b, H, refl_l(A, a)))))
local c = Const("c")
Pi(A, a, b, H, id_l(A, b, a)),
Fun(A, a, b, H,
subst_l(A, Fun(x, id_l(A, x, a)), a, b, H, refl_l(A, a)))))
local c = Local("c", A)
local H1 = Local("H1", id_l(A, a, b))
local H2 = Local("H2", id_l(A, b, c))
env = add_decl(env, mk_theorem("trans", {l},
Pi({{A, mk_sort(l)}, {a, A}, {b, A}, {c, A}, {H1, id_l(A, a, b)}, {H2, id_l(A, b, c)}}, id_l(A, a, c)),
Fun({{A, mk_sort(l)}, {a, A}, {b, A}, {c, A}, {H1, id_l(A, a, b)}, {H2, id_l(A, b, c)}},
subst_l(A, Fun(x, A, id_l(A, a, x)), b, c, H2, H1))))
Pi(A, a, b, c, H1, H2, id_l(A, a, c)),
Fun(A, a, b, c, H1, H2,
subst_l(A, Fun(x, id_l(A, a, x)), b, c, H2, H1))))
local symm_l = Const("symm", {l})
local trans_l = Const("trans", {l})
print(env:get("trans"):value())
@ -43,35 +45,24 @@ local refl_u = Const("refl", {u})
local subst_u = Const("subst", {u})
local symm_u = Const("symm", {u})
local trans_u = Const("trans", {u})
local d = Const("d")
local H3 = Const("H3")
print(tc:check(Fun({{A, mk_sort(u)}, {a, A}, {b, A}, {c, A}, {d, A},
{H1, id_u(A, b, a)},
{H2, id_u(A, b, c)},
{H3, id_u(A, c, d)}},
local A = Local("A", mk_sort(u))
local d = Local("d", A)
local H1 = Local("H1", id_u(A, b, a))
local H2 = Local("H2", id_u(A, b, c))
local H3 = Local("H3", id_u(A, c, d))
print(tc:check(Fun(A, a, b, c, d, H1, H2, H3,
trans_u(A, a, b, d,
symm_u(A, b, a, H1),
trans_u(A, b, c, d, H2, H3)))))
local g = name_generator("tst")
local tc2 = type_checker(env, g)
print("=================")
local f = Const("f")
local mf_ty = mk_metavar("f_ty", Pi(A, mk_sort(u), mk_sort(mk_meta_univ("l_f"))))
local mA1 = mk_metavar("A1", Pi({{A, mk_sort(u)}, {f, mf_ty(A)}, {a, A}}, mk_sort(mk_meta_univ("l_A1"))))
print(tc2:check(Fun({{A, mk_sort(u)}, {f, mf_ty(A)}, {a, A}},
local A = Local("A", mk_sort(u))
local mf_ty = mk_metavar("f_ty", Pi(A, mk_sort(mk_meta_univ("l_f"))))
local f = Local("f", mf_ty(A))
local a = Local("a", A)
local mA1 = mk_metavar("A1", Pi(A, f, a, mk_sort(mk_meta_univ("l_A1"))))
print(tc2:check(Fun(A, f, a,
id_u(mA1(A, f, a), f(a), a))))
local tc2 = type_checker(env, g)
local scope = {{A, mk_sort(u)}, {a, A}, {b, A}, {c, A}, {d, A}, {H1, id_u(A, b, a)},
{H2, id_u(A, b, c)}, {H3, id_u(A, c, d)}}
local mP = mk_metavar("P", Pi(scope, mk_metavar("P_ty", Pi(scope, mk_sort(mk_meta_univ("l_P"))))(A, a, b, c, d, H1, H2, H3)))(A, a, b, c, d, H1, H2, H3)
local ma = mk_metavar("a", Pi(scope, mk_metavar("a_ty", Pi(scope, mk_sort(mk_meta_univ("l_a"))))(A, a, b, c, d, H1, H2, H3)))(A, a, b, c, d, H1, H2, H3)
local mb = mk_metavar("b", Pi(scope, mk_metavar("b_ty", Pi(scope, mk_sort(mk_meta_univ("l_b"))))(A, a, b, c, d, H1, H2, H3)))(A, a, b, c, d, H1, H2, H3)
local mA1 = mk_metavar("A1", Pi(scope, mk_sort(mk_meta_univ("l_A1"))))(A, a, b, c, d, H1, H2, H3)
local mA2 = mk_metavar("A2", Pi(scope, mk_sort(mk_meta_univ("l_A2"))))(A, a, b, c, d, H1, H2, H3)
print("================")
print(tc2:check(Fun(scope,
subst_u(mA1, mP, mb, ma,
H1,
trans_u(mA2, b, c, d, H2, H3)))))

6
tests/lua/tc_bug1.lua
View file

@ -19,9 +19,9 @@ 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(Bool, Bool, Bool)))
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_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_axiom("Ax1", q(a)))
env = add_decl(env, mk_axiom("Ax2", q(a)))
env = add_decl(env, mk_axiom("Ax3", q(b)))