Day 2: Cube Conundrum

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

  • soulsourceEnglish
    1·
    10 months 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.

    Solution 
    structure Draw (α : Type) where
  red : α
  green : α
  blue : α
  deriving Repr

structure Game where
  id : Nat
  draw : List $ Draw Nat
  deriving Repr

def parse (input : String) : Option $ List Game :=
  let lines := input.splitTrim (. == '\n')
  let lines := lines.filter (not ∘ String.isEmpty)
  let parse_single_line : (String → Option Game):= λ (l : String) ↦ do
    let parse_id := λ (s : String) ↦ do
      let rest ← if s.startsWith "Game " then some (s.drop 5) else none
      rest.toNat?
    let parse_draw := λ (s : String) ↦ do
      let s := s.splitTrim (· == ',')
      let findAndRemoveTail := λ (s : String) (t : String) ↦
        if s.endsWith t then
          some $ String.dropRight s (t.length)
        else
          none
      let update_draw_parse := λ (pd : Option (Draw (Option String))) (c : String) ↦ do
        let old ← pd
        let red := findAndRemoveTail c " red"
        let green := findAndRemoveTail c " green"
        let blue := findAndRemoveTail c " blue"
        match red, green, blue with
        | some red, none, none => match old.red with
          | none => some $ {old with red := some red}
          | some _ => none
        | none, some green, none => match old.green with
          | none => some $ {old with green := some green}
          | some _ => none
        | none, none, some blue => match old.blue with
          | none => some $ {old with blue := some blue}
          | some _ => none
        | _, _, _  => none
      let parsed_draw ← s.foldl update_draw_parse (some $ Draw.mk none none none)
      let parsed_draw := {
        red := String.toNat? <$> parsed_draw.red,
        green := String.toNat? <$> parsed_draw.green,
        blue := String.toNat? <$> parsed_draw.blue : Draw _}
      let extractOrFail := λ (s : Option $ Option Nat) ↦ match s with
        | none => some 0
        | some none => none
        | some $ some x => some x
      let red ← extractOrFail parsed_draw.red
      let green ← extractOrFail parsed_draw.green
      let blue ← extractOrFail parsed_draw.blue
      pure { red := red, blue := blue, green := green : Draw _}
    let parse_draws := λ s ↦ List.mapM parse_draw $ s.splitTrim (· == ';')
    let (id, draw) ← match l.splitTrim (· == ':') with
    | [l, r] => Option.zip (parse_id l) (parse_draws r)
    | _ => none
    pure { id := id, draw := draw}
  lines.mapM parse_single_line

def part1 (games : List Game) : Nat :=
  let draw_possible := λ g ↦ g.red ≤ 12 && g.green ≤ 13 && g.blue ≤ 14
  let possible := flip List.all draw_possible
  let possible_games := games.filter (possible ∘ Game.draw)
  possible_games.map Game.id |> List.foldl Nat.add 0

def part2 (games : List Game) : Nat :=
  let powerOfGame := λ (g : Game) ↦
    let minReq := λ (c : Draw Nat → Nat) ↦
      g.draw.map c |> List.maximum? |> flip Option.getD 0
    minReq Draw.red * minReq Draw.green * minReq Draw.blue
  let powers := games.map powerOfGame
  powers.foldl Nat.add 0