0 | module Days.Day17

  2 | import Data.String

  3 | import Data.List1

  4 | import Data.Bits

  5 | import Data.Fin

  6 | import Data.IORef

  7 | import System

  8 | import System.Concurrency

 10 | import Control.Eff

 11 | import Control.Eff.Except

 12 | import Control.MonadRec

 14 | import Util

 16 | data ErrorL = LParse | LSolve

 18 | Show ErrorL where

 19 |   show LParse = "parsing"

 20 |   show LSolve = "solving"

 22 | ParseError : Type -> Type

 23 | ParseError = ExceptL LParse String

 25 | SolveError : Type -> Type

 26 | SolveError = ExceptL LSolve String

 28 | record RegisterFile where

 29 |   constructor MkRf

 30 |   a, b, c : Integer

 31 | %name RegisterFile rf

 33 | parseRegister : Has ParseError fs => String -> Eff fs (Char, Integer)

 34 | parseRegister str = do

 35 |   _ ::: name_part :: content_part :: [] <-

 36 |     pure . split (== ' ') . trim $ str

 37 |     | _ => throwAt LParse "Register incorrectly specified"

 38 |   reg :: _ <- pure . unpack $ name_part

 39 |     | _ => throwAt LParse "Name part missing?"

 40 |   content <- noteAt LParse "Register \{show reg} contained non-integer: {content_part}" $

 41 |     parseInteger content_part

 42 |   pure (reg, content)

 44 | parseRegisterFile : Has ParseError fs => List String -> Eff fs RegisterFile

 45 | parseRegisterFile strs = do

 46 |   regs <- traverse parseRegister strs

 47 |   (_, a) <- noteAt LParse "Missing A register" $ find ((== 'A') . fst) regs

 48 |   (_, b) <- noteAt LParse "Missing B register" $ find ((== 'B') . fst) regs

 49 |   (_, c) <- noteAt LParse "Missing C register" $ find ((== 'C') . fst) regs

 50 |   pure $ MkRf a b c

 52 | record Input where

 53 |   constructor MkInput

 54 |   registers : RegisterFile

 55 |   len : Nat

 56 |   program : Vect (S (S len)) (Fin 8)

 57 |   ip : Fin (S len)

 58 |   halted : Bool

 59 | %name Input i

 61 | Show Input where

 62 |   show (MkInput registers _ program ip halted) =

 63 |     let status : String = if halted then "Halted" else "Running" in

 64 |     """

 74 | parseInput : Has ParseError fs => String -> Eff fs Input

 75 | parseInput str = do

 76 |   registers ::: [program] :: [] <- pure . split null . lines . trim $ str

 77 |     | xs => throwAt LParse $ "Input had too many components: \{show xs}"

 78 |   registers <- parseRegisterFile registers

 79 |   _ ::: program :: [] <- pure . split (== ' ') . trim $ program

 80 |     | xs => throwAt LParse $ "Program had too many components: \{show xs}"

 81 |   let is ::: js = split (== ',') program

 82 |   program : List (Fin 8) <-

 83 |     noteAt LParse "Program contained invalid opcodes: \{show (is :: js)}" $

 84 |     traverse parsePositive (is :: js)

 85 |   S (S len) <- pure . length $ program

 86 |     | _ => throwAt LParse $ "Program not long enough"

 87 |   program <- noteAt LParse "Program not long enough" $

 88 |     toVect (S (S len)) program

 89 |   pure $ MkInput registers len program 0 False

 93 | executeOnce :

 94 |   Has SolveError fs => Has (State Input) fs => Has (Writer Integer) fs =>

 95 |   Eff fs Bool

 96 | executeOnce = do

 97 |   False <- map halted get

 98 |     | _ => pure False

 99 |   (opcode, _) <- readInst

100 |   case opcode of

101 |     -- adv

102 |     0 => do

103 |       numer <- map (.registers.a) get

104 |       operand <- combo

105 |       False <- pure $ operand < 0

106 |         | _ => throwAt LSolve "Negative adv power: \{show operand}"

107 |       let denom = 1 `shiftL` (integerToNat operand)

108 |       modify {registers.a := numer `div` denom}

109 |       incIp

110 |     -- bxl

111 |     1 => do

112 |       operand <- literal

113 |       modify {registers.b $= (xor operand)}

114 |       incIp

115 |     -- bst

116 |     2 => do

117 |       operand <- combo

118 |       modify {registers.b := operand `mod` 8}

119 |       incIp

120 |     -- jnz

121 |     3 => do

122 |       a <- map (.registers.a) get

123 |       if a /= 0

124 |         then do

125 |           operand <- literal

126 |           jump operand

127 |         else incIp

128 |     -- bxc

129 |     4 => do

130 |       c <- map (.registers.c) get

131 |       modify {registers.b $= (xor c)}

132 |       incIp

133 |     -- out

134 |     5 => do

135 |       operand <- combo

136 |       tell $ operand `mod` 8

137 |       incIp

138 |     -- bdv

139 |     6 => do

140 |       numer <- map (.registers.a) get

141 |       operand <- combo

142 |       False <- pure $ operand < 0

143 |         | _ => throwAt LSolve "Negative bdv power: \{show operand}"

144 |       let denom = 1 `shiftL` (integerToNat operand)

145 |       modify {registers.b := numer `div` denom}

146 |       incIp

147 |     -- cdv

148 |     7 => do

149 |       numer <- map (.registers.a) get

150 |       operand <- combo

151 |       False <- pure $ operand < 0

152 |         | _ => throwAt LSolve "Negative cdv power: \{show operand}"

153 |       let denom = 1 `shiftL` (integerToNat operand)

154 |       modify {registers.c := numer `div` denom}

155 |       incIp

156 |   where

157 |     -- Read the instruction at point

158 |     readInst : Eff fs (Fin 8, Fin 8)

159 |     readInst = do

160 |       input <- get

161 |       let instr = (weaken input.ip) `index` input.program

162 |       let oper = (FS input.ip) `index` input.program

163 |       pure (instr, oper)

164 |     -- Parse a combo operand from the instruction at point

165 |     combo : Eff fs Integer

166 |     combo = do

167 |       (_, operand) <- readInst

168 |       case operand of

169 |         4 => map (.registers.a) get

170 |         5 => map (.registers.b) get

171 |         6 => map (.registers.c) get

172 |         7 => throwAt LSolve "Combo operand with value 7"

173 |         operand => pure $ finToInteger operand

174 |     -- Parse a literal operand from the instruction at point

175 |     literal : Eff fs Integer

176 |     literal = do

177 |       (_, operand) <- readInst

178 |       pure $ finToInteger operand

179 |     -- Set the instruction pointer to the provided value, halting if that would

180 |     -- go off the end of the tape

181 |     jump : (address : Integer) -> Eff fs Bool

182 |     jump address = do

183 |       MkInput registers len program ip halted <- get

184 |       case integerToFin address (S len) of

185 |         -- Off end of tape, stopping

186 |         Nothing => do

187 |           modify {halted := True}

188 |           pure False

189 |         -- Still on tape, going to location

190 |         Just ip => do

191 |           put $ MkInput registers len program ip halted

192 |           pure True

193 |     -- Increment the instruction pointer or halt

194 |     incIp : Eff fs Bool

195 |     incIp = do

196 |       input <- get

197 |       jump (finToInteger input.ip + 2)

200 | execute :

201 |   Has SolveError fs => Has (State Input) fs => Has (Writer Integer) fs =>

202 |   Eff fs ()

203 | execute =

204 |   trSized forever () execute'

205 |   where

206 |     execute' : (v : Fuel) -> () -> Eff fs (Step Smaller v () ())

207 |     execute' Dry x = pure $ Done ()

208 |     execute' (More y) x = do

209 |       again <- executeOnce

210 |       case again of

211 |         False => pure $ Done ()

212 |         True => pure $

213 |           Cont y (believe_me ()) ()

216 | findQuine' :

217 |   Has SolveError fs => Has IO fs =>

218 |   (input : Input) -> (a : Integer) -> (program : List Integer)

219 |   -> Eff fs (Maybe Integer)

220 | findQuine' input a program = do

221 |   when (a `mod` 100_000 == 0) $

222 |     printLn a

223 |   let modified : Input = {registers.a := a} input

224 |   input_ref <- newIORef modified

225 |   writer_ref : IORef (List _) <- newIORef program

226 |   let ran = runExceptAt LSolve

227 |             $ execute {fs = [SolveError, State Input, Writer Integer]}

228 |   maybe_error <-

229 |     send $ runEff ran

230 |       [handleState {m = IO} (readIORef input_ref) (writeIORef input_ref)

231 |       , handleWriter {m = IO} (handle_writer input_ref writer_ref)]

232 |   output <- readIORef writer_ref

233 |   rethrowAt LSolve maybe_error

234 |   if output == []

235 |     then pure $ Just a

236 |     else pure Nothing

237 |   where

238 |     abort : IORef Input -> IO ()

239 |     abort x = modifyIORef x {halted := True}

240 |     handle_writer :

241 |       (input_ref : IORef Input) -> (state_ref : IORef (List Integer)) -> (item : Integer)

242 |       -> IO ()

243 |     handle_writer input_ref state_ref item = do

244 |       x :: xs <- readIORef state_ref

245 |         | _ => abort input_ref

246 |       if x == item

247 |         then do

248 |           writeIORef state_ref xs

249 |           pure ()

250 |         else abort input_ref

252 | findQuine :

253 |   Has SolveError fs => Has IO fs =>

254 |   (input : Input) -> (a : Integer) -> (program : List Integer)

255 |   -> Eff fs Integer

256 | findQuine input a program = do

257 |   -- Setup and launch our tasks

258 |   inbox : Channel Integer <- makeChannel

259 |   outbox : Channel (Integer, Maybe Integer) <- makeChannel

260 |   threads <- launch_tasks inbox outbox

261 |   -- send out an initial round of blocks

262 |   traverse_ (channelPut inbox) starting_blocks

263 |   -- enter our loop

264 |   trSized forever (block_size + thread_count) (execute' inbox outbox)

265 |   where

266 |     -- Tuning constants

267 |     thread_count : Nat

268 |     thread_count = 20

269 |     block_size : Nat

270 |     block_size = 100_000

271 |     -- Get the blocks

272 |     starting_blocks : List Integer

273 |     starting_blocks = starting' thread_count 0

274 |       where

275 |       starting' : (count : Nat) -> (current : Nat) -> List Integer

276 |       starting' 0 current = []

277 |       starting' (S k) current =

278 |         let rest = starting' k (current + block_size)

279 |         in (natToInteger current) :: rest

280 |     -- Individual block computation function

281 |     check_block : (v : Nat) -> Integer -> IO (Step Smaller v Integer (Maybe Integer))

282 |     check_block 0 i = pure $ Done Nothing

283 |     check_block (S k) i = do

284 |       let comp = runExceptAt LSolve $ findQuine' input i program {fs = [SolveError, IO]}

285 |       comp <- runEff comp [id]

286 |       case comp of

287 |         Left err => do

288 |           putStrLn err

289 |           pure $ Done Nothing

290 |         Right (Just res) => pure $ Done (Just res)

291 |         Right Nothing =>

292 |           pure $ Cont k (believe_me ()) (i + 1)

293 |     -- Loop that will run on each of the threads

294 |     task :

295 |       (inbox : Channel Integer) -> (outbox : Channel (Integer, Maybe Integer)) ->

296 |       IO ()

297 |     task inbox outbox = do

298 |       -- get a block

299 |       block <- channelGet inbox

300 |       -- process block

301 |       res <- trSized block_size block check_block

302 |       -- send it back

303 |       channelPut outbox (block, res)

304 |       -- loop

305 |       task inbox outbox

306 |     -- launch up the tasks

307 |     launch_tasks :

308 |       (inbox : Channel Integer) -> (outbox : Channel (Integer, Maybe Integer)) ->

309 |       Eff fs (List ThreadID)

310 |     launch_tasks inbox outbox = launch_tasks' thread_count

311 |       where

312 |       launch_tasks' : (counter : Nat) -> Eff fs (List ThreadID)

313 |       launch_tasks' 0 = pure []

314 |       launch_tasks' (S k) = do

315 |         xs <- launch_tasks' k

316 |         x <- send $ fork (task inbox outbox)

317 |         pure $ x :: xs

318 |     -- loop that will fill up the threads and drain values

319 |     execute' :

320 |       (inbox : Channel Integer) -> (outbox : Channel (Integer, Maybe Integer)) ->

321 |       (v : Fuel) -> Nat -> Eff fs (Step Smaller v Nat Integer)

322 |     execute' inbox outbox Dry k = pure $ Done 0

323 |     execute' inbox outbox (More v) block_start = do

324 |       -- Send out a block

325 |       channelPut inbox (cast block_start)

326 |       -- Wait for someone to be ready with a block

327 |       (res_block_start, result) <- channelGet outbox

328 |       -- Check to see if new block has the solution

329 |       -- Return or recurse

330 |       case result of

331 |         Nothing =>

332 |           pure $ Cont v (believe_me ()) (block_start + block_size)

333 |         Just result =>

334 |           pure $ Done result

337 | part1 : String -> Eff [IO, Except String] (ShowString, Input)

338 | part1 str = do

339 |   input <- tagAt LParse $ parseInput str

340 |   input_ref <- newIORef input

341 |   let state_get : IO Input = readIORef input_ref

342 |   let state_put : Input -> IO () = writeIORef input_ref

343 |   let ran = foldWriter (the (List Integer) []) (\acc, x => x :: acc)

344 |             . runExceptAt LSolve

345 |             $ execute {fs = [SolveError, State Input, Writer Integer]}

346 |   (maybe_error, reversed_output) <-

347 |     send $ runEff ran [handleState {m = IO} state_get state_put]

348 |   case maybe_error of

349 |     Left err => throw "solving: \{err}"

350 |     Right _ => do

351 |       let output = joinBy "," . map show . reverse $ reversed_output

352 |       pure (Show output, input)

355 | part2 : Input -> Eff [IO, Except String] ShowString

356 | part2 i = do

357 |   a <- tagAt LSolve $ findQuine i 0 (map finToInteger . toList $ i.program)

358 |   pure $ Show (show a)

362 | testInput : (a, b, c : Integer) -> (program : List (Fin 8)) -> Input

363 | testInput a b c program =

364 |   let S (S length) = length program

365 |       Just program = toVect (S (S length)) program

366 |   in MkInput (MkRf a b c) length program 0 False

369 | testStep :

370 |   Has IO fs => Has (Except String) fs =>

371 |   (input : Input) -> (expected : RegisterFile)

372 |   -> Eff fs ()

373 | testStep input expected = do

374 |   input_ref <- newIORef input

375 |   let stepped = foldWriter (the (List Integer) []) (\acc, x => x :: acc)

376 |               . runExceptAt LSolve

377 |               $ executeOnce {fs = [SolveError, State Input, Writer Integer]}

378 |   (maybe_error, reversed_output) <-

379 |     send $ runEff stepped [handleState {m = IO} (readIORef input_ref) (writeIORef input_ref)]

380 |   got <- readIORef input_ref

381 |   case maybe_error of

382 |     Left err => throw "opcode err:\n  \{err}"

383 |     Right _ =>

384 |       if got.registers.a == expected.a &&

385 |          got.registers.b == expected.b &&

386 |          got.registers.c == expected.c

387 |         then pure ()

388 |         else throw $ error_string got

389 |   where

390 |     error_string : (got : Input) -> String

391 |     error_string got =

392 |       let got_indented = unlines . map ("  " <+>) . lines . show $ got

393 |       in """

