From 295cae8afda0aaab381ce2f60a4e73da04454945 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 10 Aug 2021 16:50:52 -0700 Subject: [PATCH] feat: copy field default values Only basic examples are working. We still have many TODOs --- src/Lean/Elab/Structure.lean | 60 +++++++++++++++++++++++++++--------- tests/lean/run/diamond3.lean | 19 ++++++++++++ 2 files changed, 65 insertions(+), 14 deletions(-) create mode 100644 tests/lean/run/diamond3.lean diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index ecb4c5480f..215960a8e3 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -326,13 +326,45 @@ private def toVisibility (fieldInfo : StructureFieldInfo) : CoreM Visibility := else return Visibility.regular -private partial def copyNewFieldsFrom (structDeclName : Name) (infos : Array StructFieldInfo) (parentType : Expr) (k : Array StructFieldInfo → TermElabM α) : TermElabM α := do - copyFields infos parentType k +abbrev FieldMap := NameMap Expr -- Map from field name to expression representing the field + +private partial def copyDefaultValue? (fieldMap : FieldMap) (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? (cinfo.instantiateValueLevelParams us) where - copyFields (infos : Array StructFieldInfo) (parentType : Expr) (k : Array StructFieldInfo → TermElabM α) : TermElabM α := do + go? (e : Expr) : TermElabM (Option Expr) := do + match e with + | Expr.lam n d b c => + if c.binderInfo.isExplicit then + let fieldName := n + match fieldMap.find? n with + | none => return none -- TODO Generate warning? + | some val => + let valType ← inferType val + if (← isDefEq valType d) then + go? (b.instantiate1 val) + else + return none -- TODO Generate warning? + else + let arg ← mkFreshExprMVar d + go? (b.instantiate1 arg) + | e => + if e.isAppOfArity ``id 2 then + return some (← instantiateMVars e.appArg!) + else + return some (← instantiateMVars e) + +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) (parentType : Expr) (k : FieldMap → Array StructFieldInfo → TermElabM α) : TermElabM α := do let parentStructName ← getStructureName parentType let fieldNames := getStructureFields (← getEnv) parentStructName - let rec copy (i : Nat) (infos : Array StructFieldInfo) : TermElabM α := do + let rec copy (i : Nat) (fieldMap : FieldMap) (infos : Array StructFieldInfo) : TermElabM α := do if h : i < fieldNames.size then let fieldName := fieldNames.get ⟨i, h⟩ let fieldType ← getFieldType infos parentStructName parentType fieldName @@ -342,31 +374,31 @@ where unless (← isDefEq fieldType existingFieldType) do throwError "parent field type mismatch, field '{fieldName}' from parent '{parentStructName}' {← mkHasTypeButIsExpectedMsg fieldType existingFieldType}" -- TODO: if new field has a default value, it should probably override the default at `infos` (if it has one) - copy (i+1) infos + copy (i+1) (fieldMap.insert fieldName existingFieldInfo.fvar) infos | none => let some fieldInfo ← getFieldInfo? (← getEnv) parentStructName fieldName | unreachable! let addNewField : TermElabM α := do - /- TODO: we are ignoring the following information from the `fieldName` declaraion at `parentStructName`. - - Default value. - -/ + let value? ← copyDefaultValue? fieldMap parentStructName fieldName withLocalDecl fieldName fieldInfo.binderInfo fieldType fun fieldFVar => do - -- trace[Meta.debug] "copying field {fieldName} : {← inferType fieldFVar}" let fieldDeclName := structDeclName ++ fieldName let fieldDeclName ← applyVisibility (← toVisibility fieldInfo) fieldDeclName - let infos := infos.push { name := fieldName, declName := fieldDeclName, fvar := fieldFVar, value? := none, + let infos := infos.push { name := fieldName, declName := fieldDeclName, fvar := fieldFVar, value?, kind := StructFieldKind.newField, inferMod := fieldInfo.inferMod } - copy (i+1) infos + copy (i+1) (fieldMap.insert fieldName fieldFVar) infos if fieldInfo.subobject?.isSome then let fieldParentStructName ← getStructureName fieldType if (← findExistingField? infos fieldParentStructName).isSome then - copyFields infos fieldType (fun infos => copy (i+1) infos) + copyFields infos fieldType fun nestedFieldMap infos => do + -- TODO: update fieldMap + copy (i+1) fieldMap infos else addNewField else addNewField else - k infos - copy 0 infos + -- TODO: Check if `parentStructName` has overriden default values of nested structures + k fieldMap infos + copy 0 {} infos private def mkToParentName (parentStructName : Name) : Name := Name.mkSimple $ "to" ++ parentStructName.eraseMacroScopes.getString! -- erase macro scopes? diff --git a/tests/lean/run/diamond3.lean b/tests/lean/run/diamond3.lean new file mode 100644 index 0000000000..cebddcd1bf --- /dev/null +++ b/tests/lean/run/diamond3.lean @@ -0,0 +1,19 @@ +structure A where + a : Nat + +structure B where + a : Nat + b : Nat + c : Nat := a + b + +structure C extends B where + d : Nat := 0 + e : Nat := 0 + +structure D extends A, C + +def f (a b : Nat) : D := + { a, b } + +theorem ex (a b : Nat) : (f a b |>.c) = a + b := + rfl