Welcome everyone to the 2023 advent of code! Thank you all for stopping by and participating in it in programming.dev whether youre new to the event or doing it again.

This is an unofficial community for the event as no official spot exists on lemmy but ill be running it as best I can with Sigmatics modding as well. Ill be running a solution megathread every day where you can share solutions with other participants to compare your answers and to see the things other people come up with

Day 1: Trebuchet?!

Megathread guidelines

  • Keep top level comments as only solutions, if you want to say something other than a solution put it in a new post. (replies to comments can be whatever)
  • Code block support is not fully rolled out yet but likely will be in the middle of the event. Try to share solutions as both code blocks and using something such as https://topaz.github.io/paste/ or pastebin (code blocks to future proof it for when 0.19 comes out and since code blocks currently function in some apps and some instances as well if they are running a 0.19 beta)

FAQ

🔒This post will be unlocked when there is a decent amount of submissions on the leaderboard to avoid cheating for top spots

🔓 Edit: Post has been unlocked after 6 minutes

  • soulsource@discuss.tchncs.deEnglish
    1·
    1 year ago

    [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)