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

fix(library/unifier): make sure the imitation step is type correct, fix ensure_sufficient_args

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-07 14:22:39 -07:00
parent 88ef5d68f9
commit 9e6c5695be
5 changed files with 97 additions and 52 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/kernel/type_checker.cpp
View file

@ -177,8 +177,10 @@ justification type_checker::mk_macro_jst(expr const & e) {
void type_checker::check_level(level const & l, expr const & s) {
if (auto n1 = get_undef_global(l, m_env))
throw_kernel_exception(m_env, sstream() << "invalid reference to undefined global universe level '" << *n1 << "'", s);
if (auto n2 = get_undef_param(l, m_params))
throw_kernel_exception(m_env, sstream() << "invalid reference to undefined universe level parameter '" << *n2 << "'", s);
if (m_params) {
if (auto n2 = get_undef_param(l, *m_params))
throw_kernel_exception(m_env, sstream() << "invalid reference to undefined universe level parameter '" << *n2 << "'", s);
}
}
app_delayed_justification::app_delayed_justification(expr const & e, expr const & arg, expr const & f_type, expr const & a_type):
@ -374,12 +376,20 @@ expr type_checker::infer(expr const & e, buffer<constraint> & new_cnstrs) {
expr type_checker::check(expr const & e, level_param_names const & ps) {
scope mk_scope(*this);
flet<level_param_names> updt(m_params, ps);
flet<level_param_names const *> updt(m_params, &ps);
expr r = infer_type_core(e, false);
mk_scope.keep();
return r;
}
expr type_checker::check(expr const & e, buffer<constraint> & new_cnstrs) {
scope mk_scope(*this);
unsigned cs_qhead = m_cs.size();
expr r = infer_type_core(e, false);
copy_constraints(cs_qhead, new_cnstrs);
return r;
}
expr type_checker::ensure_sort(expr const & e, expr const & s) {
scope mk_scope(*this);
expr r = ensure_sort_core(e, s);
@ -487,7 +497,7 @@ unsigned type_checker::num_scopes() const {
type_checker::type_checker(environment const & env, name_generator const & g, std::unique_ptr<converter> && conv, bool memoize):
m_env(env), m_gen(g), m_conv(std::move(conv)), m_tc_ctx(*this),
m_memoize(memoize) {
m_memoize(memoize), m_params(nullptr) {
m_cs_qhead = 0;
}

3
src/kernel/type_checker.h
View file

@ -82,7 +82,7 @@ class type_checker {
type_checker_context m_tc_ctx;
bool m_memoize;
// temp flag
level_param_names m_params;
level_param_names const * m_params;
buffer<constraint> m_cs; // temporary cache of constraints
unsigned m_cs_qhead;
buffer<std::pair<unsigned, unsigned>> m_trail;
@ -145,6 +145,7 @@ public:
constraint handler can be solved.
*/
expr check(expr const & t, level_param_names const & ps = level_param_names());
expr check(expr const & t, buffer<constraint> & new_cnstrs);
/** \brief Return true iff t is definitionally equal to s. */
bool is_def_eq(expr const & t, expr const & s);
bool is_def_eq(expr const & t, expr const & s, justification const & j);

95
src/library/unifier.cpp
View file

@ -1164,30 +1164,21 @@ struct unifier_fn {
}
/** \see ensure_sufficient_args */
optional<expr> ensure_sufficient_args_core(expr mtype, unsigned i, buffer<expr> const & margs, bool relax) {
expr ensure_sufficient_args_core(expr mtype, unsigned i, buffer<expr> const & margs, bool relax) {
if (i == margs.size())
return some_expr(mtype);
return mtype;
mtype = m_tc[relax]->ensure_pi(mtype);
try {
if (!m_tc[relax]->is_def_eq(binding_domain(mtype), m_tc[relax]->infer(margs[i])))
return none_expr();
} catch (kernel_exception &) {
return none_expr();
}
expr local = mk_local_for(mtype);
expr body = instantiate(binding_body(mtype), local);
auto new_body = ensure_sufficient_args_core(body, i+1, margs, relax);
if (!new_body)
return none_expr();
return some_expr(Pi(local, *new_body));
return Pi(local, ensure_sufficient_args_core(body, i+1, margs, relax));
}
/**
\brief Make sure mtype is a Pi of size at least margs.size().
If it is not, we use ensure_pi and (potentially) add new constaints to enforce it.
*/
optional<expr> ensure_sufficient_args(expr const & mtype, buffer<expr> const & margs, buffer<constraint> & cs,
justification const & j, bool relax) {
expr ensure_sufficient_args(expr const & mtype, buffer<expr> const & margs, buffer<constraint> & cs,
justification const & j, bool relax) {
expr t = mtype;
unsigned num = 0;
while (is_pi(t)) {
@ -1195,13 +1186,11 @@ struct unifier_fn {
t = binding_body(t);
}
if (num == margs.size())
return some_expr(mtype);;
return mtype;
lean_assert(!m_tc[relax]->next_cnstr()); // make sure there are no pending constraints
// We must create a scope to make sure no constraints "leak" into the current state.
type_checker::scope scope(*m_tc[relax]);
auto new_mtype = ensure_sufficient_args_core(mtype, 0, margs, relax);
if (!new_mtype)
return none_expr();
while (auto c = m_tc[relax]->next_cnstr())
cs.push_back(update_justification(*c, mk_composite1(c->get_justification(), j)));
return new_mtype;
@ -1240,6 +1229,22 @@ struct unifier_fn {
return v;
}
/** \brief Check if term \c e (produced by an imitation step) is
type correct, and store generated constraints in \c cs.
Include \c j in all generated constraints */
bool check_imitation(expr const & e, justification const & j, bool relax, buffer<constraint> & cs) {
try {
buffer<constraint> aux;
m_tc[relax]->check(e, aux);
for (auto c : aux) {
cs.push_back(update_justification(c, mk_composite1(j, c.get_justification())));
}
return true;
} catch (exception&) {
return false;
}
}
/**
\brief Given
m := a metavariable ?m
@ -1265,9 +1270,7 @@ struct unifier_fn {
lean_assert(is_constant(f) || is_var(f));
buffer<constraint> cs;
expr mtype = mlocal_type(m);
auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j, relax);
if (!new_mtype) return;
mtype = *new_mtype;
mtype = ensure_sufficient_args(mtype, margs, cs, j, relax);
buffer<expr> rargs;
get_app_args(rhs, rargs);
buffer<expr> sargs;
@ -1282,8 +1285,10 @@ struct unifier_fn {
}
expr v = mk_app(f, sargs);
v = mk_lambda_for(mtype, v);
cs.push_back(mk_eq_cnstr(m, v, j, relax));
alts.push_back(to_list(cs.begin(), cs.end()));
if (check_imitation(v, j, relax, cs)) {
cs.push_back(mk_eq_cnstr(m, v, j, relax));
alts.push_back(to_list(cs.begin(), cs.end()));
}
}
/**
@ -1303,9 +1308,7 @@ struct unifier_fn {
lean_assert(is_binding(rhs));
buffer<constraint> cs;
expr mtype = mlocal_type(m);
auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j, relax);
if (!new_mtype) return;
mtype = *new_mtype;
mtype = ensure_sufficient_args(mtype, margs, cs, j, relax);
expr maux1 = mk_aux_metavar_for(m_ngen, mtype);
cs.push_back(mk_eq_cnstr(mk_app(maux1, margs), binding_domain(rhs), j, relax));
expr dontcare;
@ -1316,8 +1319,10 @@ struct unifier_fn {
cs.push_back(mk_eq_cnstr(mk_app(mk_app(maux2, margs), new_local), instantiate(binding_body(rhs), new_local), j, relax));
expr v = update_binding(rhs, mk_app_vars(maux1, margs.size()), mk_app_vars(maux2, margs.size() + 1));
v = mk_lambda_for(mtype, v);
cs.push_back(mk_eq_cnstr(m, v, j, relax));
alts.push_back(to_list(cs.begin(), cs.end()));
if (check_imitation(v, j, relax, cs)) {
cs.push_back(mk_eq_cnstr(m, v, j, relax));
alts.push_back(to_list(cs.begin(), cs.end()));
}
}
/**
@ -1353,9 +1358,7 @@ struct unifier_fn {
lean_assert(is_macro(rhs));
buffer<constraint> cs;
expr mtype = mlocal_type(m);
auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j, relax);
if (!new_mtype) return;
mtype = *new_mtype;
mtype = ensure_sufficient_args(mtype, margs, cs, j, relax);
// create an auxiliary metavariable for each macro argument
buffer<expr> sargs;
for (unsigned i = 0; i < macro_num_args(rhs); i++) {
@ -1365,8 +1368,10 @@ struct unifier_fn {
}
expr v = mk_macro(macro_def(rhs), sargs.size(), sargs.data());
v = mk_lambda_for(mtype, v);
cs.push_back(mk_eq_cnstr(m, v, j, relax));
alts.push_back(to_list(cs.begin(), cs.end()));
if (check_imitation(v, j, relax, cs)) {
cs.push_back(mk_eq_cnstr(m, v, j, relax));
alts.push_back(to_list(cs.begin(), cs.end()));
}
}
/**
@ -1389,15 +1394,14 @@ struct unifier_fn {
unsigned vidx = margs.size() - i - 1;
expr const & marg = margs[i];
buffer<constraint> cs;
if (auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j, relax)) {
// Remark: we should not use mk_eq_cnstr(marg, rhs, j) since is_def_eq may be able to reduce them.
// The unifier assumes the eq constraints are reduced.
if (m_tc[relax]->is_def_eq_types(marg, rhs, j, cs) &&
m_tc[relax]->is_def_eq(marg, rhs, j, cs)) {
expr v = mk_lambda_for(*new_mtype, mk_var(vidx));
cs.push_back(mk_eq_cnstr(m, v, j, relax));
alts.push_back(to_list(cs.begin(), cs.end()));
}
auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j, relax);
// Remark: we should not use mk_eq_cnstr(marg, rhs, j) since is_def_eq may be able to reduce them.
// The unifier assumes the eq constraints are reduced.
if (m_tc[relax]->is_def_eq_types(marg, rhs, j, cs) &&
m_tc[relax]->is_def_eq(marg, rhs, j, cs)) {
expr v = mk_lambda_for(new_mtype, mk_var(vidx));
cs.push_back(mk_eq_cnstr(m, v, j, relax));
alts.push_back(to_list(cs.begin(), cs.end()));
}
}
@ -1434,11 +1438,10 @@ struct unifier_fn {
} else if (is_local(marg) && is_local(rhs) && mlocal_name(marg) == mlocal_name(rhs)) {
// if the argument is local, and rhs is equal to it, then we also add a projection
buffer<constraint> cs;
if (auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j, relax)) {
expr v = mk_lambda_for(*new_mtype, mk_var(vidx));
cs.push_back(mk_eq_cnstr(m, v, j, relax));
alts.push_back(to_list(cs.begin(), cs.end()));
}
auto new_mtype = ensure_sufficient_args(mtype, margs, cs, j, relax);
expr v = mk_lambda_for(new_mtype, mk_var(vidx));
cs.push_back(mk_eq_cnstr(m, v, j, relax));
alts.push_back(to_list(cs.begin(), cs.end()));
}
}
}

31
tests/lean/run/trans.lean Normal file
View file

@ -0,0 +1,31 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import logic
definition transport {A : Type} {a b : A} {P : A → Type} (p : a = b) (H : P a) : P b
:= eq_rec H p
theorem transport_refl {A : Type} {a : A} {P : A → Type} (H : P a) : transport (refl a) H = H
:= refl H
opaque_hint (hiding transport)
theorem transport_proof_irrel {A : Type} {a b : A} {P : A → Type} (p1 p2 : a = b) (H : P a) : transport p1 H = transport p2 H
:= refl (transport p1 H)
theorem transport_eq {A : Type} {a : A} {P : A → Type} (p : a = a) (H : P a) : transport p H = H
:= calc transport p H = transport (refl a) H : transport_proof_irrel p (refl a) H
... = H : transport_refl H
theorem dcongr {A : Type} {B : A → Type} {a b : A} (f : Π x, B x) (p : a = b) : transport p (f a) = f b
:= have H1 : ∀ p1 : a = a, transport p1 (f a) = f a, from
assume p1 : a = a, transport_eq p1 (f a),
eq_rec H1 p p
theorem transport_trans {A : Type} {a b c : A} {P : A → Type} (p1 : a = b) (p2 : b = c) (H : P a) :
transport p1 (transport p2 H) = transport (trans p1 p2) H
:= have H1 : ∀ p, transport p1 (transport p H) = transport (trans p1 p) H, from
take p, calc transport p1 (transport p H) = transport p1 H : {transport_eq p H}
... = transport (trans p1 p) H : refl (transport p1 H),
eq_rec H1 p2 p2

2
tests/lua/unify4.lua
View file

@ -23,4 +23,4 @@ local l3 = mk_local("l3", "z", N)
local m = mk_metavar("m", mk_arrow(N, N, mk_metavar("m_type", mk_arrow(N, N, mk_sort(mk_meta_univ("u"))))(Var(1), Var(0))))
test_unify(env, m, m(l1, l1), f(f(a, l1), l1), 4)
print("-----------------")
test_unify(env, m, m(l1, l1), mk_lambda("z", Prop, f(l1, f(Var(0), a))), 2)
test_unify(env, m, m(l1, l1), mk_lambda("z", N, f(l1, f(Var(0), a))), 2)