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" := {}