diff options
| author | Christopher Pulte | 2015-10-19 15:36:34 +0100 |
|---|---|---|
| committer | Christopher Pulte | 2015-10-19 15:36:34 +0100 |
| commit | 602adb432b158efa403959454328bc58bddca61b (patch) | |
| tree | 20e4ce2a4c7461a39c5a1052fa201e21fd1b6720 /language/l2.lem | |
| parent | a72c474c2a5902f72ab63f21dc071a22d449b63b (diff) | |
progress on lem backend
Diffstat (limited to 'language/l2.lem')
| -rw-r--r-- | language/l2.lem | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/language/l2.lem b/language/l2.lem index 9fc9db25..71c6da00 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 @@ -284,6 +284,7 @@ and exp_aux 'a = (* Expression *) | 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 *) | E_internal_plet of (pat 'a) * (exp 'a) * (exp 'a) (* This is an internal node, used to distinguised some introduced lets during processing from original ones *) + | E_internal_return of (exp 'a) (* For internal use to embed into monad definition *) and exp 'a = | E_aux of (exp_aux 'a) * annot 'a |