4 files changed, 24 insertions, 22 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 9106f7b6..da617824 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -64,8 +64,8 @@ type value =
     integerToString (n / 10) (chr (natFromInteger (n mod 10 + 48)) :: acc)
 
 let string_of_integer i = if i = 0 then "0" else toString(integerToString i [])*)
-val string_of_integer : integer -> string
-declare ocaml target_rep function string_of_integer = `Big_int.string_of_big_int`
+(*val string_of_integer : integer -> string
+declare ocaml target_rep function string_of_integer = `Big_int_Z.string_of_big_int`*)
 
 
 let rec string_of_value v = match v with
@@ -77,7 +77,7 @@ let rec string_of_value v = match v with
     | L_one  -> "1"
     | L_true -> "true"
     | L_false -> "false"
-    | L_num num -> string_of_integer num
+    | L_num num -> show num
     | L_hex hex -> "0x" ^ hex
     | L_bin bin -> "0b" ^ bin
     | L_undef -> "undefined"
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 1e97e061..d9be8717 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -3,6 +3,7 @@ open import Interp
 open import Interp_ast
 import Assert_extra Maybe_extra (* For failwith for error reporting while debugging; and for fromJust when we know it's not Nothing *)
 open import Num
+import Num_extra
 open import List
 open import Word
 open import Bool
@@ -23,15 +24,13 @@ let hardware_quot (a:integer) (b:integer) : integer =
   then (a/b) + 1
   else a/b
 
-val integer_of_string : string -> integer
-declare ocaml target_rep function integer_of_string = `Big_int.big_int_of_string`
 
-let (max_64u : integer) = integer_of_string "18446744073709551615"
-let (max_64 : integer) = integer_of_string  "9223372036854775807"
-let (min_64 : integer) = integer_of_string "-9223372036854775808"
-let (max_32u : integer) = integer_of_string "4294967295"
-let (max_32 : integer) = integer_of_string "2147483647"
-let (min_32 : integer) = integer_of_string "-2147483648"
+let (max_64u : integer) = Num_extra.integerOfString "18446744073709551615"
+let (max_64 : integer) = Num_extra.integerOfString  "9223372036854775807"
+let (min_64 : integer) = Num_extra.integerOfString "-9223372036854775808"
+let (max_32u : integer) = Num_extra.integerOfString "4294967295"
+let (max_32 : integer) = Num_extra.integerOfString "2147483647"
+let (min_32 : integer) = Num_extra.integerOfString "-2147483648"
 let (max_8 : integer) = (integerFromNat 127)
 let (min_8 : integer) = (integerFromNat 0) - (integerFromNat 128)
 let (max_5 : integer) = (integerFromNat 31)
diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml
index 1ea6df3e..ca4abe17 100644
--- a/src/lem_interp/pretty_interp.ml
+++ b/src/lem_interp/pretty_interp.ml
@@ -17,10 +17,13 @@
 
 open Interp_ast
 open Format
-open Big_int
+open Nat_big_num
 
 let ignore_casts = ref true
 
+let zero_big = of_int 0
+let one_big = of_int 1
+
 let pp_format_id (Id_aux(i,_)) =
   match i with
   | Id(i) -> i
@@ -43,7 +46,7 @@ let doc_id (Id_aux(i,_)) =
 
 let doc_var (Kid_aux(Var v,_)) = string v
 
-let doc_int i = string (string_of_big_int i)
+let doc_int i = string (to_string i)
 
 let doc_bkind (BK_aux(k,_)) =
   string (match k with
@@ -113,12 +116,12 @@ let doc_typ, doc_atomic_typ, doc_nexp =
     Typ_arg_aux (Typ_arg_order (Ord_aux (Ord_inc, _)), _);
     Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) ->
     (doc_id id) ^^ 
-      (brackets (if eq_big_int n zero_big_int then doc_int m 
-	         else doc_op colon (doc_int n) (doc_int (add_big_int n (sub_big_int m unit_big_int)))))
+      (brackets (if equal n zero_big then doc_int m 
+	         else doc_op colon (doc_int n) (doc_int (add n (sub m one_big)))))
   | Typ_app(Id_aux (Id "range", _), [
     Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant n, _)), _);
     Typ_arg_aux(Typ_arg_nexp m, _);]) ->
-    (squarebars (if eq_big_int n zero_big_int then nexp m else doc_op colon (doc_int n) (nexp m))) 
+    (squarebars (if equal n zero_big then nexp m else doc_op colon (doc_int n) (nexp m))) 
   | _ -> atomic_typ ty 
   and atomic_typ ((Typ_aux (t, _)) as ty) = match t with
   | Typ_id id  -> doc_id id
@@ -203,7 +206,7 @@ let doc_lit (L_aux(l,_)) =
   | L_one   -> "bitone"
   | L_true  -> "true"
   | L_false -> "false"
-  | L_num i -> string_of_big_int i
+  | L_num i -> to_string i
   | L_hex n -> "0x" ^ n
   | L_bin n -> "0b" ^ n
   | L_undef -> "undefined"
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index 1764e46b..5bf3acc8 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -4,7 +4,7 @@ open Interp_utilities ;;
 open Interp_interface ;;
 open Interp_inter_imp ;;
 
-open Big_int ;;
+open Nat_big_num ;;
 
 let lit_to_string = function
  | L_unit -> "unit"
@@ -12,7 +12,7 @@ let lit_to_string = function
  | L_one -> "0b1"
  | L_true -> "true"
  | L_false -> "false"
- | L_num n -> string_of_big_int n
+ | L_num n -> to_string n
  | L_hex s -> "0x"^s
  | L_bin s -> "0b"^s
  | L_undef -> "undefined"
@@ -92,7 +92,7 @@ let hex_int_to_string i =
 
 let bytes_lifted_homogenous_to_string = function
   | Bitslh_concrete bs -> 
-      let i = Big_int.int_of_big_int (Interp_interface.integer_of_bit_list bs) in
+      let i = to_int (Interp_interface.integer_of_bit_list bs) in
       hex_int_to_string i
   | Bitslh_undef -> "uu"
   | Bitslh_unknown -> "??"
@@ -325,7 +325,7 @@ let rec compact_stack ?(acc=[]) = function
 ;;  
 
 let sub_to_string = function None -> "" | Some (x, y) -> sprintf " (%s, %s)"
-  (string_of_big_int x) (string_of_big_int y)
+  (to_string x) (to_string y)
 ;;
 
 let rec format_events = function
@@ -410,7 +410,7 @@ let instr_parm_to_string (name, typ, value) =
     | Other -> "Unrepresentable external value"
     | _ -> let intern_v = (Interp_inter_imp.intern_ifield_value D_increasing value) in
 	      match Interp_lib.to_num Interp_lib.Unsigned intern_v with
-		| V_lit (L_aux(L_num n, _)) -> string_of_big_int n
+		| V_lit (L_aux(L_num n, _)) -> to_string n
 		| _ -> ifield_to_string value
 
 let rec instr_parms_to_string ps =