From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 27 Jun 2006 16:53:48 +0000 (+0000)
Subject: used the new metadataConstraint function to retrieve equalities from the library
X-Git-Tag: make_still_working~7141
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4313889a915eb0df74bc047f89a7316c8cf4e19c;p=helm.git

used the new metadataConstraint function to retrieve equalities from the library
---

diff --git a/helm/software/components/tactics/paramodulation/inference.ml b/helm/software/components/tactics/paramodulation/inference.ml
index 1c3daffec..a27116bc9 100644
--- a/helm/software/components/tactics/paramodulation/inference.ml
+++ b/helm/software/components/tactics/paramodulation/inference.ml
@@ -331,12 +331,38 @@ let utty_of_u u =
   u, t, ty
 ;;
 
-let find_library_equalities dbd context status maxmeta = 
+let find_library_equalities caso_strano dbd context status maxmeta = 
   let module C = Cic in
   let module S = CicSubstitution in
   let module T = CicTypeChecker in
   let _ = <:start<equations_for_goal>> in
-  let eqs = (MetadataQuery.equations_for_goal ~dbd status) in
+  let signature = 
+    if caso_strano then
+      begin
+        let proof, goalno = status in
+        let _,metasenv,_,_ = proof in
+        let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
+        match ty with
+        | Cic.Appl[Cic.MutInd(u,0,_);eq_ty;l;r] ->
+            (let mainl, sigl = MetadataConstraints.signature_of l in
+            let mainr, sigr = MetadataConstraints.signature_of r in
+            match mainl,mainr with
+            | Some (uril,tyl), Some (urir, tyr) 
+                when LibraryObjects.is_eq_URI uril && 
+                     LibraryObjects.is_eq_URI urir && 
+                     tyl = tyr ->
+                  Some (mainl,MetadataConstraints.UriManagerSet.union sigl sigr)
+            | _ -> 
+                let u = (UriManager.uri_of_string
+                  (UriManager.string_of_uri u ^ "#xpointer(1/1)")) in
+                let main = Some (u, []) in
+                Some (main,MetadataConstraints.UriManagerSet.union sigl sigr))
+        | _ -> assert false
+      end
+    else
+      None
+  in
+  let eqs = (MetadataQuery.equations_for_goal ~dbd ?signature status) in
   let _ = <:stop<equations_for_goal>> in
   let candidates =
     List.fold_left
diff --git a/helm/software/components/tactics/paramodulation/inference.mli b/helm/software/components/tactics/paramodulation/inference.mli
index 0de5e8433..5c6a1979b 100644
--- a/helm/software/components/tactics/paramodulation/inference.mli
+++ b/helm/software/components/tactics/paramodulation/inference.mli
@@ -57,7 +57,7 @@ val find_equalities:
    searches the library for equalities that can be applied to the current goal
 *)
 val find_library_equalities:
-  HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int ->
+  bool -> HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int ->
     UriManager.UriSet.t * (UriManager.uri * Equality.equality) list * int
 
 (**