From c55929d04de367ebf84eac485199690d5daf0ed7 Mon Sep 17 00:00:00 2001
From: Kathy Gray
Date: Thu, 26 Jun 2014 14:44:50 +0100
Subject: 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

---
 language/l2.lem       | 3 ++-
 language/l2.ml        | 3 ++-
 language/l2.ott       | 4 +++-
 language/l2_parse.ml  | 1 +
 language/l2_parse.ott | 2 ++
 5 files changed, 10 insertions(+), 3 deletions(-)

(limited to 'language')

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 }}
 
-- 
cgit v1.2.3