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

fix(frontends/lean/pp): purify metavar_decl_ref's

Browse source 
The tests become too fragile if we don't purify them.
This commit is contained in:
Leonardo de Moura 2016-07-30 20:30:03 -07:00
parent 96ec2e5914
commit f72f9dd561
9 changed files with 33 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/frontends/lean/pp.cpp
View file

@ -193,7 +193,7 @@ static name extract_suggestion(name const & m) {
return r;
}
name pretty_fn::mk_metavar_name(name const & m) {
name pretty_fn::mk_metavar_name(name const & m, optional<name> const & prefix) {
if (auto it = m_purify_meta_table.find(m))
return *it;
if (has_embedded_suggestion(m)) {
@ -208,7 +208,11 @@ name pretty_fn::mk_metavar_name(name const & m) {
m_purify_meta_table.insert(m, r);
return r;
} else {
name new_m = m_meta_prefix.append_after(m_next_meta_idx);
name new_m;
if (prefix)
new_m = prefix->append_after(m_next_meta_idx);
else
new_m = m_meta_prefix.append_after(m_next_meta_idx);
m_next_meta_idx++;
m_purify_meta_table.insert(m, new_m);
return new_m;
@ -237,7 +241,9 @@ level pretty_fn::purify(level const & l) {
return replace(l, [&](level const & l) {
if (!has_meta(l))
return some_level(l);
if (is_meta(l) && !is_idx_metauniv(l) && !is_metavar_decl_ref(l))
if (is_metavar_decl_ref(l))
return some_level(mk_meta_univ(mk_metavar_name(meta_id(l), "l")));
if (is_meta(l) && !is_idx_metauniv(l))
return some_level(mk_meta_univ(mk_metavar_name(meta_id(l))));
return none_level();
});
@ -264,7 +270,9 @@ expr pretty_fn::purify(expr const & e) {
return replace(e, [&](expr const & e, unsigned) {
if (!has_expr_metavar(e) && !has_local(e) && (!m_universes || !has_univ_metavar(e))) {
return some_expr(e);
} else if (is_metavar(e) && !is_idx_metavar(e) && !is_metavar_decl_ref(e) && m_purify_metavars) {
} else if (is_metavar_decl_ref(e) && m_purify_metavars) {
return some_expr(mk_metavar(mk_metavar_name(mlocal_name(e), "m"), infer_type(e)));
} else if (is_metavar(e) && !is_idx_metavar(e) && m_purify_metavars) {
return some_expr(mk_metavar(mk_metavar_name(mlocal_name(e)), infer_type(e)));
} else if (is_local(e)) {
return some_expr(mk_local(mlocal_name(e), mk_local_name(mlocal_name(e), local_pp_name(e)),

5
src/frontends/lean/pp.h
View file

@ -76,7 +76,10 @@ private:
bool m_binder_types;
bool m_lazy_abstraction;
name mk_metavar_name(name const & m);
name mk_metavar_name(name const & m, optional<name> const & prefix = optional<name>());
name mk_metavar_name(name const & m, name const & prefix) {
return mk_metavar_name(m, optional<name>(prefix));
}
name mk_local_name(name const & n, name const & suggested);
level purify(level const & l);
expr purify(expr const & e);

4
tests/lean/assert_tac3.lean.expected.out
View file

@ -1,5 +1,5 @@
a : ℕ,
x : ℕ := ?m_818
x : ℕ := ?m_1
⊢ a = a
a : ℕ
@ -7,7 +7,7 @@ a : ℕ
definition tst2 : ∀ (a : ℕ), a = a :=
λ a, let x : ℕ := a in eq.refl a
a b : ℕ,
x : ℕ := ?m_1733
x : ℕ := ?m_1
⊢ a = a
a b : ℕ

2
tests/lean/elab2.lean.expected.out
View file

@ -1,6 +1,6 @@
@foo.{1 1} nat nat nat_has_add (@zero.{1} nat nat_has_zero) (@one.{1} nat nat_has_one) : nat
elab2.lean:13:6: error: type mismatch at application
@bla.{1 ?l_231} nat ?m_233 nat.zero bool.tt
@bla.{1 ?l_1} nat ?m_2 nat.zero bool.tt
term
bool.tt
has type

2
tests/lean/elab6.lean.expected.out
View file

@ -4,7 +4,7 @@ H : @transitive.{1} nat R
@F.{1} bool ?a ?b bool.tt ?e bool.tt : bool → bool
@F.{1} bool ?a ?b bool.tt ?e bool.tt bool.tt : bool
H : @transitive.{1} nat R
@F.{?l_63} ?M_1 : Π ⦃a : ?M_1⦄ {b : ?M_1}, ?M_1 → (Π ⦃e : ?M_1⦄, ?M_1 → ?M_1 → ?M_1)
@F.{?l_2} ?M_1 : Π ⦃a : ?M_1⦄ {b : ?M_1}, ?M_1 → (Π ⦃e : ?M_1⦄, ?M_1 → ?M_1 → ?M_1)
@F.{1} bool ?M_1 ?M_2 bool.tt : Π ⦃e : bool⦄, bool → bool → bool
@F.{1} bool ?M_1 ?M_2 bool.tt ?M_3 bool.tt : bool → bool
@F.{1} bool ?M_1 ?M_2 bool.tt ?M_3 bool.tt bool.tt : bool

6
tests/lean/focus_tac.lean.expected.out
View file

@ -3,7 +3,7 @@ a : ℕ
⊢ ℕ
a : ℕ,
x : ℕ := ?m_1040
x : ℕ := ?m_1
⊢ a = a
--- inside focus tac ---
a : ℕ
@ -20,12 +20,12 @@ a : ℕ
⊢ ℕ
a : ℕ,
x : ℕ := ?m_2139
x : ℕ := ?m_1
⊢ a = a
--- inside focus tac ---
a : ℕ
⊢ ℕ
---- after focus tac ----
a : ℕ,
x : ℕ := ?m_2139
x : ℕ := ?m_1
⊢ a = a

2
tests/lean/struct_class.lean.expected.out
View file

@ -8,6 +8,7 @@ has_append : Type → Type
has_coe : Type → Type → Type
has_coe_t : Type → Type → Type
has_coe_to_fun : Type → Type
has_coe_to_sort : Type → Type
has_div : Type → Type
has_dvd : Type → Type
has_inv : Type → Type
@ -44,6 +45,7 @@ has_append : Type → Type
has_coe : Type → Type → Type
has_coe_t : Type → Type → Type
has_coe_to_fun : Type → Type
has_coe_to_sort : Type → Type
has_div : Type → Type
has_dvd : Type → Type
has_inv : Type → Type

14
tests/lean/unify1.lean.expected.out
View file

@ -1,24 +1,24 @@
id (?m_95 ++ ?m_96) =?= [1, 2] ++ [3, 4]
id (?m_m_1 ++ ?m_m_2) =?= [1, 2] ++ [3, 4]
id ([1, 2] ++ [3, 4]) =?= [1, 2] ++ [3, 4]
success
?m_150 ++ ?m_151 =?= id ([1, 2] ++ [3, 4])
?m_m_1 ++ ?m_m_2 =?= id ([1, 2] ++ [3, 4])
[1, 2] ++ [3, 4] =?= id ([1, 2] ++ [3, 4])
success
?m_201 ++ ?m_202 =?= ID ([1, 2] ++ [3, 4])
?m_m_1 ++ ?m_m_2 =?= ID ([1, 2] ++ [3, 4])
[1, 2] ++ [3, 4] =?= ID ([1, 2] ++ [3, 4])
success
?m_254 ++ ?m_255 =?= ID (ID ([1, 2] ++ [3, 4]))
?m_m_1 ++ ?m_m_2 =?= ID (ID ([1, 2] ++ [3, 4]))
[1, 2] ++ [3, 4] =?= ID (ID ([1, 2] ++ [3, 4]))
success
ID (?m_310 ++ ?m_311) =?= ID ([1, 2] ++ [3, 4])
ID (?m_m_1 ++ ?m_m_2) =?= ID ([1, 2] ++ [3, 4])
ID ([1, 2] ++ [3, 4]) =?= ID ([1, 2] ++ [3, 4])
success
ID (?m_363 ++ ?m_364) =?= [1, 2] ++ [3, 4]
ID (?m_m_1 ++ ?m_m_2) =?= [1, 2] ++ [3, 4]
ID ([1, 2] ++ [3, 4]) =?= [1, 2] ++ [3, 4]
success
[1] ++ [2, 3, 4] =?= [1, 2] ++ [3, 4]
[1] ++ [2, 3, 4] =?= [1, 2] ++ [3, 4]
success
y1 :: ?m_465 ++ ?m_467 =?= let l := [y1] in l ++ [y2]
y1 :: ?m_m_1 ++ ?m_m_2 =?= let l := [y1] in l ++ [y2]
[y1] ++ [y2] =?= let l := [y1] in l ++ [y2]
success

2
tests/lean/unify3.lean.expected.out
View file

@ -1,5 +1,5 @@
pattern:
@eq.{?l_3876} ?m_3879 ?m_3882 ?m_3885
@eq.{?l_1} ?m_2 ?m_3 ?m_4
term to unify:
@eq.{1} nat a b
unification results using whnf: