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.
This commit is contained in:
jrr6
GitHub
parent
442ef6e64c
commit
119854e248
10 changed files with 849 additions and 13 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
171
src/Lean/Elab/StructInstHint.lean
Normal file
171
src/Lean/Elab/StructInstHint.lean
Normal file
|
|
@ -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
|
||||
|
|
@ -1 +1 @@
|
|||
instance1.lean:6:24-10:0: error: fields missing: 'pure', 'bind'
|
||||
instance1.lean:6:24-10:0: error: Fields missing: `pure`, `bind`
|
||||
|
|
|
|||
222
tests/lean/interactive/structInstFieldHints.lean
Normal file
222
tests/lean/interactive/structInstFieldHints.lean
Normal file
|
|
@ -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
|
||||
421
tests/lean/interactive/structInstFieldHints.lean.expected.out
Normal file
421
tests/lean/interactive/structInstFieldHints.lean.expected.out
Normal file
|
|
@ -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 := _"}]}]}}
|
||||
|
|
@ -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, .. }
|
||||
|
|
|
|||
|
|
@ -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
|
||||
-/
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue