[Projects] XRM 47: Fix array declarations.

https://svn.lrde.epita.fr/svn/xrm/trunk

Index: ChangeLog from SIGOURE Benoit sigoure.benoit@lrde.epita.fr

Fix array declarations.

* src/str/array-decl-desugar.str: Take the annotation "Generated" into account.. * src/str/xrm-to-prism.str: Call eval-meta-code before array-decl-desugar. * src/str/prism-desugar.str: Keep annotations when possible. * src/str/eval-meta-code.str: Mark generated code with the annotation "Generated". * src/str/signatures.str: New. * src/str/builtin-rand.str: Move signature to signatures.str. * src/str/collect-static-const-decl.str: Ditto. * src/str/desugar-array-access.str: Improve desugar-range (thanks to mefyl for his range-to-list). * tests/xrm/array-decl-with-meta-and-non-meta.xpm: New. * tests/prism/simple-label.pm: `label' is a reserved keyword in PRISM that's why this test was failing. * TODO: Bring up to date.

TODO | 45 +++++------------------- src/str/array-decl-desugar.str | 22 ++++++++++- src/str/builtin-rand.str | 5 -- src/str/collect-static-const-decl.str | 8 ---- src/str/desugar-array-access.str | 27 ++++++++------ src/str/eval-meta-code.str | 15 ++++++-- src/str/prism-desugar.str | 26 ++++++------- src/str/signatures.str | 24 ++++++++++++ src/str/xrm-to-prism.str | 12 ++++-- tests/prism/simple-label.pm | 2 - tests/xrm/array-decl-with-meta-and-non-meta.xpm | 3 + 11 files changed, 108 insertions(+), 81 deletions(-)

Index: src/str/array-decl-desugar.str --- src/str/array-decl-desugar.str (revision 46) +++ src/str/array-decl-desugar.str (working copy) @@ -13,10 +13,28 @@

/** ** Desugar dimensions in array declarations in explicit ranges. - ** eg: x[4] is desugared to x[0..3] + ** 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), prism-desugar;try(add-range)) + 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

Index: src/str/xrm-to-prism.str --- src/str/xrm-to-prism.str (revision 46) +++ src/str/xrm-to-prism.str (working copy) @@ -62,6 +62,14 @@ ; check-meta-vars ; notice-msg(|"xrm-to-prism: meta-vars checked")

+ /* unroll meta loops, eval meta if */ + ; eval-meta-code + ; notice-msg(|"xrm-to-prism: eval-meta-code done") + /*; notice-msg(|"debug: pretty printing current AST in ATerms to debug.aterm") + ; where(write-to => FILE(tmp-file) + ; <xtc-command(!"pp-aterm")> ["-i", tmp-file, "-o", "debug.aterm"] + )*/ + /* 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 @@ -73,10 +81,6 @@ ; topdown(try(array-decl-desugar)) ; notice-msg(|"xrm-to-prism: array declarations desugared")

- /* unroll meta loops, eval meta if */ - ; eval-meta-code - ; notice-msg(|"xrm-to-prism: eval-meta-code done") - /* flatten nested lists */ ; ModulesFile(id, flatten-list) ; ModulesFile(id, map(try(Module(id, flatten-list)))) Index: src/str/prism-desugar.str --- src/str/prism-desugar.str (revision 46) +++ src/str/prism-desugar.str (working copy) @@ -52,11 +52,11 @@

rules

- IntToDouble: Int(i) -> Double(i) + IntToDouble: Int(i){a*} -> Double(i){a*}

/** Transforms a round (or almost round) Double into an Int. */ SimplifyDoubles: - Double(d) -> Int(i) // eg: Double("41.9999999999999") -> Int("42") + Double(d){a*} -> Int(i){a*} // eg: Double("41.9999999999999") -> Int("42") where !d // "41.9999999999999" ; string-to-real // 4.199999999999990e+01 ; real-to-string(|6) // "42.000000" @@ -67,7 +67,7 @@

/** Round real numbers up to 6 digits and remove trailing zeros */ TruncateDouble: - Double(d) -> Double(d') + Double(d){a*} -> Double(d'){a*} where <rtrim-chars(?'0')> (<real-to-string(|6)> (<string-to-real> d)) => d'

rules @@ -138,16 +138,16 @@ rules

DesugarUnaryOps: - Plus(Int(i)) -> Int(i) + Plus(Int(i){a*}) -> Int(i){a*}

DesugarUnaryOps: - Plus(Double(i)) -> Double(i) + Plus(Double(i){a*}) -> Double(i){a*}

DesugarUnaryOps: - Minus(Int(i)) -> Int(j) where <mulS>(i, "-1") => j + Minus(Int(i){a*}) -> Int(j){a*} where <mulS>(i, "-1") => j

DesugarUnaryOps: - Minus(Double(i)) -> Double(j) where <mulS>(i, "-1") => j + Minus(Double(i){a*}) -> Double(j){a*} where <mulS>(i, "-1") => j

/* ** ## ==================== ## @@ -313,15 +313,15 @@

EvalMin: |[ func(min, a*) ]| -> |[ r ]| - where !a*;debug - ; map(\ Double(d) -> d );debug - ; minRL => r;debug + where !a* + ; map(\ Double(d) -> d ) + ; minRL => r

EvalMax: |[ func(max, a*) ]| -> |[ r ]| - where !a*;debug - ; map(\ Double(d) -> d );debug - ; maxRL => r;debug + where !a* + ; map(\ Double(d) -> d ) + ; maxRL => r

EvalFloor: |[ func(floor, d) ]| -> |[ r ]| where <floor>(d) => r Index: src/str/eval-meta-code.str --- src/str/eval-meta-code.str (revision 46) +++ 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. ** +** 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. @@ -13,7 +20,9 @@ ** mv .tmp eval-meta-code.str */ module eval-meta-code -imports ice +imports + ice + signatures

strategies

@@ -108,7 +117,7 @@ ///*DEBUG*/; printf(|" i = ", i) ///*DEBUG*/; say(!" <<< gen-meta-for -- propagating meta-var's value <<< ") ; !body - ; topdown(try(?meta-var; !Int(i))) + ; topdown(try(?meta-var; !Int(i){Generated("gen-meta-for")})) ///*DEBUG*/; debug ///*DEBUG*/; say(!" ~~~ gen-meta-for: now recursing") ; eval-meta-code => generated-code @@ -144,7 +153,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)) + ; topdown(try(?meta-var; !exp-to-replace{Generated("gen-meta-forin")})) ///*DEBUG*/; debug ///*DEBUG*/; say(!" ~~~ gen-meta-forin: now recursing") ; eval-meta-code => generated-code Index: src/str/signatures.str --- src/str/signatures.str (revision 0) +++ src/str/signatures.str (revision 0) @@ -0,0 +1,24 @@ +module signatures + +/** +** used in collect-static-const-decl.str +** `Type' is used to annotate the static const collected. +** This might be useful in the future. +*/ +signature constructors + Type : String -> Type + +/** +** used in builtin-rand.str +** node to replace in templates +*/ +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: src/str/builtin-rand.str --- src/str/builtin-rand.str (revision 46) +++ src/str/builtin-rand.str (working copy) @@ -12,6 +12,7 @@ ** which the same probability [1/(x-y+1)] */ module builtin-rand +imports signatures

