- done: Lean.Expr → Lean.TransformStep
- visit: Lean.Expr → Lean.TransformStep
def
Lean.Core.transform
{m : Type → Type}
[inst : Monad m]
[inst : MonadLiftT Lean.CoreM m]
[inst : MonadControlT Lean.CoreM m]
(input : Lean.Expr)
(pre : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.visit e))
(post : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.done e))
:
Equations
- Lean.Core.transform input pre post = let inst := { }; let inst_1 := { monadLift := fun {α} x => liftM (liftM x) }; (fun visit => Lean.MonadCacheT.run (visit input)) (Lean.Core.transform.visit pre post inst inst_1)
partial def
Lean.Core.transform.visit
{m : Type → Type}
[inst : Monad m]
[inst : MonadControlT Lean.CoreM m]
(pre : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.visit e))
(post : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.done e))
(inst : STWorld IO.RealWorld m)
(inst : MonadLiftT (ST IO.RealWorld) m)
(e : Lean.Expr)
:
partial def
Lean.Core.transform.visit.visitPost
{m : Type → Type}
[inst : Monad m]
[inst : MonadControlT Lean.CoreM m]
(pre : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.visit e))
(post : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.done e))
(inst : STWorld IO.RealWorld m)
(inst : MonadLiftT (ST IO.RealWorld) m)
(e : Lean.Expr)
:
Equations
- Lean.Core.betaReduce e = Lean.Core.transform e (fun e => pure (Lean.TransformStep.visit (Lean.Expr.headBeta e))) fun e => pure (Lean.TransformStep.done e)
def
Lean.Meta.transform
{m : Type → Type}
[inst : Monad m]
[inst : MonadLiftT Lean.MetaM m]
[inst : MonadControlT Lean.MetaM m]
(input : Lean.Expr)
(pre : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.visit e))
(post : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.done e))
:
Equations
- Lean.Meta.transform input pre post = let inst := { }; let inst_1 := { monadLift := fun {α} x => liftM (liftM x) }; (fun visit => Lean.MonadCacheT.run (visit input)) (Lean.Meta.transform.visit pre post inst inst_1)
partial def
Lean.Meta.transform.visit
{m : Type → Type}
[inst : Monad m]
[inst : MonadLiftT Lean.MetaM m]
[inst : MonadControlT Lean.MetaM m]
(pre : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.visit e))
(post : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.done e))
(inst : STWorld IO.RealWorld m)
(inst : MonadLiftT (ST IO.RealWorld) m)
(e : Lean.Expr)
:
partial def
Lean.Meta.transform.visit.visitPost
{m : Type → Type}
[inst : Monad m]
[inst : MonadLiftT Lean.MetaM m]
[inst : MonadControlT Lean.MetaM m]
(pre : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.visit e))
(post : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.done e))
(inst : STWorld IO.RealWorld m)
(inst : MonadLiftT (ST IO.RealWorld) m)
(e : Lean.Expr)
:
partial def
Lean.Meta.transform.visit.visitLambda
{m : Type → Type}
[inst : Monad m]
[inst : MonadLiftT Lean.MetaM m]
[inst : MonadControlT Lean.MetaM m]
(pre : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.visit e))
(post : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.done e))
(inst : STWorld IO.RealWorld m)
(inst : MonadLiftT (ST IO.RealWorld) m)
(fvars : Array Lean.Expr)
(e : Lean.Expr)
:
partial def
Lean.Meta.transform.visit.visitForall
{m : Type → Type}
[inst : Monad m]
[inst : MonadLiftT Lean.MetaM m]
[inst : MonadControlT Lean.MetaM m]
(pre : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.visit e))
(post : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.done e))
(inst : STWorld IO.RealWorld m)
(inst : MonadLiftT (ST IO.RealWorld) m)
(fvars : Array Lean.Expr)
(e : Lean.Expr)
:
partial def
Lean.Meta.transform.visit.visitLet
{m : Type → Type}
[inst : Monad m]
[inst : MonadLiftT Lean.MetaM m]
[inst : MonadControlT Lean.MetaM m]
(pre : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.visit e))
(post : optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.done e))
(inst : STWorld IO.RealWorld m)
(inst : MonadLiftT (ST IO.RealWorld) m)
(fvars : Array Lean.Expr)
(e : Lean.Expr)
:
Equations
- Lean.Meta.zetaReduce e = do let lctx ← Lean.getLCtx let pre : Lean.Expr → Lean.CoreM Lean.TransformStep := fun e => match e with | Lean.Expr.fvar fvarId x => match Lean.LocalContext.find? lctx fvarId with | none => pure (Lean.TransformStep.done e) | some localDecl => match Lean.LocalDecl.value? localDecl with | some value => pure (Lean.TransformStep.visit value) | x => pure (Lean.TransformStep.done e) | e => if Lean.Expr.hasFVar e = true then pure (Lean.TransformStep.visit e) else pure (Lean.TransformStep.done e) liftM (Lean.Core.transform e pre fun e => pure (Lean.TransformStep.done e))