I had to give Uiua another go today. (run it here)

{"Card 1: 41 48 83 86 17 | 83 86  6 31 17  9 48 53"
 "Card 2: 13 32 20 16 61 | 61 30 68 82 17 32 24 19"
 "Card 3:  1 21 53 59 44 | 69 82 63 72 16 21 14  1"
 "Card 4: 41 92 73 84 69 | 59 84 76 51 58  5 54 83"
 "Card 5: 87 83 26 28 32 | 88 30 70 12 93 22 82 36"
 "Card 6: 31 18 13 56 72 | 74 77 10 23 35 67 36 11"}

LtoDec ← ∧(+ ×10:) :0
StoDec ← LtoDec▽≥0. ▽≤9. -@0

# Split on spaces, drop dross, parse ints
≡(⊜□≠0.⊐∵(StoDec)↘ 2⊜(□)≠@\s.⊔)

# Find matches
≡(/+/+⊠(⌕)⊃(⊔⊢↙ 1)(⊔⊢↙¯1))

# part 1
/+ⁿ:2-1 ▽±..

# part 2 - start with matches and initial counts
=..:
# len times: get 1st of each, rotate both, add new counts
⍥(⬚0+↯: ⊙⊙∩(↻1) ⊙:∩(⊢.))⧻.
/+⊙;

Rust

This one wasn't too bad. The example for part 2 even tells you how to process everything by visiting each card once in order. Another option could be to recursively look at all won copies, but that's probably much less efficient.

Nim

This one was pretty simple, just parse the numbers into sets and check the size of the intersection. Part 2 just made the scoring mechanism a little more complicated.

• Day 4, part 1
• Day 4, part 2

LANGUAGE: Nim

