diff options
Diffstat (limited to 'sucl')
45 files changed, 7937 insertions, 0 deletions
diff --git a/sucl/Makefile b/sucl/Makefile new file mode 100644 index 0000000..3fd52bf --- /dev/null +++ b/sucl/Makefile @@ -0,0 +1,36 @@ +COCL = cocl +#COCLFLAGS = -lat +SYS = Clean\ System\ Files + +MODULES = basic pretty pfun graph dnc rule trd rewr complete history spine trace absmodule spine strat loop law + +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) + +%: $(SYS)/%.abc + @: + +$(SYS)/%.abc: %.icl + $(COCL) $(COCLFLAGS) $* + +$(SYS)/law.abc: law.icl law.dcl +$(SYS)/loop.abc: loop.icl loop.dcl trace.dcl strat.dcl history.dcl rule.dcl graph.dcl basic.dcl +$(SYS)/strat.abc: strat.icl strat.dcl history.dcl spine.dcl dnc.dcl rule.dcl graph.dcl pfun.dcl basic.dcl +$(SYS)/history.abc: history.icl history.dcl spine.dcl rule.dcl graph.dcl basic.dcl +$(SYS)/spine.abc: spine.icl spine.dcl rule.dcl pfun.dcl basic.dcl +$(SYS)/absmodule.abc: absmodule.icl absmodule.dcl rule.dcl +$(SYS)/trace.abc: trace.icl trace.dcl rule.dcl +$(SYS)/complete.abc: complete.icl complete.dcl graph.dcl +$(SYS)/rewr.abc: rewr.icl rewr.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 diff --git a/sucl/absmodule.dcl b/sucl/absmodule.dcl new file mode 100644 index 0000000..4b22b79 --- /dev/null +++ b/sucl/absmodule.dcl @@ -0,0 +1,13 @@ +definition module absmodule + +from rule import Rule + +:: Module sym pvar tsym tvar + = { exportedtypesymbols :: [tsym] // Exported type symbols (from DCL) + , typealias :: [(tsym,Rule tsym tvar)] // Alias types + , typeconstructors :: [(tsym,[sym])] // All constructor symbols of each declared algebraic type + , exportedsymbols :: [sym] // Exported function/constructor symbols + , aliases :: [(sym,Rule sym pvar)] // Macros + , typerules :: [(sym,Rule tsym tvar,[Bool])] // Info from type rules (actual type and argument strictnesses) + , rules :: [(sym,[Rule sym pvar])] // Rewrite rules of each symbol, absent if imported + } diff --git a/sucl/absmodule.icl b/sucl/absmodule.icl new file mode 100644 index 0000000..92addeb --- /dev/null +++ b/sucl/absmodule.icl @@ -0,0 +1,73 @@ +implementation module absmodule + +import rule + +/* + +------------------------------------------------------------------------ +Exports. + +> %export +> module +> addtalias +> addtsymdef +> addalias +> addsymdef +> newmodule + +------------------------------------------------------------------------ +Includes. + +> %include "basic.lit" +> %include "graph.lit" -extgraph +> %include "rule.lit" + +------------------------------------------------------------------------ +Module implementation. + +> module * *** **** ***** +> == ( ( [****], || Exported types +> [(****,rule **** *****)], || Type alias rules +> [(****,[*])] || Constructor symbols for algebraic type symbol +> ), +> ( [*], || Exported symbols +> [(*,rule * ***)], || Alias rules +> [(*,(rule **** *****,[bool]))], || Typerule for symbol +> [(*,[rule * ***])] || Rewrite rules for symbol, absent if imported +> ) +> ) + +*/ + +:: Module sym pvar tsym tvar + = { exportedtypesymbols :: [tsym] // Exported type symbols (from DCL) + , typealias :: [(tsym,Rule tsym tvar)] // Alias types + , typeconstructors :: [(tsym,[sym])] // All constructor symbols of each declared algebraic type + , exportedsymbols :: [sym] // Exported function/constructor symbols + , aliases :: [(sym,Rule sym pvar)] // Macros + , typerules :: [(sym,Rule tsym tvar,[Bool])] // Info from type rules (actual type and argument strictnesses) + , rules :: [(sym,[Rule sym pvar])] // Rewrite rules of each symbol, absent if imported + } + +/* + +> newmodule :: module * *** **** ***** +> newmodule = (([],[],[]),([],[],[],[])) + +> addtalias :: **** -> bool -> rule **** ***** -> module * *** **** ***** -> module * *** **** ***** +> addtalias ts exp tr ((tes,tas,tcs),defs) +> = ((cond exp (ts:tes) tes,(ts,tr):tas,tcs),defs) + +> addtsymdef :: **** -> bool -> [*] -> module * *** **** ***** -> module * *** **** ***** +> addtsymdef ts exp ss ((tes,tas,tcs),defs) +> = ((cond exp (ts:tes) tes,tas,(ts,ss):tcs),defs) + +> addalias :: * -> bool -> rule * *** -> module * *** **** ***** -> module * *** **** ***** +> addalias s exp r (tdefs,(es,as,ts,rs)) +> = (tdefs,(cond exp (s:es) es,(s,r):as,ts,rs)) + +> addsymdef :: * -> bool -> rule **** ***** -> bool -> [rule * ***] -> module * *** **** ***** -> module * *** **** ***** +> addsymdef s exp t imp rr (tdefs,(es,as,ts,rs)) +> = (tdefs,(cond exp (s:es) es,as,(s,(t,[])):ts,cond imp rs ((s,rr):rs))) + +*/ diff --git a/sucl/basic.dcl b/sucl/basic.dcl new file mode 100644 index 0000000..59558cc --- /dev/null +++ b/sucl/basic.dcl @@ -0,0 +1,168 @@ +definition module basic + +/* + +Basic definitions +================= + +Description +----------- + +Basic types and functions. + +*/ + +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 + + +// 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 + +// `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 + +// 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] + +// `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]] + +// 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 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] + +// 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 + +// `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 + +// `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 + +// `Superset xs ys' determines whether ys is a superset (actually, super-multi-set or super-list) of xs. +superset :: .[a] -> .(.[a] -> Bool) | == a diff --git a/sucl/basic.icl b/sucl/basic.icl new file mode 100644 index 0000000..f1ffb70 --- /dev/null +++ b/sucl/basic.icl @@ -0,0 +1,243 @@ +implementation module basic + +/* + +Basic definitions +================= + +Description +----------- + +Basic types and functions. + +*/ + +import StdEnv + +/* + +Implementation +-------------- + +*/ + +:: Optional t = Absent | Present t + + +// 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] (seen,rest) + | isMember x seen + = collect xs (seen,rest) + = (seen``,[y:rest``]) + where (seen`,rest``) = collect (generate y) ([x:seen],rest`) + (seen``,rest`) = collect xs ( seen`,rest) + y = process x + +// `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 + +// `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 (l,r) [] + = (l,r) +foldlr f (l,r) [x:xs] + = (l``,r``) + where (l``,r`) = foldlr f (l`,r) xs + (l`,r``) = f x (l,r`) + +foldmap :: (x:res -> w:res`) w:res` -> u:(![(arg,x:res)] -> v:(arg -> w:res`)) | == arg, [v u <= w, v <= x] +foldmap f d += foldr foldmap` (const d) + where foldmap` (x,y) g v = if (x==v) (f y) (g v) + +foldoptional :: .res .(.t -> .res) !(Optional .t) -> .res +foldoptional absent present Absent = absent +foldoptional absent present (Present x) = present x + +forget :: val -> .(![.(val,res)] -> .[(val,res)]) | == val +forget x = filter (neq x o fst) +neq x y = x <> y + +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 + +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 Absent = "" +printoptional printa (Present 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 Absent = Absent +mapoptional f (Present x) = Present (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) + +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) + +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] + +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 + +showoptional :: .(.a -> .String) !(Optional .a) -> String +showoptional showa Absent = "Absent" +showoptional showa (Present a) = "(Present "+++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 + +superset :: .[a] -> .(.[a] -> Bool) | == a +superset set = isEmpty o (removeMembers set) diff --git a/sucl/canon.icl b/sucl/canon.icl new file mode 100644 index 0000000..98572eb --- /dev/null +++ b/sucl/canon.icl @@ -0,0 +1,120 @@ +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.uncurry typerule.split.relabel localheap + +> 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) + +> 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 + +> localheap = [0..] + +------------------------------------------------------------------------ + +> foldarea :: (rgraph * **->*) -> rgraph * ** -> (*,[**]) +> foldarea label rgraph +> = (label rgraph,foldsingleton single nosingle rgraph) +> where single root sym args = args +> nosingle = snd (nodeset (rgraphgraph rgraph) [rgraphroot 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 = nodecontents 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 + +> 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 diff --git a/sucl/clean.icl b/sucl/clean.icl new file mode 100644 index 0000000..0451a4d --- /dev/null +++ b/sucl/clean.icl @@ -0,0 +1,441 @@ +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 new file mode 100644 index 0000000..311bd0f --- /dev/null +++ b/sucl/cli.icl @@ -0,0 +1,245 @@ +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 == 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 + +> typerule (tdefs,(es,as,ts,rs)) = fst.maxtypeinfo ts + +> 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 + +> maxtypeinfo :: [(symbol,(rule typesymbol typenode,[bool]))] -> symbol -> (rule typesymbol typenode,[bool]) +> maxtypeinfo ts = extendfn ts coretypeinfo + +> extendfn :: [(*,**)] -> (*->**) -> * -> ** +> extendfn mapping f x = foldmap id (f x) mapping x + +> constrs ((tes,tas,tcs),defs) = tcs + +> complete ((tes,tas,tcs),(es,as,ts,rs)) = mkclicomplete tcs (fst.maxtypeinfo ts) + +> 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) + +------------------------------------------------------------------------ + +> 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 diff --git a/sucl/complete.dcl b/sucl/complete.dcl new file mode 100644 index 0000000..42a9ee8 --- /dev/null +++ b/sucl/complete.dcl @@ -0,0 +1,17 @@ +definition module complete + +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 new file mode 100644 index 0000000..f84b69c --- /dev/null +++ b/sucl/complete.icl @@ -0,0 +1,144 @@ +implementation module complete + +import graph +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) = split pvarss + covered (sym,repvar`,pvarss`) = coveredby complete subject pvarss` (repvar (repvar` undef) svar++svars) + (sdef,(ssym,sargs)) = varcontents subject svar + tmpvalue = (fst (foldr (spl (repvar sargs) ssym) ([],[]) pvarss)) + +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. + +*/ + +split + :: [Pattern sym var] + -> ( [Pattern sym var] + , [ ( sym + , var->[var] + , [Pattern sym var] + ) + ] + ) + | == sym + & == var + +split [] = ([],[]) +split [(subject,[svar:svars]):svarss] +| not sdef += ([(subject,svars):opens`],map add closeds`) += (opens,[(ssym,repvar,[(subject,sargs++svars):ins]):closeds]) + where (opens`,closeds`) = split svarss + add (sym,repvar,svarss`) = (sym,repvar,[(subject,repvar svar++svars):svarss`]) + (opens,closeds) = split 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 new file mode 100644 index 0000000..0cef231 --- /dev/null +++ b/sucl/dnc.dcl @@ -0,0 +1,9 @@ +definition module dnc + +from graph import Graph,Node +from StdString 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 new file mode 100644 index 0000000..b17c08f --- /dev/null +++ b/sucl/dnc.icl @@ -0,0 +1,13 @@ +implementation module dnc + +import graph +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 new file mode 100644 index 0000000..bf65356 --- /dev/null +++ b/sucl/extract.icl @@ -0,0 +1,174 @@ +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 :: +> [**] -> +> [**] -> +> (rgraph * **->(*,[**])) -> +> (***->**->bool) -> +> (*,[***]) -> +> [(***,graph * ***)] -> +> rule * ** -> +> optional (rule * **,[rgraph * **]) + +> actualfold deltanodes rnfnodes foldarea self foldcont hist rule +> = Absent, if list3=[] +> = Present (mkrule rargs rroot rgraph'',areas'), otherwise +> where rargs = lhs rule; rroot = rhs rule; rgraph = rulegraph rule + +> list2 = map (pairwith (findoccs hist rule)) (nodelist rgraph [rroot]--nodelist rgraph rargs) +> || list2: list combining every node with list of every instantiable history graph + +> list3 = [(rnode,hgraph,mapping)|(rnode,(((hroot,hgraph),mapping):rest))<-list2] +> || list3: list combining every instantiable node with first instantiable history graph + +> rgraph' +> = foldr foldrec rgraph list3 +> where foldrec (rnode,hgraph,mapping) = updategraph rnode (mapsnd (map (lookup mapping)) foldcont) + +> (rgraph'',areas') = finishfold foldarea fixednodes singlenodes rroot rgraph' +> fixednodes = intersect (mkset (argnodes++foldednodes++rnfnodes)) (nodelist rgraph' [rroot]) +> singlenodes = intersect deltanodes (nodelist rgraph' [rroot]) +> argnodes = nodelist rgraph' rargs +> foldednodes = map fst3 list3 + +> findoccs +> :: [(***,graph * ***)] -> +> rule * ** -> +> ** -> +> [((***,graph * ***),[(***,**)])] + +> findoccs hist rule rnode +> = [ ((hroot,hgraph),mapping) +> | ((hroot,hgraph),(seen,mapping,[]))<-list1 || Find instantiable history rgraphs... +> ; unshared rnode (hroot,hgraph) mapping || ...which don't have shared contents... +>|| ; ~self hroot rnode || ...and aren't the history graph itself +> ] +> where rargs = lhs rule; rroot = rhs 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 (nodeset hgraph [hroot])) +> outer = nodelist (prunegraph rnode rgraph) (rroot:rargs)--[rnode] + +------------------------------------------------------------------------ + + +Splitting a rule into areas to fold to a certain area + +> splitrule +> :: (rgraph * **->(*,[**])) -> +> [**] -> +> [**] -> +> rule * ** -> +> rgraph * ** -> +> (rule * **,[rgraph * **]) + +> splitrule fold rnfnodes deltanodes rule area +> = (mkrule rargs rroot rgraph'',area':areas) +> where + +> rargs = lhs rule; rroot = rhs rule; rgraph = rulegraph rule +> aroot = rgraphroot area; agraph = rgraphgraph area + +> (rgraph'',areas) = finishfold fold fixednodes deltanodes rroot rgraph' +> fixednodes = intersect (mkset (aroot:nodelist rgraph' rargs++rnfnodes)) (nodelist rgraph' [rroot]) +> rgraph' = updategraph aroot (fold area') rgraph +> area' = mkrgraph aroot agraph' +> agraph' = foldr addnode emptygraph ins +> ins = nodelist agraph [aroot]--outs +> outs = nodelist (prunegraph aroot rgraph) (rroot:rargs++snd (nodeset 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 * **->(*,[**])) -> +> [**] -> +> [**] -> +> ** -> +> graph * ** -> +> (graph * **,[rgraph * **]) + +> 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 = nodelist (prunegraph aroot graph) arearoots++fixednodes +> ins = aroot:nodelist graph [aroot]--outs_and_aroot +> generate area +> = snd (nodeset agraph [aroot])--fixednodes +> where aroot = rgraphroot area; agraph = rgraphgraph area +> arearoots = mkset (root:singlenodes++singfixargs)--fixednodes +> singfixargs = concat (map arguments (singlenodes++fixednodes)) + +> arguments node +> = args, if def +> = [], otherwise +> where (def,(sym,args)) = dnc (const "in finishfold/1") graph node + +> addnode node +> = updategraph node cnt, if def +> = id, otherwise +> where (def,cnt) = dnc (const "in finishfold/2") graph node diff --git a/sucl/frontend.dcl b/sucl/frontend.dcl new file mode 100644 index 0000000..82175e4 --- /dev/null +++ b/sucl/frontend.dcl @@ -0,0 +1,53 @@ +definition module frontend + +from scanner import SearchPaths +from general import Optional, Yes, No +import checksupport, transform, overloading + +:: FrontEndSyntaxTree + = { fe_icl :: !IclModule // The ICL being compiled + , fe_dcls :: !{#DclModule} // ? The DCLs that were imported + , fe_components :: !{!Group} // ? Component groups of functions + , fe_dclIclConversions ::!Optional {# Index} // ? + , fe_iclDclConversions ::!Optional {# Index} // ? + , fe_globalFunctions :: !IndexRange // ? + , fe_arrayInstances :: !IndexRange // ? + } + +:: FrontEndPhase + = FrontEndPhaseCheck + | FrontEndPhaseTypeCheck + | FrontEndPhaseConvertDynamics + | FrontEndPhaseTransformGroups + | FrontEndPhaseConvertModules + | FrontEndPhaseAll + +frontEndInterface + :: !FrontEndPhase // Up to where we want `frontEndInterface' to do its work + !Ident // ? Name of module being compiled + !SearchPaths // ? Where to look for input files + !{#DclModule} // Modules in the DCL cache + !{#FunDef} // Functions and macros in the DCL cache + !(Optional Bool) // List generated types (with or without attributes) + !*PredefinedSymbols // Symbols that are predefined in the Clean langauge (which?), from the DCL cache (?) + !*HashTable // ? ... from the DCL cache + !*Files // Original file system state + !*File // Original standard error stream state + !*File // Original standard io stream state + !*File // Original standard out stream state + (!Optional !*File) // ? TCL file (?) + !*Heaps // ? ... from the DCL cache + + -> ( !Optional *FrontEndSyntaxTree // Resulting syntax tree if successful + , !.{# FunDef } // ? Cached functions and macros (which?) + , !Int // ? Don't care (?) + , !Int // ? main_dcl_module_n (?) + , !*PredefinedSymbols // ? Symbols that are predefined in the Clean language + , !*HashTable // ? + , !*Files // Resulting file system state + , !*File // Resulting standard error stream state + , !*File // Resulting standard io stream state + , !*File // Resulting standard out stream state + , !Optional !*File // ? TCL file (?) + , !*Heaps // ? + ) diff --git a/sucl/frontend.icl b/sucl/frontend.icl new file mode 100644 index 0000000..cfd07e2 --- /dev/null +++ b/sucl/frontend.icl @@ -0,0 +1,388 @@ +implementation module frontend + +// vi:set tabstop=4 noet: + +import scanner, parse, postparse, check, type, trans, convertcases, overloading, utilities, convertDynamics, + convertimportedtypes, checkKindCorrectness, compilerSwitches, analtypes, generics, supercompile + +:: FrontEndSyntaxTree + = { fe_icl :: !IclModule + , fe_dcls :: !{#DclModule} + , fe_components :: !{!Group} + , fe_dclIclConversions ::!Optional {# Index} + , fe_iclDclConversions ::!Optional {# Index} + , fe_globalFunctions :: !IndexRange + , fe_arrayInstances :: !IndexRange + } + +// trace macro +(-*->) infixl +(-*->) value trace + :== value // ---> trace + +build_optional_icl_dcl_conversions :: !Int !(Optional {# Index}) -> Optional {# Index} +build_optional_icl_dcl_conversions size No + = Yes (buildIclDclConversions size {}) +build_optional_icl_dcl_conversions size (Yes dcl_icl_conversions) + = Yes (buildIclDclConversions size dcl_icl_conversions) + +buildIclDclConversions :: !Int !{# Index} -> {# Index} +buildIclDclConversions table_size dcl_icl_conversions + # dcl_table_size = size dcl_icl_conversions + icl_dcl_conversions = update_conversion_array 0 dcl_table_size dcl_icl_conversions (createArray table_size NoIndex) + = fill_empty_positions 0 table_size dcl_table_size icl_dcl_conversions + +where + update_conversion_array dcl_index dcl_table_size dcl_icl_conversions icl_conversions + | dcl_index < dcl_table_size + # icl_index = dcl_icl_conversions.[dcl_index] + = update_conversion_array (inc dcl_index) dcl_table_size dcl_icl_conversions + { icl_conversions & [icl_index] = dcl_index } + = icl_conversions + + fill_empty_positions next_index table_size next_new_index icl_conversions + | next_index < table_size + | icl_conversions.[next_index] == NoIndex + = fill_empty_positions (inc next_index) table_size (inc next_new_index) { icl_conversions & [next_index] = next_new_index } + = fill_empty_positions (inc next_index) table_size next_new_index icl_conversions + = icl_conversions + +:: FrontEndOptions + = { feo_upToPhase :: !FrontEndPhase // How much of the frontend to execute + feo_search_paths :: !SearchPaths // Folders in which to search for files + feo_typelisting :: !Optional !Bool // Whether to list derived types, and if so whether to list attributes + feo_fusionstyle :: !FusionStyle // What type of fusion to perform + } + +:: FrontEndPhase + = FrontEndPhaseCheck + | FrontEndPhaseTypeCheck + | FrontEndPhaseConvertDynamics + | FrontEndPhaseTransformGroups + | FrontEndPhaseConvertModules + | FrontEndPhaseAll + +:: FusionStyle + = FS_online // Do online fusion (supercompilation) + | FS_offline // Do offline fusion (deforestation) + | FS_none // Do no fusion + +instance == FrontEndPhase where + (==) a b + = equal_constructor a b + +frontSyntaxTree cached_functions_and_macros n_functions_and_macros_in_dcl_modules main_dcl_module_n predef_symbols hash_table files error io out tcl_file icl_mod dcl_mods fun_defs components array_instances optional_dcl_icl_conversions + global_fun_range heaps + :== (Yes { + fe_icl = {icl_mod & icl_functions=fun_defs } + , fe_dcls = dcl_mods + , fe_components = components + , fe_dclIclConversions = optional_dcl_icl_conversions + , fe_iclDclConversions = build_optional_icl_dcl_conversions (size fun_defs) optional_dcl_icl_conversions + , fe_globalFunctions = global_fun_range + , fe_arrayInstances = array_instances + },cached_functions_and_macros,n_functions_and_macros_in_dcl_modules,main_dcl_module_n,predef_symbols,hash_table,files,error,io,out,tcl_file,heaps + ) + +//frontEndInterface :: !FrontEndPhase !Ident !SearchPaths !{#DclModule} !{#FunDef} !(Optional Bool) !*PredefinedSymbols !*HashTable !*Files !*File !*File !*File !*File !*Heaps -> ( !Optional *FrontEndSyntaxTree,!.{# FunDef },!Int,!Int,!*PredefinedSymbols, !*HashTable, !*Files, !*File !*File, !*File, !*File, !*Heaps) +frontEndInterface :: !FrontEndOptions !Ident !{#DclModule} !{#FunDef} !*PredefinedSymbols !*HashTable !*Files !*File !*File !*File (!Optional !*File) !*Heaps + -> ( !Optional *FrontEndSyntaxTree,!.{# FunDef },!Int,!Int,!*PredefinedSymbols, !*HashTable, !*Files, !*File, !*File, !*File, !Optional !*File, !*Heaps) + +frontEndInterface opts mod_ident dcl_modules functions_and_macros predef_symbols hash_table files error io out tcl_file heaps + # {feo_upToPhase=upToPhase, feo_search_paths=search_paths,feo_list_inferred_types=list_inferred_types} = opts + # (ok, mod, hash_table, error, predef_symbols, files) + = wantModule cWantIclFile mod_ident NoPos (hash_table /* ---> ("Parsing:", mod_ident)*/) error search_paths predef_symbols files + | not ok + = (No,{},0,0,predef_symbols, hash_table, files, error, io, out, tcl_file, heaps) + # cached_module_idents = [dcl_mod.dcl_name \\ dcl_mod<-:dcl_modules] + # (ok, mod, global_fun_range, mod_functions, optional_dcl_mod, modules, dcl_module_n_in_cache,n_functions_and_macros_in_dcl_modules,hash_table, error, predef_symbols, files) + = scanModule (mod -*-> "Scanning") cached_module_idents (size functions_and_macros) hash_table error search_paths predef_symbols files + /* JVG: */ +// # hash_table = {hash_table & hte_entries={}} + # hash_table = remove_icl_symbols_from_hash_table hash_table + /**/ + | not ok + = (No,{},0,0,predef_symbols, hash_table, files, error, io, out, tcl_file, heaps) + # symbol_table = hash_table.hte_symbol_heap + (ok, icl_mod, dcl_mods, components, optional_dcl_icl_conversions,cached_functions_and_macros,main_dcl_module_n,heaps, predef_symbols, symbol_table, error /* TD */, directly_imported_dcl_modules) + = checkModule mod global_fun_range mod_functions n_functions_and_macros_in_dcl_modules dcl_module_n_in_cache optional_dcl_mod modules dcl_modules functions_and_macros predef_symbols (symbol_table -*-> "Checking") error heaps + hash_table = { hash_table & hte_symbol_heap = symbol_table} + + | not ok + = (No,{},0,main_dcl_module_n,predef_symbols, hash_table, files, error, io, out, tcl_file, heaps) + + #! (icl_functions,icl_mod) = select_and_remove_icl_functions_from_record icl_mod + with + select_and_remove_icl_functions_from_record :: !*IclModule -> (!.{#FunDef},!.IclModule) + select_and_remove_icl_functions_from_record icl_mod=:{icl_functions} = (icl_functions,{icl_mod & icl_functions={}}) + +// # {icl_functions,icl_instances,icl_specials,icl_common,icl_import} = icl_mod + # {icl_instances,icl_specials,icl_common,icl_import,icl_name,icl_imported_objects,icl_used_module_numbers} = icl_mod +/* + (_,f,files) = fopen "components" FWriteText files + (components, icl_functions, f) = showComponents components 0 True icl_functions f + (ok,files) = fclose f files + | ok<>ok + = abort ""; +*/ +// dcl_mods = {{dcl_mod & dcl_declared={dcls_import=[],dcls_local=[],dcls_explicit=[]}}\\ dcl_mod<-:dcl_mods} +// # dcl_mods = {{dcl_mod & dcl_declared={dcls_import={},dcls_local=[],dcls_local_for_import={},dcls_explicit={}}}\\ dcl_mod<-:dcl_mods} + + # var_heap = heaps.hp_var_heap + type_heaps = heaps.hp_type_heaps + fun_defs = icl_functions + array_instances = {ir_from=0, ir_to=0} + + | upToPhase == FrontEndPhaseCheck + = frontSyntaxTree cached_functions_and_macros n_functions_and_macros_in_dcl_modules main_dcl_module_n predef_symbols hash_table files error io out tcl_file icl_mod dcl_mods fun_defs components array_instances optional_dcl_icl_conversions global_fun_range heaps + +// AA.. + # error_admin = {ea_file = error, ea_loc = [], ea_ok = True } + # (ti_common_defs, dcl_mods) = get_common_defs dcl_mods + ti_common_defs = { ti_common_defs & [main_dcl_module_n] = icl_common } + # (td_infos, type_heaps, error_admin) = analTypeDefs ti_common_defs icl_used_module_numbers type_heaps error_admin + (fun_defs, dcl_mods, th_vars, td_infos, error_admin) + = checkKindCorrectness main_dcl_module_n icl_instances + fun_defs ti_common_defs dcl_mods type_heaps.th_vars td_infos error_admin + type_heaps = { type_heaps & th_vars = th_vars } + # heaps = { heaps & hp_type_heaps = type_heaps } + # ti_common_defs = {dcl_common \\ {dcl_common} <-: dcl_mods } + # (saved_main_dcl_common, ti_common_defs) = replace ti_common_defs main_dcl_module_n icl_common + + #! (components, ti_common_defs, fun_defs, generic_range, td_infos, heaps, hash_table, predef_symbols, dcl_mods, optional_dcl_icl_conversions, error_admin) = + case SupportGenerics of + True -> convertGenerics + components main_dcl_module_n ti_common_defs fun_defs td_infos + heaps hash_table predef_symbols dcl_mods optional_dcl_icl_conversions error_admin + False -> (components, ti_common_defs, fun_defs, {ir_to=0,ir_from=0}, td_infos, heaps, hash_table, predef_symbols, dcl_mods, optional_dcl_icl_conversions, error_admin) + + # (icl_common, ti_common_defs) = replace copied_ti_common_defs main_dcl_module_n saved_main_dcl_common + with + copied_ti_common_defs :: !.{#CommonDefs} // needed for Clean 2.0 to disambiguate overloading of replace + copied_ti_common_defs = {x \\ x <-: ti_common_defs} + # dcl_mods = { {dcl_mod & dcl_common = common} \\ dcl_mod <-: dcl_mods & common <-: ti_common_defs } + + # error = error_admin.ea_file + #! ok = error_admin.ea_ok + | not ok + = (No,{},0,main_dcl_module_n,predef_symbols, hash_table, files, error, io, out, tcl_file, heaps) +// ..AA + + # (ok, fun_defs, array_instances, type_code_instances, common_defs, imported_funs, type_def_infos, heaps, predef_symbols, error,out) + = typeProgram (components -*-> "Typing") main_dcl_module_n fun_defs/*icl_functions*/ icl_specials list_inferred_types icl_common [a\\a<-:icl_import] dcl_mods icl_used_module_numbers td_infos heaps predef_symbols error out dcl_mods + + | not ok + = (No,{},0,main_dcl_module_n,predef_symbols, hash_table, files, error, io, out, tcl_file, heaps) + + + # (fun_def_size, fun_defs) = usize fun_defs + # (components, fun_defs) = partitionateFunctions (fun_defs -*-> "partitionateFunctions") [ global_fun_range, icl_instances, icl_specials, generic_range] + +// (components, fun_defs, error) = showTypes components 0 fun_defs error +// (components, fun_defs, error) = showComponents components 0 True fun_defs error +// (fun_defs, error) = showFunctions array_instances fun_defs error + + | upToPhase == FrontEndPhaseTypeCheck + = frontSyntaxTree cached_functions_and_macros n_functions_and_macros_in_dcl_modules main_dcl_module_n predef_symbols hash_table files error io out tcl_file icl_mod dcl_mods fun_defs components array_instances optional_dcl_icl_conversions global_fun_range heaps + + # (components, fun_defs, predef_symbols, dcl_types, used_conses_in_dynamics, var_heap, type_heaps, expression_heap, tcl_file) + = convertDynamicPatternsIntoUnifyAppls type_code_instances common_defs main_dcl_module_n (components -*-> "convertDynamics") fun_defs predef_symbols + heaps.hp_var_heap heaps.hp_type_heaps heaps.hp_expression_heap tcl_file dcl_mods icl_mod /* TD */ directly_imported_dcl_modules +// # (components, fun_defs, error) = showComponents3 components 0 False fun_defs error +// (components, fun_defs, error) = showComponents components 0 True fun_defs error + + | upToPhase == FrontEndPhaseConvertDynamics + # heaps = {hp_var_heap=var_heap, hp_type_heaps=type_heaps, hp_expression_heap=expression_heap} + = frontSyntaxTree cached_functions_and_macros n_functions_and_macros_in_dcl_modules main_dcl_module_n predef_symbols hash_table files error io out tcl_file icl_mod dcl_mods fun_defs components array_instances optional_dcl_icl_conversions global_fun_range heaps + +// (components, fun_defs, error) = showComponents components 0 True fun_defs error + +// VZ.. +// Select fusion style and do fusion + # (components, fun_defs, dcl_types, used_conses, var_heap, type_heaps, expression_heap) + = case opts.feo_fusionstyle of + FS_offline + # (cleanup_info, acc_args, components, fun_defs, var_heap, expression_heap) + = analyseGroups common_defs array_instances main_dcl_module_n (components -*-> "Analyse") fun_defs var_heap expression_heap + -> transformGroups cleanup_info main_dcl_module_n (components -*-> "Transform") fun_defs acc_args common_defs imported_funs dcl_types used_conses_in_dynamics type_def_infos var_heap type_heaps expression_heap + FS_online + -> supercompile common_defs array_instances main_dcl_module_n (components -*-> "Supercompile") fun_defs var_heap expression_heap imported_funs dcl_types used_conses_in_dynamics type_def_infos type_heaps + FS_none + -> (components, fun_defs, dcl_types, used_conses_in_dynamics, var_heap, expression_heap) +// ..VZ + + | upToPhase == FrontEndPhaseTransformGroups + # heaps = {hp_var_heap=var_heap, hp_type_heaps=type_heaps, hp_expression_heap=expression_heap} + = frontSyntaxTree cached_functions_and_macros n_functions_and_macros_in_dcl_modules main_dcl_module_n predef_symbols hash_table files error io out tcl_file icl_mod dcl_mods fun_defs components array_instances optional_dcl_icl_conversions global_fun_range heaps + + # (dcl_types, used_conses, var_heap, type_heaps) = convertIclModule main_dcl_module_n common_defs (dcl_types -*-> "Convert icl") used_conses var_heap type_heaps + # (dcl_types, used_conses, var_heap, type_heaps) = convertDclModule main_dcl_module_n dcl_mods common_defs (dcl_types -*-> "Convert dcl") used_conses var_heap type_heaps + +// (components, fun_defs, out) = showComponents components 0 False fun_defs out + + | upToPhase == FrontEndPhaseConvertModules + # heaps = {hp_var_heap=var_heap, hp_type_heaps=type_heaps, hp_expression_heap=expression_heap} + = frontSyntaxTree cached_functions_and_macros n_functions_and_macros_in_dcl_modules main_dcl_module_n predef_symbols hash_table files error io out tcl_file icl_mod dcl_mods fun_defs components array_instances optional_dcl_icl_conversions global_fun_range heaps + +// (components, fun_defs, out) = showComponents components 0 False fun_defs out + # (used_funs, components, fun_defs, dcl_types, used_conses, var_heap, type_heaps, expression_heap) + = convertCasesOfFunctions components main_dcl_module_n imported_funs common_defs fun_defs (dcl_types -*-> "Convert cases") used_conses + var_heap type_heaps expression_heap + #! (dcl_types, type_heaps, var_heap) + = convertImportedTypeSpecifications main_dcl_module_n dcl_mods imported_funs common_defs used_conses used_funs (dcl_types -*-> "Convert types") type_heaps var_heap + # heaps = {hp_var_heap = var_heap, hp_expression_heap=expression_heap, hp_type_heaps=type_heaps} +// (components, fun_defs, error) = showTypes components 0 fun_defs error +// (dcl_mods, out) = showDclModules dcl_mods out +// (components, fun_defs, out) = showComponents components 0 False fun_defs out + + #! fe ={ fe_icl = +// {icl_mod & icl_functions=fun_defs } + {icl_functions=fun_defs,icl_instances=icl_instances,icl_specials=icl_specials,icl_common=icl_common,icl_import=icl_import, + icl_name=icl_name,icl_imported_objects=icl_imported_objects,icl_used_module_numbers=icl_used_module_numbers } + + , fe_dcls = dcl_mods + , fe_components = components + , fe_dclIclConversions = optional_dcl_icl_conversions + , fe_iclDclConversions = build_optional_icl_dcl_conversions (size fun_defs) optional_dcl_icl_conversions + , fe_arrayInstances = array_instances,fe_globalFunctions=global_fun_range + } + = (Yes fe,cached_functions_and_macros,n_functions_and_macros_in_dcl_modules,main_dcl_module_n,predef_symbols,hash_table,files,error,io,out,tcl_file,heaps) + where + build_optional_icl_dcl_conversions :: !Int !(Optional {# Index}) -> Optional {# Index} + build_optional_icl_dcl_conversions size No + = Yes (build_icl_dcl_conversions size {}) + build_optional_icl_dcl_conversions size (Yes dcl_icl_conversions) + = Yes (build_icl_dcl_conversions size dcl_icl_conversions) + + build_icl_dcl_conversions :: !Int !{# Index} -> {# Index} + build_icl_dcl_conversions table_size dcl_icl_conversions + # dcl_table_size = size dcl_icl_conversions + icl_dcl_conversions = update_conversion_array 0 dcl_table_size dcl_icl_conversions (createArray table_size NoIndex) + = fill_empty_positions 0 table_size dcl_table_size icl_dcl_conversions + + update_conversion_array dcl_index dcl_table_size dcl_icl_conversions icl_conversions + | dcl_index < dcl_table_size + # icl_index = dcl_icl_conversions.[dcl_index] + = update_conversion_array (inc dcl_index) dcl_table_size dcl_icl_conversions + { icl_conversions & [icl_index] = dcl_index } + = icl_conversions + + fill_empty_positions next_index table_size next_new_index icl_conversions + | next_index < table_size + | icl_conversions.[next_index] == NoIndex + = fill_empty_positions (inc next_index) table_size (inc next_new_index) { icl_conversions & [next_index] = next_new_index } + = fill_empty_positions (inc next_index) table_size next_new_index icl_conversions + = icl_conversions + get_common_defs dcl_mods + #! size = size dcl_mods + # ({dcl_common=arbitrary_value_for_initializing}, dcl_mods) = dcl_mods![0] + = loop 0 (createArray size arbitrary_value_for_initializing) dcl_mods + where + loop :: !Int !*{#CommonDefs} !u:{#DclModule} -> (!*{#CommonDefs}, !u:{#DclModule}) + loop i common_defs dcl_mods + | i==size dcl_mods + = (common_defs, dcl_mods) + # ({dcl_common}, dcl_mods) = dcl_mods![i] + = loop (i+1) { common_defs & [i] = dcl_common } dcl_mods + +newSymbolTable :: !Int -> *{# SymbolTableEntry} +newSymbolTable size + = createArray size { ste_index = NoIndex, ste_def_level = -1, ste_kind = STE_Empty, ste_previous = abort "PreviousPlaceholder"} + +showFunctions :: !IndexRange !*{# FunDef} !*File -> (!*{# FunDef},!*File) +showFunctions {ir_from, ir_to} fun_defs file + = iFoldSt show_function ir_from ir_to (fun_defs, file) +where + show_function fun_index (fun_defs, file) + # (fd, fun_defs) = fun_defs![fun_index] + = (fun_defs, file <<< fun_index <<< fd <<< '\n') + +showComponents :: !*{! Group} !Int !Bool !*{# FunDef} !*File -> (!*{! Group}, !*{# FunDef},!*File) +showComponents comps comp_index show_types fun_defs file + | comp_index >= size comps + = (comps, fun_defs, file) + # (comp, comps) = comps![comp_index] + # (fun_defs, file) = show_component comp.group_members show_types fun_defs (file <<< "component " <<< comp_index <<< '\n') + = showComponents comps (inc comp_index) show_types fun_defs file +where + show_component [] show_types fun_defs file + = (fun_defs, file <<< '\n') + show_component [fun:funs] show_types fun_defs file + # (fun_def, fun_defs) = fun_defs![fun] + | show_types + = show_component funs show_types fun_defs (file <<< fun_def.fun_type <<< '\n' <<< fun_def) + = show_component funs show_types fun_defs (file <<< fun_def) +// = show_component funs show_types fun_defs (file <<< fun_def.fun_symb) + +showComponents2 :: !{! Group} !Int !*{# FunDef} !{! ConsClasses} !*File -> (!*{# FunDef},!*File) +showComponents2 comps comp_index fun_defs acc_args file + | comp_index >= (size comps) + = (fun_defs, file) + # (fun_defs, file) = show_component comps.[comp_index].group_members fun_defs acc_args file + = showComponents2 comps (inc comp_index) fun_defs acc_args file +where + show_component [] fun_defs _ file + = (fun_defs, file <<< '\n') + show_component [fun:funs] fun_defs acc_args file + # (fd, fun_defs) = fun_defs![fun] + # file = show_accumulating_arguments acc_args.[fun].cc_args (file <<< fd.fun_symb <<< '.' <<< fun <<< " (") + = show_component funs fun_defs acc_args (file <<< ") ") + + show_accumulating_arguments [ cc : ccs] file + | cc == cPassive + = show_accumulating_arguments ccs (file <<< 'p') + | cc == cActive + = show_accumulating_arguments ccs (file <<< 'c') + | cc == cAccumulating + = show_accumulating_arguments ccs (file <<< 'a') + = show_accumulating_arguments ccs (file <<< '?') + show_accumulating_arguments [] file + = file + + +show_components comps fun_defs = map (show_component fun_defs) comps + +show_component fun_defs [] = [] +show_component fun_defs [fun:funs] = [fun_defs.[fun ---> fun] : show_component fun_defs funs] + +showTypes :: !*{! Group} !Int !*{# FunDef} !*File -> (!*{! Group}, !*{# FunDef},!*File) +showTypes comps comp_index fun_defs file + | comp_index >= size comps + = (comps, fun_defs, file) + # (comp, comps) = comps![comp_index] + # (fun_defs, file) = show_types comp.group_members fun_defs (file <<< "component " <<< comp_index <<< '\n') + = showTypes comps (inc comp_index) fun_defs file +where + show_types [] fun_defs file + = (fun_defs, file <<< '\n') + show_types [fun:funs] fun_defs file + # (fun_def, fun_defs) = fun_defs![fun] + # properties = { form_properties = cAttributed bitor cAnnotated, form_attr_position = No } + (Yes ftype) = fun_def.fun_type + = show_types funs fun_defs (file <<< fun_def.fun_symb <<< " :: " <:: (properties, ftype, No) <<< '\n' ) + +showDclModules :: !u:{#DclModule} !*File -> (!u:{#DclModule}, !*File) +showDclModules dcl_mods file + = show_dcl_mods 0 dcl_mods file +where + show_dcl_mods mod_index dcl_mods file + # (size_dcl_mods, dcl_mods) = usize dcl_mods + | mod_index == size_dcl_mods + = (dcl_mods, file) + | otherwise + # (dcl_mod, dcl_mods) = dcl_mods ! [mod_index] + # file = show_dcl_mod dcl_mod file + = (dcl_mods, file) + + show_dcl_mod {dcl_name, dcl_functions} file + # file = file <<< dcl_name <<< ":\n" + # file = show_dcl_functions 0 dcl_functions file + = file <<< "\n" + show_dcl_functions fun_index dcl_functions file + | fun_index == size dcl_functions + = file + | otherwise + # file = show_dcl_function dcl_functions.[fun_index] file + = show_dcl_functions (inc fun_index) dcl_functions file + show_dcl_function {ft_symb, ft_type} file + = file <<< ft_symb <<< " :: " <<< ft_type <<< "\n" diff --git a/sucl/graph.dcl b/sucl/graph.dcl new file mode 100644 index 0000000..bd1738d --- /dev/null +++ b/sucl/graph.dcl @@ -0,0 +1,208 @@ +definition module graph + +from StdOverloaded import == + +// 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 | == 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 + +// 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 + +------------------------------------------------------------------------ + +> 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 + +*/ diff --git a/sucl/graph.icl b/sucl/graph.icl new file mode 100644 index 0000000..3e7f848 --- /dev/null +++ b/sucl/graph.icl @@ -0,0 +1,379 @@ +implementation module graph + +import pfun +import basic +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 + :== 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 = emptypfun + +updategraph :: .var (Node .sym .var) (Graph .sym .var) -> Graph .sym .var +updategraph var node graph = extend var node graph + +prunegraph :: .var (Graph .sym .var) -> Graph .sym .var +prunegraph var graph = restrict var graph + +restrictgraph :: !.[var] .(Graph sym var) -> Graph sym var | == var +restrictgraph vars graph = domres vars graph + +redirectgraph :: (.var->.var) !(Graph .sym .var) -> Graph .sym .var | == var +redirectgraph redirection graph += postcomp (mapsnd (map redirection)) graph + +overwritegraph :: !(Graph .sym .var) (Graph .sym .var) -> Graph .sym .var +overwritegraph newgraph oldgraph = overwrite newgraph 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 + +/* +> nodecontents +> = total (False,(nosym,noargs)).postcomp s +> where s x = (True,x) +> nosym = error "nodecontents: getting symbol of open node" +> noargs = error "nodecontents: getting arguments of open node" +*/ + +varcontents :: !(Graph .sym var) var -> (.Bool,Node .sym var) | == var +varcontents g v += (total (False,(nosym,noargs)) o postcomp found) g 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 (seen,boundfree=:(bound,free)) + | isMember var seen = (seen,boundfree) + | 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 + +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 + +> 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 + +inccounter m f n = if (n==m) (f n+1) (f n) + +/* + +Compilegraph compiles a graph from parts. +Uses in Miranda: + * reading a parsed program from a file. + +> compilegraph :: [(**,(*,[**]))] -> graph * ** +> compilegraph = foldr (uncurry updategraph) emptygraph + +`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) ([],[],[]))) + +/* + +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. + +> instantiate :: (graph * ***,graph * **) -> (***,**) -> ([(***,**)],[(***,**)],[(***,**)]) -> ([(***,**)],[(***,**)],[(***,**)]) + +> instantiate (pgraph,sgraph) (pnode,snode) (seen,mapping,errs) +> = (seen,mapping,errs), if member seen psnode +> = (psnode:seen,mapping,psnode:errs), if member (map fst seen) pnode +> = (psnode:seen,psnode:mapping,errs), if ~pdef +> = (psnode:seen,mapping,psnode:errs), if ~sdef +> = (psnode:seen,mapping,psnode:errs), if ~(psym=ssym&eqlen pargs sargs) +> = (seen',psnode:mapping',errs'), otherwise +> where (pdef,(psym,pargs)) = nodecontents pgraph pnode +> (sdef,(ssym,sargs)) = nodecontents sgraph snode +> (seen',mapping',errs') = instantiateargs (pgraph,sgraph) (zip2 pargs sargs) (psnode:seen,mapping,errs) +> psnode = (pnode,snode) + +`Instantiateargs' is the logical extension of `instantiate' to lists of node pairs. + +> instantiateargs :: (graph * ***,graph * **) -> [(***,**)] -> ([(***,**)],[(***,**)],[(***,**)]) -> ([(***,**)],[(***,**)],[(***,**)]) + +> instantiateargs psgraph [] = id +> instantiateargs psgraph (psnode:psnodes) (seen,mapping,errs) +> = (seen'',mapping'',errs'') +> where (seen',mapping'',errs'') = instantiate psgraph psnode (seen,mapping',errs') +> (seen'',mapping',errs') = instantiateargs psgraph psnodes (seen',mapping,errs) + +*/ + +:: 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 * ** -> 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 + +*/ diff --git a/sucl/history.dcl b/sucl/history.dcl new file mode 100644 index 0000000..70ff418 --- /dev/null +++ b/sucl/history.dcl @@ -0,0 +1,17 @@ +definition module history + +from spine import Spine +from rule import Rgraph +from graph import Graph + +from spine import Subspine // for Spine + +:: History sym var + :== [(var,[Rgraph sym var])] + +extendhistory + :: (Graph sym var) + (var -> var) + (Spine sym var pvar) + (History sym var) + -> History sym var diff --git a/sucl/history.icl b/sucl/history.icl new file mode 100644 index 0000000..c79accd --- /dev/null +++ b/sucl/history.icl @@ -0,0 +1,97 @@ +implementation module history + +import spine +import rule +import graph +import basic +import StdEnv + +:: History sym var + :== [(var,[Rgraph sym var])] + +/* + +> history * ** == [(**,[rgraph * **])] + +> showhistory :: (*->[char]) -> (**->[char]) -> history * ** -> [char] +> showhistory showa showb = showlist (showpair showb (showlist (showrgraph showa showb))) + +> printhistory :: (*->[char]) -> (**->[char]) -> history * ** -> [[char]] +> printhistory showa showb +> = concat.map print +> where print (node,rgraphs) +> = showb node:map2 (++) ("<= ":repeat " ") (map (printrgraph showa showb) rgraphs) + +*/ + +extendhistory + :: (Graph sym var) + (var -> var) + (Spine sym var pvar) + (History sym var) + -> History sym var + +extendhistory sgraph redirection spine history += snd (foldspine (extendpair sgraph redirection) d d id d (const d) (extendpartial sgraph) (const d) (extendredex sgraph history) d spine) + where d = (emptygraph,history) + +/* + +> extendpair :: graph * ** -> (**->**) -> ** -> (graph * **,history * **) -> (graph * **,history * **) +> extendpair sgraph redirect snode (hgraph,history) +> = (hgraph',remap (redirect snode) (mkrgraph snode hgraph':foldmap id [] history snode) (forget snode history)) +> where hgraph' = cond sdef (updategraph snode scont hgraph) hgraph +> (sdef,scont) = dnc (const "in extendpair") sgraph snode + +*/ + +extendpair + :: (Graph sym var) + (var->var) + var + (Graph sym var,History sym var) + -> (Graph sym var,History sym var) + +extendpair _ _ _ _ = undef + +/* + +> extendpartial :: graph * ** -> rule * *** -> pfun *** ** -> (graph * **,history * **) -> (graph * **,history * **) +> extendpartial sgraph rule matching (hgraph,history) +> = (extgraph' sgraph rule matching hgraph,history) + +*/ + +extendpartial + :: (Graph sym var) + (Rule sym pvar) + (Pfun pvar var) + (Graph sym var,History sym var) + -> (Graph sym var,History sym var) + +extendpartial _ _ _ _ = undef + +/* + +> extendredex :: graph * ** -> history * ** -> rule * *** -> pfun *** ** -> (graph * **,history * **) +> extendredex sgraph history rule matching +> = (extgraph' sgraph rule matching emptygraph,history) + +*/ + +extendredex + :: (Graph sym var) + (History sym var) + (Rule sym pvar) + (Pfun pvar var) + -> (Graph sym var,History sym var) + +extendredex _ _ _ _ = undef + +/* + +> extgraph' sgraph rule +> = extgraph sgraph rgraph (nodelist rgraph (lhs rule)) +> where rgraph = rulegraph rule + +*/ diff --git a/sucl/hunt.icl b/sucl/hunt.icl new file mode 100644 index 0000000..bd4c4e3 --- /dev/null +++ b/sucl/hunt.icl @@ -0,0 +1,49 @@ +>|| 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 new file mode 100644 index 0000000..e5564a5 --- /dev/null +++ b/sucl/law.dcl @@ -0,0 +1 @@ +definition module law diff --git a/sucl/law.icl b/sucl/law.icl new file mode 100644 index 0000000..836e3b3 --- /dev/null +++ b/sucl/law.icl @@ -0,0 +1,179 @@ +implementation module law + +/* + +> %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 +> = [(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 + +> 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" + +> 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 + +> 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 new file mode 100644 index 0000000..56f0a37 --- /dev/null +++ b/sucl/loop.dcl @@ -0,0 +1,29 @@ +definition module loop + +from strat import Strategy +from spine import Answer +from trace import Trace +from rule import Rgraph,Rule +from graph import Graph +from StdOverloaded import == + +from strat import Substrategy,Subspine // for Strategy +from graph import Node // for Strategy +from basic import Optional // for Answer +from spine import Spine // for Answer +from trace import History,Transformation // for Trace + +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 + +initrule + :: ![var] + (sym->[pvar]) + sym + -> ([var],Rule sym var) diff --git a/sucl/loop.icl b/sucl/loop.icl new file mode 100644 index 0000000..6ef0c7a --- /dev/null +++ b/sucl/loop.icl @@ -0,0 +1,247 @@ +implementation module loop + +import trace +import strat +import history +import spine +import rewr +import rule +import graph +import pfun +import basic +import StdEnv + +/* + +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. + +------------------------------------------------------------ + +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 + +loop strategy matchable (initheap,rule) += maketrace inithistory initfailinfo initinstdone initstricts initsroot initsubject initheap + + where maketrace history failinfo instdone stricts sroot subject heap + = Trace stricts (mkrule sargs sroot subject) answer history transf + where answer = makernfstrategy history (strategy matchable`) rnfnodes sroot subject + transf = transform 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) + + inithistory = [] + initfailinfo = const [] + initinstdone = False + initstricts = map (const False) sargs + + sargs = arguments rule; initsroot = ruleroot rule; initsubject = rulegraph rule + +listselect :: [.Bool] [.elem] -> [.elem] +listselect _ _ = undef + +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 (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 + | == var + & == pvar + +transform anode sargs (Present spine) += selectfromtip (spinetip spine) + where selectfromtip (nid,Open rgraph) = tryinstantiate nid rgraph anode sargs + selectfromtip (nid,Redex rule matching) = tryunfold nid rule matching spine + selectfromtip (nid,Strict) = tryannotate nid sargs + selectfromtip spine = dostop + +transform anode sargs Absent += dostop + +// ==== 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 + 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 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 + (heap`,subject`) = instantiate 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 = removeMembers (fst (graphvars subject sargs)) stricts + match` = removeMembers (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 + | == var + & == pvar + +tryunfold redexroot rule matching spine += act + 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) + redirect = adjust redexroot reductroot id + history` = extendhistory subject redirect spine history + 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 + 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 + where ds continue history failinfo instdone stricts sroot subject heap = Stop diff --git a/sucl/new.icl b/sucl/new.icl new file mode 100644 index 0000000..0531019 --- /dev/null +++ b/sucl/new.icl @@ -0,0 +1,46 @@ +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 new file mode 100644 index 0000000..2ddfa42 --- /dev/null +++ b/sucl/newfold.icl @@ -0,0 +1,343 @@ +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 * **])) + +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 * ** *** -> +> (rgraph * **->(*,[**])) -> +> * -> +> trace * ** *** -> +> ([bool],[rule * **],[rgraph * **]) + +> fullfold trc foldarea fnsymbol trace +> = recurseresult, if recursive +>|| = mapfst3 only (extract trc foldarea trace ([],[],[])), otherwise +> = newextract trc foldarea trace, otherwise +> where (recursive,recurseresult) = recurse foldarea fnsymbol 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 * **->(*,[**])) -> +> * -> +> trace * ** *** -> +> (bool,([bool],[rule * **],[rgraph * **])) + +> recurse foldarea fnsymbol +> = f ([],[]) +> where f (newhist,hist) (Trace stricts rule answer history (Reduce reductroot trace)) +> = f (newhist',newhist') trace, if pclosed=[] & superset popen ropen +> where rargs = lhs rule; rroot = rhs rule; rgraph = rulegraph rule +> (pclosed,popen) = nodeset rgraph rargs +> (rclosed,ropen) = nodeset rgraph [rroot] +> newhist' = (rroot,rgraph):newhist +> f (newhist,hist) (Trace stricts rule answer history (Annotate trace)) +> = f (newhist',hist) trace, if pclosed=[] & superset popen ropen +> where rargs = lhs rule; rroot = rhs rule; rgraph = rulegraph rule +> (pclosed,popen) = nodeset rgraph rargs +> (rclosed,ropen) = nodeset rgraph [rroot] +> newhist' = (rroot,rgraph):newhist +> f (newhist,hist) (Trace stricts rule answer history transf) +> = foldtips foldarea (fnsymbol,lhs rule) (mkset newhist',mkset hist) (Trace stricts rule answer history transf) +> where rroot = rhs rule; rgraph = rulegraph rule +> newhist' = (rroot,rgraph):newhist + + +`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. + +> addstrict stricts (rule,areas) = (stricts,[rule],areas) + +> foldtips :: +> (rgraph * **->(*,[**])) -> +> (*,[**]) -> +> ([(**,graph * **)],[(**,graph * **)]) -> +> trace * ** *** -> +> (bool,([bool],[rule * **],[rgraph * **])) + +> foldtips foldarea foldcont +> = ft +> where ft hist trace +> = ft' transf +> where Trace stricts rule answer history transf = trace +> ft' Stop +> = foldoptional exres (pair True.addstrict stricts) (actualfold deltanodes rnfnodes foldarea (=) foldcont (snd hist) rule) +> where deltanodes = foldoptional [] getdeltanodes answer +> rnfnodes = foldoptional [rhs rule] (const []) answer +> ft' (Instantiate yestrace notrace) +> = ft'' (ft hist yestrace) (ft hist notrace) +> where ft'' (False,yessra) (False,nosra) = exres +> ft'' (yesfound,(yesstricts,yesrules,yesareas)) (nofound,(nostricts,norules,noareas)) +> = (True,(stricts,yesrules++norules,yesareas++noareas)) +> ft' (Reduce reductroot trace) +> = ft'' (ft (fst hist,fst hist) trace) +> where ft'' (False,sra) = exres +> ft'' (found,sra) = (True,sra) +> ft' (Annotate trace) +> = ft'' (ft hist trace) +> where ft'' (False,sra) = exres +> ft'' (found,sra) = (True,sra) +> || exres = (False,mapfst3 only (extract noetrc foldarea trace ([],[],[]))) +> exres = (False,newextract noetrc foldarea trace) + +> noetrc trace area = id + +> pair x y = (x,y) + +> only :: [*] -> * +> only [x] = x +> only xs = error "only: not a singleton list" + +------------------------------------------------------------------------ + +`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 * ** *** +> == trace * ** *** -> +> rgraph * ** -> +> bool -> +> bool + +> extract +> :: etracer * ** *** -> +> (rgraph * **->(*,[**])) -> +> trace * ** *** -> +> ([[bool]],[rule * **],[rgraph * **]) -> +> ([[bool]],[rule * **],[rgraph * **]) + +> extract trc newname (Trace stricts rule answer history transf) (strictss,rules,areas) +> = (strictss',recrule:rules,recareas++areas), if trc (Trace stricts rule answer history transf) unsafearea recursive +> = mapfst3 (ifopen (const strictss') id answer) (f transf (strictss,rules,areas)), otherwise +> where f (Reduce reductroot trace) = extract trc newname trace +> f (Annotate trace) = extract trc newname trace +> f (Instantiate yestrace notrace) = extract trc newname yestrace.extract trc newname notrace +> f Stop (strictss,rules,areas) = (stricts:strictss,mkrule rargs rroot stoprgraph:rules,stopareas++areas) + +> (recursive,unsafearea) +> = foldoptional (False,undef) (findspinepart rule transf) answer, if isreduce transf +> = (False,error "extract: not a Reduce transformation"), otherwise + +> (recrule,recareas) = splitrule newname rnfnodes deltanodes rule unsafearea +> (stoprgraph,stopareas) = finishfold newname rnfnodes deltanodes rroot rgraph + +> rargs = lhs rule; rroot = rhs rule; rgraph = rulegraph rule +> rnfnodes = foldoptional (rroot:) (const id) answer (nodelist rgraph rargs) + +> deltanodes = foldoptional [] getdeltanodes answer + +> strictss' = stricts:strictss + + +This is a version of `extract' that does not use the collector argument. + +> newextract +> :: etracer * ** *** -> +> (rgraph * **->(*,[**])) -> +> trace * ** *** -> +> ([bool],[rule * **],[rgraph * **]) + +> newextract trc newname (Trace stricts rule answer history transf) +> = (stricts,[recrule],recareas), if recursive +> = subex transf, otherwise +> where subex (Reduce reductroot trace) = newextract trc newname trace +> subex (Annotate trace) = newextract trc newname trace +> subex (Instantiate yestrace notrace) +> = (stricts,yesrules++norules,yesareas++noareas) +> where (yesstricts,yesrules,yesareas) = newextract trc newname yestrace +> (nostricts,norules,noareas) = newextract trc newname notrace +> subex Stop = (stricts,[mkrule rargs rroot stoprgraph],stopareas) + +> (recursive,unsafearea) +> = foldoptional (False,undef) (findspinepart rule transf) answer, if isreduce transf +> = (False,error "newextract: not a Reduce transformation"), otherwise + +> (recrule,recareas) = splitrule newname rnfnodes deltanodes rule unsafearea +> (stoprgraph,stopareas) = finishfold newname rnfnodes deltanodes rroot rgraph + +> rargs = lhs rule; rroot = rhs rule; rgraph = rulegraph rule +> rnfnodes = foldoptional (rroot:) (const id) answer (nodelist rgraph rargs) + +> deltanodes = foldoptional [] getdeltanodes answer + +> 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 * ** -> transformation * ** *** -> spine * ** *** -> (bool,rgraph * **) + +> findspinepart rule transf spine +> = snd (foldspine pair stop stop id stop (const stop) partial (const stop) redex stop spine) +> where pair node (pattern,recursion) +> = (pattern',recursion') +> where pattern' +> = updategraph node cnt pattern, if def +> = pattern, otherwise +> (def,cnt) = dnc (const "in findspinepart") graph node +> recursion' +> = (True,mkrgraph node pattern'), if findpattern (pattern',node) (spinenodes spine) node transf +> = recursion, otherwise +> partial rule matching (pattern,recursion) = (extgraph' graph rule matching pattern,recursion) +> redex rule matching = (extgraph' graph rule matching emptygraph,norecursion) +> stop = (emptygraph,norecursion) +> norecursion = (False,error "findspinepart: no part of spine found") +> graph = rulegraph rule + +> extgraph' sgraph rule +> = extgraph sgraph rgraph (nodelist rgraph (lhs 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 * ****,****) -> [**] -> ** -> transformation * ** *** -> bool + +> findpattern pattern thespinenodes residuroot transf +> = False, if ~member thespinenodes residuroot || 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) +> = True, if or [instance pattern (graph,node)|node<-nodelist graph [residuroot]] +> where graph = rulegraph rule +> fp = findpattern' pattern +> redirect = adjust (last thespinenodes) reductroot id + +> findpattern pattern thespinenodes residuroot (Instantiate 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 * ****,****) -> ** -> trace * ** *** -> bool + +> 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 * ** *** -> +> [**] + +Uses foldspine with + + **** == (bool,[**]) + ***** == [**] + +> getdeltanodes +> = foldspine pair none (True,[]) force none (const none) partial (const none) redex none +> where pair node (forced,nodes) = cond forced (node:nodes) nodes +> none = (False,[]) +> force nodes = (True,nodes) +> partial rule matching nodes = (False,nodes) +> redex rule matching = none diff --git a/sucl/newtest.icl b/sucl/newtest.icl new file mode 100644 index 0000000..13cf8fc --- /dev/null +++ b/sucl/newtest.icl @@ -0,0 +1,394 @@ +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) +> ) + +> 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 + +`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 + +`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 + +> 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 + +> 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] + +------------------------------------------------------------------------ + +`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) + +> newsymbols main = map (User main.("New_"++)) identifiers diff --git a/sucl/pfun.dcl b/sucl/pfun.dcl new file mode 100644 index 0000000..dfd0ab8 --- /dev/null +++ b/sucl/pfun.dcl @@ -0,0 +1,42 @@ +definition module pfun + +from StdString import toString +from StdOverloaded import == + +// 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 + +// 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 + +/* `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 diff --git a/sucl/pfun.icl b/sucl/pfun.icl new file mode 100644 index 0000000..f720f51 --- /dev/null +++ b/sucl/pfun.icl @@ -0,0 +1,77 @@ +implementation module pfun + +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 + +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 +where toString pfun + = toString ['{':drop 1 (flatten (map ((cons ',') o printlink) (pfunlist pfun)))++['}']] + where printlink (arg,res) = fromString (toString arg)++['|->']++fromString (toString res) + +pfunlist :: (Pfun dom res) -> [(dom,res)] +pfunlist _ = abort "pfunlist not implemented" + +idpfun :: !.[dom] .(Pfun dom dom) -> Bool | == dom +idpfun domain pfun += all idelem domain + where idelem x = total True (postcomp ((==) x) pfun) x diff --git a/sucl/pretty.dcl b/sucl/pretty.dcl new file mode 100644 index 0000000..a723331 --- /dev/null +++ b/sucl/pretty.dcl @@ -0,0 +1,30 @@ +definition module pretty + +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 new file mode 100644 index 0000000..7e23e5c --- /dev/null +++ b/sucl/pretty.icl @@ -0,0 +1,132 @@ +implementation module pretty + +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 new file mode 100644 index 0000000..2b4448f --- /dev/null +++ b/sucl/rewr.dcl @@ -0,0 +1,51 @@ +definition module rewr + +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 + +instantiate + :: .(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 new file mode 100644 index 0000000..0dc2059 --- /dev/null +++ b/sucl/rewr.icl @@ -0,0 +1,213 @@ +implementation module rewr + +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 + +instantiate + :: .(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 + +instantiate 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 new file mode 100644 index 0000000..d2438dc --- /dev/null +++ b/sucl/rule.dcl @@ -0,0 +1,42 @@ +definition module rule + +from graph import Graph,Node + +// --- 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 + +// --- 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 diff --git a/sucl/rule.icl b/sucl/rule.icl new file mode 100644 index 0000000..c6d5acd --- /dev/null +++ b/sucl/rule.icl @@ -0,0 +1,189 @@ +implementation module rule + +import graph +import basic + +:: Rule sym var + :== ([var],var,Graph sym var) + +:: Rgraph sym var + :== (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 = (root,emptygraph) + +updatergraph :: .var (Node .sym .var) !(Rgraph .sym .var) -> Rgraph .sym .var +updatergraph var node rgraph = mapsnd (updategraph var node) rgraph + +prunergraph :: .var !(Rgraph .sym .var) -> Rgraph .sym .var +prunergraph var rgraph = mapsnd (prunegraph var) rgraph + +rgraphroot :: !(Rgraph .sym .var) -> .var +rgraphroot (root,_) = root + +rgraphgraph :: !(Rgraph .sym .var) -> Graph .sym .var +rgraphgraph (_,graph) = graph + +mkrgraph :: .var (Graph .sym .var) -> Rgraph .sym .var +mkrgraph root graph = (root,graph) + +/* +> showrgraph showfunc shownode (root,graph) +> = '(':snd (showsubgraph root ([],"emptyrgraph) "))++shownode root +> where showsubgraph node (seen,repr) +> = (seen,repr), if ~def \/ member seen node +> = (seen'',repr''), otherwise +> where (def,(f,args)) = nodecontents graph node +> (seen'',repr') = foldlr showsubgraph (seen',repr) args +> seen' = node:seen +> repr'' +> = "updatergraph "++shownode node++" ("++ +> showfunc f++',':showlist shownode args++")."++ +> repr' + +> printrgraph showfunc shownode (root,graph) +> = hd (printgraph showfunc shownode 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 = (args,root,graph) + +arguments :: !(Rule .sym .var) -> [.var] +arguments (args,_,_) = args + +ruleroot :: !(Rule .sym .var) -> .var +ruleroot (_,root,_) = root + +rulegraph :: !(Rule .sym .var) -> Graph .sym .var +rulegraph (_,_,graph) = graph + +/* +> showrule showfunc shownode (lroots,rroot,graph) +> = "((mkrule "++showlist shownode lroots++' ':shownode rroot++repr'++") emptygraph)" +> where (seen,repr') = showsubgraph rroot ([],repr) +> (seen',repr) = foldlr showsubgraph (seen,"") lroots +> showsubgraph node (seen,repr) +> = (seen,repr), if ~def \/ member seen node +> = (seen'',repr''), otherwise +> where (def,(f,args)) = nodecontents graph node +> (seen'',repr') = foldlr showsubgraph (seen',repr) args +> seen' = node:seen +> repr'' +> = ".updategraph "++shownode node++" ("++ +> showfunc f++',':showlist shownode args++')':repr' + +> printrule showfunc shownode (lroots,rroot,graph) +> = (concat.map (++" ").init) reprs++"-> "++last reprs +> where reprs = printgraph showfunc shownode graph (lroots++[rroot]) + +> compilerule :: [**] -> ** -> [(**,(*,[**]))] -> rule * ** +> compilerule args root = mkrule args root.compilegraph + +*/ diff --git a/sucl/script.icl b/sucl/script.icl new file mode 100644 index 0000000..5bdadc4 --- /dev/null +++ b/sucl/script.icl @@ -0,0 +1,7 @@ +%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 new file mode 100644 index 0000000..2ebe3a6 --- /dev/null +++ b/sucl/spine.dcl @@ -0,0 +1,193 @@ +definition module spine + +from rule import Rgraph,Rule +from pfun import Pfun +from basic import Optional + +/* + +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) + +/* + +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 (Spine sym var pvar) // Global strictness annotation forced evaluation of a subgraph + | 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) (Spine sym var pvar) // A rule was strictly partially matched + | Unsafe (Rgraph 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) + .subresult + .subresult + (.result -> .subresult) + .subresult + ((Rgraph sym pvar) -> .subresult) + ((Rule sym pvar) (Pfun pvar var) .result -> .subresult) + ((Rgraph sym var) -> .subresult) + ((Rule sym pvar) (Pfun pvar var) -> .subresult) + .subresult + .(Spine sym var pvar) + -> .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 diff --git a/sucl/spine.icl b/sucl/spine.icl new file mode 100644 index 0000000..cd9f668 --- /dev/null +++ b/sucl/spine.icl @@ -0,0 +1,244 @@ +implementation module spine + +import rule +import pfun +import basic +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) + +/* + +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 (Spine sym var pvar) // Global strictness annotation forced evaluation of a subgraph + | 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) (Spine sym var pvar) // A rule was strictly partially matched + | Unsafe (Rgraph 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) + .subresult + .subresult + (.result -> .subresult) + .subresult + ((Rgraph sym pvar) -> .subresult) + ((Rule sym pvar) (Pfun pvar var) .result -> .subresult) + ((Rgraph sym var) -> .subresult) + ((Rule sym pvar) (Pfun pvar var) -> .subresult) + .subresult + .(Spine sym var pvar) + -> .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 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 + +spinetip :: !(Spine sym var pvar) -> Spine sym var pvar +spinetip (_,Force spine) = spinetip spine +spinetip (_,Partial _ _ spine) = spinetip spine +spinetip spine = spine + +spinenodes :: .(Spine sym var pvar) -> [var] +spinenodes spine += foldspine cons [] [] id [] (const []) partial (const []) redex [] spine + where partial _ _ = id + redex _ _ = [] + +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 diff --git a/sucl/strat.dcl b/sucl/strat.dcl new file mode 100644 index 0000000..6a0dd6b --- /dev/null +++ b/sucl/strat.dcl @@ -0,0 +1,166 @@ +definition module strat + +from history import History +from spine import Answer +from rule import Rule +from graph import Graph,Node +from StdOverloaded import == + +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 + | == sym + & == var + & == pvar + + +/* ------------------------------------------------------------------------ +STRATEGY TRANSFORMERS +The funcions below tranform (simpler) strategies into more complicated ones +------------------------------------------------------------------------ */ + +// A strategy transformer that checks for constructor applications +checkconstr + :: (sym->.Bool) + (Strategy sym .var .pvar .result) + (Substrategy sym .var .pvar .result) + (Graph sym .var) + ((Subspine sym .var .pvar) -> .result) + .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 type rule +// for curried applications and strict arguments +checktype + :: !(sym -> (Rule .tsym tvar,[.Bool])) + (Strategy sym var .pvar .result) + (Substrategy sym var .pvar .result) + .(Graph sym var) + ((Subspine sym var .pvar) -> .result) + .result + !.(Node sym var) + -> .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 new file mode 100644 index 0000000..3ed23f7 --- /dev/null +++ b/sucl/strat.icl @@ -0,0 +1,461 @@ +implementation module strat + +import history +import spine +import dnc +import rule +import graph +import pfun +import basic +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 + | == sym + & == var + & == pvar + +makernfstrategy hist strat rnfnodes node graph += substrat [] spinecont rnfanswer node + where spinecont spine = Present spine + rnfanswer = Absent + + 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` = checkinstance (graph,node) histpatts strat + histpatts = foldr (foldmap (++) id hist) [] spinenodes` + +/* + +------------------------------------------------------------------------ +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 spine = found (Partial rule matching spine) + foundmatch matching = found (Redex rule matching) + +matchnodes + :: (pvar var -> .Bool) + .(Graph sym var) + (Substrategy sym var pvar result) + ((Pfun pvar var) (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 openspine + = substrat (found matching) 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 nodes + where forcenode nid rnfrest = substrat foundforce rnfrest nid + foundforce spine = found (Force spine) + +/* + +------------------------------------------------------------------------ +STRATEGY COMPOSITION + +Check for an instance in the termination history. + +*/ + +checkinstance + :: (.Graph sym var,var) + [.Rgraph sym var] + (Strategy sym var .pvar result) + -> Strategy sym var .pvar result + | == sym + & == var + & == pvar + +checkinstance (graph,node) history defaultstrategy += foldr check defaultstrategy history + where check hrgraph defaultstrategy substrat subject found rnf (ssym,sargs) + | isinstance (hgraph,hroot) (graph,node) + = found (Unsafe hrgraph) + = defaultstrategy substrat subject found rnf (ssym,sargs) + where hgraph = rgraphgraph hrgraph; hroot = rgraphroot hrgraph + + +// Check a type rule for curried applications and strict arguments + +checktype + :: !(sym -> (Rule .tsym tvar,[.Bool])) + (Strategy sym var .pvar .result) + (Substrategy sym var .pvar .result) + .(Graph sym var) + ((Subspine sym var .pvar) -> .result) + .result + !.(Node sym var) + -> .result + +checktype typeinfo defaultstrategy substrat subject found rnf (ssym,sargs) +| shorter targs sargs += rnf +| eqlen targs sargs += forcenodes substrat found rnf` strictnodes += abort "checktype: symbol occurrence with arity greater than its type" + where rnf` = defaultstrategy substrat subject found rnf (ssym,sargs) + (trule,tstricts) = typeinfo ssym + targs = arguments trule + 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->.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 isconstr defstrat substrat subject found rnf (ssym,sargs) +| isconstr ssym += rnf += defstrat substrat subject found rnf (ssym,sargs) diff --git a/sucl/sucl.prj b/sucl/sucl.prj new file mode 100644 index 0000000..e6daada --- /dev/null +++ b/sucl/sucl.prj @@ -0,0 +1,1190 @@ +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 new file mode 100644 index 0000000..29e1eff --- /dev/null +++ b/sucl/trace.dcl @@ -0,0 +1,289 @@ +definition module trace + +from history import History +from spine import Answer +from rule import Rule +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 (Trace sym var pvar) + (Trace sym var pvar) + | 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++" ") + + +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) .result .result -> .result) + !.(Trace sym var pvar) + -> .result + +foldtransformation + :: ((Trace sym var pvar) -> .result) + (var .result -> .subresult) + (.result -> .subresult) + .subresult + (.result .result -> .subresult) + ([.absresult] -> .subresult) + ((Rule sym var) -> .absresult) + (.result -> .absresult) + !.(Transformation sym var pvar) + -> .subresult diff --git a/sucl/trace.icl b/sucl/trace.icl new file mode 100644 index 0000000..335fbd8 --- /dev/null +++ b/sucl/trace.icl @@ -0,0 +1,259 @@ +implementation module trace + +import history +import spine +import rule +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 (Trace sym var pvar) + (Trace sym var pvar) + | 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++" ") + + +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) .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 yestrace notrace) = instantiate stricts rule answer history (ftr yestrace) (ftr notrace) + ftf _ _ _ _ (Abstract _) = abort "foldtrace not implemented for abstraction nodes" + +foldtransformation + :: ((Trace sym var pvar) -> .result) + (var .result -> .subresult) + (.result -> .subresult) + .subresult + (.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 yestrace notrace) = instantiate (ftr yestrace) (ftr notrace) + ftf (Abstract as) = abstract (map fab as) + fab (NewAbstraction t) = newabstraction (ftr t) + fab (KnownAbstraction r) = knownabstraction r diff --git a/sucl/trd.dcl b/sucl/trd.dcl new file mode 100644 index 0000000..bfe91b4 --- /dev/null +++ b/sucl/trd.dcl @@ -0,0 +1,23 @@ +definition module trd + +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 new file mode 100644 index 0000000..5ecc2c9 --- /dev/null +++ b/sucl/trd.icl @@ -0,0 +1,203 @@ +implementation module trd + +import rule +import graph +import basic +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] -> .(z:(Graph tsym tvar) -> .(x:[y:(var,tvar)] -> .result))) // Continuation + .[tvar] // Type heap + w:(Graph tsym tvar) // Type graph build so far + u:[v:(var,tvar)] // Assignment of type variables to variables + -> .result // Final result + | == var + & == trvar + , [u<=x,v<=y,w<=z] + +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 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:(x:(Graph sym var2) -> .result)) // Continuation + (.var->var2) // Redirection + u:(Graph sym var2) // Graph before redirection + -> .result // Final result + | == sym + & == var2 + , [u<=x,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 [] = [] |