feat: part 1-1

src/AllDays.idr

@@ -0,0 +1,3 @@
+module AllDays
+
+import public Day1.Part1

src/Data/Problem.idr

@@ -0,0 +1,88 @@
+module Data.Problem
+
+import Data.List1
+import Data.String
+import Data.Maybe
+import Data.SortedMap
+import Language.Reflection
+
+%language ElabReflection
+%default total
+
+
+public export
+data Part = Part1 | Part2
+
+public export
+Eq Part where
+  Part1 == Part1 = True
+  Part1 == Part2 = False
+  Part2 == Part2 = True
+  Part2 == Part1 = False
+
+public export
+Ord Part where
+  compare Part1 Part1 = EQ
+  compare Part1 Part2 = LT
+  compare Part2 Part2 = EQ
+  compare Part2 Part1 = GT
+
+public export
+record Problem where
+  constructor Pr
+  day : Nat
+  part : Part
+
+public export
+Eq Problem where
+  Pr d1 p1 == Pr d2 p2 = d1 == d2 && p1 == p2
+
+public export
+Ord Problem where
+  compare (Pr d1 p1) (Pr d2 p2) = compare d1 d2 <+> compare p1 p2
+
+
+public export
+partNat : Part -> Nat
+partNat Part1 = 1
+partNat Part2 = 2
+
+public export
+parsePart : String -> Maybe Part
+parsePart "1" = Just Part1
+parsePart "2" = Just Part2
+parsePart _ = Nothing
+
+public export
+parseProblem : String -> Maybe Problem
+parseProblem str =
+  let (day ::: [part]) = split (=='-') str
+        | _ => Nothing
+      dayInt = parseInteger day
+      dayNat = cast <$> filter (> 0) dayInt
+  in Pr <$> dayNat <*> parsePart part
+
+
+||| Generate a list of all problems given the latest problem solved.
+public export
+allProblems : (latest : Problem) -> List Problem
+allProblems (Pr day' part') = do
+  day <- [1..day']
+  part <- filter (<= part') [Part1, Part2]
+  pure $ Pr day part
+
+--- REFLECTION
+
+public export
+fetchSolution : Problem -> Elab (String -> String)
+fetchSolution (Pr day part) = do
+  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 =
+  fromList <$> traverse (\p => (p,) <$> fetchSolution p) (allProblems pr)

src/Day1/Part1.idr

@@ -0,0 +1,39 @@
+module Day1.Part1
+
+import Data.List
+import Data.List1
+import Data.String
+import Data.Maybe
+import Utils
+
+%default total
+
+
+--- PARSING
+
+parseLine : String -> Maybe (Nat, Nat)
+parseLine str =
+  let [n1,n2] = filter (/="") $ forget $ split (==' ') str
+      | _ => Nothing
+  in (,) <$> parseNat n1 <*> parseNat n2
+
+parseInput : String -> Maybe (List Nat, List Nat)
+parseInput = map unzip . traverse (parseLine) . lines
+
+
+--- UTILS
+
+distance : Nat -> Nat -> Nat
+distance x y =
+  cast $ abs $ natToInteger x - natToInteger y
+
+
+--- SOLUTION
+
+export
+solution : String -> Maybe Nat
+solution input = do
+  (list1, list2) <- parseInput input
+  let list1 = sort list1
+      list2 = sort list2
+  pure $ sum $ zipWith distance list1 list2

src/Main.idr

@@ -0,0 +1,46 @@
+module Main
+
+import Data.List1
+import Data.Maybe
+import Data.String
+import Data.SortedMap
+import Data.SortedMap.Dependent
+import Data.Problem
+
+import Language.Reflection
+
+import AllDays
+
+%language ElabReflection
+
+
+||| The latest problem that has been solved.
+-- NOTE: UPDATE AFTER EACH SOLUTION
+latest : Problem
+latest = Pr 1 Part1
+
+
+solMap : SortedMap Problem (String -> String)
+solMap = %runElab fetchAllSols latest
+
+getInput : IO String
+getInput = go ""
+  where
+    go : String -> IO String
+    go str = do
+      line <- getLine
+      if trim line == "\\"
+        then pure str
+        else go (str ++ "\n" ++ line)
+
+main : IO ()
+main = do
+  putStr "Solution: "
+  Just pr <- parseProblem <$> getLine
+    | Nothing => putStrLn "Invalid solution ID"
+  let Just func = lookup pr solMap
+    | Nothing => putStrLn "This part is not implemented yet!"
+
+  putStrLn "Input (end with \\):"
+  input <- trim <$> getInput
+  putStrLn $ func input

src/Utils.idr

@@ -0,0 +1,10 @@
+module Utils
+
+import Data.Maybe
+import Data.String
+
+%default total
+
+export
+parseNat : String -> Maybe Nat
+parseNat = map cast . filter (> 0) . parseInteger