From 1bb5fcf93261f2de51909ff51bf229d21e4b13a6 Mon Sep 17 00:00:00 2001
From: Jon French
Date: Thu, 14 Jun 2018 16:37:31 +0100
Subject: rename all lem support files to sail2_foo to avoid conflict with
 sail1 in rmem

---
 src/gen_lib/state_monad.lem | 280 --------------------------------------------
 1 file changed, 280 deletions(-)
 delete mode 100644 src/gen_lib/state_monad.lem

(limited to 'src/gen_lib/state_monad.lem')

diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem
deleted file mode 100644
index 89021890..00000000
--- a/src/gen_lib/state_monad.lem
+++ /dev/null
@@ -1,280 +0,0 @@
-open import Pervasives_extra
-open import Sail_instr_kinds
-open import Sail_values
-
-(* 'a is result type *)
-
-type memstate = map integer memory_byte
-type tagstate = map integer bitU
-(* type regstate = map string (vector bitU) *)
-
-type sequential_state 'regs =
-  <| regstate : 'regs;
-     memstate : memstate;
-     tagstate : tagstate;
-     write_ea : maybe (write_kind * integer * integer);
-     last_exclusive_operation_was_load : bool;
-     (* Random bool generator for use as an undefined bit oracle *)
-     next_bool : nat -> (bool * nat);
-     seed : nat |>
-
-val init_state : forall 'regs. 'regs -> (nat -> (bool* nat)) -> nat -> sequential_state 'regs
-let init_state regs o s =
-  <| regstate = regs;
-     memstate = Map.empty;
-     tagstate = Map.empty;
-     write_ea = Nothing;
-     last_exclusive_operation_was_load = false;
-     next_bool = o;
-     seed = s |>
-
-type ex 'e =
-  | Failure of string
-  | Throw of 'e
-
-type result 'a 'e =
-  | Value of 'a
-  | Ex of (ex 'e)
-
-(* State, nondeterminism and exception monad with result value type 'a
-   and exception type 'e. *)
-type monadS 'regs 'a 'e = sequential_state 'regs -> set (result 'a 'e * sequential_state 'regs)
-
-val returnS : forall 'regs 'a 'e. 'a -> monadS 'regs 'a 'e
-let returnS a s = {(Value a,s)}
-
-val bindS : forall 'regs 'a 'b 'e. monadS 'regs 'a 'e -> ('a -> monadS 'regs 'b 'e) -> monadS 'regs 'b 'e
-let bindS m f (s : sequential_state 'regs) =
-  Set.bigunion (Set.map (function
-                | (Value a, s') -> f a s'
-                | (Ex e, s') -> {(Ex e, s')}
-                end) (m s))
-
-val seqS: forall 'regs 'b 'e. monadS 'regs unit 'e -> monadS 'regs 'b 'e -> monadS 'regs 'b 'e
-let seqS m n = bindS m (fun (_ : unit) -> n)
-
-let inline (>>$=) = bindS
-let inline (>>$) = seqS
-
-val chooseS : forall 'regs 'a 'e. SetType 'a => set 'a -> monadS 'regs 'a 'e
-let chooseS xs s = Set.map (fun x -> (Value x, s)) xs
-
-val readS : forall 'regs 'a 'e. (sequential_state 'regs -> 'a) -> monadS 'regs 'a 'e
-let readS f = (fun s -> returnS (f s) s)
-
-val updateS : forall 'regs 'e. (sequential_state 'regs -> sequential_state 'regs) -> monadS 'regs unit 'e
-let updateS f = (fun s -> returnS () (f s))
-
-val failS : forall 'regs 'a 'e. string -> monadS 'regs 'a 'e
-let failS msg s = {(Ex (Failure msg), s)}
-
-val undefined_boolS : forall 'regval 'regs 'a 'e. unit -> monadS 'regs bool 'e
-let undefined_boolS () =
-  readS (fun s -> s.next_bool (s.seed)) >>$= (fun (b, seed) ->
-  updateS (fun s -> <| s with seed = seed |>) >>$
-  returnS b)
-
-val exitS : forall 'regs 'e 'a. unit -> monadS 'regs 'a 'e
-let exitS () = failS "exit"
-
-val throwS : forall 'regs 'a 'e. 'e -> monadS 'regs 'a 'e
-let throwS e s = {(Ex (Throw e), s)}
-
-val try_catchS : forall 'regs 'a 'e1 'e2. monadS 'regs 'a 'e1 -> ('e1 -> monadS 'regs 'a 'e2) ->  monadS 'regs 'a 'e2
-let try_catchS m h s =
-  Set.bigunion (Set.map (function
-                | (Value a, s') -> returnS a s'
-                | (Ex (Throw e), s') -> h e s'
-                | (Ex (Failure msg), s') -> {(Ex (Failure msg), s')}
-                end) (m s))
-
-val assert_expS : forall 'regs 'e. bool -> string -> monadS 'regs unit 'e
-let assert_expS exp msg = if exp then returnS () else failS msg
-
-(* For early return, we abuse exceptions by throwing and catching
-   the return value. The exception type is "either 'r 'e", where "Right e"
-   represents a proper exception and "Left r" an early return of value "r". *)
-type monadRS 'regs 'a 'r 'e = monadS 'regs 'a (either 'r 'e)
-
-val early_returnS : forall 'regs 'a 'r 'e. 'r -> monadRS 'regs 'a 'r 'e
-let early_returnS r = throwS (Left r)
-
-val catch_early_returnS : forall 'regs 'a 'e. monadRS 'regs 'a 'a 'e -> monadS 'regs 'a 'e
-let catch_early_returnS m =
-  try_catchS m
-    (function
-      | Left a -> returnS a
-      | Right e -> throwS e
-     end)
-
-(* Lift to monad with early return by wrapping exceptions *)
-val liftRS : forall 'a 'r 'regs 'e. monadS 'regs 'a 'e -> monadRS 'regs 'a 'r 'e
-let liftRS m = try_catchS m (fun e -> throwS (Right e))
-
-(* Catch exceptions in the presence of early returns *)
-val try_catchRS : forall 'regs 'a 'r 'e1 'e2. monadRS 'regs 'a 'r 'e1 -> ('e1 -> monadRS 'regs 'a 'r 'e2) ->  monadRS 'regs 'a 'r 'e2
-let try_catchRS m h =
-  try_catchS m
-    (function
-      | Left r -> throwS (Left r)
-      | Right e -> h e
-     end)
-
-val maybe_failS : forall 'regs 'a 'e. string -> maybe 'a -> monadS 'regs 'a 'e
-let maybe_failS msg = function
-  | Just a  -> returnS a
-  | Nothing -> failS msg
-end
-
-val read_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> monadS 'regs bitU 'e
-let read_tagS addr =
-  maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
-  readS (fun s -> fromMaybe B0 (Map.lookup addr s.tagstate)))
-
-(* Read bytes from memory and return in little endian order *)
-val read_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => read_kind -> 'a -> nat -> monadS 'regs (list memory_byte) 'e
-let read_mem_bytesS read_kind addr sz =
-  maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
-  let sz = integerFromNat sz in
-  let addrs = index_list addr (addr+sz-1) 1 in
-  let read_byte s addr = Map.lookup addr s.memstate in
-  readS (fun s -> just_list (List.map (read_byte s) addrs)) >>$= (function
-    | Just mem_val ->
-       updateS (fun s ->
-         if read_is_exclusive read_kind
-         then <| s with last_exclusive_operation_was_load = true |>
-         else s) >>$
-       returnS mem_val
-    | Nothing -> failS "read_memS"
-  end))
-
-val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs 'b 'e
-let read_memS rk a sz =
-  read_mem_bytesS rk a (nat_of_int sz) >>$= (fun bytes ->
-  maybe_failS "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes)))
-
-val excl_resultS : forall 'regs 'e. unit -> monadS 'regs bool 'e
-let excl_resultS () =
-  readS (fun s -> s.last_exclusive_operation_was_load) >>$= (fun excl_load ->
-  updateS (fun s -> <| s with last_exclusive_operation_was_load = false |>) >>$
-  chooseS (if excl_load then {false; true} else {false}))
-
-val write_mem_eaS : forall 'regs 'e 'a. Bitvector 'a => write_kind -> 'a -> nat -> monadS 'regs unit 'e
-let write_mem_eaS write_kind addr sz =
-  maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
-  let sz = integerFromNat sz in
-  updateS (fun s -> <| s with write_ea = Just (write_kind, addr, sz) |>))
-
-(* Write little-endian list of bytes to previously announced address *)
-val write_mem_bytesS : forall 'regs 'e. list memory_byte -> monadS 'regs bool 'e
-let write_mem_bytesS v =
-  readS (fun s -> s.write_ea) >>$= (function
-      | Nothing -> failS "write ea has not been announced yet"
-      | Just (_, addr, sz) ->
-         let addrs = index_list addr (addr+sz-1) 1 in
-         (*let v = external_mem_value (bits_of v) in*)
-         let a_v = List.zip addrs v in
-         let write_byte mem (addr, v) = Map.insert addr v mem in
-         updateS (fun s ->
-           <| s with memstate = List.foldl write_byte s.memstate a_v |>) >>$
-         returnS true
-    end)
-
-val write_mem_valS : forall 'regs 'e 'a. Bitvector 'a => 'a -> monadS 'regs bool 'e
-let write_mem_valS v = match mem_bytes_of_bits v with
-  | Just v -> write_mem_bytesS v
-  | Nothing -> failS "write_mem_val"
-end
-
-val write_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> bitU -> monadS 'regs bool 'e
-let write_tagS addr t =
-   maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
-   updateS (fun s -> <| s with tagstate = Map.insert addr t s.tagstate |>) >>$
-   returnS true)
-
-val read_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> monadS 'regs 'a 'e
-let read_regS reg = readS (fun s -> reg.read_from s.regstate)
-
-(* TODO
-let read_reg_range reg i j state =
-  let v = slice (get_reg state (name_of_reg reg)) i j in
-  [(Value (vec_to_bvec v),state)]
-let read_reg_bit reg i state =
-  let v = access (get_reg state (name_of_reg reg)) i in
-  [(Value v,state)]
-let read_reg_field reg regfield =
-  let (i,j) = register_field_indices reg regfield in
-  read_reg_range reg i j
-let read_reg_bitfield reg regfield =
-  let (i,_) = register_field_indices reg regfield in
-  read_reg_bit reg i *)
-
-val read_regvalS : forall 'regs 'rv 'e.
-  register_accessors 'regs 'rv -> string -> monadS 'regs 'rv 'e
-let read_regvalS (read, _) reg =
-  readS (fun s -> read reg s.regstate) >>$= (function
-      | Just v ->  returnS v
-      | Nothing -> failS ("read_regvalS " ^ reg)
-    end)
-
-val write_regvalS : forall 'regs 'rv 'e.
-  register_accessors 'regs 'rv -> string -> 'rv -> monadS 'regs unit 'e
-let write_regvalS (_, write) reg v =
-  readS (fun s -> write reg v s.regstate) >>$= (function
-      | Just rs' -> updateS (fun s -> <| s with regstate = rs' |>)
-      | Nothing ->  failS ("write_regvalS " ^ reg)
-    end)
-
-val write_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> 'a -> monadS 'regs unit 'e
-let write_regS reg v =
-  updateS (fun s -> <| s with regstate = reg.write_to v s.regstate |>)
-
-(* TODO
-val update_reg : forall 'regs 'rv 'a 'b 'e. register_ref 'regs 'rv 'a -> ('a -> 'b -> 'a) -> 'b -> monadS 'regs unit 'e
-let update_reg reg f v state =
-  let current_value = get_reg state reg in
-  let new_value = f current_value v in
-  [(Value (), set_reg state reg new_value)]
-
-let write_reg_field reg regfield = update_reg reg regfield.set_field
-
-val update_reg_range : forall 'regs 'rv 'a 'b. Bitvector 'a, Bitvector 'b => register_ref 'regs 'rv 'a -> integer -> integer -> 'a -> 'b -> 'a
-let update_reg_range reg i j reg_val new_val = set_bits (reg.is_inc) reg_val i j (bits_of new_val)
-let write_reg_range reg i j = update_reg reg (update_reg_range reg i j)
-
-let update_reg_pos reg i reg_val x = update_list reg.is_inc reg_val i x
-let write_reg_pos reg i = update_reg reg (update_reg_pos reg i)
-
-let update_reg_bit reg i reg_val bit = set_bit (reg.is_inc) reg_val i (to_bitU bit)
-let write_reg_bit reg i = update_reg reg (update_reg_bit reg i)
-
-let update_reg_field_range regfield i j reg_val new_val =
-  let current_field_value = regfield.get_field reg_val in
-  let new_field_value = set_bits (regfield.field_is_inc) current_field_value i j (bits_of new_val) in
-  regfield.set_field reg_val new_field_value
-let write_reg_field_range reg regfield i j = update_reg reg (update_reg_field_range regfield i j)
-
-let update_reg_field_pos regfield i reg_val x =
-  let current_field_value = regfield.get_field reg_val in
-  let new_field_value = update_list regfield.field_is_inc current_field_value i x in
-  regfield.set_field reg_val new_field_value
-let write_reg_field_pos reg regfield i = update_reg reg (update_reg_field_pos regfield i)
-
-let update_reg_field_bit regfield i reg_val bit =
-  let current_field_value = regfield.get_field reg_val in
-  let new_field_value = set_bit (regfield.field_is_inc) current_field_value i (to_bitU bit) in
-  regfield.set_field reg_val new_field_value
-let write_reg_field_bit reg regfield i = update_reg reg (update_reg_field_bit regfield i)*)
-
-(* TODO Add Show typeclass for value and exception type *)
-val show_result : forall 'a 'e. result 'a 'e -> string
-let show_result = function
-  | Value _ -> "Value ()"
-  | Ex (Failure msg) -> "Failure " ^ msg
-  | Ex (Throw _) -> "Throw"
-end
-
-val prerr_results : forall 'a 'e 's. SetType 's => set (result 'a 'e * 's) -> unit
-let prerr_results rs =
-  let _ = Set.map (fun (r, _) -> let _ = prerr_endline (show_result r) in ()) rs in
-  ()
-- 
cgit v1.2.3