diff options
-rw-r--r-- | library/declare.ml | 76 | ||||
-rw-r--r-- | library/declare.mli | 4 | ||||
-rw-r--r-- | library/lib.ml | 2 | ||||
-rw-r--r-- | library/lib.mli | 1 | ||||
-rwxr-xr-x | library/nametab.ml | 25 | ||||
-rwxr-xr-x | library/nametab.mli | 4 | ||||
-rw-r--r-- | parsing/prettyp.ml | 2 | ||||
-rw-r--r-- | toplevel/class.ml | 2 | ||||
-rw-r--r-- | toplevel/command.ml | 6 | ||||
-rw-r--r-- | toplevel/discharge.ml | 6 |
10 files changed, 76 insertions, 52 deletions
diff --git a/library/declare.ml b/library/declare.ml index 7bede5758..9b6466f47 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -25,27 +25,43 @@ open Indrec open Nametab open Library +(* For [DischargeAt (dir,n)], [dir] is the minimum prefix that a + construction keeps in its name (if persistent), or the section name + beyond which it is discharged (if volatile); the integer [n] + (useful only for persistent constructions), is the length of the section + part in [dir] *) + type strength = | NotDeclare - | DischargeAt of dir_path + | DischargeAt of dir_path * int | NeverDischarge -let make_strength = function - | [] -> NeverDischarge - | l -> DischargeAt l +let depth_of_strength = function + | DischargeAt (sp',n) -> n + | NeverDischarge -> 0 + | NotDeclare -> assert false + +let restrict_path n sp = + let dir, s, k = repr_path sp in + let dir' = list_lastn n dir in + Names.make_path dir' s k -let make_strength_0 () = make_strength (Lib.cwd()) +let make_strength_0 () = + let depth = Lib.sections_depth () in + let cwd = Lib.cwd() in + if depth > 0 then DischargeAt (cwd, depth) else NeverDischarge let make_strength_1 () = + let depth = Lib.sections_depth () in let cwd = Lib.cwd() in - let path = try list_firstn (List.length cwd - 1) cwd with Failure _ -> [] in - make_strength path + if depth > 1 then DischargeAt (list_firstn (List.length cwd -1) cwd, depth-1) + else NeverDischarge let make_strength_2 () = + let depth = Lib.sections_depth () in let cwd = Lib.cwd() in - let path = try list_firstn (List.length cwd - 2) cwd with Failure _ -> [] in - make_strength path - + if depth > 2 then DischargeAt (list_firstn (List.length cwd -2) cwd, depth-2) + else NeverDischarge (* Section variables. *) @@ -76,9 +92,6 @@ let _ = Summary.declare_summary "VARIABLE" Summary.survive_section = false } let cache_variable (sp,(id,(d,str,sticky))) = -(* - if Nametab.exists_cci sp then -*) (* Constr raisonne sur les noms courts *) if List.mem_assoc id (current_section_context ()) then errorlabstrm "cache_variable" @@ -87,7 +100,7 @@ let cache_variable (sp,(id,(d,str,sticky))) = | SectionLocalAssum ty -> Global.push_named_assum (id,ty) | SectionLocalDef c -> Global.push_named_def (id,c) in - Nametab.push_short_name sp (VarRef sp); + Nametab.push 0 (restrict_path 0 sp) (VarRef sp); vartab := let (m,l) = !vartab in (Spmap.add sp (id,(vd,str,sticky)) m, sp::l) let (in_variable, out_variable) = @@ -111,17 +124,16 @@ let cache_parameter (sp,c) = errorlabstrm "cache_parameter" [< pr_id (basename sp); 'sTR " already exists" >]; Global.add_parameter sp c (current_section_context ()); - Nametab.push sp (ConstRef sp); - Nametab.push_short_name sp (ConstRef sp) + Nametab.push 0 sp (ConstRef sp) let load_parameter (sp,_) = if Nametab.exists_cci sp then errorlabstrm "cache_parameter" [< pr_id (basename sp); 'sTR " already exists" >]; - Nametab.push sp (ConstRef sp) + Nametab.push 1 sp (ConstRef sp) let open_parameter (sp,_) = - Nametab.push_short_name sp (ConstRef sp) + Nametab.push 0 (restrict_path 0 sp) (ConstRef sp) (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_parameter_entry = mkProp @@ -169,25 +181,31 @@ let cache_constant (sp,(cdt,stre,op)) = | ConstantEntry ce -> Global.add_constant sp ce sc | ConstantRecipe r -> Global.add_discharged_constant sp r sc end; - Nametab.push sp (ConstRef sp); (match stre with - (* Remark & Fact outside their scope aren't visible without qualif *) - | DischargeAt sp' when not (is_dirpath_prefix_of sp' (Lib.cwd ())) -> () - (* Theorem, Lemma & Definition are accessible from the base name *) - | NeverDischarge| DischargeAt _ -> Nametab.push_short_name sp (ConstRef sp) + | DischargeAt (sp',n) when not (is_dirpath_prefix_of sp' (Lib.cwd ())) -> + (* Only qualifications including the sections segment from the current + section to the discharge section is available for Remark & Fact *) + Nametab.push (n-Lib.sections_depth()) sp (ConstRef sp) + | (NeverDischarge| DischargeAt _) -> + (* All qualifications of Theorem, Lemma & Definition are visible *) + Nametab.push 0 sp (ConstRef sp) | NotDeclare -> assert false); if op then Global.set_opaque sp; csttab := Spmap.add sp stre !csttab +(* At load-time, the segment starting from the module name to the discharge *) +(* section (if Remark or Fact) is needed to access a construction *) let load_constant (sp,(ce,stre,op)) = if Nametab.exists_cci sp then errorlabstrm "cache_constant" [< pr_id (basename sp); 'sTR " already exists" >] ; csttab := Spmap.add sp stre !csttab; - Nametab.push sp (ConstRef sp) + Nametab.push (depth_of_strength stre + 1) sp (ConstRef sp) -let open_constant (sp,_) = - Nametab.push_short_name sp (ConstRef sp) +(* Opening means making the name without its module qualification available *) +let open_constant (sp,(_,stre,_)) = + let n = depth_of_strength stre in + Nametab.push n (restrict_path n sp) (ConstRef sp) (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_constant_entry = ConstantEntry { @@ -252,17 +270,17 @@ let cache_inductive (sp,mie) = 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 sp ref) + (fun (sp, ref) -> Nametab.push 0 sp ref) names let load_inductive (sp,mie) = let names = inductive_names sp mie in List.iter check_exists_inductive names; - List.iter (fun (sp, ref) -> Nametab.push sp ref) names + List.iter (fun (sp, ref) -> Nametab.push 1 sp ref) names let open_inductive (sp,mie) = let names = inductive_names sp mie in - List.iter (fun (sp, ref) -> Nametab.push_short_name sp ref) names + List.iter (fun (sp, ref) -> Nametab.push 0 (restrict_path 0 sp) ref) names let dummy_one_inductive_entry mie = { mind_entry_nparams = 0; diff --git a/library/declare.mli b/library/declare.mli index 08c45f462..b347456ce 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -26,7 +26,7 @@ open Library type strength = | NotDeclare - | DischargeAt of dir_path + | DischargeAt of dir_path * int | NeverDischarge type section_variable_entry = @@ -67,7 +67,7 @@ val declare_eliminations : mutual_inductive_path -> unit val out_inductive : Libobject.obj -> mutual_inductive_entry -val make_strength : dir_path -> strength +(*val make_strength : dir_path -> strength*) val make_strength_0 : unit -> strength val make_strength_1 : unit -> strength val make_strength_2 : unit -> strength diff --git a/library/lib.ml b/library/lib.ml index 94cba5e0c..c6ebfa000 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -64,6 +64,8 @@ let pop_path_prefix () = let make_path id k = Names.make_path !path_prefix id k +let sections_depth () = List.length !path_prefix - List.length (module_sp ()) + let cwd () = !path_prefix let find_entry_p p = diff --git a/library/lib.mli b/library/lib.mli index 27fec78bf..0421f0812 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -55,6 +55,7 @@ val sections_are_opened : unit -> bool val make_path : identifier -> path_kind -> section_path val cwd : unit -> dir_path +val sections_depth : unit -> int val is_section_p : dir_path -> bool (* This is to declare the interactive toplevel default module name as a root*) diff --git a/library/nametab.ml b/library/nametab.ml index 1fadea6ae..979c9f2dc 100755 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -90,11 +90,9 @@ let dirpath_of_extended_ref = function "Root.Rep.Lib.name", but not "name" are pushed; which means, visibility is always 1 *) -let visibility = 1 - (* 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 extract_dirpath tab dir o = +let push_tree extract_dirpath tab visibility dir o = let rec push level (current,dirmap) = function | modid :: path as dir -> let mc = @@ -114,11 +112,11 @@ let push_tree extract_dirpath tab dir o = | [] -> (Some o,dirmap) in push 0 tab (List.rev dir) -let push_idtree extract_dirpath tab dir id o = +let push_idtree extract_dirpath tab n dir id o = let modtab = try Idmap.find id !tab with Not_found -> (None, ModIdmap.empty) in - tab := Idmap.add id (push_tree extract_dirpath modtab dir o) !tab + tab := Idmap.add id (push_tree extract_dirpath modtab n dir o) !tab 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 @@ -128,7 +126,7 @@ 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 (fun x -> x) modtab dir o) !tab + tab := ModIdmap.add id (push_tree (fun x -> x) modtab 0 dir o) !tab let push_long_names_secpath = push_modidtree the_sectab let push_long_names_libpath = push_modidtree the_libtab @@ -139,32 +137,35 @@ let push_long_names_libpath = push_modidtree the_libtab possibly limited visibility, i.e. Theorem, Lemma, Definition, Axiom, Parameter but also Remark and Fact) *) -let push_cci sp ref = +let push_cci n sp ref = let dir, s = repr_qualid (qualid_of_sp sp) in (* We push partially qualified name (with at least one prefix) *) - push_long_names_ccipath dir s (TrueGlobal ref) + push_long_names_ccipath n dir s (TrueGlobal ref) let push = push_cci +(* let push_short_name sp ref = (* We push a volatile unqualified name *) - push_short_name_ccipath [] (basename sp) (TrueGlobal ref) + push_short_name_ccipath 0 [] (basename sp) (TrueGlobal ref) +*) (* This is for Syntactic Definitions *) let push_syntactic_definition sp = let dir, s = repr_qualid (qualid_of_sp sp) in - push_long_names_ccipath dir s (SyntacticDef sp) + push_long_names_ccipath 0 dir s (SyntacticDef sp) let push_short_name_syntactic_definition sp = let _, s = repr_qualid (qualid_of_sp sp) in - push_short_name_ccipath [] s (SyntacticDef sp) + push_short_name_ccipath Pervasives.max_int [] s (SyntacticDef sp) (* This is for dischargeable non-cci objects (removed at the end of the section -- i.e. Hints, Grammar ...) *) (* --> Unused *) let push_short_name_object sp = - push_short_name_objpath [] (basename sp) sp + let _, s = repr_qualid (qualid_of_sp sp) in + push_short_name_objpath 0 [] s sp (* This is to remember absolute Section/Module names and to avoid redundancy *) diff --git a/library/nametab.mli b/library/nametab.mli index 6989e6bbf..f525d49c7 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -45,11 +45,13 @@ 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 : visibility:int -> 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 : section_path -> global_reference -> unit +*) val push_short_name_syntactic_definition : section_path -> unit val push_short_name_object : section_path -> unit diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 93751cf5d..322a61af7 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -532,7 +532,7 @@ open Classops let string_of_strength = function | NotDeclare -> "(temp)" | NeverDischarge -> "(global)" - | DischargeAt sp -> "(disch@"^(string_of_dirpath sp) + | DischargeAt (sp,_) -> "(disch@"^(string_of_dirpath sp) let print_coercion_value v = prterm (get_coercion_value v) diff --git a/toplevel/class.ml b/toplevel/class.ml index 667e12706..3fb0f67a5 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -36,7 +36,7 @@ let stre_gt = function | (NotDeclare,_) -> false | (_,NeverDischarge) -> true | (_,NotDeclare) -> true - | (DischargeAt sp1,DischargeAt sp2) -> + | (DischargeAt (sp1,_),DischargeAt (sp2,_)) -> is_dirpath_prefix_of sp1 sp2 (* was sp_gt but don't understand why - HH *) diff --git a/toplevel/command.ml b/toplevel/command.ml index f53f26b8d..f290d684b 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -75,7 +75,7 @@ let definition_body_red red_option ident (local,n) com comtypeopt = let ce' = red_constant_entry ce red_option in match n with | NeverDischarge -> declare_global_definition ident ce' n local - | DischargeAt disch_sp -> + | DischargeAt (disch_sp,_) -> if Lib.is_section_p disch_sp then begin let c = constr_of_constr_entry ce' in let sp = declare_variable ident (SectionLocalDef c,n,false) in @@ -115,7 +115,7 @@ let declare_global_assumption ident c = let hypothesis_def_var is_refining ident n c = match n with | NeverDischarge -> declare_global_assumption ident c - | DischargeAt disch_sp -> + | DischargeAt (disch_sp,_) -> if Lib.is_section_p disch_sp then begin let t = interp_type Evd.empty (Global.env()) c in let sp = declare_variable ident (SectionLocalAssum t,n,false) in @@ -437,7 +437,7 @@ let apply_tac_not_declare id pft = function let save opacity id ({const_entry_body = pft; const_entry_type = tpo} as const) strength = begin match strength with - | DischargeAt disch_sp when Lib.is_section_p disch_sp && not opacity -> + | DischargeAt (disch_sp,_) when Lib.is_section_p disch_sp && not opacity -> let c = constr_of_constr_entry const in let _ = declare_variable id (SectionLocalDef c,strength,opacity) in () | NeverDischarge | DischargeAt _ -> diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 730817bf3..819df64e0 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -218,7 +218,7 @@ let process_object oldenv dir sec_sp let cb = Environ.lookup_constant sp oldenv in let imp = is_implicit_constant sp in let newsp = match stre with - | DischargeAt d when not (is_dirpath_prefix_of d dir) -> sp + | DischargeAt (d,_) when not (is_dirpath_prefix_of d dir) -> sp | _ -> recalc_sp dir sp in let mods = let modl = build_abstract_list cb.const_hyps ids_to_discard in @@ -241,7 +241,7 @@ let process_object oldenv dir sec_sp | "CLASS" -> let ((cl,clinfo) as x) = outClass lobj in - if clinfo.cl_strength = (DischargeAt sec_sp) then + if (match clinfo.cl_strength with DischargeAt (sp,_) -> sp = sec_sp | _ -> false) then (ops,ids_to_discard,work_alist) else let (y1,y2) = process_class sec_sp ids_to_discard x in @@ -249,7 +249,7 @@ let process_object oldenv dir sec_sp | "COERCION" -> let (((_,coeinfo),_,_)as x) = outCoercion lobj in - if coercion_strength coeinfo = (DischargeAt sec_sp) then + if (match coercion_strength coeinfo with DischargeAt (sp,_) -> sp = sec_sp | _ -> false) then (ops,ids_to_discard,work_alist) else let y = process_coercion sec_sp ids_to_discard x in |