sig
type 'a var
type 'a mvar = 'a Bindlib.var array
type (-'a, +'b) binder
type ('a, 'b) mbinder
val subst : ('a, 'b) Bindlib.binder -> 'a -> 'b
val msubst : ('a, 'b) Bindlib.mbinder -> 'a array -> 'b
val new_var : ('a Bindlib.var -> 'a) -> string -> 'a Bindlib.var
val new_mvar : ('a Bindlib.var -> 'a) -> string array -> 'a Bindlib.mvar
val name_of : 'a Bindlib.var -> string
val uid_of : 'a Bindlib.var -> int
val unbind :
('a Bindlib.var -> 'a) -> ('a, 'b) Bindlib.binder -> 'a Bindlib.var * 'b
val unbind2 :
('a Bindlib.var -> 'a) ->
('a, 'b) Bindlib.binder ->
('a, 'c) Bindlib.binder -> 'a Bindlib.var * 'b * 'c
val eq_binder :
('a Bindlib.var -> 'a) ->
('b -> 'b -> bool) ->
('a, 'b) Bindlib.binder -> ('a, 'b) Bindlib.binder -> bool
val unmbind :
('a Bindlib.var -> 'a) ->
('a, 'b) Bindlib.mbinder -> 'a Bindlib.mvar * 'b
val unmbind2 :
('a Bindlib.var -> 'a) ->
('a, 'b) Bindlib.mbinder ->
('a, 'c) Bindlib.mbinder -> 'a Bindlib.mvar * 'b * 'c
val eq_mbinder :
('a Bindlib.var -> 'a) ->
('b -> 'b -> bool) ->
('a, 'b) Bindlib.mbinder -> ('a, 'b) Bindlib.mbinder -> bool
type +'a bindbox
val box_of_var : 'a Bindlib.var -> 'a Bindlib.bindbox
val box : 'a -> 'a Bindlib.bindbox
val apply_box :
('a -> 'b) Bindlib.bindbox -> 'a Bindlib.bindbox -> 'b Bindlib.bindbox
val box_apply : ('a -> 'b) -> 'a Bindlib.bindbox -> 'b Bindlib.bindbox
val box_apply2 :
('a -> 'b -> 'c) ->
'a Bindlib.bindbox -> 'b Bindlib.bindbox -> 'c Bindlib.bindbox
val bind :
('a Bindlib.var -> 'a) ->
string ->
('a Bindlib.bindbox -> 'b Bindlib.bindbox) ->
('a, 'b) Bindlib.binder Bindlib.bindbox
val mbind :
('a Bindlib.var -> 'a) ->
string array ->
('a Bindlib.bindbox array -> 'b Bindlib.bindbox) ->
('a, 'b) Bindlib.mbinder Bindlib.bindbox
val unbox : 'a Bindlib.bindbox -> 'a
val vbind :
('a Bindlib.var -> 'a) ->
string ->
('a Bindlib.var -> 'b Bindlib.bindbox) ->
('a, 'b) Bindlib.binder Bindlib.bindbox
val mvbind :
('a Bindlib.var -> 'a) ->
string array ->
('a Bindlib.var array -> 'b Bindlib.bindbox) ->
('a, 'b) Bindlib.mbinder Bindlib.bindbox
val bind_var :
'a Bindlib.var ->
'b Bindlib.bindbox -> ('a, 'b) Bindlib.binder Bindlib.bindbox
val bind_mvar :
'a Bindlib.mvar ->
'b Bindlib.bindbox -> ('a, 'b) Bindlib.mbinder Bindlib.bindbox
val box_opt : 'a Bindlib.bindbox option -> 'a option Bindlib.bindbox
val box_list : 'a Bindlib.bindbox list -> 'a list Bindlib.bindbox
val box_rev_list : 'a Bindlib.bindbox list -> 'a list Bindlib.bindbox
val box_array : 'a Bindlib.bindbox array -> 'a array Bindlib.bindbox
val box_apply3 :
('a -> 'b -> 'c -> 'd) ->
'a Bindlib.bindbox ->
'b Bindlib.bindbox -> 'c Bindlib.bindbox -> 'd Bindlib.bindbox
val box_apply4 :
('a -> 'b -> 'c -> 'd -> 'e) ->
'a Bindlib.bindbox ->
'b Bindlib.bindbox ->
'c Bindlib.bindbox -> 'd Bindlib.bindbox -> 'e Bindlib.bindbox
val box_pair :
'a Bindlib.bindbox -> 'b Bindlib.bindbox -> ('a * 'b) Bindlib.bindbox
val box_triple :
'a Bindlib.bindbox ->
'b Bindlib.bindbox ->
'c Bindlib.bindbox -> ('a * 'b * 'c) Bindlib.bindbox
module type Map =
sig
type 'a t
val map : ('a -> 'b) -> 'a Bindlib.Map.t -> 'b Bindlib.Map.t
end
module Lift :
functor (M : Map) ->
sig val lift_box : 'a Bindlib.bindbox M.t -> 'a M.t Bindlib.bindbox end
module type Map2 =
sig
type ('a, 'b) t
val map :
('a -> 'b) ->
('c -> 'd) -> ('a, 'c) Bindlib.Map2.t -> ('b, 'd) Bindlib.Map2.t
end
module Lift2 :
functor (M : Map2) ->
sig
val lift_box :
('a Bindlib.bindbox, 'b Bindlib.bindbox) M.t ->
('a, 'b) M.t Bindlib.bindbox
end
val prefix_of : 'a Bindlib.var -> string
val suffix_of : 'a Bindlib.var -> int
val hash_var : 'a Bindlib.var -> int
val compare_vars : 'a Bindlib.var -> 'b Bindlib.var -> int
val eq_vars : 'a Bindlib.var -> 'b Bindlib.var -> bool
val copy_var :
'b Bindlib.var -> string -> ('a Bindlib.var -> 'a) -> 'a Bindlib.var
val binder_name : ('a, 'b) Bindlib.binder -> string
val binder_occur : ('a, 'b) Bindlib.binder -> bool
val binder_constant : ('a, 'b) Bindlib.binder -> bool
val binder_closed : ('a, 'b) Bindlib.binder -> bool
val binder_rank : ('a, 'b) Bindlib.binder -> int
val binder_compose_left :
('a -> 'b) -> ('b, 'c) Bindlib.binder -> ('a, 'c) Bindlib.binder
val binder_compose_right :
('a, 'b) Bindlib.binder -> ('b -> 'c) -> ('a, 'c) Bindlib.binder
val mbinder_arity : ('a, 'b) Bindlib.mbinder -> int
val mbinder_names : ('a, 'b) Bindlib.mbinder -> string array
val mbinder_occurs : ('a, 'b) Bindlib.mbinder -> bool array
val mbinder_constant : ('a, 'b) Bindlib.mbinder -> bool
val mbinder_closed : ('a, 'b) Bindlib.mbinder -> bool
val mbinder_rank : ('a, 'b) Bindlib.mbinder -> int
val is_closed : 'a Bindlib.bindbox -> bool
val is_substituted : (bool -> 'a) Bindlib.bindbox -> 'a Bindlib.bindbox
val occur : 'a Bindlib.var -> 'b Bindlib.bindbox -> bool
val bind_apply :
('a, 'b) Bindlib.binder Bindlib.bindbox ->
'a Bindlib.bindbox -> 'b Bindlib.bindbox
val mbind_apply :
('a, 'b) Bindlib.mbinder Bindlib.bindbox ->
'a array Bindlib.bindbox -> 'b Bindlib.bindbox
val fixpoint :
(('a, 'b) Bindlib.binder, ('a, 'b) Bindlib.binder) Bindlib.binder
Bindlib.bindbox -> ('a, 'b) Bindlib.binder Bindlib.bindbox
type ctxt
val empty_ctxt : Bindlib.ctxt
val new_var_in :
Bindlib.ctxt ->
('a Bindlib.var -> 'a) -> string -> 'a Bindlib.var * Bindlib.ctxt
val new_mvar_in :
Bindlib.ctxt ->
('a Bindlib.var -> 'a) -> string array -> 'a Bindlib.mvar * Bindlib.ctxt
val unbind_in :
Bindlib.ctxt ->
('a Bindlib.var -> 'a) ->
('a, 'b) Bindlib.binder -> 'a Bindlib.var * 'b * Bindlib.ctxt
val unmbind_in :
Bindlib.ctxt ->
('a Bindlib.var -> 'a) ->
('a, 'b) Bindlib.mbinder -> 'a Bindlib.mvar * 'b * Bindlib.ctxt
val bind_in :
Bindlib.ctxt ->
('a Bindlib.var -> 'a) ->
string ->
('a Bindlib.bindbox -> Bindlib.ctxt -> 'b Bindlib.bindbox) ->
('a, 'b) Bindlib.binder Bindlib.bindbox
val mbind_in :
Bindlib.ctxt ->
('a Bindlib.var -> 'a) ->
string array ->
('a Bindlib.bindbox array -> Bindlib.ctxt -> 'b Bindlib.bindbox) ->
('a, 'b) Bindlib.mbinder Bindlib.bindbox
val reset_counter : unit -> unit
val dummy_bindbox : 'a Bindlib.bindbox
val binder_from_fun : string -> ('a -> 'b) -> ('a, 'b) Bindlib.binder
val mbinder_from_fun :
string array -> ('a array -> 'b) -> ('a, 'b) Bindlib.mbinder
end