1 files changed, 271 insertions, 0 deletions
diff --git a/Day5.lean b/Day5.lean
new file mode 100644
index 0000000..18f9aeb
--- /dev/null
+++ b/Day5.lean
@@ -0,0 +1,271 @@
+import Common.DayPart
+import Common.List
+
+namespace Day5
+
+structure Seed where
+  id : Nat
+  deriving BEq, Ord, Repr
+
+structure Soil where
+  id : Nat
+  deriving BEq, Ord, Repr
+
+structure Fertilizer where
+  id : Nat
+  deriving BEq, Ord, Repr
+
+structure Water where
+  id : Nat
+  deriving BEq, Ord, Repr
+
+structure Light where
+  id : Nat
+  deriving BEq, Ord, Repr
+
+structure Temperature where
+  id : Nat
+  deriving BEq, Ord, Repr
+
+structure Humidity where
+  id : Nat
+  deriving BEq, Ord, Repr
+
+structure Location where
+  id : Nat
+  deriving BEq, Ord, Repr
+
+private class NatId (α : Type) where
+  fromNat : Nat → α
+  toNat : α → Nat
+
+private instance : NatId Seed where
+  fromNat := Seed.mk
+  toNat := Seed.id
+
+private instance : NatId Soil where
+  fromNat := Soil.mk
+  toNat := Soil.id
+
+private instance : NatId Fertilizer where
+  fromNat := Fertilizer.mk
+  toNat := Fertilizer.id
+
+private instance : NatId Water where
+  fromNat := Water.mk
+  toNat := Water.id
+
+private instance : NatId Light where
+  fromNat := Light.mk
+  toNat := Light.id
+
+private instance : NatId Temperature where
+  fromNat := Temperature.mk
+  toNat := Temperature.id
+
+private instance : NatId Humidity where
+  fromNat := Humidity.mk
+  toNat := Humidity.id
+
+private instance : NatId Location where
+  fromNat := Location.mk
+  toNat := Location.id
+
+private instance : Min Location where
+  min a b := if Ord.compare a b == Ordering.lt then a else b
+
+structure Mapping (α β : Type) where
+  inputStart : α
+  outputStart : β
+  length : Nat
+  deriving Repr
+
+structure Mappings (α β : Type) where
+  mappings : List $ Mapping α β
+  deriving Repr
+
+private def Mapping.apply? {α β : Type} [NatId α] [NatId β] (mapping : Mapping α β) (input : α) : Option β :=
+  let input := NatId.toNat input
+  let fromStart := NatId.toNat mapping.inputStart
+  let toStart := NatId.toNat mapping.outputStart
+  if input ≥ fromStart ∧ input < fromStart + mapping.length then
+    some $ NatId.fromNat $ toStart + input - fromStart
+  else
+    none
+
+private def Mappings.apply {α β : Type} [NatId α] [NatId β] (mappings : Mappings α β) (input : α) : β :=
+  let applied := mappings.mappings.findSome? $ flip Mapping.apply? input
+  applied.getD $ NatId.fromNat $ NatId.toNat input
+
+structure Almanach where
+  seedsToSoil : Mappings Seed Soil
+  soilToFertilizer : Mappings Soil Fertilizer
+  fertilizerToWater : Mappings Fertilizer Water
+  waterToLight : Mappings Water Light
+  lightToTemperature : Mappings Light Temperature
+  temperatureToHumidity : Mappings Temperature Humidity
+  humidityToLocation : Mappings Humidity Location
+  deriving Repr
+
+private def parseSeeds (input : String) : Option (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?
+    List.map NatId.fromNat <$> numbers
+  else
+    none
+
+private def parseMapping {α β : Type} [NatId α] [NatId β] (input : String) : Option $ Mapping α β := do
+  let input := String.trim <$> input.split Char.isWhitespace
+  let nums ← input.mapM String.toNat?
+  match nums with
+  | [a,b,c] => some $ {inputStart := NatId.fromNat b, outputStart := NatId.fromNat a, length := c}
+  | _ => none
+
+private def parseMappings (α β : Type) [NatId α] [NatId β] (input : String) (header : String) : Option $ 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
+    Mappings.mk <$> mappings
+  else
+   none
+
+def parse (input : String) : Option ((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
+    let seeds ← parseSeeds seeds
+    let seedToSoil ← parseMappings Seed Soil seedToSoil "seed-to-soil map:"
+    let soilToFertilizer ← parseMappings Soil Fertilizer soilToFertilizer "soil-to-fertilizer map:"
+    let fertilizerToWater ← parseMappings Fertilizer Water fertilizerToWater "fertilizer-to-water map:"
+    let waterToLight ← parseMappings Water Light waterToLight "water-to-light map:"
+    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, {
+      seedsToSoil := seedToSoil
+      soilToFertilizer := soilToFertilizer
+      fertilizerToWater := fertilizerToWater
+      waterToLight := waterToLight
+      lightToTemperature := lightToTemperature
+      temperatureToHumidity := temperatureToHumidity
+      humidityToLocation := humidityToLocation
+    : Almanach})
+  else
+    none
+
+def part1 (input : ((List Seed) × Almanach)) : Option Nat :=
+  let a := input.snd
+  let seedToLocation  := a.humidityToLocation.apply
+                      ∘ a.temperatureToHumidity.apply
+                      ∘ a.lightToTemperature.apply
+                      ∘ a.waterToLight.apply
+                      ∘ a.fertilizerToWater.apply
+                      ∘ a.soilToFertilizer.apply
+                      ∘ a.seedsToSoil.apply
+  let locations := input.fst.map seedToLocation
+  NatId.toNat <$> locations.minimum?
+
+
+-- Part 2 seems unmanageable by brute force.
+-- So, let's rather combine the mappings in a smart way, and then invert them.
+-- Then we can do binary search if any seed is in the domain of the combined mapping.
+-- if not, the answer is just the smallest seed.
+
+private def Mappings.combine {α β γ : Type} [NatId α] [NatId β] [NatId γ] (a : Mappings α β) (b : Mappings β γ) : Mappings α γ :=
+  -- the combined mapping contains all ranges in b that aren't "shielded" by ranges of a.
+  -- then it contains all ranges of a, but their codomain needs to be checked if it overlaps with
+  --    any ranges in b, and if yes, those ranges need to be split accordingly.
+  let domain := λ {δ ε : Type} [NatId δ] [NatId ε] (e :Mapping δ ε) ↦ (NatId.toNat e.inputStart, NatId.toNat e.inputStart + e.length)
+  let codomain := λ {δ ε : Type} [NatId δ] [NatId ε] (e :Mapping δ ε) ↦ (NatId.toNat e.outputStart, NatId.toNat e.outputStart + e.length)
+  let unshieldedB : List (Mapping α γ) := b.mappings.bind λ bm ↦
+    let bmd := domain bm
+    let bmcd := codomain bm
+    let shielded := a.mappings.filterMap λ am ↦
+      let amd := domain am
+      let s := Nat.max amd.fst bmd.fst
+      let e := Nat.min amd.snd bmd.snd
+      if e > s then some (s,e) else none
+    -- add a range before and after to shielded, then we can take those between
+    -- we anyhow need to sort shielded, sooo
+    let shielded := (bmd.fst, bmd.fst) :: (bmd.snd, bmd.snd) :: shielded
+    let shielded := shielded.quicksortBy (·.fst < ·.fst)
+    let rs := shielded.zip (shielded.drop 1)
+    let rs : List (Nat × Nat):= rs.map λ x ↦ (x.fst.snd, x.snd.fst)
+    let rs := rs.filter λ l ↦ l.snd > l.fst -- skip emtpy, they are just noise
+    rs.map λ (x : Nat × Nat) ↦
+      let is : α := NatId.fromNat x.fst
+      let os : γ := NatId.fromNat $ bmcd.fst + x.fst - bmd.fst
+      let l : Nat := (x.snd - x.fst)
+      { inputStart := is, outputStart := os, length := l}
+  --TODO: Unify the onlyAffectedByA and affectedByBoth computations.
+  let onlyAffectedByA : List (Mapping α γ) := a.mappings.bind λ am ↦
+    let amd := domain am
+    let amcd := codomain am
+    let overlapping := b.mappings.filterMap λ bm ↦
+      let bmd := domain bm
+      let s := Nat.max amcd.fst bmd.fst
+      let e := Nat.min amcd.snd bmd.snd
+      if e > s then some (s,e) else none
+    -- overlapping is in the **codomain** of a. Transform to domain:
+    let overlapping := overlapping.map λ p ↦ (p.fst + amd.fst - amcd.fst, p.snd + amd.fst - amcd.fst)
+    let overlapping := (amd.fst, amd.fst) :: (amd.snd, amd.snd) :: overlapping
+    let overlapping := overlapping.quicksortBy (·.fst < ·.fst)
+    let rs := overlapping.zip (overlapping.drop 1)
+    let rs : List (Nat × Nat):= rs.map λ x ↦ (x.fst.snd, x.snd.fst)
+    let rs := rs.filter λ l ↦ l.snd > l.fst
+    rs.map λ (x : Nat × Nat) ↦
+      let is : α := NatId.fromNat x.fst
+      let os : γ := NatId.fromNat $ amcd.fst + x.fst - amd.fst
+      let l : Nat := (x.snd - x.fst)
+      { inputStart := is, outputStart := os, length := l}
+  let affectedByBoth : List (Mapping α γ) := sorry
+  sorry
+
+
+open DayPart
+instance : Parse ⟨5, by simp⟩ (ι := (List Seed) × Almanach) where
+  parse := parse
+
+instance : Part ⟨5, _⟩ Parts.One (ι := (List Seed) × Almanach) (ρ := Nat) where
+  run := part1
+
+
+private def TestInput := "seeds: 79 14 55 13
+
+seed-to-soil map:
+50 98 2
+52 50 48
+
+soil-to-fertilizer map:
+0 15 37
+37 52 2
+39 0 15
+
+fertilizer-to-water map:
+49 53 8
+0 11 42
+42 0 7
+57 7 4
+
+water-to-light map:
+88 18 7
+18 25 70
+
+light-to-temperature map:
+45 77 23
+81 45 19
+68 64 13
+
+temperature-to-humidity map:
+0 69 1
+1 0 69
+
+humidity-to-location map:
+60 56 37
+56 93 4
+"
+
+#eval parse TestInput
+#eval parse TestInput >>= part1