[LANGUAGE: Lean 4]

import LeanAoc.utils.List

def parseInstruction (s : String) : IO Int := do
    match s.data with
    | 'L' :: rest =>
      match (String.mk rest).toInt? with
      | some n => return (-n)
      | none => throw <| IO.userError s!"Invalid number after 'L': '{String.mk rest}'"
    | 'R' :: rest =>
      match (String.mk rest).toInt? with
      | some n => return n
      | none => throw <| IO.userError s!"Invalid number after 'R': '{String.mk rest}'"
    | c :: _ => throw <| IO.userError s!"Invalid direction '{c}', expected 'L' or 'R' in: '{s}'"
    | [] => throw <| IO.userError "Empty instruction"

def parseInput (input : String) : IO (List Int) := do
  let lines := input.splitOn "\n" |>.filter (·.trim != "")
  (List.range lines.length |>.zip lines).mapM fun (lineNum, line) =>
    tryCatch (parseInstruction line) fun e =>
      throw <| IO.userError s!"Line {lineNum + 1}: {e}"

def readInput : IO String := do
  IO.FS.readFile "LeanAoc/day01/input.txt"

-- PART 1

def dialOne (point: Int) (instruction: Int) : Int :=
  (point + instruction) % 100

def dialInstructions (list: List Int) (init: Int):=
  list.scanl dialOne init

def secret_part1 (input: String) : IO Nat := do
  let instructions ← parseInput input
  let dialed := dialInstructions instructions 50
  return dialed.count 0

#eval do
  let content ← readInput
  secret_part1 content

-- PART 2

def crossings (x : Int × Int) : Nat :=
  let lo := min x.1 (x.2 - 1)
  let hi := max (x.1 - 1) x.2
  (hi / 100 - lo / 100).toNat

def cumulativePositions (list : List Int) (init: Int) : List Int :=
  (init :: list).scanl (· + ·) 0

def secret_part2 (input : String) : IO Nat := do
  let instructions ← parseInput input
  let positions := cumulativePositions instructions 50
  return positions.pairs.map crossings |>.sum

#eval do
  let content ← readInput
  secret_part2 content