Now "only" constraint are more restrictive.

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

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index d6d5fd34add30ad755bb73963fdb47689a504925..bb1c2febf583893ed8c81fe387908782c39b0d3f 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -25,6 +25,7 @@
 
 
 (******************** OTHER USEFUL TACTICS **********************)
+(* Galla: moved in variousTactics.ml
 
 let rewrite_tac ~term:equality ~status:(proof,goal) =
  let module C = Cic in
@@ -85,6 +86,7 @@ let rewrite_simpl_tac ~term ~status =
    (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None)
   ~status
 ;;
+*)
 
 (******************** THE FOURIER TACTIC ***********************)
 
@@ -146,11 +148,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 +198,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 +257,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 +291,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 +371,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 +509,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;*)
@@ -717,7 +775,8 @@ let r =
      (*CSC: Patch to undo the over-simplification of RewriteSimpl *)
      Tacticals.then_
       ~start:
-        (ReductionTactics.fold_tac ~also_in_hypotheses:false
+        (ReductionTactics.fold_tac ~reduction:CicReduction.whd
+          ~also_in_hypotheses:false
           ~term:
             (Cic.Appl
               [_Rle ; _R0 ;
@@ -910,7 +969,7 @@ debug("inizio EQ\n");
    let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
 debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
    let (proof,goals) =
-    rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))
+    VariousTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))
      ~status:((curi,metasenv',pbo,pty),goal)
    in
    let new_goals = fresh_meta::goals in
@@ -944,9 +1003,10 @@ let assumption_tac ~status:(proof,goal)=
 (* !!!!! fix !!!!!!!!!! *)
 let contradiction_tac ~status:(proof,goal)=
        Tacticals.then_ 
-               ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima  della chiamata*)
+                (*inutile sia questo che quello prima  della chiamata*)
+               ~start:PrimitiveTactics.intros_tac
                ~continuation:(Tacticals.then_ 
-                       ~start:(Ring.elim_type_tac ~term:_False) 
+                       ~start:(VariousTactics.elim_type_tac ~term:_False) 
                        ~continuation:(assumption_tac))
        ~status:(proof,goal) 
 ;;
@@ -984,10 +1044,11 @@ theoreme,so let's parse our thesis *)
 
    (* now let's change our thesis applying the th and put it with hp *) 
 
-   let proof,gl = Tacticals.then_ 
-       ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
-       ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp)
-               ~status:(s_proof,s_goal) in
+   let proof,gl =
+    Tacticals.then_ 
+     ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
+     ~continuation:PrimitiveTactics.intros_tac
+     ~status:(s_proof,s_goal) in
    let goal = if List.length gl = 1 then List.hd gl 
                                     else failwith "a new goal" in