Advent of Code, Day 2

day2.u

unique type Pos = Pos Nat

use Pos Pos

ability IntCode where
  add : Pos -> Pos -> Pos -> ()
  mul : Pos -> Pos -> Pos -> ()
  halt : ()

ability Error where
  error : Text -> a

ability Memory where
  read : Pos -> Nat
  write : Pos -> Nat -> ()
  dump : [Nat]

outOfBounds x = error ("Memory address out of bounds: " ++ Nat.toText x)

eval : Request {IntCode} v ->{Error, Memory} [Nat]
eval instruction =
  case instruction of
    {IntCode.add x y dest -> k} ->
      handle eval in
        use Nat +
        k (write dest (read x + read y))
    {IntCode.mul x y dest -> k} ->
      handle eval in
        use Nat *
        k (write dest (read x * read y))
    {IntCode.halt -> _} -> Memory.dump
    { a } -> error "Out of memory."

access : [Nat] -> Request {Memory} v ->{Error} v
access mem instruction =
  case instruction of
    {Memory.read (Pos x) -> k} ->
      v = List.at x mem
      case v of
        None -> outOfBounds x
        Some v -> handle access mem in k v
    {Memory.write (Pos x) v -> k} ->
      mem' =
        if List.size mem > x then replace x v mem
        else
          outOfBounds x
          mem
      handle access mem' in !k
    {Memory.dump -> k} -> handle access mem in k mem
    { a } -> a

errors : Request m v -> Either Text v
errors failure =
  case failure of
    {Error.error e -> _} -> Left e
    { a } -> Right a