diff options
Diffstat (limited to 'sucl/rewr.icl')
| -rw-r--r-- | sucl/rewr.icl | 215 |
1 files changed, 0 insertions, 215 deletions
diff --git a/sucl/rewr.icl b/sucl/rewr.icl deleted file mode 100644 index 4b584ae..0000000 --- a/sucl/rewr.icl +++ /dev/null @@ -1,215 +0,0 @@ -implementation module rewr - -// $Id$ - -import rule -import graph -import pfun -import basic -import StdEnv - -/* - -Rewriting of graphs - -Exported identifiers: -\begin{description} -\item[\tt unfold] Apply a rewrite rule to a graph -\item[\tt xunfold] As {\tt unfold}, but also provides full matching - from the applied rule to the (resulting) subject - graph -\item[\tt fold] Apply a rewrite rule in reverse to a graph -\item[\tt instantiate] Instantiate a graph with a pattern -\end{description} - -Temporarily hidden: -\begin{description} -\item[\tt build] Build a copy of a graph -\end{description} - -Temporarily not exported: -\begin{description} -\item[\tt getmap] Determine mapping from one graph to another -\item[\tt existmap] Determine if a mapping from one graph to another exists -\end{description} - -> %export foldfn getmapping instantiate xunfold - - unfold - :: pfun *** ** -> || Mapping as result from match of lhs - rule * *** -> || Rule to unfold - ([**],graph * **,**) -> || Heap,graph,node - ([**],graph * **,**) || New heap,graph,node - -> xunfold -> :: ** -> || Root of the redex to unfold -> rule * *** -> || Rule to unfold by -> ( [**], || Unused heap -> **, || Root of subject -> graph * **, || Subject graph -> pfun *** ** || Matching of pattern from rule to subject -> ) -> -> ( [**], || Remaining heap -> **, || Possibly redirected root of subject -> graph * **, || Extended subject graph -> pfun *** ** || Extended matching from rule to subject -> ) - - fold - :: pfun *** ** -> || Mapping as result from match of rhs - rule * *** -> || Rule to fold - ([**],graph * **,**) -> || Heap,graph,node - ([**],graph * **,**) || New heap,graph,node - -> build -> :: graph * *** -> *** -> || Graph,root to be copied -> ([**],[**],graph * **,pfun *** **) -> || Heap,init nodes,init graph,init mapping -> ([**],[**],graph * **,pfun *** **) || New heap,new nodes,new graph,new mapping - -> getmap :: graph * *** -> *** -> graph * ** -> ** -> pfun *** ** - -> existmap :: graph * *** -> *** -> graph * ** -> ** -> bool - - -Implementation - -> %include "basic.lit" -> %include "pfun.lit" -> %include "graph.lit" -instantiate -> %include "rule.lit" - -*/ - -xunfold - :: var - (Rule sym pvar) - !( [var] - , var - , Graph sym var - , Pfun pvar var - ) - -> ( [var] - , var - , Graph sym var - , Pfun pvar var - ) | == var & == pvar - -xunfold redexroot rule (heap,root,subject,matching) -= (heap`,redirection root,redirectgraph redirection subject`,matching`) - where (heap`,[rhs`:_],subject`,matching`) - = build (rulegraph rule) (ruleroot rule) (heap,[],subject,matching) - redirection = adjust redexroot rhs` id - -rewrinstantiate - :: .(Graph sym pvar) // Pattern to instantiate with - pvar // Root of the pattern - var // Open node to instantiate - (.[var],.Graph sym var) // Heap,graph - -> .([var],Graph sym var) // New heap,graph - | == var - & == pvar - -rewrinstantiate pattern proot node (heap,graph) -| not closed -= (heap,graph) -= (heap``,graph``) - where (heap``,params``,graph``,_) - = foldr (build pattern) (heap,[],graph`,extend proot node emptypfun) params - (closed,(f,params)) = varcontents pattern proot - graph` = updategraph node (f,params``) graph - -build - :: (Graph sym pvar) - pvar - ( [var] - , [var] - , Graph sym var - , !Pfun pvar var - ) - -> ( [var] - , [var] - , Graph sym var - , Pfun pvar var - ) | == var & == pvar - -build pattern node (heap,nodes,graph,mapping) -| seen -= (heap,[seenas:nodes],graph,mapping) -| not closed -= (heap`,[node`:nodes],graph,mapping`) -= (heap``,[node`:nodes],graph``,mapping``) - where (seen,seenas) = apply mapping node - [node`:heap`] = heap - mapping` = extend node node` mapping - (closed,(f,params)) = varcontents pattern node - (heap``,params``,graph``,mapping``) - = foldr (build pattern) (heap`,[],graph`,mapping`) params - graph` = updategraph node` (f,params``) graph - -/* -Mapping - -> getmap pattern patnode graph node -> = getmapping nomatch pattern graph (patnode,node) id emptypfun -> where nomatch = error "getmap: pattern and graph do not match" - -> existmap pattern patnode graph node -> = getmapping False pattern graph (patnode,node) (const True) emptypfun -*/ - -getmapping - :: tsym - (Graph sym pvar) - (Graph sym var) - !(pvar,var) - ((Pfun pvar var) -> tsym) - !(Pfun pvar var) - -> tsym - | == sym - & == var - & == pvar - -getmapping failure patgraph graph (patnode,node) success mapping -| seen -= if (seenas==node) (success mapping) failure -| not patdef -= success mapping` -| not (def && patfunc==func && eqlen patargs args) -= failure -= foldr (getmapping failure patgraph graph) success (zip2 patargs args) mapping` - where (seen,seenas) = apply mapping patnode - (patdef,(patfunc,patargs)) = varcontents patgraph patnode - (def,(func,args)) = varcontents graph node - mapping` = extend patnode node mapping - -/* -The foldfn operation folds an area of a graph back to a function call. -The following two conditions must be satisfied in order not to need a -heap of fresh nodes: - - 1: At least one node is freed by the fold operation to hold the root of - the redex. This is the root of the reduct; since it must be freed, - the rule that is folded by must not be a projection function; - - 2: No other new nodes are necessary. Therefore, all nodes of the - pattern of the rule that is folded by except the root must also - occur in the replacement. - -Furthermore, the pattern of the rule is only given by its root symbol -and its arguments; the arguments are open nodes. - -*/ - -foldfn - :: (Pfun pvar var) // Matching of replacement - sym // Symbol at root of pattern - [pvar] // Arguments of pattern - pvar // Root of replacement - (Graph sym var) // Subject graph - -> Graph sym var // Folded subject - | == pvar - -foldfn matching symbol arguments replacementroot sgraph -= updategraph (domatching replacementroot) (symbol,map domatching arguments) sgraph - where domatching = total nomatching matching - nomatching = abort "foldfn: no matching of argument of pattern" |