1 files changed, 62 insertions, 44 deletions

diff --git a/src/Obs/Logging.idr b/src/Obs/Logging.idr
index 0761775..ef0bae6 100644
--- a/src/Obs/Logging.idr
+++ b/src/Obs/Logging.idr
@@ -1,7 +1,5 @@
 module Obs.Logging
 
-import Data.List.Lazy
-
 import System
 
 import Text.Bounded
@@ -40,60 +38,96 @@ Ord Level where
 
 record Message (ann : Type) where
   constructor MkMessage
-  lvl  : Level
-  msg  : Doc ann
+  lvl : Level
+  msg : Doc ann
+  bounds : Maybe Bounds
   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 ]
+  let leader =
+    hsep $
+      [ fill 6 (pretty (show msg.lvl) <+> colon) ] ++
+      [ Doc.pretty $ concat {t = List} $
+        case msg.bounds of
+          Nothing => []
+          Just bounds =>
+            [ show (1 + bounds.startLine)
+            , ":"
+            , show bounds.startCol
+            , "--"
+            , show (1 + bounds.endLine)
+            , ":"
+            , show bounds.endCol
+            , ":"
+            ]
+      ] ++
+      map (\s => pretty s <+> colon) msg.tags
+  in group $ width (group leader <+> line) (\width => group $ indent (2 - width) msg.msg)
 
 -- Logging Monad ---------------------------------------------------------------
 
 export
-record Logging (ann, t : Type) where
-  constructor MkLogging
-  out  : Maybe t
-  msgs : LazyList (Message ann)
+data Logging : (ann, t : Type) -> Type where
+  Cont : (msg : Message ann) -> (l : Lazy (Logging ann t)) -> Logging ann t
+  Abort : Logging ann t
+  End : (v : t) -> Logging ann t
+
+%name Logging l, l'
 
 export
 Functor (Logging ann) where
-  map f = {out $= map f}
+  map f (Cont msg l) = Cont msg (map f l)
+  map f Abort = Abort
+  map f (End v) = End (f v)
 
 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}
+  pure = End
+  (Cont msg f) <*> v = Cont msg (f <*> v)
+  Abort <*> v = Abort
+  (End f) <*> (Cont msg v) = Cont msg (End f <*> v)
+  (End f) <*> Abort = Abort
+  (End f) <*> (End v) = End (f v)
 
 export
 Monad (Logging ann) where
-  (MkLogging Nothing  msgs) >>= f = MkLogging Nothing msgs
-  (MkLogging (Just v) msgs) >>= f = {msgs $= (msgs ++)} (f v)
+  join (Cont msg l) = Cont msg (join l)
+  join Abort = Abort
+  join (End v) = v
 
--- -- Eliminators -----------------------------------------------------------------
+-- Eliminators -----------------------------------------------------------------
 
 export
 discard : Logging ann a -> Maybe a
-discard = out
+discard (Cont msg l) = discard l
+discard Abort = Nothing
+discard (End v) = Just v
 
 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
+logToTerminal lvl (Cont msg l) = do
+  () <- if msg.lvl <= lvl then putDoc (pretty msg) else pure ()
+  logToTerminal lvl l
+logToTerminal lvl Abort = exitFailure
+logToTerminal lvl (End v) = pure v
 
 export
 abort : Logging ann a
-abort = MkLogging Nothing []
+abort = Abort
+
+mapMsg : (Message ann -> Message ann') -> Logging ann a -> Logging ann' a
+mapMsg f (Cont msg l) = Cont (f msg) (mapMsg f l)
+mapMsg f Abort = Abort
+mapMsg f (End v) = End v
 
 export
 inScope : (tag : String) -> Logging ann a -> Logging ann a
-inScope tag = {msgs $= map {tags $= (tag ::)}}
+inScope tag = mapMsg {tags $= (tag ::)}
+
+export
+inBounds : Bounds -> Logging ann a -> Logging ann a
+inBounds bounds = mapMsg {bounds $= maybe (Just bounds) Just}
 
 public export
 interface Loggable (0 ann, ty : Type) where
@@ -122,27 +156,11 @@ 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 []]
+  log lvl msg = Cont (MkMessage lvl msg Nothing []) $ End ()
 
 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)