max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: auxiliary _default declaration name for parent default field values set in substructures

Browse source
This commit is contained in:
Leonardo de Moura 2020-07-24 15:54:55 -07:00
parent fb5440a074
commit 857013634d
1 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Lean/Elab/Structure.lean
View file

@ -207,7 +207,7 @@ infos.find? fun info => info.name == fieldName
private def containsFieldName (infos : Array StructFieldInfo) (fieldName : Name) : Bool :=
(findFieldInfo? infos fieldName).isSome
private partial def processSubfields {α} (ref : Syntax) (parentFVar : Expr) (parentStructName : Name) (subfieldNames : Array Name)
private partial def processSubfields {α} (ref : Syntax) (structDeclName : Name) (parentFVar : Expr) (parentStructName : Name) (subfieldNames : Array Name)
: Nat → Array StructFieldInfo → (Array StructFieldInfo → TermElabM α) → TermElabM α
| i, infos, k =>
if h : i < subfieldNames.size then do
@ -218,7 +218,10 @@ private partial def processSubfields {α} (ref : Syntax) (parentFVar : Expr) (pa
val ← Term.liftMetaM ref $ Meta.mkProjection parentFVar subfieldName;
type ← Term.inferType ref val;
Term.withLetDecl ref subfieldName type val fun subfieldFVar =>
let infos := infos.push { name := subfieldName, declName := arbitrary _, fvar := subfieldFVar, kind := StructFieldKind.fromParent };
/- The following `declName` is only used for creating the `_default` auxiliary declaration name when
its default value is overwritten in the structure. -/
let declName := structDeclName ++ subfieldName;
let infos := infos.push { name := subfieldName, declName := declName, fvar := subfieldFVar, kind := StructFieldKind.fromParent };
processSubfields (i+1) infos k
else
k infos
@ -237,7 +240,7 @@ private partial def withParents {α} (view : StructView) : Nat → Array StructF
Term.withLocalDecl parentStx 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 parentStx parentFVar parentName subfieldNames 0 infos fun infos => withParents (i+1) infos k
processSubfields parentStx view.declName parentFVar parentName subfieldNames 0 infos fun infos => withParents (i+1) infos k
else
k infos