Source file sail2_prompt.ml

(*Generated by Lem from sail2_prompt.lem.*)
open Lem_pervasives_extra
(*open import Sail_impl_base*)
open Sail2_values
open Sail2_prompt_monad

(*val >>= : forall 'rv 'a 'b 'e. monad 'rv 'a 'e -> ('a -> monad 'rv 'b 'e) -> monad 'rv 'b 'e*)

(*val >>$= : forall 'e 'a 'b. either 'e 'a -> ('a -> either 'e 'b) -> either 'e 'b*)

(*val >> : forall 'rv 'b 'e. monad 'rv unit 'e -> monad 'rv 'b 'e -> monad 'rv 'b 'e*)

(*val >>$ : forall 'e 'a. either 'e unit -> either 'e 'a -> either 'e 'a*)

(*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:('rv,(unit),'e)monad=  ((match xs with
  | x :: xs -> bind (f i x) (fun (_ : unit) -> iter_aux ( Nat_big_num.add i( (Nat_big_num.of_int 1))) f xs)
  | [] -> return ()
  ))

(*val iteri : forall 'rv 'a 'e. (integer -> 'a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e*)
let iteri f xs:('rv,(unit),'e)monad=  (iter_aux( (Nat_big_num.of_int 0)) f xs)

(*val iter : forall 'rv 'a 'e. ('a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e*)
let iter f xs:('rv,(unit),'e)monad=  (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:('rv,'vars,'e)monad=
 ((match l with
| [] -> return vars
| (x :: xs) -> bind
  (body x vars) (fun vars ->
  foreachM xs vars body)
))

(*val foreachE : forall 'a 'vars 'e.
  list 'a -> 'vars -> ('a -> 'vars -> either 'e 'vars) -> either 'e 'vars*)
let rec foreachE l vars body:('e,'vars)Either.either=
 ((match l with
| [] -> Either.Right vars
| (x :: xs) -> either_bind
  (body x vars) (fun vars ->
  foreachE xs vars body)
))

(*val genlistM : forall 'a 'rv 'e. (nat -> monad 'rv 'a 'e) -> nat -> monad 'rv (list 'a) 'e*)
let genlistM f n:('rv,('a list),'e)monad=
   (let indices = (genlist (fun n -> n) n) in
  foreachM indices [] (fun n xs -> ( bind(f n) (fun x -> return ( List.rev_append (List.rev 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:('rv,(bool),'e)monad=  (bind 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:('rv,(bool),'e)monad=  (bind 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:bitU ->('rv,(bool),'e)monad=  ((function
  | B0 -> return false
  | B1 -> return true
  | BU -> Fail "bool_of_bitU"
))

(*val bool_of_bitU_nondet : forall 'rv 'e. Register_Value 'rv => bitU -> monad 'rv bool 'e*)
let bool_of_bitU_nondet dict_Sail2_values_Register_Value_rv:bitU ->('rv,(bool),'e)monad=  ((function
  | B0 -> return false
  | B1 -> return true
  | BU -> choose_bool 
  dict_Sail2_values_Register_Value_rv "bool_of_bitU"
))

(*val bools_of_bits_nondet : forall 'rv 'e. Register_Value 'rv => list bitU -> monad 'rv (list bool) 'e*)
let bools_of_bits_nondet dict_Sail2_values_Register_Value_rv bits:('rv,((bool)list),'e)monad=
   (foreachM bits []
    (fun b bools -> bind
      (bool_of_bitU_nondet 
  dict_Sail2_values_Register_Value_rv b) (fun b ->
      return ( List.rev_append (List.rev bools) [b]))))

(*val of_bits_nondet : forall 'rv 'a 'e. Bitvector 'a, Register_Value 'rv => list bitU -> monad 'rv 'a 'e*)
let of_bits_nondet dict_Sail2_values_Bitvector_a dict_Sail2_values_Register_Value_rv bits:('rv,'a,'e)monad=  (bind
  (bools_of_bits_nondet 
  dict_Sail2_values_Register_Value_rv bits) (fun bs ->
  return (dict_Sail2_values_Bitvector_a.of_bools_method bs)))

(*val of_bits_fail : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monad 'rv 'a 'e*)
let of_bits_fail dict_Sail2_values_Bitvector_a bits:('rv,'a,'e)monad=  (maybe_fail "of_bits" (
  dict_Sail2_values_Bitvector_a.of_bits_method bits))

(*val mword_nondet : forall 'rv 'a 'e. Size 'a, Register_Value 'rv => unit -> monad 'rv (mword 'a) 'e*)
let mword_nondet dict_Machine_word_Size_a dict_Sail2_values_Register_Value_rv ():('rv,(Lem.mword),'e)monad=  (bind
  (bools_of_bits_nondet 
  dict_Sail2_values_Register_Value_rv (repeat [BU] (Nat_big_num.of_int  
  dict_Machine_word_Size_a.size_method))) (fun bs ->
  return (Lem.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:('rv,'vars,'e)monad=  (bind
  (cond vars) (fun cond_val ->
  if cond_val then bind
    (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:('rv,'vars,'e)monad=  (bind
  (body vars) (fun vars -> bind
  (cond vars) (fun cond_val ->
  if cond_val then return vars else untilM vars cond body)))

(*val choose_bools : forall 'rv 'e. Register_Value 'rv => string -> nat -> monad 'rv (list bool) 'e*)
let choose_bools dict_Sail2_values_Register_Value_rv descr n:('rv,((bool)list),'e)monad=  (genlistM (fun _ -> choose_bool 
  dict_Sail2_values_Register_Value_rv descr) n)

(*val choose_bitvector : forall 'rv 'a 'e. Bitvector 'a, Register_Value 'rv => string -> nat -> monad 'rv 'a 'e*)
let choose_bitvector dict_Sail2_values_Bitvector_a dict_Sail2_values_Register_Value_rv descr n:('rv,'a,'e)monad=  (bind (choose_bools 
  dict_Sail2_values_Register_Value_rv descr n) (fun v -> return (
  dict_Sail2_values_Bitvector_a.of_bools_method v)))

(*val choose_from_list : forall 'rv 'a 'e. Register_Value 'rv => string -> list 'a -> monad 'rv 'a 'e*)
let choose_from_list dict_Sail2_values_Register_Value_rv descr xs:('rv,'a,'e)monad=  (bind
  (choose_int dict_Sail2_values_Register_Value_rv ("choose_from_list " ^ descr)) (fun idx ->
  (match list_index xs (abs (Nat_big_num.to_int idx) mod List.length xs) with
    | Some x -> return x
    | None -> Fail ("choose_from_list " ^ descr)
  )))

(*val choose_int_in_range : forall 'rv 'e. Register_Value 'rv => string -> integer -> integer -> monad 'rv integer 'e*)
let choose_int_in_range dict_Sail2_values_Register_Value_rv descr i j:('rv,(Nat_big_num.num),'e)monad=  (bind
  (choose_int dict_Sail2_values_Register_Value_rv descr) (fun k ->
  return (Nat_big_num.max i (Nat_big_num.min j k))))

(*val choose_nat : forall 'rv 'e. Register_Value 'rv => string -> monad 'rv integer 'e*)
let choose_nat dict_Sail2_values_Register_Value_rv descr:('rv,(Nat_big_num.num),'e)monad=  (bind (choose_int 
  dict_Sail2_values_Register_Value_rv descr) (fun i -> return (Nat_big_num.max( (Nat_big_num.of_int 0)) i)))

(*val internal_pick : forall 'rv 'a 'e. Register_Value 'rv => list 'a -> monad 'rv 'a 'e*)
let internal_pick dict_Sail2_values_Register_Value_rv xs:('rv,'a,'e)monad=  (choose_from_list 
  dict_Sail2_values_Register_Value_rv "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*)