From 9bee8ce36d5e04c154fb14e7245e4274a6066e71 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 2 Feb 2017 17:19:21 -0800 Subject: [PATCH] fix(frontends/lean/elaborator): thunk gadget should not be considered in patterns The new test demonstrates the problem. --- library/init/meta/constructor_tactic.lean | 2 +- src/frontends/lean/elaborator.cpp | 6 +- tests/lean/run/isabelle.lean | 130 ++++++++++++++++++++++ 3 files changed, 135 insertions(+), 3 deletions(-) create mode 100644 tests/lean/run/isabelle.lean diff --git a/library/init/meta/constructor_tactic.lean b/library/init/meta/constructor_tactic.lean index d965e9f4af..30e7cfd26b 100644 --- a/library/init/meta/constructor_tactic.lean +++ b/library/init/meta/constructor_tactic.lean @@ -8,7 +8,7 @@ import init.meta.tactic init.function namespace tactic -private meta def get_constructors_for (e : expr) : tactic (list name) := +meta def get_constructors_for (e : expr) : tactic (list name) := do env ← get_env, I ← return $ expr.const_name (expr.get_app_fn e), when (environment.is_inductive env I = ff) (fail "constructor tactic failed, target is not an inductive datatype"), diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 81ab7f2779..ab8cb8f0a7 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1178,7 +1178,8 @@ expr elaborator::second_pass(expr const & fn, buffer const & args, } expr ref_arg = get_ref_for_child(args[i], ref); expr expected_type = info.args_expected_types[i]; - optional thunk_of = is_thunk(expected_type); + optional thunk_of; + if (!m_in_pattern) thunk_of = is_thunk(expected_type); if (thunk_of) expected_type = *thunk_of; expr new_arg = visit(args[i], some_expr(expected_type)); @@ -1251,7 +1252,8 @@ expr elaborator::visit_base_app_simple(expr const & _fn, arg_mask amask, buffer< new_arg = copy_tag(ref, mk_inaccessible(new_arg)); } else if (i < args.size()) { expr expected_type = d; - optional thunk_of = is_thunk(d); + optional thunk_of; + if (!m_in_pattern) thunk_of = is_thunk(d); if (thunk_of) expected_type = *thunk_of; // explicit argument expr ref_arg = get_ref_for_child(args[i], ref); diff --git a/tests/lean/run/isabelle.lean b/tests/lean/run/isabelle.lean new file mode 100644 index 0000000000..9fb79a09bb --- /dev/null +++ b/tests/lean/run/isabelle.lean @@ -0,0 +1,130 @@ +/- +Isabelle style tactics. +This test is based on a file created by Gabriel Ebner. +-/ +universe variables u v + +inductive lazy_list (α : Type u) : Type u +| nil {} : lazy_list +| cons : α → thunk (lazy_list) → lazy_list + +namespace lazy_list +variables {α : Type u} {β : Type v} + +def singleton : α → lazy_list α +| a := cons a nil + +def of_list : list α → lazy_list α +| [] := nil +| (h::t) := cons h (of_list t) + +def append : lazy_list α → thunk (lazy_list α) → lazy_list α +| nil l := l () +| (cons h t) l := cons h (append (t ()) (l ())) + +def map (f : α → β) : lazy_list α → lazy_list β +| nil := nil +| (cons h t) := cons (f h) (map (t ())) + +def join : lazy_list (lazy_list α) → lazy_list α +| nil := nil +| (cons h t) := append h (join (t ())) + +def for (l : lazy_list α) (f : α → β) : lazy_list β := +map f l + +def approx : nat → lazy_list α → list α +| 0 l := [] +| _ nil := [] +| (a+1) (cons h t) := h :: approx a (t ()) + +meta def above : nat → lazy_list nat +| i := cons i (above (i+1)) + +end lazy_list + +meta def lazy_tactic (α : Type u) := +tactic_state → lazy_list (α × tactic_state) + +namespace lazy_tactic +open lazy_list + +meta def of_tactic {α : Type u} (t : tactic α) : lazy_tactic α := +λ s, match t s with +| tactic_result.success a new_s := lazy_list.singleton (a, new_s) +| tactic_result.exception .α f e s := lazy_list.nil +end + +meta instance {α : Type} : has_coe (tactic α) (lazy_tactic α) := +⟨of_tactic⟩ + +protected meta def return {α} (a : α) : lazy_tactic α := +λ s, lazy_list.singleton (a, s) + +protected meta def map {α β} (f : α → β) : lazy_tactic α → lazy_tactic β +| t s := (t s)^.for (λ p, (f p.1, p.2)) + +protected meta def bind {α β} : lazy_tactic α → (α → lazy_tactic β) → lazy_tactic β := +λ t₁ t₂ s, join (map (λ p : α × tactic_state, t₂ p.1 p.2) (t₁ s)) + +protected meta def orelse {α} (t₁ t₂ : lazy_tactic α) : lazy_tactic α := +λ s, append (t₁ s) (t₂ s) + +protected meta def failure {α} : lazy_tactic α := +λ s, nil + +meta instance : monad lazy_tactic := +{ ret := @lazy_tactic.return, + bind := @lazy_tactic.bind, + map := @lazy_tactic.map } + +meta instance : alternative lazy_tactic := +{ map := @lazy_tactic.map, + pure := @lazy_tactic.return, + seq := @fapp _ _, + failure := @lazy_tactic.failure, + orelse := @lazy_tactic.orelse +} + +meta def choose {α} (xs : list α) : lazy_tactic α := +λ s, of_list $ xs^.for (λ a, (a, s)) + +meta def run {α} (t : lazy_tactic α) : tactic α := +λ s, match t s with +| nil := tactic.failed s +| cons (a, new_s) ss := tactic_result.success a new_s +end + +open tactic + +private meta def try_constructors : list name → lazy_tactic unit +| [] := failure +| (c::cs) := (mk_const c >>= apply : tactic unit) <|> try_constructors cs + +/- Backtracking version of constructor -/ +meta def constructor : lazy_tactic unit := +do t ← target, + cs ← get_constructors_for t, + try_constructors cs + +end lazy_tactic + +open lazy_tactic + +example (p q : Prop) : q → p ∨ q := +by run $ do + tactic.intros, + constructor, + tactic.trace_state, + tactic.assumption + +meta def naive_instantiation : lazy_tactic unit := +let vals := [`(1),`(2),`(3)] in do +x ← choose vals, +y ← choose vals, +e ← tactic.to_expr `(nat.add_comm %%x %%y), +tactic.trace e, +tactic.exact e + +lemma ex : 1 + 3 = 3 + 1 := +by naive_instantiation^.run