Lean.Meta.Closure

Lean.Meta.Closure.visitLevel f u = if (!Lean.Level.hasMVar u && !Lean.Level.hasParam u) = true then pure u else do let s ← get match Std.HashMap.find? s.visitedLevel u with | some v => pure v | none => do let v ← f u modify fun s => { visitedLevel := Std.HashMap.insert s.visitedLevel u v, visitedExpr := s.visitedExpr, levelParams := s.levelParams, nextLevelIdx := s.nextLevelIdx, levelArgs := s.levelArgs, newLocalDecls := s.newLocalDecls, newLocalDeclsForMVars := s.newLocalDeclsForMVars, newLetDecls := s.newLetDecls, nextExprIdx := s.nextExprIdx, exprMVarArgs := s.exprMVarArgs, exprFVarArgs := s.exprFVarArgs, toProcess := s.toProcess } pure v

source

@[inline]

def Lean.Meta.Closure.visitExpr (f : Lean.Expr → Lean.Meta.Closure.ClosureM Lean.Expr) (e : Lean.Expr) :

Lean.Meta.Closure.ClosureM Lean.Expr

Equations

Lean.Meta.Closure.visitExpr f e = if (!Lean.Expr.hasLevelParam e && !Lean.Expr.hasFVar e && !Lean.Expr.hasMVar e) = true then pure e else do let s ← get match Std.HashMap.find? s.visitedExpr { val := e } with | some r => pure r | none => do let r ← f e modify fun s => { visitedLevel := s.visitedLevel, visitedExpr := Std.HashMap.insert s.visitedExpr { val := e } r, levelParams := s.levelParams, nextLevelIdx := s.nextLevelIdx, levelArgs := s.levelArgs, newLocalDecls := s.newLocalDecls, newLocalDeclsForMVars := s.newLocalDeclsForMVars, newLetDecls := s.newLetDecls, nextExprIdx := s.nextExprIdx, exprMVarArgs := s.exprMVarArgs, exprFVarArgs := s.exprFVarArgs, toProcess := s.toProcess } pure r

source

def Lean.Meta.Closure.mkNewLevelParam (u : Lean.Level) :

Lean.Meta.Closure.ClosureM Lean.Level

Equations

Lean.Meta.Closure.mkNewLevelParam u = do let s ← get let p : Lean.Name := Lean.Name.appendIndexAfter `u s.nextLevelIdx modify fun s => { visitedLevel := s.visitedLevel, visitedExpr := s.visitedExpr, levelParams := Array.push s.levelParams p, nextLevelIdx := s.nextLevelIdx + 1, levelArgs := Array.push s.levelArgs u, newLocalDecls := s.newLocalDecls, newLocalDeclsForMVars := s.newLocalDeclsForMVars, newLetDecls := s.newLetDecls, nextExprIdx := s.nextExprIdx, exprMVarArgs := s.exprMVarArgs, exprFVarArgs := s.exprFVarArgs, toProcess := s.toProcess } pure (Lean.mkLevelParam p)

source

partial def Lean.Meta.Closure.collectLevelAux :

Lean.Level → Lean.Meta.Closure.ClosureM Lean.Level

source

def Lean.Meta.Closure.collectLevel (u : Lean.Level) :

Lean.Meta.Closure.ClosureM Lean.Level

Equations

Lean.Meta.Closure.collectLevel u = Lean.Meta.Closure.visitLevel Lean.Meta.Closure.collectLevelAux u

source

def Lean.Meta.Closure.preprocess (e : Lean.Expr) :

Lean.Meta.Closure.ClosureM Lean.Expr

Equations

Lean.Meta.Closure.preprocess e = do let e ← liftM (Lean.Meta.instantiateMVars e) let ctx ← read let _do_jp : Unit → Lean.Meta.Closure.ClosureM Lean.Expr := fun y => pure e if (!ctx.zeta) = true then do let y ← liftM (Lean.Meta.check e) _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

def Lean.Meta.Closure.mkNextUserName :

Lean.Meta.Closure.ClosureM Lean.Name

Equations

Lean.Meta.Closure.mkNextUserName = do let s ← get let n : Lean.Name := Lean.Name.appendIndexAfter `_x s.nextExprIdx modify fun s => { visitedLevel := s.visitedLevel, visitedExpr := s.visitedExpr, levelParams := s.levelParams, nextLevelIdx := s.nextLevelIdx, levelArgs := s.levelArgs, newLocalDecls := s.newLocalDecls, newLocalDeclsForMVars := s.newLocalDeclsForMVars, newLetDecls := s.newLetDecls, nextExprIdx := s.nextExprIdx + 1, exprMVarArgs := s.exprMVarArgs, exprFVarArgs := s.exprFVarArgs, toProcess := s.toProcess } pure n

source

def Lean.Meta.Closure.pushToProcess (elem : Lean.Meta.Closure.ToProcessElement) :

Lean.Meta.Closure.ClosureM Unit

Equations

