diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /plugins/nsatz/utile.ml | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'plugins/nsatz/utile.ml')
-rw-r--r-- | plugins/nsatz/utile.ml | 130 |
1 files changed, 130 insertions, 0 deletions
diff --git a/plugins/nsatz/utile.ml b/plugins/nsatz/utile.ml new file mode 100644 index 00000000..c16bd425 --- /dev/null +++ b/plugins/nsatz/utile.ml @@ -0,0 +1,130 @@ +(* 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 _ -> (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 _ -> ()) + 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 _ -> 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 _ -> ()) + 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) + +*) + + |