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

fix: another instance of the binder cache issue

Browse source 
See issue #439
This commit is contained in:
Leonardo de Moura 2021-05-05 10:43:15 -07:00
parent 6303c134a9
commit 660c49840f
1 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/Lean/Meta/Transform.lean
View file

@ -33,9 +33,9 @@ partial def transform {m} [Monad m] [MonadLiftT CoreM m] [MonadControlT CoreM m]
: m Expr :=
let inst : STWorld IO.RealWorld m := ⟨⟩
let inst : MonadLiftT (ST IO.RealWorld) m := { monadLift := fun x => liftM (m := CoreM) (liftM (m := ST IO.RealWorld) x) }
let rec visit (e : Expr) : MonadCacheT Expr Expr m Expr :=
checkCache e fun _ => Core.withIncRecDepth do
let rec visitPost (e : Expr) : MonadCacheT Expr Expr m Expr := do
let rec visit (e : Expr) : MonadCacheT ExprStructEq Expr m Expr :=
checkCache { val := e : ExprStructEq } fun _ => Core.withIncRecDepth do
let rec visitPost (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do
match (← post e) with
| TransformStep.done e => pure e
| TransformStep.visit e => visit e
@ -68,31 +68,31 @@ partial def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m]
: m Expr :=
let inst : STWorld IO.RealWorld m := ⟨⟩
let inst : MonadLiftT (ST IO.RealWorld) m := { monadLift := fun x => liftM (m := MetaM) (liftM (m := ST IO.RealWorld) x) }
let rec visit (e : Expr) : MonadCacheT Expr Expr m Expr :=
checkCache e fun _ => Meta.withIncRecDepth do
let rec visitPost (e : Expr) : MonadCacheT Expr Expr m Expr := do
let rec visit (e : Expr) : MonadCacheT ExprStructEq Expr m Expr :=
checkCache { val := e : ExprStructEq } fun _ => Meta.withIncRecDepth do
let rec visitPost (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do
match (← post e) with
| TransformStep.done e => pure e
| TransformStep.visit e => visit e
let rec visitLambda (fvars : Array Expr) (e : Expr) : MonadCacheT Expr Expr m Expr := do
let rec visitLambda (fvars : Array Expr) (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do
match e with
| Expr.lam n d b c =>
withLocalDecl n c.binderInfo (← visit (d.instantiateRev fvars)) fun x =>
visitLambda (fvars.push x) b
| e => visitPost (← mkLambdaFVars fvars (← visit (e.instantiateRev fvars)))
let rec visitForall (fvars : Array Expr) (e : Expr) : MonadCacheT Expr Expr m Expr := do
let rec visitForall (fvars : Array Expr) (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do
match e with
| Expr.forallE n d b c =>
withLocalDecl n c.binderInfo (← visit (d.instantiateRev fvars)) fun x =>
visitForall (fvars.push x) b
| e => visitPost (← mkForallFVars fvars (← visit (e.instantiateRev fvars)))
let rec visitLet (fvars : Array Expr) (e : Expr) : MonadCacheT Expr Expr m Expr := do
let rec visitLet (fvars : Array Expr) (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do
match e with
| Expr.letE n t v b _ =>
withLetDecl n (← visit (t.instantiateRev fvars)) (← visit (v.instantiateRev fvars)) fun x =>
visitLet (fvars.push x) b
| e => visitPost (← mkLetFVars fvars (← visit (e.instantiateRev fvars)))
let visitApp (e : Expr) : MonadCacheT Expr Expr m Expr :=
let visitApp (e : Expr) : MonadCacheT ExprStructEq Expr m Expr :=
e.withApp fun f args => do
visitPost (mkAppN (← visit f) (← args.mapM visit))
match (← pre e) with