feat(kernel/metavar): make sure that a metavariable 'm' can only be assigned to a term that contains free variables available in the context associated with 'm'
This commit also simplifies the method check_pi in the type_checker and type_inferer.
It also fixes process_meta_app in the elaborator.
The problem was in the method process_meta_app and process_meta_inst.
They were processing convertability constrains as equality constraints.
For example, process_meta_app would handle
ctx |- Type << ?f b
as
ctx |- Type =:= ?f b
This is not correct because a ?f that returns (Type U) for b satisfies the first but not the second.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
51aee83b70
commit
4357c9196e
9 changed files with 295 additions and 217 deletions
|
|
@ -159,19 +159,69 @@ bool metavar_env_cell::is_assigned(expr const & m) const {
|
|||
return is_assigned(metavar_name(m));
|
||||
}
|
||||
|
||||
void metavar_env_cell::assign(name const & m, expr const & t, justification const & jst) {
|
||||
bool metavar_env_cell::assign(name const & m, expr const & t, justification const & jst) {
|
||||
lean_assert(!is_assigned(m));
|
||||
inc_timestamp();
|
||||
justification jst2 = jst;
|
||||
buffer<justification> jsts;
|
||||
expr t2 = instantiate_metavars(t, jsts);
|
||||
if (!jsts.empty()) {
|
||||
jst2 = justification(new normalize_assignment_justification(get_context(m), t, jst,
|
||||
jsts.size(), jsts.data()));
|
||||
}
|
||||
unsigned ctx_size = get_context_size(m);
|
||||
if (has_metavar(t2)) {
|
||||
bool failed = false;
|
||||
// Make sure the contexts of the metavariables occurring in \c t2 are
|
||||
// not too big.
|
||||
for_each(t2, [&](expr const & e, unsigned offset) {
|
||||
if (is_metavar(e)) {
|
||||
lean_assert(!is_assigned(e));
|
||||
unsigned range = free_var_range(e, metavar_env(this));
|
||||
if (range > ctx_size + offset) {
|
||||
unsigned extra = range - ctx_size - offset;
|
||||
auto it2 = m_metavar_data.find(metavar_name(e));
|
||||
if (it2 == nullptr) {
|
||||
failed = true;
|
||||
} else {
|
||||
unsigned e_ctx_size = it2->m_context.size();
|
||||
if (e_ctx_size < extra) {
|
||||
failed = true;
|
||||
} else {
|
||||
it2->m_context = it2->m_context.remove(e_ctx_size - extra, extra);
|
||||
lean_assert(free_var_range(e, metavar_env(this)) == ctx_size + offset);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
return true;
|
||||
});
|
||||
if (failed)
|
||||
return false;
|
||||
}
|
||||
if (free_var_range(t2, metavar_env(this)) > ctx_size)
|
||||
return false;
|
||||
auto it = m_metavar_data.find(m);
|
||||
lean_assert(it);
|
||||
it->m_subst = t;
|
||||
it->m_justification = jst;
|
||||
it->m_subst = t2;
|
||||
it->m_justification = jst2;
|
||||
return true;
|
||||
}
|
||||
|
||||
void metavar_env_cell::assign(expr const & m, expr const & t, justification const & j) {
|
||||
bool metavar_env_cell::assign(name const & m, expr const & t) {
|
||||
justification j;
|
||||
return assign(m, t, j);
|
||||
}
|
||||
|
||||
bool metavar_env_cell::assign(expr const & m, expr const & t, justification const & j) {
|
||||
lean_assert(is_metavar(m));
|
||||
lean_assert(!has_local_context(m));
|
||||
assign(metavar_name(m), t, j);
|
||||
return assign(metavar_name(m), t, j);
|
||||
}
|
||||
|
||||
bool metavar_env_cell::assign(expr const & m, expr const & t) {
|
||||
justification j;
|
||||
return assign(m, t, j);
|
||||
}
|
||||
|
||||
expr apply_local_context(expr const & a, local_context const & lctx, optional<metavar_env> const & menv) {
|
||||
|
|
|
|||
|
|
@ -77,6 +77,9 @@ public:
|
|||
context get_context(expr const & m) const;
|
||||
context get_context(name const & m) const;
|
||||
|
||||
unsigned get_context_size(expr const & m) const { return get_context(m).size(); }
|
||||
unsigned get_context_size(name const & m) const { return get_context(m).size(); }
|
||||
|
||||
/**
|
||||
\brief Return the type of the given metavariable.
|
||||
\pre is_metavar(m)
|
||||
|
|
@ -126,17 +129,27 @@ public:
|
|||
\brief Assign metavariable named \c m.
|
||||
|
||||
\pre !is_assigned(m)
|
||||
|
||||
\remark The method returns false if the assignment cannot be performed
|
||||
because \c t contain free variables that are not available in the context
|
||||
associated with \c m.
|
||||
*/
|
||||
void assign(name const & m, expr const & t, justification const & j = justification());
|
||||
bool assign(name const & m, expr const & t, justification const & j);
|
||||
bool assign(name const & m, expr const & t);
|
||||
|
||||
/**
|
||||
\brief Assign metavariable \c m to \c t.
|
||||
|
||||
\remark The method returns false if the assignment cannot be performed
|
||||
because \c t contain free variables that are not available in the context
|
||||
associated with \c m.
|
||||
|
||||
\pre is_metavar(m)
|
||||
\pre !has_meta_context(m)
|
||||
\pre !is_assigned(m)
|
||||
*/
|
||||
void assign(expr const & m, expr const & t, justification const & j = justification());
|
||||
bool assign(expr const & m, expr const & t, justification const & j);
|
||||
bool assign(expr const & m, expr const & t);
|
||||
|
||||
/**
|
||||
\brief Return the substitution associated with the given metavariable
|
||||
|
|
|
|||
|
|
@ -34,6 +34,14 @@ class type_checker::imp {
|
|||
return ro_environment(m_env);
|
||||
}
|
||||
|
||||
expr lift_free_vars(expr const & e, unsigned s, unsigned d) {
|
||||
return ::lean::lift_free_vars(e, s, d, m_menv.to_some_menv());
|
||||
}
|
||||
|
||||
expr lift_free_vars(expr const & e, unsigned d) {
|
||||
return ::lean::lift_free_vars(e, d, m_menv.to_some_menv());
|
||||
}
|
||||
|
||||
expr normalize(expr const & e, context const & ctx) {
|
||||
return m_normalizer(e, ctx);
|
||||
}
|
||||
|
|
@ -46,10 +54,10 @@ class type_checker::imp {
|
|||
return r;
|
||||
if (has_metavar(r) && m_menv && m_uc) {
|
||||
// Create two fresh variables A and B,
|
||||
// and assign r == (Pi(x : A), B x)
|
||||
// and assign r == (Pi(x : A), B)
|
||||
expr A = m_menv->mk_metavar(ctx);
|
||||
expr B = m_menv->mk_metavar(ctx);
|
||||
expr p = mk_pi(g_x_name, A, B(Var(0)));
|
||||
expr B = m_menv->mk_metavar(extend(ctx, g_x_name, A));
|
||||
expr p = mk_pi(g_x_name, A, B);
|
||||
justification jst = mk_function_expected_justification(ctx, s);
|
||||
m_uc->push_back(mk_eq_constraint(ctx, r, p, jst));
|
||||
return p;
|
||||
|
|
|
|||
|
|
@ -163,10 +163,15 @@ class elaborator::imp {
|
|||
return mk_assumption_justification(id);
|
||||
}
|
||||
|
||||
void push_front(cnstr_queue & q, unification_constraint const & c) {
|
||||
// std::cout << "PUSHING: "; display(std::cout, c); std::cout << "\n";
|
||||
q.push_front(c);
|
||||
}
|
||||
|
||||
/** \brief Add given constraint to the front of the current constraint queue */
|
||||
void push_front(unification_constraint const & c) {
|
||||
reset_quota();
|
||||
m_state.m_queue.push_front(c);
|
||||
push_front(m_state.m_queue, c);
|
||||
}
|
||||
|
||||
/** \brief Add given constraint to the end of the current constraint queue */
|
||||
|
|
@ -280,9 +285,9 @@ class elaborator::imp {
|
|||
*/
|
||||
void push_new_constraint(cnstr_queue & q, bool is_eq, context const & new_ctx, expr const & new_a, expr const & new_b, justification const & new_jst) {
|
||||
if (is_eq)
|
||||
q.push_front(mk_eq_constraint(new_ctx, new_a, new_b, new_jst));
|
||||
push_front(q, mk_eq_constraint(new_ctx, new_a, new_b, new_jst));
|
||||
else
|
||||
q.push_front(mk_convertible_constraint(new_ctx, new_a, new_b, new_jst));
|
||||
push_front(q, mk_convertible_constraint(new_ctx, new_a, new_b, new_jst));
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -349,13 +354,18 @@ class elaborator::imp {
|
|||
/**
|
||||
\brief Assign \c v to \c m with justification \c tr in the current state.
|
||||
*/
|
||||
void assign(expr const & m, expr const & v, unification_constraint const & c) {
|
||||
bool assign(expr const & m, expr const & v, unification_constraint const & c, bool is_lhs) {
|
||||
lean_assert(is_metavar(m));
|
||||
if (instantiate_metavars(!is_lhs, v, c)) // make sure v does not have assigned metavars
|
||||
return true;
|
||||
reset_quota();
|
||||
context const & ctx = get_context(c);
|
||||
justification jst(new assignment_justification(c));
|
||||
metavar_env const & menv = m_state.m_menv;
|
||||
menv->assign(m, v, jst);
|
||||
if (!menv->assign(m, v, jst)) {
|
||||
m_conflict = justification(new unification_failure_justification(c));
|
||||
return false;
|
||||
}
|
||||
if (menv->has_type(m)) {
|
||||
buffer<unification_constraint> ucs;
|
||||
expr tv = m_type_inferer(v, ctx, menv, ucs);
|
||||
|
|
@ -364,6 +374,7 @@ class elaborator::imp {
|
|||
justification new_jst(new typeof_mvar_justification(ctx, m, menv->get_type(m), tv, jst));
|
||||
push_front(mk_convertible_constraint(ctx, tv, menv->get_type(m), new_jst));
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool process(unification_constraint const & c) {
|
||||
|
|
@ -414,8 +425,7 @@ class elaborator::imp {
|
|||
// or b is a proposition.
|
||||
// It is important to handle propositions since we don't want to normalize them.
|
||||
// The normalization process destroys the structure of the proposition.
|
||||
assign(a, b, c);
|
||||
return Processed;
|
||||
return assign(a, b, c, is_lhs) ? Processed : Failed;
|
||||
}
|
||||
} else {
|
||||
local_entry const & me = head(metavar_lctx(a));
|
||||
|
|
@ -742,7 +752,10 @@ class elaborator::imp {
|
|||
unsigned num_a = num_args(a);
|
||||
buffer<expr> arg_types;
|
||||
buffer<unification_constraint> ucs;
|
||||
context h_ctx = ctx; // context for new fresh metavariables used in the imitation step
|
||||
// h_ctx is the context for new fresh metavariables used in the imitation step
|
||||
// Since the imitation is going to be assigned to f_a, its context must
|
||||
// be the context of f_a + the imitation arguments
|
||||
context h_ctx = menv->get_context(metavar_name(f_a));
|
||||
for (unsigned i = 1; i < num_a; i++) {
|
||||
arg_types.push_back(m_type_inferer(arg(a, i), ctx, menv, ucs));
|
||||
for (auto uc : ucs)
|
||||
|
|
@ -821,7 +834,9 @@ class elaborator::imp {
|
|||
for further details.
|
||||
*/
|
||||
bool process_meta_app(expr const & a, expr const & b, bool is_lhs, unification_constraint const & c, bool flex_flex = false) {
|
||||
if (is_meta_app(a) && (flex_flex || !is_meta_app(b))) {
|
||||
if (is_meta_app(a) &&
|
||||
(flex_flex || !is_meta_app(b)) &&
|
||||
(is_eq(c) || (is_lhs && !is_actual_upper(b)) || (!is_lhs && !is_actual_lower(b)))) {
|
||||
std::unique_ptr<generic_case_split> new_cs(new generic_case_split(c, m_state));
|
||||
process_meta_app_core(new_cs, a, b, is_lhs, c);
|
||||
if (flex_flex && is_meta_app(b))
|
||||
|
|
@ -853,7 +868,8 @@ class elaborator::imp {
|
|||
Case 2) imitate b
|
||||
*/
|
||||
bool process_metavar_inst(expr const & a, expr const & b, bool is_lhs, unification_constraint const & c) {
|
||||
if (is_metavar_inst(a) && !is_metavar_inst(b) && !is_meta_app(b)) {
|
||||
if (is_metavar_inst(a) && !is_metavar_inst(b) && !is_meta_app(b) &&
|
||||
(is_eq(c) || (is_lhs && !is_actual_upper(b)) || (!is_lhs && !is_actual_lower(b)))) {
|
||||
context const & ctx = get_context(c);
|
||||
local_context lctx = metavar_lctx(a);
|
||||
unsigned i = head(lctx).s();
|
||||
|
|
@ -963,7 +979,7 @@ class elaborator::imp {
|
|||
bool is_lower(unification_constraint const & c) {
|
||||
return
|
||||
is_convertible(c) &&
|
||||
is_metavar(convertible_to(c)) &&
|
||||
(is_metavar(convertible_to(c)) || is_meta_app(convertible_to(c))) &&
|
||||
(is_bool(convertible_from(c)) || is_type(convertible_from(c)));
|
||||
}
|
||||
|
||||
|
|
@ -1115,14 +1131,12 @@ class elaborator::imp {
|
|||
if (!is_type(b) && !is_meta(b) && is_metavar(a) && !is_assigned(a) && !has_local_context(a)) {
|
||||
// We can assign a <- b at this point IF b is not (Type lvl) or Metavariable
|
||||
lean_assert(!has_metavar(b, a));
|
||||
assign(a, b, c);
|
||||
return true;
|
||||
return assign(a, b, c, true);
|
||||
}
|
||||
if (!is_type(a) && !is_meta(a) && a != Bool && is_metavar(b) && !is_assigned(b) && !has_local_context(b)) {
|
||||
// We can assign b <- a at this point IF a is not (Type lvl) or Metavariable or Bool.
|
||||
lean_assert(!has_metavar(a, b));
|
||||
assign(b, a, c);
|
||||
return true;
|
||||
return assign(b, a, c, false);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -65,10 +65,10 @@ class type_inferer::imp {
|
|||
t = abst_body(t);
|
||||
} else if (has_metavar(t) && m_menv && m_uc) {
|
||||
// Create two fresh variables A and B,
|
||||
// and assign r == (Pi(x : A), B x)
|
||||
// and assign r == (Pi(x : A), B)
|
||||
expr A = m_menv->mk_metavar(ctx);
|
||||
expr B = m_menv->mk_metavar(ctx);
|
||||
expr p = mk_pi(g_x_name, A, B(Var(0)));
|
||||
expr B = m_menv->mk_metavar(extend(ctx, g_x_name, A));
|
||||
expr p = mk_pi(g_x_name, A, B);
|
||||
justification jst = mk_function_expected_justification(ctx, e);
|
||||
m_uc->push_back(mk_eq_constraint(ctx, t, p, jst));
|
||||
t = abst_body(p);
|
||||
|
|
|
|||
|
|
@ -71,8 +71,9 @@ static void tst2() {
|
|||
expr g = Const("g");
|
||||
expr h = Const("h");
|
||||
expr a = Const("a");
|
||||
expr m1 = menv->mk_metavar();
|
||||
expr m2 = menv->mk_metavar();
|
||||
expr T = Const("T");
|
||||
expr m1 = menv->mk_metavar(context({{"x", T}, {"y", T}}));
|
||||
expr m2 = menv->mk_metavar(context({{"x", T}, {"y", T}}));
|
||||
// move m1 to a different context, and store new metavariable + context in m11
|
||||
std::cout << "---------------------\n";
|
||||
expr m11 = add_inst(m1, 0, f(a, m2));
|
||||
|
|
@ -92,7 +93,7 @@ static void tst3() {
|
|||
expr a = Const("a");
|
||||
expr x = Const("x");
|
||||
expr T = Const("T");
|
||||
expr m1 = menv->mk_metavar();
|
||||
expr m1 = menv->mk_metavar(context({{"x", T}, {"y", T}, {"z", T}}));
|
||||
expr F = Fun({x, T}, f(m1, x));
|
||||
menv->assign(m1, h(Var(0), Var(2)));
|
||||
std::cout << instantiate(abst_body(F), g(a)) << "\n";
|
||||
|
|
@ -108,7 +109,8 @@ static void tst4() {
|
|||
expr g = Const("g");
|
||||
expr h = Const("h");
|
||||
expr a = Const("a");
|
||||
expr m1 = menv->mk_metavar();
|
||||
expr T = Const("T");
|
||||
expr m1 = menv->mk_metavar(context({{"x", T}, {"y", T}}));
|
||||
expr F = f(m1, Var(2));
|
||||
menv->assign(m1, h(Var(1)));
|
||||
std::cout << instantiate(F, {g(Var(0)), h(a)}) << "\n";
|
||||
|
|
@ -128,8 +130,9 @@ static void tst6() {
|
|||
expr g = Const("g");
|
||||
expr h = Const("h");
|
||||
metavar_env menv;
|
||||
expr m1 = menv->mk_metavar();
|
||||
expr m2 = menv->mk_metavar();
|
||||
expr T = Const("T");
|
||||
expr m1 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}}));
|
||||
expr m2 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}}));
|
||||
expr t = f(Var(0), Fun({x, N}, f(Var(1), x, Fun({y, N}, f(Var(2), x, y)))));
|
||||
expr r = instantiate(t, g(m1, m2));
|
||||
std::cout << r << std::endl;
|
||||
|
|
@ -147,7 +150,8 @@ static void tst7() {
|
|||
expr g = Const("g");
|
||||
expr a = Const("a");
|
||||
metavar_env menv;
|
||||
expr m1 = menv->mk_metavar();
|
||||
expr T = Const("T");
|
||||
expr m1 = menv->mk_metavar(context({{"x", T}}));
|
||||
expr t = f(m1, Var(0));
|
||||
expr r = instantiate(t, a);
|
||||
menv->assign(m1, g(Var(0)));
|
||||
|
|
@ -161,7 +165,8 @@ static void tst8() {
|
|||
expr g = Const("g");
|
||||
expr a = Const("a");
|
||||
metavar_env menv;
|
||||
expr m1 = menv->mk_metavar();
|
||||
expr T = Const("T");
|
||||
expr m1 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}}));
|
||||
expr t = f(m1, Var(0), Var(2));
|
||||
expr r = instantiate(t, a);
|
||||
menv->assign(m1, g(Var(0), Var(1)));
|
||||
|
|
@ -175,7 +180,8 @@ static void tst9() {
|
|||
expr g = Const("g");
|
||||
expr a = Const("a");
|
||||
metavar_env menv;
|
||||
expr m1 = menv->mk_metavar();
|
||||
expr T = Const("T");
|
||||
expr m1 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}}));
|
||||
expr t = f(m1, Var(1), Var(2));
|
||||
expr r = lift_free_vars(t, 1, 2);
|
||||
std::cout << r << std::endl;
|
||||
|
|
@ -196,8 +202,9 @@ static void tst10() {
|
|||
expr g = Const("g");
|
||||
expr h = Const("h");
|
||||
metavar_env menv;
|
||||
expr m1 = menv->mk_metavar();
|
||||
expr m2 = menv->mk_metavar();
|
||||
expr T = Const("T");
|
||||
expr m1 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}}));
|
||||
expr m2 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}}));
|
||||
expr t = f(Var(0), Fun({x, N}, f(Var(1), Var(2), x, Fun({y, N}, f(Var(2), x, y)))));
|
||||
expr r = instantiate(t, g(m1));
|
||||
std::cout << r << std::endl;
|
||||
|
|
@ -224,7 +231,8 @@ static void tst11() {
|
|||
|
||||
static void tst12() {
|
||||
metavar_env menv;
|
||||
expr m = menv->mk_metavar();
|
||||
expr T = Const("T");
|
||||
expr m = menv->mk_metavar(context({{"x1", T}, {"x2", T}}));
|
||||
expr f = Const("f");
|
||||
std::cout << instantiate(f(m), {Var(0), Var(1)}) << "\n";
|
||||
std::cout << instantiate(f(m), {Var(1), Var(0)}) << "\n";
|
||||
|
|
@ -233,7 +241,8 @@ static void tst12() {
|
|||
static void tst13() {
|
||||
environment env;
|
||||
metavar_env menv;
|
||||
expr m = menv->mk_metavar();
|
||||
expr T = Const("T");
|
||||
expr m = menv->mk_metavar(context({{"x", T}}));
|
||||
env->add_var("N", Type());
|
||||
expr N = Const("N");
|
||||
env->add_var("f", N >> N);
|
||||
|
|
@ -253,8 +262,9 @@ static void tst13() {
|
|||
static void tst14() {
|
||||
environment env;
|
||||
metavar_env menv;
|
||||
expr m1 = menv->mk_metavar();
|
||||
expr m2 = menv->mk_metavar();
|
||||
expr T = Const("T");
|
||||
expr m1 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}, {"x5", T}}));
|
||||
expr m2 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}, {"x5", T}}));
|
||||
expr N = Const("N");
|
||||
expr f = Const("f");
|
||||
expr h = Const("h");
|
||||
|
|
@ -288,7 +298,8 @@ static void tst15() {
|
|||
environment env;
|
||||
metavar_env menv;
|
||||
normalizer norm(env);
|
||||
expr m1 = menv->mk_metavar();
|
||||
expr T = Const("T");
|
||||
expr m1 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}}));
|
||||
expr f = Const("f");
|
||||
expr x = Const("x");
|
||||
expr y = Const("y");
|
||||
|
|
@ -311,7 +322,8 @@ static void tst16() {
|
|||
normalizer norm(env);
|
||||
context ctx;
|
||||
ctx = extend(ctx, "w", Type());
|
||||
expr m1 = menv->mk_metavar();
|
||||
expr T = Const("T");
|
||||
expr m1 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}, {"x5", T}}));
|
||||
expr f = Const("f");
|
||||
expr x = Const("x");
|
||||
expr y = Const("y");
|
||||
|
|
@ -334,7 +346,8 @@ static void tst17() {
|
|||
ctx = extend(ctx, "w2", Type());
|
||||
ctx = extend(ctx, "w3", Type());
|
||||
ctx = extend(ctx, "w4", Type());
|
||||
expr m1 = menv->mk_metavar();
|
||||
expr T = Const("T");
|
||||
expr m1 = menv->mk_metavar(context({{"x1", T}, {"x2", T}, {"x3", T}, {"x4", T}}));
|
||||
expr f = Const("f");
|
||||
expr x = Const("x");
|
||||
expr y = Const("y");
|
||||
|
|
@ -379,7 +392,7 @@ static void tst18() {
|
|||
env->add_var("g", N >> N);
|
||||
env->add_var("h", N >> (N >> N));
|
||||
expr m1 = menv->mk_metavar(context({{"z", Type()}, {"f", N >> N}, {"y", Type()}}));
|
||||
expr m2 = menv->mk_metavar(context({{"z", Type()}, {"x", N}}));
|
||||
expr m2 = menv->mk_metavar(context({{"z", Type()}, {"x", N}, {"x1", N}}));
|
||||
expr F = Fun({z, Type()}, Fun({{f, N >> N}, {y, Type()}}, m1)(Fun({x, N}, g(z, x, m2)), N));
|
||||
std::cout << norm(F, ctx) << "\n";
|
||||
metavar_env menv2 = menv.copy();
|
||||
|
|
@ -400,10 +413,10 @@ static void tst19() {
|
|||
context ctx;
|
||||
ctx = extend(ctx, "w1", Type());
|
||||
ctx = extend(ctx, "w2", Type());
|
||||
expr m1 = menv->mk_metavar();
|
||||
expr x = Const("x");
|
||||
expr y = Const("y");
|
||||
expr N = Const("N");
|
||||
expr m1 = menv->mk_metavar(context({{"N", Type()}, {"x", N}, {"y", N}}));
|
||||
expr F = Fun({{N, Type()}, {x, N}, {y, N}}, m1);
|
||||
std::cout << norm(F) << "\n";
|
||||
std::cout << norm(F, ctx) << "\n";
|
||||
|
|
@ -418,13 +431,13 @@ static void tst20() {
|
|||
context ctx;
|
||||
ctx = extend(ctx, "w1", Type());
|
||||
ctx = extend(ctx, "w2", Type());
|
||||
expr m1 = menv->mk_metavar();
|
||||
expr x = Const("x");
|
||||
expr y = Const("y");
|
||||
expr z = Const("z");
|
||||
expr N = Const("N");
|
||||
expr a = Const("a");
|
||||
expr b = Const("b");
|
||||
expr m1 = menv->mk_metavar(context({{"x", N}, {"y", N}, {"z", N}, {"x", N}, {"y", N}}));
|
||||
env->add_var("N", Type());
|
||||
env->add_var("a", N);
|
||||
env->add_var("b", N);
|
||||
|
|
@ -588,10 +601,10 @@ static void tst27() {
|
|||
env->add_var("a", Int);
|
||||
env->add_var("b", Real);
|
||||
expr T1 = menv->mk_metavar();
|
||||
expr T2 = menv->mk_metavar();
|
||||
expr A1 = menv->mk_metavar();
|
||||
expr m1 = menv->mk_metavar();
|
||||
expr m2 = menv->mk_metavar();
|
||||
expr T2 = menv->mk_metavar(context({{"x", T1}}));
|
||||
expr A1 = menv->mk_metavar(context({{"x", T1}, {"y", T2}}));
|
||||
expr m1 = menv->mk_metavar(context({{"x", T1}, {"y", T2}}));
|
||||
expr m2 = menv->mk_metavar(context({{"x", T1}, {"y", T2}}));
|
||||
expr F = Fun({{x, T1}, {y, T2}}, f(A1, x, y))(m1(a), m2(b));
|
||||
std::cout << F << "\n";
|
||||
std::cout << checker.infer_type(F, context(), menv, up) << "\n";
|
||||
|
|
|
|||
|
|
@ -18,7 +18,7 @@ Failed to solve
|
|||
Assignment
|
||||
⊢ ℕ ≺ ?M::0
|
||||
Substitution
|
||||
⊢ (?M::5[inst:0 (10)]) 10 ≺ ?M::0
|
||||
⊢ ?M::5[inst:0 (10)] ≺ ?M::0
|
||||
(line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
|
||||
f::explicit
|
||||
with arguments:
|
||||
|
|
@ -26,13 +26,11 @@ Failed to solve
|
|||
?M::1 10
|
||||
⊤
|
||||
Assignment
|
||||
x : ℕ ⊢ λ x : ℕ, ℕ ≈ ?M::5
|
||||
x : ℕ ⊢ ℕ ≈ ?M::5
|
||||
Destruct/Decompose
|
||||
x : ℕ ⊢ ℕ ≈ ?M::5 x
|
||||
Destruct/Decompose
|
||||
⊢ ℕ → ℕ ≈ Π x : ?M::4, ?M::5 x
|
||||
⊢ ℕ → ℕ ≈ Π x : ?M::4, ?M::5
|
||||
Substitution
|
||||
⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 x
|
||||
⊢ ?M::3 ≈ Π x : ?M::4, ?M::5
|
||||
Function expected at
|
||||
?M::1 10
|
||||
Assignment
|
||||
|
|
@ -54,7 +52,7 @@ Failed to solve
|
|||
Assignment
|
||||
⊢ ℤ ≺ ?M::0
|
||||
Substitution
|
||||
⊢ (?M::5[inst:0 (10)]) 10 ≺ ?M::0
|
||||
⊢ ?M::5[inst:0 (10)] ≺ ?M::0
|
||||
(line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
|
||||
f::explicit
|
||||
with arguments:
|
||||
|
|
@ -62,13 +60,11 @@ Failed to solve
|
|||
?M::1 10
|
||||
⊤
|
||||
Assignment
|
||||
_ : ℕ ⊢ λ x : ℕ, ℤ ≈ ?M::5
|
||||
_ : ℕ ⊢ ℤ ≈ ?M::5
|
||||
Destruct/Decompose
|
||||
_ : ℕ ⊢ ℤ ≈ ?M::5 _
|
||||
Destruct/Decompose
|
||||
⊢ ℕ → ℤ ≈ Π x : ?M::4, ?M::5 x
|
||||
⊢ ℕ → ℤ ≈ Π x : ?M::4, ?M::5
|
||||
Substitution
|
||||
⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 x
|
||||
⊢ ?M::3 ≈ Π x : ?M::4, ?M::5
|
||||
Function expected at
|
||||
?M::1 10
|
||||
Assignment
|
||||
|
|
@ -90,7 +86,7 @@ Failed to solve
|
|||
Assignment
|
||||
⊢ ℝ ≺ ?M::0
|
||||
Substitution
|
||||
⊢ (?M::5[inst:0 (10)]) 10 ≺ ?M::0
|
||||
⊢ ?M::5[inst:0 (10)] ≺ ?M::0
|
||||
(line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
|
||||
f::explicit
|
||||
with arguments:
|
||||
|
|
@ -98,13 +94,11 @@ Failed to solve
|
|||
?M::1 10
|
||||
⊤
|
||||
Assignment
|
||||
_ : ℕ ⊢ λ x : ℕ, ℝ ≈ ?M::5
|
||||
_ : ℕ ⊢ ℝ ≈ ?M::5
|
||||
Destruct/Decompose
|
||||
_ : ℕ ⊢ ℝ ≈ ?M::5 _
|
||||
Destruct/Decompose
|
||||
⊢ ℕ → ℝ ≈ Π x : ?M::4, ?M::5 x
|
||||
⊢ ℕ → ℝ ≈ Π x : ?M::4, ?M::5
|
||||
Substitution
|
||||
⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 x
|
||||
⊢ ?M::3 ≈ Π x : ?M::4, ?M::5
|
||||
Function expected at
|
||||
?M::1 10
|
||||
Assignment
|
||||
|
|
@ -117,7 +111,7 @@ Failed to solve
|
|||
Error (line: 7, pos: 8) unexpected metavariable occurrence
|
||||
Assumed: h
|
||||
Failed to solve
|
||||
x : ?M::0, A : Type ⊢ ?M::0[lift:0:2] ≺ A
|
||||
x : ?M::0, A : Type ⊢ ?M::0 ≺ A
|
||||
(line: 11: pos: 27) Type of argument 2 must be convertible to the expected type in the application of
|
||||
h
|
||||
with arguments:
|
||||
|
|
|
|||
|
|
@ -17,20 +17,18 @@ Failed to solve
|
|||
Substitution
|
||||
⊢ ℤ ≺ ?M::6
|
||||
Substitution
|
||||
⊢ (?M::5[inst:0 i]) i ≺ ?M::6
|
||||
⊢ ?M::5[inst:0 i] ≺ ?M::6
|
||||
Type of argument 1 must be convertible to the expected type in the application of
|
||||
?M::0
|
||||
with arguments:
|
||||
?M::1 i
|
||||
p
|
||||
Assignment
|
||||
x : ℤ ⊢ λ x : ℤ, ℤ ≈ ?M::5
|
||||
x : ℤ ⊢ ℤ ≈ ?M::5
|
||||
Destruct/Decompose
|
||||
x : ℤ ⊢ ℤ ≈ ?M::5 x
|
||||
Destruct/Decompose
|
||||
⊢ ℤ → ℤ ≈ Π x : ?M::4, ?M::5 x
|
||||
⊢ ℤ → ℤ ≈ Π x : ?M::4, ?M::5
|
||||
Substitution
|
||||
⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 x
|
||||
⊢ ?M::3 ≈ Π x : ?M::4, ?M::5
|
||||
Function expected at
|
||||
?M::1 i
|
||||
Assignment
|
||||
|
|
@ -42,9 +40,9 @@ Failed to solve
|
|||
Assignment
|
||||
⊢ ℕ ≈ ?M::6
|
||||
Destruct/Decompose
|
||||
⊢ ℕ → ℕ → ℕ ≈ Π x : ?M::6, ?M::7 x
|
||||
⊢ ℕ → ℕ → ℕ ≈ Π x : ?M::6, ?M::7
|
||||
Substitution
|
||||
⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 x
|
||||
⊢ ?M::2 ≈ Π x : ?M::6, ?M::7
|
||||
Function expected at
|
||||
?M::0 (?M::1 i) p
|
||||
Assignment
|
||||
|
|
@ -58,20 +56,18 @@ Failed to solve
|
|||
Substitution
|
||||
⊢ ℝ ≺ ?M::6
|
||||
Substitution
|
||||
⊢ (?M::5[inst:0 i]) i ≺ ?M::6
|
||||
⊢ ?M::5[inst:0 i] ≺ ?M::6
|
||||
Type of argument 1 must be convertible to the expected type in the application of
|
||||
?M::0
|
||||
with arguments:
|
||||
?M::1 i
|
||||
p
|
||||
Assignment
|
||||
_ : ℤ ⊢ λ x : ℤ, ℝ ≈ ?M::5
|
||||
_ : ℤ ⊢ ℝ ≈ ?M::5
|
||||
Destruct/Decompose
|
||||
_ : ℤ ⊢ ℝ ≈ ?M::5 _
|
||||
Destruct/Decompose
|
||||
⊢ ℤ → ℝ ≈ Π x : ?M::4, ?M::5 x
|
||||
⊢ ℤ → ℝ ≈ Π x : ?M::4, ?M::5
|
||||
Substitution
|
||||
⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 x
|
||||
⊢ ?M::3 ≈ Π x : ?M::4, ?M::5
|
||||
Function expected at
|
||||
?M::1 i
|
||||
Assignment
|
||||
|
|
@ -83,9 +79,9 @@ Failed to solve
|
|||
Assignment
|
||||
⊢ ℕ ≈ ?M::6
|
||||
Destruct/Decompose
|
||||
⊢ ℕ → ℕ → ℕ ≈ Π x : ?M::6, ?M::7 x
|
||||
⊢ ℕ → ℕ → ℕ ≈ Π x : ?M::6, ?M::7
|
||||
Substitution
|
||||
⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 x
|
||||
⊢ ?M::2 ≈ Π x : ?M::6, ?M::7
|
||||
Function expected at
|
||||
?M::0 (?M::1 i) p
|
||||
Assignment
|
||||
|
|
@ -106,19 +102,17 @@ Failed to solve
|
|||
Assignment
|
||||
⊢ ℤ ≈ ?M::8
|
||||
Destruct/Decompose
|
||||
⊢ ℤ → ℤ ≈ Π x : ?M::8, ?M::9 x
|
||||
⊢ ℤ → ℤ ≈ Π x : ?M::8, ?M::9
|
||||
Substitution
|
||||
⊢ (?M::7[inst:0 (?M::1 i)]) (?M::1 i) ≈ Π x : ?M::8, ?M::9 x
|
||||
⊢ ?M::7[inst:0 (?M::1 i)] ≈ Π x : ?M::8, ?M::9
|
||||
Function expected at
|
||||
?M::0 (?M::1 i) p
|
||||
Assignment
|
||||
_ : ℤ ⊢ λ x : ℤ, ℤ → ℤ ≈ ?M::7
|
||||
_ : ℤ ⊢ ℤ → ℤ ≈ ?M::7
|
||||
Destruct/Decompose
|
||||
_ : ℤ ⊢ ℤ → ℤ ≈ ?M::7 _
|
||||
Destruct/Decompose
|
||||
⊢ ℤ → ℤ → ℤ ≈ Π x : ?M::6, ?M::7 x
|
||||
⊢ ℤ → ℤ → ℤ ≈ Π x : ?M::6, ?M::7
|
||||
Substitution
|
||||
⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 x
|
||||
⊢ ?M::2 ≈ Π x : ?M::6, ?M::7
|
||||
Function expected at
|
||||
?M::0 (?M::1 i) p
|
||||
Assignment
|
||||
|
|
@ -139,19 +133,17 @@ Failed to solve
|
|||
Assignment
|
||||
⊢ ℝ ≈ ?M::8
|
||||
Destruct/Decompose
|
||||
⊢ ℝ → ℝ ≈ Π x : ?M::8, ?M::9 x
|
||||
⊢ ℝ → ℝ ≈ Π x : ?M::8, ?M::9
|
||||
Substitution
|
||||
⊢ (?M::7[inst:0 (?M::1 i)]) (?M::1 i) ≈ Π x : ?M::8, ?M::9 x
|
||||
⊢ ?M::7[inst:0 (?M::1 i)] ≈ Π x : ?M::8, ?M::9
|
||||
Function expected at
|
||||
?M::0 (?M::1 i) p
|
||||
Assignment
|
||||
_ : ℝ ⊢ λ x : ℝ, ℝ → ℝ ≈ ?M::7
|
||||
_ : ℝ ⊢ ℝ → ℝ ≈ ?M::7
|
||||
Destruct/Decompose
|
||||
_ : ℝ ⊢ ℝ → ℝ ≈ ?M::7 _
|
||||
Destruct/Decompose
|
||||
⊢ ℝ → ℝ → ℝ ≈ Π x : ?M::6, ?M::7 x
|
||||
⊢ ℝ → ℝ → ℝ ≈ Π x : ?M::6, ?M::7
|
||||
Substitution
|
||||
⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 x
|
||||
⊢ ?M::2 ≈ Π x : ?M::6, ?M::7
|
||||
Function expected at
|
||||
?M::0 (?M::1 i) p
|
||||
Assignment
|
||||
|
|
|
|||
|
|
@ -16,19 +16,17 @@ Failed to solve
|
|||
Assignment
|
||||
⊢ ℕ ≈ ?M::8
|
||||
Destruct/Decompose
|
||||
⊢ ℕ → ℕ ≈ Π x : ?M::8, ?M::9 x
|
||||
⊢ ℕ → ℕ ≈ Π x : ?M::8, ?M::9
|
||||
Substitution
|
||||
⊢ (?M::7[inst:0 (?M::1 1)]) (?M::1 1) ≈ Π x : ?M::8, ?M::9 x
|
||||
⊢ ?M::7[inst:0 (?M::1 1)] ≈ Π x : ?M::8, ?M::9
|
||||
(line: 1: pos: 10) Function expected at
|
||||
?M::0 (?M::1 1) ⊤
|
||||
Assignment
|
||||
_ : ℕ ⊢ λ x : ℕ, ℕ → ℕ ≈ ?M::7
|
||||
_ : ℕ ⊢ ℕ → ℕ ≈ ?M::7
|
||||
Destruct/Decompose
|
||||
_ : ℕ ⊢ ℕ → ℕ ≈ ?M::7 _
|
||||
Destruct/Decompose
|
||||
⊢ ℕ → ℕ → ℕ ≈ Π x : ?M::6, ?M::7 x
|
||||
⊢ ℕ → ℕ → ℕ ≈ Π x : ?M::6, ?M::7
|
||||
Substitution
|
||||
⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 x
|
||||
⊢ ?M::2 ≈ Π x : ?M::6, ?M::7
|
||||
(line: 1: pos: 10) Function expected at
|
||||
?M::0 (?M::1 1) ⊤
|
||||
Assignment
|
||||
|
|
@ -49,19 +47,17 @@ Failed to solve
|
|||
Assignment
|
||||
⊢ ℤ ≈ ?M::8
|
||||
Destruct/Decompose
|
||||
⊢ ℤ → ℤ ≈ Π x : ?M::8, ?M::9 x
|
||||
⊢ ℤ → ℤ ≈ Π x : ?M::8, ?M::9
|
||||
Substitution
|
||||
⊢ (?M::7[inst:0 (?M::1 1)]) (?M::1 1) ≈ Π x : ?M::8, ?M::9 x
|
||||
⊢ ?M::7[inst:0 (?M::1 1)] ≈ Π x : ?M::8, ?M::9
|
||||
(line: 1: pos: 10) Function expected at
|
||||
?M::0 (?M::1 1) ⊤
|
||||
Assignment
|
||||
_ : ℤ ⊢ λ x : ℤ, ℤ → ℤ ≈ ?M::7
|
||||
_ : ℤ ⊢ ℤ → ℤ ≈ ?M::7
|
||||
Destruct/Decompose
|
||||
_ : ℤ ⊢ ℤ → ℤ ≈ ?M::7 _
|
||||
Destruct/Decompose
|
||||
⊢ ℤ → ℤ → ℤ ≈ Π x : ?M::6, ?M::7 x
|
||||
⊢ ℤ → ℤ → ℤ ≈ Π x : ?M::6, ?M::7
|
||||
Substitution
|
||||
⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 x
|
||||
⊢ ?M::2 ≈ Π x : ?M::6, ?M::7
|
||||
(line: 1: pos: 10) Function expected at
|
||||
?M::0 (?M::1 1) ⊤
|
||||
Assignment
|
||||
|
|
@ -82,19 +78,17 @@ Failed to solve
|
|||
Assignment
|
||||
⊢ ℝ ≈ ?M::8
|
||||
Destruct/Decompose
|
||||
⊢ ℝ → ℝ ≈ Π x : ?M::8, ?M::9 x
|
||||
⊢ ℝ → ℝ ≈ Π x : ?M::8, ?M::9
|
||||
Substitution
|
||||
⊢ (?M::7[inst:0 (?M::1 1)]) (?M::1 1) ≈ Π x : ?M::8, ?M::9 x
|
||||
⊢ ?M::7[inst:0 (?M::1 1)] ≈ Π x : ?M::8, ?M::9
|
||||
(line: 1: pos: 10) Function expected at
|
||||
?M::0 (?M::1 1) ⊤
|
||||
Assignment
|
||||
_ : ℝ ⊢ λ x : ℝ, ℝ → ℝ ≈ ?M::7
|
||||
_ : ℝ ⊢ ℝ → ℝ ≈ ?M::7
|
||||
Destruct/Decompose
|
||||
_ : ℝ ⊢ ℝ → ℝ ≈ ?M::7 _
|
||||
Destruct/Decompose
|
||||
⊢ ℝ → ℝ → ℝ ≈ Π x : ?M::6, ?M::7 x
|
||||
⊢ ℝ → ℝ → ℝ ≈ Π x : ?M::6, ?M::7
|
||||
Substitution
|
||||
⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 x
|
||||
⊢ ?M::2 ≈ Π x : ?M::6, ?M::7
|
||||
(line: 1: pos: 10) Function expected at
|
||||
?M::0 (?M::1 1) ⊤
|
||||
Assignment
|
||||
|
|
|
|||
Loading…
Reference in a new issue