Use sail_lib.lem values in C backend

Rather than just using strings to represent literals, now use value
types from sail_lib.lem to represent them. This allows for expressions
to be evaluated at compile time, which will be useful for future
optimisations involving constant folding and propagation, and allows
the intermediate bytecode to be interpreted using the same lem
builtins that the shallow embedding uses.

To get this to work I had to tweak the build process slightly to allow
ml files to import lem files from gen_lib/. Hopefully this doesn't
break anything!

2 files changed, 7 insertions, 1489 deletions

diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 4d67cbfc..fce595e0 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -108,6 +108,12 @@ let showBitU = function
   | BU -> "U"
 end
 
+let bitU_char = function
+  | B0 -> #'0'
+  | B1 -> #'1'
+  | BU -> #'?'
+end
+
 instance (Show bitU)
   let show = showBitU
 end
@@ -307,7 +313,7 @@ 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
+  | Nothing -> toString (#'0' :: #'b' :: map bitU_char bs)
   end
 
 (*** List operations *)
diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml
deleted file mode 100644
index 213acea1..00000000
--- a/src/gen_lib/sail_values.ml
+++ /dev/null
@@ -1,1488 +0,0 @@
-open Big_int_Z
-open Printf
-
-let trace_writes = ref false
-let tracef = printf
-
-(* only expected to be 0, 1, 2; 2 represents undef *)
-type vbit = Vone | Vzero | Vundef
-type number = Big_int_Z.big_int
-
-type _bool = vbit
-type _string = string
-type _nat = number
-type _int = number
-
-let undef_val = ref Vundef
-
-type value =
-  | Vvector of vbit array * int * bool
-  | VvectorR of value array * int * bool
-  | Vregister of vbit array ref * int * bool * string * (string * (int * int)) list
-  | Vbit of vbit (*Mostly for Vundef in place of undefined register place holders*)
-
-exception Sail_exit
-exception Sail_return
-
-let _print s = print_string s
-
-let string_of_bit = function 
-  | Vone   -> "1"
-  | Vzero  -> "0"
-  | Vundef -> "u"
-
-let bit_of_string = function
-  | "1" -> Vone
-  | "0" -> Vzero
-  | "u" -> Vundef
-  | _ -> failwith "invalid bit value"
-
-let string_of_bit_array a = Array.fold_left (^) "" (Array.map string_of_bit a) 
-
-let string_of_value = function
-  | Vvector(bits, start, inc)  -> (string_of_int start) ^ (if inc then "inc" else "dec") ^ (string_of_bit_array bits)
-  | VvectorR(values, start, inc) -> ""
-  | Vregister(bits, start, inc, name, fields) -> "reg" ^ (string_of_int start) ^ (if inc then "inc" else "dec") ^ (string_of_bit_array !bits)
-  | Vbit(b) -> string_of_bit b
-
-let to_bool = function
-  | Vzero -> false
-  | Vone  -> true
-  | Vundef -> assert false
-
-let is_one i =
-  if eq_big_int i unit_big_int
-  then Vone
-  else Vzero
-
-
-let exit _ = raise Sail_exit
-
-
-let is_one_int i =
-  if i = 1 then Vone else Vzero
-
-let get_barray  = function
-  | Vvector(a,_,_) -> a
-  | Vregister(a,_,_,_,_) -> !a
-  | _ -> assert false
-
-let get_varray = function
-  | VvectorR(a,_,_) -> a
-  | _ -> assert false
-
-let get_ord = function
-  | Vvector(_,_,o) | Vregister(_,_,o,_,_) | VvectorR(_,_,o) -> o
-  | _ -> assert false  
-
-let get_start = function
-  | Vvector(_,s,o) | Vregister(_,s,o,_,_) | VvectorR(_,s,o) -> s
-  | _ -> assert false  
-  
-let set_start i = function
-  | Vvector(a,start,dir) -> Vvector(a,i,dir)
-  | Vregister(bits,start,dir,name,regfields) -> Vregister(bits,i,dir,name,regfields)
-  | VvectorR(a,start,dir) -> VvectorR(a,i,dir)
-  | _ -> assert false  
-
-let length_int = function
-  | Vvector(array,_,_) -> Array.length array
-  | Vregister(array,_,_,_,_) -> Array.length !array
-  | VvectorR(array,_,_) -> Array.length array
-  | _ -> assert false
-  
-let set_start_to_length v = set_start ((length_int v)-1) v (* XXX should take account of direction? *)
-
-let length_big v = big_int_of_int (length_int v)
-let length = length_big
-
-let read_register = function
-  | Vregister(a,start,inc,_,_) -> Vvector(!a,start,inc)
-  | v -> v
-
-let vector_access_int v n = 
-  match v with
-  | VvectorR(array,start,is_inc) ->
-    if is_inc
-    then (array.(n-start))
-    else (array.(start-n))
-  | _ -> assert false
-
-let vector_access_big v n = vector_access_int v (int_of_big_int n)
-
-let vector_access = vector_access_big
-
-let bit_vector_access_int v n = match v with
-  | Vvector(array,start,is_inc) ->
-    if is_inc
-    then array.(n-start)
-    else array.(start-n)
-  | Vregister(array,start,is_inc,_,_) ->
-    if is_inc
-    then !array.(n-start)
-    else !array.(start-n)
-  | _ -> assert false
-
-let bit_vector_access_big v n = bit_vector_access_int v (int_of_big_int n)
-let bit_vector_access = bit_vector_access_big
-
-let vector_subrange_int v n m =
-  (*Printf.printf "vector_subrange %s %d %d\n" (string_of_value v) n m;*)
-  match v with
-  | VvectorR(array,start,is_inc) ->
-    let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
-    VvectorR(Array.sub array offset length,n,is_inc)
-  | Vvector(array,start,is_inc) ->
-    let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
-    Vvector(Array.sub array offset length,n,is_inc)
-  | Vregister(array,start,is_inc,name,fields) ->
-    let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
-    Vvector(Array.sub !array offset length,n,is_inc)
-  | _ -> v
-
-let vector_subrange_big v n m = vector_subrange_int v (int_of_big_int n) (int_of_big_int m)
-let vector_subrange = vector_subrange_big
-
-let get_register_field_vec reg field =
-  match reg with
-  | Vregister(_,_,_,name,fields) ->
-    (match List.assoc field fields with
-     | (i,j) ->
-       if i = j
-       then Vbit Vundef
-       else vector_subrange_int reg i j)
-  | _ -> Vbit Vundef
-
-let get_register_field_bit reg field =
-  match reg with
-  | Vregister(_,_,_,name,fields) ->
-    (match List.assoc field fields with
-     | (i,j) ->
-       if i = j
-       then bit_vector_access_int reg i
-       else Vundef)
-  | _ -> Vundef
-
-let set_register register value = match register,value with
-  | Vregister(a,_,_,name,_), Vregister(new_v,_,_,_,_) -> 
-     begin
-       if !trace_writes then
-         tracef "%s <- %s\n" name (string_of_value value);
-       a := !new_v
-     end
-  | Vregister(a,_,_,name,_), Vvector(new_v,_,_) ->
-     begin
-       if !trace_writes then
-         tracef "%s <- %s\n" name (string_of_value value);
-       a := new_v
-     end
-  | _ -> failwith "set_register of non-register"
-
-let set_vector_subrange_vec_int v n m new_v =
-  let walker array length offset new_values =
-    begin
-      for x = 0 to length-1
-      do array.(x+offset) <- new_values.(x) 
-      done;
-    end
-  in
-  match v, new_v with
-  | VvectorR(array,start,is_inc),VvectorR(new_v,_,_) ->
-    let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
-    walker array length offset new_v
-  | _ -> ()
-
-let set_vector_subrange_vec_big v n m new_v =
-  set_vector_subrange_vec_int v (int_of_big_int n) (int_of_big_int m) new_v
-let set_vector_subrange_vec = set_vector_subrange_vec_big (* or maybe _int *)
-
-let set_vector_subrange_bit_int v n m new_v =
-  let walker array length offset new_values =
-    begin
-      for x = 0 to length-1
-      do array.(x+offset) <- new_values.(x) 
-      done;
-    end
-  in
-  match v,new_v with
-  | Vvector(array,start,is_inc),Vvector(new_v,_,_) ->
-    let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
-    walker array length offset new_v
-  | Vregister(array,start,is_inc,name,fields),Vvector(new_v,_,_) ->
-    let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
-    walker !array length offset new_v
-  | _ -> ()
-
-let set_vector_subrange_bit_big v n m new_v =
-  set_vector_subrange_bit_int v (int_of_big_int n) (int_of_big_int m) new_v
-let set_vector_subrange_bit = set_vector_subrange_bit_big
-
-let set_register_bit_int reg n v = 
-  match reg with
-  | Vregister(array,start,inc,name,fields) ->
-     begin
-       if !trace_writes then
-         tracef "%s[%d] <- %s\n" name n (string_of_bit v);
-       (!array).(if inc then (n - start) else (start - n)) <- v
-     end
-  | _ -> failwith "set_register_bit of non-register"
-let set_register_bit_big reg n v = set_register_bit_int reg (int_of_big_int n) v
-let set_register_bit = set_register_bit_big
-
-let set_register_field_v reg field new_v =
-  match reg with
-  | Vregister(array,start,dir,name,fields) ->
-     begin
-       if !trace_writes then
-         tracef "%s[%s] <- %s\n" name field (string_of_value new_v);
-    (match List.assoc field fields with
-     | (i,j) ->
-       if i = j
-       then ()
-       else set_vector_subrange_bit_int reg i j new_v)
-     end
-  | _ -> ()
-
-let set_register_field_bit reg field new_v =
-  match reg with
-  | Vregister(array,start,dir,name,fields) ->
-     begin
-       if !trace_writes then
-         tracef "%s.%s <- %s\n" name field (string_of_bit new_v);
-    (match List.assoc field fields with
-     | (i,j) ->
-       if i = j
-       then !array.(if dir then i - start else start - i) <- new_v
-       else ())
-     end
-  | _ -> ()
-
-let set_two_reg r1 r2 vec =
-  let size = length_int r1 in
-  let dir = get_ord r1 in
-  let start = get_start vec in
-  let vsize = length_int vec in
-  let r1_v = vector_subrange_int vec start ((if dir then size - start else start - size) - 1) in
-  let r2_v = vector_subrange_int vec (if dir then size - start else start - size)
-      (if dir then vsize - start else start - vsize) in
-  begin set_register r1 r1_v; set_register r2 r2_v end
-  
-
-let make_indexed_v entries default start size dir =
-  let default_value = match default with
-    | None -> Vbit Vundef
-    | Some v -> v in
-  let array = Array.make size default_value in
-  begin
-    List.iter (fun (i,v) -> array.(if dir then start - i else i - start) <- v) entries;
-    VvectorR(array, start, dir)
-  end
-
-let make_indexed_v_big entries default start size dir =
-  make_indexed_v entries default (int_of_big_int start) (int_of_big_int size) dir
-
-let make_indexed_bitv entries default start size dir =
-  let default_value = match default with
-    | None -> Vundef
-    | Some v -> v in
-  let array = Array.make size default_value in
-  begin
-    List.iter (fun (i,v) -> array.(if dir then start - i else i - start) <- v) entries;
-    Vvector(array, start, dir)
-  end
-
-let make_indexed_bitv_big entries default start size dir =
-  make_indexed_bitv entries default (int_of_big_int start) (int_of_big_int size) dir
-
-let vector_concat l r =
-  match l,r with
-  | Vvector(arrayl,start,ord), Vvector(arrayr,_,_) ->
-    Vvector(Array.append arrayl arrayr, start, ord)
-  | Vvector(arrayl,start,ord), Vregister(arrayr,_,_,_,_) ->
-    Vvector(Array.append arrayl !arrayr, start,ord)
-  | Vregister(arrayl,start,ord,_,_), Vvector(arrayr,_,_) ->
-    Vvector(Array.append !arrayl arrayr, start, ord)
-  | Vregister(arrayl,start,ord,_,_), Vregister(arrayr,_,_,_,_) ->
-    Vvector(Array.append !arrayl !arrayr,start,ord)
-  | VvectorR(arrayl,start,ord),VvectorR(arrayr,_,_) ->
-    VvectorR(Array.append arrayl arrayr, start,ord)
-  | _ -> Vbit Vundef
-
-let has_undef = function
-  | Vvector(array,_,_) ->
-    let rec foreach i = (* XXX ideally would use Array.mem but not in ocaml 4.02.3 *)
-      if i < Array.length array
-      then
-        if array.(i) = Vundef then true
-        else foreach (i+1)
-      else false in
-    foreach 0
-  | Vregister(array,_,_,_,_) ->
-    let array = !array in
-    let rec foreach i =
-      if i < Array.length array
-      then
-        if array.(i) = Vundef then true
-        else foreach (i+1)
-      else false in
-    foreach 0
-  | _ -> false
-
-let most_significant = function
-  | Vvector(array,_,_) -> array.(0)
-  | Vregister(array,_,_,_,_) -> !array.(0)
-  | _ -> assert false
-
-let _most_significant = most_significant
-
-let bitwise_not_bit = function
-  | Vone -> Vzero
-  | Vzero -> Vone
-  | _ -> Vundef
-
-let bitwise_not = function
-  | Vvector(array,s,d)-> Vvector( Array.map bitwise_not_bit array,s,d)
-  | Vregister(array,s,d,_,_) -> Vvector( Array.map bitwise_not_bit !array,s,d)
-  | _ -> assert false 
-
-let bool_to_bit b = if b then Vone else Vzero
-
-let bitwise_binop_bit op (l,r) =
-  match l,r with
-  | Vundef,_ | _,Vundef -> Vundef (*Do we want to do this or to respect | of One and & of Zero rules?*)
-  | Vone,Vone -> bool_to_bit (op true true)
-  | Vone,Vzero -> bool_to_bit (op true false)
-  | Vzero,Vone -> bool_to_bit (op false true)
-  | Vzero,Vzero -> bool_to_bit (op false false)
-
-let bitwise_and_bit = bitwise_binop_bit (&&)
-let bitwise_or_bit = bitwise_binop_bit (||)
-let bitwise_xor_bit = bitwise_binop_bit (<>)
-
-let bitwise_binop op (l,r) =
-  let bop l arrayl arrayr =
-    let array = Array.make l Vzero in
-    begin
-      for i = 0 to (l-1) do
-        array.(i) <- bitwise_binop_bit op (arrayl.(i), arrayr.(i))
-      done;
-      array
-    end in
-  match l,r with
-  | Vvector(arrayl, start, dir), Vvector(arrayr,_,_) ->
-    Vvector(bop (Array.length arrayl) arrayl arrayr, start,dir)
-  | Vvector(arrayl, start, dir), Vregister(arrayr,_,_,_,_) ->
-    Vvector(bop (Array.length arrayl) arrayl !arrayr, start, dir)
-  | Vregister(arrayl, start,dir,_,_), Vvector(arrayr,_,_) ->
-    Vvector(bop (Array.length arrayr) !arrayl arrayr, start,dir)
-  | Vregister(arrayl, start, dir, _, _), Vregister(arrayr,_,_,_,_) ->
-    Vvector(bop (Array.length !arrayl) !arrayl !arrayr, start,dir)
-  | _ -> Vbit Vundef
-
-let bitwise_and = bitwise_binop (&&)
-let bitwise_or = bitwise_binop (||)
-let bitwise_xor = bitwise_binop (<>)
-
-let rec power_int base raiseto =
-  if raiseto = 0
-  then 1
-  else base * (power_int base (raiseto - 1))
-
-let int_of_bit_array array = 
-  let acc = ref 0 in
-  let len = Array.length array in
-  begin 
-    for i = 0 to len - 1 do
-      acc := (!acc) lsl 1;
-      match array.(i) with
-      | Vone -> acc := succ (!acc)
-      | _ -> ()
-    done;
-    !acc
-  end
-
-let unsigned_int = function
-  | (Vvector(array,_,_) as v) ->
-    if has_undef v
-    then assert false
-    else int_of_bit_array array
-  | (Vregister(array,_,_,_,_) as v)->
-    let array = !array in
-    if has_undef v
-    then assert false
-    else int_of_bit_array array
-  | _ -> assert false
-
-let big_int_of_bit_array array = 
-  let acc = ref zero_big_int in
-  let len = Array.length array in
-  begin 
-    for i = 0 to len - 1 do
-      acc := shift_left_big_int !acc 1;
-      match array.(i) with
-      | Vone -> acc := succ_big_int !acc
-      | _ -> ();
-    done;
-    !acc
-  end
-
-let unsigned_big = function
-  | (Vvector(array,_,_) as v) ->
-    if has_undef v
-    then assert false
-    else
-      big_int_of_bit_array array
-  | (Vregister(array,_,_,_,_) as v)->
-    let array = !array in
-    if has_undef v
-    then assert false
-    else
-      big_int_of_bit_array array
-  | _ -> assert false
-
-let unsigned = unsigned_big
-
-let signed_int v =
-  match most_significant v with
-  | Vone -> -(1 + (unsigned_int (bitwise_not v)))
-  | Vzero -> unsigned_int v
-  | _ -> assert false
-
-let signed_big v =
-  match most_significant v with
-  | Vone -> minus_big_int(add_int_big_int 1 (unsigned_big (bitwise_not v)))
-  | Vzero -> unsigned_big v
-  | _ -> assert false
-
-let signed = signed_big
-
-let to_num_int sign = if sign then signed_int else unsigned_int
-let to_num_big sign = if sign then signed_big else unsigned_big
-let to_num = to_num_big
-
-let two_big_int = big_int_of_int 2
-let max_64u = pred_big_int (power_big two_big_int (big_int_of_int 64))
-let max_64  = pred_big_int (power_big two_big_int (big_int_of_int 63))
-let min_64  = minus_big_int (power_big two_big_int (big_int_of_int 63))
-let max_32u = big_int_of_int 4294967295
-let max_32  = big_int_of_int 2147483647
-let min_32  = big_int_of_int (-2147483648)
-let max_8   = big_int_of_int 127
-let min_8   = big_int_of_int (-128)
-let max_5   = big_int_of_int 31
-
-let get_max_representable_in sign n = 
-  match (sign, n) with
-  | (true, 64)  -> max_64
-  | (false, 64) -> max_64u
-  | (true, 32)  -> max_32
-  | (false, 32) -> max_32u
-  | (true, 8)   -> max_8
-  | (false, 5)  -> max_5
-  | (true, _)   -> pred_big_int (power_big two_big_int (big_int_of_int (n-1)))
-  | (false, _)  -> pred_big_int (power_big two_big_int (big_int_of_int n))
-
-let get_min_representable_in sign n = 
-  match (sign, n) with
-  | (false, _)  -> zero_big_int
-  | (true, 64)  -> min_64
-  | (true, 32)  -> min_32
-  | (true, 8)   -> min_8
-  | (true, _)   -> minus_big_int (power_big two_big_int (big_int_of_int (n-1)))
-
-let to_vec_int ord len n =
-  let array = Array.make len Vzero in
-  let start = if ord then 0 else len-1 in
-  let acc = ref n in
-  for i = (len - 1) downto 0 do
-    if ((!acc) land 1) = 1 then
-      array.(i) <- Vone;
-    acc := (!acc) asr 1
-  done;
-  Vvector(array, start, ord)
-
-let to_vec_big ord len n =
-  let len = int_of_big_int len in
-  let array = Array.make len Vzero in
-  let start = if ord then 0 else len-1 in
-  if eq_big_int n zero_big_int
-  then Vvector(array, start, ord)
-  else
-    begin
-      for i = 0 to len - 1 do
-        if ((extract_big_int n (len - 1 - i) 1) == unit_big_int) then
-          array.(i) <- Vone
-      done;
-      Vvector(array, start, ord)
-    end
-
-let to_vec_inc_int (len,n) = to_vec_int true len n
-let to_vec_dec_int (len,n) = to_vec_int false len n
-
-let to_vec_inc_big (len,n) = to_vec_big true len n
-let to_vec_dec_big (len,n) = to_vec_big false len n
-
-let to_vec_inc = to_vec_inc_big
-let to_vec_dec = to_vec_dec_big
-
-let to_vec_undef_int ord len = 
-  let array = Array.make len !undef_val in
-  let start = if ord then 0 else len-1 in
-  Vvector(array, start, ord)
-
-let to_vec_undef_big ord len = 
-  let len = int_of_big_int len in
-  let array = Array.make len !undef_val in
-  let start = if ord then 0 else len-1 in
-  Vvector(array, start, ord)
-
-let to_vec_inc_undef_int len = to_vec_undef_int true len
-let to_vec_dec_undef_int len = to_vec_undef_int false len
-
-let to_vec_inc_undef_big len = to_vec_undef_big true len
-let to_vec_dec_undef_big len = to_vec_undef_big false len
-
-let to_vec_inc_undef = to_vec_inc_undef_big
-let to_vec_dec_undef = to_vec_dec_undef_big
-
-let exts_int (len, vec) = 
-  let barray = get_barray(vec) in
-  let vlen = Array.length barray in
-  let arr = 
-    if (vlen < len) then
-      (* copy most significant bit into new bits *)
-      Array.append (Array.make (len - vlen) barray.(0)) barray
-    else
-      (* truncate to least significant bits *)
-      Array.sub barray (vlen - len) len in
-  let inc = get_ord vec in
-  Vvector(arr, (if inc then 0 else (len - 1)), inc)
-
-let extz_int (len, vec) = 
-  let barray = get_barray(vec) in
-  let vlen = Array.length barray in
-  let arr = 
-    if (vlen < len) then
-      (* fill new bits with zero *)
-      Array.append (Array.make (len - vlen) Vzero) barray
-    else
-      (* truncate to least significant bits *)
-      Array.sub barray (vlen - len) len in
-  let inc = get_ord vec in
-  Vvector(arr, (if inc then 0 else (len - 1)), inc)
-
-let exts_big (len,vec) = exts_int (int_of_big_int len, vec)
-let extz_big (len,vec) = extz_int (int_of_big_int len, vec)
-
-let exts = exts_big
-let extz = extz_big
-
-let arith_op op (l,r) = op l r
-let add_big = arith_op add_big_int
-let add_signed_big = arith_op add_big_int
-let minus_big = arith_op sub_big_int
-let multiply_big = arith_op mult_big_int
-let min_big = arith_op min_big_int
-let max_big = arith_op max_big_int
-(* NB Z.div is what we want because it does truncation towards zero unlike Big_int_Z.div_big_int == Z.ediv *)
-let quot_big = arith_op (Z.div)
-let modulo_big = arith_op (Z.rem)
-
-let power_big = arith_op power_big
-
-let add_int = arith_op (+)
-let add_signed_int = arith_op (+)
-let minus_int = arith_op (-)
-let multiply_int = arith_op ( * )
-let modulo_int = arith_op (mod)
-let quot_int = arith_op (/)
-
-let power_int = arith_op power_int
-
-let add        = add_big
-let add_signed = add_signed_big
-let minus      = minus_big
-let multiply   = multiply_big
-let modulo     = modulo_big
-let quot       = quot_big
-let power      = power_big
-let min_int    = min (* the built-in version *)
-let min        = min_big (* is overwritten here *)
-let max_int    = max (* likewise *)
-let max        = max_big
-let abs_int    = abs
-let abs_big    = abs_big_int
-let abs        = abs_big
-
-let arith_op_vec_big op sign size (l,r) =
-  let ord = get_ord l in
-  let (l',r') = to_num_big sign l, to_num_big sign r in
-  let n = arith_op op (l',r') in
-  to_vec_big ord (mult_big_int size (length_big l)) n
-
-let add_vec_big = arith_op_vec_big add_big_int false unit_big_int
-let add_vec_signed_big = arith_op_vec_big add_big_int true unit_big_int
-let minus_vec_big = arith_op_vec_big sub_big_int false unit_big_int
-let multiply_vec_big = arith_op_vec_big mult_big_int false two_big_int
-let multiply_vec_signed_big = arith_op_vec_big mult_big_int true two_big_int
-
-let arith_op_vec_int op sign size (l,r) =
-  let ord = get_ord l in
-  let (l',r') = to_num_int sign l, to_num_int sign r in
-  let n = arith_op op (l',r') in
-  to_vec_int ord (size * (length_int l)) n
-
-let add_vec_int = arith_op_vec_int (+) false 1
-let add_vec_signed_int = arith_op_vec_int (+) true 1
-let minus_vec_int = arith_op_vec_int (-) false 1
-let multiply_vec_int = arith_op_vec_int ( * ) false 2
-let multiply_vec_signed_int = arith_op_vec_int ( * ) true 2
-
-let add_vec             = add_vec_big            
-let add_vec_signed      = add_vec_signed_big     
-let minus_vec           = minus_vec_big          
-let multiply_vec        = multiply_vec_big       
-let multiply_vec_signed = multiply_vec_signed_big
-
-
-let arith_op_vec_range_int op sign size (l,r) =
-  let ord = get_ord l in
-  arith_op_vec_int op sign size (l, to_vec_int ord (length_int l) r)
-
-let add_vec_range_int = arith_op_vec_range_int (+) false 1
-let add_vec_range_signed_int = arith_op_vec_range_int (+) true 1
-let minus_vec_range_int = arith_op_vec_range_int (-) false 1
-let mult_vec_range_int = arith_op_vec_range_int ( * ) false 2
-let mult_vec_range_signed_int = arith_op_vec_range_int ( * ) true 2
-
-let arith_op_vec_range_big op sign size (l,r) =
-  let ord = get_ord l in
-  arith_op_vec_big op sign size (l, to_vec_big ord (length_big l) r)
-
-let add_vec_range_big         = arith_op_vec_range_big add_big_int false unit_big_int
-let add_vec_range_signed_big  = arith_op_vec_range_big add_big_int true unit_big_int
-let minus_vec_range_big       = arith_op_vec_range_big sub_big_int false unit_big_int
-let mult_vec_range_big        = arith_op_vec_range_big mult_big_int false two_big_int
-let mult_vec_range_signed_big = arith_op_vec_range_big mult_big_int true two_big_int
-
-let add_vec_range         = add_vec_range_big        
-let add_vec_range_signed  = add_vec_range_signed_big 
-let minus_vec_range       = minus_vec_range_big      
-let mult_vec_range        = mult_vec_range_big       
-let mult_vec_range_signed = mult_vec_range_signed_big
-
-let arith_op_range_vec_int op sign size (l,r) =
-  let ord = get_ord r in
-  arith_op_vec_int op sign size ((to_vec_int ord (length_int r) l), r)
-
-let add_range_vec_int = arith_op_range_vec_int (+) false 1
-let add_range_vec_signed_int = arith_op_range_vec_int (+) true 1
-let minus_range_vec_int = arith_op_range_vec_int (-) false 1
-let mult_range_vec_int = arith_op_range_vec_int ( * ) false 2
-let mult_range_vec_signed_int = arith_op_range_vec_int ( * ) true 2
-
-let arith_op_range_vec_big op sign size (l,r) =
-  let ord = get_ord r in
-  arith_op_vec_big op sign size ((to_vec_big ord (length_big r) l), r)
-
-let add_range_vec_big         = arith_op_range_vec_big add_big_int false unit_big_int
-let add_range_vec_signed_big  = arith_op_range_vec_big add_big_int true unit_big_int
-let minus_range_vec_big       = arith_op_range_vec_big sub_big_int false unit_big_int
-let mult_range_vec_big        = arith_op_range_vec_big mult_big_int false two_big_int
-let mult_range_vec_signed_big = arith_op_range_vec_big mult_big_int true two_big_int
-
-let add_range_vec         = add_range_vec_big         
-let add_range_vec_signed  = add_range_vec_signed_big  
-let minus_range_vec       = minus_range_vec_big       
-let mult_range_vec        = mult_range_vec_big        
-let mult_range_vec_signed = mult_range_vec_signed_big 
-
-
-let arith_op_range_vec_range_int op sign (l,r) = arith_op op (l, to_num_int sign r)
-
-let add_range_vec_range_int = arith_op_range_vec_range_int (+) false
-let add_range_vec_range_signed_int = arith_op_range_vec_range_int (+) true
-let minus_range_vec_range_int = arith_op_range_vec_range_int (-) false
-
-let arith_op_range_vec_range_big op sign (l,r) = arith_op op (l, to_num_big sign r)
-
-let add_range_vec_range_big = arith_op_range_vec_range_big add_big_int false
-let add_range_vec_range_signed_big = arith_op_range_vec_range_big add_big_int true
-let minus_range_vec_range_big = arith_op_range_vec_range_big sub_big_int false
-
-let add_range_vec_range        = add_range_vec_range_big       
-let add_range_vec_range_signed = add_range_vec_range_signed_big 
-let minus_range_vec_range      = minus_range_vec_range_big     
-
-let arith_op_vec_range_range_int op sign (l,r) = arith_op op (to_num_int sign l,r)
-
-let add_vec_range_range_int = arith_op_vec_range_range_int (+) false
-let add_vec_range_range_signed_int = arith_op_vec_range_range_int (+) true
-let minus_vec_range_range_int = arith_op_vec_range_range_int (-) false
-
-let arith_op_vec_range_range_big op sign (l,r) = arith_op op (to_num_big sign l,r)
-
-let add_vec_range_range_big = arith_op_vec_range_range_big add_big_int false
-let add_vec_range_range_signed_big = arith_op_vec_range_range_big add_big_int true
-let minus_vec_range_range_big = arith_op_vec_range_range_big sub_big_int false
-
-let add_vec_range_range        = add_vec_range_range_big        
-let add_vec_range_range_signed = add_vec_range_range_signed_big 
-let minus_vec_range_range      = minus_vec_range_range_big      
-
-
-let arith_op_vec_vec_range_int op sign (l,r) = 
-  let (l',r') = (to_num_int sign l,to_num_int sign r) in
-  arith_op op (l',r')
-
-let add_vec_vec_range_int        = arith_op_vec_vec_range_int (+) false
-let add_vec_vec_range_signed_int = arith_op_vec_vec_range_int (+) true
-
-let arith_op_vec_vec_range_big op sign (l,r) = 
-  let (l',r') = (to_num_big sign l,to_num_big sign r) in
-  arith_op op (l',r')
-
-let add_vec_vec_range_big = arith_op_vec_vec_range_big add_big_int false
-let add_vec_vec_range_signed_big = arith_op_vec_vec_range_big add_big_int true
-
-let add_vec_vec_range        = add_vec_vec_range_big       
-let add_vec_vec_range_signed = add_vec_vec_range_signed_big
-
-let arith_op_vec_bit_int op sign (l,r) =
-  let ord = get_ord l in
-  let l' = to_num_int sign l in
-  let n = arith_op op (l', match r with | Vone -> 1 | _ -> 0) in
-  to_vec_int ord (length_int l) n
-    
-let add_vec_bit_int = arith_op_vec_bit_int (+) false
-let add_vec_bit_signed_int = arith_op_vec_bit_int (+) true 
-let minus_vec_bit_int = arith_op_vec_bit_int (-) true
-
-let arith_op_vec_bit_big op sign (l,r) =
-  let ord = get_ord l in
-  let l' = to_num_big sign l in
-  let n = arith_op op (l', match r with | Vone -> unit_big_int | _ -> zero_big_int) in
-  to_vec_big ord (length_big l) n
-    
-let add_vec_bit_big = arith_op_vec_bit_big add_big_int false 
-let add_vec_bit_signed_big = arith_op_vec_bit_big add_big_int true
-let minus_vec_bit_big = arith_op_vec_bit_big sub_big_int true
-
-let add_vec_bit        = add_vec_bit_big       
-let add_vec_bit_signed = add_vec_bit_signed_big
-let minus_vec_bit      = minus_vec_bit_big     
-
-
-let rec arith_op_overflow_vec_int op sign size (l,r) =
-  let ord = get_ord l in
-  let len = length_int l in
-  let act_size = len * size in
-  let (l_sign,r_sign) = (to_num_int sign l,to_num_int sign r) in
-  let (l_unsign,r_unsign) = (to_num_int false l,to_num_int false r) in
-  let n = arith_op op (l_sign,r_sign) in
-  let n_unsign = arith_op op (l_unsign,r_unsign) in
-  let correct_size_num = to_vec_int ord act_size n in
-  let one_more_size_u = to_vec_int ord (act_size +1) n_unsign in
-  let overflow = if (n <= (int_of_big_int (get_max_representable_in sign len))) &&
-                    (n >= (int_of_big_int (get_min_representable_in sign len)))
-    then Vzero
-    else Vone in
-  let c_out = most_significant one_more_size_u in
-  (correct_size_num,overflow,c_out)
-
-let add_overflow_vec_int = arith_op_overflow_vec_int (+) false 1
-let add_overflow_vec_signed_int = arith_op_overflow_vec_int (+) true 1
-let minus_overflow_vec_int = arith_op_overflow_vec_int (-) false 1
-let minus_overflow_vec_signed_int = arith_op_overflow_vec_int (-) true 1
-let mult_overflow_vec_int = arith_op_overflow_vec_int ( * ) false 2
-let mult_overflow_vec_signed_int = arith_op_overflow_vec_int ( * ) true 2
-
-let rec arith_op_overflow_vec_big op sign size (l,r) =
-  let ord = get_ord l in
-  let len = length_big l in
-  let act_size = mult_big_int len size in
-  let (l_sign,r_sign) = (to_num_big sign l,to_num_big sign r) in
-  let (l_unsign,r_unsign) = (to_num_big false l,to_num_big false r) in
-  let n = arith_op op (l_sign,r_sign) in
-  let n_unsign = arith_op op (l_unsign,r_unsign) in
-  let correct_size_num = to_vec_big ord act_size n in
-  let one_more_size_u = to_vec_big ord (succ_big_int act_size) n_unsign in
-  let overflow = if (le_big_int n (get_max_representable_in sign (int_of_big_int len))) &&
-                    (ge_big_int n (get_min_representable_in sign (int_of_big_int len)))
-    then Vzero
-    else Vone in
-  let c_out = most_significant one_more_size_u in
-  (correct_size_num,overflow,c_out)
-
-let add_overflow_vec_big = arith_op_overflow_vec_big add_big_int false unit_big_int
-let add_overflow_vec_signed_big = arith_op_overflow_vec_big add_big_int true unit_big_int
-let minus_overflow_vec_big = arith_op_overflow_vec_big sub_big_int false unit_big_int
-let minus_overflow_vec_signed_big = arith_op_overflow_vec_big sub_big_int true unit_big_int
-let mult_overflow_vec_big = arith_op_overflow_vec_big mult_big_int false two_big_int
-let mult_overflow_vec_signed_big = arith_op_overflow_vec_big mult_big_int true two_big_int
-
-let add_overflow_vec          = add_overflow_vec_big          
-let add_overflow_vec_signed   = add_overflow_vec_signed_big   
-let minus_overflow_vec        = minus_overflow_vec_big        
-let minus_overflow_vec_signed = minus_overflow_vec_signed_big 
-let mult_overflow_vec         = mult_overflow_vec_big         
-let mult_overflow_vec_signed  = mult_overflow_vec_signed_big  
-
-let rec arith_op_overflow_vec_bit_int op sign (l,r_bit) =
-  let ord = get_ord l in
-  let act_size = length_int l in
-  let l' = to_num_int sign l in
-  let l_u = to_num_int false l in
-  let (n,nu,changed) = match r_bit with
-    | Vone -> (arith_op op (l',1), arith_op op (l_u,1), true)
-    | Vzero -> (l',l_u,false)
-    | _ -> assert false
-  in
-  let correct_size_num = to_vec_int ord act_size n in
-  let one_larger = to_vec_int ord (1+ act_size) nu in
-  let overflow =
-    if changed 
-    then if (n <= (int_of_big_int (get_max_representable_in sign act_size))) &&
-            (n >= (int_of_big_int (get_min_representable_in sign act_size)))
-      then Vzero
-      else Vone 
-    else Vone in
-        (correct_size_num,overflow,most_significant one_larger)
-
-let add_overflow_vec_bit_signed_int = arith_op_overflow_vec_bit_int (+) true 
-let minus_overflow_vec_bit_int = arith_op_overflow_vec_bit_int (-) false 
-let minus_overflow_vec_bit_signed_int = arith_op_overflow_vec_bit_int (-) true
-
-let rec arith_op_overflow_vec_bit_big op sign (l,r_bit) =
-  let ord = get_ord l in
-  let act_size = length_big l in
-  let l' = to_num_big sign l in
-  let l_u = to_num_big false l in
-  let (n,nu,changed) = match r_bit with
-    | Vone -> (arith_op op (l',unit_big_int), arith_op op (l_u,unit_big_int), true)
-    | Vzero -> (l',l_u,false)
-    | _ -> assert false
-  in
-  let correct_size_num = to_vec_big ord act_size n in
-  let one_larger = to_vec_big ord (succ_big_int act_size) nu in
-  let overflow =
-    if changed 
-    then if (le_big_int n (get_max_representable_in sign (int_of_big_int act_size))) &&
-            (ge_big_int n (get_min_representable_in sign (int_of_big_int act_size)))
-      then Vzero
-      else Vone 
-    else Vone in
-        (correct_size_num,overflow,most_significant one_larger)
-
-let add_overflow_vec_bit_signed_big = arith_op_overflow_vec_bit_big add_big_int true
-let minus_overflow_vec_bit_big = arith_op_overflow_vec_bit_big sub_big_int false 
-let minus_overflow_vec_bit_signed_big = arith_op_overflow_vec_bit_big sub_big_int true
-
-let add_overflow_vec_bit_signed   = add_overflow_vec_bit_signed_big   
-let minus_overflow_vec_bit        = minus_overflow_vec_bit_big        
-let minus_overflow_vec_bit_signed = minus_overflow_vec_bit_signed_big 
-
-let shift_op_vec_int op (l,r) =
-  match l with
-  | Vvector(_,start,ord) | Vregister(_,start,ord,_,_) ->
-    let array = match l with | Vvector(array,_,_) -> array | Vregister(array,_,_,_,_) -> !array | _ -> assert false in
-    let len = Array.length array in
-    (match op with
-     | "<<" ->
-       if (r <= len) then
-         let left = Array.sub array r (len - r) in
-         let right = Array.make r Vzero in
-         let result = Array.append left right in
-         Vvector(result, start, ord)
-       else
-         Vvector(Array.make len Vzero, start, ord)
-     | ">>" ->
-       if (r <= len) then
-         let left = Array.make r Vzero in
-         let right = Array.sub array 0 (len - r) in
-         let result = Array.append left right in
-         Vvector(result, start, ord)
-       else
-         Vvector(Array.make len Vzero, start, ord)
-     | "<<<" ->
-       let rmod = r mod len in
-       let left = Array.sub array rmod (len - rmod) in
-       let right = Array.sub array 0 rmod in
-       let result = Array.append left right in
-       Vvector(result, start, ord)
-     | _ -> assert false)
-  | _ -> assert false
-
-let shift_op_vec_big op (l,r) = shift_op_vec_int op (l, int_of_big_int r)
-let bitwise_leftshift_big = shift_op_vec_big "<<"
-let bitwise_rightshift_big = shift_op_vec_big ">>"
-let bitwise_rotate_big = shift_op_vec_big "<<<"
-
-let bitwise_leftshift = bitwise_leftshift_big
-let bitwise_rightshift = bitwise_rightshift_big
-let bitwise_rotate = bitwise_rotate_big
-
-let rec arith_op_no0_big op (l,r) = 
-  if eq_big_int r zero_big_int
-  then None
-  else Some (op l r)
-
-let modulo_no0_big = arith_op_no0_big (Z.rem)
-let quot_no0_big = arith_op_no0_big (Z.div)
-
-let rec arith_op_no0_int op (l,r) = 
-  if r = 0
-  then None
-  else Some (op l r)
-
-let rec arith_op_vec_no0_int op sign size (l,r) =
-  let ord = get_ord l in
-  let act_size = ((length_int l) * size) in
-  let (l',r') = (to_num_int sign l,to_num_int sign r) in
-  let n = arith_op_no0_int op (l',r') in
-  let representable,n' = 
-    match n with 
-    | Some n' ->  
-      ((n' <= (int_of_big_int (get_max_representable_in sign act_size))) &&
-       (n' >= (int_of_big_int (get_min_representable_in sign act_size)))), n'
-    | _ -> false,0 in
-  if representable 
-  then to_vec_int ord act_size n'
-  else
-    match l with
-    | Vvector(_, start, _) | Vregister(_, start, _, _, _) ->
-      Vvector((Array.make act_size Vundef), start, ord)
-    | _ -> assert false
-
-let mod_vec_int = arith_op_vec_no0_int (mod) false 1
-let quot_vec_int = arith_op_vec_no0_int (/) false 1
-let quot_vec_signed_int = arith_op_vec_no0_int (/) true 1
-
-let rec arith_op_vec_no0_big op sign size (l,r) =
-  let ord = get_ord l in
-  let act_size = int_of_big_int (mult_int_big_int (length_int l) size) in
-  let (l',r') = (to_num_big sign l,to_num_big sign r) in
-  let n = arith_op_no0_big op (l',r') in
-  let representable,n' = 
-    match n with 
-    | Some n' ->  
-      ((le_big_int n' (get_max_representable_in sign act_size)) &&
-       (ge_big_int n' (get_min_representable_in sign act_size))), n'
-    | _ -> false,zero_big_int in
-  if representable 
-  then to_vec_big ord (big_int_of_int act_size) n'
-  else
-    match l with
-    | Vvector(_, start, _) | Vregister(_, start, _, _, _) ->
-      Vvector((Array.make act_size Vundef), start, ord)
-    | _ -> assert false
-
-let mod_vec_big = arith_op_vec_no0_big (Z.rem) false unit_big_int
-let quot_vec_big = arith_op_vec_no0_big (Z.div) false unit_big_int
-let quot_vec_signed_big = arith_op_vec_no0_big (Z.div) true unit_big_int
-
-let mod_vec         = mod_vec_big         
-let quot_vec        = quot_vec_big        
-let quot_vec_signed = quot_vec_signed_big 
-
-let arith_op_overflow_no0_vec_int op sign size (l,r) =
-  let ord = get_ord l in
-  let rep_size = (length_int r) * size in
-  let act_size = (length_int l) * size in
-  let (l',r') = ((to_num_int sign l),(to_num_int sign r)) in
-  let (l_u,r_u) = (to_num_int false l,to_num_int false r) in
-  let n = arith_op_no0_int op (l',r') in
-  let n_u = arith_op_no0_int op (l_u,r_u) in
-  let representable,n',n_u' = 
-    match n, n_u with 
-    | Some n',Some n_u' ->  
-      ((n' <= (int_of_big_int (get_max_representable_in sign rep_size))) &&
-       (n' >= (int_of_big_int (get_min_representable_in sign rep_size))), n', n_u')
-    | _ -> true,0,0 in
-  let (correct_size_num,one_more) = 
-    if representable then
-      (to_vec_int ord act_size n',to_vec_int ord (1+act_size) n_u')
-    else match l with 
-      | Vvector(_, start, _) | Vregister(_, start, _, _, _) ->
-        Vvector((Array.make act_size Vundef), start, ord),
-        Vvector((Array.make  (act_size + 1) Vundef), start, ord)
-      | _ -> assert false in
-  let overflow = if representable then Vzero else Vone in
-  (correct_size_num,overflow,most_significant one_more)
-
-let quot_overflow_vec_int = arith_op_overflow_no0_vec_int (/) false 1
-let quot_overflow_vec_signed_int = arith_op_overflow_no0_vec_int (/) true 1
-
-let arith_op_overflow_no0_vec_big op sign size (l,r) =
-  let ord = get_ord l in
-  let rep_size = mult_big_int (length_big r) size in
-  let act_size = mult_big_int (length_big l) size in
-  let (l',r') = ((to_num_big sign l),(to_num_big sign r)) in
-  let (l_u,r_u) = (to_num_big false l,to_num_big false r) in
-  let n = arith_op_no0_big op (l',r') in
-  let n_u = arith_op_no0_big op (l_u,r_u) in
-  let representable,n',n_u' = 
-    match n, n_u with 
-    | Some n',Some n_u' ->  
-      ((le_big_int n' (get_max_representable_in sign (int_of_big_int rep_size))) &&
-       (ge_big_int n' (get_min_representable_in sign (int_of_big_int rep_size))), n', n_u')
-    | _ -> true,zero_big_int,zero_big_int in
-  let (correct_size_num,one_more) = 
-    if representable then
-      (to_vec_big ord act_size n',to_vec_big ord (succ_big_int act_size) n_u')
-    else match l with 
-      | Vvector(_, start, _) | Vregister(_, start, _, _, _) ->
-        Vvector((Array.make (int_of_big_int act_size) Vundef), start, ord),
-        Vvector((Array.make  ((int_of_big_int act_size) + 1) Vundef), start, ord)
-      | _ -> assert false in
-  let overflow = if representable then Vzero else Vone in
-  (correct_size_num,overflow,most_significant one_more)
-
-let quot_overflow_vec_big = arith_op_overflow_no0_vec_big (Z.div) false unit_big_int 
-let quot_overflow_vec_signed_big = arith_op_overflow_no0_vec_big (Z.div) true unit_big_int 
-
-let quot_overflow_vec        = quot_overflow_vec_big        
-let quot_overflow_vec_signed = quot_overflow_vec_signed_big 
-
-
-let arith_op_vec_range_no0_int op sign size (l,r) =
-  let ord = get_ord l in
-  arith_op_vec_no0_int op sign size (l,(to_vec_int ord (length_int l) r))
-
-let mod_vec_range_int = arith_op_vec_range_no0_int (mod) false 1
-
-let arith_op_vec_range_no0_big op sign size (l,r) =
-  let ord = get_ord l in
-  arith_op_vec_no0_big op sign size (l,(to_vec_big ord (length_big l) r))
-
-let mod_vec_range_big = arith_op_vec_range_no0_big (Z.rem) false unit_big_int
-
-let mod_vec_range = mod_vec_range_big
-
-(* XXX Need to have a default top level direction reference I think*)
-let duplicate_int (bit,length) =
-  Vvector((Array.make length bit), (length-1), false)
-
-let duplicate_big (bit,length) =
-  duplicate_int (bit, int_of_big_int length)
-
-let duplicate = duplicate_big
-
-let duplicate_bits_big (bits, x) =
-  let len = (length_int bits) * (int_of_big_int x) in
-  let is_inc = get_ord bits in
-  let bits_arr = get_barray bits in
-  let arr = Array.concat (Array.to_list(Array.make (int_of_big_int x) bits_arr)) in
-  Vvector(arr, (if is_inc then 0 else (len - 1)), is_inc)
-
-let duplicate_bits = duplicate_bits_big
-
-let compare_op op (l,r) =
-  if (op l r)
-  then Vone
-  else Vzero
-
-let lt_big = compare_op lt_big_int
-let gt_big = compare_op gt_big_int
-let lteq_big = compare_op le_big_int
-let gteq_big = compare_op ge_big_int
-let lt_int : (int* int) -> vbit = compare_op (<)
-let gt_int : (int * int) -> vbit = compare_op (>)
-let lteq_int : (int * int) -> vbit = compare_op (<=)
-let gteq_int : (int*int) -> vbit = compare_op (>=)
-
-let lt = lt_big
-let gt = gt_big
-let lteq = lteq_big
-let gteq = gteq_big
-
-let compare_op_vec_int op sign (l,r) = 
-  let (l',r') = (to_num_int sign l, to_num_int sign r) in
-  compare_op op (l',r')
-
-let lt_vec_int = compare_op_vec_int (<) true
-let gt_vec_int = compare_op_vec_int (>) true
-let lteq_vec_int = compare_op_vec_int (<=) true
-let gteq_vec_int = compare_op_vec_int (>=) true
-let lt_vec_signed_int = compare_op_vec_int (<) true
-let gt_vec_signed_int = compare_op_vec_int (>) true
-let lteq_vec_signed_int = compare_op_vec_int (<=) true
-let gteq_vec_signed_int = compare_op_vec_int (>=) true
-let lt_vec_unsigned_int = compare_op_vec_int (<) false
-let gt_vec_unsigned_int = compare_op_vec_int (>) false
-let lteq_vec_unsigned_int = compare_op_vec_int (<=) false
-let gteq_vec_unsigned_int = compare_op_vec_int (>=) false
-
-let compare_op_vec_big op sign (l,r) = 
-  let (l',r') = (to_num_big sign l, to_num_big sign r) in
-  compare_op op (l',r')
-
-let lt_vec_big = compare_op_vec_big lt_big_int true
-let gt_vec_big = compare_op_vec_big gt_big_int true
-let lteq_vec_big = compare_op_vec_big le_big_int true
-let gteq_vec_big = compare_op_vec_big ge_big_int true
-let lt_vec_signed_big = compare_op_vec_big lt_big_int true
-let gt_vec_signed_big = compare_op_vec_big gt_big_int true
-let lteq_vec_signed_big = compare_op_vec_big le_big_int true
-let gteq_vec_signed_big = compare_op_vec_big ge_big_int true
-let lt_vec_unsigned_big = compare_op_vec_big lt_big_int false
-let gt_vec_unsigned_big = compare_op_vec_big gt_big_int false
-let lteq_vec_unsigned_big = compare_op_vec_big le_big_int false
-let gteq_vec_unsigned_big = compare_op_vec_big ge_big_int false
-
-let lt_vec            = lt_vec_big            
-let gt_vec            = gt_vec_big            
-let lteq_vec          = lteq_vec_big          
-let gteq_vec          = gteq_vec_big          
-let lt_vec_signed     = lt_vec_signed_big     
-let gt_vec_signed     = gt_vec_signed_big     
-let lteq_vec_signed   = lteq_vec_signed_big   
-let gteq_vec_signed   = gteq_vec_signed_big   
-let lt_vec_unsigned   = lt_vec_unsigned_big   
-let gt_vec_unsigned   = gt_vec_unsigned_big   
-let lteq_vec_unsigned = lteq_vec_unsigned_big 
-let gteq_vec_unsigned = gteq_vec_unsigned_big 
-
-let compare_op_vec_range_int op sign (l,r) = 
-  compare_op op ((to_num_int sign l),r)
-
-let lt_vec_range_int = compare_op_vec_range_int (<) true
-let gt_vec_range_int = compare_op_vec_range_int (>) true
-let lteq_vec_range_int = compare_op_vec_range_int (<=) true
-let gteq_vec_range_int = compare_op_vec_range_int (>=) true
-
-let compare_op_vec_range_big op sign (l,r) = 
-  compare_op op ((to_num_big sign l),r)
-
-let lt_vec_range_big = compare_op_vec_range_big lt_big_int true
-let gt_vec_range_big = compare_op_vec_range_big gt_big_int true
-let lteq_vec_range_big = compare_op_vec_range_big le_big_int true
-let gteq_vec_range_big = compare_op_vec_range_big ge_big_int true
-
-let lt_vec_range   = lt_vec_range_big   
-let gt_vec_range   = gt_vec_range_big   
-let lteq_vec_range = lteq_vec_range_big 
-let gteq_vec_range = gteq_vec_range_big 
-
-let compare_op_range_vec_int op sign (l,r) =
-  compare_op op (l, (to_num_int sign r))
-
-let lt_range_vec_int = compare_op_range_vec_int (<) true
-let gt_range_vec_int = compare_op_range_vec_int (>) true
-let lteq_range_vec_int = compare_op_range_vec_int (<=) true
-let gteq_range_vec_int = compare_op_range_vec_int (>=) true
-
-let compare_op_range_vec_big op sign (l,r) =
-  compare_op op (l, (to_num_big sign r))
-
-let lt_range_vec_big = compare_op_range_vec_big lt_big_int true
-let gt_range_vec_big = compare_op_range_vec_big gt_big_int true
-let lteq_range_vec_big = compare_op_range_vec_big le_big_int true
-let gteq_range_vec_big = compare_op_range_vec_big ge_big_int true
-
-let lt_range_vec   = lt_range_vec_big   
-let gt_range_vec   = gt_range_vec_big   
-let lteq_range_vec = lteq_range_vec_big 
-let gteq_range_vec = gteq_range_vec_big 
-
-let eq (l,r) = if l = r then Vone else Vzero
-let eq_vec_vec (l,r) = eq (to_num_big true l, to_num_big true r)
-let eq_vec (l,r) = eq_vec_vec(l,r)
-let eq_vec_range (l,r) = eq (to_num_big false l,r)
-let eq_range_vec (l,r) = eq (l, to_num_big false r)
-let eq_range = eq
-let eq_bit = bitwise_binop_bit (=)
-
-let neq (l,r) = bitwise_not_bit (eq (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_bit (l,r) = bitwise_not_bit (eq_bit(l,r))
-let neq_range = neq
-
-let mask (n,v) = 
-  let n' = int_of_big_int n in
-  match v with
-  | Vvector (bits,start,dir) ->
-     let current_size = Array.length bits in 
-     let to_drop = (current_size - n') in
-     let bits' = Array.sub bits to_drop n' in
-     Vvector (bits',(if dir then 0 else n'-1), dir)
-  | Vregister (bits,start,dir,name,fields) ->
-     let current_size = Array.length !bits in 
-     let to_drop = (current_size - n') in
-     let bits' = Array.sub !bits to_drop n' in
-     Vvector (bits',(if dir then 0 else n'-1), dir)
-  | VvectorR _ -> failwith "mask not implemented for VregisterR"
-  | Vbit _ -> failwith "mask called for bit"
-
-let slice_raw (v, i, j) = 
-  let i' = int_of_big_int i in
-  let j' = int_of_big_int j in
-  match v with
-  | Vvector (bs, start, is_inc) ->
-     let bits = Array.sub bs i' (j'-i'+1) in
-     let len = Array.length bits in
-     Vvector (bits, (if is_inc then 0 else len - 1), is_inc)
-  | _ -> failwith "slice_raw only implemented for VVector"
-let _slice_raw = slice_raw
-
-(* enough literal big ints to account for most literals found in specs *)
-(* for i = 0 to 257 do Printf.printf "let bi%d = big_int_of_int %d\n" i i done;; *)
-let bi0 = zero_big_int
-let bi1 = unit_big_int
-let bi2 = big_int_of_int 2
-let bi3 = big_int_of_int 3
-let bi4 = big_int_of_int 4
-let bi5 = big_int_of_int 5
-let bi6 = big_int_of_int 6
-let bi7 = big_int_of_int 7
-let bi8 = big_int_of_int 8
-let bi9 = big_int_of_int 9
-let bi10 = big_int_of_int 10
-let bi11 = big_int_of_int 11
-let bi12 = big_int_of_int 12
-let bi13 = big_int_of_int 13
-let bi14 = big_int_of_int 14
-let bi15 = big_int_of_int 15
-let bi16 = big_int_of_int 16
-let bi17 = big_int_of_int 17
-let bi18 = big_int_of_int 18
-let bi19 = big_int_of_int 19
-let bi20 = big_int_of_int 20
-let bi21 = big_int_of_int 21
-let bi22 = big_int_of_int 22
-let bi23 = big_int_of_int 23
-let bi24 = big_int_of_int 24
-let bi25 = big_int_of_int 25
-let bi26 = big_int_of_int 26
-let bi27 = big_int_of_int 27
-let bi28 = big_int_of_int 28
-let bi29 = big_int_of_int 29
-let bi30 = big_int_of_int 30
-let bi31 = big_int_of_int 31
-let bi32 = big_int_of_int 32
-let bi33 = big_int_of_int 33
-let bi34 = big_int_of_int 34
-let bi35 = big_int_of_int 35
-let bi36 = big_int_of_int 36
-let bi37 = big_int_of_int 37
-let bi38 = big_int_of_int 38
-let bi39 = big_int_of_int 39
-let bi40 = big_int_of_int 40
-let bi41 = big_int_of_int 41
-let bi42 = big_int_of_int 42
-let bi43 = big_int_of_int 43
-let bi44 = big_int_of_int 44
-let bi45 = big_int_of_int 45
-let bi46 = big_int_of_int 46
-let bi47 = big_int_of_int 47
-let bi48 = big_int_of_int 48
-let bi49 = big_int_of_int 49
-let bi50 = big_int_of_int 50
-let bi51 = big_int_of_int 51
-let bi52 = big_int_of_int 52
-let bi53 = big_int_of_int 53
-let bi54 = big_int_of_int 54
-let bi55 = big_int_of_int 55
-let bi56 = big_int_of_int 56
-let bi57 = big_int_of_int 57
-let bi58 = big_int_of_int 58
-let bi59 = big_int_of_int 59
-let bi60 = big_int_of_int 60
-let bi61 = big_int_of_int 61
-let bi62 = big_int_of_int 62
-let bi63 = big_int_of_int 63
-let bi64 = big_int_of_int 64
-let bi65 = big_int_of_int 65
-let bi66 = big_int_of_int 66
-let bi67 = big_int_of_int 67
-let bi68 = big_int_of_int 68
-let bi69 = big_int_of_int 69
-let bi70 = big_int_of_int 70
-let bi71 = big_int_of_int 71
-let bi72 = big_int_of_int 72
-let bi73 = big_int_of_int 73
-let bi74 = big_int_of_int 74
-let bi75 = big_int_of_int 75
-let bi76 = big_int_of_int 76
-let bi77 = big_int_of_int 77
-let bi78 = big_int_of_int 78
-let bi79 = big_int_of_int 79
-let bi80 = big_int_of_int 80
-let bi81 = big_int_of_int 81
-let bi82 = big_int_of_int 82
-let bi83 = big_int_of_int 83
-let bi84 = big_int_of_int 84
-let bi85 = big_int_of_int 85
-let bi86 = big_int_of_int 86
-let bi87 = big_int_of_int 87
-let bi88 = big_int_of_int 88
-let bi89 = big_int_of_int 89
-let bi90 = big_int_of_int 90
-let bi91 = big_int_of_int 91
-let bi92 = big_int_of_int 92
-let bi93 = big_int_of_int 93
-let bi94 = big_int_of_int 94
-let bi95 = big_int_of_int 95
-let bi96 = big_int_of_int 96
-let bi97 = big_int_of_int 97
-let bi98 = big_int_of_int 98
-let bi99 = big_int_of_int 99
-let bi100 = big_int_of_int 100
-let bi101 = big_int_of_int 101
-let bi102 = big_int_of_int 102
-let bi103 = big_int_of_int 103
-let bi104 = big_int_of_int 104
-let bi105 = big_int_of_int 105
-let bi106 = big_int_of_int 106
-let bi107 = big_int_of_int 107
-let bi108 = big_int_of_int 108
-let bi109 = big_int_of_int 109
-let bi110 = big_int_of_int 110
-let bi111 = big_int_of_int 111
-let bi112 = big_int_of_int 112
-let bi113 = big_int_of_int 113
-let bi114 = big_int_of_int 114
-let bi115 = big_int_of_int 115
-let bi116 = big_int_of_int 116
-let bi117 = big_int_of_int 117
-let bi118 = big_int_of_int 118
-let bi119 = big_int_of_int 119
-let bi120 = big_int_of_int 120
-let bi121 = big_int_of_int 121
-let bi122 = big_int_of_int 122
-let bi123 = big_int_of_int 123
-let bi124 = big_int_of_int 124
-let bi125 = big_int_of_int 125
-let bi126 = big_int_of_int 126
-let bi127 = big_int_of_int 127
-let bi128 = big_int_of_int 128
-let bi129 = big_int_of_int 129
-let bi130 = big_int_of_int 130
-let bi131 = big_int_of_int 131
-let bi132 = big_int_of_int 132
-let bi133 = big_int_of_int 133
-let bi134 = big_int_of_int 134
-let bi135 = big_int_of_int 135
-let bi136 = big_int_of_int 136
-let bi137 = big_int_of_int 137
-let bi138 = big_int_of_int 138
-let bi139 = big_int_of_int 139
-let bi140 = big_int_of_int 140
-let bi141 = big_int_of_int 141
-let bi142 = big_int_of_int 142
-let bi143 = big_int_of_int 143
-let bi144 = big_int_of_int 144
-let bi145 = big_int_of_int 145
-let bi146 = big_int_of_int 146
-let bi147 = big_int_of_int 147
-let bi148 = big_int_of_int 148
-let bi149 = big_int_of_int 149
-let bi150 = big_int_of_int 150
-let bi151 = big_int_of_int 151
-let bi152 = big_int_of_int 152
-let bi153 = big_int_of_int 153
-let bi154 = big_int_of_int 154
-let bi155 = big_int_of_int 155
-let bi156 = big_int_of_int 156
-let bi157 = big_int_of_int 157
-let bi158 = big_int_of_int 158
-let bi159 = big_int_of_int 159
-let bi160 = big_int_of_int 160
-let bi161 = big_int_of_int 161
-let bi162 = big_int_of_int 162
-let bi163 = big_int_of_int 163
-let bi164 = big_int_of_int 164
-let bi165 = big_int_of_int 165
-let bi166 = big_int_of_int 166
-let bi167 = big_int_of_int 167
-let bi168 = big_int_of_int 168
-let bi169 = big_int_of_int 169
-let bi170 = big_int_of_int 170
-let bi171 = big_int_of_int 171
-let bi172 = big_int_of_int 172
-let bi173 = big_int_of_int 173
-let bi174 = big_int_of_int 174
-let bi175 = big_int_of_int 175
-let bi176 = big_int_of_int 176
-let bi177 = big_int_of_int 177
-let bi178 = big_int_of_int 178
-let bi179 = big_int_of_int 179
-let bi180 = big_int_of_int 180
-let bi181 = big_int_of_int 181
-let bi182 = big_int_of_int 182
-let bi183 = big_int_of_int 183
-let bi184 = big_int_of_int 184
-let bi185 = big_int_of_int 185
-let bi186 = big_int_of_int 186
-let bi187 = big_int_of_int 187
-let bi188 = big_int_of_int 188
-let bi189 = big_int_of_int 189
-let bi190 = big_int_of_int 190
-let bi191 = big_int_of_int 191
-let bi192 = big_int_of_int 192
-let bi193 = big_int_of_int 193
-let bi194 = big_int_of_int 194
-let bi195 = big_int_of_int 195
-let bi196 = big_int_of_int 196
-let bi197 = big_int_of_int 197
-let bi198 = big_int_of_int 198
-let bi199 = big_int_of_int 199
-let bi200 = big_int_of_int 200
-let bi201 = big_int_of_int 201
-let bi202 = big_int_of_int 202
-let bi203 = big_int_of_int 203
-let bi204 = big_int_of_int 204
-let bi205 = big_int_of_int 205
-let bi206 = big_int_of_int 206
-let bi207 = big_int_of_int 207
-let bi208 = big_int_of_int 208
-let bi209 = big_int_of_int 209
-let bi210 = big_int_of_int 210
-let bi211 = big_int_of_int 211
-let bi212 = big_int_of_int 212
-let bi213 = big_int_of_int 213
-let bi214 = big_int_of_int 214
-let bi215 = big_int_of_int 215
-let bi216 = big_int_of_int 216
-let bi217 = big_int_of_int 217
-let bi218 = big_int_of_int 218
-let bi219 = big_int_of_int 219
-let bi220 = big_int_of_int 220
-let bi221 = big_int_of_int 221
-let bi222 = big_int_of_int 222
-let bi223 = big_int_of_int 223
-let bi224 = big_int_of_int 224
-let bi225 = big_int_of_int 225
-let bi226 = big_int_of_int 226
-let bi227 = big_int_of_int 227
-let bi228 = big_int_of_int 228
-let bi229 = big_int_of_int 229
-let bi230 = big_int_of_int 230
-let bi231 = big_int_of_int 231
-let bi232 = big_int_of_int 232
-let bi233 = big_int_of_int 233
-let bi234 = big_int_of_int 234
-let bi235 = big_int_of_int 235
-let bi236 = big_int_of_int 236
-let bi237 = big_int_of_int 237
-let bi238 = big_int_of_int 238
-let bi239 = big_int_of_int 239
-let bi240 = big_int_of_int 240
-let bi241 = big_int_of_int 241
-let bi242 = big_int_of_int 242
-let bi243 = big_int_of_int 243
-let bi244 = big_int_of_int 244
-let bi245 = big_int_of_int 245
-let bi246 = big_int_of_int 246
-let bi247 = big_int_of_int 247
-let bi248 = big_int_of_int 248
-let bi249 = big_int_of_int 249
-let bi250 = big_int_of_int 250
-let bi251 = big_int_of_int 251
-let bi252 = big_int_of_int 252
-let bi253 = big_int_of_int 253
-let bi254 = big_int_of_int 254
-let bi255 = big_int_of_int 255
-let bi256 = big_int_of_int 256
-let bi257 = big_int_of_int 257