diff options
Diffstat (limited to 'src/gen_lib')
| -rw-r--r-- | src/gen_lib/sail_values.lem | 8 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.ml | 1488 |
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 |