From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 20:04:58 +0200 Subject: Remove some unused values and types --- plugins/nsatz/ideal.ml | 57 -------------------------------------------------- plugins/nsatz/nsatz.ml | 28 ------------------------- 2 files changed, 85 deletions(-) (limited to 'plugins/nsatz') diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml index b1ff59e78..41f2edfcf 100644 --- a/plugins/nsatz/ideal.ml +++ b/plugins/nsatz/ideal.ml @@ -153,7 +153,6 @@ 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 coefm1 = P.of_num (Num.Int (-1)) let string_of_coef c = "["^(P.to_string c)^"]" (*********************************************************************** @@ -252,59 +251,6 @@ let string_of_pol zeroP hdP tlP coefterm monterm string_of_coef in (stringP p true) - - -let print_pol zeroP hdP tlP coefterm monterm string_of_coef - dimmon string_of_exp lvar p = - - let rec print_mon m coefone = - let s=ref [] in - for i=1 to (dimmon m) do - (match (string_of_exp m i) with - "0" -> () - | "1" -> s:= (!s) @ [(getvar lvar (i-1))] - | e -> s:= (!s) @ [((getvar lvar (i-1)) ^ "^" ^ e)]); - done; - (match !s with - [] -> if coefone - then print_string "1" - else () - | l -> if coefone - then print_string (String.concat "*" l) - else (print_string "*"; - print_string (String.concat "*" l))) - and print_term t start = let a = coefterm t and m = monterm t in - match (string_of_coef a) with - "0" -> () - | "1" ->(match start with - true -> print_mon m true - |false -> (print_string "+ "; - print_mon m true)) - | "-1" ->(print_string "-";print_space();print_mon m true) - | c -> if (String.get c 0)='-' - then (print_string "- "; - print_string (String.sub c 1 - ((String.length c)-1)); - print_mon m false) - else (match start with - true -> (print_string c;print_mon m false) - |false -> (print_string "+ "; - print_string c;print_mon m false)) - and printP p start = - if (zeroP p) - then (if start - then print_string("0") - else ()) - else (print_term (hdP p) start; - if start then open_hovbox 0; - print_space(); - print_cut(); - printP (tlP p) false) - in open_hovbox 3; - printP p true; - print_flush() - - let stringP metadata (p : poly) = string_of_pol (fun p -> match p with [] -> true | _ -> false) @@ -595,9 +541,6 @@ let addS x l = l @ [x] (* oblige de mettre en queue sinon le certificat decon critical pairs/s-polynomials *) -let ordcpair ((i1,j1),m1) ((i2,j2),m2) = - compare_mon m1 m2 - module CPair = struct type t = (int * int) * Monomial.t diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index a5b016611..632b9dac1 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -22,7 +22,6 @@ open Utile let num_0 = Int 0 and num_1 = Int 1 and num_2 = Int 2 -and num_10 = Int 10 let numdom r = let r' = Ratio.normalize_ratio (ratio_of_num r) in @@ -35,7 +34,6 @@ module BigInt = struct type t = big_int let of_int = big_int_of_int let coef0 = of_int 0 - let coef1 = of_int 1 let of_num = Num.big_int_of_num let to_num = Num.num_of_big_int let equal = eq_big_int @@ -49,7 +47,6 @@ module BigInt = struct let div = div_big_int let modulo = mod_big_int let to_string = string_of_big_int - let to_int x = int_of_big_int x let hash x = try (int_of_big_int x) with Failure _ -> 1 @@ -61,15 +58,6 @@ module BigInt = struct then a else if lt a b then pgcd b a else pgcd b (modulo a b) - - (* signe du pgcd = signe(a)*signe(b) si non nuls. *) - let pgcd2 a b = - if equal a coef0 then b - else if equal b coef0 then a - else let c = pgcd (abs a) (abs b) in - if ((lt coef0 a)&&(lt b coef0)) - ||((lt coef0 b)&&(lt a coef0)) - then opp c else c end (* @@ -146,8 +134,6 @@ let mul = function | (Const n,q) when eq_num n num_1 -> q | (p,q) -> Mul(p,q) -let unconstr = mkRel 1 - let tpexpr = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PExpr") let ttconst = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEc") @@ -271,20 +257,6 @@ let set_nvars_term nvars t = | Pow (t1,n) -> aux t1 nvars in aux t nvars -let string_of_term p = - let rec aux p = - match p with - | Zero -> "0" - | Const r -> string_of_num r - | Var v -> "x"^v - | Opp t1 -> "(-"^(aux t1)^")" - | Add (t1,t2) -> "("^(aux t1)^"+"^(aux t2)^")" - | Sub (t1,t2) -> "("^(aux t1)^"-"^(aux t2)^")" - | Mul (t1,t2) -> "("^(aux t1)^"*"^(aux t2)^")" - | Pow (t1,n) -> (aux t1)^"^"^(string_of_int n) - in aux p - - (*********************************************************************** Coefficients: recursive polynomials *) -- cgit v1.2.3