[Language: Lean4]
I'll only post the actual parsing and solution. I have written some helpers which are in other files, as is the main function. For the full code, please see my github repo.
Part 2 is a bit ugly, but I'm still new to Lean4, and writing it this way (structural recursion) just worked without a proof or termination.
Solution
def parse (input : String) : Option $ List String :=
some $ input.split Char.isWhitespace |> List.filter (not β String.isEmpty)
def part1 (instructions : List String) : Option Nat :=
let firstLast := Ξ» (o : Option Nat Γ Option Nat) (c : Char) β¦
let digit := match c with
| '0' => some 0
| '1' => some 1
| '2' => some 2
| '3' => some 3
| '4' => some 4
| '5' => some 5
| '6' => some 6
| '7' => some 7
| '8' => some 8
| '9' => some 9
| _ => none
if let some digit := digit then
match o.fst with
| none => (some digit, some digit)
| some _ => (o.fst, some digit)
else
o
let scanLine := Ξ» (l : String) β¦ l.foldl firstLast (none, none)
let numbers := instructions.mapM ((uncurry Option.zip) β scanLine)
let numbers := numbers.map Ξ» l β¦ l.map Ξ» (a, b) β¦ 10*a + b
numbers.map (List.foldl (.+.) 0)
def part2 (instructions : List String) : Option Nat :=
-- once I know how to prove stuff propery, I'm going to improve this. Maybe.
let instructions := instructions.map String.toList
let updateState := Ξ» (o : Option Nat Γ Option Nat) (n : Nat) β¦ match o.fst with
| none => (some n, some n)
| some _ => (o.fst, some n)
let extract_digit := Ξ» (o : Option Nat Γ Option Nat) (l : List Char) β¦
match l with
| '0' :: _ | 'z' :: 'e' :: 'r' :: 'o' :: _ => (updateState o 0)
| '1' :: _ | 'o' :: 'n' :: 'e' :: _ => (updateState o 1)
| '2' :: _ | 't' :: 'w' :: 'o' :: _ => (updateState o 2)
| '3' :: _ | 't' :: 'h' :: 'r' :: 'e' :: 'e' :: _ => (updateState o 3)
| '4' :: _ | 'f' :: 'o' :: 'u' :: 'r' :: _ => (updateState o 4)
| '5' :: _ | 'f' :: 'i' :: 'v' :: 'e' :: _ => (updateState o 5)
| '6' :: _ | 's' :: 'i' :: 'x' :: _ => (updateState o 6)
| '7' :: _ | 's' :: 'e' :: 'v' :: 'e' :: 'n' :: _ => (updateState o 7)
| '8' :: _ | 'e' :: 'i' :: 'g' :: 'h' :: 't' :: _ => (updateState o 8)
| '9' :: _ | 'n' :: 'i' :: 'n' :: 'e' :: _ => (updateState o 9)
| _ => o
let rec firstLast := Ξ» (o : Option Nat Γ Option Nat) (l : List Char) β¦
match l with
| [] => o
| _ :: cs => firstLast (extract_digit o l) cs
let scanLine := Ξ» (l : List Char) β¦ firstLast (none, none) l
let numbers := instructions.mapM ((uncurry Option.zip) β scanLine)
let numbers := numbers.map Ξ» l β¦ l.map Ξ» (a, b) β¦ 10*a + b
numbers.map (List.foldl (.+.) 0)