aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/constr.ml15
-rw-r--r--kernel/constr.mli2
-rw-r--r--kernel/cooking.ml18
-rw-r--r--kernel/declarations.ml4
-rw-r--r--kernel/declareops.ml1
-rw-r--r--kernel/environ.ml19
-rw-r--r--kernel/environ.mli24
-rw-r--r--kernel/indTyping.ml17
-rw-r--r--kernel/indTyping.mli1
-rw-r--r--kernel/type_errors.ml4
-rw-r--r--kernel/type_errors.mli4
-rw-r--r--kernel/typeops.ml18
-rw-r--r--kernel/typeops.mli2
13 files changed, 50 insertions, 79 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 15e5c512ed..84eacb196c 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -253,7 +253,7 @@ let mkFloat f = Float f
least one argument and the function is not itself an applicative
term *)
-let kind c = c
+let kind (c:t) = c
let rec kind_nocast_gen kind c =
match kind c with
@@ -338,6 +338,19 @@ let isProj c = match kind c with Proj _ -> true | _ -> false
let isFix c = match kind c with Fix _ -> true | _ -> false
let isCoFix c = match kind c with CoFix _ -> true | _ -> false
+let isRef c = match kind c with
+ | Const _ | Ind _ | Construct _ | Var _ -> true
+ | _ -> false
+
+let isRefX x c =
+ let open GlobRef in
+ match x, kind c with
+ | ConstRef c, Const (c', _) -> Constant.equal c c'
+ | IndRef i, Ind (i', _) -> eq_ind i i'
+ | ConstructRef i, Construct (i', _) -> eq_constructor i i'
+ | VarRef id, Var id' -> Id.equal id id'
+ | _ -> false
+
(* Destructs a de Bruijn index *)
let destRel c = match kind c with
| Rel n -> n
diff --git a/kernel/constr.mli b/kernel/constr.mli
index d4af1149c2..159570b5ea 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -256,6 +256,8 @@ val isRel : constr -> bool
val isRelN : int -> constr -> bool
val isVar : constr -> bool
val isVarId : Id.t -> constr -> bool
+val isRef : constr -> bool
+val isRefX : GlobRef.t -> constr -> bool
val isInd : constr -> bool
val isEvar : constr -> bool
val isMeta : constr -> bool
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index f1eb000c88..31dd26d2ba 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -258,17 +258,6 @@ let cook_constant { from = cb; info } =
(********************************)
(* Discharging mutual inductive *)
-let template_level_of_var ~template_check d =
- (* When [template_check], a universe from a section variable may not
- be in the universes from the inductive (it must be pre-declared)
- so always [None]. *)
- if template_check then None
- else
- let c = Term.strip_prod_assum (RelDecl.get_type d) in
- match kind c with
- | Sort (Type u) -> Univ.Universe.level u
- | _ -> None
-
let it_mkProd_wo_LetIn = List.fold_left (fun c d -> mkProd_wo_LetIn d c)
let abstract_rel_ctx (section_decls,subst) ctx =
@@ -305,7 +294,7 @@ let abstract_projection ~params expmod hyps t =
let _, t = decompose_prod_n_assum (List.length params + 1 + Context.Rel.nhyps (fst hyps)) t in
t
-let cook_one_ind ~template_check ~ntypes
+let cook_one_ind ~ntypes
(section_decls,_ as hyps) expmod mip =
let mind_arity = match mip.mind_arity with
| RegularArity {mind_user_arity=arity;mind_sort=sort} ->
@@ -314,7 +303,7 @@ let cook_one_ind ~template_check ~ntypes
RegularArity {mind_user_arity=arity; mind_sort=sort}
| TemplateArity {template_param_levels=levels;template_level;template_context} ->
let sec_levels = CList.map_filter (fun d ->
- if RelDecl.is_local_assum d then Some (template_level_of_var ~template_check d)
+ if RelDecl.is_local_assum d then Some None
else None)
section_decls
in
@@ -362,14 +351,13 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib =
let removed_vars = Context.Named.to_vars section_decls in
let section_decls, _ as hyps = abstract_context section_decls in
let nnewparams = Context.Rel.nhyps section_decls in
- let template_check = mib.mind_typing_flags.check_template in
let mind_params_ctxt =
let ctx = Context.Rel.map expmod mib.mind_params_ctxt in
abstract_rel_ctx hyps ctx
in
let ntypes = mib.mind_ntypes in
let mind_packets =
- Array.map (cook_one_ind ~template_check ~ntypes hyps expmod)
+ Array.map (cook_one_ind ~ntypes hyps expmod)
mib.mind_packets
in
let mind_record = match mib.mind_record with
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index c550b0d432..ac130d018d 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -89,10 +89,6 @@ type typing_flags = {
indices_matter: bool;
(** The universe of an inductive type must be above that of its indices. *)
- check_template : bool;
- (* If [false] then we don't check that the universes template-polymorphic
- inductive parameterize on are necessarily local and unbounded from below.
- This potentially introduces inconsistencies. *)
}
(* some contraints are in constant_constraints, some other may be in
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 047027984d..a3adac7a11 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -26,7 +26,6 @@ let safe_flags oracle = {
enable_VM = true;
enable_native_compiler = true;
indices_matter = true;
- check_template = true;
}
(** {6 Arities } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index f04863386f..501ac99ff3 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -275,7 +275,6 @@ 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 check_template env = env.env_typing_flags.check_template
let universes env = env.env_stratification.env_universes
let universes_lbound env = env.env_stratification.env_universes_lbound
@@ -399,9 +398,6 @@ let add_constraints c env =
let check_constraints c env =
UGraph.check_constraints c env.env_stratification.env_universes
-let push_constraints_to_env (_,univs) env =
- add_constraints univs env
-
let add_universes ~lbound ~strict ctx g =
let g = Array.fold_left
(fun g v -> UGraph.add_universe ~lbound ~strict v g)
@@ -449,7 +445,6 @@ let same_flags {
share_reduction;
enable_VM;
enable_native_compiler;
- check_template;
} alt =
check_guarded == alt.check_guarded &&
check_positive == alt.check_positive &&
@@ -458,8 +453,7 @@ let same_flags {
indices_matter == alt.indices_matter &&
share_reduction == alt.share_reduction &&
enable_VM == alt.enable_VM &&
- enable_native_compiler == alt.enable_native_compiler &&
- check_template == alt.check_template
+ enable_native_compiler == alt.enable_native_compiler
[@warning "+9"]
let set_typing_flags c env = (* Unsafe *)
@@ -591,9 +585,6 @@ let polymorphic_pind (ind,u) env =
let type_in_type_ind (mind,_i) env =
not (lookup_mind mind env).mind_typing_flags.check_universes
-let template_checked_ind (mind,_i) env =
- (lookup_mind mind env).mind_typing_flags.check_template
-
let template_polymorphic_ind (mind,i) env =
match (lookup_mind mind env).mind_packets.(i).mind_arity with
| TemplateArity _ -> true
@@ -802,14 +793,6 @@ let get_template_polymorphic_variables env r =
| IndRef ind -> template_polymorphic_variables ind env
| ConstructRef cstr -> template_polymorphic_variables (inductive_of_constructor cstr) env
-let is_template_checked env r =
- let open Names.GlobRef in
- match r with
- | VarRef _id -> false
- | ConstRef _c -> false
- | IndRef ind -> template_checked_ind ind env
- | ConstructRef cstr -> template_checked_ind (inductive_of_constructor cstr) env
-
let is_type_in_type env r =
let open Names.GlobRef in
match r with
diff --git a/kernel/environ.mli b/kernel/environ.mli
index bd5a000c2b..a596584cbe 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -112,7 +112,6 @@ val is_impredicative_set : env -> bool
val type_in_type : env -> bool
val deactivated_guard : env -> bool
val indices_matter : env -> bool
-val check_template : env -> bool
val is_impredicative_sort : env -> Sorts.t -> bool
val is_impredicative_univ : env -> Univ.Universe.t -> bool
@@ -274,7 +273,6 @@ val type_in_type_ind : inductive -> env -> bool
val template_polymorphic_ind : inductive -> env -> bool
val template_polymorphic_variables : inductive -> env -> Univ.Level.t list
val template_polymorphic_pind : pinductive -> env -> bool
-val template_checked_ind : inductive -> env -> bool
(** {5 Modules } *)
@@ -288,22 +286,21 @@ val lookup_modtype : ModPath.t -> env -> module_type_body
(** {5 Universe constraints } *)
-(** Add universe constraints to the environment.
- @raise UniverseInconsistency .
-*)
val add_constraints : Univ.Constraint.t -> env -> env
+(** Add universe constraints to the environment.
+ @raise UniverseInconsistency. *)
-(** Check constraints are satifiable in the environment. *)
val check_constraints : Univ.Constraint.t -> env -> bool
+(** Check constraints are satifiable in the environment. *)
+
val push_context : ?strict:bool -> Univ.UContext.t -> env -> env
-(* [push_context ?(strict=false) ctx env] pushes the universe context to the environment.
- @raise UGraph.AlreadyDeclared if one of the universes is already declared.
-*)
-val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env
-(* [push_context_set ?(strict=false) ctx env] pushes the universe context set
- to the environment. It does not fail if one of the universes is already declared. *)
+(** [push_context ?(strict=false) ctx env] pushes the universe context to the environment.
+ @raise UGraph.AlreadyDeclared if one of the universes is already declared. *)
-val push_constraints_to_env : 'a Univ.constrained -> env -> env
+val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env
+(** [push_context_set ?(strict=false) ctx env] pushes the universe
+ context set to the environment. It does not fail even if one of the
+ universes is already declared. *)
val push_subgraph : Univ.ContextSet.t -> env -> env
(** [push_subgraph univs env] adds the universes and constraints in
@@ -373,7 +370,6 @@ val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declarat
val is_polymorphic : env -> Names.GlobRef.t -> bool
val is_template_polymorphic : env -> GlobRef.t -> bool
val get_template_polymorphic_variables : env -> GlobRef.t -> Univ.Level.t list
-val is_template_checked : env -> GlobRef.t -> bool
val is_type_in_type : env -> GlobRef.t -> bool
(** Native compiler *)
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 113ee787f2..cc15109f06 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -197,7 +197,7 @@ let unbounded_from_below u cstrs =
(starting from the most recent and ignoring let-definitions) is not
contributing to the inductive type's sort or is Some u_k if its level
is u_k and is contributing. *)
-let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt concl =
+let template_polymorphic_univs ~ctor_levels uctx paramsctxt concl =
let check_level l =
Univ.LSet.mem l (Univ.ContextSet.levels uctx) &&
unbounded_from_below l (Univ.ContextSet.constraints uctx) &&
@@ -205,27 +205,23 @@ let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt conc
in
let univs = Univ.Universe.levels concl in
let univs =
- if template_check then
- Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs
- else univs (* Doesn't check the universes can be generalized *)
+ Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs
in
let fold acc = function
| (LocalAssum (_, p)) ->
(let c = Term.strip_prod_assum p in
match kind c with
| Sort (Type u) ->
- if template_check then
(match Univ.Universe.level u with
| Some l -> if Univ.LSet.mem l univs && not (Univ.Level.is_prop l) then Some l else None
| None -> None)
- else Univ.Universe.level u
| _ -> None) :: acc
| LocalDef _ -> acc
in
let params = List.fold_left fold [] paramsctxt in
params, univs
-let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) =
+let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) =
if not (Universe.Set.is_empty univ_info.missing)
then raise (InductiveError (MissingConstraints (univ_info.missing,univ_info.ind_univ)));
let arity = Vars.subst_univs_level_constr usubst arity in
@@ -267,9 +263,9 @@ let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,sp
splayed_lc
in
let param_levels, concl_levels =
- template_polymorphic_univs ~template_check ~ctor_levels ctx params min_univ
+ template_polymorphic_univs ~ctor_levels ctx params min_univ
in
- if template_check && List.for_all (fun x -> Option.is_empty x) param_levels
+ if List.for_all (fun x -> Option.is_empty x) param_levels
&& Univ.LSet.is_empty concl_levels then
CErrors.user_err
Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.")
@@ -356,8 +352,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
(* Abstract universes *)
let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in
let params = Vars.subst_univs_level_context usubst params in
- let template_check = Environ.check_template env in
- let data = List.map (abstract_packets ~template_check univs usubst params) data in
+ let data = List.map (abstract_packets univs usubst params) data in
let env_ar_par =
let ctx = Environ.rel_context env_ar_par in
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index 8dea8f046d..723ba5459e 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -40,7 +40,6 @@ val typecheck_inductive : env -> sec_univs:Univ.Level.t array option
(* Utility function to compute the actual universe parameters
of a template polymorphic inductive *)
val template_polymorphic_univs :
- template_check:bool ->
ctor_levels:Univ.LSet.t ->
Univ.ContextSet.t ->
Constr.rel_context ->
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index c2cdf98ee8..6c06c1e0f1 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -48,7 +48,7 @@ type ('constr, 'types) ptype_error =
| UnboundVar of variable
| NotAType of ('constr, 'types) punsafe_judgment
| BadAssumption of ('constr, 'types) punsafe_judgment
- | ReferenceVariables of Id.t * 'constr
+ | ReferenceVariables of Id.t * GlobRef.t
| ElimArity of pinductive * 'constr * ('constr, 'types) punsafe_judgment
* (Sorts.family * Sorts.family * Sorts.family * arity_error) option
| CaseNotInductive of ('constr, 'types) punsafe_judgment
@@ -182,7 +182,7 @@ let map_ptype_error f = function
| UnboundVar id -> UnboundVar id
| NotAType j -> NotAType (on_judgment f j)
| BadAssumption j -> BadAssumption (on_judgment f j)
-| ReferenceVariables (id, c) -> ReferenceVariables (id, f c)
+| ReferenceVariables (id, c) -> ReferenceVariables (id, c)
| ElimArity (pi, c, j, ar) -> ElimArity (pi, f c, on_judgment f j, ar)
| CaseNotInductive j -> CaseNotInductive (on_judgment f j)
| WrongCaseInfo (pi, ci) -> WrongCaseInfo (pi, ci)
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 0f29717f12..d9842ecefa 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -49,7 +49,7 @@ type ('constr, 'types) ptype_error =
| UnboundVar of variable
| NotAType of ('constr, 'types) punsafe_judgment
| BadAssumption of ('constr, 'types) punsafe_judgment
- | ReferenceVariables of Id.t * 'constr
+ | ReferenceVariables of Id.t * GlobRef.t
| ElimArity of pinductive * 'constr * ('constr, 'types) punsafe_judgment
* (Sorts.family * Sorts.family * Sorts.family * arity_error) option
| CaseNotInductive of ('constr, 'types) punsafe_judgment
@@ -102,7 +102,7 @@ val error_not_type : env -> unsafe_judgment -> 'a
val error_assumption : env -> unsafe_judgment -> 'a
-val error_reference_variables : env -> Id.t -> constr -> 'a
+val error_reference_variables : env -> Id.t -> GlobRef.t -> 'a
val error_elim_arity :
env -> pinductive -> constr -> unsafe_judgment ->
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index c74bfd0688..2a35f87db8 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -116,7 +116,7 @@ let type_of_variable env id =
(* Checks if a context of variables can be instantiated by the
variables of the current env.
Order does not have to be checked assuming that all names are distinct *)
-let check_hyps_inclusion env ?evars f c sign =
+let check_hyps_inclusion env ?evars c sign =
let conv env a b = conv env ?evars a b in
Context.Named.fold_outside
(fun d1 () ->
@@ -133,7 +133,7 @@ let check_hyps_inclusion env ?evars f c sign =
| LocalDef _, LocalAssum _ -> raise NotConvertible
| LocalDef (_,b2,_), LocalDef (_,b1,_) -> conv env b2 b1);
with Not_found | NotConvertible | Option.Heterogeneous ->
- error_reference_variables env id (f c))
+ error_reference_variables env id c)
sign
~init:()
@@ -146,14 +146,14 @@ let check_hyps_inclusion env ?evars f c sign =
let type_of_constant env (kn,_u as cst) =
let cb = lookup_constant kn env in
- let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in
+ let () = check_hyps_inclusion env (GlobRef.ConstRef kn) cb.const_hyps in
let ty, cu = constant_type env cst in
let () = check_constraints cu env in
ty
let type_of_constant_in env (kn,_u as cst) =
let cb = lookup_constant kn env in
- let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in
+ let () = check_hyps_inclusion env (GlobRef.ConstRef kn) cb.const_hyps in
constant_type_in env cst
(* Type of a lambda-abstraction. *)
@@ -368,18 +368,18 @@ let check_cast env c ct k expected_type =
the App case of execute; from this constraints, the expected
dynamic constraints of the form u<=v are enforced *)
-let type_of_inductive_knowing_parameters env (ind,u as indu) args =
+let type_of_inductive_knowing_parameters env (ind,u) args =
let (mib,_mip) as spec = lookup_mind_specif env ind in
- check_hyps_inclusion env mkIndU indu mib.mind_hyps;
+ check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps;
let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters
env (spec,u) args
in
check_constraints cst env;
t
-let type_of_inductive env (ind,u as indu) =
+let type_of_inductive env (ind,u) =
let (mib,mip) = lookup_mind_specif env ind in
- check_hyps_inclusion env mkIndU indu mib.mind_hyps;
+ check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps;
let t,cst = Inductive.constrained_type_of_inductive env ((mib,mip),u) in
check_constraints cst env;
t
@@ -390,7 +390,7 @@ let type_of_constructor env (c,_u as cu) =
let () =
let ((kn,_),_) = c in
let mib = lookup_mind kn env in
- check_hyps_inclusion env mkConstructU cu mib.mind_hyps
+ check_hyps_inclusion env (GlobRef.ConstructRef c) mib.mind_hyps
in
let specif = lookup_mind_specif env (inductive_of_constructor c) in
let t,cst = constrained_type_of_constructor cu specif in
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index ae816fe26e..f88bc653de 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -111,7 +111,7 @@ val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
(** Check that hyps are included in env and fails with error otherwise *)
val check_hyps_inclusion : env -> ?evars:((existential->constr option) * UGraph.t) ->
- ('a -> constr) -> 'a -> Constr.named_context -> unit
+ GlobRef.t -> Constr.named_context -> unit
val check_primitive_type : env -> CPrimitives.op_or_type -> types -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 05:05:15 +0000