bindlib 4.0 · OCaml Package

type 'a variable

type 'a mvariable = 'a variable 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 variable -> 'a) -> string -> 'a variable

val new_mvar : ('a variable -> 'a) -> string array -> 'a mvariable

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

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

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

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

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

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 binder_from_fun : string -> int -> ('a -> 'b) -> ('a, 'b) binder

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

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

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

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

val name_of : 'a variable -> string

val free_of : 'a variable -> 'a

val hash_var : 'a variable -> int

val compare_variables : 'a variable -> 'b variable -> int

val eq_variables : 'a variable -> 'b variable -> bool

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

type +'a bindbox

val unbox : 'a bindbox -> 'a

val box_of_var : 'a variable -> 'a bindbox

val box : 'a -> 'a bindbox

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

val is_closed : 'a bindbox -> bool

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

val dummy_bindbox : 'a bindbox

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

val reset_counter : unit -> unit

module type Map = sig ... end

module type Map2 = sig ... end

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

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

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

type context

val empty_context : context

val new_var_in : 
  context ->
  ('a variable -> 'a) ->
  string ->
  'a variable * context

val new_mvar_in : 
  context ->
  ('a variable -> 'a) ->
  string array ->
  'a mvariable * context

val bind_in : 
  context ->
  ('a variable -> 'a) ->
  string ->
  ('a bindbox -> context -> 'b bindbox) ->
  ('a, 'b) binder bindbox

val mbind_in : 
  context ->
  ('a variable -> 'a) ->
  string array ->
  ('a bindbox array -> context -> 'b bindbox) ->
  ('a, 'b) mbinder bindbox

val list_variables : 'a bindbox -> string list

package bindlib