cuex/algo.h: Algorithms on Expressions and Substitutions
[cuex: Expressions]

Data Structures

struct  cuex_stats

Typedefs

typedef struct cuex_stats cuex_stats_t

Functions

cu_rank_t cuex_max_arity (cuex_t e)
int cuex_max_depth (cuex_t e)
cu_bool_t cuex_match_pmap (cuex_t patn, cuex_t e, cucon_pmap_t pmap)
cuex_t cuex_unify (cuex_t x, cuex_t y)
cuex_t cuex_fallback_tran (cuex_t e, cu_clop(f, cuex_t, cuex_t))
cu_bool_t cuex_depth_conj_vars (cuex_t e, cu_clop(f, cu_bool_t, cuex_var_t))
cu_bool_t cuex_depthout_conj (cuex_t e, cu_clop(f, cu_bool_t, cuex_t))
cuex_t cuex_depthout_tran (cuex_t e, cu_clop(f, cuex_t, cuex_t))
cuex_t cuex_depth_tran_leaves (cuex_t e, cu_clop(f, cuex_t, cuex_t))
cuex_t cuex_depth_tran_vars (cuex_t e, cu_clop(f, cuex_t, cuex_var_t))
cu_bool_t cuex_maxtrees_of_leaftest_iter (cuex_t e, cu_clop(pred, cu_bool_t, cuex_t leaf), cu_clop(out, void, cuex_t subex))
cuex_t cuex_maxtrees_of_leaftest_tran (cuex_t e, cu_clop(pred, cu_bool_t, cuex_t leaf), cu_clop(tran, cuex_t, cuex_t subex))
cu_bool_t cuex_has_weak_var (cuex_t e)
cu_bool_t cuex_lgr (cuex_t ex0, cuex_t ex1, cuex_subst_t subst)
cuex_t cuex_msg_unify (cuex_t e0, cuex_t e1, cu_clop(unify, cuex_t, cuex_t e0sub, cuex_t e1sub))
cuex_t cuex_msg_unify_by_arr (size_t cnt, cuex_t *arr, cu_clop(unify, cuex_t, cuex_t *arr))
size_t cuex_count_unique_nodes (cuex_t e)
size_t cuex_count_unique_nodes_except (cuex_t e, cucon_pmap_t exclude)
cu_bool_t cuex_contains_var_in_pmap (cuex_t e, cucon_pmap_t pmap)
cu_bool_t cuex_contains_ex (cuex_t e, cuex_t sub)
cuex_t cuex_substitute_ex (cuex_t e, cuex_t var, cuex_t value)
cuex_t cuex_substitute_pmap (cuex_t e, cucon_pmap_t pmap)
cuex_t cuex_leftmost_with_meta (cuex_t e, cuex_meta_t meta)
cuex_t cuex_rightmost_with_meta (cuex_t e, cuex_meta_t meta)
cu_idr_t cuex_leftmost_idr (cuex_t e)
cu_idr_t cuex_rightmost_idr (cuex_t e)
cuex_var_t cuex_leftmost_var (cuex_t e, cuex_qcset_t qcset)
cuex_var_t cuex_rightmost_var (cuex_t e, cuex_qcset_t qcset)
int cuex_opr_depth_at (cuex_meta_t opr, int i, cuex_t e)
int cuex_binary_left_depth (cuex_meta_t opr, cuex_t e)
int cuex_binary_right_depth (cuex_meta_t opr, cuex_t e)
cuex_t cuex_binary_left_subex (cuex_meta_t opr, cuex_t e, int depth)
cuex_t cuex_binary_right_subex (cuex_meta_t opr, cuex_t e, int depth)
cuex_t cuex_binary_inject_left (cuex_meta_t opr, cuex_t e, cuex_t lhs)
cu_bool_t cuex_free_vars_conj (cuex_t e, cuex_qcset_t qcset, cucon_pset_t excl, cu_clop(fn, cu_bool_t, cuex_var_t, cucon_pset_t))
void cuex_free_vars_insert (cuex_t e, cuex_qcset_t qcset, cucon_pset_t excl, cucon_pset_t accu)
void cuex_free_vars_erase (cuex_t e, cuex_qcset_t qcset, cucon_pset_t excl, cucon_pset_t accu)
int cuex_free_vars_count (cuex_t e, cuex_qcset_t qcset, cucon_pset_t excl)
cuex_t cuex_free_vars_tran (cuex_t e, cuex_qcset_t qcset, cucon_pset_t excl, cu_clop(f, cuex_t, cuex_t, cucon_pset_t))
cuex_t cuex_free_vars_tran_pmap (cuex_t e, cuex_qcset_t qcset, cucon_pset_t excl, cucon_pmap_t subst)
cuex_t cuex_outmost_quantify_vars (cuex_meta_t opr, cucon_pset_t vars, cuex_t e)
 cu_clos_edec (cuex_pset_curried_insert_ex, cu_prot(cu_bool_t, cuex_t e),(cucon_pset_t accu;))
 cu_clos_edec (cuex_pset_curried_erase_ex, cu_prot(cu_bool_t, cuex_t e),(cucon_pset_t accu;))
void cuex_stats (cuex_t e, cuex_stats_t *stats)
cuex_t cuex_autoquantify_uvw_xyz (cuex_t e, cucon_pmap_t env)

Typedef Documentation

typedef struct cuex_stats cuex_stats_t

The statistics returned by cuex_stats.


Function Documentation

int cuex_binary_left_depth ( cuex_meta_t  opr,
cuex_t  e 
)
int cuex_binary_right_depth ( cuex_meta_t  opr,
cuex_t  e 
)
size_t cuex_count_unique_nodes ( cuex_t  e  ) 

The number of subexpressions, variables, and objects in e, counting duplicates only once.

size_t cuex_count_unique_nodes_except ( cuex_t  e,
cucon_pmap_t  exclude 
)

The number of subexpressions, variables, and objects in e, counting duplicates only once, excluding exclude, and adding all the counted items to exclude.

cu_bool_t cuex_depth_conj_vars ( cuex_t  e,
cu_clop(f, cu_bool_t, cuex_var_t)   
)

Sequentially conjunct f over variables in e in depth-first order.

cuex_t cuex_depth_tran_leaves ( cuex_t  e,
cu_clop(f, cuex_t, cuex_t  
)

Transform the leaves of e with f in depth-first order.

cuex_t cuex_depth_tran_vars ( cuex_t  e,
cu_clop(f, cuex_t, cuex_var_t)   
)

Transform the variables of e with f in depth-first order.

cu_bool_t cuex_depthout_conj ( cuex_t  e,
cu_clop(f, cu_bool_t, cuex_t  
)

Sequentially conjunct f over all nodes in e in depth-first leaf-to-root order.

cuex_t cuex_depthout_tran ( cuex_t  e,
cu_clop(f, cuex_t, cuex_t  
)

Transform each node of e with f in depth-first leaf-to-root order.

cuex_t cuex_fallback_tran ( cuex_t  e,
cu_clop(f, cuex_t, cuex_t  
)

Returns cu_call(f, e) if non-NULL, else if e is an operation, returns it with each operand transformed by a recursive call to this function, else (if e is not and operation) returns e. This function handles transformations of ACI trees.

This is quite generally applicable for doing deep transformations. It is based on the idea that f will either know how to handle a certain operator, in which case it can pre-process, invoke cuex_fallback_tran recursively, re-construct, and post-process, or it will not know the form, in which case it typically has no need for any of the processing except for the fall-back recursion and re-construction.

cu_bool_t cuex_free_vars_conj ( cuex_t  e,
cuex_qcset_t  qcset,
cucon_pset_t  excl,
cu_clop(fn, cu_bool_t, cuex_var_t, cucon_pset_t  
)

Do a sequential conjunction of fn over the free variables in e quantified as one of qcset, except for those in excl. excl may be NULL. The second argument to fn is excl augmented with locally bound variables at the current spot.

A variable which is the first operand of a scoping group, or which is a label in a labelling at said position, is considered to be bound in the remaining operands and in the right-hand sides of the labelling. This algorithm supports compounds.

Note:
excl must be thread local, as it is modified and restored by the algorithm.
int cuex_free_vars_count ( cuex_t  e,
cuex_qcset_t  qcset,
cucon_pset_t  excl 
)

The number of free variables in e with quantification in qcset, excluding excl if non-NULL.

void cuex_free_vars_erase ( cuex_t  e,
cuex_qcset_t  qcset,
cucon_pset_t  excl,
cucon_pset_t  accu 
)

Calls ref cuex_free_vars_conj with a callback that erases elements from accu.

void cuex_free_vars_insert ( cuex_t  e,
cuex_qcset_t  qcset,
cucon_pset_t  excl,
cucon_pset_t  accu 
)

Calls ref cuex_free_vars_conj with a callback that inserts elements into accu.

cuex_t cuex_free_vars_tran ( cuex_t  e,
cuex_qcset_t  qcset,
cucon_pset_t  excl,
cu_clop(f, cuex_t, cuex_t, cucon_pset_t  
)

Transforms e by replacing each free variable of quantification among qcset with their mapping under f. excl is the current set of variable considered bound; it's modified in-place and restored.

cuex_t cuex_free_vars_tran_pmap ( cuex_t  e,
cuex_qcset_t  qcset,
cucon_pset_t  excl,
cucon_pmap_t  subst 
)

Returns the result of substituting each free variable in e which has quantification among qcset and occurs in the domain of subst, with their respective mapping from subst. excl is the current set of variables considered bound; it's modified in-place and restored.

cu_idr_t cuex_leftmost_idr ( cuex_t  e  ) 

The leftmost identifier in e.

Precondition:
e must not contain ACI operators.
cuex_var_t cuex_leftmost_var ( cuex_t  e,
cuex_qcset_t  qcset 
)

The leftmost variable in e having quantification in qcset.

Precondition:
e must not contain ACI operators.
cuex_t cuex_leftmost_with_meta ( cuex_t  e,
cuex_meta_t  meta 
)

Return the leftmost leaf of e with the meta meta.

cu_rank_t cuex_max_arity ( cuex_t  e  ) 

The maximum arity of e and any of it's subexpressions. Compounds are checked for subexpressions, but count only as 1 themselves.

int cuex_max_depth ( cuex_t  e  ) 

The depth of the deepest branch of e. The depth of non-operations are considered to be 0, and μ-recursions are ignored.

cu_bool_t cuex_maxtrees_of_leaftest_iter ( cuex_t  e,
cu_clop(pred, cu_bool_t, cuex_t leaf)  ,
cu_clop(out, void, cuex_t subex)   
)

Call out with the maximum subtrees of e for which pred holds true on all leaves.

cuex_t cuex_maxtrees_of_leaftest_tran ( cuex_t  e,
cu_clop(pred, cu_bool_t, cuex_t leaf)  ,
cu_clop(tran, cuex_t, cuex_t subex)   
)

Return the result of transforming with tran all maximum subtrees of e for which pred holds true on all leaves. E.g. if pred checks if a leaf is constant, then this function transforms (x + 9) ⋅ (2 + (1 + 1)) to (x + tran(9)) ⋅ tran(2 + (1 + 1)) with tran evaluated.

cuex_t cuex_msg_unify ( cuex_t  e0,
cuex_t  e1,
cu_clop(unify, cuex_t, cuex_t e0sub, cuex_t e1sub)   
)

Computes the most specific structural generalisation of e0 and e1. Subexpressions of e0 and e1 which are different are replaced by unify(e0sub, e1sub). Typical use is for unify to return a new variable, and possibly record the mismatching sub-expressions.

cuex_t cuex_msg_unify_by_arr ( size_t  cnt,
cuex_t arr,
cu_clop(unify, cuex_t, cuex_t *arr)   
)

A variant of cuex_msg_unify which compares any number of terms simultaneously.

int cuex_opr_depth_at ( cuex_meta_t  opr,
int  i,
cuex_t  e 
)

Returns the number of occurrences of opr from the top of e, following operand number i.

cuex_t cuex_outmost_quantify_vars ( cuex_meta_t  opr,
cucon_pset_t  vars,
cuex_t  e 
)

Returns e if vars is empty, else return cuex_opn(opr, v, vars ∖ * {v}) for some v in vars.

Precondition:
opr must be binary.
cu_idr_t cuex_rightmost_idr ( cuex_t  e  ) 

The rightmost identifier in e.

Precondition:
e must not contain ACI operators.
cuex_var_t cuex_rightmost_var ( cuex_t  e,
cuex_qcset_t  qcset 
)

The rightmost variable in e having quantification in qcset.

Precondition:
e must not contain ACI operators.
cuex_t cuex_rightmost_with_meta ( cuex_t  e,
cuex_meta_t  meta 
)

Return the rightmost leaf of e with the meta meta.

void cuex_stats ( cuex_t  e,
cuex_stats_t stats 
)

Make some statistics of e.

cuex_t cuex_substitute_ex ( cuex_t  e,
cuex_t  var,
cuex_t  value 
)

Return the result of substituting var with value in e.

cuex_t cuex_substitute_pmap ( cuex_t  e,
cucon_pmap_t  pmap 
)

Return the result of substituting in e all keys of pmap with their values, where pmap maps from cuex_t to cuex_t

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