foo.scala

object Abc {
  import shapeless.{ =:!=, Nat, Succ }
  import shapeless.nat.{ _0 => D0, _1 => D1, _2 => D2, _3 => D3 }
  import shapeless.ops.nat.{ Diff, GT, LTEq, ToInt }
  import shapeless.ops.hlist._

  trait Value {
    def toShortString = ???
  }
  object Value {
    implicit def stringToValue(value: String): Value = StringValue(value)
    implicit def doubleToValue(value: Double): Value = DoubleValue(value)
    implicit def longToValue(value: Long): Value = LongValue(value)
    implicit def intToValue(value: Int): Value = LongValue(value)

    val Ordering: Ordering[Value] = new Ordering[Value] {
      def compare(x: Value, y: Value): Int = ???
    }
  }
  case class StringValue(value: String) extends Value
  case class DoubleValue(value: Double) extends Value
  case class LongValue(value: Long) extends Value

  trait Content

  sealed trait Position[P <: Nat] {
    val coordinates: List[Value]

    def apply[D <: Nat : ToInt](dim: D)(implicit ev: LTEq[D, P]): Value = coordinates(toIndex(dim))

    def update[D <: Nat : ToInt, V <% Value](dim: D, value: V)(implicit ev: LTEq[D, P]): Position[P] = {
      val v: Value = value

      PositionImpl(coordinates.updated(toIndex(dim), v))
    }

    def prepend[V <% Value](value: V): Position[Succ[P]] = {
      val v: Value = value

      PositionImpl(v +: coordinates)
    }

    def insert[D <: Nat : ToInt, V <% Value](dim: D, value: V)(implicit ev: LTEq[D, P]): Position[Succ[P]] = {
      val (h, t) = coordinates.splitAt(toIndex(dim))
      val v: Value = value

      PositionImpl(h ++ (v +: t))
    }

    def append[V <% Value](value: V): Position[Succ[P]] = {
      val v: Value = value

      PositionImpl(coordinates :+ v)
    }

    def toShortString(separator: String): String = coordinates.map(_.toShortString).mkString(separator)

    override def toString = "Position(" + coordinates.map(_.toString).mkString(",") + ")"

    def toOption(): Option[Position[P]] = Option(this)

    def compare(that: Position[_]): Int = {
      if (coordinates.length == that.coordinates.length) {
        coordinates
          .zip(that.coordinates)
          .map { case (m, t) => Value.Ordering.compare(m, t) }
          .maxBy(math.abs(_))
      } else
        coordinates.length.compare(that.coordinates.length)
    }

    def toIndex[D <: Nat : ToInt](dim: D)(implicit ev: LTEq[D, P]): Int = {
      val index = Nat.toInt[D]

      if (index == 0) coordinates.length - 1 else index - 1
    }

  }


  object Position {
    implicit def pos1ToCom(pos: Position[D1]): CompactablePosition[D1] = pos

    implicit def posToCom[P <: Nat](pos: Position[P])(implicit ev: GT[P, D1]): CompactablePosition[P] = pos

    implicit def posToPer[P <: Nat](pos: Position[P])(implicit ev: GT[P, D1]): PermutablePosition[P] = pos

    trait Foo[N <: Nat]
    implicit def foo[N <: Nat](f: Foo[N])(implicit diff: Diff[N, D1]) = 0

    implicit def posToRed[
    P <: Nat,
    L <: Nat
    ](
      pos: Position[P]
    )(implicit
      ev1: Diff.Aux[P, D1, L]
    ): ReduciblePosition[L, P] = ReduciblePositionImpl[L, P](pos.coordinates)


    def apply[V <% Value](first: V): Position[D1] = {
      PositionImpl[D1](List(first))
    }
    def apply[V <% Value, W <% Value](first: V, second: W): Position[D2] = {
      PositionImpl[D2](List(first, second))
    }
    def apply[V <% Value, W <% Value, X <% Value](first: V, second: W, third: X): Position[D3] = {
      PositionImpl[D3](List(first, second, third))
    }

    def toString[
    P <: Nat
    ](
      descriptive: Boolean = false,
      separator: String = "|"
    ): (Position[P]) => TraversableOnce[String] = (t: Position[P]) => {
      List(if (descriptive) t.toString else t.toShortString(separator))
    }
  }

  trait CompactablePosition[P <: Nat] extends Position[P] {
    type C[_]

    def toMapValue[R <: Nat](rem: Position[R], con: Content): C[Position[R]]
  }

  object ToIndex extends Poly1 {
    implicit def defaultCase[N <: Nat : ToInt, P[X <: Nat] <: Position[X], M <: Nat](implicit
      ev: LTEq[N, M]
    ) = at[(N, P[M])] { case (n, pos) => pos.coordinates(pos.toIndex(n)) }
  }

  trait PermutablePosition[P <: Nat] extends Position[P] {

    object ToIndexPoly extends Poly1 {
      implicit def default[N <: Nat : ToInt](implicit ev: LTEq[N, P]) = at[N] ((n: N) => coordinates(toIndex(n)))
    }



    def permute[D <: Nat : ToInt](order: List[D])(implicit ev: LTEq[D, P]): Position[P] = {
      // TODO: Is it possible to zip coordinates with order and then sortBy(order) ???
      // KOSTLEAN: Not quite sure what you mean. Can you elaborate?
      PositionImpl(order.map { case d => coordinates(toIndex(d)) })
    }

