tidy day3

Aoc2024/Day03/Examples.lean

@@ -1,2 +1,5 @@
-def exampleInput :=
+def exampleInputPart1 :=
 "xmul(2,4)%&mul[3,7]!@^do_not_mul(5,5)+mul(32,64]then(mul(11,8)mul(8,5))"
+
+def exampleInputPart2 :=
+"xmul(2,4)&mul[3,7]!^don't()_mul(5,5)+mul(32,64](mul(11,8)undo()?mul(8,5))"

Aoc2024/Day03/Main.lean

@@ -1,15 +1,16 @@
 import Aoc2024.Day03.Solve
 import Aoc2024.CustomMonadLift
 
-def solve (name: String) (inputPath: String) : IO Unit := do
-  IO.println name
-  let input <- IO.FS.readFile inputPath
-  IO.println s!"Part 1: {solvePart1 input}"
-  IO.println s!"Part 2: {solvePart2 input}"
-
 def main : IO Unit := do
   IO.println "Day 03"
   IO.println ""
-  solve "Example" "Aoc2024/Day03/inputs/example.txt"
+  IO.println "Part 1"
+  let example1 <- IO.FS.readFile "Aoc2024/Day03/inputs/example1.txt"
+  let example2 <- IO.FS.readFile "Aoc2024/Day03/inputs/example2.txt"
+  let input <- IO.FS.readFile "Aoc2024/Day03/inputs/input.txt"
+  IO.println s!"Example: {solvePart1 example1}"
+  IO.println s!"Input: {solvePart1 input}" -- 174960351
   IO.println ""
-  solve "Puzzle" "Aoc2024/Day03/inputs/input.txt"
+  IO.println "Part 2"
+  IO.println s!"Example: {solvePart2 example2}"
+  IO.println s!"Input: {solvePart2 input}" -- 56275602

Aoc2024/Day03/Parser.lean

@@ -1,10 +1,24 @@
 import Aoc2024.Day03.Examples
+import Aoc2024.Day03.Types
 import Std
-open Std.Internal.Parsec.String
-open Std.Internal.Parsec
+import Regex
+open Regex (Match Captures)
 
-private def inputParser : Parser (List Int) := sorry
+def instructionRegex: Regex := regex% r"mul\((\d+),(\d+)\)|do\(\)|don't\(\)"
 
-def parseThings : String -> Except String (List Int) := inputParser.run
+private def matchToMultiplyInstruction (captures: Captures): Option Instruction :=
+  match captures.groups.toList with
+  | [some m1, some m2] => Instruction.mul <$> m1.toNat? <*> m2.toNat?
+  | _ => none
 
--- #guard parseReports exampleInput == Except.ok 42
+def matchToInstruction (captures: Captures) : Option Instruction :=
+  if captures.fullMatch == "do()" then some Instruction.do
+  else if captures.fullMatch == "don't()" then some Instruction.dont
+  else matchToMultiplyInstruction captures
+
+def findInstructions (s : String) : List Instruction :=
+  Regex.all_captures s instructionRegex |>.toList |>.bind (· |> matchToInstruction |> Option.toList)
+
+#guard findInstructions "mul(1,2) mul(3,4)" == [Instruction.mul 1 2, Instruction.mul 3 4]
+#guard findInstructions "do()" == [Instruction.do]
+#guard findInstructions "don't()" == [Instruction.dont]

Aoc2024/Day03/Solve.lean

@@ -1,63 +1,27 @@
 import Aoc2024.Utils
 import Aoc2024.Day03.Examples
 import Aoc2024.Day03.Parser
-import Regex
-open Regex (Match Captures)
+import Aoc2024.Day03.Types
 
