Introduce better logging.

Led to immediate bug fixes for Pi types.

1 files changed, 148 insertions, 0 deletions

diff --git a/src/Obs/Logging.idr b/src/Obs/Logging.idr
new file mode 100644
index 0000000..0761775
--- /dev/null
+++ b/src/Obs/Logging.idr
@@ -0,0 +1,148 @@
+module Obs.Logging
+
+import Data.List.Lazy
+
+import System
+
+import Text.Bounded
+import public Text.PrettyPrint.Prettyprinter
+import Text.PrettyPrint.Prettyprinter.Render.Terminal
+
+-- Logging Levels --------------------------------------------------------------
+
+public export
+data Level = Trace | Info | Debug | Warn | Error
+
+export
+Show Level where
+  show Trace = "trace"
+  show Info  = "info"
+  show Debug = "debug"
+  show Warn  = "warn"
+  show Error = "error"
+
+levelToNat : Level -> Nat
+levelToNat Trace = 4
+levelToNat Info  = 3
+levelToNat Debug = 2
+levelToNat Warn  = 1
+levelToNat Error = 0
+
+export
+Eq Level where
+  l == l' = levelToNat l == levelToNat l'
+
+export
+Ord Level where
+  compare l l' = compare (levelToNat l) (levelToNat l')
+
+-- Logging Messages ------------------------------------------------------------
+
+record Message (ann : Type) where
+  constructor MkMessage
+  lvl  : Level
+  msg  : Doc ann
+  tags : List String
+
+pretty : Message ann -> Doc ann
+pretty msg =
+  hsep $
+  [ fill 6 (pretty (show msg.lvl) <+> colon) ] ++
+  reverse (map (\s => pretty s <+> colon) msg.tags) ++
+  [ align msg.msg ]
+
+-- Logging Monad ---------------------------------------------------------------
+
+export
+record Logging (ann, t : Type) where
+  constructor MkLogging
+  out  : Maybe t
+  msgs : LazyList (Message ann)
+
+export
+Functor (Logging ann) where
+  map f = {out $= map f}
+
+export
+Applicative (Logging ann) where
+  pure v = MkLogging {out = pure v, msgs = []}
+  f <*> v = MkLogging {out = f.out <*> v.out, msgs = f.msgs ++ v.msgs}
+
+export
+Monad (Logging ann) where
+  (MkLogging Nothing  msgs) >>= f = MkLogging Nothing msgs
+  (MkLogging (Just v) msgs) >>= f = {msgs $= (msgs ++)} (f v)
+
+-- -- Eliminators -----------------------------------------------------------------
+
+export
+discard : Logging ann a -> Maybe a
+discard = out
+
+export
+logToTerminal : Level -> Logging AnsiStyle a -> IO a
+logToTerminal lvl log = do
+  Lazy.for_ (filter (\msg => msg.lvl <= lvl) log.msgs) (putDoc . pretty)
+  case log.out of
+    Just v => pure v
+    Nothing => exitFailure
+
+export
+abort : Logging ann a
+abort = MkLogging Nothing []
+
+export
+inScope : (tag : String) -> Logging ann a -> Logging ann a
+inScope tag = {msgs $= map {tags $= (tag ::)}}
+
+public export
+interface Loggable (0 ann, ty : Type) where
+  log : Level -> ty -> Logging ann ()
+
+export
+trace : Loggable ann ty => ty -> Logging ann ()
+trace = log Trace
+
+export
+info : Loggable ann ty => ty -> Logging ann ()
+info = log Info
+
+export
+debug : Loggable ann ty => ty -> Logging ann ()
+debug = log Debug
+
+export
+warn : Loggable ann ty => ty -> Logging ann ()
+warn = log Warn
+
+export
+error : Loggable ann ty => ty -> Logging ann ()
+error = log Error
+
+export
+fatal : Loggable ann ty => ty -> Logging ann a
+fatal msg = do error msg; abort
+  
+export
+Loggable ann (Doc ann) where
+  log lvl msg = MkLogging (pure ()) [MkMessage lvl msg []]
+
+export
+Pretty x => Loggable ann x where
+  log lvl msg = log lvl $ pretty {ann = ann} msg
+
+export
+Loggable ann x => Loggable ann (WithBounds x) where
+  log lvl msg =
+    let f : Logging ann () -> Logging ann ()
+        f = case msg.isIrrelevant of
+          True => id
+          False => inScope $
+            show (1 + msg.bounds.startLine) ++
+            ":" ++
+            show msg.bounds.startCol ++
+            "--" ++
+            show (1 + msg.bounds.endLine) ++
+            ":" ++
+            show msg.bounds.endCol
+    in f (log lvl msg.val)