main

Demonstrates several :solve and :dsl-theory features together in one runnable program: the it.unibo.tuprolog.dsl.theory.logicProgramming DSL block for writing terms/theories/queries with ordinary Kotlin syntax, registering a custom it.unibo.tuprolog.solve.primitive.Primitive (gt) inside a custom it.unibo.tuprolog.solve.library.Library, building a solver with it.unibo.tuprolog.solve.Solver.prolog.solverWithDefaultBuiltins combining that library with an inline static knowledge base, and exhaustively pattern-matching over the three it.unibo.tuprolog.solve.Solution subtypes (Yes, No, Halt) returned while iterating it.unibo.tuprolog.solve.Solver.solve.

The static theory defines user/1 facts for giovanni and lorenzo, plus a rule that would always fail; the query user(X), write("hello: "), write(X), nl, gt(2, 1) asks for every user, prints a greeting for each, and checks the custom gt/2 primitive succeeds for 2 > 1.

Running this example prints, for each solution, either yes: ... with the substitution bindings, no., or halt: ... with the logic stack trace, preceded by the hello: <user> output written by the write/1 and nl/0 standard predicates.