Allow error messages in parsing (for debugging)

And fix an off-by-one in day 5

10 files changed, 62 insertions, 33 deletions

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]