diff options
| author | Kathy Gray | 2015-11-24 19:05:10 +0000 |
|---|---|---|
| committer | Kathy Gray | 2015-11-24 19:05:10 +0000 |
| commit | 4c459ece7d01288d5529862e116fd75db9c1afd9 (patch) | |
| tree | 3ac2c7ca83274b666ba61d5c78633bd486105d1d /src | |
| parent | 10321a2cf266b57dfa5ebe3606d24ac3d6bc7d74 (diff) | |
Add BE_escape effect when an E_exit is seen
Close #20
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print.ml | 3 | ||||
| -rw-r--r-- | src/type_check.ml | 3 | ||||
| -rw-r--r-- | src/type_internal.ml | 4 |
3 files changed, 8 insertions, 2 deletions
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 |