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

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

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

26 files changed, 361 insertions, 221 deletions

diff --git a/sucl/Makefile b/sucl/Makefile
index 1438f25..7e8ecf5 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 history spine trace absmodule strat loop coreclean law canon cli extract newfold newtest convert supercompile
+MODULES = cleanversion basic pfun graph dnc rule trd rewr complete history spine trace absmodule strat loop coreclean law canon cli extract newfold newtest convert supercompile
 
 ABC = $(patsubst %,$(SYS)/%.abc,$(MODULES))
 
@@ -47,5 +47,6 @@ $(SYS)/rule.abc: rule.icl rule.dcl graph.dcl basic.dcl
 $(SYS)/dnc.abc: dnc.icl dnc.dcl graph.dcl
 $(SYS)/graph.abc: graph.icl graph.dcl pfun.dcl basic.dcl
 $(SYS)/pfun.abc: pfun.icl pfun.dcl basic.dcl
-$(SYS)/pretty.abc: pretty.icl pretty.dcl
+#$(SYS)/pretty.abc: pretty.icl pretty.dcl
 $(SYS)/basic.abc: basic.icl basic.dcl
+$(SYS)/cleanversion.abc: cleanversion.icl cleanversion.dcl
diff --git a/sucl/basic.dcl b/sucl/basic.dcl
index f3edbd7..3972d39 100644
--- a/sucl/basic.dcl
+++ b/sucl/basic.dcl
@@ -213,5 +213,8 @@ zipwith :: (.a .b->.c) ![.a] [.b] -> [.c]
 // Sequential evaluation of left and right arguments
 ($) infixr :: !.a .b -> .b
 
+// List subtraction (lazier than removeMembers)
+(--) infixl :: !.[elem] .[elem] -> .[elem] | == elem
+
 // Write a list of things, each one terminated by a newline
 (writeList) infixl :: !*File [a] -> .File | <<< a
diff --git a/sucl/basic.icl b/sucl/basic.icl
index aa90104..aa78e19 100644
--- a/sucl/basic.icl
+++ b/sucl/basic.icl
@@ -299,7 +299,7 @@ stub modulename functionname message
 = abort (modulename+++": "+++functionname+++": "+++message)
 
 superset :: .[a] -> .(.[a] -> Bool) | == a
-superset set = isEmpty o (removeMembers set)
+superset set = isEmpty o ((--) set)
 
 zipwith :: (.a .b->.c) ![.a] [.b] -> [.c]
 zipwith f xs ys = [f x y \\ x<-xs & y<-ys]
@@ -311,6 +311,14 @@ zipwith f xs ys = [f x y \\ x<-xs & y<-ys]
 ($) infixr :: !.a .b -> .b
 ($) x y = y
 
+// List subtraction (lazier than removeMembers)
+(--) infixl :: !.[elem] .[elem] -> .[elem] | == elem
+(--) []     ys = []
+(--) [x:xs] ys = f maybeeqs
+                 where (noteqs,maybeeqs) = span ((<>)x) ys
+                       f []     = [x:xs--noteqs]    // x wasn't in ys
+                       f [y:ys] = xs--(noteqs++ys)  // x==y
+
 (writeList) infixl :: !*File [a] -> .File | <<< a
 (writeList) file [] = file
 (writeList) file [x:xs]
diff --git a/sucl/canon.icl b/sucl/canon.icl
index cf87b70..ea491f1 100644
--- a/sucl/canon.icl
+++ b/sucl/canon.icl
@@ -59,9 +59,9 @@ steps:
 
 */
 
-canonise :: (sym -> Rule tsym tvar) [var2] (Rgraph sym var1) -> Rgraph sym var2 | == var1
-canonise typerule heap rg
- = ((relabel heap o etaexpand typerule o splitrg o relabel localheap) rg <--- "canon.canonise ends") ---> "canon.canonise begins"
+canonise :: (sym -> Int) [var2] (Rgraph sym var1) -> Rgraph sym var2 | == var1
+canonise arity heap rg
+ = ((relabel heap o etaexpand arity o splitrg o relabel localheap) rg <--- "canon.canonise ends") ---> "canon.canonise begins"
 
 /*
 
@@ -75,7 +75,7 @@ canonise typerule heap rg
 splitrg :: (Rgraph sym Int) -> Rgraph sym Int
 splitrg rgraph
  = foldsingleton single rgraph rgraph
-   where single root sym args = mkrgraph root (updategraph root (sym,fst (claim args (removeMembers localheap [root]))) emptygraph)
+   where single root sym args = mkrgraph root (updategraph root (sym,fst (claim args (localheap--[root]))) emptygraph)
 
 /*
 >   uncurry :: (*->rule **** *****) -> rgraph * num -> rgraph * num
@@ -89,12 +89,11 @@ splitrg rgraph
 >             root = rgraphroot rgraph; graph = rgraphgraph rgraph
 */
 
-etaexpand :: (sym->Rule tsym tvar) (Rgraph sym Int) -> Rgraph sym Int
-etaexpand typerule rgraph
+etaexpand :: (sym->Int) (Rgraph sym Int) -> Rgraph sym Int
+etaexpand arity rgraph
  = f (nc root)
    where f (True,(sym,args))
-          = mkrgraph root (updategraph root (sym,fst (claim targs (args++(removeMembers localheap (varlist graph [root]))))) graph)
-            where targs = arguments (typerule sym)
+          = mkrgraph root (updategraph root (sym,take (arity sym) (args++(localheap--(varlist graph [root])))) graph)
          f cont = rgraph
          nc = varcontents graph
          root = rgraphroot rgraph; graph = rgraphgraph rgraph
@@ -115,8 +114,8 @@ localheap =: [0..]
 foldarea :: ((Rgraph sym var) -> sym) (Rgraph sym var) -> Node sym var | == var
 foldarea label rgraph
  = (((labelrgraph<---"canon.foldarea.labelrgraph begins")--->"canon.foldarea.labelrgraph ends",(foldsingleton single nosingle rgraph<---"canon.foldarea.foldsingleton ends")--->"canon.foldarea.foldsingleton begins") <--- "canon.foldarea ends") ---> "canon.foldarea begins"
-   where single root sym args = map (\arg->(arg<---"newfold.foldarea.single.arg begins")--->"newfold.foldarea.single.arg ends") args
-         nosingle = map (\arg->(arg<---"newfold.foldarea.nosingle.arg begins")--->"newfold.foldarea.nosingle.arg ends") (snd (graphvars (rgraphgraph rgraph) [rgraphroot rgraph]))
+   where single root sym args = map (\arg->(arg<---"canon.foldarea.single.arg ends")--->"canon.foldarea.single.arg begins") args
+         nosingle = map (\arg->(arg<---"newfold.foldarea.nosingle.arg ends")--->"newfold.foldarea.nosingle.arg begins") (snd (graphvars (rgraphgraph rgraph) [rgraphroot rgraph]))
          labelrgraph = (label rgraph <--- "canon.foldarea.labelrgraph ends") ---> "canon.foldarea.labelrgraph begins"
 
 /*
@@ -139,18 +138,18 @@ foldarea label rgraph
 >             aroot = rgraphroot area; agraph = rgraphgraph area
 */
 
-labelarea :: [Rgraph sym var] [sym] (Rgraph sym var) -> sym | == sym & == var
-labelarea areas labels rg
- = ((foldmap--->"canon.labelarea uses foldmap") id nolabel ((maketable--->"canon.maketable begins from canon.labelarea") ((areas<---"canon.labelarea.areas ends")--->"canon.labelarea.areas begins") ((labels<---"canon.labelarea.labels ends")--->"canon.labelarea.labels begins")) ((rg<---"canon.labelarea.rg ends")--->"canon.labelarea.rg begins") <--- "canon.labelarea ends") ---> "canon.labelarea begins"
+labelarea :: (sym->Bool) [Rgraph sym var] [sym] (Rgraph sym var) -> sym | == sym & == var
+labelarea reusable areas labels rg
+ = ((foldmap--->"canon.labelarea uses foldmap") id nolabel ((maketable--->"canon.maketable begins from canon.labelarea") reusable ((areas<---"canon.labelarea.areas ends")--->"canon.labelarea.areas begins") ((labels<---"canon.labelarea.labels ends")--->"canon.labelarea.labels begins")) ((rg<---"canon.labelarea.rg ends")--->"canon.labelarea.rg begins") <--- "canon.labelarea ends") ---> "canon.labelarea begins"
    where nolabel = abort "canon: labelarea: no label assigned to area"
 
