[micromega] Add numerical compatibility layer.

Only significant change is in gcd / lcm which now are typed in `Z.t`

1 files changed, 55 insertions, 61 deletions

diff --git a/plugins/micromega/vect.ml b/plugins/micromega/vect.ml
index f53a7b42c9..198430295b 100644
--- a/plugins/micromega/vect.ml
+++ b/plugins/micromega/vect.ml
@@ -8,7 +8,8 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Num
+open NumCompat
+open Q.Notations
 open Mutils
 
 type var = int
@@ -18,7 +19,7 @@ type var = int
         - values are all non-zero
  *)
 
-type t = (var * num) list
+type t = (var * Q.t) list
 type vector = t
 
 (** [equal v1 v2 = true] if the vectors are syntactically equal. *)
@@ -33,32 +34,30 @@ let rec equal v1 v2 =
 let hash v =
   let rec hash i = function
     | [] -> i
-    | (vr, vl) :: l -> hash (i + Hashtbl.hash (vr, float_of_num vl)) l
+    | (vr, vl) :: l -> hash (i + Hashtbl.hash (vr, Q.to_float vl)) l
   in
   Hashtbl.hash (hash 0 v)
 
 let null = []
-let is_null v = match v with [] | [(0, Int 0)] -> true | _ -> false
+
+let is_null v =
+  match v with [] -> true | [(0, x)] when Q.zero =/ x -> true | _ -> false
 
 let pp_var_num pp_var o (v, n) =
   if Int.equal v 0 then
-    if eq_num (Int 0) n then () else Printf.fprintf o "%s" (string_of_num n)
-  else
-    match n with
-    | Int 1 -> pp_var o v
-    | Int -1 -> Printf.fprintf o "-%a" pp_var v
-    | Int 0 -> ()
-    | _ -> Printf.fprintf o "%s*%a" (string_of_num n) pp_var v
+    if Q.zero =/ n then () else Printf.fprintf o "%s" (Q.to_string n)
+  else if Q.one =/ n then pp_var o v
+  else if Q.neg_one =/ n then Printf.fprintf o "-%a" pp_var v
+  else if Q.zero =/ n then ()
+  else Printf.fprintf o "%s*%a" (Q.to_string n) pp_var v
 
 let pp_var_num_smt pp_var o (v, n) =
   if Int.equal v 0 then
-    if eq_num (Int 0) n then () else Printf.fprintf o "%s" (string_of_num n)
-  else
-    match n with
-    | Int 1 -> pp_var o v
-    | Int -1 -> Printf.fprintf o "(- %a)" pp_var v
-    | Int 0 -> ()
-    | _ -> Printf.fprintf o "(* %s %a)" (string_of_num n) pp_var v
+    if Q.zero =/ n then () else Printf.fprintf o "%s" (Q.to_string n)
+  else if Q.one =/ n then pp_var o v
+  else if Q.neg_one =/ n then Printf.fprintf o "(- %a)" pp_var v
+  else if Q.zero =/ n then ()
+  else Printf.fprintf o "(* %s %a)" (Q.to_string n) pp_var v
 
 let rec pp_gen pp_var o v =
   match v with
@@ -75,36 +74,34 @@ let pp_smt o v =
   in
   Printf.fprintf o "(+ %a)" list v
 
-let from_list (l : num list) =
+let from_list (l : Q.t list) =
   let rec xfrom_list i l =
     match l with
     | [] -> []
     | e :: l ->
-      if e <>/ Int 0 then (i, e) :: xfrom_list (i + 1) l
+      if e <>/ Q.zero then (i, e) :: xfrom_list (i + 1) l
       else xfrom_list (i + 1) l
   in
   xfrom_list 0 l
 
-let zero_num = Int 0
-
 let to_list m =
   let rec xto_list i l =
     match l with
     | [] -> []
     | (x, v) :: l' ->
-      if i = x then v :: xto_list (i + 1) l' else zero_num :: xto_list (i + 1) l
+      if i = x then v :: xto_list (i + 1) l' else Q.zero :: xto_list (i + 1) l
   in
   xto_list 0 m
 
-let cons i v rst = if v =/ Int 0 then rst else (i, v) :: rst
+let cons i v rst = if v =/ Q.zero then rst else (i, v) :: rst
 
 let rec update i f t =
   match t with
-  | [] -> cons i (f zero_num) []
+  | [] -> cons i (f Q.zero) []
   | (k, v) :: l -> (
     match Int.compare i k with
     | 0 -> cons k (f v) l
-    | -1 -> cons i (f zero_num) t
+    | -1 -> cons i (f Q.zero) t
     | 1 -> (k, v) :: update i f l
     | _ -> failwith "compare_num" )
 
