Lean.Structure

source

structure Lean.StructureFieldInfo :

Type

fieldName : Lean.Name
projFn : Lean.Name
subobject? : Option Lean.Name
binderInfo : Lean.BinderInfo
inferMod : Bool

source

instance Lean.instInhabitedStructureFieldInfo :

Inhabited Lean.StructureFieldInfo

Equations

Lean.instInhabitedStructureFieldInfo = { default := { fieldName := default, projFn := default, subobject? := default, binderInfo := default, inferMod := default } }

source

instance Lean.instReprStructureFieldInfo :

Repr Lean.StructureFieldInfo

Equations

Lean.instReprStructureFieldInfo = { reprPrec := [anonymous] }

source

def Lean.StructureFieldInfo.lt (i₁ : Lean.StructureFieldInfo) (i₂ : Lean.StructureFieldInfo) :

Bool

Equations

Lean.StructureFieldInfo.lt i₁ i₂ = Lean.Name.quickLt i₁.fieldName i₂.fieldName

source

structure Lean.StructureInfo :

Type

structName : Lean.Name
fieldNames : Array Lean.Name
fieldInfo : Array Lean.StructureFieldInfo

source

instance Lean.instInhabitedStructureInfo :

Inhabited Lean.StructureInfo

Equations

Lean.instInhabitedStructureInfo = { default := { structName := default, fieldNames := default, fieldInfo := default } }

source

def Lean.StructureInfo.lt (i₁ : Lean.StructureInfo) (i₂ : Lean.StructureInfo) :

Bool

Equations

Lean.StructureInfo.lt i₁ i₂ = Lean.Name.quickLt i₁.structName i₂.structName

source

instance Lean.instInhabitedStructureState :

Inhabited Lean.StructureState

Equations

Lean.instInhabitedStructureState = { default := { map := default } }

source

constant Lean.structureExt :

Lean.SimplePersistentEnvExtension Lean.StructureInfo Lean.StructureState

source

structure Lean.StructureDescr :

Type

structName : Lean.Name
fields : Array Lean.StructureFieldInfo

source

instance Lean.instInhabitedStructureDescr :

Inhabited Lean.StructureDescr

Equations

Lean.instInhabitedStructureDescr = { default := { structName := default, fields := default } }

source

def Lean.registerStructure (env : Lean.Environment) (e : Lean.StructureDescr) :

Lean.Environment

Equations

Lean.registerStructure env e = Lean.PersistentEnvExtension.addEntry Lean.structureExt env { structName := e.structName, fieldNames := Array.map (fun e => e.fieldName) e.fields, fieldInfo := Array.qsort e.fields Lean.StructureFieldInfo.lt 0 (Array.size e.fields - 1) }

source

def Lean.getStructureInfo? (env : Lean.Environment) (structName : Lean.Name) :

Option Lean.StructureInfo

Equations

