Module Term.T

type symbol = Symbol.t

Symbol

type var = Var.t

Variable

type sort = Type.t

Sort

type attr

Attribute

type lambda_node = private
| L of sort list * t

Lambda abstraction over symbols, variables and sort of the types given. Values of the type cannot be constructed outside this module in order to maintain invariants about the data type.

and lambda = private (lambda_node, unit) Hashcons.hash_consed

Hashconsed lambda abstraction

and t_node = private
| FreeVar of var
| BoundVar of int
| Leaf of symbol
| Node of symbol * t list
| Let of lambda * t list
| Exists of lambda
| Forall of lambda
| Annot of t * attr

Abstract syntax term over symbols, variables and sort of the types given. Values of the type cannot be constructed outside this module in order to maintain invariants about the data type. Use the constructors mk_var, mk_const, mk_app, mk_let, mk_exists and mk_forall.

and t_prop = private {
bound_vars : int list;
}

Properties of a term

and t = private (t_node, t_prop) Hashcons.hash_consed

Hashconsed abstract syntax term

and flat = private
| Var of var
| Const of symbol
| App of symbol * t list
| Attr of t * attr

Term over symbols, variables and sort of the types given where the topmost symbol is not a binding

This type must remain private, because construct does not check the invariants and would be a backdoor to construct unsafe terms.

val compare : t -> t -> int

Comparison function on terms

val equal : t -> t -> bool

Equality function on terms

val hash : t -> int

Hash function on terms

val tag : t -> int

Unique identifier for term

val mk_lambda : var list -> t -> lambda

Constructor for a lambda expression

val eval_lambda : lambda -> t list -> t

Beta-evaluate a lambda expression

val partial_eval_lambda : lambda -> t list -> lambda

Partialy Beta-evaluate a lambda expression

val mk_term : t_node -> t

Constructor for a term

val mk_var : var -> t

Constructor for a free variable with indexes

val mk_const : symbol -> t

Constructor for a constant

val mk_app : symbol -> t list -> t

Constructor for a function application

val mk_let : (var * t) list -> t -> t

Constructor for a let binding

val mk_let_elim : (var * t) list -> t -> t

Constructor for a let binding

val mk_exists : var list -> t -> t

Constructor for an existential quantification over an indexed free variable

val mk_forall : var list -> t -> t

Constructor for a universal quantification over an indexed free variable

val mk_annot : t -> attr -> t

Constructor for an annotated term

val node_of_t : t -> t_node

Return the node of a hashconsed term

val node_of_lambda : lambda -> lambda_node

Return the node of a hashconsed lamda abstraction

val sorts_of_lambda : lambda -> sort list

Return the sorts of a hashconsed lambda abstraction

val tag_of_t : t -> int

Return the unique tag of a hashconsed term

val eval_t : ?⁠fail_on_quantifiers:bool -> (flat -> 'a list -> 'a) -> t -> 'a

Evaluate the term bottom-up and right-to-left. The evaluation function is called at each node of the term with the term being evaluated and the list of values computed for the subterms. Let bindings are lazily unfolded.

val map : (int -> t -> t) -> t -> t

Tail-recursive bottom-up right-to-left map on the term

Not every subterm is a proper term, since the de Bruijn indexes are shifted. Therefore, the function f is called with the number of let bindings the subterm is under as first argument, so that the indexes can be adjusted in the subterm if necessary.

val destruct : t -> flat

Return the top symbol of a term along with its subterms

If the top symbol of a term is a let binding, the binding is distributed over the subterms.

val has_quantifier : t -> bool

Returns true if the term has quantifiers

val instantiate : lambda -> t list -> t
val construct : flat -> t

Convert the flattened representation back into a term

val import : t -> t

Import a term into the hashcons table by rebuilding it bottom up

val import_lambda : lambda -> lambda

Import a lambda abstraction into the hashcons table by rebuilding it bottom up

val pp_print_term : ?⁠db:int -> Stdlib.Format.formatter -> t -> unit

Pretty-print a term

val pp_print_term : ?⁠db:int -> Stdlib.Format.formatter -> t -> unit

Pretty-print a term

val pp_print_lambda_w : (?⁠arity:int -> Stdlib.Format.formatter -> symbol -> unit) -> (Stdlib.Format.formatter -> var -> unit) -> (Stdlib.Format.formatter -> sort -> unit) -> ?⁠db:int -> Stdlib.Format.formatter -> lambda -> unit
val pp_print_term_w : (?⁠arity:int -> Stdlib.Format.formatter -> symbol -> unit) -> (Stdlib.Format.formatter -> var -> unit) -> (Stdlib.Format.formatter -> sort -> unit) -> ?⁠db:int -> Stdlib.Format.formatter -> t -> unit
val print_term : ?⁠db:int -> t -> unit

Pretty-print a term

val pp_print_lambda : ?⁠db:int -> Stdlib.Format.formatter -> lambda -> unit

Pretty-print a lambda abstraction

val print_lambda : ?⁠db:int -> lambda -> unit

Pretty-print a lambda abstraction

val stats : unit -> int * int * int * int * int * int