aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cClosure.ml54
-rw-r--r--kernel/cClosure.mli14
-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/declarations.ml28
-rw-r--r--kernel/declareops.ml1
-rw-r--r--kernel/environ.ml24
-rw-r--r--kernel/environ.mli1
-rw-r--r--kernel/indtypes.ml10
-rw-r--r--kernel/indtypes.mli5
-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.ml12
-rw-r--r--kernel/reduction.mli8
-rw-r--r--kernel/safe_typing.ml25
-rw-r--r--kernel/safe_typing.mli1
-rw-r--r--kernel/subtyping.ml6
-rw-r--r--kernel/transparentState.ml45
-rw-r--r--kernel/transparentState.mli34
-rw-r--r--kernel/typeops.ml51
-rw-r--r--kernel/uGraph.ml16
-rw-r--r--kernel/uGraph.mli2
-rw-r--r--kernel/univ.ml6
-rw-r--r--kernel/vars.ml17
-rw-r--r--kernel/vconv.ml4
30 files changed, 303 insertions, 171 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 95546a83e1..1f61bcae2e 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
@@ -303,7 +300,7 @@ and fterm =
| FCoFix of cofixpoint * fconstr subs
| FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
| FLambda of int * (Name.t * constr) list * constr * fconstr subs
- | FProd of Name.t * fconstr * fconstr
+ | FProd of Name.t * fconstr * constr * fconstr subs
| FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs
| FEvar of existential * fconstr subs
| FLIFT of int * fconstr
@@ -587,9 +584,12 @@ let rec to_constr lfts v =
let tys = List.mapi (fun i (na, c) -> na, subst_constr (subs_liftn i subs) c) tys in
let f = subst_constr (subs_liftn len subs) f in
Term.compose_lam (List.rev tys) f
- | FProd (n,t,c) ->
- mkProd (n, to_constr lfts t,
- to_constr (el_lift lfts) c)
+ | FProd (n, t, c, e) ->
+ if is_subs_id e && is_lift_id lfts then
+ mkProd (n, to_constr lfts t, c)
+ else
+ let subs' = comp_subs lfts e in
+ mkProd (n, to_constr lfts t, subst_constr (subs_lift subs') c)
| FLetIn (n,b,t,f,e) ->
let subs = comp_subs (el_lift lfts) (subs_lift e) in
mkLetIn (n, to_constr lfts b,
@@ -872,7 +872,7 @@ and knht info e t stk =
| CoFix cfx -> { norm = Cstr; term = FCoFix (cfx,e) }, stk
| Lambda _ -> { norm = Cstr; term = mk_lambda e t }, stk
| Prod (n, t, c) ->
- { norm = Whnf; term = FProd (n, mk_clos e t, mk_clos (subs_lift e) c) }, stk
+ { norm = Whnf; term = FProd (n, mk_clos e t, c, e) }, stk
| LetIn (n,b,t,c) ->
{ norm = Red; term = FLetIn (n, mk_clos e b, mk_clos e t, c, e) }, stk
| Evar ev -> { norm = Red; term = FEvar (ev, e) }, stk
@@ -995,8 +995,8 @@ and norm_head info tab m =
| FLetIn(na,a,b,f,e) ->
let c = mk_clos (subs_lift e) f in
mkLetIn(na, kl info tab a, kl info tab b, kl info tab c)
- | FProd(na,dom,rng) ->
- mkProd(na, kl info tab dom, kl info tab rng)
+ | FProd(na,dom,rng,e) ->
+ mkProd(na, kl info tab dom, kl info tab (mk_clos (subs_lift e) rng))
| FCoFix((n,(na,tys,bds)),e) ->
let ftys = Array.Fun1.map mk_clos e tys in
let fbds =
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 1ee4bccc25..c2d53eed47 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
@@ -122,7 +114,7 @@ type fterm =
| FCoFix of cofixpoint * fconstr subs
| FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
| FLambda of int * (Name.t * constr) list * constr * fconstr subs
- | FProd of Name.t * fconstr * fconstr
+ | FProd of Name.t * fconstr * constr * fconstr subs
| FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs
| FEvar of existential * fconstr subs
| FLIFT of int * fconstr
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/declarations.ml b/kernel/declarations.ml
index c1b38b4156..94832726fe 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -61,13 +61,27 @@ type constant_universes =
of a constant are tracked in their {!constant_body} so that they
can be displayed to the user. *)
type typing_flags = {
- check_guarded : bool; (** If [false] then fixed points and co-fixed
- points are assumed to be total. *)
- check_universes : bool; (** If [false] universe constraints are not checked *)
- conv_oracle : Conv_oracle.oracle; (** Unfolding strategies for conversion *)
- share_reduction : bool; (** Use by-need reduction algorithm *)
- enable_VM : bool; (** If [false], all VM conversions fall back to interpreted ones *)
- enable_native_compiler : bool; (** If [false], all native conversions fall back to VM ones *)
+ check_guarded : bool;
+ (** If [false] then fixed points and co-fixed points are assumed to
+ be total. *)
+
+ check_universes : bool;
+ (** If [false] universe constraints are not checked *)
+
+ conv_oracle : Conv_oracle.oracle;
+ (** Unfolding strategies for conversion *)
+
+ share_reduction : bool;
+ (** Use by-need reduction algorithm *)
+
+ enable_VM : bool;
+ (** If [false], all VM conversions fall back to interpreted ones *)
+
+ enable_native_compiler : bool;
+ (** If [false], all native conversions fall back to VM ones *)
+
+ indices_matter: bool;
+ (** The universe of an inductive type must be above that of its indices. *)
}
(* some contraints are in constant_constraints, some other may be in
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 3ed599c538..d1d184df69 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -24,6 +24,7 @@ let safe_flags oracle = {
share_reduction = true;
enable_VM = true;
enable_native_compiler = true;
+ indices_matter = true;
}
(** {6 Arities } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index f61dd0c101..7835a807ba 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -241,6 +241,8 @@ let is_impredicative_set env =
let type_in_type env = not (typing_flags env).check_universes
let deactivated_guard env = not (typing_flags env).check_guarded
+let indices_matter env = env.env_typing_flags.indices_matter
+
let universes env = env.env_stratification.env_universes
let named_context env = env.env_named_context.env_named_ctx
let named_context_val env = env.env_named_context
@@ -384,8 +386,28 @@ 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;
+ indices_matter;
+ share_reduction;
+ enable_VM;
+ enable_native_compiler;
+ } alt =
+ check_guarded == alt.check_guarded &&
+ check_universes == alt.check_universes &&
+ conv_oracle == alt.conv_oracle &&
+ indices_matter == alt.indices_matter &&
+ share_reduction == alt.share_reduction &&
+ enable_VM == alt.enable_VM &&
+ enable_native_compiler == alt.enable_native_compiler
+[@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/environ.mli b/kernel/environ.mli
index c285f907fc..91b28bfcbc 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -96,6 +96,7 @@ val typing_flags : env -> typing_flags
val is_impredicative_set : env -> bool
val type_in_type : env -> bool
val deactivated_guard : env -> bool
+val indices_matter : env -> bool
(** is the local context empty *)
val empty_context : env -> bool
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 20c90bc05a..a4a02791b4 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -35,14 +35,6 @@ env_ar_par = env_ar + declaration of parameters
nmr = ongoing computation of recursive parameters
*)
-(* Tell if indices (aka real arguments) contribute to size of inductive type *)
-(* If yes, this is compatible with the univalent model *)
-
-let indices_matter = ref false
-
-let enforce_indices_matter () = indices_matter := true
-let is_indices_matter () = !indices_matter
-
(* [weaker_noccur_between env n nvars t] (defined above), checks that
no de Bruijn indices between [n] and [n+nvars] occur in [t]. If
some such occurrences are found, then reduction is performed
@@ -303,7 +295,7 @@ let typecheck_inductive env mie =
let inflev =
(* The level of the inductive includes levels of indices if
in indices_matter mode *)
- if !indices_matter
+ if indices_matter env
then Some (cumulate_arity_large_levels env_params sign)
else None
in
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index a827c17683..840e23ed69 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -50,8 +50,3 @@ val check_positivity : chkpos:bool ->
(** The following function does checks on inductive declarations. *)
val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
-
-(** The following enforces a system compatible with the univalent model *)
-
-val enforce_indices_matter : unit -> unit
-val is_indices_matter : unit -> bool
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..97cd4c00d7 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
@@ -438,14 +438,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
let cuniv = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in
ccnv CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 cuniv
- | (FProd (_,c1,c2), FProd (_,c'1,c'2)) ->
+ | (FProd (_, c1, c2, e), FProd (_, c'1, c'2, e')) ->
if not (is_empty_stack v1 && is_empty_stack v2) then
anomaly (Pp.str "conversion was given ill-typed terms (FProd).");
(* Luo's system *)
let el1 = el_stack lft1 v1 in
let el2 = el_stack lft2 v2 in
let cuniv = ccnv CONV l2r infos el1 el2 c1 c'1 cuniv in
- ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv
+ ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) (mk_clos (subs_lift e) c2) (mk_clos (subs_lift e') c'2) cuniv
(* Eta-expansion on the fly *)
| (FLambda _, _) ->
@@ -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..b7f1e93062 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -192,7 +192,12 @@ 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_indices_matter indices_matter senv =
+ set_typing_flags { (Environ.typing_flags senv.env) with indices_matter } senv
let set_share_reduction b senv =
let flags = Environ.typing_flags senv.env in
@@ -496,7 +501,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 +511,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
@@ -1047,7 +1062,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/safe_typing.mli b/kernel/safe_typing.mli
index 7af773e3bc..57b01f15e3 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -136,6 +136,7 @@ val add_constraints :
(** Setting the type theory flavor *)
val set_engagement : Declarations.engagement -> safe_transformer0
+val set_indices_matter : bool -> safe_transformer0
val set_typing_flags : Declarations.typing_flags -> safe_transformer0
val set_share_reduction : bool -> safe_transformer0
val set_VM : bool -> safe_transformer0
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/typeops.ml b/kernel/typeops.ml
index c8fd83c8a9..c9acd168e8 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -151,28 +151,41 @@ let type_of_abstraction _env name var ty =
let make_judgev c t =
Array.map2 make_judge c t
+let rec check_empty_stack = function
+| [] -> true
+| CClosure.Zupdate _ :: s -> check_empty_stack s
+| _ -> false
+
let type_of_apply env func funt argsv argstv =
+ let open CClosure in
let len = Array.length argsv in
- let rec apply_rec i typ =
- if Int.equal i len then typ
- else
- (match kind (whd_all env typ) with
- | Prod (_,c1,c2) ->
- let arg = argsv.(i) and argt = argstv.(i) in
- (try
- let () = conv_leq false env argt c1 in
- apply_rec (i+1) (subst1 arg c2)
- with NotConvertible ->
- error_cant_apply_bad_type env
- (i+1,c1,argt)
- (make_judge func funt)
- (make_judgev argsv argstv))
-
+ let infos = create_clos_infos all env in
+ let tab = create_tab () in
+ let rec apply_rec i typ =
+ if Int.equal i len then term_of_fconstr typ
+ else
+ let typ, stk = whd_stack infos tab typ [] in
+ (** The return stack is known to be empty *)
+ let () = assert (check_empty_stack stk) in
+ match fterm_of typ with
+ | FProd (_, c1, c2, e) ->
+ let arg = argsv.(i) in
+ let argt = argstv.(i) in
+ let c1 = term_of_fconstr c1 in
+ begin match conv_leq false env argt c1 with
+ | () -> apply_rec (i+1) (mk_clos (Esubst.subs_cons ([| inject arg |], e)) c2)
+ | exception NotConvertible ->
+ error_cant_apply_bad_type env
+ (i+1,c1,argt)
+ (make_judge func funt)
+ (make_judgev argsv argstv)
+ end
| _ ->
- error_cant_apply_not_functional env
- (make_judge func funt)
- (make_judgev argsv argstv))
- in apply_rec 0 funt
+ error_cant_apply_not_functional env
+ (make_judge func funt)
+ (make_judgev argsv argstv)
+ in
+ apply_rec 0 (inject funt)
(* Type of product *)
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/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-30 04:23:52 +0000