Projects

projects@lrde.epita.fr

1049 discussions

Re: XRM 26: Add MetaModules and some other extensions.

by Akim Demaille

>>> "SIGOURE" == SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes: > Index: src/syn/xrm/XRM-Arrays.sdf > --- src/syn/xrm/XRM-Arrays.sdf (revision 0) > +++ src/syn/xrm/XRM-Arrays.sdf (revision 0) > @@ -0,0 +1,19 @@ > +module XRM-Arrays > +imports > + PRISM-to-XRM > +exports > + > + %% EBNF Grammar: Arrays > + %% ArrayAccess ::= Identifier ArraySubscript {ArraySubscript} > + %% > + %% ArraySubscript ::= "[" Identifier "]" > + > + sorts ArrayAccess ArraySubscript > + context-free syntax > + Identifier ArraySubscript+ -> ArrayAccess {cons("ArrayAccess")} > + "[" Identifier "]" -> ArraySubscript {bracket} Ceci n'est pas suffisant à plusieurs titres : - tableaux multidimensionnels - expressions plutôt qu'ID comme indices mais je suppose que c'est seulement le temps de passer à plus grande échelle. C'est vraiment du beau travail. > + %% Note: why use bracket here? Tu devrais préciser que tu parles de l'annotation, sinon c'est pas clair. > + %% This is a work around. In SDF, if a production contains literals, > + %% a constructor is required. With brackets, we specify that literals > + %% are allowed there, however this does not create a node in the AST. Je vois pas en quoi ça fait de ça un work-around :)

18 years, 7 months

XRM 42: Extend meta for loops + fix the XRM rand builtin.

