Fix bugs in elaborator. Cleanup tests.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
8f4a844598
commit
3721577700
4 changed files with 255 additions and 107 deletions
|
|
@ -37,7 +37,6 @@ elaborator::elaborator(environment const & env):
|
|||
|
||||
void elaborator::unify(expr const & e1, expr const & e2, context const & ctx) {
|
||||
if (has_metavar(e1) || has_metavar(e2)) {
|
||||
// std::cout << "UNIFY: " << e1 << " <--> " << e2 << "\n";
|
||||
m_metaenv.unify(e1, e2, ctx);
|
||||
}
|
||||
}
|
||||
|
|
@ -97,7 +96,12 @@ expr elaborator::process(expr const & e, context const & ctx) {
|
|||
switch (e.kind()) {
|
||||
case expr_kind::Constant:
|
||||
if (is_metavar(e)) {
|
||||
expr r = m_metaenv.root_at(e, ctx);
|
||||
if (is_metavar(r)) {
|
||||
return expr();
|
||||
} else {
|
||||
return process(r, ctx);
|
||||
}
|
||||
} else {
|
||||
return m_env.get_object(const_name(e)).get_type();
|
||||
}
|
||||
|
|
@ -150,7 +154,12 @@ expr elaborator::process(expr const & e, context const & ctx) {
|
|||
}
|
||||
|
||||
expr elaborator::operator()(expr const & e) {
|
||||
expr t = process(e, context());
|
||||
while (true) {
|
||||
process(e, context());
|
||||
if (!m_metaenv.modified())
|
||||
break;
|
||||
m_metaenv.reset_modified();
|
||||
}
|
||||
return m_metaenv.instantiate_metavars(e);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -8,9 +8,9 @@ Author: Leonardo de Moura
|
|||
#include <iomanip>
|
||||
#include "metavar_env.h"
|
||||
#include "name_set.h"
|
||||
#include "free_vars.h"
|
||||
#include "exception.h"
|
||||
#include "for_each.h"
|
||||
#include "expr_eq.h"
|
||||
#include "replace.h"
|
||||
#include "printer.h"
|
||||
#include "beta.h"
|
||||
|
|
@ -94,23 +94,6 @@ metavar_env::cell const & metavar_env::root_cell(expr const & m) const {
|
|||
return root_cell(metavar_idx(m));
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Functional object expr -> expr
|
||||
If the input expression is a (assigned) metavariable, then
|
||||
return its substitution. Otherwise, return the input expression.
|
||||
*/
|
||||
struct root_fn {
|
||||
metavar_env const & m_uf;
|
||||
root_fn(metavar_env const & uf):m_uf(uf) {}
|
||||
|
||||
expr const & operator()(expr const & e) const {
|
||||
if (is_metavar(e))
|
||||
return m_uf.root(e);
|
||||
else
|
||||
return e;
|
||||
}
|
||||
};
|
||||
|
||||
/** \brief Auxiliary function for computing the new rank of an equivalence class. */
|
||||
unsigned metavar_env::new_rank(unsigned r1, unsigned r2) {
|
||||
if (r1 == r2) return r1 + 1;
|
||||
|
|
@ -135,13 +118,25 @@ unsigned metavar_env::new_rank(unsigned r1, unsigned r2) {
|
|||
3) The context of every metavariable in s is unifiable with the
|
||||
context of m.
|
||||
*/
|
||||
void metavar_env::assign_term(expr const & m, expr const & s) {
|
||||
void metavar_env::assign_term(expr const & m, expr s, context const & ctx) {
|
||||
lean_assert(is_metavar(m));
|
||||
lean_assert(!is_assigned(m));
|
||||
lean_assert(!is_metavar(s));
|
||||
cell & mc = root_cell(m);
|
||||
unsigned len_mc = mc.m_context;
|
||||
unsigned fv_range = 0; // s may contain variables between [0, fv_range)
|
||||
unsigned len_mc = length(mc.m_context);
|
||||
unsigned len_ctx = length(ctx);
|
||||
if (len_ctx < len_mc) {
|
||||
// mc is used in a context with len_mc variables,
|
||||
// but s free variables are references to a smaller context.
|
||||
// So, we must lift s free variables.
|
||||
s = lift_free_vars(s, len_mc - len_ctx);
|
||||
} else if (len_ctx > len_mc) {
|
||||
// s must only contain free variables that are available in mc.m_context
|
||||
if (has_free_var(s, 0, len_ctx - len_mc))
|
||||
failed_to_unify();
|
||||
s = lower_free_vars(s, len_ctx - len_mc);
|
||||
}
|
||||
unsigned fv_range = 0;
|
||||
auto proc = [&](expr const & n, unsigned offset) {
|
||||
if (is_var(n)) {
|
||||
unsigned vidx = var_idx(n);
|
||||
|
|
@ -194,6 +189,7 @@ metavar_env::metavar_env(environment const & env, name_set const * available_def
|
|||
m_max_depth = max_depth;
|
||||
m_depth = 0;
|
||||
m_interrupted = false;
|
||||
m_modified = false;
|
||||
}
|
||||
|
||||
metavar_env::metavar_env(environment const & env, name_set const * available_defs):
|
||||
|
|
@ -204,6 +200,7 @@ metavar_env::metavar_env(environment const & env):metavar_env(env, nullptr) {
|
|||
}
|
||||
|
||||
expr metavar_env::mk_metavar(context const & ctx) {
|
||||
m_modified = true;
|
||||
unsigned vidx = m_cells.size();
|
||||
expr m = ::lean::mk_metavar(vidx);
|
||||
m_cells.push_back(cell(m, ctx, vidx));
|
||||
|
|
@ -211,18 +208,34 @@ expr metavar_env::mk_metavar(context const & ctx) {
|
|||
}
|
||||
|
||||
bool metavar_env::is_assigned(expr const & m) const {
|
||||
return !is_metavar(root(m));
|
||||
return !is_metavar(root_cell(m).m_expr);
|
||||
}
|
||||
|
||||
expr const & metavar_env::root(expr const & e) const {
|
||||
return is_metavar(e) ? root_cell(e).m_expr : e;
|
||||
expr metavar_env::root_at(expr const & e, unsigned ctx_size) const {
|
||||
if (is_metavar(e)) {
|
||||
cell const & c = root_cell(e);
|
||||
if (is_metavar(c.m_expr)) {
|
||||
return c.m_expr;
|
||||
} else {
|
||||
unsigned len_c = length(c.m_context);
|
||||
lean_assert(len_c <= ctx_size);
|
||||
if (len_c < ctx_size) {
|
||||
return lift_free_vars(c.m_expr, ctx_size - len_c);
|
||||
} else {
|
||||
return c.m_expr;
|
||||
}
|
||||
}
|
||||
} else {
|
||||
return e;
|
||||
}
|
||||
}
|
||||
|
||||
void metavar_env::assign(expr const & m, expr const & s) {
|
||||
void metavar_env::assign(expr const & m, expr const & s, context const & ctx) {
|
||||
lean_assert(is_metavar(m));
|
||||
lean_assert(!is_assigned(m));
|
||||
if (m == s)
|
||||
return;
|
||||
m_modified = true;
|
||||
cell & mc = root_cell(m);
|
||||
lean_assert(is_metavar(mc.m_expr));
|
||||
lean_assert(metavar_idx(mc.m_expr) == mc.m_find);
|
||||
|
|
@ -244,16 +257,11 @@ void metavar_env::assign(expr const & m, expr const & s) {
|
|||
mc.m_find = sc.m_find;
|
||||
}
|
||||
} else {
|
||||
assign_term(m, _s);
|
||||
assign_term(m, _s, ctx);
|
||||
}
|
||||
lean_assert(check_invariant());
|
||||
}
|
||||
|
||||
bool metavar_env::is_modulo_eq(expr const & e1, expr const & e2) {
|
||||
expr_eq_fn<root_fn, false> proc(root_fn(*this));
|
||||
return proc(e1, e2);
|
||||
}
|
||||
|
||||
expr metavar_env::instantiate_metavars(expr const & e) {
|
||||
auto it = [&](expr const & c, unsigned offset) -> expr {
|
||||
if (is_metavar(c)) {
|
||||
|
|
@ -268,10 +276,13 @@ expr metavar_env::instantiate_metavars(expr const & e) {
|
|||
rc.m_state = state::Processing;
|
||||
rc.m_expr = instantiate_metavars(rc.m_expr);
|
||||
rc.m_state = state::Processed;
|
||||
return rc.m_expr;
|
||||
lean_assert(length(rc.m_context) <= offset);
|
||||
return lift_free_vars(rc.m_expr, offset - length(rc.m_context));
|
||||
}
|
||||
case state::Processing: throw exception("cycle detected");
|
||||
case state::Processed: return rc.m_expr;
|
||||
case state::Processed:
|
||||
lean_assert(length(rc.m_context) <= offset);
|
||||
return lift_free_vars(rc.m_expr, offset - length(rc.m_context));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -347,7 +358,7 @@ void metavar_env::unify_ctx_entries(context const & ctx1, context const & ctx2)
|
|||
auto it1 = ctx1.begin();
|
||||
auto end1 = ctx1.end();
|
||||
auto it2 = ctx2.begin();
|
||||
for (; it1 != end1; ++it1) {
|
||||
for (; it1 != end1; ++it1, ++it2) {
|
||||
context_entry const & e1 = *it1;
|
||||
context_entry const & e2 = *it2;
|
||||
|
||||
|
|
@ -371,9 +382,8 @@ void metavar_env::unify_ctx_entries(context const & ctx1, context const & ctx2)
|
|||
|
||||
// Little hack for matching (?m #0) with t
|
||||
// TODO: implement some support for higher order unification.
|
||||
bool metavar_env::is_simple_ho_match_core(expr const & e1, expr const & e2, context const & ctx) {
|
||||
if (is_app(e1) && is_metavar(arg(e1,0)) && !is_assigned(arg(e1,0)) && is_var(arg(e1,1), 0) && num_args(e1) == 2 && length(ctx) > 0) {
|
||||
assign(arg(e1,0), mk_lambda(car(ctx).get_name(), car(ctx).get_domain(), e2));
|
||||
bool metavar_env::is_simple_ho_match(expr const & e1, expr const & e2, context const & ctx) {
|
||||
if (is_app(e1) && is_metavar(arg(e1,0)) && is_var(arg(e1,1), 0) && num_args(e1) == 2 && length(ctx) > 0) {
|
||||
return true;
|
||||
} else {
|
||||
return false;
|
||||
|
|
@ -382,8 +392,8 @@ bool metavar_env::is_simple_ho_match_core(expr const & e1, expr const & e2, cont
|
|||
|
||||
// Little hack for matching (?m #0) with t
|
||||
// TODO: implement some support for higher order unification.
|
||||
bool metavar_env::is_simple_ho_match(expr const & e1, expr const & e2, context const & ctx) {
|
||||
return is_simple_ho_match_core(e1, e2, ctx) || is_simple_ho_match_core(e2, e1, ctx);
|
||||
void metavar_env::unify_simple_ho_match(expr const & e1, expr const & e2, context const & ctx) {
|
||||
unify(arg(e1,0), mk_lambda(car(ctx).get_name(), car(ctx).get_domain(), e2), ctx);
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -396,6 +406,8 @@ void metavar_env::unify_core(expr const & e1, expr const & e2, context const & c
|
|||
lean_assert(!is_metavar(e2));
|
||||
if (e1 == e2) {
|
||||
return;
|
||||
} else if (is_type(e1) && is_type(e2)) {
|
||||
return; // ignoring type universe levels. We let the kernel check that
|
||||
} else if (is_abstraction(e1) && is_abstraction(e2)) {
|
||||
unify(abst_domain(e1), abst_domain(e2), ctx);
|
||||
unify(abst_body(e1), abst_body(e2), extend(ctx, abst_name(e1), abst_domain(e1)));
|
||||
|
|
@ -413,7 +425,9 @@ void metavar_env::unify_core(expr const & e1, expr const & e2, context const & c
|
|||
unify(arg(e1, i), arg(e2, i), ctx);
|
||||
}
|
||||
} else if (is_simple_ho_match(e1, e2, ctx)) {
|
||||
// done
|
||||
unify_simple_ho_match(e1, e2, ctx);
|
||||
} else if (is_simple_ho_match(e2, e1, ctx)) {
|
||||
unify_simple_ho_match(e2, e1, ctx);
|
||||
} else {
|
||||
failed_to_unify();
|
||||
}
|
||||
|
|
@ -422,13 +436,15 @@ void metavar_env::unify_core(expr const & e1, expr const & e2, context const & c
|
|||
|
||||
void metavar_env::unify(expr const & e1, expr const & e2, context const & ctx) {
|
||||
flet<unsigned> l(m_depth, m_depth+1);
|
||||
expr const & r1 = root(e1);
|
||||
expr const & r2 = root(e2);
|
||||
if (m_depth > m_max_depth)
|
||||
throw exception("unifier maximum recursion depth exceeded");
|
||||
expr const & r1 = root_at(e1, ctx);
|
||||
expr const & r2 = root_at(e2, ctx);
|
||||
if (is_metavar(r1)) {
|
||||
assign(r1, r2);
|
||||
assign(r1, r2, ctx);
|
||||
} else {
|
||||
if (is_metavar(r2)) {
|
||||
assign(r2, r1);
|
||||
assign(r2, r1, ctx);
|
||||
} else {
|
||||
unify_core(r1, r2, ctx);
|
||||
}
|
||||
|
|
@ -472,3 +488,4 @@ bool metavar_env::check_invariant() const {
|
|||
return true;
|
||||
}
|
||||
}
|
||||
void print(lean::metavar_env const & env) { env.display(std::cout); }
|
||||
|
|
|
|||
|
|
@ -60,6 +60,7 @@ class metavar_env {
|
|||
// If m_available_definitions != nullptr, then only the
|
||||
// definitions in m_available_definitions are unfolded during unification.
|
||||
name_set const * m_available_definitions;
|
||||
bool m_modified;
|
||||
volatile bool m_interrupted;
|
||||
|
||||
bool is_root(unsigned midx) const;
|
||||
|
|
@ -68,15 +69,14 @@ class metavar_env {
|
|||
cell const & root_cell(unsigned midx) const;
|
||||
cell & root_cell(expr const & m);
|
||||
cell const & root_cell(expr const & m) const;
|
||||
friend struct root_fn;
|
||||
unsigned new_rank(unsigned r1, unsigned r2);
|
||||
void assign_term(expr const & m, expr const & s);
|
||||
void assign_term(expr const & m, expr s, context const & ctx);
|
||||
[[noreturn]] void failed_to_unify();
|
||||
void ensure_same_length(context & ctx1, context & ctx2);
|
||||
void unify_ctx_prefix(context const & ctx1, context const & ctx2);
|
||||
void unify_ctx_entries(context const & ctx1, context const & ctx2);
|
||||
bool is_simple_ho_match_core(expr const & e1, expr const & e2, context const & ctx);
|
||||
bool is_simple_ho_match(expr const & e1, expr const & e2, context const & ctx);
|
||||
void unify_simple_ho_match(expr const & e1, expr const & e2, context const & ctx);
|
||||
void unify_core(expr const & e1, expr const & e2, context const & ctx);
|
||||
|
||||
public:
|
||||
|
|
@ -98,19 +98,26 @@ public:
|
|||
/**
|
||||
\brief If the given expression is a metavariable, then return the root
|
||||
of the equivalence class. Otherwise, return itself.
|
||||
|
||||
If the the metavariable was defined in smaller context, we lift the
|
||||
free variables to match the size of the given context.
|
||||
*/
|
||||
expr const & root(expr const & e) const;
|
||||
expr root_at(expr const & m, context const & ctx) const { return root_at(m, length(ctx)); }
|
||||
/**
|
||||
\brief Similar to the previous function, but the context is given.
|
||||
*/
|
||||
expr root_at(expr const & m, unsigned ctx_size) const;
|
||||
|
||||
/**
|
||||
\brief If the given expression is a metavariable, then return the root
|
||||
of the equivalence class. Otherwise, return itself.
|
||||
*/
|
||||
// expr const & root(expr const & e) const
|
||||
|
||||
/**
|
||||
\brief Assign m <- s
|
||||
*/
|
||||
void assign(expr const & m, expr const & s);
|
||||
|
||||
/**
|
||||
\brief Return true iff \c e1 is structurally equal to \c e2
|
||||
modulo the union find table.
|
||||
*/
|
||||
bool is_modulo_eq(expr const & e1, expr const & e2);
|
||||
void assign(expr const & m, expr const & s, context const & ctx = context());
|
||||
|
||||
/**
|
||||
\brief Replace the metavariables occurring in \c e with the
|
||||
|
|
@ -151,6 +158,9 @@ public:
|
|||
*/
|
||||
void clear();
|
||||
|
||||
bool modified() const { return m_modified; }
|
||||
void reset_modified() { m_modified = false; }
|
||||
|
||||
void set_interrupt(bool flag);
|
||||
|
||||
void display(std::ostream & out) const;
|
||||
|
|
|
|||
|
|
@ -12,10 +12,11 @@ Author: Leonardo de Moura
|
|||
#include "abstract.h"
|
||||
#include "toplevel.h"
|
||||
#include "basic_thms.h"
|
||||
#include "type_check.h"
|
||||
#include "kernel_exception.h"
|
||||
using namespace lean;
|
||||
|
||||
static name g_placeholder_name(name(name(name(0u), "library"), "placeholder"));
|
||||
static name g_placeholder_name("_");
|
||||
/** \brief Return a new placeholder expression. To be able to track location,
|
||||
a new constant for each placeholder.
|
||||
*/
|
||||
|
|
@ -77,7 +78,8 @@ expr replace_placeholders_with_metavars(expr const & e, metavar_env & menv) {
|
|||
return replace(e, context(), menv);
|
||||
}
|
||||
|
||||
expr elaborate(elaborator & elb, expr const & e) {
|
||||
expr elaborate(expr const & e, environment const & env) {
|
||||
elaborator elb(env);
|
||||
expr new_e = replace_placeholders_with_metavars(e, elb.menv());
|
||||
return elb(new_e);
|
||||
}
|
||||
|
|
@ -112,13 +114,11 @@ static void tst2() {
|
|||
expr t1 = f(m1, m2);
|
||||
expr t2 = f(m1, m1);
|
||||
lean_assert(t1 != t2);
|
||||
lean_assert(!u.is_modulo_eq(t1, t2));
|
||||
// m1 <- m2
|
||||
u.assign(m1, m2);
|
||||
std::cout << u << "\n";
|
||||
lean_assert(u.root(m2) == m2);
|
||||
lean_assert(u.root(m1) == m2);
|
||||
lean_assert(u.is_modulo_eq(t1, t2));
|
||||
lean_assert(u.root_at(m2, 0) == m2);
|
||||
lean_assert(u.root_at(m1, 0) == m2);
|
||||
expr a = Const("a");
|
||||
expr b = Const("b");
|
||||
expr g = Const("g");
|
||||
|
|
@ -127,15 +127,8 @@ static void tst2() {
|
|||
expr t5 = f(a, a);
|
||||
lean_assert(t3 != t4);
|
||||
lean_assert(t4 != t5);
|
||||
lean_assert(!u.is_modulo_eq(t3, t4));
|
||||
lean_assert(!u.is_modulo_eq(t4, t5));
|
||||
u.assign(m2, a);
|
||||
lean_assert(u.is_modulo_eq(t3, t4));
|
||||
lean_assert(u.is_modulo_eq(t4, t5));
|
||||
lean_assert(u.is_modulo_eq(g(t3, m1), g(t4, a)));
|
||||
lean_assert(!u.is_modulo_eq(g(t3, m3), g(t4, b)));
|
||||
u.assign(m3, b);
|
||||
lean_assert(u.is_modulo_eq(g(t3, m3), g(t4, b)));
|
||||
std::cout << u << "\n";
|
||||
expr m4 = u.mk_metavar();
|
||||
std::cout << u << "\n";
|
||||
|
|
@ -214,10 +207,10 @@ static void tst5() {
|
|||
metavar_env uenv2(uenv);
|
||||
uenv2.unify(t1, t2);
|
||||
std::cout << uenv2 << "\n";
|
||||
lean_assert(uenv2.root(m1) == g(a, b));
|
||||
lean_assert(uenv2.root(m2) == a);
|
||||
lean_assert(uenv2.root(m3) == A);
|
||||
lean_assert(uenv2.root(m4) == B);
|
||||
lean_assert(uenv2.root_at(m1,0) == g(a, b));
|
||||
lean_assert(uenv2.root_at(m2,0) == a);
|
||||
lean_assert(uenv2.root_at(m3,0) == A);
|
||||
lean_assert(uenv2.root_at(m4,0) == B);
|
||||
lean_assert(uenv2.instantiate_metavars(t1) == f(g(a, b), g(a, F)));
|
||||
lean_assert(uenv2.instantiate_metavars(t2) == f(g(a, b), Id(g(a, A >> B))));
|
||||
metavar_env uenv3(uenv);
|
||||
|
|
@ -251,7 +244,7 @@ static void tst6() {
|
|||
expr t2 = f(g(m3), Var(0));
|
||||
std::cout << "----------------\n";
|
||||
std::cout << uenv << "\n";
|
||||
uenv.unify(t1, t2);
|
||||
uenv.unify(t1, t2, ctx2);
|
||||
std::cout << uenv << "\n";
|
||||
std::cout << uenv.instantiate_metavars(t1) << "\n";
|
||||
std::cout << uenv.instantiate_metavars(t2) << "\n";
|
||||
|
|
@ -306,9 +299,30 @@ static void tst7() {
|
|||
std::cout << uenv.instantiate_metavars(t2) << "\n";
|
||||
}
|
||||
|
||||
// Check elaborator success
|
||||
static void success(expr const & e, expr const & expected, environment const & env) {
|
||||
std::cout << "\n" << e << "\n------>\n" << elaborate(e, env) << "\n";
|
||||
lean_assert(elaborate(e, env) == expected);
|
||||
std::cout << infer_type(elaborate(e, env), env) << "\n";
|
||||
}
|
||||
|
||||
// Check elaborator failure
|
||||
static void fails(expr const & e, environment const & env) {
|
||||
try {
|
||||
elaborate(e, env);
|
||||
lean_unreachable();
|
||||
} catch (exception &) {
|
||||
}
|
||||
}
|
||||
|
||||
// Check elaborator partial success (i.e., result still contain some metavariables */
|
||||
static void unsolved(expr const & e, environment const & env) {
|
||||
std::cout << "\n" << e << "\n------>\n" << elaborate(e, env) << "\n";
|
||||
lean_assert(has_metavar(elaborate(e, env)));
|
||||
}
|
||||
|
||||
static void tst8() {
|
||||
environment env;
|
||||
elaborator elb(env);
|
||||
expr A = Const("A");
|
||||
expr B = Const("B");
|
||||
expr F = Const("F");
|
||||
|
|
@ -320,17 +334,15 @@ static void tst8() {
|
|||
env.add_var("Real", Type());
|
||||
env.add_var("F", Pi({{A, Type()}, {B, Type()}, {g, A >> B}}, A));
|
||||
env.add_var("f", Nat >> Real);
|
||||
std::cout << "--------------------\n" << env << "\n";
|
||||
expr _ = mk_placholder();
|
||||
expr f = Const("f");
|
||||
expr t = F(_,_,f);
|
||||
std::cout << elaborate(elb, t) << "\n";
|
||||
lean_assert(elaborate(elb, t) == F(Nat, Real, f));
|
||||
success(F(_,_,f), F(Nat, Real, f), env);
|
||||
fails(F(_,Bool,f), env);
|
||||
success(F(_,_,Fun({a, Nat},a)), F(Nat,Nat,Fun({a,Nat},a)), env);
|
||||
}
|
||||
|
||||
static void tst9() {
|
||||
environment env = mk_toplevel();
|
||||
elaborator elb(env);
|
||||
expr a = Const("a");
|
||||
expr b = Const("b");
|
||||
expr c = Const("c");
|
||||
|
|
@ -342,15 +354,20 @@ static void tst9() {
|
|||
env.add_axiom("H1", Eq(a, b));
|
||||
env.add_axiom("H2", Eq(b, c));
|
||||
expr _ = mk_placholder();
|
||||
expr t = Trans(_,_,_,_,H1,H2);
|
||||
expr new_t = elb(elaborate(elb, t));
|
||||
std::cout << new_t << "\n";
|
||||
lean_assert(new_t == Trans(Bool,a,b,c,H1,H2));
|
||||
success(Trans(_,_,_,_,H1,H2), Trans(Bool,a,b,c,H1,H2), env);
|
||||
success(Trans(_,_,_,_,Symm(_,_,_,H2),Symm(_,_,_,H1)),
|
||||
Trans(Bool,c,b,a,Symm(Bool,b,c,H2),Symm(Bool,a,b,H1)), env);
|
||||
success(Symm(_,_,_,Trans(_,_,_,_,Symm(_,_,_,H2),Symm(_,_,_,H1))),
|
||||
Symm(Bool,c,a,Trans(Bool,c,b,a,Symm(Bool,b,c,H2),Symm(Bool,a,b,H1))), env);
|
||||
env.add_axiom("H3", a);
|
||||
expr H3 = Const("H3");
|
||||
success(EqTIntro(_, EqMP(_,_,Symm(_,_,_,Trans(_,_,_,_,Symm(_,_,_,H2),Symm(_,_,_,H1))), H3)),
|
||||
EqTIntro(c, EqMP(a,c,Symm(Bool,c,a,Trans(Bool,c,b,a,Symm(Bool,b,c,H2),Symm(Bool,a,b,H1))), H3)),
|
||||
env);
|
||||
}
|
||||
|
||||
static void tst10() {
|
||||
environment env = mk_toplevel();
|
||||
elaborator elb(env);
|
||||
expr Nat = Const("Nat");
|
||||
env.add_var("Nat", Type());
|
||||
env.add_var("vec", Nat >> Type());
|
||||
|
|
@ -367,14 +384,21 @@ static void tst10() {
|
|||
env.add_definition("fact", Bool, Eq(a, b));
|
||||
env.add_axiom("H", fact);
|
||||
expr _ = mk_placholder();
|
||||
expr t = Congr2(_,_,_,_,f,H);
|
||||
std::cout << elaborate(elb, t) << "\n";
|
||||
lean_assert(elaborate(elb,t) == Congr2(Nat, Fun({n,Nat}, vec(n) >> Nat), a, b, f, H));
|
||||
success(Congr2(_,_,_,_,f,H),
|
||||
Congr2(Nat, Fun({n,Nat}, vec(n) >> Nat), a, b, f, H), env);
|
||||
env.add_var("g", Pi({n, Nat}, vec(n) >> Nat));
|
||||
expr g = Const("g");
|
||||
env.add_axiom("H2", Eq(f, g));
|
||||
expr H2 = Const("H2");
|
||||
success(Congr(_,_,_,_,_,_,H2,H),
|
||||
Congr(Nat, Fun({n,Nat}, vec(n) >> Nat), f, g, a, b, H2, H), env);
|
||||
success(Congr(_,_,_,_,_,_,Refl(_,f),H),
|
||||
Congr(Nat, Fun({n,Nat}, vec(n) >> Nat), f, f, a, b, Refl(Pi({n, Nat}, vec(n) >> Nat),f), H), env);
|
||||
success(Refl(_,a), Refl(Nat,a), env);
|
||||
}
|
||||
|
||||
static void tst11() {
|
||||
environment env;
|
||||
elaborator elb(env);
|
||||
expr Nat = Const("Nat");
|
||||
env.add_var("Nat", Type());
|
||||
expr R = Const("R");
|
||||
|
|
@ -385,15 +409,19 @@ static void tst11() {
|
|||
env.add_var("f", Nat >> ((R >> Nat) >> R));
|
||||
expr x = Const("x");
|
||||
expr y = Const("y");
|
||||
expr z = Const("z");
|
||||
expr _ = mk_placholder();
|
||||
expr t = Fun({{x,_},{y,_}}, f(x, y));
|
||||
std::cout << t << "\n";
|
||||
std::cout << elaborate(elb, t) << "\n";
|
||||
success(Fun({{x,_},{y,_}}, f(x, y)),
|
||||
Fun({{x,Nat},{y,R >> Nat}}, f(x, y)), env);
|
||||
success(Fun({{x,_},{y,_},{z,_}}, Eq(f(x, y), f(x, z))),
|
||||
Fun({{x,Nat},{y,R >> Nat},{z,R >> Nat}}, Eq(f(x, y), f(x, z))), env);
|
||||
expr A = Const("A");
|
||||
success(Fun({{A,Type()},{x,_},{y,_},{z,_}}, Eq(f(x, y), f(x, z))),
|
||||
Fun({{A,Type()},{x,Nat},{y,R >> Nat},{z,R >> Nat}}, Eq(f(x, y), f(x, z))), env);
|
||||
}
|
||||
|
||||
static void tst12() {
|
||||
environment env;
|
||||
elaborator elb(env);
|
||||
expr A = Const("A");
|
||||
expr B = Const("B");
|
||||
expr a = Const("a");
|
||||
|
|
@ -405,14 +433,12 @@ static void tst12() {
|
|||
env.add_var("f", Pi({{A,Type()},{a,A},{b,A}}, A));
|
||||
env.add_var("g", Nat >> Nat);
|
||||
expr _ = mk_placholder();
|
||||
expr t = Fun({{a,_},{b,_}},g(f(_,a,b)));
|
||||
std::cout << elaborate(elb, t) << "\n";
|
||||
lean_assert(elaborate(elb, t) == Fun({{a,Nat},{b,Nat}},g(f(Nat,a,b))));
|
||||
success(Fun({{a,_},{b,_}},g(f(_,a,b))),
|
||||
Fun({{a,Nat},{b,Nat}},g(f(Nat,a,b))), env);
|
||||
}
|
||||
|
||||
static void tst13() {
|
||||
environment env;
|
||||
elaborator elb(env);
|
||||
expr lst = Const("list");
|
||||
expr nil = Const("nil");
|
||||
expr cons = Const("cons");
|
||||
|
|
@ -427,24 +453,108 @@ static void tst13() {
|
|||
env.add_var("cons", Pi({{A, Type()}, {a, A}, {l, lst(A)}}, lst(A)));
|
||||
env.add_var("f", lst(N>>N) >> Bool);
|
||||
expr _ = mk_placholder();
|
||||
expr t = Fun({a,_}, f(cons(_, a, cons(_, a, nil(_)))));
|
||||
std::cout << elaborate(elb, t) << "\n";
|
||||
success(Fun({a,_}, f(cons(_, a, cons(_, a, nil(_))))),
|
||||
Fun({a,N>>N}, f(cons(N>>N, a, cons(N>>N, a, nil(N>>N))))), env);
|
||||
}
|
||||
|
||||
static void tst14() {
|
||||
environment env;
|
||||
elaborator elb(env);
|
||||
expr x = Const("x");
|
||||
expr _ = mk_placholder();
|
||||
expr omega = mk_app(Fun({x,_}, x(x)), Fun({x,_}, x(x)));
|
||||
try {
|
||||
elaborate(elb, omega);
|
||||
lean_unreachable();
|
||||
} catch (exception ex) {
|
||||
}
|
||||
fails(omega, env);
|
||||
}
|
||||
|
||||
static void tst15() {
|
||||
environment env;
|
||||
expr B = Const("B");
|
||||
expr A = Const("A");
|
||||
expr x = Const("x");
|
||||
expr f = Const("f");
|
||||
expr _ = mk_placholder();
|
||||
env.add_var("f", Pi({B, Type()}, B >> B));
|
||||
fails(Fun({{x,_}, {A,Type()}}, f(A, x)), env);
|
||||
success(Fun({{A,Type()}, {x,_}}, f(A, x)),
|
||||
Fun({{A,Type()}, {x,A}}, f(A, x)), env);
|
||||
success(Fun({{A,Type()}, {B,Type()}, {x,_}}, f(A, x)),
|
||||
Fun({{A,Type()}, {B,Type()}, {x,A}}, f(A, x)), env);
|
||||
success(Fun({{A,Type()}, {B,Type()}, {x,_}}, f(B, x)),
|
||||
Fun({{A,Type()}, {B,Type()}, {x,B}}, f(B, x)), env);
|
||||
success(Fun({{A,Type()}, {B,Type()}, {x,_}}, Eq(f(B, x), f(_,x))),
|
||||
Fun({{A,Type()}, {B,Type()}, {x,B}}, Eq(f(B, x), f(B,x))), env);
|
||||
success(Fun({{A,Type()}, {B,_}, {x,_}}, Eq(f(B, x), f(_,x))),
|
||||
Fun({{A,Type()}, {B,Type()}, {x,B}}, Eq(f(B, x), f(B,x))), env);
|
||||
unsolved(Fun({{A,_}, {B,_}, {x,_}}, Eq(f(B, x), f(_,x))), env);
|
||||
}
|
||||
|
||||
static void tst16() {
|
||||
environment env = mk_toplevel();
|
||||
expr A = Const("A");
|
||||
expr B = Const("B");
|
||||
expr f = Const("f");
|
||||
expr g = Const("g");
|
||||
expr x = Const("x");
|
||||
expr y = Const("y");
|
||||
env.add_var("N", Type());
|
||||
env.add_var("f", Pi({A,Type()}, A >> A));
|
||||
expr N = Const("N");
|
||||
expr _ = mk_placholder();
|
||||
success(Fun({g, Pi({A, Type()}, A >> (A >> Bool))}, g(_, True, False)),
|
||||
Fun({g, Pi({A, Type()}, A >> (A >> Bool))}, g(Bool, True, False)),
|
||||
env);
|
||||
success(Fun({g, Pi({A, TypeU}, A >> (A >> Bool))}, g(_, Bool, Bool)),
|
||||
Fun({g, Pi({A, TypeU}, A >> (A >> Bool))}, g(Type(), Bool, Bool)),
|
||||
env);
|
||||
success(Fun({g, Pi({A, TypeU}, A >> (A >> Bool))}, g(_, Bool, N)),
|
||||
Fun({g, Pi({A, TypeU}, A >> (A >> Bool))}, g(Type(), Bool, N)),
|
||||
env);
|
||||
success(Fun({g, Pi({A, Type()}, A >> (A >> Bool))},
|
||||
g(_,
|
||||
Fun({{x,_},{y,_}}, Eq(f(_, x), f(_, y))),
|
||||
Fun({{x,N},{y,Bool}}, True))),
|
||||
Fun({g, Pi({A, Type()}, A >> (A >> Bool))},
|
||||
g((N >> (Bool >> Bool)),
|
||||
Fun({{x,N},{y,Bool}}, Eq(f(N, x), f(Bool, y))),
|
||||
Fun({{x,N},{y,Bool}}, True))), env);
|
||||
|
||||
success(Fun({g, Pi({A, Type()}, A >> (A >> Bool))},
|
||||
g(_,
|
||||
Fun({{x,N},{y,_}}, Eq(f(_, x), f(_, y))),
|
||||
Fun({{x,_},{y,Bool}}, True))),
|
||||
Fun({g, Pi({A, Type()}, A >> (A >> Bool))},
|
||||
g((N >> (Bool >> Bool)),
|
||||
Fun({{x,N},{y,Bool}}, Eq(f(N, x), f(Bool, y))),
|
||||
Fun({{x,N},{y,Bool}}, True))), env);
|
||||
}
|
||||
|
||||
static void tst17() {
|
||||
environment env = mk_toplevel();
|
||||
expr A = Const("A");
|
||||
expr B = Const("B");
|
||||
expr C = Const("C");
|
||||
expr a = Const("a");
|
||||
expr b = Const("b");
|
||||
expr eq = Const("eq");
|
||||
expr _ = mk_placholder();
|
||||
env.add_var("eq", Pi({A, Type()}, A >> (A >> Bool)));
|
||||
success(Fun({{A, Type()},{B,Type()},{a,_},{b,B}}, eq(_,a,b)),
|
||||
Fun({{A, Type()},{B,Type()},{a,B},{b,B}}, eq(B,a,b)), env);
|
||||
success(Fun({{A, Type()},{B,Type()},{a,_},{b,A}}, eq(_,a,b)),
|
||||
Fun({{A, Type()},{B,Type()},{a,A},{b,A}}, eq(A,a,b)), env);
|
||||
success(Fun({{A, Type()},{B,Type()},{a,A},{b,_}}, eq(_,a,b)),
|
||||
Fun({{A, Type()},{B,Type()},{a,A},{b,A}}, eq(A,a,b)), env);
|
||||
success(Fun({{A, Type()},{B,Type()},{a,B},{b,_}}, eq(_,a,b)),
|
||||
Fun({{A, Type()},{B,Type()},{a,B},{b,B}}, eq(B,a,b)), env);
|
||||
success(Fun({{A, Type()},{B,Type()},{a,B},{b,_},{C,Type()}}, eq(_,a,b)),
|
||||
Fun({{A, Type()},{B,Type()},{a,B},{b,B},{C,Type()}}, eq(B,a,b)), env);
|
||||
fails(Fun({{A, Type()},{B,Type()},{a,_},{b,_},{C,Type()}}, eq(C,a,b)), env);
|
||||
success(Fun({{A, Type()},{B,Type()},{a,_},{b,_},{C,Type()}}, eq(B,a,b)),
|
||||
Fun({{A, Type()},{B,Type()},{a,B},{b,B},{C,Type()}}, eq(B,a,b)), env);
|
||||
}
|
||||
|
||||
int main() {
|
||||
tst17();
|
||||
return 0;
|
||||
tst1();
|
||||
tst2();
|
||||
tst3();
|
||||
|
|
@ -459,5 +569,7 @@ int main() {
|
|||
tst12();
|
||||
tst13();
|
||||
tst14();
|
||||
tst15();
|
||||
tst16();
|
||||
return has_violations() ? 1 : 0;
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in a new issue