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

feat(kernel/type_checker): provide the metavar_env to instantiate, it will minimize the number of local_entries needed

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-14 15:13:56 -08:00
parent 4357c9196e
commit 3d30664611
2 changed files with 51 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/kernel/type_checker.cpp
View file

@ -42,6 +42,14 @@ class type_checker::imp {
return ::lean::lift_free_vars(e, d, m_menv.to_some_menv());
}
expr instantiate_with_closed(expr const & e, expr const & v) {
return ::lean::instantiate_with_closed(e, v, m_menv.to_some_menv());
}
expr instantiate(expr const & e, expr const & v) {
return ::lean::instantiate(e, v, m_menv.to_some_menv());
}
expr normalize(expr const & e, context const & ctx) {
return m_normalizer(e, ctx);
}
@ -158,9 +166,9 @@ class type_checker::imp {
if (closed(abst_body(f_t)))
f_t = abst_body(f_t);
else if (closed(c))
f_t = instantiate_with_closed(abst_body(f_t), c); // TODO(Leo): m_menv.to_some_menv());
f_t = instantiate_with_closed(abst_body(f_t), c);
else
f_t = instantiate(abst_body(f_t), c); // TODO(Leo): m_menv.to_some_menv());
f_t = instantiate(abst_body(f_t), c);
i++;
if (i == num)
return save_result(e, f_t, shared);
@ -212,9 +220,7 @@ class type_checker::imp {
{
cache::mk_scope sc(m_cache);
expr t = infer_type_core(let_body(e), extend(ctx, let_name(e), lt, let_value(e)));
return save_result(e,
instantiate(t, let_value(e)), // TODO(Leo): m_menv.to_some_menv()),
shared);
return save_result(e, instantiate(t, let_value(e)), shared);
}
}
case expr_kind::Value: {

43
tests/lean/elab1.lean.expected.out
View file

@ -130,10 +130,47 @@ A : Type, B : Type, a : ?M::0, b : ?M::1, C : Type ⊢ ?M::0[lift:0:3] ≺ C
Assumed: b
Assumed: H
Failed to solve
⊢ if ?M::0 ?M::1 ⊤ ≺ b
⊢ if ?M::0 (if (if ?M::3 (if a ⊥ ⊤) ⊤) ⊥ ⊤) ⊤ ≺ b
Normalize
⊢ ?M::0 ⇒ ?M::1 ≺ b
(line: 20: pos: 18) Type of definition 't1' must be convertible to expected type.
⊢ if ?M::0 (?M::3 ∧ a) ⊤ ≺ b
Substitution
⊢ if ?M::0 ?M::1 ⊤ ≺ b
Normalize
⊢ ?M::0 ⇒ ?M::1 ≺ b
(line: 20: pos: 18) Type of definition 't1' must be convertible to expected type.
Assignment
H1 : ?M::2 ⊢ ?M::3 ∧ a ≺ ?M::1
Substitution
H1 : ?M::2 ⊢ ?M::3 ∧ ?M::4 ≺ ?M::1
Destruct/Decompose
⊢ Π H1 : ?M::2, ?M::3 ∧ ?M::4 ≺ Π _ : ?M::0, ?M::1
(line: 20: pos: 18) Type of argument 3 must be convertible to the expected type in the application of
Discharge::explicit
with arguments:
?M::0
?M::1
λ H1 : ?M::2, Conj H1 (Conjunct1 H)
Assignment
H1 : ?M::2 ⊢ a ≺ ?M::4
Substitution
H1 : ?M::2 ⊢ ?M::5 ≺ ?M::4
(line: 20: pos: 37) Type of argument 4 must be convertible to the expected type in the application of
Conj::explicit
with arguments:
?M::3
?M::4
H1
Conjunct1 H
Assignment
H1 : ?M::2 ⊢ a ≈ ?M::5
Destruct/Decompose
H1 : ?M::2 ⊢ a ∧ b ≺ ?M::5 ∧ ?M::6
(line: 20: pos: 45) Type of argument 3 must be convertible to the expected type in the application of
Conjunct1::explicit
with arguments:
?M::5
?M::6
H
Failed to solve
⊢ b ≈ a
Substitution