Remove sequential code again

1 files changed, 0 insertions, 126 deletions

diff --git a/mips/mips_extras_sequential.lem b/mips/mips_extras_sequential.lem
deleted file mode 100644
index 8de5aec3..00000000
--- a/mips/mips_extras_sequential.lem
+++ /dev/null
@@ -1,126 +0,0 @@
-open import Pervasives
-open import Pervasives_extra
-open import Sail_instr_kinds
-open import Sail_values
-open import Sail_operators
-open import State_monad
-open import State
-
-val MEMr             : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monadS 'regval 'b 'e
-val MEMr_reserve     : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monadS 'regval 'b 'e
-val MEMr_tag         : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monadS 'regval (bool * 'b) 'e
-val MEMr_tag_reserve : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monadS 'regval (bool * 'b) 'e
-
-let MEMr addr size             = read_memS Read_plain addr size
-let MEMr_reserve addr size     = read_memS Read_reserve addr size
-
-val read_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> monadS 'regval bool 'e
-let read_tag_bool addr =
-  read_tagS addr >>$= fun t ->
-  maybe_failS "read_tag_bool" (bool_of_bitU t)
-
-val write_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> bool -> monadS 'regval unit 'e
-let write_tag_bool addr t = write_tagS addr (bitU_of_bool t) >>$= fun _ -> returnS ()
-
-let MEMr_tag addr size =
-  read_memS Read_plain addr size >>$= fun v ->
-  read_tag_bool addr >>$= fun t ->
-  returnS (t, v)
-
-let MEMr_tag_reserve addr size =
-  read_memS Read_plain addr size >>$= fun v ->
-  read_tag_bool addr >>$= fun t ->
-  returnS (t, v)
-
-
-val MEMea                 : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monadS 'regval unit 'e
-val MEMea_conditional     : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monadS 'regval unit 'e
-val MEMea_tag             : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monadS 'regval unit 'e
-val MEMea_tag_conditional : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monadS 'regval unit 'e
-
-let MEMea addr size                 = write_mem_eaS Write_plain addr (nat_of_int size)
-let MEMea_conditional addr size     = write_mem_eaS Write_conditional addr (nat_of_int size)
-
-let MEMea_tag addr size             = write_mem_eaS Write_plain addr (nat_of_int size)
-let MEMea_tag_conditional addr size = write_mem_eaS Write_conditional addr (nat_of_int size)
-
-
-val MEMval                 : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> 'b -> monadS 'regval unit 'e
-val MEMval_conditional     : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> 'b -> monadS 'regval bool 'e
-val MEMval_tag             : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monadS 'regval unit 'e
-val MEMval_tag_conditional : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monadS 'regval bool 'e
-
-let MEMval _ size v                      = write_mem_valS v >>$= fun _ -> returnS ()
-let MEMval_conditional _ size v          = write_mem_valS v >>$= fun b -> returnS (if b then true else false)
-let MEMval_tag addr size t v             = write_mem_valS v >>$= fun _ -> write_tag_bool addr t >>$= fun _ -> returnS ()
-let MEMval_tag_conditional addr size t v = write_mem_valS v >>$= fun b -> write_tag_bool addr t >>$= fun _ -> returnS (if b then true else false)
-
-val MEM_sync  : forall 'regval 'e. unit -> monadS 'regval unit 'e
-
-let MEM_sync () = returnS ()  (*barrier Barrier_MIPS_SYNC*)
-
-(* Some wrappers copied from aarch64_extras *)
-(* TODO: Harmonise into a common library *)
-
-let get_slice_int_bl len n lo =
-  (* TODO: Is this the intended behaviour? *)
-  let hi = lo + len - 1 in
-  let bs = bools_of_int (hi + 1) n in
-  subrange_list false bs hi lo
-
-val get_slice_int : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a
-let get_slice_int len n lo = of_bools (get_slice_int_bl len n lo)
-
-let write_ram _ size _ addr data =
-  MEMea addr size >>$
-  MEMval addr size data
-
-let read_ram _ size _ addr = MEMr addr size
-
-let inline reg_deref = read_regS
-
-let string_of_bits bs = string_of_bv (bits_of bs)
-let string_of_int = show
-
-let _sign_extend bits len = maybe_failwith (of_bits (exts_bv len bits))
-let _zero_extend bits len = maybe_failwith (of_bits (extz_bv len bits))
-
-let shift_bits_left v n =
-  let r = Maybe.bind (unsigned n) (fun n -> of_bits (shiftl_bv v n)) in
-  maybe_failS "shift_bits_left" r
-let shift_bits_right v n =
-  let r = Maybe.bind (unsigned n) (fun n -> of_bits (shiftr_bv v n)) in
-  maybe_failS "shift_bits_right" r
-let shift_bits_right_arith v n =
-  let r = Maybe.bind (unsigned n) (fun n -> of_bits (arith_shiftr_bv v n)) in
-  maybe_failS "shift_bits_right_arith" r
-
-(* Use constants for undefined values for now *)
-let internal_pick vs = returnS (head vs)
-let undefined_bool = undefined_boolS
-let undefined_string () = returnS ""
-let undefined_unit () = returnS ()
-let undefined_int () = returnS (0:ii)
-val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monadS 'rv (list 'a) 'e
-let undefined_vector len u = returnS (repeat [u] len)
-val undefined_bitvector : forall 'rv 'a 'e. Bitvector 'a => integer -> monadS 'rv 'a 'e
-let undefined_bitvector len = returnS (of_bools (repeat [false] len))
-val undefined_bits : forall 'rv 'a 'e. Bitvector 'a => integer -> monadS 'rv 'a 'e
-let undefined_bits = undefined_bitvector
-let undefined_bit () = returnS B0
-let undefined_real () = returnS (realFromFrac 0 1)
-let undefined_range i j = returnS i
-let undefined_atom i = returnS i
-let undefined_nat () = returnS (0:ii)
-
-let skip () = returnS ()
-
-val elf_entry : unit -> integer
-let elf_entry () = 0
-declare ocaml target_rep function elf_entry = `Elf_loader.elf_entry`
-
-let print_bits msg bs = prerr_endline (msg ^ (string_of_bits bs))
-
-val get_time_ns : unit -> integer
-let get_time_ns () = 0
-declare ocaml target_rep function get_time_ns = `(fun () -> Big_int.of_int (int_of_float (1e9 *. Unix.gettimeofday ())))`