%default total
This commit is contained in:
parent
b651ed5447
commit
fbb862c88b
2 changed files with 161 additions and 154 deletions
|
|
@ -7,6 +7,8 @@ import System.File
|
||||||
|
|
||||||
import Quox.Pretty
|
import Quox.Pretty
|
||||||
|
|
||||||
|
%default total
|
||||||
|
|
||||||
%hide Text.PrettyPrint.Prettyprinter.Doc.infixr.(<++>)
|
%hide Text.PrettyPrint.Prettyprinter.Doc.infixr.(<++>)
|
||||||
|
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -13,6 +13,8 @@ import Derive.Prelude
|
||||||
%language ElabReflection
|
%language ElabReflection
|
||||||
%hide TT.Name
|
%hide TT.Name
|
||||||
|
|
||||||
|
%default total
|
||||||
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
record NameContexts d n where
|
record NameContexts d n where
|
||||||
|
|
@ -246,162 +248,165 @@ where
|
||||||
hangDSingle "with quantities" $
|
hangDSingle "with quantities" $
|
||||||
separateTight !commaD $ toSnocList' !(traverse prettyQty qs)]
|
separateTight !commaD $ toSnocList' !(traverse prettyQty qs)]
|
||||||
|
|
||||||
export
|
parameters {opts : LayoutOpts} (showContext : Bool)
|
||||||
prettyErrorNoLoc : {opts : _} -> (showContext : Bool) -> Error ->
|
export
|
||||||
Eff Pretty (Doc opts)
|
inContext' : Bool -> a -> (a -> Eff Pretty (Doc opts)) ->
|
||||||
prettyErrorNoLoc showContext = \case
|
Doc opts -> Eff Pretty (Doc opts)
|
||||||
ExpectedTYPE _ ctx s =>
|
inContext' null ctx f doc =
|
||||||
hangDSingle "expected a type universe, but got"
|
if showContext && not null then
|
||||||
!(prettyTerm ctx.dnames ctx.tnames s)
|
pure $ vappend doc (sep ["in context", !(f ctx)])
|
||||||
|
else pure doc
|
||||||
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
|
|
||||||
|
|
||||||
|
export %inline
|
||||||
inTContext : TyContext d n -> Doc opts -> Eff Pretty (Doc opts)
|
inTContext : TyContext d n -> Doc opts -> Eff Pretty (Doc opts)
|
||||||
inTContext ctx doc =
|
inTContext ctx = inContext' (null ctx) ctx prettyTyContext
|
||||||
if showContext && not (null ctx) then
|
|
||||||
pure $ vappend doc (sep ["in context", !(prettyTyContext ctx)])
|
|
||||||
else pure doc
|
|
||||||
|
|
||||||
|
export %inline
|
||||||
inEContext : EqContext n -> Doc opts -> Eff Pretty (Doc opts)
|
inEContext : EqContext n -> Doc opts -> Eff Pretty (Doc opts)
|
||||||
inEContext ctx doc =
|
inEContext ctx = inContext' (null ctx) ctx prettyEqContext
|
||||||
if showContext && not (null ctx) then
|
|
||||||
pure $ vappend doc (sep ["in context", !(prettyEqContext ctx)])
|
|
||||||
else pure doc
|
|
||||||
|
|
||||||
export
|
export
|
||||||
prettyError : {opts : _} -> (showContext : Bool) ->
|
prettyErrorNoLoc : Error -> Eff Pretty (Doc opts)
|
||||||
Error -> Eff Pretty (Doc opts)
|
prettyErrorNoLoc err0 = case err0 of
|
||||||
prettyError showContext err = sep <$> sequence
|
ExpectedTYPE _ ctx s =>
|
||||||
[prettyLoc err.loc, indentD =<< prettyErrorNoLoc showContext err]
|
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]
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue