diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/safe_typing.ml | 276 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 271 | ||||
| -rw-r--r-- | kernel/term_typing.mli | 42 |
3 files changed, 283 insertions, 306 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 625b7e5073..f042001254 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -216,15 +216,55 @@ let get_opaque_body env cbo = (Opaqueproof.force_proof (Environ.opaque_tables env) opaque, Opaqueproof.force_constraints (Environ.opaque_tables env) opaque) -type private_constants = Term_typing.side_effects +type side_effect = { + from_env : Declarations.structure_body CEphemeron.key; + eff : Entries.side_eff list; +} -let empty_private_constants = Term_typing.empty_seff -let add_private = Term_typing.add_seff -let concat_private = Term_typing.concat_seff -let mk_pure_proof = Term_typing.mk_pure_proof -let inline_private_constants_in_constr = Term_typing.inline_side_effects -let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects -let side_effects_of_private_constants = Term_typing.uniq_seff +module SideEffects : +sig + type t + val repr : t -> side_effect list + val empty : t + val add : side_effect -> t -> t + val concat : t -> t -> t +end = +struct + +module SeffOrd = struct +open Entries +type t = side_effect +let compare e1 e2 = + let cmp e1 e2 = Constant.CanOrd.compare e1.seff_constant e2.seff_constant in + List.compare cmp e1.eff e2.eff +end + +module SeffSet = Set.Make(SeffOrd) + +type t = { seff : side_effect list; elts : SeffSet.t } +(** Invariant: [seff] is a permutation of the elements of [elts] *) + +let repr eff = eff.seff +let empty = { seff = []; elts = SeffSet.empty } +let add x es = + if SeffSet.mem x es.elts then es + else { seff = x :: es.seff; elts = SeffSet.add x es.elts } +let concat xes yes = + List.fold_right add xes.seff yes + +end + +type private_constants = SideEffects.t + +let side_effects_of_private_constants l = + let ans = List.rev (SideEffects.repr l) in + List.map_append (fun { eff; _ } -> eff) ans + +let empty_private_constants = SideEffects.empty +let add_private mb eff effs = + let from_env = CEphemeron.create mb in + SideEffects.add { eff; from_env } effs +let concat_private = SideEffects.concat let make_eff env cst r = let open Entries in @@ -257,7 +297,7 @@ let universes_of_private eff = | Monomorphic_const ctx -> ctx :: acc | Polymorphic_const _ -> acc in - List.fold_left fold [] (Term_typing.uniq_seff eff) + List.fold_left fold [] (side_effects_of_private_constants eff) let env_of_safe_env senv = senv.env let env_of_senv = env_of_safe_env @@ -507,8 +547,217 @@ let add_constant_aux ~in_section senv (kn, cb) = in senv'' +let mk_pure_proof c = (c, Univ.ContextSet.empty), SideEffects.empty + +let inline_side_effects env body ctx side_eff = + let open Entries in + let open Constr in + (** First step: remove the constants that are still in the environment *) + let filter { eff = se; from_env = mb } = + let map e = (e.seff_constant, e.seff_body, e.seff_env) in + let cbl = List.map map se in + let not_exists (c,_,_) = + try ignore(Environ.lookup_constant c env); false + with Not_found -> true in + let cbl = List.filter not_exists cbl in + (cbl, mb) + in + (* CAVEAT: we assure that most recent effects come first *) + let side_eff = List.map filter (SideEffects.repr side_eff) in + let sigs = List.rev_map (fun (cbl, mb) -> mb, List.length cbl) side_eff in + let side_eff = List.fold_left (fun accu (cbl, _) -> cbl @ accu) [] side_eff in + let side_eff = List.rev side_eff in + (** Most recent side-effects first in side_eff *) + if List.is_empty side_eff then (body, ctx, sigs) + else + (** Second step: compute the lifts and substitutions to apply *) + let cname c = Name (Label.to_id (Constant.label c)) in + let fold (subst, var, ctx, args) (c, cb, b) = + let (b, opaque) = match cb.const_body, b with + | Def b, _ -> (Mod_subst.force_constr b, false) + | OpaqueDef _, `Opaque (b,_) -> (b, true) + | _ -> assert false + in + match cb.const_universes with + | Monomorphic_const univs -> + (** Abstract over the term at the top of the proof *) + let ty = cb.const_type in + let subst = Cmap_env.add c (Inr var) subst in + let ctx = Univ.ContextSet.union ctx univs in + (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args) + | Polymorphic_const _auctx -> + (** Inline the term to emulate universe polymorphism *) + let subst = Cmap_env.add c (Inl b) subst in + (subst, var, ctx, args) + in + let (subst, len, ctx, args) = List.fold_left fold (Cmap_env.empty, 1, ctx, []) side_eff in + (** Third step: inline the definitions *) + let rec subst_const i k t = match Constr.kind t with + | Const (c, u) -> + let data = try Some (Cmap_env.find c subst) with Not_found -> None in + begin match data with + | None -> t + | Some (Inl b) -> + (** [b] is closed but may refer to other constants *) + subst_const i k (Vars.subst_instance_constr u b) + | Some (Inr n) -> + mkRel (k + n - i) + end + | Rel n -> + (** Lift free rel variables *) + if n <= k then t + else mkRel (n + len - i - 1) + | _ -> Constr.map_with_binders ((+) 1) (fun k t -> subst_const i k t) k t + in + let map_args i (na, b, ty, opaque) = + (** Both the type and the body may mention other constants *) + let ty = subst_const (len - i - 1) 0 ty in + let b = subst_const (len - i - 1) 0 b in + (na, b, ty, opaque) + in + let args = List.mapi map_args args in + let body = subst_const 0 0 body in + let fold_arg (na, b, ty, opaque) accu = + if opaque then mkApp (mkLambda (na, ty, accu), [|b|]) + else mkLetIn (na, b, ty, accu) + in + let body = List.fold_right fold_arg args body in + (body, ctx, sigs) + +let inline_private_constants_in_definition_entry env ce = + let open Entries in + { ce with + const_entry_body = Future.chain + ce.const_entry_body (fun ((body, ctx), side_eff) -> + let body, ctx',_ = inline_side_effects env body ctx side_eff in + (body, ctx'), ()); + } + +let inline_private_constants_in_constr env body side_eff = + pi1 (inline_side_effects env body Univ.ContextSet.empty side_eff) + +let rec is_nth_suffix n l suf = + if Int.equal n 0 then l == suf + else match l with + | [] -> false + | _ :: l -> is_nth_suffix (pred n) 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 is_direct_ancestor accu (mb, how_many) = + match accu with + | None -> None + | Some (n, curmb) -> + try + let mb = CEphemeron.get mb in + if is_nth_suffix how_many mb curmb + then Some (n + how_many, mb) + else None + with CEphemeron.InvalidKey -> None in + let sl = List.fold_left is_direct_ancestor (Some (0, curmb)) sl in + match sl with + | None -> 0 + | Some (n, _) -> n + + +let constant_entry_of_side_effect cb u = + let open Entries in + let univs = + match cb.const_universes with + | Monomorphic_const uctx -> + Monomorphic_const_entry uctx + | Polymorphic_const auctx -> + Polymorphic_const_entry (Univ.AUContext.repr auctx) + in + let pt = + match cb.const_body, u with + | OpaqueDef _, `Opaque (b, c) -> b, c + | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty + | _ -> assert false in + DefinitionEntry { + const_entry_body = Future.from_val (pt, ()); + const_entry_secctx = None; + const_entry_feedback = None; + const_entry_type = Some cb.const_type; + const_entry_universes = univs; + const_entry_opaque = Declareops.is_opaque cb; + const_entry_inline_code = cb.const_inline_code } + +let turn_direct orig = + let open Entries in + let cb = orig.seff_body in + if Declareops.is_opaque cb then + let p = match orig.seff_env with + | `Opaque (b, c) -> (b, c) + | _ -> assert false + in + let const_body = OpaqueDef (Opaqueproof.create (Future.from_val p)) in + let cb = { cb with const_body } in + { orig with seff_body = cb } + else orig + +let export_eff eff = + let open Entries in + (eff.seff_constant, eff.seff_body, eff.seff_role) + +let export_side_effects mb env c = + let open Entries in + let body = c.const_entry_body in + let _, eff = Future.force body in + let ce = { c with + Entries.const_entry_body = Future.chain body + (fun (b_ctx, _) -> b_ctx, ()) } in + let not_exists e = + try ignore(Environ.lookup_constant e.seff_constant env); false + with Not_found -> true in + let aux (acc,sl) { eff = se; from_env = mb } = + let cbl = List.filter not_exists se in + if List.is_empty cbl then acc, sl + else cbl :: acc, (mb,List.length cbl) :: sl in + let seff, signatures = List.fold_left aux ([],[]) (SideEffects.repr eff) in + let trusted = check_signatures mb signatures in + let push_seff env eff = + let { seff_constant = kn; seff_body = cb ; _ } = eff in + let env = Environ.add_constant kn cb env in + match cb.const_universes with + | Polymorphic_const _ -> env + | Monomorphic_const ctx -> + let ctx = match eff.seff_env with + | `Nothing -> ctx + | `Opaque(_, ctx') -> Univ.ContextSet.union ctx' ctx + in + Environ.push_context_set ~strict:true ctx env + in + let rec translate_seff sl seff acc env = + match seff with + | [] -> List.rev acc, ce + | cbs :: rest -> + if Int.equal sl 0 then + let env, cbs = + List.fold_left (fun (env,cbs) eff -> + let { seff_constant = kn; seff_body = ocb; seff_env = u ; _ } = eff in + let ce = constant_entry_of_side_effect ocb u in + let cb = Term_typing.translate_constant Term_typing.Pure env kn ce in + let eff = { eff with + seff_body = cb; + seff_env = `Nothing; + } in + (push_seff env eff, export_eff eff :: cbs)) + (env,[]) cbs in + translate_seff 0 rest (cbs @ acc) env + else + let cbs_len = List.length cbs in + let cbs = List.map turn_direct cbs in + let env = List.fold_left push_seff env cbs in + let ecbs = List.map export_eff cbs in + translate_seff (sl - cbs_len) rest (ecbs @ acc) env + in + translate_seff trusted seff [] env + let export_private_constants ~in_section ce senv = - let exported, ce = Term_typing.export_side_effects senv.revstruct senv.env ce in + let exported, ce = export_side_effects senv.revstruct senv.env ce in let bodies = List.map (fun (kn, cb, _) -> (kn, cb)) exported in let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in @@ -520,7 +769,12 @@ let add_constant ~in_section l decl senv = let cb = match decl with | ConstantEntry (EffectEntry, ce) -> - Term_typing.translate_constant (Term_typing.SideEffects senv.revstruct) senv.env kn ce + let handle env body uctx eff = + let body, uctx, signatures = inline_side_effects env body uctx eff in + let trusted = check_signatures senv.revstruct signatures in + body, uctx, trusted + in + Term_typing.translate_constant (Term_typing.SideEffects handle) senv.env kn ce | ConstantEntry (PureEntry, ce) -> Term_typing.translate_constant Term_typing.Pure senv.env kn ce | GlobalRecipe r -> diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 5ccc23eefc..644f07adfa 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -27,159 +27,12 @@ module NamedDecl = Context.Named.Declaration (* Insertion of constants and parameters in environment. *) -type side_effect = { - from_env : Declarations.structure_body CEphemeron.key; - eff : side_eff list; -} - -module SideEffects : -sig - type t - val repr : t -> side_effect list - val empty : t - val add : side_effect -> t -> t - val concat : t -> t -> t -end = -struct - -module SeffOrd = struct -type t = side_effect -let compare e1 e2 = - let cmp e1 e2 = Constant.CanOrd.compare e1.seff_constant e2.seff_constant in - List.compare cmp e1.eff e2.eff -end - -module SeffSet = Set.Make(SeffOrd) - -type t = { seff : side_effect list; elts : SeffSet.t } -(** Invariant: [seff] is a permutation of the elements of [elts] *) - -let repr eff = eff.seff -let empty = { seff = []; elts = SeffSet.empty } -let add x es = - if SeffSet.mem x es.elts then es - else { seff = x :: es.seff; elts = SeffSet.add x es.elts } -let concat xes yes = - List.fold_right add xes.seff yes - -end - -type side_effects = SideEffects.t +type 'a effect_handler = + env -> Constr.t -> Univ.ContextSet.t -> 'a -> (Constr.t * Univ.ContextSet.t * int) type _ trust = | Pure : unit trust -| SideEffects : structure_body -> side_effects trust - -let uniq_seff_rev = SideEffects.repr -let uniq_seff l = - let ans = List.rev (SideEffects.repr l) in - List.map_append (fun { eff ; _ } -> eff) ans - -let empty_seff = SideEffects.empty -let add_seff mb eff effs = - let from_env = CEphemeron.create mb in - SideEffects.add { eff; from_env } effs -let concat_seff = SideEffects.concat - -let mk_pure_proof c = (c, Univ.ContextSet.empty), empty_seff - -let inline_side_effects env body ctx side_eff = - (** First step: remove the constants that are still in the environment *) - let filter { eff = se; from_env = mb } = - let map e = (e.seff_constant, e.seff_body, e.seff_env) in - let cbl = List.map map se in - let not_exists (c,_,_) = - try ignore(Environ.lookup_constant c env); false - with Not_found -> true in - let cbl = List.filter not_exists cbl in - (cbl, mb) - in - (* CAVEAT: we assure that most recent effects come first *) - let side_eff = List.map filter (uniq_seff_rev side_eff) in - let sigs = List.rev_map (fun (cbl, mb) -> mb, List.length cbl) side_eff in - let side_eff = List.fold_left (fun accu (cbl, _) -> cbl @ accu) [] side_eff in - let side_eff = List.rev side_eff in - (** Most recent side-effects first in side_eff *) - if List.is_empty side_eff then (body, ctx, sigs) - else - (** Second step: compute the lifts and substitutions to apply *) - let cname c = Name (Label.to_id (Constant.label c)) in - let fold (subst, var, ctx, args) (c, cb, b) = - let (b, opaque) = match cb.const_body, b with - | Def b, _ -> (Mod_subst.force_constr b, false) - | OpaqueDef _, `Opaque (b,_) -> (b, true) - | _ -> assert false - in - match cb.const_universes with - | Monomorphic_const univs -> - (** Abstract over the term at the top of the proof *) - let ty = cb.const_type in - let subst = Cmap_env.add c (Inr var) subst in - let ctx = Univ.ContextSet.union ctx univs in - (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args) - | Polymorphic_const _auctx -> - (** Inline the term to emulate universe polymorphism *) - let subst = Cmap_env.add c (Inl b) subst in - (subst, var, ctx, args) - in - let (subst, len, ctx, args) = List.fold_left fold (Cmap_env.empty, 1, ctx, []) side_eff in - (** Third step: inline the definitions *) - let rec subst_const i k t = match Constr.kind t with - | Const (c, u) -> - let data = try Some (Cmap_env.find c subst) with Not_found -> None in - begin match data with - | None -> t - | Some (Inl b) -> - (** [b] is closed but may refer to other constants *) - subst_const i k (Vars.subst_instance_constr u b) - | Some (Inr n) -> - mkRel (k + n - i) - end - | Rel n -> - (** Lift free rel variables *) - if n <= k then t - else mkRel (n + len - i - 1) - | _ -> Constr.map_with_binders ((+) 1) (fun k t -> subst_const i k t) k t - in - let map_args i (na, b, ty, opaque) = - (** Both the type and the body may mention other constants *) - let ty = subst_const (len - i - 1) 0 ty in - let b = subst_const (len - i - 1) 0 b in - (na, b, ty, opaque) - in - let args = List.mapi map_args args in - let body = subst_const 0 0 body in - let fold_arg (na, b, ty, opaque) accu = - if opaque then mkApp (mkLambda (na, ty, accu), [|b|]) - else mkLetIn (na, b, ty, accu) - in - let body = List.fold_right fold_arg args body in - (body, ctx, sigs) - -let rec is_nth_suffix n l suf = - if Int.equal n 0 then l == suf - else match l with - | [] -> false - | _ :: l -> is_nth_suffix (pred n) 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 is_direct_ancestor accu (mb, how_many) = - match accu with - | None -> None - | Some (n, curmb) -> - try - let mb = CEphemeron.get mb in - if is_nth_suffix how_many mb curmb - then Some (n + how_many, mb) - else None - with CEphemeron.InvalidKey -> None in - let sl = List.fold_left is_direct_ancestor (Some (0, curmb)) sl in - match sl with - | None -> 0 - | Some (n, _) -> n +| SideEffects : 'a effect_handler -> 'a trust let skip_trusted_seff sl b e = let rec aux sl b e acc = @@ -259,9 +112,8 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let j = infer env body in let _ = judge_of_cast env j DEFAULTcast tyj in j, uctx - | SideEffects mb -> - let (body, uctx, signatures) = inline_side_effects env body uctx side_eff in - let valid_signatures = check_signatures mb signatures in + | SideEffects handle -> + let (body, uctx, valid_signatures) = handle env body uctx side_eff in let env = push_context_set uctx env in let body,env,ectx = skip_trusted_seff valid_signatures body env in let j = infer env body in @@ -286,9 +138,11 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let { const_entry_type = typ; const_entry_opaque = opaque ; _ } = c in let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in let (body, ctx), side_eff = Future.join body in - let body, ctx, _ = match trust with - | Pure -> body, ctx, [] - | SideEffects _ -> inline_side_effects env body ctx side_eff + let body, ctx = match trust with + | Pure -> body, ctx + | SideEffects handle -> + let body, ctx, _ = handle env body ctx side_eff in + body, ctx in let env, usubst, univs = match c.const_entry_universes with | Monomorphic_const_entry univs -> @@ -431,101 +285,6 @@ let translate_constant mb env kn ce = build_constant_declaration kn env (infer_declaration ~trust:mb env ce) -let constant_entry_of_side_effect cb u = - let univs = - match cb.const_universes with - | Monomorphic_const uctx -> - Monomorphic_const_entry uctx - | Polymorphic_const auctx -> - Polymorphic_const_entry (Univ.AUContext.repr auctx) - in - let pt = - match cb.const_body, u with - | OpaqueDef _, `Opaque (b, c) -> b, c - | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty - | _ -> assert false in - DefinitionEntry { - const_entry_body = Future.from_val (pt, ()); - const_entry_secctx = None; - const_entry_feedback = None; - const_entry_type = Some cb.const_type; - const_entry_universes = univs; - const_entry_opaque = Declareops.is_opaque cb; - const_entry_inline_code = cb.const_inline_code } -;; - -let turn_direct orig = - let cb = orig.seff_body in - if Declareops.is_opaque cb then - let p = match orig.seff_env with - | `Opaque (b, c) -> (b, c) - | _ -> assert false - in - let const_body = OpaqueDef (Opaqueproof.create (Future.from_val p)) in - let cb = { cb with const_body } in - { orig with seff_body = cb } - else orig - -type exported_side_effect = - Constant.t * constant_body * side_effect_role - -let export_eff eff = - (eff.seff_constant, eff.seff_body, eff.seff_role) - -let export_side_effects mb env c = - let { const_entry_body = body; _ } = c in - let _, eff = Future.force body in - let ce = { c with - const_entry_body = Future.chain body - (fun (b_ctx, _) -> b_ctx, ()) } in - let not_exists e = - try ignore(Environ.lookup_constant e.seff_constant env); false - with Not_found -> true in - let aux (acc,sl) { eff = se; from_env = mb } = - let cbl = List.filter not_exists se in - if List.is_empty cbl then acc, sl - else cbl :: acc, (mb,List.length cbl) :: sl in - let seff, signatures = List.fold_left aux ([],[]) (uniq_seff_rev eff) in - let trusted = check_signatures mb signatures in - let push_seff env eff = - let { seff_constant = kn; seff_body = cb ; _ } = eff in - let env = Environ.add_constant kn cb env in - match cb.const_universes with - | Polymorphic_const _ -> env - | Monomorphic_const ctx -> - let ctx = match eff.seff_env with - | `Nothing -> ctx - | `Opaque(_, ctx') -> Univ.ContextSet.union ctx' ctx - in - Environ.push_context_set ~strict:true ctx env - in - let rec translate_seff sl seff acc env = - match seff with - | [] -> List.rev acc, ce - | cbs :: rest -> - if Int.equal sl 0 then - let env, cbs = - List.fold_left (fun (env,cbs) eff -> - let { seff_constant = kn; seff_body = ocb; seff_env = u ; _ } = eff in - let ce = constant_entry_of_side_effect ocb u in - let cb = translate_constant Pure env kn ce in - let eff = { eff with - seff_body = cb; - seff_env = `Nothing; - } in - (push_seff env eff, export_eff eff :: cbs)) - (env,[]) cbs in - translate_seff 0 rest (cbs @ acc) env - else - let cbs_len = List.length cbs in - let cbs = List.map turn_direct cbs in - let env = List.fold_left push_seff env cbs in - let ecbs = List.map export_eff cbs in - translate_seff (sl - cbs_len) rest (ecbs @ acc) env - in - translate_seff trusted seff [] env -;; - let translate_local_assum env t = let j = infer env t in let t = Typeops.assumption_of_judgment env j in @@ -578,13 +337,3 @@ let translate_local_def env _id centry = (* Insertion of inductive types. *) let translate_mind env kn mie = Indtypes.check_inductive env kn mie - -let inline_entry_side_effects env ce = { ce with - const_entry_body = Future.chain - ce.const_entry_body (fun ((body, ctx), side_eff) -> - let body, ctx',_ = inline_side_effects env body ctx side_eff in - (body, ctx'), ()); -} - -let inline_side_effects env body side_eff = - pi1 (inline_side_effects env body Univ.ContextSet.empty side_eff) diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index ab25090b00..3dc498ca1c 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -14,53 +14,27 @@ open Environ open Declarations open Entries -type side_effects +(** Handlers are used to manage side-effects. The ['a] type stands for the type + of side-effects, and it is parametric because they are only defined later + on. Handlers inline the provided side-effects into the term, and return + the set of additional global constraints that need to be added for the term + to be well typed. *) +type 'a effect_handler = + env -> Constr.t -> Univ.ContextSet.t -> 'a -> (Constr.t * Univ.ContextSet.t * int) type _ trust = | Pure : unit trust -| SideEffects : structure_body -> side_effects trust +| SideEffects : 'a effect_handler -> 'a trust val translate_local_def : env -> Id.t -> section_def_entry -> constr * types val translate_local_assum : env -> types -> types -val mk_pure_proof : constr -> side_effects proof_output - -val inline_side_effects : env -> constr -> side_effects -> constr -(** Returns the term where side effects have been turned into let-ins or beta - redexes. *) - -val inline_entry_side_effects : - env -> side_effects definition_entry -> unit definition_entry -(** Same as {!inline_side_effects} but applied to entries. Only modifies the - {!Entries.const_entry_body} field. It is meant to get a term out of a not - yet type checked proof. *) - -val empty_seff : side_effects -val add_seff : Declarations.structure_body -> Entries.side_eff list -> side_effects -> side_effects -val concat_seff : side_effects -> side_effects -> side_effects -(** [concat_seff e1 e2] adds the side-effects of [e1] to [e2], i.e. effects in - [e1] must be more recent than those of [e2]. *) -val uniq_seff : side_effects -> side_eff list -(** Return the list of individual side-effects in the order of their - creation. *) - val translate_constant : 'a trust -> env -> Constant.t -> 'a constant_entry -> constant_body -type exported_side_effect = - Constant.t * constant_body * side_effect_role - -(* Given a constant entry containing side effects it exports them (either - * by re-checking them or trusting them). Returns the constant bodies to - * be pushed in the safe_env by safe typing. The main constant entry - * needs to be translated as usual after this step. *) -val export_side_effects : - structure_body -> env -> side_effects definition_entry -> - exported_side_effect list * unit definition_entry - val translate_mind : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body |