[Projects] XRM 66: Add parameterized formulas.

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit &lt;sigoure.benoit(a)lrde.epita.fr&gt; Add parameterized formulas. * src/lib/xrm/pp/xrm-formula.str: New. * src/lib/xrm/pp/xrm-formula.meta: New. * src/lib/xrm/pp/xrm-expression.str: Add boxing for parameterized formulas. * src/lib/prism/pp/pp-prism-to-box.str (very-special-conflict): Handle problematic cases with nested If's (revealed by rivf.xpm). * src/str/flatten-array-access.str: Remove useless call to concat-strings. * src/str/eval-meta-code.str: Ditto. * src/str/builtin-rand.str: Ditto. * src/str/check-meta-vars.str: Handle parameterized formulas. * src/str/xrm-to-prism.str: Ditto. * src/str/inline.str: New. * src/str/prism-desugar.str: Ditto + fix desugaring of conditional expression involving literals (int and double) which was flawed! * src/str/ice.str: Handle lists of strings. * src/str/collect-static-const-decl.str: Put some code in common. Collect parameterized formula definitions. * src/str/desugar-array-access.str: Remove deprecated and useless use of UnscopedMetaVarList. * src/str/reals.str: Add an ICE'ing condition. * src/syn/xrm/XRM-Formula.sdf: Add syntax definitions for parameterized formulas. * src/syn/xrm/XRM-Keywords.sdf: Add `rand' and `static_rand' in the list of reserved keywords... * tests/xrm/rand.xpm: ... and take that change into account here. * src/syn/xrm/XRM-Expression.sdf: Add calls to parameterized formulas. * tests/pctl/xrm-formula.xpctl: New. * tests/xrm/if-desugar.xpm: New. * tests/xrm/parametrized-formula.xpm: New. * tests/test-parse-xrm.sh.in: Fix the counting of failing tests. * tests/test-parse-xpctl.sh.in: Ditto. * TODO: Bring up to date. * doc/user-guide.txt: Ditto. TODO | 4 - doc/user-guide.txt | 29 +++++++++++- src/lib/prism/pp/pp-prism-to-box.str | 20 ++++++++ src/lib/xrm/pp/xrm-expression.str | 9 ++- src/lib/xrm/pp/xrm-formula.meta | 1 src/lib/xrm/pp/xrm-formula.str | 25 ++++++++++ src/str/builtin-rand.str | 8 +-- src/str/check-meta-vars.str | 36 ++++++++++++-- src/str/collect-static-const-decl.str | 82 ++++++++++++++++++++++------------ src/str/desugar-array-access.str | 4 - src/str/eval-meta-code.str | 16 ++---- src/str/flatten-array-access.str | 4 - src/str/ice.str | 35 +++++++++----- src/str/inline.str | 42 +++++++++++++++++ src/str/prism-desugar.str | 42 +++++++++++++---- src/str/reals.str | 4 + src/str/xrm-to-prism.str | 43 ++++++++++++----- src/syn/xrm/XRM-Expression.sdf | 4 + src/syn/xrm/XRM-Formula.sdf | 20 +++++++- src/syn/xrm/XRM-Keywords.sdf | 4 + tests/pctl/xrm-formula.xpctl | 5 ++ tests/test-parse-xpctl.sh.in | 2 tests/test-parse-xrm.sh.in | 2 tests/xrm/if-desugar.xpm | 4 + tests/xrm/parametrized-formula.xpm | 3 + tests/xrm/rand.xpm | 2 26 files changed, 350 insertions(+), 100 deletions(-) Index: src/lib/xrm/pp/xrm-formula.str --- src/lib/xrm/pp/xrm-formula.str (revision 0) +++ src/lib/xrm/pp/xrm-formula.str (revision 0) @@ -0,0 +1,25 @@ +module xrm-formula + +rules + + // "formula" Identifier "(" {Argument ","}* ")" "=" Expression ";" + // -> FormulaDef + prism-to-box: + PFormulaDef(idf, args, body) + -> V [ V is=2 [ H hs=1 [ KW["formula"] ~idf "(" ~*<args-to-box>args' ")" ] + ~body + ] + ";" ] + where <separate-by(!S(","))> args => args' + + args-to-box: + IntArg(idf) -> H hs=1 [ KW["int"] ~idf ] + + args-to-box: + DoubleArg(idf) -> H hs=1 [ KW["double"] ~idf ] + + args-to-box: + BoolArg(idf) -> H hs=1 [ KW["bool"] ~idf ] + + args-to-box: + ExpArg(idf) -> H hs=1 [ KW["exp"] ~idf ] Index: src/lib/xrm/pp/xrm-formula.meta --- src/lib/xrm/pp/xrm-formula.meta (revision 0) +++ src/lib/xrm/pp/xrm-formula.meta (revision 0) @@ -0,0 +1 @@ +Meta([Syntax("Stratego-Box")]) Index: src/lib/xrm/pp/xrm-expression.str --- src/lib/xrm/pp/xrm-expression.str (revision 65) +++ src/lib/xrm/pp/xrm-expression.str (working copy) @@ -19,10 +19,15 @@ prism-to-box: // NOTE: we use the old builtin-call style Rand(args) // because func(rand, ...) is just uggly. - -> box |[ H hs=0 [ KW["rand"] "(" H hs=1 [~args-imploded] ")" ] ]| + -> H hs=0 [ KW["rand"] "(" H hs=1 [~args-imploded] ")" ] where <implode-list(|",")> args => args-imploded prism-to-box: StaticRand(args) - -> box |[ H hs=0 [ KW["static_rand"] "(" H hs=1 [~args-imploded] ")" ] ]| + -> H hs=0 [ KW["static_rand"] "(" H hs=1 [~args-imploded] ")" ] + where <implode-list(|",")> args => args-imploded + + prism-to-box: + PFormulaCall(name, args) + -> H hs=0 [ ~name "(" H hs=1 [~args-imploded] ")" ] where <implode-list(|",")> args => args-imploded Index: src/lib/prism/pp/pp-prism-to-box.str --- src/lib/prism/pp/pp-prism-to-box.str (revision 65) +++ src/lib/prism/pp/pp-prism-to-box.str (working copy) @@ -33,5 +33,25 @@ very-special-conflict: Minus(Minus(e)) -> Minus(Parenthetical(Minus(e))) + // FIXME: Remove this rule once tests/xrm/amb-if-exp.xpm succeeds + // in parse-xrm + very-special-conflict: + If(c, then-part, else-part@If#(_)) + -> If(c, then-part, Parenthetical(else-part)) + where <not(?If#(_))> then-part + + // FIXME: Remove this rule once tests/xrm/amb-if-exp.xpm succeeds + // in parse-xrm + very-special-conflict: + If(c, then-part@If#(_), else-part) + -> If(c, Parenthetical(then-part), else-part) + where <not(?If#(_))> else-part + + // FIXME: Remove this rule once tests/xrm/amb-if-exp.xpm succeeds + // in parse-xrm + very-special-conflict: + If(c, then-part@If#(_), else-part@If#(_)) + -> If(c, Parenthetical(then-part), Parenthetical(else-part)) + very-special-conflict: Plus(Plus(e)) -> Plus(Parenthetical(Plus(e))) Index: src/str/flatten-array-access.str --- src/str/flatten-array-access.str (revision 65) +++ src/str/flatten-array-access.str (working copy) @@ -47,7 +47,7 @@ */ invalid-array-access = if ?Identifier(i) then - err-msg(|<concat-strings>["undeclared meta-variable: ", i]) + err-msg(|["undeclared meta-variable: ", i]) else if (is-int; neg) then err-msg(|"negative array subscript detected:") @@ -55,7 +55,7 @@ else err-msg(|"invalid array access:") ; debug - ; err-msg(|<concat-strings>["array subscripts must be evaluable ", + ; err-msg(|["array subscripts must be evaluable ", "down to constant positive integers."]) end end Index: src/str/check-meta-vars.str --- src/str/check-meta-vars.str (revision 65) +++ src/str/check-meta-vars.str (working copy) @@ -15,6 +15,7 @@ check-meta-for <+ check-meta-forin <+ check-meta-if + <+ check-pformula-def <+ ArrayAccess(id, check-all-identifers-are-meta-vars) <+ ArrayAccessPrime(id, check-all-identifers-are-meta-vars) <+ all(check-meta-vars) @@ -45,6 +46,21 @@ ; <check-meta-vars> else-part ) + check-pformula-def = + ?PFormulaDef(fname, args, body) + ; where({| MetaVars: + <add-args-as-meta-vars> args // Cheat: fake meta-vars. + ; <check-meta-vars> body + |}) + + add-args-as-meta-vars = + map({a: + (?_#([a]) <+ ice(|"add-args-as-meta-vars", "invalid argument", <id>)) + ; <add-meta-var> a + }) + +strategies + check-all-identifers-are-meta-vars = (?Identifier(_); check-meta-var-declared) <+ all(check-all-identifers-are-meta-vars) @@ -53,7 +69,6 @@ check-meta-var-unicity ; ?meta-var ; rules(MetaVars: meta-var) - ; rules(UnscopedMetaVarList: meta-var) check-meta-var-declared = ?Identifier(idf) @@ -61,25 +76,32 @@ /* static consts can be seen as a meta-vars here. */ + <ExpandStaticConsts> Identifier(idf) /* formulas too, as long as they are statically evaluable. */ - + (<ExpandFormulas> Identifier(idf) - ; check-all-identifers-are-meta-vars)) then - err-msg(|<concat-strings>["undeclared meta-var: ", idf]) + + ( + ( <ExpandFormulas> Identifier(idf) + + <ExpandPFormulas> Identifier(idf) + ) + /* if we successfully expanded a formula we need to check + * it's made only of meta-vars. */ + ; check-all-identifers-are-meta-vars + ) + ) then + err-msg(|["undeclared meta-var: ", idf]) ; <xtc-exit> 2 end check-meta-var-unicity = ?Identifier(idf) ; if <MetaVars> Identifier(idf) then - err-msg(|<concat-strings>["meta-var already defined: ", idf]) + err-msg(|["meta-var already defined: ", idf]) ; <xtc-exit> 2 end ; if <ExpandStaticConsts> Identifier(idf) then - err-msg(|<concat-strings>["cannot redefine `", idf, "': already ", + err-msg(|["cannot redefine `", idf, "': already ", "defined as a constant value"]) ; <xtc-exit> 2 end ; if <ExpandFormulas> Identifier(idf) then - err-msg(|<concat-strings>["cannot redefine `", idf, "': already ", + err-msg(|["cannot redefine `", idf, "': already ", "defined as a formula"]) ; <xtc-exit> 2 end Index: src/str/inline.str --- src/str/inline.str (revision 0) +++ src/str/inline.str (revision 0) @@ -0,0 +1,42 @@ +module inline + +strategies + + /** + ** Inline a call to a parameterized formula. + ** @param fname Name of the formula called (only used for + ** error messages) [string] + ** @param formal-args List of formal arguments. + ** @param effective-args List of effective arguments. + */ + inline-call(|fname, formal-args, effective-args) = + (<replace-formal-args>(fname, formal-args, effective-args, <id>) + <+ ice(|"inline-call", "replace-formal-args failed", <id>)) + +rules + + // terminate the recursion + replace-formal-args: (_, [], [], b) -> b + + replace-formal-args: + (fname, [x|xs], [], b) -> b + where err-msg(|["invalid call to the parameterized formula `", fname + ,"': not enough arguments"]) + ; <xtc-exit> 6 + + replace-formal-args: + (fname, [], [y|ys], b) -> b + where err-msg(|["invalid call to the parameterized formula `", fname + ,"': too many arguments"]) + ; <xtc-exit> 6 + + replace-formal-args: + (fname, [x|xs], [y|ys], b) -> b' + where (<?_#([x'])>x <+ ice(|"replace-formal-args", "invalid argument", x)) + //<topdown(\ x -> y \)> b // => SIGSEGV! + // FIXME: Type checking: does y (effective arg) have a compatible + // type with x (formal arg)? + ; <topdown(try(?x'; !y))> b + ; <replace-formal-args>(fname, xs, ys, <id>) => b' + + Index: src/str/xrm-to-prism.str --- src/str/xrm-to-prism.str (revision 65) +++ src/str/xrm-to-prism.str (working copy) @@ -17,13 +17,13 @@ ** - ExpandFormulas: created by the strategy collect-formulas and used by ** prism-desugar for constant propagation. Maps an identifier with an ** expression. +** - ExpandPFormulas: Same as ExpandFormulas but for parameterized +** formulas. ** - 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. ** - MetaVars: (scoped) temporary used by check-meta-vars to store the list ** of meta-vars declared in the current scope. -** - UnscopedMetaVarList: Same as MetaVars but unscoped. Used as a *dirty* -** workaround to allow declarations using meta-vars. */ module xrm-to-prism imports @@ -50,11 +50,13 @@ * Two goals: expand them if needed, look for variable name conflicts. */ ; log-timed( if <is-module-file> start-symbol then - ModulesFile(id, map(try(collect-static-const-decl) - ; try(collect-formulas))) + ModulesFile(id, map(try(collect-static-const-decl + + collect-formulas + + collect-pformulas))) else - PropertiesFile(map(try(collect-static-const-decl) - ; try(collect-and-remove-formulas))) + PropertiesFile(map(try(collect-static-const-decl + + collect-and-remove-formulas + + collect-pformulas))) end | "Collecting static const and formulas", 2) @@ -66,10 +68,14 @@ /* unroll meta loops, eval meta if */ ; 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) + /* Useful for debugging: + ; log-timed( + where( + write-to => FILE(tmp-file) ; <xtc-command(!"pp-aterm")> ["-i", tmp-file, "-o", "debug.aterm"] - )*/ + ) + | "debug: pretty printing current AST in ATerms to debug.aterm", 2) + */ /* Desugar array declarations * eg: x[4][5] is transformed into two nested meta for loops @@ -102,15 +108,26 @@ | "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? + /* Remove array accesses: x[i] -> x_i + * Remove calls to parameterized formulas. + */ + // FIXME: can we make this more efficient than a complete innermost? ; if <is-module-file> start-symbol then - log-timed(bottomup(try(flatten-array-access)) + log-timed( + innermost( + flatten-array-access + <+ expand-pformulas + ) | "Desugaring array accesses", 2) else /* NOTE: for XPCTL files we also need to expand use of XRM-Formulas * because the original definition has been removed. */ - log-timed(innermost(flatten-array-access <+ ExpandFormulas) + log-timed( + innermost( + flatten-array-access + <+ (expand-pformulas;debug(!"after expand-pformulas: ")) + <+ ExpandFormulas + ) | "Desugaring array accesses", 2) end Index: src/str/prism-desugar.str --- src/str/prism-desugar.str (revision 65) +++ src/str/prism-desugar.str (working copy) @@ -41,16 +41,18 @@ ** 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. + ** formulas and ExpandFormulas and ExpandPFormulas. */ prism-desugar-first-pass = ?Int(_); IntToDouble - <+ ExpandStaticConsts; prism-desugar-first-pass // we must desugar the + <+ ExpandStaticConsts; prism-desugar-first-pass // We must desugar the <+ ExpandFormulas; prism-desugar-first-pass // expansed code. + <+ ExpandPFormulas; prism-desugar-first-pass // Ditto. <+ ConstInt(id, prism-desugar) <+ ConstDouble(id, prism-desugar) <+ ConstBool(id, prism-desugar) <+ FormulaDef(id, prism-desugar) + <+ PFormulaDef(id, id, prism-desugar) // parameterized formula defs. <+ all(prism-desugar-first-pass) rules @@ -283,6 +285,18 @@ rules 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 ]| EvalAnd: |[ e & false ]| -> |[ false ]| @@ -294,6 +308,18 @@ |[ true & e ]| -> |[ e ]| EvalOr: + |[ d | e ]| -> |[ true ]| + where <not(real-eq)>(d, "0") + EvalOr: + |[ d | e ]| -> |[ e ]| + where <real-eq>(d, "0") + EvalOr: + |[ e | d ]| -> |[ true ]| + where <not(real-eq)>(d, "0") + EvalOr: + |[ e | d ]| -> |[ e ]| + where <real-eq>(d, "0") + EvalOr: |[ true | e ]| -> |[ true ]| EvalOr: |[ e | true ]| -> |[ true ]| @@ -320,11 +346,11 @@ EvalIf: |[ d ? e1 : e2 ]| -> |[ e1 ]| - where <not(compare(real-eq))>(d, 0) + where <not(real-eq)>(d, "0") EvalIf: |[ d ? e1 : e2 ]| -> |[ e2 ]| - where <compare(real-eq)>(d, 0) + where <real-eq>(d, "0") /* ** ## ============= ## @@ -388,9 +414,5 @@ where <not(eq)>(i, "0") LitToBool: - |[ d ]| -> |[ false ]| - where <compare(real-eq)>(d, 0) - - LitToBool: - |[ d ]| -> |[ true ]| - where <not(compare(real-eq))>(d, 0) + |[ d ]| -> res + where <compare(real-eq)>(d, "0") => res Index: src/str/eval-meta-code.str --- src/str/eval-meta-code.str (revision 65) +++ src/str/eval-meta-code.str (working copy) @@ -48,8 +48,7 @@ if !condition-value => False() then <eval-meta-code> else-part else - ice(|"eval-meta-code", <concat-strings> [ - "the conditional test of a meta if could ", + ice(|"eval-meta-code", ["the conditional test of a meta if could ", "not be reduced to a single value (True or", " False), this should have been detected ", "earlier"], @@ -90,20 +89,17 @@ check-loop-validity(|meta-var, from, to, step) = !meta-var => Identifier(idf) ; if not(!from => Int(_); !to => Int(_); !step => Int(_)) then - err-msg(|<concat-strings>["invalid meta-for loop on the meta-var `", - idf, "': the value of the ", - "fields `from', `to' and `step' must be ", - "statically evaluable down to a ", - "simple integer"]) + err-msg(|["invalid meta-for loop on the meta-var `", idf, + "': the value of the fields `from', `to' and `step' must", + "be statically evaluable down to a simple integer"]) ; <debug> from ; <debug> to ; <debug> step ; <xtc-exit> 2 end ; if <gtS>(from, to) then - err-msg(|<concat-strings>["bad `for' loop on the meta-var ", - idf, " starts at ", from, - " which is less than ", to]) + err-msg(|["bad `for' loop on the meta-var ", idf, " starts at ", + from, " which is less than ", to]) ; <xtc-exit> 2 end Index: src/str/builtin-rand.str --- src/str/builtin-rand.str (revision 65) +++ src/str/builtin-rand.str (working copy) @@ -88,7 +88,7 @@ ?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: ", + err-msg(|["invalid call to XRM builtin: ", builtin-name, " takes either one or two arguments"]) ; !current-term; debug; <xtc-exit> 4 end @@ -100,8 +100,8 @@ <invalid-call-to-rand-non-int> current-term end ; if <gtS>(ifrom, ito) then - err-msg(|<concat-strings>["invalid call to XRM builtin: ", - builtin-name, "(x,y) where x > y"]) + err-msg(|["invalid call to XRM builtin: ", builtin-name + , "(x,y) where x > y"]) ; !current-term; debug; <xtc-exit> 4 end ; !(ifrom, ito) @@ -113,7 +113,7 @@ ; rules(RandUpdateList:+ _ -> rand-update) invalid-call-to-rand-non-int = - err-msg(|<concat-strings>["invalid call to XRM builtin: rand's", + err-msg(|["invalid call to XRM builtin: rand's", " arguments must be statically evaluable."]) ; debug ; <xtc-exit> 4 Index: src/str/ice.str --- src/str/ice.str (revision 65) +++ src/str/ice.str (working copy) @@ -2,35 +2,44 @@ ** Handle internal errors (things that should not happen) */ module ice +imports tool-doc // for package-bugreport strategies ice(|calling-strategy-name) = ice(|calling-strategy-name, "unknown reason") - /** Reports an ICE and exit 42 */ + /** Reports an ICE and exit 42. + ** @param reason string or list of strings. + */ ice(|calling-strategy-name, reason) = - log(|Critical(), <concat-strings>["internal compiler error in strategy ", - calling-strategy-name, ": ", reason]) + <is-list <+ ![<id>]> reason => reason' + ; log(|Critical(), ["internal compiler error in strategy ", + calling-strategy-name, ":\n", <?[<id>]>reason', + "\nPlease report this bug to ", <package-bugreport>]) ; <xtc-exit> 42 + /** Reports an ICE and exit 42. + ** @param reason string or list of strings. + ** @param term print this term before exiting. + */ ice(|calling-strategy-name, reason, term) = - // FIXME: if has-annotation ... - log(|Critical(), <concat-strings>["internal compiler error in strategy ", - calling-strategy-name, ": ", reason]) - ; !term - ; debug + // FIXME: if has-annotation ... (locations) + <is-list <+ ![<id>]> reason => reason' + ; log(|Critical(), ["internal compiler error in strategy ", + calling-strategy-name, ":\n", <?[<id>]>reason', + "\nPlease report this bug to ", <package-bugreport>] + , term) ; <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 ", + err-msg(|["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 ", + // FIXME: if has-annotation ... (locations) + err-msg(|["not yet implemented: ", what, " (in strategy ", calling-strategy-name, ")"]) - ; !term - ; debug + ; <debug> term ; <xtc-exit> 51 Index: src/str/collect-static-const-decl.str --- src/str/collect-static-const-decl.str (revision 65) +++ src/str/collect-static-const-decl.str (working copy) @@ -4,42 +4,29 @@ ** (see prism-desugar) */ module collect-static-const-decl -imports signatures +imports + signatures + inline strategies 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) @@ -49,14 +36,37 @@ collect-formulas = //?|[ formula x = e; ]| ?FormulaDef(x, e) - ; if <ExpandStaticConsts> x then - cannot-redefine-static-const(|x) - end - ; if <ExpandFormulas> x then - cannot-redefine-formula(|x) - end + ; check-identifier-unicity(|x) ; rules(ExpandFormulas: x -> e) +strategies + + collect-pformulas = + //?|[ formula x(a*) = e; ]| + ?PFormulaDef(name@Identifier(fname), args, body) + ; check-identifier-unicity(|name) + ; <innermost(ExpandStaticConsts + ExpandFormulas)> body => body' + // FIXME: Catch recursive call (error) + ; rules(ExpandPFormulas: + PFormulaCall(name, a*) -> e + where <inline-call(|fname, args, a*)> body' => e + ) + ; ![] // we remove the parameterized formula definition + +strategies + + /** Ensure that a call to a parameterized formula is expanded. Use this + ** to catch calls to undefined formulas. */ + expand-pformulas = + ?PFormulaCall(Identifier(fname), _) + ; (ExpandPFormulas <+ call-to-undefined-pformula(|fname)) + + call-to-undefined-pformula(|fname) = + err-msg(|["invalid call to the undefined parameterized formula `" + , fname, "'"]) + ; debug + ; <xtc-exit> 6 + rules collect-and-remove-formulas: @@ -68,20 +78,38 @@ ; if <ExpandFormulas> x then cannot-redefine-formula(|x) end + ; if <ExpandPFormulas> x then + cannot-redefine-parameterized-formula(|x) + end ; rules(ExpandFormulas: x -> e) strategies + check-identifier-unicity(|idf) = + if <ExpandStaticConsts> idf then + cannot-redefine-static-const(|idf) + end + ; if <ExpandFormulas> idf then + cannot-redefine-formula(|idf) + end + cannot-redefine-static-const(|idf) = !idf => Identifier(idf') - ; err-msg(|<concat-strings>["Cannot redefine `", idf', "': already defined", + ; err-msg(|["Cannot redefine `", idf', "': already defined", " as a static const variable."]) ; <debug> (<ExpandStaticConsts> idf) ; <xtc-exit> 2 cannot-redefine-formula(|idf) = !idf => Identifier(idf') - ; err-msg(|<concat-strings>["Cannot redefine `", idf', "': already defined", + ; err-msg(|["Cannot redefine `", idf', "': already defined", " as a formula."]) ; <debug> (<ExpandFormulas> idf) ; <xtc-exit> 2 + + cannot-redefine-parameterized-formula(|idf) = + !idf => Identifier(idf') + ; err-msg(|["Cannot redefine `", idf', "': already defined", + " as a parameterized formula."]) + ; <debug> (<ExpandPFormulas> idf) + ; <xtc-exit> 2 Index: src/str/desugar-array-access.str --- src/str/desugar-array-access.str (revision 65) +++ src/str/desugar-array-access.str (working copy) @@ -40,7 +40,6 @@ collect-all(?ArrayAccess(_, <id>), conc) // collect gives us the list... ; reverse // ... with deepest array accesses first (we want the opposite) ; prism-desugar - ; if has-meta-vars then ice(|"desugar-subscripts", "shouldn't be here") end ; map( // traverse the list of dimensions map( // traverse the subscripts for a given dimension if ?Int(_) then @@ -58,9 +57,6 @@ ; flatten-list // because Ranges create nested lists ) // end outer map - has-meta-vars = - oncetd(?Identifier(_); UnscopedMetaVarList) - strategies /** Create the Cartesian product of all possible array subscripts. Index: src/str/reals.str --- src/str/reals.str (revision 65) +++ src/str/reals.str (working copy) @@ -66,9 +66,11 @@ ** => tests if there difference is less than the precision given in parameter ** operates on the input term (a, b) ** eg: <real-eq(|0.00001)> ("0.42", "0.43") -> fail + ** NOTE: The current term must be a tuple of strings containing reals! */ real-eq(|precision) = - (string-to-real, string-to-real) + ((is-string, is-string) <+ ice(|"real-eq", "bad call.")) + ; (string-to-real, string-to-real) ; subtr ; abs => difference ; <not(gtr)>(difference, precision) Index: src/syn/xrm/XRM-Formula.sdf --- src/syn/xrm/XRM-Formula.sdf (revision 65) +++ src/syn/xrm/XRM-Formula.sdf (working copy) @@ -7,8 +7,26 @@ exports %% the whole PRISM stuff.. dirty hack inside! %% EBNF Grammar: Extended Formulas - %% FormulaDef ::= "formula" ArrayAccess "=" Expression ";" + %% FormulaDef ::= + %% "formula" ArrayAccess "=" Expression ";" + %% | "formula" Identifier "(" {Argument ","} ")" "=" Expression ";" + %% + %% Argument ::= + %% "int" Identifier + %% | "double" Identifier + %% | "bool" Identifier context-free syntax "formula" ArrayAccess "=" Expression ";" -> FormulaDef {cons("FormulaDef")} + + context-free syntax + "formula" Identifier "(" {Argument ","}* ")" "=" Expression ";" + -> FormulaDef {cons("PFormulaDef")} + + sorts Argument + context-free syntax + "int" Identifier -> Argument {cons("IntArg")} + "double" Identifier -> Argument {cons("DoubleArg")} + "bool" Identifier -> Argument {cons("BoolArg")} + "exp" Identifier -> Argument {cons("ExpArg")} Index: src/syn/xrm/XRM-Keywords.sdf --- src/syn/xrm/XRM-Keywords.sdf (revision 65) +++ src/syn/xrm/XRM-Keywords.sdf (working copy) @@ -3,6 +3,10 @@ exports lexical syntax "for" -> Keyword + "rand" -> Keyword + "static_rand" -> Keyword lexical restrictions "for" -/- [A-Za-z0-9\_] + "rand" -/- [A-Za-z0-9\_] + "static_rand" -/- [A-Za-z0-9\_] Index: src/syn/xrm/XRM-Expression.sdf --- src/syn/xrm/XRM-Expression.sdf (revision 65) +++ src/syn/xrm/XRM-Expression.sdf (working copy) @@ -42,6 +42,10 @@ "func" "(" "static_rand" "," {Expression ","}+ ")" -> Expression {cons("StaticRand")} + %% "Function" calls (parametrized formulas) + Identifier "(" {Expression ","}+ ")" + -> Expression {cons("PFormulaCall")} + %% Ranges in XRM with different priority (for array accesses) sorts XRMRange context-free syntax Index: tests/pctl/xrm-formula.xpctl --- tests/pctl/xrm-formula.xpctl (revision 0) +++ tests/pctl/xrm-formula.xpctl (revision 0) @@ -0,0 +1,5 @@ +formula lfree = p2=0..4,6,10; +formula isfree(int i) = p[i]=0..4,6,10; + +P=? [ true U lfree ] +Pmin=? [ true U isfree(2) ] Index: tests/xrm/if-desugar.xpm --- tests/xrm/if-desugar.xpm (revision 0) +++ tests/xrm/if-desugar.xpm (revision 0) @@ -0,0 +1,4 @@ +const int success = 1; +const int fail = 0; + +const int test = 42 ? success : fail; Index: tests/xrm/rand.xpm --- tests/xrm/rand.xpm (revision 65) +++ tests/xrm/rand.xpm (working copy) @@ -1,5 +1,5 @@ -module rand // NOTE: no conflict here (rand isn't a reserved name) +module randtest // NOTE: rand is now a reserved keyword x : [0..42]; y : [0..1]; [] x=0 -> (x'=rand(5)); Index: tests/xrm/parametrized-formula.xpm --- tests/xrm/parametrized-formula.xpm (revision 0) +++ tests/xrm/parametrized-formula.xpm (revision 0) @@ -0,0 +1,3 @@ +formula add(int lhs, int rhs) = lhs + rhs; + +const int test = add(1, 2); Index: tests/test-parse-xrm.sh.in --- tests/test-parse-xrm.sh.in (revision 65) +++ tests/test-parse-xrm.sh.in (working copy) @@ -18,7 +18,7 @@ "@top_builddir@/src/tools/parse-xrm" -i "$file" -o /dev/null rv=$? test_cnt=$((test_cnt + 1)) - if [ $? -eq 0 ]; then + if [ $rv -eq 0 ]; then echo 'OK, no ambiguities found' test_pass=$((test_pass + 1)) else Index: tests/test-parse-xpctl.sh.in --- tests/test-parse-xpctl.sh.in (revision 65) +++ tests/test-parse-xpctl.sh.in (working copy) @@ -18,7 +18,7 @@ "@top_builddir@/src/tools/parse-xpctl" -i "$file" -o /dev/null rv=$? test_cnt=$((test_cnt + 1)) - if [ $? -eq 0 ]; then + if [ $rv -eq 0 ]; then echo 'OK, no ambiguities found' test_pass=$((test_pass + 1)) else Index: TODO --- TODO (revision 65) +++ TODO (working copy) @@ -94,8 +94,6 @@ * 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) - * Add scopes for meta variables eg: for i ... do for i ... // `i' shadows its previous definition @@ -268,3 +266,5 @@ * Write some sort of formal descriptions of the extensions offered. => see under /doc + + * Add parameterized formulas. (Pretty much like macro-functions in C) Index: doc/user-guide.txt --- doc/user-guide.txt (revision 65) +++ doc/user-guide.txt (working copy) @@ -101,8 +101,9 @@ - 1: rewriting failed (eg: it might be a bug in xrm-front) - 2: error with meta-vars (eg: undefined meta-var, redefined meta-var) - 3: arithmetic error when evaluating code (eg: division/modulo by 0) - - 4: invalid call to a builtin (eg rand(1,2,3)) + - 4: invalid call to a builtin (eg: rand(1,2,3)) - 5: invalid array access (eg: subscript is not a positive integer) + - 6: invalid call to a parameterized formula (eg: not enough arguments) - 42: internal compiler error (please send a bug report) - 51: not yet implemented @@ -308,6 +309,8 @@ XRM introduces two new builtins for generating random numbers: rand and static_rand. + o In XRM, "rand" and "static_rand" are reserved keywords and cannot be + used for identifiers. o Both rand and static_rand take either one or two arguments which must be evaluable down to simple integers at compile-time. If rand or static_rand is called with a single argument, a second @@ -350,6 +353,28 @@ in the module which called rand. The variable will be updated each time it's accessed to ensure real random numbers. + # XRM Parameterized formulas + -------------------------- + XRM formulas have been eXtended and can now be parameterized, eg: + formula isfree(int i) = p[i]=0..4,6,10; + Parameterized formulas can have 4 kinds of arguments: + o int (as in the example above) + o double + o bool + o exp + With the `exp' type, the formula behaves a bit like C's macro-functions. + We can also see that as a void type since no type-checking will be + performed on this kind of arguments. + Parameterized formulas definitions will be removed in the output PRISM + code. Invoking parameterized formulas is somewhat like calling a + function, eg: + isfree(2) will be inlined as p[2]=0..4,6,10; + However note that using the PRISM-3 calling style for builtins cannot be + used for formulas, eg: func(isfree, 2) is not supported at the moment. We + _might_ add support for this. + Once a parameterized formula has been defined, it can't be + redefined/undefined, just like a normal PRISM formula. + ************************** * XRM and Property Files * ************************** @@ -357,6 +382,8 @@ 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. + It is also possible to define formulas and parameterized formulas in + XPCTL files. ********************* * Incoming features *