by SIGOURE Benoit

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Extend meta for loops + fix the XRM rand builtin. Revision 42 \o/ The fields `from', `to' and `step' of meta for loops can now contain any expression as long as it's statically evaluable down to a simple Int. The first pass of xrm-to-prism now desugar Plus(Int(i)) to Int(i) and Minus(Int(i)) to Int(-i). This plus the previous change allows for loops to use negative numbers (eg: for i from -4 to -1 do ... end) * src/lib/xrm/pp/xrm-to-abox.str: Update a comment. * src/lib/prism/pp/prism-to-abox.str: Ditto. * src/str/xrm-to-prism.str: Move the rand builtin in another file. Handle unary operators to ease transformations. * src/str/builtin-rand.str: New. * src/str/builtin-rand.meta: New. * src/str/eval-meta-code.str: Extend for loops (as said above). * src/syn/xrm/XRM-MetaFor.sdf: Ditto. * src/str/xrm-front.str: Update the help message. * src/syn/prism/PRISM-Expression.sdf: Update a comment. * TODO: More things to do... TODO | 19 +++++++-- src/lib/prism/pp/prism-to-abox.str | 2 - src/lib/xrm/pp/xrm-to-abox.str | 2 - src/str/builtin-rand.meta | 1 src/str/builtin-rand.str | 74 +++++++++++++++++++++++++++++++++++++ src/str/eval-meta-code.str | 34 +++++++++++++---- src/str/xrm-front.str | 4 +- src/str/xrm-to-prism.str | 68 ++++++++++------------------------ src/syn/prism/PRISM-Expression.sdf | 9 ++-- src/syn/xrm/XRM-MetaFor.sdf | 16 +++++--- 10 files changed, 155 insertions(+), 74 deletions(-) Index: src/lib/xrm/pp/xrm-to-abox.str --- src/lib/xrm/pp/xrm-to-abox.str (revision 41) +++ src/lib/xrm/pp/xrm-to-abox.str (working copy) @@ -54,7 +54,7 @@ // because we simply extend it pp-xrm-to-abox(pprules) = - // strategy generated in prism-parenthesize.str by sdf2parenthesize + // strategy from xrm-parenthesize.str generated by sdf2parenthesize parenthesize-XRM ; topdown(try(very-special-conflict)) ; topdown(try(repeat(pprules))) Index: src/lib/prism/pp/prism-to-abox.str --- src/lib/prism/pp/prism-to-abox.str (revision 41) +++ src/lib/prism/pp/prism-to-abox.str (working copy) @@ -47,7 +47,7 @@ pp-prism-to-abox(prism-to-box) pp-prism-to-abox(pprules) = - // strategy generated in prism-parenthesize.str by sdf2parenthesize + // strategy from prism-parenthesize.str generated by sdf2parenthesize parenthesize-PRISM ; topdown(try(very-special-conflict)) ; topdown(try(repeat(pprules))) Index: src/str/xrm-to-prism.str --- src/str/xrm-to-prism.str (revision 41) +++ src/str/xrm-to-prism.str (working copy) @@ -17,6 +17,9 @@ ** - ExpandFormulas: created by the strategy collect-formulas and used by ** prism-desugar for constant propagation. Maps an identifier with an ** expression. +** - RandGenModules: each call to the XRM builtin rand generates a module +** which is stored in this DR. Just before xrm-to-prism finishes, we +** paste these modules at the end of the source code. */ module xrm-to-prism imports @@ -26,13 +29,15 @@ check-meta-vars eval-meta-code array-decl-desugar + builtin-rand strategies xrm-to-prism = /* remove XRM sugar, normalize some nodes */ innermost( - DesugarRightShift <+ DesugarLeftShift + DesugarUnaryOps // keep this first + <+ DesugarRightShift <+ DesugarLeftShift <+ DesugarImplicitForStep <+ DesugarImplicitElse <+ DesugarRand <+ EvalRand ) @@ -62,20 +67,32 @@ ; ModulesFile(id, flatten-list) ; ModulesFile(id, map(try(Module(id, flatten-list)))) - /* get the list of generated modules that generates random numbers */ + /* get the modules that generates random numbers (XRM rand builtin) */ ; where(bagof-RandGenModules; reverse => rand-gen-modules) - /* add the modules that generates random numbers in the ModulesFile */ + /* paste them at the end of the file */ ; ModulesFile(id, <conc>(<id>, rand-gen-modules)) /* remove array accesses: x[i] -> x_i */ - ; topdown(try(remove-array-accesses)) + ; bottomup(try(remove-array-accesses)) /* re-order modules so that all declarations appear before commands */ ; ModulesFile(id, map(try(reorder-module-contents))) rules + DesugarUnaryOps: + Plus(Int(i)) -> Int(i) + + DesugarUnaryOps: + Plus(Double(i)) -> Double(i) + + DesugarUnaryOps: + Minus(Int(i)) -> Int(j) where <mulS>(i, "-1") => j + + DesugarUnaryOps: + Minus(Double(i)) -> Double(j) where <mulS>(i, "-1") => j + DesugarRightShift: |[ e1 >> e2 ]| -> |[ e1 / func(pow, 2, e2) ]| @@ -92,51 +109,8 @@ //|[ if e then s* end ]| -> |[ if e then s* else end ]| MetaIf(e, m*) -> MetaIf(e, m*, []) - /** rand(x) -> rand(0, x) */ - DesugarRand: - Rand([arg]) -> Rand([Int("0"), arg]) - - EvalRand: - Rand(args) -> Identifier(rand-var) - where ?current-term - ; if not( !args => [from, to] ) then - err-msg(|<concat-strings>["invalid call to XRM builtin: rand", - " takes either one or two arguments"]) - ; !current-term; debug; <xtc-exit> 4 - end - ; <prism-desugar> from => from' - ; <prism-desugar> to => to' - ; if not( !from' => Int(ifrom); !to' => Int(ito) ) then - err-msg(|<concat-strings>["invalid call to XRM builtin: rand's", - " arguments must be statically evaluable"]) - ; !current-term; debug; <xtc-exit> 4 - end - ; <debug> ifrom - ; <debug> ito - ; <newname> "__rand" => rand-var - ; !ProbUpdate( Div(Int("1"), Int( <subtS>(ito, ifrom) )) - , UpdateList([UpdateElement(IdentifierPrime(rand-var), FIXME())])) - ; {| RandUpdateList: - for-loop(gen-rand-update-list | ifrom, ito, "1", []) - ; bagof-RandUpdateList - |} - ; reverse - ; !ProbUpdateList(<id>) => u - ; !|[ module ~id:rand-var - ~id:rand-var : [~int:ifrom..~int:ito]; - [] true -> u; - endmodule ]| => rand-gen-module - ; rules(RandGenModules:+ _ -> rand-gen-module) - -strategies - - gen-rand-update-list(|i, data) = - topdown(try(\ FIXME() -> Int(i) \)) => rand-update - ; rules(RandUpdateList:+ _ -> rand-update) - signature constructors Type : String -> Type - FIXME : FIXME strategies Index: src/str/eval-meta-code.str --- src/str/eval-meta-code.str (revision 41) +++ src/str/eval-meta-code.str (working copy) @@ -9,7 +9,7 @@ ** Sorry if it makes the source a bit overloaded with comments. ** ** If you want to enable debugging simply use: -** sed 's@///\*@/*@g' < eval-meta-code.str > .tmp +** sed 's@/\*@/*@g' < eval-meta-code.str > .tmp ** mv .tmp eval-meta-code.str */ module eval-meta-code @@ -48,15 +48,26 @@ strategies unroll-meta-loops = - ?MetaFor(meta-var, Int(from), Int(to), Int(step), body) - ; where(check-loop-validity(|meta-var, from, to)) + ?MetaFor(meta-var, from, to, step, body) + /* reduce the fields from to and step down to simple integers */ + ; where( <prism-desugar> from => from' + ; <prism-desugar> to => to' + ; <prism-desugar> step => step' + ) + /* check whether the loop is valid */ + ; where(check-loop-validity(|meta-var, from', to', step')) + /* bind the integers of the fields from to and step */ + ; where(!from' => Int(ifrom) + ; !to' => Int(ito) + ; !step' => Int(istep) + ) ; {| MetaCode: ///*DEBUG*/say(!" @@@ unroll-meta-loops: starting:") ///*DEBUG*/; printf(|" meta-var = ", meta-var) - ///*DEBUG*/; printf(|" from = ", from) - ///*DEBUG*/; printf(|" to = ", to); + ///*DEBUG*/; printf(|" from = ", ifrom) + ///*DEBUG*/; printf(|" to = ", ito); where(<check-meta-var-unicity> meta-var) - ; for-loop(gen-meta-code | from, to, step, []) + ; for-loop(gen-meta-code | ifrom, ito, istep, []) ///*DEBUG*/; say(!" ~~~ unroll-meta-loops: before bagof-MetaModule") ///*DEBUG*/; debug ; bagof-MetaCode @@ -65,8 +76,15 @@ ///*DEBUG*/; debug |} - check-loop-validity(|meta-var, from, to) = - if <gtS>(from, to) then + check-loop-validity(|meta-var, from, to, step) = + if not(!from => Int(_); !to => Int(_); !step => Int(_)) then + err-msg(|<concat-strings>["invalid meta for loop: the value of the ", + "fields `from', `to' and `step' must be ", + "statically evaluable down to a ", + "simple integer"]) + ; <xtc-exit> 2 + end + ; if <gtS>(from, to) then !meta-var => Identifier(idf) ; err-msg(|<concat-strings>["bad `for' loop on the meta-var ", idf, " starts at ", from, Index: src/str/builtin-rand.str --- src/str/builtin-rand.str (revision 0) +++ src/str/builtin-rand.str (revision 0) @@ -0,0 +1,74 @@ +/** +** This sub-module handles the XRM builtin rand. +** rand(x) generates a random value (at runtime) between 0 and x (inclusive) +** rand(x) is first desugared to rand(0, x). +** rand(x, y) generates a random value between x and y (inclusive). +** +** Here is how it works with rand(y, x) +** 1. Check that rand is called with the correct number of arguments. +** 2. Apply prism-desugar to those arguments in order to reduce them down +** to simple integers [Int(..)] +** 3. Generate a module with a single command which have a list of updates +** which the same probability [1/(x-y+1)] +*/ +module builtin-rand + +rules + + /** rand(x) -> rand(0, x) */ + DesugarRand: + Rand([arg]) -> Rand([Int("0"), arg]) + + EvalRand: + Rand(args) -> Identifier(rand-var) + where ?current-term // save the current term for error messages + /* check that rand is called with exactly two arguments */ + ; if not( !args => [from, to] ) then + err-msg(|<concat-strings>["invalid call to XRM builtin: rand", + " takes either one or two arguments"]) + ; !current-term; debug; <xtc-exit> 4 + end + /* desugar (constant propagation) to make both arguments simple Int */ + ; <prism-desugar> from => from' + ; <prism-desugar> to => to' + /* check that both arguments are simple Int */ + ; if not( !from' => Int(ifrom); !to' => Int(ito) ) then + err-msg(|<concat-strings>["invalid call to XRM builtin: rand's", + " arguments must be statically evaluable"]) + ; !current-term; debug; <xtc-exit> 4 + end + ; if <gtS>(ifrom, ito) then + err-msg(|<concat-strings>["invalid call to XRM builtin: ", + "rand(x,y) where x > y"]) + ; !current-term; debug; <xtc-exit> 4 + end + /* generate a name for the random variable */ + ; <newname> "__rand" => rand-var + /* template: 1/(ito-ifrom+1):(rand-var'=FIXME) */ + ; !ProbUpdate( Div(Int("1"), Int( <addS>(<subtS>(ito, ifrom), "1") )) + , UpdateList([UpdateElement(IdentifierPrime(rand-var), FIXME())])) + /* generate the updates by replacing the FIXME */ + ; {| RandUpdateList: + for-loop(gen-rand-update-list | ifrom, ito, "1", []) + ; bagof-RandUpdateList + |} + ; reverse // bagof gives us the list in reverse order + /* put our update list in the correct AST node */ + ; !ProbUpdateList(<id>) => u + /* inject that node in a module */ + ; !|[ module ~id:rand-var + ~id:rand-var : [~int:ifrom..~int:ito]; + [] true -> u; + endmodule ]| => rand-gen-module + /* save this module in a DR for later retrieval */ + ; rules(RandGenModules:+ _ -> rand-gen-module) + +strategies + + gen-rand-update-list(|i, data) = + topdown(try(\ FIXME() -> Int(i) \)) => rand-update + ; rules(RandUpdateList:+ _ -> rand-update) + +/* node to replace in templates */ +signature constructors + FIXME : FIXME Index: src/str/xrm-front.str --- src/str/xrm-front.str (revision 41) +++ src/str/xrm-front.str (working copy) @@ -133,8 +133,8 @@ <tool-doc> [ Usage("xrm-front [OPTIONS]") , Summary("Transforms an eXtended Reactive Module source file in a - PRISM-equivalent abstract syntax tree (default) or source - code. (see option -P)") + PRISM-equivalent source code (default) or abstract syntax + tree. (see option -A)") , OptionUsage() , AutoReportBugs() ] Index: src/str/builtin-rand.meta --- src/str/builtin-rand.meta (revision 0) +++ src/str/builtin-rand.meta (revision 0) @@ -0,0 +1 @@ +Meta([Syntax("StrategoXRM")]) Index: src/syn/xrm/XRM-MetaFor.sdf --- src/syn/xrm/XRM-MetaFor.sdf (revision 41) +++ src/syn/xrm/XRM-MetaFor.sdf (working copy) @@ -7,27 +7,31 @@ %% EBNF Grammar: Meta For Loops %% (* Meta For loops at the top level *) %% ModulesFileSection ::= - %% "for" Identifier "from" Int "to" Int ["step" Int] "do" + %% "for" Identifier "from" Expression "to" Expression + %% ["step" Expression] "do" %% {ModulesFileSection} "end" %% %% (* Meta For loops inside modules *) %% DeclarationOrCommand ::= - %% "for" Identifier "from" Int "to" Int ["step" Int] "do" + %% "for" Identifier "from" Expression "to" Expression + %% ["step" Expression] "do" %% {DeclarationOrCommand} "end" context-free syntax %% This MetaFor can be found only at top-level %% So we can see it as a ModulesFileSection - "for" Identifier "from" Int "to" Int "do" ModulesFileSection* "end" + "for" Identifier "from" Expression "to" Expression "do" + ModulesFileSection* "end" -> ModulesFileSection {cons("MetaFor")} - "for" Identifier "from" Int "to" Int "step" Int "do" + "for" Identifier "from" Expression "to" Expression "step" Expression "do" ModulesFileSection* "end" -> ModulesFileSection {cons("MetaFor")} %% This MetaFor can be found only inside Modules %% So we can see it as a DeclarationOrCommand - "for" Identifier "from" Int "to" Int "do" DeclarationOrCommand* "end" + "for" Identifier "from" Expression "to" Expression "do" + DeclarationOrCommand* "end" -> DeclarationOrCommand {cons("MetaFor")} - "for" Identifier "from" Int "to" Int "step" Int "do" + "for" Identifier "from" Expression "to" Expression "step" Expression "do" DeclarationOrCommand* "end" -> DeclarationOrCommand {cons("MetaFor")} Index: src/syn/prism/PRISM-Expression.sdf --- src/syn/prism/PRISM-Expression.sdf (revision 41) +++ src/syn/prism/PRISM-Expression.sdf (working copy) @@ -27,8 +27,8 @@ %% | Expression ">=" Expression %% | Expression ">" Expression %% (* Notations for describing ranges in tests *) - %% | Expression "=" (Single | Range) {Single | Range} - %% | Expression "!=" (Single | Range) {Single | Range} + %% | Expression "=" Range {"," Range} + %% | Expression "!=" Range {"," Range} %% | "!" Expression %% | Expression "&" Expression %% | Expression "|" Expression @@ -46,9 +46,8 @@ %% | "func" "(" "floor" "," Expression {"," Expression} ")" %% | "func" "(" "ceil" "," Expression {"," Expression} ")" %% - %% Single ::= Expression - %% - %% Range ::= Expression ".." Expression + %% Range ::= Expression + %% | Expression ".." Expression %% EBNF Grammar: Expressions as in PRISM's parser %% Expression ::= ExpressionITE Index: TODO --- TODO (revision 41) +++ TODO (working copy) @@ -31,6 +31,8 @@ static const int N = -1; will issue an error such as "undeclared meta variable N" whereas the real problem is that array[N] couldn't be expanded. + * Labels seems to be b0rken in parse-prism. + ## ---------- ## ## Extensions ## ## ---------- ## @@ -48,10 +50,6 @@ declared variables (globals, formulas, local declarations etc.) and ensure (in check-meta-vars) that their identifiers are unique. - * Add a "rand" builtin. Eg: - rand(50) -> random value between 0 and 50 (included) - rand(42, 50) -> random value between 42 and 50 (included) - * 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. @@ -103,6 +101,14 @@ * Add parameterized formulas. (Pretty much like macro-functions in C) + * Check why for i from -1 to -4 is not caught as an error. + + * Add scopes for meta variables + eg: for i ... do + for i ... // `i' shadows its previous definition + end + end + ## -------------- ## ## Desugarisation ## ## -------------- ## @@ -137,6 +143,7 @@ - 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 @@ -196,3 +203,7 @@ * Desugarise ranges (?) x = 1..5,7,10..13 ==> (x>=1 & x<=5) | (x=7) | (x>=10 & x<=13) + + * Add a "rand" builtin. Eg: + rand(50) -> random value between 0 and 50 (included) + rand(42, 50) -> random value between 42 and 50 (included)

