aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/byterun/coq_interp.c21
-rw-r--r--kernel/entries.ml14
-rw-r--r--kernel/indtypes.ml17
-rw-r--r--kernel/indtypes.mli19
-rw-r--r--kernel/modops.ml6
-rw-r--r--kernel/names.ml3
-rw-r--r--kernel/names.mli3
-rw-r--r--kernel/opaqueproof.ml29
-rw-r--r--kernel/opaqueproof.mli4
-rw-r--r--kernel/safe_typing.ml119
-rw-r--r--kernel/safe_typing.mli12
11 files changed, 92 insertions, 155 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 1b348ae777..4b45608ae5 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -97,7 +97,8 @@ if (sp - num_args < coq_stack_threshold) { \
several architectures.
*/
-#if defined(__GNUC__) && !defined(DEBUG)
+#if defined(__GNUC__) && !defined(DEBUG) && !defined(__INTEL_COMPILER) \
+ && !defined(__llvm__)
#ifdef __mips__
#define PC_REG asm("$16")
#define SP_REG asm("$17")
@@ -126,7 +127,7 @@ if (sp - num_args < coq_stack_threshold) { \
#define SP_REG asm("%edi")
#define ACCU_REG
#endif
-#if defined(PPC) || defined(_POWER) || defined(_IBMR2)
+#if defined(__ppc__) || defined(__ppc64__)
#define PC_REG asm("26")
#define SP_REG asm("27")
#define ACCU_REG asm("28")
@@ -141,8 +142,9 @@ if (sp - num_args < coq_stack_threshold) { \
#define SP_REG asm("a4")
#define ACCU_REG asm("d7")
#endif
-#if defined(__arm__) && !defined(__thumb2__)
-#define PC_REG asm("r9")
+/* OCaml PR#4953: these specific registers not available in Thumb mode */
+#if defined(__arm__) && !defined(__thumb__)
+#define PC_REG asm("r6")
#define SP_REG asm("r8")
#define ACCU_REG asm("r7")
#endif
@@ -152,6 +154,17 @@ if (sp - num_args < coq_stack_threshold) { \
#define ACCU_REG asm("38")
#define JUMPTBL_BASE_REG asm("39")
#endif
+#ifdef __x86_64__
+#define PC_REG asm("%r15")
+#define SP_REG asm("%r14")
+#define ACCU_REG asm("%r13")
+#endif
+#ifdef __aarch64__
+#define PC_REG asm("%x19")
+#define SP_REG asm("%x20")
+#define ACCU_REG asm("%x21")
+#define JUMPTBL_BASE_REG asm("%x22")
+#endif
#endif
#define CheckInt1() do{ \
diff --git a/kernel/entries.ml b/kernel/entries.ml
index a3d32267a7..adb3f6bd29 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -108,21 +108,7 @@ type module_entry =
| MExpr of
module_params_entry * module_struct_entry * module_struct_entry option
-
-type seff_env =
- [ `Nothing
- (* The proof term and its universes.
- Same as the constant_body's but not in an ephemeron *)
- | `Opaque of Constr.t * Univ.ContextSet.t ]
-
(** Not used by the kernel. *)
type side_effect_role =
| Subproof
| Schema of inductive * string
-
-type side_eff = {
- seff_constant : Constant.t;
- seff_body : Declarations.constant_body;
- seff_env : seff_env;
- seff_role : side_effect_role;
-}
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 009eb3da38..bb3b0a538e 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -49,20 +49,6 @@ let weaker_noccur_between env x nvars t =
(************************************************************************)
(* Various well-formedness check for inductive declarations *)
-(* Errors related to inductive constructions *)
-type inductive_error = Type_errors.inductive_error =
- | NonPos of env * constr * constr
- | NotEnoughArgs of env * constr * constr
- | NotConstructor of env * Id.t * constr * constr * int * int
- | NonPar of env * constr * int * constr * constr
- | SameNamesTypes of Id.t
- | SameNamesConstructors of Id.t
- | SameNamesOverlap of Id.t list
- | NotAnArity of env * constr
- | BadEntry
- | LargeNonPropInductiveNotInType
- | BadUnivs
-
exception InductiveError = Type_errors.InductiveError
(************************************************************************)
@@ -84,6 +70,7 @@ exception IllFormedInd of ill_formed_ind
let mind_extract_params = decompose_prod_n_assum
let explain_ind_err id ntyp env nparamsctxt c err =
+ let open Type_errors in
let (_lparams,c') = mind_extract_params nparamsctxt c in
match err with
| LocalNonPos kt ->
@@ -329,7 +316,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
| Prod (na,b,d) ->
let () = assert (List.is_empty largs) in
if not recursive && not (noccur_between n ntypes b) then
- raise (InductiveError BadEntry);
+ raise (InductiveError Type_errors.BadEntry);
let nmr',recarg = check_pos ienv nmr b in
let ienv' = ienv_push_var ienv (na,b,mk_norec) in
check_constr_rec ienv' nmr' (recarg::lrec) d
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 7810c1723e..1b8e4208ff 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -9,28 +9,9 @@
(************************************************************************)
open Names
-open Constr
open Declarations
open Environ
open Entries
(** Check an inductive. *)
val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
-
-(** Deprecated *)
-type inductive_error =
- | NonPos of env * constr * constr
- | NotEnoughArgs of env * constr * constr
- | NotConstructor of env * Id.t * constr * constr * int * int
- | NonPar of env * constr * int * constr * constr
- | SameNamesTypes of Id.t
- | SameNamesConstructors of Id.t
- | SameNamesOverlap of Id.t list
- | NotAnArity of env * constr
- | BadEntry
- | LargeNonPropInductiveNotInType
- | BadUnivs
-[@@ocaml.deprecated "Use [Type_errors.inductive_error]"]
-
-exception InductiveError of Type_errors.inductive_error
-[@@ocaml.deprecated "Use [Type_errors.InductiveError]"]
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 4f992d3972..4fdd7ab334 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -608,11 +608,7 @@ let clean_bounded_mod_expr sign =
(** {6 Stm machinery } *)
let join_constant_body except otab cb =
match cb.const_body with
- | OpaqueDef o ->
- (match Opaqueproof.uuid_opaque otab o with
- | Some uuid when not(Future.UUIDSet.mem uuid except) ->
- Opaqueproof.join_opaque otab o
- | _ -> ())
+ | OpaqueDef o -> Opaqueproof.join_opaque ~except otab o
| _ -> ()
let join_structure except otab s =
diff --git a/kernel/names.ml b/kernel/names.ml
index 9f27212967..047a1d6525 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -376,9 +376,6 @@ module KerName = struct
{ modpath; knlabel; refhash = -1; }
let repr kn = (kn.modpath, kn.knlabel)
- let make2 = make
- [@@ocaml.deprecated "Please use [KerName.make]"]
-
let modpath kn = kn.modpath
let label kn = kn.knlabel
diff --git a/kernel/names.mli b/kernel/names.mli
index 61df3bad0e..2238e932b0 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -278,9 +278,6 @@ sig
val make : ModPath.t -> Label.t -> t
val repr : t -> ModPath.t * Label.t
- val make2 : ModPath.t -> Label.t -> t
- [@@ocaml.deprecated "Please use [KerName.make]"]
-
(** Projections *)
val modpath : t -> ModPath.t
val label : t -> Label.t
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 303cb06c55..57059300b8 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -87,19 +87,18 @@ let discharge_direct_opaque ~cook_constr ci = function
| Direct (d,cu) ->
Direct (ci::d,Future.chain cu (fun (c, u) -> cook_constr c, u))
-let join_opaque { opaque_val = prfs; opaque_dir = odp; _ } = function
- | Direct (_,cu) -> ignore(Future.join cu)
+let join except cu = match except with
+| None -> ignore (Future.join cu)
+| Some except ->
+ if Future.UUIDSet.mem (Future.uuid cu) except then ()
+ else ignore (Future.join cu)
+
+let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function
+ | Direct (_,cu) -> join except cu
| Indirect (_,dp,i) ->
if DirPath.equal dp odp then
let fp = snd (Int.Map.find i prfs) in
- ignore(Future.join fp)
-
-let uuid_opaque { opaque_val = prfs; opaque_dir = odp; _ } = function
- | Direct (_,cu) -> Some (Future.uuid cu)
- | Indirect (_,dp,i) ->
- if DirPath.equal dp odp
- then Some (Future.uuid (snd (Int.Map.find i prfs)))
- else None
+ join except fp
let force_proof { opaque_val = prfs; opaque_dir = odp; _ } = function
| Direct (_,cu) ->
@@ -128,16 +127,6 @@ let get_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function
then Some(Future.chain (snd (Int.Map.find i prfs)) snd)
else !get_univ dp i
-let get_proof { opaque_val = prfs; opaque_dir = odp; _ } = function
- | Direct (_,cu) -> Future.chain cu fst
- | 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
- Future.chain pt (fun c ->
- force_constr (List.fold_right subst_substituted l (from_val c)))
-
module FMap = Future.UUIDMap
let a_constr = Future.from_val (mkRel 1)
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 5ea6da649b..d47c0bbb3c 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -39,7 +39,6 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
indirect opaque accessor configured below. *)
val force_proof : opaquetab -> opaque -> constr
val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t
-val get_proof : opaquetab -> opaque -> constr Future.computation
val get_constraints :
opaquetab -> opaque -> Univ.ContextSet.t Future.computation option
@@ -60,8 +59,7 @@ type cooking_info = {
val discharge_direct_opaque :
cook_constr:(constr -> constr) -> cooking_info -> opaque -> opaque
-val uuid_opaque : opaquetab -> opaque -> Future.UUID.t option
-val join_opaque : opaquetab -> opaque -> unit
+val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
val dump : opaquetab ->
Constr.t Future.computation array *
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 673f025c75..75375812c0 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -228,6 +228,12 @@ let check_engagement env expected_impredicative_set =
(** {6 Stm machinery } *)
+type seff_env =
+ [ `Nothing
+ (* The proof term and its universes.
+ Same as the constant_body's but not in an ephemeron *)
+ | `Opaque of Constr.t * Univ.ContextSet.t ]
+
let get_opaque_body env cbo =
match cbo.const_body with
| Undef _ -> assert false
@@ -240,7 +246,10 @@ let get_opaque_body env cbo =
type side_effect = {
from_env : Declarations.structure_body CEphemeron.key;
- eff : Entries.side_eff list;
+ seff_constant : Constant.t;
+ seff_body : Declarations.constant_body;
+ seff_env : seff_env;
+ seff_role : Entries.side_effect_role;
}
module SideEffects :
@@ -254,11 +263,9 @@ 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
+ Constant.CanOrd.compare e1.seff_constant e2.seff_constant
end
module SeffSet = Set.Make(SeffOrd)
@@ -279,37 +286,37 @@ 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
+ List.rev (SideEffects.repr l)
+
+let push_private_constants env eff =
+ let eff = side_effects_of_private_constants eff in
+ let add_if_undefined env eff =
+ try ignore(Environ.lookup_constant eff.seff_constant env); env
+ with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env
+ in
+ List.fold_left add_if_undefined env eff
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
+let private_constant env role cst =
+ (** The constant must be the last entry of the safe environment *)
+ let () = match env.revstruct with
+ | (lbl, SFBconst _) :: _ -> assert (Label.equal lbl (Constant.label cst))
+ | _ -> assert false
+ in
+ let from_env = CEphemeron.create env.revstruct in
let cbo = Environ.lookup_constant cst env.env in
- {
+ let eff = {
+ from_env = from_env;
seff_constant = cst;
seff_body = cbo;
seff_env = get_opaque_body env.env cbo;
- seff_role = r;
- }
-
-let private_con_of_con env c =
- let open Entries in
- let eff = [make_eff env c Subproof] in
- add_private env.revstruct eff empty_private_constants
-
-let private_con_of_scheme ~kind env cl =
- let open Entries in
- let eff = List.map (fun (i, c) -> make_eff env c (Schema (i, kind))) cl in
- add_private env.revstruct eff empty_private_constants
+ seff_role = role;
+ } in
+ SideEffects.add eff empty_private_constants
let universes_of_private eff =
- let open Entries in
let fold acc eff =
let acc = match eff.seff_env with
| `Nothing -> acc
@@ -588,22 +595,17 @@ let add_constant_aux ~in_section senv (kn, cb) =
let mk_pure_proof c = (c, Univ.ContextSet.empty), SideEffects.empty
let inline_side_effects env body 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)
+ let filter e =
+ let cb = (e.seff_constant, e.seff_body, e.seff_env) in
+ try ignore (Environ.lookup_constant e.seff_constant env); None
+ with Not_found -> Some (cb, e.from_env)
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.map_filter filter (SideEffects.repr side_eff) in
+ let sigs = List.rev_map (fun (_, mb) -> mb) side_eff in
+ let side_eff = List.fold_left (fun accu (cb, _) -> cb :: 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, Univ.ContextSet.empty, sigs)
@@ -675,24 +677,22 @@ let inline_private_constants_in_definition_entry env ce =
let inline_private_constants_in_constr env body side_eff =
pi1 (inline_side_effects env body 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
+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 is_direct_ancestor accu (mb, how_many) =
+ let is_direct_ancestor accu mb =
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)
+ if is_suffix mb curmb
+ then Some (n + 1, mb)
else None
with CEphemeron.InvalidKey -> None in
let sl = List.fold_left is_direct_ancestor (Some (0, curmb)) sl in
@@ -725,7 +725,6 @@ let constant_entry_of_side_effect cb u =
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
@@ -738,7 +737,6 @@ let turn_direct orig =
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 =
@@ -751,10 +749,9 @@ let export_side_effects mb env c =
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 aux (acc,sl) e =
+ if not (not_exists e) then acc, sl
+ else e :: acc, e.from_env :: 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 =
@@ -772,10 +769,9 @@ let export_side_effects mb env c =
let rec translate_seff sl seff acc env =
match seff with
| [] -> List.rev acc, ce
- | cbs :: rest ->
+ | eff :: rest ->
if Int.equal sl 0 then
- let env, cbs =
- List.fold_left (fun (env,cbs) eff ->
+ let env, cb =
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
@@ -783,15 +779,14 @@ let export_side_effects mb env c =
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
+ (push_seff env eff, export_eff eff)
+ in
+ translate_seff 0 rest (cb :: 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
+ let cb = turn_direct eff in
+ let env = push_seff env cb in
+ let ecb = export_eff cb in
+ translate_seff (sl - 1) rest (ecb :: acc) env
in
translate_seff trusted seff [] env
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 46c97c1fb8..d6c7022cf5 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -43,18 +43,13 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment
type private_constants
-val side_effects_of_private_constants :
- private_constants -> Entries.side_eff list
-(** Return the list of individual side-effects in the order of their
- creation. *)
-
val empty_private_constants : private_constants
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]. *)
-val private_con_of_con : safe_environment -> Constant.t -> private_constants
-val private_con_of_scheme : kind:string -> safe_environment -> (inductive * Constant.t) list -> private_constants
+val private_constant : safe_environment -> Entries.side_effect_role -> Constant.t -> private_constants
+(** Constant must be the last definition of the safe_environment. *)
val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output
val inline_private_constants_in_constr :
@@ -62,6 +57,9 @@ val inline_private_constants_in_constr :
val inline_private_constants_in_definition_entry :
Environ.env -> private_constants Entries.definition_entry -> unit Entries.definition_entry
+val push_private_constants : Environ.env -> private_constants -> Environ.env
+(** Push the constants in the environment if not already there. *)
+
val universes_of_private : private_constants -> Univ.ContextSet.t list
val is_curmod_library : safe_environment -> bool
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 12:07:54 +0000