Module Swipl
val initialise : unit -> unit
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
type query
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.
type ctx
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.
type atom
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 charactersname
.Note: If you call this function before
initialise
you will segfault.
val module_ : string -> module_
module_ name
returns a reference to the module with namename
.
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 callsfn
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).
val iter_solutions : ?on_error:(t -> unit) -> query -> (unit -> unit) -> bool
iter_solutions ?on_error qid fn
callsfn
once for each solution returned by the queryqid
, 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 queryqid
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 queryqid
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.
val call : ctx -> t -> unit
call ctx term
runs the query represented byterm
, 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 contextctx
and callsfn
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.
val eval : ctx -> t -> query
eval ctx term
send the prolog termterm
to the prolog engine and returns a handle to the query.
val encode_list : ctx -> t list -> t
encode_list ctx ls
returns a prolog term representing the listls
.
val encode_string : ctx -> string -> t
encode_string ctx str
returns a prolog term representing the stringstr
.
val extract_list : ctx -> t -> t list
extract_list ctx t
extracts a list of prolog terms fromt
.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.
val extract_atom : ctx -> t -> atom
extract_atom ctx t
extracts an atom fromt
.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.
val extract_bool : ctx -> t -> bool
extract_bool ctx t
extracts a bool fromt
.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.
val extract_int : ctx -> t -> int
extract_int ctx t
extracts an int fromt
.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.
val extract_float : ctx -> t -> float
extract_float ctx t
extracts a float fromt
.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.
val extract_string : ctx -> t -> string
extract_string ctx t
extracts a string fromt
.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.
val extract_functor : ctx -> t -> atom * t list
extract_int ctx t
extracts a compound term or atom fromt
.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.
val typeof : t -> ty
typeof t
returns the type of term t.Note: If you call this function before
initialise
you will segfault.
val load_source : string -> unit
load_source src
loadssrc
as prolog source code (i.e not a file) into the prolog engine.Note: If you call this function before
initialise
you will segfault.