diff --git a/Aoc2024/Day01/Parser.lean b/Aoc2024/Day01/Parser.lean index af16704..3076fae 100644 --- a/Aoc2024/Day01/Parser.lean +++ b/Aoc2024/Day01/Parser.lean @@ -3,29 +3,12 @@ import Std open Std.Internal.Parsec.String open Std.Internal.Parsec -def splitOnWhitespace (s : String) : List String := - s.split Char.isWhitespace |> .filter (· ≠ "") - -def parseNumber (s: String) : Except String Int := - s.toInt? |> getOrThrow s!"Failed to parse as number: {s}" - -def getTwoElements (l : List α) : Except String (α × α) := do - let [a, b] := l | throw s!"Expected two elements, but got {l.length}" - pure (a, b) - -def parseTwoNumbers (line : String) : Except String (Int × Int) := do - let (a, b) ← getTwoElements (splitOnWhitespace line) - Prod.mk <$> parseNumber a <*> parseNumber b - -def parseLines (s : String) : Except String (List (Int × Int)) := - s.splitOn "\n" |>.mapM parseTwoNumbers - -def lineParser : Parser (Int × Int) := do +private def lineParser : Parser (Int × Int) := do let a ← String.digits let _ <- String.ws let b ← String.digits pure (a, b) --- def inputParser : Parser (List (Int × Int)) := do --- let lines ← lineParser.many1 --- pure lines +private def inputParser : Parser (List (Int × Int)) := sepBy lineParser (String.skipChar '\n') + +def parseLines : String -> Except String (List (Int × Int)) := inputParser.run diff --git a/Aoc2024/Day01/Solve.lean b/Aoc2024/Day01/Solve.lean index f25a711..a82920b 100644 --- a/Aoc2024/Day01/Solve.lean +++ b/Aoc2024/Day01/Solve.lean @@ -2,7 +2,7 @@ import Aoc2024.Day01.Parser import Aoc2024.Utils namespace Aoc2024.Day01 -def exampleInput := +private def exampleInput := "3 4 4 3 2 5 @@ -10,7 +10,7 @@ def exampleInput := 3 9 3 3" -def solvePart1 (pairs : List (Int × Int)) : Int := +private def solvePart1 (pairs : List (Int × Int)) : Int := let (firsts, seconds) := pairs.unzip let distance (a b : Int) : Int := (a - b).natAbs (firsts.mergeSort.zipWith distance seconds.mergeSort) |> sumList @@ -19,7 +19,7 @@ def parseAndSolvePart1 : String -> Except String Int := .map solvePart1 ∘ pars #guard (parseAndSolvePart1 exampleInput == Except.ok 11) -def solvePart2 (pairs : List (Int × Int)) : Int := +private def solvePart2 (pairs : List (Int × Int)) : Int := let (firsts, seconds) := pairs.unzip let similarityScore (n : Int) : Int := seconds.count n * n firsts |> sumListBy similarityScore diff --git a/Aoc2024/Utils.lean b/Aoc2024/Utils.lean index 215d194..0f39d1b 100644 --- a/Aoc2024/Utils.lean +++ b/Aoc2024/Utils.lean @@ -1,3 +1,7 @@ +import Std +open Std.Internal.Parsec.String +open Std.Internal.Parsec + def sumList (nums : List Int) : Int := nums.foldl (· + ·) 0 #guard sumList [] = 0 @@ -38,3 +42,14 @@ def getOrThrow (message : String) : Option α -> Except String α #guard (getOrThrow "Error" (some 42) == Except.ok 42) #guard (getOrThrow "Error" (none : Option Int) == Except.error "Error") + +def sepBy (p : Parser α) (sep : Parser β) : Parser (List α) := + (do + let x ← p + let xs ← many (sep *> p) + pure (x :: xs.toList) + ) <|> pure [] + +#guard (sepBy digits (skipChar ',')).run "1,2,3" == .ok [1, 2, 3] +#guard (sepBy digits (skipChar ',')).run "4" == .ok [4] +#guard (sepBy digits (skipChar ',')).run "" == .ok []