refactor: factor out common code for structure default values (#7737)

This PR factors out a `Lean.Meta.instantiateStructDefaultValueFn?` function for instantiating default values for fields.
2025-03-31 15:40:39 -07:00 · 2025-03-31 15:40:39 -07:00 · d6303a8e7f
commit d6303a8e7f
parent 1d47360099
7 changed files with 85 additions and 145 deletions
--- a/src/Init/Internal/Order/Basic.lean
+++ b/src/Init/Internal/Order/Basic.lean
@ -488,7 +488,6 @@ instance instCCPOPProd [CCPO α] [CCPO β] : CCPO (α ×' β) where
  csup c := ⟨CCPO.csup (PProd.chain.fst c), CCPO.csup (PProd.chain.snd c)⟩
  csup_spec := by
    intro ⟨a, b⟩ c hchain
-    try dsimp -- TODO(kmill) remove
    constructor
    next =>
      intro ⟨h₁, h₂⟩ ⟨a', b'⟩ cab
--- a/src/Lean/Elab/Print.lean
+++ b/src/Lean/Elab/Print.lean
@ -86,8 +86,9 @@ private partial def printStructure (id : Name) (levelParams : List Name) (numPar
  let env ← getEnv
  let kind := if isClass env id then "class" else "structure"
  let header ← mkHeader' kind id levelParams type isUnsafe (sig := false)
+  let levels := levelParams.map Level.param
  liftTermElabM <| forallTelescope (← getConstInfo id).type fun params _ =>
-    let s := Expr.const id (levelParams.map .param)
+    let s := Expr.const id levels
    withLocalDeclD `self (mkAppN s params) fun self => do
      let mut m : MessageData := header
      -- Signature
@ -100,15 +101,12 @@ private partial def printStructure (id : Name) (levelParams : List Name) (numPar
      unless parents.isEmpty do
        m := m ++ Format.line ++ "parents:"
        for parent in parents do
-          let ptype ← inferType (mkApp (mkAppN (.const parent.projFn (levelParams.map .param)) params) self)
+          let ptype ← inferType (mkApp (mkAppN (.const parent.projFn levels) params) self)
          m := m ++ indentD m!"{.ofConstName parent.projFn (fullNames := true)} : {ptype}"
      -- Fields
-      -- Collect params in a map for default value processing
-      let paramMap : NameMap Expr ← params.foldlM (init := {}) fun paramMap param => do
-        pure <| paramMap.insert (← param.fvarId!.getUserName) param
      -- Collect autoParam tactics, which are all on the flat constructor:
      let flatCtorName := mkFlatCtorOfStructCtorName ctor
-      let flatCtorInfo ← try getConstInfo flatCtorName catch _ => getConstInfo (id ++ `_flat_ctor) -- TODO(kmill): remove catch
+      let flatCtorInfo ← getConstInfo flatCtorName
      let autoParams : NameMap Syntax ← forallTelescope flatCtorInfo.type fun args _ =>
        args[numParams:].foldlM (init := {}) fun set arg => do
          let decl ← arg.fvarId!.getDecl
@ -136,9 +134,7 @@ private partial def printStructure (id : Name) (levelParams : List Name) (numPar
              let stx : TSyntax ``Parser.Tactic.tacticSeq := ⟨stx⟩
              pure m!" := by{indentD stx}"
            else if let some defFn := getEffectiveDefaultFnForField? env id field then
-              let cinfo ← getConstInfo defFn
-              let defValue ← instantiateValueLevelParams cinfo (levelParams.map .param)
-              if let some val ← processDefaultValue paramMap fieldMap defValue then
+              if let some (_, val) ← instantiateStructDefaultValueFn? defFn levels params (pure ∘ fieldMap.find?) then
                pure m!" :={indentExpr val}"
              else
                pure m!" := <error>"
@ -157,24 +153,6 @@ private partial def printStructure (id : Name) (levelParams : List Name) (numPar
      -- Omit proofs; the delaborator enables `pp.proofs` for non-constant proofs, but we don't want this for default values
      withOptions (fun opts => opts.set pp.proofs.name false) do
        logInfo m
-where
-  processDefaultValue (paramMap : NameMap Expr) (fieldValues : NameMap Expr) : Expr → MetaM (Option Expr)
-  | .lam n d b c => do
-    if c.isExplicit then
-      let some val := fieldValues.find? n | return none
-      if ← isDefEq (← inferType val) d then
-        processDefaultValue paramMap fieldValues (b.instantiate1 val)
-      else
-        return none
-    else
-      let some param := paramMap.find? n | return none
-      if ← isDefEq (← inferType param) d then
-        processDefaultValue paramMap fieldValues (b.instantiate1 param)
-      else
-        return none
-  | e =>
-    let_expr id _ a := e | return some e
-    return some a

 private def printIdCore (id : Name) : CommandElabM Unit := do
  let env ← getEnv
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@ -399,7 +399,7 @@ The `structureType?` is the expected type of the structure instance.
 -/
 private def mkCtorHeader (ctorVal : ConstructorVal) (structureType? : Option Expr) : TermElabM CtorHeaderResult := do
  let flatCtorName := mkFlatCtorOfStructCtorName ctorVal.name
-  let cinfo ← try getConstInfo flatCtorName catch _ => getConstInfo (ctorVal.induct ++ `_flat_ctor) -- TODO(kmill): remove catch
+  let cinfo ← getConstInfo flatCtorName
  let us ← mkFreshLevelMVars ctorVal.levelParams.length
  let mut type ← instantiateTypeLevelParams cinfo.toConstantVal us
  let mut params : Array Expr := #[]
@ -726,36 +726,13 @@ 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? (fieldName : Name) : StructInstM (NameSet × Option Expr) := do
-  match getEffectiveDefaultFnForField? (← getEnv) (← read).structName fieldName with
-  | none => return ({}, none)
-  | some defaultFn =>
-    trace[Elab.struct] "default fn for '{fieldName}' is '{.ofConstName defaultFn}'"
-    let cinfo ← getConstInfo defaultFn
-    let us := (← read).levels
-    go? {} <| (← instantiateValueLevelParams cinfo us).beta (← read).params
-where
-  logFailure : StructInstM (NameSet × Option Expr) := do
-    logError m!"default value for field '{fieldName}' of structure '{.ofConstName (← read).structName}' could not be instantiated, ignoring"
-    return ({}, none)
-  go? (usedFields : NameSet) (e : Expr) : StructInstM (NameSet × Option Expr) := do
-    match e with
-    | Expr.lam n d b c =>
-      if c.isExplicit then
-        let some val := (← get).fieldMap.find? n
-          | trace[Elab.struct] "default value error: no value for field '{n}'"
-            logFailure
-        let valType ← inferType val
-        if (← isDefEq valType d) then
-          go? (usedFields.insert n) (b.instantiate1 val)
-        else
-          trace[Elab.struct] "default value error: {← mkHasTypeButIsExpectedMsg valType d}"
-          logFailure
-      else
-        trace[Elab.struct] "default value error: unexpected implicit argument{indentExpr e}"
-        logFailure
-    | e =>
-      let_expr id _ a := e | return (usedFields, some e)
-      return (usedFields, some a)
+  let some defFn := getEffectiveDefaultFnForField? (← getEnv) (← read).structName fieldName
+    | return ({}, none)
+  let fieldMap := (← get).fieldMap
+  let some (fields, val) ← instantiateStructDefaultValueFn? defFn (← read).levels (← read).params (pure ∘ fieldMap.find?)
+    | logError m!"default value for field '{fieldName}' of structure '{.ofConstName (← read).structName}' could not be instantiated, ignoring"
+      return ({}, none)
+  return (fields, val)

 /--
 Auxiliary type for `synthDefaultFields`
@ -935,7 +912,7 @@ where
    let ctor := getStructureCtor (← getEnv) parentName
    unless params.size == ctor.numParams do return .done e
    let flatCtorName := mkFlatCtorOfStructCtorName ctor.name
-    let cinfo ← try getConstInfo flatCtorName catch _ => getConstInfo (ctor.induct ++ `_flat_ctor) -- TODO(kmill): remove catch
+    let cinfo ← getConstInfo flatCtorName
    let ctorVal ← instantiateValueLevelParams cinfo us
    let fieldArgs := parentFields.map fieldMap.find!
    let e' := (ctorVal.beta params).beta fieldArgs
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@ -529,46 +529,25 @@ private def fieldFromMsg (info : StructFieldInfo) : MessageData :=
    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`.
+Instantiates default value for field `fieldName` set at structure `structName`, using the field fvars in the `StructFieldInfo`s.
 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.
+as an `_inherited_default` auxiliary function is normalized;
+we don't do those normalizations here, since that could be wasted effort if this default isn't chosen.
 -/
-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
+private partial def getFieldDefaultValue? (structName : Name) (params : Array Expr) (fieldName : Name) : StructElabM (Option Expr) := do
+  let some defFn := getDefaultFnForField? (← getEnv) structName fieldName
+    | return none
+  let fieldVal? (n : Name) : StructElabM (Option Expr) := do
+    let some info ← findFieldInfo? n | return none
+    return info.fvar
+  let some (_, val) ← instantiateStructDefaultValueFn? defFn none params fieldVal?
+    | logWarning m!"default value for field '{fieldName}' of structure '{.ofConstName structName}' could not be instantiated, ignoring"
+      return none
+  return val

-  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) :
+private def getFieldDefault? (structName : Name) (params : Array Expr) (fieldName : Name) :
    StructElabM (Option StructFieldDefault) := do
-  if let some val ← getFieldDefaultValue? structName (paramMap : NameMap Expr) fieldName then
+  if let some val ← getFieldDefaultValue? structName params 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
@ -593,7 +572,7 @@ Adds `fieldName` of type `fieldType` from structure `structName`.
 See `withStructFields` for meanings of other arguments.
 -/
 private partial def withStructField (view : StructView) (sourceStructNames : List Name) (inSubobject? : Option Expr)
-    (structName : Name) (paramMap : NameMap Expr) (fieldName : Name) (fieldType : Expr)
+    (structName : Name) (params : Array Expr) (fieldName : Name) (fieldType : Expr)
    (k : Expr → StructElabM α) : StructElabM α := do
  trace[Elab.structure] "withStructField '{.ofConstName structName}', field '{fieldName}'"
  let fieldType ← instantiateMVars fieldType
@ -612,7 +591,7 @@ private partial def withStructField (view : StructView) (sourceStructNames : Lis
    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 then
+    if let some d ← getFieldDefault? structName params fieldName then
      addFieldInheritedDefault fieldName structName d
    k existingField.fvar
  else
@ -639,7 +618,7 @@ private partial def withStructField (view : StructView) (sourceStructNames : Lis
        binfo := fieldInfo.binderInfo
        projFn? := fieldInfo.projFn
      }
-      if let some d ← getFieldDefault? structName paramMap fieldName then
+      if let some d ← getFieldDefault? structName params fieldName then
        addFieldInheritedDefault fieldName structName d
      k fieldFVar

@ -652,7 +631,7 @@ Does not add a parent field for the structure itself; that is done by `withStruc
 - 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)
+    (structType : Expr) (inSubobject? : Option Expr)
    (k : Expr → StructElabM α) : StructElabM α := do
  let structName ← getStructureName structType
  let .const _ us := structType.getAppFn | unreachable!
@ -688,7 +667,7 @@ private partial def withStructFields (view : StructView) (sourceStructNames : Li
      let fieldName := fields[i]
      let fieldMVar := fieldMVars[i]!
      let fieldType ← inferType fieldMVar
-      withStructField view sourceStructNames inSubobject? structName paramMap fieldName fieldType fun fieldFVar => do
+      withStructField view sourceStructNames inSubobject? structName params fieldName fieldType fun fieldFVar => do
        fieldMVar.mvarId!.assign fieldFVar
        goFields (i + 1)
    else
@ -739,14 +718,7 @@ private partial def withStruct (view : StructView) (sourceStructNames : List Nam

    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
+      withStructFields view sourceStructNames structType inSubobject? 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"
@ -755,7 +727,7 @@ private partial def withStruct (view : StructView) (sourceStructNames : List Nam
        -- which for inherited fields might not have been seen yet.
        -- Note: duplication is ok for now. We use a stable sort later.
        for fieldName in allFields do
-          if let some d ← getFieldDefault? structName paramMap fieldName then
+          if let some d ← getFieldDefault? structName params fieldName then
            addFieldInheritedDefault fieldName structName d
        withLetDecl rawStructFieldName structType structVal fun structFVar => do
          let info : StructFieldInfo := {
@ -1227,8 +1199,8 @@ private def registerStructure (structName : Name) (infos : Array StructFieldInfo
        fieldName  := info.name
        projFn     := info.declName
        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
+        autoParam? := none -- deprecated field
      }
    else
      return none
--- a/src/Lean/Meta/Structure.lean
+++ b/src/Lean/Meta/Structure.lean
@ -181,4 +181,42 @@ def etaStructReduce (e : Expr) (p : Name → Bool) : MetaM Expr := do
    else
      return .continue)

+/--
+Instantiates the default value given by the default value function `defaultFn`.
+- `defaultFn` is the default value function returned by `Lean.getEffectiveDefaultFnForField?` or `Lean.getDefaultFnForField?`.
+- `levels?` is the list of levels to use, and otherwise the levels are inferred.
+- `params` is the list of structure parameters. These are assumed to be correct for the given levels.
+- `fieldVal?` is a function for getting fields for values, if they exist.
+
+If successful, returns a set of fields used and the resulting default value.
+Success is expected. Callers should do metacontext backtracking themselves if needed.
+-/
+partial def instantiateStructDefaultValueFn?
+    [Monad m] [MonadEnv m] [MonadError m] [MonadLiftT MetaM m] [MonadControlT MetaM m]
+    (defaultFn : Name) (levels? : Option (List Level)) (params : Array Expr)
+    (fieldVal? : Name → m (Option Expr)) : m (Option (NameSet × Expr)) := do
+  let cinfo ← getConstInfo defaultFn
+  let us ← levels?.getDM (mkFreshLevelMVarsFor cinfo)
+  assert! us.length == cinfo.levelParams.length
+  let mut val ← liftMetaM <| instantiateValueLevelParams cinfo us
+  for param in params do
+    let .lam _ t b _ := val | return none
+    -- If no levels given, need to unify to solve for level mvars.
+    if levels?.isNone then
+      unless (← isDefEq (← inferType param) t) do return none
+    val := b.instantiate1 param
+  go? {} val
+where
+  go? (usedFields : NameSet) (e : Expr) : m (Option (NameSet × Expr)) := do
+    match e with
+    | .lam n d b _ =>
+      let some val ← fieldVal? n | return none
+      if (← isDefEq (← inferType val) d) then
+        go? (usedFields.insert n) (b.instantiate1 val)
+      else
+        return none
+    | e =>
+      let_expr id _ a := e | return some (usedFields, e)
+      return some (usedFields, a)
+
 end Lean.Meta
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@ -9,6 +9,7 @@ import Lean.PrettyPrinter.Delaborator.Basic
 import Lean.PrettyPrinter.Delaborator.SubExpr
 import Lean.PrettyPrinter.Delaborator.TopDownAnalyze
 import Lean.Meta.CoeAttr
+import Lean.Meta.Structure

 namespace Lean.PrettyPrinter.Delaborator
 open Lean.Meta
@ -556,8 +557,7 @@ def delabDelayedAssignedMVar : Delab := whenNotPPOption getPPMVarsDelayed do
    delabMVarAux decl.mvarIdPending

 private partial def collectStructFields
-    (structName : Name)
-    (paramMap : NameMap Expr)
+    (structName : Name) (levels : List Level) (params : Array Expr)
    (fields : Array (TSyntax ``Parser.Term.structInstField))
    (fieldValues : NameMap Expr)
    (s : ConstructorVal) :
@ -575,14 +575,13 @@ private partial def collectStructFields
        if ← getPPOption getPPStructureInstancesFlatten then
          if let some s' ← isConstructorApp? (← getExpr) then
            if s'.induct == parentName then
-              let (fieldValues, fields) ← collectStructFields structName paramMap fields fieldValues s'
+              let (fieldValues, fields) ← collectStructFields structName levels params fields fieldValues s'
              return (i + 1, fieldValues, fields)
-      /- Does it have the default value, and should it be omitted? -/
+      /- Does this field have a default value? and if so, can we omit the field? -/
      unless ← getPPOption getPPStructureInstancesDefaults do
        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
+          -- Use `withNewMCtxDepth` to prevent delaborator from solving metavariables.
+          if let some (_, defValue) ← withNewMCtxDepth <| instantiateStructDefaultValueFn? defFn levels params (pure ∘ fieldValues.find?) then
            if ← withReducible <| withNewMCtxDepth <| isDefEq defValue (← getExpr) then
              -- Default value matches, skip the field.
              return (i + 1, fieldValues, fields)
@ -596,24 +595,6 @@ private partial def collectStructFields
      let field ← `(structInstField|$fieldId:ident := $value)
      return (i + 1, fieldValues, fields.push field))
  return (fieldValues, fields)
-where
-  processDefaultValue (paramMap : NameMap Expr) (fieldValues : NameMap Expr) : Expr → MetaM (Option Expr)
-  | .lam n d b c => do
-    if c.isExplicit then
-      let some val := fieldValues.find? n | return none
-      if ← isDefEq (← inferType val) d then
-        processDefaultValue paramMap fieldValues (b.instantiate1 val)
-      else
-        return none
-    else
-      let some param := paramMap.find? n | return none
-      if ← isDefEq (← inferType param) d then
-        processDefaultValue paramMap fieldValues (b.instantiate1 param)
-      else
-        return none
-  | e =>
-    let_expr id _ a := e | return some e
-    return some a

 /--
 Delaborate structure constructor applications using structure instance notation or anonymous constructor notation.
@ -663,14 +644,10 @@ 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.
    -/
-    -- For default value handling, we need to create a map of type parameter names to expressions.
+    let .const _ levels := (← getExpr).getAppFn | failure
    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
+    let params := args[0:s.numParams]
+    let (_, fields) ← collectStructFields s.induct levels params #[] {} s
    let tyStx? : Option Term ← withType do
      if ← getPPOption getPPStructureInstanceType then delab else pure none
    `({ $fields,* $[: $tyStx?]? })
--- a/src/Lean/Structure.lean
+++ b/src/Lean/Structure.lean
@ -27,8 +27,7 @@ structure StructureFieldInfo where
  subobject? : Option Name
  /-- The binder info for the field from the `structure` definition. -/
  binderInfo : BinderInfo
-  /-- If set, the field is an autoparam (a field declared using `fld := by ...` syntax).
-  The expression evaluates to a tactic `Syntax` object. Generally this is an `Expr.const` expression. -/
+  /-- Deprecated. -/
  autoParam? : Option Expr := none
  deriving Inhabited, Repr