Advent 2017 Day 1

captcha.idr

import Data.Vect
import Data.Vect.Views

%default total

infixl 1 &
(&) : a -> (a -> b) -> b
x & f = f x

rotate : Vect len elem -> Vect len elem
rotate xs {len} with (snocVect xs)
    rotate [] | Empty = []
    rotate (ys ++ [y]) {len=m + S Z} | Snoc z = rewrite (plusCommutative m 1)
                                                in [y] ++ ys

toDigit : Char -> Maybe Nat
toDigit c with (toNat c)
    toDigit c | n with (48 `isLTE` n)
        toDigit c | n | Yes prf = Just (n - 48)
        toDigit c | n | No _    = Nothing

toDigits : String -> Maybe (List Nat)
toDigits str = sequence (map toDigit (unpack str))

computeCaptcha : List Nat -> Nat
computeCaptcha xs = let xs' = fromList xs
                    in zip xs' (rotate xs') 
                     & toList 
                     & filter (uncurry (==)) 
                     & map fst 
                     & sum
                
solve : String -> Maybe Nat
solve str = toDigits str & map computeCaptcha