bindlib 4.0.4 · OCaml Package

type 'a var

type 'a mvar = 'a var array

type (-'a, +'b) binder

type ('a, 'b) mbinder

val subst : ('a, 'b) binder -> 'a -> 'b

val msubst : ('a, 'b) mbinder -> 'a array -> 'b

val new_var : ('a var -> 'a) -> string -> 'a var

val new_mvar : ('a var -> 'a) -> string array -> 'a mvar

val name_of : 'a var -> string

val unbind : ('a var -> 'a) -> ('a, 'b) binder -> 'a var * 'b

val unmbind : ('a var -> 'a) -> ('a, 'b) mbinder -> 'a mvar * 'b

type +'a bindbox

val box_of_var : 'a var -> 'a bindbox

val box : 'a -> 'a bindbox

val apply_box : ('a -> 'b) bindbox -> 'a bindbox -> 'b bindbox

val box_apply : ('a -> 'b) -> 'a bindbox -> 'b bindbox

val box_apply2 : ('a -> 'b -> 'c) -> 'a bindbox -> 'b bindbox -> 'c bindbox

val bind : 
  ('a var -> 'a) ->
  string ->
  ('a bindbox -> 'b bindbox) ->
  ('a, 'b) binder bindbox

val mbind : 
  ('a var -> 'a) ->
  string array ->
  ('a bindbox array -> 'b bindbox) ->
  ('a, 'b) mbinder bindbox

val unbox : 'a bindbox -> 'a

val vbind : 
  ('a var -> 'a) ->
  string ->
  ('a var -> 'b bindbox) ->
  ('a, 'b) binder bindbox

val mvbind : 
  ('a var -> 'a) ->
  string array ->
  ('a var array -> 'b bindbox) ->
  ('a, 'b) mbinder bindbox

val bind_var : 'a var -> 'b bindbox -> ('a, 'b) binder bindbox

val bind_mvar : 'a mvar -> 'b bindbox -> ('a, 'b) mbinder bindbox

val box_opt : 'a bindbox option -> 'a option bindbox

val box_list : 'a bindbox list -> 'a list bindbox

val box_rev_list : 'a bindbox list -> 'a list bindbox

val box_array : 'a bindbox array -> 'a array bindbox

val box_apply3 : 
  ('a -> 'b -> 'c -> 'd) ->
  'a bindbox ->
  'b bindbox ->
  'c bindbox ->
  'd bindbox

val box_apply4 : 
  ('a -> 'b -> 'c -> 'd -> 'e) ->
  'a bindbox ->
  'b bindbox ->
  'c bindbox ->
  'd bindbox ->
  'e bindbox

val box_pair : 'a bindbox -> 'b bindbox -> ('a * 'b) bindbox

val box_triple : 
  'a bindbox ->
  'b bindbox ->
  'c bindbox ->
  ('a * 'b * 'c) bindbox

module type Map = sig ... end

module Lift (M : Map) : sig ... end

module type Map2 = sig ... end

module Lift2 (M : Map2) : sig ... end

val prefix_of : 'a var -> string

val suffix_of : 'a var -> int

val free_of : 'a var -> 'a

val hash_var : 'a var -> int

val compare_vars : 'a var -> 'b var -> int

val eq_vars : 'a var -> 'b var -> bool

val copy_var : 'b var -> string -> ('a var -> 'a) -> 'a var

val binder_name : ('a, 'b) binder -> string

val binder_occur : ('a, 'b) binder -> bool

val binder_constant : ('a, 'b) binder -> bool

val binder_closed : ('a, 'b) binder -> bool

val binder_rank : ('a, 'b) binder -> int

val binder_compose_left : ('a -> 'b) -> ('b, 'c) binder -> ('a, 'c) binder

val binder_compose_right : ('a, 'b) binder -> ('b -> 'c) -> ('a, 'c) binder

val mbinder_arity : ('a, 'b) mbinder -> int

val mbinder_names : ('a, 'b) mbinder -> string array

val mbinder_occurs : ('a, 'b) mbinder -> bool array

val mbinder_constant : ('a, 'b) mbinder -> bool

val mbinder_closed : ('a, 'b) mbinder -> bool

val mbinder_rank : ('a, 'b) mbinder -> int

val is_closed : 'a bindbox -> bool

val occur : 'a var -> 'b bindbox -> bool

val bind_apply : ('a, 'b) binder bindbox -> 'a bindbox -> 'b bindbox

val mbind_apply : ('a, 'b) mbinder bindbox -> 'a array bindbox -> 'b bindbox

val fixpoint : 
  (('a, 'b) binder, ('a, 'b) binder) binder bindbox ->
  ('a, 'b) binder bindbox

type ctxt

val empty_ctxt : ctxt

val new_var_in : ctxt -> ('a var -> 'a) -> string -> 'a var * ctxt

val new_mvar_in : ctxt -> ('a var -> 'a) -> string array -> 'a mvar * ctxt

val unbind_in : ctxt -> ('a var -> 'a) -> ('a, 'b) binder -> 'a var * 'b * ctxt

val unmbind_in : 
  ctxt ->
  ('a var -> 'a) ->
  ('a, 'b) mbinder ->
  'a mvar * 'b * ctxt

val bind_in : 
  ctxt ->
  ('a var -> 'a) ->
  string ->
  ('a bindbox -> ctxt -> 'b bindbox) ->
  ('a, 'b) binder bindbox

val mbind_in : 
  ctxt ->
  ('a var -> 'a) ->
  string array ->
  ('a bindbox array -> ctxt -> 'b bindbox) ->
  ('a, 'b) mbinder bindbox

val reset_counter : unit -> unit

val dummy_bindbox : 'a bindbox

val binder_from_fun : string -> ('a -> 'b) -> ('a, 'b) binder

val mbinder_from_fun : string array -> ('a array -> 'b) -> ('a, 'b) mbinder

package bindlib