From e21a3ecdc0442bf795ea665d3a4bdbc5be22602d Mon Sep 17 00:00:00 2001 From: lecopivo Date: Fri, 31 May 2024 18:10:03 -0400 Subject: [PATCH] initial version of lsimp --- SciLean/Tactic/GTrans/MetaLCtxM.lean | 152 +++++ SciLean/Tactic/LSimp/Elab.lean | 211 +------ SciLean/Tactic/LSimp/Main.lean | 813 ++++++++++----------------- SciLean/Tactic/LSimp/Test.lean | 120 ++++ SciLean/Tactic/LSimp/Types.lean | 145 +++++ 5 files changed, 743 insertions(+), 698 deletions(-) create mode 100644 SciLean/Tactic/GTrans/MetaLCtxM.lean create mode 100644 SciLean/Tactic/LSimp/Test.lean create mode 100644 SciLean/Tactic/LSimp/Types.lean diff --git a/SciLean/Tactic/GTrans/MetaLCtxM.lean b/SciLean/Tactic/GTrans/MetaLCtxM.lean new file mode 100644 index 00000000..c686ac6b --- /dev/null +++ b/SciLean/Tactic/GTrans/MetaLCtxM.lean @@ -0,0 +1,152 @@ +import Lean +import Qq + +import SciLean.Lean.Meta.Basic + +open Lean Meta + +structure _root_.Lean.Meta.ContextCtx where + lctx : LocalContext := {} + localInstances : LocalInstances := #[] + deriving Inhabited + +structure _root_.Lean.Meta.ContextCfg where + config : Meta.Config := {} + defEqCtx? : Option DefEqContext := none + synthPendingDepth : Nat := 0 + canUnfold? : Option (Meta.Config → ConstantInfo → CoreM Bool) := none + + +def Lean.Meta.Context.toCtx (ctx : Meta.Context) : ContextCtx where + lctx := ctx.lctx + localInstances := ctx.localInstances + +def Lean.Meta.Context.toCfg (cfg : Meta.Context) : ContextCfg where + config := cfg.config + defEqCtx? := cfg.defEqCtx? + synthPendingDepth := cfg.synthPendingDepth + canUnfold? := cfg.canUnfold? + + +def _root_.Lean.Meta.Context.mkCtxCfg (ctx : ContextCtx) (cfg : ContextCfg) : Meta.Context := + { config := cfg.config + lctx := ctx.lctx + localInstances := ctx.localInstances + defEqCtx? := cfg.defEqCtx? + synthPendingDepth := cfg.synthPendingDepth + canUnfold? := cfg.canUnfold? } + +-- TODO: change the monad such that we can only add variables to the context and not remove them +-- or completely changes the context +abbrev MetaLCtxM := ReaderT Meta.ContextCfg $ StateT Meta.ContextCtx $ StateRefT Meta.State CoreM + + +@[always_inline] +instance : Monad MetaLCtxM := let i := inferInstanceAs (Monad MetaLCtxM); { pure := i.pure, bind := i.bind } + +instance {α} [Inhabited α] : Inhabited (MetaLCtxM α) where + default := fun _ ctx => do pure (default,ctx) + +instance : MonadLCtx MetaLCtxM where + getLCtx := return (← get).lctx + +instance : MonadMCtx MetaLCtxM where + getMCtx := return (← getThe Meta.State).mctx + modifyMCtx f := modifyThe Meta.State fun s => { s with mctx := f s.mctx } + +instance : MonadEnv MetaLCtxM where + getEnv := return (← getThe Core.State).env + modifyEnv f := do modifyThe Core.State fun s => { s with env := f s.env, cache := {} }; modifyThe Meta.State fun s => { s with cache := {} } + +instance : AddMessageContext MetaLCtxM where + addMessageContext := addMessageContextFull + +instance : MonadLift MetaM MetaLCtxM where + monadLift x := fun cfg ctx => do let r ← x (.mkCtxCfg ctx cfg); pure (r, ctx) + +protected def MetaLCtxM.saveState : MetaLCtxM (SavedState×ContextCtx) := + return ({ core := (← getThe Core.State), meta := (← get) }, ⟨← getLCtx, ← getLocalInstances⟩) + +def MetaLCtxM.restore (b : SavedState) (ctx : ContextCtx) : MetaLCtxM Unit := do + Core.restore b.core + modify fun s => { s with mctx := b.meta.mctx, zetaDeltaFVarIds := b.meta.zetaDeltaFVarIds, postponed := b.meta.postponed } + modifyThe ContextCtx fun _ => ctx + +instance : MonadBacktrack (SavedState×ContextCtx) MetaLCtxM where + saveState := MetaLCtxM.saveState + restoreState s := MetaLCtxM.restore s.1 s.2 + +@[inline] def MetaLCtxM.run (x : MetaLCtxM α) (cfg : ContextCfg := {}) (ctx : ContextCtx := {}) (s : Meta.State := {}) : + CoreM (α × Meta.State) := do + let ((r,_),s) ← x cfg ctx |>.run s + return (r,s) + +@[inline] def MetaLCtxM.run' (x : MetaLCtxM α) (cfg : ContextCfg := {}) (ctx : ContextCtx := {}) (s : Meta.State := {}) : CoreM α := do + let ((r,_),_) ← x cfg ctx |>.run s + return r + +@[inline] def MetaLCtxM.runInMeta (a : MetaLCtxM α) (k : α → MetaM β) : MetaM β := + fun ctx => do + let cfg := ctx.toCfg + let ctx := ctx.toCtx + let (a,ctx) ← a cfg ctx + k a (.mkCtxCfg ctx cfg) + +instance [MetaEval α] : MetaEval (MetaLCtxM α) := + ⟨fun env opts x _ => MetaEval.eval env opts x.run' true⟩ + + +instance : MonadControl MetaM MetaLCtxM where + stM := fun α => α × ContextCtx + liftWith := fun f => do + let cfg ← readThe ContextCfg + let f' := (f (fun x c s => do + let (x',ctx') ← x cfg ⟨c.lctx,c.localInstances⟩ s + return (x', ctx'))) + f' + restoreM := fun x => do let (a, s) ← liftM x; set s; pure a + + +def lambdaIntro (e : Expr) : MetaLCtxM (Expr × Array Expr) := do + Meta.lambdaTelescope e fun xs e' => do + let ctx ← getThe ContextCtx + fun _ _ => return ((e',xs), ctx) + + +def letIntro (e : Expr) : MetaLCtxM (Expr × Array Expr) := do + Meta.letTelescope e fun xs e' => do + let ctx ← getThe ContextCtx + fun _ _ => return ((e',xs), ctx) + + +/-- Adds let declaration into the local context. Returns newly created free variable. + +Similar to `withLetDecl` but runs in `MetaLCtxM` instead of `MetaM`. -/ +def introLocalDecl (name : Name) (bi : BinderInfo) (type : Expr) : MetaLCtxM Expr := do + let fvarId ← mkFreshFVarId + fun _ ctx => + let ctx := {ctx with lctx := ctx.lctx.mkLocalDecl fvarId name type bi .default} + let fvar := Expr.fvar fvarId + return (fvar, ctx) + + +/-- Adds let declaration into the local context. Returns newly created free variable. + +Similar to `withLetDecl` but runs in `MetaLCtxM` instead of `MetaM`. -/ +def introLetDecl (name : Name) (type val : Expr) : MetaLCtxM Expr := do + let fvarId ← mkFreshFVarId + fun _ ctx => + let ctx := {ctx with lctx := ctx.lctx.mkLetDecl fvarId name type val (nonDep := false) .default} + let fvar := Expr.fvar fvarId + return (fvar, ctx) + + +open Lean Meta Qq in +#eval show MetaLCtxM Unit from do + let e := q(fun a b => a + b + 42) + + let (b, xs) ← lambdaIntro e + + IO.println s!"lambda body: {← ppExpr b}" + IO.println s!"lambda vars: {← liftM <| xs.mapM ppExpr}" + IO.println s!"lambda: {← ppExpr (← mkLambdaFVars xs b)}" diff --git a/SciLean/Tactic/LSimp/Elab.lean b/SciLean/Tactic/LSimp/Elab.lean index a721e858..ba75d68c 100644 --- a/SciLean/Tactic/LSimp/Elab.lean +++ b/SciLean/Tactic/LSimp/Elab.lean @@ -1,19 +1,4 @@ -/- -Copyright (c) 2020 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura --/ -import Lean.Meta.Tactic.Replace -import Lean.Elab.BuiltinNotation -import Lean.Elab.Tactic.Basic -import Lean.Elab.Tactic.ElabTerm -import Lean.Elab.Tactic.Location -import Lean.Elab.Tactic.Config - -import Lean.Elab.Tactic.Simp - import SciLean.Tactic.LSimp.Main -import SciLean.Tactic.LSimp.Notation namespace SciLean.Tactic.LSimp @@ -22,168 +7,34 @@ open TSyntax.Compat open Lean Meta -def traceSimpCall (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Unit := do - let mut stx := stx - if stx[3].isNone then - stx := stx.setArg 3 (mkNullNode #[mkAtom "only"]) - let mut args := #[] - let mut localsOrStar := some #[] - let lctx ← getLCtx - let env ← getEnv - for (thm, _) in usedSimps.toArray.qsort (·.2 < ·.2) do - match thm with - | .decl declName => -- global definitions in the environment - if env.contains declName && !simpOnlyBuiltins.contains declName then - args := args.push (← `(Parser.Tactic.simpLemma| $(mkIdent (← unresolveNameGlobal declName)):ident)) - | .fvar fvarId => -- local hypotheses in the context - if let some ldecl := lctx.find? fvarId then - localsOrStar := localsOrStar.bind fun locals => - if !ldecl.userName.isInaccessibleUserName && - (lctx.findFromUserName? ldecl.userName).get!.fvarId == ldecl.fvarId then - some (locals.push ldecl.userName) - else - none - -- Note: the `if let` can fail for `simp (config := {contextual := true})` when - -- rewriting with a variable that was introduced in a scope. In that case we just ignore. - | .stx _ thmStx => -- simp theorems provided in the local invocation - args := args.push thmStx - | .other _ => -- Ignore "special" simp lemmas such as constructed by `simp_all`. - pure () -- We can't display them anyway. - if let some locals := localsOrStar then - args := args ++ (← locals.mapM fun id => `(Parser.Tactic.simpLemma| $(mkIdent id):ident)) - else - args := args.push (← `(Parser.Tactic.simpStar| *)) - let argsStx := if args.isEmpty then #[] else #[mkAtom "[", (mkAtom ",").mkSep args, mkAtom "]"] - stx := stx.setArg 4 (mkNullNode argsStx) - logInfoAt stx[0] m!"Try this: {stx}" - - -/-- -`simpLocation ctx discharge? varIdToLemmaId loc` -runs the simplifier at locations specified by `loc`, -using the simp theorems collected in `ctx` -optionally running a discharger specified in `discharge?` on generated subgoals. - -Its primary use is as the implementation of the -`simp [...] at ...` and `simp only [...] at ...` syntaxes, -but can also be used by other tactics when a `Syntax` is not available. - -For many tactics other than the simplifier, -one should use the `withLocation` tactic combinator -when working with a `location`. --/ -def simpLocation (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (loc : Location) : TacticM Simp.UsedSimps := do - match loc with - | Location.targets hyps simplifyTarget => - withMainContext do - let fvarIds ← getFVarIds hyps - go fvarIds simplifyTarget - | Location.wildcard => - withMainContext do - go (← (← getMainGoal).getNondepPropHyps) (simplifyTarget := true) -where - go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Simp.UsedSimps := do - let mvarId ← getMainGoal - let (result?, usedSimps) ← SciLean.Tactic.lsimpGoal mvarId ctx (simplifyTarget := simplifyTarget) (discharge? := discharge?) (fvarIdsToSimp := fvarIdsToSimp) - match result? with - | none => replaceMainGoal [] - | some (_, mvarId) => replaceMainGoal [mvarId] - return usedSimps - - -/- - "simp " (config)? (discharger)? ("only ")? ("[" simpLemma,* "]")? (location)? --/ -@[tactic SciLean.Tactic.LSimp.lsimp] def evalSimp : Tactic := fun stx => do - let { ctx, dischargeWrapper } ← withMainContext <| mkSimpContext stx (eraseLocal := false) - let usedSimps ← dischargeWrapper.with fun discharge? => - simpLocation ctx discharge? (expandOptLocation stx[5]) - if tactic.simp.trace.get (← getOptions) then - traceSimpCall stx usedSimps - -open Lean Elab Tactic Conv in -@[tactic SciLean.Tactic.LSimp.lsimp_conv] def evalSimpConv : Tactic := fun stx => do - let { ctx, dischargeWrapper } ← withMainContext <| mkSimpContext stx (eraseLocal := false) - - let e ← getLhs - let (r, usedSimps) ← dischargeWrapper.with fun discharge? => - SciLean.Tactic.simp e ctx discharge? - - updateLhs r.expr (← r.getProof' e) - - if tactic.simp.trace.get (← getOptions) then - traceSimpCall stx usedSimps - -def dsimpLocation (ctx : Simp.Context) (loc : Location) : TacticM Unit := do - match loc with - | Location.targets hyps simplifyTarget => - withMainContext do - let fvarIds ← getFVarIds hyps - go fvarIds simplifyTarget - | Location.wildcard => - withMainContext do - go (← (← getMainGoal).getNondepPropHyps) (simplifyTarget := true) -where - go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Unit := do - let mvarId ← getMainGoal - let (result?, usedSimps) ← SciLean.Tactic.ldsimpGoal mvarId ctx (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp) - match result? with - | none => replaceMainGoal [] - | some mvarId => replaceMainGoal [mvarId] - if tactic.simp.trace.get (← getOptions) then - traceSimpCall (← getRef) usedSimps - -@[tactic SciLean.Tactic.LSimp.ldsimp] def evalDSimp : Tactic := fun stx => do - let { ctx, .. } ← withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp) - dsimpLocation ctx (expandOptLocation stx[5]) - - -set_option linter.unusedVariables false in -open Lean Elab Tactic Conv in -@[tactic SciLean.Tactic.LSimp.ldsimp_conv] def evalDSimpConv : Tactic := fun stx => do - let { ctx, dischargeWrapper } ← withMainContext <| mkSimpContext stx (eraseLocal := false) - - let e ← getLhs - let (e', usedSimps) ← SciLean.Tactic.dsimp e ctx - - changeLhs e' - - if tactic.simp.trace.get (← getOptions) then - traceSimpCall stx usedSimps - - -example (f : Nat → Nat) : - ( - let a := - let b := f 10 - let x := 5 - let g := hold $ λ n => n + b + 10 - let cd := (3, g (f 42)) - b + cd.1 + g 10 + cd.2 + x - let z := a + 1 - (a*a*z, a+a+z)).1 - = - sorry - := -by - -- ldsimp (config := {zeta := false}) - lsimp (config := {zeta := false}) only - - -- dsimp (config := {zeta := false}) - admit - -example (f : Nat → Nat) : - ( - let a := - let b := f 10 - b + 10 - (a*a, a+a)).1 - = - sorry - := -by - ldsimp (config := {zeta := false}) - -- lsimp (config := {zeta := false}) only - - -- dsimp (config := {zeta := false}) - admit + +def callLSimpAux (e : Expr) (k : Expr → Expr → Array Expr → MetaM α) : MetaM α := do + + let stateRef : IO.Ref Simp.State ← IO.mkRef {} + + let mut simprocs : Simp.Simprocs := {} + simprocs ← simprocs.add ``Mathlib.Meta.FunTrans.fun_trans_simproc false + let r := (lsimp e).run + (Simp.mkDefaultMethodsCore #[simprocs]) {config:={zeta:=false,singlePass:=false},simpTheorems:=#[←getSimpTheorems]} stateRef + + let a ← r.runInMeta (fun r => + k r.expr (r.proof?.getD default) r.vars) + + return a + + +def callLSimp (e : Expr) : MetaM Expr := do + callLSimpAux e (fun e _ vars => do + mkLambdaFVars vars e) + + + +open Lean.Parser.Tactic in +syntax (name:=lsimp_conv) "lsimp" /-(config)? (discharger)? (normalizer)?-/ : conv + + +open Lean Elab Tactic in +@[tactic lsimp_conv] unsafe def lsimpConv : Tactic := fun _ => do + let e ← Conv.getLhs + let e' ← callLSimp e + Conv.updateLhs e' (← mkAppM ``sorryAx #[← mkEq e e', .const ``Bool.false []]) diff --git a/SciLean/Tactic/LSimp/Main.lean b/SciLean/Tactic/LSimp/Main.lean index d6fe0e4b..59f5f56b 100644 --- a/SciLean/Tactic/LSimp/Main.lean +++ b/SciLean/Tactic/LSimp/Main.lean @@ -14,37 +14,15 @@ import Lean.Meta.Tactic.UnifyEq import Lean.Meta.Tactic.Simp.Rewrite import Lean.Meta.Match.Value -import SciLean.Lean.Meta.Basic -import SciLean.Lean.Meta.Structure -import SciLean.Util.Hold +import SciLean.Tactic.LSimp.Types -open Lean Meta Simp +open Lean Meta namespace SciLean.Tactic.LSimp -builtin_initialize congrHypothesisExceptionId : InternalExceptionId ← - registerInternalExceptionId `congrHypothesisFailed -def throwCongrHypothesisFailed : MetaM α := - throw <| Exception.internal congrHypothesisExceptionId -/-- - Helper method for bootstrapping purposes. It disables `arith` if support theorems have not been defined yet. --/ -def Config.updateArith (c : Simp.Config) : CoreM Simp.Config := do - if c.arith then - if (← getEnv).contains ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq then - return c - else - return { c with arith := false } - else - return c - -/-- Return true if `e` is of the form `ofNat n` where `n` is a kernel Nat literal -/ -def isOfNatNatLit (e : Expr) : Bool := - e.isAppOfArity ``OfNat.ofNat 3 && e.appFn!.appArg!.isNatLit - -private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do +private def reduceProjFn? (e : Expr) : LSimpM (Option Expr) := do matchConst e.getAppFn (fun _ => pure none) fun cinfo _ => do match (← getProjectionFnInfo? cinfo.name) with | none => return none @@ -67,7 +45,7 @@ private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do -/ let e? ← withReducibleAndInstances <| unfoldDefinition? e if e?.isSome then - recordSimpTheorem (.decl cinfo.name) + Simp.recordSimpTheorem (.decl cinfo.name) return e? else /- @@ -78,29 +56,24 @@ private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do unless e.getAppNumArgs > projInfo.numParams do return none let major := e.getArg! projInfo.numParams - unless major.isConstructorApp (← getEnv) do + unless (← isConstructorApp major) do return none reduceProjCont? (← withDefault <| unfoldDefinition? e) else -- `structure` projections reduceProjCont? (← unfoldDefinition? e) -private def reduceFVar (cfg : Simp.Config) (thms : SimpTheoremsArray) (e : Expr) : MetaM Expr := do - if cfg.zeta || thms.isLetDeclToUnfold e.fvarId! then - match (← getFVarLocalDecl e).value? with - | some v => return v - | none => return e +private def reduceFVar (cfg : Simp.Config) (thms : SimpTheoremsArray) (e : Expr) : LSimpM Expr := do + let localDecl ← getFVarLocalDecl e + if cfg.zetaDelta || thms.isLetDeclToUnfold e.fvarId! || localDecl.isImplementationDetail then + if !cfg.zetaDelta && thms.isLetDeclToUnfold e.fvarId! then + Simp.recordSimpTheorem (.fvar localDecl.fvarId) + let some v := localDecl.value? | return e + return v else return e -/-- - Return true if `declName` is the name of a definition of the form - ``` - def declName ... := - match ... with - | ... - ``` --/ + private partial def isMatchDef (declName : Name) : CoreM Bool := do let .defnInfo info ← getConstInfo declName | return false return go (← getEnv) info.value @@ -115,15 +88,15 @@ where /-- Try to unfold `e`. -/ -private def unfold? (e : Expr) : SimpM (Option Expr) := do +private def unfold? (e : Expr) : LSimpM (Option Expr) := do let f := e.getAppFn if !f.isConst then return none let fName := f.constName! let ctx ← getContext - let rec unfoldDeclToUnfold? : SimpM (Option Expr) := do + let rec unfoldDeclToUnfold? : LSimpM (Option Expr) := do let options ← getOptions - let cfg ← Simp.getConfig + let cfg ← getConfig -- Support for issue #2042 if cfg.unfoldPartialApp -- If we are unfolding partial applications, ignore issue #2042 -- When smart unfolding is enabled, and `f` supports it, we don't need to worry about issue #2042 @@ -156,8 +129,27 @@ private def unfold? (e : Expr) : SimpM (Option Expr) := do else return none -private def reduceStep (e : Expr) : SimpM Expr := do - let cfg ← Simp.getConfig + +def withNewLemmas {α} (xs : Array Expr) (f : LSimpM α) : LSimpM α := do + if (← getConfig).contextual then + let mut s ← Simp.getSimpTheorems + let mut updated := false + for x in xs do + if (← isProof x) then + s ← s.addTheorem (.fvar x.fvarId!) x + updated := true + if updated then + withSimpTheorems s f + else + f + else + f + + +mutual + +partial def reduceStep (e : Expr) : LSimpM Expr := do + let cfg ← getConfig let f := e.getAppFn if f.isMVar then return (← instantiateMVars e) @@ -176,66 +168,24 @@ private def reduceStep (e : Expr) : SimpM Expr := do if cfg.zeta then if let some (args, _, _, v, b) := e.letFunAppArgs? then return mkAppN (b.instantiate1 v) args + if e.isLet then + return e.letBody!.instantiate1 e.letValue! match (← unfold? e) with | some e' => trace[Meta.Tactic.simp.rewrite] "unfold {mkConst e.getAppFn.constName!}, {e} ==> {e'}" - recordSimpTheorem (.decl e.getAppFn.constName!) + Simp.recordSimpTheorem (.decl e.getAppFn.constName!) return e' | none => return e -private partial def reduce (e : Expr) : SimpM Expr := withIncRecDepth do +partial def reduce (e : Expr) : LSimpM Expr := /- withIncRecDepth -/ do let e' ← reduceStep e if e' == e then return e' else reduce e' -instance : Inhabited (SimpM α) where - default := fun _ _ _ => default -partial def lambdaTelescopeDSimp (e : Expr) (k : Array Expr → Expr → SimpM α) : SimpM α := do - go #[] e -where - go (xs : Array Expr) (e : Expr) : SimpM α := do - match e with - | .lam n d b c => withLocalDecl n c (← dsimp d) fun x => go (xs.push x) (b.instantiate1 x) - | e => k xs e - -inductive SimpLetCase where - | dep -- `let x := v; b` is not equivalent to `(fun x => b) v` - | nondepDepVar -- `let x := v; b` is equivalent to `(fun x => b) v`, but result type depends on `x` - | nondep -- `let x := v; b` is equivalent to `(fun x => b) v`, and result type does not depend on `x` - -def getSimpLetCase (n : Name) (t : Expr) (b : Expr) : MetaM SimpLetCase := do - withLocalDeclD n t fun x => do - let bx := b.instantiate1 x - /- The following step is potentially very expensive when we have many nested let-decls. - TODO: handle a block of nested let decls in a single pass if this becomes a performance problem. -/ - if (← isTypeCorrect bx) then - let bxType ← whnf (← inferType bx) - if (← dependsOn bxType x.fvarId!) then - return SimpLetCase.nondepDepVar - else - return SimpLetCase.nondep - else - return SimpLetCase.dep - -def withNewLemmas {α} (xs : Array Expr) (f : SimpM α) : SimpM α := do - if (← Simp.getConfig).contextual then - let mut s ← getSimpTheorems - let mut updated := false - for x in xs do - if (← isProof x) then - s ← s.addTheorem (.fvar x.fvarId!) x - updated := true - if updated then - withSimpTheorems s f - else - f - else - f - -def simpLit (e : Expr) : SimpM Result := do +partial def simpLit (e : Expr) : LSimpM Result := do match e.natLit? with | some n => /- If `OfNat.ofNat` is marked to be unfolded, we do not pack orphan nat literals as `OfNat.ofNat` applications @@ -246,7 +196,7 @@ def simpLit (e : Expr) : SimpM Result := do return { expr := (← mkNumeral (mkConst ``Nat) n) } | none => return { expr := e } -def simpProj (e : Expr) : SimpM Result := do +partial def simpProj (e : Expr) : LSimpM Result := do match (← reduceProj? e) with | some e => return { expr := e } | none => @@ -262,7 +212,7 @@ def simpProj (e : Expr) : SimpM Result := do else return some motive if let some motive := motive? then - let r ← simp s + let r ← lsimp s let eNew := e.updateProj! r.expr match r.proof? with | none => return { expr := eNew } @@ -270,14 +220,22 @@ def simpProj (e : Expr) : SimpM Result := do let hNew ← mkEqNDRec motive (← mkEqRefl e) h return { expr := eNew, proof? := some hNew } else - return { expr := (← dsimp e) } + return { expr := (← ldsimp e) } -def simpConst (e : Expr) : SimpM Result := +partial def simpConst (e : Expr) : LSimpM Result := return { expr := (← reduce e) } -def simpLambda (e : Expr) : SimpM Result := +partial def lambdaTelescopeDSimp [Inhabited α] (e : Expr) (k : Array Expr → Expr → LSimpM α) : LSimpM α := do + go #[] e +where + go (xs : Array Expr) (e : Expr) : LSimpM α := do + match e with + | .lam n d b c => withLocalDecl n c (← ldsimp d) fun x => go (xs.push x) (b.instantiate1 x) + | e => k xs e + +partial def simpLambda (e : Expr) : LSimpM Result := do withParent e <| lambdaTelescopeDSimp e fun xs e => withNewLemmas xs do - let r ← simp e + let r ← lsimp e let eNew ← mkLambdaFVars xs r.expr match r.proof? with | none => return { expr := eNew } @@ -286,19 +244,19 @@ def simpLambda (e : Expr) : SimpM Result := mkFunExt (← mkLambdaFVars #[x] h) return { expr := eNew, proof? := p } -def simpArrow (e : Expr) : SimpM Result := do +partial def simpArrow (e : Expr) : LSimpM Result := do trace[Debug.Meta.Tactic.simp] "arrow {e}" let p := e.bindingDomain! let q := e.bindingBody! - let rp ← simp p - trace[Debug.Meta.Tactic.simp] "arrow [{(← Simp.getConfig).contextual}] {p} [{← isProp p}] -> {q} [{← isProp q}]" - if (← pure (← Simp.getConfig).contextual <&&> isProp p <&&> isProp q) then + let rp ← lsimp p + trace[Debug.Meta.Tactic.simp] "arrow [{(← getConfig).contextual}] {p} [{← isProp p}] -> {q} [{← isProp q}]" + if (← pure (← getConfig).contextual <&&> isProp p <&&> isProp q) then trace[Debug.Meta.Tactic.simp] "ctx arrow {rp.expr} -> {q}" withLocalDeclD e.bindingName! rp.expr fun h => do - let s ← getSimpTheorems + let s ← Simp.getSimpTheorems let s ← s.addTheorem (.fvar h.fvarId!) h withSimpTheorems s do - let rq ← simp q + let rq ← lsimp q match rq.proof? with | none => mkImpCongr e rp rq | some hq => @@ -319,69 +277,70 @@ def simpArrow (e : Expr) : SimpM Result := do else return { expr := e.updateForallE! rp.expr rq.expr, proof? := (← withDefault <| mkImpCongrCtx (← rp.getProof) hq) } else - mkImpCongr e rp (← simp q) - -def simpForall (e : Expr) : SimpM Result := withParent e do - trace[Debug.Meta.Tactic.simp] "forall {e}" - if e.isArrow then - simpArrow e - else if (← isProp e) then - /- The forall is a proposition. -/ - let domain := e.bindingDomain! - if (← isProp domain) then - /- - The domain of the forall is also a proposition, and we can use `forall_prop_domain_congr` - IF we can simplify the domain. - -/ - let rd ← simp domain - if let some h₁ := rd.proof? then - /- Using - ``` - theorem forall_prop_domain_congr {p₁ p₂ : Prop} {q₁ : p₁ → Prop} {q₂ : p₂ → Prop} - (h₁ : p₁ = p₂) - (h₂ : ∀ a : p₂, q₁ (h₁.substr a) = q₂ a) - : (∀ a : p₁, q₁ a) = (∀ a : p₂, q₂ a) - ``` - Remark: we should consider whether we want to add congruence lemma support for arbitrary `forall`-expressions. - Then, the theroem above can be marked as `@[congr]` and the following code deleted. - -/ - let p₁ := domain - let p₂ := rd.expr - let q₁ := mkLambda e.bindingName! e.bindingInfo! p₁ e.bindingBody! - let result ← withLocalDecl e.bindingName! e.bindingInfo! p₂ fun a => withNewLemmas #[a] do - let prop := mkSort levelZero - let h₁_substr_a := mkApp6 (mkConst ``Eq.substr [levelOne]) prop (mkLambda `x .default prop (mkBVar 0)) p₂ p₁ h₁ a - let q_h₁_substr_a := e.bindingBody!.instantiate1 h₁_substr_a - let rb ← simp q_h₁_substr_a - let h₂ ← mkLambdaFVars #[a] (← rb.getProof) - let q₂ ← mkLambdaFVars #[a] rb.expr - let result ← mkForallFVars #[a] rb.expr - let proof := mkApp6 (mkConst ``forall_prop_domain_congr) p₁ p₂ q₁ q₂ h₁ h₂ - return { expr := result, proof? := proof } - return result - let domain ← dsimp domain - withLocalDecl e.bindingName! e.bindingInfo! domain fun x => withNewLemmas #[x] do - let b := e.bindingBody!.instantiate1 x - let rb ← simp b - let eNew ← mkForallFVars #[x] rb.expr - match rb.proof? with - | none => return { expr := eNew } - | some h => return { expr := eNew, proof? := (← mkForallCongr (← mkLambdaFVars #[x] h)) } - else - return { expr := (← dsimp e) } - -def simpLet (e : Expr) : SimpM Result := do + mkImpCongr e rp (← lsimp q) + +partial def simpForall (e : Expr) : LSimpM Result := return { expr := e } + -- withParent e do + -- trace[Debug.Meta.Tactic.simp] "forall {e}" + -- if e.isArrow then + -- simpArrow e + -- else if (← isProp e) then + -- /- The forall is a proposition. -/ + -- let domain := e.bindingDomain! + -- if (← isProp domain) then + -- /- + -- The domain of the forall is also a proposition, and we can use `forall_prop_domain_congr` + -- IF we can simplify the domain. + -- -/ + -- let rd ← simp domain + -- if let some h₁ := rd.proof? then + -- /- Using + -- ``` + -- theorem forall_prop_domain_congr {p₁ p₂ : Prop} {q₁ : p₁ → Prop} {q₂ : p₂ → Prop} + -- (h₁ : p₁ = p₂) + -- (h₂ : ∀ a : p₂, q₁ (h₁.substr a) = q₂ a) + -- : (∀ a : p₁, q₁ a) = (∀ a : p₂, q₂ a) + -- ``` + -- Remark: we should consider whether we want to add congruence lemma support for arbitrary `forall`-expressions. + -- Then, the theroem above can be marked as `@[congr]` and the following code deleted. + -- -/ + -- let p₁ := domain + -- let p₂ := rd.expr + -- let q₁ := mkLambda e.bindingName! e.bindingInfo! p₁ e.bindingBody! + -- let result ← withLocalDecl e.bindingName! e.bindingInfo! p₂ fun a => withNewLemmas #[a] do + -- let prop := mkSort levelZero + -- let h₁_substr_a := mkApp6 (mkConst ``Eq.substr [levelOne]) prop (mkLambda `x .default prop (mkBVar 0)) p₂ p₁ h₁ a + -- let q_h₁_substr_a := e.bindingBody!.instantiate1 h₁_substr_a + -- let rb ← simp q_h₁_substr_a + -- let h₂ ← mkLambdaFVars #[a] (← rb.getProof) + -- let q₂ ← mkLambdaFVars #[a] rb.expr + -- let result ← mkForallFVars #[a] rb.expr + -- let proof := mkApp6 (mkConst ``forall_prop_domain_congr) p₁ p₂ q₁ q₂ h₁ h₂ + -- return { expr := result, proof? := proof } + -- return result + -- let domain ← dsimp domain + -- withLocalDecl e.bindingName! e.bindingInfo! domain fun x => withNewLemmas #[x] do + -- let b := e.bindingBody!.instantiate1 x + -- let rb ← simp b + -- let eNew ← mkForallFVars #[x] rb.expr + -- match rb.proof? with + -- | none => return { expr := eNew } + -- | some h => return { expr := eNew, proof? := (← mkForallCongr (← mkLambdaFVars #[x] h)) } + -- else + -- return { expr := (← dsimp e) } + +partial def simpLet (e : Expr) : LSimpM Result := do let .letE n t v b _ := e | unreachable! - if (← Simp.getConfig).zeta then + if (← getConfig).zeta then return { expr := b.instantiate1 v } else - match (← getSimpLetCase n t b) with - | SimpLetCase.dep => return { expr := (← dsimp e) } - | SimpLetCase.nondep => - let rv ← simp v + match (← Simp.getSimpLetCase n t b) with + | .dep => return { expr := (← ldsimp e) } + | .nondep => + let rv ← lsimp v withLocalDeclD n t fun x => do let bx := b.instantiate1 x - let rbx ← simp bx + let rbx ← lsimp bx let hb? ← match rbx.proof? with | none => pure none | some h => pure (some (← mkLambdaFVars #[x] h)) @@ -390,11 +349,11 @@ def simpLet (e : Expr) : SimpM Result := do | none, none => return { expr := e' } | some h, none => return { expr := e', proof? := some (← mkLetValCongr (← mkLambdaFVars #[x] rbx.expr) h) } | _, some h => return { expr := e', proof? := some (← mkLetCongr (← rv.getProof) h) } - | SimpLetCase.nondepDepVar => - let v' ← dsimp v + | .nondepDepVar => + let v' ← ldsimp v withLocalDeclD n t fun x => do let bx := b.instantiate1 x - let rbx ← simp bx + let rbx ← lsimp bx let e' := mkLet n t v' (← rbx.expr.abstractM #[x]) match rbx.proof? with | none => return { expr := e' } @@ -402,29 +361,28 @@ def simpLet (e : Expr) : SimpM Result := do let h ← mkLambdaFVars #[x] h return { expr := e', proof? := some (← mkLetBodyCongr v' h) } -@[export lean_dsimp] -private partial def dsimpImpl (e : Expr) : SimpM Expr := do - let cfg ← Simp.getConfig +partial def ldsimp (e : Expr) : LSimpM Expr := do + let cfg ← getConfig unless cfg.dsimp do return e - let pre (e : Expr) : SimpM TransformStep := do - if let Step.visit r ← rewritePre (rflOnly := true) e then - if r.expr != e then - return .visit r.expr + let pre (e : Expr) : LSimpM TransformStep := do + -- if let Step.visit r ← rewritePre (rflOnly := true) e then + -- if r.expr != e then + -- return .visit r.expr return .continue - let post (e : Expr) : SimpM TransformStep := do - if let Step.visit r ← rewritePost (rflOnly := true) e then - if r.expr != e then - return .visit r.expr + let post (e : Expr) : LSimpM TransformStep := do + -- if let Step.visit r ← rewritePost (rflOnly := true) e then + -- if r.expr != e then + -- return .visit r.expr let mut eNew ← reduce e if eNew.isFVar then - eNew ← reduceFVar cfg (← getSimpTheorems) eNew + eNew ← reduceFVar cfg (← Simp.getSimpTheorems) eNew if eNew != e then return .visit eNew else return .done e transform (usedLetOnly := cfg.zeta) e (pre := pre) (post := post) -def visitFn (e : Expr) : SimpM Result := do +partial def visitFn (e : Expr) : LSimpM Result := do let f := e.getAppFn - let fNew ← simp f + let fNew ← lsimp f if fNew.expr == f then return { expr := e } else @@ -436,117 +394,150 @@ def visitFn (e : Expr) : SimpM Result := do proof ← Meta.mkCongrFun proof arg return { expr := eNew, proof? := proof } -def congrDefault (e : Expr) : SimpM Result := do - if let some result ← tryAutoCongrTheorem? e then - result.mkEqTrans (← visitFn result.expr) - else - withParent e <| e.withApp fun f args => do - congrArgs (← simp f) args - -/-- Process the given congruence theorem hypothesis. Return true if it made "progress". -/ -def processCongrHypothesis (h : Expr) : SimpM Bool := do - forallTelescopeReducing (← inferType h) fun xs hType => withNewLemmas xs do - let lhs ← instantiateMVars hType.appFn!.appArg! - let r ← simp lhs - let rhs := hType.appArg! - rhs.withApp fun m zs => do - let val ← mkLambdaFVars zs r.expr - unless (← isDefEq m val) do - throwCongrHypothesisFailed - let mut proof ← r.getProof - if hType.isAppOf ``Iff then - try proof ← mkIffOfEq proof - catch _ => throwCongrHypothesisFailed - unless (← isDefEq h (← mkLambdaFVars xs proof)) do - throwCongrHypothesisFailed - /- We used to return `false` if `r.proof? = none` (i.e., an implicit `rfl` proof) because we - assumed `dsimp` would also be able to simplify the term, but this is not true - for non-trivial user-provided theorems. - Example: - ``` - @[congr] theorem image_congr {f g : α → β} {s : Set α} (h : ∀ a, mem a s → f a = g a) : image f s = image g s := - ... - - example {Γ: Set Nat}: (image (Nat.succ ∘ Nat.succ) Γ) = (image (fun a => a.succ.succ) Γ) := by - simp only [Function.comp_apply] - ``` - `Function.comp_apply` is a `rfl` theorem, but `dsimp` will not apply it because the composition - is not fully applied. See comment at issue #1113 - - Thus, we have an extra check now if `xs.size > 0`. TODO: refine this test. - -/ - return r.proof?.isSome || (xs.size > 0 && lhs != r.expr) - -/-- Try to rewrite `e` children using the given congruence theorem -/ -def trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : SimpM (Option Result) := withNewMCtxDepth do - trace[Debug.Meta.Tactic.simp.congr] "{c.theoremName}, {e}" - let thm ← mkConstWithFreshMVarLevels c.theoremName - let (xs, bis, type) ← forallMetaTelescopeReducing (← inferType thm) - if c.hypothesesPos.any (· ≥ xs.size) then - return none - let isIff := type.isAppOf ``Iff - let lhs := type.appFn!.appArg! - let rhs := type.appArg! - let numArgs := lhs.getAppNumArgs - let mut e := e - let mut extraArgs := #[] - if e.getAppNumArgs > numArgs then - let args := e.getAppArgs - e := mkAppN e.getAppFn args[:numArgs] - extraArgs := args[numArgs:].toArray - if (← isDefEq lhs e) then - let mut modified := false - for i in c.hypothesesPos do - let x := xs[i]! - try - if (← processCongrHypothesis x) then - modified := true - catch _ => - trace[Meta.Tactic.simp.congr] "processCongrHypothesis {c.theoremName} failed {← inferType x}" - -- Remark: we don't need to check ex.isMaxRecDepth anymore since `try .. catch ..` - -- does not catch runtime exceptions by default. - return none - unless modified do - trace[Meta.Tactic.simp.congr] "{c.theoremName} not modified" - return none - unless (← synthesizeArgs (.decl c.theoremName) xs bis) do - trace[Meta.Tactic.simp.congr] "{c.theoremName} synthesizeArgs failed" - return none - let eNew ← instantiateMVars rhs - let mut proof ← instantiateMVars (mkAppN thm xs) - if isIff then - try proof ← mkAppM ``propext #[proof] - catch _ => return none - if (← hasAssignableMVar proof <||> hasAssignableMVar eNew) then - trace[Meta.Tactic.simp.congr] "{c.theoremName} has unassigned metavariables" - return none - congrArgs { expr := eNew, proof? := proof } extraArgs +partial def congrArgs (r : Result) (args : Array Expr) : LSimpM Result := do + if args.isEmpty then + return r else - return none + let cfg ← getConfig + let infos := (← getFunInfoNArgs r.expr args.size).paramInfo + let mut r := r + let mut i := 0 + for arg in args do + if h : i < infos.size then + trace[Debug.Meta.Tactic.simp] "app [{i}] {infos.size} {arg} hasFwdDeps: {infos[i].hasFwdDeps}" + let info := infos[i] + if cfg.ground && info.isInstImplicit then + -- We don't visit instance implicit arguments when we are reducing ground terms. + -- Motivation: many instance implicit arguments are ground, and it does not make sense + -- to reduce them if the parent term is not ground. + -- TODO: consider using it as the default behavior. + -- We have considered it at https://github.com/leanprover/lean4/pull/3151 + r ← mkCongrFun r arg + else if !info.hasFwdDeps then + r ← mkCongr r (← lsimp arg) + else if (← whnfD (← inferType r.expr)).isArrow then + r ← mkCongr r (← lsimp arg) + else + r ← mkCongrFun r (← ldsimp arg) + else if (← whnfD (← inferType r.expr)).isArrow then + r ← mkCongr r (← lsimp arg) + else + r ← mkCongrFun r (← ldsimp arg) + i := i + 1 + return r -def congr (e : Expr) : SimpM Result := do - let f := e.getAppFn - if f.isConst then - let congrThms ← getSimpCongrTheorems - let cs := congrThms.get f.constName! - for c in cs do - match (← trySimpCongrTheorem? c e) with - | none => pure () - | some r => return r - congrDefault e - else + +partial def congrDefault (e : Expr) : LSimpM Result := do + -- if let some result ← tryAutoCongrTheorem? e then + -- result.mkEqTrans (← visitFn result.expr) + -- else + withParent e <| e.withApp fun f args => do + congrArgs (← lsimp f) args + +-- /-- Process the given congruence theorem hypothesis. Return true if it made "progress". -/ +-- partial def processCongrHypothesis (h : Expr) : LSimpM Bool := do +-- forallTelescopeReducing (← inferType h) fun xs hType => withNewLemmas xs do +-- let lhs ← instantiateMVars hType.appFn!.appArg! +-- let r ← simp lhs +-- let rhs := hType.appArg! +-- rhs.withApp fun m zs => do +-- let val ← mkLambdaFVars zs r.expr +-- unless (← isDefEq m val) do +-- throwCongrHypothesisFailed +-- let mut proof ← r.getProof +-- if hType.isAppOf ``Iff then +-- try proof ← mkIffOfEq proof +-- catch _ => throwCongrHypothesisFailed +-- unless (← isDefEq h (← mkLambdaFVars xs proof)) do +-- throwCongrHypothesisFailed +-- /- We used to return `false` if `r.proof? = none` (i.e., an implicit `rfl` proof) because we +-- assumed `dsimp` would also be able to simplify the term, but this is not true +-- for non-trivial user-provided theorems. +-- Example: +-- ``` +-- @[congr] theorem image_congr {f g : α → β} {s : Set α} (h : ∀ a, mem a s → f a = g a) : image f s = image g s := +-- ... + +-- example {Γ: Set Nat}: (image (Nat.succ ∘ Nat.succ) Γ) = (image (fun a => a.succ.succ) Γ) := by +-- simp only [Function.comp_apply] +-- ``` +-- `Function.comp_apply` is a `rfl` theorem, but `dsimp` will not apply it because the composition +-- is not fully applied. See comment at issue #1113 + +-- Thus, we have an extra check now if `xs.size > 0`. TODO: refine this test. +-- -/ +-- return r.proof?.isSome || (xs.size > 0 && lhs != r.expr) + +-- /-- Try to rewrite `e` children using the given congruence theorem -/ +-- partial def trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : LSimpM (Option Result) := withNewMCtxDepth do +-- trace[Debug.Meta.Tactic.simp.congr] "{c.theoremName}, {e}" +-- let thm ← mkConstWithFreshMVarLevels c.theoremName +-- let (xs, bis, type) ← forallMetaTelescopeReducing (← inferType thm) +-- if c.hypothesesPos.any (· ≥ xs.size) then +-- return none +-- let isIff := type.isAppOf ``Iff +-- let lhs := type.appFn!.appArg! +-- let rhs := type.appArg! +-- let numArgs := lhs.getAppNumArgs +-- let mut e := e +-- let mut extraArgs := #[] +-- if e.getAppNumArgs > numArgs then +-- let args := e.getAppArgs +-- e := mkAppN e.getAppFn args[:numArgs] +-- extraArgs := args[numArgs:].toArray +-- if (← isDefEq lhs e) then +-- let mut modified := false +-- for i in c.hypothesesPos do +-- let x := xs[i]! +-- try +-- if (← processCongrHypothesis x) then +-- modified := true +-- catch _ => +-- trace[Meta.Tactic.simp.congr] "processCongrHypothesis {c.theoremName} failed {← inferType x}" +-- -- Remark: we don't need to check ex.isMaxRecDepth anymore since `try .. catch ..` +-- -- does not catch runtime exceptions by default. +-- return none +-- unless modified do +-- trace[Meta.Tactic.simp.congr] "{c.theoremName} not modified" +-- return none +-- unless (← synthesizeArgs (.decl c.theoremName) bis xs) do +-- trace[Meta.Tactic.simp.congr] "{c.theoremName} synthesizeArgs failed" +-- return none +-- let eNew ← instantiateMVars rhs +-- let mut proof ← instantiateMVars (mkAppN thm xs) +-- if isIff then +-- try proof ← mkAppM ``propext #[proof] +-- catch _ => return none +-- if (← hasAssignableMVar proof <||> hasAssignableMVar eNew) then +-- trace[Meta.Tactic.simp.congr] "{c.theoremName} has unassigned metavariables" +-- return none +-- congrArgs { expr := eNew, proof? := proof } extraArgs +-- else +-- return none + +partial def congr (e : Expr) : LSimpM Result := do + -- let f := e.getAppFn + -- if f.isConst then + -- let congrThms ← getSimpCongrTheorems + -- let cs := congrThms.get f.constName! + -- for c in cs do + -- match (← trySimpCongrTheorem? c e) with + -- | none => pure () + -- | some r => return r + -- congrDefault e + -- else congrDefault e -def simpApp (e : Expr) : SimpM Result := do - if isOfNatNatLit e then +partial def simpApp (e : Expr) : LSimpM Result := do + if Simp.isOfNatNatLit e then -- Recall that we expand "orphan" kernel nat literals `n` into `ofNat n` return { expr := e } else congr e -def simpStep (e : Expr) : SimpM Result := do +partial def simpStep (e : Expr) : LSimpM Result := do match e with - | .mdata m e => let r ← simp e; return { r with expr := mkMData m r.expr } + | .mdata m e => let r ← lsimp e; return { r with expr := mkMData m r.expr } | .proj .. => simpProj e | .app .. => simpApp e | .lam .. => simpLambda e @@ -557,20 +548,23 @@ def simpStep (e : Expr) : SimpM Result := do | .sort .. => return { expr := e } | .lit .. => simpLit e | .mvar .. => return { expr := (← instantiateMVars e) } - | .fvar .. => return { expr := (← reduceFVar (← Simp.getConfig) (← getSimpTheorems) e) } + | .fvar .. => return { expr := (← reduceFVar (← getConfig) (← Simp.getSimpTheorems) e) } + -def cacheResult (e : Expr) (cfg : Config) (r : Result) : SimpM Result := do +partial def cacheResult (e : Expr) (cfg : Simp.Config) (r : Result) : LSimpM Result := do if cfg.memoize && r.cache then let ctx ← readThe Simp.Context let dischargeDepth := ctx.dischargeDepth modify fun s => { s with cache := s.cache.insert e { r with dischargeDepth } } return r -partial def simpLoop (e : Expr) : SimpM Result := do - let cfg ← Simp.getConfig + +partial def simpLoop (e : Expr) : LSimpM Result := /- withIncRecDepth -/ do + let cfg ← getConfig if (← get).numSteps > cfg.maxSteps then throwError "simp failed, maximum number of steps exceeded" else + checkSystem "simp" modify fun s => { s with numSteps := s.numSteps + 1 } match (← pre e) with | .done r => cacheResult e cfg r @@ -578,7 +572,7 @@ partial def simpLoop (e : Expr) : SimpM Result := do | .continue none => visitPreContinue cfg { expr := e } | .continue (some r) => visitPreContinue cfg r where - visitPreContinue (cfg : Config) (r : Result) : SimpM Result := do + visitPreContinue (cfg : Simp.Config) (r : Result) : LSimpM Result := do let eNew ← reduceStep r.expr if eNew != r.expr then let r := { r with expr := eNew } @@ -586,252 +580,35 @@ where else let r ← r.mkEqTrans (← simpStep r.expr) visitPost cfg r - visitPost (cfg : Config) (r : Result) : SimpM Result := do + visitPost (cfg : Simp.Config) (r : Result) : LSimpM Result := do match (← post r.expr) with | .done r' => cacheResult e cfg (← r.mkEqTrans r') | .continue none => visitPostContinue cfg r | .visit r' | .continue (some r') => visitPostContinue cfg (← r.mkEqTrans r') - visitPostContinue (cfg : Config) (r : Result) : SimpM Result := do + visitPostContinue (cfg : Simp.Config) (r : Result) : LSimpM Result := do let mut r := r unless cfg.singlePass || e == r.expr do r ← r.mkEqTrans (← simpLoop r.expr) cacheResult e cfg r -@[export lean_simp] -def simpImpl (e : Expr) : SimpM Result := withIncRecDepth do - checkSystem "simp" +partial def lsimp (e : Expr) : LSimpM Result := do +-- withIncRecDepth do if (← isProof e) then return { expr := e } go where - go : SimpM Result := do - let cfg ← Simp.getConfig - if cfg.memoize then - let cache := (← get).cache - if let some result := cache.find? e then - /- - If the result was cached at a dischargeDepth > the current one, it may not be valid. - See issue #1234 - -/ - if result.dischargeDepth ≤ (← readThe Simp.Context).dischargeDepth then - return result + go : LSimpM Result := do + -- let cfg ← getConfig + -- if cfg.memoize then + -- let cache := (← get).cache + -- if let some result := cache.find? e then + -- /- + -- If the result was cached at a dischargeDepth > the current one, it may not be valid. + -- See issue #1234 + -- -/ + -- if result.dischargeDepth ≤ (← readThe Simp.Context).dischargeDepth then + -- return result trace[Meta.Tactic.simp.heads] "{repr e.toHeadIndex}" simpLoop e -@[inline] def withSimpConfig (ctx : Context) (x : MetaM α) : MetaM α := - withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible x - -def main (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods : Methods := {}) : MetaM (Result × UsedSimps) := do - let ctx := { ctx with config := (← ctx.config.updateArith) } - withSimpConfig ctx do withCatchingRuntimeEx do - try - withoutCatchingRuntimeEx do - let (r, s) ← simp e methods.toMethodsRef ctx |>.run { usedTheorems := usedSimps } - trace[Meta.Tactic.simp.numSteps] "{s.numSteps}" - return (r, s.usedTheorems) - catch ex => - if ex.isRuntime then throwNestedTacticEx `simp ex else throw ex - -def dsimpMain (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods : Methods := {}) : MetaM (Expr × UsedSimps) := do - withSimpConfig ctx do withCatchingRuntimeEx do - try - withoutCatchingRuntimeEx do - let (r, s) ← dsimp e methods.toMethodsRef ctx |>.run { usedTheorems := usedSimps } - pure (r, s.usedTheorems) - catch ex => - if ex.isRuntime then throwNestedTacticEx `dsimp ex else throw ex - -end Simp -open Simp (UsedSimps SimprocsArray) - -def simp (e : Expr) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) - (usedSimps : UsedSimps := {}) : MetaM (Simp.Result × UsedSimps) := do profileitM Exception "simp" (← getOptions) do - match discharge? with - | none => Simp.main e ctx usedSimps (methods := Simp.mkDefaultMethodsCore simprocs) - | some d => Simp.main e ctx usedSimps (methods := Simp.mkMethods simprocs d) - -def dsimp (e : Expr) (ctx : Simp.Context) - (usedSimps : UsedSimps := {}) : MetaM (Expr × UsedSimps) := do profileitM Exception "dsimp" (← getOptions) do - Simp.dsimpMain e ctx usedSimps (methods := Simp.mkDefaultMethodsCore {}) - -/-- See `simpTarget`. This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/ -def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) - (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do - let target ← instantiateMVars (← mvarId.getType) - let (r, usedSimps) ← simp target ctx simprocs discharge? usedSimps - if mayCloseGoal && r.expr.consumeMData.isConstOf ``True then - match r.proof? with - | some proof => mvarId.assign (← mkOfEqTrue proof) - | none => mvarId.assign (mkConst ``True.intro) - return (none, usedSimps) - else - return (← applySimpResultToTarget mvarId target r, usedSimps) - -/-- - Simplify the given goal target (aka type). Return `none` if the goal was closed. Return `some mvarId'` otherwise, - where `mvarId'` is the simplified new goal. -/ -def simpTarget (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) - (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := - mvarId.withContext do - mvarId.checkNotAssigned `simp - simpTargetCore mvarId ctx simprocs discharge? mayCloseGoal usedSimps - -/-- - Apply the result `r` for `prop` (which is inhabited by `proof`). Return `none` if the goal was closed. Return `some (proof', prop')` - otherwise, where `proof' : prop'` and `prop'` is the simplified `prop`. - - This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/ -def applySimpResultToProp (mvarId : MVarId) (proof : Expr) (prop : Expr) (r : Simp.Result) (mayCloseGoal := true) : MetaM (Option (Expr × Expr)) := do - if mayCloseGoal && r.expr.consumeMData.isConstOf ``False then - match r.proof? with - | some eqProof => mvarId.assign (← mkFalseElim (← mvarId.getType) (← mkEqMP eqProof proof)) - | none => mvarId.assign (← mkFalseElim (← mvarId.getType) proof) - return none - else - match r.proof? with - | some eqProof => return some ((← mkEqMP eqProof proof), r.expr) - | none => - if r.expr != prop then - return some ((← mkExpectedTypeHint proof r.expr), r.expr) - else - return some (proof, r.expr) - -def applySimpResultToFVarId (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result) (mayCloseGoal : Bool) : MetaM (Option (Expr × Expr)) := do - let localDecl ← fvarId.getDecl - applySimpResultToProp mvarId (mkFVar fvarId) localDecl.type r mayCloseGoal - -/-- - Simplify `prop` (which is inhabited by `proof`). Return `none` if the goal was closed. Return `some (proof', prop')` - otherwise, where `proof' : prop'` and `prop'` is the simplified `prop`. - - This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/ -def simpStep (mvarId : MVarId) (proof : Expr) (prop : Expr) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) - (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option (Expr × Expr) × UsedSimps) := do - let (r, usedSimps) ← simp prop ctx simprocs discharge? usedSimps - return (← applySimpResultToProp mvarId proof prop r (mayCloseGoal := mayCloseGoal), usedSimps) - -def applySimpResultToLocalDeclCore (mvarId : MVarId) (fvarId : FVarId) (r : Option (Expr × Expr)) : MetaM (Option (FVarId × MVarId)) := do - match r with - | none => return none - | some (value, type') => - let localDecl ← fvarId.getDecl - if localDecl.type != type' then - let mvarId ← mvarId.assert localDecl.userName type' value - let mvarId ← mvarId.tryClear localDecl.fvarId - let (fvarId, mvarId) ← mvarId.intro1P - return some (fvarId, mvarId) - else - return some (fvarId, mvarId) - -/-- - Simplify `simp` result to the given local declaration. Return `none` if the goal was closed. - This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/ -def applySimpResultToLocalDecl (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result) (mayCloseGoal : Bool) : MetaM (Option (FVarId × MVarId)) := do - if r.proof?.isNone then - -- New result is definitionally equal to input. Thus, we can avoid creating a new variable if there are dependencies - let mvarId ← mvarId.replaceLocalDeclDefEq fvarId r.expr - if mayCloseGoal && r.expr.consumeMData.isConstOf ``False then - mvarId.assign (← mkFalseElim (← mvarId.getType) (mkFVar fvarId)) - return none - else - return some (fvarId, mvarId) - else - applySimpResultToLocalDeclCore mvarId fvarId (← applySimpResultToFVarId mvarId fvarId r mayCloseGoal) - -def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) - (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option (FVarId × MVarId) × UsedSimps) := do - mvarId.withContext do - mvarId.checkNotAssigned `simp - let type ← instantiateMVars (← fvarId.getType) - let (r, usedSimps) ← simpStep mvarId (mkFVar fvarId) type ctx simprocs discharge? mayCloseGoal usedSimps - return (← applySimpResultToLocalDeclCore mvarId fvarId r, usedSimps) - -def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) - (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) - (usedSimps : UsedSimps := {}) : MetaM (Option (Array FVarId × MVarId) × UsedSimps) := do - mvarId.withContext do - mvarId.checkNotAssigned `simp - let mut mvarIdNew := mvarId - let mut toAssert := #[] - let mut replaced := #[] - let mut usedSimps := usedSimps - for fvarId in fvarIdsToSimp do - let localDecl ← fvarId.getDecl - let type ← instantiateMVars localDecl.type - let ctx := { ctx with simpTheorems := ctx.simpTheorems.eraseTheorem (.fvar localDecl.fvarId) } - let (r, usedSimps') ← simp type ctx simprocs discharge? usedSimps - usedSimps := usedSimps' - match r.proof? with - | some _ => match (← applySimpResultToProp mvarIdNew (mkFVar fvarId) type r) with - | none => return (none, usedSimps) - | some (value, type) => toAssert := toAssert.push { userName := localDecl.userName, type := type, value := value } - | none => - if r.expr.consumeMData.isConstOf ``False then - mvarIdNew.assign (← mkFalseElim (← mvarIdNew.getType) (mkFVar fvarId)) - return (none, usedSimps) - -- TODO: if there are no forwards dependencies we may consider using the same approach we used when `r.proof?` is a `some ...` - -- Reason: it introduces a `mkExpectedTypeHint` - mvarIdNew ← mvarIdNew.replaceLocalDeclDefEq fvarId r.expr - replaced := replaced.push fvarId - if simplifyTarget then - match (← simpTarget mvarIdNew ctx simprocs discharge? (usedSimps := usedSimps)) with - | (none, usedSimps') => return (none, usedSimps') - | (some mvarIdNew', usedSimps') => mvarIdNew := mvarIdNew'; usedSimps := usedSimps' - let (fvarIdsNew, mvarIdNew') ← mvarIdNew.assertHypotheses toAssert - mvarIdNew := mvarIdNew' - let toClear := fvarIdsToSimp.filter fun fvarId => !replaced.contains fvarId - mvarIdNew ← mvarIdNew.tryClearMany toClear - if ctx.config.failIfUnchanged && mvarId == mvarIdNew then - throwError "simp made no progress" - return (some (fvarIdsNew, mvarIdNew), usedSimps) - -def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) - (usedSimps : UsedSimps := {}) : MetaM (TacticResultCNM × UsedSimps) := mvarId.withContext do - let mut ctx := ctx - for h in (← getPropHyps) do - let localDecl ← h.getDecl - let proof := localDecl.toExpr - let simpTheorems ← ctx.simpTheorems.addTheorem (.fvar h) proof - ctx := { ctx with simpTheorems } - match (← simpTarget mvarId ctx simprocs discharge? (usedSimps := usedSimps)) with - | (none, usedSimps) => return (TacticResultCNM.closed, usedSimps) - | (some mvarId', usedSimps') => - if (← mvarId.getType) == (← mvarId'.getType) then - return (TacticResultCNM.noChange, usedSimps) - else - return (TacticResultCNM.modified mvarId', usedSimps') - -def dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) - (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do - mvarId.withContext do - mvarId.checkNotAssigned `simp - let mut mvarIdNew := mvarId - let mut usedSimps : UsedSimps := usedSimps - for fvarId in fvarIdsToSimp do - let type ← instantiateMVars (← fvarId.getType) - let (typeNew, usedSimps') ← dsimp type ctx - usedSimps := usedSimps' - if typeNew.consumeMData.isConstOf ``False then - mvarIdNew.assign (← mkFalseElim (← mvarIdNew.getType) (mkFVar fvarId)) - return (none, usedSimps) - if typeNew != type then - mvarIdNew ← mvarIdNew.replaceLocalDeclDefEq fvarId typeNew - if simplifyTarget then - let target ← mvarIdNew.getType - let (targetNew, usedSimps') ← dsimp target ctx usedSimps - usedSimps := usedSimps' - if targetNew.consumeMData.isConstOf ``True then - mvarIdNew.assign (mkConst ``True.intro) - return (none, usedSimps) - if let some (_, lhs, rhs) := targetNew.consumeMData.eq? then - if (← withReducible <| isDefEq lhs rhs) then - mvarIdNew.assign (← mkEqRefl lhs) - return (none, usedSimps) - if target != targetNew then - mvarIdNew ← mvarIdNew.replaceTargetDefEq targetNew - pure () -- FIXME: bug in do notation if this is removed? - if ctx.config.failIfUnchanged && mvarId == mvarIdNew then - throwError "dsimp made no progress" - return (some mvarIdNew, usedSimps) - -end Lean.Meta +end diff --git a/SciLean/Tactic/LSimp/Test.lean b/SciLean/Tactic/LSimp/Test.lean new file mode 100644 index 00000000..24321c42 --- /dev/null +++ b/SciLean/Tactic/LSimp/Test.lean @@ -0,0 +1,120 @@ +import SciLean.Tactic.LSimp.Elab +import SciLean.Util.RewriteBy +import SciLean.Core + +import ProofWidgets.Component.HtmlDisplay +import ProofWidgets.Component.Recharts + +open Lean ProofWidgets Recharts + + +-- def plot (x y : Array Float) : Html := + +open scoped ProofWidgets.Jsx in +def plot (data : Array (Float×Float)) : Html := Id.run do + + let mut jsonData : Array Json := #[] + for (x,y) in data do + jsonData := jsonData.push (json% {x: $(toJson x) , y: $(toJson y), z: $(toJson (y/2))}); + +

