diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index 0a936dc48f..2953888bb4 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/src/Lean/Elab/StructInst.lean @@ -845,7 +845,9 @@ private partial def elabStructInstView (s : StructInstView) (expectedType? : Opt let val ← ensureHasType d val cont val { field with val := FieldVal.nested sNew } (instMVars ++ instMVarsNew) | .default => - match d.getAutoParamTactic? with + let some fieldInfo := getFieldInfo? env s.structName fieldName + | withRef field.ref <| throwFailedToElabField fieldName s.structName m!"no such field '{fieldName}'" + match fieldInfo.autoParam? with | some (.const tacticDecl ..) => match evalSyntaxConstant env (← getOptions) tacticDecl with | .error err => throwError err @@ -855,7 +857,7 @@ private partial def elabStructInstView (s : StructInstView) (expectedType? : Opt -- We add info to get reliable positions for messages from evaluating the tactic script. let info := field.ref.getHeadInfo.nonCanonicalSynthetic let stx := stx.raw.rewriteBottomUp (·.setInfo info) - let type := (d.getArg! 0).consumeTypeAnnotations + let type := d.consumeTypeAnnotations let mvar ← mkTacticMVar type stx (.fieldAutoParam fieldName s.structName) -- Note(kmill): We are adding terminfo to simulate a previous implementation that elaborated `tacticBlock`. -- (See the aforementioned `processExplicitArg` for a comment about this.) @@ -970,13 +972,23 @@ abbrev M := ReaderT Context (StateRefT State TermElabM) def isRoundDone : M Bool := do return (← get).progress && (← read).maxDistance > 0 -/-- Returns the `expr?` for the given field. -/ -def getFieldValue? (struct : StructInstView) (fieldName : Name) : Option Expr := - struct.fields.findSome? fun field => - if getFieldName field == fieldName then - field.expr? - else - none +/-- Returns the `expr?` for the given field. The value may be inside a subobject. -/ +partial def getFieldValue? (struct : StructInstView) (fieldName : Name) : MetaM (Option Expr) := do + for field in struct.fields do + let fieldName' := getFieldName field + if fieldName' == fieldName then + return field.expr? + if let .nested s' := field.val then + if let some val ← getFieldValue? s' fieldName then + return val + if let some info := getFieldInfo? (← getEnv) struct.structName fieldName' then + if info.subobject?.isSome then + if let some e := field.expr? then + try + return ← mkProjection e fieldName + catch _ => + pure () + return none /-- Instantiates a default value from the given default value declaration, if applicable. -/ partial def mkDefaultValue? (struct : StructInstView) (cinfo : ConstantInfo) : TermElabM (Option Expr) := @@ -988,7 +1000,7 @@ where | .lam n d b c => withRef struct.ref do if c.isExplicit then let fieldName := n - match getFieldValue? struct fieldName with + match ← getFieldValue? struct fieldName with | none => return none | some val => let valType ← inferType val @@ -1078,8 +1090,9 @@ def tryToSynthesizeDefault (structs : Array StructInstView) (allStructNames : Ar return false else if h : i < structs.size then let struct := structs[i] - match getDefaultFnForField? (← getEnv) struct.structName fieldName with + match getEffectiveDefaultFnForField? (← getEnv) struct.structName fieldName with | some defFn => + trace[Elab.struct] "default fn for '{fieldName}' is '{.ofConstName defFn}'" let cinfo ← getConstInfo defFn let mctx ← getMCtx match (← mkDefaultValue? struct cinfo) with @@ -1141,7 +1154,7 @@ partial def propagateLoop (hierarchyDepth : Nat) (d : Nat) (struct : StructInstV let env := (← getEnv) let structs := (← read).allStructNames missingFields.filter fun fieldName => structs.all fun struct => - (getDefaultFnForField? env struct fieldName).isNone + (getEffectiveDefaultFnForField? env struct fieldName).isNone let fieldsToReport := if missingFieldsWithoutDefault.isEmpty then missingFields else missingFieldsWithoutDefault throwErrorAt field.ref "fields missing: {fieldsToReport.toList.map (s!"'{·}'") |> ", ".intercalate}" diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index baafbcbb00..d9c1b6e679 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -26,6 +26,8 @@ register_builtin_option structure.strictResolutionOrder : Bool := { open Meta open TSyntax.Compat +namespace Structure + /-! Recall that the `structure command syntax is ``` leading_parser (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> Term.optType >> optional «extends» >> optional (" := " >> optional structCtor >> structFields) @@ -84,7 +86,7 @@ structure StructParentInfo where /-- Whether to add term info to the ref. False if there's no user-provided parent projection. -/ addTermInfo : Bool /-- A let variable that represents this structure parent. -/ - fvar? : Option Expr + fvar : Expr structName : Name /-- Field name for parent. -/ name : Name @@ -92,27 +94,56 @@ structure StructParentInfo where declName : Name /-- Whether this parent corresponds to a `subobject` field. -/ subobject : Bool - type : Expr deriving Inhabited /-- Records the way in which a field is represented in a structure. + +Standard fields are one of `.newField`, `.copiedField`, or `.fromSubobject`. +Parent fields are one of `.subobject` or `.otherParent`. -/ inductive StructFieldKind where - /-- New field defined by this `structure`. - The field is represented as a constructor argument. -/ + /-- New field defined by the `structure`. + Represented as a constructor argument. Will have a projection function. -/ | newField /-- Field that comes from a parent but will be represented as a new field. - The field is represented as a constructor argument. - Its default value may be overridden. -/ + Represented as a constructor argument. Will have a projection function. + Its inherited default value may be overridden. -/ | copiedField /-- Field that comes from a embedded parent field, and is represented within a `subobject` field. - Its default value may be overridden. -/ + Not represented as a constructor argument. Will not have a projection function. + Its inherited default value may be overridden. -/ | fromSubobject - /-- The field is an embedded parent structure. -/ + /-- The field is an embedded parent structure. + Represented as a constructor argument. Will have a projection function. + Default values are not allowed. -/ | subobject (structName : Name) + /-- The field represents a parent projection for a parent that is not itself embedded as a subobject. + (Note: parents of `subobject` fields are `otherParent` fields.) + Not represented as a constructor argument. Will only have a projection function if it is a direct parent. + Default values are not allowed. -/ + | otherParent (structName : Name) deriving Inhabited, DecidableEq, Repr +def StructFieldKind.isFromSubobject (kind : StructFieldKind) : Bool := + kind matches StructFieldKind.fromSubobject + +def StructFieldKind.isSubobject (kind : StructFieldKind) : Bool := + kind matches StructFieldKind.subobject .. + +/-- Returns `true` if the field represents a parent projection. -/ +def StructFieldKind.isParent (kind : StructFieldKind) : Bool := + kind matches StructFieldKind.subobject .. | StructFieldKind.otherParent .. + +/-- Returns `true` if the field is represented as a field in the constructor. -/ +def StructFieldKind.isInCtor (kind : StructFieldKind) : Bool := + kind matches .newField | .copiedField | .subobject .. + +inductive StructFieldDefault where + | optParam (value : Expr) + | autoParam (tactic : Expr) + deriving Repr + /-- Elaborated field info. -/ @@ -121,17 +152,36 @@ structure StructFieldInfo where name : Name kind : StructFieldKind /-- Name of projection function. - Remark: for `fromSubobject` fields, `declName` is only relevant for auxiliary "default value" functions. -/ + Remark: for fields that don't get projection functions (like `fromSubobject` fields), only relevant for the auxiliary "default value" functions. -/ declName : Name + /-- Binder info to use when making the constructor. Only applies to those fields that will appear in the constructor. -/ + binfo : BinderInfo + /-- + Structure names that are responsible for this field being here. + - Empty if the field is a `newField`. + - Otherwise, it is a stack with the last element being a parent in the `extends` clause. + The first element is the (indirect) parent that is responsible for this field. + -/ + sourceStructNames : List Name + /-- Local variable for the field. + All fields (both real fields and parent projection fields) get a local variable. + Parent fields are ldecls constructed from non-parent fields. -/ fvar : Expr - value? : Option Expr := none + /-- An expression representing a `.fromSubobject` field as a projection of a `.subobject` field. + Used when making the constructor. + Note: `.otherParent` fields are let decls, there is no need for `projExpr?`. -/ + projExpr? : Option Expr := none + /-- The default value, as explicitly given in this `structure`. -/ + default? : Option StructFieldDefault := none + /-- The inherited default values, as parent structure / value pairs. -/ + inheritedDefaults : Array (Name × StructFieldDefault) := #[] + /-- The default that will be used for this structure. -/ + resolvedDefault? : Option StructFieldDefault := none deriving Inhabited, Repr -def StructFieldInfo.isFromSubobject (info : StructFieldInfo) : Bool := - info.kind matches StructFieldKind.fromSubobject - -def StructFieldInfo.isSubobject (info : StructFieldInfo) : Bool := - info.kind matches StructFieldKind.subobject .. +/-! +### View construction +-/ private def defaultCtorName := `mk @@ -351,91 +401,218 @@ def structureSyntaxToView (modifiers : Modifiers) (stx : Syntax) : TermElabM Str derivingClasses } -private def findFieldInfo? (infos : Array StructFieldInfo) (fieldName : Name) : Option StructFieldInfo := - infos.find? fun info => info.name == fieldName -private def containsFieldName (infos : Array StructFieldInfo) (fieldName : Name) : Bool := - (findFieldInfo? infos fieldName).isSome +/-! +### Elaboration +-/ -private def replaceFieldInfo (infos : Array StructFieldInfo) (info : StructFieldInfo) : Array StructFieldInfo := - infos.map fun info' => - if info'.name == info.name then - info - else - info' - -/-- Return `some fieldName` if field `fieldName` of the parent structure `parentStructName` is already in `infos` -/ -private def findExistingField? (infos : Array StructFieldInfo) (parentStructName : Name) : CoreM (Option Name) := do - -- Check if `parentStructName` is represented as a subobject field. - if let some info := infos.find? (·.kind == .subobject parentStructName) then - return info.name - -- Otherwise check for field overlap. - let fieldNames := getStructureFieldsFlattened (← getEnv) parentStructName - for fieldName in fieldNames do - if containsFieldName infos fieldName then - return some fieldName - return none - -private def processSubfields (structDeclName : Name) (parentFVar : Expr) (parentStructName : Name) (subfieldNames : Array Name) - (infos : Array StructFieldInfo) (k : Array StructFieldInfo → TermElabM α) : TermElabM α := - go 0 infos -where - go (i : Nat) (infos : Array StructFieldInfo) := do - if h : i < subfieldNames.size then - let subfieldName := subfieldNames[i] - if containsFieldName infos subfieldName then - throwError "field '{subfieldName}' from '{.ofConstName parentStructName}' has already been declared" - let val ← mkProjection parentFVar subfieldName - let type ← inferType val - withLetDecl subfieldName type val fun subfieldFVar => do - /- The following `declName` is only used for creating the `_default` auxiliary declaration name when - its default value is overwritten in the structure. If the default value is not overwritten, then the `declName` is irrelevant. -/ - let declName := structDeclName ++ subfieldName - let infos := infos.push { ref := (← getRef), name := subfieldName, declName, fvar := subfieldFVar, kind := StructFieldKind.fromSubobject } - go (i+1) infos - else - k infos - -/-- Given `obj.foo.bar.baz`, return `obj`. -/ -private partial def getNestedProjectionArg (e : Expr) : MetaM Expr := do - if let Expr.const subProjName .. := e.getAppFn then - if let some { numParams, .. } ← getProjectionFnInfo? subProjName then - if e.getAppNumArgs == numParams + 1 then - return ← getNestedProjectionArg e.appArg! - return e +private structure State where + /-- Immediate parents. -/ + parents : Array StructParentInfo := #[] + /-- All fields, both newly defined and inherited. Every parent has a `StructFieldInfo` too. -/ + fields : Array StructFieldInfo := #[] + /-- Map from field name to its index in `fields`. -/ + fieldIdx : NameMap Nat := {} + /-- Map from structure name to `field` index. -/ + ancestorFieldIdx : NameMap Nat := {} + /-- Map from fvar ids to its index in `fields`. -/ + fvarIdFieldIdx : FVarIdMap Nat := {} + deriving Inhabited /-- - Get field type of `fieldName` in `parentType`, but replace references - to other fields of that structure by existing field fvars. - Auxiliary method for `copyNewFieldsFrom`. - +Monad for elaborating parents and fields of a `structure`. -/ -private def getFieldType (infos : Array StructFieldInfo) (parentType : Expr) (fieldName : Name) : MetaM Expr := do - withLocalDeclD (← mkFreshId) parentType fun parent => do - let proj ← mkProjection parent fieldName - let projType ← inferType proj - /- Eliminate occurrences of `parent.field`. This happens when the structure contains dependent fields. - If the copied parent extended another structure via a subobject, - then the occurrence can also look like `parent.toGrandparent.field` - (where `toGrandparent` is not a field of the current structure). -/ - let visit (e : Expr) : MetaM TransformStep := do - if let Expr.const subProjName .. := e.getAppFn then - if let some { numParams, .. } ← getProjectionFnInfo? subProjName then - let Name.str _ subFieldName .. := subProjName - | throwError "invalid projection name {subProjName}" +private abbrev StructElabM := StateT State TermElabM + +instance : Inhabited (StructElabM α) where + default := throw default + +def runStructElabM (k : StructElabM α) (init : State := {}) : TermElabM α := k.run' init + +private def addParentInfo (parent : StructParentInfo) : StructElabM Unit := do + modify fun s => { s with parents := s.parents.push parent } + +private def findFieldInfo? (fieldName : Name) : StructElabM (Option StructFieldInfo) := do + let s ← get + return s.fieldIdx.find? fieldName |>.map fun idx => s.fields[idx]! + +private def hasFieldName (fieldName : Name) : StructElabM Bool := + return (← get).fieldIdx.contains fieldName + +private def findFieldInfoByFVarId? (fvarId : FVarId) : StructElabM (Option StructFieldInfo) := do + let s ← get + return s.fvarIdFieldIdx.find? fvarId |>.map fun idx => s.fields[idx]! + +/-- +Inserts a field info into the current state. +Throws an error if there is already a field with that name. +-/ +private def addFieldInfo (info : StructFieldInfo) : StructElabM Unit := do + if ← hasFieldName info.name then + throwError "(in addFieldInfo) structure field '{info.name}' already exists" + else + modify fun s => + let idx := s.fields.size + { s with + fields := s.fields.push info + fieldIdx := s.fieldIdx.insert info.name idx + fvarIdFieldIdx := s.fvarIdFieldIdx.insert info.fvar.fvarId! idx + ancestorFieldIdx := + match info.kind with + | .subobject structName | .otherParent structName => + s.ancestorFieldIdx.insert structName idx + | _ => + s.ancestorFieldIdx + } + +private def findParentFieldInfo? (structName : Name) : StructElabM (Option StructFieldInfo) := do + let s ← get + return s.ancestorFieldIdx.find? structName |>.map fun idx => s.fields[idx]! + +/-- +Replaces the field info for a given field. +Throws an error if there is not already a field with that name. +-/ +private def replaceFieldInfo (info : StructFieldInfo) : StructElabM Unit := do + if let some idx := (← get).fieldIdx.find? info.name then + modify fun s => { s with fields := s.fields.set! idx info } + else + throwError "(in replaceFieldInfo) structure field '{info.name}' does not already exist" + +private def addFieldInheritedDefault (fieldName : Name) (structName : Name) (d : StructFieldDefault) : StructElabM Unit := do + let some info ← findFieldInfo? fieldName + | throwError "(in addFieldInheritedDefault) structure field '{fieldName}' does not already exist" + replaceFieldInfo { info with inheritedDefaults := info.inheritedDefaults.push (structName, d) } + +/-- +Reduces projections applied to constructors or parent fvars, for structure types that have appeared as parents. + +If `zetaDelta` is true (default), then zeta reduces parent fvars. +-/ +private def reduceFieldProjs (e : Expr) (zetaDelta := true) : StructElabM Expr := do + let e ← instantiateMVars e + let postVisit (e : Expr) : StructElabM TransformStep := do + if let Expr.const projName .. := e.getAppFn then + if let some projInfo ← getProjectionFnInfo? projName then + let ConstantInfo.ctorInfo cval := (← getEnv).find? projInfo.ctorName | unreachable! + if let some info ← findParentFieldInfo? cval.induct then let args := e.getAppArgs - if let some major := args[numParams]? then - if (← getNestedProjectionArg major) == parent then - if let some existingFieldInfo := findFieldInfo? infos (.mkSimple subFieldName) then - return TransformStep.done <| mkAppN existingFieldInfo.fvar args[numParams+1:args.size] - return TransformStep.done e - let projType ← Meta.transform projType (post := visit) - if projType.containsFVar parent.fvarId! then - throwError "unsupported dependent field in {fieldName} : {projType}" - if let some info := getFieldInfo? (← getEnv) (← getStructureName parentType) fieldName then - if let some autoParamExpr := info.autoParam? then - return (← mkAppM ``autoParam #[projType, autoParamExpr]) - return projType + if let some major := args[projInfo.numParams]? then + let major ← + if zetaDelta && major == info.fvar then + pure <| (← major.fvarId!.getValue?).getD major + else + pure major + if major.isAppOfArity projInfo.ctorName (cval.numParams + cval.numFields) then + if let some arg := major.getAppArgs[projInfo.numParams + projInfo.i]? then + return TransformStep.visit <| mkAppN arg args[projInfo.numParams+1:] + return TransformStep.continue + Meta.transform e (post := postVisit) + +/-- Checks if the expression is of the form `S.mk x.1 ... x.n` with `n` nonzero +and `S.mk` a structure constructor with `S` one of the recorded structure parents. +Returns `x`. +Each projection `x.i` can be either a native projection or from a projection function. -/ +private def etaStruct? (e : Expr) : StructElabM (Option Expr) := do + let .const f _ := e.getAppFn | return none + let some (ConstantInfo.ctorInfo fVal) := (← getEnv).find? f | return none + unless (← findParentFieldInfo? fVal.induct).isSome do return none + unless 0 < fVal.numFields && e.getAppNumArgs == fVal.numParams + fVal.numFields do return none + let args := e.getAppArgs + let some (S0, i0, x) ← getProjectedExpr args[fVal.numParams]! | return none + unless S0 == fVal.induct && i0 == 0 do return none + for i in [1 : fVal.numFields] do + let arg := args[fVal.numParams + i]! + let some (S', i', x') ← getProjectedExpr arg | return none + unless S' == fVal.induct && i' == i && x' == x do return none + return x +where + /-- Given an expression that's either a native projection or a registered projection + function, gives (1) the name of the structure type, (2) the index of the projection, and + (3) the object being projected. -/ + getProjectedExpr (e : Expr) : MetaM (Option (Name × Nat × Expr)) := do + if let .proj S i x := e then + return (S, i, x) + if let .const fn _ := e.getAppFn then + if let some info ← getProjectionFnInfo? fn then + if e.getAppNumArgs == info.numParams + 1 then + if let some (ConstantInfo.ctorInfo fVal) := (← getEnv).find? info.ctorName then + return (fVal.induct, info.i, e.appArg!) + return none + +/-- Runs `etaStruct?` over the whole expression. -/ +private def etaStructReduce (e : Expr) : StructElabM Expr := do + let e ← instantiateMVars e + Meta.transform e (post := fun e => do + if let some e ← etaStruct? e then + return .done e + else + return .continue) + +/-- +Puts an expression into "field normal form". +- All projections of constructors for parent structures are reduced. +- If `zetaDelta` is true (default) then all parent fvars are zeta reduced. +- Constructors of parent structures are eta reduced. +-/ +private def fieldNormalizeExpr (e : Expr) (zetaDelta : Bool := true) : StructElabM Expr := do + etaStructReduce <| ← reduceFieldProjs e (zetaDelta := zetaDelta) + +private def fieldFromMsg (info : StructFieldInfo) : MessageData := + if let some sourceStructName := info.sourceStructNames.head? then + m!"field '{info.name}' from '{.ofConstName sourceStructName}'" + else + m!"field '{info.name}'" + +/-- +Instantiates default value for field `fieldName` set at structure `structName`. +The arguments for the `_default` auxiliary function are provided by `fieldMap`. +After default values are resolved, then the one that is added to the environment +as an `_inherited_default` auxiliary function is normalized; we don't do those normalizations here. +-/ +private partial def getFieldDefaultValue? (structName : Name) (paramMap : NameMap Expr) (fieldName : Name) : StructElabM (Option Expr) := do + match getDefaultFnForField? (← getEnv) structName fieldName with + | none => return none + | some defaultFn => + let cinfo ← getConstInfo defaultFn + let us ← mkFreshLevelMVarsFor cinfo + go? (← instantiateValueLevelParams cinfo us) +where + failed : MetaM (Option Expr) := do + logWarning m!"ignoring default value for field '{fieldName}' defined at '{.ofConstName structName}'" + return none + + go? (e : Expr) : StructElabM (Option Expr) := do + match e with + | Expr.lam n d b c => + if c.isExplicit then + let some info ← findFieldInfo? n | failed + let valType ← inferType info.fvar + if (← isDefEq valType d) then + go? (b.instantiate1 info.fvar) + else + failed + else + let some param := paramMap.find? n | return none + if ← isDefEq (← inferType param) d then + go? (b.instantiate1 param) + else + failed + | e => + let r := if e.isAppOfArity ``id 2 then e.appArg! else e + return some (← reduceFieldProjs r) + +private def getFieldDefault? (structName : Name) (paramMap : NameMap Expr) (fieldName : Name) (autoParam? : Option Expr) : + StructElabM (Option StructFieldDefault) := do + if let some tactic := autoParam? then + trace[Elab.structure] "found autoparam for '{fieldName}' from '{.ofConstName structName}'" + return StructFieldDefault.autoParam tactic + else if let some val ← getFieldDefaultValue? structName (paramMap : NameMap Expr) fieldName then + -- Important: we use `getFieldDefaultValue?` because we want default value definitions, not *inherited* ones, to properly handle diamonds + trace[Elab.structure] "found default value for '{fieldName}' from '{.ofConstName structName}'{indentExpr val}" + return StructFieldDefault.optParam val + else + return none private def toVisibility (fieldInfo : StructureFieldInfo) : CoreM Visibility := do if isProtected (← getEnv) fieldInfo.projFn then @@ -445,165 +622,252 @@ private def toVisibility (fieldInfo : StructureFieldInfo) : CoreM Visibility := else return Visibility.regular -/-- Map from field name to expression representing the field. -/ -abbrev FieldMap := NameMap Expr - -/-- Reduce projections of the structures in `structNames` -/ -private def reduceProjs (e : Expr) (structNames : NameSet) : MetaM Expr := - let reduce (e : Expr) : MetaM TransformStep := do - match (← reduceProjOf? e structNames.contains) with - | some v => return TransformStep.done v - | _ => return TransformStep.done e - transform e (post := reduce) +mutual /-- -Copies the default value for field `fieldName` set at structure `structName`. -The arguments for the `_default` auxiliary function are provided by `fieldMap`. -Recall some of the entries in `fieldMap` are constructor applications, and they needed -to be reduced using `reduceProjs`. Otherwise, the produced default value may be "cyclic". -That is, we reduce projections of the structures in `expandedStructNames`. Here is -an example that shows why the reduction is needed. -``` -structure A where - a : Nat - -structure B where - a : Nat - b : Nat - c : Nat - -structure C extends B where - d : Nat - c := b + d - -structure D extends A, C - -#print D.c._default -``` -Without the reduction, it produces -``` -def D.c._default : A → Nat → Nat → Nat → Nat := -fun toA b c d => id ({ a := toA.a, b := b, c := c : B }.b + d) -``` +Adds `fieldName` of type `fieldType` from structure `structName`. +See `withStructFields` for meanings of other arguments. -/ -private partial def copyDefaultValue? (fieldMap : FieldMap) (expandedStructNames : NameSet) (structName : Name) (fieldName : Name) : - TermElabM (Option Expr) := do - match getDefaultFnForField? (← getEnv) structName fieldName with - | none => return none - | some defaultFn => - let cinfo ← getConstInfo defaultFn - let us ← mkFreshLevelMVarsFor cinfo - go? (← instantiateValueLevelParams cinfo us) -where - failed : TermElabM (Option Expr) := do - logWarning m!"ignoring default value for field '{fieldName}' defined at '{.ofConstName structName}'" - return none +private partial def withStructField (view : StructView) (sourceStructNames : List Name) (inSubobject? : Option Expr) + (structName : Name) (paramMap : NameMap Expr) (fieldName : Name) (fieldType : Expr) + (k : Expr → StructElabM α) : StructElabM α := do + trace[Elab.structure] "withStructField '{.ofConstName structName}', field '{fieldName}'" + let fieldType ← instantiateMVars fieldType + let autoParam? := fieldType.getAutoParamTactic? + let fieldType := fieldType.consumeTypeAnnotations + let env ← getEnv + let some fieldInfo := getFieldInfo? env structName fieldName + | throwError "(withStructField internal error) no such field '{fieldName}' of '{.ofConstName structName}'" + if let some _ := fieldInfo.subobject? then + -- It's a subobject field, add it and its fields + withStruct view (structName :: sourceStructNames) (binfo := fieldInfo.binderInfo) + fieldName fieldType inSubobject? fun info => k info.fvar + else if let some existingField ← findFieldInfo? fieldName then + -- It's a pre-existing field, make sure it is compatible (unless diamonds are not allowed) + if structureDiamondWarning.get (← getOptions) then + logWarning m!"field '{fieldName}' from '{.ofConstName structName}' has already been declared" + let existingFieldType ← inferType existingField.fvar + unless (← isDefEq fieldType existingFieldType) do + throwError "field type mismatch, field '{fieldName}' from parent '{.ofConstName structName}' {← mkHasTypeButIsExpectedMsg fieldType existingFieldType}" + if let some d ← getFieldDefault? structName paramMap fieldName autoParam? then + addFieldInheritedDefault fieldName structName d + k existingField.fvar + else + -- It's a not-yet-seen field + /- For `.fromSubobject`: the following `declName` is only used for creating the `_default`/`_inherited_default` auxiliary declaration name when + its default value is overridden, otherwise the `declName` is irrelevant, except to ensure a declaration is not already declared. -/ + let mut declName := view.declName ++ fieldName + if inSubobject?.isNone then + declName ← applyVisibility (← toVisibility fieldInfo) declName + -- No need to validate links because this docstring was already added to the environment previously + addDocStringCore' declName (← findDocString? (← getEnv) fieldInfo.projFn) + checkNotAlreadyDeclared declName + withLocalDecl fieldName fieldInfo.binderInfo (← reduceFieldProjs fieldType) fun fieldFVar => do + let projExpr? ← inSubobject?.mapM fun subobject => mkProjection subobject fieldName + addFieldInfo { + ref := (← getRef) + sourceStructNames := structName :: sourceStructNames + name := fieldName + declName + kind := if inSubobject?.isSome then .fromSubobject else .copiedField + fvar := fieldFVar + projExpr? + binfo := fieldInfo.binderInfo + } + if let some d ← getFieldDefault? structName paramMap fieldName autoParam? then + addFieldInheritedDefault fieldName structName d + k fieldFVar - go? (e : Expr) : TermElabM (Option Expr) := do - match e with - | Expr.lam n d b c => - if c.isExplicit then - match fieldMap.find? n with - | none => failed - | some val => - let valType ← inferType val - if (← isDefEq valType d) then - go? (b.instantiate1 val) - else - failed +/-- +Adds all the fields from `structType` along with its parent projection fields. +Does not add a parent field for the structure itself; that is done by `withStruct`. +- if `inSubobject?` is `some e`, then `e` must be an expression representing the `.subobject` parent being constructed (a metavariable), + and the added fields are marked `.fromSubobject` and are set to have `e` projections +- `sourceStructNames` is a stack of the structures visited, used for error reporting +- the continuation `k` is run with a constructor expression for this structure +-/ +private partial def withStructFields (view : StructView) (sourceStructNames : List Name) + (structType : Expr) (inSubobject? : Option Expr) (paramMap : NameMap Expr) + (k : Expr → StructElabM α) : StructElabM α := do + let structName ← getStructureName structType + let .const _ us := structType.getAppFn | unreachable! + let params := structType.getAppArgs + + trace[Elab.structure] "withStructFields '{.ofConstName structName}'" + + let env ← getEnv + let fields := getStructureFields env structName + let parentInfos := getStructureParentInfo env structName + + let ctorVal := getStructureCtor env structName + let ctor := mkAppN (mkConst ctorVal.name us) params + let (fieldMVars, _, _) ← forallMetaTelescope (← inferType ctor) + assert! fieldMVars.size == fields.size + + -- Go through all parents to make sure parent projections are consistent. + let rec goParents (s : Expr) (i : Nat) : StructElabM α := do + if h : i < parentInfos.size then + let parentInfo := parentInfos[i] + if parentInfo.subobject then + goParents s (i + 1) else - let arg ← mkFreshExprMVar d - go? (b.instantiate1 arg) - | e => - let r := if e.isAppOfArity ``id 2 then e.appArg! else e - return some (← reduceProjs (← instantiateMVars r) expandedStructNames) + let fieldName := Name.mkSimple parentInfo.projFn.getString! + let fieldType ← inferType <| mkApp (mkAppN (.const parentInfo.projFn us) params) s + withStruct view (structName :: sourceStructNames) (binfo := .default) + fieldName fieldType inSubobject? fun _ => goParents s (i + 1) + else + k s -private partial def copyNewFieldsFrom (structDeclName : Name) (infos : Array StructFieldInfo) (parentType : Expr) (k : Array StructFieldInfo → TermElabM α) : TermElabM α := do - copyFields infos {} parentType fun infos _ _ => k infos -where - copyFields (infos : Array StructFieldInfo) (expandedStructNames : NameSet) (parentType : Expr) (k : Array StructFieldInfo → FieldMap → NameSet → TermElabM α) : TermElabM α := do - let parentStructName ← getStructureName parentType - let fieldNames := getStructureFields (← getEnv) parentStructName - let rec copy (i : Nat) (infos : Array StructFieldInfo) (fieldMap : FieldMap) (expandedStructNames : NameSet) : TermElabM α := do - if h : i < fieldNames.size then - let fieldName := fieldNames[i] - let fieldType ← getFieldType infos parentType fieldName - match findFieldInfo? infos fieldName with - | some existingFieldInfo => - -- TODO: make sure parent projections are checked too - let existingFieldType ← inferType existingFieldInfo.fvar - unless (← isDefEq fieldType existingFieldType) do - throwError "parent field type mismatch, field '{fieldName}' from parent '{.ofConstName parentStructName}' {← mkHasTypeButIsExpectedMsg fieldType existingFieldType}" - /- Remark: if structure has a default value for this field, it will be set at the `processOveriddenDefaultValues` below. -/ - copy (i+1) infos (fieldMap.insert fieldName existingFieldInfo.fvar) expandedStructNames - | none => - let some fieldInfo := getFieldInfo? (← getEnv) parentStructName fieldName | unreachable! - if let some fieldParentStructName := fieldInfo.subobject? then - if (← findExistingField? infos fieldParentStructName).isSome then - -- See comment at `copyDefaultValue?` - let expandedStructNames := expandedStructNames.insert fieldParentStructName - copyFields infos expandedStructNames fieldType fun infos nestedFieldMap expandedStructNames => do - let fieldVal ← mkCompositeField fieldType nestedFieldMap - copy (i+1) infos (fieldMap.insert fieldName fieldVal) expandedStructNames - else - let subfieldNames := getStructureFieldsFlattened (← getEnv) fieldParentStructName - let fieldName := fieldInfo.fieldName - -- This error should never happen: - if let some info := infos.find? (·.kind == .subobject fieldParentStructName) then - throwError "projection field name conflict, ancestor '{.ofConstName fieldParentStructName}' \ - has projection fields '{info.name}' and '{fieldName}'" - withLocalDecl fieldName fieldInfo.binderInfo fieldType fun parentFVar => do - let infos := infos.push { ref := (← getRef) - name := fieldName, declName := structDeclName ++ fieldName, fvar := parentFVar, - kind := StructFieldKind.subobject fieldParentStructName } - processSubfields structDeclName parentFVar fieldParentStructName subfieldNames infos fun infos => - copy (i+1) infos (fieldMap.insert fieldName parentFVar) expandedStructNames - else - withLocalDecl fieldName fieldInfo.binderInfo fieldType fun fieldFVar => do - let fieldMap := fieldMap.insert fieldName fieldFVar - let value? ← copyDefaultValue? fieldMap expandedStructNames parentStructName fieldName - let fieldDeclName := structDeclName ++ fieldName - let fieldDeclName ← applyVisibility (← toVisibility fieldInfo) fieldDeclName - -- No need to validate links because this docstring was already added to the environment previously - addDocStringCore' fieldDeclName (← findDocString? (← getEnv) fieldInfo.projFn) - let infos := infos.push { ref := (← getRef) - name := fieldName, declName := fieldDeclName, fvar := fieldFVar, value?, - kind := StructFieldKind.copiedField } - copy (i+1) infos fieldMap expandedStructNames + let rec goFields (i : Nat) : StructElabM α := do + if h : i < fields.size then + let fieldName := fields[i] + let fieldMVar := fieldMVars[i]! + let fieldType ← inferType fieldMVar + withStructField view sourceStructNames inSubobject? structName paramMap fieldName fieldType fun fieldFVar => do + fieldMVar.mvarId!.assign fieldFVar + goFields (i + 1) + else + let s ← instantiateMVars <| mkAppN ctor fieldMVars + goParents s 0 + + goFields 0 + +/-- +Adds a parent structure and all its fields. +- `structFieldName` is the name to use for the parent field. +- `rawStructFieldName` is name to use in local context, for hygiene. By default it is `structFieldName`. + +See `withStructFields` for meanings of other arguments. +-/ +private partial def withStruct (view : StructView) (sourceStructNames : List Name) (binfo : BinderInfo) + (structFieldName : Name) + (structType : Expr) (inSubobject? : Option Expr) + (k : StructFieldInfo → StructElabM α) + (rawStructFieldName := structFieldName) (projRef := Syntax.missing) : + StructElabM α := do + let env ← getEnv + let structType ← reduceFieldProjs (← whnf structType) + let structName ← getStructureName structType + let params := structType.getAppArgs + trace[Elab.structure] "withStructField '{.ofConstName structName}', using parent field '{structFieldName}'" + if let some info ← findFieldInfo? structFieldName then + -- Exact field name match. If it's a parent, then check defeq, otherwise it's a name conflict. + if info.kind.isParent then + let infoType ← inferType info.fvar + if ← isDefEq infoType structType then + k info else - let infos ← processOveriddenDefaultValues infos fieldMap expandedStructNames parentStructName - k infos fieldMap expandedStructNames - copy 0 infos {} expandedStructNames + throwError "parent type mismatch, {← mkHasTypeButIsExpectedMsg structType infoType}" + else + throwErrorAt projRef "{fieldFromMsg info} has a name conflict with parent projection for '{.ofConstName structName}'\n\n\ + The 'toParent : P' syntax can be used to adjust the name for the parent projection" + else if let some info ← findParentFieldInfo? structName then + -- The field name is different. Error. + assert! structFieldName != info.name + throwErrorAt projRef "expecting '{structFieldName}' to match {fieldFromMsg info} for parent '{.ofConstName structName}'\n\n\ + The 'toParent : P' syntax can be used to adjust the name for the parent projection" + else + -- Main case: there is no field named `structFieldName` and there is no field for the structure `structName` yet. - processOveriddenDefaultValues (infos : Array StructFieldInfo) (fieldMap : FieldMap) (expandedStructNames : NameSet) (parentStructName : Name) : TermElabM (Array StructFieldInfo) := - infos.mapM fun info => do - match (← copyDefaultValue? fieldMap expandedStructNames parentStructName info.name) with - | some value => return { info with value? := value } - | none => return info + let projDeclName := view.declName ++ structFieldName + withRef projRef do checkNotAlreadyDeclared projDeclName - mkCompositeField (parentType : Expr) (fieldMap : FieldMap) : TermElabM Expr := do - let env ← getEnv - let Expr.const parentStructName us ← pure parentType.getAppFn | unreachable! - let parentCtor := getStructureCtor env parentStructName - let mut result := mkAppN (mkConst parentCtor.name us) parentType.getAppArgs - for fieldName in getStructureFields env parentStructName do - match fieldMap.find? fieldName with - | some val => result := mkApp result val - | none => throwError "failed to copy fields from parent structure{indentExpr parentType}" -- TODO improve error message - return result + let allFields := getStructureFieldsFlattened env structName (includeSubobjectFields := false) + let withStructFields' (kind : StructFieldKind) (inSubobject? : Option Expr) (k : StructFieldInfo → StructElabM α) : StructElabM α := do + -- Create a parameter map for default value processing + let info ← getConstInfoInduct structName + let paramMap : NameMap Expr ← forallTelescope info.type fun xs _ => do + let mut paramMap := {} + for param in params, x in xs do + paramMap := paramMap.insert (← x.fvarId!.getUserName) param + return paramMap + withStructFields view sourceStructNames structType inSubobject? paramMap fun structVal => do + if let some _ ← findFieldInfo? structFieldName then + throwErrorAt projRef "field '{structFieldName}' has already been declared\n\n\ + The 'toParent : P' syntax can be used to adjust the name for the parent projection" + -- Add default values. + -- We've added some default values so far, but we want all overridden default values, + -- which for inherited fields might not have been seen yet. + -- Note: duplication is ok for now. We use a stable sort later. + -- TODO(kmill): locate all autoParams too. We are only seeing the ones present in constructors, + -- and we are not correctly handling diamond inheritence. + for fieldName in allFields do + if let some d ← getFieldDefault? structName paramMap fieldName none then + addFieldInheritedDefault fieldName structName d + withLetDecl rawStructFieldName structType structVal fun structFVar => do + let info : StructFieldInfo := { + ref := (← getRef) + sourceStructNames := sourceStructNames + name := structFieldName + declName := projDeclName + fvar := structFVar + binfo := binfo + kind + } + addFieldInfo info + k info -private partial def mkToParentName (parentView : StructParentView) (parentStructName : Name) : Name × Name := + if inSubobject?.isSome then + -- If we are currently in a subobject, then we can't use a subobject to represent this parent. + withStructFields' (.otherParent structName) inSubobject? k + else + /- + If there are no fields, we can avoid representing this structure in the constructor. + This is mainly to support test files that define structures with no fields. + TODO(kmill): remove check that there are any fields so far. + This is to get around some oddities when parent projections are all no-ops (tests fail when it is removed). + TODO(kmill): allow overlapping proof fields between subobjects! This does not harm defeq, and it should be more efficient. + -/ + let elideParent := allFields.isEmpty && (← get).fields.any (·.kind.isInCtor) + if elideParent || (← allFields.anyM hasFieldName) then + -- Or, if there is an overlapping field, we need to copy/reuse fields rather than embed the parent as a subobject. + withStructFields' (.otherParent structName) none k + else + -- Use a subobject for this parent. + -- We create a metavariable to represent the subobject, so that `withStructField` can create projections + let inSubobject ← mkFreshExprMVar structType + withStructFields' (.subobject structName) inSubobject fun info => do + inSubobject.mvarId!.assign info.fvar + k info + +end + +/-- +- `view` is the view of the structure being elaborated +- `projRef` is the ref to use for errors about the projection, set to the current ref when recursing +- `rawStructFieldName` is the name to use for the local declaration for this parent +- `structFieldName` is the field name to use for this parent +- `structType` is the parent's type +- `k` is a continuation that is run with a local context containing the fields and the ancestor fields, + and it's provided the field info for the parent +-/ +private partial def withParent (view : StructView) (projRef : Syntax) + (rawStructFieldName structFieldName : Name) + (structType : Expr) + (k : StructFieldInfo → StructElabM α) : + StructElabM α := do + let env ← getEnv + let structType ← whnf structType + let structName ← getStructureName structType + let binfo := if view.isClass && isClass env structName then BinderInfo.instImplicit else BinderInfo.default + trace[Elab.structure] "binfo for {structFieldName} is {repr binfo}" + withStruct view [] (projRef := projRef) (rawStructFieldName := rawStructFieldName) + (binfo := binfo) (inSubobject? := none) structFieldName structType k + +private def mkToParentName (parentStructName : Name) : Name := + Name.mkSimple <| "to" ++ parentStructName.eraseMacroScopes.getString! + +private def StructParentView.mkToParentNames (parentView : StructParentView) (parentStructName : Name) : Name × Name := match parentView.rawName?, parentView.name? with | some rawName, some name => (rawName, name) - | _, _ => Id.run do - let toParentName := Name.mkSimple <| "to" ++ parentStructName.eraseMacroScopes.getString! + | _, _ => + let toParentName := mkToParentName parentStructName (toParentName, toParentName) -private def withParents (view : StructView) (rs : Array ElabHeaderResult) (indFVar : Expr) - (k : Array StructFieldInfo → Array StructParentInfo → TermElabM α) : TermElabM α := do - go 0 #[] #[] +private def withParents (view : StructView) (rs : Array ElabHeaderResult) (indFVar : Expr) (k : StructElabM α) : StructElabM α := do + go 0 where - go (i : Nat) (infos : Array StructFieldInfo) (parents : Array StructParentInfo) : TermElabM α := do + go (i : Nat) : StructElabM α := do if h : i < view.parents.size then let parentView := view.parents[i] withRef parentView.ref do @@ -613,7 +877,7 @@ where let parentType ← whnf parentType if parentType.getAppFn == indFVar then logWarning "structure extends itself, skipping" - return ← go (i + 1) infos parents + return ← go (i + 1) if rs.any (fun r => r.indFVar == parentType.getAppFn) then throwError "structure cannot extend types defined in the same mutual block" let parentStructName ← try @@ -623,74 +887,27 @@ where This error is possibly due to a change in the 'structure' syntax. \ Now the syntax is 'structure S : Type extends P' rather than 'structure S extends P' : Type'.\n\n\ The purpose of the change is to accommodate 'structure S extends toP : P' syntax for naming parent projections." - let (rawToParentName, toParentName) := mkToParentName parentView parentStructName - -- Name of the parent projection declaration - let declName := view.declName ++ toParentName - withRef parentView.projRef do checkNotAlreadyDeclared declName - let throwParentNameError {β} : TermElabM β := withRef parentView.projRef do - if parentView.name?.isSome then - throwError "field '{toParentName}' has already been declared" - else - throwError "field '{toParentName}' has already been declared, \ - use 'toParent : P' syntax to give a unique name for the parent projection" - if parents.any (·.structName == parentStructName) then + let (rawToParentName, toParentName) := parentView.mkToParentNames parentStructName + if (← get).parents.any (·.structName == parentStructName) then logWarning m!"duplicate parent structure '{.ofConstName parentStructName}', skipping" - go (i + 1) infos parents - else if (← findExistingField? infos parentStructName).isSome || (findFieldInfo? infos toParentName).isSome then - if structureDiamondWarning.get (← getOptions) then - if let some existingFieldName ← findExistingField? infos parentStructName then - logWarning m!"field '{existingFieldName}' from '{.ofConstName parentStructName}' has already been declared" - copyNewFieldsFrom view.declName infos parentType fun infos => do - if let some info := infos.find? (·.kind == .subobject parentStructName) then - if info.name != toParentName then - throwError "parent is an ancestor of a previous parent, but projection name '{toParentName}' does not match '{info.name}'" - pure () - else - if let some info := findFieldInfo? infos toParentName then - unless ← isDefEq (← inferType info.fvar) parentType do - throwParentNameError - if (parents.find? (·.name == toParentName)).isSome then - throwParentNameError - let parents := parents.push { - ref := parentView.projRef - addTermInfo := parentView.name?.isSome - fvar? := none - subobject := false - structName := parentStructName - name := toParentName - declName - type := parentType - } - go (i + 1) infos parents - -- TODO: if `class`, then we need to create a let-decl that stores the local instance for the `parentStructure` + go (i + 1) + else if (← get).parents.any (·.name == toParentName) then + throwError "field '{toParentName}' has already been declared\n\n\ + The 'toParent : P' syntax can be used to adjust the name for the parent projection" else - let env ← getEnv - let subfieldNames := getStructureFieldsFlattened env parentStructName - if containsFieldName infos toParentName || subfieldNames.contains toParentName || (parents.find? (·.name == toParentName)).isSome then - throwParentNameError - let binfo := if view.isClass && isClass env parentStructName then BinderInfo.instImplicit else BinderInfo.default - withLocalDecl rawToParentName binfo parentType fun parentFVar => - let infos := infos.push { - ref := parentView.projRef - name := toParentName - declName - fvar := parentFVar - kind := StructFieldKind.subobject parentStructName - } - let parents := parents.push { + withParent view parentView.projRef rawToParentName toParentName parentType fun parentFieldInfo => do + addParentInfo { ref := parentView.projRef addTermInfo := parentView.name?.isSome - fvar? := parentFVar - subobject := true + fvar := parentFieldInfo.fvar + subobject := parentFieldInfo.kind.isSubobject structName := parentStructName name := toParentName - declName - type := parentType + declName := parentFieldInfo.declName } - processSubfields view.declName parentFVar parentStructName subfieldNames infos fun infos => - go (i+1) infos parents + go (i + 1) else - k infos parents + k private def registerFailedToInferFieldType (fieldName : Name) (e : Expr) (ref : Syntax) : TermElabM Unit := do Term.registerCustomErrorIfMVar (← instantiateMVars e) ref m!"failed to infer type of field '{.ofConstName fieldName}'" @@ -699,7 +916,54 @@ private def registerFailedToInferDefaultValue (fieldName : Name) (e : Expr) (ref Term.registerCustomErrorIfMVar (← instantiateMVars e) ref m!"failed to infer default value for field '{.ofConstName fieldName}'" Term.registerLevelMVarErrorExprInfo e ref m!"failed to infer universe levels in default value for field '{.ofConstName fieldName}'" -private def elabFieldTypeValue (view : StructFieldView) : TermElabM (Option Expr × Option Expr) := +/-- +Goes through all the natural mvars appearing in `e`, assigning any whose type is one of the inherited parents. + +Rationale 1: Structures can only extend a parent once. +There should be no other occurences of a parent except for the parent itself. + +Rationale 2: Consider the following code in the test `lean/run/balg.lean`: +```lean +structure Magma where + α : Type u + mul : α → α → α + +instance : CoeSort Magma (Type u) where + coe s := s.α + +abbrev mul {M : Magma} (a b : M) : M := + M.mul a b + +infixl:70 (priority := high) "*" => mul + +structure Semigroup extends Magma where + mul_assoc (a b c : α) : a * b * c = a * (b * c) +``` +When elaborating `*` in `mul_assoc`'s type, the `M` parameter of `mul` cannot be synthesized by unification. +Now `α` and `mul` are cdecls and `toMagma` is an ldecl, +but it used to be that `toMagma` was the cdecl and `α` and `mul` were projections of it, +which made it possible for unification to infer `toMagma` from `α`. +However, now `α` does not know its relationship to `toMagma`. + +This was not robust, since in diamond inheritance `α` only remembered *one* of its parents in this indirect way. +-/ +private def solveParentMVars (e : Expr) : StructElabM Expr := do + let env ← getEnv + Term.synthesizeSyntheticMVars (postpone := .yes) + let mvars ← getMVarsNoDelayed e + for mvar in mvars do + unless ← mvar.isAssigned do + let decl ← mvar.getDecl + if decl.kind.isNatural then + if let .const name .. := (← whnf decl.type).getAppFn then + if isStructure env name then + if let some parentInfo ← findParentFieldInfo? name then + if ← isDefEq (← mvar.getType) (← inferType parentInfo.fvar) then + discard <| MVarId.checkedAssign mvar parentInfo.fvar + return e + +private def elabFieldTypeValue (view : StructFieldView) : StructElabM (Option Expr × Option StructFieldDefault) := do + let state ← get Term.withAutoBoundImplicit <| Term.withAutoBoundImplicitForbiddenPred (fun n => view.name == n) <| Term.elabBinders view.binders.getArgs fun params => do match view.type? with | none => @@ -710,65 +974,75 @@ private def elabFieldTypeValue (view : StructFieldView) : TermElabM (Option Expr -- TODO: add forbidden predicate using `shortDeclName` from `view` let params ← Term.addAutoBoundImplicits params (view.nameId.getTailPos? (canonicalOnly := true)) let value ← Term.withoutAutoBoundImplicit <| Term.elabTerm valStx none + let value ← runStructElabM (init := state) <| solveParentMVars value registerFailedToInferFieldType view.name (← inferType value) view.nameId registerFailedToInferDefaultValue view.name value valStx let value ← mkLambdaFVars params value - return (none, value) + return (none, StructFieldDefault.optParam value) | some typeStx => let type ← Term.elabType typeStx + let type ← runStructElabM (init := state) <| solveParentMVars type registerFailedToInferFieldType view.name type typeStx Term.synthesizeSyntheticMVarsNoPostponing let params ← Term.addAutoBoundImplicits params (view.nameId.getTailPos? (canonicalOnly := true)) match view.value? with | none => - let type ← mkForallFVars params type - return (type, none) + let type ← mkForallFVars params type + let type ← instantiateMVars type + if let some tactic := type.getAutoParamTactic? then + return (type.consumeTypeAnnotations, StructFieldDefault.autoParam tactic) + else + return (type, none) | some valStx => let value ← Term.withoutAutoBoundImplicit <| Term.elabTermEnsuringType valStx type + let value ← runStructElabM (init := state) <| solveParentMVars value registerFailedToInferDefaultValue view.name value valStx Term.synthesizeSyntheticMVarsNoPostponing let type ← mkForallFVars params type let value ← mkLambdaFVars params value - return (type, value) + return (type, StructFieldDefault.optParam value) -private partial def withFields (parents : Array StructParentInfo) (views : Array StructFieldView) (infos : Array StructFieldInfo) (k : Array StructFieldInfo → TermElabM α) : TermElabM α := do - go 0 {} infos +private partial def withFields (views : Array StructFieldView) (k : StructElabM α) : StructElabM α := do + go 0 where - go (i : Nat) (defaultValsOverridden : NameSet) (infos : Array StructFieldInfo) : TermElabM α := do + go (i : Nat) : StructElabM α := do if h : i < views.size then let view := views[i] withRef view.ref do - if let some parent := parents.find? (·.name == view.name) then + if let some parent := (← get).parents.find? (·.name == view.name) then throwError "field '{view.name}' has already been declared as a projection for parent '{.ofConstName parent.structName}'" - match findFieldInfo? infos view.name with + match ← findFieldInfo? view.name with | none => - let (type?, value?) ← elabFieldTypeValue view - match type?, value? with + let (type?, default?) ← elabFieldTypeValue view + match type?, default? with | none, none => throwError "invalid field, type expected" | some type, _ => - withLocalDecl view.rawName view.binderInfo type fun fieldFVar => - let infos := infos.push { ref := view.nameId - name := view.name, declName := view.declName, fvar := fieldFVar, value? := value?, - kind := StructFieldKind.newField } - go (i+1) defaultValsOverridden infos - | none, some value => + withLocalDecl view.rawName view.binderInfo type fun fieldFVar => do + addFieldInfo { ref := view.nameId, sourceStructNames := [], + name := view.name, declName := view.declName, fvar := fieldFVar, default? := default?, + binfo := view.binderInfo, + kind := StructFieldKind.newField } + go (i+1) + | none, some (.optParam value) => let type ← inferType value - withLocalDecl view.rawName view.binderInfo type fun fieldFVar => - let infos := infos.push { ref := view.nameId - name := view.name, declName := view.declName, fvar := fieldFVar, value? := value, - kind := StructFieldKind.newField } - go (i+1) defaultValsOverridden infos + withLocalDecl view.rawName view.binderInfo type fun fieldFVar => do + addFieldInfo { ref := view.nameId, sourceStructNames := [], + name := view.name, declName := view.declName, fvar := fieldFVar, default? := default?, + binfo := view.binderInfo, + kind := StructFieldKind.newField } + go (i+1) + | none, some (.autoParam _) => + throwError "field '{view.name}' has an autoparam but no type" | some info => - let updateDefaultValue : TermElabM α := do + let updateDefaultValue : StructElabM α := do match view.value? with | none => throwError "field '{view.name}' has been declared in parent structure" | some valStx => if let some type := view.type? then throwErrorAt type "omit field '{view.name}' type to set default value" else - if defaultValsOverridden.contains info.name then + if info.default?.isSome then throwError "field '{view.name}' new default value has already been set" - let defaultValsOverridden := defaultValsOverridden.insert info.name let mut valStx := valStx if view.binders.getArgs.size > 0 then valStx ← `(fun $(view.binders.getArgs)* => $valStx:term) @@ -776,15 +1050,16 @@ where let value ← Term.elabTermEnsuringType valStx fvarType registerFailedToInferDefaultValue view.name value valStx pushInfoLeaf <| .ofFieldRedeclInfo { stx := view.ref } - let infos := replaceFieldInfo infos { info with ref := view.nameId, value? := value } - go (i+1) defaultValsOverridden infos + replaceFieldInfo { info with ref := view.nameId, default? := StructFieldDefault.optParam value } + go (i+1) match info.kind with | StructFieldKind.newField => throwError "field '{view.name}' has already been declared" - | StructFieldKind.subobject n => throwError "unexpected reference to subobject field '{n}'" -- improve error message - | StructFieldKind.copiedField => updateDefaultValue + | StructFieldKind.subobject n + | StructFieldKind.otherParent n => throwError "unexpected reference to parent field '{n}'" -- improve error message + | StructFieldKind.copiedField | StructFieldKind.fromSubobject => updateDefaultValue else - k infos + k private def collectUsedFVars (lctx : LocalContext) (localInsts : LocalInstances) (fieldInfos : Array StructFieldInfo) : StateRefT CollectFVars.State MetaM Unit := do @@ -792,31 +1067,109 @@ private def collectUsedFVars (lctx : LocalContext) (localInsts : LocalInstances) fieldInfos.forM fun info => do let fvarType ← inferType info.fvar fvarType.collectFVars - if let some value := info.value? then + if let some (.optParam value) := info.default? then value.collectFVars -private def addCtorFields (fieldInfos : Array StructFieldInfo) : Nat → Expr → TermElabM Expr - | 0, type => pure type - | i+1, type => do - let info := fieldInfos[i]! - let decl ← Term.getFVarLocalDecl! info.fvar - let type ← instantiateMVars type - let type := type.abstract #[info.fvar] - match info.kind with - | StructFieldKind.fromSubobject => - let val := decl.value - addCtorFields fieldInfos i (type.instantiate1 val) - | _ => - addCtorFields fieldInfos i (mkForall decl.userName decl.binderInfo decl.type type) +/-- +Creates a local context suitable for creating the constructor. +- Eliminates fields with a `projExpr?` field +- Eliminates non-subobject parent fields +- Adds autoParam for default values -private def mkCtor (view : StructView) (r : ElabHeaderResult) (params : Array Expr) (fieldInfos : Array StructFieldInfo) : TermElabM Constructor := +Does not do any reductions. +-/ +private def mkCtorLCtx : StructElabM LocalContext := do + let fieldInfos := (← get).fields + -- A map of all field fvars to eliminate + let mut fvarMap : ExprMap Expr := {} + let mut lctx ← instantiateLCtxMVars (← getLCtx) + let replace (fvarMap : ExprMap Expr) (e : Expr) : Expr := e.replace fun e' => fvarMap[e']? + -- As we build the map, we eagerly do the replacements. We go through the local context in order, so replacements do not need to be recursive. + let insert (fvarMap : ExprMap Expr) (field : StructFieldInfo) (e : Expr) : MetaM (ExprMap Expr) := do + let e ← instantiateMVars e + return fvarMap.insert field.fvar (replace fvarMap e) + for field in fieldInfos do + let fvarId := field.fvar.fvarId! + if !field.kind.isInCtor then + lctx := lctx.erase fvarId + let some e ← pure field.projExpr? <||> fvarId.getValue? + | throwError "(mkCtorLCtx internal error) non-constructor field has no value" + fvarMap ← insert fvarMap field e + else + -- Do replacements. + -- If it is a subobject field, change the ldecl to be a cdecl + lctx := lctx.modifyLocalDecl fvarId fun decl => + .cdecl decl.index decl.fvarId decl.userName (replace fvarMap decl.type) field.binfo decl.kind + -- Add autoParams + if let some (.autoParam tactic) := field.resolvedDefault? then + let u ← getLevel (← inferType field.fvar) + lctx := lctx.modifyLocalDecl fvarId fun decl => decl.setType (mkApp2 (.const ``autoParam [u]) decl.type tactic) + return lctx + +/-- +Builds a constructor for the type, for adding the inductive type to the environment. +-/ +private def mkCtor (view : StructView) (r : ElabHeaderResult) (params : Array Expr) : StructElabM Constructor := withRef view.ref do - let type := mkAppN r.indFVar params - let type ← addCtorFields fieldInfos fieldInfos.size type - let type ← mkForallFVars params type - let type ← instantiateMVars type - let type := type.inferImplicit params.size true - pure { name := view.ctor.declName, type } + let lctx ← mkCtorLCtx + let type ← instantiateMVars <| mkAppN r.indFVar params + let fieldInfos := (← get).fields + let fieldCtorFVars := fieldInfos |>.filter (·.kind.isInCtor) |>.map (·.fvar) + let type := lctx.mkForall fieldCtorFVars type + withLCtx lctx {} do + trace[Elab.structure] "constructor type before reductions:{indentExpr type}" + let type ← fieldNormalizeExpr type + trace[Elab.structure] "constructor type after reductions:{indentExpr type}" + let type ← mkForallFVars params type + let type ← instantiateMVars type + let type := type.inferImplicit params.size true + trace[Elab.structure] "full constructor type:{indentExpr type}" + pure { name := view.ctor.declName, type } + +/-- +Creates an alternative constructor that takes all the fields directly. +Assumes the inductive type has already been added to the environment. + +Note: we can't generally use optParams here since the default values might depend on previous ones. +We include autoParams however. +-/ +private partial def mkFlatCtorExpr (levelParams : List Name) (params : Array Expr) (structName : Name) (replaceIndFVars : Expr → MetaM Expr) : + StructElabM Expr := do + let env ← getEnv + -- build the constructor application using the fields in the local context + let ctor := getStructureCtor env structName + let mut val := mkAppN (mkConst ctor.name (levelParams.map mkLevelParam)) params + let fieldInfos := (← get).fields + for fieldInfo in fieldInfos do + if fieldInfo.kind.isInCtor then + val := mkApp val fieldInfo.fvar + -- zeta delta reduce the parent ldecls + let parentFVars := fieldInfos |>.filter (·.kind.isParent) |>.map (·.fvar.fvarId!) + val ← zetaDeltaFVars (← instantiateMVars val) parentFVars + -- abstract all non-parent fields to make a lambda expression + let fields' := fieldInfos |>.filter (!·.kind.isParent) + val ← fields'.foldrM (init := val) fun fieldInfo val => do + let decl ← fieldInfo.fvar.fvarId!.getDecl + let type ← + match fieldInfo.resolvedDefault? with + | some (.autoParam tactic) => mkAppM ``autoParam #[decl.type, tactic] + | _ => pure decl.type + let type ← zetaDeltaFVars (← instantiateMVars type) parentFVars + let type ← replaceIndFVars type + return .lam decl.userName type (val.abstract #[fieldInfo.fvar]) decl.binderInfo + val ← mkLambdaFVars params val + val ← replaceIndFVars val + fieldNormalizeExpr val + +private partial def mkFlatCtor (levelParams : List Name) (params : Array Expr) (structName : Name) (replaceIndFVars : Expr → MetaM Expr) : + StructElabM Unit := do + let val ← mkFlatCtorExpr levelParams params structName replaceIndFVars + withLCtx {} {} do trace[Elab.structure] "created flat constructor:{indentExpr val}" + unless val.hasSyntheticSorry do + let flatCtorName := mkFlatCtorOfStructName structName + let valType ← replaceIndFVars (← instantiateMVars (← inferType val)) + let valType := valType.inferImplicit params.size true + addDecl <| Declaration.defnDecl (← mkDefinitionValInferrringUnsafe flatCtorName levelParams valType val .abbrev) private partial def checkResultingUniversesForFields (fieldInfos : Array StructFieldInfo) (u : Level) : TermElabM Unit := do for info in fieldInfos do @@ -831,11 +1184,11 @@ private partial def checkResultingUniversesForFields (fieldInfos : Array StructF private def addProjections (r : ElabHeaderResult) (fieldInfos : Array StructFieldInfo) : TermElabM Unit := do let projDecls : Array StructProjDecl := fieldInfos - |>.filter (!·.isFromSubobject) + |>.filter (·.kind.isInCtor) |>.map (fun info => { ref := info.ref, projName := info.declName }) mkProjections r.view.declName projDecls r.view.isClass for fieldInfo in fieldInfos do - if fieldInfo.isSubobject then + if fieldInfo.kind.isSubobject then addDeclarationRangesFromSyntax fieldInfo.declName r.view.ref fieldInfo.ref for decl in projDecls do -- projections may generate equation theorems @@ -843,23 +1196,23 @@ private def addProjections (r : ElabHeaderResult) (fieldInfos : Array StructFiel private def registerStructure (structName : Name) (infos : Array StructFieldInfo) : TermElabM Unit := do let fields ← infos.filterMapM fun info => do - if info.kind == StructFieldKind.fromSubobject then - return none - else + if info.kind.isInCtor then return some { fieldName := info.name projFn := info.declName - binderInfo := (← getFVarLocalDecl info.fvar).binderInfo - autoParam? := (← inferType info.fvar).getAutoParamTactic? + binderInfo := info.binfo + autoParam? := if let some (.autoParam tactic) := info.resolvedDefault? then some tactic else none subobject? := if let .subobject parentName := info.kind then parentName else none } + else + return none modifyEnv fun env => Lean.registerStructure env { structName, fields } private def checkDefaults (fieldInfos : Array StructFieldInfo) : TermElabM Unit := do let mut mvars := {} let mut lmvars := {} for fieldInfo in fieldInfos do - if let some value := fieldInfo.value? then + if let some (.optParam value) := fieldInfo.resolvedDefault? then let value ← instantiateMVars value mvars := Expr.collectMVars mvars value lmvars := collectLevelMVars lmvars value @@ -869,10 +1222,47 @@ private def checkDefaults (fieldInfos : Array StructFieldInfo) : TermElabM Unit else if ← Term.logUnassignedLevelMVarsUsingErrorInfos lmvars.result then return -private def addDefaults (params : Array Expr) (replaceIndFVars : Expr → MetaM Expr) (fieldInfos : Array StructFieldInfo) : TermElabM Unit := do +/-- +Computes the resolution order and for the structure and sorts the inherited defaults. +-/ +private def resolveFieldDefaults (structName : Name) : StructElabM Unit := do + -- Resolve the order, but don't report any resolution order issues at this point. + -- We will do that in `checkResolutionOrder`, which is after the structure is registered. + let { resolutionOrder, .. } ← mergeStructureResolutionOrders structName ((← get).parents.map (·.structName)) (relaxed := true) + let mut resOrderMap : NameMap Nat := {} + for h : i in [0:resolutionOrder.size] do + resOrderMap := resOrderMap.insert resolutionOrder[i] i + for fieldInfo in (← get).fields do + if fieldInfo.default?.isSome then + replaceFieldInfo { fieldInfo with resolvedDefault? := fieldInfo.default? } + else if !fieldInfo.inheritedDefaults.isEmpty then + let inheritedDefaults := fieldInfo.inheritedDefaults.insertionSort fun d1 d2 => resOrderMap.find! d1.1 < resOrderMap.find! d2.1 + trace[Elab.structure] "inherited defaults for '{fieldInfo.name}' are {repr inheritedDefaults}" + replaceFieldInfo { fieldInfo with + inheritedDefaults + resolvedDefault? := inheritedDefaults[0]?.map (·.2) + } + +/-- +Adds declarations representing default values to the environment. + +- Default values introduced for this structure specifically are registered under the name given by `mkDefaultFnOfProjFn` +- Default values inherited by this structure are registered under the name given by `mkInheritedDefaultFnOfProjFn` + +Having both is how we are able to handle diamond inheritance of default values. +When a `structure` extends other structures, only the first type of default values are considered. + +In both cases, the default values take the fields as arguments, and everything is suitably normalized. +It used to be that subobject fields would appear as fields too, but that required +the structure instance notation elaborator to do reductions when making use of default values. +This arrangement of having declarations for all inherited values also makes +the structure instance notation delaborator able to omit default values reliably. +-/ +private def addDefaults (params : Array Expr) (replaceIndFVars : Expr → MetaM Expr) : StructElabM Unit := do + let fieldInfos := (← get).fields let lctx ← getLCtx /- The `lctx` and `defaultAuxDecls` are used to create the auxiliary "default value" declarations - The parameters `params` for these definitions must be marked as implicit, and all others as explicit. -/ + The parameters `params` for these definitions must be marked as implicit, and all others as explicit. -/ let lctx := params.foldl (init := lctx) fun (lctx : LocalContext) (p : Expr) => if p.isFVar then @@ -881,7 +1271,7 @@ private def addDefaults (params : Array Expr) (replaceIndFVars : Expr → MetaM lctx let lctx := fieldInfos.foldl (init := lctx) fun (lctx : LocalContext) (info : StructFieldInfo) => - if info.isFromSubobject then lctx -- `fromSubobject` fields are elaborated as let-decls, and are zeta-expanded when creating "default value" auxiliary functions + if info.kind.isParent then lctx else lctx.setBinderInfo info.fvar.fvarId! BinderInfo.default -- Make all indFVar replacements in the local context. let lctx ← @@ -895,19 +1285,23 @@ private def addDefaults (params : Array Expr) (replaceIndFVars : Expr → MetaM let value ← replaceIndFVars value return lctx.mkLetDecl fvarId userName type value nonDep k withLCtx lctx (← getLocalInstances) do - fieldInfos.forM fun fieldInfo => do - if let some value := fieldInfo.value? then - let declName := mkDefaultFnOfProjFn fieldInfo.declName - let type ← replaceIndFVars (← inferType fieldInfo.fvar) - let value ← instantiateMVars (← replaceIndFVars value) - trace[Elab.structure] "default value after 'replaceIndFVars': {indentExpr value}" - -- If there are mvars, `checkDefaults` already logged an error. - unless value.hasMVar || value.hasSyntheticSorry do - /- The identity function is used as "marker". -/ - let value ← mkId value - -- No need to compile the definition, since it is only used during elaboration. - discard <| mkAuxDefinition declName type value (zetaDelta := true) (compile := false) - setReducibleAttribute declName + let addDefault (fieldInfo : StructFieldInfo) (declName : Name) (value : Expr) : StructElabM Unit := do + let type ← replaceIndFVars (← inferType fieldInfo.fvar) + let value ← instantiateMVars (← replaceIndFVars value) + let value ← fieldNormalizeExpr value + trace[Elab.structure] "default value after 'replaceIndFVars': {indentExpr value}" + -- If there are mvars, `checkDefaults` already logged an error. + unless value.hasMVar || value.hasSyntheticSorry do + /- The identity function is used as "marker". -/ + let value ← mkId value + -- No need to compile the definition, since it is only used during elaboration. + discard <| mkAuxDefinition declName type value (zetaDelta := true) (compile := false) + setReducibleAttribute declName + for fieldInfo in fieldInfos do + if let some (.optParam value) := fieldInfo.default? then + addDefault fieldInfo (mkDefaultFnOfProjFn fieldInfo.declName) value + else if let some (.optParam value) := fieldInfo.resolvedDefault? then + addDefault fieldInfo (mkInheritedDefaultFnOfProjFn fieldInfo.declName) value /-- Given `type` of the form `forall ... (source : A), B`, return `forall ... [source : A], B`. @@ -924,34 +1318,15 @@ private def setSourceInstImplicit (type : Expr) : Expr := /-- Creates a projection function to a non-subobject parent. -/ -private partial def mkCoercionToCopiedParent (levelParams : List Name) (params : Array Expr) (view : StructView) (source : Expr) (parent : StructParentInfo) (parentType : Expr) : MetaM StructureParentInfo := do +private partial def mkCoercionToCopiedParent (levelParams : List Name) (params : Array Expr) (view : StructView) (source : Expr) (parent : StructParentInfo) (parentType parentVal : Expr) : MetaM StructureParentInfo := do let isProp ← Meta.isProp parentType let env ← getEnv - let structName := view.declName - let sourceFieldNames := getStructureFieldsFlattened env structName let binfo := if view.isClass && isClass env parent.structName then BinderInfo.instImplicit else BinderInfo.default let mut declType ← instantiateMVars (← mkForallFVars params (← mkForallFVars #[source] parentType)) if view.isClass && isClass env parent.structName then declType := setSourceInstImplicit declType declType := declType.inferImplicit params.size true - let rec copyFields (parentType : Expr) : MetaM Expr := do - let Expr.const parentStructName us ← pure parentType.getAppFn | unreachable! - let parentCtor := getStructureCtor env parentStructName - let mut result := mkAppN (mkConst parentCtor.name us) parentType.getAppArgs - for fieldName in getStructureFields env parentStructName do - if sourceFieldNames.contains fieldName then - let fieldVal ← mkProjection source fieldName - result := mkApp result fieldVal - else - -- fieldInfo must be a field of `parentStructName` - let some fieldInfo := getFieldInfo? env parentStructName fieldName | unreachable! - if fieldInfo.subobject?.isNone then throwError "failed to build coercion to parent structure" - let resultType ← whnfD (← inferType result) - unless resultType.isForall do throwError "failed to build coercion to parent structure, unexpected type{indentExpr resultType}" - let fieldVal ← copyFields resultType.bindingDomain! - result := mkApp result fieldVal - return result - let declVal ← instantiateMVars (← mkLambdaFVars params (← mkLambdaFVars #[source] (← copyFields parentType))) + let declVal ← instantiateMVars (← mkLambdaFVars params (← mkLambdaFVars #[source] parentVal)) let declName := parent.declName -- Logic from `mk_projections`: prop-valued projections are theorems (or at least opaque) let cval : ConstantVal := { name := declName, levelParams, type := declType } @@ -975,31 +1350,51 @@ private partial def mkCoercionToCopiedParent (levelParams : List Name) (params : addDeclarationRangesFromSyntax declName view.ref parent.ref return { structName := parent.structName, subobject := false, projFn := declName } -private def mkRemainingProjections (levelParams : List Name) (params : Array Expr) (view : StructView) - (parents : Array StructParentInfo) (fieldInfos : Array StructFieldInfo) : TermElabM (Array StructureParentInfo) := do - let structType := mkAppN (Lean.mkConst view.declName (levelParams.map mkLevelParam)) params +/-- +Make projections to parents that are not represented as subobjects. + +All other projections we get indirectly from the elaborator, which can construct projections by chaining subobject projections. +-/ +private def mkRemainingProjections (levelParams : List Name) (params : Array Expr) (view : StructView) : StructElabM (Array StructureParentInfo) := do + let us := levelParams.map mkLevelParam + let structType := mkAppN (Lean.mkConst view.declName us) params withLocalDeclD `self structType fun source => do /- Remark: copied parents might still be referring to the fvars of other parents. We need to replace these fvars with projection constants. For subobject parents, this has already been done by `mkProjections`. https://github.com/leanprover/lean4/issues/2611 -/ - let mut parentInfos := #[] - let mut parentFVarToConst : ExprMap Expr := {} - for h : i in [0:parents.size] do - let parent := parents[i] - let parentInfo : StructureParentInfo ← (do - if parent.subobject then - let some info := fieldInfos.find? (·.kind == .subobject parent.structName) | unreachable! - pure { structName := parent.structName, subobject := true, projFn := info.declName } + let mut fvarToConst : ExprMap Expr := {} + -- First add all constructor projections to `fvarToConst` + for field in (← get).fields do + if field.kind.isInCtor then + fvarToConst := fvarToConst.insert field.fvar <| mkApp (mkAppN (.const field.declName us) params) source + -- Then add remaining fields to `fvarToConst` + for field in (← get).fields do + if !field.kind.isInCtor then + if let some val ← pure field.projExpr? <||> field.fvar.fvarId!.getValue? then + let val ← instantiateMVars val + let val := val.replace (fvarToConst[·]?) + -- No need to zeta delta reduce; `fvarToConst` has replaced such fvars. + let val ← fieldNormalizeExpr val (zetaDelta := false) + fvarToConst := fvarToConst.insert field.fvar val + -- TODO(kmill): if it is a direct parent, add the coercion function the environment and use that instead of `val`, + -- and evaluate the difference. else - let parent_type := (← instantiateMVars parent.type).replace fun e => parentFVarToConst[e]? - mkCoercionToCopiedParent levelParams params view source parent parent_type) - parentInfos := parentInfos.push parentInfo - if let some fvar := parent.fvar? then - parentFVarToConst := parentFVarToConst.insert fvar <| - mkApp (mkAppN (.const parentInfo.projFn (levelParams.map mkLevelParam)) params) source - pure parentInfos + throwError m!"(mkRemainingProjections internal error) {field.name} has no value" + + let mut parentInfos := #[] + for parent in (← get).parents do + if parent.subobject then + let some info ← findParentFieldInfo? parent.structName | unreachable! + parentInfos := parentInfos.push { structName := parent.structName, subobject := true, projFn := info.declName } + else + let parent_type := (← instantiateMVars (← inferType parent.fvar)).replace (fvarToConst[·]?) + let parent_type ← fieldNormalizeExpr parent_type (zetaDelta := false) + let parent_value := fvarToConst[parent.fvar]! + let parentInfo ← mkCoercionToCopiedParent levelParams params view source parent parent_type parent_value + parentInfos := parentInfos.push parentInfo + return parentInfos /-- Precomputes the structure's resolution order. @@ -1038,14 +1433,18 @@ def elabStructureCommand : InductiveElabDescr where trace[Elab.structure] "view.levelNames: {view.levelNames}" return { view := view.toInductiveView - elabCtors := fun rs r params => do - withParents view rs r.indFVar fun parentFieldInfos parents => - withFields parents view.fields parentFieldInfos fun fieldInfos => do + elabCtors := fun rs r params => runStructElabM do + withParents view rs r.indFVar do + withFields view.fields do withRef view.ref do Term.synthesizeSyntheticMVarsNoPostponing + resolveFieldDefaults view.declName + let state ← get + let parents := state.parents + let fieldInfos := state.fields let lctx ← getLCtx let localInsts ← getLocalInstances - let ctor ← mkCtor view r params fieldInfos + let ctor ← mkCtor view r params return { ctors := [ctor] collectUsedFVars := collectUsedFVars lctx localInsts fieldInfos @@ -1061,7 +1460,7 @@ def elabStructureCommand : InductiveElabDescr where if (← getEnv).contains field.declName then Term.addTermInfo' field.ref (← mkConstWithLevelParams field.declName) (isBinder := true) finalize := fun levelParams params replaceIndFVars => do - let parentInfos ← mkRemainingProjections levelParams params view parents fieldInfos + let parentInfos ← runStructElabM (init := state) <| withLCtx lctx localInsts <| mkRemainingProjections levelParams params view withSaveInfoContext do -- Add terminfo for parents now that all parent projections exist. for parent in parents do @@ -1072,9 +1471,10 @@ def elabStructureCommand : InductiveElabDescr where if view.isClass then addParentInstances parentInfos - withLCtx lctx localInsts do - addDefaults params replaceIndFVars fieldInfos + runStructElabM (init := state) <| withLCtx lctx localInsts do + mkFlatCtor levelParams params view.declName replaceIndFVars + addDefaults params replaceIndFVars } } -end Lean.Elab.Command +end Lean.Elab.Command.Structure diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index 7480d96ee4..52350a98c4 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -556,18 +556,13 @@ def delabDelayedAssignedMVar : Delab := whenNotPPOption getPPMVarsDelayed do delabMVarAux decl.mvarIdPending private partial def collectStructFields + (structName : Name) + (paramMap : NameMap Expr) (fields : Array (TSyntax ``Parser.Term.structInstField)) (fieldValues : NameMap Expr) (s : ConstructorVal) : DelabM (NameMap Expr × Array (TSyntax ``Parser.Term.structInstField)) := do let env ← getEnv - -- For default value handling, we need to create a map of type parameter names to expressions. - let args := (← getExpr).getAppArgs - let paramMap : NameMap Expr ← forallTelescope s.type fun xs _ => do - let mut paramMap := {} - for i in [:s.numParams] do - paramMap := paramMap.insert (← xs[i]!.fvarId!.getUserName) args[i]! - return paramMap let fieldNames := getStructureFields env s.induct let (_, fieldValues, fields) ← withBoundedAppFnArgs s.numFields (do return (0, fieldValues, fields)) @@ -580,11 +575,11 @@ private partial def collectStructFields if ← getPPOption getPPStructureInstancesFlatten then if let some s' ← isConstructorApp? (← getExpr) then if s'.induct == parentName then - let (fieldValues, fields) ← collectStructFields fields fieldValues s' + let (fieldValues, fields) ← collectStructFields structName paramMap fields fieldValues s' return (i + 1, fieldValues, fields) /- Does it have the default value, and should it be omitted? -/ unless ← getPPOption getPPStructureInstancesDefaults do - if let some defFn := getDefaultFnForField? (← getEnv) s.induct fieldName then + if let some defFn := getEffectiveDefaultFnForField? (← getEnv) structName fieldName then let cinfo ← getConstInfo defFn let defValue := cinfo.instantiateValueLevelParams! (← mkFreshLevelMVarsFor cinfo) if let some defValue ← withNewMCtxDepth <| processDefaultValue paramMap fieldValues defValue then @@ -668,7 +663,14 @@ def delabStructureInstance : Delab := do If `pp.structureInstances.flatten` is true (and `pp.explicit` is false or the subobject has no parameters) then subobjects are flattened. -/ - let (_, fields) ← collectStructFields #[] {} s + -- For default value handling, we need to create a map of type parameter names to expressions. + let args := (← getExpr).getAppArgs + let paramMap : NameMap Expr ← forallTelescope s.type fun xs _ => do + let mut paramMap := {} + for param in args[:s.numParams], x in xs do + paramMap := paramMap.insert (← x.fvarId!.getUserName) param + return paramMap + let (_, fields) ← collectStructFields s.induct paramMap #[] {} s if ← withType <| getPPOption getPPStructureInstanceType then let tyStx ← withType delab `({ $fields,* : $tyStx }) diff --git a/src/Lean/Structure.lean b/src/Lean/Structure.lean index 0ab8c071b0..14f96c26fc 100644 --- a/src/Lean/Structure.lean +++ b/src/Lean/Structure.lean @@ -193,6 +193,20 @@ partial def findField? (env : Environment) (structName : Name) (fieldName : Name else getStructureSubobjects env structName |>.findSome? fun parentStructName => findField? env parentStructName fieldName +/-- +Gets the name for a structure constructor where the fields have been fully flattened. +This constructor simulates a flat representation for structures, +and it is used by structure instance notation when elaborating structure fields +and for organizing the fields into subobjects. + +The body of the flat constructor has the following properties (recursively): +- the fields come in order +- for subobject fields, the value is the unfolded flat constructor for that field +- for standard fields, the value is one of the flat constructor parameters +-/ +def mkFlatCtorOfStructName (structName : Name) : Name := + structName ++ `_flat_ctor + private partial def getStructureFieldsFlattenedAux (env : Environment) (structName : Name) (fullNames : Array Name) (includeSubobjectFields : Bool) : Array Name := (getStructureFields env structName).foldl (init := fullNames) fun fullNames fieldName => match isSubobjectField? env structName fieldName with @@ -239,19 +253,41 @@ def getProjFnInfoForField? (env : Environment) (structName : Name) (fieldName : else none -/-- Get the name of the auxiliary definition that would have the default value for the structure field. -/ +/-- +Gets the name of the auxiliary definition that would have the default value for the structure field if it exists. +-/ def mkDefaultFnOfProjFn (projFn : Name) : Name := projFn ++ `_default -def getDefaultFnForField? (env : Environment) (structName : Name) (fieldName : Name) : Option Name := +/-- +Gets the name of the auxiliary definition that would have the inherited default value for the structure field if it exists. +-/ +def mkInheritedDefaultFnOfProjFn (projFn : Name) : Name := + projFn ++ `_inherited_default + +private def getFnForFieldUsing? (mkName : Name → Name) (env : Environment) (structName : Name) (fieldName : Name) : Option Name := if let some projName := getProjFnForField? env structName fieldName then - let defFn := mkDefaultFnOfProjFn projName + let defFn := mkName projName if env.contains defFn then defFn else none else -- Check if we have a default function for a default values overridden by substructure. - let defFn := mkDefaultFnOfProjFn (structName ++ fieldName) + let defFn := mkName (structName ++ fieldName) if env.contains defFn then defFn else none +/-- +Returns the name of the auxiliary definition that defines a default value for the field, if any such definition exists. +This is *not* an inherited default. We need to store provided defaults so that it is possible to resolve defaults according to the resolution order. +-/ +def getDefaultFnForField? (env : Environment) (structName : Name) (fieldName : Name) : Option Name := + getFnForFieldUsing? mkDefaultFnOfProjFn env structName fieldName + +/-- +Returns the name of the auxiliary definition for a default value for the field, even if inherited, if any such definition exists. +-/ +def getEffectiveDefaultFnForField? (env : Environment) (structName : Name) (fieldName : Name) : Option Name := + getDefaultFnForField? env structName fieldName + <|> getFnForFieldUsing? mkInheritedDefaultFnOfProjFn env structName fieldName + partial def getPathToBaseStructureAux (env : Environment) (baseStructName : Name) (structName : Name) (path : List Name) : Option (List Name) := if baseStructName == structName then some path.reverse @@ -367,6 +403,8 @@ structure StructureResolutionOrderResult where conflicts : Array StructureResolutionOrderConflict := #[] deriving Inhabited +mutual + /-- Computes and caches the C3 linearization. Assumes parents have already been set with `setStructureParents`. If `relaxed` is false, then if the linearization cannot be computed, conflicts are recorded in the return value. @@ -377,6 +415,12 @@ partial def computeStructureResolutionOrder [Monad m] [MonadEnv m] if let some resOrder := getStructureResolutionOrder? env structName then return { resolutionOrder := resOrder } let parentNames := getStructureParentInfo env structName |>.map (·.structName) + let result ← mergeStructureResolutionOrders structName parentNames relaxed + setStructureResolutionOrder structName result.resolutionOrder + return result + +partial def mergeStructureResolutionOrders [Monad m] [MonadEnv m] + (structName : Name) (parentNames : Array Name) (relaxed : Bool) : m StructureResolutionOrderResult := do -- Don't be strict about parents: if they were supposed to be checked, they were already checked. let parentResOrders ← parentNames.mapM fun parentName => return (← computeStructureResolutionOrder parentName true).resolutionOrder @@ -405,7 +449,6 @@ partial def computeStructureResolutionOrder [Monad m] [MonadEnv m] |>.map (fun resOrder => resOrder.filter (· != name)) |>.filter (!·.isEmpty) - setStructureResolutionOrder structName resOrder return { resolutionOrder := resOrder, conflicts := defects } where selectParent (resOrders : Array (Array Name)) : m (Bool × Name) := do @@ -421,6 +464,8 @@ where -- unreachable, but correct default: return (false, resOrders[0]![0]!) +end + /-- Gets the resolution order for a structure. -/ diff --git a/tests/lean/diamond1.lean.expected.out b/tests/lean/diamond1.lean.expected.out index af1341aa19..f9c0e4d3a3 100644 --- a/tests/lean/diamond1.lean.expected.out +++ b/tests/lean/diamond1.lean.expected.out @@ -1,4 +1,4 @@ -diamond1.lean:11:40-11:45: error: parent field type mismatch, field 'a' from parent 'Baz' has type +diamond1.lean:11:40-11:45: error: field type mismatch, field 'a' from parent 'Baz' has type α → α : Type but is expected to have type α : Type diff --git a/tests/lean/mvarAtDefaultValue.lean.expected.out b/tests/lean/mvarAtDefaultValue.lean.expected.out index 69c6c1d9c4..5f7ff121e4 100644 --- a/tests/lean/mvarAtDefaultValue.lean.expected.out +++ b/tests/lean/mvarAtDefaultValue.lean.expected.out @@ -1,6 +1,6 @@ mvarAtDefaultValue.lean:5:7-5:8: error: failed to infer default value for field 'x' mvarAtDefaultValue.lean:8:7-8:8: error: don't know how to synthesize placeholder context: -toA : A -x : Nat := toA.x +x : Nat +toA : A := { x := x } ⊢ Nat diff --git a/tests/lean/run/delabStructInst.lean b/tests/lean/run/delabStructInst.lean index b14d65fa3e..92abb66950 100644 --- a/tests/lean/run/delabStructInst.lean +++ b/tests/lean/run/delabStructInst.lean @@ -158,3 +158,58 @@ structure H where /-- info: { x := 1 } : H -/ #guard_msgs in #check { x := 1 : H } + +/-! +Diamond inheritance +-/ +structure D1 where + x := 1 +structure D2 extends D1 where +structure D3 extends D1 where + x := 3 +structure D4 extends D2, D3 + +/-- info: { } : D1 -/ +#guard_msgs in #check { : D1 } +set_option pp.structureInstances.defaults true in +/-- info: { x := 1 } : D1 -/ +#guard_msgs in #check { : D1 } + +/-- info: { } : D2 -/ +#guard_msgs in #check { : D2 } +set_option pp.structureInstances.defaults true in +/-- info: { x := 1 } : D2 -/ +#guard_msgs in #check { : D2 } + +/-- info: { } : D3 -/ +#guard_msgs in #check { : D3 } +set_option pp.structureInstances.defaults true in +/-- info: { x := 3 } : D3 -/ +#guard_msgs in #check { : D3 } + +/-- info: { } : D4 -/ +#guard_msgs in #check { : D4 } +set_option pp.structureInstances.defaults true in +/-- info: { x := 3 } : D4 -/ +#guard_msgs in #check { : D4 } + +/-! +Inheritance with parameters +-/ +namespace Test1 + +structure A (α : Type) [Inhabited α] where + x : α := default +structure B (β : Type) [Inhabited β] extends A β where + +/-- info: { } : B Nat -/ +#guard_msgs in #check { : B Nat } +set_option pp.structureInstances.defaults true in +/-- info: { x := default } : B Nat -/ +#guard_msgs in #check { : B Nat } + +-- Only reducible defeq, so the `x` fields is still included: +/-- info: { x := 0 } : B Nat -/ +#guard_msgs in #check { x := 0 : B Nat } + +end Test1 diff --git a/tests/lean/run/inductive_univ.lean b/tests/lean/run/inductive_univ.lean index e7eadd343e..d46849a839 100644 --- a/tests/lean/run/inductive_univ.lean +++ b/tests/lean/run/inductive_univ.lean @@ -93,8 +93,8 @@ Errors for `structure` talk about parent projection fields too. structure A' where α : Type /-- -error: invalid universe level for field 'toA'', has type - A' +error: invalid universe level for field 'α', has type + Type at universe level 2 which is not less than or equal to the structure's resulting universe level diff --git a/tests/lean/run/structNamedParentProj.lean b/tests/lean/run/structNamedParentProj.lean index db630f05ff..5c8dcd0eb5 100644 --- a/tests/lean/run/structNamedParentProj.lean +++ b/tests/lean/run/structNamedParentProj.lean @@ -18,13 +18,21 @@ Non-atomic parent projections are not allowed. /-! Shadowing other fields is not allowed. -/ -/-- error: field 'x' has already been declared -/ -#guard_msgs in structure S' extends x : S +/-- +error: field 'x' has already been declared + +The 'toParent : P' syntax can be used to adjust the name for the parent projection +-/ +#guard_msgs in structure S' extends x : S /-! Duplicate parent projections -/ -/-- error: field 'toP' has already been declared -/ +/-- +error: field 'toP' has already been declared + +The 'toParent : P' syntax can be used to adjust the name for the parent projection +-/ #guard_msgs in structure S' extends toP : S, toP : T /-! @@ -33,16 +41,26 @@ Duplicate parent projections because from different namespaces structure NS1.S structure NS2.S /-- -error: field 'toS' has already been declared, use 'toParent : P' syntax to give a unique name for the parent projection +error: field 'toS' has already been declared + +The 'toParent : P' syntax can be used to adjust the name for the parent projection -/ #guard_msgs in structure S' extends NS1.S, NS2.S /-! Duplicate parent projections, when there are overlapping fields -/ -/-- error: field 'toS' has already been declared -/ +/-- +error: field 'toS' has already been declared + +The 'toParent : P' syntax can be used to adjust the name for the parent projection +-/ #guard_msgs in structure S' extends S, toS : U -/-- error: field 'toP' has already been declared -/ +/-- +error: field 'toP' has already been declared + +The 'toParent : P' syntax can be used to adjust the name for the parent projection +-/ #guard_msgs in structure S' extends toP : S, toP : T /-! @@ -51,7 +69,9 @@ Duplicate parent projections because from different namespaces, when there are d structure NS1.S' where x : Nat structure NS2.S' where x : Nat /-- -error: field 'toS'' has already been declared, use 'toParent : P' syntax to give a unique name for the parent projection +error: field 'toS'' has already been declared + +The 'toParent : P' syntax can be used to adjust the name for the parent projection -/ #guard_msgs in structure S' extends NS1.S', NS2.S' diff --git a/tests/lean/run/structureElab.lean b/tests/lean/run/structureElab.lean new file mode 100644 index 0000000000..5b35d3f4b9 --- /dev/null +++ b/tests/lean/run/structureElab.lean @@ -0,0 +1,340 @@ +/-! +# Tests of the structure elaborator +-/ + +-- We want to see the exact constructors in tests. +set_option pp.structureInstances false +set_option pp.proofs true + + +/-! +Diamond, look at the constructors and flat constructors +-/ +namespace Test1 + +structure S1 (α : Type) where + x : α + y : Nat + +structure S2 (α : Type) extends S1 α where + z : Nat + +structure S3 (α : Type) extends S1 α where + w : Nat + +structure S4 (α : Type) extends S2 α, S3 α where + x' : α + +/-- info: Test1.S1.mk {α : Type} (x : α) (y : Nat) : S1 α -/ +#guard_msgs in #check S1.mk +/-- info: Test1.S2.mk {α : Type} (toS1 : S1 α) (z : Nat) : S2 α -/ +#guard_msgs in #check S2.mk +/-- info: Test1.S3.mk {α : Type} (toS1 : S1 α) (w : Nat) : S3 α -/ +#guard_msgs in #check S3.mk +/-- info: Test1.S4.mk {α : Type} (toS2 : S2 α) (w : Nat) (x' : α) : S4 α -/ +#guard_msgs in #check S4.mk +/-- +info: def Test1.S1._flat_ctor : {α : Type} → α → Nat → S1 α := +fun α x y => S1.mk x y +-/ +#guard_msgs in #print S1._flat_ctor +/-- +info: def Test1.S2._flat_ctor : {α : Type} → α → Nat → Nat → S2 α := +fun α x y z => S2.mk (S1.mk x y) z +-/ +#guard_msgs in #print S2._flat_ctor +/-- +info: def Test1.S3._flat_ctor : {α : Type} → α → Nat → Nat → S3 α := +fun α x y w => S3.mk (S1.mk x y) w +-/ +#guard_msgs in #print S3._flat_ctor +/-- +info: def Test1.S4._flat_ctor : {α : Type} → α → Nat → Nat → Nat → α → S4 α := +fun α x y z w x' => S4.mk (S2.mk (S1.mk x y) z) w x' +-/ +#guard_msgs in #print S4._flat_ctor +/-- info: Test1.S4._flat_ctor {α : Type} (x : α) (y z w : Nat) (x' : α) : S4 α -/ +#guard_msgs in #check S4._flat_ctor + +end Test1 + +/-! +Verify existence of default value definitions +-/ +namespace TestD1 + +structure D1 where + x := 1 +structure D2 extends D1 where +structure D3 extends D1 where + x := 3 +structure D4 extends D2, D3 + +/-- +info: @[reducible] def TestD1.D1.x._default : Nat := +id 1 +-/ +#guard_msgs in #print D1.x._default +/-- error: unknown constant 'D2.x._default' -/ +#guard_msgs in #print D2.x._default +/-- +info: @[reducible] def TestD1.D2.x._inherited_default : Nat := +id 1 +-/ +#guard_msgs in #print D2.x._inherited_default +/-- +info: @[reducible] def TestD1.D3.x._default : Nat := +id 3 +-/ +#guard_msgs in #print D3.x._default +/-- error: unknown constant 'D4.x._default' -/ +#guard_msgs in #print D4.x._default +/-- +info: @[reducible] def TestD1.D4.x._inherited_default : Nat := +id 3 +-/ +#guard_msgs in #print D4.x._inherited_default + +end TestD1 + +/-! +Verify default value definitions can support parameters +-/ +namespace TestD2 + +structure D1 (α : Type) [Inhabited α] where + x : α := default +structure D2 (α : Type) [Inhabited α] extends D1 α where +structure D3 extends D1 Nat where + +/-- +info: @[reducible] def TestD2.D1.x._default : {α : Type} → {inst : Inhabited α} → α := +fun {α} {inst} => id default +-/ +#guard_msgs in #print D1.x._default +/-- error: unknown constant 'D2.x._default' -/ +#guard_msgs in #print D2.x._default +/-- +info: @[reducible] def TestD2.D2.x._inherited_default : {α : Type} → {inst : Inhabited α} → α := +fun {α} {inst} => id default +-/ +#guard_msgs in #print D2.x._inherited_default +/-- error: unknown constant 'D3.x._default' -/ +#guard_msgs in #print D3.x._default +/-- +info: @[reducible] def TestD2.D3.x._inherited_default : Nat := +id default +-/ +#guard_msgs in #print D3.x._inherited_default + +end TestD2 + +/-! +Make sure class parents can be used in successive parents +-/ +namespace Test2_1 + +local infixl:70 (priority := high) " * " => Mul.mul + +class AssociativeMul (α : Type _) [Mul α] : Prop where + mul_assoc (x y z : α) : x * y * z = x * (y * z) + +class Semigroup (α : Type _) extends Mul α, AssociativeMul α where + +/-- +info: Test2_1.Semigroup.mk.{u_1} {α : Type u_1} [toMul : Mul α] [toAssociativeMul : AssociativeMul α] : Semigroup α +-/ +#guard_msgs in #check Semigroup.mk +/-- +info: def Test2_1.Semigroup._flat_ctor.{u_1} : {α : Type u_1} → + (mul : α → α → α) → (∀ (x y z : α), @Eq α (mul (mul x y) z) (mul x (mul y z))) → Semigroup α := +fun α mul mul_assoc => @Semigroup.mk α (@Mul.mk α mul) (@AssociativeMul.mk α (@Mul.mk α mul) mul_assoc) +-/ +#guard_msgs in set_option pp.explicit true in #print Semigroup._flat_ctor +/-- +info: Test2_1.Semigroup._flat_ctor.{u_1} {α : Type u_1} (mul : α → α → α) + (mul_assoc : ∀ (x y z : α), @Eq α (mul (mul x y) z) (mul x (mul y z))) : Semigroup α +-/ +#guard_msgs in set_option pp.explicit true in #check Semigroup._flat_ctor + +end Test2_1 + +/-! +Make sure instances can come from parents with overlapping fields +-/ +namespace Test2_2 + +structure Add2 (α : Type _) where + add : α → α → α + +class Add3 (α : Type _) extends Add2 α, Add α where + h (x : α) : x + x = x + +/-- +info: Test2_2.Add3._flat_ctor.{u_1} {α : Type u_1} (add : α → α → α) + (h : ∀ (x : α), @Eq α (@HAdd.hAdd α α α (@instHAdd α (@Add.mk α add)) x x) x) : Add3 α +-/ +#guard_msgs in set_option pp.explicit true in #check Add3._flat_ctor + +end Test2_2 + +/-! +Example that used to be in a comment at `getFieldDefaultValue?`. +The issue was that the default value function was in terms of subobject fields, +so there could be a cyclic dependency. +With a field-centric view in #7302, this is no longer an issue to consider. +-/ +namespace Test3 + +structure A where + a : Nat + +structure B where + a : Nat + b : Nat + c : Nat + +structure C extends B where + d : Nat + c := b + d + +structure D extends A, C + +/-- +info: @[reducible] def Test3.D.c._inherited_default : Nat → Nat → Nat := +fun b d => @id Nat (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) b d) +-/ +#guard_msgs in set_option pp.explicit true in #print D.c._inherited_default + +end Test3 + +/-! +Make sure we can fill in `toMagma` at the use of `mul`. +It used to be (before #7302) that `mul` would see that the type of `a`, `b`, and `c` were `toMagma.α`, +which would cause unification to fill in the `M` argument. +However, now the types of these variables are just `α`, with no connection to `toMagma`. +We use the heuristic that parent structures should effectively be singleton types while elaborating fields, +and so the `?M : Magma` metavariable should be assigned with `toMagma`. +-/ + +namespace Test4 + +structure Magma where + α : Type u + mul : α → α → α + +instance : CoeSort Magma (Type u) where + coe s := s.α + +abbrev mul {M : Magma} (a b : M) : M := + M.mul a b + +local infixl:70 (priority := high) " * " => mul + +structure Semigroup extends Magma where + mul_assoc (a b c : α) : a * b * c = a * (b * c) + +/-- +info: Test4.Semigroup.mk.{u_1} (toMagma : Magma) + (mul_assoc : + ∀ (a b c : toMagma.α), @Eq toMagma.α (@mul toMagma (@mul toMagma a b) c) (@mul toMagma a (@mul toMagma b c))) : + Semigroup +-/ +#guard_msgs in set_option pp.explicit true in #check Semigroup.mk + +/-- +info: def Test4.Semigroup._flat_ctor.{u_1} : (α : Type u_1) → + (mul : α → α → α) → + (∀ (a b c : α), + @Eq α (@Test4.mul (Magma.mk α mul) (@Test4.mul (Magma.mk α mul) a b) c) + (@Test4.mul (Magma.mk α mul) a (@Test4.mul (Magma.mk α mul) b c))) → + Semigroup := +fun α mul mul_assoc => Semigroup.mk (Magma.mk α mul) mul_assoc +-/ +#guard_msgs in set_option pp.explicit true in #print Semigroup._flat_ctor + +end Test4 + +/-! +Default value involving parent instance +-/ +namespace Test5 + +structure C (α : Type) extends Mul α where + (x y : α) + z := x * y + +/-- +info: @[reducible] def Test5.C.z._default : {α : Type} → (α → α → α) → α → α → α := +fun {α} mul x y => @id α (@HMul.hMul α α α (@instHMul α (@Mul.mk α mul)) x y) +-/ +#guard_msgs in set_option pp.explicit true in #print C.z._default + +end Test5 + +/-! +Test from a docstring in Elab/StructInst, to check computed defaults. +-/ +namespace Test6 + +structure A where + x : Nat := 1 + +structure B extends A where + y : Nat := x + 1 + x := y + 1 + +structure C extends B where + z : Nat := 2*y + x := z + 3 + +/-- +info: @[reducible] def Test6.A.x._default : Nat := +id 1 +-/ +#guard_msgs in #print A.x._default +/-- +info: @[reducible] def Test6.B.y._default : Nat → Nat := +fun x => id (x + 1) +-/ +#guard_msgs in #print B.y._default +/-- +info: @[reducible] def Test6.B.x._default : Nat → Nat := +fun y => id (y + 1) +-/ +#guard_msgs in #print B.x._default +/-- +info: @[reducible] def Test6.C.x._default : Nat → Nat := +fun z => id (z + 3) +-/ +#guard_msgs in #print C.x._default +/-- +info: @[reducible] def Test6.C.y._inherited_default : Nat → Nat := +fun x => id (x + 1) +-/ +#guard_msgs in #print C.y._inherited_default +/-- +info: @[reducible] def Test6.C.z._default : Nat → Nat := +fun y => id (2 * y) +-/ +#guard_msgs in #print C.z._default + +end Test6 + +/-! +Dependent types to an inherited field +-/ +namespace Test7 + +structure A1 where + n : Nat +structure A2 extends A1 where + h : n > 0 + +/-- +info: def Test7.A2._flat_ctor : (n : Nat) → n > 0 → A2 := +fun n h => A2.mk (A1.mk n) h +-/ +#guard_msgs in #print A2._flat_ctor + +end Test7 diff --git a/tests/lean/struct1.lean.expected.out b/tests/lean/struct1.lean.expected.out index 1db6684d68..c1d81bedd4 100644 --- a/tests/lean/struct1.lean.expected.out +++ b/tests/lean/struct1.lean.expected.out @@ -7,7 +7,7 @@ The purpose of the change is to accommodate 'structure S extends toP : P' syntax struct1.lean:15:28-15:33: warning: field 'x' from 'B' has already been declared struct1.lean:16:1-16:2: error: field 'x' has been declared in parent structure struct1.lean:17:30-17:35: warning: duplicate parent structure 'A', skipping -struct1.lean:19:27-19:33: error: parent field type mismatch, field 'x' from parent 'B' has type +struct1.lean:19:27-19:33: error: field type mismatch, field 'x' from parent 'B' has type Bool : Type but is expected to have type Nat : Type