From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 9 Jun 2009 13:17:31 +0000 (+0000)
Subject: snaphost: supright almost done
X-Git-Tag: make_still_working~3898
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=637114791874df9ebc4e0f0936513c71886a913f;p=helm.git

snaphost: supright almost done
---

diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend
index c8985f260..0a7503d12 100644
--- a/helm/software/components/ng_paramodulation/.depend
+++ b/helm/software/components/ng_paramodulation/.depend
@@ -1,10 +1,10 @@
 terms.cmi: 
 pp.cmi: terms.cmi 
 foSubst.cmi: terms.cmi 
+orderings.cmi: terms.cmi 
 foUtils.cmi: terms.cmi 
-foUnif.cmi: terms.cmi 
 index.cmi: terms.cmi 
-orderings.cmi: terms.cmi 
+foUnif.cmi: terms.cmi 
 superposition.cmi: terms.cmi index.cmi 
 nCicBlob.cmi: terms.cmi 
 cicBlob.cmi: terms.cmi 
@@ -15,21 +15,23 @@ pp.cmo: terms.cmi pp.cmi
 pp.cmx: terms.cmx pp.cmi 
 foSubst.cmo: terms.cmi foSubst.cmi 
 foSubst.cmx: terms.cmx foSubst.cmi 
-foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi 
-foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi 
-foUnif.cmo: terms.cmi foUtils.cmi foSubst.cmi foUnif.cmi 
-foUnif.cmx: terms.cmx foUtils.cmx foSubst.cmx foUnif.cmi 
-index.cmo: terms.cmi foUtils.cmi index.cmi 
-index.cmx: terms.cmx foUtils.cmx index.cmi 
 orderings.cmo: terms.cmi orderings.cmi 
 orderings.cmx: terms.cmx orderings.cmi 
-superposition.cmo: terms.cmi index.cmi superposition.cmi 
-superposition.cmx: terms.cmx index.cmx superposition.cmi 
+foUtils.cmo: terms.cmi orderings.cmi index.cmi foSubst.cmi foUtils.cmi 
+foUtils.cmx: terms.cmx orderings.cmx index.cmx foSubst.cmx foUtils.cmi 
+index.cmo: terms.cmi foUtils.cmi index.cmi 
+index.cmx: terms.cmx foUtils.cmx index.cmi 
+foUnif.cmo: terms.cmi foUtils.cmi foSubst.cmi foUnif.cmi 
+foUnif.cmx: terms.cmx foUtils.cmx foSubst.cmx foUnif.cmi 
+superposition.cmo: terms.cmi orderings.cmi index.cmi foUtils.cmi foUnif.cmi \
+    foSubst.cmi superposition.cmi 
+superposition.cmx: terms.cmx orderings.cmx index.cmx foUtils.cmx foUnif.cmx \
+    foSubst.cmx superposition.cmi 
 nCicBlob.cmo: terms.cmi nCicBlob.cmi 
 nCicBlob.cmx: terms.cmx nCicBlob.cmi 
 cicBlob.cmo: terms.cmi cicBlob.cmi 
 cicBlob.cmx: terms.cmx cicBlob.cmi 
-paramod.cmo: terms.cmi superposition.cmi pp.cmi nCicBlob.cmi index.cmi \
+paramod.cmo: superposition.cmi pp.cmi nCicBlob.cmi index.cmi foUtils.cmi \
     foUnif.cmi paramod.cmi 
-paramod.cmx: terms.cmx superposition.cmx pp.cmx nCicBlob.cmx index.cmx \
+paramod.cmx: superposition.cmx pp.cmx nCicBlob.cmx index.cmx foUtils.cmx \
     foUnif.cmx paramod.cmi 
diff --git a/helm/software/components/ng_paramodulation/.depend.opt b/helm/software/components/ng_paramodulation/.depend.opt
index 7fa534412..1dbf27b11 100644
--- a/helm/software/components/ng_paramodulation/.depend.opt
+++ b/helm/software/components/ng_paramodulation/.depend.opt
@@ -2,7 +2,7 @@ terms.cmi:
 pp.cmi: terms.cmi 
 foSubst.cmi: terms.cmi 
 orderings.cmi: terms.cmi 