    def permuteH[H <: HList, ZL <: HList, ML <: HList](l: H)(implicit
      constZipper: ZipConst.Aux[PermutablePosition[P], H, ZL],
      mapper: Mapper.Aux[ToIndex.type, ZL, ML],
      toTraversableAux: ToTraversable.Aux[ML,List,Value]): Position[P] = {
      val zipped = l zipConst this

      PositionImpl((zipped map ToIndex).toList[Value])
    }
  }

  trait ReduciblePosition[L <: Nat, P <: Nat] extends Position[P] {
    def remove[D <: Nat : ToInt](dim: D)(implicit ev: LTEq[D, P]): Position[L] = {
      val (h, t) = coordinates.splitAt(toIndex(dim))

      PositionImpl(h ++ t.tail)
    }

    def melt[
    D <: Nat : ToInt,
    E <: Nat : ToInt,
    V <% Value
    ](
      dim: D,
      into: E,
      merge: (Value, Value) => V
    )(implicit
      ev1: D =:!= E,
      ev2: LTEq[D, P],
      ev3: LTEq[E, P]
    ): Position[L] = {
      val iidx = toIndex(into)
      val didx = toIndex(dim)
      val v: Value = merge(coordinates(iidx), coordinates(didx))

      PositionImpl(coordinates
        .updated(iidx, v)
        .zipWithIndex
        .collect { case (c, i) if (i != didx) => c })
    }
  }

  private case class CompactableD1(coordinates: List[Value]) extends CompactablePosition[D1] {
    type C[R] = Content

    def toMapValue[R <: Nat](rem: Position[R], con: Content): C[Position[R]] = con
  }

  private case class CompactableDX[P <: Nat](coordinates: List[Value]) extends CompactablePosition[P] {
    type C[R] = Map[R, Content]

    def toMapValue[R <: Nat](rem: Position[R], con: Content): C[Position[R]] = Map(rem -> con)
  }

  private case class PositionImpl[P <: Nat](coordinates: List[Value]) extends Position[P]

  private case class ReduciblePositionImpl[
  L <: Nat,
  P <: Nat
  ](
    coordinates: List[Value]
  ) extends ReduciblePosition[L, P]

  sealed trait Slice[L <: Nat, N <: Nat, D <: Nat] {
    type S <: Nat
    type R <: Nat

    val dimension: D

    def selected(pos: ReduciblePosition[L, N]): Position[S]
    def remainder(pos: ReduciblePosition[L, N]): Position[R]

    protected def remove(pos: ReduciblePosition[L, N])(implicit ev1: ToInt[D], ev2: LTEq[D, N]): Position[L] = {
      pos.remove(dimension)
    }

    protected def single(pos: Position[N])(implicit ev1: ToInt[D], ev2: LTEq[D, N]): Position[D1] = {
      Position(pos(dimension))
    }
  }

  import shapeless._

  sealed trait Over[
  L <: Nat,
  N <: Nat,
  D <: Nat
  ] extends Slice[L, N, D] {
    type S = D1
    type R = L

  }
  object Over {
    def apply[L <: Nat, N <: Nat](d: Nat)(implicit
      ev1: Diff.Aux[N, L, D1],
      ev3: LTEq[d.N, N],
      w: Witness.Aux[d.N],
      ev4: ToInt[d.N]): Over[L, N, d.N] = OverImpl[L, N, d.N](w.value)

    private case class OverImpl[L <: Nat, N <: Nat, D <: Nat : ToInt](dimension: D)(implicit
      ev1: Diff.Aux[N, L, D1],
      ev3: LTEq[D, N]
    )
    extends Over[L, N, D] {
      def selected(pos: ReduciblePosition[L, N]): Position[S] = single(pos)
      def remainder(pos: ReduciblePosition[L, N]): Position[R] = remove(pos)
    }
  }

  trait Aggregator {
    type Q[S <: Nat] <: Nat

    def present[S <: Nat](pos: Position[S]): Position[Q[S]]
  }

  case class AppendTwo() extends Aggregator {
    type Q[S <: Nat] = Succ[Succ[S]]

    def present[S <: Nat](pos: Position[S]): Position[Q[S]] = pos.append("bar").append(42)
  }

  def summarise[
  L <: Nat,
  P <: Nat,
  D <: Nat
  ](
    slice: Slice[L, P, D],
    pos: Position[P],
    aggregator: Aggregator
  )(implicit
    ev1: Diff.Aux[P, D1, L]
  ): Position[aggregator.Q[slice.S]] = aggregator.present(slice.selected(Position.posToRed[P, L](pos)))

  // ==================================

  val p1: Position[D1] = Position("foo")
  val p2: Position[D2] = p1.append("bar")
  val p3: Position[D1] = p2.remove(D1)
  val p4: Position[D0] = p3.remove(D1)

  //p4.remove(D1) // Correctly does not compile.

  val o1 = Over[D0, D1](D1)
  //val o2 = Over[D0, D1, D2](D2) // Correctly does not compile.

  val o3 = Over[D1, D2](D1)
  val o4 = Over[D1, D2](D2)

  //val o5 = Over[D0, D2, D1](D1) // Correctly does not compile

  val px = Position("foo", 3.14)
  val py = o3.selected(px)

  val p = Position("foo")
  val q = summarise(Over(D1), p, AppendTwo()).remove(D1)


  // TODO: does not compile, but should - Position("foo", 3.14).permute(List(D2, D1))
  // KOSTLEAN: This can't work. D1 and D2 are different types. That information is lost in permute.
  // The compiler can't prove that some supertype of D1 and D2 can be converted to Int, I mean
  // look at the type of List(D2, D1)

  // KOSTLEAN: This however works

  Position("foo", 3.14).permuteH(D2 :: D1 :: HNil)

  //Position("foo").permute(D1) // Correctly does not compile
}