diff options
| author | Kathy Gray | 2014-06-26 14:44:50 +0100 |
|---|---|---|
| committer | Kathy Gray | 2014-06-26 14:44:50 +0100 |
| commit | c55929d04de367ebf84eac485199690d5daf0ed7 (patch) | |
| tree | 5a7482cb88cd634955156234084b53fe154836dc /language | |
| parent | 5f3c514985ac2391aa5fff44b44d433b555b18e5 (diff) | |
Adding better support for unspecified values in indexed vectors
Also begining to add support for nondeterministic blocks and cleaning up some of the Many warnings on pattern matches
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 }} |