cuex/binding.h: Variable Binding using de Bruijn Indices
[cuex: Expressions]




cuex_t cuex_hole (int l)
cu_bool_t cuex_is_hole (cuex_t e)
cuex_t cuex_mupath_null ()
cuex_t cuex_mupath_pair (int level_diff, cuex_t head_seq, cuex_t tail_comp)
cu_bool_t cuex_opr_is_binder (cuex_meta_t opr)
cuex_t cuex_bfree_adjusted (cuex_t e, int j_diff)
void cuex_bfree_iter (cuex_t e, cu_clop(f, void, int, int), int j_top)
cuex_t cuex_bfree_tran (cuex_t e, cu_clop(f, cuex_t, int, int), int j_top)
cu_bool_t cuex_bfree_match (cu_clop(f, cu_bool_t, int, cuex_t, int), cuex_t p, cuex_t e, int j_top)
int cuex_bfree_into_uset (cuex_t e, int j_top, cucon_uset_t set)
int cuex_bfree_into_bitarray (cuex_t e, int j_top, int j_clip, cucon_bitarray_t set)
cuex_t cuex_reindex_by_int_stack (cuex_t e, int stack_top_level, int stack_span, cucon_stack_t stack)
int cuex_max_binding_depth (cuex_t e)
cucon_pmap_t cuex_unfolded_fv_sets (cuex_t e, int max_binding_depth)
void cuex_bi_sifi_indexing_accu (cuex_t e, unsigned int flags, cucon_pmap_t accu)
cucon_pmap_t cuex_bi_sifi_indexing (cuex_t e, unsigned int flags)

Detailed Description

This provides variables, scoping constructs, and algorithms for expressions using de Bruijn indexes. This includes the built-in μ-recursion and λ-expressions.

See also:
cuex/recursion.h: Functions on the Recursive Structure of Expressions

Function Documentation

cuex_t cuex_bfree_adjusted ( cuex_t  e,
int  j_diff 

For all free de Bruijn variables in e, increment their index by j_diff. This prepares the subexpression e to be substituted down across j_diff bind-sites, or for negative, up across -j_diff bind-sites.

int cuex_bfree_into_bitarray ( cuex_t  e,
int  j_top,
int  j_clip,
cucon_bitarray_t  set 

Insert de Burijn indices of free variables of e in the range [j_top, j_clip) into set, and return the number of unique free variables in the range which were not already present in set. The indices inserted into set are relative to j_top. Pass j_top = 0 and j_clip = INT_MAX to consider all free variables of e. The bit-array is resized as needed to fit the largest index.

int cuex_bfree_into_uset ( cuex_t  e,
int  j_top,
cucon_uset_t  set 

Inserts free variables of e into set, where j_top (usually 0) is considered to be the first unbound level. The index of the outermost variable is returned, or INT_MIN if there were no free variables.

void cuex_bfree_iter ( cuex_t  e,
cu_clop(f, void, int, int)  ,
int  j_top 

Calls f(lr, lr_top) for each free de Bruijn variable in e, where lr is the de Bruijn index and lr_top is j_top plus the binding depth of the hole. j_top is level relative to e at and above which variables are considered to be free.

cuex_t cuex_bfree_tran ( cuex_t  e,
cu_clop(f, cuex_t, int, int)  ,
int  j_top 

Transforms e by replacing each free de Bruijn variable with f (lr, lr_top), where lr is the de Bruijn index and lr_top is j_top plus the binding depth at which the variable occurs. j_top is the top level relative to e to consider free, typically 0.

cuex_t cuex_hole ( int  l  ) 

An expression which is bound to the surrounding binding site after skipping l levels. That is, with l = 0 binds to the immediate surrounding binding site.

cu_bool_t cuex_is_hole ( cuex_t  e  ) 

True iff e is a de Bruijn variable.

int cuex_max_binding_depth ( cuex_t  e  ) 

The maximum number of binding sites, according to cuex_og_binder_contains, which needs to be crossed to reach any leaf of e.

cu_bool_t cuex_opr_is_binder ( cuex_meta_t  opr  ) 

True iff opr binds a de Bruijn variable. A binding can only bind one such variable.

cucon_pmap_t cuex_unfolded_fv_sets ( cuex_t  e,
int  max_binding_depth 

Returns the map {xS}, where x corresponds to a μ-bind subexpression of e, and S is a cucon_uset of the de Bruijn indices of the free λ-variables of the body of the μ-bind. Each key x is a left-associated CUEX_O2_METAPAIR list of all μ-bind expressions down to and including the one S applies to.

As an optimisation, a known result of cuex_max_binding_depth may be passed for max_binding_depth, otherwise pass -1.

Generated 2009-11-23 for culibs-0.25 using Doxygen. Maintained by Petter Urkedal.