4 files changed, 122 insertions, 72 deletions

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 87778f7f7b..82f8b5b3e2 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1279,7 +1279,8 @@ module M = struct
     let dump_expr i e =
       let rec dump_expr = function
         | Mc.PEX n ->
-          EConstr.mkRel (i + List.assoc (CoqToCaml.positive n) vars_idx)
+          EConstr.mkRel
+            (i + CList.assoc_f Int.equal (CoqToCaml.positive n) vars_idx)
         | Mc.PEc z -> dexpr.dump_cst z
         | Mc.PEadd (e1, e2) ->
           EConstr.mkApp (dexpr.dump_add, [|dump_expr e1; dump_expr e2|])
@@ -1294,7 +1295,9 @@ module M = struct
       dump_expr e
     in
     let mkop op e1 e2 =
-      try EConstr.mkApp (List.assoc op dexpr.dump_op, [|e1; e2|])
+      try
+        EConstr.mkApp
+          (CList.assoc_f Mutils.Hash.eq_op2 op dexpr.dump_op, [|e1; e2|])
       with Not_found ->
         EConstr.mkApp (Lazy.force coq_Eq, [|dexpr.interp_typ; e1; e2|])
     in
@@ -1480,7 +1483,8 @@ type ('synt_c, 'prf) domain_spec =
   ; (* is the type of the syntactic coeffs - Z , Q , Rcst *)
     dump_coeff : 'synt_c -> EConstr.constr
   ; proof_typ : EConstr.constr
-  ; dump_proof : 'prf -> EConstr.constr }
+  ; dump_proof : 'prf -> EConstr.constr
+  ; coeff_eq : 'synt_c -> 'synt_c -> bool }
 (**
   * The datastructures that aggregate theory-dependent proof values.
   *)
@@ -1491,7 +1495,8 @@ let zz_domain_spec =
     ; coeff = Lazy.force coq_Z
     ; dump_coeff = dump_z
     ; proof_typ = Lazy.force coq_proofTerm
-    ; dump_proof = dump_proof_term }
+    ; dump_proof = dump_proof_term
+    ; coeff_eq = Mc.zeq_bool }
 
 let qq_domain_spec =
   lazy
@@ -1499,7 +1504,8 @@ let qq_domain_spec =
     ; coeff = Lazy.force coq_Q
     ; dump_coeff = dump_q
     ; proof_typ = Lazy.force coq_QWitness
-    ; dump_proof = dump_psatz coq_Q dump_q }
+    ; dump_proof = dump_psatz coq_Q dump_q
+    ; coeff_eq = Mc.qeq_bool }
 
 let max_tag f =
   1 + Tag.to_int (Mc.foldA (fun t1 (t2, _) -> Tag.max t1 t2) f (Tag.from 0))
@@ -1603,7 +1609,12 @@ let witness_list_tags p g = witness_list p g
   * Prune the proof object, according to the 'diff' between two cnf formulas.
   *)
 
