aboutsummaryrefslogtreecommitdiff
path: root/sucl
diff options
context:
space:
mode:
Diffstat (limited to 'sucl')
-rw-r--r--sucl/Makefile2
-rw-r--r--sucl/graph.dcl1
-rw-r--r--sucl/graph.icl17
-rw-r--r--sucl/history.dcl9
-rw-r--r--sucl/history.icl28
-rw-r--r--sucl/newtest.icl35
-rw-r--r--sucl/pfun.dcl8
-rw-r--r--sucl/pfun.icl14
-rw-r--r--sucl/rule.dcl24
-rw-r--r--sucl/rule.icl108
-rw-r--r--sucl/spine.dcl13
-rw-r--r--sucl/spine.icl44
-rw-r--r--sucl/trace.dcl15
-rw-r--r--sucl/trace.icl48
14 files changed, 289 insertions, 77 deletions
diff --git a/sucl/Makefile b/sucl/Makefile
index 7e8ecf5..19c69c5 100644
--- a/sucl/Makefile
+++ b/sucl/Makefile
@@ -37,7 +37,7 @@ $(SYS)/coreclean.abc: coreclean.icl coreclean.dcl strat.dcl spine.dcl rule.dcl g
$(SYS)/loop.abc: loop.icl loop.dcl strat.dcl trace.dcl spine.dcl history.dcl rewr.dcl rule.dcl graph.dcl pfun.dcl basic.dcl
$(SYS)/strat.abc: strat.icl strat.dcl spine.dcl history.dcl rule.dcl dnc.dcl graph.dcl pfun.dcl basic.dcl
$(SYS)/absmodule.abc: absmodule.icl absmodule.dcl rule.dcl
-$(SYS)/trace.abc: trace.icl trace.dcl spine.dcl history.dcl rule.dcl basic.dcl
+$(SYS)/trace.abc: trace.icl trace.dcl spine.dcl history.dcl rule.dcl graph.dcl basic.dcl
$(SYS)/spine.abc: spine.icl spine.dcl history.dcl rule.dcl graph.dcl pfun.dcl basic.dcl
$(SYS)/history.abc: history.icl history.dcl rule.dcl graph.dcl pfun.dcl basic.dcl
$(SYS)/complete.abc: complete.icl complete.dcl graph.dcl
diff --git a/sucl/graph.dcl b/sucl/graph.dcl
index 0a64c0c..a00a5f0 100644
--- a/sucl/graph.dcl
+++ b/sucl/graph.dcl
@@ -143,6 +143,7 @@ prefix :: .(Graph sym var) .[var] !.[var] -> .([var],[var]) | == var
// Determine a multiline representation of a graph with multiple roots
printgraph :: .(Graph sym var) .[var] -> .[String] | toString sym & toString var & == var
+printgraphBy :: (sym->String) (var->String) .(Graph sym var) .[var] -> .[String] | == var
// Do reference counting in a graph for the outer bindings.
// References from case branches are counted once only.
diff --git a/sucl/graph.icl b/sucl/graph.icl
index 313db51..e0499e0 100644
--- a/sucl/graph.icl
+++ b/sucl/graph.icl
@@ -161,23 +161,26 @@ prefix graph without vars
*/
printgraph :: .(Graph sym var) .[var] -> .[String] | toString sym & toString var & == var
-printgraph graph nodes
-= prntgrph (refcount graph nodes) graph nodes
+printgraph graph nodes = printgraphBy toString toString graph nodes
-prntgrph count graph nodes
+printgraphBy :: (sym->String) (var->String) .(Graph sym var) .[var] -> .[String] | == var
+printgraphBy showsym showvar graph nodes
+= prntgrph showsym showvar (refcount graph nodes) graph nodes
+
+prntgrph showsym showvar count graph nodes
= snd (foldlr pg ([],[]) nodes)
where pg node (seen,reprs)
= (seen2,[repr3:reprs])
where repr3
= if (not (isMember node seen) && def && count node>1)
- (toString node+++":"+++repr2)
+ (showvar node+++":"+++repr2)
repr2
(seen2,repr2)
= if (isMember node seen || not def)
- (seen,toString node)
+ (seen,showvar node)
(if (args==[])
- (seen1,toString func)
- (seen1,"("+++toString func+++foldr (+++) ")" (map ((+++)" ") repr1)))
+ (seen1,showsym func)
+ (seen1,"("+++showsym func+++foldr (+++) ")" (map ((+++)" ") repr1)))
(seen1,repr1) = foldlr pg ([node:seen],[]) args
(def,(func,args)) = varcontents graph node
diff --git a/sucl/history.dcl b/sucl/history.dcl
index af056b6..3daf399 100644
--- a/sucl/history.dcl
+++ b/sucl/history.dcl
@@ -49,3 +49,12 @@ historyToString ::
(writeHistory) infixl :: *File (History sym var) -> .File | toString sym & toString,== var
(writeHistoryAssociation) infixl :: *File (HistoryAssociation sym var) -> .File | toString sym & toString,== var
+
+printhistory ::
+ (sym->String)
+ (var->String)
+ String
+ (History sym var)
+ *File
+ -> .File
+ | == var
diff --git a/sucl/history.icl b/sucl/history.icl
index f3b6c55..c0975a9 100644
--- a/sucl/history.icl
+++ b/sucl/history.icl
@@ -75,3 +75,31 @@ historyToString history
(writeHistoryAssociation) infixl :: *File (HistoryAssociation sym var) -> .File | toString sym & toString,== var
(writeHistoryAssociation) file ha = file <<< "<historyassociation>" // showpair toString (showlist toString) ha <<< nl
+
+printhistory ::
+ (sym->String)
+ (var->String)
+ String
+ (History sym var)
+ *File
+ -> .File
+ | == var
+
+printhistory showsym showvar indent history file
+= foldl (flip (printhistoryassociation showsym showvar indent)) file history
+
+printhistoryassociation showsym showvar indent vargraphs file
+= printlist (myshowrgraph showsym showvar) (indent+++" ") rgraphs (file <<< indent <<< showvar var <<< " <=" <<< nl)
+//= file <<< indent <<< showvar var <<< " <=" <<< showlist (showrgraph showsym showvar) rgraphs <<< nl
+//= file <<< indent <<< showpair showvar (showlist toString) vargraphs <<< nl
+//= file <<< "<history>" <<< nl
+ where (var,rgraphs) = vargraphs
+
+myshowrgraph showsym showvar rgraph
+= hd (printgraphBy showsym showvar (rgraphgraph rgraph) [rgraphroot rgraph])
+
+printlist :: (elem->String) String [elem] *File -> .File
+printlist showelem indent [] file
+= file
+printlist showelem indent [x:xs] file
+= printlist showelem indent xs (file <<< indent <<< showelem x <<< nl)
diff --git a/sucl/newtest.icl b/sucl/newtest.icl
index dbb1028..62bc7ff 100644
--- a/sucl/newtest.icl
+++ b/sucl/newtest.icl
@@ -171,18 +171,29 @@ where toString srr
"\nAreas: "+++listToString srr.srr_areas+++"\n"
instance <<< (Symredresult sym var tsym tvar) | toString sym & <<<,==,toString var
-where (<<<) file srr
- = file <<< "==[BEGIN]==" <<< nl
- <<< "Task expression: " <<< srr.srr_task_expression <<< nl
- <<< "Assigned symbol: " <<< toString (srr.srr_assigned_symbol) <<< nl
- <<< "Strictness: " <<< srr.srr_strictness <<< nl
- //<<< "Type rule: ..." <<< nl
- <<< srr.srr_trace <<< nl
- //<<< "Function definition:" <<< nl
- //<<< srr.srr_function_def
- <<< "Areas:" <<< nl
- writeareas srr.srr_areas
- <<< "==[END]==" <<< nl
+where (<<<) file0 srr
+ = file5
+ where file1
+ = file0 <<< "==[BEGIN]==" <<< nl
+ <<< "Task expression: " <<< srr.srr_task_expression <<< nl
+ <<< "Assigned symbol: " <<< toString (srr.srr_assigned_symbol) <<< nl
+ <<< "Strictness: " <<< srr.srr_strictness <<< nl
+ //<<< "Type rule: ..." <<< nl
+ file2 = printtrace srr.srr_assigned_symbol toString toString toString "" srr.srr_trace file1
+ file3
+ = file2 //<<< "Function definition:" <<< nl
+ //<<< srr.srr_function_def
+ <<< "Areas:" <<< nl
+ file4 = printareas toString toString " " srr.srr_areas file3
+ file5
+ = file4 <<< "==[END]==" <<< nl
+
+printareas :: (sym->String) (var->String) String [Rgraph sym var] *File -> .File | == var
+printareas showsym showvar indent areas file
+= foldl (flip (printarea showsym showvar indent)) file areas
+
+printarea showsym showvar indent area file
+= file <<< indent <<< hd (printgraphBy showsym showvar (rgraphgraph area) [rgraphroot area]) <<< nl
(writeareas) infixl :: *File [Rgraph sym var] -> .File | toString sym & toString,== var
(writeareas) file xs = sfoldl (<<<) file xs
diff --git a/sucl/pfun.dcl b/sucl/pfun.dcl
index 920c28c..2f68103 100644
--- a/sucl/pfun.dcl
+++ b/sucl/pfun.dcl
@@ -4,6 +4,7 @@ definition module pfun
from StdString import toString
from StdOverloaded import ==
+from cleanversion import String
// Partial function abstract type
:: Pfun dom ran
@@ -42,6 +43,13 @@ apply :: !(Pfun dom .ran) dom -> (.Bool,.ran) | == dom
instance toString (Pfun dom ran) | toString dom & toString ran & == dom
(writepfun) infixl :: *File .(Pfun dom ran) -> .File | ==,toString dom & toString ran
+showpfun ::
+ (dom->String)
+ (ran->String)
+ (Pfun dom ran)
+ -> String
+ | == dom
+
/* `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 d263852..0fabaff 100644
--- a/sucl/pfun.icl
+++ b/sucl/pfun.icl
@@ -71,9 +71,17 @@ apply pfun arg
baddomain = abort "apply: partial function applied outside domain"
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)
+where toString pfun = showpfun toString toString pfun
+
+showpfun ::
+ (dom->String)
+ (ran->String)
+ (Pfun dom ran)
+ -> String
+ | == dom
+showpfun showdom showran pfun
+= toString ['{':drop 1 (flatten (map ((cons ',') o printlink) (pfunlist pfun)))++['}']]
+ where printlink (arg,res) = fromString (showdom arg)++['|->']++fromString (showran res)
pfunlist :: (Pfun dom res) -> [(dom,res)] | == dom
pfunlist EmptyPfun = []
diff --git a/sucl/rule.dcl b/sucl/rule.dcl
index f31a7e0..6f61f4c 100644
--- a/sucl/rule.dcl
+++ b/sucl/rule.dcl
@@ -30,6 +30,22 @@ rulegraph :: !.(Rule sym var) -> Graph sym var
instance toString (Rule sym var) | toString sym & toString var & == var
ruleToString :: (sym->.String) .(Rule sym var) -> String | Eq,toString var
+showrule ::
+ (sym->String)
+ (var->String)
+ (Rule sym var)
+ -> String
+ | == var
+
+showruleanch ::
+ (sym->String)
+ (var->String)
+ [Bool]
+ (Rule sym var)
+ [var]
+ -> String
+ | == var
+
// --- Functions on rooted graphs
// The empty rooted graph with a given root
@@ -52,6 +68,14 @@ mkrgraph :: var (Graph sym var) -> .Rgraph sym var
instance == (Rgraph sym var) | == sym & == var
instance toString (Rgraph sym var) | toString sym & toString var & Eq var
+
+showrgraph ::
+ (sym->String)
+ (var->String)
+ (Rgraph sym var)
+ -> String
+ | == var
+
instance <<< (Rgraph sym var) | toString sym & toString var & == var
instance <<< (Rule sym var) | toString sym & toString,== var
diff --git a/sucl/rule.icl b/sucl/rule.icl
index a60e72b..21b7c06 100644
--- a/sucl/rule.icl
+++ b/sucl/rule.icl
@@ -133,32 +133,26 @@ maprgraph :: (.(var1,Graph sym1 var1) -> .(var2,Graph sym2 var2)) !.(Rgraph sym1
maprgraph f (RgraphAlias root1 graph1) = RgraphAlias root2 graph2
where (root2,graph2) = f (root1,graph1)
-/*
-> showrgraph showfunc shownode (root,graph)
-> = '(':snd (showsubgraph root ([],"emptyrgraph) "))++shownode root
-> where showsubgraph node (seen,repr)
-> = (seen,repr), if ~def \/ member seen node
-> = (seen'',repr''), otherwise
-> where (def,(f,args)) = nodecontents graph node
-> (seen'',repr') = foldlr showsubgraph (seen',repr) args
-> seen' = node:seen
-> repr''
-> = "updatergraph "++shownode node++" ("++
-> showfunc f++',':showlist shownode args++")."++
-> repr'
-*/
-
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)
- | 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`` = "updatergraph "+++toString node+++" ("+++toString f+++","+++listToString args+++") o "+++repr`
+where toString rgraph = showrgraph toString toString rgraph
+
+showrgraph ::
+ (sym->String)
+ (var->String)
+ (Rgraph sym var)
+ -> String
+ | == var
+
+showrgraph showsym showvar (RgraphAlias root graph)
+= "("+++snd (showsubgraph root ([],"emptyrgraph) "))+++showvar root
+ where 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`` = "updatergraph "+++showvar node+++" ("+++showsym f+++","+++showlist showvar args+++") o "+++repr`
/*
> printrgraph showfunc shownode (root,graph)
@@ -191,20 +185,6 @@ rulegraph :: !.(Rule sym var) -> Graph sym var
rulegraph (RuleAlias _ _ graph) = graph
/*
-> showrule showfunc shownode (lroots,rroot,graph)
-> = "((mkrule "++showlist shownode lroots++' ':shownode rroot++repr'++") emptygraph)"
-> where (seen,repr') = showsubgraph rroot ([],repr)
-> (seen',repr) = foldlr showsubgraph (seen,"") lroots
-> showsubgraph node (seen,repr)
-> = (seen,repr), if ~def \/ member seen node
-> = (seen'',repr''), otherwise
-> where (def,(f,args)) = nodecontents graph node
-> (seen'',repr') = foldlr showsubgraph (seen',repr) args
-> seen' = node:seen
-> repr''
-> = ".updategraph "++shownode node++" ("++
-> showfunc f++',':showlist shownode args++')':repr'
-
> printrule showfunc shownode (lroots,rroot,graph)
> = (concat.map (++" ").init) reprs++"-> "++last reprs
> where reprs = printgraph showfunc shownode graph (lroots++[rroot])
@@ -219,19 +199,27 @@ where (==) (RgraphAlias root1 graph1) (RgraphAlias root2 graph2)
= root1==root2 && graph1==graph2
instance toString (Rule sym var) | toString sym & toString var & == var
-where //toString rule = "<rule>"
- toString (RuleAlias lroots rroot graph)
- = "((mkrule "+++listToString 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+++" ("+++toString f+++","+++listToString args+++")"+++repr`
+where toString rule = showrule toString toString rule
+
+showrule ::
+ (sym->String)
+ (var->String)
+ (Rule sym var)
+ -> String
+ | == var
+
+showrule showsym showvar (RuleAlias lroots rroot graph)
+= "((mkrule "+++showlist showvar lroots+++" "+++showvar 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 "+++showvar node+++" ("+++showsym f+++","+++showlist showvar args+++")"+++repr`
ruleToString :: (sym->.String) .(Rule sym var) -> String | Eq,toString var
ruleToString symToString (RuleAlias lroots rroot graph)
@@ -259,3 +247,19 @@ where (<<<) file rule = file <<< toString rule
(writerule) infixl :: *File .(Rule sym var) -> .File | toString sym & ==,toString var
(writerule) file rule = file <<< rule
+
+showruleanch ::
+ (sym->String)
+ (var->String)
+ [Bool]
+ (Rule sym var)
+ [var]
+ -> String
+ | == var
+
+showruleanch showsym showvar stricts rule anchors
+= foldr (+++) "" (map2 annot stricts argreprs)+++"-> "+++rootrepr
+ where graph = rulegraph rule; args = arguments rule; root = ruleroot rule
+ (argreprs,[rootrepr:anchorreprs]) = claim args reprs
+ reprs = printgraphBy showsym showvar graph (args++[root:anchors])
+ annot strict repr = (if strict ((+++) "!") id) (repr+++" ")
diff --git a/sucl/spine.dcl b/sucl/spine.dcl
index 88f1e68..c9aa361 100644
--- a/sucl/spine.dcl
+++ b/sucl/spine.dcl
@@ -10,6 +10,7 @@ from general import Optional
from StdOverloaded import ==
from StdFile import <<<
from StdString import toString
+from cleanversion import String
/*
@@ -92,6 +93,18 @@ that the node was in root normal form.
:: Answer sym var pvar
:== Optional (Spine sym var pvar)
+// Write a strategy answer to a file
+printanswer ::
+ (sym->String)
+ (var->String)
+ (pvar->String)
+ String
+ -> (Answer sym var pvar)
+ *File
+ -> .File
+ | == var
+ & == pvar
+
/*
Spine describes the spine returned by a strategy. It contains the node
diff --git a/sucl/spine.icl b/sucl/spine.icl
index 73000a3..cf81386 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
/*
@@ -92,6 +92,22 @@ that the node was in root normal form.
:: Answer sym var pvar
:== Optional (Spine sym var pvar)
+printanswer ::
+ (sym->String)
+ (var->String)
+ (pvar->String)
+ String
+ -> (Answer sym var pvar)
+ *File
+ -> .File
+ | == var
+ & == pvar
+
+printanswer showsym showvar showpvar indent
+= foldoptional (printrnf indent) (printspine showsym showvar showpvar indent)
+
+printrnf indent file = file <<< indent <<< "RNF" <<< nl
+
/*
Spine describes the spine returned by a strategy. It contains the node
@@ -119,6 +135,30 @@ at which the strategy was applied, and the result for that node.
:: Spine sym var pvar
:== (var,Subspine sym var pvar)
+printspine ::
+ (sym->String)
+ (var->String)
+ (pvar->String)
+ String
+ -> (Spine sym var pvar)
+ *File
+ -> .File
+ | == var
+ & == pvar
+
+printspine showsym showvar showpvar indent
+= foldspine pair cycle delta force missingcase open partial unsafe redex strict
+ where pair node (line,printrest) file = printrest (file <<< indent <<< showvar node <<< ": " <<< line <<< nl)
+ cycle = ("Cycle",id)
+ delta = ("Delta",id)
+ force argno printrest = ("Force argument "+++toString argno,printrest)
+ missingcase = ("MissingCase",id)
+ open rgraph = ("Open "+++hd (printgraphBy showsym showpvar (rgraphgraph rgraph) [rgraphroot rgraph]),id)
+ partial rule matching pvar printrest = ("Partial <fn> "+++showruleanch showsym showpvar (repeat False) rule [pvar]+++" <"+++showpvar pvar+++"> "+++showpfun showpvar showvar matching,printrest)
+ unsafe rgraph = ("Unsafe "+++hd (printgraphBy showsym showvar (rgraphgraph rgraph) [rgraphroot rgraph]),id)
+ redex rule matching = ("Redex <fn> "+++showruleanch showsym showpvar (repeat False) rule []+++" "+++showpfun showpvar showvar matching,id)
+ strict = ("Strict",id)
+
/*
Subspine describes what was the result of the strategy applied to a node
@@ -239,7 +279,7 @@ spinetip spine = spine
spinenodes :: .(Spine sym var pvar) -> [var]
spinenodes spine
-= ((nodes<---"spine.spinenodes ends") ---> ("spine.spinenodes number of spine nodes is "+++toString (length nodes))) ---> "spine.spinenodes begins"
+= nodes
where partial _ _ _ = id
redex _ _ = []
nodes = foldspine cons [] [] (const id) [] (const []) partial (const []) redex [] spine
diff --git a/sucl/trace.dcl b/sucl/trace.dcl
index 1964c66..f271084 100644
--- a/sucl/trace.dcl
+++ b/sucl/trace.dcl
@@ -8,6 +8,7 @@ from rule import Rule
from StdFile import <<<
from StdOverloaded import ==
from StdString import toString
+from cleanversion import String
// Transitive necessities
@@ -249,8 +250,22 @@ Implementation
> (args',root':anchors') = claim args reprs
> reprs = printgraph printa printb graph (args++root:anchors)
> annot strict repr = cond strict ('!':) id (repr++" ")
+*/
+
+printtrace ::
+ sym // LHS function symbol
+ (sym->String) // Symbol representation
+ (var->String) // Variable representation for transformed program
+ (pvar->String) // Variable representation for consulted program
+ String // Indent
+ (Trace sym var pvar) // Trace
+ *File // File before writing
+ -> .File // File after writing
+ | == var
+ & == pvar
+/*
Tips traverses a finite trace and produces the list of rewrite rules
that are found at the leaves of the tree. This list of rewrite rules
precisely constitutes the result of symbolic reduction of the original
diff --git a/sucl/trace.icl b/sucl/trace.icl
index 2994757..7cc9d4b 100644
--- a/sucl/trace.icl
+++ b/sucl/trace.icl
@@ -5,6 +5,7 @@ implementation module trace
import spine
import history
import rule
+import graph
import basic
import syntax
import StdEnv
@@ -193,8 +194,55 @@ Implementation
> (args',root':anchors') = claim args reprs
> reprs = printgraph printa printb graph (args++root:anchors)
> annot strict repr = cond strict ('!':) id (repr++" ")
+*/
+printtrace ::
+ sym // LHS function symbol
+ (sym->String) // Symbol representation
+ (var->String) // Variable representation for transformed program
+ (pvar->String) // Variable representation for consulted program
+ String // Indent
+ (Trace sym var pvar) // Trace
+ *File // File before writing
+ -> .File // File after writing
+ | == var
+ & == pvar
+
+printtrace sym showsym showvar showpvar indent trace file0
+= file4
+ where (Trace stricts rule answer history transf) = trace
+ file1 = file0 <<< indent <<< showsym sym <<< " " <<< showruleanch showsym showvar stricts rule (map fst history++answernodes answer) <<< nl
+ file2 = printanswer showsym showvar showpvar (indent+++" ") answer file1
+ file3 = printhistory showsym showvar (indent+++" ") history file2
+ file4 = printtransf sym showsym showvar showpvar indent transf file3
+
+printtransf ::
+ sym // LHS function symbol
+ (sym->String) // Symbol representation
+ (var->String) // Variable representation for transformed program
+ (pvar->String) // Variable representation for consulted program
+ String // Indent
+ (Transformation sym var pvar) // Transformation to print
+ *File // File before writing
+ -> .File // File after writing
+ | == var
+ & == pvar
+
+printtransf sym showsym showvar showpvar indent transf file0
+= case transf
+ of Reduce reductroot trace
+ -> ptr indent trace (file0 <<< indent <<< "Reduce to " <<< showvar reductroot <<< nl)
+ Annotate trace
+ -> ptr indent trace (file0 <<< indent <<< "Annotate" <<< nl)
+ Stop
+ -> file0 <<< indent <<< "Stop" <<< nl
+ Instantiate rgraph yestrace notrace
+ -> ptr indent notrace (ptr (indent+++" ") yestrace (file0 <<< indent <<< "Instantiate " <<< showrgraph showsym showvar rgraph <<< nl))
+ where ptr = printtrace sym showsym showvar showpvar
+
+answernodes = foldoptional [] spinenodes
+/*
Tips traverses a finite trace and produces the list of rewrite rules
that are found at the leaves of the tree. This list of rewrite rules
precisely constitutes the result of symbolic reduction of the original
generated by cgit v1.2.3 (git 2.39.1) at 2025-03-18 13:04:43 +0000