Indent all code four spaces to make the Markdown link trick work.
Chris Pressey
5 years ago
| 64 | 64 | for presentation.) As such, this document serves as an "executable |
| 65 | 65 | semantics", both defining the language and providing a ready tool. |
| 66 | 66 | |
| 67 | > module Language.Burro where | |
| 68 | > import System.Environment | |
| 67 | > module Language.Burro where | |
| 68 | > import System.Environment | |
| 69 | 69 | |
| 70 | 70 | |
| 71 | 71 | Inductive Definition of a Burro Program |
| 81 | 81 | If a and b are Burro programs, then ab is a Burro program. |
| 82 | 82 | Nothing else is a Burro program. |
| 83 | 83 | |
| 84 | > data Burro = Null | |
| 85 | > | ToggleHalt | |
| 86 | > | Inc | |
| 87 | > | Dec | |
| 88 | > | GoLeft | |
| 89 | > | GoRight | |
| 90 | > | Test Burro Burro | |
| 91 | > | Seq Burro Burro | |
| 92 | > deriving (Read, Eq) | |
| 84 | > data Burro = Null | |
| 85 | > | ToggleHalt | |
| 86 | > | Inc | |
| 87 | > | Dec | |
| 88 | > | GoLeft | |
| 89 | > | GoRight | |
| 90 | > | Test Burro Burro | |
| 91 | > | Seq Burro Burro | |
| 92 | > deriving (Read, Eq) | |
| 93 | 93 | |
| 94 | 94 | |
| 95 | 95 | Representation of Burro Programs |
| 101 | 101 | a given string of symbols into a Burro program is straightforward; all |
| 102 | 102 | symbols which are not Burro symbols are simply ignored. |
| 103 | 103 | |
| 104 | > instance Show Burro where | |
| 105 | > show Null = "e" | |
| 106 | > show ToggleHalt = "!" | |
| 107 | > show Inc = "+" | |
| 108 | > show Dec = "-" | |
| 109 | > show GoLeft = "<" | |
| 110 | > show GoRight = ">" | |
| 111 | > show (Test a b) = "(" ++ (show a) ++ "/" ++ (show b) ++ ")" | |
| 112 | > show (Seq a b) = (show a) ++ (show b) | |
| 113 | > | |
| 114 | > parse string = | |
| 104 | > instance Show Burro where | |
| 105 | > show Null = "e" | |
| 106 | > show ToggleHalt = "!" | |
| 107 | > show Inc = "+" | |
| 108 | > show Dec = "-" | |
| 109 | > show GoLeft = "<" | |
| 110 | > show GoRight = ">" | |
| 111 | > show (Test a b) = "(" ++ (show a) ++ "/" ++ (show b) ++ ")" | |
| 112 | > show (Seq a b) = (show a) ++ (show b) | |
| 113 | > | |
| 114 | > parse string = | |
| 115 | > let | |
| 116 | > (rest, acc) = parseProgram string Null | |
| 117 | > in | |
| 118 | > trim acc | |
| 119 | > | |
| 120 | > parseProgram [] acc = | |
| 121 | > ([], acc) | |
| 122 | > parseProgram ('e':rest) acc = | |
| 123 | > parseProgram rest (Seq acc Null) | |
| 124 | > parseProgram ('+':rest) acc = | |
| 125 | > parseProgram rest (Seq acc Inc) | |
| 126 | > parseProgram ('-':rest) acc = | |
| 127 | > parseProgram rest (Seq acc Dec) | |
| 128 | > parseProgram ('<':rest) acc = | |
| 129 | > parseProgram rest (Seq acc GoLeft) | |
| 130 | > parseProgram ('>':rest) acc = | |
| 131 | > parseProgram rest (Seq acc GoRight) | |
| 132 | > parseProgram ('!':rest) acc = | |
| 133 | > parseProgram rest (Seq acc ToggleHalt) | |
| 134 | > parseProgram ('(':rest) acc = | |
| 115 | 135 | > let |
| 116 | > (rest, acc) = parseProgram string Null | |
| 136 | > (rest', thenprog) = parseProgram rest Null | |
| 137 | > (rest'', elseprog) = parseProgram rest' Null | |
| 138 | > test = Test thenprog elseprog | |
| 117 | 139 | > in |
| 118 | > trim acc | |
| 119 | > | |
| 120 | > parseProgram [] acc = | |
| 121 | > ([], acc) | |
| 122 | > parseProgram ('e':rest) acc = | |
| 123 | > parseProgram rest (Seq acc Null) | |
| 124 | > parseProgram ('+':rest) acc = | |
| 125 | > parseProgram rest (Seq acc Inc) | |
| 126 | > parseProgram ('-':rest) acc = | |
| 127 | > parseProgram rest (Seq acc Dec) | |
| 128 | > parseProgram ('<':rest) acc = | |
| 129 | > parseProgram rest (Seq acc GoLeft) | |
| 130 | > parseProgram ('>':rest) acc = | |
| 131 | > parseProgram rest (Seq acc GoRight) | |
| 132 | > parseProgram ('!':rest) acc = | |
| 133 | > parseProgram rest (Seq acc ToggleHalt) | |
| 134 | > parseProgram ('(':rest) acc = | |
| 135 | > let | |
| 136 | > (rest', thenprog) = parseProgram rest Null | |
| 137 | > (rest'', elseprog) = parseProgram rest' Null | |
| 138 | > test = Test thenprog elseprog | |
| 139 | > in | |
| 140 | > parseProgram rest'' (Seq acc test) | |
| 141 | > parseProgram ('/':rest) acc = | |
| 142 | > (rest, acc) | |
| 143 | > parseProgram (')':rest) acc = | |
| 144 | > (rest, acc) | |
| 145 | > parseProgram (_:rest) acc = | |
| 146 | > parseProgram rest acc | |
| 147 | > | |
| 148 | > trim (Seq Null a) = trim a | |
| 149 | > trim (Seq a Null) = trim a | |
| 150 | > trim (Seq a b) = Seq (trim a) (trim b) | |
| 151 | > trim (Test a b) = Test (trim a) (trim b) | |
| 152 | > trim x = x | |
| 140 | > parseProgram rest'' (Seq acc test) | |
| 141 | > parseProgram ('/':rest) acc = | |
| 142 | > (rest, acc) | |
| 143 | > parseProgram (')':rest) acc = | |
| 144 | > (rest, acc) | |
| 145 | > parseProgram (_:rest) acc = | |
| 146 | > parseProgram rest acc | |
| 147 | > | |
| 148 | > trim (Seq Null a) = trim a | |
| 149 | > trim (Seq a Null) = trim a | |
| 150 | > trim (Seq a b) = Seq (trim a) (trim b) | |
| 151 | > trim (Test a b) = Test (trim a) (trim b) | |
| 152 | > trim x = x | |
| 153 | 153 | |
| 154 | 154 | |
| 155 | 155 | Group Properties of Burro Programs |
| 167 | 167 | If aa' = e and bb' = e, (a/b)(b'/a') = e. |
| 168 | 168 | If aa' = e and bb' = e, abb'a' = e. |
| 169 | 169 | |
| 170 | > inverse Null = Null | |
| 171 | > inverse ToggleHalt = ToggleHalt | |
| 172 | > inverse Inc = Dec | |
| 173 | > inverse Dec = Inc | |
| 174 | > inverse GoLeft = GoRight | |
| 175 | > inverse GoRight = GoLeft | |
| 176 | > inverse (Test a b) = Test (inverse b) (inverse a) | |
| 177 | > inverse (Seq a b) = Seq (inverse b) (inverse a) | |
| 170 | > inverse Null = Null | |
| 171 | > inverse ToggleHalt = ToggleHalt | |
| 172 | > inverse Inc = Dec | |
| 173 | > inverse Dec = Inc | |
| 174 | > inverse GoLeft = GoRight | |
| 175 | > inverse GoRight = GoLeft | |
| 176 | > inverse (Test a b) = Test (inverse b) (inverse a) | |
| 177 | > inverse (Seq a b) = Seq (inverse b) (inverse a) | |
| 178 | 178 | |
| 179 | 179 | For every Burro program x, annihilationOf x is always equivalent |
| 180 | 180 | computationally to e. |
| 181 | 181 | |
| 182 | > annihilationOf x = Seq x (inverse x) | |
| 182 | > annihilationOf x = Seq x (inverse x) | |
| 183 | 183 | |
| 184 | 184 | |
| 185 | 185 | State Model for Burro Programs |
| 199 | 199 | appears on the tape.) The second list contains everything to the right of |
| 200 | 200 | the tape head, in the same order as it appears on the tape. |
| 201 | 201 | |
| 202 | > data Tape = Tape [Integer] [Integer] | |
| 203 | > deriving (Read) | |
| 204 | > | |
| 205 | > instance Show Tape where | |
| 206 | > show t@(Tape l r) = | |
| 207 | > let | |
| 208 | > (Tape l' r') = strip t | |
| 209 | > in | |
| 210 | > show (reverse l') ++ "<" ++ (show r') | |
| 202 | > data Tape = Tape [Integer] [Integer] | |
| 203 | > deriving (Read) | |
| 204 | > | |
| 205 | > instance Show Tape where | |
| 206 | > show t@(Tape l r) = | |
| 207 | > let | |
| 208 | > (Tape l' r') = strip t | |
| 209 | > in | |
| 210 | > show (reverse l') ++ "<" ++ (show r') | |
| 211 | 211 | |
| 212 | 212 | When comparing two tapes for equality, we must disregard any zero cells |
| 213 | 213 | farther to the left/right than the outermost non-zero cells. Specifically, |
| 217 | 217 | Also, the current cell must be the same for both tapes (that is, tape heads |
| 218 | 218 | must be in the same location) for two tapes to be considered equal. |
| 219 | 219 | |
| 220 | > stripzeroes list = (reverse (sz (reverse list))) | |
| 221 | > where sz [] = [] | |
| 222 | > sz (0:rest) = sz rest | |
| 223 | > sz x = x | |
| 224 | > | |
| 225 | > ensurecell [] = [0] | |
| 226 | > ensurecell x = x | |
| 227 | > | |
| 228 | > strip (Tape l r) = Tape (ensurecell (stripzeroes l)) (stripzeroes r) | |
| 229 | > | |
| 230 | > tapeeq :: Tape -> Tape -> Bool | |
| 231 | > tapeeq t1 t2 = | |
| 232 | > let | |
| 233 | > (Tape t1l t1r) = strip t1 | |
| 234 | > (Tape t2l t2r) = strip t2 | |
| 235 | > in | |
| 236 | > (t1l == t2l) && (t1r == t2r) | |
| 237 | > | |
| 238 | > instance Eq Tape where | |
| 239 | > t1 == t2 = tapeeq t1 t2 | |
| 220 | > stripzeroes list = (reverse (sz (reverse list))) | |
| 221 | > where sz [] = [] | |
| 222 | > sz (0:rest) = sz rest | |
| 223 | > sz x = x | |
| 224 | > | |
| 225 | > ensurecell [] = [0] | |
| 226 | > ensurecell x = x | |
| 227 | > | |
| 228 | > strip (Tape l r) = Tape (ensurecell (stripzeroes l)) (stripzeroes r) | |
| 229 | > | |
| 230 | > tapeeq :: Tape -> Tape -> Bool | |
| 231 | > tapeeq t1 t2 = | |
| 232 | > let | |
| 233 | > (Tape t1l t1r) = strip t1 | |
| 234 | > (Tape t2l t2r) = strip t2 | |
| 235 | > in | |
| 236 | > (t1l == t2l) && (t1r == t2r) | |
| 237 | > | |
| 238 | > instance Eq Tape where | |
| 239 | > t1 == t2 = tapeeq t1 t2 | |
| 240 | 240 | |
| 241 | 241 | A convenience function for creating an inital tape is also provided. |
| 242 | 242 | |
| 243 | > tape :: [Integer] -> Tape | |
| 244 | > tape x = Tape [head x] (tail x) | |
| 243 | > tape :: [Integer] -> Tape | |
| 244 | > tape x = Tape [head x] (tail x) | |
| 245 | 245 | |
| 246 | 246 | We now define some operations on tapes that we will use in the semantics. |
| 247 | 247 | First, operations on tapes that alter or access the cell under the tape head. |
| 248 | 248 | |
| 249 | > inc (Tape (cell:left) right) = Tape (cell + 1 : left) right | |
| 250 | > dec (Tape (cell:left) right) = Tape (cell - 1 : left) right | |
| 251 | > get (Tape (cell:left) right) = cell | |
| 252 | > set (Tape (_:left) right) value = Tape (value : left) right | |
| 249 | > inc (Tape (cell:left) right) = Tape (cell + 1 : left) right | |
| 250 | > dec (Tape (cell:left) right) = Tape (cell - 1 : left) right | |
| 251 | > get (Tape (cell:left) right) = cell | |
| 252 | > set (Tape (_:left) right) value = Tape (value : left) right | |
| 253 | 253 | |
| 254 | 254 | Next, operations on tapes that move the tape head. |
| 255 | 255 | |
| 256 | > left (Tape (cell:[]) right) = Tape [0] (cell:right) | |
| 257 | > left (Tape (cell:left) right) = Tape left (cell:right) | |
| 258 | > right (Tape left []) = Tape (0:left) [] | |
| 259 | > right (Tape left (cell:right)) = Tape (cell:left) right | |
| 256 | > left (Tape (cell:[]) right) = Tape [0] (cell:right) | |
| 257 | > left (Tape (cell:left) right) = Tape left (cell:right) | |
| 258 | > right (Tape left []) = Tape (0:left) [] | |
| 259 | > right (Tape left (cell:right)) = Tape (cell:left) right | |
| 260 | 260 | |
| 261 | 261 | Finally, an operation on two tapes that swaps the current cell between |
| 262 | 262 | them. |
| 263 | 263 | |
| 264 | > swap t1 t2 = (set t1 (get t2), set t2 (get t1)) | |
| 264 | > swap t1 t2 = (set t1 (get t2), set t2 (get t1)) | |
| 265 | 265 | |
| 266 | 266 | A program state consists of: |
| 267 | 267 | |
| 268 | - A "data tape"; | |
| 269 | - A "stack tape"; and | |
| 270 | - A flag called the "halt flag", which may be 0 or 1. | |
| 268 | - A "data tape"; | |
| 269 | - A "stack tape"; and | |
| 270 | - A flag called the "halt flag", which may be 0 or 1. | |
| 271 | 271 | |
| 272 | 272 | The 0 and 1 are represented by False and True boolean values in this |
| 273 | 273 | semantics. |
| 274 | 274 | |
| 275 | > data State = State Tape Tape Bool | |
| 276 | > deriving (Show, Read, Eq) | |
| 277 | > | |
| 278 | > newstate = State (tape [0]) (tape [0]) True | |
| 275 | > data State = State Tape Tape Bool | |
| 276 | > deriving (Show, Read, Eq) | |
| 277 | > | |
| 278 | > newstate = State (tape [0]) (tape [0]) True | |
| 279 | 279 | |
| 280 | 280 | |
| 281 | 281 | Semantics of Burro Programs |
| 288 | 288 | If ab is a Burro program, and a maps state S to state S', and b maps |
| 289 | 289 | state S' to S'', then ab maps state S to state S''. |
| 290 | 290 | |
| 291 | > exec (Seq a b) t = exec b (exec a t) | |
| 291 | > exec (Seq a b) t = exec b (exec a t) | |
| 292 | 292 | |
| 293 | 293 | The e instruction is the identity function on states. |
| 294 | 294 | |
| 295 | > exec Null s = s | |
| 295 | > exec Null s = s | |
| 296 | 296 | |
| 297 | 297 | The ! instruction toggles the halt flag. If it is 0 in the input state, it |
| 298 | 298 | is 1 in the output state, and vice versa. |
| 299 | 299 | |
| 300 | > exec ToggleHalt (State dat stack halt) = (State dat stack (not halt)) | |
| 300 | > exec ToggleHalt (State dat stack halt) = (State dat stack (not halt)) | |
| 301 | 301 | |
| 302 | 302 | The + instruction increments the current data cell, while - decrements the |
| 303 | 303 | current data cell. |
| 304 | 304 | |
| 305 | > exec Inc (State dat stack halt) = (State (inc dat) stack halt) | |
| 306 | > exec Dec (State dat stack halt) = (State (dec dat) stack halt) | |
| 305 | > exec Inc (State dat stack halt) = (State (inc dat) stack halt) | |
| 306 | > exec Dec (State dat stack halt) = (State (dec dat) stack halt) | |
| 307 | 307 | |
| 308 | 308 | The instruction < makes the cell to the left of the current data cell, the |
| 309 | 309 | new current data cell. The instruction > makes the cell to the right of the |
| 310 | 310 | current data cell, the new current data cell. |
| 311 | 311 | |
| 312 | > exec GoLeft (State dat stack halt) = (State (left dat) stack halt) | |
| 313 | > exec GoRight (State dat stack halt) = (State (right dat) stack halt) | |
| 312 | > exec GoLeft (State dat stack halt) = (State (left dat) stack halt) | |
| 313 | > exec GoRight (State dat stack halt) = (State (right dat) stack halt) | |
| 314 | 314 | |
| 315 | 315 | (a/b) is the conditional construct, which is quite special. |
| 316 | 316 | |
| 333 | 333 | |
| 334 | 334 | Seventh, the current data cell and the current stack cell are swapped again. |
| 335 | 335 | |
| 336 | > exec (Test thn els) (State dat stack halt) = | |
| 337 | > let | |
| 338 | > x = get dat | |
| 339 | > (dat', stack') = swap dat stack | |
| 340 | > stack'' = right (set stack' (0 - (get stack'))) | |
| 341 | > f = if x > 0 then thn else if x < 0 then els else Null | |
| 342 | > (State dat''' stack''' halt') = exec f (State dat' stack'' halt) | |
| 343 | > (dat'''', stack'''') = swap dat''' (left stack''') | |
| 344 | > in | |
| 345 | > (State dat'''' stack'''' halt') | |
| 336 | > exec (Test thn els) (State dat stack halt) = | |
| 337 | > let | |
| 338 | > x = get dat | |
| 339 | > (dat', stack') = swap dat stack | |
| 340 | > stack'' = right (set stack' (0 - (get stack'))) | |
| 341 | > f = if x > 0 then thn else if x < 0 then els else Null | |
| 342 | > (State dat''' stack''' halt') = exec f (State dat' stack'' halt) | |
| 343 | > (dat'''', stack'''') = swap dat''' (left stack''') | |
| 344 | > in | |
| 345 | > (State dat'''' stack'''' halt') | |
| 346 | 346 | |
| 347 | 347 | We observe an invariant here: because only the (a/b) construct affects the |
| 348 | 348 | stack tape, and because it does so in a monotonic way — that is, both a |
| 364 | 364 | |
| 365 | 365 | Additionally, each time the program repeats, the stack tape is cleared. |
| 366 | 366 | |
| 367 | > run program state = | |
| 368 | > let | |
| 369 | > state'@(State dat' stack' halt') = exec program state | |
| 370 | > in | |
| 371 | > if | |
| 372 | > not halt' | |
| 373 | > then | |
| 374 | > run program (State dat' (tape [0]) True) | |
| 375 | > else | |
| 376 | > state' | |
| 367 | > run program state = | |
| 368 | > let | |
| 369 | > state'@(State dat' stack' halt') = exec program state | |
| 370 | > in | |
| 371 | > if | |
| 372 | > not halt' | |
| 373 | > then | |
| 374 | > run program (State dat' (tape [0]) True) | |
| 375 | > else | |
| 376 | > state' | |
| 377 | 377 | |
| 378 | 378 | |
| 379 | 379 | Central theorem of Burro |
| 494 | 494 | We define a few more convenience functions to cater for the execution |
| 495 | 495 | of Burro programs on an initial state. |
| 496 | 496 | |
| 497 | > interpret text = run (parse text) newstate | |
| 498 | ||
| 499 | > main = do | |
| 500 | > [fileName] <- getArgs | |
| 501 | > burroText <- readFile fileName | |
| 502 | > putStrLn $ show $ interpret burroText | |
| 497 | > interpret text = run (parse text) newstate | |
| 498 | ||
| 499 | > main = do | |
| 500 | > [fileName] <- getArgs | |
| 501 | > burroText <- readFile fileName | |
| 502 | > putStrLn $ show $ interpret burroText | |
| 503 | 503 | |
| 504 | 504 | Although we have proved that Burro programs form a group, it is not a |
| 505 | 505 | mechanized proof, and only goes so far in helping us tell if the |
| 516 | 516 | each one by applying the annihilationOf function to it and checking that |
| 517 | 517 | the result of executing it on a blank tape is equivalent to e. |
| 518 | 518 | |
| 519 | > testCases = [ | |
| 520 | > ("+++", "-++-++-++"), | |
| 521 | > ("+(>+++</---)", "->+++<"), | |
| 522 | > ("-(+++/>---<)", "+>---<"), | |
| 523 | > ("(!/!)", "e"), | |
| 524 | > ("+(--------!/e)", "+(/)+"), | |
| 525 | > ("+++(/)", "---"), | |
| 526 | > ("---(/)", "+++"), | |
| 527 | > ("+> +++ --(--(--(/>>>>>+)+/>>>+)+/>+)+", | |
| 528 | > "+> >>> +(---(/+)/)+") | |
| 529 | > ] | |
| 530 | ||
| 531 | > annihilationTests = [ | |
| 532 | > "e", "+", "-", "<", ">", "!", | |
| 533 | > "++", "--", "<+<-", "-->>--", | |
| 534 | > "(+/-)", "+(+/-)", "-(+/-)", | |
| 535 | > "+(--------!/e)" | |
| 536 | > ] | |
| 537 | ||
| 538 | > allTestCases = testCases ++ map nihil annihilationTests | |
| 539 | > where | |
| 540 | > nihil x = ((show (annihilationOf (parse x))), "e") | |
| 519 | > testCases = [ | |
| 520 | > ("+++", "-++-++-++"), | |
| 521 | > ("+(>+++</---)", "->+++<"), | |
| 522 | > ("-(+++/>---<)", "+>---<"), | |
| 523 | > ("(!/!)", "e"), | |
| 524 | > ("+(--------!/e)", "+(/)+"), | |
| 525 | > ("+++(/)", "---"), | |
| 526 | > ("---(/)", "+++"), | |
| 527 | > ("+> +++ --(--(--(/>>>>>+)+/>>>+)+/>+)+", | |
| 528 | > "+> >>> +(---(/+)/)+") | |
| 529 | > ] | |
| 530 | ||
| 531 | > annihilationTests = [ | |
| 532 | > "e", "+", "-", "<", ">", "!", | |
| 533 | > "++", "--", "<+<-", "-->>--", | |
| 534 | > "(+/-)", "+(+/-)", "-(+/-)", | |
| 535 | > "+(--------!/e)" | |
| 536 | > ] | |
| 537 | ||
| 538 | > allTestCases = testCases ++ map nihil annihilationTests | |
| 539 | > where | |
| 540 | > nihil x = ((show (annihilationOf (parse x))), "e") | |
| 541 | 541 | |
| 542 | 542 | Our unit test harness evaluates to a list of tests which did |
| 543 | 543 | not pass. If all went well, it will evaluate to the empty list. |
| 544 | 544 | |
| 545 | > test [] = | |
| 546 | > [] | |
| 547 | > test ((a, b):cases) = | |
| 548 | > let | |
| 549 | > resultA = interpret a | |
| 550 | > resultB = interpret b | |
| 551 | > in | |
| 552 | > if | |
| 553 | > resultA == resultB | |
| 554 | > then | |
| 555 | > test cases | |
| 556 | > else | |
| 557 | > ((a, b):(test cases)) | |
| 545 | > test [] = | |
| 546 | > [] | |
| 547 | > test ((a, b):cases) = | |
| 548 | > let | |
| 549 | > resultA = interpret a | |
| 550 | > resultB = interpret b | |
| 551 | > in | |
| 552 | > if | |
| 553 | > resultA == resultB | |
| 554 | > then | |
| 555 | > test cases | |
| 556 | > else | |
| 557 | > ((a, b):(test cases)) | |
| 558 | 558 | |
| 559 | 559 | Finally, some miscellaneous functions for helping analyze why the |
| 560 | 560 | Burro tests you've written aren't working :) |
| 561 | 561 | |
| 562 | > debug (a, b) = ((a, interpret a), (b, interpret b)) | |
| 563 | ||
| 564 | > debugTests = map debug (test allTestCases) | |
| 562 | > debug (a, b) = ((a, interpret a), (b, interpret b)) | |
| 563 | ||
| 564 | > debugTests = map debug (test allTestCases) | |
| 565 | 565 | |
| 566 | 566 | |
| 567 | 567 | Implementing a Turing Machine in Burro |