I saw a recent Advent of Code problem, and I was a bit surprised to see that part 1 was basically what I had been working on with my permutations library for Idris.

We'll use both the permutations and lightyear packages. As we shall see, a large reason that this problem is easy in Idris1 is the library support (which may be surprising to even Idris users).

We can translate the problem into the language of permutations in the following manner:

1. A spin sX will apply circulate $$X$$ times.

2. An exchange xA/B will be pi A B.

3. For pA/B we look up the positions of A and B and then swap them.

With that in mind, all we have to do is parse the input. This is easy in Idris, thanks to monadic parser combinators like those you might use in Haskell.

Here is the code:

module Mainimport Control.Permutation
import Lightyear
import Lightyear.Strings
import Lightyear.Char
import Control.Monad.State%access exportParser : Type -> Type
Parser = ParserT String (State (Vect 16 Char))num : Main.Parser Nat
num = abs <$> integerfin : Main.Parser (Fin 16) fin = assert_total$ (filter <$> integer) where filter 0 = FZ filter n = FS (either ?lifter id$ strengthen $filter$ n - 1)exchange : Main.Parser ()
exchange = do
char 'x'
n1 <- fin
char '/'
n2 <- fin
lift $modify (sigma (pi n1 n2)) pure ()swapChars : Char -> Char -> Vect n Char -> Vect n Char swapChars _ _ Nil = Nil swapChars c1 c2 (x :: xs) = if c1 == x then c2 :: swapChars c1 c2 xs else if c2 == x then c1 :: swapChars c2 c1 xs else x :: swapChars c1 c2 xsposition : Main.Parser () position = do st <- lift get char 'p' f <- anyChar char '/' s <- anyChar put$ swapChars f s st
pure ()applyN : Nat -> (a -> a) -> a -> a
applyN Z _ x = x
applyN (S m) f x = f (applyN m f x)spin : Main.Parser ()
spin = do
char 's'
n <- num
lift \$ modify (applyN n (reverse . sigma circulate . reverse))
pure ()step : Main.Parser ()
step = exchange <|> position <|> spinsteps : Main.Parser (Vect 16 Char)
steps = do
sepBy1 step (char ',')
getinitial : Vect 16 Char
initial = ['a', 'b', 'c', 'd', 'e', 'f', 'g', 'h', 'i', 'j', 'k', 'l', 'm', 'n', 'o', 'p']parse : String -> Vect 16 Char
parse s = execState (execParserT steps h) initial
where
h : State String
h = initialState (Just s) s 0main : IO ()
main = do
Left e => printLn e