open import Pervasives_extra
open import Sail_impl_base
open import Vector
open import Interp     (* only for converting between shallow- and deep-embedding values *)
open import Interp_ast (* only for converting between shallow- and deep-embedding values *)

type i = integer
type n = natural

type bitU = O | I | Undef


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

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

let name_of_reg (Register name _ _ _ _) = name
let size_of_reg (Register _ size _ _ _) = size
let start_of_reg (Register _ _ start _ _) = start
let is_inc_of_reg (Register _ _ _ is_inc _) = is_inc
let dir_of_reg (Register _ _ _ is_inc _) = dir is_inc

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 : register -> register_field -> integer * integer
let register_field_indices (Register _ _ _ _ rfields) rfield =
  match List.lookup rfield rfields with
  | None -> failwith "Invalid register/register-field combination"
  | Just indices -> indices
  end

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

let to_bool = function
  | O -> false
  | I  -> true
  | Undef -> failwith "to_bool applied to Undef"
  end


let bit_lifted_of_bitU = function
  | O -> Bitl_zero
  | I -> Bitl_one
  | Undef -> Bitl_undef
  end

let bitU_of_bit = function
  | Bitc_zero -> O
  | Bitc_one  -> I
  end

let bitU_of_bit_lifted = function
  | Bitl_zero -> O
  | Bitl_one  -> I
  | Bitl_undef -> Undef
  | Bitl_unknown -> failwith "bitU_of_bit_lifted Bitl_unknown"
  end

let has_undef (Vector bs _ _) = List.any (function Undef -> true | _ -> false end) bs

let most_significant = function
  | (Vector (b :: _) _ _) -> b
  | _ -> failwith "most_significant applied to empty vector"
  end

let bitwise_not_bit = function
  | I -> O
  | O -> I
  | _ -> Undef
  end

let (~) = bitwise_not_bit

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


let bitwise_not (Vector bs start is_inc) =
  Vector (List.map bitwise_not_bit bs) start is_inc

val is_one : integer -> bitU
let is_one i =
  if i = 1 then I else O

let bool_to_bit b = if b then I else O

let bitwise_binop_bit op = function
  | (Undef,_) -> Undef (*Do we want to do this or to respect | of I and & of B0 rules?*)
  | (_,Undef) -> Undef (*Do we want to do this or to respect | of I and & of B0 rules?*)
  | (x,y) -> bool_to_bit (op (to_bool x) (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 (&.) x y = bitwise_and_bit (x,y)

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

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

let bitwise_binop op (Vector bsl start is_inc, Vector bsr _ _) =
  let revbs = foldl (fun acc pair -> bitwise_binop_bit op pair :: acc) [] (zip bsl bsr) in
  Vector (reverse revbs) start is_inc

let bitwise_and = bitwise_binop (&&)
let bitwise_or = bitwise_binop (||)
let bitwise_xor = bitwise_binop xor

let unsigned (Vector bs _ _ as v) : integer =
  if has_undef v then failwith "unsigned applied to vector with undefined bits" else
    fst (List.foldl
           (fun (acc,exp) b -> (acc + (if b = I then integerPow 2 exp else 0),exp +1)) (0,0) bs)

let unsigned_big = unsigned
        
let signed v : integer =
  match most_significant v with
  | I -> 0 - (1 + (unsigned (bitwise_not v)))
  | O -> unsigned v
  | _ -> failwith "signed applied to vector with undefined bits"
  end

let signed_big = signed

let to_num sign = if sign then signed else unsigned
  
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)

let get_max_representable_in sign (n : integer) : integer = 
  if (n = 64) then match sign with | true -> max_64 | false -> max_64u end
  else if (n=32) then match sign with | true -> max_32 | false -> max_32u end
  else if (n=8) then max_8
  else if (n=5) then max_5
  else match sign with | true -> integerPow 2 ((natFromInteger n) -1)
                       | false -> integerPow 2 (natFromInteger n)
       end

let get_min_representable_in _ (n : integer) : integer = 
  if n = 64 then min_64
  else if n = 32 then min_32
  else if n = 8 then min_8
  else if n = 5 then min_5
  else 0 - (integerPow 2 (natFromInteger n))


let rec divide_by_2 bs (i : integer) (n : integer) =
  if i < 0 || n = 0
  then bs
  else
    if (n mod 2 = 1)
    then divide_by_2 (replace bs (i,I)) (i - 1) (n / 2)
    else divide_by_2 bs (i-1) (n div 2)

let rec add_one_bit bs co (i : integer) =
  if i < 0 then bs
  else match (List_extra.nth bs (natFromInteger i),co) with
    | (O,false) -> replace bs (i,I)
    | (O,true)  -> add_one_bit (replace bs (i,I)) true (i-1)
    | (I,false) -> add_one_bit (replace bs (i,O)) true (i-1)
    | (I,true)  -> add_one_bit bs true (i-1)
    | _ -> failwith "add_one_bit applied to list with undefined bit"
   (*    | Vundef,_ -> assert false*) 
  end

let to_vec is_inc ((len : integer),(n : integer)) =
  let bs = List.replicate (natFromInteger len) O in
  let start = if is_inc then 0 else len-1 in
  if n = 0 then
    Vector bs start is_inc
  else if n > 0 then
    Vector (divide_by_2 bs (len-1) n) start is_inc
  else
    let abs_bs = divide_by_2 bs (len-1) (abs n) in
    let (Vector bs start is_inc) = bitwise_not (Vector abs_bs start is_inc) in
    Vector (add_one_bit bs false (len-1)) start is_inc

let to_vec_big = to_vec
      
let to_vec_inc = to_vec true
let to_vec_dec = to_vec false

let to_vec_undef is_inc (len : integer) =
  Vector (replicate (natFromInteger len) Undef) (if is_inc then 0 else len-1) is_inc

let to_vec_inc_undef = to_vec_undef true
let to_vec_dec_undef = to_vec_undef false
                                    
let exts (len, vec) = to_vec (get_dir vec) (len,signed vec)
let extz (len, vec) = to_vec (get_dir vec) (len,unsigned vec)

let exts_big (len, vec) = to_vec_big (get_dir vec) (len, signed_big vec)
let extz_big (len, vec) = to_vec_big (get_dir vec) (len, unsigned_big vec)

let add = integerAdd
let add_signed = integerAdd
let minus = integerMinus
let multiply = integerMult
let modulo = integerMod
let quot = integerDiv
let power = integerPow

let arith_op_vec op sign (size : integer) (Vector _ _ is_inc as l) r =
  let (l',r') = (to_num sign l, to_num sign r) in
  let n = op  l' r' in
  to_vec is_inc (size * (length l),n)


(* add_vec
 * add_vec_signed
 * minus_vec 
 * multiply_vec 
 * multiply_vec_signed
 *)
let add_VVV = arith_op_vec integerAdd false 1
let addS_VVV = arith_op_vec integerAdd true 1
let minus_VVV = arith_op_vec integerMinus false 1
let mult_VVV = arith_op_vec integerMult false 2
let multS_VVV = arith_op_vec integerMult true 2

let arith_op_vec_range op sign size (Vector _ _ is_inc as l) r =
  arith_op_vec op sign size l (to_vec is_inc (length l,r))

(* add_vec_range
 * add_vec_range_signed
 * minus_vec_range 
 * mult_vec_range 
 * mult_vec_range_signed
 *)
let add_VIV = arith_op_vec_range integerAdd false 1
let addS_VIV = arith_op_vec_range integerAdd true 1
let minus_VIV = arith_op_vec_range integerMinus false 1
let mult_VIV = arith_op_vec_range integerMult false 2
let multS_VIV = arith_op_vec_range integerMult true 2

let arith_op_range_vec op sign size l (Vector _ _ is_inc as r) =
  arith_op_vec op sign size (to_vec is_inc (length r, l)) r

(* add_range_vec
 * add_range_vec_signed
 * minus_range_vec 
 * mult_range_vec
 * mult_range_vec_signed
 *)
let add_IVV = arith_op_range_vec integerAdd false 1
let addS_IVV = arith_op_range_vec integerAdd true 1
let minus_IVV = arith_op_range_vec integerMinus false 1
let mult_IVV = arith_op_range_vec integerMult false 2
let multS_IVV = arith_op_range_vec integerMult true 2

let arith_op_range_vec_range op sign l r = op l (to_num sign r)

(* add_range_vec_range
 * add_range_vec_range_signed
 * minus_range_vec_range 
 *)
let add_IVI = arith_op_range_vec_range integerAdd false
let addS_IVI = arith_op_range_vec_range integerAdd true
let minus_IVI = arith_op_range_vec_range integerMinus false

let arith_op_vec_range_range op sign l r = op (to_num sign l) r

(* add_vec_range_range
 * add_vec_range_range_signed
 * minus_vec_range_range
 *)
let add_VII = arith_op_vec_range_range integerAdd false
let addS_VII = arith_op_vec_range_range integerAdd true
let minus_VII = arith_op_vec_range_range integerMinus false



let arith_op_vec_vec_range op sign l r = 
  let (l',r') = (to_num sign l,to_num sign r) in
  op l' r'

(* add_vec_vec_range
 * add_vec_vec_range_signed
 *)
let add_VVI = arith_op_vec_vec_range integerAdd false
let addS_VVI = arith_op_vec_vec_range integerAdd true

let arith_op_vec_bit op sign (size : integer) (Vector _ _ is_inc as l)r =
  let l' = to_num sign l in
  let n = op l' (match r with | I -> (1 : integer) | _ -> 0 end) in
  to_vec is_inc (length l * size,n)
    
(* add_vec_bit
 * add_vec_bit_signed
 * minus_vec_bit_signed
 *)
let add_VBV = arith_op_vec_bit integerAdd false 1
let addS_VBV = arith_op_vec_bit integerAdd true 1
let minus_VBV = arith_op_vec_bit integerMinus true 1

let rec arith_op_overflow_vec (op : integer -> integer -> integer) sign size (Vector _ _ is_inc as l) r =
  let len = length l in
  let act_size = len * size in
  let (l_sign,r_sign) = (to_num sign l,to_num sign r) in
  let (l_unsign,r_unsign) = (to_num false l,to_num false r) in
  let n = op l_sign r_sign in
  let n_unsign = op l_unsign r_unsign in
  let correct_size_num = to_vec is_inc (act_size,n) in
  let one_more_size_u = to_vec is_inc (act_size + 1,n_unsign) in
  let overflow =
    if n <= get_max_representable_in sign len &&
         n >= get_min_representable_in sign len
    then O else I in
  let c_out = most_significant one_more_size_u in
  (correct_size_num,overflow,c_out)

(* add_overflow_vec
 * add_overflow_vec_signed
 * minus_overflow_vec
 * minus_overflow_vec_signed
 * mult_overflow_vec
 * mult_overflow_vec_signed
 *)
let addO_VVV = arith_op_overflow_vec integerAdd false 1
let addSO_VVV = arith_op_overflow_vec integerAdd true 1
let minusO_VVV = arith_op_overflow_vec integerMinus false 1
let minusSO_VVV = arith_op_overflow_vec integerMinus true 1
let multO_VVV = arith_op_overflow_vec integerMult false 2
let multSO_VVV = arith_op_overflow_vec integerMult true 2

let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (size : integer)
                                  (Vector _ _ is_inc as l) r_bit =
  let act_size = length l * size in
  let l' = to_num sign l in
  let l_u = to_num false l in
  let (n,nu,changed) = match r_bit with
    | I -> (op l' 1, op l_u 1, true)
    | O -> (l',l_u,false)
    | _ -> failwith "arith_op_overflow_vec_bit applied to undefined bit"
    end in
(*    | _ -> assert false *)
  let correct_size_num = to_vec is_inc (act_size,n) in
  let one_larger = to_vec is_inc (act_size + 1,nu) in
  let overflow =
    if changed 
    then
      if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size
      then O else I 
    else I in
  (correct_size_num,overflow,most_significant one_larger)

(* add_overflow_vec_bit_signed
 * minus_overflow_vec_bit
 * minus_overflow_vec_bit_signed 
 *)
let addSO_VBV = arith_op_overflow_vec_bit integerAdd true 1
let minusO_VBV = arith_op_overflow_vec_bit integerMinus false 1
let minusSO_VBV = arith_op_overflow_vec_bit integerMinus true 1
    
type shift = LL_shift | RR_shift | LLL_shift

let shift_op_vec op ((Vector bs start is_inc as l),(n : integer)) =
  let len = integerFromNat (List.length bs) in
    match op with
     | LL_shift (*"<<"*) ->
       let right_vec = Vector (List.replicate (natFromInteger n) O) 0 true in
       let left_vec = slice l n (if is_inc then len + start else start - len) in
       vector_concat left_vec right_vec
     | RR_shift (*">>"*) ->
       let right_vec = slice l start n in
       let left_vec = Vector (List.replicate (natFromInteger n) O) 0 true in
       vector_concat left_vec right_vec 
     | LLL_shift (*"<<<"*) ->
       let left_vec = slice l n (if is_inc then len + start else start - len) in
       let right_vec = slice l start n in
       vector_concat left_vec right_vec
     end

let bitwise_leftshift = shift_op_vec LL_shift (*"<<"*)
let bitwise_rightshift = shift_op_vec RR_shift (*">>"*)
let bitwise_rotate = shift_op_vec LLL_shift (*"<<<"*)

let rec arith_op_no0 (op : integer -> integer -> integer) l r = 
  if r = 0
  then Nothing
  else Just (op l r)

let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((Vector _ start is_inc) as l) r =
  let act_size = length l * size in
  let (l',r') = (to_num sign l,to_num sign r) in
  let n = arith_op_no0 op l' r' in
  let (representable,n') = 
    match n with 
    | Just n' ->  
      (n' <= get_max_representable_in sign act_size &&
         n' >= get_min_representable_in sign act_size, n')
    | _ -> (false,0)
    end in
  if representable 
  then to_vec is_inc (act_size,n')
  else Vector (List.replicate (natFromInteger act_size) Undef) start is_inc

let mod_VVV = arith_op_vec_no0 integerMod false 1
let quot_VVV = arith_op_vec_no0 integerDiv false 1
let quotS_VVV = arith_op_vec_no0 integerDiv true 1

let arith_op_overflow_no0_vec op sign size ((Vector _ start is_inc) as l) r =
  let rep_size = length r * size in
  let act_size = length l * size in
  let (l',r') = (to_num sign l,to_num sign r) in
  let (l_u,r_u) = (to_num false l,to_num false r) in
  let n = arith_op_no0 op l' r' in
  let n_u = arith_op_no0 op l_u r_u in
  let (representable,n',n_u') = 
    match (n, n_u) with 
    | (Just n',Just n_u') ->  
       ((n' <= get_max_representable_in sign rep_size &&
           n' >= (get_min_representable_in sign rep_size)), n', n_u')
    | _ -> (true,0,0)
    end in
  let (correct_size_num,one_more) = 
    if representable then
      (to_vec is_inc (act_size,n'),to_vec is_inc (act_size + 1,n_u'))
    else
      (Vector (List.replicate (natFromInteger act_size) Undef) start is_inc,
       Vector (List.replicate (natFromInteger (act_size + 1)) Undef) start is_inc) in
  let overflow = if representable then O else I in
  (correct_size_num,overflow,most_significant one_more)

let quotO_VVV = arith_op_overflow_no0_vec integerDiv false 1
let quotSO_VVV = arith_op_overflow_no0_vec integerDiv true 1

let arith_op_vec_range_no0 op sign size (Vector _ _ is_inc as l) r =
  arith_op_vec_no0 op sign size l (to_vec is_inc (length l,r))

let mod_VIV = arith_op_vec_range_no0 integerMod false 1

let duplicate (bit,length) =
  Vector (List.replicate (natFromInteger length) bit) 0 true

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_bits (Vector bits start direction,len) = 
  let bits' = repeat bits len in
  Vector bits' start direction

let compare_op op (l,r) = bool_to_bit (op l r)

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


let compare_op_vec op sign (l,r) = 
  let (l',r') = (to_num sign l, to_num sign r) in
  compare_op op (l',r')

let lt_vec = compare_op_vec (>) true
let gt_vec = compare_op_vec (>) true
let lteq_vec = compare_op_vec (<=) true
let gteq_vec = compare_op_vec (>=) true

let lt_vec_signed = compare_op_vec (<) true
let gt_vec_signed = compare_op_vec (>) true
let lteq_vec_signed = compare_op_vec (<=) true
let gteq_vec_signed = compare_op_vec (>=) true
let lt_vec_unsigned = compare_op_vec (<) false
let gt_vec_unsigned = compare_op_vec (>) false
let lteq_vec_unsigned = compare_op_vec (<=) false
let gteq_vec_unsigned = compare_op_vec (>=) false

let compare_op_vec_range op sign (l,r) = 
  compare_op op ((to_num sign l),r)

let lt_vec_range = compare_op_vec_range (<) true
let gt_vec_range = compare_op_vec_range (>) true
let lteq_vec_range = compare_op_vec_range (<=) true
let gteq_vec_range = compare_op_vec_range (>=) true

let compare_op_range_vec op sign (l,r) =
  compare_op op (l, (to_num sign r))

let lt_range_vec = compare_op_range_vec (<) true
let gt_range_vec = compare_op_range_vec (>) true
let lteq_range_vec = compare_op_range_vec (<=) true
let gteq_range_vec = compare_op_range_vec (>=) true

let eq (l,r) = bool_to_bit (l = r)
let eq_range (l,r) = bool_to_bit (l = r)
let eq_vec (l,r) = bool_to_bit (l = r)
let eq_bit (l,r) = bool_to_bit (l = r)
let eq_vec_range (l,r) = eq (to_num false l,r)
let eq_range_vec (l,r) = eq (l, to_num false r)
let eq_vec_vec (l,r) = eq (to_num true l, to_num true r)

let neq (l,r) = bitwise_not_bit (eq (l,r))
let neq_bit (l,r) = bitwise_not_bit (eq_bit (l,r))
let neq_range (l,r) = bitwise_not_bit (eq_range (l,r))
let neq_vec (l,r) = bitwise_not_bit (eq_vec_vec (l,r))
let neq_vec_range (l,r) = bitwise_not_bit (eq_vec_range (l,r))
let neq_range_vec (l,r) = bitwise_not_bit (eq_range_vec (l,r))


val make_indexed_vector : forall 'a. list (integer * 'a) -> 'a -> integer -> integer -> bool -> vector 'a
let make_indexed_vector entries default start length dir =
  let length = natFromInteger length in
  Vector (List.foldl replace (replicate length default) entries) start dir

val make_bit_vector_undef : integer -> vector bitU
let make_bitvector_undef length =
  Vector (replicate (natFromInteger length) Undef) 0 true

(* let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n) *)

let mask (n,Vector bits start dir) =
  let current_size = List.length bits in
  Vector (drop (current_size - (natFromInteger n)) bits) (if dir then 0 else (n-1)) dir


let bit_of_bit_lifted = function
  | Bitl_zero -> O
  | Bitl_one  -> I
  | Bitl_undef -> Undef
  | _ -> failwith "bit_of_bit_lifted: unexpected Bitl_unknown"
end

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 : list Sail_impl_base.byte_lifted -> vector bitU
let bitv_of_byte_lifteds v =
  Vector (foldl (fun x (Byte_lifted y) -> x ++ (List.map bitU_of_bit_lifted y)) [] v) 0 true


val byte_lifteds_of_bitv : vector bitU -> list byte_lifted
let byte_lifteds_of_bitv (Vector bits length is_inc) = 
  let bits = List.map bit_lifted_of_bitU bits in
  byte_lifteds_of_bit_lifteds bits

val address_lifted_of_bitv : vector bitU -> address_lifted
let address_lifted_of_bitv v =
  Address_lifted (byte_lifteds_of_bitv v) Nothing


val bitvFromRegisterValue : register_value -> vector bitU
let bitvFromRegisterValue v =
  Vector (List.map bitU_of_bit_lifted v.rv_bits)
         (integerFromNat v.rv_start_internal)
         (v.rv_dir = D_increasing)


val registerValueFromBitv : vector bitU -> register -> register_value
let registerValueFromBitv (Vector bits start is_inc) reg = 
  let start = natFromInteger start in
  let bit_lifteds =
    List.map bit_lifted_of_bitU bits in
  <| rv_bits = bit_lifteds;
     rv_dir = dir is_inc;
     rv_start_internal = start;
     rv_start = if is_inc then start else start+1 - (size_of_reg_nat reg) |>


class (ToNatural 'a)
  val toNatural : 'a -> natural
end


instance (ToNatural integer)
  let toNatural = naturalFromInteger
end

instance (ToNatural int)
  let toNatural = naturalFromInt
end

instance (ToNatural nat)
  let toNatural = naturalFromNat
end

instance (ToNatural natural)
  let toNatural = id
end


let toNaturalFiveTup (n1,n2,n3,n4,n5) =
  (toNatural n1,
   toNatural n2,
   toNatural n3,
   toNatural n4,
   toNatural n5)


val foreach_inc :  forall 'vars. (integer * integer * integer) -> 'vars ->
                   (integer -> 'vars -> 'vars) -> 'vars
let rec foreach_inc (i,stop,by) vars body = 
  if i <= stop
  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 i >= stop
  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 to_bool b then failwith msg else ()


class (ToFromInterpValue 'a)
  val toInterpValue : 'a -> Interp.value
  val fromInterpValue : Interp.value -> 'a
end

instance (ToFromInterpValue bool)
  let toInterpValue = function
    | true -> Interp.V_lit (L_aux (L_one) Unknown)
    | false -> Interp.V_lit (L_aux (L_zero) Unknown)
    end
  let fromInterpValue = function
    | Interp.V_lit (L_aux (L_true) _)  -> true
    | Interp.V_lit (L_aux (L_false) _) -> false
    | Interp.V_lit (L_aux (L_one) _)  -> true
    | Interp.V_lit (L_aux (L_zero) _) -> false
    | _ -> failwith "fromInterpValue bool: unexpected value"
    end
end

instance (ToFromInterpValue unit)
  let toInterpValue = fun () -> Interp.V_lit (L_aux (L_unit) Unknown)
  let fromInterpValue = function
    | Interp.V_lit (L_aux (L_unit) _) -> ()
    | _ -> failwith "fromInterpValue unit: unexpected value"
    end
end

instance (ToFromInterpValue integer)
  let toInterpValue i = V_lit (L_aux (L_num i) Unknown)
  let fromInterpValue = function
    | Interp.V_lit (L_aux (L_num i) _) -> i
    | _ -> failwith "fromInterpValue integer: unexexpected value"
    end
end

instance (ToFromInterpValue string)
  let toInterpValue s = V_lit (L_aux (L_string s) Unknown)
  let fromInterpValue = function
    | Interp.V_lit (L_aux (L_string s) _) -> s
    | _ -> failwith "fromInterpValue integer: unexexpected value"
    end
end

instance (ToFromInterpValue bitU)
  let toInterpValue = function
    | I     -> Interp.V_lit (L_aux (L_one) Unknown)
    | O     -> Interp.V_lit (L_aux (L_zero) Unknown)
    | Undef -> Interp.V_lit (L_aux (L_undef) Unknown)
    end
  let fromInterpValue = function
    | Interp.V_lit (L_aux (L_one) _)   -> I
    | Interp.V_lit (L_aux (L_zero) _)  -> O
    | Interp.V_lit (L_aux (L_undef) _) -> Undef
    | _ -> failwith "fromInterpValue bitU: unexpected value"
    end
end


let tuple2ToInterpValue (a,b) =
  V_tuple [toInterpValue a;toInterpValue b]
let tuple2FromInterpValue = function
  | V_tuple [a;b] -> (fromInterpValue a,fromInterpValue b)
  | _ -> failwith "fromInterpValue a*b: unexpected value"
  end

instance forall 'a 'b. ToFromInterpValue 'a, ToFromInterpValue 'b => (ToFromInterpValue ('a * 'b))
  let toInterpValue = tuple2ToInterpValue
  let fromInterpValue = tuple2FromInterpValue
end

let tuple3ToInterpValue (a,b,c) =
  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c]
let tuple3FromInterpValue = function
  | V_tuple [a;b;c] -> (fromInterpValue a,fromInterpValue b,fromInterpValue c)
  | _ -> failwith "fromInterpValue a*b: unexpected value"
  end

instance forall 'a 'b 'c. ToFromInterpValue 'a, ToFromInterpValue 'b, ToFromInterpValue 'c => 
    (ToFromInterpValue ('a * 'b * 'c))
  let toInterpValue = tuple3ToInterpValue
  let fromInterpValue = tuple3FromInterpValue
end

let tuple4ToInterpValue (a,b,c,d) =
  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d]
let tuple4FromInterpValue = function
  | V_tuple [a;b;c;d] -> (fromInterpValue a,fromInterpValue b,
                          fromInterpValue c,fromInterpValue d)
  | _ -> failwith "fromInterpValue a*b: unexpected value"
  end

instance forall 'a 'b 'c 'd. ToFromInterpValue 'a, ToFromInterpValue 'b, 
                             ToFromInterpValue 'c, ToFromInterpValue 'd => 
    (ToFromInterpValue ('a * 'b * 'c * 'd))
  let toInterpValue = tuple4ToInterpValue
  let fromInterpValue = tuple4FromInterpValue
end

let tuple5ToInterpValue (a,b,c,d,e) =
  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;toInterpValue e]
let tuple5FromInterpValue = function
  | V_tuple [a;b;c;d;e] ->
     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
      fromInterpValue d,fromInterpValue e)
  | _ -> failwith "fromInterpValue a*b: unexpected value"
  end

instance forall 'a 'b 'c 'd 'e. 
    ToFromInterpValue 'a, ToFromInterpValue 'b, 
    ToFromInterpValue 'c, ToFromInterpValue 'd,
    ToFromInterpValue 'e =>
    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e))
  let toInterpValue = tuple5ToInterpValue
  let fromInterpValue = tuple5FromInterpValue
end


let tuple6ToInterpValue (a,b,c,d,e,f) =
  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
           toInterpValue e;toInterpValue f]
let tuple6FromInterpValue = function
  | V_tuple [a;b;c;d;e;f] ->
     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
      fromInterpValue d,fromInterpValue e,fromInterpValue f)
  | _ -> failwith "fromInterpValue a*b: unexpected value"
  end

instance forall 'a 'b 'c 'd 'e 'f.
    ToFromInterpValue 'a, ToFromInterpValue 'b, 
    ToFromInterpValue 'c, ToFromInterpValue 'd,
    ToFromInterpValue 'e, ToFromInterpValue 'f =>
    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f))
  let toInterpValue = tuple6ToInterpValue
  let fromInterpValue = tuple6FromInterpValue