Lean.Meta.Closure.pushToProcess elem = modify fun s => { visitedLevel := s.visitedLevel, visitedExpr := s.visitedExpr, levelParams := s.levelParams, nextLevelIdx := s.nextLevelIdx, levelArgs := s.levelArgs, newLocalDecls := s.newLocalDecls, newLocalDeclsForMVars := s.newLocalDeclsForMVars, newLetDecls := s.newLetDecls, nextExprIdx := s.nextExprIdx, exprMVarArgs := s.exprMVarArgs, exprFVarArgs := s.exprFVarArgs, toProcess := Array.push s.toProcess elem }

source

partial def Lean.Meta.Closure.collectExprAux (e : Lean.Expr) :

Lean.Meta.Closure.ClosureM Lean.Expr

source

def Lean.Meta.Closure.collectExpr (e : Lean.Expr) :

Lean.Meta.Closure.ClosureM Lean.Expr

Equations

Lean.Meta.Closure.collectExpr e = do let e ← Lean.Meta.Closure.preprocess e Lean.Meta.Closure.visitExpr Lean.Meta.Closure.collectExprAux e

source

partial def Lean.Meta.Closure.pickNextToProcessAux (lctx : Lean.LocalContext) (i : Nat) (toProcess : Array Lean.Meta.Closure.ToProcessElement) (elem : Lean.Meta.Closure.ToProcessElement) :

Lean.Meta.Closure.ToProcessElement × Array Lean.Meta.Closure.ToProcessElement

source

def Lean.Meta.Closure.pickNextToProcess? :

Lean.Meta.Closure.ClosureM (Option Lean.Meta.Closure.ToProcessElement)

Equations

Lean.Meta.Closure.pickNextToProcess? = do let lctx ← Lean.getLCtx let s ← get if Array.isEmpty s.toProcess = true then pure none else modifyGet fun s => let elem := Array.back s.toProcess; let toProcess := Array.pop s.toProcess; let x := Lean.Meta.Closure.pickNextToProcessAux lctx 0 toProcess elem; match x with | (elem, toProcess) => (some elem, { visitedLevel := s.visitedLevel, visitedExpr := s.visitedExpr, levelParams := s.levelParams, nextLevelIdx := s.nextLevelIdx, levelArgs := s.levelArgs, newLocalDecls := s.newLocalDecls, newLocalDeclsForMVars := s.newLocalDeclsForMVars, newLetDecls := s.newLetDecls, nextExprIdx := s.nextExprIdx, exprMVarArgs := s.exprMVarArgs, exprFVarArgs := s.exprFVarArgs, toProcess := toProcess })

source

def Lean.Meta.Closure.pushFVarArg (e : Lean.Expr) :

Lean.Meta.Closure.ClosureM Unit

Equations

Lean.Meta.Closure.pushFVarArg e = modify fun s => { visitedLevel := s.visitedLevel, visitedExpr := s.visitedExpr, levelParams := s.levelParams, nextLevelIdx := s.nextLevelIdx, levelArgs := s.levelArgs, newLocalDecls := s.newLocalDecls, newLocalDeclsForMVars := s.newLocalDeclsForMVars, newLetDecls := s.newLetDecls, nextExprIdx := s.nextExprIdx, exprMVarArgs := s.exprMVarArgs, exprFVarArgs := Array.push s.exprFVarArgs e, toProcess := s.toProcess }

source

def Lean.Meta.Closure.pushLocalDecl (newFVarId : Lean.FVarId) (userName : Lean.Name) (type : Lean.Expr) (bi : optParam Lean.BinderInfo Lean.BinderInfo.default) :

Lean.Meta.Closure.ClosureM Unit

Equations

Lean.Meta.Closure.pushLocalDecl newFVarId userName type bi = do let type ← Lean.Meta.Closure.collectExpr type modify fun s => { visitedLevel := s.visitedLevel, visitedExpr := s.visitedExpr, levelParams := s.levelParams, nextLevelIdx := s.nextLevelIdx, levelArgs := s.levelArgs, newLocalDecls := Array.push s.newLocalDecls (Lean.LocalDecl.cdecl default newFVarId userName type bi), newLocalDeclsForMVars := s.newLocalDeclsForMVars, newLetDecls := s.newLetDecls, nextExprIdx := s.nextExprIdx, exprMVarArgs := s.exprMVarArgs, exprFVarArgs := s.exprFVarArgs, toProcess := s.toProcess }

source

partial def Lean.Meta.Closure.process :

Lean.Meta.Closure.ClosureM Unit

source

@[inline]

def Lean.Meta.Closure.mkBinding (isLambda : Bool) (decls : Array Lean.LocalDecl) (b : Lean.Expr) :

Lean.Expr

Equations

Lean.Meta.Closure.mkBinding isLambda decls b = let xs := Array.map Lean.LocalDecl.toExpr decls; let b := Lean.Expr.abstract b xs; Nat.foldRev (fun i b => let decl := Array.getOp decls i; match decl with | Lean.LocalDecl.cdecl x x_1 n ty bi => let ty := Lean.Expr.abstractRange ty i xs; if isLambda = true then Lean.mkLambda n bi ty b else Lean.mkForall n bi ty b | Lean.LocalDecl.ldecl x x_1 n ty val nonDep => if Lean.Expr.hasLooseBVar b 0 = true then let ty := Lean.Expr.abstractRange ty i xs; let val := Lean.Expr.abstractRange val i xs; Lean.mkLet n ty val b nonDep else Lean.Expr.lowerLooseBVars b 1 1) (Array.size decls) b

