From 3d45448d06307244c530a9e52d33e4a3723eec55 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 1 Feb 2005 15:21:20 +0000 Subject: [PATCH] added owner support to the disambiguator (now locate finds only objects of the current owner). --- helm/ocaml/cic_disambiguation/disambiguate.ml | 8 ++++---- helm/ocaml/cic_disambiguation/disambiguate.mli | 1 + helm/ocaml/tactics/metadataQuery.ml | 18 +++++++++++++++--- helm/ocaml/tactics/metadataQuery.mli | 2 +- 4 files changed, 21 insertions(+), 8 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index aafbeb777..b36ae5b11 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -421,8 +421,8 @@ let domain_diff dom1 dom2 = module Make (C: Callbacks) = struct - let choices_of_id dbd id = - let uris = MetadataQuery.locate ~dbd id in + let choices_of_id ?owner dbd id = + let uris = MetadataQuery.locate ?owner ~dbd id in let uris = match uris with | [] -> @@ -452,7 +452,7 @@ module Make (C: Callbacks) = uris let disambiguate_term ~(dbd:Mysql.dbd) context metasenv term - ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env + ?(initial_ugraph = CicUniv.empty_ugraph) ?owner ~aliases:current_env = debug_print "NEW DISAMBIGUATE INPUT"; let disambiguate_context = (* cic context -> disambiguate context *) @@ -477,7 +477,7 @@ module Make (C: Callbacks) = (try Hashtbl.find id_choices id with Not_found -> - let choices = choices_of_id dbd id in + let choices = choices_of_id ?owner dbd id in Hashtbl.add id_choices id choices; choices) | Symbol (symb, _) -> DisambiguateChoices.lookup_symbol_choices symb diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli index b0fe0fcd3..b240ea035 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.mli +++ b/helm/ocaml/cic_disambiguation/disambiguate.mli @@ -37,6 +37,7 @@ module Make (C : Callbacks) : Cic.metasenv -> CicAst.term -> ?initial_ugraph:CicUniv.universe_graph -> + ?owner:string -> aliases:environment -> (* previous interpretation status *) (environment * (* new interpretation status *) Cic.metasenv * (* new metasenv *) diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index f65318896..4e6b31b53 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -46,11 +46,23 @@ let nonvar s = let suffix = String.sub s (len-4) 4 in not (suffix = ".var") -let locate ~(dbd:Mysql.dbd) ?(vars = false) pat = +let locate ~(dbd:Mysql.dbd) ?(vars = false) ?owner pat = let sql_pat = sqlpat_of_shellglob pat in let query = - sprintf "SELECT source FROM %s WHERE value LIKE \"%s\"" - MetadataTypes.name_tbl sql_pat + match owner with + | None -> + sprintf "SELECT source FROM %s WHERE value LIKE \"%s\"" + MetadataTypes.name_tbl sql_pat + | Some owner -> + sprintf "SELECT %s.source FROM %s,%s WHERE + (%s.source LIKE CONCAT(%s.source,\"#%%\") OR + %s.source = %s.source) AND + value LIKE \"%s\" AND owner = \"%s\"" + MetadataTypes.name_tbl + MetadataTypes.name_tbl MetadataTypes.owners_tbl + MetadataTypes.name_tbl MetadataTypes.owners_tbl + MetadataTypes.name_tbl MetadataTypes.owners_tbl + sql_pat owner 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 0d32e4835..4ae870a4f 100644 --- a/helm/ocaml/tactics/metadataQuery.mli +++ b/helm/ocaml/tactics/metadataQuery.mli @@ -29,7 +29,7 @@ * is interpreted as 0 or more characters and "?" as exactly one character *) val locate: dbd:Mysql.dbd -> - ?vars:bool -> string -> string list + ?vars:bool -> ?owner:string -> string -> string list val hint: dbd:Mysql.dbd -> -- 2.39.2