diff options
| -rw-r--r-- | kernel/kernel.mllib | 1 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 81 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 21 | ||||
| -rw-r--r-- | kernel/section.ml | 250 | ||||
| -rw-r--r-- | kernel/section.mli | 78 | ||||
| -rw-r--r-- | library/global.ml | 1 | ||||
| -rw-r--r-- | library/global.mli | 5 | ||||
| -rw-r--r-- | library/lib.ml | 147 | ||||
| -rw-r--r-- | library/lib.mli | 6 | ||||
| -rw-r--r-- | tactics/declare.ml | 7 |
10 files changed, 407 insertions, 190 deletions
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 66bac15e9a..20e742d7f8 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -49,4 +49,5 @@ Term_typing Subtyping Mod_typing Nativelibrary +Section Safe_typing diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 783ce63b8c..8d34f3a34f 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -113,16 +113,9 @@ type library_info = DirPath.t * vodigest (** Functor and funsig parameters, most recent first *) type module_parameters = (MBId.t * module_type_body) list -(** Sections can be nested with the proviso that no monomorphic section can be - opened inside a polymorphic one. The reverse is allowed. *) -type sections = { - sec_poly : int; - sec_mono : int; -} - type safe_environment = { env : Environ.env; - sections : sections; + sections : Section.t; modpath : ModPath.t; modvariant : modvariant; modresolver : Mod_subst.delta_resolver; @@ -150,11 +143,6 @@ let rec library_dp_of_senv senv = | SIG(_,senv) -> library_dp_of_senv senv | STRUCT(_,senv) -> library_dp_of_senv senv -let empty_sections = { - sec_poly = 0; - sec_mono = 0; -} - let empty_environment = { env = Environ.empty_env; modpath = ModPath.initial; @@ -164,7 +152,7 @@ let empty_environment = revstruct = []; modlabels = Label.Set.empty; objlabels = Label.Set.empty; - sections = empty_sections; + sections = Section.empty; future_cst = []; univ = Univ.ContextSet.empty; engagement = None; @@ -331,11 +319,16 @@ let universes_of_private eff = let env_of_safe_env senv = senv.env let env_of_senv = env_of_safe_env +let sections_of_safe_env senv = senv.sections + type constraints_addition = | Now of Univ.ContextSet.t | Later of Univ.ContextSet.t Future.computation let push_context_set poly cst senv = + let () = if Section.is_polymorphic senv.sections && not (Univ.ContextSet.is_empty cst) then + CErrors.user_err (Pp.str "Cannot add global universe constraints inside a polymorphic section.") + in { senv with env = Environ.push_context_set ~strict:(not poly) cst senv.env; univ = Univ.ContextSet.union cst senv.univ } @@ -399,11 +392,8 @@ let check_current_library dir senv = match senv.modvariant with (** When operating on modules, we're normally outside sections *) -let is_empty_sections s = - Int.equal s.sec_poly 0 && Int.equal s.sec_mono 0 - let check_empty_context senv = - assert (Environ.empty_context senv.env && is_empty_sections senv.sections) + assert (Environ.empty_context senv.env && Section.is_empty senv.sections) (** When adding a parameter to the current module/modtype, it must have been freshly started *) @@ -450,21 +440,30 @@ let safe_push_named d env = with Not_found -> () in Environ.push_named d env - let push_named_def (id,de) senv = - let () = assert (not @@ is_empty_sections senv.sections) in + let sections = Section.push_local senv.sections in let c, r, typ = Term_typing.translate_local_def senv.env id de in let x = Context.make_annot id r in let env'' = safe_push_named (LocalDef (x, c, typ)) senv.env in - { senv with env = env'' } + { senv with sections; env = env'' } let push_named_assum (x,t) senv = - let () = assert (not @@ is_empty_sections senv.sections) in + let sections = Section.push_local senv.sections in let t, r = Term_typing.translate_local_assum senv.env t in let x = Context.make_annot x r in let env'' = safe_push_named (LocalAssum (x,t)) senv.env in - {senv with env=env''} - + { senv with sections; env = env'' } + +let push_section_context (nas, ctx) senv = + let sections = Section.push_context (nas, ctx) senv.sections in + let senv = { senv with sections } in + let ctx = Univ.ContextSet.of_context ctx in + (* We check that the universes are fresh. FIXME: This should be done + implicitly, but we have to work around the API. *) + let () = assert (Univ.LSet.for_all (fun u -> not (Univ.LSet.mem u (fst senv.univ))) (fst ctx)) in + { senv with + env = Environ.push_context_set ~strict:false ctx senv.env; + univ = Univ.ContextSet.union ctx senv.univ } (** {6 Insertion of new declarations to current environment } *) @@ -546,8 +545,19 @@ let add_field ?(is_include=false) ((l,sfb) as field) gn senv = | SFBmodule mb, M -> Modops.add_module mb senv.env | _ -> assert false in + let sections = match sfb, gn with + | SFBconst cb, C con -> + let poly = Declareops.constant_is_polymorphic cb in + Section.push_constant ~poly con senv.sections + | SFBmind mib, I mind -> + let poly = Declareops.inductive_is_polymorphic mib in + Section.push_inductive ~poly mind senv.sections + | _, (M | MT) -> senv.sections + | _ -> assert false + in { senv with env = env'; + sections; revstruct = field :: senv.revstruct; modlabels = Label.Set.union mlabs senv.modlabels; objlabels = Label.Set.union olabs senv.objlabels } @@ -924,26 +934,13 @@ let add_module l me inl senv = (** {6 Interactive sections *) let open_section ~poly senv = - let sections = senv.sections in - if poly then - let sections = { sections with sec_poly = sections.sec_poly + 1 } in - { senv with sections } - else if Int.equal sections.sec_poly 0 then - let sections = { sections with sec_mono = sections.sec_mono + 1 } in - { senv with sections } - else - CErrors.anomaly (Pp.str "Cannot open a monomorphic section inside a polymorphic one") + let sections = Section.open_section ~poly senv.sections in + { senv with sections } let close_section senv = - let sections = senv.sections in - if not (Int.equal sections.sec_poly 0) then - let sections = { sections with sec_poly = sections.sec_poly - 1 } in - { senv with sections } - else if not (Int.equal sections.sec_mono 0) then - let sections = { sections with sec_mono = sections.sec_mono - 1 } in - { senv with sections } - else - CErrors.anomaly (Pp.str "No open section") + (* TODO: implement me when discharging in kernel *) + let sections = Section.close_section senv.sections in + { senv with sections } (** {6 Starting / ending interactive modules and module types } *) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 4eef43b193..10fedc2faf 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -33,6 +33,8 @@ val is_initial : safe_environment -> bool val env_of_safe_env : safe_environment -> Environ.env +val sections_of_safe_env : safe_environment -> Section.t + (** The safe_environment state monad *) type safe_transformer0 = safe_environment -> safe_environment @@ -67,15 +69,6 @@ val join_safe_environment : val is_joined_environment : safe_environment -> bool (** {6 Enriching a safe environment } *) -(** Insertion of local declarations (Local or Variables) *) - -val push_named_assum : (Id.t * Constr.types) -> safe_transformer0 - -(** Returns the full universe context necessary to typecheck the definition - (futures are forced) *) -val push_named_def : - Id.t * Entries.section_def_entry -> safe_transformer0 - (** Insertion of global axioms or definitions *) type 'a effect_entry = @@ -146,6 +139,16 @@ val open_section : poly:bool -> safe_transformer0 val close_section : safe_transformer0 +(** Insertion of local declarations (Local or Variables) *) + +val push_named_assum : (Id.t * Constr.types) -> safe_transformer0 + +val push_named_def : + Id.t * Entries.section_def_entry -> safe_transformer0 + +(** Add local universes to a polymorphic section *) +val push_section_context : (Name.t array * Univ.UContext.t) -> safe_transformer0 + (** {6 Interactive module functions } *) val start_module : Label.t -> ModPath.t safe_transformer diff --git a/kernel/section.ml b/kernel/section.ml new file mode 100644 index 0000000000..12e9c2fd60 --- /dev/null +++ b/kernel/section.ml @@ -0,0 +1,250 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Util +open Names +open Univ + +module NamedDecl = Context.Named.Declaration + +type _ section_kind = +| SecMono : [ `mono ] section_kind +| SecPoly : [ `poly ] section_kind + +type _ section_universes = +| SecMonoUniv : [ `mono ] section_universes +| SecPolyUniv : Name.t array * UContext.t -> [ `poly ] section_universes + +type section_entry = +| SecDefinition of Constant.t +| SecInductive of MutInd.t + +type 'a entry_map = 'a Cmap.t * 'a Mindmap.t + +type 'a section = { + sec_context : int; + (** Length of the named context suffix that has been introduced locally *) + sec_universes : 'a section_universes; + (** Universes local to the section *) + sec_entries : section_entry list; + (** Definitions introduced in the section *) + sec_data : 'a section_universes entry_map; +} + +(** Sections can be nested with the proviso that no monomorphic section can be + opened inside a polymorphic one. The reverse is allowed. *) +type t = { + sec_poly : [ `poly ] section list; + sec_mono : [ `mono ] section list; +} + +let empty = { + sec_poly = []; + sec_mono = []; +} + +let is_empty s = + List.is_empty s.sec_poly && List.is_empty s.sec_mono + +let is_polymorphic s = + not (List.is_empty s.sec_poly) + +let find_emap e (cmap, imap) = match e with +| SecDefinition con -> Cmap.find con cmap +| SecInductive ind -> Mindmap.find ind imap + +let add_emap e v (cmap, imap) = match e with +| SecDefinition con -> (Cmap.add con v cmap, imap) +| SecInductive ind -> (cmap, Mindmap.add ind v imap) + +type on_sec = { on_sec : 'a. 'a section_kind -> 'a section -> 'a section } + +let on_last_section f { sec_poly; sec_mono } = match sec_poly, sec_mono with +| [], [] -> CErrors.user_err (Pp.str "No opened section") +| sec :: rem, _ -> + let sec_poly = f.on_sec SecPoly sec :: rem in + { sec_mono; sec_poly } +| [], sec :: rem -> + let sec_mono = f.on_sec SecMono sec :: rem in + { sec_mono; sec_poly } + +type 'r with_sec = { with_sec : 'a. ('a section_kind * 'a section) option -> 'r } + +let with_last_section f { sec_poly; sec_mono } = match sec_poly, sec_mono with +| [], [] -> f.with_sec None +| sec :: _, _ -> f.with_sec (Some (SecPoly, sec)) +| [], sec :: _ -> f.with_sec (Some (SecMono, sec)) + +let push_local s = + let on_sec _ sec = { sec with sec_context = sec.sec_context + 1 } in + on_last_section { on_sec } s + +let push_context (nas, ctx) s = + let on_sec (type a) (kind : a section_kind) (sec : a section) : a section = match kind with + | SecMono -> + CErrors.anomaly (Pp.str "Adding polymorphic constraints to monomorphic section") + | SecPoly -> + let SecPolyUniv (snas, sctx) = sec.sec_universes in + let sec_universes = SecPolyUniv (Array.append snas nas, UContext.union sctx ctx) in + { sec with sec_universes } + in + on_last_section { on_sec } s + +let open_section ~poly sections = + if poly then + let sec = { + sec_context = 0; + sec_universes = SecPolyUniv ([||], Univ.UContext.empty); + sec_entries = []; + sec_data = (Cmap.empty, Mindmap.empty); + } in + { sections with sec_poly = sec :: sections.sec_poly } + else if List.is_empty sections.sec_poly then + let sec = { + sec_context = 0; + sec_universes = SecMonoUniv; + sec_entries = []; + sec_data = (Cmap.empty, Mindmap.empty); + } in + { sections with sec_mono = sec :: sections.sec_mono } + else + CErrors.user_err (Pp.str "Cannot open a monomorphic section inside a polymorphic one") + +let close_section sections = + (* TODO: implement me correctly when discharging in kernel *) + match sections.sec_poly, sections.sec_mono with + | _sec :: psecs, _ -> + let sections = { sections with sec_poly = psecs } in + sections + | [], _sec :: msecs -> + let sections = { sections with sec_mono = msecs } in + sections + | [], [] -> + CErrors.user_err (Pp.str "No opened section.") + +let same_poly (type a) ~poly (knd : a section_kind) = match knd with +| SecPoly -> poly +| SecMono -> not poly + +let push_global ~poly e s = + if is_empty s then s + else + let on_sec knd sec = + if same_poly ~poly knd then { sec with + sec_entries = e :: sec.sec_entries; + sec_data = add_emap e sec.sec_universes sec.sec_data; + } else + CErrors.user_err (Pp.str "Cannot mix universe polymorphic and \ + monomorphic declarations in sections.") + in + on_last_section { on_sec } s + +let push_constant ~poly con s = push_global ~poly (SecDefinition con) s + +let push_inductive ~poly ind s = push_global ~poly (SecInductive ind) s + +type abstr_info = { + abstr_ctx : Constr.named_context; + abstr_subst : Univ.Instance.t; + abstr_uctx : Univ.AUContext.t; +} + +let empty_segment = { + abstr_ctx = []; + abstr_subst = Instance.empty; + abstr_uctx = AUContext.empty; +} + +let extract_hyps sec vars hyps = + (* FIXME: this code is fishy. It is supposed to check that declared section + variables are an ordered subset of the ambient ones, but it doesn't check + e.g. uniqueness of naming nor convertibility of the section data. *) + let rec aux ids hyps = match ids, hyps with + | id :: ids, decl :: hyps when Names.Id.equal id (NamedDecl.get_id decl) -> + decl :: aux ids hyps + | _ :: ids, hyps -> + aux ids hyps + | [], _ -> [] + in + let ids = List.map NamedDecl.get_id @@ List.firstn sec.sec_context vars in + aux ids hyps + +let section_segment_of_entry vars e hyps sections = + (* [vars] are the named hypotheses, [hyps] the subset that is declared by the + global *) + let with_sec (type a) (s : (a section_kind * a section) option) = match s with + | None -> + CErrors.user_err (Pp.str "No opened section.") + | Some (knd, sec) -> + let hyps = extract_hyps sec vars hyps in + let inst, auctx = match knd, find_emap e sec.sec_data with + | SecMono, SecMonoUniv -> + Instance.empty, AUContext.empty + | SecPoly, SecPolyUniv (nas, ctx) -> + Univ.abstract_universes nas ctx + in + { + abstr_ctx = hyps; + abstr_subst = inst; + abstr_uctx = auctx; + } + in + with_last_section { with_sec } sections + +let segment_of_constant env con s = + let body = Environ.lookup_constant con env in + let vars = Environ.named_context env in + section_segment_of_entry vars (SecDefinition con) body.Declarations.const_hyps s + +let segment_of_inductive env mind s = + let mib = Environ.lookup_mind mind env in + let vars = Environ.named_context env in + section_segment_of_entry vars (SecInductive mind) mib.Declarations.mind_hyps s + +let instance_from_variable_context = + List.rev %> List.filter NamedDecl.is_local_assum %> List.map NamedDecl.get_id %> Array.of_list + +let extract_worklist info = + let args = instance_from_variable_context info.abstr_ctx in + info.abstr_subst, args + +let replacement_context env s = + let with_sec sec = match sec with + | None -> CErrors.user_err (Pp.str "No opened section.") + | Some (_, sec) -> + let cmap, imap = sec.sec_data in + let cmap = Cmap.mapi (fun con _ -> extract_worklist @@ segment_of_constant env con s) cmap in + let imap = Mindmap.mapi (fun ind _ -> extract_worklist @@ segment_of_inductive env ind s) imap in + (cmap, imap) + in + with_last_section { with_sec } s + +let is_in_section env gr s = + let with_sec sec = match sec with + | None -> false + | Some (_, sec) -> + let open GlobRef in + match gr with + | VarRef id -> + let vars = List.firstn sec.sec_context (Environ.named_context env) in + List.exists (fun decl -> Id.equal id (NamedDecl.get_id decl)) vars + | ConstRef con -> + Cmap.mem con (fst sec.sec_data) + | IndRef (ind, _) | ConstructRef ((ind, _), _) -> + Mindmap.mem ind (snd sec.sec_data) + in + with_last_section { with_sec } s + +let is_polymorphic_univ u s = + let check sec = + let SecPolyUniv (_, uctx) = sec.sec_universes in + Array.mem u (Instance.to_array (UContext.instance uctx)) + in + List.exists check s.sec_poly diff --git a/kernel/section.mli b/kernel/section.mli new file mode 100644 index 0000000000..4b23115ca2 --- /dev/null +++ b/kernel/section.mli @@ -0,0 +1,78 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names +open Univ + +(** Kernel implementation of sections. *) + +type t +(** Type of sections *) + +val empty : t + +val is_empty : t -> bool +(** Checks whether there is no opened section *) + +val is_polymorphic : t -> bool +(** Checks whether last opened section is polymorphic *) + +(** {6 Manipulating sections} *) + +val open_section : poly:bool -> t -> t +(** Open a new section with the provided universe polymorphic status. Sections + can be nested, with the proviso that polymorphic sections cannot appear + inside a monomorphic one. *) + +val close_section : t -> t + +(** {6 Extending sections} *) + +val push_local : t -> t +(** Extend the current section with a local definition (cf. push_named). *) + +val push_context : Name.t array * UContext.t -> t -> t +(** Extend the current section with a local universe context. Assumes that the + last opened section is polymorphic. *) + +val push_constant : poly:bool -> Constant.t -> t -> t +(** Make the constant as having been defined in this section. *) + +val push_inductive : poly:bool -> MutInd.t -> t -> t +(** Make the inductive block as having been defined in this section. *) + +(** {6 Retrieving section data} *) + +type abstr_info = private { + abstr_ctx : Constr.named_context; + (** Section variables of this prefix *) + abstr_subst : Univ.Instance.t; + (** Actual names of the abstracted variables *) + abstr_uctx : Univ.AUContext.t; + (** Universe quantification, same length as the substitution *) +} +(** Data needed to abstract over the section variable and universe hypotheses *) + + +val empty_segment : abstr_info +(** Nothing to abstract *) + +val segment_of_constant : Environ.env -> Constant.t -> t -> abstr_info +(** Section segment at the time of the constant declaration *) + +val segment_of_inductive : Environ.env -> MutInd.t -> t -> abstr_info +(** Section segment at the time of the inductive declaration *) + +val replacement_context : Environ.env -> t -> Opaqueproof.work_list +(** Section segments of all declarations from this section. *) + +val is_in_section : Environ.env -> GlobRef.t -> t -> bool + +val is_polymorphic_univ : Level.t -> t -> bool diff --git a/library/global.ml b/library/global.ml index e51c147f6e..3d28178d7b 100644 --- a/library/global.ml +++ b/library/global.ml @@ -83,6 +83,7 @@ let i2l = Label.of_id let push_named_assum a = globalize0 (Safe_typing.push_named_assum a) let push_named_def d = globalize0 (Safe_typing.push_named_def d) +let push_section_context c = globalize0 (Safe_typing.push_section_context c) let add_constraints c = globalize0 (Safe_typing.add_constraints c) let push_context_set b c = globalize0 (Safe_typing.push_context_set b c) diff --git a/library/global.mli b/library/global.mli index 9ac6b1f53c..b809e9b241 100644 --- a/library/global.mli +++ b/library/global.mli @@ -44,6 +44,7 @@ val sprop_allowed : unit -> bool val push_named_assum : (Id.t * Constr.types) -> unit val push_named_def : (Id.t * Entries.section_def_entry) -> unit +val push_section_context : (Name.t array * Univ.UContext.t) -> unit val export_private_constants : in_section:bool -> Safe_typing.private_constants Entries.proof_output -> @@ -74,7 +75,11 @@ val add_include : (** Sections *) val open_section : poly:bool -> unit +(** [poly] is true when the section should be universe polymorphic *) + val close_section : Summary.frozen -> unit +(** Close the section and reset the global state to the one at the time when + the section what opened. *) (** Interactive modules and module types *) diff --git a/library/lib.ml b/library/lib.ml index 367a84409b..1c6f82e8a6 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -410,87 +410,11 @@ let find_opening_node id = - the list of substitution to do at section closing *) -type abstr_info = { +type abstr_info = Section.abstr_info = private { abstr_ctx : Constr.named_context; abstr_subst : Univ.Instance.t; abstr_uctx : Univ.AUContext.t; } -type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t - -type secentry = - | Variable of { - id:Names.Id.t; - } - | Context of Name.t array * Univ.UContext.t - -type section_data = { - sec_entry : secentry list; - sec_abstr : abstr_list; - sec_poly : bool; -} - -let empty_section_data ~poly = { - sec_entry = []; - sec_abstr = (Names.Cmap.empty,Names.Mindmap.empty); - sec_poly = poly; -} - -let sectab = - Summary.ref ([] : section_data list) ~name:"section-context" - -let check_same_poly p sec = - if p != sec.sec_poly then - user_err Pp.(str "Cannot mix universe polymorphic and monomorphic declarations in sections.") - -let add_section ~poly () = - List.iter (fun tab -> check_same_poly poly tab) !sectab; - sectab := empty_section_data ~poly :: !sectab - -let add_section_variable ~name ~poly = - match !sectab with - | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) - | s :: sl -> - List.iter (fun tab -> check_same_poly poly tab) !sectab; - let s = { s with sec_entry = Variable {id=name} :: s.sec_entry } in - sectab := s :: sl - -let add_section_context (nas, ctx) = - match !sectab with - | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) - | s :: sl -> - check_same_poly true s; - let s = { s with sec_entry = Context (nas, ctx) :: s.sec_entry } in - sectab := s :: sl - -exception PolyFound (* make this a let exception once possible *) -let is_polymorphic_univ u = - try - let open Univ in - List.iter (fun s -> - let vars = s.sec_entry in - List.iter (function - | Variable _ -> () - | Context (_, univs) -> - if Array.mem u (Instance.to_array (UContext.instance univs)) then raise PolyFound - ) vars - ) !sectab; - false - with PolyFound -> true - -let extract_hyps poly (secs,ohyps) = - let rec aux = function - | (Variable {id}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) -> - let l, r = aux (idl,hyps) in - decl :: l, r - | (Variable _::idl,hyps) -> - let l, r = aux (idl,hyps) in - l, r - | (Context (nas, ctx) :: idl, hyps) -> - let () = assert poly in - let l, (snas, sctx) = aux (idl, hyps) in - l, (Array.append snas nas, Univ.UContext.union sctx ctx) - | [], _ -> [], ([||], Univ.UContext.empty) - in aux (secs,ohyps) let instance_from_variable_context = List.rev %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list @@ -499,47 +423,21 @@ let extract_worklist info = let args = instance_from_variable_context info.abstr_ctx in info.abstr_subst, args -let make_worklist (cmap, mmap) = - Cmap.map extract_worklist cmap, Mindmap.map extract_worklist mmap - -let add_section_replacement g poly hyps = - match !sectab with - | [] -> () - | s :: sl -> - let () = check_same_poly poly s in - let sechyps, (nas, ctx) = extract_hyps s.sec_poly (s.sec_entry, hyps) in - let subst, ctx = Univ.abstract_universes nas ctx in - let info = { - abstr_ctx = sechyps; - abstr_subst = subst; - abstr_uctx = ctx; - } in - let s = { s with - sec_abstr = g info s.sec_abstr; - } in - sectab := s :: sl - -let add_section_kn ~poly kn = - let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in - add_section_replacement f poly - -let add_section_constant ~poly kn = - let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in - add_section_replacement f poly - -let replacement_context () = make_worklist (List.hd !sectab).sec_abstr +let sections () = Safe_typing.sections_of_safe_env @@ Global.safe_env () + +let is_polymorphic_univ u = + Section.is_polymorphic_univ u (sections ()) + +let replacement_context () = + Section.replacement_context (Global.env ()) (sections ()) let section_segment_of_constant con = - Names.Cmap.find con (fst (List.hd !sectab).sec_abstr) + Section.segment_of_constant (Global.env ()) con (sections ()) let section_segment_of_mutual_inductive kn = - Names.Mindmap.find kn (snd (List.hd !sectab).sec_abstr) + Section.segment_of_inductive (Global.env ()) kn (sections ()) -let empty_segment = { - abstr_ctx = []; - abstr_subst = Univ.Instance.empty; - abstr_uctx = Univ.AUContext.empty; -} +let empty_segment = Section.empty_segment let section_segment_of_reference = let open GlobRef in function | ConstRef c -> section_segment_of_constant c @@ -550,25 +448,20 @@ let section_segment_of_reference = let open GlobRef in function let variable_section_segment_of_reference gr = (section_segment_of_reference gr).abstr_ctx +let is_in_section ref = + Section.is_in_section (Global.env ()) ref (sections ()) + let section_instance = let open GlobRef in function | VarRef id -> - let eq = function - | Variable {id=id'} -> Names.Id.equal id id' - | Context _ -> false - in - if List.exists eq (List.hd !sectab).sec_entry - then Univ.Instance.empty, [||] - else raise Not_found + if is_in_section (VarRef id) then (Univ.Instance.empty, [||]) + else raise Not_found | ConstRef con -> - let data = Names.Cmap.find con (fst (List.hd !sectab).sec_abstr) in + let data = section_segment_of_constant con in extract_worklist data | IndRef (kn,_) | ConstructRef ((kn,_),_) -> - let data = Names.Mindmap.find kn (snd (List.hd !sectab).sec_abstr) in + let data = section_segment_of_mutual_inductive kn in extract_worklist data -let is_in_section ref = - try ignore (section_instance ref); true with Not_found -> false - (*************) (* Sections. *) let open_section ~poly id = @@ -582,9 +475,7 @@ let open_section ~poly id = add_entry (make_foname id) (OpenedSection (prefix, fs)); (*Pushed for the lifetime of the section: removed by unfrozing the summary*) Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirOpenSection prefix)); - lib_state := { !lib_state with path_prefix = prefix }; - add_section ~poly () - + lib_state := { !lib_state with path_prefix = prefix } (* Restore lib_stk and summaries as before the section opening, and add a ClosedSection object. *) diff --git a/library/lib.mli b/library/lib.mli index db6df4395b..5ce601f2d3 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -163,7 +163,7 @@ val drop_objects : frozen -> frozen val init : unit -> unit (** {6 Section management for discharge } *) -type abstr_info = private { +type abstr_info = Section.abstr_info = private { abstr_ctx : Constr.named_context; (** Section variables of this prefix *) abstr_subst : Univ.Instance.t; @@ -181,10 +181,6 @@ val variable_section_segment_of_reference : GlobRef.t -> Constr.named_context val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array val is_in_section : GlobRef.t -> bool -val add_section_variable : name:Id.t -> poly:bool -> unit -val add_section_context : Name.t array * Univ.UContext.t -> unit -val add_section_constant : poly:bool -> Constant.t -> Constr.named_context -> unit -val add_section_kn : poly:bool -> MutInd.t -> Constr.named_context -> unit val replacement_context : unit -> Opaqueproof.work_list val is_polymorphic_univ : Univ.Level.t -> bool diff --git a/tactics/declare.ml b/tactics/declare.ml index 2f9da373aa..208b8e28a7 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -63,7 +63,7 @@ let declare_universe_context ~poly ctx = let univs = Univ.LSet.filter (fun u -> not (Lib.is_polymorphic_univ u)) univs in let uctx = Univ.ContextSet.to_context (univs, cstr) in let nas = name_instance (Univ.UContext.instance uctx) in - (Global.push_context_set true ctx; Lib.add_section_context (nas, uctx)) + Global.push_section_context (nas, uctx) else Lib.add_anonymous_leaf (input_universe_context ctx) @@ -139,8 +139,6 @@ let cache_constant ((sp,kn), obj) = in assert (Constant.equal kn' (Constant.make1 kn)); Nametab.push (Nametab.Until 1) sp (GlobRef.ConstRef (Constant.make1 kn)); - let cst = Global.lookup_constant kn' in - add_section_constant ~poly:(Declareops.constant_is_polymorphic cst) kn' cst.const_hyps; Dumpglob.add_constant_kind (Constant.make1 kn) obj.cst_kind let discharge_constant ((sp, kn), obj) = @@ -373,7 +371,6 @@ let declare_variable ~name ~kind d = poly in Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name); - add_section_variable ~name ~poly; Decls.(add_variable_data name {opaque;kind}); add_anonymous_leaf (inVariable ()); Impargs.declare_var_implicits ~impl name; @@ -422,8 +419,6 @@ let cache_inductive ((sp,kn),mie) = let id = Libnames.basename sp in let kn' = Global.add_mind id mie in assert (MutInd.equal kn' (MutInd.make1 kn)); - let mind = Global.lookup_mind kn' in - add_section_kn ~poly:(Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps; List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names let discharge_inductive ((sp,kn),mie) = |