https://svn.lrde.epita.fr/svn/xrm/trunk
Index: ChangeLog
from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr>
Fix the size of generated arrays.
* src/str/array-decl-desugar.str: Stick with the C-style array
convention. (that is: array[N] has values ranging from array[0]
to array[N-1])
array-decl-desugar.str | 8 ++++++--
1 file changed, 6 insertions(+), 2 deletions(-)
Index: src/str/array-decl-desugar.str
--- src/str/array-decl-desugar.str (revision 34)
+++ src/str/array-decl-desugar.str (working copy)
@@ -45,13 +45,17 @@
/* find the first element in the list which matches ?Int(_)
* eg: [Identifier("..."), Int("1"), Int("2")] will be transformed in
* ([Identifier("...")], Int("1"), [Int("2")]) */
- ; <split-fetch-keep(?Int(_))> dims' => (dims-done, current-dim, dims-todo)
+ ; <split-fetch-keep(?Int(_))> dims'
+ => (dims-done, Int(current-dim), dims-todo)
+
+ /* array[N] has N elements ranging from 0 to N-1 */
+ ; <subtS>(current-dim, "1") => current-dim'
/* replace the dimension we're working on by the meta-var */
; <concat> [dims-done, [Identifier(x)], dims-todo]
/* return the result in a tuple */
- ; !(x, current-dim, <id>)
+ ; !(x, Int(current-dim'), <id>)
rules
// FIXME: Try to figure out why concrete syntax fails to work here
https://svn.lrde.epita.fr/svn/xrm/trunk
Index: ChangeLog
from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr>
Use static const variables in constant propagation.
* src/sig/Makefile.am: Patch a possible dependency problem.
* src/str/xrm-front.str: Change some comments.
* src/str/xrm-to-prism.str: Collect static const variables.
* src/str/prism-desugar.str: Use the known values of static const
variables in constant propagation if possible.
* TODO: Update things done. Add a question about PRISM's behavior.
TODO | 13 +++++++++----
src/sig/Makefile.am | 8 +++++---
src/str/prism-desugar.str | 21 +++++++++++++++++++--
src/str/xrm-front.str | 6 +++---
src/str/xrm-to-prism.str | 45 +++++++++++++++++++++++++++++++++++++++++----
5 files changed, 77 insertions(+), 16 deletions(-)
Index: src/sig/Makefile.am
--- src/sig/Makefile.am (revision 33)
+++ src/sig/Makefile.am (working copy)
@@ -5,7 +5,7 @@
## Mail <sigoure.benoit(a)lrde.epita.fr>
##
## Started on Mon May 8 18:38:32 2006 SIGOURE Benoit
-## Last update Tue May 9 20:39:39 2006 SIGOURE Benoit
+## Last update Thu May 25 23:41:55 2006 SIGOURE Benoit
##
include $(top_srcdir)/config/Transformers.mk
@@ -18,8 +18,10 @@
SDF2RTG_FLAGS = --main $*
-PRISM.def:
+PRISM.def: $(top_builddir)/src/syn/prism/PRISM.def
+ rm -f $@
$(LN_S) $(top_builddir)/src/syn/prism/$@ $@
-XRM.def:
+XRM.def: $(top_builddir)/src/syn/xrm/XRM.def
+ rm -f $@
$(LN_S) $(top_builddir)/src/syn/xrm/$@ $@
Index: src/str/xrm-front.str
--- src/str/xrm-front.str (revision 33)
+++ src/str/xrm-front.str (working copy)
@@ -36,7 +36,7 @@
end
end
- // pipeline of transformations performed by xrm-front
+ /** pipeline of transformations performed by xrm-front */
xrm-front-pipeline =
dbg(|"xrm-front-pipeline starting")
; xrm-to-prism
@@ -47,14 +47,14 @@
end
; id // FIXME: add more transformations here
- // list of available options for xrm-front
+ /** list of available options for xrm-front */
xrm-front-options =
pp-aterm-option
+ add-pos-option
+ keep-attributes-option
+ desugar-option
- // check the options are consistent
+ /** checks the options are consistent */
check-options =
if <get-config> "-b" then
// if we're asked for binary output, don't bother with pretty printing
Index: src/str/xrm-to-prism.str
--- src/str/xrm-to-prism.str (revision 33)
+++ src/str/xrm-to-prism.str (working copy)
@@ -1,6 +1,19 @@
/*
** This sub-module does the real work of the front-end. It transforms the
** program into a valid PRISM AST.
+**
+** Dynamic rules inventory:
+** - DeclarationList: used by the strategy reorder-module-contents to
+** store all the declarations within a given module. This way declarations
+** can be grouped together in the module (as required by the PRISM grammar)
+** - CommandList: used by the strategy reorder-module-contents to
+** store all the commands within a given module. This way commands can
+** be grouped together in the module (as required by the PRISM grammar)
+** - ExpandStaticConsts: created by the strategy collect-static-const-decl
+** and used by prism-desugar for constant propagation. Maps an identifier
+** 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).
*/
module xrm-to-prism
imports
@@ -17,11 +30,15 @@
/* remove XRM sugar, normalize some nodes */
innermost(xrm-to-prism-desugar)
- /* Desugar array declarations
+ /* Two things in one traversal:
+ * 1/ 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 */
- ; topdown(try(array-decl-desugar))
+ * 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.
+ */
+ ; topdown(try(array-decl-desugar); try(collect-static-const-decl))
/* Check that meta vars are always defined in the current scope when used
* and that they are not redefined twice in the same scope */
@@ -48,7 +65,7 @@
xrm-to-prism-desugar:
|[ e1 << e2 ]| -> |[ e1 * func(pow, 2, e2) ]|
- // if the step is not specified, it is implicitely set to 1
+ /** if the step is not specified, it is implicitly set to 1 */
xrm-to-prism-desugar:
MetaFor(identifier, from, to, body)
-> MetaFor(identifier, from, to, Int("1"), body)
@@ -58,6 +75,26 @@
//|[ if e then s* end ]| -> |[ if e then s* else end ]|
MetaIf(e, m*) -> MetaIf(e, m*, [])
+signature constructors
+ Type : String -> Type
+
+strategies
+
+ collect-static-const-decl =
+ ?ConstInt(idf, value)
+ ; where(!value{Type("int")} => v)
+ ; rules(ExpandStaticConsts: idf -> v)
+
+ collect-static-const-decl =
+ ?ConstDouble(idf, value)
+ ; where(!value{Type("double")} => v)
+ ; rules(ExpandStaticConsts: idf -> v)
+
+ collect-static-const-decl =
+ ?ConstBool(idf, value)
+ ; where(!value{Type("bool")} => v)
+ ; rules(ExpandStaticConsts: idf -> v)
+
strategies
/**
Index: src/str/prism-desugar.str
--- src/str/prism-desugar.str (revision 33)
+++ src/str/prism-desugar.str (working copy)
@@ -9,13 +9,14 @@
** 1. First convert all literal ints to doubles. This makes the
** simplifications easier to write since there is less cases to
** address (eg: int + int, int + double, double + int,
- ** double + double etc.).
+ ** double + double etc.). This first pass works in a slightly
+ ** special way, see prism-desugar-first-pass for more info.
** 2. Desugar the AST
** 3. Convert the doubles which are round numbers back to ints.
** Simplify doubles (round them up and remove trailing zeros)
*/
prism-desugar =
- topdown(try(IntToDouble))
+ prism-desugar-first-pass
; innermost(
RemoveUnconditionnalUpdates
<+ AddZero <+ MulOne <+ MulZero <+ DivOne <+ catch-div-by-zero
@@ -26,6 +27,22 @@
)
; topdown(try(SimplifyDoubles <+ TruncateDouble))
+ /**
+ ** 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; ]|.
+ */
+ prism-desugar-first-pass =
+ ConstInt(id, prism-desugar)
+ <+ ConstDouble(id, prism-desugar)
+ <+ ConstBool(id, prism-desugar)
+ <+ ?Int(_); IntToDouble
+ <+ all(try(ExpandStaticConsts); prism-desugar-first-pass)
+
rules
IntToDouble: Int(i) -> Double(i)
Index: TODO
--- TODO (revision 33)
+++ TODO (working copy)
@@ -17,6 +17,11 @@
* Add more tests. Add tests which actually do check that the generated code
is correct (which is not done ATM).
+ * How are handled mutually recursive static constant variables in PRISM?
+ eg: const int x = y;
+ const int y = x;
+ Is it even possible to define a static const variable from another one?
+
## ---------- ##
## Extensions ##
## ---------- ##
@@ -91,10 +96,6 @@
x = 1..5,7,10..13
==> (x>=1 & x<=5) | (x=7) | (x>=10 & x<=13)
- * Evaluate constant calls to built-in functions, eg
- func(min, 4, 5)
- ==> 4
-
* Expand formulas, eg
formula lfree = p2=0..4,6,10;
// ...
@@ -159,3 +160,7 @@
[] x[0]=0 -> ... => ... <=> end
endmodule => [] x_0=0 -> ... <=> [] x_0=0 -> ...
=> endmodule <=> endmodule
+
+ * Evaluate constant calls to built-in functions, eg
+ func(min, 4, 5)
+ ==> 4
https://svn.lrde.epita.fr/svn/xrm/trunk
Index: ChangeLog
from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr>
Add array declarations (sugar).
It is now possible to declare arrays such as: b[4][3] : bool;
Multi-dimensional arrays are correctly handled.
* src/str/array-decl-desugar.meta: New.
* src/str/array-decl-desugar.str: New.
* src/str/xrm-to-prism.str: Use array-decl-desugar.
* src/syn/xrm/XRM-Command.sdf: "Dirty" hack to make it work.
* tests/xrm/globals.xpm: New.
* tests/xrm/array-decl_dim_exp.xpm: New.
* tests/xrm/labels.xpm: New.
* tests/xrm/array-decl_1d.xpm: New.
* tests/xrm/array-decl_2d.xpm: New.
* tests/xrm/array-decl_3d.xpm: New.
* tests/prism/simple-label.pm: New.
* TODO: Add many more ideas from Micha.
TODO | 63 ++++++++++++++++++++++------
src/str/array-decl-desugar.meta | 1
src/str/array-decl-desugar.str | 87 +++++++++++++++++++++++++++++++++++++++
src/str/xrm-to-prism.str | 9 +++-
src/syn/xrm/XRM-Command.sdf | 4 +
tests/prism/simple-label.pm | 6 ++
tests/xrm/array-decl_1d.xpm | 8 +++
tests/xrm/array-decl_2d.xpm | 10 ++++
tests/xrm/array-decl_3d.xpm | 8 +++
tests/xrm/array-decl_dim_exp.xpm | 5 ++
tests/xrm/globals.xpm | 3 +
tests/xrm/labels.xpm | 10 ++++
12 files changed, 199 insertions(+), 15 deletions(-)
Index: src/str/array-decl-desugar.meta
--- src/str/array-decl-desugar.meta (revision 0)
+++ src/str/array-decl-desugar.meta (revision 0)
@@ -0,0 +1 @@
+Meta([Syntax("StrategoXRM")])
Index: src/str/array-decl-desugar.str
--- src/str/array-decl-desugar.str (revision 0)
+++ src/str/array-decl-desugar.str (revision 0)
@@ -0,0 +1,87 @@
+/**
+** This sub-module is used to desugar multi-dimension array declarations.
+** Each dimension will by handled by a meta for loop unrolled later.
+** So if we have a N-dimensions array declaration, it will be rewritten as
+** N nested for loops.
+**
+** eg: x[4][3] : [1..2];
+** for meta_i_0 from 0 to 4 do
+** for meta_i_1 from 0 to 3 do
+** x[meta_i_0][meta_i_1] : [1..2];
+** end
+** end
+** Since this will unrolled and flattened later in by the submodule evaluating
+** meta-code we will end up having all the x_i_j variables declared.
+**
+** NOTE: Each dimension is handled separately and recursion is not handled by
+** array-decl-desugar. The rule must be called in a topdown(try(..)) in order
+** to naturally traverse generated code and thus, handle all dimensions.
+*/
+module array-decl-desugar
+
+strategies
+
+ /**
+ ** Patch the list of dimensions with the meta-var used in the meta for loop.
+ ** Basically this strategy generates a new meta-var used as the iterator
+ ** in the meta-for loop and updates the dimensions of the declared array.
+ ** The dimension updated is the first one matching Int(_)
+ **
+ ** eg: x[4][3] : bool;
+ ** => BoolDecNoInit(Identifier("x"),
+ ** ArrayAccess( [Identifier("meta_i_0"), Int(3)] ))
+ ** will needs to be transformed as:
+ ** BoolDecNoInit(Identifier("x"),
+ ** ArrayAccess( [Identifier("meta_i_0"),
+ ** Identifier("meta_i_1")] ))
+ ** @type List(dims) -> List(meta-var, current-dim, List(all-dims-patched))
+ */
+ update-dimensions(|dims) =
+ <newname> "__meta_i" => x
+
+ /* Ensure that the list of dimensions is desugared */
+ ; <prism-desugar> dims => dims'
+
+ /* find the first element in the list which matches ?Int(_)
+ * eg: [Identifier("..."), Int("1"), Int("2")] will be transformed in
+ * ([Identifier("...")], Int("1"), [Int("2")]) */
+ ; <split-fetch-keep(?Int(_))> dims' => (dims-done, current-dim, dims-todo)
+
+ /* replace the dimension we're working on by the meta-var */
+ ; <concat> [dims-done, [Identifier(x)], dims-todo]
+
+ /* return the result in a tuple */
+ ; !(x, current-dim, <id>)
+
+rules
+// FIXME: Try to figure out why concrete syntax fails to work here
+
+ array-decl-desugar:
+ IntDecNoInit(ArrayAccess(idf, dims), low, up)
+ //-> |[ for x from 0 to ~dim step 1 do x[i] : [~low..~up]; end ]|
+ -> MetaFor(Identifier(x), Int("0"), current-dim', Int("1"),
+ [ IntDecNoInit(ArrayAccess(idf, dims'), low, up) ])
+ where update-dimensions(|dims) => (x, current-dim', dims')
+
+ array-decl-desugar:
+ IntDec(ArrayAccess(idf, dims), low, up, value)
+ //-> |[ for x from 0 to ~dim step 1 do
+ // x[i] : [~low..~up] init ~value;
+ // end ]|
+ -> MetaFor(Identifier(x), Int("0"), current-dim', Int("1"),
+ [ IntDec(ArrayAccess(idf, dims'), low, up, value) ])
+ where update-dimensions(|dims) => (x, current-dim', dims')
+
+ array-decl-desugar:
+ BoolDecNoInit(ArrayAccess(idf, dims))
+ //-> |[ for x from 0 to ~dim step 1 do x[i] : bool; end ]|
+ -> MetaFor(Identifier(x), Int("0"), current-dim', Int("1"),
+ [ BoolDecNoInit(ArrayAccess(idf, dims')) ])
+ where update-dimensions(|dims) => (x, current-dim', dims')
+
+ array-decl-desugar:
+ BoolDec(ArrayAccess(idf, dims), value)
+ //-> |[ for x from 0 to ~dim step 1 do x[i] : bool init ~value; end ]|
+ -> MetaFor(Identifier(x), Int("0"), current-dim', Int("1"),
+ [ BoolDec(ArrayAccess(idf, dims'), value) ])
+ where update-dimensions(|dims) => (x, current-dim', dims')
Index: src/str/xrm-to-prism.str
--- src/str/xrm-to-prism.str (revision 30)
+++ src/str/xrm-to-prism.str (working copy)
@@ -9,12 +9,19 @@
desugar-array-accesses
check-meta-vars
eval-meta-code
+ array-decl-desugar
strategies
xrm-to-prism =
/* remove XRM sugar, normalize some nodes */
- topdown(try(xrm-to-prism-desugar))
+ innermost(xrm-to-prism-desugar)
+
+ /* 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 */
+ ; 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 */
Index: src/syn/xrm/XRM-Command.sdf
--- src/syn/xrm/XRM-Command.sdf (revision 30)
+++ src/syn/xrm/XRM-Command.sdf (working copy)
@@ -8,4 +8,6 @@
%% Command ::= "[" ArrayAccess "]" Expression "->" Updates ";"
context-free syntax
- "[" ArrayAccess "]" Expression "->" Updates ";" -> Command {cons("Command")}
+ "[" ArrayAccess? "]" Expression "->" Updates ";"
+ -> Command {prefer,cons("Command")}
+ %% FIXME: dirty hack: ^^^^^^
Index: tests/xrm/globals.xpm
--- tests/xrm/globals.xpm (revision 0)
+++ tests/xrm/globals.xpm (revision 0)
@@ -0,0 +1,3 @@
+for i from 0 to 4 do
+ global x[i] : bool;
+end
Index: tests/xrm/array-decl_dim_exp.xpm
--- tests/xrm/array-decl_dim_exp.xpm (revision 0)
+++ tests/xrm/array-decl_dim_exp.xpm (revision 0)
@@ -0,0 +1,5 @@
+// should be equivalent as declaring x[8]
+
+module arrays
+ x[4+4] : [0..42];
+endmodule
Index: tests/xrm/labels.xpm
--- tests/xrm/labels.xpm (revision 0)
+++ tests/xrm/labels.xpm (revision 0)
@@ -0,0 +1,10 @@
+probabilistic
+
+for i from 0 to 4 do
+ module dummy[i]
+ x[i] : [0..1] init i;
+ for j from 5 to 10 do
+ [testlabel[j]] x[i]=j -> x[i]'=j+1;
+ end
+ endmodule
+end
Index: tests/xrm/array-decl_1d.xpm
--- tests/xrm/array-decl_1d.xpm (revision 0)
+++ tests/xrm/array-decl_1d.xpm (revision 0)
@@ -0,0 +1,8 @@
+// should be expanded in x_0 x_1 x_2 x_3
+
+module arrays
+ x[4] : [0..42];
+ y[4] : [0..42] init 0;
+ b[4] : bool;
+ c[4] : bool init true;
+endmodule
Index: tests/xrm/array-decl_2d.xpm
--- tests/xrm/array-decl_2d.xpm (revision 0)
+++ tests/xrm/array-decl_2d.xpm (revision 0)
@@ -0,0 +1,10 @@
+// should be expanded in x_0_0 x_1_0 x_2_0 x_3_0
+// x_0_1 x_1_1 x_2_1 x_3_1
+// x_0_2 x_1_2 x_2_2 x_3_2
+
+module arrays
+ x[4][3] : [0..42];
+ y[4][3] : [0..42] init 0;
+ b[4][3] : bool;
+ c[4][3] : bool init true;
+endmodule
Index: tests/xrm/array-decl_3d.xpm
--- tests/xrm/array-decl_3d.xpm (revision 0)
+++ tests/xrm/array-decl_3d.xpm (revision 0)
@@ -0,0 +1,8 @@
+// should be expanded in x_0_0_0 x_0_0_1 x_0_0_2 x_0_0_3 ...
+
+module arrays
+ x[4][3][2] : [0..42];
+ y[4][3][2] : [0..42] init 0;
+ b[4][3][2] : bool;
+ c[4][3][2] : bool init true;
+endmodule
Index: tests/prism/simple-label.pm
--- tests/prism/simple-label.pm (revision 0)
+++ tests/prism/simple-label.pm (revision 0)
@@ -0,0 +1,6 @@
+probabilistic
+
+module dummy
+ x: [0..1] init 1;
+ [label] x=2 -> x'=3;
+endmodule
Index: TODO
--- TODO (revision 30)
+++ TODO (working copy)
@@ -14,25 +14,30 @@
* Write some sort of formal descriptions of the extensions offered.
+ * Add more tests. Add tests which actually do check that the generated code
+ is correct (which is not done ATM).
+
## ---------- ##
## Extensions ##
## ---------- ##
* Add the following at the meta-level:
- Let's have the possibility to generate other ModulesFileSection such as:
- o Formula
- o Constant
- o Global
- o RenamedModule
- o SystemComp
- o RewardStruct
-
- * Add arrays (sugar). module varArrays <=> module varArrays
- module varArrays => x_0 : [0..3]; <=> for a_0 from 0 to 4 do
- x[4] : [0..3]; => x_1 : [0..3]; <=> x[i] : [0..3];
- [] x[0]=0 -> ... => ... <=> end
- endmodule => [] x_0=0 -> ... <=> [] x_0=0 -> ...
- => endmodule <=> endmodule
+ o Formula // add it in the grammar. should be
+ // automagically handled
+ o Constant // ditto
+ o Global // done (automagically handled)
+ o RenamedModule // need to be investigated
+ 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.
+ 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.
@@ -52,6 +57,31 @@
x[1..3]?=0 => x_1=0 | x_2=0 | x_3=0
NOTE: x[5]?=0 should be considered as an error.
+ NOTE: arrays should behave like in C (array[N] is ranging from 0 to N-1)
+ I'm not sure it's really always handled this way ATM :/
+
+ * Add non-static array accesses (as suggested by Micha). For instance:
+ module test
+ x[4] : [0..5];
+ i : [0..2];
+
+ [] x[0..i]=0 -> ... // i can't be guessed at compile time
+ endmodule
+
+ Translate this with something like:
+ module test
+ x_0 : [0..5];
+ x_1 : [0..5];
+ x_2 : [0..5];
+ 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)) -> ...
+ endmodule
+
+ /!\ This (might) require that we add another pass to collect the generated
+ variables and their type + domain and might be quite challenging to
+ handle.
## -------------- ##
## Desugarisation ##
@@ -122,3 +152,10 @@
- In between modules (that is, where we can expect a ModulesFileSection)
- In between commands (that is where we can expect a Declaration or a
Command)
+
+ * Add arrays (sugar). module varArrays <=> module varArrays
+ module varArrays => x_0 : [0..3]; <=> for a_0 from 0 to 4 do
+ x[4] : [0..3]; => x_1 : [0..3]; <=> x[a_0] : [0..3];
+ [] x[0]=0 -> ... => ... <=> end
+ endmodule => [] x_0=0 -> ... <=> [] x_0=0 -> ...
+ => endmodule <=> endmodule
Certains échecs de la build farm (pour Vaucanson) tiennent à son
utilisation des sources qui est incorrecte et qui ne repose sur aucun
des modèles connus. On a deux modèles, et seulement deux :
- mainteneur, et donc accès svn
- utilisateur, et donc une tarball
Actuellement, on fait un checkout qu'on copie ailleurs. C'est bâtard,
et en particulier mon code qui fait des checkouts à ce moment-là (et
c'est légitime) meurt à l'exécution.
Il faut choisir, mais seuls deux modèles existent :
- mainteneur, et on part d'un svn checkout
- utilisateur, et on part d'un make dist
Je vote pour le premier cas, qui comprend le second grâce à distcheck.
SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes:
> + * Add arrays (sugar). module varArrays <=> module varArrays
> + module varArrays => x_0 : [0..3]; <=> for a_0 from 0 to 4 do
> + x[4] : [0..3]; => x_1 : [0..3]; <=> x[i] : [0..3];
> + [] x[0]=0 -> ... => ... <=> end
> + endmodule => [] x_0=0 -> ... <=> [] x_0=0 -> ...
> + => endmodule <=> endmodule
Wow, et ça ne va pas conflicter avec tes boucles for sur les
modules ? Si tu comptes te servir du fait que ce soit un
identifiant, rappel toi bien que static const i = 3; x[i] c'est
joliement évalué à la compil comme un tableau de 3 éléments pour
toi.
Qui plus est, il faudra faire attention au masquage de i par une
variable de boucle.
> + * Add conditional tests on arrays (with support for ranges):
> + x[5]=0 => x_5=0
> + x[1..3]=0 => x_1=0 & x_2=0 & x_3=0
> + (support things such as: x[1..3,6,8..9])
> +
> + x[1..3]?=0 => x_1=0 | x_2=0 | x_3=0
> +
> + NOTE: x[5]?=0 should be considered as an error.
NOTE: Je ne vois pas pourquoi. Si j'ai une variable j dans mon
module, j'aimerai pouvoir écrire x[1..j] = 0, ce qui se traduirait
par (j < 1 || x_1 = 0) && (j < 2 || x_2 = 0) && ...
Ce qui pourrait conduire à écrire non seulement x[1..1], mais aussi
x[1..0].
Ajoute à ça que mon `j' peut-être connu (static const) à la
compilation, donc il ne faudra pas faire cela.
--
| Le copillage-collage Michaël `Micha' Cadilhac |
| tue le programmeur. cadilh_m - Epita 2007 - CSI |
| -- Dictons LRDE JID: micha(a)amessage.be |
`-- - - - - --'
https://svn.lrde.epita.fr/svn/xrm/trunk
Index: ChangeLog
from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr>
Correct some typos and add things to do.
* src/str/prism-desugar.str: Correct a typo (thanks vimspell).
* src/str/eval-meta-code.str: Ditto.
* src/syn/prism/PRISM-Command.sdf: Ditto.
* src/syn/xrm/XRM-Command.sdf: New. Seems to be broken.
* src/syn/xrm/XRM-Main.sdf: Import XRM-Command.
* TODO: Add a couple of nice ideas suggested by Michael Cadilhac.
Update things done.
TODO | 90 +++++++++++++++++++++++++---------------
src/str/eval-meta-code.str | 2
src/str/prism-desugar.str | 2
src/syn/prism/PRISM-Command.sdf | 2
src/syn/xrm/XRM-Command.sdf | 11 ++++
src/syn/xrm/XRM-Main.sdf | 1
6 files changed, 72 insertions(+), 36 deletions(-)
Index: src/str/prism-desugar.str
--- src/str/prism-desugar.str (revision 29)
+++ src/str/prism-desugar.str (working copy)
@@ -48,7 +48,7 @@
rules
/**
- ** Remove conditionnal updates.
+ ** Remove conditional updates.
** [] guard -> unconditionnal-update-list;
** is rewritten as:
** [] guard -> 1:(unconditionnal-update-list);
Index: src/str/eval-meta-code.str
--- src/str/eval-meta-code.str (revision 29)
+++ src/str/eval-meta-code.str (working copy)
@@ -37,7 +37,7 @@
<eval-meta-code> else-part
else
ice(|"eval-meta-code", <concat-strings> [
- "the conditionnal test of a meta if could ",
+ "the conditional test of a meta if could ",
"not be reduced to a single value (True or",
" False), this should have been detected ",
"earlier"],
Index: src/syn/xrm/XRM-Command.sdf
--- src/syn/xrm/XRM-Command.sdf (revision 0)
+++ src/syn/xrm/XRM-Command.sdf (revision 0)
@@ -0,0 +1,11 @@
+module XRM-Command
+imports
+ PRISM-to-XRM
+
+exports
+
+ %% EBNF Grammar: Extended Commands
+ %% Command ::= "[" ArrayAccess "]" Expression "->" Updates ";"
+
+ context-free syntax
+ "[" ArrayAccess "]" Expression "->" Updates ";" -> Command {cons("Command")}
Index: src/syn/xrm/XRM-Main.sdf
--- src/syn/xrm/XRM-Main.sdf (revision 29)
+++ src/syn/xrm/XRM-Main.sdf (working copy)
@@ -8,3 +8,4 @@
XRM-Literals
XRM-Declaration
XRM-Update
+ XRM-Command
Index: src/syn/prism/PRISM-Command.sdf
--- src/syn/prism/PRISM-Command.sdf (revision 29)
+++ src/syn/prism/PRISM-Command.sdf (working copy)
@@ -14,7 +14,7 @@
context-free syntax
"[" Identifier? "]" Expression "->" Updates ";" -> Command {cons("Command")}
- %% The follwing syntax was commented out in PRISM's parser...
+ %% The following syntax was commented out in PRISM's parser...
%% It seems it will be used in the near future when rewards will be fully
%% supported.
Index: TODO
--- TODO (revision 29)
+++ TODO (working copy)
@@ -14,35 +14,11 @@
* Write some sort of formal descriptions of the extensions offered.
- * Fix the Int nodes in the static for loops (if its really necessary?)
-
## ---------- ##
## Extensions ##
## ---------- ##
- * Add static for loops and static if:
- for i from 0 to 3 step 1 do => module sensor_0
- module sensor[i] => b_0 : [0..42] init 0;
- b[i] : [0..42] init 0; => s_0_0 : [0..2] init 2;
- for j from 0 to 3 do => s_0_1 : [0..4] init 2;
- if j = 1 then => s_0_2 : [0..4] init 2;
- s[i][j] : [0..j+3] init 2; => s_0_2 : [0..4] init 2;
- else =>
- s[i][j] : [0..j+2] init 2; => [] s_0_0=0 -> (b_0'=b_0+1)
- end => [] s_0_1=0 -> (b_0'=b_0+1)
- end => [] s_0_2=0 -> (b_0'=b_0+1)
- => endmodule
- for j from 0 to 3 do =>
- [] s[i][j]=0 -> (b[i]' = b[i]+1) => module sensor_1
- end => b_1 : [0..42] init 1;
- endmodule => s_1_0 : [0..2] init 2;
- end => ...
-
- Of course, the for loops must be unroll-able statically.
- Static for loops can be found:
- - In between modules (that is, where we can expect a ModulesFileSection)
- - In between commands (that is where we can expect a Declaration or a
- Command)
+ * Add the following at the meta-level:
- Let's have the possibility to generate other ModulesFileSection such as:
o Formula
o Constant
@@ -50,15 +26,32 @@
o RenamedModule
o SystemComp
o RewardStruct
- Notice: it's not necessary for Init since it seems only one Init
- section is allowed.
- I think it doesn't make sense to allow static if-then-else constructs
- outside static for loops because, ATM, static for loops are the only way
- to introduce static (meta-)variables (such as `i' and `j' in the previous
- example).
- Note: Issue a warning (or an error?) if we generate twice the same module
- name.
+ * Add arrays (sugar). module varArrays <=> module varArrays
+ module varArrays => x_0 : [0..3]; <=> for a_0 from 0 to 4 do
+ x[4] : [0..3]; => x_1 : [0..3]; <=> x[i] : [0..3];
+ [] x[0]=0 -> ... => ... <=> end
+ endmodule => [] x_0=0 -> ... <=> [] x_0=0 -> ...
+ => endmodule <=> endmodule
+
+ * 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.
+
+ * Add bound checking. (extension of the previous point)
+ Dirty way: check that each variable is declared somewhere.
+ Hard way: detect and register array declarations and detect the bounds of
+ the array. When array expansion occurs, check that we're not
+ out of bounds. This can get very tricky since a variable can be
+ expanded BEFORE its actual declaration (especially in XRM).
+
+ * Add conditional tests on arrays (with support for ranges):
+ x[5]=0 => x_5=0
+ x[1..3]=0 => x_1=0 & x_2=0 & x_3=0
+ (support things such as: x[1..3,6,8..9])
+
+ x[1..3]?=0 => x_1=0 | x_2=0 | x_3=0
+
+ NOTE: x[5]?=0 should be considered as an error.
## -------------- ##
## Desugarisation ##
@@ -98,3 +91,34 @@
// ...
[] x=3 -> ... // x=3 is impossible
[] x=0 -> (x'=3) // x=3 is not in the definition range of x
+
+ ## ---- ##
+ ## DONE ##
+ ## ---- ##
+
+ The following work has been done but is kept here because it contains some
+ useful informations to be reused in the final documentation of the package.
+
+ * Meta for loops and meta if statements:
+ for i from 0 to 3 step 1 do => module sensor_0
+ module sensor[i] => b_0 : [0..42] init 0;
+ b[i] : [0..42] init 0; => s_0_0 : [0..2] init 2;
+ for j from 0 to 3 do => s_0_1 : [0..4] init 2;
+ if j = 1 then => s_0_2 : [0..4] init 2;
+ s[i][j] : [0..j+3] init 2; => s_0_2 : [0..4] init 2;
+ else =>
+ s[i][j] : [0..j+2] init 2; => [] s_0_0=0 -> (b_0'=b_0+1)
+ end => [] s_0_1=0 -> (b_0'=b_0+1)
+ end => [] s_0_2=0 -> (b_0'=b_0+1)
+ => endmodule
+ for j from 0 to 3 do =>
+ [] s[i][j]=0 -> (b[i]' = b[i]+1) => module sensor_1
+ end => b_1 : [0..42] init 1;
+ endmodule => s_1_0 : [0..2] init 2;
+ end => ...
+
+ Of course, the for loops must be unroll-able statically.
+ Meta for loops can be found:
+ - In between modules (that is, where we can expect a ModulesFileSection)
+ - In between commands (that is where we can expect a Declaration or a
+ Command)
