diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.lem | 3 | ||||
| -rw-r--r-- | language/l2.ml | 3 | ||||
| -rw-r--r-- | language/l2.ott | 4 | ||||
| -rw-r--r-- | language/l2_parse.ml | 1 | ||||
| -rw-r--r-- | language/l2_parse.ott | 2 |
5 files changed, 10 insertions, 3 deletions
diff --git a/language/l2.lem b/language/l2.lem index af6b1485..3b86d2db 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -218,7 +218,8 @@ and fpat 'a = type exp_aux 'a = (* Expression *) - | E_block of list (exp 'a) (* block (parsing conflict with structs?) *) + | E_block of list (exp 'a) (* block *) + | E_nondet of list (exp 'a) (* nondeterminisitic block, expressions evaluate in an unspecified order, or concurrently *) | E_id of id (* identifier *) | E_lit of lit (* literal constant *) | E_cast of typ * (exp 'a) (* cast *) diff --git a/language/l2.ml b/language/l2.ml index e46014dc..a13ce981 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -232,7 +232,8 @@ typschm = type 'a exp_aux = (* Expression *) - E_block of ('a exp) list (* block (parsing conflict with structs?) *) + E_block of ('a exp) list (* block *) + | E_nondet of ('a exp) list (* nondeterminisitic block, expressions evaluate in an unspecified order, or concurrently *) | E_id of id (* identifier *) | E_lit of lit (* literal constant *) | E_cast of typ * 'a exp (* cast *) diff --git a/language/l2.ott b/language/l2.ott index c56a186b..55bad070 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -521,9 +521,11 @@ exp :: 'E_' ::= {{ com Expression }} {{ aux _ annot }} {{ auxparam 'a }} - | { exp1 ; ... ; expn } :: :: block {{ com block (parsing conflict with structs?) }} + | { exp1 ; ... ; expn } :: :: block {{ com block }} % maybe we really should have indentation-sensitive syntax :-) (given that some of the targets do) + | nondet { exp1 ; ... ; expn } :: :: nondet {{ com nondeterminisitic block, expressions evaluate in an unspecified order, or concurrently}} + | id :: :: id {{ com identifier }} diff --git a/language/l2_parse.ml b/language/l2_parse.ml index b54491bc..a96f1992 100644 --- a/language/l2_parse.ml +++ b/language/l2_parse.ml @@ -200,6 +200,7 @@ typschm = type exp_aux = (* Expression *) E_block of (exp) list (* block (parsing conflict with structs?) *) + | E_nondet of (exp) list (* block that can evaluate the contained expressions in any ordering *) | E_id of id (* identifier *) | E_lit of lit (* literal constant *) | E_cast of atyp * exp (* cast *) diff --git a/language/l2_parse.ott b/language/l2_parse.ott index e62e4587..a655959d 100644 --- a/language/l2_parse.ott +++ b/language/l2_parse.ott @@ -415,6 +415,8 @@ exp :: 'E_' ::= | { exp1 ; ... ; expn } :: :: block {{ com block (parsing conflict with structs?) }} % maybe we really should have indentation-sensitive syntax :-) (given that some of the targets do) + | nondet { exp1 ; ... ; expn } :: :: nondet {{ com block that can evaluate the contained expressions in any ordering }} + | id :: :: id {{ com identifier }} |