[Projects] XRM 27: Add meta code evaluation [debug version].

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit &lt;sigoure.benoit(a)lrde.epita.fr&gt; Add meta code evaluation [debug version]. This is the first working version with complete meta code evaluation. For loops and Ifs are evaluated at the meta-level and code is generated by xrm-front accordingly. /!\ This version contains debugging messages to be removed. The code also needs to be cleaned up and re-organized a bit. The first Release Candidate is on its way! \o/ * src/lib/xrm/pp/xrm-module.str: Remove MetaModule boxing. * src/lib/xrm/pp/xrm-expression.str: Remove PreIncr and PreDecr boxing. * src/lib/xrm/pp/xrm-arrays.str: Add ArrayAccessPrime boxing. * src/str/xrm-front.str: Add a FIXME. To be removed very soon. * src/str/xrm-to-prism.str: Add meta code evaluation. * src/str/prism-desugar.str: Add some FIXMEs and some new constant expression evaluation. * src/syn/xrm/XRM-Arrays.sdf: Add ArrayAccessPrime (eg: x[i]'). * src/syn/xrm/XRM-StartSymbols.sdf: Remove IdentifierPrime (useless). * src/syn/prism/PRISM-StartSymbols.sdf: Ditto. * src/syn/xrm/XRM-StaticIf.sdf: The then-part and else-part of an If may now be empty. * src/syn/xrm/StrategoXRM.sdf: Add static fors. * src/syn/xrm/XRM-Literals.sdf: Add a comment about SDF kernel syntax. * src/syn/xrm/XRM-MetaVars.sdf: Add new meta-vars for XRM. * src/syn/xrm/XRM-Update.sdf: New. Add updates using ArrayAccessPrime. * src/syn/xrm/XRM-Main.sdf: Import XRM-Declaration and XRM-Update. * src/syn/xrm/XRM-Declaration.sdf: New. Add declarations of ArrayAccessPrime. (eg: declarations for variables named x[i]) * src/syn/xrm/XRM-Module.sdf: Change the MetaModule constructor in Module. The new constructor was useless. * src/syn/xrm/XRM-Expression.sdf: Remove PreIncr and PreDecr (eg: ++x and --x). This was wrong and useless and used only for testing. * tests/xrm/inner-static-if.xpm: Remove the FIXME. * tests/xrm/inner-static-for-step.xpm: Ditto. * tests/xrm/outer-static-if.xpm: Ditto. * tests/xrm/outer-static-for-step.xpm: Ditto. * tests/xrm/static-if.xpm: Ditto. * tests/xrm/inner-static-for.xpm: Ditto. * tests/xrm/static-for-step.xpm: Ditto. * tests/xrm/outer-static-for.xpm: Ditto. * tests/xrm/simple_01.xpm: Ditto. * tests/xrm/static-for.xpm: Ditto. src/lib/xrm/pp/xrm-arrays.str | 6 src/lib/xrm/pp/xrm-expression.str | 6 src/lib/xrm/pp/xrm-module.str | 8 - src/str/prism-desugar.str | 47 +++++- src/str/xrm-front.str | 2 src/str/xrm-to-prism.str | 268 +++++++++++++++++++++++++++++++++-- src/syn/prism/PRISM-StartSymbols.sdf | 1 src/syn/xrm/StrategoXRM.sdf | 2 src/syn/xrm/XRM-Arrays.sdf | 9 + src/syn/xrm/XRM-Declaration.sdf | 22 ++ src/syn/xrm/XRM-Expression.sdf | 20 -- src/syn/xrm/XRM-Literals.sdf | 2 src/syn/xrm/XRM-Main.sdf | 2 src/syn/xrm/XRM-MetaVars.sdf | 4 src/syn/xrm/XRM-Module.sdf | 2 src/syn/xrm/XRM-StartSymbols.sdf | 1 src/syn/xrm/XRM-StaticIf.sdf | 12 - src/syn/xrm/XRM-Update.sdf | 22 ++ tests/xrm/inner-static-for-step.xpm | 6 tests/xrm/inner-static-for.xpm | 6 tests/xrm/inner-static-if.xpm | 8 - tests/xrm/outer-static-for-step.xpm | 4 tests/xrm/outer-static-for.xpm | 4 tests/xrm/outer-static-if.xpm | 8 - tests/xrm/simple_01.xpm | 3 tests/xrm/static-for-step.xpm | 8 - tests/xrm/static-for.xpm | 8 - tests/xrm/static-if.xpm | 14 - 28 files changed, 408 insertions(+), 97 deletions(-) Index: src/lib/xrm/pp/xrm-module.str --- src/lib/xrm/pp/xrm-module.str (revision 26) +++ src/lib/xrm/pp/xrm-module.str (working copy) @@ -10,11 +10,3 @@ ] KW["endmodule"] ] ]| - - prism-to-box: - MetaModule(array-access, dec-or-cmd-list) - -> box |[ V[ V is=2 [ H hs=1 [KW["module"] ~array-access ] - ~*dec-or-cmd-list - ] - KW["endmodule"] - ] ]| Index: src/lib/xrm/pp/xrm-expression.str --- src/lib/xrm/pp/xrm-expression.str (revision 26) +++ src/lib/xrm/pp/xrm-expression.str (working copy) @@ -3,12 +3,6 @@ rules prism-to-box: - PreIncr(exp) -> H hs=0 [ MATH["++"] ~exp ] - - prism-to-box: - PreDecr(exp) -> H hs=0 [ MATH["--"] ~exp ] - - prism-to-box: RightShift(lhs, rhs) -> H hs=1 [~lhs MATH[">>"] ~rhs] prism-to-box: Index: src/lib/xrm/pp/xrm-arrays.str --- src/lib/xrm/pp/xrm-arrays.str (revision 26) +++ src/lib/xrm/pp/xrm-arrays.str (working copy) @@ -7,3 +7,9 @@ ArrayAccess(idf, subscripts) -> H hs=0 [ ~idf ~*subscripts-impl ] where <mapconcat(\ x -> [S("["), x, S("]")] \)> subscripts => subscripts-impl + + // Identifier ArraySubscript+ "'" -> ArrayAccessPrime + prism-to-box: + ArrayAccessPrime(idf, subscripts) -> H hs=0 [ ~idf ~*subscripts-impl "'" ] + where + <mapconcat(\ x -> [S("["), x, S("]")] \)> subscripts => subscripts-impl Index: src/str/xrm-front.str --- src/str/xrm-front.str (revision 26) +++ src/str/xrm-front.str (working copy) @@ -23,7 +23,7 @@ ; xtc-transform(!"parse-xrm", // parse input (returns a FILE) !["-b", "--preserve-positions" | <pass-verbose>()]) ; read-from // read parsed input - ; strip-annos + ; /*FIXME*/strip-annos // FIXME: remove this line!!!!!!!!!!!!!!!!!!!!!!!!!! ; xrm-front-pipeline // transformations ; if not(must-keep-attributes) then strip-annos end ; if <get-config> "-b" then Index: src/str/xrm-to-prism.str --- src/str/xrm-to-prism.str (revision 26) +++ src/str/xrm-to-prism.str (working copy) @@ -1,55 +1,293 @@ module xrm-to-prism -imports XRM +imports + XRM + prism-desugar strategies xrm-to-prism = + /* remove XRM sugar, normalize some nodes */ topdown(try(xrm-to-prism-desugar)) - ; id // unroll static for loops here - ; topdown(try(reorder-module-contents)) + + /* Check that meta vars are always defined in the current scope when used + * and that they are not redefined twice in the same scope */ + ; check-meta-vars + + /* unroll static loops, eval static if */ + ; eval-meta-code + + /* flatten nested lists */ + ; ModulesFile(id, flatten-list) + ; ModulesFile(id, map(try(Module(id, flatten-list)))) + + /* remove array accesses: x[i] -> x_i */ + ; topdown(try(remove-array-accesses)) + + /* re-order modules so that all declarations appear before commands */ + ; ModulesFile(id, map(try(reorder-module-contents))) rules xrm-to-prism-desugar: - // PreIncr(exp) -> Eq(exp, [Plus(exp, Int("1"))]) - |[ ++e ]| -> |[ e = e + 1 ]| + |[ e1 >> e2 ]| -> |[ e1 / func(pow, 2, e2) ]| + + xrm-to-prism-desugar: + |[ e1 << e2 ]| -> |[ e1 * func(pow, 2, e2) ]| xrm-to-prism-desugar: - // PreDecr(exp) -> Eq(exp, [Minus(exp, Int("1"))]) - |[ --e ]| -> |[ e = e - 1 ]| + OuterStaticFor(identifier, from, to, body) + -> OuterStaticFor(identifier, from, to, Int("1"), body) xrm-to-prism-desugar: - // RightShift(lhs, rhs) -> Div(lhs, rhs) - |[ e1 >> e2 ]| -> |[ e1 / func(pow, 2, e2) ]| + InnerStaticFor(identifier, from, to, body) + -> InnerStaticFor(identifier, from, to, Int("1"), body) xrm-to-prism-desugar: - // LeftShift(lhs, rhs) -> Div(lhs, rhs) - |[ e1 << e2 ]| -> |[ e1 * func(pow, 2, e2) ]| + //|[ if e then m* end ]| -> |[ if e then m* else end ]| + OuterStaticIf(e, m*) -> OuterStaticIf(e, m*, []) + + xrm-to-prism-desugar: + //|[ if e then s* end ]| -> |[ if e then s* else end ]| + InnerStaticIf(e, s*) -> InnerStaticIf(e, s*, []) + +rules + + /** + ** Transform an array access into an identifier (eg: x[i] -> x_i) + */ + remove-array-accesses: + ArrayAccess(Identifier(idf), access-list) -> Identifier(idf') + where flatten-access-list(|idf, access-list) => idf' + + remove-array-accesses: + ArrayAccessPrime(Identifier(idf), access-list) -> IdentifierPrime(idf') + where flatten-access-list(|idf, access-list) => idf' + +strategies + + /** + ** @internal + ** Transform an access list (in array accesses) into a flat variable name + ** eg: flatten-access-list(|"x", [Int("1"), Int("2")]) -> "x_1_2" + ** NOTE: The access list can contain expressions as long as it possible to + ** evaluate them down to a constant positive Int() value. + ** + ** @param idf String + ** @param access-list List of Int() + */ + flatten-access-list(|idf, access-list) = + /* eval static expressions in the access-list + * eg: Plus(Int("1"), Int("2")) -> Int("3") */ + <prism-desugar> access-list + + /* Now the access must only contain a list of Int: [Int("1"), Int("2"), ..] + * So we can remove the Int() constructor. */ + ; map(\ Int(i) -> i \ <+ invalid-array-access) + + /* Now we have a list of strings such as: ["1", "2", ...] + * Check that the list only contains positive integers as strings */ + ; try(map(string-to-int; neg; invalid-array-access)) + + /* Insert underscores between each integer */ + ; separate-by(|"_") + + /* Produce the final identifier: eg: idf_1_2 */ + ; <concat-strings> [idf, "_" | <id>] + + /** + ** @internal + ** Report invalid array accesses. + */ + invalid-array-access = + if ?Identifier(i) then + fatal-err-msg(|<concat-strings>["internal compiler error: ", + "undeclared meta-variable: ", i, + " (should have been detected earlier!)"]) + else + if (is-int; neg) then + err-msg(|"error: negative array subscript detected:") + ; debug + ; <xtc-exit> 2 + else + err-msg(|"error: non constant term in array access:") + ; debug + ; <xtc-exit> 2 + end + end strategies - // re-order modules so that the declarations are separated from the - // commands, as required by the original PRISM grammar + /** Re-order modules so that the declarations are separated from the + ** commands, as required by the original PRISM grammar. + */ reorder-module-contents = ?Module(name, _) ; {| DeclarationList, CommandList: Module(id, map(add-command <+ add-declaration)) ; where( bagof-DeclarationList + ; reverse ; ?dec-list ; bagof-CommandList + ; reverse ; ?cmd-list ) |} ; !Module(name, dec-list, cmd-list) - // if the current term is a Command, add it in the CommandList DR + /** if the current term is a Command, add it in the CommandList DR */ add-command = ?Command(_, _, _) ; ?current-term ; rules(CommandList:+ _ -> current-term) - // if the current term is not a Command, add it in the DeclarationList DR + /** if the current term is not a Command, add it in the DeclarationList DR */ add-declaration = ?current-term ; rules(DeclarationList:+ _ -> current-term) + +strategies + + check-meta-vars = + check-static-for + <+ check-static-if + <+ ArrayAccess(id, check-all-identifers-are-meta-vars) + <+ ArrayAccessPrime(id, check-all-identifers-are-meta-vars) + <+ all(check-meta-vars) + + check-static-for = + (?OuterStaticFor(new-meta-var, from, to, step, body) + <+ ?InnerStaticFor(new-meta-var, from, to, step, body)) + ; where({| MetaVars: + <add-meta-var> new-meta-var + ; <check-all-identifers-are-meta-vars> from + ; <check-all-identifers-are-meta-vars> to + ; <check-all-identifers-are-meta-vars> step + ; <check-meta-vars> body + |}) + + check-static-if = + (?OuterStaticIf(condition, then-part, else-part) + <+ ?InnerStaticIf(condition, then-part, else-part)) + ; where( + <check-all-identifers-are-meta-vars> condition + ; <check-meta-vars> then-part + ; <check-meta-vars> else-part + ) + + check-all-identifers-are-meta-vars = + (?Identifier(_); check-meta-var-declared) + <+ all(check-all-identifers-are-meta-vars) + + add-meta-var = + check-meta-var-unicity + ; ?meta-var + ; rules(MetaVars: meta-var) + + check-meta-var-declared = + ?Identifier(idf) + ; if not(<MetaVars> Identifier(idf)) then + err-msg(|<concat-strings>["undeclared meta-var: ", idf]) + ; <xtc-exit> 2 + end + + check-meta-var-unicity = + ?Identifier(idf) + ; if <MetaVars> Identifier(idf) then + err-msg(|<concat-strings>["meta-var already defined: ", idf]) + ; <xtc-exit> 2 + end + +strategies + + eval-meta-code = + eval-meta-if + <+ unroll-static-loops + <+ all(eval-meta-code) + +strategies + + eval-meta-if = + (?OuterStaticIf(condition, then-part, else-part) + <+ ?InnerStaticIf(condition, then-part, else-part)) + /*DEBUG*/; say(!" @@@ eval-meta-if: starting:") + /*DEBUG*/; printf(|" condition = ", condition) + ; where(<prism-desugar> condition => condition-value) + /*DEBUG*/; printf(|" condition-value = ", condition-value) + ; if !condition-value => True() then + <eval-meta-code> then-part + else + if !condition-value => False() then + <eval-meta-code> else-part + else + fatal-err-msg(|"internal compiler error in eval-meta-if") + end + end + +strategies + + unroll-static-loops = + (?OuterStaticFor(meta-var, Int(from), Int(to), Int(step), body) + <+ ?InnerStaticFor(meta-var, Int(from), Int(to), Int(step), body)) + ; where(check-loop-validity(|meta-var, from, to)) + ; {| MetaCode: + /*DEBUG*/say(!" @@@ unroll-static-loops: starting:") + /*DEBUG*/; printf(|" meta-var = ", meta-var) + /*DEBUG*/; printf(|" from = ", from) + /*DEBUG*/; printf(|" to = ", to) + ; where(<check-meta-var-unicity> meta-var) + ; for-loop(gen-meta-code | from, to, step, []) + /*DEBUG*/; say(!" ~~~ unroll-static-loops: before bagof-MetaModule") + /*DEBUG*/; debug + ; bagof-MetaCode + ; reverse + /*DEBUG*/; say(!" ~~~ unroll-static-loops: after bagof-MetaModule") + /*DEBUG*/; debug + |} + + check-loop-validity(|meta-var, from, to) = + if <gtS>(from, to) then + !meta-var => Identifier(idf) + ; err-msg(|<concat-strings>["bad `for' loop on the meta-var ", + idf, " starts at ", from, + " which is less than ", to]) + ; <xtc-exit> 2 + end + +strategies + + gen-meta-code(|i, args) = + /*DEBUG*/say(!" ### gen-meta-code starting"); debug; + (?for-kind#([meta-var, _, _, _, body]) <+ fatal-err-msg(|"ICE!")) + /*DEBUG*/; say(!" >>> gen-meta-code -- start -- current term >>>") + /*DEBUG*/; debug + /*DEBUG*/; say(!" >>> gen-meta-code -- start -- iterator >>>") + /*DEBUG*/; printf(|" meta-var = ", meta-var) + /*DEBUG*/; printf(|" i = ", i) + /*DEBUG*/; say(!" <<< gen-meta-code -- propagating meta-var's value <<< ") + ; !body + ; topdown(try(?meta-var; !Int(i))) + /*DEBUG*/; debug + /*DEBUG*/; say(!" ~~~ gen-meta-code: now recursing") + ; eval-meta-code => generated-code + ; rules(MetaCode:+ _ -> generated-code) + /*DEBUG*/; say(!" ~~~ gen-meta-code: recursion finished, final result:") + /*DEBUG*/; debug + /*DEBUG*/; say(!" <<<<<<<<<<<<<<<<< gen-meta-code <<<<<<<<<<<<<<<<< ") + +strategies + /*DEBUG*/printf(|str, term) = where(<fprintnl> (stderr, [str, term])) + + /** + * for-loop(s | low, up, step, data) + * <=> in C: + * for(i = low; i <= up; i += step) + * s(|i, data) + */ + for-loop(s : Int * a * List(a) -> a | low, up, step, data) = + /*DEBUG*/where(say(!"--- for-loop ---"); printf(|" i = ", low) + /*DEBUG*/ ; printf(|" up = ", up); printf(|" step = ", step)); + if <leqS>(low, up) then + where(s(|low, data)) + ; for-loop(s | <addS>(low, step), up, step, data) + end Index: src/str/prism-desugar.str --- src/str/prism-desugar.str (revision 26) +++ src/str/prism-desugar.str (working copy) @@ -21,6 +21,7 @@ <+ AddZero <+ MulOne <+ MulZero <+ DivOne <+ catch-div-by-zero <+ EvalPlus <+ EvalMinus <+ EvalMul <+ EvalDiv <+ EvalLt <+ EvalLtEq <+ EvalGt <+ EvalGtEq <+ EvalEq <+ EvalNeq + <+ EvalAnd <+ EvalOr ) ; topdown(try(SimplifyDoubles <+ TruncateDouble)) @@ -37,7 +38,7 @@ ; split-at-dot // ("42", "000000") ; (?i, ?decimals) // i="42", decimals="000000" // strcmp(decimals, "000000") == 0 ? id : fail - ; <strcmp> (<explode-string> decimals, <explode-string> "000000") => 0 + ; !decimals => "000000" // Round real numbers up to 6 digits and remove trailing zeros TruncateDouble: @@ -64,8 +65,16 @@ compare(s) = if s then !True() else !False() end catch-div-by-zero = - ?|[ e / 0D ]|; debug; fatal-err-msg(|"Division by zero detected") + ?|[ e / 0D ]| + ; err-msg(|"Division by zero detected:") + ; debug + ; <xtc-exit> 3 +/** +** Remember: we are working exclusively with Double! The trailing 'D' at +** the end of an integer literal make it a Double() and not an Int() [This +** is one of the minor extensions of XRM] +*/ rules AddZero: @@ -86,6 +95,8 @@ DivOne: |[ e / 1D ]| -> |[ e ]| +rules + EvalPlus: |[ d1 + d2 ]| -> |[ r ]| where <addR>(d1, d2) => r @@ -110,8 +121,40 @@ EvalGtEq: |[ d1 >= d2 ]| -> <compare(geqR)>(d1, d2) + /* FIXME: The following rules could be generalized + We need to check whether d1 appears in the list at the RHS */ EvalEq: |[ d1 = d2 ]| -> <compare(real-eq)>(d1, d2) + /* FIXME: Same thing as EvalEq */ EvalNeq: |[ d1 != d2 ]| -> <compare(not(real-eq))>(d1, d2) + +rules +/* FIXME: Can we optimize this in a single rule? + Since the optimization would decrease readability, + is it worth it? + eg: + EvalAnd: + And(x, y) -> True() where x => True(); y => True() + EvalAnd: + And(x, y) -> False() where x => False() + y => False() +*/ + + EvalAnd: + |[ true & true ]| -> |[ true ]| + EvalAnd: + |[ true & false ]| -> |[ false ]| + EvalAnd: + |[ false & true ]| -> |[ false ]| + EvalAnd: + |[ false & false ]| -> |[ false ]| + + EvalOr: + |[ true | true ]| -> |[ true ]| + EvalOr: + |[ true | false ]| -> |[ true ]| + EvalOr: + |[ false | true ]| -> |[ true ]| + EvalOr: + |[ false | false ]| -> |[ false ]| Index: src/syn/xrm/XRM-Arrays.sdf --- src/syn/xrm/XRM-Arrays.sdf (revision 26) +++ src/syn/xrm/XRM-Arrays.sdf (working copy) @@ -7,13 +7,20 @@ %% ArrayAccess ::= Identifier ArraySubscript {ArraySubscript} %% %% ArraySubscript ::= "[" Identifier "]" + %% + %% ArrayAccessPrime ::= Identifier ArraySubscript+ "'" sorts ArrayAccess ArraySubscript context-free syntax Identifier ArraySubscript+ -> ArrayAccess {cons("ArrayAccess")} - "[" Identifier "]" -> ArraySubscript {bracket} + "[" Expression "]" -> ArraySubscript {bracket} %% Note: why use bracket here? %% This is a work around. In SDF, if a production contains literals, %% a constructor is required. With brackets, we specify that literals %% are allowed there, however this does not create a node in the AST. + + sorts ArrayAccessPrime + context-free syntax + Identifier ArraySubscript+ "'" + -> ArrayAccessPrime {cons("ArrayAccessPrime")} Index: src/syn/xrm/XRM-StartSymbols.sdf --- src/syn/xrm/XRM-StartSymbols.sdf (revision 26) +++ src/syn/xrm/XRM-StartSymbols.sdf (working copy) @@ -14,7 +14,6 @@ Expression Updates Identifier - IdentifierPrime SystemComp RewardStruct ModulesFileSection Index: src/syn/xrm/XRM-StaticIf.sdf --- src/syn/xrm/XRM-StaticIf.sdf (revision 26) +++ src/syn/xrm/XRM-StaticIf.sdf (working copy) @@ -24,24 +24,24 @@ context-free syntax %% if-then at top-level - "if" Expression "then" ModulesFileSection+ "end" + "if" Expression "then" ModulesFileSection* "end" -> ModulesFileSection {cons("OuterStaticIf")} %% if-then-else at top-level "if" Expression "then" - ModulesFileSection+ + ModulesFileSection* "else" - ModulesFileSection+ + ModulesFileSection* "end" -> ModulesFileSection {cons("OuterStaticIf")} context-free syntax %% if-then within modules - "if" Expression "then" DeclarationOrCommand+ "end" + "if" Expression "then" DeclarationOrCommand* "end" -> DeclarationOrCommand {cons("InnerStaticIf")} %% if-then-else within modules "if" Expression "then" - DeclarationOrCommand+ + DeclarationOrCommand* "else" - DeclarationOrCommand+ + DeclarationOrCommand* "end" -> DeclarationOrCommand {cons("InnerStaticIf")} Index: src/syn/xrm/StrategoXRM.sdf --- src/syn/xrm/StrategoXRM.sdf (revision 26) +++ src/syn/xrm/StrategoXRM.sdf (working copy) @@ -17,6 +17,8 @@ "|[" Expression "]|" -> StrategoTerm {prefer,cons("ToTerm")} "|[" Declaration "]|" -> StrategoTerm {prefer,cons("ToTerm")} "|[" Command "]|" -> StrategoTerm {prefer,cons("ToTerm")} + "|[" OuterStaticFor "]|" -> StrategoTerm {prefer,cons("ToTerm")} + "|[" InnerStaticFor "]|" -> StrategoTerm {prefer,cons("ToTerm")} context-free syntax Index: src/syn/xrm/XRM-Literals.sdf --- src/syn/xrm/XRM-Literals.sdf (revision 26) +++ src/syn/xrm/XRM-Literals.sdf (working copy) @@ -2,6 +2,8 @@ imports PRISM-to-XRM exports + %% NOTES: This block is a simple "syntax" block and contains SDF kernel + %% syntax. In fact everything is syntax <LInt-LEX> "d" -> <LDouble-CF> {bracket} <LInt-LEX> "D" -> <LDouble-CF> {bracket} Index: src/syn/xrm/XRM-MetaVars.sdf --- src/syn/xrm/XRM-MetaVars.sdf (revision 26) +++ src/syn/xrm/XRM-MetaVars.sdf (working copy) @@ -1 +1,5 @@ module XRM-MetaVars +exports + variables + [s][0-9]* -> DeclarationOrCommand {prefer} + "s"[0-9]* "*" -> DeclarationOrCommand+ {prefer} Index: src/syn/xrm/XRM-Update.sdf --- src/syn/xrm/XRM-Update.sdf (revision 0) +++ src/syn/xrm/XRM-Update.sdf (revision 0) @@ -0,0 +1,22 @@ +module XRM-Update +imports + PRISM-to-XRM + XRM-Arrays +exports + + %% EBNF Grammar: Extended Update Elements + %% UpdateElement ::= "(" ArrayAccessPrime "=" Expression ")" + %% (* The following form is kept for backwards compat. *) + %% | ArrayAccessPrime "=" Expression + + + sorts UpdateElement + context-free syntax + "(" ArrayAccessPrime "=" Expression ")" + -> UpdateElement {cons("UpdateElement")} + + %% NOTE: Officially this form is NOT supported but it is still supported + %% for backwards compatibility. This form introduces an ambiguity + %% because the `+' between the elements can be bound to the + %% Expression or can be a separator between two elements. + ArrayAccessPrime "=" Expression -> UpdateElement {cons("UpdateElement")} Index: src/syn/xrm/XRM-Main.sdf --- src/syn/xrm/XRM-Main.sdf (revision 26) +++ src/syn/xrm/XRM-Main.sdf (working copy) @@ -6,3 +6,5 @@ XRM-StaticFor XRM-StaticIf XRM-Literals + XRM-Declaration + XRM-Update Index: src/syn/xrm/XRM-Declaration.sdf --- src/syn/xrm/XRM-Declaration.sdf (revision 0) +++ src/syn/xrm/XRM-Declaration.sdf (revision 0) @@ -0,0 +1,22 @@ +module XRM-Declaration +imports + PRISM-to-XRM + XRM-Arrays +exports + + %% EBNF Grammar: Extended Variable declarations + %% Declaration ::= ArrayAccess ":" "[" Expression .. Expression "]" ";" + %% | ArrayAccess ":" "[" Expression .. Expression "]" "init" Expression ";" + %% | ArrayAccess ":" "bool" ";" + %% | ArrayAccess ":" "bool" "init" Expression ";" + + context-free syntax + ArrayAccess ":" "[" Expression ".." Expression "]" ";" + -> Declaration {cons("IntDecNoInit")} + ArrayAccess ":" "[" Expression ".." Expression "]" "init" Expression ";" + -> Declaration {cons("IntDec")} + + + ArrayAccess ":" "bool" ";" -> Declaration {cons("BoolDecNoInit")} + ArrayAccess ":" "bool" "init" Expression ";" + -> Declaration {cons("BoolDec")} Index: src/syn/xrm/XRM-Module.sdf --- src/syn/xrm/XRM-Module.sdf (revision 26) +++ src/syn/xrm/XRM-Module.sdf (working copy) @@ -15,4 +15,4 @@ context-free syntax "module" ArrayAccess DeclarationOrCommand* "endmodule" - -> Module {cons("MetaModule")} + -> Module {cons("Module")} Index: src/syn/xrm/XRM-Expression.sdf --- src/syn/xrm/XRM-Expression.sdf (revision 26) +++ src/syn/xrm/XRM-Expression.sdf (working copy) @@ -3,16 +3,19 @@ PRISM-to-XRM exports + %% EBNF Grammar: Extended Expressions + %% Expression ::= + %% ArrayAccess + %% | Expression "<<" Expression + %% | Expression ">>" Expression + context-free syntax - "++" Expression -> Expression {cons("PreIncr")} - "--" Expression -> Expression {cons("PreDecr")} + ArrayAccess -> Expression Expression ">>" Expression -> Expression {left,cons("RightShift")} Expression "<<" Expression -> Expression {left,cons("LeftShift")} context-free priorities { - "++" Expression -> Expression - "--" Expression -> Expression "+" Expression -> Expression "-" Expression -> Expression } @@ -24,12 +27,3 @@ Expression "*" Expression -> Expression Expression "/" Expression -> Expression } - - %% We need to add a lexical restriction so that when we have ++x it is - %% indeed understood as ++x and not +(+x) - %% This is due to the fact that sglr doesn't try to find the longuest match - %% So we need tell it to see whether there is another + (or -) after a - %% first + (or -) - lexical restrictions - "+" -/- [\+] - "-" -/- [\-] Index: src/syn/prism/PRISM-Declaration.sdf Index: src/syn/prism/PRISM-StartSymbols.sdf --- src/syn/prism/PRISM-StartSymbols.sdf (revision 26) +++ src/syn/prism/PRISM-StartSymbols.sdf (working copy) @@ -14,7 +14,6 @@ Expression Updates Identifier - IdentifierPrime SystemComp RewardStruct ModulesFileSection Index: tests/xrm/inner-static-if.xpm --- tests/xrm/inner-static-if.xpm (revision 26) +++ tests/xrm/inner-static-if.xpm (working copy) @@ -2,13 +2,11 @@ module dummy for i from 0 to 42 do - // FIXME: x here shall be replaced with x[i] - // but this is not supported ATM if i=0 | i=42 then - x : [0..2]; + x[i] : [0..2]; else - x : [0..1]; + x[i] : [0..1]; end - [] x=0 -> x'=1; + [] x[i]=0 -> x[i]'=1; end endmodule Index: tests/xrm/inner-static-for-step.xpm --- tests/xrm/inner-static-for-step.xpm (revision 26) +++ tests/xrm/inner-static-for-step.xpm (working copy) @@ -2,9 +2,7 @@ module dummy for i from 0 to 42 step 2 do - // FIXME: x here shall be replaced with x[i] - // but this is not supported ATM - x : [0..1]; - [] x=0 -> x'=1; + x[i] : [0..1]; + [] x[i]=0 -> x[i]'=1; end endmodule Index: tests/xrm/outer-static-if.xpm --- tests/xrm/outer-static-if.xpm (revision 26) +++ tests/xrm/outer-static-if.xpm (working copy) @@ -3,13 +3,13 @@ for i from 0 to 42 do if i<1 & i>41 then module dummy[i] - x : [0..1]; - [] x=0 -> x'=1; + x[i] : [0..1]; + [] x[i]=0 -> x[i]'=1; endmodule else module dummy[i] - x : [0..2]; - [] x=1 -> x'=2; + x[i] : [0..2]; + [] x[i]=1 -> x[i]'=2; endmodule end end Index: tests/xrm/outer-static-for-step.xpm --- tests/xrm/outer-static-for-step.xpm (revision 26) +++ tests/xrm/outer-static-for-step.xpm (working copy) @@ -2,7 +2,7 @@ for i from 0 to 42 step 2 do module dummy[i] - x : [0..1]; - [] x=0 -> x'=1; + x[i] : [0..1]; + [] x[i]=0 -> x[i]'=1; endmodule end Index: tests/xrm/static-if.xpm --- tests/xrm/static-if.xpm (revision 26) +++ tests/xrm/static-if.xpm (working copy) @@ -3,21 +3,19 @@ for i from 0 to 42 do if i<1 & i>41 then module dummy[i] - for i from 0 to 42 do - // FIXME: x here shall be replaced with x[i] - // but this is not supported ATM + for j from 0 to 42 do if i=0 | i=42 then - x : [0..2]; + x[i][j] : [0..2]; else - x : [0..1]; + x[i][j] : [0..1]; end - [] x=0 -> x'=1; + [] x[i][j]=0 -> x[i][j]'=1; end endmodule else module dummyelse[i] - y : [0..1]; - [] y=0 -> y'=1; + y[i] : [0..1]; + [] y[i]=0 -> y[i]'=1; endmodule end end Index: tests/xrm/inner-static-for.xpm --- tests/xrm/inner-static-for.xpm (revision 26) +++ tests/xrm/inner-static-for.xpm (working copy) @@ -2,9 +2,7 @@ module dummy for i from 0 to 42 do - // FIXME: x here shall be replaced with x[i] - // but this is not supported ATM - x : [0..1]; - [] x=0 -> x'=1; + x[i] : [0..1]; + [] x[i]=0 -> x[i]'=1; end endmodule Index: tests/xrm/static-for-step.xpm --- tests/xrm/static-for-step.xpm (revision 26) +++ tests/xrm/static-for-step.xpm (working copy) @@ -2,11 +2,9 @@ for i from 0 to 42 step 2 do module dummy[i] - for i from 0 to 42 step 2 do - // FIXME: x here shall be replaced with x[i] - // but this is not supported ATM - x : [0..1]; - [] x=0 -> x'=1; + for j from 0 to 42 step 2 do + x[i][j] : [0..1]; + [] x[i][j]=0 -> x[i][j]'=1; end endmodule end Index: tests/xrm/outer-static-for.xpm --- tests/xrm/outer-static-for.xpm (revision 26) +++ tests/xrm/outer-static-for.xpm (working copy) @@ -2,7 +2,7 @@ for i from 0 to 42 do module dummy[i] - x : [0..1]; - [] x=0 -> x'=1; + x[i] : [0..1]; + [] x[i]=0 -> x[i]'=1; endmodule end Index: tests/xrm/simple_01.xpm --- tests/xrm/simple_01.xpm (revision 26) +++ tests/xrm/simple_01.xpm (working copy) @@ -4,7 +4,4 @@ [] x=1 -> (x'=x/x>>2+x); [] x=2 -> (x'=x+x<<3/x); - [] (x=42) -> (x'=++x); - [] ++x=4 -> true; // x=3 - [] --x=4 -> true; // x=5 endmodule Index: tests/xrm/static-for.xpm --- tests/xrm/static-for.xpm (revision 26) +++ tests/xrm/static-for.xpm (working copy) @@ -2,11 +2,9 @@ for i from 0 to 42 do module dummy[i] - for i from 0 to 42 do - // FIXME: x here shall be replaced with x[i] - // but this is not supported ATM - x : [0..1]; - [] x=0 -> x'=1; + for j from 0 to 42 do + x[i][j] : [0..1]; + [] x[i][j]=0 -> x[i][j]'=1; end endmodule end