delta reduced, ...
open HelmLibraryObjects
-let rec injection_tac ~term ~status:((proof, goal) as status) =
+let rec injection_tac ~term status =
+ let (proof, goal) = status in
let module C = Cic in
let module U = UriManager in
let module P = PrimitiveTactics in
| _ -> raise (ProofEngineTypes.Fail "Injection: not a projectable equality")
)
| _ -> raise (ProofEngineTypes.Fail "Injection: not an equation")
- ) ~status
+ ) status
-and injection1_tac ~term ~i ~status:((proof, goal) as status) =
+and injection1_tac ~term ~i status =
+let (proof, goal) = status in
(* precondizione: t1 e t2 hanno in testa lo stesso costruttore ma differiscono (o potrebbero differire?) nell'i-esimo parametro del costruttore *)
let module C = Cic in
let module S = CicSubstitution in
;
T.then_
~start:
- (fun ~status:((proof,goal) as status) ->
+ (fun status ->
+ let (proof, goal) = status in
let _,metasenv,_,_ = proof in
let _,context,gty = CicUtil.lookup_meta goal metasenv in
prerr_endline ("XXXX goal " ^ string_of_int goal) ;
);
t1]
)
- ~status
+ status
)
~continuation:
(T.then_
~continuation:EqualityTactics.reflexivity_tac
)
]
- ~status
+ status
| _ -> raise (ProofEngineTypes.Fail "Discriminate: not a discriminable equality")
)
| _ -> raise (ProofEngineTypes.Fail "Discriminate: not an equality")
(* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori
diversi *)
-let discriminate'_tac ~term ~status:((proof, goal) as status) =
+let discriminate'_tac ~term status =
+ let (proof, goal) = status in
let module C = Cic in
let module U = UriManager in
let module P = PrimitiveTactics in
let (proof',goals') =
EliminationTactics.elim_type_tac
~term:(C.MutInd(Logic.false_URI,0,[]))
- ~status
+ status
in
(match goals' with
[goal'] ->
~start:(EqualityTactics.rewrite_back_simpl_tac ~term)
~continuation:(IntroductionTactics.constructor_tac ~n:1)
)
- ~status:(proof',goal')
+ (proof',goal')
| _ -> raise (ProofEngineTypes.Fail "Discriminate: ElimType False left more (or less) than one goal")
)
| _ -> raise (ProofEngineTypes.Fail "Discriminate: not a discriminable equality")
;;
-let discriminate_tac ~term ~status =
+let discriminate_tac ~term status =
Tacticals.then_
~start:(* (injection_tac ~term) *) Tacticals.id_tac
~continuation:(discriminate'_tac ~term) (* NOOO!!! non term ma una (qualunque) delle nuove hyp introdotte da inject *)
- ~status
+ status
;;
-let compare_tac ~term ~status:((proof, goal) as status) = Tacticals.id_tac ~status
+let compare_tac ~term status = Tacticals.id_tac status
(*
(* term is in the form t1=t2; the tactic leaves two goals: in the first you have to *)
(* demonstrate the goal with the additional hyp that t1=t2, in the second the hyp is ~t1=t2 *)
~continuations:[
T.then_ ~start:(P.intros_tac) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ;
decide_equality_tac]
- ~status
+ status
| (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) ->
let term' = (* (t1=t2) \/ ~(t1=t2) *)
C.Appl [
~continuations:[
T.then_ ~start:(P.intros_tac) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ;
decide_equality_tac]
- ~status
+ status
| _ -> raise (ProofEngineTypes.Fail "Compare: Not an equality")
*)
;;
exception TwoDifferentSubtermsFound of (Cic.term * Cic.term * int)
-let discriminate_tac ~term ~status:((proof, goal) as status) =
+let discriminate_tac ~term status =
let module C = Cic in
let module U = UriManager in
let module P = PrimitiveTactics in
let module T = Tacticals in
+ let (proof, goal) = status in
let _,metasenv,_,_ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
let (proof',goals') =
EliminationTactics.elim_type_tac
~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] )
- ~status
+ status
in
(match goals' with
[goal'] ->
~start:(EqualityTactics.rewrite_back_simpl_tac ~term:term)
~continuation:(IntroductionTactics.constructor_tac ~n:1)
)
- ~status:(proof',goal')
+ (proof',goal')
| _ -> raise (ProofEngineTypes.Fail "Discriminate: ElimType False left more (or less) than one goal")
)
| _ -> raise (ProofEngineTypes.Fail "Discriminate: not a discriminable equality")
(*
-let induction_tac ~term ~status:((proof,goal) as status) =
+let induction_tac ~term status =
+ let (proof, goal) = status in
let module C = Cic in
let module R = CicReduction in
let module P = PrimitiveTactics in
~tactic:(T.then_ ~start:(VariousTactics.generalize_tac ~term) (* chissa' se cosi' funziona? *)
~continuation:(P.intros))
~continuation:(P.elim_intros_simpl ~term)
- ~status
+ status
;;
*)
-let elim_type_tac ~term ~status =
+let elim_type_tac ~term status =
let module C = Cic in
let module P = PrimitiveTactics in
let module T = Tacticals in
T.thens
~start: (P.cut_tac term)
~continuations:[ P.elim_intros_simpl_tac ~term:(C.Rel 1) ; T.id_tac ]
- ~status
+ status
;;
;;
*)
-let decompose_tac ?(uris_choice_callback=(function l -> l)) term ~status:((proof,goal) as status) =
+let decompose_tac ?(uris_choice_callback=(function l -> l)) term status =
+ let (proof, goal) = status in
let module C = Cic in
let module R = CicReduction in
let module P = PrimitiveTactics in
(* N.B.: due to a bug in uris_choice_callback exp_named_subst are not significant (they all are []) *)
uris_choice_callback (make_list termty) in
- let rec elim_clear_tac ~term' ~nr_of_hyp_still_to_elim ~status:((proof,goal) as status) =
+ let rec elim_clear_tac ~term' ~nr_of_hyp_still_to_elim status =
+ let (proof, goal) = status in
warn ("nr_of_hyp_still_to_elim=" ^ (string_of_int nr_of_hyp_still_to_elim));
if nr_of_hyp_still_to_elim <> 0 then
let _,metasenv,_,_ = proof in
~start:(P.elim_intros_simpl_tac ~term:term')
~continuation:(
(* clear the hyp that has just been eliminated *)
- (fun ~status:((proof,goal) as status) ->
+ (fun status ->
+ let (proof, goal) = status in
let _,metasenv,_,_ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let new_context_len = List.length context in
then begin prerr_endline ("%%%%%%% no clear"); T.id_tac end
else begin prerr_endline ("%%%%%%% clear " ^ (string_of_int (new_nr_of_hyp_still_to_elim))); (S.clear ~hyp:(List.nth context (new_nr_of_hyp_still_to_elim))) end)
~continuation:(elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim)
- ~status
+ status
))
- ~status
+ status
| _ ->
let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim - 1 in
warn ("fail; hyp=" ^ (string_of_int new_nr_of_hyp_still_to_elim));
- elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim ~status
+ elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim status
else (* no hyp to elim left in this goal *)
- T.id_tac ~status
+ T.id_tac status
in
- elim_clear_tac ~term':term ~nr_of_hyp_still_to_elim:1 ~status
+ elim_clear_tac ~term':term ~nr_of_hyp_still_to_elim:1 status
;;
*)
-let rewrite_tac ~term:equality ~status:(proof,goal) =
+let rewrite_tac ~term:equality (proof,goal) =
let module C = Cic in
let module U = UriManager in
let curi,metasenv,pbo,pty = proof in
PrimitiveTactics.exact_tac
~term:(C.Appl
[eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
- ~status:((curi,metasenv',pbo,pty),goal)
+ ((curi,metasenv',pbo,pty),goal)
in
assert (List.length goals = 0) ;
(proof',[fresh_meta])
;;
-let rewrite_simpl_tac ~term ~status =
+let rewrite_simpl_tac ~term status =
Tacticals.then_
~start:(rewrite_tac ~term)
~continuation:
(ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None)
- ~status
+ status
;;
-let rewrite_back_tac ~term:equality ~status:(proof,goal) =
+let rewrite_back_tac ~term:equality (proof,goal) =
let module C = Cic in
let module U = UriManager in
let curi,metasenv,pbo,pty = proof in
PrimitiveTactics.exact_tac
~term:(C.Appl
[eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
- ~status:((curi,metasenv',pbo,pty),goal)
+ ((curi,metasenv',pbo,pty),goal)
in
assert (List.length goals = 0) ;
(proof',[fresh_meta])
;;
-let rewrite_back_simpl_tac ~term ~status =
+let rewrite_back_simpl_tac ~term status =
Tacticals.then_
~start:(rewrite_back_tac ~term)
~continuation:
(ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None)
- ~status
+ status
;;
-let replace_tac ~what ~with_what ~status:((proof, goal) as status) =
+let replace_tac ~what ~with_what status =
+ let (proof, goal) = status in
let module C = Cic in
let module U = UriManager in
let module P = PrimitiveTactics in
ProofEngineStructuralRules.clear
~hyp:(List.hd context)) ;
T.id_tac]
- ~status
+ status
else raise (ProofEngineTypes.Fail "Replace: terms not replaceable")
with (Failure "hd") -> raise (ProofEngineTypes.Fail "Replace: empty context")
;;
;;
-let symmetry_tac ~status:(proof, goal) =
+let symmetry_tac (proof, goal) =
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
match (R.whd context ty) with
(C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri HelmLibraryObjects.Logic.eq_URI) ->
- PrimitiveTactics.apply_tac ~status:(proof,goal)
+ PrimitiveTactics.apply_tac (proof,goal)
~term: (C.Const (HelmLibraryObjects.Logic.sym_eq_URI, []))
| _ -> raise (ProofEngineTypes.Fail "Symmetry failed")
;;
-let transitivity_tac ~term ~status:((proof, goal) as status) =
+let transitivity_tac ~term status =
+ let (proof, goal) = status in
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
~term: (C.Const (HelmLibraryObjects.Logic.trans_eq_URI, [])))
~continuations:
[PrimitiveTactics.exact_tac ~term ; T.id_tac ; T.id_tac]
- ~status
+ status
| _ -> raise (ProofEngineTypes.Fail "Transitivity failed")
;;
(* 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);;
* http://cs.unibo.it/helm/.
*)
-
-let constructor_tac ~n ~status:(proof, goal) =
+let constructor_tac ~n (proof, goal) =
let module C = Cic in
let module R = CicReduction in
let (_,metasenv,_,_) = proof in
| (C.Appl ((C.MutInd (uri, typeno, exp_named_subst))::_)) ->
PrimitiveTactics.apply_tac
~term: (C.MutConstruct (uri, typeno, n, exp_named_subst))
- ~status:(proof, goal)
+ (proof, goal)
| _ -> raise (ProofEngineTypes.Fail "Constructor: failed")
;;
-
-let exists_tac ~status =
- constructor_tac ~n:1 ~status
-;;
-
-
-let split_tac ~status =
- constructor_tac ~n:1 ~status
-;;
-
-
-let left_tac ~status =
- constructor_tac ~n:1 ~status
-;;
-
-
-let right_tac ~status =
- constructor_tac ~n:2 ~status
-;;
+let exists_tac status = constructor_tac ~n:1 status ;;
+let split_tac status = constructor_tac ~n:1 status ;;
+let left_tac status = constructor_tac ~n:1 status ;;
+let right_tac status = constructor_tac ~n:2 status ;;
*)
-let absurd_tac ~term ~status:((proof,goal) as status) =
+let absurd_tac ~term status =
+ let (proof, goal) = status in
let module C = Cic in
let module U = UriManager in
let module P = PrimitiveTactics in
let _,context,ty = CicUtil.lookup_meta goal metasenv in
if ((CicTypeChecker.type_of_aux' metasenv context term) = (C.Sort C.Prop)) (* ma questo controllo serve?? *)
then P.apply_tac
- ~term:(C.Appl [(C.Const (HelmLibraryObjects.Logic.absurd_URI , [] )) ; term ; ty]) ~status
+ ~term:(C.Appl [(C.Const (HelmLibraryObjects.Logic.absurd_URI , [] )) ; term ; ty]) status
else raise (ProofEngineTypes.Fail "Absurd: Not a Proposition")
;;
-let contradiction_tac ~status =
+let contradiction_tac status =
let module C = Cic in
let module U = UriManager in
let module P = PrimitiveTactics in
~term:
(C.MutInd (HelmLibraryObjects.Logic.false_URI, 0, [])))
~continuation: VariousTactics.assumption_tac)
- ~status
+ status
with
(ProofEngineTypes.Fail "Assumption: No such assumption") -> raise (ProofEngineTypes.Fail "Contradiction: No such assumption")
(* sarebbe piu' elegante se Assumtion sollevasse un'eccezione tutta sua che questa cattura, magari con l'aiuto di try_tactics *)
(* Questa era in fourierR.ml
(* !!!!! fix !!!!!!!!!! *)
-let contradiction_tac ~status:(proof,goal)=
+let contradiction_tac (proof,goal)=
Tacticals.then_
~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima della chiamata*)
~continuation:(Tacticals.then_
~start:(VariousTactics.elim_type_tac ~term:_False)
~continuation:(assumption_tac))
- ~status:(proof,goal)
+ (proof,goal)
;;
*)
new_fresh_meta,newmetasenvfragment,exp_named_subst',exp_named_subst_diff
;;
-let apply_tac ~term ~status:(proof, goal) =
+let apply_tac ~term (proof, goal) =
(* Assumption: The term "term" must be closed in the current context *)
let module T = CicTypeChecker in
let module R = CicReduction in
(* TODO per implementare i tatticali e' necessario che tutte le tattiche
sollevino _solamente_ Fail *)
-let apply_tac ~term ~status =
+let apply_tac ~term status =
try
- apply_tac ~term ~status
+ apply_tac ~term status
(* TODO cacciare anche altre eccezioni? *)
with CicUnification.UnificationFailure _ as e ->
raise (Fail (Printexc.to_string e))
let intros_tac
?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) ()
- ~status:(proof, goal)
+ (proof, goal)
=
let module C = Cic in
let module R = CicReduction in
let cut_tac
?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
- term ~status:(proof, goal)
+ term (proof, goal)
=
let module C = Cic in
let curi,metasenv,pbo,pty = proof in
let letin_tac
?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
- term ~status:(proof, goal)
+ term (proof, goal)
=
let module C = Cic in
let curi,metasenv,pbo,pty = proof in
(newproof, [newmeta])
(** functional part of the "exact" tactic *)
-let exact_tac ~term ~status:(proof, goal) =
+let exact_tac ~term (proof, goal) =
(* Assumption: the term bo must be closed in the current context *)
let (_,metasenv,_,_) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
(* not really "primitive" tactics .... *)
-let elim_tac ~term ~status:(proof, goal) =
+let elim_tac ~term (proof, goal) =
let module T = CicTypeChecker in
let module U = UriManager in
let module R = CicReduction in
(*CSC: while [what] can have a richer context (because of binders) *)
(*CSC: So it is _NOT_ possible to use those binders in the [with_what] term. *)
(*CSC: Is that evident? Is that right? Or should it be changed? *)
-let change_tac ~what ~with_what ~status:(proof, goal) =
+let change_tac ~what ~with_what (proof, goal) =
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
(* are_convertible works only on well-typed terms *)
open ProofEngineTypes
-let clearbody ~hyp ~status:(proof, goal) =
+let clearbody ~hyp (proof, goal) =
let module C = Cic in
match hyp with
None -> assert false
in
(curi,metasenv',pbo,pty), [goal]
-let clear ~hyp:hyp_to_clear ~status:(proof, goal) =
+let clear ~hyp:hyp_to_clear (proof, goal) =
let module C = Cic in
match hyp_to_clear with
None -> assert false
(** current goal, integer index *)
type goal = int
type status = proof * goal
+
(**
a tactic: make a transition from one status to another one or, usually,
raise a "Fail" (@see Fail) exception in case of failure
*)
(** an unfinished proof with the optional current goal *)
-type tactic = status:status -> proof * goal list
+type tactic = status -> proof * goal list
(** tactic failure *)
exception Fail of string
*)
(*
-let reduction_tac ~reduction ~status:(proof,goal) =
+let reduction_tac ~reduction (proof,goal) =
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let new_ty = reduction context ty in
*)
(* The default of term is the thesis of the goal to be prooved *)
-let reduction_tac ~also_in_hypotheses ~reduction ~terms ~status:(proof,goal) =
+let reduction_tac ~also_in_hypotheses ~reduction ~terms (proof,goal) =
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let terms =
let reduce_tac = reduction_tac ~reduction:ProofEngineReduction.reduce ;;
let whd_tac = reduction_tac ~reduction:CicReduction.whd ;;
-let fold_tac ~reduction ~also_in_hypotheses ~term ~status:(proof,goal) =
+let fold_tac ~reduction ~also_in_hypotheses ~term (proof,goal) =
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let term' = reduction context term in
@raise Failure if proof is None
@return current goal's metasenv
*)
-let metasenv_of_status ~status:((_,m,_,_), _) = m
+let metasenv_of_status ((_,m,_,_), _) = m
(**
@param status a proof engine status
@raise Failure when proof or goal are None
@return context corresponding to current goal
*)
-let context_of_status ~status:(proof, goal as status) =
- let metasenv = metasenv_of_status ~status:status in
+let context_of_status status =
+ let (proof, goal) = status in
+ let metasenv = metasenv_of_status status in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
context
@param status current proof engine status
@param term term to cut
*)
-let elim_type_tac ~term ~status =
+let elim_type_tac ~term status =
warn "in Ring.elim_type_tac";
Tacticals.thens ~start:(cut_tac ~term)
- ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] ~status
+ ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] status
*)
(**
@param term term to cut
@param proof term used to prove second subgoal generated by elim_type
*)
-let elim_type2_tac ~term ~proof ~status =
+let elim_type2_tac ~term ~proof status =
let module E = EliminationTactics in
warn "in Ring.elim_type2";
Tacticals.thens ~start:(E.elim_type_tac ~term)
- ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof] ~status
+ ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof] status
(* Galla: spostata in variousTactics.ml
(**
only refl_eqT, coq's one also try "refl_equal"
@param status current proof engine status
*)
-let reflexivity_tac ~status:(proof, goal) =
+let reflexivity_tac (proof, goal) =
warn "in Ring.reflexivity_tac";
let refl_eqt = mkCtor ~uri:refl_eqt_uri ~exp_named_subst:[] in
try
- apply_tac ~status:(proof, goal) ~term:refl_eqt
+ apply_tac (proof, goal) ~term:refl_eqt
with (Fail _) as e ->
let e_str = Printexc.to_string e in
raise (Fail ("Reflexivity failed with exception: " ^ e_str))
@param count number of hypotheses to remove
@param status current proof engine status
*)
-let purge_hyps_tac ~count ~status:(proof, goal as status) =
+let purge_hyps_tac ~count status =
let module S = ProofEngineStructuralRules in
+ let (proof, goal) = status in
let rec aux n context status =
assert(n>=0);
match (n, context) with
| (0, _) -> status
| (n, hd::tl) ->
aux (n-1) tl
- (status_of_single_goal_tactic_result (S.clear ~hyp:hd ~status))
+ (status_of_single_goal_tactic_result (S.clear ~hyp:hd status))
| (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left"
in
let (_, metasenv, _, _) = proof in
Ring tactic, does associative and commutative rewritings in Reals ring
@param status current proof engine status
*)
-let ring_tac ~status:((proof, goal) as status) =
+let ring_tac status =
+ let (proof, goal) = status in
warn "in Ring tactic";
let eqt = mkMutInd (Logic.eq_URI, 0) [] in
let r = Reals.r in
- let metasenv = metasenv_of_status ~status in
+ let metasenv = metasenv_of_status status in
let (metano, context, ty) = CicUtil.lookup_meta goal metasenv in
let (t1, t2) = split_eq ty in (* goal like t1 = t2 *)
match (build_segments ~terms:[t1; t2]) with
try
let new_hyps = ref 0 in (* number of new hypotheses created *)
Tacticals.try_tactics
- ~status
+ status
~tactics:[
"reflexivity", EqualityTactics.reflexivity_tac ;
"exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ;
] ;
t1'_eq_t1''
]) ;
- "elim_type eqt su t1 ...", (fun ~status ->
+ "elim_type eqt su t1 ...", (fun status ->
let status' = (* status after 1st elim_type use *)
- let context = context_of_status ~status in
+ let context = context_of_status status in
if not (are_convertible context t1'' t1) then begin
warn "t1'' and t1 are NOT CONVERTIBLE";
let newstatus =
elim_type2_tac (* 1st elim_type use *)
- ~status ~proof:t1'_eq_t1''
+ status ~proof:t1'_eq_t1''
~term:(Cic.Appl [eqt; r; t1''; t1])
in
incr new_hyps; (* elim_type add an hyp *)
in
let status'' =
Tacticals.try_tactics (* try to solve 1st subgoal *)
- ~status:status'
+ status'
~tactics:[
"exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'';
"exact sym_eqt su t2 ...",
] ;
t2'_eq_t2''
]) ;
- "elim_type eqt su t2 ...", (fun ~status ->
+ "elim_type eqt su t2 ...", (fun status ->
let status' =
- let context = context_of_status ~status in
+ let context = context_of_status status in
if not (are_convertible context t2'' t2) then begin
warn "t2'' and t2 are NOT CONVERTIBLE";
let newstatus =
elim_type2_tac (* 2nd elim_type use *)
- ~status ~proof:t2'_eq_t2''
+ status ~proof:t2'_eq_t2''
~term:(Cic.Appl [eqt; r; t2''; t2])
in
incr new_hyps; (* elim_type add an hyp *)
in
try (* try to solve main goal *)
warn "trying reflexivity ....";
- EqualityTactics.reflexivity_tac ~status:status'
+ EqualityTactics.reflexivity_tac status'
with (Fail _) -> (* leave conclusion to the user *)
warn "reflexivity failed, solution's left as an ex :-)";
- purge_hyps_tac ~count:!new_hyps ~status:status')]
+ purge_hyps_tac ~count:!new_hyps status')]
in
status'')]
with (Fail s) ->
assert false
(* wrap ring_tac catching GoalUnringable and raising Fail *)
-let ring_tac ~status =
+let ring_tac status =
try
- ring_tac ~status
+ ring_tac status
with GoalUnringable ->
raise (Fail "goal unringable")
module G = MQueryGenerator
(* search arguments on which Apply tactic doesn't fail *)
-let matchConclusion mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() ~status =
+let matchConclusion mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() status =
let ((_, metasenv, _, _), metano) = status in
let (_, ey ,ty) = CicUtil.lookup_meta metano metasenv in
let list_of_must, only = CGMatchConclusion.get_constraints metasenv ey ty in
(PrimitiveTactics.apply_tac
~term:(MQueryMisc.term_of_cic_textual_parser_uri
(MQueryMisc.cic_textual_parser_uri_of_string uri))
- ~status);
+ status);
true
with ProofEngineTypes.Fail _ -> false)
then
(*matchConclusion modificata per evitare una doppia apply*)
-let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() ~status =
+let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() status =
let ((_, metasenv, _, _), metano) = status in
let (_, ey ,ty) = CicUtil.lookup_meta metano metasenv in
let list_of_must, only = CGMatchConclusion.get_constraints metasenv ey ty in
((PrimitiveTactics.apply_tac
~term:(MQueryMisc.term_of_cic_textual_parser_uri
(MQueryMisc.cic_textual_parser_uri_of_string uri))
- ~status)::tl')
+ status)::tl')
with ProofEngineTypes.Fail _ -> tl'
in
prerr_endline (string_of_int (List.length uris));
(*function taking a status and returning a new status after having searching a theorem to apply ,theorem which *)
(*generate the less number of subgoals*)
-let searchTheorem ~status:(proof,goal) =
+let searchTheorem (proof,goal) =
let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log] (* default MathQL interpreter options *)
in
let mqi_handle = MQIC.init mqi_flags prerr_string
in
let uris' =
matchConclusion
- mqi_handle ~choose_must() ~status:(proof, goal)
+ mqi_handle ~choose_must() (proof, goal)
in
let list_of_termin =
List.map
let list_proofgoal =
List.map
(function term ->
- PrimitiveTactics.apply_tac ~term ~status:(proof,goal))
+ PrimitiveTactics.apply_tac ~term (proof,goal))
list_of_termin
in
let (list_of_subgoal: int list list) =
(* modifico la str in modo che sia accettata da apply*)
in*)
- PrimitiveTactics.apply_tac ~term:uri' ~status:(proof,goal)
+ PrimitiveTactics.apply_tac ~term:uri' (proof,goal)
;;
*)
-let searchTheorems mqi_handle ~status:(proof,goal) =
+let searchTheorems mqi_handle (proof,goal) =
(*prerr_endline "1";*)
let uris' =
- matchConclusion2 mqi_handle ~choose_must() ~status:(proof, goal) in
+ matchConclusion2 mqi_handle ~choose_must() (proof, goal) in
prerr_endline (string_of_int (List.length uris'));
(*prerr_endline "2";*)
(* let list_of_termin =
let list_proofgoal =
List.map
(function term ->
- PrimitiveTactics.apply_tac ~term ~status:(proof,goal)) list_of_termin in*)
+ PrimitiveTactics.apply_tac ~term (proof,goal)) list_of_termin in*)
(*prerr_endline "4";*)
let res =
List.sort
choose_must:(MQGTypes.r_obj list list ->
MQGTypes.r_obj list ->
MQGTypes.r_obj list) ->
- unit -> status: ProofEngineTypes.status -> string list
+ unit -> ProofEngineTypes.status -> string list
(* TODO: OLD CODE TO BE REMOVED
-val searchTheorem : status: ProofEngineTypes.status -> ProofEngineTypes.proof * ProofEngineTypes.goal list
+val searchTheorem : ProofEngineTypes.status -> ProofEngineTypes.proof * ProofEngineTypes.goal list
*)
-val searchTheorems : MQIConn.handle -> status: ProofEngineTypes.status -> (ProofEngineTypes.proof * ProofEngineTypes.goal list) list
-
+val searchTheorems:
+ MQIConn.handle -> ProofEngineTypes.status ->
+ (ProofEngineTypes.proof * ProofEngineTypes.goal list) list
(* not a tactical, but it's used only here (?) *)
-let id_tac ~status:(proof,goal) =
- (proof,[goal])
+let id_tac (proof,goal) = (proof,[goal])
(**
Galla: is this exactly Coq's "First"?
*)
-let rec try_tactics ~(tactics: (string * tactic) list) ~status =
+let rec try_tactics ~(tactics: (string * tactic) list) status =
warn "in Tacticals.try_tactics";
match tactics with
| (descr, tac)::tactics ->
warn ("Tacticals.try_tactics IS TRYING " ^ descr);
(try
- let res = tac ~status in
+ let res = tac status in
warn ("Tacticals.try_tactics: " ^ descr ^ " succedeed!!!");
res
with
warn (
"Tacticals.try_tactics failed with exn: " ^
Printexc.to_string e);
- try_tactics ~tactics ~status
+ try_tactics ~tactics status
| _ -> raise e (* [e] must not be caught ; let's re-raise it *)
)
| [] -> raise (Fail "try_tactics: no tactics left")
-let thens ~start ~continuations ~status =
- let (proof,new_goals) = start ~status in
+let thens ~start ~continuations status =
+ let (proof,new_goals) = start status in
try
List.fold_left2
(fun (proof,goals) goal tactic ->
- let (proof',new_goals') = tactic ~status:(proof,goal) in
+ let (proof',new_goals') = tactic (proof,goal) in
(proof',goals@new_goals')
) (proof,[]) new_goals continuations
with
-let then_ ~start ~continuation ~status =
- let (proof,new_goals) = start ~status in
+let then_ ~start ~continuation status =
+ let (proof,new_goals) = start status in
List.fold_left
(fun (proof,goals) goal ->
- let (proof',new_goals') = continuation ~status:(proof,goal) in
+ let (proof',new_goals') = continuation (proof,goal) in
(proof',goals@new_goals')
) (proof,[]) new_goals
(* When <tactic> generates more than one goal, you have a tree of
application on the tactic, repeat_tactic works in depth on this tree *)
-let rec repeat_tactic ~tactic ~status =
+let rec repeat_tactic ~tactic status =
warn "in repeat_tactic";
- try let (proof, goallist) = tactic ~status in
+ try let (proof, goallist) = tactic status in
let rec step proof goallist =
match goallist with
[] -> (proof, [])
| head::tail ->
- let (proof', goallist') = repeat_tactic ~tactic ~status:(proof, head) in
+ let (proof', goallist') = repeat_tactic ~tactic (proof, head) in
let (proof'', goallist'') = step proof' tail in
proof'', goallist'@goallist''
in
with
(Fail _) as e ->
warn ("Tacticals.repeat_tactic failed after nth time with exception: " ^ Printexc.to_string e) ;
- id_tac ~status
+ id_tac status
;;
(* This tries to apply tactic n times *)
-let rec do_tactic ~n ~tactic ~status =
+let rec do_tactic ~n ~tactic status =
warn "in do_tactic";
try
let (proof, goallist) =
- if (n>0) then tactic ~status
- else id_tac ~status in
+ if (n>0) then tactic status
+ else id_tac status in
(* else (proof, []) in *)(* perche' non va bene questo? stessa questione di ##### ? *)
let rec step proof goallist =
match goallist with
[] -> (proof, [])
| head::tail ->
- let (proof', goallist') = do_tactic ~n:(n-1) ~tactic ~status:(proof, head) in
+ let (proof', goallist') = do_tactic ~n:(n-1) ~tactic (proof, head) in
let (proof'', goallist'') = step proof' tail in
proof'', goallist'@goallist''
in
with
(Fail _) as e ->
warn ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e) ;
- id_tac ~status
+ id_tac status
;;
(* This applies tactic and catches its possible failure *)
-let rec try_tactic ~tactic ~status =
+let rec try_tactic ~tactic status =
warn "in Tacticals.try_tactic";
try
- tactic ~status
+ tactic status
with
(Fail _) as e ->
warn ( "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e);
- id_tac ~status
+ id_tac status
;;
(* This tries tactics until one of them doesn't _solve_ the goal *)
(* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)
-let rec solve_tactics ~(tactics: (string * tactic) list) ~status =
+let rec solve_tactics ~(tactics: (string * tactic) list) status =
warn "in Tacticals.solve_tactics";
match tactics with
| (descr, currenttactic)::moretactics ->
warn ("Tacticals.solve_tactics is trying " ^ descr);
(try
- let (proof, goallist) = currenttactic ~status in
+ let (proof, goallist) = currenttactic status in
match goallist with
[] -> warn ("Tacticals.solve_tactics: " ^ descr ^ " solved the goal!!!");
(* questo significa che non ci sono piu' goal, o che current_tactic non ne ha aperti di nuovi? (la 2a!) ##### *)
(* nel secondo caso basta per dire che solve_tactics has solved the goal? (si!) *)
(proof, goallist)
| _ -> warn ("Tacticals.solve_tactics: try the next tactic");
- solve_tactics ~tactics:(moretactics) ~status
+ solve_tactics ~tactics:(moretactics) status
with
(Fail _) as e ->
warn ("Tacticals.solve_tactics: current tactic failed with exn: " ^ Printexc.to_string e);
- solve_tactics ~tactics ~status
+ solve_tactics ~tactics status
)
| [] -> raise (Fail "solve_tactics cannot solve the goal");
- id_tac ~status
+ id_tac status
;;
(** tattica di prova per debuggare i tatticali *)
(*
-let thens' ~start ~continuations ~status =
- let (proof,new_goals) = start ~status in
+let thens' ~start ~continuations status =
+ let (proof,new_goals) = start status in
try
List.fold_left2
(fun (proof,goals) goal tactic ->
- let (proof',new_goals') = tactic ~status:(proof,goal) in
+ let (proof',new_goals') = tactic (proof,goal) in
(proof',goals@new_goals')
) (proof,[]) new_goals continuations
with
Invalid_argument _ -> raise (Fail "thens: wrong number of new goals")
let prova_tac =
- let apply_T_tac ~status:((proof,goal) as status) =
+ let apply_T_tac status =
+ let (proof, goal) = status in
let curi,metasenv,pbo,pty = proof in
let metano,context,gty = CicUtil.lookup_meta goal metasenv in
let rel =
find 1 context
in
prerr_endline ("eseguo apply");
- apply_tac ~term:(Cic.Rel rel) ~status
+ apply_tac ~term:(Cic.Rel rel) status
in
(* do_tactic ~n:2 *)
repeat_tactic
* http://cs.unibo.it/helm/.
*)
-let search_theorems_in_context ~status:((proof,goal) as status) =
+let search_theorems_in_context status =
+ let (proof, goal) = status in
let module C = Cic in
let module R = CicReduction in
let module S = CicSubstitution in
| hd::tl ->
let res =
try
- Some (PrimitiveTactics.apply_tac ~status ~term:(C.Rel n))
+ Some (PrimitiveTactics.apply_tac status ~term:(C.Rel n))
with
ProofEngineTypes.Fail _ -> None in
(match res with
else
(* choices is a list of pairs proof and goallist *)
let choices =
- (search_theorems_in_context ~status:(proof,goal))@
- (TacticChaser.searchTheorems mqi_handle ~status:(proof,goal))
+ (search_theorems_in_context (proof,goal))@
+ (TacticChaser.searchTheorems mqi_handle (proof,goal))
in
let rec try_choices = function
[] -> raise NotApplicableTheorem
try_choices tl) in
try_choices choices;;
-let auto_tac mqi_handle ~status:(proof,goal) =
+let auto_tac mqi_handle (proof,goal) =
prerr_endline "Entro in Auto";
try
let proof = auto_tac mqi_handle depth proof goal in
chiedere: find dovrebbe restituire una lista di hyp (?) da passare all'utonto con una
funzione di callback che restituisce la (sola) hyp da applicare *)
-let assumption_tac ~status:((proof,goal) as status) =
+let assumption_tac status =
+ let (proof, goal) = status in
let module C = Cic in
let module R = CicReduction in
let module S = CicSubstitution in
| _ -> find (n+1) tl
)
| [] -> raise (ProofEngineTypes.Fail "Assumption: No such assumption")
- in PrimitiveTactics.apply_tac ~status ~term:(C.Rel (find 1 context))
+ in PrimitiveTactics.apply_tac status ~term:(C.Rel (find 1 context))
;;
(* ANCORA DA DEBUGGARE *)
let generalize_tac
?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
- terms ~status:((proof,goal) as status)
+ terms status
=
+ let (proof, goal) = status in
let module C = Cic in
let module P = PrimitiveTactics in
let module T = Tacticals in
~where:ty)
)))
~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac]
- ~status
+ status
;;
ProofEngineTypes.tactic
val auto_tac :
- MQIConn.handle ->
- status:ProofEngineTypes.status
- -> ProofEngineTypes.proof * ProofEngineTypes.goal list
+ MQIConn.handle -> ProofEngineTypes.status ->
+ ProofEngineTypes.proof * ProofEngineTypes.goal list
+
projects / helm.git / commitdiff