diff options
Diffstat (limited to 'plugins/fourier/fourierR.ml')
| -rw-r--r-- | plugins/fourier/fourierR.ml | 40 |
1 files changed, 22 insertions, 18 deletions
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 2cabcf52..48493785 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: fourierR.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - (* La tactique Fourier ne fonctionne de manière sûre que si les coefficients @@ -31,17 +29,23 @@ qui donne le coefficient d'un terme du calcul des constructions, qui est zéro si le terme n'y est pas. *) -type flin = {fhom:(constr , rational)Hashtbl.t; +module Constrhash = Hashtbl.Make + (struct type t = constr + let equal = eq_constr + let hash = hash_constr + end) + +type flin = {fhom: rational Constrhash.t; fcste:rational};; -let flin_zero () = {fhom=Hashtbl.create 50;fcste=r0};; +let flin_zero () = {fhom=Constrhash.create 50;fcste=r0};; -let flin_coef f x = try (Hashtbl.find f.fhom x) with _-> r0;; +let flin_coef f x = try (Constrhash.find f.fhom x) with _-> r0;; let flin_add f x c = let cx = flin_coef f x in - Hashtbl.remove f.fhom x; - Hashtbl.add f.fhom x (rplus cx c); + Constrhash.remove f.fhom x; + Constrhash.add f.fhom x (rplus cx c); f ;; let flin_add_cste f c = @@ -53,20 +57,20 @@ let flin_one () = flin_add_cste (flin_zero()) r1;; let flin_plus f1 f2 = let f3 = flin_zero() in - Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom; - Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom; + Constrhash.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom; + Constrhash.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom; flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste; ;; let flin_minus f1 f2 = let f3 = flin_zero() in - Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom; - Hashtbl.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom; + Constrhash.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom; + Constrhash.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom; flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste); ;; let flin_emult a f = let f2 = flin_zero() in - Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom; + Constrhash.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom; flin_add_cste f2 (rmult a f.fcste); ;; @@ -167,7 +171,7 @@ let rec flin_of_constr c = let flin_to_alist f = let res=ref [] in - Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f; + Constrhash.iter (fun x c -> res:=(c,x)::(!res)) f; !res ;; @@ -256,17 +260,17 @@ let ineq1_of_constr (h,t) = let fourier_lineq lineq1 = let nvar=ref (-1) in - let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *) + let hvar=Constrhash.create 50 in (* la table des variables des inéquations *) List.iter (fun f -> - Hashtbl.iter (fun x _ -> if not (Hashtbl.mem hvar x) then begin + Constrhash.iter (fun x _ -> if not (Constrhash.mem hvar x) then begin nvar:=(!nvar)+1; - Hashtbl.add hvar x (!nvar) + Constrhash.add hvar x (!nvar) end) f.hflin.fhom) lineq1; let sys= List.map (fun h-> let v=Array.create ((!nvar)+1) r0 in - Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x)<-c) + Constrhash.iter (fun x c -> v.(Constrhash.find hvar x)<-c) h.hflin.fhom; ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict)) lineq1 in |