rules

@@ -85,7 +86,3 @@ " arguments must be statically evaluable"]) ; debug ; <xtc-exit> 4 - -/* node to replace in templates */ -signature constructors - FIXME : FIXME Index: src/str/collect-static-const-decl.str --- src/str/collect-static-const-decl.str (revision 46) +++ src/str/collect-static-const-decl.str (working copy) @@ -4,13 +4,7 @@ ** (see prism-desugar) */ module collect-static-const-decl - -/** -** `Type' is used to annotate the static const collected. -** This might be useful in the future. -*/ -signature constructors - Type : String -> Type +imports signatures

strategies

Index: src/str/desugar-array-access.str --- src/str/desugar-array-access.str (revision 46) +++ src/str/desugar-array-access.str (working copy) @@ -121,24 +121,27 @@ ; if <ltS>(to, from) then invalid-range-in-array-access end - ; ![to] // start with the highest value - ; rec x( - {h,t: // restrict h and t to this scope - ?[h|t] - ; if not(<eq>(h, from)) then - ![<subtS>(h, "1") | <id>] - ; x - end - } - ) + ; <range-to-list> (<string-to-int> from, <string-to-int> to) + ; map(int-to-string) + +rules + + range-to-list: + (a, a) -> [a] + + range-to-list: + (a, b) -> [a | <range-to-list>(<addi>(a, 1), b)] + where <lt>(a, b) + +strategies

