day3 part 1

Aoc2024/Day03/Examples.lean

@@ -1,2 +1,2 @@
 def exampleInput :=
-"..."
+"xmul(2,4)%&mul[3,7]!@^do_not_mul(5,5)+mul(32,64]then(mul(11,8)mul(8,5))"

Aoc2024/Day03/Main.lean

@@ -4,8 +4,8 @@ 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: {<- parseAndSolvePart1 input}"
-  IO.println s!"Part 2: {<- parseAndSolvePart2 input}"
+  IO.println s!"Part 1: {solvePart1 input}"
+  -- IO.println s!"Part 2: {<- parseAndSolvePart2 input}"
 
 def main : IO Unit := do
   IO.println "Day 03"

Aoc2024/Day03/Solve.lean

@@ -1,12 +1,31 @@
 import Aoc2024.Utils
 import Aoc2024.Day03.Examples
 import Aoc2024.Day03.Parser
+import Regex
+open Regex (Match Captures)
 
-private def solvePart1 (things : List Int) : Int := sorry
+def mulRegex := regex% r"mul\((\d+),(\d+)\)"
 
-def parseAndSolvePart1 (s : String): Except String Int := parseThings s |>.map solvePart1
+def matchToNat (m : Match) : Option Nat := m.toNat?
 
--- #guard parseAndSolvePart1 exampleInput == Except.ok 2
+def optMatchToNat (m : Option Match) : Option Nat := m >>= matchToNat
+
+def matchesToNatPair (ms : Array (Option Match)): Option (Nat × Nat) :=
+  match ms.toList with
+  | [some m1, some m2] => Prod.mk <$> matchToNat m1 <*> matchToNat m2
+  | _ => none
+
+def capturesToNatPair (captures: Captures) : Option (Nat × Nat) :=
+  matchesToNatPair captures.groups
+
+def findMatches (s : String) : List (Nat × Nat) :=
+  Regex.all_captures s mulRegex |>.toList |>.bind (fun captures => captures |> capturesToNatPair |> Option.toList)
+
+#guard findMatches "mul(1,2) mul(3,4)" = [(1, 2), (3, 4)]
+
+def solvePart1 (s : String) : Int := findMatches s |>.sumBy (fun (n1, n2) => n1 * n2)
+
+#guard solvePart1 exampleInput = 161
 
 private def solvePart2 (things : List Int) : Int := sorry
 

Aoc2024/Day03/inputs/example.txt

@@ -0,0 +1 @@
+xmul(2,4)%&mul[3,7]!@^do_not_mul(5,5)+mul(32,64]then(mul(11,8)mul(8,5))

Aoc2024/Utils.lean

@@ -47,6 +47,8 @@ def sepBy (p : Parser α) (sep : Parser β) : Parser (List α) :=
 
 namespace List
 
+  def sum (xs: List Int) : Int := xs.foldl .add 0
+
   def sumBy (f : α → Int) (xs : List α) : Int := xs.foldl (λ acc x => acc + f x) 0
 
   def toSet {α:Type} [BEq α] [Hashable α] (xs: List α) : HashSet α :=
@@ -57,6 +59,9 @@ namespace List
 
 end List
 
+#guard [].sum = 0
+#guard [1, 2, 3].sum = 6
+
 #guard [1, 2, 3].sumBy (λ x => x * x) = 14
 
 #guard [].differences == []

lake-manifest.json

@@ -1,15 +1,35 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/batteries",
+ [{"url": "https://github.com/fgdorais/lean4-unicode-basic.git",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "7805acf1864ba1a2e359f86a8f092ccf1438ad83",
+   "scope": "",
+   "rev": "b41bc9cec7f433d6e1d74ff3b59edaaf58ad2915",
+   "name": "UnicodeBasic",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v1.1.0",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "31a10a332858d6981dbcf55d54ee51680dd75f18",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.13.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/bergmannjg/regex",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "b42eb7a7b1338cb18873fc1e5a985600026c2f56",
+   "name": "Regex",
+   "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": false,
-   "configFile": "lakefile.toml"}],
+   "configFile": "lakefile.lean"}],
  "name": "aoc2024",
  "lakeDir": ".lake"}

lakefile.toml

@@ -22,6 +22,6 @@ name = "dayXX"
 root = "Aoc2024.DayXX.Main"
 
 [[require]]
-name = "batteries"
-scope = "leanprover-community"
+name = "Regex"
+git = "https://github.com/bergmannjg/regex"
 rev = "main"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.15.0-rc1
+leanprover/lean4:v4.13.0