bug in hypotesis parsing solved

diff --git a/helm/gTopLevel/esempi/fourier.cic b/helm/gTopLevel/esempi/fourier.cic
index ba51e64ad80b3a8ee7dab716b0b34e6b93fe4f3f..d2f9e4983b456c06c95231b3481a8a159e36614c 100644 (file)
--- a/helm/gTopLevel/esempi/fourier.cic
+++ b/helm/gTopLevel/esempi/fourier.cic
@@ -14,7 +14,13 @@ alias eqT    /Coq/Init/Logic_Type/eqT.ind#1/1
 alias not      /Coq/Init/Logic/not.con
 alias or /Coq/Init/Logic/or.ind#1/1
 
-(*test real*)
+//baco
+!x:R.
+(Rlt (Rmult(Ropp x)R1)
+R0)
+->(Rlt R0 x)
+
+// test 3x4 -> 35''
 !x:R.!y:R.!z:R.
 (Rge
 (Rplus
@@ -44,6 +50,39 @@ alias or /Coq/Init/Logic/or.ind#1/1
 
 -> (Rlt z R1)
 
+// test 6x6 -> 
+
+!x:R.!y:R.!z:R.!t:R.!u:R.!v:R.
+(Rgt
+(Rplus (Ropp x) (Rplus y (Rplus z (Rplus t (Rplus u (Rplus v (Rplus R1 R1)))))))
+  R0)
+->
+(Rgt
+(Rplus x (Rplus (Ropp y) (Rplus (Ropp z) (Rplus (Ropp t) (Rplus (Ropp u) (Rplus R1 R1))))))
+  R0)
+->
+(Rgt
+(Rplus y (Rplus (Ropp z) (Rplus t (Rplus u (Rplus R1 R1)))))
+  R0)
+->
+(Rgt
+(Rplus y (Rplus z (Rplus (Ropp t) (Rplus (Ropp (Rmult (Rplus R1 R1)v)) (Rplus R1 R1)))))
+  R0)
+->
+(Rgt
+(Rplus y (Rplus z (Rplus t (Rplus (Ropp u) (Rplus R1 R1)))))
+  R0)
+->
+(Rlt
+(Rplus (Rmult (Rplus R1 R1) x) (Rplus v y))
+  R0)
+-> (Rlt (Rmult (Rplus R1 R1) x) R0)
+
+
+
+
+
+
 //test base1 ok
 !x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1))
 

diff --git a/helm/gTopLevel/fourier.ml b/helm/gTopLevel/fourier.ml
index 3704bf67bb388e3e23973d3b50db35144e9d25fd..d7728c0b338e7b4fa12066c60007463dcef530e4 100644 (file)
--- a/helm/gTopLevel/fourier.ml
+++ b/helm/gTopLevel/fourier.ml
@@ -171,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.
 *)
@@ -184,7 +186,7 @@ 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
 ;;

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index d6d5fd34add30ad755bb73963fdb47689a504925..f6f44e950fe961ce3c7b4f6bb8dd771447b1c1a9 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -146,11 +146,18 @@ let flin_coef f x =
        @param c a rational
        @return the new flin
 *)
