diff options
| -rw-r--r-- | sucl/Makefile | 11 | ||||
| -rw-r--r-- | sucl/absmodule.dcl | 14 | ||||
| -rw-r--r-- | sucl/absmodule.icl | 14 | ||||
| -rw-r--r-- | sucl/basic.dcl | 3 | ||||
| -rw-r--r-- | sucl/basic.icl | 4 | ||||
| -rw-r--r-- | sucl/cli.icl | 33 | ||||
| -rw-r--r-- | sucl/law.dcl | 16 | ||||
| -rw-r--r-- | sucl/law.icl | 51 | ||||
| -rw-r--r-- | sucl/loop.icl | 134 | ||||
| -rw-r--r-- | sucl/spine.icl | 3 |
10 files changed, 260 insertions, 23 deletions
diff --git a/sucl/Makefile b/sucl/Makefile index 7f462df..7732f75 100644 --- a/sucl/Makefile +++ b/sucl/Makefile @@ -6,7 +6,7 @@ COCL = cocl #COCLFLAGS = -lat SYS = Clean\ System\ Files -MODULES = basic pretty pfun graph dnc rule trd rewr complete history spine trace absmodule spine strat loop law coreclean convert supercompile +MODULES = basic pretty pfun graph dnc rule trd rewr complete history spine trace absmodule strat loop coreclean law canon cli extract newfold newtest convert supercompile ABC = $(patsubst %,$(SYS)/%.abc,$(MODULES)) @@ -25,10 +25,11 @@ tags: *.dcl *.icl ../compiler/*.dcl ../compiler/*.icl $(SYS)/%.abc: %.icl $(COCL) $(COCLFLAGS) $* -$(SYS)/supercompile.abc: supercompile.icl supercompile.dcl -$(SYS)/convert.abc: convert.icl convert.dcl coreclean.dcl rule.dcl -$(SYS)/coreclean.abc: coreclean.icl coreclean.dcl -$(SYS)/law.abc: law.icl law.dcl +$(SYS)/supercompile.abc: supercompile.icl supercompile.dcl convert.dcl +$(SYS)/convert.abc: convert.icl convert.dcl coreclean.dcl rule.dcl graph.dcl basic.dcl +$(SYS)/cli.abc: cli.icl cli.dcl absmodule.dcl coreclean.dcl law.dcl strat.dcl rule.dcl basic.dcl +$(SYS)/coreclean.abc: coreclean.icl coreclean.dcl strat.dcl spine.dcl rule.dcl graph.dcl +$(SYS)/law.abc: law.icl law.dcl coreclean.dcl strat.dcl spine.dcl rule.dcl graph.dcl dnc.dcl basic.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 diff --git a/sucl/absmodule.dcl b/sucl/absmodule.dcl index 2cf9a35..ccea9f3 100644 --- a/sucl/absmodule.dcl +++ b/sucl/absmodule.dcl @@ -5,11 +5,11 @@ 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 + = { 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 index 3f30317..f18ecc6 100644 --- a/sucl/absmodule.icl +++ b/sucl/absmodule.icl @@ -42,13 +42,13 @@ Module implementation. */ :: 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 + = { 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/basic.dcl b/sucl/basic.dcl index b288043..be3260a 100644 --- a/sucl/basic.dcl +++ b/sucl/basic.dcl @@ -53,6 +53,9 @@ disjoint :: .[elem] !.[elem] -> Bool | == elem // `Eqlen xs ys' determines whether `xs' and `ys' are equally long. eqlen :: ![.elem1] ![.elem2] -> .Bool +// Extend a function using the elements of a mapping +extendfn :: [(src,dst)] (src->dst) src -> dst | == src + // `Foldlm' is a combination of foldl and map. foldlm :: ((.collect,.elem) -> (.collect,.elem`)) !(.collect,![.elem]) -> (.collect,[.elem`]) diff --git a/sucl/basic.icl b/sucl/basic.icl index 86770b5..a508599 100644 --- a/sucl/basic.icl +++ b/sucl/basic.icl @@ -71,6 +71,10 @@ eqlen [x:xs] [y:ys] = eqlen xs ys eqlen [] [] = True eqlen xs ys = False +// Extend a function using the elements of a mapping +extendfn :: [(src,dst)] (src->dst) src -> dst | == src +extendfn mapping f x = foldmap id (f x) mapping x + // `Foldlm' is a combination of foldl and map. foldlm :: ((.collect,.elem) -> (.collect,.elem`)) !(.collect,![.elem]) -> (.collect,[.elem`]) foldlm f (l,[]) = (l,[]) diff --git a/sucl/cli.icl b/sucl/cli.icl index 88bbe6e..3e1c8ae 100644 --- a/sucl/cli.icl +++ b/sucl/cli.icl @@ -2,6 +2,14 @@ implementation module cli // $Id$ +import absmodule +import coreclean +import law +import strat +import rule +import basic +import StdEnv + /* cli.lit - Clean implementation modules @@ -94,7 +102,11 @@ Abstype implementation. > aliases :: cli -> [(typesymbol,rule typesymbol typenode)] > macros :: cli -> [(symbol,rule symbol node)] > stripexports :: [char] -> cli -> cli +*/ +:: Cli :== Module SuclSymbol SuclVariable SuclTypeSymbol SuclTypeVariable + +/* > cli == module symbol node typesymbol typenode > readcli = compilecli.readcleanparts @@ -126,13 +138,26 @@ Abstype implementation. > ) (corestrategy matchable) || Checks rules for symbols in the language core (IF, _AP, ...) > where islocal (User m i) = member (map fst rs) (User m i) > islocal rsym = True || Symbols in the language core are always completely known +*/ + +clistrategy :: Cli ((Graph SuclSymbol SuclVariable) SuclVariable var -> Bool) -> Strategy SuclSymbol var SuclVariable answer | == var +clistrategy cli=:{exportedtypesymbols=tes,typealias=tas,typeconstructors=tcs,exportedsymbols=es,aliases=as,typerules=ts,rules=rs} matchable + = ( checkarity (typearity o maxtypeinfo ts) // Checks curried occurrences and strict arguments + o checklaws cleanlaws // Checks for special (hard coded) rules (+x0=x /y1=y ...) + o checkrules matchable (foldmap id [] rs) // Checks normal rewrite rules + o checkimport islocal // Checks for delta symbols + o checkconstr (flip isMember (flatten (map snd tcs))) // Checks for constructors + ) (corestrategy matchable) // Checks rules for symbols in the language core (IF, _AP, ...) + where islocal rsym=:(SuclUser s) = isMember rsym (map fst rs) + islocal rsym = True // Symbols in the language core are always completely known -> maxtypeinfo :: [(symbol,(rule typesymbol typenode,[bool]))] -> symbol -> (rule typesymbol typenode,[bool]) -> maxtypeinfo ts = extendfn ts coretypeinfo +typearity :: (Rule SuclTypeSymbol SuclTypeVariable,[Bool]) -> Int +typearity ti = length (arguments (fst ti)) -> extendfn :: [(*,**)] -> (*->**) -> * -> ** -> extendfn mapping f x = foldmap id (f x) mapping x +maxtypeinfo :: [(SuclSymbol,(Rule SuclTypeSymbol SuclTypeVariable,[Bool]))] SuclSymbol -> (Rule SuclTypeSymbol SuclTypeVariable,[Bool]) +maxtypeinfo defs sym = extendfn defs coretypeinfo sym +/* > constrs ((tes,tas,tcs),defs) = tcs > complete ((tes,tas,tcs),(es,as,ts,rs)) = mkclicomplete tcs (fst.maxtypeinfo ts) diff --git a/sucl/law.dcl b/sucl/law.dcl index e17f005..e136b46 100644 --- a/sucl/law.dcl +++ b/sucl/law.dcl @@ -1,3 +1,19 @@ definition module law // $Id$ + +from coreclean import SuclSymbol,SuclVariable +from strat import Law,Strategy +from StdOverloaded import == + +// Transitive necessities + +from strat import Substrategy +from spine import Spine,Subspine +from graph import Graph,Node + +// The list of special Clean transformation laws +cleanlaws :: [(SuclSymbol,Law SuclSymbol var SuclVariable result)] + +// The strategy for built in clean symbols +corestrategy :: ((Graph SuclSymbol SuclVariable) SuclVariable var -> Bool) -> Strategy SuclSymbol var SuclVariable result | == var diff --git a/sucl/law.icl b/sucl/law.icl index b8cede6..1f14ee4 100644 --- a/sucl/law.icl +++ b/sucl/law.icl @@ -2,6 +2,15 @@ implementation module law // $Id$ +import coreclean +import strat +import spine +import rule +import graph +import dnc +import basic +import StdEnv + /* > %export @@ -101,7 +110,12 @@ implementation module law ------------------------------------------------------------------------ > cleanlaws :: [(symbol,law symbol ** node ****)] +*/ +cleanlaws :: [(SuclSymbol,Law SuclSymbol var SuclVariable result)] +cleanlaws =: [] + +/* > cleanlaws > = [(User "deltaI" "*",law) | law <- mullaws] ++ > [(User "deltaI" "+",law) | law <- addlaws] ++ @@ -134,7 +148,24 @@ Also, using trylaw is easier > corestrategy matchable substrat subject found rnf (ssym,snodes) > = rnf +*/ + +// The strategy for built in clean symbols +corestrategy :: ((Graph SuclSymbol SuclVariable) SuclVariable var -> Bool) -> Strategy SuclSymbol var SuclVariable result | == var +corestrategy matchable =(\ substrat subject found rnf snode + -> let (ssym,sargs) = snode + in case ssym + of SuclUser sptr + -> found MissingCase + SuclCase eptr + -> found MissingCase + SuclApply argc + -> trylaw subject found sargs (applyrule nc) (found Delta) + where nc = dnc (const "in corestrategy") subject (hd sargs) + _ + -> rnf) +/* > applyrule :: (bool,(*,[**])) -> rule * node > applyrule (sdef,scont) > = aprule (anode,(sym,aargs)) [enode] aroot @@ -143,7 +174,17 @@ Also, using trylaw is easier > = scont, if sdef > = (nosym,[]), otherwise > nosym = error "applyrule: no function symbol available" +*/ + +applyrule :: (Bool,Node sym var) -> Rule sym SuclVariable +applyrule (sdef,scont) + = aprule (anode,(sym,aargs)) [enode] aroot + where (aargs,[anode,aroot,enode:_]) = claim sargs suclheap + (sym,sargs) + = if sdef scont (nosym,[]) + nosym = abort "applyrule: no function symbol available" +/* > aprule :: (***,(*,[***])) -> [***] -> *** -> rule * *** > aprule (anode,(sym,aargs)) anodes aroot > = mkrule (anode:anodes) aroot agraph @@ -151,7 +192,17 @@ Also, using trylaw is easier > = ( updategraph aroot (sym,aargs++anodes) > . updategraph anode (sym,aargs) > ) emptygraph +*/ + +aprule :: (pvar,Node sym pvar) [pvar] pvar -> Rule sym pvar +aprule (anode,(sym,aargs)) anodes aroot + = mkrule [anode:anodes] aroot agraph + where agraph + = ( updategraph aroot (sym,aargs++anodes) + o updategraph anode (sym,aargs) + ) emptygraph +/* > apmatching :: [**] -> [***] -> pfun *** ** > apmatching snodes anodes > = foldr (uncurry extend) emptypfun nodepairs diff --git a/sucl/loop.icl b/sucl/loop.icl index c94c1b6..85d1233 100644 --- a/sucl/loop.icl +++ b/sucl/loop.icl @@ -28,6 +28,140 @@ like instantiation, reduction or strict annotation. ------------------------------------------------------------ +The function that produces a trace is given an initial task expression. + +The function first determines a transformation (Reduce,Annotate,Instantiate) to +apply, using the strategy. + +This may fail when the termination history indicates a required abstraction +higher up. In that case, return at once with failure, and the current graph +(with shared parts excluded) as the most specific generaliser. + +After application of the transformation, a trace is produced for the resulting +graph(s). + +However, the production of the subtraces may fail initially because of a +necessary abstraction higher-up which wasn't there (introduced recursion). + +Therefore, producing a trace can return one of two results: either a successful +trace, or failure, with an indication of which abstraction was actually +necessary. + +The needed generalisation is computed by taking the most specific generaliser +for each pattern in the termination history. + +In the general case, generation of the subtraces fails for both the history +pattern of the current transformation, and some patterns higher up (which were +also passed to the trace generation function. There are now two courses of +action: + +[1] Apply abstraction instead of the current transformation. Use the returned + most specific generaliser and the original graph to determine how to + abstract. Then, generate subtraces. There should be no more abstractions + necessary for the current node, because they should be handled in the + graphs resulting from the abstraction.[*] + +[2] Immediately return the failure, assuming (rule of thumb) that when the + upper generalisation was necessary, the lower one won't make it go away. + This is probably an optimisation of the optimisation process, but it can be + important, as some backtracking code (exponential!) may not have to be + executed. + +[*] This may not be entirely true in the case of sharing. Because shared parts + must be pruned, the termination pattern may get smaller in the abstraction + operation. + +Questions: + +[?] Which would yield better results and/or perform better: [1] or [2] above? + +[?] Must the abstracted areas be associated with termination patterns that + caused their introduction? Or somehow with the trace node where they were + introduced? The termination patterns don't have to be the same over + different branches of the trace! Do they play a role at all in selecting + the abstracted part? Actually, they don't. We just need their roots so we + can find the corresponding subgraphs and determine the MSG's. + +It would appear we can traverse the trace when everything is done and collected +all the introduced functions from it. + +------------------------------------------------------------ + +*/ + +:: FallibleTrace sym var pvar + = GoodTrace (Trace sym var pvar) + | NeedAbstraction [Rgraph sym var] + +:: Strat sym var pvar + :== (History sym var) + (Rgraph sym var) + -> Answer sym var pvar + +maketrace + :: (Strat sym var pvar) // The strategy + (History sym var) // Patterns to stop partial evaluation + (Rgraph sym var) // Subject graph + -> FallibleTrace sym var pvar // The result + +maketrace strategy history subject + = ( case answer + of No // Root normal form, abstract and continue with arguments + -> handlernf + Yes spine // Do something, even if it is to fail + -> ( case subspine + of Cycle // Cycle in spine. Generate x:_Strict x x with _Strict :: !a b -> b. Probably becomes a #! + -> handlecycle + Delta // Primitive function. Abstract its application and continue with remainder. + -> handledelta + Force n (spine) // Shouldn't happen + -> abort "loop: maketrace: spinetip returned Force???" + MissingCase // Missing case. Generate _MissingCase, possibly parametrised with user function? + -> handlemissingcase + Open pattern // Need instantiation. Generate two branches, extend history (for both) and continue. + -> handleopen pattern + Partial rule match rulenode spine + -> abort "loop: maketrace: spinetop returned Partial???" + Unsafe histpat // Require pattern from history. + -> handleunsafe histpat // If we have a more general version with a name attached, use that. + // Otherwise, fail with the corresponding subgraph + Redex rule match // Found a redex. Unfold, extend history and continue. + -> handleredex rule match + Strict // Need to put a strictness annotation on an open node-id. + -> handlestrict // Abstract _Strict <mumble> <mumble> and continue with rest. + ) spine + where (redexroot,subspine) = spinetip spine + ) strategy history subject + where answer = strategy history subject + +handlernf :: (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar +handlernf _ _ _ = undef + +handlecycle :: (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar +handlecycle _ _ _ _ = undef + +handledelta :: (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar +handledelta _ _ _ _ = undef + +handlemissingcase :: (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar +handlemissingcase _ _ _ _ = undef + +handleopen :: (Rgraph sym pvar) (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar +handleopen _ _ _ _ _ = undef + +handleunsafe :: (HistoryPattern sym var) (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar +handleunsafe _ _ _ _ _ = undef + +handleredex :: (Rule sym pvar) (Pfun pvar var) (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar +handleredex _ _ _ _ _ _ = undef + +handlestrict :: (Spine sym var pvar) (Strat sym var pvar) (History sym var) (Rgraph sym var) -> FallibleTrace sym var pvar +handlestrict _ _ _ _ = undef + +/* + +------------------------------------------------------------ + Types ----- diff --git a/sucl/spine.icl b/sucl/spine.icl index 89da146..735cd95 100644 --- a/sucl/spine.icl +++ b/sucl/spine.icl @@ -349,6 +349,9 @@ extendforce sgraph argno forcesub snode link extender0 extender2 = adjust link histpat1 extender1 // Extend history patterns according to an Open spine +// FIXME: this should build TWO extended versions: +// one for succesful instantiation +// one for failed instantiation extendopen :: rgraph // Pattern to drive instantiation (not used) var // Node-id in subject graph that was open |