From 119854e2487d4f342d9814ef1dce70e6af305b47 Mon Sep 17 00:00:00 2001 From: jrr6 <7482866+jrr6@users.noreply.github.com> Date: Wed, 16 Jul 2025 23:22:34 -0400 Subject: [PATCH] feat: add hints for missing structure instance fields (#9317) This PR adds to the "fields missing" error message for structure instance notation a code-action hint that inserts all missing fields. --- src/Lean/Elab.lean | 1 + src/Lean/Elab/StructInst.lean | 19 +- src/Lean/Elab/StructInstHint.lean | 171 +++++++ tests/lean/instance1.lean.expected.out | 2 +- .../interactive/structInstFieldHints.lean | 222 +++++++++ .../structInstFieldHints.lean.expected.out | 421 ++++++++++++++++++ tests/lean/run/461b.lean | 2 +- tests/lean/run/structInst.lean | 17 +- .../semicolonOrLinebreak.lean.expected.out | 2 +- tests/lean/setLit.lean.expected.out | 5 +- 10 files changed, 849 insertions(+), 13 deletions(-) create mode 100644 src/Lean/Elab/StructInstHint.lean create mode 100644 tests/lean/interactive/structInstFieldHints.lean create mode 100644 tests/lean/interactive/structInstFieldHints.lean.expected.out diff --git a/src/Lean/Elab.lean b/src/Lean/Elab.lean index 6011d9c3f4..2433a0ba56 100644 --- a/src/Lean/Elab.lean +++ b/src/Lean/Elab.lean @@ -23,6 +23,7 @@ import Lean.Elab.Quotation import Lean.Elab.Syntax import Lean.Elab.Do import Lean.Elab.StructInst +import Lean.Elab.StructInstHint import Lean.Elab.MutualInductive import Lean.Elab.Inductive import Lean.Elab.Structure diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index 5980449c05..3c46a051af 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/src/Lean/Elab/StructInst.lean @@ -9,6 +9,7 @@ import Lean.Parser.Term import Lean.Meta.Structure import Lean.Elab.App import Lean.Elab.Binders +import Lean.Elab.StructInstHint import Lean.PrettyPrinter /-! @@ -747,6 +748,7 @@ private structure PendingField where deps : NameSet val? : Option Expr + /-- Synthesize pending optParams. -/ @@ -812,7 +814,7 @@ private def synthOptParamFields : StructInstM Unit := do toRemove := toRemove.push selected.fieldName else assignErrors := assignErrors.push m!"\ - occurs check failed, field '{selected.fieldName}' of type{indentExpr fieldType}\n\ + Occurs check failed: Field `{selected.fieldName}` of type{indentExpr fieldType}\n\ cannot be assigned the default value{indentExpr selectedVal}" else assignErrors := assignErrors.push m!"\ @@ -833,22 +835,29 @@ private def synthOptParamFields : StructInstM Unit := do 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}'" + Cannot synthesize placeholder for field `{pendingField.fieldName}`" return let assignErrorsMsg := MessageData.joinSep (assignErrors.map (m!"\n\n" ++ ·)).toList "" let mut requiredErrors : Array MessageData := #[] + let mut unsolvedFields : Std.HashSet Name := {} for pendingField in pendingFields do if (← isFieldNotSolved? pendingField.fieldName).isNone then + unsolvedFields := unsolvedFields.insert pendingField.fieldName let e := (← get).fieldMap.find! pendingField.fieldName requiredErrors := requiredErrors.push m!"\ - field '{pendingField.fieldName}' must be explicitly provided, its synthesized value is{indentExpr e}" + 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}" + let missing := missingFields |>.map (s!"`{·.fieldName}`") |>.toList + let missingFieldsValues ← missingFields.mapM fun field => do + if unsolvedFields.contains field.fieldName then + pure <| (field.fieldName, some <| (← get).fieldMap.find! field.fieldName) + else pure (field.fieldName, none) + let missingFieldsHint ← mkMissingFieldsHint missingFieldsValues (← read).view.ref + let msg := m!"Fields missing: {", ".intercalate missing}{assignErrorsMsg}{requiredErrorsMsg}{missingFieldsHint}" if (← readThe Term.Context).errToSorry then -- Assign all pending problems using synthetic sorries and log an error. for pendingField in pendingFields do diff --git a/src/Lean/Elab/StructInstHint.lean b/src/Lean/Elab/StructInstHint.lean new file mode 100644 index 0000000000..a2d100ab64 --- /dev/null +++ b/src/Lean/Elab/StructInstHint.lean @@ -0,0 +1,171 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Rotella +-/ + +prelude +import Lean.Parser.Term +import Lean.Meta.Hint +import Lean.PrettyPrinter + +/-! +# Missing-field hints for structure instance elaborator + +This module generates suggested edits for structure instance notation that is missing required +fields. The suggestions adapt to the style of the existing structure instance syntax and +automatically insert any values inferred via constraints generated by already present fields. +-/ + +namespace Lean.Elab.Term.StructInst + +open Meta +open TSyntax.Compat + +/-- Auxiliary type for `mkMissingFieldsHint` -/ +private structure FieldsHintView where + /-- The position of the first existing field in the structure instance, if one exists. -/ + initFieldPos? : Option String.Pos + /-- The tail position of the last existing field, or `none` if there are none. -/ + lastFieldTailPos? : Option String.Pos + /-- Does this structure instance have a `with` clause? -/ + hasWith : Bool + /-- The number of existing fields present in the structure instance. -/ + numFields : Nat + /-- The position of the opening syntax (i.e., `{`) for the structure instance. -/ + openingPos : String.Pos + /-- The position of the "leader" immediately preceding the fields -- either `with` or `{`. -/ + leaderPos : String.Pos + /-- The tail position of the "leader" syntax. -/ + leaderTailPos : String.Pos + /-- + The position of the closing syntax (i.e., `}`) for the structure instance. + + We refer only to the "closing" token `}` rather than a flexible "trailer" because macro-expansion + erases the type annotation if it was present, and it's impossible to have an ellipsis if we're + generating a "fields missing" error. + -/ + closingPos : String.Pos + +/-- +Creates a hint message for the "fields missing" error that fills in the missing fields, adapting to +the structure instance notation style of the current syntax. Note that if the syntax is malformed or +synthetic, this function returns an empty message instead. +-/ +def mkMissingFieldsHint (fields : Array (Name × Option Expr)) (stx : Syntax) : MetaM MessageData := do + let some view := mkFieldsHintView? stx | return .nil + let newFields ← fields.mapM fun (fieldName, fieldVal?) => do + let value ← if let some fieldVal := fieldVal? then + let stx ← withOptions (pp.mvars.set · false) <| PrettyPrinter.delab fieldVal + pure (← PrettyPrinter.ppCategory `term stx).pretty + else pure "_" + pure s!"{fieldName} := {value}" + let useSingleLine ← isSingleLineStyle view + let suggestionText := + if useSingleLine then + .group (behavior := .fill) <| + newFields.foldl (init := Std.Format.nil) (fun acc sug => acc ++ "," ++ .line ++ format sug) + else + Format.line.joinSep newFields.toList + + let fileMap ← getFileMap + let col (p : String.Pos) := (fileMap.utf8PosToLspPos p).character + let indent := + if let some initFieldPos := view.initFieldPos? then + col initFieldPos + else + -- Take the minimum of the opening and closing brace indentations to account for both the + -- `...\n{ f := v\n ... }` and `...{\n f := v\n ... \n}` styles + min (col view.openingPos) (col view.closingPos) + 2 + + let leaderLine := (fileMap.utf8PosToLspPos view.leaderPos).line + let leaderClosingSeparated : Bool := leaderLine < (fileMap.utf8PosToLspPos view.closingPos).line + -- If a line separates the leader and `}`, and there's no intervening text, `interveningLineEndPos?` + -- gives the position on that line (the min of column `indent` and the line end) at which to insert + let interveningLineEndPos? := + if leaderLine + 1 ≥ (fileMap.utf8PosToLspPos view.closingPos).line then none else + let leaderLineEnd := findLineEnd fileMap.source view.leaderTailPos + let indentPos := (indent + 1).fold (init := leaderLineEnd) (fun _ _ p => fileMap.source.next p) + let interveningLineEnd := findLineEnd fileMap.source (fileMap.source.next leaderLineEnd) + let nextTwoLines := Substring.mk fileMap.source view.leaderTailPos interveningLineEnd + if nextTwoLines.all (·.isWhitespace) then some (min indentPos nextTwoLines.stopPos) else none + + let (preWs, postWs) : Format × Format := + -- If we're in single-line mode, `suggestionText` already has a leading `, `, so insert it as-is + if useSingleLine then + (.nil, .nil) + -- Ensure a line break for consistent indentation if fields exist or there are no fields after `with` + else if view.numFields > 0 || (view.hasWith && !leaderClosingSeparated) then + (.line, .nil) + -- If there is no intervening line, add spaces before and after for `{ f := v\n ...}` style + else if !leaderClosingSeparated then + (" ", " ") + -- If there is an intervening line, insert therein if the region is empty; else insert before + -- it, as the nonempty region may contain a type annotation + else + match interveningLineEndPos? with + | none => (.line, .nil) + | some interveningLineEndPos => + (String.mk (List.replicate (indent - col interveningLineEndPos) ' '), .nil) + let suggestionText := preWs ++ suggestionText ++ postWs + let insPos := view.lastFieldTailPos?.getD <| interveningLineEndPos?.getD view.leaderTailPos + let width := Tactic.TryThis.format.inputWidth.get (← getOptions) + -- Limit only the span of the suggestion so the code action appears everywhere in the structure + let suggestion := { + suggestion := suggestionText.pretty width indent (col insPos), + span? := Syntax.ofRange ⟨insPos, insPos⟩, + toCodeActionTitle? := some fun _ => "Add missing fields" + } + MessageData.hint m!"Add missing fields:" #[suggestion] +where + /-- + Constructs a `FieldsHintView` used to generate missing-fields hint suggestions. This method + consolidates the low-level syntax inspection required for `mkMissingFieldsHint`. + -/ + mkFieldsHintView? (stx : Syntax) : Option FieldsHintView := do + -- Only show suggestions for user-entered structure-instance notation + -- TODO: selectively let through macro-expanded `where` notation + guard <| stx.getHeadInfo matches .original .. + guard <| stx.getKind == ``Parser.Term.structInst + let (leader, hasWith) := if stx[1][1] matches .missing then + (stx[0], false) + else + (stx[1][1], true) + let fields := stx[2][0].getSepArgs + some { leaderPos := (← leader.getPos?) + leaderTailPos := (← leader.getTailPos?) + openingPos := (← stx[0].getPos?) + closingPos := (← stx[5].getPos?) + numFields := fields.size + initFieldPos? := fields[0]?.bind (·.getPos?) + lastFieldTailPos? := fields[fields.size - 1]?.bind (·.getTailPos?) + hasWith } + + /-- + Returns the position of the end of the line that contains the position `pos`. + Counterpart of `String.findLineStart`. + -/ + findLineEnd (s : String) (p : String.Pos) : String.Pos := + s.findAux (· == '\n') s.endPos p + + /-- + Is the structure instance notation `stx` described by `view` using single-line styling? + + We infer this based on whether the last two fields are comma-separated and either on the same line + or indented in a way not possible with one-field-per-line styling. + -/ + isSingleLineStyle (view : FieldsHintView) : MetaM Bool := do + unless view.numFields ≥ 2 do return false + let rawFields := stx[2][0] + -- Account for the fact that we may have a trailing separator: + let lastInterveningSepIdx := rawFields.getNumArgs - 2 - ((rawFields.getNumArgs + 1) % 2) + unless rawFields[lastInterveningSepIdx].getKind == `«,» do + return false + + let some penultimateFieldPos := rawFields[lastInterveningSepIdx - 1].getPos? | return false + let some lastFieldPos := rawFields[lastInterveningSepIdx + 1].getPos? | return false + let some lastFieldTailPos := rawFields[lastInterveningSepIdx + 1].getTailPos? | return false + let fileMap ← getFileMap + let ⟨penultimateFieldLine, penultimateFieldCol⟩ := fileMap.utf8PosToLspPos penultimateFieldPos + let ⟨lastFieldLine, lastFieldCol⟩ := fileMap.utf8PosToLspPos lastFieldPos + return lastFieldLine == penultimateFieldLine || lastFieldCol < penultimateFieldCol diff --git a/tests/lean/instance1.lean.expected.out b/tests/lean/instance1.lean.expected.out index 174df89903..60e2e68d35 100644 --- a/tests/lean/instance1.lean.expected.out +++ b/tests/lean/instance1.lean.expected.out @@ -1 +1 @@ -instance1.lean:6:24-10:0: error: fields missing: 'pure', 'bind' +instance1.lean:6:24-10:0: error: Fields missing: `pure`, `bind` diff --git a/tests/lean/interactive/structInstFieldHints.lean b/tests/lean/interactive/structInstFieldHints.lean new file mode 100644 index 0000000000..c2e1ffe7bc --- /dev/null +++ b/tests/lean/interactive/structInstFieldHints.lean @@ -0,0 +1,222 @@ +import Lean.Parser.Term +/-! +# Hints for missing structure instance fields + +This file tests the code action-containing hints for missing fields in structure instances. It tests +a variety of formatting styles to ensure that the generated code action adheres to the conventions +of the in-progress structure instance. +-/ + +structure SBase where + field1 : Nat +structure S extends SBase where + -- `field2` depends on `field1` so must be inserted after + field2 : Vector Nat field1 + sh : String + longerFieldName : Bool + field3 : Bool + +/-! ## No existing fields -/ +example : S := + {} +--^ codeAction +example : S := {} + --^ codeAction + +example : S := { + +} +--^ codeAction +example : S := + { + + } +--^ codeAction +example : S := + -- VS Code's auto-formatting makes this scenario unlikely, but we test it for completeness + { + } +--^ codeAction +example : S := { +} +--^ codeAction +example : S := { + -- comment in the way +} +--^ codeAction + +/-! ## One field per line, braces not separated -/ +example : S := + { field1 := 0 + field2 := #v[] } + --^ codeAction + +/-! ## One field per line, braces separated -/ +example : S := + { + field1 := 31 + field3 := true + } +--^ codeAction + +/-! ## One field per line, braces separated without initial line break -/ +example : S := { + field1 := 31 + field3 := true +} +--^ codeAction + +/-! ## Many fields per line, braces not separated -/ +example : S := + { field1 := 0, field2 := #v[] } + --^ codeAction + +/-! ## Many fields per line, braces not separated, next field must go on a new line -/ +example : S := + { field1 := 0, sh := "a long string value that forces this line to the maximum column length" } + --^ codeAction + +/-! ## Many fields per line, braces not separated, with an existing line break -/ +example : S := + { field1 := 0, sh := "a long string value that forces this line to the maximum column length", + field2 := #v[] } + --^ codeAction + +/-! ## Ambiguous styling intent -/ +example : S := + { sh := "hi" } + --^ codeAction + +def base : SBase := + ⟨0⟩ + +/-! ## Using `with`, many fields per line -/ +example : S := + { base with field3 := true, sh := "bar" } + --^ codeAction + +/-! ## Using `with`, many fields per line, next field requires a break -/ +example : S := + { base with sh := "a long string value that forces this line near max length", field3 := false } + --^ codeAction + +/-! ## Using `with`, one field per line, no initial line break -/ +example : S := { base with + field1 := 0 + field3 := true +} +--^ codeAction + +/-! ## Using `with`, one field per line, indented post-`with` -/ +example : S := + { base with field1 := 0 + field3 := true } + --^ codeAction + +/-! ## Using `with`, no fields -/ +example : S := + { base with } + --^ codeAction +example : S := + { base with + } +--^ codeAction +example : S := { base with +} +--^ codeAction +example : S := { base with + +} +--^ codeAction + +/-! ## `with` at same indentation as fields -/ +example : S := { + base with + field1 := 0, field2 := #v[], + field3 := true +} +--^ codeAction + +/-! ## With type annotation -/ +example := { + : S +} +--^ codeAction +example := { : S } + --^ codeAction +example := { : S +} +--^ codeAction +example := { + field1 := 1 + : S +} +--^ codeAction +example := + { field1 := 1 + field3 := true : S } + --^ codeAction +example := { field1 := 1 : S } + --^ codeAction + +/-! ## `with` and type annotation -/ +example := + { base with : S} + --^ codeAction +example := { base with + : S +} +--^ codeAction +example := { base with : S + +} +--^ codeAction + +/-! ## Missing constrained field -/ +example : S := + { field2 := #v[] } + --^ codeAction + +/-! ## Missing constrained but not fully determined field -/ +inductive BadDepType : Nat → Type where + | mk : BadDepType (n + 4) +structure BadDepStruct where + n : Nat + bdt : BadDepType n +example : BadDepStruct := + { bdt := .mk } + --^ codeAction + + +structure DateES where + día : Nat + mes : Nat + año : Nat + +/-! ## Multi-byte characters in indentation offset -/ +def números : Nat × Nat := {} + --^ codeAction +def números' : Nat × Nat := { fst := 23 } + --^ codeAction + + +/-! ## Inapplicable syntax -/ + +-- TODO: eventually, we'd like to support `where` +example : S where + --^ codeAction + +example : S where + field2 := #v[42] + --^ codeAction + +section +local macro "a_structure_with" args:(ident "equal_to" term "in_addition_to"?)* : term => do + let fields ← args.raw.mapM fun a => + `(Lean.Parser.Term.structInstField | $(Lean.mkIdent a[0].getId):ident := $(.mk a[2])) + `({ $[$fields]* }) + +example : S := + a_structure_with field1 equal_to 3 in_addition_to sh equal_to "Hello" + --^ codeAction +end diff --git a/tests/lean/interactive/structInstFieldHints.lean.expected.out b/tests/lean/interactive/structInstFieldHints.lean.expected.out new file mode 100644 index 0000000000..26cc102755 --- /dev/null +++ b/tests/lean/interactive/structInstFieldHints.lean.expected.out @@ -0,0 +1,421 @@ +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 20, "character": 3}, + "end": {"line": 20, "character": 3}}, + "newText": + " field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _ "}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 22, "character": 16}, + "end": {"line": 22, "character": 16}}, + "newText": + " field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _ "}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 26, "character": 0}, + "end": {"line": 26, "character": 0}}, + "newText": + " field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 31, "character": 0}, + "end": {"line": 31, "character": 0}}, + "newText": + " field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 36, "character": 3}, + "end": {"line": 36, "character": 3}}, + "newText": + "\n field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 39, "character": 16}, + "end": {"line": 39, "character": 16}}, + "newText": + "\n field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 42, "character": 16}, + "end": {"line": 42, "character": 16}}, + "newText": + "\n field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 50, "character": 18}, + "end": {"line": 50, "character": 18}}, + "newText": + "\n sh := _\n longerFieldName := _\n field3 := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 57, "character": 18}, + "end": {"line": 57, "character": 18}}, + "newText": + "\n field2 := _\n sh := _\n longerFieldName := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 64, "character": 16}, + "end": {"line": 64, "character": 16}}, + "newText": "\n field2 := _\n sh := _\n longerFieldName := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 70, "character": 31}, + "end": {"line": 70, "character": 31}}, + "newText": ", sh := _, longerFieldName := _, field3 := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 75, "character": 95}, + "end": {"line": 75, "character": 95}}, + "newText": ",\n field2 := _, longerFieldName := _, field3 := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 81, "character": 18}, + "end": {"line": 81, "character": 18}}, + "newText": ", longerFieldName := _, field3 := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 86, "character": 14}, + "end": {"line": 86, "character": 14}}, + "newText": + "\n field1 := _\n field2 := _\n longerFieldName := _\n field3 := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 94, "character": 41}, + "end": {"line": 94, "character": 41}}, + "newText": ", field2 := _, longerFieldName := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 99, "character": 96}, + "end": {"line": 99, "character": 96}}, + "newText": ",\n field2 := _, longerFieldName := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 105, "character": 16}, + "end": {"line": 105, "character": 16}}, + "newText": "\n field2 := _\n sh := _\n longerFieldName := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 112, "character": 28}, + "end": {"line": 112, "character": 28}}, + "newText": + "\n field2 := _\n sh := _\n longerFieldName := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 117, "character": 13}, + "end": {"line": 117, "character": 13}}, + "newText": + "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 120, "character": 13}, + "end": {"line": 120, "character": 13}}, + "newText": + "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 123, "character": 26}, + "end": {"line": 123, "character": 26}}, + "newText": + "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 127, "character": 0}, + "end": {"line": 127, "character": 0}}, + "newText": + " field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 135, "character": 16}, + "end": {"line": 135, "character": 16}}, + "newText": ", sh := _, longerFieldName := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 140, "character": 12}, + "end": {"line": 140, "character": 12}}, + "newText": + "\n field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 144, "character": 12}, + "end": {"line": 144, "character": 12}}, + "newText": + " field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _ "}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 146, "character": 12}, + "end": {"line": 146, "character": 12}}, + "newText": + "\n field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 150, "character": 13}, + "end": {"line": 150, "character": 13}}, + "newText": + "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 156, "character": 18}, + "end": {"line": 156, "character": 18}}, + "newText": + "\n field2 := _\n sh := _\n longerFieldName := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 158, "character": 24}, + "end": {"line": 158, "character": 24}}, + "newText": + "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 163, "character": 13}, + "end": {"line": 163, "character": 13}}, + "newText": + "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 165, "character": 22}, + "end": {"line": 165, "character": 22}}, + "newText": + "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 169, "character": 22}, + "end": {"line": 169, "character": 22}}, + "newText": + "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 176, "character": 18}, + "end": {"line": 176, "character": 18}}, + "newText": + "\n field1 := 0\n sh := _\n longerFieldName := _\n field3 := _"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 186, "character": 14}, + "end": {"line": 186, "character": 14}}, + "newText": "\n n := ?_ + 4"}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 196, "character": 28}, + "end": {"line": 196, "character": 28}}, + "newText": " fst := _\n snd := _ "}]}]}} +{"title": "Add missing fields", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 198, "character": 39}, + "end": {"line": 198, "character": 39}}, + "newText": "\n snd := _"}]}]}} diff --git a/tests/lean/run/461b.lean b/tests/lean/run/461b.lean index a6353cf3db..a6bce6ed4d 100644 --- a/tests/lean/run/461b.lean +++ b/tests/lean/run/461b.lean @@ -10,7 +10,7 @@ structure BarS extends FooS where def f (x : Nat) : BarS := { x, y := x, h' := rfl } -/-- error: cannot synthesize placeholder for field 'h' -/ +/-- error: Cannot synthesize placeholder for field `h` -/ #guard_msgs in example (x : Nat) : BarS := { x, h' := rfl, .. } diff --git a/tests/lean/run/structInst.lean b/tests/lean/run/structInst.lean index 32d40a21ee..5a560cd8a3 100644 --- a/tests/lean/run/structInst.lean +++ b/tests/lean/run/structInst.lean @@ -60,7 +60,12 @@ structure C extends B where -- This first example does not work because the default values at `C` are the only ones considered. /-- -error: fields missing: 'y', 'z' +error: Fields missing: `y`, `z` + +Hint: Add missing fields: + ⏎ + ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲y̲ ̲:̲=̲ ̲_̲ + ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲z̲ ̲:̲=̲ ̲_̲ --- info: { x := 1, y := sorry, z := sorry } : C -/ @@ -71,7 +76,7 @@ info: { x := 1, y := sorry, z := sorry } : 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' -/ +/-- error: Fields missing: `y`, `z` -/ #guard_msgs in def test1 : C where x := 1 @@ -220,10 +225,14 @@ structure S where variable (x : Fin 3) /-- -error: fields missing: 'n' +error: Fields missing: `n` -field 'n' must be explicitly provided, its synthesized value is +Field `n` must be explicitly provided; its synthesized value is 3 + +Hint: Add missing fields: + ⏎ + ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲n̲ ̲:̲=̲ ̲3̲ --- info: { n := 3, m := x } : S -/ diff --git a/tests/lean/semicolonOrLinebreak.lean.expected.out b/tests/lean/semicolonOrLinebreak.lean.expected.out index 4f7219e6c4..dcef2c05ca 100644 --- a/tests/lean/semicolonOrLinebreak.lean.expected.out +++ b/tests/lean/semicolonOrLinebreak.lean.expected.out @@ -1,5 +1,5 @@ semicolonOrLinebreak.lean:2:12: error: expected ';' or line break -semicolonOrLinebreak.lean:9:31-10:8: error: fields missing: 'y' +semicolonOrLinebreak.lean:9:31-10:8: error: Fields missing: `y` semicolonOrLinebreak.lean:10:8-10:9: error: unexpected identifier; expected command semicolonOrLinebreak.lean:20:4-20:7: error: Function expected at x diff --git a/tests/lean/setLit.lean.expected.out b/tests/lean/setLit.lean.expected.out index 4c58eef7d5..566336deb5 100644 --- a/tests/lean/setLit.lean.expected.out +++ b/tests/lean/setLit.lean.expected.out @@ -4,7 +4,10 @@ setLit.lean:22:19-22:21: error: overloaded, errors Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command. - fields missing: 'data' + Fields missing: `data` + + Hint: Add missing fields: + ̲d̲a̲t̲a̲ ̲:̲=̲ ̲_̲ ̲ setLit.lean:24:31-24:38: error: overloaded, errors failed to synthesize Singleton Nat String