Initial commit

.gitignore

@@ -0,0 +1,3 @@
+build/
+inputs/
+*.*~

advent.ipkg

@@ -0,0 +1,55 @@
+package advent
+version = 0.1.0
+authors = "Nathan McCarty"
+-- maintainers =
+-- license =
+-- brief =
+-- readme =
+-- homepage =
+-- sourceloc =
+-- bugtracker =
+
+-- the Idris2 version required (e.g. langversion >= 0.5.1)
+-- langversion
+
+-- packages to add to search path
+depends = base
+        , contrib
+        , structures
+        , eff
+        , elab-util
+        , ansi
+        , if-unsolved-implicit
+
+-- modules to install
+modules = Runner
+        , Util
+        , Util.Eff
+
+-- main file (i.e. file to load at REPL)
+main = Main
+
+-- name of executable
+executable = "advent"
+-- opts =
+sourcedir = "src"
+-- builddir =
+-- outputdir =
+
+-- script to run before building
+-- prebuild =
+
+-- script to run after building
+-- postbuild =
+
+-- script to run after building, before installing
+-- preinstall =
+
+-- script to run after installing
+-- postinstall =
+
+-- script to run before cleaning
+-- preclean =
+
+-- script to run after cleaning
+-- postclean =

pack.toml

@@ -0,0 +1,9 @@
+[custom.all.advent]
+type = "local"
+path = "."
+ipkg = "advent.ipkg"
+
+[custom.all.structures]
+type = "local"
+path = "../structures"
+ipkg = "structures.ipkg"

src/Main.idr

@@ -0,0 +1,158 @@
+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
+
+data Flag = UseExample | Verbose
+%runElab derive "Flag" [Eq, Show]
+
+advent : Advent
+advent = MkAdvent [
+    y2015
+  ]
+
+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...]"
+
+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
+
+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
+
+||| 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)
+
+covering
+||| Actual main, as an effectful computation
+start : Eff [IO, Except Error] ()
+start = do
+  -- Read and parse arguments/options
+  args <- getArgs
+  let opts = getOpt Permute options (drop 1 args)
+  when (not . null $ opts.errors) $
+    throw (OptionsError opts.errors)
+  (year, day_n) <- argumentsToPair opts.nonOptions
+  -- 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
+  -- 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
+  -- Attempt to locate the provided day
+  Just day <- pure $ locate year day_n advent | _ => throw $ NoSuchDay year day_n
+  -- 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
+  -- 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
+  where
+    -- print to standard error
+    ePutStrLn : String -> IO ()
+    ePutStrLn str = do
+      _ <- fPutStrLn stderr str
+      pure ()
+    -- Decompose a writer, eases type inference
+    unwriter : WriterL "log" String a -> (a, String)
+    unwriter (Tell vw) = ((), vw)
+    -- 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
+
+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

src/Runner.idr

@@ -0,0 +1,88 @@
+module Runner
+
+import Control.Eff
+import Structures.Dependent.FreshList
+
+||| 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, WriterL "log" String, ReaderL "input" String]
+
+||| 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
+
+namespace Day
+  ||| 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 = ()}
+
+  ||| 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 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
+
+||| 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 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
+
+||| Collect all years
+public export
+record Advent where
+  constructor MkAdvent
+  years : FreshList FreshYear Year
+%name Advent advent, advent2, advent3
+
+namespace Advent
+  ||| 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

src/Util.idr

@@ -0,0 +1,10 @@
+module Util
+
+-----------------------------------
+-- Standard Data Type Extensions --
+-----------------------------------
+namespace Either
+  export
+  mapLeft : (f : a -> b) -> Either a c -> Either b c
+  mapLeft f (Left x) = Left (f x)
+  mapLeft f (Right x) = Right x

src/Util/Eff.idr

@@ -0,0 +1,26 @@
+module Util.Eff
+
+import Control.Eff
+import Text.ANSI
+
+-----------------------
+-- Logging Utilities --
+-----------------------
+namespace Logging
+  export
+  info : Has (WriterL "log" String) fs => 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 => 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 => String -> Eff fs ()
+  warn str =
+    let tag = show . bolden . show . colored Yellow $ "[WARN]"
+    in tellAt "log" (tag ++ ": " ++ str ++ "\n")

src/Years/Y2015.idr

@@ -0,0 +1,13 @@
+module Years.Y2015
+
+import Structures.Dependent.FreshList
+
+import Runner
+
+import Years.Y2015.Day1
+
+export
+y2015 : Year
+y2015 = MkYear 2015 [
+    day1
+  ]

src/Years/Y2015/Day1.idr

@@ -0,0 +1,11 @@
+module Years.Y2015.Day1
+
+import Control.Eff
+
+import Runner
+
+part1 : Eff (PartEff String) ((), ())
+
+export
+day1 : Day
+day1 = First 1 part1