Lean.Compiler.InitAttr

source

@[extern lean_run_mod_init]

unsafe constant Lean.runModInit (mod : Lean.Name) :

IO Bool

source

@[extern lean_run_init]

unsafe constant Lean.runInit (env : Lean.Environment) (opts : Lean.Options) (decl : Lean.Name) (initDecl : Lean.Name) :

IO Unit

source

unsafe def Lean.registerInitAttrUnsafe (attrName : Lean.Name) (runAfterImport : Bool) :

IO (Lean.ParametricAttribute Lean.Name)

Equations

Lean.registerInitAttrUnsafe attrName runAfterImport = Lean.registerParametricAttribute { toAttributeImplCore := { name := attrName, descr := "initialization procedure for global references", applicationTime := Lean.AttributeApplicationTime.afterTypeChecking }, getParam := fun declName stx => do let decl ← Lean.getConstInfo declName let a ← Lean.Attribute.Builtin.getIdent? stx match a with | some initFnName => do let initFnName ← Lean.resolveGlobalConstNoOverload initFnName let initDecl ← Lean.getConstInfo initFnName match Lean.getIOTypeArg (Lean.ConstantInfo.type initDecl) with | none => Lean.throwError (Lean.toMessageData "initialization function '" ++ Lean.toMessageData initFnName ++ Lean.toMessageData "' must have type of the form `IO `") | some initTypeArg => if (Lean.ConstantInfo.type decl == initTypeArg) = true then pure initFnName else Lean.throwError (Lean.toMessageData "initialization function '" ++ Lean.toMessageData initFnName ++ Lean.toMessageData "' type mismatch") | none => if Lean.isIOUnit (Lean.ConstantInfo.type decl) = true then pure Lean.Name.anonymous else Lean.throwError (Lean.toMessageData "initialization function must have type `IO Unit`"), afterSet := fun env x x => pure (), afterImport := fun entries => do let ctx ← read let a ← liftM Lean.isInitializerExecutionEnabled if (runAfterImport && a) = true then let s := toStream entries; do let r ← let col := ctx.env.header.moduleNames; forIn col s fun mod r => let s := r; match Stream.next? s with | none => pure (ForInStep.done s) | some (modEntries, s') => let s := s'; do let a ← liftM (Lean.runModInit mod) if (!a) = true then do let r ← forIn modEntries PUnit.unit fun x r => match x with | (decl, initDecl) => if Lean.Name.isAnonymous initDecl = true then do let initFn ← liftM (IO.ofExcept (Lean.Environment.evalConst (IO Unit) ctx.env ctx.opts decl)) liftM initFn pure (ForInStep.yield PUnit.unit) else do liftM (Lean.runInit ctx.env ctx.opts decl initDecl) pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit pure (ForInStep.yield s) else do pure PUnit.unit pure (ForInStep.yield s) let x : Subarray (Array (Lean.Name × Lean.Name)) := r let s : Subarray (Array (Lean.Name × Lean.Name)) := x pure PUnit.unit else pure PUnit.unit }

source

@[implementedBy Lean.registerInitAttrUnsafe]

constant Lean.registerInitAttr (attrName : Lean.Name) (runAfterImport : Bool) :

IO (Lean.ParametricAttribute Lean.Name)

source

constant Lean.regularInitAttr :

Lean.ParametricAttribute Lean.Name

source

constant Lean.builtinInitAttr :

Lean.ParametricAttribute Lean.Name

source

def Lean.getInitFnNameForCore? (env : Lean.Environment) (attr : Lean.ParametricAttribute Lean.Name) (fn : Lean.Name) :

Option Lean.Name

Equations

Lean.getInitFnNameForCore? env attr fn = match Lean.ParametricAttribute.getParam attr env fn with | some Lean.Name.anonymous => none | some n => some n | x => none

source

def Lean.getBuiltinInitFnNameFor? (env : Lean.Environment) (fn : Lean.Name) :

Option Lean.Name

Equations

Lean.getBuiltinInitFnNameFor? env fn = Lean.getInitFnNameForCore? env Lean.builtinInitAttr fn

source

def Lean.getRegularInitFnNameFor? (env : Lean.Environment) (fn : Lean.Name) :

Option Lean.Name

Equations

Lean.getRegularInitFnNameFor? env fn = Lean.getInitFnNameForCore? env Lean.regularInitAttr fn

source

def Lean.getInitFnNameFor? (env : Lean.Environment) (fn : Lean.Name) :

Option Lean.Name

Equations

Lean.getInitFnNameFor? env fn = HOrElse.hOrElse (Lean.getBuiltinInitFnNameFor? env fn) fun x => Lean.getRegularInitFnNameFor? env fn

source

def Lean.isIOUnitInitFnCore (env : Lean.Environment) (attr : Lean.ParametricAttribute Lean.Name) (fn : Lean.Name) :

Bool

Equations

Lean.isIOUnitInitFnCore env attr fn = match Lean.ParametricAttribute.getParam attr env fn with | some Lean.Name.anonymous => true | x => false

source

def Lean.isIOUnitRegularInitFn (env : Lean.Environment) (fn : Lean.Name) :

Bool

Equations

Lean.isIOUnitRegularInitFn env fn = Lean.isIOUnitInitFnCore env Lean.regularInitAttr fn

source

def Lean.isIOUnitBuiltinInitFn (env : Lean.Environment) (fn : Lean.Name) :

Bool

Equations

Lean.isIOUnitBuiltinInitFn env fn = Lean.isIOUnitInitFnCore env Lean.builtinInitAttr fn

source

def Lean.isIOUnitInitFn (env : Lean.Environment) (fn : Lean.Name) :

Bool

Equations

Lean.isIOUnitInitFn env fn = (Lean.isIOUnitBuiltinInitFn env fn || Lean.isIOUnitRegularInitFn env fn)

source

def Lean.hasInitAttr (env : Lean.Environment) (fn : Lean.Name) :

Bool

Equations

Lean.hasInitAttr env fn = Option.isSome (Lean.getInitFnNameFor? env fn)

source

def Lean.setBuiltinInitAttr (env : Lean.Environment) (declName : Lean.Name) (initFnName : optParam Lean.Name Lean.Name.anonymous) :

Except String Lean.Environment

Equations

Lean.setBuiltinInitAttr env declName initFnName = Lean.ParametricAttribute.setParam Lean.builtinInitAttr env declName initFnName

source

def Lean.declareBuiltin (forDecl : Lean.Name) (value : Lean.Expr) :

Lean.CoreM Unit

Equations

Lean.declareBuiltin forDecl value = let name := `_regBuiltin ++ forDecl; let type := Lean.mkApp (Lean.mkConst `IO) (Lean.mkConst `Unit); let decl := Lean.Declaration.defnDecl { toConstantVal := { name := name, levelParams := [], type := type }, value := value, hints := Lean.ReducibilityHints.opaque, safety := Lean.DefinitionSafety.safe }; do let a ← Lean.getEnv match Lean.Environment.addAndCompile a { entries := [] } decl with | Except.error e => do let msg ← liftM (Lean.MessageData.toString (Lean.KernelException.toMessageData e { entries := [] })) Lean.throwError (Lean.toMessageData "failed to emit registration code for builtin '" ++ Lean.toMessageData forDecl ++ Lean.toMessageData "': " ++ Lean.toMessageData msg ++ Lean.toMessageData "") | Except.ok env => liftM (IO.ofExcept (Lean.setBuiltinInitAttr env name)) >>= Lean.setEnv