Welcome to the advent of parsing!
Took me a lot more time than it should (Please, don't check prior commits 😅).

day_04.nim

Haskell

11:39 -- I spent most of the time reading the scoring rules and (as usual) writing a parser...

import Control.Monad
import Data.Bifunctor
import Data.List

readCard :: String -> ([Int], [Int])
readCard =
  join bimap (map read) . second tail . break (== "|") . words . tail . dropWhile (/= ':')

countShared = length . uncurry intersect

part1 = sum . map ((\n -> if n > 0 then 2 ^ (n - 1) else 0) . countShared)

part2 = sum . foldr ((\n a -> 1 + sum (take n a) : a) . countShared) []

main = do
  input <- map readCard . lines <$> readFile "input04"
  print $ part1 input
  print $ part2 input

Factor on github (with comments and imports):

: line>cards ( line -- winning-nums player-nums )
  ":|" split rest
  [
    [ CHAR: space = ] trim
    split-words harvest [ string>number ] map
  ] map first2
;

: points ( winning-nums player-nums -- n )
  intersect length
  dup 0 > [ 1 - 2^ ] when
;

: part1 ( -- )
  "vocab:aoc-2023/day04/input.txt" utf8 file-lines
  [ line>cards points ] map-sum .
;

: follow-card ( i commons -- n )
  [ 1 ] 2dip
  2dup nth swapd
  over + (a..b]
  [ over follow-card ] map-sum
  nip +
;

: part2 ( -- )
  "vocab:aoc-2023/day04/input.txt" utf8 file-lines
  [ line>cards intersect length ] map
  dup length  swap '[ _ follow-card ]
  map-sum .
;

Python

Questions and feedback welcome!

import collections
import re

from .solver import Solver

class Day04(Solver):
  def __init__(self):
    super().__init__(4)
    self.cards = []

  def presolve(self, input: str):
    lines = input.rstrip().split('\n')
    self.cards = []
    for line in lines:
      left, right = re.split(r' +\| +', re.split(': +', line)[1])
      left, right = map(int, re.split(' +', left)), map(int, re.split(' +', right))
      self.cards.append((list(left), list(right)))

  def solve_first_star(self):
    points = 0
    for winning, having in self.cards:
      matches = len(set(winning) & set(having))
      if not matches:
        continue
      points += 1 << (matches - 1)
    return points

  def solve_second_star(self):
    factors = collections.defaultdict(lambda: 1)
    count = 0
    for i, (winning, having) in enumerate(self.cards):
      count += factors[i]
      matches = len(set(winning) & set(having))
      if not matches:
        continue
      for j in range(i + 1, i + 1 + matches):
        factors[j] = factors[j] + factors[i]
    return count

Python

Part 1: https://github.com/porotoman99/Advent-of-Code-2023/blob/main/Day%204/part1.py

Part 2: https://github.com/porotoman99/Advent-of-Code-2023/blob/main/Day%204/part2.py

I found out about this event for the first time yesterday and was able to get caught up in time for day 4.

(python) Much easier than day 3.

import pathlib

base_dir = pathlib.Path(__file__).parent
filename = base_dir / "day4_input.txt"

with open(base_dir / filename) as f:
    lines = f.read().splitlines()

score = 0

extra_cards = [0 for _ in lines]
n_cards = [1 for _ in lines]

for i, line in enumerate(lines):
    _, numbers = line.split(":")
    winning, have = numbers.split(" | ")

    winning_numbers = {int(n) for n in winning.split()}
    have_numbers = {int(n) for n in have.split()}

    have_winning_numbers = winning_numbers & have_numbers
    n_matches = len(have_winning_numbers)

    if n_matches:
        score += 2 ** (n_matches - 1)

    j = i + 1
    for _ in range(n_matches):
        if j >= len(lines):
            break
        n_cards[j] += n_cards[i]
        j += 1

answer_p1 = score
print(f"{answer_p1=}")

answer_p2 = sum(n_cards)
print(f"{answer_p2=}")

Dart Solution

Okay, that's more like it. Simple parsing and a bit of recursion, and fits on one screen. Perfect for day 4 :-)

int matchCount(String line) => line
    .split(RegExp('[:|]'))
    .skip(1)
    .map((ee) => ee.trim().split(RegExp(r'\s+')).map(int.parse))
    .map((e) => e.toSet())
    .reduce((s, t) => s.intersection(t))
    .length;

late List matches;
late List totals;

int scoreFor(int ix) {
  if (totals[ix] != 0) return totals[ix];
  return totals[ix] =
      [for (var m in 0.to(matches[ix])) scoreFor(m + ix + 1) + 1].sum;
}

part1(List lines) =>
    lines.map((e) => pow(2, matchCount(e) - 1).toInt()).sum;

part2(List lines) {
  matches = [for (var e in lines) matchCount(e)];
  totals = List.filled(matches.length, 0);
  return matches.length + 0.to(matches.length).map(scoreFor).sum;
}

Ruby

[email protected]

Somehow took way longer on the second part than the first part trying a recursive approach and then realizing that was dumb.

https://github.com/snowe2010/advent-of-code/blob/master/ruby_aoc/2023/day04/day04.rb

APL

I'm using this years' AoC to learn (Dyalog) APL, so this is probably terrible code. I'm happy to receive pointers for improvement, particularly if there is a way to write the same logic with tacit functions or inner/outer products that I missed.

input←⊃⎕NGET'inputs/day4.txt'1
num_matches←'Card [ \d]+: ([ 0-9]+) \| ([ 0-9]+)'⎕S{≢↑∩/0~⍨¨{,⎕CSV⍠'Separator' ' '⊢⍵'S'3}¨⍵.(1↓Lengths↑¨Offsets↓¨⊂Block)} input
⎕←+/2*1-⍨0~⍨num_matches ⍝ part 1
⎕←+/{⍺←0 ⋄ ⍺=≢⍵:⍵ ⋄ (⍺+1)∇⍵ + (≢⍵)↑∊((⍺+1)⍴0)(num_matches[⍺]⍴⍵[⍺])((≢⍵)⍴0)}(≢num_matches)⍴1 ⍝ part 2

I enjoyed this one. It was a nice simple break after Days 1 and 3; the type of basic puzzle I expect from the first few days of Advent of Code. Pretty simple logic in this one, I don't think I would change too much. I'm sure I'll find a way to clean up how it's written a bit, but I'm happy with this one today.

https://github.com/capitalpb/advent_of_code_2023/blob/main/src/solvers/day04.rs

struct Scratchcard {
    winning_numbers: HashSet,
    player_numbers: HashSet,
}

impl Scratchcard {
    fn from(input: &str) -> Scratchcard {
        let (_, numbers) = input.split_once(':').unwrap();
        let (winning_numbers, player_numbers) = numbers.split_once('|').unwrap();
        let winning_numbers = winning_numbers
            .split_ascii_whitespace()
            .filter_map(|number| number.parse::().ok())
            .collect::>();
        let player_numbers = player_numbers
            .split_ascii_whitespace()
            .filter_map(|number| number.parse::().ok())
            .collect::>();

        Scratchcard {
            winning_numbers,
            player_numbers,
        }
    }

    fn matches(&self) -> u32 {
        self.winning_numbers
            .intersection(&self.player_numbers)
            .count() as u32
    }
}

pub struct Day04;

impl Solver for Day04 {
    fn star_one(&self, input: &str) -> String {
        input
            .lines()
            .map(Scratchcard::from)
            .map(|card| {
                let matches = card.matches();
                if matches == 0 {
                    0
                } else {
                    2u32.pow(matches - 1)
                }
            })
            .sum::()
            .to_string()
    }

    fn star_two(&self, input: &str) -> String {
        let cards: Vec = input.lines().map(Scratchcard::from).collect();
        let mut card_counts = vec![1usize; cards.len()];

        for card_number in 0..cards.len() {
            let matches = cards[card_number].matches();

            if matches == 0 {
                continue;
            }

            for i in 1..=matches {
                card_counts[card_number + i as usize] += card_counts[card_number];
            }
        }

        card_counts.iter().sum::().to_string()
    }
}

Nice and easy.

::: spoiler Lua

-- SPDX-FileCopyrightText: 2023 Jummit
--
-- SPDX-License-Identifier: GPL-3.0-or-later

local function nums(str)
	local res = {}
	for num in str:gmatch("%d+") do
		res[num] = true
	end
	return res
end

local cards = {}
local points = 0
for line in io.open("4.input"):lines() do
	local winning, have = line:match("Card%s*%d+: (.*) | (.*)")
	winning = nums(winning)
	have = nums(have)
	local first = true
	local score = 0
	local matching = 0
	for num in pairs(have) do
		if winning[num] then
			matching = matching + 1
			if first then
				first = false
				score = score + 1
			else
				score = score * 2
			end
		end
	end
	points = points + score
	table.insert(cards, {have=have, wins=matching, count=1})
end
print(points)

local cardSum = 0
for i, card in ipairs(cards) do
	cardSum = cardSum + card.count
	for n = i + 1, i + card.wins do
		cards[n].count = cards[n].count + card.count
	end
end
print(cardSum)

Language: Python

Numbers = set[int]
Card    = list[Numbers]

def read_cards(stream=sys.stdin) -> Iterator[Card]:
    for line in stream:
        yield [set(map(int, n.split())) for n in line.split(':')[-1].split('|')]

def main(stream=sys.stdin) -> None:
    cards  = [numbers & winning for winning, numbers in read_cards(stream)]
    points = sum(2**(len(card)-1) for card in cards if card)
    print(points)

def main(stream=sys.stdin) -> None:
    cards  = [numbers & winning for winning, numbers in read_cards(stream)]
    counts = defaultdict(int)

    for index, card in enumerate(cards, 1):
        counts[index] += 1
        for copy in range(index + 1, index + len(card) + 1):
            counts[copy] += counts[index]

    print(sum(counts.values()))

GitHub Repo

Feels like the challenges are getting easier than harder currently. Fairly straightforward when doing it the lazy way with python. ::: spoiler Python

import re

winning_number_pattern: re.Pattern = re.compile(r' +([\d ]*?) +\|')
lottery_number_pattern: re.Pattern = re.compile(r'\| +([\d ]*)')


def get_winning_numbers(line: str) -> set[str]:
    return set(winning_number_pattern.search(line).group(1).split())


def get_lottery_numbers(line: str) -> set[str]:
    return set(lottery_number_pattern.search(line).group(1).split())


def get_winnings(winning_numbers: set[str], lottery_numbers: set[str]) -> int:
    return int(2 ** (len(winning_numbers.intersection(lottery_numbers)) - 1))


def puzzle_1() -> int:
    points: int = 0
    with open('day4_scratchcards.txt', 'r', encoding='utf-8') as file:
        for line in file:
            points += get_winnings(get_winning_numbers(line), get_lottery_numbers(line))
    return points


class ScratchCard:
    def __init__(self, line: str):
        self.amount: int = 1
        self.winnings: int = len(get_winning_numbers(line).intersection(get_lottery_numbers(line)))

    def update(self, extra: int) -> None:
        self.amount = self.amount + extra

    def __radd__(self, other):
        return self.amount + other


def puzzle_2() -> int:
    scratch_card_list: list[ScratchCard] = []
    with open('day4_scratchcards.txt', 'r', encoding='utf-8') as file:
        for line in file:
            scratch_card_list.append(ScratchCard(line))

    for i, scratch_card in enumerate(scratch_card_list):
        for j in range(1, scratch_card.winnings + 1):
            try:
                scratch_card_list[i + j].update(scratch_card.amount)
            except IndexError:
                pass
    return sum(scratch_card_list)


if __name__ == '__main__':
    print(puzzle_1())
    print(puzzle_2())

Language: C

Another day of parsing, another day of strsep() to the rescue. Today was one of those satisfying days where the puzzle text is complicated but the solution is simple once well understood.

GitHub link

:::spoiler Code (29 lines)

int main()
{
	char line[128], *rest, *tok;
	int nextra[200]={0}, nums[10], nnums;
	int p1=0,p2=0, id,val,nmatch, i;

	for (id=0; (rest = fgets(line, sizeof(line), stdin)); id++) {
		nnums = nmatch = 0;

		while ((tok = strsep(&rest, " ")) && !strchr(tok, ':'))
			;
		while ((tok = strsep(&rest, " ")) && !strchr(tok, '|'))
			if ((val = atoi(tok)))
				nums[nnums++] = val;
		while ((tok = strsep(&rest, " ")))
			if ((val = atoi(tok)))
				for (i=0; i

PHP

Today was the easiest day so far IMHO. Today, I coded in PHP, a horrible language that produces even worse code. (Ok, full confession, I fed my family for about half a decade on PHP. I seemed to have gotten stuck with it, and so I earned a PhD to escape it.)

Anyway, the only trouble I had was I forgot about the explode function's capacity to return empty strings. Once I filtered those I had the correct answer on the first one, and then 10 minutes later I had the second part. I wrote my code true to raw php's awful idioms, though I didn't make it web based. I read from stdin.

My code is linked on github:

• https://github.com/pngwen/advent-2023/blob/main/day-4a.php
• https://github.com/pngwen/advent-2023/blob/main/day-4b.php

C# Recursion Time! (max depth 24)

Today I learnt how to get multiple captures out of the same group in Regex. I also learnt how much a console line write slows down your app.... (2 seconds without, never finished with)

internal class Day4Task1 : IRunnable
    {
        public void Run()
        {
            var inputLines = File.ReadAllLines("Days/Four/Day4Input.txt");
            var regex = new Regex("Card\\s*\\d*: ([\\d\\s]{2} )*\\|( [\\d\\s]{2})*");
            int sumScore = 0;

            foreach (var line in inputLines)
            {
                int lineScore = 0;
                var winningSet = new HashSet();
                var matches = regex.Match(line);
                foreach(Capture capture in matches.Groups[1].Captures) {
                    
                    winningSet.Add(capture.Value.Trim());
                }

                foreach (Capture capture in matches.Groups[2].Captures)
                {
                    if(winningSet.Contains(capture.Value.Trim()))
                    {
                        lineScore = lineScore == 0 ? 1 : lineScore * 2;
                    }
                }

                sumScore += lineScore;
                Console.WriteLine(lineScore.ToString());

            }

            Console.WriteLine("Sum:"+sumScore.ToString());
        }
    }

internal class Day4Task2 : IRunnable
    {
        private Regex _regex = new Regex("Card\\s*\\d*: ([\\d\\s]{2} )*\\|( [\\d\\s]{2})*");
        private Dictionary _matchCountCache = new Dictionary();
        private int _maxDepth = 0;

        public void Run()
        {
            var inputLines = File.ReadAllLines("Days/Four/Day4Input.txt");
            int sumScore = 0;

            for (int i = 0; i < inputLines.Length; i++)
            {
                sumScore += ScoreCard(i, inputLines, 0);
                Console.WriteLine("!!!" + i + "!!!");
            }

            Console.WriteLine("Sum:"+sumScore.ToString());
            Console.WriteLine("Max Recursion Depth:"+ _maxDepth.ToString());
        }

        private int ScoreCard(int lineId, string[] inputLines, int depth)
        {
            if( depth > _maxDepth )
            {
                _maxDepth = depth;
            }

            if(lineId >= inputLines.Length)
            {
                return 0;
            }

            int matchCount = 0;

            if (!_matchCountCache.ContainsKey(lineId)) {

                var winningSet = new HashSet();
                var matches = _regex.Match(inputLines[lineId]);
                foreach (Capture capture in matches.Groups[1].Captures)
                {
                    winningSet.Add(capture.Value.Trim());
                }

                foreach (Capture capture in matches.Groups[2].Captures)
                {
                    if (winningSet.Contains(capture.Value.Trim()))
                    {
                        matchCount++;
                    }
                }

                _matchCountCache[lineId] = matchCount;
            }

            matchCount = _matchCountCache[lineId];

            int totalCards = 1;
            while(matchCount > 0)
            {
                totalCards += ScoreCard(lineId+matchCount, inputLines, depth+1);
                matchCount--;
            }
            //Console.WriteLine("Finished processing id: " + lineId + " Sum is: " + totalCards);
            return totalCards;
        }
    }

Late as always (actually a day late by UK time).

My solution to this one runs slow, but it gets the job done. I didn't actually need the CardInfo struct by the time I was done, but couldn't be bothered to remove it. Previously, it held more than just count.

Day 04 in Rust 🦀

View formatted on GitLab

use std::{
    collections::BTreeMap,
    env, fs,
    io::{self, BufRead, BufReader, Read},
};

fn main() -> io::Result<()> {
    let args: Vec = env::args().collect();
    let filename = &args[1];
    let file1 = fs::File::open(filename)?;
    let file2 = fs::File::open(filename)?;
    let reader1 = BufReader::new(file1);
    let reader2 = BufReader::new(file2);

    println!("Part one: {}", process_part_one(reader1));
    println!("Part two: {}", process_part_two(reader2));
    Ok(())
}

fn process_part_one(reader: BufReader) -> u32 {
    let mut sum = 0;
    for line in reader.lines().flatten() {
        let card_data: Vec<_> = line.split(": ").collect();
        let all_numbers = card_data[1];
        let number_parts: Vec> = all_numbers
            .split('|')
            .map(|x| {
                x.replace("  ", " ")
                    .split_whitespace()
                    .map(|val| val.to_string())
                    .collect()
            })
            .collect();
        let (winning_nums, owned_nums) = (&number_parts[0], &number_parts[1]);
        let matches = owned_nums
            .iter()
            .filter(|num| winning_nums.contains(num))
            .count();
        if matches > 0 {
            sum += 2_u32.pow((matches - 1) as u32);
        }
    }
    sum
}

#[derive(Debug)]
struct CardInfo {
    count: u32,
}

fn process_part_two(reader: BufReader) -> u32 {
    let mut cards: BTreeMap = BTreeMap::new();
    for line in reader.lines().flatten() {
        let card_data: Vec<_> = line.split(": ").collect();
        let card_id: u32 = card_data[0]
            .replace("Card", "")
            .trim()
            .parse()
            .expect("is digit");
        let all_numbers = card_data[1];
        let number_parts: Vec> = all_numbers
            .split('|')
            .map(|x| {
                x.replace("  ", " ")
                    .split_whitespace()
                    .map(|val| val.to_string())
                    .collect()
            })
            .collect();
        let (winning_nums, owned_nums) = (&number_parts[0], &number_parts[1]);
        let matches = owned_nums
            .iter()
            .filter(|num| winning_nums.contains(num))
            .count();
        let card_details = CardInfo { count: 1 };
        if let Some(old_card_info) = cards.insert(card_id, card_details) {
            let card_entry = cards.get_mut(&card_id);
            card_entry.expect("card exists").count += old_card_info.count;
        };
        let current_card = cards.get(&card_id).expect("card exists");
        if matches > 0 {
            for _ in 0..current_card.count {
                for i in (card_id + 1)..=(matches as u32) + card_id {
                    let new_card_info = CardInfo { count: 1 };
                    if let Some(old_card_info) = cards.insert(i, new_card_info) {
                        let card_entry = cards.get_mut(&i).expect("card exists");
                        card_entry.count += old_card_info.count;
                    }
                }
            }
        }
    }
    let sum = cards.iter().fold(0, |acc, c| acc + c.1.count);
    sum
}

#[cfg(test)]
mod tests {
    use super::*;

    const INPUT: &str = "Card 1: 41 48 83 86 17 | 83 86  6 31 17  9 48 53
Card 2: 13 32 20 16 61 | 61 30 68 82 17 32 24 19
Card 3:  1 21 53 59 44 | 69 82 63 72 16 21 14  1
Card 4: 41 92 73 84 69 | 59 84 76 51 58  5 54 83
Card 5: 87 83 26 28 32 | 88 30 70 12 93 22 82 36
Card 6: 31 18 13 56 72 | 74 77 10 23 35 67 36 11";

    #[test]
    fn test_process_part_one() {
        let input_bytes = INPUT.as_bytes();
        assert_eq!(13, process_part_one(BufReader::new(input_bytes)));
    }

    #[test]
    fn test_process_part_two() {
        let input_bytes = INPUT.as_bytes();
        assert_eq!(30, process_part_two(BufReader::new(input_bytes)));
    }
}

My solution in C for part 1: https://git.sr.ht/~aidenisik/aoc23/tree/master/item/day4

I've been running a day behind the whole time since I forgot about it on day 1, I should really catch up.

EDIT: Part 2 is also uploaded.

Crystal

late because I had to skip two days of aoc. Fairly easy

input =  File.read("input.txt").lines

sum = 0
winnings = Array.new(input.size) {[1, 0]}
input.each_with_index do |line, i|
	card, values = line.split(":")
	nums = values.split("|").map(&.split.map(&.to_i))

	points = 0
	nums[1].each do |num|
		if nums[0].includes?(num)
			points = points == 0 ? 1 : points * 2
			winnings[i][1] += 1
	end    end
	sum += points
end
puts sum

winnings.each_with_index do |card, i|
	next if card[1] == 0
	(1..card[1]).each do |n|
		winnings[i+n][0] += card[0]
end    end
puts winnings.sum(&.[0])

Language: Python

Github

Catching up missed days.

[JavaScript] Swapped over to javascript from rust since I want to also practice some js. Managed to get part 1 in 4 minutes and got top 400 on the global leaderboard. Second part took a bit longer and took me 13 mins since I messed up by originally trying to append to the card array. (eventually swapped to keeping track of amounts in a separate array)

// Part 1
// ======

function part1(input) {
  const lines = input.split("\n");
  let sum = 0;

  for (const line of lines) {
    const content = line.split(":")[1];
    const winningNums = content.split("|")[0].match(/\d+/g);
    const myNums = content.split("|")[1].match(/\d+/g);

    let cardSum = 0;

    for (const num of winningNums) {
      if (myNums.includes(num)) {
        if (cardSum == 0) {
          cardSum = 1;
        } else {
          cardSum = cardSum * 2;
        }
      }
    }

    sum = sum + cardSum;
  }

  return sum;
}

// Part 2
// ======

function part2(input) {
  let lines = input.split("\n");
  let amount = Array(lines.length).fill(1);

  for (const [i, line] of lines.entries()) {
    const content = line.split(":")[1];
    const winningNums = content.split("|")[0].match(/\d+/g);
    const myNums = content.split("|")[1].match(/\d+/g);

    let cardSum = 0;

    for (const num of winningNums) {
      if (myNums.includes(num)) {
        cardSum += 1;
      }
    }

    for (let j = 1; j <= cardSum; j++) {
      if (i + j >= lines.length) {
        break;
      }
      amount[i + j] += amount[i];
    }
  }

  return lines.reduce((acc, line, i) => {
    return acc + amount[i];
  }, 0);
}

Code Link

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

I'm pretty sure that implementing part 2 in a naive way would cause Lean to demand a proof of termination, what might not be that easy to supply in this case... Luckily there's a way more elegant and way faster solution than the naive one, that can use structural recursion and therefore doesn't need an extra proof of termination.

structure Card where
  id : Nat
  winningNumbers : List Nat
  haveNumbers : List Nat
  deriving Repr

private def Card.matches (c : Card) : Nat :=
  flip c.haveNumbers.foldl 0 λo n ↦
    if c.winningNumbers.contains n then o + 1 else o

private def Card.score : Card → Nat :=
  (· / 2) ∘ (2^·) ∘ Card.matches

abbrev Deck := List Card

private def Deck.score : Deck → Nat :=
  List.foldl (· + ·.score) 0

def parse (input : String) : Option Deck := do
  let mut cards : Deck := []
  for line in input.splitOn "\n" do
    if line.isEmpty then
      continue
    let cs := line.splitOn ":"
    if p : cs.length = 2 then
      let f := String.trim $ cs[0]'(by simp[p])
      let g := String.trim $ cs[1]'(by simp[p])
      if not $ f.startsWith "Card " then
        failure
      let f := f.drop 5 |> String.trim
      let f ← f.toNat?
      let g := g.splitOn "|"
      if q : g.length = 2 then
        let winners := String.trim $ g[0]'(by simp[q])
        let draws := String.trim $ g[1]'(by simp[q])
        let toNumbers := λ(s : String) ↦
          s.split (·.isWhitespace)
          |> List.filter (not ∘ String.isEmpty)
          |> List.mapM String.toNat?
        let winners ← toNumbers winners
        let draws ← toNumbers draws
        cards := {id := f, winningNumbers := winners, haveNumbers := draws : Card} :: cards
      else
        failure
    else
      failure
  return cards -- cards is **reversed**, that's intentional. It doesn't affect part 1, but makes part 2 easier.

def part1 : Deck → Nat := Deck.score

def part2 (input : Deck) : Nat :=
  -- Okay, doing this brute-force is dumb.
  -- Instead let's compute how many cards each original card is worth, and sum that up.
  -- This relies on parse outputting the cards in **reverse** order.
  let multipliers := input.map Card.matches
  let sumNextN : Nat → List Nat → Nat := λn l ↦ (l.take n).foldl (· + ·) 0
  let rec helper : List Nat → List Nat → List Nat := λ input output ↦ match input with
    | [] => output
    | a :: as => helper as $ (1 + (sumNextN a output)) :: output
  let worths := helper multipliers []
  worths.foldl (· + ·) 0