[Projects] XRM 63: Finish eXtended PCTL integration in xrm-front.

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit &lt;sigoure.benoit(a)lrde.epita.fr&gt; Finish eXtended PCTL integration in xrm-front. NOTE: instead of using --verbose notice you should now use --statistics 1 or 2. * src/tools/parse-pctl.str: Fix a typo. * src/tools/parse-xpctl.str: Ditto. * src/lib/xrm/pp/Makefile.am: Fix dependencies. * src/lib/xpctl/pp/Makefile.am: Ditto. * src/lib/xpctl/pp/pp-xpctl-to-box.str: Fix imports. * src/str/xrm-to-prism.str: Re-organize. Use log-timed. * src/str/log-timed.str: New. * src/str/xrm-front.str: Use log-timed. * src/syn/xrm/XRM-Arrays.sdf: Dirty hack with imports. * src/syn/xrm/XRM-Expression.sdf: Ditto. * src/syn/xrm/XRM-Keywords.sdf: New. * src/syn/xrm/XRM-Main.sdf: Import XRM-Keywords. * src/syn/xrm/XRM-MetaFor.sdf: Ditto. * src/syn/xpctl/XPCTL-MetaFor.sdf: Extend ForIn with Property. * src/syn/xpctl/XPCTL-Main.sdf: Import XRM-Expression and XRM-Arrays. * tests/pctl/rivf.xpctl: New. * doc/user-guide.txt: Bring up to date. doc/user-guide.txt | 11 +++++ src/lib/xpctl/pp/Makefile.am | 8 --- src/lib/xpctl/pp/pp-xpctl-to-box.str | 3 + src/lib/xrm/pp/Makefile.am | 8 --- src/str/log-timed.str | 73 +++++++++++++++++++++++++++++++++++ src/str/xrm-front.str | 39 +++++++++--------- src/str/xrm-to-prism.str | 65 +++++++++++++++++-------------- src/syn/xpctl/XPCTL-Main.sdf | 2 src/syn/xpctl/XPCTL-MetaFor.sdf | 3 - src/syn/xrm/XRM-Arrays.sdf | 6 +- src/syn/xrm/XRM-Expression.sdf | 6 +- src/syn/xrm/XRM-Keywords.sdf | 8 +++ src/syn/xrm/XRM-Main.sdf | 1 src/syn/xrm/XRM-MetaFor.sdf | 1 src/tools/parse-pctl.str | 2 src/tools/parse-xpctl.str | 2 tests/pctl/rivf.xpctl | 12 +++++ 17 files changed, 182 insertions(+), 68 deletions(-) Index: src/tools/parse-pctl.str --- src/tools/parse-pctl.str (revision 62) +++ src/tools/parse-pctl.str (working copy) @@ -59,7 +59,7 @@ strategies /* ** We use two parse tables for performances. One of them (PCTL.tbl) has a - ** single start symbol (ModulesFile) and the other (PCTL-StartSymbols) has + ** single start symbol (PropertiesFile) 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. Index: src/tools/parse-xpctl.str --- src/tools/parse-xpctl.str (revision 62) +++ src/tools/parse-xpctl.str (working copy) @@ -59,7 +59,7 @@ strategies /* ** We use two parse tables for performances. One of them (XPCTL.tbl) has a - ** single start symbol (ModulesFile) and the other (XPCTL-StartSymbols) has + ** single start symbol (PropertiesFile) and the other (XPCTL-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. Index: src/lib/xrm/pp/Makefile.am --- src/lib/xrm/pp/Makefile.am (revision 62) +++ src/lib/xrm/pp/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; ## ## Started on Wed May 10 19:27:12 2006 SIGOURE Benoit -## Last update Sun Jun 11 03:26:50 2006 SIGOURE Benoit +## Last update Sun Jun 11 04:08:22 2006 SIGOURE Benoit ## include $(top_srcdir)/config/toplevel.mk @@ -29,11 +29,7 @@ EXTRA_DIST = $(wildcard *.str) $(wildcard *.meta) -SDEFS = \ - $(top_builddir)/src/syn/prism/PRISM.def \ - $(top_builddir)/src/syn/xrm/XRM.def - -xrm-parenthesize.str: $(SDEFS) +xrm-parenthesize.str: $(top_builddir)/src/syn/xrm/XRM.def $(SDF_TOOLS)/bin/sdf2parenthesize -i $< -o $@ \ -m XRM \ --omod xrm-parenthesize \ Index: src/lib/xpctl/pp/pp-xpctl-to-box.str --- src/lib/xpctl/pp/pp-xpctl-to-box.str (revision 62) +++ src/lib/xpctl/pp/pp-xpctl-to-box.str (working copy) @@ -3,6 +3,7 @@ Box XPCTL // signature PCTL // signature of the base language + XRM // signature (required since we use parts of the language) prism-constant prism-expression xpctl-parenthesize @@ -13,6 +14,8 @@ pctl-path pctl-reward pctl-filter + xrm-expression + xrm-arrays xrm-meta-for // Hack: Meta-For loops are identical in XPCTL and XRM. :) xrm-meta-if // Ditto. Index: src/lib/xpctl/pp/Makefile.am --- src/lib/xpctl/pp/Makefile.am (revision 62) +++ src/lib/xpctl/pp/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; ## ## Started on Sat Jun 10 03:59:11 2006 SIGOURE Benoit -## Last update Sun Jun 11 03:26:36 2006 SIGOURE Benoit +## Last update Sun Jun 11 04:08:59 2006 SIGOURE Benoit ## include $(top_srcdir)/config/toplevel.mk @@ -31,11 +31,7 @@ EXTRA_DIST = $(wildcard *.str) $(wildcard *.meta) -SDEFS = \ - $(top_builddir)/src/syn/pctl/PCTL.def \ - $(top_builddir)/src/syn/xpctl/XPCTL.def - -xpctl-parenthesize.str: $(SDEFS) +xpctl-parenthesize.str: $(top_builddir)/src/syn/xpctl/XPCTL.def $(SDF_TOOLS)/bin/sdf2parenthesize -i $< -o $@ \ -m XPCTL \ --omod xpctl-parenthesize \ Index: src/str/xrm-to-prism.str --- src/str/xrm-to-prism.str (revision 62) +++ src/str/xrm-to-prism.str (working copy) @@ -36,46 +36,36 @@ eval-meta-code array-decl-desugar builtin-rand + log-timed strategies xrm-to-prism = /* bind the start-symbol (ModulesFile or PropertiesFile) */ ?start-symbol#(_) - ; if <is-module-file> start-symbol then - /* remove XRM sugar, normalize some nodes */ - innermost(xrm-generic-desugar <+ DesugarRand <+ EvalRand) - else - if <is-properties-file> start-symbol then - /* rand isn't allowed in PropertiesFile hence the catch-rand */ - innermost(xrm-generic-desugar <+ catch-rand) - else - ice(|"xrm-to-prism", "Unexpected start-symbol", start-symbol) - end - end - ; notice-msg(|"xrm-to-prism: XRM sugar removed") + + ; log-timed(remove-xrm-sugar(|start-symbol) | "Removing XRM sugar", 2) /* Collect static const variables * Two goals: expand them if needed, look for variable name conflicts. */ - ; if <is-module-file> start-symbol then + ; log-timed( + if <is-module-file> start-symbol then ModulesFile(id, map(try(collect-static-const-decl) ; try(collect-formulas))) else PropertiesFile(map(try(collect-static-const-decl) ; try(collect-formulas))) end - ; notice-msg(|"xrm-to-prism: static const and formulas collected") + | "Collecting static const and formulas", 2) /* Check that meta vars are always defined in the current scope when used * and that they are not redefined twice in the same scope. This must come * AFTER collect-static-const-decl/collect-formulas since it needs some of * the information gathered by them (in DR's). */ - ; check-meta-vars - ; notice-msg(|"xrm-to-prism: meta-vars checked") + ; log-timed(check-meta-vars | "Checking meta-vars", 2) /* unroll meta loops, eval meta if */ - ; eval-meta-code - ; notice-msg(|"xrm-to-prism: eval-meta-code done") + ; log-timed(eval-meta-code | "Evaluating meta-code", 2) /*; notice-msg(|"debug: pretty printing current AST in ATerms to debug.aterm") ; where(write-to => FILE(tmp-file) ; <xtc-command(!"pp-aterm")> ["-i", tmp-file, "-o", "debug.aterm"] @@ -89,32 +79,38 @@ * This must come AFTER collect-static-const-decl since we might need * to expand an arrays which rely on static const variables. */ - ; topdown(try(array-decl-desugar); try(EvalStaticRand)) - ; notice-msg(|"xrm-to-prism: array declarations desugared") + ; log-timed(topdown(try(array-decl-desugar); try(EvalStaticRand)) + | "Desugaring array declarations", 2) /* flatten nested lists */ - ; if <is-module-file> start-symbol then + ; log-timed( + if <is-module-file> start-symbol then ModulesFile(id, flatten-list) ; ModulesFile(id, map(try(Module(id, flatten-list)))) - ; notice-msg(|"xrm-to-prism: flatten-list done") + else + PropertiesFile(flatten-list) + end + | "AST normalization (flatten-list)", 2) + ; if <is-module-file> start-symbol then + log-timed( /* get the modules that generates random numbers (XRM rand builtin) */ - ; where(bagof-RandGenModules; reverse => rand-gen-modules) + where(bagof-RandGenModules; reverse => rand-gen-modules) /* paste them at the end of the file */ ; ModulesFile(id, <conc>(<id>, rand-gen-modules)) - ; notice-msg(|"xrm-to-prism: added modules for random numbers") + | "Adding modules for random numbers", 2) end /* remove array accesses: x[i] -> x_i */ // FIXME: can we make this more efficient than a complete bottomup? - ; bottomup(try(flatten-array-access)) - ; notice-msg(|"xrm-to-prism: flatten-array-access done") + ; log-timed(bottomup(try(flatten-array-access)) + | "Desugaring array accesses", 2) ; if <is-module-file> start-symbol then /* re-order modules so that all declarations appear before commands */ - ModulesFile(id, map(try(reorder-module-contents))) - ; notice-msg(|"xrm-to-prism: reorder-module-contents done") + log-timed(ModulesFile(id, map(try(reorder-module-contents))) + | "Reordering module contents", 2) end is-module-file = ?"ModulesFile" @@ -122,6 +118,19 @@ strategies + /** remove XRM sugar, normalize some nodes */ + remove-xrm-sugar(|start-symbol) = + if <is-module-file> start-symbol then + innermost(xrm-generic-desugar <+ DesugarRand <+ EvalRand) + else + if <is-properties-file> start-symbol then + /* rand isn't allowed in PropertiesFile hence the catch-rand */ + innermost(xrm-generic-desugar <+ catch-rand) + else + ice(|"xrm-to-prism", "Unexpected start-symbol", start-symbol) + end + end + /** ** Perform generic transformations which can apply to either a ModulesFile ** or a PropertiesFile. Index: src/str/log-timed.str --- src/str/log-timed.str (revision 0) +++ src/str/log-timed.str (revision 0) @@ -0,0 +1,73 @@ +/** +** Original code from strc (The Stratego Compiler) +** by Eelco Visser &lt;visser(a)acm.org&gt; +*/ +module log-timed + +strategies + + /** + ** Execute and time a strategy. + ** @param s strategy to execute. + ** @param msg message to print. + ** @param level --statistics level from which the timing+msg will be + ** printed. (default level=1) + */ + log-timed(s | msg, level) = + if <geq>(<get-config> "--statistics", level) then + where( + times => start + ; print-log-msg(|msg) + ) + ; s + ; where( + <diff-times>(<times>, start) + ; <concat-strings>[" : [user=" + , <self-children-user-time + ; ticks-to-seconds + ; real-to-string(|2)> + , "s/system=" + , <self-children-sys-time + ; ticks-to-seconds + ; real-to-string(|2)> + , "s]\n" + ] + ; log-puts + ) + else + s + end + + /** + ** Same thing as log-timed but nothing will be printed until s finished. + */ + log-timed-reentrant(s | msg, level) = + if <geq>(<get-config> "--statistics", level) then + where(times => start) + ; s + ; where( + print-log-msg(|msg) + ; <diff-times>(<times>, start) + ; <concat-strings>[" : [user=" + , <self-children-user-time + ; ticks-to-seconds + ; real-to-string(|2)> + , "s/system=" + , <self-children-sys-time + ; ticks-to-seconds + ; real-to-string(|2)> + , "s]\n" + ] + ; log-puts + ) + else + s + end + + print-log-msg(|msg) = + <concat-strings>["[ " + , <log-src> + , " | info ] " + , <align-left>(' ', msg, 40) // 40 = max strlen(msg) + ] + ; log-puts Index: src/str/xrm-front.str --- src/str/xrm-front.str (revision 62) +++ src/str/xrm-front.str (working copy) @@ -5,6 +5,7 @@ tool-doc xrm-to-prism prism-desugar + log-timed strategies @@ -14,7 +15,7 @@ xrm-front-options , xrm-front-usage , xrm-front-about - , !["parse-xrm", "pp-prism", "pp-aterm"] + , !["parse-xrm", "parse-xpctl", "pp-prism", "pp-pctl", "pp-aterm"] , main-wrapped ) @@ -29,15 +30,15 @@ ; write-to ; if not(<get-config> "-b") then if must-pp-aterm then // output pp-ATerms - notice-msg(|"pretty printing ATerms") - ; xtc-transform(!"pp-aterm", pass-verbose) + log-timed(xtc-transform(!"pp-aterm", pass-verbose) + | "pretty printed ATerms", 1) else if must-parse-pctl then // output PCTL source - notice-msg(|"pretty printing PCTL code") - ; xtc-transform(!"pp-pctl", pass-verbose) + log-timed(xtc-transform(!"pp-pctl", pass-verbose) + | "pretty printed PCTL code", 1) else // output PRISM source - notice-msg(|"pretty printing PRISM code") - ; xtc-transform(!"pp-prism", pass-verbose) + log-timed(xtc-transform(!"pp-prism", pass-verbose) + | "pretty printed PRISM code", 1) end end end @@ -46,12 +47,10 @@ /** pipeline of transformations performed by xrm-front */ xrm-front-pipeline = - notice-msg(|"transformation pipeline starting") - ; where(<set-random-seed> (<time>)) - ; xrm-to-prism + where(<set-random-seed> (<time>)) + ; log-timed-reentrant(xrm-to-prism | "XRM to PRISM succeeded", 0) ; if must-desugar then - prism-desugar - ; notice-msg(|"prism-desugar finished") + log-timed(prism-desugar | "Additionnal desugarisation (-D)", 0) end /** list of available options for xrm-front */ @@ -78,7 +77,7 @@ Option("-K" + "--keep-attributes" , <set-keep-attributes> "yes" , !HelpString("-K | --keep-attributes", "Don't remove attributes when - printing ATerms (this includes positions)") + printing ATerms (this includes positions).") ) set-keep-attributes = @@ -92,7 +91,7 @@ pp-aterm-option = Option("-A" + "--pp-aterm" , <set-pp-aterm> "yes" - , !HelpString("-A | --pp-aterm", "Pretty print output with pp-aterm") + , !HelpString("-A | --pp-aterm", "Pretty print output with pp-aterm.") ) set-pp-aterm = @@ -106,7 +105,7 @@ desugar-option = Option("-D" + "--desugar" , <set-desugar> "yes" - , !HelpString("-D | --desugar", "Desugar the generated PRISM code") + , !HelpString("-D | --desugar", "Desugar the generated PRISM code.") ) set-desugar = @@ -136,18 +135,18 @@ strategies parse-pctl-option = - Option("-p" + "--pctl" + Option("-p" + "--pctl" + "--xpctl" , <set-parse-pctl> "yes" - , !HelpString("-p | --pctl", "The input file is an eXtended PCTL file") + , !HelpString("-p | --pctl", "The input file is an eXtended PCTL file.") ) set-parse-pctl = - <set-config> ("parse-pctl", <id>) + <set-config> ("parse-xpctl", <id>) must-parse-pctl = - <get-config> "parse-pctl" => "yes" + <get-config> "parse-xpctl" => "yes" - get-parser = must-parse-pctl < !"parse-pctl" + !"parse-xrm" + get-parser = must-parse-pctl < !"parse-xpctl" + !"parse-xrm" /** * Documentation Index: src/syn/xrm/XRM-Arrays.sdf --- src/syn/xrm/XRM-Arrays.sdf (revision 62) +++ src/syn/xrm/XRM-Arrays.sdf (working copy) @@ -1,7 +1,9 @@ module XRM-Arrays imports - PRISM-to-XRM -exports + XRM-Expression +%%imports %% import commented out so that we can import +%% PRISM-to-XRM %% XRM-MetaIfExp from XPCTL without importing +exports %% the whole PRISM stuff.. dirty hack inside! %% FIXME: we can probably make this look nicer. %% EBNF Grammar: Arrays Index: src/syn/xrm/XRM-Keywords.sdf --- src/syn/xrm/XRM-Keywords.sdf (revision 0) +++ src/syn/xrm/XRM-Keywords.sdf (revision 0) @@ -0,0 +1,8 @@ +module XRM-Keywords +imports PRISM-Keywords +exports + lexical syntax + "for" -> Keyword + + lexical restrictions + "for" -/- [A-Za-z0-9\_] Index: src/syn/xrm/XRM-Main.sdf --- src/syn/xrm/XRM-Main.sdf (revision 62) +++ src/syn/xrm/XRM-Main.sdf (working copy) @@ -11,3 +11,4 @@ XRM-Command XRM-Formula XRM-Constant + XRM-Keywords Index: src/syn/xrm/XRM-MetaFor.sdf --- src/syn/xrm/XRM-MetaFor.sdf (revision 62) +++ src/syn/xrm/XRM-MetaFor.sdf (working copy) @@ -2,6 +2,7 @@ imports PRISM-to-XRM XRM-Module + XRM-Keywords exports %% EBNF Grammar: Meta For Loops Index: src/syn/xrm/XRM-Expression.sdf --- src/syn/xrm/XRM-Expression.sdf (revision 62) +++ src/syn/xrm/XRM-Expression.sdf (working copy) @@ -1,7 +1,7 @@ module XRM-Expression -imports - PRISM-to-XRM -exports +%%imports %% import commented out so that we can import +%% PRISM-to-XRM %% XRM-MetaIfExp from XPCTL without importing +exports %% the whole PRISM stuff.. dirty hack inside! %% EBNF Grammar: Extended Expressions %% Expression ::= Index: src/syn/xpctl/XPCTL-MetaFor.sdf --- src/syn/xpctl/XPCTL-MetaFor.sdf (revision 62) +++ src/syn/xpctl/XPCTL-MetaFor.sdf (working copy) @@ -1,6 +1,7 @@ module XPCTL-MetaFor imports PCTL-PropertiesFile + XRM-Keywords exports %% EBNF Grammar: Meta For Loops @@ -20,5 +21,5 @@ "for" Identifier "from" Expression "to" Expression "step" Expression "do" PropertiesFileSection* "end" -> PropertiesFileSection {cons("MetaFor")} - "for" Identifier "in" {Expression ","}+ "do" + "for" Identifier "in" {Property ","}+ "do" PropertiesFileSection* "end" -> PropertiesFileSection {cons("MetaForIn")} Index: src/syn/xpctl/XPCTL-Main.sdf --- src/syn/xpctl/XPCTL-Main.sdf (revision 62) +++ src/syn/xpctl/XPCTL-Main.sdf (working copy) @@ -3,3 +3,5 @@ PCTL-Main XPCTL-MetaFor XPCTL-MetaIf + XRM-Expression + XRM-Arrays Index: tests/pctl/rivf.xpctl --- tests/pctl/rivf.xpctl (revision 0) +++ tests/pctl/rivf.xpctl (revision 0) @@ -0,0 +1,12 @@ +for i from 0 to 1200 step 100 do + P=? [ true U (t <= i & (sensor[0][0]= 4 | sensor[0][1]= 4 | sensor[0][2]= 4 + | sensor[0][3]= 4 | sensor[0][4]= 4 | sensor[0][5]= 4 | sensor[0][6]= 4 | + sensor[0][7]= 4 | sensor[0][8]= 4 | sensor[0][9]= 4 | sensor[9][0] = 4 | + sensor[9][1] = 4 | sensor[9][2] = 4 | sensor[9][3] = 4 | sensor[9][4] = 4 | + sensor[9][5] = 4 | sensor[9][6] = 4 | sensor[9][7] = 4 | sensor[9][8] = 4 | + sensor[9][9] = 4 | sensor[1][0] = 4 | sensor[2][0] = 4 | sensor[3][0] = 4 | + sensor[4][0] = 4 | sensor[5][0] = 4 | sensor[6][0] = 4 | sensor[7][0] = 4 | + sensor[8][0] = 4 | sensor[1][9] = 4 | sensor[2][9] = 4 | sensor[3][9] = 4 | + sensor[4][9] = 4 | sensor[5][9] = 4 | sensor[6][9] = 4 | sensor[7][9] = 4 | + sensor[8][9] = 4)) ] +end Index: doc/user-guide.txt --- doc/user-guide.txt (revision 62) +++ doc/user-guide.txt (working copy) @@ -89,6 +89,7 @@ -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. + -p | --pctl The input file is an eXtended PCTL file. # Return value ------------ @@ -214,6 +215,8 @@ 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 The word "for" is a reserved keyword in XRM and cannot be used for an + identifier. 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'. @@ -344,6 +347,14 @@ in the module which called rand. The variable will be updated each time it's accessed to ensure real random numbers. + ************************** + * XRM and Property Files * + ************************** + + Almost all the features of the XRM language are available in eXtended + Property Files. There is an exception: + o The rand builtin cannot be used in property files. + ********************* * Incoming features * *********************