Minor changes.

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

diff --git a/components/tactics/metadataQuery.ml b/components/tactics/metadataQuery.ml
index be68c31f750c4a1fb73b5c7fc03ee2b48b5d2566..9b4f565c801a5bad56419ec2bebedbc3f15b7cb8 100644 (file)
--- a/components/tactics/metadataQuery.ml
+++ b/components/tactics/metadataQuery.ml
@@ -192,7 +192,26 @@ let cmatch' =
 *)
 let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose
 let cmatch' = Constr.cmatch'
-  
+
+(* used only by te old auto *)
+let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
+ let (_, metasenv, _, _) = proof in
+ 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
+ let uris =
+  sigmatch ~dbd ~facts:false ~where:`Statement (None,all_constants_closed) in
+ let uris = List.filter nonvar (List.map snd uris) in
+ let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
+  uris
+
 let is_predicate u = 
     let ty, _ = 
       try CicTypeChecker.type_of_aux' [] []
@@ -212,16 +231,16 @@ 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;*)
+(*
+  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 
 ;;
 
-let universe_of_goals ~(dbd:HMysql.dbd) proof goals =
-  let (_, metasenv, _, _) = proof in
+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
@@ -241,7 +260,6 @@ 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 -> 
@@ -252,7 +270,6 @@ 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) 
@@ -269,6 +286,7 @@ let filter_out_predicate set ctx menv =
 ;;
 
 let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) =
+(*
   let to_string set =
     "{\n" ^
       (String.concat "\n"
@@ -276,6 +294,7 @@ let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) =
             (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 =