June 2006 - Projects

Re: XRM 66: Add parameterized formulas.
by Akim Demaille 12 Jun '06

12 Jun '06

>>> "SIGOURE" == SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes: > cannot-redefine-static-const(|idf) = > !idf => Identifier(idf') > cannot-redefine-formula(|idf) = > !idf => Identifier(idf') > + > + cannot-redefine-parameterized-formula(|idf) = > + !idf => Identifier(idf') Shouldn't you introduce string-from-identifier? Or identifier-to-string, I don't know if there is a name convention.

1 0

Re: XRM 66: Add parameterized formulas.
by Akim Demaille 12 Jun '06

12 Jun '06

>>> "SIGOURE" == SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes: > collect-static-const-decl = > ?ConstInt(idf, value) > - ; if <ExpandStaticConsts> idf then > - cannot-redefine-static-const(|idf) > - end > - ; if <ExpandFormulas> idf then > - cannot-redefine-formula(|idf) > - end > + ; check-identifier-unicity(|idf) > ; where(<innermost(ExpandStaticConsts + ExpandFormulas)> value => v' > ; !v'{Type("int")} => v) > ; rules(ExpandStaticConsts: idf -> v) > collect-static-const-decl = > ?ConstDouble(idf, value) > - ; if <ExpandStaticConsts> idf then > - cannot-redefine-static-const(|idf) > - end > - ; if <ExpandFormulas> idf then > - cannot-redefine-formula(|idf) > - end > + ; check-identifier-unicity(|idf) > ; where(<innermost(ExpandStaticConsts + ExpandFormulas)> value => v' > ; !v'{Type("double")} => v) > ; rules(ExpandStaticConsts: idf -> v) > collect-static-const-decl = > ?ConstBool(idf, value) > - ; if <ExpandStaticConsts> idf then > - cannot-redefine-static-const(|idf) > - end > - ; if <ExpandFormulas> idf then > - cannot-redefine-formula(|idf) > - end > + ; check-identifier-unicity(|idf) > ; where(<innermost(ExpandStaticConsts + ExpandFormulas)> value => v' > ; !v'{Type("bool")} => v) > ; rules(ExpandStaticConsts: idf -> v) That's nice :)

1 0

Re: XRM 66: Add parameterized formulas.
by Akim Demaille 12 Jun '06

12 Jun '06

>>> "SIGOURE" == SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes: > EvalAnd: > + |[ d & e ]| -> |[ e ]| > + where <not(real-eq)>(d, "0") > + EvalAnd: > + |[ d & e ]| -> |[ false ]| > + where <real-eq>(d, "0") > + EvalAnd: > + |[ e & d ]| -> |[ e ]| > + where <not(real-eq)>(d, "0") > + EvalAnd: > + |[ e & d ]| -> |[ false ]| > + where <real-eq>(d, "0") > + EvalAnd: >> [ true & true ]| -> |[ true ]| There is no better way to do it? I think you should traverse & and | operands trying to evaluate them to Booleans, and then there would remain only the bool cases.

1 0

Re: XRM 64: Use --verbose instead of --statistics.
by Akim Demaille 12 Jun '06

12 Jun '06

>>> "SIGOURE" == 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> > Use --verbose instead of --statistics. > This cancels the note of the previous commit. I have not seen the removal of --statistics support.

1 0

Re: XRM 59: Add (buggy) support for PCTL/CSL formulas.
by Akim Demaille 12 Jun '06

12 Jun '06

>>> "SIGOURE" == SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes: > +pkgdata_DATA_built = \ The usual way to say "built" is nodist_pkgdata_DATA

1 0

Re: XRM 59: Add (buggy) support for PCTL/CSL formulas.
by Akim Demaille 12 Jun '06

12 Jun '06

>>> "SIGOURE" == SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes: > Index: src/tools/parse-pctl.str > --- src/tools/parse-pctl.str (revision 58) > +++ src/tools/parse-pctl.str (working copy) > @@ -1,23 +1,23 @@ > // Code mostly from parse-java by Martin Bravenboer <martin(a)cs.uu.nl> > -module parse-prism > +module parse-pctl There is obviously a great deal of code duplication between your prism and pctrl. Can't you do something about it?

1 0

Re: XRM 59: Add (buggy) support for PCTL/CSL formulas.
by Akim Demaille 12 Jun '06

12 Jun '06

>>> "SIGOURE" == SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes: > + ** We use two parse tables for performances. One of them > + (PCTL.tbl) has a ** single start symbol (ModulesFile) and the > + other (PCTL-StartSymbols) has > ** several other start symbols. We're doing this because start > symbol ** selection happens *after* parsing in sglr. So first > all the alternatives ** are parsed, and then the selected start > symbol is chosen. Wow!

1 0

Re: XRM 58: Add ConstantDef in concrete syntax.
by Akim Demaille 12 Jun '06

12 Jun '06

>>> "SIGOURE" == SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes: > Index: src/syn/prism/StrategoPRISM.sdf > --- src/syn/prism/StrategoPRISM.sdf (revision 57) > +++ src/syn/prism/StrategoPRISM.sdf (working copy) > @@ -15,6 +15,7 @@ > "|[" Expression "]|" -> StrategoTerm {prefer,cons("ToTerm")} > "|[" Declaration "]|" -> StrategoTerm {prefer,cons("ToTerm")} > "|[" Command "]|" -> StrategoTerm {prefer,cons("ToTerm")} > + "|[" ConstantDef "]|" -> StrategoTerm {prefer,cons("ToTerm")} > context-free syntax Can you teach me the different between this file, and the change XRM 56: Index: src/syn/prism/PRISM-MetaCongruences.sdf --- src/syn/prism/PRISM-MetaCongruences.sdf (revision 55) +++ src/syn/prism/PRISM-MetaCongruences.sdf (working copy) @@ -7,3 +7,4 @@ "|[" Expression "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} "|[" Declaration "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} "|[" Command "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} + "|[" ConstantDef "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} ? I can see there is "ToStrategy" ot1h and ToTerm otoh, but what are the respective roles? And isn't this a sign you'd like to generate the two files from a common sources?

1 0

Re: XRM 57: Fix boxing of meta-if at Expression level.
by Akim Demaille 12 Jun '06

12 Jun '06

>>> "SIGOURE" == SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes: > Fix boxing of meta-if at Expression level. > The new test fails because of an ambiguity. This ambiguity is a bit > tricky and (IMHO) must be resolved at the grammar level. > Basically we have: > test1 ? test1-true : test2 ? test2-true : test2-false > The ambiguity is: > (test1 ? test1-true : test2) ? test2-true : test2-false > -or- > test1 ? test1-true : (test2 ? test2-true : test2-false) > The second choice seems more natural and that's how it works in C. > Obviously we can't keep this ambiguity in the grammar. You might want to read the third problem in this exam.

1 0

Re: XRM 55: Add documentation draft for XRM.
by Akim Demaille 12 Jun '06

12 Jun '06

>>> "SIGOURE" == SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> writes: > doc/user-guide.txt | 392 +++++++++++++++++++++++++++++++++++++++ This is nice (and seldom done!).

1 0