*)
open Fourier
+open ProofEngineTypes
let debug x = print_string ("____ "^x) ; flush stdout;;
(* preuve que 0<n*1/d
*)
-let tac_zero_inf_pos (n,d) ~status =
+let tac_zero_inf_pos (n,d) =
+ let tac_zero_inf_pos (n,d) status =
(*let cste = pf_parse_constr gl in*)
- let pall str ~status:(proof,goal) t =
+ let pall str (proof,goal) t =
debug ("tac "^str^" :\n" );
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
debug ("th = "^ CicPp.ppterm t ^"\n");
debug ("ty = "^ CicPp.ppterm ty^"\n");
in
- let tacn=ref
- (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
+ 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))
;;
(* 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))
;;
(* 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:(proof,goal as 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:(proof,goal as status)=
-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 ~status:(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
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)) (* ??? *)
- ~status:(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 ~status:(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)]
- ~status:(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:(proof,goal as status) =
-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) ->
[(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))
- ~status:((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)
+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
+ mk_tactic (equality_replace a b)
;;
-let tcl_fail a ~status:(proof,goal) =
- match a with
- 1 -> raise (ProofEngineTypes.Fail "fail-tactical")
- |_-> (proof,[goal])
+let tcl_fail a (proof,goal) =
+ match a with
+ 1 -> raise (ProofEngineTypes.Fail (lazy "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
)
context
in
- Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
+ Tacticals.first ~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");
+ 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
(* 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 ())
- ~status:(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
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 ) *)
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");
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;
(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
in
tac:=(Tacticals.thens
~start:(my_cut ~term:ineq)
- ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)(**)Tacticals.then_
- ~start:(fun ~status:(proof,goal as 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
- ~status
+ ~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:(proof,goal as 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
(* check if ty is of type *)
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:=*)
|_-> assert false); (*match res*)
debug ("finalmente applico tac\n");
(
- let r = !tac ~status:(proof,goal) in
+ let r = apply_tactic !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 = mk_tactic fourier
projects / helm.git / blobdiff