-foUtils.cmi: terms.cmi 
+foUtils.cmi: terms.cmi index.cmi 
 foUnif.cmi: terms.cmi 
 index.cmi: terms.cmi 
 superposition.cmi: terms.cmi index.cmi 
@@ -17,8 +17,8 @@ foSubst.cmo: terms.cmi foSubst.cmi
 foSubst.cmx: terms.cmx foSubst.cmi 
 orderings.cmo: terms.cmi orderings.cmi 
 orderings.cmx: terms.cmx orderings.cmi 
-foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi 
-foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi 
+foUtils.cmo: terms.cmi orderings.cmi index.cmi foSubst.cmi foUtils.cmi 
+foUtils.cmx: terms.cmx orderings.cmx index.cmx foSubst.cmx foUtils.cmi 
 foUnif.cmo: terms.cmi foUtils.cmi foSubst.cmi foUnif.cmi 
 foUnif.cmx: terms.cmx foUtils.cmx foSubst.cmx foUnif.cmi 
 index.cmo: terms.cmi foUtils.cmi index.cmi 
@@ -31,7 +31,7 @@ nCicBlob.cmo: terms.cmi nCicBlob.cmi
 nCicBlob.cmx: terms.cmx nCicBlob.cmi 
 cicBlob.cmo: terms.cmi cicBlob.cmi 
 cicBlob.cmx: terms.cmx cicBlob.cmi 
-paramod.cmo: terms.cmi superposition.cmi pp.cmi nCicBlob.cmi index.cmi \
+paramod.cmo: superposition.cmi pp.cmi nCicBlob.cmi index.cmi foUtils.cmi \
     foUnif.cmi paramod.cmi 
-paramod.cmx: terms.cmx superposition.cmx pp.cmx nCicBlob.cmx index.cmx \
+paramod.cmx: superposition.cmx pp.cmx nCicBlob.cmx index.cmx foUtils.cmx \
     foUnif.cmx paramod.cmi 
diff --git a/helm/software/components/ng_paramodulation/Makefile b/helm/software/components/ng_paramodulation/Makefile
index d6a970b20..6fff2162c 100644
--- a/helm/software/components/ng_paramodulation/Makefile
+++ b/helm/software/components/ng_paramodulation/Makefile
@@ -2,7 +2,7 @@ PACKAGE = ng_paramodulation
 
 INTERFACE_FILES = \
 	terms.mli pp.mli foSubst.mli \
-	orderings.mli foUtils.mli foUnif.mli index.mli superposition.mli \
+	orderings.mli foUtils.mli index.mli foUnif.mli superposition.mli \
 	nCicBlob.mli cicBlob.mli paramod.mli
 
 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
diff --git a/helm/software/components/ng_paramodulation/cicBlob.ml b/helm/software/components/ng_paramodulation/cicBlob.ml
index c6cb31cfc..88ec26c2e 100644
--- a/helm/software/components/ng_paramodulation/cicBlob.ml
+++ b/helm/software/components/ng_paramodulation/cicBlob.ml
@@ -34,7 +34,8 @@ module CicBlob(C : CicContext) : Terms.Blob with type t = Cic.term = struct
 
   let embed t = assert false;;
 
-  let is_eq_predicate = assert false
-  let saturate = assert false 
+  let eqP = assert false;;
+
+  let saturate = assert false;;
 end
 
diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml
index 69e451e2e..d53b19c82 100644
--- a/helm/software/components/ng_paramodulation/foUtils.ml
+++ b/helm/software/components/ng_paramodulation/foUtils.ml
@@ -118,7 +118,7 @@ module Utils (B : Terms.Blob) = struct
     in
     let lit = 
       match ty with
-      | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.is_eq_predicate eq ->
+      | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq ->
            let o = Order.compare_terms l r in
            Terms.Equation (l, r, ty, o)
       | t -> Terms.Predicate t
