Permalink
Browse files

checkpoint logic part 2

  • Loading branch information...
1 parent f7d3a9f commit c43b8e7d7ad8f15f6c688198370850ef3a58d657 @jaked committed Apr 21, 2011
@@ -48,57 +48,53 @@ object LogicList extends Logic {
}
object LogicSFK extends Logic {
- // type FK[R] = => R
- type SK[A,R] = (A, => R) => R
+ type FK[R] = () => R
+ type SK[A,R] = (A, FK[R]) => R
- trait T[A] { def apply[R](sk: SK[A,R], fk: => R): R }
+ trait T[A] { def apply[R](sk: SK[A,R], fk: FK[R]): R }
def fail[A] =
new T[A] {
- def apply[R](sk: SK[A,R], fk: => R) = fk
+ def apply[R](sk: SK[A,R], fk: FK[R]) = fk()
}
def unit[A](a: A) =
new T[A] {
- def apply[R](sk: SK[A,R], fk: => R) = sk(a, fk)
+ def apply[R](sk: SK[A,R], fk: FK[R]) = sk(a, fk)
}
def or[A](t1: T[A], t2: => T[A]) =
new T[A] {
- def apply[R](sk: SK[A,R], fk: => R) = t1(sk, t2(sk, fk))
+ def apply[R](sk: SK[A,R], fk: FK[R]) = t1(sk, { () => t2(sk, fk) })
}
def bind[A,B](t: T[A], f: A => T[B]) =
new T[B] {
- def apply[R](sk: SK[B,R], fk: => R) =
+ def apply[R](sk: SK[B,R], fk: FK[R]) =
t(({ (a, fk) => f(a)(sk, fk) }: SK[A,R]), fk)
}
def apply[A,B](t: T[A], f: A => B) =
new T[B] {
- def apply[R](sk: SK[B,R], fk: => R) =
+ def apply[R](sk: SK[B,R], fk: FK[R]) =
t(({ (a, fk) => sk(f(a), fk) }: SK[A,R]), fk)
}
def filter[A](t: T[A], p: A => Boolean) =
new T[A] {
- def apply[R](sk: SK[A,R], fk: => R) =
- t(({ (a, fk) => if (p(a)) sk(a, fk) else fk }: SK[A,R]), fk)
+ def apply[R](sk: SK[A,R], fk: FK[R]) =
+ t(({ (a, fk) => if (p(a)) sk(a, fk) else fk() }: SK[A,R]), fk)
}
def split[A](t: T[A]) = {
- def unsplit(r: Option[(A,T[A])]): T[A] =
- r match {
+ def unsplit(fk: FK[Option[(A,T[A])]]): T[A] =
+ fk() match {
case None => fail
case Some((a, t)) => or(unit(a), t)
}
- def unit[A](a: => A) =
- new T[A] {
- def apply[R](sk: SK[A,R], fk: => R) = sk(a, fk)
- }
def sk : SK[A,Option[(A,T[A])]] =
- { (a, fk) => Some(a, bind(unit(fk), unsplit)) }
- t(sk, None)
+ { (a, fk) => Some((a, bind(unit(fk), unsplit))) }
+ t(sk, { () => None })
}
}
@@ -9,6 +9,9 @@ trait LogicState { L =>
def filter[S,A](t: T[S,A], p: A => Boolean): T[S,A]
def split[S,A](s: S, t: T[S,A]): Option[(S,A,T[S,A])]
+ def get[S]: T[S,S]
+ def set[S](s: S): T[S, Unit]
+
def or[S,A](as: List[A]): T[S,A] =
as.foldRight(fail[S,A])((a, t) => or(unit(a), t))
@@ -26,6 +29,7 @@ trait LogicState { L =>
def withFilter(p: A => Boolean): T[S,A] = L.filter(t, p)
def |(t2: => T[S,A]): T[S,A] = L.or(t, t2)
+ def &[B](t2: => T[S,B]): T[S,B] = L.bind(t, { _: A => t2 })
}
implicit def syntax[S,A](t: T[S,A]) = Syntax(t)
@@ -88,6 +92,16 @@ object LogicStateSFK extends LogicState {
{ (s, a, fk) => Some(s, a, byNameUnit(fk).flatMap(unsplit)) }
t(s, sk, None)
}
+
+ def get[S]: T[S,S] =
+ new T[S,S] {
+ def apply[R](s: S, sk: SK[S,S,R], fk: => R) = sk(s, s, fk)
+ }
+
+ def set[S](s: S): T[S,Unit] =
+ new T[S,Unit] {
+ def apply[R](_s: S, sk: SK[S,Unit,R], fk: => R) = sk(s, (), fk)
+ }
}
object LogicStateSKE extends LogicState {
@@ -129,4 +143,8 @@ object LogicStateSKE extends LogicState {
}
catch { case Fail | Finish => lb.result }
}
+
+ def get[S] = { (s, sk) => sk(s, s) }
+
+ def set[S](s: S) = { (_s, sk) => sk(s, ()) }
}
@@ -0,0 +1,155 @@
+import scala.collection.immutable.HashMap
+
+class Evar[A](val name: String)
+object Evar { def apply[A](name: String) = new Evar[A](name) }
+
+class Env(m: HashMap[Evar[Any],Term[Any]]) {
+ def apply[A](v: Evar[A]) =
+ m(v.asInstanceOf[Evar[Any]]).asInstanceOf[Term[A]]
+ def get[A](v: Evar[A]): Option[Term[A]] =
+ m.get(v.asInstanceOf[Evar[Any]]).asInstanceOf[Option[Term[A]]]
+ def updated[A](v: Evar[A], t: Term[A]) =
+ Env(m.updated(v.asInstanceOf[Evar[Any]], t.asInstanceOf[Term[Any]]))
+
+ override def toString = {
+ "{ " + m.map({ case (k, v) => k.name + " = " + v.toString }).mkString(", ") + " }"
+ }
+}
+object Env {
+ def apply(m: HashMap[Evar[Any],Term[Any]]) = new Env(m)
+ def empty = new Env(HashMap())
+}
+
+trait Term[A] {
+ def unify(e: Env, t: Term[A]): Option[Env]
+ def occurs[B](e: Env, v: Evar[B]): Boolean
+ def subst(e: Env): Term[A]
+ def ground(e: Env): A
+
+ import LogicStateSKE._
+ def =!=(t2: Term[A]): T[Env, Unit] =
+ for {
+ env <- get
+ env2 <-
+ (unify(env, t2) match {
+ case None => fail[Env,Unit]
+ case Some(e) => set(e)
+ })
+ } yield env2
+}
+
+case class VarTerm[A](v: Evar[A]) extends Term[A] {
+ def unify(e: Env, t: Term[A]) =
+ e.get(v) match {
+ case Some(t2) => t2.unify(e, t)
+ case None =>
+ t match {
+ case VarTerm(v2) if (v2 == v) => Some(e)
+ case _ =>
+ if (t.occurs(e, v)) None
+ else Some(e.updated(v, t))
+ }
+ }
+
+ def occurs[B](e: Env, v2: Evar[B]) =
+ e.get(v) match {
+ case Some(t) => t.occurs(e, v2)
+ case None => v2 == v
+ }
+
+ def subst(e: Env) =
+ e.get(v) match {
+ case Some(t) => t.subst(e)
+ case None => this
+ }
+
+ def ground(e: Env) =
+ e.get(v) match {
+ case Some(t) => t.ground(e)
+ case None => throw new IllegalArgumentException("not ground")
+ }
+
+ override def toString = { v.name }
+}
+
+case class LitTerm[A](a: A) extends Term[A] {
+ def unify(e: Env, t: Term[A]) =
+ t match {
+ case LitTerm(a2) => if (a == a2) Some(e) else None
+ case _: VarTerm[_] => t.unify(e, this)
+ case _ => t.unify(e, this)
+ }
+
+ def occurs[B](e: Env, v2: Evar[B]) = false
+ def subst(e: Env) = this
+ def ground(e: Env) = a
+
+ override def toString = { a.toString }
+}
+
+case class Tuple2Term[A,B](_1: Term[A], _2: Term[B]) extends Term[(A,B)] {
+ def unify(e: Env, t: Term[(A,B)]) =
+ t match {
+ case Tuple2Term(_1_, _2_) =>
+ for (e1 <- _1.unify(e, _1_); e2 <- _2.unify(e1, _2_)) yield e2
+ case _: VarTerm[_] => t.unify(e, this)
+ case _ => None
+ }
+
+ def occurs[C](e: Env, v: Evar[C]) = _1.occurs(e, v) || _2.occurs(e, v)
+ def subst(e: Env) = Tuple2Term(_1.subst(e), _2.subst(e))
+ def ground(e: Env) = (_1.ground(e), _2.ground(e))
+
+ override def toString = { (_1, _2).toString }
+}
+
+case class NilTerm[A]() extends Term[List[A]] {
+ def unify(e: Env, t: Term[List[A]]) =
+ t match {
+ case NilTerm() => Some(e)
+ case _: VarTerm[_] => t.unify(e, this)
+ case _ => None
+ }
+
+ def occurs[B](e: Env, v: Evar[B]) = false
+ def subst(e: Env) = this
+ def ground(e: Env) = Nil
+
+ override def toString = { Nil.toString }
+}
+
+case class ConsTerm[A](hd: Term[A], tl: Term[List[A]]) extends Term[List[A]] {
+ def unify(e: Env, t: Term[List[A]]) =
+ t match {
+ case ConsTerm(hd2, tl2) =>
+ for (e1 <- hd.unify(e, hd2); e2 <- tl.unify(e1, tl2)) yield e2
+ case _: VarTerm[_] => t.unify(e, this)
+ case _ => None
+ }
+
+ def occurs[C](e: Env, v: Evar[C]) = hd.occurs(e, v) || tl.occurs(e, v)
+ def subst(e: Env) = ConsTerm(hd.subst(e), tl.subst(e))
+ def ground(e: Env) = hd.ground(e) :: tl.ground(e)
+
+ override def toString = { hd.toString + " :: " + tl.toString }
+}
+
+object Term {
+ implicit def var2term[A](v: Evar[A]): VarTerm[A] = VarTerm(v)
+ //implicit def lit2term[A](a: A): LitTerm[A] = LitTerm(a)
+ implicit def int2term(a: Int): LitTerm[Int] = LitTerm(a)
+ implicit def tuple2term[A,B](ab: Tuple2[Term[A],Term[B]]): Tuple2Term[A,B] =
+ Tuple2Term(ab._1, ab._2)
+ implicit def list2term[A](l: List[Term[A]]): Term[List[A]] =
+ l match {
+ case Nil => NilTerm[A]
+ case hd :: tl => ConsTerm(hd, list2term(tl))
+ }
+}
+
+object Run {
+ import LogicStateSKE._
+
+ def run[A](t: T[Env,Unit], n: Int, tm: Term[A]): List[Term[A]] =
+ LogicStateSKE.run(Env.empty, t, n).map({ case (e, _) => tm.subst(e) })
+}
@@ -0,0 +1,10 @@
+object Test {
+ import Term._
+ import LogicStateSKE._
+
+ def member[A](x: Term[A], l: Term[List[A]]): T[Env,Unit] = {
+ val hd = Evar[A]("hd"); val tl = Evar[List[A]]("tl")
+ ConsTerm(hd, tl) =!= l &
+ (x =!= hd | member(x, tl))
+ }
+}
Oops, something went wrong.

0 comments on commit c43b8e7

Please sign in to comment.