Advent Day 5

Advent.idr

import SignedNat
import Data.Vect

step : (Fin n, Vect n SignedNat) -> (SignedNat, Vect n SignedNat)
step (i, xs) = let delta = index i xs in
                   let xs' = updateAt i succ xs in
                   let i' = (toSignedNatNat (finToNat i)) + delta in
                   (i', xs')

signedNatToFin : SignedNat -> (m : Nat) -> Maybe (Fin m)
signedNatToFin _      Z     = Nothing
signedNatToFin (NS _) _     = Nothing
signedNatToFin ZZ     (S _) = Just FZ
signedNatToFin (PS n) (S m) = map FS (natToFin n m)

solve : (Fin n, Vect n SignedNat) -> Either (Fin n, Vect n SignedNat) SignedNat
solve z {n} with (step z)
  solve z {n} | (i, xs) with (signedNatToFin i n)
    solve z {n} | (i, xs) | Just i' = Left (i', xs)
    solve z {n} | (i, xs) | Nothing = Right i

manyStep : (Nat, a) -> (a -> Either a b) -> (Nat, b)
manyStep (n, x) f with (f x)
  manyStep (n, x) f | Left x' = manyStep (S n, x') f
  manyStep (n, x) f | Right y = (S n, y)

manySolve : Vect (S n) SignedNat -> Nat
manySolve xs = let (n, _) = manyStep (0, (FZ, xs)) solve in n