package WithoutVariance
import scala.language.implicitConversions

/**
  * Here we demonstrate embeddings which do not use covariance. Comments will
  * focus on the differences with GADTWithVariance.scala.
  */

// Simply-typed lambda-calculus, using higher-order abstract syntax.
trait 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]
  case class Fun[S, T](body: Exp[S] => Exp[T]) extends Exp[S => T]
}

// An interpreter for simply-typed lambda-calculus.
trait Interp extends Lambda {
  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)))
      //case Fun(body) =>
        //x => eval(body(Const(x)))
    }
}

/////////////////////////////////////////////////
// Extensions for simply-typed lambda calculus //
/////////////////////////////////////////////////

// The extensions below are similar to ones in GADTWithVariance.scala, but they
// work with less problems.

trait LamExamples extends Lambda {
  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, Const(1)))
}

trait Lists extends Lambda 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 Null() =>
        List()
      case Car(l) =>
        eval(l).head
      case Cdr(l) =>
        eval(l).tail
      case _ =>
        super.eval(term)
    }
}

trait Nums extends Lambda 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)
      case _ =>
        super.eval(term)
    }
}

trait NumsGen extends Lambda 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))
      case _ =>
        super.eval(term)
    }
}

trait BetaReduce extends Lambda {
  def betaReduce[T](term: Exp[T]): Exp[T] =
    term match {
      case App(Fun(f), arg) => f(arg)
      case e => e
    }
}

trait Colls extends Lambda 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)
      case _ =>
        super.eval(term)
    }
}

// Express type-preserving map fusion, but more succesfully. We only encounter
// some limitations of type inference.

trait Fusion extends Lambda with Colls {

  // fusePrecise uses only typed patterns, which are not nestable, hence they
  // are only a fancy syntax for type-casing but do not have the full power of
  // nested pattern matching.
  //
  def fusePrecise[T](t: Exp[T]): Exp[T] =
    t match {
      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))))
          case _ => m1
        }
      case _ => t
    }

  // fuseSimple tries using real pattern-matching, but runs into problems.
  //
  def fuseSimple[T](t: Exp[T]): Exp[T] =
    t match {
      //case MapOp(MapOp(coll, f), g) =>
        //MapOp(coll, Fun(x => App(g, App(f, x))))
      //Doesn't work, we need to annotate the type of x.
      case MapOp(m: MapOp[a, b], g) =>
        m match {
          case MapOp(coll, f) =>
            MapOp(coll, Fun((x: Exp[a]) => App(g, App(f, x))))
          case _ => t
        }
      case _ => t
    }
}

object Language extends Lambda with Lists with NumsGen with BetaReduce
    with LamExamples with LambdaUpcast with Implicit {
  //class Null2[T]() extends Null[T] with Exp[Nil.type]
  class Null2[T]() extends Null[T] with Exp[List[T]]
  val a = ((v: Int) => (null: Exp[List[Int]] with Exp[Nil.type]))
  def f1(b: Int => Exp[List[Int]]) = b(0)
  f1(a)
}


//////////////////////////////////////////////////////////
// An embedding of lambda-sub with explicit subsumption //
//////////////////////////////////////////////////////////

trait LambdaUpcast extends Lambda with Interp {
  case class Upcast[U, T <: U](e: Exp[T]) extends Exp[U]

  override def eval[T](term: Exp[T]): T =
    term match {
      case Upcast(e) => eval(e)
      case _ =>
        super.eval(term)
    }
}

// Already betaReduce needs to deal with Upcast by code duplication.
trait BetaReduceSub extends LambdaUpcast {
  def betaReduce[T](term: Exp[T]): Exp[T] =
    term match {
      case App(Fun(f), arg) => f(arg)
      case App(Upcast(Fun(f)), arg) =>
        // Why is this accepted? No implicit conversion is available here.
        f(arg)
      case e => e
    }
}

// Similar code duplication appears also with map fusion. Note that this version
// contains multiple experiments.

