Projects May 2006

projects@lrde.epita.fr

10 participants
53 discussions

by michael.cadilhac＠lrde.org

Les nouveaux flags pour ICC sont : # Don't use CXXFLAGS, it's CPP and LD stuffs. export CPPFLAGS="-D_LINUX -I/home/lrde/admin/lrde/usr/intel/compiler90/include/c++/" export LDFLAGS="-cxxlib-icc" export LD_LIBRARY_PATH=/home/lrde/admin/lrde/usr/intel/compiler90/include/lib/ PATH=/home/lrde/admin/lrde/usr/intel/compiler90/bin:$PATH test_tree vaucanson-icc bootstrap configure build demos install distcheck C'est obligatoire car VCSN détruit les CXXFLAGS pour une partie du make check. -- | Would someone please DTRT with this, Michaël `Micha' Cadilhac | | then ACK? cadilh_m - Epita 2007 - CSI | | -- Richard Stallman JID: micha(a)amessage.be | `-- - - - - --'

17 years, 11 months

XRM 41: Add the rand() builtin.

by SIGOURE Benoit

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Add the rand() builtin. * src/lib/xrm/pp/xrm-expression.str: Add boxing for the rand builtin. * src/str/xrm-to-prism.str: Split xrm-to-prism-desugar in several rules. Add rand(N) and rand(from, to) builtin. * src/str/ice.str: Add not-implemented() strategy. * src/str/eval-meta-code.str: Nothing. * src/syn/xrm/XRM-Expression.sdf: Add the rand builtin. * src/syn/prism/PRISM-MetaVars.sdf: Add a meta-var. * src/syn/prism/StrategoPRISM.sdf: Ditto. * tests/xrm/rand.xpm: New. * tests/prism/formula.pm: New. * TODO: Update. TODO | 12 +++++++ src/lib/xrm/pp/xrm-expression.str | 6 +++ src/str/eval-meta-code.str | 2 - src/str/ice.str | 14 ++++++++ src/str/xrm-to-prism.str | 63 ++++++++++++++++++++++++++++++++++---- src/syn/prism/PRISM-MetaVars.sdf | 1 src/syn/prism/StrategoPRISM.sdf | 1 src/syn/xrm/XRM-Expression.sdf | 9 +++++ tests/prism/formula.pm | 6 +++ tests/xrm/rand.xpm | 12 +++++++ 10 files changed, 120 insertions(+), 6 deletions(-) Index: src/lib/xrm/pp/xrm-expression.str --- src/lib/xrm/pp/xrm-expression.str (revision 40) +++ src/lib/xrm/pp/xrm-expression.str (working copy) @@ -1,4 +1,5 @@ module xrm-expression +imports helpers rules @@ -7,3 +8,8 @@ prism-to-box: LeftShift(lhs, rhs) -> H hs=1 [~lhs MATH["<<"] ~rhs] + + prism-to-box: // NOTE: we use the old builtin-call style + Rand(args) // func(rand, ...) is just uggly. + -> box |[ H hs=0 [ "rand" "(" H hs=1 [ ~args-imploded ] ")" ] ]| + where <implode-list(|",")> args => args-imploded Index: src/str/xrm-to-prism.str --- src/str/xrm-to-prism.str (revision 40) +++ src/str/xrm-to-prism.str (working copy) @@ -31,7 +31,11 @@ xrm-to-prism = /* remove XRM sugar, normalize some nodes */ - innermost(xrm-to-prism-desugar) + innermost( + DesugarRightShift <+ DesugarLeftShift + <+ DesugarImplicitForStep <+ DesugarImplicitElse + <+ DesugarRand <+ EvalRand + ) /* Collect static const variables * Two goals: expand them if needed, look for variable name conflicts. */ @@ -58,6 +62,12 @@ ; ModulesFile(id, flatten-list) ; ModulesFile(id, map(try(Module(id, flatten-list)))) + /* get the list of generated modules that generates random numbers */ + ; where(bagof-RandGenModules; reverse => rand-gen-modules) + + /* add the modules that generates random numbers in the ModulesFile */ + ; ModulesFile(id, <conc>(<id>, rand-gen-modules)) + /* remove array accesses: x[i] -> x_i */ ; topdown(try(remove-array-accesses)) @@ -66,24 +76,67 @@ rules - xrm-to-prism-desugar: + DesugarRightShift: |[ e1 >> e2 ]| -> |[ e1 / func(pow, 2, e2) ]| - xrm-to-prism-desugar: + DesugarLeftShift: |[ e1 << e2 ]| -> |[ e1 * func(pow, 2, e2) ]| /** if the step is not specified, it is implicitly set to 1 */ - xrm-to-prism-desugar: + DesugarImplicitForStep: MetaFor(identifier, from, to, body) -> MetaFor(identifier, from, to, Int("1"), body) - xrm-to-prism-desugar: + DesugarImplicitElse: //|[ if e then m* end ]| -> |[ if e then m* else end ]| //|[ if e then s* end ]| -> |[ if e then s* else end ]| MetaIf(e, m*) -> MetaIf(e, m*, []) + /** rand(x) -> rand(0, x) */ + DesugarRand: + Rand([arg]) -> Rand([Int("0"), arg]) + + EvalRand: + Rand(args) -> Identifier(rand-var) + where ?current-term + ; if not( !args => [from, to] ) then + err-msg(|<concat-strings>["invalid call to XRM builtin: rand", + " takes either one or two arguments"]) + ; !current-term; debug; <xtc-exit> 4 + end + ; <prism-desugar> from => from' + ; <prism-desugar> to => to' + ; if not( !from' => Int(ifrom); !to' => Int(ito) ) then + err-msg(|<concat-strings>["invalid call to XRM builtin: rand's", + " arguments must be statically evaluable"]) + ; !current-term; debug; <xtc-exit> 4 + end + ; <debug> ifrom + ; <debug> ito + ; <newname> "__rand" => rand-var + ; !ProbUpdate( Div(Int("1"), Int( <subtS>(ito, ifrom) )) + , UpdateList([UpdateElement(IdentifierPrime(rand-var), FIXME())])) + ; {| RandUpdateList: + for-loop(gen-rand-update-list | ifrom, ito, "1", []) + ; bagof-RandUpdateList + |} + ; reverse + ; !ProbUpdateList(<id>) => u + ; !|[ module ~id:rand-var + ~id:rand-var : [~int:ifrom..~int:ito]; + [] true -> u; + endmodule ]| => rand-gen-module + ; rules(RandGenModules:+ _ -> rand-gen-module) + +strategies + + gen-rand-update-list(|i, data) = + topdown(try(\ FIXME() -> Int(i) \)) => rand-update + ; rules(RandUpdateList:+ _ -> rand-update) + signature constructors Type : String -> Type + FIXME : FIXME strategies Index: src/str/ice.str --- src/str/ice.str (revision 40) +++ src/str/ice.str (working copy) @@ -20,3 +20,17 @@ ; !term ; debug ; <xtc-exit> 42 + + /** Things that should work but are not yet supported. */ + not-implemented(|calling-strategy-name, what) = + err-msg(|<concat-strings>["not yet implemented: ", what, " (in strategy ", + calling-strategy-name, ")"]) + ; <xtc-exit> 51 + + not-implemented(|calling-strategy-name, what, term) = + // FIXME: if has-annotation ... + err-msg(|<concat-strings>["not yet implemented: ", what, " (in strategy ", + calling-strategy-name, ")"]) + ; !term + ; debug + ; <xtc-exit> 51 Index: src/str/eval-meta-code.str --- src/str/eval-meta-code.str (revision 40) +++ src/str/eval-meta-code.str (working copy) @@ -76,7 +76,7 @@ strategies - gen-meta-code(|i, args) = + gen-meta-code(|i, data) = ///*DEBUG*/say(!" ### gen-meta-code starting"); debug; (?MetaFor(meta-var, _, _, _, body) <+ fatal-err-msg(|"ICE!")) ///*DEBUG*/; say(!" >>> gen-meta-code -- start -- current term >>>") Index: src/syn/xrm/XRM-Expression.sdf --- src/syn/xrm/XRM-Expression.sdf (revision 40) +++ src/syn/xrm/XRM-Expression.sdf (working copy) @@ -8,12 +8,21 @@ %% ArrayAccess %% | Expression "<<" Expression %% | Expression ">>" Expression + %% + %% ExpressionFunc ::= + %% (* older builtin functions for backwards compat. *) + %% "rand" "(" Expression {"," Expression} ")" + %% (* builtin functions calls using the "func" notation *) + %% | "func" "(" "rand" "," Expression {"," Expression} ")" context-free syntax ArrayAccess -> Expression Expression ">>" Expression -> Expression {left,cons("RightShift")} Expression "<<" Expression -> Expression {left,cons("LeftShift")} + "rand" "(" {Expression ","}+ ")" -> Expression {cons("Rand")} + "func" "(" "rand" "," {Expression ","}+ ")" -> Expression {cons("Rand")} + context-free priorities { "+" Expression -> Expression Index: src/syn/prism/PRISM-MetaVars.sdf --- src/syn/prism/PRISM-MetaVars.sdf (revision 40) +++ src/syn/prism/PRISM-MetaVars.sdf (working copy) @@ -12,3 +12,4 @@ "m"[0-9]* "*" -> Module+ {prefer} [c][0-9]* -> Command {prefer} "c"[0-9]* "*" -> Command+ {prefer} + [u][0-9]* -> Updates {prefer} Index: src/syn/prism/StrategoPRISM.sdf --- src/syn/prism/StrategoPRISM.sdf (revision 40) +++ src/syn/prism/StrategoPRISM.sdf (working copy) @@ -24,3 +24,4 @@ "~id':" StrategoTerm -> IdentifierPrime {prefer,cons("FromTerm")} "~int:" StrategoTerm -> LInt {prefer,cons("FromTerm")} "~double:" StrategoTerm -> LDouble {prefer,cons("FromTerm")} + "~updates:" StrategoTerm -> Updates {prefer,cons("FromTerm")} Index: tests/xrm/rand.xpm --- tests/xrm/rand.xpm (revision 0) +++ tests/xrm/rand.xpm (revision 0) @@ -0,0 +1,12 @@ + +module rand // NOTE: no conflict here (rand isn't a reserved name) + x : [0..42]; + y : [0..1]; + [] x=0 -> (x'=rand(5)); + [] x=1 -> (y'=1) & (x'=rand(5)); + [] x=2 -> (x'=rand(5)+3); + //[] x=2 -> 0.5:(y'=2) + 0.5:(x'=rand(5)); + [] x=3 -> (x'=rand(3, 9)); + [] x=4 -> 1/5:(x'=0) + 1/5:(x'=1) + 1/5:(x'=2) + + 1/5:(x'=3) + 1/5:(x'=4) + 1/5:(x'=5); +endmodule Index: tests/prism/formula.pm --- tests/prism/formula.pm (revision 0) +++ tests/prism/formula.pm (revision 0) @@ -0,0 +1,6 @@ +formula lfree = p2=0..4,6,10; + +module test + p1 : [0..42] init 0; + [] p1=2 & lfree -> (p1'=4); +endmodule Index: TODO --- TODO (revision 40) +++ TODO (working copy) @@ -128,6 +128,18 @@ [] x=3 -> ... // x=3 is impossible [] x=0 -> (x'=3) // x=3 is not in the definition range of x + ## ------------- ## + ## Documentation ## + ## ------------- ## + + * Document the return values of xrm-front. + - 1: rewriting failed + - 2: error with meta-vars (eg: undefined meta-var, redefined meta-var) + - 3: arithmetic error when evaluating code (eg: division/modulo by 0) + - 4: invalid call to a builtin (eg rand(1,2,3)) + - 42: internal compiler error + - 51: not yet implemented + ## ---- ## ## DONE ## ## ---- ##

