From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 25 Oct 2004 12:50:46 +0000 (+0000)
Subject: - added var selection boolean to locate
X-Git-Tag: V_0_0_10~15
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a151195a387e7dd1e68c58f7d5ee648622c52cf7;p=helm.git

- 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 d280b0928..56bb93ac2 100644
--- 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))