X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FmetadataQuery.ml;h=2941a806e3193025436a4d23393cd3ce8e9ff8ef;hb=ac31c84bb9bcf327554976d4296d787853fc8db5;hp=a5c387971736f486004323b1d6bb729aa612a3c6;hpb=52100c501bb50273660c4f4c7d92e87a90fa68a9;p=helm.git

diff --git a/helm/software/components/tactics/metadataQuery.ml b/helm/software/components/tactics/metadataQuery.ml
index a5c387971..2941a806e 100644
--- 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),
@@ -108,7 +109,7 @@ let filter_uris_backward ~dbd ~facts signature uris =
     intersect uris siguris 
 
 let compare_goal_list proof goal1 goal2 =
-  let _,metasenv,_,_ = proof in
+  let _,metasenv, _subst, _,_, _ = proof in
   let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
   let (_, ey2, ty2) =  CicUtil.lookup_meta goal2 metasenv in
   let ty_sort1,_ = 
@@ -192,8 +193,9 @@ let cmatch' =
 let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose
 let cmatch' = Constr.cmatch'
 
-let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
- let (_, metasenv, _, _) = proof in
+(* used only by te old auto *)
+let signature_of_goal ~(dbd:HSql.dbd) ((proof, goal) as _status) =
+ let (_, metasenv, _subst, _, _, _) = 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
@@ -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,20 +223,128 @@ 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 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:HSql.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
+  in
+  let uris =
+    Constr.UriManagerSet.fold
+      (fun u acc -> 
+         debug_print (lazy ("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 *)
+           (debug_print (lazy "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
+                  debug_print (lazy ("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
+           (debug_print (lazy "normal treatment");
+           let uris =
+             sigmatch ~dbd ~facts:false ~where:`Statement 
+               (Some (u,[]),set_for_sigmatch)
+           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
+  if apply_only then 
+    List.filter (only all_constants_closed) uris 
+  else 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 equations_for_goal ~(dbd:HSql.dbd) ?signature ((proof, goal) as _status) =
+(*
+  let to_string set =
+    "{\n" ^
+      (String.concat "\n"
          (Constr.UriManagerSet.fold
-            (fun u l -> (UriManager.string_of_uri u)::l) set []))
-    ^ " }"
-  in *)
- let (_, metasenv, _, _) = proof in
+            (fun u l -> ("  "^UriManager.string_of_uri u)::l) set []))
+    ^ "\n}"
+  in
+*)
+ let (_, metasenv, _subst, _, _, _) = proof in
  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
  let main, sig_constants = 
    match signature with 
@@ -268,23 +376,25 @@ 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 *)
 
 let experimental_hint 
-  ~(dbd:HMysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
-  let (_, metasenv, _, _) = proof in
+  ~(dbd:HSql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
+  let (_, metasenv, _subst, _, _, _) = proof in
   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
   let (uris, (main, sig_constants)) =
     match signature with
@@ -365,10 +475,10 @@ let experimental_hint
     (aux uris)
 
 let new_experimental_hint 
-  ~(dbd:HMysql.dbd) ?(facts=false) ?signature ~universe
+  ~(dbd:HSql.dbd) ?(facts=false) ?signature ~universe
   ((proof, goal) as status)
 =
-  let (_, metasenv, _, _) = proof in
+  let (_, metasenv,  _subst, _, _, _) = proof in
   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
   let (uris, (main, sig_constants)) =
     match signature with