package WithVariance

/**
  * Here we demonstrate embeddings using covariance.
  */
trait Consts {
  // A very simple expression language, figuring only arbitrary literals:
  trait Exp[+T]
  case class Const[T](t: T) extends Exp[T]
  // The above encodes the Haskell ADT:
  //
  //   data Exp t = Const t
  //
  // But note that this encoding is extensible.

  //A simple evaluator. We will show it is not type-correct. (It only compiles because of an unsoundness bug,
  //https://issues.scala-lang.org/browse/SI-6944).
  def eval[T](term: Exp[T]): T =
    term match {
      case Const(t) => t
    }

  //The simplest term transformation for this language. This is also not type-correct.
  def rebuild[T](term: Exp[T]): Exp[T] =
    term match {
      case Const(t) => Const(t)
    }
}

trait LambdaSub extends Consts {
  // Extend this language declared in Const to the simply-typed lambda calculus with subtyping (also known as lambda-sub
  // or $\lambda_<:$):

  /*trait Exp[+T]
  case class Const[T](t: T) extends Exp[T]*/
  case class App[S, T](fun: Exp[S => T], arg: Exp[S]) extends Exp[T]

  //Instead of representing variables explicitly, we reuse the binding support of Scala through higher-order abstract
  //syntax.

  case class Fun[S, T](body: Exp[S] => Exp[T]) extends Exp[S => T]

  //The extensions of the interpreter and term transformation come right after.
}

// An interpreter for this calculus. Note that we needed to use casts to write it.
trait Interp extends LambdaSub {
  override def eval[T](term: Exp[T]): T =
    term match {
      case App(fun, arg) =>
        eval(fun) apply eval(arg)
      case f: Fun[s, t] =>
        //(x: s) => eval(f.body(Const(x)))
        (((x: s) => eval(f.body(Const(x)))): (s => t)).asInstanceOf[T]
      //case Fun(body) =>
        //x => eval(body(Const(x)))
      case _ => super.eval(term)
    }

  override def rebuild[T](term: Exp[T]): Exp[T] =
    term match {
      case App(fun, arg) => App(fun, arg)

      // What we would like to write:
      //
      //   case Fun(body) => Fun(f.body)
      //
      // What we have to write instead:
      //
      case f: Fun[s, t] =>
        Fun(f.body).asInstanceOf[Exp[T]]
      case _ => super.rebuild(term)
    }
}

// Define a few valid terms in our lambda calculus
trait LamExamples extends LambdaSub {
  val term1 = App(Fun((x: Exp[Int]) => x), Const(1))

  //Use the host language to define some syntactic sugar
  def let[S, T](arg: Exp[S])(f: Exp[S => T]) = App(f, arg)

  //Using let, we need less type annotations:
  val term2 = let(Const(1))(Fun(x => x))

  //val termWrong = Fun((x: Exp[Int]) => App(x, 1))
}

// Extends the language to include lists
trait Lists extends LambdaSub with Interp {
  case class Cons[T](car: Exp[T], cdr: Exp[List[T]]) extends Exp[List[T]]
  case class Null[T]() extends Exp[List[T]]
  case class Car[T](l: Exp[List[T]]) extends Exp[T]
  case class Cdr[T](l: Exp[List[T]]) extends Exp[List[T]]

  override def eval[T](term: Exp[T]): T =
    term match {
      //case Cons(car, cdr) =>
        //eval(car) :: eval(cdr)
      case cons: Cons[t] => //T <: List[t]
        ((eval(cons.car) :: eval(cons.cdr)) : List[t]).asInstanceOf[T]
      //case Null() =>
        //List()
      case nil: Null[t] =>
        (List(): List[t]).asInstanceOf[T]
      case Car(l) =>
        eval(l).head
      //case Cdr(l) =>
        //eval(l).tail
      case cdr: Cdr[t] =>
        (eval(cdr.l).tail: List[t]).asInstanceOf[T]
      case _ =>
        super.eval(term)
    }
}

// Extend the language for addition on Ints:
trait Nums extends LambdaSub with Interp {
  case class Plus(a: Exp[Int], b: Exp[Int]) extends Exp[Int]

  override def eval[T](term: Exp[T]): T =
    term match {
      case p @ Plus(a, b) =>
        ((eval(a) + eval(b)): Int).asInstanceOf[T]
      case _ =>
        super.eval(term)
    }
}

// Extend the language for addition on instances of the Numeric "type-class":
trait NumsGen extends LambdaSub with Interp {
  case class Plus[T](a: Exp[T], b: Exp[T])(implicit val num: Numeric[T]) extends Exp[T]
  override def eval[T](term: Exp[T]): T =
    term match {
      //case p @ Plus(a, b) =>
        //p.num.plus(eval(a), eval(b)) //works with Scala 2.9.2, doesn't with 2.10.x
      case p: Plus[t] =>
        (p.num.plus(eval(p.a), eval(p.b)): t).asInstanceOf[T]
      case _ =>
        super.eval(term)
    }
}

