summaryrefslogtreecommitdiff
path: root/language
diff options
context:
space:
mode:
Diffstat (limited to 'language')
-rw-r--r--language/l2.lem1
-rw-r--r--language/l2.ml1
-rw-r--r--language/l2.ott2
3 files changed, 3 insertions, 1 deletions
diff --git a/language/l2.lem b/language/l2.lem
index 63869068..1055a8ff 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -281,6 +281,7 @@ and exp_aux 'a = (* Expression *)
| 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_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_internal_let of (lexp 'a) * (exp 'a) * (exp 'a) (* This is an internal node for compilation that demonstrates the scope of a local mutable variable *)
and exp 'a =
| E_aux of (exp_aux 'a) * annot 'a
diff --git a/language/l2.ml b/language/l2.ml
index ea3252da..d5ea7c33 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -270,6 +270,7 @@ type
| 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_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_internal_let of 'a lexp * 'a exp * 'a exp (* This is an internal node for compilation that demonstrates the scope of a local mutable variable *)
and 'a exp =
E_aux of 'a exp_aux * 'a annot
diff --git a/language/l2.ott b/language/l2.ott
index 721ee60f..eea0fba1 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -646,7 +646,7 @@ exp :: 'E_' ::=
| ( 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 }}
| annot , annot' :: :: internal_exp_user {{ com This is like the above but the user has specified an implicit parameter for the current function }}
-
+ | let lexp = exp in exp' :: :: internal_let {{ com This is an internal node for compilation that demonstrates the scope of a local mutable variable }}
lexp :: 'LEXP_' ::= {{ com lvalue expression }}