Merge pull request #1015 from lorchrob/choose-op-syntax

Add generic "choose type" syntax

doc/usr/source/2_input/1_lustre.rst

@@ -1083,9 +1083,9 @@ nondeterministic behaviors must be modeled.
 Kind 2 offers a convenient binder of the form
 ``choose { x: T | P(x) }`` which denotes an arbitrary stream of
 values of type ``T`` each satisfying the predicate ``P``.
-In the expression above ``x`` is a locally bound variable of type ``T``,
-and ``P(x)`` is a Boolean expression that typically, 
-but not necessarily, contains ``x``. The expression ``P(x)``
+In the expression above ``x`` is a locally bound variable of
+Lustre type ``T``, and ``P(x)`` is a Lustre boolean expression that
+typically, but not necessarily, contains ``x``. The expression ``P(x)``
 may also contain any input, output, or local variable that
 are in the scope of the ``choose`` expression.
 The following example shows a component using the ``choose``
@@ -1104,6 +1104,10 @@ operator to define a local stream ``l`` of arbitrary odd values.
      z = y + l;
    tel
 
+In addition, the ``choose`` operator can take any Lustre type as argument.
+For instance, the expression ``choose int`` is also accepted
+and denotes an arbitrary stream of values of type ``int``.
+
 A challenge for the user with the use of ``choose`` expressions arises if
 the specified condition is inconsistent, or more generally, unrealizable.
 In that case, the system model may be satisfied by no execution trace.
@@ -1157,4 +1161,8 @@ was not included.
    let
      b = a + 10;
      z = choose { x: int | a <= x and x <= b assuming a<=b };
-   tel
+     check z>=a+10 => z=b;
+   tel
+
+Moreover, Kind 2 checks that any specified assumption in
+a choose expression holds when model checking the component.

src/lustre/lustreParser.messages

@@ -840,10 +840,6 @@ one_expr: WEAKLY LPARAMBRACKET WEAKLY SEMICOLON XOR
 
 Syntax Error!
 
-one_expr: WEAKLY LPARAMBRACKET WEAKLY XOR
-
-Syntax Error!
-
 one_expr: WEAKLY LPARAMBRACKET XOR
 
 Syntax Error!
@@ -2943,3 +2939,15 @@ Syntax Error!
 main: FUNCTION ASSUME LPAREN RPAREN RETURNS LPAREN RPAREN LET ASSERT CHOOSE LCURLYBRACKET ASSUME COLON ASSUME BAR ASSUME ASSUMING DECIMAL WEAKLY
 
 Syntax Error!
+
+one_expr: CHOOSE ASSUME WEAKLY
+
+Syntax Error!
+
+one_expr: CHOOSE ASSUME CARET DECIMAL WEAKLY
+
+Syntax Error!
+
+main: FUNCTION ASSUME LPAREN RPAREN RETURNS LPAREN RPAREN LET ASSERT CHOOSE ASSUME RPARAMBRACKET
+
+Syntax Error!

src/lustre/lustreParser.mly

@@ -218,6 +218,7 @@ let mk_span start_pos end_pos =
 %nonassoc INT REAL 
 %nonassoc NOT
 %nonassoc BVNOT 
+%nonassoc CHOOSE
 %left CARET 
 %left LSQBRACKET DOT DOTPERCENT
 
@@ -922,6 +923,8 @@ pexpr(Q):
     { A.ChooseOp (mk_pos $startpos, id, e, None) } 
   | CHOOSE; LCURLYBRACKET; id = typed_ident; BAR; e1 = pexpr(Q); ASSUMING; e2 = pexpr(Q); RCURLYBRACKET
     { A.ChooseOp (mk_pos $startpos, id, e1, Some e2) } 
+  | CHOOSE; ty = lustre_type;
+    { A.ChooseOp (mk_pos $startpos, (mk_pos $startpos, HString.mk_hstring "_", ty), Const(mk_pos $startpos, True), None)}
 
   (* Recursive node call *)
   | WITH; pexpr(Q); THEN; pexpr(Q); ELSE; pexpr(Q)