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 71c6da00..7abd595c 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -1,4 +1,4 @@ -(* generated by Ott 0.25 from: l2_typ.ott l2.ott *) +(* generated by Ott 0.24 from: l2_typ.ott l2.ott *) open import Pervasives open import Map @@ -75,6 +75,7 @@ type base_effect_aux = (* effect *) | BE_unspec (* unspecified values *) | BE_nondet (* nondeterminism from intra-instruction parallelism *) | BE_lset (* Local mutation happend; not user-writable *) + | BE_escape (* Internal tracking of expressions and functions that might call exit *) type base_effect = diff --git a/language/l2.ml b/language/l2.ml index 9f7b1636..2f2bc839 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -1,4 +1,4 @@ -(* generated by Ott 0.25 from: l2.ott *) +(* generated by Ott 0.24 from: l2.ott *) type text = string @@ -72,6 +72,7 @@ base_effect_aux = (* effect *) | BE_unspec (* unspecified values *) | BE_nondet (* nondeterminism from intra-instruction parallelism *) | BE_lset (* Local mutation happend; not user-writable *) + | BE_escape (* Internal tracking of expressions and functions that might call exit *) type diff --git a/language/l2.ott b/language/l2.ott index 736b1c99..fcd3abe8 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -194,6 +194,7 @@ base_effect :: 'BE_' ::= | unspec :: :: unspec {{ com unspecified values }} | nondet :: :: nondet {{ com nondeterminism from intra-instruction parallelism }} | lset :: :: lset {{ com Local mutation happend; not user-writable }} + | escape :: :: escape {{ com Internal tracking of expressions and functions that might call exit }} effect :: 'Effect_' ::= |