advent/README.md

# 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

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](https://lists.sr.ht/~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](src/Runner.md)

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

- [Main](src/Main.md)

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

- [Util](src/Util.md)

  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](src/Util/Eff.md)

    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
  - [Day 1](src/Years/Y2015/Day1.md)

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

  - [Day 2](src/Years/Y2015/Day2.md)

    An early hint of effectful parsing.

  - [Day 3](src/Years/Y2015/Day3.md)

    Peculiarities of writing mutually recursive functions in dependently typed
    languages.

  - [Day 4](src/Years/Y2015/Day4.md)

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

  - [Day 5](src/Years/Y2015/Day5.md)

    First introduction to views and dependent pattern matching[^1].

  - [Day 6](src/Years/Y2015/Day6.md)

    Naive approach to handling the first 2d grid problem.

  - [Day 7](src/Years/Y2015/Day7.md)

    Introduces dependent maps and indexed type families.

  - [Day 8](src/Years/Y2015/Day8.md)

    Proper effectful parsers and non-determinism in effect stacks.

  - [Day 9](src/Years/Y2015/Day9.md)

    Naive approach to handling the first graph traversal problem.

  - [Day 10](src/Years/Y2015/Day10.md)

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

  - [Day 11](src/Years/Y2015/Day11.md)

    Introduces refinement types

## References

[^1]: Idris 2 Manual:
    [Views and the "with" rule](https://idris2.readthedocs.io/en/latest/tutorial/views.html#views-and-the-with-rule)