X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FmetadataQuery.ml;h=0dc19582a329261b1d8e43e0b20a0c017b0d6646;hb=e53c9d7cf1a5d3d33c41cad5b046b018a62a9d2d;hp=b9c0536538e4295726347b7ad82071e1c89ed160;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/tactics/metadataQuery.ml b/components/tactics/metadataQuery.ml
index b9c053653..0dc19582a 100644
--- a/components/tactics/metadataQuery.ml
+++ b/components/tactics/metadataQuery.ml
@@ -38,15 +38,36 @@ let debug_print s = if debug then prerr_endline (Lazy.force s)
 
 let ( ** ) x y = int_of_float ((float_of_int x) ** (float_of_int y))
 
-let signature_of_hypothesis context =
-  List.fold_left
-    (fun set hyp ->
-      match hyp with
-      | None -> set
-      | Some (_, Cic.Decl t)
-      | Some (_, Cic.Def (t, _)) ->
-          Constr.UriManagerSet.union set (Constr.constants_of t))
-    Constr.UriManagerSet.empty context
+let signature_of_hypothesis context metasenv =
+  let set, _ =
+    List.fold_right
+      (fun hyp (set,current_ctx) ->
+        match hyp with
+        | None -> set, hyp::current_ctx
+        | Some (_, Cic.Decl t) -> 
+            Constr.UriManagerSet.union set (Constr.constants_of t),
+            hyp::current_ctx
+        | Some (_, Cic.Def (t, _)) ->
+            try 
+              let ty,_ = 
+                CicTypeChecker.type_of_aux' 
+                  metasenv current_ctx t CicUniv.empty_ugraph 
+              in
+              let sort,_ = 
+                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),
+                     hyp::current_ctx
+            with
+            | CicTypeChecker.TypeCheckerFailure _ -> set, hyp::current_ctx)
+      context (Constr.UriManagerSet.empty,[]) 
+  in
+  set
+;;
 
 let intersect uris siguris =
   let set1 = List.fold_right Constr.UriManagerSet.add uris Constr.UriManagerSet.empty in
@@ -171,26 +192,67 @@ let cmatch' =
 *)
 let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose
 let cmatch' = Constr.cmatch'
+  
+let is_predicate u = 
+    let ty, _ = 
+      try CicTypeChecker.type_of_aux' [] []
+        (CicUtil.term_of_uri u) CicUniv.empty_ugraph
+      with CicTypeChecker.TypeCheckerFailure _ -> assert false
+    in
+    let rec check_last_pi = function
+      | Cic.Prod (_,_,tgt) -> check_last_pi tgt
+      | Cic.Sort Cic.Prop -> true
+      | _ -> false
+    in
+    check_last_pi ty
+;;
 
-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 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 universe_of_goals ~(dbd:HMysql.dbd) proof goals =
+  let (_, metasenv, _, _) = proof in
+  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
+(*
+  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 equations_for_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
+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 ", "
@@ -200,33 +262,42 @@ let equations_for_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
   in *)
  let (_, metasenv, _, _) = proof in
  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
- let main, sig_constants = Constr.signature_of ty in
+ let main, sig_constants = 
+   match signature with 
+   | None -> Constr.signature_of ty 
+   | Some s -> s
+ in
 (*  Printf.printf "\nsig_constants: %s\n\n" (to_string sig_constants); *)
 (*  match main with *)
 (*      None -> raise Goal_is_not_an_equation *)
 (*    | Some (m,l) -> *)
- let m, l =
+ let l =
    let eq_URI =
-     let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
-     UriManager.uri_of_string (us ^ "#xpointer(1/1)")
+    match LibraryObjects.eq_URI () with
+       None -> None
+     | Some s ->
+        Some
+         (UriManager.uri_of_string
+          (UriManager.string_of_uri s ^ "#xpointer(1/1)"))
    in
-   match main with
-   | None -> eq_URI, []
-   | Some (m, l) when UriManager.eq m eq_URI -> m, l
-   | Some (m, l) -> eq_URI, []
+   match eq_URI,main with
+   | Some eq_URI, Some (m, l) when UriManager.eq m eq_URI -> m::l
+   | _ -> []
  in
- Printf.printf "\nSome (m, l): %s, [%s]\n\n"
-   (UriManager.string_of_uri m)
-   (String.concat "; " (List.map UriManager.string_of_uri l));
+ (*Printf.printf "\nSome (m, l): %s, [%s]\n\n"
+   (UriManager.string_of_uri (List.hd l))
+   (String.concat "; " (List.map UriManager.string_of_uri (List.tl l)));
+ *)
  (*        if m == UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI then ( *)
- let set = signature_of_hypothesis context in
+ 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_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 (m::l) set in
+ let set = List.fold_right Constr.UriManagerSet.remove l set in
  let uris =
    sigmatch ~dbd ~facts:false ~where:`Statement (main,set) in
  let uris = List.filter nonvar (List.map snd uris) in
@@ -258,7 +329,7 @@ let experimental_hint
   let all_constants =
     let hyp_and_sug =
       Constr.UriManagerSet.union
-        (signature_of_hypothesis context) 
+        (signature_of_hypothesis context metasenv) 
         sig_constants
     in
     let main =