From 801acd3e620578f505f180dc159c7a74b8bb2c88 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 21 Jul 2020 14:57:36 -0700 Subject: [PATCH] feat: elaborate fields --- src/Lean/Elab/Structure.lean | 56 ++++++++++++++++++++++++---- tests/lean/struct1.lean | 16 ++++++++ tests/lean/struct1.lean.expected.out | 19 ++++++++++ 3 files changed, 83 insertions(+), 8 deletions(-) diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 98d018b10c..841c2e2ea7 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -139,7 +139,7 @@ fieldBinders.foldlM let declName := structDeclName ++ name; declName ← applyVisibility ident modifiers.visibility declName; pure $ views.push { - ref := fieldBinder, + ref := ident, modifiers := modifiers, binderInfo := binfo, inferMod := inferMod, @@ -165,8 +165,11 @@ match parent.getAppFn with pure c | _ => Term.throwError ref $ "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 := -infos.any fun info => info.name == fieldName +(findFieldInfo? infos fieldName).isSome private partial def processSubfields {α} (ref : Syntax) (parentFVar : Expr) (parentStructName : Name) (subfieldNames : Array Name) : Nat → Array StructFieldInfo → (Array StructFieldInfo → TermElabM α) → TermElabM α @@ -204,19 +207,56 @@ private partial def withParents {α} (view : StructView) : Nat → Array StructF private partial def withFields {α} (views : Array StructFieldView) : Nat → Array StructFieldInfo → (Array StructFieldInfo → TermElabM α) → TermElabM α | i, infos, k => - if h : i < views.size then + if h : i < views.size then do let view := views.get ⟨i, h⟩; - Term.elabBinders view.binders.getArgs $ fun params => - - k infos + (type?, value?) ← Term.elabBinders view.binders.getArgs $ fun params => do { + type? ← match view.type? with + | none => pure none + | some typeStx => do { type ← Term.elabType typeStx; type ← Term.mkForall typeStx params type; pure $ some type }; + value? ← match view.value? with + | none => pure none + | some valStx => do { + value ← Term.elabTerm valStx type?; + value ← Term.mkLambda valStx params value; + value ← Term.ensureHasType valStx type? value; + pure $ some value + }; + pure (type?, value?) + }; + match findFieldInfo? infos view.name with + | none => do + match type?, value? with + | none, none => Term.throwError view.ref "invalid field, type expected" + | some type, _ => + Term.withLocalDecl view.ref view.name view.binderInfo type $ fun fieldFVar => + let infos := infos.push { name := view.name, fvar := fieldFVar, value? := value?, kind := StructFieldKind.newField }; + withFields (i+1) infos k + | none, some value => do + type ← Term.inferType view.ref value; + Term.withLocalDecl view.ref view.name view.binderInfo type $ fun fieldFVar => + let infos := infos.push { name := view.name, fvar := fieldFVar, kind := StructFieldKind.newField }; + withFields (i+1) infos k + | some info => + match info.kind with + | StructFieldKind.newField => Term.throwError view.ref ("field '" ++ view.name ++ "' has already been declared") + | StructFieldKind.fromParent => + match value?, type? with + | none, _ => Term.throwError view.ref ("field '" ++ view.name ++ "' has been declared in parent structure") + | _, some _ => Term.throwError view.type?.get! ("omit field '" ++ view.name ++ "' type to set default value") + | some value, none => do + fvarType ← Term.inferType view.ref info.fvar; + value ← Term.ensureHasType view.value?.get! fvarType value; + let infos := infos.push { info with value? := value }; + withFields (i+1) infos k + | StructFieldKind.subobject => unreachable! else k infos private def elabStructureView (view : StructView) : TermElabM ElabStructResult := do type ← Term.elabType view.type; unless (validStructType type) $ Term.throwError view.type "expected Type"; -withParents view 0 #[] fun fieldInfos => do - +withParents view 0 #[] fun fieldInfos => +withFields view.fields 0 fieldInfos fun fieldInfos => -- TODO Term.throwError view.ref "WIP" diff --git a/tests/lean/struct1.lean b/tests/lean/struct1.lean index 280869c92b..ba6ec0ea98 100644 --- a/tests/lean/struct1.lean +++ b/tests/lean/struct1.lean @@ -23,3 +23,19 @@ structure S := -- error '_' is not allowed structure S := -- error '_' is not allowed (x _y : Nat) + +structure S := +(x : Nat) +(x : Nat) -- error + +structure S extends A Nat := +(x : Nat) -- error + +structure S extends A Nat := +(x := true) -- error type mismatch + +structure S extends A Nat := +(x : Bool := true) -- error omit type + +structure S := +(x : Nat := true) -- error type mismatch diff --git a/tests/lean/struct1.lean.expected.out b/tests/lean/struct1.lean.expected.out index 113ad0eb72..d765df5cbe 100644 --- a/tests/lean/struct1.lean.expected.out +++ b/tests/lean/struct1.lean.expected.out @@ -4,3 +4,22 @@ struct1.lean:15:27: error: field 'toA' has already been declared struct1.lean:18:27: error: field 'x' from 'B' has already been declared struct1.lean:22:1: error: invalid field name '_x', identifiers starting with '_' are reserved to the system struct1.lean:25:3: error: invalid field name '_y', identifiers starting with '_' are reserved to the system +struct1.lean:29:1: error: field 'x' has already been declared +struct1.lean:32:1: error: field 'x' has been declared in parent structure +struct1.lean:35:6: error: type mismatch + true +has type + Bool +but it is expected to have type + Nat +failed to synthesize instance + CoeT Bool true Nat +struct1.lean:38:5: error: omit field 'x' type to set default value +struct1.lean:41:12: error: type mismatch + true +has type + Bool +but it is expected to have type + Nat +failed to synthesize instance + CoeT Bool true Nat