diff options
author | johnvg | 2011-05-10 13:45:26 +0000 |
---|---|---|
committer | johnvg | 2011-05-10 13:45:26 +0000 |
commit | 851602809c397be0fa3bde9ed89eca0a9ebdd927 (patch) | |
tree | c2dd6a8facb349d1c78de019bc2d19822998f0b7 /sucl | |
parent | delete portToNewSyntax (diff) |
delete sucl, the same files can be found in the branch sucl
git-svn-id: https://svn.cs.ru.nl/repos/clean-compiler/trunk@1940 1f8540f1-abd5-4d5b-9d24-4c5ce8603e2d
Diffstat (limited to 'sucl')
43 files changed, 0 insertions, 9063 deletions
diff --git a/sucl/Makefile b/sucl/Makefile deleted file mode 100644 index 909c333..0000000 --- a/sucl/Makefile +++ /dev/null @@ -1,54 +0,0 @@ -#! /usr/bin/make -f - -# $Id$ - -COCL = cocl -#COCLFLAGS = -lat -SYS = Clean\ System\ Files -#SYS = . - -MODULES = cleanversion basic pfun graph dnc rule trd rewr complete history spine trace absmodule strat loop coreclean law canon cli extract newfold newtest expand convert supercompile - -ABC = $(patsubst %,$(SYS)/%.abc,$(MODULES)) - -#default: $(SYS)/history.abc $(SYS)/spine.abc $(SYS)/absmodule.abc $(SYS)/trace.abc $(SYS)/complete.abc $(SYS)/rewr.abc $(SYS)/trd.abc $(SYS)/rule.abc $(SYS)/dnc.abc $(SYS)/graph.abc $(SYS)/pfun.abc $(SYS)/pretty.abc $(SYS)/basic.abc -default: $(ABC) - -clean: - rm -Rf errors.err $(SYS) - -tags: *.dcl *.icl ../compiler/*.dcl ../compiler/*.icl - sh cleantags $^ >$@ - -%: $(SYS)/%.abc - @: - -$(SYS)/%.abc: %.icl - $(COCL) $(COCLFLAGS) $* - -$(SYS)/supercompile.abc: supercompile.icl supercompile.dcl convert.dcl expand.dcl newtest.dcl cli.dcl coreclean.dcl basic.dcl -$(SYS)/convert.abc: convert.icl convert.dcl coreclean.dcl rule.dcl graph.dcl basic.dcl -$(SYS)/expand.abc: expand.icl expand.dcl newtest.dcl newfold.dcl rule.dcl rewr.dcl graph.dcl pfun.dcl basic.dcl -$(SYS)/newtest.abc: newtest.icl newtest.dcl newfold.dcl cli.dcl canon.dcl coreclean.dcl loop.dcl trace.dcl spine.dcl history.dcl complete.dcl trd.dcl rule.dcl graph.dcl basic.dcl -$(SYS)/newfold.abc: newfold.icl newfold.dcl extract.dcl trace.dcl spine.dcl history.dcl rule.dcl dnc.dcl graph.dcl basic.dcl -$(SYS)/extract.abc: extract.icl extract.dcl rule.dcl dnc.dcl graph.dcl basic.dcl -$(SYS)/cli.abc: cli.icl cli.dcl law.dcl coreclean.dcl strat.dcl absmodule.dcl rule.dcl dnc.dcl graph.dcl basic.dcl -$(SYS)/canon.abc: canon.icl canon.dcl rule.dcl graph.dcl basic.dcl -$(SYS)/law.abc: law.icl law.dcl coreclean.dcl strat.dcl spine.dcl rule.dcl dnc.dcl graph.dcl basic.dcl -$(SYS)/coreclean.abc: coreclean.icl coreclean.dcl strat.dcl spine.dcl rule.dcl graph.dcl basic.dcl -$(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 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 -$(SYS)/rewr.abc: rewr.icl rewr.dcl rule.dcl graph.dcl pfun.dcl basic.dcl -$(SYS)/trd.abc: trd.icl trd.dcl rule.dcl graph.dcl basic.dcl -$(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)/basic.abc: basic.icl basic.dcl -$(SYS)/cleanversion.abc: cleanversion.icl cleanversion.dcl diff --git a/sucl/absmodule.dcl b/sucl/absmodule.dcl deleted file mode 100644 index fa81565..0000000 --- a/sucl/absmodule.dcl +++ /dev/null @@ -1,14 +0,0 @@ -definition module absmodule - -// $Id$ - -from rule import Rule - -:: Module sym pvar tsym tvar - = { arities :: [(sym,Int)] // Arity of each symbol - , typeconstructors :: [(tsym,[sym])] // All constructor symbols of each declared algebraic type - , exportedsymbols :: [sym] // Exported function/constructor symbols - , typerules :: [(sym,Rule tsym tvar)] // Principal types of symbols - , stricts :: [(sym,[Bool])] // Strict arguments of functions - , rules :: [(sym,[Rule sym pvar])] // Rewrite rules of each symbol, absent if imported - } diff --git a/sucl/absmodule.icl b/sucl/absmodule.icl deleted file mode 100644 index 4c0f1be..0000000 --- a/sucl/absmodule.icl +++ /dev/null @@ -1,39 +0,0 @@ -implementation module absmodule - -// $Id$ - -import rule - -/* - ------------------------------------------------------------------------- -Exports. - -> %export -> module -> addtalias -> addtsymdef -> addalias -> addsymdef -> newmodule - ------------------------------------------------------------------------- -Includes. - -> %include "basic.lit" -> %include "graph.lit" -extgraph -> %include "rule.lit" - ------------------------------------------------------------------------- -Module implementation. - -*/ - -:: Module sym pvar tsym tvar - = { arities :: [(sym,Int)] // Arity of each symbol - , typeconstructors :: [(tsym,[sym])] // All constructor symbols of each declared algebraic type - , exportedsymbols :: [sym] // Exported function/constructor symbols - , typerules :: [(sym,Rule tsym tvar)] // Principal types of symbols - , stricts :: [(sym,[Bool])] // Strict arguments of functions - , rules :: [(sym,[Rule sym pvar])] // Rewrite rules of each symbol, absent if imported - } diff --git a/sucl/basic.dcl b/sucl/basic.dcl deleted file mode 100644 index 188d8d0..0000000 --- a/sucl/basic.dcl +++ /dev/null @@ -1,223 +0,0 @@ -definition module basic - -// $Id$ - -/* - -Basic definitions -================= - -Description ------------ - -Basic types and functions. - -*/ - -from general import Optional -from StdFile import <<< -import StdOverloaded -import StdString - -/* - -Implementation --------------- - -*/ - -// The optional type of type t is a type like t -// where the actual t value may be present or absent. -//:: Optional t = Absent | Present t -//Now using Optional from cocl's general module - -instance == (Optional a) | == a - - -// Adjust a function for a single argument -adjust :: !arg res (arg->res) !arg -> res | == arg - -// Claim a list of nodes from a heap -claim :: ![.param] u:[.cell] -> ([.cell],v:[.cell]), [u<=v] - -// Cons prepends an element to a list -cons :: .elem u:[.elem] -> v:[.elem], [u <= v] - -// Depthfirst does depth first enumeration of a search process -/* Depthfirst collects results of a function (called process), applied to a - given list of inputs and other inputs which are generated from the - results recursively, and so on. Duplicates are removed. -*/ -depthfirst :: (res->.[elem]) (elem->res) !.[elem] -> .[res] | == elem - -// `Disjoint xs ys' checks whether xs and ys are disjoint. -disjoint :: .[elem] !.[elem] -> Bool | == elem - -// `Eqlen xs ys' determines whether `xs' and `ys' are equally long. -eqlen :: ![.elem1] ![.elem2] -> .Bool - -// Extend a function using the elements of a mapping -extendfn :: [(src,dst)] (src->dst) src -> dst | == src - -// `Foldlm' is a combination of foldl and map. -foldlm :: ((.collect,.elem) -> (.collect,.elem`)) !(.collect,![.elem]) -> (.collect,[.elem`]) - -// Foldlr combines foldl and foldr: -// Information flows both forward and backward through the list. -foldlr :: (.elem -> .((.lrinfo,.rlinfo) -> (.lrinfo,.rlinfo))) !(.lrinfo,.rlinfo) ![.elem] -> (.lrinfo,.rlinfo) - -// Foldmap is the fold function for a map type (from arg to res) given by a list, -// deriving a total function from it giving res`. -foldmap :: (x:res -> w:res`) w:res` -> u:(![(arg,x:res)] -> v:(arg -> w:res`)) | == arg, [v u <= w, v <= x] - -// 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 - -// Indent a list of strings with spaces, -// except the first which is indented with a specific string. -indent :: .String -> .([.String] -> .[String]) - -// `Identifiers' is the list of all identifiers -identifiers :: [String] - -// `Inccounter m f' increments counting function f by one at point m. -inccounter :: a (a->b) a -> b | == a & +,one b - -// `Intersect xs ys' is the intersection of list `ys' with list `xs'. -intersect :: ![elem] [elem] -> .[elem] | == elem - -// `Join x xss' is the join of the list of lists `xss', separated by `x'. -join :: a ![.[a]] -> .[a] - -/* `Kleene xs' determines the kleene closure of the list `xs' of symbols, - i.e. all strings over that list in standard order. The implementation - is designed for maximum sharing. -*/ -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] - -// Map a function onto the zip of two lists. -map2 :: (.a -> .(.b -> .c)) ![.a] [.b] -> [.c] - -// Map a function on the first element of a 2-tuple. -mapfst :: v:(.a -> .b) -> u:((.a,.c) -> (.b,.c)), [u <= v] - -// Map a function on the first element of a triple. -mapfst3 :: v:(.a -> .b) -> u:((.a,.c,.d) -> (.b,.c,.d)), [u <= v] - -// Map a function onto the head of a list. -maphd :: .(.a -> .a) !u:[.a] -> v:[.a], [u <= v] - -// Map a function onto an optional value. -mapoptional :: .(.a -> .b) !(Optional .a) -> Optional .b - -// Map two functions onto a pair. -mappair :: .(.a -> .b) .(.c -> .d) !(.a,.c) -> (.b,.d) - -// Map a function onto the second element of a 2-tuple. -mapsnd :: v:(.a -> .b) -> u:((.c,.a) -> (.c,.b)), [u <= v] - -// Map a function on the second element of a triple. -mapsnd3 :: v:(.a -> .b) -> u:((.c,.a,.d) -> (.c,.b,.d)), [u <= v] - -// Map a function onto the tail of a list. -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) - -// Partition a list. -// The first argument is a representer function that defines partition blocks. -// The second argument is a selector function that is applied to each element of each block. -partition :: (a -> b) (a -> .c) -> .(!.[a] -> [(b,[.c])]) | == b - -// Plookup is a printable lookup with a more readable error message for the not found case. -plookup :: .(arg -> String) ![(arg,.res)] arg -> .res | == arg - -// Power applies a function a number of times to a value. -power :: !Int (.t -> .t) -> .(.t -> .t) - -// Printoptional produces a printable representation of an optional type. -printoptional :: .(.t -> String) !(Optional .t) -> String - -// Proc is an argument-permuted variant of foldr -proc :: .((w:elem -> .(.res -> .res)) -> v:(![w:elem] -> u:(.res -> .res))), [u <= v, u <= w] - -// `Relimg rel x' is the relational image of `x' in relation `rel' (represented by a table). -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 - -// `Showpair showa showb pair' is the string representation of a pair, -// where showa and showb represent the internal types. -showpair :: !.(.a -> .String) !.(.b -> .String) !(.a,.b) -> String - -// `Showstring s' represents a string as a string. -showstring :: .(!.String -> a) | fromString a - -// `Showtriple' determines the string representation of a triple. -showtriple :: !.(.a -> .String) !.(.b -> .String) !.(.c -> .String) !(.a,.b,.c) -> String - -// `Split sep' splits a list into a list of sublists which are separated by `sep'. -split :: a -> .(.[a] -> [.[a]]) | == a - -// `Stub modulename functionname message' aborts with a explanatory message -stub :: .String .String .String -> .a - -// `Superset xs ys' determines whether ys is a superset (actually, super-multi-set or super-list) of xs. -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 - -// 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 - -// Prettyprint a list to a file with indent -printlist :: (elem->String) String [elem] *File -> .File diff --git a/sucl/basic.icl b/sucl/basic.icl deleted file mode 100644 index e6beaa0..0000000 --- a/sucl/basic.icl +++ /dev/null @@ -1,331 +0,0 @@ -implementation module basic - -// $Id$ - -/* - -Basic definitions -================= - -Description ------------ - -Basic types and functions. - -*/ - -import StdEnv - -/* - -Implementation --------------- - -*/ - -//:: Optional t = Absent | Present t -// Now using Optional type from cocl's general module -from general import Optional,No,Yes,---> - -instance == (Optional a) | == a - where (==) No No = True - (==) (Yes x1) (Yes x2) = x1==x2 - (==) _ _ = False - - -// Adjust a function for a single argument - -adjust :: !arg res (arg->res) !arg -> res | == arg -adjust a r f x - | x==a = r - = f x - - -// Claim a list of nodes from a heap -claim :: ![.param] u:[.cell] -> ([.cell],v:[.cell]), [u<=v] - -claim [] heap = ([],heap) -claim [pnode:pnodes] [snode:heap] -= ([snode:snodes],heap`) - where (snodes,heap`) = claim pnodes heap -claim pnodes emptyheap = abort "claim: out of heap" // Just in case. Should be used with an infinite heap. - -/* Depthfirst collects results of a function (called process), applied to a -given list of inputs and other inputs which are generated from the -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] seenrest - | isMember x seen - = 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. - -disjoint :: .[elem] !.[elem] -> Bool | == elem -disjoint xs ys = not (or (map (flip isMember xs) ys)) - -eqlen :: ![.elem1] ![.elem2] -> .Bool -eqlen [x:xs] [y:ys] = eqlen xs ys -eqlen [] [] = True -eqlen xs ys = False - -// Extend a function using the elements of a mapping -extendfn :: [(src,dst)] (src->dst) src -> dst | == src -extendfn mapping f x = foldmap id (f x) mapping x - -// `Foldlm' is a combination of foldl and map. -foldlm :: ((.collect,.elem) -> (.collect,.elem`)) !(.collect,![.elem]) -> (.collect,[.elem`]) -foldlm f (l,[]) = (l,[]) -foldlm f (l,[m:ms]) -= (l``,[m`:ms`]) - where (l`,m`) = f (l,m) - (l``,ms`) = foldlm f (l`,ms) - -foldlr :: (.elem -> .((.lrinfo,.rlinfo) -> (.lrinfo,.rlinfo))) !(.lrinfo,.rlinfo) ![.elem] -> (.lrinfo,.rlinfo) -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` 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 - -inccounter :: a (a->b) a -> b | == a & +,one b -inccounter m f n = if (n==m) (f n+one) (f n) - -indent :: .String -> .([.String] -> .[String]) -indent first = map2 (+++) [first:repeat (createArray (size first) ' ')] - -map2 :: (.a -> .(.b -> .c)) ![.a] [.b] -> [.c] -map2 f [x:xs] [y:ys] = [f x y:map2 f xs ys] -map2 f _ _ = [] - -// `Identifiers' is the list of all identifiers -identifiers :: [String] -identifiers =: map toString (tl (kleene ['abcdefghijklmnopqrstuvwxyz'])) - -// `Intersect xs ys' is the intersection of list `ys' with list `xs'. -intersect :: ![elem] [elem] -> .[elem] | == elem -intersect [] _ = [] -intersect [y:ys] xs = elim (cons y o intersect ys) (intersect ys xs) y xs - -// Elim removes a given element from a list. -// There are two continuations, one for failure and one for success. -elim :: .(v:[elem] -> .res) .res elem u:[elem] -> .res | == elem, [u <= v] -elim found notfound y [] -= notfound -elim found notfound y [x:xs] -| x==y -= found xs -= elim (found o cons x) notfound y xs - -// Cons prepends an element to a list -cons :: .elem u:[.elem] -> v:[.elem], [u <= v] -cons x xs = [x:xs] - -// `Join x xss' is the join of the list of lists `xss', separated by `x'. -join :: a ![.[a]] -> .[a] -join sep [] = [] -join sep [x:xs] = x++flatten (map (cons sep) xs) - -/* `Kleene xs' determines the kleene closure of the list `xs' of symbols, - i.e. all strings over that list in standard order. The implementation - is designed for maximum sharing. -*/ -kleene :: !.[symbol] -> .[[symbol]] -kleene [] = [[]] -kleene symbols -= flatten (iterate prefix [[]]) - where prefix strings - = 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") - -pairwith :: .(arg -> .res) arg -> (arg,.res) -pairwith f x = (x,f x) - -plookup :: .(arg -> String) ![(arg,.res)] arg -> .res | == arg -plookup showa tbl a = foldmap id (abort (showa a+++": not found")) tbl a - -power :: !Int (.t -> .t) -> .(.t -> .t) -power n f -| n <= 0 -= id -= f o power (n-1) f - -printoptional :: .(.t -> String) !(Optional .t) -> String -printoptional printa No = "" -printoptional printa (Yes a) = printa a - -proc :: .((w:elem -> .(.res -> .res)) -> v:(![w:elem] -> u:(.res -> .res))), [u <= v, u <= w] -proc = flip o foldr - -mapfst :: v:(.a -> .b) -> u:((.a,.c) -> (.b,.c)), [u <= v] -mapfst f = app2 (f,id) - -mapfst3 :: v:(.a -> .b) -> u:((.a,.c,.d) -> (.b,.c,.d)), [u <= v] -mapfst3 f = app3 (f,id,id) - -maphd :: .(.a -> .a) !u:[.a] -> v:[.a], [u <= v] -maphd f [] = [] -maphd f [x:xs] = [f x:xs] - -mapoptional :: .(.a -> .b) !(Optional .a) -> Optional .b -mapoptional f No = No -mapoptional f (Yes x) = Yes (f x) - -mappair :: .(.a -> .b) .(.c -> .d) !(.a,.c) -> (.b,.d) -mappair f g (x,y) = (f x,g y) - -mapsnd :: v:(.a -> .b) -> u:((.c,.a) -> (.c,.b)), [u <= v] -mapsnd f = app2 (id,f) - -mapsnd3 :: v:(.a -> .b) -> u:((.c,.a,.d) -> (.c,.b,.d)), [u <= v] -mapsnd3 f = app3 (id,f,id) - -maptl :: .(x:[.a] -> u:[.a]) !w:[.a] -> v:[.a], [u <= v, w <= x] -maptl f [] = [] -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 - where h [] = [] - h [x:xs] - = [((r,[g x:ins])):h outs] - where ins = [g x\\x<-xs|f x==r] - outs = [x\\x<-xs|f x<>r] - r = f x - -relimg :: ![(a,.b)] a -> [.b] | == a -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 -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+++")" - -showpair :: !.(.a -> .String) !.(.b -> .String) !(.a,.b) -> String -showpair showa showb (a,b) = "("+++showa a+++","+++showb b+++")" - -showstring :: .(!.String -> a) | fromString a -showstring = fromString - -showtriple :: !.(.a -> .String) !.(.b -> .String) !.(.c -> .String) !(.a,.b,.c) -> String -showtriple showa showb showc (a,b,c) = "("+++showa a+++","+++showb b+++","+++showc c+++")" - -split :: a -> .(.[a] -> [.[a]]) | == a -split sep -= uncurry cons o spl - where spl [] = ([],[]) - spl [x:xs] - | x==sep - = ([],[ys:yss]) - = ([x:ys],yss) - where (ys,yss) = spl xs - -// `Stub modulename functionname message' aborts with a explanatory message -stub :: .String .String .String -> .a -stub modulename functionname message -= abort (modulename+++": "+++functionname+++": "+++message) - -superset :: .[a] -> .(.[a] -> Bool) | == a -superset set = isEmpty o ((--) 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 - -// 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] -= file <<< x <<< nl writeList xs - -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/canon.icl b/sucl/canon.icl deleted file mode 100644 index 515404f..0000000 --- a/sucl/canon.icl +++ /dev/null @@ -1,227 +0,0 @@ -implementation module canon - -// $Id$ - -import rule -import graph -import basic -import general -import StdEnv - -/* - -canon.lit - Area canonicalization -================================= - -Description ------------ - -This script defines functions for folding areas and generating canonical -forms from them for renewed symbolic reduction. - ------------------------------------------------------------------------- - -Interface ---------- - -Exported identifiers: - -> %export -> canonise || Transform an area into canonical form -> foldarea || Fold an area to an application of its assigned symbol -> labelarea || Use a list of symbols to label a list of areas - ------------------------------------------------------------------------- - -Includes --------- - -> %include "basic.lit" -uncurry -split -> %include "graph.lit" -extgraph -> %include "rule.lit" - ------------------------------------------------------------------------- - -`Canonise heap' canonises an area to a standard form, so that equal -areas are detected by the `=' operator. Canonisation is done in three -steps: - -(1) Splitting arguments to prevent too much sharing and allowing delta - functions to be recognised. - -(2) Adding extra arguments to the full complement according to the type - rule for the top symbol. - -(3) Relabeling the nodes in a standard way. - -> canonise :: (*->rule **** *****) -> [***] -> rgraph * ** -> rgraph * *** -> canonise typerule heap = relabel heap.etaexpand typerule.splitrg.relabel localheap - -*/ - -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 - -/* - -> split :: rgraph * num -> rgraph * num -> split rgraph -> = foldsingleton single rgraph rgraph -> where single root sym args = mkrgraph root (updategraph root (sym,fst (claim args (localheap--[root]))) emptygraph) - -*/ - -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 (localheap--[root]))) emptygraph) - -/* -> uncurry :: (*->rule **** *****) -> rgraph * num -> rgraph * num -> uncurry typerule rgraph -> = f (nc root) -> where f (True,(sym,args)) -> = mkrgraph root (updategraph root (sym,fst (claim targs (args++localheap--nodelist graph [root]))) graph) -> where targs = lhs (typerule sym) -> f cont = rgraph -> nc = nodecontents graph -> root = rgraphroot rgraph; graph = rgraphgraph 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,take (arity sym) (args++(localheap--(varlist graph [root])))) graph) - f cont = rgraph - nc = varcontents graph - root = rgraphroot rgraph; graph = rgraphgraph rgraph - -localheap :: [Int] -localheap =: [0..] - -/* ------------------------------------------------------------------------- - -> foldarea :: (rgraph * **->*) -> rgraph * ** -> (*,[**]) -> foldarea label rgraph -> = (label rgraph,foldsingleton single nosingle rgraph) -> where single root sym args = args -> nosingle = snd (varset (rgraphgraph rgraph) [rgraphroot rgraph]) -*/ - -foldarea :: ((Rgraph sym var) -> sym) (Rgraph sym var) -> Node sym var | == var -foldarea label rgraph - = (labelrgraph,foldsingleton single nosingle rgraph) - where single root sym = id - nosingle = snd (graphvars (rgraphgraph rgraph) [rgraphroot rgraph]) - labelrgraph = label rgraph - -/* ------------------------------------------------------------------------- - -> labelarea :: [rgraph * **] -> [*] -> rgraph * ** -> * -> labelarea areas labels -> = foldmap id nolabel (maketable areas labels) -> where nolabel = error "labelarea: no label assigned to area" - -> maketable :: [rgraph * **] -> [*] -> [(rgraph * **,*)] -> maketable [] = const [] -> maketable (area:areas) labels -> = (area,label):maketable areas labels' -> where (label,labels') = getlabel (nc aroot) labels -> getlabel (True,(asym,aargs)) labels = (asym,labels), if ~or (map (fst.nc) aargs) -> getlabel acont (label:labels) = (label,labels) -> getlabel = error "maketable: out of labels" -> nc = varcontents agraph -> aroot = rgraphroot area; agraph = rgraphgraph area -*/ - -labelarea :: (sym->Bool) [Rgraph sym var] [sym] (Rgraph sym var) -> sym | == sym & == var -labelarea reusable areas labels rg - = foldmap id nolabel (maketable reusable areas labels) rg - where nolabel = abort "canon: labelarea: no label assigned to area" - -maketable :: (sym->Bool) [Rgraph sym var] [sym] -> [(Rgraph sym var,sym)] | == var -maketable _ [] _ = [] -maketable reusable [area:areas] labels - = [(area,label):maketable reusable areas labels`] - where (label,labels`) = getlabel (nc aroot) labels - getlabel (True,(asym,aargs)) labels - | reusable asym && not (or (map (fst o nc) aargs)) - = (asym,labels) - getlabel acont [label:labels] - = (label,labels) - getlabel _ _ - = abort "canon: maketable: out of labels" - nc = varcontents agraph - aroot = rgraphroot area; agraph = rgraphgraph area - -/* ------------------------------------------------------------------------- - -> relabel :: [***] -> rgraph * ** -> rgraph * *** - -> relabel heap rgraph -> = mkrgraph (move root) graph' -> where root = rgraphroot rgraph; graph = rgraphgraph rgraph -> nodes = nodelist graph [root] -> table = zip2 nodes heap -> move = foldmap id nonew table -> nonew = error "relabel: no new node assigned to node" -> graph' = foldr addnode emptygraph table -> addnode (node,node') -> = updategraph node' (sym,map move args), if def -> = id, otherwise -> where (def,(sym,args)) = nc node -> nc = nodecontents graph -*/ - -relabel :: [var2] (Rgraph sym var1) -> Rgraph sym var2 | == var1 -relabel heap rgraph - = mkrgraph (move root) graph` - where root = rgraphroot rgraph; graph = rgraphgraph rgraph - nodes = varlist graph [root] - table = zip2 nodes heap - move = foldmap id nonew table - nonew = abort "relabel: no new node assigned to node" - graph` = foldr addnode emptygraph table - addnode (node,node`) - | def - = updategraph node` (sym,map move args) - = id - where (def,(sym,args)) = nc node - nc = varcontents graph - -/* -> foldsingleton -> :: (**->*->[**]->***) -> -> *** -> -> rgraph * ** -> -> *** - -> foldsingleton single nosingle rgraph -> = f (nc root) -> where f (True,(sym,args)) = single root sym args, if ~or (map (fst.nc) args) -> f cont = nosingle -> nc = nodecontents graph -> root = rgraphroot rgraph; graph = rgraphgraph rgraph -*/ - -foldsingleton :: - (var sym [var] -> pvar) - pvar - (Rgraph sym var) - -> pvar - | == var - -foldsingleton single nosingle rgraph - = case nc root - of (True,(sym,args)) - | not (or (map (fst o nc) args)) - -> single root sym args - _ - -> nosingle - where nc = varcontents graph - root = rgraphroot rgraph; graph = rgraphgraph rgraph diff --git a/sucl/clean.icl b/sucl/clean.icl deleted file mode 100644 index 6f4964f..0000000 --- a/sucl/clean.icl +++ /dev/null @@ -1,449 +0,0 @@ -implementation module clean - -// $Id$ - -/* - -clean.lit - Clean core language -=============================== - -Description ------------ - -This script contains the implementation of the core of the Clean -language. - ------------------------------------------------------------- - -Interface ---------- - -Exported identifiers: - -> %export || law.lit cli.lit test.lit - -> cleanpart || + + - -> node || + + + -> symbol || + + + -> typenode || + + + -> typesymbol || + + + - -> cleantyperule || - + - -> corecomplete || + + - -> coretypeinfo -> coretyperule || - + - -> readcleanparts || - + - -> showcleanpart -> shownode || - - + -> showsymbol || + + + -> showtypenode || - + - -> showtypesymbol || - + - -> symbolmodule -> typesymbolmodule -> usersym - -> cleanalias -> cleanmacro -> cleantype -> cleanrule - -> heap || Infinite list of anonymous nodes -> typeheap || Infinite list of anonymous type nodes - ------------------------------------------------------------- - -Includes --------- - -> %include "basic.lit" -> %include "hunt.lit" -> %include "graph.lit" -extgraph -> %include "rule.lit" - ------------------------------------------------------------- - -Implementation --------------- - -Implementation of identifier - -> typesymbol -> ::= INT | || Integer -> BOOL | || Boolean -> CHAR | || Character -> STRING | || String -> REAL | || Real -> FILE | || File -> FN | || Function -> LIST | || List -> TUPLE num | || Tuple of specific arity -> USER [char] [char] || User-defined type <module.ident> - -> typenode -> ::= NAMED [char] | || A type node with an explicit nodeid -> ANONYMOUS num || A type node without an explicit nodeid - -> symbol -> ::= Int num | || A specific integer -> Bool bool | || A specific boolean -> Char char | || A specific character -> String [char] | || A specific string -> Real num | || A specific real -> Tuple num | || The tuple constructor of specific arity -> Cons | || The list constructor -> Nil | || The empty list -> Apply | || The curried function application symbol -> If | || The predefined if symbol -> Select num num | || The tuple element selector for tuple arity and element number -> User [char] [char] || A user-defined symbol <module.ident> - -> node -> ::= Named [char] | || A node with an explicit nodeid -> Anonymous num || A node without an explicit nodeid - -> cleanpart -> ::= Typeexport typesymbol | -> Alias typesymbol [typenode] typenode [(typenode,(typesymbol,[typenode]))] | -> Algebra typesymbol [symbol] | -> Export symbol | -> Macro symbol [node] node [(node,(symbol,[node]))] | -> Type symbol [typenode] typenode [(typenode,(typesymbol,[typenode]))] [char] | -> Rules symbol | -> Rule symbol [node] node [(node,(symbol,[node]))] | -> Constructor symbol - -> showcleanpart :: cleanpart -> [char] -> showcleanpart = show - -> ct = printrule show show.coretyperule - -> coreconstructor :: symbol -> bool - -> coreconstructor (Int i) = True -> coreconstructor (Bool b) = True -> coreconstructor (Char c) = True -> coreconstructor (String s) = True -> coreconstructor (Real r) = True -> coreconstructor (Tuple a) = True -> coreconstructor (Cons ) = True -> coreconstructor (Nil ) = True -> coreconstructor (Apply ) = True -> coreconstructor (If ) = False -> coreconstructor (Select a i) = False -> coreconstructor (User m n) = False - -> coreexports :: [symbol] - -> coreexports = [] - -> coreimported :: symbol -> bool - -> coreimported (Int i) = False -> coreimported (Bool b) = False -> coreimported (Char c) = False -> coreimported (String s) = False -> coreimported (Real r) = False -> coreimported (Tuple a) = False -> coreimported (Cons ) = False -> coreimported (Nil ) = False -> coreimported (Apply ) = True -> coreimported (If ) = False -> coreimported (Select a i) = False -> coreimported (User m n) = False - -> corerules :: symbol -> [rule symbol node] - -> corerules (Int i) = [] -> corerules (Bool b) = [] -> corerules (Char c) = [] -> corerules (String s) = [] -> corerules (Real r) = [] -> corerules (Tuple a) = [] -> corerules (Cons ) = [] -> corerules (Nil ) = [] -> corerules (Apply ) = [] -> corerules (If ) -> = [ mkrule [Named "cond",Named "then",Named "else"] (Named "else") (updategraph (Named "cond") (Bool False,[]) emptygraph) -> , mkrule [Named "cond",Named "then",Named "else"] (Named "then") (updategraph (Named "cond") (Bool True ,[]) emptygraph) -> ] -> corerules (Select a i) = [mkrule [Named "tuple"] (Anonymous i) (updategraph (Named "tuple") (Tuple a,map Anonymous [1..a]) emptygraph)] -> corerules (User m n) = [] - - coresymbols :: [symbol] - - coresymbols = [If,Select a i] - -> coretyperule (Int i) = mkrule [] (NAMED "int" ) (updategraph (NAMED "int" ) (INT ,[]) emptygraph) -> coretyperule (Bool b) = mkrule [] (NAMED "bool" ) (updategraph (NAMED "bool" ) (BOOL ,[]) emptygraph) -> coretyperule (Char c) = mkrule [] (NAMED "char" ) (updategraph (NAMED "char" ) (CHAR ,[]) emptygraph) -> coretyperule (String s) = mkrule [] (NAMED "string") (updategraph (NAMED "string") (STRING,[]) emptygraph) -> coretyperule (Real r) = mkrule [] (NAMED "real" ) (updategraph (NAMED "real" ) (REAL ,[]) emptygraph) -> coretyperule (Tuple a) -> = mkrule args (NAMED "tuple") (updategraph (NAMED "tuple") (TUPLE a,args) emptygraph) -> where args = take a (map ANONYMOUS [1..]) -> coretyperule Cons = mkrule [NAMED "element",NAMED "list"] (NAMED "list") (updategraph (NAMED "list") (LIST,[NAMED "element"]) emptygraph) -> coretyperule Nil = mkrule [] (NAMED "list") (updategraph (NAMED "list") (LIST,[NAMED "element"]) emptygraph) -> coretyperule Apply = mkrule [NAMED "fn",NAMED "arg"] (NAMED "res") (updategraph (NAMED "fn") (FN,[NAMED "arg",NAMED "res"]) emptygraph) -> coretyperule If = mkrule [NAMED "bool",NAMED "res",NAMED "res"] (NAMED "res") (updategraph (NAMED "bool") (BOOL,[]) emptygraph) -> coretyperule (Select a i) = mkrule [NAMED "tuple"] (ANONYMOUS i) (updategraph (NAMED "tuple") (TUPLE a,map ANONYMOUS [1..a]) emptygraph) -> coretyperule (User m n) = error ("coretyperule: untyped user symbol "++m++'.':n) - -> coretypeinfo :: symbol -> (rule typesymbol typenode,[bool]) -> coretypeinfo sym -> = (trule,corestricts sym) -> where corestricts Apply = [True,False] -> corestricts If = [True,False,False] -> corestricts (Select a i) = [True] -> corestricts sym = map (const False) (lhs trule) -> trule = coretyperule sym - -> readcleanparts :: [char] -> [cleanpart] -> readcleanparts = readvals.findclean - -> findclean :: [char] -> [char] -> findclean base -> = foldr const (error ("findclean: "++show base++" not found.")) files -> where files = findfiles readable ["",".cli"] (getpath ["."] "CLIPATH") base - -> corecomplete :: typesymbol -> [symbol] -> bool - -> corecomplete INT = const False -> corecomplete BOOL = superset (map Bool [False,True]) -> corecomplete CHAR = superset (map (Char.decode) [0..255]) -> corecomplete STRING = const False -> corecomplete REAL = const False -> corecomplete FILE = const False -> corecomplete FN = const False -> corecomplete LIST = superset [Nil,Cons] -> corecomplete (TUPLE arity) = superset [Tuple arity] -> corecomplete (USER module identifier) = const False - -> showtypesymbol INT = "INT" -> showtypesymbol BOOL = "BOOL" -> showtypesymbol CHAR = "CHAR" -> showtypesymbol STRING = "STRING" -> showtypesymbol REAL = "REAL" -> showtypesymbol FILE = "FILE" -> showtypesymbol FN = "=>" -> showtypesymbol LIST = "_LIST" -> showtypesymbol (TUPLE a) = "_TUPLE"++shownum a -> showtypesymbol (USER module ident) = ident - -> showtypenode (NAMED ident) = ident -> showtypenode (ANONYMOUS n) = "type"++shownum n - -> showtypenodedef :: typesymbol -> [([char],[char])] -> ([char],[char]) -> showtypenodedef (TUPLE a) [] = issafe "()" -> showtypenodedef (TUPLE a) [arg] = arg -> showtypenodedef (TUPLE a) ((safearg,unsafearg):args) -> = issafe ('(':unsafearg++f args) -> where f [] = ")" -> f ((safearg,unsafearg):args) = ',':unsafearg++f args -> showtypenodedef LIST [(safearg,unsafearg)] = issafe ('[':unsafearg++"]") -> showtypenodedef symbol [] = issafe (showtypesymbol symbol) -> showtypenodedef symbol args = showappl (showtypesymbol symbol) args - -> showsymbol :: symbol -> [char] -> showsymbol (Int i) = shownum i -> showsymbol (Bool False) = "FALSE" -> showsymbol (Bool True) = "TRUE" -> showsymbol (Char c) = show c -> showsymbol (String s) = show s -> showsymbol (Real r) = show (r+0.0) -> showsymbol (Tuple a) = "_Tuple"++show a -> showsymbol Cons = "_CONS" -> showsymbol Nil = "[]" -> showsymbol Apply = "_AP" -> showsymbol If = "IF" -> showsymbol (Select a i) = "_Select"++show a++'.':show i -> showsymbol (User module ident) = ident - -> shownode (Named ident) = ident -> shownode (Anonymous n) = "node"++shownum n - -> shownodedef :: symbol -> [([char],[char])] -> ([char],[char]) -> shownodedef (Tuple a) [] = issafe "()" -> shownodedef (Tuple a) [arg] = arg -> shownodedef (Tuple a) ((safearg,unsafearg):args) -> = issafe ('(':unsafearg++f args) -> where f [] = ")" -> f ((safearg,unsafearg):args) = ',':unsafearg++f args -> shownodedef Cons [(safehead,unsafehead),(safetail,unsafetail)] -> = issafe ('[':unsafehead++f unsafetail) -> where f "[]" = "]" -> f ('[':ttail) = ',':ttail -> f unsafetail = '|':unsafetail++"]" -> shownodedef Apply [fn] = fn -> shownodedef Apply ((safefn,unsafefn):args) = showappl unsafefn args -> shownodedef symbol [] = issafe (showsymbol symbol) -> shownodedef symbol args = showappl (showsymbol symbol) args - -> showappl sym args = mksafe (sym++concat (map ((' ':).fst) args)) -> mksafe unsafe = ('(':unsafe++")",unsafe) -> issafe safe = (safe,safe) - -> cleantyperule :: symbol -> (rule typesymbol typenode,[bool]) -> [char] - -> cleantyperule sym (trule,tstricts) -> = ":: "++showsymbol sym++concat (map2 printarg tstricts targs)++" -> "++snd (lookup' troot)++";" -> where targs = lhs trule; troot = rhs trule; tgraph = rulegraph trule -> lookup' = lookup table -> table = map (pairwith printunraveled) (nodelist tgraph (troot:targs)) -> printunraveled tnode -> = showtypenodedef tsym (map lookup' targs), if tdef -> = issafe (showtypenode tnode), otherwise -> where (tdef,(tsym,targs)) = nodecontents tgraph tnode -> printarg tstrict targ = ' ':cond tstrict ('!':) id (fst (lookup' targ)) - -> prettyrule :: (**->[char]) -> (*->[([char],[char])]->([char],[char])) -> rule * ** -> [char] -> prettyrule shownode shownodedef rule -> = concat (map ((++" ").fst) (init shownnodes))++"-> "++snd (last shownnodes) -> where shownnodes = foldgraph prettydef (issafe.shownode) shownodedef graph (args++[root]) -> prettydef node (saferef,unsaferef) = issafe (shownode node++':':saferef) -> graph = rulegraph rule -> args = lhs rule -> root = rhs rule - -> usersym :: symbol -> bool -> usersym (User module name) = True -> usersym sym = False - -> symbolmodule :: symbol -> optional [char] -> symbolmodule (User module ident) = Present module -> symbolmodule symbol = Absent - -> typesymbolmodule :: typesymbol -> optional [char] -> typesymbolmodule (USER module ident) = Present module -> typesymbolmodule symbol = Absent - -======================================================================== - -Get the Select nodes from a graph. - -> getselectnodes :: graph symbol ** -> ** -> [((**,num),(num,**))] - -> getselectnodes graph root -> = foldr (withmeta (nodecontents graph) addselectnode) [] (nodelist graph [root]) -> where addselectnode (True,(Select arity index,[tuplenode])) selectnode -> = (((tuplenode,arity),(index,selectnode)):) -> addselectnode contents node = id - -Distribute the Select nodes over their indexes. - -> splitselectnodes :: ((**,num),[(num,**)]) -> (**,[[**]]) - -> splitselectnodes ((tuplenode,arity),selects) -> = (tuplenode,foldr dist (rep arity []) selects) -> where dist (1,selectnode) (ns:nss) = (selectnode:ns):nss -> dist (index,selectnode) (ns:nss) = ns:dist (index-1,selectnode) nss - -Make left hand sides. - -> makelhss :: [**] -> [[**]] -> ([**],[[**]]) - -> makelhss heap nss -> = (heap,[]), if empty -> = (heap'',ns':nss''), otherwise -> where (heap'',nss'') = makelhss heap' nss' -> (empty,ns',heap',nss') = heads heap nss -> heads heap [] = (True,[],heap,[]) -> heads (node:heap) ([]:nss) -> = (empty,node:ns',heap',[]:nss') -> where (empty,ns',heap',nss') = heads heap nss -> heads heap ((n:ns):nss) -> = (False,n:ns',heap',ns:nss') -> where (empty,ns',heap',nss') = heads heap nss - -> maketuplenodedefs :: [**] -> [(**,[[**]])] -> [([**],**)] - -> maketuplenodedefs heap [] -> = [] -> maketuplenodedefs heap ((tuplenode,nss):rest) -> = map (converse pair tuplenode) lhss++tuplenodedefs -> where (heap',lhss) = makelhss heap nss -> tuplenodedefs = maketuplenodedefs heap' rest - -> printtree :: graph symbol node -> node -> ([char],[char]) -> printtree = unravelwith (issafe.shownode) shownodedef - -> cleanalias sym = indent ":: ".totalpretty typeheap (const (const [])) showtypesymbol showtypenodedef showtypenode sym -> cleanmacro sym = indent " ".totalpretty heap (const (const [])) showsymbol shownodedef shownode sym -> cleantype sym = indent ":: ".totalpretty typeheap (const (const [])) showsymbol showtypenodedef showtypenode sym -> cleanrule sym = indent " ".totalpretty heap getselectnodes showsymbol shownodedef shownode sym - -> heap = map Anonymous [0..] -> typeheap = map ANONYMOUS [0..] - -> totalpretty -> :: [***] -> -> (graph ** ***->***->[((***,num),(num,***))]) -> -> (*->[char]) -> -> (**->[([char],[char])]->([char],[char])) -> -> (***->[char]) -> -> * -> -> rule ** *** -> -> [[char]] - -> totalpretty heap getselectnodes showlhssymbol shownodedef shownode lhssymbol rule -> = punctuate "" "," " " "" lhsheader lhsbody++ -> punctuate "-> " "," " " ";" rhsheader rhsbody - -> where - -> args = lhs rule; root = rhs rule; graph = rulegraph rule -> selectnodes = getselectnodes graph root -> prunedgraph = foldr prunegraph graph (map (snd.snd) selectnodes) -> tuplenodedefs -> = ( maketuplenodedefs (heap--nodelist graph (root:args)). -> map splitselectnodes. -> partition fst snd -> ) selectnodes -> tuplenodes = map snd tuplenodedefs -> count = refcount prunedgraph (args++root:tuplenodes) -> sharednodes = [node|node<-nodelist prunedgraph (args++root:tuplenodes);count node>1;fst (nodecontents prunedgraph node)] -> reprunedgraph = foldr prunegraph prunedgraph sharednodes -> (argreprs:[rootrepr]:tuplereprs:sharedargreprs) -> = map (map (unravelwith (issafe.shownode) shownodedef reprunedgraph)) (args:[root]:tuplenodes:map (snd.snd.nodecontents prunedgraph) sharednodes) - -> showtupledef (selectnodes,tuplenode) tuplerepr -> = '(':join ',' (map shownode selectnodes)++"): "++snd tuplerepr -> showshareddef (node,argreprs) -> = mapfst addline, if patnode node -> = mapsnd addline, otherwise -> where addline = ((shownode node++": "++snd (shownodedef (fst cont) argreprs)):) -> (True,cont) = nodecontents prunedgraph node - -> patnode = member (nodelist graph args) - -> lhsheader = showlhssymbol lhssymbol++concat (map ((' ':).fst) argreprs) -> rhsheader = snd rootrepr -> (lhslines,rhslines) = foldr showshareddef ([],[]) (zip2 sharednodes sharedargreprs) -> lhsbody = lhslines -> rhsbody = map2 showtupledef tuplenodedefs tuplereprs++rhslines - -> punctuate :: [char] -> [char] -> [char] -> [char] -> [char] -> [[char]] -> [[char]] - -> punctuate open endline beginline close l ls -> = (open++l++end):ls' -> where (end,ls') = f ls -> f [] = (close,[]) -> f (l:ls) = (endline,punctuate beginline endline beginline close l ls) - ------------------------------------------------------------------------- -Useful (higher order) functions. - -> withmeta :: (*->**) -> (**->*->***) -> * -> *** -> withmeta meta f x = f (meta x) x - -> pair :: * -> ** -> (*,**) -> pair x y = (x,y) - -> unravelwith :: (**->***) -> (*->[***]->***) -> graph * ** -> ** -> *** -> unravelwith foldopen foldclosed graph -> = unravel -> where unravel node -> = foldclosed sym (map unravel args), if def -> = foldopen node, otherwise -> where (def,(sym,args)) = nodecontents graph node - -*/ diff --git a/sucl/cli.icl b/sucl/cli.icl deleted file mode 100644 index 9ced531..0000000 --- a/sucl/cli.icl +++ /dev/null @@ -1,363 +0,0 @@ -implementation module cli - -// $Id$ - -import law -import coreclean -import strat -import absmodule -import rule -import dnc -import basic -from syntax import SK_Function -import general -import StdEnv - -/* - -cli.lit - Clean implementation modules -====================================== - -Description ------------ - -This script implements Clean modules (type module) and partial Clean -programs (type cli), which are essentially sets of Clean modules. - ------------------------------------------------------------- - -Interface ---------- - -Exported identifiers: - -> %export -> cli -> readcli -> loadclis -> exports -> typerule -> imports -> clistrategy -> constrs -> complete -> showcli -> printcli -> aliases -> macros -> stripexports - -> printalgebra - -Required types: - - identifier - type@source.lit type@source.lit - ... - ------------------------------------------------------------- - -Includes --------- - -> %include "dnc.lit" - -> %include "../src/basic.lit" -> %include "../src/pfun.lit" -> %include "../src/graph.lit" -> %include "../src/rule.lit" -> %include "../src/spine.lit" -> %include "strat.lit" -> %include "law.lit" -> %include "../src/clean.lit" -> %include "../src/module.lit" - - ------------------------------------------------------------- - -Implementation --------------- - -Implementation of identifier - - identifier - :: type - - identifierone arguments - = body - -... - ------------------------------------------------------------------------- - -Abstype implementation. - -> abstype cli -> with readcli :: [char] -> cli -> loadclis :: [[char]] -> cli -> exports :: cli -> [symbol] -> typerule :: cli -> symbol -> rule typesymbol typenode -> rules :: cli -> symbol -> optional [rule symbol node] -> imports :: cli -> [symbol] -> clistrategy :: cli -> (graph symbol node->node->**->bool) -> strategy symbol ** node **** -> constrs :: cli -> [(typesymbol,[symbol])] -> complete :: cli -> [symbol] -> bool -> showcli :: cli -> [char] -> aliases :: cli -> [(typesymbol,rule typesymbol typenode)] -> macros :: cli -> [(symbol,rule symbol node)] -> stripexports :: [char] -> cli -> cli -*/ - -:: Cli = CliAlias (SuclSymbol->String) (Module SuclSymbol SuclVariable SuclTypeSymbol SuclTypeVariable) - -/* -> cli == module symbol node typesymbol typenode - -> readcli = compilecli.readcleanparts - -> loadclis -> = compilecli.concat.map readcleanparts - -> stripexports main (tdefs,(es,as,ts,rs)) = (tdefs,([User m i|User m i<-es;m=main],as,ts,rs)) - -> exports (tdefs,(es,as,ts,rs)) = es -*/ - -exports :: Cli -> [SuclSymbol] -exports (CliAlias ss m) = m.exportedsymbols - -// Determine the arity of a core clean symbol -arity :: Cli SuclSymbol -> Int -arity (CliAlias ss m) sym -= extendfn m.arities (length o arguments o (extendfn m.typerules (coretyperule--->"coreclean.coretyperule begins from cli.arity"))) sym - -/* -> typerule (tdefs,(es,as,ts,rs)) = maxtyperule ts -*/ - -typerule :: Cli SuclSymbol -> Rule SuclTypeSymbol SuclTypeVariable -typerule (CliAlias ss m) sym -= maxtyperule m.typerules sym - -/* -> rules (tdefs,(es,as,ts,rs)) = foldmap Present Absent rs - -> imports (tdefs,(es,as,ts,rs)) = [sym|(sym,tdef)<-ts;~member (map fst rs) sym] - -> aliases ((tes,tas,tcs),defs) = tas -> macros (tdefs,(es,as,ts,rs)) = as - -> clistrategy ((tes,tas,tcs),(es,as,ts,rs)) matchable -> = ( checktype (maxtypeinfo ts). || Checks curried occurrences and strict arguments -> checklaws cleanlaws. || Checks for special (hard coded) rules (+x0=x /y1=y ...) -> checkrules matchable (foldmap id [] rs). -> || Checks normal rewrite rules -> checkimport islocal. || Checks for delta symbols -> checkconstr (member (concat (map snd tcs))) -> || Checks for constructors -> ) (corestrategy matchable) || Checks rules for symbols in the language core (IF, _AP, ...) -> where islocal (User m i) = member (map fst rs) (User m i) -> islocal rsym = True || Symbols in the language core are always completely known -*/ - -clistrategy :: Cli ((Graph SuclSymbol SuclVariable) SuclVariable var -> Bool) -> Strategy SuclSymbol var SuclVariable answer | == var -clistrategy (CliAlias showsymbol {arities=as,typeconstructors=tcs,typerules=ts,rules=rs}) matchable - = ( checkarity getarity // Checks curried occurrences and strict arguments - o checklaws cleanlaws // Checks for special (hard coded) rules (+x0=x /y1=y ...) - o checkrules matchable (foldmap id [] rs) // Checks normal rewrite rules - o checkimport islocal // Checks for delta symbols - o ( checkconstr toString (flip isMember (flatten (map snd tcs))) // Checks for constructors - ---> ("cli.clistrategy.checkconstr",tcs) - ) - ) (corestrategy matchable) // Checks rules for symbols in the language core (IF, _AP, ...) - where islocal rsym=:(SuclUser (SK_Function _)) = isMember rsym (map fst rs) // User-defined function symbols can be imported, so they're known if we have a list of rules for them - islocal _ = True // Symbols in the language core (the rest) are always completely known - // This includes lifted case symbols; we lifted them ourselves, after all - getarity sym - = (arity <--- ("cli.clistrategy.getarity ends with "+++toString arity)) ---> ("cli.clistrategy.getarity begins for "+++showsymbol sym) - where arity = extendfn as (typearity o (maxtyperule--->"cli.clistrategy.getarity uses maxtyperule") ts) sym - -typearity :: (Rule SuclTypeSymbol SuclTypeVariable) -> Int -typearity ti = length (arguments ti) - -//maxtypeinfo :: [(SuclSymbol,(Rule SuclTypeSymbol SuclTypeVariable,[Bool]))] SuclSymbol -> (Rule SuclTypeSymbol SuclTypeVariable,[Bool]) -//maxtypeinfo defs sym = extendfn defs coretypeinfo sym - -maxtyperule :: [(SuclSymbol,Rule SuclTypeSymbol SuclTypeVariable)] SuclSymbol -> Rule SuclTypeSymbol SuclTypeVariable -maxtyperule defs sym = extendfn defs (coretyperule--->"cli.coretyperule begins from cli.maxtyperule") sym - -maxstricts :: [(SuclSymbol,[Bool])] SuclSymbol -> [Bool] -maxstricts defs sym = extendfn defs corestricts sym - -/* -> constrs ((tes,tas,tcs),defs) = tcs - -> complete ((tes,tas,tcs),(es,as,ts,rs)) = mkclicomplete tcs (fst.maxtypeinfo ts) -*/ - -complete :: Cli -> [SuclSymbol] -> Bool -complete (CliAlias ss m) = mkclicomplete m.typeconstructors (maxtyperule m.typerules) - -/* -> showcli = printcli - -> mkclicomplete -> :: [(typesymbol,[symbol])] -> -> (symbol->rule typesymbol *****) -> -> [symbol] -> -> bool - -> mkclicomplete tcs typerule [] = False -> mkclicomplete tcs typerule syms -> = False, if ~tdef -> = foldmap superset (corecomplete tsym) tcs tsym syms, otherwise -> where trule = typerule (hd syms) -> (tdef,(tsym,targs)) = dnc (const "in mkclicomplete") (rulegraph trule) (rhs trule) -*/ - -mkclicomplete :: - [(SuclTypeSymbol,[SuclSymbol])] - (SuclSymbol->Rule SuclTypeSymbol tvar) - [SuclSymbol] - -> Bool - | == tvar - -mkclicomplete tcs typerule [] = False -mkclicomplete tcs typerule syms -| not tdef - = False -= foldmap superset (corecomplete tsym) tcs tsym syms - where trule = typerule (hd syms) - (tdef,(tsym,_)) = dnc (const "in mkclicomplete") (rulegraph trule) (ruleroot trule) - -/* ------------------------------------------------------------------------- - -> printcli :: module symbol node typesymbol typenode -> [char] -> printcli ((tes,tas,tcs),(es,as,ts,rs)) -> = lay -> ( (implementation++"MODULE "++thismodule++";"): -> "": -> "<< EXPORT": -> map cleandef es++ -> ">>": -> "": -> map showimport (partition fst snd (itypesyms++isyms))++ -> concat (map cleanalg tcs)++ -> concat (map cleanimp [(sym,plookup showsymbol ts sym,rules)|(sym,rules)<-rs;usersym sym]) -> ) -> where cleandef sym = " "++cleantyperule sym (maxtypeinfo ts sym) -> cleanalg constr -> = ["","TYPE",printalgebra (fst.maxtypeinfo ts) constr], if typesymbolmodule (fst constr)=Present thismodule -> = [], otherwise -> cleanimp (sym,tinfo,rules) -> = prepend (trulelines++concat (map (cleanrule sym) rules)) -> where trulelines -> = [], if member (concat (map snd tcs)) sym -> = [cleantyperule sym tinfo], otherwise -> prepend [] = [] -> prepend lines = "":"RULE":lines -> implementation -> = "", if showsymbol (hd es)="Start" -> = "IMPLEMENTATION ", otherwise -> isyms = [(module,ident)|((User module ident),tinfo)<-ts;~member (map fst rs) (User module ident)] -> itypesyms -> = foldr add [] tcs -> where add (USER module ident,constrs) rest -> = (module,ident):foldr addc rest constrs, if module~=thismodule -> add typesymbol = id -> addc (User module ident) rest -> = (module,ident):rest -> addc symbol = id -> thismodule = foldoptional undef id (symbolmodule (hd es)) - -> showimport :: ([char],[[char]]) -> [char] -> showimport (module,idents) = "FROM "++module++" IMPORT "++join ',' idents++";" - -> printalgebra :: (symbol->rule typesymbol typenode) -> (typesymbol,[symbol]) -> [char] -> printalgebra typerule (tsym,syms) -> = ":: "++ -> showtypesymbol tsym++ -> concat (map ((' ':).showtypenode) trargs)++ -> concat (map2 (++) (" -> ":repeat " | ") alts)++ -> ";" -> where symtrules = map (pairwith typerule) syms -> trule = snd (hd symtrules) -> trroot = rhs trule -> (trdef,trcont) = dnc (const "in printalgebra") (rulegraph trule) trroot -> (trsym,trargs) -> = trcont, if trdef -> = (notrsym,notrargs), otherwise -> notrsym = error ("printalgebra: no type symbol for typenode "++showtypenode trroot) -> notrargs = error ("printalgebra: no type arguments for typenode "++showtypenode trroot) -> alts = map (printalt trargs) symtrules - -> printalt :: [typenode] -> (symbol,rule typesymbol typenode) -> [char] -> printalt trargs' (sym,trule) -> = showsymbol sym++concat (map (' ':) (printgraph showtypesymbol showtypenode tgraph' targs')) -> where targs = lhs trule; troot = rhs trule; tgraph = rulegraph trule -> (trdef,(trsym,trargs)) = dnc (const "in printalt") tgraph troot -> tnodes = trargs++(nodelist tgraph targs--trargs) -> tnodes' = trargs'++(typeheap--trargs') -> redirection = foldr (uncurry adjust) noredir (zip2 tnodes tnodes') -> noredir tnode = error ("printalt: no redirection for typenode "++showtypenode tnode) -> targs' = map redirection targs -> tgraph' = movegraph redirection tnodes tgraph - -Compiling clean parts into module information... - -> compilecli -> :: [cleanpart] -> -> module symbol node typesymbol typenode - -> compilecli parts -> = ((typeexports,aliases,typedefs),(exports,macros,typerules,locals)) -> where typeexports = [tsym|Typeexport tsym<-parts] -> aliases = [(tsym,compilerule targs troot tnodedefs)|Alias tsym targs troot tnodedefs<-parts] -> typedefs = [(tsym,syms)|Algebra tsym syms<-parts] -> exports = [sym|Export sym<-parts] -> macros = [(sym,compilerule args root nodedefs)|Macro sym args root nodedefs<-parts] -> typerules = [(sym,(compilerule targs troot tnodedefs,map (='!') stricts))|Type sym targs troot tnodedefs stricts<-parts] -> locals = [(sym,rules sym)|Rules sym<-parts] -> rules lsym = [compilerule args root nodedefs|Rule sym args root nodedefs<-parts;sym=lsym] - -> currytrule :: **** -> [*****] -> rule **** ***** -> rule **** ***** -> currytrule fn theap trule -> = mkrule ctargs ctroot ctgraph -> where targs = lhs trule; troot = rhs trule; tgraph = rulegraph trule -> ctargs = init targs -> ctroot = hd (theap--nodelist tgraph (troot:targs)) -> ctgraph = updategraph ctroot (fn,[last targs,troot]) tgraph - -*/ - -mkcli :: - (SuclSymbol->String) - [(SuclSymbol,Rule SuclTypeSymbol SuclTypeVariable)] - [(SuclSymbol,[Bool])] - [SuclSymbol] - [(SuclSymbol,Int)] - [(SuclTypeSymbol,[(SuclSymbol,(Rule SuclTypeSymbol SuclTypeVariable,[Bool]))])] - [(SuclSymbol,(Int,[Rule SuclSymbol SuclVariable]))] - -> Cli - -mkcli showsymbol typerules stricts exports imports constrs bodies -= CliAlias - showsymbol - { arities = map (mapsnd fst) bodies++imports - , typeconstructors = map (mapsnd (map fst)) constrs - , exportedsymbols = exports - , 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 - } - -instance <<< Cli -where (<<<) file (CliAlias showsymbol m) - # file = file <<< "=== Arities ===" <<< nl - # file = printlist (showpair showsymbol toString) "" m.arities file - # file = file <<< "=== Type Rules ===" <<< nl - # file = printlist (showpair showsymbol toString) "" m.typerules file - # file = file <<< "=== Rules ===" <<< nl - # file = printlist (showpair showsymbol (showlist showrule`)) "" m.rules file - = file - where showrule` rule = showruleanch showsymbol toString (map (const False) (arguments rule)) rule [] diff --git a/sucl/complete.dcl b/sucl/complete.dcl deleted file mode 100644 index 365deeb..0000000 --- a/sucl/complete.dcl +++ /dev/null @@ -1,19 +0,0 @@ -definition module complete - -// $Id$ - -from graph import Graph -from StdOverloaded import == - -:: Pattern sym var - :== (Graph sym var,[var]) - -coveredby - :: ([sym]->Bool) - (Graph sym var) - ![Pattern sym pvar] - [var] - -> Bool - | == sym - & == var - & == pvar diff --git a/sucl/complete.icl b/sucl/complete.icl deleted file mode 100644 index 136db40..0000000 --- a/sucl/complete.icl +++ /dev/null @@ -1,148 +0,0 @@ -implementation module complete - -// $Id$ - -import graph -import basic -import StdEnv - -/* - -To check completeness of patterns, we need to know whether, given a list -of (constructor) symbols, this list completely covers a type. - - complete :: [sym] -> Bool - -It is assumed that a type can never be empty, so an empty list of -constructors can never cover a type. Otherwise, separate type -information would be needed to determine the completeness of an empty -list of constructors. - - -The algorithm uses /multipatterns/, which are lists of simple patterns. A -multipattern is used to match at multiple node-ids in a graph in parallel. -This is necessary in the case of matching of product types. - -*/ - -:: Pattern sym var - :== (Graph sym var,[var]) - -/* - -Coveredby checks whether a multipattern is covered by a list of -multipatterns. There are five cases to consider. - - First, if the multipattern is not the empty list, then to cover it - some multipattern must exist, so if the list of multipatterns is - empty, then the multipattern is not covered. - - Second, if the multipattern is the empty list, it is trivially - covered by any list of multipatterns, including the empty. - - Third, if the first pattern of the multipattern is closed, we select - only the multipatterns that it can match, then continue with the - arguments, and then the rest of the multipattern. - - Fourth, if the first pattern of the multipattern is open, and all - its type constructors are present in the first patterns of the - multipatterns in the list of multipatterns, then the first pattern - of the multipattern is split according to all constructors, and all - possibilities must be covered. - - Fifth, if not all constructors are present, then the multipatterns - of which the first pattern is open must cover the multipattern. So - those are selected and we continue with the tails of the - multipatterns in this list. - -To understand the order of the first two cases, check how a single open -integer pattern is covered by a list of integer patterns either -containing or not containing an open pattern. - -*/ - -coveredby - :: ([sym]->Bool) - (Graph sym var) - ![Pattern sym pvar] - [var] - -> Bool - | == sym - & == var - & == pvar - -coveredby complete subject [] svars = False -coveredby complete subject pvarss [] = True -coveredby complete subject pvarss [svar:svars] -| sdef -= coveredby complete subject tmpvalue (sargs++svars) -| complete (map fst3 closeds) -= and (map covered closeds) -= coveredby complete subject opens 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 - -/* - -Split splits a list of multipatterns into parts; on one hand, those of -which the first pattern is open, and on the other hand, for every -constructor, the list of applicable multipatterns, in which case the -multipatterns with an open pattern are expanded and added as well. - -*/ - -psplit - :: [Pattern sym var] - -> ( [Pattern sym var] - , [ ( sym - , var->[var] - , [Pattern sym var] - ) - ] - ) - | == sym - & == var - -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`) = psplit svarss - add (sym,repvar,svarss`) = (sym,repvar,[(subject,repvar svar++svars):svarss`]) - (opens,closeds) = psplit outs - (ins,outs) = foldr (spl repvar ssym) ([],[]) svarss - repvar svar = map (const svar) sargs - (sdef,(ssym,sargs)) = varcontents subject svar - -/* - -Spl, given a symbol, derives two lists of multipatterns from one. The -first are the multipatterns of which the first pattern can match the -symbol, i.e. open ones and closed ones with the correct symbol. The -second are the multipatterns that can match other symbols, i.e. also -open ones, and closed ones with the wrong symbol. - -*/ - -spl - :: (var -> [var]) - sym - (Pattern sym var) - ([Pattern sym var],[Pattern sym var]) - -> ([Pattern sym var],[Pattern sym var]) - | == sym - & == var - -spl repvar sym (subject,[svar:svars]) (ins,outs) -| not sdef -= ([(subject,repvar svar++svars):ins],[(subject,[svar:svars]):outs]) -| ssym==sym -= ([(subject,sargs++svars):ins],outs) -= (ins,[(subject,[svar:svars]):outs]) - where (sdef,(ssym,sargs)) = varcontents subject svar diff --git a/sucl/dnc.dcl b/sucl/dnc.dcl deleted file mode 100644 index 2b262b6..0000000 --- a/sucl/dnc.dcl +++ /dev/null @@ -1,11 +0,0 @@ -definition module dnc - -// $Id$ - -from graph import Graph,Node -from cleanversion import String -from StdOverloaded import == - -// dnc is like varcontents, but can give a more reasonable error message -// when the contents is used when undefined. -dnc :: (var->.String) !.(Graph sym var) var -> (.Bool,Node sym var) | == var diff --git a/sucl/dnc.icl b/sucl/dnc.icl deleted file mode 100644 index 1c7e08c..0000000 --- a/sucl/dnc.icl +++ /dev/null @@ -1,16 +0,0 @@ -implementation module dnc - -// $Id$ - -import graph -import basic -import StdEnv - -// dnc is like varcontents, but can give a more reasonable error message -// when the contents is used when undefined. -dnc :: (var->.String) !.(Graph sym var) var -> (.Bool,Node sym var) | == var -dnc makemessage graph var -| fst vc = vc - = (False,(wrong "symbol",wrong "arguments")) - where vc = varcontents graph var - wrong element = abort ("getting "+++element+++" of free variable: "+++makemessage var) diff --git a/sucl/extract.icl b/sucl/extract.icl deleted file mode 100644 index 57cef81..0000000 --- a/sucl/extract.icl +++ /dev/null @@ -1,196 +0,0 @@ -implementation module extract - -// $Id$ - -import rule -import dnc -import graph -import basic -from general import Yes,No -import StdEnv - -/* - -extract.lit - Folding of subject graphs -======================================= - -Description ------------ - -This module defines functions that can fold subject graphs, as they are -usually found at the tips of the trace of a symbolic reduction process. - -Three versions are provided; `actualfold' for folding initiated by -autorecursion, `splitrule' for folding initiated by introduced recursion -and `finishfold' for folding initiated without recursion. - ------------------------------------------------------------- - -Interface ---------- - -Exported identifiers: - -> %export -> actualfold || Fold subject graph according to autorecursion -> splitrule || Fold subject graph according to introduced recursion -> finishfold || Finish folding by introducing areas - ------------------------------------------------------------- - -Includes --------- - -> %include "dnc.lit" - -> %include "../src/basic.lit" -> %include "../src/pfun.lit" -> %include "../src/graph.lit" -> %include "../src/rule.lit" - ------------------------------------------------------------- - -Implementation --------------- - -`Actualfold foldarea foldcont hist rule' is the result of -folding occurrences of areas in `hist' to `foldcont', and introducing new -areas for parts that aren't folded. - -`Self' determines whether an instance of a history graph is the history -graph itself. We don't want to fold back something we unfolded earlier! -*/ - -actualfold :: - [var] - [var] - ((Rgraph sym var)->Node sym var) - (pvar->var->bool) - (sym,[pvar]) - [(pvar,Graph sym pvar)] - (Rule sym var) - -> Optional (Rule sym var,[Rgraph sym var]) - | == sym - & == var - & == pvar - -actualfold deltanodes rnfnodes foldarea self foldcont hist rule -| isEmpty list3 - = No -= Yes (mkrule rargs rroot rgraph``,areas`) - where rargs = arguments rule; rroot = ruleroot rule; rgraph = rulegraph rule - - 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] - // list3: list combining every instantiable node with first instantiable history graph - - rgraph` - = foldr foldrec rgraph list3 - where foldrec (rnode,mapping) = updategraph rnode (mapsnd (map (lookup mapping)) foldcont) - - (rgraph``,areas`) = finishfold foldarea fixednodes singlenodes rroot rgraph` - fixednodes = intersect (removeDup (argnodes++foldednodes++rnfnodes)) (varlist rgraph` [rroot]) - singlenodes = intersect deltanodes (varlist rgraph` [rroot]) - argnodes = varlist rgraph` rargs - foldednodes = map fst list3 - -findoccs :: - [(pvar,Graph sym pvar)] - (Rule sym var) - var - -> [[(pvar,var)]] - | == sym - & == var - & == pvar - -findoccs hist rule rnode -= [ mapping - \\ ((hroot,hgraph),(seen,mapping,[]))<-list1 // Find instantiable history rgraphs... - | unshared rnode (hroot,hgraph) mapping // ...which don't have shared contents - ] - where rargs = arguments rule; rroot = ruleroot rule; rgraph = rulegraph rule - list1 - = [((hroot,hgraph),inst (hroot,hgraph))\\(hroot,hgraph)<-hist] - where inst (hroot,hgraph) - = instantiate (hgraph,rgraph) (hroot,rnode) ([],[],[]) - // list1: all instantiation attempts at rnode with the history rgraphs - - unshared rnode (hroot,hgraph) mapping - = disjoint inner outer - where inner = map (lookup mapping) (fst (graphvars hgraph [hroot])) - outer = varlist (prunegraph rnode rgraph) [rroot:rargs]--[rnode] - -/* ------------------------------------------------------------------------- - - -Splitting a rule into areas to fold to a certain area -*/ - -splitrule :: - ((Rgraph sym var)->Node sym var) - [var] - [var] - (Rule sym var) - (Rgraph sym var) - -> (Rule sym var,[Rgraph sym var]) - | == var - -splitrule fold rnfnodes deltanodes rule area -= (mkrule rargs rroot rgraph``,[area`:areas]) - where rargs = arguments rule; rroot = ruleroot rule; rgraph = rulegraph rule - aroot = rgraphroot area; agraph = rgraphgraph area - - (rgraph``,areas) = finishfold fold fixednodes deltanodes rroot rgraph` - fixednodes = intersect (removeDup [aroot:varlist rgraph` rargs++rnfnodes]) (varlist rgraph` [rroot]) - rgraph` = updategraph aroot (fold area`) rgraph - area` = mkrgraph aroot agraph` - agraph` = foldr addnode emptygraph ins - 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)) - -/* ------------------------------------------------------------- - - -`Finishfold foldarea fixednodes root graph' finishes folding of a graph -by introducing areas for parts of the graph that are not fixed in some -way (e.g. when part of the pattern of the rule, already folded, or -bearing a delta function symbol). -*/ - -finishfold :: - ((Rgraph sym var)->Node sym var) - [var] - [var] - var - (Graph sym var) - -> (Graph sym var,[Rgraph sym var]) - | == var - -finishfold foldarea fixednodes singlenodes root graph -= (graph`,areas) - where graph` = foldr foldarea` graph areas - foldarea` area = updategraph (rgraphroot area) (foldarea area) - areas = depthfirst generate process arearoots - process aroot - = mkrgraph aroot (foldr addnode emptygraph ins) - where outs_and_aroot = varlist (prunegraph aroot graph) arearoots++fixednodes - ins = [aroot:varlist graph [aroot]--outs_and_aroot] - generate area - = snd (graphvars agraph [aroot])--fixednodes - where aroot = rgraphroot area; agraph = rgraphgraph area - arearoots = removeDup [root:singlenodes++singfixargs]--fixednodes - singfixargs = flatten (map arguments (singlenodes++fixednodes)) - - arguments node - = if def args [] - where (def,(_,args)) = dnc (const "in finishfold/1") graph node - - addnode node - = if def (updategraph node cnt) id - where (def,cnt) = dnc (const "in finishfold/2") graph node diff --git a/sucl/graph.dcl b/sucl/graph.dcl deleted file mode 100644 index a00a5f0..0000000 --- a/sucl/graph.dcl +++ /dev/null @@ -1,235 +0,0 @@ -definition module graph - -// $Id$ - -from pfun import Pfun -from StdOverloaded import == -from cleanversion import String -from StdString import toString - -// A rule associating a replacement with a pattern -//:: Rule sym var - -// A mapping from variables to nodes (unrooted) -:: Graph sym var - -// A node, bearing the contents of a variable -:: Node sym var - :== (sym,[var]) - -/* - -graph.lit - Unrooted graphs -=========================== - -Description ------------ - -This script implements an abstract type for unrooted graphs and useful -functions to manipulate them. - ------------------------------------------------------------- - -Interface ---------- - -Exported identifiers: - -> %export -> compilegraph || Compile graph from list of node definitions -> emptygraph || The empty unrooted graph -> extgraph || Extend a graph with the image of a matching -> foldgraph || Fold up a graph -> graph || Unrooted graphs over functorspace * and nodespace ** -> instance || Check whether second graph is instance of first -> instantiate || Matches a pattern in a graph, if possible -> movegraph || Move a graph to a new node domain -> nodecontents || Determine the contents of a node -> nodelist || Determine the preorder list of reachable nodes from a given node -> nodeset || Determine the reachable nodes from a given node -> overwritegraph || Overwrite a graph with a given graph -> paths || List of all paths in the graph -> printgraph || Prints a graph seen from given nodes -> prunegraph || Undefine the contents of a node -> redirectgraph || Redirects all references to nodes in a graph -> refcount || Determines the reference count function of a graph -> restrictgraph || Restricts the graph to certain defined nodes -> showgraph || Text representation of a graph -> updategraph || Update the contents of a node - -Required types: none - ------------------------------------------------------------- - -Includes --------- - -> %include "basic.lit" || foldlr mapsnd showlist showpair -> %include "pfun.lit" || domres emptypfun extend overwrite pfun postcomp restrict showpfun total - ------------------------------------------------------------- - -Implementation --------------- - -> abstype graph * ** -> with emptygraph :: graph * ** -> updategraph :: ** -> (*,[**]) -> graph * ** -> graph * ** -> prunegraph :: ** -> graph * ** -> graph * ** -> restrictgraph :: [**] -> graph * ** -> graph * ** -> redirectgraph :: (**->**) -> graph * ** -> graph * ** -> overwritegraph :: graph * ** -> graph * ** -> graph * ** -> showgraph :: (*->[char]) -> (**->[char]) -> graph * ** -> [char] -> nodecontents :: graph * ** -> ** -> (bool,(*,[**])) -> nodeset :: graph * ** -> [**] -> ([**],[**]) - -> movegraph :: (***->**) -> [***] -> graph * *** -> graph * ** -> printgraph :: (*->[char]) -> (**->[char]) -> graph * ** -> [**] -> [[char]] -> refcount :: graph * ** -> [**] -> ** -> num - -> graph * ** == pfun ** (*,[**]) - -> emptygraph = emptypfun -> updategraph = extend -> prunegraph = restrict -> restrictgraph = domres -> redirectgraph = postcomp.mapsnd.map -> overwritegraph = overwrite -> showgraph showfunc shownode = showpfun shownode (showpair showfunc (showlist shownode)) -*/ - -// The empty graph. -emptygraph :: .Graph sym var - -// Assign a node to a variable in a graph. -updategraph :: var .(Node sym var) !.(Graph sym var) -> .Graph sym var - -// Unassign a variable in a graph, making it free. -prunegraph :: var !.(Graph sym var) -> .Graph sym var - -// Restrict a graph to a given domain, i.e. -// make all variables free except those in the domain. -restrictgraph :: .[var] .(Graph sym var) -> .Graph sym var | == var - -// Redirect references (node arguments) in a graph -// according to a redirection function -redirectgraph :: (var->var) !.(Graph sym var) -> .Graph sym var - -// Overwrite the variables in the second graph by their contents in the first. -// Keeps the contents of the second graph if free in the first. -overwritegraph :: !.(Graph sym var) !.(Graph sym var) -> .Graph sym var - -// Movegraph moves a graph to a different variable domain -// Requires a list of bound variables in the graph -movegraph :: (var1->var2) !.[var1] .(Graph sym var1) -> .Graph sym var2 | == var1 - -// Varcontents obtains the contents of a variable in a graph -// Returns a boolean determining if it's bound, and -// its contents if the boolean is True. -varcontents :: !.(Graph sym var) var -> (.Bool,Node sym var) | == var - -// Graphvars determines the top-level-bound and free variables in a graph, -// reachable from a given list of variables. -// No duplicates. -graphvars :: .(Graph sym var) !.[var] -> (.[var],.[var]) | == var - -// Graphvarlist determines all top level variables in a graph, -// reachable from a given list of variables. -// No duplicates. -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 -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. -// Initial list of variables is counted too. -refcount :: .(Graph sym var) !.[var] -> (var -> Int) | == var - -// Determine whether the second argument is an instance of the first, -// i.e. whether there is a structure preserving mapping from the first to the second. -// Free variables may be mapped to anything. -// Bound variables may not be mapped to free variables. -isinstance - :: (.Graph sym pvar,pvar) - (.Graph sym var,var) - -> Bool - | == sym - & == var - & == pvar - -/* -> compilegraph :: [(**,(*,[**]))] -> graph * ** -> compilegraph = foldr (uncurry updategraph) emptygraph -*/ - -compilegraph :: ![(var,Node sym var)] -> Graph sym var - -/* - ------------------------------------------------------------------------- - -> foldgraph -> :: (**->***->***) -> -> (**->***) -> -> (*->[***]->***) -> -> graph * ** -> -> [**] -> -> [***] - -> foldgraph folddef foldref foldcont graph roots -> = foldedroots -> where count = refcount graph roots -> (unused,foldedroots) = foldlm fold ([],roots) -> fold (seen,node) -> = (seen,foldref node), if member seen node -> = (seen'',cond (def&count node>1) (folddef node folded) folded), otherwise -> where (seen'',folded) -> = (seen',foldcont sym foldedargs), if def -> = (node:seen,foldref node), otherwise -> (seen',foldedargs) = foldlm fold (node:seen,args) -> (def,(sym,args)) = nodecontents graph node - - -> paths :: graph * ** -> ** -> [[**]] - -> paths graph node -> = paths' [] node [] -> where paths' top node rest -> = rest, if member top node -> = top':cond def (foldr (paths' top') rest args) rest, otherwise -> where (def,(sym,args)) = nodecontents graph node -> top' = node:top - - -> extgraph :: graph * ** -> graph * *** -> [***] -> pfun *** ** -> graph * ** -> graph * ** -> extgraph sgraph pattern pnodes matching graph -> = foldr addnode graph pnodes -> where addnode pnode -> = total id (postcomp addnode' matching) pnode, if fst (nodecontents pattern pnode) -> = id, otherwise -> addnode' snode -> = updategraph snode scont, if sdef -> = id, otherwise ->|| = error "extgraph: closed node mapped to open node", otherwise -> || Could have used id, but let's report error when there is one... -> where (sdef,scont) = nodecontents sgraph snode - -*/ - -extgraph :: (Graph sym var) (Graph sym pvar) [pvar] (Pfun pvar var) (Graph sym var) -> Graph sym var | == var & == pvar - -instance == (Graph sym var) | == sym & == var - -instantiate :: - (Graph sym pvar,Graph sym var) - (pvar,var) - ([(pvar,var)],[(pvar,var)],[(pvar,var)]) - -> ([(pvar,var)],[(pvar,var)],[(pvar,var)]) - | == sym - & == var - & == pvar diff --git a/sucl/graph.icl b/sucl/graph.icl deleted file mode 100644 index e0499e0..0000000 --- a/sucl/graph.icl +++ /dev/null @@ -1,427 +0,0 @@ -implementation module graph - -// $Id$ - -import pfun -import basic -import general -import StdEnv - -/* - -graph.lit - Unrooted graphs -=========================== - -Description ------------ - -This script implements an abstract type for unrooted graphs and useful -functions to manipulate them. - -*/ - -// A mapping from variables to nodes (unrooted) -:: Graph sym var - = GraphAlias !(Pfun var (Node sym var)) - -// A node, bearing the contents of a variable -:: Node sym var - :== (sym,[var]) - -// ==> Symbols and variables are going to be defined in different modules. -// They're here now because I don't want to throw them away. -:: Symbol - = Apply // Unwritten expression application - | Cons // Non-empty list - | Nil // Empty list - | Int Int // A specified integer - | Char Char // A specified character - | User String String // A user-supplied symbol - | Tuple Int // A tuple symbol of specified arity - | Select Int Int // A tuple selection operator of specified arity and index - | If // Predefined IF function - | Bool Bool // A specified boolean -// | MkRecord [Field] // Record construction? -// | GetField [Field] Field // Record field selection? - -:: Variable - = Named String // Variable was named in the program - | Anonymous Int // Implicit variable - -/* - -> emptygraph = emptypfun -> updategraph = extend -> prunegraph = restrict -> restrictgraph = domres -> redirectgraph = postcomp.mapsnd.map -> overwritegraph = overwrite -> showgraph showfunc shownode = showpfun shownode (showpair showfunc (showlist shownode)) -*/ - -// The empty set of bindings -emptygraph :: .Graph sym var -emptygraph = GraphAlias emptypfun - -updategraph :: var .(Node sym var) !.(Graph sym var) -> .Graph sym var -updategraph var node graph = mapgraph (extend var node) graph - -prunegraph :: var !.(Graph sym var) -> .Graph sym var -prunegraph var graph = mapgraph (restrict var) graph - -restrictgraph :: .[var] .(Graph sym var) -> .Graph sym var | == var -restrictgraph vars graph = mapgraph (domres vars) graph - -redirectgraph :: (var->var) !.(Graph sym var) -> .Graph sym var -redirectgraph redirection graph -= mapgraph (postcomp (mapsnd (map redirection))) graph - -overwritegraph :: !.(Graph sym var) !.(Graph sym var) -> .Graph sym var -overwritegraph (GraphAlias newpf) oldgraph = mapgraph (overwrite newpf) oldgraph - -movegraph :: (var1->var2) !.[var1] .(Graph sym var1) -> .Graph sym var2 | == var1 -movegraph movevar varspace oldgraph -= foldr addvar emptygraph varspace - where addvar var - | def - = updategraph (movevar var) (sym,map movevar args) - = id - where (def,(sym,args)) = varcontents oldgraph var - -varcontents :: !.(Graph sym var) var -> (.Bool,Node sym var) | == var -varcontents (GraphAlias pfun) v -= (total (False,(nosym,noargs)) o postcomp found) pfun v - where found x = (True,x) - nosym = abort "varcontents: getting symbol of free variable" - noargs = abort "varcontents: getting arguments of free variable" - -graphvars :: .(Graph sym var) !.[var] -> (.[var],.[var]) | == var -graphvars graph roots -= 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 (prune,([],[])) roots) - where ns var seenboundfree - | 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 -varlist graph roots -= depthfirst arguments id roots - where arguments var - | def = args - = [] - where (def,(_,args)) = varcontents graph var - -/* -> prefix graph without nodes -> = foldlr f (without,[]) nodes -> where f node (seen,nodes) -> = (seen,nodes), if member seen node -> = (seen',node:nodes'), otherwise -> where (seen',nodes') -> = (node:seen,nodes), if ~def -> = foldlr f (node:seen,nodes) args, otherwise -> (def,(sym,args)) = nodecontents graph node -*/ -prefix :: .(Graph sym var) .[var] !.[var] -> .([var],[var]) | == var -prefix graph without vars -= foldlr f (without,[]) vars - where f var (seen,vars) - | isMember var seen = (seen,vars) - = (seen`,[var:vars`]) - where (seen`,vars`) - = if (not def) ([var:seen],vars) - (foldlr f ([var:seen],vars) args) - (def,(_,args)) = varcontents graph var - -/* -> printgraph showfunc shownode graph nodes -> = prntgrph showfunc shownode (refcount graph nodes) graph nodes - -> prntgrph showfunc shownode count graph -> = snd.foldlr pg ([],[]) -> where pg node (seen,reprs) -> = (seen2,repr3:reprs) -> where repr3 -> = shownode node++':':repr2, if ~member seen node & def & count node>1 -> = repr2, otherwise -> (seen2,repr2) -> = (seen,shownode node), if member seen node \/ ~def -> = (seen1,showfunc func), if args=[] -> = (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 = printgraphBy toString toString 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) - (showvar node+++":"+++repr2) - repr2 - (seen2,repr2) - = if (isMember node seen || not def) - (seen,showvar node) - (if (args==[]) - (seen1,showsym func) - (seen1,"("+++showsym 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 -> = count', if count node>0 \/ ~def -> = foldr rfcnt count' args, otherwise -> where count' = inc node count -> (def,(func,args)) = nodecontents graph node - -> inc n f n = f n+1 -> inc m f n = f n -*/ -refcount :: .(Graph sym var) !.[var] -> (var -> Int) | == var -refcount graph roots -= foldr rfcnt (const 0) roots - where rfcnt var count - | (count var>0) || (not def) = count` - = foldr rfcnt count` args - where count` = inccounter var count - (def,(_,args)) = varcontents graph var - -/* - -Compilegraph compiles a graph from parts. -Uses in Miranda: - * reading a parsed program from a file. -*/ - -compilegraph :: ![(var,Node sym var)] -> Graph sym var -compilegraph nds = foldr (uncurry updategraph) emptygraph nds - -/* - -`Instance g1 g2' determines whether g2 is an instance of g1. -Uses in Miranda: - * strat.lit.m: checking whether the strategy is starting a graph that is already in the history. - * newfold.lit.m: checking whether a tail of the spine occurs in the history. - -> instance :: (graph * ***,***) -> (graph * **,**) -> bool -> instance (pgraph,pnode) (sgraph,snode) -> = errs=[] -> where (seen,mapping,errs) = instantiate (pgraph,sgraph) (pnode,snode) ([],[],[]) - -*/ - -isinstance - :: (.Graph sym pvar,pvar) - (.Graph sym var,var) - -> Bool - | == sym - & == var - & == pvar - -isinstance (pgraph,pvar) (sgraph,svar) -= isEmpty (thd3 (findmatching (pgraph,sgraph) (pvar,svar) ([],[],[]))) <--- "graph.isinstance ends" - -/* - -Suppose `Instantiate (pattern,graph) (pnode,gnode) (seen,mapping,errs)' -returns `(seen',mapping',errs')'. - -Then `mapping'' is the best attempt at extending the `mapping' to show that `graph' is an instance of `pattern'. -If it is not, then `errs'' is `errs' extended with node pairs that fail to match. -In the mean time, the nodes pairs examined are added to `seen', and returned as `seen''. -Node pairs already in `seen' are assumed to have already been checked and are not checked again. - -Uses in Miranda: - * extract.lit.m: used to find instances of patterns in the termination history, while folding trace tips. - * transform.lit.m: Uses a different `instantiate' from rewr.lit.m. - -`Instantiateargs' is the logical extension of `instantiate' to lists of node pairs. - -*/ - -instantiate :: - (Graph sym pvar,Graph sym var) - (pvar,var) - ([(pvar,var)],[(pvar,var)],[(pvar,var)]) - -> ([(pvar,var)],[(pvar,var)],[(pvar,var)]) - | == sym - & == var - & == pvar - -instantiate (pgraph,sgraph) (pnode,snode) (seen,mapping,errs) -| isMember psnode seen - = (seen,mapping,errs) -| isMember pnode (map fst seen) - = ([psnode:seen],mapping,[psnode:errs]) -| not pdef - = ([psnode:seen],[psnode:mapping],errs) -| not sdef - = ([psnode:seen],mapping,[psnode:errs]) -| not (psym==ssym && eqlen pargs sargs) - = ([psnode:seen],mapping,[psnode:errs]) -= (seen`,[psnode:mapping`],errs`) - where (pdef,(psym,pargs)) = varcontents pgraph pnode - (sdef,(ssym,sargs)) = varcontents sgraph snode - (seen`,mapping`,errs`) = instantiateargs (pgraph,sgraph) (zip2 pargs sargs) ([psnode:seen],mapping,errs) - psnode = (pnode,snode) - -instantiateargs :: - (Graph sym pvar,Graph sym var) - [(pvar,var)] - ([(pvar,var)],[(pvar,var)],[(pvar,var)]) - -> ([(pvar,var)],[(pvar,var)],[(pvar,var)]) - | == sym - & == var - & == pvar - -instantiateargs psgraph [] sme = sme -instantiateargs psgraph [psnode:psnodes] (seen,mapping,errs) -= (seen``,mapping``,errs``) - where (seen`,mapping``,errs``) = instantiate psgraph psnode (seen,mapping`,errs`) - (seen``,mapping`,errs`) = instantiateargs psgraph psnodes (seen`,mapping,errs) - -:: Matchstate var pvar - :== ( [(pvar,var)] // Pattern-subject var combo's already visited - , [(pvar,var)] // Mapping from pattern vars to subject vars - , [(pvar,var)] // Pattern-subject var combo's that don't match (different symbol or arities) - ) - -findmatching - :: (Graph sym pvar,Graph sym var) - .(pvar,var) - u:(Matchstate var pvar) - -> u:Matchstate var pvar - | == sym - & == var - & == pvar - -findmatching (pgraph,sgraph) (pvar,svar) (seen,mapping,errs) -| isMember psvar seen -= (seen,mapping,errs) -| isMember pvar (map fst seen) -= ([psvar:seen],mapping,[psvar:errs]) -| not pdef -= ([psvar:seen],[psvar:mapping],errs) -| not sdef -= ([psvar:seen],mapping,[psvar:errs]) -| not (psym==ssym && eqlen pargs sargs) -= ([psvar:seen],mapping,[psvar:errs]) -= (seen`,[psvar:mapping`],errs`) - where (pdef,(psym,pargs)) = varcontents pgraph pvar - (sdef,(ssym,sargs)) = varcontents sgraph svar - (seen`,mapping`,errs`) = findargmatching (pgraph,sgraph) (zip2 pargs sargs) ([psvar:seen],mapping,errs) - psvar = (pvar,svar) - -findargmatching - :: (Graph sym pvar,Graph sym var) - [.(pvar,var)] - u:(Matchstate var pvar) - -> v:Matchstate var pvar - | == sym - & == var - & == pvar - , [u<=v] - -findargmatching psgraph [] seenmappingerrs = seenmappingerrs -findargmatching psgraph [psvar:psvars] (seen,mapping,errs) -= (seen``,mapping``,errs``) - where (seen`,mapping``,errs``) = findmatching psgraph psvar (seen,mapping`,errs`) - (seen``,mapping`,errs`) = findargmatching psgraph psvars (seen`,mapping,errs) - -/* - ------------------------------------------------------------------------- - -A folding function for graphs. -Uses in Miranda: - * clean.lit.m: pretty-printing rewrite rules. - * pretty.lit.m: pretty-printing rewrite rules. - -> foldgraph -> :: (**->***->***) -> -> (**->***) -> -> (*->[***]->***) -> -> graph * ** -> -> [**] -> -> [***] - -> foldgraph folddef foldref foldcont graph roots -> = foldedroots -> where count = refcount graph roots -> (unused,foldedroots) = foldlm fold ([],roots) -> fold (seen,node) -> = (seen,foldref node), if member seen node -> = (seen'',cond (def&count node>1) (folddef node folded) folded), otherwise -> where (seen'',folded) -> = (seen',foldcont sym foldedargs), if def -> = (node:seen,foldref node), otherwise -> (seen',foldedargs) = foldlm fold (node:seen,args) -> (def,(sym,args)) = nodecontents graph node - -`Paths' lists all paths in a graph. -Never used in Miranda. - -> paths :: graph * ** -> ** -> [[**]] -> paths graph node -> = paths' [] node [] -> where paths' top node rest -> = rest, if member top node -> = top':cond def (foldr (paths' top') rest args) rest, otherwise -> where (def,(sym,args)) = nodecontents graph node -> top' = node:top - -`Extgraph sgraph pattern pnodes matching' extends some graph according -to the closed nodes in sgraph that closed nodes in pgraph are mapped to. -That is, we take the nodes from `pnodes', see if they are closed, -follow the mapping to `sgraph', see if they are closed there too, -and if so, add the contents in `sgraph' to the graph we're extending. - -Uses in Miranda: - * newfold.lit.m: function `findspinepart', to find parts of a spine. - Specifically, to extend history patterns as one traverses down the trace. - * transtree.lit.m: to extend the history when the reduce transformation is applied. - * transform.lit.m: idem. - -`Extgraph' is excluded in most import statements, -but there doesn't seem to be any other definition of it. -*/ - -extgraph :: (Graph sym var) (Graph sym pvar) [pvar] (Pfun pvar var) (Graph sym var) -> Graph sym var | == var & == pvar -extgraph sgraph pattern pnodes matching graph -= foldr addnode graph pnodes - where addnode pnode - = if (fst (varcontents pattern pnode)) (total id (postcomp addnode` matching) pnode) id - addnode` snode - = if sdef (updategraph snode scont) id - where (sdef,scont) = varcontents sgraph snode - -mapgraph :: - !( (Pfun var1 (sym1,[var1])) - -> Pfun var2 (sym2,[var2]) - ) - !.(Graph sym1 var1) - -> .Graph sym2 var2 -mapgraph f (GraphAlias pfun) = GraphAlias (f pfun) - -instance == (Graph sym var) | == sym & == var -where (==) (GraphAlias pf1) (GraphAlias pf2) - = pf1 == pf2 diff --git a/sucl/history.dcl b/sucl/history.dcl deleted file mode 100644 index 3daf399..0000000 --- a/sucl/history.dcl +++ /dev/null @@ -1,60 +0,0 @@ -definition module history - -// $Id$ - -from rule import Rgraph -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 - :== [HistoryAssociation sym var] - -// An association between a node-id in the subject graph and a history pattern -:: HistoryAssociation sym var - :== ( var // Attachment point in the subject graph where the history pattern is "housed" - , [HistoryPattern sym var] // The pattern in the history - ) - -// A pattern in the history, specifying the most general subject graph (footprint) for a reduction sequence -:: HistoryPattern sym var - :== Rgraph sym var - -// A link in a graph, indicated by its source node-id and the argument number -// The root of a graph can be indicated by the No constructor -:: Link var - :== Optional (var,Int) - -// Check the current subject graph in the history -matchhistory - :: (History sym var) // Complete history against which to check - [var] // Node-ids for which to include history patterns - (Graph sym var) // Current subject graph - var // Current application point of strategy - -> [HistoryPattern sym var] // Matching history patterns - | 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 - -printhistory :: - (sym->String) - (var->String) - String - (History sym var) - *File - -> .File - | == var diff --git a/sucl/history.icl b/sucl/history.icl deleted file mode 100644 index 8713904..0000000 --- a/sucl/history.icl +++ /dev/null @@ -1,99 +0,0 @@ -implementation module history - -// $Id$ - -import rule -import graph -import pfun -import basic -from general import Optional,Yes,No,---> -import StdEnv - -// A history relates node-ids in the subject graph to patterns -:: History sym var - :== [HistoryAssociation sym var] - -// An association between a node-id in the subject graph and a history pattern -:: HistoryAssociation sym var - :== ( var // Attachment point in the subject graph where the history pattern is "housed" - , [HistoryPattern sym var] // The pattern in the history - ) - -// A pattern in the history, specifying the most general subject graph (footprint) for a reduction sequence -:: HistoryPattern sym var - :== Rgraph sym var - -// A link in a graph, indicated by its source node-id and the argument number -// The root of a graph can be indicated by the No constructor -:: Link var - :== Optional (var,Int) - - -/************************************************ -* Verifying a subject graph against the history * -************************************************/ - -matchhistory - :: (History sym var) // Complete history against which to check - [var] // Node-ids for which to include history patterns - (Graph sym var) // Current subject graph - var // Current application point of strategy - -> [HistoryPattern sym var] // Matching history patterns - | Eq sym - & Eq var - -matchhistory hist spinenodes sgraph snode -= 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--->"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 :: - (HistoryPattern sym pvar) - (Graph sym var) - var - ([(pvar,var)],[(pvar,var)],[(pvar,var)]) - -> ([(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 = file <<< "<history>" // sfoldl (writeHistoryAssociation) file 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]) diff --git a/sucl/hunt.icl b/sucl/hunt.icl deleted file mode 100644 index 747230c..0000000 --- a/sucl/hunt.icl +++ /dev/null @@ -1,57 +0,0 @@ -implementation module hunt - -// $Id$ - -/* - ->|| Literal script "hunt.lit" - -> %export -> findfiles -> glob -> readable -> writable -> getpath -> expand - -> %include "basic.lit" - -> findfiles :: ([char]->bool) -> [[char]] -> [[char]] -> [char] -> [[char]] - -> findfiles goodmode exts paths base -> = filter (goodmode.filemode) (expand exts paths base) - -> relative :: [char] -> bool -> relative ('/':cs) = False -> relative ccs = True - -> expand :: [[char]] -> [[char]] -> [char] -> [[char]] -> expand exts paths base -> = [path++'/':base++ext|path<-mkset paths;ext<-mkset exts], if relative base -> = [base++ext|ext<-mkset exts], otherwise - -> readable :: [char] -> bool -> readable ('d':rwx) = False -> readable (d:'r':wx) = True -> readable drwx = False - -> writable :: [char] -> bool -> writable "" = True -> writable ('d':rwx) = False -> writable (d:r:'w':x) = True -> writable drwx = False - -> getpath :: [[char]] -> [char] -> [[char]] -> getpath syspath varname -> = foldr (fill syspath) [] (split ':' (getenv varname)) - -> fill syspath [] = (syspath++) -> fill syspath = (:) - -> glob :: [char] -> [[char]] -> glob pattern -> = filter (~=[]) ((concat.map (split ' ').lines) stdout), if return=0 -> = error ("glob: "++stderr), otherwise -> where (stdout,stderr,return) = system ("echo "++pattern) - -*/ diff --git a/sucl/law.dcl b/sucl/law.dcl deleted file mode 100644 index e136b46..0000000 --- a/sucl/law.dcl +++ /dev/null @@ -1,19 +0,0 @@ -definition module law - -// $Id$ - -from coreclean import SuclSymbol,SuclVariable -from strat import Law,Strategy -from StdOverloaded import == - -// Transitive necessities - -from strat import Substrategy -from spine import Spine,Subspine -from graph import Graph,Node - -// The list of special Clean transformation laws -cleanlaws :: [(SuclSymbol,Law SuclSymbol var SuclVariable result)] - -// The strategy for built in clean symbols -corestrategy :: ((Graph SuclSymbol SuclVariable) SuclVariable var -> Bool) -> Strategy SuclSymbol var SuclVariable result | == var diff --git a/sucl/law.icl b/sucl/law.icl deleted file mode 100644 index ef33b2e..0000000 --- a/sucl/law.icl +++ /dev/null @@ -1,233 +0,0 @@ -implementation module law - -// $Id$ - -import coreclean -import strat -import spine -import rule -import dnc -import graph -import basic -from general import ---> -import StdEnv - -/* - -> %export -> cleanlaws -> corestrategy - -> %include "dnc.lit" - -> %include "../src/basic.lit" -> %include "../src/pfun.lit" -> %include "../src/graph.lit" -> %include "../src/complete.lit" -> %include "../src/rule.lit" -> %include "../src/spine.lit" -> %include "strat.lit" -> %include "../src/clean.lit" - -> intmullaw :: law symbol ** node **** - -> intmullaw substrat subject found rnf sargs fail - -> = rulelaw (leftunitrule (Int 1)) substrat subject found rnf sargs fail' -> where fail' = rulelaw (rightunitrule (Int 1)) substrat subject found rnf sargs fail'' -> fail'' = primlaw (intop product) substrat subject found rnf sargs fail - -> mullaws -> = [ rulelaw (leftunitrule (Int 1)) -> , rulelaw (rightunitrule (Int 1)) -> , primlaw (intop product) -> ] - -> intaddlaw :: law symbol ** node **** - -> intaddlaw substrat subject found rnf sargs fail -> = trylaw subject found' sargs (leftunitrule (Int 0)) fail' -> where fail' = trylaw subject found' sargs (rightunitrule (Int 0)) fail'' -> fail'' = strictprimop (intop sum) substrat subject found sargs fail -> found' subspine = found subspine - -> addlaws -> = [ rulelaw (leftunitrule (Int 0)) -> , rulelaw (rightunitrule (Int 0)) -> , primlaw (intop sum) -> ] - -> intsublaw :: law symbol ** node **** - -> intsublaw substrat subject found rnf sargs fail -> = trylaw subject found' sargs (rightunitrule (Int 0)) fail' -> where fail' = strictprimop (intop sublist) substrat subject found sargs fail -> found' subspine = found subspine -> sublist [x,y] = x-y - -> sublaws -> = [ rulelaw (rightunitrule (Int 0)) -> , primlaw (intop sublist) -> ] -> where sublist [x,y] = x-y - -> intop :: ([num]->num) -> [symbol] -> symbol -> intop op symbols = Int (op [i|Int i<-symbols]) - -> leftunitrule leftunit -> = mkrule [Named "leftarg",Named "rightarg"] (Named "rightarg") (updategraph (Named "leftarg") (leftunit,[]) emptygraph) - -> rightunitrule rightunit -> = mkrule [Named "leftarg",Named "rightarg"] (Named "leftarg") (updategraph (Named "rightarg") (rightunit,[]) emptygraph) - -> strictprimop -> :: ([*]->*) -> -> substrategy * ** node **** -> -> graph * ** -> -> (subspine * ** node->****) -> -> [**] -> -> **** -> -> **** - -> strictprimop op substrat subject found sargs fail -> = forcenodes substrat found foundredex sargs, if and (map fst conts) -> = fail, otherwise -> where conts = map (dnc (const "in strictprimop") subject) sargs -> result = op (map (fst.snd) conts) -> primrule = mkrule primargs primroot primgraph -> primargs = map snd (zip2 sargs heap) -> primroot = Named "primresult" -> primgraph = updategraph primroot (result,[]) emptygraph -> matching = foldr (uncurry extend) emptypfun (zip2 primargs sargs) -> foundredex = found (Redex primrule matching) - -> primlaw -> :: ([*]->*) -> -> law * ** node **** - -> primlaw op substrat subject found rnf sargs fail -> = strictprimop op substrat subject found sargs fail - ------------------------------------------------------------------------- - -> cleanlaws :: [(symbol,law symbol ** node ****)] -*/ - -cleanlaws :: [(SuclSymbol,Law SuclSymbol var SuclVariable result)] -cleanlaws =: [] - -/* -> cleanlaws -> = [(User "deltaI" "*",law) | law <- mullaws] ++ -> [(User "deltaI" "+",law) | law <- addlaws] ++ -> [(User "deltaI" "-",law) | law <- sublaws] ++ -> [(User "deltaI" "++",primlaw inc)] ++ -> [(User "deltaI" "--",primlaw dec)] - -> inc [Int n] = Int (n+1) -> dec [Int n] = Int (n-1) - ------------------------------------------------------------------------- - -> corestrategy :: (graph symbol node->node->**->bool) -> strategy symbol ** node **** - -Forcing arguments has already been done by the type rule -Also, using trylaw is easier - -> corestrategy matchable substrat subject found rnf (Apply,snodes) -> = trylaw subject found snodes (applyrule nc) (found Delta) -> where nc = dnc (const "in corestrategy") subject (hd snodes) - -> corestrategy matchable substrat subject found rnf (If,snodes) -> = tryrules matchable substrat subject found snodes (found MissingCase) ifrules - -> corestrategy matchable substrat subject found rnf (Select a i,snodes) -> = tryrules matchable substrat subject found snodes (found MissingCase) [selectrule a i] - -> corestrategy matchable substrat subject found rnf (User module id,snodes) -> = found MissingCase - -> corestrategy matchable substrat subject found rnf (ssym,snodes) -> = rnf -*/ - -// The strategy for built in clean symbols -corestrategy :: ((Graph SuclSymbol SuclVariable) SuclVariable var -> Bool) -> Strategy SuclSymbol var SuclVariable result | == var -corestrategy matchable =(\ substrat subject found rnf snode - -> let (ssym,sargs) = snode - in case ssym - of SuclUser sptr - -> found MissingCase - SuclCase eptr - -> found MissingCase - SuclApply argc - -> trylaw subject found sargs (applyrule nc) (found Delta) - where nc = dnc (const "in corestrategy") subject (hd sargs) - _ - -> rnf) - -/* -> applyrule :: (bool,(*,[**])) -> rule * node -> applyrule (sdef,scont) -> = aprule (anode,(sym,aargs)) [enode] aroot -> where (aargs,anode:aroot:enode:heap') = claim sargs heap -> (sym,sargs) -> = scont, if sdef -> = (nosym,[]), otherwise -> nosym = error "applyrule: no function symbol available" -*/ - -applyrule :: (Bool,Node sym var) -> Rule sym SuclVariable -applyrule (sdef,scont) - = aprule (anode,(sym,aargs)) [enode] aroot - where (aargs,[anode,aroot,enode:_]) = (claim--->"basic.claim begins from law.applyrule") sargs suclheap - (sym,sargs) - = if sdef scont (nosym,[]) - nosym = abort "applyrule: no function symbol available" - -/* -> aprule :: (***,(*,[***])) -> [***] -> *** -> rule * *** -> aprule (anode,(sym,aargs)) anodes aroot -> = mkrule (anode:anodes) aroot agraph -> where agraph -> = ( updategraph aroot (sym,aargs++anodes) -> . updategraph anode (sym,aargs) -> ) emptygraph -*/ - -aprule :: (pvar,Node sym pvar) [pvar] pvar -> Rule sym pvar -aprule (anode,(sym,aargs)) anodes aroot - = mkrule [anode:anodes] aroot agraph - where agraph - = ( updategraph aroot (sym,aargs++anodes) - o updategraph anode (sym,aargs) - ) emptygraph - -/* -> apmatching :: [**] -> [***] -> pfun *** ** -> apmatching snodes anodes -> = foldr (uncurry extend) emptypfun nodepairs -> where nodepairs = zip2 anodes snodes - -> claims :: [[*]] -> [**] -> ([[**]],[**]) -> claims [] heap = ([],heap) -> claims (nodes:nodess) heap -> = (nodes':nodess',heap'') -> where (nodes',heap') = claim nodes heap -> (nodess',heap'') = claims nodess heap' - -> ifrules :: [rule symbol node] - -> ifrules -> = [ifrule True then,ifrule False else] -> where ifrule bool branch = mkrule [cond,then,else] branch (updategraph cond (Bool bool,[]) emptygraph) -> cond = Named "cond"; then = Named "then"; else = Named "else" - -> selectrule :: num -> num -> rule symbol node - -> selectrule a i -> = mkrule [tuple] (args!(i-1)) (updategraph tuple (Tuple a,args) emptygraph) -> where tuple = Named "tuple" -> args = take a (tl heap) - -*/ diff --git a/sucl/loop.dcl b/sucl/loop.dcl deleted file mode 100644 index cdc6fc1..0000000 --- a/sucl/loop.dcl +++ /dev/null @@ -1,37 +0,0 @@ -definition module loop - -// $Id$ - -from strat import Strategy -from trace import Trace -from spine import Answer -from history import HistoryAssociation,HistoryPattern -from rule import Rgraph,Rule -from graph import Graph -from StdOverloaded import == -from StdFile import <<< -from StdString import toString - -from strat import Substrategy,Subspine // for Strategy -from trace import History,Transformation // for Trace -from spine import Spine // for Answer -from graph import Node // for Strategy -from basic import Optional // for Answer - -loop - :: (((Graph sym pvar) pvar var -> ub:Bool) -> Strategy sym var pvar (Answer sym var pvar)) - ([Rgraph sym pvar] (Rgraph sym pvar) -> ub:Bool) - !(.[var],.Rule sym var) - -> Trace sym var pvar - | == sym - & == var - & == pvar - & toString sym // Debugging - & toString var // Debugging - & <<< var // Debugging - -initrule - :: ![var] - (sym->[pvar]) - sym - -> ([var],Rule sym var) diff --git a/sucl/loop.icl b/sucl/loop.icl deleted file mode 100644 index 1090a88..0000000 --- a/sucl/loop.icl +++ /dev/null @@ -1,405 +0,0 @@ -implementation module loop - -// $Id$ - -import strat -import trace -import spine -import history -import rewr -import rule -import graph -import pfun -import basic -from general import Yes,No,---> -import StdEnv - -mstub = stub "loop" -block func = mstub func "blocked for debugging" - -/* - -loop.lit - Looping to produce a trace -===================================== - -Description ------------ - -This module describes the transformation of a tree of spines into a -trace. This is where the actual transformations on graphs are applied -like instantiation, reduction or strict annotation. - ------------------------------------------------------------- - -The function that produces a trace is given an initial task expression. - -The function first determines a transformation (Reduce,Annotate,Instantiate) to -apply, using the strategy. - -This may fail when the termination history indicates a required abstraction -higher up. In that case, return at once with failure, and the current graph -(with shared parts excluded) as the most specific generaliser. - -After application of the transformation, a trace is produced for the resulting -graph(s). - -However, the production of the subtraces may fail initially because of a -necessary abstraction higher-up which wasn't there (introduced recursion). - -Therefore, producing a trace can return one of two results: either a successful -trace, or failure, with an indication of which abstraction was actually -necessary. - -The needed generalisation is computed by taking the most specific generaliser -for each pattern in the termination history. - -In the general case, generation of the subtraces fails for both the history -pattern of the current transformation, and some patterns higher up (which were -also passed to the trace generation function. There are now two courses of -action: - -[1] Apply abstraction instead of the current transformation. Use the returned - most specific generaliser and the original graph to determine how to - abstract. Then, generate subtraces. There should be no more abstractions - necessary for the current node, because they should be handled in the - graphs resulting from the abstraction.[*] - -[2] Immediately return the failure, assuming (rule of thumb) that when the - upper generalisation was necessary, the lower one won't make it go away. - This is probably an optimisation of the optimisation process, but it can be - important, as some backtracking code (exponential!) may not have to be - executed. - -[*] This may not be entirely true in the case of sharing. Because shared parts - must be pruned, the termination pattern may get smaller in the abstraction - operation. - -Questions: - -[?] Which would yield better results and/or perform better: [1] or [2] above? - -[?] Must the abstracted areas be associated with termination patterns that - caused their introduction? Or somehow with the trace node where they were - introduced? The termination patterns don't have to be the same over - different branches of the trace! Do they play a role at all in selecting - the abstracted part? Actually, they don't. We just need their roots so we - can find the corresponding subgraphs and determine the MSG's. - -It would appear we can traverse the trace when everything is done and collected -all the introduced functions from it. - ------------------------------------------------------------- - -*/ - -/* Disable the new abstraction node - Unsafe subtraces are going to be pruned again. - -:: FallibleTrace sym var pvar - = GoodTrace (Trace sym var pvar) - | NeedAbstraction [Rgraph sym var] - -:: Strat sym var pvar - :== (History sym var) - (Rgraph sym var) - -> Answer sym var pvar - -maketrace - :: (Strat sym var pvar) // The strategy - (History sym var) // Patterns to stop partial evaluation - (Rgraph sym var) // Subject graph - -> FallibleTrace sym var pvar // The result - -maketrace strategy history subject - = ( case answer - of No // Root normal form, abstract and continue with arguments - -> handlernf - Yes spine // Do something, even if it is to fail - -> ( case subspine - of Cycle // Cycle in spine. Generate x:_Strict x x with _Strict :: !a b -> b. Probably becomes a #! - -> handlecycle - Delta // Primitive function. Abstract its application and continue with remainder. - -> handledelta - Force n (spine) // Shouldn't happen - -> abort "loop: maketrace: spinetip returned Force???" - MissingCase // Missing case. Generate _MissingCase, possibly parametrised with user function? - -> handlemissingcase - Open pattern // Need instantiation. Generate two branches, extend history (for both) and continue. - -> handleopen pattern - Partial rule match rulenode spine - -> abort "loop: maketrace: spinetop returned Partial???" - Unsafe histpat // Require pattern from history. - -> handleunsafe histpat // If we have a more general version with a name attached, use that. - // Otherwise, fail with the corresponding subgraph - Redex rule match // Found a redex. Unfold, extend history and continue. - -> handleredex rule match - Strict // Need to put a strictness annotation on an open node-id. - -> handlestrict // Abstract _Strict <mumble> <mumble> and continue with rest. - ) spine - where (redexroot,subspine) = spinetip spine - ) strategy history subject - where answer = strategy history subject - -handlernf :: (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar -handlernf _ _ _ = undef - -handlecycle :: (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar -handlecycle _ _ _ _ = undef - -handledelta :: (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar -handledelta _ _ _ _ = undef - -handlemissingcase :: (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar -handlemissingcase _ _ _ _ = undef - -handleopen :: (Rgraph sym pvar) (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar -handleopen _ _ _ _ _ = undef - -handleunsafe :: (HistoryPattern sym var) (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar -handleunsafe _ _ _ _ _ = undef - -handleredex :: (Rule sym pvar) (Pfun pvar var) (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar -handleredex _ _ _ _ _ _ = undef - -handlestrict :: (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar -handlestrict _ _ _ _ = undef - ------------------------------------------------------------- - -Types ------ - -*/ - -/* The action itself takes various arguments, and returns a transformation -*/ - -:: Action sym var pvar - :== (Actcont sym var pvar) // Continuation to do subsequent symbolic reduction - (History sym var) // Termination patterns - (Failinfo sym var pvar) // Failed matches - Bool // Instantiation attempted - [Bool] // Strict arguments of function to generate - var // Root of subject graph - (Graph sym var) // Subject graph - [var] // Heap of unused nodes - -> Transformation sym var pvar - -/* Action continuation - An action continuation takes the result of a single partial evaluation action, - and ultimately collects all suchs actions into a trace. -*/ - -:: Actcont sym var pvar - :== (History sym var) // Termination patterns - (Failinfo sym var pvar) // Failed matches - Bool // Instantiation attempted - [Bool] // Strict arguments of function to generate - var // Root of subject graph - (Graph sym var) // Subject graph - [var] // Heap of unused nodes - -> Trace sym var pvar - -/* Failinfo is a function type - A function of this type assigns a list of rooted graphs to a varable. - This list of rooted graphs are precisely those patterns that symfailedsym to - match at the given variable in the subject graph. -*/ - -:: Failinfo sym var pvar - :== var - -> [Rgraph sym pvar] - -/* - ------------------------------------------------------------- - -Implementation --------------- - -*/ - -loop - :: (((Graph sym pvar) pvar var -> ub:Bool) -> Strategy sym var pvar (Answer sym var pvar)) - ([Rgraph sym pvar] (Rgraph sym pvar) -> ub:Bool) - !(.[var],.Rule sym var) - -> Trace sym var pvar - | == sym - & == var - & == pvar - & toString sym // Debugging - & 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 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--->"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 - initstricts = map (const False) sargs - - sargs = arguments rule; initsroot = ruleroot rule; initsubject = rulegraph rule - -listselect :: [.Bool] [.elem] -> [.elem] -listselect [True:bs] [x:xs] = [x:listselect bs xs] -listselect [False:bs] [x:xs] = listselect bs xs -listselect _ _ = [] - -initrule - :: ![var] - (sym->[pvar]) - sym - -> ([var],Rule sym var) - -initrule [root:heap] template sym -= (heap`,mkrule args root (updategraph root (sym,args) emptygraph)) - where (args,heap`) = (claim--->"basic.claim begins from loop.initrule") (template sym) heap -initrule _ _ _ -= abort "initrule: out of heap space" - -/* ------------------------------------------------------------------------ */ - -transform - :: var // Top of spine (starting point for strategy) - [var] // Arguments of function to generate - !(Answer sym var pvar) // Result of strategy - -> Action sym var pvar - | == sym - & == var - & == pvar - -transform anode sargs (Yes spine) -= (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--->"loop.dostop begins from loop.transform") <--- "loop.transform ends for no spine" - -// ==== ATTEMPT TO INSTANTIATE A FREE VARIABLE WITH A PATTERN ==== - -tryinstantiate - :: var // The open node - (Rgraph sym pvar) // The pattern to instantiate with - var // The root of the spine - [var] // Arguments of the function to generate - -> Action sym var pvar - | == var - & == pvar - -tryinstantiate onode rpattern anode sargs -= 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 - = Instantiate ipattern success fail - = Stop - where success = continue history failinfo True stricts` sroot subject` heap` - fail = continue history failinfo` True stricts` sroot subject heap - failinfo` = adjust onode [rpattern:failinfo onode] failinfo - ipattern = mkrgraph onode subject` - (heap`,subject`) = rewrinstantiate pgraph proot onode (heap,subject) - proot = rgraphroot rpattern; pgraph = rgraphgraph rpattern - - stricts` = if instdone stricts (map2 ((||) o (==) onode) sargs stricts) - // Quickly annotate the open node as strict if this is the first instantiation - - strictargs = [sarg\\(True,sarg)<-zip2 stricts` sargs] - -goodorder - :: [var] - [var] - (Graph sym var) - (Graph sym var) - -> Bool - | == var - -goodorder stricts sargs subject subject` -= startswith match match` - 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 - :: .[elem] // list S - .[elem] // list L - -> .Bool // whether L starts with S - | == elem - -startswith [] _ = True -startswith [x:xs] [y:ys] -| x==y -= startswith xs ys -startswith _ _ = False - - -// ==== ATTEMPT TO UNFOLD A REWRITE RULE ==== - -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 - -> Action sym var pvar - | == sym - & == var - & == pvar - -tryunfold redexroot rule matching spine -= act <--- "loop.tryunfold ends" - where act continue history failinfo instdone stricts sroot subject heap - = Reduce reductroot trace - where (heap`,sroot`,subject`,matching`) - = xunfold redexroot rule (heap,sroot,subject,matching) - noredir = abort "transtree: no mapping foor root of replacement" - reductroot = total noredir matching` (ruleroot rule) - history` = extendhistory subject redirect spine history - redirect = adjust redexroot reductroot id - trace = continue history` failinfo instdone stricts sroot` subject` heap` - -tryannotate - :: var // The node to be made strict - [var] // Arguments of the function to generate - -> Action sym var pvar - | == var - -tryannotate strictnode sargs -= act <--- "loop.tryannotate ends" - where act continue history failinfo instdone stricts sroot subject heap - | not instdone && isMember strictnode sargs - = Annotate trace - = Stop - where stricts` = map2 ((||) o (==) strictnode) sargs stricts - trace = continue history failinfo instdone stricts` sroot subject heap - - -// ==== STOP PARTIAL EVALUATION ==== - -dostop - :: Action sym var pvar - -dostop -= ds <--- "loop.dostop ends" - where ds continue history failinfo instdone stricts sroot subject heap = Stop diff --git a/sucl/new.icl b/sucl/new.icl deleted file mode 100644 index 6507612..0000000 --- a/sucl/new.icl +++ /dev/null @@ -1,54 +0,0 @@ -implementation module new - -// $Id$ - -/* - -new.lit - One line module description -===================================== - -Description ------------ - -Describe in a few paragraphs what this module defines. - ------------------------------------------------------------------------- - -Interface ---------- - -Exported identifiers: - -> %export -> identifier || One line description -> ... - -Required types: - - identifier - type@source.lit type@source.lit - ... - ------------------------------------------------------------------------- - -Includes --------- - -> %include "source.lit" || identifier ... -> ... - ------------------------------------------------------------------------- - -Implementation --------------- - -Implementation of identifier - -> identifier -> :: type - -> identifierone arguments -> = body - -... - -*/ diff --git a/sucl/newfold.icl b/sucl/newfold.icl deleted file mode 100644 index ce7dff9..0000000 --- a/sucl/newfold.icl +++ /dev/null @@ -1,425 +0,0 @@ -implementation module newfold - -// $Id$ - -import extract -import trace -import spine -import rule -import dnc -import graph -import basic -import StdEnv - -import general - -/* - -newfold.lit - New folding function -================================== - -Description ------------ - -This module defines one function, `fullfold'. It derives a function -defintion from a trace, by first searching and folding autorecursion, -and searching the remainder of the trace for introduced recursion. - ------------------------------------------------------------- - -Includes --------- - -> %include "dnc.lit" - -> %include "../src/basic.lit" -> %include "../src/pfun.lit" -> %include "../src/graph.lit" -> %include "../src/rule.lit" -> %include "../src/spine.lit" -> %include "trace.lit" -> %include "extract.lit" - ------------------------------------------------------------- - -Interface ---------- - -Exported identifiers: - -> %export -> fullfold || Full folding function -> tracer || Debugging -> || extract || Fold a trace and extract new functions -> || etracer || Debugging - ------------------------------------------------------------- - -Deprecated type ---------------- - -> tracer * ** *** -> == ( (rgraph * **->(*,[**])) -> -> * -> -> trace * ** *** -> -> (bool,([bool],[rule * **],[rgraph * **])) -> ) -> -> (rgraph * **->(*,[**])) -> -> * -> -> trace * ** *** -> -> (bool,([bool],[rule * **],[rgraph * **])) -*/ - -:: FuncDef sym var - :== ( [var] // Arguments of function - , FuncBody sym var // Right hand side of function - ) - -:: FuncBody sym var - = MatchPattern - (Rgraph sym var) // Pattern to match - (FuncBody sym var) // Right hand side for matching graph (case branch) - (FuncBody sym var) // Right hand side for failed match (case default) - | BuildGraph - (Rgraph sym var) // Right hand side to reduce to - -/* -Implementation --------------- - -`Fullfold foldarea fnsymbol trace' folds the trace. It returns a -resulting list of rewrite rules and rooted graphs for which new -functions have to be introduced. - -First, an attempt is made to fold to the right hand side of the initial -rewrite rule (autorecursion), or residues of the right hand side for -which no instantiation was necessary. If any tip of the trace can be -folded, this is done. - -The remaining subtraces of the trace (which is possibly the whole trace) -are folded in their own right. Introduced recursion is applied if it -occurs within any subtrace. -*/ - -fullfold :: - (Etracer sym var pvar) - ((Rgraph sym var)->(sym,[var])) - sym - (Trace sym var pvar) - -> ([Bool],FuncDef sym var,[Rgraph sym var]) - | == sym - & == var - & == pvar - & toString sym - & toString var - & toString pvar - & <<< var - & <<< pvar - -fullfold trc foldarea fnsymbol trace -| recursive - = addlhs recurseresult -= addlhs (newextract trc foldarea trace) - where (recursive,recurseresult) = recurse foldarea fnsymbol trace - addlhs = mapsnd3 (pair (arguments rule)) - (Trace _ rule _ _ _) = trace - -/* -`Recurse foldarea fnsymbol trace' is a pair `(recursive,recurseresult)'. -`Recurseresult' is the derived function definition (strictness, rules, -and new areas), obtained by folding the trace. `Recurse' tries to fold -the areas in the trace to recursive function calls when at all possible. -The allowed patterns for the autorecursion are derived from the top of -the trace. If no recursive function call can be found, `recurseresult' -is `False'. -*/ - -recurse :: - ((Rgraph sym var)->(sym,[var])) - sym - -> (Trace sym var pvar) - -> (Bool,([Bool],FuncBody sym var,[Rgraph sym var])) - | == sym - & == var - & == pvar - & toString sym - & toString var - & toString pvar - & <<< var - & <<< pvar - -recurse foldarea fnsymbol -= f ([],[]) - where f newhisthist trace - | (trace--->trace) $ False - = error "shouldn't happen" - 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] - (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] - (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 - - -/* -`Foldtips foldarea foldcont hist trace' folds all occurrences of (rooted -graphs in hist) in the tips of the trace. It returns a list of rules, -which are the results of folding, and a list of areas for which -functions must be introduced. If no occurrences were found, Absent is -returned. -*/ - -foldtips :: - ((Rgraph sym var)->(sym,[var])) - (sym,[var]) - -> ([(var,Graph sym var)],[(var,Graph sym var)]) - (Trace sym var pvar) - -> (Bool,([Bool],FuncBody sym var,[Rgraph sym var])) - | == sym - & == var - & == pvar - -foldtips foldarea foldcont -= ft - 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) - where deltanodes = foldoptional [] getdeltanodes answer - rnfnodes = foldoptional [ruleroot rule] (const []) answer - Instantiate ipattern yestrace notrace - -> ft` (ft hist yestrace) (ft hist notrace) - where ft` (False,yessra) (False,nosra) = exres - ft` (yesfound,(yesstricts,yesbody,yesareas)) (nofound,(nostricts,nobody,noareas)) - = (True,(stricts,MatchPattern ipattern yesbody nobody,yesareas++noareas)) - Reduce reductroot trace - -> ft` (ft (fst hist,fst hist) trace) - where ft` (False,sra) = exres - ft` (found,sra) = (True,sra) - Annotate trace - -> ft` (ft hist trace) - where ft` (False,sra) = exres - ft` (found,sra) = (True,sra) - where (Trace stricts rule answer _ transf) = trace - exres = (False,newextract noetrc foldarea trace) - -rule2body rule = buildgraph (arguments rule) (ruleroot rule) (rulegraph rule) - -addstrict stricts (body,areas) = (stricts,body,areas) - -noetrc trace area = id - -pair x y = (x,y) - -/* ------------------------------------------------------------------------- - -`Extract foldarea trace (rules,areas)' folds the trace, creating rules -which are prepended to `rules' and areas for introduced functions which -are prepended to `areas'. - -The use of `extract' is to derive rules for parts of a trace that aren't -already folded by the detection of either auto or introduced recursion. - -The accumulator argument is for efficiency reasons. It is probably -clearer to drop it and instead apply `concat' at a higher level. - -Introduced recursion may be detected inside the trace. Since the trace -is in practice a subtrace of another trace, introduced recursion might -exist to the supertrace. This does not count, since it is not possible -to fold the first occurrence of the termination history pattern which is -in the supertrace. -*/ - -:: Etracer sym var pvar :== - (Trace sym var pvar) - (Rgraph sym var) - Bool - -> Bool - -newextract :: - (Etracer sym var pvar) - ((Rgraph sym var)->(sym,[var])) - (Trace sym var pvar) - -> ([Bool],FuncBody sym var,[Rgraph sym var]) - | == sym - & == var - & == pvar - -newextract trc newname (Trace stricts rule answer history transf) -| recursive - = (stricts,rule2body recrule,recareas) -= case transf - of Reduce reductroot trace - -> newextract trc newname trace - Annotate trace - -> newextract trc newname trace - Instantiate ipattern yestrace notrace - -> (stricts,MatchPattern ipattern yesbody nobody,yesareas++noareas) - where (_,yesbody,yesareas) = newextract trc newname yestrace - (_,nobody,noareas) = newextract trc newname notrace - Stop - -> (stricts,buildgraph rargs rroot stoprgraph,stopareas) - - where (recursive,unsafearea) - = if (isreduce transf) - (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 - - rargs = arguments rule; rroot = ruleroot rule; rgraph = rulegraph rule - rnfnodes = foldoptional (cons rroot) (const id) answer (varlist rgraph rargs) - - deltanodes = foldoptional [] getdeltanodes answer - -buildgraph :: - [var] - var - (Graph sym var) - -> FuncBody sym var | == var -buildgraph args root graph -= BuildGraph (mkrgraph root (compilegraph (map (pairwith (snd o varcontents graph)) newnodes))) - where newnodes = closedreplnodes--patnodes - closedreplnodes = fst (graphvars graph [root]) - patnodes = varlist graph args - -isreduce (Reduce reductroot trace) = True -isreduce transf = False - - -/* -`Findspinepart toprule rule spine (transformation,trace)' is a pair with -a boolean determining whether some instance of the `spine', determined -using `toprule', occurs in a residu of itself in `trace'. - -The use of `findspinepart' is to detect introduced recursion in `trace' -to its root. -*/ - -findspinepart :: (Rule sym var) (Transformation sym var pvar) (Spine sym var pvar) -> (Bool,Rgraph sym var) | == sym & == var & == pvar - -findspinepart rule transf spine -= snd (foldspine pair stop stop force stop (const stop) partial (const stop) redex stop spine) - where pair node (pattern,recursion) - = (pattern`,recursion`) - where pattern` - = if def (updategraph node cnt pattern) pattern - (def,cnt) = dnc (const "in findspinepart") graph node - recursion` - | findpattern (pattern`,node) (spinenodes spine) node transf - = (True,mkrgraph node pattern`) - = recursion - force _ res = res - 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") - graph = rulegraph rule - -extgraph` sgraph rule -= extgraph sgraph rgraph (varlist rgraph (arguments rule)) - where rgraph = rulegraph rule - -/* -`Findpattern pattern rule residuroot transformation trace' bepaalt of -een instance van `pattern' voorkomt in een residu van `residuroot' in de -`trace'. - -Omwille van optimalisatie worden, met behulp van `transformation' en -`rule', alleen nieuw toegevoegde nodes na een rewrite in de trace -bekeken. De rest is toch niet veranderd. -*/ - -findpattern :: (Graph sym var2,var2) [var] var (Transformation sym var pvar) -> Bool | == sym & == var & == var2 & == pvar - -findpattern pattern thespinenodes residuroot transf -| isMember residuroot thespinenodes - = False // Root of residu no longer in spine - must have come to RNF. - -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]] - = True - where graph = rulegraph rule - fp residuroot trace = findpattern` pattern residuroot trace - redirect = adjust (last thespinenodes) reductroot id - -findpattern pattern thespinenodes residuroot (Instantiate ipattern yestrace notrace) -= findpattern` pattern residuroot yestrace || findpattern` pattern residuroot notrace - -findpattern pattern thespinenodes residuroot (Annotate trace) -= findpattern` pattern residuroot trace - -findpattern pattern thespinenodes residuroot Stop -= False - - -findpattern` :: (Graph sym var2,var2) var (Trace sym var pvar) -> Bool | == sym & == var & == var2 & == pvar - -findpattern` pattern residuroot (Trace stricts rule answer history transf) -= findpattern pattern thespinenodes residuroot transf - where thespinenodes = foldoptional [] spinenodes answer - -/* -`Getdeltanodes spine' is the list of nodes in the spine that we don't -want to introduce new functions for because they contain a delta symbol -or a strict argument. -*/ - -getdeltanodes :: - (Spine sym var pvar) - -> [var] - -getdeltanodes spine -= foldspine pair none (True,[]) force none (const none) partial (const none) redex none spine - where pair node (forced,nodes) = if forced [node:nodes] nodes - none = (False,[]) - 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: " /* <<< toString (rgraphroot pat) <<< " =?= " */ <<< pat <<< nl - <<< "Match succes:" <<< nl - <<< yesbody - <<< "Match failure:" <<< nl - <<< nobody - (<<<) file (BuildGraph rgraph) - = file <<< "Build: " <<< toString rgraph <<< nl - -printfuncdef :: (sym->String) (var->String) (FuncDef sym var) *File -> .File | == var -printfuncdef showsym showvar funcdef file -= printfuncbody showsym showvar "" body (file <<< "Arguments: " <<< showlist showvar args <<< nl) - where (args,body) = funcdef - -printfuncbody :: (sym->String) (var->String) String (FuncBody sym var) *File -> .File | == var -printfuncbody showsym showvar indent (MatchPattern pattern yesbody nobody) file0 -= file3 - where file3 = printfuncbody showsym showvar indent nobody (file2 <<< indent <<< "Otherwise:" <<< nl) - file2 = printfuncbody showsym showvar (indent+++" ") yesbody file1 - file1 = file0 <<< indent <<< "Match " <<< showvar (rgraphroot pattern) <<< " =?= " <<< showrgraph showsym showvar pattern <<< nl -printfuncbody showsym showvar indent (BuildGraph replacement) file0 -= file1 - where file1 = file0 <<< indent <<< showrgraph showsym showvar replacement <<< nl diff --git a/sucl/newtest.icl b/sucl/newtest.icl deleted file mode 100644 index f7e2787..0000000 --- a/sucl/newtest.icl +++ /dev/null @@ -1,568 +0,0 @@ -implementation module newtest - -// $Id$ - -import cli -import coreclean -import newfold -import complete -import trd -import loop -import trace -import rule -import graph -import canon -import basic -import general -import StdEnv - -/* - -newtest.lit - Testing the new trace implementation -================================================== - -Description ------------ - -Describe in a few paragraphs what this module defines. - ------------------------------------------------------------- - -Interface ---------- - -Exported identifiers: - -> %export -> all || List of all clasp modules -> list || List a clean module -> listopt || List rules with introduction -> listfull || List full processing of optimization ->|| listtrace || List the trace for a clean module -> optfiles || Optimize files obeying a pattern -> optimize || Optimize a clean module - -Required types: - - identifier - type@source.lit type@source.lit - ... - ------------------------------------------------------------- - -Includes --------- - -> %include "dnc.lit" - -> %include "../src/basic.lit" -> %include "../src/hunt.lit" -> %include "../src/pfun.lit" -> %include "../src/graph.lit" -> %include "../src/rule.lit" -> %include "../src/trd.lit" -> %include "../src/spine.lit" -> %include "strat.lit" -> %include "trace.lit" -> %include "loop.lit" -> %include "../src/clean.lit" -> %include "../src/module.lit" -> %include "cli.lit" -> %include "../src/complete.lit" ->|| %include "fold.lit" -> %include "newfold.lit" -> %include "../src/canon.lit" - ------------------------------------------------------------- - -Implementation --------------- - ------------------------------------------------------------------------- - -> optfiles :: [char] -> [sys_message] -> optfiles -> = optimize.foldr addmodule [].glob.join ' '.expand [".cli"] (getpath ["."] "CLIPATH") - -> addmodule filename modules -> = subcli scont filename -> where subcli success ".cli" = success "" -> subcli success ('/':cs) = subcli scont cs -> subcli success (c:cs) = subcli (success.(c:)) cs -> subcli success cs = modules -> scont = (:modules) - -> all = (foldr addmodule [].glob.join ' '.expand [".cli"] (getpath ["."] "CLIPATH")) "*" - -> optimize :: [[char]] -> [sys_message] - -> optimize modules -> = complaints++loads++concat (map optone goodnames)++[Stdout "Done.\n",Exit (#complaints)] -> where allnames = [(module,findfiles readable [".cli"] (getpath ["."] "CLIPATH") module)|module<-modules] -> badnames = [module|(module,[])<-allnames] -> goodnames = [(module,cliname,init cliname++"o")|(module,cliname:clinames)<-allnames] -> complaints -> = [], if badnames=[] -> = [Stderr ("Warning: cannot find module"++showmodules badnames++" (ignored).\n")], otherwise -> where showmodules [module] -> = ": "++showstring module -> showmodules modules -> = "s: "++join ',' (map showstring modules) -> loads -> = [], if goodnames=[] -> = [Stdout ("Loaded modules: "++join ',' [module|(module,cli,clo)<-goodnames]++".\n")], otherwise -> cli = loadclis (map snd3 goodnames) -> optone (module,cliname,cloname) -> = [ Stdout ("Optimizing "++module++" ("++showstring cliname++") to "++show cloname++"..."), -> Tofile cloname (listnew module cli), -> Stdout "\n" -> ] - ------------------------------------------------------------------------- - -`Newfunction' is the type of a new function produced by symbolic -reduction applied to a cli module. Symbolic reduction on a cli module -actually produces a list of new functions. - -> newfunction * ** **** ***** -> == ( *, || Assigned symbol of the new function -> rule * **, || Initial rule of the new function -> [bool], || Strictness annotations -> rule **** *****, || Type rule -> bool, || Export annotation -> [rule * **], || Rewrite rules -> bool || Import annotation -> ) - -`Symredresult' is the output produced by symbolic reduction applied to -an area. Symbolic reduction on an area actually produces a list of -these tuples. - -> symredresult * ** **** ***** -> == ( rgraph * **, || The initial area in canonical form -> *, || The assigned symbol -> [bool], || Strictness annotations -> rule **** *****, || Type rule -> trace * ** **, || Truncated and folded trace -> [rule * **], || Resulting rewrite rules -> [rgraph * **] || New areas for further symbolic reduction (not necessarily canonical) -> ) -*/ - -:: Symredresult sym var tsym tvar - = { srr_task_expression :: Rgraph sym var // The initial area in canonical form - , srr_assigned_symbol :: sym // The assigned symbol - , srr_strictness :: [Bool] // Strictness annotations - , srr_arity :: Int // Arity - , srr_typerule :: Rule tsym tvar // Type rule - , srr_trace :: Trace sym var var // Truncated and folded trace - , srr_function_def :: FuncDef sym var // Resulting rewrite rules - , 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 & Eq var -where toString srr - = "Task: "+++toString srr.srr_task_expression+++ - "\nSymbol: "+++toString srr.srr_assigned_symbol+++ - "\nStrictness: "+++listToString srr.srr_strictness+++ - "\nArity: "+++toString srr.srr_arity+++ - "\nTyperule: "+++"<typerule>"+++ - "\nTrace: "+++"<trace>"+++ - "\nFunction definition: "+++"<funcdef>"+++ - "\nAreas: "+++listToString srr.srr_areas+++"\n" - -instance <<< (Symredresult sym var tsym tvar) | toString sym & <<<,==,toString var -where (<<<) file0 srr - = file7 - 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 - file4 = printfuncdef toString toString srr.srr_function_def file3 - file5 = file4 <<< "Areas:" <<< nl - file6 = printareas toString toString " " srr.srr_areas file5 - file7 = file6 <<< "==[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 - -/* -> listopt :: [char] -> [[char]] -> [char] - -> listopt main = listnew main.loadclis - -> listnew :: [char] -> cli -> [char] - -> listnew main cli = (lay.printnew cli.map (makenew cli).filter hasusersym.fullsymred main.stripexports main) cli - -> printnew -> :: cli -> -> [newfunction symbol node typesymbol typenode] -> -> [[char]] - -> printnew cli results -> = (implementation exports++"MODULE "++modulename++";"): -> prefix [""] (showimports [symbol|(symbol,initialrule,stricts,trule,exported,rules,True)<-results])++ -> showtypes ((map (uncurry cleanalias).aliases) cli) (map (printalgebra (typerule cli)) (constrs cli))++ -> prefix ["","MACRO"] ((concat.map (uncurry cleanmacro).macros) cli)++ -> concat (map (shownewrules cli) [(symbol,initialrule,(trule,stricts),rules)|(symbol,initialrule,stricts,trule,exported,rules,imported)<-results;rules~=[]]) -> where exports = [symbol|(symbol,initialrule,stricts,trule,True,rules,imported)<-results] -> implementation [User module "Start"] = "" -> implementation exports = "IMPLEMENTATION " -> getmodule (User module ident) = module -> modulename = hd (map getmodule exports++["empty"]) - -> showimports symbols -> = map showblock (partition getmodule getident symbols) -> where getmodule (User module ident) = module -> getident (User module ident) = ident -> showblock (module,idents) -> = "FROM "++module++" IMPORT "++join ',' idents++";" - -> showtypes aliastexts algebralines -> = prefix ["","TYPE"] (prefix [""] (concat aliastexts)++prefix [""] algebralines) - -> prefix xs [] = [] -> prefix xs ys = xs++ys - -> shownewrules cli (symbol,initialrule,tinfo,rules) -> = prefix ("":"<<":cleanrule symbol initialrule++[">>","RULE"]) (cleantyperule symbol tinfo:concat (map (cleanrule symbol) rules)) - -> makenew -> :: cli -> -> symredresult symbol node typesymbol typenode -> -> newfunction symbol node typesymbol typenode - -> makenew cli (area,symbol,stricts,trule,Trace initialstricts initialrule answer history results,rules,areas) -> = (symbol,initialrule,stricts,trule,exported,rules',imported) -> where exported = member (exports cli) symbol -> imported = member (imports cli) symbol -> rules' = filter ((~).unchanged) rules -> unchanged rule -> = def & root=initialroot & sym=symbol -> where root = rhs rule; graph = rulegraph rule -> (def,(sym,args')) = dnc (const "in makenew") graph root -> initialroot = rhs initialrule - -> hasusersym -> :: symredresult symbol node typesymbol typenode -> -> bool - -> hasusersym (area,symbol,stricts,trule,trace,rules,areas) = usersym symbol - ------------------------------------------------------------------------- - -> listfull :: [char] -> [[char]] -> [char] -> listfull main filenames -> = (lay.map (showfull cli).fullsymred main) cli -> where cli = stripexports main (loadclis (main:filenames)) - -> showfull -> :: cli -> -> symredresult symbol node typesymbol typenode -> -> [char] - -> showfull cli (area,symbol,stricts,trule,trace,rules,areas) -> = hline++ -> "::: AREA :::\n"++ -> printrgraph showsymbol shownode area++ -> "\n\n::: ASSIGNED SYMBOL :::\n"++ -> showsymbol symbol++ -> "\n\n::: DERIVED TYPE RULE :::\n"++ -> printrule showtypesymbol showtypenode trule++ -> "\n\n::: TRACE :::\n"++ -> lay (printtrace symbol showsymbol shownode shownode trace)++ -> "\n\n::: DERIVED STRICTNESS :::\n"++ -> map strictchar stricts++ -> "\n::: RULES :::\n"++ -> lay (map (((showsymbol symbol++" ")++).printrule showsymbol shownode) rules)++ -> "\n::: NEW AREAS :::\n"++ -> lay (map (printrgraph showsymbol shownode) areas)++ -> hline - -> hline = rep 72 '='++"\n" - -> fullsymred -> :: [char] -> -> cli -> -> [symredresult symbol node typesymbol typenode] - -> fullsymred main cli -> = results -> where results = depthfirst generate process (initareas cli) -> generate result = map canonise' (getareas result) -> process area = symredarea foldarea' cli area - -> foldarea' = foldarea (labelarea'.canonise') -> labelarea' = labelarea (map getinit results) (newsymbols main) -> canonise' = canonise (typerule cli) heap -*/ - -fullsymred :: - [SuclSymbol] // Fresh function symbols - Cli // Module to optimise - -> [Symredresult SuclSymbol SuclVariable SuclTypeSymbol SuclTypeVariable] - -fullsymred freshsymbols cli - = results - where results = depthfirst generate process (initareas cli) - generate result = map canonise` (getareas result) - process area = symredarea foldarea` cli area - - foldarea` = foldarea (labelarea` o canonise`) - labelarea` = labelarea isSuclUserSym (map getinit results) freshsymbols - canonise` = canonise (arity cli) suclheap - -isSuclUserSym (SuclUser _) = True -isSuclUserSym _ = False - -/* -`Initareas cli' is the list of initial rooted graphs that must be -symbolically reduced. An initial rooted graph is formed by applying an -exported symbol to its full complement of open arguments according to -its type rule. - -> initareas :: cli -> [rgraph symbol node] - -> initareas cli -> = map (initialise heap) (exports cli) -> where initialise (root:nodes) symbol -> = mkrgraph root (updategraph root (symbol,args) emptygraph) -> where args = map2 const nodes targs -> targs = lhs (typerule cli symbol) - -> getinit :: symredresult * ** **** ***** -> rgraph * ** -> getinit (area,symbol,stricts,trule,trace,rules,areas) = area - -> getareas :: symredresult * ** **** ***** -> [rgraph * **] -> getareas (area,symbol,stricts,trule,trace,rules,areas) = areas -*/ - -initareas :: Cli -> [Rgraph SuclSymbol SuclVariable] -initareas cli -= map (initialise suclheap) (exports cli) - where initialise [root:nodes] symbol - = mkrgraph root (updategraph root (symbol,args) emptygraph) - where args = map2 const nodes targs - targs = arguments (typerule cli symbol) - -getinit :: (Symredresult sym var tsym tvar) -> Rgraph sym var -getinit srr -= srr.srr_task_expression - -getareas :: (Symredresult sym var tsym tvar) -> [Rgraph sym var] -getareas srr -= srr.srr_areas - -/* -`Symredarea' is the function that does symbolic reduction of a single -area. - -> symredarea -> :: (rgraph symbol node->(symbol,[node])) -> -> cli -> -> rgraph symbol node -> -> symredresult symbol node typesymbol typenode - -> symredarea foldarea cli area -> = (area,symbol,stricts,trule,trace,rules,areas) -> where agraph = rgraphgraph area; aroot = rgraphroot area -> (symbol,aargs) = foldarea area -> arule = mkrule aargs aroot agraph -> trule = ruletype typeheap (ctyperule FN typeheap (typerule cli)) arule -> trace = loop strategy' complete' matchable' (heap--nodelist agraph [aroot],arule) -> (stricts,rules,areas) = fullfold (trc symbol) foldarea symbol trace -> complete' = (~).converse matchable' (mkrgraph () emptygraph) -> matchable' = matchable (complete cli) -> strategy' = clistrategy cli -*/ - -:: Unit = Unit - -symredarea :: - ((Rgraph SuclSymbol SuclVariable)->(SuclSymbol,[SuclVariable])) - Cli - (Rgraph SuclSymbol SuclVariable) - -> Symredresult SuclSymbol SuclVariable SuclTypeSymbol SuclTypeVariable - -symredarea foldarea cli area -= { srr_task_expression = area - , srr_assigned_symbol = symbol - , srr_strictness = stricts - , srr_arity = length aargs - , srr_typerule = trule - , srr_trace = trace - , srr_function_def = rules - , srr_areas = areas - } - 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` (suclheap--varlist agraph [aroot],arule) - (stricts,rules,areas) = fullfold (trc symbol) foldarea symbol trace - matchable` = matchable (complete cli) - strategy` = clistrategy cli - -/* -> trc :: symbol -> trace symbol node node -> rgraph symbol node -> bool -> bool - -> trc symbol trace area recursive -> = error (lay ("Trace is recursive in area":printrgraph showsymbol shownode area:printtrace symbol showsymbol shownode shownode trace)), if esymbol symbol & recursive -> = recursive, otherwise -*/ - -trc symbol trace area recursive = recursive - -/* -> esymbol (User m "E") = True -> esymbol symbol = False - ------------------------------------------------------------------------- - -> printelem symbol (result,optsra) -> = ( indent "subtrace: " (printresult symbol showsymbol shownode shownode result)++ -> foldoptional [] printsra optsra -> ) - -> printsra (stricts,rules,areas) -> = ( ("stricts: "++map strictchar stricts): -> indent "rules: " (map (showrule showsymbol shownode) rules)++ -> indent "areas: " (map (showrgraph showsymbol shownode) areas) -> ) - -> printsras (strictss,rules,areas) -> = ( showlist (showstring.map strictchar) strictss: -> indent "rules: " (map (showrule showsymbol shownode) rules)++ -> indent "areas: " (map (showrgraph showsymbol shownode) areas) -> ) - -> trsym (User module "New_ab") = True -> trsym = const False - -> looping :: * -> rule * ** -> bool -> looping symbol rule -> = rdef & rsym=symbol & rargs=args -> where args = lhs rule; root = rhs rule; graph = rulegraph rule -> (rdef,(rsym,rargs)) = dnc (const "in looping") graph root - ------------------------------------------------------------------------- - - listtrace :: [char] -> [[char]] -> [char] - listtrace main = lay.map clitraces.mktraces.stripexports main.loadclis.(main:) - -> clitraces :: (symbol,(trace symbol node node,[rule symbol node])) -> [char] -> clitraces (sym,(trace,rules)) = lay (printtrace sym showsymbol shownode shownode trace) - - mktraces :: cli -> [(symbol,(trace symbol node node,[rule symbol node]))] - mktraces cli - = depthfirst - ( foldr addsymbols []. - snd. - snd - ) - (pairwith clisymred') - (exports cli) - where clisymred' symbol - = clisymred ((~=hd heap).rhs) cli symbol (initrule heap (lhs.typerule cli) symbol) - -> addsymbols :: rule * *** -> [*] -> [*] -> addsymbols rule rest -> = foldr (addsymbol.dnc (const "in addsymbols") rgraph) rest nodes -> where nodes = nodelist rgraph (rroot:lroots) -> rgraph = rulegraph rule -> rroot = rhs rule -> lroots = lhs rule -> addsymbol (def,(sym,args)) = cond def (sym:) id - ------------------------------------------------------------------------- - -> list :: [char] -> [[char]] -> [char] - -> list main = showcli.stripexports main.loadclis.(main:) - ------------------------------------------------------------------------- - - clisymred :: (rule symbol **->bool) -> cli -> symbol -> ([**],rule symbol **) -> (trace symbol ** node,[rule symbol **]) - - clisymred unchanged cli symbol rule - = ( mapsnd (filter unchanged) - . pairwith tips - . onresults (foldtrace symbol) - . loop strategy' complete' matchable' - ) rule - where complete' - = (~).converse matchable' (mkrgraph () emptygraph) - matchable' = matchable (complete cli) - strategy' = clistrategy cli - -> matchable :: ([*]->bool)->[rgraph * ***]->rgraph * **->bool - -> matchable complete patterns rgraph -> = ~coveredby complete (rgraphgraph rgraph) [(rgraphgraph pattern,[rgraphroot pattern])|pattern<-patterns] [rgraphroot rgraph] -*/ - -matchable :: - ([sym]->Bool) - [Rgraph sym pvar] - (Rgraph sym var) - -> Bool - | == sym - & == var - & == pvar -matchable complete patterns rgraph -= not (coveredby complete (rgraphgraph rgraph) [(rgraphgraph pattern,[rgraphroot pattern]) \\ pattern<-patterns] [rgraphroot rgraph]) - -/* ------------------------------------------------------------------------- - -`Ctyperule' cli (sym,args)' is the typerule of an occurrence of symbol -sym with the given arguments, curried if there are too few. - -> ctyperule -> :: **** -> -> [*****] -> -> (*->rule **** *****) -> -> (*,[**]) -> -> rule **** ***** - -> ctyperule fn typeheap typerule (sym,args) -> = mkrule targs' troot' tgraph' -> where targs = lhs trule; troot = rhs trule; tgraph = rulegraph trule -> trule = typerule sym -> (targs',targs'') = claim args targs -> (troot',tgraph',theap') = foldr build (troot,tgraph,typeheap--nodelist tgraph (troot:targs)) targs'' -> build targ (troot,tgraph,tnode:tnodes) -> = (tnode,updategraph tnode (fn,[targ,troot]) tgraph,tnodes) -*/ - -ctyperule :: - (Int -> tsym) // The arrow type symbol for functions of given arity - [tvar] // Fresh type variables - (sym->Rule tsym tvar) // Type rule of a symbol - (sym,[var]) // Node to abstract - -> Rule tsym tvar - | == tvar - -ctyperule fn typeheap typerule (sym,args) -= mkrule targs` troot` tgraph` - where targs = arguments trule; troot = ruleroot trule; tgraph = rulegraph trule - trule = typerule sym - (targs`,targs``) = claim args 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) - -/* -> newsymbols main = map (User main.("New_"++)) identifiers -*/ diff --git a/sucl/pfun.dcl b/sucl/pfun.dcl deleted file mode 100644 index 2f68103..0000000 --- a/sucl/pfun.dcl +++ /dev/null @@ -1,58 +0,0 @@ -definition module pfun - -// $Id$ - -from StdString import toString -from StdOverloaded import == -from cleanversion import String - -// Partial function abstract type -:: Pfun dom ran - -// The empty partial function -emptypfun :: .Pfun .dom .ran - -// Extend a partial function -extend :: .dom .ran (Pfun .dom .ran) -> Pfun .dom .ran - -// Restrict a partial function (take away one mapping) -restrict :: .dom (Pfun .dom .ran) -> Pfun .dom .ran - -// Overwrite partial function with a new one -// first arg is the new p.f. -// second arg is overwritten -overwrite :: !(Pfun .dom .ran) (Pfun .dom .ran) -> (Pfun .dom .ran) - -// Modify a partial function by applying a function to all its results -postcomp :: (.ran1 -> .ran2) !(Pfun .dom .ran1) -> Pfun .dom .ran2 - -// Build a total function from a partial one by supplying a default value -total :: .ran !(Pfun dom .ran) dom -> .ran | == dom - -// Apply partial function with a default value -foldpfun :: (.ran1 -> .ran2) .ran2 !(Pfun dom .ran1) dom -> .ran2 | == dom - -// Domain restriction of a partial function -domres :: !.[dom] .(Pfun dom ran) -> Pfun dom ran | == dom - -// Apply a partial function to an argument -// getting a result that may fail -apply :: !(Pfun dom .ran) dom -> (.Bool,.ran) | == dom - -// Partial functions are printable -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. -*/ -idpfun :: !.[dom] .(Pfun dom dom) -> Bool | == dom - -instance == (Pfun dom ran) | == dom & == ran diff --git a/sucl/pfun.icl b/sucl/pfun.icl deleted file mode 100644 index 0fabaff..0000000 --- a/sucl/pfun.icl +++ /dev/null @@ -1,105 +0,0 @@ -implementation module pfun - -// $Id$ - -import basic -import StdEnv - -/* - -pfun.lit - Partial functions -============================ - -Description ------------ - -This script implements an abstract type for partial functions and useful -operations on them. - -Implementation --------------- - -*/ - -:: Pfun dom ran - = EmptyPfun - | Extend dom ran (Pfun dom ran) - | Restrict dom (Pfun dom ran) - -emptypfun :: .Pfun .dom .ran -emptypfun = EmptyPfun - -extend :: .dom .ran (Pfun .dom .ran) -> Pfun .dom .ran -extend arg res pfun = Extend arg res pfun - -restrict :: .dom (Pfun .dom .ran) -> Pfun .dom .ran -restrict arg pfun = Restrict arg pfun - -overwrite :: !(Pfun .dom .ran) (Pfun .dom .ran) -> (Pfun .dom .ran) -overwrite EmptyPfun old = old -overwrite (Extend org img new) old = Extend org img (overwrite new old) -overwrite (Restrict org new) old = Restrict org (overwrite new old) - -postcomp :: (.ran1 -> .ran2) !(Pfun .dom .ran1) -> Pfun .dom .ran2 -postcomp f EmptyPfun = EmptyPfun -postcomp f (Extend x y p) = Extend x (f y) (postcomp f p) -postcomp f (Restrict x p) = Restrict x (postcomp f p) - -total :: .ran !(Pfun dom .ran) dom -> .ran | == dom -total def EmptyPfun arg = def -total def (Extend x y p) arg -| arg==x = y - = total def p arg -total def (Restrict x p) arg -| arg==x = def - = total def p arg - -// Apply partial function with a default value -foldpfun :: (.ran1 -> .ran2) .ran2 !(Pfun dom .ran1) dom -> .ran2 | == dom -foldpfun found notfound pfun arg - = total notfound (postcomp found pfun) arg - -domres :: !.[dom] .(Pfun dom ran) -> Pfun dom ran | == dom -domres domain oldpfun -= foldr adddom emptypfun domain - where adddom org = total id (postcomp (extend org) oldpfun) org - -apply :: !(Pfun dom .ran) dom -> (.Bool,.ran) | == dom -apply pfun arg -= total (False,baddomain) (postcomp s pfun) arg - where s x = (True,x) - baddomain = abort "apply: partial function applied outside domain" - -instance toString Pfun dom ran | toString dom & toString ran & == dom -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 = [] -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 -= all idelem domain - where idelem x = total True (postcomp ((==) x) pfun) x - -instance == (Pfun dom ran) | == dom & == ran -where (==) EmptyPfun EmptyPfun = True - (==) (Extend x1 y1 pf1) (Extend x2 y2 pf2) - = x1==x2 && y1==y2 && pf1==pf2 - (==) (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/pretty.dcl b/sucl/pretty.dcl deleted file mode 100644 index e781352..0000000 --- a/sucl/pretty.dcl +++ /dev/null @@ -1,32 +0,0 @@ -definition module pretty - -// $Id$ - -from StdFile import <<< -from StdString import String - -/* Pretty printing - =============== - - We don't want to have to concatenate strings all the time. - - Here's a puny data structure for pretty printing. - It's relatively easy to generate, fits most needs. - - The idea is to generate this once, and then run along it once - as the constituent strings are written to an output file. - -*/ - -:: Layout - = Line String // A single line - | Indent String [Layout] // A sequence of lines, the first of which is indented by a string (and the rest by an equivalent number of spaces) - -class Pretty t -where pretty :: t -> Layout - -// We can pretty-print strings (and via it everything that can be written as a string). -instance Pretty {#Char} - -// Layout structures can be written to a file. -instance <<< Layout diff --git a/sucl/pretty.icl b/sucl/pretty.icl deleted file mode 100644 index af3112d..0000000 --- a/sucl/pretty.icl +++ /dev/null @@ -1,134 +0,0 @@ -implementation module pretty - -// $Id$ - -import StdEnv - -:: Layout - = Line String // A single line - | Indent String [Layout] // A sequence of lines, the first of which is indented by a string (and the rest by an equivalent number of spaces) - -class Pretty t -where pretty :: t -> Layout - -instance Pretty {#Char} -where pretty s = Line s - -instance <<< Layout -where <<< f l - = printlayout l cont True [] f - where cont first prefixes f = f - -printlayout (Line s) cont first is f -= cont False (if first (asspaces is) is) ((printindents is f) <<< s) -printlayout (Indent i ls) cont first is f -= foldr printlayout cont` ls True [i:is] f - where cont` first` is` f` - = cont first is f` - -asspaces is = [toString (spaces (sum (map size is)))] - -printindents is f -= foldr printindent f is -printindent i f = f<<<i - -/* - -> %include "basic.lit" -> %include "graph.lit" -extgraph -> %include "rule.lit" -> %include "clean.lit" -cleanrule -cleantyperule -coretyperule -symbolmodule -typesymbolmodule - ------------------------------------------------------------------------- - -Get the Select nodes from a graph. - -> getselectnodes :: graph symbol ** -> ** -> [((**,num),(num,**))] - -> getselectnodes graph root -> = foldr (withmeta (nodecontents graph) addselectnode) [] (nodelist graph [root]) -> where addselectnode (True,(Select arity index,[tuplenode])) selectnode -> = (((tuplenode,arity),(index,selectnode)):) -> addselectnode contents node = id - -Distribute the Select nodes over their indexes. - -> splitselectnodes :: ((**,num),[(num,**)]) -> (**,[[**]]) - -> splitselectnodes ((tuplenode,arity),selects) -> = (tuplenode,foldr dist (rep arity []) selects) -> where dist (1,selectnode) (ns:nss) = (selectnode:ns):nss -> dist (index,selectnode) (ns:nss) = ns:dist (index-1,selectnode) nss - -Make left hand sides. - -> makelhss :: [**] -> [[**]] -> ([**],[[**]]) - -> makelhss heap nss -> = (heap,[]), if empty -> = (heap'',ns':nss''), otherwise -> where (heap'',nss'') = makelhss heap' nss' -> (empty,ns',heap',nss') = heads heap nss -> heads heap [] = (True,[],heap,[]) -> heads (node:heap) ([]:nss) -> = (empty,node:ns',heap',[]:nss') -> where (empty,ns',heap',nss') = heads heap nss -> heads heap ((n:ns):nss) -> = (False,n:ns',heap',ns:nss') -> where (empty,ns',heap',nss') = heads heap nss - -> makenodedefs :: [**] -> [(**,[[**]])] -> [(**,[**])] - -> makenodedefs heap [] -> = [] -> makenodedefs heap ((tuplenode,nss):rest) -> = map (pair tuplenode) lhss++nodedefs -> where (heap',lhss) = makelhss heap nss -> nodedefs = makenodedefs heap' rest - - - -> pretty :: symbol -> rule symbol node -> [[char]] - -> pretty symbol rule -> = (showsymbol symbol++' ':concat (map ((++" ").fst) argreprs)++"-> "++snd rootrepr): -> map2 shownodedef nodedefs (map snd tuplereprs) -> where args = lhs rule; root = rhs rule; graph = rulegraph rule -> nodedefs = makenodedefs (heap--nodelist graph (root:args)) tupleselections -> tupleselections -> = ( map splitselectnodes. -> partition fst snd -> ) (getselectnodes graph root) -> tuplenodes = map fst tupleselections -> prunedgraph = foldr prunegraph graph tuplenodes - -> [argreprs,[rootrepr],tuplereprs] -> = hof (foldgraph prettyref (issafe.shownode) prettydef prunedgraph) [args,[root],map fst nodedefs] -> where prettyref node (saferef,unsaferef) = issafe (shownode node++':':saferef) - -> shownodedef (tuplenode,selectnodes) tuplerepr -> = ", ("++join ',' (map shownode selectnodes)++"): "++tuplerepr - ->issafe::[char]->([char],[char]) ->prettydef::symbol->[([char],[char])]->([char],[char]) - ------------------------------------------------------------------------- -Useful (higher order) functions. - -> withmeta :: (*->**) -> (**->*->***) -> * -> *** -> withmeta meta f x = f (meta x) x - -> pair :: * -> ** -> (*,**) -> pair x y = (x,y) - -> hof :: ([*]->[**]) -> [[*]] -> [[**]] -> hof f xss -> = claims xss (f (concat xss)) - -> claims :: [[*]] -> [**] -> [[**]] -> claims [] ys = [] -> claims (xs:xss) ys -> = zs:claims xss ys' -> where (zs,ys') = claim xs ys - -*/ diff --git a/sucl/rewr.dcl b/sucl/rewr.dcl deleted file mode 100644 index a36e550..0000000 --- a/sucl/rewr.dcl +++ /dev/null @@ -1,53 +0,0 @@ -definition module rewr - -// $Id$ - -from rule import Rule -from graph import Graph -from pfun import Pfun -from StdOverloaded import == - -// Unfold a rewrite rule -xunfold - :: var - (Rule sym pvar) - !( [var] - , var - , Graph sym var - , Pfun pvar var - ) - -> ( [var] - , var - , Graph sym var - , Pfun pvar var - ) | == var & == pvar - -foldfn - :: (Pfun pvar var) // Matching of replacement - sym // Symbol at root of pattern - [pvar] // Arguments of pattern - pvar // Root of replacement - (Graph sym var) // Subject graph - -> Graph sym var // Folded subject - | == pvar - -getmapping - :: tsym - (Graph sym pvar) - (Graph sym var) - !(pvar,var) - ((Pfun pvar var) -> tsym) - !(Pfun pvar var) - -> tsym - | == sym - & == var - & == pvar - -rewrinstantiate - :: .(Graph sym pvar) // Pattern to instantiate with - pvar // Root of the pattern - var // Open node to instantiate - (.[var],.Graph sym var) // Heap,graph - -> .([var],Graph sym var) // New heap,graph - | == var - & == pvar diff --git a/sucl/rewr.icl b/sucl/rewr.icl deleted file mode 100644 index 4b584ae..0000000 --- a/sucl/rewr.icl +++ /dev/null @@ -1,215 +0,0 @@ -implementation module rewr - -// $Id$ - -import rule -import graph -import pfun -import basic -import StdEnv - -/* - -Rewriting of graphs - -Exported identifiers: -\begin{description} -\item[\tt unfold] Apply a rewrite rule to a graph -\item[\tt xunfold] As {\tt unfold}, but also provides full matching - from the applied rule to the (resulting) subject - graph -\item[\tt fold] Apply a rewrite rule in reverse to a graph -\item[\tt instantiate] Instantiate a graph with a pattern -\end{description} - -Temporarily hidden: -\begin{description} -\item[\tt build] Build a copy of a graph -\end{description} - -Temporarily not exported: -\begin{description} -\item[\tt getmap] Determine mapping from one graph to another -\item[\tt existmap] Determine if a mapping from one graph to another exists -\end{description} - -> %export foldfn getmapping instantiate xunfold - - unfold - :: pfun *** ** -> || Mapping as result from match of lhs - rule * *** -> || Rule to unfold - ([**],graph * **,**) -> || Heap,graph,node - ([**],graph * **,**) || New heap,graph,node - -> xunfold -> :: ** -> || Root of the redex to unfold -> rule * *** -> || Rule to unfold by -> ( [**], || Unused heap -> **, || Root of subject -> graph * **, || Subject graph -> pfun *** ** || Matching of pattern from rule to subject -> ) -> -> ( [**], || Remaining heap -> **, || Possibly redirected root of subject -> graph * **, || Extended subject graph -> pfun *** ** || Extended matching from rule to subject -> ) - - fold - :: pfun *** ** -> || Mapping as result from match of rhs - rule * *** -> || Rule to fold - ([**],graph * **,**) -> || Heap,graph,node - ([**],graph * **,**) || New heap,graph,node - -> build -> :: graph * *** -> *** -> || Graph,root to be copied -> ([**],[**],graph * **,pfun *** **) -> || Heap,init nodes,init graph,init mapping -> ([**],[**],graph * **,pfun *** **) || New heap,new nodes,new graph,new mapping - -> getmap :: graph * *** -> *** -> graph * ** -> ** -> pfun *** ** - -> existmap :: graph * *** -> *** -> graph * ** -> ** -> bool - - -Implementation - -> %include "basic.lit" -> %include "pfun.lit" -> %include "graph.lit" -instantiate -> %include "rule.lit" - -*/ - -xunfold - :: var - (Rule sym pvar) - !( [var] - , var - , Graph sym var - , Pfun pvar var - ) - -> ( [var] - , var - , Graph sym var - , Pfun pvar var - ) | == var & == pvar - -xunfold redexroot rule (heap,root,subject,matching) -= (heap`,redirection root,redirectgraph redirection subject`,matching`) - where (heap`,[rhs`:_],subject`,matching`) - = build (rulegraph rule) (ruleroot rule) (heap,[],subject,matching) - redirection = adjust redexroot rhs` id - -rewrinstantiate - :: .(Graph sym pvar) // Pattern to instantiate with - pvar // Root of the pattern - var // Open node to instantiate - (.[var],.Graph sym var) // Heap,graph - -> .([var],Graph sym var) // New heap,graph - | == var - & == pvar - -rewrinstantiate pattern proot node (heap,graph) -| not closed -= (heap,graph) -= (heap``,graph``) - where (heap``,params``,graph``,_) - = foldr (build pattern) (heap,[],graph`,extend proot node emptypfun) params - (closed,(f,params)) = varcontents pattern proot - graph` = updategraph node (f,params``) graph - -build - :: (Graph sym pvar) - pvar - ( [var] - , [var] - , Graph sym var - , !Pfun pvar var - ) - -> ( [var] - , [var] - , Graph sym var - , Pfun pvar var - ) | == var & == pvar - -build pattern node (heap,nodes,graph,mapping) -| seen -= (heap,[seenas:nodes],graph,mapping) -| not closed -= (heap`,[node`:nodes],graph,mapping`) -= (heap``,[node`:nodes],graph``,mapping``) - where (seen,seenas) = apply mapping node - [node`:heap`] = heap - mapping` = extend node node` mapping - (closed,(f,params)) = varcontents pattern node - (heap``,params``,graph``,mapping``) - = foldr (build pattern) (heap`,[],graph`,mapping`) params - graph` = updategraph node` (f,params``) graph - -/* -Mapping - -> getmap pattern patnode graph node -> = getmapping nomatch pattern graph (patnode,node) id emptypfun -> where nomatch = error "getmap: pattern and graph do not match" - -> existmap pattern patnode graph node -> = getmapping False pattern graph (patnode,node) (const True) emptypfun -*/ - -getmapping - :: tsym - (Graph sym pvar) - (Graph sym var) - !(pvar,var) - ((Pfun pvar var) -> tsym) - !(Pfun pvar var) - -> tsym - | == sym - & == var - & == pvar - -getmapping failure patgraph graph (patnode,node) success mapping -| seen -= if (seenas==node) (success mapping) failure -| not patdef -= success mapping` -| not (def && patfunc==func && eqlen patargs args) -= failure -= foldr (getmapping failure patgraph graph) success (zip2 patargs args) mapping` - where (seen,seenas) = apply mapping patnode - (patdef,(patfunc,patargs)) = varcontents patgraph patnode - (def,(func,args)) = varcontents graph node - mapping` = extend patnode node mapping - -/* -The foldfn operation folds an area of a graph back to a function call. -The following two conditions must be satisfied in order not to need a -heap of fresh nodes: - - 1: At least one node is freed by the fold operation to hold the root of - the redex. This is the root of the reduct; since it must be freed, - the rule that is folded by must not be a projection function; - - 2: No other new nodes are necessary. Therefore, all nodes of the - pattern of the rule that is folded by except the root must also - occur in the replacement. - -Furthermore, the pattern of the rule is only given by its root symbol -and its arguments; the arguments are open nodes. - -*/ - -foldfn - :: (Pfun pvar var) // Matching of replacement - sym // Symbol at root of pattern - [pvar] // Arguments of pattern - pvar // Root of replacement - (Graph sym var) // Subject graph - -> Graph sym var // Folded subject - | == pvar - -foldfn matching symbol arguments replacementroot sgraph -= updategraph (domatching replacementroot) (symbol,map domatching arguments) sgraph - where domatching = total nomatching matching - nomatching = abort "foldfn: no matching of argument of pattern" diff --git a/sucl/rule.dcl b/sucl/rule.dcl deleted file mode 100644 index 6f61f4c..0000000 --- a/sucl/rule.dcl +++ /dev/null @@ -1,83 +0,0 @@ -definition module rule - -// $Id$ - -from graph import Graph,Node -from StdOverloaded import ==,toString -from StdFile import <<< -from cleanversion import String -from StdClass import Eq - -// --- Exported types - -:: Rule sym var -:: Rgraph sym var - -// --- Functions on rules - -// Build a rule from its constituents -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 - -// 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 -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 -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 - -// Prune a rooted graph at a variable (making it free) -prunergraph :: var !.(Rgraph sym var) -> .Rgraph sym var - -// Get the root of a rooted graph -rgraphroot :: !.(Rgraph sym var) -> var - -// Get the graph part of a rooted graph -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 - -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 - -(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 deleted file mode 100644 index 21b7c06..0000000 --- a/sucl/rule.icl +++ /dev/null @@ -1,265 +0,0 @@ -implementation module rule - -// $Id$ - -import graph -import basic -import StdEnv - -:: Rule sym var - = RuleAlias [var] var (Graph sym var) - -:: Rgraph sym var - = RgraphAlias var (Graph sym var) - -/* - -rule.lit - Rooted graphs and rules -================================== - -Description ------------ - -This module implements abstract types for rooted graphs and rules, -together with some useful functions on them. Though very simple -definitions, it greatly helps the readability of error messages if -rooted graphs or rules occur in them. - -A rooted graph is a tuple consisting of a root and an unrooted graph -(how obvious). - -The implementation of a rule is less obvious. Instead of simply using a -graph with two roots, the root of the pattern and its associated -function symbol have been taken out. Hence the pattern is only -accessibly by its arguments. The root of the replacement is still -accessible. The reason for this is twofold: the root must be defined -anyway, and if the rule is a type rule, we are now able to use two -different domains for (normal) symbols and type symbols. - ------------------------------------------------------------- - -Interface ---------- - -Exported identifiers: - -> %export -> compilerule || Compile a rule from all loose parts -> emptyrgraph || Creates an empty rooted graph -> lhs || Determines the left root of a rule -> mkrgraph || Composes a rooted graph from a root and a graph -> mkrule || Composes a rule from left and right roots and a graph -> printrgraph || Makes a readable representation of a rooted graph -> printrule || Makes a readable representation of a rule -> prunergraph || Undefines the contents of a node of a rooted graph -> rgraph || Type of rooted graph over functorspace * and nodespace ** -> rgraphgraph || Determines the (unrooted) graph of a rooted graph -> rgraphroot || Determines the root of a rooted graph -> rhs || Determines the right root of a rule -> rule || Type of rules over functorspace * and nodespace ** -> rulegraph || Determines the graph of a rule -> showrgraph || Make a representation of a rooted graph -> showrule || Make a representation of a rule -> updatergraph || Updates the contents of a node of a rooted graph - -Required types: - - mkrgraph - graph@graph.lit - mkrule - graph@graph.lit - rgraphgraph - graph@graph.lit - rulegraph - graph@graph.lit - ------------------------------------------------------------- - -Includes --------- - -> %include "basic.lit" -> %include "graph.lit" -extgraph - ------------------------------------------------------------- - -Implementation --------------- - -> abstype rgraph * ** -> with emptyrgraph :: ** -> rgraph * ** -> updatergraph :: ** -> (*,[**]) -> rgraph * ** -> rgraph * ** -> prunergraph :: ** -> rgraph * ** -> rgraph * ** -> rgraphroot :: rgraph * ** -> ** -> rgraphgraph :: rgraph * ** -> graph * ** -> mkrgraph :: ** -> graph * ** -> rgraph * ** -> showrgraph :: (*->[char]) -> (**->[char]) -> rgraph * ** -> [char] -> printrgraph :: (*->[char]) -> (**->[char]) -> rgraph * ** -> [char] - -> abstype rule * ** -> with mkrule :: [**] -> ** -> graph * ** -> rule * ** -> lhs :: rule * ** -> [**] -> rhs :: rule * ** -> ** -> rulegraph :: rule * ** -> graph * ** -> showrule :: (*->[char]) -> (**->[char]) -> rule * ** -> [char] -> printrule :: (*->[char]) -> (**->[char]) -> rule * ** -> [char] - - -Rooted graphs - -> emptyrgraph root = (root,emptygraph) -> updatergraph node contents (root,graph) = (root,updategraph node contents graph) -> prunergraph node (root,graph) = (root,prunegraph node graph) -> rgraphroot (root,graph) = root -> rgraphgraph (root,graph) = graph -> mkrgraph root graph = (root,graph) -*/ - -emptyrgraph :: var -> .Rgraph sym var -emptyrgraph root = RgraphAlias root emptygraph - -updatergraph :: var .(Node sym var) !.(Rgraph sym var) -> .Rgraph sym var -updatergraph var node rgraph = maprgraph (mapsnd (updategraph var node)) rgraph - -prunergraph :: var !.(Rgraph sym var) -> .Rgraph sym var -prunergraph var rgraph = maprgraph (mapsnd (prunegraph var)) rgraph - -rgraphroot :: !.(Rgraph sym var) -> var -rgraphroot (RgraphAlias root _) = root - -rgraphgraph :: !.(Rgraph sym var) -> Graph sym var -rgraphgraph (RgraphAlias _ graph) = graph - -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 f (RgraphAlias root1 graph1) = RgraphAlias root2 graph2 - where (root2,graph2) = f (root1,graph1) - -instance toString (Rgraph sym var) | toString sym & toString var & Eq var -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) -> = 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) -> lhs (lroots,rroot,graph) = lroots -> rhs (lroots,rroot,graph) = rroot -> rulegraph (lroots,rroot,graph) = graph -*/ - -mkrule :: .[var] var (Graph sym var) -> .Rule sym var -mkrule args root graph = RuleAlias args root graph - -arguments :: !.(Rule sym var) -> [var] -arguments (RuleAlias args _ _) = args - -ruleroot :: !.(Rule sym var) -> var -ruleroot (RuleAlias _ root _) = root - -rulegraph :: !.(Rule sym var) -> Graph sym var -rulegraph (RuleAlias _ _ graph) = graph - -/* -> printrule showfunc shownode (lroots,rroot,graph) -> = (concat.map (++" ").init) reprs++"-> "++last reprs -> where reprs = printgraph showfunc shownode graph (lroots++[rroot]) - -> compilerule :: [**] -> ** -> [(**,(*,[**]))] -> rule * ** -> compilerule args root = mkrule args root.compilegraph - -*/ - -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 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) -/* -= 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 - -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/script.icl b/sucl/script.icl deleted file mode 100644 index 9be719c..0000000 --- a/sucl/script.icl +++ /dev/null @@ -1,15 +0,0 @@ -implementation module script - -// $Id$ - -/* - -%include "../src/clean.lit" - -cleanalias -cleanmacro -cleanrule -cleantype -cleantyperule - -corecomplete -coretypeinfo -coretyperule -heap - -readcleanparts -shownode -showsymbol -showtypenode - -showtypesymbol -symbolmodule -typeheap -typesymbolmodule - -usersym -%include "newtest.lit" - -*/ diff --git a/sucl/spine.dcl b/sucl/spine.dcl deleted file mode 100644 index c9aa361..0000000 --- a/sucl/spine.dcl +++ /dev/null @@ -1,229 +0,0 @@ -definition module spine - -// $Id$ - -from history import History,HistoryAssociation,HistoryPattern -from rule import Rgraph,Rule -from graph import Graph -from pfun import Pfun -from general import Optional -from StdOverloaded import == -from StdFile import <<< -from StdString import toString -from cleanversion import String - -/* - -spine.lit - The extended functional strategy -============================================ - -Description ------------ - -This script implements the strategy answer, and a function to compute it -for a given graph in a rewrite system. - -The strategy answer is a spine -- in principle a colon of partial -matches from patterns of rewrite rules to the graph, with at the bottom -the insteresting part: a redex, an open node or something else. See the -definition of subspine for that. - -The strategy function attempts to find a redex to reduce the graph to -normal form instead of root normal form. This is done by applying a -root normal form strategy recursively in preorder over the graph (of -course ignoring cycles). The node at which the root normal form -strategy was applied is returned in the strategy answer, so laziness can -be preserved. - ------------------------------------------------------------- - -Interface ---------- - -Exported identifiers: - -> %export -> answer || Strategy answer type -> foldspine || Higher order general spine folding -> ifopen || Check for answer indicating Open -> printanswer || Make a human-readable representation of an answer -> printspine || Make a human-readable representation of a spine -> showanswer || Make a representation of an answer -> showspine || Make a representation of a spine -> showsubspine || Make a representation of a subspine -> spine || Colon of partial matches -> spinenodes || Determine nodes in a spine -> spinetip || Determine bottom of spine -> subspine || Bottom of spine - -> history || Symbolic reduction history type -> printhistory || Make a human-readable representation of a history -> showhistory || Make a representation of a history - -Required types: - - subspine - rule@rule.lit,rgraph@rule.lit,pfun@pfun.lit - ------------------------------------------------------------- - -Includes --------- - -> %include "basic.lit" || optional -> %include "pfun.lit" || pfun -> %include "graph.lit" || graph -> %include "rule.lit" || rgraph rule - ------------------------------------------------------------- - -Implementation --------------- - - -Answer describes the answer of a strategy. Absence of a spine implies -that the node was in root normal form. - -> answer * ** *** == optional (spine * ** ***) - -> showanswer showa showb showc = showoptional (showspine showa showb showc) -> printanswer printa printb printc = foldoptional ["Rnf"] (printspine printa printb printc) - -*/ - -:: 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 -at which the strategy was applied, and the result for that node. - -> spine * ** *** == (**,subspine * ** ***) - -> showspine showa showb showc = showpair showb (showsubspine showa showb showc) - -> printspine printa printb printc -> = foldspine pair cycle delta force missingcase open partial unsafe redex strict -> where pair node (line,lines) = (printb node++" => "++line):lines -> cycle = ("Cycle",[]) -> delta = ("Delta",[]) -> force lines = ("Force",lines) -> missingcase = ("MissingCase",[]) -> open rgraph = ("Open "++printrgraph printa printc rgraph,[]) -> partial rule matching lines = ("Partial <fn> "++printrule printa printc rule++' ':printpfun printc printb matching,lines) -> unsafe rgraph = ("Unsafe "++printrgraph printa printb rgraph,[]) -> redex rule matching = ("Redex <fn> "++printrule printa printc rule++' ':printpfun printc printb matching,[]) -> strict = ("Strict",[]) - -*/ - -:: Spine sym var pvar - :== (var,Subspine sym var pvar) - -/* - -Subspine describes what was the result of the strategy applied to a node -in a graph. - -> subspine * ** *** -> ::= Cycle | || The spine contains a cycle -> Delta | || An imported (delta) rule was found -> Force (spine * ** ***) | || Global strictness annotation forced evaluation of a subgraph -> MissingCase | || All alternatives failed for a function symbol -> Open (rgraph * ***) | || Need root normal form of open node for matching -> Partial (rule * ***) (pfun *** **) (spine * ** ***) | || A rule was strictly partially matched -> Unsafe (rgraph * **) | || Terminated due to immininent recursion -> Redex (rule * ***) (pfun *** **) | || Total match -> Strict || Need root normal form due to strictness - -> showsubspine showa showb showc -> = sh -> where sh Cycle = "Cycle" -> sh Delta = "Delta" -> sh (Force spine) = "(Force "++showspine showa showb showc spine++")" -> sh MissingCase = "MissingCase" -> sh (Open rgraph) = "(Open "++showrgraph showa showc rgraph++")" -> sh (Partial rule matching spine) = "(Partial "++showrule showa showc rule++' ':showpfun showc showb matching++' ':showspine showa showb showc spine++")" -> sh (Unsafe rgraph) = "(Unsafe "++showrgraph showa showb rgraph++")" -> sh (Redex rule matching) = "(Redex "++showrule showa showc rule++' ':showpfun showc showb matching++")" -> sh Strict = "Strict" - - printsubspine printa printb printc - = pr - where pr Cycle = "Cycle" - pr Delta = "Delta" - pr (Force spine) = "(Force "++printspine printa printb printc spine++")" - pr MissingCase = "MissingCase" - pr (Open rgraph) = "(Open "++printrgraph printa printc rgraph++")" - pr (Partial rule matching spine) = "(Partial "++printrule printa printc rule++' ':printpfun printc printb matching++' ':printspine printa printb printc spine++")" - pr (Unsafe rgraph) = "(Unsafe "++printrgraph printa printb rgraph++")" - pr (Redex rule matching) = "(Redex "++printrule printa printc rule++' ':printpfun printc printb matching++")" - pr Strict = "Strict" - -*/ - -:: Subspine sym var pvar - = Cycle // The spine contains a cycle - | Delta // An imported (delta) rule was found - | Force Int (Spine sym var pvar) // Global strictness annotation forced evaluation of a subgraph at specified argument position - | MissingCase // All alternatives failed for a function symbol - | Open (Rgraph sym pvar) // Need root normal form of open node for matching - | Partial (Rule sym pvar) (Pfun pvar var) pvar (Spine sym var pvar) // A rule was strictly partially matched - | Unsafe (HistoryPattern sym var) // Terminated due to immininent recursion - | Redex (Rule sym pvar) (Pfun pvar var) // Total match - | Strict // Need root normal form due to strictness - -// Fold up a spine using a function for each constructor -foldspine - :: !(var .subresult -> .result) // Fold the spine itself - .subresult // Fold a Cycle subspine - .subresult // Fold a Delta subspine - (Int .result -> .subresult) // Fold a Force subspine - .subresult // Fold a MissingCase subspine - ((Rgraph sym pvar) -> .subresult) // Fold an Open subspine - ((Rule sym pvar) (Pfun pvar var) pvar .result -> .subresult) // Fold a Partial subspine - ((HistoryPattern sym var) -> .subresult) // Fold an Unsafe subspine - ((Rule sym pvar) (Pfun pvar var) -> .subresult) // Fold a Redex subspine - .subresult // Fold a Strict subspine - .(Spine sym var pvar) // The spine to fold - -> .result // The final result - -// Get the tip of a spine, -// i.e. the last part when all Partial's and Force's are stripped. -spinetip :: !(Spine sym var pvar) -> Spine sym var pvar - -// Get the main nodes of a spine, -// i.e. where the spine constructors are applied -// (not the matched nodes of partial matchings) -spinenodes :: .(Spine sym var pvar) -> [var] - -// Make a decision (continuation based) on whether a spine ends in Open -ifopen :: result result !.(Answer sym var pvar) -> result - -// Extend the history according to a spine -extendhistory - :: (Graph sym var) - (var -> var) - (Spine sym var pvar) - (History sym var) - -> History sym var - | == var - & == pvar - -(writeanswer) infixl :: *File (Answer sym var pvar) -> .File | toString sym & ==,toString,<<< var // & ==,toString,<<< pvar - -(writespine) infixl :: *File (Spine sym var pvar) -> .File | toString sym & ==,toString,<<< var // & ==,toString,<<< pvar - -instance <<< (Subspine sym var pvar) | toString sym & ==,toString,<<< var // & ==,toString,<<< pvar diff --git a/sucl/spine.icl b/sucl/spine.icl deleted file mode 100644 index cf81386..0000000 --- a/sucl/spine.icl +++ /dev/null @@ -1,381 +0,0 @@ -implementation module spine - -// $Id$ - -import history -import rule -import dnc -import graph -import pfun -import basic -from general import No,Yes -import StdEnv - -/* - -spine.lit - The extended functional strategy -============================================ - -Description ------------ - -This script implements the strategy answer, and a function to compute it -for a given graph in a rewrite system. - -The strategy answer is a spine -- in principle a colon of partial -matches from patterns of rewrite rules to the graph, with at the bottom -the insteresting part: a redex, an open node or something else. See the -definition of subspine for that. - -The strategy function attempts to find a redex to reduce the graph to -normal form instead of root normal form. This is done by applying a -root normal form strategy recursively in preorder over the graph (of -course ignoring cycles). The node at which the root normal form -strategy was applied is returned in the strategy answer, so laziness can -be preserved. - ------------------------------------------------------------- - -Interface ---------- - -Exported identifiers: - -> %export -> answer || Strategy answer type -> foldspine || Higher order general spine folding -> ifopen || Check for answer indicating Open -> printanswer || Make a human-readable representation of an answer -> printspine || Make a human-readable representation of a spine -> showanswer || Make a representation of an answer -> showspine || Make a representation of a spine -> showsubspine || Make a representation of a subspine -> spine || Colon of partial matches -> spinenodes || Determine nodes in a spine -> spinetip || Determine bottom of spine -> subspine || Bottom of spine - -> history || Symbolic reduction history type -> printhistory || Make a human-readable representation of a history -> showhistory || Make a representation of a history - -Required types: - - subspine - rule@rule.lit,rgraph@rule.lit,pfun@pfun.lit - ------------------------------------------------------------- - -Includes --------- - -> %include "basic.lit" || optional -> %include "pfun.lit" || pfun -> %include "graph.lit" || graph -> %include "rule.lit" || rgraph rule - ------------------------------------------------------------- - -Implementation --------------- - - -Answer describes the answer of a strategy. Absence of a spine implies -that the node was in root normal form. - -> answer * ** *** == optional (spine * ** ***) - -> showanswer showa showb showc = showoptional (showspine showa showb showc) -> printanswer printa printb printc = foldoptional ["Rnf"] (printspine printa printb printc) - -*/ - -:: 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 -at which the strategy was applied, and the result for that node. - -> spine * ** *** == (**,subspine * ** ***) - -> showspine showa showb showc = showpair showb (showsubspine showa showb showc) - -> printspine printa printb printc -> = foldspine pair cycle delta force missingcase open partial unsafe redex strict -> where pair node (line,lines) = (printb node++" => "++line):lines -> cycle = ("Cycle",[]) -> delta = ("Delta",[]) -> force lines = ("Force",lines) -> missingcase = ("MissingCase",[]) -> open rgraph = ("Open "++printrgraph printa printc rgraph,[]) -> partial rule matching lines = ("Partial <fn> "++printrule printa printc rule++' ':printpfun printc printb matching,lines) -> unsafe rgraph = ("Unsafe "++printrgraph printa printb rgraph,[]) -> redex rule matching = ("Redex <fn> "++printrule printa printc rule++' ':printpfun printc printb matching,[]) -> strict = ("Strict",[]) - -*/ - -:: 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 -in a graph. - -> subspine * ** *** -> ::= Cycle | || The spine contains a cycle -> Delta | || An imported (delta) rule was found -> Force (spine * ** ***) | || Global strictness annotation forced evaluation of a subgraph -> MissingCase | || All alternatives failed for a function symbol -> Open (rgraph * ***) | || Need root normal form of open node for matching -> Partial (rule * ***) (pfun *** **) (spine * ** ***) | || A rule was strictly partially matched -> Unsafe (rgraph * **) | || Terminated due to immininent recursion -> Redex (rule * ***) (pfun *** **) | || Total match -> Strict || Need root normal form due to strictness - -> showsubspine showa showb showc -> = sh -> where sh Cycle = "Cycle" -> sh Delta = "Delta" -> sh (Force spine) = "(Force "++showspine showa showb showc spine++")" -> sh MissingCase = "MissingCase" -> sh (Open rgraph) = "(Open "++showrgraph showa showc rgraph++")" -> sh (Partial rule matching spine) = "(Partial "++showrule showa showc rule++' ':showpfun showc showb matching++' ':showspine showa showb showc spine++")" -> sh (Unsafe rgraph) = "(Unsafe "++showrgraph showa showb rgraph++")" -> sh (Redex rule matching) = "(Redex "++showrule showa showc rule++' ':showpfun showc showb matching++")" -> sh Strict = "Strict" - - printsubspine printa printb printc - = pr - where pr Cycle = "Cycle" - pr Delta = "Delta" - pr (Force argno spine) = "(Force <argno> "++printspine printa printb printc spine++")" - pr MissingCase = "MissingCase" - pr (Open rgraph) = "(Open "++printrgraph printa printc rgraph++")" - pr (Partial rule matching spine) = "(Partial "++printrule printa printc rule++' ':printpfun printc printb matching++' ':printspine printa printb printc spine++")" - pr (Unsafe rgraph) = "(Unsafe "++printrgraph printa printb rgraph++")" - pr (Redex rule matching) = "(Redex "++printrule printa printc rule++' ':printpfun printc printb matching++")" - pr Strict = "Strict" - -*/ - -:: Subspine sym var pvar - = Cycle // The spine contains a cycle - | Delta // An imported (delta) rule was found - | Force Int (Spine sym var pvar) // Global strictness annotation forced evaluation of a subgraph at specified argument position - | MissingCase // All alternatives failed for a function symbol - | Open (Rgraph sym pvar) // Need root normal form of open node for matching - | Partial (Rule sym pvar) (Pfun pvar var) pvar (Spine sym var pvar) // A rule was strictly partially matched - | Unsafe (HistoryPattern sym var) // Terminated due to immininent recursion - | Redex (Rule sym pvar) (Pfun pvar var) // Total match - | Strict // Need root normal form due to strictness - -/* - -> foldspine -> :: (**->****->*****) -> -> **** -> -> **** -> -> (*****->****) -> -> **** -> -> (rgraph * ***->****) -> -> (rule * ***->pfun *** **->*****->****) -> -> (rgraph * **->****) -> -> (rule * ***->pfun *** **->****) -> -> **** -> -> spine * ** *** -> -> ***** - -> foldspine pair cycle delta force missingcase open partial unsafe redex strict -> = fold -> where fold (node,subspine) = pair node (foldsub subspine) -> foldsub Cycle = cycle -> foldsub Delta = delta -> foldsub (Force spine) = force (fold spine) -> foldsub MissingCase = missingcase -> foldsub (Open rgraph) = open rgraph -> foldsub (Partial rule matching spine) = partial rule matching (fold spine) -> foldsub (Unsafe rgraph) = unsafe rgraph -> foldsub (Redex rule matching) = redex rule matching -> foldsub Strict = strict - -*/ - -foldspine - :: !(var .subresult -> .result) // Fold the spine itself - .subresult // Fold a Cycle subspine - .subresult // Fold a Delta subspine - (Int .result -> .subresult) // Fold a Force subspine - .subresult // Fold a MissingCase subspine - ((Rgraph sym pvar) -> .subresult) // Fold an Open subspine - ((Rule sym pvar) (Pfun pvar var) pvar .result -> .subresult) // Fold a Partial subspine - ((HistoryPattern sym var) -> .subresult) // Fold an Unsafe subspine - ((Rule sym pvar) (Pfun pvar var) -> .subresult) // Fold a Redex subspine - .subresult // Fold a Strict subspine - .(Spine sym var pvar) // The spine to fold - -> .result // The final result - -foldspine pair cycle delta force missingcase open partial unsafe redex strict spine -= fold spine - where fold spine - = pair node (foldsub subspine) - where (node,subspine) = spine - foldsub Cycle = cycle - foldsub Delta = delta - foldsub (Force argno spine) = force argno (fold spine) - foldsub MissingCase = missingcase - foldsub (Open rgraph) = open rgraph - foldsub (Partial rule matching rnode spine) = partial rule matching rnode (fold spine) - foldsub (Unsafe histpat) = unsafe histpat - foldsub (Redex rule matching) = redex rule matching - foldsub Strict = strict - -spinetip :: !(Spine sym var pvar) -> Spine sym var pvar -spinetip (_,Force argno spine) = spinetip spine -spinetip (_,Partial _ _ pnode spine) = spinetip spine -spinetip spine = spine - -spinenodes :: .(Spine sym var pvar) -> [var] -spinenodes spine -= nodes - 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 -= foldoptional other (checkopen o spinetip) spine - where checkopen (onode,Open pattern) = open - checkopen tip = other - - -/********************************************* -* Extending the history according to a spine * -*********************************************/ - -// A function that associates specific patterns with extensible nodes -// To be used for extending history patterns -:: LinkExtender sym var - :== (Link var) // The extensible link to look for - -> HistoryPattern sym var // The associated pattern - -extendhistory - :: (Graph sym var) - (var -> var) - (Spine sym var pvar) - (History sym var) - -> History sym var - | == var - & == pvar - -extendhistory sgraph redirection spine history -= snd (foldspine (extendpair sgraph redirection) d d (const id) d (const d) (extendpartial sgraph) (const d) (extendredex sgraph history) d spine) - where d = (emptygraph,history) - - -extendpair - :: (Graph sym var) - (var->var) - var - (Graph sym var,History sym var) - -> (Graph sym var,History sym var) - | == var - -extendpair sgraph redirect snode (hgraph,history) -= (hgraph`,remap (redirect snode) [mkrgraph snode hgraph`:foldmap id [] history snode] (forget snode history)) - where hgraph` = if sdef (updategraph snode scont hgraph) hgraph - (sdef,scont) = dnc (const "in extendpair") sgraph snode - -extendpartial - :: (Graph sym var) - (Rule sym pvar) - (Pfun pvar var) - pvar - (Graph sym var,History sym var) - -> (Graph sym var,History sym var) - | == var - & == pvar - -extendpartial sgraph rule matching rnode (hgraph,history) -= (extgraph` sgraph rule matching hgraph,history) - -extendredex - :: (Graph sym var) - (History sym var) - (Rule sym pvar) - (Pfun pvar var) - -> (Graph sym var,History sym var) - | == var - & == pvar - -extendredex sgraph history rule matching -= (extgraph` sgraph rule matching emptygraph,history) - -extgraph` :: (Graph sym var) (Rule sym pvar) -> (Pfun pvar var) (Graph sym var) -> Graph sym var | == var & == pvar -extgraph` sgraph rule -= extgraph sgraph rgraph (varlist rgraph (arguments rule)) - where rgraph = rulegraph rule - -(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 | toString sym & ==,toString,<<< var // & ==,toString,<<< pvar -(writespine) file (var,subspine) = file <<< "(" <<< var <<< "," <<< 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 deleted file mode 100644 index c2b6ce6..0000000 --- a/sucl/strat.dcl +++ /dev/null @@ -1,183 +0,0 @@ -definition module strat - -// $Id$ - -from spine import Answer -from history import History -from rule import Rule -from graph import Graph,Node -from StdOverloaded import == -from StdClass import Eq -from cleanversion import String - -from history import HistoryAssociation,HistoryPattern,Link // for History -from spine import Spine // for Answer -from spine import Subspine // for Spine -from rule import Rgraph // for History -from basic import Optional // for Spine - -:: Strategy sym var pvar result - :== (Substrategy sym var pvar result) - (Graph sym var) - ((Subspine sym var pvar) -> result) - result - (Node sym var) - -> result - -:: Substrategy sym var pvar result - :== ((Spine sym var pvar) -> result) - result - var - -> result - -:: Law sym var pvar result - :== (Substrategy sym var pvar result) - (Graph sym var) - ((Subspine sym var pvar) -> result) - result - [var] - result - -> result - -// Apply a strategy recursively to a graph -// by deriving the substrategy from it and feeding it back to it -// Think Y operator -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 - (Graph sym var) // Subject graph - -> Answer sym var pvar - | Eq sym - & Eq var - & Eq pvar - - -/* ------------------------------------------------------------------------ -STRATEGY TRANSFORMERS -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 - .result // RNF continuation - !.(Node sym var) // Subject node - -> .result - -// A strategy transformer that checks for constructor applications -checkconstr - :: (sym->String) - (sym->.Bool) - (Strategy sym var pvar .result) - (Substrategy sym var pvar .result) - (Graph sym var) - ((Subspine sym var pvar) -> .result) - .result - .(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) - .result - .(Node sym var) - -> .result - -// A strategy transformer that checks (hard coded) laws -checklaws - :: [(sym,Law 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) - -> result - | == sym - -// A strategy transformere that checks a list of rewrite rules -// This is the real thing that characterises the functional strategy -checkrules - :: ((Graph sym pvar) pvar var -> .Bool) - (sym -> .[Rule sym pvar]) - (Strategy sym var pvar result) - (Substrategy sym var pvar result) - (Graph sym var) - ((Subspine sym var pvar) -> result) - result - (Node sym var) - -> result - | == sym - & == var - & == pvar - -// A strategy transformer that checks a function application -// 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 - .result // RNF continuation - !.(Node sym var) // Subject node - -> .result - -/* ------------------------------------------------------------------------ -USEFUL AIDS FOR DEFINING STRATEGY TRANSFORMERS -The functions below are useful for inspecting a graph -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) - .result - !.[var] - -> .result - -// Try to apply a transformation rule (that doesn't need evaluated arguments) -rulelaw - :: (Rule sym pvar) - -> Law sym var pvar result - | == sym - & == var - & == pvar - -// Try to apply a law -trylaw - :: (Graph sym var) - (.(Subspine sym var pvar) -> result) - .[var] - (Rule sym pvar) - result - -> result - | == sym - & == var - & == pvar - -// Try a list of rewrite rules -// Requires argument evaluation for closed patterns -tryrules - :: ((Graph sym pvar) pvar var -> .Bool) - (Substrategy sym var pvar result) - (Graph sym var) - ((Subspine sym var pvar) -> result) - .[var] - -> result - .[Rule sym pvar] - -> result - | == sym - & == var - & == pvar diff --git a/sucl/strat.icl b/sucl/strat.icl deleted file mode 100644 index 4241129..0000000 --- a/sucl/strat.icl +++ /dev/null @@ -1,486 +0,0 @@ -implementation module strat - -// $Id$ - -import spine -import history -import rule -import dnc -import graph -import pfun -import basic -from general import No,Yes,---> -import StdEnv - -/* - -strat.lit - Extended functional strategy -======================================== - -Description ------------ - -Describe in a few paragraphs what this module defines. - ------------------------------------------------------------- - -Interface ---------- - -Exported identifiers: - -> %export - -> law -> strategy -> substrategy - -> makernfstrategy - -> checkconstr -> checkimport -> checklaws -> checkrules -> checktype - -> forcenodes -> rulelaw -> trylaw -> tryrules - -Required types: - - identifier - type@source.lit type@source.lit - ... - ------------------------------------------------------------- - -Includes --------- - -> %include "dnc.lit" - -> %include "../src/basic.lit" -> %include "../src/pfun.lit" -> %include "../src/graph.lit" -instantiate -> %include "../src/rule.lit" -> %include "../src/spine.lit" - ------------------------------------------------------------- - -Types ------ - -*/ - -:: Substrategy sym var pvar result - :== ((Spine sym var pvar) -> result) - result - var - -> result - -:: Strategy sym var pvar result - :== (Substrategy sym var pvar result) - (Graph sym var) - ((Subspine sym var pvar) -> result) - result - (Node sym var) - -> result - -:: Law sym var pvar result - :== (Substrategy sym var pvar result) - (Graph sym var) - ((Subspine sym var pvar) -> result) - result - [var] - result - -> result - -//------------------------------------------------------------------------ - -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 - (Graph sym var) // Subject graph - -> Answer sym var pvar - | Eq sym - & Eq var - & Eq pvar - -makernfstrategy hist strat rnfnodes node graph -= substrat [] spinecont rnfanswer node - where spinecont spine = Yes spine - rnfanswer = No - - substrat spinenodes spinecont rnfanswer node - | isMember node spinenodes - = subspinecont Cycle - | isMember node rnfnodes - = rnfanswer - | not def - = subspinecont Strict - = strat` (substrat spinenodes`) graph subspinecont rnfanswer cnt - where (def,cnt) = dnc (const "in makernfstrategy") graph node - spinenodes` = [node:spinenodes] - subspinecont subspine = spinecont (node,subspine) - strat` = (checkhistory--->"strat.checkhistory begins from strat.makernfstrategy.substrat.strat`") (graph,node) spinenodes` hist strat - -/* - ------------------------------------------------------------------------- -NORMAL REWRITE RULE STRATEGY - -*/ - -tryrules - :: ((Graph sym pvar) pvar var -> .Bool) - (Substrategy sym var pvar result) - (Graph sym var) - ((Subspine sym var pvar) -> result) - .[var] - -> result - .[Rule sym pvar] - -> result - | == sym - & == var - & == pvar - -tryrules matchable substrat subject found sargs -= foldr (matchrule matchable substrat subject found sargs) - -matchrule - :: ((Graph sym pvar) pvar var -> .Bool) - (Substrategy sym var pvar result) - (Graph sym var) - ((Subspine sym var pvar) -> result) - .[var] - (Rule sym pvar) - result - -> result - | == sym - & == var - & == pvar - -matchrule matchable substrat subject found sargs rule fail -| eqlen pargs sargs -= matchnodes matchable` subject substrat foundsub fail pattern foundmatch pairs emptypfun -= fail - where pargs = arguments rule - pattern = rulegraph rule - pairs = zip2 pargs sargs - matchable` = matchable pattern - foundsub matching rnode spine = found (Partial rule matching rnode spine) - foundmatch matching = found (Redex rule matching) - -matchnodes - :: (pvar var -> .Bool) - (Graph sym var) - (Substrategy sym var pvar result) - ((Pfun pvar var) pvar (Spine sym var pvar) -> result) - result - (Graph sym pvar) - -> ((Pfun pvar var) -> result) - [.(pvar,var)] - (Pfun pvar var) - -> result - | == sym - & == var - & == pvar - -matchnodes matchable subject substrat found fail pattern -= foldr matchpair - where matchpair (pnode,snode) match matching - | not (matchable pnode snode) - = fail - | not pdef - = match (extend pnode snode matching) - | not sdef - = found matching pnode openspine - = substrat (found matching pnode) rnfanswer snode - where openspine = (snode,Open (mkrgraph pnode pattern)) - rnfanswer - | psym==ssym && eqlen pargs sargs - = foldr matchpair match` psargs matching - = fail - match` matching = match (extend pnode snode matching) - psargs = zip2 pargs sargs - (pdef,(psym,pargs)) = (dnc (const "in matchnodes (pattern)")) pattern pnode - (sdef,(ssym,sargs)) = (dnc (const "in matchnodes (subject)")) subject snode - -/* - ------------------------------------------------------------------------- -SPECIAL LAW STRATEGY - -Does not try to reduce arguments before matching. - -> rulelaw -> :: rule * *** -> -> law * ** *** **** - -> rulelaw rule substrat subject found rnf snids fail -> = trylaw subject found snids rule fail - -> trylaw -> :: graph * ** -> -> (subspine * ** ***->****) -> -> [**] -> -> rule * *** -> -> **** -> -> **** - -> trylaw graph found sargs rule fail -> = lawmatch pattern graph fail found' pairs emptypfun, if eqlen pargs sargs -> = fail, otherwise -> where pargs = lhs rule; pattern = rulegraph rule -> found' matching = found (Redex rule matching) -> pairs = zip2 pargs sargs - -> lawmatch -> :: graph * *** -> -> graph * ** -> -> **** -> -> (pfun *** **->****) -> -> [(***,**)] -> -> pfun *** ** -> **** - -> lawmatch pattern subject fail -> = foldr lawmatch' -> where lawmatch' (pnode,snode) success matching -> = success matching', if ~pdef -> = fail, if ~sdef \/ ssym~=psym \/ ~eqlen pargs sargs -> = foldr lawmatch' success (zip2 pargs sargs) matching', otherwise -> where matching' = extend pnode snode matching -> (pdef,(psym,pargs)) = (dnc (const "in lawmatch/1")) pattern pnode -> (sdef,(ssym,sargs)) = (dnc (const "in lawmatch/2")) subject snode - -*/ - -rulelaw - :: (Rule sym pvar) - -> Law sym var pvar result - | == sym - & == var - & == pvar - -rulelaw rule -= law -where law substrat subject found rnf snids fail - = trylaw subject found snids rule fail - -trylaw - :: (Graph sym var) - (.(Subspine sym var pvar) -> result) - .[var] - (Rule sym pvar) - result - -> result - | == sym - & == var - & == pvar - -trylaw graph found sargs rule fail -| eqlen pargs sargs -= lawmatch pattern graph fail found` pairs emptypfun -= fail - where pargs = arguments rule; pattern = rulegraph rule - found` matching = found (Redex rule matching) - pairs = zip2 pargs sargs - -lawmatch - :: (Graph sym pvar) - (Graph sym var) - result - -> ((Pfun pvar var) -> result) - [.(pvar,var)] - (Pfun pvar var) - -> result - | == sym - & == var - & == pvar - -lawmatch pattern subject fail -= foldr lawmatch` - where lawmatch` (pnode,snode) success matching - | not pdef - = success matching` - | not sdef || ssym <> psym || not (eqlen pargs sargs) - = fail - = foldr lawmatch` success (zip2 pargs sargs) matching` - where matching` = extend pnode snode matching - (pdef,(psym,pargs)) = (dnc (const "in lawmatch (pattern)")) pattern pnode - (sdef,(ssym,sargs)) = (dnc (const "in lawmatch (subject)")) subject snode - -/* - ------------------------------------------------------------------------- -FORCING EVALUATION OF (STRICT) ARGUMENTS - -*/ - -forcenodes - :: (Substrategy sym var pvar .result) - ((Subspine sym var pvar) -> .result) - .result - !.[var] - -> .result - -forcenodes substrat found rnf nodes -= foldr forcenode rnf (zip2 [0..] nodes) - where forcenode (argno,nid) rnfrest - = substrat foundforce rnfrest nid - where foundforce spine = found (Force argno spine) - -/* - ------------------------------------------------------------------------- -STRATEGY COMPOSITION - -Check for an instance in the termination history. - -*/ - -checkhistory - :: (Graph sym var,var) - [var] - (History sym var) - (Strategy sym var pvar result) - -> Strategy sym var pvar result - | Eq sym - & Eq var - -checkhistory (sgraph,snode) spinenodes history defaultstrategy -= (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 - .result // RNF continuation - !.(Node sym var) // Subject node - -> .result - -checkarity funarity defaultstrategy substrat subject found rnf (ssym,sargs) -| shortern arity sargs -= rnf -| eqlenn arity sargs -= defaultstrategy substrat subject found rnf (ssym,sargs) -= abort ("checktype: symbol occurrence with actual arity "+++toString (length sargs)+++" greater than its type arity "+++toString arity) - where arity = funarity ssym - -shortern n _ | n<=0 = False -shortern _ [] = True -shortern n [x:xs] = shortern (n-1) xs - -eqlenn n _ | n<0 = False -eqlenn 0 [] = True -eqlenn n [x:xs] = eqlenn (n-1) xs - - -// Check 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 - .result // RNF continuation - !.(Node sym var) // Subject node - -> .result - -checkstricts funstricts defaultstrategy substrat subject found rnf (ssym,sargs) -= forcenodes substrat found rnf` strictnodes - where rnf` = defaultstrategy substrat subject found rnf (ssym,sargs) - tstricts = funstricts ssym - strictnodes = [sarg\\(True,sarg)<-zip2 tstricts sargs] - - -// Check (hard coded) laws - -checklaws - :: [(sym,Law 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) - -> result - | == sym - -checklaws laws defaultstrategy substrat subject found rnf (ssym,sargs) -= foldr checklaw (defaultstrategy substrat subject found rnf (ssym,sargs)) laws - where checklaw (lsym,law) fail - | lsym==ssym - = law substrat subject found rnf sargs fail - = fail - - -// Check a list of rewrite rules (this is the real thing) - -checkrules - :: ((Graph sym pvar) pvar var -> .Bool) - (sym -> .[Rule sym pvar]) - (Strategy sym var pvar result) - (Substrategy sym var pvar result) - (Graph sym var) - ((Subspine sym var pvar) -> result) - result - (Node sym var) - -> result - | == sym - & == var - & == pvar - -checkrules matchable ruledefs defstrat substrat subject found rnf (ssym,sargs) -= tryrules matchable substrat subject found sargs fail (ruledefs ssym) - where fail = defstrat substrat subject found rnf (ssym,sargs) - - -// Check for delta/imported/abstract/black-box (whatever) symbols - -checkimport - :: !(sym->.Bool) - (Strategy sym var pvar .result) - (Substrategy sym var pvar .result) - (Graph sym var) - ((Subspine sym var pvar) -> .result) - .result - .(Node sym var) - -> .result - -checkimport local defstrat substrat subject found rnf (ssym,sargs) -| not (local ssym) -= found Delta -= defstrat substrat subject found rnf (ssym,sargs) - - -// Check for constructors - -checkconstr - :: (sym->String) - (sym->.Bool) - (Strategy sym var pvar .result) - (Substrategy sym var pvar .result) - (Graph sym var) - ((Subspine sym var pvar) -> .result) - .result - .(Node sym var) - -> .result - -checkconstr showsym isconstr defstrat substrat subject found rnf (ssym,sargs) -| isconstr ssym ---> ("strat.checkconstr begins for "+++showsym ssym) -= rnf <--- ("strat.checkconstr ends (RNF)") -= defstrat substrat subject found rnf (ssym,sargs) <--- ("strat.checkconstr ends (default strategy)") diff --git a/sucl/sucl.prj b/sucl/sucl.prj deleted file mode 100644 index e6daada..0000000 --- a/sucl/sucl.prj +++ /dev/null @@ -1,1190 +0,0 @@ -Version: 1.4 -Global - Built: False - Target: StdEnv - Exec: {Project}\sucl.exe - CodeGen - CheckStacks: False - CheckIndexes: False - TargetProcessor: CurrentProcessor - Application - HeapSize: 409600 - StackSize: 102400 - ExtraMemory: 81920 - IntialHeapSize: 204800 - HeapSizeMultiplier: 4096 - ShowExecutionTime: False - ShowGC: False - ShowStackSize: False - MarkingCollector: False - StandardRuntimeEnv: True - Profile - Memory: False - MemoryMinimumHeapSize: 0 - Time: False - Stack: False - Output - Output: ShowConstructors - Font: Courier - FontSize: 9 - WriteStdErr: False - Link - LinkMethod: Static - GenerateRelocations: False - GenerateLinkMap: False - LinkResources: False - ResourceSource: - Paths - Path: {Project} - Path: C:\Vincent\cocl\compiler -MainModule - Name: basic - Dir: {Project} - Compiler - NeverMemoryProfile: False - NeverTimeProfile: False - StrictnessAnalysis: True - ListTypes: AllTypes - ListAttributes: True - Warnings: True - Verbose: True - ReadableABC: False - ReuseUniqueNodes: False - Dcl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 552 - SizeY: 697 - DclOpen: False - Icl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 24 - SizeX: 1136 - SizeY: 751 - IclOpen: False - LastModified: No 0 0 0 0 0 0 -OtherModules - Module - Name: StdOverloaded - Dir: {Application}\StdEnv - Compiler - NeverMemoryProfile: False - NeverTimeProfile: False - StrictnessAnalysis: True - ListTypes: StrictExportTypes - ListAttributes: True - Warnings: True - Verbose: True - ReadableABC: False - ReuseUniqueNodes: False - Dcl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 999 - SizeY: 511 - DclOpen: False - Icl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - IclOpen: False - LastModified: No 0 0 0 0 0 0 - Module - Name: StdEnv - Dir: {Application}\StdEnv - Compiler - NeverMemoryProfile: False - NeverTimeProfile: False - StrictnessAnalysis: True - ListTypes: StrictExportTypes - ListAttributes: True - Warnings: True - Verbose: True - ReadableABC: False - ReuseUniqueNodes: False - Dcl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - DclOpen: False - Icl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - IclOpen: False - LastModified: No 0 0 0 0 0 0 - Module - Name: StdBool - Dir: {Application}\StdEnv - Compiler - NeverMemoryProfile: False - NeverTimeProfile: False - StrictnessAnalysis: True - ListTypes: AllTypes - ListAttributes: True - Warnings: True - Verbose: True - ReadableABC: False - ReuseUniqueNodes: False - Dcl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 970 - SizeY: 517 - DclOpen: False - Icl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - IclOpen: False - LastModified: No 0 0 0 0 0 0 - Module - Name: StdInt - Dir: {Application}\StdEnv - Compiler - NeverMemoryProfile: False - NeverTimeProfile: False - StrictnessAnalysis: True - ListTypes: AllTypes - ListAttributes: True - Warnings: True - Verbose: True - ReadableABC: False - ReuseUniqueNodes: False - Dcl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - DclOpen: False - Icl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - IclOpen: False - LastModified: No 0 0 0 0 0 0 - Module - Name: StdReal - Dir: {Application}\StdEnv - Compiler - NeverMemoryProfile: False - NeverTimeProfile: False - StrictnessAnalysis: True - ListTypes: AllTypes - ListAttributes: True - Warnings: True - Verbose: True - ReadableABC: False - ReuseUniqueNodes: False - Dcl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - DclOpen: False - Icl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - IclOpen: False - LastModified: No 0 0 0 0 0 0 - Module - Name: StdChar - Dir: {Application}\StdEnv - Compiler - NeverMemoryProfile: False - NeverTimeProfile: False - StrictnessAnalysis: True - ListTypes: AllTypes - ListAttributes: True - Warnings: True - Verbose: True - ReadableABC: False - ReuseUniqueNodes: False - Dcl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - DclOpen: False - Icl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - IclOpen: False - LastModified: No 0 0 0 0 0 0 - Module - Name: StdArray - Dir: {Application}\StdEnv - Compiler - NeverMemoryProfile: False - NeverTimeProfile: False - StrictnessAnalysis: True - ListTypes: StrictExportTypes - ListAttributes: True - Warnings: True - Verbose: True - ReadableABC: False - ReuseUniqueNodes: False - Dcl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - DclOpen: False - Icl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - IclOpen: False - LastModified: No 0 0 0 0 0 0 - Module - Name: _SystemArray - Dir: {Application}\StdEnv - Compiler - NeverMemoryProfile: False - NeverTimeProfile: False - StrictnessAnalysis: True - ListTypes: AllTypes - ListAttributes: True - Warnings: True - Verbose: True - ReadableABC: False - ReuseUniqueNodes: False - Dcl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - DclOpen: False - Icl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - IclOpen: False - LastModified: No 0 0 0 0 0 0 - Module - Name: StdString - Dir: {Application}\StdEnv - Compiler - NeverMemoryProfile: False - NeverTimeProfile: False - StrictnessAnalysis: True - ListTypes: AllTypes - ListAttributes: True - Warnings: True - Verbose: True - ReadableABC: False - ReuseUniqueNodes: False - Dcl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - DclOpen: False - Icl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - IclOpen: False - LastModified: No 0 0 0 0 0 0 - Module - Name: StdFile - Dir: {Application}\StdEnv - Compiler - NeverMemoryProfile: False - NeverTimeProfile: False - StrictnessAnalysis: True - ListTypes: AllTypes - ListAttributes: True - Warnings: True - Verbose: True - ReadableABC: False - ReuseUniqueNodes: False - Dcl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - DclOpen: False - Icl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - IclOpen: False - LastModified: No 0 0 0 0 0 0 - Module - Name: StdClass - Dir: {Application}\StdEnv - Compiler - NeverMemoryProfile: False - NeverTimeProfile: False - StrictnessAnalysis: True - ListTypes: StrictExportTypes - ListAttributes: True - Warnings: True - Verbose: True - ReadableABC: False - ReuseUniqueNodes: False - Dcl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 1083 - SizeY: 475 - DclOpen: False - Icl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - IclOpen: False - LastModified: No 0 0 0 0 0 0 - Module - Name: StdList - Dir: {Application}\StdEnv - Compiler - NeverMemoryProfile: False - NeverTimeProfile: False - StrictnessAnalysis: True - ListTypes: StrictExportTypes - ListAttributes: True - Warnings: True - Verbose: True - ReadableABC: False - ReuseUniqueNodes: False - Dcl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 1001 - SizeY: 401 - DclOpen: False - Icl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - IclOpen: False - LastModified: No 0 0 0 0 0 0 - Module - Name: StdMisc - Dir: {Application}\StdEnv - Compiler - NeverMemoryProfile: False - NeverTimeProfile: False - StrictnessAnalysis: True - ListTypes: AllTypes - ListAttributes: True - Warnings: True - Verbose: True - ReadableABC: False - ReuseUniqueNodes: False - Dcl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - DclOpen: False - Icl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - IclOpen: False - LastModified: No 0 0 0 0 0 0 - Module - Name: StdEnum - Dir: {Application}\StdEnv - Compiler - NeverMemoryProfile: False - NeverTimeProfile: False - StrictnessAnalysis: True - ListTypes: StrictExportTypes - ListAttributes: True - Warnings: True - Verbose: True - ReadableABC: False - ReuseUniqueNodes: False - Dcl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - DclOpen: False - Icl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - IclOpen: False - LastModified: No 0 0 0 0 0 0 - Module - Name: _SystemEnum - Dir: {Application}\StdEnv - Compiler - NeverMemoryProfile: False - NeverTimeProfile: False - StrictnessAnalysis: True - ListTypes: StrictExportTypes - ListAttributes: True - Warnings: True - Verbose: True - ReadableABC: False - ReuseUniqueNodes: False - Dcl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - DclOpen: False - Icl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - IclOpen: False - LastModified: No 0 0 0 0 0 0 - Module - Name: StdOrdList - Dir: {Application}\StdEnv - Compiler - NeverMemoryProfile: False - NeverTimeProfile: False - StrictnessAnalysis: True - ListTypes: StrictExportTypes - ListAttributes: True - Warnings: True - Verbose: True - ReadableABC: False - ReuseUniqueNodes: False - Dcl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - DclOpen: False - Icl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - IclOpen: False - LastModified: No 0 0 0 0 0 0 - Module - Name: StdTuple - Dir: {Application}\StdEnv - Compiler - NeverMemoryProfile: False - NeverTimeProfile: False - StrictnessAnalysis: True - ListTypes: StrictExportTypes - ListAttributes: True - Warnings: True - Verbose: True - ReadableABC: False - ReuseUniqueNodes: False - Dcl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - DclOpen: False - Icl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - IclOpen: False - LastModified: No 0 0 0 0 0 0 - Module - Name: StdCharList - Dir: {Application}\StdEnv - Compiler - NeverMemoryProfile: False - NeverTimeProfile: False - StrictnessAnalysis: True - ListTypes: StrictExportTypes - ListAttributes: True - Warnings: True - Verbose: True - ReadableABC: False - ReuseUniqueNodes: False - Dcl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - DclOpen: False - Icl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - IclOpen: False - LastModified: No 0 0 0 0 0 0 - Module - Name: StdFunc - Dir: {Application}\StdEnv - Compiler - NeverMemoryProfile: False - NeverTimeProfile: False - StrictnessAnalysis: True - ListTypes: StrictExportTypes - ListAttributes: True - Warnings: True - Verbose: True - ReadableABC: False - ReuseUniqueNodes: False - Dcl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - DclOpen: False - Icl - Editor - TabSize: 4 - Font: Courier New - FontSize: 10 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - IclOpen: False - LastModified: No 0 0 0 0 0 0 - Module - Name: pfun - Dir: {Project} - Compiler - NeverMemoryProfile: False - NeverTimeProfile: False - StrictnessAnalysis: True - ListTypes: AllTypes - ListAttributes: True - Warnings: True - Verbose: True - ReadableABC: False - ReuseUniqueNodes: False - Dcl - Editor - TabSize: 8 - Font: Courier - FontSize: 7 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 1110 - SizeY: 128 - DclOpen: False - Icl - Editor - TabSize: 8 - Font: Courier - FontSize: 7 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 169 - SizeX: 1136 - SizeY: 679 - IclOpen: False - LastModified: No 0 0 0 0 0 0 - Module - Name: graph - Dir: {Project} - Compiler - NeverMemoryProfile: False - NeverTimeProfile: False - StrictnessAnalysis: True - ListTypes: AllTypes - ListAttributes: True - Warnings: True - Verbose: True - ReadableABC: False - ReuseUniqueNodes: False - Dcl - Editor - TabSize: 8 - Font: Courier - FontSize: 7 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 10 - Y: 10 - SizeX: 800 - SizeY: 520 - DclOpen: False - Icl - Editor - TabSize: 8 - Font: Courier - FontSize: 7 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 10 - Y: 10 - SizeX: 1102 - SizeY: 477 - IclOpen: False - LastModified: No 0 0 0 0 0 0 - Module - Name: casegraph - Dir: {Project} - Compiler - NeverMemoryProfile: False - NeverTimeProfile: False - StrictnessAnalysis: True - ListTypes: StrictExportTypes - ListAttributes: True - Warnings: True - Verbose: True - ReadableABC: False - ReuseUniqueNodes: False - Dcl - Editor - TabSize: 8 - Font: Courier - FontSize: 7 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 10 - Y: 10 - SizeX: 1116 - SizeY: 133 - DclOpen: False - Icl - Editor - TabSize: 8 - Font: Courier - FontSize: 7 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 10 - Y: 10 - SizeX: 1110 - SizeY: 636 - IclOpen: False - LastModified: No 0 0 0 0 0 0 - Module - Name: dnc - Dir: {Project} - Compiler - NeverMemoryProfile: False - NeverTimeProfile: False - StrictnessAnalysis: True - ListTypes: AllTypes - ListAttributes: True - Warnings: True - Verbose: True - ReadableABC: False - ReuseUniqueNodes: False - Dcl - Editor - TabSize: 8 - Font: Courier - FontSize: 7 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 10 - Y: 10 - SizeX: 800 - SizeY: 520 - DclOpen: False - Icl - Editor - TabSize: 8 - Font: Courier - FontSize: 7 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 10 - Y: 10 - SizeX: 800 - SizeY: 521 - IclOpen: False - LastModified: No 0 0 0 0 0 0 - Module - Name: rule - Dir: {Project} - Compiler - NeverMemoryProfile: False - NeverTimeProfile: False - StrictnessAnalysis: True - ListTypes: AllTypes - ListAttributes: True - Warnings: True - Verbose: True - ReadableABC: False - ReuseUniqueNodes: False - Dcl - Editor - TabSize: 8 - Font: Courier - FontSize: 7 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 10 - Y: 10 - SizeX: 784 - SizeY: 520 - DclOpen: False - Icl - Editor - TabSize: 8 - Font: Courier - FontSize: 7 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 10 - Y: 10 - SizeX: 800 - SizeY: 520 - IclOpen: False - LastModified: No 0 0 0 0 0 0 - Module - Name: rewr - Dir: {Project} - Compiler - NeverMemoryProfile: False - NeverTimeProfile: False - StrictnessAnalysis: True - ListTypes: AllTypes - ListAttributes: True - Warnings: True - Verbose: True - ReadableABC: False - ReuseUniqueNodes: False - Dcl - Editor - TabSize: 8 - Font: Courier - FontSize: 7 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 0 - Y: 0 - SizeX: 500 - SizeY: 300 - DclOpen: False - Icl - Editor - TabSize: 8 - Font: Courier - FontSize: 7 - AutoIndent: True - ShowTabs: False - ShowLins: True - WindowPosition - X: 10 - Y: 10 - SizeX: 800 - SizeY: 520 - IclOpen: False - LastModified: No 0 0 0 0 0 0 -Static - Mods - Path: C:\Vincent\Sucl\basic.icl - Path: C:\Clean 1.3.3\StdEnv\StdOverloaded.icl - Path: C:\Clean 1.3.3\StdEnv\StdEnv.icl - Path: C:\Clean 1.3.3\StdEnv\StdBool.icl - Path: C:\Clean 1.3.3\StdEnv\StdInt.icl - Path: C:\Clean 1.3.3\StdEnv\StdReal.icl - Path: C:\Clean 1.3.3\StdEnv\StdChar.icl - Path: C:\Clean 1.3.3\StdEnv\StdArray.icl - Path: C:\Clean 1.3.3\StdEnv\_SystemArray.icl - Path: C:\Clean 1.3.3\StdEnv\StdString.icl - Path: C:\Clean 1.3.3\StdEnv\StdFile.icl - Path: C:\Clean 1.3.3\StdEnv\StdClass.icl - Path: C:\Clean 1.3.3\StdEnv\StdList.icl - Path: C:\Clean 1.3.3\StdEnv\StdMisc.icl - Path: C:\Clean 1.3.3\StdEnv\StdEnum.icl - Path: C:\Clean 1.3.3\StdEnv\_SystemEnum.icl - Path: C:\Clean 1.3.3\StdEnv\StdOrdList.icl - Path: C:\Clean 1.3.3\StdEnv\StdTuple.icl - Path: C:\Clean 1.3.3\StdEnv\StdCharList.icl - Path: C:\Clean 1.3.3\StdEnv\StdFunc.icl - Objs - Path: C:\Clean 1.3.3\StdEnv\Clean System Files\_startup0.o - Path: C:\Clean 1.3.3\StdEnv\Clean System Files\_startup1.o - Path: C:\Clean 1.3.3\StdEnv\Clean System Files\_startup2.o - Path: C:\Clean 1.3.3\StdEnv\Clean System Files\_system.o - Path: C:\Vincent\Sucl\Clean System Files\basic.o - Path: C:\Clean 1.3.3\StdEnv\Clean System Files\StdOverloaded.o - Path: C:\Clean 1.3.3\StdEnv\Clean System Files\StdString.o - Path: C:\Clean 1.3.3\StdEnv\Clean System Files\StdEnv.o - Path: C:\Clean 1.3.3\StdEnv\Clean System Files\StdBool.o - Path: C:\Clean 1.3.3\StdEnv\Clean System Files\StdInt.o - Path: C:\Clean 1.3.3\StdEnv\Clean System Files\StdReal.o - Path: C:\Clean 1.3.3\StdEnv\Clean System Files\StdChar.o - Path: C:\Clean 1.3.3\StdEnv\Clean System Files\StdArray.o - Path: C:\Clean 1.3.3\StdEnv\Clean System Files\_SystemArray.o - Path: C:\Clean 1.3.3\StdEnv\Clean System Files\StdFile.o - Path: C:\Clean 1.3.3\StdEnv\Clean System Files\StdClass.o - Path: C:\Clean 1.3.3\StdEnv\Clean System Files\StdList.o - Path: C:\Clean 1.3.3\StdEnv\Clean System Files\StdOrdList.o - Path: C:\Clean 1.3.3\StdEnv\Clean System Files\StdTuple.o - Path: C:\Clean 1.3.3\StdEnv\Clean System Files\StdCharList.o - Path: C:\Clean 1.3.3\StdEnv\Clean System Files\StdFunc.o - Path: C:\Clean 1.3.3\StdEnv\Clean System Files\StdMisc.o - Path: C:\Clean 1.3.3\StdEnv\Clean System Files\StdEnum.o - Path: C:\Clean 1.3.3\StdEnv\Clean System Files\_SystemEnum.o - Dlib - Path: C:\Clean 1.3.3\StdEnv\Clean System Files\kernel_library - Path: C:\Clean 1.3.3\StdEnv\Clean System Files\comdlg_library - Path: C:\Clean 1.3.3\StdEnv\Clean System Files\gdi_library - Path: C:\Clean 1.3.3\StdEnv\Clean System Files\user_library - Pths - Path: C:\Vincent\Sucl - Path: C:\Vincent\cocl\compiler - Path: C:\Clean 1.3.3\StdEnv - AppP: C:\Clean 1.3.3 - PrjP: C:\Vincent\Sucl diff --git a/sucl/trace.dcl b/sucl/trace.dcl deleted file mode 100644 index f271084..0000000 --- a/sucl/trace.dcl +++ /dev/null @@ -1,318 +0,0 @@ -definition module trace - -// $Id$ - -from spine import Answer -from history import History,HistoryAssociation,HistoryPattern -from rule import Rule -from StdFile import <<< -from StdOverloaded import == -from StdString import toString -from cleanversion import String - -// Transitive necessities - -from spine import Spine,Subspine // for Answer -from rule import Rgraph // for History -from basic import Optional // for Answer - -/* - -trace.lit - Symbolic reduction traces -===================================== - -Description ------------ - -This script implements traces of symbolic reduction, indicating what -happened and why. Representation functions for traces are also -provided. - -A trace is a possibly infinite tree, with the nodes labeled with a -rewrite rule, the strategy answer for that rewrite rule, and the -selected transformation according to the rewrite rule and the strategy -answer. If any transformation is applicable, then a list of subtrees is -present and indicates the result of applying the transformation to the -rewrite rule. This is a list because a transformation may return more -than one transformed rewrite rule. - ------------------------------------------------------------------------- - -Interface ---------- - -Exported identifiers: - -> %export -> trace || Type of a trace -> transformation || Type of applied transformation - -> foldtransformation || Break down a transformation -> mapleaves || Map a function on the rules at the leaves of a trace -> printtrace || Make a human-readable representation of a trace -> showtrace || Make a representation of a trace -> strictchar || Representation of strictness annotation -> tips || Determine tips of a finite trace - -> result || Deprecated in the new trace structure -> onresults || Deprecated -> printresult || Deprecated - -Required types: - ------------------------------------------------------------- - -Includes --------- - -> %include "../src/basic.lit" || optional - -> %include "../src/pfun.lit" || pfun - -> %include "../src/graph.lit" -> %include "../src/rule.lit" || rule - printrule rhs rulegraph showrule -> %include "../src/spine.lit" - ------------------------------------------------------------- - -Deprecated ----------- - -> result * ** *** :: type -> onresults :: (result * ** ***->result * ** ***) -> trace * ** *** -> trace * ** *** -> printresult :: * -> (*->[char]) -> (**->[char]) -> (***->[char]) -> result * ** *** -> [[char]] - -Implementation --------------- - -> trace * ** *** -> ::= Trace -> [bool] || Strict arguments -> (rule * **) || Current rule -> (answer * ** ***) || Answer for uninstantiated rule -> (history * **) || History up to current rule -> (transformation * ** ***) || The applied action and subtraces - -*/ - -:: Trace sym var pvar - = Trace [Bool] - (Rule sym var) - (Answer sym var pvar) - (History sym var) - (Transformation sym var pvar) - -/* - -> transformation * ** *** -> ::= Reduce ** (trace * ** ***) | || Reduction of the graph by a rewrite rule -> Annotate (trace * ** ***) | || Addition of a strictness annotation to an argument -> Stop | || Stop symbolic reduction -> Instantiate (trace * ** ***) -> (trace * ** ***) || Instantiation - -*/ - -/* The abstraction transformation divides the subject graph into areas. - The abstraction operation is applied when a part or parts of the subject graph must be turned into closures. - There are two possibilities: closure to an existing function, and closure to a new function. - Each area becomes a new initial task expression, for which a trace is subsequently produced. - The root of each area is the same variable as its root in the original subject graph. - The arguments of each area are found back as the arguments of the initial rewrite rule of the subsequent trace. - The arguments of each area should be repeated for each of their occurrences in the area. - Alternatively, an area can become a backpointer to an earlier occurrence in the trace. - - Abstraction can happen for several reasons: - - [1] The result of the application of a primitive function is needed. - The abstracted area is the application of the primitive function alone. - It is "folded" to itself. - The abstracted area is not partially evaluated itself. - - [2] The strategy found an instance of a pattern in the history. - The old pattern had a function name attached. - The abstracted area is the pattern. It is folded to the named function. - The abstracted area is no longer partially evaluated. - - [3] The strategy found a cycle in the spine. - The abstracted area is the cyclic tail of the spine. - It is "folded" to itself (or maybe a special "cycle in spine" function). - The abstracted area is not partially evaluated itself. - In fact, the whole graph can be replaced with the "cycle in spine" operator, - though this may seem kind of opportunistic, - and just an optimisation of the optimisation process. - - [4] Partial evaluation of the graph had a new occurrence of the area (introduced recursion). - The current occurrence has no name attached. - The abstracted area is the recurring pattern. - It is abstracted, and a name is assigned to it. - It is folded to the assigned name. - The abstracted area is still partially evaluated by itself. - - [5] The graph is in root normal form. - The root node should be abstracted. - The root node must be "folded" to an application of itself. - The remainder must be partially evaluated. - - In all these cases, one specific area for abstraction is indicated. - This specific area may or may not be partially evaluated itself. - - The meaning of the Stop constructor should be changed. - It is no longer used to force stopping when abstraction is needed. - Instead, it is used when nothing at all is left to be done. -*/ - -:: Transformation sym var pvar - = Reduce var (Trace sym var pvar) - | Annotate (Trace sym var pvar) - | Stop - | Instantiate (Rgraph sym var) - (Trace sym var pvar) - (Trace sym var pvar) - -/* Disable the new abstraction node for now... - - | Abstract [Abstraction sym var pvar] - -:: Abstraction sym var pvar - = NewAbstraction (Trace sym var pvar) - | KnownAbstraction (Rule sym var) - - Alternatives for the Abstract constructor: - - Abstract [Trace sym var pvar] - together with: Backpointer (Trace sym var pvar) - - This means there is always a new trace after an area of the abstraction operator. - - However, the area is never really partially evaluated. - Instead, a trace is produced that immediately ends with the Stop operator. - - - - Abstract [Abstraction sym var pvar] - with - :: Abstraction sym var pvar - = NewAbstraction (Trace sym var pvar) - | OldAbstraction (Rule sym var) - - In this case, the abstraction also determines what happens to the area. - This may also happen in the former case, but here it's included. - The former seems better. -*/ - -/* - -> showtrace showa showb showc (Trace stricts rule answer history transf) -> = "(Trace "++ -> show (map strictchar stricts)++' ': -> showrule showa showb rule++' ': -> showanswer showa showb showc answer++' ': -> showhistory showa showb history++' ': -> showtransf showa showb showc transf++")" - -> showtransf showa showb showc -> = stf -> where stf (Reduce reductroot trace) = "(Reduce "++showb reductroot++' ':str trace++")" -> stf (Annotate trace) = "(Annotate "++str trace++")" -> stf Stop = "Stop" -> stf (Instantiate yestrace notrace) = "(Instantiate "++str yestrace++' ':str notrace++")" -> str = showtrace showa showb showc - -> strictchar :: bool -> char -> strictchar strict = cond strict '!' '-' - -> printtrace :: * -> (*->[char]) -> (**->[char]) -> (***->[char]) -> trace * ** *** -> [[char]] - -> printtrace sym showa showb showc -> = ptr -> where ptr (Trace stricts rule answer history transf) -> = (showa sym++' ':printrule' showa showb stricts rule (map fst history++answernodes answer)): -> indent " " (printanswer showa showb showc answer)++ -> printhistory showa showb history++ -> printtransf sym showa showb showc transf - -> printtransf :: * -> (*->[char]) -> (**->[char]) -> (***->[char]) -> transformation * ** *** -> [[char]] - -> printtransf sym showa showb showc -> = ptf -> where ptf (Reduce reductroot trace) = ("Reduce to "++showb reductroot):ptr trace -> ptf (Annotate trace) = "Annotate":ptr trace -> ptf Stop = ["Stop"] -> ptf (Instantiate yestrace notrace) = indent "I=> " (ptr yestrace)++ptr notrace -> ptr = printtrace sym showa showb showc - -> answernodes = foldoptional [] spinenodes - -> printrule' :: (*->[char]) -> (**->[char]) -> [bool] -> rule * ** -> [**] -> [char] - -> printrule' printa printb stricts rule anchors -> = concat (map2 annot stricts args')++"-> "++root' -> where graph = rulegraph rule; args = lhs rule; root = rhs rule -> (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 -rewrite rule, which can be found at the root of the tree. No folds have -been applied; this has to be done afterwards. - -> tips :: trace * ** *** -> [rule * **] - -> tips -> = oldtrace reduce annotate stop instantiate -> where reduce stricts rule answer history reductroot = id -> annotate stricts rule answer history = id -> stop stricts rule answer history = [rule] -> instantiate stricts rule answer history = (++) - - -Mapleaves maps a function onto the rules of the leaves of a trace. - -> mapleaves :: (rule * **->rule * **) -> trace * ** *** -> trace * ** *** - -> mapleaves f -> = foldtrace reduce annotate stop instantiate -> where reduce stricts rule answer history reductroot trace = Trace stricts rule answer history (Reduce reductroot trace) -> annotate stricts rule answer history trace = Trace stricts rule answer history (Annotate trace) -> stop stricts rule answer history = Trace stricts (f rule) answer history Stop -> instantiate stricts rule answer history yestrace notrace = Trace stricts rule answer history (Instantiate yestrace notrace) - -*/ - -foldtrace - :: ([Bool] (Rule sym var) (Answer sym var pvar) (History sym var) var .result -> .result) - ([Bool] (Rule sym var) (Answer sym var pvar) (History sym var) .result -> .result) - ([Bool] (Rule sym var) (Answer sym var pvar) (History sym var) -> .result) - ([Bool] (Rule sym var) (Answer sym var pvar) (History sym var) (Rgraph sym var) .result .result -> .result) - !.(Trace sym var pvar) - -> .result - -foldtransformation - :: ((Trace sym var pvar) -> .result) - (var .result -> .subresult) - (.result -> .subresult) - .subresult - ((Rgraph sym var) .result .result -> .subresult) - ([.absresult] -> .subresult) - ((Rule sym var) -> .absresult) - (.result -> .absresult) - !.(Transformation sym var pvar) - -> .subresult - -instance <<< (Trace sym var pvar) | toString sym & ==,toString,<<< var // & ==,toString,<<< pvar diff --git a/sucl/trace.icl b/sucl/trace.icl deleted file mode 100644 index 7cc9d4b..0000000 --- a/sucl/trace.icl +++ /dev/null @@ -1,376 +0,0 @@ -implementation module trace - -// $Id$ - -import spine -import history -import rule -import graph -import basic -import syntax -import StdEnv - -/* - -trace.lit - Symbolic reduction traces -===================================== - -Description ------------ - -This script implements traces of symbolic reduction, indicating what -happened and why. Representation functions for traces are also -provided. - -A trace is a possibly infinite tree, with the nodes labeled with a -rewrite rule, the strategy answer for that rewrite rule, and the -selected transformation according to the rewrite rule and the strategy -answer. If any transformation is applicable, then a list of subtrees is -present and indicates the result of applying the transformation to the -rewrite rule. This is a list because a transformation may return more -than one transformed rewrite rule. - ------------------------------------------------------------------------- - -Interface ---------- - -Exported identifiers: - -> %export -> trace || Type of a trace -> transformation || Type of applied transformation - -> foldtransformation || Break down a transformation -> mapleaves || Map a function on the rules at the leaves of a trace -> printtrace || Make a human-readable representation of a trace -> showtrace || Make a representation of a trace -> strictchar || Representation of strictness annotation -> tips || Determine tips of a finite trace - ------------------------------------------------------------- - -Implementation --------------- - -*/ - -:: Trace sym var pvar - = Trace [Bool] - (Rule sym var) - (Answer sym var pvar) - (History sym var) - (Transformation sym var pvar) - -/* The trace (and transformation) data structure provides a record of the - actions taken by the partial evaluation algorithm. When partial evaluation - is finished, the result is a trace which can be divided into sections - separated by abstraction nodes. Thus, abstraction nodes delimit sections. - - Each section gives rise to a generated function. The rewrite rules of the - function (or its case branches, whichever representation is chosen) - correspond to the abstraction nodes that delimited the bottom of the trace - section. The abstraction node at the top section can be forgotten as it - belongs to the above section. However, the state in the top node may be of - interest. - - The abstraction transformation divides the subject graph into areas. The - abstraction operation is applied when a part or parts of the subject graph - must be turned into closures. There are two possibilities: closure to an - existing function, and closure to a new function. Each area becomes a new - initial task expression, for which a trace is subsequently produced. The - root of each area is the same variable as its root in the original subject - graph. The arguments of each area are found back as the arguments of the - initial rewrite rule of the subsequent trace. The arguments of each area - should be repeated for each of their occurrences in the area. - Alternatively, an area can become a backpointer to an earlier occurrence in - the trace. - - Abstraction can happen for several reasons: - - [1] The result of the application of a primitive function is needed. - The abstracted area is the application of the primitive function alone. - It is "folded" to itself. - The abstracted area is not partially evaluated itself. - - [2] The strategy found an instance of a pattern in the history. - The old pattern had a function name attached. - The abstracted area is the pattern. It is folded to the named function. - The abstracted area is no longer partially evaluated. - - [3] The strategy found a cycle in the spine. - The abstracted area is the cyclic tail of the spine. - It is "folded" to itself (or maybe a special "cycle in spine" function). - The abstracted area is not partially evaluated itself. - In fact, the whole graph can be replaced with the "cycle in spine" operator, - though this may seem kind of opportunistic, - and just an optimisation of the optimisation process. - - [4] Partial evaluation of the graph had a new occurrence of the area (introduced recursion). - The current occurrence has no name attached. - The abstracted area is the recurring pattern. - It is abstracted, and a name is assigned to it. - It is folded to the assigned name. - The abstracted area is still partially evaluated by itself. - - [5] The graph is in root normal form. - The root node should be abstracted. - The root node must be "folded" to an application of itself. - The remainder must be partially evaluated. - - In all these cases, one specific area for abstraction is indicated. - This specific area may or may not be partially evaluated itself. - - The meaning of the Stop constructor should be changed. - It is no longer used to force stopping when abstraction is needed. - Instead, it is used when nothing at all is left to be done. -*/ - -:: Transformation sym var pvar - = Reduce var (Trace sym var pvar) - | Annotate (Trace sym var pvar) - | Stop - | Instantiate (Rgraph sym var) - (Trace sym var pvar) - (Trace sym var pvar) - -/* Disable the abstraction node for now... - - | Abstract [Abstraction sym var pvar] - -// Some abstractions (introduced recursion) spawn a fresh subtrace, but others -// just complete stop partial evaluation, folding to a known rule. - -:: Abstraction sym var pvar - = NewAbstraction (Trace sym var pvar) - | KnownAbstraction (Rule sym var) - -> showtrace showa showb showc (Trace stricts rule answer history transf) -> = "(Trace "++ -> show (map strictchar stricts)++' ': -> showrule showa showb rule++' ': -> showanswer showa showb showc answer++' ': -> showhistory showa showb history++' ': -> showtransf showa showb showc transf++")" - -> showtransf showa showb showc -> = stf -> where stf (Reduce reductroot trace) = "(Reduce "++showb reductroot++' ':str trace++")" -> stf (Annotate trace) = "(Annotate "++str trace++")" -> stf Stop = "Stop" -> stf (Instantiate yestrace notrace) = "(Instantiate "++str yestrace++' ':str notrace++")" -> str = showtrace showa showb showc - -> strictchar :: bool -> char -> strictchar strict = cond strict '!' '-' - -> printtrace :: * -> (*->[char]) -> (**->[char]) -> (***->[char]) -> trace * ** *** -> [[char]] - -> printtrace sym showa showb showc -> = ptr -> where ptr (Trace stricts rule answer history transf) -> = (showa sym++' ':printrule' showa showb stricts rule (map fst history++answernodes answer)): -> indent " " (printanswer showa showb showc answer)++ -> printhistory showa showb history++ -> printtransf sym showa showb showc transf - -> printtransf :: * -> (*->[char]) -> (**->[char]) -> (***->[char]) -> transformation * ** *** -> [[char]] - -> printtransf sym showa showb showc -> = ptf -> where ptf (Reduce reductroot trace) = ("Reduce to "++showb reductroot):ptr trace -> ptf (Annotate trace) = "Annotate":ptr trace -> ptf Stop = ["Stop"] -> ptf (Instantiate yestrace notrace) = indent "I=> " (ptr yestrace)++ptr notrace -> ptr = printtrace sym showa showb showc - -> answernodes = foldoptional [] spinenodes - -> printrule' :: (*->[char]) -> (**->[char]) -> [bool] -> rule * ** -> [**] -> [char] - -> printrule' printa printb stricts rule anchors -> = concat (map2 annot stricts args')++"-> "++root' -> where graph = rulegraph rule; args = lhs rule; root = rhs rule -> (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 -rewrite rule, which can be found at the root of the tree. No folds have -been applied; this has to be done afterwards. - -> tips :: trace * ** *** -> [rule * **] - -> tips -> = foldtrace reduce annotate stop instantiate -> where reduce stricts rule answer history reductroot = id -> annotate stricts rule answer history = id -> stop stricts rule answer history = [rule] -> instantiate stricts rule answer history = (++) - - -Mapleaves maps a function onto the rules of the leaves of a trace. - -> mapleaves :: (rule * **->rule * **) -> trace * ** *** -> trace * ** *** - -> mapleaves f -> = foldtrace reduce annotate stop instantiate -> where reduce stricts rule answer history reductroot trace = Trace stricts rule answer history (Reduce reductroot trace) -> annotate stricts rule answer history trace = Trace stricts rule answer history (Annotate trace) -> stop stricts rule answer history = Trace stricts (f rule) answer history Stop -> instantiate stricts rule answer history yestrace notrace = Trace stricts rule answer history (Instantiate yestrace notrace) - -*/ - -foldtrace - :: ([Bool] (Rule sym var) (Answer sym var pvar) (History sym var) var .result -> .result) - ([Bool] (Rule sym var) (Answer sym var pvar) (History sym var) .result -> .result) - ([Bool] (Rule sym var) (Answer sym var pvar) (History sym var) -> .result) - ([Bool] (Rule sym var) (Answer sym var pvar) (History sym var) (Rgraph sym var) .result .result -> .result) - !.(Trace sym var pvar) - -> .result - -foldtrace reduce annotate stop instantiate trace -= ftr trace - where ftr (Trace stricts rule answer history transf) - = ftf stricts rule answer history transf - ftf stricts rule answer history (Reduce reductroot trace) = reduce stricts rule answer history reductroot (ftr 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 ipattern yestrace notrace) = instantiate stricts rule answer history ipattern (ftr yestrace) (ftr notrace) -// ftf _ _ _ _ (Abstract _) = error "foldtrace not implemented for abstraction nodes" - -foldtransformation - :: ((Trace sym var pvar) -> .result) - (var .result -> .subresult) - (.result -> .subresult) - .subresult - ((Rgraph sym var) .result .result -> .subresult) - ([.absresult] -> .subresult) - ((Rule sym var) -> .absresult) - (.result -> .absresult) - !.(Transformation sym var pvar) - -> .subresult - -foldtransformation ftr reduce annotate stop instantiate abstract knownabstraction newabstraction transf -= ftf transf - where ftf (Reduce reductroot trace) = reduce reductroot (ftr trace) - ftf (Annotate trace) = annotate (ftr trace) - ftf Stop = stop - ftf (Instantiate ipattern yestrace notrace) = instantiate ipattern (ftr yestrace) (ftr notrace) -// 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 // & ==,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 - // <<< "History:" <<< nl - // writeHistory history - <<< "Transformation:" <<< nl writeTransformation transf - where (Trace stricts rule answer history transf) = trace - -(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 - (<<<) file (Instantiate ipattern yestrace notrace) - = file <<< "Instantiate" <<< nl - // <<< "Pattern: " <<< ipattern <<< nl - <<< "Successful match..." <<< nl - <<< yestrace - <<< "End of successful match." <<< nl - <<< "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 ipattern yestrace notrace) -= file <<< "Instantiate" <<< nl - // <<< "Pattern: " <<< ipattern <<< 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 deleted file mode 100644 index 09b2467..0000000 --- a/sucl/trd.dcl +++ /dev/null @@ -1,25 +0,0 @@ -definition module trd - -// $Id$ - -from rule import Rule -from graph import Node -from StdOverloaded import == - -/* -`Ruletype theap symtype rule' determines the type of `rule'. -`Theap' must be an endless supply of type variables. -`Symtype' associates type rules with the symbols that occur in `rule'. - -If typing does not succeed, the function aborts. -*/ - -ruletype - :: .[tvar] - ((Node sym var) -> Rule tsym trvar) - (Rule sym var) - -> .Rule tsym tvar - | == var - & == tsym - & == tvar - & == trvar diff --git a/sucl/trd.icl b/sucl/trd.icl deleted file mode 100644 index 2a7d151..0000000 --- a/sucl/trd.icl +++ /dev/null @@ -1,206 +0,0 @@ -implementation module trd - -// $Id$ - -import rule -import graph -import basic -from general import ---> -import StdEnv - -/* - -trd.lit - Type rule derivation -============================== - -Description ------------ - -This module defines the derivation of a type rule from a given rule. - ------------------------------------------------------------- - -Interface ---------- - -Exported identifiers: - -> %export -> ruletype || Derive a type rule from a rule - ------------------------------------------------------------- - -Includes --------- - -> %include "basic.lit" -> %include "pfun.lit" -> %include "graph.lit" -> %include "rule.lit" - -Naming conventions: - - * - symbol (sym) - ** - node (node) - *** - type symbol (tsym) - **** - type node in type rule to build (tnode) - ***** - type node in given type rules (trnode) - ------------------------------------------------------------- - -Implementation --------------- - -`Ruletype' determines the type of a rule. - -First, for every closed node, its type rule is copied into a global -(initially unconnected) type graph, and for every open node, a distinct -type node is allocated in the same type graph. Then for every closed -node n and argument n-i, the result type of n-i is unified with the i-th -argument type of n. - -> ruletype -> :: [****] -> -> ((*,[**])->rule *** *****) -> -> rule * ** -> -> rule *** **** - -> ruletype theap typerule rule -> = foldr (buildtype typerule graph) bcont nodes theap emptygraph [] -> where args = lhs rule; root = rhs rule; graph = rulegraph rule -> nodes = nodelist graph (root:args) -> bcont theap tgraph assignment -> = foldr sharepair spcont pairs id tgraph assignment -> where pairs = mkpairs assignment -> spcont redirection tgraph assignment -> = mkrule (map lookup args) (lookup root) tgraph -> where lookup = redirection.foldmap id notype assignment -> notype = error "ruletype: no type node assigned to node" - -*/ - -ruletype - :: .[tvar] - ((Node sym var) -> Rule tsym trvar) - (Rule sym var) - -> .Rule tsym tvar - | == var - & == tsym - & == tvar - & == trvar - -ruletype theap typerule rule -= foldr (buildtype typerule graph) bcont nodes theap emptygraph [] - where args = arguments rule - root = ruleroot rule - graph = rulegraph rule - nodes = varlist graph [root:args] - bcont theap tgraph assignment - = foldr sharepair spcont pairs id tgraph assignment - where pairs = mkpairs assignment - spcont redirection tgraph assignment - = mkrule (map lookup args) (lookup root) tgraph - where lookup = redirection o (foldmap id notype assignment) - notype = abort "ruletype: no type node assigned to node" - -/* - -`Buildtype' builds the part of the global type graph corresponding to a -node. For a closed node, the type rule is copied; for an open node, a -single type node is allocated. Track is kept of which type nodes have -been assigned to the node and its arguments. - -*/ - -buildtype - :: .((Node sym var) -> Rule tsym trvar) // Assignement of type rules to symbols - .(Graph sym var) // Graph to which to apply typing - var // ??? - .([tvar] -> .(u:(Graph tsym tvar) -> .(v:[w:(var,tvar)] -> .result))) // Continuation - .[tvar] // Type heap - u:(Graph tsym tvar) // Type graph build so far - x:[y:(var,tvar)] // Assignment of type variables to variables - -> .result // Final result - | == var - & == trvar - , [x<=v,v y<=w,x<=y] - -buildtype typerule graph node bcont theap tgraph assignment -| def -= bcont theap` tgraph` assignment` -= bcont (tl theap) tgraph [(node,hd theap):assignment] - where (def,cont) = varcontents graph node - (_,args) = cont - trule = typerule cont - trargs = arguments trule; trroot = ruleroot trule; trgraph = rulegraph trule - trnodes = varlist trgraph [trroot:trargs] - (tnodes,theap`) = (claim--->"basic.claim begins from trd.buildtype") trnodes theap - matching = zip2 trnodes tnodes - tgraph` = foldr addnode tgraph matching - addnode (trnode,tnode) - | trdef - = updategraph tnode (mapsnd (map match) trcont) - = id - where (trdef,trcont) = varcontents trgraph trnode - match = foldmap id nomatch matching - nomatch = abort "buildtype: no match from type rule node to type node" - assignment` = zip2 [node:args] (map match [trroot:trargs])++assignment - -sharepair - :: (.var,.var) // Variables to share - w:((.var->var2) -> v:((Graph sym var2) -> .result)) // Continuation - (.var->var2) // Redirection - (Graph sym var2) // Graph before redirection - -> .result // Final result - | == sym - & == var2 - , [v<=w] - -sharepair lrnode spcont redirection graph -= share (mappair redirection redirection lrnode) spcont redirection graph - -/* - -`Share' shares two nodes in a graph by redirecting all references from -one to the other, and sharing the arguments recursively. The resulting -redirection function is also returned. - -*/ -/* -share :: - (var,var) // Variables to share - ((var->var) (Graph sym var) -> result) // Continuation - (var->var) // Redirection - (Graph sym var) // Graph before redirection - -> result | == sym & == var // Final result -*/ -share lrnode scont redirect graph -| lnode==rnode -= scont redirect graph -| ldef && rdef -= foldr share scont lrargs redirect` graph` -= scont redirect` graph` - where (lnode,rnode) = lrnode - (ldef,(lsym,largs)) = varcontents graph lnode - (rdef,(rsym,rargs)) = varcontents graph rnode - lrargs - | lsym<>rsym - = abort "share: incompatible symbols" - | not (eqlen largs rargs) - = abort "share: incompatible arities" - = zip2 (redargs largs) (redargs rargs) - redargs = map adjustone - redirect` = adjustone o redirect - adjustone - | ldef - = adjust rnode lnode id - = adjust lnode rnode id - graph` = redirectgraph adjustone graph -/* -mkpairs :: [(var1,var2)] -> [(var2,var2)] | == var1 -*/ -mkpairs pairs -= f (map snd (partition fst snd pairs)) - where f [[x1,x2:xs]:xss] = [(x1,x2):f [[x2:xs]:xss]] - f [xs:xss] = f xss - f [] = [] |