diff options
Diffstat (limited to 'sucl/trace.icl')
| -rw-r--r-- | sucl/trace.icl | 376 |
1 files changed, 0 insertions, 376 deletions
diff --git a/sucl/trace.icl b/sucl/trace.icl deleted file mode 100644 index 7cc9d4b..0000000 --- a/sucl/trace.icl +++ /dev/null @@ -1,376 +0,0 @@ -implementation module trace - -// $Id$ - -import spine -import history -import rule -import graph -import basic -import syntax -import StdEnv - -/* - -trace.lit - Symbolic reduction traces -===================================== - -Description ------------ - -This script implements traces of symbolic reduction, indicating what -happened and why. Representation functions for traces are also -provided. - -A trace is a possibly infinite tree, with the nodes labeled with a -rewrite rule, the strategy answer for that rewrite rule, and the -selected transformation according to the rewrite rule and the strategy -answer. If any transformation is applicable, then a list of subtrees is -present and indicates the result of applying the transformation to the -rewrite rule. This is a list because a transformation may return more -than one transformed rewrite rule. - ------------------------------------------------------------------------- - -Interface ---------- - -Exported identifiers: - -> %export -> trace || Type of a trace -> transformation || Type of applied transformation - -> foldtransformation || Break down a transformation -> mapleaves || Map a function on the rules at the leaves of a trace -> printtrace || Make a human-readable representation of a trace -> showtrace || Make a representation of a trace -> strictchar || Representation of strictness annotation -> tips || Determine tips of a finite trace - ------------------------------------------------------------- - -Implementation --------------- - -*/ - -:: Trace sym var pvar - = Trace [Bool] - (Rule sym var) - (Answer sym var pvar) - (History sym var) - (Transformation sym var pvar) - -/* The trace (and transformation) data structure provides a record of the - actions taken by the partial evaluation algorithm. When partial evaluation - is finished, the result is a trace which can be divided into sections - separated by abstraction nodes. Thus, abstraction nodes delimit sections. - - Each section gives rise to a generated function. The rewrite rules of the - function (or its case branches, whichever representation is chosen) - correspond to the abstraction nodes that delimited the bottom of the trace - section. The abstraction node at the top section can be forgotten as it - belongs to the above section. However, the state in the top node may be of - interest. - - The abstraction transformation divides the subject graph into areas. The - abstraction operation is applied when a part or parts of the subject graph - must be turned into closures. There are two possibilities: closure to an - existing function, and closure to a new function. Each area becomes a new - initial task expression, for which a trace is subsequently produced. The - root of each area is the same variable as its root in the original subject - graph. The arguments of each area are found back as the arguments of the - initial rewrite rule of the subsequent trace. The arguments of each area - should be repeated for each of their occurrences in the area. - Alternatively, an area can become a backpointer to an earlier occurrence in - the trace. - - Abstraction can happen for several reasons: - - [1] The result of the application of a primitive function is needed. - The abstracted area is the application of the primitive function alone. - It is "folded" to itself. - The abstracted area is not partially evaluated itself. - - [2] The strategy found an instance of a pattern in the history. - The old pattern had a function name attached. - The abstracted area is the pattern. It is folded to the named function. - The abstracted area is no longer partially evaluated. - - [3] The strategy found a cycle in the spine. - The abstracted area is the cyclic tail of the spine. - It is "folded" to itself (or maybe a special "cycle in spine" function). - The abstracted area is not partially evaluated itself. - In fact, the whole graph can be replaced with the "cycle in spine" operator, - though this may seem kind of opportunistic, - and just an optimisation of the optimisation process. - - [4] Partial evaluation of the graph had a new occurrence of the area (introduced recursion). - The current occurrence has no name attached. - The abstracted area is the recurring pattern. - It is abstracted, and a name is assigned to it. - It is folded to the assigned name. - The abstracted area is still partially evaluated by itself. - - [5] The graph is in root normal form. - The root node should be abstracted. - The root node must be "folded" to an application of itself. - The remainder must be partially evaluated. - - In all these cases, one specific area for abstraction is indicated. - This specific area may or may not be partially evaluated itself. - - The meaning of the Stop constructor should be changed. - It is no longer used to force stopping when abstraction is needed. - Instead, it is used when nothing at all is left to be done. -*/ - -:: Transformation sym var pvar - = Reduce var (Trace sym var pvar) - | Annotate (Trace sym var pvar) - | Stop - | Instantiate (Rgraph sym var) - (Trace sym var pvar) - (Trace sym var pvar) - -/* Disable the abstraction node for now... - - | Abstract [Abstraction sym var pvar] - -// Some abstractions (introduced recursion) spawn a fresh subtrace, but others -// just complete stop partial evaluation, folding to a known rule. - -:: Abstraction sym var pvar - = NewAbstraction (Trace sym var pvar) - | KnownAbstraction (Rule sym var) - -> showtrace showa showb showc (Trace stricts rule answer history transf) -> = "(Trace "++ -> show (map strictchar stricts)++' ': -> showrule showa showb rule++' ': -> showanswer showa showb showc answer++' ': -> showhistory showa showb history++' ': -> showtransf showa showb showc transf++")" - -> showtransf showa showb showc -> = stf -> where stf (Reduce reductroot trace) = "(Reduce "++showb reductroot++' ':str trace++")" -> stf (Annotate trace) = "(Annotate "++str trace++")" -> stf Stop = "Stop" -> stf (Instantiate yestrace notrace) = "(Instantiate "++str yestrace++' ':str notrace++")" -> str = showtrace showa showb showc - -> strictchar :: bool -> char -> strictchar strict = cond strict '!' '-' - -> printtrace :: * -> (*->[char]) -> (**->[char]) -> (***->[char]) -> trace * ** *** -> [[char]] - -> printtrace sym showa showb showc -> = ptr -> where ptr (Trace stricts rule answer history transf) -> = (showa sym++' ':printrule' showa showb stricts rule (map fst history++answernodes answer)): -> indent " " (printanswer showa showb showc answer)++ -> printhistory showa showb history++ -> printtransf sym showa showb showc transf - -> printtransf :: * -> (*->[char]) -> (**->[char]) -> (***->[char]) -> transformation * ** *** -> [[char]] - -> printtransf sym showa showb showc -> = ptf -> where ptf (Reduce reductroot trace) = ("Reduce to "++showb reductroot):ptr trace -> ptf (Annotate trace) = "Annotate":ptr trace -> ptf Stop = ["Stop"] -> ptf (Instantiate yestrace notrace) = indent "I=> " (ptr yestrace)++ptr notrace -> ptr = printtrace sym showa showb showc - -> answernodes = foldoptional [] spinenodes - -> printrule' :: (*->[char]) -> (**->[char]) -> [bool] -> rule * ** -> [**] -> [char] - -> printrule' printa printb stricts rule anchors -> = concat (map2 annot stricts args')++"-> "++root' -> where graph = rulegraph rule; args = lhs rule; root = rhs rule -> (args',root':anchors') = claim args reprs -> reprs = printgraph printa printb graph (args++root:anchors) -> annot strict repr = cond strict ('!':) id (repr++" ") -*/ - -printtrace :: - sym // LHS function symbol - (sym->String) // Symbol representation - (var->String) // Variable representation for transformed program - (pvar->String) // Variable representation for consulted program - String // Indent - (Trace sym var pvar) // Trace - *File // File before writing - -> .File // File after writing - | == var - & == pvar - -printtrace sym showsym showvar showpvar indent trace file0 -= file4 - where (Trace stricts rule answer history transf) = trace - file1 = file0 <<< indent <<< showsym sym <<< " " <<< showruleanch showsym showvar stricts rule (map fst history++answernodes answer) <<< nl - file2 = printanswer showsym showvar showpvar (indent+++" ") answer file1 - file3 = printhistory showsym showvar (indent+++" ") history file2 - file4 = printtransf sym showsym showvar showpvar indent transf file3 - -printtransf :: - sym // LHS function symbol - (sym->String) // Symbol representation - (var->String) // Variable representation for transformed program - (pvar->String) // Variable representation for consulted program - String // Indent - (Transformation sym var pvar) // Transformation to print - *File // File before writing - -> .File // File after writing - | == var - & == pvar - -printtransf sym showsym showvar showpvar indent transf file0 -= case transf - of Reduce reductroot trace - -> ptr indent trace (file0 <<< indent <<< "Reduce to " <<< showvar reductroot <<< nl) - Annotate trace - -> ptr indent trace (file0 <<< indent <<< "Annotate" <<< nl) - Stop - -> file0 <<< indent <<< "Stop" <<< nl - Instantiate rgraph yestrace notrace - -> ptr indent notrace (ptr (indent+++" ") yestrace (file0 <<< indent <<< "Instantiate " <<< showrgraph showsym showvar rgraph <<< nl)) - where ptr = printtrace sym showsym showvar showpvar - -answernodes = foldoptional [] spinenodes - -/* -Tips traverses a finite trace and produces the list of rewrite rules -that are found at the leaves of the tree. This list of rewrite rules -precisely constitutes the result of symbolic reduction of the original -rewrite rule, which can be found at the root of the tree. No folds have -been applied; this has to be done afterwards. - -> tips :: trace * ** *** -> [rule * **] - -> tips -> = foldtrace reduce annotate stop instantiate -> where reduce stricts rule answer history reductroot = id -> annotate stricts rule answer history = id -> stop stricts rule answer history = [rule] -> instantiate stricts rule answer history = (++) - - -Mapleaves maps a function onto the rules of the leaves of a trace. - -> mapleaves :: (rule * **->rule * **) -> trace * ** *** -> trace * ** *** - -> mapleaves f -> = foldtrace reduce annotate stop instantiate -> where reduce stricts rule answer history reductroot trace = Trace stricts rule answer history (Reduce reductroot trace) -> annotate stricts rule answer history trace = Trace stricts rule answer history (Annotate trace) -> stop stricts rule answer history = Trace stricts (f rule) answer history Stop -> instantiate stricts rule answer history yestrace notrace = Trace stricts rule answer history (Instantiate yestrace notrace) - -*/ - -foldtrace - :: ([Bool] (Rule sym var) (Answer sym var pvar) (History sym var) var .result -> .result) - ([Bool] (Rule sym var) (Answer sym var pvar) (History sym var) .result -> .result) - ([Bool] (Rule sym var) (Answer sym var pvar) (History sym var) -> .result) - ([Bool] (Rule sym var) (Answer sym var pvar) (History sym var) (Rgraph sym var) .result .result -> .result) - !.(Trace sym var pvar) - -> .result - -foldtrace reduce annotate stop instantiate trace -= ftr trace - where ftr (Trace stricts rule answer history transf) - = ftf stricts rule answer history transf - ftf stricts rule answer history (Reduce reductroot trace) = reduce stricts rule answer history reductroot (ftr trace) - ftf stricts rule answer history (Annotate trace) = annotate stricts rule answer history (ftr trace) - ftf stricts rule answer history Stop = stop stricts rule answer history - ftf stricts rule answer history (Instantiate ipattern yestrace notrace) = instantiate stricts rule answer history ipattern (ftr yestrace) (ftr notrace) -// ftf _ _ _ _ (Abstract _) = error "foldtrace not implemented for abstraction nodes" - -foldtransformation - :: ((Trace sym var pvar) -> .result) - (var .result -> .subresult) - (.result -> .subresult) - .subresult - ((Rgraph sym var) .result .result -> .subresult) - ([.absresult] -> .subresult) - ((Rule sym var) -> .absresult) - (.result -> .absresult) - !.(Transformation sym var pvar) - -> .subresult - -foldtransformation ftr reduce annotate stop instantiate abstract knownabstraction newabstraction transf -= ftf transf - where ftf (Reduce reductroot trace) = reduce reductroot (ftr trace) - ftf (Annotate trace) = annotate (ftr trace) - ftf Stop = stop - ftf (Instantiate ipattern yestrace notrace) = instantiate ipattern (ftr yestrace) (ftr notrace) -// ftf (Abstract as) = abstract (map fab as) -// fab (NewAbstraction t) = newabstraction (ftr t) -// fab (KnownAbstraction r) = knownabstraction r - -instance <<< Trace sym var pvar | toString sym & ==,toString,<<< var // & ==,toString,<<< pvar -where // (<<<) file trace = error "trace.<<<(Trace): blocked for debugging" - (<<<) file trace - = file <<< "Trace:" <<< nl - <<< "Stricts: " <<< showlist toString stricts <<< nl - // <<< "Rule: " <<< toString rule <<< nl - // <<< "Answer:" <<< nl writeanswer answer - // <<< "History:" <<< nl - // writeHistory history - <<< "Transformation:" <<< nl writeTransformation transf - where (Trace stricts rule answer history transf) = trace - -(writeTrace) infixl :: *File .(Trace sym var pvar) -> .File | toString sym & ==,toString,<<< var // & ==,toString,<<< pvar -(writeTrace) file trace -= file <<< "Trace:" <<< nl - <<< "Stricts: " <<< showlist toString stricts <<< nl - // <<< "Rule: " <<< ruleToString toString rule <<< nl - // <<< "Answer:" <<< nl writeanswer answer - // <<< "History:" <<< nl - // writeHistory history - <<< "Transformation:" <<< nl writeTransformation transf - where (Trace stricts rule answer history transf) = trace - -instance <<< (Transformation sym var pvar) | toString sym & ==,toString,<<< var // & ==,toString,<<< pvar -where (<<<) file (Reduce reductroot subtrace) = file <<< "Reduce; root of reduct: " <<< reductroot <<< nl <<< subtrace - (<<<) file (Annotate subtrace) = file <<< "Annotate" <<< nl <<< subtrace - (<<<) file Stop = file <<< "Stop" <<< nl - (<<<) file (Instantiate ipattern yestrace notrace) - = file <<< "Instantiate" <<< nl - // <<< "Pattern: " <<< ipattern <<< nl - <<< "Successful match..." <<< nl - <<< yestrace - <<< "End of successful match." <<< nl - <<< "Failing match..." <<< nl - <<< notrace - <<< "End of failing match." <<< nl - -(writeTransformation) infixl :: - *File - .(Transformation sym var pvar) - -> .File - | toString sym - & ==,toString,<<< var - // & ==,toString,<<< pvar - -(writeTransformation) file (Reduce reductroot subtrace) -= file <<< "Reduce; root of reduct: " <<< reductroot <<< nl - writeTrace subtrace -(writeTransformation) file (Annotate subtrace) -= file <<< "Annotate" <<< nl - writeTrace subtrace -(writeTransformation) file Stop -= file <<< "Stop" <<< nl -(writeTransformation) file (Instantiate ipattern yestrace notrace) -= file <<< "Instantiate" <<< nl - // <<< "Pattern: " <<< ipattern <<< nl - <<< "Successful match..." <<< nl - // writeTrace yestrace - <<< "End of successful match." <<< nl - <<< "Failing match..." <<< nl - // writeTrace notrace - <<< "End of failing match." <<< nl |