max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add Lean.Elab.Term.getMVarErrorInfo?

Browse source
This commit is contained in:
Leonardo de Moura 2021-12-09 06:05:55 -08:00
parent 914f181641
commit ff90459fd2
7 changed files with 129 additions and 123 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

38
src/Lean/Elab/Term.lean
View file

@ -92,6 +92,7 @@ inductive MVarErrorKind where
| implicitArg (ctx : Expr)
| hole
| custom (msgData : MessageData)
deriving Inhabited
instance : ToString MVarErrorKind where
toString
@ -103,6 +104,7 @@ structure MVarErrorInfo where
mvarId : MVarId
ref : Syntax
kind : MVarErrorKind
deriving Inhabited
structure LetRecToLift where
ref : Syntax
@ -119,7 +121,7 @@ structure LetRecToLift where
structure State where
levelNames : List Name := []
syntheticMVars : List SyntheticMVarDecl := []
mvarErrorInfos : List MVarErrorInfo := []
mvarErrorInfos : MVarIdMap MVarErrorInfo := {}
messages : MessageLog := {}
letRecsToLift : List LetRecToLift := []
infoState : InfoState := {}
@ -378,13 +380,16 @@ def registerSyntheticMVarWithCurrRef (mvarId : MVarId) (kind : SyntheticMVarKind
registerSyntheticMVar (← getRef) mvarId kind
def registerMVarErrorHoleInfo (mvarId : MVarId) (ref : Syntax) : TermElabM Unit := do
modify fun s => { s with mvarErrorInfos := { mvarId := mvarId, ref := ref, kind := MVarErrorKind.hole } :: s.mvarErrorInfos }
modify fun s => { s with mvarErrorInfos := s.mvarErrorInfos.insert mvarId { mvarId := mvarId, ref := ref, kind := MVarErrorKind.hole } }
def registerMVarErrorImplicitArgInfo (mvarId : MVarId) (ref : Syntax) (app : Expr) : TermElabM Unit := do
modify fun s => { s with mvarErrorInfos := { mvarId := mvarId, ref := ref, kind := MVarErrorKind.implicitArg app } :: s.mvarErrorInfos }
modify fun s => { s with mvarErrorInfos := s.mvarErrorInfos.insert mvarId { mvarId := mvarId, ref := ref, kind := MVarErrorKind.implicitArg app } }
def registerMVarErrorCustomInfo (mvarId : MVarId) (ref : Syntax) (msgData : MessageData) : TermElabM Unit := do
modify fun s => { s with mvarErrorInfos := { mvarId := mvarId, ref := ref, kind := MVarErrorKind.custom msgData } :: s.mvarErrorInfos }
modify fun s => { s with mvarErrorInfos := s.mvarErrorInfos.insert mvarId { mvarId := mvarId, ref := ref, kind := MVarErrorKind.custom msgData } }
def getMVarErrorInfo? (mvarId : MVarId) : TermElabM (Option MVarErrorInfo) := do
return (← get).mvarErrorInfos.find? mvarId
def registerCustomErrorIfMVar (e : Expr) (ref : Syntax) (msgData : MessageData) : TermElabM Unit :=
match e.getAppFn with
@ -433,22 +438,23 @@ def logUnassignedUsingErrorInfos (pendingMVarIds : Array MVarId) (extraMsg? : Op
let hasOtherErrors := s.messages.hasErrors
let mut hasNewErrors := false
let mut alreadyVisited : MVarIdSet := {}
for mvarErrorInfo in s.mvarErrorInfos do
let mut errors : Array MVarErrorInfo := #[]
for (_, mvarErrorInfo) in s.mvarErrorInfos do
let mvarId := mvarErrorInfo.mvarId
unless alreadyVisited.contains mvarId do
alreadyVisited := alreadyVisited.insert mvarId
let foundError ← withMVarContext mvarId do
/- The metavariable `mvarErrorInfo.mvarId` may have been assigned or
delayed assigned to another metavariable that is unassigned. -/
let mvarDeps ← getMVars (mkMVar mvarId)
if mvarDeps.any pendingMVarIds.contains then do
unless hasOtherErrors do
mvarErrorInfo.logError extraMsg?
pure true
else
pure false
if foundError then
/- The metavariable `mvarErrorInfo.mvarId` may have been assigned or
delayed assigned to another metavariable that is unassigned. -/
let mvarDeps ← getMVars (mkMVar mvarId)
if mvarDeps.any pendingMVarIds.contains then do
unless hasOtherErrors do
errors := errors.push mvarErrorInfo
hasNewErrors := true
-- To sort the errors by position use
-- let sortedErrors := errors.qsort fun e₁ e₂ => e₁.ref.getPos?.getD 0 < e₂.ref.getPos?.getD 0
for error in errors do
withMVarContext error.mvarId do
error.logError extraMsg?
return hasNewErrors
/-- Ensure metavariables registered using `registerMVarErrorInfos` (and used in the given declaration) have been assigned. -/

6
tests/lean/217.lean.expected.out
View file

@ -1,6 +1,6 @@
217.lean:5:30-5:31: error: don't know how to synthesize placeholder
context:
⊢ CoreM Unit
217.lean:5:28-5:29: error: don't know how to synthesize placeholder
context:
⊢ CoreM Unit → Name → ConstantInfo → CoreM Unit
217.lean:5:30-5:31: error: don't know how to synthesize placeholder
context:
⊢ CoreM Unit

2
tests/lean/450.lean.expected.out
View file

@ -1,4 +1,4 @@
450.lean:2:6-2:7: error: failed to infer 'let' declaration type
450.lean:2:11-2:12: error: don't know how to synthesize placeholder
context:
⊢ ?m
450.lean:2:6-2:7: error: failed to infer 'let' declaration type

4
tests/lean/holeErrors.lean.expected.out
View file

@ -1,8 +1,8 @@
holeErrors.lean:3:7-3:12: error: failed to infer definition type
holeErrors.lean:3:10-3:12: error: don't know how to synthesize implicit argument
@id ?m
context:
⊢ Sort u_1
holeErrors.lean:3:7-3:12: error: failed to infer definition type
holeErrors.lean:5:9-5:10: error: failed to infer definition type
when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed
holeErrors.lean:8:9-8:11: error: don't know how to synthesize implicit argument
@ -13,8 +13,8 @@ holeErrors.lean:8:4-8:5: error: failed to infer 'let' declaration type
holeErrors.lean:7:7-9:1: error: failed to infer definition type
holeErrors.lean:11:11-11:15: error: failed to infer definition type
holeErrors.lean:11:8-11:9: error: failed to infer binder type
holeErrors.lean:13:15-13:19: error: failed to infer definition type
holeErrors.lean:13:12-13:13: error: failed to infer binder type
holeErrors.lean:13:15-13:19: error: failed to infer definition type
holeErrors.lean:16:4-16:5: error: failed to infer binder type
holeErrors.lean:15:7-16:10: error: failed to infer definition type
holeErrors.lean:19:13-19:15: error: don't know how to synthesize implicit argument

2
tests/lean/implicitTypePos.lean.expected.out
View file

@ -1,5 +1,5 @@
implicitTypePos.lean:1:8-1:9: error: failed to infer binder type
implicitTypePos.lean:1:6-1:7: error: failed to infer binder type
implicitTypePos.lean:1:8-1:9: error: failed to infer binder type
implicitTypePos.lean:3:9-3:10: error: failed to infer binder type
implicitTypePos.lean:5:9-5:10: error: failed to infer binder type
implicitTypePos.lean:7:10-7:11: error: failed to infer binder type

196
tests/lean/jason1.lean.expected.out
View file

@ -1,3 +1,101 @@
jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
x✝ : G
⊢ G
jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
x✝ : G
⊢ G
jason1.lean:48:100-48:117: error: don't know how to synthesize implicit argument
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
x✝ : G
⊢ G
jason1.lean:48:119-48:124: error: don't know how to synthesize implicit argument
@EGrfl
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
x✝ : G
⊢ G
jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
@TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
x✝ : G
⊢ G
jason1.lean:48:125-48:130: error: don't know how to synthesize implicit argument
@EGrfl
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
x✝ : G
⊢ G
jason1.lean:48:41-48:130: error: don't know how to synthesize implicit argument
@TySyntaxLayer.arrow G T EG getCtx
(getCtx
@ -33,101 +131,3 @@ TAlgebra : TySyntaxLayer G T EG getCtx → T
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
x✝ : G
⊢ G
jason1.lean:48:125-48:130: error: don't know how to synthesize implicit argument
@EGrfl
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
x✝ : G
⊢ G
jason1.lean:48:119-48:124: error: don't know how to synthesize implicit argument
@EGrfl
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝))))
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
x✝ : G
⊢ G
jason1.lean:48:100-48:117: error: don't know how to synthesize implicit argument
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
x✝ : G
⊢ G
jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
x✝ : G
⊢ G
jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
x✝ : G
⊢ G
jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
@TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep x✝¹ x✝)
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
x✝ : G
⊢ G

4
tests/lean/multiConstantError.lean.expected.out
View file

@ -1,6 +1,6 @@
multiConstantError.lean:1:13-1:14: error: failed to infer binder type
recall that you cannot declare multiple constants in a single declaration. The identifier(s) `b`, `c` are being interpreted as parameters `(b : _)`, `(c : _)`
multiConstantError.lean:1:11-1:12: error: failed to infer binder type
recall that you cannot declare multiple constants in a single declaration. The identifier(s) `b`, `c` are being interpreted as parameters `(b : _)`, `(c : _)`
multiConstantError.lean:1:13-1:14: error: failed to infer binder type
recall that you cannot declare multiple constants in a single declaration. The identifier(s) `b`, `c` are being interpreted as parameters `(b : _)`, `(c : _)`
multiConstantError.lean:3:11-3:12: error: failed to infer binder type
recall that you cannot declare multiple constants in a single declaration. The identifier(s) `α`, `β` are being interpreted as parameters `(α : _)`, `(β : _)`