18 years, 7 months

Re: XRM 32: Fix the Makefiles.

by michael.cadilhac＠lrde.org

SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes: > 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 > ## Please don't use such headers. SVN $Id$ is here for you. Parce que bon, tu peux pas demander à tes contributeurs d'installer les .el Épita ;-) -- | Pour les 35-40 ans, l'humour Michaël `Micha' Cadilhac | | c'est une plus-value. cadilh_m - Epita 2007 - CSI | | -- Guillaume L. JID: micha(a)amessage.be | `-- - - - - --'

18 years, 7 months

Re: XRM 41: Add the rand() builtin.

by michael.cadilhac＠lrde.org

SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes: > https://svn.lrde.epita.fr/svn/xrm/trunk > > > Index: ChangeLog > from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> > > Add the rand() builtin. > > * src/lib/xrm/pp/xrm-expression.str: Add boxing for the rand builtin. > * src/str/xrm-to-prism.str: Split xrm-to-prism-desugar in several > rules. Add rand(N) and rand(from, to) builtin. > * src/str/ice.str: Add not-implemented() strategy. > * src/str/eval-meta-code.str: Nothing. > * src/syn/xrm/XRM-Expression.sdf: Add the rand builtin. > * src/syn/prism/PRISM-MetaVars.sdf: Add a meta-var. > * src/syn/prism/StrategoPRISM.sdf: Ditto. > * tests/xrm/rand.xpm: New. > * tests/prism/formula.pm: New. > * TODO: Update. Marvelous, thanks a lot ! Et mes amitiés à ta copine ! ;-) -- | La culture c'est comme la confiture, Michaël `Micha' Cadilhac | | c'est meilleur avec du pain. cadilh_m - Epita 2007 - CSI | | -- MOI59 JID: micha(a)amessage.be | `-- - - - - --'

