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)