From a151195a387e7dd1e68c58f7d5ee648622c52cf7 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 25 Oct 2004 12:50:46 +0000 Subject: [PATCH] - added var selection boolean to locate - added cardinality constraints checking to match_term --- helm/ocaml/tactics/metadataQuery.ml | 26 +++++++++++++++----------- 1 file changed, 15 insertions(+), 11 deletions(-) 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)) -- 2.39.2