From fdce7a99e13f938d1b56ba13da5e2dd78bd4bf34 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 9 Aug 2021 10:26:14 -0700 Subject: [PATCH] feat: structure diamonds basic support See TODO in the new comments. --- src/Lean/Elab/Structure.lean | 104 +++++++++++++++++++------- tests/lean/diamond1.lean | 27 +++++++ tests/lean/diamond1.lean.expected.out | 10 +++ tests/lean/struct1.lean | 4 +- tests/lean/struct1.lean.expected.out | 12 ++- 5 files changed, 124 insertions(+), 33 deletions(-) create mode 100644 tests/lean/diamond1.lean create mode 100644 tests/lean/diamond1.lean.expected.out diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index dbef2064da..eb245754a6 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -7,6 +7,7 @@ import Lean.Parser.Command import Lean.Meta.Closure import Lean.Meta.SizeOf import Lean.Meta.Injective +import Lean.Meta.Structure import Lean.Elab.Command import Lean.Elab.DeclModifiers import Lean.Elab.DeclUtil @@ -227,23 +228,30 @@ private def validStructType (type : Expr) : Bool := | Expr.sort .. => true | _ => false -private def checkParentIsStructure (parent : Expr) : TermElabM Name := - match parent.getAppFn with - | Expr.const c _ _ => do - unless isStructure (← getEnv) c do - throwError "'{c}' is not a structure" - pure c - | _ => throwError "expected structure" - 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 +register_builtin_option structureDiamondWarning : Bool := { + defValue := true -- TODO: set as false after finishing support for diamonds + descr := "enable/disable warning messages for structure diamonds" +} + +/-- 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 + let fieldNames := getStructureFieldsFlattened (← getEnv) parentStructName + for fieldName in fieldNames do + if containsFieldName infos fieldName then + return some fieldName + return none + private partial def processSubfields (structDeclName : Name) (parentFVar : Expr) (parentStructName : Name) (subfieldNames : Array Name) (infos : Array StructFieldInfo) (k : Array StructFieldInfo → TermElabM α) : TermElabM α := - let rec loop (i : Nat) (infos : Array StructFieldInfo) := do + go 0 infos +where + go (i : Nat) (infos : Array StructFieldInfo) := do if h : i < subfieldNames.size then let subfieldName := subfieldNames.get ⟨i, h⟩ if containsFieldName infos subfieldName then @@ -255,28 +263,65 @@ private partial def processSubfields (structDeclName : Name) (parentFVar : Expr) its default value is overwritten in the structure. -/ let declName := structDeclName ++ subfieldName let infos := infos.push { name := subfieldName, declName, fvar := subfieldFVar, kind := StructFieldKind.fromParent } - loop (i+1) infos + go (i+1) infos + else + k infos + +private partial def copyNewFieldsFrom (view : StructView) (infos : Array StructFieldInfo) (parent : Expr) (parentStructName : Name) (k : Array StructFieldInfo → TermElabM α) : TermElabM α := do + let fieldNames := getStructureFieldsFlattened (← getEnv) parentStructName + let rec go (i : Nat) (infos : Array StructFieldInfo) : TermElabM α := do + if h : i < fieldNames.size then + let fieldName := fieldNames.get ⟨i, h⟩ + let fieldType ← getFieldType parent fieldName + match (← findFieldInfo? infos fieldName) with + | some existingFieldInfo => + let existingFieldType ← inferType existingFieldInfo.fvar + unless (← isDefEq fieldType existingFieldType) do + throwError "parent field type mismatch, field '{fieldName}' from parent '{parentStructName}' {← mkHasTypeButIsExpectedMsg fieldType existingFieldType}" + go (i+1) infos + | none => + /- TODO: we are ignoring the following information from the `fieldName` declaraion at `parentStructName`. + - Binder annotation + - Visibility annotation (private/protected) + - `inferMod` + - Default value. + -/ + withLocalDeclD fieldName fieldType fun fieldFVar => do + let fieldDeclName := view.declName ++ fieldName + let infos := infos.push { name := fieldName, declName := fieldDeclName, fvar := fieldFVar, value? := none, + kind := StructFieldKind.newField, inferMod := false } + go (i+1) infos + else + k infos + go 0 infos + +private partial def withParents (view : StructView) (k : Array StructFieldInfo → TermElabM α) : TermElabM α := do + go 0 #[] +where + go (i : Nat) (infos : Array StructFieldInfo) : TermElabM α := do + if h : i < view.parents.size then + let parentStx := view.parents.get ⟨i, h⟩ + withRef parentStx do + let parent ← Term.elabType parentStx + let parentStructName ← getStructureName parent + if let some existingFieldName ← findExistingField? infos parentStructName then + if structureDiamondWarning.get (← getOptions) then + logWarning s!"field '{existingFieldName}' from '{parentStructName}' has already been declared" + copyNewFieldsFrom view infos parent parentStructName fun infos => go (i+1) infos + -- TODO: if `class`, then we need to create a let-decl that stores the local instance for the `parentStructure` + else + let toParentName := Name.mkSimple $ "to" ++ parentStructName.eraseMacroScopes.getString! -- erase macro scopes? + if containsFieldName infos toParentName then + throwErrorAt parentStx "field '{toParentName}' has already been declared" + let env ← getEnv + let binfo := if view.isClass && isClass env parentStructName then BinderInfo.instImplicit else BinderInfo.default + withLocalDecl toParentName binfo parent fun parentFVar => + let infos := infos.push { name := toParentName, declName := view.declName ++ toParentName, fvar := parentFVar, kind := StructFieldKind.subobject } + let subfieldNames := getStructureFieldsFlattened env parentStructName + processSubfields view.declName parentFVar parentStructName subfieldNames infos fun infos => go (i+1) infos else k infos - loop 0 infos -private partial def withParents (view : StructView) (i : Nat) (infos : Array StructFieldInfo) (k : Array StructFieldInfo → TermElabM α) : TermElabM α := do - if h : i < view.parents.size then - let parentStx := view.parents.get ⟨i, h⟩ - withRef parentStx do - let parent ← Term.elabType parentStx - let parentName ← checkParentIsStructure parent - let toParentName := Name.mkSimple $ "to" ++ parentName.eraseMacroScopes.getString! -- erase macro scopes? - if containsFieldName infos toParentName then - throwErrorAt parentStx "field '{toParentName}' has already been declared" - let env ← getEnv - let binfo := if view.isClass && isClass env parentName then BinderInfo.instImplicit else BinderInfo.default - withLocalDecl toParentName binfo parent fun parentFVar => - let infos := infos.push { name := toParentName, declName := view.declName ++ toParentName, fvar := parentFVar, kind := StructFieldKind.subobject } - let subfieldNames := getStructureFieldsFlattened env parentName - processSubfields view.declName parentFVar parentName subfieldNames infos fun infos => withParents view (i+1) infos k - else - k infos private def elabFieldTypeValue (view : StructFieldView) : TermElabM (Option Expr × Option Expr) := do Term.withAutoBoundImplicit <| Term.elabBinders view.binders.getArgs fun params => do @@ -516,7 +561,7 @@ private def elabStructureView (view : StructView) : TermElabM Unit := do let type ← Term.elabType view.type unless validStructType type do throwErrorAt view.type "expected Type" withRef view.ref do - withParents view 0 #[] fun fieldInfos => + withParents view fun fieldInfos => withFields view.fields 0 fieldInfos fun fieldInfos => do Term.synthesizeSyntheticMVarsNoPostponing let u ← getResultUniverse type @@ -554,6 +599,7 @@ private def elabStructureView (view : StructView) : TermElabM Unit := do let projInstances := instParents.toList.map fun info => info.declName Term.applyAttributesAt view.declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking projInstances.forM fun declName => addInstance declName AttributeKind.global (eval_prio default) + -- TODO: we must create `to` functions for the parent structures that have been flattened, and mark them as instances (if class) let lctx ← getLCtx let fieldsWithDefault := fieldInfos.filter fun info => info.value?.isSome let defaultAuxDecls ← fieldsWithDefault.mapM fun info => do diff --git a/tests/lean/diamond1.lean b/tests/lean/diamond1.lean new file mode 100644 index 0000000000..54d93ea796 --- /dev/null +++ b/tests/lean/diamond1.lean @@ -0,0 +1,27 @@ +structure Bar (α : Type) where + a : α + b : Nat → α + +structure Baz (α : Type) where + a : α → α + c : Bool → α + d : Nat + +set_option structureDiamondWarning false in +structure Foo (α : Type) extends Bar α, Baz α -- Error: parent field type mismatch + +set_option structureDiamondWarning false in +structure Foo (α : Type) extends Bar (α → α), Baz α + +#print Foo + +def f (x : Nat) : Foo Nat := + { a := fun y => x + y + b := (. + .) + c := fun _ => x + d := x } + +#print f + +set_option structureDiamondWarning true in +structure Foo' (α : Type) extends Bar (α → α), Baz α -- Warning: parent field duplication diff --git a/tests/lean/diamond1.lean.expected.out b/tests/lean/diamond1.lean.expected.out new file mode 100644 index 0000000000..c46ed88a08 --- /dev/null +++ b/tests/lean/diamond1.lean.expected.out @@ -0,0 +1,10 @@ +diamond1.lean:11:40-11:45: error: parent field type mismatch, field 'a' from parent 'Baz' has type + α → α : Type +but is expected to have type + α : Type +inductive Foo : Type → Type +constructors: +Foo.mk : {α : Type} → Bar (α → α) → (Bool → α) → Nat → Foo α +def f : Nat → Foo Nat := +fun x => { toBar := { a := fun y => x + y, b := fun a a_1 => a + a_1 }, c := fun x_1 => x, d := x } +diamond1.lean:27:47-27:52: warning: field 'a' from 'Baz' has already been declared diff --git a/tests/lean/struct1.lean b/tests/lean/struct1.lean index 2cc3e72bcb..f6cc3037f4 100644 --- a/tests/lean/struct1.lean +++ b/tests/lean/struct1.lean @@ -11,8 +11,8 @@ structure S : Nat := -- error expected Type structure S extends Nat → Nat := -- error expected structure (x : Nat) - -structure S extends A Nat, A Bool := -- error field toA already declared +set_option structureDiamondWarning true in +structure S' extends A Nat, A Bool := -- error field toA already declared (x : Nat) structure S extends A Nat, B Bool := -- error field `x` from `B` has already been declared diff --git a/tests/lean/struct1.lean.expected.out b/tests/lean/struct1.lean.expected.out index b2455de782..1a821f7bcf 100644 --- a/tests/lean/struct1.lean.expected.out +++ b/tests/lean/struct1.lean.expected.out @@ -1,7 +1,15 @@ struct1.lean:9:14-9:17: error: expected Type struct1.lean:12:20-12:29: error: expected structure -struct1.lean:15:27-15:33: error: field 'toA' has already been declared -struct1.lean:18:27-18:33: error: field 'x' from 'B' has already been declared +struct1.lean:15:28-15:34: warning: field 'x' from 'A' has already been declared +struct1.lean:15:28-15:34: error: parent field type mismatch, field 'x' from parent 'A' has type + Bool : Type +but is expected to have type + Nat : Type +struct1.lean:18:27-18:33: warning: field 'x' from 'B' has already been declared +struct1.lean:18:27-18:33: error: parent field type mismatch, field 'x' from parent 'B' has type + Bool : Type +but is expected to have type + Nat : Type struct1.lean:29:1-29:2: error: field 'x' has already been declared struct1.lean:32:1-32:2: error: field 'x' has been declared in parent structure struct1.lean:35:6-35:10: error: type mismatch