18 years, 7 months

build-farm 288 and 289: Update caracas.

by michael.cadilhac＠lrde.org

Les nouveaux flags pour ICC sont : # Don't use CXXFLAGS, it's CPP and LD stuffs. export CPPFLAGS="-D_LINUX -I/home/lrde/admin/lrde/usr/intel/compiler90/include/c++/" export LDFLAGS="-cxxlib-icc" export LD_LIBRARY_PATH=/home/lrde/admin/lrde/usr/intel/compiler90/include/lib/ PATH=/home/lrde/admin/lrde/usr/intel/compiler90/bin:$PATH test_tree vaucanson-icc bootstrap configure build demos install distcheck C'est obligatoire car VCSN détruit les CXXFLAGS pour une partie du make check. -- | Would someone please DTRT with this, Michaël `Micha' Cadilhac | | then ACK? cadilh_m - Epita 2007 - CSI | | -- Richard Stallman JID: micha(a)amessage.be | `-- - - - - --'

18 years, 7 months

XRM 41: Add the rand() builtin.

by SIGOURE Benoit

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Add the rand() builtin. * src/lib/xrm/pp/xrm-expression.str: Add boxing for the rand builtin. * src/str/xrm-to-prism.str: Split xrm-to-prism-desugar in several rules. Add rand(N) and rand(from, to) builtin. * src/str/ice.str: Add not-implemented() strategy. * src/str/eval-meta-code.str: Nothing. * src/syn/xrm/XRM-Expression.sdf: Add the rand builtin. * src/syn/prism/PRISM-MetaVars.sdf: Add a meta-var. * src/syn/prism/StrategoPRISM.sdf: Ditto. * tests/xrm/rand.xpm: New. * tests/prism/formula.pm: New. * TODO: Update. TODO | 12 +++++++ src/lib/xrm/pp/xrm-expression.str | 6 +++ src/str/eval-meta-code.str | 2 - src/str/ice.str | 14 ++++++++ src/str/xrm-to-prism.str | 63 ++++++++++++++++++++++++++++++++++---- src/syn/prism/PRISM-MetaVars.sdf | 1 src/syn/prism/StrategoPRISM.sdf | 1 src/syn/xrm/XRM-Expression.sdf | 9 +++++ tests/prism/formula.pm | 6 +++ tests/xrm/rand.xpm | 12 +++++++ 10 files changed, 120 insertions(+), 6 deletions(-) Index: src/lib/xrm/pp/xrm-expression.str --- src/lib/xrm/pp/xrm-expression.str (revision 40) +++ src/lib/xrm/pp/xrm-expression.str (working copy) @@ -1,4 +1,5 @@ module xrm-expression +imports helpers rules @@ -7,3 +8,8 @@ prism-to-box: LeftShift(lhs, rhs) -> H hs=1 [~lhs MATH["<<"] ~rhs] + + prism-to-box: // NOTE: we use the old builtin-call style + Rand(args) // func(rand, ...) is just uggly. + -> box |[ H hs=0 [ "rand" "(" H hs=1 [ ~args-imploded ] ")" ] ]| + where <implode-list(|",")> args => args-imploded Index: src/str/xrm-to-prism.str --- src/str/xrm-to-prism.str (revision 40) +++ src/str/xrm-to-prism.str (working copy) @@ -31,7 +31,11 @@ xrm-to-prism = /* remove XRM sugar, normalize some nodes */ - innermost(xrm-to-prism-desugar) + innermost( + DesugarRightShift <+ DesugarLeftShift + <+ DesugarImplicitForStep <+ DesugarImplicitElse + <+ DesugarRand <+ EvalRand + ) /* Collect static const variables * Two goals: expand them if needed, look for variable name conflicts. */ @@ -58,6 +62,12 @@ ; ModulesFile(id, flatten-list) ; ModulesFile(id, map(try(Module(id, flatten-list)))) + /* get the list of generated modules that generates random numbers */ + ; where(bagof-RandGenModules; reverse => rand-gen-modules) + + /* add the modules that generates random numbers in the ModulesFile */ + ; ModulesFile(id, <conc>(<id>, rand-gen-modules)) + /* remove array accesses: x[i] -> x_i */ ; topdown(try(remove-array-accesses)) @@ -66,24 +76,67 @@ rules - xrm-to-prism-desugar: + DesugarRightShift: |[ e1 >> e2 ]| -> |[ e1 / func(pow, 2, e2) ]| - xrm-to-prism-desugar: + DesugarLeftShift: |[ e1 << e2 ]| -> |[ e1 * func(pow, 2, e2) ]| /** if the step is not specified, it is implicitly set to 1 */ - xrm-to-prism-desugar: + DesugarImplicitForStep: MetaFor(identifier, from, to, body) -> MetaFor(identifier, from, to, Int("1"), body) - xrm-to-prism-desugar: + DesugarImplicitElse: //|[ if e then m* end ]| -> |[ if e then m* else end ]| //|[ if e then s* end ]| -> |[ if e then s* else end ]| MetaIf(e, m*) -> MetaIf(e, m*, []) + /** rand(x) -> rand(0, x) */ + DesugarRand: + Rand([arg]) -> Rand([Int("0"), arg]) + + EvalRand: + Rand(args) -> Identifier(rand-var) + where ?current-term + ; if not( !args => [from, to] ) then + err-msg(|<concat-strings>["invalid call to XRM builtin: rand", + " takes either one or two arguments"]) + ; !current-term; debug; <xtc-exit> 4 + end + ; <prism-desugar> from => from' + ; <prism-desugar> to => to' + ; if not( !from' => Int(ifrom); !to' => Int(ito) ) then + err-msg(|<concat-strings>["invalid call to XRM builtin: rand's", + " arguments must be statically evaluable"]) + ; !current-term; debug; <xtc-exit> 4 + end + ; <debug> ifrom + ; <debug> ito + ; <newname> "__rand" => rand-var + ; !ProbUpdate( Div(Int("1"), Int( <subtS>(ito, ifrom) )) + , UpdateList([UpdateElement(IdentifierPrime(rand-var), FIXME())])) + ; {| RandUpdateList: + for-loop(gen-rand-update-list | ifrom, ito, "1", []) + ; bagof-RandUpdateList + |} + ; reverse + ; !ProbUpdateList(<id>) => u + ; !|[ module ~id:rand-var + ~id:rand-var : [~int:ifrom..~int:ito]; + [] true -> u; + endmodule ]| => rand-gen-module + ; rules(RandGenModules:+ _ -> rand-gen-module) + +strategies + + gen-rand-update-list(|i, data) = + topdown(try(\ FIXME() -> Int(i) \)) => rand-update + ; rules(RandUpdateList:+ _ -> rand-update) + signature constructors Type : String -> Type + FIXME : FIXME strategies Index: src/str/ice.str --- src/str/ice.str (revision 40) +++ src/str/ice.str (working copy) @@ -20,3 +20,17 @@ ; !term ; debug ; <xtc-exit> 42 + + /** Things that should work but are not yet supported. */ + not-implemented(|calling-strategy-name, what) = + err-msg(|<concat-strings>["not yet implemented: ", what, " (in strategy ", + calling-strategy-name, ")"]) + ; <xtc-exit> 51 + + not-implemented(|calling-strategy-name, what, term) = + // FIXME: if has-annotation ... + err-msg(|<concat-strings>["not yet implemented: ", what, " (in strategy ", + calling-strategy-name, ")"]) + ; !term + ; debug + ; <xtc-exit> 51 Index: src/str/eval-meta-code.str --- src/str/eval-meta-code.str (revision 40) +++ src/str/eval-meta-code.str (working copy) @@ -76,7 +76,7 @@ strategies - gen-meta-code(|i, args) = + gen-meta-code(|i, data) = ///*DEBUG*/say(!" ### gen-meta-code starting"); debug; (?MetaFor(meta-var, _, _, _, body) <+ fatal-err-msg(|"ICE!")) ///*DEBUG*/; say(!" >>> gen-meta-code -- start -- current term >>>") Index: src/syn/xrm/XRM-Expression.sdf --- src/syn/xrm/XRM-Expression.sdf (revision 40) +++ src/syn/xrm/XRM-Expression.sdf (working copy) @@ -8,12 +8,21 @@ %% ArrayAccess %% | Expression "<<" Expression %% | Expression ">>" Expression + %% + %% ExpressionFunc ::= + %% (* older builtin functions for backwards compat. *) + %% "rand" "(" Expression {"," Expression} ")" + %% (* builtin functions calls using the "func" notation *) + %% | "func" "(" "rand" "," Expression {"," Expression} ")" context-free syntax ArrayAccess -> Expression Expression ">>" Expression -> Expression {left,cons("RightShift")} Expression "<<" Expression -> Expression {left,cons("LeftShift")} + "rand" "(" {Expression ","}+ ")" -> Expression {cons("Rand")} + "func" "(" "rand" "," {Expression ","}+ ")" -> Expression {cons("Rand")} + context-free priorities { "+" Expression -> Expression Index: src/syn/prism/PRISM-MetaVars.sdf --- src/syn/prism/PRISM-MetaVars.sdf (revision 40) +++ src/syn/prism/PRISM-MetaVars.sdf (working copy) @@ -12,3 +12,4 @@ "m"[0-9]* "*" -> Module+ {prefer} [c][0-9]* -> Command {prefer} "c"[0-9]* "*" -> Command+ {prefer} + [u][0-9]* -> Updates {prefer} Index: src/syn/prism/StrategoPRISM.sdf --- src/syn/prism/StrategoPRISM.sdf (revision 40) +++ src/syn/prism/StrategoPRISM.sdf (working copy) @@ -24,3 +24,4 @@ "~id':" StrategoTerm -> IdentifierPrime {prefer,cons("FromTerm")} "~int:" StrategoTerm -> LInt {prefer,cons("FromTerm")} "~double:" StrategoTerm -> LDouble {prefer,cons("FromTerm")} + "~updates:" StrategoTerm -> Updates {prefer,cons("FromTerm")} Index: tests/xrm/rand.xpm --- tests/xrm/rand.xpm (revision 0) +++ tests/xrm/rand.xpm (revision 0) @@ -0,0 +1,12 @@ + +module rand // NOTE: no conflict here (rand isn't a reserved name) + x : [0..42]; + y : [0..1]; + [] x=0 -> (x'=rand(5)); + [] x=1 -> (y'=1) & (x'=rand(5)); + [] x=2 -> (x'=rand(5)+3); + //[] x=2 -> 0.5:(y'=2) + 0.5:(x'=rand(5)); + [] x=3 -> (x'=rand(3, 9)); + [] x=4 -> 1/5:(x'=0) + 1/5:(x'=1) + 1/5:(x'=2) + + 1/5:(x'=3) + 1/5:(x'=4) + 1/5:(x'=5); +endmodule Index: tests/prism/formula.pm --- tests/prism/formula.pm (revision 0) +++ tests/prism/formula.pm (revision 0) @@ -0,0 +1,6 @@ +formula lfree = p2=0..4,6,10; + +module test + p1 : [0..42] init 0; + [] p1=2 & lfree -> (p1'=4); +endmodule Index: TODO --- TODO (revision 40) +++ TODO (working copy) @@ -128,6 +128,18 @@ [] x=3 -> ... // x=3 is impossible [] x=0 -> (x'=3) // x=3 is not in the definition range of x + ## ------------- ## + ## 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)) + - 42: internal compiler error + - 51: not yet implemented + ## ---- ## ## DONE ## ## ---- ##

18 years, 7 months

XRM 40: Use libxtclib instead of liblib.

by SIGOURE Benoit

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Use libxtclib instead of liblib. See https://bugs.cs.uu.nl/browse/STR-564. Actually we can't use libstratego-xtc at the moment, since it hasn't made it to strc 0.16 and we target this version of the compiler ATM. In the future we shall update the imports as commented in FIXMEs. * src/tools/parse-xrm.str: Import libxtclib instead of liblib. * src/tools/parse-prism.str, * src/tools/pp-xrm.str, * src/tools/pp-prism.str, * src/lib/xrm/pp/xrm-to-abox.str, * src/lib/prism/pp/prism-to-abox.str, * src/str/xrm-front.str: Ditto. * tests/xrm/array_with_static_dim.xpm: New. * tests/xrm/desugar_builtins.pm: Move... * tests/prism/desugar_builtins.pm: Here. * TODO: More things to do... TODO | 9 +++++++++ src/lib/prism/pp/prism-to-abox.str | 2 +- src/lib/xrm/pp/xrm-to-abox.str | 2 +- src/str/xrm-front.str | 3 +-- src/tools/parse-prism.str | 2 +- src/tools/parse-xrm.str | 2 +- src/tools/pp-prism.str | 2 +- src/tools/pp-xrm.str | 2 +- tests/xrm/array_with_static_dim.xpm | 5 +++++ 9 files changed, 21 insertions(+), 8 deletions(-) Index: src/tools/parse-xrm.str --- src/tools/parse-xrm.str (revision 39) +++ src/tools/parse-xrm.str (working copy) @@ -2,7 +2,7 @@ module parse-xrm imports - liblib + libxtclib // FIXME: import libstratego-xtc for strc 0.17 tool-doc parser-common Index: src/tools/parse-prism.str --- src/tools/parse-prism.str (revision 39) +++ src/tools/parse-prism.str (working copy) @@ -2,7 +2,7 @@ module parse-prism imports - liblib + libxtclib // FIXME: import libstratego-xtc for strc 0.17 tool-doc parser-common Index: src/tools/pp-xrm.str --- src/tools/pp-xrm.str (revision 39) +++ src/tools/pp-xrm.str (working copy) @@ -2,7 +2,7 @@ module pp-xrm imports - liblib + libxtclib // FIXME: import libstratego-xtc for strc 0.17 tool-doc strategies Index: src/tools/pp-prism.str --- src/tools/pp-prism.str (revision 39) +++ src/tools/pp-prism.str (working copy) @@ -2,7 +2,7 @@ module pp-prism imports - liblib + libxtclib // FIXME: import libstratego-xtc for strc 0.17 tool-doc strategies Index: src/lib/xrm/pp/xrm-to-abox.str --- src/lib/xrm/pp/xrm-to-abox.str (revision 39) +++ src/lib/xrm/pp/xrm-to-abox.str (working copy) @@ -1,6 +1,6 @@ module xrm-to-abox imports - liblib + libxtclib // FIXME: import libstratego-xtc for strc 0.17 tool-doc Box XRM // signature Index: src/lib/prism/pp/prism-to-abox.str --- src/lib/prism/pp/prism-to-abox.str (revision 39) +++ src/lib/prism/pp/prism-to-abox.str (working copy) @@ -1,6 +1,6 @@ module prism-to-abox imports - liblib + libxtclib // FIXME: import libstratego-xtc for strc 0.17 tool-doc Box PRISM // signature Index: src/str/xrm-front.str --- src/str/xrm-front.str (revision 39) +++ src/str/xrm-front.str (working copy) @@ -1,7 +1,7 @@ module xrm-front imports - liblib + libxtclib // FIXME: import libstratego-xtc for strc 0.17 tool-doc xrm-to-prism prism-desugar @@ -23,7 +23,6 @@ ; xtc-transform(!"parse-xrm", // parse input (returns a FILE) <concat>[ ["-b"], <pass-verbose>(), <pass-add-pos>() ]) ; read-from // read parsed input - ; /*FIXME*/strip-annos // FIXME: remove this line!!!!!!!!!!!!!!!!!!!!!!!!!! ; xrm-front-pipeline // transformations ; if not(must-keep-attributes) then strip-annos end ; if <get-config> "-b" then Index: tests/xrm/array_with_static_dim.xpm --- tests/xrm/array_with_static_dim.xpm (revision 0) +++ tests/xrm/array_with_static_dim.xpm (revision 0) @@ -0,0 +1,5 @@ +const int N = 10; + +module test + s[N] : [0..1]; +endmodule Index: TODO --- TODO (revision 39) +++ TODO (working copy) @@ -48,6 +48,10 @@ declared variables (globals, formulas, local declarations etc.) and ensure (in check-meta-vars) that their identifiers are unique. + * Add a "rand" builtin. Eg: + rand(50) -> random value between 0 and 50 (included) + rand(42, 50) -> random value between 42 and 50 (included) + * 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. @@ -94,6 +98,11 @@ x[3] : [0..4] init {0, 1, 2}; const int array[3] = {0, 1, 2}; + * Add a possibility to import another module, eg: import common.pm + A module can be imported only once. + + * Add parameterized formulas. (Pretty much like macro-functions in C) + ## -------------- ## ## Desugarisation ## ## -------------- ##

