swipl

Bindings to SWI-Prolog for OCaml
IN THIS PACKAGE
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 t

t [@@deriving eq, ord, show] represents prolog 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 fn

fn [@@deriving eq, ord] represents function symbols.

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 characters name.

Note: If you call this function before initialise you will segfault.

type module_

module_ [@@deriving eq, ord] represents SWI-prolog modules.

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 `Closeing the query (dropping all bindings), or `Cutting 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 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.

val call : ctx -> t -> unit

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.

val eval : ctx -> t -> query

eval ctx term send the prolog term term 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 list ls.

val encode_string : ctx -> string -> t

encode_string ctx str returns a prolog term representing the string str.

val fresh : ctx -> t

fresh ctx creates a new prolog variable that lasts for the scope of ctx.

val extract_list : ctx -> t -> t list

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.

val extract_atom : ctx -> t -> atom

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.

val extract_bool : ctx -> t -> bool

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.

val extract_int : ctx -> t -> int

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.

val extract_float : ctx -> t -> float

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.

val extract_string : ctx -> t -> string

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.

val extract_functor : ctx -> t -> atom * t list

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.

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 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.