The type of universe_of_goals has slightly changed, omitting

[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 a5c387971736f486004323b1d6bb729aa612a3c6..9b4f565c801a5bad56419ec2bebedbc3f15b7cb8 100644 (file)
--- a/helm/software/components/tactics/metadataQuery.ml
+++ b/helm/software/components/tactics/metadataQuery.ml
@@ -57,6 +57,7 @@ let signature_of_hypothesis context metasenv =
                 CicTypeChecker.type_of_aux' 
                   metasenv current_ctx ty CicUniv.empty_ugraph 
               in
+              let set = Constr.UriManagerSet.union set(Constr.constants_of ty)in
               match sort with
               | Cic.Sort Cic.Prop -> set, hyp::current_ctx
               | _ -> Constr.UriManagerSet.union set (Constr.constants_of t),
@@ -192,6 +193,7 @@ 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
@@ -209,13 +211,11 @@ let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
  let uris = List.filter nonvar (List.map snd uris) in
  let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
   uris
-;;
 
-let filter_predicate set ctx menv =
-  let is_predicate t = 
+let is_predicate u = 
     let ty, _ = 
       try CicTypeChecker.type_of_aux' [] []
-        (CicUtil.term_of_uri t) CicUniv.empty_ugraph
+        (CicUtil.term_of_uri u) CicUniv.empty_ugraph
       with CicTypeChecker.TypeCheckerFailure _ -> assert false
     in
     let rec check_last_pi = function
@@ -223,19 +223,78 @@ let filter_predicate set ctx menv =
       | Cic.Sort Cic.Prop -> true
       | _ -> false
     in
-    not (check_last_pi ty)
+    check_last_pi ty
+;;
+
+let only constants uri =
+  prerr_endline (UriManager.string_of_uri 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 
+;;
+
+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
+  (* we split predicates from the rest *)
+  let predicates, rest = 
+    Constr.UriManagerSet.partition is_predicate all_constants_closed
+  in
+  let uris =
+    Constr.UriManagerSet.fold
+      (fun u acc -> 
+        let uris =
+          sigmatch ~dbd ~facts:false ~where:`Statement 
+            (Some (u,[]),all_constants_closed)
+        in
+        acc @ uris)
+      predicates []
   in
-  Constr.UriManagerSet.filter is_predicate set  
+(*
+  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
+  let uris = List.filter (only all_constants_closed) uris in
+   uris
+;;
+
+let filter_out_predicate set ctx menv =
+  Constr.UriManagerSet.filter (fun u -> not (is_predicate u)) set  
 ;;
 
 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 = 
@@ -268,16 +327,18 @@ let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) =
  let set = signature_of_hypothesis context metasenv in
  (*          Printf.printf "\nsignature_of_hypothesis: %s\n\n" (to_string set); *)
  let set = Constr.UriManagerSet.union set sig_constants in
- let set = filter_predicate set context metasenv in
+ let set = filter_out_predicate set context metasenv in
  let set = close_with_types set metasenv context in
  (*          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 *)