- some fixes regarding URIs of equality that now should be coherent with the

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

diff --git a/helm/software/components/tactics/paramodulation/inference.ml b/helm/software/components/tactics/paramodulation/inference.ml
index 6004de44ceb29ef815daf390b824678aa8863ef3..e2f85fa2b4acce69dfa6604b1c92799234771bf1 100644 (file)
--- a/helm/software/components/tactics/paramodulation/inference.ml
+++ b/helm/software/components/tactics/paramodulation/inference.ml
@@ -211,7 +211,6 @@ let find_equalities context proof =
   let module C = Cic in
   let module S = CicSubstitution in
   let module T = CicTypeChecker in
-  let eq_uri = Utils.eq_URI () in
   let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
   let ok_types ty menv =
     List.for_all (fun (_, _, mt) -> mt = ty) menv
@@ -234,7 +233,8 @@ let find_equalities context proof =
               in (
                 match head with
                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
-                    when (UriManager.eq uri eq_uri) && (ok_types ty newmetas) ->
+                    when (LibraryObjects.is_eq_URI uri) && 
+                         (ok_types ty newmetas) ->
                     debug_print
                       (lazy
                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
@@ -247,7 +247,7 @@ let find_equalities context proof =
                 | _ -> None, newmeta
               )
           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
-              when UriManager.eq uri eq_uri ->
+              when LibraryObjects.is_eq_URI uri ->
               let ty = S.lift index ty in
               let t1 = S.lift index t1 in
               let t2 = S.lift index t2 in
@@ -315,43 +315,39 @@ let equations_blacklist =
 *)
 let equations_blacklist = UriManager.UriSet.empty;;
 
+let tty_of_u u = 
+  let _ = <:start<tty_of_u>> in
+  let t = CicUtil.term_of_uri u in
+  let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
+  let _ = <:stop<tty_of_u>> in
+  t, ty
+;;
+
+let utty_of_u u =
+  let t,ty = tty_of_u u in
+  u, t, ty
+;;
 
 let find_library_equalities dbd context status maxmeta = 
   let module C = Cic in
   let module S = CicSubstitution in
   let module T = CicTypeChecker in
-  let blacklist =
-    List.fold_left
-      (fun s u -> UriManager.UriSet.add u s)
-      equations_blacklist
-      [eq_XURI (); sym_eq_URI (); trans_eq_URI (); eq_ind_URI ();
-       eq_ind_r_URI ()]
-  in
+  let _ = <:start<equations_for_goal>> in
+  let eqs = (MetadataQuery.equations_for_goal ~dbd status) in
+  let _ = <:stop<equations_for_goal>> in
   let candidates =
     List.fold_left
       (fun l uri ->
-         if UriManager.UriSet.mem uri blacklist then
+        if LibraryObjects.is_eq_refl_URI uri ||
+           LibraryObjects.is_sym_eq_URI uri ||
+           LibraryObjects.is_trans_eq_URI uri ||
+           LibraryObjects.is_eq_ind_URI uri ||
+           LibraryObjects.is_eq_ind_r_URI uri 
+         then 
            l
          else
-           let t = CicUtil.term_of_uri uri in
-           let ty, _ =
-             CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph
-           in
-           (uri, t, ty)::l)
-      []
-      (let t1 = Unix.gettimeofday () in
-       let eqs = (MetadataQuery.equations_for_goal ~dbd status) in
-       let t2 = Unix.gettimeofday () in
-       (debug_print
-          (lazy
-             (Printf.sprintf "Tempo di MetadataQuery.equations_for_goal: %.9f\n"
-                (t2 -. t1))));
-       eqs)
-  in
-  let eq_uri1 = eq_XURI ()
-  and eq_uri2 = Utils.eq_URI () in
-  let iseq uri =
-    (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2)
+           (utty_of_u uri)::l)
+      [] eqs
   in
   let ok_types ty menv =
     List.for_all (fun (_, _, mt) -> mt = ty) menv
@@ -386,7 +382,9 @@ let find_library_equalities dbd context status maxmeta =
               in (
                   match head with
                     | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
-                        when (iseq uri) && (ok_types ty newmetas) ->
+                        when (LibraryObjects.is_eq_URI uri ||
+                              LibraryObjects.is_eq_refl_URI uri) && 
+                             (ok_types ty newmetas) ->
                     debug_print
                       (lazy
                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
@@ -399,7 +397,10 @@ let find_library_equalities dbd context status maxmeta =
                 | _ -> None, newmeta
               )
           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
-              when iseq uri && not (has_vars termty) ->
+              when 
+                (LibraryObjects.is_eq_URI uri || 
+                 LibraryObjects.is_eq_refl_URI uri) && 
+                not (has_vars termty) ->
               let o = !Utils.compare_terms t1 t2 in
               let stat = (ty,t1,t2,o) in
               let w = compute_equality_weight stat in
@@ -439,36 +440,33 @@ let find_library_theorems dbd env status equalities_uris =
   let module C = Cic in
   let module S = CicSubstitution in
   let module T = CicTypeChecker in
-  let blacklist =
-    let refl_equal =
-      UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)" in
-    let s =
-      UriManager.UriSet.remove refl_equal
-        (UriManager.UriSet.union equalities_uris equations_blacklist)
-    in
-    List.fold_left
-      (fun s u -> UriManager.UriSet.add u s)
-      s [eq_XURI () ;sym_eq_URI (); trans_eq_URI (); eq_ind_URI ();
-         eq_ind_r_URI ()]
-  in
-  let metasenv, context, ugraph = env in
   let candidates =
     List.fold_left
       (fun l uri ->
-         if UriManager.UriSet.mem uri blacklist then l
+        if LibraryObjects.is_sym_eq_URI uri ||
+           LibraryObjects.is_trans_eq_URI uri ||
+           LibraryObjects.is_eq_ind_URI uri ||
+           LibraryObjects.is_eq_ind_r_URI uri 
+         then l
          else
-           let t = CicUtil.term_of_uri uri in
-           let ty, _ = CicTypeChecker.type_of_aux' metasenv context t ugraph in
-           (t, ty, [])::l)
+           (let t,ty = tty_of_u uri in t, ty, [] )::l)
       [] (MetadataQuery.signature_of_goal ~dbd status)
   in
   let refl_equal =
-    let u = eq_XURI () in
-    let t = CicUtil.term_of_uri u in
+    let eq = 
+      match LibraryObjects.eq_URI () with
+      | Some u -> u
+      | None -> 
+          raise 
+            (ProofEngineTypes.Fail 
+              (lazy "No default eq defined when running find_library_theorems"))
+    in
+    let t = CicUtil.term_of_uri (LibraryObjects.eq_refl_URI ~eq) in
     let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
     (t, ty, [])
   in
-  refl_equal::candidates
+  let res = refl_equal::candidates in
+  res
 ;;