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.

2 files changed, 27 insertions, 27 deletions

diff --git a/mips_new_tc/mips_extras_embed.lem b/mips_new_tc/mips_extras_embed.lem
index 82f208f6..bda70274 100644
--- a/mips_new_tc/mips_extras_embed.lem
+++ b/mips_new_tc/mips_extras_embed.lem
@@ -4,10 +4,10 @@ open import Sail_impl_base
 open import Sail_values
 open import Prompt
 
-val MEMr             : forall 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'b
-val MEMr_reserve     : forall 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'b
-val MEMr_tag         : forall 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'b
-val MEMr_tag_reserve : forall 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'b
+val MEMr             : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'b 'e
+val MEMr_reserve     : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'b 'e
+val MEMr_tag         : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'b 'e
+val MEMr_tag_reserve : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'b 'e
 
 let MEMr (addr,size)             = read_mem false Read_plain addr size
 let MEMr_reserve (addr,size)     = read_mem false Read_reserve addr size
@@ -16,10 +16,10 @@ let MEMr_tag (addr,size)         = read_mem false Read_plain addr size
 let MEMr_tag_reserve (addr,size) = read_mem false Read_reserve addr size
 
 
-val MEMea                 : forall 'a. Bitvector 'a => ('a * integer) -> M unit
-val MEMea_conditional     : forall 'a. Bitvector 'a => ('a * integer) -> M unit
-val MEMea_tag             : forall 'a. Bitvector 'a => ('a * integer) -> M unit
-val MEMea_tag_conditional : forall 'a. Bitvector 'a => ('a * integer) -> M unit
+val MEMea                 : forall 'a 'e. Bitvector 'a => ('a * integer) -> M unit 'e
+val MEMea_conditional     : forall 'a 'e. Bitvector 'a => ('a * integer) -> M unit 'e
+val MEMea_tag             : forall 'a 'e. Bitvector 'a => ('a * integer) -> M unit 'e
+val MEMea_tag_conditional : forall 'a 'e. Bitvector 'a => ('a * integer) -> M unit 'e
 
 let MEMea (addr,size)                 = write_mem_ea Write_plain addr size
 let MEMea_conditional (addr,size)     = write_mem_ea Write_conditional addr size
@@ -28,10 +28,10 @@ let MEMea_tag (addr,size)             = write_mem_ea Write_plain addr size
 let MEMea_tag_conditional (addr,size) = write_mem_ea Write_conditional addr size
 
 
-val MEMval                 : forall 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M unit
-val MEMval_conditional     : forall 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M bool
-val MEMval_tag             : forall 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M unit
-val MEMval_tag_conditional : forall 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M bool
+val MEMval                 : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M unit 'e
+val MEMval_conditional     : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M bool 'e
+val MEMval_tag             : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M unit 'e
+val MEMval_tag_conditional : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M bool 'e
 
 let MEMval (_,_,v)                 = write_mem_val v >>= fun _ -> return ()
 let MEMval_conditional (_,_,v)     = write_mem_val v >>= fun b -> return (if b then true else false)
@@ -39,9 +39,9 @@ let MEMval_tag (_,_,v)             = write_mem_val v >>= fun _ -> return ()
 let MEMval_tag_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then true else false)
 
 (* TODO *)
-val TAGw : (vector bitU * vector bitU) -> M unit
+val TAGw : forall 'e. (vector bitU * vector bitU) -> M unit 'e
 let TAGw (addr, tag) = failwith "TAGw not implemented"
 
-val MEM_sync  : unit -> M unit
+val MEM_sync  : forall 'e. unit -> M unit 'e
 
 let MEM_sync () = barrier Barrier_Isync
diff --git a/mips_new_tc/mips_extras_embed_sequential.lem b/mips_new_tc/mips_extras_embed_sequential.lem
index c32f297e..b50052dc 100644
--- a/mips_new_tc/mips_extras_embed_sequential.lem
+++ b/mips_new_tc/mips_extras_embed_sequential.lem
@@ -5,10 +5,10 @@ open import Sail_values
 open import Sail_operators_mwords
 open import State
 
-val MEMr             : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs 'b
-val MEMr_reserve     : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs 'b
-val MEMr_tag         : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs (bool * 'b)
-val MEMr_tag_reserve : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs (bool * 'b)
+val MEMr             : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs 'b 'e
+val MEMr_reserve     : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs 'b 'e
+val MEMr_tag         : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs (bool * 'b) 'e
+val MEMr_tag_reserve : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs (bool * 'b) 'e
 
 let MEMr (addr,size)             = read_mem false Read_plain addr size
 let MEMr_reserve (addr,size)     = read_mem false Read_reserve addr size
@@ -24,10 +24,10 @@ let MEMr_tag_reserve (addr,size) =
   return (bitU_to_bool t, v)
 
 
-val MEMea                 : forall 'regs 'a. Bitvector 'a => ('a * integer) -> M 'regs unit
-val MEMea_conditional     : forall 'regs 'a. Bitvector 'a => ('a * integer) -> M 'regs unit
-val MEMea_tag             : forall 'regs 'a. Bitvector 'a => ('a * integer) -> M 'regs unit
-val MEMea_tag_conditional : forall 'regs 'a. Bitvector 'a => ('a * integer) -> M 'regs unit
+val MEMea                 : forall 'regs 'a 'e. Bitvector 'a => ('a * integer) -> M 'regs unit 'e
+val MEMea_conditional     : forall 'regs 'a 'e. Bitvector 'a => ('a * integer) -> M 'regs unit 'e
+val MEMea_tag             : forall 'regs 'a 'e. Bitvector 'a => ('a * integer) -> M 'regs unit 'e
+val MEMea_tag_conditional : forall 'regs 'a 'e. Bitvector 'a => ('a * integer) -> M 'regs unit 'e
 
 let MEMea (addr,size)                 = write_mem_ea Write_plain addr size
 let MEMea_conditional (addr,size)     = write_mem_ea Write_conditional addr size
@@ -36,16 +36,16 @@ let MEMea_tag (addr,size)             = write_mem_ea Write_plain addr size
 let MEMea_tag_conditional (addr,size) = write_mem_ea Write_conditional addr size
 
 
-val MEMval                 : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M 'regs unit
-val MEMval_conditional     : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M 'regs bool
-val MEMval_tag             : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer * bool * 'b) -> M 'regs unit
-val MEMval_tag_conditional : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer * bool * 'b) -> M 'regs bool
+val MEMval                 : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M 'regs unit 'e
+val MEMval_conditional     : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M 'regs bool 'e
+val MEMval_tag             : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * bool * 'b) -> M 'regs unit 'e
+val MEMval_tag_conditional : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * bool * 'b) -> M 'regs bool 'e
 
 let MEMval (_,size,v)                   = write_mem_val v >>= fun _ -> return ()
 let MEMval_conditional (_,size,v)       = write_mem_val v >>= fun b -> return (if b then true else false)
 let MEMval_tag (_,size,t,v)             = write_mem_val v >>= fun _ -> write_tag (bool_to_bitU t) >>= fun _ -> return ()
 let MEMval_tag_conditional (_,size,t,v) = write_mem_val v >>= fun b -> write_tag (bool_to_bitU t) >>= fun _ -> return (if b then true else false)
 
-val MEM_sync  : forall 'regs. unit -> M 'regs unit
+val MEM_sync  : forall 'regs 'e. unit -> M 'regs unit 'e
 
 let MEM_sync () = barrier Barrier_MIPS_SYNC