sig
  module type BaseTypes =
    sig
      type symbol
      type var
      type sort
      type attr
      val hash_of_symbol : Ltree.BaseTypes.symbol -> int
      val hash_of_var : Ltree.BaseTypes.var -> int
      val hash_of_sort : Ltree.BaseTypes.sort -> int
      val hash_of_attr : Ltree.BaseTypes.attr -> int
      val sort_of_var : Ltree.BaseTypes.var -> Ltree.BaseTypes.sort
      val mk_fresh_var : Ltree.BaseTypes.sort -> Ltree.BaseTypes.var
      val import_symbol : Ltree.BaseTypes.symbol -> Ltree.BaseTypes.symbol
      val import_var : Ltree.BaseTypes.var -> Ltree.BaseTypes.var
      val import_sort : Ltree.BaseTypes.sort -> Ltree.BaseTypes.sort
      val pp_print_symbol :
        Format.formatter -> Ltree.BaseTypes.symbol -> unit
      val pp_print_var : Format.formatter -> Ltree.BaseTypes.var -> unit
      val pp_print_sort : Format.formatter -> Ltree.BaseTypes.sort -> unit
      val pp_print_attr : Format.formatter -> Ltree.BaseTypes.attr -> unit
    end
  module type S =
    sig
      type symbol
      type var
      type sort
      type attr
      type lambda_node = private L of Ltree.S.sort list * Ltree.S.t
      and lambda = private (Ltree.S.lambda_node, unit) Hashcons.hash_consed
      and t_node = private
          FreeVar of Ltree.S.var
        | BoundVar of int
        | Leaf of Ltree.S.symbol
        | Node of Ltree.S.symbol * Ltree.S.t list
        | Let of Ltree.S.lambda * Ltree.S.t list
        | Exists of Ltree.S.lambda
        | Forall of Ltree.S.lambda
        | Annot of Ltree.S.t * Ltree.S.attr
      and t_prop = private { bound_vars : int list; }
      and t = private (Ltree.S.t_node, Ltree.S.t_prop) Hashcons.hash_consed
      and flat = private
          Var of Ltree.S.var
        | Const of Ltree.S.symbol
        | App of Ltree.S.symbol * Ltree.S.t list
        | Attr of Ltree.S.t * Ltree.S.attr
      val compare : Ltree.S.t -> Ltree.S.t -> int
      val equal : Ltree.S.t -> Ltree.S.t -> bool
      val hash : Ltree.S.t -> int
      val tag : Ltree.S.t -> int
      val mk_lambda : Ltree.S.var list -> Ltree.S.t -> Ltree.S.lambda
      val eval_lambda : Ltree.S.lambda -> Ltree.S.t list -> Ltree.S.t
      val partial_eval_lambda :
        Ltree.S.lambda -> Ltree.S.t list -> Ltree.S.lambda
      val mk_term : Ltree.S.t_node -> Ltree.S.t
      val mk_var : Ltree.S.var -> Ltree.S.t
      val mk_const : Ltree.S.symbol -> Ltree.S.t
      val mk_app : Ltree.S.symbol -> Ltree.S.t list -> Ltree.S.t
      val mk_let : (Ltree.S.var * Ltree.S.t) list -> Ltree.S.t -> Ltree.S.t
      val mk_let_elim :
        (Ltree.S.var * Ltree.S.t) list -> Ltree.S.t -> Ltree.S.t
      val mk_exists : Ltree.S.var list -> Ltree.S.t -> Ltree.S.t
      val mk_forall : Ltree.S.var list -> Ltree.S.t -> Ltree.S.t
      val mk_annot : Ltree.S.t -> Ltree.S.attr -> Ltree.S.t
      val node_of_t : Ltree.S.t -> Ltree.S.t_node
      val node_of_lambda : Ltree.S.lambda -> Ltree.S.lambda_node
      val sorts_of_lambda : Ltree.S.lambda -> Ltree.S.sort list
      val tag_of_t : Ltree.S.t -> int
      val eval_t :
        ?fail_on_quantifiers:bool ->
        (Ltree.S.flat -> 'a list -> 'a) -> Ltree.S.t -> 'a
      val map : (int -> Ltree.S.t -> Ltree.S.t) -> Ltree.S.t -> Ltree.S.t
      val destruct : Ltree.S.t -> Ltree.S.flat
      val has_quantifier : Ltree.S.t -> bool
      val instantiate : Ltree.S.lambda -> Ltree.S.t list -> Ltree.S.t
      val construct : Ltree.S.flat -> Ltree.S.t
      val import : Ltree.S.t -> Ltree.S.t
      val import_lambda : Ltree.S.lambda -> Ltree.S.lambda
      val pp_print_term : ?db:int -> Format.formatter -> Ltree.S.t -> unit
      val pp_print_lambda_w :
        (?arity:int -> Format.formatter -> Ltree.S.symbol -> unit) ->
        (Format.formatter -> Ltree.S.var -> unit) ->
        (Format.formatter -> Ltree.S.sort -> unit) ->
        ?db:int -> Format.formatter -> Ltree.S.lambda -> unit
      val pp_print_term_w :
        (?arity:int -> Format.formatter -> Ltree.S.symbol -> unit) ->
        (Format.formatter -> Ltree.S.var -> unit) ->
        (Format.formatter -> Ltree.S.sort -> unit) ->
        ?db:int -> Format.formatter -> Ltree.S.t -> unit
      val print_term : ?db:int -> Ltree.S.t -> unit
      val pp_print_lambda :
        ?db:int -> Format.formatter -> Ltree.S.lambda -> unit
      val print_lambda : ?db:int -> Ltree.S.lambda -> unit
      val stats : unit -> int * int * int * int * int * int
    end
  module Make :
    functor (T : BaseTypes->
      sig
        type symbol = T.symbol
        type var = T.var
        type sort = T.sort
        type attr = T.attr
        type lambda_node = private L of sort list * t
        and lambda = private (lambda_node, unit) Hashcons.hash_consed
        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
        and t_prop = private { bound_vars : int list; }
        and t = private (t_node, t_prop) Hashcons.hash_consed
        and flat = private
            Var of var
          | Const of symbol
          | App of symbol * t list
          | Attr of t * attr
        val compare : t -> t -> int
        val equal : t -> t -> bool
        val hash : t -> int
        val tag : t -> int
        val mk_lambda : var list -> t -> lambda
        val eval_lambda : lambda -> t list -> t
        val partial_eval_lambda : lambda -> t list -> lambda
        val mk_term : t_node -> t
        val mk_var : var -> t
        val mk_const : symbol -> t
        val mk_app : symbol -> t list -> t
        val mk_let : (var * t) list -> t -> t
        val mk_let_elim : (var * t) list -> t -> t
        val mk_exists : var list -> t -> t
        val mk_forall : var list -> t -> t
        val mk_annot : t -> attr -> t
        val node_of_t : t -> t_node
        val node_of_lambda : lambda -> lambda_node
        val sorts_of_lambda : lambda -> sort list
        val tag_of_t : t -> int
        val eval_t :
          ?fail_on_quantifiers:bool -> (flat -> 'a list -> 'a) -> t -> 'a
        val map : (int -> t -> t) -> t -> t
        val destruct : t -> flat
        val has_quantifier : t -> bool
        val instantiate : lambda -> t list -> t
        val construct : flat -> t
        val import : t -> t
        val import_lambda : lambda -> lambda
        val pp_print_term : ?db:int -> Format.formatter -> t -> unit
        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
        val pp_print_lambda : ?db:int -> Format.formatter -> lambda -> unit
        val print_lambda : ?db:int -> lambda -> unit
        val stats : unit -> int * int * int * int * int * int
      end
end