package object recs2 {

//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 o(r: Rec, f: Rec, g: Rec, h: Rec) = Cn(r.arity, this, List(r, f, g, h))
  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 {
  require(m < n, println("Id m < n:" + m + " " + n))

  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 {
  require(f.arity == gs.length, 
          println("CN " + f + "  " + gs.mkString(",") + "\n" + 
                  "f.arity gs.length:" + f.arity + " " + gs.length))
  
  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(", "),
                     "gs: " + gs.mkString(", "),
                     "ns.length == n " + (ns.length == n).toString,
                     "gs.forall(_.arity == n) " + (gs.forall(_.arity == n)).toString,
                     "f.arity == gs.length " + (f.arity == gs.length).toString
                    )
      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.head == 0) f.eval(ns.tail)
      else {
        val r = Pr(n, f, g).eval(ns.head - 1 :: ns.tail)
        g.eval(ns.head - 1 :: r :: ns.tail)
      }
    }
    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(n :: ns) == 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
}

object Mn {
  def apply(f: Rec) : Rec = Mn(f.arity - 1, f)
}




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

def Swap(f: Rec) = f o (Id(2, 1), Id(2, 0))
val Add = Pr(Id(1, 0), S o Id(3, 1))
val Mult = Pr(Z, Add o (Id(3, 1), Id(3, 2)))
val Power = Swap(Pr(Const(1), Mult o (Id(3, 1), Id(3, 2))))
val Fact = (Pr (Const(1), Mult o (S o Id(3, 0), Id(3, 1)))) o (Id(1, 0), Id(1, 0))
val Pred = Pr(Z, Id(3, 0)) o (Id(1, 0), Id(1, 0))
val Minus = Swap(Pr(Id(1, 0), Pred o Id(3, 1)))

val Sign = Minus o (Const(1), Minus o (Const(1), Id(1, 0)))
val Not = Minus o (Const(1), Id(1, 0))
val Eq = Minus o (Const(1) o Id(2, 0), Add o (Minus, Swap(Minus))) 
val Noteq = Not o Eq 
val Conj = Sign o Mult
val Disj = Sign o Add 
val Imp = Disj o (Not o Id(2, 0), Id(2, 1))
val Ifz = Pr(Id(2, 0), Id(4, 3))
val If = Ifz o (Not o Id(3, 0), Id(3, 1), Id (3, 2))

val Less = Sign o (Swap(Minus))
val Le = Disj o (Less, Eq)

def Sigma1(f: Rec) = Pr(f o (Z o (Id(1, 0)), Id(1, 0)), 
                        Add o (Id(3, 1), f o (S o Id(3, 0), Id(3, 2))))
def Sigma2(f: Rec) = Pr(f o (Z o (Id(2, 0)), Id(2, 0), Id(2, 1)), 
                        Add o (Id(4, 1), f o (S o Id(4, 0), Id(4, 2), Id(4, 3))))

def Accum1(f: Rec) = Pr(f o (Z o (Id(1, 0)), Id(1, 0)), 
                        Mult o (Id(3, 1), f o (S o Id(3, 0), Id(3, 2))))
def Accum2(f: Rec) = Pr(f o (Z o (Id(2, 0)), Id(2, 0), Id(2, 1)), 
                        Mult o (Id(4, 1), f o (S o Id(4, 0), Id(4, 2), Id(4, 3))))
def Accum3(f: Rec) = Pr(f o (Z o (Id(3, 0)), Id(3, 0), Id(3, 1), Id(3, 2)), 
                        Mult o (Id(5, 1), f o (S o Id(5, 0), Id(5, 2), Id(5, 3), Id(5, 4))))

def All1(f: Rec) = Sign o (Accum1(f))
def All2(f: Rec) = Sign o (Accum2(f))
def All3(f: Rec) = Sign o (Accum3(f))

def All1_less(f: Rec) = {
  val cond1 = Eq o (Id(3, 0), Id(3, 1))
  val cond2 = f o (Id(3, 0), Id(3, 2))
  All2(Disj o (cond1, cond2)) o (Id(2, 0), Id(2, 0), Id(2, 1))
}

