(* $Id: index.mli 9822 2009-06-03 15:37:06Z tassi $ *)
-module Superposition (B : Terms.Blob) =
+module Superposition (B : Orderings.Blob) =
struct
module IDX = Index.Index(B)
module Unif = FoUnif.Founif(B)
module Subst = FoSubst
- module Order = Orderings.Orderings(B)
+ module Order = B
module Utils = FoUtils.Utils(B)
module Pp = Pp.Pp(B)
let prof_demod_u = HExtlib.profile ~enable "demod.unify";;
let prof_demod_r = HExtlib.profile ~enable "demod.retrieve_generalizations";;
let prof_demod_o = HExtlib.profile ~enable "demod.compare_terms";;
+ let prof_demod_s = HExtlib.profile ~enable "demod.apply_subst";;
let demod table varlist subterm =
let cands =
try
let subst =
prof_demod_u.HExtlib.profile
- (Unif.unification (varlist@vl) varlist subterm) side
+ (Unif.unification (* (varlist@vl) *) varlist subterm) side
in
- let side = Subst.apply_subst subst side in
- let newside = Subst.apply_subst subst newside in
+ let side =
+ prof_demod_s.HExtlib.profile
+ (Subst.apply_subst subst) side
+ in
+ let newside =
+ prof_demod_s.HExtlib.profile
+ (Subst.apply_subst subst) newside
+ in
if o = Terms.Incomparable then
let o =
prof_demod_o.HExtlib.profile
let is_identity_clause ~unify = function
| _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> true
| _, Terms.Equation (l,r,_,_), vl, proof when unify ->
- (try ignore(Unif.unification vl [] l r); true
+ (try ignore(Unif.unification (* vl *) [] l r); true
with FoUnif.UnificationFailure _ -> false)
| _, Terms.Equation (_,_,_,_), _, _ -> false
| _, Terms.Predicate _, _, _ -> assert false
| [] -> None
| (id2,dir,c,vl1)::tl ->
try
- let subst = Unif.unification (vl@vl1) locked_vars c t in
+ let subst = Unif.unification (* (vl@vl1) *) locked_vars c t in
Some (id2, dir, subst)
with FoUnif.UnificationFailure _ -> aux tl
in
let l = Subst.apply_subst subst l in
let r = Subst.apply_subst subst r in
try
- let subst1 = Unif.unification vl [] l r in
+ let subst1 = Unif.unification (* vl *) [] l r in
let lit =
match lit with Terms.Predicate _ -> assert false
| Terms.Equation (l,r,ty,o) ->
let side, newside = if dir=Terms.Left2Right then l,r else r,l in
try
let subst =
- Unif.unification (varlist@vl) [] subterm side
+ Unif.unification (* (varlist@vl)*) [] subterm side
in
if o = Terms.Incomparable then
let side = Subst.apply_subst subst side in