Advent

The goal of this project is to get all 500 currently available stars in the form of one single Idris application, and thoroughly document the results as literate Idris files.

Authors Note

This entire book is a single literate code base, the source code is available at https://git.stranger.systems/Idris/advent.

The solutions contained in this project are intended to be read in sequential order, though can reasonably be read in any order if you have a good level of familiarity with more advanced functional programming topics.

The solutions will involve progressively more advanced topics as day and year number increase, though I try not to introduce too much within the scope of any one day.

Suggestions and other feedback are highly welcome, please reach out to me via any platform you know me on, or send an email to the ~thatonelutenist/public-inbox mailing list on source hut.

While this project is intended to read more like a book, while it is still a work in progress, you can follow its development as a psuedo-blog by subscribing to the rss feed for the repository in your feed reader: https://git.stranger.systems/Idris/advent.rss.

Index of non-day modules

• Runner

  Provides data structures for structuring the division of the project into years, days, and parts.

• Main

Provides the Runner based command line interface for running a selected day's solution.

• Util

  Provides extensions of the functionality of the standard library and external libraries. Extensions to the standard library are in the base of this module.

  • Util.Eff

    Extend the functionality of the effects included in the eff library

  • Util.Digits

    Provide views that enable recursively pattern matching numbers as lists of digits, in both ascending and descending order of significance.

• Array

  Provider wrappers over the standard library IOArray type to make them more ergonomic to use.

• Parser

  Effectful parser mini-library

  • Interface

    Effectful parser API

  • ParserState

    Internal state of a parser

  • Numbers

    Parsers for numerical values in multiple bases

  • JSON

  JSON Parser

Index of years and days

• 2015

  • Day 1

    Warm up problem, breaks in our new runner and not much else interesting.

  • Day 2

    An early hint of effectful parsing.

  • Day 3

    Peculiarities of writing mutually recursive functions in dependently typed languages.

  • Day 4

    Basic FFI to openssl to steal its MD5 function for Idris's use.

  • Day 5

    First introduction to views and dependent pattern matching¹.

  • Day 6

    Naive approach to handling the first 2d grid problem.

  • Day 7

    Introduces dependent maps and indexed type families.

  • Day 8

    Proper effectful parsers and non-determinism in effect stacks.

  • Day 9

    Naive approach to handling the first graph traversal problem.

  • Day 10

    Introduce our Digits, dependent pattern matching on integers as lists of digits.

  • Day 11

    Introduces refinement types

  • Day 12

    New Parser Effect stack and DLists

  • Day 13

    Naive ring buffer and parameters blocks²

  • Day 14

    Introduction to streams, infinite collections of data

References

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.

This provides a defensively built API for constructing the overall Advent data structure that prevents registering a day/year twice or registering days/years out of order.

module Runner

import Control.Eff
import Structures.Dependent.FreshList

import public Util.Eff

%default total

Effectful Parts

The solution to each part of a day is run as an effectful computation, and as the effect stack is meant to be the same across both parts, only varying in the type of the error value for the Except effect, we construct a type level function to have a single source of truth. The err type can be any type with a Show implementation, but that constraint will be tacked on in the next step.

The Logger effect is provided for logging, and a Reader effect is provided to pass in the input, 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 will come in handy if a part needs IO for performance reasons.

||| The effect type is the same in boths parts one and two, modulo potentially
||| different error types, so we calucate it here
public export
PartEff : (err : Type) -> List (Type -> Type)
PartEff err =
  [IO, Except err, Logger, ReaderL "input" String]

The Day Record

The Day type groups together an effectful part1 computation, an optional effectful part2 computation, and the day number, with some type wrangling to get the type system out of our way.

part1 and part2 are allowed independent output and error types, and this record captures Show implementations for those output and error types so that we can display them in Main, where the Day is consumed, without having to actually know what the types are.

It is often useful to pass a bit of context, such as the data structures resulting from parsing, between part1 and part2. This is achieved through the erased ctx type, which is totally opaque to the runner. The code in Main will provide the value of the ctx type produced as part of the output of part1 and as the input of part2.

||| Model solving a single day
public export
record Day where
  constructor MkDay
  day : Nat
  {0 out1, out2, err1, err2 : Type}
  {auto showOut1 : Show out1}
  {auto showOut2 : Show out2}
  {auto showErr1 : Show err1}
  {auto showErr2 : Show err2}
  part1 : Eff (PartEff err1) (out1, ctx)
  part2 : Maybe (ctx -> Eff (PartEff err2) out2)
%name Day day, day2, day3

Smarter Constructors

The default MkDay constructor is slightly cumbersome to use, always requiring something for the part2 slot, even if there isn't a part 2 yet, and requiring that part2 be wrapped in a Just when there is one. We provide a pair of constructors for the case where there is only a part1, as well as one for when there is a part1 and a part2.

namespace Day

First