def All2_less(f: Rec) = {
  val cond1 = Eq o (Id(4, 0), Id(4, 1))
  val cond2 = f o (Id(4, 0), Id(4, 2), Id(4, 3))
  All3(Disj o (cond1, cond2)) o (Id(3, 0), Id(3, 0), Id(3, 1), Id(3, 2))
}

def Ex1(f: Rec) = Sign o (Sigma1(f))
def Ex2(f: Rec) = Sign o (Sigma2(f))

val Quo = {
  val lhs = S o (Id(3, 0))
  val rhs = Mult o (Id(3, 2), S o (Id(3, 1)))
  val cond = Eq o (lhs, rhs)
  val if_stmt = If o (cond, S o (Id(3, 1)), Id(3, 1))
  Pr(Z, if_stmt)
}

def Iter(f: Rec) = Pr(Id(1, 0), f o (Id(3, 1)))

def Max1(f: Rec) = Pr(Z, Ifz o (f o (S o (Id(3, 0)), Id(3, 2)), S o (Id(3, 0)), Id(3, 1)))
def Max2(f: Rec) = Pr(Z, Ifz o (f o (S o (Id(4, 0)), Id(4, 2), Id(4, 3)), S o (Id(4, 0)), Id(4, 1)))
 
val Triangle = Quo o (Mult o (Id(1, 0), S), Const(2))

val MaxTriangle = {
  val cond = Not o (Le o (Triangle o (Id(2, 0)), Id(2, 1))) 
  Max1(cond) o (Id(1, 0), Id(1, 0))
}

val MaxTriangle2 = {
  Pred o Mn(Le o (Triangle o (Id(2, 0)), Id(2, 1)))
}

case object MaxTriangleFast extends Rec {
  def triangle(n: Int) : Int = (n * (n + 1)) / 2

  def search(m: Int, n: Int) : Int = {
    if (triangle(n) > m) n - 1 else search(m, n + 1)
  }

  override def eval(ns: List[Int]) = ns match {
    case n::Nil => search(n, 0)
    case _ => throw new IllegalArgumentException("MT args: " + ns)
  }

  override def arity = 1
}

case object TriangleFast extends Rec {
  def triangle(n: Int) : Int = (n * (n + 1)) / 2

  override def eval(ns: List[Int]) = ns match {
    case n::Nil => triangle(n)
    case _ => throw new IllegalArgumentException("Tr args: " + ns)
  }

  override def arity = 1
}

//(0 until 200).map(MaxTriangleFast.eval(_))


val Penc = Add o (TriangleFast o (Add o (Id(2, 0), Id(2, 1))), Id(2, 0))
val Pdec1 = Minus o (Id(1, 0), Triangle o (MaxTriangle o (Id(1, 0)))) 
val Pdec2 = Minus o (MaxTriangle o (Id(1, 0)), Pdec1 o (Id(1, 0))) 

def Lenc(fs: List[Rec]) : Rec = fs match {
  case Nil => Z
  case f::fs => Penc o (S o (f), Lenc(fs))
}

val Ldec = Pred o (Pdec1 o (Swap (Iter(Pdec2))))

val Within = Less o (Z o (Id(2, 0)), Swap (Iter(Pdec2)))
val Enclen = (Max1(Not o (Within o (Id(2, 1), Pred o (Id(2, 0)))))) o (Id(1, 0), Id(1, 0))
 

val Read = Ldec o (Id(1, 0), Const(0))
val Write = Penc o (S o (Id(2, 0)), Pdec2 o (Id(2, 1)))

val Newleft = {
  val cond0 = Eq o (Id(3, 2), Const(0))
  val cond1 = Eq o (Id(3, 2), Const(1))
  val cond2 = Eq o (Id(3, 2), Const(2))
  val cond3 = Eq o (Id(3, 2), Const(3))
  val case3 = Penc o (S o (Read o (Id(3, 1))), Id(3, 0)) 
  If o (cond0, 
        Id(3, 0),
        If o (cond1, 
              Id(3, 0),  
              If o (cond2, 
                    Pdec2 o (Id(3, 0)),
                    If o (cond3, case3, Id(3, 0)))))
}

