fixed LetIn proofs

[helm.git] / components / tactics / paramodulation / inference.ml

diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml
index f088d54543aa265f6550e53bf0552f886c409e8f..ab27f8a314b13e4b75cce13afbd272a7f9440475 100644 (file)
--- a/components/tactics/paramodulation/inference.ml
+++ b/components/tactics/paramodulation/inference.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+let _profiler = <:profiler<_profiler>>;;
+
 (* $Id$ *)
 
 open Utils;;
@@ -30,7 +32,7 @@ open Printf;;
 
 let check_disjoint_invariant subst metasenv msg =
   if (List.exists 
-        (fun (i,_,_) -> (Equality.is_in_subst i subst)) metasenv)
+        (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv)
   then 
     begin 
       prerr_endline ("not disjoint: " ^ msg);
@@ -65,7 +67,7 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph =
   let module C = Cic in
   let module M = CicMetaSubst in
   let module U = CicUnification in
-  let lookup = Equality.lookup_subst in
+  let lookup = Subst.lookup_subst in
   let rec occurs_check subst what where =
     match where with
     | t when what = t -> true
@@ -99,8 +101,8 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph =
     | C.Meta (i, l), t -> (
         try
           let _, _, ty = CicUtil.lookup_meta i menv in
-          assert (not (Equality.is_in_subst i subst));
-          let subst = Equality.buildsubst i context t ty subst in
+          assert (not (Subst.is_in_subst i subst));
+          let subst = Subst.buildsubst i context t ty subst in
           let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *)
           subst, menv
         with CicUtil.Meta_not_found m ->
@@ -126,8 +128,8 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph =
     | _, _ ->
         raise (U.UnificationFailure (lazy "Inference.unification.unif"))
   in
-  let subst, menv = unif Equality.empty_subst metasenv t1 t2 in
-  let menv = Equality.filter subst menv in
+  let subst, menv = unif Subst.empty_subst metasenv t1 t2 in
+  let menv = Subst.filter subst menv in
   subst, menv, ugraph
 ;;
 
@@ -144,7 +146,7 @@ let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
         (lazy
            (Printf.sprintf "NOT SIMPLE TERMS: %s %s"
               (CicPp.ppterm t1) (CicPp.ppterm t2)));
-      raise (CicUnification .UnificationFailure (lazy "Inference.unification.unif"))
+      raise (CicUnification.UnificationFailure (lazy "Inference.unification.unif"))
     ) else
       if b then
         (* full unification *)
@@ -170,22 +172,24 @@ let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
 
 exception MatchingFailure;;
 
-let matching1 metasenv1 metasenv2 context t1 t2 ugraph = 
+(** matching takes in input the _disjoint_ metasenv of t1 and  t2;
+it perform unification in the union metasenv, then check that
+the first metasenv has not changed *)
+let matching metasenv1 metasenv2 context t1 t2 ugraph = 
   try 
     unification_aux false metasenv1 metasenv2 context t1 t2 ugraph
   with
-    CicUnification .UnificationFailure _ ->
+    CicUnification.UnificationFailure _ -> 
       raise MatchingFailure
 ;;
 
-let unification = unification_aux true 
+let unification m1 m2 c t1 t2 ug = 
+  try 
+    unification_aux true m1 m2 c t1 t2 ug
+  with exn -> 
+    raise exn
 ;;
 
-(** matching takes in input the _disjoint_ metasenv of t1 and  t2;
-it perform unification in the union metasenv, then check that
-the first metasenv has not changed *)
-
-let matching = matching1;;
 
 let check_eq context msg eq =
   let w, proof, (eq_ty, left, right, order), metas = eq in
@@ -234,10 +238,7 @@ let find_equalities context proof =
                     let o = !Utils.compare_terms t1 t2 in
                     let stat = (ty,t1,t2,o) in
                     let w = compute_equality_weight stat in
-                    let proof_old = 
-                      Equality.BasicProof (Equality.empty_subst,p) in
-                    let proof_new = Equality.Exact p in
-                    let proof = proof_new , proof_old in
+                    let proof = Equality.Exact p in
                     let e = Equality.mk_equality (w, proof, stat, newmetas) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
@@ -251,9 +252,7 @@ let find_equalities context proof =
               let stat = (ty,t1,t2,o) in
               let w = compute_equality_weight stat in
               let p = C.Rel index in
-              let proof_old = Equality.BasicProof (Equality.empty_subst,p) in
-              let proof_new = Equality.Exact p in
-              let proof = proof_new, proof_old in
+              let proof = Equality.Exact p in
               let e = Equality.mk_equality (w, proof,stat,[]) in
               Some e, (newmeta+1)
           | _ -> None, newmeta
@@ -391,10 +390,7 @@ let find_library_equalities dbd context status maxmeta =
                     let o = !Utils.compare_terms t1 t2 in
                     let stat = (ty,t1,t2,o) in
                     let w = compute_equality_weight stat in
-                    let proof_old = 
-                      Equality.BasicProof (Equality.empty_subst,p) in
-                    let proof_new = Equality.Exact p in
-                    let proof = proof_new, proof_old in
+                    let proof = Equality.Exact p in
                     let e = Equality.mk_equality (w, proof, stat, newmetas) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
@@ -404,9 +400,7 @@ let find_library_equalities dbd context status maxmeta =
               let o = !Utils.compare_terms t1 t2 in
               let stat = (ty,t1,t2,o) in
               let w = compute_equality_weight stat in
-              let old_proof = Equality.BasicProof (Equality.empty_subst,term) in
-              let new_proof = Equality.Exact term in 
-              let proof = new_proof, old_proof in
+              let proof = Equality.Exact term in 
               let e = Equality.mk_equality (w, proof, stat, []) in
               Some e, (newmeta+1)
           | _ -> None, newmeta
@@ -495,3 +489,4 @@ let find_context_hypotheses env equalities_indexes =
   res
 ;;
 
+let get_stats () = <:show<Inference.>> ;;