A simple logger

log.idr

module Main

import Effect.State
import Effect.StdIO
import Effect.System

data Level = Debug | Info | Warn | Error | Critical

-- Apparently Idris doesn't have deriving yet, so define those instances
-- manually. 

total
levelToNat : Level -> Nat
levelToNat Debug = 0
levelToNat Info = 1
levelToNat Warn = 2
levelToNat Error = 3
levelToNat Critical = 4

instance Eq Level where
  a == b = levelToNat a == levelToNat b

instance Ord Level where
  compare a b = compare (levelToNat a) (levelToNat b)

instance Show Level where
  show Debug = "Debug"
  show Info = "Info"
  show Warn = "Warn"
  show Error = "Error"
  show Critical = "Critical"

record LogState : Type where
  MkLogState : (log_level : Level) -> LogState

logLine : Level -> String -> { [STATE LogState, STDIO, SYSTEM] } Eff IO ()
logLine l s = do
  st <- get
  if log_level st > l
    then return ()
    else do
      t <- time
      -- No time functions for formatting yet
      let line = show t ++ "|" ++ show l ++ "|" ++ s
      -- Would like to write to standard output but StdIO doesn't support that
      putStrLn line

main : IO ()
main = do
  runInit [MkLogState Info, (), ()] $ do
    logLine Debug "A"
    logLine Info "B"
    logLine Warn "C"