checkpoint

_code/scala-logic/Logic.scala

@@ -51,7 +51,7 @@ trait Logic { L =>
     def runAcc(t: T[A], n: Int, acc: List[A]): List[A] =
       if (n <= 0) acc.reverse else
         split(t) match {
-          case None => acc
+          case None => acc.reverse
           case Some((a, t)) => runAcc(t, n - 1, a :: acc)
         }
     runAcc(t, n, Nil)

_code/scala-logic/LogicForgetState.scala

@@ -0,0 +1,18 @@
+trait LogicForgetState extends Logic {
+  val LogicState: LogicState
+
+  type T[A] = LogicState.T[Unit,A]
+
+  def fail[A]: T[A] = LogicState.fail
+  def unit[A](a: A): T[A] = LogicState.unit(a)
+  def or[A](t1: T[A], t2: => T[A]): T[A] = LogicState.or(t1, t2)
+  def bind[A,B](t: T[A], f: A => T[B]): T[B] = LogicState.bind(t, f)
+  def apply[A,B](t: T[A], f: A => B): T[B] = LogicState.apply(t, f)
+  def filter[A](t: T[A], p: A => Boolean): T[A] = LogicState.filter(t, p)
+  def split[A](t: T[A]): Option[(A,T[A])] = {
+    LogicState.split((), t) match {
+      case None => None
+      case Some((_, a, t)) => Some(a, t)
+    }
+  }
+}

_code/scala-logic/LogicState.scala

@@ -56,7 +56,7 @@ trait LogicState { L =>
     def runAcc(t: T[S,A], n: Int, acc: List[(S,A)]): List[(S,A)] =
       if (n <= 0) acc.reverse else
         split(s0, t) match {
-          case None => acc
+          case None => acc.reverse
           case Some((s, a, t)) => runAcc(t, n - 1, (s, a) :: acc)
         }
     runAcc(t, n, Nil)

_code/scala-logic/Scrolog.scala

@@ -21,14 +21,9 @@ trait Scrolog {
   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) })
+  def run[A](t: P, n: Int, tm: Term[A]*): List[Seq[Term[A]]] =
+    LogicState.run(Env.empty, t, n)
+      .map({ case (e, _) => tm.map(_.subst(e)) })
 }

_code/scala-logic/Term.scala

@@ -3,6 +3,15 @@ import scala.collection.immutable.{Map,HashMap}
 class Evar[A](val name: String)
 object Evar { def apply[A](name: String) = new Evar[A](name) }
 
+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: A
+}
+
 class Env(m: Map[Evar[Any],Term[Any]]) {
   def apply[A](v: Evar[A]) =
     m(v.asInstanceOf[Evar[Any]]).asInstanceOf[Term[A]]
@@ -25,15 +34,6 @@ object Env {
   def empty = new Env(HashMap())
 }
 
-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
-}
-
 case class VarTerm[A](v: Evar[A]) extends Term[A] {
   def unify(e: Env, t: Term[A]) =
     t match {
@@ -51,11 +51,8 @@ case class VarTerm[A](v: Evar[A]) extends Term[A] {
       case None => this
     }
 
-  def ground(e: Env) =
-    e.get(v) match {
-      case Some(t) => t.ground(e)
-      case None => throw new IllegalArgumentException("not ground")
-    }
+  def ground =
+    throw new IllegalArgumentException("not ground")
 
   override def toString = { v.name  }
 }
@@ -70,12 +67,14 @@ case class LitTerm[A](a: A) extends Term[A] {
 
   def occurs[B](v: Evar[B]) = false
   def subst(e: Env) = this
-  def ground(e: Env) = a
+  def ground = a
 
   override def toString = { a.toString }
 }
 
-case class Tuple2Term[A,B](_1: Term[A], _2: Term[B]) extends Term[(A,B)] {
+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_) =>
@@ -89,9 +88,9 @@ case class Tuple2Term[A,B](_1: Term[A], _2: Term[B]) extends Term[(A,B)] {
 
   def occurs[C](v: Evar[C]) = _1.occurs(v) || _2.occurs(v)
   def subst(e: Env) = Tuple2Term(_1.subst(e), _2.subst(e))
-  def ground(e: Env) = (_1.ground(e), _2.ground(e))
+  def ground = (_1.ground, _2.ground)
 
-    override def toString = { (_1, _2).toString }
+  override def toString = { (_1, _2).toString }
 }
 
 case class NilTerm[A]() extends Term[List[A]] {
@@ -104,12 +103,14 @@ case class NilTerm[A]() extends Term[List[A]] {
 
   def occurs[B](v: Evar[B]) = false
   def subst(e: Env) = this
-  def ground(e: Env) = Nil
+  def ground = Nil
 
   override def toString = { Nil.toString }
 }
 
-case class ConsTerm[A](hd: Term[A], tl: Term[List[A]]) extends Term[List[A]] {
+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) =>
@@ -123,7 +124,7 @@ case class ConsTerm[A](hd: Term[A], tl: Term[List[A]]) extends Term[List[A]] {
 
   def occurs[C](v: Evar[C]) = hd.occurs(v) || tl.occurs(v)
   def subst(e: Env) = ConsTerm(hd.subst(e), tl.subst(e))
-  def ground(e: Env) = hd.ground(e) :: tl.ground(e)
+  def ground = hd.ground :: tl.ground
 
   override def toString = { hd.toString + " :: " + tl.toString }
 }

_code/scala-logic/Test.scala

@@ -1,5 +1,3 @@
-import Term._
-
 trait Test {
   val Scrolog: Scrolog
   import Scrolog._
@@ -24,7 +22,7 @@ trait Test {
 
     def occurs[A](v: Evar[A]) = false
     def subst(e: Env) = this
-    def ground(e: Env) = Z
+    def ground = Z
 
     override def toString = { Z.toString }
   }
@@ -39,7 +37,7 @@ trait Test {
 
     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))
+    def ground = S(n.ground)
 
     override def toString = { "S(" + n.toString + ")" }
   }
@@ -51,7 +49,7 @@ trait Test {
     }
 
   def sum(m: Term[Nat], n: Term[Nat], p: Term[Nat]): P = {
-    val m2 = Evar[Nat]("m2"); val p2 = Evar[Nat]("p2")
+    val m2 = Evar[Nat]("m"); val p2 = Evar[Nat]("p")
     (m =:= Z & n =:= p) |
     (m =:= STerm(m2) & p =:= STerm(p2) & sum(m2, n, p2))
   }