diff options
Diffstat (limited to 'kernel')
| -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 |
5 files changed, 380 insertions, 51 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 |