end

let tuple7ToInterpValue (a,b,c,d,e,f,g) =
  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
           toInterpValue e;toInterpValue f;toInterpValue g]
let tuple7FromInterpValue = function
  | V_tuple [a;b;c;d;e;f;g] ->
     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
      fromInterpValue d,fromInterpValue e,fromInterpValue f,
      fromInterpValue g)
  | _ -> failwith "fromInterpValue a*b: unexpected value"
  end

instance forall 'a 'b 'c 'd 'e 'f 'g.
    ToFromInterpValue 'a, ToFromInterpValue 'b, 
    ToFromInterpValue 'c, ToFromInterpValue 'd,
    ToFromInterpValue 'e, ToFromInterpValue 'f,
    ToFromInterpValue 'g =>
    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g))
  let toInterpValue = tuple7ToInterpValue
  let fromInterpValue = tuple7FromInterpValue
end


let tuple8ToInterpValue (a,b,c,d,e,f,g,h) =
  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
           toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h]
let tuple8FromInterpValue = function
  | V_tuple [a;b;c;d;e;f;g;h] ->
     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
      fromInterpValue d,fromInterpValue e,fromInterpValue f,
      fromInterpValue g,fromInterpValue h)
  | _ -> failwith "fromInterpValue a*b: unexpected value"
  end

