Skip to content

Commit

Permalink
Makes stateMachine direction generic since we shouldn't actually be d…
Browse files Browse the repository at this point in the history
…oing anything

with it.
  • Loading branch information
ncik-roberts committed Jul 31, 2016
1 parent c17dc96 commit bc50aaa
Show file tree
Hide file tree
Showing 6 changed files with 31 additions and 28 deletions.
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
.cm/
18 changes: 10 additions & 8 deletions examples.sml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -33,32 +31,36 @@ 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

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,
Expand Down
12 changes: 5 additions & 7 deletions turingMachine/stateMachine/functionsm.sml
Original file line number Diff line number Diff line change
@@ -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,
Expand All @@ -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
Expand Down
16 changes: 8 additions & 8 deletions turingMachine/stateMachine/stateMachine.sig
Original file line number Diff line number Diff line change
Expand Up @@ -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
7 changes: 4 additions & 3 deletions turingMachine/turing.sig
Original file line number Diff line number Diff line change
Expand Up @@ -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
5 changes: 3 additions & 2 deletions turingMachine/turing.sml
Original file line number Diff line number Diff line change
@@ -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
Expand Down

0 comments on commit bc50aaa

Please sign in to comment.