sig
type variable
and symbol
and compound
and term =
Variable of Term.variable
| Constant of Term.symbol
| Compound of Term.compound
| Integer of int
| Float of float
| Unbound
val make_variable : int -> Term.variable
val variable_number : Term.variable -> int
val gensym : unit -> Term.symbol
val symbol_name : Term.symbol -> string
val symbol_arity : Term.symbol -> int
val make_compound : Term.symbol -> Term.term array -> Term.compound
val compound_functor : Term.compound -> Term.symbol
val compound_args : Term.compound -> Term.term array
type symbol_table
val make_symbol_table : unit -> Term.symbol_table
val find_symbol : Term.symbol_table -> string -> int -> Term.symbol
val symbol_table_iter : (Term.symbol -> unit) -> Term.symbol_table -> unit
val get_meta_functor_symbol : Term.symbol_table -> Term.symbol
val get_rule_symbol : Term.symbol_table -> Term.symbol
val get_disjunction_symbol : Term.symbol_table -> Term.symbol
val get_conjunction_symbol : Term.symbol_table -> Term.symbol
val get_true_symbol : Term.symbol_table -> Term.symbol
val get_false_symbol : Term.symbol_table -> Term.symbol
val get_stratified_neg_as_failure_symbol : Term.symbol_table -> Term.symbol
val get_stratified_neg_as_failure_alternate_symbol :
Term.symbol_table -> Term.symbol
val get_stratified_neg_as_failure_not_subsumed_symbol :
Term.symbol_table -> Term.symbol
val get_findall_symbol : Term.symbol_table -> Term.symbol
val get_neg2_symbol : Term.symbol_table -> Term.symbol
val set_meta_functor_symbol : Term.symbol_table -> Term.symbol -> unit
val set_rule_symbol : Term.symbol_table -> Term.symbol -> unit
val set_disjunction_symbol : Term.symbol_table -> Term.symbol -> unit
val set_conjunction_symbol : Term.symbol_table -> Term.symbol -> unit
val set_true_symbol : Term.symbol_table -> Term.symbol -> unit
val set_false_symbol : Term.symbol_table -> Term.symbol -> unit
val set_stratified_neg_as_failure_symbol :
Term.symbol_table -> Term.symbol -> unit
val set_stratified_neg_as_failure_alternate_symbol :
Term.symbol_table -> Term.symbol -> unit
val set_stratified_neg_as_failure_not_subsumed_symbol :
Term.symbol_table -> Term.symbol -> unit
val set_findall_symbol : Term.symbol_table -> Term.symbol -> unit
val set_neg2_symbol : Term.symbol_table -> Term.symbol -> unit
type context
val max_vars : int
exception Max_vars_exceeded
val make_context : int -> Term.context
val null_context : Term.context
val context_multiplier : Term.context -> int
val dereference : Term.term -> Term.context -> Term.term * Term.context
type trail
val make_trail : unit -> Term.trail
val fail : Term.trail
val failed : Term.trail -> bool
type saved_trail
val save_trail : Term.trail -> Term.saved_trail
val undo_bindings : Term.trail -> Term.saved_trail -> Term.trail
val unify :
Term.term ->
Term.context -> Term.term -> Term.context -> Term.trail -> Term.trail
val apply : Term.term -> Term.context -> Term.term
val copy_term : Term.term -> Term.term
val match_terms :
Term.term -> Term.context -> Term.term -> Term.trail -> Term.trail
val subsumes_chk : Term.term -> Term.term -> bool
val variant : Term.term -> Term.term -> bool
val term_ident : Term.term -> Term.term -> bool
val renumber_variables_term : int array -> Term.term -> unit
type deterministic_builtin =
Term.term -> Term.context -> Term.context -> Term.trail -> Term.trail
type p =
PUnbound
| PDeterministic of Term.deterministic_builtin *
(Opt.mode_specifier * Opt.discrimination_values * Opt.proof)
val symbol_predicate : Term.symbol -> Term.p
val set_symbol_predicate : Term.symbol -> Term.p -> unit
type f =
FUnbound
| FUnary of (Term.term -> Term.term)
| FBinary of (Term.term -> Term.term -> Term.term)
val symbol_function : Term.symbol -> Term.f
val set_symbol_function : Term.symbol -> Term.f -> unit
end