How to translate this 2p-specific code in 2p-kt?

[enrdenti]

Issue: How to convert old-fashioned Java code for classic 2p into newer Java (perhaps Kotlin) code for 2p-kt

What is needed: the equivalent of basic methods to instantiate a prolog engine and use it from Java (kotlin), such as in the following snapshot:

Prolog engine = new Prolog(); 
Theory t = new Theory(new FileInputStream("exp_parser.pl"));
engine.setTheory(t);
SolveInfo info = engine.solve("evalExpr(" + prologInputString + ",Result).");
if (info.isSuccess()) { Term resultTerm = info.getTerm("Result");  …}

[gciatto]

Hello @enrdenti.

Here's a complete rewrite of your code.

There are a couple of things to be taken into account:

1. you need to have at least modules :solve-classic and :parser-theory (as well as their direct and indirect dependencies) in your classpath, as you need both resolution facilities (term representation + unification + theories + resolution) and parsing facilities (for both terms and theories)

   • hence, if you manage dependencies with Gradle (like I do here you may be willing to add the following section:

   dependecies {
       implementation("it.unibo.tuprolog:solve-classic-jvm:$tuprologVersion")
       implementation("it.unibo.tuprolog:parser-theory-jvm:$tuprologVersion")
   }

2. you have to keep in mind the following conceptual map:

   • There is no Prolog class anymore, there's a new unified interface for all solvers: Solver
   • Solvers are created via some SolverFactory
   • There may exist several sorts of Solvers, hence as many sorts of SolverFactorys
     • the "classic" solver is the one working similarly to 2P's Prolog engines
   • In any case solvers can be either Solvers (unmodifiable interface) or MutableSolvers (modifiable interface)
     • unmodifiable solvers (i.e. instances ofSolver) expose no method to vary their internal status (e.g. dynamic KB, flags, etc.), yet such status may still vary as a by-product of Prolog queries being executed
     • modifiable solvers (i.e. instances ofMutableSolver) expose many methods to vary their internal status (e.g. dynamic KB, flags, etc.) from Java
     • notice that MutableSolver is a sub-type of Solver
   • To instantiate a Solver you must instantiate a SolverFactory first
     • you can instantiate a SolverFactory for "classic" Solvers via either Solve.getClassic or ClassicSolverFactory.INSTANCE
   • Each instance of SolverFactory comes with several methods to instantiate Solvers with, namely:
     • factory.solverOf(...) creating an empty (i.e. with no built-in) and unmodifiable Solver instance
     • factory.solverWithDefaultBuiltins(...) creating an unmodifiable Solver instance with default Prolog builtins
     • factory.mutableSolverOf(...) creating an empty (i.e. with no built-in) and modifiable instance of MutableSolver
     • factory.mutableSolverWithDefaultBuiltins(...) creating an instance of MutableSolver with default Prolog builtins
     • notice that all such methods come with several overloads letting the caller specify initialization aspects of the to-be-created solvers (e.g. static KB, flags, input/output/warning channels etc.)
   • So, if you create a Solver, the Theory must be provided as an argument upon creation, whereas if you create a MutableSolver the static KB can be edited even after the solver has been instantiated
     • hence, there is no equivalent of .setTheory(...) on Solvers, while there is .loadStaticKB(...) on MutableSolvers

3. concerning parsing, keep in mind that
   -Theorys and Terms are just immutable data structures

   • They can be either parsed from a string or read a file via the following classes:
     • TermParser whose instances aim at parsing single terms (or structs, or whatever) from in-memory strings
     • TermReader whose instances aim at reading single terms (or structs, or whatever) from input streams or readers (which may be files, sockets, or in-memory buffers)
     • ClausesParser whose instances aim at parsing sequences of clauses (or theories) from in-memory strings, either lazily or eagerly
     • TermReader whose instances aim at parsing sequences of clauses (or theories) from input streams or readers (which may be files, sockets, or in-memory buffers), either lazily or eagerly
   • Notice that all such types must be constructed out of an OperatorSet, which specifies which symbols should be considered as operators while parsing (and with which associativity and priority)
     • static factory methods are available to create readers/parsers out of default Prolog operators

4. notice that, because of the single responsibility principle, it is not Solvers' responsibility to perform parsing of queries

   • hence there is no solve method accepting a string as query
   • the query Struct must be parsed before calling the solver's solve method, via some TermParser

5. notice that there is no such a notion like 2P's SolveInfo: Solvers' solve method returns a Sequence of Solutions

   • Solution is an interface, and it is the base type for all logic solutions
     • it comes with three subtypes: Solution.Yes for successful answers, Solution.No for negative answers, and Solution.Halt for exceptions
     • by testing the type of a Solution via instanceof one may figure out what situation is at hand
     • by casting a Solution to the most adequate subtype, one may access relevant information, such as the resolving Substitution (from which variable bindings can be retrieved) of a Solution.Yes or the exception which caused a Solution.Halt
   • Sequences<T> are (possibly lazy) streams of data of type T
     • they can be conveniently handled in Kotlin via extension methods
     • in Java they could be converted into instances of Stream (cf. https://kotlinlang.org/api/latest/jvm/stdlib/kotlin.streams/kotlin.sequences.-sequence/as-stream.html)...
     • ... or iterated via the iterator pattern:

      Iterator<Solution> si = solver.solve(….).iterator();
      while (si.hasNext() {
          Solution solution = si.next();
          // handle solution here
      }

6. notice that there is a convenient abstraction: SolutionFormatter which aims at converting solutions into presentable strings

   • hence if you plan to show your solver's solutions to the user you may consider implementing your own SolutionFormatter or use some default implementation instead

[gciatto]

So, the first alternative is far more clear. Yet, the second could be viable, effective and intuitive if moved into the SolverFactory class.

I disagree. It is a common practice in JVM-based languages, when one has the X, XFactory and/or XBuilder types to allow the instantiation of factories or builders from the "main" type -- X, in my example -- via ad-hoc static methods.

[gciatto]

As concerns the operator handling: I do appreciate that operator directives are handled automatically in solvers, and also appreciate that TermParser is both conceptually and physically separate entity. However, putting the two aspects together, usability can become somehow counter-intuitive, in that if the user means to parse terms (typically, queries) to be submitted to a solver that includes some user-defined operators, having to re-define such operators in the TermParser is weird. Moreover, for the solver to work, I guess it internally does instantiate and use a TermParser with the suitable operator set already in place. So, why not just make that TermParser accessible, providing a method such as solver.getTermParser? That would be straightforward (and also avoid duplicating the parser object): one would just re-use the inherently correct term parser, borrowed from the solver.

No, your guess is not correct, this time :)
Solvers hide no parser behind the scenes, and this is not only intended but strictly enforced.
The rationale behind this choice is, once again, the single responsibility principle: Solvers are not in charge of parsing terms, nor theories.
Indeed, one can only either create a Solver out of an already-parsed Theory, or load an already-parsed Theory into an already created MutableSolver. In both cases, the Theory must be parsed/read externally w.r.t. the Solver.

More generally, if you look carefully at the project map, you will notice that there is no direct dependency among any :solver-* and any :parser-* module.
This is deliberate.
The goal is to make it difficult for the people developing 2P-Kt (or some new module in the ecosystem) to abuse the exploitation of the parser, unless strictly necessary.
This, in turn, is aimed at avoiding core functionalities (e.g. resolution, and the Prolog standard builtins) to use the parser behind the scenes, which would imply potential inefficiencies.
(I really wanted to avoid some errors which I found in the implementation of 2P-Java, a few years ago, such as cloning terms by converting them into strings and parsing them back)

Of course, there exist standard IO builtins that technically require parsing, such as consult/1, or read*/N.
These are indeed placed into the io-lib module which does rely on the parser behind the scenes.

So, long story short, if you need a quick way to create a TermParser out of a Solver, you can simply create your own utility method, such as:

public static TermParser termParserFor(Solver solver) {
    return TermParser.withOperators(solver.getOperators);
}

public static Struct parseGoal(Solver solver, String string) {
    return termParserFor(solver).parseStruct(string);
}

public static Sequence<Solution> solve(Solver solver, String query, SolveOptions options) {
    return solver.solve(parseGoal(query), options);
}

public static Sequence<Solution> solve(Solver solver, String query) {
    return solve(solver, query, SolveOptions.DEFAULT);
}

This solution would of course imply the creation of several TermParsers... yet don't worry: TermParsers are very lightweight objects, and they can be created very quickly.

[enrdenti]

I possibly mis-explained my point, sorry. The fact is that solvers do interpret the :-op/3 directives, as you mentioned; and they do so by loading a theory, which - then - must have already been parsed. Your example actually does so via the theoryReader object, which is an instance of ClausesReader (with default operators, btw). So, I possibly spoke about "term parsers" when should have said "clauses reader", but as a matter of fact it seems someone there does parse :-op/3 and the theory, which is then passed to the solver (and I do agree with the separation). Correct?

[gciatto]

Yes, you're correct.

There are 2 disjoint, yet interrelated, mechanisms here:

1. ClausesReaders and ClausesParsers can consider :- op/3 directives while reading/parsing, adding the corresponding operators to the set of operators used for reading/parsing the remainder of the file. The result is usually a theory containing a Directive object, which is a particular case of Clause
2. Solvers have their own set of operators as part of their internal state. This is accessible via Solver.getOperators(). It may evolve because of queries being solved. However, a Solver's operator set is initialised by merging:
   • all operators explicitly declared by each library loaded into that Solver (in the case of Prolog standard builtin libraries, this means the whole set of Prolog standard operators)
   • all operators implicitly declared in the Solver's static and dynamic KBs (which are Theorys), as :- op/3 directives

[enrdenti]

perfect! crystal clear now