diff options
| -rw-r--r-- | sucl/Makefile | 2 | ||||
| -rw-r--r-- | sucl/history.dcl | 18 | ||||
| -rw-r--r-- | sucl/history.icl | 283 | ||||
| -rw-r--r-- | sucl/loop.dcl | 1 | ||||
| -rw-r--r-- | sucl/loop.icl | 9 | ||||
| -rw-r--r-- | sucl/spine.dcl | 17 | ||||
| -rw-r--r-- | sucl/spine.icl | 314 | ||||
| -rw-r--r-- | sucl/strat.dcl | 1 | ||||
| -rw-r--r-- | sucl/strat.icl | 45 | ||||
| -rw-r--r-- | sucl/trace.dcl | 2 |
10 files changed, 348 insertions, 344 deletions
diff --git a/sucl/Makefile b/sucl/Makefile index 4237b18..7f462df 100644 --- a/sucl/Makefile +++ b/sucl/Makefile @@ -6,7 +6,7 @@ COCL = cocl #COCLFLAGS = -lat SYS = Clean\ System\ Files -MODULES = basic pretty pfun graph dnc rule trd rewr complete spine history trace absmodule spine strat loop law coreclean convert supercompile +MODULES = basic pretty pfun graph dnc rule trd rewr complete history spine trace absmodule spine strat loop law coreclean convert supercompile ABC = $(patsubst %,$(SYS)/%.abc,$(MODULES)) diff --git a/sucl/history.dcl b/sucl/history.dcl index 0d9ba86..d2f68a4 100644 --- a/sucl/history.dcl +++ b/sucl/history.dcl @@ -2,15 +2,10 @@ definition module history // $Id$ -from spine import Spine from graph import Graph from general import Optional from StdOverloaded import == -// Transitive necessities - -from spine import Subspine - // A history relates node-ids in the subject graph to patterns :: History sym var :== [HistoryAssociation sym var] @@ -23,22 +18,15 @@ from spine import Subspine // 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) -// 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 - & == pvar - // Check the current subject graph in the history matchhistory :: (History sym var) // Complete history against which to check diff --git a/sucl/history.icl b/sucl/history.icl index 2482b5a..4ece980 100644 --- a/sucl/history.icl +++ b/sucl/history.icl @@ -32,279 +32,6 @@ import StdEnv :== Optional (var,Int) -/********************************************* -* Extending the history according to a spine * -*********************************************/ - -// 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 - -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 - & == 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)) - -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 - (Link var) - (LinkExtender sym var) - -> ( HistoryAssociation sym var - , HistoryPattern sym var - , LinkExtender 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 -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 - -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 - & == pvar - -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 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 - & == 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 - -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 - - /************************************************ * Verifying a subject graph against the history * ************************************************/ @@ -334,13 +61,3 @@ checkpat sgraph OpenHist snode = not (fst (varcontents sgraph snode)) checkpat _ (Extensible _) _ = True - - -/**************** -* Miscellaneous * -****************/ - -instance == (Optional a) | == a - where (==) No No = True - (==) (Yes x1) (Yes x2) = x1==x2 - (==) _ _ = False diff --git a/sucl/loop.dcl b/sucl/loop.dcl index f4821fe..2fcbe3f 100644 --- a/sucl/loop.dcl +++ b/sucl/loop.dcl @@ -5,6 +5,7 @@ definition module loop from strat import Strategy from spine import Answer from trace import Trace +from history import HistoryAssociation,HistoryPattern from rule import Rgraph,Rule from graph import Graph from StdOverloaded import == diff --git a/sucl/loop.icl b/sucl/loop.icl index 0ecb18d..c94c1b6 100644 --- a/sucl/loop.icl +++ b/sucl/loop.icl @@ -132,7 +132,8 @@ transform [var] // Arguments of function to generate !(Answer sym var pvar) // Result of strategy -> Action sym var pvar - | == var + | == sym + & == var & == pvar transform anode sargs (Yes spine) @@ -209,7 +210,8 @@ tryunfold (Pfun pvar var) // The matching from rule's pattern to subject (Spine sym var pvar) // The spine returned by the strategy -> Action sym var pvar - | == var + | == sym + & == var & == pvar tryunfold redexroot rule matching spine @@ -220,8 +222,7 @@ 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) - redirect = adjust redexroot reductroot id - history` = extendhistory subject redirect spine history + history` = extendhistory subject spine history trace = continue history` failinfo instdone stricts sroot` subject` heap` tryannotate diff --git a/sucl/spine.dcl b/sucl/spine.dcl index fb7b784..f45a0f5 100644 --- a/sucl/spine.dcl +++ b/sucl/spine.dcl @@ -2,9 +2,12 @@ definition module spine // $Id$ +from history import History,HistoryAssociation,HistoryPattern from rule import Rgraph,Rule +from graph import Graph from pfun import Pfun from general import Optional +from StdOverloaded import == /* @@ -163,7 +166,7 @@ in a graph. | MissingCase // All alternatives failed for a function symbol | Open (Rgraph sym pvar) // Need root normal form of open node for matching | Partial (Rule sym pvar) (Pfun pvar var) pvar (Spine sym var pvar) // A rule was strictly partially matched - | Unsafe (Rgraph sym var) // Terminated due to immininent recursion + | Unsafe (HistoryPattern sym var) // Terminated due to immininent recursion | Redex (Rule sym pvar) (Pfun pvar var) // Total match | Strict // Need root normal form due to strictness @@ -176,7 +179,7 @@ foldspine .subresult // Fold a MissingCase subspine ((Rgraph sym pvar) -> .subresult) // Fold an Open subspine ((Rule sym pvar) (Pfun pvar var) pvar .result -> .subresult) // Fold a Partial subspine - ((Rgraph sym var) -> .subresult) // Fold an Unsafe subspine + ((HistoryPattern sym var) -> .subresult) // Fold an Unsafe subspine ((Rule sym pvar) (Pfun pvar var) -> .subresult) // Fold a Redex subspine .subresult // Fold a Strict subspine .(Spine sym var pvar) // The spine to fold @@ -193,3 +196,13 @@ spinenodes :: .(Spine sym var pvar) -> [var] // Make a decision (continuation based) on whether a spine ends in Open 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 + & == pvar diff --git a/sucl/spine.icl b/sucl/spine.icl index 930ffc7..89da146 100644 --- a/sucl/spine.icl +++ b/sucl/spine.icl @@ -2,9 +2,12 @@ implementation module spine // $Id$ +import history import rule +import graph import pfun import basic +from general import No,Yes import StdEnv /* @@ -164,7 +167,7 @@ in a graph. | MissingCase // All alternatives failed for a function symbol | Open (Rgraph sym pvar) // Need root normal form of open node for matching | Partial (Rule sym pvar) (Pfun pvar var) pvar (Spine sym var pvar) // A rule was strictly partially matched - | Unsafe (Rgraph sym var) // Terminated due to immininent recursion + | Unsafe (HistoryPattern sym var) // Terminated due to immininent recursion | Redex (Rule sym pvar) (Pfun pvar var) // Total match | Strict // Need root normal form due to strictness @@ -200,18 +203,18 @@ in a graph. */ foldspine - :: !(var .subresult -> .result) - .subresult - .subresult - (Int .result -> .subresult) - .subresult - ((Rgraph sym pvar) -> .subresult) - ((Rule sym pvar) (Pfun pvar var) pvar .result -> .subresult) - ((Rgraph sym var) -> .subresult) - ((Rule sym pvar) (Pfun pvar var) -> .subresult) - .subresult - .(Spine sym var pvar) - -> .result + :: !(var .subresult -> .result) // Fold the spine itself + .subresult // Fold a Cycle subspine + .subresult // Fold a Delta subspine + (Int .result -> .subresult) // Fold a Force subspine + .subresult // Fold a MissingCase subspine + ((Rgraph sym pvar) -> .subresult) // Fold an Open subspine + ((Rule sym pvar) (Pfun pvar var) pvar .result -> .subresult) // Fold a Partial subspine + ((HistoryPattern sym var) -> .subresult) // Fold an Unsafe subspine + ((Rule sym pvar) (Pfun pvar var) -> .subresult) // Fold a Redex subspine + .subresult // Fold a Strict subspine + .(Spine sym var pvar) // The spine to fold + -> .result // The final result foldspine pair cycle delta force missingcase open partial unsafe redex strict spine = fold spine @@ -224,7 +227,7 @@ foldspine pair cycle delta force missingcase open partial unsafe redex strict sp foldsub MissingCase = missingcase foldsub (Open rgraph) = open rgraph foldsub (Partial rule matching rnode spine) = partial rule matching rnode (fold spine) - foldsub (Unsafe rgraph) = unsafe rgraph + foldsub (Unsafe histpat) = unsafe histpat foldsub (Redex rule matching) = redex rule matching foldsub Strict = strict @@ -244,3 +247,286 @@ ifopen open other spine = foldoptional other (checkopen o spinetip) spine where checkopen (onode,Open pattern) = open checkopen tip = other + + +/********************************************* +* Extending the history according to a spine * +*********************************************/ + +// 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 + +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 + & == 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)) + +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 + (Link var) + (LinkExtender sym var) + -> ( HistoryAssociation sym var + , HistoryPattern sym var + , LinkExtender 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 +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 + +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 + & == pvar + +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 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 + & == 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 + +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 diff --git a/sucl/strat.dcl b/sucl/strat.dcl index d65972d..01589e0 100644 --- a/sucl/strat.dcl +++ b/sucl/strat.dcl @@ -8,6 +8,7 @@ from rule import Rule from graph import Graph,Node from StdOverloaded import == +from history import HistoryAssociation,HistoryPattern,Link // for History from spine import Spine // for Answer from spine import Subspine // for Spine from rule import Rgraph // for History diff --git a/sucl/strat.icl b/sucl/strat.icl index 8d1d469..0f938b8 100644 --- a/sucl/strat.icl +++ b/sucl/strat.icl @@ -124,11 +124,8 @@ makernfstrategy hist strat rnfnodes node graph = strat` (substrat spinenodes`) graph subspinecont rnfanswer cnt where (def,cnt) = dnc (const "in makernfstrategy") graph node spinenodes` = [node:spinenodes] - subspinecont subspine = spinecont (node,subspine) - - strat` = checkinstance (graph,node) histpatts strat - histpatts = foldr (foldmap (++) id hist) [] spinenodes` + strat` = checkhistory (graph,node) spinenodes hist strat /* @@ -174,14 +171,14 @@ matchrule matchable substrat subject found sargs rule fail pattern = rulegraph rule pairs = zip2 pargs sargs matchable` = matchable pattern - foundsub matching spine = found (Partial rule matching spine) + foundsub matching rnode spine = found (Partial rule matching rnode spine) foundmatch matching = found (Redex rule matching) matchnodes :: (pvar var -> .Bool) .(Graph sym var) (Substrategy sym var pvar result) - ((Pfun pvar var) (Spine sym var pvar) -> result) + ((Pfun pvar var) pvar (Spine sym var pvar) -> result) result .(Graph sym pvar) -> ((Pfun pvar var) -> result) @@ -200,8 +197,8 @@ matchnodes matchable subject substrat found fail pattern | not pdef = match (extend pnode snode matching) | not sdef - = found matching openspine - = substrat (found matching) rnfanswer snode + = found matching pnode openspine + = substrat (found matching pnode) rnfanswer snode where openspine = (snode,Open (mkrgraph pnode pattern)) rnfanswer | psym==ssym && eqlen pargs sargs @@ -331,9 +328,10 @@ forcenodes -> .result forcenodes substrat found rnf nodes -= foldr forcenode rnf nodes - where forcenode nid rnfrest = substrat foundforce rnfrest nid - foundforce spine = found (Force spine) += foldr forcenode rnf (zip2 [0..] nodes) + where forcenode (argno,nid) rnfrest + = substrat foundforce rnfrest nid + where foundforce spine = found (Force argno spine) /* @@ -344,22 +342,21 @@ Check for an instance in the termination history. */ -checkinstance - :: (.Graph sym var,var) - [.Rgraph sym var] - (Strategy sym var .pvar result) - -> Strategy sym var .pvar result +checkhistory + :: (Graph sym var,var) + [var] + (History sym var) + (Strategy sym var pvar result) + -> Strategy sym var pvar result | == sym & == var - & == pvar -checkinstance (graph,node) history defaultstrategy -= foldr check defaultstrategy history - where check hrgraph defaultstrategy substrat subject found rnf (ssym,sargs) - | isinstance (hgraph,hroot) (graph,node) - = found (Unsafe hrgraph) - = defaultstrategy substrat subject found rnf (ssym,sargs) - where hgraph = rgraphgraph hrgraph; hroot = rgraphroot hrgraph +checkhistory (sgraph,snode) spinenodes history defaultstrategy + = if (isEmpty histpats) defaultstrategy unsafestrategy + where histpats + = matchhistory history spinenodes sgraph snode + unsafestrategy _ _ found _ _ + = found (Unsafe (hd histpats)) // Check for curried applications diff --git a/sucl/trace.dcl b/sucl/trace.dcl index 5479b52..f8e884d 100644 --- a/sucl/trace.dcl +++ b/sucl/trace.dcl @@ -2,7 +2,7 @@ definition module trace // $Id$ -from history import History +from history import History,HistoryAssociation,HistoryPattern from spine import Answer from rule import Rule from spine import Spine,Subspine // for Answer |