import lib._
import turing._
import abacus._
import recs._
import comp1._
//import comp2._

// Turing machine examples
val TMCopy = TM((WBk, 5), (R, 2), (R, 3), (R, 2), (WOc, 3), 
                (L, 4), (L, 4), (L, 5), (R, 11), (R, 6), 
                (R, 7), (WBk, 6), (R, 7), (R, 8), (WOc, 9), 
                (R, 8), (L, 10), (L, 9), (L, 10), (L, 5), 
                (L, 0), (R, 12), (WOc, 13), (L, 14), (R, 12), 
                (R, 12), (L, 15), (WBk, 14), (R, 0), (L, 15))

println("TMCopy:    " + (TMCopy.run(Tape(3))))
println("TMfindnth: " + (TMFindnth(3).run(Tape(1,2,3,4,5))))
println("TMMopup:   " + (TMMopup(3).run(Tape(1,2,3,4,5))))


// Abacus machine examples
def Copy(in: Int, out: Int, jump: Int) = 
  Abacus(List(Dec(in, jump), Inc(out), Goto(0))) 

def Plus(m: Int, n: Int, tmp: Int, jump: Int) =
  Abacus(List(Dec(m, 4), Inc(n), Inc(tmp), Goto(0), Dec(tmp, jump), Inc(m), Goto(4)))

def Mult(in1: Int, in2: Int, out: Int, tmp: Int, jump: Int) = 
  Abacus(List(Dec(in1, jump))) ++ Plus(in2, out, tmp, -1).shift(1, -1).adjust(-1, 0)

def Expo(in1: Int, in2: Int, out: Int, tmp1: Int, tmp2: Int, jump: Int) = {
  Abacus(List(Inc(out), Dec(in1, jump))) ++ 
  Mult(out, in2, tmp2, tmp1, -1).shift(2, -1).adjust(-1, 10) ++
  Copy(tmp2, out, -1).shift(10, -1). adjust(-1, 1)
}

println("Copy 3:     " + (Copy(0, 1, -1).run(Map(0 -> 3, 1 -> 0))))
println("Plus 3 + 4: " + (Plus(0, 1, 2, -1).run(Map(0 -> 3, 1 -> 4, 2 -> 0))))
println("Mult 3 * 5: " + (Mult(0, 1, 2, 3, -1).run(Map(0 -> 3, 1 -> 5, 2 -> 0, 3 -> 0))))
println("Expo 3 ^ 4: " + (Expo(0, 1, 2, 3, 4, -1).run(Map(0 -> 4, 1 -> 3, 2 -> 0, 3 -> 0, 4 -> 0))))


// Abacus-to-TM translation examples
println("Compiled Copy 3:     " + toTM(Copy(0, 1, Int.MaxValue).p).run(Tape(3,0,0)))
println("Compiled Plus 3 + 4: " + toTM(Plus(0, 1, 2, Int.MaxValue).p).run(Tape(3,4,0,0)))
println("Compiled Mult 3 * 5: " + toTM(Mult(0, 1, 2, 3, Int.MaxValue).p).run(Tape(3,5,0,0)))
println("Compiled Expo 3 ^ 4: " + toTM(Expo(0, 1, 2, 3, 4, 10000).p).run(Tape(3,4,0,0,0)))

// Recursive Function examples
def arity(f: Rec) = f match {
  case Z => 1
  case S => 1
  case Id(n, _) => n
  case Cn(n, _, _) => n
  case Pr(n, _, _) => n + 1
  case Mn(n, _) => n 
}

val Add = Pr(1, Id(1, 0), Cn(3, S, List(Id(3, 2))))
val Mult = Pr(1, Z, Cn(3, Add, List(Id(3, 0), Id(3, 2))))
val Pred = Cn(1, Pr(1, Z, Id(3, 1)), List(Id(1, 0), Id(1, 0)))
val Minus = Pr(1, Id(1, 0), Cn(3, Pred, List(Id(3, 2))))

def Const(n: Int) : Rec = n match {
  case 0 => Z
  case n => Cn(1, S, List(Const(n - 1)))
}

val Sign = Cn(1, Minus, List(Const(1), Cn(1, Minus, List(Const(1), Id(1, 0)))))
val Less = Cn(2, Sign, List(Cn(2, Minus, List(Id(2, 1), Id(2, 0)))))
val Not = Cn(1, Minus, List(Const(1), Id(1, 0)))
val Eq = Cn(2, Minus, List(Cn(2, Const(1), List(Id(2, 0))), 
           Cn(2, Add, List(Cn(2, Minus, List(Id(2, 0), Id(2, 1))), 
             Cn(2, Minus, List(Id(2, 1), Id(2, 0)))))))
val Conj = Cn(2, Sign, List(Cn(2, Mult, List(Id(2, 0), Id(2, 1)))))
val Disj = Cn(2, Sign, List(Cn(2, Add, List(Id(2, 0), Id(2, 1)))))

def Nargs(n: Int, m: Int) : List[Rec] = m match {
  case 0 => Nil
  case m => Nargs(n, m - 1) ::: List(Id(n, m - 1))
}

def Sigma(f: Rec) = {
  val ar = arity(f)  
  Pr(ar - 1, Cn(ar - 1, f, Nargs(ar - 1, ar - 1) :::
                    List(Cn(ar - 1, Const(0), List(Id(ar - 1, 0))))), 
             Cn(ar + 1, Add, List(Id(ar + 1, ar), 
                    Cn(ar + 1, f, Nargs(ar + 1, ar - 1) :::
                        List(Cn(ar + 1, S, List(Id(ar + 1, ar - 1))))))))
}

println("Add 3 4:   " + Add.eval(List(3, 4)))
println("Mult 3 4:  " + Mult.eval(List(3, 4)))
println("Pred 9:    " + Pred.eval(List(9)))
println("Pred 0:    " + Pred.eval(List(0)))
println("Minus 6 2: " + Minus.eval(List(6, 2)))
println("Minus 6 8: " + Minus.eval(List(6, 8)))
println("Const 8:   " + Const(8).eval(List(67)))
println("Sign 8:    " + Sign.eval(List(8)))
println("Sign 0:    " + Sign.eval(List(0)))
println("Less 4 4:  " + Less.eval(List(4, 4)))
println("Less 4 6:  " + Less.eval(List(4, 6)))
println("Less 6 4:  " + Less.eval(List(6, 4)))
println("Not 0:     " + Not.eval(List(0)))
println("Not 6:     " + Not.eval(List(6)))
println("Eq 4 4:    " + Eq.eval(List(4, 4)))
println("Eq 4 6:    " + Eq.eval(List(4, 6)))
println("Eq 6 4:    " + Eq.eval(List(6, 4)))
println("Conj 0 6:  " + Conj.eval(List(0, 6)))
println("Conj 6 4:  " + Conj.eval(List(6, 4)))
println("Conj 0 0:  " + Conj.eval(List(0, 0)))
println("Disj 0 6:  " + Disj.eval(List(0, 6)))
println("Disj 6 4:  " + Disj.eval(List(6, 4)))
println("Disj 0 0:  " + Disj.eval(List(0, 0)))
//println("Sigma:     " + Sigma(S).eval(List(0,1,2)))
//println("Sigma:     " + Sigma(S).eval(List(0,1,2,3,4,5)))


val ABCZero = Abacus(List(Goto(1)))
val ABCSucc = Plus(0, 1, 2, 7) ++ Abacus(List(Inc(1))).shift(Plus(0, 1, 2, 7).p.length, -1)
def ABCId(n: Int, m: Int) = Plus(m, n, n + 1, 7)