From fbb862c88beb0c03a79b944ee470414f8be8cd7c Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Fri, 20 Oct 2023 05:28:42 +0200 Subject: [PATCH] %default total --- lib/Quox/Parser/FromParser/Error.idr | 2 + lib/Quox/Typing/Error.idr | 313 ++++++++++++++------------- 2 files changed, 161 insertions(+), 154 deletions(-) diff --git a/lib/Quox/Parser/FromParser/Error.idr b/lib/Quox/Parser/FromParser/Error.idr index 301ff59..44cd0db 100644 --- a/lib/Quox/Parser/FromParser/Error.idr +++ b/lib/Quox/Parser/FromParser/Error.idr @@ -7,6 +7,8 @@ import System.File import Quox.Pretty +%default total + %hide Text.PrettyPrint.Prettyprinter.Doc.infixr.(<++>) diff --git a/lib/Quox/Typing/Error.idr b/lib/Quox/Typing/Error.idr index a48b4d7..1589612 100644 --- a/lib/Quox/Typing/Error.idr +++ b/lib/Quox/Typing/Error.idr @@ -13,6 +13,8 @@ import Derive.Prelude %language ElabReflection %hide TT.Name +%default total + public export record NameContexts d n where @@ -246,162 +248,165 @@ where hangDSingle "with quantities" $ separateTight !commaD $ toSnocList' !(traverse prettyQty qs)] -export -prettyErrorNoLoc : {opts : _} -> (showContext : Bool) -> Error -> - Eff Pretty (Doc opts) -prettyErrorNoLoc showContext = \case - ExpectedTYPE _ ctx s => - hangDSingle "expected a type universe, but got" - !(prettyTerm ctx.dnames ctx.tnames s) - - ExpectedPi _ ctx s => - hangDSingle "expected a function type, but got" - !(prettyTerm ctx.dnames ctx.tnames s) - - ExpectedSig _ ctx s => - hangDSingle "expected a pair type, but got" - !(prettyTerm ctx.dnames ctx.tnames s) - - ExpectedEnum _ ctx s => - hangDSingle "expected an enumeration type, but got" - !(prettyTerm ctx.dnames ctx.tnames s) - - ExpectedEq _ ctx s => - hangDSingle "expected an enumeration type, but got" - !(prettyTerm ctx.dnames ctx.tnames s) - - ExpectedNat _ ctx s => - hangDSingle - ("expected the type" <++> - !(prettyTerm [<] [<] $ Nat noLoc) <+> ", but got") - !(prettyTerm ctx.dnames ctx.tnames s) - - ExpectedBOX _ ctx s => - hangDSingle "expected a box type, but got" - !(prettyTerm ctx.dnames ctx.tnames s) - - BadUniverse _ k l => pure $ - sep ["the universe level" <++> !(prettyUniverse k), - "is not strictly less than" <++> !(prettyUniverse l)] - - TagNotIn _ tag set => - hangDSingle (hsep ["the tag", !(prettyTag tag), "is not contained in"]) - !(prettyTerm [<] [<] $ Enum set noLoc) - - BadCaseEnum _ head body => sep <$> sequence - [hangDSingle "case expression has head of type" - !(prettyTerm [<] [<] $ Enum head noLoc), - hangDSingle "but cases for" - !(prettyTerm [<] [<] $ Enum body noLoc)] - - BadQtys _ what ctx arms => - hangDSingle (text "inconsistent variable usage in \{what}") $ - sep !(printCaseQtys ctx ctx.tnames arms) - - ClashT _ ctx mode ty s t => - inEContext ctx . sep =<< sequence - [hangDSingle "the term" !(prettyTerm [<] ctx.tnames s), - hangDSingle (text "is not \{prettyMode mode}") - !(prettyTerm [<] ctx.tnames t), - hangDSingle "at type" !(prettyTerm [<] ctx.tnames ty)] - - ClashTy _ ctx mode a b => - inEContext ctx . sep =<< sequence - [hangDSingle "the type" !(prettyTerm [<] ctx.tnames a), - hangDSingle (text "is not \{prettyMode mode}") - !(prettyTerm [<] ctx.tnames b)] - - ClashE _ ctx mode e f => - inEContext ctx . sep =<< sequence - [hangDSingle "the term" !(prettyElim [<] ctx.tnames e), - hangDSingle (text "is not \{prettyMode mode}") - !(prettyElim [<] ctx.tnames f)] - - ClashU _ mode k l => pure $ - sep ["the universe level" <++> !(prettyUniverse k), - text "is not \{prettyModeU mode}" <++> !(prettyUniverse l)] - - ClashQ _ pi rh => pure $ - sep ["the quantity" <++> !(prettyQty pi), - "is not equal to" <++> !(prettyQty rh)] - - NotInScope _ x => pure $ - hsep [!(prettyFree x), "is not in scope"] - - NotType _ ctx s => - inTContext ctx . sep =<< sequence - [hangDSingle "the term" !(prettyTerm ctx.dnames ctx.tnames s), - pure "is not a type"] - - WrongType _ ctx ty s => - inEContext ctx . sep =<< sequence - [hangDSingle "the term" !(prettyTerm [<] ctx.tnames s), - hangDSingle "cannot have type" !(prettyTerm [<] ctx.tnames ty)] - - MissingEnumArm _ tag tags => pure $ - sep [hsep ["the tag", !(prettyTag tag), "is not contained in"], - !(prettyTerm [<] [<] $ Enum (fromList tags) noLoc)] - - WhileChecking ctx sg s a err => - [|vappendBlank - (inTContext ctx . sep =<< sequence - [hangDSingle "while checking" !(prettyTerm ctx.dnames ctx.tnames s), - hangDSingle "has type" !(prettyTerm ctx.dnames ctx.tnames a), - hangDSingle "with quantity" !(prettyQty sg.qty)]) - (prettyErrorNoLoc showContext err)|] - - WhileCheckingTy ctx a k err => - [|vappendBlank - (inTContext ctx . sep =<< sequence - [hangDSingle "while checking" !(prettyTerm ctx.dnames ctx.tnames a), - pure $ text $ isTypeInUniverse k]) - (prettyErrorNoLoc showContext err)|] - - WhileInferring ctx sg e err => - [|vappendBlank - (inTContext ctx . sep =<< sequence - [hangDSingle "while inferring the type of" - !(prettyElim ctx.dnames ctx.tnames e), - hangDSingle "with quantity" !(prettyQty sg.qty)]) - (prettyErrorNoLoc showContext err)|] - - WhileComparingT ctx mode sg a s t err => - [|vappendBlank - (inEContext ctx . sep =<< sequence - [hangDSingle "while checking that" !(prettyTerm [<] ctx.tnames s), - hangDSingle (text "is \{prettyMode mode}") - !(prettyTerm [<] ctx.tnames t), - hangDSingle "at type" !(prettyTerm [<] ctx.tnames a), - hangDSingle "with quantity" !(prettyQty sg.qty)]) - (prettyErrorNoLoc showContext err)|] - - WhileComparingE ctx mode sg e f err => - [|vappendBlank - (inEContext ctx . sep =<< sequence - [hangDSingle "while checking that" !(prettyElim [<] ctx.tnames e), - hangDSingle (text "is \{prettyMode mode}") - !(prettyElim [<] ctx.tnames f), - hangDSingle "with quantity" !(prettyQty sg.qty)]) - (prettyErrorNoLoc showContext err)|] - -where - vappendBlank : Doc opts -> Doc opts -> Doc opts - vappendBlank a b = flush a `vappend` b +parameters {opts : LayoutOpts} (showContext : Bool) + export + inContext' : Bool -> a -> (a -> Eff Pretty (Doc opts)) -> + Doc opts -> Eff Pretty (Doc opts) + inContext' null ctx f doc = + if showContext && not null then + pure $ vappend doc (sep ["in context", !(f ctx)]) + else pure doc + export %inline inTContext : TyContext d n -> Doc opts -> Eff Pretty (Doc opts) - inTContext ctx doc = - if showContext && not (null ctx) then - pure $ vappend doc (sep ["in context", !(prettyTyContext ctx)]) - else pure doc + inTContext ctx = inContext' (null ctx) ctx prettyTyContext + export %inline inEContext : EqContext n -> Doc opts -> Eff Pretty (Doc opts) - inEContext ctx doc = - if showContext && not (null ctx) then - pure $ vappend doc (sep ["in context", !(prettyEqContext ctx)]) - else pure doc + inEContext ctx = inContext' (null ctx) ctx prettyEqContext -export -prettyError : {opts : _} -> (showContext : Bool) -> - Error -> Eff Pretty (Doc opts) -prettyError showContext err = sep <$> sequence - [prettyLoc err.loc, indentD =<< prettyErrorNoLoc showContext err] + export + prettyErrorNoLoc : Error -> Eff Pretty (Doc opts) + prettyErrorNoLoc err0 = case err0 of + ExpectedTYPE _ ctx s => + hangDSingle "expected a type universe, but got" + !(prettyTerm ctx.dnames ctx.tnames s) + + ExpectedPi _ ctx s => + hangDSingle "expected a function type, but got" + !(prettyTerm ctx.dnames ctx.tnames s) + + ExpectedSig _ ctx s => + hangDSingle "expected a pair type, but got" + !(prettyTerm ctx.dnames ctx.tnames s) + + ExpectedEnum _ ctx s => + hangDSingle "expected an enumeration type, but got" + !(prettyTerm ctx.dnames ctx.tnames s) + + ExpectedEq _ ctx s => + hangDSingle "expected an enumeration type, but got" + !(prettyTerm ctx.dnames ctx.tnames s) + + ExpectedNat _ ctx s => + hangDSingle + ("expected the type" <++> + !(prettyTerm [<] [<] $ Nat noLoc) <+> ", but got") + !(prettyTerm ctx.dnames ctx.tnames s) + + ExpectedBOX _ ctx s => + hangDSingle "expected a box type, but got" + !(prettyTerm ctx.dnames ctx.tnames s) + + BadUniverse _ k l => pure $ + sep ["the universe level" <++> !(prettyUniverse k), + "is not strictly less than" <++> !(prettyUniverse l)] + + TagNotIn _ tag set => + hangDSingle (hsep ["the tag", !(prettyTag tag), "is not contained in"]) + !(prettyTerm [<] [<] $ Enum set noLoc) + + BadCaseEnum _ head body => sep <$> sequence + [hangDSingle "case expression has head of type" + !(prettyTerm [<] [<] $ Enum head noLoc), + hangDSingle "but cases for" + !(prettyTerm [<] [<] $ Enum body noLoc)] + + BadQtys _ what ctx arms => + hangDSingle (text "inconsistent variable usage in \{what}") $ + sep !(printCaseQtys ctx ctx.tnames arms) + + ClashT _ ctx mode ty s t => + inEContext ctx . sep =<< sequence + [hangDSingle "the term" !(prettyTerm [<] ctx.tnames s), + hangDSingle (text "is not \{prettyMode mode}") + !(prettyTerm [<] ctx.tnames t), + hangDSingle "at type" !(prettyTerm [<] ctx.tnames ty)] + + ClashTy _ ctx mode a b => + inEContext ctx . sep =<< sequence + [hangDSingle "the type" !(prettyTerm [<] ctx.tnames a), + hangDSingle (text "is not \{prettyMode mode}") + !(prettyTerm [<] ctx.tnames b)] + + ClashE _ ctx mode e f => + inEContext ctx . sep =<< sequence + [hangDSingle "the term" !(prettyElim [<] ctx.tnames e), + hangDSingle (text "is not \{prettyMode mode}") + !(prettyElim [<] ctx.tnames f)] + + ClashU _ mode k l => pure $ + sep ["the universe level" <++> !(prettyUniverse k), + text "is not \{prettyModeU mode}" <++> !(prettyUniverse l)] + + ClashQ _ pi rh => pure $ + sep ["the quantity" <++> !(prettyQty pi), + "is not equal to" <++> !(prettyQty rh)] + + NotInScope _ x => pure $ + hsep [!(prettyFree x), "is not in scope"] + + NotType _ ctx s => + inTContext ctx . sep =<< sequence + [hangDSingle "the term" !(prettyTerm ctx.dnames ctx.tnames s), + pure "is not a type"] + + WrongType _ ctx ty s => + inEContext ctx . sep =<< sequence + [hangDSingle "the term" !(prettyTerm [<] ctx.tnames s), + hangDSingle "cannot have type" !(prettyTerm [<] ctx.tnames ty)] + + MissingEnumArm _ tag tags => pure $ + sep [hsep ["the tag", !(prettyTag tag), "is not contained in"], + !(prettyTerm [<] [<] $ Enum (fromList tags) noLoc)] + + WhileChecking ctx sg s a err => + [|vappendBlank + (inTContext ctx . sep =<< sequence + [hangDSingle "while checking" !(prettyTerm ctx.dnames ctx.tnames s), + hangDSingle "has type" !(prettyTerm ctx.dnames ctx.tnames a), + hangDSingle "with quantity" !(prettyQty sg.qty)]) + (prettyErrorNoLoc err)|] + + WhileCheckingTy ctx a k err => + [|vappendBlank + (inTContext ctx . sep =<< sequence + [hangDSingle "while checking" !(prettyTerm ctx.dnames ctx.tnames a), + pure $ text $ isTypeInUniverse k]) + (prettyErrorNoLoc err)|] + + WhileInferring ctx sg e err => + [|vappendBlank + (inTContext ctx . sep =<< sequence + [hangDSingle "while inferring the type of" + !(prettyElim ctx.dnames ctx.tnames e), + hangDSingle "with quantity" !(prettyQty sg.qty)]) + (prettyErrorNoLoc err)|] + + WhileComparingT ctx mode sg a s t err => + [|vappendBlank + (inEContext ctx . sep =<< sequence + [hangDSingle "while checking that" !(prettyTerm [<] ctx.tnames s), + hangDSingle (text "is \{prettyMode mode}") + !(prettyTerm [<] ctx.tnames t), + hangDSingle "at type" !(prettyTerm [<] ctx.tnames a), + hangDSingle "with quantity" !(prettyQty sg.qty)]) + (prettyErrorNoLoc err)|] + + WhileComparingE ctx mode sg e f err => + [|vappendBlank + (inEContext ctx . sep =<< sequence + [hangDSingle "while checking that" !(prettyElim [<] ctx.tnames e), + hangDSingle (text "is \{prettyMode mode}") + !(prettyElim [<] ctx.tnames f), + hangDSingle "with quantity" !(prettyQty sg.qty)]) + (prettyErrorNoLoc err)|] + + where + vappendBlank : Doc opts -> Doc opts -> Doc opts + vappendBlank a b = flush a `vappend` b + + export + prettyError : Error -> Eff Pretty (Doc opts) + prettyError err = sep <$> sequence + [prettyLoc err.loc, indentD =<< prettyErrorNoLoc err]