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/ast_util.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src/ast_util.mli')

diff --git a/src/ast_util.mli b/src/ast_util.mli
index a45ca4e9..68955387 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -192,6 +192,7 @@ val string_of_letbind : 'a letbind -> string
 val string_of_index_range : index_range -> string
 
 val id_of_fundef : 'a fundef -> id
+val id_of_type_def : 'a type_def -> id
 
 val id_of_kid : kid -> id
 val kid_of_id : id -> kid
-- 
cgit v1.2.3