diff options
Diffstat (limited to 'src/Obs/Logging.idr')
| -rw-r--r-- | src/Obs/Logging.idr | 22 |
1 files changed, 19 insertions, 3 deletions
diff --git a/src/Obs/Logging.idr b/src/Obs/Logging.idr index 07060e6..1fc6454 100644 --- a/src/Obs/Logging.idr +++ b/src/Obs/Logging.idr @@ -43,8 +43,8 @@ record Message (ann : Type) where bounds : Maybe Bounds tags : List String -pretty : Message ann -> Doc ann -pretty msg = +prettyMsg : Message ann -> Doc ann +prettyMsg msg = let leader = hsep $ [ fill 6 (pretty (show msg.lvl) <+> colon) ] ++ @@ -107,7 +107,7 @@ discard (End v) = Just v export logToTerminal : Level -> Logging AnsiStyle a -> IO a logToTerminal lvl (Cont msg l) = do - () <- if msg.lvl <= lvl then putDoc (pretty msg) else pure () + () <- if msg.lvl <= lvl then putDoc (prettyMsg msg) else pure () logToTerminal lvl l logToTerminal lvl Abort = exitFailure logToTerminal lvl (End v) = pure v @@ -167,3 +167,19 @@ Loggable ann (Doc ann) where export Pretty x => Loggable ann x where log lvl msg = log lvl $ pretty {ann = ann} msg + +-- Loggings ---------------------------------------------------------------------- + +export +mismatch : (expected, got : Doc ann) -> Logging ann a +mismatch lhs rhs = fatal $ + hang 2 (pretty "expected" <+> line <+> lhs) <+> comma <+> line <+> + hang 2 (pretty "got" <+> line <+> align rhs) + +export +typeMismatch : Doc ann -> Doc ann -> Logging ann a +typeMismatch lhs rhs = inScope "type mismatch" $ mismatch lhs rhs + +export +universeMismatch : Doc ann -> Doc ann -> Logging ann a +universeMismatch lhs rhs = inScope "universe mismatch" $ mismatch lhs rhs |