X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matitaB%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;fp=matitaB%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=1152571cedb3e9c5d409f9da6fa6665555c22d54;hb=4f3b04e9966484011328d5b0eb358da4416e29b0;hp=42cf063b64f08b3e352693d7a30bebff78025e95;hpb=d0d2ebcf0ad48c38dcd69142f5e080e987fc5536;p=helm.git

diff --git a/matitaB/components/ng_paramodulation/superposition.ml b/matitaB/components/ng_paramodulation/superposition.ml
index 42cf063b6..1152571ce 100644
--- a/matitaB/components/ng_paramodulation/superposition.ml
+++ b/matitaB/components/ng_paramodulation/superposition.ml
@@ -27,7 +27,8 @@ module Superposition (B : Orderings.Blob) =
       * B.t Terms.substitution
 
     let print s = prerr_endline (Lazy.force s);; 
-    let debug _ = ();; 
+    let debug _ = ();;
+    (* let debug = print;; *) 
     let enable = true;;
 
     let rec list_first f = function
@@ -140,7 +141,7 @@ module Superposition (B : Orderings.Blob) =
       if filter subst then
         let literal = 
           match t with
-          | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP 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
@@ -281,12 +282,12 @@ module Superposition (B : Orderings.Blob) =
       | Terms.Equation (l,r,ty,_) ->
           let bag,l,id1 = 
 	    visit bag [2]
-            (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) id l
+            (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; x; r ]) id l
             (ctx_demod table vl)
 	  in 
 	  let bag,_,id2 = 
             visit bag [3]
-              (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) id1 r
+              (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; l; x ]) id1 r
               (ctx_demod table vl)
 	  in 
           let cl,_,_ = Terms.get_from_bag id2 bag in
@@ -310,7 +311,7 @@ module Superposition (B : Orderings.Blob) =
         match lit with
           | Terms.Predicate _ -> assert false
           | Terms.Equation (l,r,ty,_) ->
-              Terms.Node [Terms.Leaf B.eqP; ty; l ; r]
+              Terms.Node [Terms.Leaf (B.eqP()); ty; l ; r]
       in
         try ignore(Unif.alpha_eq (get_term cl1) (get_term cl2)) ; true
         with FoUnif.UnificationFailure _ -> false
@@ -379,11 +380,11 @@ module Superposition (B : Orderings.Blob) =
         let reverse = (dir = Terms.Left2Right) = b in
         let l, r, proof_rewrite_dir = if reverse then l,r,Terms.Left2Right
         else r,l, Terms.Right2Left in
-          (id,proof_rewrite_dir,Terms.Node [ Terms.Leaf B.eqP; ty; l; r ], vl)
+          (id,proof_rewrite_dir,Terms.Node [ Terms.Leaf (B.eqP()); ty; l; r ], vl)
       in
       let cands1 = List.map (f true) (IDX.ClauseSet.elements lcands) in
       let cands2 = List.map (f false) (IDX.ClauseSet.elements rcands) in
-      let t = Terms.Node [ Terms.Leaf B.eqP; ty; l; r ] in
+      let t = Terms.Node [ Terms.Leaf (B.eqP()); ty; l; r ] in
       let locked_vars = if unify then [] else vl in
       let rec aux = function
         | [] -> None
@@ -403,7 +404,7 @@ module Superposition (B : Orderings.Blob) =
           match rewrite_eq ~unify l r ty vl table with
             | None -> None
             | Some (id2, dir, subst) ->
-                let id_t = Terms.Node [ Terms.Leaf B.eqP; ty; r; r ] in
+                let id_t = Terms.Node [ Terms.Leaf (B.eqP()); ty; r; r ] in
                   build_new_clause bag maxvar (fun _ -> true)
                   Terms.Superposition id_t subst id id2 [2] dir 
     ;;
@@ -437,7 +438,7 @@ module Superposition (B : Orderings.Blob) =
                   let newsubst = Subst.concat subst1 subst in
                   let id_t = 
                     FoSubst.apply_subst newsubst
-                      (Terms.Node[Terms.Leaf B.eqP;ty;contextl r;contextr r]) 
+                      (Terms.Node[Terms.Leaf (B.eqP());ty;contextl r;contextr r]) 
                   in
                     (match 
                       build_new_clause_reloc bag maxvar (fun _ -> true)
@@ -714,14 +715,14 @@ module Superposition (B : Orderings.Blob) =
           fold_build_new_clause bag maxvar id Terms.Superposition
             (fun _ -> true)
             (all_positions [3] 
-              (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
+              (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; l; x ])
               r (superposition table vl))
       | Terms.Equation (l,r,ty,Terms.Invertible)
       | Terms.Equation (l,r,ty,Terms.Gt) ->
           fold_build_new_clause bag maxvar id Terms.Superposition
             (fun _ -> true)
             (all_positions [2] 
-              (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
+              (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; x; r ])
               l (superposition table vl))
       | Terms.Equation (l,r,ty,Terms.Incomparable) ->
 	  let filtering avoid subst = (* Riazanov: p.33 condition (iv) *)
@@ -734,14 +735,14 @@ module Superposition (B : Orderings.Blob) =
 	    fold_build_new_clause bag maxvar id Terms.Superposition
               (filtering Terms.Gt)
               (all_positions [3] 
-		 (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
+		 (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; l; x ])
 		 r (superposition table vl))
 	  in
 	  let bag, maxvar, l_terms =
 	    fold_build_new_clause bag maxvar id Terms.Superposition
               (filtering Terms.Lt)
               (all_positions [2] 
-		 (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
+		 (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; x; r ])
 		 l (superposition table vl))
 	  in
 	    bag, maxvar, r_terms @ l_terms