From 296d4b0f09f60f26e7ae350a8568275b322f7bdf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 19 Feb 2017 13:10:36 -0800 Subject: [PATCH] refactor(library/tactic, library/init/meta): simplify_config => simp_config --- library/init/meta/interactive.lean | 18 +++++----- library/init/meta/simp_tactic.lean | 42 +++++++++++------------ library/init/meta/smt/interactive.lean | 6 ++-- src/library/inductive_compiler/nested.cpp | 2 +- src/library/tactic/simplify.cpp | 18 +++++----- src/library/tactic/simplify.h | 16 ++++----- src/library/tactic/smt/smt_state.cpp | 2 +- tmp/mini_crush.lean | 11 ------ 8 files changed, 52 insertions(+), 63 deletions(-) diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 1862d8b692..3b6616f596 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -436,14 +436,14 @@ do s₀ ← join_user_simp_lemmas attr_names, s₁ ← simp_lemmas.append_pexprs s₀ hs, return $ simp_lemmas.erase s₁ ex -private meta def simp_goal (cfg : simplify_config) : simp_lemmas → tactic unit +private meta def simp_goal (cfg : simp_config) : simp_lemmas → tactic unit | s := do (new_target, Heq) ← target >>= simplify_core cfg s `eq, tactic.assert `Htarget new_target, swap, Ht ← get_local `Htarget, mk_eq_mpr Heq Ht >>= tactic.exact -private meta def simp_hyp (cfg : simplify_config) (s : simp_lemmas) (h_name : name) : tactic unit := +private meta def simp_hyp (cfg : simp_config) (s : simp_lemmas) (h_name : name) : tactic unit := do h ← get_local h_name, htype ← infer_type h, (new_htype, eqpr) ← simplify_core cfg s `eq htype, @@ -451,11 +451,11 @@ do h ← get_local h_name, mk_eq_mp eqpr h >>= tactic.exact, try $ tactic.clear h -private meta def simp_hyps (cfg : simplify_config) : simp_lemmas → list name → tactic unit +private meta def simp_hyps (cfg : simp_config) : simp_lemmas → list name → tactic unit | s [] := skip | s (h::hs) := simp_hyp cfg s h >> simp_hyps s hs -private meta def simp_core (cfg : simplify_config) (ctx : list expr) (hs : list pexpr) (attr_names : list name) (ids : list name) (loc : list name) : tactic unit := +private meta def simp_core (cfg : simp_config) (ctx : list expr) (hs : list pexpr) (attr_names : list name) (ids : list name) (loc : list name) : tactic unit := do s ← mk_simp_set attr_names hs ids, s ← s^.append ctx, match loc : _ → tactic unit with @@ -482,23 +482,23 @@ It has many variants. - `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`. -/ meta def simp (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (loc : parse location) - (cfg : simplify_config := {}) : tactic unit := + (cfg : simp_config := {}) : tactic unit := simp_core cfg [] hs attr_names ids loc /-- Similar to the `simp` tactic, but adds all applicable hypotheses as simplification rules. -/ meta def simp_using_hs (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) - (cfg : simplify_config := {}) : tactic unit := + (cfg : simp_config := {}) : tactic unit := do ctx ← collect_ctx_simps, simp_core cfg ctx hs attr_names ids [] meta def simph (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) - (cfg : simplify_config := {}) : tactic unit := + (cfg : simp_config := {}) : tactic unit := simp_using_hs hs attr_names ids cfg meta def simp_intros (ids : parse ident*) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) - (wo_ids : parse without_ident_list) (cfg : simplify_config := {}) : tactic unit := + (wo_ids : parse without_ident_list) (cfg : simp_config := {}) : tactic unit := do s ← mk_simp_set attr_names hs wo_ids, match ids with | [] := simp_intros_using s cfg @@ -507,7 +507,7 @@ do s ← mk_simp_set attr_names hs wo_ids, try triv >> try (reflexivity reducible) meta def simph_intros (ids : parse ident*) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) - (wo_ids : parse without_ident_list) (cfg : simplify_config := {}) : tactic unit := + (wo_ids : parse without_ident_list) (cfg : simp_config := {}) : tactic unit := do s ← mk_simp_set attr_names hs wo_ids, match ids with | [] := simph_intros_using s cfg diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean index 1475ce7895..103eec9c30 100644 --- a/library/init/meta/simp_tactic.lean +++ b/library/init/meta/simp_tactic.lean @@ -185,7 +185,7 @@ do num_reverted ← revert h, change $ expr.pi n bi new_d b, intron num_reverted -structure simplify_config := +structure simp_config := (max_steps : nat := default_max_steps) (contextual : bool := ff) (lift_eq : bool := tt) @@ -195,7 +195,7 @@ structure simplify_config := (zeta : bool := tt) meta constant simplify_core - (c : simplify_config) + (c : simp_config) (s : simp_lemmas) (r : name) : expr → tactic (expr × expr) @@ -205,7 +205,7 @@ meta constant ext_simplify_core {α : Type} /- Initial user data -/ (a : α) - (c : simplify_config) + (c : simp_config) /- Congruence and simplification lemmas. Remark: the simplification lemmas at not applied automatically like in the simplify_core tactic. the caller must use them at pre/post. -/ @@ -230,7 +230,7 @@ meta constant ext_simplify_core (r : name) : expr → tactic (α × expr × expr) -meta def simplify (S : simp_lemmas) (e : expr) (cfg : simplify_config := {}) : tactic (expr × expr) := +meta def simplify (S : simp_lemmas) (e : expr) (cfg : simp_config := {}) : tactic (expr × expr) := do e_type ← infer_type e >>= whnf, simplify_core cfg S `eq e @@ -239,16 +239,16 @@ do assert `htarget new_target, swap, ht ← get_local `htarget, mk_eq_mpr pr ht >>= exact -meta def simplify_goal (S : simp_lemmas) (cfg : simplify_config := {}) : tactic unit := +meta def simplify_goal (S : simp_lemmas) (cfg : simp_config := {}) : tactic unit := do t ← target, (new_t, pr) ← simplify S t cfg, replace_target new_t pr -meta def simp (cfg : simplify_config := {}) : tactic unit := +meta def simp (cfg : simp_config := {}) : tactic unit := do S ← simp_lemmas.mk_default, simplify_goal S cfg >> try triv >> try (reflexivity reducible) -meta def simp_using (hs : list expr) (cfg : simplify_config := {}) : tactic unit := +meta def simp_using (hs : list expr) (cfg : simp_config := {}) : tactic unit := do S ← simp_lemmas.mk_default, S ← S^.append hs, simplify_goal S cfg >> try triv @@ -288,10 +288,10 @@ meta def collect_ctx_simps : tactic (list expr) := local_context >>= collect_simps /-- Simplify target using all hypotheses in the local context. -/ -meta def simp_using_hs (cfg : simplify_config := {}) : tactic unit := +meta def simp_using_hs (cfg : simp_config := {}) : tactic unit := do es ← collect_ctx_simps, simp_using es cfg -meta def simph (cfg : simplify_config := {}) := +meta def simph (cfg : simp_config := {}) := simp_using_hs cfg meta def intro1_aux : bool → list name → tactic expr @@ -299,7 +299,7 @@ meta def intro1_aux : bool → list name → tactic expr | tt (n::ns) := intro n | _ _ := failed -meta def simp_intro_aux (cfg : simplify_config) (updt : bool) : simp_lemmas → bool → list name → tactic unit +meta def simp_intro_aux (cfg : simp_config) (updt : bool) : simp_lemmas → bool → list name → tactic unit | S tt [] := return () | S use_ns ns := do t ← target, @@ -322,21 +322,21 @@ meta def simp_intro_aux (cfg : simplify_config) (updt : bool) : simp_lemmas → if new_t^.is_pi then change new_t >> simp_intro_aux S use_ns ns else return () -meta def simp_intros_using (s : simp_lemmas) (cfg : simplify_config := {}) : tactic unit := +meta def simp_intros_using (s : simp_lemmas) (cfg : simp_config := {}) : tactic unit := simp_intro_aux cfg ff s ff [] -meta def simph_intros_using (s : simp_lemmas) (cfg : simplify_config := {}) : tactic unit := +meta def simph_intros_using (s : simp_lemmas) (cfg : simp_config := {}) : tactic unit := do s ← collect_ctx_simps >>= s^.append, simp_intro_aux cfg tt s ff [] -meta def simp_intro_lst_using (ns : list name) (s : simp_lemmas) (cfg : simplify_config := {}) : tactic unit := +meta def simp_intro_lst_using (ns : list name) (s : simp_lemmas) (cfg : simp_config := {}) : tactic unit := simp_intro_aux cfg ff s tt ns -meta def simph_intro_lst_using (ns : list name) (s : simp_lemmas) (cfg : simplify_config := {}) : tactic unit := +meta def simph_intro_lst_using (ns : list name) (s : simp_lemmas) (cfg : simp_config := {}) : tactic unit := do s ← collect_ctx_simps >>= s^.append, simp_intro_aux cfg tt s tt ns -meta def simp_at (h : expr) (extra_lemmas : list expr := []) (cfg : simplify_config := {}) : tactic unit := +meta def simp_at (h : expr) (extra_lemmas : list expr := []) (cfg : simp_config := {}) : tactic unit := do when (expr.is_local_constant h = ff) (fail "tactic simp_at failed, the given expression is not a hypothesis"), htype ← infer_type h, S ← simp_lemmas.mk_default, @@ -346,11 +346,11 @@ do when (expr.is_local_constant h = ff) (fail "tactic simp_at failed, the given mk_eq_mp heq h >>= exact, try $ clear h -meta def simp_at_using_hs (h : expr) (extra_lemmas : list expr := []) (cfg : simplify_config := {}) : tactic unit := +meta def simp_at_using_hs (h : expr) (extra_lemmas : list expr := []) (cfg : simp_config := {}) : tactic unit := do hs ← collect_ctx_simps, simp_at h (list.filter (≠ h) hs ++ extra_lemmas) cfg -meta def simph_at (h : expr) (extra_lemmas : list expr := []) (cfg : simplify_config := {}) : tactic unit := +meta def simph_at (h : expr) (extra_lemmas : list expr := []) (cfg : simp_config := {}) : tactic unit := simp_at_using_hs h extra_lemmas cfg meta def mk_eq_simp_ext (simp_ext : expr → tactic (expr × expr)) : tactic unit := @@ -394,24 +394,24 @@ meta def join_user_simp_lemmas : list name → tactic simp_lemmas and pr is a proof that the input argument is equal to n. -/ meta constant norm_num : expr → tactic (expr × expr) -meta def simplify_top_down {α} (a : α) (pre : α → expr → tactic (α × expr × expr)) (e : expr) (cfg : simplify_config := {}) : tactic (α × expr × expr) := +meta def simplify_top_down {α} (a : α) (pre : α → expr → tactic (α × expr × expr)) (e : expr) (cfg : simp_config := {}) : tactic (α × expr × expr) := ext_simplify_core a cfg simp_lemmas.mk (λ _, failed) (λ a _ _ _ e, do (new_a, new_e, pr) ← pre a e, guard (¬ new_e =ₐ e), return (new_a, new_e, some pr, tt)) (λ _ _ _ _ _, failed) `eq e -meta def simp_top_down (pre : expr → tactic (expr × expr)) (cfg : simplify_config := {}) : tactic unit := +meta def simp_top_down (pre : expr → tactic (expr × expr)) (cfg : simp_config := {}) : tactic unit := do t ← target, (_, new_target, pr) ← simplify_top_down () (λ _ e, do (new_e, pr) ← pre e, return ((), new_e, pr)) t cfg, replace_target new_target pr -meta def simplify_bottom_up {α} (a : α) (post : α → expr → tactic (α × expr × expr)) (e : expr) (cfg : simplify_config := {}) : tactic (α × expr × expr) := +meta def simplify_bottom_up {α} (a : α) (post : α → expr → tactic (α × expr × expr)) (e : expr) (cfg : simp_config := {}) : tactic (α × expr × expr) := ext_simplify_core a cfg simp_lemmas.mk (λ _, failed) (λ _ _ _ _ _, failed) (λ a _ _ _ e, do (new_a, new_e, pr) ← post a e, guard (¬ new_e =ₐ e), return (new_a, new_e, some pr, tt)) `eq e -meta def simp_bottom_up (post : expr → tactic (expr × expr)) (cfg : simplify_config := {}) : tactic unit := +meta def simp_bottom_up (post : expr → tactic (expr × expr)) (cfg : simp_config := {}) : tactic unit := do t ← target, (_, new_target, pr) ← simplify_bottom_up () (λ _ e, do (new_e, pr) ← post e, return ((), new_e, pr)) t cfg, replace_target new_target pr diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean index b6569df7a4..2906eb2970 100644 --- a/library/init/meta/smt/interactive.lean +++ b/library/init/meta/smt/interactive.lean @@ -232,14 +232,14 @@ slift (tactic.interactive.induction p rec_name ids) open tactic /-- Simplify the target type of the main goal. -/ -meta def simp (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simplify_config := {}) : smt_tactic unit := +meta def simp (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simp_config := {}) : smt_tactic unit := tactic.interactive.simp hs attr_names ids [] cfg /-- Simplify the target type of the main goal using simplification lemmas and the current set of hypotheses. -/ -meta def simp_using_hs (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simplify_config := {}) : smt_tactic unit := +meta def simp_using_hs (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simp_config := {}) : smt_tactic unit := tactic.interactive.simp_using_hs hs attr_names ids cfg -meta def simph (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simplify_config := {}) : smt_tactic unit := +meta def simph (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simp_config := {}) : smt_tactic unit := simp_using_hs hs attr_names ids cfg meta def dsimp (es : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : smt_tactic unit := diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp index 13510d4c2c..903a2a3b1a 100644 --- a/src/library/inductive_compiler/nested.cpp +++ b/src/library/inductive_compiler/nested.cpp @@ -1260,7 +1260,7 @@ class add_nested_inductive_decl_fn { all_lemmas = add(tctx_whnf, all_lemmas, mlocal_name(H), H_type, H, LEAN_DEFAULT_PRIORITY); } lean_trace(name({"inductive_compiler", "nested", "simp", "start"}), tout() << thm << "\n";); - simplify_config cfg; + simp_config cfg; cfg.m_max_steps = 1000000; cfg.m_contextual = false; cfg.m_lift_eq = false; diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp index f508058499..b9f42c4d0f 100644 --- a/src/library/tactic/simplify.cpp +++ b/src/library/tactic/simplify.cpp @@ -60,7 +60,7 @@ namespace lean { #define lean_simp_trace(CTX, N, CODE) lean_trace(N, scope_trace_env _scope1(CTX.env(), CTX); CODE) #define lean_simp_trace_d(CTX, N, CODE) lean_trace_d(N, scope_trace_env _scope1(CTX.env(), CTX); CODE) -simplify_config::simplify_config(): +simp_config::simp_config(): m_max_steps(LEAN_DEFAULT_SIMPLIFY_MAX_STEPS), m_contextual(LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL), m_lift_eq(LEAN_DEFAULT_SIMPLIFY_LIFT_EQ), @@ -70,7 +70,7 @@ simplify_config::simplify_config(): m_zeta(false) { } -simplify_config::simplify_config(vm_obj const & obj) { +simp_config::simp_config(vm_obj const & obj) { m_max_steps = force_to_unsigned(cfield(obj, 0)); m_contextual = to_bool(cfield(obj, 1)); m_lift_eq = to_bool(cfield(obj, 2)); @@ -853,7 +853,7 @@ optional> simplify_core_fn::post(expr const &, optional< } simplify_core_fn::simplify_core_fn(type_context & ctx, defeq_canonizer::state & dcs, simp_lemmas const & slss, - simplify_config const & cfg): + simp_config const & cfg): m_ctx(ctx), m_defeq_canonizer(m_ctx, dcs), m_slss(slss), m_cfg(cfg) { } @@ -915,7 +915,7 @@ optional simplify_core_fn::prove_by_simp(name const & rel, expr const & e) ------------------------------------ */ simplify_ext_core_fn::simplify_ext_core_fn(type_context & ctx, defeq_can_state & dcs, simp_lemmas const & slss, - simplify_config const & cfg): + simp_config const & cfg): simplify_core_fn(ctx, dcs, slss, cfg) { } @@ -1149,7 +1149,7 @@ class vm_simplify_fn : public simplify_ext_core_fn { } public: - vm_simplify_fn(type_context & ctx, defeq_can_state & dcs, simp_lemmas const & slss, simplify_config const & cfg, + vm_simplify_fn(type_context & ctx, defeq_can_state & dcs, simp_lemmas const & slss, simp_config const & cfg, vm_obj const & prove, vm_obj const & pre, vm_obj const & post, tactic_state const & s): simplify_ext_core_fn(ctx, dcs, slss, cfg), m_prove(prove), m_pre(pre), m_post(post), @@ -1164,7 +1164,7 @@ public: /* meta constant simplify_core - (c : simplify_config) + (c : simp_config) (s : simp_lemmas) (r : name) : expr → tactic (expr × expr) @@ -1172,7 +1172,7 @@ meta constant simplify_core vm_obj tactic_simplify_core(vm_obj const & c, vm_obj const & slss, vm_obj const & rel, vm_obj const & e, vm_obj const & _s) { tactic_state const & s = tactic::to_state(_s); try { - simplify_config cfg(c); + simp_config cfg(c); type_context ctx = mk_type_context_for(s, transparency_mode::Reducible); defeq_can_state dcs = s.dcs(); simplify_fn simp(ctx, dcs, to_simp_lemmas(slss), cfg); @@ -1193,7 +1193,7 @@ static vm_obj ext_simplify_core(vm_obj const & a, vm_obj const & c, simp_lemmas vm_obj const & pre, vm_obj const & post, name const & r, expr const & e, tactic_state const & s) { try { - simplify_config cfg(c); + simp_config cfg(c); type_context ctx = mk_type_context_for(s, transparency_mode::Reducible); defeq_can_state dcs = s.dcs(); vm_simplify_fn simp(ctx, dcs, slss, cfg, prove, pre, post, s); @@ -1215,7 +1215,7 @@ static vm_obj ext_simplify_core(vm_obj const & a, vm_obj const & c, simp_lemmas meta constant ext_simplify_core {A : Type} (a : A) - (c : simplify_config) + (c : simp_config) (l : simp_lemmas) (prove : A → tactic A) (pre : A → name → simp_lemmas → option expr → expr → tactic (A × expr × option expr × bool)) diff --git a/src/library/tactic/simplify.h b/src/library/tactic/simplify.h index f5a2ab618a..d36e05919f 100644 --- a/src/library/tactic/simplify.h +++ b/src/library/tactic/simplify.h @@ -14,7 +14,7 @@ Author: Daniel Selsam, Leonardo de Moura namespace lean { /* -structure simplify_config := +structure simp_config := (max_steps : nat) (contextual : bool) (lift_eq : bool) @@ -23,7 +23,7 @@ structure simplify_config := (use_axioms : bool) (zeta : bool) */ -struct simplify_config { +struct simp_config { unsigned m_max_steps; bool m_contextual; bool m_lift_eq; @@ -34,8 +34,8 @@ struct simplify_config { /* The following option should be removed as soon as we refactor the inductive compiler. */ bool m_use_matcher{true}; - simplify_config(); - simplify_config(vm_obj const & o); + simp_config(); + simp_config(vm_obj const & o); }; /* Core simplification procedure. It performs the following tasks: @@ -72,7 +72,7 @@ protected: bool m_need_restart{false}; /* Options */ - simplify_config m_cfg; + simp_config m_cfg; simp_result join(simp_result const & r1, simp_result const & r2); void inc_num_steps(); @@ -128,7 +128,7 @@ protected: public: simplify_core_fn(type_context & ctx, defeq_canonizer::state & dcs, simp_lemmas const & slss, - simplify_config const & cfg); + simp_config const & cfg); environment const & env() const; simp_result operator()(name const & rel, expr const & e); @@ -147,7 +147,7 @@ protected: virtual simp_result visit_let(expr const & e) override; public: simplify_ext_core_fn(type_context & ctx, defeq_canonizer::state & dcs, simp_lemmas const & slss, - simplify_config const & cfg); + simp_config const & cfg); }; /* Default (bottom-up) simplifier: reduce projections, apply simplification lemmas, @@ -159,7 +159,7 @@ protected: virtual optional prove(expr const & e) override; public: simplify_fn(type_context & ctx, defeq_canonizer::state & dcs, simp_lemmas const & slss, - simplify_config const & cfg): + simp_config const & cfg): simplify_ext_core_fn(ctx, dcs, slss, cfg) {} }; diff --git a/src/library/tactic/smt/smt_state.cpp b/src/library/tactic/smt/smt_state.cpp index 812b81a51e..818b7f0e15 100644 --- a/src/library/tactic/smt/smt_state.cpp +++ b/src/library/tactic/smt/smt_state.cpp @@ -209,7 +209,7 @@ static dsimplify_fn mk_dsimp(type_context & ctx, defeq_can_state & dcs, smt_pre_ } static simplify_fn mk_simp(type_context & ctx, defeq_can_state & dcs, smt_pre_config const & cfg) { - simplify_config scfg; + simp_config scfg; scfg.m_max_steps = cfg.m_max_steps; scfg.m_contextual = false; scfg.m_lift_eq = true; diff --git a/tmp/mini_crush.lean b/tmp/mini_crush.lean index da39bce99e..e2c0fdd3a1 100644 --- a/tmp/mini_crush.lean +++ b/tmp/mini_crush.lean @@ -39,17 +39,6 @@ do ctx ← local_context, /- repeat simp & intro -/ -meta def simph_and_intro_aux : simp_lemmas → tactic unit -| S := do - t ← target, - - -return () - -meta def simph_and_intro : tactic unit := -do S ← simp_lemmas.mk_default, - S ← collect_ctx_simps >>= S^.append, - simph_and_intro_aux S meta def collect_ctx_simps : tactic (list expr) :=