diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.lem | 3 | ||||
| -rw-r--r-- | language/l2.ml | 3 | ||||
| -rw-r--r-- | language/l2.ott | 1 |
3 files changed, 5 insertions, 2 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 diff --git a/language/l2.ml b/language/l2.ml index 6a062418..9f7b1636 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -1,4 +1,4 @@ -(* generated by Ott 0.24 from: l2.ott *) +(* generated by Ott 0.25 from: l2.ott *) type text = string @@ -273,6 +273,7 @@ type | 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 *) | E_internal_plet of 'a pat * 'a exp * 'a exp (* This is an internal node, used to distinguised some introduced lets during processing from original ones *) + | E_internal_return of 'a exp (* For internal use to embed into monad definition *) and 'a exp = E_aux of 'a exp_aux * 'a annot diff --git a/language/l2.ott b/language/l2.ott index 599d7bdc..736b1c99 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -649,6 +649,7 @@ exp :: 'E_' ::= | 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 }} | let pat = exp in exp' :: :: internal_plet {{ com This is an internal node, used to distinguised some introduced lets during processing from original ones }} + | return ( exp ) :: :: internal_return {{ com For internal use to embed into monad definition }} lexp :: 'LEXP_' ::= {{ com lvalue expression }} |