Skip to content

Instantly share code, notes, and snippets.

# JadenGeller/Advent.idr Created Dec 17, 2017

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
to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.