/**
 * The ATerm library preserves maximal sharing of subterms
 * through hash-consing. This sharing is not directly available
 * to the user of an ATerm. For some applications it is necessary
 * to make the implicit sharing in terms explicit in the form of
 * a let construct in which all occurences of a shared subterm
 * are replaced by a symbolic pointer (variable).
 */
module term/share
imports 
  collection/list/set 
  strategy/general/unification 
  term/common

strategies

 /**
  * The strategy share defined in this module achieves such
  * an explicit sharing for arbitrary terms. The approach used by
  * the strategy is to first turn the term into its underlying
  * graph and then inlining those subterms that are not shared
  * (only occur once) or that cannot be shared in this way (upto
  * the needs of an application).
  */
  share(mkvar, always, mklet) = 
	graph(mkvar); 
	inline-graph(always, mklet)

strategies

  edge(mkvar)      = split(address; mkvar, all(address; mkvar))
  list-edge(mkvar) = split(address; mkvar, map(address; mkvar))

 /**
  * The graph of a term is obtained by turning each node
  * \verb|F(t1,...,tn)| into an edge \verb|(a, F(a1,...,an))|,
  * where \verb|a| is the address of the node and the \verb|ai|
  * are the addresses of its direct subterms. The \verb|mkvar|
  * parameter is used to embed the address in some constructor.
  * (If \verb|mkvar| is \verb|id|, nothing is done.)
  * 
  * The first edge in the graph is the root of the tree. By
  * definition it is never shared. The graph can be turned into
  * one big let-expression with the root as its body. That is what
  * the first line of the definition of \verb|inline-graph|
  * accomplishes. 
  * 
  * Subsequently, nodes that are not shared, i.e., a pointer to
  * which only occurs once, can be inlined. Some nodes may always
  * have to be inlined (for application specific reasons). The
  * shape of such nodes is specified by the parameter
  * \verb|always|.  Edges that cannot be inlined are turned into a
  * let-binding the form of which is determined by the parameter
  * \verb|mklet|.
  * 
  * After all graph edges have either been inlined or turned into
  * let-bindings the, now empty, \verb|GraphLet| is discarded and
  * replaced by its body.
  */

  graph(mkvar) = 
    rec x(is-list; split(list-edge(mkvar), map(x); unions); MkCons
                <+ split(edge(mkvar), \ _#(xs) -> xs\ ; map(x); unions); 
                   MkCons)

signature
  constructors
    GraphLet : List(Product([Int, Term])) * Term -> Term

strategies

  inline-graph(always, mklet) = 
	\ [(a, t) | graph] -> GraphLet(graph, t) \ ;
	repeat(
          term-share-inline; (GraphLet([(id,always) | id], id) + term-share-dead) <+ 
          term-share-dead <+
          term-share-dont-inline(mklet));
	\ GraphLet([], t) -> t \

rules

  term-share-inline : 
	GraphLet([(a, skel) | graph], t) ->
	GraphLet([(a, skel) | graph], t')
	where <oncetd((a -> skel))> t => t'

  term-share-dead : 
	GraphLet([(a, skel) | graph], t) -> 
	GraphLet(graph, t)
	where <not(is-subterm)> (a, t)

  term-share-dont-inline(mklet) : 
	GraphLet([(a, skel) | graph], t) -> 
	GraphLet(graph, <mklet>(a, skel, t))