From 7562b71d0a7c232cd84018ed7e3d0e81a621d690 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 12 Jan 2006 13:54:08 +0000
Subject: [PATCH] fixed paramodulation trnsition

---
 helm/matita/configure.ac                      |  2 -
 helm/ocaml/METAS/meta.helm-paramodulation.src |  5 --
 helm/ocaml/Makefile.in                        |  1 -
 .../ocaml/tactics/paramodulation/indexing.mli | 88 +++++++++++++++++++
 4 files changed, 88 insertions(+), 8 deletions(-)
 delete mode 100644 helm/ocaml/METAS/meta.helm-paramodulation.src
 create mode 100644 helm/ocaml/tactics/paramodulation/indexing.mli

diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac
index 1075d605d..c07a962ae 100644
--- 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
index 34a25fef0..000000000
--- 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 0c2d49411..88410454c 100644
--- 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
index 000000000..9b051bc40
--- /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
-- 
2.39.2