summaryrefslogtreecommitdiff
path: root/language/l2.lem
diff options
context:
space:
mode:
authorKathy Gray2015-09-24 11:46:21 +0100
committerKathy Gray2015-09-24 11:57:00 +0100
commit30780bad55a5b20f7f894464913a012a8635640d (patch)
tree6867525787d4bfb0d94650f00d830e13df6d3e0e /language/l2.lem
parentddd603c61644bdef9e5b98860a448348b90b614e (diff)
Parameterise the rewriter's for multiple different rewritings
Add a new internal node for moving assignments into scope-preserving expressions that more explicitly define the scope
Diffstat (limited to 'language/l2.lem')
-rw-r--r--language/l2.lem1
1 files changed, 1 insertions, 0 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