feat(solver): add utility extension method to check and cast the type of solutions

Author: kelvin-olaiya

src/main/scala/io/github/kelvindev15/prolog/solver/Solver.scala

@@ -6,6 +6,8 @@ import io.github.kelvindev15.prolog.solver.Solver.Solution
 import io.github.kelvindev15.prolog.solver.Solver.Solution.{Halt, Yes}
 import io.github.kelvindev15.prolog.solver.tuprolog.TuPrologClassicSolver
 
+import scala.reflect.ClassTag
+
 /** Instances of this trait solve [[PrologProgram]]s. */
 trait Solver:
 
@@ -25,7 +27,8 @@ trait Solver:
     * @return
     *   a lazy list of the program's [[Solution]]s.
     */
-  def lazySolve(program: PrologProgram): LazyList[Solution] = solve(program).to(LazyList)
+  def lazySolve(program: PrologProgram): LazyList[Solution] =
+    solve(program).to(LazyList)
 
   /** Solves a program.
     *
@@ -34,12 +37,27 @@ trait Solver:
     * @return
     *   a list of the program's [[Solution]]s.
     */
-  def solutionsOf(program: PrologProgram): Seq[Solution] = solve(program).to(Seq)
+  def solutionsOf(program: PrologProgram): Seq[Solution] =
+    solve(program).to(Seq)
 
-  def admitsSolutions(program: PrologProgram): Boolean =
+  /** Returns true if the program admits at least one solution.
+    *
+    * @param program
+    *   the program to solve.
+    */
+  def hasSolutionFor(program: PrologProgram): Boolean =
     val solutions = solve(program)
     solutions.hasNext && solutions.next().isInstanceOf[Solution.Yes]
 
+  /** Returns true if the provided goal admits at least one solution.
+    *
+    * @param goal
+    *   the program to satisfy.
+    */
+  def hasSolutionFor(goal: Term): Boolean =
+    val solutions = solve(PrologProgram.emptyTheory withGoal goal)
+    solutions.hasNext && solutions.next().isInstanceOf[Solution.Yes]
+
 object Solver:
   /** A mapping from [[Variable]]s to [[Term]]s */
   type Substitution = Map[Variable, Term]
@@ -64,6 +82,52 @@ object Solver:
       */
     case Halt(exception: Exception)
 
+  extension (solution: Solution)
+    def apply(variable: Variable): Option[Term] = solution match
+      case y: Solution.Yes => Some(y.substitution(variable))
+      case _               => None
+
+    /** Returns true if the solution is a [[Yes]]. */
+    def isYes: Boolean = solution.isInstanceOf[Solution.Yes]
+
+    /** Returns true if the solution is a [[No]]. */
+    def isNo: Boolean = solution.isInstanceOf[Solution.No]
+
+    /** Returns true if the solution is a [[Halt]]. */
+    def isHalt: Boolean = solution.isInstanceOf[Solution.Halt]
+
+    /** Cast the solution to a [[Solution]] of type [[T]].
+      *
+      * @tparam T
+      *   the type of the expected solution
+      *
+      * @throws ClassCastException
+      *   if [[T]] is not the runtime type of the solution.
+      */
+    def as[T <: Solution](using ClassTag[T]): Solution =
+      solution.asInstanceOf[T]
+
+    /** Cast the solution to a [[Yes]] [[Solution]].
+      *
+      * @throws ClassCastException
+      *   if [[Yes]] is not the runtime type of the solution.
+      */
+    def asYes: Solution = solution.as[Solution.Yes]
+
+    /** Cast the solution to a [[No]] [[Solution]].
+      *
+      * @throws ClassCastException
+      *   if [[No]] is not the runtime type of the solution.
+      */
+    def asNo: Solution = solution.as[Solution.No]
+
+    /** Cast the solution to a [[Halt]] [[Solution]].
+      *
+      * @throws ClassCastException
+      *   if [[Halt]] is not the runtime type of the solution.
+      */
+    def asHalt: Solution = solution.as[Solution.Halt]
+
   /** Returns a Solver that leverages on the tuProlog engine. */
   def tuPrologSolver(): Solver = TuPrologClassicSolver()
 
@@ -147,22 +211,26 @@ object Solver:
   ): LazyList[Solution] =
     solver lazySolve (PrologProgram.emptyTheory withGoal query)
 
-  /** Returns true if the program admits at least one solution.
-   *
-   * @param solver the solver that should be used.
-   * @param program the program to solve.
-   */
+  /** Returns true if the program admits at least one solution. If not specified
+    * the default solver that will be used is the [[TuPrologClassicSolver]].
+    *
+    * @param solver
+    *   the solver that should be used.
+    * @param program
+    *   the program to solve.
+    */
   def hasSolutionForProgram(using solver: Solver = tuPrologSolver())(
-    program: PrologProgram
-  ): Boolean =
-    val solutions = solve(program)
-    solutions.hasNext && solutions.next().isInstanceOf[Solution.Yes]
+      program: PrologProgram
+  ): Boolean = solver hasSolutionFor program
 
