advent/src/Main.md

<!-- markdown-toc start - Don't edit this section. Run M-x markdown-toc-refresh-toc -->
**Table of Contents**

- [Advent of Code](#advent-of-code)
- [Command Line Interface](#command-line-interface)
    - [Error Type](#error-type)
    - [Extract the year and day](#extract-the-year-and-day)
- [The Advent ](#the-advent)
- [The Hard Part](#the-hard-part)
    - [Parsing the arguments](#parsing-the-arguments)
    - [Handling the arguments and finding the input](#handling-the-arguments-and-finding-the-input)
    - [Executing the parts](#executing-the-parts)
    - [Helper functions](#helper-functions)
        - [Print strings to stderr](#print-strings-to-stderr)
        - [Decompose a Writer](#decompose-a-writer)
        - [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)

<!-- markdown-toc end -->

# 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`. 

This runner will automatically locate the appropriate input file and then run the selected day's solution against it. See [Runner](Runner.md) for the definitions of the `Day`, `Year`, and `Advent` data types.

```idris
module Main

import System
import System.Path
import System.File
import System.Directory
import System.Console.GetOpt
import Data.String
import Data.Vect

import Control.Eff
import Derive.Prelude

import Structures.Dependent.FreshList

import Runner
import Util
import Util.Eff

import Years.Y2015;

%language ElabReflection
%default total
```

# Command Line Interface

Since this is a simple application, I am using `GetOpt` from `contrib` for argument parsing. Here we define our options list, a data type to describe our flags, and the usage message header.

```idris
data Flag = UseExample | Verbose
%runElab derive "Flag" [Eq, Show]

options : List (OptDescr Flag)
options =
  [
    MkOpt ['u'] ["use-example"] (NoArg UseExample) "Use example input instead of main input"
  , MkOpt ['v'] ["verbose"] (NoArg Verbose) "Enable logging to stderr"
  ]

header : String
header = "Usage: advent YEAR DAY [OPTION...]"
```

## Error Type

We will be using one unified error type for the entire `Main` module, but we must go ahead and define it before we go any further with command line arguments parsing, as we are about to do some things that might fail.

```idris
data Error : Type where
  OptionsError : (errs : List String) -> Error
  ArgumentsError : (count : Nat) -> Error
  InvalidYear : (year : String) -> Error
  InvalidDay : (year : Nat) -> (day : String) -> Error
  NoSuchDay : (year : Nat) -> (day : Nat) -> Error
  NoCurrentDir : Error
  InputRead : (path : String) -> (err : FileError) -> Error
  SolveError : Show e => (year, day, part : Nat) -> (err : e) -> Error
%name Error err
```

A `Show` implementation for `Error` is provided, hidden in this document for brevity.


<!-- idris
Show Error where
  show (OptionsError errs) =
    let errs = unlines . map ("  " ++) . lines . joinBy "\n" $ errs
    in "Error parsing options:\n" ++ errs ++ "\n" ++ usageInfo header options
  show (ArgumentsError count) =
    "Error parsing arguments: Expected 2 positional arguments, got \{show count}. Provide only year and date.\n" ++
    usageInfo header options
  show (InvalidYear year) =
    "Error parsing arguments: Unable to parse year argument: \{year}"
  show (InvalidDay year day) =
    "Error parsing arguments: Failed to parse day \{day} of year \{show year}"
  show (NoSuchDay year day) =
    "Error locating day: No such day \{show day} of year \{show year}"
  show NoCurrentDir =
    "Unknown error getting current working directory"
  show (InputRead path err) =
    let err = unlines . map ("  " ++) . lines . show $ err
    in "Error reading input: Encountered error reading input at \{path}\n" ++ err
  show (SolveError year day part err) =
    let err = unlines . map ("  " ++) . lines . show $ err
    in "Error solving day \{show day} part \{show part} of year \{show year}: \n" ++ err
-->

## Extract the year and day

After peeling off our options from the arguments using `GetOpt`, we will be left with a list of non-option arguments, which we must then parse into our year number/day number pair. We perform some pattern matching to make sure the list is the correct length, and then parse the individual integers, throwing an error if anything goes wrong

```idris
||| Convert the non-option arguments into a Year/Day pair
argumentsToPair : Has (Except Error) fs =>
  List String -> Eff fs (Nat, Nat)
argumentsToPair [] = throw $ ArgumentsError 0
argumentsToPair [x] = throw $ ArgumentsError 1
argumentsToPair [year, day] = do
  year <- note (InvalidYear year) $ parsePositive year
  day <- note (InvalidDay year day) $ parsePositive day
  pure (year, day)
argumentsToPair xs = throw $ ArgumentsError (length xs)
```

# The Advent 

Construct our top-level `Advent` record from the imported `Year` modules. The argument to the `MkAdvent` constructor is a `FreshList`, with a freshness criteria ensuring that the list is in ascending order and does not include any duplicate `Year`s.

```idris
advent : Advent
advent = MkAdvent [
    y2015
  ]
```

# The Hard Part

Now we must glue everything together, parse our arguments, handle any supplied options, locate the relevant year and day, locate the corresponding input file, read it, and then run the selected `Day` against it.

Because we are building our application around effects, the actual core of the application is the effectful `start` computation, that the `main` function will then apply `IO` based handlers to.

Our reader and writer aren't ready yet, we need to do some setup first, so the top level type signature doesn't include them, so we'll add them to the effects list as they become available.

```idris
covering
||| Actual main, as an effectful computation
start : Eff [IO, Except Error] ()
start = do
```

## Parsing the arguments

Feed the augments from `System.getArgs` into `getOpt`, making sure to drop the name the binary was invoked with, then check for any errors in the result, throwing our own error if any are encountered.

```idris
  -- Read and parse arguments/options
  args <- getArgs
  let opts = getOpt Permute options (drop 1 args)
  when (not . null $ opts.errors) $
    throw (OptionsError opts.errors)
```

Use our `argumentsToPair` function to extract the selected year and day numbers from the positional arguments, implicitly throwing an error if there are any failures doing so.

```idris
  (year, day_n) <- argumentsToPair opts.nonOptions
```

## 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.

```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 ())
  -- Add the logging writer to the effect
  logHandler $ do
```

Find the current directory and append to it to find the input file. If the `--use-example/-u` flag is set, look for the input file at `inputs/examples/$year/$day`, otherwise look for it at `inputs/real/$year/$day`.

After we've located it, attempt to read from it, throwing an `InputRead` error if any errors occur, then insert the contents into our `Reader` and inject it into the effects list.

```idris
  -- Locate and read in the input file
  Just cwd <- currentDir | _ => throw NoCurrentDir
  let cwd = parse cwd
  let use_example = any (== UseExample) opts.options
  let base_dir = cwd /> "inputs" /> (if use_example then "examples" else "real");
  let input_path = show $ base_dir /> (show year) /> (show day_n)
  info "Reading input from \{input_path}"
  Right contents <- readFile input_path | Left err => throw $ InputRead input_path err
  -- Now add the reader that provides the input to the effect
  runReaderAt "input" contents {fs = PartEff Error} $ do
```

Try and locate the `Day` in our `Advent` record, throwing an error if we are unable to locate it

```idris
  -- Attempt to locate the provided day
  Just day <- pure $ locate year day_n advent | _ => throw $ NoSuchDay year day_n
```

## Executing the parts

Run the selected `Day`'s part 1, wrapping any errors that it returns in a `SolveError`. Collect both the result and the opaque context value, then print out the result.

```idris
  -- Run part 1
  part_1 <- lift $ runExcept day.part1
  (part_1, ctx) <- rethrow . mapLeft (SolveError year day_n 1 @{day.showErr1}) $ part_1
  putStrLn "\{show year} day \{show day_n} part 1:"
  putStrLn $ unlines . map ("  " ++) . lines . show @{day.showOut1} $ part_1
```

Check and see if the selected `Day` has a part 2, if it does, feed the opaque context value collected from part 1 into it, wrap any errors that it returns in a `SolveError`, then print out the result, then return, closing out the program.

```idris
  -- Run part 2 if we have it
  case day.part2 of
    Nothing => pure ()
    Just part_2_f => do
      part_2 <- lift . runExcept $ part_2_f ctx
      part_2 <- rethrow . mapLeft (SolveError year day_n 2 @{day.showErr2}) $ part_2
      putStrLn "\{show year} day \{show day_n} part 2:"
      putStrLn $ unlines . map ("  " ++) . lines . show @{day.showOut2} $ part_2
```

## Helper functions

```idris
  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 : 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. 

```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 : 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
```

# Handle the effectful action as an IO action 

Use `runEff` to translate the effects in `start`'s effects list into IO actions, and return the resulting `IO ()`.

The `IO` component of the effects list is handled via `id`, translating `IO` actions into themselves, and we construct a helper function to handle errors as IO actions by printing the error and crashing the program.

```idris
covering
||| Shim main, which simply executes the effectful computation
main : IO ()
main = runEff start [id, handleError]
  where
  handleError : Except Error a -> IO a
  handleError (Err err) = do
    printLn err
    exitFailure
```