-maketable :: [Rgraph sym var] [sym] -> [(Rgraph sym var,sym)] | == var
-maketable [] _ = [] <--- "canon.maketable ends empty"
-maketable [area:areas] labels
- = [(((area<---"canon.maketable.area ends")--->"canon.maketable.area begins",(label<---"canon.maketable.label ends")--->"canon.maketable.label begins") <--- "canon.maketable.head ends") ---> "canon.maketable.head begins":(maketable--->"canon.maketable begins from maketable") areas labels`] <--- "canon.maketable ends nonempty"
+maketable :: (sym->Bool) [Rgraph sym var] [sym] -> [(Rgraph sym var,sym)] | == var
+maketable _ [] _ = [] <--- "canon.maketable ends empty"
+maketable reusable [area:areas] labels
+ = [(((area<---"canon.maketable.area ends")--->"canon.maketable.area begins",(label<---"canon.maketable.label ends")--->"canon.maketable.label begins") <--- "canon.maketable.head ends") ---> "canon.maketable.head begins":(maketable--->"canon.maketable begins from maketable") reusable areas labels`] <--- "canon.maketable ends nonempty"
    where (label,labels`) = getlabel (nc aroot) labels
          getlabel (True,(asym,aargs)) labels
-          | not (or (map (fst o nc) aargs))
+          | reusable asym && not (or (map (fst o nc) aargs))
             = (asym,labels)
          getlabel acont [label:labels]
           = (label,labels)
diff --git a/sucl/cli.icl b/sucl/cli.icl
index faa1a4b..90f731f 100644
--- a/sucl/cli.icl
+++ b/sucl/cli.icl
@@ -9,6 +9,7 @@ import absmodule
 import rule
 import dnc
 import basic
+import general
 import StdEnv
 
 /*
@@ -123,6 +124,11 @@ Abstype implementation.
 exports :: Cli -> [SuclSymbol]
 exports (CliAlias m) = m.exportedsymbols
 
+// Determine the arity of a core clean symbol
+arity :: Cli SuclSymbol -> Int
+arity (CliAlias m) sym
+= extendfn m.arities (length o arguments o (extendfn m.typerules coretyperule)) sym
+
 /*
 >   typerule (tdefs,(es,as,ts,rs)) = maxtyperule ts
 */
@@ -160,8 +166,9 @@ clistrategy (CliAlias {arities=as,typeconstructors=tcs,typerules=ts,rules=rs}) m
    o checkimport islocal                            // Checks for delta symbols
    o checkconstr (flip isMember (flatten (map snd tcs))) // Checks for constructors
    ) (corestrategy matchable)                       // Checks rules for symbols in the language core (IF, _AP, ...)
-   where islocal rsym=:(SuclUser s) = isMember rsym (map fst rs)
-         islocal rsym = True                        // Symbols in the language core are always completely known
+   where islocal rsym=:(SuclUser s) = isMember rsym (map fst rs)// User-defined symbols can be imported, so they're known if we have a list of rules for them
+         islocal rsym               = True                      // Symbols in the language core (the rest) are always completely known
+                                                                // This includes lifted case symbols; we lifted them ourselves, after all
 
 typearity :: (Rule SuclTypeSymbol SuclTypeVariable) -> Int
 typearity ti = length (arguments ti)
@@ -321,17 +328,17 @@ mkcli ::
     [(SuclSymbol,Rule SuclTypeSymbol SuclTypeVariable)]
     [(SuclSymbol,[Bool])]
     [SuclSymbol]
-    [(SuclTypeSymbol,[SuclSymbol])]
+    [(SuclTypeSymbol,[(SuclSymbol,(Rule SuclTypeSymbol SuclTypeVariable,[Bool]))])]
     [(SuclSymbol,(Int,[Rule SuclSymbol SuclVariable]))]
  -> Cli
 
 mkcli typerules stricts exports constrs bodies
 = CliAlias
   { arities          = map (mapsnd fst) bodies
-  , typeconstructors = constrs
+  , typeconstructors = map (mapsnd (map fst)) constrs
   , exportedsymbols  = exports
-  , typerules        = typerules
-  , stricts          = stricts
+  , typerules        = typerules++flatten ((map (map (mapsnd fst) o snd)) constrs)
+  , stricts          = stricts++flatten ((map (map (mapsnd snd) o snd)) constrs)
   , rules            = map (mapsnd snd) bodies
   }
 
diff --git a/sucl/dnc.dcl b/sucl/dnc.dcl
index 081dc97..2b262b6 100644
--- a/sucl/dnc.dcl
+++ b/sucl/dnc.dcl
@@ -3,7 +3,7 @@ definition module dnc
 // $Id$
 
 from graph import Graph,Node
-from StdString import String
+from cleanversion import String
 from StdOverloaded import ==
 
 // dnc is like varcontents, but can give a more reasonable error message
diff --git a/sucl/extract.icl b/sucl/extract.icl
index b2d0e46..57cef81 100644
--- a/sucl/extract.icl
+++ b/sucl/extract.icl
@@ -80,7 +80,7 @@ actualfold deltanodes rnfnodes foldarea self foldcont hist rule
 = Yes (mkrule rargs rroot rgraph``,areas`)
   where rargs = arguments rule; rroot = ruleroot rule; rgraph = rulegraph rule
 
-        list2 = map (pairwith (findoccs hist rule)) (removeMembers (varlist rgraph [rroot]) (varlist rgraph rargs))
+        list2 = map (pairwith (findoccs hist rule)) (varlist rgraph [rroot]--varlist rgraph rargs)
         // list2: list combining every node with list of every instantiable history graph
 
         list3 = [(rnode,mapping) \\ (rnode,[mapping:_])<-list2]
@@ -120,7 +120,7 @@ findoccs hist rule rnode
         unshared rnode (hroot,hgraph) mapping
         = disjoint inner outer
           where inner = map (lookup mapping) (fst (graphvars hgraph [hroot]))
-                outer = removeMembers (varlist (prunegraph rnode rgraph) [rroot:rargs]) [rnode]
+                outer = varlist (prunegraph rnode rgraph) [rroot:rargs]--[rnode]
 
 /*
 ------------------------------------------------------------------------
@@ -148,8 +148,8 @@ splitrule fold rnfnodes deltanodes rule area
         rgraph` = updategraph aroot (fold area`) rgraph
         area` = mkrgraph aroot agraph`
         agraph` = foldr addnode emptygraph ins
-        ins = removeMembers (varlist agraph [aroot]) outs
-        outs = removeMembers (varlist (prunegraph aroot rgraph) [rroot:rargs++snd (graphvars agraph [aroot])]) [aroot]
+        ins = varlist agraph [aroot]--outs
+        outs = varlist (prunegraph aroot rgraph) [rroot:rargs++snd (graphvars agraph [aroot])]--[aroot]
 
         addnode node = updategraph node (snd (dnc (const "in splitrule") rgraph node))
 
@@ -180,11 +180,11 @@ finishfold foldarea fixednodes singlenodes root graph
         process aroot
         = mkrgraph aroot (foldr addnode emptygraph ins)
           where outs_and_aroot = varlist (prunegraph aroot graph) arearoots++fixednodes
-                ins = [aroot:removeMembers (varlist graph [aroot]) outs_and_aroot]
+                ins = [aroot:varlist graph [aroot]--outs_and_aroot]
         generate area
-        = removeMembers (snd (graphvars agraph [aroot])) fixednodes
+        = snd (graphvars agraph [aroot])--fixednodes
           where aroot = rgraphroot area; agraph = rgraphgraph area
-        arearoots = removeMembers (removeDup [root:singlenodes++singfixargs]) fixednodes
+        arearoots = removeDup [root:singlenodes++singfixargs]--fixednodes
         singfixargs = flatten (map arguments (singlenodes++fixednodes))
 
         arguments node
diff --git a/sucl/graph.dcl b/sucl/graph.dcl
index eaeb1d0..0a64c0c 100644
--- a/sucl/graph.dcl
+++ b/sucl/graph.dcl
@@ -4,7 +4,8 @@ definition module graph
 
 from pfun import Pfun
 from StdOverloaded import ==
-from StdString import String,toString
+from cleanversion import String
+from StdString import toString
 
 // A rule associating a replacement with a pattern
 //:: Rule sym var
@@ -98,7 +99,7 @@ Implementation
 */
 
 // The empty graph.
-emptygraph :: Graph .sym .var
+emptygraph :: .Graph sym var
 
 // Assign a node to a variable in a graph.
 updategraph :: var .(Node sym var) !.(Graph sym var) -> .Graph sym var
diff --git a/sucl/graph.icl b/sucl/graph.icl
index 2021826..313db51 100644
--- a/sucl/graph.icl
+++ b/sucl/graph.icl
@@ -60,7 +60,7 @@ functions to manipulate them.
 */
 
 // The empty set of bindings
-emptygraph :: Graph .sym .var
+emptygraph :: .Graph sym var
 emptygraph = GraphAlias emptypfun
 
 updategraph :: var .(Node sym var) !.(Graph sym var) -> .Graph sym var
@@ -97,18 +97,18 @@ varcontents (GraphAlias pfun) v
 
 graphvars :: .(Graph sym var) !.[var] -> (.[var],.[var]) | == var
 graphvars graph roots
