From: denes <??>
Date: Wed, 29 Jul 2009 16:17:28 +0000 (+0000)
Subject: Reorganized foUtils, added Clauses module to avoid duplicate code around are_invertib... 
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2041f4fefe300f77338f6aea598f025f84db1bbc;p=helm.git

Reorganized foUtils, added Clauses module to avoid duplicate code around are_invertible (in orderings)
---

diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend
index 6dc4150c1..489a80a1a 100644
--- a/helm/software/components/ng_paramodulation/.depend
+++ b/helm/software/components/ng_paramodulation/.depend
@@ -1,9 +1,10 @@
 pp.cmi: terms.cmi 
 foSubst.cmi: terms.cmi 
+foUtils.cmi: terms.cmi 
+foUnif.cmi: terms.cmi 
 orderings.cmi: terms.cmi 
-foUtils.cmi: terms.cmi orderings.cmi 
+clauses.cmi: orderings.cmi 
 index.cmi: terms.cmi orderings.cmi 
-foUnif.cmi: terms.cmi orderings.cmi 
 superposition.cmi: terms.cmi orderings.cmi index.cmi 
 stats.cmi: terms.cmi orderings.cmi 
 paramod.cmi: terms.cmi orderings.cmi 
@@ -16,22 +17,22 @@ pp.cmo: terms.cmi pp.cmi
 pp.cmx: terms.cmx pp.cmi 
 foSubst.cmo: terms.cmi foSubst.cmi 
 foSubst.cmx: terms.cmx foSubst.cmi 
-orderings.cmo: terms.cmi pp.cmi orderings.cmi 
-orderings.cmx: terms.cmx pp.cmx orderings.cmi 
-foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi 
-foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi 
-index.cmo: terms.cmi pp.cmi orderings.cmi foUtils.cmi foUnif.cmi foSubst.cmi \
-    index.cmi 
-index.cmx: terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx foSubst.cmx \
-    index.cmi 
-foUnif.cmo: terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi 
-foUnif.cmx: terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi 
+foUtils.cmo: terms.cmi foSubst.cmi foUtils.cmi 
+foUtils.cmx: terms.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 
+orderings.cmo: terms.cmi pp.cmi foUnif.cmi foSubst.cmi orderings.cmi 
+orderings.cmx: terms.cmx pp.cmx foUnif.cmx foSubst.cmx orderings.cmi 
+clauses.cmo: terms.cmi orderings.cmi foUtils.cmi foSubst.cmi clauses.cmi 
+clauses.cmx: terms.cmx orderings.cmx foUtils.cmx foSubst.cmx clauses.cmi 
+index.cmo: terms.cmi orderings.cmi foUtils.cmi index.cmi 
+index.cmx: terms.cmx orderings.cmx foUtils.cmx index.cmi 
 superposition.cmo: terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \
     foUnif.cmi foSubst.cmi superposition.cmi 
 superposition.cmx: terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \
     foUnif.cmx foSubst.cmx superposition.cmi 
-stats.cmo: terms.cmi stats.cmi 
-stats.cmx: terms.cmx stats.cmi 
+stats.cmo: terms.cmi pp.cmi stats.cmi 
+stats.cmx: terms.cmx pp.cmx stats.cmi 
 paramod.cmo: terms.cmi superposition.cmi pp.cmi orderings.cmi index.cmi \
     foUtils.cmi foUnif.cmi paramod.cmi 
 paramod.cmx: terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \
diff --git a/helm/software/components/ng_paramodulation/Makefile b/helm/software/components/ng_paramodulation/Makefile
index 6196ab1f9..0d2eef103 100644
--- a/helm/software/components/ng_paramodulation/Makefile
+++ b/helm/software/components/ng_paramodulation/Makefile
@@ -2,7 +2,8 @@ PACKAGE = ng_paramodulation
 
 INTERFACE_FILES = \
 	terms.mli pp.mli foSubst.mli \
