From 8d6efb1c1fdddc1fbad167510ce25e56be684130 Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Thu, 7 Dec 2023 20:26:51 +0100 Subject: Allow error messages in parsing (for debugging) And fix an off-by-one in day 5 --- Common/DayPart.lean | 2 +- Day1.lean | 6 +++--- Day2.lean | 2 +- Day3.lean | 4 ++-- Day4.lean | 14 +++++++------- Day5.lean | 31 ++++++++++++++++--------------- Day6.lean | 27 +++++++++++++++++++++++++++ Main.lean | 5 +---- inputs/day6.input | 2 ++ lakefile.lean | 2 ++ 10 files changed, 62 insertions(+), 33 deletions(-) create mode 100644 Day6.lean create mode 100644 inputs/day6.input diff --git a/Common/DayPart.lean b/Common/DayPart.lean index c6a4d44..a701272 100644 --- a/Common/DayPart.lean +++ b/Common/DayPart.lean @@ -6,7 +6,7 @@ inductive Parts | Two class Parse (day : Days) {ι : outParam Type} where - parse : String → Option ι + parse : String → Except String ι class Part (day : Days) (part : Parts) {ι ρ : outParam Type} [Parse day (ι := ι)] [ToString ρ] where run : ι → Option ρ -- can fail, because it deals with user input... diff --git a/Day1.lean b/Day1.lean index f0e9c14..d9f0c69 100644 --- a/Day1.lean +++ b/Day1.lean @@ -2,8 +2,8 @@ import Common namespace Day1 -def parse (input : String) : Option $ List String := - some $ input.split Char.isWhitespace |> List.filter (not ∘ String.isEmpty) +def parse (input : String) : List String := + input.split Char.isWhitespace |> List.filter (not ∘ String.isEmpty) -- Both parts could still be improved by doing two searches, one from the left, one from the right @@ -62,7 +62,7 @@ def part2 (instructions : List String) : Option Nat := open DayPart instance : Parse ⟨1, by simp⟩ (ι := List String) where - parse := parse + parse := pure ∘ parse instance : Part ⟨1, _⟩ Parts.One (ι := List String) (ρ := Nat) where run := part1 diff --git a/Day2.lean b/Day2.lean index 7208a3d..7ed10aa 100644 --- a/Day2.lean +++ b/Day2.lean @@ -78,7 +78,7 @@ def part2 (games : List Game) : Nat := open DayPart instance : Parse ⟨2, by simp⟩ (ι := List Game) where - parse := parse + parse := (λ o ↦ match o with | some a => pure a | none => throw "Failed to parse input") ∘ parse instance : Part ⟨2,_⟩ Parts.One (ι := List Game) (ρ := Nat) where run := some ∘ part1 diff --git a/Day3.lean b/Day3.lean index 76c06be..e15e205 100644 --- a/Day3.lean +++ b/Day3.lean @@ -78,10 +78,10 @@ private def extractPartNumbers (input : List (Coordinate × Char)) : List PartNu acc :: helper as none helper input none -def parse (schematic : String) : Option Schematic := do +def parse (schematic : String) : Except String Schematic := do -- I think this one is easier if we don't split the input in lines. Because: let charsWithCoordinates ← match schematic.toList with - | [] => none + | [] => throw "Could not pare input: Empty" | c :: cs => pure $ cs.scan (λ s c ↦ (uncurry Coordinate.nextByChar s, c)) (Coordinate.default, c) -- Whitespaces are **intentionally** left in. This makes extracting the numbers easier. pure $ { diff --git a/Day4.lean b/Day4.lean index d016dfa..4466053 100644 --- a/Day4.lean +++ b/Day4.lean @@ -20,7 +20,7 @@ abbrev Deck := List Card private def Deck.score : Deck → Nat := List.foldl (· + ·.score) 0 -def parse (input : String) : Option Deck := do +def parse (input : String) : Except String Deck := do let mut cards : Deck := [] for line in input.splitOn "\n" do if line.isEmpty then @@ -30,9 +30,9 @@ def parse (input : String) : Option Deck := do let f := String.trim $ cs[0]'(by simp[p]) let g := String.trim $ cs[1]'(by simp[p]) if not $ f.startsWith "Card " then - failure + throw "All cards need to start with the term \"Card \"" let f := f.drop 5 |> String.trim - let f ← f.toNat? + let f ← if let some f := f.toNat? then pure f else throw "Card numbers need to be numbers." let g := g.splitOn "|" if q : g.length = 2 then let winners := String.trim $ g[0]'(by simp[q]) @@ -41,13 +41,13 @@ def parse (input : String) : Option Deck := do s.split (·.isWhitespace) |> List.filter (not ∘ String.isEmpty) |> List.mapM String.toNat? - let winners ← toNumbers winners - let draws ← toNumbers draws + let winners ← if let some winners := toNumbers winners then pure winners else throw "Failed to parse winning numbers." + let draws ← if let some draws := toNumbers draws then pure draws else throw "Failed to parse draws" cards := {id := f, winningNumbers := winners, haveNumbers := draws : Card} :: cards else - failure + throw "Failed to split input line between winners and draws" else - failure + throw "Failed to split between card number and winners/draws" return cards -- cards is **reversed**, that's intentional. It doesn't affect part 1, but makes part 2 easier. def part2 (input : Deck) : Nat := diff --git a/Day5.lean b/Day5.lean index 1fe40dd..f1c96a5 100644 --- a/Day5.lean +++ b/Day5.lean @@ -107,21 +107,22 @@ structure Almanach where humidityToLocation : Mappings Humidity Location deriving Repr -private def parseSeeds (input : String) : Option (List Seed) := +private def parseSeeds (input : String) : Except String (List Seed) := if input.startsWith "seeds: " then let input := input.drop 7 let input := String.trim <$> input.split Char.isWhitespace let numbers := input.mapM String.toNat? + let numbers := if let some numbers := numbers then pure numbers else throw s!"Failed to parse a seed number in {input}" List.map NatId.fromNat <$> numbers else - none + throw s!"Seeds line does not start with \"seeds: \": {input}" -private def parseMapping {α β : Type} [NatId α] [NatId β] (input : String) : Option $ Mapping α β := do +private def parseMapping {α β : Type} [NatId α] [NatId β] (input : String) : Except String $ Mapping α β := do let input := String.trim <$> input.split Char.isWhitespace - let nums ← input.mapM String.toNat? + let nums ← input.mapM $ (λ o ↦ if let some o := o then pure o else throw s!"Failed to parse mapping {input}, expected number") ∘ String.toNat? match nums with - | [a,b,c] => some $ {inputStart := NatId.fromNat b, outputStart := NatId.fromNat a, length := c} - | _ => none + | [a,b,c] => pure $ {inputStart := NatId.fromNat b, outputStart := NatId.fromNat a, length := c} + | _ => throw "Failed to parse mapping {input}, expected 3 numbers." private def Mapping.overlap {α β : Type} [NatId α] [NatId β] (a : Mapping α β) (b : Mapping α β) : Bool := let aStart := NatId.toNat $ a.inputStart @@ -129,23 +130,23 @@ private def Mapping.overlap {α β : Type} [NatId α] [NatId β] (a : Mapping α let bStart := NatId.toNat $ b.inputStart let bEnd := bStart + b.length (bStart ≥ aStart && bStart < aEnd) - || (bEnd ≥ aStart && bEnd < aEnd) + || (bEnd > aStart && bEnd ≤ aEnd) || (aStart ≥ bStart && aStart < bEnd) - || (aEnd ≥ bStart && aEnd < bEnd) + || (aEnd > bStart && aEnd ≤ bEnd) -private def parseMappings (α β : Type) [NatId α] [NatId β] (input : String) (header : String) : Option $ Mappings α β := +private def parseMappings (α β : Type) [NatId α] [NatId β] (input : String) (header : String) : Except String $ Mappings α β := if input.startsWith header then let lines := String.trim <$> input.splitOn "\n" |> List.drop 1 |> List.filter (not ∘ String.isEmpty) - let mappings := lines.mapM parseMapping + let mappings : Except String (List $ Mapping α β) := lines.mapM parseMapping let rec overlapHelper := λ (a : List $ Mapping α β) ↦ match a with | [] => false | a :: as => as.any (λ b ↦ a.overlap b) || overlapHelper as - let mappings := mappings.filter overlapHelper --make sure no ranges overlap. That would be faulty + let mappings := mappings.bind λ m ↦ if overlapHelper m then throw s!"There is an overlap in mapping {input}" else pure m Mappings.mk <$> mappings else - none + throw s!"Input line does not start with the required header: {header} {input}" -def parse (input : String) : Option ((List Seed) × Almanach) := do +def parse (input : String) : Except String ((List Seed) × Almanach) := do let blocks := input.splitOn "\n\n" |> List.filter (not ∘ String.isEmpty) let blocks := String.trim <$> blocks if let [seeds, seedToSoil, soilToFertilizer, fertilizerToWater, waterToLight, lightToTemperature, temperatureToHumidity, humidityToLocation] := blocks then @@ -157,7 +158,7 @@ def parse (input : String) : Option ((List Seed) × Almanach) := do let lightToTemperature ← parseMappings Light Temperature lightToTemperature "light-to-temperature map:" let temperatureToHumidity ← parseMappings Temperature Humidity temperatureToHumidity "temperature-to-humidity map:" let humidityToLocation ← parseMappings Humidity Location humidityToLocation "humidity-to-location map:" - (seeds, { + pure (seeds, { seedsToSoil := seedToSoil soilToFertilizer := soilToFertilizer fertilizerToWater := fertilizerToWater @@ -167,7 +168,7 @@ def parse (input : String) : Option ((List Seed) × Almanach) := do humidityToLocation := humidityToLocation : Almanach}) else - none + throw "Failed to parse input, it doe not have the required number of blocks" def part1 (input : ((List Seed) × Almanach)) : Option Nat := let a := input.snd diff --git a/Day6.lean b/Day6.lean new file mode 100644 index 0000000..54464ea --- /dev/null +++ b/Day6.lean @@ -0,0 +1,27 @@ +import Common.Option +import Common.Helpers + +structure Race where + timeLimit : Nat + recordDistance : Nat + +private def parseLine (header : String) (input : String) : Option (List Nat) := do + if not $ input.startsWith header then + failure + let input := input.drop header.length |> String.trim + let numbers := input.split Char.isWhitespace + |> List.map String.trim + |> List.filter String.isEmpty + numbers.mapM String.toNat? + +def parse (input : String) : Option (List Race) := do + let lines := input.splitOn "\n" + |> List.map String.trim + |> List.filter String.isEmpty + let (times, distances) ← match lines with + | [times, distances] => Option.zip (parseLine "Time:" times) (parseLine "Distance:" distances) + | _ => none + if times.length != distances.length then + failure + let pairs := times.zip distances + return pairs.map $ uncurry Race.mk diff --git a/Main.lean b/Main.lean index b6d152e..1ad3933 100644 --- a/Main.lean +++ b/Main.lean @@ -9,10 +9,7 @@ open DayPart def try_run_day_part (day : Days) (part : Parts) (data : String) : IO String := let impl : {ι : Type} → (d : Days) → (p : Parts) → String → [Parse d (ι := ι)] → [Part d p (ι := ι)] → IO String := λ day part data ↦ do - let instructions ← if let some instructions := Parse.parse day data then - pure instructions - else - throw $ IO.userError "Failed to parse input file." + let instructions ← IO.ofExcept $ Parse.parse day data if let some result := (Part.run day part instructions).map ToString.toString then pure result else diff --git a/inputs/day6.input b/inputs/day6.input new file mode 100644 index 0000000..27b64c4 --- /dev/null +++ b/inputs/day6.input @@ -0,0 +1,2 @@ +Time: 58 81 96 76 +Distance: 434 1041 2219 1218 diff --git a/lakefile.lean b/lakefile.lean index a9f27b9..3ddbc23 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -15,6 +15,8 @@ lean_lib «Day4» where lean_lib «Day5» where +lean_lib «Day6» where + lean_lib «Common» where @[default_target] -- cgit v1.2.3