2: is_identity -> is_weak_identity

[helm.git] / helm / software / components / tactics / paramodulation / indexing.ml

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index 0b3ec04a8176d53b9af64b0e384bab55f090b3fb..ff5bf23cbbaae16548a4dd6a643fa089856ec96c 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -151,11 +151,11 @@ let check_target bag context target msg =
 (*
   try 
       ignore(CicTypeChecker.type_of_aux'
-        metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph)
+        metas context (Founif.build_proof_term proof) CicUniv.empty_ugraph)
   with e ->  
       prerr_endline msg;
-      prerr_endline (Inference.string_of_proof proof);
-      prerr_endline (CicPp.ppterm (Inference.build_proof_term proof));
+      prerr_endline (Founif.string_of_proof proof);
+      prerr_endline (CicPp.ppterm (Founif.build_proof_term proof));
       prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left));
       prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right)); 
       raise e 
@@ -246,7 +246,7 @@ let rec find_matches bag metasenv context ugraph lift_amount term termty =
         ) else
           let do_match c =
             let subst', metasenv', ugraph' =
-              Inference.matching 
+              Founif.matching 
                 metasenv metas context term (S.lift lift_amount c) ugraph
             in
             Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate)
@@ -259,7 +259,7 @@ let rec find_matches bag metasenv context ugraph lift_amount term termty =
             let res =
               try
                 do_match c 
-              with Inference.MatchingFailure ->
+              with Founif.MatchingFailure ->
                 find_matches bag metasenv context ugraph lift_amount term termty tl
             in
               if Utils.debug_res then ignore (check_res res "find1");
@@ -267,7 +267,7 @@ let rec find_matches bag metasenv context ugraph lift_amount term termty =
           else
             let res =
               try do_match c 
-              with Inference.MatchingFailure -> None
+              with Founif.MatchingFailure -> None
             in
             if Utils.debug_res then ignore (check_res res "find2");
             match res with
@@ -292,9 +292,9 @@ let find_matches metasenv context ugraph lift_amount term termty =
 
 (*
   as above, but finds all the matching equalities, and the matching condition
-  can be either Inference.matching or Inference.unification
+  can be either Founif.matching or Inference.unification
 *)
-let rec find_all_matches ?(unif_fun=Inference.unification)
+let rec find_all_matches ?(unif_fun=Founif.unification)
     metasenv context ugraph lift_amount term termty =
   let module C = Cic in
   let module U = Utils in
@@ -323,7 +323,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
             res::(find_all_matches ~unif_fun metasenv context ugraph
                     lift_amount term termty tl)
           with
-          | Inference.MatchingFailure
+          | Founif.MatchingFailure
           | CicUnification.UnificationFailure _
           | CicUnification.Uncertain _ ->
               find_all_matches ~unif_fun metasenv context ugraph
@@ -343,7 +343,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
                   find_all_matches ~unif_fun metasenv context ugraph
                     lift_amount term termty tl
           with
-          | Inference.MatchingFailure
+          | Founif.MatchingFailure
           | CicUnification.UnificationFailure _
           | CicUnification.Uncertain _ ->
               find_all_matches ~unif_fun metasenv context ugraph
@@ -356,7 +356,7 @@ let find_all_matches
     find_all_matches 
       ?unif_fun metasenv context ugraph lift_amount term termty l 
   (*prerr_endline "CANDIDATES:";
-  List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l;
+  List.iter (fun (_,x)->prerr_endline (Founif.string_of_equality x)) l;
   prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
   (List.length rc));*)
 ;;
@@ -374,9 +374,9 @@ let subsumption_aux use_unification env table target =
   let metasenv = tmetas in
   let predicate, unif_fun = 
     if use_unification then
-      Unification, Inference.unification
+      Unification, Founif.unification
     else
-      Matching, Inference.matching
+      Matching, Founif.matching
   in
   let leftr =
     match left with
@@ -401,7 +401,7 @@ let subsumption_aux use_unification env table target =
           | None -> ok what leftorright tl
           | Some s -> Some (s, equation, leftorright <> pos ))
         with 
-        | Inference.MatchingFailure 
+        | Founif.MatchingFailure 
         | CicUnification.UnificationFailure _ -> ok what leftorright tl
   in
   match ok right Utils.Left  leftr with
@@ -592,15 +592,17 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target =
     !maxmeta, res 
   in
 
-  let res = demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left in
+  let res = 
+    demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left 
+  in
   if Utils.debug_res then check_res res "demod result";
   let newmeta, newtarget = 
     match res with
     | Some t ->
         let newmeta, newtarget = build_newtarget true t in
           assert (not (Equality.meta_convertibility_eq target newtarget));
-          if (Equality.is_weak_identity newtarget) ||
-            (Equality.meta_convertibility_eq target newtarget) then
+          if (Equality.is_weak_identity newtarget) (* || *)
+            (*Equality.meta_convertibility_eq target newtarget*) then
               newmeta, newtarget
           else 
             demodulation_equality bag ?from eq_uri newmeta env table newtarget
@@ -822,7 +824,7 @@ let superposition_right bag
         if ordering = U.Gt then newgoal, apply_subst s right
         else apply_subst s left, newgoal in
       let neworder = !Utils.compare_terms left right in
-      let newmenv = (* Inference.filter s *) m in
+      let newmenv = (* Founif.filter s *) m in
       let stat = (eq_ty, left, right, neworder) in
       let eq' =
         let w = Utils.compute_equality_weight stat in
@@ -841,7 +843,7 @@ let superposition_right bag
   in
   let new1 = List.map (build_new U.Gt) res1
   and new2 = List.map (build_new U.Lt) res2 in
-  let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
+  let ok e = not (Equality.is_weak_identity (*metasenv', context, ugraph*) e) in
   (!maxmeta,
    (List.filter ok (new1 @ new2)))
 ;;
@@ -951,7 +953,7 @@ let build_newgoal bag context goal posu rule expansion =
     let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
     bo, (newgoalproofstep::goalproof)
   in
-  let newmetasenv = (* Inference.filter subst *) menv in
+  let newmetasenv = (* Founif.filter subst *) menv in
   (newgoalproof, newmetasenv, newterm)
 ;;