X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FfourierR.ml;h=13dd9f410af6c74b2019842158a4a1b1a96a25c0;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=f5cc890aa9d03873d3d7590f0777df32bd9fb1ec;hpb=a6fc115fd7d4cfba94a43f001f4c27322d3db1a8;p=helm.git diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml index f5cc890aa..13dd9f410 100644 --- a/helm/ocaml/tactics/fourierR.ml +++ b/helm/ocaml/tactics/fourierR.ml @@ -31,6 +31,7 @@ des in *) open Fourier +open ProofEngineTypes let debug x = print_string ("____ "^x) ; flush stdout;; @@ -569,7 +570,8 @@ let rational_to_real x = (* preuve que 0 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 + let tacn=ref (mk_tactic (fun status -> + pall "n0" status _Rlt_zero_1 ; + apply_tactic (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1) status )) in + let tacd=ref (mk_tactic (fun status -> + pall "d0" status _Rlt_zero_1 ; + apply_tactic (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) - ~continuation:!tacn); + tacn:=(Tacticals.then_ + ~start:(mk_tactic (fun status -> + pall ("n"^string_of_int i) status _Rlt_zero_pos_plus1; + apply_tactic + (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:(mk_tactic (fun status -> + pall "d" status _Rlt_zero_pos_plus1 ; + apply_tactic + (PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) status)) + ~continuation:!tacd); done; - - debug("TAC ZERO INF POS\n"); - -(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) - ~continuations:[ - !tacn ; - !tacd ] - status) + apply_tactic + (Tacticals.thens + ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) + ~continuations:[!tacn ;!tacd ] ) + status + in + mk_tactic (tac_zero_inf_pos (n,d)) ;; @@ -614,30 +621,32 @@ debug("TAC ZERO INF POS\n"); (* preuve que 0<=n*1/d *) -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 - (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero ) - 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 - tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac - ~term:_Rle_zero_pos_plus1) ~continuation:!tacn); - done; - for i=1 to d-1 do - tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac - ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); - done; - let r = - (Tacticals.thens ~start:(PrimitiveTactics.apply_tac - ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd]) status in - debug("fine tac_zero_infeq_pos\n"); - r +let tac_zero_infeq_pos gl (n,d) = + 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 + (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero ) + 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 + tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac + ~term:_Rle_zero_pos_plus1) ~continuation:!tacn); + done; + for i=1 to d-1 do + tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac + ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); + done; + apply_tactic + (Tacticals.thens + ~start:(PrimitiveTactics.apply_tac ~term:_Rle_mult_inv_pos) + ~continuations:[!tacn;!tacd]) status + in + mk_tactic (tac_zero_infeq_pos gl (n,d)) ;; @@ -645,75 +654,67 @@ 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= - 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("fine\n"); - r) - else - (debug "2\n";let r = (Tacticals.then_ ~start:( - fun status -> +let tac_zero_inf_false gl (n,d) = + let tac_zero_inf_false gl (n,d) status = + if n=0 then + apply_tactic (PrimitiveTactics.apply_tac ~term:_Rnot_lt0) status + else + apply_tactic (Tacticals.then_ + ~start:( mk_tactic (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 - debug("!!!!!!!!!2\n"); - r - ) - ~continuation:(tac_zero_infeq_pos gl (-n,d))) status in - debug("fine\n"); - r - ) + apply_tactic (PrimitiveTactics.apply_tac ~term:_Rle_not_lt) status)) + ~continuation:(tac_zero_infeq_pos gl (-n,d))) + status + in + mk_tactic (tac_zero_inf_false gl (n,d)) ;; (* preuve que 0<=n*(1/d) => False ; n est negatif *) -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 - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - - debug("faccio fold di " ^ CicPp.ppterm - (Cic.Appl - [_Rle ; _R0 ; - Cic.Appl - [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]] - ] - ) ^ "\n") ; - debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n"); - (*CSC: Patch to undo the over-simplification of RewriteSimpl *) - Tacticals.then_ - ~start: - (ReductionTactics.fold_tac ~reduction:CicReduction.whd - ~also_in_hypotheses:false - ~term: +let tac_zero_infeq_false gl (n,d) = + let tac_zero_infeq_false gl (n,d) status = + let (proof, goal) = status in + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in + + debug("faccio fold di " ^ CicPp.ppterm + (Cic.Appl + [_Rle ; _R0 ; + Cic.Appl + [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]] + ] + ) ^ "\n") ; + debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n"); + (*CSC: Patch to undo the over-simplification of RewriteSimpl *) + apply_tactic + (Tacticals.then_ + ~start: + (ReductionTactics.fold_tac + ~reduction:(const_lazy_reduction CicReduction.whd) + ~pattern:(ProofEngineTypes.conclusion_pattern None) + ~term: + (const_lazy_term (Cic.Appl - [_Rle ; _R0 ; - Cic.Appl - [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]] - ] - ) - ) - ~continuation: - (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le) - ~continuation:(tac_zero_inf_pos (-n,d))) status in - debug("end tac_zero_infeq_false\n"); - r -(*PORTING - Tacticals.id_tac status -*) + [_Rle ; _R0 ; + Cic.Appl + [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]]))) + ~continuation: + (Tacticals.then_ + ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le) + ~continuation:(tac_zero_inf_pos (-n,d)))) + status + in + mk_tactic (tac_zero_infeq_false gl (n,d)) ;; (* *********** ********** ******** ??????????????? *********** **************) -let apply_type_tac ~cast:t ~applist:al (proof,goal) = +let apply_type_tac ~cast:t ~applist:al = + 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 @@ -722,76 +723,73 @@ let apply_type_tac ~cast:t ~applist:al (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)) (* ??? *)*) - ~term:(Cic.Appl ((Cic.Meta (fresh_meta,irl))::al)) (* ??? *) - (proof',goal) + apply_tactic + (PrimitiveTactics.apply_tac + (*~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) *) + ~term:(Cic.Appl ((Cic.Meta (fresh_meta,irl))::al))) (* ??? *) + (proof',goal) in proof'',fresh_meta::goals + in + mk_tactic (apply_type_tac ~cast:t ~applist:al) ;; - - - - -let my_cut ~term:c (proof,goal)= +let my_cut ~term:c = + let my_cut ~term:c (proof,goal) = let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in - -debug("my_cut di "^CicPp.ppterm c^"\n"); - - let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let metasenv' = (fresh_meta,context,c)::metasenv in let proof' = curi,metasenv',pbo,pty in let proof'',goals = - apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c, - CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)] - (proof',goal) + apply_tactic + (apply_type_tac + ~cast:(Cic.Prod(Cic.Name "Anonymous",c,CicSubstitution.lift 1 ty)) + ~applist:[Cic.Meta(fresh_meta,irl)]) + (proof',goal) in (* We permute the generated goals to be consistent with Coq *) match goals with [] -> assert false | he::tl -> proof'',he::fresh_meta::tl + in + mk_tactic (my_cut ~term:c) ;; - let exact = PrimitiveTactics.exact_tac;; -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 -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 - |"Rle" -> exact ~term:h.hname status - |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac - ~term:_Rfourier_gt_to_lt) - ~continuation:(exact ~term:h.hname)) status - |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac - ~term:_Rfourier_ge_to_le) - ~continuation:(exact ~term:h.hname)) status - |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac - ~term:_Rfourier_eqLR_to_le) - ~continuation:(exact ~term:h.hname)) status - |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac - ~term:_Rfourier_eqRL_to_le) - ~continuation:(exact ~term:h.hname)) status - |_->assert false -in -debug("Fine TAC_USE\n"); -res +let tac_use h = + 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 + debug ("hname = "^ CicPp.ppterm h.hname ^"\n"); + debug ("ty = "^ CicPp.ppterm ty^"\n"); + apply_tactic + (match h.htype with + "Rlt" -> exact ~term:h.hname + | "Rle" -> exact ~term:h.hname + | "Rgt" -> (Tacticals.then_ + ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_gt_to_lt) + ~continuation:(exact ~term:h.hname)) + | "Rge" -> (Tacticals.then_ + ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_ge_to_le) + ~continuation:(exact ~term:h.hname)) + | "eqTLR" -> (Tacticals.then_ + ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqLR_to_le) + ~continuation:(exact ~term:h.hname)) + | "eqTRL" -> (Tacticals.then_ + ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqRL_to_le) + ~continuation:(exact ~term:h.hname)) + | _->assert false) + status + in + mk_tactic (tac_use h) ;; - - let is_ineq (h,t) = match t with Cic.Appl ( Cic.Const(u,boh)::next) -> @@ -843,62 +841,67 @@ let rec filter_real_hyp context cont = [(Cic.Rel(n),t)] @ filter_real_hyp next cont) | a::next -> debug(" no\n"); filter_real_hyp next cont ;;*) + let filter_real_hyp context _ = let rec filter_aux context num = match context with - [] -> [] - | Some(Cic.Name(h),Cic.Decl(t))::next -> - ( - (*let n = find_in_context h cont in*) - debug("assegno "^string_of_int num^" a "^h^":"^CicPp.ppterm t^"\n"); - [(Cic.Rel(num),t)] @ filter_aux next (num+1) - ) - | a::next -> filter_aux next (num+1) + [] -> [] + | Some(Cic.Name(h),Cic.Decl(t))::next -> + [(Cic.Rel(num),t)] @ filter_aux next (num+1) + | a::next -> filter_aux next (num+1) in - filter_aux context 1 + filter_aux context 1 ;; (* lifts everithing at the conclusion level *) let rec superlift c n= match c with - [] -> [] - | Some(name,Cic.Decl(a))::next -> [Some(name,Cic.Decl( - CicSubstitution.lift n a))] @ superlift next (n+1) - | Some(name,Cic.Def(a,None))::next -> [Some(name,Cic.Def(( - CicSubstitution.lift n a),None))] @ superlift next (n+1) - | Some(name,Cic.Def(a,Some ty))::next -> [Some(name,Cic.Def(( - CicSubstitution.lift n a),Some (CicSubstitution.lift n ty)))] @ superlift next (n+1) + [] -> [] + | Some(name,Cic.Decl(a))::next -> + [Some(name,Cic.Decl(CicSubstitution.lift n a))]@ superlift next (n+1) + | Some(name,Cic.Def(a,None))::next -> + [Some(name,Cic.Def((CicSubstitution.lift n a),None))]@ superlift next (n+1) + | Some(name,Cic.Def(a,Some ty))::next -> + [Some(name, + Cic.Def((CicSubstitution.lift n a),Some (CicSubstitution.lift n ty))) + ] @ superlift next (n+1) | _::next -> superlift next (n+1) (*?? ??*) ;; -let equality_replace a b status = -debug("inizio EQ\n"); - let module C = Cic in - let proof,goal = status in - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in - let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context in - let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in -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)) +let equality_replace a b = + let equality_replace a b status = + debug("inizio EQ\n"); + let module C = Cic in + let proof,goal = status in + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in + let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in + let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in + debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl))); + let (proof,goals) = apply_tactic + (EqualityTactics.rewrite_simpl_tac + ~direction:`LeftToRight + ~pattern:(ProofEngineTypes.conclusion_pattern None) + (C.Meta (fresh_meta,irl))) ((curi,metasenv',pbo,pty),goal) - in - let new_goals = fresh_meta::goals in -debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = " - ^string_of_int( List.length goals)^"+ meta\n"); - (proof,new_goals) + in + let new_goals = fresh_meta::goals in + debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = " + ^string_of_int( List.length goals)^"+ meta\n"); + (proof,new_goals) + in + mk_tactic (equality_replace a b) ;; let tcl_fail a (proof,goal) = - match a with - 1 -> raise (ProofEngineTypes.Fail "fail-tactical") - |_-> (proof,[goal]) + match a with + 1 -> raise (ProofEngineTypes.Fail (lazy "fail-tactical")) + | _ -> (proof,[goal]) ;; (* Galla: moved in variousTactics.ml @@ -914,7 +917,7 @@ let assumption_tac (proof,goal)= ) context in - Tacticals.try_tactics ~tactics:tac_list (proof,goal) + Tacticals.first ~tactics:tac_list (proof,goal) ;; *) (* Galla: moved in negationTactics.ml @@ -935,13 +938,13 @@ let contradiction_tac (proof,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"); + debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto:\n"); debug_pcontext s_context; let fhyp = String.copy "new_hyp_for_fourier" in -(* here we need to negate the thesis, but to do this we need to apply the right -theoreme,so let's parse our thesis *) +(* here we need to negate the thesis, but to do this we need to apply the + right theoreme,so let's parse our thesis *) let th_to_appl = ref _Rfourier_not_le_gt in (match s_ty with @@ -961,11 +964,12 @@ theoreme,so let's parse our thesis *) (* now let's change our thesis applying the th and put it with hp *) - let proof,gl = - Tacticals.then_ - ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl) - ~continuation:(PrimitiveTactics.intros_tac ()) - (s_proof,s_goal) in + let proof,gl = apply_tactic + (Tacticals.then_ + ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl) + ~continuation:(PrimitiveTactics.intros_tac ())) + (s_proof,s_goal) + in let goal = if List.length gl = 1 then List.hd gl else failwith "a new goal" in @@ -977,7 +981,6 @@ theoreme,so let's parse our thesis *) let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in - (* now we want to convert hp to inequations, but first we must lift everyting to thesis level, so that a variable has the save Rel(n) in each hp ( needed by ineq1_of_term ) *) @@ -997,7 +1000,6 @@ theoreme,so let's parse our thesis *) List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq)) with _-> ()) hyps; - debug ("applico fourier a "^ string_of_int (List.length !lineq)^ " disequazioni\n"); @@ -1057,28 +1059,26 @@ theoreme,so let's parse our thesis *) debug "inizio a costruire tac1\n"; Fourier.print_rational(c1); - let tac1=ref ( fun status -> - if h1.hstrict then + let tac1=ref ( mk_tactic (fun status -> + apply_tactic + (if h1.hstrict then (Tacticals.thens - ~start:( - fun status -> + ~start:(mk_tactic (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) - ~continuations:[tac_use h1;tac_zero_inf_pos - (rational_to_fraction c1)] - status - ) - else + apply_tactic + (PrimitiveTactics.apply_tac ~term:_Rfourier_lt) status)) + ~continuations:[tac_use h1; + tac_zero_inf_pos (rational_to_fraction c1)]) + 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)) in s:=h1.hstrict; @@ -1087,45 +1087,39 @@ theoreme,so let's parse our thesis *) (if h.hstrict then (debug("tac1 1\n"); tac1:=(Tacticals.thens - ~start:(PrimitiveTactics.apply_tac - ~term:_Rfourier_lt_lt) + ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_lt_lt) ~continuations:[!tac1;tac_use h;tac_zero_inf_pos - (rational_to_fraction c)]) - ) - else + (rational_to_fraction c)])) + else (debug("tac1 2\n"); Fourier.print_rational(c1); tac1:=(Tacticals.thens - ~start:( - fun status -> + ~start:(mk_tactic (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) + apply_tactic + (PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le) + status)) ~continuations:[!tac1;tac_use h;tac_zero_inf_pos - (rational_to_fraction c)]) - ) - ) - else + (rational_to_fraction c)]))) + else (if h.hstrict then (debug("tac1 3\n"); tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt) ~continuations:[!tac1;tac_use h;tac_zero_inf_pos - (rational_to_fraction c)]) - ) - else + (rational_to_fraction c)])) + else (debug("tac1 4\n"); tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le) ~continuations:[!tac1;tac_use h;tac_zero_inf_pos - (rational_to_fraction c)]) - ) - ) - ); - s:=(!s)||(h.hstrict)) lutil;(*end List.iter*) + (rational_to_fraction c)])))); + s:=(!s)||(h.hstrict)) (* end fun -> *) + lutil;(*end List.iter*) let tac2 = if sres then @@ -1135,48 +1129,47 @@ theoreme,so let's parse our thesis *) in tac:=(Tacticals.thens ~start:(my_cut ~term:ineq) - ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)(**)Tacticals.then_ - ~start:(fun status -> + ~continuations:[Tacticals.then_ + ~start:( mk_tactic (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) + apply_tactic + (ReductionTactics.change_tac + ~pattern:(ProofEngineTypes.conclusion_pattern (Some ty)) + (const_lazy_term (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 -> - debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n"); - let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc + ~start:(mk_tactic (fun status -> + debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^ + CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n"); + let r = apply_tactic + (equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc) status in (match r with (p,gl) -> debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" )); - r) + r)) ~continuations:[(Tacticals.thens - ~start:( - fun status -> - let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 status in + ~start:(mk_tactic (fun status -> + let r = apply_tactic + (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) + r)) ~continuations: - [PrimitiveTactics.apply_tac ~term:_Rinv_R1 - ;Tacticals.try_tactics - ~tactics:[ "ring", (fun status -> - debug("begin RING\n"); - let r = Ring.ring_tac status in - debug ("end RING\n"); - r) - ; "id", Tacticals.id_tac] - ]) + [PrimitiveTactics.apply_tac ~term:_Rinv_R1; + Tacticals.first + ~tactics:[ "ring",Ring.ring_tac; "id", Tacticals.id_tac] + ]) ;(*Tacticals.id_tac*) Tacticals.then_ - ~start: - ( - fun status -> + ~start:(mk_tactic (fun status -> let (proof, goal) = status in let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in @@ -1187,11 +1180,13 @@ 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 = apply_tactic + (ReductionTactics.change_tac + ~pattern:(ProofEngineTypes.conclusion_pattern (Some ty)) + (const_lazy_term w1)) status + in debug("fine MY_CHNGE\n"); - r - - ) + r)) ~continuation:(*PORTINGTacticals.id_tac*)tac2])) ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*) @@ -1199,12 +1194,12 @@ theoreme,so let's parse our thesis *) |_-> assert false); (*match res*) debug ("finalmente applico tac\n"); ( - let r = !tac (proof,goal) in + let r = apply_tactic !tac (proof,goal) in debug("\n\n]]]]]]]]]]]]]]]]]) That's all folks ([[[[[[[[[[[[[[[[[[[\n\n");r ) ;; -let fourier_tac (proof,goal) = fourier (proof,goal);; +let fourier_tac = mk_tactic fourier