GenericUnification.scala

package logprog

import scalaz._, Scalaz._
import shapeless._

abstract class GenericUnifiable[T, Children <: HList] {
  def decompose(t: T): VarId \/ Children 
  def mapChildren(t: T)(f: Children => Children): T
  def topLevelEquivalent(t1: T, t2: T): Boolean
}
object GenericUnifiable {
  def atomicUniversalEquality[T]: GenericUnifiable[T, HNil] = new GenericUnifiable[T, HNil] {
    def decompose(t: T) = HNil.right
    def mapChildren(t: T)(f: HNil => HNil) = t
    def topLevelEquivalent(t1: T, t2: T) = t1 == t2
  }
}

object GenericUnification {
  implicit val intGenericUnifiable: GenericUnifiable[Int, HNil] = GenericUnifiable.atomicUniversalEquality[Int]

  implicit def tupleGenericUnifiable[T1, T2] = new GenericUnifiable[Tuple2[T1, T2], T2 :: T1 :: HNil] {
    def decompose(t: Tuple2[T1, T2]): VarId \/ (T2 :: T1 :: HNil) = {
      children(t).right
    }

    def children(t: Tuple2[T1, T2]): (T2 :: T1 :: HNil) = {
      (t._2 :: t._1 :: HNil)
    }

    def mapChildren(t: Tuple2[T1, T2])(f: T2 :: T1 :: HNil => T2 :: T1 :: HNil): Tuple2[T1, T2] = {
      val hlist = f(children(t))
      hlist.tail.head -> hlist.head
    }

    def topLevelEquivalent(t1: Tuple2[T1, T2], t2: Tuple2[T1, T2]): Boolean = {
      true
    }
  }
    
  sealed abstract class Logical[T1] {
    def zip[T2](other: Logical[T2]): Logical[(T1, T2)] = ???
    def map[T2](f: T1 => T2): Logical[T2] = ???
  }
  object Logical {
    case class Value[T](value: T) extends Logical[T]
    case class Reference[T](varId: VarId) extends Logical[T]

    implicit def logicalGenericUnifiable[T, Children <: HList](implicit genericTerm: GenericUnifiable[T, Children]) = 
      new GenericUnifiable[Logical[T], T :: HNil] {
        def decompose(t: Logical[T]): VarId \/ (T :: HNil) = t match {
          case Value(value)     => (value :: HNil).right
          case Reference(varId) => varId.left
        }

        def mapChildren(t: Logical[T])(f: T :: HNil => T :: HNil): Logical[T] = t match {
          case Value(value) => 
            Value(f(value :: HNil).head)
          case v: Reference[T] =>
            v
        }

        def topLevelEquivalent(t1: Logical[T], t2: Logical[T]): Boolean = {
          (t1, t2) match {
            case (Reference(l),   Reference(r)) => l == r
            case (Value(_), Value(_)) => true
            case other => false
          }
        }
      }
  }

  /*
   * Proof that the Universe of types has the following children types  
   */
  sealed abstract class UniverseChildren[
    Universe <: HList,
    Children <: HList
  ] {
    def unifyChildren(left: Children, right: Children, knowledge: Option[Knowledge[Any]]): Option[Knowledge[Any]]
    def varsInChildren(children: Children): List[VarId]
  }

  implicit def universeChildrenBase: UniverseChildren[HNil, HNil] = new UniverseChildren[HNil, HNil] {
    override def unifyChildren(left: HNil, right: HNil, k: Option[Knowledge[Any]]) = k
    override def varsInChildren(children: HNil): List[VarId] = List.empty
  }

  implicit def universeChildrenRec[
    X, 
    XChildren    <: HList,
    XUniverse    <: HList,
    Tail         <: HList,
    TailUniverse <: HList
  ](implicit xUnifiable: GenericUnifiable[X, XChildren],
             xUniverse: UniverseChildren[XUniverse, XChildren],
             tUniverse: UniverseChildren[TailUniverse, Tail]): UniverseChildren[
    (X :: XUniverse :: HNil) :: TailUniverse,
     X :: Tail
  ] = new UniverseChildren[
    (X :: XUniverse :: HNil) :: TailUniverse,
     X :: Tail
  ] {
    override def unifyChildren(left: X :: Tail, right: X :: Tail, maybeK: Option[Knowledge[Any]]) = {
      maybeK.flatMap { k0 =>
        val k1 = unifyWith(left.head, right.head, k0)
        tUniverse.unifyChildren(left.tail, right.tail, k1)
      }
    }

    override def varsInChildren(children: X :: Tail): List[VarId] = {
      val vs = xUnifiable.decompose(children.head) match {
        case -\/(vId)       => List(vId)
        case \/-(xChildren) => xUniverse.varsInChildren(xChildren)
      }

      vs ::: tUniverse.varsInChildren(children.tail)
    }
  }


