summaryrefslogtreecommitdiff
path: root/plugins/nsatz/utile.ml
blob: 8e2fc07c042c5082297760a6fd82069f3ca29cd7 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
(* Printing *)

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 info s =
  Flags.if_verbose prerr_string 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 Errors.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 Errors.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 Errors.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)

*)