Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Advent Day 5
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.