From: Stefano Zacchiroli Date: Fri, 3 Dec 2004 16:04:01 +0000 (+0000) Subject: changed "locate" so that it supports shell-like pattern matching with X-Git-Tag: V_0_1_0~170 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6c6530f435e82cc7688c3f76c4d61b4e0bd7a0e5;p=helm.git changed "locate" so that it supports shell-like pattern matching with '*' and '?' wildcards --- diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index 180091c0a..f65318896 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -28,15 +28,29 @@ open Printf module Constr = MetadataConstraints module PET = ProofEngineTypes + (** maps a shell like pattern (which uses '*' and '?') to a sql pattern for + * the "like" operator (which uses '%' and '_'). Does not support escaping. *) +let sqlpat_of_shellglob = + let star_RE, qmark_RE, percent_RE, uscore_RE = + Pcre.regexp "\\*", Pcre.regexp "\\?", Pcre.regexp "%", Pcre.regexp "_" + in + fun shellglob -> + Pcre.replace ~rex:star_RE ~templ:"%" + (Pcre.replace ~rex:qmark_RE ~templ:"_" + (Pcre.replace ~rex:percent_RE ~templ:"\\%" + (Pcre.replace ~rex:uscore_RE ~templ:"\\_" + shellglob))) + let nonvar s = let len = String.length s in let suffix = String.sub s (len-4) 4 in not (suffix = ".var") -let locate ~(dbd:Mysql.dbd) ?(vars = false) name = +let locate ~(dbd:Mysql.dbd) ?(vars = false) pat = + let sql_pat = sqlpat_of_shellglob pat in let query = - sprintf "SELECT source FROM %s WHERE value = \"%s\"" - MetadataTypes.name_tbl name + sprintf "SELECT source FROM %s WHERE value LIKE \"%s\"" + MetadataTypes.name_tbl sql_pat in let result = Mysql.exec dbd query in List.filter nonvar diff --git a/helm/ocaml/tactics/metadataQuery.mli b/helm/ocaml/tactics/metadataQuery.mli index b3b506de9..0d32e4835 100644 --- a/helm/ocaml/tactics/metadataQuery.mli +++ b/helm/ocaml/tactics/metadataQuery.mli @@ -24,7 +24,9 @@ *) (** @param vars if set variables (".var" URIs) are considered. Defaults to - * false *) + * false + * @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 locate: dbd:Mysql.dbd -> ?vars:bool -> string -> string list