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.

1 files changed, 13 insertions, 14 deletions

diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 421219da..368f7505 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -905,36 +905,35 @@ end
 
 (* the address_lifted types should go away here and be replaced by address *)
 type with_aux 'o = 'o * maybe ((unit -> (string * string)) * ((list (reg_name * register_value)) -> list event))
-type outcome_r 'a 'r =
+type outcome 'a 'e =
   (* Request to read memory, value is location to read, integer is size to read,
      followed by registers that were used in computing that size *)
-  | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> with_aux (outcome_r 'a 'r))
+  | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> with_aux (outcome 'a 'e))
   (* Tell the system a write is imminent, at address lifted, of size nat *)
-  | Write_ea of (write_kind * address_lifted * nat) * (with_aux (outcome_r 'a 'r))
+  | Write_ea of (write_kind * address_lifted * nat) * (with_aux (outcome 'a 'e))
   (* Request the result of store-exclusive *)
-  | Excl_res of (bool -> with_aux (outcome_r 'a 'r))
+  | Excl_res of (bool -> with_aux (outcome 'a 'e))
   (* Request to write memory at last signalled address. Memory value should be 8
      times the size given in ea signal *)
-  | Write_memv of memory_value * (bool -> with_aux (outcome_r 'a 'r))
+  | Write_memv of memory_value * (bool -> with_aux (outcome 'a 'e))
   (* Request a memory barrier *)
-  | Barrier of barrier_kind * with_aux (outcome_r 'a 'r)
+  | Barrier of barrier_kind * with_aux (outcome 'a 'e)
   (* Tell the system to dynamically recalculate dependency footprint *)
-  | Footprint of with_aux (outcome_r 'a 'r)
+  | Footprint of with_aux (outcome 'a 'e)
   (* Request to read register, will track dependency when mode.track_values *)
-  | Read_reg of reg_name * (register_value -> with_aux (outcome_r 'a 'r))
+  | Read_reg of reg_name * (register_value -> with_aux (outcome 'a 'e))
   (* Request to write register *)
-  | Write_reg of (reg_name * register_value) * with_aux (outcome_r 'a 'r)
+  | Write_reg of (reg_name * register_value) * with_aux (outcome 'a 'e)
   | Escape of maybe string
   (*Result of a failed assert with possible error message to report*)
   | Fail of maybe string
-  (* Early return with value of type 'r *)
-  | Return of 'r
-  | Internal of (maybe string * maybe (unit -> string)) * with_aux (outcome_r 'a 'r)
+  (* Exception of type 'e *)
+  | Exception of 'e
+  | Internal of (maybe string * maybe (unit -> string)) * with_aux (outcome 'a 'e)
   | Done of 'a
   | Error of string
 
-type outcome 'a = outcome_r 'a unit
-type outcome_s 'a = with_aux (outcome 'a)
+type outcome_s 'a 'e = with_aux (outcome 'a 'e)
 (* first string : output of instruction_stack_to_string
    second string: output of local_variables_to_string *)