Start splitting values/etc into int/big_int for ocaml generation

4 files changed, 85 insertions, 3 deletions

diff --git a/src/rewriter.ml b/src/rewriter.ml
index 88d2f451..18994458 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -1138,11 +1138,56 @@ let rewrite_defs_exp_lift_assign defs = rewrite_defs_base
      rewrite_fun = rewrite_fun;
      rewrite_def = rewrite_def;
      rewrite_defs = rewrite_defs_base} defs
+    
+let rewrite_exp_separate_ints rewriters nmap ((E_aux (exp,(l,annot))) as full_exp) =
+  let tparms,t,tag,nexps,eff,cum_eff,bounds = match annot with
+    | Base((tparms,t),tag,nexps,eff,cum_eff,bounds) -> tparms,t,tag,nexps,eff,cum_eff,bounds
+    | _ -> [],unit_t,Emp_local,[],pure_e,pure_e,nob in
+  let rewrap e = E_aux (e,(l,annot)) in
+  let rewrap_effects e effsum =
+    E_aux (e,(l,Base ((tparms,t),tag,nexps,eff,effsum,bounds))) in
+  let rewrite_rec = rewriters.rewrite_exp rewriters nmap in
+  let rewrite_base = rewrite_exp rewriters nmap in
+  match exp with
+  | E_lit (L_aux (((L_num _) as lit),_)) ->
+    (match (is_within_machine64 t nexps) with
+     | Yes | Maybe -> rewrite_base full_exp
+     | No -> E_aux(E_app(Id_aux (Id "integer_of_int",l),[rewrite_base full_exp]),
+                   (l, Base((tparms,t),External(None),nexps,eff,cum_eff,bounds))))
+  | E_cast (typ, exp) -> rewrap (E_cast (typ, rewrite_rec exp))
+  | E_app (id,exps) -> rewrap (E_app (id,List.map rewrite_rec exps))
+  | E_app_infix(el,id,er) -> rewrap (E_app_infix(rewrite_rec el,id,rewrite_rec er))
+  | E_for (id, e1, e2, e3, o, body) ->
+      rewrap (E_for (id, rewrite_rec e1, rewrite_rec e2, rewrite_rec e3, o, rewrite_rec body))
+  | E_vector_access (vec,index) -> rewrap (E_vector_access (rewrite_rec vec,rewrite_rec index))
+  | E_vector_subrange (vec,i1,i2) ->
+    rewrap (E_vector_subrange (rewrite_rec vec,rewrite_rec i1,rewrite_rec i2))
+  | E_vector_update (vec,index,new_v) -> 
+    rewrap (E_vector_update (rewrite_rec vec,rewrite_rec index,rewrite_rec new_v))
+  | E_vector_update_subrange (vec,i1,i2,new_v) ->
+    rewrap (E_vector_update_subrange (rewrite_rec vec,rewrite_rec i1,rewrite_rec i2,rewrite_rec new_v))
+  | E_case (exp ,pexps) -> 
+    rewrap (E_case (rewrite_rec exp,
+                    (List.map 
+                       (fun (Pat_aux (Pat_exp(p,e),pannot)) -> 
+                          Pat_aux (Pat_exp(rewriters.rewrite_pat rewriters nmap p,rewrite_rec e),pannot)) pexps)))
+  | E_let (letbind,body) -> rewrap (E_let(rewriters.rewrite_let rewriters nmap letbind,rewrite_rec body))
+  | _ -> rewrite_rec full_exp
+
+let rewrite_defs_separate_numbs defs = rewrite_defs_base
+    {rewrite_exp = rewrite_exp_separate_ints;
+     rewrite_pat = rewrite_pat;
+     rewrite_let = rewrite_let; (*will likely need a new one?*)
+     rewrite_lexp = rewrite_lexp; (*will likely need a new one?*)
+     rewrite_fun = rewrite_fun;
+     rewrite_def = rewrite_def;
+     rewrite_defs = rewrite_defs_base} defs
 
 let rewrite_defs_ocaml defs =
   let defs_vec_concat_removed = rewrite_defs_remove_vector_concat defs in
   let defs_lifted_assign = rewrite_defs_exp_lift_assign defs_vec_concat_removed in
-  defs_lifted_assign
+  let defs_separate_nums = rewrite_defs_separate_numbs defs_lifted_assign in
+  defs_separate_nums
 
 let remove_blocks =
 
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 0c751c9b..278243b8 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -70,10 +70,42 @@ let unpower_of_2 b =
   let two = big_int_of_int 2 in
   let four = big_int_of_int 4 in
   let eight = big_int_of_int 8 in
-  ()
+  let sixteen = big_int_of_int 16 in
+  let thirty_two = big_int_of_int 32 in
+  let sixty_four = big_int_of_int 64 in
+  let onetwentyeight = big_int_of_int 128 in
+  let twofiftysix = big_int_of_int 256 in
+  let fivetwelve = big_int_of_int 512 in
+  let oneotwentyfour = big_int_of_int 1024 in
+  let to_the_sixteen = big_int_of_int 65536 in
+  let to_the_thirtytwo = big_int_of_string "4294967296" in
+  let to_the_sixtyfour = big_int_of_string "18446744073709551616" in
+  let ck i = eq_big_int b i in
+  if      ck unit_big_int     then zero_big_int
+  else if ck two              then unit_big_int
+  else if ck four             then two
+  else if ck eight            then big_int_of_int 3
+  else if ck sixteen          then four
+  else if ck thirty_two       then big_int_of_int 5
+  else if ck sixty_four       then big_int_of_int 6
+  else if ck onetwentyeight   then big_int_of_int 7
+  else if ck twofiftysix      then eight
+  else if ck fivetwelve       then big_int_of_int 9
+  else if ck oneotwentyfour   then big_int_of_int 10
+  else if ck to_the_sixteen   then sixteen
+  else if ck to_the_thirtytwo then thirty_two
+  else if ck to_the_sixtyfour then sixty_four
+  else let rec unpower b power =
+         if eq_big_int b unit_big_int
+         then power
+         else (unpower (div_big_int b  two) (succ_big_int power)) in
+    unpower b zero_big_int
 
 let is_within_range candidate range constraints =
-  match candidate.t with
+  let candidate_actual = match candidate.t with
+    | Tabbrev(_,t) -> t
+    | _ -> candidate in
+  match candidate_actual.t with
   | Tapp("atom", [TA_nexp n]) ->
     (match n.nexp with
      | Nconst i | N2n(_,Some i) -> if check_in_range i range then Yes else No
@@ -97,3 +129,6 @@ let is_within_range candidate range constraints =
        else No
      | _ -> Maybe)
   | _ -> Maybe
+
+let is_within_machine64 candidate constraints = is_within_range candidate int64_t constraints
+  
diff --git a/src/spec_analysis.mli b/src/spec_analysis.mli
index 1b1197dd..731bd822 100644
--- a/src/spec_analysis.mli
+++ b/src/spec_analysis.mli
@@ -17,3 +17,4 @@ val default_order : tannot defs -> order
   suitable unwrapping of abbreviations, reg, and registers). 
 *)
 val is_within_range: typ -> typ -> nexp_range list -> triple
+val is_within_machine64 : typ -> nexp_range list -> triple
diff --git a/src/type_internal.mli b/src/type_internal.mli
index c45f5342..dd7993fd 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -205,6 +205,7 @@ val initial_abbrev_env : tannot Envmap.t
 val initial_typ_env : tannot Envmap.t
 val nat_t : t
 val unit_t : t
+val int64_t : t
 val bool_t : t
 val bit_t : t
 val string_t : t