@@ -127,4 +127,15 @@ module Utils (B : Terms.Blob) = struct
     fresh_unit_clause maxvar (mk_id (), lit, varlist, proof)
   ;;
 
+  let add_to_bag =
+  let id = ref 0 in
+  fun bag  (_,lit,vl,proof) ->
+    incr id;
+    let clause = (!id, lit, vl, proof) in
+    let bag = Terms.M.add !id clause bag in
+    bag, clause 
+   ;;
+    
+  let empty_bag = Terms.M.empty ;;
+
 end
diff --git a/helm/software/components/ng_paramodulation/foUtils.mli b/helm/software/components/ng_paramodulation/foUtils.mli
index 5d83a987d..4cddee8c1 100644
--- a/helm/software/components/ng_paramodulation/foUtils.mli
+++ b/helm/software/components/ng_paramodulation/foUtils.mli
@@ -27,6 +27,19 @@ module Utils (B : Terms.Blob) :
     val eq_unit_clause : B.t Terms.unit_clause -> B.t Terms.unit_clause -> bool
     val compare_unit_clause : B.t Terms.unit_clause -> B.t Terms.unit_clause -> int
 
+(*
     val fresh_unit_clause : 
           int -> B.t Terms.unit_clause -> B.t Terms.unit_clause * int
+*)
+
+    (* relocate [maxvar] [varlist] -> [newmaxvar] * [varlist] * [relocsubst] *)
+    val relocate : int -> int list -> int * int list * B.t Terms.substitution 
+
+    (* also gives a fresh ID to the clause *)
+    val add_to_bag : 
+          B.t Terms.bag -> B.t Terms.unit_clause -> 
+            B.t Terms.bag * B.t Terms.unit_clause
+
+    val empty_bag : B.t Terms.bag
+
   end
diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml
index ca30c9b50..6c26e7b86 100644
--- a/helm/software/components/ng_paramodulation/index.ml
+++ b/helm/software/components/ng_paramodulation/index.ml
@@ -79,4 +79,18 @@ module Index(B : Terms.Blob) = struct
       type dataset = ClauseSet.t
     = Make(FotermIndexable)(ClauseSet)
 
+  let index_unit_clause t = function
+    | (_,Terms.Equation (l,_,_,Terms.Gt),_,_) as c -> 
+          DT.index t l (Terms.Left2Right, c)
+    | (_,Terms.Equation (_,r,_,Terms.Lt),_,_) as c -> 
+          DT.index t r (Terms.Right2Left, c)
+    | (_,Terms.Equation (l,r,_,Terms.Incomparable),_,_) as c ->  
+          DT.index  
+           (DT.index t l (Terms.Left2Right, c))
+           r (Terms.Right2Left, c)
+    | (_,Terms.Equation (_,r,_,Terms.Eq),_,_)  -> assert false
+    | (_,Terms.Predicate p,_,_) as c ->
+          DT.index t p (Terms.Nodir, c)
+  ;;
+
 end
diff --git a/helm/software/components/ng_paramodulation/index.mli b/helm/software/components/ng_paramodulation/index.mli
index 3f86cc1e0..5581f7cfa 100644
--- a/helm/software/components/ng_paramodulation/index.mli
+++ b/helm/software/components/ng_paramodulation/index.mli
@@ -25,5 +25,8 @@ module Index (B : Terms.Blob) :
       type input = B.t Terms.foterm and 
       type data = ClauseSet.elt and 
       type dataset = ClauseSet.t
+    
+    val index_unit_clause :
+          DT.t -> B.t Terms.unit_clause -> DT.t 
 
   end
diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml
index a0fa80ada..7cd4e5762 100644
--- a/helm/software/components/ng_paramodulation/nCicBlob.ml
+++ b/helm/software/components/ng_paramodulation/nCicBlob.ml
@@ -63,7 +63,14 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
     proof, sty
   ;;
 
