summaryrefslogtreecommitdiff
path: root/plugins/nsatz/utile.ml
blob: 17c8654ba4b880ea3d51a4d74d483a285c7fb39a (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
119
120
121
122
123
124
125
126
127
128
129
130
131
132
(* 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


(* Memoization
   f is compatible with nf: f(nf(x)) = f(x)
*)

let memos s memoire nf f x =
   try (let v = Hashtbl.find memoire (nf x) in pr s;v)
   with e when Errors.noncritical e ->
     (pr "#";
      let v = f x in
      Hashtbl.add memoire (nf x) v;
      v)


(**********************************************************************
  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.create (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)

*)