diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/rewrites.ml | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/src/rewrites.ml b/src/rewrites.ml index c9eece20..64cfe48b 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -3662,19 +3662,19 @@ let rewrite_defs_remove_superfluous_letbinds env = when Id.compare id id' = 0 && small exp1 && not (effectful exp1) -> let (E_aux (_,e1annot)) = exp1 in E_aux (E_internal_return (exp1),e1annot) + | _, (E_aux (E_throw e, a), _), _ -> E_aux (E_throw e, a) + | (pat, _), (E_aux (E_assert (c, msg), a) as assert_exp, _), _ -> + begin match typ_of c with + | Typ_aux (Typ_app (Id_aux (Id "atom_bool", _), [A_aux (A_bool nc, _)]), _) + when prove __POS__ (env_of c) (nc_not nc) -> + (* Drop rest of block after an 'assert(false)' *) + let exit_exp = E_aux (E_exit (infer_exp (env_of c) (mk_lit_exp L_unit)), a) in + E_aux (E_internal_plet (pat, assert_exp, exit_exp), annot) + | _ -> + E_aux (exp, annot) + end | _ -> E_aux (exp,annot) end - | E_internal_plet (_, E_aux (E_throw e, a), _) -> E_aux (E_throw e, a) - | E_internal_plet (pat, (E_aux (E_assert (c, msg), a) as assert_exp), _) -> - begin match typ_of c with - | Typ_aux (Typ_app (Id_aux (Id "atom_bool", _), [A_aux (A_bool nc, _)]), _) - when prove __POS__ (env_of c) (nc_not nc) -> - (* Drop rest of block after an 'assert(false)' *) - let exit_exp = E_aux (E_exit (infer_exp (env_of c) (mk_lit_exp L_unit)), a) in - E_aux (E_internal_plet (pat, assert_exp, exit_exp), annot) - | _ -> - E_aux (exp, annot) - end | _ -> E_aux (exp,annot) in let alg = { id_exp_alg with e_aux = e_aux } in |