https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit &lt;sigoure.benoit(a)lrde.epita.fr&gt; 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) =