diff options
Diffstat (limited to 'src/gen_lib/state.lem')
| -rw-r--r-- | src/gen_lib/state.lem | 24 |
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 |