From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 26 Nov 2002 19:45:48 +0000 (+0000)
Subject: comments in fourier.ml now are in ocamldoc style
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c6b222d016300d3b123a4d1863c048b950292844;p=helm.git

comments in fourier.ml now are in ocamldoc style
bug in fourierR.ml (wrong Rel) solved
---

diff --git a/helm/gTopLevel/fourier.ml b/helm/gTopLevel/fourier.ml
index c1a40e6e1..3704bf67b 100644
--- 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.
@@ -165,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
diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index 17ff3f8fe..d6d5fd34a 100644
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -461,7 +461,7 @@ let fourier_lineq lineq1 =
    debug("Il numero di incognite e' "^string_of_int (!nvar+1)^"\n");
    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) 
+               Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x) <- c) 
                   h.hflin.fhom;
                ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
              lineq1 in
@@ -847,7 +847,7 @@ let rec strip_outer_cast c = match c with
   | _ -> c
 ;;
 
-let find_in_context id context =
+(*let find_in_context id context =
   let rec find_in_context_aux c n =
   	match c with
 	[] -> failwith (id^" not found in context")      
@@ -865,10 +865,26 @@ let rec filter_real_hyp context cont =
   [] -> []
   | Some(Cic.Name(h),Cic.Decl(t))::next -> (
   				let n = find_in_context h cont in
+				debug("assegno "^string_of_int n^" a "^CicPp.ppterm t^"\n");
   			[(Cic.Rel(n),t)] @ filter_real_hyp next cont)
   | a::next -> debug("  no\n"); filter_real_hyp next cont
+;;*)
+let filter_real_hyp context _ =
+  let rec filter_aux context num =
+   match context with
+  [] -> []
+  | Some(Cic.Name(h),Cic.Decl(t))::next -> 
+  		(
+  		(*let n = find_in_context h cont in*)
+		debug("assegno "^string_of_int num^" a "^h^":"^CicPp.ppterm t^"\n");
+  		[(Cic.Rel(num),t)] @ filter_aux next (num+1)
+		)
+  | a::next -> filter_aux next (num+1)
+  in
+  filter_aux context 1
 ;;
 
+
 (* lifts everithing at the conclusion level *)	
 let rec superlift c n=
   match c with
@@ -1192,7 +1208,6 @@ theoreme,so let's parse our thesis *)
 		   let w1 = 
 		     debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n");
 		     (match ty with
-		     (* Fix: aspetta mail di Claudio per capire cosa comporta anonimous*)
 		     Cic.Prod (Cic.Anonymous,a,b) -> (Cic.Appl [_not;a])
 		     |_ -> assert false)
 		   in
@@ -1203,14 +1218,6 @@ theoreme,so let's parse our thesis *)
 		  ) 
 		 ~continuation:(*PORTINGTacticals.id_tac*)tac2]))
 	 ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*)
-       (*tac:=(Tacticals.thens 
-         ~start:(PrimitiveTactics.cut_tac ~term:_False)
-	 ~continuations:[Tacticals.then_ 
-	   ~start:(PrimitiveTactics.intros_tac ~name:"??")
-	   ~continuation:contradiction_tac
-	 ;!tac]) FIXED - this was useless*)
-	(* tac:=!tac*)
-
 
     |_-> assert false)(*match (!lutil) *)
   |_-> assert false); (*match res*)
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 8aa9e8288..aca0fe12d 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -60,18 +60,19 @@ let htmlfooter =
  "</html>"
 ;;
 
-(*
+(* TASSI
 let prooffile = "/home/tassi/miohelm/tmp/currentproof";;
-let prooffile = "/public/sacerdot/currentproof";;
+let prooffiletype = "/home/tassi/miohelm/tmp/currentprooftype";;
 *)
 
 let prooffile = "/public/sacerdot/currentproof";;
 let prooffiletype = "/public/sacerdot/currentprooftype";;
 
 (*CSC: the getter should handle the innertypes, not the FS *)
-(*
+
+(* TASSI 
 let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";;
-let innertypesfile = "/public/sacerdot/innertypes";;
+let constanttypefile = "/home/tassi/miohelm/tmp/constanttype";;
 *)
 
 let innertypesfile = "/public/sacerdot/innertypes";;