non-const-range-in-array-access = - err-msg(|"error: non constant term used in a range in an array access:") + err-msg(|"non constant term used in a range in an array access:") ; debug ; <xtc-exit> 2

invalid-range-in-array-access = - err-msg(|"error: invalid range in an array access [x..y] where x>y:") + err-msg(|"invalid range in an array access [x..y] where x>y:") ; debug ; <xtc-exit> 2

Index: tests/xrm/array-decl-with-meta-and-non-meta.xpm --- tests/xrm/array-decl-with-meta-and-non-meta.xpm (revision 0) +++ tests/xrm/array-decl-with-meta-and-non-meta.xpm (revision 0) @@ -0,0 +1,3 @@ +for i from 0 to 4 do + const int N[i][3] = 0; +end Index: tests/prism/simple-label.pm --- tests/prism/simple-label.pm (revision 46) +++ tests/prism/simple-label.pm (working copy) @@ -2,5 +2,5 @@

module dummy x: [0..1] init 1; - [label] x=2 -> x'=3; + [mylabel] x=2 -> x'=3; endmodule Index: TODO --- TODO (revision 46) +++ TODO (working copy) @@ -17,6 +17,7 @@

* Add more tests. Add tests which actually do check that the generated code is correct (which is not done ATM). + Factorize current tests with shell functions.

* How are handled mutually recursive static constant variables in PRISM? eg: const int x = y; @@ -29,8 +30,6 @@ 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.

- * Labels seems to be b0rken in parse-prism. - ## ---------- ## ## Extensions ## ## ---------- ## @@ -44,10 +43,6 @@ 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. - * 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.

@@ -70,7 +65,7 @@ * Add non-static array accesses (as suggested by Micha). For instance: module test x[4] : [0..5]; - i : [0..2]; + i : [0..3];

[] x[0..i]=0 -> ... // i can't be guessed at compile time endmodule @@ -83,7 +78,7 @@ 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)) -> ... + [] ((i<0 | 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 @@ -99,39 +94,12 @@

* Add parameterized formulas. (Pretty much like macro-functions in C)

- * Check why for i from -1 to -4 is not caught as an error. - * Add scopes for meta variables eg: for i ... do for i ... // `i' shadows its previous definition end end

- * It is currently impossible to declare something partially with meta-vars. - eg: for i from 0 to 3 do - const int N[i][5] = 0; - end - This is because array declarations are desugared down to simple - declarations before the meta-code has been evaluated in the pipeline. - On the other hand, if we evaluate the meta-code before desugaring array - declarations, we will end up with N_i_5 for all `i' and not with - N_i_0 ... N_i_5. Moreover, this will most likely fail because we have - generated something like: const int N[0][5] = 0; - const int N[1][5] = 0; - ... - const int N[2][5] = 0; - but how can we know that we should interpret this as: - const int N[0][0..5] = 0; - const int N[1][0..5] = 0; - ... - that is: the meta-var which has been expanded must no go further - expansions (eg: const int N[0..1][0..5] = 0;) We will also get an error - about declaring an array with a size of 0 element. - - Idea to work around the problem: tag the expanded meta-vars with an - annotation on the AST and handle the special case when desugaring array - declarations. - ## -------------- ## ## Desugarisation ## ## -------------- ## @@ -246,3 +214,10 @@

* Disallow associativity for the "=" and "!=" operators: won't fix (see src/syn/prism/README) + + * Labels seems to be b0rken in parse-prism. + => no it's just that "label" is a reserved keyword. + + * 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.