diff options
Diffstat (limited to 'sucl/spine.icl')
| -rw-r--r-- | sucl/spine.icl | 381 |
1 files changed, 0 insertions, 381 deletions
diff --git a/sucl/spine.icl b/sucl/spine.icl deleted file mode 100644 index cf81386..0000000 --- a/sucl/spine.icl +++ /dev/null @@ -1,381 +0,0 @@ -implementation module spine - -// $Id$ - -import history -import rule -import dnc -import graph -import pfun -import basic -from general import No,Yes -import StdEnv - -/* - -spine.lit - The extended functional strategy -============================================ - -Description ------------ - -This script implements the strategy answer, and a function to compute it -for a given graph in a rewrite system. - -The strategy answer is a spine -- in principle a colon of partial -matches from patterns of rewrite rules to the graph, with at the bottom -the insteresting part: a redex, an open node or something else. See the -definition of subspine for that. - -The strategy function attempts to find a redex to reduce the graph to -normal form instead of root normal form. This is done by applying a -root normal form strategy recursively in preorder over the graph (of -course ignoring cycles). The node at which the root normal form -strategy was applied is returned in the strategy answer, so laziness can -be preserved. - ------------------------------------------------------------- - -Interface ---------- - -Exported identifiers: - -> %export -> answer || Strategy answer type -> foldspine || Higher order general spine folding -> ifopen || Check for answer indicating Open -> printanswer || Make a human-readable representation of an answer -> printspine || Make a human-readable representation of a spine -> showanswer || Make a representation of an answer -> showspine || Make a representation of a spine -> showsubspine || Make a representation of a subspine -> spine || Colon of partial matches -> spinenodes || Determine nodes in a spine -> spinetip || Determine bottom of spine -> subspine || Bottom of spine - -> history || Symbolic reduction history type -> printhistory || Make a human-readable representation of a history -> showhistory || Make a representation of a history - -Required types: - - subspine - rule@rule.lit,rgraph@rule.lit,pfun@pfun.lit - ------------------------------------------------------------- - -Includes --------- - -> %include "basic.lit" || optional -> %include "pfun.lit" || pfun -> %include "graph.lit" || graph -> %include "rule.lit" || rgraph rule - ------------------------------------------------------------- - -Implementation --------------- - - -Answer describes the answer of a strategy. Absence of a spine implies -that the node was in root normal form. - -> answer * ** *** == optional (spine * ** ***) - -> showanswer showa showb showc = showoptional (showspine showa showb showc) -> printanswer printa printb printc = foldoptional ["Rnf"] (printspine printa printb printc) - -*/ - -:: Answer sym var pvar - :== Optional (Spine sym var pvar) - -printanswer :: - (sym->String) - (var->String) - (pvar->String) - String - -> (Answer sym var pvar) - *File - -> .File - | == var - & == pvar - -printanswer showsym showvar showpvar indent -= foldoptional (printrnf indent) (printspine showsym showvar showpvar indent) - -printrnf indent file = file <<< indent <<< "RNF" <<< nl - -/* - -Spine describes the spine returned by a strategy. It contains the node -at which the strategy was applied, and the result for that node. - -> spine * ** *** == (**,subspine * ** ***) - -> showspine showa showb showc = showpair showb (showsubspine showa showb showc) - -> printspine printa printb printc -> = foldspine pair cycle delta force missingcase open partial unsafe redex strict -> where pair node (line,lines) = (printb node++" => "++line):lines -> cycle = ("Cycle",[]) -> delta = ("Delta",[]) -> force lines = ("Force",lines) -> missingcase = ("MissingCase",[]) -> open rgraph = ("Open "++printrgraph printa printc rgraph,[]) -> partial rule matching lines = ("Partial <fn> "++printrule printa printc rule++' ':printpfun printc printb matching,lines) -> unsafe rgraph = ("Unsafe "++printrgraph printa printb rgraph,[]) -> redex rule matching = ("Redex <fn> "++printrule printa printc rule++' ':printpfun printc printb matching,[]) -> strict = ("Strict",[]) - -*/ - -:: Spine sym var pvar - :== (var,Subspine sym var pvar) - -printspine :: - (sym->String) - (var->String) - (pvar->String) - String - -> (Spine sym var pvar) - *File - -> .File - | == var - & == pvar - -printspine showsym showvar showpvar indent -= foldspine pair cycle delta force missingcase open partial unsafe redex strict - where pair node (line,printrest) file = printrest (file <<< indent <<< showvar node <<< ": " <<< line <<< nl) - cycle = ("Cycle",id) - delta = ("Delta",id) - force argno printrest = ("Force argument "+++toString argno,printrest) - missingcase = ("MissingCase",id) - open rgraph = ("Open "+++hd (printgraphBy showsym showpvar (rgraphgraph rgraph) [rgraphroot rgraph]),id) - partial rule matching pvar printrest = ("Partial <fn> "+++showruleanch showsym showpvar (repeat False) rule [pvar]+++" <"+++showpvar pvar+++"> "+++showpfun showpvar showvar matching,printrest) - unsafe rgraph = ("Unsafe "+++hd (printgraphBy showsym showvar (rgraphgraph rgraph) [rgraphroot rgraph]),id) - redex rule matching = ("Redex <fn> "+++showruleanch showsym showpvar (repeat False) rule []+++" "+++showpfun showpvar showvar matching,id) - strict = ("Strict",id) - -/* - -Subspine describes what was the result of the strategy applied to a node -in a graph. - -> subspine * ** *** -> ::= Cycle | || The spine contains a cycle -> Delta | || An imported (delta) rule was found -> Force (spine * ** ***) | || Global strictness annotation forced evaluation of a subgraph -> MissingCase | || All alternatives failed for a function symbol -> Open (rgraph * ***) | || Need root normal form of open node for matching -> Partial (rule * ***) (pfun *** **) (spine * ** ***) | || A rule was strictly partially matched -> Unsafe (rgraph * **) | || Terminated due to immininent recursion -> Redex (rule * ***) (pfun *** **) | || Total match -> Strict || Need root normal form due to strictness - -> showsubspine showa showb showc -> = sh -> where sh Cycle = "Cycle" -> sh Delta = "Delta" -> sh (Force spine) = "(Force "++showspine showa showb showc spine++")" -> sh MissingCase = "MissingCase" -> sh (Open rgraph) = "(Open "++showrgraph showa showc rgraph++")" -> sh (Partial rule matching spine) = "(Partial "++showrule showa showc rule++' ':showpfun showc showb matching++' ':showspine showa showb showc spine++")" -> sh (Unsafe rgraph) = "(Unsafe "++showrgraph showa showb rgraph++")" -> sh (Redex rule matching) = "(Redex "++showrule showa showc rule++' ':showpfun showc showb matching++")" -> sh Strict = "Strict" - - printsubspine printa printb printc - = pr - where pr Cycle = "Cycle" - pr Delta = "Delta" - pr (Force argno spine) = "(Force <argno> "++printspine printa printb printc spine++")" - pr MissingCase = "MissingCase" - pr (Open rgraph) = "(Open "++printrgraph printa printc rgraph++")" - pr (Partial rule matching spine) = "(Partial "++printrule printa printc rule++' ':printpfun printc printb matching++' ':printspine printa printb printc spine++")" - pr (Unsafe rgraph) = "(Unsafe "++printrgraph printa printb rgraph++")" - pr (Redex rule matching) = "(Redex "++printrule printa printc rule++' ':printpfun printc printb matching++")" - pr Strict = "Strict" - -*/ - -:: Subspine sym var pvar - = Cycle // The spine contains a cycle - | Delta // An imported (delta) rule was found - | Force Int (Spine sym var pvar) // Global strictness annotation forced evaluation of a subgraph at specified argument position - | MissingCase // All alternatives failed for a function symbol - | Open (Rgraph sym pvar) // Need root normal form of open node for matching - | Partial (Rule sym pvar) (Pfun pvar var) pvar (Spine sym var pvar) // A rule was strictly partially matched - | Unsafe (HistoryPattern sym var) // Terminated due to immininent recursion - | Redex (Rule sym pvar) (Pfun pvar var) // Total match - | Strict // Need root normal form due to strictness - -/* - -> foldspine -> :: (**->****->*****) -> -> **** -> -> **** -> -> (*****->****) -> -> **** -> -> (rgraph * ***->****) -> -> (rule * ***->pfun *** **->*****->****) -> -> (rgraph * **->****) -> -> (rule * ***->pfun *** **->****) -> -> **** -> -> spine * ** *** -> -> ***** - -> foldspine pair cycle delta force missingcase open partial unsafe redex strict -> = fold -> where fold (node,subspine) = pair node (foldsub subspine) -> foldsub Cycle = cycle -> foldsub Delta = delta -> foldsub (Force spine) = force (fold spine) -> foldsub MissingCase = missingcase -> foldsub (Open rgraph) = open rgraph -> foldsub (Partial rule matching spine) = partial rule matching (fold spine) -> foldsub (Unsafe rgraph) = unsafe rgraph -> foldsub (Redex rule matching) = redex rule matching -> foldsub Strict = strict - -*/ - -foldspine - :: !(var .subresult -> .result) // Fold the spine itself - .subresult // Fold a Cycle subspine - .subresult // Fold a Delta subspine - (Int .result -> .subresult) // Fold a Force subspine - .subresult // Fold a MissingCase subspine - ((Rgraph sym pvar) -> .subresult) // Fold an Open subspine - ((Rule sym pvar) (Pfun pvar var) pvar .result -> .subresult) // Fold a Partial subspine - ((HistoryPattern sym var) -> .subresult) // Fold an Unsafe subspine - ((Rule sym pvar) (Pfun pvar var) -> .subresult) // Fold a Redex subspine - .subresult // Fold a Strict subspine - .(Spine sym var pvar) // The spine to fold - -> .result // The final result - -foldspine pair cycle delta force missingcase open partial unsafe redex strict spine -= fold spine - where fold spine - = pair node (foldsub subspine) - where (node,subspine) = spine - foldsub Cycle = cycle - foldsub Delta = delta - foldsub (Force argno spine) = force argno (fold spine) - foldsub MissingCase = missingcase - foldsub (Open rgraph) = open rgraph - foldsub (Partial rule matching rnode spine) = partial rule matching rnode (fold spine) - foldsub (Unsafe histpat) = unsafe histpat - foldsub (Redex rule matching) = redex rule matching - foldsub Strict = strict - -spinetip :: !(Spine sym var pvar) -> Spine sym var pvar -spinetip (_,Force argno spine) = spinetip spine -spinetip (_,Partial _ _ pnode spine) = spinetip spine -spinetip spine = spine - -spinenodes :: .(Spine sym var pvar) -> [var] -spinenodes spine -= nodes - where partial _ _ _ = id - redex _ _ = [] - nodes = foldspine cons [] [] (const id) [] (const []) partial (const []) redex [] spine - -ifopen :: result result !.(Answer sym var pvar) -> result -ifopen open other spine -= foldoptional other (checkopen o spinetip) spine - where checkopen (onode,Open pattern) = open - checkopen tip = other - - -/********************************************* -* Extending the history according to a spine * -*********************************************/ - -// A function that associates specific patterns with extensible nodes -// To be used for extending history patterns -:: LinkExtender sym var - :== (Link var) // The extensible link to look for - -> HistoryPattern sym var // The associated pattern - -extendhistory - :: (Graph sym var) - (var -> var) - (Spine sym var pvar) - (History sym var) - -> History sym var - | == var - & == pvar - -extendhistory sgraph redirection spine history -= snd (foldspine (extendpair sgraph redirection) d d (const id) d (const d) (extendpartial sgraph) (const d) (extendredex sgraph history) d spine) - where d = (emptygraph,history) - - -extendpair - :: (Graph sym var) - (var->var) - var - (Graph sym var,History sym var) - -> (Graph sym var,History sym var) - | == var - -extendpair sgraph redirect snode (hgraph,history) -= (hgraph`,remap (redirect snode) [mkrgraph snode hgraph`:foldmap id [] history snode] (forget snode history)) - where hgraph` = if sdef (updategraph snode scont hgraph) hgraph - (sdef,scont) = dnc (const "in extendpair") sgraph snode - -extendpartial - :: (Graph sym var) - (Rule sym pvar) - (Pfun pvar var) - pvar - (Graph sym var,History sym var) - -> (Graph sym var,History sym var) - | == var - & == pvar - -extendpartial sgraph rule matching rnode (hgraph,history) -= (extgraph` sgraph rule matching hgraph,history) - -extendredex - :: (Graph sym var) - (History sym var) - (Rule sym pvar) - (Pfun pvar var) - -> (Graph sym var,History sym var) - | == var - & == pvar - -extendredex sgraph history rule matching -= (extgraph` sgraph rule matching emptygraph,history) - -extgraph` :: (Graph sym var) (Rule sym pvar) -> (Pfun pvar var) (Graph sym var) -> Graph sym var | == var & == pvar -extgraph` sgraph rule -= extgraph sgraph rgraph (varlist rgraph (arguments rule)) - where rgraph = rulegraph rule - -(writeanswer) infixl :: *File (Answer sym var pvar) -> .File | toString sym & ==,toString,<<< var // & ==,toString,<<< pvar -(writeanswer) file No = file <<< "<root-normal-form>" <<< nl -(writeanswer) file (Yes spine) = file writespine spine <<< nl - -(writespine) infixl :: *File (Spine sym var pvar) -> .File | toString sym & ==,toString,<<< var // & ==,toString,<<< pvar -(writespine) file (var,subspine) = file <<< "(" <<< var <<< "," <<< subspine <<< ")" - -instance <<< (Subspine sym var pvar) | toString sym & ==,toString,<<< var // & ==,toString,<<< pvar -where -/* - (<<<) file _ = file <<< "<subspine>" -*/ - (<<<) file Cycle = file <<< "Cycle" - (<<<) file Delta = file <<< "Delta" - (<<<) file (Force argno spine) = file <<< "Force " <<< argno <<< " " writespine spine - (<<<) file MissingCase = file <<< "MissingCase" - (<<<) file (Open pattern) = file <<< "Open <rgraph>" - (<<<) file (Partial rule matching focus spine) = file <<< "Partial {rule=<Rule sym pvar>, matching=<Pfun pvar var>, focus=<pvar>, spine=" writespine spine <<< "}" - (<<<) file (Unsafe pattern) = file <<< "Unsafe " writergraph pattern - (<<<) file (Redex rule matching) = file <<< "Redex {rule=<Rule sym pvar>, matching=<Pfun pvar var>}" - (<<<) file Strict = file <<< "Strict" |