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

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

Remove an ambiguity in XRM Formulas.

* src/str/prism-desugar.str (SimplifyDoubles): Use simple pattern matching instead of congruence with inlined strategies. * src/str/collect-static-const-decl.str: Factor some code. * src/syn/xrm/XRM-Formula.sdf: Remove an ambiguity. * tests/xrm/amb-formula.xrm: New. This was ambiguous. * tests/xrm/rivf.xrm: Rename `power' to `POWER' and `lossage' to `LOSS'.

src/str/collect-static-const-decl.str | 27 +++++++++++++-------------- src/str/prism-desugar.str | 2 +- src/syn/xrm/XRM-Formula.sdf | 14 ++++++++++++-- tests/xrm/amb-formula.xrm | 3 +++ tests/xrm/rivf.xrm | 6 +++--- 5 files changed, 32 insertions(+), 20 deletions(-)

Index: src/str/prism-desugar.str --- src/str/prism-desugar.str (revision 84) +++ src/str/prism-desugar.str (working copy) @@ -66,7 +66,7 @@ ; string-to-real // 4.199999999999990e+01 ; real-to-string(|6) // "42.000000" ; split-at-dot // ("42", "000000") - ; (?i, ?decimals) // i="42", decimals="000000" + ; ?(i, decimals) // i="42", decimals="000000" // strcmp(decimals, "000000") == 0 ? id : fail ; !decimals => "000000"

Index: src/str/collect-static-const-decl.str --- src/str/collect-static-const-decl.str (revision 84) +++ src/str/collect-static-const-decl.str (working copy) @@ -11,31 +11,30 @@

strategies

- // const int - collect-static-const-decl = - ?ConstInt(idf@Identifier(_), value) - ; check-identifier-unicity(|idf) + register-static-const(|idf, value, type) = + check-identifier-unicity(|idf) + /* NOTE: We omitted ExpandPFormulas in the following attempt to simplify + * the value before storing it in the DR because it will expand the value + * forever if it contains call to recursive parameterized formula. + */ ; where(<innermost(ExpandStaticConsts + ExpandFormulas)> value => v' - ; !v'{Type("int")} => v) + ; !v'{Type(type)} => v) ; rules(ExpandStaticConsts: idf -> v)

+ // const int + collect-static-const-decl = + ?ConstInt(idf@Identifier(_), value) + ; register-static-const(|idf, value, "int")

// const double collect-static-const-decl = ?ConstDouble(idf@Identifier(_), value) - ; check-identifier-unicity(|idf) - ; where(<innermost(ExpandStaticConsts + ExpandFormulas)> value => v' - ; !v'{Type("double")} => v) - ; rules(ExpandStaticConsts: idf -> v) - + ; register-static-const(|idf, value, "double")

// const bool collect-static-const-decl = ?ConstBool(idf@Identifier(_), value) - ; check-identifier-unicity(|idf) - ; where(<innermost(ExpandStaticConsts + ExpandFormulas)> value => v' - ; !v'{Type("bool")} => v) - ; rules(ExpandStaticConsts: idf -> v) + ; register-static-const(|idf, value, "bool")

strategies

Index: src/syn/xrm/XRM-Formula.sdf --- src/syn/xrm/XRM-Formula.sdf (revision 84) +++ src/syn/xrm/XRM-Formula.sdf (working copy) @@ -21,10 +21,20 @@ -> FormulaDef {cons("FormulaDef")}

context-free syntax - "formula" Identifier "(" {Argument ","}* ")" "=" (Expression|Update) ";" + "formula" Identifier "(" {Argument ","}* ")" "=" Expression ";" -> FormulaDef {cons("PFormulaDef")} + "formula" Identifier "(" {Argument ","}* ")" "=" Update ";" + -> FormulaDef {cons("PFormulaDef"),prefer} "formula" Identifier "=" Update ";" - -> FormulaDef {cons("FormulaDef")} + -> FormulaDef {cons("FormulaDef"),prefer} + %% We use `prefer' here for the following reason: + %% In one single case, the above rules will lead to an ambiguity + %% formula amb = parameterized_formula(...); + %% Because of the nature of PFormulaCall (see XRM-Expression) which can + %% be either an Expression or an Update, sglr will create an amb node + %% with two identical choices. This is (AFAIK) the only case which will + %% lead to an ambiguity. Since both choices are identical, we can safely + %% remove the ambiguity using a dirty `prefer'.

sorts Argument context-free syntax Index: tests/xrm/amb-formula.xrm --- tests/xrm/amb-formula.xrm (revision 0) +++ tests/xrm/amb-formula.xrm (revision 0) @@ -0,0 +1,3 @@ +formula inc(int n) = n + 1; + +formula two = inc(1); Index: tests/xrm/rivf.xrm --- tests/xrm/rivf.xrm (revision 84) +++ tests/xrm/rivf.xrm (working copy) @@ -11,7 +11,7 @@ const int event_x = floor(width/2), event_y = floor(height/2);

// Initial energy, percentage of lost cells. -const int power = 15, lossage = 50; +const int POWER = 15, LOSS = 50;

// States. const int OFF = 0, SLEEP = 1, SENSE = 2, @@ -68,8 +68,8 @@ for y from 0 to height - 1 do module sensor[x][y]

- s[x][y] : [0..4] init (static_rand (0, 100) < lossage) ? OFF : SENSE; - b[x][y] : [0..power] init power; + s[x][y] : [0..4] init (static_rand (0, 100) < LOSS) ? OFF : SENSE; + b[x][y] : [0..POWER] init POWER;

[] s[x][y] = SENSE -> 1: transition (x, y, senses (x, y) ? BROADCAST : LISTEN, COST_SENSE); [] s[x][y] = LISTEN -> 1: transition (x, y, ears (x, y) ? BROADCAST : SLEEP, COST_LISTEN);