Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: have autoparams report parameter/field on failure #5474

Merged
merged 5 commits into from
Sep 27, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 6 additions & 2 deletions src/Lean/Elab/App.lean
Original file line number Diff line number Diff line change
Expand Up @@ -584,7 +584,6 @@ mutual
match evalSyntaxConstant env opts tacticDecl with
| Except.error err => throwError err
| Except.ok tacticSyntax =>
-- TODO(Leo): does this work correctly for tactic sequences?
let tacticBlock ← `(by $(⟨tacticSyntax⟩))
/-
We insert position information from the current ref into `stx` everywhere, simulating this being
Expand All @@ -596,7 +595,12 @@ mutual
-/
let info := (← getRef).getHeadInfo
let tacticBlock := tacticBlock.raw.rewriteBottomUp (·.setInfo info)
let argNew := Arg.stx tacticBlock
let mvar ← mkTacticMVar argType.consumeTypeAnnotations tacticBlock (.autoParam argName)
-- Note(kmill): We are adding terminfo to simulate a previous implementation that elaborated `tacticBlock`.
-- We should look into removing this since terminfo for synthetic syntax is suspect,
-- but we noted it was necessary to preserve the behavior of the unused variable linter.
addTermInfo' tacticBlock mvar
let argNew := Arg.expr mvar
propagateExpectedType argNew
elabAndAddNewArg argName argNew
main
Expand Down
18 changes: 1 addition & 17 deletions src/Lean/Elab/BuiltinTerm.lean
Original file line number Diff line number Diff line change
Expand Up @@ -150,26 +150,10 @@ private def getMVarFromUserName (ident : Syntax) : MetaM Expr := do
elabTerm b expectedType?
| _ => throwUnsupportedSyntax

private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr := do
let mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque
let mvarId := mvar.mvarId!
let ref ← getRef
registerSyntheticMVar ref mvarId <| SyntheticMVarKind.tactic tacticCode (← saveContext)
return mvar

register_builtin_option debug.byAsSorry : Bool := {
defValue := false
group := "debug"
descr := "replace `by ..` blocks with `sorry` IF the expected type is a proposition"
}

@[builtin_term_elab byTactic] def elabByTactic : TermElab := fun stx expectedType? => do
match expectedType? with
| some expectedType =>
if ← pure (debug.byAsSorry.get (← getOptions)) <&&> isProp expectedType then
mkSorry expectedType false
else
mkTacticMVar expectedType stx
mkTacticMVar expectedType stx .term
| none =>
tryPostpone
throwError ("invalid 'by' tactic, expected type has not been provided")
Expand Down
7 changes: 6 additions & 1 deletion src/Lean/Elab/StructInst.lean
Original file line number Diff line number Diff line change
Expand Up @@ -682,7 +682,12 @@ private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : Term
-- We add info to get reliable positions for messages from evaluating the tactic script.
let info := field.ref.getHeadInfo
let stx := stx.raw.rewriteBottomUp (·.setInfo info)
cont (← elabTermEnsuringType stx (d.getArg! 0).consumeTypeAnnotations) field
let type := (d.getArg! 0).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 aformentioned `processExplicitArg` for a comment about this.)
addTermInfo' stx mvar
cont mvar field
| _ =>
if bi == .instImplicit then
let val ← withRef field.ref <| mkFreshExprMVar d .synthetic
Expand Down
27 changes: 21 additions & 6 deletions src/Lean/Elab/SyntheticMVars.lean
Original file line number Diff line number Diff line change
Expand Up @@ -316,6 +316,18 @@ def PostponeBehavior.ofBool : Bool → PostponeBehavior
| true => .yes
| false => .no

private def TacticMVarKind.logError (tacticCode : Syntax) (kind : TacticMVarKind) : TermElabM Unit := do
match kind with
| term => pure ()
| autoParam argName => logErrorAt tacticCode m!"could not synthesize default value for parameter '{argName}' using tactics"
| fieldAutoParam fieldName structName => logErrorAt tacticCode m!"could not synthesize default value for field '{fieldName}' of '{structName}' using tactics"

private def TacticMVarKind.maybeWithoutRecovery (kind : TacticMVarKind) (m : TacticM α) : TacticM α := do
if kind matches .autoParam .. | .fieldAutoParam .. then
withoutErrToSorry <| Tactic.withoutRecover <| m
else
m

mutual

/--
Expand All @@ -325,7 +337,7 @@ mutual

If `report := false`, then `runTactic` will not capture exceptions nor will report unsolved goals. Unsolved goals become exceptions.
-/
partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) (report := true) : TermElabM Unit := withoutAutoBoundImplicit do
partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) (kind : TacticMVarKind) (report := true) : TermElabM Unit := withoutAutoBoundImplicit do
instantiateMVarDeclMVars mvarId
/-
TODO: consider using `runPendingTacticsAt` at `mvarId` local context and target type.
Expand All @@ -342,7 +354,7 @@ mutual
in more complicated scenarios.
-/
tryCatchRuntimeEx
(do let remainingGoals ← withInfoHole mvarId <| Tactic.run mvarId do
(do let remainingGoals ← withInfoHole mvarId <| Tactic.run mvarId <| kind.maybeWithoutRecovery do
withTacticInfoContext tacticCode do
-- also put an info node on the `by` keyword specifically -- the token may be `canonical` and thus shown in the info
-- view even though it is synthetic while a node like `tacticCode` never is (#1990)
Expand All @@ -354,10 +366,13 @@ mutual
synthesizeSyntheticMVars (postpone := .no)
unless remainingGoals.isEmpty do
if report then
kind.logError tacticCode
reportUnsolvedGoals remainingGoals
else
throwError "unsolved goals\n{goalsToMessageData remainingGoals}")
fun ex => do
if report then
kind.logError tacticCode
if report && (← read).errToSorry then
for mvarId in (← getMVars (mkMVar mvarId)) do
mvarId.admit
Expand Down Expand Up @@ -385,10 +400,10 @@ mutual
return false
-- NOTE: actual processing at `synthesizeSyntheticMVarsAux`
| .postponed savedContext => resumePostponed savedContext mvarSyntheticDecl.stx mvarId postponeOnError
| .tactic tacticCode savedContext =>
| .tactic tacticCode savedContext kind =>
withSavedContext savedContext do
if runTactics then
runTactic mvarId tacticCode
runTactic mvarId tacticCode kind
return true
else
return false
Expand Down Expand Up @@ -529,9 +544,9 @@ the result of a tactic block.
def runPendingTacticsAt (e : Expr) : TermElabM Unit := do
for mvarId in (← getMVars e) do
let mvarId ← getDelayedMVarRoot mvarId
if let some { kind := .tactic tacticCode savedContext, .. } ← getSyntheticMVarDecl? mvarId then
if let some { kind := .tactic tacticCode savedContext kind, .. } ← getSyntheticMVarDecl? mvarId then
withSavedContext savedContext do
runTactic mvarId tacticCode
runTactic mvarId tacticCode kind
markAsResolved mvarId

builtin_initialize
Expand Down
2 changes: 1 addition & 1 deletion src/Lean/Elab/Tactic/Simp.lean
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ def tacticToDischarge (tacticCode : Syntax) : TacticM (IO.Ref Term.State × Simp
-/
withoutModifyingStateWithInfoAndMessages do
Term.withSynthesize (postpone := .no) do
Term.runTactic (report := false) mvar.mvarId! tacticCode
Term.runTactic (report := false) mvar.mvarId! tacticCode .term
let result ← instantiateMVars mvar
if result.hasExprMVar then
return none
Expand Down
31 changes: 30 additions & 1 deletion src/Lean/Elab/Term.lean
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,15 @@ structure SavedContext where
errToSorry : Bool
levelNames : List Name

/-- The kind of a tactic metavariable, used for additional error reporting. -/
inductive TacticMVarKind
/-- Standard tactic metavariable, arising from `by ...` syntax. -/
| term
/-- Tactic metavariable arising from an autoparam for a function application. -/
| autoParam (argName : Name)
/-- Tactic metavariable arising from an autoparam for a structure field. -/
| fieldAutoParam (fieldName structName : Name)

/-- We use synthetic metavariables as placeholders for pending elaboration steps. -/
inductive SyntheticMVarKind where
/--
Expand All @@ -43,7 +52,7 @@ inductive SyntheticMVarKind where
Otherwise, we generate the error `("type mismatch" ++ e ++ "has type" ++ eType ++ "but it is expected to have type" ++ expectedType)` -/
| coe (header? : Option String) (expectedType : Expr) (e : Expr) (f? : Option Expr)
/-- Use tactic to synthesize value for metavariable. -/
| tactic (tacticCode : Syntax) (ctx : SavedContext)
| tactic (tacticCode : Syntax) (ctx : SavedContext) (kind : TacticMVarKind)
/-- Metavariable represents a hole whose elaboration has been postponed. -/
| postponed (ctx : SavedContext)
deriving Inhabited
Expand Down Expand Up @@ -1191,6 +1200,26 @@ private def postponeElabTermCore (stx : Syntax) (expectedType? : Option Expr) :
def getSyntheticMVarDecl? (mvarId : MVarId) : TermElabM (Option SyntheticMVarDecl) :=
return (← get).syntheticMVars.find? mvarId

register_builtin_option debug.byAsSorry : Bool := {
defValue := false
group := "debug"
descr := "replace `by ..` blocks with `sorry` IF the expected type is a proposition"
}

/--
Creates a new metavariable of type `type` that will be synthesized using the tactic code.
The `tacticCode` syntax is the full `by ..` syntax.
-/
def mkTacticMVar (type : Expr) (tacticCode : Syntax) (kind : TacticMVarKind) : TermElabM Expr := do
if ← pure (debug.byAsSorry.get (← getOptions)) <&&> isProp type then
mkSorry type false
else
let mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque
let mvarId := mvar.mvarId!
let ref ← getRef
registerSyntheticMVar ref mvarId <| SyntheticMVarKind.tactic tacticCode (← saveContext) kind
return mvar

/--
Create an auxiliary annotation to make sure we create an `Info` even if `e` is a metavariable.
See `mkTermInfo`.
Expand Down
20 changes: 20 additions & 0 deletions tests/lean/interactive/4880.lean.expected.out
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,16 @@
"uri": "file:///4880.lean",
"diagnostics":
[{"source": "Lean 4",
"severity": 1,
"range":
{"start": {"line": 16, "character": 12},
"end": {"line": 16, "character": 17}},
"message":
"could not synthesize default value for field 'h1' of 'B' using tactics",
"fullRange":
{"start": {"line": 16, "character": 12},
"end": {"line": 16, "character": 17}}},
{"source": "Lean 4",
"severity": 1,
"range":
{"start": {"line": 16, "character": 12},
Expand All @@ -11,6 +21,16 @@
"fullRange":
{"start": {"line": 16, "character": 12},
"end": {"line": 16, "character": 17}}},
{"source": "Lean 4",
"severity": 1,
"range":
{"start": {"line": 22, "character": 17},
"end": {"line": 22, "character": 20}},
"message":
"could not synthesize default value for parameter '_h1' using tactics",
"fullRange":
{"start": {"line": 22, "character": 17},
"end": {"line": 22, "character": 20}}},
{"source": "Lean 4",
"severity": 1,
"range":
Expand Down
33 changes: 33 additions & 0 deletions tests/lean/run/autoparam.lean
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
/-!
# Testing the autoparam feature
-/

def f (x y : Nat) (h : x = y := by assumption) : Nat :=
x + x
Expand All @@ -13,3 +16,33 @@ x + x

#check fun x => f2 x x
#check fun x => f3 x x

/--
error: could not synthesize default value for parameter 'h' using tactics
---
error: tactic 'assumption' failed
⊢ 1 = 2
-/
#guard_msgs in example := f 1 2

/-!
From #2950, field autoparam should mention which field failed.
-/

structure Foo where
val : String
len : Nat := val.length
inv : val.length = len := by next => decide

/--
error: could not synthesize default value for field 'inv' of 'Foo' using tactics
---
error: tactic 'decide' proved that the proposition
"abc".length = 5
is false
-/
#guard_msgs in
def test2 : Foo := {
val := "abc"
len := 5
}
4 changes: 4 additions & 0 deletions tests/lean/run/mergeSort.lean
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,8 @@ inductive NoLE
| mk : NoLE

/--
error: could not synthesize default value for parameter 'le' using tactics
---
error: failed to synthesize
LE NoLE
Additional diagnostic information may be available using the `set_option diagnostics true` command.
Expand All @@ -51,6 +53,8 @@ instance : LE UndecidableLE where
le := fun _ _ => true

/--
error: could not synthesize default value for parameter 'le' using tactics
---
error: type mismatch
a ≤ b
has type
Expand Down
Loading