[Projects] XRM 38: Add support for ranges in constant propagation.

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit &lt;sigoure.benoit(a)lrde.epita.fr&gt; Add support for ranges in constant propagation. /!\ This commit has all the debugging messages left in the source of prism-desugar because it seems to trigger a bug in the Stratego compiler. Therefore we'll be able to use this revision to investigate the bug. Roughly, what happens is that a strategy such as: a;b;c;...; (X <+ Y <+ Z ...) is inlined and transformed (in C) as something like: ((a;b;c;...;X) <+ (a;b;c;...;Y) <+ (a;b;c;...;Z) <+ ...) which is totally wrong if a;b;c;... has side effects (such as defining dynamic rules) * src/str/prism-desugar.str: Add support for ranges. * src/str/reals.str: Fix newbie mistake. * tests/prism/testeq.pm: New. * TODO: Update. TODO | 20 ++++++------- src/str/prism-desugar.str | 70 +++++++++++++++++++++++++++++++--------------- src/str/reals.str | 4 +- tests/prism/testeq.pm | 21 +++++++++++++ 4 files changed, 81 insertions(+), 34 deletions(-) Index: src/str/prism-desugar.str --- src/str/prism-desugar.str (revision 37) +++ src/str/prism-desugar.str (working copy) @@ -147,43 +147,69 @@ EvalGtEq: |[ d1 >= d2 ]| -> <compare(geqR)>(d1, d2) - /* FIXME: The following rules could be generalized - We need to check whether d1 appears in the list at the RHS */ - EvalEq: - |[ d1 = d2 ]| -> <compare(real-eq)>(d1, d2) + EvalSimpleEq: + |[ d1 = d2 ]| -> res + where say(!"@@@ EvalSimpleEq");debug + ; <compare(real-eq)>(d1, d2) => res;debug + + EvalSimpleRangeEq: + |[ e = e1..e2 ]| -> res + where say(!"@@@ EvalSimpleRangeEq range");debug + ; <DesugarRangeEq(|e)>(Range(e1, e2)) => res;debug + + EvalComplexEq: + Eq(e, a*) -> res + where say(!"@@@ EvalComplexEq");<debug>a* + ; !a* + ; map(DesugarRangeEq(|e) <+ \ e2 -> |[ e=e2 ]| \);debug + ; foldr(!False(), \ (x, y) -> Or(x, y) \) => res + ; say(!" end of EvalComplexEq:");debug - /* FIXME: Same thing as EvalEq */ +strategies + + EvalEq = ?a;?Eq(_,_);say(!"@@@ EvalEq starting:");debug;rules(Hello: a); + (?Eq(_, [Eq(_, _)]) <+ EvalSimpleEq <+ EvalSimpleRangeEq <+ (?|[ e = e2 ]| < debug;fail + EvalComplexEq)) + +rules + + + //EvalNeq: + // |[ d1 != d2 ]| -> <compare(not(real-eq))>(d1, d2) EvalNeq: - |[ d1 != d2 ]| -> <compare(not(real-eq))>(d1, d2) + NotEq(e, a*) -> res + where say(!"@@@ EvalNeq");<not(?[_])>a*;<debug>a* + ; map(DesugarRangeNeq(|e) <+ \ e2 -> |[ e!=e2 ]| \);debug + ; foldr(!False(), \ (x, y) -> Or(x, y) \) => res;debug + + DesugarRangeEq(|e): + Range(e2, e3) -> |[ e >= e2 & e <= e3]| + + DesugarRangeNeq(|e): + Range(e2, e3) -> |[ e < e2 & e > e3]| rules -/* FIXME: Can we optimize this in a single rule? - Since the optimization would decrease readability, - is it worth it? - eg: - EvalAnd: - And(x, y) -> True() where x => True(); y => True() - EvalAnd: - And(x, y) -> False() where x => False() + y => False() -*/ EvalAnd: |[ true & true ]| -> |[ true ]| EvalAnd: - |[ true & false ]| -> |[ false ]| + |[ e & false ]| -> |[ false ]| + EvalAnd: + |[ false & e ]| -> |[ false ]| EvalAnd: - |[ false & true ]| -> |[ false ]| + |[ e & true ]| -> |[ e ]| EvalAnd: - |[ false & false ]| -> |[ false ]| + |[ true & e ]| -> |[ e ]| EvalOr: - |[ true | true ]| -> |[ true ]| + |[ true | e ]| -> |[ true ]| EvalOr: - |[ true | false ]| -> |[ true ]| - EvalOr: - |[ false | true ]| -> |[ true ]| + |[ e | true ]| -> |[ true ]| EvalOr: |[ false | false ]| -> |[ false ]| + EvalOr: + |[ e | false ]| -> |[ e ]| + EvalOr: + |[ false | e ]| -> |[ e ]| rules Index: src/str/reals.str --- src/str/reals.str (revision 37) +++ src/str/reals.str (working copy) @@ -16,8 +16,8 @@ divR = (string-to-real, string-to-real); divr; real-to-string gtR = where((string-to-real, string-to-real); gtr) - geqR = where((string-to-real, string-to-real); ?(x,x) <+ gtr) - ltR = where((string-to-real, string-to-real); not(?(x,x) <+ gtr)) + geqR = where((string-to-real, string-to-real); (?(x,x) <+ gtr)) + ltR = where((string-to-real, string-to-real); (not(?(x,x) <+ gtr))) leqR = where((string-to-real, string-to-real); not(gtr)) maxR = where((string-to-real, string-to-real); maxr) minR = where((string-to-real, string-to-real); minr) Index: tests/prism/testeq.pm --- tests/prism/testeq.pm (revision 0) +++ tests/prism/testeq.pm (revision 0) @@ -0,0 +1,21 @@ +module test + x : [0..42]; + [] 10=10 -> (x'=1); + [] 10=1 -> (x'=2); + [] 10=1 | 10=10 -> (x'=3); + + [] 10<=10 -> (x'=4); + [] 10<10 -> (x'=5); + [] 10>=10 -> (x'=6); + [] 10>10 -> (x'=7); + + [] 1<=10 -> (x'=8); + [] 1<10 -> (x'=9); + [] 1>=10 -> (x'=10); + [] 1>10 -> (x'=11); + + [] 10<=1 -> (x'=12); + [] 10<1 -> (x'=13); + [] 10>=1 -> (x'=14); + [] 10>1 -> (x'=15); +endmodule Index: TODO --- TODO (revision 37) +++ TODO (working copy) @@ -98,16 +98,6 @@ ## Desugarisation ## ## -------------- ## - * Desugarise ranges (?) - x = 1..5,7,10..13 - ==> (x>=1 & x<=5) | (x=7) | (x>=10 & x<=13) - - * Expand formulas, eg - formula lfree = p2=0..4,6,10; - // ... - [] p1=2 & lfree -> (p1'=4); - ==> [] p1=2 & (p2=0..4,6,10) -> (p1'=4); - ## ------------- ## ## Type checking ## ## ------------- ## @@ -175,3 +165,13 @@ prism-desugar to take these values into account (which will automagically allow things such as x[N] to declare an array for instance, where N is a global const) + + * Expand formulas, eg + formula lfree = p2=0..4,6,10; + // ... + [] p1=2 & lfree -> (p1'=4); + ==> [] p1=2 & (p2=0..4,6,10) -> (p1'=4); + + * Desugarise ranges (?) + x = 1..5,7,10..13 + ==> (x>=1 & x<=5) | (x=7) | (x>=10 & x<=13)