Defines | |
| #define | CUEX_BI_SIFI_FLAG_PRUNE 1 |
Functions | |
| 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) |
This provides variables, scoping constructs, and algorithms for expressions using de Bruijn indexes. This includes the built-in μ-recursion and λ-expressions.
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.
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.
| 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 {x ↦ S}, 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.