(* 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 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 quotient_int (l,r) = integerDiv l r
let quotient_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 list_append (l, r) = l ++ r
let list_length xs = integerFromNat (List.length xs)
let list_take (n, xs) = List.take (natFromInteger n) xs
let list_drop (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)

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

let upper n = n

(*** 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 bitU_to_bool = function
  | B0 -> false
  | B1  -> true
  | BU -> failwith "to_bool applied to BU"
  end

let bool_to_bitU b = if b then B1 else B0

instance (BitU bool)
  let to_bitU = bool_to_bitU
  let of_bitU = bitU_to_bool
end

let cast_bit_bool = bitU_to_bool

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 bitwise_not_bit = function
  | B1 -> B0
  | B0 -> B1
  | BU -> BU
  end

(* let inline (~) = bitwise_not_bit *)

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

let bitwise_binop_bit op = function
  | (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) -> bool_to_bitU (op (bitU_to_bool x) (bitU_to_bool y))
  end

val bitwise_and_bit : bitU * bitU -> bitU
let bitwise_and_bit = bitwise_binop_bit (&&)

val bitwise_or_bit : bitU * bitU -> bitU
let bitwise_or_bit = bitwise_binop_bit (||)

val bitwise_xor_bit : bitU * bitU -> bitU
let bitwise_xor_bit = bitwise_binop_bit xor

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

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

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

val to_bin_aux : natural -> list bitU
let rec to_bin_aux x =
  if x = 0 then []
  else (if x mod 2 = 1 then B1 else B0) :: to_bin_aux (x / 2)
let to_bin n = List.reverse (to_bin_aux n)

val of_bin : list bitU -> natural
let of_bin bits =
  let (sum,_) =
    List.foldr
      (fun b (acc,exp) ->
        match b with
        | B1 -> (acc + naturalPow 2 exp, exp + 1)
        | B0 -> (acc, exp + 1)
        | BU -> failwith "of_bin: bitvector has undefined bits"
        end)
      (0,0) bits in
  sum

val bitlist_to_integer : list bitU -> integer
let bitlist_to_integer bs = integerFromNatural (of_bin bs)

val pad_zero : list bitU -> integer -> list bitU
let rec pad_zero bits n =
  if n <= 0 then bits else pad_zero (B0 :: bits) (n -1)

let bitwise_not_bitlist = List.map bitwise_not_bit

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

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

let bits_of_nat ((len : integer),(n : natural)) =
  let bits = to_bin n in
  let len_bits = integerFromNat (List.length bits) in
  let longer = len - len_bits in
  if longer < 0 then drop (natFromInteger (abs (longer))) bits
  else pad_zero bits longer

let bits_of_int ((len : integer),(n : integer)) =
  let bits = bits_of_nat (len, naturalFromInteger (abs n)) in
  if n > (0 : integer)
  then bits
  else (add_one_bit_ignore_overflow (bitwise_not_bitlist bits))


(*** Vectors *)

(* element list * start * has increasing direction *)
type vector 'a = Vector of list 'a * integer * bool

let showVector (Vector elems start inc) =
  "Vector " ^ show elems ^ " " ^ show start ^ " " ^ show inc

let get_dir (Vector _ _ ord) = ord
let get_start (Vector _ s _) = s
let get_elems (Vector elems _ _) = elems
let length (Vector bs _ _) = integerFromNat (length bs)
let vector_length = length

instance forall 'a. Show 'a => (Show (vector 'a))
  let show = showVector
end

let dir is_inc = if is_inc then D_increasing else D_decreasing
let bool_of_dir = function
  | D_increasing -> true
  | D_decreasing -> false
  end

(*** Vector operations *)

val set_vector_start : forall 'a. (integer * vector 'a) -> vector 'a
let set_vector_start (new_start, Vector bs _ is_inc) =
  Vector bs new_start is_inc

let reset_vector_start v =
  set_vector_start (if (get_dir v) then 0 else (length v - 1), v)

let set_vector_start_to_length v =
  set_vector_start (length v - 1, v)

let vector_concat (Vector bs start is_inc, Vector bs' _ _) =
  Vector (bs ++ bs') start is_inc

let inline (^^) = vector_concat

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

val update_sublist : forall 'a. list 'a -> (nat * nat) -> list 'a -> list 'a
let update_sublist xs (i,j) xs' =
  let (toJ,suffix) = List.splitAt (j+1) xs in
  let (prefix,_fromItoJ) = List.splitAt i toJ in
  prefix ++ xs' ++ suffix

val slice_aux : forall 'a. bool -> integer -> list 'a -> integer -> integer -> list 'a
let slice_aux is_inc start bs i j =
  let iN = natFromInteger i in
  let jN = natFromInteger j in
  let startN = natFromInteger start in
  sublist bs (if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN))

val slice : forall 'a. vector 'a -> integer -> integer -> vector 'a
let slice (Vector bs start is_inc) i j =
  Vector (slice_aux is_inc start bs i j) i is_inc

let vector_subrange_inc (start, v, i, j) = slice v i j
let vector_subrange_dec (start, v, i, j) = slice v i j

(* this is for the vector slicing introduced in vector-concat patterns: i and j
index into the "raw data", the list of bits. Therefore getting the bit list is
easy, but the start index has to be transformed to match the old vector start
and the direction. *)
val slice_raw : forall 'a. vector 'a -> integer -> integer -> vector 'a
let slice_raw (Vector bs start is_inc) i j =
  let iN = natFromInteger i in
  let jN = natFromInteger j in
  let bits = sublist bs (iN,jN) in
  let len = integerFromNat (List.length bits) in
  Vector bits (if is_inc then 0 else len - 1) is_inc


val update_aux : forall 'a. bool -> integer -> list 'a -> integer -> integer -> list 'a -> list 'a
let update_aux is_inc start bs i j bs' =
  let iN = natFromInteger i in
  let jN = natFromInteger j in
  let startN = natFromInteger start in
  update_sublist bs
      (if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN)) bs'

val update : forall 'a. vector 'a -> integer -> integer -> vector 'a -> vector 'a
let update (Vector bs start is_inc) i j (Vector bs' _ _) =
  Vector (update_aux is_inc start bs i j bs') start is_inc

let vector_update_subrange_inc (start, v, i, j, v') = update v i j v'
let vector_update_subrange_dec (start, v, i, j, v') = update v i j v'

val access_aux : forall 'a. bool -> integer -> list 'a -> integer -> 'a
let access_aux is_inc start xs n =
  if is_inc then List_extra.nth xs (natFromInteger (n - start))
  else List_extra.nth xs (natFromInteger (start - n))

val access : forall 'a. vector 'a -> integer -> 'a
let access (Vector bs start is_inc) n = access_aux is_inc start bs n

let vector_access_inc (start, v, i) = access v i
let vector_access_dec (start, v, i) = access v i

val update_pos : forall 'a. vector 'a -> integer -> 'a -> vector 'a
let update_pos v n b =
  update v n n (Vector [b] 0 false)

let vector_update_pos_inc (start, v, i, x) = update_pos v i x
let vector_update_pos_dec (start, v, i, x) = update_pos v i x

let extract_only_element (Vector elems _ _) = match elems with
  | [] -> failwith "extract_only_element called for empty vector"
  | [e] -> e
  | _ -> failwith "extract_only_element called for vector with more elements"
end

(*** Bitvectors *)

(* element list * start * has increasing direction *)
type bitvector 'a = mword 'a (* Bitvector of mword 'a * integer * bool *)
declare isabelle target_sorts bitvector = `len`

class (Bitvector 'a)
  val bits_of : 'a -> list bitU
  val of_bits : list bitU -> 'a
  val unsigned : 'a -> integer
  (* The first two parameters of the following specify indexing:
     indexing order and start index *)
  val get_bit : bool -> integer -> 'a -> integer -> bitU
  val set_bit : bool -> integer -> 'a -> integer -> bitU -> 'a
  val get_bits : bool -> integer -> 'a -> integer -> integer -> list bitU
  val set_bits : bool -> integer -> '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 unsigned v = bitlist_to_integer (List.map to_bitU v)
  let get_bit is_inc start v n = to_bitU (access_aux is_inc start v n)
  let set_bit is_inc start v n b = update_aux is_inc start v n n [of_bitU b]
  let get_bits is_inc start v i j = List.map to_bitU (slice_aux is_inc start v i j)
  let set_bits is_inc start v i j v' = update_aux is_inc start v i j (List.map of_bitU v')
end

instance forall 'a. BitU 'a => (Bitvector (vector 'a))
  let bits_of v = List.map to_bitU (get_elems v)
  let of_bits v = Vector (List.map of_bitU v) (integerFromNat (List.length v) - 1) false
  let unsigned v = unsigned (get_elems v)
  let get_bit is_inc start v n = to_bitU (access v n)
  let set_bit is_inc start v n b = update_pos v n (of_bitU b)
  let get_bits is_inc start v i j = List.map to_bitU (get_elems (slice v i j))
  let set_bits is_inc start v i j v' = update v i j (Vector (List.map of_bitU v') (integerFromNat (List.length v') - 1) false)
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 unsigned v = unsignedIntegerFromWord v
  let get_bit is_inc start v n = to_bitU (access_aux is_inc start (bitlistFromWord v) n)
  let set_bit is_inc start v n b = wordFromBitlist (update_aux is_inc start (bitlistFromWord v) n n [of_bitU b])
  let get_bits is_inc start v i j = slice_aux is_inc start (List.map to_bitU (bitlistFromWord v)) i j
  let set_bits is_inc start v i j v' = wordFromBitlist (update_aux is_inc start (bitlistFromWord v) i j (List.map of_bitU v'))
end

(*let showBitvector (Bitvector elems start inc) =
  "Bitvector " ^ show elems ^ " " ^ show start ^ " " ^ show inc

let bvget_dir (Bitvector _ _ ord) = ord
let bvget_start (Bitvector _ s _) = s
let bvget_elems (Bitvector elems _ _) = elems

instance forall 'a. (Show (bitvector 'a))
  let show = showBitvector
end*)

let bvec_to_vec is_inc start bs =
  let bits = List.map bool_to_bitU (bitlistFromWord bs) in
  Vector bits start is_inc

let vec_to_bvec (Vector elems start is_inc) =
  (*let word =*) wordFromBitlist (List.map bitU_to_bool elems) (*in
  Bitvector word start is_inc*)

(*** Vector operations *)

(* Bytes and addresses *)

val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a)
let rec byte_chunks n list = match (n,list) with
  | (0,_) -> []
  | (n+1, a::b::c::d::e::f::g::h::rest) -> [a;b;c;d;e;f;g;h] :: byte_chunks n rest
  | _ -> failwith "byte_chunks not given enough bits"
end

val bitv_of_byte_lifteds : bool -> list Sail_impl_base.byte_lifted -> list bitU
let bitv_of_byte_lifteds dir v =
  let bits = foldl (fun x (Byte_lifted y) -> x ++ (List.map bitU_of_bit_lifted y)) [] v in
  let len = integerFromNat (List.length bits) in
  bits (*Vector bits (if dir then 0 else len - 1) dir*)

val bitv_of_bytes : bool -> list Sail_impl_base.byte -> list bitU
let bitv_of_bytes dir v =
  let bits = foldl (fun x (Byte y) -> x ++ (List.map bitU_of_bit y)) [] v in
  let len = integerFromNat (List.length bits) in
  bits (*Vector bits (if dir then 0 else len - 1) dir*)


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 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_bl bits =
  if List.length bits <= 8 then bits else
    list_append(reverse_endianness_bl(list_drop(8, bits)), list_take(8, bits))

val reverse_endianness : forall 'a. Bitvector 'a => 'a -> 'a
let reverse_endianness v = of_bits (reverse_endianness_bl (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 'a =
  <| reg_name : string;
     reg_start : integer;
     reg_is_inc : bool;
     read_from : 'regstate -> 'a;
     write_to : 'regstate -> 'a -> '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 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, slice_end) ->
        ((if dir = D_increasing then slice_start else (reg_start - slice_start)),
         slice_start, dir)
     | Reg_field _ reg_start dir _ (slice_start, slice_end) ->
        ((if dir = D_increasing then slice_start else (reg_start - slice_start)),
         slice_start, dir)
     | Reg_f_slice _ reg_start dir _ _ (slice_start, slice_end) ->
        ((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 

let external_reg_whole reg =
  Reg (name_of_reg reg) (start_of_reg_nat reg) (size_of_reg_nat reg) (dir_of_reg reg)
      
let external_reg_slice reg (i,j) =
  let start = start_of_reg_nat reg in
  let dir = dir_of_reg reg in
  Reg_slice (name_of_reg reg) 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))

let external_mem_value v =
  byte_lifteds_of_bitv v $> List.reverse

let internal_mem_value direction bytes =
  List.reverse bytes $> bitv_of_byte_lifteds direction



                       

val foreach_inc :  forall 'vars. (integer * integer * integer) -> 'vars ->
                   (integer -> 'vars -> 'vars) -> 'vars
let rec foreach_inc (i,stop,by) vars body =
  if (by > 0 && i <= stop) || (by < 0 && stop <= i)
  then let vars = body i vars in
       foreach_inc (i + by,stop,by) vars body
  else vars

val foreach_dec : forall 'vars. (integer * integer * integer) -> 'vars ->
                  (integer -> 'vars -> 'vars) -> 'vars
let rec foreach_dec (i,stop,by) vars body =
  if (by > 0 && i >= stop) || (by < 0 && stop >= i)
  then let vars = body i vars in
       foreach_dec (i - by,stop,by) vars body
  else vars

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_LR
  | NIAFP_CTR
  | NIAFP_register of regfp

(* 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 (bits_of v))
  | NIAFP_LR -> NIA_LR
  | NIAFP_CTR -> NIA_CTR
  | NIAFP_register r -> NIA_register (regfp_to_reg reginfo r)
end

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