We can translate the problem into the language of permutations in the following manner:
sX will apply
circulate \(X\) times.
xA/B will be
pi A B.
pA/B we look up the positions of
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:
import Control.Permutation import Lightyear import Lightyear.Strings import Lightyear.Char import Control.Monad.State
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.