From 7b2a24d0beee17b61281a5c64fca5cf7388479d3 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 18 Feb 2005 22:17:50 +0000 Subject: Moving centralised discharge into dispatched discharge_function; required to delay some computation from before to after caching time + various simplifications and uniformisations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6748 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/declare.ml | 222 +++++++++++++++++++++---------------------- library/declare.mli | 18 ---- library/dischargedhypsmap.ml | 7 +- library/impargs.ml | 40 +++++--- library/impargs.mli | 2 + library/lib.ml | 134 ++++++++++++++++++++++++-- library/lib.mli | 24 ++++- library/libobject.ml | 12 +++ library/libobject.mli | 2 + library/library.ml | 3 + library/library.mli | 6 -- 11 files changed, 307 insertions(+), 163 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index 2109c6325..6bace2654 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -31,11 +31,7 @@ open Decl_kinds (**********************************************) -(* 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] *) +(* Strength *) open Nametab @@ -75,13 +71,16 @@ type checked_variable_declaration = let vartab = ref (Idmap.empty : checked_variable_declaration Idmap.t) let _ = Summary.declare_summary "VARIABLE" - { Summary.freeze_function = (fun () -> !vartab); - Summary.unfreeze_function = (fun ft -> vartab := ft); - Summary.init_function = (fun () -> vartab := Idmap.empty); - Summary.survive_module = false; - Summary.survive_section = false } - -let cache_variable ((sp,_),(id,(p,d,mk))) = + { Summary.freeze_function = (fun () -> !vartab); + Summary.unfreeze_function = (fun ft -> vartab := ft); + Summary.init_function = (fun () -> vartab := Idmap.empty); + Summary.survive_module = false; + Summary.survive_section = false } + +let cache_variable ((sp,_),o) = + match o with + | Inl cst -> Global.add_constraints cst + | Inr (id,(p,d,mk)) -> (* Constr raisonne sur les noms courts *) if Idmap.mem id !vartab then errorlabstrm "cache_variable" (pr_id id ++ str " already exists"); @@ -95,31 +94,33 @@ let cache_variable ((sp,_),(id,(p,d,mk))) = let (_,bd,ty) = Global.lookup_named id in CheckedSectionLocalDef (out_some bd,ty,cst,opaq) in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); + add_section_variable id; + Dischargedhypsmap.set_discharged_hyps sp []; vartab := Idmap.add id (p,vd,mk) !vartab +let get_variable_constraints id = + match pi2 (Idmap.find id !vartab) with + | CheckedSectionLocalDef (c,ty,cst,opaq) -> cst + | CheckedSectionLocalAssum (ty,cst) -> cst + +let discharge_variable (_,o) = match o with + | Inr (id,_) -> Some (Inl (get_variable_constraints id)) + | Inl _ -> Some o + let (in_variable, out_variable) = declare_object { (default_object "VARIABLE") with cache_function = cache_variable; + discharge_function = discharge_variable; classify_function = (fun _ -> Dispose) } -let declare_variable_common id obj = - let oname = add_leaf id (in_variable (id,obj)) in - declare_var_implicits id; - Notation.declare_ref_arguments_scope (VarRef id); - oname - (* for initial declaration *) let declare_variable id obj = - let (sp,kn as oname) = declare_variable_common id obj in + let oname = add_leaf id (in_variable (Inr (id,obj))) in + declare_var_implicits id; + Notation.declare_ref_arguments_scope (VarRef id); !xml_declare_variable oname; - Dischargedhypsmap.set_discharged_hyps sp []; oname -(* when coming from discharge: no xml output *) -let redeclare_variable id discharged_hyps obj = - let oname = declare_variable_common id obj in - Dischargedhypsmap.set_discharged_hyps (fst oname) discharged_hyps - (* Globals: constants and parameters *) type constant_declaration = constant_entry * global_kind @@ -133,37 +134,56 @@ let _ = Summary.declare_summary "CONSTANT" Summary.survive_module = false; Summary.survive_section = false } -let cache_constant ((sp,kn),(cdt,kind)) = - (if Idmap.mem (basename sp) !vartab then - errorlabstrm "cache_constant" - (pr_id (basename sp) ++ str " already exists")); - (if Nametab.exists_cci sp then - let (_,id) = repr_path sp in - errorlabstrm "cache_constant" (pr_id id ++ str " already exists")); - let _,dir,_ = repr_kn kn in - let kn' = Global.add_constant dir (basename sp) cdt in - if kn' <> (constant_of_kn kn) then - anomaly "Kernel and Library names do not match"; - Nametab.push (Nametab.Until 1) sp (ConstRef kn'); - csttab := Spmap.add sp kind !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 i ((sp,kn),(_,kind)) = - (if Nametab.exists_cci sp then - let (_,id) = repr_path sp in - errorlabstrm "cache_constant" (pr_id id ++ str " already exists")); - csttab := Spmap.add sp kind !csttab; - Nametab.push (Nametab.Until i) sp (ConstRef (constant_of_kn kn)) +let load_constant i ((sp,kn),(_,_,_,kind)) = + if Nametab.exists_cci sp then + errorlabstrm "cache_constant" + (pr_id (basename sp) ++ str " already exists"); + Nametab.push (Nametab.Until i) sp (ConstRef (constant_of_kn kn)); + csttab := Spmap.add sp kind !csttab (* Opening means making the name without its module qualification available *) let open_constant i ((sp,kn),_) = Nametab.push (Nametab.Exactly i) sp (ConstRef (constant_of_kn kn)) +let cache_constant ((sp,kn),(cdt,dhyps,imps,kind) as o) = + let id = basename sp in + let _,dir,_ = repr_kn kn in + if Idmap.mem id !vartab then + errorlabstrm "cache_constant" (pr_id id ++ str " already exists"); + if Nametab.exists_cci sp then + errorlabstrm "cache_constant" (pr_id id ++ str " already exists"); + let kn' = Global.add_constant dir id cdt in + assert (kn' = constant_of_kn kn); + Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn)); + add_section_constant kn' (Global.lookup_constant kn').const_hyps; + Dischargedhypsmap.set_discharged_hyps sp dhyps; + with_implicits imps declare_constant_implicits kn'; + Notation.declare_ref_arguments_scope (ConstRef kn'); + csttab := Spmap.add sp kind !csttab + +(*s Registration as global tables and rollback. *) + +open Cooking + +let discharged_hyps kn sechyps = + let (_,dir,_) = repr_kn kn in + let args = array_map_to_list destVar (instance_from_named_context sechyps) in + List.rev (List.map (Libnames.make_path dir) args) + +let discharge_constant ((sp,kn),(cdt,dhyps,imps,kind)) = + let con = constant_of_kn kn in + let cb = Global.lookup_constant con in + let (repl1,_ as repl) = replacement_context () in + let sechyps = section_segment (ConstRef con) in + let recipe = { d_from=cb; d_modlist=repl; d_abstract=sechyps } in + Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,imps,kind) + (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_constant_entry = ConstantEntry (ParameterEntry mkProp) -let dummy_constant (ce,mk) = dummy_constant_entry,mk +let dummy_constant (ce,_,imps,mk) = dummy_constant_entry,[],imps,mk let export_constant cst = Some (dummy_constant cst) @@ -176,6 +196,7 @@ let (in_constant, out_constant) = open_function = open_constant; classify_function = classify_constant; subst_function = ident_subst_function; + discharge_function = discharge_constant; export_function = export_constant } let hcons_constant_declaration = function @@ -188,12 +209,10 @@ let hcons_constant_declaration = function const_entry_boxed = ce.const_entry_boxed } | cd -> cd -let declare_constant_common id discharged_hyps (cd,kind) = - let (sp,kn as oname) = add_leaf id (in_constant (cd,kind)) in +let declare_constant_common id dhyps (cd,kind) = + let imps = implicits_flags () in + let (sp,kn as oname) = add_leaf id (in_constant (cd,dhyps,imps,kind)) in let kn = constant_of_kn kn in - declare_constant_implicits kn; - Notation.declare_ref_arguments_scope (ConstRef kn); - Dischargedhypsmap.set_discharged_hyps sp discharged_hyps; kn let declare_constant_gen internal id (cd,kind) = @@ -205,13 +224,15 @@ let declare_constant_gen internal id (cd,kind) = let declare_internal_constant = declare_constant_gen true let declare_constant = declare_constant_gen false -(* when coming from discharge *) -let redeclare_constant id discharged_hyps (cd,kind) = - let _ = declare_constant_common id discharged_hyps (GlobalRecipe cd,kind) in - () - (* Inductives. *) +let declare_inductive_argument_scopes kn mie = + list_iter_i (fun i {mind_entry_consnames=lc} -> + Notation.declare_ref_arguments_scope (IndRef (kn,i)); + for j=1 to List.length lc do + Notation.declare_ref_arguments_scope (ConstructRef ((kn,i),j)); + done) mie.mind_entry_inds + let inductive_names sp kn mie = let (dp,_) = repr_path sp in let names, _ = @@ -232,37 +253,43 @@ let inductive_names sp kn mie = ([], 0) mie.mind_entry_inds in names - let check_exists_inductive (sp,_) = (if Idmap.mem (basename sp) !vartab then - errorlabstrm "cache_inductive" + errorlabstrm "" (pr_id (basename sp) ++ str " already exists")); if Nametab.exists_cci sp then let (_,id) = repr_path sp in - errorlabstrm "cache_inductive" (pr_id id ++ str " already exists") - -let cache_inductive ((sp,kn),mie) = - let names = inductive_names sp kn mie in - List.iter check_exists_inductive names; - let _,dir,_ = repr_kn kn in - let kn' = Global.add_mind dir (basename sp) mie in - if kn' <> kn then - anomaly "Kernel and Library names do not match"; - - List.iter - (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) - names + errorlabstrm "" (pr_id id ++ str " already exists") -let load_inductive i ((sp,kn),mie) = +let load_inductive i ((sp,kn),(_,_,mie)) = let names = inductive_names sp kn mie in List.iter check_exists_inductive names; List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref) names -let open_inductive i ((sp,kn),mie) = +let open_inductive i ((sp,kn),(_,_,mie)) = let names = inductive_names sp kn mie in -(* List.iter (fun (sp, ref) -> Nametab.push 0 (restrict_path 0 sp) ref) names*) List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names +let cache_inductive ((sp,kn),(dhyps,imps,mie)) = + let names = inductive_names sp kn mie in + List.iter check_exists_inductive names; + let id = basename sp in + let _,dir,_ = repr_kn kn in + let kn' = Global.add_mind dir id mie in + assert (kn'=kn); + add_section_kn kn (Global.lookup_mind kn').mind_hyps; + Dischargedhypsmap.set_discharged_hyps sp dhyps; + with_implicits imps declare_mib_implicits kn; + declare_inductive_argument_scopes kn mie; + List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names + +let discharge_inductive ((sp,kn),(dhyps,imps,mie)) = + let mie = Global.lookup_mind kn in + let repl = replacement_context () in + let sechyps = section_segment (IndRef (kn,0)) in + Some (discharged_hyps kn sechyps,imps, + Discharge.process_inductive sechyps repl mie) + let dummy_one_inductive_entry mie = { mind_entry_params = []; mind_entry_typename = mie.mind_entry_typename; @@ -272,10 +299,10 @@ let dummy_one_inductive_entry mie = { } (* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_inductive_entry m = { +let dummy_inductive_entry (_,imps,m) = ([],imps,{ mind_entry_record = false; mind_entry_finite = true; - mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds } + mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds }) let export_inductive x = Some (dummy_inductive_entry x) @@ -286,38 +313,19 @@ let (in_inductive, out_inductive) = open_function = open_inductive; classify_function = (fun (_,a) -> Substitute (dummy_inductive_entry a)); subst_function = ident_subst_function; + discharge_function = discharge_inductive; export_function = export_inductive } -let declare_inductive_argument_scopes kn mie = - list_iter_i (fun i {mind_entry_consnames=lc} -> - Notation.declare_ref_arguments_scope (IndRef (kn,i)); - for j=1 to List.length lc do - Notation.declare_ref_arguments_scope (ConstructRef ((kn,i),j)); - done) mie.mind_entry_inds - -let declare_inductive_common mie = - let id = match mie.mind_entry_inds with - | ind::_ -> ind.mind_entry_typename - | [] -> anomaly "cannot declare an empty list of inductives" - in - let oname = add_leaf id (in_inductive mie) in - declare_mib_implicits (snd oname); - declare_inductive_argument_scopes (snd oname) mie; - oname - (* for initial declaration *) let declare_mind isrecord mie = - let (sp,kn as oname) = declare_inductive_common mie in - Dischargedhypsmap.set_discharged_hyps sp [] ; + let imps = implicits_flags () in + let id = match mie.mind_entry_inds with + | ind::_ -> ind.mind_entry_typename + | [] -> anomaly "cannot declare an empty list of inductives" in + let oname = add_leaf id (in_inductive ([],imps,mie)) in !xml_declare_inductive (isrecord,oname); oname -(* when coming from discharge: no xml output *) -let redeclare_inductive discharged_hyps mie = - let oname = declare_inductive_common mie in - Dischargedhypsmap.set_discharged_hyps (fst oname) discharged_hyps ; - oname - (*s Test and access functions. *) let is_constant sp = @@ -332,12 +340,6 @@ let get_variable id = | CheckedSectionLocalDef (c,ty,cst,opaq) -> (id,Some c,ty) | CheckedSectionLocalAssum (ty,cst) -> (id,None,ty) -let get_variable_with_constraints id = - let (p,x,_) = Idmap.find id !vartab in - match x with - | CheckedSectionLocalDef (c,ty,cst,opaq) -> ((id,Some c,ty),cst) - | CheckedSectionLocalAssum (ty,cst) -> ((id,None,ty),cst) - let variable_strength _ = Local let find_section_variable id = @@ -380,12 +382,6 @@ let mind_oper_of_id sp id mib = mip.mind_consnames) mib.mind_packets -let context_of_global_reference = function - | VarRef id -> [] - | ConstRef sp -> (Global.lookup_constant sp).const_hyps - | IndRef (sp,_) -> (Global.lookup_mind sp).mind_hyps - | ConstructRef ((sp,_),_) -> (Global.lookup_mind sp).mind_hyps - let last_section_hyps dir = fold_named_context (fun (id,_,_) sec_ids -> diff --git a/library/declare.mli b/library/declare.mli index 6af513888..c141985be 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -40,10 +40,6 @@ type variable_declaration = dir_path * section_variable_entry * local_kind val declare_variable : variable -> variable_declaration -> object_name -(* Declaration from Discharge *) -val redeclare_variable : - variable -> Dischargedhypsmap.discharged_hyps -> variable_declaration -> unit - (* Declaration of global constructions *) (* i.e. Definition/Theorem/Axiom/Parameter/... *) @@ -58,21 +54,11 @@ val declare_constant : val declare_internal_constant : identifier -> constant_declaration -> constant -val redeclare_constant : - identifier -> Dischargedhypsmap.discharged_hyps -> - Cooking.recipe * global_kind -> unit - (* [declare_mind me] declares a block of inductive types with their constructors in the current section; it returns the path of the whole block (boolean must be true iff it is a record) *) val declare_mind : bool -> mutual_inductive_entry -> object_name -(* Declaration from Discharge *) -val redeclare_inductive : - Dischargedhypsmap.discharged_hyps -> mutual_inductive_entry -> object_name - -val out_inductive : Libobject.obj -> mutual_inductive_entry - val strength_min : strength * strength -> strength val string_of_strength : strength -> string @@ -82,10 +68,7 @@ val is_constant : section_path -> bool val constant_strength : section_path -> strength val constant_kind : section_path -> global_kind -val out_variable : Libobject.obj -> identifier * variable_declaration val get_variable : variable -> named_declaration -val get_variable_with_constraints : - variable -> named_declaration * Univ.constraints val variable_strength : variable -> strength val variable_kind : variable -> local_kind val find_section_variable : variable -> section_path @@ -94,7 +77,6 @@ val clear_proofs : named_context -> named_context (*s Global references *) -val context_of_global_reference : global_reference -> section_context val strength_of_global : global_reference -> strength (* hooks for XML output *) diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml index 96ed944b2..0e7bdef30 100644 --- a/library/dischargedhypsmap.ml +++ b/library/dischargedhypsmap.ml @@ -24,13 +24,16 @@ type discharged_hyps = section_path list let discharged_hyps_map = ref Spmap.empty -let cache_discharged_hyps_map (_,(sp,hyps)) = +let load_discharged_hyps_map _ (_,(sp,hyps)) = discharged_hyps_map := Spmap.add sp hyps !discharged_hyps_map +let cache_discharged_hyps_map o = + load_discharged_hyps_map 1 o + let (in_discharged_hyps_map, _) = declare_object { (default_object "DISCHARGED-HYPS-MAP") with cache_function = cache_discharged_hyps_map; - load_function = (fun _ -> cache_discharged_hyps_map); + load_function = load_discharged_hyps_map; export_function = (fun x -> Some x) } let set_discharged_hyps sp hyps = diff --git a/library/impargs.ml b/library/impargs.ml index 8daf939ef..f41d26c99 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -55,6 +55,14 @@ let is_contextual_implicit_args () = !contextual_implicit_args type implicits_flags = (bool * bool * bool) * (bool * bool * bool) +let implicits_flags () = + (!implicit_args, + !strict_implicit_args, + !contextual_implicit_args), + (!implicit_args_out, + !strict_implicit_args_out, + !contextual_implicit_args_out) + let with_implicits ((a,b,c),(d,e,g)) f x = let oa = !implicit_args in let ob = !strict_implicit_args in @@ -342,6 +350,16 @@ let compute_var_implicits id = let var_implicits id = try Idmap.find id !var_table with Not_found -> No_impl,No_impl +(* Implicits of a global reference. *) + +let compute_global_implicits = function + | VarRef id -> compute_var_implicits id + | ConstRef kn -> compute_constant_implicits kn + | IndRef (kn,i) -> + let ((_,imps),_) = (compute_mib_implicits kn).(i) in imps + | ConstructRef ((kn,i),j) -> + let (_,cimps) = (compute_mib_implicits kn).(i) in snd cimps.(j-1) + (* Caching implicits *) let cache_implicits_decl (r,imps) = @@ -355,7 +373,15 @@ let cache_implicits_decl (r,imps) = | ConstructRef consp -> constructors_table := Constrmap.add consp imps !constructors_table -let cache_implicits (_,l) = List.iter cache_implicits_decl l +let load_implicits _ (_,l) = List.iter cache_implicits_decl l + +let cache_implicits o = + load_implicits 1 o + +(* +let discharge_implicits (_,(r,imps)) = + match r with VarRef _ -> None | _ -> Some (r,compute_global_implicits r) +*) let subst_implicits_decl subst (r,imps as o) = let r' = fst (subst_global subst r) in if r==r' then o else (r',imps) @@ -366,21 +392,11 @@ let subst_implicits (_,subst,l) = let (in_implicits, _) = declare_object {(default_object "IMPLICITS") with cache_function = cache_implicits; - load_function = (fun _ -> cache_implicits); + load_function = load_implicits; subst_function = subst_implicits; classify_function = (fun (_,x) -> Substitute x); export_function = (fun x -> Some x) } -(* Implicits of a global reference. *) - -let compute_global_implicits = function - | VarRef id -> compute_var_implicits id - | ConstRef kn -> compute_constant_implicits kn - | IndRef (kn,i) -> - let ((_,imps),_) = (compute_mib_implicits kn).(i) in imps - | ConstructRef ((kn,i),j) -> - let (_,cimps) = (compute_mib_implicits kn).(i) in snd cimps.(j-1) - let declare_implicits_gen r = add_anonymous_leaf (in_implicits [r,compute_global_implicits r]) diff --git a/library/impargs.mli b/library/impargs.mli index c1eba6923..212a93a0f 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -64,6 +64,8 @@ val is_implicit_var : variable -> implicits_flags val implicits_of_global : global_reference -> implicits_list +val implicits_flags : unit -> implicits_flags + (* For translator *) val implicits_of_global_out : global_reference -> implicits_list val is_implicit_args_out : unit -> bool diff --git a/library/lib.ml b/library/lib.ml index babb3863b..548b80d42 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -215,6 +215,7 @@ let is_something_opened = function | (_,OpenedModtype _) -> true | _ -> false +(* let export_segment seg = let rec clean acc = function | (_,CompilingLibrary _) :: _ | [] -> acc @@ -229,7 +230,7 @@ let export_segment seg = | (_,FrozenState _) :: stk -> clean acc stk in clean [] seg - +*) let start_module export id mp nametab = let dir = extend_dirpath (fst !path_prefix) id in @@ -383,6 +384,70 @@ let is_module () = (* Returns the most recent OpenedThing node *) let what_is_opened () = find_entry_p is_something_opened +(* Discharge tables *) + +let sectab = + ref ([] : (identifier list * + (identifier array Cmap.t * identifier array KNmap.t) * + (Sign.named_context Cmap.t * Sign.named_context KNmap.t)) list) + +let add_section () = + sectab := ([],(Cmap.empty,KNmap.empty),(Cmap.empty,KNmap.empty)) :: !sectab + +let add_section_variable id = + match !sectab with + | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) + | (vars,repl,abs)::sl -> sectab := (id::vars,repl,abs)::sl + +let rec extract_hyps = function + | (id::idl,(id',_,_ as d)::hyps) when id=id' -> d :: extract_hyps (idl,hyps) + | (id::idl,hyps) -> extract_hyps (idl,hyps) + | [], _ -> [] + +let add_section_replacement f g hyps = + match !sectab with + | [] -> () + | (vars,exps,abs)::sl -> + let sechyps = extract_hyps (vars,hyps) in + let args = Sign.instance_from_named_context (List.rev sechyps) in + sectab := (vars,f (Array.map Term.destVar args) exps,g sechyps abs)::sl + +let add_section_kn kn = + let f = (fun x (l1,l2) -> (l1,KNmap.add kn x l2)) in + add_section_replacement f f + +let add_section_constant kn = + let f = (fun x (l1,l2) -> (Cmap.add kn x l1,l2)) in + add_section_replacement f f + +let replacement_context () = pi2 (List.hd !sectab) + +let section_segment = function + | VarRef id -> + [] + | ConstRef con -> + Cmap.find con (fst (pi3 (List.hd !sectab))) + | IndRef (kn,_) | ConstructRef ((kn,_),_) -> + KNmap.find kn (snd (pi3 (List.hd !sectab))) + +let section_instance r = + Sign.instance_from_named_context (List.rev (section_segment r)) + +let init () = sectab := [] +let freeze () = !sectab +let unfreeze s = sectab := s + +let _ = + Summary.declare_summary "section-context" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init; + Summary.survive_module = false; + Summary.survive_section = false } + +(*************) +(* Sections. *) + (* XML output hooks *) let xml_open_section = ref (fun id -> ()) let xml_close_section = ref (fun id -> ()) @@ -390,8 +455,6 @@ let xml_close_section = ref (fun id -> ()) let set_xml_open_section f = xml_open_section := f let set_xml_close_section f = xml_close_section := f -(* Sections. *) - let open_section id = let olddir,(mp,oldsec) = !path_prefix in let dir = extend_dirpath olddir id in @@ -405,11 +468,19 @@ let open_section id = Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix); path_prefix := prefix; if !Options.xml_export then !xml_open_section id; + add_section (); prefix (* Restore lib_stk and summaries as before the section opening, and add a ClosedSection object. *) + +let discharge_item = function + | ((sp,_ as oname),Leaf lobj) -> + option_app (fun o -> (basename sp,o)) (discharge_object (oname,lobj)) + | _ -> + None + let close_section ~export id = let oname,fs = try match find_entry_p is_something_opened with @@ -421,25 +492,31 @@ let close_section ~export id = with Not_found -> error "no opened section" in - let (after,_,before) = split_lib oname in + let (secdecls,_,before) = split_lib oname in lib_stk := before; - let prefix = !path_prefix in + let full_olddir = fst !path_prefix in pop_path_prefix (); +(* let closed_sec = - ClosedSection (export, (fst prefix), export_segment after) - in + ClosedSection (export, full_olddir, export_segment secdecls) in let name = make_path id, make_kn id in add_entry name closed_sec; +*) if !Options.xml_export then !xml_close_section id; - (prefix, after, fs) + let newdecls = List.map discharge_item secdecls in + Summary.section_unfreeze_summaries fs; + List.iter (option_iter (fun (id,o) -> ignore (add_leaf id o))) newdecls; + Cooking.clear_cooking_sharing (); + Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir) +(*****************) (* Backtracking. *) let recache_decl = function | (sp, Leaf o) -> cache_object (sp,o) + | (_,OpenedSection _) -> add_section () | _ -> () - let recache_context ctx = List.iter recache_decl ctx @@ -475,7 +552,7 @@ let is_mod_node = function the same name *) let reset_mod (loc,id) = - let (ent,before) = + let (_,before) = try find_split_p (fun (sp,node) -> let (_,spi) = repr_path (fst sp) in id = spi @@ -583,3 +660,40 @@ let library_part ref = else (* Theorem/Lemma outside its outer section of definition *) dir + +(************************) +(* Discharging names *) + +let pop_kn kn = + let (mp,dir,l) = Names.repr_kn kn in + Names.make_kn mp (dirpath_prefix dir) l + +let pop_con con = + let (mp,dir,l) = Names.repr_con con in + Names.make_con mp (dirpath_prefix dir) l + +let con_defined_in_sec kn = + let _,dir,_ = repr_con kn in + dir <> empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ()) + +let defined_in_sec kn = + let _,dir,_ = repr_kn kn in + dir <> empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ()) + +let discharge_global = function + | ConstRef kn when con_defined_in_sec kn -> + ConstRef (pop_con kn) + | IndRef (kn,i) when defined_in_sec kn -> + IndRef (pop_kn kn,i) + | ConstructRef ((kn,i),j) when defined_in_sec kn -> + ConstructRef ((pop_kn kn,i),j) + | r -> r + +let discharge_kn kn = + if defined_in_sec kn then pop_kn kn else kn + +let discharge_con cst = + if con_defined_in_sec cst then pop_con cst else cst + +let discharge_inductive (kn,i) = + (discharge_kn kn,i) diff --git a/library/lib.mli b/library/lib.mli index 0433897ba..9a4a810ae 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -128,8 +128,7 @@ val library_part : global_reference -> dir_path val open_section : identifier -> object_prefix -val close_section : export:bool -> identifier -> - object_prefix * library_segment * Summary.frozen +val close_section : export:bool -> identifier -> unit (*s Backtracking (undo). *) @@ -157,3 +156,24 @@ val reset_initial : unit -> unit (* XML output hooks *) val set_xml_open_section : (identifier -> unit) -> unit val set_xml_close_section : (identifier -> unit) -> unit + + +(*s Section management for discharge *) + +val section_segment : global_reference -> Sign.named_context +val section_instance : global_reference -> Term.constr array + +val add_section_variable : identifier -> unit +val add_section_constant : constant -> Sign.named_context -> unit +val add_section_kn : kernel_name -> Sign.named_context -> unit +val replacement_context : unit -> + (identifier array Cmap.t * identifier array KNmap.t) + +(*s Discharge: decrease the section level if in the current section *) + +val discharge_kn : kernel_name -> kernel_name +val discharge_con : constant -> constant +val discharge_global : global_reference -> global_reference +val discharge_inductive : inductive -> inductive + + diff --git a/library/libobject.ml b/library/libobject.ml index 25d5a329f..d84e0bc26 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -36,6 +36,7 @@ type 'a object_declaration = { open_function : int -> object_name * 'a -> unit; classify_function : object_name * 'a -> 'a substitutivity; subst_function : object_name * substitution * 'a -> 'a; + discharge_function : object_name * 'a -> 'a option; export_function : 'a -> 'a option } let yell s = anomaly s @@ -48,6 +49,7 @@ let default_object s = { subst_function = (fun _ -> yell ("The object "^s^" does not know how to substitute!")); classify_function = (fun (_,obj) -> Keep obj); + discharge_function = (fun _ -> None); export_function = (fun _ -> None)} @@ -72,6 +74,7 @@ type dynamic_object_declaration = { dyn_open_function : int -> object_name * obj -> unit; dyn_subst_function : object_name * substitution * obj -> obj; dyn_classify_function : object_name * obj -> obj substitutivity; + dyn_discharge_function : object_name * obj -> obj option; dyn_export_function : obj -> obj option } let object_tag lobj = Dyn.tag lobj @@ -104,6 +107,11 @@ let declare_object odecl = | Anticipate (obj) -> Anticipate (infun obj) else anomaly "somehow we got the wrong dynamic object in the classifyfun" + and discharge (oname,lobj) = + if Dyn.tag lobj = na then + option_app infun (odecl.discharge_function (oname,outfun lobj)) + else + anomaly "somehow we got the wrong dynamic object in the dischargefun" and exporter lobj = if Dyn.tag lobj = na then option_app infun (odecl.export_function (outfun lobj)) @@ -116,6 +124,7 @@ let declare_object odecl = dyn_open_function = opener; dyn_subst_function = substituter; dyn_classify_function = classifier; + dyn_discharge_function = discharge; dyn_export_function = exporter }; (infun,outfun) @@ -154,5 +163,8 @@ let subst_object ((_,_,lobj) as node) = let classify_object ((_,lobj) as node) = apply_dyn_fun Dispose (fun d -> d.dyn_classify_function node) lobj +let discharge_object ((_,lobj) as node) = + apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj + let export_object lobj = apply_dyn_fun None (fun d -> d.dyn_export_function lobj) lobj diff --git a/library/libobject.mli b/library/libobject.mli index 37447ffbe..3d60e48ad 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -70,6 +70,7 @@ type 'a object_declaration = { open_function : int -> object_name * 'a -> unit; classify_function : object_name * 'a -> 'a substitutivity; subst_function : object_name * substitution * 'a -> 'a; + discharge_function : object_name * 'a -> 'a option; export_function : 'a -> 'a option } (* The default object is a "Keep" object with empty methods. @@ -103,4 +104,5 @@ val open_object : int -> object_name * obj -> unit val subst_object : object_name * substitution * obj -> obj val classify_object : object_name * obj -> obj substitutivity val export_object : obj -> obj option +val discharge_object : object_name * obj -> obj option val relax : bool -> unit diff --git a/library/library.ml b/library/library.ml index fee383233..09169c4ae 100644 --- a/library/library.ml +++ b/library/library.ml @@ -554,11 +554,14 @@ let load_require _ (_,(modl,_)) = OS dependent fields from .vo files for cross-platform compatibility *) let export_require (l,e) = Some (l,e) +let discharge_require (_,o) = Some o + let (in_require, out_require) = declare_object {(default_object "REQUIRE") with cache_function = cache_require; load_function = load_require; export_function = export_require; + discharge_function = discharge_require; classify_function = (fun (_,o) -> Anticipate o) } (* Require libraries, import them if [export <> None], mark them for export diff --git a/library/library.mli b/library/library.mli index 4ecc76809..bfcc04eb9 100644 --- a/library/library.mli +++ b/library/library.mli @@ -76,9 +76,3 @@ val locate_qualified_library : (*s Statistics: display the memory use of a library. *) val mem : dir_path -> Pp.std_ppcmds - -(*s For discharge *) -type library_reference - -val out_require : Libobject.obj -> library_reference -val reload_library : library_reference -> unit -- cgit v1.2.3