diff options
| author | Kathy Gray | 2016-05-12 14:06:10 +0100 |
|---|---|---|
| committer | Kathy Gray | 2016-05-27 10:10:09 +0100 |
| commit | 6145f35df564fa9bd502619dfd812df21cd9f333 (patch) | |
| tree | 26e21ccd2d1d9050593aa039fe8747d1e8898997 /language/l2.lem | |
| parent | 7b3bec91d88cbf79a5d69b3b6e9a1d761e423b3d (diff) | |
Also add to ott
Diffstat (limited to 'language/l2.lem')
| -rw-r--r-- | language/l2.lem | 6 |
1 files changed, 4 insertions, 2 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 *) |