aboutsummaryrefslogtreecommitdiff
path: root/sucl/law.icl
diff options
context:
space:
mode:
Diffstat (limited to 'sucl/law.icl')
-rw-r--r--sucl/law.icl179
1 files changed, 179 insertions, 0 deletions
diff --git a/sucl/law.icl b/sucl/law.icl
new file mode 100644
index 0000000..836e3b3
--- /dev/null
+++ b/sucl/law.icl
@@ -0,0 +1,179 @@
+implementation module law
+
+/*
+
+> %export
+> cleanlaws
+> corestrategy
+
+> %include "dnc.lit"
+
+> %include "../src/basic.lit"
+> %include "../src/pfun.lit"
+> %include "../src/graph.lit"
+> %include "../src/complete.lit"
+> %include "../src/rule.lit"
+> %include "../src/spine.lit"
+> %include "strat.lit"
+> %include "../src/clean.lit"
+
+> intmullaw :: law symbol ** node ****
+
+> intmullaw substrat subject found rnf sargs fail
+
+> = rulelaw (leftunitrule (Int 1)) substrat subject found rnf sargs fail'
+> where fail' = rulelaw (rightunitrule (Int 1)) substrat subject found rnf sargs fail''
+> fail'' = primlaw (intop product) substrat subject found rnf sargs fail
+
+> mullaws
+> = [ rulelaw (leftunitrule (Int 1))
+> , rulelaw (rightunitrule (Int 1))
+> , primlaw (intop product)
+> ]
+
+> intaddlaw :: law symbol ** node ****
+
+> intaddlaw substrat subject found rnf sargs fail
+> = trylaw subject found' sargs (leftunitrule (Int 0)) fail'
+> where fail' = trylaw subject found' sargs (rightunitrule (Int 0)) fail''
+> fail'' = strictprimop (intop sum) substrat subject found sargs fail
+> found' subspine = found subspine
+
+> addlaws
+> = [ rulelaw (leftunitrule (Int 0))
+> , rulelaw (rightunitrule (Int 0))
+> , primlaw (intop sum)
+> ]
+
+> intsublaw :: law symbol ** node ****
+
+> intsublaw substrat subject found rnf sargs fail
+> = trylaw subject found' sargs (rightunitrule (Int 0)) fail'
+> where fail' = strictprimop (intop sublist) substrat subject found sargs fail
+> found' subspine = found subspine
+> sublist [x,y] = x-y
+
+> sublaws
+> = [ rulelaw (rightunitrule (Int 0))
+> , primlaw (intop sublist)
+> ]
+> where sublist [x,y] = x-y
+
+> intop :: ([num]->num) -> [symbol] -> symbol
+> intop op symbols = Int (op [i|Int i<-symbols])
+
+> leftunitrule leftunit
+> = mkrule [Named "leftarg",Named "rightarg"] (Named "rightarg") (updategraph (Named "leftarg") (leftunit,[]) emptygraph)
+
+> rightunitrule rightunit
+> = mkrule [Named "leftarg",Named "rightarg"] (Named "leftarg") (updategraph (Named "rightarg") (rightunit,[]) emptygraph)
+
+> strictprimop
+> :: ([*]->*) ->
+> substrategy * ** node **** ->
+> graph * ** ->
+> (subspine * ** node->****) ->
+> [**] ->
+> **** ->
+> ****
+
+> strictprimop op substrat subject found sargs fail
+> = forcenodes substrat found foundredex sargs, if and (map fst conts)
+> = fail, otherwise
+> where conts = map (dnc (const "in strictprimop") subject) sargs
+> result = op (map (fst.snd) conts)
+> primrule = mkrule primargs primroot primgraph
+> primargs = map snd (zip2 sargs heap)
+> primroot = Named "primresult"
+> primgraph = updategraph primroot (result,[]) emptygraph
+> matching = foldr (uncurry extend) emptypfun (zip2 primargs sargs)
+> foundredex = found (Redex primrule matching)
+
+> primlaw
+> :: ([*]->*) ->
+> law * ** node ****
+
+> primlaw op substrat subject found rnf sargs fail
+> = strictprimop op substrat subject found sargs fail
+
+------------------------------------------------------------------------
+
+> cleanlaws :: [(symbol,law symbol ** node ****)]
+
+> cleanlaws
+> = [(User "deltaI" "*",law) | law <- mullaws] ++
+> [(User "deltaI" "+",law) | law <- addlaws] ++
+> [(User "deltaI" "-",law) | law <- sublaws] ++
+> [(User "deltaI" "++",primlaw inc)] ++
+> [(User "deltaI" "--",primlaw dec)]
+
+> inc [Int n] = Int (n+1)
+> dec [Int n] = Int (n-1)
+
+------------------------------------------------------------------------
+
+> corestrategy :: (graph symbol node->node->**->bool) -> strategy symbol ** node ****
+
+Forcing arguments has already been done by the type rule
+Also, using trylaw is easier
+
+> corestrategy matchable substrat subject found rnf (Apply,snodes)
+> = trylaw subject found snodes (applyrule nc) (found Delta)
+> where nc = dnc (const "in corestrategy") subject (hd snodes)
+
+> corestrategy matchable substrat subject found rnf (If,snodes)
+> = tryrules matchable substrat subject found snodes (found MissingCase) ifrules
+
+> corestrategy matchable substrat subject found rnf (Select a i,snodes)
+> = tryrules matchable substrat subject found snodes (found MissingCase) [selectrule a i]
+
+> corestrategy matchable substrat subject found rnf (User module id,snodes)
+> = found MissingCase
+
+> corestrategy matchable substrat subject found rnf (ssym,snodes)
+> = rnf
+
+> applyrule :: (bool,(*,[**])) -> rule * node
+> applyrule (sdef,scont)
+> = aprule (anode,(sym,aargs)) [enode] aroot
+> where (aargs,anode:aroot:enode:heap') = claim sargs heap
+> (sym,sargs)
+> = scont, if sdef
+> = (nosym,[]), otherwise
+> nosym = error "applyrule: no function symbol available"
+
+> aprule :: (***,(*,[***])) -> [***] -> *** -> rule * ***
+> aprule (anode,(sym,aargs)) anodes aroot
+> = mkrule (anode:anodes) aroot agraph
+> where agraph
+> = ( updategraph aroot (sym,aargs++anodes)
+> . updategraph anode (sym,aargs)
+> ) emptygraph
+
+> apmatching :: [**] -> [***] -> pfun *** **
+> apmatching snodes anodes
+> = foldr (uncurry extend) emptypfun nodepairs
+> where nodepairs = zip2 anodes snodes
+
+> claims :: [[*]] -> [**] -> ([[**]],[**])
+> claims [] heap = ([],heap)
+> claims (nodes:nodess) heap
+> = (nodes':nodess',heap'')
+> where (nodes',heap') = claim nodes heap
+> (nodess',heap'') = claims nodess heap'
+
+> ifrules :: [rule symbol node]
+
+> ifrules
+> = [ifrule True then,ifrule False else]
+> where ifrule bool branch = mkrule [cond,then,else] branch (updategraph cond (Bool bool,[]) emptygraph)
+> cond = Named "cond"; then = Named "then"; else = Named "else"
+
+> selectrule :: num -> num -> rule symbol node
+
+> selectrule a i
+> = mkrule [tuple] (args!(i-1)) (updategraph tuple (Tuple a,args) emptygraph)
+> where tuple = Named "tuple"
+> args = take a (tl heap)
+
+*/