- added Tactics module as a common point where tactics could be accessed

diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend
index 1f98e15f455e729a4975eede0c714ada1ac71a6c..8e1412bbbba85b1107e80e7cd39b284e19698158 100644 (file)
--- 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 33391a5e4740714803dfab360a543c866eb66c4b..60ca2cd0c205ee28a4e6fe9390289f8fa74451e3 100644 (file)
--- 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 c411340ae829ee94159f7ac90e5d0e76c7882a71..fa696856010431f53bb14546df11163a440c61b0 100644 (file)
--- 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 5bbc7d188412702d49a8e1a615f30a04c7170664..6538946375ed953be4f0c468bef6fa99d1237be4 100644 (file)
--- 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 (file)
index 0000000..152e07b
--- /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 (file)
index 0000000..7b77124
--- /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