From 28127d3bb4a0e151820e04a3efc4846ababb7d71 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Wed, 10 Oct 2018 08:35:43 +0000
Subject: [nsatz] remove dead code

---
 plugins/nsatz/utile.ml  | 109 ------------------------------------------------
 plugins/nsatz/utile.mli |  13 ------
 2 files changed, 122 deletions(-)

(limited to 'plugins')

diff --git a/plugins/nsatz/utile.ml b/plugins/nsatz/utile.ml
index d3cfd75e56..1caa042db6 100644
--- a/plugins/nsatz/utile.ml
+++ b/plugins/nsatz/utile.ml
@@ -3,116 +3,7 @@
 let pr x =
   if !Flags.debug then (Format.printf "@[%s@]" x; flush(stdout);)else ()
 
-let prn x =
-  if !Flags.debug then (Format.printf "@[%s\n@]" x; flush(stdout);) else ()
-
 let prt0 s = () (* print_string s;flush(stdout)*)
 
-let prt s =
-  if !Flags.debug then (print_string (s^"\n");flush(stdout)) else ()
-
 let sinfo s = if !Flags.debug then Feedback.msg_debug (Pp.str s)
 let info s = if !Flags.debug then Feedback.msg_debug (Pp.str (s ()))
-
-(* Lists *)
-
-let rec list_mem_eq eq x l =
-  match l with
-    [] -> false
-   |y::l1 -> if (eq x y) then true else (list_mem_eq eq x l1)
-
-let set_of_list_eq eq l =
-   let res = ref [] in
-   List.iter (fun x -> if not (list_mem_eq eq x (!res)) then res:=x::(!res)) l;
-   List.rev !res
-
-(**********************************************************************
-  Eléments minimaux pour un ordre partiel de division.
-  E est un ensemble, avec une multiplication
-  et une division partielle div (la fonction div peut échouer),
-  constant est un prédicat qui définit un sous-ensemble C de E.
-*)
-(*
-  Etant donnée une partie A de E, on calcule une partie B de E disjointe de C
-  telle que:
-    - les éléments de A sont des produits d'éléments de B et d'un de C.
-    - B est minimale pour cette propriété.
-*)
-
-let facteurs_liste div constant lp =
-   let lp = List.filter (fun x -> not (constant x)) lp in
-   let rec factor lmin lp = (* lmin: ne se divisent pas entre eux *)
-      match lp with
-        [] -> lmin
-       |p::lp1 ->
-         (let l1 = ref [] in
-          let p_dans_lmin = ref false in
-          List.iter (fun q -> try (let r = div p q in
-                                   if not (constant r)
-				   then l1:=r::(!l1)
-                                   else p_dans_lmin:=true)
-			      with e when CErrors.noncritical e -> ())
-                     lmin;
-          if !p_dans_lmin
-          then factor lmin lp1
-          else if (!l1)=[]
-          (* aucun q de lmin ne divise p *)
-          then (let l1=ref lp1 in
-		let lmin1=ref [] in
-                List.iter (fun q -> try (let r = div q p in
-					 if not (constant r)
-					 then l1:=r::(!l1))
-				    with e when CErrors.noncritical e ->
-                                      lmin1:=q::(!lmin1))
-                          lmin;
-	        factor (List.rev (p::(!lmin1))) !l1)
-          (* au moins un q de lmin divise p non trivialement *)
-          else factor lmin ((!l1)@lp1))
-    in
-    factor [] lp
-
-
-(* On suppose que tout élément de A est produit d'éléments de B et d'un de C:
-   A et B sont deux tableaux,  rend un tableau de couples
-      (élément de C, listes d'indices l)
-   tels que A.(i) = l.(i)_1*Produit(B.(j), j dans l.(i)_2)
-   zero est un prédicat sur E tel que (zero x) => (constant x):
-         si (zero x) est vrai on ne decompose pas x
-   c est un élément quelconque de E.
-*)
-let factorise_tableau div zero c f l1 =
-    let res = Array.make (Array.length f) (c,[]) in
-    Array.iteri (fun i p ->
-      let r = ref p in
-      let li = ref [] in
-      if not (zero p)
-      then
-      Array.iteri (fun j q ->
-	              try (while true do
-                               let rr = div !r q in
-      	                       li:=j::(!li);
-                               r:=rr;
-			   done)
-                      with e when CErrors.noncritical e -> ())
-                  l1;
-      res.(i)<-(!r,!li))
-     f;
-    (l1,res)
-
-
-(* exemples:
-
-let l =  [1;2;6;24;720]
-and div1 = (fun a b -> if a mod b =0 then a/b else failwith "div")
-and constant = (fun x -> x<2)
-and zero = (fun x -> x=0)
-
-
-let f = facteurs_liste div1 constant l
-
-
-factorise_tableau div1 zero 0 (Array.of_list l) (Array.of_list f)
-
-*)
-
-
diff --git a/plugins/nsatz/utile.mli b/plugins/nsatz/utile.mli
index 9308577e0f..5af7ece5a3 100644
--- a/plugins/nsatz/utile.mli
+++ b/plugins/nsatz/utile.mli
@@ -1,19 +1,6 @@
 
 (* Printing *)
 val pr : string -> unit
-val prn : string -> unit
 val prt0 : 'a -> unit
-val prt : string -> unit
 val info : (unit -> string) -> unit
 val sinfo : string -> unit
-
-(* Listes *)
-val list_mem_eq : ('a -> 'b -> bool) -> 'a -> 'b list -> bool
-val set_of_list_eq : ('a -> 'a -> bool) -> 'a list -> 'a list
-
-
-val facteurs_liste : ('a -> 'a -> 'a) -> ('a -> bool) -> 'a list -> 'a list
-val factorise_tableau :
-  ('a -> 'b -> 'a) ->
-  ('a -> bool) ->
-  'a -> 'a array -> 'b array -> 'b array * ('a * int list) array
-- 
cgit v1.2.3