module Term:The structure of terms.`sig`

..`end`

`type `

key

Hash keys for terms

`type `

db_index

de Bruijn indices for bound variables

`type `

term = private

`|` |
`Bound of ` |
`(*` | Bound variables | `*)` |

`|` |
`Variable of ` |
`(*` | Free variables | `*)` |

`|` |
`Constant of ` |
`(*` | Constants | `*)` |

`|` |
`Application of ` |
`(*` | Function application | `*)` |

`|` |
`Abstraction of ` |
`(*` | 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.

`val is_variable : ``term -> bool`

Is the term a variable?

`val variable : ``Variable.t -> term`

A variable.

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

- Require
`is_constant t`

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

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

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

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

- Require
`is_application t`

`val application_argument : ``term -> term`

The argument in an application.

- Require
`is_application t`

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

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

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.

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

`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