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

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

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

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