From f72f9dd561fdff28ad963c03299c7ff1e79b6abd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 30 Jul 2016 20:30:03 -0700 Subject: [PATCH] fix(frontends/lean/pp): purify metavar_decl_ref's The tests become too fragile if we don't purify them. --- src/frontends/lean/pp.cpp | 16 ++++++++++++---- src/frontends/lean/pp.h | 5 ++++- tests/lean/assert_tac3.lean.expected.out | 4 ++-- tests/lean/elab2.lean.expected.out | 2 +- tests/lean/elab6.lean.expected.out | 2 +- tests/lean/focus_tac.lean.expected.out | 6 +++--- tests/lean/struct_class.lean.expected.out | 2 ++ tests/lean/unify1.lean.expected.out | 14 +++++++------- tests/lean/unify3.lean.expected.out | 2 +- 9 files changed, 33 insertions(+), 20 deletions(-) diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index b20d7b16ad..48b94670da 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -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 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)), diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h index 46b77a7f1c..8d918c123e 100644 --- a/src/frontends/lean/pp.h +++ b/src/frontends/lean/pp.h @@ -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 const & prefix = optional()); + name mk_metavar_name(name const & m, name const & prefix) { + return mk_metavar_name(m, optional(prefix)); + } name mk_local_name(name const & n, name const & suggested); level purify(level const & l); expr purify(expr const & e); diff --git a/tests/lean/assert_tac3.lean.expected.out b/tests/lean/assert_tac3.lean.expected.out index ec9f5927c9..24a56f4c00 100644 --- a/tests/lean/assert_tac3.lean.expected.out +++ b/tests/lean/assert_tac3.lean.expected.out @@ -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 : ℕ diff --git a/tests/lean/elab2.lean.expected.out b/tests/lean/elab2.lean.expected.out index 00feed3e0a..7bee78eeb1 100644 --- a/tests/lean/elab2.lean.expected.out +++ b/tests/lean/elab2.lean.expected.out @@ -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 diff --git a/tests/lean/elab6.lean.expected.out b/tests/lean/elab6.lean.expected.out index 2e6ccad339..343ed8224a 100644 --- a/tests/lean/elab6.lean.expected.out +++ b/tests/lean/elab6.lean.expected.out @@ -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 diff --git a/tests/lean/focus_tac.lean.expected.out b/tests/lean/focus_tac.lean.expected.out index 437ab37c8c..ed8eda523f 100644 --- a/tests/lean/focus_tac.lean.expected.out +++ b/tests/lean/focus_tac.lean.expected.out @@ -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 diff --git a/tests/lean/struct_class.lean.expected.out b/tests/lean/struct_class.lean.expected.out index cd345d05f5..3bcab2f4b7 100644 --- a/tests/lean/struct_class.lean.expected.out +++ b/tests/lean/struct_class.lean.expected.out @@ -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 diff --git a/tests/lean/unify1.lean.expected.out b/tests/lean/unify1.lean.expected.out index 64736bb878..c5156a7fea 100644 --- a/tests/lean/unify1.lean.expected.out +++ b/tests/lean/unify1.lean.expected.out @@ -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 diff --git a/tests/lean/unify3.lean.expected.out b/tests/lean/unify3.lean.expected.out index fbb5baba8e..c4524a40bc 100644 --- a/tests/lean/unify3.lean.expected.out +++ b/tests/lean/unify3.lean.expected.out @@ -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: