[Projects] XRM 37: Add formulas in constant propagation.

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit &lt;sigoure.benoit(a)lrde.epita.fr&gt; Add formulas in constant propagation. * src/str/xrm-to-prism.str: Fix the traversals collecting static * const decls and add formulas collections. Update comments. * src/str/prism-desugar.str: Expand formulas. * tests/xrm/static-const-arrays-desugar.xpm: New. * TODO: Update. New idea: array initializations a la C :). TODO | 18 +++++++++++------- src/str/prism-desugar.str | 20 +++++++++++++------- src/str/xrm-to-prism.str | 26 ++++++++++++++++++++------ tests/xrm/static-const-arrays-desugar.xpm | 26 ++++++++++++++++++++++++++ 4 files changed, 70 insertions(+), 20 deletions(-) Index: src/str/xrm-to-prism.str --- src/str/xrm-to-prism.str (revision 36) +++ src/str/xrm-to-prism.str (working copy) @@ -14,6 +14,9 @@ ** with a value and an annotated type. Only constants with a static value ** provided will be put here (constants can have their value defined in ** init blocks and chosen at random at runtime). +** - ExpandFormulas: created by the strategy collect-formulas and used by +** prism-desugar for constant propagation. Maps an identifier with an +** expression. */ module xrm-to-prism imports @@ -30,15 +33,19 @@ /* remove XRM sugar, normalize some nodes */ innermost(xrm-to-prism-desugar) - /* Two things in one traversal: - * 1/ Desugar array declarations + /* Collect static const variables + * Two goals: expand them if needed, look for variable name conflicts. */ + ; topdown(try(collect-static-const-decl); try(collect-formulas)) + + /* 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 - * 2/ Collect static const variables - * Two goals: expand them if needed, look for variable name conflicts. + * traversal is bottomup and won't recurse into generated code. + * + * This must come AFTER collect-static-const-decl since we might need + * to expand an array which relies on static const variables. */ - ; topdown(try(array-decl-desugar); try(collect-static-const-decl)) + ; 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 */ @@ -95,6 +102,13 @@ ; where(!value{Type("bool")} => v) ; rules(ExpandStaticConsts: idf -> v) +rules + + collect-formulas = + //?|[ formula x = e; ]| + ?FormulaDef(x, e) + ; rules(ExpandFormulas: x -> e) + strategies /** Index: src/str/prism-desugar.str --- src/str/prism-desugar.str (revision 36) +++ src/str/prism-desugar.str (working copy) @@ -29,19 +29,25 @@ /** ** Main goal: Transform all Int(_) -> Double(_) - ** In this first pass we also want to expand static consts. However, we - ** must be careful as to where these expansions occur. For instance, say - ** that N=10 (we know it thanks to the DR ExpandStaticConsts). If we are - ** on the node where N is declared (that is: |[ const int N = 10; ]|) we - ** should NOT expand `N' here. Otherwise we'll end up with - ** |[ const int 10 = 10; ]|. + ** + ** In this first pass we also want to expand static consts and formulas. + ** However, we must be careful as to where these expansions occur. For + ** instance, say that N=10 (we know it thanks to the DR ExpandStaticConsts). + ** + ** If we are on the node where N is declared (that is: + ** |[ const int N = 10; ]|) we should NOT expand `N' here. Otherwise + ** we'll end up with |[ const int 10 = 10; ]|. The same thing applies for + ** formulas and ExpandFormulas. */ prism-desugar-first-pass = ConstInt(id, prism-desugar) <+ ConstDouble(id, prism-desugar) <+ ConstBool(id, prism-desugar) + <+ FormulaDef(id, prism-desugar) <+ ?Int(_); IntToDouble - <+ all(try(ExpandStaticConsts); prism-desugar-first-pass) + <+ all(try(ExpandStaticConsts) + ; try(ExpandFormulas) + ; prism-desugar-first-pass) rules Index: tests/xrm/static-const-arrays-desugar.xpm --- tests/xrm/static-const-arrays-desugar.xpm (revision 0) +++ tests/xrm/static-const-arrays-desugar.xpm (revision 0) @@ -0,0 +1,26 @@ +const int N = 3; +const int array[N] = 42; + +module test + x[N] : [0..N] init array[N]; + + [] x[array[N]]=0 -> (x[array[N]]'=1); +endmodule + +// The above code will generate the following code once +// collect-static-const-decl and array-decl-desugar have runned. +// The problem is that the loop "hides" static const variables which +// are not caught by collect-static-const-decl. + +// const int N = 3; +// +// for __meta_i_0 from 0 to 2 step 1 do +// const int array[__meta_i_0] = 42; +// end +// +// module test +// for __meta_i_2 from 0 to 2 step 1 do +// x[__meta_i_2] : [0..N] init array[N]; +// end +// [] x[array[N]]=0 -> (x[array[N]]'=1); +// endmodule Index: TODO --- TODO (revision 36) +++ TODO (working copy) @@ -37,9 +37,8 @@ * Add the following at the meta-level: - Let's have the possibility to generate other ModulesFileSection such as: - o Formula // add it in the grammar. should be - // automagically handled - o Constant // ditto + o Formula // done (automagically handled) + o Constant // done (automagically handled) o Global // done (automagically handled) o RenamedModule // need to be investigated o RewardStruct // ditto @@ -48,10 +47,6 @@ * 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. @@ -95,6 +90,10 @@ variables and their type + domain and might be quite challenging to handle. + * Add array initializations a la C: + x[3] : [0..4] init {0, 1, 2}; + const int array[3] = {0, 1, 2}; + ## -------------- ## ## Desugarisation ## ## -------------- ## @@ -171,3 +170,8 @@ * Evaluate constant calls to built-in functions, eg func(min, 4, 5) ==> 4 + + * 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)