From 544a6cbb9485813dd8422de4aa795c1a590a99ea Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 5 Jan 2021 07:57:09 -0800 Subject: [PATCH] chore: cleanup --- src/Lean/Meta/Reduce.lean | 2 +- src/Lean/Meta/Tactic/Simp/Main.lean | 37 +++++++++++++------------- src/Lean/Meta/Tactic/Simp/Rewrite.lean | 10 +++---- src/Lean/Meta/Tactic/Simp/Types.lean | 29 ++++++++++---------- 4 files changed, 39 insertions(+), 39 deletions(-) diff --git a/src/Lean/Meta/Reduce.lean b/src/Lean/Meta/Reduce.lean index e80518b618..bbc1359b30 100644 --- a/src/Lean/Meta/Reduce.lean +++ b/src/Lean/Meta/Reduce.lean @@ -28,7 +28,7 @@ partial def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : Meta if !explicitOnly || info.isExplicit then args ← args.modifyM i visit else - args ← args.modifyM i visit + args ← args.modifyM i visit pure (mkAppN f args) | Expr.lam .. => lambdaTelescope e fun xs b => do mkLambdaFVars xs (← visit b) | Expr.forallE .. => forallTelescope e fun xs b => do mkForallFVars xs (← visit b) diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index 7476bffccb..d25ba97dde 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/src/Lean/Meta/Tactic/Simp/Main.lean @@ -80,10 +80,10 @@ private partial def reduce (cfg : Config) (e : Expr) : MetaM Expr := withIncRecD | none => pure () return e -private partial def dsimp (e : Expr) : M σ Expr := do +private partial def dsimp (e : Expr) : M Expr := do return e -- TODO -partial def simp {σ} (e : Expr) : M σ Result := withIncRecDepth do +partial def simp (e : Expr) : M Result := withIncRecDepth do let cfg ← getConfig if cfg.memoize then if let some result := (← get).cache.find? e then @@ -91,7 +91,7 @@ partial def simp {σ} (e : Expr) : M σ Result := withIncRecDepth do simpLoop { expr := e } where - simpLoop (r : Result) : M σ Result := do + simpLoop (r : Result) : M Result := do let cfg ← getConfig if (← get).numSteps > cfg.maxSteps then throwError! "simp failed, maximum number of steps exceeded" @@ -112,7 +112,7 @@ where else simpLoop r - simpStep (e : Expr) : M σ Result := do + simpStep (e : Expr) : M Result := do match e with | Expr.mdata _ e _ => simp e | Expr.proj .. => pure { expr := (← reduceProj e) } @@ -127,7 +127,7 @@ where | Expr.mvar .. => pure { expr := (← instantiateMVars e) } | Expr.fvar .. => pure { expr := (← reduceFVar (← getConfig) e) } - simpApp (e : Expr) : M σ Result := do + simpApp (e : Expr) : M Result := do let e ← reduce (← getConfig) e if !e.isApp then simp e @@ -145,7 +145,7 @@ where i := i + 1 return r - withNewLemmas (xs : Array Expr) (f : M σ Result) : M σ Result := do + withNewLemmas (xs : Array Expr) (f : M Result) : M Result := do if (← getConfig).contextual then let mut s ← getSimpLemmas let mut updated := false @@ -160,17 +160,18 @@ where else f - simpLambda (e : Expr) : M σ Result := - withParent e <| lambdaTelescope e fun xs e => withNewLemmas xs do + simpLambda (e : Expr) : M Result := + withParent e $ lambdaTelescope e fun xs e => withNewLemmas xs do let r ← simp e + let eNew ← mkLambdaFVars xs r.expr match r.proof? with - | none => return { expr := (← mkLambdaFVars xs r.expr) } + | none => return { expr := eNew } | some h => let p ← xs.foldrM (init := h) fun x h => do mkFunExt (← mkLambdaFVars #[x] h) - return { expr := (← mkLambdaFVars xs r.expr), proof? := p } + return { expr := eNew, proof? := p } - simpArrow (e : Expr) : M σ Result := do + simpArrow (e : Expr) : M Result := do trace[Meta.Tactic.simp]! "arrow {e}" let p := e.bindingDomain! let q := e.bindingBody! @@ -191,7 +192,7 @@ where else mkImpCongr rp (← simp q) - simpForall (e : Expr) : M σ Result := withParent e do + simpForall (e : Expr) : M Result := withParent e do trace[Meta.Tactic.simp]! "forall {e}" if e.isArrow then simpArrow e @@ -206,7 +207,7 @@ where else return { expr := (← dsimp e) } - simpLet (e : Expr) : M σ Result := do + simpLet (e : Expr) : M Result := do if (← getConfig).zeta then match e with | Expr.letE _ _ v b _ => return { expr := b.instantiate1 v } @@ -215,21 +216,21 @@ where -- TODO: simplify nondependent let-decls return { expr := (← dsimp e) } - cacheResult (cfg : Config) (r : Result) : M σ Result := do + cacheResult (cfg : Config) (r : Result) : M Result := do if cfg.memoize then modify fun s => { s with cache := s.cache.insert e r } return r -def main (e : Expr) (s : σ) (config : Config := {}) (methods : Methods σ := {}) (simpLemmas : SimpLemmas := {}) : MetaM Result := do +def main (e : Expr) (config : Config := {}) (methods : Methods := {}) (simpLemmas : SimpLemmas := {}) : MetaM Result := do withReducible do - simp e methods { config := config, simpLemmas := simpLemmas } |>.run' { user := s } + simp e methods { config := config, simpLemmas := simpLemmas } |>.run' {} end Simp def simp (e : Expr) (config : Simp.Config := {}) (simpLemmas : SimpLemmas := {}) : MetaM Simp.Result := do - let discharge? (e : Expr) : SimpM Unit (Option Expr) := return none -- TODO: use simp, and add config option + let discharge? (e : Expr) : SimpM (Option Expr) := return none -- TODO: use simp, and add config option let pre := (Simp.preDefault · discharge?) let post := (Simp.postDefault · discharge?) - Simp.main e () (config := config) (methods := { pre := pre, post := post, discharge? := discharge? }) (simpLemmas := simpLemmas) + Simp.main e (config := config) (methods := { pre := pre, post := post, discharge? := discharge? }) (simpLemmas := simpLemmas) end Lean.Meta diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean index c6ce9f657b..a23165e939 100644 --- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean +++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean @@ -11,7 +11,7 @@ namespace Lean.Meta.Simp /- Remark: the parameter tag is used for creating trace messages. It is irrelevant otherwise. -/ -def rewrite (e : Expr) (s : DiscrTree SimpLemma) (discharge? : Expr → SimpM σ (Option Expr)) (tag : String) : SimpM σ Result := do +def rewrite (e : Expr) (s : DiscrTree SimpLemma) (discharge? : Expr → SimpM (Option Expr)) (tag : String) : SimpM Result := do let lemmas ← s.getMatch e if lemmas.isEmpty then trace[Meta.Tactic.simp]! "no lemmas found for {tag}-rewriting {e}" @@ -37,7 +37,7 @@ where | SimpLemmaKind.eq => return type.appArg! | SimpLemmaKind.iff => return type.appArg! - synthesizeArgs (lemma : SimpLemma) (xs : Array Expr) (bis : Array BinderInfo) : SimpM σ Bool := do + synthesizeArgs (lemma : SimpLemma) (xs : Array Expr) (bis : Array BinderInfo) : SimpM Bool := do for x in xs, bi in bis do let type ← inferType x if bi.isInstImplicit then @@ -67,7 +67,7 @@ where | SimpLemmaKind.pos => mkEqTrue proof | SimpLemmaKind.neg => mkEqFalse proof - tryLemma? (lemma : SimpLemma) : SimpM σ (Option Result) := + tryLemma? (lemma : SimpLemma) : SimpM (Option Result) := withNewMCtxDepth do let val ← lemma.getValue let type ← inferType val @@ -90,11 +90,11 @@ where trace[Meta.Tactic.simp.unify]! "{lemma}, failed to unify {lhs} with {e}" return none -def preDefault (e : Expr) (discharge? : Expr → SimpM σ (Option Expr)) : SimpM σ Step := do +def preDefault (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do let lemmas ← (← read).simpLemmas return Step.visit (← rewrite e lemmas.pre discharge? (tag := "pre")) -def postDefault (e : Expr) (discharge? : Expr → SimpM σ (Option Expr)) : SimpM σ Step := do +def postDefault (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do let lemmas ← (← read).simpLemmas return Step.visit (← rewrite e lemmas.post discharge? (tag := "post")) diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean index df8105609c..e260b92b24 100644 --- a/src/Lean/Meta/Tactic/Simp/Types.lean +++ b/src/Lean/Meta/Tactic/Simp/Types.lean @@ -21,12 +21,11 @@ structure Context where parent? : Option Expr := none simpLemmas : SimpLemmas -structure State (σ : Type) where - user : σ -- user state +structure State where cache : Cache := {} numSteps : Nat := 0 -abbrev SimpM (σ : Type) := ReaderT Context $ StateRefT (State σ) $ MetaM +abbrev SimpM := ReaderT Context $ StateRefT State MetaM inductive Step where | visit : Result → Step @@ -36,33 +35,33 @@ def Step.result : Step → Result | Step.visit r => r | Step.done r => r -structure Methods (σ : Type) where - pre : Expr → SimpM σ Step := fun e => return Step.visit { expr := e } - post : Expr → SimpM σ Step := fun e => return Step.done { expr := e } - discharge? : Expr → SimpM σ (Option Expr) := fun e => return none +structure Methods where + pre : Expr → SimpM Step := fun e => return Step.visit { expr := e } + post : Expr → SimpM Step := fun e => return Step.done { expr := e } + discharge? : Expr → SimpM (Option Expr) := fun e => return none /- Internal monad -/ -abbrev M (σ : Type) := ReaderT (Methods σ) $ SimpM σ +abbrev M := ReaderT Methods SimpM -def pre (e : Expr) : M σ Step := do +def pre (e : Expr) : M Step := do (← read).pre e -def post (e : Expr) : M σ Step := do +def post (e : Expr) : M Step := do (← read).post e -def discharge? (e : Expr) : M σ (Option Expr) := do +def discharge? (e : Expr) : M (Option Expr) := do (← read).discharge? e -def getConfig : M σ Config := +def getConfig : M Config := return (← readThe Context).config -@[inline] def withParent (parent : Expr) (f : M σ α) : M σ α := +@[inline] def withParent (parent : Expr) (f : M α) : M α := withTheReader Context (fun ctx => { ctx with parent? := parent }) f -def getSimpLemmas : M σ SimpLemmas := +def getSimpLemmas : M SimpLemmas := return (← readThe Context).simpLemmas -@[inline] def withSimpLemmas (s : SimpLemmas) (x : M σ α) : M σ α := do +@[inline] def withSimpLemmas (s : SimpLemmas) (x : M α) : M α := do let cacheSaved := (← get).cache modify fun s => { s with cache := {} } try