406 | testAll :

407 |   Has IO fs => Has (Except String) fs =>

408 |   (input : Input) -> (test_rf : RegisterFile -> Maybe String) -> (expected : List Integer)

409 |   -> Eff fs ()

410 | testAll input test_rf expected = do

411 |   input_ref <- newIORef input

412 |   let stepped = foldWriter (the (List Integer) []) (\acc, x => x :: acc)

413 |               . runExceptAt LSolve

414 |               $ execute {fs = [SolveError, State Input, Writer Integer]}

415 |   (maybe_error, reversed_output) <-

416 |     send $ runEff stepped [handleState {m = IO} (readIORef input_ref) (writeIORef input_ref)]

417 |   got <- readIORef input_ref

418 |   case maybe_error of

419 |     Left err => throw "opcode err:\n  \{err}"

420 |     Right _ =>

421 |       case test_rf got.registers of

422 |         Just err => throw $ register_error got err

423 |         Nothing =>

424 |           if (reverse reversed_output) == expected

425 |             then pure ()

426 |             else throw $ output_error got (reverse reversed_output)

427 |   where

428 |     register_error : (got : Input) -> (err : String) -> String

429 |     register_error got err =

430 |       """

441 |     output_error : (input : Input) -> (got : List Integer) -> String

442 |     output_error input got =

443 |       let input_indented = unlines . map ("    " <+>) . lines . show $ input

444 |       in

445 |       """

