Skip to content

# jaked/ambassadortothecomputers.blogspot.com

### Subversion checkout URL

You can clone with
or
.

# Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also compare across forks.

# Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also compare across forks.
...
• 2 commits
• 6 files changed
• 0 commit comments
• 1 contributor
Commits on May 27, 2011
 jaked `checkpoint scrolog` `f2a6e8f`
Commits on Jun 02, 2011
 jaked `checkpoint` `7ece415`
2  _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)
18 _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) + } + } +}
2  _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)
29 _code/scala-logic/Scrolog.scala
 @@ -0,0 +1,29 @@ +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 syntax[A](t: P) = LogicState.syntax(t) + + 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)) }) +}
75 _code/scala-logic/Term.scala
 @@ -3,15 +3,26 @@ 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]] 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 = { @@ -23,24 +34,6 @@ object Env { def empty = new Env(HashMap()) } -trait Term[A] { - 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] { def unify(e: Env, t: Term[A]) = t match { @@ -58,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 } } @@ -77,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_) => @@ -96,7 +88,7 @@ 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 } } @@ -111,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) => @@ -130,27 +124,20 @@ 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 } } 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) }) -}
58 _code/scala-logic/Test.scala
 @@ -1,10 +1,56 @@ -object Test { - import Term._ - import LogicStateSKE._ +trait Test { + val Scrolog: Scrolog + import Scrolog._ - def member[A](x: Term[A], l: Term[List[A]]): T[Env,Unit] = { + 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 = 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 = S(n.ground) + + 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]("m"); val p2 = Evar[Nat]("p") + (m =:= Z & n =:= p) | + (m =:= STerm(m2) & p =:= STerm(p2) & sum(m2, n, p2)) } }

### No commit comments for this range

Something went wrong with that request. Please try again.