Substitutions are here implemented as maps from variables to equivalence sets of variables and value-expressions. A cuex_subst_t has a specified set of active quantification kinds. cuex_subst_unify will attempt to extend the substitution so as to unify two expressions by adding bindings for variables with active quantification. Unification can produce variable equivalences of the form x = y where x and y are variables, or bindings of the form x = e where e is an expression. This is handled by mapping each variable x to (S, e), where S is the set of x and all variables equivalent to it and e is an optional binding for all variables in S. (S, e) is represented by cuex_veqv and is shared between variables in S.
| cuex_t cuex_subst_apply | ( | cuex_subst_t | subst, | |
| cuex_t | ex | |||
| ) |
Return the application of subst to ex.
| void cuex_subst_block | ( | cuex_subst_t | subst, | |
| cuex_var_t | v | |||
| ) |
Block v from being unified with non-variables.
| void cuex_subst_delete | ( | cuex_subst_t | subst | ) |
Indicate that subst is no longer in use. This is just an optimisation, you never need to call this.
| void cuex_subst_dump | ( | cuex_subst_t | subst, | |
| FILE * | file | |||
| ) |
Debug dump of subst.
| cuex_t cuex_subst_expand | ( | cuex_subst_t | subst, | |
| cuex_t | ex | |||
| ) |
Return ex with a single expansion of variabels from subst. This also works for non-idempotent substitutions.
| void cuex_subst_flatten | ( | cuex_subst_t | subst | ) |
Merge all relevant bindings from inherited substitutions of subst into subst, and drop the inheritance.
| cu_bool_t cuex_subst_free_vars_conj | ( | cuex_subst_t | subst, | |
| cuex_t | ex, | |||
| cu_clop(cb, cu_bool_t, cuex_var_t) | ||||
| ) |
Sequentially conjunct cb over variables that would be left after applying subst to ex. For variables in ex which are part of an equavalence, cb is called with the primary variable.
| void cuex_subst_free_vars_erase | ( | cuex_subst_t | subst, | |
| cuex_t | ex, | |||
| cucon_pset_t | accu | |||
| ) |
Erase each variable that would be left after applying subst to ex from accu.
| void cuex_subst_free_vars_insert | ( | cuex_subst_t | subst, | |
| cuex_t | ex, | |||
| cucon_pset_t | accu | |||
| ) |
Insert each variable that would be left after applying subst to ex into accu.
| void cuex_subst_freshen_and_block_vars_in | ( | cuex_subst_t | subst, | |
| cuex_t | ex | |||
| ) |
For each variable in ex which does not have a mapping, insert a substitution from it to a fresh blocked variable.
| void cuex_subst_init | ( | cuex_subst_t | subst, | |
| cuex_qcset_t | qcset | |||
| ) |
Construct subst where variables of quantisation in qcset are unifiable (substitutable).
| cu_bool_t cuex_subst_is_identity | ( | cuex_subst_t | subst | ) |
True iff subst is the identity substitution.
| void cuex_subst_iter_veqv | ( | cuex_subst_t | subst, | |
| cu_clop(cb, void, cuex_veqv_t) | ||||
| ) |
Call cb for each veqv in subst.
| void cuex_subst_iter_veqv_cache | ( | cuex_subst_t | subst, | |
| size_t | cache_size, | |||
| cu_clop(f, void, cuex_veqv_t veqv, void *cache, void *sub_data) | ||||
| ) |
Call f for each veqv in subst. To each cuex_veqv_t a unique cache slot of cache_size bytes is passed to f. f may request the cache data of another variable to be computed before returing, but calling cuex_subst_iter_veqv_cache_sub on the provided sub_data.
| void* cuex_subst_iter_veqv_cache_sub | ( | void * | sub_data, | |
| cuex_t | var | |||
| ) |
This is used only inside the callback of cuex_subst_iter_veqv_cache. It forces a computation of cache data for var before finishing the current callback. It is unsafe to use this on non-idempotent substitutions.
| cuex_t cuex_subst_lookup | ( | cuex_subst_t | subst, | |
| cuex_var_t | var | |||
| ) |
Return the mapping of var in subst. If there is no mapping to non-variables, return the primary variable.
| cuex_subst_t cuex_subst_new | ( | cuex_qcset_t | qcset | ) |
Return a substitution with qcset as the quantisation of variables which are substitutable.
| cuex_subst_t cuex_subst_new_clone | ( | cuex_subst_t | src_subst, | |
| cuex_qcset_t | qcset | |||
| ) |
Return a shallow copy of src_subst, which may be NULL.
| cuex_subst_t cuex_subst_new_copy | ( | cuex_subst_t | src_subst | ) |
Return a deep copy of subst.
| void cuex_subst_print | ( | cuex_subst_t | subst, | |
| cufo_stream_t | fos, | |||
| char const * | sep | |||
| ) |
Print subst to file, using sep to separate elements.
| size_t cuex_subst_size | ( | cuex_subst_t | subst | ) |
The number of variables in subst, possible counting variables which have been shadowed after cloning and modifying a substitution. For cloned substitutions this is just for estimation, since treatment of shadowing is inherently unpredictable.
| cuex_subst_t cuex_subst_tran_cache | ( | cuex_subst_t | subst, | |
| size_t | cache_size, | |||
| cu_clop(f, cuex_t, cuex_t value, void *cache, void *sub_data) | ||||
| ) |
Transform all bindings in subst with f. f is passed a cache of cache_size bytes, where it can store auxiliary data used during the computation. The cache associated with a set of equivalent variables can be queried with cuex_subst_tran_cache_sub, which will force the given variable to be processed if necessary.
| void* cuex_subst_tran_cache_sub | ( | void * | sub_data, | |
| cuex_t | var | |||
| ) |
This is used only inside the callback of cuex_subst_tran_cache. It forces a computation of cache data for var. It is unsafe to use this on non-idempotent substitutions.
| void cuex_subst_unblock | ( | cuex_subst_t | subst, | |
| cuex_var_t | v | |||
| ) |
Remove a unification-block of v.
| void cuex_subst_unblock_all | ( | cuex_subst_t | subst | ) |
Remove all unification-blocks for variables in subst.
| cu_bool_t cuex_subst_unify | ( | cuex_subst_t | subst, | |
| cuex_t | ex0, | |||
| cuex_t | ex1 | |||
| ) |
Attempt to unify ex0 and ex1 while respecting and adding new variable unifications in subst. If both ex0 and ex1 are valueless variables, the primary variable of ex1 is preserved.
| cuex_t cuex_subst_unify_aux | ( | cuex_subst_t | subst, | |
| cuex_t | ex0, | |||
| cuex_t | ex1, | |||
| cu_clop(aux_unify, cuex_t, cuex_subst_t, cuex_t, cuex_t) | ||||
| ) |
Attempt to unify ex0 and ex1 while respecting and adding new variable unifications in subst. If both ex0 and ex1 are valueless variables, the primary variable of ex1 is preserved. Whenever unification fails for pair of subexpressions, the result of aux_unify is used instead.
| void cuex_subst_update_tvar_types | ( | cuex_subst_t | subst, | |
| cuex_t | ex | |||
| ) |
Update each cuex_tvar_t type in ex to the result of applying subst to it.
| cuex_veqv_it_t cuex_veqv_begin | ( | cuex_veqv_t | vq | ) |
An iterator to the first variable in vq.
| cuex_veqv_it_t cuex_veqv_end | ( | cuex_veqv_t | vq | ) |
An iterator beyond the range of variables in vq.
| cu_bool_t cuex_veqv_is_feedback | ( | cuex_veqv_t | vq | ) |
After calling cuex_subst_mark_min_feedback or cuex_subst_mark_all_feedback, and before any further change to the substitution, this will return true iff the variables of vq are part of a minimum feedback set or which are strongly connected, rsp. Useful only for non-idempotent substitutions.
| cuex_var_t cuex_veqv_it_get | ( | cuex_veqv_it_t | it | ) |
The variable at it.
| cuex_veqv_it_t cuex_veqv_it_next | ( | cuex_veqv_it_t | it | ) |
The iterator next after it in a range of variables.
| cuex_var_t cuex_veqv_primary_var | ( | cuex_veqv_t | vq | ) |
The primary variable of vq.
| cuex_qcode_t cuex_veqv_qcode | ( | cuex_veqv_t | vq | ) |
The quantification of variables in vq.
| cuex_t cuex_veqv_value | ( | cuex_veqv_t | vq | ) |
The value of variables in vq or NULL if unknown.