X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FfourierR.ml;h=f5cc890aa9d03873d3d7590f0777df32bd9fb1ec;hb=a6fc115fd7d4cfba94a43f001f4c27322d3db1a8;hp=7a003dd7b197bad62259d3dd33ff61810c2ca5aa;hpb=d651bf2e3d560e194fbe948dd950dd600a40eab6;p=helm.git diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml index 7a003dd7b..f5cc890aa 100644 --- a/helm/ocaml/tactics/fourierR.ml +++ b/helm/ocaml/tactics/fourierR.ml @@ -569,9 +569,9 @@ let rational_to_real x = (* preuve que 0 pall "n0" ~status _Rlt_zero_1 ; - PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in + (fun status -> pall "n0" status _Rlt_zero_1 ; + PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 status ) in let tacd=ref - (fun ~status -> pall "d0" ~status _Rlt_zero_1 ; - PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in + (fun status -> pall "d0" status _Rlt_zero_1 ; + PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 status ) in for i=1 to n-1 do - tacn:=(Tacticals.then_ ~start:(fun ~status -> pall ("n"^string_of_int i) - ~status _Rlt_zero_pos_plus1; - PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status) + tacn:=(Tacticals.then_ ~start:(fun status -> pall ("n"^string_of_int i) + status _Rlt_zero_pos_plus1; + PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 status) ~continuation:!tacn); done; for i=1 to d-1 do - tacd:=(Tacticals.then_ ~start:(fun ~status -> pall "d" - ~status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac - ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacd); + tacd:=(Tacticals.then_ ~start:(fun status -> pall "d" + status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac + ~term:_Rlt_zero_pos_plus1 status) ~continuation:!tacd); done; @@ -606,7 +606,7 @@ debug("TAC ZERO INF POS\n"); ~continuations:[ !tacn ; !tacd ] - ~status) + status) ;; @@ -614,7 +614,7 @@ debug("TAC ZERO INF POS\n"); (* preuve que 0<=n*1/d *) -let tac_zero_infeq_pos gl (n,d) ~status = +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 @@ -635,7 +635,7 @@ let tac_zero_infeq_pos gl (n,d) ~status = done; let r = (Tacticals.thens ~start:(PrimitiveTactics.apply_tac - ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd]) ~status in + ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd]) status in debug("fine tac_zero_infeq_pos\n"); r ;; @@ -645,24 +645,25 @@ let tac_zero_infeq_pos gl (n,d) ~status = (* preuve que 0<(-n)*(1/d) => False *) -let tac_zero_inf_false gl (n,d) ~status= +let tac_zero_inf_false gl (n,d) status= debug("inizio tac_zero_inf_false\n"); if n=0 then - (debug "1\n";let r =(PrimitiveTactics.apply_tac ~term:_Rnot_lt0 ~status) in + (debug "1\n";let r =(PrimitiveTactics.apply_tac ~term:_Rnot_lt0 status) in debug("fine\n"); r) else (debug "2\n";let r = (Tacticals.then_ ~start:( - fun ~status:(proof,goal as status) -> + fun status -> + let (proof, goal) = status in let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in debug("!!!!!!!!!1: unify "^CicPp.ppterm _Rle_not_lt^" with " ^ CicPp.ppterm ty ^"\n"); - let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt ~status in + let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt status in debug("!!!!!!!!!2\n"); r ) - ~continuation:(tac_zero_infeq_pos gl (-n,d))) ~status in + ~continuation:(tac_zero_infeq_pos gl (-n,d))) status in debug("fine\n"); r ) @@ -671,7 +672,8 @@ let tac_zero_inf_false gl (n,d) ~status= (* preuve que 0<=n*(1/d) => False ; n est negatif *) -let tac_zero_infeq_false gl (n,d) ~status:(proof,goal as status)= +let tac_zero_infeq_false gl (n,d) status= +let (proof, goal) = status in debug("stat tac_zero_infeq_false\n"); let r = let curi,metasenv,pbo,pty = proof in @@ -700,18 +702,18 @@ let r = ) ~continuation: (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le) - ~continuation:(tac_zero_inf_pos (-n,d))) ~status in + ~continuation:(tac_zero_inf_pos (-n,d))) status in debug("end tac_zero_infeq_false\n"); r (*PORTING - Tacticals.id_tac ~status + Tacticals.id_tac status *) ;; (* *********** ********** ******** ??????????????? *********** **************) -let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) = +let apply_type_tac ~cast:t ~applist:al (proof,goal) = let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in @@ -723,7 +725,7 @@ let apply_type_tac ~cast:t ~applist: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) + (proof',goal) in proof'',fresh_meta::goals ;; @@ -732,7 +734,7 @@ let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) = -let my_cut ~term:c ~status:(proof,goal)= +let my_cut ~term:c (proof,goal)= let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in @@ -747,7 +749,7 @@ debug("my_cut di "^CicPp.ppterm c^"\n"); let proof'',goals = apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c, CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)] - ~status:(proof',goal) + (proof',goal) in (* We permute the generated goals to be consistent with Coq *) match goals with @@ -758,7 +760,8 @@ debug("my_cut di "^CicPp.ppterm c^"\n"); let exact = PrimitiveTactics.exact_tac;; -let tac_use h ~status:(proof,goal as status) = +let tac_use h status = +let (proof, goal) = status in debug("Inizio TC_USE\n"); let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in @@ -767,20 +770,20 @@ debug ("ty = "^ CicPp.ppterm ty^"\n"); let res = match h.htype with - "Rlt" -> exact ~term:h.hname ~status - |"Rle" -> exact ~term:h.hname ~status + "Rlt" -> exact ~term:h.hname status + |"Rle" -> exact ~term:h.hname status |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_gt_to_lt) - ~continuation:(exact ~term:h.hname)) ~status + ~continuation:(exact ~term:h.hname)) status |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_ge_to_le) - ~continuation:(exact ~term:h.hname)) ~status + ~continuation:(exact ~term:h.hname)) status |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqLR_to_le) - ~continuation:(exact ~term:h.hname)) ~status + ~continuation:(exact ~term:h.hname)) status |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqRL_to_le) - ~continuation:(exact ~term:h.hname)) ~status + ~continuation:(exact ~term:h.hname)) status |_->assert false in debug("Fine TAC_USE\n"); @@ -870,7 +873,7 @@ let rec superlift c n= ;; -let equality_replace a b ~status = +let equality_replace a b status = debug("inizio EQ\n"); let module C = Cic in let proof,goal = status in @@ -884,7 +887,7 @@ debug("inizio EQ\n"); debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl))); let (proof,goals) = EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl)) - ~status:((curi,metasenv',pbo,pty),goal) + ((curi,metasenv',pbo,pty),goal) in let new_goals = fresh_meta::goals in debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = " @@ -892,14 +895,14 @@ debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = " (proof,new_goals) ;; -let tcl_fail a ~status:(proof,goal) = +let tcl_fail a (proof,goal) = match a with 1 -> raise (ProofEngineTypes.Fail "fail-tactical") |_-> (proof,[goal]) ;; (* Galla: moved in variousTactics.ml -let assumption_tac ~status:(proof,goal)= +let assumption_tac (proof,goal)= let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let num = ref 0 in @@ -911,25 +914,25 @@ let assumption_tac ~status:(proof,goal)= ) context in - Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal) + Tacticals.try_tactics ~tactics:tac_list (proof,goal) ;; *) (* Galla: moved in negationTactics.ml (* !!!!! fix !!!!!!!!!! *) -let contradiction_tac ~status:(proof,goal)= +let contradiction_tac (proof,goal)= Tacticals.then_ (*inutile sia questo che quello prima della chiamata*) ~start:PrimitiveTactics.intros_tac ~continuation:(Tacticals.then_ ~start:(VariousTactics.elim_type_tac ~term:_False) ~continuation:(assumption_tac)) - ~status:(proof,goal) + (proof,goal) ;; *) (* ********************* TATTICA ******************************** *) -let rec fourier ~status:(s_proof,s_goal)= +let rec fourier (s_proof,s_goal)= let s_curi,s_metasenv,s_pbo,s_pty = s_proof in let s_metano,s_context,s_ty = CicUtil.lookup_meta s_goal s_metasenv in debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n"); @@ -962,7 +965,7 @@ theoreme,so let's parse our thesis *) Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl) ~continuation:(PrimitiveTactics.intros_tac ()) - ~status:(s_proof,s_goal) in + (s_proof,s_goal) in let goal = if List.length gl = 1 then List.hd gl else failwith "a new goal" in @@ -1054,26 +1057,26 @@ theoreme,so let's parse our thesis *) debug "inizio a costruire tac1\n"; Fourier.print_rational(c1); - let tac1=ref ( fun ~status -> + let tac1=ref ( fun status -> if h1.hstrict then (Tacticals.thens ~start:( - fun ~status -> + fun status -> debug ("inizio t1 strict\n"); let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n"); debug ("ty = "^ CicPp.ppterm ty^"\n"); - PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status) + PrimitiveTactics.apply_tac ~term:_Rfourier_lt status) ~continuations:[tac_use h1;tac_zero_inf_pos (rational_to_fraction c1)] - ~status + status ) else (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le) ~continuations:[tac_use h1;tac_zero_inf_pos - (rational_to_fraction c1)] ~status + (rational_to_fraction c1)] status ) ) @@ -1094,13 +1097,13 @@ theoreme,so let's parse our thesis *) Fourier.print_rational(c1); tac1:=(Tacticals.thens ~start:( - fun ~status -> + fun status -> debug("INIZIO TAC 1 2\n"); let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta 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) + PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le status) ~continuations:[!tac1;tac_use h;tac_zero_inf_pos (rational_to_fraction c)]) ) @@ -1133,37 +1136,38 @@ theoreme,so let's parse our thesis *) tac:=(Tacticals.thens ~start:(my_cut ~term:ineq) ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)(**)Tacticals.then_ - ~start:(fun ~status:(proof,goal as status) -> + ~start:(fun status -> + let (proof, goal) = status in let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in PrimitiveTactics.change_tac ~what:ty - ~with_what:(Cic.Appl [ _not; ineq]) ~status) + ~with_what:(Cic.Appl [ _not; ineq]) status) ~continuation:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term: (if sres then _Rnot_lt_lt else _Rnot_le_le)) ~continuation:(Tacticals.thens ~start:( - fun ~status -> + 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 + status in (match r with (p,gl) -> debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" )); r) ~continuations:[(Tacticals.thens ~start:( - fun ~status -> - let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in + fun status -> + let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 status in (match r with (p,gl) -> debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" )); r) ~continuations: [PrimitiveTactics.apply_tac ~term:_Rinv_R1 ;Tacticals.try_tactics - ~tactics:[ "ring", (fun ~status -> + ~tactics:[ "ring", (fun status -> debug("begin RING\n"); - let r = Ring.ring_tac ~status in + let r = Ring.ring_tac status in debug ("end RING\n"); r) ; "id", Tacticals.id_tac] @@ -1172,7 +1176,8 @@ theoreme,so let's parse our thesis *) Tacticals.then_ ~start: ( - fun ~status:(proof,goal as status) -> + fun status -> + let (proof, goal) = status in let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in (* check if ty is of type *) @@ -1182,7 +1187,7 @@ theoreme,so let's parse our thesis *) Cic.Prod (Cic.Anonymous,a,b) -> (Cic.Appl [_not;a]) |_ -> assert false) in - let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 ~status in + let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 status in debug("fine MY_CHNGE\n"); r @@ -1194,12 +1199,12 @@ theoreme,so let's parse our thesis *) |_-> assert false); (*match res*) debug ("finalmente applico tac\n"); ( - let r = !tac ~status:(proof,goal) in + let r = !tac (proof,goal) in debug("\n\n]]]]]]]]]]]]]]]]]) That's all folks ([[[[[[[[[[[[[[[[[[[\n\n");r ) ;; -let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);; +let fourier_tac (proof,goal) = fourier (proof,goal);;