(* Version of sail_values.lem that uses Lem's machine words library *)

open import Pervasives_extra
open import Machine_word
(*open import Sail_impl_base*)


type ii = integer
type nn = natural

val pow : integer -> integer -> integer
let pow m n = m ** (natFromInteger n)

let pow2 n = pow 2 n

let inline lt = (<)
let inline gt = (>)
let inline lteq = (<=)
let inline gteq = (>=)

val eq : forall 'a. Eq 'a => 'a -> 'a -> bool
let inline eq l r = (l = r)

val neq : forall 'a. Eq 'a => 'a -> 'a -> bool
let inline neq l r = (l <> r)

(*let add_int l r = integerAdd l r
let add_signed l r = integerAdd l r
let sub_int l r = integerMinus l r
let mult_int l r = integerMult l r
let div_int l r = integerDiv l r
let div_nat l r = natDiv l r
let power_int_nat l r = integerPow l r
let power_int_int l r = integerPow l (natFromInteger r)
let negate_int i = integerNegate i
let min_int l r = integerMin l r
let max_int l r = integerMax l r

let add_real l r = realAdd l r
let sub_real l r = realMinus l r
let mult_real l r = realMult l r
let div_real l r = realDiv l r
let negate_real r = realNegate r
let abs_real r = realAbs r
let power_real b e = realPowInteger b e*)

let or_bool l r = (l || r)
let and_bool l r = (l && r)
let xor_bool l r = xor l r

let append_list l r = l ++ r
let length_list xs = integerFromNat (List.length xs)
let take_list n xs = List.take (natFromInteger n) xs
let drop_list n xs = List.drop (natFromInteger n) xs

val repeat : forall 'a. list 'a -> integer -> list 'a
let rec repeat xs n =
  if n <= 0 then []
  else xs ++ repeat xs (n-1)
declare {isabelle} termination_argument repeat = automatic

let duplicate_to_list bit length = repeat [bit] length

let rec replace bs (n : integer) b' = match bs with
  | [] -> []
  | b :: bs ->
     if n = 0 then b' :: bs
              else b :: replace bs (n - 1) b'
  end
declare {isabelle} termination_argument replace = automatic

let upper n = n

(* Modulus operation corresponding to quot below -- result
   has sign of dividend. *)
let hardware_mod (a: integer) (b:integer) : integer =
  let m = (abs a) mod (abs b) in
  if a < 0 then ~m else m

(* 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 (trucation towards zero) from
that *)
let hardware_quot (a:integer) (b:integer) : integer =
  let q = (abs a) / (abs b) in
  if ((a<0) = (b<0)) then
    q  (* same sign -- result positive *)
  else
    ~q (* different sign -- result negative *)

let max_64u = (integerPow 2 64) - 1
let max_64  = (integerPow 2 63) - 1
let min_64  = 0 - (integerPow 2 63)
let max_32u = (4294967295 : integer)
let max_32  = (2147483647 : integer)
let min_32  = (0 - 2147483648 : integer)
let max_8   = (127 : integer)
let min_8   = (0 - 128 : integer)
let max_5   = (31 : integer)
let min_5   = (0 - 32 : integer)

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

let showBitU = function
  | B0 -> "O"
  | B1 -> "I"
  | BU -> "U"
end

instance (Show bitU)
  let show = showBitU
end

class (BitU 'a)
  val to_bitU : 'a -> bitU
  val of_bitU : bitU -> 'a
end

instance (BitU bitU)
  let to_bitU b = b
  let of_bitU b = b
end

let bool_of_bitU = function
  | B0 -> false
  | B1 -> true
  | BU -> failwith "bool_of_bitU applied to BU"
  end

let bitU_of_bool b = 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 = bool_of_bitU

(*let bit_lifted_of_bitU = function
  | B0 -> Bitl_zero
  | B1 -> Bitl_one
  | BU -> Bitl_undef
  end

let bitU_of_bit = function
  | Bitc_zero -> B0
  | Bitc_one  -> B1
  end

let bit_of_bitU = function
  | B0 -> Bitc_zero
  | B1 -> Bitc_one
  | BU -> failwith "bit_of_bitU: BU"
  end

let bitU_of_bit_lifted = function
  | Bitl_zero -> B0
  | Bitl_one  -> B1
  | Bitl_undef -> BU
  | Bitl_unknown -> failwith "bitU_of_bit_lifted Bitl_unknown"
  end*)

let not_bit = function
  | B1 -> B0
  | B0 -> B1
  | BU -> BU
  end

val is_one : integer -> bitU
let is_one i =
  if i = 1 then B1 else B0

let binop_bit op x y = match (x, y) with
  | (BU,_) -> BU (*Do we want to do this or to respect | of I and & of B0 rules?*)
  | (_,BU) -> BU (*Do we want to do this or to respect | of I and & of B0 rules?*)
  | (x,y) -> bitU_of_bool (op (bool_of_bitU x) (bool_of_bitU y))
  end

val and_bit : bitU -> bitU -> bitU
let and_bit = binop_bit (&&)

val or_bit : bitU -> bitU -> bitU
let or_bit = binop_bit (||)

val xor_bit : bitU -> bitU -> bitU
let xor_bit = binop_bit xor

val (&.) : bitU -> bitU -> bitU
let inline (&.) x y = and_bit x y

val (|.) : bitU -> bitU -> bitU
let inline (|.) x y = or_bit x y

val (+.) : bitU -> bitU -> bitU
let inline (+.) x y = xor_bit x y


(*** Bit lists ***)

val bits_of_nat_aux : natural -> list bitU
let rec bits_of_nat_aux x =
  if x = 0 then []
  else (if x mod 2 = 1 then B1 else B0) :: bits_of_nat_aux (x / 2)
declare {isabelle} termination_argument bits_of_nat_aux = automatic
let bits_of_nat n = List.reverse (bits_of_nat_aux n)

val nat_of_bits_aux : natural -> list bitU -> natural
let rec nat_of_bits_aux acc bs = match bs with
  | [] -> acc
  | B1 :: bs -> nat_of_bits_aux ((2 * acc) + 1) bs
  | B0 :: bs -> nat_of_bits_aux (2 * acc) bs
  | BU :: _ -> failwith "nat_of_bits_aux: bit list has undefined bits"
end
declare {isabelle} termination_argument nat_of_bits_aux = automatic
let nat_of_bits bits = nat_of_bits_aux 0 bits

let not_bits = List.map not_bit

let binop_bits op bsl bsr =
  foldr (fun (bl, br) acc -> binop_bit op bl br :: acc) [] (zip bsl bsr)

let and_bits = binop_bits (&&)
let or_bits = binop_bits (||)
let xor_bits = binop_bits xor

val unsigned_of_bits : list bitU -> integer
let unsigned_of_bits bs = integerFromNatural (nat_of_bits bs)

val signed_of_bits : list bitU -> integer
let signed_of_bits bits =
  match bits with
  | B1 :: _ -> 0 - (1 + (unsigned_of_bits (not_bits bits)))
  | B0 :: _ -> unsigned_of_bits bits
  | BU :: _ -> failwith "signed_of_bits applied to list with undefined bits"
  | [] -> failwith "signed_of_bits applied to empty list"
  end

val pad_bitlist : bitU -> list bitU -> integer -> list bitU
let rec pad_bitlist b bits n =
  if n <= 0 then bits else pad_bitlist b (b :: bits) (n - 1)
declare {isabelle} termination_argument pad_bitlist = automatic

let ext_bits pad len bits =
  let longer = len - (integerFromNat (List.length bits)) in
  if longer < 0 then drop (natFromInteger (abs (longer))) bits
  else pad_bitlist pad bits longer

let extz_bits len bits = ext_bits B0 len bits
let exts_bits len bits =
  match bits with
  | BU :: _ -> failwith "exts_bits: undefined bit"
  | B1 :: _ -> ext_bits B1 len bits
  | _ -> ext_bits B0 len bits
  end

let rec add_one_bit_ignore_overflow_aux bits = match bits with
  | [] -> []
  | B0 :: bits -> B1 :: bits
  | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits
  | BU :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit"
end
declare {isabelle} termination_argument add_one_bit_ignore_overflow_aux = automatic

let add_one_bit_ignore_overflow bits =
  List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits))