val Newright = {
  val cond0 = Eq o (Id(3, 2), Const(0))
  val cond1 = Eq o (Id(3, 2), Const(1))
  val cond2 = Eq o (Id(3, 2), Const(2))
  val cond3 = Eq o (Id(3, 2), Const(3))
  val case2 = Penc o (S o (Read o (Id(3, 0))), Id(3, 1))
  If o (cond0, 
        Write o (Const(0), Id(3, 1)),
        If o (cond1, 
              Write o (Const(1), Id(3, 1)),  
              If o (cond2, 
                    case2,
                    If o (cond3, Pdec2 o (Id(3, 1)), Id(3, 0)))))
}

val Actn = Swap (Pr(Pdec1 o (Pdec1 o (Id(1, 0))), Pdec1 o (Pdec2 o (Id(3, 2)))))

val Action = {
  val cond1 = Noteq o (Id(3, 1), Z)
  val cond2 = Within o (Id(3, 0), Pred o (Id(3, 1)))
  val if_branch = Actn o (Ldec o (Id(3, 0), Pred o (Id(3, 1))), Id(3, 2))
  If o (Conj o (cond1, cond2), if_branch, Const(4))
}

val Newstat = Swap (Pr (Pdec2 o (Pdec1 o (Id(1, 0))),
                        Pdec2 o (Pdec2 o (Id(3, 2)))))

val Newstate = {
  val cond = Noteq o (Id(3, 1), Z)
  val if_branch = Newstat o (Ldec o (Id(3, 0), Pred o (Id(3, 1))), Id(3, 2))
  If o (cond, if_branch, Z)
}

val Conf = Lenc (List(Id(3, 0), Id(3, 1), Id(3, 2)))

val State = Ldec o (Id(1, 0), Z)

val Left = Ldec o (Id(1, 0), Const(1))

val Right = Ldec o (Id(1, 0), Const(2))

val Step = {
  val left = Left o (Id(2, 0))
  val right = Right o (Id(2, 0))
  val state = State o (Id(2, 0))
  val read = Read o (right)
  val action = Action o (Id(2, 1), state, read)
  val newstate = Newstate o (Id(2, 1), state, read)
  val newleft = Newleft o (left, right, action)
  val newright = Newright o (left, right, action) 
  Conf o (newstate, newleft, newright)
 } 

val Steps = Pr (Id(2, 0), Step o (Id(4, 1), Id(4, 3)))

val Stknum = Minus o (Sigma1(Ldec o (Id(2, 1), Id(2, 0))) o (Enclen o (Id(1, 0)), Id(1, 0)),
                      Ldec o (Id(1, 0), Enclen o (Id(1, 0))))

val Right_std = {
  val bound = Enclen o (Id(1, 0))
  val cond1 = Le o (Const(1) o (Id(2, 0)), Id(2, 0))
  val cond2 = All1_less (Eq o (Ldec o (Id(2, 1), Id(2, 0)), Const(1)))
  val bound2 = Minus o (Enclen o (Id(2, 1)), Id(2, 0))
  val cond3 = 
    (All2_less (Eq o (Ldec o (Id(3, 2), Add o (Id(3, 1), Id(3, 0))), Z))) o (bound2, Id(2, 0), Id(2, 1)) 
  Ex1(Conj o (Conj o (cond1, cond2), cond3)) o (bound, Id(1, 0))
}

val Left_std = {
  val cond = Eq o (Ldec o (Id(2, 1), Id(2, 0)), Z)
  (All1_less(cond)) o (Enclen o (Id(1, 0)), Id(1, 0))
}

val Std = Conj o (Left_std o (Left o (Id(1, 0))), Right_std o (Right o (Id(1, 0))))

val Final = Eq o (State o (Id(1, 0)), Z)

val Stop = {
  val stps = Steps o (Id(3, 2), Id(3, 1), Id(3, 0))
  Conj o (Final o (stps), Std o (stps))
}

val Halt = Mn (Not o (Stop o (Id(3, 1), Id(3, 2), Id(3, 0))))

val UF = Pred o (Stknum o (Right o (Steps o (Halt o (Id(2, 0), Id(2, 1)), Id(2, 1), Id(2, 0)))))

}