upgraded code to work with non-default equalities

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index e30d4403490cd01fce5fe4050141656bef3a48f4..a7b2c30399d20ab40016827e1419fe4bbc4a8b5d 100644 (file)
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -228,8 +228,8 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
                   (candidate, eq_URI))
           in
           let c, other, eq_URI =
-            if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI
-            else right, left, HL.Logic.eq_ind_r_URI
+            if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
+            else right, left, Utils.eq_ind_r_URI ()
           in
           if o <> U.Incomparable then
             try
@@ -317,8 +317,8 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
              (candidate, eq_URI))
           in
           let c, other, eq_URI =
-            if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI
-            else right, left, HL.Logic.eq_ind_r_URI
+            if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
+            else right, left, Utils.eq_ind_r_URI ()
           in
           if o <> U.Incomparable then
             try
@@ -507,16 +507,6 @@ let rec demodulation_aux metasenv context ugraph table lift_amount term =
 ;;
 
 
-let build_ens_for_sym_eq ty x y = 
-  [(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_newtarget_time = ref 0.;;
 
 
@@ -555,7 +545,7 @@ let rec demodulation_equality newmeta env table sign target =
       incr demod_counter;
       let bo' =
         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
-        C.Appl [C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
+        C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
                 S.lift 1 eq_ty; l; r]
       in
       if sign = Utils.Positive then
@@ -574,13 +564,16 @@ let rec demodulation_equality newmeta env table sign target =
 (*         let target' = *)
           let eq_found =
             let proof' =
-              let ens =
-                if pos = Utils.Left then
-                  build_ens_for_sym_eq ty what other
-                else
-                  build_ens_for_sym_eq ty other what
+(*               let ens = *)
+(*                 if pos = Utils.Left then *)
+(*                   build_ens_for_sym_eq ty what other *)
+(*                 else *)
+(*                   build_ens_for_sym_eq ty other what *)
+              let termlist =
+                if pos = Utils.Left then [ty; what; other]
+                else [ty; other; what]
               in
-              Inference.ProofSymBlock (ens, proof')
+              Inference.ProofSymBlock (termlist, proof')
             in
             let what, other =
               if pos = Utils.Left then what, other else other, what
@@ -606,7 +599,7 @@ let rec demodulation_equality newmeta env table sign target =
 (*         in *)
         let refl =
           C.Appl [C.MutConstruct (* reflexivity *)
-                    (HelmLibraryObjects.Logic.eq_URI, 0, 1, []);
+                    (LibraryObjects.eq_URI (), 0, 1, []);
                   eq_ty; if is_left then right else left]          
         in
         (bo,
@@ -828,7 +821,8 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
       let bo'' = 
         let l, r =
           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
-        C.Appl [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty; l; r]
+        C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
+                S.lift 1 eq_ty; l; r]
       in
       incr maxmeta;
       let metaproof =
@@ -839,13 +833,17 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
 (*       let target' = *)
         let eq_found =
           let proof' =
-            let ens =
-              if pos = Utils.Left then
-                build_ens_for_sym_eq ty what other
-              else
-                build_ens_for_sym_eq ty other what
+(*             let ens = *)
+(*               if pos = Utils.Left then *)
+(*                 build_ens_for_sym_eq ty what other *)
+(*               else *)
+(*                 build_ens_for_sym_eq ty other what *)
+(*             in *)
+            let termlist =
+              if pos = Utils.Left then [ty; what; other]
+              else [ty; other; what]
             in
-            Inference.ProofSymBlock (ens, proof')
+            Inference.ProofSymBlock (termlist, proof')
           in
           let what, other =
             if pos = Utils.Left then what, other else other, what
@@ -870,7 +868,7 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
 (*       in *)
       let refl =
         C.Appl [C.MutConstruct (* reflexivity *)
-                  (HelmLibraryObjects.Logic.eq_URI, 0, 1, []);
+                  (LibraryObjects.eq_URI (), 0, 1, []);
                 eq_ty; if ordering = U.Gt then right else left]
       in
       (bo',
@@ -940,7 +938,8 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
       let bo'' =
         let l, r =
           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
-        C.Appl [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty; l; r]
+        C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
+                S.lift 1 eq_ty; l; r]
       in
       bo',
       Inference.ProofBlock (
@@ -1029,11 +1028,15 @@ let rec demodulation_goal newmeta env table goal =
       in
       let eq_found =
         let proof' =
-          let ens =
-            if pos = Utils.Left then build_ens_for_sym_eq ty what other
-            else build_ens_for_sym_eq ty other what
+(*           let ens = *)
+(*             if pos = Utils.Left then build_ens_for_sym_eq ty what other *)
+(*             else build_ens_for_sym_eq ty other what *)
+(*           in *)
+          let termlist =
+            if pos = Utils.Left then [ty; what; other]
+            else [ty; other; what]
           in
-          Inference.ProofSymBlock (ens, proof')
+          Inference.ProofSymBlock (termlist, proof')
         in
         let what, other =
           if pos = Utils.Left then what, other else other, what

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 ->

diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli
index d0556dd5444b1fbf52bb6e9db227f0fe073687b0..560af55da9af9a438b2f086fe7a4aa722949857c 100644 (file)
--- a/helm/ocaml/paramodulation/inference.mli
+++ b/helm/ocaml/paramodulation/inference.mli
@@ -18,7 +18,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
 
 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph
@@ -54,8 +55,7 @@ val beta_expand:
    fresh metas...
 *)
 val find_equalities:
-  ?eq_uri:UriManager.uri -> Cic.context -> ProofEngineTypes.proof ->
-  int list * equality list * int
+  Cic.context -> ProofEngineTypes.proof -> int list * equality list * int
 
 
 exception TermIsNotAnEquality;;
@@ -64,10 +64,9 @@ exception TermIsNotAnEquality;;
    raises TermIsNotAnEquality if term is not an equation.
    The first Cic.term is a proof of the equation
 *)
-val equality_of_term: ?eq_uri:UriManager.uri -> Cic.term -> Cic.term ->
-  equality
+val equality_of_term: Cic.term -> Cic.term -> equality
 
-val term_is_equality: ?eq_uri:UriManager.uri -> Cic.term -> bool
+val term_is_equality: Cic.term -> bool
 
 (**
    superposition_left env target source

diff --git a/helm/ocaml/paramodulation/saturate_main.ml b/helm/ocaml/paramodulation/saturate_main.ml
index bf9ec689726298a62fafbf366edc36e5f9be62e5..ab39ff3deb327587e32ef6b8393aaa42088bece2 100644 (file)
--- a/helm/ocaml/paramodulation/saturate_main.ml
+++ b/helm/ocaml/paramodulation/saturate_main.ml
@@ -1,6 +1,6 @@
-let configuration_file = ref "../helm/matita/matita.conf.xml";;
+let configuration_file = ref "../../matita/matita.conf.xml";;
 
-let core_notation_script = "../helm/matita/core_notation.moo";;
+let core_notation_script = "../../matita/core_notation.moo";;
 
 let get_from_user ~(dbd:HMysql.dbd) =
   let rec get () =
@@ -59,7 +59,7 @@ let _ =
 in
 Helm_registry.load_from !configuration_file;
 CicNotation.load_notation core_notation_script;
-CicNotation.load_notation "../helm/matita/coq.ma";
+CicNotation.load_notation "../../matita/coq.ma";
 let dbd = HMysql.quick_connect
   ~host:(Helm_registry.get "db.host")
   ~user:(Helm_registry.get "db.user")

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index bc935d7f730c518d97ed9c3a7dba09ba03c64714..4cf14ae18a4baf579c13e8f54db8d8f68d57b962 100644 (file)
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -875,7 +875,8 @@ let apply_equality_to_goal env equality goal =
   let module I = Inference in
   let metasenv, context, ugraph = env in
   let _, proof, (ty, left, right, _), metas, args = equality in
-  let eqterm = C.Appl [C.MutInd (HL.Logic.eq_URI, 0, []); ty; left; right] in
+  let eqterm =
+    C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right] in
   let gproof, gmetas, gterm = goal in
   try
     let subst, metasenv', _ =
@@ -1969,7 +1970,8 @@ let saturate
         context_hyp @ thms
       else
         let refl_equal =
-          UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"
+          let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
+          UriManager.uri_of_string (us ^ "#xpointer(1/1/1)")
         in
         let t = CicUtil.term_of_uri refl_equal in
         let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in

diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index 2d5ee24ce7612527102a3f128c586fa66511145d..27934674808bf339ec9c797c00de0375786da493 100644 (file)
--- a/helm/ocaml/paramodulation/utils.ml
+++ b/helm/ocaml/paramodulation/utils.ml
@@ -513,3 +513,12 @@ let string_of_pos = function
   | Left -> "Left"
   | Right -> "Right"
 ;;
+
+
+let eq_ind_URI () = LibraryObjects.eq_ind_URI ~eq:(LibraryObjects.eq_URI ())
+let eq_ind_r_URI () = LibraryObjects.eq_ind_r_URI ~eq:(LibraryObjects.eq_URI ())
+let sym_eq_URI () = LibraryObjects.sym_eq_URI ~eq:(LibraryObjects.eq_URI ())
+let eq_XURI () =
+  let s = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
+  UriManager.uri_of_string (s ^ "#xpointer(1/1/1)")
+let trans_eq_URI () = LibraryObjects.trans_eq_URI ~eq:(LibraryObjects.eq_URI ())

diff --git a/helm/ocaml/paramodulation/utils.mli b/helm/ocaml/paramodulation/utils.mli
index 7814a4b88d3eed6c83e0f57d7e8ff0c0522155e2..910c4a651940d11e25afeb5b44539e8eb3c3af9d 100644 (file)
--- a/helm/ocaml/paramodulation/utils.mli
+++ b/helm/ocaml/paramodulation/utils.mli
@@ -45,3 +45,9 @@ val string_of_pos: pos -> string
 val compute_equality_weight: Cic.term -> Cic.term -> Cic.term -> int
 
 val debug_print: string Lazy.t -> unit
+
+val eq_ind_URI: unit -> UriManager.uri
+val eq_ind_r_URI: unit -> UriManager.uri
+val sym_eq_URI: unit -> UriManager.uri
+val eq_XURI: unit -> UriManager.uri
+val trans_eq_URI: unit -> UriManager.uri