-  let is_eq_predicate t = assert false;;
+  let eqP = 
+    let r = 
+      OCic2NCic.reference_of_oxuri 
+       (UriManager.uri_of_string 
+         "cic:/matita/logic/equality/eq.ind#xpointer(1/1)")
+    in
+    NCic.Const r
+  ;;
 
 
  end
diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index 3da8477a9..66188c4d8 100644
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -58,7 +58,7 @@ module Orderings (B : Terms.Blob) = struct
     | Terms.Predicate t -> 
         let w, m = weight_of_term t in 
         weight_of_polynomial w m
-    | Terms.Equation (_,x,_,Terms.Lt)
+    | Terms.Equation (_,x,_,Terms.Lt) 
     | Terms.Equation (x,_,_,Terms.Gt) ->
         let w, m = weight_of_term x in 
         weight_of_polynomial w m
diff --git a/helm/software/components/ng_paramodulation/orderings.mli b/helm/software/components/ng_paramodulation/orderings.mli
index 74989c3eb..ccd6bf286 100644
--- a/helm/software/components/ng_paramodulation/orderings.mli
+++ b/helm/software/components/ng_paramodulation/orderings.mli
@@ -17,6 +17,7 @@ module Orderings (B : Terms.Blob) :
     (* This order relation should be:
      * - stable for instantiation
      * - total on ground terms
+     *
      *)
     val compare_terms : 
           B.t Terms.foterm -> B.t Terms.foterm -> Terms.comparison
diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index b1fc1c704..1bd9bcf4f 100644
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -1,4 +1,4 @@
-let nparamod metasenv subst context t =
+let nparamod metasenv subst context t table =
   let module C = struct
     let metasenv = metasenv
     let subst = subst
@@ -7,10 +7,11 @@ let nparamod metasenv subst context t =
   in
   let module B = NCicBlob.NCicBlob(C) in
   let module Pp = Pp.Pp (B) in
-  let res = B.embed t in
   let module FU = FoUnif.Founif(B) in
   let module IDX = Index.Index(B) in
   let module Sup = Superposition.Superposition(B) in
+  let module Utils = FoUtils.Utils(B) in
+(*
   let test_unification _ = function
     | Terms.Node [_; _; lhs; rhs] ->
 	prerr_endline "Unification test :";
@@ -24,4 +25,29 @@ let nparamod metasenv subst context t =
     prerr_endline (Pp.pp_foterm res);
     prerr_endline "Substitution :";
     prerr_endline (Pp.pp_substitution subst)
+*)
+  let mk_clause maxvar t =
+    let ty = B.embed t in
+    let proof = B.embed (NCic.Rel ~-1) in
+    Utils.mk_unit_clause maxvar ty proof 
+  in
+  let clause, maxvar = mk_clause 0 t in
+  prerr_endline "Input clause :";
+  prerr_endline (Pp.pp_unit_clause clause);
+  let bag = Utils.empty_bag in
+  let active_clauses, maxvar = 
+    List.fold_left
+      (fun (cl,maxvar) t -> 
+         let c, m = mk_clause maxvar t in
+         c::cl, m)
+      ([],maxvar) table 
+  in
+  let table =  
+    List.fold_left IDX.index_unit_clause IDX.DT.empty active_clauses
+  in
+  let bag, maxvar, newclauses = 
+    Sup.superposition_right_with_table bag maxvar clause table
+  in
+  prerr_endline "Output clauses :";
+  List.iter (fun c -> prerr_endline (Pp.pp_unit_clause c)) newclauses;
 ;;
diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli
index db112450d..78bea9934 100644
--- a/helm/software/components/ng_paramodulation/paramod.mli
+++ b/helm/software/components/ng_paramodulation/paramod.mli
@@ -1 +1,4 @@
-val nparamod : NCic.metasenv -> NCic.substitution -> NCic.context -> NCic.term -> unit
+val nparamod : 
+  NCic.metasenv -> NCic.substitution -> NCic.context -> 
+    NCic.term -> NCic.term list ->
+     unit
diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index b002dce33..64cc35bd4 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -17,11 +17,12 @@ module Superposition (B : Terms.Blob) =
     module Unif = FoUnif.Founif(B)
     module Subst = FoSubst.Subst(B)
     module Order = Orderings.Orderings(B)