-inductive Instruction where
-  | mul (n m : Nat) : Instruction
-  | do : Instruction
-  | dont: Instruction
-deriving instance BEq, Hashable, Repr for Instruction
-
-def instructionRegex: Regex := regex% r"mul\((\d+),(\d+)\)|do\(\)|don't\(\)"
-
-def matchToNat (m : Match) : Option Nat := m.toNat?
-
-def optMatchToNat (m : Option Match) : Option Nat := m >>= matchToNat
-
-def matchesToInstruction (ms : Array (Option Match)): Option Instruction :=
-  match ms.toList with
-  | [some m1, some m2] => Instruction.mul <$> matchToNat m1 <*> matchToNat m2
-  | _ => none
-
-def capturesToInstruction (captures: Captures) : Option Instruction :=
-  if captures.fullMatch == "do()" then some Instruction.do
-  else if captures.fullMatch == "don't()" then some Instruction.dont
-  else matchesToInstruction captures.groups
-
-def findInstructions (s : String) : List Instruction :=
-  Regex.all_captures s instructionRegex |>.toList |>.bind (fun captures => captures |> capturesToInstruction |> Option.toList)
-
-#guard findInstructions "mul(1,2) mul(3,4)" == [Instruction.mul 1 2, Instruction.mul 3 4]
-#guard findInstructions "do()" == [Instruction.do]
-#guard findInstructions "don't()" == [Instruction.dont]
-
-def solvePart1 (s : String) : Int := findInstructions s |>.sumBy (fun
+def Instruction.value : Instruction -> Int
   | Instruction.mul n m => n * m
-  | _ => 1
-)
+  | Instruction.do => 1
+  | Instruction.dont => 1
 
-#guard solvePart1 exampleInput = 161
+def solvePart1 (s : String) : Int := findInstructions s |>.sumBy (·.value)
 
-private def filterInstructions (enabled : Bool) : List Instruction -> List Instruction
-  | List.nil => []
-  | List.cons (Instruction.mul m n) rest =>
-    if enabled then List.cons (Instruction.mul m n) (filterInstructions enabled rest)
-   else filterInstructions enabled rest
-  | List.cons Instruction.do rest => filterInstructions true rest
-  | List.cons Instruction.dont rest => filterInstructions false rest
-
-#eval findInstructions "xmul(2,4)&mul[3,7]!^don't()_mul(5,5)+mul(32,64](mul(11,8)undo()?mul(8,5))" |> filterInstructions true
-
-def solvePart2 (s : String) : Int := s |> findInstructions |> filterInstructions true |> List.sumBy (fun
-  | Instruction.mul n m => n * m
-  | _ => 1
-)
+#guard solvePart1 exampleInputPart1 == 161
 
-#eval solvePart2 "xmul(2,4)&mul[3,7]!^don't()_mul(5,5)+mul(32,64](mul(11,8)undo()?mul(8,5))"
-
-#guard solvePart2 "xmul(2,4)&mul[3,7]!^don't()_mul(5,5)+mul(32,64](mul(11,8)undo()?mul(8,5))" == 48
-
-
--- #guard parseAndSolvePart2 exampleInput == Except.ok 4
+private def filterInstructions (enabled : Bool) : List Instruction -> List Instruction
+  | [] => []
+  | List.cons instruction rest =>
+    match instruction with
+      | Instruction.mul m n =>
+        if enabled then List.cons (Instruction.mul m n) (filterInstructions enabled rest)
+        else filterInstructions enabled rest
+      | Instruction.do => filterInstructions true rest
+      | Instruction.dont => filterInstructions false rest
+
+def solvePart2 (s : String) : Int := findInstructions s |> filterInstructions true |> List.sumBy (·.value)
+
+#guard solvePart2 exampleInputPart2 == 48

Aoc2024/Day03/Types.lean

@@ -0,0 +1,5 @@
+inductive Instruction where
+  | mul (n m : Nat) : Instruction
+  | do : Instruction
+  | dont: Instruction
+deriving instance BEq, Hashable, Repr for Instruction

Aoc2024/Day03/inputs/example2.txt

@@ -0,0 +1 @@
+xmul(2,4)&mul[3,7]!^don't()_mul(5,5)+mul(32,64](mul(11,8)undo()?mul(8,5))