-= (graphvars` [] graph roots<---"graph.graphvars ends")--->"graph.graphvars begins"
+= graphvars` [] graph roots
 
 // Finds bound and free variables in a graph
 // Excludes the variables only reachable through "prune"
 graphvars` :: .[var] .(Graph sym var) .[var] -> (.[var],.[var]) | == var
 graphvars` prune graph roots
-= (snd (foldlr (ns--->"graph.graphvars`.ns begins from graph.graphvars`") (prune,([],[])) roots)<---"graph.graphvars` ends")--->"graph.graphvars` begins"
+= snd (foldlr ns (prune,([],[])) roots)
   where ns var seenboundfree
-        | isMember var seen = seenboundfree<---"graph.graphvars`.ns ends (already seen)"
-        | not def           = ([var:seen],(bound,[var:free]))<---"graph.graphvars`.ns ends (open variable)"
-                            = (seen`,([var:bound`],free`))<---"graph.graphvars`.ns ends (closed variable)"
-          where (seen`,(bound`,free`)) = foldlr (ns--->"graph.graphvars`.ns begins from graph.graphvars`.ns") ([var:seen],boundfree) args
+        | isMember var seen = seenboundfree
+        | not def           = ([var:seen],(bound,[var:free]))
+                            = (seen`,([var:bound`],free`))
+          where (seen`,(bound`,free`)) = foldlr ns ([var:seen],boundfree) args
                 (def,(_,args)) = varcontents graph var
                 (seen,boundfree=:(bound,free)) = seenboundfree
 varlist :: .(Graph sym var) !.[var] -> .[var] | == var
@@ -235,7 +235,7 @@ isinstance
  &  == pvar
 
 isinstance (pgraph,pvar) (sgraph,svar)
-= isEmpty (thd3 (findmatching (pgraph,sgraph) (pvar,svar) ([],[],[])))
+= isEmpty (thd3 (findmatching (pgraph,sgraph) (pvar,svar) ([],[],[]))) <--- "graph.isinstance ends"
 
 /*
 
@@ -413,12 +413,12 @@ extgraph sgraph pattern pnodes matching graph
 
 mapgraph ::
     !(  (Pfun var1 (sym1,[var1]))
-     -> Pfun .var2 (.sym2,[.var2])
+     -> Pfun var2 (sym2,[var2])
      )
     !.(Graph sym1 var1)
- -> Graph .sym2 .var2
+ -> .Graph sym2 var2
 mapgraph f (GraphAlias pfun) = GraphAlias (f pfun)
 
 instance == (Graph sym var) | == sym & == var
 where (==) (GraphAlias pf1) (GraphAlias pf2)
-      = ((pf1 == pf2) <--- "graph.==(Graph) ends") ---> "graph.==(Graph) begins"
+      = pf1 == pf2
diff --git a/sucl/history.dcl b/sucl/history.dcl
index 1c4913d..af056b6 100644
--- a/sucl/history.dcl
+++ b/sucl/history.dcl
@@ -7,6 +7,8 @@ from graph import Graph
 from general import Optional
 from StdOverloaded import ==
 from StdString import toString
+from StdClass import Eq
+from cleanversion import String
 
 // A history relates node-ids in the subject graph to patterns
 :: History sym var
@@ -34,8 +36,16 @@ matchhistory
     (Graph sym var)             // Current subject graph
     var                         // Current application point of strategy
  -> [HistoryPattern sym var]    // Matching history patterns
- |  == sym
- &  == var
+ |  Eq sym
+ &  Eq var
+
+// Convert a history to its string representation
+historyToString ::
+    (History sym var)
+ -> String
+ |  toString sym
+ &  toString var
+ &  Eq var
 
 (writeHistory) infixl :: *File (History sym var) -> .File | toString sym & toString,== var
 (writeHistoryAssociation) infixl :: *File (HistoryAssociation sym var) -> .File | toString sym & toString,== var
diff --git a/sucl/history.icl b/sucl/history.icl
index 31d8907..f3b6c55 100644
--- a/sucl/history.icl
+++ b/sucl/history.icl
@@ -6,7 +6,7 @@ import rule
 import graph
 import pfun
 import basic
-from general import Optional,Yes,No
+from general import Optional,Yes,No,--->
 import StdEnv
 
 // A history relates node-ids in the subject graph to patterns
@@ -39,17 +39,17 @@ matchhistory
     (Graph sym var)             // Current subject graph
     var                         // Current application point of strategy
  -> [HistoryPattern sym var]    // Matching history patterns
- |  == sym
- &  == var
+ |  Eq sym
+ &  Eq var
 
 matchhistory hist spinenodes sgraph snode
- = foldr (checkassoc spinenodes sgraph snode) [] hist
+= foldr ((checkassoc--->"history.checkassoc begins from history.matchhistory") spinenodes sgraph snode) [] hist <--- "history.matchhistory ends"
 
 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
+= ((if (isMember var spinenodes) (foldr (checkpat--->"history.checkassoc.checkpat begins from history.checkassoc") rest pats) (rest--->"history.checkassoc history attachment node is not part of the spine nodes")) <--- "history.checkassoc ends") ---> ("history.checkassoc number of history patterns for node is "+++toString (length pats))
+  where checkpat pat rest
+        = (if ((isinstance--->"graph.isinstance begins from history.checkassoc.checkpat") (hgraph,hroot) (sgraph,snode)) [pat:rest] rest) <--- "history.checkassoc.checkpat ends"
+          where hgraph = rgraphgraph pat; hroot = rgraphroot pat
 
 /*
 instantiate ::
@@ -60,8 +60,18 @@ instantiate ::
  -> ([(pvar,var)],[(pvar,var)],[(pvar,var)])
 */
 
+historyToString ::
+    (History sym var)
+ -> String
+ |  toString sym
+ &  toString var
+ &  Eq var
+
+historyToString history
+= showlist (showpair toString (showlist toString)) history
+
 (writeHistory) infixl :: *File (History sym var) -> .File | toString sym & toString,== var
-(writeHistory) file history = sfoldl (writeHistoryAssociation) file history
+(writeHistory) file history = file <<< "<history>" // sfoldl (writeHistoryAssociation) file history
 
 (writeHistoryAssociation) infixl :: *File (HistoryAssociation sym var) -> .File | toString sym & toString,== var
-(writeHistoryAssociation) file ha = file <<< showpair toString (showlist toString) ha <<< nl
+(writeHistoryAssociation) file ha = file <<< "<historyassociation>" // showpair toString (showlist toString) ha <<< nl
diff --git a/sucl/loop.icl b/sucl/loop.icl
index 50b6021..e589150 100644
--- a/sucl/loop.icl
+++ b/sucl/loop.icl
@@ -11,9 +11,12 @@ import rule
 import graph
 import pfun
 import basic
-from general import Yes,No
+from general import Yes,No,--->
 import StdEnv
 
+mstub = stub "loop"
+block func = mstub func "blocked for debugging"
+
 /*
 
 loop.lit - Looping to produce a trace
@@ -228,19 +231,22 @@ loop
  &  toString var    // Debugging
  &  <<< var         // Debugging
 
+// loop _ _ _ = block "loop"
 loop strategy matchable (initheap,rule)
 = result
   where result = maketrace inithistory initfailinfo initinstdone initstricts initsroot initsubject initheap
         maketrace history failinfo instdone stricts sroot subject heap
-        = Trace stricts (mkrule sargs sroot subject) answer history transf
+        = (Trace stricts currentrule answer history transf ---> ("loop.loop.maketrace rule "+++ruleToString toString currentrule)) ---> ("loop.loop.maketrace history "+++historyToString history)
           where answer = makernfstrategy history (strategy matchable`) rnfnodes sroot subject
-                transf = transform sroot sargs answer maketrace history failinfo instdone stricts sroot subject heap
+                transf = (transform--->"loop.transform begins from loop.loop") sroot sargs answer maketrace history failinfo instdone stricts sroot subject heap
 
                 rnfnodes = removeDup (listselect stricts sargs++fst (graphvars subject sargs))
 
                 matchable` pgraph pnode snode
                 = matchable (failinfo snode) (mkrgraph pnode pgraph)
 
+                currentrule = mkrule sargs sroot subject
+
         inithistory = []
         initfailinfo = const []
         initinstdone = False
@@ -277,14 +283,20 @@ transform
  &  == pvar
 
 transform anode sargs (Yes spine)
-= selectfromtip (spinetip spine)
-  where selectfromtip (nid,Open rgraph) = tryinstantiate nid rgraph anode sargs
-        selectfromtip (nid,Redex rule matching) = tryunfold nid rule matching spine
-        selectfromtip (nid,Strict) = tryannotate nid sargs
-        selectfromtip spine = dostop
+= (selectfromtip--->"loop.transform.selectfromtip begins from loop.transform") (spinetip spine) <--- "loop.transform ends for some spine"
+  where selectfromtip (nid,Open rgraph) = (tryinstantiate--->"loop.tryinstantiate begins from loop.transform.selectfromtip") nid rgraph anode sargs <--- "loop.transform.selectfromtip ends for Open spine"
+        selectfromtip (nid,Redex rule matching) = (tryunfold--->"loop.tryunfold begins from loop.transform.selectfromtip") nid rule matching spine <--- "loop.transform.selectfromtip ends for Redex spine"
+        selectfromtip (nid,Strict) = (tryannotate--->"loop.tryannotate begins from loop.transform.selectfromtip") nid sargs <--- "loop.transform.selectfromtip ends for Strict spine"
+        selectfromtip (nid,Cycle) = (dostop--->"loop.dostop begins from loop.transform.selectfromtip") <--- "loop.transform.selectfromtip ends for Cycle spine"
+        selectfromtip (nid,Delta) = (dostop--->"loop.dostop begins from loop.transform.selectfromtip") <--- "loop.transform.selectfromtip ends for Delta spine"
+        selectfromtip (nid,Force _ _) = (dostop--->"loop.dostop begins from loop.transform.selectfromtip") <--- "loop.transform.selectfromtip ends for Force spine"
+        selectfromtip (nid,MissingCase) = (dostop--->"loop.dostop begins from loop.transform.selectfromtip") <--- "loop.transform.selectfromtip ends for MissingCase spine"
+        selectfromtip (nid,Partial _ _ _ _) = (dostop--->"loop.dostop begins from loop.transform.selectfromtip") <--- "loop.transform.selectfromtip ends for Partial spine"
+        selectfromtip (nid,Unsafe _) = (dostop--->"loop.dostop begins from loop.transform.selectfromtip") <--- "loop.transform.selectfromtip ends for Unsafe spine"
+        //selectfromtip spine = (dostop--->"loop.dostop begins from loop.transform.selectfromtip") <--- "loop.transform.selectfromtip ends for other spine"
 
 transform anode sargs No
-= dostop
+= (dostop--->"loop.dostop begins from loop.transform") <--- "loop.transform ends for no spine"
 
 // ==== ATTEMPT TO INSTANTIATE A FREE VARIABLE WITH A PATTERN ====
 
@@ -298,7 +310,7 @@ tryinstantiate
  &  == pvar
 
 tryinstantiate onode rpattern anode sargs
-= act
+= act <--- "loop.tryinstantiate ends"
   where act continue history failinfo instdone stricts sroot subject heap
         | anode==sroot                                   // Check if strategy applied at root
           && goodorder strictargs sargs subject subject` // Check if order of arguments of rule ok
@@ -325,8 +337,8 @@ goodorder
 
 goodorder stricts sargs subject subject`
 = startswith match match`
-  where match = removeMembers (fst (graphvars subject sargs)) stricts
-        match` = removeMembers (fst (graphvars subject` sargs)) stricts
+  where match = fst (graphvars subject sargs)--stricts
+        match` = fst (graphvars subject` sargs)--stricts
 
 // See if second argument list has the first one as its initial part
 startswith