+    module Utils = FoUtils.Utils(B)
 
-    let all_positions t f =
+    let all_positions pos ctx t f =
       let rec aux pos ctx = function
-      | Terms.Leaf a as t -> f t pos ctx 
-      | Terms.Var i -> []
+      | Terms.Leaf _ as t -> f t pos ctx 
+      | Terms.Var _ -> []
       | Terms.Node l as t-> 
           let acc, _, _ = 
             List.fold_left
@@ -34,7 +35,7 @@ module Superposition (B : Terms.Blob) =
           in
            acc
       in
-        aux [] (fun x -> x) t
+        aux pos ctx t
     ;;
 
     let superposition_right table varlist subterm pos context =
@@ -44,38 +45,85 @@ module Superposition (B : Terms.Blob) =
            match lit with
            | Terms.Predicate _ -> assert false
            | Terms.Equation (l,r,_,o) ->
+               assert(o <> Terms.Eq);
                let side, newside = if dir=Terms.Left2Right then l,r else r,l in
                try 
                  let subst, varlist = 
                    Unif.unification (varlist@vl) [] subterm side 
                  in
-                 Some (context newside, subst, varlist, id, pos, dir)
+                 if o = Terms.Incomparable then
+                   let side = Subst.apply_subst subst side in
+                   let newside = Subst.apply_subst subst newside in
+                   let o = Order.compare_terms side newside in
+                   (* XXX: check Riazanov p. 33 (iii) *)
+                   if o <> Terms.Lt && o <> Terms.Eq then  
+                     Some (context newside, subst, varlist, id, pos, dir)
+                   else 
+                     None
+                 else
+                   Some (context newside, subst, varlist, id, pos, dir)
                with FoUnif.UnificationFailure _ -> None)
         (IDX.ClauseSet.elements cands)
     ;;
 
-    let superposition_right_step bag (id,selected,vl,_) table =
+    let build_new_clause bag maxvar filter t subst vl id id2 pos dir =
+      let maxvar, vl, relocsubst = Utils.relocate maxvar vl in
+      let subst = Subst.concat relocsubst subst in
+      let proof = Terms.Step(Terms.SuperpositionRight,id,id2,dir,pos,subst) in
+      let t = Subst.apply_subst subst t in
+      if filter t then
+        let literal = 
+          match t with
+          | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq ->
+               let o = Order.compare_terms l r in
+               Terms.Equation (l, r, ty, o)
+          | t -> Terms.Predicate t
+        in
+        let bag, uc = 
+          Utils.add_to_bag bag (0, literal, vl, proof)
+        in
+        Some (bag, maxvar, uc)
+      else
+        None
+    ;;
+
+    let fold_build_new_clause bag maxvar id filter res =
+      let maxvar, bag, new_clauses = 
+        List.fold_left
+          (fun (maxvar, bag, acc) (t,subst,vl,id2,pos,dir) -> 
+             match build_new_clause bag maxvar filter t subst vl id id2 pos dir
+             with Some (bag, maxvar, uc) -> maxvar, bag, uc::acc
+                | None -> maxvar, bag, acc)
+          (maxvar, bag, []) res
+      in
+      bag, maxvar, new_clauses
+    ;;
+
+    let superposition_right_with_table bag maxvar (id,selected,vl,_) table =
       match selected with 
       | Terms.Predicate _ -> assert false
