From 03cb4be465e546a00f870213b14dcf1b71c4831d Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 5 Nov 2004 11:03:01 +0000 Subject: [PATCH] - added Tactics module as a common point where tactics could be accessed --- helm/ocaml/tactics/.depend | 13 ++++- helm/ocaml/tactics/Makefile | 8 +++- helm/ocaml/tactics/primitiveTactics.ml | 4 +- helm/ocaml/tactics/primitiveTactics.mli | 6 ++- helm/ocaml/tactics/tactics.ml | 64 +++++++++++++++++++++++++ helm/ocaml/tactics/tactics.mli | 62 ++++++++++++++++++++++++ 6 files changed, 150 insertions(+), 7 deletions(-) create mode 100644 helm/ocaml/tactics/tactics.ml create mode 100644 helm/ocaml/tactics/tactics.mli diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index 1f98e15f4..8e1412bbb 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -14,6 +14,7 @@ discriminationTactics.cmi: proofEngineTypes.cmi ring.cmi: proofEngineTypes.cmi fourierR.cmi: proofEngineTypes.cmi statefulProofEngine.cmi: proofEngineTypes.cmi +tactics.cmi: proofEngineTypes.cmi proofEngineTypes.cmo: proofEngineTypes.cmi proofEngineTypes.cmx: proofEngineTypes.cmi proofEngineReduction.cmo: proofEngineReduction.cmi @@ -36,6 +37,8 @@ primitiveTactics.cmo: proofEngineHelpers.cmi proofEngineReduction.cmi \ primitiveTactics.cmx: proofEngineHelpers.cmx proofEngineReduction.cmx \ proofEngineTypes.cmx reductionTactics.cmx tacticals.cmx \ primitiveTactics.cmi +hashtbl_equiv.cmo: hashtbl_equiv.cmi +hashtbl_equiv.cmx: hashtbl_equiv.cmi metadataQuery.cmo: hashtbl_equiv.cmi primitiveTactics.cmi \ proofEngineTypes.cmi metadataQuery.cmi metadataQuery.cmx: hashtbl_equiv.cmx primitiveTactics.cmx \ @@ -44,8 +47,6 @@ variousTactics.cmo: primitiveTactics.cmi proofEngineReduction.cmi \ proofEngineTypes.cmi tacticals.cmi variousTactics.cmi variousTactics.cmx: primitiveTactics.cmx proofEngineReduction.cmx \ proofEngineTypes.cmx tacticals.cmx variousTactics.cmi -hashtbl_equiv.cmo: hashtbl_equiv.cmi -hashtbl_equiv.cmx: hashtbl_equiv.cmi autoTactic.cmo: metadataQuery.cmi primitiveTactics.cmi proofEngineHelpers.cmi \ proofEngineTypes.cmi autoTactic.cmi autoTactic.cmx: metadataQuery.cmx primitiveTactics.cmx proofEngineHelpers.cmx \ @@ -96,3 +97,11 @@ statefulProofEngine.cmo: history.cmi proofEngineTypes.cmi \ statefulProofEngine.cmi statefulProofEngine.cmx: history.cmx proofEngineTypes.cmx \ statefulProofEngine.cmi +tactics.cmo: autoTactic.cmi discriminationTactics.cmi eliminationTactics.cmi \ + equalityTactics.cmi fourierR.cmi introductionTactics.cmi \ + negationTactics.cmi primitiveTactics.cmi reductionTactics.cmi ring.cmi \ + variousTactics.cmi tactics.cmi +tactics.cmx: autoTactic.cmx discriminationTactics.cmx eliminationTactics.cmx \ + equalityTactics.cmx fourierR.cmx introductionTactics.cmx \ + negationTactics.cmx primitiveTactics.cmx reductionTactics.cmx ring.cmx \ + variousTactics.cmx tactics.cmi diff --git a/helm/ocaml/tactics/Makefile b/helm/ocaml/tactics/Makefile index 33391a5e4..60ca2cd0c 100644 --- a/helm/ocaml/tactics/Makefile +++ b/helm/ocaml/tactics/Makefile @@ -12,8 +12,14 @@ INTERFACE_FILES = \ variousTactics.mli autoTactic.mli \ introductionTactics.mli eliminationTactics.mli negationTactics.mli \ equalityTactics.mli discriminationTactics.mli ring.mli fourier.mli \ - fourierR.mli history.mli statefulProofEngine.mli + fourierR.mli history.mli statefulProofEngine.mli tactics.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) +all: + +tactics.mli: tactics.ml *Tactics.mli autoTactic.mli fourierR.mli ring.mli + echo "(* GENERATED FILE, DO NOT EDIT *)" > $@ + $(OCAMLC) -i $< >> $@ + include ../Makefile.common diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index c411340ae..fa6968560 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -382,7 +382,7 @@ let intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) ()= in mk_tactic (intros_tac ~mk_fresh_name_callback ()) -let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) term= +let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) ~term= let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) term (proof, goal) @@ -417,7 +417,7 @@ let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) term= in mk_tactic (cut_tac ~mk_fresh_name_callback term) -let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name) term= +let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name) ~term= let letin_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) term (proof, goal) diff --git a/helm/ocaml/tactics/primitiveTactics.mli b/helm/ocaml/tactics/primitiveTactics.mli index 5bbc7d188..653894637 100644 --- a/helm/ocaml/tactics/primitiveTactics.mli +++ b/helm/ocaml/tactics/primitiveTactics.mli @@ -37,10 +37,12 @@ val intros_tac: ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> unit -> ProofEngineTypes.tactic val cut_tac: - ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term -> + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> + term:Cic.term -> ProofEngineTypes.tactic val letin_tac: - ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term -> + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> + term:Cic.term -> ProofEngineTypes.tactic val elim_intros_simpl_tac: diff --git a/helm/ocaml/tactics/tactics.ml b/helm/ocaml/tactics/tactics.ml new file mode 100644 index 000000000..152e07b27 --- /dev/null +++ b/helm/ocaml/tactics/tactics.ml @@ -0,0 +1,64 @@ +(* Copyright (C) 2004, 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/. + *) + +let absurd = NegationTactics.absurd_tac +let apply = PrimitiveTactics.apply_tac +let assumption = VariousTactics.assumption_tac +let auto = AutoTactic.auto_tac +let auto_new = AutoTactic.auto_tac_new +let change = PrimitiveTactics.change_tac +let compare = DiscriminationTactics.compare_tac +let constructor = IntroductionTactics.constructor_tac +let contradiction = NegationTactics.contradiction_tac +let cut = PrimitiveTactics.cut_tac +let decide_equality = DiscriminationTactics.decide_equality_tac +let decompose = EliminationTactics.decompose_tac +let discriminate = DiscriminationTactics.discriminate_tac +let elim_intros_simpl = PrimitiveTactics.elim_intros_simpl_tac +let elim_type = EliminationTactics.elim_type_tac +let exact = PrimitiveTactics.exact_tac +let exists = IntroductionTactics.exists_tac +let fold = ReductionTactics.fold_tac +let fourier = FourierR.fourier_tac +let generalize = VariousTactics.generalize_tac +let injection = DiscriminationTactics.injection_tac +let intros = PrimitiveTactics.intros_tac +let left = IntroductionTactics.left_tac +let letin = PrimitiveTactics.letin_tac +let reduce = ReductionTactics.reduce_tac +let reflexivity = EqualityTactics.reflexivity_tac +let replace = EqualityTactics.replace_tac +let rewrite_back = EqualityTactics.rewrite_back_tac +let rewrite_back_simpl = EqualityTactics.rewrite_back_simpl_tac +let rewrite = EqualityTactics.rewrite_tac +let rewrite_simpl = EqualityTactics.rewrite_simpl_tac +let right = IntroductionTactics.right_tac +let ring = Ring.ring_tac +let simpl = ReductionTactics.simpl_tac +let split = IntroductionTactics.split_tac +let symmetry = EqualityTactics.symmetry_tac +let transitivity = EqualityTactics.transitivity_tac +let whd = ReductionTactics.whd_tac + diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli new file mode 100644 index 000000000..7b771249e --- /dev/null +++ b/helm/ocaml/tactics/tactics.mli @@ -0,0 +1,62 @@ +(* GENERATED FILE, DO NOT EDIT *) +val absurd : term:Cic.term -> ProofEngineTypes.tactic +val apply : term:Cic.term -> ProofEngineTypes.tactic +val assumption : ProofEngineTypes.tactic +val auto : dbd:Mysql.dbd -> ProofEngineTypes.tactic +val auto_new : dbd:Mysql.dbd -> ProofEngineTypes.tactic +val change : what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic +val compare : term:Cic.term -> ProofEngineTypes.tactic +val constructor : n:int -> ProofEngineTypes.tactic +val contradiction : ProofEngineTypes.tactic +val cut : + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> + term:Cic.term -> ProofEngineTypes.tactic +val decide_equality : ProofEngineTypes.tactic +val decompose : + ?uris_choice_callback:((UriManager.uri * int * + (UriManager.uri * Cic.term) list) + list -> + (UriManager.uri * int * + (UriManager.uri * Cic.term) list) + list) -> + Cic.term -> ProofEngineTypes.tactic +val discriminate : term:Cic.term -> ProofEngineTypes.tactic +val elim_intros_simpl : term:Cic.term -> ProofEngineTypes.tactic +val elim_type : term:Cic.term -> ProofEngineTypes.tactic +val exact : term:Cic.term -> ProofEngineTypes.tactic +val exists : ProofEngineTypes.tactic +val fold : + reduction:(Cic.context -> Cic.term -> Cic.term) -> + also_in_hypotheses:bool -> term:Cic.term -> ProofEngineTypes.tactic +val fourier : ProofEngineTypes.tactic +val generalize : + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> + Cic.term list -> ProofEngineTypes.tactic +val injection : term:Cic.term -> ProofEngineTypes.tactic +val intros : + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> + unit -> ProofEngineTypes.tactic +val left : ProofEngineTypes.tactic +val letin : + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> + term:Cic.term -> ProofEngineTypes.tactic +val reduce : + also_in_hypotheses:bool -> + terms:Cic.term list option -> ProofEngineTypes.tactic +val reflexivity : ProofEngineTypes.tactic +val replace : what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic +val rewrite_back : term:Cic.term -> ProofEngineTypes.tactic +val rewrite_back_simpl : term:Cic.term -> ProofEngineTypes.tactic +val rewrite : term:Cic.term -> ProofEngineTypes.tactic +val rewrite_simpl : term:Cic.term -> ProofEngineTypes.tactic +val right : ProofEngineTypes.tactic +val ring : ProofEngineTypes.tactic +val simpl : + also_in_hypotheses:bool -> + terms:Cic.term list option -> ProofEngineTypes.tactic +val split : ProofEngineTypes.tactic +val symmetry : ProofEngineTypes.tactic +val transitivity : term:Cic.term -> ProofEngineTypes.tactic +val whd : + also_in_hypotheses:bool -> + terms:Cic.term list option -> ProofEngineTypes.tactic -- 2.39.2