advent-of-code-2024.ipkg

@@ -9,12 +9,10 @@ license = "MIT"
 sourcedir = "src"
 
 langversion >= 0.6.0
-depends = contrib
 
 executable = advent-of-code-2024
 main = Main
 modules = Main, Utils, AllDays,
           Data.Problem,
           Day1.Part1, Day1.Part2,
-          Day2.Part1, Day2.Part2,
+          Day2.Part1, Day2.Part2
-          Day3.Part1, Day3.Part2

src/AllDays.idr

@@ -4,5 +4,3 @@ import public Day1.Part1
 import public Day1.Part2
 import public Day2.Part1
 import public Day2.Part2
-import public Day3.Part1
-import public Day3.Part2

src/Data/Problem.idr

@@ -73,31 +73,16 @@ allProblems (Pr day' part') = do
 
 --- REFLECTION
 
-solutionName : Problem -> Name
-solutionName (Pr day part) =
-    NS (MkNS ["Part" ++ show (partNat part),
-              "Day" ++ show day]) `{solution}
-
 public export
 fetchSolution : Problem -> Elab (String -> String)
-fetchSolution pr = do
+fetchSolution (Pr day part) = do
-  let name = solutionName pr
+  let name =
+    NS (MkNS ["Part" ++ show (partNat part),
+              "Day" ++ show day]) `{solution}
   check `(\s => show (~(IVar EmptyFC name) s))
     <|> fail "\{show name} does not exist as a valid solution"
 
 public export
 fetchAllSols : (latest : Problem) -> Elab (SortedMap Problem (String -> String))
 fetchAllSols pr =
-  let prs = allProblems pr
+  fromList <$> traverse (\p => (p,) <$> fetchSolution p) (allProblems pr)
-      list = foldr (\pr,tt => `(Prelude.(::)
-                                (Builtin.MkPair
-                                 (Data.Problem.Pr
-                                  (Prelude.fromInteger
-                                   ~(IPrimVal EmptyFC $ BI $ natToInteger pr.day))
-                                  ~(case pr.part of
-                                      Part1 => `(Data.Problem.Part1)
-                                      Part2 => `(Data.Problem.Part2)))
-                                 (\s => show (~(IVar EmptyFC $ solutionName pr) s)))
-                                ~(tt))) `(Prelude.Nil) prs
-      ttimp = `(Data.SortedMap.fromList ~(list))
-  in check ttimp

src/Day3/Part1.idr

@@ -1,26 +0,0 @@
-module Day3.Part1
-
-import Data.Either
-import Data.Maybe
-import Data.String
-import Data.String.Parser
-import Utils
-
---- PARSING
-
-export
-mul : Parser Integer
-mul = do
-  skip $ string "mul("
-  x <- integer
-  skip $ string ","
-  y <- integer
-  skip $ string ")"
-  pure $ x * y
-
---- SOLUTION
-
-export
-solution : String -> Integer
-solution = fromMaybe 0 . map (sum . fst) . eitherToMaybe .
-            parse (many $ scan mul)

src/Day3/Part2.idr

@@ -1,26 +0,0 @@
-module Day3.Part2
-
-import Data.Either
-import Data.Maybe
-import Data.String
-import Data.String.Parser
-import Utils
-
-import Day3.Part1
-
---- PARSING
-
-export
-mulsDo : Parser (List Integer)
-mulsDo = map join $ many $ do
-  s <- scan $ string "do()" <|> string "don't()"
-  if s == "do()"
-    then many $ scanWhile (requireFailure (string "do()" <|> string "don't()")) mul
-    else pure []
-
---- SOLUTION
-
-export
-solution : String -> Integer
-solution = fromMaybe 0 . map (sum . fst) . eitherToMaybe .
-            parse mulsDo . ("do()" ++)

src/Main.idr

@@ -1,6 +1,10 @@
 module Main
 
+import Data.List1
+import Data.Maybe
+import Data.String
 import Data.SortedMap
+import Data.SortedMap.Dependent
 import Data.Problem
 import Utils
 
@@ -14,7 +18,7 @@ import AllDays
 ||| The latest problem that has been solved.
 -- NOTE: UPDATE AFTER EACH SOLUTION
 latest : Problem
-latest = Pr 3 Part2
+latest = Pr 2 Part2
 
 
 solMap : SortedMap Problem (String -> String)

src/Utils.idr

@@ -2,29 +2,9 @@ module Utils
 
 import Data.Maybe
 import Data.String
-import Data.String.Parser
 
 %default total
 
 export
 parseNat : String -> Maybe Nat
 parseNat = map cast . filter (> 0) . parseInteger
-
-
-export
-lookahead : Functor m => ParseT m a -> ParseT m a
-lookahead p = P $ \s => map (\case
-                                OK r _ => OK r s
-                                Fail i err => Fail i err)
-                            (p.runParser s)
-export covering
-until : Monad m => ParseT m a -> ParseT m ()
-until p = skip $ many (requireFailure p *> skip (satisfy (const True)))
-
-export covering
-scan : Monad m => ParseT m a -> ParseT m a
-scan p = until p *> p
-
-export covering
-scanWhile : Monad m => ParseT m a -> ParseT m b -> ParseT m b
-scanWhile w p = many (lookahead w *> requireFailure p *> skip (satisfy (const True))) *> p