diff --git a/.gitignore b/.gitignore index 28e34b4..5224155 100644 --- a/.gitignore +++ b/.gitignore @@ -3,3 +3,4 @@ inputs/ *.*~ support/*.o support/advent-support +tmp/ diff --git a/src/Main.md b/src/Main.md index b8aae63..b859238 100644 --- a/src/Main.md +++ b/src/Main.md @@ -1,4 +1,3 @@ - **Table of Contents** - [Advent of Code](#advent-of-code) @@ -16,8 +15,6 @@ - [Lower logging into the IO component of the effect](#lower-logging-into-the-io-component-of-the-effect) - [Handle the effectful action as an IO action ](#handle-the-effectful-action-as-an-io-action) - - # Advent of Code This module provides a command line interface for running the solution to a specific day for a specific year, run as `advent $YEAR $DAY`. @@ -180,11 +177,9 @@ Handle the verbosity flag, if it is set, hook our logger up to stderr, otherwise ```idris -- If the verbose flag is set, hook up the logging writer to stderr - let verbose = any (== Verbose) opts.options - let logHandler : Eff [IO, Except Error, WriterL "log" String] () -> Eff [IO, Except Error] () = - if verbose - then handleLog ePutStrLn - else handleLog (\x => pure ()) + let verbosity = count (== Verbose) opts.options + let logHandler : Eff [IO, Except Error, Logger] () -> Eff [IO, Except Error] () = + handleLog (Warn >+ verbosity) -- Add the logging writer to the effect logHandler $ do ``` @@ -244,28 +239,6 @@ Check and see if the selected `Day` has a part 2, if it does, feed the opaque co where ``` -### Print strings to stderr - -Putting this in its own function makes dealing with the potential error returned by `fPutStrLn` a bit eaiser. It's reasonable to ignore this error, since if we can't write to stderr we are kinda powerless to tell anyone about it. - -```idris - -- print to standard error - ePutStrLn : Lazy String -> IO () - ePutStrLn str = do - _ <- fPutStrLn stderr str - pure () -``` - -### Decompose a Writer - -Having this be a function keeps the `a` somewhat opaque and helps with they type checking. Only values of `Writer $TYPE ()` can actually be constructed, but the type checker gets a little bit confused about this when you try to do this by pattern matching inline. - -```idris - -- Decompose a writer, eases type inference - unwriter : WriterL "log" String a -> (a, String) - unwriter (Tell vw) = ((), vw) -``` - ### Lower logging into the IO component of the effect This function uses the provided `String -> IO ()` to remove the `Writer` from the effects list by translating `tell` calls to IO actions within the effect. @@ -273,14 +246,13 @@ This function uses the provided `String -> IO ()` to remove the `Writer` from th ```idris -- Lowers logging into IO within the effect using the given IO function handleLog : - Has (WriterL "log" String) fs => Has IO (fs - WriterL "log" String) => - (tell : Lazy String -> IO ()) -> Eff fs a -> Eff (fs - (WriterL "log" String)) a - handleLog tell x = - handle - (\msg, f => - do let (val, msg) = unwriter msg - _ <- send $ tell msg - f val) x + Has Logger fs => Has IO (fs - Logger) => + (max_log : Level) -> Eff fs a -> Eff (fs - Logger) a + handleLog max_log x = + handle + (\msg, f => + do _ <- send $ handleLoggerIO max_log msg + f $ ignore msg) x ``` # Handle the effectful action as an IO action diff --git a/src/Runner.md b/src/Runner.md index 01a85c3..54a09da 100644 --- a/src/Runner.md +++ b/src/Runner.md @@ -1,4 +1,3 @@ - **Table of Contents** - [Unified interface for any day from any year](#unified-interface-for-any-day-from-any-year) @@ -14,8 +13,6 @@ - [Methods](#methods) - [locate](#locate) - - # Unified interface for any day from any year This module provides some basic data types for building an application containing all my solutions to all of the parts of all the days across all of the years. @@ -28,6 +25,8 @@ module Runner import Control.Eff import Structures.Dependent.FreshList +import public Util.Eff + %default total ``` @@ -43,7 +42,7 @@ A `Writer` effect is provided for logging, and a `Reader` effect is provided to public export PartEff : (err : Type) -> List (Type -> Type) PartEff err = - [IO, Except err, WriterL "log" String, ReaderL "input" String] + [IO, Except err, Logger, ReaderL "input" String] ``` # The `Day` Record diff --git a/src/Util/Eff.md b/src/Util/Eff.md index 358cf0a..3d8c95d 100644 --- a/src/Util/Eff.md +++ b/src/Util/Eff.md @@ -8,32 +8,139 @@ module Util.Eff import Control.Eff import Text.ANSI +import System +import System.File + %default total ``` ## Logging -Use the `WriterL "log" String` effect like a logging library. We'll provide a few "log levels" as verbs for the effect, but no filtering is done, when logging is enabled, all logs are always displayed, however the log level is indicated with a colored tag. +### Log Levels + +Basic enumeration describing log levels, we define some (hidden) utility functions for working with these. + +```idris +public export +data Level = Err | Warn | Info | Debug | Trace | Other Nat +``` + +Convert a `Level` into a colorized tag + ```idris - export - info : Has (WriterL "log" String) fs => Lazy String -> Eff fs () - info str = - let tag = show . bolden . show . colored Green $ "[INFO]" - in tellAt "log" (tag ++ ": " ++ str ++ "\n") - - export - debug : Has (WriterL "log" String) fs => Lazy String -> Eff fs () - debug str = - let tag = show . bolden . show . colored BrightWhite $ "[DEBUG]" - in tellAt "log" (tag ++ ": " ++ str ++ "\n") - - export - warn : Has (WriterL "log" String) fs => Lazy String -> Eff fs () - warn str = - let tag = show . bolden . show . colored Yellow $ "[WARN]" - in tellAt "log" (tag ++ ": " ++ str ++ "\n") +export +levelToTag : Level -> String +levelToTag Err = + show . bolden . show . colored BrightRed $ "[Error]" +levelToTag Warn = + show . bolden . show . colored BrightYellow $ "[Warning]" +levelToTag Info = + show . bolden . show . colored Green $ "[Info]" +levelToTag Debug = + show . bolden . show . colored Magenta $ "[Debug]" +levelToTag Trace = + show . bolden . show . colored Cyan $ "[Trace]" +levelToTag (Other k) = + show . bolden . show . colored BrightWhite $ "[\{show k}]" +``` + +### Logger effect + +This is a basic data structure that captures a lazy log message (so we don't have to pay any of the costs associated with generating the log message when it is filtered) + +```idris +public export +data Logger : Type -> Type where + Log : (level : Level) -> (msg : Lazy String) -> Logger () +``` + +We'll also provide some basic accessors, and an `ignore` function useful for writing handlers. + +```idris +export +(.level) : Logger t -> Level +(.level) (Log level msg) = level + +export +(.msg) : Logger t -> Lazy String +(.msg) (Log level msg) = msg + +export +ignore : Logger t -> t +ignore (Log level msg) = () +``` + +#### Handler + +Because we know that we will only be using `logger` in an `IO` context, we aren't currently going to provide a `runLogger` or the like, instead we'll define a function, suitable for use as a `runEff` handler, that filters log messages and prints them to `stderr` over `IO`. + +In the event a log message is filtered out, it's inner message is never inspected, avoiding evaluation. + +```idris +export +handleLoggerIO : + (max_level : Level) -> Logger t -> IO t +handleLoggerIO max_level x = + if x.level <= max_level + then do + _ <- fPutStrLn stderr "\{levelToTag x.level}: \{x.msg}" + pure . ignore $ x + else pure . ignore $ x +``` + +Use the `WriterL "log" String` effect like a logging library. We'll provide a few "log levels" as verbs for the effect, but no filtering is done, when logging is enabled, all logs are always displayed, however the log level is indicated with a colored tag. + +```idris +export +error : Has Logger fs => Lazy String -> Eff fs () +error x = send $ Log Err x + +export +warn : Has Logger fs => Lazy String -> Eff fs () +warn x = send $ Log Warn x + +export +info : Has Logger fs => Lazy String -> Eff fs () +info x = send $ Log Info x + +export +debug : Has Logger fs => Lazy String -> Eff fs () +debug x = send $ Log Debug x + +export +trace : Has Logger fs => Lazy String -> Eff fs () +trace x = send $ Log Trace x ```