summaryrefslogtreecommitdiff
path: root/plugins/nsatz/polynom.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/nsatz/polynom.ml')
-rw-r--r--plugins/nsatz/polynom.ml94
1 files changed, 43 insertions, 51 deletions
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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Recursive polynomials: R[x1]...[xn]. *)
-open Utile
open Util
+open Utile
(* 1. Coefficients: R *)
@@ -133,7 +133,7 @@ let x n = Prec (n,[|cf0;cf1|])
let monome v n =
match n with
0->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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 12:33:27 +0000