From 71922d0022ee8f9e507f601dc93a2f68c2080d85 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 13 Sep 2002 11:19:59 +0000 Subject: [PATCH] ring.ml* splitted into ring.ml* and tacticals.ml* --- helm/gTopLevel/.depend | 11 +++-- helm/gTopLevel/Makefile | 8 ++-- helm/gTopLevel/fourierR.ml | 15 ++---- helm/gTopLevel/ring.ml | 59 ++---------------------- helm/gTopLevel/ring.mli | 10 ---- helm/gTopLevel/tacticals.ml | 89 ++++++++++++++++++++++++++++++++++++ helm/gTopLevel/tacticals.mli | 34 ++++++++++++++ 7 files changed, 142 insertions(+), 84 deletions(-) create mode 100644 helm/gTopLevel/tacticals.ml create mode 100644 helm/gTopLevel/tacticals.mli diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index dfdd053fb..5ea3dfae2 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -14,13 +14,16 @@ primitiveTactics.cmo: proofEngineHelpers.cmi proofEngineReduction.cmi \ primitiveTactics.cmx: proofEngineHelpers.cmx proofEngineReduction.cmx \ proofEngineTypes.cmx primitiveTactics.cmi primitiveTactics.cmi: proofEngineTypes.cmo +tacticals.cmo: primitiveTactics.cmi proofEngineTypes.cmo tacticals.cmi +tacticals.cmx: primitiveTactics.cmx proofEngineTypes.cmx tacticals.cmi +tacticals.cmi: proofEngineTypes.cmo ring.cmo: primitiveTactics.cmi proofEngineStructuralRules.cmi \ - proofEngineTypes.cmo ring.cmi + proofEngineTypes.cmo tacticals.cmi ring.cmi ring.cmx: primitiveTactics.cmx proofEngineStructuralRules.cmx \ - proofEngineTypes.cmx ring.cmi + proofEngineTypes.cmx tacticals.cmx ring.cmi ring.cmi: proofEngineTypes.cmo -fourierR.cmo: fourier.cmo fourierR.cmi -fourierR.cmx: fourier.cmx fourierR.cmi +fourierR.cmo: fourier.cmo primitiveTactics.cmi ring.cmi fourierR.cmi +fourierR.cmx: fourier.cmx primitiveTactics.cmx ring.cmx fourierR.cmi fourierR.cmi: proofEngineTypes.cmo proofEngine.cmo: fourierR.cmi primitiveTactics.cmi proofEngineHelpers.cmi \ proofEngineReduction.cmi proofEngineStructuralRules.cmi \ diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index 0b3fd06b1..f0ec4bfce 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -17,7 +17,8 @@ opt: gTopLevel.opt DEPOBJS = xml2Gdome.ml xml2Gdome.mli proofEngineTypes.ml proofEngineHelpers.ml \ proofEngineReduction.ml proofEngineReduction.mli \ proofEngineStructuralRules.ml proofEngineStructuralRules.mli \ - primitiveTactics.ml primitiveTactics.mli ring.ml ring.mli fourier.ml fourierR.ml fourierR.mli\ + primitiveTactics.ml primitiveTactics.mli tacticals.ml tacticals.mli \ + ring.ml ring.mli fourier.ml fourierR.ml fourierR.mli\ proofEngine.ml proofEngine.mli \ doubleTypeInference.ml doubleTypeInference.mli cic2acic.ml \ cic2acic.mli cic2Xml.ml cic2Xml.mli logicalOperations.ml \ @@ -25,8 +26,9 @@ DEPOBJS = xml2Gdome.ml xml2Gdome.mli proofEngineTypes.ml proofEngineHelpers.ml \ mQueryGenerator.ml gTopLevel.ml TOPLEVELOBJS = xml2Gdome.cmo proofEngineTypes.cmo proofEngineHelpers.cmo \ - proofEngineReduction.cmo proofEngineStructuralRules.cmo \ - primitiveTactics.cmo ring.cmo fourier.cmo fourierR.cmo proofEngine.cmo \ + proofEngineReduction.cmo proofEngineStructuralRules.cmo \ + primitiveTactics.cmo tacticals.cmo ring.cmo \ + fourier.cmo fourierR.cmo proofEngine.cmo \ doubleTypeInference.cmo cic2acic.cmo cic2Xml.cmo \ logicalOperations.cmo sequentPp.cmo mQueryGenerator.cmo \ gTopLevel.cmo diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index b8d88ae19..815a39aa1 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -461,24 +461,15 @@ let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_ let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/_Rlt_mult_inv_pos.con") 0 ;; -let tcl_then ~start ~continuation ~status = - let tcl_then_aux (proof,goals) goal = - let (newproof,newgoals) = continuation ~status:(proof,goal) in - (newproof, goals @ newgoals) - in - let (proof,new_goals) = start ~status in - List.fold_left tcl_then_aux (proof,[]) new_goals -;; - let tac_zero_inf_pos gl (n,d) = (*let cste = pf_parse_constr gl in*) let tacn=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in for i=1 to n-1 do - tacn:=(tcl_then ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacn); done; + tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacn); done; for i=1 to d-1 do - tacd:=(tcl_then ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); done; - (Ring.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) ~continuations:[!tacn;!tacd]) + tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); done; + (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) ~continuations:[!tacn;!tacd]) ;; (* preuve que 0<=n*1/d diff --git a/helm/gTopLevel/ring.ml b/helm/gTopLevel/ring.ml index 69f4b87a3..953ed6444 100644 --- a/helm/gTopLevel/ring.ml +++ b/helm/gTopLevel/ring.ml @@ -369,57 +369,6 @@ let build_segments ~terms ~proof = [lxy_false; varmap; rtheory; t])) aterms -(** AUX TACTIC{,AL}S *) - - (** - naive implementation of ORELSE tactical, try a sequence of tactics in turn: - if one fails pass to the next one and so on, eventually raises (failure "no - tactics left") - TODO warning: not tail recursive due to "try .. with" boxing - *) -let rec try_tactics ~(tactics: (string * tactic) list) ~status = - warn "in Ring.try_tactics"; - match tactics with - | (descr, tac)::tactics -> - warn ("Ring.try_tactics IS TRYING " ^ descr); - (try - let res = tac ~status in - warn ("Ring.try_tactics: " ^ descr ^ " succedeed!!!"); - res - with - e -> - match e with - (Fail _) - | (CicTypeChecker.NotWellTyped _) - | (CicUnification.UnificationFailed) -> - warn ( - "Ring.try_tactics failed with exn: " ^ - Printexc.to_string e); - 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 - try - List.fold_left2 - (fun (proof,goals) goal tactic -> - let (proof',new_goals') = tactic ~status:(proof,goal) in - (proof',goals@new_goals') - ) (proof,[]) new_goals continuations - with - Invalid_argument _ -> raise (Fail "thens: wrong number of new goals") - -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 - (proof',goals@new_goals') - ) (proof,[]) new_goals - - let id_tac ~status:(proof,goal) = (proof,[goal]) @@ -436,7 +385,7 @@ let status_of_single_goal_tactic_result = *) let elim_type_tac ~term ~status = warn "in Ring.elim_type_tac"; - thens ~start:(cut_tac ~term) + Tacticals.thens ~start:(cut_tac ~term) ~continuations:[elim_intros_simpl_tac ~term:(Cic.Rel 1) ; id_tac] ~status (** @@ -447,7 +396,7 @@ let elim_type_tac ~term ~status = *) let elim_type2_tac ~term ~proof ~status = warn "in Ring.elim_type2"; - thens ~start:(elim_type_tac ~term) + Tacticals.thens ~start:(elim_type_tac ~term) ~continuations:[id_tac ; exact_tac ~term:proof] ~status (** @@ -519,7 +468,7 @@ let ring_tac ~status:(proof, goal) = t2; t2'; t2''; t2'_eq_t2'']); try let new_hyps = ref 0 in (* number of new hypotheses created *) - try_tactics + Tacticals.try_tactics ~status ~tactics:[ "reflexivity", reflexivity_tac; @@ -552,7 +501,7 @@ let ring_tac ~status:(proof, goal) = lift 1 (t1,t1',t1'',t1'_eq_t1'', t2,t2',t2'',t2'_eq_t2'') in let status'' = - try_tactics (* try to solve 1st subgoal *) + Tacticals.try_tactics (* try to solve 1st subgoal *) ~status:status' ~tactics:[ "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2''; diff --git a/helm/gTopLevel/ring.mli b/helm/gTopLevel/ring.mli index 67bc1a164..224f150cc 100644 --- a/helm/gTopLevel/ring.mli +++ b/helm/gTopLevel/ring.mli @@ -6,13 +6,3 @@ val ring_tac: ProofEngineTypes.tactic val elim_type_tac: term: Cic.term -> ProofEngineTypes.tactic val reflexivity_tac: ProofEngineTypes.tactic val id_tac : ProofEngineTypes.tactic - - (* pseudo tacticals *) -val try_tactics: - tactics: (string * ProofEngineTypes.tactic) list -> ProofEngineTypes.tactic -val thens: - start: ProofEngineTypes.tactic -> - continuations: ProofEngineTypes.tactic list -> ProofEngineTypes.tactic -val then_: - start: ProofEngineTypes.tactic -> - continuation: ProofEngineTypes.tactic -> ProofEngineTypes.tactic diff --git a/helm/gTopLevel/tacticals.ml b/helm/gTopLevel/tacticals.ml new file mode 100644 index 000000000..f3cd13b44 --- /dev/null +++ b/helm/gTopLevel/tacticals.ml @@ -0,0 +1,89 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +open CicReduction +open PrimitiveTactics +open ProofEngineTypes +open UriManager + +(** DEBUGGING *) + + (** perform debugging output? *) +let debug = false + + (** debugging print *) +let warn s = + if debug then + prerr_endline ("TACTICALS WARNING: " ^ s) + +(** AUX TACTIC{,AL}S *) + + (** + naive implementation of ORELSE tactical, try a sequence of tactics in turn: + if one fails pass to the next one and so on, eventually raises (failure "no + tactics left") + TODO warning: not tail recursive due to "try .. with" boxing + *) +let rec try_tactics ~(tactics: (string * tactic) list) ~status = + warn "in Ring.try_tactics"; + match tactics with + | (descr, tac)::tactics -> + warn ("Ring.try_tactics IS TRYING " ^ descr); + (try + let res = tac ~status in + warn ("Ring.try_tactics: " ^ descr ^ " succedeed!!!"); + res + with + e -> + match e with + (Fail _) + | (CicTypeChecker.NotWellTyped _) + | (CicUnification.UnificationFailed) -> + warn ( + "Ring.try_tactics failed with exn: " ^ + Printexc.to_string e); + 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 + try + List.fold_left2 + (fun (proof,goals) goal tactic -> + let (proof',new_goals') = tactic ~status:(proof,goal) in + (proof',goals@new_goals') + ) (proof,[]) new_goals continuations + with + Invalid_argument _ -> raise (Fail "thens: wrong number of new goals") + +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 + (proof',goals@new_goals') + ) (proof,[]) new_goals diff --git a/helm/gTopLevel/tacticals.mli b/helm/gTopLevel/tacticals.mli new file mode 100644 index 000000000..d2cadf4c8 --- /dev/null +++ b/helm/gTopLevel/tacticals.mli @@ -0,0 +1,34 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + + (* pseudo tacticals *) +val try_tactics: + tactics: (string * ProofEngineTypes.tactic) list -> ProofEngineTypes.tactic +val thens: + start: ProofEngineTypes.tactic -> + continuations: ProofEngineTypes.tactic list -> ProofEngineTypes.tactic +val then_: + start: ProofEngineTypes.tactic -> + continuation: ProofEngineTypes.tactic -> ProofEngineTypes.tactic -- 2.39.2