source

def Lean.Meta.Closure.mkLambda (decls : Array Lean.LocalDecl) (b : Lean.Expr) :

Lean.Expr

Equations

Lean.Meta.Closure.mkLambda decls b = Lean.Meta.Closure.mkBinding true decls b

source

def Lean.Meta.Closure.mkForall (decls : Array Lean.LocalDecl) (b : Lean.Expr) :

Lean.Expr

Equations

Lean.Meta.Closure.mkForall decls b = Lean.Meta.Closure.mkBinding false decls b

source

structure Lean.Meta.Closure.MkValueTypeClosureResult :

Type

levelParams : Array Lean.Name
type : Lean.Expr
value : Lean.Expr
levelArgs : Array Lean.Level
exprArgs : Array Lean.Expr

source

def Lean.Meta.Closure.mkValueTypeClosureAux (type : Lean.Expr) (value : Lean.Expr) :

Lean.Meta.Closure.ClosureM (Lean.Expr × Lean.Expr)

Equations

Lean.Meta.Closure.mkValueTypeClosureAux type value = do liftM Lean.Meta.resetZetaFVarIds Lean.Meta.withTrackingZeta do let type ← Lean.Meta.Closure.collectExpr type let value ← Lean.Meta.Closure.collectExpr value Lean.Meta.Closure.process pure (type, value)

source

def Lean.Meta.Closure.mkValueTypeClosure (type : Lean.Expr) (value : Lean.Expr) (zeta : Bool) :

Lean.MetaM Lean.Meta.Closure.MkValueTypeClosureResult

Equations

Lean.Meta.Closure.mkValueTypeClosure type value zeta = do let discr ← StateRefT'.run (ReaderT.run (Lean.Meta.Closure.mkValueTypeClosureAux type value) { zeta := zeta }) { visitedLevel := ∅, visitedExpr := ∅, levelParams := #[], nextLevelIdx := 1, levelArgs := #[], newLocalDecls := #[], newLocalDeclsForMVars := #[], newLetDecls := #[], nextExprIdx := 1, exprMVarArgs := #[], exprFVarArgs := #[], toProcess := #[] } let x : (Lean.Expr × Lean.Expr) × Lean.Meta.Closure.State := discr match x with | ((type, value), s) => let newLocalDecls := Array.reverse s.newLocalDecls ++ s.newLocalDeclsForMVars; let newLetDecls := Array.reverse s.newLetDecls; let type := Lean.Meta.Closure.mkForall newLocalDecls (Lean.Meta.Closure.mkForall newLetDecls type); let value := Lean.Meta.Closure.mkLambda newLocalDecls (Lean.Meta.Closure.mkLambda newLetDecls value); pure { levelParams := s.levelParams, type := type, value := value, levelArgs := s.levelArgs, exprArgs := Array.reverse s.exprFVarArgs ++ s.exprMVarArgs }

source

def Lean.Meta.mkAuxDefinition (name : Lean.Name) (type : Lean.Expr) (value : Lean.Expr) (zeta : optParam Bool false) (compile : optParam Bool true) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkAuxDefinition name type value zeta compile = let cls := `Meta.debug; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM Lean.Expr := fun y => do let result ← Lean.Meta.Closure.mkValueTypeClosure type value zeta let env ← Lean.getEnv let decl : Lean.Declaration := Lean.Declaration.defnDecl { toConstantVal := { name := name, levelParams := Array.toList result.levelParams, type := result.type }, value := result.value, hints := Lean.ReducibilityHints.regular (Lean.getMaxHeight env result.value + 1), safety := if (Lean.Environment.hasUnsafe env result.type || Lean.Environment.hasUnsafe env result.value) = true then Lean.DefinitionSafety.unsafe else Lean.DefinitionSafety.safe } let cls : Lean.Name := `Meta.debug let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM Lean.Expr := fun y => do Lean.addDecl decl let _do_jp : Unit → Lean.MetaM Lean.Expr := fun y => pure (Lean.mkAppN (Lean.mkConst name (Array.toList result.levelArgs)) result.exprArgs) if compile = true then do let y ← Lean.compileDecl decl _do_jp y else do let y ← pure PUnit.unit _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData name ++ Lean.toMessageData " : " ++ Lean.toMessageData result.type ++ Lean.toMessageData " := " ++ Lean.toMessageData result.value ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData name ++ Lean.toMessageData " : " ++ Lean.toMessageData type ++ Lean.toMessageData " := " ++ Lean.toMessageData value ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

def Lean.Meta.mkAuxDefinitionFor (name : Lean.Name) (value : Lean.Expr) (zeta : optParam Bool false) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkAuxDefinitionFor name value zeta = do let type ← Lean.Meta.inferType value let type : Lean.Expr := Lean.Expr.headBeta type Lean.Meta.mkAuxDefinition name type value zeta true