18 years, 7 months

XRM 39: Remove debugging messages from prism-desugar.

by SIGOURE Benoit

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Remove debugging messages from prism-desugar. * src/str/prism-desugar.str: Remove debugging stuff. * tests/prism/range-desugar.pm: New. src/str/prism-desugar.str | 119 +++++++++++++++++++++++++++++++++++-------- tests/prism/range-desugar.pm | 13 ++++ 2 files changed, 112 insertions(+), 20 deletions(-) Index: src/str/prism-desugar.str --- src/str/prism-desugar.str (revision 38) +++ src/str/prism-desugar.str (working copy) @@ -21,7 +21,7 @@ RemoveUnconditionnalUpdates <+ AddZero <+ MulOne <+ MulZero <+ DivOne <+ catch-div-by-zero <+ EvalPlus <+ EvalMinus <+ EvalMul <+ EvalDiv - <+ EvalLt <+ EvalLtEq <+ EvalGt <+ EvalGtEq <+ EvalEq <+ EvalNeq + <+ EvalLt <+ EvalLtEq <+ EvalGt <+ EvalGtEq <+ EvalEq <+ EvalNotEq <+ EvalAnd <+ EvalOr <+ EvalMin <+ EvalMax <+ EvalFloor <+ EvalCeil <+ EvalPow <+ EvalMod ) @@ -101,6 +101,15 @@ ** the end of an integer literal make it a Double() and not an Int() [This ** is one of the minor extensions of XRM] */ + +/* +** ## ======== ## +** ## Simplify ## +** ## ======== ## +** +** Simplify arithmetic operations. +*/ + rules AddZero: @@ -121,6 +130,12 @@ DivOne: |[ e / 1D ]| -> |[ e ]| +/* +** ## ==================== ## +** ## Constant propagation ## +** ## ==================== ## +*/ + rules EvalPlus: @@ -147,46 +162,102 @@ EvalGtEq: |[ d1 >= d2 ]| -> <compare(geqR)>(d1, d2) +/* +** ## ============== ## +** ## Equality tests ## +** ## ============== ## +** +** - Eval constant equality tests (eg: 1=3 -> false) +** - Desugar complex equality tests +** eg: x=1..5,7,10..13 -> (x>=1 & x<=5) | (x=7) | (x>=10 & x<=13) +** This part is a bit complex since we need to handle several cases in +** different ways. +*/ + +strategies + + /** Simple constant equality tests */ EvalSimpleEq: |[ d1 = d2 ]| -> res - where say(!"@@@ EvalSimpleEq");debug - ; <compare(real-eq)>(d1, d2) => res;debug + where <compare(real-eq)>(d1, d2) => res + /** Simple equality tests with a range (eg: x=[1..5]) */ EvalSimpleRangeEq: |[ e = e1..e2 ]| -> res - where say(!"@@@ EvalSimpleRangeEq range");debug - ; <DesugarRangeEq(|e)>(Range(e1, e2)) => res;debug + where <DesugarRangeEq(|e)>(Range(e1, e2)) => res + /** Complex equality tests (something not in the form of x=exp) */ EvalComplexEq: Eq(e, a*) -> res - where say(!"@@@ EvalComplexEq");<debug>a* - ; !a* - ; map(DesugarRangeEq(|e) <+ \ e2 -> |[ e=e2 ]| \);debug + where !a* + ; map(DesugarRangeEq(|e) <+ \ e2 -> |[ e=e2 ]| \) ; foldr(!False(), \ (x, y) -> Or(x, y) \) => res - ; say(!" end of EvalComplexEq:");debug strategies - EvalEq = ?a;?Eq(_,_);say(!"@@@ EvalEq starting:");debug;rules(Hello: a); - (?Eq(_, [Eq(_, _)]) <+ EvalSimpleEq <+ EvalSimpleRangeEq <+ (?|[ e = e2 ]| < debug;fail + EvalComplexEq)) + /** Eval/desugar an equality test. + ** 1. Try to see whether it's a simple constant equality test in which + ** case it can be evaluated right away. + ** 2. Try to see whether it's a simple equality test with a range, in + ** which case it can be desugared (and maybe latter evaluated by + ** another pass) + ** 3. a) If 1/ and 2/ failed, and if we have an equality test of the + ** form x = exp, we can't desugar/evaluate it further, so give up. + ** b) If 1/ and 2/ failed but we're not on a simple equality test, + ** try to desugar it further since it's a complex equality test. + */ + EvalEq = + EvalSimpleEq + <+ EvalSimpleRangeEq + <+ (?|[ e = e2 ]| < fail + EvalComplexEq) rules + DesugarRangeEq(|e): + Range(e2, e3) -> |[ e >= e2 & e <= e3]| + +/* +** ## ================= ## +** ## "Not equal" tests ## +** ## ================= ## +** +** Everything works in the exact same way as the above for equality tests. +*/ + +strategies + + EvalSimpleNotEq: + |[ d1 != d2 ]| -> res + where <compare(not(real-eq))>(d1, d2) => res + + EvalSimpleRangeNotEq: + |[ e != e1..e2 ]| -> res + where <DesugarRangeNotEq(|e)>(Range(e1, e2)) => res - //EvalNeq: - // |[ d1 != d2 ]| -> <compare(not(real-eq))>(d1, d2) - EvalNeq: + EvalComplexNotEq: NotEq(e, a*) -> res - where say(!"@@@ EvalNeq");<not(?[_])>a*;<debug>a* - ; map(DesugarRangeNeq(|e) <+ \ e2 -> |[ e!=e2 ]| \);debug - ; foldr(!False(), \ (x, y) -> Or(x, y) \) => res;debug + where !a* + ; map(DesugarRangeNotEq(|e) <+ \ e2 -> |[ e!=e2 ]| \) + ; foldr(!False(), \ (x, y) -> Or(x, y) \) => res - DesugarRangeEq(|e): - Range(e2, e3) -> |[ e >= e2 & e <= e3]| +strategies - DesugarRangeNeq(|e): + EvalNotEq = + EvalSimpleNotEq + <+ EvalSimpleRangeNotEq + <+ (?|[ e != e2 ]| < fail + EvalComplexNotEq) + +rules + + DesugarRangeNotEq(|e): Range(e2, e3) -> |[ e < e2 & e > e3]| +/* +** ## ================= ## +** ## Logical operators ## +** ## ================= ## +*/ + rules EvalAnd: @@ -211,6 +282,14 @@ EvalOr: |[ false | e ]| -> |[ e ]| +/* +** ## ============= ## +** ## Eval Builtins ## +** ## ============= ## +** +** Try to evaluate builtin calls. +*/ + rules EvalMin: Index: tests/prism/range-desugar.pm --- tests/prism/range-desugar.pm (revision 0) +++ tests/prism/range-desugar.pm (revision 0) @@ -0,0 +1,13 @@ +module range + x : [0..42] init 0; + + [] 10=1,10 -> true; + [] 10=1..10 -> true; + [] 10=1,2..11 -> true; + [] 10=1,2..11,12 -> true; + + [] x=1,10 -> true; + [] x=1..10 -> true; + [] x=1,2..11 -> true; + [] x=1,2..11,12 -> true; +endmodule

