blog

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 Idris¹ 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.