diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/prompt_monad.lem | 2 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.lem | 12 | ||||
| -rw-r--r-- | src/gen_lib/state.lem | 24 | ||||
| -rw-r--r-- | src/state.ml | 2 |
4 files changed, 22 insertions, 18 deletions
diff --git a/src/gen_lib/prompt_monad.lem b/src/gen_lib/prompt_monad.lem index ff5e3726..38f79868 100644 --- a/src/gen_lib/prompt_monad.lem +++ b/src/gen_lib/prompt_monad.lem @@ -125,7 +125,7 @@ let write_mem_val v = match bytes_of_bits v with | Just v -> let k successful = (return successful) in Write_memv (List.reverse v) k - | Nothing -> fail "write_mem_val" + | Nothing -> Fail "write_mem_val" end val read_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> monad 'rv 'a 'e diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 33caac37..b981bb91 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -379,11 +379,13 @@ end (* just_list takes a list of maybes and returns Just xs if all elements have a value, and Nothing if one of the elements is Nothing. *) val just_list : forall 'a. list (maybe 'a) -> maybe (list 'a) -let rec just_list [] = Just [] -and just_list (x :: xs) = - match (x, just_list xs) with - | (Just x, Just xs) -> Just (x :: xs) - | (_, _) -> Nothing +let rec just_list l = match l with + | [] -> Just [] + | (x :: xs) -> + match (x, just_list xs) with + | (Just x, Just xs) -> Just (x :: xs) + | (_, _) -> Nothing + end end declare {isabelle} termination_argument just_list = automatic 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 diff --git a/src/state.ml b/src/state.ml index 67eda5b8..5873c472 100644 --- a/src/state.ml +++ b/src/state.ml @@ -238,7 +238,7 @@ let register_refs_lem prefix_recordtype mwords registers = separate hardline setters ^^ hardline ^^ string " Nothing" ^^ hardline ^^ hardline ^^ string "let register_accessors = (get_regval, set_regval)" ^^ hardline ^^ hardline ^^ - string "let liftS = liftState register_accessors" ^^ hardline + string "let liftS s = liftState register_accessors s" ^^ hardline in separate hardline [generic_convs; refs; getters_setters] |