aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--sucl/basic.dcl25
-rw-r--r--sucl/basic.icl75
-rw-r--r--sucl/canon.icl12
-rw-r--r--sucl/complete.icl16
-rw-r--r--sucl/dnc.icl1
-rw-r--r--sucl/graph.dcl4
-rw-r--r--sucl/graph.icl28
-rw-r--r--sucl/history.dcl4
-rw-r--r--sucl/history.icl6
-rw-r--r--sucl/loop.icl6
-rw-r--r--sucl/newfold.icl56
-rw-r--r--sucl/newtest.icl63
-rw-r--r--sucl/pfun.icl2
-rw-r--r--sucl/rule.dcl14
-rw-r--r--sucl/rule.icl52
-rw-r--r--sucl/spine.dcl7
-rw-r--r--sucl/spine.icl10
-rw-r--r--sucl/strat.icl4
-rw-r--r--sucl/trace.dcl5
-rw-r--r--sucl/trace.icl28
20 files changed, 337 insertions, 81 deletions
diff --git a/sucl/basic.dcl b/sucl/basic.dcl
index 0d06233..c7d04c7 100644
--- a/sucl/basic.dcl
+++ b/sucl/basic.dcl
@@ -15,6 +15,7 @@ Basic types and functions.
*/
from general import Optional
+from StdFile import <<<
import StdOverloaded
import StdString
@@ -72,6 +73,9 @@ foldmap :: (x:res -> w:res`) w:res` -> u:(![(arg,x:res)] -> v:(arg -> w:res`)) |
// Foldoptional is the standard fold for the optional type.
foldoptional :: .res .(.t -> .res) !(Optional .t) -> .res
+// Force evaluation of first argument to root normal form before returning second
+force :: !.a .b -> .b
+
// Forget drops a mapped value from a map given by a list.
forget :: val -> .(![.(val,res)] -> .[(val,res)]) | == val
@@ -97,6 +101,12 @@ join :: a ![.[a]] -> .[a]
*/
kleene :: !.[symbol] -> .[[symbol]]
+// Lazy variant of the predefined abort function
+error :: .String -> .a
+
+// Determine the string representation of a list
+listToString :: [a] -> String | toString a
+
// Lookup finds a value mapped in a list mapping.
lookup :: u:([(arg,w:res)] -> v:(arg -> w:res)) | == arg, [v u <= w]
@@ -130,6 +140,9 @@ maptl :: .(x:[.a] -> u:[.a]) !w:[.a] -> v:[.a], [u <= v, w <= x]
// Map three functions onto a triple.
maptriple :: x:(.a -> .b) w:(.c -> .d) v:(.e -> .f) -> u:((.a,.c,.e) -> (.b,.d,.f)), [u <= v, u <= w, u <= x]
+// String representation of line terminator
+nl :: String
+
// Pairwith pairs a value with its result under a given function
pairwith :: .(arg -> .res) arg -> (arg,.res)
@@ -156,12 +169,18 @@ relimg :: ![(a,.b)] a -> [.b] | == a
// `Remap x y mapping' alters the mapping by associating y with x, removing the old values.
remap :: a b [.(a,b)] -> .[(a,b)] | == a
+// A variant of foldl that is strict in its accumulator
+sfoldl :: (.a -> .(.b -> .a)) !.a [.b] -> .a
+
// `Shorter xs' determines whether a list is shorter than list `xs'.
shorter :: ![.a] [.b] -> .Bool
// `Showbool b' is the string representation of boolean `b'.
showbool :: .(!.Bool -> a) | fromBool a
+// Determine a string representation of a list
+showlist :: (.elem -> .String) ![.elem] -> String
+
// `Showoptional showa opt' is the string representation of optional value `opt',
// where `showa' determines the string representation of the inner value.
showoptional :: .(.a -> .String) !(Optional .a) -> String
@@ -187,3 +206,9 @@ superset :: .[a] -> .(.[a] -> Bool) | == a
// zipwith zips up two lists with a joining function
zipwith :: (.a .b->.c) ![.a] [.b] -> [.c]
+
+// Strict version of --->, which evaluates its lhs first
+(<---) infix :: !.a !b -> .a | <<< b
+
+// Sequential evaluation of left and right arguments
+($) infixr :: !.a .b -> .b
diff --git a/sucl/basic.icl b/sucl/basic.icl
index 7319b67..bd01b2a 100644
--- a/sucl/basic.icl
+++ b/sucl/basic.icl
@@ -25,7 +25,7 @@ Implementation
//:: Optional t = Absent | Present t
// Now using Optional type from cocl's general module
-from general import Optional,No,Yes
+from general import Optional,No,Yes,--->
instance == (Optional a) | == a
where (==) No No = True
@@ -56,15 +56,16 @@ results recursively, and so on. Duplicates are removed. */
depthfirst :: (res->.[elem]) (elem->res) !.[elem] -> .[res] | == elem
depthfirst generate process xs
-= snd (collect xs ([],[]))
- where collect [] seenrest = seenrest
- collect [x:xs] (seen,rest)
+= snd (collect xs ([],[]))
+ where collect [] seenrest = seenrest
+ collect [x:xs] seenrest
| isMember x seen
- = collect xs (seen,rest)
- = (seen``,[y:rest``])
- where (seen`,rest``) = collect (generate y) ([x:seen],rest`)
- (seen``,rest`) = collect xs ( seen`,rest)
- y = process x
+ = collect xs seenrest
+ = (seen``,[y:rest``])
+ where (seen`,rest``) = collect (generate y) ([x:seen],rest`)
+ (seen``,rest`) = collect xs ( seen`,rest)
+ y = process x
+ (seen,rest) = seenrest
// `Disjoint xs ys' checks whether xs and ys are disjoint.
@@ -89,22 +90,28 @@ foldlm f (l,[m:ms])
(l``,ms`) = foldlm f (l`,ms)
foldlr :: (.elem -> .((.lrinfo,.rlinfo) -> (.lrinfo,.rlinfo))) !(.lrinfo,.rlinfo) ![.elem] -> (.lrinfo,.rlinfo)
-foldlr f (l,r) []
- = (l,r)
-foldlr f (l,r) [x:xs]
+foldlr f lr []
+ = lr
+foldlr f lr [x:xs]
= (l``,r``)
where (l``,r`) = foldlr f (l`,r) xs
(l`,r``) = f x (l,r`)
+ (l,r) = lr
foldmap :: (x:res -> w:res`) w:res` -> u:(![(arg,x:res)] -> v:(arg -> w:res`)) | == arg, [v u <= w, v <= x]
foldmap f d
-= foldr foldmap` (const d)
- where foldmap` (x,y) g v = if (x==v) (f y) (g v)
+= foldr foldmap` (const d)
+ where foldmap` xy g v
+ = if (x==v) (f y) (g v)
+ where (x,y) = xy
foldoptional :: .res .(.t -> .res) !(Optional .t) -> .res
foldoptional no yes No = no
foldoptional no yes (Yes x) = yes x
+force :: !.a .b -> .b
+force x y = y
+
forget :: val -> .(![.(val,res)] -> .[(val,res)]) | == val
forget x = filter (neq x o fst)
neq x y = x <> y
@@ -159,6 +166,14 @@ kleene symbols
= flatten (map appendstrings symbols)
where appendstrings symbol = map (cons symbol) strings
+// Lazy variant of the predefined abort function
+error :: .String -> .a
+error message = abort message
+
+// Determine the string representation of a list
+listToString :: [a] -> String | toString a
+listToString xs = showlist toString xs
+
lookup :: u:([(arg,w:res)] -> v:(arg -> w:res)) | == arg, [v u <= w]
lookup = foldmap id (abort "lookup: not found")
@@ -211,6 +226,10 @@ maptl f [x:xs] = [x:f xs]
maptriple :: x:(.a -> .b) w:(.c -> .d) v:(.e -> .f) -> u:((.a,.c,.e) -> (.b,.d,.f)), [u <= v, u <= w, u <= x]
maptriple f g h = app3 (f,g,h)
+// String representation of line terminator
+nl :: String
+nl =: "\n"
+
partition :: (a -> b) (a -> .c) -> .(!.[a] -> [(b,[.c])]) | == b
partition f g
= h
@@ -227,6 +246,14 @@ relimg rel x` = [y\\(x,y)<-rel|x==x`]
remap :: a b [.(a,b)] -> .[(a,b)] | == a
remap x y xys = [(x,y):forget x xys]
+// A variant of foldl that is strict in its accumulator
+sfoldl :: (.a -> .(.b -> .a)) !.a [.b] -> .a
+sfoldl f a xxs
+#! a = a
+= case xxs
+ of [] -> a
+ [x:xs] -> sfoldl f (f a x) xs
+
shorter :: ![.a] [.b] -> .Bool
shorter [] yys = False
shorter [x:xs] [] = True
@@ -235,6 +262,14 @@ shorter [x:xs] [y:ys] = shorter xs ys
showbool :: .(!.Bool -> a) | fromBool a
showbool = fromBool
+showlist :: (.elem -> .String) ![.elem] -> String
+showlist showa xs
+= "["+++inner xs+++"]"
+ where inner [] = ""
+ inner [x:xs] = showa x+++continue xs
+ continue [] = ""
+ continue [x:xs] = ","+++showa x+++continue xs
+
showoptional :: .(.a -> .String) !(Optional .a) -> String
showoptional showa No = "No"
showoptional showa (Yes a) = "(Yes "+++showa a+++")"
@@ -268,3 +303,15 @@ superset set = isEmpty o (removeMembers set)
zipwith :: (.a .b->.c) ![.a] [.b] -> [.c]
zipwith f xs ys = [f x y \\ x<-xs & y<-ys]
+
+// Strict version of --->, which evaluates its lhs first
+(<---) infix :: !.a !b -> .a | <<< b
+(<---) value message = value ---> message
+
+($) infixr :: !.a .b -> .b
+($) x y = y
+
+(writeList) infixl :: !*File [a] -> .File | <<< a
+(writeList) file [] = file
+(writeList) file [x:xs]
+= file <<< x writeList xs
diff --git a/sucl/canon.icl b/sucl/canon.icl
index d4a860f..95b57a3 100644
--- a/sucl/canon.icl
+++ b/sucl/canon.icl
@@ -5,6 +5,7 @@ implementation module canon
import rule
import graph
import basic
+import general
import StdEnv
/*
@@ -60,7 +61,7 @@ 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
+ = ((relabel heap o etaexpand typerule o splitrg o relabel localheap) rg <--- "canon.canonise ends") ---> "canon.canonise begins"
/*
@@ -113,9 +114,10 @@ localheap =: [0..]
foldarea :: ((Rgraph sym var) -> sym) (Rgraph sym var) -> Node sym var | == var
foldarea label rgraph
- = (label rgraph,foldsingleton single nosingle rgraph)
+ = ((id (labelrgraph,foldsingleton single nosingle rgraph)) <--- "canon.foldarea ends") ---> "canon.foldarea begins"
where single root sym args = args
nosingle = snd (graphvars (rgraphgraph rgraph) [rgraphroot rgraph])
+ labelrgraph = (label rgraph <--- "canon.foldarea.labelrgraph ends") ---> "canon.foldarea.labelrgraph begins"
/*
------------------------------------------------------------------------
@@ -139,13 +141,13 @@ foldarea label rgraph
labelarea :: [Rgraph sym var] [sym] (Rgraph sym var) -> sym | == sym & == var
labelarea areas labels rg
- = foldmap id nolabel (maketable 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"
where nolabel = abort "canon: labelarea: no label assigned to area"
maketable :: [Rgraph sym var] [sym] -> [(Rgraph sym var,sym)] | == var
-maketable [] _ = []
+maketable [] _ = [] <--- "canon.maketable ends empty"
maketable [area:areas] labels
- = [(area,label):maketable 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"
where (label,labels`) = getlabel (nc aroot) labels
getlabel (True,(asym,aargs)) labels
| not (or (map (fst o nc) aargs))
diff --git a/sucl/complete.icl b/sucl/complete.icl
index 25e56c8..136db40 100644
--- a/sucl/complete.icl
+++ b/sucl/complete.icl
@@ -3,6 +3,7 @@ implementation module complete
// $Id$
import graph
+import basic
import StdEnv
/*
@@ -78,10 +79,11 @@ coveredby complete subject pvarss [svar:svars]
| complete (map fst3 closeds)
= and (map covered closeds)
= coveredby complete subject opens svars
- where (opens,closeds) = split pvarss
- covered (sym,repvar`,pvarss`) = coveredby complete subject pvarss` (repvar (repvar` undef) svar++svars)
+ where (opens,closeds) = psplit pvarss
+ covered (sym,repvar`,pvarss`) = coveredby complete subject pvarss` (repvar (repvar` dummyvar) svar++svars)
(sdef,(ssym,sargs)) = varcontents subject svar
tmpvalue = (fst (foldr (spl (repvar sargs) ssym) ([],[]) pvarss))
+ dummyvar = abort "complete: error: accessing dummy variable"
repvar pvars svar = map (const svar) pvars
@@ -94,7 +96,7 @@ multipatterns with an open pattern are expanded and added as well.
*/
-split
+psplit
:: [Pattern sym var]
-> ( [Pattern sym var]
, [ ( sym
@@ -106,14 +108,14 @@ split
| == sym
& == var
-split [] = ([],[])
-split [(subject,[svar:svars]):svarss]
+psplit [] = ([],[])
+psplit [(subject,[svar:svars]):svarss]
| not sdef
= ([(subject,svars):opens`],map add closeds`)
= (opens,[(ssym,repvar,[(subject,sargs++svars):ins]):closeds])
- where (opens`,closeds`) = split svarss
+ where (opens`,closeds`) = psplit svarss
add (sym,repvar,svarss`) = (sym,repvar,[(subject,repvar svar++svars):svarss`])
- (opens,closeds) = split outs
+ (opens,closeds) = psplit outs
(ins,outs) = foldr (spl repvar ssym) ([],[]) svarss
repvar svar = map (const svar) sargs
(sdef,(ssym,sargs)) = varcontents subject svar
diff --git a/sucl/dnc.icl b/sucl/dnc.icl
index 3c644de..1c7e08c 100644
--- a/sucl/dnc.icl
+++ b/sucl/dnc.icl
@@ -3,6 +3,7 @@ implementation module dnc
// $Id$
import graph
+import basic
import StdEnv
// dnc is like varcontents, but can give a more reasonable error message
diff --git a/sucl/graph.dcl b/sucl/graph.dcl
index 3300097..eaeb1d0 100644
--- a/sucl/graph.dcl
+++ b/sucl/graph.dcl
@@ -4,6 +4,7 @@ definition module graph
from pfun import Pfun
from StdOverloaded import ==
+from StdString import String,toString
// A rule associating a replacement with a pattern
//:: Rule sym var
@@ -139,6 +140,9 @@ varlist :: .(Graph sym var) !.[var] -> .[var] | == var
// Cannot remember what this one does???
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
+
// Do reference counting in a graph for the outer bindings.
// References from case branches are counted once only.
// Initial list of variables is counted too.
diff --git a/sucl/graph.icl b/sucl/graph.icl
index 076220b..02362f1 100644
--- a/sucl/graph.icl
+++ b/sucl/graph.icl
@@ -4,6 +4,7 @@ implementation module graph
import pfun
import basic
+import general
import StdEnv
/*
@@ -157,7 +158,30 @@ prefix graph without vars
> = (seen1,'(':showfunc func++concat (map (' ':) repr1)++")"), otherwise
> (seen1,repr1) = foldlr pg (node:seen,[]) args
> (def,(func,args)) = nodecontents graph node
+*/
+
+printgraph :: .(Graph sym var) .[var] -> .[String] | toString sym & toString var & == var
+printgraph graph nodes
+= prntgrph (refcount graph nodes) graph nodes
+
+prntgrph 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)
+ repr2
+ (seen2,repr2)
+ = if (isMember node seen || not def)
+ (seen,toString node)
+ (if (args==[])
+ (seen1,toString func)
+ (seen1,"("+++toString func+++foldr (+++) ")" (map ((+++)" ") repr1)))
+ (seen1,repr1) = foldlr pg ([node:seen],[]) args
+ (def,(func,args)) = varcontents graph node
+/*
> refcount graph
> = foldr rfcnt (const 0)
> where rfcnt node count
@@ -396,5 +420,5 @@ mapgraph ::
mapgraph f (GraphAlias pfun) = GraphAlias (f pfun)
instance == (Graph sym var) | == sym & == var
-where (==) pf1 pf2
- = pf1 == pf2
+where (==) (GraphAlias pf1) (GraphAlias pf2)
+ = ((pf1 == pf2) <--- "graph.==(Graph) ends") ---> "graph.==(Graph) begins"
diff --git a/sucl/history.dcl b/sucl/history.dcl
index 61b0141..1c4913d 100644
--- a/sucl/history.dcl
+++ b/sucl/history.dcl
@@ -6,6 +6,7 @@ from rule import Rgraph
from graph import Graph
from general import Optional
from StdOverloaded import ==
+from StdString import toString
// A history relates node-ids in the subject graph to patterns
:: History sym var
@@ -35,3 +36,6 @@ matchhistory
-> [HistoryPattern sym var] // Matching history patterns
| == sym
& == 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 a97ab37..31d8907 100644
--- a/sucl/history.icl
+++ b/sucl/history.icl
@@ -59,3 +59,9 @@ instantiate ::
([(pvar,var)],[(pvar,var)],[(pvar,var)])
-> ([(pvar,var)],[(pvar,var)],[(pvar,var)])
*/
+
+(writeHistory) infixl :: *File (History sym var) -> .File | toString sym & toString,== var
+(writeHistory) 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
diff --git a/sucl/loop.icl b/sucl/loop.icl
index 88ab3c8..f8674c3 100644
--- a/sucl/loop.icl
+++ b/sucl/loop.icl
@@ -11,7 +11,7 @@ import rule
import graph
import pfun
import basic
-from general import Yes,No
+from general import Yes,No,--->
import StdEnv
/*
@@ -341,8 +341,8 @@ startswith _ _ = False
// ==== ATTEMPT TO UNFOLD A REWRITE RULE ====
-tryunfold
- :: var // The root of the redex
+tryunfold ::
+ var // The root of the redex
(Rule sym pvar) // The rule to unfold
(Pfun pvar var) // The matching from rule's pattern to subject
(Spine sym var pvar) // The spine returned by the strategy
diff --git a/sucl/newfold.icl b/sucl/newfold.icl
index a8afa18..ebb6550 100644
--- a/sucl/newfold.icl
+++ b/sucl/newfold.icl
@@ -11,6 +11,8 @@ import graph
import basic
import StdEnv
+import general
+
/*
newfold.lit - New folding function
@@ -110,9 +112,9 @@ fullfold ::
& == pvar
fullfold trc foldarea fnsymbol trace
-| recursive
- = addlhs recurseresult
-= addlhs (newextract trc foldarea trace)
+| recursive ---> "newfold.fullfold begins"
+ = addlhs recurseresult <--- "newfold.fullfold ends (recursive=True)"
+= addlhs (newextract trc foldarea trace) <--- "newfold.fullfold ends (recursive=False)"
where (recursive,recurseresult) = recurse foldarea fnsymbol trace
addlhs = mapsnd3 (pair (arguments rule))
(Trace _ rule _ _ _) = trace
@@ -137,25 +139,28 @@ recurse ::
& == pvar
recurse foldarea fnsymbol
-= f ([],[])
- where f (newhist,hist) (Trace stricts rule answer history (Reduce reductroot trace))
+= (f ([],[]) <--- "newfold.recurse ends") ---> "newfold.recurse begins"
+ where f newhisthist (Trace stricts rule answer history (Reduce reductroot trace))
| isEmpty pclosed && superset popen ropen
= f (newhist`,newhist`) trace
where rargs = arguments rule; rroot = ruleroot rule; rgraph = rulegraph rule
(pclosed,popen) = graphvars rgraph rargs
(_,ropen) = graphvars rgraph [rroot]
newhist` = [(rroot,rgraph):newhist]
- f (newhist,hist) (Trace stricts rule answer history (Annotate trace))
+ (newhist,hist) = newhisthist
+ f newhisthist (Trace stricts rule answer history (Annotate trace))
| isEmpty pclosed && superset popen ropen
= f (newhist`,hist) trace
where rargs = arguments rule; rroot = ruleroot rule; rgraph = rulegraph rule
(pclosed,popen) = graphvars rgraph rargs
(_,ropen) = graphvars rgraph [rroot]
newhist` = [(rroot,rgraph):newhist]
- f (newhist,hist) (Trace stricts rule answer history transf)
+ (newhist,hist) = newhisthist
+ f newhisthist (Trace stricts rule answer history transf)
= foldtips foldarea (fnsymbol,arguments rule) (removeDup newhist`,removeDup hist) (Trace stricts rule answer history transf)
where rroot = ruleroot rule; rgraph = rulegraph rule
newhist` = [(rroot,rgraph):newhist]
+ (newhist,hist) = newhisthist
/*
@@ -252,24 +257,25 @@ newextract ::
& == pvar
newextract trc newname (Trace stricts rule answer history transf)
-| recursive
- = (stricts,rule2body recrule,recareas)
+| recursive ---> "newfold.newextract begins"
+ = (stricts,rule2body recrule,recareas) <--- "newfold.newextract ends (recursive=True)"
= case transf
of Reduce reductroot trace
- -> newextract trc newname trace
+ -> newextract trc newname trace <--- "newfold.newextract ends (at Reduce transformation)"
Annotate trace
- -> newextract trc newname trace
+ -> newextract trc newname trace <--- "newfold.newextract ends (at Annotate transformation)"
Instantiate yestrace notrace
- -> (stricts,matchpattern answer yesbody nobody,yesareas++noareas)
+ -> (stricts,matchpattern answer yesbody nobody,yesareas++noareas) <--- "newfold.newextract ends (at Instantiate transformation)"
where (_,yesbody,yesareas) = newextract trc newname yestrace
(_,nobody,noareas) = newextract trc newname notrace
Stop
- -> (stricts,buildgraph rargs rroot stoprgraph,stopareas)
+ -> (stricts,buildgraph rargs rroot stoprgraph,stopareas) <--- "newfold.newextract ends (at Stop transformation)"
where (recursive,unsafearea)
= if (isreduce transf)
- (foldoptional (False,undef) (findspinepart rule transf) answer)
+ (foldoptional (False,dummycontents) (findspinepart rule transf) answer)
(False,abort "newextract: not a Reduce transformation")
+ dummycontents = abort "newfold: newextract: accessing dummy node contents"
(recrule,recareas) = splitrule newname rnfnodes deltanodes rule unsafearea
(stoprgraph,stopareas) = finishfold newname rnfnodes deltanodes rroot rgraph
@@ -283,8 +289,12 @@ buildgraph ::
[var]
var
(Graph sym var)
- -> FuncBody sym var
-buildgraph _ _ _ = undef
+ -> 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
+ closedreplnodes = fst (graphvars graph [root])
+ patnodes = varlist graph args
isreduce (Reduce reductroot trace) = True
isreduce transf = False
@@ -313,7 +323,9 @@ findspinepart rule transf spine
= (True,mkrgraph node pattern`)
= recursion
force _ res = res
- partial rule matching _ (pattern,recursion) = (extgraph` graph rule matching pattern,recursion)
+ partial rule matching _ pr
+ = (extgraph` graph rule matching pattern,recursion)
+ where (pattern,recursion) = pr
redex rule matching = (extgraph` graph rule matching emptygraph,norecursion)
stop = (emptygraph,norecursion)
norecursion = (False,abort "findspinepart: no part of spine found")
@@ -381,3 +393,13 @@ getdeltanodes spine
force _ nodes = (True,nodes)
partial _ _ _ nodes = (False,nodes)
redex _ _ = none
+
+instance <<< FuncBody sym var | toString sym & ==,toString var
+where (<<<) file (MatchPattern pat yesbody nobody)
+ = file <<< "?Match: " <<< pat <<< nl
+ <<< "Match succes:" <<< nl
+ <<< yesbody
+ <<< "Match failure:" <<< nl
+ <<< nobody
+ (<<<) file (BuildGraph rgraph)
+ = file <<< "Build: " <<< toString rgraph <<< nl
diff --git a/sucl/newtest.icl b/sucl/newtest.icl
index 688cb08..d9a7087 100644
--- a/sucl/newtest.icl
+++ b/sucl/newtest.icl
@@ -13,6 +13,7 @@ import rule
import graph
import canon
import basic
+import general
import StdEnv
/*
@@ -157,6 +158,32 @@ 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
+where toString srr
+ = "Task: "+++toString srr.srr_task_expression+++
+ "\nSymbol: "+++toString srr.srr_assigned_symbol+++
+ "\nStrictness: "+++listToString srr.srr_strictness+++
+ "\nTyperule: "+++"<typerule>"+++
+ "\nTrace: "+++"<trace>"+++
+ "\nFunction definition: "+++"<funcdef>"+++
+ "\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 <--- "newtest.<<<(Symredresult).srr_task_expression ends") ---> "newtest.<<<(Symredresult).srr_task_expression begins") <<< nl
+ <<< "Assigned symbol: " <<< toString (srr.srr_assigned_symbol) <<< nl
+ <<< "Strictness: " <<< srr.srr_strictness <<< nl
+ <<< "Type rule: ..." <<< nl
+ <<< srr.srr_trace <<< nl
+ //<<< "Function definition: ..." <<< nl
+ <<< "Areas:" <<< nl
+ writeareas srr.srr_areas
+ <<< "==[END]==" <<< nl
+
+(writeareas) infixl :: *File [Rgraph sym var] -> .File | toString sym & toString,== var
+(writeareas) file xs = sfoldl (<<<) file xs
+
/*
> listopt :: [char] -> [[char]] -> [char]
@@ -276,13 +303,13 @@ fullsymred ::
fullsymred freshsymbols cli
= results
- where results = depthfirst generate process (initareas cli)
- generate result = map canonise` (getareas result)
- process area = symredarea foldarea` cli area
+ where results = (depthfirst generate process (initareas cli) <--- "newtest.fullsymred.results ends") ---> "newtest.fullsymred.results begins"
+ generate result = (map canonise` (getareas result) <--- "newtest.fullsymred.generate begins") ---> "newtest.fullsymred.generate begins"
+ process area = (symredarea foldarea` cli area <--- "newtest.fullsymred.process ends") ---> "newtest.fullsymred.process begins"
- foldarea` = foldarea (labelarea` o canonise`)
- labelarea` = labelarea (map getinit results) freshsymbols
- canonise` = canonise (typerule cli) suclheap
+ foldarea` = ((id (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"
/*
`Initareas cli' is the list of initial rooted graphs that must be
@@ -315,10 +342,12 @@ initareas cli
targs = arguments (typerule cli symbol)
getinit :: (Symredresult sym var tsym tvar) -> Rgraph sym var
-getinit srr = srr.srr_task_expression
+getinit srr
+= (srr.srr_task_expression <--- "newtest.getinit ends") ---> "newtest.getinit begins"
getareas :: (Symredresult sym var tsym tvar) -> [Rgraph sym var]
-getareas srr = srr.srr_areas
+getareas srr
+= (srr.srr_areas <--- "newtest.getareas ends") ---> "newtest.getareas begins"
/*
`Symredarea' is the function that does symbolic reduction of a single
@@ -352,20 +381,20 @@ symredarea ::
-> Symredresult SuclSymbol SuclVariable SuclTypeSymbol SuclTypeVariable
symredarea foldarea cli area
-= { srr_task_expression = area
- , srr_assigned_symbol = symbol
- , srr_strictness = stricts
+= { srr_task_expression = (area <--- "newtest.symredarea.srr_task_expression ends") ---> "newtest.symredarea.srr_task_expression begins"
+ , srr_assigned_symbol = (symbol <--- "newtest.symredarea.srr_assigned_symbol ends") ---> "newtest.symredarea.srr_assigned_symbol begins"
+ , srr_strictness = (stricts <--- "newtest.symredarea.srr_strictness ends") ---> "newtest.symredarea.srr_strictness begins"
, srr_typerule = trule
- , srr_trace = trace
- , srr_function_def = rules
- , srr_areas = areas
+ , srr_trace = (trace <--- "newtest.symredarea.srr_trace ends") ---> "newtest.symredarea.srr_trace begins"
+ , srr_function_def = (rules <--- "newtest.symredarea.srr_function_def ends") ---> "newtest.symredarea.srr_function_def begins"
+ , srr_areas = (areas <--- "newtest.symredarea.srr_areas ends") ---> "newtest.symredarea.srr_areas begins"
}
where agraph = rgraphgraph area; aroot = rgraphroot area
(symbol,aargs) = foldarea area
arule = mkrule aargs aroot agraph
- trule = ruletype sucltypeheap (ctyperule SuclFN sucltypeheap (typerule cli)) arule
- trace = loop strategy` matchable` (removeMembers suclheap (varlist agraph [aroot]),arule)
- (stricts,rules,areas) = fullfold (trc symbol) foldarea symbol trace
+ 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"
+ (stricts,rules,areas) = (fullfold (trc symbol) foldarea symbol trace <--- "newtest.symredarea.(,,).fullfold ends") ---> "newtest.symredarea.(,,).fullfold begins"
matchable` = matchable (complete cli)
strategy` = clistrategy cli
diff --git a/sucl/pfun.icl b/sucl/pfun.icl
index 053799f..111ecdf 100644
--- a/sucl/pfun.icl
+++ b/sucl/pfun.icl
@@ -76,7 +76,7 @@ where toString pfun
where printlink (arg,res) = fromString (toString arg)++['|->']++fromString (toString res)
pfunlist :: (Pfun dom res) -> [(dom,res)]
-pfunlist _ = abort "pfunlist not implemented"
+pfunlist _ = error "pfunlist not implemented"
idpfun :: !.[dom] .(Pfun dom dom) -> Bool | == dom
idpfun domain pfun
diff --git a/sucl/rule.dcl b/sucl/rule.dcl
index e7b408c..a865837 100644
--- a/sucl/rule.dcl
+++ b/sucl/rule.dcl
@@ -3,7 +3,8 @@ definition module rule
// $Id$
from graph import Graph,Node
-from StdOverloaded import ==
+from StdOverloaded import ==,toString
+from StdFile import <<<
// --- Exported types
@@ -16,13 +17,15 @@ from StdOverloaded import ==
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]
+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
+rulegraph :: !.(Rule sym var) -> Graph sym var
+
+instance toString Rule sym var | toString sym & toString var & == var
// --- Functions on rooted graphs
@@ -45,3 +48,6 @@ rgraphgraph :: !.(Rgraph sym var) -> Graph 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
diff --git a/sucl/rule.icl b/sucl/rule.icl
index 24c2e46..288b317 100644
--- a/sucl/rule.icl
+++ b/sucl/rule.icl
@@ -7,7 +7,7 @@ import basic
import StdEnv
:: Rule sym var
- :== ([var],var,Graph sym var)
+ = RuleAlias [var] var (Graph sym var)
:: Rgraph sym var
= RgraphAlias var (Graph sym var)
@@ -146,11 +146,30 @@ maprgraph f (RgraphAlias root1 graph1) = RgraphAlias root2 graph2
> = "updatergraph "++shownode node++" ("++
> showfunc f++',':showlist shownode args++")."++
> repr'
+*/
+
+instance toString Rgraph sym var | toString sym & toString var & == 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`
+/*
> printrgraph showfunc shownode (root,graph)
> = hd (printgraph showfunc shownode graph [root])
+*/
+instance <<< Rgraph sym var | toString sym & toString var & == var
+where (<<<) file (RgraphAlias root graph)
+ = file <<< hd (printgraph graph [root])
+/*
Rules
> mkrule lroots rroot graph = (lroots,rroot,graph)
@@ -160,16 +179,16 @@ Rules
*/
mkrule :: [.var] .var (Graph .sym .var) -> Rule .sym .var
-mkrule args root graph = (args,root,graph)
+mkrule args root graph = RuleAlias args root graph
-arguments :: !(Rule .sym .var) -> [.var]
-arguments (args,_,_) = args
+arguments :: !.(Rule sym var) -> [var]
+arguments (RuleAlias args _ _) = args
-ruleroot :: !(Rule .sym .var) -> .var
-ruleroot (_,root,_) = root
+ruleroot :: !.(Rule sym var) -> var
+ruleroot (RuleAlias _ root _) = root
-rulegraph :: !(Rule .sym .var) -> Graph .sym .var
-rulegraph (_,_,graph) = graph
+rulegraph :: !.(Rule sym var) -> Graph sym var
+rulegraph (RuleAlias _ _ graph) = graph
/*
> showrule showfunc shownode (lroots,rroot,graph)
@@ -198,3 +217,20 @@ rulegraph (_,_,graph) = graph
instance == (Rgraph sym var) | == sym & == var
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)
+ = "((mkrule "+++listToString lroots+++" "+++toString rroot+++repr`+++") emptygraph)"
+ where (seen,repr`) = showsubgraph rroot ([],repr)
+ (seen`,repr) = foldlr showsubgraph (seen,"") lroots
+ 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`
+
+instance <<< Rule sym var | toString sym & toString,== var
+where (<<<) file rule = file <<< toString rule
diff --git a/sucl/spine.dcl b/sucl/spine.dcl
index 0aae75a..15b03ef 100644
--- a/sucl/spine.dcl
+++ b/sucl/spine.dcl
@@ -8,6 +8,7 @@ from graph import Graph
from pfun import Pfun
from general import Optional
from StdOverloaded import ==
+from StdFile import <<<
/*
@@ -206,3 +207,9 @@ extendhistory
-> History sym var
| == var
& == pvar
+
+(writeanswer) infixl :: *File (Answer sym var pvar) -> .File | <<< var
+
+(writespine) infixl :: *File (Spine sym var pvar) -> .File | <<< var
+
+instance <<< Subspine sym var pvar
diff --git a/sucl/spine.icl b/sucl/spine.icl
index 6bb12b2..6770061 100644
--- a/sucl/spine.icl
+++ b/sucl/spine.icl
@@ -316,3 +316,13 @@ extgraph` :: (Graph sym var) (Rule sym pvar) -> (Pfun pvar var) (Graph sym var)
extgraph` sgraph rule
= extgraph sgraph rgraph (varlist rgraph (arguments rule))
where rgraph = rulegraph rule
+
+(writeanswer) infixl :: *File (Answer sym var pvar) -> .File | <<< var
+(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) file (var,subspine) = file <<< "(" <<< var <<< "," <<< subspine <<< ")"
+
+instance <<< Subspine sym var pvar
+where (<<<) file subspine = file <<< "<subspine>"
diff --git a/sucl/strat.icl b/sucl/strat.icl
index 04ea9f9..c1d3bd6 100644
--- a/sucl/strat.icl
+++ b/sucl/strat.icl
@@ -98,8 +98,8 @@ Types
//------------------------------------------------------------------------
-makernfstrategy
- :: .(History sym var) // History of previous rooted graphs attached to nodes
+makernfstrategy ::
+ .(History sym var) // History of previous rooted graphs attached to nodes
(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
diff --git a/sucl/trace.dcl b/sucl/trace.dcl
index 8b818f8..e4adfcd 100644
--- a/sucl/trace.dcl
+++ b/sucl/trace.dcl
@@ -5,6 +5,9 @@ definition module trace
from spine import Answer
from history import History,HistoryAssociation,HistoryPattern
from rule import Rule
+from StdFile import <<<
+from StdOverloaded import ==
+from StdString import toString
// Transitive necessities
@@ -295,3 +298,5 @@ foldtransformation
(.result -> .absresult)
!.(Transformation sym var pvar)
-> .subresult
+
+instance <<< Trace sym var pvar | toString sym & <<<,==,toString var
diff --git a/sucl/trace.icl b/sucl/trace.icl
index 090f4b2..0295d5e 100644
--- a/sucl/trace.icl
+++ b/sucl/trace.icl
@@ -5,6 +5,8 @@ implementation module trace
import spine
import history
import rule
+import basic
+import syntax
import StdEnv
/*
@@ -237,7 +239,7 @@ foldtrace reduce annotate stop instantiate trace
ftf stricts rule answer history (Annotate trace) = annotate stricts rule answer history (ftr trace)
ftf stricts rule answer history Stop = stop stricts rule answer history
ftf stricts rule answer history (Instantiate yestrace notrace) = instantiate stricts rule answer history (ftr yestrace) (ftr notrace)
-// ftf _ _ _ _ (Abstract _) = abort "foldtrace not implemented for abstraction nodes"
+// ftf _ _ _ _ (Abstract _) = error "foldtrace not implemented for abstraction nodes"
foldtransformation
:: ((Trace sym var pvar) -> .result)
@@ -260,3 +262,27 @@ foldtransformation ftr reduce annotate stop instantiate abstract knownabstractio
// ftf (Abstract as) = abstract (map fab as)
// fab (NewAbstraction t) = newabstraction (ftr t)
// fab (KnownAbstraction r) = knownabstraction r
+
+instance <<< Trace sym var pvar | toString sym & <<<,==,toString var
+where (<<<) 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
+ where (Trace stricts rule answer history transf) = trace
+
+instance <<< Transformation sym var pvar | toString sym & <<<,==,toString var
+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
+ (<<<) file (Instantiate yestrace notrace)
+ = file <<< "Instantiate" <<< nl
+ <<< "Successful match..." <<< nl
+ <<< yestrace
+ <<< "End of successful match." <<< nl
+ <<< "Failing match..." <<< nl
+ <<< notrace
+ <<< "End of failing match." <<< nl
generated by cgit v1.2.3 (git 2.39.1) at 2025-03-15 00:45:51 +0000