diff --git a/src/library/elaborator.cpp b/src/library/elaborator.cpp index 7577cc303..90ea46ff4 100644 --- a/src/library/elaborator.cpp +++ b/src/library/elaborator.cpp @@ -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)) { - return expr(); + 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); } } diff --git a/src/library/metavar_env.cpp b/src/library/metavar_env.cpp index 2451e337e..6e42d146c 100644 --- a/src/library/metavar_env.cpp +++ b/src/library/metavar_env.cpp @@ -8,9 +8,9 @@ Author: Leonardo de Moura #include #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 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 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); } diff --git a/src/library/metavar_env.h b/src/library/metavar_env.h index 279aee21e..abc8b6fc7 100644 --- a/src/library/metavar_env.h +++ b/src/library/metavar_env.h @@ -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; diff --git a/src/tests/library/implicit_args.cpp b/src/tests/library/implicit_args.cpp index 16d639aa5..7c37c675c 100644 --- a/src/tests/library/implicit_args.cpp +++ b/src/tests/library/implicit_args.cpp @@ -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; }