From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 1 Feb 2005 15:21:20 +0000 (+0000)
Subject: added owner support to the disambiguator (now locate finds only objects
X-Git-Tag: V_0_1_0~72
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3d45448d06307244c530a9e52d33e4a3723eec55;p=helm.git

added owner support to the disambiguator (now locate finds only objects
of the current owner).
---

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 ->