diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cooking.ml | 10 | ||||
| -rw-r--r-- | kernel/cooking.mli | 2 | ||||
| -rw-r--r-- | kernel/entries.ml | 8 | ||||
| -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/nativevalues.ml | 4 | ||||
| -rw-r--r-- | kernel/opaqueproof.ml | 102 | ||||
| -rw-r--r-- | kernel/opaqueproof.mli | 19 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 201 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 32 | ||||
| -rw-r--r-- | kernel/section.ml | 216 | ||||
| -rw-r--r-- | kernel/section.mli | 85 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 28 |
14 files changed, 796 insertions, 160 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 0951b07d49..fae06f7163 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -161,7 +161,7 @@ type 'opaque result = { cook_universes : universes; cook_relevance : Sorts.relevance; cook_inline : inline; - cook_context : Constr.named_context option; + cook_context : Id.Set.t option; } let expmod_constr_subst cache modlist subst c = @@ -239,14 +239,10 @@ let cook_constant { from = cb; info } = | Undef _ as x -> x | Def cs -> Def (Mod_subst.from_val (map (Mod_subst.force_constr cs))) | OpaqueDef o -> - OpaqueDef (Opaqueproof.discharge_direct_opaque info o) + OpaqueDef (Opaqueproof.discharge_opaque info o) | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked") in - let const_hyps = - Context.Named.fold_outside (fun decl hyps -> - List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl'))) - hyps) - hyps0 ~init:cb.const_hyps in + let const_hyps = Id.Set.diff (Context.Named.to_vars cb.const_hyps) (Context.Named.to_vars hyps0) in let typ = abstract_constant_type (expmod cb.const_type) hyps in { cook_body = body; diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 671cdf51fe..83a8b9edfc 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -23,7 +23,7 @@ type 'opaque result = { cook_universes : universes; cook_relevance : Sorts.relevance; cook_inline : inline; - cook_context : Constr.named_context option; + cook_context : Names.Id.Set.t option; } val cook_constant : recipe -> Opaqueproof.opaque result diff --git a/kernel/entries.ml b/kernel/entries.ml index 47e2f72b0e..1e6bc14935 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -61,7 +61,7 @@ type mutual_inductive_entry = { type definition_entry = { const_entry_body : constr; (* List of section variables *) - const_entry_secctx : Constr.named_context option; + const_entry_secctx : Id.Set.t option; (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; const_entry_type : types option; @@ -70,7 +70,7 @@ type definition_entry = { type section_def_entry = { secdef_body : constr; - secdef_secctx : Constr.named_context option; + secdef_secctx : Id.Set.t option; secdef_feedback : Stateid.t option; secdef_type : types option; } @@ -78,7 +78,7 @@ type section_def_entry = { type 'a opaque_entry = { opaque_entry_body : 'a; (* List of section variables *) - opaque_entry_secctx : Constr.named_context; + opaque_entry_secctx : Id.Set.t; (* State id on which the completion of type checking is reported *) opaque_entry_feedback : Stateid.t option; opaque_entry_type : types; @@ -88,7 +88,7 @@ type 'a opaque_entry = { type inline = int option (* inlining level, None for no inlining *) type parameter_entry = - Constr.named_context option * types in_universes_entry * inline + Id.Set.t option * types in_universes_entry * inline type primitive_entry = { prim_entry_type : types option; 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/nativevalues.ml b/kernel/nativevalues.ml index e54118c775..f788832d5b 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -96,14 +96,14 @@ let mk_accu (a : atom) : t = else let data = { data with acc_arg = x :: data.acc_arg } in let ans = Obj.repr (accumulate data) in - let () = Obj.set_tag ans accumulate_tag in + let () = Obj.set_tag ans accumulate_tag [@ocaml.alert "--deprecated"] in ans in let acc = { acc_atm = a; acc_arg = [] } in let ans = Obj.repr (accumulate acc) in (** FIXME: use another representation for accumulators, this causes naked pointers. *) - let () = Obj.set_tag ans accumulate_tag in + let () = Obj.set_tag ans accumulate_tag [@ocaml.alert "--deprecated"] in (Obj.obj ans : t) let get_accu (k : accumulator) = diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index e256466112..f0b706e4f5 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -24,7 +24,7 @@ type 'a delayed_universes = | PrivateMonomorphic of 'a | PrivatePolymorphic of int * Univ.ContextSet.t -type opaque_proofterm = cooking_info list * (Constr.t * unit delayed_universes) option +type opaque_proofterm = (Constr.t * unit delayed_universes) option type indirect_accessor = { access_proof : DirPath.t -> int -> opaque_proofterm; @@ -38,10 +38,10 @@ let drop_mono = function type proofterm = (constr * Univ.ContextSet.t delayed_universes) Future.computation type opaque = - | Indirect of substitution list * DirPath.t * int (* subst, lib, index *) - | Direct of cooking_info list * proofterm +| Indirect of substitution list * cooking_info list * DirPath.t * int (* subst, discharge, lib, index *) + type opaquetab = { - opaque_val : (cooking_info list * proofterm) Int.Map.t; + opaque_val : proofterm Int.Map.t; (** Actual proof terms *) opaque_len : int; (** Size of the above map *) @@ -56,44 +56,33 @@ let empty_opaquetab = { let not_here () = CErrors.user_err Pp.(str "Cannot access opaque delayed proof") -let create cu = Direct ([],cu) - -let turn_indirect dp o tab = match o with - | Indirect (_,_,i) -> - if not (Int.Map.mem i tab.opaque_val) - then CErrors.anomaly (Pp.str "Indirect in a different table.") - else CErrors.anomaly (Pp.str "Already an indirect opaque.") - | Direct (d, cu) -> - (* Invariant: direct opaques only exist inside sections, we turn them - indirect as soon as we are at toplevel. At this moment, we perform - hashconsing of their contents, potentially as a future. *) - let hcons (c, u) = - let c = Constr.hcons c in - let u = match u with - | PrivateMonomorphic u -> PrivateMonomorphic (Univ.hcons_universe_context_set u) - | PrivatePolymorphic (n, u) -> PrivatePolymorphic (n, Univ.hcons_universe_context_set u) - in - (c, u) - in - let cu = Future.chain cu hcons in - let id = tab.opaque_len in - let opaque_val = Int.Map.add id (d,cu) tab.opaque_val in - let opaque_dir = - if DirPath.equal dp tab.opaque_dir then tab.opaque_dir - else if DirPath.equal tab.opaque_dir DirPath.initial then dp - else CErrors.anomaly - (Pp.str "Using the same opaque table for multiple dirpaths.") in - let ntab = { opaque_val; opaque_dir; opaque_len = id + 1 } in - Indirect ([],dp,id), ntab +let create dp cu tab = + let hcons (c, u) = + let c = Constr.hcons c in + let u = match u with + | PrivateMonomorphic u -> PrivateMonomorphic (Univ.hcons_universe_context_set u) + | PrivatePolymorphic (n, u) -> PrivatePolymorphic (n, Univ.hcons_universe_context_set u) + in + (c, u) + in + let cu = Future.chain cu hcons in + let id = tab.opaque_len in + let opaque_val = Int.Map.add id cu tab.opaque_val in + let opaque_dir = + if DirPath.equal dp tab.opaque_dir then tab.opaque_dir + else if DirPath.equal tab.opaque_dir DirPath.initial then dp + else CErrors.anomaly + (Pp.str "Using the same opaque table for multiple dirpaths.") in + let ntab = { opaque_val; opaque_dir; opaque_len = id + 1 } in + Indirect ([], [], dp, id), ntab let subst_opaque sub = function - | Indirect (s,dp,i) -> Indirect (sub::s,dp,i) - | Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque.") +| Indirect (s, ci, dp, i) -> Indirect (sub :: s, ci, dp, i) -let discharge_direct_opaque ci = function - | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") - | Direct (d, cu) -> - Direct (ci :: d, cu) +let discharge_opaque info = function +| Indirect (s, ci, dp, i) -> + assert (CList.is_empty s); + Indirect ([], info :: ci, dp, i) let join except cu = match except with | None -> ignore (Future.join cu) @@ -102,25 +91,21 @@ let join except cu = match except with else ignore (Future.join cu) let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (_,cu) -> join except cu - | Indirect (_,dp,i) -> - if DirPath.equal dp odp then - let (_, fp) = Int.Map.find i prfs in - join except fp +| Indirect (_,_,dp,i) -> + if DirPath.equal dp odp then + let fp = Int.Map.find i prfs in + join except fp let force_proof access { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (d, cu) -> - let (c, u) = Future.force cu in - access.access_discharge d (c, drop_mono u) - | Indirect (l,dp,i) -> + | Indirect (l,d,dp,i) -> let c, u = if DirPath.equal dp odp then - let (d, cu) = Int.Map.find i prfs in + let cu = Int.Map.find i prfs in let (c, u) = Future.force cu in access.access_discharge d (c, drop_mono u) else - let (d, cu) = access.access_proof dp i in + let cu = access.access_proof dp i in match cu with | None -> not_here () | Some (c, u) -> access.access_discharge d (c, u) @@ -133,26 +118,19 @@ let get_mono (_, u) = match u with | PrivatePolymorphic _ -> Univ.ContextSet.empty let force_constraints _access { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (_,cu) -> - get_mono (Future.force cu) - | Indirect (_,dp,i) -> +| Indirect (_,_,dp,i) -> if DirPath.equal dp odp then - let ( _, cu) = Int.Map.find i prfs in + let cu = Int.Map.find i prfs in get_mono (Future.force cu) else Univ.ContextSet.empty -let get_direct_constraints = function -| Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") -| Direct (_, cu) -> - Future.chain cu get_mono - module FMap = Future.UUIDMap let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ } = - let opaque_table = Array.make n ([], None) in + let opaque_table = Array.make n None in let f2t_map = ref FMap.empty in - let iter n (d, cu) = + let iter n cu = let uid = Future.uuid cu in let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in let c = @@ -165,7 +143,7 @@ let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ CErrors.anomaly Pp.(str"Proof object "++int n++str" is not checked nor to be checked") in - opaque_table.(n) <- (d, c) + opaque_table.(n) <- c in let () = Int.Map.iter iter otab in opaque_table, !f2t_map diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 7c53656c3c..1870241dcd 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -16,10 +16,7 @@ open Mod_subst Opaque proof terms are special since: - they can be lazily computed and substituted - they are stored in an optionally loaded segment of .vo files - An [opaque] proof terms holds the real data until fully discharged. - In this case it is called [direct]. - When it is [turn_indirect] the data is relocated to an opaque table - and the [opaque] is turned into an index. *) + An [opaque] proof terms holds an index into an opaque table. *) type 'a delayed_universes = | PrivateMonomorphic of 'a @@ -33,12 +30,7 @@ type opaque val empty_opaquetab : opaquetab (** From a [proofterm] to some [opaque]. *) -val create : proofterm -> opaque - -(** Turn a direct [opaque] into an indirect one. It is your responsibility to - hashcons the inner term beforehand. The integer is an hint of the maximum id - used so far *) -val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab +val create : DirPath.t -> proofterm -> opaquetab -> opaque * opaquetab type work_list = (Univ.Instance.t * Id.t array) Cmap.t * (Univ.Instance.t * Id.t array) Mindmap.t @@ -47,14 +39,14 @@ type cooking_info = { modlist : work_list; abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t } -type opaque_proofterm = cooking_info list * (Constr.t * unit delayed_universes) option +type opaque_proofterm = (Constr.t * unit delayed_universes) option type indirect_accessor = { access_proof : DirPath.t -> int -> opaque_proofterm; access_discharge : cooking_info list -> (Constr.t * unit delayed_universes) -> (Constr.t * unit delayed_universes); } -(** When stored indirectly, opaque terms are indexed by their library +(** Opaque terms are indexed by their library dirpath and an integer index. The two functions above activate this indirect storage, by telling how to retrieve terms. *) @@ -63,11 +55,10 @@ type indirect_accessor = { indirect opaque accessor given as an argument. *) val force_proof : indirect_accessor -> opaquetab -> opaque -> constr * unit delayed_universes val force_constraints : indirect_accessor -> opaquetab -> opaque -> Univ.ContextSet.t -val get_direct_constraints : opaque -> Univ.ContextSet.t Future.computation val subst_opaque : substitution -> opaque -> opaque -val discharge_direct_opaque : +val discharge_opaque : cooking_info -> opaque -> opaque val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 6970a11e72..9b4d2e69ac 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 +(** Part of the safe_env at a section opening time to be backtracked *) +type section_data = { + rev_env : Environ.env; + rev_univ : Univ.ContextSet.t; + rev_objlabels : Label.Set.t; +} + type safe_environment = { env : Environ.env; + sections : section_data Section.t; modpath : ModPath.t; modvariant : modvariant; modresolver : Mod_subst.delta_resolver; @@ -151,6 +159,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,14 +326,23 @@ 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 = - { senv with - env = Environ.push_context_set ~strict:(not poly) cst senv.env; - univ = Univ.ContextSet.union cst senv.univ } + if Univ.ContextSet.is_empty cst then senv + else + let sections = + if Section.is_empty senv.sections then senv.sections + else Section.push_constraints cst senv.sections + in + { senv with + env = Environ.push_context_set ~strict:(not poly) cst senv.env; + univ = Univ.ContextSet.union cst senv.univ; + sections } let add_constraints cst senv = match cst with @@ -386,7 +404,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 +451,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 +556,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 } @@ -549,30 +589,9 @@ type exported_private_constant = Constant.t let add_constant_aux ~in_section senv (kn, cb) = let l = Constant.label kn in - let delayed_cst = match cb.const_body with - | OpaqueDef o when not (Declareops.constant_is_polymorphic cb) -> - let fc = Opaqueproof.get_direct_constraints o in - begin match Future.peek_val fc with - | None -> [Later fc] - | Some c -> [Now c] - end - | Undef _ | Def _ | Primitive _ | OpaqueDef _ -> [] - in (* This is the only place where we hashcons the contents of a constant body *) let cb = if in_section then cb else Declareops.hcons_const_body cb in - let cb, otab = match cb.const_body with - | OpaqueDef lc when not in_section -> - (* In coqc, opaque constants outside sections will be stored - indirectly in a specific table *) - let od, otab = - Opaqueproof.turn_indirect - (library_dp_of_senv senv) lc (Environ.opaque_tables senv.env) in - { cb with const_body = OpaqueDef od }, otab - | _ -> cb, (Environ.opaque_tables senv.env) - in - let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in let senv' = add_field (l,SFBconst cb) (C kn) senv in - let senv' = add_constraints_list delayed_cst senv' in let senv'' = match cb.const_body with | Undef (Some lev) -> update_resolver @@ -703,7 +722,7 @@ let constant_entry_of_side_effect eff = if Declareops.is_opaque cb then OpaqueEff { opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); - opaque_entry_secctx = cb.const_hyps; + opaque_entry_secctx = Context.Named.to_vars cb.const_hyps; opaque_entry_feedback = None; opaque_entry_type = cb.const_type; opaque_entry_universes = univs; @@ -711,7 +730,7 @@ let constant_entry_of_side_effect eff = else DefinitionEff { const_entry_body = p; - const_entry_secctx = Some cb.const_hyps; + const_entry_secctx = Some (Context.Named.to_vars cb.const_hyps); const_entry_feedback = None; const_entry_type = Some cb.const_type; const_entry_universes = univs; @@ -775,27 +794,30 @@ let export_side_effects mb env (b_ctx, eff) = in translate_seff trusted seff [] env +let push_opaque_proof pf senv = + let o, otab = Opaqueproof.create (library_dp_of_senv senv) pf (Environ.opaque_tables senv.env) in + let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in + senv, o + let export_private_constants ~in_section ce senv = let exported, ce = export_side_effects senv.revstruct senv.env ce in - let map univs p = - let local = match univs with + let map senv (kn, c) = match c.const_body with + | OpaqueDef p -> + let local = match c.const_universes with | Monomorphic _ -> Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty | Polymorphic auctx -> Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, Univ.ContextSet.empty) in - Opaqueproof.create (Future.from_val (p, local)) + let senv, o = push_opaque_proof (Future.from_val (p, local)) senv in + senv, (kn, { c with const_body = OpaqueDef o }) + | Def _ | Undef _ | Primitive _ as body -> + senv, (kn, { c with const_body = body }) in - let map (kn, cb) = (kn, map_constant (fun c -> map cb.const_universes c) cb) in - let bodies = List.map map exported in + let senv, bodies = List.fold_left_map map senv exported in let exported = List.map (fun (kn, _) -> kn) exported in + (* No delayed constants to declare *) let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in (ce, exported), senv -let add_recipe ~in_section l r senv = - let kn = Constant.make2 senv.modpath l in - let cb = Term_typing.translate_recipe senv.env kn r in - let senv = add_constant_aux ~in_section senv (kn, cb) in - kn, senv - let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl senv : (Constant.t * a) * safe_environment = let kn = Constant.make2 senv.modpath l in let cb = @@ -811,8 +833,29 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen Term_typing.translate_constant Term_typing.Pure senv.env kn ce in let senv = - let cb = map_constant (fun c -> Opaqueproof.create c) cb in - add_constant_aux ~in_section senv (kn, cb) in + let senv, cb, delayed_cst = match cb.const_body with + | OpaqueDef fc -> + let senv, o = push_opaque_proof fc senv in + let delayed_cst = + if not (Declareops.constant_is_polymorphic cb) then + let map (_, u) = match u with + | Opaqueproof.PrivateMonomorphic ctx -> ctx + | Opaqueproof.PrivatePolymorphic _ -> assert false + in + let fc = Future.chain fc map in + match Future.peek_val fc with + | None -> [Later fc] + | Some c -> [Now c] + else [] + in + senv, { cb with const_body = OpaqueDef o }, delayed_cst + | Undef _ | Def _ | Primitive _ as body -> + senv, { cb with const_body = body }, [] + in + let senv = add_constant_aux ~in_section senv (kn, cb) in + add_constraints_list delayed_cst senv + in + let senv = match decl with | ConstantEntry (_,(Entries.PrimitiveEntry { Entries.prim_entry_content = CPrimitives.OT_type t; _ })) -> @@ -902,6 +945,76 @@ let add_module l me inl senv = in (mp,mb.mod_delta),senv'' +(** {6 Interactive sections *) + +let open_section senv = + let custom = { + rev_env = senv.env; + rev_univ = senv.univ; + rev_objlabels = senv.objlabels; + } in + let sections = Section.open_section ~custom senv.sections in + { senv with sections } + +let close_section senv = + let open Section in + let sections0 = senv.sections in + let env0 = senv.env in + (* First phase: revert the declarations added in the section *) + let sections, entries, cstrs, revert = Section.close_section sections0 in + let rec pop_revstruct accu entries revstruct = match entries, revstruct with + | [], revstruct -> accu, revstruct + | _ :: _, [] -> + CErrors.anomaly (Pp.str "Unmatched section data") + | entry :: entries, (lbl, leaf) :: revstruct -> + let data = match entry, leaf with + | SecDefinition kn, SFBconst cb -> + let () = assert (Label.equal lbl (Constant.label kn)) in + `Definition (kn, cb) + | SecInductive ind, SFBmind mib -> + let () = assert (Label.equal lbl (MutInd.label ind)) in + `Inductive (ind, mib) + | (SecDefinition _ | SecInductive _), (SFBconst _ | SFBmind _) -> + CErrors.anomaly (Pp.str "Section content mismatch") + | (SecDefinition _ | SecInductive _), (SFBmodule _ | SFBmodtype _) -> + CErrors.anomaly (Pp.str "Module inside a section") + in + pop_revstruct (data :: accu) entries revstruct + in + let redo, revstruct = pop_revstruct [] entries senv.revstruct in + (* Don't revert the delayed constraints. If some delayed constraints were + forced inside the section, they have been turned into global monomorphic + that are going to be replayed. Those that are not forced are not readded + by {!add_constant_aux}. *) + let { rev_env = env; rev_univ = univ; rev_objlabels = objlabels } = revert in + (* Do not revert the opaque table, the discharged opaque constants are + referring to it. *) + let env = Environ.set_opaque_tables env (Environ.opaque_tables senv.env) in + let senv = { senv with env; revstruct; sections; univ; objlabels; } in + (* Second phase: replay the discharged section contents *) + let senv = add_constraints (Now cstrs) senv in + let modlist = Section.replacement_context env0 sections0 in + let cooking_info seg = + let { abstr_ctx; abstr_subst; abstr_uctx } = seg in + let abstract = (abstr_ctx, abstr_subst, abstr_uctx) in + { Opaqueproof.modlist; abstract } + in + let fold senv = function + | `Definition (kn, cb) -> + let in_section = not (Section.is_empty senv.sections) in + let info = cooking_info (Section.segment_of_constant env0 kn sections0) in + let r = { Cooking.from = cb; info } in + let cb = Term_typing.translate_recipe senv.env kn r in + (* Delayed constants are already in the global environment *) + add_constant_aux ~in_section senv (kn, cb) + | `Inductive (ind, mib) -> + let info = cooking_info (Section.segment_of_inductive env0 ind sections0) in + let mie = Cooking.cook_inductive info mib in + let mie = InferCumulativity.infer_inductive senv.env mie in + let _, senv = add_mind (MutInd.label ind) mie senv in + senv + in + List.fold_left fold senv redo (** {6 Starting / ending interactive modules and module types } *) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index fa53fa33fa..d97d61a72f 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -27,12 +27,16 @@ val digest_match : actual:vodigest -> required:vodigest -> bool type safe_environment +type section_data + val empty_environment : safe_environment val is_initial : safe_environment -> bool val env_of_safe_env : safe_environment -> Environ.env +val sections_of_safe_env : safe_environment -> section_data Section.t + (** The safe_environment state monad *) type safe_transformer0 = safe_environment -> safe_environment @@ -67,15 +71,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 = @@ -96,9 +91,6 @@ val add_constant : side_effect:'a effect_entry -> in_section:bool -> Label.t -> global_declaration -> (Constant.t * 'a) safe_transformer -val add_recipe : - in_section:bool -> Label.t -> Cooking.recipe -> Constant.t safe_transformer - (** Adding an inductive type *) val add_mind : @@ -140,6 +132,22 @@ val set_allow_sprop : bool -> safe_transformer0 val check_engagement : Environ.env -> Declarations.set_predicativity -> unit +(** {6 Interactive section functions } *) + +val open_section : 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..babd9fe7a1 --- /dev/null +++ b/kernel/section.ml @@ -0,0 +1,216 @@ +(************************************************************************) +(* * 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_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_mono_universes : ContextSet.t; + sec_poly_universes : Name.t array * UContext.t; + (** Universes local to the section *) + has_poly_univs : bool; + (** Are there polymorphic universes or constraints, including in previous sections. *) + sec_entries : section_entry list; + (** Definitions introduced in the section *) + sec_data : (Instance.t * AUContext.t) entry_map; + (** Additional data synchronized with the section *) + sec_custom : 'a; +} + +(** Sections can be nested with the proviso that no monomorphic section can be + opened inside a polymorphic one. The reverse is allowed. *) +type 'a t = 'a section list + +let empty = [] + +let is_empty = List.is_empty + +let has_poly_univs = function + | [] -> false + | sec :: _ -> sec.has_poly_univs + +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) + +let on_last_section f sections = match sections with +| [] -> CErrors.user_err (Pp.str "No opened section") +| sec :: rem -> f sec :: rem + +let with_last_section f sections = match sections with +| [] -> f None +| sec :: _ -> f (Some 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 sec = + if UContext.is_empty ctx then sec + else + let (snas, sctx) = sec.sec_poly_universes in + let sec_poly_universes = (Array.append snas nas, UContext.union sctx ctx) in + { sec with sec_poly_universes; has_poly_univs = true } + in + on_last_section on_sec s + +let is_polymorphic_univ u s = + let check sec = + let (_, uctx) = sec.sec_poly_universes in + Array.exists (fun u' -> Level.equal u u') (Instance.to_array (UContext.instance uctx)) + in + List.exists check s + +let push_constraints uctx s = + let on_sec sec = + if sec.has_poly_univs && Constraint.exists (fun (l,_,r) -> is_polymorphic_univ l s || is_polymorphic_univ r s) (snd uctx) + then CErrors.user_err Pp.(str "Cannot add monomorphic constraints which refer to section polymorphic universes."); + let uctx' = sec.sec_mono_universes in + let sec_mono_universes = (ContextSet.union uctx uctx') in + { sec with sec_mono_universes } + in + on_last_section on_sec s + +let open_section ~custom sections = + let sec = { + sec_context = 0; + sec_mono_universes = ContextSet.empty; + sec_poly_universes = ([||], UContext.empty); + has_poly_univs = has_poly_univs sections; + sec_entries = []; + sec_data = (Cmap.empty, Mindmap.empty); + sec_custom = custom; + } in + sec :: sections + +let close_section sections = + match sections with + | sec :: sections -> + sections, sec.sec_entries, sec.sec_mono_universes, sec.sec_custom + | [] -> + CErrors.user_err (Pp.str "No opened section.") + +let make_decl_univs (nas,uctx) = abstract_universes nas uctx + +let push_global ~poly e s = + if is_empty s then s + else if has_poly_univs s && not poly + then CErrors.user_err + Pp.(str "Cannot add a universe monomorphic declaration when \ + section polymorphic universes are present.") + else + let on_sec sec = + { sec with + sec_entries = e :: sec.sec_entries; + sec_data = add_emap e (make_decl_univs sec.sec_poly_universes) sec.sec_data; + } + 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 : Instance.t; + abstr_uctx : AUContext.t; +} + +let empty_segment = { + abstr_ctx = []; + abstr_subst = Instance.empty; + abstr_uctx = AUContext.empty; +} + +let extract_hyps sec vars used = + (* Keep the section-local segment of variables *) + let vars = List.firstn sec.sec_context vars in + (* Only keep the part that is used by the declaration *) + List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) used) vars + +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 s = match s with + | None -> + CErrors.user_err (Pp.str "No opened section.") + | Some sec -> + let hyps = extract_hyps sec vars hyps in + let inst, auctx = find_emap e sec.sec_data 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 + let used = Context.Named.to_vars body.Declarations.const_hyps in + section_segment_of_entry vars (SecDefinition con) used s + +let segment_of_inductive env mind s = + let mib = Environ.lookup_mind mind env in + let vars = Environ.named_context env in + let used = Context.Named.to_vars mib.Declarations.mind_hyps in + section_segment_of_entry vars (SecInductive mind) used 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 diff --git a/kernel/section.mli b/kernel/section.mli new file mode 100644 index 0000000000..56b4d9ba8f --- /dev/null +++ b/kernel/section.mli @@ -0,0 +1,85 @@ +(************************************************************************) +(* * 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 'a t +(** Type of sections with additional data ['a] *) + +val empty : 'a t + +val is_empty : 'a t -> bool +(** Checks whether there is no opened section *) + +(** {6 Manipulating sections} *) + +type section_entry = +| SecDefinition of Constant.t +| SecInductive of MutInd.t + +val open_section : custom:'a -> 'a t -> 'a 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. A custom data can be attached to this section, + that will be returned by {!close_section}. *) + +val close_section : 'a t -> 'a t * section_entry list * ContextSet.t * 'a +(** Close the current section and returns the entries defined inside, the set + of global monomorphic constraints added in this section, and the custom data + provided at the opening of the section. *) + +(** {6 Extending sections} *) + +val push_local : 'a t -> 'a t +(** Extend the current section with a local definition (cf. push_named). *) + +val push_context : Name.t array * UContext.t -> 'a t -> 'a t +(** Extend the current section with a local universe context. Assumes that the + last opened section is polymorphic. *) + +val push_constraints : ContextSet.t -> 'a t -> 'a t +(** Extend the current section with a global universe context. + Assumes that the last opened section is monomorphic. *) + +val push_constant : poly:bool -> Constant.t -> 'a t -> 'a t +(** Make the constant as having been defined in this section. *) + +val push_inductive : poly:bool -> MutInd.t -> 'a t -> 'a 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 -> 'a t -> abstr_info +(** Section segment at the time of the constant declaration *) + +val segment_of_inductive : Environ.env -> MutInd.t -> 'a t -> abstr_info +(** Section segment at the time of the inductive declaration *) + +val replacement_context : Environ.env -> 'a t -> Opaqueproof.work_list +(** Section segments of all declarations from this section. *) + +val is_in_section : Environ.env -> GlobRef.t -> 'a t -> bool diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index b65e62ba30..f70b2960cf 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -221,9 +221,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let build_constant_declaration env result = let open Cooking in let typ = result.cook_type in - let check declared inferred = - let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in - let inferred_set, declared_set = mk_set inferred, mk_set declared in + let check declared_set inferred_set = if not (Id.Set.subset inferred_set declared_set) then let l = Id.Set.elements (Id.Set.diff inferred_set declared_set) in let n = List.length l in @@ -239,11 +237,6 @@ let build_constant_declaration env result = str "Proof using " ++ declared_vars ++ fnl () ++ str "to" ++ fnl () ++ str "Proof using " ++ inferred_vars) in - let sort l = - List.filter (fun decl -> - let id = NamedDecl.get_id decl in - List.exists (NamedDecl.get_id %> Names.Id.equal id) l) - (named_context env) in (* We try to postpone the computation of used section variables *) let hyps, def = let context_ids = List.map NamedDecl.get_id (named_context env) in @@ -252,7 +245,7 @@ let build_constant_declaration env result = | None -> if List.is_empty context_ids then (* Empty section context: no need to check *) - [], def + Id.Set.empty, def else (* No declared section vars, and non-empty section context: we must look at the body NOW, if any *) @@ -264,16 +257,19 @@ let build_constant_declaration env result = (* Opaque definitions always come with their section variables *) assert false in - keep_hyps env (Id.Set.union ids_typ ids_def), def + Environ.really_needed env (Id.Set.union ids_typ ids_def), def | Some declared -> + let needed = Environ.really_needed env declared in + (* Transitive closure ensured by the upper layers *) + let () = assert (Id.Set.equal needed declared) in (* We use the declared set and chain a check of correctness *) - sort declared, + declared, match def with | Undef _ | Primitive _ as x -> x (* nothing to check *) | Def cs as x -> let ids_typ = global_vars_set env typ in let ids_def = global_vars_set env (Mod_subst.force_constr cs) in - let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in + let inferred = Environ.really_needed env (Id.Set.union ids_typ ids_def) in check declared inferred; x | OpaqueDef lc -> (* In this case we can postpone the check *) @@ -281,12 +277,13 @@ let build_constant_declaration env result = let kont c = let ids_typ = global_vars_set env typ in let ids_def = global_vars_set env c in - let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in + let inferred = Environ.really_needed env (Id.Set.union ids_typ ids_def) in check declared inferred in OpaqueDef (iter kont lc) in let univs = result.cook_universes in + let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in let tps = let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in Option.map Cemitcodes.from_val res @@ -317,7 +314,10 @@ let translate_recipe env _kn r = let univs = result.cook_universes in let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs result.cook_body in let tps = Option.map Cemitcodes.from_val res in - { const_hyps = Option.get result.cook_context; + let hyps = Option.get result.cook_context in + (* Trust the set of section hypotheses generated by Cooking *) + let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in + { const_hyps = hyps; const_body = result.cook_body; const_type = result.cook_type; const_body_code = tps; |