feat: part 3-2

advent-of-code-2024.ipkg

@@ -9,10 +9,12 @@ 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,3 +4,5 @@ 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,16 +73,31 @@ allProblems (Pr day' part') = do
 
 --- REFLECTION
 
-public export
-fetchSolution : Problem -> Elab (String -> String)
-fetchSolution (Pr day part) = do
-  let name =
+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
+  let name = solutionName pr
   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 =
-  fromList <$> traverse (\p => (p,) <$> fetchSolution p) (allProblems pr)
+  let prs = 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

@@ -0,0 +1,26 @@
+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

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

src/Utils.idr

@@ -2,9 +2,29 @@ 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