Lean.getStructureInfo? env structName = match Lean.Environment.getModuleIdxFor? env structName with | some modIdx => Array.binSearch (Lean.PersistentEnvExtension.getModuleEntries Lean.structureExt env modIdx) { structName := structName, fieldNames := #[], fieldInfo := #[] } Lean.StructureInfo.lt 0 (Array.size (Lean.PersistentEnvExtension.getModuleEntries Lean.structureExt env modIdx) - 1) | none => Std.PersistentHashMap.find? (Lean.SimplePersistentEnvExtension.getState Lean.structureExt env).map structName

source

def Lean.getStructureCtor (env : Lean.Environment) (constName : Lean.Name) :

Lean.ConstructorVal

Equations

Lean.getStructureCtor env constName = match Lean.Environment.find? env constName with | some (Lean.ConstantInfo.inductInfo { toConstantVal := { name := x, levelParams := x_1, type := x_2 }, numParams := x_3, numIndices := x_4, all := x_5, ctors := [ctorName], isRec := false, isUnsafe := x_6, isReflexive := x_7, isNested := x_8 }) => match Lean.Environment.find? env ctorName with | some (Lean.ConstantInfo.ctorInfo val) => val | x => panicWithPosWithDecl "Lean.Structure" "Lean.getStructureCtor" 67 11 "ill-formed environment" | x => panicWithPosWithDecl "Lean.Structure" "Lean.getStructureCtor" 68 9 "structure expected"

source

def Lean.getStructureFields (env : Lean.Environment) (structName : Lean.Name) :

Array Lean.Name

Equations

Lean.getStructureFields env structName = match Lean.getStructureInfo? env structName with | some info => info.fieldNames | x => panicWithPosWithDecl "Lean.Structure" "Lean.getStructureFields" 75 4 "structure expected"

source

def Lean.getFieldInfo? (env : Lean.Environment) (structName : Lean.Name) (fieldName : Lean.Name) :

Option Lean.StructureFieldInfo

Equations

Lean.getFieldInfo? env structName fieldName = match Lean.getStructureInfo? env structName with | some info => Array.binSearch info.fieldInfo { fieldName := fieldName, projFn := default, subobject? := none, binderInfo := default, inferMod := false } Lean.StructureFieldInfo.lt 0 (Array.size info.fieldInfo - 1) | x => none

source

def Lean.isSubobjectField? (env : Lean.Environment) (structName : Lean.Name) (fieldName : Lean.Name) :

Option Lean.Name

Equations

Lean.isSubobjectField? env structName fieldName = match Lean.getFieldInfo? env structName fieldName with | some fieldInfo => fieldInfo.subobject? | x => none

source

def Lean.getParentStructures (env : Lean.Environment) (structName : Lean.Name) :

Array Lean.Name

Equations

Lean.getParentStructures env structName = let fieldNames := Lean.getStructureFields env structName; Array.foldl (fun acc fieldName => match Lean.isSubobjectField? env structName fieldName with | some parentStructName => Array.push acc parentStructName | none => acc) #[] fieldNames 0 (Array.size fieldNames)

source

def Lean.getAllParentStructures (env : Lean.Environment) (structName : Lean.Name) :

Array Lean.Name

Equations

Lean.getAllParentStructures env structName = (fun visit => (StateT.run (visit structName) #[]).snd) (Lean.getAllParentStructures.visit env)

source

partial def Lean.getAllParentStructures.visit (env : Lean.Environment) (structName : Lean.Name) :

StateT (Array Lean.Name) Id Unit

source

partial def Lean.findField? (env : Lean.Environment) (structName : Lean.Name) (fieldName : Lean.Name) :

Option Lean.Name

source

def Lean.getStructureFieldsFlattened (env : Lean.Environment) (structName : Lean.Name) (includeSubobjectFields : optParam Bool true) :

Array Lean.Name

Equations

Lean.getStructureFieldsFlattened env structName includeSubobjectFields = Lean.getStructureFieldsFlattenedAux env structName #[] includeSubobjectFields

source

def Lean.isStructure (env : Lean.Environment) (constName : Lean.Name) :

Bool

Equations

Lean.isStructure env constName = Option.isSome (Lean.getStructureInfo? env constName)

source

def Lean.getProjFnForField? (env : Lean.Environment) (structName : Lean.Name) (fieldName : Lean.Name) :

Option Lean.Name

Equations

Lean.getProjFnForField? env structName fieldName = match Lean.getFieldInfo? env structName fieldName with | some fieldInfo => some fieldInfo.projFn | x => none

source

def Lean.mkDefaultFnOfProjFn (projFn : Lean.Name) :

Lean.Name

Equations

Lean.mkDefaultFnOfProjFn projFn = projFn ++ `_default

source

def Lean.getDefaultFnForField? (env : Lean.Environment) (structName : Lean.Name) (fieldName : Lean.Name) :

Option Lean.Name

Equations

Lean.getDefaultFnForField? env structName fieldName = match Lean.getProjFnForField? env structName fieldName with | some projName => let defFn := Lean.mkDefaultFnOfProjFn projName; if Lean.Environment.contains env defFn = true then some defFn else none | x => let defFn := Lean.mkDefaultFnOfProjFn (structName ++ fieldName); if Lean.Environment.contains env defFn = true then some defFn else none

source

partial def Lean.getPathToBaseStructureAux (env : Lean.Environment) (baseStructName : Lean.Name) (structName : Lean.Name) (path : List Lean.Name) :

Option (List Lean.Name)

source

def Lean.getPathToBaseStructure? (env : Lean.Environment) (baseStructName : Lean.Name) (structName : Lean.Name) :

Option (List Lean.Name)

Equations

Lean.getPathToBaseStructure? env baseStructName structName = Lean.getPathToBaseStructureAux env baseStructName structName []

source

def Lean.isStructureLike (env : Lean.Environment) (constName : Lean.Name) :

Bool

Equations

Lean.isStructureLike env constName = match Lean.Environment.find? env constName with | some (Lean.ConstantInfo.inductInfo { toConstantVal := { name := x, levelParams := x_1, type := x_2 }, numParams := x_3, numIndices := 0, all := x_4, ctors := [ctor], isRec := false, isUnsafe := x_5, isReflexive := x_6, isNested := x_7 }) => true | x => false

source

def Lean.getStructureLikeNumFields (env : Lean.Environment) (constName : Lean.Name) :

Nat

Equations

Lean.getStructureLikeNumFields env constName = match Lean.Environment.find? env constName with | some (Lean.ConstantInfo.inductInfo { toConstantVal := { name := x, levelParams := x_1, type := x_2 }, numParams := x_3, numIndices := 0, all := x_4, ctors := [ctor], isRec := false, isUnsafe := x_5, isReflexive := x_6, isNested := x_7 }) => match Lean.Environment.find? env ctor with | some (Lean.ConstantInfo.ctorInfo { toConstantVal := { name := x, levelParams := x_8, type := x_9 }, induct := x_10, cidx := x_11, numParams := x_12, numFields := n, isUnsafe := x_13 }) => n | x => 0 | x => 0