diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-07 13:07:17 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-07 13:07:17 +0000 |
commit | 47d1e4d9d09dee1fccce3e2d7b1c7330440bd318 (patch) | |
tree | 05b1a2c365530a8b517f1ac8a678900b9e3066b3 | |
parent | 18e28049e62ce80a45c8f7bd6f496b502caa8ad1 (diff) |
Suppression des library roots, on teste si un nom est absolu autrement
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1927 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | library/declare.ml | 17 | ||||
-rw-r--r-- | library/library.ml | 17 | ||||
-rwxr-xr-x | library/nametab.ml | 108 | ||||
-rwxr-xr-x | library/nametab.mli | 6 | ||||
-rw-r--r-- | toplevel/errors.ml | 3 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 9 | ||||
-rw-r--r-- | toplevel/vernacinterp.ml | 2 |
7 files changed, 91 insertions, 71 deletions
diff --git a/library/declare.ml b/library/declare.ml index ca1cea16a..1c9875718 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -82,7 +82,7 @@ let cache_variable (sp,(id,(d,_,_) as vd)) = | SectionLocalAssum ty -> Global.push_named_assum (id,ty) | SectionLocalDef c -> Global.push_named_def (id,c) end; - Nametab.push_short_name id (VarRef sp); + Nametab.push_short_name sp (VarRef sp); vartab := let (m,l) = !vartab in (Spmap.add sp vd m, sp::l) let (in_variable, out_variable) = @@ -107,7 +107,7 @@ let cache_parameter (sp,c) = [< pr_id (basename sp); 'sTR " already exists" >]; Global.add_parameter sp c (current_section_context ()); Nametab.push sp (ConstRef sp); - Nametab.push_short_name (basename sp) (ConstRef sp) + Nametab.push_short_name sp (ConstRef sp) let load_parameter (sp,_) = if Nametab.exists_cci sp then @@ -116,7 +116,7 @@ let load_parameter (sp,_) = Nametab.push sp (ConstRef sp) let open_parameter (sp,_) = - Nametab.push_short_name (basename sp) (ConstRef sp) + Nametab.push_short_name sp (ConstRef sp) let export_parameter x = Some x @@ -162,7 +162,7 @@ let cache_constant (sp,(cdt,stre,op)) = | ConstantRecipe r -> Global.add_discharged_constant sp r sc end; Nametab.push sp (ConstRef sp); - Nametab.push_short_name (basename sp) (ConstRef sp); + Nametab.push_short_name sp (ConstRef sp); if op then Global.set_opaque sp; csttab := Spmap.add sp stre !csttab @@ -174,7 +174,7 @@ let load_constant (sp,(ce,stre,op)) = Nametab.push sp (ConstRef sp) let open_constant (sp,_) = - Nametab.push_short_name (basename sp) (ConstRef sp) + Nametab.push_short_name sp (ConstRef sp) (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_constant_entry = ConstantEntry { @@ -234,8 +234,9 @@ let cache_inductive (sp,mie) = let names = inductive_names sp mie in List.iter check_exists_inductive names; Global.add_mind sp mie (current_section_context ()); - List.iter (fun (sp, ref) -> Nametab.push sp ref; Nametab.push_short_name - (basename sp) ref) names + List.iter + (fun (sp, ref) -> Nametab.push sp ref; Nametab.push_short_name sp ref) + names let load_inductive (sp,mie) = let names = inductive_names sp mie in @@ -244,7 +245,7 @@ let load_inductive (sp,mie) = let open_inductive (sp,mie) = let names = inductive_names sp mie in - List.iter (fun (sp, ref) -> Nametab.push_short_name (basename sp) ref) names + List.iter (fun (sp, ref) -> Nametab.push_short_name sp ref) names let dummy_one_inductive_entry mie = { mind_entry_nparams = 0; diff --git a/library/library.ml b/library/library.ml index 5556bf32e..bc95496bc 100644 --- a/library/library.ml +++ b/library/library.ml @@ -271,7 +271,7 @@ and load_absolute_module_from dir = [< 'sTR"Cannot find module "; pr_dirpath dir; 'sTR" in loadpath">] | _ -> assert false -let try_locate_qualified_library qid = +let locate_qualified_library qid = (* Look if loaded *) try let dir = Nametab.locate_loaded_library qid in @@ -282,12 +282,9 @@ let try_locate_qualified_library qid = let dir, base = repr_qualid qid in let loadpath = if dir = [] then get_load_path () - else if is_absolute_dirpath dir then + else + (* we assume dir is an absolute dirpath *) load_path_of_logical_path dir - else - error - ("Not loaded partially qualified library names not implemented: " - ^(string_of_qualid qid)) in if loadpath = [] then raise LibUnmappedDir; let name = (string_of_id base)^".vo" in @@ -295,9 +292,9 @@ let try_locate_qualified_library qid = (LibInPath, find_logical_path path@[base], file) with Not_found -> raise LibNotFound -let locate_qualified_library qid = +let try_locate_qualified_library qid = try - try_locate_qualified_library qid + locate_qualified_library qid with | LibUnmappedDir -> let prefix, id = repr_qualid qid in @@ -346,10 +343,10 @@ let locate_module qid = function locate_by_filename_only (Some id) f | None -> (* No name, we need to find the file name *) - locate_qualified_library qid + try_locate_qualified_library qid let read_module qid = - ignore (load_module (locate_qualified_library qid)) + ignore (load_module (try_locate_qualified_library qid)) let read_module_from_file f = let _, f = System.find_file_in_path (get_load_path ()) (f^".vo") in diff --git a/library/nametab.ml b/library/nametab.ml index 3d7ca98f4..a33bb9705 100755 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -32,20 +32,27 @@ let qualid_of_dirpath dir = make_qualid l a exception GlobalizationError of qualid +exception GlobalizationConstantError of qualid let error_global_not_found_loc loc q = Stdpp.raise_with_loc loc (GlobalizationError q) +let error_global_constant_not_found_loc loc q = + Stdpp.raise_with_loc loc (GlobalizationConstantError q) + let error_global_not_found q = raise (GlobalizationError q) (*s Roots of the space of absolute names *) -let roots = ref [] -let push_library_root s = roots := list_add_set s !roots - let coq_root = id_of_string "Coq" let default_root_prefix = [] +(* Obsolète +let roots = ref [] +let push_library_root s = roots := list_add_set s !roots +*) +let push_library_root s = () + (* Constructions and syntactic definitions live in the same space *) type extended_global_reference = | TrueGlobal of global_reference @@ -61,6 +68,16 @@ let the_libtab = ref (ModIdmap.empty : dirtab) let the_sectab = ref (ModIdmap.empty : dirtab) let the_objtab = ref (Idmap.empty : objtab) +let dirpath_of_reference = function + | ConstRef sp -> dirpath sp + | VarRef sp -> dirpath sp + | ConstructRef ((sp,_),_) -> dirpath sp + | IndRef (sp,_) -> dirpath sp + +let dirpath_of_extended_ref = function + | TrueGlobal ref -> dirpath_of_reference ref + | SyntacticDef sp -> dirpath sp + (* How necessarily_open works: concretely, roots and directory are always open but libraries are open only during their interactive construction or on demand if a precompiled one; then for a name @@ -69,33 +86,41 @@ let the_objtab = ref (Idmap.empty : objtab) (* We add a binding of [[modid1;...;modidn;id]] to [o] in the name tab *) (* We proceed in the reverse way, looking first to [id] *) -let push_tree tab dir o = +let push_tree extract_dirpath tab dir o = let rec push necessarily_open (current,dirmap) = function | modid :: path as dir -> let mc = try ModIdmap.find modid dirmap with Not_found -> (None, ModIdmap.empty) in - let this = if necessarily_open then Some o else current in + let this = + if necessarily_open then + if option_app extract_dirpath current = Some dir then + (* This is an absolute name, we must keep it otherwise it may + become unaccessible forever *) + current + else + Some o + else current in (this, ModIdmap.add modid (push true mc path) dirmap) | [] -> (Some o,dirmap) in push false tab (List.rev dir) -let push_idtree tab dir id o = +let push_idtree extract_dirpath tab dir id o = let modtab = try Idmap.find id !tab with Not_found -> (None, ModIdmap.empty) in - tab := Idmap.add id (push_tree modtab dir o) !tab + tab := Idmap.add id (push_tree extract_dirpath modtab dir o) !tab -let push_long_names_ccipath = push_idtree the_ccitab -let push_short_name_ccipath = push_idtree the_ccitab -let push_short_name_objpath = push_idtree the_objtab +let push_long_names_ccipath = push_idtree dirpath_of_extended_ref the_ccitab +let push_short_name_ccipath = push_idtree dirpath_of_extended_ref the_ccitab +let push_short_name_objpath = push_idtree dirpath the_objtab let push_modidtree tab dir id o = let modtab = try ModIdmap.find id !tab with Not_found -> (None, ModIdmap.empty) in - tab := ModIdmap.add id (push_tree modtab dir o) !tab + tab := ModIdmap.add id (push_tree (fun x -> x) modtab dir o) !tab let push_long_names_secpath = push_modidtree the_sectab let push_long_names_libpath = push_modidtree the_libtab @@ -113,9 +138,9 @@ let push_cci sp ref = let push = push_cci -let push_short_name id ref = +let push_short_name sp ref = (* We push a volatile unqualified name *) - push_short_name_ccipath [] id (TrueGlobal ref) + push_short_name_ccipath [] (basename sp) (TrueGlobal ref) (* This is for Syntactic Definitions *) @@ -142,7 +167,6 @@ let push_section fulldir = push_long_names_secpath [] s fulldir (* These are entry points to locate names *) -(* If the name starts with the coq_root name, then it is an absolute name *) let locate_in_tree tab dir = let dir = List.rev dir in let rec search (current,modidtab) = function @@ -185,8 +209,10 @@ let locate_section qid = (* Derived functions *) let locate_constant qid = + (* TODO: restrict to defined constants *) match locate_cci qid with | TrueGlobal (ConstRef sp) -> sp + | TrueGlobal (VarRef sp) -> sp | _ -> raise Not_found let sp_of_id _ id = match locate_cci (make_qualid [] id) with @@ -200,6 +226,7 @@ let constant_sp_of_id id = | TrueGlobal (ConstRef sp) -> sp | _ -> raise Not_found +(* let check_absoluteness dir = match dir with | a::_ when List.mem a !roots -> () @@ -216,34 +243,19 @@ let absolute_reference sp = let locate_in_absolute_module dir id = check_absoluteness dir; locate (make_qualid dir id) - -(* -(* These are entry points to make the contents of a module/section visible *) -(* in the current env (does not affect the absolute name space `coq_root') *) -let open_module_contents qid = - let _, (Closed (ccitab,objtab,modtab)) = locate_module qid in - Idmap.iter push_cci_current ccitab; -(* Idmap.iter (fun _ -> Libobject.open_object) objtab;*) - Stringmap.iter push_mod_current modtab - -let conditional_push ref = push_cci_current ref (* TODO *) - -let open_section_contents qid = - let _, (Closed (ccitab,objtab,modtab)) = locate_module qid in - Idmap.iter push_cci_current ccitab; -(* Idmap.iter (fun _ -> Libobject.open_object) objtab;*) - Stringmap.iter push_mod_current modtab - -let rec rec_open_module_contents qid = - let _, (Closed (ccitab,objtab,modtab)) = locate_module qid in - Idmap.iter push_cci_current ccitab; -(* Idmap.iter (fun _ -> Libobject.open_object) objtab;*) - Stringmap.iter - (fun m (sp,_ as mt) -> - push_mod_current m mt; - rec_open_module_contents (qualid_of_sp sp)) - modtab *) + +let absolute_reference sp = + let a = locate_cci (qualid_of_sp sp) in + if not (dirpath_of_extended_ref a = dirpath sp) then + anomaly ("Not an absolute path: "^(string_of_path sp)); + match a with + | TrueGlobal ref -> ref + | _ -> raise Not_found + +let locate_in_absolute_module dir id = + absolute_reference (make_path dir id CCI) + let exists_cci sp = try let _ = locate_cci (qualid_of_sp sp) in true with Not_found -> false @@ -263,22 +275,22 @@ let init () = the_ccitab := Idmap.empty; the_libtab := ModIdmap.empty; the_sectab := ModIdmap.empty; - the_objtab := Idmap.empty; - roots := [] + the_objtab := Idmap.empty +(* ;roots := []*) let freeze () = !the_ccitab, !the_libtab, !the_sectab, - !the_objtab, - !roots + !the_objtab +(* ,!roots*) -let unfreeze (mc,ml,ms,mo,r) = +let unfreeze (mc,ml,ms,mo(*,r*)) = the_ccitab := mc; the_libtab := ml; the_sectab := ms; - the_objtab := mo; - roots := r + the_objtab := mo(*; + roots := r*) let _ = Summary.declare_summary "names" diff --git a/library/nametab.mli b/library/nametab.mli index 927205dea..6989e6bbf 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -37,17 +37,19 @@ val pr_qualid : qualid -> std_ppcmds val qualid_of_sp : section_path -> qualid exception GlobalizationError of qualid +exception GlobalizationConstantError of qualid (* Raises a globalization error *) val error_global_not_found_loc : loc -> qualid -> 'a val error_global_not_found : qualid -> 'a +val error_global_constant_not_found_loc : loc -> qualid -> 'a (*s Register visibility of absolute paths by qualified names *) val push : section_path -> global_reference -> unit val push_syntactic_definition : section_path -> unit (*s Register visibility of absolute paths by short names *) -val push_short_name : identifier -> global_reference -> unit +val push_short_name : section_path -> global_reference -> unit val push_short_name_syntactic_definition : section_path -> unit val push_short_name_object : section_path -> unit @@ -99,7 +101,9 @@ val push_library_root : module_ident -> unit references inside a block of mutual inductive *) val absolute_reference : section_path -> global_reference +(* val is_absolute_dirpath : dir_path -> bool +*) (* [locate_in_absolute_module dir id] finds [id] in module [dir] or in one of its section/subsection *) diff --git a/toplevel/errors.ml b/toplevel/errors.ml index 11e7c38cc..cf48f0764 100644 --- a/toplevel/errors.ml +++ b/toplevel/errors.ml @@ -81,6 +81,9 @@ let rec explain_exn_default = function 'sTR "The reference"; 'sPC; Nametab.pr_qualid q; 'sPC ; 'sTR "was not found"; 'sPC ; 'sTR "in the current"; 'sPC ; 'sTR "environment" >] + | Nametab.GlobalizationConstantError q -> + hOV 0 [< 'sTR "Error:"; 'sPC; + 'sTR "No constant of this name:"; 'sPC; Nametab.pr_qualid q >] | Tacmach.FailError i -> hOV 0 [< 'sTR "Error: Fail tactic always fails (level "; 'iNT i; 'sTR")." >] diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 82d31cf64..7618aadd7 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -179,11 +179,14 @@ let msg_found_library = function let msg_notfound_library qid = function | Library.LibUnmappedDir -> let dir = fst (Nametab.repr_qualid qid) in - mSG [< 'sTR "No physical path is bound to "; pr_dirpath dir; 'fNL >] + errorlabstrm "locate_library" + [< 'sTR "Cannot find a physical path bound to logical path "; + pr_dirpath dir; 'fNL >] | Library.LibNotFound -> mSG (hOV 0 - [< 'sTR"Unable to locate library"; 'sPC; Nametab.pr_qualid qid; 'fNL >]) - | _ -> assert false + [< 'sTR"Unable to locate library"; + 'sPC; Nametab.pr_qualid qid; 'fNL >]) + | e -> assert false let _ = add "LocateLibrary" diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index f1d38494f..3d170e6be 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -89,7 +89,7 @@ let rec cvt_varg ast = let q = Astterm.interp_qualid p in let sp = try Nametab.locate_constant q - with Not_found -> Nametab.error_global_not_found_loc loc q + with Not_found -> Nametab.error_global_constant_not_found_loc loc q in VARG_CONSTANT sp | Str(_,s) -> VARG_STRING s | Id(_,s) -> VARG_STRING s |