fixed paramodulation trnsition

diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac
index 1075d605d4d025496621b4bf47e8cee5f61315fb..c07a962ae2d12011a9019cc44f15e0cb18235e98 100644 (file)
--- a/helm/matita/configure.ac
+++ b/helm/matita/configure.ac
@@ -48,7 +48,6 @@ helm-extlib \
 "
 FINDLIB_CREQUIRES=" \
 $FINDLIB_COMREQUIRES \
-helm-paramodulation \
 "
 FINDLIB_REQUIRES="\
 $FINDLIB_CREQUIRES \
@@ -56,7 +55,6 @@ lablgtk2.glade \
 lablgtkmathview \
 lablgtksourceview \
 helm-xmldiff \
-helm-paramodulation \
 "
 for r in $FINDLIB_REQUIRES
 do

diff --git a/helm/ocaml/METAS/meta.helm-paramodulation.src b/helm/ocaml/METAS/meta.helm-paramodulation.src
deleted file mode 100644 (file)
index 34a25fe..0000000
--- a/helm/ocaml/METAS/meta.helm-paramodulation.src
+++ /dev/null
@@ -1,5 +0,0 @@
-requires="helm-registry helm-tactics"
-version="0.0.1"
-archive(byte)="paramodulation.cma"
-archive(native)="paramodulation.cmxa"
-linkopts=""

diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in
index 0c2d4941177a12cacac17e0b24afb51f7d32da6b..88410454c48931e63cedc45ace1d735a2ba4c257 100644 (file)
--- a/helm/ocaml/Makefile.in
+++ b/helm/ocaml/Makefile.in
@@ -23,7 +23,6 @@ MODULES =                     \
        cic_unification         \
        whelp                   \
        tactics                 \
-       paramodulation          \
        cic_disambiguation      \
        lexicon                 \
        grafite_engine          \

diff --git a/helm/ocaml/tactics/paramodulation/indexing.mli b/helm/ocaml/tactics/paramodulation/indexing.mli
new file mode 100644 (file)
index 0000000..9b051bc
--- /dev/null
+++ b/helm/ocaml/tactics/paramodulation/indexing.mli
@@ -0,0 +1,88 @@
+(* Copyright (C) 2005, 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/.
+ *)
+
+(* $Id$ *)
+
+module Index :
+  sig
+    module PosEqSet : Set.S 
+      with type elt = Utils.pos * Inference.equality
+      and type t = Equality_indexing.DT.PosEqSet.t
+    type t = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet).t
+    type key = Cic.term
+  end
+
+val index : Index.t -> Inference.equality -> Index.t
+val remove_index : Index.t -> Inference.equality -> Index.t
+val in_index : Index.t -> Inference.equality -> bool
+val empty : Index.t
+val match_unif_time_ok : float ref
+val match_unif_time_no : float ref
+val indexing_retrieval_time : float ref
+val init_index : unit -> unit
+val build_newtarget_time : float ref
+val subsumption :
+  Cic.metasenv * Cic.context * CicUniv.universe_graph ->
+  Index.t ->
+  'a * 'b * ('c * Index.key * Index.key * 'd) * Cic.metasenv * 'e ->
+  bool * Cic.substitution
+val superposition_left :
+  int ->
+  Cic.metasenv * Cic.context * CicUniv.universe_graph ->
+  Index.t ->
+  'a * Inference.proof *
+  (Index.key * Index.key * Index.key * Utils.comparison) * 'b * 'c ->
+  int *
+  (int * Inference.proof *
+   (Index.key * Index.key * Index.key * Utils.comparison) * 'd list * 
+   'e list)
+  list
+val superposition_right :
+  int ->
+  Cic.metasenv * Cic.context * CicUniv.universe_graph ->
+  Index.t ->
+  'a * Inference.proof *
+  (Cic.term * Index.key * Index.key * Utils.comparison) *
+  Cic.metasenv * Cic.term list -> int * Inference.equality list
+val demodulation_equality :
+  int ->
+  Cic.metasenv * Cic.context * CicUniv.universe_graph ->
+  Index.t ->
+  Utils.equality_sign -> Inference.equality -> int * Inference.equality
+val demodulation_goal :
+  int ->
+  Cic.metasenv * Cic.context * CicUniv.universe_graph ->
+  Index.t ->
+  Inference.proof * Cic.metasenv * Index.key ->
+  int * (Inference.proof * Cic.metasenv * Index.key)
+val demodulation_theorem :
+  'a ->
+  Cic.metasenv * Cic.context * CicUniv.universe_graph ->
+  Index.t ->
+  Cic.term * Index.key * Cic.metasenv ->
+  'a * (Cic.term * Index.key * Cic.metasenv)
+val demodulate_tac: 
+  dbd:HMysql.dbd ->  
+  pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic