00001 /* Part of the culibs project, <http://www.eideticdew.org/culibs/>. 00002 * Copyright (C) 2005--2009 Petter Urkedal <urkedal@nbi.dk> 00003 * 00004 * This program is free software: you can redistribute it and/or modify 00005 * it under the terms of the GNU General Public License as published by 00006 * the Free Software Foundation, either version 3 of the License, or 00007 * (at your option) any later version. 00008 * 00009 * This program is distributed in the hope that it will be useful, 00010 * but WITHOUT ANY WARRANTY; without even the implied warranty of 00011 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 00012 * GNU General Public License for more details. 00013 * 00014 * You should have received a copy of the GNU General Public License 00015 * along with this program. If not, see <http://www.gnu.org/licenses/>. 00016 */ 00017 00018 #ifndef CUEX_ALGO_H 00019 #define CUEX_ALGO_H 00020 00021 #include <cuex/fwd.h> 00022 #include <cuex/var.h> 00023 #include <cu/idr.h> 00024 #include <cucon/fwd.h> 00025 00026 CU_BEGIN_DECLARATIONS 00027 /** \defgroup cuex_algo cuex/algo.h: Algorithms on Expressions and Substitutions 00028 ** @{ \ingroup cuex_mod */ 00029 00030 /** The maximum arity of \a e and any of it's subexpressions. Compounds are 00031 ** checked for subexpressions, but count only as 1 themselves. */ 00032 cu_rank_t cuex_max_arity(cuex_t e); 00033 00034 /** The depth of the deepest branch of \a e. The depth of non-operations are 00035 ** considered to be 0, and μ-recursions are ignored. */ 00036 int cuex_max_depth(cuex_t e); 00037 00038 cu_bool_t cuex_match_pmap(cuex_t patn, cuex_t e, cucon_pmap_t pmap); 00039 00040 cuex_t cuex_unify(cuex_t x, cuex_t y); 00041 00042 /** Returns <code>cu_call(\a f, \a e)</code> if non-\c NULL, else if \a e is 00043 ** an operation, returns it with each operand transformed by a recursive call 00044 ** to this function, else (if \a e is not and operation) returns \a e. This 00045 ** function handles transformations of ACI trees. 00046 ** 00047 ** This is quite generally applicable for doing deep transformations. It is 00048 ** based on the idea that \a f will either know how to handle a certain 00049 ** operator, in which case it can pre-process, invoke cuex_fallback_tran 00050 ** recursively, re-construct, and post-process, or it will not know the form, 00051 ** in which case it typically has no need for any of the processing except for 00052 ** the fall-back recursion and re-construction. */ 00053 cuex_t cuex_fallback_tran(cuex_t e, cu_clop(f, cuex_t, cuex_t)); 00054 00055 /** Sequentially conjunct \a f over variables in \a e in depth-first order. */ 00056 cu_bool_t cuex_depth_conj_vars(cuex_t e, cu_clop(f, cu_bool_t, cuex_var_t)); 00057 00058 /** Sequentially conjunct \a f over all nodes in \a e in depth-first 00059 ** leaf-to-root order. */ 00060 cu_bool_t cuex_depthout_conj(cuex_t e, cu_clop(f, cu_bool_t, cuex_t)); 00061 00062 /** Transform each node of \a e with \a f in depth-first leaf-to-root 00063 ** order. */ 00064 cuex_t cuex_depthout_tran(cuex_t e, cu_clop(f, cuex_t, cuex_t)); 00065 00066 /** Transform the leaves of \a e with \a f in depth-first order. */ 00067 cuex_t cuex_depth_tran_leaves(cuex_t e, cu_clop(f, cuex_t, cuex_t)); 00068 00069 /** Transform the variables of \a e with \a f in depth-first order. */ 00070 cuex_t cuex_depth_tran_vars(cuex_t e, cu_clop(f, cuex_t, cuex_var_t)); 00071 00072 /** Call \a out with the maximum subtrees of \a e for which \a pred holds true 00073 ** on all leaves. */ 00074 cu_bool_t cuex_maxtrees_of_leaftest_iter(cuex_t e, 00075 cu_clop(pred, cu_bool_t, cuex_t leaf), 00076 cu_clop(out, void, cuex_t subex)); 00077 00078 /** Return the result of transforming with \a tran all maximum subtrees of \a e 00079 ** for which \a pred holds true on all leaves. 00080 ** E.g. if \a pred checks if a leaf is constant, then this function 00081 ** transforms (\e x + 9) ⋅ (2 + (1 + 1)) to 00082 ** (\e x + \a tran(9)) ⋅ \a tran(2 + (1 + 1)) with \a tran evaluated. */ 00083 cuex_t cuex_maxtrees_of_leaftest_tran(cuex_t e, 00084 cu_clop(pred, cu_bool_t, cuex_t leaf), 00085 cu_clop(tran, cuex_t, cuex_t subex)); 00086 00087 00088 cu_bool_t cuex_has_weak_var(cuex_t e); 00089 00090 cu_bool_t cuex_lgr(cuex_t ex0, cuex_t ex1, cuex_subst_t subst); 00091 00092 /** Computes the most specific structural generalisation of \a e0 and \a e1. 00093 ** Subexpressions of \a e0 and \a e1 which are different are replaced by 00094 ** <code>unify(\a e0sub, \a e1sub)</code>. Typical use is for \a unify to 00095 ** return a new variable, and possibly record the mismatching 00096 ** sub-expressions. */ 00097 cuex_t cuex_msg_unify(cuex_t e0, cuex_t e1, 00098 cu_clop(unify, cuex_t, cuex_t e0sub, cuex_t e1sub)); 00099 00100 /** A variant of \ref cuex_msg_unify which compares any number of terms 00101 ** simultaneously. */ 00102 cuex_t cuex_msg_unify_by_arr(size_t cnt, cuex_t *arr, 00103 cu_clop(unify, cuex_t, cuex_t *arr)); 00104 00105 /** The number of subexpressions, variables, and objects in \a e, counting 00106 ** duplicates only once. */ 00107 size_t cuex_count_unique_nodes(cuex_t e); 00108 00109 /** The number of subexpressions, variables, and objects in \a e, counting 00110 ** duplicates only once, excluding \a exclude, and adding all the counted 00111 ** items to \a exclude. */ 00112 size_t cuex_count_unique_nodes_except(cuex_t e, cucon_pmap_t exclude); 00113 00114 cu_bool_t cuex_contains_var_in_pmap(cuex_t e, cucon_pmap_t pmap); 00115 00116 cu_bool_t cuex_contains_ex(cuex_t e, cuex_t sub); 00117 00118 /** Return the result of substituting \a var with \a value in \a e. */ 00119 cuex_t cuex_substitute_ex(cuex_t e, cuex_t var, cuex_t value); 00120 00121 /** Return the result of substituting in \a e all keys of \a pmap with their 00122 ** values, where \a pmap maps from \ref cuex_t to \ref cuex_t */ 00123 cuex_t cuex_substitute_pmap(cuex_t e, cucon_pmap_t pmap); 00124 00125 /** Return the leftmost leaf of \a e with the meta \a meta. */ 00126 cuex_t cuex_leftmost_with_meta(cuex_t e, cuex_meta_t meta); 00127 00128 /** Return the rightmost leaf of \a e with the meta \a meta. */ 00129 cuex_t cuex_rightmost_with_meta(cuex_t e, cuex_meta_t meta); 00130 00131 /** The leftmost identifier in \a e. 00132 ** \pre \a e must not contain ACI operators. */ 00133 CU_SINLINE cu_idr_t cuex_leftmost_idr(cuex_t e) 00134 { return (cu_idr_t)cuex_leftmost_with_meta(e, 00135 cuoo_type_to_meta(cu_idr_type())); } 00136 00137 /** The rightmost identifier in \a e. 00138 ** \pre \a e must not contain ACI operators. */ 00139 CU_SINLINE cu_idr_t cuex_rightmost_idr(cuex_t e) 00140 { return (cu_idr_t)cuex_rightmost_with_meta(e, 00141 cuoo_type_to_meta(cu_idr_type())); } 00142 00143 /** The leftmost variable in \a e having quantification in \a qcset. 00144 ** \pre \a e must not contain ACI operators. */ 00145 cuex_var_t cuex_leftmost_var(cuex_t e, cuex_qcset_t qcset); 00146 00147 /** The rightmost variable in \a e having quantification in \a qcset. 00148 ** \pre \a e must not contain ACI operators. */ 00149 cuex_var_t cuex_rightmost_var(cuex_t e, cuex_qcset_t qcset); 00150 00151 /** Returns the number of occurrences of \a opr from the top of \a e, following 00152 ** operand number \a i. */ 00153 int cuex_opr_depth_at(cuex_meta_t opr, int i, cuex_t e); 00154 00155 /** \deprecated Use \ref cuex_opr_depth_at. */ 00156 CU_SINLINE int cuex_binary_left_depth(cuex_meta_t opr, cuex_t e) 00157 { return cuex_opr_depth_at(opr, 0, e); } 00158 00159 /** \deprecated Use \ref cuex_opr_depth_at. */ 00160 CU_SINLINE int cuex_binary_right_depth(cuex_meta_t opr, cuex_t e) 00161 { return cuex_opr_depth_at(opr, 1, e); } 00162 00163 cuex_t cuex_binary_left_subex(cuex_meta_t opr, cuex_t e, int depth); 00164 cuex_t cuex_binary_right_subex(cuex_meta_t opr, cuex_t e, int depth); 00165 00166 cuex_t cuex_binary_inject_left(cuex_meta_t opr, cuex_t e, cuex_t lhs); 00167 00168 /** Do a sequential conjunction of \a fn over the free variables in \a e 00169 ** quantified as one of \a qcset, except for those in \a excl. \a excl may be 00170 ** \c NULL. The second argument to \a fn is \a excl augmented with locally 00171 ** bound variables at the current spot. 00172 ** 00173 ** A variable which is the first operand of a scoping group, or which is a 00174 ** label in a labelling at said position, is considered to be bound in the 00175 ** remaining operands and in the right-hand sides of the labelling. This 00176 ** algorithm supports compounds. 00177 ** 00178 ** \note \a excl must be thread local, as it is modified and restored by the 00179 ** algorithm. */ 00180 cu_bool_t 00181 cuex_free_vars_conj(cuex_t e, cuex_qcset_t qcset, cucon_pset_t excl, 00182 cu_clop(fn, cu_bool_t, cuex_var_t, cucon_pset_t)); 00183 00184 /** Calls \a ref cuex_free_vars_conj with a callback that inserts elements into 00185 ** \a accu. */ 00186 void cuex_free_vars_insert(cuex_t e, cuex_qcset_t qcset, cucon_pset_t excl, 00187 cucon_pset_t accu); 00188 00189 /** Calls \a ref cuex_free_vars_conj with a callback that erases elements from 00190 ** \a accu. */ 00191 void cuex_free_vars_erase(cuex_t e, cuex_qcset_t qcset, cucon_pset_t excl, 00192 cucon_pset_t accu); 00193 00194 /** The number of free variables in \a e with quantification in \a qcset, 00195 ** excluding \a excl if non-\c NULL. */ 00196 int cuex_free_vars_count(cuex_t e, cuex_qcset_t qcset, cucon_pset_t excl); 00197 00198 /** Transforms \a e by replacing each free variable of quantification among \a 00199 ** qcset with their mapping under \a f. \a excl is the current set of 00200 ** variable considered bound; it's modified in-place and restored. */ 00201 cuex_t 00202 cuex_free_vars_tran(cuex_t e, cuex_qcset_t qcset, cucon_pset_t excl, 00203 cu_clop(f, cuex_t, cuex_t, cucon_pset_t)); 00204 00205 /** Returns the result of substituting each free variable in \a e which has 00206 ** quantification among \a qcset and occurs in the domain of \a subst, with 00207 ** their respective mapping from \a subst. \a excl is the current set of 00208 ** variables considered bound; it's modified in-place and restored. */ 00209 cuex_t 00210 cuex_free_vars_tran_pmap(cuex_t e, cuex_qcset_t qcset, cucon_pset_t excl, 00211 cucon_pmap_t subst); 00212 00213 /** Returns \a e if \a vars is empty, else return 00214 ** <code>cuex_opn(\a opr, \e v, vars ∖ * {\e v})</code> for some \e v in \a 00215 ** vars. 00216 ** \pre \a opr must be binary. */ 00217 cuex_t cuex_outmost_quantify_vars(cuex_meta_t opr, cucon_pset_t vars, cuex_t e); 00218 00219 /* Insert e into accum and return true. */ 00220 cu_clos_edec(cuex_pset_curried_insert_ex, 00221 cu_prot(cu_bool_t, cuex_t e), 00222 ( cucon_pset_t accu; )); 00223 00224 /* Erase e from accum and return true. */ 00225 cu_clos_edec(cuex_pset_curried_erase_ex, 00226 cu_prot(cu_bool_t, cuex_t e), 00227 ( cucon_pset_t accu; )); 00228 00229 00230 /** The statistics returned by \ref cuex_stats. */ 00231 typedef struct cuex_stats 00232 { 00233 size_t node_cnt; /*!< total number of nodes */ 00234 size_t var_cnt; /*!< number of variables of any kind */ 00235 size_t strong_var_cnt; 00236 size_t weak_var_cnt; 00237 size_t passive_var_cnt; 00238 size_t other_var_cnt; 00239 size_t opn_cnt; /*!< number of operations */ 00240 size_t obj_cnt; /*!< number of objects (constants) */ 00241 size_t other_node_cnt; 00242 } cuex_stats_t; 00243 00244 /** Make some statistics of \a e. */ 00245 void cuex_stats(cuex_t e, cuex_stats_t *stats); 00246 00247 cuex_t cuex_autoquantify_uvw_xyz(cuex_t e, cucon_pmap_t env); 00248 00249 #ifdef CUCONF_DEBUG_CLIENT 00250 cuex_t cuex_binary_inject_left_D(cuex_meta_t, cuex_t, cuex_t); 00251 #define cuex_binary_inject_left cuex_binary_inject_left_D 00252 #endif 00253 00254 /** @} */ 00255 CU_END_DECLARATIONS 00256 00257 #endif