From 4838fd47542018ba61cd096c93edf45b7ef68529 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 8 Aug 2019 13:48:57 +0200 Subject: Refine the API to declare section-local universes. The section local universes are undoubtedly ordered, but the API was requiring an unordered ContextSet. We also move the naming one level up. Unfortunately, some callers are currently defining the same polymorphic universes in a section several times, notably the "Variable" command. I had to hack around this behaviour. --- library/lib.ml | 39 ++++++++++----------------------------- library/lib.mli | 2 +- tactics/declare.ml | 27 ++++++++++++++++++++++++--- 3 files changed, 35 insertions(+), 33 deletions(-) diff --git a/library/lib.ml b/library/lib.ml index 851f086961..1f97424590 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -421,7 +421,7 @@ type secentry = | Variable of { id:Names.Id.t; } - | Context of Univ.ContextSet.t + | Context of Name.t array * Univ.UContext.t type section_data = { sec_entry : secentry list; @@ -454,12 +454,12 @@ let add_section_variable ~name ~poly = let s = { s with sec_entry = Variable {id=name} :: s.sec_entry } in sectab := s :: sl -let add_section_context ctx = +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 ctx :: s.sec_entry } in + 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 *) @@ -470,8 +470,8 @@ let is_polymorphic_univ u = let vars = s.sec_entry in List.iter (function | Variable _ -> () - | Context (univs,_) -> - if LSet.mem u univs then raise PolyFound + | Context (_, univs) -> + if Array.mem u (Instance.to_array (UContext.instance univs)) then raise PolyFound ) vars ) !sectab; false @@ -485,11 +485,11 @@ let extract_hyps poly (secs,ohyps) = | (Variable _::idl,hyps) -> let l, r = aux (idl,hyps) in l, r - | (Context ctx :: idl, hyps) -> + | (Context (nas, ctx) :: idl, hyps) -> let () = assert poly in - let l, r = aux (idl, hyps) in - l, Univ.ContextSet.union r ctx - | [], _ -> [],Univ.ContextSet.empty + 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 = @@ -502,31 +502,12 @@ let extract_worklist info = let make_worklist (cmap, mmap) = Cmap.map extract_worklist cmap, Mindmap.map extract_worklist mmap -let name_instance inst = - (* FIXME: this should probably be done at an upper level, by storing the - name information in the section data structure. *) - let map lvl = match Univ.Level.name lvl with - | None -> (* Having Prop/Set/Var as section universes makes no sense *) - assert false - | Some na -> - try - let qid = Nametab.shortest_qualid_of_universe na in - Name (Libnames.qualid_basename qid) - with Not_found -> - (* Best-effort naming from the string representation of the level. - See univNames.ml for a similar hack. *) - Name (Id.of_string_soft (Univ.Level.to_string lvl)) - in - Array.map map (Univ.Instance.to_array inst) - let add_section_replacement g poly hyps = match !sectab with | [] -> () | s :: sl -> let () = check_same_poly poly s in - let sechyps,ctx = extract_hyps s.sec_poly (s.sec_entry, hyps) in - let ctx = Univ.ContextSet.to_context ctx in - let nas = name_instance (Univ.UContext.instance ctx) 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; diff --git a/library/lib.mli b/library/lib.mli index 9ffa69ef93..db6df4395b 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -182,7 +182,7 @@ 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 : Univ.ContextSet.t -> 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 diff --git a/tactics/declare.ml b/tactics/declare.ml index 3a02e5451a..2f9da373aa 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -40,9 +40,30 @@ let input_universe_context : Univ.ContextSet.t -> Libobject.obj = ~cache:(fun (na, uctx) -> Global.push_context_set false uctx) ~discharge:(fun (_, x) -> Some x) +let name_instance inst = + let map lvl = match Univ.Level.name lvl with + | None -> (* Having Prop/Set/Var as section universes makes no sense *) + assert false + | Some na -> + try + let qid = Nametab.shortest_qualid_of_universe na in + Name (Libnames.qualid_basename qid) + with Not_found -> + (* Best-effort naming from the string representation of the level. + See univNames.ml for a similar hack. *) + Name (Id.of_string_soft (Univ.Level.to_string lvl)) + in + Array.map map (Univ.Instance.to_array inst) + let declare_universe_context ~poly ctx = if poly then - (Global.push_context_set true ctx; Lib.add_section_context ctx) + (* FIXME: some upper layers declare universes several times, we hack around + by checking whether the universes already exist. *) + let (univs, cstr) = ctx in + 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)) else Lib.add_anonymous_leaf (input_universe_context ctx) @@ -632,9 +653,9 @@ let do_universe ~poly l = let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx) Univ.LSet.empty l, Univ.Constraint.empty in - let () = declare_universe_context ~poly ctx in let src = if poly then BoundUniv else UnqualifiedUniv in - Lib.add_anonymous_leaf (input_univ_names (src, l)) + let () = Lib.add_anonymous_leaf (input_univ_names (src, l)) in + declare_universe_context ~poly ctx let do_constraint ~poly l = let open Univ in -- cgit v1.2.3 From 24eccfc6dfec012da081a0891c397f013cc590e5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 17 May 2019 15:58:05 +0200 Subject: Stub code for handling sections in kernel. For now we only keep a count of the number of open sections, discriminating between polymorphic and monomorphic ones. --- kernel/safe_typing.ml | 44 +++++++++++++++++++++++++++++++++++++++++++- kernel/safe_typing.mli | 6 ++++++ library/global.ml | 7 +++++++ library/global.mli | 5 +++++ library/lib.ml | 3 ++- 5 files changed, 63 insertions(+), 2 deletions(-) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 6970a11e72..783ce63b8c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -113,8 +113,16 @@ 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; modpath : ModPath.t; modvariant : modvariant; modresolver : Mod_subst.delta_resolver; @@ -142,6 +150,11 @@ 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; @@ -151,6 +164,7 @@ let empty_environment = revstruct = []; modlabels = Label.Set.empty; objlabels = Label.Set.empty; + sections = empty_sections; future_cst = []; univ = Univ.ContextSet.empty; engagement = None; @@ -385,8 +399,11 @@ 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) + assert (Environ.empty_context senv.env && is_empty_sections senv.sections) (** When adding a parameter to the current module/modtype, it must have been freshly started *) @@ -435,12 +452,14 @@ let safe_push_named d env = let push_named_def (id,de) senv = + let () = assert (not @@ is_empty_sections 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'' } let push_named_assum (x,t) senv = + let () = assert (not @@ is_empty_sections 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 @@ -902,6 +921,29 @@ let add_module l me inl senv = in (mp,mb.mod_delta),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 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") (** {6 Starting / ending interactive modules and module types } *) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index fa53fa33fa..4eef43b193 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -140,6 +140,12 @@ 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 + (** {6 Interactive module functions } *) val start_module : Label.t -> ModPath.t safe_transformer diff --git a/library/global.ml b/library/global.ml index 6bb4614aa4..e51c147f6e 100644 --- a/library/global.ml +++ b/library/global.ml @@ -104,6 +104,13 @@ let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl) let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl) +let open_section ~poly = globalize0 (Safe_typing.open_section ~poly) +let close_section fs = + (* TODO: use globalize0_with_summary *) + Summary.unfreeze_summaries fs; + let env = Safe_typing.close_section (safe_env ()) in + GlobalSafeEnv.set_safe_env env + let start_module id = globalize (Safe_typing.start_module (i2l id)) let start_modtype id = globalize (Safe_typing.start_modtype (i2l id)) diff --git a/library/global.mli b/library/global.mli index d0bd556d70..9ac6b1f53c 100644 --- a/library/global.mli +++ b/library/global.mli @@ -71,6 +71,11 @@ val add_include : Entries.module_struct_entry -> bool -> Declarations.inline -> Mod_subst.delta_resolver +(** Sections *) + +val open_section : poly:bool -> unit +val close_section : Summary.frozen -> unit + (** Interactive modules and module types *) val start_module : Id.t -> ModPath.t diff --git a/library/lib.ml b/library/lib.ml index 1f97424590..367a84409b 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -572,6 +572,7 @@ let is_in_section ref = (*************) (* Sections. *) let open_section ~poly id = + let () = Global.open_section ~poly in let opp = !lib_state.path_prefix in let obj_dir = add_dirpath_suffix opp.Nametab.obj_dir id in let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in @@ -612,7 +613,7 @@ let close_section () = lib_state := { !lib_state with lib_stk = before }; pop_path_prefix (); let newdecls = List.map discharge_item secdecls in - Summary.unfreeze_summaries fs; + let () = Global.close_section fs in List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls (* State and initialization. *) -- cgit v1.2.3 From 6176c2879dd989029a83642caec7cd66a2a4f527 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Jul 2019 10:34:47 +0200 Subject: Move cumulativity inference to the kernel. This is not quite pretty, but it is needed by the section mechanism to rebuild an inductive when closing a section. Hopefully this can be moved back at some point. --- kernel/inferCumulativity.ml | 233 +++++++++++++++++++++++++++++++++++++++ kernel/inferCumulativity.mli | 14 +++ kernel/kernel.mllib | 1 + pretyping/inferCumulativity.ml | 234 ---------------------------------------- pretyping/inferCumulativity.mli | 14 --- pretyping/pretyping.mllib | 1 - 6 files changed, 248 insertions(+), 249 deletions(-) create mode 100644 kernel/inferCumulativity.ml create mode 100644 kernel/inferCumulativity.mli delete mode 100644 pretyping/inferCumulativity.ml delete mode 100644 pretyping/inferCumulativity.mli diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml new file mode 100644 index 0000000000..8b5b254f45 --- /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 *) +(* 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 _infos 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 infos 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 *) +(* 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..66bac15e9a 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -43,6 +43,7 @@ Inductive Typeops IndTyping Indtypes +InferCumulativity Cooking Term_typing Subtyping diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml deleted file mode 100644 index ed069eace0..0000000000 --- a/pretyping/inferCumulativity.ml +++ /dev/null @@ -1,234 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* 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 infos 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 infos 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 (ci,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, params = 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 { mind_entry_params = params; - mind_entry_inds = entries; } = mie - 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/pretyping/inferCumulativity.mli b/pretyping/inferCumulativity.mli deleted file mode 100644 index a234e334d1..0000000000 --- a/pretyping/inferCumulativity.mli +++ /dev/null @@ -1,14 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* Entries.mutual_inductive_entry -> - Entries.mutual_inductive_entry - -val dummy_variance : Entries.universes_entry -> Univ.Variance.t array diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 0ca39f0404..7e140f4399 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -4,7 +4,6 @@ Locusops Pretype_errors Reductionops Inductiveops -InferCumulativity Arguments_renaming Retyping Vnorm -- cgit v1.2.3 From 58a9de2acacb05291d87fe2b656728ae05d59df4 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Jul 2019 10:48:28 +0200 Subject: Move the Lib section data into the kernel. Due to the redundancy with some other declaration-specific data from the kernel, we also seize the opportunity to clean it up. Note also that discharging is still performed outside of the kernel for now. --- kernel/kernel.mllib | 1 + kernel/safe_typing.ml | 81 ++++++++-------- kernel/safe_typing.mli | 21 +++-- kernel/section.ml | 250 +++++++++++++++++++++++++++++++++++++++++++++++++ kernel/section.mli | 78 +++++++++++++++ library/global.ml | 1 + library/global.mli | 5 + library/lib.ml | 147 ++++------------------------- library/lib.mli | 6 +- tactics/declare.ml | 7 +- 10 files changed, 407 insertions(+), 190 deletions(-) create mode 100644 kernel/section.ml create mode 100644 kernel/section.mli 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 *) +(* [ `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 *) +(* 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) = -- cgit v1.2.3 From df563b34440f6ea14356843b7b1c402a99266910 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 17 Aug 2019 19:38:47 +0200 Subject: Clean up InferCumulativity after its move to the kernel. --- kernel/inferCumulativity.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml index 8b5b254f45..3b8c2cd788 100644 --- a/kernel/inferCumulativity.ml +++ b/kernel/inferCumulativity.ml @@ -77,7 +77,7 @@ let infer_sort cv_pb variances s = | CUMUL -> LSet.fold infer_level_leq (Universe.levels (Sorts.univ_of_sort s)) variances -let infer_table_key _infos variances c = +let infer_table_key variances c = let open Names in match c with | ConstKey (_, u) -> @@ -103,7 +103,7 @@ let rec infer_fterm cv_pb infos variances hd stk = | FRel _ -> infer_stack infos variances stk | FInt _ -> infer_stack infos variances stk | FFlex fl -> - let variances = infer_table_key infos variances fl in + let variances = infer_table_key variances fl in infer_stack infos variances stk | FProj (_,c) -> let variances = infer_fterm CONV infos variances c [] in -- cgit v1.2.3 From 6adc6e9484fde99ae943b31989f1454b6d079aaa Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 2 Sep 2019 09:17:29 +0200 Subject: Adding documentation for the move of sections data to kernel. --- dev/doc/critical-bugs | 12 ++++++++ .../01-kernel/10664-sections-stack-in-kernel.rst | 6 ++++ doc/sphinx/addendum/universe-polymorphism.rst | 33 ++++++++++++++-------- 3 files changed, 40 insertions(+), 11 deletions(-) create mode 100644 doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index d00c8cb11a..78d7061259 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -129,6 +129,18 @@ Universes GH issue number: #9294 risk: moderate risk to be activated by chance + component: universe polymorphism, asynchronous proofs + summary: universe constraints erroneously discarded when forcing an asynchronous proof containing delayed monomorphic constraints inside a universe polymorphic section + introduced: between 8.4 and 8.5 by merging the asynchronous proofs feature branch and universe polymorphism one + impacted released: V8.5-V8.10 + impacted development branches: none + impacted coqchk versions: immune + fixed in: PR#10664 + found by: Pédrot + exploit: no test + GH issue number: none + risk: unlikely to be triggered in interactive mode, not present in batch mode (i.e. coqc) + Primitive projections component: primitive projections, guard condition diff --git a/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst b/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst new file mode 100644 index 0000000000..bac08d12ea --- /dev/null +++ b/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst @@ -0,0 +1,6 @@ +- Section data is now part of the kernel. Solves a soundness issue + in interactive mode where global monomorphic universe constraints would be + dropped when forcing a delayed opaque proof inside a polymorphic section. Also + relaxes the nesting criterion for sections, as polymorphic sections can now + appear inside a monomorphic one + (#10664, by Pierre-Marie Pédrot). diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 7e698bfb66..1d0b732e7d 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -147,14 +147,7 @@ Many other commands support the ``Polymorphic`` flag, including: - :cmd:`Section` will locally set the polymorphism flag inside the section. - ``Variables``, ``Context``, ``Universe`` and ``Constraint`` in a section support - polymorphism. This means that the universe variables (and associated - constraints) are discharged polymorphically over definitions that use - them. In other words, two definitions in the section sharing a common - variable will both get parameterized by the universes produced by the - variable declaration. This is in contrast to a “mononorphic” variable - which introduces global universes and constraints, making the two - definitions depend on the *same* global universes associated to the - variable. + polymorphism. See :ref:`universe-polymorphism-in-sections` for more details. - :cmd:`Hint Resolve` and :cmd:`Hint Rewrite` will use the auto/rewrite hint polymorphically, not at a single instance. @@ -375,9 +368,7 @@ to universes and explicitly instantiate polymorphic definitions. as well. Global universe names live in a separate namespace. The command supports the ``Polymorphic`` flag only in sections, meaning the universe quantification will be discharged on each section definition - independently. One cannot mix polymorphic and monomorphic - declarations in the same section. - + independently. .. cmd:: Constraint @universe_constraint Polymorphic Constraint @universe_constraint @@ -510,3 +501,23 @@ underscore or by omitting the annotation to a polymorphic definition. Lemma baz : Type@{outer}. Proof. exact Type@{inner}. Qed. About baz. + +.. _universe-polymorphism-in-sections: + +Universe polymorphism and sections +---------------------------------- + +The universe polymorphic or monomorphic status is +attached to each individual section, and all term or universe declarations +contained inside must respect it, as described below. It is possible to nest a +polymorphic section inside a monomorphic one, but the converse is not allowed. + +:cmd:`Variables`, :cmd:`Context`, :cmd:`Universe` and :cmd:`Constraint` in a section support +polymorphism. This means that the universe variables and their associated +constraints are discharged polymorphically over definitions that use +them. In other words, two definitions in the section sharing a common +variable will both get parameterized by the universes produced by the +variable declaration. This is in contrast to a “mononorphic” variable +which introduces global universes and constraints, making the two +definitions depend on the *same* global universes associated to the +variable. -- cgit v1.2.3