From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- plugins/nsatz/Nsatz.v | 8 +-- plugins/nsatz/ideal.ml | 134 +++++++++++++++++++++++----------------------- plugins/nsatz/nsatz.ml4 | 60 ++++++++------------- plugins/nsatz/polynom.ml | 94 +++++++++++++++----------------- plugins/nsatz/polynom.mli | 2 +- plugins/nsatz/utile.ml | 16 +----- plugins/nsatz/utile.mli | 4 -- 7 files changed, 137 insertions(+), 181 deletions(-) (limited to 'plugins/nsatz') diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v index f8929d58..eaf95e94 100644 --- a/plugins/nsatz/Nsatz.v +++ b/plugins/nsatz/Nsatz.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* PolZ -> R := (InitialRing.gen_phiZ ring0 ring1 add mul opp)). Definition PEevalR : list R -> PEZ -> R := - PEeval ring0 add mul sub opp + PEeval ring0 ring1 add mul sub opp (gen_phiZ ring0 ring1 add mul opp) N.to_nat pow. @@ -241,7 +241,9 @@ Fixpoint interpret3 t fv {struct t}: R := | (PEpow t1 t2) => let v1 := interpret3 t1 fv in pow v1 (N.to_nat t2) | (PEc t1) => (IZR1 t1) - | (PEX n) => List.nth (pred (Pos.to_nat n)) fv 0 + | PEO => 0 + | PEI => 1 + | (PEX _ n) => List.nth (pred (Pos.to_nat n)) fv 0 end. diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml index 4bfcc436..8ff82454 100644 --- a/plugins/nsatz/ideal.ml +++ b/plugins/nsatz/ideal.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* P.equal c1 c2 && m1=m2) let hash p = - let c = map fst p in - let m = map snd p in - fold_left (fun h p -> h * 17 + P.hash p) (Hashtbl.hash m) c + let c = List.map fst p in + let m = List.map snd p in + List.fold_left (fun h p -> h * 17 + P.hash p) (Hashtbl.hash m) c module Hashpol = Hashtbl.Make( struct @@ -236,9 +235,8 @@ module Hashpol = Hashtbl.Make( open Format let getvar lv i = - try (nth lv i) - with e when Errors.noncritical e -> - (fold_left (fun r x -> r^" "^x) "lv= " lv) + try (List.nth lv i) + with Failure _ -> (List.fold_left (fun r x -> r^" "^x) "lv= " lv) ^" i="^(string_of_int i) let string_of_pol zeroP hdP tlP coefterm monterm string_of_coef @@ -363,8 +361,8 @@ let stringPcut p = (*Polynomesrec.nsP1:=20;*) nsP2:=10; let res = - if (length p)> !nsP2 - then (stringP [hd p])^" + "^(string_of_int (length p))^" terms" + if (List.length p)> !nsP2 + then (stringP [List.hd p])^" + "^(string_of_int (List.length p))^" terms" else stringP p in (*Polynomesrec.nsP1:= max_int;*) nsP2:= max_int; @@ -399,7 +397,7 @@ let zeroP = [] (* returns a constant polynom ial with d variables *) let polconst d c = - let m = Array.create (d+1) 0 in + let m = Array.make (d+1) 0 in let m = set_deg m in [(c,m)] @@ -432,7 +430,7 @@ let coef_of_int x = P.of_num (Num.Int x) (* variable i *) let gen d i = - let m = Array.create (d+1) 0 in + let m = Array.make (d+1) 0 in m.(i) <- 1; let m = set_deg m in [((coef_of_int 1),m)] @@ -463,10 +461,10 @@ let puisP p n= match p with [] -> [] |_ -> - let d = nvar (snd (hd p)) in + let d = nvar (snd (List.hd p)) in let rec puisP n = match n with - 0 -> [coef1, Array.create (d+1) 0] + 0 -> [coef1, Array.make (d+1) 0] | 1 -> p |_ -> multP p (puisP (n-1)) in puisP n @@ -484,7 +482,7 @@ let contentPlist lp = match lp with |[] -> coef1 |p::l1 -> - fold_left + List.fold_left (fun r q -> if P.equal r coef1 || P.equal r coefm1 then r @@ -501,17 +499,17 @@ let polynom0 = {pol = ref []; num = 0; sugar = 0} let ppol p = !(p.pol) -let lm p = snd (hd (ppol p)) +let lm p = snd (List.hd (ppol p)) let nallpol = ref 0 -let allpol = ref (Array.create 1000 polynom0) +let allpol = ref (Array.make 1000 polynom0) let new_allpol p s = nallpol := !nallpol + 1; if !nallpol >= Array.length !allpol then - allpol := Array.append !allpol (Array.create !nallpol polynom0); + allpol := Array.append !allpol (Array.make !nallpol polynom0); let p = {pol = ref p; num = !nallpol; sugar = s} in !allpol.(!nallpol)<- p; p @@ -521,7 +519,7 @@ let new_allpol p s = let rec selectdiv m l = match l with [] -> polynom0 - |q::r -> let m'= snd (hd (ppol q)) in + |q::r -> let m'= snd (List.hd (ppol q)) in match (div_mon_test m m') with true -> q |false -> selectdiv m r @@ -550,7 +548,7 @@ let div_coef a b = P.divP a b (* remainder r of the division of p by polynomials of l, returns (c,r) where c is the coefficient for pseudo-division : c p = sum_i q_i p_i + r *) let reduce2 p l = - let l = if nouveaux_pol_en_tete then rev l else l in + let l = if nouveaux_pol_en_tete then List.rev l else l in let rec reduce p = match p with [] -> (coef1,[]) @@ -601,8 +599,8 @@ let coefpoldep_set p q c = let initcoefpoldep d lp = poldep:=lp; - poldepcontent:= map (fun p -> contentP (ppol p)) lp; - iter + poldepcontent:= List.map (fun p -> contentP (ppol p)) lp; + List.iter (fun p -> coefpoldep_set p p (polconst d (coef_of_int 1))) lp @@ -610,7 +608,7 @@ let initcoefpoldep d lp = divides without pseudodivisions *) let reduce2_trace p l lcp = - let l = if nouveaux_pol_en_tete then rev l else l in + let l = if nouveaux_pol_en_tete then List.rev l else l in (* rend (lq,r), ou r = p + sum(lq) *) let rec reduce p = match p with @@ -646,10 +644,10 @@ let reduce2_trace p l lcp = info ((stringP x)^"\n")) lq; info "ok\n";*) - (map2 + (List.map2 (fun c0 q -> let c = - fold_left + List.fold_left (fun x (a,m,s) -> if equal (ppol s) (ppol q) then @@ -672,7 +670,7 @@ let pol_courant = ref polynom0 let sugar_flag = ref true let compute_sugar p = - fold_left (fun s (a,m) -> max s m.(0)) 0 p + List.fold_left (fun s (a,m) -> max s m.(0)) 0 p let mk_polynom p = new_allpol p (compute_sugar p) @@ -680,12 +678,12 @@ let mk_polynom p = let spol ps qs= let p = ppol ps in let q = ppol qs in - let m = snd (hd p) in - let m'= snd (hd q) in - let a = fst (hd p) in - let b = fst (hd q) in - let p'= tl p in - let q'= tl q in + let m = snd (List.hd p) in + let m'= snd (List.hd q) in + let a = fst (List.hd p) in + let b = fst (List.hd q) in + let p'= List.tl p in + let q'= List.tl q in let c = (pgcdpos a b) in let m''=(ppcm_mon m m') in let m1 = div_mon m'' m in @@ -709,8 +707,8 @@ let spol ps qs= let etrangers p p'= - let m = snd (hd p) in - let m'= snd (hd p') in + let m = snd (List.hd p) in + let m'= snd (List.hd p') in let d = nvar m in let res=ref true in let i=ref 1 in @@ -723,9 +721,9 @@ let etrangers p p'= (* teste if head monomial of p'' divides lcm of lhead monomials of p and p' *) let div_ppcm p p' p'' = - let m = snd (hd p) in - let m'= snd (hd p') in - let m''= snd (hd p'') in + let m = snd (List.hd p) in + let m'= snd (List.hd p') in + let m''= snd (List.hd p'') in let d = nvar m in let res=ref true in let i=ref 1 in @@ -766,7 +764,7 @@ let slice i a q = (* sugar strategy *) -let rec addS x l = l @ [x] (* oblige de mettre en queue sinon le certificat deconne *) +let addS x l = l @ [x] (* oblige de mettre en queue sinon le certificat deconne *) let addSsugar x l = if !sugar_flag @@ -823,10 +821,10 @@ let ordcpair ((i1,j1),m1) ((i2,j2),m2) = compare_mon m1 m2 let sortcpairs lcp = - sort ordcpair lcp + List.sort ordcpair lcp let mergecpairs l1 l2 = - merge ordcpair l1 l2 + List.merge ordcpair l1 l2 let ord i j = if i r @ (cpair p q)) [] lq) + sortcpairs (List.fold_left (fun r q -> r @ (cpair p q)) [] lq) let cpairs lp = let rec aux l = @@ -849,18 +847,18 @@ let cpairs lp = let critere2 ((i,j),m) lp lcp = - exists + List.exists (fun h -> h.num <> i && h.num <> j && (div_mon_test m (lm h)) && (let c1 = ord i h.num in - not (exists (fun (c,_) -> c1 = c) lcp)) + not (List.exists (fun (c,_) -> c1 = c) lcp)) && (let c1 = ord j h.num in - not (exists (fun (c,_) -> c1 = c) lcp))) + not (List.exists (fun (c,_) -> c1 = c) lcp))) lp let critere3 ((i,j),m) lp lcp = - exists + List.exists (fun h -> h.num <> i && h.num <> j && (div_mon_test m (lm h)) @@ -881,8 +879,8 @@ let step = ref 0 let infobuch p q = if !step = 0 - then (info ("[" ^ (string_of_int (length p)) - ^ "," ^ (string_of_int (length q)) + then (info ("[" ^ (string_of_int (List.length p)) + ^ "," ^ (string_of_int (List.length q)) ^ "]")) (* in lp new polynomials are at the end *) @@ -900,13 +898,13 @@ let test_dans_ideal p lp lp0 = pol_courant:= mk_polynom r; if r=[] then (info "polynomial reduced to 0\n"; - let lcp = map (fun q -> []) !poldep in + let lcp = List.map (fun q -> []) !poldep in let c = !coef_courant in let (lcq,r) = reduce2_trace (emultP c p) lp lcp in info "r ok\n"; info ("r: "^(stringP r)^"\n"); let res=ref (emultP c p) in - iter2 + List.iter2 (fun cq q -> res:=plusP (!res) (multP cq (ppol q)); ) lcq !poldep; @@ -916,22 +914,22 @@ let test_dans_ideal p lp lp0 = match lp with |[] -> [] |p::lp -> - (map + (List.map (fun q -> coefpoldep_find p q) lp)::(aux lp) in let coefficient_multiplicateur = c in - let liste_polynomes_de_depart = rev lp0 in + let liste_polynomes_de_depart = List.rev lp0 in let polynome_a_tester = p in let liste_des_coefficients_intermediaires = - (let lci = rev (aux (rev lp)) in + (let lci = List.rev (aux (List.rev lp)) in let lci = ref lci (* (map rev lci) *) in - iter (fun x -> lci := tl (!lci)) lp0; + List.iter (fun x -> lci := List.tl (!lci)) lp0; !lci) in let liste_des_coefficients = - map + List.map (fun cq -> emultP (coef_of_int (-1)) cq) - (rev lcq) in + (List.rev lcq) in (liste_polynomes_de_depart, polynome_a_tester, {coef = coefficient_multiplicateur; @@ -946,7 +944,7 @@ let test_dans_ideal p lp lp0 = let divide_rem_with_critical_pair = ref false let list_diff l x = - filter (fun y -> y <> x) l + List.filter (fun y -> y <> x) l let deg_hom p = match p with @@ -984,12 +982,12 @@ let pbuchf pq p lp0= (* info "pair reduced\n";*) a.pol := emultP ca (ppol a); let (lca,a0) = reduce2_trace (ppol a) lp - (map (fun q -> emultP ca (coefpoldep_find a q)) + (List.map (fun q -> emultP ca (coefpoldep_find a q)) !poldep) in (* info "paire re-reduced";*) a.pol := a0; (* let a0 = new_allpol a0 sa in*) - iter2 (fun c q -> + List.iter2 (fun c q -> coefpoldep_remove a q; coefpoldep_set a q c) lca !poldep; let a0 = a in @@ -1009,7 +1007,7 @@ let is_homogeneous p = match p with | [] -> true | (a,m)::p1 -> let d = m.(0) in - for_all (fun (b,m') -> m'.(0)=d) p1 + List.for_all (fun (b,m') -> m'.(0)=d) p1 (* returns c @@ -1030,15 +1028,15 @@ let in_ideal d lp p = Hashtbl.clear hmon; Hashtbl.clear coefpoldep; nallpol := 0; - allpol := Array.create 1000 polynom0; - homogeneous := for_all is_homogeneous (p::lp); + allpol := Array.make 1000 polynom0; + homogeneous := List.for_all is_homogeneous (p::lp); if !homogeneous then info "homogeneous polynomials\n"; info ("p: "^(stringPcut p)^"\n"); - info ("lp:\n"^(fold_left (fun r p -> r^(stringPcut p)^"\n") "" lp)); + info ("lp:\n"^(List.fold_left (fun r p -> r^(stringPcut p)^"\n") "" lp)); (*info ("p: "^(stringP p)^"\n"); info ("lp:\n"^(fold_left (fun r p -> r^(stringP p)^"\n") "" lp));*) - let lp = map mk_polynom lp in + let lp = List.map mk_polynom lp in let p = mk_polynom p in initcoefpoldep d lp; coef_courant:=coef1; @@ -1049,7 +1047,7 @@ let in_ideal d lp p = with NotInIdeal -> pbuchf (lp, (cpairs lp)) p lp in info "computed\n"; - (map ppol lp1, p1, cert) + (List.map ppol lp1, p1, cert) (* *) end diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4 index a66bd44b..b4eb57ec 100644 --- a/plugins/nsatz/nsatz.ml4 +++ b/plugins/nsatz/nsatz.ml4 @@ -1,42 +1,24 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* 1 + with Failure _ -> 1 let puis = power_big_int_positive_int (* a et b positifs, résultat positif *) @@ -156,7 +138,7 @@ type term = let const n = if eq_num n num_0 then Zero else Const n -let pow(p,i) = if i=1 then p else Pow(p,i) +let pow(p,i) = if Int.equal i 1 then p else Pow(p,i) let add = function (Zero,q) -> q | (p,Zero) -> p @@ -212,7 +194,7 @@ let rec mkt_pos n = mkt_app pxI [mkt_pos (quo_num n num_2)] let mkt_n n = - if n=num_0 + if Num.eq_num n num_0 then Lazy.force nN0 else mkt_app nNpos [mkt_pos n] @@ -232,7 +214,7 @@ let rec mkt_term t = match t with | Add (t1,t2) -> mkt_app ttadd [Lazy.force tz; mkt_term t1; mkt_term t2] | Sub (t1,t2) -> mkt_app ttsub [Lazy.force tz; mkt_term t1; mkt_term t2] | Mul (t1,t2) -> mkt_app ttmul [Lazy.force tz; mkt_term t1; mkt_term t2] -| Pow (t1,n) -> if (n = 0) then +| Pow (t1,n) -> if Int.equal n 0 then mkt_app ttconst [Lazy.force tz; mkt_z num_1] else mkt_app ttpow [Lazy.force tz; mkt_term t1; mkt_n (num_of_int n)] @@ -331,7 +313,7 @@ let term_pol_sparse np t= match t with | Zero -> zeroP | Const r -> - if r = num_0 + if Num.eq_num r num_0 then zeroP else polconst d (Poly.Pint (Coef.of_num r)) | Var v -> @@ -385,19 +367,19 @@ let pol_sparse_to_term n2 p = if m.(k)>0 then i0:=k done; - if !i0 = 0 + if Int.equal !i0 0 then (r,d) else if !i0 > r then (!i0, m.(!i0)) - else if !i0 = r && m.(!i0)=m then () @@ -543,7 +525,7 @@ let theoremedeszeros_termes lp = 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 -> x=zeroP) lc with + match remove_zeros (fun x -> equal x zeroP) lc with | [] -> assert false | (lq::lci) -> (* lci commence par les nouveaux polynomes *) @@ -610,7 +592,7 @@ let nsatz_compute t = return_term lpol TACTIC EXTEND nsatz_compute -| [ "nsatz_compute" constr(lt) ] -> [ nsatz_compute lt ] +| [ "nsatz_compute" constr(lt) ] -> [ Proofview.V82.tactic (nsatz_compute lt) ] END diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml index 026b66c7..a9651304 100644 --- a/plugins/nsatz/polynom.ml +++ b/plugins/nsatz/polynom.ml @@ -1,14 +1,14 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Pint coef1; - |_->let tmp = Array.create (n+1) (Pint coef0) in + |_->let tmp = Array.make (n+1) (Pint coef0) in tmp.(n)<-(Pint coef1); Prec (v, tmp) @@ -159,28 +159,21 @@ let rec max_var_pol2 p = Pint _ -> 0 |Prec(v,c)-> Array.fold_right (fun q m -> max (max_var_pol2 q) m) c v -let rec max_var l = Array.fold_right (fun p m -> max (max_var_pol2 p) m) l 0 +let max_var l = Array.fold_right (fun p m -> max (max_var_pol2 p) m) l 0 (* equality between polynomials *) let rec equal p q = match (p,q) with (Pint a,Pint b) -> C.equal a b - |(Prec(x,p1),Prec(y,q1)) -> - if x<>y then false - else if (Array.length p1)<>(Array.length q1) then false - else (try (Array.iteri (fun i a -> if not (equal a q1.(i)) - then failwith "raté") - p1; - true) - with e when Errors.noncritical e -> false) + |(Prec(x,p1),Prec(y,q1)) -> (Int.equal x y) && Array.for_all2 equal p1 q1 | (_,_) -> false (* normalize polynomial: remove head zeros, coefficients are normalized if constant, returns the coefficient *) -let rec norm p = match p with +let norm p = match p with Pint _ -> p |Prec (x,a)-> let d = (Array.length a -1) in @@ -189,17 +182,17 @@ let rec norm p = match p with n:=!n-1; done; if !n<0 then Pint coef0 - else if !n=0 then a.(0) - else if !n=d then p - else (let b=Array.create (!n+1) (Pint coef0) in + else if Int.equal !n 0 then a.(0) + else if Int.equal !n d then p + else (let b=Array.make (!n+1) (Pint coef0) in for i=0 to !n do b.(i)<-a.(i);done; Prec(x,b)) (* degree in v, v >= max var of p *) -let rec deg v p = +let deg v p = match p with - Prec(x,p1) when x=v -> Array.length p1 -1 + Prec(x,p1) when Int.equal x v -> Array.length p1 -1 |_ -> 0 @@ -219,8 +212,8 @@ let rec copyP p = (* coefficient of degree i in v, v >= max var of p *) let coef v i p = match p with - Prec (x,p1) when x=v -> if i<(Array.length p1) then p1.(i) else Pint coef0 - |_ -> if i=0 then p else Pint coef0 + Prec (x,p1) when Int.equal x v -> if i<(Array.length p1) then p1.(i) else Pint coef0 + |_ -> if Int.equal i 0 then p else Pint coef0 (* addition *) @@ -243,7 +236,7 @@ let rec plusP p q = Prec (x,p2)) else (let n=max (deg x p) (deg x q) in - let r=Array.create (n+1) (Pint coef0) in + let r=Array.make (n+1) (Pint coef0) in for i=0 to n do r.(i)<- plusP (coef x i p) (coef x i q); done; @@ -275,15 +268,15 @@ let rec vars=function (* multiply p by v^n, v >= max_var p *) -let rec multx n v p = +let multx n v p = match p with - Prec (x,p1) when x=v -> let p2= Array.create ((Array.length p1)+n) (Pint coef0) in + Prec (x,p1) when Int.equal x v -> let p2= Array.make ((Array.length p1)+n) (Pint coef0) in for i=0 to (Array.length p1)-1 do p2.(i+n)<-p1.(i); done; Prec (x,p2) |_ -> if equal p (Pint coef0) then (Pint coef0) - else (let p2=Array.create (n+1) (Pint coef0) in + else (let p2=Array.make (n+1) (Pint coef0) in p2.(n)<-p; Prec (v,p2)) @@ -313,14 +306,14 @@ let rec multP p q = (* derive p with variable v, v >= max_var p *) -let rec deriv v p = +let deriv v p = match p with Pint a -> Pint coef0 - | Prec(x,p1) when x=v -> + | Prec(x,p1) when Int.equal x v -> let d = Array.length p1 -1 in - if d=1 then p1.(1) + if Int.equal d 1 then p1.(1) else - (let p2 = Array.create d (Pint coef0) in + (let p2 = Array.make d (Pint coef0) in for i=0 to d-1 do p2.(i)<- multP (Pint (coef_of_int (i+1))) p1.(i+1); done; @@ -415,7 +408,7 @@ let rec string_of_Pcut p = and s=ref "" and sp=ref "" in let st0 = string_of_Pcut t.(0) in - if st0<>"0" + if not (String.equal st0 "0") then s:=st0; let fin = ref false in for i=(Array.length t)-1 downto 1 do @@ -426,31 +419,31 @@ let rec string_of_Pcut p = else ( let si=string_of_Pcut t.(i) in sp:=""; - if i=1 + if Int.equal i 1 then ( - if si<>"0" + if not (String.equal si "0") then (nsP:=(!nsP)-1; - if si="1" + if String.equal si "1" then sp:=v else (if (String.contains si '+') then sp:="("^si^")*"^v else sp:=si^"*"^v))) else ( - if si<>"0" + if not (String.equal si "0") then (nsP:=(!nsP)-1; - if si="1" + if String.equal si "1" then sp:=v^"^"^(string_of_int i) else (if (String.contains si '+') then sp:="("^si^")*"^v^"^"^(string_of_int i) else sp:=si^"*"^v^"^"^(string_of_int i)))); - if !sp<>"" && not (!fin) + if not (String.is_empty !sp) && not (!fin) then (nsP:=(!nsP)-1; - if !s="" + if String.is_empty !s then s:=!sp else s:=(!s)^"+"^(!sp))); done; - if !s="" then (nsP:=(!nsP)-1; + if String.is_empty !s then (nsP:=(!nsP)-1; (s:="0")); !s @@ -473,7 +466,7 @@ let print_lpoly lp = print_tpoly (Array.of_list lp) (* return (s,r) s.t. p = s*q+r *) let rec quo_rem_pol p q x = - if x=0 + if Int.equal x 0 then (match (p,q) with |(Pint a, Pint b) -> if C.equal (C.modulo a b) coef0 @@ -519,12 +512,11 @@ let divP p q= let div_pol_rat p q= let x = max (max_var_pol p) (max_var_pol q) in - try (let s = div_pol (multP p (puisP (Pint(coef_int_tete q)) - (1+(deg x p) - (deg x q)))) - q x in - (* degueulasse, mais c 'est pour enlever un warning *) - if s==s then true else true) - with e when Errors.noncritical e -> false + try + let r = puisP (Pint(coef_int_tete q)) (1+(deg x p)-(deg x q)) in + let _ = div_pol (multP p r) q x in + true + with Failure _ -> false (*********************************************************************** 5. Pseudo-division and gcd with subresultants. @@ -538,7 +530,7 @@ let div_pol_rat p q= let pseudo_div p q x = match q with Pint _ -> (cf0, q,1, p) - | Prec (v,q1) when x<>v -> (cf0, q,1, p) + | Prec (v,q1) when not (Int.equal x v) -> (cf0, q,1, p) | Prec (v,q1) -> ( (* pr "pseudo_division: c^d*p = s*q + r";*) @@ -575,13 +567,13 @@ and pgcd_pol p q x = and content_pol p x = match p with - Prec(v,p1) when v=x -> + Prec(v,p1) when Int.equal v x -> Array.fold_left (fun a b -> pgcd_pol_rec a b (x-1)) cf0 p1 | _ -> p and pgcd_coef_pol c p x = match p with - Prec(v,p1) when x=v -> + Prec(v,p1) when Int.equal x v -> Array.fold_left (fun a b -> pgcd_pol_rec a b (x-1)) c p1 |_ -> pgcd_pol_rec c p (x-1) @@ -593,9 +585,9 @@ and pgcd_pol_rec p q x = then q else if equal q cf0 then p - else if (deg x q) = 0 + else if Int.equal (deg x q) 0 then pgcd_coef_pol q p x - else if (deg x p) = 0 + else if Int.equal (deg x p) 0 then pgcd_coef_pol p q x else ( let a = content_pol p x in @@ -610,7 +602,7 @@ and pgcd_pol_rec p q x = res ) -(* Sub-résultants: +(* Sub-résultants: ai*Ai = Qi*Ai+1 + bi*Ai+2 @@ -655,7 +647,7 @@ and gcd_sub_res_rec p q s c d x = and lazard_power c s d x = let res = ref c in - for i=1 to d-1 do + for _i = 1 to d - 1 do res:= div_pol ((!res)@@c) s x; done; !res diff --git a/plugins/nsatz/polynom.mli b/plugins/nsatz/polynom.mli index 0f1e0481..9d46cd99 100644 --- a/plugins/nsatz/polynom.mli +++ b/plugins/nsatz/polynom.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* if not (list_mem_eq eq x (!res)) then res:=x::(!res)) l; List.rev !res - -(* Memoization - f is compatible with nf: f(nf(x)) = f(x) -*) - -let memos s memoire nf f x = - try (let v = Hashtbl.find memoire (nf x) in pr s;v) - with e when Errors.noncritical e -> - (pr "#"; - let v = f x in - Hashtbl.add memoire (nf x) v; - v) - - (********************************************************************** Eléments minimaux pour un ordre partiel de division. E est un ensemble, avec une multiplication @@ -95,7 +81,7 @@ let facteurs_liste div constant lp = c est un élément quelconque de E. *) let factorise_tableau div zero c f l1 = - let res = Array.create (Array.length f) (c,[]) in + let res = Array.make (Array.length f) (c,[]) in Array.iteri (fun i p -> let r = ref p in let li = ref [] in diff --git a/plugins/nsatz/utile.mli b/plugins/nsatz/utile.mli index 83b2ac39..1f841575 100644 --- a/plugins/nsatz/utile.mli +++ b/plugins/nsatz/utile.mli @@ -10,10 +10,6 @@ val info : string -> unit val list_mem_eq : ('a -> 'b -> bool) -> 'a -> 'b list -> bool val set_of_list_eq : ('a -> 'a -> bool) -> 'a list -> 'a list -(* Memoization *) -val memos : - string -> ('a, 'b) Hashtbl.t -> ('c -> 'a) -> ('c -> 'b) -> 'c -> 'b - val facteurs_liste : ('a -> 'a -> 'a) -> ('a -> bool) -> 'a list -> 'a list val factorise_tableau : -- cgit v1.2.3