[Projects] XRM 55: Add documentation draft for XRM.

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit &lt;sigoure.benoit(a)lrde.epita.fr&gt; Add documentation draft for XRM. * src/str/desugar-array-access.str: Add an ICE condition. * tests/xrm/static_rand.xpm: New. * TODO: Bring up to date. * doc: New. * doc/user-guide.txt: New. TODO | 16 - doc/user-guide.txt | 392 +++++++++++++++++++++++++++++++++++++++ src/str/desugar-array-access.str | 7 tests/xrm/static_rand.xpm | 1 4 files changed, 398 insertions(+), 18 deletions(-) Index: src/str/desugar-array-access.str --- src/str/desugar-array-access.str (revision 54) +++ src/str/desugar-array-access.str (working copy) @@ -35,17 +35,12 @@ ** NOTE: we have a 2D list. The first level of lists represents the ** dimension, the second level, the subscripts accessed for that ** dimension. - ** NOTE: If the subscripts contain at least one meta-var, we completely - ** discard this array-access (by failing) and let the eval-meta-code - ** part take care of it. This is a *dirty* hack to allow declarations - ** using meta-vars. This implies that it's impossible to declare - ** something only partially using meta-vars. :| */ desugar-subscripts = collect-all(?ArrayAccess(_, <id>), conc) // collect gives us the list... ; reverse // ... with deepest array accesses first (we want the opposite) ; prism-desugar - ; if has-meta-vars then fail end // see the 2nd NOTE above. + ; if has-meta-vars then ice(|"desugar-subscripts", "shouldn't be here") end ; map( // traverse the list of dimensions map( // traverse the subscripts for a given dimension if ?Int(_) then Index: tests/xrm/static_rand.xpm --- tests/xrm/static_rand.xpm (revision 0) +++ tests/xrm/static_rand.xpm (revision 0) @@ -0,0 +1 @@ +const int N = static_rand(0, 100); Index: TODO --- TODO (revision 54) +++ TODO (working copy) @@ -13,8 +13,6 @@ * Add tests using "system ... endsystem" (it's properly not parsed atm) - * 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). Factorize current tests with shell functions. @@ -63,8 +61,6 @@ x[1..3]?=0 => x_1=0 | x_2=0 | x_3=0 - NOTE: x[5]?=0 should be considered as an error. - * Add non-static array accesses (as suggested by Micha). For instance: module test x[4] : [0..5]; @@ -145,14 +141,7 @@ ## Documentation ## ## ------------- ## - * Document the return values of xrm-front. - - 1: rewriting failed - - 2: error with meta-vars (eg: undefined meta-var, redefined meta-var) - - 3: arithmetic error when evaluating code (eg: division/modulo by 0) - - 4: invalid call to a builtin (eg rand(1,2,3)) - - 5: invalid array access (eg: subscript is not a positive integer) - - 42: internal compiler error - - 51: not yet implemented + see in the doc/ folder. ## ---- ## ## DONE ## @@ -224,3 +213,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. + + * Write some sort of formal descriptions of the extensions offered. + => see under /doc Index: doc/user-guide.txt --- doc/user-guide.txt (revision 0) +++ doc/user-guide.txt (revision 0) @@ -0,0 +1,392 @@ + ooooooo ooooo ooooooooo. ooo ooooo + `8888 d8' `888 `Y88. `88. .888' + Y888..8P 888 .d88' 888b d'888 + `8888' 888ooo88P' 8 Y88. .P 888 + .8PY888. 888`88b. 8 `888' 888 + d8' `888b 888 `88b. 8 Y 888 + o888o o88888o o888o o888o o8o o888o + eXtended Reactive Modules + + ~ Users' Guide ~ + // FIXME: LaTeXise me + + **************** + * Introduction * + **************** + + // FIXME: An introduction about PRISM and what is/isn't XRM is missing + // here. + + **************** + * Installation * + **************** + + - Requirements: + o Stratego/XT 0.17M1 (at least revision 15278 committed Mon, 29 May 2006) + because of libstratego-gpp (added in Stratego/XT 0.17M1 rev 15278). + o Any version of gcc (3.x or 4.x will do). + o Machine with executable stack (Beware of problems with MacIntel). + o ATerm 2.4.2 or newer. + o SDF2-Bundle 2.3.4 or newer. + + - Using Nix: + Nix is a package management system that ensures safe and complete + installation of packages. + You can get Nix from http://www.cs.uu.nl/wiki/Trace/Nix (pick up the + latest unstable release). + Once Nix is installed, use the following commands (you might need to be + root depending on how you installed nix): + $ nix-channel --add http://nix.cs.uu.nl/dist/stratego/channels-v3/strategoxt-unstable + $ nix-env --install aterm sdf2-bundle strategoxt + There you are! + Add the following line to your .bashrc/.zshrc: + [ -r /nix/etc/profile.d/nix.sh ] && source /nix/etc/profile.d/nix.sh + That's it! + + - Without Nix: + Install ATerm, SDF2 Bundle and Stratego/XT from: + http://www.stratego-language.org/Stratego/ContinuousDistribution + Additional install instructions can be found there. + + - Installing XRM: + o Uncompress the tarball: gunzip -c xrm-version.tar.gz | tar -xf - + o Use the following command to setup a build-tree: + $ cd xrm-version && mkdir _build && cd _build + o Invoke configure to generate the Makefiles + If you use Nix, simply use `../configure' + If you don't use Nix, use `PKG_CONFIG_PATH=P ../configure' where + `P' stands for the path(s) to the directory(ies) where the .pc + files of your Stratego/XT installation were installed. eg: + /usr/lib/pkgconfig/aterm.pc + /usr/lib/pkgconfig/sdf2-bundle.pc + /usr/lib/pkgconfig/stratego*.pc + o Then simply type `make all check' then `make install' + + *************************** + * Tools provided with XRM * + *************************** + + - xrm-front: The front-end provided by XRM will take as input an XRM source + code and will transform it into a standard PRISM source code. + - parse-prism: Parse a PRISM source code and yield an AST in ATerms. + - parse-xrm: Ditto with XRM source code. + - pp-prism: Pretty print ("unparse") a PRISM AST as PRISM source code. + - pp-xrm: Ditto but for XRM. + - prism-to-abox: Transform a PRISM AST into a Box AST for pretty printing. + - xrm-to-abox: Ditto but for XRM. + + ******************* + * Using xrm-front * + ******************* + + xrm-front is the main tool of the XRM package. It will transform a source + written in XRM into a standard PRISM source. + + # Common options + -------------- + The options can be reviewed by invoking xrm-front with the --help argument. + Common options include: + -D | --desugar Desugar the generated PRISM code. + --verbose notice Keep you informed about stages of the pipeline. + -A | --pp-aterm Pretty print output with pp-aterm. + + # Return value + ------------ + xrm-front will return 0 if it succeeds and non zero if an error occured. + Possible return values are: + - 1: rewriting failed (eg: it might be a bug in xrm-front) + - 2: error with meta-vars (eg: undefined meta-var, redefined meta-var) + - 3: arithmetic error when evaluating code (eg: division/modulo by 0) + - 4: invalid call to a builtin (eg rand(1,2,3)) + - 5: invalid array access (eg: subscript is not a positive integer) + - 42: internal compiler error (please send a bug report) + - 51: not yet implemented + + ******************** + * The XRM language * + ******************** + + # Introduction + ------------ + + The specification of the base language is documented in PRISM's manual (a + copy is available in the prism/ directory). + + The XRM language is 100% PRISM compliant and only offers extension to the + language. + + Numerous of the constructs in XRM are `meta' because they cannot be + translated in the PRISM language, thus we must evaluate them at + compile-time (this is xrm-front's job) in order to break them down to + simpler PRISM constructs. + + # XRM Modules + ----------- + + Within XRM modules, it is not mandatory to specify declarations before + commands. They can be freely intertwined in any particular order (whereas + in plain PRISM, declarations must come first and then commands will follow). + The following module is valid in XRM: + + module OutOfOrder + [] x=0 -> (x'=1); + x : [0..1] init 0; + endmodule + + The last step of xrm-front's pipeline is to group all declarations together + at the beginning of the module so that the module will be valid standard + PRISM. + + # XRM Expressions + --------------- + + o XRM has arrays (see below). Array accesses are expressions. + o XRM introduces two operators: "<<" and ">>" which have the same semantics + as in C. They are desugared using calls to the builtin pow. + + TODO: "?=" and "?!=" operators for arrays. + + # XRM Arrays + ---------- + + o It is possible to declare an array of variables instead of a several + variables. Everywhere a variable declaration was allowed in PRISM, an + array declaration is allowed in XRM. + o Arrays can be declared like in C, eg: + x[4] : [0..1] init 0; + will declare an array of 4 elements: x[0], x[1], x[2] and x[3]. + So it's all like in C (access from to 0 through N-1) + o It's possible to declare multidimensional arrays, eg: + x[3][4] : [0..1] init 0; + Again this is *almost* like C with the exception for multidimensional + arrays that intermediate dimensions are not accessible (simply because + they don't exist). So the former declaration will declare: + x[0][0], x[0][1], x[0][2], x[0][3], + x[1][0], x[1][1], x[1][2], x[1][3], + x[2][0], x[2][1], x[2][2], x[2][3] + But in this case accessing x[0] for example doesn't make sense. + o It is also possible to specify manually the dimensions of an array using + lists and ranges, eg: + x[2..4][0,3..5] will declare only: x[2][0], x[2][3], x[2][4], x[2][5], + x[3][0], x[3][3], x[3][4], x[3][5], + x[4][0], x[4][3], x[4][4], x[4][5] + So basically, when one of the dimensions of an array declaration is a + simple integer, eg: x[N] it is expansed in x[0..N]. Then the Cartesian + product of all the dimensions of the array is used to compute the set of + accessible variables. + o Dimensions of size zero are not allowed, eg: x[0] : [0..1]; + o Arrays can also be implicitly declared using for loops (see below, the + section about for loops in XRM). + o Array accesses can be found (nearly) everywhere a simple variable + identifier is allowed in PRISM. + o Update of values in arrays is illustrated in the following example: + [] x[N][M]=0 -> (x[N][M]'=1); + Notice that the prime (') comes after the dimensions of the array access. + o All the subscripts in array accesses must be evaluable down to a simple + positive integer at compile time, eg: + const int N = 3; + // ... + i : [0..42] init 0; // declaration of `i'. + [] x[N+3]=0 -> ...; // valid: N+3 can be worked out at compile time. + [] x[i+3]=0 -> ...; // invalid: the value of `i' is dynamic and unknown + // at compile time. + + TODO: Array accesses with dynamic subscripts. + + # XRM Meta-code + ------------- + + XRM introduces meta-for loops and meta-if statements in the language. + These constructs are said to be `meta' because they are evaluated by + xrm-front and lead to code generation. + + o Meta-for loops can be found in only 2 places within a XRM source file: + * Where we could expect a module declaration. + * Where we could expect a declaration or a command, within a module. + This implies that meta-for loops can only be used to generate modules (or + other file sections, such as formulas, globals, etc.) or commands and + declarations within modules. + o There exists 2 flavors of for loops: + * For loops a la Pascal + * For loops a la Shell + Example: + for i from 0 to 3 do ... end // Pascal-like + for i from 0 to 10 step 2 do ... end // Pascal-like + for i in a, 1+2, N do .. end // Shell-like + In each of these 3 cases, the variable `i' will be considered as a + meta-variable, meaning it will only exists at the meta-level and won't + appear in the final source code. + o For Pascal-like for-loops, the fields `from', `to' and `step' must be + evaluable down to simple integers at compile time. The value of the field + `from' must be less than or equal to that of the field `to'. + o For-loops are unrolled by copying the body of the loop and replacing + every match of the identifier of the meta-var by its successive values. + o For-loops are the only way of declaring a meta-var at the moment. + o For-loops can be used to create new modules. Since each module must have + a unique name, it will have to be suffixed by an array access using a + meta-var, eg: + for i from 1 to 3 do + module dummy[i] + x[i] : [0..1] init 0; + endmodule + end + will generate 3 modules: dummy[1], dummy[2] and dummy[3]. + Of course, since each module has its own unique variables too, the + variables declared in that generated module will also have to be suffixed + by an array access with the meta-var. + In this case though, when `i' gets replaced by its successive values, we + have the following modules: + module dummy[1] + x[1] : [0..1] init 0; // not an array declaration + endmodule + module dummy[2] + x[2] : [0..1] init 0; // ditto + endmodule + module dummy[3] + x[3] : [0..1] init 0; // ditto + endmodule + But fortunately, this will not create 3 times an array called `x'. In + this very special case, the numerical values will not be expansed as + x[0..1] for dummy[1], x[0..2] for dummy[2] and x[0..3] for dummy[3] + because the integer in the array subscript comes from the expansion of a + meta-var and won't be further expanded. + Thus in this case you get 3 different modules, each with their own single + unique variable `x'. + If you wish to provide each module with an array of, say 6 elements, then + do the following: + for i from 1 to 3 do + module dummy[i] + x[i][5] : [0..1] init 0; + endmodule + end + In this case the first dimensions (`i') will first be expansed by the + loop unrolling, which will equip each generated module with its own + unique variable `x' and then the second dimension will be expansed to + 0..5 which will create an array of 6 elements for each generated module. + o Meta-for loops can also be used to declare arrays implicitely: + module ImplicitArray + for i from 0 to 3 do + x[i] : [0..i] init i; + end + endmodule + In this case the module ImplicitArray will have a single array named `x' + of 4 elements. This method offers a greater control on how each element + of the array is declared. + + o Meta-if statements can be found in only 3 places within a XRM source file: + * Where we could expect a module declaration. + * Where we could expect a declaration or a command, within a module. + * Where we would expect an expression. + However the latter case has a restriction that the two formers don't have: + the then-part and the else-part of the if statements cannot contain more + than one expression. + o The syntax for meta-if statements is illustrated in the following example: + if true then + module alwaysGenerated + if 0 = 42 - 21 then + neverGenerated : [0..42] init 0; + else + alwaysGeneratedToo : [0..42] init 0; + end + endmodule + end + o The condition of the meta-if statements must be evaluable at compile + time. It must either be evaluable down to true or false, or down to a + simple integer/double. If that integer/double is 0, the condition will be + false, otherwise it will be true (like in C). Comparison on reals are + done with a precision of 10^-7 which means that if the condition is + reduced down to 0.00000001 (for instance) it will be evaluated as being + false. + + # XRM builtins + ------------ + + XRM introduces two new builtins for generating random numbers: rand and + static_rand. + + o Both rand and static_rand take either one or two arguments which must + be evaluable down to simple integers at compile-time. + If rand or static_rand is called with a single argument, a second + argument (an integer equal to zero) is added. If the single argument + is positive, the zero is added before it, otherwise it's added after + it, eg: + rand(3) will be desugared to rand(0, 3) + rand(-3) will be desugared to rand(-3, 0) + o static_rand(low, hi) will be transformed into a random integer ranging + from `low' to `hi' (included). The random number is obtain with rand(3) + which is seeded with the current UNIX time-stamp when xrm-front starts. + o Calls to static_rand will be evaluated after unrolling of meta-for + loops to ensure that each iteration of the loop gets its own random + number. It will be evaluated earlier if it happens to be used where + a statically evaluable value is required more early in the pipeline + (eg: in meta-if statements' condition, in the fields `from', `to' or + `step' of a meta-for loop, etc.) + o Bear in mind that the random numbers generated by static_rand are + constant from one run to another unless you re-generate the PRISM + source (with xrm-front) each time before running. + o rand(low, hi) will be transformed into a new variable (each call to + rand will generate a new unique variable) which will be controlled by + an external module with a single command: + module testRand => module testRand + x : [0..42] init 0; => x : [0..42] init 0; + [] x=0 -> x'=rand(42); => [] x=0 -> x'=__rand_0; + endmodule => endmodule + => module __rand_0 + => __rand_0 : [0..42]; + => [] true -> 1/43:(__rand_0'=0) + => + 1/43:(__rand_0'=1) + => ... + => + 1/43:(__rand_0'=42); + => endmodule + /!\ This is not a reliable random number generator! + + TODO: The current implementation of rand will be renamed (maybe as + bad_rand or old_rand) and a new reliable implementation will be + provided as a replacement. In this implementation, the random variable + won't be hosted in a foreign module anymore, it will be hosted directly + in the module which called rand. The variable will be updated each time + it's accessed to ensure real random numbers. + + ********************* + * Incoming features * + ********************* + + The following features are not yet implemented (or only partially + implemented or broken). They are ordered in term of the estimated time + needed to successfully implement them. For a complete list of things to be + done please review the TODO file. + - More sanity checks for all declarations at different stages of the + pipeline to ensure that everything is well defined. (variables used have + been declared somewhere etc.) + - Possibility to import another module, eg: import common.pm + - Parameterized formulas. (Pretty much like macro-functions in C) + - Scopes for meta variables (allow redefinitions/shadowing). + - Bound/Type checking (ensure that variables are properly used according to + their type/domain definition). + - Conditional tests on arrays. "?=" and "?!=" operators for arrays. eg: + x[1..3]=0 => x_1=0 & x_2=0 & x_3=0 + x[1..3]?=0 => x_1=0 | x_2=0 | x_3=0 + - Dynamic array accesses, eg: x[i] where `i' is not known at compile-time. + - Array initializations a la C: + x[3] : [0..4] init {0, 1, 2}; + const int array[3] = {0, 1, 2}; + - Better error messages (with the location of error). + + ************** + * Known bugs * + ************** + + - The construct "system ... endsystem" (for system compositions) is broken + at the moment (meaning: using it will result in a parse error). It's + probably a simple problem with the base SDF grammar. I've never seen a + PRISM source using this construct so this has been in the TODO list since + the beginning but with a very low priority. + - Unary operators are allowed in the base language whereas they should not + (because they are not allowed in the original PRISM parser). + - There is nearly no warranty that the generated code will work in PRISM. + Generally speaking, if the input XRM source is correct, the output PRISM + source will also be correct. However, at this stage of the development, + the front-end is still pretty fragile and I am sure it's quite easy to + generate invalid PRISM code without having any error reported by + xrm-front (in this case please report the bug). + What we clearly need to thwart this is: + - Type checking. + - Bound checking. + - Probably many other things. (run make check and see the tests that fail).