Advent of Code 2024 - Day 3

Stream: general

[James Sully]

Here's my solution. Feedback appreciated, and please post your own solution!

This one's pretty janky at the moment, using sort of pseudo parsers. I might clean it up later.
I took it as an opportunity to learn how String.Iterator works. I'll probably rework it with Std.Internal.Parsec.
I am particularly interested in seeing other peoples' solutions who didn't resort to full parser combinators though, since it feels like it ought to be a relatively simple problem, and I still don't feel like I have a good grasp on the string api.

structure MulInstruction where
  a : Nat
  b : Nat
  deriving Repr

def MulInstruction.execute : MulInstruction → Nat
| {a, b} => a * b

def parseString (iter : String.Iterator) (s : String)
  : Option (Unit × String.Iterator) := Id.run do
  let mut sIter := s.iter
  let mut iter' := iter
  while sIter.hasNext do
    if iter'.atEnd || sIter.curr != iter'.curr then
      return .none
    sIter := sIter.next
    iter' := iter'.next
  .some ((), iter')

def parseNat (iter : String.Iterator) : Option (Nat × String.Iterator)
  := Id.run do
  let mut iter' := iter
  while iter'.curr.isDigit do
    if iter'.hasNext then
      iter' := iter'.next
    else
      break
  let subs := iter.extract iter'
  match subs.toNat? with
  | .some n => .some (n, iter')
  | .none => .none

def parseMulInstruction (iter : String.Iterator)
  : Option (MulInstruction × String.Iterator) := do
  let (_, iter₁) ← parseString iter "mul("
  let (a, iter₂) ← parseNat iter₁
  let (_, iter₃) ← parseString iter₂ ","
  let (b, iter₄) ← parseNat iter₃
  let (_, iter₅) ← parseString iter₄ ")"
  .some ({a,b}, iter₅)

def extractUncorruptedMuls (input : String) : Array MulInstruction := Id.run do
  let mut instructions := #[]
  let mut iter := input.iter
  while iter.hasNext do
    if let .some (mul, iter') := parseMulInstruction iter then
      instructions := instructions.push mul
      iter := iter'
    else
      iter := iter.next
  instructions

def part1 (input : String) : Nat :=
  let instructions := extractUncorruptedMuls input
  instructions.map (·.execute)
  |>.toList
  |>.sum

def extractMulsWithToggle (input : String) : Array MulInstruction := Id.run do
  let mut instructions := #[]
  let mut iter := input.iter
  let mut mulEnabled := true

  while iter.hasNext do
    if let .some (_, iter') := parseString iter "don't()" then
      iter := iter'
      mulEnabled := false
      continue

    if let .some (_, iter') := parseString iter "do()" then
      iter := iter'
      mulEnabled := true
      continue

    if mulEnabled then
      if let .some (mul, iter') := parseMulInstruction iter then
        instructions := instructions.push mul
        iter := iter'
        continue

    iter := iter.next

  instructions

def part2 (input : String) : Nat :=
  let instructions := extractMulsWithToggle input
  instructions.map (·.execute)
    |>.toList
    |>.sum

[James Sully]

version 2: turns out Std.Internal.Parsec is extremely straightforward to use, love it. Next I think the extract* functions ought to be refactored into Parsers somehow.

import Std.Internal.Parsec.String

namespace Day03
open Std.Internal.Parsec.String

structure MulInstruction where
  a : Nat
  b : Nat
  deriving Repr

def MulInstruction.execute : MulInstruction → Nat
| {a, b} => a * b

def pmulInstruction : Parser MulInstruction := do
  let _ ← pstring "mul("
  let a ← digits
  let _ ← pstring ","
  let b ← digits
  let _ ← pstring ")"
  return {a, b}

def extractUncorruptedMuls (input : String) : Array MulInstruction := Id.run do
  let mut instructions := #[]
  let mut iter := input.iter
  while iter.hasNext do
    if let .success iter' mul := pmulInstruction iter then
      instructions := instructions.push mul
      iter := iter'
    else
      iter := iter.next
  instructions

def part1 (input : String) : Nat :=
  let instructions := extractUncorruptedMuls input
  instructions.map (·.execute)
  |>.toList
  |>.sum

def extractMulsWithToggle (input : String) : Array MulInstruction := Id.run do
  let mut instructions := #[]
  let mut iter := input.iter
  let mut mulEnabled := true

  while iter.hasNext do
    if let .success iter' _ := pstring "don't()" iter then
      iter := iter'
      mulEnabled := false
      continue

    if let .success iter' _ := pstring "do()" iter then
      iter := iter'
      mulEnabled := true
      continue

    if mulEnabled then
      if let .success iter' mul := pmulInstruction iter then
        instructions := instructions.push mul
        iter := iter'
        continue

    iter := iter.next

  instructions

def part2 (input : String) : Nat :=
  let instructions := extractMulsWithToggle input
  instructions.map (·.execute)
    |>.toList
    |>.sum

[Kyle Miller]

Tip: there are some parsers to consume strings/chars:

def pmulInstruction : Parser MulInstruction := do
  skipString "mul("
  let a ← digits
  skipChar ','
  let b ← digits
  skipChar ')'
  return {a, b}

[Kyle Miller]

One of the benefits of structures is projections:

def MulInstruction.execute (s : MulInstruction) : Nat := s.a * s.b

[Kyle Miller]

There's a many combinator:

def extractUncorruptedMuls (input : String) : Array MulInstruction :=
  match many pmulInstruction input.mkIterator with
  | .success _ instructions => instructions
  | .error .. => #[]

[James Sully]

Thanks! I'll use skipString and skipChar. I prefer the look of the pattern match for execute personally.

I think that definition of extractUncorruptedMuls is incorrect, because there will be a bunch of garbage data between them. Example input:

xmul(2,4)%&mul[3,7]!@^do_not_mul(5,5)+mul(32,64]then(mul(11,8)mul(8,5))

[James Sully]

I'm working on a parser version of extractUncorruptedMuls now, this is what I have so far. I'm trying to figure out how to skip any character:

partial def pmulInstructions : Parser (List MulInstruction) := do
  ( do
      let mul ← pmulInstruction
      let muls ← pmulInstructions
      return mul :: muls
  ) <|> (
    do
      -- ?? skip single character here
      pmulInstructions
  )

[James Sully]

I see in the definition of pchar they use any, but I can't figure out where to import any from.

@[inline]
def pchar (c : Char) : Parser Char := attempt do
  if (← any) = c then pure c else fail s!"expected: '{c}'"

[Kyle Miller]

Here's a way to handle the garbage:

partial def extractUncorruptedMuls (input : String) : Array MulInstruction :=
  let parser := do
    many ((some <$> pmulInstruction) <|> (skip *> pure none))
  match parser input.mkIterator with
  | .success _ instructions => instructions.filterMap id
  | .error .. => #[]

It accumulates Option MulInstruction, with garbage giving nones

[Kyle Miller]

open Std.Internal.Parsec for the rest of the combinators

[James Sully]

ah clever approach, thanks.

[Frédéric Dupuis]

BTW, what are the plans for Std.Internal.Parsec? The name sounds like it's meant to be an implementation detail for something else and that we shouldn't be using it.

[James Sully]

yeah, i was also curious about that

[Kyle Miller]

Good question — all I know is that the release notes mentioned how to migrate to it, so I've been assuming it's ok to use.

[Kyle Miller]

(Full disclosure: I may have written said release notes, but it was reviewed!)

[Frédéric Dupuis]

In that case, maybe a more inviting name might be in order :-) In any case, for AoC, I've been trying out @François G. Dorais 's parser library.

[James Sully]

version 3 of part 1, thanks kyle for the help:

import Std.Internal.Parsec.String
import Std.Internal.Parsec

namespace Day03
open Std.Internal.Parsec.String
open Std.Internal.Parsec (skip many many1 attempt)

structure MulInstruction where
  a : Nat
  b : Nat
  deriving Repr

def MulInstruction.execute : MulInstruction → Nat
| {a, b} => a * b

def pmulInstruction : Parser MulInstruction := do
  skipString "mul("
  let a ← digits
  skipChar ','
  let b ← digits
  skipChar ')'
  return {a, b}

def pmulInstructions : Parser (Array MulInstruction) :=
  Array.filterMap id <$> many step
  where
    step := some <$> attempt pmulInstruction <|> skip *> pure none

def part1 (input : String) : Nat :=
  let instructions : Array MulInstruction := pmulInstructions.run input
    |>.toOption
    |>.getD #[]
  instructions.map (·.execute)
    |>.toList
    |>.sum

[James Sully]

part 2 will be slightly trickier because it's stateful

[James Sully]

version 3 of part 2:

partial def pMulInstructionsWithToggle (mulEnabled : Bool)
  : Parser (List MulInstruction) :=
  if mulEnabled then
    pdont <|> pdo <|> mul <|> next <|> done
  else
    pdont <|> pdo <|>         next <|> done
  where
    pdont := attempt <| pstring "don't()" *> pMulInstructionsWithToggle false
    pdo := attempt <| pstring "do()" *> pMulInstructionsWithToggle true
    mul := do
      let mulInstr ← attempt pmulInstruction
      let instructions ← pMulInstructionsWithToggle mulEnabled
      return mulInstr :: instructions
    next := skip *> pMulInstructionsWithToggle mulEnabled
    done := eof *> pure []

def part2 (input : String) : Nat :=
  let instructions := (pMulInstructionsWithToggle true).run input
    |>.toOption
    |>.getD []
  instructions.map (·.execute)
    |>.sum

[Ayhon]

This is my version of Day 3, also using Std.Internal.Parsec which I asked about yesterday. I couldn't get the "parse a mul instruction if it's present, otherwise skip the first character" part to work until I looked at this discussion and saw that I needed to add an attempt to my mul parser, so thanks for that!

import Std.Internal.Parsec
import Std.Internal.Parsec.String

namespace Day3
open Std.Internal.Parsec.String
open Std.Internal.Parsec (skip many many1 attempt)

abbrev Input := String

def parse_input(ls: List String): Input := String.join ls

namespace Part1
  def mul: Parser (Nat × Nat):= do
    skipString "mul("
    let num1 <- digits
    skipChar ','
    let num2 <- digits
    skipString ")"
    /- dbg_trace s!"{num1} × {num2}" -/
    return (num1 , num2)

  def mul_or_move: Parser (Option (Nat × Nat)) := do
    let res <- some <$> (attempt mul) <|> skip *> pure none
    /- dbg_trace s!"{res}" -/
    return res

  def corrupt_memory := do
    let results <- many mul_or_move
    let res := results.toList.reduceOption
    /- dbg_trace s!"results={results}" -/
    /- dbg_trace s!"res={res}" -/
    return res

  def solve(mem: Input): Int :=
    /- dbg_trace mem; -/
    match corrupt_memory mem.iter with
    | .success _ ls => ls.map (fun (a,b) => a*b) |>.sum
    | .error _ err => dbg_trace err; -1

end Part1

namespace Part2
  def pdo := skipString "do()" *> pure true
  def pdont := skipString "don't()" *> pure false
  def do_dont := pdo <|> pdont

  def mul_or_do_dont_or_move :=
    let mulRes := some ∘ Sum.inr
    let dosRes := some ∘ Sum.inl
    mulRes <$> attempt Part1.mul <|>
    dosRes <$> attempt do_dont   <|>
    skip *> pure none

  def corrupt_memory := do
    let results <- many mul_or_do_dont_or_move
    return results.toList.reduceOption

  def computeResult(ls: List (Bool ⊕ (Nat × Nat)))(enabled: Bool): Nat :=
    match ls, enabled with
    | .inl en :: rest, _ => computeResult rest en
    | .inr (a,b) :: rest, true => computeResult rest enabled + a * b
    | .inr _ :: rest, false => computeResult rest enabled
    | [], _ => 0

  def solve(mem: Input): Int :=
    match corrupt_memory mem.iter with
    | .success _ tks => computeResult tks true
    | .error _ err => dbg_trace err; -1

end Part2

[Ayhon]

Something else that I wasn't expecting is that whenever I try to use >> instead of *>, Lean get's stuck in a typeclass instance problem. I haven't yet understood why this would be the case though. Isn't bind defined for Parser, since we use it in do-notation? Perhaps I'm not understanding the difference between >> and *> correctly :shrug:

[Markus Himmel]

Frédéric Dupuis said:

BTW, what are the plans for Std.Internal.Parsec? The name sounds like it's meant to be an implementation detail for something else and that we shouldn't be using it.

Std.Internal.Parsec exists to enable specific use-cases within Lean core. It does not try to be a complete general-purpose parser library. It should be considered an implementation detail and is not a stable API. If it works for your specific use case, then feel free to use it, but we may change it in the future. We will try to make it easy to migrate if that happens, but we won't put as much effort into it as we would for a public/stable API. I haven't looked into the parser library linked above, but that one definitely has the advantage of being written with downstream users in mind.

[James Sully]

Ayhon said:

let res := results.toList.reduceOption

Oh, I didn't know about reduceOption, that's handy

[James Sully]

I like the approach of sort of parsing it into an IR with explicit representation of the the enabled toggles

[James Sully]

makes a lot of sense

[François G. Dorais]

Solution using my Parser library:

import Parser.RegEx

open Parser Char

def part1 : TrivialParser Substring Char Nat := do
  let mulRE := RegEx.compile! r"mul\(([1-9][0-9]{,2}),([1-9][0-9]{,2})\)|."
  let mut sum := 0
  while !(← test endOfInput) do
    let a ← matchStr mulRE
    match a[0]! >>= Substring.toNat?, a[1]! >>= Substring.toNat? with
    | some x, some y => sum := sum + x * y
    | _, _ => continue
  return sum

def part2 : TrivialParser Substring Char Nat := do
  let re := RegEx.compile! r"mul\(([1-9][0-9]{,2}),([1-9][0-9]{,2})\)|(do\(\))|(don't\(\))|."
  let mut state := true
  let mut sum := 0
  while !(← test endOfInput) do
    let a ← matchStr re
    match a[0]! >>= Substring.toNat?, a[1]! >>= Substring.toNat?, a[2]!, a[3]! with
    | some x, some y, none, none => sum := bif state then sum + x * y else sum
    | none, none, some _, none => state := true
    | none, none, none, some _ => state := false
    | _, _, _, _ => continue
  return sum

def str := include_str "input.txt"

#eval part1.run str
#eval part2.run str

[Ayhon]

Didn't know about include_str. It seems pretty useful

[Greg Shuflin]

François G. Dorais said:

Solution using my Parser library:

import Parser.RegEx

open Parser Char

def part1 : TrivialParser Substring Char Nat := do
  let mulRE := RegEx.compile! r"mul\(([1-9][0-9]{,2}),([1-9][0-9]{,2})\)|."
  let mut sum := 0
  while !(← test endOfInput) do
    let a ← matchStr mulRE
    match a[0]! >>= Substring.toNat?, a[1]! >>= Substring.toNat? with
    | some x, some y => sum := sum + x * y
    | _, _ => continue
  return sum

def part2 : TrivialParser Substring Char Nat := do
  let re := RegEx.compile! r"mul\(([1-9][0-9]{,2}),([1-9][0-9]{,2})\)|(do\(\))|(don't\(\))|."
  let mut state := true
  let mut sum := 0
  while !(← test endOfInput) do
    let a ← matchStr re
    match a[0]! >>= Substring.toNat?, a[1]! >>= Substring.toNat?, a[2]!, a[3]! with
    | some x, some y, none, none => sum := bif state then sum + x * y else sum
    | none, none, some _, none => state := true
    | none, none, none, some _ => state := false
    | _, _, _, _ => continue
  return sum

def str := include_str "input.txt"

#eval part1.run str
#eval part2.run str

I am working on this problem right now, and found your library, and was put off from it by the lack of general documentation. It would be great if you could add a general explanation of how to get started with the library on the README or some other place it links to

[Greg Shuflin]

in particular I didn't know that your library had regex functionality, I was just looking for ways that you could match strings against a regex in lean

[François G. Dorais]

Indeed, missing docs is one of the reasons why I keep delaying a v1.0.0 release. The examples directory is the closest thing to a getting started guide for now. The regex functionality is new and still experimental; there are no examples for that yet. I'm actually happily surprised it worked for this problem!

Please add an issue to pressure me into writing docs that would help you.

[Frédéric Dupuis]

Even running doc-gen on it and hosting the result somewhere would be a big gain in usability I think. I've used it for a few AoC problems as well and it's very nice!

[François G. Dorais]

That already exists https://www.dorais.org/lean4-parser/doc/ But I never posted the link anywhere :oops: (Fixed now.)

[Frédéric Dupuis]

Ah nice, thanks!

[Greg Shuflin]

François G. Dorais said:

Indeed, missing docs is one of the reasons why I keep delaying a v1.0.0 release. The examples directory is the closest thing to a getting started guide for now. The regex functionality is new and still experimental; there are no examples for that yet. I'm actually happily surprised it worked for this problem!

Please add an issue to pressure me into writing docs that would help you.

https://github.com/fgdorais/lean4-parser/issues/57

[JJ]

my initial solution to today. i might rewrite it to try and learn monadic parsing? it just so happened there were enough tricks you could do that String.splitOn + Option + functional primitives were able to make it work, though.

def parse_mul (input : String) : List (List Nat) :=
  input.replace "\n" "" |>.splitOn "mul" |>.tail
  |>.map (fun x => (x.splitOn ")").head!.stripPrefix "(")
  |>.map (fun x => (x.splitOn ",").map String.toNat?)
  |>.filter (fun x => x.length == 2 && x.all Option.isSome)
  |>.map (fun x => x.map Option.get!)

def solution (input : String) : String :=
  let p1 := parse_mul input
    |>.foldl (fun acc x => (x.foldl (· * ·) 1) + acc) 0
  let p2 := input.splitOn "do()"
    |>.map (fun x => (x.splitOn "don't()").get! 0)
    |>.foldl (fun acc x => acc ++ x) ""
    |> parse_mul
    |>.foldl (fun acc x => (x.foldl (· * ·) 1) + acc) 0
  s!"{p1}, {p2}"