X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Ffourier.ml;h=3704bf67bb388e3e23973d3b50db35144e9d25fd;hb=8b9c9eae1f9da8908ede64b37f04bb7d9e476f7a;hp=bb8b4ea136316365d262a56825ba71b495ea69ab;hpb=5a8a7dd777c55a9907699a709760b0616b571919;p=helm.git

diff --git a/helm/gTopLevel/fourier.ml b/helm/gTopLevel/fourier.ml
index bb8b4ea13..3704bf67b 100644
--- a/helm/gTopLevel/fourier.ml
+++ b/helm/gTopLevel/fourier.ml
@@ -21,13 +21,23 @@ Pages: 326-327
 http://gallica.bnf.fr/
 *)
 
+(** @author The Coq Development Team *)
+
+
 (* Un peu de calcul sur les rationnels... 
 Les opérations rendent des rationnels normalisés,
 i.e. le numérateur et le dénominateur sont premiers entre eux.
 *)
-type rational = {num:int;
-                 den:int}
-;;
+
+
+(** Type for coefficents *)
+type rational = {
+num:int; (** Numerator *)
+den:int;  (** Denumerator *)
+};;
+
+(** Debug function.
+    @param x the rational to print*)
 let print_rational x =
         print_int x.num;
         print_string "/";
@@ -36,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
@@ -45,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.
@@ -159,13 +189,20 @@ let deduce lie =
    !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
@@ -202,4 +239,4 @@ let test2=[
 deduce test2;;
 unsolvable test2;;
 
-*)
\ No newline at end of file
+*)