aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/dune7
-rw-r--r--kernel/environ.ml15
-rw-r--r--kernel/environ.mli2
-rw-r--r--kernel/float64_31.ml35
-rw-r--r--kernel/float64_63.ml35
-rw-r--r--kernel/float64_common.ml (renamed from kernel/float64.ml)24
-rw-r--r--kernel/float64_common.mli95
-rw-r--r--kernel/indTyping.ml2
-rw-r--r--kernel/kernel.mllib1
-rw-r--r--kernel/mod_typing.ml10
-rw-r--r--kernel/nativeconv.ml4
-rw-r--r--kernel/reduction.ml42
-rw-r--r--kernel/reduction.mli6
-rw-r--r--kernel/safe_typing.ml10
-rw-r--r--kernel/subtyping.ml2
-rw-r--r--kernel/typeops.mli2
-rw-r--r--kernel/uGraph.ml32
-rw-r--r--kernel/uGraph.mli12
-rw-r--r--kernel/univ.ml42
-rw-r--r--kernel/vconv.ml4
-rw-r--r--kernel/vmbytecodes.ml6
21 files changed, 284 insertions, 104 deletions
diff --git a/kernel/dune b/kernel/dune
index ce6fdc03df..bd663974da 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_31 uint63_63))
+ (modules (:standard \ genOpcodeFiles uint63_31 uint63_63 float64_31 float64_63))
(libraries lib byterun dynlink))
(executable
@@ -19,6 +19,11 @@
(deps (:gen-file uint63_%{ocaml-config:int_size}.ml))
(action (copy# %{gen-file} %{targets})))
+(rule
+ (targets float64.ml)
+ (deps (:gen-file float64_%{ocaml-config:int_size}.ml))
+ (action (copy# %{gen-file} %{targets})))
+
(documentation
(package coq))
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 03c9cb4be6..dec9e1deb8 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -274,6 +274,11 @@ let is_impredicative_sort env = function
let is_impredicative_univ env u = is_impredicative_sort env (Sorts.sort_of_univ u)
+let is_impredicative_family env = function
+ | Sorts.InSProp | Sorts.InProp -> true
+ | Sorts.InSet -> is_impredicative_set env
+ | Sorts.InType -> false
+
let type_in_type env = not (typing_flags env).check_universes
let deactivated_guard env = not (typing_flags env).check_guarded
@@ -467,14 +472,22 @@ let same_flags {
[@warning "+9"]
let set_cumulative_sprop b = map_universes (UGraph.set_cumulative_sprop b)
+let set_type_in_type b = map_universes (UGraph.set_type_in_type b)
let set_typing_flags c env =
if same_flags env.env_typing_flags c then env
- else set_cumulative_sprop c.cumulative_sprop { env with env_typing_flags = c }
+ else
+ let env = { env with env_typing_flags = c } in
+ let env = set_cumulative_sprop c.cumulative_sprop env in
+ let env = set_type_in_type (not c.check_universes) env in
+ env
let set_cumulative_sprop b env =
set_typing_flags {env.env_typing_flags with cumulative_sprop=b} env
+let set_type_in_type b env =
+ set_typing_flags {env.env_typing_flags with check_universes=not b} env
+
let set_allow_sprop b env =
{ env with env_stratification =
{ env.env_stratification with env_sprop_allowed = b } }
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 974e794c6b..f443ba38e1 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -122,6 +122,7 @@ val indices_matter : env -> bool
val is_impredicative_sort : env -> Sorts.t -> bool
val is_impredicative_univ : env -> Univ.Universe.t -> bool
+val is_impredicative_family : env -> Sorts.family -> bool
(** is the local context empty *)
val empty_context : env -> bool
@@ -320,6 +321,7 @@ val push_subgraph : Univ.ContextSet.t -> env -> env
val set_engagement : engagement -> env -> env
val set_typing_flags : typing_flags -> env -> env
val set_cumulative_sprop : bool -> env -> env
+val set_type_in_type : bool -> env -> env
val set_allow_sprop : bool -> env -> env
val sprop_allowed : env -> bool
diff --git a/kernel/float64_31.ml b/kernel/float64_31.ml
new file mode 100644
index 0000000000..09b28e6cf0
--- /dev/null
+++ b/kernel/float64_31.ml
@@ -0,0 +1,35 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(* \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) *)
+(************************************************************************)
+
+include Float64_common
+
+external mul : float -> float -> float = "coq_fmul_byte" "coq_fmul"
+[@@unboxed] [@@noalloc]
+
+external add : float -> float -> float = "coq_fadd_byte" "coq_fadd"
+[@@unboxed] [@@noalloc]
+
+external sub : float -> float -> float = "coq_fsub_byte" "coq_fsub"
+[@@unboxed] [@@noalloc]
+
+external div : float -> float -> float = "coq_fdiv_byte" "coq_fdiv"
+[@@unboxed] [@@noalloc]
+
+external sqrt : float -> float = "coq_fsqrt_byte" "coq_fsqrt"
+[@@unboxed] [@@noalloc]
+
+(*** Test at runtime that no harmful double rounding seems to
+ be performed with an intermediate 80 bits representation (x87). *)
+let () =
+ let b = ldexp 1. 53 in
+ let s = add 1. (ldexp 1. (-52)) in
+ if add b s <= b || add b 1. <> b || ldexp 1. (-1074) <= 0. then
+ failwith "Detected non IEEE-754 compliant architecture (or wrong \
+ rounding mode). Use of Float is thus unsafe."
diff --git a/kernel/float64_63.ml b/kernel/float64_63.ml
new file mode 100644
index 0000000000..0025531cb1
--- /dev/null
+++ b/kernel/float64_63.ml
@@ -0,0 +1,35 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(* \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) *)
+(************************************************************************)
+
+include Float64_common
+
+let mul (x : float) (y : float) : float = x *. y
+[@@ocaml.inline always]
+
+let add (x : float) (y : float) : float = x +. y
+[@@ocaml.inline always]
+
+let sub (x : float) (y : float) : float = x -. y
+[@@ocaml.inline always]
+
+let div (x : float) (y : float) : float = x /. y
+[@@ocaml.inline always]
+
+let sqrt (x : float) : float = sqrt x
+[@@ocaml.inline always]
+
+(*** Test at runtime that no harmful double rounding seems to
+ be performed with an intermediate 80 bits representation (x87). *)
+let () =
+ let b = ldexp 1. 53 in
+ let s = add 1. (ldexp 1. (-52)) in
+ if add b s <= b || add b 1. <> b || ldexp 1. (-1074) <= 0. then
+ failwith "Detected non IEEE-754 compliant architecture (or wrong \
+ rounding mode). Use of Float is thus unsafe."
diff --git a/kernel/float64.ml b/kernel/float64_common.ml
index 76005a3dc6..2991a20b49 100644
--- a/kernel/float64.ml
+++ b/kernel/float64_common.ml
@@ -88,21 +88,6 @@ let classify x =
| FP_nan -> NaN
[@@ocaml.inline always]
-external mul : float -> float -> float = "coq_fmul_byte" "coq_fmul"
-[@@unboxed] [@@noalloc]
-
-external add : float -> float -> float = "coq_fadd_byte" "coq_fadd"
-[@@unboxed] [@@noalloc]
-
-external sub : float -> float -> float = "coq_fsub_byte" "coq_fsub"
-[@@unboxed] [@@noalloc]
-
-external div : float -> float -> float = "coq_fdiv_byte" "coq_fdiv"
-[@@unboxed] [@@noalloc]
-
-external sqrt : float -> float = "coq_fsqrt_byte" "coq_fsqrt"
-[@@unboxed] [@@noalloc]
-
let of_int63 x = Uint63.to_float x
[@@ocaml.inline always]
@@ -157,12 +142,3 @@ let total_compare f1 f2 =
let is_float64 t =
Obj.tag t = Obj.double_tag
[@@ocaml.inline always]
-
-(*** Test at runtime that no harmful double rounding seems to
- be performed with an intermediate 80 bits representation (x87). *)
-let () =
- let b = ldexp 1. 53 in
- let s = add 1. (ldexp 1. (-52)) in
- if add b s <= b || add b 1. <> b || ldexp 1. (-1074) <= 0. then
- failwith "Detected non IEEE-754 compliant architecture (or wrong \
- rounding mode). Use of Float is thus unsafe."
diff --git a/kernel/float64_common.mli b/kernel/float64_common.mli
new file mode 100644
index 0000000000..4fb1c114a5
--- /dev/null
+++ b/kernel/float64_common.mli
@@ -0,0 +1,95 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(* \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) *)
+(************************************************************************)
+
+(** [t] is currently implemented by OCaml's [float] type.
+
+Beware: NaNs have a sign and a payload, while they should be
+indistinguishable from Coq's perspective. *)
+type t = float
+
+(** Test functions for special values to avoid calling [classify] *)
+val is_nan : t -> bool
+val is_infinity : t -> bool
+val is_neg_infinity : t -> bool
+
+val of_string : string -> t
+
+(** Print a float exactly as an hexadecimal value (exact decimal
+ * printing would be possible but sometimes requires more than 700
+ * digits). *)
+val to_hex_string : t -> string
+
+(** Print a float as a decimal value. The printing is not exact (the
+ * real value printed is not always the given floating-point value),
+ * however printing is precise enough that forall float [f],
+ * [of_string (to_decimal_string f) = f]. *)
+val to_string : t -> string
+
+val compile : t -> string
+
+val of_float : float -> t
+
+(** Return [true] for "-", [false] for "+". *)
+val sign : t -> bool
+
+val opp : t -> t
+val abs : t -> t
+
+type float_comparison = FEq | FLt | FGt | FNotComparable
+
+val eq : t -> t -> bool
+
+val lt : t -> t -> bool
+
+val le : t -> t -> bool
+
+(** The IEEE 754 float comparison.
+ * NotComparable is returned if there is a NaN in the arguments *)
+val compare : t -> t -> float_comparison
+[@@ocaml.inline always]
+
+type float_class =
+ | PNormal | NNormal | PSubn | NSubn | PZero | NZero | PInf | NInf | NaN
+
+val classify : t -> float_class
+[@@ocaml.inline always]
+
+(** Link with integers *)
+val of_int63 : Uint63.t -> t
+[@@ocaml.inline always]
+
+val normfr_mantissa : t -> Uint63.t
+[@@ocaml.inline always]
+
+(** Shifted exponent extraction *)
+val eshift : int
+
+val frshiftexp : t -> t * Uint63.t (* float remainder, shifted exponent *)
+[@@ocaml.inline always]
+
+val ldshiftexp : t -> Uint63.t -> t
+[@@ocaml.inline always]
+
+val next_up : t -> t
+
+val next_down : t -> t
+
+(** Return true if two floats are equal.
+ * All NaN values are considered equal. *)
+val equal : t -> t -> bool
+[@@ocaml.inline always]
+
+val hash : t -> int
+
+(** Total order relation over float values. Behaves like [Pervasives.compare].*)
+val total_compare : t -> t -> int
+
+val is_float64 : Obj.t -> bool
+[@@ocaml.inline always]
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 179353d3f0..b2520b780f 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -77,7 +77,7 @@ let check_univ_leq ?(is_real_arg=false) env u info =
else info
in
(* Inductive types provide explicit lifting from SProp to other universes, so allow SProp <= any. *)
- if type_in_type env || Univ.Universe.is_sprop u || UGraph.check_leq (universes env) u ind_univ
+ if Univ.Universe.is_sprop u || UGraph.check_leq (universes env) u ind_univ
then { info with ind_min_univ = Option.map (Universe.sup u) info.ind_min_univ }
else if is_impredicative_univ env ind_univ
&& Option.is_empty info.ind_min_univ then { info with ind_squashed = true }
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index d4d7150222..5b2a7bd9c2 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -2,6 +2,7 @@ Names
TransparentState
Uint63
Parray
+Float64_common
Float64
Univ
UGraph
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 5873d1f502..c7b866179b 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -80,12 +80,11 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
let j = Typeops.infer env' c in
assert (j.uj_val == c); (* relevances should already be correct here *)
let typ = cb.const_type in
- let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
- j.uj_type typ in
+ let cst' = Reduction.infer_conv_leq env' j.uj_type typ in
j.uj_val, cst'
| Def cs ->
let c' = Mod_subst.force_constr cs in
- c, Reduction.infer_conv env' (Environ.universes env') c c'
+ c, Reduction.infer_conv env' c c'
| Primitive _ ->
error_incorrect_with_constraint lab
in
@@ -103,12 +102,11 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
let j = Typeops.infer env' c in
assert (j.uj_val == c); (* relevances should already be correct here *)
let typ = cb.const_type in
- let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
- j.uj_type typ in
+ let cst' = Reduction.infer_conv_leq env' j.uj_type typ in
cst'
| Def cs ->
let c' = Mod_subst.force_constr cs in
- let cst' = Reduction.infer_conv env' (Environ.universes env') c c' in
+ let cst' = Reduction.infer_conv env' c c' in
cst'
| Primitive _ ->
error_incorrect_with_constraint lab
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 01e9550ec5..fc6afb79d4 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -176,7 +176,7 @@ let native_conv cv_pb sigma env t1 t2 =
else Constr.eq_constr_univs univs t1 t2
in
if not b then
- let univs = (univs, checked_universes) in
+ let state = (univs, checked_universes) in
let t1 = Term.it_mkLambda_or_LetIn t1 (Environ.rel_context env) in
let t2 = Term.it_mkLambda_or_LetIn t2 (Environ.rel_context env) in
- let _ = native_conv_gen cv_pb sigma env univs t1 t2 in ()
+ let _ = native_conv_gen cv_pb sigma env state t1 t2 in ()
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 7c6b869b4a..96bf370342 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -189,7 +189,7 @@ type 'a kernel_conversion_function = env -> 'a -> 'a -> unit
(* functions of this type can be called from outside the kernel *)
type 'a extended_conversion_function =
?l2r:bool -> ?reds:TransparentState.t -> env ->
- ?evars:((existential->constr option) * UGraph.t) ->
+ ?evars:(existential->constr option) ->
'a -> 'a -> unit
exception NotConvertible
@@ -210,9 +210,6 @@ type conv_pb =
let is_cumul = function CUMUL -> true | CONV -> false
type 'a universe_compare = {
- (* used in reduction *)
- compare_graph : 'a -> UGraph.t;
-
(* Might raise NotConvertible *)
compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
@@ -224,7 +221,7 @@ type 'a universe_state = 'a * 'a universe_compare
type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b
-type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t
+type 'a infer_conversion_function = env -> 'a -> 'a -> Univ.Constraint.t
let sort_cmp_universes env pb s0 s1 (u, check) =
(check.compare_sorts env pb s0 s1 u, check)
@@ -765,9 +762,8 @@ and convert_list l2r infos lft1 lft2 v1 v2 cuniv = match v1, v2 with
convert_list l2r infos lft1 lft2 v1 v2 cuniv
| _, _ -> raise NotConvertible
-let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
+let clos_gen_conv trans cv_pb l2r evars env graph univs t1 t2 =
let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in
- let graph = (snd univs).compare_graph (fst univs) in
let infos = create_clos_infos ~univs:graph ~evars reds env in
let infos = {
cnv_inf = infos;
@@ -815,8 +811,7 @@ let check_inductive_instances cv_pb variance u1 u2 univs =
else raise NotConvertible
let checked_universes =
- { compare_graph = (fun x -> x);
- compare_sorts = checked_sort_cmp_universes;
+ { compare_sorts = checked_sort_cmp_universes;
compare_instances = check_convert_instances;
compare_cumul_instances = check_inductive_instances; }
@@ -878,8 +873,7 @@ let infer_inductive_instances cv_pb variance u1 u2 (univs,csts') =
(univs, Univ.Constraint.union csts csts')
let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare =
- { compare_graph = (fun (x,_) -> x);
- compare_sorts = infer_cmp_universes;
+ { compare_sorts = infer_cmp_universes;
compare_instances = infer_convert_instances;
compare_cumul_instances = infer_inductive_instances; }
@@ -890,12 +884,12 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 =
in
if b then ()
else
- let _ = clos_gen_conv reds cv_pb l2r evars env (univs, checked_universes) t1 t2 in
+ let _ = clos_gen_conv reds cv_pb l2r evars env univs (univs, checked_universes) t1 t2 in
()
(* Profiling *)
-let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _->None), universes env) =
- let evars, univs = evars in
+let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _->None)) =
+ let univs = Environ.universes env in
if Flags.profile then
let fconv_universes_key = CProfile.declare_profile "trans_fconv_universes" in
CProfile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs
@@ -906,35 +900,37 @@ let conv = gen_conv CONV
let conv_leq = gen_conv CUMUL
let generic_conv cv_pb ~l2r evars reds env univs t1 t2 =
+ let graph = Environ.universes env in
let (s, _) =
- clos_gen_conv reds cv_pb l2r evars env univs t1 t2
+ clos_gen_conv reds cv_pb l2r evars env graph univs t1 t2
in s
-let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 =
+let infer_conv_universes cv_pb l2r evars reds env t1 t2 =
+ let univs = Environ.universes env in
let b, cstrs =
if cv_pb == CUMUL then Constr.leq_constr_univs_infer univs t1 t2
else Constr.eq_constr_univs_infer univs t1 t2
in
if b then cstrs
else
- let univs = ((univs, Univ.Constraint.empty), inferred_universes) in
- let ((_,cstrs), _) = clos_gen_conv reds cv_pb l2r evars env univs t1 t2 in
+ let state = ((univs, Univ.Constraint.empty), inferred_universes) in
+ let ((_,cstrs), _) = clos_gen_conv reds cv_pb l2r evars env univs state t1 t2 in
cstrs
(* Profiling *)
let infer_conv_universes =
if Flags.profile then
let infer_conv_universes_key = CProfile.declare_profile "infer_conv_universes" in
- CProfile.profile8 infer_conv_universes_key infer_conv_universes
+ CProfile.profile7 infer_conv_universes_key infer_conv_universes
else infer_conv_universes
let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full)
- env univs t1 t2 =
- infer_conv_universes CONV l2r evars ts env univs t1 t2
+ env t1 t2 =
+ infer_conv_universes CONV l2r evars ts env t1 t2
let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full)
- env univs t1 t2 =
- infer_conv_universes CUMUL l2r evars ts env univs t1 t2
+ env t1 t2 =
+ infer_conv_universes CUMUL l2r evars ts env t1 t2
let default_conv cv_pb ?l2r:_ env t1 t2 =
gen_conv cv_pb env t1 t2
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 4ae3838691..7d32596f74 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -31,14 +31,12 @@ exception NotConvertible
type 'a kernel_conversion_function = env -> 'a -> 'a -> unit
type 'a extended_conversion_function =
?l2r:bool -> ?reds:TransparentState.t -> env ->
- ?evars:((existential->constr option) * UGraph.t) ->
+ ?evars:(existential->constr option) ->
'a -> 'a -> unit
type conv_pb = CONV | CUMUL
type 'a universe_compare = {
- compare_graph : 'a -> UGraph.t; (* used for case inversion in reduction *)
-
(* Might raise NotConvertible *)
compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
@@ -50,7 +48,7 @@ type 'a universe_state = 'a * 'a universe_compare
type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b
-type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t
+type 'a infer_conversion_function = env -> 'a -> 'a -> Univ.Constraint.t
val get_cumulativity_constraints : conv_pb -> Univ.Variance.t array ->
Univ.Instance.t -> Univ.Instance.t -> Univ.Constraint.t
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index da77a2882e..3dee3d2b2f 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -79,8 +79,10 @@ module NamedDecl = Context.Named.Declaration
* STRUCT (params,oldsenv) : inside a local module, with
module parameters [params] and earlier environment [oldsenv]
* SIG (params,oldsenv) : same for a local module type
- - [modresolver] : delta_resolver concerning the module content
- - [paramresolver] : delta_resolver concerning the module parameters
+ - [modresolver] : delta_resolver concerning the module content, that needs to
+ be marshalled on disk
+ - [paramresolver] : delta_resolver in scope but not part of the library per
+ se, that is from functor parameters and required libraries
- [revstruct] : current module content, most recent declarations first
- [modlabels] and [objlabels] : names defined in the current module,
either for modules/modtypes or for constants/inductives.
@@ -1301,7 +1303,9 @@ let import lib cst vodigest senv =
mp,
{ senv with
env;
- modresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.modresolver;
+ (* Do NOT store the name quotient from the dependencies in the set of
+ constraints that will be marshalled on disk. *)
+ paramresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.paramresolver;
required = DPmap.add lib.comp_name vodigest senv.required;
loads = (mp,mb)::senv.loads;
sections;
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 28baa82666..76a1c190be 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -85,7 +85,7 @@ let make_labmap mp list =
let check_conv_error error why cst poly f env a1 a2 =
try
- let cst' = f env (Environ.universes env) a1 a2 in
+ let cst' = f env a1 a2 in
if poly then
if Constraint.is_empty cst' then cst
else error (IncompatiblePolymorphism (env, a1, a2))
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 87a5666fcc..d381e55dd6 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -111,7 +111,7 @@ val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
(** {6 Miscellaneous. } *)
(** Check that hyps are included in env and fails with error otherwise *)
-val check_hyps_inclusion : env -> ?evars:((existential->constr option) * UGraph.t) ->
+val check_hyps_inclusion : env -> ?evars:(existential->constr option) ->
GlobRef.t -> Constr.named_context -> unit
(** Types for primitives *)
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 52e93a9e22..096e458ec4 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -29,7 +29,12 @@ module G = AcyclicGraph.Make(struct
code (eg add_universe with a constraint vs G.add with no
constraint) *)
-type t = { graph: G.t; sprop_cumulative : bool }
+type t = {
+ graph: G.t;
+ sprop_cumulative : bool;
+ type_in_type : bool;
+}
+
type 'a check_function = t -> 'a -> 'a -> bool
let g_map f g =
@@ -39,6 +44,10 @@ let g_map f g =
let set_cumulative_sprop b g = {g with sprop_cumulative=b}
+let set_type_in_type b g = {g with type_in_type=b}
+
+let type_in_type g = g.type_in_type
+
let check_smaller_expr g (u,n) (v,m) =
let diff = n - m in
match diff with
@@ -55,28 +64,33 @@ let real_check_leq g u v =
Universe.for_all (fun ul -> exists_bigger g ul v) u
let check_leq g u v =
+ type_in_type g ||
Universe.equal u v || (g.sprop_cumulative && Universe.is_sprop u) ||
(not (Universe.is_sprop u) && not (Universe.is_sprop v) &&
(is_type0m_univ u ||
real_check_leq g u v))
let check_eq g u v =
+ type_in_type g ||
Universe.equal u v ||
(not (Universe.is_sprop u || Universe.is_sprop v) &&
(real_check_leq g u v && real_check_leq g v u))
let check_eq_level g u v =
u == v ||
+ type_in_type g ||
(not (Level.is_sprop u || Level.is_sprop v) && G.check_eq g.graph u v)
-let empty_universes = {graph=G.empty; sprop_cumulative=false}
+let empty_universes = {graph=G.empty; sprop_cumulative=false; type_in_type=false}
let initial_universes =
let big_rank = 1000000 in
let g = G.empty in
let g = G.add ~rank:big_rank Level.prop g in
let g = G.add ~rank:big_rank Level.set g in
- {graph=G.enforce_lt Level.prop Level.set g; sprop_cumulative=false}
+ {empty_universes with graph=G.enforce_lt Level.prop Level.set g}
+
+let initial_universes_with g = {g with graph=initial_universes.graph}
let enforce_constraint (u,d,v) g =
match d with
@@ -91,6 +105,10 @@ let enforce_constraint (u,d,v as cst) g =
| true, Le, false when g.sprop_cumulative -> g
| _ -> raise (UniverseInconsistency (d,Universe.make u, Universe.make v, None))
+let enforce_constraint cst g =
+ if not (type_in_type g) then enforce_constraint cst g
+ else try enforce_constraint cst g with UniverseInconsistency _ -> g
+
let merge_constraints csts g = Constraint.fold enforce_constraint csts g
let check_constraint g (u,d,v) =
@@ -103,8 +121,8 @@ let check_constraint g (u,d,v as cst) =
match Level.is_sprop u, d, Level.is_sprop v with
| false, _, false -> check_constraint g.graph cst
| true, (Eq|Le), true -> true
- | true, Le, false -> g.sprop_cumulative
- | _ -> false
+ | true, Le, false -> g.sprop_cumulative || type_in_type g
+ | _ -> type_in_type g
let check_constraints csts g = Constraint.for_all (check_constraint g) csts
@@ -145,8 +163,10 @@ let enforce_leq_alg u v g =
let enforce_leq_alg u v g =
match Universe.is_sprop u, Universe.is_sprop v with
| true, true -> Constraint.empty, g
- | true, false | false, true -> raise (UniverseInconsistency (Le, u, v, None))
| false, false -> enforce_leq_alg u v g
+ | left, _ ->
+ if left && g.sprop_cumulative then Constraint.empty, g
+ else raise (UniverseInconsistency (Le, u, v, None))
(* sanity check wrapper *)
let enforce_leq_alg u v g =
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index c9fbd7f694..87b3634e28 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -16,6 +16,15 @@ type t
val set_cumulative_sprop : bool -> t -> t
(** Makes the system incomplete. *)
+val set_type_in_type : bool -> t -> t
+
+(** When [type_in_type], functions adding constraints do not fail and
+ may instead ignore inconsistent constraints.
+
+ Checking functions such as [check_leq] always return [true].
+*)
+val type_in_type : t -> bool
+
type 'a check_function = t -> 'a -> 'a -> bool
val check_leq : Universe.t check_function
@@ -25,6 +34,9 @@ val check_eq_level : Level.t check_function
(** The initial graph of universes: Prop < Set *)
val initial_universes : t
+(** Initial universes, but keeping options such as type in type from the argument. *)
+val initial_universes_with : t -> t
+
(** Check equality of instances w.r.t. a universe graph *)
val check_eq_instances : Instance.t check_function
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 6d8aa02dff..a2fd14025e 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -205,12 +205,6 @@ module Level = struct
let pr u = str (to_string u)
- let apart u v =
- match data u, data v with
- | SProp, _ | _, SProp
- | Prop, Set | Set, Prop -> true
- | _ -> false
-
let vars = Array.init 20 (fun i -> make (Var i))
let var n =
@@ -250,7 +244,7 @@ module LMap = struct
ext empty
let pr f m =
- h 0 (prlist_with_sep fnl (fun (u, v) ->
+ h (prlist_with_sep fnl (fun (u, v) ->
Level.pr u ++ f v) (bindings m))
end
@@ -568,16 +562,6 @@ let constraint_type_ord c1 c2 = match c1, c2 with
| Eq, Eq -> 0
| Eq, _ -> 1
-(* Universe inconsistency: error raised when trying to enforce a relation
- that would create a cycle in the graph of universes. *)
-
-type univ_inconsistency = constraint_type * universe * universe * explanation Lazy.t option
-
-exception UniverseInconsistency of univ_inconsistency
-
-let error_inconsistency o u v p =
- raise (UniverseInconsistency (o,Universe.make u,Universe.make v,p))
-
(* Constraints and sets of constraints. *)
type univ_constraint = Level.t * constraint_type * Level.t
@@ -660,8 +644,6 @@ type 'a constraint_function = 'a -> 'a -> constraints -> constraints
let enforce_eq_level u v c =
(* We discard trivial constraints like u=u *)
if Level.equal u v then c
- else if Level.apart u v then
- error_inconsistency Eq u v None
else Constraint.add (u,Eq,v) c
let enforce_eq u v c =
@@ -684,9 +666,9 @@ let constraint_add_leq v u c =
let j = m - n in
if j = -1 (* n = m+1, v+1 <= u <-> v < u *) then
Constraint.add (x,Lt,y) c
- else if j <= -1 (* n = m+k, v+k <= u <-> v+(k-1) < u *) then
- if Level.equal x y then (* u+(k+1) <= u *)
- raise (UniverseInconsistency (Le, Universe.tip v, Universe.tip u, None))
+ else if j <= -1 (* n = m+k, v+k <= u and k>0 *) then
+ if Level.equal x y then (* u+k <= u with k>0 *)
+ Constraint.add (x,Lt,x) c
else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints.")
else if j = 0 then
Constraint.add (x,Le,y) c
@@ -703,8 +685,8 @@ let check_univ_leq u v =
let enforce_leq u v c =
match Universe.is_sprop u, Universe.is_sprop v with
| true, true -> c
- | true, false | false, true ->
- raise (UniverseInconsistency (Le, u, v, None))
+ | true, false -> Constraint.add (Level.sprop,Le,Level.prop) c
+ | false, true -> Constraint.add (Level.prop,Le,Level.sprop) c
| false, false ->
List.fold_left (fun c v -> (List.fold_left (fun c u -> constraint_add_leq u v c) c u)) c v
@@ -961,7 +943,7 @@ struct
let pr prl ?variance (univs, cst as ctx) =
if is_empty ctx then mt() else
- h 0 (Instance.pr prl ?variance univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
+ h (Instance.pr prl ?variance univs ++ str " |= ") ++ h (v 0 (Constraint.pr prl cst))
let hcons (univs, cst) =
(Instance.hcons univs, hcons_constraints cst)
@@ -1076,7 +1058,7 @@ struct
let pr prl (univs, cst as ctx) =
if is_empty ctx then mt() else
- h 0 (LSet.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
+ h (LSet.pr prl univs ++ str " |= ") ++ h (v 0 (Constraint.pr prl cst))
let constraints (_univs, cst) = cst
let levels (univs, _cst) = univs
@@ -1232,6 +1214,14 @@ let hcons_universe_context_set (v, c) =
let hcons_univ x = Universe.hcons x
+(* Universe inconsistency: error raised when trying to enforce a relation
+ that would create a cycle in the graph of universes. *)
+
+type univ_inconsistency = constraint_type * universe * universe * explanation Lazy.t option
+
+(* Do not use in this file as we may be type-in-type *)
+exception UniverseInconsistency of univ_inconsistency
+
let explain_universe_inconsistency prl (o,u,v,p : univ_inconsistency) =
let pr_uni = Universe.pr_with prl in
let pr_rel = function
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index cc2c2c0b4b..948195797e 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -211,5 +211,5 @@ let vm_conv cv_pb env t1 t2 =
else Constr.eq_constr_univs univs t1 t2
in
if not b then
- let univs = (univs, checked_universes) in
- let _ = vm_conv_gen cv_pb env univs t1 t2 in ()
+ let state = (univs, checked_universes) in
+ let _ = vm_conv_gen cv_pb env state t1 t2 in ()
diff --git a/kernel/vmbytecodes.ml b/kernel/vmbytecodes.ml
index 74405a0105..c156a21c86 100644
--- a/kernel/vmbytecodes.ml
+++ b/kernel/vmbytecodes.ml
@@ -106,14 +106,14 @@ let rec pp_instr i =
| Kclosure(lbl, n) ->
str "closure " ++ pp_lbl lbl ++ str ", " ++ int n
| Kclosurerec(fv,init,lblt,lblb) ->
- h 1 (str "closurerec " ++
+ hv 1 (str "closurerec " ++
int fv ++ str ", " ++ int init ++
str " types = " ++
prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
str " bodies = " ++
prlist_with_sep spc pp_lbl (Array.to_list lblb))
| Kclosurecofix (fv,init,lblt,lblb) ->
- h 1 (str "closurecofix " ++
+ hv 1 (str "closurecofix " ++
int fv ++ str ", " ++ int init ++
str " types = " ++
prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
@@ -129,7 +129,7 @@ let rec pp_instr i =
str "makeswitchblock " ++ pp_lbl lblt ++ str ", " ++
pp_lbl lbls ++ str ", " ++ int sz
| Kswitch(lblc,lblb) ->
- h 1 (str "switch " ++
+ hv 1 (str "switch " ++
prlist_with_sep spc pp_lbl (Array.to_list lblc) ++
str " | " ++
prlist_with_sep spc pp_lbl (Array.to_list lblb))
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 19:56:45 +0000