trait FusionUpcast extends LambdaUpcast with Colls {
  def fuseExperiments[T](t: Exp[T]): Exp[T] =
    t match {
      case MapOp(m: MapOp[a, b], g) =>
        m match {
          case MapOp(coll: Exp[Traversable[`a`]], f) =>
            MapOp(coll, Fun((x: Exp[a]) => App(g, App(f, x))))
          case MapOp(coll, f) =>
            MapOp(coll, Fun((x: Exp[a]) => App(g, App(f, x))))
        }
/*
      case MapOp(u: Upcast[s, t], g) =>
        u match {
          case Upcast(m: MapOp[a, b]) =>
            m match {
              case MapOp(coll, f) =>
                MapOp(coll, Fun((x: Exp[a]) => App(g, App(f, x))))
            }
        }
 */
      case MapOp(Upcast(m: MapOp[a, b]), g) =>
        m match {
          case MapOp(coll, f) =>
            //This probably works by upcasting ... the return value?
            //g has type Any => Any.
            MapOp(coll, Fun((x: Exp[a]) => App(g, App(f, x))))
        }
      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))))
          case u: Upcast[Traversable[`t`], Traversable[s]] => //s <: t
            u.e match { //u.e: Exp[Traversable[s]]
              //case m2: MapOp[r, `s`] => //should be correct
              case m2: MapOp[r, `s`] =>
                //case class Upcast[U, T <: U](e: Exp[T]) extends Exp[U]
                //implicit def upcast[U, T <: U](e: Exp[T]): Exp[U] = Upcast(e)
                MapOp(m2.coll, Fun((x: Exp[r]) => App[t, u](m1.f, /*Upcast[t, s]*/(App[r, s](m2.f, x): Exp[s]).asInstanceOf[Exp[t]])))
                //m1
              case _ => m1
            }
          case _ => m1
        }
      case e => e
    }
}

// Model subsumption through an implicit conversion:
trait Implicit extends Colls with NumsGen with LambdaUpcast with Fusion {
  implicit def upcast[U, T <: U](e: Exp[T]): Exp[U] = Upcast(e)
}

// If we model subsumption through an implicit conversion, we run into type
// inference problems; some examples are demonstrated here.
trait InferenceProblems extends Implicit {
  val plus1: Exp[Int => Int] = Fun((x: Exp[Int]) => Plus(x, Const(1)))
  val id: Exp[Any => Any] = Fun(x => x)

  val res1 = MapOp[Int, Int](MapOp[Int, Int](Const(List(1, 2, 3)), plus1), plus1)
  //val res2 = MapOp[Int, Int](MapOp(Const(List(1, 2, 3)), plus1), plus1) //Type inference fails here.

  val baseColl1 = Const(List(1, 2, 3))
  //val res3 = MapOp[Int, Int](MapOp(baseColl1, plus1), plus1) //Type inference fails here too

  val baseColl2: Exp[List[Int]] = Const(List(1, 2, 3))
  //val res4 = MapOp[Int, Int](MapOp(baseColl2, plus1), plus1) //Type inference fails here too

  //Moving the type annotation fixes the problem

  val res4_2 = MapOp(MapOp[Int, Int](upcast(baseColl2), plus1), plus1) //but upcast, now, is not needed
  val res4 = MapOp(MapOp[Int, Int](baseColl2, plus1), plus1)
  //val res4_1 = MapOp[Int, Int](MapOp(upcast(baseColl2), plus1), plus1) //Type inference fails here too?

  //But by moving the type annotation, we can save much work
  val res2 = MapOp(MapOp[Int, Int](Const(List(1, 2, 3)), plus1), plus1)
  val res3 = MapOp(MapOp[Int, Int](baseColl1, plus1), plus1)

  val res = MapOp(res4.coll, id)
  val fused = fuseSimple(res)
}

trait UseSiteVariance {
  //trait Base_[T]; type Base[T] = Base_[_ <: T]
  trait Base[T]; type Base_[T] = Base[_ <: T]
  class Derived[T] extends Base[T]
}

// We can try using use-site variance instead of definition-site variance. This
// interpreter tries to interpret a term Exp[_x] type unknown but bound by _x <:
// T, which is like allowing subsumption at the root of the argument. This is
// however not an interpreter for lambda-sub, since subsumption is not allowed
// in the middle of the term.
//
// We encounter what seems to be an unneccessary limitation of the typechecker,
// hence we did not try to embed full lambda-sub yet. We should however
// investigate this limitation.

trait InterpWildcard extends Lambda {
  def eval[T](term: Exp[_x] forSome {type _x <: T} ): T =
    term match {
      case Const(t) => t
      case App(fun, arg) =>
        eval(fun) apply eval(arg)
      case f: Fun[s, t] =>
        //s => t <: _x <: T, so this should arguably typecheck. Here the
        //typechecker is failing!
        ((x: s) => eval(f.body(Const(x)))).asInstanceOf[T]
      //case Fun(body) =>
        //x => eval(body(Const(x)))
    }
}