aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/byterun/coq_uint63_native.h55
-rw-r--r--kernel/declarations.ml9
-rw-r--r--kernel/declareops.ml2
-rw-r--r--kernel/dune4
-rw-r--r--kernel/environ.ml63
-rw-r--r--kernel/environ.mli11
-rw-r--r--kernel/indTyping.ml70
-rw-r--r--kernel/indTyping.mli9
-rw-r--r--kernel/indtypes.ml2
-rw-r--r--kernel/mod_typing.ml3
-rw-r--r--kernel/reduction.ml2
-rw-r--r--kernel/safe_typing.ml12
-rw-r--r--kernel/safe_typing.mli3
-rw-r--r--kernel/subtyping.ml3
-rw-r--r--kernel/uGraph.ml8
-rw-r--r--kernel/uGraph.mli4
-rw-r--r--kernel/uint63.mli10
-rw-r--r--kernel/uint63_31.ml (renamed from kernel/uint63_i386_31.ml)63
-rw-r--r--kernel/uint63_63.ml (renamed from kernel/uint63_amd64_63.ml)67
-rw-r--r--kernel/write_uint63.ml38
20 files changed, 232 insertions, 206 deletions
diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h
index 1fdafc9d8f..9fbd3f83d8 100644
--- a/kernel/byterun/coq_uint63_native.h
+++ b/kernel/byterun/coq_uint63_native.h
@@ -111,51 +111,26 @@ value uint63_mulc(value x, value y, value* h) {
#define le128(xh,xl,yh,yl) (uint63_lt(xh,yh) || (uint63_eq(xh,yh) && uint63_leq(xl,yl)))
#define maxuint63 ((uint64_t)0x7FFFFFFFFFFFFFFF)
-/* precondition: y <> 0 */
-/* outputs r and sets ql to q % 2^63 s.t. x = q * y + r, r < y */
+/* precondition: xh < y */
+/* outputs r and sets ql to q s.t. x = q * y + r, r < y */
static value uint63_div21_aux(value xh, value xl, value y, value* ql) {
- xh = uint63_of_value(xh);
- xl = uint63_of_value(xl);
+ uint64_t nh = uint63_of_value(xh);
+ uint64_t nl = uint63_of_value(xl);
y = uint63_of_value(y);
- uint64_t maskh = 0;
- uint64_t maskl = 1;
- uint64_t dh = 0;
- uint64_t dl = y;
- int cmp = 1;
- /* int n = 0 */
- /* loop invariant: mask = 2^n, d = mask * y, (2 * d <= x -> cmp), n >= 0, d < 2^(2*63) */
- while (!(dh >> (63 - 1)) && cmp) {
- dh = (dh << 1) | (dl >> (63 - 1));
- dl = (dl << 1) & maxuint63;
- maskh = (maskh << 1) | (maskl >> (63 - 1));
- maskl = (maskl << 1) & maxuint63;
- /* ++n */
- cmp = lt128(dh,dl,xh,xl);
+ uint64_t q = 0;
+ for (int i = 0; i < 63; ++i) {
+ // invariants: 0 <= nh < y, nl = (xl*2^i) % 2^64,
+ // (q*y + nh) * 2^(63-i) + (xl % 2^(63-i)) = (xh%y) * 2^63 + xl
+ nl <<= 1;
+ nh = (nh << 1) | (nl >> 63);
+ q <<= 1;
+ if (nh >= y) { q |= 1; nh -= y; }
}
- uint64_t remh = xh;
- uint64_t reml = xl;
- /* uint64_t quotienth = 0; */
- uint64_t quotientl = 0;
- /* loop invariant: x = quotient * y + rem, y * 2^(n+1) > r,
- mask = floor(2^n), d = mask * y, n >= -1 */
- while (maskh | maskl) {
- if (le128(dh,dl,remh,reml)) { /* if rem >= d, add one bit and subtract d */
- /* quotienth = quotienth | maskh */
- quotientl = quotientl | maskl;
- remh = (uint63_lt(reml,dl)) ? (remh - dh - 1) : (remh - dh);
- reml = reml - dl;
- }
- maskl = (maskl >> 1) | ((maskh << (63 - 1)) & maxuint63);
- maskh = maskh >> 1;
- dl = (dl >> 1) | ((dh << (63 - 1)) & maxuint63);
- dh = dh >> 1;
- /* decr n */
- }
- *ql = Val_int(quotientl);
- return Val_int(reml);
+ *ql = Val_int(q);
+ return Val_int(nh);
}
value uint63_div21(value xh, value xl, value y, value* ql) {
- if (uint63_of_value(y) == 0) {
+ if (uint63_leq(y, xh)) {
*ql = Val_int(0);
return Val_int(0);
} else {
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index dff19dee5e..44676c9da5 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -66,6 +66,10 @@ type typing_flags = {
(** If [false] then fixed points and co-fixed points are assumed to
be total. *)
+ check_positive : bool;
+ (** If [false] then inductive types are assumed positive and co-inductive
+ types are assumed productive. *)
+
check_universes : bool;
(** If [false] universe constraints are not checked *)
@@ -83,6 +87,11 @@ type typing_flags = {
indices_matter: bool;
(** The universe of an inductive type must be above that of its indices. *)
+
+ check_template : bool;
+ (* If [false] then we don't check that the universes template-polymorphic
+ inductive parameterize on are necessarily local and unbounded from below.
+ This potentially introduces inconsistencies. *)
}
(* some contraints are in constant_constraints, some other may be in
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 7a553700e8..7225671a1e 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -19,12 +19,14 @@ module RelDecl = Context.Rel.Declaration
let safe_flags oracle = {
check_guarded = true;
+ check_positive = true;
check_universes = true;
conv_oracle = oracle;
share_reduction = true;
enable_VM = true;
enable_native_compiler = true;
indices_matter = true;
+ check_template = true;
}
(** {6 Arities } *)
diff --git a/kernel/dune b/kernel/dune
index 4038bf5638..5f7502ef6b 100644
--- a/kernel/dune
+++ b/kernel/dune
@@ -3,7 +3,7 @@
(synopsis "The Coq Kernel")
(public_name coq.kernel)
(wrapped false)
- (modules (:standard \ genOpcodeFiles uint63_i386_31 uint63_amd64_63 write_uint63))
+ (modules (:standard \ genOpcodeFiles uint63_31 uint63_63))
(libraries lib byterun dynlink))
(executable
@@ -16,7 +16,7 @@
(rule
(targets uint63.ml)
- (deps (:gen-file uint63_%{ocaml-config:architecture}_%{ocaml-config:int_size}.ml))
+ (deps (:gen-file uint63_%{ocaml-config:int_size}.ml))
(action (copy# %{gen-file} %{targets})))
(documentation
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 9a75f0b682..4a2aeea22d 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -59,8 +59,9 @@ type globals = {
type stratification = {
env_universes : UGraph.t;
- env_engagement : engagement;
env_sprop_allowed : bool;
+ env_universes_lbound : Univ.Level.t;
+ env_engagement : engagement
}
type val_kind =
@@ -119,9 +120,9 @@ let empty_env = {
env_nb_rel = 0;
env_stratification = {
env_universes = UGraph.initial_universes;
- env_engagement = PredicativeSet;
env_sprop_allowed = false;
- };
+ env_universes_lbound = Univ.Level.set;
+ env_engagement = PredicativeSet };
env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
retroknowledge = Retroknowledge.empty;
indirect_pterms = Opaqueproof.empty_opaquetab;
@@ -216,6 +217,9 @@ let lookup_named_ctxt id ctxt =
let fold_constants f env acc =
Cmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_constants acc
+let fold_inductives f env acc =
+ Mindmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_inductives acc
+
(* Global constants *)
let lookup_constant_key kn env =
@@ -259,8 +263,15 @@ let type_in_type env = not (typing_flags env).check_universes
let deactivated_guard env = not (typing_flags env).check_guarded
let indices_matter env = env.env_typing_flags.indices_matter
+let check_template env = env.env_typing_flags.check_template
let universes env = env.env_stratification.env_universes
+let universes_lbound env = env.env_stratification.env_universes_lbound
+
+let set_universes_lbound env lbound =
+ let env_stratification = { env.env_stratification with env_universes_lbound = lbound } in
+ { env with env_stratification }
+
let named_context env = env.env_named_context.env_named_ctx
let named_context_val env = env.env_named_context
let rel_context env = env.env_rel_context.env_rel_ctx
@@ -379,29 +390,30 @@ let check_constraints c env =
let push_constraints_to_env (_,univs) env =
add_constraints univs env
-let add_universes strict ctx g =
+let add_universes ~lbound ~strict ctx g =
let g = Array.fold_left
- (fun g v -> UGraph.add_universe v strict g)
+ (fun g v -> UGraph.add_universe ~lbound ~strict v g)
g (Univ.Instance.to_array (Univ.UContext.instance ctx))
in
UGraph.merge_constraints (Univ.UContext.constraints ctx) g
let push_context ?(strict=false) ctx env =
- map_universes (add_universes strict ctx) env
+ map_universes (add_universes ~lbound:(universes_lbound env) ~strict ctx) env
-let add_universes_set strict ctx g =
+let add_universes_set ~lbound ~strict ctx g =
let g = Univ.LSet.fold
(* Be lenient, module typing reintroduces universes and constraints due to includes *)
- (fun v g -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g)
+ (fun v g -> try UGraph.add_universe ~lbound ~strict v g with UGraph.AlreadyDeclared -> g)
(Univ.ContextSet.levels ctx) g
in UGraph.merge_constraints (Univ.ContextSet.constraints ctx) g
let push_context_set ?(strict=false) ctx env =
- map_universes (add_universes_set strict ctx) env
+ map_universes (add_universes_set ~lbound:(universes_lbound env) ~strict ctx) env
let push_subgraph (levels,csts) env =
+ let lbound = universes_lbound env in
let add_subgraph g =
- let newg = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g) levels g in
+ let newg = Univ.LSet.fold (fun v g -> UGraph.add_universe ~lbound ~strict:false v g) levels g in
let newg = UGraph.merge_constraints csts newg in
(if not (Univ.Constraint.is_empty csts) then
let restricted = UGraph.constraints_for ~kept:(UGraph.domain g) newg in
@@ -418,20 +430,24 @@ let set_engagement c env = (* Unsafe *)
(* It's convenient to use [{flags with foo = bar}] so we're smart wrt to it. *)
let same_flags {
check_guarded;
+ check_positive;
check_universes;
conv_oracle;
indices_matter;
share_reduction;
enable_VM;
enable_native_compiler;
+ check_template;
} alt =
check_guarded == alt.check_guarded &&
+ check_positive == alt.check_positive &&
check_universes == alt.check_universes &&
conv_oracle == alt.conv_oracle &&
indices_matter == alt.indices_matter &&
share_reduction == alt.share_reduction &&
enable_VM == alt.enable_VM &&
- enable_native_compiler == alt.enable_native_compiler
+ enable_native_compiler == alt.enable_native_compiler &&
+ check_template == alt.check_template
[@warning "+9"]
let set_typing_flags c env = (* Unsafe *)
@@ -563,11 +579,20 @@ let polymorphic_pind (ind,u) env =
let type_in_type_ind (mind,_i) env =
not (lookup_mind mind env).mind_typing_flags.check_universes
+let template_checked_ind (mind,_i) env =
+ (lookup_mind mind env).mind_typing_flags.check_template
+
let template_polymorphic_ind (mind,i) env =
match (lookup_mind mind env).mind_packets.(i).mind_arity with
| TemplateArity _ -> true
| RegularArity _ -> false
+let template_polymorphic_variables (mind,i) env =
+ match (lookup_mind mind env).mind_packets.(i).mind_arity with
+ | TemplateArity { Declarations.template_param_levels = l; _ } ->
+ List.map_filter (fun level -> level) l
+ | RegularArity _ -> []
+
let template_polymorphic_pind (ind,u) env =
if not (Univ.Instance.is_empty u) then false
else template_polymorphic_ind ind env
@@ -757,6 +782,22 @@ let is_template_polymorphic env r =
| IndRef ind -> template_polymorphic_ind ind env
| ConstructRef cstr -> template_polymorphic_ind (inductive_of_constructor cstr) env
+let get_template_polymorphic_variables env r =
+ let open Names.GlobRef in
+ match r with
+ | VarRef _id -> []
+ | ConstRef _c -> []
+ | IndRef ind -> template_polymorphic_variables ind env
+ | ConstructRef cstr -> template_polymorphic_variables (inductive_of_constructor cstr) env
+
+let is_template_checked env r =
+ let open Names.GlobRef in
+ match r with
+ | VarRef _id -> false
+ | ConstRef _c -> false
+ | IndRef ind -> template_checked_ind ind env
+ | ConstructRef cstr -> template_checked_ind (inductive_of_constructor cstr) env
+
let is_type_in_type env r =
let open Names.GlobRef in
match r with
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 6cd4f96645..f7de98dcfb 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -51,8 +51,9 @@ type globals
type stratification = {
env_universes : UGraph.t;
- env_engagement : engagement;
env_sprop_allowed : bool;
+ env_universes_lbound : Univ.Level.t;
+ env_engagement : engagement
}
type named_context_val = private {
@@ -85,6 +86,8 @@ val eq_named_context_val : named_context_val -> named_context_val -> bool
val empty_env : env
val universes : env -> UGraph.t
+val universes_lbound : env -> Univ.Level.t
+val set_universes_lbound : env -> Univ.Level.t -> env
val rel_context : env -> Constr.rel_context
val named_context : env -> Constr.named_context
val named_context_val : env -> named_context_val
@@ -99,6 +102,7 @@ val is_impredicative_set : env -> bool
val type_in_type : env -> bool
val deactivated_guard : env -> bool
val indices_matter : env -> bool
+val check_template : env -> bool
val is_impredicative_sort : env -> Sorts.t -> bool
val is_impredicative_univ : env -> Univ.Universe.t -> bool
@@ -176,6 +180,7 @@ val pop_rel_context : int -> env -> env
(** Useful for printing *)
val fold_constants : (Constant.t -> Opaqueproof.opaque constant_body -> 'a -> 'a) -> env -> 'a -> 'a
+val fold_inductives : (MutInd.t -> Declarations.mutual_inductive_body -> 'a -> 'a) -> env -> 'a -> 'a
(** {5 Global constants }
{6 Add entries to global environment } *)
@@ -253,7 +258,9 @@ val type_in_type_ind : inductive -> env -> bool
(** Old-style polymorphism *)
val template_polymorphic_ind : inductive -> env -> bool
+val template_polymorphic_variables : inductive -> env -> Univ.Level.t list
val template_polymorphic_pind : pinductive -> env -> bool
+val template_checked_ind : inductive -> env -> bool
(** {5 Modules } *)
@@ -345,6 +352,8 @@ val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declarat
val is_polymorphic : env -> Names.GlobRef.t -> bool
val is_template_polymorphic : env -> GlobRef.t -> bool
+val get_template_polymorphic_variables : env -> GlobRef.t -> Univ.Level.t list
+val is_template_checked : env -> GlobRef.t -> bool
val is_type_in_type : env -> GlobRef.t -> bool
(** Native compiler *)
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index c8e04b9fee..06d2e1bb21 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -236,22 +236,53 @@ let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_;ind_has_relevant_arg=_}
if not ind_squashed then InType
else Sorts.family (Sorts.sort_of_univ ind_univ)
+(* For a level to be template polymorphic, it must be introduced
+ by the definition (so have no constraint except lbound <= l)
+ and not to be constrained from below, so any universe l' <= l
+ can be used as an instance of l. All bounds from above, i.e.
+ l <=/< r will be valid for any l' <= l. *)
+let unbounded_from_below u cstrs =
+ Univ.Constraint.for_all (fun (l, d, r) ->
+ match d with
+ | Eq -> not (Univ.Level.equal l u) && not (Univ.Level.equal r u)
+ | Lt | Le -> not (Univ.Level.equal r u))
+ cstrs
+
(* Returns the list [x_1, ..., x_n] of levels contributing to template
- polymorphism. The elements x_k is None if the k-th parameter (starting
- from the most recent and ignoring let-definitions) is not contributing
- or is Some u_k if its level is u_k and is contributing. *)
-let param_ccls paramsctxt =
+ polymorphism. The elements x_k is None if the k-th parameter
+ (starting from the most recent and ignoring let-definitions) is not
+ contributing to the inductive type's sort or is Some u_k if its level
+ is u_k and is contributing. *)
+let template_polymorphic_univs ~template_check uctx paramsctxt concl =
+ let check_level l =
+ if Univ.LSet.mem l (Univ.ContextSet.levels uctx) &&
+ unbounded_from_below l (Univ.ContextSet.constraints uctx) then
+ Some l
+ else None
+ in
+ let univs = Univ.Universe.levels concl in
+ let univs =
+ if template_check then
+ Univ.LSet.filter (fun l -> Option.has_some (check_level l) || Univ.Level.is_prop l) univs
+ else univs (* Doesn't check the universes can be generalized *)
+ in
let fold acc = function
| (LocalAssum (_, p)) ->
(let c = Term.strip_prod_assum p in
match kind c with
- | Sort (Type u) -> Univ.Universe.level u
+ | Sort (Type u) ->
+ if template_check then
+ (match Univ.Universe.level u with
+ | Some l -> if Univ.LSet.mem l univs && not (Univ.Level.is_prop l) then Some l else None
+ | None -> None)
+ else Univ.Universe.level u
| _ -> None) :: acc
| LocalDef _ -> acc
in
- List.fold_left fold [] paramsctxt
+ let params = List.fold_left fold [] paramsctxt in
+ params, univs
-let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) =
+let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) =
let arity = Vars.subst_univs_level_constr usubst arity in
let lc = Array.map (Vars.subst_univs_level_constr usubst) lc in
let indices = Vars.subst_univs_level_context usubst indices in
@@ -264,14 +295,20 @@ let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_i
let ind_univ = Univ.subst_univs_level_universe usubst univ_info.ind_univ in
let arity = match univ_info.ind_min_univ with
- | None -> RegularArity {mind_user_arity=arity;mind_sort=Sorts.sort_of_univ ind_univ}
+ | None -> RegularArity {mind_user_arity = arity; mind_sort = Sorts.sort_of_univ ind_univ}
| Some min_univ ->
- ((match univs with
- | Monomorphic _ -> ()
+ let ctx = match univs with
+ | Monomorphic ctx -> ctx
| Polymorphic _ ->
CErrors.anomaly ~label:"polymorphic_template_ind"
- Pp.(strbrk "Template polymorphism and full polymorphism are incompatible."));
- TemplateArity {template_param_levels=param_ccls params; template_level=min_univ})
+ Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") in
+ let param_levels, concl_levels = template_polymorphic_univs ~template_check ctx params min_univ in
+ if template_check && List.for_all (fun x -> Option.is_empty x) param_levels
+ && Univ.LSet.is_empty concl_levels then
+ CErrors.anomaly ~label:"polymorphic_template_ind"
+ Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.")
+ else
+ TemplateArity {template_param_levels = param_levels; template_level = min_univ}
in
let kelim = allowed_sorts univ_info in
@@ -286,10 +323,14 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
mind_check_names mie;
assert (List.is_empty (Environ.rel_context env));
+ let has_template_poly = List.exists (fun oie -> oie.mind_entry_template) mie.mind_entry_inds in
+
(* universes *)
let env_univs =
match mie.mind_entry_universes with
- | Monomorphic_entry ctx -> push_context_set ctx env
+ | Monomorphic_entry ctx ->
+ let env = if has_template_poly then set_universes_lbound env Univ.Level.prop else env in
+ push_context_set ctx env
| Polymorphic_entry (_, ctx) -> push_context ctx env
in
@@ -335,7 +376,8 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
(* Abstract universes *)
let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in
let params = Vars.subst_univs_level_context usubst params in
- let data = List.map (abstract_packets univs usubst params) data in
+ let template_check = Environ.check_template env in
+ let data = List.map (abstract_packets ~template_check univs usubst params) data in
let env_ar_par =
let ctx = Environ.rel_context env_ar_par in
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index aaa0d6a149..8da4e2885c 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -33,3 +33,12 @@ val typecheck_inductive : env -> mutual_inductive_entry ->
(Constr.rel_context * (Constr.rel_context * Constr.types) array) *
Sorts.family)
array
+
+(* Utility function to compute the actual universe parameters
+ of a template polymorphic inductive *)
+val template_polymorphic_univs :
+ template_check:bool ->
+ Univ.ContextSet.t ->
+ Constr.rel_context ->
+ Univ.Universe.t ->
+ Univ.Level.t option list * Univ.LSet.t
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index b0366d6ec0..aa3ef715db 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -546,7 +546,7 @@ let check_inductive env kn mie =
(* First type-check the inductive definition *)
let (env_ar_par, univs, variance, record, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in
(* Then check positivity conditions *)
- let chkpos = (Environ.typing_flags env).check_guarded in
+ let chkpos = (Environ.typing_flags env).check_positive in
let names = Array.map_of_list (fun entry -> entry.mind_entry_typename, entry.mind_entry_consnames)
mie.mind_entry_inds
in
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 9305a91731..ccc218771a 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -94,7 +94,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
c', Monomorphic Univ.ContextSet.empty, cst
| Polymorphic uctx, Some ctx ->
let () =
- if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then
+ if not (UGraph.check_subtype ~lbound:(Environ.universes_lbound env)
+ (Environ.universes env) uctx ctx) then
error_incorrect_with_constraint lab
in
(** Terms are compared in a context with De Bruijn universe indices *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 53f228c618..327cb2efeb 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -777,7 +777,7 @@ let infer_cmp_universes env pb s0 s1 univs =
| Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible else univs
| Set, Prop -> raise NotConvertible
| Set, Type u -> infer_pb Univ.type0_univ u
- | Type _u, Prop -> raise NotConvertible
+ | Type u, Prop -> infer_pb u Univ.type0m_univ
| Type u, Set -> infer_pb u Univ.type0_univ
| Type u0, Type u1 -> infer_pb u0 u1
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ea45f699ce..6970a11e72 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -194,6 +194,18 @@ let set_typing_flags c senv =
if env == senv.env then senv
else { senv with env }
+let set_check_guarded b senv =
+ let flags = Environ.typing_flags senv.env in
+ set_typing_flags { flags with check_guarded = b } senv
+
+let set_check_positive b senv =
+ let flags = Environ.typing_flags senv.env in
+ set_typing_flags { flags with check_positive = b } senv
+
+let set_check_universes b senv =
+ let flags = Environ.typing_flags senv.env in
+ set_typing_flags { flags with check_universes = b } senv
+
let set_indices_matter indices_matter senv =
set_typing_flags { (Environ.typing_flags senv.env) with indices_matter } senv
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 2406b6add1..fa53fa33fa 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -130,6 +130,9 @@ val set_engagement : Declarations.engagement -> safe_transformer0
val set_indices_matter : bool -> safe_transformer0
val set_typing_flags : Declarations.typing_flags -> safe_transformer0
val set_share_reduction : bool -> safe_transformer0
+val set_check_guarded : bool -> safe_transformer0
+val set_check_positive : bool -> safe_transformer0
+val set_check_universes : bool -> safe_transformer0
val set_VM : bool -> safe_transformer0
val set_native_compiler : bool -> safe_transformer0
val make_sprop_cumulative : safe_transformer0
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index d47dc0c6e1..d22ec3b7ca 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -97,7 +97,8 @@ let check_universes error env u1 u2 =
match u1, u2 with
| Monomorphic _, Monomorphic _ -> env
| Polymorphic auctx1, Polymorphic auctx2 ->
- if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then
+ let lbound = Environ.universes_lbound env in
+ if not (UGraph.check_subtype ~lbound (Environ.universes env) auctx2 auctx1) then
error (IncompatibleConstraints { got = auctx1; expect = auctx2; } )
else
Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 6fde6e9c5f..33336079bb 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -149,10 +149,10 @@ let enforce_leq_alg u v g =
cg
exception AlreadyDeclared = G.AlreadyDeclared
-let add_universe u strict g =
+let add_universe u ~lbound ~strict g =
let graph = G.add u g.graph in
let d = if strict then Lt else Le in
- enforce_constraint (Level.set,d,u) {g with graph}
+ enforce_constraint (lbound,d,u) {g with graph}
let add_universe_unconstrained u g = {g with graph=G.add u g.graph}
@@ -164,11 +164,11 @@ let constraints_for ~kept g = G.constraints_for ~kept:(LSet.remove Level.sprop k
(** Subtyping of polymorphic contexts *)
-let check_subtype univs ctxT ctx =
+let check_subtype ~lbound univs ctxT ctx =
if AUContext.size ctxT == AUContext.size ctx then
let (inst, cst) = UContext.dest (AUContext.repr ctx) in
let cstT = UContext.constraints (AUContext.repr ctxT) in
- let push accu v = add_universe v false accu in
+ let push accu v = add_universe v ~lbound ~strict:false accu in
let univs = Array.fold_left push univs (Instance.to_array inst) in
let univs = merge_constraints cstT univs in
check_constraints cst univs
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index e1b5868d55..d90f01d8d1 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -48,7 +48,7 @@ val enforce_leq_alg : Universe.t -> Universe.t -> t -> Constraint.t * t
exception AlreadyDeclared
-val add_universe : Level.t -> bool -> t -> t
+val add_universe : Level.t -> lbound:Level.t -> strict:bool -> t -> t
(** Add a universe without (Prop,Set) <= u *)
val add_universe_unconstrained : Level.t -> t -> t
@@ -86,7 +86,7 @@ val constraints_for : kept:LSet.t -> t -> Constraint.t
val domain : t -> LSet.t
(** Known universes *)
-val check_subtype : AUContext.t check_function
+val check_subtype : lbound:Level.t -> AUContext.t check_function
(** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of
[ctx1]. *)
diff --git a/kernel/uint63.mli b/kernel/uint63.mli
index 5542716af2..d22ba3468f 100644
--- a/kernel/uint63.mli
+++ b/kernel/uint63.mli
@@ -1,3 +1,13 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
type t
val uint_size : int
diff --git a/kernel/uint63_i386_31.ml b/kernel/uint63_31.ml
index 2a3fc75ec1..b8eccd19fb 100644
--- a/kernel/uint63_i386_31.ml
+++ b/kernel/uint63_31.ml
@@ -88,55 +88,28 @@ let diveucl x y = (div x y, rem x y)
let addmuldiv p x y =
l_or (l_sl x p) (l_sr y Int64.(sub (of_int uint_size) p))
-(* A few helper functions on 128 bits *)
-let lt128 xh xl yh yl =
- lt xh yh || (xh = yh && lt xl yl)
-
-let le128 xh xl yh yl =
- lt xh yh || (xh = yh && le xl yl)
-
(* division of two numbers by one *)
-(* precondition: y <> 0 *)
-(* outputs: q % 2^63, r s.t. x = q * y + r, r < y *)
+(* precondition: xh < y *)
+(* outputs: q, r s.t. x = q * y + r, r < y *)
let div21 xh xl y =
- let maskh = ref zero in
- let maskl = ref one in
- let dh = ref zero in
- let dl = ref y in
- let cmp = ref true in
- (* n = ref 0 *)
- (* loop invariant: mask = 2^n, d = mask * y, (2 * d <= x -> cmp), n >= 0 *)
- while Int64.equal (l_sr !dh (of_int (uint_size - 1))) zero && !cmp do
- (* We don't use addmuldiv below to avoid checks on 1 *)
- dh := l_or (l_sl !dh one) (l_sr !dl (of_int (uint_size - 1)));
- dl := l_sl !dl one;
- maskh := l_or (l_sl !maskh one) (l_sr !maskl (of_int (uint_size - 1)));
- maskl := l_sl !maskl one;
- (* incr n *)
- cmp := lt128 !dh !dl xh xl;
- done; (* mask = 2^n, d = 2^n * d, 2 * d > x *)
- let remh = ref xh in
- let reml = ref xl in
- (* quotienth = ref 0 *)
- let quotientl = ref zero in
- (* loop invariant: x = quotient * y + rem, y * 2^(n+1) > r,
- mask = floor(2^n), d = mask * y, n >= -1 *)
- while not (Int64.equal (l_or !maskh !maskl) zero) do
- if le128 !dh !dl !remh !reml then begin (* if rem >= d, add one bit and subtract d *)
- (* quotienth := !quotienth lor !maskh *)
- quotientl := l_or !quotientl !maskl;
- remh := if lt !reml !dl then sub (sub !remh !dh) one else sub !remh !dh;
- reml := sub !reml !dl
- end;
- maskl := l_or (l_sr !maskl one) (l_sl !maskh (of_int (uint_size - 1)));
- maskh := l_sr !maskh one;
- dl := l_or (l_sr !dl one) (l_sl !dh (of_int (uint_size - 1)));
- dh := l_sr !dh one
- (* decr n *)
+ let nh = ref xh in
+ let nl = ref xl in
+ let q = ref 0L in
+ for _i = 0 to 62 do
+ (* invariants: 0 <= nh < y, nl = (xl*2^i) % 2^64,
+ (q*y + nh) * 2^(63-i) + (xl % 2^(63-i)) = (xh%y) * 2^63 + xl *)
+ nl := Int64.shift_left !nl 1;
+ nh := Int64.logor (Int64.shift_left !nh 1) (Int64.shift_right_logical !nl 63);
+ q := Int64.shift_left !q 1;
+ (* TODO: use "Int64.unsigned_compare !nh y >= 0",
+ once OCaml 4.08 becomes the minimal required version *)
+ if Int64.compare !nh 0L < 0 || Int64.compare !nh y >= 0 then
+ begin q := Int64.logor !q 1L; nh := Int64.sub !nh y; end
done;
- !quotientl, !reml
+ !q, !nh
-let div21 xh xl y = if Int64.equal y zero then zero, zero else div21 xh xl y
+let div21 xh xl y =
+ if Int64.compare y xh <= 0 then zero, zero else div21 xh xl y
(* exact multiplication *)
let mulc x y =
diff --git a/kernel/uint63_amd64_63.ml b/kernel/uint63_63.ml
index d6b077a9f5..5c4028e1c8 100644
--- a/kernel/uint63_amd64_63.ml
+++ b/kernel/uint63_63.ml
@@ -96,55 +96,32 @@ let le (x : int) (y : int) =
(x lxor 0x4000000000000000) <= (y lxor 0x4000000000000000)
[@@ocaml.inline always]
-(* A few helper functions on 128 bits *)
-let lt128 xh xl yh yl =
- lt xh yh || (xh = yh && lt xl yl)
-
-let le128 xh xl yh yl =
- lt xh yh || (xh = yh && le xl yl)
-
(* division of two numbers by one *)
-(* precondition: y <> 0 *)
-(* outputs: q % 2^63, r s.t. x = q * y + r, r < y *)
+(* precondition: xh < y *)
+(* outputs: q, r s.t. x = q * y + r, r < y *)
let div21 xh xl y =
- let maskh = ref 0 in
- let maskl = ref 1 in
- let dh = ref 0 in
- let dl = ref y in
- let cmp = ref true in
- (* n = ref 0 *)
- (* loop invariant: mask = 2^n, d = mask * y, (2 * d <= x -> cmp), n >= 0 *)
- while !dh >= 0 && !cmp do (* dh >= 0 tests that dh highest bit is zero *)
- (* We don't use addmuldiv below to avoid checks on 1 *)
- dh := (!dh lsl 1) lor (!dl lsr (uint_size - 1));
- dl := !dl lsl 1;
- maskh := (!maskh lsl 1) lor (!maskl lsr (uint_size - 1));
- maskl := !maskl lsl 1;
- (* incr n *)
- cmp := lt128 !dh !dl xh xl;
- done; (* mask = 2^n, d = 2^n * y, 2 * d > x *)
- let remh = ref xh in
- let reml = ref xl in
- (* quotienth = ref 0 *)
- let quotientl = ref 0 in
- (* loop invariant: x = quotient * y + rem, y * 2^(n+1) > r,
- mask = floor(2^n), d = mask * y, n >= -1 *)
- while !maskh lor !maskl <> 0 do
- if le128 !dh !dl !remh !reml then begin (* if rem >= d, add one bit and subtract d *)
- (* quotienth := !quotienth lor !maskh *)
- quotientl := !quotientl lor !maskl;
- remh := if lt !reml !dl then !remh - !dh - 1 else !remh - !dh;
- reml := !reml - !dl;
- end;
- maskl := (!maskl lsr 1) lor (!maskh lsl (uint_size - 1));
- maskh := !maskh lsr 1;
- dl := (!dl lsr 1) lor (!dh lsl (uint_size - 1));
- dh := !dh lsr 1;
- (* decr n *)
+ (* nh might temporarily grow as large as 2*y - 1 in the loop body,
+ so we store it as a 64-bit unsigned integer *)
+ let nh = ref xh in
+ let nl = ref xl in
+ let q = ref 0 in
+ for _i = 0 to 62 do
+ (* invariants: 0 <= nh < y, nl = (xl*2^i) % 2^63,
+ (q*y + nh) * 2^(63-i) + (xl % 2^(63-i)) = (xh%y) * 2^63 + xl *)
+ nh := Int64.logor (Int64.shift_left !nh 1) (Int64.of_int (!nl lsr 62));
+ nl := !nl lsl 1;
+ q := !q lsl 1;
+ (* TODO: use "Int64.unsigned_compare !nh y >= 0",
+ once OCaml 4.08 becomes the minimal required version *)
+ if Int64.compare !nh 0L < 0 || Int64.compare !nh y >= 0 then
+ begin q := !q lor 1; nh := Int64.sub !nh y; end
done;
- !quotientl, !reml
+ !q, Int64.to_int !nh
-let div21 xh xl y = if y = 0 then 0, 0 else div21 xh xl y
+let div21 xh xl y =
+ let xh = to_uint64 xh in
+ let y = to_uint64 y in
+ if Int64.compare y xh <= 0 then 0, 0 else div21 xh xl y
(* exact multiplication *)
(* TODO: check that none of these additions could be a logical or *)
diff --git a/kernel/write_uint63.ml b/kernel/write_uint63.ml
deleted file mode 100644
index 57a170c8f5..0000000000
--- a/kernel/write_uint63.ml
+++ /dev/null
@@ -1,38 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-(** Equivalent of rm -f *)
-let safe_remove f =
- try Unix.chmod f 0o644; Sys.remove f with _ -> ()
-
-(** * Generate an implementation of 63-bit arithmetic *)
-let ml_file_copy input output =
- safe_remove output;
- let i = open_in input in
- let o = open_out output in
- let pr s = Printf.fprintf o s in
- pr "(* DO NOT EDIT THIS FILE: automatically generated by ./write_uint63.ml *)\n";
- pr "(* see uint63_amd64.ml and uint63_x86.ml *)\n";
- try
- while true do
- output_string o (input_line i); output_char o '\n'
- done
- with End_of_file ->
- close_in i;
- close_out o;
- Unix.chmod output 0o444
-
-let write_uint63 () =
- ml_file_copy
- (if max_int = 1073741823 (* 32-bits *) then "uint63_i386_31.ml"
- else (* 64 bits *) "uint63_amd64_63.ml")
- "uint63.ml"
-
-let () = write_uint63 ()
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 00:57:40 +0000