Lean.Compiler.LCNF.PhaseExt

source

def Lean.Compiler.LCNF.isDeclTransparent (env : Environment) (phase : Phase) (declName : Name) :

Bool

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Lean.Compiler.LCNF.setDeclTransparent (env : Environment) (phase : Phase) (declName : Name) :

Environment

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[reducible, inline]

abbrev Lean.Compiler.LCNF.AbstractDeclExtState (pu : Purity) (β : Purity → Type) :

Type

Equations

Lean.Compiler.LCNF.AbstractDeclExtState pu β = Lean.PHashMap Lean.Name (β pu)

Instances For

source

@[reducible, inline]

abbrev Lean.Compiler.LCNF.DeclExtState (pu : Purity) :

Type

Equations

Lean.Compiler.LCNF.DeclExtState pu = Lean.Compiler.LCNF.AbstractDeclExtState pu Lean.Compiler.LCNF.Decl

Instances For

source

def Lean.Compiler.LCNF.DeclExt (pu : Purity) :

Type

Equations

Lean.Compiler.LCNF.DeclExt pu = Lean.PersistentEnvExtension (Lean.Compiler.LCNF.Decl pu) (Lean.Compiler.LCNF.Decl pu) (Lean.Compiler.LCNF.DeclExtState pu)

Instances For

source

@[implicit_reducible]

instance Lean.Compiler.LCNF.instInhabitedDeclExt {pu : Purity} :

Inhabited (DeclExt pu)

Equations

Lean.Compiler.LCNF.instInhabitedDeclExt = { default := Lean.Compiler.LCNF.instInhabitedDeclExt._aux_1 }

source

def Lean.Compiler.LCNF.mkDeclExt (phase : Phase) (name : Name := by exact decl_name%) :

IO (DeclExt phase.toPurity)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

opaque Lean.Compiler.LCNF.baseExt :

DeclExt Purity.pure

source

opaque Lean.Compiler.LCNF.monoExt :

DeclExt Purity.pure

source

opaque Lean.Compiler.LCNF.impureExt :

EnvExtension (DeclExtState Purity.impure)

source

@[reducible, inline]

abbrev Lean.Compiler.LCNF.SigExtState (pu : Purity) :

Type

Equations

Lean.Compiler.LCNF.SigExtState pu = Lean.Compiler.LCNF.AbstractDeclExtState pu Lean.Compiler.LCNF.Signature

Instances For

source

def Lean.Compiler.LCNF.SigExt (pu : Purity) :

Type

Equations

Lean.Compiler.LCNF.SigExt pu = Lean.PersistentEnvExtension (Lean.Compiler.LCNF.Signature pu) (Lean.Compiler.LCNF.Signature pu) (Lean.Compiler.LCNF.SigExtState pu)

Instances For

source

@[implicit_reducible]

instance Lean.Compiler.LCNF.instInhabitedSigExt {pu : Purity} :

Inhabited (SigExt pu)

Equations

Lean.Compiler.LCNF.instInhabitedSigExt = { default := Lean.Compiler.LCNF.instInhabitedSigExt._aux_1 }

source

def Lean.Compiler.LCNF.mkSigDeclExt (phase : Phase) (name : Name := by exact decl_name%) :

IO (SigExt phase.toPurity)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

opaque Lean.Compiler.LCNF.impureSigExt :

SigExt Purity.impure

source

def Lean.Compiler.LCNF.getDeclCore? {pu : Purity} (env : Environment) (ext : DeclExt pu) (declName : Name) :

Option (Decl pu)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Lean.Compiler.LCNF.getSigCore? {pu : Purity} (env : Environment) (ext : SigExt pu) (declName : Name) :

Option (Signature pu)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Lean.Compiler.LCNF.getBaseDecl? (declName : Name) :

CoreM (Option (Decl Purity.pure))

Equations

Lean.Compiler.LCNF.getBaseDecl? declName = do let __do_lift ← Lean.getEnv pure (Lean.Compiler.LCNF.getDeclCore? __do_lift Lean.Compiler.LCNF.baseExt declName)

Instances For

source

def Lean.Compiler.LCNF.getMonoDecl? (declName : Name) :

CoreM (Option (Decl Purity.pure))

Equations

Lean.Compiler.LCNF.getMonoDecl? declName = do let __do_lift ← Lean.getEnv pure (Lean.Compiler.LCNF.getDeclCore? __do_lift Lean.Compiler.LCNF.monoExt declName)

Instances For

source

def Lean.Compiler.LCNF.getLocalImpureDecl? (declName : Name) :