The First constructor only accepts a part1, it does the work of filling in part2 with Nothing and setting all of part2's type arguments to ().

  ||| Constructor for a day with only part one ready to run
  public export
  First : Show err => Show out =>
    (day : Nat) -> (part1 : Eff (PartEff err) (out, ctx'))
    -> Day
  First day part1 =
    MkDay day part1 Nothing {out2 = ()} {err2 = ()}

Both

The Both constructor does less heavy lifting, the only thing it needs to do is wrap part2 in a Just.

  ||| Constructor for a day with both parts ready to run
  public export
  Both : Show o1 => Show o2 => Show e1 => Show e2 =>
    (day : Nat) -> (part1 : Eff (PartEff e1) (o1, ctx')) ->
    (part2 :ctx' -> Eff (PartEff e2) o2)
    -> Day
  Both day part1 part2 =
    MkDay day part1 (Just part2)

Freshness

We will be using a Fresh List from the structures package to build our API defensively against duplicate days and cosmetically annoying out of order day registration. A Fresh List structurally only allows you to prepend/cons an element onto it when it satisfies some freshness criteria relative to the elements already contained in the list.

We compare the day numbers of the two Days using the less-than(<) relationship. Since we are operating on the start of the list when this comparison takes place, this enforces, through type checking, that the resulting Fresh List of Days is sorted in ascending order and that no two Days have the same day number.

||| Freshness criteria for days
|||
||| A day is fresh compared to another if the day number of the former day is
||| strictly less than the day number of the latter day
|||
||| This ensures that the days list is always in incrimenting sorted order
||| (since we are consing to the front of the list) with no duplicate days
public export
FreshDay : Day -> Day -> Bool
FreshDay x y = x.day < y.day

The Year Record

The Year record collects a number of Days into a single Fresh List for the year, also containing the year number for this collection.

||| Collect all the days in a given year
public export
record Year where
  constructor MkYear
  year : Nat
  days : FreshList FreshDay Day
%name Year year, year2, year3

Freshness

Much like Days are stored in a FreshList in Year, Years will be stored in a FreshList in Advent, so we need to provide a freshness criteria for Year as well.

We do so by applying the less-than relationship against the year number of the two Years, for the same reasons and with the same results as with FreshDay.

||| Freshness criteria for years
|||
||| A year is fresh compared to another if the year number of the former year is
||| strictly less than the year number of the latter year
|||
||| This ensures that the years list is always in incrimenting sorted order
||| (since we are consing to the front of the list) with no duplicate years
public export
FreshYear : Year -> Year -> Bool
FreshYear x y = x.year < y.year

The Advent Record

The Advent record collects a number of Years in much the same way that Year collects a number of days.

||| Collect all years
public export
record Advent where
  constructor MkAdvent
  years : FreshList FreshYear Year
%name Advent advent, advent2, advent3

Methods

namespace Advent

locate

This is a utility function that searches the FreshList of Years for the provided year number, then searches the resulting Year, if one exists, for the provided day number.

We don't have to worry about potentially encountering duplicates here because of the freshness restriction.

  ||| Attempt to locate `Day` entry corresponding to the provided day and year numbers
  export
  locate : (year, day : Nat) -> Advent -> Maybe Day
  locate year day advent = do
    year <- find (\x => x.year == year) advent.years
    find (\x => x.day == day) year.days

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 for the definitions of the Day, Year, and Advent data types.

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.

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.

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.

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

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

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.

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.

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

  (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 Logger into the effects list.

  -- If the verbose flag is set, hook up the logging writer to stderr
  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

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.

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

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

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

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

  where

Lower logging into the IO component of the effect

Makes use of Logger's handleLoggerIO function to "lower" logging actions into IO within the effect.

    -- Lowers logging into IO within the effect using the given IO function
    handleLog :
      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

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.

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

Utility functions

This module contains functions that extend the functionality of standard data types, other types of utility functionality get their own module

module Util

import Data.SortedSet
import Data.String
import Data.List.Lazy
import Data.List1
import Data.Vect
import Data.Fin

%default total

Foldable

General utility functions for foldables

minBy

  ||| Get the minimum element of a collection using the provided comparison
  ||| function and seed value
  export
  minBy : Foldable f => (cmp : a -> a -> Ordering) -> (acc : a) -> f a -> a
  minBy cmp acc x = 
    foldl 
      (\acc, e => 
        case e `cmp` acc of
          LT => e
          _ => acc)
      acc x

  ||| Get the maximum element of a collection using the provided comparison
  ||| function and seed value
  export
  maxBy : Foldable f => (cmp : a -> a -> Ordering) -> (acc : a) -> f a -> a
  maxBy cmp acc x = 
    foldl 
      (\acc, e => 
        case e `cmp` acc of
          GT => e
          _ => acc)
      acc x

Functions

repeatN

Recursively applies f to seed N times

export
repeatN : (times : Nat) -> (f : a -> a) -> (seed : a) -> a
repeatN 0 f seed = seed
repeatN (S times') f seed = repeatN times' f (f seed)

Either

mapLeft

Applies a function to the contents of a Left if the value of the given Either is actually a Left, otherwise, leaves Rights untouched.

  export
  mapLeft : (f : a -> b) -> Either a c -> Either b c
  mapLeft f (Left x) = Left (f x)
  mapLeft f (Right x) = Right x

List

contains

Returns True if the list contains the given value

  export
  contains : Eq a => a -> List a -> Bool
  contains x [] = False
  contains x (y :: xs) = 
    if x == y 
      then True
      else contains x xs

rotations

Provides all the 'rotations' of a list.

Example:

rotations [1, 2, 3] == [[1, 2, 3], [3, 1, 2], [2, 3, 1]]

  export
  rotations : List a -> List (List a) 
  rotations xs = rotations' (length xs) xs []
    where
      rotations' : Nat -> List a -> (acc : List (List a)) -> List (List a)
      rotations' 0 xs acc = acc
      rotations' (S k) [] acc = acc
      rotations' (S k) (x :: xs) acc = 
        let next = xs ++ [x]
        in rotations' k next (next :: acc)

permutations

Lazily generate all of the permutations of a list

  export
  permutations : List a -> LazyList (List a)
  permutations [] = pure []
  permutations xs = do
    (head, tail) <- select xs
    tail <- permutations (assert_smaller xs tail)
    pure $ head :: tail
    where 
      consSnd : a -> (a, List a) -> (a, List a)
      consSnd x (y, xs) = (y, x :: xs)
      select : List a -> LazyList (a, List a)
      select [] = []
      select (x :: xs) = (x, xs) :: map (consSnd x) (select xs)

Vect

permutations

Lazily generate all the permutations of a Vect

  export
  permutations : Vect n a -> LazyList (Vect n a)
  permutations [] = []
  permutations [x] = [[x]]
  permutations (x :: xs) = do
    (head, tail) <- select (x :: xs)
    tail <- permutations tail
    pure $ head :: tail
    where
      consSnd : a -> (a, Vect m a) -> (a, Vect (S m) a)
      consSnd x (y, xs) = (y, x :: xs)
      select : Vect (S m) a -> LazyList (a, Vect m a)
      select [y] = [(y, [])]
      select (y :: (z :: ys)) = 
        (y, z :: ys) :: map (consSnd y) (select (z :: ys))

minBy and maxBy

  ||| Get the minimum element of a non-empty vector by using the provided
  ||| comparison function 
  export
  minBy : (f : a -> a -> Ordering) -> Vect (S n) a -> a
  minBy f (x :: xs) = Foldable.minBy f x xs

  ||| Get the maximum element of a non-empty vector by using the provided
  ||| comparison function 
  export
  maxBy : (f : a -> a -> Ordering) -> Vect (S n) a -> a
  maxBy f (x :: xs) = Foldable.maxBy f x xs

Convert a list to a vect as a sigma type

  export
  listToVect : List a -> (n : Nat ** Vect n a)
  listToVect xs = (length xs ** fromList xs)

Fin

  ||| Decriment a Fin, wrapping on overflow
  export
  unfinS : {n : _} -> Fin n -> Fin n
  unfinS FZ = last
  unfinS (FS x) = weaken x

Vectors

Define some operations for pairs of numbers, treating them roughly like vectors

Addition and Subtraction

  public export
  (>+<) : Num a => (x, y : (a, a)) -> (a, a)
  (x_1, x_2) >+< (y_1, y_2) = (x_1 + y_1, x_2 + y_2)

  public export
  (>-<) : Neg a => (x, y : (a, a)) -> (a, a)
  (x_1, x_2) >-< (y_1, y_2) = (x_1 - y_1, x_2 - y_2)

Set

Extend Data.SortedSet

length

Count the number of elements in a sorted set

  export
  length : SortedSet k -> Nat
  length x = foldl (\acc, e => acc + 1) 0 x

String

Extend Data.String

isSubstr

Returns True if needle is a substring of haystack

We first check to see if the needle is a prefix of the top level haystack, before calling into a tail recursive helper function that peels one character off of the string at a time, checking if the needle is a prefix at each step.

  export
  isSubstr : (needle, haystack : String) -> Bool
  isSubstr needle haystack = 
    if needle `isPrefixOf` haystack 
      then True
      else isSubstr' haystack
    where
    isSubstr' : String -> Bool
    isSubstr' str with (asList str)
      isSubstr' "" | [] = False
      isSubstr' (strCons c str) | (c :: x) = 
        if needle `isPrefixOf` str
          then True
          else isSubstr' str | x

Lazy List

Cartesian product

Lazily take the cartesian product of two foldables

  export
  cartProd : Foldable a => Foldable b => a e -> b f -> LazyList (e, f)
  cartProd x y = 
    let y = foldToLazy y
    in foldr (\e, acc => combine e y acc) [] x
    where
      foldToLazy : Foldable a' => a' e' -> LazyList e'
      foldToLazy x = foldr (\e, acc => e :: acc) [] x
      combine : e -> LazyList f -> LazyList (e, f) -> LazyList (e, f)
      combine x [] rest = rest
      combine x (y :: ys) rest = (x, y) :: combine x ys rest

Concat

Lazily concatenate a LazyList of LazyLists

  export
  lazyConcat : LazyList (LazyList a) -> LazyList a
  lazyConcat [] = []
  lazyConcat (x :: xs) = x ++ lazyConcat xs

Group

Lazily group a LazyList

  export
  lazyGroup : Eq a => LazyList a -> LazyList (List1 a)
  lazyGroup [] = []
  lazyGroup (x :: xs) = lazyGroup' xs x (x ::: [])
    where
      lazyGroup' : LazyList a -> (current : a) -> (acc : List1 a)
        -> LazyList (List1 a)
      lazyGroup' [] current acc = [acc]
      lazyGroup' (y :: ys) current acc@(head ::: tail) = 
        if y == current
          then lazyGroup' ys current (head ::: (y :: tail))
          else acc :: lazyGroup (y :: ys)

length

Calculate the length of a LazyList

  export
  length : LazyList a -> Nat
  length = length' 0
    where
      length' : Nat -> LazyList a -> Nat
      length' k [] = k
      length' k (x :: xs) = length' (S k) xs

Effects utilities

Contains utility functions extending the functionality of the eff package.

module Util.Eff

import Control.Eff
import Data.Subset
import Text.ANSI

import System
import System.File

%default total

Logging

Log Levels

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.

public export
data Level : Type where
  Err : Level
  Warn : Level
  Info : Level
  Debug : Level
  Trace : Level
  Other : (n : Nat) -> {auto _ : n `GT` 4} -> Level

Convert a Level into a colorized tag

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)

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.

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.

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

Provide a family of effectful actions that emit log messages at the different log levels.

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

export
logAt : Has Logger fs => Level -> Lazy String -> Eff fs ()
logAt level x = send $ Log level x

Choose

Lifts any foldable data structure into the Choose effect, enabling the style of nondeterministic programming from the list monad

export
oneOf : Has (Choose) fs => Foldable f =>
    f a -> Eff fs a
oneOf x = foldl oneOf' empty x
  where
  oneOf' : Eff fs a -> a -> Eff fs a
  oneOf' acc val = pure val `alt` acc

Lifts any foldable of effectful computations into the Choose effect much the same as oneOf

export
oneOfM : Has (Choose) fs => Foldable f =>
    f (Eff fs a) -> Eff fs a
oneOfM x = foldl alt empty x

Subset

Reorder the first two elements of the first argument of a subset

public export
subsetReorderLeft : Subset (x :: g :: xs) ys -> Subset (g :: x :: xs) ys
subsetReorderLeft (e :: (e' :: subset)) = e' :: e :: subset

Add the same element to both arguments of a subset

public export
subsetConsBoth : {0 xs, ys : List a} -> {0 g : a} -> Subset xs ys 
  -> Subset (g :: xs) (g :: ys)
subsetConsBoth {xs = []} {ys = ys} [] = [Z]
subsetConsBoth {xs = (x :: xs)} {ys} (e :: subset) = 
  let rest = S e :: subsetConsBoth subset {g}
  in subsetReorderLeft rest

A list is always a subset of itself

public export
subsetReflexive : {xs : List a} -> Subset xs xs
subsetReflexive {xs = []} = []
subsetReflexive {xs = (x :: xs)} = 
  let rest = subsetReflexive {xs} 
  in subsetConsBoth rest

If xs is a subset of ys, then it is also a subset of ys + g

public export
subsetConsRight : {0 g: _} -> {0 xs, ys: _} -> Subset xs ys -> Subset xs (g :: ys)
subsetConsRight {xs = []} {ys = ys} [] = []
subsetConsRight {xs = (x :: xs)} {ys} (e :: subset) = 
  S e :: subsetConsRight subset {g}

xs is always a subset of xs + g

public export
trivialSubset : {0 g : a} -> {xs : List a} -> Subset xs (g :: xs)
trivialSubset = subsetConsRight subsetReflexive

fs - f is always a subset of f

public export
minusLemma : {fs : List a} -> {0 x : a} -> {auto prf : Has x fs} 
  -> Subset (fs - x) fs
minusLemma {fs = (_ :: vs)} {prf = Z} = trivialSubset
minusLemma {fs = (w :: vs)} {prf = (S y)} = 
  let rest = minusLemma {fs = vs} {prf = y}
  in subsetConsBoth rest

Effects utilities

Contains utility functions extending the functionality of the eff package.

module Util.Eff

import Control.Eff
import Data.Subset
import Text.ANSI

import System
import System.File

%default total

Logging

Log Levels

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.

public export
data Level : Type where
  Err : Level
  Warn : Level
  Info : Level
  Debug : Level
  Trace : Level
  Other : (n : Nat) -> {auto _ : n `GT` 4} -> Level

Convert a Level into a colorized tag

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)

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.

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.

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

Provide a family of effectful actions that emit log messages at the different log levels.

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

export
logAt : Has Logger fs => Level -> Lazy String -> Eff fs ()
logAt level x = send $ Log level x

Choose

Lifts any foldable data structure into the Choose effect, enabling the style of nondeterministic programming from the list monad

export
oneOf : Has (Choose) fs => Foldable f =>
    f a -> Eff fs a
oneOf x = foldl oneOf' empty x
  where
  oneOf' : Eff fs a -> a -> Eff fs a
  oneOf' acc val = pure val `alt` acc

Lifts any foldable of effectful computations into the Choose effect much the same as oneOf

export
oneOfM : Has (Choose) fs => Foldable f =>
    f (Eff fs a) -> Eff fs a
oneOfM x = foldl alt empty x

Subset

Reorder the first two elements of the first argument of a subset

public export
subsetReorderLeft : Subset (x :: g :: xs) ys -> Subset (g :: x :: xs) ys
subsetReorderLeft (e :: (e' :: subset)) = e' :: e :: subset

Add the same element to both arguments of a subset

public export
subsetConsBoth : {0 xs, ys : List a} -> {0 g : a} -> Subset xs ys 
  -> Subset (g :: xs) (g :: ys)
subsetConsBoth {xs = []} {ys = ys} [] = [Z]
subsetConsBoth {xs = (x :: xs)} {ys} (e :: subset) = 
  let rest = S e :: subsetConsBoth subset {g}
  in subsetReorderLeft rest

A list is always a subset of itself

public export
subsetReflexive : {xs : List a} -> Subset xs xs
subsetReflexive {xs = []} = []
subsetReflexive {xs = (x :: xs)} = 
  let rest = subsetReflexive {xs} 
  in subsetConsBoth rest

If xs is a subset of ys, then it is also a subset of ys + g

public export
subsetConsRight : {0 g: _} -> {0 xs, ys: _} -> Subset xs ys -> Subset xs (g :: ys)
subsetConsRight {xs = []} {ys = ys} [] = []
subsetConsRight {xs = (x :: xs)} {ys} (e :: subset) = 
  S e :: subsetConsRight subset {g}

xs is always a subset of xs + g

public export
trivialSubset : {0 g : a} -> {xs : List a} -> Subset xs (g :: xs)
trivialSubset = subsetConsRight subsetReflexive

fs - f is always a subset of f

public export
minusLemma : {fs : List a} -> {0 x : a} -> {auto prf : Has x fs} 
  -> Subset (fs - x) fs
minusLemma {fs = (_ :: vs)} {prf = Z} = trivialSubset
minusLemma {fs = (w :: vs)} {prf = (S y)} = 
  let rest = minusLemma {fs = vs} {prf = y}
  in subsetConsBoth rest

Array Wrappers

module Array

import Data.IOArray
import Data.Vect
import Data.List.Lazy
import Data.Fin
import Data.Iterable
import Decidable.Equality
import Control.WellFounded

%default total
%hide Prelude.Types.elem

Provide some wrappers over the standard library IO arrays, using plenty of unsafe operations along the way.

Internal Utility Functions

Unsafely unwrap a Maybe, making the assumption that it is a Just.

%unsafe
unwrapUnsafe : Maybe a -> a
unwrapUnsafe x = assert_total $ unwrapUnsafe' x
  where 
    partial
    unwrapUnsafe' : Maybe a -> a
    unwrapUnsafe' (Just x) = x

Insert an element into an IOArray at the index described by the given Fin.

insertPair : IOArray e -> (e, Fin n) -> IO ()
insertPair arr (elem, idx) = do
  let idx : Int = cast . finToInteger $ idx
  _ <- writeArray arr idx elem
  pure ()

Tail safe monadic recursion with lazy lists

Generate all of the fins of a given size, lazily.

allFins : (n : Nat) -> LazyList (Fin n)
allFins 0 = []
allFins (S k) = FZ :: map FS (allFins k)

LazyLists have a size

Sized (LazyList e) where
  size [] = 0
  size (x :: xs) = S (size xs)

Convert a Vect to a LazyList

vectLazy : Vect n e -> LazyList e
vectLazy [] = []
vectLazy (x :: xs) = x :: vectLazy xs

LazyLists are iterable

refl : {k : Nat} -> LTE k k
refl = reflexive {x = k}

Iterable (LazyList a) a where
  iterM accum done ini seed =
    trSized seed ini $
      \case Nil    => pure . Done . done
            h :: t => map (Cont t refl) . accum h

Immutable arrays

Immutable arrays created from vectors that provide constant time indexing and slicing operations.

As an invariant of the the type, every "slot" in the inner IOArray must always be a Just, unsafe operations are performed that depend on that.

  ||| An immutable array of length `n`
  export
  data IArray : Nat -> Type -> Type where
    MkIArray : (size : Nat) -> (offset : Int) -> (inner : IOArray e) 
      -> IArray size e
  %name IArray xs, ys, zs

Basic Interface

Indexing operation

  export
  index : (idx : Fin n) -> IArray n e -> e
  index idx (MkIArray size offset inner) = unsafePerformIO index' 
    where
      index' : IO e
      index' = do
        -- Convert the index to an Int for use in the IO array
        let idx : Int = cast . finToInteger $ idx
        map unwrapUnsafe $ readArray inner (idx + offset) 

Getting the length of an IArray, as well as a proof of correctness for the length function

  export
  length : IArray n e -> Nat
  length (MkIArray n _ inner) = n
  
  export
  lengthCorrect : (array : IArray n e) -> length array = n
  lengthCorrect (MkIArray n _ inner) = Refl

Basic conversion operations

  export
  fromVect : {n : Nat} -> Vect n e -> IArray n e
  fromVect xs = unsafePerformIO fromVect'
    where
      fromVect' : IO $ IArray n e
      fromVect' = do
        let pairs = zip (vectLazy xs) (allFins n)
        array <- newArray (cast n)
        forM_ (insertPair array) pairs
        pure $ MkIArray n 0 array
  
  export
  replicate : (n : Nat) -> e -> IArray n e
  replicate n x = unsafePerformIO replicate'
    where
      insertR : IOArray e -> Fin n -> IO ()
      insertR arr idx = do
        let idx : Int = cast . finToInteger $ idx
        _ <- writeArray arr idx x
        pure ()
      replicate' : IO $ IArray n e
      replicate' = do
        array <- newArray (cast n)
        forM_ (insertR array) (Array.allFins n)
        pure $ MkIArray n 0 array

  export
  toVect : IArray n e -> Vect n e
  toVect xs = 
    let xs' : IArray (length xs) e = rewrite lengthCorrect xs in xs
        values : Vect _ e = map (flip index $ xs') (allFins _)
    in rewrite sym $ lengthCorrect xs in values
  
  arrayToList : IArray n e -> List e
  arrayToList xs = 
    let xs' : IArray (length xs) e = rewrite lengthCorrect xs in xs
    in map (flip index $ xs') (allFins (length xs))

Unsafely create an array from a lazy list of values, for internal use only. Will cause crashes if the provided LazyList isn't the right length.

  %unsafe
  unsafeFromLazy : {n : Nat} -> LazyList e -> IO (IArray n e)
  unsafeFromLazy xs = do
    array <- newArray (cast n)
    let pairs = zip xs (allFins n)
    forM_ (insertPair array) pairs
    pure $ MkIArray _ 0 array

Typical drop and take operations, implemented in constant time

  -- TODO: Minimize whatever compiler bug is requiring us to use this
  newOffset : Nat -> Int -> Int
  newOffset k i = cast k + i

  export
  drop : (n : Nat) -> IArray (n + m) e -> IArray m e
  drop n xs@(MkIArray _ offset inner) = 
    believe_me $ MkIArray (length xs `minus` n) (newOffset n offset) inner

  export
  drop' : (n : Nat) -> IArray l e -> IArray (minus l n) e
  drop' n (MkIArray l offset inner) = 
    if n >= l
      then believe_me $ fromVect [] {e}
      else MkIArray (l `minus` n) (newOffset n offset) inner
  
  export
  take : (n : Nat) -> IArray (n + m) e -> IArray n e
  take n (MkIArray _ offset inner) = MkIArray n offset inner

A view for pattern matching on IArrays as if they were lists

  namespace View
    public export
    data AsList : IArray n e -> Type where
      Nil : {0 tail : IArray 0 e} -> AsList tail
      (::) : {0 xs : IArray (S n) e} -> {rest : IArray n e} 
        -> (head : e) -> (tail : Lazy (AsList rest)) -> AsList xs
    
    public export 
    asList : (xs : IArray n e) -> AsList xs
    asList (MkIArray 0 offset inner) = []
    asList xs@(MkIArray (S k) offset inner) = 
      let head = 0 `index` xs
          rest = drop 1 xs
      in head :: (asList rest)

Convert to a LazyList using our view

  export
  toLazy : IArray n e -> LazyList e
  toLazy xs with (asList xs)
    toLazy xs | [] = []
    toLazy xs | (head :: tail) = 
      head :: toLazy _ | tail

Typical filtering and finding interface

  -- Don't know if this one is really worth optimizing
  export
  filter : (e -> Bool) -> IArray n e -> (p : Nat ** IArray p e)
  filter f xs = 
    let (_ ** ps) = filter f (toVect xs)
    in (_ ** fromVect ps)
 
  export
  find : (e -> Bool) -> IArray n e -> Maybe e
  find f xs with (asList xs)
    find f xs | [] = Nothing
    find f xs | (head :: tail) = 
      if f head
        then Just head
        else find f _ | tail
 
  export
  findIndex : (e -> Bool) -> IArray n e -> Maybe (Fin n)
  findIndex f xs = 
    let indexed = zip (toLazy xs) (allFins (length xs))
    in findIndex' f indexed
    where
      findIndex' : (e -> Bool) -> LazyList (e, Fin (length xs)) -> Maybe (Fin n)
      findIndex' f [] = Nothing
      findIndex' f ((e, idx) :: ys) = 
        if f e
          then rewrite sym $ lengthCorrect xs in Just idx
          else findIndex' f ys
 
  export
  findIndices : (e -> Bool) -> IArray n e -> List (Fin n)
  findIndices f xs@(MkIArray n _ _) = 
    let pairs = zip (toLazy xs) (allFins n)
    in toList . map snd . filter (f . fst) $ pairs

Interface Implementations

Provide a Foldable implementation by performing indexing within the context of unsafePerformIO.

  export
  Foldable (IArray n) where
    foldl f acc_val (MkIArray n offset inner) = unsafePerformIO $ foldl'
      where 
        liftF : Fin n -> acc -> IO acc
        liftF idx acc_val = do
          let idx : Int = cast . finToInteger $ idx
          val <- map unwrapUnsafe $ readArray inner (idx + offset)
          pure $ f acc_val val
        foldl' : IO acc
        foldl' = iterM liftF id acc_val (Array.allFins n)
    foldr f acc_val (MkIArray n offset inner) = unsafePerformIO $ foldr'
      where
        liftF : Fin n -> acc -> IO acc
        liftF idx acc_val = do
          let idx : Int = cast . finToInteger $ idx
          val <- map unwrapUnsafe $ readArray inner (idx + offset)
          pure $ f val acc_val
        foldr' : IO acc
        -- TODO: Make a lazy reverse allFins function so we aren't instantiating
        -- the full index list here
        foldr' = iterM liftF id acc_val (reverse $ List.allFins n)
    toList = arrayToList

Provide implementations of Eq, Ord, and DecEq in terms of our AsList view. The DecEq implementation requires use of unsafe believe_me, as arrays are primitive types the compiler has no insight into the structure of.

  export
  Eq e => Eq (IArray n e) where
    xs == ys = (toLazy xs) == (toLazy ys)
  
  export
  Ord e => Ord (IArray n e) where
    compare xs ys = compare (toLazy xs) (toLazy ys)
  
  -- TODO : Optimize IArray DecEq
  decEq' : DecEq e => {m : Nat} -> (xs, ys : IArray m e) -> Dec (xs = ys)
  decEq' xs ys with (asList xs, asList ys)
    decEq' xs ys | ([], []) = believe_me $ the (xs = xs) Refl
    decEq' xs ys | ((h_x :: t_x), (h_y :: t_y)) = 
      case decEq h_x h_y of
        Yes prf => 
          believe_me $ decEq' _ _ | (t_x, t_y)
        No contra => believe_me contra

  export
  DecEq e => DecEq (IArray n e) where
    decEq xs@(MkIArray n _ _) ys = decEq' xs ys

Provide Functor, Applicative, Monad, and Traverseable implementations by building a new array in an IO context

  map' : (f : a -> b) -> IArray n a -> IO (IArray n b)
  map' f xs@(MkIArray n _ _) = do
    array <- newArray (cast n)
    let pairs = zip (map f . toLazy $ xs) (Array.allFins n)
    forM_ (insertPair array) pairs
    pure $ MkIArray n 0 array

  export
  Functor (IArray k) where
    map f xs = unsafePerformIO $ map' f xs
  
  apply' : {n : Nat} -> IArray n (a -> b) -> IArray n a -> IO (IArray n b)
  apply' fs xs = do
    array <- newArray (cast n)
    let applied = map (\(f, x) => f x) $ zip (toLazy fs) (toLazy xs)
    let pairs = zip applied (allFins n)
    forM_ (insertPair array) pairs
    pure $ MkIArray n 0 array
 
  -- Applicative requires the length of the array to be available at runtime at
  -- the type level for `replicate`
  export
  {k : Nat} -> Applicative (IArray k) where
    pure = replicate _
    fs <*> xs = unsafePerformIO $ apply' fs xs

  -- Like `Vect`'s `join`, this takes the diagonal elements
  export
  {k : Nat} -> Monad (IArray k) where 
    join xs = 
      let lazys = join' . map toLazy $ toLazy xs
      in assert_total $ unsafePerformIO $ unsafeFromLazy lazys
      where
        covering
        join' : LazyList (LazyList a) -> LazyList a
        join' [] = []
        join' ([] :: y) = []
        join' ((x :: _) :: xs) = 
          x :: join' (map (drop 1) xs)
    -- join xs = fromVect . join . map toVect . toVect $ xs
 
  -- TODO: Maybe take another pass at optimizing this? 
  export
  Traversable (IArray k) where 
    traverse fun xs@(MkIArray k _ _) = 
      map (unsafePerformIO . unsafeFromLazy . fromList) 
      . Prelude.traverse fun 
      . toList 
      $ xs

Provide a Show implementation in terms of our AsList view through the asLazy wrapper.

  export
  Show e => Show (IArray n e) where
    show xs = 
      let elements = map show $ toLazy xs
      in case elements of
        [] => "[]"
        (x :: xs) => "[\{join' xs x}]"
      where
        join' : LazyList String -> (acc : String) -> String
        join' [] acc = acc
        join' (x :: []) acc = "\{acc}, \{x}"
        join' (x :: (y :: xs)) acc = 
          join' (y :: xs) "\{acc}, \{x}"

Provide a Zippable implementation by roundtripping through a Vect. This isn't the most efficient, but this provides a workable starter implementation.

  export
  Zippable (IArray k) where 
    zipWith f xs@(MkIArray k _ _) ys = 
      unsafePerformIO . unsafeFromLazy $ zipWith f (toLazy xs) (toLazy ys)
    zipWith3 f xs@(MkIArray k _ _) ys zs = 
      unsafePerformIO . unsafeFromLazy $ zipWith3 f (toLazy xs) (toLazy ys) (toLazy zs)
    unzipWith f xs@(MkIArray k _ _) = 
      let (xs, ys) = unzipWith f (toLazy xs)
      in (unsafePerformIO . unsafeFromLazy $ xs, 
          unsafePerformIO . unsafeFromLazy $ ys)
    unzipWith3 f xs@(MkIArray k _ _) = 
      let (xs, ys, zs) = unzipWith3 f (toLazy xs)
      in (unsafePerformIO . unsafeFromLazy $ xs, 
          unsafePerformIO . unsafeFromLazy $ ys, 
          unsafePerformIO . unsafeFromLazy $ zs)

Provide Semigroup and Monoid implementations, matching those for Vect, in terms of our other interfaces.

  export
  Semigroup a => Semigroup (IArray k a) where 
    xs <+> ys = zipWith (<+>) xs ys
  
  -- Monoid requires the length argument to be available at runtime for 
  -- `replicate` to work
  export
  {k : Nat} -> Monoid a => Monoid (IArray k a) where 
    neutral = replicate _ neutral

Unit tests

IArray

-- @@test IArray RoundTrip
iRoundTrip : IO Bool
iRoundTrip = do
  let test_vect : Vect _ Nat = [1, 2, 3, 4, 5]
  putStrLn "test_vect: \{show test_vect}"
  let xs = fromVect test_vect
  putStrLn "xs: \{show xs}"
  let round_tripped = toVect xs 
  putStrLn "round_tripped: \{show round_tripped}"
  pure $ test_vect == round_tripped

-- @@test IArray drop/take
iDropTake : IO Bool
iDropTake = do
  let test = fromVect [1, 2, 3, 4, 5]
  putStrLn "test: \{show test}"
  let dropped = drop 2 test
  putStrLn "dropped: \{show dropped}"
  let taked = take 3 test
  putStrLn "taked: \{show taked}"
  pure $ (toVect dropped) == [3, 4, 5] && (toVect taked) == [1, 2, 3]

-- @@test IArray toLazy
iLazy : IO Bool
iLazy = do
  let test_vect : Vect _ Nat = [1, 2, 3, 4, 5]
  let test_array = fromVect test_vect
  putStrLn "test_array: \{show test_array}"
  let output_lazy = toLazy test_array
  putStrLn "output_lazy: \{show output_lazy}"
  pure $ vectLazy test_vect == output_lazy

-- @@test IArray foldl/foldr
iFold : IO Bool
iFold = do
  let test = fromVect [1, 2, 3, 4, 5]
  putStrLn "test: \{show test}"
  let foldl_test = foldl (flip (::)) [] test
  putStrLn "foldl_test: \{show foldl_test}"
  let foldr_test = foldr (::) [] test
  putStrLn "foldr_test: \{show foldr_test}"
  pure $ foldl_test == [5, 4, 3, 2, 1] && foldr_test == [1, 2, 3, 4, 5]

-- @@test IArray functor
iFunctor : IO Bool
iFunctor = do
  let test = fromVect [1, 2, 3, 4, 5]
  putStrLn "test: \{show test}"
  let output = map (+ 1) test
  putStrLn "output: \{show output}"
  pure $ toVect output == [2, 3, 4, 5, 6]
  
-- @@test IArray show
iShow : IO Bool
iShow = do
  let test = fromVect [1, 2, 3, 4, 5]
  putStrLn "test: \{show test}"
  let empty : IArray _ Nat = fromVect []
  putStrLn "empty: \{show empty}"
  let singleton = fromVect [1]
  putStrLn "singleton: \{show singleton}"
  pure $ 
    show test == "[1, 2, 3, 4, 5]"  
    && show empty == "[]"  
    && show singleton == "[1]"  

-- @@test IArray monad
iMonad : IO Bool
iMonad = do
  let test_vect : Vect 3 (Vect 3 Nat) = [[1, 2, 3], [4, 5, 6], [7, 8 ,9]]
  let test_array = fromVect $ map fromVect test_vect
  let vect_out = join test_vect
  let array_out = join test_array
  putStrLn "vect: \{show vect_out} array: \{show array_out}"
  pure $ toVect array_out == vect_out

Parsing Utilties

module Parser

import public Parser.Interface as Parser
import public Parser.ParserState as Parser

The interface of a Parser

module Parser.Interface
  
import public Data.List1

import public Parser.ParserState

import public Control.Eff

export infixr 4 >|
export infixr 5 >&

Parser Errors

Combine the parser state at time of error with an error message.

public export
data ParseError : Type where
  -- TODO: Rename this constructor
  MkParseError : (state : ParserInternal Id) -> (message : String) -> ParseError
  BeforeParse : (message : String) -> ParseError
  NestedErrors : (state : ParserInternal Id) -> (message : String)
    -> (rest : List ParseError) -> ParseError

Type Alias

public export
Parser : Type -> Type
Parser a = Eff [ParserState, Except ParseError] a

Error Generation

Provide a few effectful actions to generate an error from an error message, and either return it or throw it.

export
parseError : Has ParserState fs => (message : String) -> Eff fs ParseError
parseError message = do
  state <- save
  pure $ MkParseError state message

export
throwParseError : Has ParserState fs => Has (Except ParseError) fs =>
  (message : String) -> Eff fs a
throwParseError message = do
  err <- parseError message
  throw err

export
guardMaybe : Has ParserState fs => Has (Except ParseError) fs =>
  (message : String) -> Eff fs (Maybe a) -> Eff fs a
guardMaybe message x = do
  Just x <- x
    | _ => throwParseError message
  pure x

export
replaceError : (message : String) -> Parser (a -> Parser b)
replaceError message = do
  state <- save
  pure (\_ => throw $ MkParseError state message)

Running a parser

We will use the phrasing "rundown" to refer to running all the effects in the parser effect stack except ParserState, which is left in the effect stack to facilitate handling in the context of another monad or effect stack, since it benefits from mutability.

Rundown a parser, accepting the first returning parse, which may be failing or succeding, and automatically generating a "no valid parses" message in the event no paths in the Choice effect produce a returning parse.

export
rundownFirst : (f : Parser a) -> Eff [ParserState] (Either ParseError a)
rundownFirst f = 
  runExcept f

Provide wrappers for rundownFirst for evaluating it in various contexts.

export
runFirstIO : HasIO io => MonadRec io =>
  (f : Parser a) -> String -> io (Either ParseError a)
runFirstIO f str = do
  Just state <- newInternalIO str
    | _ => pure . Left $ BeforeParse "Empty input"
  runEff (rundownFirst f) [handleParserStateIO state]

export
runFirstIODebug : (f : Parser a) -> String -> IO (Either ParseError a)
runFirstIODebug f str = do
  Just state <- newInternalIO str
    | _ => pure . Left $ BeforeParse "Empty input"
  runEff (rundownFirst f) [handleParserStateIODebug state]

export
runFirst : (f : Parser a) -> String -> Eff fs (Either ParseError a)
runFirst f str = do
  Just state <- pure $ newInternal str
    | _ => pure . Left $ BeforeParse "Empty input"
  (result, _) <- lift . runParserState state . rundownFirst $ f
  pure result

export
runFirst' : (f : Parser a) -> String -> Either ParseError a
runFirst' f str = extract $ runFirst f str {fs = []}

Utility functionality

Parser combinators

Try to run a computation in the context of the Parser effect stack, if it fails (via Except), reset the state and resort to the supplied callback

Also supply a version specialized to ignore the error value, returning Just a if the parse succeeds, and Nothing if it fails.

export
try : (f : Parser a) -> (err : ParseError -> Parser a) -> Parser a
try f err = do
  starting_state <- save
  result <- lift . runExcept $ f
  case result of
    Left error => do
      load starting_state
      err error 
    Right result => pure result

export
tryMaybe : (f : Parser a) -> Parser (Maybe a)
tryMaybe f = try (map Just f) (\_ => pure Nothing)
  
export
tryEither : (f : Parser a) -> Parser (Either ParseError a)
tryEither f = try (map Right f) (pure . Left)

Attempt to parse one of the given input parsers, in the provided order, invoking the provided error action on failure.

The state will not be modified when an input parser fails

export
oneOfE : (err : String) -> List (Parser a) -> Parser a
oneOfE err xs = do
  start <- save
  oneOfE' err start [] xs
  where
    oneOfE' : (err : String) -> (start : ParserInternal Id) 
      -> (errs : List ParseError) -> List (Parser a) -> Parser a
    oneOfE' err start errs [] = do
      throw $ NestedErrors start err (reverse errs) 
    oneOfE' err start errs (x :: xs) = do
      x <- tryEither x
      case x of
        Right val => pure val
        Left error => oneOfE' err start (error :: errs) xs

Attempt to parse 0+ of an item

export
many : (f : Parser a) -> Parser (List a)
many f = do
  Just next <- tryMaybe f
    | _ => pure []
  map (next ::) $ many f

Attempt to parse 1+ of an item, invoking the supplied error action on failure

export
atLeastOne : (err : ParseError -> Parser (List1 a)) -> (f : Parser a)
  -> Parser (List1 a)
atLeastOne err f = do
  Right next <- tryEither f
    | Left e => err e
  map (next :::) $ many f

Lift a parser producing a List or List1 of Char into a parser producing a String

-- TODO: Rename these
export
liftString : Parser (List Char) -> Parser String
liftString x = do
  xs <- x
  pure $ pack xs

export
liftString' : Parser (List1 Char) -> Parser String
liftString' x = liftString $ map forget x

Attempt to parse a specified character

export
charExact : Char -> Parser Char
charExact c = do
  result <- charExact' c
  case result of
    GotChar char => pure char
    GotError err => throwParseError "Got \{show err} Expected \{show c}"
    EndOfInput => throwParseError "End of input"

Attempt to parse one of a list of chars

export
theseChars : List Char -> Parser Char
theseChars cs = do
  pnote "Parsing one of: \{show cs}"
  result <- charPredicate (\x => any (== x) cs)
  case result of
    GotChar char => pure char
    GotError err => throwParseError "Got \{show err} Expected one of \{show cs}"
    EndOfInput => throwParseError "End of input"