commented out are_convertible in is_identity

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

diff --git a/helm/software/components/tactics/metadataQuery.ml b/helm/software/components/tactics/metadataQuery.ml
index cd14f3f5eb8d6be766c272b73e5af3fd9aa730fa..be68c31f750c4a1fb73b5c7fc03ee2b48b5d2566 100644 (file)
--- a/helm/software/components/tactics/metadataQuery.ml
+++ b/helm/software/components/tactics/metadataQuery.ml
@@ -212,6 +212,11 @@ let only constants uri =
   let t = CicUtil.term_of_uri uri in (* FIXME: write ty_of_term *)
   let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
   let consts = Constr.constants_of ty in
+(*  prerr_endline ("XXX " ^ UriManager.string_of_uri uri);*)
+(*  Constr.UriManagerSet.iter (fun u -> prerr_endline (" - " ^*)
+(*  UriManager.string_of_uri u)) consts;*)
+(*  Constr.UriManagerSet.iter (fun u -> prerr_endline (" + " ^*)
+(*  UriManager.string_of_uri u)) constants;*)
   Constr.UriManagerSet.subset consts constants 
 ;;
 
@@ -236,6 +241,7 @@ let universe_of_goals ~(dbd:HMysql.dbd) proof goals =
   let predicates, rest = 
     Constr.UriManagerSet.partition is_predicate all_constants_closed
   in
+  prerr_endline ("FOO!1");
   let uris =
     Constr.UriManagerSet.fold
       (fun u acc -> 
@@ -246,6 +252,7 @@ let universe_of_goals ~(dbd:HMysql.dbd) proof goals =
         acc @ uris)
       predicates []
   in
+  prerr_endline ("FOO!2");
 (*
   let uris =
     sigmatch ~dbd ~facts:false ~where:`Statement (None,all_constants_closed) 
@@ -262,13 +269,13 @@ let filter_out_predicate set ctx menv =
 ;;
 
 let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) =
-(*   let to_string set =
-    "{ " ^
-      (String.concat ", "
+  let to_string set =
+    "{\n" ^
+      (String.concat "\n"
          (Constr.UriManagerSet.fold
-            (fun u l -> (UriManager.string_of_uri u)::l) set []))
-    ^ " }"
-  in *)
+            (fun u l -> ("  "^UriManager.string_of_uri u)::l) set []))
+    ^ "\n}"
+  in
  let (_, metasenv, _, _) = proof in
  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
  let main, sig_constants = 
@@ -306,11 +313,13 @@ let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) =
  (*          Printf.printf "\ndopo close_with_types: %s\n\n" (to_string set); *)
  let set = close_with_constructors set metasenv context in
  (*          Printf.printf "\ndopo close_with_constructors: %s\n\n" (to_string set); *)
- let set = List.fold_right Constr.UriManagerSet.remove l set in
+ let set_for_sigmatch = List.fold_right Constr.UriManagerSet.remove l set in
  let uris =
-   sigmatch ~dbd ~facts:false ~where:`Statement (main,set) in
+   sigmatch ~dbd ~facts:false ~where:`Statement (main,set_for_sigmatch) in
  let uris = List.filter nonvar (List.map snd uris) in
  let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
+ let set = List.fold_right Constr.UriManagerSet.add l set in
+ let uris = List.filter (only set) uris in
  uris
    (*        ) *)
    (*        else raise Goal_is_not_an_equation *)