From ff90459fd207268cf6b2c2a35ba1c031acb8c545 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 9 Dec 2021 06:05:55 -0800 Subject: [PATCH] feat: add `Lean.Elab.Term.getMVarErrorInfo?` --- src/Lean/Elab/Term.lean | 38 ++-- tests/lean/217.lean.expected.out | 6 +- tests/lean/450.lean.expected.out | 2 +- tests/lean/holeErrors.lean.expected.out | 4 +- tests/lean/implicitTypePos.lean.expected.out | 2 +- tests/lean/jason1.lean.expected.out | 196 +++++++++--------- .../lean/multiConstantError.lean.expected.out | 4 +- 7 files changed, 129 insertions(+), 123 deletions(-) diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 7245e572e0..d003a2e1af 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -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. -/ diff --git a/tests/lean/217.lean.expected.out b/tests/lean/217.lean.expected.out index 1d06e22a0c..2f072d2154 100644 --- a/tests/lean/217.lean.expected.out +++ b/tests/lean/217.lean.expected.out @@ -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 diff --git a/tests/lean/450.lean.expected.out b/tests/lean/450.lean.expected.out index 8017fe9571..2ba2013d9e 100644 --- a/tests/lean/450.lean.expected.out +++ b/tests/lean/450.lean.expected.out @@ -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 diff --git a/tests/lean/holeErrors.lean.expected.out b/tests/lean/holeErrors.lean.expected.out index 3acaf5a8e6..bda9d8befa 100644 --- a/tests/lean/holeErrors.lean.expected.out +++ b/tests/lean/holeErrors.lean.expected.out @@ -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 diff --git a/tests/lean/implicitTypePos.lean.expected.out b/tests/lean/implicitTypePos.lean.expected.out index 67464413a8..7491818549 100644 --- a/tests/lean/implicitTypePos.lean.expected.out +++ b/tests/lean/implicitTypePos.lean.expected.out @@ -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 diff --git a/tests/lean/jason1.lean.expected.out b/tests/lean/jason1.lean.expected.out index 2af7ac48fb..b150b2d7c9 100644 --- a/tests/lean/jason1.lean.expected.out +++ b/tests/lean/jason1.lean.expected.out @@ -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 diff --git a/tests/lean/multiConstantError.lean.expected.out b/tests/lean/multiConstantError.lean.expected.out index 824eb1ee1d..6ff26c39b1 100644 --- a/tests/lean/multiConstantError.lean.expected.out +++ b/tests/lean/multiConstantError.lean.expected.out @@ -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 `(α : _)`, `(β : _)`