/**
 * 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))>)