refactor(library/tactic, library/init/meta): simplify_config => simp_config
This commit is contained in:
Leonardo de Moura
parent
b52e8d67be
commit
296d4b0f09
8 changed files with 52 additions and 63 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 :=
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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<pair<simp_result, bool>> 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<expr> 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))
|
||||
|
|
|
|||
|
|
@ -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<expr> 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) {}
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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) :=
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue