From 094e4649c29e2426daca0476c140439de901dafe Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 16 Oct 2018 14:55:30 +0200 Subject: [numeral] [plugins] Switch from `Big_int` to ZArith. We replace Coq's use of `Big_int` and `num` by the ZArith OCaml library which is a more modern version. We switch the core files and easy plugins only for now, more complex numerical plugins will be done in their own commit. We thus keep the num library linked for now until all plugins are ported. Co-authored-by: Vincent Laporte --- plugins/extraction/big.ml | 76 ++++++++++++++++++++---------------------- plugins/extraction/dune | 2 +- plugins/nsatz/dune | 2 +- plugins/omega/coq_omega.ml | 27 +++++++++++---- plugins/syntax/float_syntax.ml | 10 +++--- plugins/syntax/r_syntax.ml | 49 +++++++++++++-------------- 6 files changed, 89 insertions(+), 77 deletions(-) (limited to 'plugins') diff --git a/plugins/extraction/big.ml b/plugins/extraction/big.ml index 19055fd425..7228f709f1 100644 --- a/plugins/extraction/big.ml +++ b/plugins/extraction/big.ml @@ -8,63 +8,61 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** [Big] : a wrapper around ocaml [Big_int] with nicer names, +(** [Big] : a wrapper around ocaml [ZArith] with nicer names, and a few extraction-specific constructions *) -(** To be linked with [nums.(cma|cmxa)] *) +(** To be linked with [zarith] *) -open Big_int - -type big_int = Big_int.big_int +type big_int = Z.t (** The type of big integers. *) -let zero = zero_big_int +let zero = Z.zero (** The big integer [0]. *) -let one = unit_big_int +let one = Z.one (** The big integer [1]. *) -let two = big_int_of_int 2 +let two = Z.of_int 2 (** The big integer [2]. *) (** {6 Arithmetic operations} *) -let opp = minus_big_int +let opp = Z.neg (** Unary negation. *) -let abs = abs_big_int +let abs = Z.abs (** Absolute value. *) -let add = add_big_int +let add = Z.add (** Addition. *) -let succ = succ_big_int - (** Successor (add 1). *) +let succ = Z.succ +(** Successor (add 1). *) -let add_int = add_int_big_int +let add_int = Z.add (** Addition of a small integer to a big integer. *) -let sub = sub_big_int +let sub = Z.sub (** Subtraction. *) -let pred = pred_big_int +let pred = Z.pred (** Predecessor (subtract 1). *) -let mult = mult_big_int +let mult = Z.mul (** Multiplication of two big integers. *) -let mult_int = mult_int_big_int +let mult_int x y = Z.mul (Z.of_int x) y (** Multiplication of a big integer by a small integer *) -let square = square_big_int +let square x = Z.mul x x (** Return the square of the given big integer *) -let sqrt = sqrt_big_int +let sqrt = Z.sqrt (** [sqrt_big_int a] returns the integer square root of [a], that is, the largest big integer [r] such that [r * r <= a]. Raise [Invalid_argument] if [a] is negative. *) -let quomod = quomod_big_int +let quomod = Z.div_rem (** Euclidean division of two big integers. The first part of the result is the quotient, the second part is the remainder. @@ -72,18 +70,18 @@ let quomod = quomod_big_int [a = q * b + r] and [0 <= r < |b|]. Raise [Division_by_zero] if the divisor is zero. *) -let div = div_big_int +let div = Z.div (** Euclidean quotient of two big integers. This is the first result [q] of [quomod_big_int] (see above). *) -let modulo = mod_big_int +let modulo = Z.(mod) (** Euclidean modulus of two big integers. This is the second result [r] of [quomod_big_int] (see above). *) -let gcd = gcd_big_int +let gcd = Z.gcd (** Greatest common divisor of two big integers. *) -let power = power_big_int_positive_big_int +let power = Z.pow (** Exponentiation functions. Return the big integer representing the first argument [a] raised to the power [b] (the second argument). Depending @@ -92,45 +90,45 @@ let power = power_big_int_positive_big_int (** {6 Comparisons and tests} *) -let sign = sign_big_int +let sign = Z.sign (** Return [0] if the given big integer is zero, [1] if it is positive, and [-1] if it is negative. *) -let compare = compare_big_int +let compare = Z.compare (** [compare_big_int a b] returns [0] if [a] and [b] are equal, [1] if [a] is greater than [b], and [-1] if [a] is smaller than [b]. *) -let eq = eq_big_int -let le = le_big_int -let ge = ge_big_int -let lt = lt_big_int -let gt = gt_big_int +let eq = Z.equal +let le = Z.leq +let ge = Z.geq +let lt = Z.lt +let gt = Z.gt (** Usual boolean comparisons between two big integers. *) -let max = max_big_int +let max = Z.max (** Return the greater of its two arguments. *) -let min = min_big_int +let min = Z.min (** Return the smaller of its two arguments. *) (** {6 Conversions to and from strings} *) -let to_string = string_of_big_int +let to_string = Z.to_string (** Return the string representation of the given big integer, in decimal (base 10). *) -let of_string = big_int_of_string +let of_string = Z.of_string (** Convert a string to a big integer, in decimal. The string consists of an optional [-] or [+] sign, followed by one or several decimal digits. *) (** {6 Conversions to and from other numerical types} *) -let of_int = big_int_of_int +let of_int = Z.of_int (** Convert a small integer to a big integer. *) -let is_int = is_int_big_int +let is_int = Z.fits_int (** Test whether the given big integer is small enough to be representable as a small integer (type [int]) without loss of precision. On a 32-bit platform, @@ -139,7 +137,7 @@ let is_int = is_int_big_int [is_int_big_int a] returns [true] if and only if [a] is between -2{^62} and 2{^62}-1. *) -let to_int = int_of_big_int +let to_int = Z.to_int (** Convert a big integer to a small integer (type [int]). Raises [Failure "int_of_big_int"] if the big integer is not representable as a small integer. *) diff --git a/plugins/extraction/dune b/plugins/extraction/dune index 0c01dcd488..d9d675fe6a 100644 --- a/plugins/extraction/dune +++ b/plugins/extraction/dune @@ -2,6 +2,6 @@ (name extraction_plugin) (public_name coq.plugins.extraction) (synopsis "Coq's extraction plugin") - (libraries num coq.plugins.ltac)) + (libraries coq.plugins.ltac)) (coq.pp (modules g_extraction)) diff --git a/plugins/nsatz/dune b/plugins/nsatz/dune index b921c9c408..3b67ab3429 100644 --- a/plugins/nsatz/dune +++ b/plugins/nsatz/dune @@ -2,6 +2,6 @@ (name nsatz_plugin) (public_name coq.plugins.nsatz) (synopsis "Coq's nsatz solver plugin") - (libraries num coq.plugins.ltac)) + (libraries coq.plugins.ltac)) (coq.pp (modules g_nsatz)) diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index cd5b747d75..4f7b3fbe74 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -32,7 +32,22 @@ open Tactypes open Context.Named.Declaration module NamedDecl = Context.Named.Declaration -module OmegaSolver = Omega.MakeOmegaSolver (Bigint) + +module ZOmega = struct + type bigint = Z.t + let equal = Z.equal + let less_than = Z.lt + let add = Z.add + let sub = Z.sub + let mult = Z.mul + let euclid = Z.div_rem + let neg = Z.neg + let zero = Z.zero + let one = Z.one + let to_string = Z.to_string +end + +module OmegaSolver = Omega.MakeOmegaSolver (ZOmega) open OmegaSolver (* Added by JCF, 09/03/98 *) @@ -719,7 +734,7 @@ let rec shuffle p (t1,t2) = Oplus(l2,t') else [],Oplus(t1,t2) | Oz t1,Oz t2 -> - [focused_simpl p], Oz(Bigint.add t1 t2) + [focused_simpl p], Oz(Z.add t1 t2) | t1,t2 -> if weight t1 < weight t2 then [clever_rewrite p [[P_APP 1];[P_APP 2]] @@ -741,7 +756,7 @@ let shuffle_mult p_init k1 e1 k2 e2 = [P_APP 2; P_APP 2]] (Lazy.force coq_fast_OMEGA10) in - if Bigint.add (Bigint.mult k1 c1) (Bigint.mult k2 c2) =? zero then + if Z.add (Z.mul k1 c1) (Z.mul k2 c2) =? zero then let tac' = clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] (Lazy.force coq_fast_Zred_factor5) in @@ -798,7 +813,7 @@ let shuffle_mult_right p_init e1 k2 e2 = [P_APP 2; P_APP 2]] (Lazy.force coq_fast_OMEGA15) in - if Bigint.add c1 (Bigint.mult k2 c2) =? zero then + if Z.add c1 (Z.mul k2 c2) =? zero then let tac' = clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] (Lazy.force coq_fast_Zred_factor5) @@ -1004,7 +1019,7 @@ let reduce_factor p = function | Otimes(Oatom v,c) -> let rec compute = function | Oz n -> n - | Oplus(t1,t2) -> Bigint.add (compute t1) (compute t2) + | Oplus(t1,t2) -> Z.add (compute t1) (compute t2) | _ -> CErrors.user_err Pp.(str "condense.1") in [focused_simpl (P_APP 2 :: p)], Otimes(Oatom v,Oz(compute c)) @@ -1160,7 +1175,7 @@ let replay_history tactic_normalisation = | NOT_EXACT_DIVIDE (e1,k) :: l -> let c = floor_div e1.constant k in - let d = Bigint.sub e1.constant (Bigint.mult c k) in + let d = Z.sub e1.constant (Z.mul c k) in let e2 = {id=e1.id; kind=EQUA;constant = c; body = map_eq_linear (fun c -> c / k) e1.body } in let eq2 = val_of(decompile e2) in diff --git a/plugins/syntax/float_syntax.ml b/plugins/syntax/float_syntax.ml index 8e87fc13ca..5d8dcd04fe 100644 --- a/plugins/syntax/float_syntax.ml +++ b/plugins/syntax/float_syntax.ml @@ -48,21 +48,21 @@ let interp_float ?loc n = | None -> "" | Some f -> NumTok.UnsignedNat.to_string f in let e = match e with | None -> "0" | Some e -> NumTok.SignedNat.to_string e in - Bigint.of_string (i ^ f), + Z.of_string (i ^ f), (try int_of_string e with Failure _ -> 0) - String.length f in let m', e' = let m', e' = Float64.frshiftexp f in let m' = Float64.normfr_mantissa m' in let e' = Uint63.to_int_min e' 4096 - Float64.eshift - 53 in - Bigint.of_string (Uint63.to_string m'), + Z.of_string (Uint63.to_string m'), e' in - let c2, c5 = Bigint.(of_int 2, of_int 5) in + let c2, c5 = Z.(of_int 2, of_int 5) in (* check m*5^e <> m'*2^e' *) let check m e m' e' = - not (Bigint.(equal (mult m (pow c5 e)) (mult m' (pow c2 e')))) in + not (Z.(equal (mul m (pow c5 e)) (mul m' (pow c2 e')))) in (* check m*5^e*2^e' <> m' *) let check' m e e' m' = - not (Bigint.(equal (mult (mult m (pow c5 e)) (pow c2 e')) m')) in + not (Z.(equal (mul (mul m (pow c5 e)) (pow c2 e')) m')) in (* we now have to check m*10^e <> m'*2^e' *) if e >= 0 then if e <= e' then check m e m' (e' - e) diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 23a7cc07c5..d66b9537b4 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -11,7 +11,6 @@ open Util open Names open Glob_term -open Bigint (* Poor's man DECLARE PLUGIN *) let __coq_plugin_name = "r_syntax_plugin" @@ -47,10 +46,10 @@ let pos_of_bignat ?loc x = let ref_xH = DAst.make @@ GRef (glob_xH, None) in let ref_xO = DAst.make @@ GRef (glob_xO, None) in let rec pos_of x = - match div2_with_rest x with - | (q,false) -> DAst.make @@ GApp (ref_xO,[pos_of q]) - | (q,true) when not (Bigint.equal q zero) -> DAst.make @@ GApp (ref_xI,[pos_of q]) - | (q,true) -> ref_xH + match Z.(div_rem x (of_int 2)) with + | (q,rem) when rem = Z.zero -> DAst.make @@ GApp (ref_xO,[pos_of q]) + | (q,_) when not Z.(equal q zero) -> DAst.make @@ GApp (ref_xI,[pos_of q]) + | (q,_) -> ref_xH in pos_of x @@ -59,9 +58,9 @@ let pos_of_bignat ?loc x = (**********************************************************************) let rec bignat_of_pos c = match DAst.get c with - | GApp (r, [a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a) - | GApp (r, [a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a)) - | GRef (a, _) when GlobRef.equal a glob_xH -> Bigint.one + | GApp (r, [a]) when is_gr r glob_xO -> Z.mul Z.(of_int 2) (bignat_of_pos a) + | GApp (r, [a]) when is_gr r glob_xI -> Z.add Z.one Z.(mul (of_int 2) (bignat_of_pos a)) + | GRef (a, _) when GlobRef.equal a glob_xH -> Z.one | _ -> raise Non_closed_number (**********************************************************************) @@ -77,9 +76,9 @@ let glob_POS = GlobRef.ConstructRef path_of_POS let glob_NEG = GlobRef.ConstructRef path_of_NEG let z_of_int ?loc n = - if not (Bigint.equal n zero) then + if not Z.(equal n zero) then let sgn, n = - if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in + if Z.(leq zero n) then glob_POS, n else glob_NEG, Z.neg n in DAst.make @@ GApp(DAst.make @@ GRef (sgn,None), [pos_of_bignat ?loc n]) else DAst.make @@ GRef (glob_ZERO, None) @@ -90,8 +89,8 @@ let z_of_int ?loc n = let bigint_of_z c = match DAst.get c with | GApp (r,[a]) when is_gr r glob_POS -> bignat_of_pos a - | GApp (r,[a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a) - | GRef (a, _) when GlobRef.equal a glob_ZERO -> Bigint.zero + | GApp (r,[a]) when is_gr r glob_NEG -> Z.neg (bignat_of_pos a) + | GRef (a, _) when GlobRef.equal a glob_ZERO -> Z.zero | _ -> raise Non_closed_number (**********************************************************************) @@ -122,13 +121,13 @@ let r_of_rawnum ?loc n = let rdiv r r' = DAst.make @@ GApp (DAst.make @@ GRef(glob_Rdiv,None), [r; r']) in let pow p e = - let p = z_of_int ?loc (Bigint.of_int p) in + let p = z_of_int ?loc (Z.of_int p) in let e = pos_of_bignat e in DAst.make @@ GApp (DAst.make @@ GRef(glob_pow_pos,None), [p; e]) in let n = izr (z_of_int ?loc n) in - if Bigint.is_strictly_pos e then rmult n (izr (pow p e)) - else if Bigint.is_strictly_neg e then rdiv n (izr (pow p (neg e))) + if Int.equal (Z.sign e) 1 then rmult n (izr (pow p e)) + else if Int.equal (Z.sign e) (-1) then rdiv n (izr (pow p (Z.neg e))) else n (* e = 0 *) (**********************************************************************) @@ -141,24 +140,24 @@ let rawnum_of_r c = (* choose between 123e-2 and 1.23, this is purely heuristic and doesn't play any soundness role *) let choose_exponent = - if Bigint.is_strictly_pos e then + if Int.equal (Z.sign e) 1 then true (* don't print 12 * 10^2 as 1200 to distinguish them *) else - let i = Bigint.to_string i in + let i = Z.to_string i in let li = if i.[0] = '-' then String.length i - 1 else String.length i in - let e = Bigint.neg e in - let le = String.length (Bigint.to_string e) in - Bigint.(less_than (add (of_int li) (of_int le)) e) in + let e = Z.neg e in + let le = String.length (Z.to_string e) in + Z.(lt (add (of_int li) (of_int le)) e) in (* print 123 * 10^-2 as 123e-2 *) let numTok_exponent () = NumTok.Signed.of_bigint_and_exponent i (NumTok.EDec e) in (* print 123 * 10^-2 as 1.23, precondition e < 0 *) let numTok_dot () = let s, i = - if Bigint.is_pos_or_zero i then NumTok.SPlus, Bigint.to_string i - else NumTok.SMinus, Bigint.(to_string (neg i)) in + if Z.sign i >= 0 then NumTok.SPlus, Z.to_string i + else NumTok.SMinus, Z.(to_string (neg i)) in let ni = String.length i in - let e = - (Bigint.to_int e) in + let e = - (Z.to_int e) in assert (e > 0); let i, f = if e < ni then String.sub i 0 (ni - e), String.sub i (ni - e) e @@ -178,12 +177,12 @@ let rawnum_of_r c = begin match DAst.get r with | GApp (p, [t; e]) when is_gr p glob_pow_pos -> let t = bigint_of_z t in - if not (Bigint.(equal t (of_int 10))) then + if not (Z.(equal t (of_int 10))) then raise Non_closed_number else let i = bigint_of_z l in let e = bignat_of_pos e in - let e = if is_gr md glob_Rdiv then neg e else e in + let e = if is_gr md glob_Rdiv then Z.neg e else e in numTok_of_int_exp i e | _ -> raise Non_closed_number end -- cgit v1.2.3 From 5a28133182c75292d9b2adc7826cba47e6a138a7 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Tue, 16 Oct 2018 15:10:45 +0000 Subject: [nsatz] num → zarith --- plugins/nsatz/ideal.ml | 6 ++-- plugins/nsatz/nsatz.ml | 81 ++++++++++++++++++++++------------------------- plugins/nsatz/polynom.ml | 10 +++--- plugins/nsatz/polynom.mli | 4 +-- 4 files changed, 47 insertions(+), 54 deletions(-) (limited to 'plugins') diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml index 387145a5d0..cbc1773ede 100644 --- a/plugins/nsatz/ideal.ml +++ b/plugins/nsatz/ideal.ml @@ -153,8 +153,8 @@ end module Make (P:Polynom.S) = struct type coef = P.t - let coef0 = P.of_num (Num.Int 0) - let coef1 = P.of_num (Num.Int 1) + let coef0 = P.of_num Q.zero + let coef1 = P.of_num Q.one let string_of_coef c = "["^(P.to_string c)^"]" (*********************************************************************** @@ -305,7 +305,7 @@ let mult_t_pol a m 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) +let coef_of_int x = P.of_num (Q.of_int x) (* variable i *) let gen d i = diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index 29d08fb4ea..f3021f4ee6 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -13,30 +13,20 @@ open Util open Constr open Tactics -open Num open Utile (*********************************************************************** Operations on coefficients *) -let num_0 = Int 0 -and num_1 = Int 1 -and num_2 = Int 2 - -let numdom r = - let r' = Ratio.normalize_ratio (ratio_of_num r) in - num_of_big_int(Ratio.numerator_ratio r'), - num_of_big_int(Ratio.denominator_ratio r') - module BigInt = struct - open Big_int + open Big_int_Z type t = big_int let of_int = big_int_of_int let coef0 = of_int 0 - let of_num = Num.big_int_of_num - let to_num = Num.num_of_big_int + let of_num = Q.to_bigint + let to_num = Q.of_bigint let equal = eq_big_int let lt = lt_big_int let le = le_big_int @@ -113,7 +103,7 @@ type vname = string type term = | Zero - | Const of Num.num + | Const of Q.t | Var of vname | Opp of term | Add of term * term @@ -122,7 +112,7 @@ type term = | Pow of term * int let const n = - if eq_num n num_0 then Zero else Const n + if Q.(equal zero) n then Zero else Const n let pow(p,i) = if Int.equal i 1 then p else Pow(p,i) let add = function (Zero,q) -> q @@ -131,8 +121,8 @@ let add = function let mul = function (Zero,_) -> Zero | (_,Zero) -> Zero - | (p,Const n) when eq_num n num_1 -> p - | (Const n,q) when eq_num n num_1 -> q + | (p,Const n) when Q.(equal one) n -> p + | (Const n,q) when Q.(equal one) n -> q | (p,q) -> Mul(p,q) let gen_constant n = lazy (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n)) @@ -167,62 +157,64 @@ let mkt_app name l = mkApp (Lazy.force name, Array.of_list l) let tlp () = mkt_app tlist [mkt_app tpexpr [Lazy.force tz]] let tllp () = mkt_app tlist [tlp()] -let rec mkt_pos n = - if n =/ num_1 then Lazy.force pxH - else if mod_num n num_2 =/ num_0 then - mkt_app pxO [mkt_pos (quo_num n num_2)] +let mkt_pos n = + let rec mkt_pos n = + if Z.(equal one) n then Lazy.force pxH + else if Z.is_even n then + mkt_app pxO [mkt_pos Z.(n asr 1)] else - mkt_app pxI [mkt_pos (quo_num n num_2)] + mkt_app pxI [mkt_pos Z.(n asr 1)] + in mkt_pos (Q.to_bigint n) let mkt_n n = - if Num.eq_num n num_0 + if Q.(equal zero) n then Lazy.force nN0 else mkt_app nNpos [mkt_pos n] let mkt_z z = - if z =/ num_0 then Lazy.force z0 - else if z >/ num_0 then + if Q.(equal zero) z then Lazy.force z0 + else if Q.(lt zero) z then mkt_app zpos [mkt_pos z] else - mkt_app zneg [mkt_pos ((Int 0) -/ z)] + mkt_app zneg [mkt_pos (Q.neg z)] let rec mkt_term t = match t with -| Zero -> mkt_term (Const num_0) -| Const r -> let (n,d) = numdom r in - mkt_app ttconst [Lazy.force tz; mkt_z n] -| Var v -> mkt_app ttvar [Lazy.force tz; mkt_pos (num_of_string v)] +| Zero -> mkt_term (Const Q.zero) +| Const r -> let n = r |> Q.num |> Q.of_bigint in + mkt_app ttconst [Lazy.force tz; mkt_z n] +| Var v -> mkt_app ttvar [Lazy.force tz; mkt_pos (Q.of_string v)] | Opp t1 -> mkt_app ttopp [Lazy.force tz; mkt_term t1] | 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 Int.equal n 0 then - mkt_app ttconst [Lazy.force tz; mkt_z num_1] + mkt_app ttconst [Lazy.force tz; mkt_z Q.one] else - mkt_app ttpow [Lazy.force tz; mkt_term t1; mkt_n (num_of_int n)] + mkt_app ttpow [Lazy.force tz; mkt_term t1; mkt_n (Q.of_int n)] let rec parse_pos p = match Constr.kind p with | App (a,[|p2|]) -> - if Constr.equal a (Lazy.force pxO) then num_2 */ (parse_pos p2) - else num_1 +/ (num_2 */ (parse_pos p2)) -| _ -> num_1 + if Constr.equal a (Lazy.force pxO) then Q.(mul (of_int 2)) (parse_pos p2) + else Q.(add one) Q.(mul (of_int 2) (parse_pos p2)) +| _ -> Q.one let parse_z z = match Constr.kind z with | App (a,[|p2|]) -> - if Constr.equal a (Lazy.force zpos) then parse_pos p2 else (num_0 -/ (parse_pos p2)) -| _ -> num_0 + if Constr.equal a (Lazy.force zpos) then parse_pos p2 else Q.neg (parse_pos p2) +| _ -> Q.zero let parse_n z = match Constr.kind z with | App (a,[|p2|]) -> parse_pos p2 -| _ -> num_0 +| _ -> Q.zero let rec parse_term p = match Constr.kind p with | App (a,[|_;p2|]) -> - if Constr.equal a (Lazy.force ttvar) then Var (string_of_num (parse_pos p2)) + if Constr.equal a (Lazy.force ttvar) then Var (Q.to_string (parse_pos p2)) else if Constr.equal a (Lazy.force ttconst) then Const (parse_z p2) else if Constr.equal a (Lazy.force ttopp) then Opp (parse_term p2) else Zero @@ -231,7 +223,7 @@ let rec parse_term p = else if Constr.equal a (Lazy.force ttsub) then Sub (parse_term p2, parse_term p3) else if Constr.equal a (Lazy.force ttmul) then Mul (parse_term p2, parse_term p3) else if Constr.equal a (Lazy.force ttpow) then - Pow (parse_term p2, int_of_num (parse_n p3)) + Pow (parse_term p2, Q.to_int (parse_n p3)) else Zero | _ -> Zero @@ -278,7 +270,7 @@ let term_pol_sparse nvars np t= match t with | Zero -> zeroP | Const r -> - if Num.eq_num r num_0 + if Q.(equal zero) r then zeroP else polconst d (Poly.Pint (Coef.of_num r)) | Var v -> @@ -316,7 +308,7 @@ let pol_sparse_to_term n2 p = let p = PIdeal.repr p in let rec aux p = match p with - [] -> const (num_of_string "0") + [] -> const Q.zero | (a,m)::p1 -> let m = Ideal.Monomial.repr m in let n = (Array.length m)-1 in @@ -443,8 +435,9 @@ let expand_pol lb lp = let theoremedeszeros_termes lp = let nvars = List.fold_left set_nvars_term 0 lp in match lp with - | Const (Int sugarparam)::Const (Int nparam)::lp -> - ((match sugarparam with + | Const sugarparam :: Const nparam :: lp -> + let nparam = Q.to_int nparam in + ((match Q.to_int sugarparam with |0 -> sinfo "computation without sugar"; lexico:=false; |1 -> sinfo "computation with sugar"; diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml index 726ad54cad..2565d88b13 100644 --- a/plugins/nsatz/polynom.ml +++ b/plugins/nsatz/polynom.ml @@ -30,7 +30,7 @@ module type Coef = sig val pgcd : t -> t -> t val hash : t -> int - val of_num : Num.num -> t + val of_num : Q.t -> t val to_string : t -> string end @@ -39,7 +39,7 @@ module type S = sig type variable = int type t = Pint of coef | Prec of variable * t array - val of_num : Num.num -> t + val of_num : Q.t -> t val x : variable -> t val monome : variable -> int -> t val is_constantP : t -> bool @@ -106,7 +106,7 @@ end module Make (C:Coef) = struct type coef = C.t -let coef_of_int i = C.of_num (Num.Int i) +let coef_of_int i = C.of_num (Q.of_int i) let coef0 = coef_of_int 0 let coef1 = coef_of_int 1 @@ -125,8 +125,8 @@ type t = (* constant polynomials *) let of_num x = Pint (C.of_num x) -let cf0 = of_num (Num.Int 0) -let cf1 = of_num (Num.Int 1) +let cf0 = of_num Q.zero +let cf1 = of_num Q.one (* nth variable *) let x n = Prec (n,[|cf0;cf1|]) diff --git a/plugins/nsatz/polynom.mli b/plugins/nsatz/polynom.mli index 3807a8582b..91f1bcda90 100644 --- a/plugins/nsatz/polynom.mli +++ b/plugins/nsatz/polynom.mli @@ -26,7 +26,7 @@ module type Coef = sig val pgcd : t -> t -> t val hash : t -> int - val of_num : Num.num -> t + val of_num : Q.t -> t val to_string : t -> string end @@ -35,7 +35,7 @@ module type S = sig type variable = int type t = Pint of coef | Prec of variable * t array - val of_num : Num.num -> t + val of_num : Q.t -> t val x : variable -> t val monome : variable -> int -> t val is_constantP : t -> bool -- cgit v1.2.3