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

fix(frontends/lean/elaborator): support for local instances

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-04 18:37:49 -07:00
parent 6ea7bb3ea4
commit 99fb6431a6
2 changed files with 42 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

35
src/frontends/lean/elaborator.cpp
View file

@ -140,22 +140,17 @@ class elaborator {
substitution m_subst; substitution m_subst;
justification m_jst; justification m_jst;
class_elaborator(elaborator & elab, expr const & mvar, expr const & mvar_type, list<name> const & instances, class_elaborator(elaborator & elab, expr const & mvar, expr const & mvar_type,
list<expr> const & local_insts, list<name> const & instances,
context const & ctx, substitution const & s, justification const & j): context const & ctx, substitution const & s, justification const & j):
m_elab(elab), m_mvar(mvar), m_mvar_type(mvar_type), m_instances(instances), m_ctx(ctx), m_subst(s), m_jst(j) { m_elab(elab), m_mvar(mvar), m_mvar_type(mvar_type), m_local_instances(local_insts), m_instances(instances),
if (elab.m_use_local_instances) m_ctx(ctx), m_subst(s), m_jst(j) {
m_local_instances = ctx;
} }
virtual optional<constraints> next() { virtual optional<constraints> next() {
while (!empty(m_local_instances)) { while (!empty(m_local_instances)) {
expr inst = head(m_local_instances); expr inst = head(m_local_instances);
m_local_instances = tail(m_local_instances); m_local_instances = tail(m_local_instances);
if (!is_local(inst))
continue;
expr inst_type = mlocal_type(inst);
if (!is_constant(get_app_fn(inst_type)) || const_name(get_app_fn(inst_type)) != const_name(get_app_fn(m_mvar_type)))
continue;
constraints cs(mk_eq_cnstr(m_mvar, inst, m_jst)); constraints cs(mk_eq_cnstr(m_mvar, inst, m_jst));
return optional<constraints>(cs); return optional<constraints>(cs);
} }
@ -399,13 +394,29 @@ public:
context ctx = m_ctx; context ctx = m_ctx;
justification j = mk_justification("failed to apply class instances", some_expr(m)); justification j = mk_justification("failed to apply class instances", some_expr(m));
auto choice_fn = [=](expr const & mvar, expr const & mvar_type, substitution const & s, name_generator const & /* ngen */) { auto choice_fn = [=](expr const & mvar, expr const & mvar_type, substitution const & s, name_generator const & /* ngen */) {
if (!is_constant(get_app_fn(mvar_type)))
return lazy_list<constraints>(constraints());
list<expr> local_insts;
if (m_use_local_instances) {
buffer<expr> buffer;
for (auto const & l : ctx) {
if (!is_local(l))
continue;
expr inst_type = mlocal_type(l);
if (!is_constant(get_app_fn(inst_type)) ||
const_name(get_app_fn(inst_type)) != const_name(get_app_fn(mvar_type)))
continue;
buffer.push_back(l);
}
local_insts = to_list(buffer.begin(), buffer.end());
}
auto insts = get_class_instances(mvar_type); auto insts = get_class_instances(mvar_type);
if (empty(insts)) if (empty(insts) && empty(local_insts))
return lazy_list<constraints>(constraints()); return lazy_list<constraints>(constraints());
else else
return choose(std::make_shared<class_elaborator>(*this, mvar, mvar_type, insts, ctx, s, j)); return choose(std::make_shared<class_elaborator>(*this, mvar, mvar_type, local_insts, insts, ctx, s, j));
}; };
add_cnstr(mk_choice_cnstr(m, choice_fn, false, j)); add_cnstr(mk_choice_cnstr(m, choice_fn, true, j));
} }
return m; return m;
} }

19
tests/lean/run/class3.lean Normal file
View file

@ -0,0 +1,19 @@
import standard
using num
section
parameter {A : Type}
parameter {B : Type}
parameter Ha : inhabited A
parameter Hb : inhabited B
-- The section mechanism only includes parameters that are explicitly cited.
-- So, we use the 'including' expression to make explicit we want to use
-- Ha and Hb
theorem tst : inhabited (Bool × A × B)
:= including Ha Hb, _
end
(*
print(get_env():find("tst"):value())
*)