diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-22 21:32:03 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-22 21:32:03 +0000 |
commit | 937ca7a6dbc1a031b7c4540c665b8774440c1bb9 (patch) | |
tree | 3a2c73669cb40011c2e62a11d3364d39f74040ba /library/nametab.ml | |
parent | de9150e6033467fd2fa8fc93d5f057e8c2f6537f (diff) |
Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 'section_path' pour les noms absolus
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@919 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/nametab.ml')
-rwxr-xr-x | library/nametab.ml | 51 |
1 files changed, 26 insertions, 25 deletions
diff --git a/library/nametab.ml b/library/nametab.ml index 8e15870e0..c45e7d93e 100755 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -7,65 +7,66 @@ open Libobject open Declarations open Term -type cci_table = global_reference Idmap.t -type obj_table = (section_path * obj) Idmap.t +type cci_table = global_reference Stringmap.t +type obj_table = (section_path * obj) Stringmap.t type mod_table = module_contents Stringmap.t and module_contents = Closed of cci_table * obj_table * mod_table let mod_tab = ref (Stringmap.empty : mod_table) -let cci_tab = ref (Idmap.empty : cci_table) -let obj_tab = ref (Idmap.empty : obj_table) +let cci_tab = ref (Stringmap.empty : cci_table) +let obj_tab = ref (Stringmap.empty : obj_table) -let sp_of_id _ id = Idmap.find id !cci_tab +let sp_of_id _ id = Stringmap.find (string_of_id id) !cci_tab let constant_sp_of_id id = - match Idmap.find id !cci_tab with + match Stringmap.find (string_of_id id) !cci_tab with | ConstRef sp -> sp | _ -> raise Not_found -let push_cci id sp = cci_tab := Idmap.add id sp !cci_tab -let push_obj id sp = obj_tab := Idmap.add id sp !obj_tab -let push_module id mc = mod_tab := Stringmap.add id mc !mod_tab +let push_cci s sp = cci_tab := Stringmap.add s sp !cci_tab +let push_obj s sp = obj_tab := Stringmap.add s sp !obj_tab +let push_module s mc = mod_tab := Stringmap.add s mc !mod_tab -let push = push_cci +let push_object id = push_obj (string_of_id id) +let push id = push_cci (string_of_id id) -let locate sp = - let (dir,id,_) = repr_path sp in +let locate qid = + let (dir,id) = repr_qualid qid in let rec search (ccitab,modtab) = function | id :: dir' -> let (Closed (ccitab, _, modtab)) = Stringmap.find id modtab in search (ccitab,modtab) dir' - | [] -> Idmap.find id ccitab + | [] -> Stringmap.find id ccitab in search (!cci_tab,!mod_tab) dir -let locate_obj sp = - let (dir,id,_) = repr_path sp in +let locate_obj qid = + let (dir,id) = repr_qualid qid in let rec search (objtab,modtab) = function | id :: dir' -> let (Closed (_, objtab, modtab)) = Stringmap.find id modtab in search (objtab,modtab) dir' - | [] -> Idmap.find id objtab + | [] -> Stringmap.find id objtab in search (!obj_tab,!mod_tab) dir -let locate_constant sp = - match locate sp with +let locate_constant qid = + match locate qid with | ConstRef sp -> sp | _ -> raise Not_found -let open_module_contents id = - let (Closed (ccitab,objtab,modtab)) = Stringmap.find id !mod_tab in - Idmap.iter push_cci ccitab; - Idmap.iter (fun _ -> Libobject.open_object) objtab; +let open_module_contents s = + let (Closed (ccitab,objtab,modtab)) = Stringmap.find s !mod_tab in + Stringmap.iter push_cci ccitab; + Stringmap.iter (fun _ -> Libobject.open_object) objtab; Stringmap.iter push_module modtab (* Registration as a global table and roolback. *) let init () = - cci_tab := Idmap.empty; - obj_tab := Idmap.empty; + cci_tab := Stringmap.empty; + obj_tab := Stringmap.empty; mod_tab := Stringmap.empty; -type frozen = cci_table Idmap.t * obj_table Idmap.t * mod_table Stringmap.t +type frozen = cci_table Stringmap.t * obj_table Stringmap.t * mod_table Stringmap.t let freeze () = (!cci_tab, !obj_tab, !mod_tab) |