- idtac used for debugging removed

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

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index 5fa37103070316b30b6d96e8980137335bf5e7f8..1de87fdd99c4d6eb53c4185524192c8acd09839e 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -483,6 +483,7 @@ let rec rational_to_fraction x= (x.num,x.den)
 let rec int_to_real_aux n =
   match n with
     0 -> _R0 (* o forse R0 + R0 ????? *)
+  | 1 -> _R1
   | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
 ;;     
        
@@ -541,7 +542,7 @@ let tac_zero_inf_pos (n,d) ~status =
 
 
 
-debug("\nTAC ZERO INF POS\n");
+debug("TAC ZERO INF POS\n");
 
 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) 
   ~continuations:[
@@ -632,8 +633,13 @@ let my_cut ~term:c ~status:(proof,goal)=
 
 let exact = PrimitiveTactics.exact_tac;;
 
-let tac_use h ~status = 
+let tac_use h ~status:(proof,goal as status) = 
 debug("Inizio TC_USE\n");
+let curi,metasenv,pbo,pty = proof in
+let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+debug ("hname = "^ CicPp.ppterm h.hname ^"\n"); 
+debug ("ty = "^ CicPp.ppterm ty^"\n"); 
+
 let res = 
 match h.htype with
   "Rlt" -> exact ~term:h.hname ~status
@@ -648,7 +654,7 @@ match h.htype with
       ~continuation:(exact ~term:h.hname)) ~status
   |_->assert false
 in
-debug("Fine TAC_USE");
+debug("Fine TAC_USE\n");
 res
 ;;
 
@@ -885,12 +891,25 @@ let rec fourier ~status:(s_proof,s_goal)=
           (* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *)
        
           debug "inizio a costruire tac1\n";
+         Fourier.print_rational(c1);
          
           let tac1=ref ( fun ~status -> 
-                       debug "Sotto tattica t1\n";
+                       debug ("Sotto tattica t1 "^(if h1.hstrict then "strict" else "lasc")^"\n");
                        if h1.hstrict then 
-                           (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_lt)
-                                             ~continuations:[tac_use h1;tac_zero_inf_pos (rational_to_fraction c1)] ~status)
+                           (Tacticals.thens ~start:(
+                           fun ~status -> 
+                           debug ("inizio t1 strict\n");
+                           let curi,metasenv,pbo,pty = proof in
+                           let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+                           debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n"); 
+                           debug ("ty = "^ CicPp.ppterm ty^"\n"); 
+     
+                           PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status)
+                                             ~continuations:[tac_use h1;
+                                            
+                                            tac_zero_inf_pos (rational_to_fraction c1)] ~status
+                                            
+                                            )
                          else 
                            (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
                                              ~continuations:[tac_use h1;tac_zero_inf_pos                                                 (rational_to_fraction c1)] ~status))
@@ -903,18 +922,31 @@ let rec fourier ~status:(s_proof,s_goal)=
                    (if h.hstrict then 
                        (debug("tac1 1\n");
                        tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac 
-                                                      ~term:_Rfourier_lt_lt)
+                                                       ~term:_Rfourier_lt_lt)
                                               ~continuations:[!tac1;tac_use h;
                                                       tac_zero_inf_pos   
                                                       (rational_to_fraction c)]))
                    else 
                    (
                        debug("tac1 2\n");
-                       tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac 
-                                                      ~term:_Rfourier_lt_le)
+                       Fourier.print_rational(c1);
+                       tac1:=(Tacticals.thens ~start:(
+                                       fun ~status -> 
+                                       debug("INIZIO TAC 1 2\n");
+                                       
+                                       let curi,metasenv,pbo,pty = proof in
+                                       let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+                                       debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n"); 
+                                       debug ("ty = "^ CicPp.ppterm ty^"\n"); 
+     
+                                       PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status
+                                                      
+                                                      )
                                               ~continuations:[!tac1;tac_use h; 
-                                                      tac_zero_inf_pos  
-                                                       (rational_to_fraction c)]))
+                                                      
+                                                      tac_zero_inf_pos (rational_to_fraction c)
+                                                      
+                                                      ]))
                     )
                else 
                    (if h.hstrict then