From 7607dbbaf3c411a62300da0594c8b078bca091c5 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 11 Oct 2002 09:38:46 +0000
Subject: [PATCH] More debug printings. Replacing the wrong tac with id_tac it
 goes straight to the end, lefting 1 more goals open: 0 < (1+0)/(1+0)

Remember that the tactic fails applying
0<1 to 0<1+0
---
 helm/gTopLevel/fourierR.ml | 57 ++++++++++++++++++++++++++++++--------
 1 file changed, 46 insertions(+), 11 deletions(-)

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index 5fa371030..0998a37d0 100644
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -541,7 +541,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 +632,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 +653,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 +890,27 @@ 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;
+					     
+						Ring.id_tac] ~status
+					     
+					     (*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 +923,33 @@ 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)]))
+					               
+						       Ring.id_tac
+						       (*tac_zero_inf_pos  
+                                                       (rational_to_fraction c)*)
+						       
+						       ]))
                     )
 	        else 
 		    (if h.hstrict then 
-- 
2.39.2