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 Main

import Control.Permutation import Lightyear import Lightyear.Strings import Lightyear.Char import Control.Monad.State

%access export

Parser : Type -> Type Parser = ParserT String (State (Vect 16 Char))

num : Main.Parser Nat num = abs <$> integer fin : 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 xs position : 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 <|> spin

steps : Main.Parser (Vect 16 Char) steps = do sepBy1 step (char ',') get

initial : 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 0

main : IO () main = do x <- readFile "input.txt" case x of Right r => printLn (Main.parse r) Left e => printLn e

This gives the correct answer when run, in 82 lines. On the downside, it's a bit slower than we'd like - the initial program runs takes 3.1 seconds to run.

1: It's also a fairly nice demonstration of a case in which ATS is the best choice for the problem. We use Idris here because of the library support, but it is slower.