18 years, 7 months

XRM 38: Add support for ranges in constant propagation.

by SIGOURE Benoit

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Add support for ranges in constant propagation. /!\ This commit has all the debugging messages left in the source of prism-desugar because it seems to trigger a bug in the Stratego compiler. Therefore we'll be able to use this revision to investigate the bug. Roughly, what happens is that a strategy such as: a;b;c;...; (X <+ Y <+ Z ...) is inlined and transformed (in C) as something like: ((a;b;c;...;X) <+ (a;b;c;...;Y) <+ (a;b;c;...;Z) <+ ...) which is totally wrong if a;b;c;... has side effects (such as defining dynamic rules) * src/str/prism-desugar.str: Add support for ranges. * src/str/reals.str: Fix newbie mistake. * tests/prism/testeq.pm: New. * TODO: Update. TODO | 20 ++++++------- src/str/prism-desugar.str | 70 +++++++++++++++++++++++++++++++--------------- src/str/reals.str | 4 +- tests/prism/testeq.pm | 21 +++++++++++++ 4 files changed, 81 insertions(+), 34 deletions(-) Index: src/str/prism-desugar.str --- src/str/prism-desugar.str (revision 37) +++ src/str/prism-desugar.str (working copy) @@ -147,43 +147,69 @@ EvalGtEq: |[ d1 >= d2 ]| -> <compare(geqR)>(d1, d2) - /* FIXME: The following rules could be generalized - We need to check whether d1 appears in the list at the RHS */ - EvalEq: - |[ d1 = d2 ]| -> <compare(real-eq)>(d1, d2) + EvalSimpleEq: + |[ d1 = d2 ]| -> res + where say(!"@@@ EvalSimpleEq");debug + ; <compare(real-eq)>(d1, d2) => res;debug + + EvalSimpleRangeEq: + |[ e = e1..e2 ]| -> res + where say(!"@@@ EvalSimpleRangeEq range");debug + ; <DesugarRangeEq(|e)>(Range(e1, e2)) => res;debug + + EvalComplexEq: + Eq(e, a*) -> res + where say(!"@@@ EvalComplexEq");<debug>a* + ; !a* + ; map(DesugarRangeEq(|e) <+ \ e2 -> |[ e=e2 ]| \);debug + ; foldr(!False(), \ (x, y) -> Or(x, y) \) => res + ; say(!" end of EvalComplexEq:");debug - /* FIXME: Same thing as EvalEq */ +strategies + + EvalEq = ?a;?Eq(_,_);say(!"@@@ EvalEq starting:");debug;rules(Hello: a); + (?Eq(_, [Eq(_, _)]) <+ EvalSimpleEq <+ EvalSimpleRangeEq <+ (?|[ e = e2 ]| < debug;fail + EvalComplexEq)) + +rules + + + //EvalNeq: + // |[ d1 != d2 ]| -> <compare(not(real-eq))>(d1, d2) EvalNeq: - |[ d1 != d2 ]| -> <compare(not(real-eq))>(d1, d2) + NotEq(e, a*) -> res + where say(!"@@@ EvalNeq");<not(?[_])>a*;<debug>a* + ; map(DesugarRangeNeq(|e) <+ \ e2 -> |[ e!=e2 ]| \);debug + ; foldr(!False(), \ (x, y) -> Or(x, y) \) => res;debug + + DesugarRangeEq(|e): + Range(e2, e3) -> |[ e >= e2 & e <= e3]| + + DesugarRangeNeq(|e): + Range(e2, e3) -> |[ e < e2 & e > e3]| rules -/* FIXME: Can we optimize this in a single rule? - Since the optimization would decrease readability, - is it worth it? - eg: - EvalAnd: - And(x, y) -> True() where x => True(); y => True() - EvalAnd: - And(x, y) -> False() where x => False() + y => False() -*/ EvalAnd: |[ true & true ]| -> |[ true ]| EvalAnd: - |[ true & false ]| -> |[ false ]| + |[ e & false ]| -> |[ false ]| + EvalAnd: + |[ false & e ]| -> |[ false ]| EvalAnd: - |[ false & true ]| -> |[ false ]| + |[ e & true ]| -> |[ e ]| EvalAnd: - |[ false & false ]| -> |[ false ]| + |[ true & e ]| -> |[ e ]| EvalOr: - |[ true | true ]| -> |[ true ]| + |[ true | e ]| -> |[ true ]| EvalOr: - |[ true | false ]| -> |[ true ]| - EvalOr: - |[ false | true ]| -> |[ true ]| + |[ e | true ]| -> |[ true ]| EvalOr: |[ false | false ]| -> |[ false ]| + EvalOr: + |[ e | false ]| -> |[ e ]| + EvalOr: + |[ false | e ]| -> |[ e ]| rules Index: src/str/reals.str --- src/str/reals.str (revision 37) +++ src/str/reals.str (working copy) @@ -16,8 +16,8 @@ divR = (string-to-real, string-to-real); divr; real-to-string gtR = where((string-to-real, string-to-real); gtr) - geqR = where((string-to-real, string-to-real); ?(x,x) <+ gtr) - ltR = where((string-to-real, string-to-real); not(?(x,x) <+ gtr)) + geqR = where((string-to-real, string-to-real); (?(x,x) <+ gtr)) + ltR = where((string-to-real, string-to-real); (not(?(x,x) <+ gtr))) leqR = where((string-to-real, string-to-real); not(gtr)) maxR = where((string-to-real, string-to-real); maxr) minR = where((string-to-real, string-to-real); minr) Index: tests/prism/testeq.pm --- tests/prism/testeq.pm (revision 0) +++ tests/prism/testeq.pm (revision 0) @@ -0,0 +1,21 @@ +module test + x : [0..42]; + [] 10=10 -> (x'=1); + [] 10=1 -> (x'=2); + [] 10=1 | 10=10 -> (x'=3); + + [] 10<=10 -> (x'=4); + [] 10<10 -> (x'=5); + [] 10>=10 -> (x'=6); + [] 10>10 -> (x'=7); + + [] 1<=10 -> (x'=8); + [] 1<10 -> (x'=9); + [] 1>=10 -> (x'=10); + [] 1>10 -> (x'=11); + + [] 10<=1 -> (x'=12); + [] 10<1 -> (x'=13); + [] 10>=1 -> (x'=14); + [] 10>1 -> (x'=15); +endmodule Index: TODO --- TODO (revision 37) +++ TODO (working copy) @@ -98,16 +98,6 @@ ## Desugarisation ## ## -------------- ## - * Desugarise ranges (?) - x = 1..5,7,10..13 - ==> (x>=1 & x<=5) | (x=7) | (x>=10 & x<=13) - - * Expand formulas, eg - formula lfree = p2=0..4,6,10; - // ... - [] p1=2 & lfree -> (p1'=4); - ==> [] p1=2 & (p2=0..4,6,10) -> (p1'=4); - ## ------------- ## ## Type checking ## ## ------------- ## @@ -175,3 +165,13 @@ 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) + + * Expand formulas, eg + formula lfree = p2=0..4,6,10; + // ... + [] p1=2 & lfree -> (p1'=4); + ==> [] p1=2 & (p2=0..4,6,10) -> (p1'=4); + + * Desugarise ranges (?) + x = 1..5,7,10..13 + ==> (x>=1 & x<=5) | (x=7) | (x>=10 & x<=13)

18 years, 7 months

XRM 37: Add formulas in constant propagation.

by SIGOURE Benoit

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

18 years, 7 months

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

Projects