@@ -118,18 +115,17 @@ let rec set i n t =
     | 1 -> (k, v) :: set i n l
     | _ -> failwith "compare_num" )
 
-let cst n = if n =/ Int 0 then [] else [(0, n)]
+let cst n = if n =/ Q.zero then [] else [(0, n)]
 
 let mul z t =
-  match z with
-  | Int 0 -> []
-  | Int 1 -> t
-  | _ -> List.map (fun (i, n) -> (i, mult_num z n)) t
+  if z =/ Q.zero then []
+  else if z =/ Q.one then t
+  else List.map (fun (i, n) -> (i, z */ n)) t
 
 let div z t =
-  if z <>/ Int 1 then List.map (fun (x, nx) -> (x, nx // z)) t else t
+  if z <>/ Q.one then List.map (fun (x, nx) -> (x, nx // z)) t else t
 
-let uminus t = List.map (fun (i, n) -> (i, minus_num n)) t
+let uminus t = List.map (fun (i, n) -> (i, Q.neg n)) t
 
 let rec add (ve1 : t) (ve2 : t) =
   match (ve1, ve2) with
@@ -137,12 +133,12 @@ let rec add (ve1 : t) (ve2 : t) =
   | (v1, c1) :: l1, (v2, c2) :: l2 ->
     let cmp = Int.compare v1 v2 in
     if cmp == 0 then
-      let s = add_num c1 c2 in
-      if eq_num (Int 0) s then add l1 l2 else (v1, s) :: add l1 l2
+      let s = c1 +/ c2 in
+      if Q.zero =/ s then add l1 l2 else (v1, s) :: add l1 l2
     else if cmp < 0 then (v1, c1) :: add l1 ve2
     else (v2, c2) :: add l2 ve1
 
-let rec xmul_add (n1 : num) (ve1 : t) (n2 : num) (ve2 : t) =
+let rec xmul_add (n1 : Q.t) (ve1 : t) (n2 : Q.t) (ve2 : t) =
   match (ve1, ve2) with
   | [], _ -> mul n2 ve2
   | _, [] -> mul n1 ve1
@@ -150,19 +146,19 @@ let rec xmul_add (n1 : num) (ve1 : t) (n2 : num) (ve2 : t) =
     let cmp = Int.compare v1 v2 in
     if cmp == 0 then
       let s = (n1 */ c1) +/ (n2 */ c2) in
-      if eq_num (Int 0) s then xmul_add n1 l1 n2 l2
+      if Q.zero =/ s then xmul_add n1 l1 n2 l2
       else (v1, s) :: xmul_add n1 l1 n2 l2
     else if cmp < 0 then (v1, n1 */ c1) :: xmul_add n1 l1 n2 ve2
     else (v2, n2 */ c2) :: xmul_add n1 ve1 n2 l2
 
 let mul_add n1 ve1 n2 ve2 =
-  if n1 =/ Int 1 && n2 =/ Int 1 then add ve1 ve2 else xmul_add n1 ve1 n2 ve2
+  if n1 =/ Q.one && n2 =/ Q.one then add ve1 ve2 else xmul_add n1 ve1 n2 ve2
 
 let compare : t -> t -> int =
   Mutils.Cmp.compare_list (fun x y ->
       Mutils.Cmp.compare_lexical
         [ (fun () -> Int.compare (fst x) (fst y))
-        ; (fun () -> compare_num (snd x) (snd y)) ])
+        ; (fun () -> Q.compare (snd x) (snd y)) ])
 
 (** [tail v vect] returns
         - [None] if [v] is not a variable of the vector [vect]
@@ -181,28 +177,28 @@ let rec tail (v : var) (vect : t) =
 
 (* Hopeless *)
 
-let get v vect = match tail v vect with None -> Int 0 | Some (vl, _) -> vl
+let get v vect = match tail v vect with None -> Q.zero | Some (vl, _) -> vl
 let is_constant v = match v with [] | [(0, _)] -> true | _ -> false
-let get_cst vect = match vect with (0, v) :: _ -> v | _ -> Int 0
+let get_cst vect = match vect with (0, v) :: _ -> v | _ -> Q.zero
 let choose v = match v with [] -> None | (vr, vl) :: rst -> Some (vr, vl, rst)
 let rec fresh v = match v with [] -> 1 | [(v, _)] -> v + 1 | _ :: v -> fresh v
 let variables v = List.fold_left (fun acc (x, _) -> ISet.add x acc) ISet.empty v
-let decomp_cst v = match v with (0, vl) :: v -> (vl, v) | _ -> (Int 0, v)
+let decomp_cst v = match v with (0, vl) :: v -> (vl, v) | _ -> (Q.zero, v)
 
 let rec decomp_at i v =
   match v with
-  | [] -> (Int 0, null)
+  | [] -> (Q.zero, null)
   | (vr, vl) :: r ->
-    if i = vr then (vl, r) else if i < vr then (Int 0, v) else decomp_at i r
+    if i = vr then (vl, r) else if i < vr then (Q.zero, v) else decomp_at i r
 
-let decomp_fst v = match v with [] -> ((0, Int 0), []) | x :: v -> (x, v)
+let decomp_fst v = match v with [] -> ((0, Q.zero), []) | x :: v -> (x, v)
 
 let rec subst (vr : int) (e : t) (v : t) =
   match v with
   | [] -> []
   | (x, n) :: v' -> (
     match Int.compare vr x with
-    | 0 -> mul_add n e (Int 1) v'
+    | 0 -> mul_add n e Q.one v'
     | -1 -> v
     | 1 -> add [(x, n)] (subst vr e v')
     | _ -> assert false )
@@ -227,25 +223,23 @@ let for_all p l = List.for_all (fun (v, n) -> p v n) l
 let decr_var i v = List.map (fun (v, n) -> (v - i, n)) v
 let incr_var i v = List.map (fun (v, n) -> (v + i, n)) v
 
-open Big_int
-
 let gcd v =
   let res =
     fold
       (fun c _ n ->
-        assert (Int.equal (compare_big_int (denominator n) unit_big_int) 0);
-        gcd_big_int c (numerator n))
-      zero_big_int v
+        assert (Int.equal (Z.compare (Q.den n) Z.one) 0);
+        Z.gcd c (Q.num n))
+      Z.zero v
   in
-  if Int.equal (compare_big_int res zero_big_int) 0 then unit_big_int else res
+  if Int.equal (Z.compare res Z.zero) 0 then Z.one else res
 
 let normalise v =
-  let ppcm = fold (fun c _ n -> ppcm c (denominator n)) unit_big_int v in
+  let ppcm = fold (fun c _ n -> Z.ppcm c (Q.den n)) Z.one v in
   let gcd =
-    let gcd = fold (fun c _ n -> gcd_big_int c (numerator n)) zero_big_int v in
-    if Int.equal (compare_big_int gcd zero_big_int) 0 then unit_big_int else gcd
+    let gcd = fold (fun c _ n -> Z.gcd c (Q.num n)) Z.zero v in
+    if Int.equal (Z.compare gcd Z.zero) 0 then Z.one else gcd
   in
-  List.map (fun (x, v) -> (x, v */ Big_int ppcm // Big_int gcd)) v
+  List.map (fun (x, v) -> (x, v */ Q.of_bigint ppcm // Q.of_bigint gcd)) v
 
 let rec exists2 p vect1 vect2 =
   match (vect1, vect2) with
@@ -265,7 +259,7 @@ let dotproduct v1 v2 =
       else if x1 < x2 then dot acc v1' v2
       else dot acc v1 v2'
   in
-  dot (Int 0) v1 v2
+  dot Q.zero v1 v2
 
 let map f v = List.map (fun (x, v) -> f x v) v
 
@@ -276,18 +270,18 @@ let abs_min_elt v =
     Some
       (List.fold_left
          (fun (v1, vl1) (v2, vl2) ->
-           if abs_num vl1 </ abs_num vl2 then (v1, vl1) else (v2, vl2))
+           if Q.abs vl1 </ Q.abs vl2 then (v1, vl1) else (v2, vl2))
          (v, vl) r)
 
 let partition p = List.partition (fun (vr, vl) -> p vr vl)
-let mkvar x = set x (Int 1) null
+let mkvar x = set x Q.one null
 
 module Bound = struct
-  type t = {cst : num; var : var; coeff : num}
+  type t = {cst : Q.t; var : var; coeff : Q.t}
 
   let of_vect (v : vector) =
     match v with
-    | [(x, v)] -> if x = 0 then None else Some {cst = Int 0; var = x; coeff = v}
+    | [(x, v)] -> if x = 0 then None else Some {cst = Q.zero; var = x; coeff = v}
     | [(0, v); (x, v')] -> Some {cst = v; var = x; coeff = v'}
     | _ -> None
 end