From d0c2c73b35b50d26058e554575d440e95a2b3563 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 3 May 2017 10:56:43 +0200 Subject: [PATCH] refactor(init/meta,tools): rename `now` tactic to `done` It was pointed out that Coq already uses `now` for a different kind of tactic. And `done` is more descriptive anyway. --- library/init/meta/interactive.lean | 2 +- library/init/meta/mk_has_sizeof_instance.lean | 2 +- library/init/meta/mk_inhabited_instance.lean | 2 +- library/init/meta/smt/rsimp.lean | 2 +- library/init/meta/tactic.lean | 4 ++-- library/tools/mini_crush/default.lean | 14 +++++++------- library/tools/mini_crush/nano_crush.lean | 6 +++--- library/tools/super/cdcl_solver.lean | 2 +- library/tools/super/trim.lean | 2 +- tests/lean/run/aexp.lean | 2 +- tests/lean/run/listex3.lean | 2 +- 11 files changed, 20 insertions(+), 20 deletions(-) diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index b4510402fa..ee649985ee 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -241,7 +241,7 @@ Like `exact`, but takes a list of terms and checks that all goals are discharged after the tactic. -/ meta def exacts : parse qexpr_list_or_texpr → tactic unit -| [] := now +| [] := done | (t :: ts) := exact t >> exacts ts private meta def get_locals : list name → tactic (list expr) diff --git a/library/init/meta/mk_has_sizeof_instance.lean b/library/init/meta/mk_has_sizeof_instance.lean index 1bd0aa113a..7ff9a7b6d6 100644 --- a/library/init/meta/mk_has_sizeof_instance.lean +++ b/library/init/meta/mk_has_sizeof_instance.lean @@ -53,7 +53,7 @@ do szs ← mk_sizeof use_default I_name F_name field_names 0, exact (mk_sum szs) private meta def for_each_has_sizeof_goal : bool → name → name → list (list name) → tactic unit -| d I_name F_name [] := now <|> fail "mk_has_sizeof_instance failed, unexpected number of cases" +| d I_name F_name [] := done <|> fail "mk_has_sizeof_instance failed, unexpected number of cases" | d I_name F_name (ns::nss) := do solve1 (has_sizeof_case d I_name F_name ns), for_each_has_sizeof_goal d I_name F_name nss diff --git a/library/init/meta/mk_inhabited_instance.lean b/library/init/meta/mk_inhabited_instance.lean index 9687e05c9f..225a37d070 100644 --- a/library/init/meta/mk_inhabited_instance.lean +++ b/library/init/meta/mk_inhabited_instance.lean @@ -32,7 +32,7 @@ do tgt ← target, private meta def try_constructors : nat → nat → tactic unit | 0 n := failed | (i+1) n := - do {constructor_idx (n - i), all_goals mk_inhabited_arg, now} + do {constructor_idx (n - i), all_goals mk_inhabited_arg, done} <|> try_constructors i n diff --git a/library/init/meta/smt/rsimp.lean b/library/init/meta/smt/rsimp.lean index 743477320f..073e64cf9c 100644 --- a/library/init/meta/smt/rsimp.lean +++ b/library/init/meta/smt/rsimp.lean @@ -124,7 +124,7 @@ do focus1 $ using_smt_with {em_attr := cfg.attr_name} $ add_lemmas_from_facts, add_lemmas extra, repeat_at_most cfg.max_rounds (ematch >> try smt_tactic.close), - (now >> return cc_state.mk) + (done >> return cc_state.mk) <|> to_cc_state diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 015472b14c..6e4bfd9fc6 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -739,9 +739,9 @@ do n ← num_goals, when (n = 0) (fail "tactic failed, there are no goals to be solved") /- Fail if there are unsolved goals. -/ -meta def now : tactic unit := +meta def done : tactic unit := do n ← num_goals, - when (n ≠ 0) (fail "now tactic failed, there are unsolved goals") + when (n ≠ 0) (fail "done tactic failed, there are unsolved goals") meta def apply (e : expr) : tactic unit := apply_core e >> return () diff --git a/library/tools/mini_crush/default.lean b/library/tools/mini_crush/default.lean index 9b02218962..9a25fa4ef3 100644 --- a/library/tools/mini_crush/default.lean +++ b/library/tools/mini_crush/default.lean @@ -92,7 +92,7 @@ local_context >>= mfoldl (λ r h, mcond (is_inductive h) (return $ h::r) (return meta def try_induction_aux (cont : expr → tactic unit) : list expr → tactic unit | [] := failed -| (e::es) := (step (induction e); cont e; now) <|> try_induction_aux es +| (e::es) := (step (induction e); cont e; done) <|> try_induction_aux es meta def try_induction (cont : expr → tactic unit) : tactic unit := focus1 $ collect_inductive_hyps >>= try_induction_aux cont @@ -113,10 +113,10 @@ when_tracing `mini_crush $ /- Simple tactic -/ meta def close_aux (hs : hinst_lemmas) : tactic unit := triv <|> reflexivity reducible <|> contradiction -<|> try_for 1000 (rsimp {} hs >> now) <|> try_for 1000 reflexivity +<|> try_for 1000 (rsimp {} hs >> done) <|> try_for 1000 reflexivity meta def close (hs : hinst_lemmas) (s : name) (e : option expr) : tactic unit := - now + done <|> close_aux hs <|> report_failure s e >> failed @@ -135,11 +135,11 @@ tactic.write meta def try_snapshots {α} (cont : α → tactic unit) : list (α × snapshot) → tactic unit | [] := failed -| ((a, s)::ss) := (restore s >> cont a >> now) <|> try_snapshots ss +| ((a, s)::ss) := (restore s >> cont a >> done) <|> try_snapshots ss meta def search {α} (max_depth : nat) (act : nat → α → tactic (list (α × snapshot))) : nat → α → tactic unit | n s := do - now + done <|> if n > max_depth then when_tracing `mini_crush (trace "max depth reached" >> trace_state) >> failed else all_goals $ try intros >> act n s >>= try_snapshots (search (n+1)) @@ -208,7 +208,7 @@ meta def strategy_2_aux (cfg : simp_config) (hs : hinst_lemmas) : simp_lemmas do s ← simp_intro_aux cfg tt s tt [`_], -- Introduce next hypothesis h ← list.ilast <$> local_context, try $ solve1 (mwhen (is_inductive h) $ induction' h; simple s hs cfg "strategy 2" (some h)), - now <|> strategy_2_aux s + done <|> strategy_2_aux s meta def strategy_2 (cfg : simp_config := {}) (s : option simp_lemmas := none) (hs : option hinst_lemmas := none) : tactic unit := do s ← mk_simp_lemmas s, @@ -218,7 +218,7 @@ do s ← mk_simp_lemmas s, meta def strategy_3 (cfg : simp_config := {}) (max_depth : nat := 1) (s : option simp_lemmas := none) (hs : option hinst_lemmas := none) : tactic unit := do s ← mk_simp_lemmas s, hs ← mk_hinst_lemmas hs, - try_induction (λ h, try (simph_intros_using s cfg); try (close_aux hs); (now <|> search_cases max_depth s hs cfg "strategy 3")) + try_induction (λ h, try (simph_intros_using s cfg); try (close_aux hs); (done <|> search_cases max_depth s hs cfg "strategy 3")) end mini_crush diff --git a/library/tools/mini_crush/nano_crush.lean b/library/tools/mini_crush/nano_crush.lean index 05458eaf3e..84214a9621 100644 --- a/library/tools/mini_crush/nano_crush.lean +++ b/library/tools/mini_crush/nano_crush.lean @@ -90,7 +90,7 @@ local_context >>= mfoldl (λ r h, mcond (is_inductive h) (return $ h::r) (return meta def try_list_aux {α} (s : tactic_state) (tac : α → tactic unit) : list α → tactic unit | [] := failed -| (e::es) := (write s >> tac e >> now) <|> try_list_aux es +| (e::es) := (write s >> tac e >> done) <|> try_list_aux es meta def try_list {α} (tac : α → tactic unit) (es : list α) : tactic unit := do s ← read, try_list_aux s tac es @@ -102,8 +102,8 @@ meta def split (tac : tactic unit) : tactic unit := collect_inductive_from_target >>= try_list (λ e, cases e; tac) meta def search (tac : tactic unit) : nat → tactic unit -| 0 := all_goals tac >> now -| (d+1) := all_goals (try tac) >> (now <|> split (search d)) +| 0 := all_goals tac >> done +| (d+1) := all_goals (try tac) >> (done <|> split (search d)) meta def rsimp' (hs : hinst_lemmas) : tactic unit := rsimp {} hs diff --git a/library/tools/super/cdcl_solver.lean b/library/tools/super/cdcl_solver.lean index acd8b16311..e3b939253b 100644 --- a/library/tools/super/cdcl_solver.lean +++ b/library/tools/super/cdcl_solver.lean @@ -419,7 +419,7 @@ subgoal ← mk_meta_var s.local_false, goals ← get_goals, set_goals [subgoal], hvs ← for hyps (λhyp, assertv hyp.local_pp_name hyp.local_type hyp), -solved ← (do th_solver, now, return tt) <|> return ff, +solved ← (do th_solver, done, return tt) <|> return ff, set_goals goals, if solved then do proof ← instantiate_mvars subgoal, diff --git a/library/tools/super/trim.lean b/library/tools/super/trim.lean index 69d0a6258a..15727978f8 100644 --- a/library/tools/super/trim.lean +++ b/library/tools/super/trim.lean @@ -46,7 +46,7 @@ match gs with g' ← infer_type g >>= mk_meta_var, set_goals [g'], r ← tac, - now, + done, set_goals (g::gs), instantiate_mvars g' >>= trim' >>= exact, return r diff --git a/tests/lean/run/aexp.lean b/tests/lean/run/aexp.lean index e8d8362ed8..b4dfa099a1 100644 --- a/tests/lean/run/aexp.lean +++ b/tests/lean/run/aexp.lean @@ -53,7 +53,7 @@ attribute [ematch] asimp_const aval -- set_option trace.smt.ematch true -meta def not_done : tactic unit := fail_if_success now +meta def not_done : tactic unit := fail_if_success done lemma aval_asimp_const (a : aexp) (s : state) : aval (asimp_const a) s = aval a s := begin [smt] diff --git a/tests/lean/run/listex3.lean b/tests/lean/run/listex3.lean index bd66f785c5..ae31b5ae67 100644 --- a/tests/lean/run/listex3.lean +++ b/tests/lean/run/listex3.lean @@ -20,7 +20,7 @@ when_tracing `search_mem_list (do t ← target, f ← pp t, trace (to_fmt "searc (`[apply in_head]) <|> (`[apply in_tail] >> mk_mem_list_rec)) ->> now +>> done meta def mk_mem_list : tactic unit := solve1 mk_mem_list_rec