diff options
| -rw-r--r-- | sucl/extract.icl | 8 | ||||
| -rw-r--r-- | sucl/graph.dcl | 9 | ||||
| -rw-r--r-- | sucl/graph.icl | 61 | ||||
| -rw-r--r-- | sucl/history.dcl | 9 | ||||
| -rw-r--r-- | sucl/history.icl | 35 | ||||
| -rw-r--r-- | sucl/loop.icl | 5 | ||||
| -rw-r--r-- | sucl/newfold.icl | 52 | ||||
| -rw-r--r-- | sucl/rewr.dcl | 2 | ||||
| -rw-r--r-- | sucl/rewr.icl | 4 | ||||
| -rw-r--r-- | sucl/spine.dcl | 12 | ||||
| -rw-r--r-- | sucl/spine.icl | 293 |
11 files changed, 172 insertions, 318 deletions
diff --git a/sucl/extract.icl b/sucl/extract.icl index e0c738e..b2d0e46 100644 --- a/sucl/extract.icl +++ b/sucl/extract.icl @@ -70,7 +70,8 @@ actualfold :: [(pvar,Graph sym pvar)] (Rule sym var) -> Optional (Rule sym var,[Rgraph sym var]) - | == var + | == sym + & == var & == pvar actualfold deltanodes rnfnodes foldarea self foldcont hist rule @@ -100,7 +101,8 @@ findoccs :: (Rule sym var) var -> [[(pvar,var)]] - | == var + | == sym + & == var & == pvar findoccs hist rule rnode @@ -120,8 +122,6 @@ findoccs hist rule rnode where inner = map (lookup mapping) (fst (graphvars hgraph [hroot])) outer = removeMembers (varlist (prunegraph rnode rgraph) [rroot:rargs]) [rnode] -instantiate = undef - /* ------------------------------------------------------------------------ diff --git a/sucl/graph.dcl b/sucl/graph.dcl index eef57a7..3300097 100644 --- a/sucl/graph.dcl +++ b/sucl/graph.dcl @@ -218,3 +218,12 @@ compilegraph :: ![(var,Node sym var)] -> Graph sym var extgraph :: (Graph sym var) (Graph sym pvar) [pvar] (Pfun pvar var) (Graph sym var) -> Graph sym var | == var & == pvar instance == (Graph sym var) | == sym & == var + +instantiate :: + (Graph sym pvar,Graph sym var) + (pvar,var) + ([(pvar,var)],[(pvar,var)],[(pvar,var)]) + -> ([(pvar,var)],[(pvar,var)],[(pvar,var)]) + | == sym + & == var + & == pvar diff --git a/sucl/graph.icl b/sucl/graph.icl index 8812b9a..2929125 100644 --- a/sucl/graph.icl +++ b/sucl/graph.icl @@ -229,31 +229,50 @@ Uses in Miranda: * extract.lit.m: used to find instances of patterns in the termination history, while folding trace tips. * transform.lit.m: Uses a different `instantiate' from rewr.lit.m. -> instantiate :: (graph * ***,graph * **) -> (***,**) -> ([(***,**)],[(***,**)],[(***,**)]) -> ([(***,**)],[(***,**)],[(***,**)]) - -> instantiate (pgraph,sgraph) (pnode,snode) (seen,mapping,errs) -> = (seen,mapping,errs), if member seen psnode -> = (psnode:seen,mapping,psnode:errs), if member (map fst seen) pnode -> = (psnode:seen,psnode:mapping,errs), if ~pdef -> = (psnode:seen,mapping,psnode:errs), if ~sdef -> = (psnode:seen,mapping,psnode:errs), if ~(psym=ssym&eqlen pargs sargs) -> = (seen',psnode:mapping',errs'), otherwise -> where (pdef,(psym,pargs)) = nodecontents pgraph pnode -> (sdef,(ssym,sargs)) = nodecontents sgraph snode -> (seen',mapping',errs') = instantiateargs (pgraph,sgraph) (zip2 pargs sargs) (psnode:seen,mapping,errs) -> psnode = (pnode,snode) - `Instantiateargs' is the logical extension of `instantiate' to lists of node pairs. -> instantiateargs :: (graph * ***,graph * **) -> [(***,**)] -> ([(***,**)],[(***,**)],[(***,**)]) -> ([(***,**)],[(***,**)],[(***,**)]) +*/ -> instantiateargs psgraph [] = id -> instantiateargs psgraph (psnode:psnodes) (seen,mapping,errs) -> = (seen'',mapping'',errs'') -> where (seen',mapping'',errs'') = instantiate psgraph psnode (seen,mapping',errs') -> (seen'',mapping',errs') = instantiateargs psgraph psnodes (seen',mapping,errs) +instantiate :: + (Graph sym pvar,Graph sym var) + (pvar,var) + ([(pvar,var)],[(pvar,var)],[(pvar,var)]) + -> ([(pvar,var)],[(pvar,var)],[(pvar,var)]) + | == sym + & == var + & == pvar -*/ +instantiate (pgraph,sgraph) (pnode,snode) (seen,mapping,errs) +| isMember psnode seen + = (seen,mapping,errs) +| isMember pnode (map fst seen) + = ([psnode:seen],mapping,[psnode:errs]) +| not pdef + = ([psnode:seen],[psnode:mapping],errs) +| not sdef + = ([psnode:seen],mapping,[psnode:errs]) +| not (psym==ssym && eqlen pargs sargs) + = ([psnode:seen],mapping,[psnode:errs]) += (seen`,[psnode:mapping`],errs`) + where (pdef,(psym,pargs)) = varcontents pgraph pnode + (sdef,(ssym,sargs)) = varcontents sgraph snode + (seen`,mapping`,errs`) = instantiateargs (pgraph,sgraph) (zip2 pargs sargs) ([psnode:seen],mapping,errs) + psnode = (pnode,snode) + +instantiateargs :: + (Graph sym pvar,Graph sym var) + [(pvar,var)] + ([(pvar,var)],[(pvar,var)],[(pvar,var)]) + -> ([(pvar,var)],[(pvar,var)],[(pvar,var)]) + | == sym + & == var + & == pvar + +instantiateargs psgraph [] sme = sme +instantiateargs psgraph [psnode:psnodes] (seen,mapping,errs) += (seen``,mapping``,errs``) + where (seen`,mapping``,errs``) = instantiate psgraph psnode (seen,mapping`,errs`) + (seen``,mapping`,errs`) = instantiateargs psgraph psnodes (seen`,mapping,errs) :: Matchstate var pvar :== ( [(pvar,var)] // Pattern-subject var combo's already visited diff --git a/sucl/history.dcl b/sucl/history.dcl index d2f68a4..61b0141 100644 --- a/sucl/history.dcl +++ b/sucl/history.dcl @@ -2,6 +2,7 @@ definition module history // $Id$ +from rule import Rgraph from graph import Graph from general import Optional from StdOverloaded import == @@ -12,15 +13,13 @@ from StdOverloaded import == // An association between a node-id in the subject graph and a history pattern :: HistoryAssociation sym var - :== ( var // Attachment point in the subject graph where the history pattern is "housed" - , HistoryPattern sym var // The pattern in the history + :== ( var // Attachment point in the subject graph where the history pattern is "housed" + , [HistoryPattern sym var] // The pattern in the history ) // A pattern in the history, specifying the most general subject graph (footprint) for a reduction sequence :: HistoryPattern sym var - = Closed sym [HistoryPattern sym var] // Indicates a closed node-id in the subject graph (created by a (partial) match) - | OpenHist // Indicates an open node-id in the subject graph (created by instantiation) - | Extensible (Link var) // Indicates a link to an untouched node-id in the subject graph, where this pattern can be extended + :== Rgraph sym var // A link in a graph, indicated by its source node-id and the argument number // The root of a graph can be indicated by the No constructor diff --git a/sucl/history.icl b/sucl/history.icl index a8d7c66..a97ab37 100644 --- a/sucl/history.icl +++ b/sucl/history.icl @@ -15,15 +15,13 @@ import StdEnv // An association between a node-id in the subject graph and a history pattern :: HistoryAssociation sym var - :== ( var // Attachment point in the subject graph where the history pattern is "housed" - , HistoryPattern sym var // The pattern in the history + :== ( var // Attachment point in the subject graph where the history pattern is "housed" + , [HistoryPattern sym var] // The pattern in the history ) // A pattern in the history, specifying the most general subject graph (footprint) for a reduction sequence :: HistoryPattern sym var - = Closed sym [HistoryPattern sym var] // Indicates a closed node-id in the subject graph (created by a (partial) match) - | OpenHist // Indicates an open node-id in the subject graph (created by instantiation) - | Extensible (Link var) // Indicates a link to an untouched node-id in the subject graph, where this pattern can be extended + :== Rgraph sym var // A link in a graph, indicated by its source node-id and the argument number // The root of a graph can be indicated by the No constructor @@ -47,16 +45,17 @@ matchhistory matchhistory hist spinenodes sgraph snode = foldr (checkassoc spinenodes sgraph snode) [] hist -checkassoc spinenodes sgraph snode (var,pat) rest - | isMember var spinenodes && checkpat sgraph pat snode - = [pat:rest] - = rest - -checkpat :: (Graph sym var) (HistoryPattern sym var) var -> Bool | == sym & == var -checkpat sgraph (Closed psym pargs) snode - # (sdef,(ssym,sargs)) = varcontents sgraph snode - = sdef && psym==ssym && eqlen pargs sargs && and [checkpat sgraph parg sarg \\ parg<-pargs & sarg<-sargs] -checkpat sgraph OpenHist snode - = not (fst (varcontents sgraph snode)) -checkpat _ (Extensible _) _ - = True +checkassoc spinenodes sgraph snode (var,pats) rest + = if (isMember var spinenodes) (foldr checkpat rest pats) rest + where checkpat pat rest + = if (isinstance (hgraph,hroot) (sgraph,snode)) [pat:rest] rest + where hgraph = rgraphgraph pat; hroot = rgraphroot pat + +/* +instantiate :: + (HistoryPattern sym pvar) + (Graph sym var) + var + ([(pvar,var)],[(pvar,var)],[(pvar,var)]) + -> ([(pvar,var)],[(pvar,var)],[(pvar,var)]) +*/ diff --git a/sucl/loop.icl b/sucl/loop.icl index 758b07a..88ab3c8 100644 --- a/sucl/loop.icl +++ b/sucl/loop.icl @@ -304,7 +304,7 @@ tryinstantiate onode rpattern anode sargs where success = continue history failinfo True stricts` sroot subject` heap` fail = continue history failinfo` True stricts` sroot subject heap failinfo` = adjust onode [rpattern:failinfo onode] failinfo - (heap`,subject`) = instantiate pgraph proot onode (heap,subject) + (heap`,subject`) = rewrinstantiate pgraph proot onode (heap,subject) proot = rgraphroot rpattern; pgraph = rgraphgraph rpattern stricts` = if instdone stricts (map2 ((||) o (==) onode) sargs stricts) @@ -359,7 +359,8 @@ tryunfold redexroot rule matching spine = xunfold redexroot rule (heap,sroot,subject,matching) noredir = abort "transtree: no mapping foor root of replacement" reductroot = total noredir matching` (ruleroot rule) - history` = extendhistory subject spine history + history` = extendhistory subject redirect spine history + redirect = adjust redexroot reductroot id trace = continue history` failinfo instdone stricts sroot` subject` heap` tryannotate diff --git a/sucl/newfold.icl b/sucl/newfold.icl index 604c60f..3357303 100644 --- a/sucl/newfold.icl +++ b/sucl/newfold.icl @@ -140,8 +140,6 @@ recurse foldarea fnsymbol where rroot = ruleroot rule; rgraph = rulegraph rule newhist` = [(rroot,rgraph):newhist] -foldtips = undef - /* `Foldtips foldarea foldcont hist trace' folds all occurrences of (rooted @@ -150,8 +148,6 @@ which are the results of folding, and a list of areas for which functions must be introduced. If no occurrences were found, Absent is returned. -> addstrict stricts (rule,areas) = (stricts,[rule],areas) - > foldtips :: > (rgraph * **->(*,[**])) -> > (*,[**]) -> @@ -184,6 +180,8 @@ returned. > || exres = (False,mapfst3 only (extract noetrc foldarea trace ([],[],[]))) > exres = (False,newextract noetrc foldarea trace) +> addstrict stricts (rule,areas) = (stricts,[rule],areas) + > noetrc trace area = id > pair x y = (x,y) @@ -191,7 +189,53 @@ returned. > only :: [*] -> * > only [x] = x > only xs = error "only: not a singleton list" +*/ +foldtips :: + ((Rgraph sym var)->(sym,[var])) + (sym,[var]) + -> ([(var,Graph sym var)],[(var,Graph sym var)]) + (Trace sym var pvar) + -> (Bool,([Bool],[Rule sym var],[Rgraph sym var])) + | == sym + & == var + & == pvar + +foldtips foldarea foldcont += ft + where ft hist trace + = ft` transf + where (Trace stricts rule answer history transf) = trace + ft` Stop + = foldoptional exres (pair True o addstrict stricts) (actualfold deltanodes rnfnodes foldarea (==) foldcont (snd hist) rule) + where deltanodes = foldoptional [] getdeltanodes answer + rnfnodes = foldoptional [ruleroot rule] (const []) answer + ft` (Instantiate yestrace notrace) + = ft`` (ft hist yestrace) (ft hist notrace) + where ft`` (False,yessra) (False,nosra) = exres + ft`` (yesfound,(yesstricts,yesrules,yesareas)) (nofound,(nostricts,norules,noareas)) + = (True,(stricts,yesrules++norules,yesareas++noareas)) + ft` (Reduce reductroot trace) + = ft`` (ft (fst hist,fst hist) trace) + where ft`` (False,sra) = exres + ft`` (found,sra) = (True,sra) + ft` (Annotate trace) + = ft`` (ft hist trace) + where ft`` (False,sra) = exres + ft`` (found,sra) = (True,sra) + exres = (False,newextract noetrc foldarea trace) + +addstrict stricts (rule,areas) = (stricts,[rule],areas) + +noetrc trace area = id + +pair x y = (x,y) + +only :: [.elem] -> .elem +only [x] = x +only xs = abort "only: not a singleton list" + +/* ------------------------------------------------------------------------ `Extract foldarea trace (rules,areas)' folds the trace, creating rules diff --git a/sucl/rewr.dcl b/sucl/rewr.dcl index 4f6914a..a36e550 100644 --- a/sucl/rewr.dcl +++ b/sucl/rewr.dcl @@ -43,7 +43,7 @@ getmapping & == var & == pvar -instantiate +rewrinstantiate :: .(Graph sym pvar) // Pattern to instantiate with pvar // Root of the pattern var // Open node to instantiate diff --git a/sucl/rewr.icl b/sucl/rewr.icl index fae1cb6..4b584ae 100644 --- a/sucl/rewr.icl +++ b/sucl/rewr.icl @@ -100,7 +100,7 @@ xunfold redexroot rule (heap,root,subject,matching) = build (rulegraph rule) (ruleroot rule) (heap,[],subject,matching) redirection = adjust redexroot rhs` id -instantiate +rewrinstantiate :: .(Graph sym pvar) // Pattern to instantiate with pvar // Root of the pattern var // Open node to instantiate @@ -109,7 +109,7 @@ instantiate | == var & == pvar -instantiate pattern proot node (heap,graph) +rewrinstantiate pattern proot node (heap,graph) | not closed = (heap,graph) = (heap``,graph``) diff --git a/sucl/spine.dcl b/sucl/spine.dcl index f45a0f5..0aae75a 100644 --- a/sucl/spine.dcl +++ b/sucl/spine.dcl @@ -199,10 +199,10 @@ ifopen :: result result !.(Answer sym var pvar) -> result // Extend the history according to a spine extendhistory - :: (Graph sym var) // Subject graph - (Spine sym var pvar) // Spine leading to the reduction operation - (History sym var) // Old history - -> History sym var // New history - | == sym - & == var + :: (Graph sym var) + (var -> var) + (Spine sym var pvar) + (History sym var) + -> History sym var + | == var & == pvar diff --git a/sucl/spine.icl b/sucl/spine.icl index 735cd95..6bb12b2 100644 --- a/sucl/spine.icl +++ b/sucl/spine.icl @@ -4,6 +4,7 @@ implementation module spine import history import rule +import dnc import graph import pfun import basic @@ -260,276 +261,58 @@ ifopen open other spine -> HistoryPattern sym var // The associated pattern extendhistory - :: (Graph sym var) // Subject graph - (Spine sym var pvar) // Spine leading to the reduction operation - (History sym var) // Old history - -> History sym var // New history - | == sym - & == var + :: (Graph sym var) + (var -> var) + (Spine sym var pvar) + (History sym var) + -> History sym var + | == var & == pvar -extendhistory sgraph spine history - = [newpattern:touchmod history] - where (newpattern,_,extender) - = foldspine extendpair extenddefault extenddefault (extendforce sgraph) extenddefault extendopen (extendpartial sgraph) (const extenddefault) (extendredex sgraph) extenddefault spine No Extensible - touchmod = map (mapsnd (patextend extender)) +extendhistory sgraph redirection spine history += snd (foldspine (extendpair sgraph redirection) d d (const id) d (const d) (extendpartial sgraph) (const d) (extendredex sgraph history) d spine) + where d = (emptygraph,history) -patextend - :: (LinkExtender sym var) - (HistoryPattern sym var) - -> HistoryPattern sym var - -patextend extender (Closed sym args) = Closed sym (map (patextend extender) args) -patextend extender OpenHist = OpenHist -patextend extender (Extensible link) = extender link extendpair - :: var // Subject node-id where spine is rooted - ( var - (Link var) - (LinkExtender sym var) - -> ( HistoryAssociation sym var - , HistoryPattern sym var - , LinkExtender sym var - ) - ) - (Link var) // Link in subject graph to this spine - (LinkExtender sym var) // Input link extender - -> ( HistoryAssociation sym var - , HistoryPattern sym var // Returned history pattern - , LinkExtender sym var // Returned link extender - ) - -extendpair snode extendsub link extender - = extendsub snode link extender - -extenddefault - :: var - (Link var) - (LinkExtender sym var) - -> ( HistoryAssociation sym var - , HistoryPattern sym var - , LinkExtender sym var - ) -extenddefault _ link extender - = (nonewpattern,Extensible link,extender) - where nonewpattern = abort "history: extenddefault: no new pattern for default spine" - -// Extend history for a Force spine -// FIXME: For now, only look at function node and to-be-strict argument -// Forget what was already determined strict -extendforce :: (Graph sym var) - Int - ( (Link var) - (LinkExtender sym var) - -> ( HistoryAssociation sym var - , HistoryPattern sym var - , LinkExtender sym var - ) - ) + (var->var) var - (Link var) - (LinkExtender sym var) - -> ( HistoryAssociation sym var - , HistoryPattern sym var - , LinkExtender sym var - ) + (Graph sym var,History sym var) + -> (Graph sym var,History sym var) | == var -extendforce sgraph argno forcesub snode link extender0 - | not sdef - = abort "history: extendforce: force from open node-id???" - = (newpattern,histpat1,extender2) - where (newpattern,histpat0,extender1) = forcesub (Yes (snode,argno)) extender0 - histpat1 = Closed ssym [argpat i \\ i <- [0..] & _ <- sargs] - argpat i - = if (i==argno) histpat0 (Extensible (Yes (snode,i))) - (sdef,(ssym,sargs)) = varcontents sgraph snode - extender2 = adjust link histpat1 extender1 - -// Extend history patterns according to an Open spine -// FIXME: this should build TWO extended versions: -// one for succesful instantiation -// one for failed instantiation -extendopen - :: rgraph // Pattern to drive instantiation (not used) - var // Node-id in subject graph that was open - (Link var) // Where subject graph pointed to this open node-id - (LinkExtender sym var) // Input link extender - -> ( HistoryAssociation sym var - , HistoryPattern sym var // Pattern for this spine - , LinkExtender sym var // Resulting link extender - ) - | == var - -extendopen _ snode link extender0 - = (newpattern,histpat,extender1) - where histpat = OpenHist - newpattern = (snode,histpat) - extender1 = adjust link histpat extender0 +extendpair sgraph redirect snode (hgraph,history) += (hgraph`,remap (redirect snode) [mkrgraph snode hgraph`:foldmap id [] history snode] (forget snode history)) + where hgraph` = if sdef (updategraph snode scont hgraph) hgraph + (sdef,scont) = dnc (const "in extendpair") sgraph snode extendpartial - :: (Graph sym var) // Subject graph - (Rule sym pvar) // Applied rewrite rule - (Pfun pvar var) // Partial match from rewrite rule's pattern to subject graph - pvar // Node-id in rule where partial match went to subspine - ( (Link var) // Link passed to subspine handler - (LinkExtender sym var) // Link extender input to subspine handler - -> ( HistoryAssociation sym var - , HistoryPattern sym var // Pattern returned for subspine - , LinkExtender sym var // Link extender returned for subspine - ) - ) - var // Node-id in subject with function application - (Link var) // Link to root of partial match in subject graph - (LinkExtender sym var) // Remaining link extender - -> ( HistoryAssociation sym var - , HistoryPattern sym var // History patterns with derived pattern prefixed - , LinkExtender sym var // Extended link extender - ) - | == sym - & == var + :: (Graph sym var) + (Rule sym pvar) + (Pfun pvar var) + pvar + (Graph sym var,History sym var) + -> (Graph sym var,History sym var) + | == var & == pvar -extendpartial sgraph rule matching subnode extendsub snode link restextender - = extendfunction sgraph rule matching ((==)subnode) (const extendsub) snode link restextender +extendpartial sgraph rule matching rnode (hgraph,history) += (extgraph` sgraph rule matching hgraph,history) extendredex - :: (Graph sym var) // Subject graph - (Rule sym pvar) // Applied rewrite rule - (Pfun pvar var) // Partial match from rewrite rule's pattern to subject graph - var // Root of redex in subject graph - (Link var) // Link to root of redex in subject graph - (LinkExtender sym var) // Remaining link extender - -> ( HistoryAssociation sym var - , HistoryPattern sym var // History patterns with derived pattern prefixed - , LinkExtender sym var // Extended link extender - ) - | == sym - & == var - & == pvar - -extendredex sgraph rule matching snode link extender - = extendfunction sgraph rule matching (const False) nosub snode link extender - where nosub = abort "history: extendredex: full match with subspine??" - -extendfunction - :: (Graph sym var) // Subject graph - (Rule sym pvar) // Applied rewrite rule - (Pfun pvar var) // Partial match from rewrite rule's pattern to subject graph - (pvar -> Bool) // Checks whether the subspine applies here - ( (HistoryAssociation sym var) - (Link var) // Link passed to subspine handler - (LinkExtender sym var) // Link extender input to subspine handler - -> ( HistoryAssociation sym var - , HistoryPattern sym var // Pattern returned for subspine - , LinkExtender sym var // Link extender returned for subspine - ) - ) - var // Root of partial match in subject graph - (Link var) // Link to root of partial match in subject graph - (LinkExtender sym var) // Remaining link extender - -> ( HistoryAssociation sym var - , HistoryPattern sym var // History patterns with derived pattern prefixed - , LinkExtender sym var // Extended link extender - ) - | == sym - & == var - & == pvar - -extendfunction sgraph rule matching issub extendsub snode link extender0 - | not sdef - = abort "history: extendfunction: partial or full match at open node-id???" - = (newpattern,thispat,extender2) - where extender2 = adjust link thispat extender1 - thispat = Closed ssym argpatts - (newpattern,argpatts,extender1) = extendnodes sgraph rgraph matching snode issub extendsub thisnewpattern extender0 rargs - (sdef,(ssym,_)) = varcontents sgraph snode - rgraph = rulegraph rule - rargs = arguments rule - thisnewpattern = (snode,thispat) - -extendnodes - :: (Graph sym var) // Subject graph - (Graph sym pvar) // Applied rewrite rule - (Pfun pvar var) // Partial match from rewrite rule's pattern to subject graph - var // Parent node-id in subject graph to this node-id list for creating links - (pvar -> Bool) // Tells if this is where the subspine was attached - ( (HistoryAssociation sym var) - (Link var) // Link passed to subspine handler - (LinkExtender sym var) // Link extender input to subspine handler - -> ( HistoryAssociation sym var - , HistoryPattern sym var // Pattern returned for subspine - , LinkExtender sym var // Link extender returned for subspine - ) - ) - (HistoryAssociation sym var) - (LinkExtender sym var) // Remaining link extender - [pvar] // Node-ids in rule to handle - -> ( HistoryAssociation sym var - , [HistoryPattern sym var] // History patterns with derived pattern prefixed - , LinkExtender sym var // Extended link extender - ) - | == sym - & == var + :: (Graph sym var) + (History sym var) + (Rule sym pvar) + (Pfun pvar var) + -> (Graph sym var,History sym var) + | == var & == pvar -extendnodes sgraph rgraph matching sparent issub extendsub newpattern restextender rnodes - = foldr (extendnode sgraph rgraph matching issub extendsub) (newpattern,[],restextender) (zip2 links rnodes) - where links = [Yes (sparent,i)\\i<-[0..]] - -extendnode - :: (Graph sym var) // Subject graph - (Graph sym pvar) // Applied rewrite rule - (Pfun pvar var) // Partial match from rewrite rule's pattern to subject graph - (pvar -> Bool) // Tells if this is where the subspine was attached - ( (HistoryAssociation sym var) - (Link var) // Link passed to subspine handler - (LinkExtender sym var) // Link extender input to subspine handler - -> ( HistoryAssociation sym var - , HistoryPattern sym var // Pattern returned for subspine - , LinkExtender sym var // Link extender returned for subspine - ) - ) - ( Link var // Referring link to current node-id - , pvar // Current node-id in rule - ) - ( HistoryAssociation sym var - , [HistoryPattern sym var] // History patterns to prefix derived patterns to - , (LinkExtender sym var) // Remaining link extender - ) - -> ( HistoryAssociation sym var - , [HistoryPattern sym var] // History patterns with derived pattern prefixed - , (LinkExtender sym var) // Extended link extender - ) - | == sym - & == var - & == pvar +extendredex sgraph history rule matching += (extgraph` sgraph rule matching emptygraph,history) -extendnode sgraph rgraph matching issub extendsub (link,rnode) (newpattern0,rest,extender0) - | issub rnode - = (subnewpattern,[subpattern:rest],subextender) - | rdef - = foldpfun mapped unmapped matching rnode - = unmapped - where (subnewpattern,subpattern,subextender) - = extendsub newpattern0 link extender0 - mapped snode - = (newpattern1,[thispat:rest],extender2) - where extender2 = adjust link thispat extender1 - thispat = Closed rsym argpatts - (newpattern1,argpatts,extender1) = extendnodes sgraph rgraph matching snode issub extendsub newpattern0 extender0 rargs - unmapped - = (newpattern0,[Extensible link:rest],extender0) - (rdef,(rsym,rargs)) = varcontents rgraph rnode - - -/**************** -* Miscellaneous * -****************/ - -instance == (Optional a) | == a - where (==) No No = True - (==) (Yes x1) (Yes x2) = x1==x2 - (==) _ _ = False +extgraph` :: (Graph sym var) (Rule sym pvar) -> (Pfun pvar var) (Graph sym var) -> Graph sym var | == var & == pvar +extgraph` sgraph rule += extgraph sgraph rgraph (varlist rgraph (arguments rule)) + where rgraph = rulegraph rule |