  /*
   * Unify t1 with t2 with some knowledge.
   */
  def unifyWith[
      T, 
      // (Child1 :: Child1Universe :: HNil) :: 
      // (Child2 :: Child2Universe :: HNil) :: 
      // ... :: 
      // (ChildN :: ChildUniverse :: HNil) :: HNil
      Universe <: HList,
      Children <: HList
  ](
      t1: T, 
      t2: T, 
      knowledge: Knowledge[Any]
  )(implicit 
      unifiable:        GenericUnifiable[T, Children],
      universeChildren: UniverseChildren[Universe, Children]): Option[Knowledge[Any]] = {

    def unifyTerms(
        lChildren: Children, 
        rChildren: Children,
        k0: Knowledge[Any]): Option[Knowledge[Any]] = {
      universeChildren.unifyChildren(lChildren, rChildren, Some(k0))
    }

    (unifiable.decompose(t1), unifiable.decompose(t2)) match {
      case (\/-(c1), \/-(c2)) => 
        if (unifiable.topLevelEquivalent(t1, t2)) {
          unifyTerms(c1, c2, knowledge)
        } else {
          None
        }

      case (-\/(v1), -\/(v2)) =>
        if (v1 == v2) {
          Some(knowledge)
        } else {
          bind(v1, t2, knowledge)
        }

      case (-\/(v1), \/-(_)) =>
        bind(v1, t2, knowledge)

      case (\/-(_), -\/(v2)) =>
        bind(v2, t1, knowledge)
    }
  }

  def bind[
      T, 
      Children <: HList,
      Universe <: HList
  ](
      v: VarId, 
      t: T, 
      knowledge: Knowledge[Any]
  )(implicit 
      unifiable: GenericUnifiable[T, Children],
      universeChildren: UniverseChildren[Universe, Children]): Option[Knowledge[Any]] = {
    /*
     * Trying to unify `V` with foo(V, b, c) should fail as this is equivalent to infinite regression.
     *
     * this should be implemented in UniverseChildren
    if (occursCheck(v, knowledge, t)) {
      None
    } else {
    */

    knowledge.lookup(v) match {
      // v is free
      case None =>
        Some(knowledge.modBind(v, t))

      // v is bound to term `otherT` (either iteself or transitively via other variable)
      case Some(any) =>
        val otherT = any.asInstanceOf[T]
        unifyWith(t, otherT, knowledge).map { k => k.modBind(v, t) }
    }
  }

  /*
  def bind[T, Children <: HList](
      v: VarId, 
      t: T, 
      knowledge: Knowledge[Any])(implicit unifiable: GenericUnifiable[T, Children]): Option[Knowledge[T]] = {
    /*
     * Trying to unify `V` with foo(V, b, c) should fail as this is equivalent to infinite regression.
     */
    if (occursCheck(v, knowledge, t)) {
      None
    } else {
      knowledge.lookup(v) match {
        // v is free
        case None =>
          Some(knowledge.modBind(v, t))

        // v is bound to term `otherT` (either iteself or transitively via other variable)
        case Some(otherT) =>
          unifyWith(t, otherT, knowledge).map { k => k.modBind(v, t) }
      }
    }
  }
  */

  /*
   * Recursively checks if `v` occurs in `t` using the supplied knowledge.
   *
  def occursCheck[T](v: VarId, knowledge: Knowledge[T], t: T)(implicit unifiable: GenericUnifiable[T]): Boolean = {
    def reachlist(l: List[VarId]): List[VarId] = l ::: l.flatMap(reachable)
    def reachable(v: VarId): List[VarId] = reachlist(knowledge.lookup(v).map { x => vars(x) }.getOrElse(List.empty))

    // v may be aliased to some other variable 
    val aliased = knowledge.lookup(v).flatMap(unifiable.varCheck) match {
      case Some(alias) =>
        alias
      case None =>
        v
    }

    reachlist(vars(t)).contains(aliased)
  }

  def vars[
    T,
    Children <: HList,
    Universe <: HList
  ](t: T)(implicit unifiable: GenericUnifiable[T, Children], universeChildren: UniverseChildren[Universe, Children]): List[VarId] = {
    unifiable.decompose(t) match {
      case -\/(varId)    => List(varId)
      case \/-(children) => universeChildren.varsInChildren(children)
    }
  }
  */

  type LogicalK[F[_], A] = Logical[F[Logical[A]]]

  def ===[
    A,
    Children <: HList,
    Universe <: HList
  ](l: A, r: A)(implicit unifiable: GenericUnifiable[A, Children],
                         universe: UniverseChildren[Universe, Children]) = {

    Relation.succeed[Knowledge[Any]].flatMap { knowledge =>
      unifyWith(l, r, knowledge) match {
        case Some(newKnowledge) => 
          Relation.succeed.map(_ => newKnowledge)
        case None =>
          Relation.fail
      }
    }
  }

  import Relation.{Predicate, defpred}

  /*
  implicit def listUnifiable[
    A,
    Children <: HList
  ](unifiable: GenericUnifiable[A, Children]): GenericUnifiable[LogicalK[List, A], Children] = 
    new GenericUnifiable[LogicalK[List, A], Children] {
      def decompose(t: LogicalK[List, A]): VarId \/ Children = {
        t match {
          case Val
        }
      }

      def children(t: Tuple2[T1, T2]): (T2 :: T1 :: HNil) = {
        (t._2 :: t._1 :: HNil)
      }

      def mapChildren(t: Tuple2[T1, T2])(f: T2 :: T1 :: HNil => T2 :: T1 :: HNil): Tuple2[T1, T2] = {
        val hlist = f(children(t))
        hlist.tail.head -> hlist.head
      }

      def topLevelEquivalent(t1: Tuple2[T1, T2], t2: Tuple2[T1, T2]): Boolean = {
        true
      }
    }
    */
}