From 3f98f6bc07c76444b04d21e034d023fb282b4091 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 30 Mar 2025 10:40:36 -0700 Subject: [PATCH] feat: structure instance notation elaboration improvements (#7717) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR changes how `{...}`/`where` notation ("structure instance notation") elaborates. The notation now tries to simulate a flat representation as much as possible, without exposing the details of subobjects. Features: - When fields are elaborated, their expected types now have a couple reductions applied. For all projections and constructors associated to the structure and its parents, projections of constructors are reduced and constructors of projections are eta reduced, and also implementation detail local variables are zeta reduced in propositions (so tactic proofs should never see them anymore). Furthermore, field values are beta reduced automatically in successive field types. The example in [mathlib4#12129](https://github.com/leanprover-community/mathlib4/issues/12129#issuecomment-2056134533) now shows a goal of `0 = 0` rather than `{ toFun := fun x => x }.toFun 0 = 0`. - All parents can now be used as field names, not just the subobject parents. These are like additional sources but with three constraints: every field of the value must be used, the fields must not overlap with other provided fields, and every field of the specified parent must be provided for. Similar to sources, the values are hoisted to `let`s if they are not already variables, to avoid multiple evaluation. They are implementation detail local variables, so they get unfolded for successive fields. - All class parents are now used to fill in missing fields, not just the subobject parents. Closes #6046. Rules: (1) only those parents whose fields are a subset of the remaining fields are considered, (2) parents are considered only before any fields are elaborated, and (3) only those parents whose type can be computed are considered (this can happen if a parent depends on another parent, which is possible since #7302). - Default values and autoparams now respect the resolution order completely: each field has at most one default value definition that can provide for it. The algorithm that tries to unstick default values by walking up the subobject hierarchy has been removed. If there are applications of default value priorities, we might consider it in a future release. - The resulting constructors are now fully packed. This is implemented by doing structure eta reduction of the elaborated expressions. - "Magic field definitions" (as reported [on Zulip](https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Where.20is.20sSup.20defined.20on.20submodules.3F/near/499578795)) have been eliminated. This was where fields were being solved for by unification, tricking the default value system into thinking they had actually been provided. Now the default value system keeps track of which fields it has actually solved for, and which fields the user did not provide. Explicit structure fields (the default kind) without any explicit value definition will result in an error. If it was solved for by unification, the error message will include the inferred value, like "field 'f' must be explicitly provided, its synthesized value is v" - When the notation is used in patterns, it now no longer inserts fields using class parents, and it no longer applies autoparams or default values. The motivation is that one expects patterns to match only the given fields. This is still imperfect, since fields might be solved for indirectly. - Elaboration now attempts error recovery. Extraneous fields log errors and are ignored, missing fields are filled with `sorry`. This is a breaking change, but generally the mitigation is to remove `dsimp only` from the beginnings of proofs. Sometimes "magic fields" need to be provided — four possible mitigations are (1) to provide the field, (2) to provide `_` for the value of the field, (3) to add `..` to the structure instance notation, (4) or decide to modify the `structure` command to make the field implicit. Lastly, sometimes parent instances don't apply when they should. This could be because some of the provided fields overlap with the class, or it could be that the parent depends on some of the fields for synthesis — and as parents are only considered before any fields are elaborated, such parents might not be possible to use — we will look into refining this further. There is also a change to elaboration: now the `afterTypeChecking` attributes are run with all `structure` data set up (e.g. the list of parents, along with all parent projections in the environment). This is necessary since attributes like `@[ext]` use structure instance notation, and the notation needs all this data to be set up now. --- src/Init/Internal/Order/Basic.lean | 2 +- src/Lean/Elab/MutualInductive.lean | 16 +- src/Lean/Elab/Print.lean | 9 +- src/Lean/Elab/StructInst.lean | 1839 +++++++++-------- src/Lean/Elab/Structure.lean | 83 +- src/Lean/Elab/Tactic/Omega/Core.lean | 6 +- src/Lean/Meta/Structure.lean | 65 + src/Lean/Structure.lean | 90 +- src/lake/Lake/Load/Toml.lean | 1 + tests/lean/autoIssue.lean | 2 +- tests/lean/autoIssue.lean.expected.out | 2 +- tests/lean/diamond2.lean | 6 +- tests/lean/mkProjStx.lean | 25 - tests/lean/mkProjStx.lean.expected.out | 3 - tests/lean/run/1986.lean | 2 + tests/lean/run/3150.lean | 17 +- tests/lean/run/3807.lean | 11 +- tests/lean/run/4534.lean | 2 + tests/lean/run/461b.lean | 7 +- tests/lean/run/5406.lean | 19 +- tests/lean/run/6123_cat_adjunction.lean | 1 - tests/lean/run/7353.lean | 3 +- tests/lean/run/linearCategory_perf_issue.lean | 4 - tests/lean/run/mathlibetaissue.lean | 1 + tests/lean/run/solve_by_elim.lean | 2 +- tests/lean/run/structInst.lean | 161 +- tests/lean/run/structInst3.lean | 66 +- tests/lean/run/structInst4.lean | 89 +- tests/lean/{ => run}/structInstExtraEta.lean | 21 +- tests/lean/run/structInstFast.lean | 2 +- tests/lean/run/structInstUpdates.lean | 17 + tests/lean/run/structNamedParentProj.lean | 12 + tests/lean/run/struct_inst_typed.lean | 13 +- tests/lean/run/structureElab.lean | 82 +- tests/lean/run/tactic_config.lean | 11 + tests/lean/structInst1.lean.expected.out | 2 +- .../lean/structInstExtraEta.lean.expected.out | 9 - ...ctInstSourcesLeftToRight.lean.expected.out | 4 +- tests/pkg/prv/Prv.lean | 2 +- 39 files changed, 1595 insertions(+), 1114 deletions(-) delete mode 100644 tests/lean/mkProjStx.lean delete mode 100644 tests/lean/mkProjStx.lean.expected.out rename tests/lean/{ => run}/structInstExtraEta.lean (56%) create mode 100644 tests/lean/run/structInstUpdates.lean delete mode 100644 tests/lean/structInstExtraEta.lean.expected.out diff --git a/src/Init/Internal/Order/Basic.lean b/src/Init/Internal/Order/Basic.lean index 7978f6c86f..d0a0fbf9e9 100644 --- a/src/Init/Internal/Order/Basic.lean +++ b/src/Init/Internal/Order/Basic.lean @@ -488,7 +488,7 @@ 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 - dsimp + try dsimp -- TODO(kmill) remove constructor next => intro ⟨h₁, h₂⟩ ⟨a', b'⟩ cab diff --git a/src/Lean/Elab/MutualInductive.lean b/src/Lean/Elab/MutualInductive.lean index 20209e732e..12f1b4c7c3 100644 --- a/src/Lean/Elab/MutualInductive.lean +++ b/src/Lean/Elab/MutualInductive.lean @@ -121,6 +121,12 @@ structure ElabHeaderResult extends PreElabHeaderResult where indFVar : Expr deriving Inhabited +/-- An intermediate step for mutual inductive elaboration. See `InductiveElabDescr` -/ +structure InductiveElabStep3 where + /-- Finalize the inductive type, after they are all added to the environment, after auxiliary definitions are added, and after computed fields are registered. + The `levelParams`, `params`, and `replaceIndFVars` arguments of `prefinalize` are still valid here. -/ + finalize : TermElabM Unit := pure () + /-- An intermediate step for mutual inductive elaboration. See `InductiveElabDescr`. -/ structure InductiveElabStep2 where /-- The constructors produced by `InductiveElabStep1`. -/ @@ -133,9 +139,7 @@ structure InductiveElabStep2 where /-- Step to finalize term elaboration, done immediately after universe level processing is complete. -/ finalizeTermElab : TermElabM Unit := pure () /-- Like `finalize`, but occurs before `afterTypeChecking` attributes. -/ - prefinalize (levelParams : List Name) (params : Array Expr) (replaceIndFVars : Expr → MetaM Expr) : TermElabM Unit := fun _ _ _ => pure () - /-- Finalize the inductive type, after they are all added to the environment, after auxiliary definitions are added, and after computed fields are registered. -/ - finalize (levelParams : List Name) (params : Array Expr) (replaceIndFVars : Expr → MetaM Expr) : TermElabM Unit := fun _ _ _ => pure () + prefinalize (levelParams : List Name) (params : Array Expr) (replaceIndFVars : Expr → MetaM Expr) : TermElabM InductiveElabStep3 := fun _ _ _ => pure {} deriving Inhabited /-- An intermediate step for mutual inductive elaboration. See `InductiveElabDescr`. -/ @@ -160,7 +164,7 @@ Elaboration occurs in the following steps: - Elaboration of constructors is finalized, with additional tasks done by each `InductiveStep2.collectUniverses`. - The inductive family is added to the environment and is checked by the kernel. - Attributes and other finalization activities are performed, including those defined - by `InductiveStep2.prefinalize` and `InductiveStep2.finalize`. + by `InductiveStep2.prefinalize` and `InductiveStep3.finalize`. -/ structure InductiveElabDescr where mkInductiveView : Modifiers → Syntax → TermElabM InductiveElabStep1 @@ -1048,9 +1052,9 @@ private def elabInductiveViewsPostprocessing (views : Array InductiveView) (res let ref := view0.ref applyComputedFields views -- NOTE: any generated code before this line is invalid liftTermElabM <| withMCtx res.mctx <| withLCtx res.lctx res.localInsts do - for elab' in res.elabs do elab'.prefinalize res.levelParams res.params res.replaceIndFVars + let finalizers ← res.elabs.mapM fun elab' => elab'.prefinalize res.levelParams res.params res.replaceIndFVars for view in views do withRef view.declId <| Term.applyAttributesAt view.declName view.modifiers.attrs .afterTypeChecking - for elab' in res.elabs do elab'.finalize res.levelParams res.params res.replaceIndFVars + for elab' in finalizers do elab'.finalize applyDerivingHandlers views runTermElabM fun _ => Term.withDeclName view0.declName do withRef ref do for view in views do withRef view.declId <| Term.applyAttributesAt view.declName view.modifiers.attrs .afterCompilation diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean index 06c22150b1..e8587b56ad 100644 --- a/src/Lean/Elab/Print.lean +++ b/src/Lean/Elab/Print.lean @@ -81,7 +81,7 @@ private partial def getFieldOrigin (structName field : Name) : MetaM StructureFi return fi open Meta in -private partial def printStructure (id : Name) (levelParams : List Name) (numParams : Nat) (type : Expr) +private partial def printStructure (id : Name) (levelParams : List Name) (numParams : Nat) (type : Expr) (ctor : Name) (isUnsafe : Bool) : CommandElabM Unit := do let env ← getEnv let kind := if isClass env id then "class" else "structure" @@ -107,8 +107,9 @@ private partial def printStructure (id : Name) (levelParams : List Name) (numPar 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 := mkFlatCtorOfStructName id - let autoParams : NameMap Syntax ← forallTelescope (← getConstInfo flatCtorName).type fun args _ => + let flatCtorName := mkFlatCtorOfStructCtorName ctor + let flatCtorInfo ← try getConstInfo flatCtorName catch _ => getConstInfo (id ++ `_flat_ctor) -- TODO(kmill): remove catch + let autoParams : NameMap Syntax ← forallTelescope flatCtorInfo.type fun args _ => args[numParams:].foldlM (init := {}) fun set arg => do let decl ← arg.fvarId!.getDecl if let some (.const tacticDecl _) := decl.type.getAutoParamTactic? then @@ -187,7 +188,7 @@ private def printIdCore (id : Name) : CommandElabM Unit := do | ConstantInfo.recInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "recursor" id us t u | ConstantInfo.inductInfo { levelParams := us, numParams, type := t, ctors, isUnsafe := u, .. } => if isStructure env id then - printStructure id us numParams t u + printStructure id us numParams t ctors[0]! u else printInduct id us numParams t ctors u | none => throwUnknownId id diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index 2953888bb4..e678cfd90a 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/src/Lean/Elab/StructInst.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura +Authors: Leonardo de Moura, Kyle Miller -/ prelude import Lean.Util.FindExpr @@ -18,7 +18,9 @@ A *structure instance* is notation to construct a term of a `structure`. Examples: `{ x := 2, y.z := true }`, `{ s with cache := c' }`, and `{ s with values[2] := v }`. Structure instances are the preferred way to invoke a `structure`'s constructor, since they hide Lean implementation details such as whether parents are represented as subobjects, -and also they do correct processing of default values, which are complicated due to the fact that `structure`s can override default values of their parents. +and also they do correct processing of default values, +which are complicated due to the fact that `structure`s can override default values of their parents, +and furthermore overridden default values can use fields that come after in the order the fields appear in the constructor. This module elaborates structure instance notation. Note that the `where` syntax to define structures (`Lean.Parser.Command.whereStructInst`) @@ -73,7 +75,7 @@ Structure instance notation makes use of the expected type. let stxNew := stx.setArg 4 mkNullNode `(($stxNew : $expected)) -def mkStructInstField (lval : TSyntax ``Parser.Term.structInstLVal) (binders : TSyntaxArray ``Parser.Term.structInstFieldBinder) +private def mkStructInstField (lval : TSyntax ``Parser.Term.structInstLVal) (binders : TSyntaxArray ``Parser.Term.structInstFieldBinder) (type? : Option Term) (val : Term) : MacroM (TSyntax ``Parser.Term.structInstField) := do let mut val := val if let some type := type? then @@ -124,67 +126,14 @@ Expands fields. let structInstFields := structInstFields.setArg 0 <| Syntax.mkSep fields (mkAtomFrom stx ", ") return stx.setArg 2 structInstFields -/-- -If `stx` is of the form `{ s₁, ..., sₙ with ... }` and `sᵢ` is not a local variable, -expands into `let __src := sᵢ; { ..., __src, ... with ... }`. -The significance of `__src` is that the variable is treated as an implementation-detail local variable, -which can be unfolded by `simp` when `zetaDelta := false`. - -Note that this one is not a `Macro` because we need to access the local context. --/ -private def expandNonAtomicExplicitSources (stx : Syntax) : TermElabM (Option Syntax) := do - let sourcesOpt := stx[1] - if sourcesOpt.isNone then - return none - else - let sources := sourcesOpt[0] - if sources.isMissing then - throwAbortTerm - let sources := sources.getSepArgs - if (← sources.allM fun source => return (← isLocalIdent? source).isSome) then - return none - if sources.any (·.isMissing) then - throwAbortTerm - return some (← go sources.toList #[]) -where - go (sources : List Syntax) (sourcesNew : Array Syntax) : TermElabM Syntax := do - match sources with - | [] => - let sources := Syntax.mkSep sourcesNew (mkAtomFrom stx ", ") - return stx.setArg 1 (stx[1].setArg 0 sources) - | source :: sources => - if (← isLocalIdent? source).isSome then - go sources (sourcesNew.push source) - else - withFreshMacroScope do - /- - Recall that local variables starting with `__` are treated as impl detail. - See `LocalContext.lean`. - Moreover, implementation detail let-vars are unfolded by `simp` - even when `zetaDelta := false`. - Motivation: the following failure when `zetaDelta := true` - ``` - structure A where - a : Nat - structure B extends A where - b : Nat - w : a = b - def x : A where a := 37 - @[simp] theorem x_a : x.a = 37 := rfl - - def y : B := { x with b := 37, w := by simp } - ``` - -/ - let sourceNew ← `(__src) - let r ← go sources (sourcesNew.push sourceNew) - `(let __src := $source; $r) - /-- An *explicit source* is one of the structures `sᵢ` that appear in `{ s₁, …, sₙ with … }`. -/ structure ExplicitSourceView where /-- The syntax of the explicit source. -/ stx : Syntax + /-- The local variable for this source. -/ + fvar : Expr /-- The name of the structure for the type of the explicit source. -/ structName : Name deriving Inhabited @@ -199,11 +148,6 @@ structure SourcesView where implicit : Option Syntax deriving Inhabited -/-- Returns `true` if the structure instance has no sources (neither explicit sources nor a `..`). -/ -def SourcesView.isNone : SourcesView → Bool - | { explicit := #[], implicit := none } => true - | _ => false - /-- Given an array of explicit sources, returns syntax of the form `optional (atomic (sepBy1 termParser ", " >> " with ")` @@ -229,7 +173,7 @@ private def getStructSources (structStx : Syntax) : TermElabM SourcesView := let srcType ← whnf (← inferType src) tryPostponeIfMVar srcType let structName ← getStructureName srcType - return { stx, structName } + return { stx, fvar := src, structName } let implicit := if implicitSource[0].isNone then none else implicitSource return { explicit, implicit } @@ -256,15 +200,15 @@ private def isModifyOp? (stx : Syntax) : TermElabM (Option Syntax) := do match s? with | none => return some arg | some s => - if s.getKind == ``Lean.Parser.Term.structInstArrayRef then - throwErrorAt arg "invalid \{...} notation, at most one `[..]` at a given level" + if s[0][0].getKind == ``Lean.Parser.Term.structInstArrayRef then + throwErrorAt arg "invalid \{...} notation, can have at most one `[..]` at a given level" else throwErrorAt arg "invalid \{...} notation, can't mix field and `[..]` at a given level" else match s? with | none => return some arg | some s => - if s.getKind == ``Lean.Parser.Term.structInstArrayRef then + if s[0][0].getKind == ``Lean.Parser.Term.structInstArrayRef then throwErrorAt arg "invalid \{...} notation, can't mix field and `[..]` at a given level" else return s? @@ -278,13 +222,16 @@ private def isModifyOp? (stx : Syntax) : TermElabM (Option Syntax) := do Given a `stx` that is a structure instance notation that's a modifyOp (according to `isModifyOp?`), elaborates it. Only supports structure instances with a single source. -/ -private def elabModifyOp (stx modifyOp : Syntax) (sources : Array ExplicitSourceView) (expectedType? : Option Expr) : TermElabM Expr := do - if sources.size > 1 then - throwError "invalid \{...} notation, multiple sources and array update is not supported." +private def elabModifyOp (stx modifyOp : Syntax) (sourcesView : SourcesView) (expectedType? : Option Expr) : TermElabM Expr := do + unless sourcesView.explicit.size == 1 do + throwError "invalid \{...} notation, exactly one explicit source is required when using '[] := ' update notation" + if let some implicit := sourcesView.implicit then + throwErrorAt implicit "invalid \{...} notation, '[] := ' update notation does not support ellipsis" + let source := sourcesView.explicit[0]! let cont (val : Syntax) : TermElabM Expr := do let lval := modifyOp[0][0] let idx := lval[1] - let self := sources[0]!.stx + let self := source.stx let stxNew ← `($(self).modifyOp (idx := $idx) (fun s => $val)) trace[Elab.struct.modifyOp] "{stx}\n===>\n{stxNew}" withMacroExpansion stx stxNew <| elabTerm stxNew expectedType? @@ -304,47 +251,16 @@ private def elabModifyOp (stx modifyOp : Syntax) (sources : Array ExplicitSource trace[Elab.struct.modifyOp] "{stx}\nval: {val}" cont val -/-- -Gets the structure name for the structure instance from the expected type and the sources. -This method tries to postpone execution if the expected type is not available. - -If the expected type is available and it is a structure, then we use it. -Otherwise, we use the type of the first source. --/ -private def getStructName (expectedType? : Option Expr) (sourceView : SourcesView) : TermElabM Name := do - tryPostponeIfNoneOrMVar expectedType? - let useSource : Unit → TermElabM Name := fun _ => do - unless sourceView.explicit.isEmpty do - return sourceView.explicit[0]!.structName - match expectedType? with - | some expectedType => throwUnexpectedExpectedType expectedType - | none => throwUnknownExpectedType - match expectedType? with - | none => useSource () - | some expectedType => - let expectedType ← whnf expectedType - match expectedType.getAppFn with - | Expr.const constName _ => - unless isStructure (← getEnv) constName do - throwError "invalid \{...} notation, structure type expected{indentExpr expectedType}" - return constName - | _ => useSource () -where - throwUnknownExpectedType := - throwError "invalid \{...} notation, expected type is not known" - throwUnexpectedExpectedType type (kind := "expected") := do - let type ← instantiateMVars type - if type.getAppFn.isMVar then - throwUnknownExpectedType - else - throwError "invalid \{...} notation, {kind} type is not of the form (C ...){indentExpr type}" - /-- A component of a left-hand side for a field appearing in structure instance syntax. -/ inductive FieldLHS where /-- A name component for a field left-hand side. For example, `x` and `y` in `{ x.y := v }`. -/ | fieldName (ref : Syntax) (name : Name) + /-- (Can't be written by users.) A field setting an entire parent. + The `structName` is the name of the parent structure, and `name` is the projection field name. + Always appears as the only LHS component. -/ + | parentFieldName (ref : Syntax) (structName : Name) (name : Name) /-- A numeric index component for a field left-hand side. For example `3` in `{ x.3 := v }`. -/ | fieldIndex (ref : Syntax) (idx : Nat) /-- An array indexing component for a field left-hand side. For example `[3]` in `{ arr[3] := v }`. -/ @@ -353,90 +269,49 @@ inductive FieldLHS where instance : ToFormat FieldLHS where format - | .fieldName _ n => format n - | .fieldIndex _ i => format i - | .modifyOp _ i => "[" ++ i.prettyPrint ++ "]" - -mutual - /-- - `FieldVal StructInstView` is a representation of a field value in the structure instance. - -/ - inductive FieldVal where - /-- A `term` to use for the value of the field. -/ - | term (stx : Syntax) : FieldVal - /-- A `StructInstView` to use for the value of a subobject field. -/ - | nested (s : StructInstView) : FieldVal - /-- A field that was not provided and should be synthesized using default values. -/ - | default : FieldVal - deriving Inhabited - - /-- - `Field StructInstView` is a representation of a field in the structure instance. - -/ - structure Field where - /-- The whole field syntax. -/ - ref : Syntax - /-- The LHS decomposed into components. -/ - lhs : List FieldLHS - /-- The value of the field. -/ - val : FieldVal - /-- The elaborated field value, filled in at `elabStruct`. - Missing fields use a metavariable for the elaborated value and are later solved for in `DefaultFields.propagate`. -/ - expr? : Option Expr := none - deriving Inhabited - - /-- - The view for structure instance notation. - -/ - structure StructInstView where - /-- The syntax for the whole structure instance. -/ - ref : Syntax - /-- The name of the structure for the type of the structure instance. -/ - structName : Name - /-- Used for default values, to propagate structure type parameters. It is initially empty, and then set at `elabStruct`. -/ - params : Array (Name × Expr) - /-- The fields of the structure instance. -/ - fields : List Field - /-- The additional sources for fields for the structure instance. -/ - sources : SourcesView - deriving Inhabited -end + | .fieldName _ n => format n + | .parentFieldName _ _ n => format n + | .fieldIndex _ i => format i + | .modifyOp _ i => "[" ++ i.prettyPrint ++ "]" /-- -Returns if the field has a single component in its LHS. +`Field StructInstView` is a representation of a field in the structure instance. -/ -def Field.isSimple : Field → Bool - | { lhs := [_], .. } => true - | _ => false +structure FieldView where + /-- The whole field syntax. -/ + ref : Syntax + /-- The LHS components. This is nonempty. -/ + lhs : List FieldLHS + /-- The value of the field. -/ + val : Term + deriving Inhabited -/-- `true` iff all fields of the given structure are marked as `default` -/ -partial def StructInstView.allDefault (s : StructInstView) : Bool := - s.fields.all fun { val := val, .. } => match val with - | .term _ => false - | .default => true - | .nested s => allDefault s +/-- +The view for structure instance notation. +-/ +structure StructInstView where + /-- The syntax for the whole structure instance. -/ + ref : Syntax + /-- The fields of the structure instance. -/ + fields : Array FieldView + /-- The additional sources for fields for the structure instance. -/ + sources : SourcesView + deriving Inhabited -def formatField (formatStruct : StructInstView → Format) (field : Field) : Format := - Format.joinSep field.lhs " . " ++ " := " ++ - match field.val with - | .term v => v.prettyPrint - | .nested s => formatStruct s - | .default => "" +private def formatField (field : FieldView) : Format := + Format.joinSep field.lhs " . " ++ " := " ++ format field.val -partial def formatStruct : StructInstView → Format - | ⟨_, _, _, fields, source⟩ => - let fieldsFmt := Format.joinSep (fields.map (formatField formatStruct)) ", " +private def formatStruct : StructInstView → Format + | ⟨_, fields, source⟩ => + let fieldsFmt := Format.joinSep (fields.toList.map formatField) ", " let implicitFmt := if source.implicit.isSome then " .. " else "" if source.explicit.isEmpty then "{" ++ fieldsFmt ++ implicitFmt ++ "}" else "{" ++ format (source.explicit.map (·.stx)) ++ " with " ++ fieldsFmt ++ implicitFmt ++ "}" +instance : ToFormat FieldView := ⟨formatField⟩ instance : ToFormat StructInstView := ⟨formatStruct⟩ -instance : ToString StructInstView := ⟨toString ∘ format⟩ - -instance : ToFormat Field := ⟨formatField formatStruct⟩ -instance : ToString Field := ⟨toString ∘ format⟩ /-- Converts a `FieldLHS` back into syntax. This assumes the `ref` fields have the correct structure. @@ -450,24 +325,18 @@ def structInstArrayRef := leading_parser "[" >> termParser >>"]" -/ -- Remark: this code relies on the fact that `expandStruct` only transforms `fieldLHS.fieldName` private def FieldLHS.toSyntax (first : Bool) : FieldLHS → Syntax - | .modifyOp stx _ => stx - | .fieldName stx name => if first then mkIdentFrom stx name else mkGroupNode #[mkAtomFrom stx ".", mkIdentFrom stx name] - | .fieldIndex stx _ => if first then stx else mkGroupNode #[mkAtomFrom stx ".", stx] + | .modifyOp stx .. => stx + | .fieldName stx name | .parentFieldName stx _ name => + if first then mkIdentFrom stx name else mkGroupNode #[mkAtomFrom stx ".", mkIdentFrom stx name] + | .fieldIndex stx .. => if first then stx else mkGroupNode #[mkAtomFrom stx ".", stx] /-- -Converts a `FieldVal StructInstView` back into syntax. Only supports `.term`, and it assumes the `stx` field has the correct structure. +Converts a `FieldView` back into syntax. Used to construct synthetic structure instance notation for subobjects in `StructInst.expandStruct` processing. -/ -private def FieldVal.toSyntax : FieldVal → Syntax - | .term stx => stx - | _ => unreachable! - -/-- -Converts a `Field StructInstView` back into syntax. Used to construct synthetic structure instance notation for subobjects in `StructInst.expandStruct` processing. --/ -private def Field.toSyntax : Field → Syntax +private def FieldView.toSyntax : FieldView → TSyntax ``Parser.Term.structInstField | field => let stx := field.ref - let stx := stx.setArg 1 <| stx[1].setArg 2 <| stx[1][2].setArg 1 field.val.toSyntax + let stx := stx.setArg 1 <| stx[1].setArg 2 <| stx[1][2].setArg 1 field.val match field.lhs with | first::rest => stx.setArg 0 <| mkNode ``Parser.Term.structInstLVal #[first.toSyntax true, mkNullNode <| rest.toArray.map (FieldLHS.toSyntax false) ] | _ => unreachable! @@ -486,11 +355,10 @@ private def toFieldLHS (stx : Syntax) : MacroM FieldLHS := | none => Macro.throwErrorAt stx "unexpected structure syntax" /-- -Creates a structure instance view from structure instance notation -and the computed structure name (from `Lean.Elab.Term.StructInst.getStructName`) +Creates a view from structure instance notation and structure source view (from `Lean.Elab.Term.StructInst.getStructSources`). -/ -private def mkStructView (stx : Syntax) (structName : Name) (sources : SourcesView) : MacroM StructInstView := do +private def mkStructView (stx : Syntax) (sources : SourcesView) : MacroM StructInstView := do /- Recall that `stx` is of the form ``` @@ -502,708 +370,946 @@ private def mkStructView (stx : Syntax) (structName : Name) (sources : SourcesVi ``` This method assumes that `structInstField` had already been expanded by the macro `expandStructInstFields`. -/ - let fields ← stx[2][0].getSepArgs.toList.mapM fun fieldStx => do + let fields ← stx[2][0].getSepArgs.mapM fun fieldStx => do let `(Parser.Term.structInstField| $lval:structInstLVal := $val) := fieldStx | Macro.throwUnsupported let first ← toFieldLHS lval.raw[0] let rest ← lval.raw[1].getArgs.toList.mapM toFieldLHS - return { ref := fieldStx, lhs := first :: rest, val := FieldVal.term val : Field } - return { ref := stx, structName, params := #[], fields, sources } - -def StructInstView.modifyFieldsM {m : Type → Type} [Monad m] (s : StructInstView) (f : List Field → m (List Field)) : m StructInstView := - match s with - | { ref, structName, params, fields, sources } => return { ref, structName, params, fields := (← f fields), sources } - -def StructInstView.modifyFields (s : StructInstView) (f : List Field → List Field) : StructInstView := - Id.run <| s.modifyFieldsM f - -/-- Expands name field LHSs with multi-component names into multi-component LHSs. -/ -private def expandCompositeFields (s : StructInstView) : StructInstView := - s.modifyFields fun fields => fields.map fun field => match field with - | { lhs := .fieldName _ (.str Name.anonymous ..) :: _, .. } => field - | { lhs := .fieldName ref n@(.str ..) :: rest, .. } => - let newEntries := n.components.map <| FieldLHS.fieldName ref - { field with lhs := newEntries ++ rest } - | _ => field - -/-- Replaces numeric index field LHSs with the corresponding named field, or throws an error if no such field exists. -/ -private def expandNumLitFields (s : StructInstView) : TermElabM StructInstView := - s.modifyFieldsM fun fields => do - let env ← getEnv - let fieldNames := getStructureFields env s.structName - fields.mapM fun field => match field with - | { lhs := .fieldIndex ref idx :: rest, .. } => - if idx == 0 then throwErrorAt ref "invalid field index, index must be greater than 0" - else if idx > fieldNames.size then throwErrorAt ref "invalid field index, structure has only #{fieldNames.size} fields" - else return { field with lhs := .fieldName ref fieldNames[idx - 1]! :: rest } - | _ => return field - -/-- -Expands fields that are actually represented as fields of subobject fields. - -For example, consider the following structures: -``` -structure A where - x : Nat - -structure B extends A where - y : Nat - -structure C extends B where - z : Bool -``` -This method expands parent structure fields using the path to the parent structure. -For example, -``` -{ x := 0, y := 0, z := true : C } -``` -is expanded into -``` -{ toB.toA.x := 0, toB.y := 0, z := true : C } -``` --/ -private def expandParentFields (s : StructInstView) : TermElabM StructInstView := do - let env ← getEnv - s.modifyFieldsM fun fields => fields.mapM fun field => do match field with - | { lhs := .fieldName ref fieldName :: _, .. } => - addCompletionInfo <| CompletionInfo.fieldId ref fieldName (← getLCtx) s.structName - match findField? env s.structName fieldName with - | none => throwErrorAt ref "'{fieldName}' is not a field of structure '{.ofConstName s.structName}'" - | some baseStructName => - if baseStructName == s.structName then pure field - else match getPathToBaseStructure? env baseStructName s.structName with - | some path => - let path := path.map fun funName => match funName with - | .str _ s => .fieldName ref (Name.mkSimple s) - | _ => unreachable! - return { field with lhs := path ++ field.lhs } - | _ => throwErrorAt ref "failed to access field '{fieldName}' in parent structure" - | _ => return field - -private abbrev FieldMap := Std.HashMap Name (List Field) - -/-- -Creates a hash map collecting all fields with the same first name component. -Throws an error if there are multiple simple fields with the same name. -Used by `StructInst.expandStruct` processing. --/ -private def mkFieldMap (fields : List Field) : TermElabM FieldMap := - fields.foldlM (init := {}) fun fieldMap field => - match field.lhs with - | .fieldName _ fieldName :: _ => - match fieldMap[fieldName]? with - | some (prevField::restFields) => - if field.isSimple || prevField.isSimple then - throwErrorAt field.ref "field '{fieldName}' has already been specified" - else - return fieldMap.insert fieldName (field::prevField::restFields) - | _ => return fieldMap.insert fieldName [field] - | _ => unreachable! - -/-- -Given a value of the hash map created by `mkFieldMap`, returns true if the value corresponds to a simple field. --/ -private def isSimpleField? : List Field → Option Field - | [field] => if field.isSimple then some field else none - | _ => none - -/-- -Creates projection notation for the given structure field. Used --/ -def mkProjStx? (s : Syntax) (structName : Name) (fieldName : Name) : TermElabM (Option Syntax) := do - if (findField? (← getEnv) structName fieldName).isNone then - return none - return some <| - mkNode ``Parser.Term.explicit - #[mkAtomFrom s "@", - mkNode ``Parser.Term.proj #[s, mkAtomFrom s ".", mkIdentFrom s fieldName]] - -/-- -Finds a simple field of the given name. --/ -def findField? (fields : List Field) (fieldName : Name) : Option Field := - fields.find? fun field => - match field.lhs with - | [.fieldName _ n] => n == fieldName - | _ => false - -mutual - - /-- - Groups compound fields according to which subobject they are from. - -/ - private partial def groupFields (s : StructInstView) : TermElabM StructInstView := do - let env ← getEnv - withRef s.ref do - s.modifyFieldsM fun fields => do - let fieldMap ← mkFieldMap fields - fieldMap.toList.mapM fun ⟨fieldName, fields⟩ => do - match isSimpleField? fields with - | some field => pure field - | none => - let substructFields := fields.map fun field => { field with lhs := field.lhs.tail! } - let field := fields.head! - match Lean.isSubobjectField? env s.structName fieldName with - | some substructName => - let substruct := { ref := s.ref, structName := substructName, params := #[], fields := substructFields, sources := s.sources } - let substruct ← expandStruct substruct - pure { field with lhs := [field.lhs.head!], val := FieldVal.nested substruct } - | none => - let updateSource (structStx : Syntax) : TermElabM Syntax := do - let sourcesNew ← s.sources.explicit.filterMapM fun source => mkProjStx? source.stx source.structName fieldName - let explicitSourceStx := if sourcesNew.isEmpty then mkNullNode else mkSourcesWithSyntax sourcesNew - let implicitSourceStx := s.sources.implicit.getD (mkNode ``Parser.Term.optEllipsis #[mkNullNode]) - return (structStx.setArg 1 explicitSourceStx).setArg 3 implicitSourceStx - let valStx := s.ref -- construct substructure syntax using s.ref as template - let valStx := valStx.setArg 4 mkNullNode -- erase optional expected type - let args := substructFields.toArray.map (·.toSyntax) - let fieldsStx := mkNode ``Parser.Term.structInstFields - #[mkNullNode <| mkSepArray args (mkAtom ",")] - let valStx := valStx.setArg 2 fieldsStx - let valStx ← updateSource valStx - return { field with lhs := [field.lhs.head!], val := FieldVal.term valStx } - /-- - Adds in the missing fields using the explicit sources. - Invariant: a missing field always comes from the first source that can provide it. - -/ - private partial def addMissingFields (s : StructInstView) : TermElabM StructInstView := do - let env ← getEnv - let fieldNames := getStructureFields env s.structName - let ref := s.ref.mkSynthetic - withRef ref do - let fields ← fieldNames.foldlM (init := []) fun fields fieldName => do - match findField? s.fields fieldName with - | some field => return field::fields - | none => - let addField (val : FieldVal) : TermElabM (List Field) := do - return { ref, lhs := [FieldLHS.fieldName ref fieldName], val := val } :: fields - match Lean.isSubobjectField? env s.structName fieldName with - | some substructName => - -- Get all leaf fields of `substructName` - let downFields := getStructureFieldsFlattened env substructName false - -- Filter out all explicit sources that do not share a leaf field keeping - -- structure with no fields - let filtered := s.sources.explicit.filter fun sources => - let sourceFields := getStructureFieldsFlattened env sources.structName false - sourceFields.any (fun name => downFields.contains name) || sourceFields.isEmpty - -- Take the first such one remaining - match filtered[0]? with - | some src => - -- If it is the correct type, use it - if src.structName == substructName then - addField (FieldVal.term src.stx) - -- If a projection of it is the correct type, use it - else if let some val ← mkProjStx? src.stx src.structName fieldName then - addField (FieldVal.term val) - -- No sources could provide this subobject in the proper order. - -- Recurse to handle default values for fields. - else - let substruct := { ref, structName := substructName, params := #[], fields := [], sources := s.sources } - let substruct ← expandStruct substruct - addField (FieldVal.nested substruct) - -- No sources could provide this subobject. - -- Recurse to handle default values for fields. - | none => - let substruct := { ref, structName := substructName, params := #[], fields := [], sources := s.sources } - let substruct ← expandStruct substruct - addField (FieldVal.nested substruct) - -- Since this is not a subobject field, we are free to use the first source that can - -- provide it. - | none => - if let some val ← s.sources.explicit.findSomeM? fun source => mkProjStx? source.stx source.structName fieldName then - addField (FieldVal.term val) - else if s.sources.implicit.isSome then - addField (FieldVal.term (mkHole ref)) - else - addField FieldVal.default - return { s with fields := fields.reverse } - - /-- - Expands all fields of the structure instance, consolidates compound fields into subobject fields, and adds missing fields. - -/ - private partial def expandStruct (s : StructInstView) : TermElabM StructInstView := do - let s := expandCompositeFields s - let s ← expandNumLitFields s - let s ← expandParentFields s - let s ← groupFields s - addMissingFields s - -end + return { ref := fieldStx, lhs := first :: rest, val : FieldView } + return { ref := stx, fields, sources } /-- The constructor to use for the structure instance notation. -/ -structure CtorHeaderResult where +private structure CtorHeaderResult where /-- The constructor function with applied structure parameters. -/ ctorFn : Expr /-- The type of `ctorFn` -/ ctorFnType : Expr - /-- Instance metavariables for structure parameters that are instance implicit. -/ - instMVars : Array MVarId - /-- Type parameter names and metavariables for each parameter. Used to seed `StructInstView.params`. -/ - params : Array (Name × Expr) + /-- The type of the structure. -/ + structType : Expr + /-- Universe levels. -/ + levels : List Level + /-- Parameters for the type. -/ + params : Array Expr -private def mkCtorHeaderAux : Nat → Expr → Expr → Array MVarId → Array (Name × Expr) → TermElabM CtorHeaderResult - | 0, type, ctorFn, instMVars, params => return { ctorFn , ctorFnType := type, instMVars, params } - | n+1, type, ctorFn, instMVars, params => do - match (← whnfForall type) with - | .forallE paramName d b c => - match c with - | .instImplicit => - let a ← mkFreshExprMVar d .synthetic - mkCtorHeaderAux n (b.instantiate1 a) (mkApp ctorFn a) (instMVars.push a.mvarId!) (params.push (paramName, a)) - | _ => - let a ← mkFreshExprMVar d - mkCtorHeaderAux n (b.instantiate1 a) (mkApp ctorFn a) instMVars (params.push (paramName, a)) - | _ => throwError "unexpected constructor type" +/-- +Elaborates the structure's flat constructor using the expected type, filling in the structure type parameters. -private partial def getForallBody : Nat → Expr → Option Expr - | i+1, .forallE _ _ b _ => getForallBody i b - | _+1, _ => none - | 0, type => type - -/-- Attempts to use the expected type to solve for structure parameters. -/ -private def propagateExpectedType (type : Expr) (numFields : Nat) (expectedType? : Option Expr) : TermElabM Unit := do - match expectedType? with - | none => return () - | some expectedType => - match getForallBody numFields type with - | none => pure () - | some typeBody => - unless typeBody.hasLooseBVars do - discard <| isDefEq expectedType typeBody - -/-- Elaborates the structure constructor using the expected type, filling in all structure parameters. -/ -private def mkCtorHeader (ctorVal : ConstructorVal) (expectedType? : Option Expr) : TermElabM CtorHeaderResult := do +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 us ← mkFreshLevelMVars ctorVal.levelParams.length - let val := Lean.mkConst ctorVal.name us - let type ← instantiateTypeLevelParams ctorVal.toConstantVal us - let r ← mkCtorHeaderAux ctorVal.numParams type val #[] #[] - propagateExpectedType r.ctorFnType ctorVal.numFields expectedType? - synthesizeAppInstMVars r.instMVars r.ctorFn - return r + let mut type ← instantiateTypeLevelParams cinfo.toConstantVal us + let mut params : Array Expr := #[] + let mut instMVars : Array MVarId := #[] + for _ in [0 : ctorVal.numParams] do + let .forallE _ d b bi := type + | throwError "unexpected constructor type" + let param ← + if bi.isInstImplicit then + let mvar ← mkFreshExprMVar d .synthetic + instMVars := instMVars.push mvar.mvarId! + pure mvar + else + mkFreshExprMVar d + params := params.push param + type := b.instantiate1 param + let structType := mkAppN (.const ctorVal.induct us) params + if let some structureType := structureType? then + discard <| isDefEq structureType structType + let val ← instantiateValueLevelParams cinfo us + let val := val.beta params + synthesizeAppInstMVars instMVars val + return { ctorFn := val, ctorFnType := type, structType, levels := us, params } -/-- Annotates an expression that it is a value for a missing field. -/ -def markDefaultMissing (e : Expr) : Expr := - mkAnnotation `structInstDefault e +/-- +Normalizes the head of the LHS of the `FieldView` in the following ways: +- Replaces numeric index field LHS's with the corresponding named field. + If this is a subobject field, continues normalizing it. +- Consumes nonterminal parent projections, e.g. `toA.x` becomes `x`. Throws an error if `A` does not have an `x` field. +- If a field name is not atomic, splits it into a multi-component LHS. -/-- If the expression has been annotated by `markDefaultMissing`, returns the unannotated expression. -/ -def defaultMissing? (e : Expr) : Option Expr := - annotation? `structInstDefault e +Normalization is not done for the entire LHS; only the head of each field LHS is normalized. -/-- Throws "failed to elaborate field" error. -/ -def throwFailedToElabField {α} (fieldName : Name) (structName : Name) (msgData : MessageData) : TermElabM α := - throwError "failed to elaborate field '{fieldName}' of '{structName}, {msgData}" +Validates that fields are indeed fields, and adds completion info. +On validation errors, errors are logged and the corresponding fields are omitted. -/-- If the struct has all-missing fields, tries to synthesize the structure using typeclass inference. -/ -def trySynthStructInstance? (s : StructInstView) (expectedType : Expr) : TermElabM (Option Expr) := do - if !s.allDefault then - return none - else - try synthInstance? expectedType catch _ => return none +Assumed invariant: parent projections and field names are disjoint sets. This is validated in the `structure` elaborator. -/-- The result of elaborating a `StructInstView` structure instance view. -/ -structure ElabStructResult where - /-- The elaborated value. -/ - val : Expr - /-- The modified `StructInstView` view after elaboration. -/ - struct : StructInstView +Resulting invariant: the field has a LHS that has one of these forms: +- `.fieldName .. :: _` +- `[.parentFieldName ..]` +-/ +private partial def normalizeField (structName : Name) (fieldView : FieldView) : MetaM FieldView := do + let env ← getEnv + match fieldView.lhs with + | .fieldIndex ref idx :: rest => + if idx == 0 then + throwErrorAt ref m!"invalid field index, index must be greater than 0" + let fieldNames := getStructureFields env structName + if idx > fieldNames.size then + throwErrorAt ref m!"invalid field index, structure '{.ofConstName structName}' has only {fieldNames.size} fields" + normalizeField structName { fieldView with lhs := .fieldName ref fieldNames[idx - 1]! :: rest } + | .fieldName ref name :: rest => + if !name.isAtomic then + let newEntries := name.components.map (FieldLHS.fieldName ref ·) + normalizeField structName { fieldView with lhs := newEntries ++ rest } + else + addCompletionInfo <| CompletionInfo.fieldId ref name (← getLCtx) structName + if let some parentName := findParentProjStruct? env structName name then + if rest.isEmpty then + return { fieldView with lhs := [.parentFieldName ref parentName name] } + else + normalizeField parentName { fieldView with lhs := rest } + else if (findField? env structName name).isSome then + return fieldView + else + throwErrorAt ref m!"'{name}' is not a field of structure '{.ofConstName structName}'" + | _ => unreachable! + +private inductive ExpandedFieldVal + | term (stx : Term) + /-- Like `stx.fieldName`, but later we will be sure to elaborate `stx` exactly once for the given `parentStructName`. + The `fvarId` will be used later when elaborating `stx`. It becomes a local decl; if it is a new fvar, an impl. detail. -/ + | proj (fvarId : FVarId) (stx : Term) (parentStructName : Name) (parentFieldName : Name) + | source (fvar : Expr) + | nested (fieldViews : Array FieldView) (sources : Array ExplicitSourceView) + +private structure ExpandedField where + ref : Syntax + name : Name + val : ExpandedFieldVal + +private def ExpandedField.isNested (f : ExpandedField) : Bool := f.val matches .nested .. + +instance : ToMessageData ExpandedFieldVal where + toMessageData + | .term stx => m!"term {stx}" + | .proj fvarId stx parentStructName _ => m!"proj {Expr.fvar fvarId} {.ofConstName parentStructName}{indentD stx}" + | .source fvar => m!"source {fvar}" + | .nested fieldViews sources => m!"nested {MessageData.joinSep (sources.map (·.stx)).toList ", "} {MessageData.joinSep (fieldViews.map (indentD <| toMessageData ·)).toList "\n"}" + +instance : ToMessageData ExpandedField where + toMessageData field := m!"field '{field.name}' is {field.val}" + +abbrev ExpandedFields := NameMap ExpandedField + +/-- +Normalizes and expands the field views. +Validates that there are no duplicate fields. +-/ +private def expandFields (structName : Name) (fieldViews : Array FieldView) (recover : Bool) : MetaM (Bool × ExpandedFields) := do + let mut fields : ExpandedFields := {} + let mut errors : Bool := false + for fieldView in fieldViews do + try + let fieldView ← normalizeField structName fieldView + match fieldView.lhs with + | .fieldName ref name :: rest => + if let some field := fields.find? name then + if rest.isEmpty || !field.isNested then + throwErrorAt ref m!"field '{name}' has already been specified" + else + -- There is a pre-existing nested field, and we are looking at a nested field. So, insert. + let .nested views' sources := field.val | unreachable! + let views' := views'.push { fieldView with lhs := rest } + fields := fields.insert name { field with val := .nested views' sources } + else if rest.isEmpty then + -- A simple field + fields := fields.insert name { ref := ref, name, val := .term fieldView.val } + else + -- A new nested field + let fieldView' := { fieldView with lhs := rest } + fields := fields.insert name { ref := ref, name, val := .nested #[fieldView'] #[] } + | [.parentFieldName ref parentStructName name] => + -- Parent field + let fvarId ← mkFreshFVarId + for parentField in getStructureFieldsFlattened (← getEnv) parentStructName false do + if fields.contains parentField then + throwErrorAt ref m!"field '{name}' from structure '{.ofConstName parentStructName}' has already been specified" + else + let val := ExpandedFieldVal.proj fvarId fieldView.val parentStructName name + fields := fields.insert parentField { ref := ref, name := parentField, val } + | _ => unreachable! + catch ex => + if recover then + logException ex + errors := true + else + throw ex + return (errors, fields) + +/-- +Adds fields from the sources, updating any nested fields. + +Rule: a missing field always comes from the first source that can provide it. +-/ +private def addSourceFields (structName : Name) (sources : Array ExplicitSourceView) (fields : ExpandedFields) : MetaM ExpandedFields := do + let mut fields := fields + let env ← getEnv + let fieldNames := getStructureFieldsFlattened env structName false + for source in sources do + let sourceFieldNames := getStructureFieldsFlattened env source.structName false + for fieldName in sourceFieldNames do + if fieldNames.contains fieldName then + match fields.find? fieldName with + | none => + -- Missing field, take it from this source + let val := ExpandedFieldVal.source source.fvar + fields := fields.insert fieldName { ref := source.stx.mkSynthetic, name := fieldName, val } + | some field@{ val := .nested subFields sources', .. } => + -- Existing nested field, add this source + let val := ExpandedFieldVal.nested subFields (sources'.push source) + fields := fields.insert fieldName { field with val } + | _ => + -- Field already exists and is known to be complete. + pure () + return fields + +private structure StructInstContext where + view : StructInstView + /-- True if the structure instance has a trailing `..`. -/ + ellipsis : Bool + structName : Name + structType : Expr + /-- Structure universe levels. -/ + levels : List Level + /-- Structure parameters. -/ + params : Array Expr + /-- The flat constructor with applied parameters. -/ + val : Expr + /-- The expanded structure instance fields, to be elaborated. -/ + fieldViews : ExpandedFields + +private structure StructInstState where + /-- The type of the flat constructor with applied parameters and applied fields. -/ + type : Expr + /-- A set of the structure name and all its parents. -/ + structNameSet : NameSet := {} + /-- The elaborated fields. -/ + fieldMap : NameMap Expr := {} + /-- The elaborated fields, in order. -/ + fields : Array Expr := #[] /-- Metavariables for instance implicit fields. These will be registered after default value propagation. -/ - instMVars : Array MVarId + instMVars : Array MVarId := #[] + /-- The let decls created when processing `ExpandedFieldVal.proj` fields. -/ + liftedFVars : Array Expr := #[] + /-- When processing `ExpandedFieldVal.proj` fields, sometimes we can re-use pre-existing fvars. -/ + liftedFVarRemap : FVarIdMap FVarId := {} + /-- Fields to synthesize using default values, if they don't get synthesized by other means. + If the boolean is `true`, then the field *must* be solved for. This is used for explicit fields. -/ + optParamFields : Array (Name × Expr × Bool) := #[] + deriving Inhabited + +/-- +Monad for elaborating the fields of structure instance notation. +-/ +private abbrev StructInstM := ReaderT StructInstContext (StateRefT StructInstState TermElabM) + +private structure SavedState where + termState : Term.SavedState + state : StructInstState + deriving Nonempty + +private def saveState : StructInstM SavedState := + return { termState := (← Term.saveState), state := (← get) } + +private def SavedState.restore (s : SavedState) : StructInstM Unit := do + s.termState.restore + set s.state + +private instance : MonadBacktrack SavedState StructInstM where + saveState := saveState + restoreState b := b.restore + +/-- +Initialize cached data. +-/ +private def initializeState : StructInstM Unit := do + let structName := (← read).structName + let resolutionOrder ← getStructureResolutionOrder structName + let structNameSet : NameSet := resolutionOrder.foldl (·.insert ·) {} + modify fun s => { s with structNameSet } + +private def withViewRef {α : Type} (x : StructInstM α) : StructInstM α := do + let ref := (← read).view.ref + withRef ref x + +/-- +If the field has already been visited by `loop` but has not been solved for yet, returns its metavariable. +-/ +private def isFieldNotSolved? (fieldName : Name) : StructInstM (Option MVarId) := do + let some val := (← get).fieldMap.find? fieldName | return none + let .mvar mvarId ← instantiateMVars val | return none + return mvarId + +/-- +Reduce projections for all structures appearing in `structNameSet`. +-/ +private def reduceFieldProjs (e : Expr) : StructInstM Expr := do + let e ← instantiateMVars e + let postVisit (e : Expr) : StructInstM TransformStep := do + if let Expr.const projName .. := e.getAppFn then + if let some projInfo ← getProjectionFnInfo? projName then + let ConstantInfo.ctorInfo cval := (← getEnv).find? projInfo.ctorName | unreachable! + if (← get).structNameSet.contains cval.induct then + let args := e.getAppArgs + if let some major := args[projInfo.numParams]? then + if major.isAppOfArity projInfo.ctorName (cval.numParams + cval.numFields) then + if let some arg := major.getAppArgs[projInfo.numParams + projInfo.i]? then + return TransformStep.visit <| mkAppN arg args[projInfo.numParams+1:] + return TransformStep.continue + Meta.transform e (post := postVisit) + +/-- +Unfolds implementation decl let vars that appear in propositions. +-/ +private def zetaDeltaImplDetailsInProps (e : Expr) : MetaM Expr := do + let unfoldPre (e : Expr) : MetaM TransformStep := do + let .fvar fvarId := e.getAppFn | return .continue + let decl ← fvarId.getDecl + if decl.isLet && decl.kind matches .implDetail then + return .visit <| (← instantiateMVars decl.value).beta e.getAppArgs + else + return .continue + let pre (e : Expr) : MetaM TransformStep := do + if ← Meta.isProp e then + let e ← transform e (pre := unfoldPre) + return .done e + else + return .continue + transform (← instantiateMVars e) (pre := pre) + +private def etaStructReduce' (e : Expr) : StructInstM Expr := do + let names := (← get).structNameSet + etaStructReduce e names.contains + +private def normalizeExpr (e : Expr) (zetaDeltaImpl : Bool := true) : StructInstM Expr := do + let e ← if zetaDeltaImpl then zetaDeltaImplDetailsInProps e else pure e + let e ← reduceFieldProjs e + etaStructReduce' e + +private def addStructFieldAux (fieldName : Name) (e : Expr) : StructInstM Unit := do + trace[Elab.struct] "setting '{fieldName}' value to{indentExpr e}" + modify fun s => { s with + type := s.type.bindingBody!.instantiateBetaRevRange 0 1 #[e] + fields := s.fields.push e + fieldMap := s.fieldMap.insert fieldName e + } + +private def addStructField (fieldView : ExpandedField) (e : Expr) : StructInstM Unit := do + let fieldName := fieldView.name + addStructFieldAux fieldName e + let projName := (← read).structName ++ fieldName + pushInfoTree <| InfoTree.node (children := {}) <| Info.ofFieldInfo { + projName, fieldName, lctx := (← getLCtx), val := e, stx := fieldView.ref + } + +private def elabStructField (_fieldName : Name) (stx : Term) (fieldType : Expr) : StructInstM Expr := do + let fieldType ← normalizeExpr fieldType + elabTermEnsuringType stx fieldType + +private def addStructFieldMVar (fieldName : Name) (ty : Expr) (kind : MetavarKind := .natural) : StructInstM Expr := do + let ty ← normalizeExpr ty + let e ← mkFreshExprMVar ty (kind := kind) + addStructFieldAux fieldName e + return e + +/-- +Instantiates default value for field `fieldName` set at structure `structName`. +The arguments for the `_default` auxiliary function are provided by `fieldMap`. +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) + +/-- +Auxiliary type for `synthDefaultFields` +-/ +private structure PendingField where + fieldName : Name + fieldType : Expr + required : Bool + deps : NameSet + val? : Option Expr + +/-- +Synthesize pending optParams. +-/ +private def synthOptParamFields : StructInstM Unit := do + let optParamFields ← modifyGet fun s => (s.optParamFields, { s with optParamFields := #[] }) + if optParamFields.isEmpty then return + /- + We try to synthesize pending mvars before trying to use default values. + This is important in examples such as + ``` + structure MyStruct where + {α : Type u} + {β : Type v} + a : α + b : β + + #check { a := 10, b := true : MyStruct } + ``` + were the `α` will remain "unknown" until the default instance for `OfNat` is used to ensure that `10` is a `Nat`. + + TODO: investigate whether this design decision may have unintended side effects or produce confusing behavior. + -/ + synthesizeSyntheticMVarsUsingDefault + + trace[Elab.struct] "field values before default value synth:{indentD <| toMessageData (← get).fieldMap.toArray}" + + -- Process default values for pending optParam fields. + let mut pendingFields : Array PendingField ← optParamFields.filterMapM fun (fieldName, fieldType, required) => do + if required || (← isFieldNotSolved? fieldName).isSome then + let (deps, val?) ← getFieldDefaultValue? fieldName + if let some val := val? then + trace[Elab.struct] "default value for {fieldName}:{indentExpr val}" + else + trace[Elab.struct] "no default value for {fieldName}" + pure <| some { fieldName, fieldType, required, deps, val? } + else + pure none + -- We then iteratively look for pending fields that do not depend on unsolved-for fields. + -- The assignments might fail (due to occurs checks or stuck metavariables), + -- so we need to keep trying until no more progress is made. + let mut pendingSet : NameSet := pendingFields.foldl (init := {}) fun set pending => set.insert pending.fieldName + while !pendingSet.isEmpty do + let selectedFields := pendingFields.filter fun pendingField => + pendingField.val?.isSome && pendingField.deps.all (fun dep => !pendingSet.contains dep) + let mut toRemove : Array Name := #[] + let mut assignErrors : Array MessageData := #[] + for selected in selectedFields do + let some selectedVal := selected.val? | unreachable! + if let some mvarId ← isFieldNotSolved? selected.fieldName then + let fieldType := selected.fieldType + let selectedType ← inferType selectedVal + if ← isDefEq fieldType selectedType then + /- + We must use `checkedAssign` here to ensure we do not create a cyclic + assignment. See #3150. + This can happen when there are holes in the the fields the default value + depends on. + Possible improvement: create a new `_` instead of returning `false` when + `checkedAssign` fails. Reason: the field will not be needed after the + other `_` are resolved by the user. + -/ + if ← MVarId.checkedAssign mvarId selectedVal then + toRemove := toRemove.push selected.fieldName + else + assignErrors := assignErrors.push m!"\ + occurs check failed, field '{selected.fieldName}' of type{indentExpr fieldType}\n\ + cannot be assigned the default value{indentExpr selectedVal}" + else + assignErrors := assignErrors.push m!"\ + default value for field '{selected.fieldName}' {← mkHasTypeButIsExpectedMsg selectedType fieldType}" + else + if selected.required then + -- Clear the value but preserve its pending status, for the "fields missing" error. + -- Rationale: this is a field that must be explicitly provided (if default values don't solve for it), + -- and *not* solved for by unification. Users expect explicit fields to be required to be provided by some explicit means. + pendingFields := pendingFields.map fun pending => + if pending.fieldName = selected.fieldName then + { pending with val? := none } + else + pending + toRemove := toRemove.push selected.fieldName + if toRemove.isEmpty then + if (← read).ellipsis then + for pendingField in pendingFields do + if let some mvarId ← isFieldNotSolved? pendingField.fieldName then + registerCustomErrorIfMVar (.mvar mvarId) (← read).view.ref m!"\ + cannot synthesize placeholder for field '{pendingField.fieldName}'" + return + let assignErrorsMsg := MessageData.joinSep (assignErrors.map (m!"\n\n" ++ ·)).toList "" + let mut requiredErrors : Array MessageData := #[] + for pendingField in pendingFields do + if (← isFieldNotSolved? pendingField.fieldName).isNone then + let e := (← get).fieldMap.find! pendingField.fieldName + requiredErrors := requiredErrors.push m!"\ + field '{pendingField.fieldName}' must be explicitly provided, its synthesized value is{indentExpr e}" + let requiredErrorsMsg := MessageData.joinSep (requiredErrors.map (m!"\n\n" ++ ·)).toList "" + let missingFields := pendingFields |>.filter (fun pending => pending.val?.isNone) + -- TODO(kmill): when fields are all stuck, report better. + -- For now, just report all pending fields in case there are no obviously missing ones. + let missingFields := if missingFields.isEmpty then pendingFields else missingFields + let missing := missingFields |>.map (s!"'{·.fieldName}'") |>.toList + let msg := m!"fields missing: {", ".intercalate missing}{assignErrorsMsg}{requiredErrorsMsg}" + if (← readThe Term.Context).errToSorry then + -- Assign all pending problems using synthetic sorries and log an error. + for pendingField in pendingFields do + if let some mvarId ← isFieldNotSolved? pendingField.fieldName then + mvarId.assign <| ← mkLabeledSorry (← mvarId.getType) (synthetic := true) (unique := true) + logError msg + return + else + throwError msg + pendingSet := pendingSet.filter (!toRemove.contains ·) + pendingFields := pendingFields.filter fun pendingField => pendingField.val?.isNone || !toRemove.contains pendingField.fieldName + +private def finalize : StructInstM Expr := withViewRef do + let val := (← read).val.beta (← get).fields + trace[Elab.struct] "constructor{indentExpr val}" + synthesizeAppInstMVars (← get).instMVars val + trace[Elab.struct] "constructor after synthesizing instMVars{indentExpr val}" + synthOptParamFields + trace[Elab.struct] "constructor after synthesizing defaults{indentExpr val}" + -- Compact the constructors: + let val ← etaStructReduce' val + if (← readThe Term.Context).inPattern then + -- In patterns, there is no multiple evaluation worry. + -- We also don't want any lingering `let`s in that case. + zetaDeltaFVars (← instantiateMVars val) ((← get).liftedFVars.map Expr.fvarId!) + else + mkLetFVars (← get).liftedFVars val + +/-- +Replace (subobject) parent projections of a `self` fvar by a constructor expression, +if all the fields for the parent are already defined. +-/ +private partial def reduceSelfProjs (self : Expr) (e : Expr) : StructInstM Expr := do + let e ← instantiateMVars e + Meta.transform (skipConstInApp := true) e (pre := replaceParentProj) +where + /-- If `e` is a subobject projection from a structure type that is in `structNameSet`, + return the name of the structure being projected to and the object being projected. -/ + parentProjInfo? (e : Expr) : StructInstM (Option (Name × Expr)) := do + let env ← getEnv + let .const c@(.str _ field) _ := e.getAppFn | return none + let some info := env.getProjectionFnInfo? c | return none + let some (.ctorInfo cVal) := env.find? info.ctorName | return none + let numArgs := e.getAppNumArgs + unless numArgs == cVal.numParams + 1 do return none + unless (← get).structNameSet.contains cVal.induct do return none + let some parentStruct := isSubobjectField? env cVal.induct (Name.mkSimple field) | return none + return (parentStruct, e.appArg!) + /-- Recursively applies `parentProjInfo?`. -/ + withoutParentProj? (e : Expr) : StructInstM (Option (Name × Expr)) := do + let some (field, e') ← parentProjInfo? e | return none + let some (_, e'') ← withoutParentProj? e.appArg! | return (field, e') + return (field, e'') + replaceParentProj (e : Expr) : StructInstM TransformStep := do + let some (parentName, x) ← withoutParentProj? e | return .continue + unless x == self do return .continue + let parentFields := getStructureFieldsFlattened (← getEnv) parentName (includeSubobjectFields := false) + let fieldMap := (← get).fieldMap + -- Unless every field is present, we cannot eliminate this expression or any subexpressions + unless parentFields.all fieldMap.contains do return .done e + let type ← whnf (← inferType e) + let .const _ us := type.getAppFn | return .done e + let params := type.getAppArgs + 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 ctorVal ← instantiateValueLevelParams cinfo us + let fieldArgs := parentFields.map fieldMap.find! + let e' := (ctorVal.beta params).beta fieldArgs + return .done e' + +private def getParentStructType? (parentStructName : Name) : StructInstM (Option (Expr × Option Name)) := do + let env ← getEnv + let structName := (← read).structName + let structType := (← read).structType + let some path := getPathToBaseStructure? env parentStructName structName | return none + withLocalDeclD `self structType fun self => do + let proj ← path.foldlM (init := self) fun e projFn => do + let ty ← whnf (← inferType e) + let .const _ us := ty.getAppFn | unreachable! + let params := ty.getAppArgs + pure <| mkApp (mkAppN (.const projFn us) params) e + let projTy ← whnf <| ← inferType proj + let projTy ← reduceSelfProjs self projTy + let projTy ← normalizeExpr projTy + if projTy.containsFVar self.fvarId! then + -- unsupported dependent type, parent depends on fields that haven't been visited yet. + trace[Elab.struct] "getParentStructType? '{parentStructName}', failed, computed type depends on {self}{indentExpr projTy}" + return none + return (projTy, path.getLast?) + +/-- +If there is a path to `parentStructName`, compute its type. Also returns the last projection to the parent. +Otherwise, create a type with fresh metavariables. +-/ +private def getParentStructType (parentStructName : Name) : StructInstM (Expr × Option Name) := do + if let some res ← getParentStructType? parentStructName then + return res + else + let c ← mkConstWithFreshMVarLevels parentStructName + let (args, _, _) ← forallMetaTelescopeReducing (← inferType c) + return (mkAppN c args, none) + +/-- +Creates projection notation for the given structure field. +-/ +private def mkProjStx (s : Syntax) (fieldName : Name) : Syntax := + mkNode ``Parser.Term.explicit + #[mkAtomFrom s "@", + mkNode ``Parser.Term.proj #[s, mkAtomFrom s ".", mkIdentFrom s fieldName]] + +private def processField (loop : StructInstM α) (field : ExpandedField) (fieldType : Expr) : StructInstM α := withRef field.ref do + let fieldType := fieldType.consumeTypeAnnotations + trace[Elab.struct] "processing field '{field.name}' of type {fieldType}{indentD (toMessageData field)}" + match field.val with + | .term val => withRef val do + trace[Elab.struct] "field.val is term {field.name}" + let e ← elabStructField field.name val fieldType + addStructField field e + loop + | .nested fields sources => + trace[Elab.struct] "field.val is nested {field.name}" + -- Nested field. Create synthetic structure instance notation with projected sources, then elaborate it like a `.term` field. + let sourceStxs : Array Term := sources.map (fun source => mkProjStx source.stx field.name) + let fieldStxs := fields.map (fun field => field.toSyntax) + let ellipsis := (← read).view.sources.implicit + let stx ← `({ $sourceStxs,* with $fieldStxs,* $[..%$ellipsis]? }) + let e ← elabStructField field.name stx fieldType + addStructField field e + loop + | .source fvar => + trace[Elab.struct] "field.val is source {field.name} from {fvar}" + let e ← mkProjection fvar field.name + let e ← ensureHasType fieldType e + addStructFieldAux field.name e + loop + | .proj fvarId val parentStructName parentFieldName => + trace[Elab.struct] "field.val is proj {field.name}" + let processProjAux (fvarId : FVarId) : StructInstM α := do + try + let e ← mkProjection (.fvar fvarId) field.name + let eType ← inferType e + unless ← isDefEq eType fieldType do + throwError m!"type of field '{field.name}' from structure '{.ofConstName parentStructName}' \ + {← mkHasTypeButIsExpectedMsg eType fieldType}" + addStructFieldAux field.name e + catch ex => + if (← readThe Term.Context).errToSorry then + let e ← exceptionToSorry ex fieldType + addStructFieldAux field.name e + else + throw ex + loop + if let some fvarId' := (← get).liftedFVarRemap.find? fvarId then + processProjAux fvarId' + else if (← getLCtx).contains fvarId then + processProjAux fvarId + else + let (parentTy, projName?) ← getParentStructType parentStructName + let parentVal ← elabTermEnsuringType val parentTy + -- Add terminfo so that the `toParent` field has some hover information. + if let some projName := projName? then + pushInfoTree <| InfoTree.node (children := {}) <| Info.ofFieldInfo { + projName, fieldName := parentFieldName, lctx := (← getLCtx), val := parentVal, stx := field.ref + } + let parentVal ← instantiateMVars parentVal + if parentVal.isFVar then + -- Reuse the fvar rather than add a new decl to the environment. + let fvarId' := parentVal.fvarId! + modify fun s => { s with liftedFVarRemap := s.liftedFVarRemap.insert fvarId fvarId' } + processProjAux fvarId' + else + let parentStructName' := parentStructName.eraseMacroScopes + let declNameStr := if parentStructName'.isStr then s!"__{parentStructName'.getString!}" else "__psrc" + let declName ← Core.mkFreshUserName (Name.mkSimple declNameStr) + let decl := LocalDecl.ldecl 0 fvarId declName parentTy parentVal false .implDetail + modify fun s => { s with liftedFVars := s.liftedFVars.push (.fvar fvarId) } + withExistingLocalDecls [decl] do processProjAux fvarId + +/-- +Handle the case when no field is given. + +These fields can still be solved for by parent instance synthesis later. +-/ +private def processNoField (loop : StructInstM α) (fieldName : Name) (binfo : BinderInfo) (fieldType : Expr) : StructInstM α := do + trace[Elab.struct] "processNoField '{fieldName}' of type {fieldType}" + if (← read).ellipsis && (← readThe Term.Context).inPattern then + -- See the note in `ElabAppArgs.processExplicitArg` + -- In ellipsis & pattern mode, do not use optParams or autoParams. + let e ← addStructFieldMVar fieldName fieldType + registerCustomErrorIfMVar e (← read).view.ref m!"don't know how to synthesize placeholder for field '{fieldName}'" + loop + else + let autoParam? := fieldType.getAutoParamTactic? + let fieldType := fieldType.consumeTypeAnnotations + if binfo.isInstImplicit then + let e ← addStructFieldMVar fieldName fieldType .synthetic + modify fun s => { s with instMVars := s.instMVars.push e.mvarId! } + loop + else if let some (.const tacticDecl ..) := autoParam? then + match evalSyntaxConstant (← getEnv) (← getOptions) tacticDecl with + | .error err => throwError err + | .ok tacticSyntax => + let stx ← `(by $tacticSyntax) + -- See comment in `Lean.Elab.Term.ElabAppArgs.processExplicitArg` about `tacticSyntax`. + -- We add info to get reliable positions for messages from evaluating the tactic script. + let info := (← getRef).getHeadInfo.nonCanonicalSynthetic + let stx := stx.raw.rewriteBottomUp (·.setInfo info) + let fieldType ← normalizeExpr fieldType + let mvar ← mkTacticMVar fieldType stx (.fieldAutoParam fieldName (← read).structName) + -- Note(kmill): We are adding terminfo to simulate a previous implementation that elaborated `tacticSyntax`. + -- This is necessary for the unused variable linter. + -- (See `processExplicitArg` for a comment about this.) + addTermInfo' stx mvar + addStructFieldAux fieldName mvar + loop + else + -- Default case: natural metavariable, register it for optParams + discard <| addStructFieldMVar fieldName fieldType + modify fun s => { s with optParamFields := s.optParamFields.push (fieldName, fieldType, binfo.isExplicit) } + loop + +private partial def loop : StructInstM Expr := withViewRef do + let type := (← get).type + trace[Elab.struct] "loop, constructor type:{indentExpr type}" + if let .forallE fieldName fieldType _ binfo := type then + if let some fieldValue := (← get).fieldMap.find? fieldName then + -- This is a field that was added by `addParentInstanceFields` + trace[Elab.struct] "field '{fieldName}' already exists, with type {fieldType}" + let fieldValueType ← inferType fieldValue + unless ← isDefEq fieldType fieldValueType do + throwError "field '{fieldName}' inferred from a parent class {← mkHasTypeButIsExpectedMsg fieldValueType fieldType}" + addStructFieldAux fieldName fieldValue + loop + else if let some field := (← read).fieldViews.find? fieldName then + processField loop field fieldType + else + processNoField loop fieldName binfo fieldType + else + finalize + +/-- +For each parent class, see if it can be used to synthesize the fields that haven't been provided. +-/ +private partial def addParentInstanceFields : StructInstM Unit := do + let env ← getEnv + let structName := (← read).structName + let fieldNames := getStructureFieldsFlattened env structName (includeSubobjectFields := false) + let fieldViews := (← read).fieldViews + if fieldNames.all fieldViews.contains then + -- Every field is accounted for already + return + + -- We look at class parents in resolution order + let parents ← getAllParentStructures structName + let classParents := parents.filter (isClass env) + if classParents.isEmpty then return + + let allowedFields := fieldNames.filter (!fieldViews.contains ·) + let mut remainingFields := allowedFields + + -- Worklist of parent/fields pairs. If fields is empty, then it will be computed later. + let mut worklist : List (Name × Array Name) := classParents |>.map (·, #[]) |>.toList + let mut deferred : List (Name × Array Name) := [] + + while !worklist.isEmpty do + let (parentName, parentFields) :: worklist' := worklist | unreachable! + worklist := worklist' + let parentFields := if parentFields.isEmpty then getStructureFieldsFlattened env parentName (includeSubobjectFields := false) else parentFields + -- We only try synthesizing if the parent contains one of the remaining fields + -- and if every parent field is an allowed field. + if remainingFields.any parentFields.contains && parentFields.all allowedFields.contains then + -- We also need to be able to compute the parent type from the structure type. + -- This may fail if there is a complicated dependence. In that case, we put the problem on the deferred list. + match ← getParentStructType? parentName with + | none => + trace[Elab.struct] "could not calculate type for parent '{.ofConstName parentName}'" + deferred := (parentName, parentFields) :: deferred + | some (parentTy, _) => + match ← trySynthInstance parentTy with + | .none => trace[Elab.struct] "failed to synthesize instance for parent {parentTy}" + | .undef => + trace[Elab.struct] "instance synthesis stuck for parent {parentTy}" + deferred := (parentName, parentFields) :: deferred + | .some inst => + -- The fields are all-or-nothing + let saved ← saveState + try + for parentField in parentFields do + let proj ← mkProjection inst parentField + let proj ← normalizeExpr proj + match (← get).fieldMap.find? parentField with + | some fieldVal => + let projType ← inferType proj + let fieldType ← inferType fieldVal + unless ← isDefEq projType fieldType do + throwError "parent field '{parentField}' {← mkHasTypeButIsExpectedMsg proj fieldType}" + unless ← isDefEq proj fieldVal do + throwError "parent field '{parentField}'{indentExpr proj}\nis not definitionally equal to overlapping field{indentExpr fieldVal}" + trace[Elab.struct] "checked field '{parentField}' from parent '{parentTy}' is definitionally equal" + | none => + modify fun s => { s with fieldMap := s.fieldMap.insert parentField proj } + trace[Elab.struct] "added field '{parentField}' from parent '{parentTy}'" + -- All the fields have been added, update the list of remaining fields. + remainingFields := remainingFields.filter (!parentFields.contains ·) + -- Move the deferred list back the front of the work list + worklist := deferred.reverseAux worklist + deferred := [] + catch ex => + restoreState saved + -- Failed, don't try this parent again. + trace[Elab.struct] "failed to use instance for {parentTy}\n{ex.toMessageData}" + +private def main : StructInstM Expr := do + initializeState + unless (← read).ellipsis && (← readThe Term.Context).inPattern do + -- Inside a pattern with ellipsis mode, users expect to match just the fields provided. + addParentInstanceFields + loop /-- Main elaborator for structure instances. -/ -private partial def elabStructInstView (s : StructInstView) (expectedType? : Option Expr) : TermElabM ElabStructResult := withRef s.ref do +private def elabStructInstView (s : StructInstView) (structName : Name) (structType? : Option Expr) : + TermElabM Expr := withRef s.ref do let env ← getEnv - let ctorVal := getStructureCtor env s.structName + let ctorVal := getStructureCtor env structName if isPrivateNameFromImportedModule env ctorVal.name then - throwError "invalid \{...} notation, constructor for `{s.structName}` is marked as private" - -- We store the parameters at the resulting `StructInstView`. We use this information during default value propagation. - let { ctorFn, ctorFnType, params, .. } ← mkCtorHeader ctorVal expectedType? - let (e, _, fields, instMVars) ← s.fields.foldlM (init := (ctorFn, ctorFnType, [], #[])) fun (e, type, fields, instMVars) field => do - match field.lhs with - | [.fieldName ref fieldName] => - let type ← whnfForall type - trace[Elab.struct] "elabStruct {field}, {type}" - match type with - | .forallE _ d b bi => - let cont (val : Expr) (field : Field) (instMVars := instMVars) : TermElabM (Expr × Expr × List Field × Array MVarId) := do - pushInfoTree <| InfoTree.node (children := {}) <| Info.ofFieldInfo { - projName := s.structName.append fieldName, fieldName, lctx := (← getLCtx), val, stx := ref } - let e := mkApp e val - let type := b.instantiate1 val - let field := { field with expr? := some val } - return (e, type, field::fields, instMVars) - match field.val with - | .term stx => cont (← elabTermEnsuringType stx d.consumeTypeAnnotations) field - | .nested s => - -- if all fields of `s` are marked as `default`, then try to synthesize instance - match (← trySynthStructInstance? s d) with - | some val => cont val { field with val := FieldVal.term (mkHole field.ref) } - | none => - let { val, struct := sNew, instMVars := instMVarsNew } ← elabStructInstView s (some d) - let val ← ensureHasType d val - cont val { field with val := FieldVal.nested sNew } (instMVars ++ instMVarsNew) - | .default => - let some fieldInfo := getFieldInfo? env s.structName fieldName - | withRef field.ref <| throwFailedToElabField fieldName s.structName m!"no such field '{fieldName}'" - match fieldInfo.autoParam? with - | some (.const tacticDecl ..) => - match evalSyntaxConstant env (← getOptions) tacticDecl with - | .error err => throwError err - | .ok tacticSyntax => - let stx ← `(by $tacticSyntax) - -- See comment in `Lean.Elab.Term.ElabAppArgs.processExplicitArg` about `tacticSyntax`. - -- We add info to get reliable positions for messages from evaluating the tactic script. - let info := field.ref.getHeadInfo.nonCanonicalSynthetic - let stx := stx.raw.rewriteBottomUp (·.setInfo info) - let type := d.consumeTypeAnnotations - let mvar ← mkTacticMVar type stx (.fieldAutoParam fieldName s.structName) - -- Note(kmill): We are adding terminfo to simulate a previous implementation that elaborated `tacticBlock`. - -- (See the aforementioned `processExplicitArg` for a comment about this.) - addTermInfo' stx mvar - cont mvar field - | _ => - if bi == .instImplicit then - let val ← withRef field.ref <| mkFreshExprMVar d .synthetic - cont val field (instMVars.push val.mvarId!) - else - let val ← withRef field.ref <| mkFreshExprMVar (some d) - cont (markDefaultMissing val) field - | _ => withRef field.ref <| throwFailedToElabField fieldName s.structName m!"unexpected constructor type{indentExpr type}" - | _ => throwErrorAt field.ref "unexpected unexpanded structure field" - return { val := e, struct := { s with fields := fields.reverse, params }, instMVars } - -namespace DefaultFields + throwError "invalid \{...} notation, constructor for '{structName}' is marked as private" + let { ctorFn, ctorFnType, structType, levels, params } ← mkCtorHeader ctorVal structType? + let (_, fields) ← expandFields structName s.fields (recover := (← read).errToSorry) + let fields ← addSourceFields structName s.sources.explicit fields + trace[Elab.struct] "expanded fields:\n{MessageData.joinSep (fields.toList.map (fun (_, field) => m!"- {MessageData.nestD (toMessageData field)}")) "\n"}" + let ellipsis := s.sources.implicit.isSome + let (val, _) ← main + |>.run { view := s, structName, structType, levels, params, fieldViews := fields, val := ctorFn, ellipsis } + |>.run { type := ctorFnType } + return val /-- -Context for default value propagation. +If `stx` is of the form `{ s₁, ..., sₙ with ... }` and `sᵢ` is not a local variable, +expands into `let __src := sᵢ; { ..., __src, ... with ... }`. +The significance of `__src` is that the variable is treated as an implementation-detail local variable, +which can be unfolded by `simp` when `zetaDelta := false`. + +Note that this one is not a `Macro` because we need to access the local context. + +Note also that having this as a separate step from main elaboration lets it postpone without re-elaborating the sources. -/ -structure Context where - /-- The current path through `.nested` subobject structures. We must search for default values overridden in derived structures. -/ - structs : Array StructInstView := #[] - /-- The collection of structures that could provide a default value. -/ - allStructNames : Array Name := #[] - /-- - Consider the following example: - ```lean - structure A where - x : Nat := 1 - - structure B extends A where - y : Nat := x + 1 - x := y + 1 - - structure C extends B where - z : Nat := 2*y - x := z + 3 - ``` - And we are trying to elaborate a structure instance for `C`. There are default values for `x` at `A`, `B`, and `C`. - We say the default value at `C` has distance 0, the one at `B` distance 1, and the one at `A` distance 2. - The field `maxDistance` specifies the maximum distance considered in a round of Default field computation. - Remark: since `C` does not set a default value of `y`, the default value at `B` is at distance 0. - - The fixpoint for setting default values works in the following way. - - Keep computing default values using `maxDistance == 0`. - - We increase `maxDistance` whenever we failed to compute a new default value in a round. - - If `maxDistance > 0`, then we interrupt a round as soon as we compute some default value. - We use depth-first search. - - We sign an error if no progress is made when `maxDistance` == structure hierarchy depth (2 in the example above). - -/ - maxDistance : Nat := 0 - -/-- -State for default value propagation --/ -structure State where - /-- Whether progress has been made so far on this round of the propagation loop. -/ - progress : Bool := false - -/-- Collects all structures that may provide default values for fields. -/ -partial def collectStructNames (struct : StructInstView) (names : Array Name) : Array Name := - let names := names.push struct.structName - struct.fields.foldl (init := names) fun names field => - match field.val with - | .nested struct => collectStructNames struct names - | _ => names - -/-- Gets the maximum nesting depth of subobjects. -/ -partial def getHierarchyDepth (struct : StructInstView) : Nat := - struct.fields.foldl (init := 0) fun max field => - match field.val with - | .nested struct => Nat.max max (getHierarchyDepth struct + 1) - | _ => max - -/-- Returns whether the field is still missing. -/ -def isDefaultMissing? [Monad m] [MonadMCtx m] (field : Field) : m Bool := do - if let some expr := field.expr? then - if let some (.mvar mvarId) := defaultMissing? expr then - unless (← mvarId.isAssigned) do - return true - return false - -/-- Returns a field that is still missing. -/ -partial def findDefaultMissing? [Monad m] [MonadMCtx m] (struct : StructInstView) : m (Option Field) := - struct.fields.findSomeM? fun field => do - match field.val with - | .nested struct => findDefaultMissing? struct - | _ => return if (← isDefaultMissing? field) then field else none - -/-- Returns all fields that are still missing. -/ -partial def allDefaultMissing [Monad m] [MonadMCtx m] (struct : StructInstView) : m (Array Field) := - go struct *> get |>.run' #[] -where - go (struct : StructInstView) : StateT (Array Field) m Unit := - for field in struct.fields do - if let .nested struct := field.val then - go struct - else if (← isDefaultMissing? field) then - modify (·.push field) - -/-- Returns the name of the field. Assumes all fields under consideration are simple and named. -/ -def getFieldName (field : Field) : Name := - match field.lhs with - | [.fieldName _ fieldName] => fieldName - | _ => unreachable! - -abbrev M := ReaderT Context (StateRefT State TermElabM) - -/-- Returns whether we should interrupt the round because we have made progress allowing nonzero depth. -/ -def isRoundDone : M Bool := do - return (← get).progress && (← read).maxDistance > 0 - -/-- Returns the `expr?` for the given field. The value may be inside a subobject. -/ -partial def getFieldValue? (struct : StructInstView) (fieldName : Name) : MetaM (Option Expr) := do - for field in struct.fields do - let fieldName' := getFieldName field - if fieldName' == fieldName then - return field.expr? - if let .nested s' := field.val then - if let some val ← getFieldValue? s' fieldName then - return val - if let some info := getFieldInfo? (← getEnv) struct.structName fieldName' then - if info.subobject?.isSome then - if let some e := field.expr? then - try - return ← mkProjection e fieldName - catch _ => - pure () - return none - -/-- Instantiates a default value from the given default value declaration, if applicable. -/ -partial def mkDefaultValue? (struct : StructInstView) (cinfo : ConstantInfo) : TermElabM (Option Expr) := - withRef struct.ref do - let us ← mkFreshLevelMVarsFor cinfo - process (← instantiateValueLevelParams cinfo us) -where - process : Expr → TermElabM (Option Expr) - | .lam n d b c => withRef struct.ref do - if c.isExplicit then - let fieldName := n - match ← getFieldValue? struct fieldName with - | none => return none - | some val => - let valType ← inferType val - if (← isDefEq valType d) then - process (b.instantiate1 val) - else - return none - else - if let some (_, param) := struct.params.find? fun (paramName, _) => paramName == n then - -- Recall that we did not use to have support for parameter propagation here. - if (← isDefEq (← inferType param) d) then - process (b.instantiate1 param) - else - return none - else - let arg ← mkFreshExprMVar d - process (b.instantiate1 arg) - | e => - let_expr id _ a := e | return some e - return some a - -/-- -Reduces a default value. It performs beta reduction and projections of the given structures to reduce them to the provided values for fields. --/ -partial def reduce (structNames : Array Name) (e : Expr) : MetaM Expr := do - match e with - | .forallE .. => - forallTelescope e fun xs b => withReduceLCtx xs do - mkForallFVars xs (← reduce structNames b) - | .lam .. | .letE .. => - lambdaLetTelescope e fun xs b => withReduceLCtx xs do - mkLambdaFVars (usedLetOnly := true) xs (← reduce structNames b) - | .proj _ i b => - match (← Meta.project? b i) with - | some r => reduce structNames r - | none => return e.updateProj! (← reduce structNames b) - | .app f .. => - -- Recall that proposition fields are theorems. Thus, we must set transparency to .all - -- to ensure they are unfolded here - match (← withTransparency .all <| reduceProjOf? e structNames.contains) with - | some r => reduce structNames r - | none => - let f := f.getAppFn - let f' ← reduce structNames f - if f'.isLambda then - let revArgs := e.getAppRevArgs - reduce structNames (f'.betaRev revArgs) - else - let args ← e.getAppArgs.mapM (reduce structNames) - return mkAppN f' args - | .mdata _ b => - let b ← reduce structNames b - if (defaultMissing? e).isSome && !b.isMVar then - return b - else - return e.updateMData! b - | .mvar mvarId => - match (← getExprMVarAssignment? mvarId) with - | some val => if val.isMVar then pure val else reduce structNames val - | none => return e - | e => return e +private def expandNonAtomicExplicitSources (stx : Syntax) : TermElabM (Option Syntax) := do + let sourcesOpt := stx[1] + if sourcesOpt.isNone then + return none + else + let sources := sourcesOpt[0] + if sources.isMissing then + throwAbortTerm + let sources := sources.getSepArgs + if (← sources.allM fun source => return (← isLocalIdent? source).isSome) then + return none + if sources.any (·.isMissing) then + throwAbortTerm + return some (← go sources.toList #[]) where /-- - Reduce the types and values of the local variables `xs` in the local context. + If the source is a local, we can use it. + *However*, we need to watch out that the local doesn't have implicit arguemnts, + since that could cause multiple evaluation. + For simplicity, we just check that the fvar isn't a forall. -/ - withReduceLCtx {α} (xs : Array Expr) (k : MetaM α) (i : Nat := 0) : MetaM α := do - if h : i < xs.size then - let fvarId := xs[i].fvarId! - let decl ← fvarId.getDecl - let type ← reduce structNames decl.type - let mut lctx ← getLCtx - if let some value := decl.value? then - let value ← reduce structNames value - lctx := lctx.modifyLocalDecl fvarId (· |>.setType type |>.setValue value) + isSuitableLocalIdent (term : Syntax) : TermElabM Bool := do + let some fvar ← isLocalIdent? term | return false + let type ← whnf (← inferType fvar) + return !type.isForall + go (sources : List Syntax) (sourcesNew : Array Syntax) : TermElabM Syntax := do + match sources with + | [] => + let sources := Syntax.mkSep sourcesNew (mkAtomFrom stx ", ") + return stx.setArg 1 (stx[1].setArg 0 sources) + | source :: sources => + if (← isSuitableLocalIdent source) then + go sources (sourcesNew.push source) else - lctx := lctx.modifyLocalDecl fvarId (· |>.setType type) - withLCtx lctx (← getLocalInstances) (withReduceLCtx xs k (i + 1)) + withFreshMacroScope do + /- + Recall that local variables starting with `__` are treated as impl detail. + See `LocalContext.lean`. + Moreover, implementation detail let-vars are unfolded by `simp` + even when `zetaDelta := false`. + Motivation: the following failure when `zetaDelta := true` + ``` + structure A where + a : Nat + structure B extends A where + b : Nat + w : a = b + def x : A where a := 37 + @[simp] theorem x_a : x.a = 37 := rfl + + def y : B := { x with b := 37, w := by simp } + ``` + -/ + let sourceNew ← `(__src) + let r ← go sources (sourcesNew.push sourceNew) + `(let __src := $source; $r) + +/-- +Uses the expected type and sources to determine the structure type name to use for the structure instance. +This function tries to postpone execution if the expected type is not available. + +If the expected type is available and it is a structure, then we use it. +Otherwise, we use the type of the first source. + +Possibly returns the expected structure type as well. +-/ +private def getStructName (expectedType? : Option Expr) (sourceView : SourcesView) : TermElabM (Name × Option Expr) := do + tryPostponeIfNoneOrMVar expectedType? + match expectedType? with + | none => useSource () + | some expectedType => + let expectedType ← whnf expectedType + match expectedType.getAppFn with + | Expr.const constName _ => + unless isStructure (← getEnv) constName do + throwError "invalid \{...} notation, structure type expected{indentExpr expectedType}" + return (constName, expectedType) + | _ => useSource () +where + useSource : Unit → TermElabM (Name × Option Expr) := fun _ => do + unless sourceView.explicit.isEmpty do + return (sourceView.explicit[0]!.structName, none) + match expectedType? with + | some expectedType => throwUnexpectedExpectedType expectedType + | none => throwUnknownExpectedType + throwUnknownExpectedType := + throwError "invalid \{...} notation, expected type is not known" + throwUnexpectedExpectedType type (kind := "expected") := do + let type ← instantiateMVars type + if type.getAppFn.isMVar then + throwUnknownExpectedType else - k - -/-- -Attempts to synthesize a default value for a missing field `fieldName` using default values from each structure in `structs`. --/ -def tryToSynthesizeDefault (structs : Array StructInstView) (allStructNames : Array Name) (maxDistance : Nat) (fieldName : Name) (mvarId : MVarId) : TermElabM Bool := - let rec loop (i : Nat) (dist : Nat) := do - if dist > maxDistance then - return false - else if h : i < structs.size then - let struct := structs[i] - match getEffectiveDefaultFnForField? (← getEnv) struct.structName fieldName with - | some defFn => - trace[Elab.struct] "default fn for '{fieldName}' is '{.ofConstName defFn}'" - let cinfo ← getConstInfo defFn - let mctx ← getMCtx - match (← mkDefaultValue? struct cinfo) with - | none => setMCtx mctx; loop (i+1) (dist+1) - | some val => - let val ← reduce allStructNames val - trace[Elab.struct] "default value for {fieldName}:{indentExpr val}" - match val.find? fun e => (defaultMissing? e).isSome with - | some _ => setMCtx mctx; loop (i+1) (dist+1) - | none => - let mvarDecl ← getMVarDecl mvarId - let val ← ensureHasType mvarDecl.type val - /- - We must use `checkedAssign` here to ensure we do not create a cyclic - assignment. See #3150. - This can happen when there are holes in the the fields the default value - depends on. - Possible improvement: create a new `_` instead of returning `false` when - `checkedAssign` fails. Reason: the field will not be needed after the - other `_` are resolved by the user. - -/ - mvarId.checkedAssign val - | _ => loop (i+1) dist - else - return false - loop 0 0 - -/-- -Performs one step of default value synthesis. --/ -partial def step (struct : StructInstView) : M Unit := - unless (← isRoundDone) do - withReader (fun ctx => { ctx with structs := ctx.structs.push struct }) do - for field in struct.fields do - match field.val with - | .nested struct => step struct - | _ => match field.expr? with - | none => unreachable! - | some expr => - match defaultMissing? expr with - | some (.mvar mvarId) => - unless (← mvarId.isAssigned) do - let ctx ← read - if (← withRef field.ref <| tryToSynthesizeDefault ctx.structs ctx.allStructNames ctx.maxDistance (getFieldName field) mvarId) then - modify fun _ => { progress := true } - | _ => pure () - -/-- -Main entry point to default value synthesis in the `M` monad. --/ -partial def propagateLoop (hierarchyDepth : Nat) (d : Nat) (struct : StructInstView) : M Unit := do - match (← findDefaultMissing? struct) with - | none => return () -- Done - | some field => - trace[Elab.struct] "propagate [{d}] [field := {field}]: {struct}" - if d > hierarchyDepth then - let missingFields := (← allDefaultMissing struct).map getFieldName - let missingFieldsWithoutDefault := - let env := (← getEnv) - let structs := (← read).allStructNames - missingFields.filter fun fieldName => structs.all fun struct => - (getEffectiveDefaultFnForField? env struct fieldName).isNone - let fieldsToReport := - if missingFieldsWithoutDefault.isEmpty then missingFields else missingFieldsWithoutDefault - throwErrorAt field.ref "fields missing: {fieldsToReport.toList.map (s!"'{·}'") |> ", ".intercalate}" - else withReader (fun ctx => { ctx with maxDistance := d }) do - modify fun _ => { progress := false } - step struct - if (← get).progress then - propagateLoop hierarchyDepth 0 struct - else - propagateLoop hierarchyDepth (d+1) struct - -/-- -Synthesizes default values for all missing fields, if possible. --/ -def propagate (struct : StructInstView) : TermElabM Unit := - let hierarchyDepth := getHierarchyDepth struct - let structNames := collectStructNames struct #[] - propagateLoop hierarchyDepth 0 struct { allStructNames := structNames } |>.run' {} - -end DefaultFields - -/-- -Main entry point to elaborator for structure instance notation, unless the structure instance is a modifyOp. --/ -private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (sources : SourcesView) : TermElabM Expr := do - let structName ← getStructName expectedType? sources - let struct ← liftMacroM <| mkStructView stx structName sources - let struct ← expandStruct struct - trace[Elab.struct] "{struct}" - /- We try to synthesize pending problems with `withSynthesize` combinator before trying to use default values. - This is important in examples such as - ``` - structure MyStruct where - {α : Type u} - {β : Type v} - a : α - b : β - - #check { a := 10, b := true : MyStruct } - ``` - were the `α` will remain "unknown" until the default instance for `OfNat` is used to ensure that `10` is a `Nat`. - - TODO: investigate whether this design decision may have unintended side effects or produce confusing behavior. - -/ - let { val := r, struct, instMVars } ← withSynthesize (postpone := .yes) <| elabStructInstView struct expectedType? - trace[Elab.struct] "before propagate {r}" - DefaultFields.propagate struct - synthesizeAppInstMVars instMVars r - return r + throwError "invalid \{...} notation, {kind} type is not of the form (C ...){indentExpr type}" @[builtin_term_elab structInst] def elabStructInst : TermElab := fun stx expectedType? => do match (← expandNonAtomicExplicitSources stx) with @@ -1211,11 +1317,14 @@ private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (sour | none => let sourcesView ← getStructSources stx if let some modifyOp ← isModifyOp? stx then - if sourcesView.explicit.isEmpty then - throwError "invalid \{...} notation, explicit source is required when using '[] := '" - elabModifyOp stx modifyOp sourcesView.explicit expectedType? + elabModifyOp stx modifyOp sourcesView expectedType? else - elabStructInstAux stx expectedType? sourcesView + let (structName, structType?) ← getStructName expectedType? sourcesView + let struct ← liftMacroM <| mkStructView stx sourcesView + trace[Elab.struct] "StructInstView:{indentD (toMessageData struct)}" + let r ← withSynthesize (postpone := .yes) <| elabStructInstView struct structName structType? + trace[Elab.struct] "result:{indentExpr r}" + return r builtin_initialize registerTraceClass `Elab.struct diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 885699bbfb..1e04b4c59a 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -510,46 +510,6 @@ private def reduceFieldProjs (e : Expr) (zetaDelta := true) : StructElabM Expr : return TransformStep.continue Meta.transform e (post := postVisit) -/-- Checks if the expression is of the form `S.mk x.1 ... x.n` with `n` nonzero -and `S.mk` a structure constructor with `S` one of the recorded structure parents. -Returns `x`. -Each projection `x.i` can be either a native projection or from a projection function. -/ -private def etaStruct? (e : Expr) : StructElabM (Option Expr) := do - let .const f _ := e.getAppFn | return none - let some (ConstantInfo.ctorInfo fVal) := (← getEnv).find? f | return none - unless (← findParentFieldInfo? fVal.induct).isSome do return none - unless 0 < fVal.numFields && e.getAppNumArgs == fVal.numParams + fVal.numFields do return none - let args := e.getAppArgs - let some (S0, i0, x) ← getProjectedExpr args[fVal.numParams]! | return none - unless S0 == fVal.induct && i0 == 0 do return none - for i in [1 : fVal.numFields] do - let arg := args[fVal.numParams + i]! - let some (S', i', x') ← getProjectedExpr arg | return none - unless S' == fVal.induct && i' == i && x' == x do return none - return x -where - /-- Given an expression that's either a native projection or a registered projection - function, gives (1) the name of the structure type, (2) the index of the projection, and - (3) the object being projected. -/ - getProjectedExpr (e : Expr) : MetaM (Option (Name × Nat × Expr)) := do - if let .proj S i x := e then - return (S, i, x) - if let .const fn _ := e.getAppFn then - if let some info ← getProjectionFnInfo? fn then - if e.getAppNumArgs == info.numParams + 1 then - if let some (ConstantInfo.ctorInfo fVal) := (← getEnv).find? info.ctorName then - return (fVal.induct, info.i, e.appArg!) - return none - -/-- Runs `etaStruct?` over the whole expression. -/ -private def etaStructReduce (e : Expr) : StructElabM Expr := do - let e ← instantiateMVars e - Meta.transform e (post := fun e => do - if let some e ← etaStruct? e then - return .done e - else - return .continue) - /-- Puts an expression into "field normal form". - All projections of constructors for parent structures are reduced. @@ -557,7 +517,8 @@ Puts an expression into "field normal form". - Constructors of parent structures are eta reduced. -/ private def fieldNormalizeExpr (e : Expr) (zetaDelta : Bool := true) : StructElabM Expr := do - etaStructReduce <| ← reduceFieldProjs e (zetaDelta := zetaDelta) + let ancestors := (← get).ancestorFieldIdx + etaStructReduce (p := ancestors.contains) <| ← reduceFieldProjs e (zetaDelta := zetaDelta) private def fieldFromMsg (info : StructFieldInfo) : MessageData := if let some sourceStructName := info.sourceStructNames.head? then @@ -1150,11 +1111,9 @@ Assumes the inductive type has already been added to the environment. Note: we can't generally use optParams here since the default values might depend on previous ones. We include autoParams however. -/ -private def mkFlatCtorExpr (levelParams : List Name) (params : Array Expr) (structName : Name) (replaceIndFVars : Expr → MetaM Expr) : +private def mkFlatCtorExpr (levelParams : List Name) (params : Array Expr) (ctor : ConstructorVal) (replaceIndFVars : Expr → MetaM Expr) : StructElabM Expr := do - let env ← getEnv -- build the constructor application using the fields in the local context - let ctor := getStructureCtor env structName let mut val := mkAppN (mkConst ctor.name (levelParams.map mkLevelParam)) params let fieldInfos := (← get).fields for fieldInfo in fieldInfos do @@ -1173,17 +1132,20 @@ private def mkFlatCtorExpr (levelParams : List Name) (params : Array Expr) (stru | _ => pure decl.type let type ← zetaDeltaFVars (← instantiateMVars type) parentFVars let type ← replaceIndFVars type - return .lam decl.userName type (val.abstract #[fieldInfo.fvar]) decl.binderInfo + return .lam decl.userName.eraseMacroScopes type (val.abstract #[fieldInfo.fvar]) decl.binderInfo val ← mkLambdaFVars params val val ← replaceIndFVars val fieldNormalizeExpr val private partial def mkFlatCtor (levelParams : List Name) (params : Array Expr) (structName : Name) (replaceIndFVars : Expr → MetaM Expr) : StructElabM Unit := do - let val ← mkFlatCtorExpr levelParams params structName replaceIndFVars + let env ← getEnv + let ctor := getStructureCtor env structName + let val ← mkFlatCtorExpr levelParams params ctor replaceIndFVars withLCtx {} {} do trace[Elab.structure] "created flat constructor:{indentExpr val}" unless val.hasSyntheticSorry do - let flatCtorName := mkFlatCtorOfStructName structName + -- Note: flatCtorName will be private if the constructor is private + let flatCtorName := mkFlatCtorOfStructCtorName ctor.name let valType ← replaceIndFVars (← instantiateMVars (← inferType val)) let valType := valType.inferImplicit params.size true addDecl <| Declaration.defnDecl (← mkDefinitionValInferrringUnsafe flatCtorName levelParams valType val .abbrev) @@ -1393,8 +1355,8 @@ private def mkRemainingProjections (levelParams : List Name) (params : Array Exp -- No need to zeta delta reduce; `fvarToConst` has replaced such fvars. let val ← fieldNormalizeExpr val (zetaDelta := false) fvarToConst := fvarToConst.insert field.fvar val - -- TODO(kmill): if it is a direct parent, add the coercion function the environment and use that instead of `val`, - -- and evaluate the difference. + -- TODO(kmill): if it is a direct parent, try adding the coercion function from the environment and use that instead of `val`. + -- (This should be evaluated to see if it is a good idea.) else throwError m!"(mkRemainingProjections internal error) {field.name} has no value" @@ -1465,30 +1427,31 @@ def elabStructureCommand : InductiveElabDescr where collectUsedFVars := collectUsedFVars lctx localInsts fieldInfos checkUniverses := fun _ u => withLCtx lctx localInsts do checkResultingUniversesForFields fieldInfos u finalizeTermElab := withLCtx lctx localInsts do checkDefaults fieldInfos - prefinalize := fun _ _ _ => do + prefinalize := fun levelParams params replaceIndFVars => do withLCtx lctx localInsts do addProjections r fieldInfos registerStructure view.declName fieldInfos + runStructElabM (init := state) do + mkFlatCtor levelParams params view.declName replaceIndFVars + addDefaults levelParams params replaceIndFVars + let parentInfos ← withLCtx lctx localInsts <| runStructElabM (init := state) do + mkRemainingProjections levelParams params view + setStructureParents view.declName parentInfos withSaveInfoContext do -- save new env for field in view.fields do -- may not exist if overriding inherited field if (← getEnv).contains field.declName then Term.addTermInfo' field.ref (← mkConstWithLevelParams field.declName) (isBinder := true) - finalize := fun levelParams params replaceIndFVars => do - let parentInfos ← runStructElabM (init := state) <| withLCtx lctx localInsts <| mkRemainingProjections levelParams params view - withSaveInfoContext do -- Add terminfo for parents now that all parent projections exist. for parent in parents do if parent.addTermInfo then Term.addTermInfo' parent.ref (← mkConstWithLevelParams parent.declName) (isBinder := true) - setStructureParents view.declName parentInfos checkResolutionOrder view.declName - if view.isClass then - addParentInstances parentInfos - - runStructElabM (init := state) <| withLCtx lctx localInsts do - mkFlatCtor levelParams params view.declName replaceIndFVars - addDefaults levelParams params replaceIndFVars + return { + finalize := do + if view.isClass then + addParentInstances parentInfos + } } } diff --git a/src/Lean/Elab/Tactic/Omega/Core.lean b/src/Lean/Elab/Tactic/Omega/Core.lean index 59feee15ee..ea45d5828d 100644 --- a/src/Lean/Elab/Tactic/Omega/Core.lean +++ b/src/Lean/Elab/Tactic/Omega/Core.lean @@ -139,12 +139,14 @@ instance : ToString Fact where /-- `tidy`, implemented on `Fact`. -/ def tidy (f : Fact) : Fact := match f.justification.tidy? with - | some ⟨_, _, justification⟩ => { justification } + | some ⟨constraint, coeffs, justification⟩ => { coeffs, constraint, justification } | none => f /-- `combo`, implemented on `Fact`. -/ def combo (a : Int) (f : Fact) (b : Int) (g : Fact) : Fact := - { justification := .combo a f.justification b g.justification } + { coeffs := .combo a f.coeffs b g.coeffs + constraint := .combo a f.constraint b g.constraint + justification := .combo a f.justification b g.justification } end Fact diff --git a/src/Lean/Meta/Structure.lean b/src/Lean/Meta/Structure.lean index fe1267e04f..348ffb785e 100644 --- a/src/Lean/Meta/Structure.lean +++ b/src/Lean/Meta/Structure.lean @@ -109,4 +109,69 @@ def mkProjections (n : Name) (projDecls : Array StructProjDecl) (instImplicit : let proj := mkApp (mkAppN (.const projName lvls) params) self ctorType := ctorType.bindingBody!.instantiate1 proj +/-- +Checks if the expression is of the form `S.mk x.1 ... x.n` with `n` nonzero +and `S.mk` a structure constructor with `S` one of the recorded structure parents. +Returns `x`. +Each projection `x.i` can be either a native projection or from a projection function. +-/ +def etaStruct? (e : Expr) (p : Name → Bool) : MetaM (Option Expr) := do + let .const ctor _ := e.getAppFn | return none + let some (ConstantInfo.ctorInfo fVal) := (← getEnv).find? ctor | return none + unless p fVal.induct do return none + unless 0 < fVal.numFields && e.getAppNumArgs == fVal.numParams + fVal.numFields do return none + let args := e.getAppArgs + let params := args.extract 0 fVal.numParams + let some x ← getProjectedExpr ctor fVal.induct params 0 args[fVal.numParams]! none | return none + for i in [1 : fVal.numFields] do + let arg := args[fVal.numParams + i]! + let some x' ← getProjectedExpr ctor fVal.induct params i arg x | return none + unless x' == x do return none + return x +where + sameParams (params1 params2 : Array Expr) : MetaM Bool := withNewMCtxDepth do + if params1.size == params2.size then + for p1 in params1, p2 in params2 do + unless ← isDefEqGuarded p1 p2 do + return false + return true + else + return false + /-- + Given an expression `e` that's either a native projection or a registered projection + function, gives the object being projected. + Checks that the parameters are defeq to `params`, that the projection index is equal to `idx`, + and, if `x?` is provided, that the object being projected is equal to it. + -/ + getProjectedExpr (ctor induct : Name) (params : Array Expr) (idx : Nat) (e : Expr) (x? : Option Expr) : MetaM (Option Expr) := do + if let .proj S i x := e then + if i == idx && induct == S && (x? |>.map (· == x) |>.getD true) then + let ety ← whnf (← inferType e) + let params' := ety.getAppArgs + if ← sameParams params params' then + return x + return none + if let .const fn _ := e.getAppFn then + if let some info ← getProjectionFnInfo? fn then + if info.ctorName == ctor && info.i == idx && e.getAppNumArgs == info.numParams + 1 then + let x := e.appArg! + if (x? |>.map (· == x) |>.getD true) then + let params' := e.appFn!.getAppArgs + if ← sameParams params params' then + return e.appArg! + return none + +/-- +Eta reduces all structures satisfying `p` in the whole expression. + +See `etaStruct?` for reducing single expressions. +-/ +def etaStructReduce (e : Expr) (p : Name → Bool) : MetaM Expr := do + let e ← instantiateMVars e + Meta.transform e (post := fun e => do + if let some e ← etaStruct? e p then + return .done e + else + return .continue) + end Lean.Meta diff --git a/src/Lean/Structure.lean b/src/Lean/Structure.lean index 86a06ef5ea..350e9e671a 100644 --- a/src/Lean/Structure.lean +++ b/src/Lean/Structure.lean @@ -6,6 +6,7 @@ Authors: Leonardo de Moura Helper functions for retrieving structure information. -/ prelude +import Init.Control.Option import Lean.Environment import Lean.ProjFns import Lean.Exception @@ -98,7 +99,7 @@ structure StructureDescr where deriving Inhabited /-- -Declare a new structure to the elaborator. +Declares a new structure to the elaborator. Every structure created by `structure` or `class` has such an entry. This should be followed up with `setStructureParents` and `setStructureResolutionOrder`. -/ @@ -110,7 +111,7 @@ def registerStructure (env : Environment) (e : StructureDescr) : Environment := } /-- -Set parent projection info for a structure defined in the current module. +Sets parent projection info for a structure defined in the current module. Throws an error if the structure has not already been registered with `Lean.registerStructure`. -/ def setStructureParents [Monad m] [MonadEnv m] [MonadError m] (structName : Name) (parentInfo : Array StructureParentInfo) : m Unit := do @@ -154,26 +155,29 @@ def getStructureCtor (env : Environment) (constName : Name) : ConstructorVal := def getStructureFields (env : Environment) (structName : Name) : Array Name := (getStructureInfo env structName).fieldNames -/-- Get the `StructureFieldInfo` for the given direct field of the structure. -/ +/-- Gets the `StructureFieldInfo` for the given direct field of the structure. -/ def getFieldInfo? (env : Environment) (structName : Name) (fieldName : Name) : Option StructureFieldInfo := if let some info := getStructureInfo? env structName then info.fieldInfo.binSearch { fieldName := fieldName, projFn := default, subobject? := none, binderInfo := default } StructureFieldInfo.lt else none -/-- If `fieldName` is a subobject (that it, if it is an embedded parent structure), then returns the name of that parent structure. -/ +/-- +If `fieldName` is a subobject (that it, if it is an embedded parent structure), +then returns the name of that parent structure. +-/ def isSubobjectField? (env : Environment) (structName : Name) (fieldName : Name) : Option Name := if let some fieldInfo := getFieldInfo? env structName fieldName then fieldInfo.subobject? else none -/-- Get information for all the parents that appear in the `extends` clause. -/ +/-- Gets information for all the parents that appear in the `extends` clause. -/ def getStructureParentInfo (env : Environment) (structName : Name) : Array StructureParentInfo := (getStructureInfo env structName).parentInfo /-- -Return the parent structures that are embedded in the structure. +Returns the parent structures that are embedded in the structure. This is the array of all results from `Lean.isSubobjectField?` in order. Note: this is *not* a subset of the parents from `getStructureParentInfo`. @@ -184,14 +188,37 @@ def getStructureSubobjects (env : Environment) (structName : Name) : Array Name (getStructureFields env structName).filterMap (isSubobjectField? env structName) /-- -Return the name of the structure that contains the field relative to structure `structName`. +Returns the name of the structure that contains the field relative to structure `structName`. If `structName` contains the field itself, returns that, -and otherwise recursively looks into parents that are subobjects. -/ +and otherwise recursively looks into parents that are subobjects. +-/ partial def findField? (env : Environment) (structName : Name) (fieldName : Name) : Option Name := if (getStructureFields env structName).contains fieldName then some structName else - getStructureSubobjects env structName |>.findSome? fun parentStructName => findField? env parentStructName fieldName + getStructureSubobjects env structName |>.findSome? (findField? env · fieldName) + +/-- +Given a structure `structName` and a parent projection name `projName` (e.g. `toParentStructName`), +returns the corresponding parent structure name. +The parent projection name is a single-component name. + +Note: this relies on the fact that projection names are checked to be consistent across all parents. +-/ +partial def findParentProjStruct? (env : Environment) (structName : Name) (projName : Name) : Option Name := + go structName |>.run' {} +where + -- Use a cache to navigate the DAG in polynomial time + go (structName : Name) : StateM NameSet (Option Name) := do + if (← get).contains structName then + return none + else + let parentInfos := getStructureParentInfo env structName + if let some parentInfo := parentInfos.find? (projName.isSuffixOf ·.projFn) then + return some parentInfo.structName + else + modify fun s => s.insert structName + parentInfos.findSomeM? (go ·.structName) /-- Gets the name for a structure constructor where the fields have been fully flattened. @@ -204,8 +231,8 @@ The body of the flat constructor has the following properties (recursively): - for subobject fields, the value is the unfolded flat constructor for that field - for standard fields, the value is one of the flat constructor parameters -/ -def mkFlatCtorOfStructName (structName : Name) : Name := - structName ++ `_flat_ctor +def mkFlatCtorOfStructCtorName (structCtorName : Name) : Name := + structCtorName ++ `_flat_ctor private partial def getStructureFieldsFlattenedAux (env : Environment) (structName : Name) (fullNames : Array Name) (includeSubobjectFields : Bool) : Array Name := (getStructureFields env structName).foldl (init := fullNames) fun fullNames fieldName => @@ -302,30 +329,27 @@ The effective autoParams are collected in the flat constructor. def getAutoParamFnForField? (env : Environment) (structName : Name) (fieldName : Name) : Option Name := getFnForFieldUsing? mkAutoParamFnOfProjFn env structName fieldName -partial def getPathToBaseStructureAux (env : Environment) (baseStructName : Name) (structName : Name) (path : List Name) : Option (List Name) := - if baseStructName == structName then - some path.reverse - else - if let some info := getStructureInfo? env structName then - -- Prefer subobject projections - (info.fieldInfo.findSome? fun field => - match field.subobject? with - | none => none - | some parentStructName => getPathToBaseStructureAux env baseStructName parentStructName (field.projFn :: path)) - -- Otherwise, consider other parents - <|> info.parentInfo.findSome? fun parent => - if parent.subobject then - none - else - getPathToBaseStructureAux env baseStructName parent.structName (parent.projFn :: path) - else none - /-- -If `baseStructName` is an ancestor structure for `structName`, then return a sequence of projection functions +If `baseStructName` is an ancestor structure for `structName`, then returns a sequence of projection functions to go from `structName` to `baseStructName`. Returns `[]` if `baseStructName == structName`. -/ -def getPathToBaseStructure? (env : Environment) (baseStructName : Name) (structName : Name) : Option (List Name) := - getPathToBaseStructureAux env baseStructName structName [] +partial def getPathToBaseStructure? (env : Environment) (baseStructName : Name) (structName : Name) : Option (List Name) := + OptionT.run (go structName []) |>.run' {} +where + go (structName : Name) (path : List Name) : OptionT (StateM NameSet) (List Name) := do + if baseStructName == structName then + return path.reverse + else + guard <| !(← get).contains structName + modify fun s => s.insert structName + let some info := getStructureInfo? env structName | failure + -- Prefer subobject projections + (info.fieldInfo.firstM fun field => do + let some parentStructName := field.subobject? | failure + go parentStructName (field.projFn :: path)) + -- Otherwise, consider other parents + <|> info.parentInfo.firstM fun parent => do + go parent.structName (parent.projFn :: path) /-- Returns true iff `constName` is a non-recursive inductive datatype that has only one constructor and no indices. @@ -348,7 +372,7 @@ def getStructureLikeCtor? (env : Environment) (constName : Name) : Option Constr | _ => panic! "ill-formed environment" | _ => none -/-- Return number of fields for a structure-like type -/ +/-- Returns the number of fields for a structure-like type -/ def getStructureLikeNumFields (env : Environment) (constName : Name) : Nat := match env.find? constName with | some (.inductInfo { isRec := false, ctors := [ctor], numIndices := 0, .. }) => diff --git a/src/lake/Lake/Load/Toml.lean b/src/lake/Lake/Load/Toml.lean index c0e803e81a..d5897a609a 100644 --- a/src/lake/Lake/Load/Toml.lean +++ b/src/lake/Lake/Load/Toml.lean @@ -430,6 +430,7 @@ def loadTomlConfig (cfg: LoadConfig) : LogIO Package := do let defaultTargets := defaultTargets.map stringToLegalOrSimpleName let depConfigs ← table.tryDecodeD `require #[] return { + name := name dir := cfg.pkgDir relDir := cfg.relPkgDir relConfigFile := cfg.relConfigFile diff --git a/tests/lean/autoIssue.lean b/tests/lean/autoIssue.lean index a400028baa..90fbe216f7 100644 --- a/tests/lean/autoIssue.lean +++ b/tests/lean/autoIssue.lean @@ -50,7 +50,7 @@ def tst : MetaM Unit := example (z : A) : z.x = 1 := by match z with - | { a' := h } => trace_state; exact h + | { a' := h, .. } => trace_state; exact h example (z : A) : z.x = 1 := by match z with diff --git a/tests/lean/autoIssue.lean.expected.out b/tests/lean/autoIssue.lean.expected.out index 88a26e331b..5d2608f067 100644 --- a/tests/lean/autoIssue.lean.expected.out +++ b/tests/lean/autoIssue.lean.expected.out @@ -16,7 +16,7 @@ a' : x = 1 ⊢ { x := x, a' := a' }.x = 1 case mk x y : Nat -⊢ { x := x, y := y } = { x := { x := x, y := y }.x, y := { x := x, y := y }.y } +⊢ { x := x, y := y } = { x := x, y := y } a.1 = 1 z : A x✝ : Nat diff --git a/tests/lean/diamond2.lean b/tests/lean/diamond2.lean index 42cbf3ac98..956f931481 100644 --- a/tests/lean/diamond2.lean +++ b/tests/lean/diamond2.lean @@ -14,7 +14,8 @@ structure Foo1 (α : Type) extends Bar (α → α), Baz α #check Foo1.mk def f1 (x : Nat) : Foo1 Nat := - { a := id + { β := _ + a := id x := (· + ·) b := fun _ => "" } @@ -29,7 +30,8 @@ structure Foo2 (α : Type) extends Bar (α → α), Boo2 α #check Foo2.mk def f2 (v : Nat) : Foo2 Nat := - { a := id + { β := _ + a := id x := (· + ·) b := fun _ => "" x1 := 1 diff --git a/tests/lean/mkProjStx.lean b/tests/lean/mkProjStx.lean deleted file mode 100644 index f131073c3a..0000000000 --- a/tests/lean/mkProjStx.lean +++ /dev/null @@ -1,25 +0,0 @@ -import Lean - -structure A where - x : Nat := 0 - -structure B extends A where - y : Nat := 0 - -structure C extends B where - z : Nat := 0 - -def c : C := {} - -open Lean -open Lean.Elab - -def tst (varName structName fieldName : Name) : TermElabM Unit := do - let c := mkIdent varName - let some p ← Lean.Elab.Term.StructInst.mkProjStx? c structName fieldName | throwError "failed" - let p ← Term.elabTerm p none - logInfo s!"{p}" - -#eval tst `c `C `x -#eval tst `c `C `y -#eval tst `c `C `z diff --git a/tests/lean/mkProjStx.lean.expected.out b/tests/lean/mkProjStx.lean.expected.out deleted file mode 100644 index 5fdd564176..0000000000 --- a/tests/lean/mkProjStx.lean.expected.out +++ /dev/null @@ -1,3 +0,0 @@ -A.x (B.toA (C.toB c)) -B.y (C.toB c) -C.z c diff --git a/tests/lean/run/1986.lean b/tests/lean/run/1986.lean index 821b3d75ac..6923b53d08 100644 --- a/tests/lean/run/1986.lean +++ b/tests/lean/run/1986.lean @@ -145,11 +145,13 @@ instance PartialOrder {ι : Type u} {α : ι → Type v} [∀ i, PartialOrder ( le_antisymm := sorry } instance semilatticeSup [∀ i, SemilatticeSup (α' i)] : SemilatticeSup (∀ i, α' i) where + sup x y i := x i ⊔ y i le_sup_left _ _ _ := SemilatticeSup.le_sup_left _ _ le_sup_right _ _ _ := SemilatticeSup.le_sup_right _ _ sup_le _ _ _ ac bc i := SemilatticeSup.sup_le _ _ _ (ac i) (bc i) instance semilatticeInf [∀ i, SemilatticeInf (α' i)] : SemilatticeInf (∀ i, α' i) where + inf x y i := x i ⊓ y i inf_le_left _ _ _ := SemilatticeInf.inf_le_left _ _ inf_le_right _ _ _ := SemilatticeInf.inf_le_right _ _ le_inf _ _ _ ac bc i := SemilatticeInf.le_inf _ _ _ (ac i) (bc i) diff --git a/tests/lean/run/3150.lean b/tests/lean/run/3150.lean index 4bb5f22555..d4f95fd943 100644 --- a/tests/lean/run/3150.lean +++ b/tests/lean/run/3150.lean @@ -15,8 +15,23 @@ structure Subalgebra [OneHom R A] : Type extends Subone A where algebraMap_mem : ∀ r : R, mem (OneHom.toFun r) one_mem := OneHom.map_one (R := R) (A := A) ▸ algebraMap_mem One.one +set_option pp.mvars false /-- -error: fields missing: 'one_mem' +error: don't know how to synthesize placeholder +context: +R A : Type +inst✝² : One R +inst✝¹ : One A +inst✝ : OneHom R A +⊢ ∀ (r : R), ?_ R A _example (OneHom.toFun r) +--- +error: don't know how to synthesize placeholder +context: +R A : Type +inst✝² : One R +inst✝¹ : One A +inst✝ : OneHom R A +⊢ A → Prop -/ #guard_msgs in example [OneHom R A] : Subalgebra R A where diff --git a/tests/lean/run/3807.lean b/tests/lean/run/3807.lean index 0febd7b3ba..16da556a15 100644 --- a/tests/lean/run/3807.lean +++ b/tests/lean/run/3807.lean @@ -522,9 +522,11 @@ namespace Pi variable {ι : Type _} {α' : ι → Type _} instance instOrderTop [∀ i, LE (α' i)] [∀ i, OrderTop (α' i)] : OrderTop (∀ i, α' i) where + top := fun _ => ⊤ le_top _ := fun _ => le_top instance instOrderBot [∀ i, LE (α' i)] [∀ i, OrderBot (α' i)] : OrderBot (∀ i, α' i) where + bot := fun _ => ⊥ bot_le _ := fun _ => bot_le end Pi @@ -2519,7 +2521,7 @@ variable {L : Type _} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E (f : L →ₐ[F] K) -- This only required 16,000 heartbeats prior to #3807, and now takes ~210,000. -set_option maxHeartbeats 20000 +set_option maxHeartbeats 16000 theorem exists_algHom_adjoin_of_splits''' : ∃ φ : adjoin L S →ₐ[F] K, φ.comp (IsScalarTower.toAlgHom F L _) = f := by let L' := (IsScalarTower.toAlgHom F L E).fieldRange @@ -2531,7 +2533,12 @@ theorem exists_algHom_adjoin_of_splits''' : · simp only [← SetLike.coe_subset_coe, coe_restrictScalars, adjoin_subset_adjoin_iff] exact ⟨subset_adjoin_of_subset_left S (F := L'.toSubfield) le_rfl, subset_adjoin _ _⟩ · ext x - exact (congrFun (congrArg (fun g : L' →ₐ[F] K => (g : L' → K)) hφ) _).trans (congrArg f <| AlgEquiv.symm_apply_apply _ _) + exact + Eq.trans + (congrFun (congrArg (fun g : L' →ₐ[F] K => (g : L' → K)) hφ) + (DFunLike.coe (AlgEquiv.ofInjectiveField _) x)) + (congrArg f + (AlgEquiv.symm_apply_apply (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)) x)) end IntermediateField diff --git a/tests/lean/run/4534.lean b/tests/lean/run/4534.lean index 678a456f58..62632e2345 100644 --- a/tests/lean/run/4534.lean +++ b/tests/lean/run/4534.lean @@ -6,6 +6,8 @@ class MyClass (α : Type u) extends LE α where sup_of_le_left : ∀ a b : α, b ≤ a → sup a b = a instance : MyClass Prop where + le p q := p → q + sup p q := p ∨ q le_refl _ := id sup_of_le_left _ _ h := propext ⟨Or.rec id h, Or.inl⟩ diff --git a/tests/lean/run/461b.lean b/tests/lean/run/461b.lean index cd35443892..a6353cf3db 100644 --- a/tests/lean/run/461b.lean +++ b/tests/lean/run/461b.lean @@ -10,5 +10,10 @@ structure BarS extends FooS where def f (x : Nat) : BarS := { x, y := x, h' := rfl } +/-- error: cannot synthesize placeholder for field 'h' -/ +#guard_msgs in +example (x : Nat) : BarS := + { x, h' := rfl, .. } + def f1 (x : Nat) : BarS := - { x, h' := rfl } + { x, h' := rfl, y := _ } diff --git a/tests/lean/run/5406.lean b/tests/lean/run/5406.lean index 05dbf65804..dac6d9bf27 100644 --- a/tests/lean/run/5406.lean +++ b/tests/lean/run/5406.lean @@ -6,16 +6,17 @@ This is to fix a bug where structure instance notation was not working when ther /-! Motivating issue from https://github.com/leanprover/lean4/issues/5406 -The `example` had an elaboration error because the structure instance was expanding to `{b := m.b}`. -Now it expands to `{b := @m.b}`. +The `example` had an elaboration error because the structure instance was expanding to `{b := m.b, x := 1}`. +Now it expands to `{b := @m.b, x := 1}`. -/ structure Methods where b : Nat → (opt : Nat := 42) → Nat + x : Nat -example (m : Methods) : Methods := { m with } +example (m : Methods) : Methods := { m with x := 1 } -/-- info: fun m => { b := @Methods.b m } : Methods → Methods -/ -#guard_msgs in #check fun (m : Methods) => { m with } +/-- info: fun m => { b := @Methods.b m, x := 1 } : Methods → Methods -/ +#guard_msgs in #check fun (m : Methods) => { m with x := 1 } /-! @@ -54,6 +55,7 @@ We need this so that structure instances work properly. class C (α : Type) [Inhabited α] where f (x : α := default) : α + x : Nat /-- info: fun inst => C.f : C Nat → Nat -/ #guard_msgs in #check fun (inst : C Nat) => inst.f @@ -64,8 +66,8 @@ class C (α : Type) [Inhabited α] where /-- info: fun inst => @C.f Nat instInhabitedNat inst : C Nat → optParam Nat default → Nat -/ #guard_msgs in #check fun (inst : C Nat) => @C.f _ _ inst -/-- info: fun inst => { f := @C.f Nat instInhabitedNat inst } : C Nat → C Nat -/ -#guard_msgs in #check fun (inst : C Nat) => { inst with } +/-- info: fun inst => { f := @C.f Nat instInhabitedNat inst, x := 1 } : C Nat → C Nat -/ +#guard_msgs in #check fun (inst : C Nat) => { inst with x := 1 } /-! @@ -93,7 +95,8 @@ Tests of implicit arguments in updates. structure I where f : {_ : Nat} → Nat + x := 1 -- used to give `fun i ↦ ?m.369 i : I → I` /-- info: fun i => { f := @I.f i } : I → I -/ -#guard_msgs in #check fun (i : I) => {i with} +#guard_msgs in #check fun (i : I) => {i with x := 1 } diff --git a/tests/lean/run/6123_cat_adjunction.lean b/tests/lean/run/6123_cat_adjunction.lean index 39f2879643..5c3234cb9d 100644 --- a/tests/lean/run/6123_cat_adjunction.lean +++ b/tests/lean/run/6123_cat_adjunction.lean @@ -338,7 +338,6 @@ end Cat def typeToCat : Type u ⥤ Cat where obj X := Cat.of (Discrete X) map := fun {X} {Y} f => by - dsimp exact Discrete.functor (Discrete.mk ∘ f) @[simp] theorem typeToCat_obj (X : Type u) : typeToCat.obj X = Cat.of (Discrete X) := rfl diff --git a/tests/lean/run/7353.lean b/tests/lean/run/7353.lean index ffa0b6c603..50cad34b7a 100644 --- a/tests/lean/run/7353.lean +++ b/tests/lean/run/7353.lean @@ -13,8 +13,7 @@ set_option pp.explicit true info: def foo : Foo := { obj := fun x => @Function.const Type (@Eq Unit Unit.unit Unit.unit) Nat foo.proof_1, map := - @id ((fun x => @Function.const Type (@Eq Unit Unit.unit Unit.unit) Nat foo.proof_1) Unit.unit) - (@OfNat.ofNat Nat 0 (instOfNatNat 0)) } + @id (@Function.const Type (@Eq Unit Unit.unit Unit.unit) Nat foo.proof_1) (@OfNat.ofNat Nat 0 (instOfNatNat 0)) } -/ #guard_msgs in #print foo diff --git a/tests/lean/run/linearCategory_perf_issue.lean b/tests/lean/run/linearCategory_perf_issue.lean index e195a964b9..d29f3d8895 100644 --- a/tests/lean/run/linearCategory_perf_issue.lean +++ b/tests/lean/run/linearCategory_perf_issue.lean @@ -265,17 +265,14 @@ instance Functor.category : Category.{max u₁ v₂} (C ⥤ D) where comp α β := vcomp α β id_comp := by intro X Y f - simp_all only ext x : 2 apply id_comp comp_id := by intro X Y f - simp_all only ext x : 2 apply comp_id assoc := by intro W X Y Z f g h - simp_all only ext x : 2 apply assoc @@ -384,7 +381,6 @@ instance functorCategoryPreadditive : Preadditive (C ⥤ D) where apply add_zero neg_add_cancel := by intros - dsimp only ext apply neg_add_cancel } add_comp := by diff --git a/tests/lean/run/mathlibetaissue.lean b/tests/lean/run/mathlibetaissue.lean index 248a518b73..5245204591 100644 --- a/tests/lean/run/mathlibetaissue.lean +++ b/tests/lean/run/mathlibetaissue.lean @@ -129,6 +129,7 @@ end Mathlib.Algebra.Ring.Defs section Mathlib.Data.Int.Basic instance : CommRing Int where + one := 1 mul_comm := sorry mul_one := Int.mul_one -- Replacing this with `sorry` makes the timeout go away! add_zero := Int.add_zero -- Similarly here. diff --git a/tests/lean/run/solve_by_elim.lean b/tests/lean/run/solve_by_elim.lean index 56591116b4..d9d507b0fa 100644 --- a/tests/lean/run/solve_by_elim.lean +++ b/tests/lean/run/solve_by_elim.lean @@ -122,7 +122,7 @@ example : 6 = 6 ∧ [7] = [7] := by -- Test that `Config.intros` causes `solve_by_elim` to call `intro` on intermediate goals. example (P : Prop) : P → P := by - fail_if_success solve_by_elim (config := {intros := false}) + fail_if_success solve_by_elim (config := {intro := false}) solve_by_elim -- This worked in mathlib3 without the `@`, but now goes into a loop. diff --git a/tests/lean/run/structInst.lean b/tests/lean/run/structInst.lean index e0b1513d18..580b34f647 100644 --- a/tests/lean/run/structInst.lean +++ b/tests/lean/run/structInst.lean @@ -58,13 +58,21 @@ structure B extends A where structure C extends B where (z : Nat := 2*y) (x := z + 2) (y := z + 3) -/-- info: { x := 1, y := 1 + 2, z := 2 * (1 + 2) } : C -/ +-- This first example does not work because the default values at `C` are the only ones considered. +/-- +error: fields missing: 'y', 'z' +--- +info: { x := 1, y := sorry, z := sorry } : C +-/ #guard_msgs in #check { x := 1 : C } /-- info: { x := 2 * 1 + 2, y := 1, z := 2 * 1 } : C -/ #guard_msgs in #check { y := 1 : C } /-- info: { x := 1 + 2, y := 1 + 3, z := 1 } : C -/ #guard_msgs in #check { z := 1 : C } +-- This first example does not work because the default values at `C` are the only ones considered. +/-- error: fields missing: 'y', 'z' -/ +#guard_msgs in def test1 : C where x := 1 def test2 : C where @@ -159,3 +167,154 @@ def test1 (z : Int) : A Int Int where z end Ex5 + +/-! +Default instances are applied before analyzing default values. +Without this, `α` would be reported as being a missing field. +-/ +namespace Ex6 +structure MyStruct where + {α : Type u} + {β : Type v} + a : α + b : β + +/-- info: { α := Nat, β := Bool, a := 10, b := true } : MyStruct -/ +#guard_msgs in #check { a := 10, b := true : MyStruct } +end Ex6 + +/-! +Make sure we have the Lean 3 behavior, where field projections are unfolded. +https://github.com/leanprover-community/mathlib4/issues/12129#issuecomment-2056134533 +-/ +namespace Mathlib12129 + +structure Foo where + toFun : Nat → Nat + +structure Bar extends Foo where + prop : toFun 0 = 0 + +/- +Rather than `(fun x => x) 0 = 0` or `{ toFun := fun x => x }.toFun 0 = 0` +-/ +/-- info: ⊢ 0 = 0 -/ +#guard_msgs in +def bar : Bar where + toFun x := x + prop := by + trace_state + rfl + +end Mathlib12129 + +/-! +Explicit fields must be provided, even if they can be inferred. +-/ +namespace Ex7 + +structure S where + n : Nat + m : Fin n + +variable (x : Fin 3) + +/-- +error: fields missing: 'n' + +field 'n' must be explicitly provided, its synthesized value is + 3 +--- +info: { n := 3, m := x } : S +-/ +#guard_msgs in #check { m := x : S } + +/-- info: { n := 3, m := x } : S -/ +#guard_msgs in #check { n := _, m := x : S } + +/-- info: { n := 3, m := x } : S -/ +#guard_msgs in #check { m := x, .. : S } + +/-- info: { n := 3, m := x } : S -/ +#guard_msgs in #check { n := 3, m := x : S } + +end Ex7 + +/-! +Diamond inheritance, acquire field values from parent classes. +https://github.com/leanprover/lean4/issues/6046 +-/ +namespace Issue6046 +set_option structure.strictResolutionOrder true + +class A + +class B extends A where + b : Unit + +structure B' where + b : Unit + +class C extends B', B, A + +instance : A where + +instance : B where + b := () + +instance : C where + +/-- +info: def Issue6046.instC : C := +{ b := B.b } +-/ +#guard_msgs in #print Issue6046.instC + +end Issue6046 + +/-! +Make sure parent fields still work if one parent depends on another. +-/ +namespace Ex8 + +class A (α : Type) where + val : α → Nat +class B (α : Type) [A α] where + val' : α → Nat + h : ∃ x : α, A.val x = val' x +class C (α : Type) extends A α, B α + +instance : A Nat where + val := id +instance : B Nat where + val' _ := 0 + h := by exists 0 + +/- +This was "fields missing: 'val'', 'h'" at some point during testing. +To succeed, this relies on being able to compute the type of the `B` parent, +which depends on fields of the structure instance being elaborated. +-/ +/-- info: { toA := instANat, toB := instBNat } : C Nat -/ +#guard_msgs in #check { : C Nat } + +end Ex8 + +/-! +Autoparams are elaborated eagerly. Here we see that `a` is printed before `b`. +-/ +namespace Ex9 +structure A where + n : Nat := by trace "a"; exact 1 + m : Fin n + +/-- +info: a +--- +info: b +-/ +#guard_msgs in +example : A where + m := by trace "b"; exact 0 + +end Ex9 diff --git a/tests/lean/run/structInst3.lean b/tests/lean/run/structInst3.lean index 136a250408..2dacbf5c0b 100644 --- a/tests/lean/run/structInst3.lean +++ b/tests/lean/run/structInst3.lean @@ -1,16 +1,18 @@ universe u +set_option pp.structureInstanceTypes true + namespace Ex1 -structure A (α : Type u) := -(x : α) (f : α → α := λ x => x) +structure A (α : Type u) where + (x : α) (f : α → α := λ x => x) -structure B (α : Type u) extends A α := -(y : α := f (f x)) (g : α → α → α := λ x y => f x) +structure B (α : Type u) extends A α where + (y : α := f (f x)) (g : α → α → α := λ x y => f x) -structure C (α : Type u) extends B α := -(z : α := g x y) (x := f z) +structure C (α : Type u) extends B α where + (z : α := g x y) (x := f z) end Ex1 @@ -18,24 +20,60 @@ open Ex1 def c1 : C Nat := { x := 1 } -#check { c1 with z := 2 } - -#check { c1 with z := 2 } +/-- +info: let __src := c1; +{ toB := __src.toB, z := 2 : C Nat } : C Nat +-/ +#guard_msgs in #check { c1 with z := 2 } theorem ex1 : { c1 with z := 2 }.z = 2 := rfl -#check ex1 +/-- +info: ex1 : + (let __src := c1; + { toB := __src.toB, z := 2 : C Nat }).z = + 2 +-/ +#guard_msgs in #check ex1 theorem ex2 : { c1 with z := 2 }.x = c1.x := rfl -#check ex2 +/-- +info: ex2 : + (let __src := c1; + { toB := __src.toB, z := 2 : C Nat }).x = + c1.x +-/ +#guard_msgs in #check ex2 def c2 : C (Nat × Nat) := { z := (1, 1) } -#check { c2 with x.fst := 2 } +/-- +info: let __src := c2; +{ + x := + let __src := __src.x; + (2, __src.snd), + f := __src.f, y := __src.y, g := __src.g, z := __src.z : C (Nat × Nat) } : C (Nat × Nat) +-/ +#guard_msgs in #check { c2 with x.fst := 2 } -#check { c2 with x.1 := 3 } +/-- +info: let __src := c2; +{ + x := + let __src := __src.x; + (3, __src.snd), + f := __src.f, y := __src.y, g := __src.g, z := __src.z : C (Nat × Nat) } : C (Nat × Nat) +-/ +#guard_msgs in #check { c2 with x.1 := 3 } -#check show C _ from { c2.toB with .. } +/-- +info: let_fun this := + let __src := c2.toB; + { toB := __src, z := __src.g __src.x __src.y : C (Nat × Nat) }; +this : C (Nat × Nat) +-/ +#guard_msgs in #check show C _ from { c2.toB with .. } diff --git a/tests/lean/run/structInst4.lean b/tests/lean/run/structInst4.lean index cde1f3d5e3..5e8dced536 100644 --- a/tests/lean/run/structInst4.lean +++ b/tests/lean/run/structInst4.lean @@ -3,23 +3,88 @@ universe u def a : Array ((Nat × Nat) × Bool) := #[] def b : Array Nat := #[] -structure Foo := -(x : Array ((Nat × Nat) × Bool) := #[]) -(y : Nat := 0) +structure Foo where + (x : Array ((Nat × Nat) × Bool) := #[]) + (y : Nat := 0) -#check (b).modifyOp (idx := 1) (fun s => 2) +/-- info: b.modifyOp 1 fun _s => 2 : Array Nat -/ +#guard_msgs in #check (b).modifyOp (idx := 1) (fun _s => 2) -#check { b with [1] := 2 } +/-- +info: let __src := b; +__src.modifyOp 1 fun s => 2 : Array Nat +-/ +#guard_msgs in #check { b with [1] := 2 } -#check { a with [1].fst.2 := 1 } +/-- +info: let __src := a; +__src.modifyOp 1 fun s => + (let __src := s.fst; + (__src.fst, 1), + s.snd) : Array ((Nat × Nat) × Bool) +-/ +#guard_msgs in #check { a with [1].fst.2 := 1 } def foo : Foo := {} -#check foo.x[1]!.1.2 +/-- info: foo.x[1]!.fst.snd : Nat -/ +#guard_msgs in #check foo.x[1]!.1.2 -#check { foo with x[1].2 := true } -#check { foo with x[1].fst.snd := 1 } -#check { foo with x[1].1.fst := 1 } +/-- +info: let __src := foo; +{ + x := + let __src := __src.x; + __src.modifyOp 1 fun s => (s.fst, true), + y := __src.y } : Foo +-/ +#guard_msgs in #check { foo with x[1].2 := true } +/-- +info: let __src := foo; +{ + x := + let __src := __src.x; + __src.modifyOp 1 fun s => + (let __src := s.fst; + (__src.fst, 1), + s.snd), + y := __src.y } : Foo +-/ +#guard_msgs in #check { foo with x[1].fst.snd := 1 } +/-- +info: let __src := foo; +{ + x := + let __src := __src.x; + __src.modifyOp 1 fun s => + (let __src := s.fst; + (1, __src.snd), + s.snd), + y := __src.y } : Foo +-/ +#guard_msgs in #check { foo with x[1].1.fst := 1 } -#check { foo with x[1].1.1 := 5 } -#check { foo with x[1].1.2 := 5 } +/-- +info: let __src := foo; +{ + x := + let __src := __src.x; + __src.modifyOp 1 fun s => + (let __src := s.fst; + (5, __src.snd), + s.snd), + y := __src.y } : Foo +-/ +#guard_msgs in #check { foo with x[1].1.1 := 5 } +/-- +info: let __src := foo; +{ + x := + let __src := __src.x; + __src.modifyOp 1 fun s => + (let __src := s.fst; + (__src.fst, 5), + s.snd), + y := __src.y } : Foo +-/ +#guard_msgs in #check { foo with x[1].1.2 := 5 } diff --git a/tests/lean/structInstExtraEta.lean b/tests/lean/run/structInstExtraEta.lean similarity index 56% rename from tests/lean/structInstExtraEta.lean rename to tests/lean/run/structInstExtraEta.lean index b8c92b9d67..4bdfc01fd2 100644 --- a/tests/lean/structInstExtraEta.lean +++ b/tests/lean/run/structInstExtraEta.lean @@ -18,10 +18,25 @@ structure D extends B def a : A := ⟨ 0 ⟩ def b : B := { a with } -#print b +/-- +info: def b : B := +let __src := a; +{ toA := __src } +-/ +#guard_msgs in #print b def c : C := { a with } -#print c +/-- +info: def c : C := +let __src := a; +{ toB := { toA := __src } } +-/ +#guard_msgs in #print c def d : D := { c with } -#print d +/-- +info: def d : D := +let __src := c; +{ toB := __src.toB } +-/ +#guard_msgs in #print d diff --git a/tests/lean/run/structInstFast.lean b/tests/lean/run/structInstFast.lean index e398a09469..ef5c7c0b8a 100644 --- a/tests/lean/run/structInstFast.lean +++ b/tests/lean/run/structInstFast.lean @@ -48,7 +48,7 @@ def baseTypeIdent := mkIdent (Name.mkSimple "Base") def init (type val : TSyntax `ident) (width : Nat) : MacroM (TSyntax `command) := do let fieldsStx ← mkFieldsStx type "base_" width - let vals := Array.mkArray width val + let vals := Array.replicate width val `(structure $baseTypeIdent where $fieldsStx:structFields def $baseIdent : $baseTypeIdent := ⟨$vals,*⟩) diff --git a/tests/lean/run/structInstUpdates.lean b/tests/lean/run/structInstUpdates.lean new file mode 100644 index 0000000000..d6d26eefb6 --- /dev/null +++ b/tests/lean/run/structInstUpdates.lean @@ -0,0 +1,17 @@ +structure A where + x : Nat := 0 + +structure B extends A where + y : Nat := 0 + +structure C extends B where + z : Nat := 0 + +variable (c : C) + +/-- info: { x := 1, y := c.y, z := c.z } : C -/ +#guard_msgs in #check { c with x := 1 } +/-- info: { toA := c.toA, y := 1, z := c.z } : C -/ +#guard_msgs in #check { c with y := 1 } +/-- info: { toB := c.toB, z := 1 } : C -/ +#guard_msgs in #check { c with z := 1 } diff --git a/tests/lean/run/structNamedParentProj.lean b/tests/lean/run/structNamedParentProj.lean index 5c8dcd0eb5..b3d1883af0 100644 --- a/tests/lean/run/structNamedParentProj.lean +++ b/tests/lean/run/structNamedParentProj.lean @@ -122,3 +122,15 @@ field notation resolution order: S2', S, U -/ #guard_msgs in #print S2' + +/-! +Structure instances, setting a parent +-/ +/-- info: { toTheS := s, y := 1 } : S2' -/ +#guard_msgs in variable (s : S) in #check { toTheS := s, y := 1 : S2' } +/-- info: { x := s.x, y := 1 } : S2' -/ +#guard_msgs in variable (s : U) in #check { toTheU := s, y := 1 : S2' } +/-- info: { x := 2, y := 1 } : S2' -/ +#guard_msgs in #check { toTheS.x := 2, y := 1 : S2' } +/-- info: { x := 2, y := 1 } : S2' -/ +#guard_msgs in #check { toTheU.x := 2, y := 1 : S2' } diff --git a/tests/lean/run/struct_inst_typed.lean b/tests/lean/run/struct_inst_typed.lean index 02de514f66..dae607da55 100644 --- a/tests/lean/run/struct_inst_typed.lean +++ b/tests/lean/run/struct_inst_typed.lean @@ -1,10 +1,13 @@ -#check { fst := 10, snd := 20 : Nat × Nat } +/-- info: (10, 20) : Nat × Nat -/ +#guard_msgs in #check { fst := 10, snd := 20 : Nat × Nat } -structure S := -(x : Nat) (y : Bool) (z : String) +structure S where + (x : Nat) (y : Bool) (z : String) -#check { x := 10, y := true, z := "hello" : S } +/-- info: { x := 10, y := true, z := "hello" } : S -/ +#guard_msgs in #check { x := 10, y := true, z := "hello" : S } -#check { fst := "hello", snd := "world" : Prod _ _ } +/-- info: ("hello", "world") : String × String -/ +#guard_msgs in #check { fst := "hello", snd := "world" : Prod _ _ } diff --git a/tests/lean/run/structureElab.lean b/tests/lean/run/structureElab.lean index f92c3601a2..86dfd2530b 100644 --- a/tests/lean/run/structureElab.lean +++ b/tests/lean/run/structureElab.lean @@ -34,27 +34,27 @@ structure S4 (α : Type) extends S2 α, S3 α where /-- info: Test1.S4.mk {α : Type} (toS2 : S2 α) (w : Nat) (x' : α) : S4 α -/ #guard_msgs in #check S4.mk /-- -info: def Test1.S1._flat_ctor : {α : Type} → α → Nat → S1 α := +info: def Test1.S1.mk._flat_ctor : {α : Type} → α → Nat → S1 α := fun α x y => S1.mk x y -/ -#guard_msgs in #print S1._flat_ctor +#guard_msgs in #print S1.mk._flat_ctor /-- -info: def Test1.S2._flat_ctor : {α : Type} → α → Nat → Nat → S2 α := +info: def Test1.S2.mk._flat_ctor : {α : Type} → α → Nat → Nat → S2 α := fun α x y z => S2.mk (S1.mk x y) z -/ -#guard_msgs in #print S2._flat_ctor +#guard_msgs in #print S2.mk._flat_ctor /-- -info: def Test1.S3._flat_ctor : {α : Type} → α → Nat → Nat → S3 α := +info: def Test1.S3.mk._flat_ctor : {α : Type} → α → Nat → Nat → S3 α := fun α x y w => S3.mk (S1.mk x y) w -/ -#guard_msgs in #print S3._flat_ctor +#guard_msgs in #print S3.mk._flat_ctor /-- -info: def Test1.S4._flat_ctor : {α : Type} → α → Nat → Nat → Nat → α → S4 α := +info: def Test1.S4.mk._flat_ctor : {α : Type} → α → Nat → Nat → Nat → α → S4 α := fun α x y z w x' => S4.mk (S2.mk (S1.mk x y) z) w x' -/ -#guard_msgs in #print S4._flat_ctor -/-- info: Test1.S4._flat_ctor {α : Type} (x : α) (y z w : Nat) (x' : α) : S4 α -/ -#guard_msgs in #check S4._flat_ctor +#guard_msgs in #print S4.mk._flat_ctor +/-- info: Test1.S4.mk._flat_ctor {α : Type} (x : α) (y z w : Nat) (x' : α) : S4 α -/ +#guard_msgs in #check S4.mk._flat_ctor end Test1 @@ -146,16 +146,16 @@ info: Test2_1.Semigroup.mk.{u_1} {α : Type u_1} [toMul : Mul α] [toAssociative -/ #guard_msgs in #check Semigroup.mk /-- -info: def Test2_1.Semigroup._flat_ctor.{u_1} : {α : Type u_1} → +info: def Test2_1.Semigroup.mk._flat_ctor.{u_1} : {α : Type u_1} → (mul : α → α → α) → (∀ (x y z : α), @Eq α (mul (mul x y) z) (mul x (mul y z))) → Semigroup α := fun α mul mul_assoc => @Semigroup.mk α (@Mul.mk α mul) (@AssociativeMul.mk α (@Mul.mk α mul) mul_assoc) -/ -#guard_msgs in set_option pp.explicit true in #print Semigroup._flat_ctor +#guard_msgs in set_option pp.explicit true in #print Semigroup.mk._flat_ctor /-- -info: Test2_1.Semigroup._flat_ctor.{u_1} {α : Type u_1} (mul : α → α → α) +info: Test2_1.Semigroup.mk._flat_ctor.{u_1} {α : Type u_1} (mul : α → α → α) (mul_assoc : ∀ (x y z : α), @Eq α (mul (mul x y) z) (mul x (mul y z))) : Semigroup α -/ -#guard_msgs in set_option pp.explicit true in #check Semigroup._flat_ctor +#guard_msgs in set_option pp.explicit true in #check Semigroup.mk._flat_ctor end Test2_1 @@ -171,10 +171,10 @@ class Add3 (α : Type _) extends Add2 α, Add α where h (x : α) : x + x = x /-- -info: Test2_2.Add3._flat_ctor.{u_1} {α : Type u_1} (add : α → α → α) +info: Test2_2.Add3.mk._flat_ctor.{u_1} {α : Type u_1} (add : α → α → α) (h : ∀ (x : α), @Eq α (@HAdd.hAdd α α α (@instHAdd α (@Add.mk α add)) x x) x) : Add3 α -/ -#guard_msgs in set_option pp.explicit true in #check Add3._flat_ctor +#guard_msgs in set_option pp.explicit true in #check Add3.mk._flat_ctor end Test2_2 @@ -243,7 +243,7 @@ info: Test4.Semigroup.mk.{u_1} (toMagma : Magma) #guard_msgs in set_option pp.explicit true in #check Semigroup.mk /-- -info: def Test4.Semigroup._flat_ctor.{u_1} : (α : Type u_1) → +info: def Test4.Semigroup.mk._flat_ctor.{u_1} : (α : Type u_1) → (mul : α → α → α) → (∀ (a b c : α), @Eq α (@Test4.mul (Magma.mk α mul) (@Test4.mul (Magma.mk α mul) a b) c) @@ -251,7 +251,7 @@ info: def Test4.Semigroup._flat_ctor.{u_1} : (α : Type u_1) → Semigroup := fun α mul mul_assoc => Semigroup.mk (Magma.mk α mul) mul_assoc -/ -#guard_msgs in set_option pp.explicit true in #print Semigroup._flat_ctor +#guard_msgs in set_option pp.explicit true in #print Semigroup.mk._flat_ctor end Test4 @@ -332,10 +332,10 @@ structure A2 extends A1 where h : n > 0 /-- -info: def Test7.A2._flat_ctor : (n : Nat) → n > 0 → A2 := +info: def Test7.A2.mk._flat_ctor : (n : Nat) → n > 0 → A2 := fun n h => A2.mk (A1.mk n) h -/ -#guard_msgs in #print A2._flat_ctor +#guard_msgs in #print A2.mk._flat_ctor end Test7 @@ -384,23 +384,22 @@ structure S4 extends S2, S3 #guard_msgs in #check S3.mk /-- info: TestO1.S4.mk (toS2 : S2) : S4 -/ #guard_msgs in #check S4.mk -/-- info: TestO1.S1._flat_ctor (x : Nat := by exact 0) : S1 -/ -#guard_msgs in #check S1._flat_ctor -/-- info: TestO1.S2._flat_ctor (x : Nat := by exact 0) : S2 -/ -#guard_msgs in #check S2._flat_ctor -/-- info: TestO1.S3._flat_ctor (x : Nat := by exact 1) : S3 -/ -#guard_msgs in #check S3._flat_ctor -/-- info: TestO1.S4._flat_ctor (x : Nat := by exact 1) : S4 -/ -#guard_msgs in #check S4._flat_ctor +/-- info: TestO1.S1.mk._flat_ctor (x : Nat := by exact 0) : S1 -/ +#guard_msgs in #check S1.mk._flat_ctor +/-- info: TestO1.S2.mk._flat_ctor (x : Nat := by exact 0) : S2 -/ +#guard_msgs in #check S2.mk._flat_ctor +/-- info: TestO1.S3.mk._flat_ctor (x : Nat := by exact 1) : S3 -/ +#guard_msgs in #check S3.mk._flat_ctor +/-- info: TestO1.S4.mk._flat_ctor (x : Nat := by exact 1) : S4 -/ +#guard_msgs in #check S4.mk._flat_ctor --- TODO These don't work yet. Need to fix structure instance notation elaborator. /-- info: S1.mk 0 : S1 -/ #guard_msgs in #check { : S1 } /-- info: S2.mk (S1.mk 0) : S2 -/ #guard_msgs in #check { : S2 } -/-- info: S3.mk (S1.mk 0) : S3 -/ +/-- info: S3.mk (S1.mk 1) : S3 -/ #guard_msgs in #check { : S3 } -/-- info: S4.mk (S2.mk (S1.mk 0)) : S4 -/ +/-- info: S4.mk (S2.mk (S1.mk 1)) : S4 -/ #guard_msgs in #check { : S4 } end TestO1 @@ -426,27 +425,26 @@ structure S4 extends S2, S3 #guard_msgs in #check S3.mk /-- info: TestO2.S4.mk (toS2 : S2) : S4 -/ #guard_msgs in #check S4.mk -/-- info: TestO2.S1._flat_ctor (x : Nat := by exact 0) : S1 -/ -#guard_msgs in #check S1._flat_ctor -/-- info: TestO2.S2._flat_ctor (x : Nat := by exact 0) : S2 -/ -#guard_msgs in #check S2._flat_ctor -/-- info: TestO2.S3._flat_ctor (x : Nat) : S3 -/ -#guard_msgs in #check S3._flat_ctor +/-- info: TestO2.S1.mk._flat_ctor (x : Nat := by exact 0) : S1 -/ +#guard_msgs in #check S1.mk._flat_ctor +/-- info: TestO2.S2.mk._flat_ctor (x : Nat := by exact 0) : S2 -/ +#guard_msgs in #check S2.mk._flat_ctor +/-- info: TestO2.S3.mk._flat_ctor (x : Nat) : S3 -/ +#guard_msgs in #check S3.mk._flat_ctor /-- info: TestO2.S3.x._default : Nat -/ #guard_msgs in #check S3.x._default -/-- info: TestO2.S4._flat_ctor (x : Nat) : S4 -/ -#guard_msgs in #check S4._flat_ctor +/-- info: TestO2.S4.mk._flat_ctor (x : Nat) : S4 -/ +#guard_msgs in #check S4.mk._flat_ctor /-- info: TestO2.S4.x._inherited_default : Nat -/ #guard_msgs in #check S4.x._inherited_default --- TODO These don't work yet. Need to fix structure instance notation elaborator. /-- info: S1.mk 0 : S1 -/ #guard_msgs in #check { : S1 } /-- info: S2.mk (S1.mk 0) : S2 -/ #guard_msgs in #check { : S2 } -/-- info: S3.mk (S1.mk 0) : S3 -/ +/-- info: S3.mk (S1.mk 1) : S3 -/ #guard_msgs in #check { : S3 } -/-- info: S4.mk (S2.mk (S1.mk 0)) : S4 -/ +/-- info: S4.mk (S2.mk (S1.mk 1)) : S4 -/ #guard_msgs in #check { : S4 } end TestO2 diff --git a/tests/lean/run/tactic_config.lean b/tests/lean/run/tactic_config.lean index 61747a8115..5dee17ae49 100644 --- a/tests/lean/run/tactic_config.lean +++ b/tests/lean/run/tactic_config.lean @@ -150,10 +150,21 @@ Responds to recovery mode. In these, `ctac` continues even though configuration error: structure 'C' does not have a field named 'x' --- info: config is { b := { toA := { x := true } } } +--- +info: ⊢ True -/ #guard_msgs in example : True := by ctac -x + trace_state + trivial + +-- Check that when recovery mode is false, no error is reported. +/-- info: ⊢ True -/ +#guard_msgs in +example : True := by + fail_if_success ctac -x + trace_state trivial /-- diff --git a/tests/lean/structInst1.lean.expected.out b/tests/lean/structInst1.lean.expected.out index 408bf2f8ac..7742a6f402 100644 --- a/tests/lean/structInst1.lean.expected.out +++ b/tests/lean/structInst1.lean.expected.out @@ -1,3 +1,3 @@ -structInst1.lean:12:11-12:19: error: field 'toA' has already been specified +structInst1.lean:12:21-12:22: error: field 'x' has already been specified f5 (c : C) (a : A) : C f6 (c : C) (a : A) : A diff --git a/tests/lean/structInstExtraEta.lean.expected.out b/tests/lean/structInstExtraEta.lean.expected.out deleted file mode 100644 index 91c2ef1ab7..0000000000 --- a/tests/lean/structInstExtraEta.lean.expected.out +++ /dev/null @@ -1,9 +0,0 @@ -def b : B := -let __src := a; -{ toA := __src } -def c : C := -let __src := a; -{ toB := { toA := __src } } -def d : D := -let __src := c; -{ toB := __src.toB } diff --git a/tests/lean/structInstSourcesLeftToRight.lean.expected.out b/tests/lean/structInstSourcesLeftToRight.lean.expected.out index 84843fa79c..597f3b9c38 100644 --- a/tests/lean/structInstSourcesLeftToRight.lean.expected.out +++ b/tests/lean/structInstSourcesLeftToRight.lean.expected.out @@ -1,7 +1,7 @@ def foo : A → B → B := fun a b => { x := a.x, y := b.y } def boo : A → B → B := -fun a b => { x := b.x, y := b.y } +fun a b => b def baz : A → B → C := fun a b => { toB := { x := a.x, y := b.y } } def biz : A → B → C := @@ -9,4 +9,4 @@ fun a b => { toB := b } def faz : A → C → C := fun a c => { toB := { x := a.x, y := c.y } } def fiz : A → C → C := -fun a c => { toB := c.toB } +fun a c => c diff --git a/tests/pkg/prv/Prv.lean b/tests/pkg/prv/Prv.lean index 512ed50963..3eda5fb5e0 100644 --- a/tests/pkg/prv/Prv.lean +++ b/tests/pkg/prv/Prv.lean @@ -17,7 +17,7 @@ error: overloaded, errors ⏎ ⏎ Additional diagnostic information may be available using the `set_option diagnostics true` command. ⏎ - invalid {...} notation, constructor for `Name` is marked as private + invalid {...} notation, constructor for 'Name' is marked as private -/ #guard_msgs in def m1 : Name "hello" := {}