summaryrefslogtreecommitdiff
path: root/plugins/fourier/fourierR.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/fourier/fourierR.ml')
-rw-r--r--plugins/fourier/fourierR.ml56
1 files changed, 32 insertions, 24 deletions
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 2cabcf52..e0e4f7d6 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-2012 *)
(* \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 Not_found -> 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);
;;
@@ -137,10 +141,12 @@ let rec flin_of_constr c =
(try (let a=(rational_of_constr args.(0)) in
try (let b = (rational_of_constr args.(1)) in
(flin_add_cste (flin_zero()) (rmult a b)))
- with _-> (flin_add (flin_zero())
+ with e when Errors.noncritical e ->
+ (flin_add (flin_zero())
args.(1)
a))
- with _-> (flin_add (flin_zero())
+ with e when Errors.noncritical e ->
+ (flin_add (flin_zero())
args.(0)
(rational_of_constr args.(1))))
| "Rinv"->
@@ -150,7 +156,8 @@ let rec flin_of_constr c =
(let b=(rational_of_constr args.(1)) in
try (let a = (rational_of_constr args.(0)) in
(flin_add_cste (flin_zero()) (rdiv a b)))
- with _-> (flin_add (flin_zero())
+ with e when Errors.noncritical e ->
+ (flin_add (flin_zero())
args.(0)
(rinv b)))
|_->assert false)
@@ -160,14 +167,15 @@ let rec flin_of_constr c =
|"R0" -> flin_zero ()
|_-> assert false)
|_-> assert false)
- with _ -> flin_add (flin_zero())
+ with e when Errors.noncritical e ->
+ flin_add (flin_zero())
c
r1
;;
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 +264,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
@@ -490,13 +498,13 @@ let rec fourier gl=
|_->assert false)
|_->assert false
in tac gl)
- with _ ->
+ with e when Errors.noncritical e ->
(* les hypothèses *)
let hyps = List.map (fun (h,t)-> (mkVar h,t))
(list_of_sign (pf_hyps gl)) in
let lineq =ref [] in
List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
- with _ -> ())
+ with e when Errors.noncritical e -> ())
hyps;
(* lineq = les inéquations découlant des hypothèses *)
if !lineq=[] then Util.error "No inequalities";