diff options
Diffstat (limited to 'kernel')
33 files changed, 331 insertions, 190 deletions
diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml index 314cb54d1d..5cd91b4e74 100644 --- a/kernel/cPrimitives.ml +++ b/kernel/cPrimitives.ml @@ -58,7 +58,6 @@ type t = | Arraydefault | Arrayset | Arraycopy - | Arrayreroot | Arraylength let parse = function @@ -110,7 +109,6 @@ let parse = function | "array_set" -> Arrayset | "array_length" -> Arraylength | "array_copy" -> Arraycopy - | "array_reroot" -> Arrayreroot | _ -> raise Not_found let equal (p1 : t) (p2 : t) = @@ -164,8 +162,7 @@ let hash = function | Arraydefault -> 45 | Arrayset -> 46 | Arraycopy -> 47 - | Arrayreroot -> 48 - | Arraylength -> 49 + | Arraylength -> 48 (* Should match names in nativevalues.ml *) let to_string = function @@ -216,7 +213,6 @@ let to_string = function | Arraydefault -> "arraydefault" | Arrayset -> "arrayset" | Arraycopy -> "arraycopy" - | Arrayreroot -> "arrayreroot" | Arraylength -> "arraylength" type const = @@ -302,7 +298,6 @@ let types = | Arraydefault -> [array_ty; PITT_param 1] | Arrayset -> [array_ty; int_ty; PITT_param 1; array_ty] | Arraycopy -> [array_ty; array_ty] - | Arrayreroot -> [array_ty; array_ty] | Arraylength -> [array_ty; int_ty] let one_param = @@ -360,7 +355,6 @@ let params = function | Arraydefault | Arrayset | Arraycopy - | Arrayreroot | Arraylength -> one_param let nparams x = List.length (params x) @@ -414,7 +408,6 @@ let univs = function | Arraydefault | Arrayset | Arraycopy - | Arrayreroot | Arraylength -> one_univ type arg_kind = diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index 41b3bff465..0db643faf4 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -56,7 +56,6 @@ type t = | Arraydefault | Arrayset | Arraycopy - | Arrayreroot | Arraylength (** Can raise [Not_found]. 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/nativevalues.ml b/kernel/nativevalues.ml index 9e17f97a56..05c98e4b87 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -739,15 +739,6 @@ let arraycopy accu vA t = no_check_arraycopy t else accu vA t -let no_check_arrayreroot t = - of_parray (Parray.reroot (to_parray t)) -[@@ocaml.inline always] - -let arrayreroot accu vA t = - if is_parray t then - no_check_arrayreroot t - else accu vA t - let no_check_arraylength t = mk_uint (Parray.length (to_parray t)) [@@ocaml.inline always] diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 08c5bd7126..b9b75a9d7c 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -344,7 +344,6 @@ val arrayget : t -> t -> t -> t -> t (* accu A t n *) val arraydefault : t -> t -> t (* accu A t *) val arrayset : t -> t -> t -> t -> t -> t (* accu A t n v *) val arraycopy : t -> t -> t -> t (* accu A t *) -val arrayreroot : t -> t -> t -> t (* accu A t *) val arraylength : t -> t -> t -> t (* accu A t *) val arrayinit : t -> t -> t -> t (* accu A n f def *) val arraymap : t -> t -> t (* accu A B f t *) @@ -364,8 +363,5 @@ val no_check_arrayset : t -> t -> t -> t val no_check_arraycopy : t -> t [@@ocaml.inline always] -val no_check_arrayreroot : t -> t -[@@ocaml.inline always] - val no_check_arraylength : t -> t [@@ocaml.inline always] diff --git a/kernel/parray.ml b/kernel/parray.ml index ea314c1883..0953f4b33f 100644 --- a/kernel/parray.ml +++ b/kernel/parray.ml @@ -27,45 +27,52 @@ and 'a kind = let unsafe_of_array t def = ref (Array (t,def)) let of_array t def = unsafe_of_array (Array.copy t) def -let rec length_int p = - match !p with - | Array (t,_) -> Array.length t - | Updated (_, _, p) -> length_int p +let rec rerootk t k = + match !t with + | Array (a, _) -> k a + | Updated (i, v, p) -> + let k' a = + let v' = Array.unsafe_get a i in + Array.unsafe_set a i v; + t := !p; (* i.e., Array (a, def) *) + p := Updated (i, v', t); + k a in + rerootk p k' + +let reroot t = rerootk t (fun a -> a) + +let length_int p = + Array.length (reroot p) let length p = Uint63.of_int @@ length_int p -let rec get p n = - match !p with - | Array (t,def) -> - let l = Array.length t in - if Uint63.le Uint63.zero n && Uint63.lt n (Uint63.of_int l) then - Array.unsafe_get t (length_to_int n) - else def - | Updated (k,e,p) -> - if Uint63.equal n (Uint63.of_int k) then e - else get p n +let get p n = + let t = reroot p in + let l = Array.length t in + if Uint63.le Uint63.zero n && Uint63.lt n (Uint63.of_int l) then + Array.unsafe_get t (length_to_int n) + else + match !p with + | Array (_, def) -> def + | Updated _ -> assert false let set p n e = - let kind = !p in - match kind with - | Array (t,_) -> - let l = Uint63.of_int @@ Array.length t in - if Uint63.le Uint63.zero n && Uint63.lt n l then - let res = ref kind in - let n = length_to_int n in - p := Updated (n, Array.unsafe_get t n, res); - Array.unsafe_set t n e; - res - else p - | Updated _ -> - if Uint63.le Uint63.zero n && Uint63.lt n (length p) then - ref (Updated((length_to_int n), e, p)) - else p - -let rec default p = + let a = reroot p in + let l = Uint63.of_int (Array.length a) in + if Uint63.le Uint63.zero n && Uint63.lt n l then + let i = length_to_int n in + let v' = Array.unsafe_get a i in + Array.unsafe_set a i e; + let t = ref !p in (* i.e., Array (a, def) *) + p := Updated (i, v', t); + t + else p + +let default p = + let _ = reroot p in match !p with | Array (_,def) -> def - | Updated (_,_,p) -> default p + | Updated _ -> assert false let make n def = ref (Array (Array.make (trunc_size n) def, def)) @@ -75,33 +82,19 @@ let init n f def = let t = Array.init n f in ref (Array (t, def)) -let rec to_array p = +let to_array p = + let _ = reroot p in match !p with | Array (t,def) -> Array.copy t, def - | Updated (n,e,p) -> - let (t,_) as r = to_array p in - Array.unsafe_set t n e; r + | Updated _ -> assert false let copy p = let (t,def) = to_array p in ref (Array (t,def)) -let rec rerootk t k = - match !t with - | Array _ -> k () - | Updated (i, v, t') -> - let k' () = - begin match !t' with - | Array (a,_def) as n -> - let v' = a.(i) in - Array.unsafe_set a i v; - t := n; - t' := Updated (i, v', t) - | Updated _ -> assert false - end; k() in - rerootk t' k' - -let reroot t = rerootk t (fun () -> t) +let reroot t = + let _ = reroot t in + t let map f p = let p = reroot p in diff --git a/kernel/parray.mli b/kernel/parray.mli index 0276278bd0..8b6565c159 100644 --- a/kernel/parray.mli +++ b/kernel/parray.mli @@ -19,7 +19,6 @@ val default : 'a t -> 'a val make : Uint63.t -> 'a -> 'a t val init : Uint63.t -> (int -> 'a) -> 'a -> 'a t val copy : 'a t -> 'a t -val reroot : 'a t -> 'a t val map : ('a -> 'b) -> 'a t -> 'b t diff --git a/kernel/primred.ml b/kernel/primred.ml index 90eeeb9be7..f158cfacea 100644 --- a/kernel/primred.ml +++ b/kernel/primred.ml @@ -365,11 +365,6 @@ struct let t = get_parray evd args 1 in let t' = Parray.copy t in E.mkArray env u t' ty - | Arrayreroot -> - let ar = E.get args 1 in - let t = E.get_parray evd ar in - let _ = Parray.reroot t in - ar | Arraylength -> let t = get_parray evd args 1 in E.mkInt env (Parray.length t) 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)) diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml index 375b1aface..16a0f42664 100644 --- a/kernel/vmbytegen.ml +++ b/kernel/vmbytegen.ml @@ -508,7 +508,6 @@ let is_caml_prim = let open CPrimitives in function | Arraydefault | Arrayset | Arraycopy - | Arrayreroot | Arraylength -> true | _ -> false diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml index f913cb906c..ec8601edc9 100644 --- a/kernel/vmemitcodes.ml +++ b/kernel/vmemitcodes.ml @@ -262,7 +262,7 @@ let check_prim_op = function | Arraymake -> opISINT_CAML_CALL2 | Arrayget -> opISARRAY_INT_CAML_CALL2 | Arrayset -> opISARRAY_INT_CAML_CALL3 - | Arraydefault | Arraycopy | Arrayreroot | Arraylength -> + | Arraydefault | Arraycopy | Arraylength -> opISARRAY_CAML_CALL1 let emit_instr env = function diff --git a/kernel/vmsymtable.ml b/kernel/vmsymtable.ml index 4ad830a298..9d80dc578b 100644 --- a/kernel/vmsymtable.ml +++ b/kernel/vmsymtable.ml @@ -69,7 +69,6 @@ let parray_get = set_global Vmvalues.parray_get let parray_get_default = set_global Vmvalues.parray_get_default let parray_set = set_global Vmvalues.parray_set let parray_copy = set_global Vmvalues.parray_copy -let parray_reroot = set_global Vmvalues.parray_reroot let parray_length = set_global Vmvalues.parray_length (* table pour les structured_constant et les annotations des switchs *) @@ -135,7 +134,6 @@ let slot_for_caml_prim = | Arraydefault -> parray_get_default | Arrayset -> parray_set | Arraycopy -> parray_copy - | Arrayreroot -> parray_reroot | Arraylength -> parray_length | _ -> assert false diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 0678f37a0b..2068133b10 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -700,5 +700,4 @@ let parray_get = Obj.magic Parray.get let parray_get_default = Obj.magic Parray.default let parray_set = Obj.magic Parray.set let parray_copy = Obj.magic Parray.copy -let parray_reroot = Obj.magic Parray.reroot let parray_length = Obj.magic Parray.length diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index 6632dc46b2..d15595766a 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -204,5 +204,4 @@ val parray_get : values val parray_get_default : values val parray_set : values val parray_copy : values -val parray_reroot : values val parray_length : values |