From 11ca3113365639136cf65a74c345080a9434e69b Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 27 Sep 2013 19:20:27 +0000 Subject: Removing a bunch of generic equalities. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/nsatz/nsatz.ml4 | 24 ++++++++++++------------ plugins/nsatz/polynom.ml | 48 ++++++++++++++++++++++++------------------------ 2 files changed, 36 insertions(+), 36 deletions(-) (limited to 'plugins/nsatz') diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4 index e31eba4e0..286fa6335 100644 --- a/plugins/nsatz/nsatz.ml4 +++ b/plugins/nsatz/nsatz.ml4 @@ -136,7 +136,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 @@ -192,7 +192,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] @@ -212,7 +212,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)] @@ -311,7 +311,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 -> @@ -365,19 +365,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) x=zeroP) lc with + match remove_zeros (fun x -> equal x zeroP) lc with | [] -> assert false | (lq::lci) -> (* lci commence par les nouveaux polynomes *) diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml index ca6d305e8..78883a660 100644 --- a/plugins/nsatz/polynom.ml +++ b/plugins/nsatz/polynom.ml @@ -168,7 +168,7 @@ exception Failed let rec equal p q = match (p,q) with (Pint a,Pint b) -> C.equal a b - |(Prec(x,p1),Prec(y,q1)) -> (x=y) && Array.for_all2 equal p1 q1 + |(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 @@ -184,8 +184,8 @@ let 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 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)) @@ -194,7 +194,7 @@ let norm p = match p with (* degree in v, v >= max var of 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 @@ -214,8 +214,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 *) @@ -272,7 +272,7 @@ let rec vars=function (* multiply p by v^n, v >= max_var p *) let multx n v p = match p with - Prec (x,p1) when x=v -> let p2= Array.make ((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; @@ -311,9 +311,9 @@ let rec multP p q = 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.make d (Pint coef0) in for i=0 to d-1 do @@ -410,7 +410,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 @@ -421,31 +421,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 @@ -468,7 +468,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 @@ -532,7 +532,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";*) @@ -569,13 +569,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) @@ -587,9 +587,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 -- cgit v1.2.3