Note: this is broken.
If it were not broken, this would be a compiler which, given the description of a n-symbol m-state Turing machine, would produce a corresponding Burro program, thus showing that Burro is Turing complete. But it's broken. So it doesn't show that.
It is basically a mechanized version of the construction described in "Implementing a Turing Machine in Burro" in the Burro.lhs file in the Burro 2.0 distribution, with some gaps cleaned up.
Both tape cells and TM state indexes are encoded as odd positive integers, starting at 1, then 3, 5, etc. The start state is considered to be state 1. Blank tape cells are considered to be 1.
The TM should be supplied as a list of pairs: (state-index, choices). The choices is a list of quadruples: (if-read-this-symbol, write-this-symbol, move-this-direction, go-to-this-state-next).
The TM state list must begin with state 1, then state 3, state 5, etc with no gaps. Similarly, each choices list must begin with if-read 1, then if-read 3, 5, etc with no gaps and no omissions (every choices list must name every possible tape symbol.)
Transitioning to any state beyond the last defined state halts the machine.
Each TM tape cell is encoded as 4 Burro data tape cells like so: (state-index, junk, tm-tape-cell-contents, junk)
module TM2Burro where type StateID = Integer type Choices = [(Integer, Integer, Integer, Integer)] -- BROKEN testFor :: [(Integer, String)] -> String -> String testFor branches else_ = testFor' 1 branches where testFor' n  = else_ testFor' n ((val, code):rest) = if n == val then "--(" ++ (testFor' (n+2) rest) ++ ">/" ++ code ++ ">)<" else error "Mismatch, should be " ++ (show n) ++ " not " ++ (show val) write 0 = "" write n = "+" ++ write (n-1) move (-1) = "<<<<" move 1 = ">>>>" move 0 = "" next n = "<<" ++ (write n) compileState :: Choices -> String compileState choices = ">>" ++ (testFor (map (\(i, w, m, n) -> (i, (write w) ++ (move m) ++ (next n))) choices) "") compileStates :: [(StateID, Choices)] -> String compileStates states = testFor (map (\(index, choices) -> (index, compileState choices)) states) "!" compileTM :: [(StateID, Choices)] -> String compileTM states = -- if the current state index isn't one of the possible states, set it to 1 (testFor (map (\(index, choices) -> (index, write index)) states) "+") ++ -- if the current tape cell isn't one of the possible tape symbols, set it to 1 (testFor (map (\(n, _, _, _) -> (n, write n)) (snd (head states))) "+") ++ -- turn off the halt flag "!" ++ compileStates states