@@ -355,7 +367,7 @@ tryunfold ::
  &  == pvar
 
 tryunfold redexroot rule matching spine
-= act
+= act <--- "loop.tryunfold ends"
   where act continue history failinfo instdone stricts sroot subject heap
         = Reduce reductroot trace
           where (heap`,sroot`,subject`,matching`)
@@ -373,7 +385,7 @@ tryannotate
  |  == var
 
 tryannotate strictnode sargs
-= act
+= act <--- "loop.tryannotate ends"
   where act continue history failinfo instdone stricts sroot subject heap
         | not instdone && isMember strictnode sargs
         = Annotate trace
@@ -388,5 +400,5 @@ dostop
  :: Action sym var pvar
 
 dostop
-= ds
+= ds <--- "loop.dostop ends"
   where ds continue history failinfo instdone stricts sroot subject heap = Stop
diff --git a/sucl/newfold.icl b/sucl/newfold.icl
index a9b9f48..1e60c13 100644
--- a/sucl/newfold.icl
+++ b/sucl/newfold.icl
@@ -110,9 +110,11 @@ fullfold ::
  |  == sym
  &  == var
  &  == pvar
+ &  toString sym
  &  toString var
+ &  toString pvar
  &  <<< var
- &  toString sym
+ &  <<< pvar
 
 fullfold trc foldarea fnsymbol trace
 | recursive ---> "newfold.fullfold begins"
@@ -140,9 +142,11 @@ recurse ::
  |  == sym
  &  == var
  &  == pvar
+ &  toString sym
  &  toString var
+ &  toString pvar
  &  <<< var
- &  toString sym
+ &  <<< pvar
 
 recurse foldarea fnsymbol
 = ((f--->"newfold.recurse.f begins from newfold.recurse") ([],[]) <--- "newfold.recurse ends") ---> "newfold.recurse begins"
@@ -195,22 +199,22 @@ foldtips foldarea foldcont
   where ft hist trace
         = case transf
           of Stop
-              -> foldoptional exres (pair True o addstrict stricts o mapfst rule2body) (actualfold deltanodes rnfnodes foldarea (==) foldcont (snd hist) rule) <--- "newfold.foldtips.ft ends (Stop)"
+              -> (foldoptional exres (pair True o addstrict stricts o mapfst rule2body) (actualfold deltanodes rnfnodes foldarea (==) foldcont (snd hist) rule) <--- "newfold.foldtips.ft ends (Stop)") ---> "newfold.foldtips.ft case = Stop"
                  where deltanodes = foldoptional [] getdeltanodes answer
                        rnfnodes = foldoptional [ruleroot rule] (const []) answer
              Instantiate yestrace notrace
               -> ft` ((ft--->"newfold.foldtips.ft begins from newfold.foldtips.ft.Instantiate.match") hist yestrace) ((ft--->"newfold.foldtips.ft begins from newfold.foldtips.ft.Instantiate.fail") hist notrace)
-                 where ft` (False,yessra) (False,nosra) = exres <--- "newfold.foldtips.ft ends (Instantiate/no)"
+                 where ft` (False,yessra) (False,nosra) = (exres <--- "newfold.foldtips.ft ends (Instantiate/no)") ---> "newfold.foldtips.ft case Instantiate/no"
                        ft` (yesfound,(yesstricts,yesbody,yesareas)) (nofound,(nostricts,nobody,noareas))
-                       = (True,(stricts,matchpattern answer yesbody nobody,yesareas++noareas)) <--- "newfold.foldtips.ft ends (Instantiate/yes)"
+                       = ((True,(stricts,matchpattern answer yesbody nobody,yesareas++noareas)) <--- "newfold.foldtips.ft ends (Instantiate/yes)") ---> "newfold.foldtips.ft case Instantiate/yes"
              Reduce reductroot trace
               -> ft` ((ft--->"newfold.foldtips.ft begins from newfold.foldtips.ft.Reduce") (fst hist,fst hist) trace)
-                 where ft` (False,sra) = exres <--- "newfold.foldtips.ft ends (Reduce/no)"
-                       ft` (found,sra) = (True,sra) <--- "newfold.foldtips.ft ends (Reduce/yes)"
+                 where ft` (False,sra) = (exres <--- "newfold.foldtips.ft ends (Reduce/no)") ---> "newfold.foldtips.ft case Reduce/no"
+                       ft` (found,sra) = ((True,sra) <--- "newfold.foldtips.ft ends (Reduce/yes)") ---> "newfold.foldtips.ft case Reduce/no"
              Annotate trace
               -> ft` ((ft--->"newfold.foldtips.ft begins from newfold.foldtips.ft.Annotate") hist trace)
-                 where ft` (False,sra) = exres <--- "newfold.foldtips.ft ends (Annotate/no)"
-                       ft` (found,sra) = (True,sra) <--- "newfold.foldtips.ft ends (Annotate/yes)"
+                 where ft` (False,sra) = (exres <--- "newfold.foldtips.ft ends (Annotate/no)") ---> "newfold.foldtips.ft case Annotate/no"
+                       ft` (found,sra) = ((True,sra) <--- "newfold.foldtips.ft ends (Annotate/yes)") ---> "newfold.foldtips.ft case Annotate/no"
           where (Trace stricts rule answer _ transf) = trace
                 exres = (False,newextract noetrc foldarea trace)
 
@@ -301,7 +305,7 @@ buildgraph ::
  -> FuncBody sym var | == var
 buildgraph args root graph
 = (BuildGraph (mkrgraph root (compilegraph (map (pairwith (snd o varcontents graph)) newnodes))) <--- "newfold.buildgraph ends") ---> "newfold.buildgraph begins"
-  where newnodes = removeMembers closedreplnodes patnodes
+  where newnodes = closedreplnodes--patnodes
         closedreplnodes = fst (graphvars graph [root])
         patnodes = varlist graph args
 
@@ -363,7 +367,7 @@ findpattern pattern thespinenodes residuroot transf
 findpattern pattern thespinenodes residuroot (Reduce reductroot trace)
 = fp (redirect residuroot) trace
   where fp residuroot (Trace stricts rule answer history transf)
-         | or [isinstance pattern (graph,node) \\ node<-varlist graph [residuroot]]
+         | or [(isinstance--->"graph.isinstance begins from newfold.findpattern.fp") pattern (graph,node) \\ node<-varlist graph [residuroot]]
            = True
              where graph = rulegraph rule
         fp residuroot trace = findpattern` pattern residuroot trace
diff --git a/sucl/newtest.icl b/sucl/newtest.icl
index 13fe716..6a0cdc9 100644
--- a/sucl/newtest.icl
+++ b/sucl/newtest.icl
@@ -158,7 +158,7 @@ these tuples.
      , srr_areas           :: [Rgraph sym var]  // New areas for further symbolic reduction (not necessarily canonical)
      }
 
-instance toString Symredresult sym var tsym tvar | toString sym & toString var & == var
+instance toString (Symredresult sym var tsym tvar) | toString sym & toString var & Eq var
 where toString srr
       = "Task: "+++toString srr.srr_task_expression+++
         "\nSymbol: "+++toString srr.srr_assigned_symbol+++
@@ -168,7 +168,7 @@ where toString srr
         "\nFunction definition: "+++"<funcdef>"+++
         "\nAreas: "+++listToString srr.srr_areas+++"\n"
 
-instance <<< Symredresult sym var tsym tvar | toString sym & <<<,==,toString var
+instance <<< (Symredresult sym var tsym tvar) | toString sym & <<<,==,toString var
 where (<<<) file srr
       = file <<< "==[BEGIN]==" <<< nl
              <<< "Task expression: " <<< ((srr.srr_task_expression <--- "newtest.<<<(Symredresult).srr_task_expression ends") ---> "newtest.<<<(Symredresult).srr_task_expression begins") <<< nl
@@ -309,8 +309,11 @@ fullsymred freshsymbols cli
          process area = (symredarea foldarea` cli area <--- "newtest.fullsymred.process ends") ---> "newtest.fullsymred.process begins"
 
          foldarea` = ((foldarea (labelarea` o canonise`)) <--- "newtest.fullsymred.foldarea` ends") ---> "newtest.fullsymred.foldarea` begins"
-         labelarea` = (labelarea (map getinit results) freshsymbols <--- "newtest.fullsymred.labelarea` ends") ---> "newtest.fullsymred.labelarea` begins"
-         canonise` = (canonise (typerule cli) suclheap <--- "newtest.fullsymred.canonise` ends") ---> "newtest.fullsymred.canonise` begins"
+         labelarea` = (labelarea isSuclUserSym (map getinit results) freshsymbols <--- "newtest.fullsymred.labelarea` ends") ---> "newtest.fullsymred.labelarea` begins"
+         canonise` = (canonise (arity cli) suclheap <--- "newtest.fullsymred.canonise` ends") ---> "newtest.fullsymred.canonise` begins"
+
+isSuclUserSym (SuclUser _) = True
+isSuclUserSym _ = False
 
 /*
 `Initareas cli' is the list  of  initial  rooted  graphs  that  must  be
