Use big_nums from Lem

1 files changed, 12 insertions, 14 deletions

diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 3b7a7345..110c0b31 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -51,7 +51,6 @@
 open Type_check
 open Ast
 open Format
-open Big_int
 open Pretty_print_common
 
 (****************************************************************************
@@ -78,11 +77,11 @@ let base ppf s = fprintf ppf "%s" s
 let quot_string ppf s = fprintf ppf "\"%s\"" s
 
 let lemnum default n =
-  if le_big_int zero_big_int n && le_big_int n (big_int_of_int 128) then
-    "int" ^ string_of_big_int n
-  else if ge_big_int n zero_big_int then
+  if Big_int.less_equal Big_int.zero n && Big_int.less_equal n (Big_int.of_int 128) then
+    "int" ^ Big_int.to_string n
+  else if Big_int.greater_equal n Big_int.zero then
     default n
-  else ("(int0 - " ^ (default (abs_big_int n)) ^ ")")
+  else ("(int0 - " ^ (default (Big_int.abs n)) ^ ")")
 
 let pp_format_id (Id_aux(i,_)) =
   match i with
@@ -151,7 +150,7 @@ and pp_format_nexp_lem (Nexp_aux(n,l)) =
   (match n with
    | Nexp_id(i) -> "(Nexp_id " ^ pp_format_id_lem i ^ ")"
    | Nexp_var(v) -> "(Nexp_var " ^ pp_format_var_lem v ^ ")"
-   | Nexp_constant(i) -> "(Nexp_constant " ^ (lemnum string_of_big_int i) ^ ")"
+   | Nexp_constant(i) -> "(Nexp_constant " ^ (lemnum Big_int.to_string i) ^ ")"
    | Nexp_sum(n1,n2) -> "(Nexp_sum " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
    | Nexp_minus(n1,n2) -> "(Nexp_minus " ^ (pp_format_nexp_lem n1)^ " " ^ (pp_format_nexp_lem n2) ^ ")"
    | Nexp_times(n1,n2) -> "(Nexp_times " ^  (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
@@ -189,7 +188,6 @@ and pp_format_base_effect_lem (BE_aux(e,l)) =
 and pp_format_effects_lem (Effect_aux(e,l)) =
   "(Effect_aux " ^
   (match e with
-  | Effect_var(v) -> "(Effect_var " ^ pp_format_var v ^ ")"
   | Effect_set(efcts) ->
     "(Effect_set [" ^
       (list_format "; " pp_format_base_effect_lem efcts) ^ " ])") ^ " " ^
@@ -215,7 +213,7 @@ and pp_format_nexp_constraint_lem (NC_aux(nc,l)) =
   | NC_set(id,bounds) -> "(NC_set " ^
     pp_format_var_lem id ^
       " [" ^
-      list_format "; " string_of_big_int bounds ^
+      list_format "; " Big_int.to_string bounds ^
       "])") ^ " " ^
   (pp_format_l_lem l) ^ ")"
 
@@ -278,7 +276,7 @@ let pp_format_lit_lem (L_aux(lit,l)) =
   | L_one -> "L_one"
   | L_true -> "L_true"
   | L_false -> "L_false"
-  | L_num(i) -> "(L_num " ^ (lemnum string_of_big_int i) ^ ")"
+  | L_num(i) -> "(L_num " ^ (lemnum Big_int.to_string i) ^ ")"
   | L_hex(n) -> "(L_hex \"" ^ n ^ "\")"
   | L_bin(n) -> "(L_bin \"" ^ n ^ "\")"
   | L_undef -> "L_undef"
@@ -430,14 +428,14 @@ and pp_lem_exp ppf (E_aux(e,(l,annot)) as exp) =
         | Tapp("vector",[TA_nexp _;TA_nexp r;_;_]) ->
           (match r.nexp with
           | Nconst bi -> fprintf ppf "@[<0>(E_aux (E_lit (L_aux (L_num %a) %a)) (%a, %a))@]"
-                                       kwd (lemnum string_of_int (int_of_big_int bi)) pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob))
+                                       kwd (lemnum string_of_int (Big_int.to_int bi)) pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob))
           | Nvar v -> fprintf ppf  "@[<0>(E_aux (E_id (Id_aux (Id \"%a\") %a)) (%a,%a))@]"
                                      kwd v pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob))
           | _ ->  raise (Reporting_basic.err_unreachable l "Internal exp given vector without known length"))
         | Tapp("implicit",[TA_nexp r]) ->
           (match r.nexp with
             | Nconst bi -> fprintf ppf "@[<0>(E_aux (E_lit (L_aux (L_num %a) %a)) (%a, %a))@]"
-                                       kwd (lemnum string_of_int (int_of_big_int bi)) pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob))
+                                       kwd (lemnum string_of_int (Big_int.to_int bi)) pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob))
             | Nvar v -> fprintf ppf "@[<0>(E_aux (E_id (Id_aux (Id \"%a\") %a)) (%a,%a))@]"
                                      kwd v pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob))
             | _ -> raise (Reporting_basic.err_unreachable l "Internal_exp given implicit without variable or const"))
@@ -518,8 +516,8 @@ let pp_lem_namescm ppf (Name_sect_aux(ns,l)) =
 
 let rec pp_lem_range ppf (BF_aux(r,l)) =
   match r with
-  | BF_single(i) -> fprintf ppf "(BF_aux (BF_single %i) %a)" (int_of_big_int i) pp_lem_l l
-  | BF_range(i1,i2) -> fprintf ppf "(BF_aux (BF_range %i %i) %a)" (int_of_big_int i1) (int_of_big_int i2) pp_lem_l l
+  | BF_single(i) -> fprintf ppf "(BF_aux (BF_single %i) %a)" (Big_int.to_int i) pp_lem_l l
+  | BF_range(i1,i2) -> fprintf ppf "(BF_aux (BF_range %i %i) %a)" (Big_int.to_int i1) (Big_int.to_int i2) pp_lem_l l
   | BF_concat(ir1,ir2) -> fprintf ppf "(BF_aux (BF_concat %a %a) %a)" pp_lem_range ir1 pp_lem_range ir2 pp_lem_l l
 
 let pp_lem_typdef ppf (TD_aux(td,(l,annot))) =
@@ -626,7 +624,7 @@ let rec pp_lem_def ppf d =
   | DEF_val(lbind) -> fprintf ppf "(DEF_val %a);@\n" pp_lem_let lbind
   | DEF_reg_dec(dec) -> fprintf ppf "(DEF_reg_dec %a);@\n" pp_lem_dec dec
   | DEF_comm d -> fprintf ppf ""
-  | DEF_fixity (prec, n, id) -> fprintf ppf "(DEF_fixity %a %s %a);@\n" pp_lem_prec prec (lemnum string_of_big_int n) pp_lem_id id
+  | DEF_fixity (prec, n, id) -> fprintf ppf "(DEF_fixity %a %s %a);@\n" pp_lem_prec prec (lemnum Big_int.to_string n) pp_lem_id id
   | DEF_internal_mutrec f_defs -> List.iter (fun f_def -> pp_lem_def ppf (DEF_fundef f_def)) f_defs
   | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "initial_check didn't remove all scattered Defs")