let bitlist_of_int n =
  let bits_abs = B0 :: bits_of_nat (naturalFromInteger (abs n)) in
  if n >= (0 : integer) then bits_abs
  else add_one_bit_ignore_overflow (not_bits bits_abs)

let bits_of_int len n = exts_bits len (bitlist_of_int n)

let char_of_nibble = function
  | (B0, B0, B0, B0) -> Just #'0'
  | (B0, B0, B0, B1) -> Just #'1'
  | (B0, B0, B1, B0) -> Just #'2'
  | (B0, B0, B1, B1) -> Just #'3'
  | (B0, B1, B0, B0) -> Just #'4'
  | (B0, B1, B0, B1) -> Just #'5'
  | (B0, B1, B1, B0) -> Just #'6'
  | (B0, B1, B1, B1) -> Just #'7'
  | (B1, B0, B0, B0) -> Just #'8'
  | (B1, B0, B0, B1) -> Just #'9'
  | (B1, B0, B1, B0) -> Just #'A'
  | (B1, B0, B1, B1) -> Just #'B'
  | (B1, B1, B0, B0) -> Just #'C'
  | (B1, B1, B0, B1) -> Just #'D'
  | (B1, B1, B1, B0) -> Just #'E'
  | (B1, B1, B1, B1) -> Just #'F'
  | _ -> Nothing
  end

