BeginPackage["CSM`TuringRecursive`", {"CSM`Turing`", "CSM`TuringMacros`"}]

zero::usage = "zero is the TM program for zero."
plus1::usage = "plus1 is the TM program for the successor."
p::usage = "p[k, n] is the TM program for the projection p^n_k."
comp::usage = "comp[n, f, {g1, ..., gp}] is the TM program for composition."
pr::usage = "pr[n, f, g] is the TM program for primitive recursion."
args::usage = "args[n1, n2, ...] gives the initial tape for arguments n1, n2, ..."

Begin["`Private`"]

zero = noop

plus1 =
compose[
  skip[1],
  {instruction[1, b, m, r, 0]}, (* write 1 *)
  skip[-1]
]

(* projections, kth argument of n *)

p[k_, n_] :=
    compose[
      compose @@ Table[eat1[j], {j, n, n-k+2, -1}],
      If[ k < n,
	  compose[
	      skip[1],
	      compose @@ Table[eat1[j], {j, n-k, 1, -1}],
	      skip[-1] ],
	  noop
      ]
    ]

(* composition of p functions of n arguments
   f[ g1[...], ..., gp[...] ] *)

comp[ n_, f_, gs_List ] :=
    With[{p = Length[gs]},
      compose[
        compose @@ Table[
        	compose[
        	    copy[n, n+i-1], (* copy arguments *)
        	    gs[[i]],        (* execute g_i *)
        	    skip[-(n+i-1)]  (* back to the beginning *)
        	], {i, 1, p} ],
        compose @@ Table[eat1[i+p], {i, n, 1, -1}],
        f
      ]
    ]

(* subtract 1, for numbers > 0, with n arguments following *)

sub1[n_] :=
compose[
  right,
  {instruction[1, m, b, s, 0]},
  shiftleft[n+1]
]

(* primitive recursion h(k, m1,...,mn) *)

pr[n_, f_, g_] :=
compose[            (*:k m1...mn                   *)
  skip[n+1],        (* k m1...mn:                  *)
  zero,             (* k m1...mn:0                 *)
  skip[-n],         (* k:m1...mn 0                 *)
  copy[n, n+1],     (* k m1...mn 0:m1...mn         *)
  f,                (* k m1...mn 0:h0              *)
  skip[-(n+2)],     (*:k m1...mn 0 h0              *)
  right,            (* k m1...mn 0 h0              *)
  while[ (* k > 0 *)
    compose[
      left,         (*:k' m1...mn:i hi             *)
      sub1[n+2],    (*:k m1...mn i hi              *)
      skip[n+1],    (* k m1...mn:i hi              *)
      copy[2, 2],   (* k m1...mn i hi:i hi         *)
      skip[-(n+2)], (* k:m1...mn i hi i hi         *)
      copy[n, n+4], (* k m1...mn i hi i hi:m1...mn *)
      skip[-2],     (* k m1...mn i hi:i hi m1...mn *)
      g,            (* k m1...mn i hi:hi'          *)
      skip[-2],     (* k m1...mn:i hi hi'          *)
      copy[1, 3],   (* k m1...mn i hi hi':i        *)
      plus1,        (* k m1...mn i hi hi':i'       *)
      skip[-1],     (* k m1...mn i hi:hi' i'       *)
      copy[1, 2],   (* k m1...mn i hi hi' i':hi'   *)
      skip[-4],     (* k m1...mn:i hi hi' i' hi'   *)
      eat1[5],      (* k m1...mn:hi hi' i' hi'     *)
      eat1[4],      (* k m1...mn:hi' i' hi'        *)
      eat1[3],      (* k m1...mn:i' hi'            *)
      skip[-(n+1)], (*:k m1...mn i' hi'            *)
      right         (* k m1...mn i' hi'            *)
    ]
  ],
  left,             (*:0 m1...mn k hk              *)
  p[n+3, n+3]       (*:hk                          *)
]

unary[n_] := Prepend[Table[m, {n}], b]

args[n___] := Join @@ unary /@ {n}

End[]

Protect[ zero, plus1, p, comp, pr, args ]

EndPackage[]
