implemented in place old Filter_auto filtering

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 18ea81381eebb8ae2b025462bef1ecd4c52e9edd..13a73b561b6e477b164c1f008e351b832e9bdb17 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -36,10 +36,13 @@ let locate ~(dbh:Dbi.connection) name =
   List.map (function [`String s] -> s | _ -> assert false) (query#fetchall ())
 
 let match_term ~(dbh:Dbi.connection) ty =
-  let metadata = MetadataExtractor.compute ~body:None ~ty in
-  Constr.at_least ~dbh metadata
+  let constraints =
+    List.map MetadataTypes.constr_of_metadata
+      (MetadataExtractor.compute ~body:None ~ty)
+  in
+  Constr.at_least ~dbh constraints
 
-let nonvar (_, s) =
+let nonvar s =
   let len = String.length s in
   let suffix = String.sub s (len-4) 4 in
   not (suffix  = ".var")
@@ -56,6 +59,28 @@ let signature_of_hypothesis context =
           Constr.StringSet.union set (Constr.constants_of t))
     Constr.StringSet.empty context
 
+let intersect l1 l2 =
+  let set1 = List.fold_right Constr.StringSet.add l1 Constr.StringSet.empty in
+  let set2 = List.fold_right Constr.StringSet.add l2 Constr.StringSet.empty in
+  Constr.StringSet.elements (Constr.StringSet.inter set1 set2)
+
+let filter_uris_forward ~dbh (main, constants) uris =
+  let main_uris =
+    match main with
+    | None -> []
+    | Some (main, types) -> main :: types
+  in
+  let full_signature =
+    List.fold_right Constr.StringSet.add main_uris constants
+  in
+  List.filter (Constr.at_most ~dbh full_signature) uris
+
+let filter_uris_backward ~dbh signature uris =
+  let siguris =
+    List.map snd (MetadataConstraints.sigmatch ~dbh ~where:`Statement signature)
+  in
+  intersect uris siguris
+
 let hint ~(dbh:Dbi.connection) ?signature ((proof, goal) as status) =
   let (_, metasenv, _, _) = proof in
   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
@@ -64,15 +89,7 @@ let hint ~(dbh:Dbi.connection) ?signature ((proof, goal) as status) =
     | Some signature -> (Constr.sigmatch ~dbh signature, signature)
     | None -> (Constr.cmatch' ~dbh ty, Constr.signature_of ty)
   in
-  let uris = List.filter nonvar uris in
-(*
-  let concl_constants =
-    match main with
-    | None -> sig_constants
-    | Some (main, types) ->
-        List.fold_right Constr.StringSet.add sig_constants (main :: types)
-  in
-*)
+  let uris = List.filter nonvar (List.map snd uris) in
   let types_constants =
     match main with
     | None -> Constr.StringSet.empty
@@ -87,12 +104,10 @@ let hint ~(dbh:Dbi.connection) ?signature ((proof, goal) as status) =
   let uris = 
     if (List.length uris < 2 ** (Constr.StringSet.cardinal other_constants))
     then begin
-      prerr_endline
-        "MetadataQuery: large signature, falling back to old method";
-      List.filter (Filter_auto.filter_new_constants ~dbh all_constants main)
-        uris
+      prerr_endline "MetadataQuery: large sig, falling back to old method";
+      filter_uris_forward ~dbh (main, other_constants) uris
     end else
-      Filter_auto.filter_uris ~dbh all_constants uris main
+      filter_uris_backward ~dbh (main, other_constants) uris
   in
   List.map
     (fun uri ->
@@ -100,4 +115,5 @@ let hint ~(dbh:Dbi.connection) ?signature ((proof, goal) as status) =
        ProofEngineTypes.apply_tactic
         (PrimitiveTactics.apply_tac ~term:(CicUtil.term_of_uri uri))
         status))
+    uris