Source file sail2_values.ml

(*Generated by Lem from sail2_values.lem.*)
open Lem_pervasives_extra
open Lem_machine_word
(*open import Sail_impl_base*)

type( 'a, 'b) result = | Ok of ('a) | Err of ('b)

type ii = Nat_big_num.num
type nn = Nat_big_num.num

(*val nat_of_int : integer -> nat*)
let nat_of_int i:int=  (if Nat_big_num.less i( (Nat_big_num.of_int 0)) then 0 else abs (Nat_big_num.to_int i))

(*val pow : integer -> integer -> integer*)
let pow m n:Nat_big_num.num=  (Nat_big_num.pow_int m (nat_of_int n))

let pow2 n:Nat_big_num.num=  (pow( (Nat_big_num.of_int 2)) n)

(*val eq : forall 'a. Eq 'a => 'a -> 'a -> bool*)

(*val neq : forall 'a. Eq 'a => 'a -> 'a -> bool*)

(*val print_endline : string -> unit*)
(*let print_endline _:unit=  ()*)

(*val print : string -> unit*)
(*let print _:unit=  ()*)

(*val prerr_endline : string -> unit*)
(*let prerr_endline _:unit=  ()*)

let prerr x:unit=  (prerr_endline x)

(*val print_int : string -> integer -> unit*)
let print_int msg i:unit=  (print_endline (msg ^ (Nat_big_num.to_string i)))

(*val prerr_int : string -> integer -> unit*)
let prerr_int msg i:unit=  (prerr_endline (msg ^ (Nat_big_num.to_string i)))

(*val putchar : integer -> unit*)
(*let putchar _:unit=  ()*)

(*val shr_int : ii -> ii -> ii*)
let rec shr_int x s:Nat_big_num.num=  (if Nat_big_num.greater s( (Nat_big_num.of_int 0)) then shr_int ( Nat_big_num.div x( (Nat_big_num.of_int 2))) ( Nat_big_num.sub s( (Nat_big_num.of_int 1))) else x)

(*val shl_int : integer -> integer -> integer*)
let rec shl_int i shift1:Nat_big_num.num=  (if Nat_big_num.greater shift1( (Nat_big_num.of_int 0)) then Nat_big_num.mul( (Nat_big_num.of_int 2)) (shl_int i ( Nat_big_num.sub shift1( (Nat_big_num.of_int 1)))) else i)

(*val align_int : integer -> integer -> integer*)
let align_int x y:Nat_big_num.num=  (Nat_big_num.mul (Nat_big_num.div x y) y)
let take_list n xs:'a list=  (Lem_list.take (nat_of_int n) xs)
let drop_list n xs:'a list=  (Lem_list.drop (nat_of_int n) xs)

