Also add to ott

5 files changed, 15 insertions, 5 deletions

diff --git a/language/l2.lem b/language/l2.lem
index a845f1f6..dd300c89 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -1,4 +1,4 @@
-(* generated by Ott 0.24 from: l2_typ.ott l2.ott *)
+(* generated by Ott 0.25 from: l2_typ.ott l2.ott *)
 open import Pervasives
 
 open import Map
@@ -255,10 +255,12 @@ type exp_aux 'a =  (* Expression *)
  | E_case of (exp 'a) * list (pexp 'a) (* pattern matching *)
  | E_let of (letbind 'a) * (exp 'a) (* let expression *)
  | E_assign of (lexp 'a) * (exp 'a) (* imperative assignment *)
+ | E_sizeof of nexp (* Expression to return the value of the nexp variable or expression at run time *)
  | E_exit of (exp 'a) (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *)
- | E_assert of (exp 'a) * (exp 'a) (* expression to halt with error, when the first expression is true, reporting the optional string as an error *)
+ | E_assert of (exp 'a) * (exp 'a) (* expression to halt with error, when the first expression is false, reporting the optional string as an error *)
  | E_internal_cast of annot 'a * (exp 'a) (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *)
  | E_internal_exp of annot 'a (* This is an internal use for passing nexp information  to library functions, postponed for constraint solving *)
+ | E_sizeof_internal of annot 'a (* For sizeof during type checking, to replace nexp with internal n *)
  | E_internal_exp_user of annot 'a * annot 'a (* This is like the above but the user has specified an implicit parameter for the current function *)
  | E_comment of string (* For generated unstructured comments *)
  | E_comment_struc of (exp 'a) (* For generated structured comments *)
diff --git a/language/l2.ml b/language/l2.ml
index fbc52b10..931bc01f 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -1,4 +1,4 @@
-(* generated by Ott 0.24 from: l2.ott *)
+(* generated by Ott 0.25 from: l2.ott *)
 
 
 type text = string
@@ -269,10 +269,12 @@ type
  | E_case of 'a exp * ('a pexp) list (* pattern matching *)
  | E_let of 'a letbind * 'a exp (* let expression *)
  | E_assign of 'a lexp * 'a exp (* imperative assignment *)
+ | E_sizeof of nexp (* Expression to return the value of the nexp variable or expression at run time *)
  | E_exit of 'a exp (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *)
- | E_assert of 'a exp * 'a exp (* expression to halt with error, when the first expression is true, reporting the optional string as an error *)
+ | E_assert of 'a exp * 'a exp (* expression to halt with error, when the first expression is false, reporting the optional string as an error *)
  | E_internal_cast of 'a annot * 'a exp (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *)
  | E_internal_exp of 'a annot (* This is an internal use for passing nexp information  to library functions, postponed for constraint solving *)
+ | E_sizeof_internal of 'a annot (* For sizeof during type checking, to replace nexp with internal n *)
  | E_internal_exp_user of 'a annot * 'a annot (* This is like the above but the user has specified an implicit parameter for the current function *)
  | E_comment of string (* For generated unstructured comments *)
  | E_comment_struc of 'a exp (* For generated structured comments *)
diff --git a/language/l2.ott b/language/l2.ott
index 345c7707..4af3b9a3 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -662,6 +662,9 @@ exp :: 'E_' ::=
   | lexp := exp                                      :: :: assign
     {{ com imperative assignment }}
 
+  | sizeof nexp                                         :: :: sizeof
+  {{ com Expression to return the value of the nexp variable or expression at run time }}
+
   | exit exp						:: :: exit
     {{ com expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp }}
   | assert ( exp , exp' )                            :: :: assert
@@ -669,6 +672,7 @@ exp :: 'E_' ::=
   | ( exp )                                             :: S :: paren {{ ichlo [[exp]] }}
   | ( annot ) exp                                   :: :: internal_cast {{ com This is an internal cast, generated during type checking that will resolve into a syntactic cast after }}
   | annot                       :: :: internal_exp {{ com This is an internal use for passing nexp information  to library functions, postponed for constraint solving }}
+  | sizeof annot             :: :: sizeof_internal {{ com For sizeof during type checking, to replace nexp with internal n}}
   | annot , annot'           :: :: internal_exp_user {{ com This is like the above but the user has specified an implicit parameter for the current function }}
   | comment string            :: :: comment {{ com For generated unstructured comments }}
   | comment exp               :: :: comment_struc {{ com For generated structured comments }}
diff --git a/language/l2_parse.ml b/language/l2_parse.ml
index d4d71cfe..b94d16fe 100644
--- a/language/l2_parse.ml
+++ b/language/l2_parse.ml
@@ -1,4 +1,4 @@
-(* generated by Ott 0.24 from: l2_parse.ott *)
+(* generated by Ott 0.25 from: l2_parse.ott *)
 
 
 type text = string
@@ -231,6 +231,7 @@ exp_aux =  (* Expression *)
  | E_case of exp * (pexp) list (* pattern matching *)
  | E_let of letbind * exp (* let expression *)
  | E_assign of exp * exp (* imperative assignment *)
+ | E_sizeof of atyp
  | E_exit of exp
  | E_assert of exp * exp
 
diff --git a/language/l2_parse.ott b/language/l2_parse.ott
index 224fea06..d768c766 100644
--- a/language/l2_parse.ott
+++ b/language/l2_parse.ott
@@ -544,6 +544,7 @@ exp :: 'E_' ::=
   | exp := exp'                                      :: :: assign
     {{ com imperative assignment }}
 
+  | sizeof atyp                                         :: :: sizeof
   | exit exp						:: :: exit
   | assert ( exp , exp' )                               :: :: assert