diff options
Diffstat (limited to 'src/monomorphise.ml')
| -rw-r--r-- | src/monomorphise.ml | 48 |
1 files changed, 24 insertions, 24 deletions
diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 05b9efcb..7d72b974 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -51,7 +51,7 @@ open Parse_ast open Ast open Ast_util -open Big_int +module Big_int = Nat_big_num open Type_check let size_set_limit = 8 @@ -138,18 +138,18 @@ let subst_src_typ substs t = in s_styp substs t let make_vector_lit sz i = - let f j = if eq_big_int (mod_big_int (shift_right_big_int i (sz-j-1)) (big_int_of_int 2)) zero_big_int then '0' else '1' in + let f j = if Big_int.equal (Big_int.modulus (Big_int.shift_right i (sz-j-1)) (Big_int.of_int 2)) Big_int.zero then '0' else '1' in let s = String.init sz f in L_aux (L_bin s,Generated Unknown) let tabulate f n = let rec aux acc n = let acc' = f n::acc in - if eq_big_int n zero_big_int then acc' else aux acc' (sub_big_int n unit_big_int) - in if eq_big_int n zero_big_int then [] else aux [] (sub_big_int n unit_big_int) + if Big_int.equal n Big_int.zero then acc' else aux acc' (Big_int.sub n (Big_int.of_int 1)) + in if Big_int.equal n Big_int.zero then [] else aux [] (Big_int.sub n (Big_int.of_int 1)) let make_vectors sz = - tabulate (make_vector_lit sz) (shift_left_big_int unit_big_int sz) + tabulate (make_vector_lit sz) (Big_int.shift_left (Big_int.of_int 1) sz) let pat_id_is_variable env id = match Env.lookup_id id env with @@ -412,7 +412,7 @@ let split_src_type id ty (TypQ_aux (q,ql)) = in let name_seg = function | (_,None) -> "" - | (k,Some i) -> string_of_kid k ^ string_of_big_int i + | (k,Some i) -> string_of_kid k ^ Big_int.to_string i in let name l i = String.concat "_" (i::(List.map name_seg l)) in Some (List.map (fun (l,ty) -> (l, wrap (name l),ty)) variants) @@ -421,11 +421,11 @@ let reduce_nexp subst ne = let rec eval (Nexp_aux (ne,_) as nexp) = match ne with | Nexp_constant i -> i - | Nexp_sum (n1,n2) -> add_big_int (eval n1) (eval n2) - | Nexp_minus (n1,n2) -> sub_big_int (eval n1) (eval n2) - | Nexp_times (n1,n2) -> mult_big_int (eval n1) (eval n2) - | Nexp_exp n -> shift_left_big_int (eval n) 1 - | Nexp_neg n -> minus_big_int (eval n) + | Nexp_sum (n1,n2) -> Big_int.add (eval n1) (eval n2) + | Nexp_minus (n1,n2) -> Big_int.sub (eval n1) (eval n2) + | Nexp_times (n1,n2) -> Big_int.mul (eval n1) (eval n2) + | Nexp_exp n -> Big_int.shift_left (eval n) 1 + | Nexp_neg n -> Big_int.negate (eval n) | _ -> raise (Reporting_basic.err_general Unknown ("Couldn't turn nexp " ^ string_of_nexp nexp ^ " into concrete value")) @@ -465,7 +465,7 @@ let refine_constructor refinements l env id args = (fun v (_,w) -> match v,w with | _,None -> true - | Some (U_nexp (Nexp_aux (Nexp_constant n, _))),Some m -> eq_big_int n m + | Some (U_nexp (Nexp_aux (Nexp_constant n, _))),Some m -> Big_int.equal n m | _,_ -> false) bindings mapping in match List.find matches_refinement irefinements with @@ -617,7 +617,7 @@ let remove_bound env pat = let lit_match = function | (L_zero | L_false), (L_zero | L_false) -> true | (L_one | L_true ), (L_one | L_true ) -> true - | L_num i1, L_num i2 -> eq_big_int i1 i2 + | L_num i1, L_num i2 -> Big_int.equal i1 i2 | l1,l2 -> l1 = l2 (* There's no undefined nexp, so replace undefined sizes with a plausible size. @@ -660,8 +660,8 @@ let rec drop_casts = function | exp -> exp let int_of_str_lit = function - | L_hex hex -> big_int_of_string ("0x" ^ hex) - | L_bin bin -> big_int_of_string ("0b" ^ bin) + | L_hex hex -> Big_int.of_string ("0x" ^ hex) + | L_bin bin -> Big_int.of_string ("0b" ^ bin) | _ -> assert false let lit_eq (L_aux (l1,_)) (L_aux (l2,_)) = @@ -670,9 +670,9 @@ let lit_eq (L_aux (l1,_)) (L_aux (l2,_)) = | (L_one |L_true ), (L_one |L_true) -> Some true | (L_hex _| L_bin _), (L_hex _|L_bin _) - -> Some (eq_big_int (int_of_str_lit l1) (int_of_str_lit l2)) + -> Some (Big_int.equal (int_of_str_lit l1) (int_of_str_lit l2)) | L_undef, _ | _, L_undef -> None - | L_num i1, L_num i2 -> Some (eq_big_int i1 i2) + | L_num i1, L_num i2 -> Some (Big_int.equal i1 i2) | _ -> Some (l1 = l2) let try_app (l,ann) (id,args) = @@ -704,12 +704,12 @@ let try_app (l,ann) (id,args) = else if is_id "shl_int" then match args with | [E_aux (E_lit L_aux (L_num i,_),_); E_aux (E_lit L_aux (L_num j,_),_)] -> - Some (E_aux (E_lit (L_aux (L_num (shift_left_big_int i (int_of_big_int j)),new_l)),(l,ann))) + Some (E_aux (E_lit (L_aux (L_num (Big_int.shift_left i (Big_int.to_int j)),new_l)),(l,ann))) | _ -> None else if is_id "mult_int" then match args with | [E_aux (E_lit L_aux (L_num i,_),_); E_aux (E_lit L_aux (L_num j,_),_)] -> - Some (E_aux (E_lit (L_aux (L_num (mult_big_int i j),new_l)),(l,ann))) + Some (E_aux (E_lit (L_aux (L_num (Big_int.mul i j),new_l)),(l,ann))) | _ -> None else if is_id "ex_int" then match args with @@ -720,8 +720,8 @@ let try_app (l,ann) (id,args) = | [E_aux (E_lit L_aux ((L_hex _ | L_bin _) as lit,_),_); E_aux (E_lit L_aux (L_num i,_),_)] -> let v = int_of_str_lit lit in - let b = and_big_int (shift_right_big_int v (int_of_big_int i)) unit_big_int in - let lit' = if eq_big_int b unit_big_int then L_one else L_zero in + let b = Big_int.bitwise_and (Big_int.shift_right v (Big_int.to_int i)) (Big_int.of_int 1) in + let lit' = if Big_int.equal b (Big_int.of_int 1) then L_one else L_zero in Some (E_aux (E_lit (L_aux (lit',new_l)),(l,ann))) | _ -> None else None @@ -1231,14 +1231,14 @@ let split_defs splits defs = | Typ_app (Id_aux (Id "vector",_), [_;Typ_arg_aux (Typ_arg_nexp len,_);_;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) -> (match len with | Nexp_aux (Nexp_constant sz,_) -> - if int_of_big_int sz <= vector_split_limit then - let lits = make_vectors (int_of_big_int sz) in + if Big_int.to_int sz <= vector_split_limit then + let lits = make_vectors (Big_int.to_int sz) in List.map (fun lit -> P_aux (P_lit lit,(l,annot)), [var,E_aux (E_lit lit,(new_l,annot))]) lits else raise (Reporting_basic.err_general l - ("Refusing to split vector type of length " ^ string_of_big_int sz ^ + ("Refusing to split vector type of length " ^ Big_int.to_string sz ^ " above limit " ^ string_of_int vector_split_limit ^ " for variable " ^ v)) | _ -> |