Remove nums

alt-ergo-lib.opam

@@ -20,7 +20,6 @@ depends: [
   "dolmen" {>= "0.8.1"}
   "dolmen_type" {>= "0.8.1"}
   "dolmen_loop" {>= "0.8.1"}
-  "num"
   "ocplib-simplex" {>= "0.5"}
   "zarith" {>= "1.4"}
   "seq"

configure.ml

@@ -20,25 +20,6 @@ let static = ref false
 
 let pkg = ref ""
 
-(* this option add the possibility to choose the library that handle numbers in Alt-Ergo between zarith and nums *)
-type numbers_lib =
-  | Nums
-  | Zarith
-
-let print_numbers_lib = function
-  | Nums -> "Nums"
-  | Zarith -> "Zarith"
-
-let numbers_lib = ref Zarith
-
-let set_numbers_lib s =
-  match s with
-  | "nums" | "Nums" -> numbers_lib := Nums
-  | "zarith" | "Zarith" -> numbers_lib := Zarith
-  | _ ->
-    Format.eprintf "Unknown library name %s, use Nums or Zarith@." s;
-    exit 1
-
 (* Parse command line arguments *)
 let () =
   let args =
@@ -48,7 +29,6 @@ let () =
         ("--libdir", Arg.Set_string libdir, "<path> lib directory");
         ("--mandir", Arg.Set_string mandir, "<path> man directory");
         ("--static", Arg.Set static, " Enable statically compilation");
-        ("--numbers-lib", Arg.String set_numbers_lib, " Choose numbers library between Zarith and Nums");
       ]
   in
   let anon_fun s =
@@ -138,10 +118,6 @@ let () =
   let () = Format.fprintf fmt {|let libdir = "%s"@.|} !libdir in
   let () = Format.fprintf fmt {|let mandir = "%s"@.|} !mandir in
 
-  let () = Format.fprintf fmt {|type numbers_lib = | Nums | Zarith@.|} in
-  let () = Format.fprintf fmt {|let numbers_lib = %s@.|}
-      (print_numbers_lib !numbers_lib) in
-
   let () = Format.fprintf fmt {|
 (* Dynamic configuration, relative to the executable path *)
 

dune-project

@@ -108,7 +108,6 @@ See more details on http://alt-ergo.ocamlpro.com/"
   (dolmen (>= 0.8.1))
   (dolmen_type (>= 0.8.1))
   (dolmen_loop (>= 0.8.1))
-  num
   (ocplib-simplex (>= 0.5))
   (zarith (>= 1.4))
   seq

src/bin/gui/annoted_ast.ml

@@ -608,19 +608,15 @@ let print_tconstant fmt = function
   | Ttrue -> fprintf fmt "true"
   | Tfalse -> fprintf fmt "false"
   | Tint s -> fprintf fmt "%s" s
-  | Treal n -> fprintf fmt "%s" (Num.string_of_num n)
+  | Treal n -> fprintf fmt "%s" (Numbers.Q.to_string n)
   | Tbitv s -> fprintf fmt "%s" s
 
 let tconstant_to_string = function
   | Tvoid -> "void"
   | Ttrue -> "true"
   | Tfalse -> "false"
   | Tint s -> s
-  | Treal (Num.Int i) -> string_of_int i ^ "."
-  | Treal (Num.Big_int i) -> Big_int.string_of_big_int i ^ "."
-  | Treal (Num.Ratio r) ->
-    Big_int.string_of_big_int (Ratio.numerator_ratio r) ^ "./" ^
-    Big_int.string_of_big_int (Ratio.denominator_ratio r) ^ "."
+  | Treal n -> Numbers.Q.to_string n
   | Tbitv s -> s
 
 let rec print_var_list fmt = function

src/lib/dune

@@ -26,7 +26,6 @@
   (libraries
     seq
     unix
-    num
     str
     zarith
     dynlink
@@ -40,7 +39,7 @@
   )
 
   ; .mli only modules *also* need to be in this field
-  (modules_without_implementation matching_types numbersInterface sig sig_rel)
+  (modules_without_implementation matching_types sig sig_rel)
 
   ; modules that make up the lib
   (modules
@@ -58,8 +57,8 @@
     Expr Var Ty Typed Xliteral ModelMap
     ; util
     Config Emap Gc_debug Hconsing Hstring Iheap Lists Loc
-    MyDynlink MyUnix Numbers NumsNumbers NumbersInterface
-    Options Timers Util Vec Version ZarithNumbers Steps Printer Format_shims
+    MyDynlink MyUnix Numbers
+    Options Timers Util Vec Version Steps Printer Format_shims
     My_zip
   )
 

src/lib/frontend/cnf.ml

@@ -61,7 +61,7 @@ let rec make_term up_qv quant_basename t =
     | TTconst (Tint i) ->
       E.int i
     | TTconst (Treal n) ->
-      E.real (Num.string_of_num n)
+      E.real (Numbers.Q.to_string n)
     | TTconst (Tbitv bt) ->
       E.bitv bt ty
     | TTvar s -> E.mk_term s [] ty

src/lib/frontend/parsed_interface.mli

@@ -123,7 +123,7 @@ val mk_logic_type : ppure_type list -> ppure_type option -> plogic_type
 
 val mk_int_const  : Loc.t -> string -> lexpr
 
-val mk_real_const : Loc.t -> Num.num -> lexpr
+val mk_real_const : Loc.t -> Numbers.Q.t -> lexpr
 
 val mk_add : Loc.t -> lexpr -> lexpr -> lexpr
 

src/lib/frontend/typechecker.ml

@@ -528,7 +528,7 @@ let rec type_term ?(call_from_type_form=false) env f =
       TTconst(Tint ("-"^n)), Ty.Tint
     | PPprefix(PPneg, { pp_desc=PPconst (ConstReal n); _ }) ->
       Options.tool_req 1 (append_type "TR-Typing-OpUnarith type" Ty.Treal);
-      TTconst(Treal (Num.minus_num n)), Ty.Treal
+      TTconst(Treal (Numbers.Q.minus n)), Ty.Treal
     | PPprefix(PPneg, e) ->
       let te = type_term env e in
       let ty = Ty.shorten te.c.tt_ty in
@@ -838,9 +838,9 @@ and type_bound env bnd ty ~is_open ~is_lower =
       let ty_x, q =
         try match num with
           | ConstInt s  ->
-            Ty.Tint,  Numbers.Q.from_string s
+            Ty.Tint, Numbers.Q.from_string s
           | ConstReal s ->
-            Ty.Treal, Numbers.Q.from_string (Num.string_of_num s)
+            Ty.Treal, s
           | _ -> assert false
         with _ -> assert false (*numbers well constructed with regular exprs*)
       in

src/lib/index.mld

@@ -157,9 +157,6 @@ AltErgoLib.Vec
 AltErgoLib.Loc
 AltErgoLib.MyUnix
 AltErgoLib.Numbers
-AltErgoLib.ZarithNumbers
-AltErgoLib.NumsNumbers
-AltErgoLib.NumbersInterface
 }
 
 

