CN: Make assert optional

[dc-mak]

diff --git a/parsers/c/c_parser.mly b/parsers/c/c_parser.mly
index f3aea1d1c..313eec789 100644
--- a/parsers/c/c_parser.mly
+++ b/parsers/c/c_parser.mly
@@ -2332,6 +2332,7 @@ cn_option_func_body:
     { Some cn_func_body }
 |
     { None }
+;

 clause:
 | CN_TAKE str= cn_variable EQ res= resource SEMICOLON c= clause
@@ -2340,7 +2341,7 @@ clause:
 | CN_LET str= cn_variable EQ e= expr SEMICOLON c= clause
     { let loc = point $startpos(str) in
       Cerb_frontend.Cn.CN_letExpr (loc, str, e, c) }
-| ASSERT e= delimited(LPAREN, assert_expr, RPAREN) SEMICOLON c= clause
+| e=assert_clause SEMICOLON c= clause
     { Cerb_frontend.Cn.CN_assert (region $loc noCursor, e, c) }
 | RETURN ret= expr
     { Cerb_frontend.Cn.CN_return (region $loc(ret) noCursor, ret) }
@@ -2350,7 +2351,6 @@ clause:
         CNExpr (region $loc noCursor, CNExpr_const CNConst_unit)) }
 ;

-
 assert_expr:
 | CN_EACH LPAREN bTy= base_type str= cn_variable SEMICOLON e1= expr RPAREN
       LBRACE e2= expr RBRACE
@@ -2358,8 +2358,14 @@ assert_expr:
                                       , bTy, e1, e2) }
 | e= expr_without_let
     { Cerb_frontend.Cn.CN_assert_exp e }
+;

-
+assert_clause:
+| ASSERT e= delimited(LPAREN, assert_expr, RPAREN)
+    { e }
+| e= assert_expr
+    { e }
+;

 resource:
 | p= pred es= delimited(LPAREN, separated_list(COMMA, expr), RPAREN)
@@ -2401,7 +2407,7 @@ condition:
 | CN_LET str= cn_variable EQ e= expr SEMICOLON
     { let loc = point $startpos(str) in
       Cerb_frontend.Cn.CN_cletExpr (loc, str, e) }
-| e= assert_expr SEMICOLON
+| e= assert_clause SEMICOLON
     { Cerb_frontend.Cn.CN_cconstr (region $loc noCursor, e) }
 ;

@@ -2496,7 +2502,7 @@ cn_statement:
 | CN_APPLY id=cn_variable es= delimited(LPAREN, separated_list(COMMA, expr), RPAREN) SEMICOLON
     { let loc = region ($startpos, $endpos) noCursor in
       CN_statement (loc, CN_apply (id, es)) }
-| ASSERT LPAREN e=assert_expr RPAREN SEMICOLON
+| e=assert_clause SEMICOLON

This is the obvious thing to try, but the issue is that it causes an extra conflict in the parser because this

** Conflict (shift/reduce) in state 1780.
** Tokens involved: STAR SEMICOLON MINUS LBRACK AMPERSAND
** The following explanations concentrate on token STAR.
** This state is reached from cn_toplevel after reading:

CN_PREDICATE cn_attrs cn_pred_output UNAME VARIABLE LPAREN cn_args RPAREN LBRACE RETURN

** The derivations that appear below have the following common factor:
** (The question mark symbol (?) represents the spot where the derivations begin to differ.)

cn_toplevel
list(cn_toplevel_elem) EOF
cn_toplevel_elem list(cn_toplevel_elem)
cn_predicate
CN_PREDICATE cn_attrs cn_pred_output UNAME VARIABLE LPAREN cn_args RPAREN cn_option_pred_clauses
                                                                          LBRACE clauses RBRACE
                                                                                 clause SEMICOLON
                                                                                 (?)

** In state 1780, looking ahead at STAR, reducing production
** prim_expr -> RETURN
** is permitted because of the following sub-derivation:

assert_clause SEMICOLON clause
assert_expr
expr_without_let
list_expr
bool_or_expr
bool_implies_expr
bool_and_expr
rel_expr
add_expr
mul_expr
mul_expr STAR unary_expr // lookahead token appears
unary_expr // lookahead token is inherited
prim_expr // lookahead token is inherited
RETURN .

** In state 1780, looking ahead at STAR, shifting is permitted
** because of the following sub-derivation:

RETURN expr
       expr_without_let
       list_expr
       bool_or_expr
       bool_implies_expr
       bool_and_expr
       rel_expr
       add_expr
       mul_expr
       unary_expr
       . STAR unary_expr

Simply put, inside a predicate definition, the parser is confused whether return * x; is meant to be a return statement, or an implicit assertion.

[dc-mak]

Solution may be to parameterise the production for primitive expressions over the return production: https://gallium.inria.fr/~fpottier/menhir/manual.html#sec32

[cp526]

There's the basic difference between predicates (return a value) and function specifications (don't).

If we want to unify the parsing of predicates and specifications, we could "rename" return in function specifications (as a binder for the return value) to something else: return in predicate definitions matches return in C (enough), but return in function specifications is maybe a bit confusing already?

[dc-mak]

Agreed, I guess we basically want a way to express this without using the "return" keyword and we would then have no conflict: randInt() /*@ ensures (0i32 <= return) && (return < 100i32); @*/.

If we want to pick a single name, then perhaps result? Or we can just ask the user to pick a name all the time with some syntax like ensures <binder>

[cp526]

Agreed, I guess we basically want a way to express this without using the "return" keyword and we would then have no conflict: randInt() /*@ ensures (0i32 <= return) && (return < 100i32); @*/.

If we want to pick a single name, then perhaps result? Or we can just ask the user to pick a name all the time with some syntax like ensures <binder>

A syntax that doesn't require a binder would be ideal. I like result; the name return (though perhaps slightly confusing) has the advantage that it's already a keyword in C, so it can't clash with any variable names in the C code.