// Code transformation to reduce a beta-redex (note that this does not traverse the term *looking* for beta-redexes, for simplicity):
trait BetaReduce extends LambdaSub {
  def betaReduce[T](term: Exp[T]): Exp[T] =
    term match {
      case App(Fun(f), arg) => f(arg)
      case e => e
    }
}

// Extend the language with the map operation on generic Scala collections:
trait Colls extends LambdaSub with Interp {
  case class MapOp[T, U](coll: Exp[Traversable[T]], f: Exp[T => U]) extends Exp[Traversable[U]]
  override def eval[T](term: Exp[T]): T =
    term match {
      case MapOp(coll, f) =>
        ((eval(coll) map eval(f)): Traversable[Any]).asInstanceOf[T]
      case _ =>
        super.eval(term)
    }
}

// Attempts at implementing map fusion.

trait Fusion extends LambdaSub with Colls {
  def fusePrecise[T](t: Exp[T]): Exp[T] =
    t match {
      // First attempt to write map fusion, rejected by the type-checker:

      /*
       case MapOp(m: MapOp[a, b], g) =>
        m match {

          case MapOp(coll, f) =>
            MapOp(coll, Fun((x: Exp[a]) => App(g, App(f, x))))

          //Doesn't help.
          //case MapOp(coll: Exp[Traversable[`a`]], f) =>
            //MapOp(coll, Fun((x: Exp[a]) => App(g, App(f, x))))
          case _ => t
        }
       */

      // Let's try again. Since type inference for nested patterns is unreliable in Scala, let's try using typed pattern
      // matches and binding the existential type variable, for use in type annotations:
      case m1: MapOp[t, u] =>
        m1.coll match { //Exp[Traversable[t]]
          case m2: MapOp[s, `t`] =>
            ((MapOp(m2.coll, Fun((x: Exp[s]) => App(m1.f, App(m2.f, x))))): MapOp[s, u])
              //We still need this cast:
              .asInstanceOf[Exp[T]]
          case _ => m1
        }
      case _ => t
    }
}

// Example programs using map.
trait CollsExamples extends Colls with NumsGen with LambdaSub with Fusion{
  val plus1: Exp[Int => Int] = Fun((x: Exp[Int]) => Plus(x, Const(1)))
  val id: Exp[Any => Any] = Fun(x => x)
  val res1 = MapOp(MapOp(Const(List(1, 2, 3)), plus1), plus1)
}

object Language extends LambdaSub with Lists with NumsGen with BetaReduce
    with LamExamples {

  //Demonstrate why all branches of the lambda-calculus interpreter can trigger an error, by defining appropriate exotic terms.
  class UnsoundFun[T]() extends Fun[T, T](x => x) with Exp[runtime.AbstractFunction1[T, T]]
  class UnsoundApp[T](t: T) extends App[Int, List[T]](Fun(x => Const(List(t))), Const(1)) with Exp[Nil.type]
  class UnsoundConst(t: String) extends Const[Any](t) with Exp[Boolean]

  // Lambda-calculus terms are not special. We can get the same for instance for Cons:
  class UnsoundConsNil[T](t: Exp[T]) extends Cons[T](t, Null()) with Exp[Nil.type]
}

object TriggerUnsoundness {
  import Language._

  // Call these methods to see the relevant type errors:

  def unsound1 = eval(new UnsoundConst(""))
  def unsound2 = eval(new UnsoundApp(1))
  def unsound3 = eval(let(Const(1))(new UnsoundFun()))
  def unsound4 = eval(new UnsoundConsNil(Const(1)))

  //println(unsound1) //This works thanks to heap pollution
  //println(unsound2) //Ditto

  /*Executing 'eval(new MyApp(1))' in the REPL won't work -
    |you'll get a ClassCastException""".stripMargin)
  """Same for 'eval(new UnsoundConst(""))'""")*/
}

trait LambdaInterpFinal {
  trait Exp[+T]
  /*
  final case class Const[+T](t: T) extends Exp[T]
  final case class App[S, +T](fun: Exp[S => T], arg: Exp[S]) extends Exp[T]
  final case class Fun[-S, +T](body: Exp[S] => Exp[T]) extends Exp[S => T]
   */

  final case class Const[T](t: T) extends Exp[T]
  final case class App[S, T](fun: Exp[S => T], arg: Exp[S]) extends Exp[T]
  final case class Fun[S, T](body: Exp[S] => Exp[T]) extends Exp[S => T]

  def eval[T](term: Exp[T]): T =
    term match {
      case Const(t) => t
      case App(fun, arg) =>
        eval(fun) apply eval(arg)
      case f: Fun[s, t] =>
        (x: s) => eval(f.body(Const(x)))
    }
}

// Misc

trait LambdaSubMoreVariant {
  //An even more variant encoding:
  trait Exp[+T]
  case class Const[+T](t: T) extends Exp[T]
  case class App[S, +T](fun: Exp[S => T], arg: Exp[S]) extends Exp[T]
  case class Fun[-S, +T](body: Exp[S] => Exp[T]) extends Exp[S => T]
}

trait DeclarationSiteVariance {
  trait Base[+T]
  class Derived[T] extends Base[T] //@ \label{ln:derived}
  class DerivedAgain[T] extends Derived[Any] with Base[Boolean]
}