This commit was generated by cvs2svn to compensate for changes in r595,

which included commits to RCS files with non-trunk default branches.

git-svn-id: https://svn.cs.ru.nl/repos/clean-compiler/trunk@596 1f8540f1-abd5-4d5b-9d24-4c5ce8603e2d

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