May 2006 - Projects

XRM 32: Fix the Makefiles.
by SIGOURE Benoit 25 May '06

25 May '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Fix the Makefiles. * src/tools/Makefile.am: Fix the include of .dep files. * src/lib/xrm/pp/Makefile.am: Ditto. * src/lib/prism/pp/Makefile.am: Ditto. * src/str/Makefile.am: Ditto. * tests/Makefile.am: Don't need to include toplevel.mk. * src/syn/xrm/Makefile.am: Fix the include of .dep files + prevent make distclean from deleting the sources... hehe :| * src/syn/prism/Makefile.am: Ditto. src/lib/prism/pp/Makefile.am | 4 ++-- src/lib/xrm/pp/Makefile.am | 4 ++-- src/str/Makefile.am | 4 ++-- src/syn/prism/Makefile.am | 8 ++++---- src/syn/xrm/Makefile.am | 8 ++++---- src/tools/Makefile.am | 4 ++-- tests/Makefile.am | 4 ++-- 7 files changed, 18 insertions(+), 18 deletions(-) Index: src/tools/Makefile.am --- src/tools/Makefile.am (revision 31) +++ src/tools/Makefile.am (working copy) @@ -5,11 +5,11 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Mon May 8 21:16:56 2006 SIGOURE Benoit -## Last update Fri May 12 13:35:58 2006 SIGOURE Benoit +## Last update Thu May 25 17:28:02 2006 SIGOURE Benoit ## include $(top_srcdir)/config/Transformers.mk -include $(wildcard *.dep) +-include $(wildcard *.dep) bin_PROGRAMS = \ parse-prism \ Index: src/lib/xrm/pp/Makefile.am --- src/lib/xrm/pp/Makefile.am (revision 31) +++ src/lib/xrm/pp/Makefile.am (working copy) @@ -5,11 +5,11 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Wed May 10 19:27:12 2006 SIGOURE Benoit -## Last update Fri May 12 05:35:52 2006 SIGOURE Benoit +## Last update Thu May 25 17:27:04 2006 SIGOURE Benoit ## include $(top_srcdir)/config/toplevel.mk -include $(wildcard *.dep) +-include $(wildcard *.dep) pkgdata_DATA = xrm-parenthesize.str libexec_PROGRAMS = xrm-to-abox Index: src/lib/prism/pp/Makefile.am --- src/lib/prism/pp/Makefile.am (revision 31) +++ src/lib/prism/pp/Makefile.am (working copy) @@ -5,11 +5,11 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Wed May 10 19:27:12 2006 SIGOURE Benoit -## Last update Fri May 12 05:23:29 2006 SIGOURE Benoit +## Last update Thu May 25 17:26:51 2006 SIGOURE Benoit ## include $(top_srcdir)/config/toplevel.mk -include $(wildcard *.dep) +-include $(wildcard *.dep) pkgdata_DATA = prism-parenthesize.str libexec_PROGRAMS = prism-to-abox Index: src/str/Makefile.am --- src/str/Makefile.am (revision 31) +++ src/str/Makefile.am (working copy) @@ -5,11 +5,11 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Thu Apr 27 17:59:35 2006 SIGOURE Benoit -## Last update Thu May 18 16:49:50 2006 SIGOURE Benoit +## Last update Thu May 25 17:27:20 2006 SIGOURE Benoit ## include $(top_srcdir)/config/Transformers.mk -include $(wildcard *.dep) +-include $(wildcard *.dep) bin_PROGRAMS = xrm-front xrm_SOURCES = xrm-front.c Index: src/syn/xrm/Makefile.am --- src/syn/xrm/Makefile.am (revision 31) +++ src/syn/xrm/Makefile.am (working copy) @@ -5,11 +5,11 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Thu Apr 27 17:40:41 2006 SIGOURE Benoit -## Last update Thu May 18 16:53:05 2006 SIGOURE Benoit +## Last update Thu May 25 17:28:59 2006 SIGOURE Benoit ## include $(top_srcdir)/config/Transformers.mk -include $(wildcard *.dep) +-include $(wildcard *.dep) PGEN_FLAGS = -m $* SDF2RTG_FLAGS = -m $* @@ -38,8 +38,8 @@ CLEANFILES = $(pkgdata_DATA_built) \ $(wildcard *.dep) \ XRM.{c,str,c.dep} \ - XRM-StartSymbols.sdf \ - XRM-Prefixed.sdf + XRM-StartSymbols.def \ + XRM-Prefixed.def SDFS = XRM-Expression.sdf \ XRM-Main.sdf \ Index: src/syn/prism/Makefile.am --- src/syn/prism/Makefile.am (revision 31) +++ src/syn/prism/Makefile.am (working copy) @@ -5,11 +5,11 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Thu Apr 27 17:40:41 2006 SIGOURE Benoit -## Last update Thu May 18 16:52:52 2006 SIGOURE Benoit +## Last update Thu May 25 17:28:59 2006 SIGOURE Benoit ## include $(top_srcdir)/config/Transformers.mk -include $(wildcard *.dep) +-include $(wildcard *.dep) PGEN_FLAGS = -m $* SDF2RTG_FLAGS = -m $* @@ -36,8 +36,8 @@ CLEANFILES = $(pkgdata_DATA_built) \ $(wildcard *.dep) \ PRISM.{c,str,c.dep} \ - PRISM-StartSymbols.sdf \ - PRISM-Prefixed.sdf + PRISM-StartSymbols.def \ + PRISM-Prefixed.def SDFS = PRISM-Command.sdf \ PRISM-Constant.sdf \ Index: tests/Makefile.am --- tests/Makefile.am (revision 31) +++ tests/Makefile.am (working copy) @@ -5,10 +5,10 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Thu Apr 27 16:56:50 2006 SIGOURE Benoit -## Last update Tue May 16 04:04:35 2006 SIGOURE Benoit +## Last update Thu May 25 17:29:32 2006 SIGOURE Benoit ## -include $(top_srcdir)/config/toplevel.mk +#include $(top_srcdir)/config/toplevel.mk dist_check_SCRIPTS = \ test-parse-prism.sh \

