Module Term

module Term: sig .. end

Term representation and operations on terms.

Term representation and operations roughly follow the implementation in the OTTER theorem prover.

Term Structure

type variable

Different occurences of the same variable are not shared as objects. They are identified by their variable_number.

type symbol

A symbol corresponds to a constant or functor symbol along with its arity. Object identity (i.e. '==') is used as symbol identifier.

type compound

type term =

`\|`	`Variable of variable`
`\|`	`Constant of symbol`
`\|`	`Compound of compound`
`\|`	`Integer of int`
`\|`	`Float of float`
`\|`	`Unbound`

val make_variable : int -> variable

val variable_number : variable -> int

val gensym : unit -> symbol

gensym () returns a newly generated symbol that is not maintained by a symbol table.

val symbol_name : symbol -> string

val symbol_arity : symbol -> int

val make_compound : symbol -> term array -> compound

val compound_functor : compound -> symbol

val compound_args : compound -> term array

Symbol Table

type symbol_table

Symbols are maintained by a symbol table.

val make_symbol_table : unit -> symbol_table

Create a symbol table.

val find_symbol : symbol_table -> string -> int -> symbol

find_symbol name arity returns the symbol corresponding to name and arity in the symbol table. If no such symbol is in the table, one is created and put into the table.

val symbol_table_iter : (symbol -> unit) -> symbol_table -> unit

Iterate over the symbols in the symbol table.

Symbols for Logic Operators

val get_meta_functor_symbol : symbol_table -> symbol

val get_rule_symbol : symbol_table -> symbol

val get_disjunction_symbol : symbol_table -> symbol

val get_conjunction_symbol : symbol_table -> symbol

val get_true_symbol : symbol_table -> symbol

val get_false_symbol : symbol_table -> symbol

val get_stratified_neg_as_failure_symbol : symbol_table -> symbol

val get_stratified_neg_as_failure_alternate_symbol : symbol_table -> symbol

val get_stratified_neg_as_failure_not_subsumed_symbol : symbol_table -> symbol

val get_findall_symbol : symbol_table -> symbol

val get_neg2_symbol : symbol_table -> symbol

val set_meta_functor_symbol : symbol_table -> symbol -> unit

val set_rule_symbol : symbol_table -> symbol -> unit

val set_disjunction_symbol : symbol_table -> symbol -> unit

val set_conjunction_symbol : symbol_table -> symbol -> unit

val set_true_symbol : symbol_table -> symbol -> unit

val set_false_symbol : symbol_table -> symbol -> unit

val set_stratified_neg_as_failure_symbol : symbol_table -> symbol -> unit

val set_stratified_neg_as_failure_alternate_symbol : symbol_table -> symbol -> unit

val set_stratified_neg_as_failure_not_subsumed_symbol : symbol_table -> symbol -> unit

val set_findall_symbol : symbol_table -> symbol -> unit

val set_neg2_symbol : symbol_table -> symbol -> unit

Context

type context

A context is used to represent undoable variable bindings within a term.

With a context, a so called multiplier is associated. It is used to distinguish variables from different terms when applying a substitution. (See also the OTTER implementation.)

val max_vars : int

LIMIT: The maximum number of distinct variables in a clause.

exception Max_vars_exceeded

Thrown if the maximum number of distinct variables in a clause is exceeded.

val make_context : int -> context

Create a context. The int argument is the multiplier, i.e. an integer >= 0, of the context.

val null_context : context

A context that represents the empty binding. It is allowed as argument only where explicitely specified.

val context_multiplier : context -> int

Returns the multiplier of the given context.

val dereference : term -> context -> term * context

If term is a variable, dereference_term term context returns its binding in context along with the context too look up bindings in subterms, otherwise the input is returned. This function is not called recursively, i.e. a returned term may contain bound variables.

context may be null_context.

Trail

type trail

A trail is used to record variable bindings, that may be undone. Also, a special instance of type trail is used to represent unification failure.

val make_trail : unit -> trail

make_trail returns an empty trail that is different from fail.

val fail : trail

fail represents unification failure. This object is identified with the failed function.

val failed : trail -> bool

failed trail tests if the given trail is fail.

type saved_trail

A representation of a trail state, that can be used to undo bindings.

val save_trail : trail -> saved_trail

save_trail trail returns a representation of the given trail's state, that can be used to undo bindings.

val undo_bindings : trail -> saved_trail -> trail

undo_bindings trail saved_trail undoes bindings in trail until the state represented by saved_trail is reached. The given trail may be destructively modified by the implementation.

Returns fail.

Term Operations

val unify : term ->
       context -> term -> context -> trail -> trail

unify term1 context1 term2 context2 attempts to unify term1 in context1 with term2 in context2. If unification succeeds, the contexts may be modified and the resulting trail is returned. If the unification fails, fail is returned and the contexts have the same state as before.

val apply : term -> context -> term

apply term context returns a copy of term with the substitution context applied.

val copy_term : term -> term

copy_term returns a copy of term.

val match_terms : term -> context -> term -> trail -> trail

match_terms term1 context1 term2 trail computes the substitution context1 under which term2 is an instance of term1.

Both terms may not share variables.

Variables in term2 must be uninstantiated.

context1 must be fresh or modified by calls to match_terms only (and no call to unify (???)).

Similar as in unify, if the matching succeeds, the resulting trail is returned. If the matching fails, the context has the same state as before and fail is returned.

val subsumes_chk : term -> term -> bool

subsumes_chk term1 term2 is true iff term2 is an instance of term1.

Both terms may not share variables.

val variant : term -> term -> bool

variant term1 term2 is true iff both terms are variants.

Both terms may not share variables.

val term_ident : term -> term -> bool

term_ident term1 term2 returns true iff both terms are identical, i.e. have the same structure and identical variables.

val renumber_variables_term : int array -> term -> unit

renumber_variables table term reassigns variable numbers starting from 0 to the variables in term. table is an int array of length max_vars, that maps old var numbers to the new ones. It must be initialized by -1. table is modified and can be passed to the next call of renumber_variables to consistently renumber variables in a set of terms.

Note: variables in term may not be shared as objects.

Built-Ins and Evaluable Arithmetic Functions

type deterministic_builtin = term -> context -> context -> trail -> trail

Function type for a built-in that succeeds at most once. It is performed by calling that function, say f, in the following way:

f term context1
   context2 trail

. term in context1 is the input term. context2 is an auxiliary fresh context with proper multiplier, that may be used, and has to be restored by this function when it returns fail. The result is a trail corresponding to the input trail extended by variable bindings performed as side effects in the contexts or fail. See example implementations in module builtins.

type p =

`\|`	`PUnbound`
`\|`	`PDeterministic of deterministic_builtin * (Opt.mode_specifier * Opt.discrimination_values * Opt.proof)`

The type of functions which are associated with symbols in predicate role. They are used for implementing built-in predicates.

val symbol_predicate : symbol -> p

val set_symbol_predicate : symbol -> p -> unit

type f =

`\|`	`FUnbound`
`\|`	`FUnary of (term -> term)`
`\|`	`FBinary of (term -> term -> term)`

The type of functions which are associated with symbols in functional role. They are used for implementing Prolog-style arithmetic evaluation.

val symbol_function : symbol -> f

val set_symbol_function : symbol -> f -> unit