Implemented example with logical unification

jvm/src/test/scala/cpstest/TestInferredByDefault.scala

@@ -26,7 +26,8 @@ class TestInferredByDefault {
        println(s)
        s
      }
-     v match {
+
+     (v: @unchecked) match {
        case cf: CompletableFuture[?] =>
           println("CompletableFuture")
        case f: scala.concurrent.Future[?] =>

shared/src/test/scala/logic/unification1/Unifiable.scala

@@ -90,7 +90,6 @@ object Point {
               yrBindings
             }
           }
-        case _ => failure()
     }
 
   }

shared/src/test/scala/logic/unification1/examples/DBAccess1.scala

@@ -64,6 +64,8 @@ object DBAccess1 {
               or(users.map(u => userFact.unify[R](u, term, bindings)))
             else
               failure()
+          case CheckedLogicalTerm(term, cast, check) =>
+            ???
       }
 
   }
@@ -116,6 +118,10 @@ object DBAccess2 {
               reflect(or(users.map(u => userFact.unify[R](u, term, bindings))))
             else
               reflect(failure())
+          case CheckedLogicalTerm(term, cast, check) =>
+
+              ???
+
       }
 
 
@@ -144,7 +150,7 @@ object DBAccess3 {
         term match
           case lv: LogicalVariable =>
             reflect(asyncOr(collection.asyncFind().map(u => bindings.bind(lv, QueryAllUsers(u)))))
-          case lc@LogicalConstant(value) =>
+          case _ =>
             ??? // logic similar to the previous example
       }
 

shared/src/test/scala/logic/unification2/Access.scala

@@ -0,0 +1,7 @@
+package logic.unification2
+
+trait Access[-T] {
+
+  def get[S<:T]: S
+
+}

shared/src/test/scala/logic/unification2/LogicalTerm.scala

@@ -0,0 +1,45 @@
+package logic.unification2
+
+import logic.CpsLogicMonad
+
+sealed trait LogicalExpression
+
+
+sealed trait LogicalTerm extends LogicalExpression {
+
+   type Type
+   def symbol: Unifiable[Type]
+
+}
+
+object LogicalTerm {
+
+  type Aux[T] = LogicalTerm { type Type = T }
+
+}
+
+sealed trait TypedLogicalTerm[T:Unifiable] extends LogicalTerm {
+
+  type Type = T
+
+  def symbol = summon[Unifiable[T]]
+
+}
+
+case class LogicalVariable[T:Unifiable](id:Long, name: String) extends TypedLogicalTerm[T] 
+
+
+case class LogicalConstant[T:Unifiable](value: T) extends TypedLogicalTerm[T]
+
+
+case class LogicalFunctionalTerm[T:Unifiable](args: IndexedSeq[LogicalTerm]) extends TypedLogicalTerm[T] {
+
+
+
+}
+
+
+
+
+
+

shared/src/test/scala/logic/unification2/Unifiable.scala

@@ -0,0 +1,73 @@
+package logic.unification2
+
+import cps.*
+import logic.CpsLogicMonad
+
+
+trait Unifiable[T]  {
+
+  type Environment[M[_]] <: UnificationEnvironment[M]
+
+  type InstanceData = Any
+
+  def unify[M[_]:Environment](a: M[T], b: M[T])(using data: Access[InstanceData]): M[T]
+
+  def fromTerm(term: LogicalTerm): Option[T]
+
+  def className: String
+
+  lazy val classNameHash: Int = className.hashCode
+
+  // don;t use Environment,  becase when we cast, we don;t have in code exact type of term
+  // and can't deduce Environment.
+  def  castTo[M[_]:UnificationEnvironment, S:Unifiable](t: LogicalTerm): M[TypedLogicalTerm[S]] =
+    if (summon[Unifiable[S]] == this) then
+      summon[UnificationEnvironment[M]].pure(t.asInstanceOf[TypedLogicalTerm[S]])
+    else
+      summon[UnificationEnvironment[M]].mzero
+
+}
+
+object Unifiable {
+
+  given Ordering[Unifiable[?]] with
+    def compare(x: Unifiable[?], y: Unifiable[?]): Int =
+      x.classNameHash - y.classNameHash
+
+  given Equiv[Unifiable[?]] with
+    def equiv(x: Unifiable[?], y: Unifiable[?]): Boolean =
+      x.className == y.className
+
+  given Unifiable[Int] with
+    type Environment[M[_]] = UnificationEnvironment[M]
+
+    override def unify[M[_]:Environment](a: M[Int], b: M[Int])(using data: Access[InstanceData]): M[Int] = reify[M] {
+      a.toTerm match
+        case lc: LogicalConstant[?] => ???
+          /*
+          b.toTerm match
+            case lc2: LogicalConstant[Int] =>
+              if lc2 == lc then reflect(a) else failure[M,Int]
+            case lv: LogicalVariable[Int] =>
+              lv.bind(a.toTerm)
+            case fun: FunctionalTerm[?] =>
+              ???
+
+           */
+
+    }
+
+    override def fromTerm(term: LogicalTerm): Option[Int] = term match
+      case lc: LogicalConstant[?] =>
+        if (lc.symbol == summon[Unifiable[Int]]) then
+          Some(lc.value.asInstanceOf[Int])
+        else
+          None
+      case _ => None
+
+    //override def compare(x: Int, y: Int): Int = x - y
+
+    override def className: String = "Int"
+
+
+}

