Imported Upstream version 8.6upstream/8.6

8 files changed, 169 insertions, 121 deletions

diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v
index 3068b534..b11d15e5 100644
--- a/plugins/nsatz/Nsatz.v
+++ b/plugins/nsatz/Nsatz.v
@@ -298,7 +298,9 @@ Ltac nsatz_call_n info nparam p rr lp kont :=
   match goal with
   | |- (?c::PEpow _ ?r::?lq0)::?lci0 = _ -> _ =>
     intros _;
+    let lci := fresh "lci" in
     set (lci:=lci0);
+    let lq := fresh "lq" in
     set (lq:=lq0);
     kont c rr lq lci
   end.
@@ -380,10 +382,13 @@ Ltac nsatz_generic radicalmax info lparam lvar :=
     end in 
 
   SplitPolyList ltac:(fun p lp =>
+    let p21 := fresh "p21" in
+    let lp21 := fresh "lp21" in
     set (p21:=p) ;
     set (lp21:=lp);
 (*    idtac "nparam:"; idtac nparam; idtac "p:"; idtac p; idtac "lp:"; idtac lp; *)
     nsatz_call radicalmax info nparam p lp ltac:(fun c r lq lci => 
+      let q := fresh "q" in
       set (q := PEmul c (PEpow p21 r)); 
       let Hg := fresh "Hg" in 
       assert (Hg:check lp21 q (lci,lq) = true); 
diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4
new file mode 100644
index 00000000..5f906a8d
--- /dev/null
+++ b/plugins/nsatz/g_nsatz.ml4
@@ -0,0 +1,17 @@
+DECLARE PLUGIN "nsatz_plugin"
+
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i camlp4deps: "grammar/grammar.cma" i*)
+
+DECLARE PLUGIN "nsatz_plugin"
+
+TACTIC EXTEND nsatz_compute
+| [ "nsatz_compute"  constr(lt) ] -> [ Nsatz.nsatz_compute lt ]
+END
diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index 482ce505..48bdad82 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -19,75 +19,6 @@ open Utile
 
 exception NotInIdeal
 
-module type S = sig
-
-(* Monomials *)
-type mon = int array
-
-val mult_mon : mon -> mon -> mon
-val deg : mon -> int
-val compare_mon : mon -> mon -> int
-val div_mon : mon -> mon -> mon
-val div_mon_test : mon -> mon -> bool
-val ppcm_mon : mon -> mon -> mon
-
-(* Polynomials *)
-
-type deg = int
-type coef
-type poly
-type polynom 
-
-val repr : poly -> (coef * mon) list
-val polconst : coef -> poly
-val zeroP : poly
-val gen : int -> poly
-
-val equal : poly -> poly -> bool
-val name_var : string list ref
-val getvar : string list -> int -> string
-val lstringP : poly list -> string
-val printP : poly -> unit
-val lprintP : poly list -> unit
-
-val div_pol_coef : poly -> coef -> poly
-val plusP : poly -> poly -> poly
-val mult_t_pol : coef -> mon -> poly -> poly
-val selectdiv : mon -> poly list -> poly
-val oppP : poly -> poly
-val emultP : coef -> poly -> poly
-val multP : poly -> poly -> poly
-val puisP : poly -> int -> poly
-val contentP : poly -> coef
-val contentPlist : poly list -> coef
-val pgcdpos : coef -> coef -> coef
-val div_pol : poly -> poly -> coef -> coef -> mon -> poly
-val reduce2 : poly -> poly list -> coef * poly
-
-val poldepcontent : coef list ref
-val coefpoldep_find : poly -> poly -> poly
-val coefpoldep_set : poly -> poly -> poly -> unit
-val initcoefpoldep : poly list -> unit
-val reduce2_trace : poly -> poly list -> poly list -> poly list * poly
-val spol : poly -> poly -> poly
-val etrangers : poly -> poly -> bool
-val div_ppcm : poly -> poly -> poly -> bool
-
-val genPcPf : poly -> poly list -> poly list -> poly list
-val genOCPf : poly list -> poly list
-
-val is_homogeneous : poly -> bool
-
-type certificate =
-    { coef : coef; power : int;
-      gb_comb : poly list list; last_comb : poly list }
-
-val test_dans_ideal : poly -> poly list -> poly list ->
-  poly list * poly * certificate
-val in_ideal : deg -> poly list -> poly -> poly list * poly * certificate
-
-end
-
 (***********************************************************************
    Global options
 *)
@@ -127,11 +58,11 @@ type polynom =
     num : int;
     sugar : int}
 
