Documentation

Lean.Elab.StructInst

def Lean.Elab.Term.StructInst.expandStructInstExpectedType :

Equations

Lean.Elab.Term.StructInst.expandStructInstExpectedType stx = let expectedArg := Lean.Syntax.getOp stx 4; if Lean.Syntax.isNone expectedArg = true then Lean.Macro.throwUnsupported else let expected := Lean.Syntax.getOp expectedArg 1; let stxNew := Lean.Syntax.setArg stx 4 Lean.mkNullNode; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[stxNew, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeAscription #[Lean.Syntax.atom info ":", expected]]], Lean.Syntax.atom info ")"])

def Lean.Elab.Term.StructInst.expandStructInstFieldAbbrev :

Equations

Lean.Elab.Term.StructInst.expandStructInstFieldAbbrev stx = if Array.any (Lean.Syntax.getArgs (Lean.Syntax.getOp stx 2)) (fun arg => Lean.Syntax.getKind (Lean.Syntax.getOp arg 0) == `Lean.Parser.Term.structInstFieldAbbrev) 0 (Array.size (Lean.Syntax.getArgs (Lean.Syntax.getOp stx 2))) = true then do let fieldsNew ← Array.mapM (fun stx => let field := Lean.Syntax.getOp stx 0; if (Lean.Syntax.getKind field == `Lean.Parser.Term.structInstFieldAbbrev) = true then let id := Lean.Syntax.getOp field 0; do let fieldNew ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.structInstField #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.structInstLVal #[id, Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ":=", id]) pure (Lean.Syntax.setArg stx 0 fieldNew) else pure stx) (Lean.Syntax.getArgs (Lean.Syntax.getOp stx 2)) pure (Lean.Syntax.setArg stx 2 (Lean.mkNullNode fieldsNew)) else Lean.Macro.throwUnsupported

structure Lean.Elab.Term.StructInst.ExplicitSourceInfo :

Type

stx : Lean.Syntax
structName : Lean.Name

instance Lean.Elab.Term.StructInst.instInhabitedExplicitSourceInfo :

Inhabited Lean.Elab.Term.StructInst.ExplicitSourceInfo

Equations

Lean.Elab.Term.StructInst.instInhabitedExplicitSourceInfo = { default := { stx := default, structName := default } }

inductive Lean.Elab.Term.StructInst.Source :

Type

none: Lean.Elab.Term.StructInst.Source
implicit: Lean.Syntax → Lean.Elab.Term.StructInst.Source
explicit: Array Lean.Elab.Term.StructInst.ExplicitSourceInfo → Lean.Elab.Term.StructInst.Source

instance Lean.Elab.Term.StructInst.instInhabitedSource :

Inhabited Lean.Elab.Term.StructInst.Source

Equations

Lean.Elab.Term.StructInst.instInhabitedSource = { default := Lean.Elab.Term.StructInst.Source.none }

def Lean.Elab.Term.StructInst.Source.isNone :

Lean.Elab.Term.StructInst.Source → Bool

Equations

Lean.Elab.Term.StructInst.Source.isNone x = match x with | Lean.Elab.Term.StructInst.Source.none => true | x => false

inductive Lean.Elab.Term.StructInst.FieldLHS :

Type

fieldName: Lean.Syntax → Lean.Name → Lean.Elab.Term.StructInst.FieldLHS
fieldIndex: Lean.Syntax → Nat → Lean.Elab.Term.StructInst.FieldLHS
modifyOp: Lean.Syntax → Lean.Syntax → Lean.Elab.Term.StructInst.FieldLHS

instance Lean.Elab.Term.StructInst.instInhabitedFieldLHS :

Inhabited Lean.Elab.Term.StructInst.FieldLHS

Equations

Lean.Elab.Term.StructInst.instInhabitedFieldLHS = { default := Lean.Elab.Term.StructInst.FieldLHS.fieldName default default }

instance Lean.Elab.Term.StructInst.instToFormatFieldLHS :

Lean.ToFormat Lean.Elab.Term.StructInst.FieldLHS

Equations

Lean.Elab.Term.StructInst.instToFormatFieldLHS = { format := fun lhs => match lhs with | Lean.Elab.Term.StructInst.FieldLHS.fieldName x n => Lean.format n | Lean.Elab.Term.StructInst.FieldLHS.fieldIndex x i => Lean.format i | Lean.Elab.Term.StructInst.FieldLHS.modifyOp x i => Std.Format.text "[" ++ Lean.Syntax.prettyPrint i ++ Std.Format.text "]" }

inductive Lean.Elab.Term.StructInst.FieldVal (σ : Type) :

Type

term: {σ : Type} → Lean.Syntax → Lean.Elab.Term.StructInst.FieldVal σ
nested: {σ : Type} → σ → Lean.Elab.Term.StructInst.FieldVal σ
default: {σ : Type} → Lean.Elab.Term.StructInst.FieldVal σ

instance Lean.Elab.Term.StructInst.instInhabitedFieldVal :

{a : Type} → Inhabited (Lean.Elab.Term.StructInst.FieldVal a)

Equations

Lean.Elab.Term.StructInst.instInhabitedFieldVal = { default := Lean.Elab.Term.StructInst.FieldVal.term default }

structure Lean.Elab.Term.StructInst.Field (σ : Type) :

Type

ref : Lean.Syntax
lhs : List Lean.Elab.Term.StructInst.FieldLHS
val : Lean.Elab.Term.StructInst.FieldVal σ
expr? : Option Lean.Expr

instance Lean.Elab.Term.StructInst.instInhabitedField :

{a : Type} → Inhabited (Lean.Elab.Term.StructInst.Field a)

Equations

Lean.Elab.Term.StructInst.instInhabitedField = { default := { ref := default, lhs := default, val := default, expr? := default } }

def Lean.Elab.Term.StructInst.Field.isSimple {σ : Type} :

Lean.Elab.Term.StructInst.Field σ → Bool

Equations

Lean.Elab.Term.StructInst.Field.isSimple x = match x with | { ref := x_1, lhs := [x], val := x_2, expr? := x_3 } => true | x => false

inductive Lean.Elab.Term.StructInst.Struct :

Type

mk: Lean.Syntax → Lean.Name → List (Lean.Elab.Term.StructInst.Field Lean.Elab.Term.StructInst.Struct) → Lean.Elab.Term.StructInst.Source → Lean.Elab.Term.StructInst.Struct

instance Lean.Elab.Term.StructInst.instInhabitedStruct :

Inhabited Lean.Elab.Term.StructInst.Struct

Equations

Lean.Elab.Term.StructInst.instInhabitedStruct = { default := Lean.Elab.Term.StructInst.Struct.mk default default default default }

@[inline]

abbrev Lean.Elab.Term.StructInst.Fields :

Type

Equations

Lean.Elab.Term.StructInst.Fields = List (Lean.Elab.Term.StructInst.Field Lean.Elab.Term.StructInst.Struct)

def Lean.Elab.Term.StructInst.Struct.ref :

Lean.Elab.Term.StructInst.Struct → Lean.Syntax

Equations

Lean.Elab.Term.StructInst.Struct.ref x = match x with | Lean.Elab.Term.StructInst.Struct.mk ref x x_1 x_2 => ref

def Lean.Elab.Term.StructInst.Struct.structName :

Lean.Elab.Term.StructInst.Struct → Lean.Name

Equations

Lean.Elab.Term.StructInst.Struct.structName x = match x with | Lean.Elab.Term.StructInst.Struct.mk x structName x_1 x_2 => structName

def Lean.Elab.Term.StructInst.Struct.fields :

Lean.Elab.Term.StructInst.Struct → Lean.Elab.Term.StructInst.Fields

Equations

Lean.Elab.Term.StructInst.Struct.fields x = match x with | Lean.Elab.Term.StructInst.Struct.mk x x_1 fields x_2 => fields

def Lean.Elab.Term.StructInst.Struct.source :

Lean.Elab.Term.StructInst.Struct → Lean.Elab.Term.StructInst.Source

Equations

Lean.Elab.Term.StructInst.Struct.source x = match x with | Lean.Elab.Term.StructInst.Struct.mk x x_1 x_2 s => s

partial def Lean.Elab.Term.StructInst.Struct.allDefault (s : Lean.Elab.Term.StructInst.Struct) :

def Lean.Elab.Term.StructInst.formatField (formatStruct : Lean.Elab.Term.StructInst.Struct → Lean.Format) (field : Lean.Elab.Term.StructInst.Field Lean.Elab.Term.StructInst.Struct) :

Equations

Lean.Elab.Term.StructInst.formatField formatStruct field = Lean.Format.joinSep field.lhs (Std.Format.text " . ") ++ Std.Format.text " := " ++ match field.val with | Lean.Elab.Term.StructInst.FieldVal.term v => Lean.Syntax.prettyPrint v | Lean.Elab.Term.StructInst.FieldVal.nested s => formatStruct s | Lean.Elab.Term.StructInst.FieldVal.default => Std.Format.text ""

partial def Lean.Elab.Term.StructInst.formatStruct :

Lean.Elab.Term.StructInst.Struct → Lean.Format

instance Lean.Elab.Term.StructInst.instToFormatStruct :

Lean.ToFormat Lean.Elab.Term.StructInst.Struct

Equations

Lean.Elab.Term.StructInst.instToFormatStruct = { format := Lean.Elab.Term.StructInst.formatStruct }

instance Lean.Elab.Term.StructInst.instToStringStruct :

ToString Lean.Elab.Term.StructInst.Struct

Equations

Lean.Elab.Term.StructInst.instToStringStruct = { toString := toString ∘ Lean.format }

instance Lean.Elab.Term.StructInst.instToFormatFieldStruct :

Lean.ToFormat (Lean.Elab.Term.StructInst.Field Lean.Elab.Term.StructInst.Struct)

Equations

Lean.Elab.Term.StructInst.instToFormatFieldStruct = { format := Lean.Elab.Term.StructInst.formatField Lean.Elab.Term.StructInst.formatStruct }

instance Lean.Elab.Term.StructInst.instToStringFieldStruct :

ToString (Lean.Elab.Term.StructInst.Field Lean.Elab.Term.StructInst.Struct)

Equations

Lean.Elab.Term.StructInst.instToStringFieldStruct = { toString := toString ∘ Lean.format }

def Lean.Elab.Term.StructInst.FieldLHS.toSyntax (first : Bool) :

Lean.Elab.Term.StructInst.FieldLHS → Lean.Syntax

Equations

Lean.Elab.Term.StructInst.FieldLHS.toSyntax first x = match x with | Lean.Elab.Term.StructInst.FieldLHS.modifyOp stx x => stx | Lean.Elab.Term.StructInst.FieldLHS.fieldName stx name => if first = true then Lean.mkIdentFrom stx name else Lean.mkGroupNode #[Lean.mkAtomFrom stx ".", Lean.mkIdentFrom stx name] | Lean.Elab.Term.StructInst.FieldLHS.fieldIndex stx x => if first = true then stx else Lean.mkGroupNode #[Lean.mkAtomFrom stx ".", stx]

def Lean.Elab.Term.StructInst.FieldVal.toSyntax :

Lean.Elab.Term.StructInst.FieldVal Lean.Elab.Term.StructInst.Struct → Lean.Syntax

Equations

Lean.Elab.Term.StructInst.FieldVal.toSyntax x = match x with | Lean.Elab.Term.StructInst.FieldVal.term stx => stx | x => panicWithPosWithDecl "Lean.Elab.StructInst" "Lean.Elab.Term.StructInst.FieldVal.toSyntax" 319 25 "unreachable code has been reached"

def Lean.Elab.Term.StructInst.Field.toSyntax :

Lean.Elab.Term.StructInst.Field Lean.Elab.Term.StructInst.Struct → Lean.Syntax

Equations

Lean.Elab.Term.StructInst.Field.toSyntax x = let field := x; let stx := field.ref; let stx := Lean.Syntax.setArg stx 2 (Lean.Elab.Term.StructInst.FieldVal.toSyntax field.val); match field.lhs with | first :: rest => Lean.Syntax.setArg stx 0 (Lean.mkNullNode #[Lean.Elab.Term.StructInst.FieldLHS.toSyntax true first, Lean.mkNullNode (Array.map (Lean.Elab.Term.StructInst.FieldLHS.toSyntax false) (List.toArray rest))]) | x => panicWithPosWithDecl "Lean.Elab.StructInst" "Lean.Elab.Term.StructInst.Field.toSyntax" 327 11 "unreachable code has been reached"

def Lean.Elab.Term.StructInst.Struct.modifyFieldsM {m : Type → Type} [inst : Monad m] (s : Lean.Elab.Term.StructInst.Struct) (f : Lean.Elab.Term.StructInst.Fields → m Lean.Elab.Term.StructInst.Fields) :

m Lean.Elab.Term.StructInst.Struct

Equations

Lean.Elab.Term.StructInst.Struct.modifyFieldsM s f = match s with | Lean.Elab.Term.StructInst.Struct.mk ref structName fields source => do let a ← f fields pure (Lean.Elab.Term.StructInst.Struct.mk ref structName a source)

def Lean.Elab.Term.StructInst.Struct.modifyFields (s : Lean.Elab.Term.StructInst.Struct) (f : Lean.Elab.Term.StructInst.Fields → Lean.Elab.Term.StructInst.Fields) :

Lean.Elab.Term.StructInst.Struct

Equations

Lean.Elab.Term.StructInst.Struct.modifyFields s f = Id.run (Lean.Elab.Term.StructInst.Struct.modifyFieldsM s f)

def Lean.Elab.Term.StructInst.Struct.setFields (s : Lean.Elab.Term.StructInst.Struct) (fields : Lean.Elab.Term.StructInst.Fields) :

Lean.Elab.Term.StructInst.Struct

Equations

Lean.Elab.Term.StructInst.Struct.setFields s fields = Lean.Elab.Term.StructInst.Struct.modifyFields s fun x => fields

def Lean.Elab.Term.StructInst.mkProjStx? (s : Lean.Syntax) (structName : Lean.Name) (fieldName : Lean.Name) :

Lean.Elab.TermElabM (Option Lean.Syntax)

Equations

Lean.Elab.Term.StructInst.mkProjStx? s structName fieldName = do let a ← Lean.getEnv let a ← pure (Lean.findField? a structName fieldName) let _do_jp : PUnit → Lean.Elab.TermElabM (Option Lean.Syntax) := fun y => pure (some (Lean.mkNode `Lean.Parser.Term.proj #[s, Lean.mkAtomFrom s ".", Lean.mkIdentFrom s fieldName])) if Option.isNone a = true then pure none else do let y ← pure PUnit.unit _do_jp y

def Lean.Elab.Term.StructInst.findField? (fields : Lean.Elab.Term.StructInst.Fields) (fieldName : Lean.Name) :

Option (Lean.Elab.Term.StructInst.Field Lean.Elab.Term.StructInst.Struct)

Equations

Lean.Elab.Term.StructInst.findField? fields fieldName = List.find? (fun field => match field.lhs with | [Lean.Elab.Term.StructInst.FieldLHS.fieldName x n] => n == fieldName | x => false) fields

structure Lean.Elab.Term.StructInst.CtorHeaderResult :

Type

ctorFn : Lean.Expr
ctorFnType : Lean.Expr
instMVars : Array Lean.MVarId

def Lean.Elab.Term.StructInst.markDefaultMissing (e : Lean.Expr) :

Equations

Lean.Elab.Term.StructInst.markDefaultMissing e = Lean.mkAnnotation `structInstDefault e

def Lean.Elab.Term.StructInst.defaultMissing? (e : Lean.Expr) :

Option Lean.Expr

Equations

Lean.Elab.Term.StructInst.defaultMissing? e = Lean.annotation? `structInstDefault e

def Lean.Elab.Term.StructInst.throwFailedToElabField {α : Type} (fieldName : Lean.Name) (structName : Lean.Name) (msgData : Lean.MessageData) :

Lean.Elab.TermElabM α

Equations

Lean.Elab.Term.StructInst.throwFailedToElabField fieldName structName msgData = Lean.throwError (Lean.toMessageData "failed to elaborate field '" ++ Lean.toMessageData fieldName ++ Lean.toMessageData "' of '" ++ Lean.toMessageData structName ++ Lean.toMessageData ", " ++ Lean.toMessageData msgData ++ Lean.toMessageData "")

def Lean.Elab.Term.StructInst.trySynthStructInstance? (s : Lean.Elab.Term.StructInst.Struct) (expectedType : Lean.Expr) :

Lean.Elab.TermElabM (Option Lean.Expr)

Equations

Lean.Elab.Term.StructInst.trySynthStructInstance? s expectedType = if (!Lean.Elab.Term.StructInst.Struct.allDefault s) = true then pure none else tryCatch (liftM (Lean.Meta.synthInstance? expectedType none)) fun x => pure none

structure Lean.Elab.Term.StructInst.DefaultFields.Context :

Type

structs : Array Lean.Elab.Term.StructInst.Struct
allStructNames : Array Lean.Name
maxDistance : Nat

structure Lean.Elab.Term.StructInst.DefaultFields.State :

Type

progress : Bool

partial def Lean.Elab.Term.StructInst.DefaultFields.collectStructNames (struct : Lean.Elab.Term.StructInst.Struct) (names : Array Lean.Name) :

Array Lean.Name

partial def Lean.Elab.Term.StructInst.DefaultFields.getHierarchyDepth (struct : Lean.Elab.Term.StructInst.Struct) :

partial def Lean.Elab.Term.StructInst.DefaultFields.findDefaultMissing? (mctx : Lean.MetavarContext) (struct : Lean.Elab.Term.StructInst.Struct) :

Option (Lean.Elab.Term.StructInst.Field Lean.Elab.Term.StructInst.Struct)

def Lean.Elab.Term.StructInst.DefaultFields.getFieldName (field : Lean.Elab.Term.StructInst.Field Lean.Elab.Term.StructInst.Struct) :

Equations

Lean.Elab.Term.StructInst.DefaultFields.getFieldName field = match field.lhs with | [Lean.Elab.Term.StructInst.FieldLHS.fieldName x fieldName] => fieldName | x => panicWithPosWithDecl "Lean.Elab.StructInst" "Lean.Elab.Term.StructInst.DefaultFields.getFieldName" 708 9 "unreachable code has been reached"

@[inline]

abbrev Lean.Elab.Term.StructInst.DefaultFields.M (α : Type) :

Type

Equations

Lean.Elab.Term.StructInst.DefaultFields.M = ReaderT Lean.Elab.Term.StructInst.DefaultFields.Context (StateRefT' IO.RealWorld Lean.Elab.Term.StructInst.DefaultFields.State Lean.Elab.TermElabM)

def Lean.Elab.Term.StructInst.DefaultFields.isRoundDone :

Lean.Elab.Term.StructInst.DefaultFields.M Bool

Equations

Lean.Elab.Term.StructInst.DefaultFields.isRoundDone = do let a ← get let a_1 ← read pure (a.progress && decide (a_1.maxDistance > 0))

def Lean.Elab.Term.StructInst.DefaultFields.getFieldValue? (struct : Lean.Elab.Term.StructInst.Struct) (fieldName : Lean.Name) :

Option Lean.Expr

Equations

Lean.Elab.Term.StructInst.DefaultFields.getFieldValue? struct fieldName = List.findSome? (fun field => if (Lean.Elab.Term.StructInst.DefaultFields.getFieldName field == fieldName) = true then field.expr? else none) (Lean.Elab.Term.StructInst.Struct.fields struct)

partial def Lean.Elab.Term.StructInst.DefaultFields.mkDefaultValueAux? (struct : Lean.Elab.Term.StructInst.Struct) :

Lean.Expr → Lean.Elab.TermElabM (Option Lean.Expr)

def Lean.Elab.Term.StructInst.DefaultFields.mkDefaultValue? (struct : Lean.Elab.Term.StructInst.Struct) (cinfo : Lean.ConstantInfo) :

Lean.Elab.TermElabM (Option Lean.Expr)

Equations

Lean.Elab.Term.StructInst.DefaultFields.mkDefaultValue? struct cinfo = Lean.withRef (Lean.Elab.Term.StructInst.Struct.ref struct) do let us ← liftM (Lean.Meta.mkFreshLevelMVarsFor cinfo) Lean.Elab.Term.StructInst.DefaultFields.mkDefaultValueAux? struct (Lean.ConstantInfo.instantiateValueLevelParams cinfo us)

partial def Lean.Elab.Term.StructInst.DefaultFields.reduce (structNames : Array Lean.Name) (e : Lean.Expr) :

Lean.MetaM Lean.Expr

def Lean.Elab.Term.StructInst.DefaultFields.tryToSynthesizeDefault (structs : Array Lean.Elab.Term.StructInst.Struct) (allStructNames : Array Lean.Name) (maxDistance : Nat) (fieldName : Lean.Name) (mvarId : Lean.MVarId) :

Lean.Elab.TermElabM Bool

Equations

Lean.Elab.Term.StructInst.DefaultFields.tryToSynthesizeDefault structs allStructNames maxDistance fieldName mvarId = (fun loop => loop 0 0) (Lean.Elab.Term.StructInst.DefaultFields.tryToSynthesizeDefault.loop structs allStructNames maxDistance fieldName mvarId)

partial def Lean.Elab.Term.StructInst.DefaultFields.tryToSynthesizeDefault.loop (structs : Array Lean.Elab.Term.StructInst.Struct) (allStructNames : Array Lean.Name) (maxDistance : Nat) (fieldName : Lean.Name) (mvarId : Lean.MVarId) (i : Nat) (dist : Nat) :

Lean.Elab.TermElabM Bool

partial def Lean.Elab.Term.StructInst.DefaultFields.step (struct : Lean.Elab.Term.StructInst.Struct) :

Lean.Elab.Term.StructInst.DefaultFields.M Unit

partial def Lean.Elab.Term.StructInst.DefaultFields.propagateLoop (hierarchyDepth : Nat) (d : Nat) (struct : Lean.Elab.Term.StructInst.Struct) :

Lean.Elab.Term.StructInst.DefaultFields.M Unit

def Lean.Elab.Term.StructInst.DefaultFields.propagate (struct : Lean.Elab.Term.StructInst.Struct) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.Term.StructInst.DefaultFields.propagate struct = let hierarchyDepth := Lean.Elab.Term.StructInst.DefaultFields.getHierarchyDepth struct; let structNames := Lean.Elab.Term.StructInst.DefaultFields.collectStructNames struct #[]; StateRefT'.run' (Lean.Elab.Term.StructInst.DefaultFields.propagateLoop hierarchyDepth 0 struct { structs := #[], allStructNames := structNames, maxDistance := 0 }) { progress := false }

def Lean.Elab.Term.StructInst.elabStructInst :

Lean.Elab.Term.TermElab

Equations

Lean.Elab.Term.StructInst.elabStructInst stx expectedType? = do let a ← Lean.Elab.Term.StructInst.expandNonAtomicExplicitSources stx match a with | some stxNew => Lean.Elab.Term.withMacroExpansion stx stxNew (Lean.Elab.Term.elabTerm stxNew expectedType? true true) | none => do let sourceView ← Lean.Elab.Term.StructInst.getStructSource stx let a ← Lean.Elab.Term.StructInst.isModifyOp? stx match a, sourceView with | some modifyOp, Lean.Elab.Term.StructInst.Source.explicit sources => Lean.Elab.Term.StructInst.elabModifyOp stx modifyOp sources expectedType? | some x, x_1 => Lean.throwError (Lean.toMessageData "invalid {...} notation, explicit source is required when using '[] := '") | x, x_1 => Lean.Elab.Term.StructInst.elabStructInstAux stx expectedType? sourceView