shared/src/test/scala/logic/unification2/UnificationEnvironment.scala

@@ -0,0 +1,95 @@
+package logic.unification2
+
+import cps.*
+import logic.*
+import logic.CpsLogicMonad
+
+
+trait UnificationEnvironment[M[_]] extends CpsLogicMonad[M] {
+
+  override type Context <: UnificationEnvironmentContext[M]
+
+  def toTerm[A:Unifiable](ma: M[A]): M[TypedLogicalTerm[A]]
+
+  def fromTerm[A:Unifiable](t:TypedLogicalTerm[A]): M[A]
+
+  def bindTerm[A:Unifiable](v:LogicalVariable[A], t:TypedLogicalTerm[A]): M[A]
+
+  def bind[A:Unifiable](v:LogicalVariable[A], ma: M[A]): M[A] 
+
+}
+
+trait UnificationEnvironmentContext[M[_]] extends CpsLogicMonadContext[M] {
+
+  override def monad: UnificationEnvironment[M]
+
+}
+
+extension [M[_],A](ma:M[A])(using env: UnificationEnvironmentContext[M], ua: Unifiable[A])  {
+
+  def _toTerm: M[TypedLogicalTerm[A]] =
+    env.monad.toTerm(ma)
+
+  transparent inline def toTerm: TypedLogicalTerm[A] =
+    reflect(env.monad.toTerm(ma))
+
+}
+
+extension [M[_],A](lv:LogicalVariable[A])(using env: UnificationEnvironmentContext[M], ua: Unifiable[A])  {
+
+  def _bindTerm(t:TypedLogicalTerm[A]): M[A] =
+    env.monad.bindTerm(lv, t)
+
+  transparent inline def bindTerm(t:TypedLogicalTerm[A]): A =
+    reflect(env.monad.bindTerm(lv, t))
+
+  def _bind(ma:M[A]): M[A] =
+    env.monad.bind(lv, ma)
+
+  transparent inline def bind(ma:M[A]): A =
+    reflect(env.monad.bind(lv, ma))  
+
+}
+
+extension [M[_],A](t:TypedLogicalTerm[A])(using ua: Unifiable[A], ctx: UnificationEnvironmentContext[M])  {
+
+  def _fromTerm: M[A] =
+    ctx.monad.fromTerm(t)
+
+  transparent inline def fromTerm: A =
+    reflect(ctx.monad.fromTerm(t))
+
+
+}
+
+
+extension [M[_]](t: LogicalTerm)(using ctx: UnificationEnvironmentContext[M], env: UnificationEnvironment[M])  {
+
+
+  def _castToTerm[S: Unifiable]: M[TypedLogicalTerm[S]] =
+    t.symbol.castTo[M, S](t)
+
+  transparent inline def castToTerm[S: Unifiable]: TypedLogicalTerm[S] =
+    reflect(t.symbol.castTo[M, S](t))
+
+  def castToM[S: Unifiable]: M[S] =
+    ctx.monad.flatMap(t.symbol.castTo[M, S](t))(ctx.monad.fromTerm(_))
+
+
+}
+
+
+transparent inline def failure[M[_],A](using env: UnificationEnvironmentContext[M]): A =
+  reflect(env.monad.mzero[A])
+
+transparent inline def success[M[_],A](a:A)(using env: UnificationEnvironmentContext[M]): A =
+  reflect(env.monad.pure(a))
+
+
+
+object UnificationEnvironment {
+
+
+
+
+}