module Term: sig .. end
The structure of terms.
Term data-structures
type
Hash keys for terms
type
de Bruijn indices for bound variables
type
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.
- Ensure
not (is_symbolic_constant t) || is_constant t
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.
- Require
is_symbolic_constant t
Integer Constants
val is_integer_constant : term -> bool
Is a term an integer constant.
- Ensure
not (is_integer_constant t) || is_constant t
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.
- Require
is_integer_constant t
Rational Constants
val is_rational_constant : term -> bool
Is a term a rational constant.
- Ensure
not (is_rational_constant t) || is_constant t
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
* web site.
*Other names and brands may be claimed as the property
of others.