-  /** Returns true if the program admits at least one solution.
-   *
-   * @param solver  the solver that should be used.
-   * @param goal the program to satisfy.
-   */
+  /** Returns true if the provided goal admits at least one solution. If not
+    * specified the default solver that will be used is the
+    * [[TuPrologClassicSolver]].
+    * @param solver
+    *   the solver that should be used.
+    * @param goal
+    *   the program to satisfy.
+    */
   def hasSolutionForGoal(using solver: Solver = tuPrologSolver())(
-    goal: Term
-  ): Boolean = hasSolutionForProgram(PrologProgram.emptyTheory withGoal goal)
+      goal: Term
+  ): Boolean = solver hasSolutionFor goal

src/main/scala/io/github/kelvindev15/prolog/solver/tuprolog/TuPrologClassicSolver.scala

@@ -48,7 +48,7 @@ private[tuprolog] object ConversionsUtils:
     _.asScala.map(identity)
 
 /** A [[Solver]] that leverages on the tuProlog engine */
-class TuPrologClassicSolver extends Solver:
+private[solver] class TuPrologClassicSolver extends Solver:
   import ConversionsUtils.given
 
   private def classicSolverOf(

src/test/scala/io/github/kelvindev15/prolog/solver/engine/TestPrologEngine.scala renamed to src/test/scala/io/github/kelvindev15/prolog/solver/engine/PrologEngineSpec.scala

@@ -1,18 +1,19 @@
 package io.github.kelvindev15.prolog.solver.engine
 
 import io.github.kelvindev15.prolog.PrologProgram
-import io.github.kelvindev15.prolog.core.{PrologList, Term}
+import io.github.kelvindev15.prolog.core.{Constant, PrologList, Term}
 import io.github.kelvindev15.prolog.dsl.{DeclarativeProlog, PrologDSL}
 import io.github.kelvindev15.prolog.solver.Solver
 import io.github.kelvindev15.prolog.solver.Solver.Solution
 import io.github.kelvindev15.prolog.solver.engine.utils.EngineTestUtils
 import org.scalatest.flatspec.AnyFlatSpec
+import org.scalatest.funsuite.AnyFunSuite
 import org.scalatest.matchers.should.Matchers
 
 import scala.reflect
 import scala.reflect.ClassTag
 
-class TestPrologEngine
+class PrologEngineSpec
     extends AnyFlatSpec
     with Matchers
     with EngineTestUtils
@@ -66,3 +67,24 @@ class TestPrologEngine
     " with at least one solution" in:
     assert(!(Solver hasSolutionForGoal member("notInList", list(1, 2, 4))))
     assert(Solver hasSolutionForGoal member("b", list("a", "b", "c", 1)))
+
+class TestPrologEngine extends AnyFunSuite with Matchers with PrologDSL with DeclarativeProlog:
+  test("Access to substitutions of Yes/No solutions"):
+    val solutions = Solver query member(X, list(1, 2, 3))
+    assert(solutions.hasNext)
+    val first = solutions.next()
+    assert(first.isYes)
+    first.asYes(X) shouldBe Some(Constant(1))
+    { solutions.next(); solutions.next() }
+    assert(solutions.hasNext)
+    val last = solutions.next()
+    assert(last.isNo)
+    last.asNo(X) shouldBe None
+
+  test("Access to substitutions of Halt solutions"):
+    val solutions = Solver query (X is Y)
+    assert(solutions.hasNext)
+    val theSolution = solutions.next()
+    assert(theSolution.isHalt)
+    theSolution.asHalt(X) shouldBe None
+    

src/test/scala/io/github/kelvindev15/prolog/solver/engine/TestBuiltins.scala

@@ -138,4 +138,4 @@ class TestBuiltins
 
   test("Test operators"):
     expectOne[Solution.Yes]:
-      Solver query (&&(X `=` 3, 2 < X))
+      Solver query &&(X `=` 3, 2 < X)

src/test/scala/io/github/kelvindev15/prolog/solver/engine/utils/EngineTestUtils.scala

@@ -1,6 +1,5 @@
 package io.github.kelvindev15.prolog.solver.engine.utils
 
-import io.github.kelvindev15.prolog.PrologProgram
 import io.github.kelvindev15.prolog.core.{Struct, Term, Variable}
 import io.github.kelvindev15.prolog.solver.Solver
 import io.github.kelvindev15.prolog.solver.Solver.Solution.Yes