upgraded code to work with non-default equalities

[helm.git] / helm / ocaml / paramodulation / inference.ml

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index 474f0a4d14f7ab63f8f8dc545a7da8e82fb1ab20..ac99340005eec05a88c3209c0b175168dcb8d6a8 100644 (file)
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -21,7 +21,8 @@ and proof =
 (*         (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) *  *)
         (Utils.pos * equality) * proof
   | ProofGoalBlock of proof * proof (* equality *)
-  | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof
+(*   | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof *)
+  | ProofSymBlock of Cic.term list * proof
   | SubProof of Cic.term * int * proof
 ;;
 
@@ -45,6 +46,29 @@ let string_of_equality ?env =
 ;;
 
 
+let build_ens_for_sym_eq sym_eq_URI termlist =
+  let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph sym_eq_URI in
+  match obj with
+  | Cic.Constant (_, _, _, uris, _) ->
+      assert (List.length uris <= List.length termlist);
+      let rec aux = function
+        | [], tl -> [], tl
+        | (uri::uris), (term::tl) ->
+            let ens, args = aux (uris, tl) in
+            (uri, term)::ens, args
+        | _, _ -> assert false
+      in
+      aux (uris, termlist)
+  | _ -> assert false
+(*   [(UriManager.uri_of_string *)
+(*       "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var", ty); *)
+(*    (UriManager.uri_of_string *)
+(*       "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var", x); *)
+(*    (UriManager.uri_of_string *)
+(*       "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var", y)] *)
+;;
+
+
 let build_proof_term proof =
   let rec do_build_proof proof = 
     match proof with
@@ -55,12 +79,16 @@ let build_proof_term proof =
     | ProofGoalBlock (proofbit, proof) ->
         print_endline "found ProofGoalBlock, going up...";
         do_build_goal_proof proofbit proof
-    | ProofSymBlock (ens, proof) ->
+(*     | ProofSymBlock (ens, proof) -> *)
+(*         let proof = do_build_proof proof in *)
+(*         Cic.Appl [ *)
+(*           Cic.Const (Utils.sym_eq_URI (), ens); (\* symmetry *\) *)
+(*           proof *)
+(*         ] *)
+    | ProofSymBlock (termlist, proof) ->
         let proof = do_build_proof proof in
-        Cic.Appl [
-          Cic.Const (HelmLibraryObjects.Logic.sym_eq_URI, ens); (* symmetry *)
-          proof
-        ]
+        let ens, args = build_ens_for_sym_eq (Utils.sym_eq_URI ()) termlist in
+        Cic.Appl ([Cic.Const (Utils.sym_eq_URI (), ens)] @ args @ [proof])
     | ProofBlock (subst, eq_URI, (name, ty), bo(* t' *), (pos, eq), eqproof) ->
         let t' = Cic.Lambda (name, ty, bo) in
         let proof' =
@@ -1019,10 +1047,11 @@ let beta_expand ?(metas_ok=true) ?(match_only=false)
 ;;
 
 
-let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
+let find_equalities context proof =
   let module C = Cic in
   let module S = CicSubstitution in
   let module T = CicTypeChecker in
+  let eq_uri = LibraryObjects.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
@@ -1121,11 +1150,18 @@ 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 candidates =
     List.fold_left
       (fun l uri ->
        let suri = UriManager.string_of_uri uri in
-         if UriManager.UriSet.mem uri equations_blacklist then
+         if UriManager.UriSet.mem uri blacklist then
            l
          else
            let t = CicUtil.term_of_uri uri in
@@ -1136,8 +1172,8 @@ let find_library_equalities dbd context status maxmeta =
       []
       (MetadataQuery.equations_for_goal ~dbd status)
   in
-  let eq_uri1 = UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI
-  and eq_uri2 = HelmLibraryObjects.Logic.eq_URI in
+  let eq_uri1 = eq_XURI () (* UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI *)
+  and eq_uri2 = LibraryObjects.eq_URI () in (* HelmLibraryObjects.Logic.eq_URI in *)
   let iseq uri =
     (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2)
   in
@@ -1214,8 +1250,13 @@ let find_library_theorems dbd env status equalities_uris =
   let blacklist =
     let refl_equal =
       UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)" in
-    UriManager.UriSet.remove refl_equal
-      (UriManager.UriSet.union equalities_uris equations_blacklist)
+    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 [sym_eq_URI (); trans_eq_URI (); eq_ind_URI (); eq_ind_r_URI ()]
   in
   let metasenv, context, ugraph = env in
   let candidates =
@@ -1348,8 +1389,8 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
 ;;
 
 
-let term_is_equality ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) term =
-  let iseq uri = UriManager.eq uri eq_uri in
+let term_is_equality term =
+  let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
   match term with
   | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
   | _ -> false
@@ -1358,7 +1399,8 @@ let term_is_equality ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) term =
 
 exception TermIsNotAnEquality;;
 
-let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof term =
+let equality_of_term proof term =
+  let eq_uri = LibraryObjects.eq_URI () in
   let iseq uri = UriManager.eq uri eq_uri in
   match term with
   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->