Module Term.T

module T: Ltree.S 
  with type symbol = Symbol.t
  and type var = Var.t
  and type sort = Type.t

type symbol 
Symbol
type var 
Variable
type sort 
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.
type lambda = private (lambda_node, unit) Hashcons.hash_consed 
Hashconsed lambda abstraction
type 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 Ltree.S.mk_var, Ltree.S.mk_const, Ltree.S.mk_app, Ltree.S.mk_let, Ltree.S.mk_exists and Ltree.S.mk_forall.
type t_prop = private {
   bound_vars : int list;
}
Properties of a term
type t = private (t_node, t_prop) Hashcons.hash_consed 
Hashconsed abstract syntax term
type 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 Ltree.S.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 -> Format.formatter -> t -> unit
Pretty-print a term
val pp_print_term : ?db:int -> Format.formatter -> t -> unit
Pretty-print a term
val pp_print_lambda_w : (?arity:int -> Format.formatter -> symbol -> unit) ->
(Format.formatter -> var -> unit) ->
(Format.formatter -> sort -> unit) ->
?db:int -> Format.formatter -> lambda -> unit
val pp_print_term_w : (?arity:int -> Format.formatter -> symbol -> unit) ->
(Format.formatter -> var -> unit) ->
(Format.formatter -> sort -> unit) ->
?db:int -> Format.formatter -> t -> unit
val print_term : ?db:int -> t -> unit
Pretty-print a term
val pp_print_lambda : ?db:int -> 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