module Obs.Logging

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
  bounds : Maybe Bounds
  tags : List String

prettyMsg : Message ann -> Doc ann
prettyMsg msg =
  let leader =
    hsep $
      [ fill 6 (pretty (show msg.lvl) <+> colon) ] ++
      (case msg.bounds of
        Nothing => []
        Just bounds =>
          [ Doc.pretty $ concat {t = List} $
            [ 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
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 (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 = 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
  join (Cont msg l) = Cont msg (join l)
  join Abort = Abort
  join (End v) = v

-- Eliminators -----------------------------------------------------------------

export
discard : Logging ann a -> Maybe a
discard (Cont msg l) = discard l
discard Abort = Nothing
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 (prettyMsg msg) else pure ()
  logToTerminal lvl l
logToTerminal lvl Abort = exitFailure
logToTerminal lvl (End v) = pure v

export
abort : Logging ann a
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 = mapMsg {tags $= (tag ::)}

export
inBounds : WithBounds (Logging ann a) -> Logging ann a
inBounds msg =
  let map : Logging ann a -> Logging ann a
      map = if msg.isIrrelevant then id else mapMsg {bounds $= maybe (Just msg.bounds) Just}
  in map msg.val

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 = Cont (MkMessage lvl msg Nothing []) $ End ()

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