diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/inferCumulativity.ml | 233 | ||||
| -rw-r--r-- | kernel/inferCumulativity.mli | 14 | ||||
| -rw-r--r-- | kernel/kernel.mllib | 2 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 49 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 27 | ||||
| -rw-r--r-- | kernel/section.ml | 250 | ||||
| -rw-r--r-- | kernel/section.mli | 78 |
7 files changed, 639 insertions, 14 deletions
diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml new file mode 100644 index 0000000000..3b8c2cd788 --- /dev/null +++ b/kernel/inferCumulativity.ml @@ -0,0 +1,233 @@ +(************************************************************************) +(* * 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 Reduction +open Declarations +open Constr +open Univ +open Variance +open Util + +type inferred = IrrelevantI | CovariantI + +(** Throughout this module we modify a map [variances] from local + universes to [inferred]. It starts as a trivial mapping to + [Irrelevant] and every time we encounter a local universe we + restrict it accordingly. + [Invariant] universes are removed from the map. +*) +exception TrivialVariance + +let maybe_trivial variances = + if LMap.is_empty variances then raise TrivialVariance + else variances + +let infer_level_eq u variances = + maybe_trivial (LMap.remove u variances) + +let infer_level_leq u variances = + (* can only set Irrelevant -> Covariant so nontrivial *) + LMap.update u (function + | None -> None + | Some CovariantI as x -> x + | Some IrrelevantI -> Some CovariantI) + variances + +let infer_generic_instance_eq variances u = + Array.fold_left (fun variances u -> infer_level_eq u variances) + variances (Instance.to_array u) + +let infer_cumulative_ind_instance cv_pb mind_variance variances u = + Array.fold_left2 (fun variances varu u -> + match cv_pb, varu with + | _, Irrelevant -> variances + | _, Invariant | CONV, Covariant -> infer_level_eq u variances + | CUMUL, Covariant -> infer_level_leq u variances) + variances mind_variance (Instance.to_array u) + +let infer_inductive_instance cv_pb env variances ind nargs u = + let mind = Environ.lookup_mind (fst ind) env in + match mind.mind_variance with + | None -> infer_generic_instance_eq variances u + | Some mind_variance -> + if not (Int.equal (inductive_cumulativity_arguments (mind,snd ind)) nargs) + then infer_generic_instance_eq variances u + else infer_cumulative_ind_instance cv_pb mind_variance variances u + +let infer_constructor_instance_eq env variances ((mi,ind),ctor) nargs u = + let mind = Environ.lookup_mind mi env in + match mind.mind_variance with + | None -> infer_generic_instance_eq variances u + | Some _ -> + if not (Int.equal (constructor_cumulativity_arguments (mind,ind,ctor)) nargs) + then infer_generic_instance_eq variances u + else variances (* constructors are convertible at common supertype *) + +let infer_sort cv_pb variances s = + match cv_pb with + | CONV -> + LSet.fold infer_level_eq (Universe.levels (Sorts.univ_of_sort s)) variances + | CUMUL -> + LSet.fold infer_level_leq (Universe.levels (Sorts.univ_of_sort s)) variances + +let infer_table_key variances c = + let open Names in + match c with + | ConstKey (_, u) -> + infer_generic_instance_eq variances u + | VarKey _ | RelKey _ -> variances + +let whd_stack (infos, tab) hd stk = CClosure.whd_stack infos tab hd stk + +let rec infer_fterm cv_pb infos variances hd stk = + Control.check_for_interrupt (); + let hd,stk = whd_stack infos hd stk in + let open CClosure in + match fterm_of hd with + | FAtom a -> + begin match kind a with + | Sort s -> infer_sort cv_pb variances s + | Meta _ -> infer_stack infos variances stk + | _ -> assert false + end + | FEvar ((_,args),e) -> + let variances = infer_stack infos variances stk in + infer_vect infos variances (Array.map (mk_clos e) args) + | FRel _ -> infer_stack infos variances stk + | FInt _ -> infer_stack infos variances stk + | FFlex fl -> + let variances = infer_table_key variances fl in + infer_stack infos variances stk + | FProj (_,c) -> + let variances = infer_fterm CONV infos variances c [] in + infer_stack infos variances stk + | FLambda _ -> + let (_,ty,bd) = destFLambda mk_clos hd in + let variances = infer_fterm CONV infos variances ty [] in + infer_fterm CONV infos variances bd [] + | FProd (_,dom,codom,e) -> + let variances = infer_fterm CONV infos variances dom [] in + infer_fterm cv_pb infos variances (mk_clos (Esubst.subs_lift e) codom) [] + | FInd (ind, u) -> + let variances = + if Instance.is_empty u then variances + else + let nargs = stack_args_size stk in + infer_inductive_instance cv_pb (info_env (fst infos)) variances ind nargs u + in + infer_stack infos variances stk + | FConstruct (ctor,u) -> + let variances = + if Instance.is_empty u then variances + else + let nargs = stack_args_size stk in + infer_constructor_instance_eq (info_env (fst infos)) variances ctor nargs u + in + infer_stack infos variances stk + | FFix ((_,(_,tys,cl)),e) | FCoFix ((_,(_,tys,cl)),e) -> + let n = Array.length cl in + let variances = infer_vect infos variances (Array.map (mk_clos e) tys) in + let le = Esubst.subs_liftn n e in + let variances = infer_vect infos variances (Array.map (mk_clos le) cl) in + infer_stack infos variances stk + + (* Removed by whnf *) + | FLOCKED | FCaseT _ | FLetIn _ | FApp _ | FLIFT _ | FCLOS _ -> assert false + +and infer_stack infos variances (stk:CClosure.stack) = + match stk with + | [] -> variances + | z :: stk -> + let open CClosure in + let variances = match z with + | Zapp v -> infer_vect infos variances v + | Zproj _ -> variances + | Zfix (fx,a) -> + let variances = infer_fterm CONV infos variances fx [] in + infer_stack infos variances a + | ZcaseT (_, p, br, e) -> + let variances = infer_fterm CONV infos variances (mk_clos e p) [] in + infer_vect infos variances (Array.map (mk_clos e) br) + | Zshift _ -> variances + | Zupdate _ -> variances + | Zprimitive (_,_,rargs,kargs) -> + let variances = List.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances rargs in + let variances = List.fold_left (fun variances (_,c) -> infer_fterm CONV infos variances c []) variances kargs in + variances + in + infer_stack infos variances stk + +and infer_vect infos variances v = + Array.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances v + +let infer_term cv_pb env variances c = + let open CClosure in + let infos = (create_clos_infos all env, create_tab ()) in + infer_fterm cv_pb infos variances (CClosure.inject c) [] + +let infer_arity_constructor is_arity env variances arcn = + let infer_typ typ (env,variances) = + match typ with + | Context.Rel.Declaration.LocalAssum (_, typ') -> + (Environ.push_rel typ env, infer_term CUMUL env variances typ') + | Context.Rel.Declaration.LocalDef _ -> assert false + in + let typs, codom = Reduction.dest_prod env arcn in + let env, variances = Context.Rel.fold_outside infer_typ typs ~init:(env, variances) in + (* If we have Inductive foo@{i j} : ... -> Type@{i} := C : ... -> foo Type@{j} + i is irrelevant, j is invariant. *) + if not is_arity then infer_term CUMUL env variances codom else variances + +open Entries + +let infer_inductive_core env params entries uctx = + let uarray = Instance.to_array @@ UContext.instance uctx in + if Array.is_empty uarray then raise TrivialVariance; + let env = Environ.push_context uctx env in + let variances = + Array.fold_left (fun variances u -> LMap.add u IrrelevantI variances) + LMap.empty uarray + in + let env, _ = Typeops.check_context env params in + let variances = List.fold_left (fun variances entry -> + let variances = infer_arity_constructor true + env variances entry.mind_entry_arity + in + List.fold_left (infer_arity_constructor false env) + variances entry.mind_entry_lc) + variances + entries + in + Array.map (fun u -> match LMap.find u variances with + | exception Not_found -> Invariant + | IrrelevantI -> Irrelevant + | CovariantI -> Covariant) + uarray + +let infer_inductive env mie = + let open Entries in + let params = mie.mind_entry_params in + let entries = mie.mind_entry_inds in + let variances = + match mie.mind_entry_variance with + | None -> None + | Some _ -> + let uctx = match mie.mind_entry_universes with + | Monomorphic_entry _ -> assert false + | Polymorphic_entry (_,uctx) -> uctx + in + try Some (infer_inductive_core env params entries uctx) + with TrivialVariance -> Some (Array.make (UContext.size uctx) Invariant) + in + { mie with mind_entry_variance = variances } + +let dummy_variance = let open Entries in function + | Monomorphic_entry _ -> assert false + | Polymorphic_entry (_,uctx) -> Array.make (UContext.size uctx) Irrelevant diff --git a/kernel/inferCumulativity.mli b/kernel/inferCumulativity.mli new file mode 100644 index 0000000000..a234e334d1 --- /dev/null +++ b/kernel/inferCumulativity.mli @@ -0,0 +1,14 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + +val infer_inductive : Environ.env -> Entries.mutual_inductive_entry -> + Entries.mutual_inductive_entry + +val dummy_variance : Entries.universes_entry -> Univ.Variance.t array diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 59c1d5890f..20e742d7f8 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -43,9 +43,11 @@ Inductive Typeops IndTyping Indtypes +InferCumulativity Cooking Term_typing Subtyping Mod_typing Nativelibrary +Section Safe_typing diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 6970a11e72..8d34f3a34f 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -115,6 +115,7 @@ type module_parameters = (MBId.t * module_type_body) list type safe_environment = { env : Environ.env; + sections : Section.t; modpath : ModPath.t; modvariant : modvariant; modresolver : Mod_subst.delta_resolver; @@ -151,6 +152,7 @@ let empty_environment = revstruct = []; modlabels = Label.Set.empty; objlabels = Label.Set.empty; + sections = Section.empty; future_cst = []; univ = Univ.ContextSet.empty; engagement = None; @@ -317,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 } @@ -386,7 +393,7 @@ let check_current_library dir senv = match senv.modvariant with (** When operating on modules, we're normally outside sections *) let check_empty_context senv = - assert (Environ.empty_context senv.env) + 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 *) @@ -433,19 +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 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 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 } *) @@ -527,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 } @@ -902,6 +931,16 @@ let add_module l me inl senv = in (mp,mb.mod_delta),senv'' +(** {6 Interactive sections *) + +let open_section ~poly senv = + let sections = Section.open_section ~poly senv.sections in + { senv with sections } + +let close_section senv = + (* 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 fa53fa33fa..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 = @@ -140,6 +133,22 @@ val set_allow_sprop : bool -> safe_transformer0 val check_engagement : Environ.env -> Declarations.set_predicativity -> unit +(** {6 Interactive section functions } *) + +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 |