-let compact_proofs (cnf_ff : 'cst cnf) res (cnf_ff' : 'cst cnf) =
+let compact_proofs (eq_cst : 'cst -> 'cst -> bool) (cnf_ff : 'cst cnf) res
+    (cnf_ff' : 'cst cnf) =
+  let eq_formula (p1, o1) (p2, o2) =
+    let open Mutils.Hash in
+    eq_pol eq_cst p1 p2 && eq_op1 o1 o2
+  in
   let compact_proof (old_cl : 'cst clause) (prf, prover) (new_cl : 'cst clause)
       =
     let new_cl = List.mapi (fun i (f, _) -> (f, i)) new_cl in
@@ -1611,7 +1622,7 @@ let compact_proofs (cnf_ff : 'cst cnf) res (cnf_ff' : 'cst cnf) =
       let formula =
         try fst (List.nth old_cl i) with Failure _ -> failwith "bad old index"
       in
-      List.assoc formula new_cl
+      CList.assoc_f eq_formula formula new_cl
     in
     (* if debug then
        begin
@@ -1641,7 +1652,13 @@ let compact_proofs (cnf_ff : 'cst cnf) res (cnf_ff' : 'cst cnf) =
       (new_cl : 'cst clause) =
     let hyps_idx = prover.hyps prf in
     let hyps = selecti hyps_idx old_cl in
-    is_sublist ( = ) hyps new_cl
+    let eq (f1, (t1, e1)) (f2, (t2, e2)) =
+      Int.equal (Tag.compare t1 t2) 0
+      && eq_formula f1 f2
+      && (e1 : EConstr.t) = (e2 : EConstr.t)
+      (* FIXME: what equality should we use here? *)
+    in
+    is_sublist eq hyps new_cl
   in
   let cnf_res = List.combine cnf_ff res in
   (* we get pairs clause * proof *)
@@ -1798,7 +1815,7 @@ let micromega_tauto pre_process cnf spec prover env
            | None -> failwith "abstraction is wrong"
            | Some res -> ()
        end ; *)
-    let res' = compact_proofs cnf_ff res cnf_ff' in
+    let res' = compact_proofs spec.coeff_eq cnf_ff res cnf_ff' in
     let ff', res', ids = (ff', res', Mc.ids_of_formula ff') in
     let res' = dump_list spec.proof_typ spec.dump_proof res' in
     Prf (ids, ff', res')
@@ -1946,7 +1963,8 @@ let micromega_genr prover tac =
       ; coeff = Lazy.force coq_Rcst
       ; dump_coeff = dump_q
       ; proof_typ = Lazy.force coq_QWitness
-      ; dump_proof = dump_psatz coq_Q dump_q }
+      ; dump_proof = dump_psatz coq_Q dump_q
+      ; coeff_eq = Mc.qeq_bool }
   in
   Proofview.Goal.enter (fun gl ->
       let sigma = Tacmach.New.project gl in
@@ -1979,7 +1997,7 @@ let micromega_genr prover tac =
         | Prf (ids, ff', res') ->
           let ff, ids =
             formula_hyps_concl
-              (List.filter (fun (n, _) -> List.mem n ids) hyps)
+              (List.filter (fun (n, _) -> CList.mem_f Id.equal n ids) hyps)
               concl
           in
           let ff' = abstract_wrt_formula ff' ff in
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index f9a23751bf..27b917383b 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -385,7 +385,13 @@ module Hash = struct
   let int_of_eq_op1 =
     Mc.(function Equal -> 0 | NonEqual -> 1 | Strict -> 2 | NonStrict -> 3)
 
-  let eq_op1 o1 o2 = int_of_eq_op1 o1 = int_of_eq_op1 o2
+  let int_of_eq_op2 =
+    Mc.(
+      function
+      | OpEq -> 0 | OpNEq -> 1 | OpLe -> 2 | OpGe -> 3 | OpLt -> 4 | OpGt -> 5)
+
+  let eq_op1 o1 o2 = Int.equal (int_of_eq_op1 o1) (int_of_eq_op1 o2)
+  let eq_op2 o1 o2 = Int.equal (int_of_eq_op2 o1) (int_of_eq_op2 o2)
   let hash_op1 h o = combine h (int_of_eq_op1 o)
 
   let rec eq_positive p1 p2 =
diff --git a/plugins/micromega/mutils.mli b/plugins/micromega/mutils.mli
index 5e0c913996..146860ca00 100644
--- a/plugins/micromega/mutils.mli
+++ b/plugins/micromega/mutils.mli
@@ -43,6 +43,7 @@ module Tag : sig
   val max : t -> t -> t
   val from : int -> t
   val to_int : t -> int
+  val compare : t -> t -> int
 end
 
 module TagSet : CSig.SetS with type elt = Tag.t
@@ -73,6 +74,7 @@ end
 
 module Hash : sig
   val eq_op1 : Micromega.op1 -> Micromega.op1 -> bool
+  val eq_op2 : Micromega.op2 -> Micromega.op2 -> bool
   val eq_positive : Micromega.positive -> Micromega.positive -> bool
   val eq_z : Micromega.z -> Micromega.z -> bool
   val eq_q : Micromega.q -> Micromega.q -> bool
diff --git a/plugins/micromega/vect.ml b/plugins/micromega/vect.ml
index 1742f81b34..15f37868f7 100644
--- a/plugins/micromega/vect.ml
+++ b/plugins/micromega/vect.ml
@@ -19,7 +19,8 @@ type var = int
         - values are all non-zero
  *)
 
-type t = (var * Q.t) list
+type mono = {var : var; coe : Q.t}
+type t = mono list
 type vector = t
 
 (** [equal v1 v2 = true] if the vectors are syntactically equal. *)
@@ -29,21 +30,25 @@ let rec equal v1 v2 =
   | [], [] -> true
   | [], _ -> false
   | _ :: _, [] -> false
-  | (i1, n1) :: v1, (i2, n2) :: v2 -> Int.equal i1 i2 && n1 =/ n2 && equal v1 v2
+  | {var = i1; coe = n1} :: v1, {var = i2; coe = n2} :: v2 ->
+    Int.equal i1 i2 && n1 =/ n2 && equal v1 v2
 
 let hash v =
   let rec hash i = function
     | [] -> i
-    | (vr, vl) :: l -> hash (i + Hashtbl.hash (vr, Q.to_float vl)) l
+    | {var = vr; coe = 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 [] -> true | [(0, x)] when Q.zero =/ x -> true | _ -> false
+  match v with
+  | [] -> true
+  | [{var = 0; coe = x}] when Q.zero =/ x -> true
+  | _ -> false
 
-let pp_var_num pp_var o (v, n) =
+let pp_var_num pp_var o {var = v; coe = n} =
   if Int.equal v 0 then
     if Q.zero =/ n then () else Printf.fprintf o "%s" (Q.to_string n)
   else if Q.one =/ n then pp_var o v
@@ -51,7 +56,7 @@ let pp_var_num pp_var o (v, n) =
   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) =
+let pp_var_num_smt pp_var o {var = v; coe = n} =
   if Int.equal v 0 then
     if Q.zero =/ n then () else Printf.fprintf o "%s" (Q.to_string n)
   else if Q.one =/ n then pp_var o v
@@ -79,7 +84,7 @@ let from_list (l : Q.t list) =
     match l with
     | [] -> []
     | e :: l ->
-      if e <>/ Q.zero then (i, e) :: xfrom_list (i + 1) l
+      if e <>/ Q.zero then {var = i; coe = e} :: xfrom_list (i + 1) l
       else xfrom_list (i + 1) l
   in
   xfrom_list 0 l
@@ -88,68 +93,71 @@ 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 Q.zero :: xto_list (i + 1) l
+    | {var = x; coe = v} :: l' ->
+      if Int.equal 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 =/ Q.zero then rst else (i, v) :: rst
+let cons i v rst = if v =/ Q.zero then rst else {var = i; coe = v} :: rst
 
 let rec update i f t =
   match t with
   | [] -> cons i (f Q.zero) []
-  | (k, v) :: l -> (
-    match Int.compare i k with
-    | 0 -> cons k (f v) l
+  | x :: l -> (
+    match Int.compare i x.var with
+    | 0 -> cons x.var (f x.coe) l
     | -1 -> cons i (f Q.zero) t
-    | 1 -> (k, v) :: update i f l
+    | 1 -> x :: update i f l
     | _ -> failwith "compare_num" )
 
 let rec set i n t =
   match t with
   | [] -> cons i n []
-  | (k, v) :: l -> (
-    match Int.compare i k with
-    | 0 -> cons k n l
+  | x :: l -> (
+    match Int.compare i x.var with
+    | 0 -> cons x.var n l
     | -1 -> cons i n t
-    | 1 -> (k, v) :: set i n l
+    | 1 -> x :: set i n l
     | _ -> failwith "compare_num" )
 
-let cst n = if n =/ Q.zero then [] else [(0, n)]
+let cst n = if n =/ Q.zero then [] else [{var = 0; coe = n}]
 
 let mul z t =
   if z =/ Q.zero then []
   else if z =/ Q.one then t
-  else List.map (fun (i, n) -> (i, z */ n)) t
+  else List.map (fun {var = i; coe = n} -> {var = i; coe = z */ n}) t
 
 let div z t =
-  if z <>/ Q.one then List.map (fun (x, nx) -> (x, nx // z)) t else t
+  if z <>/ Q.one then
+    List.map (fun {var = x; coe = nx} -> {var = x; coe = nx // z}) t
+  else t
 
-let uminus t = List.map (fun (i, n) -> (i, Q.neg n)) t
+let uminus t = List.map (fun {var = i; coe = n} -> {var = i; coe = Q.neg n}) t
 
 let rec add (ve1 : t) (ve2 : t) =
   match (ve1, ve2) with
   | [], v | v, [] -> v
-  | (v1, c1) :: l1, (v2, c2) :: l2 ->
+  | {var = v1; coe = c1} :: l1, {var = v2; coe = c2} :: l2 ->
     let cmp = Int.compare v1 v2 in
     if cmp == 0 then
       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
+      if Q.zero =/ s then add l1 l2 else {var = v1; coe = s} :: add l1 l2
+    else if cmp < 0 then {var = v1; coe = c1} :: add l1 ve2
+    else {var = v2; coe = c2} :: add l2 ve1
 
 let rec xmul_add (n1 : Q.t) (ve1 : t) (n2 : Q.t) (ve2 : t) =
   match (ve1, ve2) with
   | [], _ -> mul n2 ve2
   | _, [] -> mul n1 ve1
-  | (v1, c1) :: l1, (v2, c2) :: l2 ->
+  | {var = v1; coe = c1} :: l1, {var = v2; coe = c2} :: l2 ->
     let cmp = Int.compare v1 v2 in
     if cmp == 0 then
       let s = (n1 */ c1) +/ (n2 */ c2) in
       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
+      else {var = v1; coe = s} :: xmul_add n1 l1 n2 l2
+    else if cmp < 0 then {var = v1; coe = n1 */ c1} :: xmul_add n1 l1 n2 ve2
+    else {var = v2; coe = n2 */ c2} :: xmul_add n1 ve1 n2 l2
 
 let mul_add n1 ve1 n2 ve2 =
   if n1 =/ Q.one && n2 =/ Q.one then add ve1 ve2 else xmul_add n1 ve1 n2 ve2
@@ -157,8 +165,7 @@ let mul_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 () -> Q.compare (snd x) (snd y)) ])
+        [(fun () -> Int.compare x.var y.var); (fun () -> Q.compare x.coe y.coe)])
 
 (** [tail v vect] returns
         - [None] if [v] is not a variable of the vector [vect]
@@ -169,7 +176,7 @@ let compare : t -> t -> int =
 let rec tail (v : var) (vect : t) =
   match vect with
   | [] -> None
-  | (v', vl) :: vect' -> (
+  | {var = v'; coe = vl} :: vect' -> (
     match Int.compare v' v with
     | 0 -> Some (vl, vect) (* Ok, found *)
     | -1 -> tail v vect' (* Might be in the tail *)
@@ -178,38 +185,49 @@ let rec tail (v : var) (vect : t) =
 (* Hopeless *)
 
 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 | _ -> 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) | _ -> (Q.zero, v)
+let is_constant v = match v with [] | [{var = 0}] -> true | _ -> false
+let get_cst vect = match vect with {var = 0; coe = v} :: _ -> v | _ -> Q.zero
+
+let choose v =
+  match v with [] -> None | {var = vr; coe = vl} :: rst -> Some (vr, vl, rst)
+
+let rec fresh v =
+  match v with [] -> 1 | [{var = v}] -> v + 1 | _ :: v -> fresh v
+
+let variables v =
+  List.fold_left (fun acc {var = x} -> ISet.add x acc) ISet.empty v
+
+let decomp_cst v =
+  match v with {var = 0; coe = vl} :: v -> (vl, v) | _ -> (Q.zero, v)
 
 let rec decomp_at i v =
   match v with
   | [] -> (Q.zero, null)
-  | (vr, vl) :: r ->
-    if i = vr then (vl, r) else if i < vr then (Q.zero, v) else decomp_at i r
+  | {var = vr; coe = vl} :: r ->
+    if Int.equal 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, Q.zero), []) | x :: v -> (x, v)
+let decomp_fst v =
+  match v with [] -> ((0, Q.zero), []) | x :: v -> ((x.var, x.coe), v)
 
 let rec subst (vr : int) (e : t) (v : t) =
   match v with
   | [] -> []
-  | (x, n) :: v' -> (
+  | {var = x; coe = n} :: v' -> (
     match Int.compare vr x with
     | 0 -> mul_add n e Q.one v'
     | -1 -> v
-    | 1 -> add [(x, n)] (subst vr e v')
+    | 1 -> add [{var = x; coe = n}] (subst vr e v')
     | _ -> assert false )
 
-let fold f acc v = List.fold_left (fun acc (v, i) -> f acc v i) acc v
+let fold f acc v = List.fold_left (fun acc x -> f acc x.var x.coe) acc v
 
 let fold_error f acc v =
   let rec fold acc v =
     match v with
     | [] -> Some acc
-    | (x, i) :: v' -> (
+    | {var = x; coe = i} :: v' -> (
       match f acc x i with None -> None | Some acc' -> fold acc' v' )
   in
   fold acc v
@@ -217,11 +235,12 @@ let fold_error f acc v =
 let rec find p v =
   match v with
   | [] -> None
-  | (v, n) :: v' -> ( match p v n with None -> find p v' | Some r -> Some r )
+  | {var = v; coe = n} :: v' -> (
+    match p v n with None -> find p v' | Some r -> Some r )
 
-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
+let for_all p l = List.for_all (fun {var = v; coe = n} -> p v n) l
+let decr_var i v = List.map (fun x -> {x with var = x.var - i}) v
+let incr_var i v = List.map (fun x -> {x with var = x.var + i}) v
 
 let gcd v =
   let res =
@@ -239,12 +258,15 @@ let normalise v =
     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 */ Q.of_bigint ppcm // Q.of_bigint gcd)) v
+  List.map
+    (fun {var = x; coe = v} ->
+      {var = x; coe = v */ Q.of_bigint ppcm // Q.of_bigint gcd})
+    v
 
 let rec exists2 p vect1 vect2 =
   match (vect1, vect2) with
   | _, [] | [], _ -> None
-  | (v1, n1) :: vect1', (v2, n2) :: vect2' ->
+  | {var = v1; coe = n1} :: vect1', {var = v2; coe = n2} :: vect2' ->
     if Int.equal v1 v2 then
       if p n1 n2 then Some (v1, n1, n2) else exists2 p vect1' vect2'
     else if v1 < v2 then exists2 p vect1' vect2
@@ -254,26 +276,26 @@ let dotproduct v1 v2 =
   let rec dot acc v1 v2 =
     match (v1, v2) with
     | [], _ | _, [] -> acc
-    | (x1, n1) :: v1', (x2, n2) :: v2' ->
-      if x1 == x2 then dot (acc +/ (n1 */ n2)) v1' v2'
+    | {var = x1; coe = n1} :: v1', {var = x2; coe = n2} :: v2' ->
+      if Int.equal x1 x2 then dot (acc +/ (n1 */ n2)) v1' v2'
       else if x1 < x2 then dot acc v1' v2
       else dot acc v1 v2'
   in
   dot Q.zero v1 v2
 
-let map f v = List.map (fun (x, v) -> f x v) v
+let map f v = List.map (fun {var = x; coe = v} -> f x v) v
 
 let abs_min_elt v =
   match v with
   | [] -> None
-  | (v, vl) :: r ->
+  | {var = v; coe = vl} :: r ->
     Some
       (List.fold_left
-         (fun (v1, vl1) (v2, vl2) ->
+         (fun (v1, vl1) {var = v2; coe = 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 partition p = List.partition (fun {var = vr; coe = vl} -> p vr vl)
 let mkvar x = set x Q.one null
 
 module Bound = struct
@@ -281,7 +303,9 @@ module Bound = struct
 
   let of_vect (v : vector) =
     match v with
-    | [(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'}
+    | [{var = x; coe = v}] ->
+      if Int.equal x 0 then None else Some {cst = Q.zero; var = x; coeff = v}
+    | [{var = 0; coe = v}; {var = x; coe = v'}] ->
+      Some {cst = v; var = x; coeff = v'}
     | _ -> None
 end