Modifications to auto due to the introduction of the universe in

[helm.git] / components / tactics / metadataQuery.ml

diff --git a/components/tactics/metadataQuery.ml b/components/tactics/metadataQuery.ml
index 9b4f565c801a5bad56419ec2bebedbc3f15b7cb8..443ae973fe2c7b0c86d288ab08015c482db471a9 100644 (file)
--- a/components/tactics/metadataQuery.ml
+++ b/components/tactics/metadataQuery.ml
@@ -240,22 +240,47 @@ let only constants uri =
   Constr.UriManagerSet.subset consts constants 
 ;;
 
-let universe_of_goals ~(dbd:HMysql.dbd) metasenv goals =
-  let add_uris_for acc goal =
-   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
-   let main, sig_constants = Constr.signature_of ty in
-   let set = signature_of_hypothesis context metasenv in
-   let set =
-    match main with
-       None -> set
-     | Some (main,l) ->
-        List.fold_right Constr.UriManagerSet.add (main::l) set in
-   let set = Constr.UriManagerSet.union set sig_constants in
-   let all_constants_closed = close_with_types set metasenv context in
-   Constr.UriManagerSet.union all_constants_closed acc
-  in
-  let all_constants_closed = 
-    List.fold_left add_uris_for Constr.UriManagerSet.empty goals in
+let rec types_of_equality = function
+  | Cic.Appl [Cic.MutInd (uri, _, _); ty; _; _] 
+    when (LibraryObjects.is_eq_URI uri) -> 
+      let uri_set = Constr.constants_of ty in
+      if Constr.UriManagerSet.equal uri_set Constr.UriManagerSet.empty then
+       Constr.SetSet.empty
+      else Constr.SetSet.singleton uri_set
+  | Cic.Prod (_, s, t) -> 
+      Constr.SetSet.union (types_of_equality s) (types_of_equality t)
+  | _ -> Constr.SetSet.empty
+;;
+
+let types_for_equality metasenv goal =
+  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
+  let all = types_of_equality ty in
+  let _, all = 
+    List.fold_left
+      (fun (i,acc) _ ->         
+        let ty, _ = 
+           CicTypeChecker.type_of_aux' 
+             metasenv context (Cic.Rel i) CicUniv.empty_ugraph in
+        let newty = types_of_equality ty in
+          (i+1,Constr.SetSet.union newty acc)) 
+      (1,all) context
+  in all
+;;
+          
+let signature_of metasenv goal = 
+  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
+  let ty_set = Constr.constants_of ty in
+  let hyp_set = signature_of_hypothesis context metasenv in
+  let set = Constr.UriManagerSet.union ty_set hyp_set in
+    close_with_types set metasenv context
+
+
+let universe_of_goal ~(dbd:HMysql.dbd) apply_only metasenv goal =
+  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
+  let ty_set = Constr.constants_of ty in
+  let hyp_set = signature_of_hypothesis context metasenv in
+  let set = Constr.UriManagerSet.union ty_set hyp_set in
+  let all_constants_closed = close_with_types set metasenv context in
   (* we split predicates from the rest *)
   let predicates, rest = 
     Constr.UriManagerSet.partition is_predicate all_constants_closed
@@ -263,11 +288,34 @@ let universe_of_goals ~(dbd:HMysql.dbd) metasenv goals =
   let uris =
     Constr.UriManagerSet.fold
       (fun u acc -> 
-        let uris =
-          sigmatch ~dbd ~facts:false ~where:`Statement 
-            (Some (u,[]),all_constants_closed)
-        in
-        acc @ uris)
+         prerr_endline ("processing "^(UriManager.string_of_uri u));
+         let set_for_sigmatch = 
+          Constr.UriManagerSet.remove u all_constants_closed in
+        if LibraryObjects.is_eq_URI (UriManager.strip_xpointer u) then
+          (* equality has a special treatment *)
+           (prerr_endline "special treatment";
+          let tfe =
+            Constr.SetSet.elements (types_for_equality metasenv goal) 
+          in
+            List.fold_left 
+              (fun acc l ->
+                 let tyl = Constr.UriManagerSet.elements l in
+                  prerr_endline ("tyl: "^(String.concat "\n" 
+                       (List.map UriManager.string_of_uri tyl)));
+                 let set_for_sigmatch =
+                   Constr.UriManagerSet.diff set_for_sigmatch l in
+                 let uris =
+                   sigmatch ~dbd ~facts:false ~where:`Statement 
+                     (Some (u,tyl),set_for_sigmatch) in
+                   acc @ uris) 
+              acc tfe)
+        else
+           (prerr_endline "normal treatment";
+           let uris =
+             sigmatch ~dbd ~facts:false ~where:`Statement 
+               (Some (u,[]),set_for_sigmatch)
+           in
+             acc @ uris))
       predicates []
   in
 (*
@@ -277,8 +325,9 @@ let universe_of_goals ~(dbd:HMysql.dbd) metasenv goals =
 *)
   let uris = List.filter nonvar (List.map snd uris) in
   let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
-  let uris = List.filter (only all_constants_closed) uris in
-   uris
+  if apply_only then 
+    List.filter (only all_constants_closed) uris 
+  else uris
 ;;
 
 let filter_out_predicate set ctx menv =