diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.lem | 2 | ||||
| -rw-r--r-- | language/l2.ml | 2 | ||||
| -rw-r--r-- | language/l2.ott | 2 |
3 files changed, 6 insertions, 0 deletions
diff --git a/language/l2.lem b/language/l2.lem index 2fd685f4..0c94e399 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -240,6 +240,8 @@ 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_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 of an nexp (in the annot) for passing length information after resolution of constraints *) and exp 'a = | E_aux of (exp_aux 'a) * annot 'a diff --git a/language/l2.ml b/language/l2.ml index 80c94b39..927f702b 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -282,6 +282,8 @@ and 'a exp_aux = (* Expression *) | 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_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 of an nexp (in the annot) for passing length information after resolution of constraints *) and 'a exp = E_aux of 'a exp_aux * 'a annot diff --git a/language/l2.ott b/language/l2.ott index 8aa7417a..a6918526 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -628,6 +628,8 @@ exp :: 'E_' ::= {{ com imperative assignment }} | ( 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 of an nexp (in the annot) for passing length information after resolution of constraints }} lexp :: 'LEXP_' ::= {{ com lvalue expression }} |