diff options
author | 2009-03-20 01:22:58 +0000 | |
---|---|---|
committer | 2009-03-20 01:22:58 +0000 | |
commit | 7d220f8b61649646692983872626d6a8042446a9 (patch) | |
tree | fefceb2c59cf155c55fffa25ad08bec629de523e /plugins/groebner/utile.ml | |
parent | ad1fea78e3c23c903b2256d614756012d5f05d87 (diff) |
Directory 'contrib' renamed into 'plugins', to end confusion with archive of user contribs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/groebner/utile.ml')
-rw-r--r-- | plugins/groebner/utile.ml | 161 |
1 files changed, 161 insertions, 0 deletions
diff --git a/plugins/groebner/utile.ml b/plugins/groebner/utile.ml new file mode 100644 index 000000000..52a69dc10 --- /dev/null +++ b/plugins/groebner/utile.ml @@ -0,0 +1,161 @@ +(*********************************************************************** + Utilitaires. +*) + +(* Impression *) + +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 = + output_string stderr s; flush stderr + +(********************************************************************** + Listes +*) + +(* appartenance à une liste , on donne l'égalité *) +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) + +(* vire les repetitions d'une liste, on donne l'égalité *) +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 + + +(*********************************************************************** + Un outil pour faire une mémo-fonction: + fonction est la fonction(!) + memoire est une référence au graphe déjà calculé + (liste de couples, c'est une variable globale) + egal est l'égalité sur les arguments + valeur est une valeur possible de la fonction (sert uniquement pour le typage) +*) + +let memo memoire egal valeur fonction x = + let res = ref valeur in + try (List.iter (fun (y,v) -> if egal y x + then (res:=v; + failwith "trouve")) + !memoire; + let v = fonction x in + memoire:=(x,v)::(!memoire); + v) + with _ -> !res + + +(* un autre plus efficace, + utilisant une fonction intermediaire (utile si on n'a pas + l'égalité = sur les arguments de fonction) + s chaîne imprimée s'il n'y a pas calcul *) + +let memos s memoire print fonction x = + try (let v = Hashtbl.find memoire (print x) in pr s;v) + with _ -> (pr "#"; + let v = fonction x in + Hashtbl.add memoire (print 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) + + +*) + + |