|
| 1 | +package io.github.kelvindev15.prolog.engine |
| 2 | + |
| 3 | +import io.github.kelvindev15.prolog.PrologProgram |
| 4 | +import io.github.kelvindev15.prolog.core.{Struct, Term, Variable} |
| 5 | +import io.github.kelvindev15.prolog.core.Theory.Theory |
| 6 | +import io.github.kelvindev15.prolog.engine.Solver.Solution |
| 7 | +import io.github.kelvindev15.prolog.engine.Solver.Solution.{Halt, Yes} |
| 8 | +import io.github.kelvindev15.prolog.engine.visitors.{BackVisitor, TuPKtTermVisitor} |
| 9 | +import it.unibo.tuprolog.core.{Clause as KClause, Struct as KStruct, Substitution as KSubstitution, Term as KTerm} |
| 10 | +import it.unibo.tuprolog.solve.Solver as KSolver |
| 11 | +import it.unibo.tuprolog.solve.channel.{InputStore, OutputStore} |
| 12 | +import it.unibo.tuprolog.solve.classic.ClassicSolverFactory |
| 13 | +import it.unibo.tuprolog.solve.flags.FlagStore |
| 14 | +import it.unibo.tuprolog.theory.Theory as KTheory |
| 15 | +import it.unibo.tuprolog.unify.Unificator |
| 16 | +import it.unibo.tuprolog.solve.Solution as KSolution |
| 17 | + |
| 18 | +trait Solver: |
| 19 | + def solve(program: PrologProgram): Iterator[Solution] |
| 20 | + |
| 21 | +import scala.jdk.CollectionConverters.* |
| 22 | + |
| 23 | +object Solver: |
| 24 | + type Substitution = Map[Variable, Term] |
| 25 | + enum Solution: |
| 26 | + case Yes(query: Struct, substitution: Substitution) |
| 27 | + case No(query: Struct) |
| 28 | + case Halt |
| 29 | + |
| 30 | + private val visitor = TuPKtTermVisitor() |
| 31 | + private val back = BackVisitor() |
| 32 | + given Conversion[Term, KTerm] = _.accept(visitor) |
| 33 | + given Conversion[KTerm, KClause] = _.asClause() |
| 34 | + given Conversion[KTerm, KStruct] = _.asStruct() |
| 35 | + given Conversion[Theory, KTheory] with |
| 36 | + override def apply(theory: Theory): KTheory = KTheory.of(theory.map(_.asClause()) *) |
| 37 | + given Conversion[KStruct, Struct] = back.visitStruct(_) |
| 38 | + given Conversion[KSubstitution, Substitution] = { |
| 39 | + case substitution: KSubstitution.Unifier => Map( |
| 40 | + substitution.asScala.toSeq.map(p => (back.visitVar(p._1), back.visitTerm(p._2)))* |
| 41 | + ) |
| 42 | + } |
| 43 | + given Conversion[KSolution, Solution] = { |
| 44 | + case yes: KSolution.Yes => Yes(yes.getQuery, yes.getSubstitution) |
| 45 | + case no: KSolution.No => Solution.No(no.getQuery) |
| 46 | + case halt: KSolution.Halt => Halt |
| 47 | + } |
| 48 | + given Conversion[java.util.Iterator[KSolution], Iterator[Solution]] = _.asScala.map(identity) |
| 49 | + |
| 50 | + private def tuPrologClassicSolverOf(staticTheory: Theory, dynamicTheory: Theory): KSolver = |
| 51 | + ClassicSolverFactory.INSTANCE.solverOf( |
| 52 | + Unificator.getDefault, |
| 53 | + ClassicSolverFactory.INSTANCE.getDefaultRuntime, |
| 54 | + FlagStore.DEFAULT, |
| 55 | + staticTheory, |
| 56 | + dynamicTheory, |
| 57 | + InputStore.fromStandard(), |
| 58 | + OutputStore.fromStandard() |
| 59 | + ) |
| 60 | + |
| 61 | + def tuPrologSolver(): Solver = (program: PrologProgram) => |
| 62 | + val solver = tuPrologClassicSolverOf(program.dynamicTheory, program.staticTheory) |
| 63 | + program.goal.map { goal => solver.solve(goal.asStruct()).iterator() }.get |
0 commit comments