max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2021-01-05 07:57:09 -08:00
parent 597304db95
commit 544a6cbb94
4 changed files with 39 additions and 39 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Meta/Reduce.lean
View file

@ -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)

37
src/Lean/Meta/Tactic/Simp/Main.lean
View file

@ -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

10
src/Lean/Meta/Tactic/Simp/Rewrite.lean
View file

@ -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"))

29
src/Lean/Meta/Tactic/Simp/Types.lean
View file

@ -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