instance forall 'a 'b 'c 'd 'e 'f 'g 'h.
    ToFromInterpValue 'a, ToFromInterpValue 'b, 
    ToFromInterpValue 'c, ToFromInterpValue 'd,
    ToFromInterpValue 'e, ToFromInterpValue 'f,
    ToFromInterpValue 'g, ToFromInterpValue 'h =>
    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h))
  let toInterpValue = tuple8ToInterpValue
  let fromInterpValue = tuple8FromInterpValue
end

let tuple9ToInterpValue (a,b,c,d,e,f,g,h,i) =
  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
           toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h;
           toInterpValue i]
let tuple9FromInterpValue = function
  | V_tuple [a;b;c;d;e;f;g;h;i] ->
     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
      fromInterpValue d,fromInterpValue e,fromInterpValue f,
      fromInterpValue g,fromInterpValue h,fromInterpValue i)
  | _ -> failwith "fromInterpValue a*b: unexpected value"
  end

instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i.
    ToFromInterpValue 'a, ToFromInterpValue 'b, 
    ToFromInterpValue 'c, ToFromInterpValue 'd,
    ToFromInterpValue 'e, ToFromInterpValue 'f,
    ToFromInterpValue 'g, ToFromInterpValue 'h,
    ToFromInterpValue 'i =>
    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i))
  let toInterpValue = tuple9ToInterpValue
  let fromInterpValue = tuple9FromInterpValue
