diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..bbe8fa9 --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +.cm/ diff --git a/examples.sml b/examples.sml index 4123e4d..fa28a4b 100644 --- a/examples.sml +++ b/examples.sml @@ -4,9 +4,7 @@ struct structure TM = Turing( structure T = BiinfiniteTape(open LRS) - structure SM = FunctionSM( - type direction = LRS.direction - type action = action)) + structure SM = FunctionSM(type action = action)) (* Have access to SM constructor and subroutine without an annoying prefix *) open TM.SM @@ -33,18 +31,21 @@ struct | qLeftOne (SOME One) = (SOME One, Left, SM qLeftOne) | qLeftOne (SOME Zero) = (SOME One, Left, SM qLeftZero) + val sLeftZero = SM qLeftZero + (* Let's separate every pair of ones *) fun qStart NONE = (NONE, Left, Halt Accept) | qStart (SOME Zero) = (SOME Zero, Right, SM qStart) | qStart (SOME One) = (SOME One, Right, SM qJustReadOne) and qJustReadOne NONE = (NONE, Left, Halt Accept) | qJustReadOne (SOME Zero) = (SOME Zero, Right, SM qStart) - | qJustReadOne (SOME One) = (SOME One, Left, SM (qDepair ())) - and qDepair () = + | qJustReadOne (SOME One) = let - fun onHalt _ x = (x, Stay, SM qStart) + (* Upon completion of subroutine, go back to initial state *) + val qDepair = subroutine sLeftZero (fn (_, x) => (x, Stay, SM qStart)) in - subroutine (SM qLeftZero) onHalt + (* Hand off control to subroutine *) + (SOME One, Left, SM qDepair) end end @@ -52,13 +53,14 @@ structure TM_Tester = struct open TM_Creator + (* Test on empty input tape *) val (Accept, [SOME Zero]) = TM.simulate (SM qRightZero) [] val tape = [One, One] val (Accept, [SOME Zero, SOME One, SOME One]) = TM.simulate (SM qRightZero) tape val (Accept, [SOME One, SOME One, SOME One]) = TM.simulate (SM qLeftOne) tape - (* Let's separate the ones in friends! *) + (* Separate all pairs of ones *) val depair = SM qStart val friends = [One, One, Zero, Zero, One, One, One] val result = [SOME One, SOME Zero, SOME One, SOME Zero, SOME Zero, SOME One, diff --git a/turingMachine/stateMachine/functionsm.sml b/turingMachine/stateMachine/functionsm.sml index 6c71f31..aba729c 100644 --- a/turingMachine/stateMachine/functionsm.sml +++ b/turingMachine/stateMachine/functionsm.sml @@ -1,17 +1,15 @@ functor FunctionSM (OPTIONS : sig type action - type direction end) : STATE_MACHINE = struct open OPTIONS - type direction = direction type 'a tapeSymbol = 'a option - datatype 'a sm = Halt of action - | SM of 'a state - withtype 'a state = 'a tapeSymbol -> ('a tapeSymbol * direction * 'a sm) + datatype ('a, 'b) sm = Halt of action + | SM of ('a, 'b) state + withtype ('a, 'b) move = 'a tapeSymbol * 'b * ('a, 'b) sm + and ('a, 'b) state = 'a tapeSymbol -> ('a, 'b) move - type 'a move = 'a tapeSymbol * direction * 'a sm exception Halted (* Strip away datatype constructor and return transition function, @@ -22,7 +20,7 @@ struct (* Allows us to make subroutines *) fun subroutine sm onHalt = let - fun subroutine' (Halt action) x = onHalt action x + fun subroutine' (Halt action) x = onHalt (action, x) | subroutine' (SM q) x = case q x of (sym, dir, act) => (sym, dir, SM (subroutine' act)) in diff --git a/turingMachine/stateMachine/stateMachine.sig b/turingMachine/stateMachine/stateMachine.sig index b5c883d..d25309e 100644 --- a/turingMachine/stateMachine/stateMachine.sig +++ b/turingMachine/stateMachine/stateMachine.sig @@ -2,21 +2,21 @@ signature STATE_MACHINE = sig (* What to do when the TM has halted *) type action - (* Direction of the head to move. *) - type direction - - type 'a state type 'a tapeSymbol - datatype 'a sm = Halt of action | SM of 'a state - type 'a move = 'a tapeSymbol * direction * 'a sm + + (* Alpha represents the tape symbol, beta represents the direction *) + type ('a, 'b) state + datatype ('a, 'b) sm = Halt of action | SM of ('a, 'b) state + type ('a, 'b) move = 'a tapeSymbol * 'b * ('a, 'b) sm (* Exception raised when nextMove is called on a halted sm *) exception Halted (* Determine the next move (incl. symbol to write, direction of tape head, and * next state) based on current configuration *) - val nextMove : 'a sm -> 'a tapeSymbol -> 'a move + val nextMove : ('a, 'b) sm -> 'a tapeSymbol -> ('a, 'b) move (* Make subroutines *) - val subroutine : 'a sm -> (action -> 'a tapeSymbol -> 'a move) -> 'a tapeSymbol -> 'a move + val subroutine : ('a, 'b) sm -> (action * 'a tapeSymbol -> ('a, 'b) move) + -> 'a tapeSymbol -> ('a, 'b) move end diff --git a/turingMachine/turing.sig b/turingMachine/turing.sig index e7fc885..90439cc 100644 --- a/turingMachine/turing.sig +++ b/turingMachine/turing.sig @@ -3,11 +3,12 @@ sig structure T : TAPE structure SM : STATE_MACHINE where type 'a tapeSymbol = 'a T.tapeSymbol - sharing type T.direction = SM.direction + + type 'a sm = ('a, T.direction) SM.sm (* Simulate a single step on the turing machine *) - val step : 'a SM.sm -> 'a T.tape -> 'a SM.sm * 'a T.tape + val step : 'a sm -> 'a T.tape -> 'a sm * 'a T.tape (* Simulate the turing machine until it halts. *) - val simulate : 'a SM.sm -> 'a list -> SM.action * 'a T.tapeSymbol list + val simulate : 'a sm -> 'a list -> SM.action * 'a T.tapeSymbol list end diff --git a/turingMachine/turing.sml b/turingMachine/turing.sml index c5dffef..5fb439c 100644 --- a/turingMachine/turing.sml +++ b/turingMachine/turing.sml @@ -1,12 +1,13 @@ functor Turing ( structure T : TAPE structure SM : STATE_MACHINE - where type 'a tapeSymbol = 'a T.tapeSymbol - sharing type T.direction = SM.direction) : TURING_MACHINE = + where type 'a tapeSymbol = 'a T.tapeSymbol) : TURING_MACHINE = struct structure T = T structure SM = SM + type 'a sm = ('a, T.direction) SM.sm + (* Simulate 1 step on the stateMachine and tape *) fun step stateMachine tape = let