diff options
| -rw-r--r-- | sucl/history.dcl | 21 | ||||
| -rw-r--r-- | sucl/history.icl | 317 |
2 files changed, 285 insertions, 53 deletions
diff --git a/sucl/history.dcl b/sucl/history.dcl index 2e9f50a..b27567b 100644 --- a/sucl/history.dcl +++ b/sucl/history.dcl @@ -2,18 +2,21 @@ definition module history // $Id$ -from spine import Spine -from rule import Rgraph from graph import Graph +from spine import Spine +from StdOverloaded import == + +// Transitive necessities -from spine import Subspine // for Spine +from spine import Subspine :: History sym var - :== [(var,[Rgraph sym var])] extendhistory - :: (Graph sym var) - (var -> var) - (Spine sym var pvar) - (History sym var) - -> History sym var + :: (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 + & == pvar diff --git a/sucl/history.icl b/sucl/history.icl index b39b6e3..42c8315 100644 --- a/sucl/history.icl +++ b/sucl/history.icl @@ -5,11 +5,37 @@ implementation module history import spine import rule import graph +import pfun import basic +from general import Optional,Yes,No import StdEnv +// A history relates node-ids in the subject graph to patterns :: History sym var - :== [(var,[Rgraph sym var])] + :== [HistoryAssociation sym var] + +// An association between a node-id in the subject graph and a history pattern +:: HistoryAssociation sym var + :== ( (Link 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 + +// 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 +:: Link var + :== Optional (var,Int) + +// A function that associates specific patterns with extensible nodes +// To be used for extending history patterns +:: LinkExtender sym var + :== (Link var) // The extensible link to look for + -> HistoryPattern sym var // The associated pattern /* @@ -27,34 +53,111 @@ import StdEnv */ extendhistory - :: (Graph sym var) - (var -> var) - (Spine sym var pvar) - (History sym var) - -> History sym var + :: (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 + & == pvar -extendhistory sgraph redirection spine history -= snd (foldspine (extendpair sgraph redirection) d d id d (const d) (extendpartial sgraph) (const d) (extendredex sgraph history) d spine) - where d = (emptygraph,history) +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)) -/* +patextend + :: (LinkExtender sym var) + (HistoryPattern sym var) + -> HistoryPattern sym var -> extendpair :: graph * ** -> (**->**) -> ** -> (graph * **,history * **) -> (graph * **,history * **) -> extendpair sgraph redirect snode (hgraph,history) -> = (hgraph',remap (redirect snode) (mkrgraph snode hgraph':foldmap id [] history snode) (forget snode history)) -> where hgraph' = cond sdef (updategraph snode scont hgraph) hgraph -> (sdef,scont) = dnc (const "in extendpair") sgraph snode - -*/ +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) - (var->var) + Int + ( (Link var) + (LinkExtender sym var) + -> ( HistoryAssociation sym var + , HistoryPattern sym var + , LinkExtender sym var + ) + ) var - (Graph sym var,History sym var) - -> (Graph sym var,History sym var) + (Link var) + (LinkExtender sym var) + -> ( HistoryAssociation sym var + , HistoryPattern sym var + , LinkExtender sym var + ) + | == var -extendpair _ _ _ _ = undef +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 +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 _ _ link extender0 + = (newpattern,histpat,extender1) + where histpat = OpenHist + newpattern = (link,histpat) + extender1 = adjust link histpat extender0 /* @@ -65,35 +168,161 @@ extendpair _ _ _ _ = undef */ extendpartial - :: (Graph sym var) - (Rule sym pvar) - (Pfun pvar var) - (Graph sym var,History sym var) - -> (Graph sym var,History sym var) + :: (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 + & == pvar -extendpartial _ _ _ _ = undef +extendpartial sgraph rule matching subnode extendsub snode link restextender + = extendfunction sgraph rule matching ((==)subnode) (const extendsub) snode link restextender -/* +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 :: graph * ** -> history * ** -> rule * *** -> pfun *** ** -> (graph * **,history * **) -> extendredex sgraph history rule matching -> = (extgraph' sgraph rule matching emptygraph,history) +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 -extendredex - :: (Graph sym var) - (History sym var) - (Rule sym pvar) - (Pfun pvar var) - -> (Graph sym var,History sym var) +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 = (link,thispat) -extendredex _ _ _ _ = undef +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 + & == 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..]] -> extgraph' sgraph rule -> = extgraph sgraph rgraph (nodelist rgraph (lhs rule)) -> where rgraph = rulegraph rule +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 -*/ +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 + +instance == (Optional a) | == a + where (==) No No = True + (==) (Yes x1) (Yes x2) = x1==x2 + (==) _ _ = False |