bug in hypotesis parsing solved

[helm.git] / helm / gTopLevel / fourier.ml

diff --git a/helm/gTopLevel/fourier.ml b/helm/gTopLevel/fourier.ml
index c1a40e6e10f52c76337bed8538461cf7dec105b2..d7728c0b338e7b4fa12066c60007463dcef530e4 100644 (file)
--- a/helm/gTopLevel/fourier.ml
+++ b/helm/gTopLevel/fourier.ml
@@ -21,7 +21,7 @@ Pages: 326-327
 http://gallica.bnf.fr/
 *)
 
-
+(** @author The Coq Development Team *)
 
 
 (* Un peu de calcul sur les rationnels... 
@@ -30,10 +30,14 @@ i.e. le num
 *)
 
 
+(** Type for coefficents *)
+type rational = {
+num:int; (** Numerator *)
+den:int;  (** Denumerator *)
+};;
 
-type rational = {num:int;
-                 den:int}
-;;
+(** Debug function.
+    @param x the rational to print*)
 let print_rational x =
         print_int x.num;
         print_string "/";
@@ -42,8 +46,9 @@ let print_rational x =
 
 let rec pgcd x y = if y = 0 then x else pgcd y (x mod y);;
 
-
+(** The constant 0*)
 let r0 = {num=0;den=1};;
+(** The constant 1*)
 let r1 = {num=1;den=1};;
 
 let rnorm x = let x = (if x.den<0 then {num=(-x.num);den=(-x.den)} else x) in
@@ -51,22 +56,41 @@ let rnorm x = let x = (if x.den<0 then {num=(-x.num);den=(-x.den)} else x) in
               else (let d=pgcd x.num x.den in
                    let d= (if d<0 then -d else d) in
                     {num=(x.num)/d;den=(x.den)/d});;
- 
+
+(** Calculates the opposite of a rational.
+    @param x The rational
+    @return -x*)
 let rop x = rnorm {num=(-x.num);den=x.den};;
 
+(** Sums two rationals.
+    @param x A rational
+    @param y Another rational
+    @return x+y*)
 let rplus x y = rnorm {num=x.num*y.den + y.num*x.den;den=x.den*y.den};;
-
+(** Substracts two rationals.
+    @param x A rational
+    @param y Another rational
+    @return x-y*)
 let rminus x y = rnorm {num=x.num*y.den - y.num*x.den;den=x.den*y.den};;
-
+(** Multiplyes two rationals.
+    @param x A rational
+    @param y Another rational
+    @return x*y*)
 let rmult x y = rnorm {num=x.num*y.num;den=x.den*y.den};;
-
+(** Inverts arational.
+    @param x A rational
+    @return x{^ -1} *)
 let rinv x = rnorm {num=x.den;den=x.num};;
-
+(** Divides two rationals.
+    @param x A rational
+    @param y Another rational
+    @return x/y*)
 let rdiv x y = rnorm {num=x.num*y.den;den=x.den*y.num};;
 
 let rinf x y = x.num*y.den < y.num*x.den;;
 let rinfeq x y = x.num*y.den <= y.num*x.den;;
 
+
 (* {coef;hist;strict}, où coef=[c1; ...; cn; d], représente l'inéquation
 c1x1+...+cnxn < d si strict=true, <= sinon,
 hist donnant les coefficients (positifs) d'une combinaison linéaire qui permet d'obtenir l'inéquation à partir de celles du départ.
@@ -147,12 +171,14 @@ let deduce_add lneg lpos =
 (* élimination de la première variable à partir d'une liste d'inéquations:
 opération qu'on itère dans l'algorithme de Fourier.
 *)
-let deduce1 s =
+let deduce1 s i=
     match (partitionne s) with 
       [lneg;lnul;lpos] ->
-    let lnew = deduce_add lneg lpos in
-    (List.map ie_tl lnul)@lnew
-     |_->assert false
+         let lnew = deduce_add lneg lpos in
+        (match lneg with [] -> print_string("non posso ridurre "^string_of_int i^"\n")|_->();
+         match lpos with [] -> print_string("non posso ridurre "^string_of_int i^"\n")|_->());
+         (List.map ie_tl lnul)@lnew
+   |_->assert false
 ;;
 (* algorithme de Fourier: on élimine successivement toutes les variables.
 *)
@@ -160,18 +186,25 @@ let deduce lie =
    let n = List.length (fst (List.hd lie)) in
    let lie=ref (add_hist lie) in
    for i=1 to n-1 do
-      lie:= deduce1 !lie;
+      lie:= deduce1 !lie i;
    done;
    !lie
 ;;
 
-(* donne [] si le système a des solutions,
+(* donne [] si le système a des  find solutions,
 sinon donne [c,s,lc]
 où lc est la combinaison linéaire des inéquations de départ
 qui donne 0 < c si s=true
        ou 0 <= c sinon
 cette inéquation étant absurde.
 *)
+(** Tryes to find if the system admits solutions.
+    @param lie the list of inequations 
+    @return a list that can be empty if the system has solutions. Otherwise it returns a
+            one elements list [\[(c,s,lc)\]]. {b c} is the rational that can be obtained solving the system,
+           {b s} is true if the inequation that proves that the system is absurd is of type [c < 0], false if 
+           [c <= 0], {b lc} is a list of rational that represents the liear combination to obtain the
+           absurd inequation *)
 let unsolvable lie =
    let lr = deduce lie in
    let res = ref [] in