From ff65d1e285a97295708899bebdcc83ec214cd347 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Sat, 7 Jan 2023 21:10:30 +0000
Subject: Add containers types.

Containers are syntactic sugar. They are also completely untested.
---
 src/Obs/Logging.idr | 22 +++++++++++++++++++---
 1 file changed, 19 insertions(+), 3 deletions(-)

(limited to 'src/Obs/Logging.idr')

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
-- 
cgit v1.2.3