cram_reasoning

The package cram_reasoning contains a full-featured Prolog interpreter completely written in Common Lisp. In contrast to other Prolog variants it is specifically designed for programmatic use. Instead of returning one solution and waiting for user input as a Prolog shell does, the Prolog interpreter returns a lazy list of solutions that are generated on demand by accessing elements of this lazy list.

The package provides the Lisp function prolog to execute the interpreter and prove a goal. The following example demonstrates its use:

CRS> (prolog `(member ?x (a b c))
(((?X . 1)) . #S(CRAM-UTILITIES::LAZY-CONS-ELEM :GENERATOR #<CLOSURE # {10029F487B}>))

This call generates a lazy list over the solutions and the only the first solution is generated by this call. By expanding the lazy list using the function force-ll, all solutions can be generated. The result looks like this:

CRS> (force-ll (prolog `(member ?x (a b c))))
(((?X . 1)) ((?X . 2)) ((?X . 3)))

As can be seen, the result is a list of sets of bindings. Each set of bindings is a list containing tuples (i.e. cons cells) with the variable name in its car and the corresponding value in its cdr. For accessing variables, the function var-value and the macro with-vars-bound are provided. The following example shows the use of var-value:

CRS> (var-value '?x (lazy-car (prolog `(member ?x (a b c)))))
A

Alternatively, with-vars-bound can be used. It binds the specified variables lexically when executing the body:

CRS> (with-vars-bound (?x) (lazy-car (prolog `(member ?x (a b c))))
       ?x)
A

The cram_reasoning package provides two ways of defining predicates. The first one is using fact-groups. The second is implementing a lisp function that gets the current bindings and the predicate's parameters and returns a list of binding sets.

To allow for easy re-compilation in an interactive development environments, predicates are grouped together in fact groups. When a fact-group is recompiled, it completely replaces its previous definition. That way, it is possible to define and re-define predicates interactively.

Fact groups are defined with the macro

def-fact-group name (public-predicate*) fact-definiton*

The public-predicate field is used to declare which predicates can be defined in other fact-groups as well. This is mainly for improving code robustness because the user needs to explicitly declare which predicates can be defined elsewere, too. This prevents a common error where users defined predicates at multiple locations accidentally.

Predicates are defined as fact-definition using ←.

The following example shows the definition of the member predicate:

(def-fact-group member-group ()
  (<- (member ?x (?x . ?_))
  (<- (member ?x (?y . ?z)
    (member ?x ?z))

For easy integration with Common Lisp and for the implementation of optimized predicates, the system provides so-called Prolog handlers. A Prolog handler is a lisp function that gets the current environment (i.e. bindings) and the values of the predicate variables and returns a list of binding sets. The predicate format that is used for printing debug info on the screen can be implemented as follows:

(def-prolog-handler format (bdgs ?string &rest args)
  (let ((string (var-value ?string bdgs))
        (substituted-args (mapcar (lambda (arg) (var-value arg bdgs)) args)))
    (declare (type string string))
    (apply #'format t string args)
    (list bdgs)))

Since the variables passed to the handler can be bound to variables, the actual variable values are read using var-value. Then format is called and since this predicate always holds, the list of unchanged bindings is returned.

If both, a Prolog handler and fact group define a predicate, the fact group predicate is only used if the Prolog handler fails.

For easier integration of Common Lisp, two helper predicates are provided: lisp-fun and lisp-pred. lisp-fun allows to call a lisp function and bind its result to a Prolog variable while lisp-pred can be used to use a lisp predicate function. If the predicate function returns NIL, the lisp-pred predicate will fail.

lisp-fun can be used as follows:

CRS> (lazy-car (prolog `(lisp-fun symbol-value *package* ?p)))
((?P . #<PACKAGE "CRAM-REASONING">))

As can be seen, the result of the call to symbol-value is bound to the variable ?p.

The following example shows the use of lisp-pred to compare two variables using equal:

(lisp-pred equal ?a ?b)

The predicate only holds when the lisp function returns non-NIL.