>>> "Roland" == Roland Levillain <roland(a)lrde.epita.fr> writes:
> Vcs' messages go to the projects list instead of the tiger-patches
> list, as for Nolimips and HAVM.
I prefer tiger-patches for havm. I would vote for tiger-patches for
the other two, but I'm not responsible for them.
https://svn.lrde.epita.fr/svn/xrm/trunk
Index: ChangeLog
from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr>
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).
**************
https://svn.lrde.epita.fr/svn/xrm/trunk
Index: ChangeLog
from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr>
Add lazy and/or evaluation at the meta-level.
One can now rely on laziness of logical operators to prevent what
could be an error at the meta-level, eg: x > 0 & s[x-1]=0
* src/str/eval-meta-code.str (eval-meta-code): Add lazy and/or
evaluation.
* src/str/eval-meta-code.meta: New.
* tests/xrm/formula-amb.xpm: New. Failing test case (ticket #25).
* tests/xrm/rivf.xpm: Use the lazyness.
src/str/eval-meta-code.str | 29 +++++++++++++++++++++++++++++
tests/xrm/formula-amb.xpm | 1 +
tests/xrm/rivf.xpm | 2 +-
3 files changed, 31 insertions(+), 1 deletion(-)
Index: src/str/eval-meta-code.str
--- src/str/eval-meta-code.str (revision 77)
+++ src/str/eval-meta-code.str (working copy)
@@ -3,6 +3,13 @@
** XRM modules can contain meta for loops as well as meta if statements
** which have to evaluated and transformed in PRISM source code.
**
+** NOTE: We also evaluate normal if statements if possible because they can
+** be used as a short way of writing meta-if statements. We also perform a
+** lazy evaluation of and's (`&') and or's (`|') because they can be used to
+** protect potentially invalid meta code, eg: x > 0 & s[x-1]=0 relies on the
+** 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).
@@ -29,6 +36,8 @@
eval-meta-code =
eval-meta-if
+ <+ lazy-eval-and
+ <+ lazy-eval-or
<+ unroll-meta-for
<+ unroll-meta-forin
<+ (expand-pformulas; eval-meta-code) // try again on expansed code.
@@ -72,6 +81,26 @@
end
end
+ lazy-eval-and =
+ ?|[ e1 & e2 ]|
+ ; <prism-desugar> e1
+ ; try(LitToBool) => e1'
+ ; if !e1' => False() then
+ !False()
+ else
+ fail
+ end
+
+ lazy-eval-or =
+ ?|[ e1 | e2 ]|
+ ; <prism-desugar> e1
+ ; try(LitToBool) => e1'
+ ; if !e1' => True() then
+ !True()
+ else
+ fail
+ end
+
strategies
unroll-meta-for =
Index: tests/xrm/formula-amb.xpm
--- tests/xrm/formula-amb.xpm (revision 0)
+++ tests/xrm/formula-amb.xpm (revision 0)
@@ -0,0 +1 @@
+formula amb = true;
Index: tests/xrm/rivf.xpm
--- tests/xrm/rivf.xpm (revision 77)
+++ tests/xrm/rivf.xpm (working copy)
@@ -32,7 +32,7 @@
// Whether (x, y) is valid, and broadcasts.
formula broadcasts (int x, int y) =
- if valid (x, y) then s[x][y] = BROADCASTS else false end;
+ valid (x, y) & s[x][y] = BROADCAST;
// Whether a neighbor of (x, y) is broadcasting.
formula ears (int x, int y) =