-	orderings.mli foUtils.mli foUnif.mli index.mli superposition.mli \
+	foUtils.mli foUnif.mli orderings.mli \
+        clauses.mli index.mli superposition.mli \
 	stats.mli paramod.mli nCicBlob.mli cicBlob.mli nCicProof.mli \
 	nCicParamod.mli
 
diff --git a/helm/software/components/ng_paramodulation/foUnif.ml b/helm/software/components/ng_paramodulation/foUnif.ml
index 61bbdcd8b..916e33ca8 100644
--- a/helm/software/components/ng_paramodulation/foUnif.ml
+++ b/helm/software/components/ng_paramodulation/foUnif.ml
@@ -25,7 +25,7 @@ let mem2 a b l =
    aux false false l
 ;;
 
-module Founif (B : Orderings.Blob) = struct
+module FoUnif (B : Terms.Blob) = struct
   module Subst = FoSubst 
   module U = FoUtils.Utils(B)
 
diff --git a/helm/software/components/ng_paramodulation/foUnif.mli b/helm/software/components/ng_paramodulation/foUnif.mli
index 2371f2180..87792ec8c 100644
--- a/helm/software/components/ng_paramodulation/foUnif.mli
+++ b/helm/software/components/ng_paramodulation/foUnif.mli
@@ -13,7 +13,7 @@
 
 exception UnificationFailure of string Lazy.t;;
 
-module Founif (B : Orderings.Blob) : 
+module FoUnif (B : Terms.Blob) : 
   sig
 
    val unification:
diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml
index 7b192579d..5dd1268b0 100644
--- a/helm/software/components/ng_paramodulation/foUtils.ml
+++ b/helm/software/components/ng_paramodulation/foUtils.ml
@@ -21,9 +21,8 @@ let rec lexicograph f l1 l2 =
   | _,[] -> 1
 ;;
   
-module Utils (B : Orderings.Blob) = struct
+module Utils (B : Terms.Blob) = struct
   module Subst = FoSubst;; 
-  module Order = B;;
 
   let rec eq_foterm x y =
     x == y ||
@@ -69,9 +68,6 @@ module Utils (B : Orderings.Blob) = struct
     | Terms.Equation _, Terms.Predicate _ -> 1
   ;;
 
