Scala Typed Logic DSL

gistfile1.scala

trait Unifiable[A] {
  ???
}

def symbol[A: Unifiable]: Symbol[A] = ???

def pred[A: Unifiable](a: Symbol[A])(f: => Set[Fact]): Predicate1[A] = ???
def pred[A: Unifiable, B: Unifiable](a: Symbol[A], b: Symbol[B])(f: => Set[Fact]): Predicate2[A, B] = ???

lazy val factorial: Predicate2[Int, Int] = {
  val N = symbol[Int]
  val F = symbol[Int]
  
  pred(N, F) {
    val N1 = symbol[Int]
    val F1 = symbol[Int]
    
    Set(
      N > 0,
      N1 is (N - 1),
      factorial(N1, F1),
      F is (N * F1))
  }
}

lazy val move: Predicate4[Int, Int, Int, Int] = {
  val N = symbol[Int]
  val X = symbol[Int]
  val Y = symbol[Int]
  val Z = symbol[Int]
  
  pred(1, X, Y, *) {
    Set(
      print("Move top disk from "),
      print(X),
      print(" to "),
      println(Y))
  } ~
  pred(N, X, Y, Z) {
    val M = symbol[Int]
    
    Set(
      N > 1,
      M is (N - 1),
      
      move(M, X, Z, Y),
      move(1, X, Y, *),
      move(M, Z, Y, X))
  }
}

// lift assumes last-symbol return convention
val runnableFact: PartialFunction[Int, Int] = factorial.run

// TODO there are a lot of obvious combinators here