17 years, 11 months

XRM 40: Use libxtclib instead of liblib.

by SIGOURE Benoit

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Use libxtclib instead of liblib. See https://bugs.cs.uu.nl/browse/STR-564. Actually we can't use libstratego-xtc at the moment, since it hasn't made it to strc 0.16 and we target this version of the compiler ATM. In the future we shall update the imports as commented in FIXMEs. * src/tools/parse-xrm.str: Import libxtclib instead of liblib. * src/tools/parse-prism.str, * src/tools/pp-xrm.str, * src/tools/pp-prism.str, * src/lib/xrm/pp/xrm-to-abox.str, * src/lib/prism/pp/prism-to-abox.str, * src/str/xrm-front.str: Ditto. * tests/xrm/array_with_static_dim.xpm: New. * tests/xrm/desugar_builtins.pm: Move... * tests/prism/desugar_builtins.pm: Here. * TODO: More things to do... TODO | 9 +++++++++ src/lib/prism/pp/prism-to-abox.str | 2 +- src/lib/xrm/pp/xrm-to-abox.str | 2 +- src/str/xrm-front.str | 3 +-- src/tools/parse-prism.str | 2 +- src/tools/parse-xrm.str | 2 +- src/tools/pp-prism.str | 2 +- src/tools/pp-xrm.str | 2 +- tests/xrm/array_with_static_dim.xpm | 5 +++++ 9 files changed, 21 insertions(+), 8 deletions(-) Index: src/tools/parse-xrm.str --- src/tools/parse-xrm.str (revision 39) +++ src/tools/parse-xrm.str (working copy) @@ -2,7 +2,7 @@ module parse-xrm imports - liblib + libxtclib // FIXME: import libstratego-xtc for strc 0.17 tool-doc parser-common Index: src/tools/parse-prism.str --- src/tools/parse-prism.str (revision 39) +++ src/tools/parse-prism.str (working copy) @@ -2,7 +2,7 @@ module parse-prism imports - liblib + libxtclib // FIXME: import libstratego-xtc for strc 0.17 tool-doc parser-common Index: src/tools/pp-xrm.str --- src/tools/pp-xrm.str (revision 39) +++ src/tools/pp-xrm.str (working copy) @@ -2,7 +2,7 @@ module pp-xrm imports - liblib + libxtclib // FIXME: import libstratego-xtc for strc 0.17 tool-doc strategies Index: src/tools/pp-prism.str --- src/tools/pp-prism.str (revision 39) +++ src/tools/pp-prism.str (working copy) @@ -2,7 +2,7 @@ module pp-prism imports - liblib + libxtclib // FIXME: import libstratego-xtc for strc 0.17 tool-doc strategies Index: src/lib/xrm/pp/xrm-to-abox.str --- src/lib/xrm/pp/xrm-to-abox.str (revision 39) +++ src/lib/xrm/pp/xrm-to-abox.str (working copy) @@ -1,6 +1,6 @@ module xrm-to-abox imports - liblib + libxtclib // FIXME: import libstratego-xtc for strc 0.17 tool-doc Box XRM // signature Index: src/lib/prism/pp/prism-to-abox.str --- src/lib/prism/pp/prism-to-abox.str (revision 39) +++ src/lib/prism/pp/prism-to-abox.str (working copy) @@ -1,6 +1,6 @@ module prism-to-abox imports - liblib + libxtclib // FIXME: import libstratego-xtc for strc 0.17 tool-doc Box PRISM // signature Index: src/str/xrm-front.str --- src/str/xrm-front.str (revision 39) +++ src/str/xrm-front.str (working copy) @@ -1,7 +1,7 @@ module xrm-front imports - liblib + libxtclib // FIXME: import libstratego-xtc for strc 0.17 tool-doc xrm-to-prism prism-desugar @@ -23,7 +23,6 @@ ; xtc-transform(!"parse-xrm", // parse input (returns a FILE) <concat>[ ["-b"], <pass-verbose>(), <pass-add-pos>() ]) ; read-from // read parsed input - ; /*FIXME*/strip-annos // FIXME: remove this line!!!!!!!!!!!!!!!!!!!!!!!!!! ; xrm-front-pipeline // transformations ; if not(must-keep-attributes) then strip-annos end ; if <get-config> "-b" then Index: tests/xrm/array_with_static_dim.xpm --- tests/xrm/array_with_static_dim.xpm (revision 0) +++ tests/xrm/array_with_static_dim.xpm (revision 0) @@ -0,0 +1,5 @@ +const int N = 10; + +module test + s[N] : [0..1]; +endmodule Index: TODO --- TODO (revision 39) +++ TODO (working copy) @@ -48,6 +48,10 @@ declared variables (globals, formulas, local declarations etc.) and ensure (in check-meta-vars) that their identifiers are unique. + * Add a "rand" builtin. Eg: + rand(50) -> random value between 0 and 50 (included) + rand(42, 50) -> random value between 42 and 50 (included) + * Add a sanity check after xrm-front has finished to generate everything in order to ensure that each module/var decl has a unique name. @@ -94,6 +98,11 @@ x[3] : [0..4] init {0, 1, 2}; const int array[3] = {0, 1, 2}; + * Add a possibility to import another module, eg: import common.pm + A module can be imported only once. + + * Add parameterized formulas. (Pretty much like macro-functions in C) + ## -------------- ## ## Desugarisation ## ## -------------- ##

17 years, 11 months

XRM 39: Remove debugging messages from prism-desugar.

by SIGOURE Benoit

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Remove debugging messages from prism-desugar. * src/str/prism-desugar.str: Remove debugging stuff. * tests/prism/range-desugar.pm: New. src/str/prism-desugar.str | 119 +++++++++++++++++++++++++++++++++++-------- tests/prism/range-desugar.pm | 13 ++++ 2 files changed, 112 insertions(+), 20 deletions(-) Index: src/str/prism-desugar.str --- src/str/prism-desugar.str (revision 38) +++ src/str/prism-desugar.str (working copy) @@ -21,7 +21,7 @@ RemoveUnconditionnalUpdates <+ AddZero <+ MulOne <+ MulZero <+ DivOne <+ catch-div-by-zero <+ EvalPlus <+ EvalMinus <+ EvalMul <+ EvalDiv - <+ EvalLt <+ EvalLtEq <+ EvalGt <+ EvalGtEq <+ EvalEq <+ EvalNeq + <+ EvalLt <+ EvalLtEq <+ EvalGt <+ EvalGtEq <+ EvalEq <+ EvalNotEq <+ EvalAnd <+ EvalOr <+ EvalMin <+ EvalMax <+ EvalFloor <+ EvalCeil <+ EvalPow <+ EvalMod ) @@ -101,6 +101,15 @@ ** the end of an integer literal make it a Double() and not an Int() [This ** is one of the minor extensions of XRM] */ + +/* +** ## ======== ## +** ## Simplify ## +** ## ======== ## +** +** Simplify arithmetic operations. +*/ + rules AddZero: @@ -121,6 +130,12 @@ DivOne: |[ e / 1D ]| -> |[ e ]| +/* +** ## ==================== ## +** ## Constant propagation ## +** ## ==================== ## +*/ + rules EvalPlus: @@ -147,46 +162,102 @@ EvalGtEq: |[ d1 >= d2 ]| -> <compare(geqR)>(d1, d2) +/* +** ## ============== ## +** ## Equality tests ## +** ## ============== ## +** +** - Eval constant equality tests (eg: 1=3 -> false) +** - Desugar complex equality tests +** eg: x=1..5,7,10..13 -> (x>=1 & x<=5) | (x=7) | (x>=10 & x<=13) +** This part is a bit complex since we need to handle several cases in +** different ways. +*/ + +strategies + + /** Simple constant equality tests */ EvalSimpleEq: |[ d1 = d2 ]| -> res - where say(!"@@@ EvalSimpleEq");debug - ; <compare(real-eq)>(d1, d2) => res;debug + where <compare(real-eq)>(d1, d2) => res + /** Simple equality tests with a range (eg: x=[1..5]) */ EvalSimpleRangeEq: |[ e = e1..e2 ]| -> res - where say(!"@@@ EvalSimpleRangeEq range");debug - ; <DesugarRangeEq(|e)>(Range(e1, e2)) => res;debug + where <DesugarRangeEq(|e)>(Range(e1, e2)) => res + /** Complex equality tests (something not in the form of x=exp) */ EvalComplexEq: Eq(e, a*) -> res - where say(!"@@@ EvalComplexEq");<debug>a* - ; !a* - ; map(DesugarRangeEq(|e) <+ \ e2 -> |[ e=e2 ]| \);debug + where !a* + ; map(DesugarRangeEq(|e) <+ \ e2 -> |[ e=e2 ]| \) ; foldr(!False(), \ (x, y) -> Or(x, y) \) => res - ; say(!" end of EvalComplexEq:");debug strategies - EvalEq = ?a;?Eq(_,_);say(!"@@@ EvalEq starting:");debug;rules(Hello: a); - (?Eq(_, [Eq(_, _)]) <+ EvalSimpleEq <+ EvalSimpleRangeEq <+ (?|[ e = e2 ]| < debug;fail + EvalComplexEq)) + /** Eval/desugar an equality test. + ** 1. Try to see whether it's a simple constant equality test in which + ** case it can be evaluated right away. + ** 2. Try to see whether it's a simple equality test with a range, in + ** which case it can be desugared (and maybe latter evaluated by + ** another pass) + ** 3. a) If 1/ and 2/ failed, and if we have an equality test of the + ** form x = exp, we can't desugar/evaluate it further, so give up. + ** b) If 1/ and 2/ failed but we're not on a simple equality test, + ** try to desugar it further since it's a complex equality test. + */ + EvalEq = + EvalSimpleEq + <+ EvalSimpleRangeEq + <+ (?|[ e = e2 ]| < fail + EvalComplexEq) rules + DesugarRangeEq(|e): + Range(e2, e3) -> |[ e >= e2 & e <= e3]| + +/* +** ## ================= ## +** ## "Not equal" tests ## +** ## ================= ## +** +** Everything works in the exact same way as the above for equality tests. +*/ + +strategies + + EvalSimpleNotEq: + |[ d1 != d2 ]| -> res + where <compare(not(real-eq))>(d1, d2) => res + + EvalSimpleRangeNotEq: + |[ e != e1..e2 ]| -> res + where <DesugarRangeNotEq(|e)>(Range(e1, e2)) => res - //EvalNeq: - // |[ d1 != d2 ]| -> <compare(not(real-eq))>(d1, d2) - EvalNeq: + EvalComplexNotEq: 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 + where !a* + ; map(DesugarRangeNotEq(|e) <+ \ e2 -> |[ e!=e2 ]| \) + ; foldr(!False(), \ (x, y) -> Or(x, y) \) => res - DesugarRangeEq(|e): - Range(e2, e3) -> |[ e >= e2 & e <= e3]| +strategies - DesugarRangeNeq(|e): + EvalNotEq = + EvalSimpleNotEq + <+ EvalSimpleRangeNotEq + <+ (?|[ e != e2 ]| < fail + EvalComplexNotEq) + +rules + + DesugarRangeNotEq(|e): Range(e2, e3) -> |[ e < e2 & e > e3]| +/* +** ## ================= ## +** ## Logical operators ## +** ## ================= ## +*/ + rules EvalAnd: @@ -211,6 +282,14 @@ EvalOr: |[ false | e ]| -> |[ e ]| +/* +** ## ============= ## +** ## Eval Builtins ## +** ## ============= ## +** +** Try to evaluate builtin calls. +*/ + rules EvalMin: Index: tests/prism/range-desugar.pm --- tests/prism/range-desugar.pm (revision 0) +++ tests/prism/range-desugar.pm (revision 0) @@ -0,0 +1,13 @@ +module range + x : [0..42] init 0; + + [] 10=1,10 -> true; + [] 10=1..10 -> true; + [] 10=1,2..11 -> true; + [] 10=1,2..11,12 -> true; + + [] x=1,10 -> true; + [] x=1..10 -> true; + [] x=1,2..11 -> true; + [] x=1,2..11,12 -> true; +endmodule