-      | Terms.Equation (l,r,ty,Terms.Lt) -> 
-          let res = all_positions r (superposition_right table vl) in
-          let _new_clauses = 
-            List.map
-              (fun (r,subst,vl,id2,pos,dir) -> 
-                 let proof = 
-                   Terms.Step(Terms.SuperpositionRight,id,id2, dir, pos, subst)
-                 in
-                 let r = Subst.apply_subst subst r in
-                 let l = Subst.apply_subst subst l in
-                 let ty = Subst.apply_subst subst ty in
-                 let o = Order.compare_terms l r in
-                 (* can unif compute the right vl for both sides? *)
-                 (0, Terms.Equation (l,r,ty,o), vl, proof))
-              res
-          in
-          (* fresh ID and metas and compute orientataion of new_clauses *)
-          assert false
-      | Terms.Equation (l,r,_,Terms.Gt) -> assert false
+      | Terms.Equation (l,r,ty,Terms.Lt) ->
+          fold_build_new_clause bag maxvar id (fun _ -> true)
+            (all_positions [3] 
+              (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
+              r (superposition_right table vl))          
+      | Terms.Equation (l,r,ty,Terms.Gt) ->
+          fold_build_new_clause bag maxvar id (fun _ -> true)
+            (all_positions [2] 
+              (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
+              l (superposition_right table vl))
+      | Terms.Equation (l,r,ty,Terms.Incomparable) -> 
+          fold_build_new_clause bag maxvar id
+            (function (* Riazanov: p.33 condition (iv) *)
+              | Terms.Node [Terms.Leaf eq; ty; l; r ] when B.eq B.eqP eq -> 
+                  Order.compare_terms l r <> Terms.Eq
+              | _ -> assert false)
+            ((all_positions [3] 
+               (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
+               r (superposition_right table vl)) @         
+             (all_positions [2] 
+               (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
+               l (superposition_right table vl)))
       | _ -> assert false
     ;;
           
diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli
index c2c0ef43d..b67233563 100644
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -15,11 +15,12 @@
 module Superposition (B : Terms.Blob) : 
   sig
 
-    val superposition_right_step :
+    val superposition_right_with_table :
           B.t Terms.bag -> 
+          int -> (* maxvar *)
           B.t Terms.unit_clause ->
           Index.Index(B).DT.t ->
-            B.t Terms.bag * B.t Terms.unit_clause list
+            B.t Terms.bag * int * B.t Terms.unit_clause list
                   
   end
 
diff --git a/helm/software/components/ng_paramodulation/terms.ml b/helm/software/components/ng_paramodulation/terms.ml
index 9b374a8a5..0e7bed7fb 100644
--- a/helm/software/components/ng_paramodulation/terms.ml
+++ b/helm/software/components/ng_paramodulation/terms.ml
@@ -63,7 +63,7 @@ module type Blob =
     type t
     val eq : t -> t -> bool
     val compare : t -> t -> int
-    val is_eq_predicate : t -> bool
+    val eqP : t
     val pp : t -> string
     val embed : t -> t foterm
     val saturate : t -> t -> t foterm * t foterm
diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli
index c16b6f9b7..d7f4b74e3 100644
--- a/helm/software/components/ng_paramodulation/terms.mli
+++ b/helm/software/components/ng_paramodulation/terms.mli
@@ -21,7 +21,10 @@ type 'a substitution = (int * 'a foterm) list
 type comparison = Lt | Eq | Gt | Incomparable
 
 type rule = SuperpositionRight | SuperpositionLeft | Demodulation
+
+(* A Discrimination tree is a map: foterm |-> (dir, clause) *)
 type direction = Left2Right | Right2Left | Nodir
+
 type position = int list
 
 type 'a proof =
@@ -51,7 +54,7 @@ type 'a passive_clause = int * 'a unit_clause (* weight * equation *)
 
 module M : Map.S with type key = int 
 
-type 'a bag = 'a unit_clause M.t
+type 'a bag = 'a unit_clause M.t 
 
 module type Blob =
   sig
@@ -62,7 +65,7 @@ module type Blob =
     type t
     val eq : t -> t -> bool
     val compare : t -> t -> int
-    val is_eq_predicate : t -> bool
+    val eqP : t
     (* TODO: consider taking in input an imperative buffer for Format 
      *  val pp : Format.formatter -> t -> unit
      * *)