From 8d6ae6cc323015ca66e6328f431b72cd40a9b217 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Tue, 2 May 2023 19:03:05 +0200 Subject: [PATCH] move location to the start of type errors --- lib/Quox/Typing/Error.idr | 93 ++++++++++++++++++++++++++------------- 1 file changed, 62 insertions(+), 31 deletions(-) diff --git a/lib/Quox/Typing/Error.idr b/lib/Quox/Typing/Error.idr index b786ce6..4211504 100644 --- a/lib/Quox/Typing/Error.idr +++ b/lib/Quox/Typing/Error.idr @@ -111,6 +111,35 @@ ErrorEff : Type -> Type ErrorEff = Except Error +export +Located Error where + (ExpectedTYPE loc _ _).loc = loc + (ExpectedPi loc _ _).loc = loc + (ExpectedSig loc _ _).loc = loc + (ExpectedEnum loc _ _).loc = loc + (ExpectedEq loc _ _).loc = loc + (ExpectedNat loc _ _).loc = loc + (ExpectedBOX loc _ _).loc = loc + (BadUniverse loc _ _).loc = loc + (TagNotIn loc _ _).loc = loc + (BadCaseEnum loc _ _).loc = loc + (BadQtys loc _ _ _).loc = loc + (ClashT loc _ _ _ _ _).loc = loc + (ClashTy loc _ _ _ _).loc = loc + (ClashE loc _ _ _ _).loc = loc + (ClashU loc _ _ _).loc = loc + (ClashQ loc _ _).loc = loc + (NotInScope loc _).loc = loc + (NotType loc _ _).loc = loc + (WrongType loc _ _ _).loc = loc + (MissingEnumArm loc _ _).loc = loc + (WhileChecking _ _ _ _ err).loc = err.loc + (WhileCheckingTy _ _ _ err).loc = err.loc + (WhileInferring _ _ _ err).loc = err.loc + (WhileComparingT _ _ _ _ _ err).loc = err.loc + (WhileComparingE _ _ _ _ err).loc = err.loc + + ||| whether the error is surrounded in some context ||| (e.g. "while checking s : A, …") public export @@ -240,90 +269,87 @@ parameters (unicode : Bool) "uses variables", commaList $ (TV . name) <$> ns, "with quantities", commaList qs] - -- [todo] only show some contexts, probably export - prettyError : (showContext : Bool) -> Error -> Doc HL - prettyError showContext = \case - ExpectedTYPE loc ctx s => - sep [prettyLoc loc <++> "expected a type universe, but got", termn ctx s] + prettyErrorNoLoc : (showContext : Bool) -> Error -> Doc HL + prettyErrorNoLoc showContext = \case + ExpectedTYPE _ ctx s => + sep ["expected a type universe, but got", termn ctx s] ExpectedPi loc ctx s => - sep [prettyLoc loc <++> "expected a function type, but got", termn ctx s] + sep ["expected a function type, but got", termn ctx s] ExpectedSig loc ctx s => - sep [prettyLoc loc <++> "expected a pair type, but got", termn ctx s] + sep ["expected a pair type, but got", termn ctx s] ExpectedEnum loc ctx s => - sep [prettyLoc loc <++> "expected an enumeration type, but got", - termn ctx s] + sep ["expected an enumeration type, but got", termn ctx s] ExpectedEq loc ctx s => - sep [prettyLoc loc <++> "expected an equality type, but got", termn ctx s] + sep ["expected an equality type, but got", termn ctx s] ExpectedNat loc ctx s {d, n} => - sep [prettyLoc loc <++> "expected the type", + sep ["expected the type", pretty0 unicode $ Nat noLoc {d, n}, "but got", termn ctx s] ExpectedBOX loc ctx s => - sep [prettyLoc loc <++> "expected a box type, but got", termn ctx s] + sep ["expected a box type, but got", termn ctx s] BadUniverse loc k l => - sep [prettyLoc loc <++> "the universe level", prettyUniverse k, + sep ["the universe level", prettyUniverse k, "is not strictly less than", prettyUniverse l] TagNotIn loc tag set => - sep [hsep [prettyLoc loc, "tag", prettyTag tag, "is not contained in"], + sep [hsep ["tag", prettyTag tag, "is not contained in"], termn empty (Enum set noLoc)] BadCaseEnum loc type arms => - sep [prettyLoc loc <++> "case expression has head of type", + sep ["case expression has head of type", termn empty (Enum type noLoc), "but cases for", termn empty (Enum arms noLoc)] BadQtys loc what ctx arms => hang 4 $ sep $ - hsep [prettyLoc loc, "inconsistent variable usage in", fromString what] + hsep ["inconsistent variable usage in", fromString what] :: printCaseQtys ctx ctx.tnames arms ClashT loc ctx mode ty s t => inEContext ctx $ - sep [prettyLoc loc <++> "the term", termn ctx.names0 s, + sep ["the term", termn ctx.names0 s, hsep ["is not", prettyMode mode], termn ctx.names0 t, "at type", termn ctx.names0 ty] ClashTy loc ctx mode a b => inEContext ctx $ - sep [prettyLoc loc <++> "the type", termn ctx.names0 a, + sep ["the type", termn ctx.names0 a, hsep ["is not", prettyMode mode], termn ctx.names0 b] ClashE loc ctx mode e f => inEContext ctx $ - sep [prettyLoc loc <++> "the term", termn ctx.names0 $ E e, + sep ["the term", termn ctx.names0 $ E e, hsep ["is not", prettyMode mode], termn ctx.names0 $ E f] ClashU loc mode k l => - sep [prettyLoc loc <++> "the universe level", prettyUniverse k, + sep ["the universe level", prettyUniverse k, hsep ["is not", prettyMode mode], prettyUniverse l] ClashQ loc pi rh => - sep [prettyLoc loc <++> "the quantity", pretty0 unicode pi, + sep ["the quantity", pretty0 unicode pi, "is not equal to", pretty0 unicode rh] NotInScope loc x => - hsep [prettyLoc loc, hl' Free $ pretty0 unicode x, "is not in scope"] + hsep [hl' Free $ pretty0 unicode x, "is not in scope"] NotType loc ctx s => inTContext ctx $ - sep [prettyLoc loc <++> "the term", termn ctx.names s, "is not a type"] + sep ["the term", termn ctx.names s, "is not a type"] WrongType loc ctx ty s => inEContext ctx $ - sep [prettyLoc loc <++> "the term", termn ctx.names0 s, + sep ["the term", termn ctx.names0 s, "cannot have type", termn ctx.names0 ty] MissingEnumArm loc tag tags => - sep [hsep [prettyLoc loc, "the tag", hl Tag $ pretty tag, - "is not contained in"], + sep [hsep ["the tag", hl Tag $ pretty tag, "is not contained in"], termn empty $ Enum (fromList tags) noLoc] WhileChecking ctx pi s a err => @@ -331,32 +357,32 @@ parameters (unicode : Bool) sep ["while checking", termn ctx.names s, "has type", termn ctx.names a, hsep ["with quantity", pretty0 unicode pi]], - prettyError showContext err] + prettyErrorNoLoc showContext err] WhileCheckingTy ctx a k err => vsep [inTContext ctx $ sep ["while checking", termn ctx.names a, isTypeInUniverse k], - prettyError showContext err] + prettyErrorNoLoc showContext err] WhileInferring ctx pi e err => vsep [inTContext ctx $ sep ["while inferring the type of", termn ctx.names $ E e, hsep ["with quantity", pretty0 unicode pi]], - prettyError showContext err] + prettyErrorNoLoc showContext err] WhileComparingT ctx mode a s t err => vsep [inEContext ctx $ sep ["while checking that", termn ctx.names0 s, hsep ["is", prettyMode mode], termn ctx.names0 t, "at type", termn ctx.names0 a], - prettyError showContext err] + prettyErrorNoLoc showContext err] WhileComparingE ctx mode e f err => vsep [inEContext ctx $ sep ["while checking that", termn ctx.names0 $ E e, hsep ["is", prettyMode mode], termn ctx.names0 $ E f], - prettyError showContext err] + prettyErrorNoLoc showContext err] where inTContext : TyContext d n -> Doc HL -> Doc HL inTContext ctx doc = @@ -369,3 +395,8 @@ parameters (unicode : Bool) if showContext && not (null ctx) then vsep [sep ["in context", prettyEqContext unicode ctx], doc] else doc + + export + prettyError : (showContext : Bool) -> Error -> Doc HL + prettyError showContext err = + sep [prettyLoc err.loc, indent 4 $ prettyErrorNoLoc showContext err]