aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cClosure.ml37
-rw-r--r--kernel/cClosure.mli12
-rw-r--r--kernel/conv_oracle.ml3
-rw-r--r--kernel/conv_oracle.mli2
-rw-r--r--kernel/environ.ml20
-rw-r--r--kernel/kernel.mllib1
-rw-r--r--kernel/modops.ml3
-rw-r--r--kernel/modops.mli3
-rw-r--r--kernel/names.ml7
-rw-r--r--kernel/names.mli8
-rw-r--r--kernel/reduction.ml8
-rw-r--r--kernel/reduction.mli8
-rw-r--r--kernel/safe_typing.ml4
-rw-r--r--kernel/subtyping.ml6
-rw-r--r--kernel/transparentState.ml45
-rw-r--r--kernel/transparentState.mli34
-rw-r--r--kernel/uGraph.ml16
-rw-r--r--kernel/uGraph.mli2
-rw-r--r--kernel/univ.ml6
-rw-r--r--kernel/vconv.ml4
20 files changed, 151 insertions, 78 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 95546a83e1..7e73609996 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -72,11 +72,8 @@ let with_stats c =
end else
Lazy.force c
-let all_opaque = (Id.Pred.empty, Cpred.empty)
-let all_transparent = (Id.Pred.full, Cpred.full)
-
-let is_transparent_variable (ids, _) id = Id.Pred.mem id ids
-let is_transparent_constant (_, csts) cst = Cpred.mem cst csts
+let all_opaque = TransparentState.empty
+let all_transparent = TransparentState.full
module type RedFlagsSig = sig
type reds
@@ -93,8 +90,8 @@ module type RedFlagsSig = sig
val no_red : reds
val red_add : reds -> red_kind -> reds
val red_sub : reds -> red_kind -> reds
- val red_add_transparent : reds -> transparent_state -> reds
- val red_transparent : reds -> transparent_state
+ val red_add_transparent : reds -> TransparentState.t -> reds
+ val red_transparent : reds -> TransparentState.t
val mkflags : red_kind list -> reds
val red_set : reds -> red_kind -> bool
val red_projection : reds -> Projection.t -> bool
@@ -106,11 +103,13 @@ module RedFlags = (struct
(* [r_const=(false,cl)] means only those in [cl] *)
(* [r_delta=true] just mean [r_const=(true,[])] *)
+ open TransparentState
+
type reds = {
r_beta : bool;
r_delta : bool;
r_eta : bool;
- r_const : transparent_state;
+ r_const : TransparentState.t;
r_zeta : bool;
r_match : bool;
r_fix : bool;
@@ -143,30 +142,30 @@ module RedFlags = (struct
| ETA -> { red with r_eta = true }
| DELTA -> { red with r_delta = true; r_const = all_transparent }
| CONST kn ->
- let (l1,l2) = red.r_const in
- { red with r_const = l1, Cpred.add kn l2 }
+ let r = red.r_const in
+ { red with r_const = { r with tr_cst = Cpred.add kn r.tr_cst } }
| MATCH -> { red with r_match = true }
| FIX -> { red with r_fix = true }
| COFIX -> { red with r_cofix = true }
| ZETA -> { red with r_zeta = true }
| VAR id ->
- let (l1,l2) = red.r_const in
- { red with r_const = Id.Pred.add id l1, l2 }
+ let r = red.r_const in
+ { red with r_const = { r with tr_var = Id.Pred.add id r.tr_var } }
let red_sub red = function
| BETA -> { red with r_beta = false }
| ETA -> { red with r_eta = false }
| DELTA -> { red with r_delta = false }
| CONST kn ->
- let (l1,l2) = red.r_const in
- { red with r_const = l1, Cpred.remove kn l2 }
+ let r = red.r_const in
+ { red with r_const = { r with tr_cst = Cpred.remove kn r.tr_cst } }
| MATCH -> { red with r_match = false }
| FIX -> { red with r_fix = false }
| COFIX -> { red with r_cofix = false }
| ZETA -> { red with r_zeta = false }
| VAR id ->
- let (l1,l2) = red.r_const in
- { red with r_const = Id.Pred.remove id l1, l2 }
+ let r = red.r_const in
+ { red with r_const = { r with tr_var = Id.Pred.remove id r.tr_var } }
let red_transparent red = red.r_const
@@ -179,12 +178,10 @@ module RedFlags = (struct
| BETA -> incr_cnt red.r_beta beta
| ETA -> incr_cnt red.r_eta eta
| CONST kn ->
- let (_,l) = red.r_const in
- let c = Cpred.mem kn l in
+ let c = is_transparent_constant red.r_const kn in
incr_cnt c delta
| VAR id -> (* En attendant d'avoir des kn pour les Var *)
- let (l,_) = red.r_const in
- let c = Id.Pred.mem id l in
+ let c = is_transparent_variable red.r_const id in
incr_cnt c delta
| ZETA -> incr_cnt red.r_zeta zeta
| MATCH -> incr_cnt red.r_match nb_match
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 1ee4bccc25..b6c87b3732 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -24,14 +24,6 @@ val with_stats: 'a Lazy.t -> 'a
Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of
a LetIn expression is Letin reduction *)
-
-
-val all_opaque : transparent_state
-val all_transparent : transparent_state
-
-val is_transparent_variable : transparent_state -> variable -> bool
-val is_transparent_constant : transparent_state -> Constant.t -> bool
-
(** Sets of reduction kinds. *)
module type RedFlagsSig = sig
type reds
@@ -60,10 +52,10 @@ module type RedFlagsSig = sig
val red_sub : reds -> red_kind -> reds
(** Adds a reduction kind to a set *)
- val red_add_transparent : reds -> transparent_state -> reds
+ val red_add_transparent : reds -> TransparentState.t -> reds
(** Retrieve the transparent state of the reduction flags *)
- val red_transparent : reds -> transparent_state
+ val red_transparent : reds -> TransparentState.t
(** Build a reduction set from scratch = iter [red_add] on [no_red] *)
val mkflags : red_kind list -> reds
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index ac78064235..fe82353b70 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -81,7 +81,8 @@ let fold_strategy f { var_opacity; cst_opacity; _ } accu =
let accu = Id.Map.fold fvar var_opacity accu in
Cmap.fold fcst cst_opacity accu
-let get_transp_state { var_trstate; cst_trstate; _ } = (var_trstate, cst_trstate)
+let get_transp_state { var_trstate; cst_trstate; _ } =
+ { TransparentState.tr_var = var_trstate; tr_cst = cst_trstate }
let dep_order l2r k1 k2 = match k1, k2 with
| RelKey _, RelKey _ -> l2r
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 67add5dd35..bc06cc21b6 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -41,5 +41,5 @@ val set_strategy : oracle -> Constant.t tableKey -> level -> oracle
(** Fold over the non-transparent levels of the oracle. Order unspecified. *)
val fold_strategy : (Constant.t tableKey -> level -> 'a -> 'a) -> oracle -> 'a -> 'a
-val get_transp_state : oracle -> transparent_state
+val get_transp_state : oracle -> TransparentState.t
diff --git a/kernel/environ.ml b/kernel/environ.ml
index f61dd0c101..019c0a6819 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -384,8 +384,26 @@ let set_engagement c env = (* Unsafe *)
{ env with env_stratification =
{ env.env_stratification with env_engagement = c } }
+(* It's convenient to use [{flags with foo = bar}] so we're smart wrt to it. *)
+let same_flags {
+ check_guarded;
+ check_universes;
+ conv_oracle;
+ share_reduction;
+ enable_VM;
+ enable_native_compiler;
+ } alt =
+ check_guarded == alt.check_guarded &&
+ check_universes == alt.check_universes &&
+ conv_oracle == alt.conv_oracle &&
+ share_reduction == alt.share_reduction &&
+ enable_VM == alt.enable_VM &&
+ enable_native_compiler == alt.enable_native_compiler
+[@warning "+9"]
+
let set_typing_flags c env = (* Unsafe *)
- { env with env_typing_flags = c }
+ if same_flags env.env_typing_flags c then env
+ else { env with env_typing_flags = c }
(* Global constants *)
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index a18c5d1e20..54c239349d 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -1,4 +1,5 @@
Names
+TransparentState
Uint31
Univ
UGraph
diff --git a/kernel/modops.ml b/kernel/modops.ml
index bab2eae3df..0dde1c7e75 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -47,10 +47,9 @@ type signature_mismatch_error =
| RecordFieldExpected of bool
| RecordProjectionsExpected of Name.t list
| NotEqualInductiveAliases
- | IncompatibleInstances
| IncompatibleUniverses of Univ.univ_inconsistency
| IncompatiblePolymorphism of env * types * types
- | IncompatibleConstraints of Univ.AUContext.t
+ | IncompatibleConstraints of { got : Univ.AUContext.t; expect : Univ.AUContext.t }
type module_typing_error =
| SignatureMismatch of
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 8e7e618fcd..0acd09fb12 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -106,10 +106,9 @@ type signature_mismatch_error =
| RecordFieldExpected of bool
| RecordProjectionsExpected of Name.t list
| NotEqualInductiveAliases
- | IncompatibleInstances
| IncompatibleUniverses of Univ.univ_inconsistency
| IncompatiblePolymorphism of env * types * types
- | IncompatibleConstraints of Univ.AUContext.t
+ | IncompatibleConstraints of { got : Univ.AUContext.t; expect : Univ.AUContext.t }
type module_typing_error =
| SignatureMismatch of
diff --git a/kernel/names.ml b/kernel/names.ml
index 18560d5f8d..b2d6a489a6 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -715,13 +715,6 @@ let hcons_construct = Hashcons.simple_hcons Hconstruct.generate Hconstruct.hcons
(*****************)
-type transparent_state = Id.Pred.t * Cpred.t
-
-let empty_transparent_state = (Id.Pred.empty, Cpred.empty)
-let full_transparent_state = (Id.Pred.full, Cpred.full)
-let var_full_transparent_state = (Id.Pred.full, Cpred.empty)
-let cst_full_transparent_state = (Id.Pred.empty, Cpred.full)
-
type 'a tableKey =
| ConstKey of 'a
| VarKey of Id.t
diff --git a/kernel/names.mli b/kernel/names.mli
index 98995752a2..350db871d5 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -510,14 +510,6 @@ type 'a tableKey =
| VarKey of Id.t
| RelKey of Int.t
-(** Sets of names *)
-type transparent_state = Id.Pred.t * Cpred.t
-
-val empty_transparent_state : transparent_state
-val full_transparent_state : transparent_state
-val var_full_transparent_state : transparent_state
-val cst_full_transparent_state : transparent_state
-
type inv_rel_key = int (** index in the [rel_context] part of environment
starting by the end, {e inverse}
of de Bruijn indice *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 5515ff9767..fbb481424f 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -177,7 +177,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:Names.transparent_state -> env ->
+ ?l2r:bool -> ?reds:TransparentState.t -> env ->
?evars:((existential->constr option) * UGraph.t) ->
'a -> 'a -> unit
@@ -758,7 +758,7 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 =
()
(* Profiling *)
-let gen_conv cv_pb ?(l2r=false) ?(reds=full_transparent_state) env ?(evars=(fun _->None), universes env) =
+let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _->None), universes env) =
let evars, univs = evars in
if Flags.profile then
let fconv_universes_key = CProfile.declare_profile "trans_fconv_universes" in
@@ -792,11 +792,11 @@ let infer_conv_universes =
CProfile.profile8 infer_conv_universes_key infer_conv_universes
else infer_conv_universes
-let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_state)
+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
-let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_state)
+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
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 581e8bd88a..0408dbf057 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -31,7 +31,7 @@ exception NotConvertibleVect of int
type 'a kernel_conversion_function = env -> 'a -> 'a -> unit
type 'a extended_conversion_function =
- ?l2r:bool -> ?reds:Names.transparent_state -> env ->
+ ?l2r:bool -> ?reds:TransparentState.t -> env ->
?evars:((existential->constr option) * UGraph.t) ->
'a -> 'a -> unit
@@ -77,15 +77,15 @@ val conv_leq : types extended_conversion_function
(** These conversion functions are used by module subtyping, which needs to infer
universe constraints inside the kernel *)
val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) ->
- ?ts:Names.transparent_state -> constr infer_conversion_function
+ ?ts:TransparentState.t -> constr infer_conversion_function
val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) ->
- ?ts:Names.transparent_state -> types infer_conversion_function
+ ?ts:TransparentState.t -> types infer_conversion_function
(** Depending on the universe state functions, this might raise
[UniverseInconsistency] in addition to [NotConvertible] (for better error
messages). *)
val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) ->
- Names.transparent_state -> (constr,'a) generic_conversion_function
+ TransparentState.t -> (constr,'a) generic_conversion_function
val default_conv : conv_pb -> ?l2r:bool -> types kernel_conversion_function
val default_conv_leq : ?l2r:bool -> types kernel_conversion_function
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index df10398b2f..2464df799e 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -192,7 +192,9 @@ let set_engagement c senv =
engagement = Some c }
let set_typing_flags c senv =
- { senv with env = Environ.set_typing_flags c senv.env }
+ let env = Environ.set_typing_flags c senv.env in
+ if env == senv.env then senv
+ else { senv with env }
let set_share_reduction b senv =
let flags = Environ.typing_flags senv.env in
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index d64342dbb0..347c30dd64 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -93,10 +93,8 @@ let check_conv_error error why cst poly f env a1 a2 =
| Univ.UniverseInconsistency e -> error (IncompatibleUniverses e)
let check_polymorphic_instance error env auctx1 auctx2 =
- if not (Univ.AUContext.size auctx1 == Univ.AUContext.size auctx2) then
- error IncompatibleInstances
- else if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then
- error (IncompatibleConstraints auctx1)
+ if not (UGraph.check_subtype (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/transparentState.ml b/kernel/transparentState.ml
new file mode 100644
index 0000000000..9661dace6a
--- /dev/null
+++ b/kernel/transparentState.ml
@@ -0,0 +1,45 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <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) *)
+(************************************************************************)
+
+open Names
+
+type t = {
+ tr_var : Id.Pred.t;
+ tr_cst : Cpred.t;
+}
+
+let empty = {
+ tr_var = Id.Pred.empty;
+ tr_cst = Cpred.empty;
+}
+
+let full = {
+ tr_var = Id.Pred.full;
+ tr_cst = Cpred.full;
+}
+
+let var_full = {
+ tr_var = Id.Pred.full;
+ tr_cst = Cpred.empty;
+}
+
+let cst_full = {
+ tr_var = Id.Pred.empty;
+ tr_cst = Cpred.full;
+}
+
+let is_empty ts =
+ Id.Pred.is_empty ts.tr_var && Cpred.is_empty ts.tr_cst
+
+let is_transparent_variable ts id =
+ Id.Pred.mem id ts.tr_var
+
+let is_transparent_constant ts cst =
+ Cpred.mem cst ts.tr_cst
diff --git a/kernel/transparentState.mli b/kernel/transparentState.mli
new file mode 100644
index 0000000000..f2999c6869
--- /dev/null
+++ b/kernel/transparentState.mli
@@ -0,0 +1,34 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <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) *)
+(************************************************************************)
+
+open Names
+
+(** Sets of names *)
+type t = {
+ tr_var : Id.Pred.t;
+ tr_cst : Cpred.t;
+}
+
+val empty : t
+(** Everything opaque *)
+
+val full : t
+(** Everything transparent *)
+
+val var_full : t
+(** All variables transparent *)
+
+val cst_full : t
+(** All constant transparent *)
+
+val is_empty : t -> bool
+
+val is_transparent_variable : t -> Id.t -> bool
+val is_transparent_constant : t -> Constant.t -> bool
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 9ff51fca55..9083156745 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -942,34 +942,36 @@ let check_eq_instances g t1 t2 =
(** Pretty-printing *)
+let pr_umap sep pr map =
+ let cmp (u,_) (v,_) = Level.compare u v in
+ Pp.prlist_with_sep sep pr (List.sort cmp (UMap.bindings map))
+
let pr_arc prl = function
| _, Canonical {univ=u; ltle; _} ->
if UMap.is_empty ltle then mt ()
else
prl u ++ str " " ++
v 0
- (pr_sequence (fun (v, strict) ->
+ (pr_umap Pp.spc (fun (v, strict) ->
(if strict then str "< " else str "<= ") ++ prl v)
- (UMap.bindings ltle)) ++
+ ltle) ++
fnl ()
| u, Equiv v ->
prl u ++ str " = " ++ prl v ++ fnl ()
let pr_universes prl g =
- let graph = UMap.fold (fun u a l -> (u,a)::l) g.entries [] in
- prlist (pr_arc prl) graph
+ pr_umap mt (pr_arc prl) g.entries
(* Dumping constraints to a file *)
let dump_universes output g =
let dump_arc u = function
| Canonical {univ=u; ltle; _} ->
- let u_str = Level.to_string u in
UMap.iter (fun v strict ->
let typ = if strict then Lt else Le in
- output typ u_str (Level.to_string v)) ltle;
+ output typ u v) ltle;
| Equiv v ->
- output Eq (Level.to_string u) (Level.to_string v)
+ output Eq u v
in
UMap.iter dump_arc g.entries
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 4336a22b8c..a2cc5b3116 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -86,7 +86,7 @@ val check_subtype : AUContext.t check_function
(** {6 Dumping to a file } *)
val dump_universes :
- (constraint_type -> string -> string -> unit) -> t -> unit
+ (constraint_type -> Level.t -> Level.t -> unit) -> t -> unit
(** {6 Debugging} *)
val check_universes_invariants : t -> unit
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 0edf750997..2b3b4f9486 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -570,9 +570,9 @@ struct
include S
let pr prl c =
- fold (fun (u1,op,u2) pp_std ->
- pp_std ++ prl u1 ++ pr_constraint_type op ++
- prl u2 ++ fnl () ) c (str "")
+ v 0 (prlist_with_sep spc (fun (u1,op,u2) ->
+ hov 0 (prl u1 ++ pr_constraint_type op ++ prl u2))
+ (elements c))
end
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index c1130e62c9..246c90c09d 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -191,7 +191,7 @@ let warn_bytecode_compiler_failed =
let vm_conv_gen cv_pb env univs t1 t2 =
if not (typing_flags env).Declarations.enable_VM then
Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
- full_transparent_state env univs t1 t2
+ TransparentState.full env univs t1 t2
else
try
let v1 = val_of_constr env t1 in
@@ -200,7 +200,7 @@ let vm_conv_gen cv_pb env univs t1 t2 =
with Not_found | Invalid_argument _ ->
warn_bytecode_compiler_failed ();
Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
- full_transparent_state env univs t1 t2
+ TransparentState.full env univs t1 t2
let vm_conv cv_pb env t1 t2 =
let univs = Environ.universes env in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 13:37:04 +0000