+ + + + + + +

+ +#html plot #[(1,1),(2,4),(3,9),(5,25)] + +open SciLean Lean Meta Qq + +set_default_scalar Float + + +inductive ExprType where + | v1 | v2 | v3 + +def testExpressionAux (n : Nat) (k : Array Expr → MetaM α) (t : ExprType := .v1) : MetaM α := do + match n with + | 0 => + withLocalDeclD `x q(Float) fun x => k #[x] + | n+1 => + testExpressionAux n fun xs => do + let val ← + match t with + | .v1 => + mkAppFoldlM ``HMul.hMul xs + | .v2 => + if xs.size == 1 then + mkAppFoldlM ``HMul.hMul #[xs[0]!, xs[0]!] + else + mkAppFoldlM ``HMul.hMul xs[xs.size-2:xs.size] + | .v3 => + if xs.size == 1 then + mkAppFoldlM ``HMul.hMul #[xs[0]!, xs[0]!] + else + mkAppFoldlM ``HMul.hMul #[xs[xs.size-1]!, xs[0]!] + withLetDecl ((`x).appendAfter (toString n)) q(Float) val fun x => do + k (xs.push x) + + +def testExpression (n : Nat) : MetaM Q(Float → Float) := + testExpressionAux n (fun xs => mkLambdaFVars xs xs[xs.size-1]!) + + +#eval show MetaM Unit from do + IO.println (← ppExpr (← testExpression 8)) + + +#check (0 + 1 + 0) rewrite_by lsimp + + +structure MeasureData where + time : Aesop.Nanos + numSteps : Nat + +open SciLean.Tactic.LSimp +def callLSimpData (e : Expr) : MetaM (Expr×MeasureData) := do + + let stateRef : IO.Ref Simp.State ← IO.mkRef {} + + let mut simprocs : Simp.Simprocs := {} + simprocs ← simprocs.add ``Mathlib.Meta.FunTrans.fun_trans_simproc false + let r := (lsimp e).run + (Simp.mkDefaultMethodsCore #[simprocs]) {config:={zeta:=false,singlePass:=false},simpTheorems:=#[←getSimpTheorems]} stateRef + + let (e,t) ← Aesop.time <| r.runInMeta (fun r => mkLambdaFVars r.vars r.expr) + + + return (e, { time := t, numSteps := (← stateRef.get).numSteps }) + + + +def measureOnTestExpression (n : Nat) : MetaM (Array MeasureData) := do + + + + for i in [0:n] do + let e := q(cderiv Float $(← testExpression i)) + let (e',data) ← callLSimpData e + + IO.println s!"{← ppExpr e}\n==>\n{← ppExpr e'}\n" + + + return #[] + + + +#eval show MetaM Unit from do + let _ ← measureOnTestExpression 10 + +set_option trace.Meta.Tactic.fun_trans true +set_option trace.Meta.Tactic.fun_trans.step true + +#check (cderiv Float (fun x : Float => x * x)) rewrite_by lsimp; lsimp + + +#check (cderiv Float (fun x : Float => let x1 := x * x; x1*x1)) + rewrite_by fun_trans (config:={zeta:=false}) [Tactic.lift_lets_simproc] diff --git a/SciLean/Tactic/LSimp/Types.lean b/SciLean/Tactic/LSimp/Types.lean new file mode 100644 index 00000000..e93e735b --- /dev/null +++ b/SciLean/Tactic/LSimp/Types.lean @@ -0,0 +1,145 @@ +import Lean +import Lean.Util.Trace + +import SciLean.Lean.Meta.Basic + +import SciLean.Tactic.GTrans.MetaLCtxM + +import Mathlib.Tactic.FunTrans.Core +import Mathlib.Tactic.FunTrans.Elab + +open Lean Meta + + +namespace SciLean.Tactic.LSimp + + +---------------------------------------------------------------------------------------------------- +-- Result ------------------------------------------------------------------------------------------ +---------------------------------------------------------------------------------------------------- + +structure Result where + expr : Expr + proof? : Option Expr := none + vars : Array Expr := #[] + dischargeDepth : UInt32 := 0 + cache : Bool := true + deriving Inhabited + + +def mkEqTransOptProofResult (h? : Option Expr) (cache : Bool) (r : Result) : MetaM Result := + match h?, cache with + | none, true => return r + | none, false => return { r with cache := false } + | some p₁, cache => match r.proof? with + | none => return { r with proof? := some p₁, cache := cache && r.cache } + | some p₂ => return { r with proof? := (← Meta.mkEqTrans p₁ p₂), cache := cache && r.cache } + +def Result.mkEqTrans (r₁ r₂ : Result) : MetaM Result := + mkEqTransOptProofResult r₁.proof? r₁.cache {r₂ with vars := r₁.vars ++ r₂.vars} + +def _root_.Lean.Meta.Simp.Result.toLResult (s : Simp.Result) : Result := + { expr := s.expr, + proof? := s.proof?, + vars := #[], + dischargeDepth := s.dischargeDepth, + cache := s.cache } + +def Result.getProof (r : Result) : MetaLCtxM Expr := + match r.proof? with + | some p => return p + | none => mkEqRefl r.expr + +def mkCongrFun (r : Result) (a : Expr) : MetaM Result := + match r.proof? with + | none => return { expr := mkApp r.expr a, proof? := none, vars := r.vars } + | some h => return { expr := mkApp r.expr a, proof? := (← Meta.mkCongrFun h a), vars := r.vars } + +def mkCongr (r₁ r₂ : Result) : MetaM Result := + let e := mkApp r₁.expr r₂.expr + match r₁.proof?, r₂.proof? with + | none, none => return { expr := e, proof? := none, vars := r₁.vars ++ r₂.vars } + | some h, none => return { expr := e, proof? := (← Meta.mkCongrFun h r₂.expr), vars := r₁.vars ++ r₂.vars } + | none, some h => return { expr := e, proof? := (← Meta.mkCongrArg r₁.expr h), vars := r₁.vars ++ r₂.vars } + | some h₁, some h₂ => return { expr := e, proof? := (← Meta.mkCongr h₁ h₂), vars := r₁.vars ++ r₂.vars } + +def mkImpCongr (src : Expr) (r₁ r₂ : Result) : MetaLCtxM Result := do + let e := src.updateForallE! r₁.expr r₂.expr + match r₁.proof?, r₂.proof? with + | none, none => return { expr := e, proof? := none } + | _, _ => return { expr := e, proof? := (← Meta.mkImpCongr (← r₁.getProof) (← r₂.getProof)) } -- TODO specialize if bottleneck + + +---------------------------------------------------------------------------------------------------- +-- LSimpM ------------------------------------------------------------------------------------------ +---------------------------------------------------------------------------------------------------- + +abbrev LSimpM := ReaderT Simp.Methods $ ReaderT Simp.Context $ StateRefT Simp.State MetaLCtxM + +instance : MonadLift SimpM LSimpM where + monadLift x := fun m c s => x m.toMethodsRef c s + +def LSimpM.runInSimp (x : LSimpM X) (k : X → MetaM Y) : SimpM Y := do + fun mths ctx s => do + let m : Simp.Methods := Simp.MethodsRef.toMethods mths + (x m ctx s).runInMeta k + +instance : Inhabited (LSimpM α) where + default := fun _ _ _ _ _ _ => default + +---------------------------------------------------------------------------------------------------- +-- LSimp forward declaration ----------------------------------------------------------------------- +---------------------------------------------------------------------------------------------------- + +-- @[extern "scilean_lsimp"] +-- opaque lsimp (e : Expr) : LSimpM Result + +-- @[extern "scilean_ldsimp"] +-- opaque ldsimp (e : Expr) : LSimpM Expr + + +---------------------------------------------------------------------------------------------------- +-- Step -------------------------------------------------------------------------------------------- +---------------------------------------------------------------------------------------------------- + +inductive Step where + | done (r : Result) + | visit (e : Result) + | continue (e? : Option Result := none) + deriving Inhabited + +def mkEqTransResultStep (r : Result) (s : Step) : MetaM Step := + match s with + | .done r' => return .done (← mkEqTransOptProofResult r.proof? r.cache r') + | .visit r' => return .visit (← mkEqTransOptProofResult r.proof? r.cache r') + | .continue none => return .continue r + | .continue (some r') => return .continue (some (← mkEqTransOptProofResult r.proof? r.cache r')) + +def _root_.Lean.Meta.Simp.Step.toLStep (s : Simp.Step) : Step := + match s with + | .done r => LSimp.Step.done r.toLResult + | .visit r => LSimp.Step.visit r.toLResult + | .continue r => LSimp.Step.continue (r.map (·.toLResult)) + + +---------------------------------------------------------------------------------------------------- +-- Utility Functions ------------------------------------------------------------------------------- +---------------------------------------------------------------------------------------------------- + +def pre (e : Expr) : LSimpM Step := do + Simp.getMethods >>= (·.pre e) >>= fun s => pure s.toLStep + +def post (e : Expr) : LSimpM Step := do + Simp.getMethods >>= (·.post e) >>= fun s => pure s.toLStep + +@[inline] def getContext : LSimpM Simp.Context := + readThe Simp.Context + +def getConfig : LSimpM Simp.Config := + return (← getContext).config + +@[inline] def withParent (parent : Expr) (f : LSimpM α) : LSimpM α := + withTheReader Simp.Context (fun ctx => { ctx with parent? := parent }) f + +@[inline] def withSimpTheorems (s : SimpTheoremsArray) (x : LSimpM α) : LSimpM α := do + savingCache <| withTheReader Simp.Context (fun ctx => { ctx with simpTheorems := s }) x