From 407149dd4a6053482c64986b9fbf67b623717a8c Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Thu, 23 Jan 2025 00:17:19 -0500 Subject: [PATCH] Documentation tweaks and fixes --- README.md | 5 +++++ src/Main.md | 8 ++++---- src/Runner.md | 6 +++--- src/Util/Eff.md | 23 +++++++++++++++++------ 4 files changed, 29 insertions(+), 13 deletions(-) diff --git a/README.md b/README.md index 2ce05fb..db8f4f9 100644 --- a/README.md +++ b/README.md @@ -26,6 +26,11 @@ solution. Extend the functionality of the effects included in the [eff](https://github.com/stefan-hoeck/idris2-eff/) library + - [Util.Digits](src/Util/Digits.md) + + Provide views that enable recursively pattern matching numbers as lists of + digits, in both ascending and descending order of significance. + # Index of years and days - 2015 diff --git a/src/Main.md b/src/Main.md index a913135..f602362 100644 --- a/src/Main.md +++ b/src/Main.md @@ -181,8 +181,8 @@ failures doing so. ## Handling the arguments and finding the input Handle the verbosity flag, if it is set, hook our logger up to stderr, otherwise -blackhole the logs. Afterwards, use `logHandler` to introduce the logging -`Writer` into the effects list. +blackhole the logs. Afterwards, use `logHandler` to introduce the `Logger` into +the effects list. ```idris -- If the verbose flag is set, hook up the logging writer to stderr @@ -259,8 +259,8 @@ a `SolveError`, then print out the result, then return, closing out the program. ### 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. +Makes use of `Logger`'s `handleLoggerIO` function to "lower" logging actions +into `IO` within the effect. ```idris -- Lowers logging into IO within the effect using the given IO function diff --git a/src/Runner.md b/src/Runner.md index 500821b..201baff 100644 --- a/src/Runner.md +++ b/src/Runner.md @@ -28,9 +28,9 @@ function to have a single source of truth for this. The `err` type can be any type with a `Show` implementation, but that constraint will be tacked on in the next step. -A `Writer` effect is provided for logging, and a `Reader` effect is provided to -pass in the input, just to make the top level API a little bit cleaner. `IO` is -also provided, even though the part solutions themselves shouldn't really be +The `Logger` effect is provided for logging, and a `Reader` effect is provided +to pass in the input, just to make the top level API a little bit cleaner. `IO` +is also provided, even though the part solutions themselves shouldn't really be doing any IO, this may come in handy if a part needs `IO` for performance reasons. diff --git a/src/Util/Eff.md b/src/Util/Eff.md index 1b51cba..1baa453 100644 --- a/src/Util/Eff.md +++ b/src/Util/Eff.md @@ -22,9 +22,18 @@ import System.File Basic enumeration describing log levels, we define some (hidden) utility functions for working with these. +The `Other n` log level is restricted to `n` greater than 4, to prevent +ambiguity between custom log levels and predefined log levels. + ```idris public export -data Level = Err | Warn | Info | Debug | Trace | Other Nat +data Level : Type where + Err : Level + Warn : Level + Info : Level + Debug : Level + Trace : Level + Other : (n : Nat) -> {auto _ : n `GT` 4} -> Level ```