checkpoint scrolog

_code/scala-logic/Scrolog.scala

@@ -0,0 +1,34 @@
+trait Scrolog {
+  val LogicState: LogicState
+  import LogicState._
+
+  type P = T[Env,Unit]
+
+  class TermSyntax[A](t: Term[A]) {
+    def =:=(t2: Term[A]): P =
+      for {
+        env <- get
+        env2 <- {
+          t.subst(env).unify(env, t2.subst(env)) match {
+            case None => fail[Env,Unit]
+            case Some(e) => set(e)
+          }
+        }
+      } yield env2
+  }
+
+  def printEnv: P = for (env <- get) yield Console.println(env)
+  def println(m: String): P = unit(Console.println(m))
+
+  implicit def termSyntax[A](t: Term[A]) = new TermSyntax(t)
+  implicit def varTermSyntax[A](t: VarTerm[A]) = new TermSyntax(t)
+  implicit def litTermSyntax[A](t: LitTerm[A]) = new TermSyntax(t)
+  implicit def tuple2TermSyntax[A,B](t: Tuple2Term[A,B]) = new TermSyntax(t)
+  implicit def nilTermSyntax[A](t: NilTerm[A]) = new TermSyntax(t)
+  implicit def consTermSyntax[A](t: ConsTerm[A]) = new TermSyntax(t)
+
+  implicit def syntax[A](t: P) = LogicState.syntax(t)
+
+  def run[A](t: P, n: Int, tm: Term[A]): List[Term[A]] =
+    LogicState.run(Env.empty, t, n).map({ case (e, _) => tm.subst(e) })
+}

_code/scala-logic/Term.scala

@@ -9,9 +9,11 @@ class Env(m: Map[Evar[Any],Term[Any]]) {
   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 = {
-    val e2 = Env.empty.updated(v, t)
+    val v2 = v.asInstanceOf[Evar[Any]]
+    val t2 = t.asInstanceOf[Term[Any]]
+    val e2 = Env(Map(v2 -> t2))
     val m2 = m.mapValues(_.subst(e2))
-    Env(m2.updated(v.asInstanceOf[Evar[Any]], t.asInstanceOf[Term[Any]]))
+    Env(m2.updated(v2, t2))
   }
 
   override def toString = {
@@ -24,21 +26,12 @@ object Env {
 }
 
 trait Term[A] {
+  // invariant: on call to unify, this and t have e substituted
   def unify(e: Env, t: Term[A]): Option[Env]
+
   def occurs[B](v: Evar[B]): Boolean
   def subst(e: Env): Term[A]
   def ground(e: Env): A
-
-  import LogicStateSFK._
-  def =!=(t2: Term[A]): T[Env, Unit] =
-    for {
-      env <- get
-      env2 <-
-      (subst(env).unify(env, t2.subst(env)) match {
-        case None => fail[Env,Unit]
-        case Some(e) => set(e)
-      })
-    } yield env2
 }
 
 case class VarTerm[A](v: Evar[A]) extends Term[A] {
@@ -98,7 +91,7 @@ case class Tuple2Term[A,B](_1: Term[A], _2: Term[B]) extends Term[(A,B)] {
   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 }
+    override def toString = { (_1, _2).toString }
 }
 
 case class NilTerm[A]() extends Term[List[A]] {
@@ -136,21 +129,14 @@ case class ConsTerm[A](hd: Term[A], tl: Term[List[A]]) extends Term[List[A]] {
 }
 
 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] =
+  implicit def var2Term[A](v: Evar[A]): Term[A] = VarTerm(v)
+  //implicit def lit2term[A](a: A): Term[A] = LitTerm(a)
+  implicit def int2Term(a: Int): Term[Int] = LitTerm(a)
+  implicit def tuple2Term[A,B](ab: Tuple2[Term[A],Term[B]]): Term[(A,B)] =
     Tuple2Term(ab._1, ab._2)
-  implicit def list2term[A](l: List[Term[A]]): Term[List[A]] =
+  implicit def list2Term[A](l: List[Term[A]]): Term[List[A]] =
     l match {
       case Nil => NilTerm[A]
-      case hd :: tl => ConsTerm(hd, list2term(tl))
+      case hd :: tl => ConsTerm(hd, list2Term(tl))
     }
 }
-
-object Run {
-  import LogicStateSFK._
-
-  def run[A](t: T[Env,Unit], n: Int, tm: Term[A]): List[Term[A]] =
-    LogicStateSFK.run(Env.empty, t, n).map({ case (e, _) => tm.subst(e) })
-}

_code/scala-logic/Test.scala

@@ -1,10 +1,58 @@
-object Test {
-  import Term._
-  import LogicStateSKE._
+import Term._
 
-  def member[A](x: Term[A], l: Term[List[A]]): T[Env,Unit] = {
+trait Test {
+  val Scrolog: Scrolog
+  import Scrolog._
+
+  def member[A](x: Term[A], l: Term[List[A]]): P = {
     val hd = Evar[A]("hd"); val tl = Evar[List[A]]("tl")
-    ConsTerm(hd, tl) =!= l &
-    (x =!= hd | member(x, tl))
+    ConsTerm(hd, tl) =:= l &
+    (x =:= hd | member(x, tl))
+  }
+
+  sealed trait Nat
+  case object Z extends Nat
+  case class S(n: Nat) extends Nat
+
+  case object ZTerm extends Term[Nat] {
+    def unify(e: Env, t: Term[Nat]) =
+      t match {
+        case ZTerm => Some(e)
+        case _: VarTerm[_] => t.unify(e, this)
+        case _ => None
+      }
+
+    def occurs[A](v: Evar[A]) = false
+    def subst(e: Env) = this
+    def ground(e: Env) = Z
+
+    override def toString = { Z.toString }
+  }
+
+  case class STerm(n: Term[Nat]) extends Term[Nat] {
+    def unify(e: Env, t: Term[Nat]) =
+      t match {
+        case STerm(n2) => n.unify(e, n2)
+        case _: VarTerm[_] => t.unify(e, this)
+        case _ => None
+      }
+
+    def occurs[A](v: Evar[A]) = n.occurs(v)
+    def subst(e: Env) = STerm(n.subst(e))
+    def ground(e: Env) = S(n.ground(e))
+
+    override def toString = { "S(" + n.toString + ")" }
+  }
+
+  implicit def nat2Term(n: Nat): Term[Nat] =
+    n match {
+      case Z => ZTerm
+      case S(n) => STerm(nat2Term(n))
+    }
+
+  def sum(m: Term[Nat], n: Term[Nat], p: Term[Nat]): P = {
+    val m2 = Evar[Nat]("m2"); val p2 = Evar[Nat]("p2")
+    (m =:= Z & n =:= p) |
+    (m =:= STerm(m2) & p =:= STerm(p2) & sum(m2, n, p2))
   }
 }