From a6fc115fd7d4cfba94a43f001f4c27322d3db1a8 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 20 Apr 2004 17:00:07 +0000 Subject: [PATCH] got rid of ~status label so that tactics can now be applied partially, delta reduced, ... --- helm/ocaml/tactics/discriminationTactics.ml | 39 +++--- helm/ocaml/tactics/eliminationTactics.ml | 28 ++-- helm/ocaml/tactics/equalityTactics.ml | 30 ++-- helm/ocaml/tactics/fourierR.ml | 129 +++++++++--------- helm/ocaml/tactics/introductionTactics.ml | 28 +--- helm/ocaml/tactics/negationTactics.ml | 13 +- helm/ocaml/tactics/primitiveTactics.ml | 18 +-- .../tactics/proofEngineStructuralRules.ml | 4 +- helm/ocaml/tactics/proofEngineTypes.ml | 3 +- helm/ocaml/tactics/reductionTactics.ml | 6 +- helm/ocaml/tactics/ring.ml | 53 +++---- helm/ocaml/tactics/tacticChaser.ml | 22 +-- helm/ocaml/tactics/tacticChaser.mli | 9 +- helm/ocaml/tactics/tacticals.ml | 66 ++++----- helm/ocaml/tactics/variousTactics.ml | 21 +-- helm/ocaml/tactics/variousTactics.mli | 6 +- 16 files changed, 242 insertions(+), 233 deletions(-) diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml index 5523c137c..dd2e68d09 100644 --- a/helm/ocaml/tactics/discriminationTactics.ml +++ b/helm/ocaml/tactics/discriminationTactics.ml @@ -25,7 +25,8 @@ 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 @@ -71,10 +72,11 @@ let rec injection_tac ~term ~status:((proof, goal) as status) = | _ -> 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 @@ -147,7 +149,8 @@ prerr_endline ("XXXX cominciamo!") ; ; 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) ; @@ -178,7 +181,7 @@ prerr_endline ("XXXX new t1' " ^ CicPp.ppterm new_t1') ; ); t1] ) - ~status + status ) ~continuation: (T.then_ @@ -186,7 +189,7 @@ prerr_endline ("XXXX new t1' " ^ CicPp.ppterm new_t1') ; ~continuation:EqualityTactics.reflexivity_tac ) ] - ~status + status | _ -> raise (ProofEngineTypes.Fail "Discriminate: not a discriminable equality") ) | _ -> raise (ProofEngineTypes.Fail "Discriminate: not an equality") @@ -199,7 +202,8 @@ exception TwoDifferentSubtermsFound of int (* 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 @@ -284,7 +288,7 @@ prerr_endline ("XXXX nth funzionano ") ; let (proof',goals') = EliminationTactics.elim_type_tac ~term:(C.MutInd(Logic.false_URI,0,[])) - ~status + status in (match goals' with [goal'] -> @@ -326,7 +330,7 @@ prerr_endline ("XXXX rewrite<- " ^ CicPp.ppterm term ^ " : " ^ CicPp.ppterm (Cic ~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") @@ -335,11 +339,11 @@ prerr_endline ("XXXX rewrite<- " ^ CicPp.ppterm term ^ " : " ^ CicPp.ppterm (Cic ;; -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 ;; @@ -352,7 +356,7 @@ e' vera o no e lo risolve *) -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 *) @@ -382,7 +386,7 @@ let compare_tac ~term ~status:((proof, goal) as status) = Tacticals.id_tac ~stat ~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 [ @@ -400,7 +404,7 @@ let compare_tac ~term ~status:((proof, goal) as status) = Tacticals.id_tac ~stat ~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") *) ;; @@ -411,11 +415,12 @@ let compare_tac ~term ~status:((proof, goal) as status) = Tacticals.id_tac ~stat 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 @@ -497,7 +502,7 @@ prerr_endline ("XXXX nth funzionano ") ; 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'] -> @@ -543,7 +548,7 @@ prerr_endline ("XXXX rewrite<- " ^ CicPp.ppterm term ^ " : " ^ CicPp.ppterm (Cic ~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") diff --git a/helm/ocaml/tactics/eliminationTactics.ml b/helm/ocaml/tactics/eliminationTactics.ml index cd401a2ec..29aa1c4f1 100644 --- a/helm/ocaml/tactics/eliminationTactics.ml +++ b/helm/ocaml/tactics/eliminationTactics.ml @@ -36,7 +36,8 @@ let warn s = (* -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 @@ -51,19 +52,19 @@ let induction_tac ~term ~status:((proof,goal) as status) = ~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 ;; @@ -130,7 +131,8 @@ let call_back uris = ;; *) -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 @@ -174,7 +176,8 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term ~status:((proof (* 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 @@ -191,7 +194,8 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term ~status:((proof ~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 @@ -203,18 +207,18 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term ~status:((proof 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 ;; diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index 232911450..0e9f72b0f 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -24,7 +24,7 @@ *) -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 @@ -63,23 +63,23 @@ let rewrite_tac ~term:equality ~status:(proof,goal) = 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 @@ -118,7 +118,7 @@ let rewrite_back_tac ~term:equality ~status:(proof,goal) = 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]) @@ -126,16 +126,17 @@ let rewrite_back_tac ~term:equality ~status:(proof,goal) = ;; -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 @@ -161,7 +162,7 @@ let replace_tac ~what ~with_what ~status:((proof, goal) as status) = 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") ;; @@ -174,7 +175,7 @@ let reflexivity_tac = ;; -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 @@ -182,14 +183,15 @@ let symmetry_tac ~status:(proof, goal) = 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 @@ -203,7 +205,7 @@ let transitivity_tac ~term ~status:((proof, goal) as status) = ~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") ;; diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml index 7a003dd7b..f5cc890aa 100644 --- a/helm/ocaml/tactics/fourierR.ml +++ b/helm/ocaml/tactics/fourierR.ml @@ -569,9 +569,9 @@ let rational_to_real x = (* preuve que 0 pall "n0" ~status _Rlt_zero_1 ; - PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in + (fun status -> pall "n0" status _Rlt_zero_1 ; + PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 status ) in let tacd=ref - (fun ~status -> pall "d0" ~status _Rlt_zero_1 ; - PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in + (fun status -> pall "d0" status _Rlt_zero_1 ; + PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 status ) in for i=1 to n-1 do - tacn:=(Tacticals.then_ ~start:(fun ~status -> pall ("n"^string_of_int i) - ~status _Rlt_zero_pos_plus1; - PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status) + tacn:=(Tacticals.then_ ~start:(fun status -> pall ("n"^string_of_int i) + status _Rlt_zero_pos_plus1; + PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 status) ~continuation:!tacn); done; for i=1 to d-1 do - tacd:=(Tacticals.then_ ~start:(fun ~status -> pall "d" - ~status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac - ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacd); + tacd:=(Tacticals.then_ ~start:(fun status -> pall "d" + status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac + ~term:_Rlt_zero_pos_plus1 status) ~continuation:!tacd); done; @@ -606,7 +606,7 @@ debug("TAC ZERO INF POS\n"); ~continuations:[ !tacn ; !tacd ] - ~status) + status) ;; @@ -614,7 +614,7 @@ debug("TAC ZERO INF POS\n"); (* preuve que 0<=n*1/d *) -let tac_zero_infeq_pos gl (n,d) ~status = +let tac_zero_infeq_pos gl (n,d) status = (*let cste = pf_parse_constr gl in*) debug("inizio tac_zero_infeq_pos\n"); let tacn = ref @@ -635,7 +635,7 @@ let tac_zero_infeq_pos gl (n,d) ~status = done; let r = (Tacticals.thens ~start:(PrimitiveTactics.apply_tac - ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd]) ~status in + ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd]) status in debug("fine tac_zero_infeq_pos\n"); r ;; @@ -645,24 +645,25 @@ let tac_zero_infeq_pos gl (n,d) ~status = (* preuve que 0<(-n)*(1/d) => False *) -let tac_zero_inf_false gl (n,d) ~status= +let tac_zero_inf_false gl (n,d) status= debug("inizio tac_zero_inf_false\n"); if n=0 then - (debug "1\n";let r =(PrimitiveTactics.apply_tac ~term:_Rnot_lt0 ~status) in + (debug "1\n";let r =(PrimitiveTactics.apply_tac ~term:_Rnot_lt0 status) in debug("fine\n"); r) else (debug "2\n";let r = (Tacticals.then_ ~start:( - fun ~status:(proof,goal as status) -> + fun status -> + let (proof, goal) = status in let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in debug("!!!!!!!!!1: unify "^CicPp.ppterm _Rle_not_lt^" with " ^ CicPp.ppterm ty ^"\n"); - let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt ~status in + let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt status in debug("!!!!!!!!!2\n"); r ) - ~continuation:(tac_zero_infeq_pos gl (-n,d))) ~status in + ~continuation:(tac_zero_infeq_pos gl (-n,d))) status in debug("fine\n"); r ) @@ -671,7 +672,8 @@ let tac_zero_inf_false gl (n,d) ~status= (* preuve que 0<=n*(1/d) => False ; n est negatif *) -let tac_zero_infeq_false gl (n,d) ~status:(proof,goal as status)= +let tac_zero_infeq_false gl (n,d) status= +let (proof, goal) = status in debug("stat tac_zero_infeq_false\n"); let r = let curi,metasenv,pbo,pty = proof in @@ -700,18 +702,18 @@ let r = ) ~continuation: (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le) - ~continuation:(tac_zero_inf_pos (-n,d))) ~status in + ~continuation:(tac_zero_inf_pos (-n,d))) status in debug("end tac_zero_infeq_false\n"); r (*PORTING - Tacticals.id_tac ~status + Tacticals.id_tac status *) ;; (* *********** ********** ******** ??????????????? *********** **************) -let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) = +let apply_type_tac ~cast:t ~applist:al (proof,goal) = let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in @@ -723,7 +725,7 @@ let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) = PrimitiveTactics.apply_tac (*~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) (* ??? *)*) ~term:(Cic.Appl ((Cic.Meta (fresh_meta,irl))::al)) (* ??? *) - ~status:(proof',goal) + (proof',goal) in proof'',fresh_meta::goals ;; @@ -732,7 +734,7 @@ let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) = -let my_cut ~term:c ~status:(proof,goal)= +let my_cut ~term:c (proof,goal)= let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in @@ -747,7 +749,7 @@ debug("my_cut di "^CicPp.ppterm c^"\n"); let proof'',goals = apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c, CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)] - ~status:(proof',goal) + (proof',goal) in (* We permute the generated goals to be consistent with Coq *) match goals with @@ -758,7 +760,8 @@ debug("my_cut di "^CicPp.ppterm c^"\n"); let exact = PrimitiveTactics.exact_tac;; -let tac_use h ~status:(proof,goal as status) = +let tac_use h status = +let (proof, goal) = status in debug("Inizio TC_USE\n"); let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in @@ -767,20 +770,20 @@ debug ("ty = "^ CicPp.ppterm ty^"\n"); let res = match h.htype with - "Rlt" -> exact ~term:h.hname ~status - |"Rle" -> exact ~term:h.hname ~status + "Rlt" -> exact ~term:h.hname status + |"Rle" -> exact ~term:h.hname status |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_gt_to_lt) - ~continuation:(exact ~term:h.hname)) ~status + ~continuation:(exact ~term:h.hname)) status |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_ge_to_le) - ~continuation:(exact ~term:h.hname)) ~status + ~continuation:(exact ~term:h.hname)) status |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqLR_to_le) - ~continuation:(exact ~term:h.hname)) ~status + ~continuation:(exact ~term:h.hname)) status |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqRL_to_le) - ~continuation:(exact ~term:h.hname)) ~status + ~continuation:(exact ~term:h.hname)) status |_->assert false in debug("Fine TAC_USE\n"); @@ -870,7 +873,7 @@ let rec superlift c n= ;; -let equality_replace a b ~status = +let equality_replace a b status = debug("inizio EQ\n"); let module C = Cic in let proof,goal = status in @@ -884,7 +887,7 @@ debug("inizio EQ\n"); debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl))); let (proof,goals) = EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl)) - ~status:((curi,metasenv',pbo,pty),goal) + ((curi,metasenv',pbo,pty),goal) in let new_goals = fresh_meta::goals in debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = " @@ -892,14 +895,14 @@ debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = " (proof,new_goals) ;; -let tcl_fail a ~status:(proof,goal) = +let tcl_fail a (proof,goal) = match a with 1 -> raise (ProofEngineTypes.Fail "fail-tactical") |_-> (proof,[goal]) ;; (* Galla: moved in variousTactics.ml -let assumption_tac ~status:(proof,goal)= +let assumption_tac (proof,goal)= let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let num = ref 0 in @@ -911,25 +914,25 @@ let assumption_tac ~status:(proof,goal)= ) context in - Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal) + Tacticals.try_tactics ~tactics:tac_list (proof,goal) ;; *) (* Galla: moved in negationTactics.ml (* !!!!! fix !!!!!!!!!! *) -let contradiction_tac ~status:(proof,goal)= +let contradiction_tac (proof,goal)= Tacticals.then_ (*inutile sia questo che quello prima della chiamata*) ~start:PrimitiveTactics.intros_tac ~continuation:(Tacticals.then_ ~start:(VariousTactics.elim_type_tac ~term:_False) ~continuation:(assumption_tac)) - ~status:(proof,goal) + (proof,goal) ;; *) (* ********************* TATTICA ******************************** *) -let rec fourier ~status:(s_proof,s_goal)= +let rec fourier (s_proof,s_goal)= let s_curi,s_metasenv,s_pbo,s_pty = s_proof in let s_metano,s_context,s_ty = CicUtil.lookup_meta s_goal s_metasenv in debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n"); @@ -962,7 +965,7 @@ theoreme,so let's parse our thesis *) Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl) ~continuation:(PrimitiveTactics.intros_tac ()) - ~status:(s_proof,s_goal) in + (s_proof,s_goal) in let goal = if List.length gl = 1 then List.hd gl else failwith "a new goal" in @@ -1054,26 +1057,26 @@ theoreme,so let's parse our thesis *) debug "inizio a costruire tac1\n"; Fourier.print_rational(c1); - let tac1=ref ( fun ~status -> + let tac1=ref ( fun status -> if h1.hstrict then (Tacticals.thens ~start:( - fun ~status -> + fun status -> debug ("inizio t1 strict\n"); let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n"); debug ("ty = "^ CicPp.ppterm ty^"\n"); - PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status) + PrimitiveTactics.apply_tac ~term:_Rfourier_lt status) ~continuations:[tac_use h1;tac_zero_inf_pos (rational_to_fraction c1)] - ~status + status ) else (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le) ~continuations:[tac_use h1;tac_zero_inf_pos - (rational_to_fraction c1)] ~status + (rational_to_fraction c1)] status ) ) @@ -1094,13 +1097,13 @@ theoreme,so let's parse our thesis *) Fourier.print_rational(c1); tac1:=(Tacticals.thens ~start:( - fun ~status -> + fun status -> debug("INIZIO TAC 1 2\n"); let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n"); debug ("ty = "^ CicPp.ppterm ty^"\n"); - PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status) + PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le status) ~continuations:[!tac1;tac_use h;tac_zero_inf_pos (rational_to_fraction c)]) ) @@ -1133,37 +1136,38 @@ theoreme,so let's parse our thesis *) tac:=(Tacticals.thens ~start:(my_cut ~term:ineq) ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)(**)Tacticals.then_ - ~start:(fun ~status:(proof,goal as status) -> + ~start:(fun status -> + let (proof, goal) = status in let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in PrimitiveTactics.change_tac ~what:ty - ~with_what:(Cic.Appl [ _not; ineq]) ~status) + ~with_what:(Cic.Appl [ _not; ineq]) status) ~continuation:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term: (if sres then _Rnot_lt_lt else _Rnot_le_le)) ~continuation:(Tacticals.thens ~start:( - fun ~status -> + fun status -> debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n"); let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc - ~status + status in (match r with (p,gl) -> debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" )); r) ~continuations:[(Tacticals.thens ~start:( - fun ~status -> - let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in + fun status -> + let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 status in (match r with (p,gl) -> debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" )); r) ~continuations: [PrimitiveTactics.apply_tac ~term:_Rinv_R1 ;Tacticals.try_tactics - ~tactics:[ "ring", (fun ~status -> + ~tactics:[ "ring", (fun status -> debug("begin RING\n"); - let r = Ring.ring_tac ~status in + let r = Ring.ring_tac status in debug ("end RING\n"); r) ; "id", Tacticals.id_tac] @@ -1172,7 +1176,8 @@ theoreme,so let's parse our thesis *) Tacticals.then_ ~start: ( - fun ~status:(proof,goal as status) -> + fun status -> + let (proof, goal) = status in let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in (* check if ty is of type *) @@ -1182,7 +1187,7 @@ theoreme,so let's parse our thesis *) Cic.Prod (Cic.Anonymous,a,b) -> (Cic.Appl [_not;a]) |_ -> assert false) in - let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 ~status in + let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 status in debug("fine MY_CHNGE\n"); r @@ -1194,12 +1199,12 @@ theoreme,so let's parse our thesis *) |_-> assert false); (*match res*) debug ("finalmente applico tac\n"); ( - let r = !tac ~status:(proof,goal) in + let r = !tac (proof,goal) in debug("\n\n]]]]]]]]]]]]]]]]]) That's all folks ([[[[[[[[[[[[[[[[[[[\n\n");r ) ;; -let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);; +let fourier_tac (proof,goal) = fourier (proof,goal);; diff --git a/helm/ocaml/tactics/introductionTactics.ml b/helm/ocaml/tactics/introductionTactics.ml index b425f219a..9751b2b74 100644 --- a/helm/ocaml/tactics/introductionTactics.ml +++ b/helm/ocaml/tactics/introductionTactics.ml @@ -23,8 +23,7 @@ * 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 @@ -34,27 +33,12 @@ let constructor_tac ~n ~status:(proof, goal) = | (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 ;; diff --git a/helm/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml index fc21ec405..65fe892fa 100644 --- a/helm/ocaml/tactics/negationTactics.ml +++ b/helm/ocaml/tactics/negationTactics.ml @@ -24,7 +24,8 @@ *) -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 @@ -32,12 +33,12 @@ let absurd_tac ~term ~status:((proof,goal) as status) = 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 @@ -52,7 +53,7 @@ let contradiction_tac ~status = ~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 *) @@ -60,13 +61,13 @@ let contradiction_tac ~status = (* 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) ;; *) diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index 5909075d8..30d08c9bd 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -250,7 +250,7 @@ let 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 @@ -328,16 +328,16 @@ let apply_tac ~term ~status:(proof, goal) = (* 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 @@ -354,7 +354,7 @@ let intros_tac 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 @@ -386,7 +386,7 @@ let cut_tac 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 @@ -410,7 +410,7 @@ let letin_tac (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 @@ -428,7 +428,7 @@ let exact_tac ~term ~status:(proof, goal) = (* 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 @@ -571,7 +571,7 @@ exception NotConvertible (*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 *) diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.ml b/helm/ocaml/tactics/proofEngineStructuralRules.ml index 7f4a89fb8..20b0f21c9 100644 --- a/helm/ocaml/tactics/proofEngineStructuralRules.ml +++ b/helm/ocaml/tactics/proofEngineStructuralRules.ml @@ -25,7 +25,7 @@ open ProofEngineTypes -let clearbody ~hyp ~status:(proof, goal) = +let clearbody ~hyp (proof, goal) = let module C = Cic in match hyp with None -> assert false @@ -91,7 +91,7 @@ let clearbody ~hyp ~status:(proof, goal) = 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 diff --git a/helm/ocaml/tactics/proofEngineTypes.ml b/helm/ocaml/tactics/proofEngineTypes.ml index 334c594da..d668090e4 100644 --- a/helm/ocaml/tactics/proofEngineTypes.ml +++ b/helm/ocaml/tactics/proofEngineTypes.ml @@ -30,12 +30,13 @@ type proof = UriManager.uri * Cic.metasenv * Cic.term * Cic.term (** 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 diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml index 5a567b84a..80cb3306a 100644 --- a/helm/ocaml/tactics/reductionTactics.ml +++ b/helm/ocaml/tactics/reductionTactics.ml @@ -24,7 +24,7 @@ *) (* -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 @@ -40,7 +40,7 @@ let reduction_tac ~reduction ~status:(proof,goal) = *) (* 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 = @@ -93,7 +93,7 @@ let simpl_tac = reduction_tac ~reduction:ProofEngineReduction.simpl ;; 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 diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml index f9755474c..e2de04591 100644 --- a/helm/ocaml/tactics/ring.ml +++ b/helm/ocaml/tactics/ring.ml @@ -130,15 +130,16 @@ let uri_of_proof ~proof:(uri, _, _, _) = uri @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 @@ -376,10 +377,10 @@ let status_of_single_goal_tactic_result = @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 *) (** @@ -388,11 +389,11 @@ let elim_type_tac ~term ~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 (** @@ -401,11 +402,11 @@ let elim_type2_tac ~term ~proof ~status = 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)) @@ -422,15 +423,16 @@ let lift ~n (a,b,c,d,e,f,g,h) = @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 @@ -445,11 +447,12 @@ let purge_hyps_tac ~count ~status:(proof, goal as status) = 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 @@ -465,7 +468,7 @@ let ring_tac ~status:((proof, goal) as status) = 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'' ; @@ -480,14 +483,14 @@ let ring_tac ~status:((proof, goal) as status) = ] ; 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 *) @@ -504,7 +507,7 @@ let ring_tac ~status:((proof, goal) as status) = 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 ...", @@ -518,14 +521,14 @@ let ring_tac ~status:((proof, goal) as status) = ] ; 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 *) @@ -539,10 +542,10 @@ let ring_tac ~status:((proof, goal) as status) = 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) -> @@ -552,9 +555,9 @@ let ring_tac ~status:((proof, goal) as status) = 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") diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml index fe593a4f8..5851b1467 100644 --- a/helm/ocaml/tactics/tacticChaser.ml +++ b/helm/ocaml/tactics/tacticChaser.ml @@ -40,7 +40,7 @@ module U = MQGUtil 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 @@ -80,7 +80,7 @@ match list_of_must with (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 @@ -111,7 +111,7 @@ match list_of_must with (*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 @@ -151,7 +151,7 @@ match list_of_must with ((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)); @@ -192,14 +192,14 @@ let position n = (*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 @@ -212,7 +212,7 @@ in 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) = @@ -234,15 +234,15 @@ in (* 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 = @@ -255,7 +255,7 @@ prerr_endline "3"; 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 diff --git a/helm/ocaml/tactics/tacticChaser.mli b/helm/ocaml/tactics/tacticChaser.mli index e7e63954a..d4f8a2c54 100644 --- a/helm/ocaml/tactics/tacticChaser.mli +++ b/helm/ocaml/tactics/tacticChaser.mli @@ -28,13 +28,14 @@ val matchConclusion : MQIConn.handle -> 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 diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml index 8414698e7..8d4eb891e 100644 --- a/helm/ocaml/tactics/tacticals.ml +++ b/helm/ocaml/tactics/tacticals.ml @@ -42,8 +42,7 @@ let warn s = (* not a tactical, but it's used only here (?) *) -let id_tac ~status:(proof,goal) = - (proof,[goal]) +let id_tac (proof,goal) = (proof,[goal]) (** @@ -55,13 +54,13 @@ let id_tac ~status:(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 @@ -73,19 +72,19 @@ let rec try_tactics ~(tactics: (string * tactic) list) ~status = 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 @@ -93,11 +92,11 @@ let thens ~start ~continuations ~status = -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 @@ -112,14 +111,14 @@ let then_ ~start ~continuation ~status = (* When 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 @@ -127,25 +126,25 @@ let rec repeat_tactic ~tactic ~status = 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 @@ -153,48 +152,48 @@ let rec do_tactic ~n ~tactic ~status = 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 ;; @@ -208,19 +207,20 @@ let rec solve_tactics ~(tactics: (string * tactic) list) ~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 = @@ -234,7 +234,7 @@ let prova_tac = 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 diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index 080ba224d..98c13e80b 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -23,7 +23,8 @@ * 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 @@ -35,7 +36,7 @@ let search_theorems_in_context ~status:((proof,goal) as status) = | 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 @@ -65,8 +66,8 @@ if level = 0 then 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 @@ -93,7 +94,7 @@ prerr_endline ("GOALLIST = " ^ string_of_int (List.length goallist)); 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 @@ -109,7 +110,8 @@ prerr_endline "AUTO_TAC HA FINITO"; 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 @@ -128,7 +130,7 @@ let assumption_tac ~status:((proof,goal) as status) = | _ -> 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 *) @@ -141,8 +143,9 @@ contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *) 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 @@ -173,7 +176,7 @@ let generalize_tac ~where:ty) ))) ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac] - ~status + status ;; diff --git a/helm/ocaml/tactics/variousTactics.mli b/helm/ocaml/tactics/variousTactics.mli index 2be47c1ec..c27e542ff 100644 --- a/helm/ocaml/tactics/variousTactics.mli +++ b/helm/ocaml/tactics/variousTactics.mli @@ -33,6 +33,6 @@ val generalize_tac: ProofEngineTypes.tactic val auto_tac : - MQIConn.handle -> - status:ProofEngineTypes.status - -> ProofEngineTypes.proof * ProofEngineTypes.goal list + MQIConn.handle -> ProofEngineTypes.status -> + ProofEngineTypes.proof * ProofEngineTypes.goal list + -- 2.39.2