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/polynom.ml | 94 ++++++++++++++++++++++-------------------------- 1 file changed, 43 insertions(+), 51 deletions(-) (limited to 'plugins/nsatz/polynom.ml') 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 -- cgit v1.2.3