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/constr.ml72
-rw-r--r--kernel/constr.mli11
-rw-r--r--kernel/conv_oracle.ml3
-rw-r--r--kernel/conv_oracle.mli2
-rw-r--r--kernel/entries.ml6
-rw-r--r--kernel/environ.ml20
-rw-r--r--kernel/indtypes.ml14
-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.ml24
-rw-r--r--kernel/subtyping.ml6
-rw-r--r--kernel/term_typing.ml10
-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.ml53
-rw-r--r--kernel/univ.mli10
-rw-r--r--kernel/vars.ml17
-rw-r--r--kernel/vconv.ml4
27 files changed, 285 insertions, 151 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/constr.ml b/kernel/constr.ml
index 704e6de6b8..8e5d15dd2d 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -452,27 +452,6 @@ let fold f acc c = match kind c with
| CoFix (_,(_lna,tl,bl)) ->
Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
-let fold_with_full_binders g f n acc c =
- let open Context.Rel.Declaration in
- match kind c with
- | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ -> acc
- | Cast (c,_, t) -> f n (f n acc c) t
- | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
- | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
- | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c
- | App (c,l) -> Array.fold_left (f n) (f n acc c) l
- | Proj (_,c) -> f n acc c
- | Evar (_,l) -> Array.fold_left (f n) acc l
- | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
- | Fix (_,(lna,tl,bl)) ->
- let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in
- let fd = Array.map2 (fun t b -> (t,b)) tl bl in
- Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
- | CoFix (_,(lna,tl,bl)) ->
- let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in
- let fd = Array.map2 (fun t b -> (t,b)) tl bl in
- Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
-
(* [iter f c] iters [f] on the immediate subterms of [c]; it is
not recursive and the order with which subterms are processed is
not specified *)
@@ -534,12 +513,12 @@ let fold_constr_with_binders g f n acc c =
| Proj (_p,c) -> f n acc c
| Evar (_,l) -> Array.fold_left (f n) acc l
| Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
- | Fix (_,(lna,tl,bl)) ->
- let n' = CArray.fold_left2 (fun c _n _t -> g c) n lna tl in
+ | Fix (_,(_,tl,bl)) ->
+ let n' = iterate g (Array.length tl) n in
let fd = Array.map2 (fun t b -> (t,b)) tl bl in
Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
- | CoFix (_,(lna,tl,bl)) ->
- let n' = CArray.fold_left2 (fun c _n _t -> g c) n lna tl in
+ | CoFix (_,(_,tl,bl)) ->
+ let n' = iterate g (Array.length tl) n in
let fd = Array.map2 (fun t b -> (t,b)) tl bl in
Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
@@ -799,6 +778,49 @@ let map_with_binders g f l c0 = match kind c0 with
let bl' = Array.Fun1.Smart.map f l' bl in
mkCoFix (ln,(lna,tl',bl'))
+(*********************)
+(* Lifting *)
+(*********************)
+
+(* The generic lifting function *)
+let rec exliftn el c =
+ let open Esubst in
+ match kind c with
+ | Rel i -> mkRel(reloc_rel i el)
+ | _ -> map_with_binders el_lift exliftn el c
+
+(* Lifting the binding depth across k bindings *)
+
+let liftn n k c =
+ let open Esubst in
+ match el_liftn (pred k) (el_shft n el_id) with
+ | ELID -> c
+ | el -> exliftn el c
+
+let lift n = liftn n 1
+
+let fold_with_full_binders g f n acc c =
+ let open Context.Rel.Declaration in
+ match kind c with
+ | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ -> acc
+ | Cast (c,_, t) -> f n (f n acc c) t
+ | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
+ | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
+ | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c
+ | App (c,l) -> Array.fold_left (f n) (f n acc c) l
+ | Proj (_,c) -> f n acc c
+ | Evar (_,l) -> Array.fold_left (f n) acc l
+ | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
+ | Fix (_,(lna,tl,bl)) ->
+ let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
+ let fd = Array.map2 (fun t b -> (t,b)) tl bl in
+ Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+ | CoFix (_,(lna,tl,bl)) ->
+ let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
+ let fd = Array.map2 (fun t b -> (t,b)) tl bl in
+ Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+
+
type 'univs instance_compare_fn = GlobRef.t -> int ->
'univs -> 'univs -> bool
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 1be1f63ff7..f2cedcdabb 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -383,6 +383,17 @@ type rel_context = rel_declaration list
type named_context = named_declaration list
type compacted_context = compacted_declaration list
+(** {6 Relocation and substitution } *)
+
+(** [exliftn el c] lifts [c] with lifting [el] *)
+val exliftn : Esubst.lift -> constr -> constr
+
+(** [liftn n k c] lifts by [n] indexes above or equal to [k] in [c] *)
+val liftn : int -> int -> constr -> constr
+
+(** [lift n c] lifts by [n] the positive indexes in [c] *)
+val lift : int -> constr -> constr
+
(** {6 Functionals working on expressions canonically abstracted over
a local context (possibly with let-ins)} *)
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/entries.ml b/kernel/entries.ml
index c5bcd74072..58bb782f15 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -30,8 +30,8 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1];
type inductive_universes =
| Monomorphic_ind_entry of Univ.ContextSet.t
- | Polymorphic_ind_entry of Univ.UContext.t
- | Cumulative_ind_entry of Univ.CumulativityInfo.t
+ | Polymorphic_ind_entry of Name.t array * Univ.UContext.t
+ | Cumulative_ind_entry of Name.t array * Univ.CumulativityInfo.t
type one_inductive_entry = {
mind_entry_typename : Id.t;
@@ -60,7 +60,7 @@ type 'a const_entry_body = 'a proof_output Future.computation
type constant_universes_entry =
| Monomorphic_const_entry of Univ.ContextSet.t
- | Polymorphic_const_entry of Univ.UContext.t
+ | Polymorphic_const_entry of Name.t array * Univ.UContext.t
type 'a in_constant_universes_entry = 'a * constant_universes_entry
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/indtypes.ml b/kernel/indtypes.ml
index 0346026aa4..20c90bc05a 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -268,8 +268,8 @@ let typecheck_inductive env mie =
let env' =
match mie.mind_entry_universes with
| Monomorphic_ind_entry ctx -> push_context_set ctx env
- | Polymorphic_ind_entry ctx -> push_context ctx env
- | Cumulative_ind_entry cumi -> push_context (Univ.CumulativityInfo.univ_context cumi) env
+ | Polymorphic_ind_entry (_, ctx) -> push_context ctx env
+ | Cumulative_ind_entry (_, cumi) -> push_context (Univ.CumulativityInfo.univ_context cumi) env
in
let env_params = check_context env' mie.mind_entry_params in
let paramsctxt = mie.mind_entry_params in
@@ -407,7 +407,7 @@ let typecheck_inductive env mie =
match mie.mind_entry_universes with
| Monomorphic_ind_entry _ -> ()
| Polymorphic_ind_entry _ -> ()
- | Cumulative_ind_entry cumi -> check_subtyping cumi paramsctxt env_arities inds
+ | Cumulative_ind_entry (_, cumi) -> check_subtyping cumi paramsctxt env_arities inds
in (env_arities, env_ar_par, paramsctxt, inds)
(************************************************************************)
@@ -851,12 +851,12 @@ let compute_projections (kn, i as ind) mib =
let abstract_inductive_universes iu =
match iu with
| Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx)
- | Polymorphic_ind_entry ctx ->
- let (inst, auctx) = Univ.abstract_universes ctx in
+ | Polymorphic_ind_entry (nas, ctx) ->
+ let (inst, auctx) = Univ.abstract_universes nas ctx in
let inst = Univ.make_instance_subst inst in
(inst, Polymorphic_ind auctx)
- | Cumulative_ind_entry cumi ->
- let (inst, acumi) = Univ.abstract_cumulativity_info cumi in
+ | Cumulative_ind_entry (nas, cumi) ->
+ let (inst, acumi) = Univ.abstract_cumulativity_info nas cumi in
let inst = Univ.make_instance_subst inst in
(inst, Cumulative_ind acumi)
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 8b11851bbb..83d890b628 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
@@ -496,7 +498,7 @@ type generic_name =
| M (** name already known, cf the mod_mp field *)
| MT (** name already known, cf the mod_mp field *)
-let add_field ((l,sfb) as field) gn senv =
+let add_field ?(is_include=false) ((l,sfb) as field) gn senv =
let mlabs,olabs = match sfb with
| SFBmind mib ->
let l = labels_of_mib mib in
@@ -506,8 +508,18 @@ let add_field ((l,sfb) as field) gn senv =
| SFBmodule _ | SFBmodtype _ ->
check_modlabel l senv; (Label.Set.singleton l, Label.Set.empty)
in
- let cst = constraints_of_sfb senv.env sfb in
- let senv = add_constraints_list cst senv in
+ let senv =
+ if is_include then
+ (* Universes and constraints were added when the included module
+ was defined eg in [Include F X.] (one of the trickier
+ versions of Include) the constraints on the fields are
+ exactly those of the fields of F which was defined
+ separately. *)
+ senv
+ else
+ let cst = constraints_of_sfb senv.env sfb in
+ add_constraints_list cst senv
+ in
let env' = match sfb, gn with
| SFBconst cb, C con -> Environ.add_constant con cb senv.env
| SFBmind mib, I mind -> Environ.add_mind mind mib senv.env
@@ -682,7 +694,7 @@ let constant_entry_of_side_effect cb u =
| Monomorphic_const uctx ->
Monomorphic_const_entry uctx
| Polymorphic_const auctx ->
- Polymorphic_const_entry (Univ.AUContext.repr auctx)
+ Polymorphic_const_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx)
in
let pt =
match cb.const_body, u with
@@ -1047,7 +1059,7 @@ let add_include me is_module inl senv =
| SFBmodule _ -> M
| SFBmodtype _ -> MT
in
- add_field field new_name senv
+ add_field ~is_include:true field new_name senv
in
resolver, List.fold_left add senv str
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/term_typing.ml b/kernel/term_typing.ml
index fb1b3e236c..35fa871b4e 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -68,8 +68,8 @@ let feedback_completion_typecheck =
let abstract_constant_universes = function
| Monomorphic_const_entry uctx ->
Univ.empty_level_subst, Monomorphic_const uctx
- | Polymorphic_const_entry uctx ->
- let sbst, auctx = Univ.abstract_universes uctx in
+ | Polymorphic_const_entry (nas, uctx) ->
+ let sbst, auctx = Univ.abstract_universes nas uctx in
let sbst = Univ.make_instance_subst sbst in
sbst, Polymorphic_const auctx
@@ -78,7 +78,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
| ParameterEntry (ctx,(t,uctx),nl) ->
let env = match uctx with
| Monomorphic_const_entry uctx -> push_context_set ~strict:true uctx env
- | Polymorphic_const_entry uctx -> push_context ~strict:false uctx env
+ | Polymorphic_const_entry (_, uctx) -> push_context ~strict:false uctx env
in
let j = infer env t in
let usubst, univs = abstract_constant_universes uctx in
@@ -150,7 +150,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
let ctx = Univ.ContextSet.union univs ctx in
let env = push_context_set ~strict:true ctx env in
env, Univ.empty_level_subst, Monomorphic_const ctx
- | Polymorphic_const_entry uctx ->
+ | Polymorphic_const_entry (nas, uctx) ->
(** Ensure not to generate internal constraints in polymorphic mode.
The only way for this to happen would be that either the body
contained deferred universes, or that it contains monomorphic
@@ -160,7 +160,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
i.e. [trust] is always [Pure]. *)
let () = assert (Univ.ContextSet.is_empty ctx) in
let env = push_context ~strict:false uctx env in
- let sbst, auctx = Univ.abstract_universes uctx in
+ let sbst, auctx = Univ.abstract_universes nas uctx in
let sbst = Univ.make_instance_subst sbst in
env, sbst, Polymorphic_const auctx
in
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 d09b54e7ec..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
@@ -937,17 +937,30 @@ let hcons_universe_context = UContext.hcons
module AUContext =
struct
- include UContext
+ type t = Names.Name.t array constrained
let repr (inst, cst) =
- (Array.mapi (fun i _l -> Level.var i) inst, cst)
+ (Array.init (Array.length inst) (fun i -> Level.var i), cst)
- let pr f ?variance ctx = pr f ?variance (repr ctx)
+ let pr f ?variance ctx = UContext.pr f ?variance (repr ctx)
let instantiate inst (u, cst) =
assert (Array.length u = Array.length inst);
subst_instance_constraints inst cst
+ let names (nas, _) = nas
+
+ let hcons (univs, cst) =
+ (Array.map Names.Name.hcons univs, hcons_constraints cst)
+
+ let empty = ([||], Constraint.empty)
+
+ let is_empty (nas, cst) = Array.is_empty nas && Constraint.is_empty cst
+
+ let union (nas, cst) (nas', cst') = (Array.append nas nas', Constraint.union cst cst')
+
+ let size (nas, _) = Array.length nas
+
end
let hcons_abstract_universe_context = AUContext.hcons
@@ -993,7 +1006,22 @@ end
let hcons_cumulativity_info = CumulativityInfo.hcons
-module ACumulativityInfo = CumulativityInfo
+module ACumulativityInfo =
+struct
+ type t = AUContext.t * Variance.t array
+
+ let pr prl (univs, variance) =
+ AUContext.pr prl ~variance univs
+
+ let hcons (univs, variance) = (* should variance be hconsed? *)
+ (AUContext.hcons univs, variance)
+
+ let univ_context (univs, _subtypcst) = univs
+ let variance (_univs, variance) = variance
+
+ let leq_constraints (_,variance) u u' csts = Variance.leq_constraints variance u u' csts
+ let eq_constraints (_,variance) u u' csts = Variance.eq_constraints variance u u' csts
+end
let hcons_abstract_cumulativity_info = ACumulativityInfo.hcons
@@ -1145,19 +1173,20 @@ let make_inverse_instance_subst i =
LMap.empty arr
let make_abstract_instance (ctx, _) =
- Array.mapi (fun i _l -> Level.var i) ctx
+ Array.init (Array.length ctx) (fun i -> Level.var i)
-let abstract_universes ctx =
+let abstract_universes nas ctx =
let instance = UContext.instance ctx in
+ let () = assert (Int.equal (Array.length nas) (Instance.length instance)) in
let subst = make_instance_subst instance in
let cstrs = subst_univs_level_constraints subst
(UContext.constraints ctx)
in
- let ctx = UContext.make (instance, cstrs) in
+ let ctx = (nas, cstrs) in
instance, ctx
-let abstract_cumulativity_info (univs, variance) =
- let subst, univs = abstract_universes univs in
+let abstract_cumulativity_info nas (univs, variance) =
+ let subst, univs = abstract_universes nas univs in
subst, (univs, variance)
let rec compact_univ s vars i u =
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 7ac8247ca4..de7b334ae4 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -336,9 +336,6 @@ sig
val empty : t
val is_empty : t -> bool
- (** Don't use. *)
- val instance : t -> Instance.t
-
val size : t -> int
(** Keeps the order of the instances *)
@@ -347,6 +344,9 @@ sig
val instantiate : Instance.t -> t -> Constraint.t
(** Generate the set of instantiated Constraint.t **)
+ val names : t -> Names.Name.t array
+ (** Return the names of the bound universe variables *)
+
end
(** Universe info for cumulative inductive types: A context of
@@ -466,8 +466,8 @@ val make_instance_subst : Instance.t -> universe_level_subst
val make_inverse_instance_subst : Instance.t -> universe_level_subst
-val abstract_universes : UContext.t -> Instance.t * AUContext.t
-val abstract_cumulativity_info : CumulativityInfo.t -> Instance.t * ACumulativityInfo.t
+val abstract_universes : Names.Name.t array -> UContext.t -> Instance.t * AUContext.t
+val abstract_cumulativity_info : Names.Name.t array -> CumulativityInfo.t -> Instance.t * ACumulativityInfo.t
(** TODO: move universe abstraction out of the kernel *)
val make_abstract_instance : AUContext.t -> Instance.t
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 7380a860dd..f9c576ca4a 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -9,7 +9,6 @@
(************************************************************************)
open Names
-open Esubst
module RelDecl = Context.Rel.Declaration
@@ -80,19 +79,9 @@ let noccur_with_meta n m term =
(* Lifting *)
(*********************)
-(* The generic lifting function *)
-let rec exliftn el c = match Constr.kind c with
- | Constr.Rel i -> Constr.mkRel(reloc_rel i el)
- | _ -> Constr.map_with_binders el_lift exliftn el c
-
-(* Lifting the binding depth across k bindings *)
-
-let liftn n k c =
- match el_liftn (pred k) (el_shft n el_id) with
- | ELID -> c
- | el -> exliftn el c
-
-let lift n = liftn n 1
+let exliftn = Constr.exliftn
+let liftn = Constr.liftn
+let lift = Constr.lift
(*********************)
(* Substituting *)
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-04-27 19:46:40 +0000