From 5e555d94508037ffe3a4b58b6d1660925887e342 Mon Sep 17 00:00:00 2001 From: Matt Russell Date: Tue, 3 Dec 2024 18:50:04 +0000 Subject: [PATCH] wip --- Aoc2024/Day03/Solve.lean | 27 +++++++++++++++------------ 1 file changed, 15 insertions(+), 12 deletions(-) diff --git a/Aoc2024/Day03/Solve.lean b/Aoc2024/Day03/Solve.lean index 4d48d8a..4542d36 100644 --- a/Aoc2024/Day03/Solve.lean +++ b/Aoc2024/Day03/Solve.lean @@ -3,6 +3,8 @@ import Aoc2024.Day03.Examples import Aoc2024.Day03.Parser import Aoc2024.Day03.Types +-- Part 1 + private def Instruction.value : Instruction -> Int | Instruction.mul n m => n * m | _ => 1 @@ -11,23 +13,24 @@ def solvePart1 (s : String) : Int := findInstructions s |>.sumBy (ยท.value) #guard solvePart1 exampleInputPart1 == 161 +-- Part 2 + private structure State where isEnabled: Bool enabledMuls: List Instruction -def State.enable (s : State): State := { s with isEnabled := true } -def State.disable (s : State): State := { s with isEnabled := false } -def State.recordMul (instruction : Instruction) (s : State): State := +private def State.enable (s : State): State := { s with isEnabled := true } +private def State.disable (s : State): State := { s with isEnabled := false } +private def State.recordMul (instruction : Instruction) (s : State): State := { s with enabledMuls := instruction :: s.enabledMuls } -def State.initial: State := { isEnabled := true, enabledMuls := [] } - -private def processInstruction (instruction: Instruction): StateM State Unit := - match instruction with - | Instruction.mul _ _ => do - if (<- get).isEnabled then - modify (State.recordMul instruction) - | Instruction.do => modify State.enable - | Instruction.dont => modify State.disable +private def State.initial: State := { isEnabled := true, enabledMuls := [] } + +private def processInstruction : Instruction -> StateM State Unit + | i@(Instruction.mul _ _) => do + if (<- get).isEnabled then + modify (State.recordMul i) + | Instruction.do => modify State.enable + | Instruction.dont => modify State.disable private def getEnabledMuls (instructions : List Instruction) : List Instruction := instructions.forM processInstruction |>.run State.initial |>.snd.enabledMuls