aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cooking.ml24
-rw-r--r--kernel/declarations.ml7
-rw-r--r--kernel/declareops.ml7
-rw-r--r--kernel/entries.ml2
-rw-r--r--kernel/environ.ml8
-rw-r--r--kernel/indTyping.ml126
-rw-r--r--kernel/indTyping.mli3
-rw-r--r--kernel/indtypes.ml7
-rw-r--r--kernel/inductive.ml10
-rw-r--r--kernel/inductive.mli3
-rw-r--r--kernel/safe_typing.ml141
11 files changed, 214 insertions, 124 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 31dd26d2ba..13ee353c6b 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -295,20 +295,14 @@ let abstract_projection ~params expmod hyps t =
t
let cook_one_ind ~ntypes
- (section_decls,_ as hyps) expmod mip =
+ hyps expmod mip =
let mind_arity = match mip.mind_arity with
| RegularArity {mind_user_arity=arity;mind_sort=sort} ->
let arity = abstract_as_type (expmod arity) hyps in
let sort = destSort (expmod (mkSort sort)) in
RegularArity {mind_user_arity=arity; mind_sort=sort}
- | TemplateArity {template_param_levels=levels;template_level;template_context} ->
- let sec_levels = CList.map_filter (fun d ->
- if RelDecl.is_local_assum d then Some None
- else None)
- section_decls
- in
- let levels = List.rev_append sec_levels levels in
- TemplateArity {template_param_levels=levels;template_level;template_context}
+ | TemplateArity {template_level} ->
+ TemplateArity {template_level}
in
let mind_arity_ctxt =
let ctx = Context.Rel.map expmod mip.mind_arity_ctxt in
@@ -386,6 +380,17 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib =
in
Some (Array.append newvariance variance), Some sec_variance
in
+ let mind_template = match mib.mind_template with
+ | None -> None
+ | Some {template_param_levels=levels; template_context} ->
+ let sec_levels = CList.map_filter (fun d ->
+ if RelDecl.is_local_assum d then Some None
+ else None)
+ section_decls
+ in
+ let levels = List.rev_append sec_levels levels in
+ Some {template_param_levels=levels; template_context}
+ in
{
mind_packets;
mind_record;
@@ -396,6 +401,7 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib =
mind_nparams_rec = mib.mind_nparams_rec + nnewparams;
mind_params_ctxt;
mind_universes;
+ mind_template;
mind_variance;
mind_sec_variance;
mind_private = mib.mind_private;
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index ac130d018d..11a07ee5cf 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -30,8 +30,11 @@ type engagement = set_predicativity
*)
type template_arity = {
- template_param_levels : Univ.Level.t option list;
template_level : Univ.Universe.t;
+}
+
+type template_universes = {
+ template_param_levels : Univ.Level.t option list;
template_context : Univ.ContextSet.t;
}
@@ -218,6 +221,8 @@ type mutual_inductive_body = {
mind_universes : universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *)
+ mind_template : template_universes option;
+
mind_variance : Univ.Variance.t array option; (** Variance info, [None] when non-cumulative. *)
mind_sec_variance : Univ.Variance.t array option;
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index a3adac7a11..a1122d1279 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -46,9 +46,10 @@ let map_decl_arity f g = function
| TemplateArity a -> TemplateArity (g a)
let hcons_template_arity ar =
+ { template_level = Univ.hcons_univ ar.template_level; }
+
+let hcons_template_universe ar =
{ template_param_levels = ar.template_param_levels;
- (* List.Smart.map (Option.Smart.map Univ.hcons_univ_level) ar.template_param_levels; *)
- template_level = Univ.hcons_univ ar.template_level;
template_context = Univ.hcons_universe_context_set ar.template_context }
let universes_context = function
@@ -247,6 +248,7 @@ let subst_mind_body sub mib =
Context.Rel.map (subst_mps sub) mib.mind_params_ctxt;
mind_packets = Array.Smart.map (subst_mind_packet sub) mib.mind_packets ;
mind_universes = mib.mind_universes;
+ mind_template = mib.mind_template;
mind_variance = mib.mind_variance;
mind_sec_variance = mib.mind_sec_variance;
mind_private = mib.mind_private;
@@ -323,6 +325,7 @@ let hcons_mind mib =
{ mib with
mind_packets = Array.Smart.map hcons_mind_packet mib.mind_packets;
mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt;
+ mind_template = Option.Smart.map hcons_template_universe mib.mind_template;
mind_universes = hcons_universes mib.mind_universes }
(** Hashconsing of modules *)
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 8d930b521c..983fa822e9 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -37,7 +37,6 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1];
type one_inductive_entry = {
mind_entry_typename : Id.t;
mind_entry_arity : constr;
- mind_entry_template : bool; (* Use template polymorphism *)
mind_entry_consnames : Id.t list;
mind_entry_lc : constr list }
@@ -50,6 +49,7 @@ type mutual_inductive_entry = {
mind_entry_params : Constr.rel_context;
mind_entry_inds : one_inductive_entry list;
mind_entry_universes : universes_entry;
+ mind_entry_template : bool; (* Use template polymorphism *)
mind_entry_cumulative : bool;
(* universe constraints and the constraints for subtyping of
inductive types in the block. *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 501ac99ff3..1b5a77cc96 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -590,11 +590,11 @@ let template_polymorphic_ind (mind,i) env =
| TemplateArity _ -> true
| RegularArity _ -> false
-let template_polymorphic_variables (mind,i) env =
- match (lookup_mind mind env).mind_packets.(i).mind_arity with
- | TemplateArity { Declarations.template_param_levels = l; _ } ->
+let template_polymorphic_variables (mind, _) env =
+ match (lookup_mind mind env).mind_template with
+ | Some { Declarations.template_param_levels = l; _ } ->
List.map_filter (fun level -> level) l
- | RegularArity _ -> []
+ | None -> []
let template_polymorphic_pind (ind,u) env =
if not (Univ.Instance.is_empty u) then false
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index cc15109f06..d5aadd0c02 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -101,10 +101,10 @@ let check_indices_matter env_params info indices =
else check_context_univs ~ctor:false env_params info indices
(* env_ar contains the inductives before the current ones in the block, and no parameters *)
-let check_arity env_params env_ar ind =
+let check_arity ~template env_params env_ar ind =
let {utj_val=arity;utj_type=_} = Typeops.infer_type env_params ind.mind_entry_arity in
let indices, ind_sort = Reduction.dest_arity env_params arity in
- let ind_min_univ = if ind.mind_entry_template then Some Universe.type0m else None in
+ let ind_min_univ = if template then Some Universe.type0m else None in
let univ_info = {
ind_squashed=false;
ind_has_relevant_arg=false;
@@ -200,28 +200,88 @@ let unbounded_from_below u cstrs =
let template_polymorphic_univs ~ctor_levels uctx paramsctxt concl =
let check_level l =
Univ.LSet.mem l (Univ.ContextSet.levels uctx) &&
+ (let () = assert (not @@ Univ.Level.is_small l) in true) &&
unbounded_from_below l (Univ.ContextSet.constraints uctx) &&
not (Univ.LSet.mem l ctor_levels)
in
let univs = Univ.Universe.levels concl in
- let univs =
- Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs
- in
+ let univs = Univ.LSet.filter (fun l -> check_level l) univs in
let fold acc = function
| (LocalAssum (_, p)) ->
(let c = Term.strip_prod_assum p in
match kind c with
| Sort (Type u) ->
(match Univ.Universe.level u with
- | Some l -> if Univ.LSet.mem l univs && not (Univ.Level.is_prop l) then Some l else None
+ | Some l -> if Univ.LSet.mem l univs then Some l else None
| None -> None)
| _ -> None) :: acc
| LocalDef _ -> acc
in
let params = List.fold_left fold [] paramsctxt in
- params, univs
+ if Universe.is_type0m concl then Some (univs, params)
+ else if not @@ Univ.LSet.is_empty univs then Some (univs, params)
+ else None
+
+let get_param_levels ctx params arity splayed_lc =
+ let min_univ = match arity with
+ | RegularArity _ ->
+ CErrors.user_err
+ Pp.(strbrk "Ill-formed template mutual inductive declaration: all types must be template.")
+ | TemplateArity ar -> ar.template_level
+ in
+ let ctor_levels =
+ let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in
+ let param_levels =
+ List.fold_left (fun levels d -> match d with
+ | LocalAssum _ -> levels
+ | LocalDef (_,b,t) -> add_levels b (add_levels t levels))
+ Univ.LSet.empty params
+ in
+ Array.fold_left
+ (fun levels (d,c) ->
+ let levels =
+ List.fold_left (fun levels d ->
+ Context.Rel.Declaration.fold_constr add_levels d levels)
+ levels d
+ in
+ add_levels c levels)
+ param_levels
+ splayed_lc
+ in
+ match template_polymorphic_univs ~ctor_levels ctx params min_univ with
+ | None ->
+ CErrors.user_err
+ Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.")
+ | Some (_, param_levels) ->
+ param_levels
+
+let get_template univs params data =
+ let ctx = match univs with
+ | Monomorphic ctx -> ctx
+ | Polymorphic _ ->
+ CErrors.anomaly ~label:"polymorphic_template_ind"
+ Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") in
+ (* For each type in the block, compute potential template parameters *)
+ let params = List.map (fun ((arity, _), (_, splayed_lc), _) -> get_param_levels ctx params arity splayed_lc) data in
+ (* Pick the lower bound of template parameters. Note that in particular, if
+ one of the the inductive types from the block is Prop-valued, then no
+ parameters are template. *)
+ let fold min params =
+ let map u v = match u, v with
+ | (None, _) | (_, None) -> None
+ | Some u, Some v ->
+ let () = assert (Univ.Level.equal u v) in
+ Some u
+ in
+ List.map2 map min params
+ in
+ let params = match params with
+ | [] -> assert false
+ | hd :: rem -> List.fold_left fold hd rem
+ in
+ { template_param_levels = params; template_context = ctx }
-let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) =
+let abstract_packets usubst ((arity,lc),(indices,splayed_lc),univ_info) =
if not (Universe.Set.is_empty univ_info.missing)
then raise (InductiveError (MissingConstraints (univ_info.missing,univ_info.ind_univ)));
let arity = Vars.subst_univs_level_constr usubst arity in
@@ -237,40 +297,7 @@ let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_i
let arity = match univ_info.ind_min_univ with
| None -> RegularArity {mind_user_arity = arity; mind_sort = Sorts.sort_of_univ ind_univ}
- | Some min_univ ->
- let ctx = match univs with
- | Monomorphic ctx -> ctx
- | Polymorphic _ ->
- CErrors.anomaly ~label:"polymorphic_template_ind"
- Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") in
- let ctor_levels =
- let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in
- let param_levels =
- List.fold_left (fun levels d -> match d with
- | LocalAssum _ -> levels
- | LocalDef (_,b,t) -> add_levels b (add_levels t levels))
- Univ.LSet.empty params
- in
- Array.fold_left
- (fun levels (d,c) ->
- let levels =
- List.fold_left (fun levels d ->
- Context.Rel.Declaration.fold_constr add_levels d levels)
- levels d
- in
- add_levels c levels)
- param_levels
- splayed_lc
- in
- let param_levels, concl_levels =
- template_polymorphic_univs ~ctor_levels ctx params min_univ
- in
- if List.for_all (fun x -> Option.is_empty x) param_levels
- && Univ.LSet.is_empty concl_levels then
- CErrors.user_err
- Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.")
- else
- TemplateArity {template_param_levels = param_levels; template_level = min_univ; template_context = ctx }
+ | Some min_univ -> TemplateArity { template_level = min_univ; }
in
let kelim = allowed_sorts univ_info in
@@ -285,7 +312,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
mind_check_names mie;
assert (List.is_empty (Environ.rel_context env));
- let has_template_poly = List.exists (fun oie -> oie.mind_entry_template) mie.mind_entry_inds in
+ let has_template_poly = mie.mind_entry_template in
(* universes *)
let env_univs =
@@ -306,7 +333,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
let env_params, params = Typeops.check_context env_univs mie.mind_entry_params in
(* Arities *)
- let env_ar, data = List.fold_left_map (check_arity env_params) env_univs mie.mind_entry_inds in
+ let env_ar, data = List.fold_left_map (check_arity ~template:has_template_poly env_params) env_univs mie.mind_entry_inds in
let env_ar_par = push_rel_context params env_ar in
(* Constructors *)
@@ -352,7 +379,14 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
(* Abstract universes *)
let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in
let params = Vars.subst_univs_level_context usubst params in
- let data = List.map (abstract_packets univs usubst params) data in
+ let data = List.map (abstract_packets usubst) data in
+ let template =
+ let check ((arity, _), _, _) = match arity with
+ | TemplateArity _ -> true
+ | RegularArity _ -> false
+ in
+ if List.exists check data then Some (get_template univs params data) else None
+ in
let env_ar_par =
let ctx = Environ.rel_context env_ar_par in
@@ -361,4 +395,4 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
Environ.push_rel_context ctx env
in
- env_ar_par, univs, variance, record, params, Array.of_list data
+ env_ar_par, univs, template, variance, record, params, Array.of_list data
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index 723ba5459e..babb82c39e 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -29,6 +29,7 @@ val typecheck_inductive : env -> sec_univs:Univ.Level.t array option
-> mutual_inductive_entry
-> env
* universes
+ * template_universes option
* Univ.Variance.t array option
* Names.Id.t array option option
* Constr.rel_context
@@ -44,4 +45,4 @@ val template_polymorphic_univs :
Univ.ContextSet.t ->
Constr.rel_context ->
Univ.Universe.t ->
- Univ.Level.t option list * Univ.LSet.t
+ (Univ.LSet.t * Univ.Level.t option list) option
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index b6b8e5265c..58e5e76b61 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -466,7 +466,7 @@ let compute_projections (kn, i as ind) mib =
Array.of_list (List.rev rs),
Array.of_list (List.rev pbs)
-let build_inductive env ~sec_univs names prv univs variance
+let build_inductive env ~sec_univs names prv univs template variance
paramsctxt kn isrecord isfinite inds nmr recargs =
let ntypes = Array.length inds in
(* Compute the set of used section variables *)
@@ -538,6 +538,7 @@ let build_inductive env ~sec_univs names prv univs variance
mind_params_ctxt = paramsctxt;
mind_packets = packets;
mind_universes = univs;
+ mind_template = template;
mind_variance = variance;
mind_sec_variance = sec_variance;
mind_private = prv;
@@ -562,7 +563,7 @@ let build_inductive env ~sec_univs names prv univs variance
let check_inductive env ~sec_univs kn mie =
(* First type-check the inductive definition *)
- let (env_ar_par, univs, variance, record, paramsctxt, inds) =
+ let (env_ar_par, univs, template, variance, record, paramsctxt, inds) =
IndTyping.typecheck_inductive env ~sec_univs mie
in
(* Then check positivity conditions *)
@@ -575,6 +576,6 @@ let check_inductive env ~sec_univs kn mie =
(Array.map (fun ((_,lc),(indices,_),_) -> Context.Rel.nhyps indices,lc) inds)
in
(* Build the inductive packets *)
- build_inductive env ~sec_univs names mie.mind_entry_private univs variance
+ build_inductive env ~sec_univs names mie.mind_entry_private univs template variance
paramsctxt kn record mie.mind_entry_finite
inds nmr recargs
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 1be86f2bf8..6325779675 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -185,8 +185,8 @@ let make_subst =
exception SingletonInductiveBecomesProp of Id.t
-let instantiate_universes ctx ar args =
- let subst = make_subst (ctx,ar.template_param_levels,args) in
+let instantiate_universes ctx (templ, ar) args =
+ let subst = make_subst (ctx,templ.template_param_levels,args) in
let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in
let ty =
(* Singleton type not containing types are interpretable in Prop *)
@@ -215,8 +215,12 @@ let type_of_inductive_gen ?(polyprop=true) ((mib,mip),u) paramtyps =
match mip.mind_arity with
| RegularArity a -> subst_instance_constr u a.mind_user_arity
| TemplateArity ar ->
+ let templ = match mib.mind_template with
+ | None -> assert false
+ | Some t -> t
+ in
let ctx = List.rev mip.mind_arity_ctxt in
- let ctx,s = instantiate_universes ctx ar paramtyps in
+ let ctx,s = instantiate_universes ctx (templ, ar) paramtyps in
(* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e.
the situation where a non-Prop singleton inductive becomes Prop
when applied to Prop params *)
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index b690fe1157..90571844b9 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -123,9 +123,6 @@ exception SingletonInductiveBecomesProp of Id.t
val max_inductive_sort : Sorts.t array -> Universe.t
-val instantiate_universes : Constr.rel_context ->
- template_arity -> param_univs -> Constr.rel_context * Sorts.t
-
(** {6 Debug} *)
type size = Large | Strict
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index d8e1b6537e..a37d04d82c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -249,11 +249,52 @@ let check_engagement env expected_impredicative_set =
(** {6 Stm machinery } *)
+module Certificate :
+sig
+ type t
+
+ val make : safe_environment -> t
+
+ val universes : t -> Univ.ContextSet.t
+
+ (** Checks whether [dst] is a valid extension of [src] *)
+ val check : src:t -> dst:t -> bool
+end =
+struct
+
+type t = {
+ certif_struc : Declarations.structure_body;
+ certif_univs : Univ.ContextSet.t;
+}
+
+let make senv = {
+ certif_struc = senv.revstruct;
+ certif_univs = senv.univ;
+}
+
+let is_suffix l suf = match l with
+| [] -> false
+| _ :: l -> l == suf
+
+let is_subset (s1, cst1) (s2, cst2) =
+ Univ.LSet.subset s1 s2 && Univ.Constraint.subset cst1 cst2
+
+let check ~src ~dst =
+ is_suffix dst.certif_struc src.certif_struc &&
+ is_subset src.certif_univs dst.certif_univs
+
+let universes c = c.certif_univs
+
+end
+
type side_effect = {
- from_env : Declarations.structure_body CEphemeron.key;
+ seff_certif : Certificate.t CEphemeron.key;
seff_constant : Constant.t;
seff_body : Constr.t Declarations.constant_body;
}
+(* Invariant: For any senv, if [Certificate.check senv seff_certif] then
+ senv where univs := Certificate.universes seff_certif] +
+ (c.seff_constant -> seff_body) is well-formed. *)
module SideEffects :
sig
@@ -609,7 +650,7 @@ let inline_side_effects env body side_eff =
let filter e =
let cb = (e.seff_constant, e.seff_body) in
if Environ.mem_constant e.seff_constant env then None
- else Some (cb, e.from_env)
+ else Some (cb, e.seff_certif)
in
(* CAVEAT: we assure that most recent effects come first *)
let side_eff = List.map_filter filter (SideEffects.repr side_eff) in
@@ -678,28 +719,27 @@ let inline_private_constants env ((body, ctx), side_eff) =
let ctx' = Univ.ContextSet.union ctx ctx' in
(body, ctx')
-let is_suffix l suf = match l with
-| [] -> false
-| _ :: l -> l == suf
-
(* Given the list of signatures of side effects, checks if they match.
* I.e. if they are ordered descendants of the current revstruct.
Returns the number of effects that can be trusted. *)
-let check_signatures curmb sl =
+let check_signatures senv sl =
+ let curmb = Certificate.make senv in
let is_direct_ancestor accu mb =
match accu with
| None -> None
- | Some (n, curmb) ->
+ | Some curmb ->
try
let mb = CEphemeron.get mb in
- if is_suffix mb curmb
- then Some (n + 1, mb)
+ if Certificate.check ~src:curmb ~dst:mb
+ then Some mb
else None
with CEphemeron.InvalidKey -> None in
- let sl = List.fold_left is_direct_ancestor (Some (0, curmb)) sl in
+ let sl = List.fold_left is_direct_ancestor (Some curmb) sl in
match sl with
- | None -> 0
- | Some (n, _) -> n
+ | None -> None
+ | Some mb ->
+ let univs = Certificate.universes mb in
+ Some (Univ.ContextSet.diff univs senv.univ)
type side_effect_declaration =
| DefinitionEff : Entries.definition_entry -> side_effect_declaration
@@ -759,13 +799,14 @@ let translate_direct_opaque env kn ce =
let () = assert (is_empty_private u) in
{ cb with const_body = OpaqueDef c }
-let export_side_effects mb env eff =
+let export_side_effects senv eff =
+ let env = senv.env in
let not_exists e = not (Environ.mem_constant e.seff_constant env) in
let aux (acc,sl) e =
if not (not_exists e) then acc, sl
- else e :: acc, e.from_env :: sl in
+ else e :: acc, e.seff_certif :: sl in
let seff, signatures = List.fold_left aux ([],[]) (SideEffects.repr eff) in
- let trusted = check_signatures mb signatures in
+ let trusted = check_signatures senv signatures in
let push_seff env eff =
let { seff_constant = kn; seff_body = cb ; _ } = eff in
let env = Environ.add_constant kn (lift_constant cb) env in
@@ -774,31 +815,29 @@ let export_side_effects mb env eff =
| Monomorphic ctx ->
Environ.push_context_set ~strict:true ctx env
in
- let rec translate_seff sl seff acc env =
- match seff with
- | [] -> List.rev acc
- | eff :: rest ->
- if Int.equal sl 0 then
- let env, cb =
- let kn = eff.seff_constant in
- let ce = constant_entry_of_side_effect eff in
- let open Entries in
- let cb = match ce with
- | DefinitionEff ce ->
- Term_typing.translate_constant env kn (DefinitionEntry ce)
- | OpaqueEff ce ->
- translate_direct_opaque env kn ce
- in
- let eff = { eff with seff_body = cb } in
- (push_seff env eff, export_eff eff)
- in
- translate_seff 0 rest (cb :: acc) env
- else
- let env = push_seff env eff in
- let ecb = export_eff eff in
- translate_seff (sl - 1) rest (ecb :: acc) env
- in
- translate_seff trusted seff [] env
+ match trusted with
+ | Some univs ->
+ univs, List.map export_eff seff
+ | None ->
+ let rec recheck_seff seff acc env = match seff with
+ | [] -> List.rev acc
+ | eff :: rest ->
+ let env, cb =
+ let kn = eff.seff_constant in
+ let ce = constant_entry_of_side_effect eff in
+ let open Entries in
+ let cb = match ce with
+ | DefinitionEff ce ->
+ Term_typing.translate_constant env kn (DefinitionEntry ce)
+ | OpaqueEff ce ->
+ translate_direct_opaque env kn ce
+ in
+ let eff = { eff with seff_body = cb } in
+ (push_seff env eff, export_eff eff)
+ in
+ recheck_seff rest (cb :: acc) env
+ in
+ Univ.ContextSet.empty, recheck_seff 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
@@ -806,7 +845,8 @@ let push_opaque_proof pf senv =
senv, o
let export_private_constants eff senv =
- let exported = export_side_effects senv.revstruct senv.env eff in
+ let uctx, exported = export_side_effects senv eff in
+ let senv = push_context_set ~strict:true uctx senv in
let map senv (kn, c) = match c.const_body with
| OpaqueDef p ->
let local = empty_private c.const_universes in
@@ -828,7 +868,11 @@ let add_constant l decl senv =
| OpaqueEntry ce ->
let handle env body eff =
let body, uctx, signatures = inline_side_effects env body eff in
- let trusted = check_signatures senv.revstruct signatures in
+ let trusted = check_signatures senv signatures in
+ let trusted, uctx = match trusted with
+ | None -> 0, uctx
+ | Some univs -> List.length signatures, Univ.ContextSet.union univs uctx
+ in
body, uctx, trusted
in
let cb, ctx = Term_typing.translate_opaque senv.env kn ce in
@@ -890,9 +934,9 @@ let add_private_constant l decl senv : (Constant.t * private_constants) * safe_e
in
let senv = add_constant_aux senv (kn, dcb) in
let eff =
- let from_env = CEphemeron.create senv.revstruct in
+ let from_env = CEphemeron.create (Certificate.make senv) in
let eff = {
- from_env = from_env;
+ seff_certif = from_env;
seff_constant = kn;
seff_body = cb;
} in
@@ -1259,12 +1303,7 @@ let start_library dir senv =
required = senv.required }
let export ?except ~output_native_objects senv dir =
- let senv =
- try join_safe_environment ?except senv
- with e ->
- let e = Exninfo.capture e in
- CErrors.user_err ~hdr:"export" (CErrors.iprint e)
- in
+ let senv = join_safe_environment ?except senv in
assert(senv.future_cst = []);
let () = check_current_library dir senv in
let mp = senv.modpath in
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 15:29:49 +0000