end

let tuple10ToInterpValue (a,b,c,d,e,f,g,h,i,j) =
  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
           toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h;
           toInterpValue i;toInterpValue j;]
let tuple10FromInterpValue = function
  | V_tuple [a;b;c;d;e;f;g;h;i;j] ->
     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
      fromInterpValue d,fromInterpValue e,fromInterpValue f,
      fromInterpValue g,fromInterpValue h,fromInterpValue i,
      fromInterpValue j)
  | _ -> failwith "fromInterpValue a*b: unexpected value"
  end

instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j.
    ToFromInterpValue 'a, ToFromInterpValue 'b, 
    ToFromInterpValue 'c, ToFromInterpValue 'd,
    ToFromInterpValue 'e, ToFromInterpValue 'f,
    ToFromInterpValue 'g, ToFromInterpValue 'h,
    ToFromInterpValue 'i, ToFromInterpValue 'j =>
    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j))
  let toInterpValue = tuple10ToInterpValue
  let fromInterpValue = tuple10FromInterpValue
end

let tuple11ToInterpValue (a,b,c,d,e,f,g,h,i,j,k) =
  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
           toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h;
           toInterpValue i;toInterpValue j;toInterpValue k;]
let tuple11FromInterpValue = function
  | V_tuple [a;b;c;d;e;f;g;h;i;j;k] ->
     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
      fromInterpValue d,fromInterpValue e,fromInterpValue f,
      fromInterpValue g,fromInterpValue h,fromInterpValue i,
      fromInterpValue j,fromInterpValue k)
  | _ -> failwith "fromInterpValue a*b: unexpected value"
  end

instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k.
    ToFromInterpValue 'a, ToFromInterpValue 'b, 
    ToFromInterpValue 'c, ToFromInterpValue 'd,
    ToFromInterpValue 'e, ToFromInterpValue 'f,
    ToFromInterpValue 'g, ToFromInterpValue 'h,
    ToFromInterpValue 'i, ToFromInterpValue 'j,
    ToFromInterpValue 'k =>
    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k))
  let toInterpValue = tuple11ToInterpValue
  let fromInterpValue = tuple11FromInterpValue
end


let tuple12ToInterpValue (a,b,c,d,e,f,g,h,i,j,k,l) =
  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
           toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h;
           toInterpValue i;toInterpValue j;toInterpValue k;toInterpValue l;]
let tuple12FromInterpValue = function
  | V_tuple [a;b;c;d;e;f;g;h;i;j;k;l] ->
     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
      fromInterpValue d,fromInterpValue e,fromInterpValue f,
      fromInterpValue g,fromInterpValue h,fromInterpValue i,
      fromInterpValue j,fromInterpValue k,fromInterpValue l)
  | _ -> failwith "fromInterpValue a*b: unexpected value"
  end

instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k 'l.
    ToFromInterpValue 'a, ToFromInterpValue 'b, 
    ToFromInterpValue 'c, ToFromInterpValue 'd,
    ToFromInterpValue 'e, ToFromInterpValue 'f,
    ToFromInterpValue 'g, ToFromInterpValue 'h,
    ToFromInterpValue 'i, ToFromInterpValue 'j,
    ToFromInterpValue 'k, ToFromInterpValue 'l =>
    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l))
  let toInterpValue = tuple12ToInterpValue
  let fromInterpValue = tuple12FromInterpValue
