X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FfourierR.ml;h=17ff3f8fe732a37a923a6a3b2a91346ba7f98ccc;hb=850b1a2e1b00104239484ac25aef29c0b943e1e5;hp=66e895119daf37b7239ef88b48f46dad0d9ad6da;hpb=989a5444a5162ba9259858a25a1dadab300291a3;p=helm.git diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index 66e895119..17ff3f8fe 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -394,7 +394,7 @@ let ineq1_of_term (h,t) = |_->assert false)(* match u *) | Cic.MutInd (u,i,o) -> (match UriManager.string_of_uri u with - "cic:/Coq/Init/Logic_Type/eqT.con" -> + "cic:/Coq/Init/Logic_Type/eqT.ind" -> let t0= arg1 in let arg1= arg2 in let arg2= List.hd(List.tl (List.tl next)) in @@ -531,8 +531,8 @@ let _Rle_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") [] ;; let _Rle_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") [] ;; -let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") [] ;; +(*let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") [] ;;*) let _Rlt = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rlt.con") [] ;; let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string @@ -647,11 +647,11 @@ let tac_zero_infeq_pos gl (n,d) ~status = (*let cste = pf_parse_constr gl in*) debug("inizio tac_zero_infeq_pos\n"); let tacn = ref - (if n=0 then + (*(if n=0 then (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero ) - else + else*) (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 ) - ) + (* ) *) in let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in for i=1 to n-1 do @@ -748,8 +748,10 @@ let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) = let metasenv' = (fresh_meta,context,t)::metasenv in let proof' = curi,metasenv',pbo,pty in let proof'',goals = - PrimitiveTactics.apply_tac ~term:(Cic.Appl ((Cic.Cast (Cic.Meta - (fresh_meta,irl),t))::al)) ~status:(proof',goal) + PrimitiveTactics.apply_tac + (*~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) (* ??? *)*) + ~term:(Cic.Appl ((Cic.Meta (fresh_meta,irl))::al)) (* ??? *) + ~status:(proof',goal) in proof'',fresh_meta::goals ;; @@ -762,6 +764,9 @@ let my_cut ~term:c ~status:(proof,goal)= let curi,metasenv,pbo,pty = proof in let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in +debug("my_cut di "^CicPp.ppterm c^"\n"); + + let fresh_meta = ProofEngineHelpers.new_meta proof in let irl = ProofEngineHelpers.identity_relocation_list_for_metavariable context in @@ -923,7 +928,7 @@ let assumption_tac ~status:(proof,goal)= (* !!!!! fix !!!!!!!!!! *) let contradiction_tac ~status:(proof,goal)= Tacticals.then_ - ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) + ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima della chiamata*) ~continuation:(Tacticals.then_ ~start:(Ring.elim_type_tac ~term:_False) ~continuation:(assumption_tac)) @@ -1138,7 +1143,7 @@ theoreme,so let's parse our thesis *) in tac:=(Tacticals.thens ~start:(my_cut ~term:ineq) - ~continuations:[Tacticals.then_ + ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)(**)Tacticals.then_ ~start:(fun ~status:(proof,goal as status) -> let curi,metasenv,pbo,pty = proof in let metano,context,ty = List.find (function (m,_,_) -> m=goal) @@ -1151,6 +1156,7 @@ theoreme,so let's parse our thesis *) ~continuation:(Tacticals.thens ~start:( fun ~status -> + debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n"); let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc ~status in @@ -1166,25 +1172,6 @@ theoreme,so let's parse our thesis *) r) ~continuations: [PrimitiveTactics.apply_tac ~term:_Rinv_R1 -(* CSC: Il nostro goal e' 1^-1 = 1 e non 1 = 1^-1. Quindi non c'e' bisogno - di applicare sym_eqT. Perche' in Coq il goal e' al contrario? Forse i - parametri della equality_replace vengono passati al contrario? Oppure la - tattica usa i parametri al contrario? - CODICE NEL COMMENTO NON PORTATO. ORA ESISTE ANCHE LA TATTICA symmetry_tac - ~continuations:[Tacticals.then_ - ~start:( - fun ~status:(proof,goal as status) -> - debug("ECCOCI\n"); - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m= - goal) metasenv in - debug("ty = "^CicPp.ppterm ty^"\n"); - let r = PrimitiveTactics.apply_tac ~term:_sym_eqT - ~status in - debug("fine ECCOCI\n"); - r) - ~continuation:(PrimitiveTactics.apply_tac ~term:_Rinv_R1) -*) ;Tacticals.try_tactics ~tactics:[ "ring", (fun ~status -> debug("begin RING\n"); @@ -1193,7 +1180,8 @@ theoreme,so let's parse our thesis *) r) ; "id", Tacticals.id_tac] ]) - ;Tacticals.then_ + ;(*Tacticals.id_tac*) + Tacticals.then_ ~start: ( fun ~status:(proof,goal as status) -> @@ -1211,21 +1199,27 @@ theoreme,so let's parse our thesis *) let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 ~status in debug("fine MY_CHNGE\n"); r + ) ~continuation:(*PORTINGTacticals.id_tac*)tac2])) ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*) - tac:=(Tacticals.thens + (*tac:=(Tacticals.thens ~start:(PrimitiveTactics.cut_tac ~term:_False) ~continuations:[Tacticals.then_ ~start:(PrimitiveTactics.intros_tac ~name:"??") ~continuation:contradiction_tac - ;!tac]) + ;!tac]) FIXED - this was useless*) + (* tac:=!tac*) |_-> assert false)(*match (!lutil) *) |_-> assert false); (*match res*) debug ("finalmente applico tac\n"); - (!tac ~status:(proof,goal)) + ( + let r = !tac ~status:(proof,goal) in + debug("\n\n]]]]]]]]]]]]]]]]]) That's all folks ([[[[[[[[[[[[[[[[[[[\n\n");r + + ) ;; let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;