snapshot of queries for auto+paramod

diff --git a/components/metadata/metadataConstraints.ml b/components/metadata/metadataConstraints.ml
index cb84601475f239463d668281bca7547583a1ef4a..785f73fe4a326aa88b4f63e9ad9399baeeebe7e8 100644 (file)
--- a/components/metadata/metadataConstraints.ml
+++ b/components/metadata/metadataConstraints.ml
@@ -29,7 +29,7 @@ open Printf
 open MetadataTypes 
 
 let critical_value = 7
-let just_factor = 3
+let just_factor = 1
 
 module UriManagerSet = UriManager.UriSet
 module SetSet = Set.Make (UriManagerSet)
@@ -546,7 +546,10 @@ let compute_with_only ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion)
           maximal_prefixes)
     in
 (*     Printf.fprintf stderr "all: %d\n" (List.length all);flush_all (); *)
-    List.filter (function (_,uri) -> at_most ~dbd ~where constants uri) all in
+    List.filter (function (_,uri) -> 
+      prerr_endline ("W" ^UriManager.string_of_uri uri);
+      at_most ~dbd ~where constants uri) all 
+    in
   let equal_to = compute_exactly ~dbd ~facts ~where main prefixes in
     greater_than @ equal_to
 
@@ -624,6 +627,7 @@ let sigmatch ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion)
       let types_no = List.length types in
       List.map (function (n,l) -> (n+types_no,types@l)) subsets
     in
+    prerr_endline ("critical_value exceded..." ^ string_of_int constants_no);
     let all_constants = 
      let all = match main with None -> types | Some m -> m::types in
       List.fold_right UriManagerSet.add all constants

diff --git a/components/tactics/metadataQuery.ml b/components/tactics/metadataQuery.ml
index a5c387971736f486004323b1d6bb729aa612a3c6..0dc19582a329261b1d8e43e0b20a0c017b0d6646 100644 (file)
--- a/components/tactics/metadataQuery.ml
+++ b/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),
@@ -191,31 +192,11 @@ 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
- 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 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,9 +204,52 @@ let filter_predicate set ctx menv =
       | Cic.Sort Cic.Prop -> true
       | _ -> false
     in
-    not (check_last_pi ty)
+    check_last_pi ty
+;;
+
+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
-  Constr.UriManagerSet.filter is_predicate set  
+*)
+  let uris = List.filter nonvar (List.map snd uris) in
+  let uris = List.filter Hashtbl_equiv.not_a_duplicate 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) =
@@ -268,7 +292,7 @@ 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

diff --git a/components/tactics/metadataQuery.mli b/components/tactics/metadataQuery.mli
index 0fa4a01df892070f9beeaf04c07b98f1a754f3c8..c260d5e991bbf899e02ca6ed2b85122d05fac3d8 100644 (file)
--- a/components/tactics/metadataQuery.mli
+++ b/components/tactics/metadataQuery.mli
@@ -28,8 +28,9 @@
   * @param pat shell like pattern matching over object names, a string where "*"
   * is interpreted as 0 or more characters and "?" as exactly one character *)
 
-val signature_of_goal:
-  dbd:HMysql.dbd -> ProofEngineTypes.status -> UriManager.uri list
+val universe_of_goals:
+  dbd:HMysql.dbd -> ProofEngineTypes.proof -> ProofEngineTypes.goal list ->
+    UriManager.uri list
 
 val equations_for_goal:
   dbd:HMysql.dbd ->