summaryrefslogtreecommitdiff
path: root/src/monomorphise.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/monomorphise.ml')
-rw-r--r--src/monomorphise.ml58
1 files changed, 29 insertions, 29 deletions
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 0cbeda49..06f0683a 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
@@ -102,7 +102,7 @@ let rec subst_nc substs (NC_aux (nc,l) as n_constraint) =
begin
match KBindings.find kid substs with
| Nexp_aux (Nexp_constant i,_) ->
- if List.exists (fun j -> Big_int.eq_big_int i j) is then re NC_true else re NC_false
+ if List.exists (fun j -> Big_int.equal i j) is then re NC_true else re NC_false
| nexp ->
raise (Reporting_basic.err_general l
("Unable to substitute " ^ string_of_nexp nexp ^
@@ -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
@@ -551,7 +551,7 @@ let nexp_subst_fns substs =
| E_assert (e1,e2) -> re (E_assert (s_exp e1,s_exp e2))
| E_internal_cast ((l,ann),e) -> re (E_internal_cast ((l,s_tannot ann),s_exp e))
| E_comment_struc e -> re (E_comment_struc e)
- | E_internal_let (le,e1,e2) -> re (E_internal_let (s_lexp le, s_exp e1, s_exp e2))
+ | E_var (le,e1,e2) -> re (E_var (s_lexp le, s_exp e1, s_exp e2))
| E_internal_plet (p,e1,e2) -> re (E_internal_plet (s_pat p, s_exp e1, s_exp e2))
| E_internal_return e -> re (E_internal_return (s_exp e))
| E_throw e -> re (E_throw (s_exp e))
@@ -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
@@ -1040,7 +1040,7 @@ let split_defs splits defs =
| E_comment_struc e -> re (E_comment_struc e) assigns
| E_app_infix _
- | E_internal_let _
+ | E_var _
| E_internal_plet _
| E_internal_return _
-> raise (Reporting_basic.err_unreachable l
@@ -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))
| _ ->
@@ -1458,7 +1458,7 @@ let split_defs splits defs =
| E_assert (e1,e2) -> re (E_assert (map_exp e1,map_exp e2))
| E_internal_cast (ann,e) -> re (E_internal_cast (ann,map_exp e))
| E_comment_struc e -> re (E_comment_struc e)
- | E_internal_let (le,e1,e2) -> re (E_internal_let (map_lexp le, map_exp e1, map_exp e2))
+ | E_var (le,e1,e2) -> re (E_var (map_lexp le, map_exp e1, map_exp e2))
| E_internal_plet (p,e1,e2) -> re (E_internal_plet (check_single_pat p, map_exp e1, map_exp e2))
| E_internal_return e -> re (E_internal_return (map_exp e))
and map_opt_default ((Def_val_aux (ed,annot)) as eda) =
@@ -2226,7 +2226,7 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) =
-> raise (Reporting_basic.err_unreachable l
("Unexpected expression encountered in monomorphisation: " ^ string_of_exp exp))
- | E_internal_let (lexp,e1,e2) ->
+ | E_var (lexp,e1,e2) ->
(* Really we ought to remove the assignment after e2 *)
let d1,assigns,r1 = analyse_exp fn_id env assigns e1 in
let assigns,r' = analyse_lexp fn_id env assigns d1 lexp in
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 04:46:52 +0000