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 ##
## ---- ##