Add BE_escape effect when an E_exit is seen

Close #20

6 files changed, 13 insertions, 4 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_' ::=
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 6b1b364a..2108c62f 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -149,7 +149,8 @@ and pp_format_base_effect_lem (BE_aux(e,l)) =
     | BE_undef -> "BE_undef"
     | BE_unspec -> "BE_unspec"
     | BE_nondet -> "BE_nondet"
-    | BE_lset -> "BE_lset") ^ " " ^
+    | BE_lset -> "BE_lset"
+    | BE_escape -> "BE_escape") ^ " " ^
   (pp_format_l_lem l) ^ ")"
 and pp_format_effects_lem (Effect_aux(e,l)) =
   "(Effect_aux " ^
diff --git a/src/type_check.ml b/src/type_check.ml
index 61a33d1a..634ad5aa 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1304,7 +1304,8 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       (E_aux(E_assign(lexp',exp'),(l,(Base(([],unit_t),tag,[],efl,effects,nob)))),unit_t,t_env',cs@cs'@c',b_env',effects)
     | E_exit e ->
       let (e',t',_,_,_,_) = check_exp envs imp_param (new_t ()) e in
-      (E_aux (E_exit e',(l,(simple_annot expect_t))),expect_t,t_env,[],nob,pure_e)
+      let efs = add_effect (BE_aux(BE_escape, l)) pure_e in
+      (E_aux (E_exit e',(l,(simple_annot_efr expect_t efs))),expect_t,t_env,[],nob,efs)
     | E_internal_cast _ | E_internal_exp _ | E_internal_exp_user _ | E_internal_let _
     | E_internal_plet _ | E_internal_return _ -> 
       raise (Reporting_basic.err_unreachable l "Internal expression passed back into type checker")
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 5366d5dd..0c1c953b 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -303,6 +303,7 @@ and ef_to_string (Ast.BE_aux(b,l)) =
       | Ast.BE_unspec-> "unspec"
       | Ast.BE_nondet-> "nondet"
       | Ast.BE_lset  -> "lset"
+      | Ast.BE_escape -> "escape" 
 and efs_to_string es = 
   match es with
     | [] -> ""
@@ -2403,6 +2404,9 @@ let compare_effect (BE_aux(e1,_)) (BE_aux(e2,_)) =
   | (BE_depend,_) -> -1
   | (_,BE_depend) -> 1
   | (BE_lset,BE_lset) -> 0
+  | (BE_lset,_) -> -1
+  | (_,BE_lset) -> 1
+  | (BE_escape,BE_escape) -> 0
 
 let effect_sort = List.sort compare_effect