package object recs {

//Recursive Functions

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

  //syntactic convenience for composition
  def o(r: Rec) = Cn(r.arity, this, List(r))
  def o(r: Rec, f: Rec) = Cn(r.arity, this, List(r, f))
  def o(r: Rec, f: Rec, g: Rec) = Cn(r.arity, this, List(r, f, g))

  def arity : Int
}

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

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)
  }
  override def arity = 1 
} 

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)

  override def arity = n
}

case class Cn(n: Int, f: Rec, gs: List[Rec]) extends Rec {
  override def eval(ns: List[Int]) = 
    if (ns.length == n && gs.forall(_.arity == n) && f.arity == gs.length) f.eval(gs.map(_.eval(ns)))
    else { 
      val msg = List("Cn f: " + f, 
                     "n: " + n,
                     "f arity: " + f.arity, 
                     "ns-args: " + ns,
                     "gs arities: " + gs.map(_.arity).mkString("\n"),
                     "gs: " + gs.mkString(", ")
                    )
      throw new IllegalArgumentException(msg.mkString("\n"))
    }

  override def arity = n
  override def toString = f.toString + gs.map(_.toString).mkString ("(",", ", ")")
}

// syntactic convenience
object Cn {
  def apply(n: Int, f: Rec, g: Rec) : Rec = new Cn(n, f, List(g))
}

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 {
      val msg = List("Pr f: " + f, 
                     "g: " + g,
                     "n: " + n,
                     "f arity: " + f.arity,
                     "g arity: " + g.arity,
                     "ns-args: " + ns)
      throw new IllegalArgumentException(msg.mkString("\n"))
    }

  override def arity = n + 1
  override def toString = "Pr(" + f.toString + ", " + g.toString + ")"
}

// syntactic convenience
object Pr {
  def apply(r: Rec, f: Rec) : Rec = Pr(r.arity, r, f) 
}

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")

  override def arity = n
}



// Recursive Function examples
def Const(n: Int) : Rec = n match {
  case 0 => Z
  case n => S o Const(n - 1)
}

val Add = Pr(Id(1, 0), S o Id(3, 2))
val Mult = Pr(Z, Add o (Id(3, 0), Id(3, 2)))
val Twice = Mult o (Id(1, 0), Const(2))
val Fourtimes = Mult o (Id(1, 0), Const(4))
val Pred = Pr(Z, Id(3, 1)) o (Id(1, 0), Id(1, 0))
val Minus = Pr(Id(1, 0), Pred o Id(3, 2))
val Power = Pr(Const(1), Mult o (Id(3, 0), Id(3, 2)))
val Fact = Pr(Const(1), Mult o (Id(3, 2), S o Id(3, 1))) o (Id(1, 0), Id(1, 0))

val Sign = Minus o (Const(1), Minus o (Const(1), Id(1, 0)))
val Less = Sign o (Minus o (Id(2, 1), Id(2, 0)))
val Not = Minus o (Const(1), Id(1, 0))
val Eq = Minus o (Const(1) o Id(2, 0), 
                  Add o (Minus o (Id(2, 0), Id(2, 1)), 
                         Minus o (Id(2, 1), Id(2, 0))))
val Noteq = Not o (Eq o (Id(2, 0), Id(2, 1)))
val Conj = Sign o (Mult o (Id(2, 0), Id(2, 1)))
val Disj = Sign o (Add o (Id(2, 0), Id(2, 1)))
val Le = Disj o (Less, Eq)

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 = f.arity
  println("sigma f-ar: " + ar)
  Pr(Cn(ar - 1, f, Nargs(ar - 1, ar - 1) ::: List(Const(0) o Id(ar - 1, 0))), 
     Add o (Id(ar + 1, ar), 
            Cn(ar + 1, f, Nargs(ar + 1, ar - 1) ::: List(S o (Id(ar + 1, ar - 1))))))
}

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

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

def Ex(t: Rec, f: Rec) = {
  val ar = f.arity
  Sign o (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 = f.arity
  println("f-arity " + ar)
  println("Nargs " + Nargs(ar + 1, ar - 1) + " and " + List(Id(ar + 1, ar)))
  Sigma(All(Id(ar, ar - 1), Not o (Cn(ar + 1, f, Nargs(ar + 1, ar - 1) ::: List(Id(ar + 1, ar))))))
}

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


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

//Returns the first prime number after n (very slow for n > 4)
val NextPrime = {
  val R = Conj o (Less o (Id(2, 0), Id(2, 1)), Prime o Id(2, 1))
  Minr(R) o (Id(1, 0), S o Fact)
}

val NthPrime = Pr(Const(2), NextPrime o Id(3, 2)) o (Id(1, 0), Id(1, 0))

def Listsum(k: Int, m: Int) : Rec = m match {
  case 0 => Z o Id(k, 0)
  case n => Add o (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 => Z o Id(l, 0)
    case n => {
      val rec_dbound = Add o (Listsum(l, n - 1), Const(n - 1) o Id(l, 0))
      Add o (Strt_aux(l, n - 1), 
             Minus o (Power o (Const(2) o Id(l, 0), Add o (Id(l, n - 1), rec_dbound)), 
                      Power o (Const(2) o Id(l, 0), rec_dbound)))
    }
  }

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


//Mutli-way branching statement on page 79 of Boolos's book
def Branch(rs: List[(Rec, Rec)]) = {

  def Branch_aux(rs: List[(Rec, Rec)], l: Int) : Rec = rs match {
    case Nil => Z o Id(l, l - 1)
    case (rg, rc)::recs => Add o (Mult o (rg, rc), Branch_aux(recs, l))
  }

  Branch_aux(rs, rs.head._1.arity)
}

val Lg = {
 val lgR = Le o (Power o (Id(3, 1), Id(3, 2)), Id(3, 0))
 val conR1 = Conj o (Less o (Const(1) o (Id(2, 0), Id(2, 0))), 
                     Less o (Const(1) o (Id(2, 0), Id(2, 1))))
 val conR2 = Not o (conR1)
 Add o (Mult o (conR1, Maxr(lgR) o (Id(2, 0), Id(2, 1), Id(2, 0))), 
        Mult o (conR2, Const(0) o (Id(2, 0)))) 
}


}