aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/declarations.mli6
-rw-r--r--kernel/declareops.ml18
-rw-r--r--kernel/declareops.mli12
-rw-r--r--kernel/entries.mli25
-rw-r--r--kernel/opaqueproof.ml5
-rw-r--r--kernel/safe_typing.ml103
-rw-r--r--kernel/safe_typing.mli41
-rw-r--r--kernel/term_typing.ml188
-rw-r--r--kernel/term_typing.mli33
9 files changed, 341 insertions, 90 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 7def963e73..dc5c17a75b 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -79,12 +79,6 @@ type constant_body = {
const_proj : projection_body option;
const_inline_code : bool }
-type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ]
-
-type side_effect =
- | SEsubproof of constant * constant_body * seff_env
- | SEscheme of (inductive * constant * constant_body * seff_env) list * string
-
(** {6 Representation of mutual inductive types in the kernel } *)
type recarg =
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index a7051d5c13..248504c1b1 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -304,17 +304,7 @@ let hcons_mind mib =
(** {6 Stm machinery } *)
-let string_of_side_effect = function
- | SEsubproof (c,_,_) -> Names.string_of_con c
- | SEscheme (cl,_) ->
- String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl)
-type side_effects = side_effect list
-let no_seff = ([] : side_effects)
-let iter_side_effects f l = List.iter f (List.rev l)
-let fold_side_effects f a l = List.fold_left f a l
-let uniquize_side_effects l = List.rev (CList.uniquize (List.rev l))
-let union_side_effects l1 l2 = l1 @ l2
-let flatten_side_effects l = List.flatten l
-let side_effects_of_list l = l
-let cons_side_effects x l = x :: l
-let side_effects_is_empty = List.is_empty
+let string_of_side_effect { Entries.eff } = match eff with
+ | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.string_of_con c ^ ")"
+ | Entries.SEscheme (cl,_) ->
+ "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl) ^ ")"
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index ce65af975e..1b87009589 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -9,6 +9,7 @@
open Declarations
open Mod_subst
open Univ
+open Entries
(** Operations concerning types in [Declarations] :
[constant_body], [mutual_inductive_body], [module_body] ... *)
@@ -49,17 +50,6 @@ val is_opaque : constant_body -> bool
val string_of_side_effect : side_effect -> string
-type side_effects
-val no_seff : side_effects
-val iter_side_effects : (side_effect -> unit) -> side_effects -> unit
-val fold_side_effects : ('a -> side_effect -> 'a) -> 'a -> side_effects -> 'a
-val uniquize_side_effects : side_effects -> side_effects
-val union_side_effects : side_effects -> side_effects -> side_effects
-val flatten_side_effects : side_effects list -> side_effects
-val side_effects_of_list : side_effect list -> side_effects
-val cons_side_effects : side_effect -> side_effects -> side_effects
-val side_effects_is_empty : side_effects -> bool
-
(** {6 Inductive types} *)
val eq_recarg : recarg -> recarg -> bool
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 303d27d355..e058519e96 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -54,11 +54,11 @@ type mutual_inductive_entry = {
mind_entry_private : bool option }
(** {6 Constants (Definition/Axiom) } *)
-type proof_output = constr Univ.in_universe_context_set * Declareops.side_effects
-type const_entry_body = proof_output Future.computation
+type 'a proof_output = constr Univ.in_universe_context_set * 'a
+type 'a const_entry_body = 'a proof_output Future.computation
-type definition_entry = {
- const_entry_body : const_entry_body;
+type 'a definition_entry = {
+ const_entry_body : 'a const_entry_body;
(* List of section variables *)
const_entry_secctx : Context.section_context option;
(* State id on which the completion of type checking is reported *)
@@ -78,8 +78,8 @@ type projection_entry = {
proj_entry_ind : mutual_inductive;
proj_entry_arg : int }
-type constant_entry =
- | DefinitionEntry of definition_entry
+type 'a constant_entry =
+ | DefinitionEntry of 'a definition_entry
| ParameterEntry of parameter_entry
| ProjectionEntry of projection_entry
@@ -96,3 +96,16 @@ type module_entry =
| MType of module_params_entry * module_struct_entry
| MExpr of
module_params_entry * module_struct_entry * module_struct_entry option
+
+type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ]
+
+type side_eff =
+ | SEsubproof of constant * Declarations.constant_body * seff_env
+ | SEscheme of (inductive * constant * Declarations.constant_body * seff_env) list * string
+
+type side_effect = {
+ from_env : Declarations.structure_body Ephemeron.key;
+ eff : side_eff;
+}
+
+type side_effects = side_effect list
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 9f4361f401..badb15b561 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -43,7 +43,10 @@ let set_indirect_univ_accessor f = (get_univ := f)
let create cu = Direct ([],cu)
let turn_indirect dp o (prfs,odp) = match o with
- | Indirect _ -> Errors.anomaly (Pp.str "Already an indirect opaque")
+ | Indirect (_,_,i) ->
+ if not (Int.Map.mem i prfs)
+ then Errors.anomaly (Pp.str "Indirect in a different table")
+ else Errors.anomaly (Pp.str "Already an indirect opaque")
| Direct (d,cu) ->
let cu = Future.chain ~pure:true cu (fun (c, u) -> hcons_constr c, u) in
let id = Int.Map.cardinal prfs in
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ec245b0648..b71cd31b5c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -207,15 +207,55 @@ let get_opaque_body env cbo =
(Opaqueproof.force_proof (Environ.opaque_tables env) opaque,
Opaqueproof.force_constraints (Environ.opaque_tables env) opaque)
-let sideff_of_con env c =
+type private_constant = Entries.side_effect
+type private_constants = private_constant list
+
+type private_constant_role = Term_typing.side_effect_role =
+ | Subproof
+ | Schema of inductive * string
+
+let empty_private_constants = []
+let add_private x xs = x :: xs
+let concat_private xs ys = xs @ ys
+let mk_pure_proof = Term_typing.mk_pure_proof
+let inline_private_constants_in_constr = Term_typing.handle_side_effects
+let inline_private_constants_in_definition_entry = Term_typing.handle_entry_side_effects
+let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x)
+
+let constant_entry_of_private_constant = function
+ | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } ->
+ [ kn, Term_typing.constant_entry_of_side_effect cb eff_env ]
+ | { Entries.eff = Entries.SEscheme (l,_) } ->
+ List.map (fun (_,kn,cb,eff_env) ->
+ kn, Term_typing.constant_entry_of_side_effect cb eff_env) l
+
+let private_con_of_con env c =
let cbo = Environ.lookup_constant c env.env in
- SEsubproof (c, cbo, get_opaque_body env.env cbo)
-let sideff_of_scheme kind env cl =
- SEscheme(
- List.map (fun (i,c) ->
- let cbo = Environ.lookup_constant c env.env in
- i, c, cbo, get_opaque_body env.env cbo) cl,
- kind)
+ { Entries.from_env = Ephemeron.create env.revstruct;
+ Entries.eff = Entries.SEsubproof (c,cbo,get_opaque_body env.env cbo) }
+
+let private_con_of_scheme ~kind env cl =
+ { Entries.from_env = Ephemeron.create env.revstruct;
+ Entries.eff = Entries.SEscheme(
+ List.map (fun (i,c) ->
+ let cbo = Environ.lookup_constant c env.env in
+ i, c, cbo, get_opaque_body env.env cbo) cl,
+ kind) }
+
+let universes_of_private eff =
+ let open Declarations in
+ List.fold_left (fun acc { Entries.eff } ->
+ match eff with
+ | Entries.SEscheme (l,s) ->
+ List.fold_left (fun acc (_,_,cb,c) ->
+ let acc = match c with
+ | `Nothing -> acc
+ | `Opaque (_, ctx) -> ctx :: acc in
+ if cb.const_polymorphic then acc
+ else (Univ.ContextSet.of_context cb.const_universes) :: acc)
+ acc l
+ | Entries.SEsubproof _ -> acc)
+ [] eff
let env_of_safe_env senv = senv.env
let env_of_senv = env_of_safe_env
@@ -337,7 +377,7 @@ let safe_push_named (id,_,_ as d) env =
let push_named_def (id,de) senv =
- let c,typ,univs = Term_typing.translate_local_def senv.env id de in
+ let c,typ,univs = Term_typing.translate_local_def senv.revstruct senv.env id de in
let poly = de.Entries.const_entry_polymorphic in
let univs = Univ.ContextSet.of_context univs in
let c, univs = match c with
@@ -442,19 +482,16 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver }
(** Insertion of constants and parameters in environment *)
type global_declaration =
- | ConstantEntry of Entries.constant_entry
+ | ConstantEntry of bool * private_constants Entries.constant_entry
| GlobalRecipe of Cooking.recipe
-let add_constant dir l decl senv =
- let kn = make_con senv.modpath dir l in
- let cb = match decl with
- | ConstantEntry ce -> Term_typing.translate_constant senv.env kn ce
- | GlobalRecipe r ->
- let cb = Term_typing.translate_recipe senv.env kn r in
- if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb
- in
+type exported_private_constant =
+ constant * private_constants Entries.constant_entry * private_constant_role
+
+let add_constant_aux no_section senv (kn, cb) =
+ let l = pi3 (Constant.repr3 kn) in
let cb, otab = match cb.const_body with
- | OpaqueDef lc when DirPath.is_empty dir ->
+ | OpaqueDef lc when no_section ->
(* In coqc, opaque constants outside sections will be stored
indirectly in a specific table *)
let od, otab =
@@ -471,7 +508,33 @@ let add_constant dir l decl senv =
(Mod_subst.add_inline_delta_resolver (user_con kn) (lev,None)) senv'
| _ -> senv'
in
- kn, senv''
+ senv''
+
+let add_constant dir l decl senv =
+ let kn = make_con senv.modpath dir l in
+ let no_section = DirPath.is_empty dir in
+ let seff_to_export, decl =
+ match decl with
+ | ConstantEntry (true, ce) ->
+ let exports, ce =
+ Term_typing.validate_side_effects_for_export
+ senv.revstruct senv.env ce in
+ exports, ConstantEntry (false, ce)
+ | _ -> [], decl
+ in
+ let senv =
+ List.fold_left (add_constant_aux no_section) senv
+ (List.map (fun (kn,cb,_,_) -> kn, cb) seff_to_export) in
+ let senv =
+ let cb =
+ match decl with
+ | ConstantEntry (export_seff,ce) ->
+ Term_typing.translate_constant senv.revstruct senv.env kn ce
+ | GlobalRecipe r ->
+ let cb = Term_typing.translate_recipe senv.env kn r in
+ if no_section then Declareops.hcons_const_body cb else cb in
+ add_constant_aux no_section senv (kn, cb) in
+ (kn, List.map (fun (kn,_,ce,r) -> kn, ce, r) seff_to_export), senv
(** Insertion of inductive types *)
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index eac08eb834..2214cf8bb8 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -39,10 +39,30 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment
(** {6 Stm machinery } *)
-val sideff_of_con : safe_environment -> constant -> Declarations.side_effect
-val sideff_of_scheme :
- string -> safe_environment -> (inductive * constant) list ->
- Declarations.side_effect
+type private_constant
+type private_constants
+
+type private_constant_role =
+ | Subproof
+ | Schema of inductive * string
+
+val side_effects_of_private_constants :
+ private_constants -> Entries.side_effects
+
+val empty_private_constants : private_constants
+val add_private : private_constant -> private_constants -> private_constants
+val concat_private : private_constants -> private_constants -> private_constants
+
+val private_con_of_con : safe_environment -> constant -> private_constant
+val private_con_of_scheme : kind:string -> safe_environment -> (inductive * constant) list -> private_constant
+
+val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output
+val inline_private_constants_in_constr :
+ Environ.env -> Constr.constr -> private_constants -> Constr.constr
+val inline_private_constants_in_definition_entry :
+ Environ.env -> private_constants Entries.definition_entry -> private_constants Entries.definition_entry
+
+val universes_of_private : private_constants -> Univ.universe_context_set list
val is_curmod_library : safe_environment -> bool
@@ -63,16 +83,23 @@ val push_named_assum :
(** Returns the full universe context necessary to typecheck the definition
(futures are forced) *)
val push_named_def :
- Id.t * Entries.definition_entry -> Univ.universe_context_set safe_transformer
+ Id.t * private_constants Entries.definition_entry -> Univ.universe_context_set safe_transformer
(** Insertion of global axioms or definitions *)
type global_declaration =
- | ConstantEntry of Entries.constant_entry
+ (* bool: export private constants *)
+ | ConstantEntry of bool * private_constants Entries.constant_entry
| GlobalRecipe of Cooking.recipe
+type exported_private_constant =
+ constant * private_constants Entries.constant_entry * private_constant_role
+
+(** returns the main constant plus a list of auxiliary constants (empty
+ unless one requires the side effects to be exported) *)
val add_constant :
- DirPath.t -> Label.t -> global_declaration -> constant safe_transformer
+ DirPath.t -> Label.t -> global_declaration ->
+ (constant * exported_private_constant list) safe_transformer
(** Adding an inductive type *)
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index cab99077f0..d75bd73fb6 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -43,10 +43,29 @@ let map_option_typ = function None -> `None | Some x -> `Some x
(* Insertion of constants and parameters in environment. *)
-let mk_pure_proof c = (c, Univ.ContextSet.empty), Declareops.no_seff
+let mk_pure_proof c = (c, Univ.ContextSet.empty), []
+
+let equal_eff e1 e2 =
+ let open Entries in
+ match e1, e2 with
+ | { eff = SEsubproof (c1,_,_) }, { eff = SEsubproof (c2,_,_) } ->
+ Names.Constant.equal c1 c2
+ | { eff = SEscheme (cl1,_) }, { eff = SEscheme (cl2,_) } ->
+ CList.for_all2eq
+ (fun (_,c1,_,_) (_,c2,_,_) -> Names.Constant.equal c1 c2)
+ cl1 cl2
+ | _ -> false
+
+let rec uniq_seff = function
+ | [] -> []
+ | x :: xs -> x :: uniq_seff (List.filter (fun y -> not (equal_eff x y)) xs)
+(* The list of side effects is in reverse order (most recent first).
+ * To keep the "tological" order between effects we have to uniqize from the
+ * tail *)
+let uniq_seff l = List.rev (uniq_seff (List.rev l))
let handle_side_effects env body ctx side_eff =
- let handle_sideff (t,ctx) se =
+ let handle_sideff (t,ctx,sl) { eff = se; from_env = mb } =
let cbl = match se with
| SEsubproof (c,cb,b) -> [c,cb,b]
| SEscheme (cl,_) -> List.map (fun (_,c,cb,b) -> c,cb,b) cl in
@@ -65,7 +84,7 @@ let handle_side_effects env body ctx side_eff =
let rec sub_body c u b i x = match kind_of_term x with
| Const (c',u') when eq_constant c c' ->
Vars.subst_instance_constr u' b
- | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub_body c u b i x) i x in
+ | _ -> map_constr_with_binders ((+) 1) (sub_body c u b) i x in
let fix_body (c,cb,b) (t,ctx) =
match cb.const_body, b with
| Def b, _ ->
@@ -87,17 +106,60 @@ let handle_side_effects env body ctx side_eff =
let t = sub c 1 (Vars.lift 1 t) in
mkApp (mkLambda (cname c, b_ty, t), [|b|]),
Univ.ContextSet.union ctx
- (Univ.ContextSet.of_context cb.const_universes)
+ (Univ.ContextSet.of_context cb.const_universes)
else
let univs = cb.const_universes in
sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t), ctx
| _ -> assert false
in
- List.fold_right fix_body cbl (t,ctx)
+ let t, ctx = List.fold_right fix_body cbl (t,ctx) in
+ t, ctx, (mb,List.length cbl) :: sl
in
(* CAVEAT: we assure a proper order *)
- Declareops.fold_side_effects handle_sideff (body,ctx)
- (Declareops.uniquize_side_effects side_eff)
+ List.fold_left handle_sideff (body,ctx,[]) (uniq_seff side_eff)
+
+let check_signatures curmb sl =
+ let is_direct_ancestor (sl, curmb) (mb, how_many) =
+ match curmb with
+ | None -> None, None
+ | Some curmb ->
+ try
+ let mb = Ephemeron.get mb in
+ match sl with
+ | None -> sl, None
+ | Some n ->
+ if List.length mb >= how_many && CList.skipn how_many mb == curmb
+ then Some (n + how_many), Some mb
+ else None, None
+ with Ephemeron.InvalidKey -> None, None in
+ let sl, _ = List.fold_left is_direct_ancestor (Some 0,Some curmb) sl in
+ sl
+
+let trust_seff sl b e =
+ let rec aux sl b e acc =
+ match sl, kind_of_term b with
+ | (None|Some 0), _ -> b, e, acc
+ | Some sl, LetIn (n,c,ty,bo) ->
+ aux (Some (sl-1)) bo
+ (Environ.push_rel (n,Some c,ty) e) (`Let(n,c,ty)::acc)
+ | Some sl, App(hd,arg) ->
+ begin match kind_of_term hd with
+ | Lambda (n,ty,bo) ->
+ aux (Some (sl-1)) bo
+ (Environ.push_rel (n,None,ty) e) (`Cut(n,ty,arg)::acc)
+ | _ -> assert false
+ end
+ | _ -> assert false
+ in
+ aux sl b e []
+
+let rec unzip ctx j =
+ match ctx with
+ | [] -> j
+ | `Let (n,c,ty) :: ctx ->
+ unzip ctx { j with uj_val = mkLetIn (n,c,ty,j.uj_val) }
+ | `Cut (n,ty,arg) :: ctx ->
+ unzip ctx { j with uj_val = mkApp (mkLambda (n,ty,j.uj_val),arg) }
let hcons_j j =
{ uj_val = hcons_constr j.uj_val; uj_type = hcons_constr j.uj_type}
@@ -105,7 +167,7 @@ let hcons_j j =
let feedback_completion_typecheck =
Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete)
-let infer_declaration env kn dcl =
+let infer_declaration ~trust env kn dcl =
match dcl with
| ParameterEntry (ctx,poly,(t,uctx),nl) ->
let env = push_context ~strict:(not poly) uctx env in
@@ -124,9 +186,14 @@ let infer_declaration env kn dcl =
let tyj = infer_type env typ in
let proofterm =
Future.chain ~greedy:true ~pure:true body (fun ((body, ctx),side_eff) ->
- let body,ctx = handle_side_effects env body ctx side_eff in
+ let body, ctx, signatures =
+ handle_side_effects env body ctx side_eff in
+ let trusted_signatures = check_signatures trust signatures in
let env' = push_context_set ctx env in
- let j = infer env' body in
+ let j =
+ let body, env', zip_ctx = trust_seff trusted_signatures body env' in
+ let j = infer env' body in
+ unzip zip_ctx j in
let j = hcons_j j in
let subst = Univ.LMap.empty in
let _typ = constrain_type env' j c.const_entry_polymorphic subst
@@ -143,7 +210,7 @@ let infer_declaration env kn dcl =
let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
let (body, ctx), side_eff = Future.join body in
let univsctx = Univ.ContextSet.of_context c.const_entry_universes in
- let body, ctx = handle_side_effects env body
+ let body, ctx, _ = handle_side_effects env body
(Univ.ContextSet.union univsctx ctx) side_eff in
let env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in
let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in
@@ -294,8 +361,93 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
(*s Global and local constant declaration. *)
-let translate_constant env kn ce =
- build_constant_declaration kn env (infer_declaration env (Some kn) ce)
+let translate_constant mb env kn ce =
+ build_constant_declaration kn env
+ (infer_declaration ~trust:mb env (Some kn) ce)
+
+let constant_entry_of_side_effect cb u =
+ 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 =
+ (match cb.const_type with RegularArity t -> Some t | _ -> None);
+ const_entry_polymorphic = cb.const_polymorphic;
+ const_entry_universes = cb.const_universes;
+ const_entry_opaque = Declareops.is_opaque cb;
+ const_entry_inline_code = cb.const_inline_code }
+;;
+
+let turn_direct (kn,cb,u,r as orig) =
+ match cb.const_body, u with
+ | OpaqueDef _, `Opaque (b,c) ->
+ let pt = Future.from_val (b,c) in
+ kn, { cb with const_body = OpaqueDef (Opaqueproof.create pt) }, u, r
+ | _ -> orig
+;;
+
+type side_effect_role =
+ | Subproof
+ | Schema of inductive * string
+
+type exported_side_effect =
+ constant * constant_body * side_effects Entries.constant_entry * side_effect_role
+
+let validate_side_effects_for_export mb env ce =
+ match ce with
+ | ParameterEntry _ | ProjectionEntry _ -> [], ce
+ | DefinitionEntry c ->
+ let { const_entry_body = body } = c in
+ let _, eff = Future.force body in
+ let ce = DefinitionEntry { c with
+ const_entry_body = Future.chain ~greedy:true ~pure:true body
+ (fun (b_ctx, _) -> b_ctx, []) } in
+ let not_exists (c,_,_,_) =
+ try ignore(Environ.lookup_constant c env); false
+ with Not_found -> true in
+ let aux (acc,sl) { eff = se; from_env = mb } =
+ let cbl = match se with
+ | SEsubproof (c,cb,b) -> [c,cb,b,Subproof]
+ | SEscheme (cl,k) ->
+ List.map (fun (i,c,cb,b) -> c,cb,b,Schema(i,k)) cl in
+ let cbl = List.filter not_exists cbl in
+ if cbl = [] then acc, sl
+ else cbl :: acc, (mb,List.length cbl) :: sl in
+ let seff, signatures = List.fold_left aux ([],[]) (uniq_seff eff) in
+ let trusted = check_signatures mb signatures in
+ let push_seff env = function
+ | kn, cb, `Nothing, _ ->
+ Environ.add_constant kn cb env
+ | kn, cb, `Opaque(_, ctx), _ ->
+ let env = Environ.add_constant kn cb env in
+ Environ.push_context_set
+ ~strict:(not cb.const_polymorphic) ctx env in
+ let rec translate_seff sl seff acc env =
+ match sl, seff with
+ | _, [] -> List.rev acc, ce
+ | (None | Some 0), cbs :: rest ->
+ let env, cbs =
+ List.fold_left (fun (env,cbs) (kn, ocb, u, r) ->
+ let ce = constant_entry_of_side_effect ocb u in
+ let cb = translate_constant mb env kn ce in
+ (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,ce,r) :: cbs))
+ (env,[]) cbs in
+ translate_seff sl rest (cbs @ acc) env
+ | Some sl, cbs :: rest ->
+ 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 (fun (kn,cb,u,r) ->
+ kn, cb, constant_entry_of_side_effect cb u, r) cbs in
+ translate_seff (Some (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
@@ -305,9 +457,9 @@ let translate_local_assum env t =
let translate_recipe env kn r =
build_constant_declaration kn env (Cooking.cook_constant env r)
-let translate_local_def env id centry =
+let translate_local_def mb env id centry =
let def,typ,proj,poly,univs,inline_code,ctx =
- infer_declaration env None (DefinitionEntry centry) in
+ infer_declaration ~trust:mb env None (DefinitionEntry centry) in
let typ = type_of_constant_type env typ in
if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin
match def with
@@ -332,9 +484,9 @@ let translate_mind env kn mie = Indtypes.check_inductive env kn mie
let handle_entry_side_effects env ce = { ce with
const_entry_body = Future.chain ~greedy:true ~pure:true
ce.const_entry_body (fun ((body, ctx), side_eff) ->
- let body, ctx' = handle_side_effects env body ctx side_eff in
- (body, ctx'), Declareops.no_seff);
+ let body, ctx',_ = handle_side_effects env body ctx side_eff in
+ (body, ctx'), []);
}
let handle_side_effects env body side_eff =
- fst (handle_side_effects env body Univ.ContextSet.empty side_eff)
+ pi1 (handle_side_effects env body Univ.ContextSet.empty side_eff)
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 8d92bcc68f..509160ccc7 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -12,23 +12,42 @@ open Environ
open Declarations
open Entries
-val translate_local_def : env -> Id.t -> definition_entry ->
+val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry ->
constant_def * types * constant_universes
val translate_local_assum : env -> types -> types
-val mk_pure_proof : constr -> proof_output
+val mk_pure_proof : constr -> side_effects proof_output
-val handle_side_effects : env -> constr -> Declareops.side_effects -> constr
+val handle_side_effects : env -> constr -> side_effects -> constr
(** Returns the term where side effects have been turned into let-ins or beta
redexes. *)
-val handle_entry_side_effects : env -> definition_entry -> definition_entry
+val handle_entry_side_effects : env -> side_effects definition_entry -> side_effects definition_entry
(** Same as {!handle_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 translate_constant : env -> constant -> constant_entry -> constant_body
+val uniq_seff : side_effects -> side_effects
+
+val translate_constant : structure_body -> env -> constant -> side_effects constant_entry -> constant_body
+
+(* Checks weather the side effects in constant_entry can be trusted.
+ * Returns the list of effects to be exported.
+ * Note: It forces the Future.computation. *)
+type side_effect_role =
+ | Subproof
+ | Schema of inductive * string
+
+type exported_side_effect =
+ constant * constant_body * side_effects Entries.constant_entry * side_effect_role
+
+val validate_side_effects_for_export :
+ structure_body -> env -> side_effects constant_entry ->
+ exported_side_effect list * side_effects constant_entry
+
+val constant_entry_of_side_effect :
+ constant_body -> seff_env -> side_effects constant_entry
val translate_mind :
env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
@@ -37,8 +56,8 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body
(** Internal functions, mentioned here for debug purpose only *)
-val infer_declaration : env -> constant option ->
- constant_entry -> Cooking.result
+val infer_declaration : trust:structure_body -> env -> constant option ->
+ side_effects constant_entry -> Cooking.result
val build_constant_declaration :
constant -> env -> Cooking.result -> constant_body
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 08:56:12 +0000