-  let eq_clause (id1,_,_,_,_) (id2,_,_,_,_) = id1 = id2
-  let compare_clause (id1,_,_,_,_) (id2,_,_,_,_) = Pervasives.compare id1 id2
-    
   let relocate maxvar varlist subst =
     List.fold_right
       (fun i (maxvar, varlist, s) -> 
@@ -79,61 +75,4 @@ module Utils (B : Orderings.Blob) = struct
       varlist (maxvar+1, [], subst)
   ;;
 
-  let fresh_clause maxvar (id, nlit, plit, varlist, proof) =
-    let maxvar, varlist, subst = relocate maxvar varlist Subst.id_subst in
-    let apply_subst_on_lit = function
-      | Terms.Equation (l,r,ty,o) ->
-          let l = Subst.apply_subst subst l in
-          let r = Subst.apply_subst subst r in
-          let ty = Subst.apply_subst subst ty in
-          Terms.Equation (l,r,ty,o)
-      | Terms.Predicate p ->
-          let p = Subst.apply_subst subst p in
-          Terms.Predicate p
-    in
-    let nlit = List.map (fun (l,s) -> (apply_subst_on_lit l,s)) nlit in
-    let plit = List.map (fun (l,s) -> (apply_subst_on_lit l,s)) plit in
-    let proof =
-      match proof with
-      | Terms.Exact t -> Terms.Exact (Subst.apply_subst subst t)
-      | Terms.Step (rule,c1,c2,dir,pos,s) ->
-          Terms.Step(rule,c1,c2,dir,pos,Subst.concat subst s)
-    in
-     (id, nlit, plit, varlist, proof), maxvar
-  ;;
-
-  (* may be moved inside the bag *)
-  let mk_clause maxvar nlit plit proofterm =
-    let foterm_to_lit (acc,literals) ty =
-      let vars = Terms.vars_of_term ~start_acc:acc ty in
-      match ty with
-      | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq ->
-           let o = Order.compare_terms l r in
-           (vars,(Terms.Equation (l, r, ty, o),true)::literals)
-      | _ -> (vars,(Terms.Predicate ty,true)::literals)
-    in
-    let varlist = Terms.vars_of_term proofterm in
-    let (varlist,nlit) = List.fold_left foterm_to_lit (varlist,[]) nlit in
-    let (varlist,plit) = List.fold_left foterm_to_lit (varlist,[]) plit in
-    let proof = Terms.Exact proofterm in
-    fresh_clause maxvar (0, nlit, plit, varlist, proof)
-  ;;
-
-  let mk_passive_clause cl =
-    (Order.compute_clause_weight cl, cl)
-  ;;
-
-  let mk_passive_goal g =
-    (Order.compute_clause_weight g, g)
-  ;;
-
-  let compare_passive_clauses_weight (w1,(id1,_,_,_,_)) (w2,(id2,_,_,_,_)) =
-    if w1 = w2 then id1 - id2
-    else w1 - w2
-  ;;
-
-  let compare_passive_clauses_age (_,(id1,_,_,_,_)) (_,(id2,_,_,_,_)) =
-    id1 - id2
-  ;;
-
 end
diff --git a/helm/software/components/ng_paramodulation/foUtils.mli b/helm/software/components/ng_paramodulation/foUtils.mli
index 48ef1d90b..fcb94c22e 100644
--- a/helm/software/components/ng_paramodulation/foUtils.mli
+++ b/helm/software/components/ng_paramodulation/foUtils.mli
@@ -13,7 +13,7 @@
 
 val lexicograph : ('a -> 'b -> int) -> 'a list -> 'b list -> int
 
-module Utils (B : Orderings.Blob) :
+module Utils (B : Terms.Blob) :
   sig
     val eq_foterm : B.t Terms.foterm -> B.t Terms.foterm -> bool
     val compare_foterm : B.t Terms.foterm -> B.t Terms.foterm -> int
@@ -21,36 +21,7 @@ module Utils (B : Orderings.Blob) :
     val eq_literal : B.t Terms.literal -> B.t Terms.literal -> bool
     val compare_literal : B.t Terms.literal -> B.t Terms.literal -> int
 
-    (* mk_clause [maxvar] [type] [proof] -> [clause] * [maxvar] *)
-    val mk_clause : 
-      int ->
-      B.t Terms.foterm list -> (* negative literals in clause *)
-      B.t Terms.foterm list -> (* positive literals in clause *)
-      B.t Terms.foterm -> 
-      B.t Terms.clause * int
-
-    val mk_passive_clause :
-      B.t Terms.clause -> B.t Terms.passive_clause
-
-    val mk_passive_goal :
-      B.t Terms.clause -> B.t Terms.passive_clause
-
-    val eq_clause : B.t Terms.clause -> B.t Terms.clause -> bool
-    val compare_clause : B.t Terms.clause -> B.t Terms.clause -> int
-
-
-    val fresh_clause : 
-          int -> B.t Terms.clause -> B.t Terms.clause * int
-
-    (* relocate [maxvar] [varlist] -> [newmaxvar] * [varlist] * [relocsubst] *)
-    val relocate : 
-          int -> int list -> B.t Terms.substitution -> 
-            int * int list * B.t Terms.substitution 
-
-    val compare_passive_clauses_weight :
-      B.t Terms.passive_clause -> B.t Terms.passive_clause -> int
-
-    val compare_passive_clauses_age :
-      B.t Terms.passive_clause -> B.t Terms.passive_clause -> int
+    val relocate : int -> int list -> B.t Terms.substitution 
+                       -> int * int list * B.t Terms.substitution
 
   end
diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml
index beb3aed86..e44d79131 100644
--- a/helm/software/components/ng_paramodulation/index.ml
+++ b/helm/software/components/ng_paramodulation/index.ml
@@ -13,6 +13,7 @@
 
 module Index(B : Orderings.Blob) = struct
   module U = FoUtils.Utils(B)
+  module Clauses = Clauses.Clauses(B)
 
   module ClauseOT =
     struct 
@@ -23,7 +24,7 @@ module Index(B : Orderings.Blob) = struct
  
       let compare (d1,p1,pos1,uc1) (d2,p2,pos2,uc2) = 
         let c = Pervasives.compare (d1,p1,pos1) (d2,p2,pos2) in
-        if c <> 0 then c else U.compare_clause uc1 uc2
+        if c <> 0 then c else Clauses.compare_clause uc1 uc2
       ;;
     end
 
diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index 47f6b4512..89b390b07 100644
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -186,58 +186,25 @@ let compare_terms o x y =
       | _ -> assert false
 ;;
 
+let are_invertible relocate alpha_eq l r =
+    let varlist = Terms.vars_of_term l in
+    let maxvar = List.fold_left max 0 varlist in
+    let _,_,subst = relocate maxvar varlist FoSubst.id_subst in
+    let l = FoSubst.apply_subst subst l in
+      try (ignore(alpha_eq l r);true) with
+	  FoUnif.UnificationFailure _ -> false;;
+
 module NRKBO (B : Terms.Blob) = struct
   let name = "nrkbo"
   include B 
 
   module Pp = Pp.Pp(B)
+  module Unif = FoUnif.FoUnif(B)
+  module Utils = FoUtils.Utils(B)
 
   let eq_foterm = eq_foterm B.eq;;
 
-exception UnificationFailure of string Lazy.t;;
-
-
-(* DUPLICATE CODE FOR TESTS (see FoUnif)  *)
-  let alpha_eq s t =
-    let rec equiv subst s t =
-      let s = match s with Terms.Var i -> FoSubst.lookup i subst | _ -> s
-      and t = match t with Terms.Var i -> FoSubst.lookup i subst | _ -> t
-        
-      in
-      match s, t with
-        | s, t when eq_foterm s t -> subst
-        | Terms.Var i, Terms.Var j
-            when (not (List.exists (fun (_,k) -> k=t) subst)) ->
-            let subst = FoSubst.build_subst i t subst in
-              subst
-        | Terms.Node l1, Terms.Node l2 -> (
-            try
-              List.fold_left2
-                (fun subst' s t -> equiv subst' s t)
-                subst l1 l2
-            with Invalid_argument _ ->
-              raise (UnificationFailure (lazy "Inference.unification.unif"))
-          )
-        | _, _ ->
-            raise (UnificationFailure (lazy "Inference.unification.unif"))
-    in
-      equiv FoSubst.id_subst s t
-;;
-
-let relocate maxvar varlist subst =
-    List.fold_right
-      (fun i (maxvar, varlist, s) -> 
-         maxvar+1, maxvar::varlist, FoSubst.build_subst i (Terms.Var maxvar) s)
-      varlist (maxvar+1, [], subst)
-  ;;
-
-  let are_invertible l r =
-    let varlist = Terms.vars_of_term l in
-    let maxvar = List.fold_left max 0 varlist in
-    let _,_,subst = relocate maxvar varlist FoSubst.id_subst in
-    let l = FoSubst.apply_subst subst l in
-      try (ignore(alpha_eq l r);true) with
-	  UnificationFailure _ -> false
+  let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;;
 
   let compute_clause_weight = compute_clause_weight;;
   
@@ -270,9 +237,13 @@ module KBO (B : Terms.Blob) = struct
   include B 
 
   module Pp = Pp.Pp(B)
+  module Unif = FoUnif.FoUnif(B)
+  module Utils = FoUtils.Utils(B)
 
   let eq_foterm = eq_foterm B.eq;;
 
+  let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;;
+
   let compute_clause_weight = compute_clause_weight;;
   let compute_goal_weight = compute_goal_weight;;
 
@@ -336,9 +307,13 @@ module LPO (B : Terms.Blob) = struct
   include B 
 
   module Pp = Pp.Pp(B)
+  module Unif = FoUnif.FoUnif(B)
+  module Utils = FoUtils.Utils(B)
 
   let eq_foterm = eq_foterm B.eq;;
 
+  let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;;
+
   let compute_clause_weight = compute_clause_weight;;
   let compute_goal_weight = compute_goal_weight;;
 
diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 8024dbba0..1f64314c9 100644
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -43,21 +43,22 @@ module Paramod (B : Orderings.Blob) = struct
   exception Stop of szsontology
   type bag = B.t Terms.bag * int
   module Pp = Pp.Pp (B) 
-  module FU = FoUnif.Founif(B) 
+  module FU = FoUnif.FoUnif(B) 
   module IDX = Index.Index(B) 
   module Sup = Superposition.Superposition(B) 
   module Utils = FoUtils.Utils(B) 
   module Order = B
+  module Clauses = Clauses.Clauses(B)
   module WeightOrderedPassives =
       struct
         type t = B.t Terms.passive_clause
-        let compare = Utils.compare_passive_clauses_weight
+        let compare = Clauses.compare_passive_clauses_weight
       end
 
   module AgeOrderedPassives =
       struct
         type t = B.t Terms.passive_clause
-        let compare = Utils.compare_passive_clauses_age
+        let compare = Clauses.compare_passive_clauses_age
       end
   
   module WeightPassiveSet = Set.Make(WeightOrderedPassives)
@@ -65,13 +66,13 @@ module Paramod (B : Orderings.Blob) = struct
 
   let add_passive_clause ?(no_weight=false) (passives_w,passives_a) cl =
     let cl = if no_weight then (0,cl)
-    else Utils.mk_passive_clause cl in
+    else Clauses.mk_passive_clause cl in
     WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a
   ;;
 
   let add_passive_goal ?(no_weight=false) (passives_w,passives_a) g =
     let g = if no_weight then (0,g)
-    else Utils.mk_passive_goal g in
+    else Clauses.mk_passive_goal g in
     WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a
   ;;
 
@@ -337,7 +338,7 @@ module Paramod (B : Orderings.Blob) = struct
     let bag = Terms.empty_bag in
     let maxvar = 0 in
     let build_clause (bag,maxvar,l) (t,(nlit,plit)) =
-      let c,maxvar = Utils.mk_clause maxvar nlit plit t in
+      let c,maxvar = Clauses.mk_clause maxvar nlit plit t in
       let bag,c = Terms.add_to_bag c bag in
       (bag,maxvar,c::l)
     in
diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 306104658..47119d477 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -14,11 +14,12 @@
 module Superposition (B : Orderings.Blob) = 
   struct
     module IDX = Index.Index(B)
-    module Unif = FoUnif.Founif(B)
+    module Unif = FoUnif.FoUnif(B)
     module Subst = FoSubst 
     module Order = B
     module Utils = FoUtils.Utils(B)
     module Pp = Pp.Pp(B)
+    module Clauses = Clauses.Clauses(B)
     
     exception Success of B.t Terms.bag * int * B.t Terms.clause
 
@@ -688,7 +689,7 @@ module Superposition (B : Orderings.Blob) =
         current :: alist, IDX.index_clause atable current
       in
         debug (lazy "Indexed");
-      let fresh_current, maxvar = Utils.fresh_clause maxvar current in
+      let fresh_current, maxvar = Clauses.fresh_clause maxvar current in
         (* We need to put fresh_current into the bag so that all *
          * variables clauses refer to are known.                 *)
       let bag, fresh_current = Terms.add_to_bag fresh_current bag in