2 1

XRM 31: Add array declarations (sugar).
by SIGOURE Benoit 24 May '06

24 May '06

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

1 0

havm 168: Close all opened file handles before leaving.
by Roland Levillain 24 May '06

24 May '06

https://svn.lrde.epita.fr/svn/havm/trunk Index: ChangeLog from Roland Levillain <roland(a)lrde.epita.fr> Close all opened file handles before leaving. * src/Main.hs (closeHandle): New function. (evalM): Use it to close all opened file handles. Main.hs | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) Index: src/Main.hs --- src/Main.hs (revision 167) +++ src/Main.hs (working copy) @@ -101,7 +101,14 @@ storeHandle ph else return () +-- Close a (maybe) file handle. +closeHandle :: Maybe Handle -> Mnd () +closeHandle mh = + case mh of + Just h -> lift $ hClose h + Nothing -> return () +-- Evaluate the program. evalM :: Map String OptVal -> [Stm Ann] -> Mnd () evalM fm stms = do optset "low" $ findWithDefault (BVal False) "low" fm @@ -121,10 +128,9 @@ trace ["evaling"] evalExp $ Call NoAnn (Name NoAnn "main") [] profileM - mph <- getProfileHandle - case mph of - Just ph -> lift $ hClose ph - Nothing -> return () + getProfileHandle >>= closeHandle + getDisplayHandle >>= closeHandle + getTraceHandle >>= closeHandle main :: IO () main =

1 0

Des échecs de la build farm
by Akim Demaille 24 May '06

24 May '06

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.

2 1

Re: XRM 30: Correct some typos and add things to do.
by michael.cadilhac＠lrde.org 24 May '06

24 May '06

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 | `-- - - - - --'

1 0

XRM 30: Correct some typos and add things to do.
by SIGOURE Benoit 23 May '06

23 May '06

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)

1 0

[build-farm] 286: Change VCSN related compilation stuffs.
by michael.cadilhac＠lrde.org 23 May '06

23 May '06

demos précisé à la main car c'est désormais une règle à part. Index: caracas.fns =================================================================== --- caracas.fns (revision 285) +++ caracas.fns (working copy) @@ -12,18 +12,18 @@ CXX=g++-3.4 CC=gcc-3.4 -test_tree vaucanson +test_tree vaucanson bootstrap configure build demos install distcheck CC=gcc-4.0 CXX=g++-4.0 -test_tree vaucanson-gcc4.0 +test_tree vaucanson-gcc4.0 bootstrap configure build demos install distcheck CC=icpc # fixme: to remove ccache CXX=icpc -CXXFLAGS="-D_LINUX -cxxlib-icc -I/home/lrde/admin/lrde/usr/include/c++/" +export CXXFLAGS="-D_LINUX -cxxlib-icc -I/home/lrde/admin/lrde/usr/include/c++/" PATH=$PATH:/home/lrde/admin/lrde/usr/bin export LD_LIBRARY_PATH=/home/lrde/admin/lrde/usr/lib/ -test_tree vaucanson-icc +test_tree vaucanson-icc bootstrap configure build demos install distcheck CXX=g++ test_tree ranch

2 3

Vcs configuration
by Roland Levillain 23 May '06

23 May '06

I've extended the Vcs Wiki page to document the essential environment variables it relies on. It should help users to start using Vcs. http://www.lrde.epita.fr/cgi-bin/twiki/view/Projects/Vcs

2 2

Re: XRM 27: Add meta code evaluation [debug version].
by Akim Demaille 22 May '06

22 May '06

>>> "SIGOURE" == SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes: > 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 C'est la fête !

2 1

Re: XRM 27: Add meta code evaluation [debug version].
by Akim Demaille 22 May '06

22 May '06

>>> "SIGOURE" == SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes: > + 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")} Je comprends pas bien ce que tu veux dire.

2 1