CoreM (Option (Decl Purity.impure))

Equations

Lean.Compiler.LCNF.getLocalImpureDecl? declName = do let __do_lift ← Lean.getEnv pure (Lean.PersistentHashMap.find? (Lean.Compiler.LCNF.impureExt.getState __do_lift) declName)

Instances For

source

def Lean.Compiler.LCNF.getLocalImpureDecls :

CoreM (Array Name)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Lean.Compiler.LCNF.getImpureSignature? (declName : Name) :

CoreM (Option (Signature Purity.impure))

Equations

Lean.Compiler.LCNF.getImpureSignature? declName = do let __do_lift ← Lean.getEnv pure (Lean.Compiler.LCNF.getSigCore? __do_lift Lean.Compiler.LCNF.impureSigExt declName)

Instances For

source

def Lean.Compiler.LCNF.saveBaseDeclCore (env : Environment) (decl : Decl Purity.pure) :

Environment

Equations

Lean.Compiler.LCNF.saveBaseDeclCore env decl = Lean.PersistentEnvExtension.addEntry Lean.Compiler.LCNF.baseExt env decl

Instances For

source

def Lean.Compiler.LCNF.saveMonoDeclCore (env : Environment) (decl : Decl Purity.pure) :

Environment

Equations

Lean.Compiler.LCNF.saveMonoDeclCore env decl = Lean.PersistentEnvExtension.addEntry Lean.Compiler.LCNF.monoExt env decl

Instances For

source

def Lean.Compiler.LCNF.saveImpureDeclCore (env : Environment) (decl : Decl Purity.impure) :

Environment

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Lean.Compiler.LCNF.Decl.saveBase (decl : Decl Purity.pure) :

CoreM Unit

Equations

decl.saveBase = Lean.modifyEnv fun (x : Lean.Environment) => Lean.Compiler.LCNF.saveBaseDeclCore x decl

Instances For

source

def Lean.Compiler.LCNF.Decl.saveMono (decl : Decl Purity.pure) :

CoreM Unit

Equations

decl.saveMono = Lean.modifyEnv fun (x : Lean.Environment) => Lean.Compiler.LCNF.saveMonoDeclCore x decl

Instances For

source

def Lean.Compiler.LCNF.Decl.saveImpure (decl : Decl Purity.impure) :

CoreM Unit

Equations

decl.saveImpure = Lean.modifyEnv fun (x : Lean.Environment) => Lean.Compiler.LCNF.saveImpureDeclCore x decl

Instances For

source

def Lean.Compiler.LCNF.Decl.save {pu : Purity} (decl : Decl pu) :

CompilerM Unit

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Lean.Compiler.LCNF.getDeclAt? (declName : Name) (phase : Phase) :

CoreM (Option (Decl phase.toPurity))

Equations

Lean.Compiler.LCNF.getDeclAt? declName Lean.Compiler.LCNF.Phase.base = Lean.Compiler.LCNF.getBaseDecl? declName
Lean.Compiler.LCNF.getDeclAt? declName Lean.Compiler.LCNF.Phase.mono = Lean.Compiler.LCNF.getMonoDecl? declName
Lean.Compiler.LCNF.getDeclAt? declName Lean.Compiler.LCNF.Phase.impure = Lean.throwError (Lean.toMessageData "Internal compiler error: getDecl? on impure is unuspported for now")

Instances For

source

@[inline]

def Lean.Compiler.LCNF.getDecl? (declName : Name) :

CompilerM (Option ((pu : Purity) × Decl pu))

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Lean.Compiler.LCNF.getLocalDeclAt? (declName : Name) (phase : Phase) :

CompilerM (Option (Decl phase.toPurity))

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[inline]

def Lean.Compiler.LCNF.getLocalDecl? (declName : Name) :

CompilerM (Option ((pu : Purity) × Decl pu))

Equations

One or more equations did not get rendered due to their size.

Instances For

source

opaque Lean.Compiler.LCNF.declOrderExt :

EnvExtension (List Name × NameSet)

source

def Lean.Compiler.LCNF.recordFinalImpureDecl (env : Environment) (name : Name) :

Environment

Equations

Lean.Compiler.LCNF.recordFinalImpureDecl env name = Lean.Compiler.LCNF.declOrderExt.modifyState env fun (s : List Lean.Name × Lean.NameSet) => (name :: s.fst, s.snd.insert name)

Instances For

source

def Lean.Compiler.LCNF.getImpureDeclIndices (env : Environment) (targets : Array Name) :

Std.HashMap Name Nat

Equations

One or more equations did not get rendered due to their size.

Instances For