[Projects] XRM 79: Generalize ranges.

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit &lt;sigoure.benoit(a)lrde.epita.fr&gt; Generalize ranges. /!\ Backward compatibility broken! In order to declare an array, one MUST now use ranges. Before this commit, declarations such as: const int array[N]; were desugared down to: const int array[0..N-1]; This expansion will no longer take place automatically so one must write const int array[0..N-1] explicitly. Writing const int array[N] will only declare one variable, that is the Nth variable of the array. * src/str/array-decl-desugar.str: Remove automatic desugarisation of array declarations. * src/str/eval-meta-code.str: Remove now useless comments and annotations about substituted meta-vars. * src/str/signatures.str: Remove non longer needed signature. * tests/xrm/exists-eq.xpm, * tests/xrm/array-decl-with-meta-and-non-meta-and-exp.xpm, * tests/xrm/cond-array-access.xpm, * tests/xrm/array-decl_1d.xpm, * tests/xrm/array-decl_3d.xpm, * tests/xrm/priorities-exp-array-subscript.xpm, * tests/xrm/array-decl_dim_exp.xpm, * tests/xrm/array-decl-with-meta-and-non-meta.xpm, * tests/xrm/static-const-arrays-desugar.xpm, * tests/xrm/array-decl_2d.xpm, * tests/xrm/consts.xpm, * tests/xrm/array_with_static_dim.xpm: Update array declarations. * doc/user-guide.txt: Bring up to date. doc/user-guide.txt | 49 +++------- src/str/array-decl-desugar.str | 75 ++-------------- src/str/eval-meta-code.str | 11 -- src/str/signatures.str | 8 - tests/xrm/array-decl-with-meta-and-non-meta-and-exp.xpm | 2 tests/xrm/array-decl-with-meta-and-non-meta.xpm | 2 tests/xrm/array-decl_1d.xpm | 8 - tests/xrm/array-decl_2d.xpm | 8 - tests/xrm/array-decl_3d.xpm | 8 - tests/xrm/array-decl_dim_exp.xpm | 2 tests/xrm/array_with_static_dim.xpm | 2 tests/xrm/cond-array-access.xpm | 2 tests/xrm/consts.xpm | 12 +- tests/xrm/exists-eq.xpm | 4 tests/xrm/priorities-exp-array-subscript.xpm | 4 tests/xrm/static-const-arrays-desugar.xpm | 4 16 files changed, 59 insertions(+), 142 deletions(-) Index: src/str/array-decl-desugar.str --- src/str/array-decl-desugar.str (revision 78) +++ src/str/array-decl-desugar.str (working copy) @@ -9,51 +9,6 @@ module array-decl-desugar imports desugar-array-access -strategies - - /** - ** Desugar dimensions in array declarations in explicit ranges. - ** eg: x[1,2][4] is desugared to x[1,2][0..3] - */ - desugar-array-access-for-decl = - ArrayAccess(try(desugar-array-access-for-decl), try(try-add-range)) - - /** - ** Try to add a range if one of the dimensions is a simple Int - */ - try-add-range = - if ?[single-elem] then // we might need to add a range (x[4] -> x[0..3]) - /* in the current term (including subterms), we're collecting all the - * annotations that match Generated(_) which means that the dimensions - * has been generated by eval-meta-code and must no be transformed into - * a range */ - where(collect-all({a*:?_{a*};<fetch(?Generated(_))> a*}) => genlist) - ; prism-desugar - ; if !genlist => [] then // the dimension wasn't generated: - add-range // we can (try to) expand it in a range - end - else // no need to add a range, simply desugar the array access - prism-desugar - end - -rules - - /** @internal Rewrite simple dimensions with ranges (x[4] -> x[0..3]). */ - add-range: - [Int(i)] -> [Range(Int("0"), Int(j))] - where if <eq>(i, "0") then - err-msg(|"array declared with a size of 0 element") - ; debug - ; <xtc-exit> 2 - else - if <ltS>(i, "0") then - err-msg(|"array declared with a negative number of elements") - ; debug - ; <xtc-exit> 2 - end - end - ; <subtS>(i, "1") => j - rules // FIXME: Try to figure out why concrete syntax fails to work here. // FIXME: Try to put some code in common in order to shorten the rules. @@ -69,8 +24,7 @@ IntDecNoInit(aa@ArrayAccess(aa_idf, _), low, up) -> int-decl-no-init-list where <fetch-idf> aa_idf => idf - ; <desugar-array-access-for-decl> aa - ; desugar-array-access + ; <desugar-array-access> aa ; desugared-array-access-list-to-identifier-list(|idf) ; map({var-name: ?var-name @@ -83,8 +37,7 @@ IntDec(aa@ArrayAccess(aa_idf, _), low, up, value) -> int-decl-list where <fetch-idf> aa_idf => idf - ; <desugar-array-access-for-decl> aa - ; desugar-array-access + ; <desugar-array-access> aa ; desugared-array-access-list-to-identifier-list(|idf) ; map({var-name: ?var-name @@ -99,8 +52,7 @@ BoolDecNoInit(aa@ArrayAccess(aa_idf, _)) -> bool-decl-no-init-list where <fetch-idf> aa_idf => idf - ; <desugar-array-access-for-decl> aa - ; desugar-array-access + ; <desugar-array-access> aa ; desugared-array-access-list-to-identifier-list(|idf) ; map({var-name: ?var-name @@ -113,8 +65,7 @@ BoolDec(aa@ArrayAccess(aa_idf, _), value) -> bool-decl-list where <fetch-idf> aa_idf => idf - ; <desugar-array-access-for-decl> aa - ; desugar-array-access + ; <desugar-array-access> aa ; desugared-array-access-list-to-identifier-list(|idf) ; map({var-name: ?var-name @@ -133,8 +84,7 @@ ConstInt(aa@ArrayAccess(aa_idf, _), value) -> const-int-decl-list where <fetch-idf> aa_idf => idf - ; <desugar-array-access-for-decl> aa - ; desugar-array-access + ; <desugar-array-access> aa ; desugared-array-access-list-to-identifier-list(|idf) ; map({var-name: ?var-name @@ -147,8 +97,7 @@ ConstIntNoInit(aa@ArrayAccess(aa_idf, _)) -> const-int-decl-no-init-list where <fetch-idf> aa_idf => idf - ; <desugar-array-access-for-decl> aa - ; desugar-array-access + ; <desugar-array-access> aa ; desugared-array-access-list-to-identifier-list(|idf) ; map({var-name: ?var-name @@ -163,8 +112,7 @@ ConstDouble(aa@ArrayAccess(aa_idf, _), value) -> const-double-decl-list where <fetch-idf> aa_idf => idf - ; <desugar-array-access-for-decl> aa - ; desugar-array-access + ; <desugar-array-access> aa ; desugared-array-access-list-to-identifier-list(|idf) ; map({var-name: ?var-name @@ -177,8 +125,7 @@ ConstDoubleNoInit(aa@ArrayAccess(aa_idf, _)) -> const-double-decl-no-init-list where <fetch-idf> aa_idf => idf - ; <desugar-array-access-for-decl> aa - ; desugar-array-access + ; <desugar-array-access> aa ; desugared-array-access-list-to-identifier-list(|idf) ; map({var-name: ?var-name @@ -193,8 +140,7 @@ ConstBool(aa@ArrayAccess(aa_idf, _), value) -> const-bool-decl-list where <fetch-idf> aa_idf => idf - ; <desugar-array-access-for-decl> aa - ; desugar-array-access + ; <desugar-array-access> aa ; desugared-array-access-list-to-identifier-list(|idf) ; map({var-name: ?var-name @@ -207,8 +153,7 @@ ConstBoolNoInit(aa@ArrayAccess(aa_idf, _)) -> const-bool-decl-no-init-list where <fetch-idf> aa_idf => idf - ; <desugar-array-access-for-decl> aa - ; desugar-array-access + ; <desugar-array-access> aa ; desugared-array-access-list-to-identifier-list(|idf) ; map({var-name: ?var-name Index: src/str/eval-meta-code.str --- src/str/eval-meta-code.str (revision 78) +++ src/str/eval-meta-code.str (working copy) @@ -10,13 +10,6 @@ ** fact that the `&' is lazy and that s[x-1] won't be expanded for invalid ** values of x. ** -** The code generated is annotated with the Generated("s") annotation where -** s is the name of the strategy which generated the code (can be useful for -** debugging). -** We annotate generated code because the rest of the pipeline might need to -** know what has been generated and what comes from the user to take -** different actions depending on that (eg: in array-decl-desugar.str). -** ** NOTE: This is a tricky part so debugging stuff have been kept and ** commented out instead of being deleted. Hopefully this will make ** debugging easier. This might also make the code easier to understand. @@ -160,7 +153,7 @@ ///*DEBUG*/; printf(|" i = ", i) ///*DEBUG*/; say(!" <<< gen-meta-for -- propagating meta-var's value <<< ") ; !body - ; topdown(try(?meta-var; !Int(i){Generated("gen-meta-for")})) + ; topdown(try(?meta-var; !Int(i))) ///*DEBUG*/; debug ///*DEBUG*/; say(!" ~~~ gen-meta-for: now recursing") ; eval-meta-code => generated-code @@ -196,7 +189,7 @@ ///*DEBUG*/; printf(|" exp-to-replace = ", exp-to-replace) ///*DEBUG*/; say(!" <<< gen-meta-forin -- propagating meta-var's value <<< ") ; !body - ; topdown(try(?meta-var; !exp-to-replace{Generated("gen-meta-forin")})) + ; topdown(try(?meta-var; !exp-to-replace)) ///*DEBUG*/; debug ///*DEBUG*/; say(!" ~~~ gen-meta-forin: now recursing") ; eval-meta-code => generated-code Index: src/str/signatures.str --- src/str/signatures.str (revision 78) +++ src/str/signatures.str (working copy) @@ -14,11 +14,3 @@ */ signature constructors FIXME : FIXME - -/** -** used in eval-meta-code.str -** annotation to indicate generated code which must not go through further -** expansions. -*/ -signature constructors - Generated : String -> Generated Index: tests/xrm/exists-eq.xpm --- tests/xrm/exists-eq.xpm (revision 78) +++ tests/xrm/exists-eq.xpm (working copy) @@ -1,8 +1,8 @@ formula N = 4; module test - x[N] : [0..42]; - y[4][4] : [0..42] init 0; + x[0..N] : [0..42]; + y[0..4][0..4] : [0..42] init 0; [] x[3]?=0 -> true; [] y[3][2]?=0 -> true; Index: tests/xrm/array-decl-with-meta-and-non-meta-and-exp.xpm --- tests/xrm/array-decl-with-meta-and-non-meta-and-exp.xpm (revision 78) +++ tests/xrm/array-decl-with-meta-and-non-meta-and-exp.xpm (working copy) @@ -1,5 +1,5 @@ for i from 0 to 4 do for j in 0, 1 do - const int N[i+2+j][3] = 0; + const int N[i+2+j][0..3] = 0; end end Index: tests/xrm/cond-array-access.xpm --- tests/xrm/cond-array-access.xpm (revision 78) +++ tests/xrm/cond-array-access.xpm (working copy) @@ -1,4 +1,4 @@ module test - x[4] : [0..42] init 0; + x[0..4] : [0..42] init 0; [] x[-1<0?0:-1]=0 -> true; endmodule Index: tests/xrm/array-decl_1d.xpm --- tests/xrm/array-decl_1d.xpm (revision 78) +++ tests/xrm/array-decl_1d.xpm (working copy) @@ -1,8 +1,8 @@ // should be expanded in x_0 x_1 x_2 x_3 module arrays - x[4] : [0..42]; - y[4] : [0..42] init 0; - b[4] : bool; - c[4] : bool init true; + x[0..4] : [0..42]; + y[0..4] : [0..42] init 0; + b[0..4] : bool; + c[0..4] : bool init true; endmodule Index: tests/xrm/array-decl_3d.xpm --- tests/xrm/array-decl_3d.xpm (revision 78) +++ tests/xrm/array-decl_3d.xpm (working copy) @@ -1,8 +1,8 @@ // should be expanded in x_0_0_0 x_0_0_1 x_0_0_2 x_0_0_3 ... module arrays - x[4][3][2] : [0..42]; - y[4][3][2] : [0..42] init 0; - b[4][3][2] : bool; - c[4][3][2] : bool init true; + x[0..4][0..3][0..2] : [0..42]; + y[0..4][0..3][0..2] : [0..42] init 0; + b[0..4][0..3][0..2] : bool; + c[0..4][0..3][0..2] : bool init true; endmodule Index: tests/xrm/priorities-exp-array-subscript.xpm --- tests/xrm/priorities-exp-array-subscript.xpm (revision 78) +++ tests/xrm/priorities-exp-array-subscript.xpm (working copy) @@ -1,7 +1,7 @@ module test - x[3] : bool init false; + x[0..3] : bool init false; y : bool init true; - x[4] : [0..42] init 0; + x[0..4] : [0..42] init 0; //[] true -> x[1|1]'=true; [] x[true?2:3]=0 -> true; Index: tests/xrm/array-decl_dim_exp.xpm --- tests/xrm/array-decl_dim_exp.xpm (revision 78) +++ tests/xrm/array-decl_dim_exp.xpm (working copy) @@ -1,5 +1,5 @@ // should be equivalent as declaring x[8] module arrays - x[4+4] : [0..42]; + x[0..4+4] : [0..42]; endmodule Index: tests/xrm/array-decl-with-meta-and-non-meta.xpm --- tests/xrm/array-decl-with-meta-and-non-meta.xpm (revision 78) +++ tests/xrm/array-decl-with-meta-and-non-meta.xpm (working copy) @@ -1,3 +1,3 @@ for i from 0 to 4 do - const int N[i][3] = 0; + const int N[i][0..3] = 0; end Index: tests/xrm/static-const-arrays-desugar.xpm --- tests/xrm/static-const-arrays-desugar.xpm (revision 78) +++ tests/xrm/static-const-arrays-desugar.xpm (working copy) @@ -1,8 +1,8 @@ const int N = 3; -const int array[N] = 42; +const int array[0..N] = 42; module test - x[N] : [0..N] init array[N]; + x[0..N] : [0..N] init array[N]; [] x[array[N]]=0 -> (x[array[N]]'=1); endmodule Index: tests/xrm/array-decl_2d.xpm --- tests/xrm/array-decl_2d.xpm (revision 78) +++ tests/xrm/array-decl_2d.xpm (working copy) @@ -3,8 +3,8 @@ // x_0_2 x_1_2 x_2_2 x_3_2 module arrays - x[4][3] : [0..42]; - y[4][3] : [0..42] init 0; - b[4][3] : bool; - c[4][3] : bool init true; + x[0..4][0..3] : [0..42]; + y[0..4][0..3] : [0..42] init 0; + b[0..4][0..3] : bool; + c[0..4][0..3] : bool init true; endmodule Index: tests/xrm/consts.xpm --- tests/xrm/consts.xpm (revision 78) +++ tests/xrm/consts.xpm (working copy) @@ -2,9 +2,9 @@ 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; +const int y[0..5]; +const z[0..5] = 42; +const double d[0..3] = 3.14; +rate c[0..4] = 42 > 3.14; +probe d[0..4]; +const bool b[0..3] = true; Index: tests/xrm/array_with_static_dim.xpm --- tests/xrm/array_with_static_dim.xpm (revision 78) +++ tests/xrm/array_with_static_dim.xpm (working copy) @@ -1,5 +1,5 @@ const int N = 10; module test - s[N] : [0..1]; + s[0..N] : [0..1]; endmodule Index: doc/user-guide.txt --- doc/user-guide.txt (revision 78) +++ doc/user-guide.txt (working copy) @@ -37,6 +37,7 @@ Once Nix is installed, use the following commands (you might need to be root depending on how you installed nix): $ nix-channel --add http://nix.cs.uu.nl/dist/stratego/channels-v3/strategoxt-unstable + $ nix-env -u '*' $ nix-env --install aterm sdf2-bundle strategoxt There you are! Add the following line to your .bashrc/.zshrc: @@ -159,11 +160,11 @@ variables. Everywhere a variable declaration was allowed in PRISM, an array declaration is allowed in XRM. o Arrays can be declared like in C, eg: - x[4] : [0..1] init 0; + x[0..4] : [0..1] init 0; will declare an array of 4 elements: x[0], x[1], x[2] and x[3]. So it's all like in C (access from to 0 through N-1) o It's possible to declare multidimensional arrays, eg: - x[3][4] : [0..1] init 0; + x[0..3][0..4] : [0..1] init 0; Again this is *almost* like C with the exception for multidimensional arrays that intermediate dimensions are not accessible (simply because they don't exist). So the former declaration will declare: @@ -176,11 +177,8 @@ x[2..4][0,3..5] will declare only: x[2][0], x[2][3], x[2][4], x[2][5], x[3][0], x[3][3], x[3][4], x[3][5], x[4][0], x[4][3], x[4][4], x[4][5] - So basically, when one of the dimensions of an array declaration is a - simple integer, eg: x[N] it is expansed in x[0..N-1]. Then the Cartesian - product of all the dimensions of the array is used to compute the set of - accessible variables. - o Dimensions of size zero are not allowed, eg: x[0] : [0..1]; + The Cartesian product of all the dimensions of the array is used to + compute the set of accessible variables. o Arrays can also be implicitly declared using for loops (see below, the section about for loops in XRM). o Array accesses can be found (nearly) everywhere a simple variable @@ -196,6 +194,14 @@ [] x[N+3]=0 -> ...; // valid: N+3 can be worked out at compile time. [] x[i+3]=0 -> ...; // invalid: the value of `i' is dynamic and unknown // at compile time. + o NOTE: In XRM 1.0 and before, it was possible to declare arrays like in C, + eg: + const int array[N]; + was automatically desugared to: + const int array[0..N-1]; + This is no longer true since XRM 1.1, one must now explicitly write + const int array[0..N-1] and const int array[N] leads to the declaration + of a single variable, that is, the Nth variable of the array. + TODO: Array accesses with dynamic subscripts. # XRM Meta-code @@ -238,38 +244,19 @@ endmodule end will generate 3 modules: dummy[1], dummy[2] and dummy[3]. - Of course, since each module has its own unique variables too, the - variables declared in that generated module will also have to be suffixed - by an array access with the meta-var. - In this case though, when `i' gets replaced by its successive values, we - have the following modules: - module dummy[1] - x[1] : [0..1] init 0; // not an array declaration - endmodule - module dummy[2] - x[2] : [0..1] init 0; // ditto - endmodule - module dummy[3] - x[3] : [0..1] init 0; // ditto - endmodule - But fortunately, this will not create 3 times an array called `x'. In - this very special case, the numerical values will not be expansed as - x[0..1] for dummy[1], x[0..2] for dummy[2] and x[0..3] for dummy[3] - because the integer in the array subscript comes from the expansion of a - meta-var and won't be further expanded. Thus in this case you get 3 different modules, each with their own single unique variable `x'. If you wish to provide each module with an array of, say 6 elements, then do the following: for i from 1 to 3 do module dummy[i] - x[i][5] : [0..1] init 0; + x[i][0..5] : [0..1] init 0; endmodule end In this case the first dimensions (`i') will first be expansed by the loop unrolling, which will equip each generated module with its own - unique variable `x' and then the second dimension will be expansed to - 0..5 which will create an array of 6 elements for each generated module. + unique variable `x' and then the second dimension will create an array of + 6 elements for each generated module. o Meta-for loops can also be used to declare arrays implicitely: module ImplicitArray for i from 0 to 3 do @@ -437,8 +424,8 @@ x[1..3]?=0 => x_1=0 | x_2=0 | x_3=0 - Dynamic array accesses, eg: x[i] where `i' is not known at compile-time. - Array initializations a la C: - x[3] : [0..4] init {0, 1, 2}; - const int array[3] = {0, 1, 2}; + x[0..3] : [0..4] init {0, 1, 2}; + const int array[0..3] = {0, 1, 2}; - Better error messages (with the location of error). **************