From 7607dbbaf3c411a62300da0594c8b078bca091c5 Mon Sep 17 00:00:00 2001 From: Enrico Tassi 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