Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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
}
}
*/
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.