Merge branch 'sail2' into union_barrier

1 files changed, 139 insertions, 0 deletions

diff --git a/src/gen_lib/0.11/sail2_prompt.lem b/src/gen_lib/0.11/sail2_prompt.lem
new file mode 100644
index 00000000..3cde7ade
--- /dev/null
+++ b/src/gen_lib/0.11/sail2_prompt.lem
@@ -0,0 +1,139 @@
+open import Pervasives_extra
+(*open import Sail_impl_base*)
+open import Sail2_values
+open import Sail2_prompt_monad
+open import {isabelle} `Sail2_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 genlistM : forall 'a 'rv 'e. (nat -> monad 'rv 'a 'e) -> nat -> monad 'rv (list 'a) 'e
+let genlistM f n =
+  let indices = genlist (fun n -> n) n in
+  foreachM indices [] (fun n xs -> (f n >>= (fun x -> return (xs ++ [x]))))
+
+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_nondet : forall 'rv 'e. bitU -> monad 'rv bool 'e
+let bool_of_bitU_nondet = function
+  | B0 -> return false
+  | B1 -> return true
+  | BU -> choose_bool "bool_of_bitU"
+end
+
+val bools_of_bits_nondet : forall 'rv 'e. list bitU -> monad 'rv (list bool) 'e
+let bools_of_bits_nondet bits =
+  foreachM bits []
+    (fun b bools ->
+      bool_of_bitU_nondet b >>= (fun b ->
+      return (bools ++ [b])))
+
+val of_bits_nondet : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monad 'rv 'a 'e
+let of_bits_nondet bits =
+  bools_of_bits_nondet 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_nondet : forall 'rv 'a 'e. Size 'a => unit -> monad 'rv (mword 'a) 'e
+let mword_nondet () =
+  bools_of_bits_nondet (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
+
+val choose_bools : forall 'rv 'e. string -> nat -> monad 'rv (list bool) 'e
+let choose_bools descr n = genlistM (fun _ -> choose_bool descr) n
+
+val choose : forall 'rv 'a 'e. string -> list 'a -> monad 'rv 'a 'e
+let choose descr xs =
+  (* Use sufficiently many nondeterministically chosen bits and convert into an
+     index into the list *)
+  choose_bools descr (List.length xs) >>= fun bs ->
+  let idx = (natFromNatural (nat_of_bools bs)) mod List.length xs in
+  match index xs idx with
+    | Just x -> return x
+    | Nothing -> Fail ("choose " ^ descr)
+  end
+
+declare {isabelle} rename function choose = chooseM
+
+val internal_pick : forall 'rv 'a 'e. list 'a -> monad 'rv 'a 'e
+let internal_pick xs = choose "internal_pick" xs
+
+(*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*)