(* A deterministic Turing machine *)
(* Author: Carsten Schuermann *)

signature TURING = 
  sig
    datatype State 
      = State of int
      
    datatype Letter
      = One
    | Zero
    | Blank
      
    datatype Move
      = Left
    | Right
      
    datatype Command
      = Command of (State * Letter) * (Letter * State * Move) option

    datatype Tape 
      = Tape of Letter list * Letter list

    datatype Program 
      = Program of Command list

    datatype Machine
      = Machine of Program * State * Tape

    val run : Machine -> Tape
  end

structure Turing : TURING =
  struct 
    datatype State 
      = State of int
      
    datatype Letter
      = One
    | Zero
    | Blank
      
    datatype Move
      = Left
    | Right
      
    datatype Command
      = Command of (State * Letter) * (Letter * State * Move) option

    datatype Tape 
      = Tape of Letter list * Letter list

    datatype Program 
      = Program of Command list

    datatype Machine
      = Machine of Program * State * Tape
 
    (* normalize (t) = t'
 
       Invariant: 
       t' = t where the next blank position on the tape is exposed 
       (if necessary) 
    *) 
    fun normalize (Tape ([], [])) = Tape ([Blank], [Blank])
      | normalize (Tape (r, [])) = Tape (r, [Blank])
      | normalize (Tape ([], l)) = Tape ([Blank], l)
      | normalize t = t
 
    (* some printing functions *)
    fun letterToString Zero = "0"
      | letterToString One = "1"
      | letterToString Blank = " "
      
    fun tapeToString n t =
          tapeToString' n (normalize t)
    and tapeToString' n (Tape (l, x :: r)) =
          tapeToStrings n (Tape (l, r)) (" >" ^ letterToString x ^ "< ")
    and tapeToStrings n t s = 
          tapeToStrings' n (normalize t) s
    and tapeToStrings' 0 (Tape (l, r)) s = s 
      | tapeToStrings' n (Tape (x :: l, y :: r)) s =
           tapeToStrings (n-1) (Tape (l, r)) 
	   ("  " ^ letterToString x ^ s ^ letterToString y ^ "  ") 

    fun blanks 0 s = " " ^ s
      | blanks n s = blanks (n-1) ("   " ^ s)

    fun machineToString n (Machine (p, State s, t)) = 
      (tapeToString n t ^ "\n" ^
       blanks n " ^\n" ^
       blanks n (" " ^ Int.toString s) ^ "\n\n")


    (* lookup (s, x) = (y, s', m) 

       Invariant: 
       If   s is a state of a Turing machine
       and  x is the letter on the tape
       then y is the letter to be written
       and  s' is the successor state of s
       and  m indcates if the read head moves to the left or to the right
    *)
    fun lookup (s, x) (Program cs) = lookup' (s, x) cs
    and lookup' (s, x) (Command ((s', x'), r) :: cs) =
          if (s = s') andalso (x = x') then r
          else lookup' (s, x) cs


    (* run (M) = t

       Invariant:  
       If   M is a Turing machine that consists of a program, a tape, and a state
       then t is the tape after the Turing machine comes to a halt.
    *)

    fun run (M as Machine (p, s, t)) =
      (print (machineToString 5 M); 
       run' (Machine (p, s, normalize t)))
    and run' (Machine (p, s, Tape (x :: l, y :: r))) =
      (case lookup (s, y) p
         of NONE => Tape (x :: l, y :: r)
          | SOME (z, s', m) =>
	      run (Machine (p, s', case m 
		                     of Left  => Tape (l, x :: z :: r)
	                              | Right => Tape (z :: x :: l, r))))

end


(* a Turing program to increment a binary number *)
local 
  open Turing

in

  val increment = Program 
    [Command ((State 1,  Zero), SOME ( Zero, State 1, Right)),
     Command ((State 1,   One), SOME (  One, State 1, Right)),
     Command ((State 1, Blank), SOME (Blank, State 2,  Left)),
     Command ((State 2,  Zero), SOME (  One, State 3,  Left)),
     Command ((State 2,   One), SOME ( Zero, State 2,  Left)),
     Command ((State 2, Blank), SOME (Blank, State 4, Right)),
     Command ((State 3,  Zero), SOME ( Zero, State 3,  Left)),
     Command ((State 3,   One), SOME (  One, State 3,  Left)),
     Command ((State 3, Blank), SOME (Blank, State 4, Right)),
     Command ((State 4,  Zero), NONE),
     Command ((State 4,   One), NONE),
     Command ((State 4, Blank), NONE)]
  

    
  val busybeaver = Program
    [Command ((State 1,   One), SOME (  One, State 3, Left)),
     Command ((State 1, Blank), SOME (  One, State 2, Right)),
     Command ((State 2,   One), SOME (  One, State 2, Right)),
     Command ((State 2, Blank), SOME (  One, State 1, Left)),
     Command ((State 3,   One), NONE),
     Command ((State 3, Blank), SOME (  One, State 2, Left))]
    
  (* some initial tapes *)
  val tape1 = Tape ([],[One,One,One,Zero]) : Tape
  val tape2 = Tape ([],[One,One,One,Zero,One,One,One,One]) : Tape
  val tape3 = Tape ([],[]) : Tape

  (* some Turing machines for testing *)
  val machine1 = Machine (increment, State 1, tape1)
  val machine2 = Machine (increment, State 1, tape2)
  val machine3 = Machine (busybeaver, State 1, tape3)


  val _ = run machine1
  val _ = run machine2
  val _ = run machine3
end