- added var selection boolean to locate

- added cardinality constraints checking to match_term

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index d280b0928ee0b074f28f8d2a79f596df94ea6bd6..56bb93ac2134fe566e740f1c53bd8370f4bb779f 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -27,25 +27,29 @@ open Printf
 
 module Constr = MetadataConstraints
 
-let locate ~(dbh:Dbi.connection) name =
+let nonvar s =
+  let len = String.length s in
+  let suffix = String.sub s (len-4) 4 in
+  not (suffix  = ".var")
+
+let locate ~(dbh:Dbi.connection) ?(vars = false) name =
   let query =
     dbh#prepare (sprintf "SELECT source FROM %s WHERE value = \"%s\""
       MetadataTypes.name_tbl name)
   in
   query#execute [];
-  List.map (function [`String s] -> s | _ -> assert false) (query#fetchall ())
+  List.filter nonvar
+    (List.map (function [`String s] -> s | _ -> assert false)
+      (query#fetchall ()))
 
 let match_term ~(dbh:Dbi.connection) ty =
-  let constraints =
-    List.map MetadataTypes.constr_of_metadata
-      (MetadataExtractor.compute ~body:None ~ty)
+  let metadata = MetadataExtractor.compute ~body:None ~ty in
+  let constants_no =
+    MetadataConstraints.StringSet.cardinal (MetadataConstraints.constants_of ty)
   in
-  Constr.at_least ~dbh constraints
-
-let nonvar s =
-  let len = String.length s in
-  let suffix = String.sub s (len-4) 4 in
-  not (suffix  = ".var")
+  let constraints = List.map MetadataTypes.constr_of_metadata metadata in
+  Constr.at_least ~dbh ~full_card:(MetadataConstraints.Eq constants_no)
+    constraints
 
 let ( ** ) x y = int_of_float ((float_of_int x) ** (float_of_int y))