(* preuve que 0<n*1/d
*)
-let tac_zero_inf_pos (n,d) ~status =
+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 ("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
+ (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;
~continuations:[
!tacn ;
!tacd ]
- ~status)
+ status)
;;
(* 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
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
;;
(* 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
)
(* 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
)
~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
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
;;
-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
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
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
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");
;;
-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
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) ^" = "
(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
)
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");
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
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
)
)
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)])
)
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]
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 *)
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
|_-> 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);;
projects / helm.git / blobdiff