-let nvar m =  Array.length m - 1
+let nvar (m : mon) =  Array.length m - 1
 
-let deg m = m.(0)
+let deg (m : mon) = m.(0)
 
-let mult_mon m m' =
+let mult_mon (m : mon) (m' : mon) =
   let d = nvar m in
   let m'' = Array.make (d+1) 0 in
   for i=0 to d do
@@ -140,7 +71,7 @@ let mult_mon m m' =
   m''
 
 
-let compare_mon m m' =
+let compare_mon (m : mon) (m' : mon) =
   let d = nvar m in
   if !lexico
   then (
@@ -148,18 +79,18 @@ let compare_mon m m' =
     let res=ref 0 in
     let i=ref 1 in (* 1 si lexico pur 0 si degre*)
     while (!res=0) && (!i<=d) do
-      res:= (compare m.(!i) m'.(!i));
+      res:= (Int.compare m.(!i) m'.(!i));
       i:=!i+1;
     done;
     !res)
   else (
      (* degre lexicographique inverse *)
-    match compare m.(0) m'.(0) with
+    match Int.compare m.(0) m'.(0) with
     | 0 -> (* meme degre total *)
 	let res=ref 0 in
 	let i=ref d in
 	while (!res=0) && (!i>=1) do
-	  res:= - (compare m.(!i) m'.(!i));
+	  res:= - (Int.compare m.(!i) m'.(!i));
 	  i:=!i-1;
 	done;
 	!res
@@ -402,29 +333,25 @@ let polconst d c =
   [(c,m)]
 
 let plusP p q =
-  let rec plusP p q =
-    match p with
-      [] -> q
-    |t::p' -> 
-	match q with
-	  [] -> p
-	|t'::q' ->
-            match compare_mon (snd t) (snd t') with
-              1 -> t::(plusP p' q)
-            |(-1) -> t'::(plusP p q')
-            |_ -> let c=P.plusP (fst t) (fst t') in
-              match P.equal c coef0 with
-                true -> (plusP p' q')
-              |false -> (c,(snd t))::(plusP p' q')
-  in plusP p q
+  let rec plusP p q accu = match p, q with
+  | [], [] -> List.rev accu
+  | [], _ -> List.rev_append accu q
+  | _, [] -> List.rev_append accu p
+  | t :: p', t' :: q' ->
+    let c = compare_mon (snd t) (snd t') in
+    if c > 0 then plusP p' q (t :: accu)
+    else if c < 0 then plusP p q' (t' :: accu)
+    else
+      let c = P.plusP (fst t) (fst t') in
+      if P.equal c coef0 then plusP p' q' accu
+      else plusP p' q' ((c, (snd t)) :: accu)
+  in
+  plusP p q []
 
 (* multiplication by (a,monomial) *)
 let mult_t_pol a m p =
-  let rec mult_t_pol p =
-    match p with
-      [] -> []
-    |(b,m')::p -> ((P.multP a b),(mult_mon m m'))::(mult_t_pol p)
-  in mult_t_pol p
+  let map (b, m') = (P.multP a b, mult_mon m m') in
+  CList.map map p
 
 let coef_of_int x = P.of_num (Num.Int x)
 
@@ -451,23 +378,27 @@ let emultP a p =
   in emultP p
 
 let multP p q =
-  let rec aux p =
+  let rec aux p accu =
     match p with
-      [] -> []
-    |(a,m)::p' -> plusP (mult_t_pol a m q) (aux p')
-  in aux p
+      [] -> accu
+    |(a,m)::p' -> aux p' (plusP (mult_t_pol a m q) accu)
+  in aux p []
 
 let puisP p n=
   match p with
     [] -> []
   |_ ->
+    if n = 0 then
       let d = nvar (snd (List.hd p)) in
-      let rec puisP n =
-	match n with
-	  0 -> [coef1, Array.make (d+1) 0]
-	| 1 -> p
-	|_ -> multP p (puisP (n-1))
-      in puisP n
+      [coef1, Array.make (d+1) 0]
+    else
+      let rec puisP p n =
+        if n = 1 then p
+        else
+          let q = puisP p (n / 2) in
+          let q = multP q q in
+          if n mod 2 = 0 then q else multP p q
+      in puisP p n
 	
 let rec contentP p =
   match p with
diff --git a/plugins/nsatz/ideal.mli b/plugins/nsatz/ideal.mli
new file mode 100644
index 00000000..d1a2a0a7
--- /dev/null
+++ b/plugins/nsatz/ideal.mli
@@ -0,0 +1,47 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+module Make (P : Polynom.S) :
+sig
+(* Polynomials *)
+
+type deg = int
+type coef = P.t
+type poly
+
+val repr : poly -> (coef * int array) list
+val polconst : int -> coef -> poly
+val zeroP : poly
+val gen : int -> int -> poly
+
+val equal : poly -> poly -> bool
+val name_var : string list ref
+
+val plusP : poly -> poly -> poly
+val oppP : poly -> poly
+val multP : poly -> poly -> poly
+val puisP : poly -> int -> poly
+
+val poldepcontent : coef list ref
+
+type certificate =
+    { coef : coef; power : int;
+      gb_comb : poly list list; last_comb : poly list }
+
+val in_ideal : deg -> poly list -> poly -> poly list * poly * certificate
+
+module Hashpol : Hashtbl.S with type key = poly
+
+val sugar_flag : bool ref
+val divide_rem_with_critical_pair : bool ref
+
+end
+
+exception NotInIdeal
+
+val lexico : bool ref
diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml
index ced53d82..36bce780 100644
--- a/plugins/nsatz/nsatz.ml4
+++ b/plugins/nsatz/nsatz.ml
@@ -6,9 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
-open Errors
+open CErrors
 open Util
 open Term
 open Tactics
@@ -17,8 +15,6 @@ open Coqlib
 open Num
 open Utile
 
-DECLARE PLUGIN "nsatz_plugin"
-
 (***********************************************************************
  Operations on coefficients
 *)
@@ -472,6 +468,44 @@ let theoremedeszeros lpol p =
 
 open Ideal
 
+(* Remove zero polynomials and duplicates from the list of polynomials lp
+   Return (clp, lb)
+   where clp is the reduced list and lb is a list of booleans
+   that has the same size than lp and where true indicates an
+   element that has been removed
+ *)
+let rec clean_pol lp =
+  let t = Hashpol.create 12 in
+  let find p = try Hashpol.find t p 
+               with 
+                 Not_found -> Hashpol.add t p true; false in
+  let rec aux lp =
+    match lp with
+    | [] -> [], []
+    | p :: lp1 -> 
+      let clp, lb = aux lp1 in
+      if equal p zeroP ||  find p then clp, true::lb 
+       else
+        (p :: clp, false::lb) in
+     aux lp
+
+(* Expand the list of polynomials lp putting zeros where the list of 
+   booleans lb indicates there is a missing element 
+   Warning:
+   the expansion is relative to the end of the list in reversed order
+   lp cannot have less elements than lb
+*)
+let expand_pol lb lp =
+ let rec aux lb lp = 
+   match lb with
+   | [] -> lp
+   | true :: lb1 ->  zeroP :: aux lb1 lp
+   | false :: lb1 ->
+     match lp with
+     [] -> assert false
+     | p :: lp1 -> p :: aux lb1 lp1 
+  in List.rev (aux lb (List.rev lp))
+
 let theoremedeszeros_termes lp =
   nvars:=0;(* mise a jour par term_pol_sparse *)
   List.iter set_nvars_term  lp;
@@ -522,20 +556,29 @@ let theoremedeszeros_termes lp =
       | [] -> assert false
       | p::lp1 ->
 	  let lpol = List.rev lp1 in
+          (* preprocessing :
+             we remove zero polynomials and duplicate that are not handled by in_ideal
+             lb is kept in order to fix the certificate in the post-processing 
+          *)
+	  let lpol, lb  = clean_pol lpol in
 	  let (cert,lp0,p,_lct) = theoremedeszeros lpol p in
           info "cert ok\n";
 	  let lc = cert.last_comb::List.rev cert.gb_comb in
 	  match remove_zeros (fun x -> equal x zeroP) lc with
 	  | [] -> assert false
 	  | (lq::lci) ->
+              (* post-processing : we apply the correction for the last line *)
+              let lq = expand_pol lb lq in
 	      (* lci commence par les nouveaux polynomes *)
-	      let m= !nvars in
+	      let m = !nvars in
 	      let c = pol_sparse_to_term m (polconst m cert.coef) in
 	      let r = Pow(Zero,cert.power) in
 	      let lci = List.rev lci in
+              (* post-processing we apply the correction for the other lines *)
+	      let lci = List.map (expand_pol lb) lci in
 	      let lci = List.map (List.map (pol_sparse_to_term m)) lci in
 	      let lq = List.map (pol_sparse_to_term m) lq in
-	      info ("number of parametres: "^string_of_int nparam^"\n");
+	      info ("number of parameters: "^string_of_int nparam^"\n");
 	      info "term computed\n";
 	      (c,r,lci,lq)
       )
@@ -591,8 +634,4 @@ let nsatz_compute t =
       error "nsatz cannot solve this problem" in
   return_term lpol
 
-TACTIC EXTEND nsatz_compute
-| [ "nsatz_compute"  constr(lt) ] -> [ Proofview.V82.tactic (nsatz_compute lt) ]
-END
-
 
diff --git a/plugins/nsatz/nsatz.mli b/plugins/nsatz/nsatz.mli
new file mode 100644
index 00000000..e876ccfa
--- /dev/null
+++ b/plugins/nsatz/nsatz.mli
@@ -0,0 +1,9 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+val nsatz_compute : Constr.t -> unit Proofview.tactic
diff --git a/plugins/nsatz/nsatz_plugin.mllib b/plugins/nsatz/nsatz_plugin.mlpack
index a25e649d..b55adf43 100644
--- a/plugins/nsatz/nsatz_plugin.mllib
+++ b/plugins/nsatz/nsatz_plugin.mlpack
@@ -2,4 +2,4 @@ Utile
 Polynom
 Ideal
 Nsatz
-Nsatz_plugin_mod
+G_nsatz
diff --git a/plugins/nsatz/utile.ml b/plugins/nsatz/utile.ml
index 8e2fc07c..92243246 100644
--- a/plugins/nsatz/utile.ml
+++ b/plugins/nsatz/utile.ml
@@ -51,7 +51,7 @@ let facteurs_liste div constant lp =
                                    if not (constant r)
 				   then l1:=r::(!l1)
                                    else p_dans_lmin:=true)
-			      with e when Errors.noncritical e -> ())
+			      with e when CErrors.noncritical e -> ())
                      lmin;
           if !p_dans_lmin
           then factor lmin lp1
@@ -62,7 +62,7 @@ let facteurs_liste div constant lp =
                 List.iter (fun q -> try (let r = div q p in
 					 if not (constant r)
 					 then l1:=r::(!l1))
-				    with e when Errors.noncritical e ->
+				    with e when CErrors.noncritical e ->
                                       lmin1:=q::(!lmin1))
                           lmin;
 	        factor (List.rev (p::(!lmin1))) !l1)
@@ -93,7 +93,7 @@ let factorise_tableau div zero c f l1 =
       	                       li:=j::(!li);
                                r:=rr;
 			   done)
-                      with e when Errors.noncritical e -> ())
+                      with e when CErrors.noncritical e -> ())
                   l1;
       res.(i)<-(!r,!li))
      f;