end



val listToInterpValue : forall 'a. ToFromInterpValue 'a => list 'a -> Interp.value
let listToInterpValue l = V_list (List.map toInterpValue l)

val listFromInterpValue : forall 'a. ToFromInterpValue 'a => Interp.value -> list 'a
let listFromInterpValue = function
  | V_list l -> List.map fromInterpValue l
  | _ -> failwith "fromInterpValue a*b: unexpected value"
  end

instance forall 'a. ToFromInterpValue 'a => (ToFromInterpValue (list 'a))
  let toInterpValue = listToInterpValue
  let fromInterpValue = listFromInterpValue
end


val vectorToInterpValue : forall 'a. ToFromInterpValue 'a => vector 'a -> Interp.value
let vectorToInterpValue (Vector vs start direction) =
  V_vector (natFromInteger start) (if direction then IInc else IDec) (List.map toInterpValue vs)

val vectorFromInterpValue : forall 'a. ToFromInterpValue 'a => Interp.value -> vector 'a
let vectorFromInterpValue = function
  | V_vector start direction vs ->
     Vector (List.map fromInterpValue vs) (integerFromNat start)
            (match direction with | IInc -> true | IDec -> false end)
  | V_vector_sparse start length direction valuemap defaultval ->
     make_indexed_vector
       (List.map (fun (i,v) -> (integerFromNat i,fromInterpValue v)) valuemap)
       (fromInterpValue defaultval)
       (integerFromNat start) (integerFromNat length)
       (match direction with | IInc -> true | IDec -> false end)
  | _ -> failwith "fromInterpValue a*b: unexpected value"
  end

instance forall 'a. ToFromInterpValue 'a => (ToFromInterpValue (vector 'a))
  let toInterpValue = vectorToInterpValue
  let fromInterpValue = vectorFromInterpValue
end

(* Here the type information is not accurate: instead of T_id "option" it should
   be T_app (T_id "option) (...), but temporarily we'll do it like this. The
   same thing has to be fixed in pretty_print.ml when we're generating the
   type-class instances. *)
val maybeToInterpValue : forall 'a. ToFromInterpValue 'a => maybe 'a -> Interp.value
let maybeToInterpValue = function
  | Nothing -> V_ctor (Id_aux (Id "None") Unknown) (T_id "option") C_Union (V_lit (L_aux L_unit Unknown))
  | Just a  -> V_ctor (Id_aux (Id "Some") Unknown) (T_id "option") C_Union (toInterpValue a)
  end

val maybeFromInterpValue : forall 'a. ToFromInterpValue 'a => Interp.value -> maybe 'a
let maybeFromInterpValue = function
  | V_ctor (Id_aux (Id "None") _) _ _ _ -> Nothing
  | V_ctor (Id_aux (Id "Some") _) _ _ v -> Just (fromInterpValue v)
  | _ -> failwith "fromInterpValue maybe: unexpected value"
  end

instance forall 'a. ToFromInterpValue 'a => (ToFromInterpValue (maybe 'a))
  let toInterpValue = maybeToInterpValue
  let fromInterpValue = maybeFromInterpValue
end