max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

dev(library/type_context): add process_assignment

Browse source
This commit is contained in:
Leonardo de Moura 2016-03-13 14:16:14 -07:00
parent 9ecd4a2c85
commit 5ba3086a3e
2 changed files with 300 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

290
src/library/type_context.cpp
View file

@ -7,6 +7,8 @@ Author: Leonardo de Moura
#include "util/flet.h"
#include "util/interrupt.h"
#include "kernel/instantiate.h"
#include "kernel/replace_fn.h"
#include "kernel/for_each_fn.h"
#include "library/idx_metavar.h"
#include "library/reducible.h"
#include "library/metavar_util.h"
@ -146,6 +148,11 @@ expr type_context::abstract_locals(expr const & e, unsigned num_locals, expr con
return e;
}
expr type_context::mk_fun(buffer<expr> const & locals, expr const & e) {
// TODO(Leo)
lean_unreachable();
}
/* ---------------------
Normalization
-------------------- */
@ -508,6 +515,7 @@ bool type_context::is_prop(expr const & e) {
void type_context::set_tmp_mode(unsigned next_uidx, unsigned next_midx) {
lean_assert(!m_tmp_mode);
m_tmp_mode = true;
m_tmp_mvar_lctx = m_lctx;
m_tmp_uassignment.resize(next_uidx, none_level());
m_tmp_eassignment.resize(next_midx, none_expr());
}
@ -763,6 +771,288 @@ bool type_context::is_def_eq_core(expr const & t, expr const & s) {
return false;
}
bool type_context::approximate() {
// TODO(Leo): add flag at type_context_cache to force approximated mode.
return m_tmp_mode;
}
/* If \c e is a let local-decl, then unfold it, otherwise return e. */
expr type_context::try_zeta(expr const & e) {
if (!is_local_decl_ref(e))
return e;
if (auto d = m_lctx.get_local_decl(e)) {
if (auto v = d->get_value())
return *v;
}
return e;
}
expr type_context::expand_let_decls(expr const & e) {
return replace(e, [&](expr const & e, unsigned) {
if (is_local_decl_ref(e)) {
if (auto d = m_lctx.get_local_decl(e)) {
if (auto v = d->get_value())
return some_expr(*v);
}
}
return none_expr();
});
}
/*
We declare metavariables with respect to a local context.
We use the notation (`?M@C`) to denote a metavariable `?M` that was defined at local context `C`.
Remark: for temporary metavariables, the variable m_tmp_mvar_lctx stores their context.
The following method process the unification constraint
?M@C a_1 ... a_n =?= t
We say the unification constraint is a pattern IFF
1) `a_1 ... a_n` are pairwise distinct local constants that are ​*not*​ references to let-decls.
2) `a_1 ... a_n` have ​*not*​ been defined in `C`
3) `t` only contains local constants in `C` and/or `{a_1, ..., a_n}`
4) For every metavariable `?M'@C'` occurring in `t`, `C'` is a subset of `C`
5) `?M` does not occur in `t`
Claim: we don't have to check local declaration definitions. That is,
if `t` contains a reference to `x : A := v`, we don't need to check `v`.
Reason: The reference to `x` is a local constant, and it must be in `C` (by 1 and 3).
If `x` is in `C`, then any metavariable occurring in `v` must have been defined in a strict subset of `C`.
So, condition 4 and 5 are satisfied.
If the conditions above have been satisfied, then the
solution for the unification constrain is
?M := fun a_1 ... a_n, t
Now, we consider some workarounds/approximations.
A1) Suppose `t` contains a reference to `x : A := v` and `x` is not in `C` (failed condition 3)
(precise) solution: unfold `x` in `t`.
A2) Suppose some `a_i` is in `C` (failed condition 2)
(approximated) solution (when approximate() predicate returns true) :
ignore condition and also use
?M := fun a_1 ... a_n, t
Here is an example where this approximation fails:
Given `C` containing `a : nat`, consider the following two constraints
?M@C a =?= a
?M@C b =?= a
If we use the approximation in the first constraint, we get
?M := fun x, x
when we apply this solution to the second one we get a failure.
A3) `a_1 ... a_n` are not pairwise distinct (failed condition 1).
We can approximate again, but the limitations are very similar to the previous one.
A4) `t` contains a metavariable `?M'@C'` where `C'` is not a subset of `C`.
(approximated) solution: restrict the context of `?M'`
If `?M'` is assigned, the workaround is precise, and we just unfold `?M'`.
Remark: we only implement the ?M' assigned case.
A5) If some `a_i` is not a local constant,
then we use first-order unification (if approximate() is true)
?M a_1 ... a_i a_{i+1} ... a_{i+k} =?= f b_1 ... b_k
reduces to
?M a_1 ... a_i =?= f
a_{i+1} =?= b_1
...
a_{i+k} =?= b_k
*/
bool type_context::process_assignment(expr const & m, expr const & v) {
buffer<expr> args;
expr const & mvar = get_app_args(m, args);
lean_assert(is_mvar(mvar));
optional<metavar_decl> mvar_decl;
if (!m_tmp_mode) {
mvar_decl = m_mctx.get_metavar_decl(mvar);
if (!mvar_decl) return false;
}
buffer<expr> locals;
bool use_fo = false; /* if true, we use first-order unification */
bool add_locals = true; /* while true we copy args to locals */
for (unsigned i = 0; i < args.size(); i++) {
expr arg = args[i];
/* try to instantiate */
if (is_meta(arg))
arg = instantiate(arg);
arg = try_zeta(arg); /* unfold let-constant if needed. */
args[i] = arg;
if (!is_local_decl_ref(arg)) {
/* m is of the form (?M ... t ...) where t is not a local constant. */
if (approximate()) {
/* workaround A5 */
use_fo = true;
add_locals = false;
} else {
return false;
}
} else {
if (std::any_of(locals.begin(), locals.end(),
[&](expr const & local) { return mlocal_name(local) == mlocal_name(arg); })) {
/* m is of the form (?M ... l ... l ...) where l is a local constant. */
if (approximate()) {
/* workaround A3 */
add_locals = false;
} else {
return false;
}
}
/* Make sure arg is not in the context of the metavariable mvar
The code is slightly different for tmp mode because the metavariables
do not store their local context. */
if (m_tmp_mode) {
if (m_tmp_mvar_lctx.get_local_decl(arg)) {
/* m is of the form (?M@C ... l ...) where l is a local constant in C */
if (!approximate())
return false;
}
} else {
if (mvar_decl->get_context().contains(mlocal_name(arg))) {
/* m is of the form (?M@C ... l ...) where l is a local constant in C. */
if (!approximate())
return false;
}
}
}
if (add_locals)
locals.push_back(arg);
}
expr new_v = instantiate(v); /* enforce A4 */
if (use_fo) {
/* Use first-order unification.
Workaround A5. */
buffer<expr> new_v_args;
expr const & new_v_fn = get_app_args(new_v, new_v_args);
if (args.size() < new_v_args.size())
return false;
expr new_m = mk_app(mvar, args.size() - new_v_args.size(), args.data());
if (!is_def_eq_core(new_m, new_v_fn))
return false;
unsigned i = args.size() - new_v_args.size();
unsigned j = 0;
for (; j < new_v_args.size(); i++, j++) {
if (!is_def_eq_core(args[i], new_v_args[j]))
return false;
}
return true;
}
while (true) {
/* We use a loop here to implement workaround A1.
If new_v has a "bad" let local decl, we expand it and try again. */
bool ok = true;
bool bad_let_refs = false;
for_each(new_v, [&](expr const & e, unsigned) {
if (!ok)
return false; // stop search
if (is_mvar(e)) {
if (mvar == e) {
/* mvar occurs in v */
ok = false;
return false;
}
if (!m_tmp_mode) {
/* Recall that in tmp_mode all metavariables have the same local context.
So, we don't need to check anything.
In regular mode, we need to check condition 4
For every metavariable `?M'@C'` occurring in `t`, `C'` is a subset of `C`
*/
optional<metavar_decl> const & e_decl = m_mctx.get_metavar_decl(e);
if (!e_decl || e_decl->get_context().is_subset_of(mvar_decl->get_context())) {
ok = false;
return false;
}
}
return false;
} else if (is_local_decl_ref(e)) {
bool in_ctx;
if (m_tmp_mode) {
in_ctx = static_cast<bool>(m_tmp_mvar_lctx.get_local_decl(e));
} else {
in_ctx = mvar_decl->get_context().contains(mlocal_name(e));
}
if (!in_ctx) {
if (m_lctx.get_local_decl(e)->get_value()) {
/* let-decl that is not in the metavar context
workaround A1 */
ok = false;
bad_let_refs = true;
return false;
}
if (std::all_of(locals.begin(), locals.end(), [&](expr const & a) {
return mlocal_name(a) != mlocal_name(e); })) {
ok = false;
return false;
}
}
return false;
}
return true;
});
if (ok) {
break;
} else if (bad_let_refs) {
new_v = instantiate(expand_let_decls(new_v));
} else {
return false;
}
}
if (args.empty()) {
/* easy case */
} else if (args.size() == locals.size()) {
new_v = mk_fun(locals, new_v);
} else {
/*
This case is imprecise since it is not a higher order pattern.
That the term \c m is of the form (?M t_1 ... t_n) and the t_i's are not pairwise
distinct local constants.
*/
tmp_locals new_ls(*this);
expr mvar_type = infer(mvar);
for (unsigned i = 0; i < args.size(); i++) {
mvar_type = relaxed_whnf(mvar_type);
if (!is_pi(mvar_type))
return false;
lean_assert(i <= locals.size());
if (i == locals.size()) {
expr new_l = new_ls.push_local(binding_name(mvar_type), binding_domain(mvar_type));
locals.push_back(new_l);
}
lean_assert(i < locals.size());
mvar_type = ::lean::instantiate(binding_body(mvar_type), locals[i]);
}
lean_assert(locals.size() == args.size());
new_v = mk_fun(locals, new_v);
}
/* check types */
try {
expr t1 = infer(mvar);
expr t2 = infer(new_v);
if (!is_def_eq_core(t1, t2))
return false;
} catch (exception &) {
return false;
}
assign(mvar, new_v);
return true;
}
bool type_context::is_def_eq_binding(expr e1, expr e2) {
lean_assert(e1.kind() == e2.kind());
lean_assert(is_binding(e1));

10
src/library/type_context.h
View file

@ -125,6 +125,9 @@ class type_context : public abstract_type_context {
as opaque constants, and temporary metavariables (idx_metavar) are treated as metavariables,
and their assignment is stored at m_tmp_eassignment and m_tmp_uassignment. */
bool m_tmp_mode;
/* m_tmp_mvar_local_context contains m_lctx when tmp mode is activated.
This is the context for all temporary meta-variables. */
local_context m_tmp_mvar_lctx;
/* m_tmp_eassignment and m_tmp_uassignment store assignment for temporary/idx metavars
These assignments are only used during type class resolution and matching operations. */
@ -161,6 +164,8 @@ public:
virtual void pop_local() override;
virtual expr abstract_locals(expr const & e, unsigned num_locals, expr const * locals) override;
expr mk_fun(buffer<expr> const & locals, expr const & e);
/* Add a let-decl (aka local definition) to the local context */
expr push_let(name const & ppn, expr const & type, expr const & value) {
return m_lctx.mk_local_decl(ppn, type, value);
@ -268,6 +273,11 @@ private:
void commit() { m_owner.commit_scope(); m_keep = true; }
};
bool approximate();
expr try_zeta(expr const & e);
expr expand_let_decls(expr const & e);
bool process_assignment(expr const & m, expr const & v);
optional<declaration> is_delta(expr const & e);
bool is_def_eq(levels const & ls1, levels const & ls2);