0 | module Main
  1 |
  2 | import System
  3 | import System.Path
  4 | import System.File
  5 | import System.Directory
  6 | import System.Console.GetOpt
  7 | import Data.String
  8 | import Data.Vect
  9 |
 10 | import Control.Eff
 11 | import Derive.Prelude
 12 |
 13 | import Structures.Dependent.FreshList
 14 |
 15 | import Runner
 16 | import Util
 17 | import Util.Eff
 18 |
 19 | import Years.Y2015;
 20 |
 21 | %language ElabReflection
 22 | %default total
 23 |
 24 | data Flag = UseExample | Verbose
 25 | %runElab derive "Flag" [Eq, Show]
 26 |
 27 | advent : Advent
 28 | advent = MkAdvent [
 29 |     y2015
 30 |   ]
 31 |
 32 | options : List (OptDescr Flag)
 33 | options =
 34 |   [
 35 |     MkOpt ['u'] ["use-example"] (NoArg UseExample) "Use example input instead of main input"
 36 |   , MkOpt ['v'] ["verbose"] (NoArg Verbose) "Enable logging to stderr"
 37 |   ]
 38 |
 39 | header : String
 40 | header = "Usage: advent YEAR DAY [OPTION...]"
 41 |
 42 | data Error : Type where
 43 |   OptionsError : (errs : List String) -> Error
 44 |   ArgumentsError : (count : Nat) -> Error
 45 |   InvalidYear : (year : String) -> Error
 46 |   InvalidDay : (year : Nat) -> (day : String) -> Error
 47 |   NoSuchDay : (year : Nat) -> (day : Nat) -> Error
 48 |   NoCurrentDir : Error
 49 |   InputRead : (path : String) -> (err : FileError) -> Error
 50 |   SolveError : Show e => (year, day, part : Nat) -> (err : e) -> Error
 51 | %name Error err
 52 |
 53 | Show Error where
 54 |   show (OptionsError errs) =
 55 |     let errs = unlines . map ("  " ++) . lines . joinBy "\n" $ errs
 56 |     in "Error parsing options:\n" ++ errs ++ "\n" ++ usageInfo header options
 57 |   show (ArgumentsError count) =
 58 |     "Error parsing arguments: Expected 2 positional arguments, got \{show count}. Provide only year and date.\n" ++
 59 |     usageInfo header options
 60 |   show (InvalidYear year) =
 61 |     "Error parsing arguments: Unable to parse year argument: \{year}"
 62 |   show (InvalidDay year day) =
 63 |     "Error parsing arguments: Failed to parse day \{day} of year \{show year}"
 64 |   show (NoSuchDay year day) =
 65 |     "Error locating day: No such day \{show day} of year \{show year}"
 66 |   show NoCurrentDir =
 67 |     "Unknown error getting current working directory"
 68 |   show (InputRead path err) =
 69 |     let err = unlines . map ("  " ++) . lines . show $ err
 70 |     in "Error reading input: Encountered error reading input at \{path}\n" ++ err
 71 |   show (SolveError year day part err) =
 72 |     let err = unlines . map ("  " ++) . lines . show $ err
 73 |     in "Error solving day \{show day} part \{show part} of year \{show year}: \n" ++ err
 74 |
 75 | ||| Convert the non-option arguments into a Year/Day pair
 76 | argumentsToPair : Has (Except Error) fs =>
 77 |   List String -> Eff fs (Nat, Nat)
 78 | argumentsToPair [] = throw $ ArgumentsError 0
 79 | argumentsToPair [x] = throw $ ArgumentsError 1
 80 | argumentsToPair [year, day] = do
 81 |   year <- note (InvalidYear year) $ parsePositive year
 82 |   day <- note (InvalidDay year day) $ parsePositive day
 83 |   pure (year, day)
 84 | argumentsToPair xs = throw $ ArgumentsError (length xs)
 85 |
 86 | covering
 87 | ||| Actual main, as an effectful computation
 88 | start : Eff [IO, Except Error] ()
 89 | start = do
 90 |   -- Read and parse arguments/options
 91 |   args <- getArgs
 92 |   let opts = getOpt Permute options (drop 1 args)
 93 |   when (not . null $ opts.errors) $
 94 |     throw (OptionsError opts.errors)
 95 |   (year, day_n) <- argumentsToPair opts.nonOptions
 96 |   -- If the verbose flag is set, hook up the logging writer to stderr
 97 |   let verbose = any (== Verbose) opts.options
 98 |   let logHandler : Eff [IO, Except Error, WriterL "log" String] () -> Eff [IO, Except Error] () =
 99 |     if verbose
100 |        then handleLog ePutStrLn
101 |        else handleLog (\x => pure ())
102 |   -- Add the logging writer to the effect
103 |   logHandler $ do
104 |   -- Locate and read in the input file
105 |   Just cwd <- currentDir | _ => throw NoCurrentDir
106 |   let cwd = parse cwd
107 |   let use_example = any (== UseExample) opts.options
108 |   let base_dir = cwd /> "inputs" /> (if use_example then "examples" else "real");
109 |   let input_path = show $ base_dir /> (show year) /> (show day_n)
110 |   info "Reading input from \{input_path}"
111 |   Right contents <- readFile input_path | Left err => throw $ InputRead input_path err
112 |   -- Now add the reader that provides the input to the effect
113 |   runReaderAt "input" contents {fs = PartEff Error} $ do
114 |   -- Attempt to locate the provided day
115 |   Just day <- pure $ locate year day_n advent | _ => throw $ NoSuchDay year day_n
116 |   -- Run part 1
117 |   part_1 <- lift $ runExcept day.part1
118 |   (part_1, ctx) <- rethrow . mapLeft (SolveError year day_n 1 @{day.showErr1}) $ part_1
119 |   putStrLn "\{show year} day \{show day_n} part 1:"
120 |   putStrLn $ unlines . map ("  " ++) . lines . show @{day.showOut1} $ part_1
121 |   -- Run part 2 if we have it
122 |   case day.part2 of
123 |     Nothing => pure ()
124 |     Just part_2_f => do
125 |       part_2 <- lift . runExcept $ part_2_f ctx
126 |       part_2 <- rethrow . mapLeft (SolveError year day_n 2 @{day.showErr2}) $ part_2
127 |       putStrLn "\{show year} day \{show day_n} part 2:"
128 |       putStrLn $ unlines . map ("  " ++) . lines . show @{day.showOut2} $ part_2
129 |   where
130 |     -- print to standard error
131 |     ePutStrLn : String -> IO ()
132 |     ePutStrLn str = do
133 |       _ <- fPutStrLn stderr str
134 |       pure ()
135 |     -- Decompose a writer, eases type inference
136 |     unwriter : WriterL "log" String a -> (a, String)
137 |     unwriter (Tell vw) = ((), vw)
138 |     -- Lowers logging into IO within the effect using the given IO function
139 |     handleLog :
140 |       Has (WriterL "log" String) fs => Has IO (fs - WriterL "log" String) => 
141 |       (tell : String -> IO ()) -> Eff fs a -> Eff (fs - (WriterL "log" String)) a
142 |     handleLog tell x =
143 |       handle
144 |         (\msg, f =>
145 |             do let (val, msg) = unwriter msg
146 |                _ <- send $ tell msg
147 |                f val) x
148 |
149 | covering
150 | ||| Shim main, which simply executes the effectful computation
151 | main : IO ()
152 | main = runEff start [id, handleError]
153 |   where
154 |   handleError : Except Error a -> IO a
155 |   handleError (Err err) = do
156 |     printLn err
157 |     exitFailure
158 |