rename all lem support files to sail2_foo to avoid conflict with sail1 in rmem

1 files changed, 0 insertions, 115 deletions

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
deleted file mode 100644
index 830f2350..00000000
--- a/src/gen_lib/prompt.lem
+++ /dev/null
@@ -1,115 +0,0 @@
-open import Pervasives_extra
-(*open import Sail_impl_base*)
-open import Sail_values
-open import Prompt_monad
-open import {isabelle} `Prompt_monad_lemmas`
-
-val (>>=) : forall 'rv 'a 'b 'e. monad 'rv 'a 'e -> ('a -> monad 'rv 'b 'e) -> monad 'rv 'b 'e
-declare isabelle target_rep function (>>=) = infix `\<bind>`
-let inline ~{isabelle} (>>=) = bind
-
-val (>>) : forall 'rv 'b 'e. monad 'rv unit 'e -> monad 'rv 'b 'e -> monad 'rv 'b 'e
-declare isabelle target_rep function (>>) = infix `\<then>`
-let inline ~{isabelle} (>>) m n = m >>= fun (_ : unit) -> n
-
-val iter_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e
-let rec iter_aux i f xs = match xs with
-  | x :: xs -> f i x >> iter_aux (i + 1) f xs
-  | [] -> return ()
-  end
-
-declare {isabelle} termination_argument iter_aux = automatic
-
-val iteri : forall 'rv 'a 'e. (integer -> 'a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e
-let iteri f xs = iter_aux 0 f xs
-
-val iter : forall 'rv 'a 'e. ('a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e
-let iter f xs = iteri (fun _ x -> f x) xs
-
-val foreachM : forall 'a 'rv 'vars 'e.
-  list 'a -> 'vars -> ('a -> 'vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
-let rec foreachM l vars body =
-match l with
-| [] -> return vars
-| (x :: xs) ->
-  body x vars >>= fun vars ->
-  foreachM xs vars body
-end
-
-declare {isabelle} termination_argument foreachM = automatic
-
-val and_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e
-let and_boolM l r = l >>= (fun l -> if l then r else return false)
-
-val or_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e
-let or_boolM l r = l >>= (fun l -> if l then return true else r)
-
-val bool_of_bitU_fail : forall 'rv 'e. bitU -> monad 'rv bool 'e
-let bool_of_bitU_fail = function
-  | B0 -> return false
-  | B1 -> return true
-  | BU -> Fail "bool_of_bitU"
-end
-
-val bool_of_bitU_oracle : forall 'rv 'e. bitU -> monad 'rv bool 'e
-let bool_of_bitU_oracle = function
-  | B0 -> return false
-  | B1 -> return true
-  | BU -> undefined_bool ()
-end
-
-val bools_of_bits_oracle : forall 'rv 'e. list bitU -> monad 'rv (list bool) 'e
-let bools_of_bits_oracle bits =
-  foreachM bits []
-    (fun b bools ->
-      bool_of_bitU_oracle b >>= (fun b ->
-      return (bools ++ [b])))
-
-val of_bits_oracle : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monad 'rv 'a 'e
-let of_bits_oracle bits =
-  bools_of_bits_oracle bits >>= (fun bs ->
-  return (of_bools bs))
-
-val of_bits_fail : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monad 'rv 'a 'e
-let of_bits_fail bits = maybe_fail "of_bits" (of_bits bits)
-
-val mword_oracle : forall 'rv 'a 'e. Size 'a => unit -> monad 'rv (mword 'a) 'e
-let mword_oracle () =
-  bools_of_bits_oracle (repeat [BU] (integerFromNat size)) >>= (fun bs ->
-  return (wordFromBitlist bs))
-
-val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
-                ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
-let rec whileM vars cond body =
-  cond vars >>= fun cond_val ->
-  if cond_val then
-    body vars >>= fun vars -> whileM vars cond body
-  else return vars
-
-val untilM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
-                ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
-let rec untilM vars cond body =
-  body vars >>= fun vars ->
-  cond vars >>= fun cond_val ->
-  if cond_val then return vars else untilM vars cond body
-
-(*let write_two_regs r1 r2 vec =
-  let is_inc =
-    let is_inc_r1 = is_inc_of_reg r1 in
-    let is_inc_r2 = is_inc_of_reg r2 in
-    let () = ensure (is_inc_r1 = is_inc_r2)
-                    "write_two_regs called with vectors of different direction" in
-    is_inc_r1 in
-
-  let (size_r1 : integer) = size_of_reg r1 in
-  let (start_vec : integer) = get_start vec in
-  let size_vec = length vec in
-  let r1_v =
-    if is_inc
-    then slice vec start_vec (size_r1 - start_vec - 1)
-    else slice vec start_vec (start_vec - size_r1 - 1) in
-  let r2_v =
-    if is_inc
-    then slice vec (size_r1 - start_vec) (size_vec - start_vec)
-    else slice vec (start_vec - size_r1) (start_vec - size_vec) in
-  write_reg r1 r1_v >> write_reg r2 r2_v*)