let rec hexstring_of_bits bs = 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
     | (Just n, Just s) -> Just (n :: s)
     | _ -> Nothing
     end
  | _ -> Nothing
  end
declare {isabelle} termination_argument hexstring_of_bits = automatic

let show_bitlist bs =
  match hexstring_of_bits bs with
  | Just s -> toString (#'0' :: #'x' :: s)
  | Nothing -> show bs
  end

(*** List operations *)

let inline (^^) = append_list

val subrange_list_inc : forall 'a. list 'a -> integer -> integer -> list 'a
let subrange_list_inc xs i j =
  let (toJ,_suffix) = List.splitAt (natFromInteger j + 1) xs in
  let (_prefix,fromItoJ) = List.splitAt (natFromInteger i) toJ in
  fromItoJ

val subrange_list_dec : forall 'a. list 'a -> integer -> integer -> list 'a
let subrange_list_dec xs i j =
  let top = (length_list xs) - 1 in
  subrange_list_inc xs (top - i) (top - j)

val subrange_list : forall 'a. bool -> list 'a -> integer -> integer -> list 'a
let subrange_list is_inc xs i j = 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' =
  let (toJ,suffix) = List.splitAt (natFromInteger j + 1) xs in
  let (prefix,_fromItoJ) = List.splitAt (natFromInteger i) toJ in
  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' =
  let top = (length_list xs) - 1 in
  update_subrange_list_inc xs (top - i) (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' =
  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 = List_extra.nth xs (natFromInteger n)

val access_list_dec : forall 'a. list 'a -> integer -> 'a
let access_list_dec xs n =
  let top = (length_list xs) - 1 in
  access_list_inc xs (top - n)

val access_list : forall 'a. bool -> list 'a -> integer -> 'a
let access_list is_inc xs n =
  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 = List.update xs (natFromInteger n) x

val update_list_dec : forall 'a. list 'a -> integer -> 'a -> list 'a
let update_list_dec xs n x =
  let top = (length_list xs) - 1 in
  update_list_inc xs (top - n) x

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

let extract_only_element = function
  | [] -> failwith "extract_only_element called for empty list"
  | [e] -> e
  | _ -> failwith "extract_only_element called for list with more elements"
end

(* 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 = match l with
  | [] -> Just []
  | (x :: xs) ->
    match (x, just_list xs) with
      | (Just x, Just xs) -> Just (x :: xs)
      | (_, _) -> Nothing
    end
  end
declare {isabelle} termination_argument just_list = automatic

lemma just_list_spec:
  ((forall xs. (just_list xs = Nothing) <-> List.elem Nothing xs) &&
   (forall xs es. (just_list xs = Just es) <-> (xs = List.map Just es)))

(*** Machine words *)

val length_mword : forall 'a. mword 'a -> integer
let length_mword w = integerFromNat (word_length w)

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

val slice_mword_inc : forall 'a 'b. mword 'a -> integer -> integer -> mword 'b
let slice_mword_inc w i j =
  let top = (length_mword w) - 1 in
  slice_mword_dec w (top - i) (top - j)

val slice_mword : forall 'a 'b. bool -> mword 'a -> integer -> integer -> mword 'b
let slice_mword is_inc w i j = 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' = word_update w (natFromInteger i) (natFromInteger 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' =
  let top = (length_mword w) - 1 in
  update_slice_mword_dec w (top - i) (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' =
  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_of_bool (getBit w (natFromInteger n))

val access_mword_inc : forall 'a. mword 'a -> integer -> bitU
let access_mword_inc w n =
  let top = (length_mword w) - 1 in
  access_mword_dec w (top - n)

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

val update_mword_dec : forall 'a. mword 'a -> integer -> bitU -> mword 'a
let update_mword_dec w n b = setBit w (natFromInteger n) (bool_of_bitU b)

val update_mword_inc : forall 'a. mword 'a -> integer -> bitU -> mword 'a
let update_mword_inc w n b =
  let top = (length_mword w) - 1 in
  update_mword_dec w (top - n) b

val update_mword : forall 'a. bool -> mword 'a -> integer -> bitU -> mword 'a
let update_mword is_inc w n b =
  if is_inc then update_mword_inc w n b else update_mword_dec w n b

val mword_of_int : forall 'a. Size 'a => integer -> integer -> mword 'a
let mword_of_int len n =
  let w = wordFromInteger n in
  if (length_mword w = len) then w else failwith "unexpected word length"

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

let size_itself_int x = integerFromNat (size_itself 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 inline make_the_value x = the_value

(*** Bitvectors *)

class (Bitvector 'a)
  val bits_of : 'a -> list bitU
  val of_bits : list bitU -> 'a
  (* The first parameter specifies the desired length of the bitvector *)
  val of_int : integer -> integer -> 'a
  val length : 'a -> integer
  val unsigned : 'a -> integer
  val signed : 'a -> integer
  (* The first parameter specifies the indexing order (true is increasing) *)
  val get_bit : bool -> 'a -> integer -> bitU
  val set_bit : bool -> 'a -> integer -> bitU -> 'a
  val get_bits : bool -> 'a -> integer -> integer -> list bitU
  val set_bits : bool -> 'a -> integer -> integer -> list bitU -> 'a
end

instance forall 'a. BitU 'a => (Bitvector (list 'a))
  let bits_of v = List.map to_bitU v
  let of_bits v = List.map of_bitU v
  let of_int len n = List.map of_bitU (bits_of_int len n)
  let length = length_list
  let unsigned v = unsigned_of_bits (List.map to_bitU v)
  let signed v = signed_of_bits (List.map to_bitU v)
  let get_bit is_inc v n = to_bitU (access_list is_inc v n)
  let set_bit is_inc v n b = update_list is_inc v n (of_bitU b)
  let get_bits is_inc v i j = List.map to_bitU (subrange_list is_inc v i j)
  let set_bits is_inc v i j v' = update_subrange_list is_inc v i j (List.map of_bitU v')
end

instance forall 'a. Size 'a => (Bitvector (mword 'a))
  let bits_of v = List.map to_bitU (bitlistFromWord v)
  let of_bits v = wordFromBitlist (List.map of_bitU v)
  let of_int = mword_of_int
  let length v = integerFromNat (word_length v)
  let unsigned = unsignedIntegerFromWord
  let signed = signedIntegerFromWord
  let get_bit = access_mword
  let set_bit = update_mword
  let get_bits is_inc v i j = get_bits is_inc (bitlistFromWord v) i j
  let set_bits is_inc v i j v' = wordFromBitlist (set_bits is_inc (bitlistFromWord v) i j v')
end

let access_bv_inc v n = get_bit true  v n
let access_bv_dec v n = get_bit false v n

let update_bv_inc v n b = set_bit true  v n b
let update_bv_dec v n b = set_bit false v n b

let subrange_bv_inc v i j = of_bits (get_bits true  v i j)
let subrange_bv_dec v i j = of_bits (get_bits false v i j)

let update_subrange_bv_inc v i j v' = set_bits true  v i j (bits_of v')
let update_subrange_bv_dec v i j v' = set_bits false v i j (bits_of v')

val extz_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b => integer -> 'a -> 'b
let extz_bv n v = of_bits (extz_bits n (bits_of v))

val exts_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b => integer -> 'a -> 'b
let exts_bv n v = of_bits (exts_bits n (bits_of v))

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

(*** Bytes and addresses *)

type memory_byte = list bitU

val byte_chunks : forall 'a. list 'a -> maybe (list (list 'a))
let rec byte_chunks bs = match bs with
  | [] -> Just []
  | a::b::c::d::e::f::g::h::rest ->
     Maybe.bind (byte_chunks rest) (fun rest -> Just ([a;b;c;d;e;f;g;h] :: rest))
  | _ -> Nothing
end
declare {isabelle} termination_argument byte_chunks = automatic

val bytes_of_bits : forall 'a. Bitvector 'a => 'a -> maybe (list memory_byte)
let bytes_of_bits bs = byte_chunks (bits_of bs)

val bits_of_bytes : forall 'a. Bitvector 'a => list memory_byte -> 'a
let bits_of_bytes bs = of_bits (List.concat (List.map bits_of bs))

let mem_bytes_of_bits bs = Maybe.map List.reverse (bytes_of_bits bs)
let bits_of_mem_bytes bs = bits_of_bytes (List.reverse 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 =
  if List.length bits <= 8 then bits else
    reverse_endianness_list (drop_list 8 bits) ++ take_list 8 bits

val reverse_endianness : forall 'a. Bitvector 'a => 'a -> 'a
let reverse_endianness v = of_bits (reverse_endianness_list (bits_of v))


(*** 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 register_ref 'regstate 'regval 'a =
  <| name : string;
     (*is_inc : bool;*)
     read_from : 'regstate -> 'a;
     write_to : 'a -> 'regstate -> 'regstate;
     of_regval : 'regval -> maybe 'a;
     regval_of : 'a -> 'regval |>

type register_accessors 'regstate 'regval =
  ((string -> 'regstate -> maybe 'regval) *
   (string -> 'regval -> 'regstate -> maybe 'regstate))

type field_ref 'regtype 'a =
  <| field_name : string;
     field_start : integer;
     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/concurrecny 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 [] vars _ = vars
and foreach (x :: xs) vars body = foreach xs (body x vars) body

declare {isabelle} termination_argument foreach = automatic

val index_list : integer -> integer -> integer -> list integer
let rec index_list from to step =
  if (step > 0 && from <= to) || (step < 0 && to <= from) then
    from :: index_list (from + step) to step
  else []

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

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


let assert' b msg_opt =
  let msg = match msg_opt with
  | Just msg -> msg
  | Nothing  -> "unspecified error"
  end in
  if b then () else failwith msg

(* convert numbers unsafely to naturals *)

class (ToNatural 'a) val toNatural : 'a -> natural end
(* eta-expanded for Isabelle output, otherwise it breaks *)
instance (ToNatural integer) let toNatural = (fun n -> naturalFromInteger n) end
instance (ToNatural int)     let toNatural = (fun n -> naturalFromInt n)     end
instance (ToNatural nat)     let toNatural = (fun n -> naturalFromNat n)     end
instance (ToNatural natural) let toNatural = (fun n -> n)                    end

let toNaturalFiveTup (n1,n2,n3,n4,n5) =
  (toNatural n1,
   toNatural n2,
   toNatural n3,
   toNatural n4,
   toNatural 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
*)