17 years, 11 months

XRM 38: Add support for ranges in constant propagation.

by SIGOURE Benoit

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> 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)

17 years, 11 months

XRM 37: Add formulas in constant propagation.

by SIGOURE Benoit

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Add formulas in constant propagation. * src/str/xrm-to-prism.str: Fix the traversals collecting static * const decls and add formulas collections. Update comments. * src/str/prism-desugar.str: Expand formulas. * tests/xrm/static-const-arrays-desugar.xpm: New. * TODO: Update. New idea: array initializations a la C :). TODO | 18 +++++++++++------- src/str/prism-desugar.str | 20 +++++++++++++------- src/str/xrm-to-prism.str | 26 ++++++++++++++++++++------ tests/xrm/static-const-arrays-desugar.xpm | 26 ++++++++++++++++++++++++++ 4 files changed, 70 insertions(+), 20 deletions(-) Index: src/str/xrm-to-prism.str --- src/str/xrm-to-prism.str (revision 36) +++ src/str/xrm-to-prism.str (working copy) @@ -14,6 +14,9 @@ ** with a value and an annotated type. Only constants with a static value ** provided will be put here (constants can have their value defined in ** init blocks and chosen at random at runtime). +** - ExpandFormulas: created by the strategy collect-formulas and used by +** prism-desugar for constant propagation. Maps an identifier with an +** expression. */ module xrm-to-prism imports @@ -30,15 +33,19 @@ /* remove XRM sugar, normalize some nodes */ innermost(xrm-to-prism-desugar) - /* Two things in one traversal: - * 1/ Desugar array declarations + /* Collect static const variables + * Two goals: expand them if needed, look for variable name conflicts. */ + ; topdown(try(collect-static-const-decl); try(collect-formulas)) + + /* Desugar array declarations * eg: x[4][5] is transformed into two nested meta for loops * We can't do this in xrm-to-prism-desugar because the innermost - * traversal is bottomup and won't recurse into generated code - * 2/ Collect static const variables - * Two goals: expand them if needed, look for variable name conflicts. + * traversal is bottomup and won't recurse into generated code. + * + * This must come AFTER collect-static-const-decl since we might need + * to expand an array which relies on static const variables. */ - ; topdown(try(array-decl-desugar); try(collect-static-const-decl)) + ; topdown(try(array-decl-desugar)) /* Check that meta vars are always defined in the current scope when used * and that they are not redefined twice in the same scope */ @@ -95,6 +102,13 @@ ; where(!value{Type("bool")} => v) ; rules(ExpandStaticConsts: idf -> v) +rules + + collect-formulas = + //?|[ formula x = e; ]| + ?FormulaDef(x, e) + ; rules(ExpandFormulas: x -> e) + strategies /** Index: src/str/prism-desugar.str --- src/str/prism-desugar.str (revision 36) +++ src/str/prism-desugar.str (working copy) @@ -29,19 +29,25 @@ /** ** Main goal: Transform all Int(_) -> Double(_) - ** In this first pass we also want to expand static consts. However, we - ** must be careful as to where these expansions occur. For instance, say - ** that N=10 (we know it thanks to the DR ExpandStaticConsts). If we are - ** on the node where N is declared (that is: |[ const int N = 10; ]|) we - ** should NOT expand `N' here. Otherwise we'll end up with - ** |[ const int 10 = 10; ]|. + ** + ** In this first pass we also want to expand static consts and formulas. + ** However, we must be careful as to where these expansions occur. For + ** instance, say that N=10 (we know it thanks to the DR ExpandStaticConsts). + ** + ** If we are on the node where N is declared (that is: + ** |[ const int N = 10; ]|) we should NOT expand `N' here. Otherwise + ** we'll end up with |[ const int 10 = 10; ]|. The same thing applies for + ** formulas and ExpandFormulas. */ prism-desugar-first-pass = ConstInt(id, prism-desugar) <+ ConstDouble(id, prism-desugar) <+ ConstBool(id, prism-desugar) + <+ FormulaDef(id, prism-desugar) <+ ?Int(_); IntToDouble - <+ all(try(ExpandStaticConsts); prism-desugar-first-pass) + <+ all(try(ExpandStaticConsts) + ; try(ExpandFormulas) + ; prism-desugar-first-pass) rules Index: tests/xrm/static-const-arrays-desugar.xpm --- tests/xrm/static-const-arrays-desugar.xpm (revision 0) +++ tests/xrm/static-const-arrays-desugar.xpm (revision 0) @@ -0,0 +1,26 @@ +const int N = 3; +const int array[N] = 42; + +module test + x[N] : [0..N] init array[N]; + + [] x[array[N]]=0 -> (x[array[N]]'=1); +endmodule + +// The above code will generate the following code once +// collect-static-const-decl and array-decl-desugar have runned. +// The problem is that the loop "hides" static const variables which +// are not caught by collect-static-const-decl. + +// const int N = 3; +// +// for __meta_i_0 from 0 to 2 step 1 do +// const int array[__meta_i_0] = 42; +// end +// +// module test +// for __meta_i_2 from 0 to 2 step 1 do +// x[__meta_i_2] : [0..N] init array[N]; +// end +// [] x[array[N]]=0 -> (x[array[N]]'=1); +// endmodule Index: TODO --- TODO (revision 36) +++ TODO (working copy) @@ -37,9 +37,8 @@ * Add the following at the meta-level: - Let's have the possibility to generate other ModulesFileSection such as: - o Formula // add it in the grammar. should be - // automagically handled - o Constant // ditto + o Formula // done (automagically handled) + o Constant // done (automagically handled) o Global // done (automagically handled) o RenamedModule // need to be investigated o RewardStruct // ditto @@ -48,10 +47,6 @@ * Add a sanity check before check-meta-vars to collect all statically declared variables (globals, formulas, local declarations etc.) and ensure (in check-meta-vars) that their identifiers are unique. - Keep the (static) constant globals somewhere in order to allow - 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) * Add a sanity check after xrm-front has finished to generate everything in order to ensure that each module/var decl has a unique name. @@ -95,6 +90,10 @@ variables and their type + domain and might be quite challenging to handle. + * Add array initializations a la C: + x[3] : [0..4] init {0, 1, 2}; + const int array[3] = {0, 1, 2}; + ## -------------- ## ## Desugarisation ## ## -------------- ## @@ -171,3 +170,8 @@ * Evaluate constant calls to built-in functions, eg func(min, 4, 5) ==> 4 + + * Keep the (static) constant globals somewhere in order to allow + 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)

17 years, 11 months

XRM 36: Add static const arrays.

