package object recs {

//Recursive Functions

abstract class Rec {
  def eval(ns: List[Int]) : Int
  def eval(ns: Int*) : Int = eval(ns.toList)
}

case object Z extends Rec {
  override def eval(ns: List[Int]) = ns match {
    case n::Nil => 0
    case _ => throw new IllegalArgumentException("Z args: " + ns)
  }
} 

case object S extends Rec {
  override def eval(ns: List[Int]) = ns match {
    case n::Nil => n + 1
    case _ => throw new IllegalArgumentException("S args: " + ns)
  }
} 

case class Id(n: Int, m: Int) extends Rec {
  override def eval(ns: List[Int]) = 
    if (ns.length == n && m < n) ns(m)
    else throw new IllegalArgumentException("Id args: " + ns + "," + n + "," + m)
}

case class Cn(n: Int, f: Rec, gs: List[Rec]) extends Rec {
  override def eval(ns: List[Int]) = 
    if (ns.length == n) f.eval(gs.map(_.eval(ns)))
    else throw new IllegalArgumentException("Cn: args")
}

case class Pr(n: Int, f: Rec, g: Rec) extends Rec {
  override def eval(ns: List[Int]) = 
    if (ns.length == n + 1) {
      if (ns.last == 0) f.eval(ns.init)
      else {
        val r = Pr(n, f, g).eval(ns.init ::: List(ns.last - 1))
        g.eval(ns.init ::: List(ns.last - 1, r))
      }
    }
    else throw new IllegalArgumentException("Pr: args")
}

case class Mn(n: Int, f: Rec) extends Rec {
  def evaln(ns: List[Int], n: Int) : Int = 
    if (f.eval(ns ::: List(n)) == 0) n else evaln(ns, n + 1)

  override def eval(ns: List[Int]) = 
    if (ns.length == n) evaln(ns, 0) 
    else throw new IllegalArgumentException("Mn: args")
}



// 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 Twice = Cn(1, Mult, List(Id(1, 0), Const(2)))
val Fourtimes = Cn(1, Mult, List(Id(1, 0), Const(4)))
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 Power = Pr(1, Const(1), Cn(3, Mult, List(Id(3, 0), Id(3, 2))))
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 Noteq = Cn(2, Not, List(Cn(2, Eq, List(Id(2, 0), Id(2, 1))))) 
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))))))))
}

def Accum(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, Mult, 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))))))))
}

def All(t: Rec, f: Rec) = {
  val ar = arity(f)
  Cn(ar - 1, Sign, List(Cn(ar - 1, Accum(f), Nargs(ar - 1, ar - 1) ::: List(t))))
}

def Ex(t: Rec, f: Rec) = {
  val ar = arity(f)
  Cn(ar - 1, Sign, List(Cn(ar - 1, Sigma(f), Nargs(ar - 1, ar - 1) ::: List(t))))
}

//Definition on page 77 of Boolos's book.
def Minr(f: Rec) = {
  val ar = arity(f)
  val rq = All(Id(ar, ar - 1), 
    Cn(ar + 1, Not, List(Cn(ar + 1, f, Nargs(ar + 1, ar - 1) ::: List(Id(ar + 1, ar)))))) 
  Sigma(rq)
}

//Definition on page 77 of Boolos's book.
def Maxr(f: Rec) = {
  val ar  = arity(f) 
  val rt  = Id(ar + 1, ar - 1) 
  val rf1 = Cn(ar + 2, Less, List(Id(ar + 2, ar + 1), Id(ar + 2, ar))) 
  val rf2 = Cn(ar + 2, Not, List(Cn (ar + 2, f, Nargs(ar + 2, ar - 1) ::: List(Id(ar + 2, ar + 1))))) 
  val rf  = Cn(ar + 2, Disj, List(rf1, rf2)) 
  val rq  = All(rt, rf) 
  val Qf  = Cn(ar + 1, Not, List(rq))
  Cn(ar, Sigma(Qf), Nargs(ar, ar) ::: List(Id(ar, ar - 1)))
}

//Mutli-way branching statement on page 79 of Boolos's book
def Branch(rs: List[(Rec, Rec)]) = {
  val ar = arity(rs.head._1)
  
  def Branch_aux(rs: List[(Rec, Rec)], l: Int) : Rec = rs match {
    case Nil => Cn(l, Z, List(Id(l, l - 1)))
    case (rg, rc)::recs => Cn(l, Add, List(Cn(l, Mult, List(rg, rc)), Branch_aux(recs, l)))
  }

  Branch_aux(rs, ar)
}

//Factorial
val Fact = {
  val Fact_aux = Pr(1, Const(1), Cn(3, Mult, List(Id(3, 2), Cn(3, S, List(Id(3, 1))))))
  Cn(1, Fact_aux, List(Id(1, 0), Id(1, 0)))
}

//Prime test
val Prime = Cn(1, Conj, List(Cn(1, Less, List(Const(1), Id(1, 0))),
                             All(Cn(1, Minus, List(Id(1, 0), Const(1))), 
                                 All(Cn(2, Minus, List(Id(2, 0), Cn(2, Const(1), List(Id(2, 0))))), 
                                     Cn(3, Noteq, List(Cn(3, Mult, List(Id(3, 1), Id(3, 2))), Id(3, 0)))))))

//Returns the first prime number after n
val NextPrime = {
  val R = Cn(2, Conj, List(Cn(2, Less, List(Id(2, 0), Id(2, 1))), 
                           Cn(2, Prime, List(Id(2, 1)))))
  Cn(1, Minr(R), List(Id(1, 0), Cn(1, S, List(Fact))))
}

val NthPrime = {
  val NthPrime_aux = Pr(1, Const(2), Cn(3, NextPrime, List(Id(3, 2))))
  Cn(1, NthPrime_aux, List(Id(1, 0), Id(1, 0)))
}

def Listsum(k: Int, m: Int) : Rec = m match {
  case 0 => Cn(k, Z, List(Id(k, 0)))
  case n => Cn(k, Add, List(Listsum(k, n - 1), Id(k, n - 1)))
}

//strt-function on page 90 of Boolos, but our definition generalises 
//the original one in order to deal with multiple input-arguments

def Strt(n: Int) = {
  def Strt_aux(l: Int, k: Int) : Rec = k match {
    case 0 => Cn(l, Z, List(Id(l, 0)))
    case n => {
      val rec_dbound = Cn(l, Add, List(Listsum(l, n - 1), Cn(l, Const(n - 1), List(Id(l, 0)))))
      Cn(l, Add, List(Strt_aux(l, n - 1), 
                      Cn(l, Minus, List(Cn(l, Power, List(Cn(l, Const(2), List(Id(l, 0))), 
                                                          Cn(l, Add, List(Id(l, n - 1), rec_dbound)))), 
                                        Cn(l, Power, List(Cn(l, Const(2), List(Id(l, 0))), rec_dbound))))))
    }
  }

  def Rmap(f: Rec, k: Int) = (0 until k).map{i => Cn(k, f, List(Id(k, i)))}.toList
 
  Cn(n, Strt_aux(n, n), Rmap(S, n))
}

}