Merge branch 'sail2' of github.com:rems-project/sail into sail2

1 files changed, 13 insertions, 11 deletions

diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 4675428e..fba8d9b7 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -9,17 +9,19 @@ open import {isabelle} `State_monad_extras`
 (* State monad wrapper around prompt monad *)
 
 val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e
-let rec liftState _ (Done a)          = returnS a
-and liftState ra (Read_mem rk a sz k) = bindS (read_memS rk a sz)     (fun v -> liftState ra (k v))
-and liftState ra (Write_memv descr k) = bindS (write_mem_valS descr)  (fun v -> liftState ra (k v))
-and liftState ra (Read_reg descr k)   = bindS (read_regvalS ra descr) (fun v -> liftState ra (k v))
-and liftState ra (Excl_res k)         = bindS (excl_resultS ())       (fun v -> liftState ra (k v))
-and liftState ra (Write_ea wk a sz k) = seqS (write_mem_eaS wk a sz)  (liftState ra k)
-and liftState ra (Write_reg r v k)    = seqS (write_regvalS ra r v)   (liftState ra k)
-and liftState ra (Barrier _ k)        = liftState ra k
-and liftState _  (Fail descr)         = failS descr
-and liftState _  (Error descr)        = failS descr
-and liftState _  (Exception e)        = throwS e
+let rec liftState ra s = match s with
+  | (Done a)             -> returnS a
+  | (Read_mem rk a sz k) -> bindS (read_memS rk a sz)     (fun v -> liftState ra (k v))
+  | (Write_memv descr k) -> bindS (write_mem_valS descr)  (fun v -> liftState ra (k v))
+  | (Read_reg descr k)   -> bindS (read_regvalS ra descr) (fun v -> liftState ra (k v))
+  | (Excl_res k)         -> bindS (excl_resultS ())       (fun v -> liftState ra (k v))
+  | (Write_ea wk a sz k) -> seqS (write_mem_eaS wk a sz)  (liftState ra k)
+  | (Write_reg r v k)    -> seqS (write_regvalS ra r v)   (liftState ra k)
+  | (Barrier _ k)        -> liftState ra k
+  | (Fail descr)         -> failS descr
+  | (Error descr)        -> failS descr
+  | (Exception e)        -> throwS e
+end
 
 
 (* TODO