diff options
Diffstat (limited to 'sucl/newfold.icl')
| -rw-r--r-- | sucl/newfold.icl | 343 |
1 files changed, 343 insertions, 0 deletions
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 |