diff options
Diffstat (limited to 'sucl/strat.icl')
| -rw-r--r-- | sucl/strat.icl | 486 |
1 files changed, 0 insertions, 486 deletions
diff --git a/sucl/strat.icl b/sucl/strat.icl deleted file mode 100644 index 4241129..0000000 --- a/sucl/strat.icl +++ /dev/null @@ -1,486 +0,0 @@ -implementation module strat - -// $Id$ - -import spine -import history -import rule -import dnc -import graph -import pfun -import basic -from general import No,Yes,---> -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 - | Eq sym - & Eq var - & Eq pvar - -makernfstrategy hist strat rnfnodes node graph -= substrat [] spinecont rnfanswer node - where spinecont spine = Yes spine - rnfanswer = No - - 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` = (checkhistory--->"strat.checkhistory begins from strat.makernfstrategy.substrat.strat`") (graph,node) spinenodes` hist strat - -/* - ------------------------------------------------------------------------- -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 rnode spine = found (Partial rule matching rnode spine) - foundmatch matching = found (Redex rule matching) - -matchnodes - :: (pvar var -> .Bool) - (Graph sym var) - (Substrategy sym var pvar result) - ((Pfun pvar var) pvar (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 pnode openspine - = substrat (found matching pnode) 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 (zip2 [0..] nodes) - where forcenode (argno,nid) rnfrest - = substrat foundforce rnfrest nid - where foundforce spine = found (Force argno spine) - -/* - ------------------------------------------------------------------------- -STRATEGY COMPOSITION - -Check for an instance in the termination history. - -*/ - -checkhistory - :: (Graph sym var,var) - [var] - (History sym var) - (Strategy sym var pvar result) - -> Strategy sym var pvar result - | Eq sym - & Eq var - -checkhistory (sgraph,snode) spinenodes history defaultstrategy -= (if (isEmpty histpats) defaultstrategy unsafestrategy) <--- "strat.checkhistory ends" - where histpats - = (matchhistory--->"history.matchhistory begins from strat.checkhistory.histpats") history spinenodes sgraph snode - unsafestrategy _ _ found _ _ - = found (Unsafe (hd histpats)) - - -// Check for curried applications - -checkarity - :: !(sym -> Int) // Arity of function symbol - (Strategy sym var pvar .result) // Default strategy - (Substrategy sym var pvar .result) // Substrategy - (Graph sym var) // Subject graph - ((Subspine sym var pvar) -> .result) // Spine continuation - .result // RNF continuation - !.(Node sym var) // Subject node - -> .result - -checkarity funarity defaultstrategy substrat subject found rnf (ssym,sargs) -| shortern arity sargs -= rnf -| eqlenn arity sargs -= defaultstrategy substrat subject found rnf (ssym,sargs) -= abort ("checktype: symbol occurrence with actual arity "+++toString (length sargs)+++" greater than its type arity "+++toString arity) - where arity = funarity ssym - -shortern n _ | n<=0 = False -shortern _ [] = True -shortern n [x:xs] = shortern (n-1) xs - -eqlenn n _ | n<0 = False -eqlenn 0 [] = True -eqlenn n [x:xs] = eqlenn (n-1) xs - - -// Check for strict arguments - -checkstricts - :: !(sym -> [.Bool]) // Strict arguments of function - (Strategy sym var pvar .result) // Default strategy - (Substrategy sym var pvar .result) // Substrategy - (Graph sym var) // Subject graph - ((Subspine sym var pvar) -> .result) // Spine continuation - .result // RNF continuation - !.(Node sym var) // Subject node - -> .result - -checkstricts funstricts defaultstrategy substrat subject found rnf (ssym,sargs) -= forcenodes substrat found rnf` strictnodes - where rnf` = defaultstrategy substrat subject found rnf (ssym,sargs) - tstricts = funstricts ssym - 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->String) - (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 showsym isconstr defstrat substrat subject found rnf (ssym,sargs) -| isconstr ssym ---> ("strat.checkconstr begins for "+++showsym ssym) -= rnf <--- ("strat.checkconstr ends (RNF)") -= defstrat substrat subject found rnf (ssym,sargs) <--- ("strat.checkconstr ends (default strategy)") |