aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cClosure.ml2
-rw-r--r--kernel/cClosure.mli4
-rw-r--r--kernel/environ.ml2
-rw-r--r--kernel/nativelib.ml2
-rw-r--r--kernel/nativevalues.ml4
-rw-r--r--kernel/safe_typing.ml169
-rw-r--r--kernel/safe_typing.mli2
-rw-r--r--kernel/section.ml2
-rw-r--r--kernel/section.mli3
-rw-r--r--kernel/sorts.ml2
-rw-r--r--kernel/sorts.mli2
11 files changed, 114 insertions, 80 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 1316dfe069..c31cdae6f5 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -678,6 +678,8 @@ let rec zip m stk =
let fapp_stack (m,stk) = zip m stk
+let term_of_process c stk = term_of_fconstr (zip c stk)
+
(*********************************************************************)
(* The assertions in the functions below are granted because they are
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 9e94248113..79092813bc 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -227,6 +227,10 @@ val kni: clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack
val knr: clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack
val kl : clos_infos -> clos_tab -> fconstr -> constr
+val zip : fconstr -> stack -> fconstr
+
+val term_of_process : fconstr -> stack -> constr
+
val to_constr : lift -> fconstr -> constr
(** End of cbn debug section i*)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 2d2c9a454b..de8692ff21 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -128,7 +128,7 @@ let empty_env = {
env_nb_rel = 0;
env_stratification = {
env_universes = UGraph.initial_universes;
- env_sprop_allowed = false;
+ env_sprop_allowed = true;
env_universes_lbound = Univ.Level.set;
env_engagement = PredicativeSet };
env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index dde1274152..494282d4e1 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -37,7 +37,7 @@ let ( / ) = Filename.concat
let my_temp_dir = lazy (CUnix.mktemp_dir "Coq_native" "")
let () = at_exit (fun () ->
- if Lazy.is_val my_temp_dir then
+ if not !Flags.debug && Lazy.is_val my_temp_dir then
try
let d = Lazy.force my_temp_dir in
Array.iter (fun f -> Sys.remove (Filename.concat d f)) (Sys.readdir d);
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 6cfe44c5ff..a5fcfae1fc 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 [@ocaml.alert "--deprecated"] in
+ let () = Obj.set_tag ans accumulate_tag [@ocaml.warning "-3"] 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 [@ocaml.alert "--deprecated"] in
+ let () = Obj.set_tag ans accumulate_tag [@ocaml.warning "-3"] in
(Obj.obj ans : t)
let get_accu (k : accumulator) =
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 181ec4860c..58b516dfdd 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -113,11 +113,22 @@ type library_info = DirPath.t * vodigest
(** Functor and funsig parameters, most recent first *)
type module_parameters = (MBId.t * module_type_body) list
+type compiled_library = {
+ comp_name : DirPath.t;
+ comp_mod : module_body;
+ comp_deps : library_info array;
+ comp_enga : engagement;
+ comp_natsymbs : Nativevalues.symbols
+}
+
+type reimport = compiled_library * Univ.ContextSet.t * vodigest
+
(** 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;
+ rev_reimport : reimport list;
}
type safe_environment =
@@ -301,6 +312,7 @@ sig
type t
val repr : t -> side_effect list
val empty : t
+ val is_empty : t -> bool
val add : side_effect -> t -> t
val concat : t -> t -> t
end =
@@ -319,6 +331,7 @@ type t = { seff : side_effect list; elts : SeffSet.t }
let repr eff = eff.seff
let empty = { seff = []; elts = SeffSet.empty }
+let is_empty { seff; elts } = List.is_empty seff && SeffSet.is_empty elts
let add x es =
if SeffSet.mem x es.elts then es
else { seff = x :: es.seff; elts = SeffSet.add x es.elts }
@@ -349,6 +362,7 @@ let push_private_constants env eff =
List.fold_left add_if_undefined env eff
let empty_private_constants = SideEffects.empty
+let is_empty_private_constants c = SideEffects.is_empty c
let concat_private = SideEffects.concat
let universes_of_private eff =
@@ -1002,74 +1016,6 @@ 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=Some sections }
-
-let close_section senv =
- let open Section in
- let sections0 = get_section 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 = push_context_set ~strict:true 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 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 senv (kn, cb)
- | `Inductive (ind, mib) ->
- let info = cooking_info (Section.segment_of_inductive env0 ind sections0) in
- let mib = Cooking.cook_inductive info mib in
- add_checked_mind ind mib senv
- in
- List.fold_left fold senv redo
-
(** {6 Starting / ending interactive modules and module types } *)
let start_module l senv =
@@ -1275,14 +1221,6 @@ let add_include me is_module inl senv =
(** {6 Libraries, i.e. compiled modules } *)
-type compiled_library = {
- comp_name : DirPath.t;
- comp_mod : module_body;
- comp_deps : library_info array;
- comp_enga : engagement;
- comp_natsymbs : Nativevalues.symbols
-}
-
let module_of_library lib = lib.comp_mod
type native_library = Nativecode.global list
@@ -1351,14 +1289,93 @@ let import lib cst vodigest senv =
Modops.add_linked_module mb linkinfo env
in
let env = Environ.add_native_symbols lib.comp_name lib.comp_natsymbs env in
+ let sections =
+ Option.map (Section.map_custom (fun custom ->
+ {custom with rev_reimport = (lib,cst,vodigest) :: custom.rev_reimport}))
+ senv.sections
+ in
mp,
{ senv with
env;
modresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.modresolver;
required = DPmap.add lib.comp_name vodigest senv.required;
loads = (mp,mb)::senv.loads;
+ sections;
}
+(** {6 Interactive sections *)
+
+let open_section senv =
+ let custom = {
+ rev_env = senv.env;
+ rev_univ = senv.univ;
+ rev_objlabels = senv.objlabels;
+ rev_reimport = [];
+ } in
+ let sections = Section.open_section ~custom senv.sections in
+ { senv with sections=Some sections }
+
+let close_section senv =
+ let open Section in
+ let sections0 = get_section 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; rev_reimport } = 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 Requires *)
+ let senv = List.fold_left (fun senv (lib,cst,vodigest) -> snd (import lib cst vodigest senv))
+ senv (List.rev rev_reimport)
+ in
+ (* Third phase: replay the discharged section contents *)
+ let senv = push_context_set ~strict:true 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 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 senv (kn, cb)
+ | `Inductive (ind, mib) ->
+ let info = cooking_info (Section.segment_of_inductive env0 ind sections0) in
+ let mib = Cooking.cook_inductive info mib in
+ add_checked_mind ind mib senv
+ in
+ List.fold_left fold senv redo
+
(** {6 Safe typing } *)
type judgment = Environ.unsafe_judgment
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index f8d5d319a9..b42746a882 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -50,6 +50,8 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment
type private_constants
val empty_private_constants : private_constants
+val is_empty_private_constants : private_constants -> bool
+
val concat_private : private_constants -> private_constants -> private_constants
(** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in
[e1] must be more recent than those of [e2]. *)
diff --git a/kernel/section.ml b/kernel/section.ml
index 948a967f96..8c36f16799 100644
--- a/kernel/section.ml
+++ b/kernel/section.ml
@@ -45,6 +45,8 @@ let has_poly_univs sec = sec.has_poly_univs
let all_poly_univs sec = sec.all_poly_univs
+let map_custom f sec = {sec with sec_custom = f sec.sec_custom}
+
let find_emap e (cmap, imap) = match e with
| SecDefinition con -> Cmap.find con cmap
| SecInductive ind -> Mindmap.find ind imap
diff --git a/kernel/section.mli b/kernel/section.mli
index 89739c7da2..2ebb4564b3 100644
--- a/kernel/section.mli
+++ b/kernel/section.mli
@@ -19,6 +19,9 @@ type 'a t
val depth : 'a t -> int
(** Number of nested sections. *)
+val map_custom : ('a -> 'a) -> 'a t -> 'a t
+(** Modify the custom data *)
+
(** {6 Manipulating sections} *)
type section_entry =
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index 466fbacca4..3a89b73bd5 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -12,6 +12,8 @@ open Univ
type family = InSProp | InProp | InSet | InType
+let all_families = [InSProp; InProp; InSet; InType]
+
type t =
| SProp
| Prop
diff --git a/kernel/sorts.mli b/kernel/sorts.mli
index 49549e224d..fe939b1d95 100644
--- a/kernel/sorts.mli
+++ b/kernel/sorts.mli
@@ -12,6 +12,8 @@
type family = InSProp | InProp | InSet | InType
+val all_families : family list
+
type t = private
| SProp
| Prop
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 14:09:29 +0000