Advent of Code - Intcode

Stream: general

[Chris Henson]

I'm planning to do Advent of Code in Lean this year for the first time, so I decided to go back and rewrite the 2019 Intcode machine as a bit of practice. Thought I'd post here in case others are curious or have feedback for me, here's the code: https://github.com/chenson2018/advent-of-code/blob/main/2019/LeanIntcode/LeanIntcode/Intcode.lean

[Kim Morrison]

match Nat.decLt should just be a plain if statement using <. Matching on the decidable instance yourself is just obfuscatory.

[Kim Morrison]

I'd use [i]? instead of get? everywhere.

[Kim Morrison]

The data ++ mkArray looks a bit smelly, but is probably fine.

[Kim Morrison]

If you wanted to prove things about this, you'd probably avoid partial and instead use a fuel parameter or fuel monad state.

[Kim Morrison]

If you wanted to be fancy with your monads, silent seems a bit out of place in the VM state, and instead could be stored in a monad context for running the VM.

[Chris Henson]

Thanks for the feedback! For the match Nat.decLt, I didn't know how to use an if statement and be able to construct something of type Fin based on the condition, is that possible?

[Kyle Miller]

if h : a < b then gives you the proposition inside the branches

[Chris Henson]

Kyle Miller said:

if h : a < b then gives you the proposition inside the branches

Ah thanks. I'd tried that, but with parenthesis which doesn't work.

[Chris Henson]

Kim Morrison said:

If you wanted to be fancy with your monads, silent seems a bit out of place in the VM state, and instead could be stored in a monad context for running the VM.

Yeah, this makes sense. For this (and informative error messages) I guess StateT IO would be more appropriate.

[Chris Henson]

I guess you could also argue that the input/output fields should be held in state too. They are not really aspects of the machine, but implementation details of how something external interacts with its effects.