/** * Some primitives for the manipulation of terms. */ module term/common imports strategy/traversal/simple collection/list/common collection/list/set strategies /** * Build a term given a constructor name and a list of terms. * * Note that this primitive strategy has been turned into a language construct. * * The pattern f#(xs) denotes the decomposition of a term into its function symbol * f and its list of arguments xs. This pattern can be used in matching ?f#(xs) * and building !f#(xs) terms (so also in left- and right-hand sides of rules) and * also as a congruence s1#(s2). * * E.g. <mkterm> (f, [t1,...,tn]) builds the constructor application f(t1,...,tn). */ mkterm = ?(c,ts); prim("SSL_mkterm",c,ts) /** * Decompose a term into a constructor name and a list of terms. * * Note that this primitive strategy has been turned into a language construct. * * The pattern f#(xs) denotes the decomposition of a term into its function symbol * f and its list of arguments xs. This pattern can be used in matching ?f#(xs) * and building !f#(xs) terms (so also in left- and right-hand sides of rules) and * also as a congruence s1#(s2). * * E.g. <explode-term> f(t1,...,tn) is the inverse of mkterm and produces (f, [t1,...,tn]). * * Note that explode-term is equivalent to !(<get-constructor>, <get-arguments>). */ explode-term = ?t; prim("SSL_explode_term",t) /** * Get the constructor of a term. * * Note that explode-term is equivalent to !(<get-constructor>, <get-arguments>). */ get-constructor = ?t; prim("SSL_get_constructor", t) /** * Get the arguments of a term. * * Note that explode-term is equivalent to !(<get-constructor>, <get-arguments>). */ get-arguments = ?t; prim("SSL_get_arguments", t) /** * Get the arguments of a term application. */ get-appl-arguments = get-appl-arguments(id) /** * Get the arguments of a term application, applying s to the individual arguments. * * @param a -> b * @type f(a1 ... an) -> [b1 ... bn] */ get-appl-arguments(s) = ?t; prim("SSL_get_appl_arguments_map", s | t) /** * Compare the address of two terms and succeeds if the address of the first is * smaller than the address of the second. * * This predicate induces a total ordering on terms and can be used to sort terms. * Note that this relation is valid in one session (but what happens after * rehashing), but not necessarily between two sessions. */ address-lt = ?(t1,t2); prim("SSL_address_lt",t1,t2) /** * Compare the address of two terms and succeeds if the address of the current * term is smaller than the address of the argument. */ term-address-lt(|t2) = ?t1; prim("SSL_address_lt",t1,t2) /** * Give the address of a term. * * <address> t replaces t with its address (represented as a string). * This can be used to obtain a unique symbolic reference to a term. * * @type t -> String */ address = ?t; prim("SSL_address",t) /** * Give checksum of a term. Similar to atsum from aterm package. */ checksum = ?t ; prim("SSL_checksum",t) strategies crush(nul, sum) : _#(xs) -> <foldr(nul,sum)> xs crush(nul, sum, s) : _#(xs) -> <foldr(nul,sum, s)> xs strategies node-size = crush(!0, add, !1) term-size = crush(!1, add, term-size) strategies at-depth(depth, s) = !(<depth> (), <id>) ; topdown( {d : ?(0, <s> ) <+ ?(d, <id>); all(!(<dec> d, <id>)) } ) /** * Occurence Counting. */ strategies om-occurrences(s) = if s then !1 else crush(!0, add, om-occurrences(s)) end occurrences(s) = <add> (<if s then !1 else !0 end>, <crush(!0, add, occurrences(s))>)