src/lib/structures/parsed.ml

@@ -31,7 +31,7 @@
 type constant =
   | ConstBitv of string
   | ConstInt of string
-  | ConstReal of Num.num
+  | ConstReal of Numbers.Q.t
   | ConstTrue
   | ConstFalse
   | ConstVoid
@@ -41,7 +41,7 @@ let pp_const fmt =
   function
   | ConstBitv s -> fprintf fmt "%s" s
   | ConstInt s -> fprintf fmt "%s" s
-  | ConstReal v -> fprintf fmt "%s" (Num.string_of_num v)
+  | ConstReal v -> fprintf fmt "%s" (Numbers.Q.to_string v)
   | ConstTrue -> fprintf fmt "true"
   | ConstFalse -> fprintf fmt "false"
   | ConstVoid -> fprintf fmt "void"

src/lib/structures/parsed.mli

@@ -31,7 +31,7 @@
 type constant =
   | ConstBitv of string
   | ConstInt of string
-  | ConstReal of Num.num
+  | ConstReal of Numbers.Q.t
   | ConstTrue
   | ConstFalse
   | ConstVoid

src/lib/structures/typed.ml

@@ -43,7 +43,7 @@ let mk ?(annot=new_id ()) c = { c; annot; }
 
 type tconstant =
   | Tint of string
-  | Treal of Num.num
+  | Treal of Numbers.Q.t
   | Tbitv of string
   | Ttrue
   | Tfalse
@@ -201,7 +201,7 @@ let rec print_term =
     | TTconst (Tint n) ->
       fprintf fmt "%s" n
     | TTconst (Treal n) ->
-      fprintf fmt "%s" (Num.string_of_num n)
+      fprintf fmt "%s" (Numbers.Q.to_string n)
     | TTconst Tbitv s ->
       fprintf fmt "%s" s
     | TTvar s ->

src/lib/structures/typed.mli

@@ -56,12 +56,12 @@ val mk : ?annot:int -> 'a -> ('a, int) annoted
 
 type tconstant =
   (* TODO: make Tint hold an arbitrary precision integer ? *)
-  | Tint of string      (** An integer constant. *)
-  | Treal of Num.num    (** Real constant. *)
-  | Tbitv of string     (** Bitvector constant. *)
-  | Ttrue               (** The true boolean (or proposition ?) *)
-  | Tfalse              (** The false boolean *)
-  | Tvoid               (** The only value of type unit *)
+  | Tint of string        (** An integer constant. *)
+  | Treal of Numbers.Q.t  (** Real constant. *)
+  | Tbitv of string       (** Bitvector constant. *)
+  | Ttrue                 (** The true boolean (or proposition ?) *)
+  | Tfalse                (** The false boolean *)
+  | Tvoid                 (** The only value of type unit *)
 (** Typed constants. *)
 
 type oplogic =