458 | runTest : (name : String) -> (test : Eff [Except String, IO] ()) -> IO ()

459 | runTest name test = do

460 |   putStrLn "Running \{name}:"

461 |   test <- runEff (runExcept test) [id]

462 |   case test of

463 |     Left err => do

464 |       putStrLn "  Failure!\n"

465 |       putStrLn $ unlines . map ("  " <+>) . lines $ err

466 |       exitFailure

467 |     Right _ =>

468 |       putStrLn "  Pass."

471 | tests : IO ()

472 | tests = do

473 |   -- If register C contains 9, the program 2,6 would set register B to 1.

474 |   runTest "C=9 P=2,6" $

475 |     testStep (testInput 0 0 9 [2, 6]) (MkRf 0 1 9)

476 |   -- If register A contains 10, the program 5,0,5,1,5,4 would output 0,1,2.

477 |   runTest "A=10 P=5,0,5,1,5,4" $

478 |     testAll (testInput 10 0 0 [5, 0, 5, 1, 5, 4]) (const Nothing) [0, 1, 2]

479 |   -- If register A contains 2024, the program 0,1,5,4,3,0 would output

480 |   -- 4,2,5,6,7,7,7,7,3,1,0 and leave 0 in register A.

481 |   runTest "A=2024 P=0,1,5,4,3,0" $

482 |     testAll

483 |       (testInput 2024 0 0 [0,1,5,4,3,0])

484 |       (\x => if x.a == 0 then Nothing else Just "A=0")

485 |       [4, 2, 5, 6, 7, 7, 7, 7, 3, 1, 0]

486 |   -- If register B contains 29, the program 1,7 would set register B to 26.

487 |   runTest "B=29 P=1,7" $

488 |     testStep (testInput 0 29 0 [1, 7]) (MkRf 0 26 0)

489 |   -- If register B contains 2024 and register C contains 43690, the program 4,0

490 |   -- would set register B to 44354.

491 |   runTest "B=2024 C=43690 P=4,0" $

492 |     testStep (testInput 0 2024 43690 [4, 0]) (MkRf 0 44354 43690)

493 |   -- example

494 |   runTest "example" $

495 |     testAll

496 |       (testInput 729 0 0 [0, 1, 5, 4, 3, 0])

497 |       (const Nothing)

498 |       [4, 6, 3, 5, 6, 3, 5, 2, 1, 0]