https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit@lrde.epita.fr> Add array declarations (sugar). It is now possible to declare arrays such as: b[4][3] : bool; Multi-dimensional arrays are correctly handled. * src/str/array-decl-desugar.meta: New. * src/str/array-decl-desugar.str: New. * src/str/xrm-to-prism.str: Use array-decl-desugar. * src/syn/xrm/XRM-Command.sdf: "Dirty" hack to make it work. * tests/xrm/globals.xpm: New. * tests/xrm/array-decl_dim_exp.xpm: New. * tests/xrm/labels.xpm: New. * tests/xrm/array-decl_1d.xpm: New. * tests/xrm/array-decl_2d.xpm: New. * tests/xrm/array-decl_3d.xpm: New. * tests/prism/simple-label.pm: New. * TODO: Add many more ideas from Micha. TODO | 63 ++++++++++++++++++++++------ src/str/array-decl-desugar.meta | 1 src/str/array-decl-desugar.str | 87 +++++++++++++++++++++++++++++++++++++++ src/str/xrm-to-prism.str | 9 +++- src/syn/xrm/XRM-Command.sdf | 4 + tests/prism/simple-label.pm | 6 ++ tests/xrm/array-decl_1d.xpm | 8 +++ tests/xrm/array-decl_2d.xpm | 10 ++++ tests/xrm/array-decl_3d.xpm | 8 +++ tests/xrm/array-decl_dim_exp.xpm | 5 ++ tests/xrm/globals.xpm | 3 + tests/xrm/labels.xpm | 10 ++++ 12 files changed, 199 insertions(+), 15 deletions(-) Index: src/str/array-decl-desugar.meta --- src/str/array-decl-desugar.meta (revision 0) +++ src/str/array-decl-desugar.meta (revision 0) @@ -0,0 +1 @@ +Meta([Syntax("StrategoXRM")]) Index: src/str/array-decl-desugar.str --- src/str/array-decl-desugar.str (revision 0) +++ src/str/array-decl-desugar.str (revision 0) @@ -0,0 +1,87 @@ +/** +** This sub-module is used to desugar multi-dimension array declarations. +** Each dimension will by handled by a meta for loop unrolled later. +** So if we have a N-dimensions array declaration, it will be rewritten as +** N nested for loops. +** +** eg: x[4][3] : [1..2]; +** for meta_i_0 from 0 to 4 do +** for meta_i_1 from 0 to 3 do +** x[meta_i_0][meta_i_1] : [1..2]; +** end +** end +** Since this will unrolled and flattened later in by the submodule evaluating +** meta-code we will end up having all the x_i_j variables declared. +** +** NOTE: Each dimension is handled separately and recursion is not handled by +** array-decl-desugar. The rule must be called in a topdown(try(..)) in order +** to naturally traverse generated code and thus, handle all dimensions. +*/ +module array-decl-desugar + +strategies + + /** + ** Patch the list of dimensions with the meta-var used in the meta for loop. + ** Basically this strategy generates a new meta-var used as the iterator + ** in the meta-for loop and updates the dimensions of the declared array. + ** The dimension updated is the first one matching Int(_) + ** + ** eg: x[4][3] : bool; + ** => BoolDecNoInit(Identifier("x"), + ** ArrayAccess( [Identifier("meta_i_0"), Int(3)] )) + ** will needs to be transformed as: + ** BoolDecNoInit(Identifier("x"), + ** ArrayAccess( [Identifier("meta_i_0"), + ** Identifier("meta_i_1")] )) + ** @type List(dims) -> List(meta-var, current-dim, List(all-dims-patched)) + */ + update-dimensions(|dims) = + <newname> "__meta_i" => x + + /* Ensure that the list of dimensions is desugared */ + ; <prism-desugar> dims => dims' + + /* 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) + + /* 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>) + +rules +// FIXME: Try to figure out why concrete syntax fails to work here + + array-decl-desugar: + IntDecNoInit(ArrayAccess(idf, dims), low, up) + //-> |[ for x from 0 to ~dim step 1 do x[i] : [~low..~up]; end ]| + -> MetaFor(Identifier(x), Int("0"), current-dim', Int("1"), + [ IntDecNoInit(ArrayAccess(idf, dims'), low, up) ]) + where update-dimensions(|dims) => (x, current-dim', dims') + + array-decl-desugar: + IntDec(ArrayAccess(idf, dims), low, up, value) + //-> |[ for x from 0 to ~dim step 1 do + // x[i] : [~low..~up] init ~value; + // end ]| + -> MetaFor(Identifier(x), Int("0"), current-dim', Int("1"), + [ 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 ]| + -> MetaFor(Identifier(x), Int("0"), current-dim', Int("1"), + [ BoolDecNoInit(ArrayAccess(idf, dims')) ]) + where update-dimensions(|dims) => (x, current-dim', dims') + + array-decl-desugar: + BoolDec(ArrayAccess(idf, dims), value) + //-> |[ for x from 0 to ~dim step 1 do x[i] : bool init ~value; end ]| + -> MetaFor(Identifier(x), Int("0"), current-dim', Int("1"), + [ BoolDec(ArrayAccess(idf, dims'), value) ]) + where update-dimensions(|dims) => (x, current-dim', dims') Index: src/str/xrm-to-prism.str --- src/str/xrm-to-prism.str (revision 30) +++ src/str/xrm-to-prism.str (working copy) @@ -9,12 +9,19 @@ desugar-array-accesses check-meta-vars eval-meta-code + array-decl-desugar strategies xrm-to-prism = /* remove XRM sugar, normalize some nodes */ - topdown(try(xrm-to-prism-desugar)) + innermost(xrm-to-prism-desugar) + + /* 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)) /* Check that meta vars are always defined in the current scope when used * and that they are not redefined twice in the same scope */ Index: src/syn/xrm/XRM-Command.sdf --- src/syn/xrm/XRM-Command.sdf (revision 30) +++ src/syn/xrm/XRM-Command.sdf (working copy) @@ -8,4 +8,6 @@ %% Command ::= "[" ArrayAccess "]" Expression "->" Updates ";" context-free syntax - "[" ArrayAccess "]" Expression "->" Updates ";" -> Command {cons("Command")} + "[" ArrayAccess? "]" Expression "->" Updates ";" + -> Command {prefer,cons("Command")} + %% FIXME: dirty hack: ^^^^^^ Index: tests/xrm/globals.xpm --- tests/xrm/globals.xpm (revision 0) +++ tests/xrm/globals.xpm (revision 0) @@ -0,0 +1,3 @@ +for i from 0 to 4 do + global x[i] : bool; +end Index: tests/xrm/array-decl_dim_exp.xpm --- tests/xrm/array-decl_dim_exp.xpm (revision 0) +++ tests/xrm/array-decl_dim_exp.xpm (revision 0) @@ -0,0 +1,5 @@ +// should be equivalent as declaring x[8] + +module arrays + x[4+4] : [0..42]; +endmodule Index: tests/xrm/labels.xpm --- tests/xrm/labels.xpm (revision 0) +++ tests/xrm/labels.xpm (revision 0) @@ -0,0 +1,10 @@ +probabilistic + +for i from 0 to 4 do + module dummy[i] + x[i] : [0..1] init i; + for j from 5 to 10 do + [testlabel[j]] x[i]=j -> x[i]'=j+1; + end + endmodule +end Index: tests/xrm/array-decl_1d.xpm --- tests/xrm/array-decl_1d.xpm (revision 0) +++ tests/xrm/array-decl_1d.xpm (revision 0) @@ -0,0 +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; +endmodule Index: tests/xrm/array-decl_2d.xpm --- tests/xrm/array-decl_2d.xpm (revision 0) +++ tests/xrm/array-decl_2d.xpm (revision 0) @@ -0,0 +1,10 @@ +// should be expanded in x_0_0 x_1_0 x_2_0 x_3_0 +// x_0_1 x_1_1 x_2_1 x_3_1 +// 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; +endmodule Index: tests/xrm/array-decl_3d.xpm --- tests/xrm/array-decl_3d.xpm (revision 0) +++ tests/xrm/array-decl_3d.xpm (revision 0) @@ -0,0 +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; +endmodule Index: tests/prism/simple-label.pm --- tests/prism/simple-label.pm (revision 0) +++ tests/prism/simple-label.pm (revision 0) @@ -0,0 +1,6 @@ +probabilistic + +module dummy + x: [0..1] init 1; + [label] x=2 -> x'=3; +endmodule Index: TODO --- TODO (revision 30) +++ TODO (working copy) @@ -14,25 +14,30 @@ * Write some sort of formal descriptions of the extensions offered. + * Add more tests. Add tests which actually do check that the generated code + is correct (which is not done ATM). + ## ---------- ## ## Extensions ## ## ---------- ## * Add the following at the meta-level: - Let's have the possibility to generate other ModulesFileSection such as: - o Formula - o Constant - o Global - o RenamedModule - o SystemComp - o RewardStruct - - * Add arrays (sugar). module varArrays <=> module varArrays - module varArrays => x_0 : [0..3]; <=> for a_0 from 0 to 4 do - x[4] : [0..3]; => x_1 : [0..3]; <=> x[i] : [0..3]; - [] x[0]=0 -> ... => ... <=> end - endmodule => [] x_0=0 -> ... <=> [] x_0=0 -> ... - => endmodule <=> endmodule + o Formula // add it in the grammar. should be + // automagically handled + o Constant // ditto + o Global // done (automagically handled) + o RenamedModule // need to be investigated + o RewardStruct // ditto + o SystemComp // b0rken anyway + + * 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. @@ -52,6 +57,31 @@ 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 + x[4] : [0..5]; + i : [0..2]; + + [] x[0..i]=0 -> ... // i can't be guessed at compile time + endmodule + + Translate this with something like: + module test + x_0 : [0..5]; + x_1 : [0..5]; + x_2 : [0..5]; + x_3 : [0..5]; + i : [0..3]; + + [] x_0=0 & ((i<1 | x_1=0) & (i<2 | x_2=0) & (i<3 | x_3=0)) -> ... + endmodule + + /!\ This (might) require that we add another pass to collect the generated + variables and their type + domain and might be quite challenging to + handle. ## -------------- ## ## Desugarisation ## @@ -122,3 +152,10 @@ - In between modules (that is, where we can expect a ModulesFileSection) - In between commands (that is where we can expect a Declaration or a Command) + + * Add arrays (sugar). module varArrays <=> module varArrays + module varArrays => x_0 : [0..3]; <=> for a_0 from 0 to 4 do + x[4] : [0..3]; => x_1 : [0..3]; <=> x[a_0] : [0..3]; + [] x[0]=0 -> ... => ... <=> end + endmodule => [] x_0=0 -> ... <=> [] x_0=0 -> ... + => endmodule <=> endmodule