@@ -394,7 +397,7 @@ symredarea foldarea cli area
         (symbol,aargs) = foldarea area
         arule = mkrule aargs aroot agraph
         trule = (ruletype sucltypeheap (ctyperule SuclFN sucltypeheap (typerule cli)) arule <--- "newtest.symredarea.trule.ruletype ends") ---> "newtest.symredarea.trule.ruletype begins"
-        trace = (loop strategy` matchable` (removeMembers suclheap (varlist agraph [aroot]),arule) <--- "newtest.symredarea.trace.loop ends") ---> "newtest.symredarea.trace.loop begins"
+        trace = (loop strategy` matchable` (suclheap--varlist agraph [aroot],arule) <--- "newtest.symredarea.trace.loop ends") ---> "newtest.symredarea.trace.loop begins"
         (stricts,rules,areas) = (fullfold (trc symbol) foldarea symbol trace <--- "newtest.symredarea.(,,).fullfold ends") ---> "newtest.symredarea.(,,).fullfold begins"
         matchable` = matchable (complete cli)
         strategy` = clistrategy cli
@@ -544,7 +547,7 @@ ctyperule fn typeheap typerule (sym,args)
   where targs = arguments trule; troot = ruleroot trule; tgraph = rulegraph trule
         trule = typerule sym
         (targs`,targs``) = claim args targs
-        (troot`,tgraph`,_) = foldr build (troot,tgraph,removeMembers typeheap (varlist tgraph [troot:targs])) targs``
+        (troot`,tgraph`,_) = foldr build (troot,tgraph,typeheap--varlist tgraph [troot:targs]) targs``
         build targ (troot,tgraph,[tnode:tnodes])
         = (tnode,updategraph tnode (fn 1,[targ,troot]) tgraph,tnodes)
 
diff --git a/sucl/pfun.dcl b/sucl/pfun.dcl
index 022188a..920c28c 100644
--- a/sucl/pfun.dcl
+++ b/sucl/pfun.dcl
@@ -39,7 +39,8 @@ domres :: !.[dom] .(Pfun dom ran) -> Pfun dom ran | == dom
 apply :: !(Pfun dom .ran) dom -> (.Bool,.ran) | == dom
 
 // Partial functions are printable
-instance toString Pfun dom ran | toString dom & toString ran
+instance toString (Pfun dom ran) | toString dom & toString ran & == dom
+(writepfun) infixl :: *File .(Pfun dom ran) -> .File | ==,toString dom & toString ran
 
 /* `Idpfun dom pfun' checks whether partial function `pfun' is the identity
    on the nodes in `dom' for which it is defined.
diff --git a/sucl/pfun.icl b/sucl/pfun.icl
index 111ecdf..d263852 100644
--- a/sucl/pfun.icl
+++ b/sucl/pfun.icl
@@ -70,13 +70,15 @@ apply pfun arg
   where s x = (True,x)
         baddomain = abort "apply: partial function applied outside domain"
 
-instance toString Pfun dom ran | toString dom & toString ran
+instance toString Pfun dom ran | toString dom & toString ran & == dom
 where toString pfun
       = toString ['{':drop 1 (flatten (map ((cons ',') o printlink) (pfunlist pfun)))++['}']]
         where printlink (arg,res) = fromString (toString arg)++['|->']++fromString (toString res)
 
-pfunlist :: (Pfun dom res) -> [(dom,res)]
-pfunlist _ = error "pfunlist not implemented"
+pfunlist :: (Pfun dom res) -> [(dom,res)] | == dom
+pfunlist EmptyPfun = []
+pfunlist (Extend x y pf) = [(x,y):pfunlist (Restrict x pf)]
+pfunlist (Restrict x pf) = [xxyy \\ xxyy=:(xx,yy) <- pfunlist pf | xx<>x]
 
 idpfun :: !.[dom] .(Pfun dom dom) -> Bool | == dom
 idpfun domain pfun
@@ -90,3 +92,6 @@ where (==) EmptyPfun EmptyPfun = True
       (==) (Restrict x1 pf1) (Restrict x2 pf2)
             = x1==x2 && pf1==pf2
       (==) _ _ = False
+
+(writepfun) infixl :: *File .(Pfun dom ran) -> .File | ==,toString dom & toString ran
+(writepfun) file pfun = file <<< toString pfun
diff --git a/sucl/rule.dcl b/sucl/rule.dcl
index a865837..f31a7e0 100644
--- a/sucl/rule.dcl
+++ b/sucl/rule.dcl
@@ -5,6 +5,8 @@ definition module rule
 from graph import Graph,Node
 from StdOverloaded import ==,toString
 from StdFile import <<<
+from cleanversion import String
+from StdClass import Eq
 
 // --- Exported types
 
@@ -14,23 +16,24 @@ from StdFile import <<<
 // --- Functions on rules
 
 // Build a rule from its constituents
-mkrule :: [.var] .var (Graph .sym .var) -> Rule .sym .var
+mkrule    :: .[var] var (Graph sym var) -> .Rule sym var
 
 // The arguments of a rule, i.e. the roots of its lhs
 arguments :: !.(Rule sym var) -> [var]
 
 // The root of a rule, i.e. of its rhs
-ruleroot :: !.(Rule sym var) -> var
+ruleroot  :: !.(Rule sym var) -> var
 
 // The graph part of a rule, i.e. its bindings
 rulegraph :: !.(Rule sym var) -> Graph sym var
 
-instance toString Rule sym var | toString sym & toString var & == var
+instance toString (Rule sym var) | toString sym & toString var & == var
+ruleToString :: (sym->.String) .(Rule sym var) -> String | Eq,toString var
 
 // --- Functions on rooted graphs
 
 // The empty rooted graph with a given root
-emptyrgraph  :: .var -> Rgraph .sym .var
+emptyrgraph  :: var -> .Rgraph sym var
 
 // Update the contents of a variable in a rooted graph
 updatergraph :: var .(Node sym var) !.(Rgraph sym var) -> .Rgraph sym var
@@ -45,9 +48,12 @@ rgraphroot   :: !.(Rgraph sym var) -> var
 rgraphgraph  :: !.(Rgraph sym var) -> Graph sym var
 
 // Build a rooted graph from a root and a graph
-mkrgraph     :: .var (Graph .sym .var) -> Rgraph .sym .var
+mkrgraph     :: var (Graph sym var) -> .Rgraph sym var
 
 instance == (Rgraph sym var) | == sym & == var
-instance toString (Rgraph sym var) | toString sym & toString var & == var
-instance <<< Rgraph sym var | toString sym & toString var & == var
-instance <<< Rule sym var | toString sym & toString,== var
+instance toString (Rgraph sym var) | toString sym & toString var & Eq var
+instance <<< (Rgraph sym var) | toString sym & toString var & == var
+instance <<< (Rule sym var) | toString sym & toString,== var
+
+(writergraph) infixl :: *File .(Rgraph sym var) -> .File | toString sym & ==,toString var
+(writerule) infixl :: *File .(Rule sym var) -> .File | toString sym & ==,toString var
diff --git a/sucl/rule.icl b/sucl/rule.icl
index 288b317..a60e72b 100644
--- a/sucl/rule.icl
+++ b/sucl/rule.icl
@@ -111,7 +111,7 @@ Rooted graphs
 >   mkrgraph root graph = (root,graph)
 */
 
-emptyrgraph :: .var -> Rgraph .sym .var
+emptyrgraph :: var -> .Rgraph sym var
 emptyrgraph root = RgraphAlias root emptygraph
 
 updatergraph :: var .(Node sym var) !.(Rgraph sym var) -> .Rgraph sym var
@@ -126,10 +126,10 @@ rgraphroot (RgraphAlias root _) = root
 rgraphgraph  :: !.(Rgraph sym var) -> Graph sym var
 rgraphgraph (RgraphAlias _ graph) = graph
 
-mkrgraph :: .var (Graph .sym .var) -> Rgraph .sym .var
+mkrgraph :: var (Graph sym var) -> .Rgraph sym var
 mkrgraph root graph = RgraphAlias root graph
 
-maprgraph :: (.(var1,Graph sym1 var1) -> (.var2,Graph .sym2 .var2)) !.(Rgraph sym1 var1) -> Rgraph .sym2 .var2
+maprgraph :: (.(var1,Graph sym1 var1) -> .(var2,Graph sym2 var2)) !.(Rgraph sym1 var1) -> .Rgraph sym2 var2
 maprgraph f (RgraphAlias root1 graph1) = RgraphAlias root2 graph2
    where (root2,graph2) = f (root1,graph1)
 
@@ -148,7 +148,7 @@ maprgraph f (RgraphAlias root1 graph1) = RgraphAlias root2 graph2
 >                                 repr'
 */
 
-instance toString Rgraph sym var | toString sym & toString var & == var
+instance toString (Rgraph sym var) | toString sym & toString var & Eq var
 where toString (RgraphAlias root graph)
       = "("+++snd (showsubgraph root ([],"emptyrgraph) "))+++toString root
         where showsubgraph node (seen,repr)
@@ -165,7 +165,7 @@ where toString (RgraphAlias root graph)
 >       = hd (printgraph showfunc shownode graph [root])
 */
 
-instance <<< Rgraph sym var | toString sym & toString var & == var
+instance <<< (Rgraph sym var) | toString sym & toString var & == var
 where (<<<) file (RgraphAlias root graph)
       = file <<< hd (printgraph graph [root])
 
@@ -178,7 +178,7 @@ Rules
 >   rulegraph (lroots,rroot,graph) = graph
 */
 
-mkrule :: [.var] .var (Graph .sym .var) -> Rule .sym .var
+mkrule :: .[var] var (Graph sym var) -> .Rule sym var
 mkrule args root graph = RuleAlias args root graph
 
 arguments :: !.(Rule sym var) -> [var]
@@ -219,10 +219,11 @@ where (==) (RgraphAlias root1 graph1) (RgraphAlias root2 graph2)
        = root1==root2 && graph1==graph2
 
 instance toString (Rule sym var) | toString sym & toString var & == var
-where toString (RuleAlias lroots rroot graph)
+where //toString rule = "<rule>"
+      toString (RuleAlias lroots rroot graph)
       = "((mkrule "+++listToString lroots+++" "+++toString rroot+++repr`+++") emptygraph)"
-        where (seen,repr`) = showsubgraph rroot ([],repr)
-              (seen`,repr) = foldlr showsubgraph (seen,"") lroots
+        where (seen,repr`) = foldlr showsubgraph ([],repr) lroots
+              (seen`,repr) = showsubgraph rroot (seen,"")
               showsubgraph node (seen,repr)
               | not def || isMember node seen
                 = (seen,repr)
@@ -232,5 +233,29 @@ where toString (RuleAlias lroots rroot graph)
                       seen` = [node:seen]
                       repr`` = " o updategraph "+++toString node+++" ("+++toString f+++","+++listToString args+++")"+++repr`
 
-instance <<< Rule sym var | toString sym & toString,== var
+ruleToString :: (sym->.String) .(Rule sym var) -> String | Eq,toString var
+ruleToString symToString (RuleAlias lroots rroot graph)
+/*
+= if def ("<rule with root "+++symToString sym+++">") "<rule with no root>"
+  where (def,(sym,args)) = varcontents graph rroot
+*/
+= "((mkrule "+++showlist toString lroots+++" "+++toString rroot+++repr`+++") emptygraph)"
+  where (seen,repr`) = foldlr showsubgraph ([],repr) lroots
+        (seen`,repr) = showsubgraph rroot (seen,"")
+        showsubgraph node (seen,repr)
+        | not def || isMember node seen
+          = (seen,repr)
+        = (seen``,repr``)
+          where (def,(f,args)) = varcontents graph node
+                (seen``,repr`) = foldlr showsubgraph (seen`,repr) args
+                seen` = [node:seen]
+                repr`` = " o updategraph "+++toString node+++" ("+++symToString f+++","+++showlist toString args+++")"+++repr`
+
+instance <<< (Rule sym var) | toString sym & toString,== var
 where (<<<) file rule = file <<< toString rule
+
+(writergraph) infixl :: *File .(Rgraph sym var) -> .File | toString sym & ==,toString var
+(writergraph) file rgraph = file <<< rgraph
+
+(writerule) infixl :: *File .(Rule sym var) -> .File | toString sym & ==,toString var
+(writerule) file rule = file <<< rule
diff --git a/sucl/spine.dcl b/sucl/spine.dcl
index 15b03ef..88f1e68 100644
--- a/sucl/spine.dcl
+++ b/sucl/spine.dcl
@@ -9,6 +9,7 @@ from pfun import Pfun
 from general import Optional
 from StdOverloaded import ==
 from StdFile import <<<
+from StdString import toString
 
 /*
 
@@ -208,8 +209,8 @@ extendhistory
  |  == var
  &  == pvar
 
-(writeanswer) infixl :: *File (Answer sym var pvar) -> .File | <<< var
+(writeanswer) infixl :: *File (Answer sym var pvar) -> .File | toString sym & ==,toString,<<< var // & ==,toString,<<< pvar
 
-(writespine) infixl :: *File (Spine sym var pvar) -> .File | <<< var
+(writespine) infixl :: *File (Spine sym var pvar) -> .File | toString sym & ==,toString,<<< var // & ==,toString,<<< pvar
 
-instance <<< Subspine sym var pvar
+instance <<< (Subspine sym var pvar) | toString sym & ==,toString,<<< var // & ==,toString,<<< pvar
diff --git a/sucl/spine.icl b/sucl/spine.icl
index 6770061..73000a3 100644
--- a/sucl/spine.icl
+++ b/sucl/spine.icl
@@ -8,7 +8,7 @@ import dnc
 import graph
 import pfun
 import basic
-from general import No,Yes
+from general import No,Yes,--->
 import StdEnv
 
 /*
@@ -239,9 +239,10 @@ spinetip spine = spine
 
 spinenodes :: .(Spine sym var pvar) -> [var]
 spinenodes spine
-= foldspine cons [] [] (const id) [] (const []) partial (const []) redex [] spine
+= ((nodes<---"spine.spinenodes ends") ---> ("spine.spinenodes number of spine nodes is "+++toString (length nodes))) ---> "spine.spinenodes begins"
   where partial _ _ _ = id
         redex _ _ = []
+        nodes = foldspine cons [] [] (const id) [] (const []) partial (const []) redex [] spine
 
 ifopen :: result result !.(Answer sym var pvar) -> result
 ifopen open other spine
@@ -317,12 +318,24 @@ extgraph` sgraph rule
 = extgraph sgraph rgraph (varlist rgraph (arguments rule))
   where rgraph = rulegraph rule
 
-(writeanswer) infixl :: *File (Answer sym var pvar) -> .File | <<< var
+(writeanswer) infixl :: *File (Answer sym var pvar) -> .File | toString sym & ==,toString,<<< var // & ==,toString,<<< pvar
 (writeanswer) file No = file <<< "<root-normal-form>" <<< nl
 (writeanswer) file (Yes spine) = file writespine spine <<< nl
 
-(writespine) infixl :: *File (Spine sym var pvar) -> .File | <<< var
+(writespine) infixl :: *File (Spine sym var pvar) -> .File | toString sym & ==,toString,<<< var // & ==,toString,<<< pvar
 (writespine) file (var,subspine) = file <<< "(" <<< var <<< "," <<< subspine <<< ")"
 
-instance <<< Subspine sym var pvar
-where (<<<) file subspine = file <<< "<subspine>"
+instance <<< (Subspine sym var pvar) | toString sym & ==,toString,<<< var // & ==,toString,<<< pvar
+where
+/*
+      (<<<) file _ = file <<< "<subspine>"
+*/
+      (<<<) file Cycle = file <<< "Cycle"
+      (<<<) file Delta = file <<< "Delta"
+      (<<<) file (Force argno spine) = file <<< "Force " <<< argno <<< " " writespine spine
+      (<<<) file MissingCase = file <<< "MissingCase"
+      (<<<) file (Open pattern) = file <<< "Open <rgraph>"
+      (<<<) file (Partial rule matching focus spine) = file <<< "Partial {rule=<Rule sym pvar>, matching=<Pfun pvar var>, focus=<pvar>, spine=" writespine spine <<< "}"
+      (<<<) file (Unsafe pattern) = file <<< "Unsafe " writergraph pattern
+      (<<<) file (Redex rule matching) = file <<< "Redex {rule=<Rule sym pvar>, matching=<Pfun pvar var>}"
+      (<<<) file Strict = file <<< "Strict"
diff --git a/sucl/strat.dcl b/sucl/strat.dcl
index 1123a78..c397013 100644
--- a/sucl/strat.dcl
+++ b/sucl/strat.dcl
@@ -7,6 +7,7 @@ from history import History
 from rule import Rule
 from graph import Graph,Node
 from StdOverloaded import ==
+from StdClass import Eq
 
 from history import HistoryAssociation,HistoryPattern,Link // for History
 from spine import Spine    // for Answer
@@ -45,11 +46,11 @@ makernfstrategy
     (Strategy sym var pvar (Answer sym var pvar)) // Strategy for a defined node
     .[var]                                        // List of nodes known in RNF (closed pattern nodes of subject rule+strict args)
     var                                           // Root of replacement
-    .(Graph sym var)                              // Subject graph
+    (Graph sym var)                              // Subject graph
  -> Answer sym var pvar
- |  == sym
- &  == var
- &  == pvar
+ |  Eq sym
+ &  Eq var
+ &  Eq pvar
 
 
 /* ------------------------------------------------------------------------
@@ -60,10 +61,10 @@ The funcions below tranform (simpler) strategies into more complicated ones
 // A strategy transformer that checks for partial applications
 checkarity
  :: !(sym -> Int)                         // Arity of function symbol
-    (Strategy sym var .pvar .result)      // Default strategy
-    (Substrategy sym var .pvar .result)   // Substrategy
-    .(Graph sym var)                      // Subject graph
-    ((Subspine sym var .pvar) -> .result) // Spine continuation
+    (Strategy sym var pvar .result)      // Default strategy
+    (Substrategy sym var pvar .result)   // Substrategy
+    (Graph sym var)                      // Subject graph
+    ((Subspine sym var pvar) -> .result) // Spine continuation
     .result                               // RNF continuation
     !.(Node sym var)                      // Subject node
  -> .result
@@ -71,23 +72,23 @@ checkarity
 // A strategy transformer that checks for constructor applications
 checkconstr
  :: (sym->.Bool)
-    (Strategy sym .var .pvar .result)
-    (Substrategy sym .var .pvar .result)
-    (Graph sym .var)
-    ((Subspine sym .var .pvar) -> .result)
+    (Strategy sym var pvar .result)
+    (Substrategy sym var pvar .result)
+    (Graph sym var)
+    ((Subspine sym var pvar) -> .result)
     .result
-    (Node sym .var)
+    .(Node sym var)
  -> .result
 
 // A strategy transformer that checks for primitive symbol applications
 checkimport
  :: !(sym->.Bool)
-    (Strategy sym .var .pvar .result)
-    (Substrategy sym .var .pvar .result)
-    (Graph sym .var)
-    ((Subspine sym .var .pvar) -> .result)
+    (Strategy sym var pvar .result)
+    (Substrategy sym var pvar .result)
+    (Graph sym var)
+    ((Subspine sym var pvar) -> .result)
     .result
-    (Node sym .var)
+    .(Node sym var)
  -> .result
 
 // A strategy transformer that checks (hard coded) laws
@@ -106,7 +107,7 @@ checklaws
 // This is the real thing that characterises the functional strategy
 checkrules
  :: ((Graph sym pvar) pvar var -> .Bool)
-    (sym -> [.Rule sym pvar])
+    (sym -> .[Rule sym pvar])
     (Strategy sym var pvar result)
     (Substrategy sym var pvar result)
     (Graph sym var)
@@ -122,10 +123,10 @@ checkrules
 // for strict arguments
 checkstricts
  :: !(sym -> [.Bool])                     // Strict arguments of function
-    (Strategy sym var .pvar .result)      // Default strategy
-    (Substrategy sym var .pvar .result)   // Substrategy
-    .(Graph sym var)                      // Subject graph
-    ((Subspine sym var .pvar) -> .result) // Spine continuation
+    (Strategy sym var pvar .result)      // Default strategy
+    (Substrategy sym var pvar .result)   // Substrategy
+    (Graph sym var)                      // Subject graph
+    ((Subspine sym var pvar) -> .result) // Spine continuation
     .result                               // RNF continuation
     !.(Node sym var)                      // Subject node
  -> .result
@@ -138,15 +139,15 @@ such as done by a strategy transformer.
 
 // Force evaluation of stricts arguments of a node in the graph
 forcenodes
- :: (Substrategy .sym .var .pvar .result)
-    ((Subspine .sym .var .pvar) -> .result)
+ :: (Substrategy sym var pvar .result)
+    ((Subspine sym var pvar) -> .result)
     .result
-    ![.var]
+    !.[var]
  -> .result
 
 // Try to apply a transformation rule (that doesn't need evaluated arguments)
 rulelaw
- :: .(Rule sym pvar)
+ :: (Rule sym pvar)
  -> Law sym var pvar result
  |  == sym
  &  == var
@@ -154,10 +155,10 @@ rulelaw
 
 // Try to apply a law
 trylaw
- :: .(Graph sym var)
+ :: (Graph sym var)
     (.(Subspine sym var pvar) -> result)
     .[var]
-    .(Rule sym pvar)
+    (Rule sym pvar)
     result
  -> result
  |  == sym
@@ -169,11 +170,11 @@ trylaw
 tryrules
  :: ((Graph sym pvar) pvar var -> .Bool)
     (Substrategy sym var pvar result)
-    .(Graph sym var)
+    (Graph sym var)
     ((Subspine sym var pvar) -> result)
     .[var]
  -> result
-    [.Rule sym pvar]
+    .[Rule sym pvar]
  -> result
  |  == sym
  &  == var
diff --git a/sucl/strat.icl b/sucl/strat.icl
index c1d3bd6..b8500e8 100644
--- a/sucl/strat.icl
+++ b/sucl/strat.icl
@@ -9,7 +9,7 @@ import dnc
 import graph
 import pfun
 import basic
-from general import No,Yes
+from general import No,Yes,--->
 import StdEnv
 
 /*
@@ -103,11 +103,11 @@ makernfstrategy ::
     (Strategy sym var pvar (Answer sym var pvar)) // Strategy for a defined node
     .[var]                                        // List of nodes known in RNF (closed pattern nodes of subject rule+strict args)
     var                                           // Root of replacement
-    .(Graph sym var)                              // Subject graph
+    (Graph sym var)                              // Subject graph
  -> Answer sym var pvar
- |  == sym
- &  == var
- &  == pvar
+ |  Eq sym
+ &  Eq var
+ &  Eq pvar
 
 makernfstrategy hist strat rnfnodes node graph
 = substrat [] spinecont rnfanswer node
@@ -125,7 +125,7 @@ makernfstrategy hist strat rnfnodes node graph
           where (def,cnt) = dnc (const "in makernfstrategy") graph node
                 spinenodes` = [node:spinenodes]
                 subspinecont subspine = spinecont (node,subspine)
-                strat` = checkhistory (graph,node) spinenodes hist strat
+                strat` = (checkhistory--->"strat.checkhistory begins from strat.makernfstrategy.substrat.strat`") (graph,node) spinenodes` hist strat
 
 /*
 
@@ -137,11 +137,11 @@ NORMAL REWRITE RULE STRATEGY
 tryrules
  :: ((Graph sym pvar) pvar var -> .Bool)
     (Substrategy sym var pvar result)
-    .(Graph sym var)
+    (Graph sym var)
     ((Subspine sym var pvar) -> result)
     .[var]
  -> result
-    [.Rule sym pvar]
+    .[Rule sym pvar]
  -> result
  |  == sym
  &  == var
@@ -153,10 +153,10 @@ tryrules matchable substrat subject found sargs
 matchrule
  :: ((Graph sym pvar) pvar var -> .Bool)
     (Substrategy sym var pvar result)
-    .(Graph sym var)
+    (Graph sym var)
     ((Subspine sym var pvar) -> result)
     .[var]
-    .(Rule sym pvar)
+    (Rule sym pvar)
     result
  -> result
  |  == sym
@@ -176,11 +176,11 @@ matchrule matchable substrat subject found sargs rule fail
 
 matchnodes
  :: (pvar var -> .Bool)
-    .(Graph sym var)
+    (Graph sym var)
     (Substrategy sym var pvar result)
     ((Pfun pvar var) pvar (Spine sym var pvar) -> result)
     result
-    .(Graph sym pvar)
+    (Graph sym pvar)
  -> ((Pfun pvar var) -> result)
     [.(pvar,var)]
     (Pfun pvar var)
@@ -259,7 +259,7 @@ Does not try to reduce arguments before matching.
 */
 
 rulelaw
- :: .(Rule sym pvar)
+ :: (Rule sym pvar)
  -> Law sym var pvar result
  |  == sym
  &  == var
@@ -271,10 +271,10 @@ where law substrat subject found rnf snids fail
       = trylaw subject found snids rule fail
 
 trylaw
- :: .(Graph sym var)
+ :: (Graph sym var)
     (.(Subspine sym var pvar) -> result)
     .[var]
-    .(Rule sym pvar)
+    (Rule sym pvar)
     result
  -> result
  |  == sym
@@ -290,8 +290,8 @@ trylaw graph found sargs rule fail
         pairs = zip2 pargs sargs
 
 lawmatch
- :: .(Graph sym pvar)
-    .(Graph sym var)
+ :: (Graph sym pvar)
+    (Graph sym var)
     result
  -> ((Pfun pvar var) -> result)
     [.(pvar,var)]
@@ -321,10 +321,10 @@ FORCING EVALUATION OF (STRICT) ARGUMENTS
 */
 
 forcenodes
- :: (Substrategy .sym .var .pvar .result)
-    ((Subspine .sym .var .pvar) -> .result)
+ :: (Substrategy sym var pvar .result)
+    ((Subspine sym var pvar) -> .result)
     .result
-    ![.var]
+    !.[var]
  -> .result
 
 forcenodes substrat found rnf nodes
@@ -348,25 +348,25 @@ checkhistory
     (History sym var)
     (Strategy sym var pvar result)
  -> Strategy sym var pvar result
- |  == sym
- &  == var
+ |  Eq sym
+ &  Eq var
 
 checkhistory (sgraph,snode) spinenodes history defaultstrategy
- = if (isEmpty histpats) defaultstrategy unsafestrategy
-   where histpats
-          = matchhistory history spinenodes sgraph snode
-         unsafestrategy _ _ found _ _
-          = found (Unsafe (hd histpats))
+= (if (isEmpty histpats) defaultstrategy unsafestrategy) <--- "strat.checkhistory ends"
+  where histpats
+        = (matchhistory--->"history.matchhistory begins from strat.checkhistory.histpats") history spinenodes sgraph snode
+        unsafestrategy _ _ found _ _
+        = found (Unsafe (hd histpats))
 
 
 // Check for curried applications
 
 checkarity
  :: !(sym -> Int)                         // Arity of function symbol
-    (Strategy sym var .pvar .result)      // Default strategy
-    (Substrategy sym var .pvar .result)   // Substrategy
-    .(Graph sym var)                      // Subject graph
-    ((Subspine sym var .pvar) -> .result) // Spine continuation
+    (Strategy sym var pvar .result)      // Default strategy
+    (Substrategy sym var pvar .result)   // Substrategy
+    (Graph sym var)                      // Subject graph
+    ((Subspine sym var pvar) -> .result) // Spine continuation
     .result                               // RNF continuation
     !.(Node sym var)                      // Subject node
  -> .result
@@ -392,10 +392,10 @@ eqlenn n [x:xs]       = eqlenn (n-1) xs
 
 checkstricts
  :: !(sym -> [.Bool])                     // Strict arguments of function
-    (Strategy sym var .pvar .result)      // Default strategy
-    (Substrategy sym var .pvar .result)   // Substrategy
-    .(Graph sym var)                      // Subject graph
-    ((Subspine sym var .pvar) -> .result) // Spine continuation
+    (Strategy sym var pvar .result)      // Default strategy
+    (Substrategy sym var pvar .result)   // Substrategy
+    (Graph sym var)                      // Subject graph
+    ((Subspine sym var pvar) -> .result) // Spine continuation
     .result                               // RNF continuation
     !.(Node sym var)                      // Subject node
  -> .result
@@ -432,7 +432,7 @@ checklaws laws defaultstrategy substrat subject found rnf (ssym,sargs)
 
 checkrules
  :: ((Graph sym pvar) pvar var -> .Bool)
-    (sym -> [.Rule sym pvar])
+    (sym -> .[Rule sym pvar])
     (Strategy sym var pvar result)
     (Substrategy sym var pvar result)
     (Graph sym var)
@@ -453,12 +453,12 @@ checkrules matchable ruledefs defstrat substrat subject found rnf (ssym,sargs)
 
 checkimport
  :: !(sym->.Bool)
-    (Strategy sym .var .pvar .result)
-    (Substrategy sym .var .pvar .result)
-    (Graph sym .var)
-    ((Subspine sym .var .pvar) -> .result)
+    (Strategy sym var pvar .result)
+    (Substrategy sym var pvar .result)
+    (Graph sym var)
+    ((Subspine sym var pvar) -> .result)
     .result
-    (Node sym .var)
+    .(Node sym var)
  -> .result
 
 checkimport local defstrat substrat subject found rnf (ssym,sargs)
@@ -471,12 +471,12 @@ checkimport local defstrat substrat subject found rnf (ssym,sargs)
 
 checkconstr
  :: (sym->.Bool)
-    (Strategy sym .var .pvar .result)
-    (Substrategy sym .var .pvar .result)
-    (Graph sym .var)
-    ((Subspine sym .var .pvar) -> .result)
+    (Strategy sym var pvar .result)
+    (Substrategy sym var pvar .result)
+    (Graph sym var)
+    ((Subspine sym var pvar) -> .result)
     .result
-    (Node sym .var)
+    .(Node sym var)
  -> .result
 
 checkconstr isconstr defstrat substrat subject found rnf (ssym,sargs)
diff --git a/sucl/trace.dcl b/sucl/trace.dcl
index e4adfcd..6db2445 100644
--- a/sucl/trace.dcl
+++ b/sucl/trace.dcl
@@ -299,4 +299,4 @@ foldtransformation
     !.(Transformation sym var pvar)
  -> .subresult
 
-instance <<< Trace sym var pvar | toString sym & <<<,==,toString var
+instance <<< (Trace sym var pvar) | toString sym & ==,toString,<<< var // & ==,toString,<<< pvar
diff --git a/sucl/trace.icl b/sucl/trace.icl
index 0295d5e..48bfe68 100644
--- a/sucl/trace.icl
+++ b/sucl/trace.icl
@@ -263,18 +263,30 @@ foldtransformation ftr reduce annotate stop instantiate abstract knownabstractio
 //      fab (NewAbstraction t) = newabstraction (ftr t)
 //      fab (KnownAbstraction r) = knownabstraction r
 
-instance <<< Trace sym var pvar | toString sym & <<<,==,toString var
-where (<<<) file trace
+instance <<< Trace sym var pvar | toString sym & ==,toString,<<< var // & ==,toString,<<< pvar
+where // (<<<) file trace = error "trace.<<<(Trace): blocked for debugging"
+      (<<<) file trace
       = file <<< "Trace:" <<< nl
              <<< "Stricts: " <<< showlist toString stricts <<< nl
-             <<< "Rule: " <<< toString rule <<< nl
-             <<< "Answer:" <<< nl writeanswer answer // <<< getAnswer trace // answer
-             <<< "History:" <<< nl
-             writeHistory history
-             <<< "Transformation:" <<< nl <<< transf
+             // <<< "Rule: " <<< toString rule <<< nl
+             // <<< "Answer:" <<< nl writeanswer answer
+             // <<< "History:" <<< nl
+             // writeHistory history
+             <<< "Transformation:" <<< nl writeTransformation transf
         where (Trace stricts rule answer history transf) = trace
 
-instance <<< Transformation sym var pvar | toString sym & <<<,==,toString var
+(writeTrace) infixl :: *File .(Trace sym var pvar) -> .File | toString sym & ==,toString,<<< var // & ==,toString,<<< pvar
+(writeTrace) file trace
+= file <<< "Trace:" <<< nl
+       <<< "Stricts: " <<< showlist toString stricts <<< nl
+       // <<< "Rule: " <<< ruleToString toString rule <<< nl
+       // <<< "Answer:" <<< nl writeanswer answer
+       // <<< "History:" <<< nl
+       // writeHistory history
+       <<< "Transformation:" <<< nl writeTransformation transf
+  where (Trace stricts rule answer history transf) = trace
+
+instance <<< Transformation sym var pvar | toString sym & ==,toString,<<< var // & ==,toString,<<< pvar
 where (<<<) file (Reduce reductroot subtrace) = file <<< "Reduce; root of reduct: " <<< reductroot <<< nl <<< subtrace
       (<<<) file (Annotate subtrace) = file <<< "Annotate" <<< nl <<< subtrace
       (<<<) file Stop = file <<< "Stop" <<< nl
@@ -286,3 +298,21 @@ where (<<<) file (Reduce reductroot subtrace) = file <<< "Reduce; root of reduct
                    <<< "Failing match..." <<< nl
                    <<< notrace
                    <<< "End of failing match." <<< nl
+
+(writeTransformation) infixl :: *File .(Transformation sym var pvar) -> .File | toString sym & ==,toString,<<< var // & ==,toString,<<< pvar
+(writeTransformation) file (Reduce reductroot subtrace)
+                      = file <<< "Reduce; root of reduct: " <<< reductroot <<< nl
+                             writeTrace subtrace
+(writeTransformation) file (Annotate subtrace)
+                      = file <<< "Annotate" <<< nl
+                             writeTrace subtrace
+(writeTransformation) file Stop
+                      = file <<< "Stop" <<< nl
+(writeTransformation) file (Instantiate yestrace notrace)
+                      = file <<< "Instantiate" <<< nl
+                             <<< "Successful match..." <<< nl
+                             // writeTrace yestrace
+                             <<< "End of successful match." <<< nl
+                             <<< "Failing match..." <<< nl
+                             // writeTrace notrace
+                             <<< "End of failing match." <<< nl
diff --git a/sucl/trd.dcl b/sucl/trd.dcl
index f1492c3..09b2467 100644
--- a/sucl/trd.dcl
+++ b/sucl/trd.dcl
@@ -16,8 +16,8 @@ If typing does not succeed, the function aborts.
 
 ruletype
  :: .[tvar]
-    ((Node sym var) -> .Rule tsym trvar)
-    .(Rule sym var)
+    ((Node sym var) -> Rule tsym trvar)
+    (Rule sym var)
  -> .Rule tsym tvar
  |  == var
  &  == tsym
diff --git a/sucl/trd.icl b/sucl/trd.icl
index fa2e1c1..45861d8 100644
--- a/sucl/trd.icl
+++ b/sucl/trd.icl
@@ -80,8 +80,8 @@ argument type of n.
 
 ruletype
  :: .[tvar]
-    ((Node sym var) -> .Rule tsym trvar)
-    .(Rule sym var)
+    ((Node sym var) -> Rule tsym trvar)
+    (Rule sym var)
  -> .Rule tsym tvar
  |  == var
  &  == tsym
@@ -112,17 +112,17 @@ been assigned to the node and its arguments.
 */
 
 buildtype
- :: .((Node sym var) -> .Rule tsym trvar)                                       // Assignement of type rules to symbols
+ :: .((Node sym var) -> Rule tsym trvar)                                       // Assignement of type rules to symbols
     .(Graph sym var)                                                            // Graph to which to apply typing
     var                                                                         // ???
-    .([tvar] -> .(z:(Graph tsym tvar) -> .(x:[y:(var,tvar)] -> .result)))       // Continuation
+    .([tvar] -> .(u:(Graph tsym tvar) -> .(v:[w:(var,tvar)] -> .result)))       // Continuation
     .[tvar]                                                                     // Type heap
-    w:(Graph tsym tvar)                                                         // Type graph build so far
-    u:[v:(var,tvar)]                                                            // Assignment of type variables to variables
+    u:(Graph tsym tvar)                                                         // Type graph build so far
+    x:[y:(var,tvar)]                                                            // Assignment of type variables to variables
  -> .result                                                                     // Final result
  |  == var
  &  == trvar
- ,  [u<=x,v<=y,w<=z]
+ ,  [x<=v,v y<=w,x<=y]
 
 buildtype typerule graph node bcont theap tgraph assignment
 | def
@@ -147,13 +147,13 @@ buildtype typerule graph node bcont theap tgraph assignment
 
 sharepair
  :: (.var,.var)                                    // Variables to share
-    w:((.var->var2) -> v:(x:(Graph sym var2) -> .result))       // Continuation
+    w:((.var->var2) -> v:((Graph sym var2) -> .result))       // Continuation
     (.var->var2)                                   // Redirection
-    u:(Graph sym var2)                              // Graph before redirection
+    (Graph sym var2)                              // Graph before redirection
  -> .result                  // Final result
  |  == sym
  &  == var2
- ,  [u<=x,v<=w]
+ ,  [v<=w]
 
 sharepair lrnode spcont redirection graph
 = share (mappair redirection redirection lrnode) spcont redirection graph