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