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