private structure Mapping2 (α β : Type) where
  start : α --okay, next time I do this, I'll encode end and offset, not start and offset...
  offset : Int
  deriving Repr

private structure Mappings2 (α β : Type) where
  mappings : List $ Mapping2 α β
  deriving Repr

private def Mappings2.fromMappings {α β : Type} [NatId α] [NatId β] [Ord α] (input : Mappings α β) : Mappings2 α β :=
  let input := input.mappings.quicksortBy λ a b ↦ (Ord.compare a.inputStart b.inputStart == Ordering.lt)
  let rec helper := λ
    | [] => []
    | a :: [] => [{ start:= a.inputStart, offset := (NatId.toNat a.outputStart) - (NatId.toNat a.inputStart)},
                 {start:= NatId.fromNat (NatId.toNat a.inputStart + a.length), offset := 0}]
    | a :: b :: as => if (NatId.toNat b.inputStart) != (NatId.toNat a.inputStart + a.length) then
                        { start:= a.inputStart, offset := (NatId.toNat a.outputStart) - (NatId.toNat a.inputStart)}
                        :: { start:= NatId.fromNat (NatId.toNat a.inputStart + a.length), offset := 0}
                        :: helper (b :: as)
                      else
                        { start:= a.inputStart, offset := (NatId.toNat a.outputStart) - (NatId.toNat a.inputStart)}
                        :: helper (b :: as)
  let result := match input with
    | [] => []
    | a :: _ =>  if NatId.toNat a.inputStart != 0 then
                    { start:= NatId.fromNat 0, offset := 0 : Mapping2 α β} :: helper input
                  else
                    helper input
  Mappings2.mk result

private def Mappings2.apply (α β : Type) [NatId α] [NatId β] [Ord α] (mapping : Mappings2 α β) (value : α) : β :=
  let rec findOffsetHelper := λ
    | [] => 0
    | a :: [] => a.offset
    | a :: b :: as => if (Ord.compare value b.start == Ordering.lt) then a.offset else findOffsetHelper (b :: as)
  let offset : Int := findOffsetHelper mapping.mappings
  let result : Int := (NatId.toNat value + offset)
  NatId.fromNat result.toNat

private def Mappings2.combine {α β γ : Type} [NatId α] [NatId β] [NatId γ] (a : Mappings2 α β) (b : Mappings2 β γ) : Mappings2 α γ :=
  -- at this point, let's just go integer
  let a : List (Int × Int) := a.mappings.map λ m ↦ (NatId.toNat m.start, m.offset)
  let b : List (Int × Int):= b.mappings.map λ m ↦ (NatId.toNat m.start, m.offset)
  let rec findOffsetHelper := λ (list : List (Int × Int)) (value : Int) ↦ match list with
    | [] => 0
    | a :: [] => a.snd
    | a :: b :: as => if (value < b.fst) then a.snd else findOffsetHelper (b :: as) value

  let rec helper := λ
    | [] => b
    | a :: [] =>
      let bOffsetAtA := findOffsetHelper b (a.fst + a.snd)
      let bRemainder := b.dropWhile (λ (bb : Int × Int) ↦ a.fst + a.snd > bb.fst)
      match bRemainder with
        | [] => [(a.fst, a.snd + bOffsetAtA)]
        | b :: _ =>  if b.fst - a.snd == a.fst then
                        bRemainder.map λ (b : Int × Int) ↦ (b.fst - a.snd, a.snd + b.snd)
                      else
                        (a.fst, a.snd + bOffsetAtA) :: bRemainder.map λ (b : Int × Int) ↦ (b.fst - a.snd, a.snd + b.snd)
    | a :: aa :: as =>
      let bOffsetAtA := findOffsetHelper b (a.fst + a.snd)
      let relevantBs := b.filter (λ (bb : Int × Int) ↦ a.fst + a.snd ≤ bb.fst && aa.fst + a.snd > bb.fst)
      match relevantBs with
        | [] => (a.fst, a.snd + bOffsetAtA) :: (helper (aa :: as))
        | b :: _ =>  if b.fst - a.snd == a.fst then
                        (relevantBs.map λ (b : Int × Int) ↦ (b.fst - a.snd, a.snd + b.snd))
                        ++ helper (aa :: as)
                      else
                        (a.fst, a.snd + bOffsetAtA) :: (relevantBs.map λ (b : Int × Int) ↦ (b.fst - a.snd, a.snd + b.snd))
                        ++ helper (aa :: as)
  let result := helper a
  Mappings2.mk $ result.map λ p ↦ { start := NatId.fromNat p.fst.toNat, offset := p.snd : Mapping2 α γ}

private structure SeedRange where
  start : Seed
  ending : Seed
  deriving Repr

private def SeedRange.fromList (input : List Seed) : List SeedRange :=
  let rec helper : List Seed → List SeedRange := λ
    | [] => []
    | _ :: [] => []
    | a :: b :: as => { start := a, ending := Seed.mk $ b.id + a.id} :: SeedRange.fromList as
  (helper input).quicksortBy λ a b ↦ a.start.id < b.start.id

private def SeedRange.findSmallestSeedAbove (seedRanges : List SeedRange) (value : Seed) : Option Seed :=
  -- two options: If the value is inside a seedRange, the value itself is the result
  --              If not, the start of the first seedRange above the value is the result
  let rangeContains := λ r ↦ (Ord.compare r.start value != Ordering.gt) && (Ord.compare r.ending value == Ordering.gt)
  let rec helper := λ
  | [] => none
  | r :: rs =>  if rangeContains r then
                  some value
                else
                  if Ord.compare r.start value == Ordering.gt then
                    r.start
                  else
                    helper rs
  helper seedRanges

def part2 (input : ((List Seed) × Almanach)) : Option Nat :=
  let a := input.snd
  let seedToLocation := Mappings2.fromMappings a.seedsToSoil
    |> flip Mappings2.combine (Mappings2.fromMappings a.soilToFertilizer)
    |> flip Mappings2.combine (Mappings2.fromMappings a.fertilizerToWater)
    |> flip Mappings2.combine (Mappings2.fromMappings a.waterToLight)
    |> flip Mappings2.combine (Mappings2.fromMappings a.lightToTemperature)
    |> flip Mappings2.combine (Mappings2.fromMappings a.temperatureToHumidity)
    |> flip Mappings2.combine (Mappings2.fromMappings a.humidityToLocation)

  let seedRanges := SeedRange.fromList input.fst

  let potentialSeeds := seedToLocation.mappings.filterMap λ m ↦
    (SeedRange.findSmallestSeedAbove seedRanges m.start) -- could filter by range end, but who cares?
  let locations := potentialSeeds.map seedToLocation.apply
  NatId.toNat <$> locations.minimum?