-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);
-    f
+let flin_add f x c = 
+    match x with
+    Cic.Rel(n) ->(
+      let cx = flin_coef f x in
+      Hashtbl.remove f.fhom x;
+      Hashtbl.add f.fhom x (rplus cx c);
+      f)
+    |_->debug ("Internal error in Fourier! this is not a Rel "^CicPp.ppterm x^"\n");
+      let cx = flin_coef f x in
+      Hashtbl.remove f.fhom x;
+      Hashtbl.add f.fhom x (rplus cx c);
+      f
 ;;
 (**
        Adds c to f.fcste
@@ -189,7 +196,7 @@ let flin_minus f1 f2 =
 ;;
 
 (**
-       @return f times a
+       @return a times f
 *)
 let flin_emult a f =
     let f2 = flin_zero() in
@@ -248,7 +255,13 @@ let rec rational_of_term t =
 (* coq wrapper
 let rational_of_const = rational_of_term;;
 *)
-
+let fails f a =
+ try
+   let tmp = (f a) in
+   false
+ with 
+   _-> true
+ ;;
 
 let rec flin_of_term t =
        let fl_of_binop f l =
@@ -276,19 +289,59 @@ let rec flin_of_term t =
                let arg1 = (List.hd next) and
                    arg2 = (List.hd(List.tl next)) 
                in
-               try 
+               if fails rational_of_term arg1 
+                  then
+                  if fails rational_of_term arg2
+                     then
+                     ( (* prodotto tra 2 incognite ????? impossibile*)
+                     failwith "Sistemi lineari!!!!\n" 
+                     )
+                     else
+                     (
+                     match arg1 with
+                     Cic.Rel(n) -> (*trasformo al volo*)
+                                   (flin_add (flin_zero()) arg1 (rational_of_term arg2))
+                     |_-> (* test this *)
+                          let tmp = flin_of_term arg1 in
+                          flin_emult  (rational_of_term arg2) (tmp)
+                     )
+                  else
+                  if fails rational_of_term arg2
+                     then
+                     (
+                     match arg2 with
+                     Cic.Rel(n) -> (*trasformo al volo*)
+                                   (flin_add (flin_zero()) arg2 (rational_of_term arg1))
+                     |_-> (* test this *)
+                          let tmp = flin_of_term arg2 in
+                          flin_emult (rational_of_term arg1) (tmp)
+
+                     )
+                     else
+                     (  (*prodotto tra razionali*)
+                     (flin_add_cste (flin_zero()) (rmult (rational_of_term arg1) (rational_of_term arg2)))  
+                     )
+                       (*try
                        begin
-                       let a = rational_of_term arg1 in
+                       (*let a = rational_of_term arg1 in
+                       debug("ho fatto rational of term di "^CicPp.ppterm arg1^
+                        " e ho ottenuto "^string_of_int a.num^"/"^string_of_int a.den^"\n");*)
+                       let a = flin_of_term arg1  
                        try 
                                begin
                                let b = (rational_of_term arg2) in
+                               debug("ho fatto rational of term di "^CicPp.ppterm arg2^
+                                " e ho ottenuto "^string_of_int b.num^"/"^string_of_int b.den^"\n");
                                (flin_add_cste (flin_zero()) (rmult a b))
                                end
                        with 
-                               _ -> (flin_add (flin_zero()) arg2 a)
+                               _ -> debug ("ho fallito2 su "^CicPp.ppterm arg2^"\n");
+                                    (flin_add (flin_zero()) arg2 a)
                        end
                with 
-                       _-> (flin_add(flin_zero()) arg1 (rational_of_term arg2))
+                       _-> debug ("ho fallito1 su "^CicPp.ppterm arg1^"\n");
+                           (flin_add(flin_zero()) arg1 (rational_of_term arg2))
+                           *)
                end
            |"cic:/Coq/Reals/Rdefinitions/Rinv.con"->
               let a=(rational_of_term (List.hd next)) in
@@ -316,7 +369,7 @@ let rec flin_of_term t =
         |_-> assert false
        end
   |_-> assert false)
-  with _ -> flin_add (flin_zero()) t r1
+  with _ -> debug("eccezione = "^CicPp.ppterm t^"\n");flin_add (flin_zero()) t r1
 ;;
 
 (* coq wrapper
@@ -454,7 +507,10 @@ let fourier_lineq lineq1 =
                Hashtbl.iter (fun x c ->
                                 try (Hashtbl.find hvar x;())
                                 with _-> nvar:=(!nvar)+1;
-                                         Hashtbl.add hvar x (!nvar))
+                                         Hashtbl.add hvar x (!nvar);
+                                         debug("aggiungo una var "^
+                                          string_of_int !nvar^" per "^
+                                           CicPp.ppterm x^"\n"))
                             f.hflin.fhom)
              lineq1;
    (*print_hash hvar;*)