From b938fd99a9f16d4bb2ef1c483574a2850aa6e640 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Tue, 19 Dec 2017 11:53:23 +0000
Subject: Support user-defined exceptions in Lem shallow embedding

The type-checker already supports a user-defined "exception" type that can be
used in throw and try-catch expressions.  This patch adds support for that to
the Lem shallow embedding by adapting the existing exception mechanisms of the
state and prompt monads.  User-defined exceptions are distinguished from
builtin exception cases.  For example, the state monad uses

type ex 'e =
  | Exit
  | Assert of string
  | Throw of 'e

to distinguish between calls to "exit", failed assertions, and user-defined
exceptions, respectively.  Early return is also handled using the exception
mechanism, by lifting to a monad with "either 'r exception" as the exception
type, where 'r is the expected return type and "exception" is the user-defined
exception type.
---
 src/rewriter.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'src/rewriter.ml')

diff --git a/src/rewriter.ml b/src/rewriter.ml
index 88fb17a5..31bcb577 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -130,12 +130,11 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with
     | E_record_update(e,fexps) ->
       union_effects (effect_of e) (effect_of_fexps fexps)
     | E_field (e,_) -> effect_of e
-    | E_case (e,pexps) ->
+    | E_case (e,pexps) | E_try (e,pexps) ->
       List.fold_left union_effects (effect_of e) (List.map effect_of_pexp pexps)
     | E_let (lb,e) -> union_effects (effect_of_lb lb) (effect_of e)
     | E_assign (lexp,e) -> union_effects (effect_of_lexp lexp) (effect_of e)
-    | E_exit e -> union_effects eff (effect_of e)
-    | E_return e -> union_effects eff (effect_of e)
+    | E_exit e | E_return e | E_throw e -> union_effects eff (effect_of e)
     | E_sizeof _ | E_sizeof_internal _ | E_constraint _ -> no_effect
     | E_assert (c,m) -> union_effects eff (union_eff_exps [c; m])
     | E_comment _ | E_comment_struc _ -> no_effect
-- 
cgit v1.2.3