by SIGOURE Benoit

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Add static const arrays. * src/str/array-decl-desugar.str: Add static const arrays. * src/syn/xrm/XRM-Formula.sdf: New. * src/syn/xrm/XRM-Constant.sdf: New. * src/syn/xrm/XRM-Main.sdf: Import XRM-Formula and XRM-Constant. * src/syn/xrm/Makefile.am: Update $(SDFS) and $(EXTRA_DIST) * src/syn/prism/Makefile.am: Ditto. * tests/xrm/consts.xpm: New. * tests/test-parse-xrm.sh.in: Add missing line. * TODO: Bring up to date. TODO | 11 ++++++-- src/str/array-decl-desugar.str | 50 +++++++++++++++++++++++++++++++++++++ src/syn/prism/Makefile.am | 14 ++++++---- src/syn/xrm/Makefile.am | 25 ++++++++++++++---- src/syn/xrm/XRM-Constant.sdf | 55 +++++++++++++++++++++++++++++++++++++++++ src/syn/xrm/XRM-Formula.sdf | 10 +++++++ src/syn/xrm/XRM-Main.sdf | 2 + tests/test-parse-xrm.sh.in | 1 tests/xrm/consts.xpm | 10 +++++++ 9 files changed, 166 insertions(+), 12 deletions(-) Index: src/str/array-decl-desugar.str --- src/str/array-decl-desugar.str (revision 35) +++ src/str/array-decl-desugar.str (working copy) @@ -76,6 +76,8 @@ [ IntDec(ArrayAccess(idf, dims'), low, up, value) ]) where update-dimensions(|dims) => (x, current-dim', dims') + + array-decl-desugar: BoolDecNoInit(ArrayAccess(idf, dims)) //-> |[ for x from 0 to ~dim step 1 do x[i] : bool; end ]| @@ -89,3 +91,51 @@ -> MetaFor(Identifier(x), Int("0"), current-dim', Int("1"), [ BoolDec(ArrayAccess(idf, dims'), value) ]) where update-dimensions(|dims) => (x, current-dim', dims') + + + + array-decl-desugar: + ConstInt(ArrayAccess(idf, dims), value) + //-> |[ for x from 0 to ~dim step 1 do const int x[i] = ~value; end ]| + -> MetaFor(Identifier(x), Int("0"), current-dim', Int("1"), + [ ConstInt(ArrayAccess(idf, dims'), value) ]) + where update-dimensions(|dims) => (x, current-dim', dims') + + array-decl-desugar: + ConstIntNoInit(ArrayAccess(idf, dims)) + //-> |[ for x from 0 to ~dim step 1 do const int x[i]; end ]| + -> MetaFor(Identifier(x), Int("0"), current-dim', Int("1"), + [ ConstIntNoInit(ArrayAccess(idf, dims')) ]) + where update-dimensions(|dims) => (x, current-dim', dims') + + + + array-decl-desugar: + ConstDouble(ArrayAccess(idf, dims), value) + //-> |[ for x from 0 to ~dim step 1 do const double x[i] = ~value; end ]| + -> MetaFor(Identifier(x), Int("0"), current-dim', Int("1"), + [ ConstDouble(ArrayAccess(idf, dims'), value) ]) + where update-dimensions(|dims) => (x, current-dim', dims') + + array-decl-desugar: + ConstDoubleNoInit(ArrayAccess(idf, dims)) + //-> |[ for x from 0 to ~dim step 1 do const double x[i]; end ]| + -> MetaFor(Identifier(x), Int("0"), current-dim', Int("1"), + [ ConstDoubleNoInit(ArrayAccess(idf, dims')) ]) + where update-dimensions(|dims) => (x, current-dim', dims') + + + + array-decl-desugar: + ConstBool(ArrayAccess(idf, dims), value) + //-> |[ for x from 0 to ~dim step 1 do const bool x[i] = ~value; end ]| + -> MetaFor(Identifier(x), Int("0"), current-dim', Int("1"), + [ ConstBool(ArrayAccess(idf, dims'), value) ]) + where update-dimensions(|dims) => (x, current-dim', dims') + + array-decl-desugar: + ConstBoolNoInit(ArrayAccess(idf, dims)) + //-> |[ for x from 0 to ~dim step 1 do const bool x[i]; end ]| + -> MetaFor(Identifier(x), Int("0"), current-dim', Int("1"), + [ ConstBoolNoInit(ArrayAccess(idf, dims')) ]) + where update-dimensions(|dims) => (x, current-dim', dims') Index: src/syn/xrm/XRM-Formula.sdf --- src/syn/xrm/XRM-Formula.sdf (revision 0) +++ src/syn/xrm/XRM-Formula.sdf (revision 0) @@ -0,0 +1,10 @@ +module XRM-Formula +imports PRISM-to-XRM +exports + + %% EBNF Grammar: Extended Formulas + %% FormulaDef ::= "formula" ArrayAccess "=" Expression ";" + + context-free syntax + "formula" ArrayAccess "=" Expression ";" + -> FormulaDef {cons("FormulaDef")} Index: src/syn/xrm/XRM-Main.sdf --- src/syn/xrm/XRM-Main.sdf (revision 35) +++ src/syn/xrm/XRM-Main.sdf (working copy) @@ -9,3 +9,5 @@ XRM-Declaration XRM-Update XRM-Command + XRM-Formula + XRM-Constant Index: src/syn/xrm/XRM-Constant.sdf --- src/syn/xrm/XRM-Constant.sdf (revision 0) +++ src/syn/xrm/XRM-Constant.sdf (revision 0) @@ -0,0 +1,55 @@ +module XRM-Constant +imports PRISM-to-XRM +exports + + %% EBNF Grammar: Extended Constants + %% ConstantDef ::= "const" "int" ArrayAccess ["=" Expression] ";" + %% | "const" "double" ArrayAccess ["=" Expression] ";" + %% | "const" "bool" ArrayAccess ["=" Expression] ";" + %% + %% (* old style constant defs for backwards compat *) + %% (* no type explicitly given => integers *) + %% | "const" ArrayAccess ["=" Expression] ";" + %% (* doubles *) + %% | "rate" ArrayAccess ["=" Expression] ";" + %% | "prob" ArrayAccess ["=" Expression] ";" + + %% FIXME: This might not be the most efficiant way of using although it + %% should work thanks to the SGLR parser. + + context-free syntax + "const" "int" ArrayAccess "=" Expression ";" + -> ConstantDef {cons("ConstInt")} + + "const" ArrayAccess "=" Expression ";" + -> ConstantDef {cons("ConstInt")} + + + + "const" "int" ArrayAccess ";" -> ConstantDef {cons("ConstIntNoInit")} + "const" ArrayAccess ";" -> ConstantDef {cons("ConstIntNoInit")} + + + + "const" "double" ArrayAccess "=" Expression ";" + -> ConstantDef {cons("ConstDouble")} + + "rate" ArrayAccess "=" Expression ";" + -> ConstantDef {cons("ConstDouble")} + + "prob" ArrayAccess "=" Expression ";" + -> ConstantDef {cons("ConstDouble")} + + + + "const" "double" ArrayAccess ";" -> ConstantDef {cons("ConstDoubleNoInit")} + "rate" ArrayAccess ";" -> ConstantDef {cons("ConstDoubleNoInit")} + "probe" ArrayAccess ";" -> ConstantDef {cons("ConstDoubleNoInit")} + + + + "const" "bool" ArrayAccess "=" Expression ";" + -> ConstantDef {cons("ConstBool")} + + "const" "bool" ArrayAccess ";" + -> ConstantDef {cons("ConstBoolNoInit")} Index: src/syn/xrm/Makefile.am --- src/syn/xrm/Makefile.am (revision 35) +++ src/syn/xrm/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Thu Apr 27 17:40:41 2006 SIGOURE Benoit -## Last update Thu May 25 17:28:59 2006 SIGOURE Benoit +## Last update Fri May 26 02:12:42 2006 SIGOURE Benoit ## include $(top_srcdir)/config/Transformers.mk @@ -41,12 +41,27 @@ XRM-StartSymbols.def \ XRM-Prefixed.def -SDFS = XRM-Expression.sdf \ +SDFS = \ + PRISM-to-XRM.sdf \ + StrategoXRM.sdf \ + XRM-Arrays.sdf \ + XRM-Command.sdf \ + XRM-Constant.sdf \ + XRM-Declaration.sdf \ + XRM-Expression.sdf \ + XRM-Formula.sdf \ + XRM-Literals.sdf \ XRM-Main.sdf \ - XRM.sdf \ - XRM-StartSymbols.sdf + XRM-MetaCongruences.sdf \ + XRM-MetaFor.sdf \ + XRM-MetaIf.sdf \ + XRM-MetaVars.sdf \ + XRM-Module.sdf \ + XRM-StartSymbols.sdf \ + XRM-Update.sdf \ + XRM.sdf -EXTRA_DIST = $(wildcard *.sdf) +EXTRA_DIST = $(SDFS) XRM.def: $(SDFS) XRM-StartSymbols.def: $(SDFS) Index: src/syn/prism/Makefile.am --- src/syn/prism/Makefile.am (revision 35) +++ src/syn/prism/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Thu Apr 27 17:40:41 2006 SIGOURE Benoit -## Last update Thu May 25 17:28:59 2006 SIGOURE Benoit +## Last update Fri May 26 02:12:29 2006 SIGOURE Benoit ## include $(top_srcdir)/config/Transformers.mk @@ -39,7 +39,8 @@ PRISM-StartSymbols.def \ PRISM-Prefixed.def -SDFS = PRISM-Command.sdf \ +SDFS = \ + PRISM-Command.sdf \ PRISM-Constant.sdf \ PRISM-Declaration.sdf \ PRISM-Expression.sdf \ @@ -51,17 +52,20 @@ PRISM-Label.sdf \ PRISM-Layout.sdf \ PRISM-Literals.sdf \ + PRISM-Main.sdf \ + PRISM-MetaCongruences.sdf \ + PRISM-MetaVars.sdf \ PRISM-Module.sdf \ PRISM-ModulesFile.sdf \ PRISM-ModulesFileType.sdf \ PRISM-Reward.sdf \ + PRISM-StartSymbols.sdf \ PRISM-SystemComposition.sdf \ PRISM-Update.sdf \ - PRISM-Main.sdf \ PRISM.sdf \ - PRISM-StartSymbols.sdf + StrategoPRISM.sdf -EXTRA_DIST = $(wildcard *.sdf) +EXTRA_DIST = $(SDFS) PRISM.def: $(SDFS) PRISM-StartSymbols.def: $(SDFS) Index: tests/xrm/consts.xpm --- tests/xrm/consts.xpm (revision 0) +++ tests/xrm/consts.xpm (revision 0) @@ -0,0 +1,10 @@ +for i from 0 to 4 do + const int x[i] = 2*i; +end + +const int y[5]; +const z[5] = 42; +const double d[3] = 3.14; +rate c[4] = 42 > 3.14; +probe d[4]; +const bool b[3] = true; Index: tests/test-parse-xrm.sh.in --- tests/test-parse-xrm.sh.in (revision 35) +++ tests/test-parse-xrm.sh.in (working copy) @@ -16,6 +16,7 @@ for file in `find "@srcdir@" -name '*.pm' -o -name '*.nm' -o -name '*.sm' -o -name '*.xpm' | sort`; do echo @ECHO_N@ " Parsing `basename $file` ... " "@top_builddir@/src/tools/parse-xrm" -i "$file" -o /dev/null + rv=$? if [ $? -eq 0 ]; then echo 'OK, no ambiguities found' test_pass=$((test_pass + 1)) Index: TODO --- TODO (revision 35) +++ TODO (working copy) @@ -4,6 +4,9 @@ ## Misc. ## ## ----- ## + * Check why make distcheck fails because of autom4te.cache ?! + ./configure && make # runs configure twice!?? (probably related) + * PRISM's parser has a ForLoop node: Identifier "=" Expression ":" Expression [":" Expression] What the hell is this? @@ -22,6 +25,12 @@ const int y = x; Is it even possible to define a static const variable from another one? + * Improve the error messages using locations provided by addPosInfo when + they are available (xrm-front invoked with --add-pos|-P). + Some cases are very hard to handle for example array[N] where N is + static const int N = -1; will issue an error such as "undeclared meta + variable N" whereas the real problem is that array[N] couldn't be expanded. + ## ---------- ## ## Extensions ## ## ---------- ## @@ -62,8 +71,6 @@ x[1..3]?=0 => x_1=0 | x_2=0 | x_3=0 NOTE: x[5]?=0 should be considered as an error. - NOTE: arrays should behave like in C (array[N] is ranging from 0 to N-1) - I'm not sure it's really always handled this way ATM :/ * Add non-static array accesses (as suggested by Micha). For instance: module test

17 years, 11 months

XRM 35: Fix the size of generated arrays.

by SIGOURE Benoit

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Fix the size of generated arrays. * src/str/array-decl-desugar.str: Stick with the C-style array convention. (that is: array[N] has values ranging from array[0] to array[N-1]) array-decl-desugar.str | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) Index: src/str/array-decl-desugar.str --- src/str/array-decl-desugar.str (revision 34) +++ src/str/array-decl-desugar.str (working copy) @@ -45,13 +45,17 @@ /* find the first element in the list which matches ?Int(_) * eg: [Identifier("..."), Int("1"), Int("2")] will be transformed in * ([Identifier("...")], Int("1"), [Int("2")]) */ - ; <split-fetch-keep(?Int(_))> dims' => (dims-done, current-dim, dims-todo) + ; <split-fetch-keep(?Int(_))> dims' + => (dims-done, Int(current-dim), dims-todo) + + /* array[N] has N elements ranging from 0 to N-1 */ + ; <subtS>(current-dim, "1") => current-dim' /* replace the dimension we're working on by the meta-var */ ; <concat> [dims-done, [Identifier(x)], dims-todo] /* return the result in a tuple */ - ; !(x, current-dim, <id>) + ; !(x, Int(current-dim'), <id>) rules // FIXME: Try to figure out why concrete syntax fails to work here

17 years, 11 months

XRM 34: Use static const variables in constant propagation.

by SIGOURE Benoit

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Use static const variables in constant propagation. * src/sig/Makefile.am: Patch a possible dependency problem. * src/str/xrm-front.str: Change some comments. * src/str/xrm-to-prism.str: Collect static const variables. * src/str/prism-desugar.str: Use the known values of static const variables in constant propagation if possible. * TODO: Update things done. Add a question about PRISM's behavior. TODO | 13 +++++++++---- src/sig/Makefile.am | 8 +++++--- src/str/prism-desugar.str | 21 +++++++++++++++++++-- src/str/xrm-front.str | 6 +++--- src/str/xrm-to-prism.str | 45 +++++++++++++++++++++++++++++++++++++++++---- 5 files changed, 77 insertions(+), 16 deletions(-) Index: src/sig/Makefile.am --- src/sig/Makefile.am (revision 33) +++ src/sig/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Mon May 8 18:38:32 2006 SIGOURE Benoit -## Last update Tue May 9 20:39:39 2006 SIGOURE Benoit +## Last update Thu May 25 23:41:55 2006 SIGOURE Benoit ## include $(top_srcdir)/config/Transformers.mk @@ -18,8 +18,10 @@ SDF2RTG_FLAGS = --main $* -PRISM.def: +PRISM.def: $(top_builddir)/src/syn/prism/PRISM.def + rm -f $@ $(LN_S) $(top_builddir)/src/syn/prism/$@ $@ -XRM.def: +XRM.def: $(top_builddir)/src/syn/xrm/XRM.def + rm -f $@ $(LN_S) $(top_builddir)/src/syn/xrm/$@ $@ Index: src/str/xrm-front.str --- src/str/xrm-front.str (revision 33) +++ src/str/xrm-front.str (working copy) @@ -36,7 +36,7 @@ end end - // pipeline of transformations performed by xrm-front + /** pipeline of transformations performed by xrm-front */ xrm-front-pipeline = dbg(|"xrm-front-pipeline starting") ; xrm-to-prism @@ -47,14 +47,14 @@ end ; id // FIXME: add more transformations here - // list of available options for xrm-front + /** list of available options for xrm-front */ xrm-front-options = pp-aterm-option + add-pos-option + keep-attributes-option + desugar-option - // check the options are consistent + /** checks the options are consistent */ check-options = if <get-config> "-b" then // if we're asked for binary output, don't bother with pretty printing Index: src/str/xrm-to-prism.str --- src/str/xrm-to-prism.str (revision 33) +++ src/str/xrm-to-prism.str (working copy) @@ -1,6 +1,19 @@ /* ** This sub-module does the real work of the front-end. It transforms the ** program into a valid PRISM AST. +** +** Dynamic rules inventory: +** - DeclarationList: used by the strategy reorder-module-contents to +** store all the declarations within a given module. This way declarations +** can be grouped together in the module (as required by the PRISM grammar) +** - CommandList: used by the strategy reorder-module-contents to +** store all the commands within a given module. This way commands can +** be grouped together in the module (as required by the PRISM grammar) +** - ExpandStaticConsts: created by the strategy collect-static-const-decl +** and used by prism-desugar for constant propagation. Maps an identifier +** with a value and an annotated type. Only constants with a static value +** provided will be put here (constants can have their value defined in +** init blocks and chosen at random at runtime). */ module xrm-to-prism imports @@ -17,11 +30,15 @@ /* remove XRM sugar, normalize some nodes */ innermost(xrm-to-prism-desugar) - /* Desugar array declarations + /* Two things in one traversal: + * 1/ Desugar array declarations * eg: x[4][5] is transformed into two nested meta for loops * We can't do this in xrm-to-prism-desugar because the innermost - * traversal is bottomup and won't recurse into generated code */ - ; topdown(try(array-decl-desugar)) + * traversal is bottomup and won't recurse into generated code + * 2/ Collect static const variables + * Two goals: expand them if needed, look for variable name conflicts. + */ + ; topdown(try(array-decl-desugar); try(collect-static-const-decl)) /* Check that meta vars are always defined in the current scope when used * and that they are not redefined twice in the same scope */ @@ -48,7 +65,7 @@ xrm-to-prism-desugar: |[ e1 << e2 ]| -> |[ e1 * func(pow, 2, e2) ]| - // if the step is not specified, it is implicitely set to 1 + /** if the step is not specified, it is implicitly set to 1 */ xrm-to-prism-desugar: MetaFor(identifier, from, to, body) -> MetaFor(identifier, from, to, Int("1"), body) @@ -58,6 +75,26 @@ //|[ if e then s* end ]| -> |[ if e then s* else end ]| MetaIf(e, m*) -> MetaIf(e, m*, []) +signature constructors + Type : String -> Type + +strategies + + collect-static-const-decl = + ?ConstInt(idf, value) + ; where(!value{Type("int")} => v) + ; rules(ExpandStaticConsts: idf -> v) + + collect-static-const-decl = + ?ConstDouble(idf, value) + ; where(!value{Type("double")} => v) + ; rules(ExpandStaticConsts: idf -> v) + + collect-static-const-decl = + ?ConstBool(idf, value) + ; where(!value{Type("bool")} => v) + ; rules(ExpandStaticConsts: idf -> v) + strategies /** Index: src/str/prism-desugar.str --- src/str/prism-desugar.str (revision 33) +++ src/str/prism-desugar.str (working copy) @@ -9,13 +9,14 @@ ** 1. First convert all literal ints to doubles. This makes the ** simplifications easier to write since there is less cases to ** address (eg: int + int, int + double, double + int, - ** double + double etc.). + ** double + double etc.). This first pass works in a slightly + ** special way, see prism-desugar-first-pass for more info. ** 2. Desugar the AST ** 3. Convert the doubles which are round numbers back to ints. ** Simplify doubles (round them up and remove trailing zeros) */ prism-desugar = - topdown(try(IntToDouble)) + prism-desugar-first-pass ; innermost( RemoveUnconditionnalUpdates <+ AddZero <+ MulOne <+ MulZero <+ DivOne <+ catch-div-by-zero @@ -26,6 +27,22 @@ ) ; topdown(try(SimplifyDoubles <+ TruncateDouble)) + /** + ** Main goal: Transform all Int(_) -> Double(_) + ** In this first pass we also want to expand static consts. However, we + ** must be careful as to where these expansions occur. For instance, say + ** that N=10 (we know it thanks to the DR ExpandStaticConsts). If we are + ** on the node where N is declared (that is: |[ const int N = 10; ]|) we + ** should NOT expand `N' here. Otherwise we'll end up with + ** |[ const int 10 = 10; ]|. + */ + prism-desugar-first-pass = + ConstInt(id, prism-desugar) + <+ ConstDouble(id, prism-desugar) + <+ ConstBool(id, prism-desugar) + <+ ?Int(_); IntToDouble + <+ all(try(ExpandStaticConsts); prism-desugar-first-pass) + rules IntToDouble: Int(i) -> Double(i) Index: TODO --- TODO (revision 33) +++ TODO (working copy) @@ -17,6 +17,11 @@ * Add more tests. Add tests which actually do check that the generated code is correct (which is not done ATM). + * How are handled mutually recursive static constant variables in PRISM? + eg: const int x = y; + const int y = x; + Is it even possible to define a static const variable from another one? + ## ---------- ## ## Extensions ## ## ---------- ## @@ -91,10 +96,6 @@ x = 1..5,7,10..13 ==> (x>=1 & x<=5) | (x=7) | (x>=10 & x<=13) - * Evaluate constant calls to built-in functions, eg - func(min, 4, 5) - ==> 4 - * Expand formulas, eg formula lfree = p2=0..4,6,10; // ... @@ -159,3 +160,7 @@ [] x[0]=0 -> ... => ... <=> end endmodule => [] x_0=0 -> ... <=> [] x_0=0 -> ... => endmodule <=> endmodule + + * Evaluate constant calls to built-in functions, eg + func(min, 4, 5) + ==> 4

17 years, 11 months

XRM 33: Add constant propagation for builtins.

by SIGOURE Benoit

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Add constant propagation for builtins. Some C code was needed to implement easily and efficiently some operations on reals. The --pp-prism|-P option of xrm-front was removed and replaced by --add-pos|-P. The reason for this is that xrm-front takes PRISM code as input and was producing PRISM AST as output, which is a bit inconsistent. So the default is now to produce PRISM source code. addPosInfo is now only invoked with --add-pos|-P because it is very inefficient and introduces a big memory/time penalty. On big inputs it will even get killed by the system. * src/lib/xrm/Makefile.am: Remove useless include. * src/lib/Makefile.am: Ditto. * src/lib/prism/Makefile.am: Ditto. * src/syn/Makefile.am: Ditto. * src/lib/native: New. * src/lib/native/floor.c: New. * src/lib/native/libstr-reals.h: New. * src/lib/native/Makefile.am: New. * src/lib/native/ceil.c: New. * src/lib/native/power.c: New. * src/str/xrm-front.str: Change the -P option to be --add-pos. * src/str/Makefile.am: Use libstr-reals. * src/str/prism-desugar.str: Add builtins desugarisation. * src/str/reals.str: Add more new strategies using libstr-reals. * src/syn/prism/PRISM-MetaVars.sdf: Update the meta-var `a*'. * src/Makefile.am: Build the `lib' subdir before `str'. * tests/test-pp-prism.sh.in: Save the reason of the failing tests. * tests/test-xrm-front.sh.in: Ditto. * tests/test-parse-xrm.sh.in: Ditto. * tests/test-parse-prism.sh.in: Ditto. * tests/test-pp-xrm.sh.in: Ditto. * tests/xrm/desugar_builtins.pm: New. * configure.ac: Add src/lib/native/Makefile's generation. * bootstrap (svn:executable): Mark as executable. configure.ac | 3 +- src/Makefile.am | 4 +- src/lib/Makefile.am | 6 +--- src/lib/native/Makefile.am | 30 +++++++++++++++++++++ src/lib/native/ceil.c | 23 ++++++++++++++++ src/lib/native/floor.c | 22 +++++++++++++++ src/lib/native/libstr-reals.h | 41 +++++++++++++++++++++++++++++ src/lib/native/power.c | 37 ++++++++++++++++++++++++++ src/lib/prism/Makefile.am | 4 -- src/lib/xrm/Makefile.am | 4 -- src/str/Makefile.am | 9 ++++-- src/str/prism-desugar.str | 39 ++++++++++++++++++++++++++++ src/str/reals.str | 52 ++++++++++++++++++++++++++++++++++++- src/str/xrm-front.str | 54 ++++++++++++++++----------------------- src/syn/Makefile.am | 4 -- src/syn/prism/PRISM-MetaVars.sdf | 2 - tests/test-parse-prism.sh.in | 9 +++++- tests/test-parse-xrm.sh.in | 6 ++++ tests/test-pp-prism.sh.in | 12 +++++++- tests/test-pp-xrm.sh.in | 12 +++++++- tests/test-xrm-front.sh.in | 29 ++++++++++---------- tests/xrm/desugar_builtins.pm | 29 ++++++++++++++++++++ 22 files changed, 360 insertions(+), 71 deletions(-) Index: src/lib/xrm/Makefile.am --- src/lib/xrm/Makefile.am (revision 32) +++ src/lib/xrm/Makefile.am (working copy) @@ -5,9 +5,7 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Wed May 10 19:27:12 2006 SIGOURE Benoit -## Last update Fri May 12 05:20:11 2006 SIGOURE Benoit +## Last update Thu May 25 18:44:02 2006 SIGOURE Benoit ## -include $(top_srcdir)/config/toplevel.mk - SUBDIRS = pp Index: src/lib/native/floor.c --- src/lib/native/floor.c (revision 0) +++ src/lib/native/floor.c (revision 0) @@ -0,0 +1,22 @@ +/* +** floor.c for str-reals in /home/tsuna/work/xrm/trunk/src/lib/native +** +** Made by SIGOURE Benoit +** Mail <sigoure.benoit(a)lrde.epita.fr> +** +** Started on Thu May 25 16:32:59 2006 SIGOURE Benoit +** Last update Thu May 25 18:57:46 2006 SIGOURE Benoit +*/ + +#include <math.h> +#include "libstr-reals.h" + +ATerm STR_REALS_floor(ATerm t) +{ + double r; + + if(ATgetType(t) != AT_REAL && ATgetType(t) != AT_INT) + return NULL; + NUMERIC_ATERM_TO_REAL(r, t); + return (ATerm) ATmakeReal(floor(r)); +} Index: src/lib/native/libstr-reals.h --- src/lib/native/libstr-reals.h (revision 0) +++ src/lib/native/libstr-reals.h (revision 0) @@ -0,0 +1,41 @@ +/* +** libstr-reals.h for str-reals in /home/tsuna/work/xrm/trunk/src/lib/native +** +** Made by SIGOURE Benoit +** Mail <sigoure.benoit(a)lrde.epita.fr> +** +** Started on Thu May 25 16:32:27 2006 SIGOURE Benoit +** Last update Thu May 25 20:10:05 2006 SIGOURE Benoit +*/ + +#ifndef LIBSTR_REALS_H_ +# define LIBSTR_REALS_H_ + +# include <srts/stratego.h> + +/** +** Transform an ATerm which is either an AT_REAL or an AT_INT into a double. +** @param dst destination double (itself, not a pointer to it) +** @param term term to transform in double. +** @warning the caller MUST ensure that @a term is of type AT_REAL or AT_INT. +*/ +# define NUMERIC_ATERM_TO_REAL(dst, term) \ + do { \ + if(ATgetType(term) == AT_REAL) \ + { \ + dst = ATgetReal((ATermReal) term); \ + } \ + else /* (ATgetType(term) == AT_INT) */ \ + { \ + dst = ATgetInt((ATermInt) term); \ + } \ + } while(0) + +ATerm STR_REALS_ceil(ATerm t); +ATerm STR_REALS_floor(ATerm t); +ATerm STR_REALS_powi(ATerm base, ATerm power); +ATerm STR_REALS_powr(ATerm base, ATerm power); +ATerm STR_REALS_modi(ATerm lhs, ATerm rhs); +ATerm STR_REALS_modr(ATerm lhs, ATerm rhs); + +#endif /* !LIBSTR_REALS_H_ */ Index: src/lib/native/Makefile.am --- src/lib/native/Makefile.am (revision 0) +++ src/lib/native/Makefile.am (revision 0) @@ -0,0 +1,30 @@ +## +## Makefile.am for xrm in /home/tsuna/work/xrm/trunk/src/lib/native +## +## Made by SIGOURE Benoit +## Mail <sigoure.benoit(a)lrde.epita.fr> +## +## Started on Wed May 10 19:27:12 2006 SIGOURE Benoit +## Last update Thu May 25 20:19:00 2006 SIGOURE Benoit +## + +include $(top_srcdir)/config/toplevel.mk + +lib_LTLIBRARIES = libstr-reals.la +include_HEADERS = libstr-reals.h + +libstr_reals_la_SOURCES = $(include_HEADERS) \ + ceil.c \ + floor.c \ + power.c + +# FIXME: Detect in configure whether -lm needs to be used. +libstr_reals_la_LIBADD = $(SSL_LIBS) -lm + +BUILT_SOURCES = import-libstr-reals.c + +import-libstr-reals.c: Makefile + echo "/* code generated; used for strc --C-include \"'$@'\" */" > $@ + for f in $(libstr_reals_la_SOURCES); do \ + echo "#include \"$$f\"" >> $@; \ + done Index: src/lib/native/ceil.c --- src/lib/native/ceil.c (revision 0) +++ src/lib/native/ceil.c (revision 0) @@ -0,0 +1,23 @@ +/* +** ceil.c for str-reals in /home/tsuna/work/xrm/trunk/src/lib/native +** +** Made by SIGOURE Benoit +** Mail <sigoure.benoit(a)lrde.epita.fr> +** +** Started on Thu May 25 16:32:50 2006 SIGOURE Benoit +** Last update Thu May 25 19:19:48 2006 SIGOURE Benoit +*/ + +#include <math.h> +#include <stdio.h> +#include "libstr-reals.h" + +ATerm STR_REALS_ceil(ATerm t) +{ + double r; + + if(ATgetType(t) != AT_REAL && ATgetType(t) != AT_INT) + return NULL; + NUMERIC_ATERM_TO_REAL(r, t); + return (ATerm) ATmakeReal(ceil(r)); +} Index: src/lib/native/power.c --- src/lib/native/power.c (revision 0) +++ src/lib/native/power.c (revision 0) @@ -0,0 +1,37 @@ +/* +** power.c for str-reals in /home/tsuna/work/xrm/trunk/src/lib/native +** +** Made by SIGOURE Benoit +** Mail <sigoure.benoit(a)lrde.epita.fr> +** +** Started on Thu May 25 16:33:04 2006 SIGOURE Benoit +** Last update Thu May 25 20:07:23 2006 SIGOURE Benoit +*/ + +#include <math.h> +#include "libstr-reals.h" + +ATerm STR_REALS_powi(ATerm base, ATerm power) +{ + int ibase; + int ipower; + + if(ATgetType(base) != AT_INT || ATgetType(power) != AT_INT) + return NULL; + ibase = ATgetInt((ATermInt) base); + ipower = ATgetInt((ATermInt) power); + return (ATerm) ATmakeReal(pow(ibase, ipower)); +} + +ATerm STR_REALS_powr(ATerm base, ATerm power) +{ + double rbase; + double rpower; + + if((ATgetType(base) != AT_REAL && ATgetType(base) != AT_INT) || + (ATgetType(power) != AT_REAL && ATgetType(power) != AT_INT)) + return NULL; + NUMERIC_ATERM_TO_REAL(rbase, base); + NUMERIC_ATERM_TO_REAL(rpower, power); + return (ATerm) ATmakeReal(pow(rbase, rpower)); +} Index: src/lib/Makefile.am --- src/lib/Makefile.am (revision 32) +++ src/lib/Makefile.am (working copy) @@ -5,9 +5,7 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Wed May 10 19:27:12 2006 SIGOURE Benoit -## Last update Fri May 12 05:34:10 2006 SIGOURE Benoit +## Last update Thu May 25 18:55:45 2006 SIGOURE Benoit ## -include $(top_srcdir)/config/toplevel.mk - -SUBDIRS = prism xrm +SUBDIRS = prism xrm native Index: src/lib/prism/Makefile.am --- src/lib/prism/Makefile.am (revision 32) +++ src/lib/prism/Makefile.am (working copy) @@ -5,9 +5,7 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Wed May 10 19:27:12 2006 SIGOURE Benoit -## Last update Wed May 10 19:39:03 2006 SIGOURE Benoit +## Last update Thu May 25 18:43:55 2006 SIGOURE Benoit ## -include $(top_srcdir)/config/toplevel.mk - SUBDIRS = pp Index: src/str/xrm-front.str --- src/str/xrm-front.str (revision 32) +++ src/str/xrm-front.str (working copy) @@ -21,7 +21,7 @@ main-wrapped = check-options ; xtc-transform(!"parse-xrm", // parse input (returns a FILE) - !["-b", "--preserve-positions" | <pass-verbose>()]) + <concat>[ ["-b"], <pass-verbose>(), <pass-add-pos>() ]) ; read-from // read parsed input ; /*FIXME*/strip-annos // FIXME: remove this line!!!!!!!!!!!!!!!!!!!!!!!!!! ; xrm-front-pipeline // transformations @@ -29,14 +29,10 @@ ; if <get-config> "-b" then write-to // output binary ATerms else - if must-pp-prism then // output PRISM source - write-to; xtc-transform(!"pp-prism", pass-verbose) - else if must-pp-aterm then // output pp-ATerms write-to; xtc-transform(!"pp-aterm", pass-verbose) - else - write-to-text // output text ATerms - end + else // output PRISM source + write-to; xtc-transform(!"pp-prism", pass-verbose) end end @@ -53,8 +49,8 @@ // list of available options for xrm-front xrm-front-options = - pp-prism-option - + pp-aterm-option + pp-aterm-option + + add-pos-option + keep-attributes-option + desugar-option @@ -66,13 +62,6 @@ where(<set-pp-aterm> "no") ; warn-msg(|"Pretty printing cancelled: binary output requested.") end - - // it doesn't make sense: we're asked for binary output + PRISM output! - ; if must-pp-prism then - err-msg(|"Cannot generate binary output (-b) and PRISM output - (--pp-prism|-P) at the same time.") - ; <exit> 1 - end end strategies @@ -92,21 +81,6 @@ strategies - pp-prism-option = - Option("-P" + "--pp-prism" - , <set-pp-prism> "yes" - , !HelpString("-P | --pp-prism", "Convert output in PRISM source code - using pp-prism") - ) - - set-pp-prism = - <set-config> ("pp-prism", <id>) - - must-pp-prism = - <get-config> "pp-prism" => "yes" - -strategies - pp-aterm-option = Option("-A" + "--pp-aterm" , <set-pp-aterm> "yes" @@ -133,6 +107,24 @@ must-desugar = <get-config> "desugar" => "yes" +strategies + + add-pos-option = + Option("-P" + "--add-pos" + , <set-add-pos> "yes" + , !HelpString("-P | --add-pos", "When issuing error messages, tell the line + and column of the error. This is disabled by default as it + implies a big memory overhead if the input file is big.") + ) + + set-add-pos = + <set-config> ("add-pos", <id>) + + must-add-pos = + <get-config> "add-pos" => "yes" + + pass-add-pos = must-add-pos < !["--preserve-positions"] + ![] + /** * Documentation */ Index: src/str/Makefile.am --- src/str/Makefile.am (revision 32) +++ src/str/Makefile.am (working copy) @@ -5,19 +5,22 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Thu Apr 27 17:59:35 2006 SIGOURE Benoit -## Last update Thu May 25 17:27:20 2006 SIGOURE Benoit +## Last update Thu May 25 19:32:14 2006 SIGOURE Benoit ## include $(top_srcdir)/config/Transformers.mk -include $(wildcard *.dep) bin_PROGRAMS = xrm-front -xrm_SOURCES = xrm-front.c +xrm_front_SOURCES= xrm-front.c SCFLAGS = --main main-$* STRINCLUDES = -I $(srcdir) -I $(XTC)/share/xtc \ -I $(top_builddir)/src/sig \ - -I $(top_builddir)/src/syn/xrm + -I $(top_builddir)/src/syn/xrm \ + --C-include '"$(top_builddir)/src/lib/native/import-libstr-reals.c"' +AM_CFLAGS = -I$(top_srcdir)/src/lib/native + LDADD += $(SSL_LIBS) EXTRA_DIST = $(wildcard *.str) Index: src/str/prism-desugar.str --- src/str/prism-desugar.str (revision 32) +++ src/str/prism-desugar.str (working copy) @@ -22,6 +22,7 @@ <+ EvalPlus <+ EvalMinus <+ EvalMul <+ EvalDiv <+ EvalLt <+ EvalLtEq <+ EvalGt <+ EvalGtEq <+ EvalEq <+ EvalNeq <+ EvalAnd <+ EvalOr + <+ EvalMin <+ EvalMax <+ EvalFloor <+ EvalCeil <+ EvalPow <+ EvalMod ) ; topdown(try(SimplifyDoubles <+ TruncateDouble)) @@ -160,3 +161,41 @@ |[ false | true ]| -> |[ true ]| EvalOr: |[ false | false ]| -> |[ false ]| + +rules + + EvalMin: + |[ func(min, a*) ]| -> |[ r ]| + where !a*;debug + ; map(\ Double(d) -> d \);debug + ; minRL => r;debug + + EvalMax: + |[ func(max, a*) ]| -> |[ r ]| + where !a*;debug + ; map(\ Double(d) -> d \);debug + ; maxRL => r;debug + + EvalFloor: + |[ func(floor, d) ]| -> |[ r ]| where <floor>(d) => r + + EvalCeil: + |[ func(ceil, d) ]| -> |[ r ]| where <ceil>(d) => r + + EvalPow: + |[ func(pow, d1, d2) ]| -> |[ r ]| where <powR>(d1, d2) => r + + EvalMod: + |[ func(mod, d1, d2) ]| -> |[ r ]| + where !Double(d1) => ast_d1 + ; !Double(d2) => ast_d2 + /* ensure that d1 and d2 are in fact Int */ + ; <SimplifyDoubles> ast_d1 => Int(i) + ; <SimplifyDoubles> ast_d2 => Int(j) + ; if !j => "0" then + err-msg(|"Modulo by zero detected:") + ; debug + ; <xtc-exit> 3 + else + <modS> (i, j) => r + end Index: src/str/reals.str --- src/str/reals.str (revision 32) +++ src/str/reals.str (working copy) @@ -2,16 +2,64 @@ strategies - // for some reason the following rules are only defined for integers - // in the stratego-lib. Here is their equivalent for reals. + /* + ** for some reason the following rules are only defined for integers + ** in the stratego-lib. Here is their equivalent for reals. + */ + + maxr = gtr < Fst + Snd + minr = gtr < Snd + Fst + addR = (string-to-real, string-to-real); addr; real-to-string subtR = (string-to-real, string-to-real); subtr; real-to-string mulR = (string-to-real, string-to-real); mulr; real-to-string 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)) 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) + + pow = powR <+ powI + + /** Let (x, y) be a tuple of reals, this strategy returns the value of x + ** raised to the power of y. + ** @type (String, String) -> String + */ + powR = (string-to-real, string-to-real); powr; real-to-string + + /** Let (x, y) be a tuple of integers, this strategy returns the value of x + ** raised to the power of y. + ** @warning the result may not be an integer (eg, if y is less than zero) + ** @type (String, String) -> String + */ + powS = (string-to-int, string-to-int); powi; real-to-string + + /** @type (Real, Real) -> Real */ + powr = ?(x, y); prim("STR_REALS_powr", x, y) + /** @type (Int, Int) -> Real */ + powi = ?(x, y); prim("STR_REALS_powi", x, y) + + ceil = string-to-real; prim("STR_REALS_ceil", <id>); real-to-string + floor = string-to-real; prim("STR_REALS_floor", <id>); real-to-string + + /** Find the min in a list of reals within strings + ** @type List(String) -> String + */ + minRL = + ?[h|t] + ; foldr(<string-to-real> h, minr, string-to-real) + ; real-to-string + + /** Find the max in a list of reals within strings + ** @type List(String) -> String + */ + maxRL = + ?[h|t] + ; foldr(<string-to-real> h, maxr, string-to-real) + ; real-to-string /** ** tests whether two reals are equal Index: src/syn/Makefile.am --- src/syn/Makefile.am (revision 32) +++ src/syn/Makefile.am (working copy) @@ -5,9 +5,7 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Thu Apr 27 17:40:41 2006 SIGOURE Benoit -## Last update Tue May 9 20:36:52 2006 SIGOURE Benoit +## Last update Thu May 25 18:44:17 2006 SIGOURE Benoit ## -include $(top_srcdir)/config/Transformers.mk - SUBDIRS = prism xrm Index: src/syn/prism/PRISM-MetaVars.sdf --- src/syn/prism/PRISM-MetaVars.sdf (revision 32) +++ src/syn/prism/PRISM-MetaVars.sdf (working copy) @@ -7,7 +7,7 @@ %% FIXME: The following doesn't work [xyzfgh][0-9]* "'" -> IdentifierPrime {prefer} [e][0-9]* -> Expression {prefer} - "a"[0-9]* "*" -> {Identifier ","}+ {prefer} + "a"[0-9]* "*" -> {Expression ","}+ {prefer} [m][0-9]* -> Module {prefer} "m"[0-9]* "*" -> Module+ {prefer} [c][0-9]* -> Command {prefer} Index: src/Makefile.am --- src/Makefile.am (revision 32) +++ src/Makefile.am (working copy) @@ -5,9 +5,9 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Thu Apr 27 16:57:03 2006 SIGOURE Benoit -## Last update Thu May 11 00:15:37 2006 SIGOURE Benoit +## Last update Thu May 25 19:05:24 2006 SIGOURE Benoit ## include $(top_srcdir)/config/toplevel.mk -SUBDIRS = syn sig str lib tools +SUBDIRS = syn sig lib str tools Index: tests/test-pp-prism.sh.in --- tests/test-pp-prism.sh.in (revision 32) +++ tests/test-pp-prism.sh.in (working copy) @@ -12,6 +12,7 @@ test_cnt=0 test_pass=0 target_dir='output-pp-prism' +rm -f failed_tests.$$ test ! -d $target_dir && { mkdir $target_dir \ || { echo "Cannot create $target_dir/ directory" && exit 1; } } @@ -31,6 +32,7 @@ "@top_builddir@/src/tools/parse-prism" -i "$file" -o "$outdir/$bfile.aterm" if [ $? -ne 0 ]; then echo 'FAILED, continuing with the next test...' + echo " * $file: parsing FAILED" >> failed_tests.$$ continue fi echo 'OK, no ambiguities found' @@ -40,6 +42,7 @@ -i "$outdir/$bfile.aterm" -o "$outdir/$bfile.pp.pm" if [ $? -ne 0 ]; then echo 'FAILED, continuing with the next test...' + echo " * $file: pretty printing FAILED" >> failed_tests.$$ continue fi echo 'OK' @@ -53,6 +56,7 @@ cat -n "$outdir/$bfile.pp.pm" echo '<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<' echo 'Now continuing with the next test...' + echo " * $file: re-parsing FAILED" >> failed_tests.$$ continue fi echo 'OK, no ambiguities found' @@ -62,6 +66,7 @@ -i "$outdir/$bfile.pp2aterm" -o "$outdir/$bfile.pp2.pm" if [ $? -ne 0 ]; then echo 'FAILED, continuing with the next test...' + echo " * $file: re-pretty printing FAILED" >> failed_tests.$$ continue fi echo 'OK' @@ -78,10 +83,14 @@ @STRATEGOXT@/bin/pp-aterm \ -i "$outdir/$bfile.pp2aterm" -o "$outdir/$bfile.pp2aterm.pp" diff -u "$outdir/$bfile.aterm.pp" "$outdir/$bfile.pp2aterm.pp" + echo " * $file: both parses did NOT produce the same AST" >> failed_tests.$$ + continue ;; *pp*) echo 'FAILED: the two pretty printing did NOT produce the same source:' diff -u "$outdir/$bfile.pp.pm" "$outdir/$bfile.pp2.pm" + echo " * $file: both pretty pretty did NIT produce the same source" >> failed_tests.$$ + continue ;; esac @@ -91,6 +100,7 @@ echo "$0: $test_pass/$test_cnt tests passed" echo "`date` $0: $test_pass/$test_cnt tests passed" >> test_summary -rm -rf "$outdir" +cat failed_tests.$$ >> test_summary +rm -rf failed_tests.$$ "$outdir" test $test_pass -eq $test_cnt Index: tests/xrm/desugar_builtins.pm --- tests/xrm/desugar_builtins.pm (revision 0) +++ tests/xrm/desugar_builtins.pm (revision 0) @@ -0,0 +1,29 @@ +module desugarme + x : [0..42]; + + // [] x=min(0) -> (x'=1); // invalid (must have at least 2 args) + [] x=func(min, 1, 2) -> (x'=0); + [] x=func(min, 4, 3, 5) -> (x'=1); + + // [] x=max(4) -> (x'=2); // invalid (must have at least 2 args) + [] x=func(max, 4, 5) -> (x'=3); + [] x=max(4, 5, 6) -> (x'=4); + + [] x=floor(41) -> (x'=5); + [] x=func(floor, 42.2) -> (x'=6); + // [] x=func(floor, 5, 6) -> (x'=7); // invalid (must have 1 arg) + + [] x=ceil(40) -> (x'=8); + [] x=func(ceil, 41.2) -> (x'=9); + // [] x=func(ceil, 5, 6) -> (x'=10); // invalid (must have 1 arg) + + // NOTE: there is no "short" version for pow, eg pow(2, 8) + // NOTE: short versions are "deprecated" + [] x=func(pow, 2, 8) -> (x'=11); + [] x=func(pow, 9.0, 0.5) -> (x'=12); + // [] x=func(pow, 5, 6, 7) -> (x'=13); // invalid (must have 2 args) + + [] x=func(mod, 1977, 100) -> (x'=14); + // [] x=func(mod, 42, 0) -> (x'=15); // invalid (modulo by 0) + // [] x=func(mod, 5, 6, 7) -> (x'=16); // invalid (must have 2 args) +endmodule Index: tests/test-xrm-front.sh.in --- tests/test-xrm-front.sh.in (revision 32) +++ tests/test-xrm-front.sh.in (working copy) @@ -12,6 +12,7 @@ test_cnt=0 test_pass=0 target_dir='output-xrm-front' +rm -f failed_tests.$$ test ! -d $target_dir && { mkdir $target_dir \ || { echo "Cannot create $target_dir/ directory" && exit 1; } } @@ -27,46 +28,43 @@ echo ">>> Starting the test for $basefile" test_cnt=$((test_cnt + 1)) - echo @ECHO_N@ " Converting $basefile into standard PRISM AST ... " - "@top_builddir@/src/str/xrm-front" \ + echo @ECHO_N@ " Converting $basefile into standard PRISM ... " + "@top_builddir@/src/str/xrm-front" -A \ -i "$file" -o "$outdir/$bfile.pm.aterm" if [ $? -ne 0 ]; then echo 'FAILED, continuing with the next test...' + echo " * $file: xrm-front failed (-A) FAILED" >> failed_tests.$$ continue fi echo 'OK' echo @ECHO_N@ " Converting $basefile into standard PRISM code ... " - "@top_builddir@/src/str/xrm-front" -P \ + "@top_builddir@/src/str/xrm-front" \ -i "$file" -o "$outdir/$bfile.pm" if [ $? -ne 0 ]; then echo 'FAILED, continuing with the next test...' + echo " * $file: xrm-front failed FAILED" >> failed_tests.$$ continue fi echo 'OK' echo @ECHO_N@ " Re-Parsing generated PRISM code for $basefile ... " - "@top_builddir@/src/tools/parse-prism" \ + "@top_builddir@/src/tools/parse-prism" -A \ -i "$outdir/$bfile.pm" -o "$outdir/$bfile.pm2.aterm" if [ $? -ne 0 ]; then echo 'FAILED, continuing with the next test...' + echo " * $file: re-parsing FAILED" >> failed_tests.$$ continue fi echo 'OK, no ambiguities found' - err='' - diff -q "$outdir/$bfile.pm.aterm" "$outdir/$bfile.pm2.aterm" || err='aterm' + diff -q "$outdir/$bfile.pm.aterm" "$outdir/$bfile.pm2.aterm" - case $err in - *aterm*) + if [ $? -ne 0 ]; then echo 'FAILED: the two parses did NOT produce the same AST:' - @STRATEGOXT@/bin/pp-aterm \ - -i "$outdir/$bfile.pm.aterm" -o "$outdir/$bfile.pm.aterm.pp" - @STRATEGOXT@/bin/pp-aterm \ - -i "$outdir/$bfile.pm2.aterm" -o "$outdir/$bfile.pm2.aterm.pp" + echo " * $file: both parses did NOT produce the same AST" >> failed_tests.$$ diff -u "$outdir/$bfile.pm.aterm.pp" "$outdir/$bfile.pm2.aterm.pp" - ;; - esac + fi echo "<<< Test for $basefile PASSED" test_pass=$((test_pass + 1)) @@ -74,6 +72,7 @@ echo "$0: $test_pass/$test_cnt tests passed" echo "`date` $0: $test_pass/$test_cnt tests passed" >> test_summary -rm -rf "$outdir" +cat failed_tests.$$ >> test_summary +rm -rf failed_tests.$$ "$outdir" test $test_pass -eq $test_cnt Index: tests/test-parse-xrm.sh.in --- tests/test-parse-xrm.sh.in (revision 32) +++ tests/test-parse-xrm.sh.in (working copy) @@ -11,16 +11,22 @@ test_cnt=0 test_pass=0 +rm -f failed_tests.$$ + for file in `find "@srcdir@" -name '*.pm' -o -name '*.nm' -o -name '*.sm' -o -name '*.xpm' | sort`; do echo @ECHO_N@ " Parsing `basename $file` ... " "@top_builddir@/src/tools/parse-xrm" -i "$file" -o /dev/null if [ $? -eq 0 ]; then echo 'OK, no ambiguities found' test_pass=$((test_pass + 1)) + else + echo " * $file: FAILED (bad return value: $rv)" >> failed_tests.$$ fi test_cnt=$((test_cnt + 1)) done echo "$0: $test_pass/$test_cnt tests passed" echo "`date` $0: $test_pass/$test_cnt tests passed" >> test_summary +cat failed_tests.$$ >> test_summary +rm -f failed_tests.$$ test $test_pass -eq $test_cnt Index: tests/test-parse-prism.sh.in --- tests/test-parse-prism.sh.in (revision 32) +++ tests/test-parse-prism.sh.in (working copy) @@ -11,16 +11,23 @@ test_cnt=0 test_pass=0 +rm -f failed_tests.$$ + for file in `find "@srcdir@" -name '*.pm' -o -name '*.nm' -o -name '*.sm' | sort`; do echo @ECHO_N@ " Parsing `basename $file` ... " "@top_builddir@/src/tools/parse-prism" -i "$file" -o /dev/null - if [ $? -eq 0 ]; then + rv=$? + if [ $rv -eq 0 ]; then echo 'OK, no ambiguities found' test_pass=$((test_pass + 1)) + else + echo " * $file: FAILED (bad return value: $rv)" >> failed_tests.$$ fi test_cnt=$((test_cnt + 1)) done echo "$0: $test_pass/$test_cnt tests passed" echo "`date` $0: $test_pass/$test_cnt tests passed" >> test_summary +cat failed_tests.$$ >> test_summary +rm -f failed_tests.$$ test $test_pass -eq $test_cnt Index: tests/test-pp-xrm.sh.in --- tests/test-pp-xrm.sh.in (revision 32) +++ tests/test-pp-xrm.sh.in (working copy) @@ -12,6 +12,7 @@ test_cnt=0 test_pass=0 target_dir='output-pp-xrm' +rm -f failed_tests.$$ test ! -d $target_dir && { mkdir $target_dir \ || { echo "Cannot create $target_dir/ directory" && exit 1; } } @@ -31,6 +32,7 @@ "@top_builddir@/src/tools/parse-xrm" -i "$file" -o "$outdir/$bfile.aterm" if [ $? -ne 0 ]; then echo 'FAILED, continuing with the next test...' + echo " * $file: parsing FAILED" >> failed_tests.$$ continue fi echo 'OK, no ambiguities found' @@ -40,6 +42,7 @@ -i "$outdir/$bfile.aterm" -o "$outdir/$bfile.pp.xpm" if [ $? -ne 0 ]; then echo 'FAILED, continuing with the next test...' + echo " * $file: pretty printing FAILED" >> failed_tests.$$ continue fi echo 'OK' @@ -53,6 +56,7 @@ cat -n "$outdir/$bfile.pp.xpm" echo '<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<' echo 'Now continuing with the next test...' + echo " * $file: re-parsing FAILED" >> failed_tests.$$ continue fi echo 'OK, no ambiguities found' @@ -62,6 +66,7 @@ -i "$outdir/$bfile.pp2aterm" -o "$outdir/$bfile.pp2.xpm" if [ $? -ne 0 ]; then echo 'FAILED, continuing with the next test...' + echo " * $file: re-pretty printing FAILED" >> failed_tests.$$ continue fi echo 'OK' @@ -78,10 +83,14 @@ @STRATEGOXT@/bin/pp-aterm \ -i "$outdir/$bfile.pp2aterm" -o "$outdir/$bfile.pp2aterm.pp" diff -u "$outdir/$bfile.aterm.pp" "$outdir/$bfile.pp2aterm.pp" + echo " * $file: both parses did NOT produce the same AST" >> failed_tests.$$ + continue ;; *pp*) echo 'FAILED: the two pretty printing did NOT produce the same source:' diff -u "$outdir/$bfile.pp.xpm" "$outdir/$bfile.pp2.xpm" + echo " * $file: both pretty pretty did NIT produce the same source" >> failed_tests.$$ + continue ;; esac @@ -91,6 +100,7 @@ echo "$0: $test_pass/$test_cnt tests passed" echo "`date` $0: $test_pass/$test_cnt tests passed" >> test_summary -rm -rf "$outdir" +cat failed_tests.$$ >> test_summary +rm -rf failed_tests.$$ "$outdir" test $test_pass -eq $test_cnt Index: configure.ac --- configure.ac (revision 32) +++ configure.ac (working copy) @@ -5,7 +5,7 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Thu Apr 27 15:55:56 2006 SIGOURE Benoit -## Last update Tue May 16 04:03:02 2006 SIGOURE Benoit +## Last update Thu May 25 18:56:02 2006 SIGOURE Benoit ## ## --------------- ## @@ -79,6 +79,7 @@ src/lib/prism/pp/Makefile src/lib/xrm/Makefile src/lib/xrm/pp/Makefile + src/lib/native/Makefile src/tools/Makefile tests/Makefile ]) Property changes on: bootstrap ___________________________________________________________________ Name: svn:executable + *

17 years, 11 months

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

Projects May 2006