aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/byterun/coq_memory.c2
-rw-r--r--kernel/cClosure.ml4
-rw-r--r--kernel/cClosure.mli2
-rw-r--r--kernel/cbytegen.ml2
-rw-r--r--kernel/constr.mli2
-rw-r--r--kernel/declarations.ml4
-rw-r--r--kernel/environ.ml10
-rw-r--r--kernel/environ.mli6
-rw-r--r--kernel/inductive.ml2
-rw-r--r--kernel/mod_typing.ml2
-rw-r--r--kernel/modops.ml2
-rw-r--r--kernel/opaqueproof.ml78
-rw-r--r--kernel/opaqueproof.mli37
-rw-r--r--kernel/safe_typing.ml31
-rw-r--r--kernel/uint63.mli2
-rw-r--r--kernel/univ.ml2
-rw-r--r--kernel/univ.mli2
-rw-r--r--kernel/vmvalues.ml2
18 files changed, 84 insertions, 108 deletions
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index 542a05fd25..a1c49bee95 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -105,7 +105,7 @@ value init_coq_vm(value unit) /* ML */
init_coq_interpreter();
/* Some predefined pointer code.
- * It is typically contained in accumlator blocks whose tag is 0 and thus
+ * It is typically contained in accumulator blocks whose tag is 0 and thus
* scanned by the GC, so make it look like an OCaml block. */
value accu_block = (value) coq_stat_alloc(2 * sizeof(value));
Hd_hp (accu_block) = Make_header (1, Abstract_tag, Caml_black); \
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 95f88c0306..fc7d1a54f2 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -226,7 +226,7 @@ let unfold_red kn =
* this constant or abstraction.
* * i_tab is the cache table of the results
*
- * ref_value_cache searchs in the tab, otherwise uses i_repr to
+ * ref_value_cache searches in the tab, otherwise uses i_repr to
* compute the result and store it in the table. If the constant can't
* be unfolded, returns None, but does not store this failure. * This
* doesn't take the RESET into account. You mustn't keep such a table
@@ -645,7 +645,7 @@ and subst_constr subst c = match [@ocaml.warning "-4"] Constr.kind c with
and comp_subs el s =
Esubst.lift_subst (fun el c -> lazy (to_constr el c)) el s
-(* This function defines the correspondance between constr and
+(* This function defines the correspondence between constr and
fconstr. When we find a closure whose substitution is the identity,
then we directly return the constr to avoid possibly huge
reallocation. *)
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 1a790eaed6..60185464c5 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -200,7 +200,7 @@ val whd_val : clos_infos -> clos_tab -> fconstr -> constr
val whd_stack :
clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack
-(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding
+(** [eta_expand_ind_stack env ind c s t] computes stacks corresponding
to the conversion of the eta expansion of t, considered as an inhabitant
of ind, and the Constructor c of this inductive type applied to arguments
s.
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 69f004307d..90fbcb8ae3 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -386,7 +386,7 @@ let rec is_tailcall = function
| Klabel _ :: c -> is_tailcall c
| _ -> None
-(* Extention of the continuation *)
+(* Extension of the continuation *)
(* Add a Kpop n instruction in front of a continuation *)
let rec add_pop n = function
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 7fc57cdb8a..aa5878c9d7 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -141,7 +141,7 @@ val mkRef : GlobRef.t Univ.puniverses -> constr
[mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac]
presented as describe in [ci].
- [p] stucture is [fun args x -> "return clause"]
+ [p] structure is [fun args x -> "return clause"]
[ac]{^ ith} element is ith constructor case presented as
{e lambda construct_args (without params). case_term } *)
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 36ee952099..860d19fe26 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -22,11 +22,11 @@ type engagement = set_predicativity
(** {6 Representation of constants (Definition/Axiom) } *)
(** Non-universe polymorphic mode polymorphism (Coq 8.2+): inductives
- and constants hiding inductives are implicitely polymorphic when
+ and constants hiding inductives are implicitly polymorphic when
applied to parameters, on the universes appearing in the whnf of
their parameters and their conclusion, in a template style.
- In truely universe polymorphic mode, we always use RegularArity.
+ In truly universe polymorphic mode, we always use RegularArity.
*)
type template_arity = {
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 05f342a82a..c47bde0864 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -483,16 +483,6 @@ let constant_value_and_type env (kn, u) =
in
b', subst_instance_constr u cb.const_type, cst
-let body_of_constant_body env cb =
- let otab = opaque_tables env in
- match cb.const_body with
- | Undef _ | Primitive _ ->
- None
- | Def c ->
- Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb)
- | OpaqueDef o ->
- Some (Opaqueproof.force_proof otab o, Declareops.constant_polymorphic_context cb)
-
(* These functions should be called under the invariant that [env]
already contains the constraints corresponding to the constant
application. *)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index f6cd41861e..2abcea148a 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -215,12 +215,6 @@ val constant_value_and_type : env -> Constant.t puniverses ->
polymorphic *)
val constant_context : env -> Constant.t -> Univ.AUContext.t
-(** Returns the body of the constant if it has any, and the polymorphic context
- it lives in. For monomorphic constant, the latter is empty, and for
- polymorphic constants, the term contains De Bruijn universe variables that
- need to be instantiated. *)
-val body_of_constant_body : env -> Opaqueproof.opaque constant_body -> (Constr.constr * Univ.AUContext.t) option
-
(* These functions should be called under the invariant that [env]
already contains the constraints corresponding to the constant
application. *)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index d9335d39b5..ca7086a3e4 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -166,7 +166,7 @@ let make_subst env =
(* template, it is identity substitution otherwise (ie. when u is *)
(* already in the domain of the substitution) [remember_subst] will *)
(* update its image [x] by [sup x u] in order not to forget the *)
- (* dependency in [u] that remains to be fullfilled. *)
+ (* dependency in [u] that remains to be fulfilled. *)
make (remember_subst u subst) (sign, exp, [])
| _sign, [], _ ->
(* Uniform parameters are exhausted *)
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 2de5faa6df..72393d0081 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -188,7 +188,7 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
in
let new_equiv = add_delta_resolver equiv new_mb.mod_delta in
(* we propagate the new equality in the rest of the signature
- with the identity substitution accompagned by the new resolver*)
+ with the identity substitution accompanied by the new resolver*)
let id_subst = map_mp mp' mp' new_mb.mod_delta in
let new_after = subst_structure id_subst after in
before@(lab,SFBmodule new_mb')::new_after, new_equiv, cst
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 4fdd7ab334..472fddb829 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -515,7 +515,7 @@ and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso =
"Module M:=P." or "Module M. Include P. End M."
We need to perform two operations to compute the body of M.
- The first one is applying the substitution {P <- M} on the type of P
- - The second one is strenghtening. *)
+ - The second one is strengthening. *)
let strengthen_and_subst_mb mb mp include_b = match mb.mod_type with
|NoFunctor struc ->
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 18c1bcc0f8..75f96da3eb 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -16,6 +16,11 @@ open Mod_subst
type work_list = (Instance.t * Id.t array) Cmap.t *
(Instance.t * Id.t array) Mindmap.t
+type indirect_accessor = {
+ access_proof : DirPath.t -> int -> constr option;
+ access_constraints : DirPath.t -> int -> Univ.ContextSet.t option;
+}
+
type cooking_info = {
modlist : work_list;
abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
@@ -36,20 +41,8 @@ let empty_opaquetab = {
opaque_dir = DirPath.initial;
}
-(* hooks *)
-let default_get_opaque dp _ =
- CErrors.user_err Pp.(pr_sequence str ["Cannot access opaque proofs in library"; DirPath.to_string dp])
-let default_get_univ dp _ =
- CErrors.user_err (Pp.pr_sequence Pp.str [
- "Cannot access universe constraints of opaque proofs in library ";
- DirPath.to_string dp])
-
-let get_opaque = ref default_get_opaque
-let get_univ = ref default_get_univ
-
-let set_indirect_opaque_accessor f = (get_opaque := f)
-let set_indirect_univ_accessor f = (get_univ := f)
-(* /hooks *)
+let not_here () =
+ CErrors.user_err Pp.(str "Cannot access opaque delayed proof")
let create cu = Direct ([],cu)
@@ -95,51 +88,52 @@ let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function
let fp = snd (Int.Map.find i prfs) in
join except fp
-let force_proof { opaque_val = prfs; opaque_dir = odp; _ } = function
+let force_proof access { opaque_val = prfs; opaque_dir = odp; _ } = function
| Direct (_,cu) ->
fst(Future.force cu)
| Indirect (l,dp,i) ->
let pt =
if DirPath.equal dp odp
then Future.chain (snd (Int.Map.find i prfs)) fst
- else !get_opaque dp i in
+ else match access.access_proof dp i with
+ | None -> not_here ()
+ | Some v -> Future.from_val v
+ in
let c = Future.force pt in
force_constr (List.fold_right subst_substituted l (from_val c))
-let force_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function
+let force_constraints access { opaque_val = prfs; opaque_dir = odp; _ } = function
| Direct (_,cu) -> snd(Future.force cu)
| Indirect (_,dp,i) ->
if DirPath.equal dp odp
then snd (Future.force (snd (Int.Map.find i prfs)))
- else match !get_univ dp i with
+ else match access.access_constraints dp i with
| None -> Univ.ContextSet.empty
- | Some u -> Future.force u
+ | Some u -> u
-let get_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function
- | Direct (_,cu) -> Some(Future.chain cu snd)
- | Indirect (_,dp,i) ->
- if DirPath.equal dp odp
- then Some(Future.chain (snd (Int.Map.find i prfs)) snd)
- else !get_univ dp i
+let get_direct_constraints = function
+| Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
+| Direct (_, cu) -> Future.chain cu snd
module FMap = Future.UUIDMap
-let a_constr = Future.from_val (mkRel 1)
-let a_univ = Future.from_val Univ.ContextSet.empty
-let a_discharge : cooking_info list = []
-
-let dump { opaque_val = otab; opaque_len = n; _ } =
- let opaque_table = Array.make n a_constr in
- let univ_table = Array.make n a_univ in
- let disch_table = Array.make n a_discharge in
+let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ } =
+ let opaque_table = Array.make n None in
+ let univ_table = Array.make n None in
+ let disch_table = Array.make n [] in
let f2t_map = ref FMap.empty in
- Int.Map.iter (fun n (d,cu) ->
- let c, u = Future.split2 cu in
- Future.sink u;
- Future.sink c;
- opaque_table.(n) <- c;
- univ_table.(n) <- u;
- disch_table.(n) <- d;
- f2t_map := FMap.add (Future.uuid cu) n !f2t_map)
- otab;
+ let iter n (d, cu) =
+ let uid = Future.uuid cu in
+ let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in
+ if Future.is_val cu then
+ let (c, u) = Future.force cu in
+ let () = univ_table.(n) <- Some u in
+ opaque_table.(n) <- Some c
+ else if Future.UUIDSet.mem uid except then
+ disch_table.(n) <- d
+ else
+ CErrors.anomaly
+ Pp.(str"Proof object "++int n++str" is not checked nor to be checked")
+ in
+ let () = Int.Map.iter iter otab in
opaque_table, univ_table, disch_table, !f2t_map
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 4e8956af06..4646206e55 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -35,12 +35,20 @@ val create : proofterm -> opaque
used so far *)
val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
+type indirect_accessor = {
+ access_proof : DirPath.t -> int -> constr option;
+ access_constraints : DirPath.t -> int -> Univ.ContextSet.t option;
+}
+(** When stored indirectly, 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.
+*)
+
(** From a [opaque] back to a [constr]. This might use the
- indirect opaque accessor configured below. *)
-val force_proof : opaquetab -> opaque -> constr
-val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t
-val get_constraints :
- opaquetab -> opaque -> Univ.ContextSet.t Future.computation option
+ indirect opaque accessor given as an argument. *)
+val force_proof : indirect_accessor -> opaquetab -> opaque -> constr
+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
@@ -60,21 +68,8 @@ val discharge_direct_opaque :
val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
-val dump : opaquetab ->
- Constr.t Future.computation array *
- Univ.ContextSet.t Future.computation array *
+val dump : ?except:Future.UUIDSet.t -> opaquetab ->
+ Constr.t option array *
+ Univ.ContextSet.t option array *
cooking_info list array *
int Future.UUIDMap.t
-
-(** When stored indirectly, opaque terms are indexed by their library
- dirpath and an integer index. The following two functions activate
- this indirect storage, by telling how to store and retrieve terms.
- Default creator always returns [None], preventing the creation of
- any indirect link, and default accessor always raises an error.
-*)
-
-val set_indirect_opaque_accessor :
- (DirPath.t -> int -> constr Future.computation) -> unit
-val set_indirect_univ_accessor :
- (DirPath.t -> int -> Univ.ContextSet.t Future.computation option) -> unit
-
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a5d8a480ee..873cc2a172 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -458,19 +458,11 @@ let labels_of_mib mib =
Array.iter visit_mip mib.mind_packets;
get ()
-let globalize_constant_universes env cb =
+let globalize_constant_universes cb =
match cb.const_universes with
| Monomorphic cstrs ->
- Now (false, cstrs) ::
- (match cb.const_body with
- | (Undef _ | Def _ | Primitive _) -> []
- | OpaqueDef lc ->
- match Opaqueproof.get_constraints (Environ.opaque_tables env) lc with
- | None -> []
- | Some fc ->
- match Future.peek_val fc with
- | None -> [Later fc]
- | Some c -> [Now (false, c)])
+ (* Constraints hidden in the opaque body are added by [add_constant_aux] *)
+ [Now (false, cstrs)]
| Polymorphic _ ->
[Now (true, Univ.ContextSet.empty)]
@@ -480,9 +472,9 @@ let globalize_mind_universes mb =
[Now (false, ctx)]
| Polymorphic _ -> [Now (true, Univ.ContextSet.empty)]
-let constraints_of_sfb env sfb =
+let constraints_of_sfb sfb =
match sfb with
- | SFBconst cb -> globalize_constant_universes env cb
+ | SFBconst cb -> globalize_constant_universes cb
| SFBmind mib -> globalize_mind_universes mib
| SFBmodtype mtb -> [Now (false, mtb.mod_constraints)]
| SFBmodule mb -> [Now (false, mb.mod_constraints)]
@@ -520,7 +512,8 @@ let add_field ?(is_include=false) ((l,sfb) as field) gn senv =
separately. *)
senv
else
- let cst = constraints_of_sfb senv.env sfb in
+ (* Delayed constraints from opaque body are added by [add_constant_aux] *)
+ let cst = constraints_of_sfb sfb in
add_constraints_list cst senv
in
let env' = match sfb, gn with
@@ -553,6 +546,15 @@ type exported_private_constant =
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 (false, c)]
+ end
+ | Undef _ | Def _ | Primitive _ | OpaqueDef _ -> []
+ in
let cb, otab = match cb.const_body with
| OpaqueDef lc when not in_section ->
(* In coqc, opaque constants outside sections will be stored
@@ -565,6 +567,7 @@ let add_constant_aux ~in_section senv (kn, cb) =
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
diff --git a/kernel/uint63.mli b/kernel/uint63.mli
index f25f24512d..93632da110 100644
--- a/kernel/uint63.mli
+++ b/kernel/uint63.mli
@@ -13,7 +13,7 @@ val of_uint : int -> t
val hash : t -> int
- (* convertion to a string *)
+ (* conversion to a string *)
val to_string : t -> string
val of_string : string -> t
diff --git a/kernel/univ.ml b/kernel/univ.ml
index b1bbc25fe6..2b88d6884d 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -726,7 +726,7 @@ let univ_level_rem u v min =
| Some u' -> if Level.equal u u' then min else v
| None -> List.filter (fun (l, n) -> not (Int.equal n 0 && Level.equal u l)) v
-(* Is u mentionned in v (or equals to v) ? *)
+(* Is u mentioned in v (or equals to v) ? *)
(**********************************************************************)
diff --git a/kernel/univ.mli b/kernel/univ.mli
index db178c4bb0..ddb204dd52 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -163,7 +163,7 @@ val super : Universe.t -> Universe.t
val universe_level : Universe.t -> Level.t option
-(** [univ_level_mem l u] Is l is mentionned in u ? *)
+(** [univ_level_mem l u] Is l is mentioned in u ? *)
val univ_level_mem : Level.t -> Universe.t -> bool
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 777a207013..5e3a3c3347 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -12,7 +12,7 @@ open Univ
open Constr
(*******************************************)
-(* Initalization of the abstract machine ***)
+(* Initialization of the abstract machine ***)
(* Necessary for [relaccu_tbl] *)
(*******************************************)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 04:01:05 +0000