Library
Module
Module type
Parameter
Class
Class type
initialise ()
initialises the SWI-prolog engine. It must be called at the start of the program before creating any terms.
type ty = [
| `Atom
| `Blob
| `Bool
| `Dict
| `Float
| `Integer
| `ListPair
| `Nil
| `Rational
| `String
| `Term
| `Variable
]
Represents types of prolog terms
Represents an in-progress prolog query.
Note: It is an error to run another query before the result of a prior query has been consumed.
Represents a term context - all terms are tied to a given context, and are discarded when the context ends. It is undefined behaviour to manipulate a term that has been freed, so make sure to extract any relevant terms to OCaml before the context is discarded.
Represents atoms in prolog. This is an internal type that is primarily exposed for performance reasons - in particular, comparing whether two atoms : atom
are equal will be faster than comparing if two terms : t
are equal.
val atom : string -> atom
atom name
constructs an atom with characters name
.
Note: If you call this function before initialise
you will segfault.
val module_ : string -> module_
module_ name
returns a reference to the module with name name
.
val fold_solutions :
([> `Exception of t | `Last | `Solution ] -> [< `Close | `Cut ] option) ->
query ->
bool
fold_solutions fn qid
is the most general combinator for consuming the output of Prolog queries. It calls fn
once for each solution to the query (or exception raised by the query), and allows the function to terminate early by either `Close
ing the query (dropping all bindings), or `Cut
ting the query (and keeping the bindings introduced by the current result). The function returns a boolean representing whether there were any results or not.
For many cases you probably don't need the generality of this combinator, and can get away with using one of the simpler wrappers we provide (see below).
iter_solutions ?on_error qid fn
calls fn
once for each solution returned by the query qid
, and returns true if there were any solutions at all. on_error
is called with any exception terms that are raised by the query (if any).
val first_solution : query -> bool
first_solution qid
consumes the query qid
and preserves the bindings from the first solution to the query. The function returns a boolean representing whether there were any solutions or not.
raises Failure if the prolog query raises an exception.
val last_solution : query -> bool
last_solution qid
consumes the query qid
and preserves the bindings from the last solution to the query. The function returns a boolean representing whether there were any solutions or not.
raises Failure if the prolog query raises an exception.
call ctx term
runs the query represented by term
, preserving the bindings produced by the first solution if the query succeeds at all (does not check if the query succeeds at all).
raises Failure if the prolog query raises an exception.
module Syntax : sig ... end
The Syntax
module provides a useful set of combinators for constructing prolog terms using idiomatic OCaml syntax.
val with_ctx : (ctx -> 'a) -> 'a
with_ctx fn
creates a new term context ctx
and calls fn
with that context.
Note: Any terms created within the context will be dropped at the end of this function - it is undefined behaviour to try and escape prolog terms out of fn
. (You have been warned, nasal demons at the ready).
Note: If you call this function before initialise
you will segfault.
eval ctx term
send the prolog term term
to the prolog engine and returns a handle to the query.
encode_list ctx ls
returns a prolog term representing the list ls
.
encode_string ctx str
returns a prolog term representing the string str
.
extract_list ctx t
extracts a list of prolog terms from t
.
Note: It is undefined behaviour to call this function on a term that is not a list. If in doubt, check the type of the term with typeof
first.
extract_atom ctx t
extracts an atom from t
.
Note: It is undefined behaviour to call this function on a term that is not an atom. If in doubt, check the type of the term with typeof
first.
extract_bool ctx t
extracts a bool from t
.
Note: It is undefined behaviour to call this function on a term that is not a bool. If in doubt, check the type of the term with typeof
first.
extract_int ctx t
extracts an int from t
.
Note: It is undefined behaviour to call this function on a term that is not an int. If in doubt, check the type of the term with typeof
first.
extract_float ctx t
extracts a float from t
.
Note: It is undefined behaviour to call this function on a term that is not a float. If in doubt, check the type of the term with typeof
first.
extract_string ctx t
extracts a string from t
.
Note: It is undefined behaviour to call this function on a term that is not a string. If in doubt, check the type of the term with typeof
first.
extract_int ctx t
extracts a compound term or atom from t
.
Note: It is undefined behaviour to call this function on a term that is not a functor or atom. If in doubt, check the type of the term with typeof
first.
typeof t
returns the type of term t.
Note: If you call this function before initialise
you will segfault.
load_source src
loads src
as prolog source code (i.e not a file) into the prolog engine.
Note: If you call this function before initialise
you will segfault.