Module Term


module Term: sig .. end
The structure of terms.


Term data-structures


type key 
Hash keys for terms
type db_index 
de Bruijn indices for bound variables

type term = private
| Bound of db_index (*Bound variables*)
| Variable of key * Variable.t (*Free variables*)
| Constant of key * Constant.t (*Constants*)
| Application of key * term * term (*Function application*)
| Abstraction of key * Variable.t * term (*Lambda abstraction*)
Terms
val term_equal : term -> term -> bool
Are two terms equal?
val term_compare : term -> term -> int
An arbitrary ordering on terms.
val term_hash : term -> int
A hash key for the term.

Variables


val is_variable : term -> bool
Is the term a variable?
val variable : Variable.t -> term
A variable.

Constants


val is_constant : term -> bool
Is the term a constant?
val constant : Constant.t -> term
A constant.
val constant_value : term -> Constant.t
constant_value t is the value of a constant.



Symbolic Constants


val is_symbolic_constant : term -> bool
Is a term a symbolic constant.


val symbolic_constant : Symbol.t -> term
A symbolic constant.
val symbolic_value : term -> Symbol.t
symbolic_value t is the value of a symbolic constant.



Integer Constants


val is_integer_constant : term -> bool
Is a term an integer constant.


val integer_constant : Big_int.big_int -> term
Integer constant.
val integer_value : term -> Big_int.big_int
integer_value t is the value of an integer constant.



Rational Constants


val is_rational_constant : term -> bool
Is a term a rational constant.


val rational_constant : Num.num -> term
Arbitrary precision rational constant.
val rational_value : term -> Num.num
rational_value t is the value of a rational constant.



Applications


val is_application : term -> bool
Is a term an application?
val application : term -> term -> term
The application of the given terms.
val application_function : term -> term
The function in an application.


val application_argument : term -> term
The argument in an application.


val binary_application : term -> term -> term -> term
binary_application f x y is equivalent to application (application f x) y.
val ternary_application : term -> term -> term -> term -> term
ternary_application f x y z is equivalent to application (application (application f x) y) z.
val nary_application : term -> term list -> term
nary_application f args is equivalent to List.fold_left application f args.
val nary_application_decomposition : term -> term * term list
Decompose a term to yield a function and a list of arguments. If the term is not an application then the pair of the term and the empty list is produced.

Abstractions


val is_abstraction : term -> bool
Is a term an abstraction?
val abstraction : Variable.t -> term -> term
abstraction v tm is \v. tm.
val nary_abstraction : Variable.t list -> term -> term
nary_abstraction [v0, ... ,vn] tm is \v0. ... \vn.tm.
val beta_normal_form : term -> term
The term obtained by reducing all beta-redexes in a term. Applicative order reduction is used.

Data-structures.


module Term_compared: Util.ComparedType  with type t = term
Terms augmented with comparison functions.
module Term_hashtbl: Hashtbl.S  with type key = term
Hash tables keyed off terms.
module Term_set: Set.S  with type elt = term
Sets of terms.
module Term_mutable_set: Index.Set  with type elt = term
Mutable sets of terms.
module Term_map: Map.S  with type key = term
Maps from terms.
module Term_union_find: Union_find.S  with type elem = term
Union-find over terms.

Miscellaneous


val uninterpret : (term -> bool) ->
term Term_hashtbl.t -> term -> term
uninterpret p tbl tm replaces "uninterpreted constants", i.e. constant subterms s such that not (p s), with fresh variables.
val free_variables : term -> Term_set.t
The free variables of a term.

Pretty-Printing.


val string_of_term : term -> string
String representation of term.
val pp_print_term : Format.formatter -> term -> unit
Pretty-print a term.
val print_term : term -> unit
Print a term using std_formatter.
val pp_compact_print_term : Format.formatter -> term -> unit
Pretty-print a term, compactly by defining local lets to avoid repetitiously printing shared sub-terms.
val compact_print_term : term -> unit
Compactly print a term using std_formatter.
val log_term : int -> term -> unit
log_term level tm is equivalent to Log.log level pp_print_term tm

Hosted by the SourceForge.net Logo* web site.
*Other names and brands may be claimed as the property of others.