(*val repeat : forall 'a. list 'a -> integer -> list 'a*)
let rec repeat xs n:'a list=
   (if Nat_big_num.less_equal n( (Nat_big_num.of_int 0)) then []
  else  List.rev_append (List.rev xs) (repeat xs (Nat_big_num.sub n( (Nat_big_num.of_int 1)))))

let duplicate_to_list bit length:'a list=  (repeat [bit] length)

let rec replace bs (n : Nat_big_num.num) b':'a list=  ((match bs with
  | [] -> []
  | b :: bs ->
     if Nat_big_num.equal n( (Nat_big_num.of_int 0)) then b' :: bs
              else b :: replace bs ( Nat_big_num.sub n( (Nat_big_num.of_int 1))) b'
  ))

let upper n:'a=  n

(* Modulus operation corresponding to quot below -- result
   has sign of dividend. *)
let tmod_int (a: Nat_big_num.num) (b:Nat_big_num.num) : Nat_big_num.num=
   (let m = (Nat_big_num.modulus (Nat_big_num.abs a) (Nat_big_num.abs b)) in
  if Nat_big_num.less a( (Nat_big_num.of_int 0)) then Nat_big_num.negate m else m)

let hardware_mod:Nat_big_num.num ->Nat_big_num.num ->Nat_big_num.num=  tmod_int

(* There are different possible answers for integer divide regarding
rounding behaviour on negative operands. Positive operands always
round down so derive the one we want (truncation towards zero) from
that *)
let tdiv_int (a:Nat_big_num.num) (b:Nat_big_num.num) : Nat_big_num.num=
   (let q = (Nat_big_num.div (Nat_big_num.abs a) (Nat_big_num.abs b)) in
  if ((Nat_big_num.less a( (Nat_big_num.of_int 0))) = (Nat_big_num.less b( (Nat_big_num.of_int 0)))) then
    q  (* same sign -- result positive *)
  else
    Nat_big_num.negate q) (* different sign -- result negative *)

let hardware_quot:Nat_big_num.num ->Nat_big_num.num ->Nat_big_num.num=  tdiv_int

let max_64u:Nat_big_num.num=  (Nat_big_num.sub (Nat_big_num.pow_int( (Nat_big_num.of_int 2)) 64)( (Nat_big_num.of_int 1)))
let max_64:Nat_big_num.num=   (Nat_big_num.sub (Nat_big_num.pow_int( (Nat_big_num.of_int 2)) 63)( (Nat_big_num.of_int 1)))
let min_64:Nat_big_num.num=   (Nat_big_num.sub( (Nat_big_num.of_int 0)) (Nat_big_num.pow_int( (Nat_big_num.of_int 2)) 63))
let max_32u:Nat_big_num.num=  (( (Nat_big_num.of_string "4294967295") : Nat_big_num.num))
let max_32:Nat_big_num.num=   (( (Nat_big_num.of_string "2147483647") : Nat_big_num.num))
let min_32:Nat_big_num.num=   (( Nat_big_num.sub( (Nat_big_num.of_int 0))( (Nat_big_num.of_string "2147483648")) : Nat_big_num.num))
let max_8:Nat_big_num.num=    (( (Nat_big_num.of_int 127) : Nat_big_num.num))
let min_8:Nat_big_num.num=    (( Nat_big_num.sub( (Nat_big_num.of_int 0))( (Nat_big_num.of_int 128)) : Nat_big_num.num))
let max_5:Nat_big_num.num=    (( (Nat_big_num.of_int 31) : Nat_big_num.num))
let min_5:Nat_big_num.num=    (( Nat_big_num.sub( (Nat_big_num.of_int 0))( (Nat_big_num.of_int 32)) : Nat_big_num.num))

(* just_list takes a list of maybes and returns Just xs if all elements have
   a value, and Nothing if one of the elements is Nothing. *)
(*val just_list : forall 'a. list (maybe 'a) -> maybe (list 'a)*)
let rec just_list l:('a list)option=  ((match l with
  | [] -> Some []
  | (x :: xs) ->
    (match (x, just_list xs) with
      | (Some x, Some xs) -> Some (x :: xs)
      | (_, _) -> None
    )
  ))

(*val maybe_failwith : forall 'a. maybe 'a -> 'a*)
let maybe_failwith:'a option ->'a=  ((function
  | Some a -> a
  | None -> failwith "maybe_failwith"
))

(*** Bits *)
type bitU = B0 | B1 | BU

let showBitU:bitU ->string=  ((function
  | B0 -> "O"
  | B1 -> "I"
  | BU -> "U"
))

let bitU_char:bitU ->char=  ((function
  | B0 -> '0'
  | B1 -> '1'
  | BU -> '?'
))

let instance_Show_Show_Sail2_values_bitU_dict:(bitU)show_class= ({

  show_method = showBitU})

(*val compare_bitU : bitU -> bitU -> ordering*)
let compare_bitU l r:int=  ((match (l, r) with
  | (BU, BU) -> 0
  | (B0, B0) -> 0
  | (B1, B1) -> 0
  | (BU, _)  -> (-1)
  | (_, BU)  -> 1
  | (B0, _)  -> (-1)
  | (_, _)   -> 1
))

let instance_Basic_classes_Ord_Sail2_values_bitU_dict:(bitU)ord_class= ({

  compare_method = compare_bitU;

  isLess_method = (fun  l r-> Lem.orderingEqual(compare_bitU l r) (-1));

  isLessEqual_method = (fun l r-> not (Lem.orderingEqual (compare_bitU l r) 1));

  isGreater_method = (fun  l r-> Lem.orderingEqual(compare_bitU l r) 1);

  isGreaterEqual_method = (fun l r-> not (Lem.orderingEqual (compare_bitU l r) (-1)))})

type 'a bitU_class={
  to_bitU_method : 'a -> bitU;
  of_bitU_method : bitU -> 'a
}

let instance_Sail2_values_BitU_Sail2_values_bitU_dict:(bitU)bitU_class= ({

  to_bitU_method = (fun b->b);

  of_bitU_method = (fun b->b)})

let bool_of_bitU:bitU ->(bool)option=  ((function
  | B0 -> Some false
  | B1 -> Some true
  | BU -> None
  ))

let bitU_of_bool b:bitU=  (if b then B1 else B0)

(*instance (BitU bool)
  let to_bitU = bitU_of_bool
  let of_bitU = bool_of_bitU
end*)

let cast_bit_bool:bitU ->(bool)option=  bool_of_bitU

let not_bit:bitU ->bitU=  ((function
  | B1 -> B0
  | B0 -> B1
  | BU -> BU
  ))

(*val is_one : integer -> bitU*)
let is_one i:bitU=
   (if Nat_big_num.equal i( (Nat_big_num.of_int 1)) then B1 else B0)

(*val and_bit : bitU -> bitU -> bitU*)
let and_bit x y:bitU=
   ((match (x, y) with
    | (B0, _) -> B0
    | (_, B0) -> B0
    | (B1, B1) -> B1
    | (_, _) -> BU
  ))

(*val or_bit : bitU -> bitU -> bitU*)
let or_bit x y:bitU=
   ((match (x, y) with
    | (B1, _) -> B1
    | (_, B1) -> B1
    | (B0, B0) -> B0
    | (_, _) -> BU
  ))

(*val xor_bit : bitU -> bitU -> bitU*)
let xor_bit x y:bitU=
  ((match (x, y) with
    | (B0, B0) -> B0
    | (B0, B1) -> B1
    | (B1, B0) -> B1
    | (B1, B1) -> B0
    | (_, _) -> BU
  ))

(*val &. : bitU -> bitU -> bitU*)

(*val |. : bitU -> bitU -> bitU*)

(*val +. : bitU -> bitU -> bitU*)


(*** Bool lists ***)

(*val bools_of_nat_aux : integer -> natural -> list bool -> list bool*)
let rec bools_of_nat_aux len x acc:(bool)list=
   (if Nat_big_num.less_equal len( (Nat_big_num.of_int 0)) then acc
  else bools_of_nat_aux ( Nat_big_num.sub len( (Nat_big_num.of_int 1))) ( Nat_big_num.div x( (Nat_big_num.of_int 2))) ((if Nat_big_num.equal (Nat_big_num.modulus x( (Nat_big_num.of_int 2)))( (Nat_big_num.of_int 1)) then true else false) :: acc))
let bools_of_nat len n:(bool)list=  (bools_of_nat_aux len n []) (*List.reverse (bools_of_nat_aux n)*)

(*val nat_of_bools_aux : natural -> list bool -> natural*)
let rec nat_of_bools_aux acc bs:Nat_big_num.num=  ((match bs with
  | [] -> acc
  | true :: bs -> nat_of_bools_aux ( Nat_big_num.add( Nat_big_num.mul( (Nat_big_num.of_int 2)) acc)( (Nat_big_num.of_int 1))) bs
  | false :: bs -> nat_of_bools_aux ( Nat_big_num.mul( (Nat_big_num.of_int 2)) acc) bs
))
let nat_of_bools bs:Nat_big_num.num=  (nat_of_bools_aux( (Nat_big_num.of_int 0)) bs)

(*val unsigned_of_bools : list bool -> integer*)
let unsigned_of_bools bs:Nat_big_num.num=  ((nat_of_bools bs))

(*val signed_of_bools : list bool -> integer*)
let signed_of_bools bs:Nat_big_num.num=
   ((match bs with
    | true :: _  -> Nat_big_num.sub( (Nat_big_num.of_int 0)) ( Nat_big_num.add( (Nat_big_num.of_int 1)) (unsigned_of_bools (Lem_list.map not bs)))
    | false :: _ -> unsigned_of_bools bs
    | [] -> (Nat_big_num.of_int 0) (* Treat empty list as all zeros *)
  ))

(*val int_of_bools : bool -> list bool -> integer*)
let int_of_bools sign bs:Nat_big_num.num=  (if sign then signed_of_bools bs else unsigned_of_bools bs)

(*val pad_list : forall 'a. 'a -> list 'a -> integer -> list 'a*)
let rec pad_list x xs n:'a list=
   (if Nat_big_num.less_equal n( (Nat_big_num.of_int 0)) then xs else pad_list x (x :: xs) ( Nat_big_num.sub n( (Nat_big_num.of_int 1))))

let ext_list pad len xs:'a list=
   (let longer = (Nat_big_num.sub len (Nat_big_num.of_int (List.length xs))) in
  if Nat_big_num.less longer( (Nat_big_num.of_int 0)) then drop (nat_of_int (Nat_big_num.abs (longer))) xs
  else pad_list pad xs longer)

let extz_bools len bs:(bool)list=  (ext_list false len bs)
let exts_bools len bs:(bool)list=
   ((match bs with
    | true :: _ -> ext_list true len bs
    | _ -> ext_list false len bs
  ))

let rec add_one_bool_ignore_overflow_aux bits:(bool)list=  ((match bits with
  | [] -> []
  | false :: bits -> true :: bits
  | true :: bits -> false :: add_one_bool_ignore_overflow_aux bits
))

let add_one_bool_ignore_overflow bits:(bool)list=
   (List.rev (add_one_bool_ignore_overflow_aux (List.rev bits)))

(*let bool_list_of_int n =
  let bs_abs = false :: bools_of_nat (naturalFromInteger (abs n)) in
  if n >= (0 : integer) then bs_abs
  else add_one_bool_ignore_overflow (List.map not bs_abs)
let bools_of_int len n = exts_bools len (bool_list_of_int n)*)
let bools_of_int len n:(bool)list=
   (let bs_abs = (bools_of_nat len (Nat_big_num.abs (Nat_big_num.abs n))) in
  if Nat_big_num.greater_equal n ( (Nat_big_num.of_int 0) : Nat_big_num.num) then bs_abs
  else add_one_bool_ignore_overflow (Lem_list.map not bs_abs))

(*** Bit lists ***)

(*val has_undefined_bits : list bitU -> bool*)
let has_undefined_bits bs:bool=  (List.exists ((function BU -> true | _ -> false )) bs)

let bits_of_nat len n:(bitU)list=  (Lem_list.map bitU_of_bool (bools_of_nat len n))

let nat_of_bits bits:(Nat_big_num.num)option=
   ((match (just_list (Lem_list.map bool_of_bitU bits)) with
    | Some bs -> Some (nat_of_bools bs)
    | None -> None
  ))

let not_bits:(bitU)list ->(bitU)list=  (Lem_list.map not_bit)

(*val binop_list : forall 'a. ('a -> 'a -> 'a) -> list 'a -> list 'a -> list 'a*)
let binop_list op xs ys:'a list=
   (List.fold_right (fun (x, y) acc -> op x y :: acc) (list_combine xs ys) [])

let unsigned_of_bits bits:(Nat_big_num.num)option=
   ((match (just_list (Lem_list.map bool_of_bitU bits)) with
    | Some bs -> Some (unsigned_of_bools bs)
    | None -> None
  ))

let signed_of_bits bits:(Nat_big_num.num)option=
   ((match (just_list (Lem_list.map bool_of_bitU bits)) with
    | Some bs -> Some (signed_of_bools bs)
    | None -> None
  ))

(*val int_of_bits : bool -> list bitU -> maybe integer*)
let int_of_bits sign bs:(Nat_big_num.num)option=  (if sign then signed_of_bits bs else unsigned_of_bits bs)

let extz_bits len bits:(bitU)list=  (ext_list B0 len bits)
let exts_bits len bits:(bitU)list=
   ((match bits with
  | BU :: _ -> ext_list BU len bits
  | B1 :: _ -> ext_list B1 len bits
  | _ -> ext_list B0 len bits
  ))

let rec add_one_bit_ignore_overflow_aux bits:(bitU)list=  ((match bits with
  | [] -> []
  | B0 :: bits -> B1 :: bits
  | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits
  | BU :: bits -> BU :: Lem_list.map (fun _ -> BU) bits
))

let add_one_bit_ignore_overflow bits:(bitU)list=
   (List.rev (add_one_bit_ignore_overflow_aux (List.rev bits)))

(*let bit_list_of_int n = List.map bitU_of_bool (bool_list_of_int n)
let bits_of_int len n = exts_bits len (bit_list_of_int n)*)
let bits_of_int len n:(bitU)list=  (Lem_list.map bitU_of_bool (bools_of_int len n))

(*val arith_op_bits :
  (integer -> integer -> integer) -> bool -> list bitU -> list bitU -> list bitU*)
let arith_op_bits op sign l r:(bitU)list=
   ((match (int_of_bits sign l, int_of_bits sign r) with
    | (Some li, Some ri) -> bits_of_int (Nat_big_num.of_int (List.length l)) (op li ri)
    | (_, _) -> repeat [BU] (Nat_big_num.of_int (List.length l))
  ))

let char_of_nibble:bitU*bitU*bitU*bitU ->(char)option=  ((function
  | (B0, B0, B0, B0) -> Some '0'
  | (B0, B0, B0, B1) -> Some '1'
  | (B0, B0, B1, B0) -> Some '2'
  | (B0, B0, B1, B1) -> Some '3'
  | (B0, B1, B0, B0) -> Some '4'
  | (B0, B1, B0, B1) -> Some '5'
  | (B0, B1, B1, B0) -> Some '6'
  | (B0, B1, B1, B1) -> Some '7'
  | (B1, B0, B0, B0) -> Some '8'
  | (B1, B0, B0, B1) -> Some '9'
  | (B1, B0, B1, B0) -> Some 'A'
  | (B1, B0, B1, B1) -> Some 'B'
  | (B1, B1, B0, B0) -> Some 'C'
  | (B1, B1, B0, B1) -> Some 'D'
  | (B1, B1, B1, B0) -> Some 'E'
  | (B1, B1, B1, B1) -> Some 'F'
  | _ -> None
  ))

let nibble_of_char:char ->(bitU*bitU*bitU*bitU)option=  ((function
  | '0' -> Some (B0, B0, B0, B0)
  | '1' -> Some (B0, B0, B0, B1)
  | '2' -> Some (B0, B0, B1, B0)
  | '3' -> Some (B0, B0, B1, B1)
  | '4' -> Some (B0, B1, B0, B0)
  | '5' -> Some (B0, B1, B0, B1)
  | '6' -> Some (B0, B1, B1, B0)
  | '7' -> Some (B0, B1, B1, B1)
  | '8' -> Some (B1, B0, B0, B0)
  | '9' -> Some (B1, B0, B0, B1)
  | 'A' -> Some (B1, B0, B1, B0)
  | 'B' -> Some (B1, B0, B1, B1)
  | 'C' -> Some (B1, B1, B0, B0)
  | 'D' -> Some (B1, B1, B0, B1)
  | 'E' -> Some (B1, B1, B1, B0)
  | 'F' -> Some (B1, B1, B1, B1)
  | _ -> None
  ))

let rec hexstring_of_bits bs:((char)list)option=  ((match bs with
  | b1 :: b2 :: b3 :: b4 :: bs ->
     let n = (char_of_nibble (b1, b2, b3, b4)) in
     let s = (hexstring_of_bits bs) in
     (match (n, s) with
     | (Some n, Some s) -> Some (n :: s)
     | _ -> None
     )
  | [] -> Some []
  | _ -> None
  ))

let show_bitlist_prefix c bs:string=
   ((match hexstring_of_bits bs with
  | Some s -> Xstring.implode (c :: ('x' :: s))
  | None -> Xstring.implode (c :: ('b' :: map bitU_char bs))
  ))

let show_bitlist bs:string=  (show_bitlist_prefix '0' bs)

(*val hex_char : natural -> char*)

let hex_char n:char= (
 if(Nat_big_num.equal n ( (Nat_big_num.of_int 0))) then '0' else
   (
   if(Nat_big_num.equal n ( (Nat_big_num.of_int 1))) then '1' else
     (
     if(Nat_big_num.equal n ( (Nat_big_num.of_int 2))) then '2' else
       (
       if(Nat_big_num.equal n ( (Nat_big_num.of_int 3))) then '3' else
         (
         if(Nat_big_num.equal n ( (Nat_big_num.of_int 4))) then '4' else
           (
           if(Nat_big_num.equal n ( (Nat_big_num.of_int 5))) then '5' else
             (
             if(Nat_big_num.equal n ( (Nat_big_num.of_int 6))) then '6' else
               (
               if(Nat_big_num.equal n ( (Nat_big_num.of_int 7))) then 
               '7' else
                 (
                 if(Nat_big_num.equal n ( (Nat_big_num.of_int 8))) then 
                 '8' else
                   (
                   if(Nat_big_num.equal n ( (Nat_big_num.of_int 9))) then 
                   '9' else
                     (
                     if(Nat_big_num.equal n ( (Nat_big_num.of_int 10))) then
                       'A' else
                       (
                       if(Nat_big_num.equal n ( (Nat_big_num.of_int 11))) then
                         'B' else
                         (
                         if(Nat_big_num.equal n ( (Nat_big_num.of_int 12))) then
                           'C' else
                           (
                           if(Nat_big_num.equal n ( (Nat_big_num.of_int 13))) then
                             'D' else
                             (
                             if(Nat_big_num.equal n
                                  ( (Nat_big_num.of_int 14))) then 'E' else
                               (
                               if(Nat_big_num.equal n
                                    ( (Nat_big_num.of_int 15))) then 
                               'F' else
                                 (failwith
                                    "hex_char: not a hexadecimal digit")))))))))))))))))

(*val hex_str_aux : natural -> list char -> list char*)

let rec hex_str_aux n acc:(char)list=
   (if Nat_big_num.equal n( (Nat_big_num.of_int 0)) then acc else
  hex_str_aux ( Nat_big_num.div n( (Nat_big_num.of_int 16))) (hex_char ( Nat_big_num.modulus n( (Nat_big_num.of_int 16))) :: acc))

(*val hex_str : integer -> string*)

let hex_str i:string=
   (if Nat_big_num.less i( (Nat_big_num.of_int 0)) then failwith "hex_str: negative" else
  if Nat_big_num.equal i( (Nat_big_num.of_int 0)) then "0x0" else
  "0x" ^ Xstring.implode (hex_str_aux (Nat_big_num.abs (Nat_big_num.abs i)) []))

(*val subrange_list_inc : forall 'a. list 'a -> integer -> integer -> list 'a*)
let subrange_list_inc xs i j:'a list=
   (let (toJ,_suffix) = (Lem_list.split_at (nat_of_int ( Nat_big_num.add j( (Nat_big_num.of_int 1)))) xs) in
  let (_prefix,fromItoJ) = (Lem_list.split_at (nat_of_int i) toJ) in
  fromItoJ)

(*val subrange_list_dec : forall 'a. list 'a -> integer -> integer -> list 'a*)
let subrange_list_dec xs i j:'a list=
   (let top = (Nat_big_num.sub (Nat_big_num.of_int (List.length xs))( (Nat_big_num.of_int 1))) in
  subrange_list_inc xs ( Nat_big_num.sub top i) ( Nat_big_num.sub top j))

(*val subrange_list : forall 'a. bool -> list 'a -> integer -> integer -> list 'a*)
let subrange_list is_inc xs i j:'a list=  (if is_inc then subrange_list_inc xs i j else subrange_list_dec xs i j)

(*val update_subrange_list_inc : forall 'a. list 'a -> integer -> integer -> list 'a -> list 'a*)
let update_subrange_list_inc xs i j xs':'a list=
   (let (toJ,suffix) = (Lem_list.split_at (nat_of_int ( Nat_big_num.add j( (Nat_big_num.of_int 1)))) xs) in
  let (prefix,_fromItoJ) = (Lem_list.split_at (nat_of_int i) toJ) in 
  List.rev_append (List.rev (List.rev_append (List.rev prefix) xs')) suffix)

(*val update_subrange_list_dec : forall 'a. list 'a -> integer -> integer -> list 'a -> list 'a*)
let update_subrange_list_dec xs i j xs':'a list=
   (let top = (Nat_big_num.sub (Nat_big_num.of_int (List.length xs))( (Nat_big_num.of_int 1))) in
  update_subrange_list_inc xs ( Nat_big_num.sub top i) ( Nat_big_num.sub top j) xs')

(*val update_subrange_list : forall 'a. bool -> list 'a -> integer -> integer -> list 'a -> list 'a*)
let update_subrange_list is_inc xs i j xs':'a list=
   (if is_inc then update_subrange_list_inc xs i j xs' else update_subrange_list_dec xs i j xs')

(*val access_list_inc : forall 'a. list 'a -> integer -> 'a*)
let access_list_inc xs n:'a=  (List.nth xs (nat_of_int n))

(*val access_list_dec : forall 'a. list 'a -> integer -> 'a*)
let access_list_dec xs n:'a=
   (let top = (Nat_big_num.sub (Nat_big_num.of_int (List.length xs))( (Nat_big_num.of_int 1))) in
  access_list_inc xs ( Nat_big_num.sub top n))

(*val access_list : forall 'a. bool -> list 'a -> integer -> 'a*)
let access_list is_inc xs n:'a=
   (if is_inc then access_list_inc xs n else access_list_dec xs n)

(*val update_list_inc : forall 'a. list 'a -> integer -> 'a -> list 'a*)
let update_list_inc xs n x:'a list=  (Lem_list.list_update xs (nat_of_int n) x)

(*val update_list_dec : forall 'a. list 'a -> integer -> 'a -> list 'a*)
let update_list_dec xs n x:'a list=
   (let top = (Nat_big_num.sub (Nat_big_num.of_int (List.length xs))( (Nat_big_num.of_int 1))) in
  update_list_inc xs ( Nat_big_num.sub top n) x)

(*val update_list : forall 'a. bool -> list 'a -> integer -> 'a -> list 'a*)
let update_list is_inc xs n x:'a list=
   (if is_inc then update_list_inc xs n x else update_list_dec xs n x)

let extract_only_bit:(bitU)list ->bitU=  ((function
  | [] ->  BU
  | [e] -> e
  | _ ->   BU
))

(*** Machine words *)

(*val length_mword : forall 'a. mword 'a -> integer*)

(*val slice_mword_dec : forall 'a 'b. mword 'a -> integer -> integer -> mword 'b*)
let slice_mword_dec w i j:Lem.mword=  (Lem.word_extract (nat_of_int i) (nat_of_int j) w)

(*val slice_mword_inc : forall 'a 'b. mword 'a -> integer -> integer -> mword 'b*)
let slice_mword_inc w i j:Lem.mword=
   (let top = (Nat_big_num.sub (Nat_big_num.of_int (Lem.word_length w))( (Nat_big_num.of_int 1))) in
  slice_mword_dec w ( Nat_big_num.sub top i) ( Nat_big_num.sub top j))

(*val slice_mword : forall 'a 'b. bool -> mword 'a -> integer -> integer -> mword 'b*)
let slice_mword is_inc w i j:Lem.mword=  (if is_inc then slice_mword_inc w i j else slice_mword_dec w i j)

(*val update_slice_mword_dec : forall 'a 'b. mword 'a -> integer -> integer -> mword 'b -> mword 'a*)
let update_slice_mword_dec w i j w':Lem.mword=  (Lem.word_update w (nat_of_int i) (nat_of_int j) w')

(*val update_slice_mword_inc : forall 'a 'b. mword 'a -> integer -> integer -> mword 'b -> mword 'a*)
let update_slice_mword_inc w i j w':Lem.mword=
   (let top = (Nat_big_num.sub (Nat_big_num.of_int (Lem.word_length w))( (Nat_big_num.of_int 1))) in
  update_slice_mword_dec w ( Nat_big_num.sub top i) ( Nat_big_num.sub top j) w')

(*val update_slice_mword : forall 'a 'b. bool -> mword 'a -> integer -> integer -> mword 'b -> mword 'a*)
let update_slice_mword is_inc w i j w':Lem.mword=
   (if is_inc then update_slice_mword_inc w i j w' else update_slice_mword_dec w i j w')

(*val access_mword_dec : forall 'a. mword 'a -> integer -> bitU*)
let access_mword_dec w n:bitU=  (bitU_of_bool (Lem.word_getBit w (nat_of_int n)))

(*val access_mword_inc : forall 'a. mword 'a -> integer -> bitU*)
let access_mword_inc w n:bitU=
   (let top = (Nat_big_num.sub (Nat_big_num.of_int (Lem.word_length w))( (Nat_big_num.of_int 1))) in
  access_mword_dec w ( Nat_big_num.sub top n))

(*val access_mword : forall 'a. bool -> mword 'a -> integer -> bitU*)
let access_mword is_inc w n:bitU=
   (if is_inc then access_mword_inc w n else access_mword_dec w n)

(*val update_mword_bool_dec : forall 'a. mword 'a -> integer -> bool -> mword 'a*)
let update_mword_bool_dec w n b:Lem.mword=  (Lem.word_setBit w (nat_of_int n) b)
let update_mword_dec w n b:(Lem.mword)option=  (Lem.option_map (update_mword_bool_dec w n) (bool_of_bitU b))

(*val update_mword_bool_inc : forall 'a. mword 'a -> integer -> bool -> mword 'a*)
let update_mword_bool_inc w n b:Lem.mword=
   (let top = (Nat_big_num.sub (Nat_big_num.of_int (Lem.word_length w))( (Nat_big_num.of_int 1))) in
  update_mword_bool_dec w ( Nat_big_num.sub top n) b)
let update_mword_inc w n b:(Lem.mword)option=  (Lem.option_map (update_mword_bool_inc w n) (bool_of_bitU b))

(*val int_of_mword : forall 'a. bool -> mword 'a -> integer*)
let int_of_mword sign w:Nat_big_num.num=
   (if sign then Lem.signedIntegerFromWord w else Lem.naturalFromWord w)

(* Translating between a type level number (itself 'n) and an integer *)

let size_itself_int dict_Machine_word_Size_a x:Nat_big_num.num=  (Nat_big_num.of_int (size_itself 
  dict_Machine_word_Size_a x))

(* NB: the corresponding sail type is forall 'n. atom('n) -> itself('n),
   the actual integer is ignored. *)

(*val make_the_value : forall 'n. integer -> itself 'n*)
let make_the_value _:unit=  ()

(*** Bitvectors *)

type 'a bitvector_class={
  bits_of_method : 'a -> bitU list;
  (* We allow of_bits to be partial, as not all bitvector representations
     support undefined bits *)
  of_bits_method : bitU list ->  'a option;
  of_bools_method : bool list -> 'a;
  length_method : 'a -> Nat_big_num.num;
  (* of_int: the first parameter specifies the desired length of the bitvector *)
  of_int_method : Nat_big_num.num -> Nat_big_num.num -> 'a;
  (* Conversion to integers is undefined if any bit is undefined *)
  unsigned_method : 'a ->  Nat_big_num.num option;
  signed_method : 'a ->  Nat_big_num.num option;
  (* Lifting of integer operations to bitvectors:  The boolean flag indicates
     whether to treat the bitvectors as signed (true) or not (false). *)
  arith_op_bv_method : (Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num) -> bool -> 'a -> 'a -> 'a
}

(*val of_bits_failwith : forall 'a. Bitvector 'a => list bitU -> 'a*)
let of_bits_failwith dict_Sail2_values_Bitvector_a bits:'a=  (maybe_failwith (
  dict_Sail2_values_Bitvector_a.of_bits_method bits))

let int_of_bv dict_Sail2_values_Bitvector_a sign:'a ->(Nat_big_num.num)option=  (if sign then  
  dict_Sail2_values_Bitvector_a.signed_method else  dict_Sail2_values_Bitvector_a.unsigned_method)

let instance_Sail2_values_Bitvector_list_dict dict_Sail2_values_BitU_a:('a list)bitvector_class= ({

  bits_of_method = (fun v->Lem_list.map  
  dict_Sail2_values_BitU_a.to_bitU_method v);

  of_bits_method = (fun v->Some (Lem_list.map  
  dict_Sail2_values_BitU_a.of_bitU_method v));

  of_bools_method = (fun v->Lem_list.map  
  dict_Sail2_values_BitU_a.of_bitU_method (Lem_list.map bitU_of_bool v));

  length_method = (fun xs->Nat_big_num.of_int (List.length xs));

  of_int_method = (fun len n->Lem_list.map  
  dict_Sail2_values_BitU_a.of_bitU_method (bits_of_int len n));

  unsigned_method = (fun v->unsigned_of_bits (Lem_list.map  
  dict_Sail2_values_BitU_a.to_bitU_method v));

  signed_method = (fun v->signed_of_bits (Lem_list.map  
  dict_Sail2_values_BitU_a.to_bitU_method v));

  arith_op_bv_method = (fun op sign l r->Lem_list.map  
  dict_Sail2_values_BitU_a.of_bitU_method (arith_op_bits op sign (Lem_list.map  
  dict_Sail2_values_BitU_a.to_bitU_method l) (Lem_list.map  dict_Sail2_values_BitU_a.to_bitU_method r)))})

let instance_Sail2_values_Bitvector_Machine_word_mword_dict dict_Machine_word_Size_a:(Lem.mword)bitvector_class= ({

  bits_of_method = (fun v->Lem_list.map bitU_of_bool (Lem.bitlistFromWord v));

  of_bits_method = (fun v->Lem.option_map Lem.wordFromBitlist (just_list (Lem_list.map bool_of_bitU v)));

  of_bools_method = (fun v->Lem.wordFromBitlist v);

  length_method = (fun v->Nat_big_num.of_int (Lem.word_length v));

  of_int_method = (fun _ n -> wordFromInteger 
  dict_Machine_word_Size_a n);

  unsigned_method = (fun v->Some (Lem.naturalFromWord v));

  signed_method = (fun v->Some (Lem.signedIntegerFromWord v));

  arith_op_bv_method = (fun op sign l r->wordFromInteger 
  dict_Machine_word_Size_a (op (int_of_mword sign l) (int_of_mword sign r)))})

let access_bv_inc dict_Sail2_values_Bitvector_a v n:bitU=  (access_list true  (
  dict_Sail2_values_Bitvector_a.bits_of_method v) n)
let access_bv_dec dict_Sail2_values_Bitvector_a v n:bitU=  (access_list false (
  dict_Sail2_values_Bitvector_a.bits_of_method v) n)

let update_bv_inc dict_Sail2_values_Bitvector_a v n b:(bitU)list=  (update_list true  (
  dict_Sail2_values_Bitvector_a.bits_of_method v) n b)
let update_bv_dec dict_Sail2_values_Bitvector_a v n b:(bitU)list=  (update_list false (
  dict_Sail2_values_Bitvector_a.bits_of_method v) n b)

let subrange_bv_inc dict_Sail2_values_Bitvector_a v i j:(bitU)list=  (subrange_list true  (
  dict_Sail2_values_Bitvector_a.bits_of_method v) i j)
let subrange_bv_dec dict_Sail2_values_Bitvector_a v i j:(bitU)list=  (subrange_list false (
  dict_Sail2_values_Bitvector_a.bits_of_method v) i j)

let update_subrange_bv_inc dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b v i j v':(bitU)list=  (update_subrange_list true  (
  dict_Sail2_values_Bitvector_b.bits_of_method v) i j (dict_Sail2_values_Bitvector_a.bits_of_method v'))
let update_subrange_bv_dec dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b v i j v':(bitU)list=  (update_subrange_list false (
  dict_Sail2_values_Bitvector_b.bits_of_method v) i j (dict_Sail2_values_Bitvector_a.bits_of_method v'))

(*val extz_bv : forall 'a. Bitvector 'a => integer -> 'a -> list bitU*)
let extz_bv dict_Sail2_values_Bitvector_a n v:(bitU)list=  (extz_bits n (
  dict_Sail2_values_Bitvector_a.bits_of_method v))

(*val exts_bv : forall 'a. Bitvector 'a => integer -> 'a -> list bitU*)
let exts_bv dict_Sail2_values_Bitvector_a n v:(bitU)list=  (exts_bits n (
  dict_Sail2_values_Bitvector_a.bits_of_method v))

(*val nat_of_bv : forall 'a. Bitvector 'a => 'a -> maybe nat*)
let nat_of_bv dict_Sail2_values_Bitvector_a v:(int)option=  (Lem.option_map nat_of_int (
  dict_Sail2_values_Bitvector_a.unsigned_method v))

(*val string_of_bv : forall 'a. Bitvector 'a => 'a -> string*)
let string_of_bv dict_Sail2_values_Bitvector_a v:string=  (show_bitlist (
  dict_Sail2_values_Bitvector_a.bits_of_method v))

(*val string_of_bv_subrange : forall 'a. Bitvector 'a => 'a -> integer -> integer -> string*)
let string_of_bv_subrange dict_Sail2_values_Bitvector_a v i j:string=  (show_bitlist (subrange_bv_dec 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (dict_Sail2_values_Bitvector_a.bits_of_method v) i j))

(*val print_bits : forall 'a. Bitvector 'a => string -> 'a -> unit*)
let print_bits dict_Sail2_values_Bitvector_a str v:unit=  (print_endline (str ^ string_of_bv 
  dict_Sail2_values_Bitvector_a v))

(*val prerr_bits : forall 'a. Bitvector 'a => string -> 'a -> unit*)
let prerr_bits dict_Sail2_values_Bitvector_a str v:unit=  (prerr_endline (str ^ string_of_bv 
  dict_Sail2_values_Bitvector_a v))

(*val dec_str : integer -> string*)
let dec_str bv:string=  (Nat_big_num.to_string bv)

(*val concat_str : string -> string -> string*)
let concat_str str1 str2:string=  (str1 ^ str2)

(*val int_of_bit : bitU -> integer*)
let int_of_bit b:Nat_big_num.num=
   ((match b with
  | B0 -> (Nat_big_num.of_int 0)
  | B1 -> (Nat_big_num.of_int 1)
  | _ -> failwith "int_of_bit saw unknown"
  ))

(*val count_leading_zero_bits : list bitU -> integer*)
let rec count_leading_zero_bits v:Nat_big_num.num=
   ((match v with
  | B0 :: v' -> Nat_big_num.add (count_leading_zero_bits v')( (Nat_big_num.of_int 1))
  | _ -> (Nat_big_num.of_int 0)
  ))

(*val count_leading_zeros_bv : forall 'a. Bitvector 'a => 'a -> integer*)
let count_leading_zeros_bv dict_Sail2_values_Bitvector_a v:Nat_big_num.num=  (count_leading_zero_bits (
  dict_Sail2_values_Bitvector_a.bits_of_method v))

(*val decimal_string_of_bv : forall 'a. Bitvector 'a => 'a -> string*)
let decimal_string_of_bv dict_Sail2_values_Bitvector_a bv:string=
   (let place_values =
    (Lem_list.mapi
      (fun i b -> Nat_big_num.mul (int_of_bit b) ( Nat_big_num.pow_int( (Nat_big_num.of_int 2)) i))
      (List.rev (dict_Sail2_values_Bitvector_a.bits_of_method bv)))
  in
  let sum = (List.fold_left Nat_big_num.add( (Nat_big_num.of_int 0)) place_values) in
  Nat_big_num.to_string sum)

(*val align_bits : forall 'a. Bitvector 'a => 'a -> integer -> 'a*)
let align_bits dict_Sail2_values_Bitvector_a x y:'a=
   (let len = (dict_Sail2_values_Bitvector_a.length_method x) in
  (match  dict_Sail2_values_Bitvector_a.unsigned_method x with
  | Some x -> dict_Sail2_values_Bitvector_a.of_int_method len (align_int x y)
  | None -> failwith "align_bits: failed to convert bitvector"
  ))

(*** Bytes and addresses *)

type memory_byte = bitU list

(*val byte_chunks : forall 'a. list 'a -> maybe (list (list 'a))*)
let rec byte_chunks bs:(('a list)list)option=  ((match bs with
  | [] -> Some []
  | a::b::c::d::e::f::g::h::rest ->
     Lem.option_bind (byte_chunks rest) (fun rest -> Some ([a;b;c;d;e;f;g;h] :: rest))
  | _ -> None
))

(*val bytes_of_bits : forall 'a. Bitvector 'a => 'a -> maybe (list memory_byte)*)
let bytes_of_bits dict_Sail2_values_Bitvector_a bs:(((bitU)list)list)option=  (byte_chunks (
  dict_Sail2_values_Bitvector_a.bits_of_method bs))

(*val bits_of_bytes : list memory_byte -> list bitU*)
let bits_of_bytes bs:(bitU)list=  (List.concat (Lem_list.map (fun v->Lem_list.map (fun b->b) v) bs))

let mem_bytes_of_bits dict_Sail2_values_Bitvector_a bs:(((bitU)list)list)option=  (Lem.option_map List.rev (bytes_of_bits 
  dict_Sail2_values_Bitvector_a bs))
let bits_of_mem_bytes bs:(bitU)list=  (bits_of_bytes (List.rev bs))

(*val bitv_of_byte_lifteds : list Sail_impl_base.byte_lifted -> list bitU
let bitv_of_byte_lifteds v =
  foldl (fun x (Byte_lifted y) -> x ++ (List.map bitU_of_bit_lifted y)) [] v

val bitv_of_bytes : list Sail_impl_base.byte -> list bitU
let bitv_of_bytes v =
  foldl (fun x (Byte y) -> x ++ (List.map bitU_of_bit y)) [] v

val byte_lifteds_of_bitv : list bitU -> list byte_lifted
let byte_lifteds_of_bitv bits =
  let bits = List.map bit_lifted_of_bitU bits in
  byte_lifteds_of_bit_lifteds bits

val bytes_of_bitv : list bitU -> list byte
let bytes_of_bitv bits =
  let bits = List.map bit_of_bitU bits in
  bytes_of_bits bits

val bit_lifteds_of_bitUs : list bitU -> list bit_lifted
let bit_lifteds_of_bitUs bits = List.map bit_lifted_of_bitU bits

val bit_lifteds_of_bitv : list bitU -> list bit_lifted
let bit_lifteds_of_bitv v = bit_lifteds_of_bitUs v


val address_lifted_of_bitv : list bitU -> address_lifted
let address_lifted_of_bitv v =
  let byte_lifteds = byte_lifteds_of_bitv v in
  let maybe_address_integer =
    match (maybe_all (List.map byte_of_byte_lifted byte_lifteds)) with
    | Just bs -> Just (integer_of_byte_list bs)
    | _ -> Nothing
    end in
  Address_lifted byte_lifteds maybe_address_integer

val bitv_of_address_lifted : address_lifted -> list bitU
let bitv_of_address_lifted (Address_lifted bs _) = bitv_of_byte_lifteds bs

val address_of_bitv : list bitU -> address
let address_of_bitv v =
  let bytes = bytes_of_bitv v in
  address_of_byte_list bytes*)

let rec reverse_endianness_list bits:'a list=
   (if List.length bits <= 8 then bits else 
    List.rev_append (List.rev (reverse_endianness_list (drop_list( (Nat_big_num.of_int 8)) bits))) (take_list( (Nat_big_num.of_int 8)) bits))


(*** Registers *)

(*type register_field = string
type register_field_index = string * (integer * integer) (* name, start and end *)

type register =
  | Register of string * (* name *)
                integer * (* length *)
                integer * (* start index *)
                bool * (* is increasing *)
                  list register_field_index
  | UndefinedRegister of integer (* length *)
  | RegisterPair of register * register*)

type 'rv register_Value_class={
  bool_of_regval_method : 'rv ->  bool option;
  regval_of_bool_method : bool -> 'rv;
  int_of_regval_method : 'rv ->  Nat_big_num.num option;
  regval_of_int_method : Nat_big_num.num -> 'rv;
  real_of_regval_method : 'rv ->  float option;
  regval_of_real_method : float -> 'rv;
  string_of_regval_method : 'rv ->  string option;
  regval_of_string_method : string -> 'rv
}

type( 'regstate, 'regval, 'a) register_ref =
  { name : string;
     (*is_inc : bool;*)
     read_from : 'regstate -> 'a;
     write_to : 'a -> 'regstate -> 'regstate;
     of_regval : 'regval ->  'a option;
     regval_of : 'a -> 'regval }

(* Register operations which do not depend on polymorphic type *)
type( 'regstate, 'regval) register_ops =
  (('regval -> bool) * ('regstate -> 'regval) *
   ('regval -> 'regstate ->  'regstate option))

(*val register_ops_of : forall 'st 'regval 'a.
    register_ref 'st 'regval 'a -> register_ops 'st 'regval*)
let register_ops_of reg:('regval ->bool)*('st ->'regval)*('regval ->'st ->'st option)=
   ((fun x -> Lem.is_some (reg.of_regval x)),
   (fun x -> reg.regval_of (reg.read_from x)),
   (fun x st -> Lem.option_map (fun v -> reg.write_to v st) (reg.of_regval x)))

(* Register accessors: pair of functions for reading and writing register values *)
type( 'regstate, 'regval) register_accessors =
  ((string -> 'regstate ->  'regval option) *
   (string -> 'regval -> 'regstate ->  'regstate option))

(*val mk_accessors : forall 'st 'v.
    (string -> maybe (register_ops 'st 'v)) -> register_accessors 'st 'v*)
let mk_accessors regs:(string ->'st ->'v option)*(string ->'v ->'st ->'st option)=
   ((fun nm st -> Lem.option_map (fun (_, acc, _) -> acc st) (regs nm)),
   (fun nm v st -> Lem.option_bind (regs nm) (fun (_, _, put) -> put v st)))

type( 'regtype, 'a) field_ref =
  { field_name : string;
     field_start : Nat_big_num.num;
     field_is_inc : bool;
     get_field : 'regtype -> 'a;
     set_field : 'regtype -> 'a -> 'regtype }

(*let name_of_reg = function
  | Register name _ _ _ _ -> name
  | UndefinedRegister _ -> failwith "name_of_reg UndefinedRegister"
  | RegisterPair _ _ -> failwith "name_of_reg RegisterPair"
end

let size_of_reg = function
  | Register _ size _ _ _ -> size
  | UndefinedRegister size -> size
  | RegisterPair _ _ -> failwith "size_of_reg RegisterPair"
end

let start_of_reg = function
  | Register _ _ start _ _ -> start
  | UndefinedRegister _ -> failwith "start_of_reg UndefinedRegister"
  | RegisterPair _ _ -> failwith "start_of_reg RegisterPair"
end

let is_inc_of_reg = function
  | Register _ _ _ is_inc _ -> is_inc
  | UndefinedRegister _ -> failwith "is_inc_of_reg UndefinedRegister"
  | RegisterPair _ _ -> failwith "in_inc_of_reg RegisterPair"
end

let dir_of_reg = function
  | Register _ _ _ is_inc _ -> dir_of_bool is_inc
  | UndefinedRegister _ -> failwith "dir_of_reg UndefinedRegister"
  | RegisterPair _ _ -> failwith "dir_of_reg RegisterPair"
end

let size_of_reg_nat reg = natFromInteger (size_of_reg reg)
let start_of_reg_nat reg = natFromInteger (start_of_reg reg)

val register_field_indices_aux : register -> register_field -> maybe (integer * integer)
let rec register_field_indices_aux register rfield =
  match register with
  | Register _ _ _ _ rfields -> List.lookup rfield rfields
  | RegisterPair r1 r2 ->
      let m_indices = register_field_indices_aux r1 rfield in
      if isJust m_indices then m_indices else register_field_indices_aux r2 rfield
  | UndefinedRegister _ -> Nothing
  end

val register_field_indices : register -> register_field -> integer * integer
let register_field_indices register rfield =
  match register_field_indices_aux register rfield with
  | Just indices -> indices
  | Nothing -> failwith "Invalid register/register-field combination"
  end

let register_field_indices_nat reg regfield=
  let (i,j) = register_field_indices reg regfield in
  (natFromInteger i,natFromInteger j)*)

(*let rec external_reg_value reg_name v =
  let (internal_start, external_start, direction) =
    match reg_name with
     | Reg _ start size dir ->
        (start, (if dir = D_increasing then start else (start - (size +1))), dir)
     | Reg_slice _ reg_start dir (slice_start, _) ->
        ((if dir = D_increasing then slice_start else (reg_start - slice_start)),
         slice_start, dir)
     | Reg_field _ reg_start dir _ (slice_start, _) ->
        ((if dir = D_increasing then slice_start else (reg_start - slice_start)),
         slice_start, dir)
     | Reg_f_slice _ reg_start dir _ _ (slice_start, _) ->
        ((if dir = D_increasing then slice_start else (reg_start - slice_start)),
         slice_start, dir)
     end in
  let bits = bit_lifteds_of_bitv v in
  <| rv_bits           = bits;
     rv_dir            = direction;
     rv_start          = external_start;
     rv_start_internal = internal_start |>

val internal_reg_value : register_value -> list bitU
let internal_reg_value v =
  List.map bitU_of_bit_lifted v.rv_bits
         (*(integerFromNat v.rv_start_internal)
         (v.rv_dir = D_increasing)*)


let external_slice (d:direction) (start:nat) ((i,j):(nat*nat)) =
  match d with
  (* This is the case the thread/concurrency model expects, so no change needed *)
  | D_increasing -> (i,j)
  | D_decreasing -> let slice_i = start - i in
                    let slice_j = (i - j) + slice_i in
                    (slice_i,slice_j)
  end *)

(* TODO
let external_reg_whole r =
  Reg (r.name) (natFromInteger r.start) (natFromInteger r.size) (dir_of_bool r.is_inc)

let external_reg_slice r (i,j) =
  let start = natFromInteger r.start in
  let dir = dir_of_bool r.is_inc in
  Reg_slice (r.name) start dir (external_slice dir start (i,j))

let external_reg_field_whole reg rfield =
  let (m,n) = register_field_indices_nat reg rfield in
  let start = start_of_reg_nat reg in
  let dir = dir_of_reg reg in
  Reg_field (name_of_reg reg) start dir rfield (external_slice dir start (m,n))

let external_reg_field_slice reg rfield (i,j) =
  let (m,n) = register_field_indices_nat reg rfield in
  let start = start_of_reg_nat reg in
  let dir = dir_of_reg reg in
  Reg_f_slice (name_of_reg reg) start dir rfield
              (external_slice dir start (m,n))
              (external_slice dir start (i,j))*)

(*val external_mem_value : list bitU -> memory_value
let external_mem_value v =
  byte_lifteds_of_bitv v $> List.reverse

val internal_mem_value : memory_value -> list bitU
let internal_mem_value bytes =
  List.reverse bytes $> bitv_of_byte_lifteds*)


(*val foreach : forall 'a 'vars.
  (list 'a) -> 'vars -> ('a -> 'vars -> 'vars) -> 'vars*)
let rec foreach l vars body:'vars=
   ((match l with
    | [] -> vars
    | (x :: xs) -> foreach xs (body x vars) body
  ))

(*val index_list : integer -> integer -> integer -> list integer*)
let rec index_list from to1 step:(Nat_big_num.num)list=
   (if ( Nat_big_num.greater step( (Nat_big_num.of_int 0)) && Nat_big_num.less_equal from to1) || ( Nat_big_num.less step( (Nat_big_num.of_int 0)) && Nat_big_num.less_equal to1 from) then
    from :: index_list ( Nat_big_num.add from step) to1 step
  else [])

(*val while : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars*)
let rec while0 vars cond body:'vars=
   (if cond vars then while0 (body vars) cond body else vars)

(*val until : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars*)
let rec until vars cond body:'vars=
   (let vars = (body vars) in
  if cond vars then vars else until (body vars) cond body)


(* convert numbers unsafely to naturals *)

type 'a toNatural_class={ toNatural_method : 'a -> Nat_big_num.num }
(* eta-expanded for Isabelle output, otherwise it breaks *)
let instance_Sail2_values_ToNatural_Num_integer_dict:(Nat_big_num.num)toNatural_class= ({

  toNatural_method = (fun n -> Nat_big_num.abs n)})
let instance_Sail2_values_ToNatural_Num_int_dict:(int)toNatural_class= ({

  toNatural_method = (fun n -> Nat_big_num.of_int (abs n))})
let instance_Sail2_values_ToNatural_nat_dict:(int)toNatural_class= ({

  toNatural_method = (fun n -> Nat_big_num.of_int n)})
let instance_Sail2_values_ToNatural_Num_natural_dict:(Nat_big_num.num)toNatural_class= ({

  toNatural_method = (fun n -> n)})

let toNaturalFiveTup dict_Sail2_values_ToNatural_a dict_Sail2_values_ToNatural_b dict_Sail2_values_ToNatural_c dict_Sail2_values_ToNatural_d dict_Sail2_values_ToNatural_e (n1,n2,n3,n4,n5):Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*Nat_big_num.num*Nat_big_num.num=
   (dict_Sail2_values_ToNatural_d.toNatural_method n1, dict_Sail2_values_ToNatural_c.toNatural_method n2, dict_Sail2_values_ToNatural_b.toNatural_method n3, dict_Sail2_values_ToNatural_a.toNatural_method n4, dict_Sail2_values_ToNatural_e.toNatural_method n5)

(* Let the following types be generated by Sail per spec, using either bitlists
   or machine words as bitvector representation *)
(*type regfp =
  | RFull of (string)
  | RSlice of (string * integer * integer)
  | RSliceBit of (string * integer)
  | RField of (string * string)

type niafp =
  | NIAFP_successor
  | NIAFP_concrete_address of vector bitU
  | NIAFP_indirect_address

(* only for MIPS *)
type diafp =
  | DIAFP_none
  | DIAFP_concrete of vector bitU
  | DIAFP_reg of regfp

let regfp_to_reg (reg_info : string -> maybe string -> (nat * nat * direction * (nat * nat))) = function
  | RFull name ->
     let (start,length,direction,_) = reg_info name Nothing in
     Reg name start length direction
  | RSlice (name,i,j) ->
     let i = natFromInteger i in
     let j = natFromInteger j in
     let (start,length,direction,_) = reg_info name Nothing in
     let slice = external_slice direction start (i,j) in
     Reg_slice name start direction slice
  | RSliceBit (name,i) ->
     let i = natFromInteger i in
     let (start,length,direction,_) = reg_info name Nothing in
     let slice = external_slice direction start (i,i) in
     Reg_slice name start direction slice
  | RField (name,field_name) ->
     let (start,length,direction,span) = reg_info name (Just field_name) in
     let slice = external_slice direction start span in
     Reg_field name start direction field_name slice
end

let niafp_to_nia reginfo = function
  | NIAFP_successor -> NIA_successor
  | NIAFP_concrete_address v -> NIA_concrete_address (address_of_bitv v)
  | NIAFP_indirect_address -> NIA_indirect_address
end

let diafp_to_dia reginfo = function
  | DIAFP_none -> DIA_none
  | DIAFP_concrete v -> DIA_concrete_address (address_of_bitv v)
  | DIAFP_reg r -> DIA_register (regfp_to_reg reginfo r)
end
*)