aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cPrimitives.ml2
-rw-r--r--kernel/declarations.ml2
-rw-r--r--kernel/declareops.ml7
-rw-r--r--kernel/indtypes.ml6
-rw-r--r--kernel/inductive.ml10
-rw-r--r--kernel/inductive.mli2
-rw-r--r--kernel/mod_subst.ml3
-rw-r--r--kernel/primred.ml4
-rw-r--r--kernel/retroknowledge.ml1
-rw-r--r--kernel/retroknowledge.mli1
-rw-r--r--kernel/type_errors.ml5
-rw-r--r--kernel/type_errors.mli3
-rw-r--r--kernel/typeops.ml21
13 files changed, 34 insertions, 33 deletions
diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index da5c4fb07b..fdc93cfa89 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -148,7 +148,7 @@ let prim_ind_to_string = function
| PIT_cmp -> "cmp"
let prim_type_to_string = function
- | PT_int63 -> "int63"
+ | PT_int63 -> "int63_type"
let op_or_type_to_string = function
| OT_op op -> to_string op
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 6777e0c223..567850645e 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -166,7 +166,7 @@ type one_inductive_body = {
mind_kelim : Sorts.family list; (** List of allowed elimination sorts *)
- mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion exposes the inductive type *)
+ mind_nf_lc : (rel_context * types) array; (** Head normalized constructor types so that their conclusion exposes the inductive type *)
mind_consnrealargs : int array;
(** Number of expected proper arguments of the constructors (w/o params) *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 9e0230c3ba..d56502a095 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -214,7 +214,7 @@ let subst_mind_packet sub mbp =
mind_consnrealdecls = mbp.mind_consnrealdecls;
mind_consnrealargs = mbp.mind_consnrealargs;
mind_typename = mbp.mind_typename;
- mind_nf_lc = Array.Smart.map (subst_mps sub) mbp.mind_nf_lc;
+ mind_nf_lc = Array.Smart.map (fun (ctx, c) -> Context.Rel.map (subst_mps sub) ctx, subst_mps sub c) mbp.mind_nf_lc;
mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt;
mind_arity = subst_ind_arity sub mbp.mind_arity;
mind_user_lc = Array.Smart.map (subst_mps sub) mbp.mind_user_lc;
@@ -299,9 +299,8 @@ let hcons_ind_arity =
let hcons_mind_packet oib =
let user = Array.Smart.map Constr.hcons oib.mind_user_lc in
- let nf = Array.Smart.map Constr.hcons oib.mind_nf_lc in
- (* Special optim : merge [mind_user_lc] and [mind_nf_lc] if possible *)
- let nf = if Array.equal (==) user nf then user else nf in
+ let map (ctx, c) = Context.Rel.map Constr.hcons ctx, Constr.hcons c in
+ let nf = Array.Smart.map map oib.mind_nf_lc in
{ oib with
mind_typename = Names.Id.hcons oib.mind_typename;
mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt;
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 8f06e1e4b8..457c17907e 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -416,7 +416,9 @@ let compute_projections (kn, i as ind) mib =
let pkt = mib.mind_packets.(i) in
let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in
- let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in
+ let (ctx, cty) = pkt.mind_nf_lc.(0) in
+ let cty = it_mkProd_or_LetIn cty ctx in
+ let rctx, _ = decompose_prod_assum (substl subst cty) in
let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
(** We build a substitution smashing the lets in the record parameters so
that typechecking projections requires just a substitution and not
@@ -475,7 +477,7 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite
(* Check one inductive *)
let build_one_packet (id,cnames) ((arity,lc),(indices,splayed_lc),kelim) recarg =
(* Type of constructors in normal form *)
- let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b (d@paramsctxt)) splayed_lc in
+ let nf_lc = Array.map (fun (d, b) -> (d@paramsctxt, b)) splayed_lc in
let consnrealdecls =
Array.map (fun (d,_) -> Context.Rel.length d)
splayed_lc in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 848ae65c51..f4c2483c14 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -251,7 +251,11 @@ let constrained_type_of_constructor (_cstr,u as cstru) (mib,_mip as ind) =
let arities_of_specif (kn,u) (mib,mip) =
let specif = mip.mind_nf_lc in
- Array.map (constructor_instantiate kn u mib) specif
+ let map (ctx, c) =
+ let cty = Term.it_mkProd_or_LetIn c ctx in
+ constructor_instantiate kn u mib cty
+ in
+ Array.map map specif
let arities_of_constructors ind specif =
arities_of_specif (fst (fst ind), snd ind) specif
@@ -342,7 +346,8 @@ let is_correct_arity env c pj ind specif params =
(* [p] is the predicate, [i] is the constructor number (starting from 0),
and [cty] is the type of the constructor (params not instantiated) *)
let build_branches_type (ind,u) (_,mip as specif) params p =
- let build_one_branch i cty =
+ let build_one_branch i (ctx, c) =
+ let cty = Term.it_mkProd_or_LetIn c ctx in
let typi = full_constructor_instantiate (ind,u,specif,params) cty in
let (cstrsign,ccl) = Term.decompose_prod_assum typi in
let nargs = Context.Rel.length cstrsign in
@@ -597,6 +602,7 @@ let lambda_implicit_lift n a =
(* This removes global parameters of the inductive types in lc (for
nested inductive types only ) *)
let abstract_mind_lc ntyps npars lc =
+ let lc = Array.map (fun (ctx, c) -> Term.it_mkProd_or_LetIn c ctx) lc in
if Int.equal npars 0 then
lc
else
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 3c1464c6c9..ad35c16c22 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -139,4 +139,4 @@ val subterm_specif : guard_env -> stack_element list -> constr -> subterm_spec
val lambda_implicit_lift : int -> constr -> constr
-val abstract_mind_lc : int -> Int.t -> constr array -> constr array
+val abstract_mind_lc : int -> Int.t -> (rel_context * constr) array -> constr array
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index cd675653cb..9397772415 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -339,9 +339,6 @@ let subst_retro_action subst action =
| Register_type(prim,c) ->
let c' = subst_constant subst c in
if c == c' then action else Register_type(prim, c')
- | Register_inline(c) ->
- let c' = subst_constant subst c in
- if c == c' then action else Register_inline(c')
(* Here the semantics is completely unclear.
What does "Hint Unfold t" means when "t" is a parameter?
diff --git a/kernel/primred.ml b/kernel/primred.ml
index d95d7de7aa..d6d0a6143a 100644
--- a/kernel/primred.ml
+++ b/kernel/primred.ml
@@ -44,10 +44,6 @@ let add_retroknowledge env action =
{ retro with retro_cmp = Some r }
in
set_retroknowledge env retro
- | Register_inline(c) ->
- let (cb,r) = lookup_constant_key c env in
- let cb = {cb with Declarations.const_inline_code = true} in
- add_constant_key c cb !(fst r) env
let get_int_type env =
match env.retroknowledge.retro_int63 with
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 18fafdb6d3..e1c4cec5b5 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -38,4 +38,3 @@ let empty = {
type action =
| Register_ind of CPrimitives.prim_ind * inductive
| Register_type of CPrimitives.prim_type * Constant.t
- | Register_inline of Constant.t
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 1554fe88da..09e8140308 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -25,4 +25,3 @@ val empty : retroknowledge
type action =
| Register_ind of CPrimitives.prim_ind * inductive
| Register_type of CPrimitives.prim_type * Constant.t
- | Register_inline of Constant.t
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 964d32c6b3..481ffc290c 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -55,6 +55,7 @@ type ('constr, 'types) ptype_error =
| IllFormedBranch of 'constr * pconstructor * 'constr * 'constr
| Generalization of (Name.t * 'types) * ('constr, 'types) punsafe_judgment
| ActualType of ('constr, 'types) punsafe_judgment * 'types
+ | IncorrectPrimitive of (CPrimitives.op_or_type,'types) punsafe_judgment * 'types
| CantApplyBadType of
(int * 'constr * 'constr) * ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
| CantApplyNonFunctional of ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
@@ -120,6 +121,9 @@ let error_generalization env nvar c =
let error_actual_type env j expty =
raise (TypeError (env, ActualType (j,expty)))
+let error_incorrect_primitive env p t =
+ raise (TypeError (env, IncorrectPrimitive (p, t)))
+
let error_cant_apply_not_functional env rator randl =
raise (TypeError (env, CantApplyNonFunctional (rator,randl)))
@@ -175,6 +179,7 @@ let map_ptype_error f = function
| IllFormedBranch (c, pc, t1, t2) -> IllFormedBranch (f c, pc, f t1, f t2)
| Generalization ((na, t), j) -> Generalization ((na, f t), on_judgment f j)
| ActualType (j, t) -> ActualType (on_judgment f j, f t)
+| IncorrectPrimitive (p, t) -> IncorrectPrimitive ({p with uj_type=f p.uj_type}, f t)
| CantApplyBadType ((n, c1, c2), j, vj) ->
CantApplyBadType ((n, f c1, f c2), on_judgment f j, Array.map (on_judgment f) vj)
| CantApplyNonFunctional (j, jv) -> CantApplyNonFunctional (on_judgment f j, Array.map (on_judgment f) jv)
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 4b832930e1..c5ab9a4e73 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -56,6 +56,7 @@ type ('constr, 'types) ptype_error =
| IllFormedBranch of 'constr * pconstructor * 'constr * 'constr
| Generalization of (Name.t * 'types) * ('constr, 'types) punsafe_judgment
| ActualType of ('constr, 'types) punsafe_judgment * 'types
+ | IncorrectPrimitive of (CPrimitives.op_or_type,'types) punsafe_judgment * 'types
| CantApplyBadType of
(int * 'constr * 'constr) * ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
| CantApplyNonFunctional of ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
@@ -112,6 +113,8 @@ val error_generalization : env -> Name.t * types -> unsafe_judgment -> 'a
val error_actual_type : env -> unsafe_judgment -> types -> 'a
+val error_incorrect_primitive : env -> (CPrimitives.op_or_type,types) punsafe_judgment -> types -> 'a
+
val error_cant_apply_not_functional :
env -> unsafe_judgment -> unsafe_judgment array -> 'a
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 7eb8e803b3..227a164549 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -252,6 +252,11 @@ let type_of_prim env t =
in
nary_int63_op (CPrimitives.arity t) return_ty
+let type_of_prim_or_type env = let open CPrimitives in
+ function
+ | OT_type t -> type_of_prim_type env t
+ | OT_op op -> type_of_prim env op
+
let judge_of_int env i =
make_judge (Constr.mkInt i) (type_of_int env)
@@ -664,17 +669,7 @@ let judge_of_case env ci pj cj lfj =
(* Building type of primitive operators and type *)
-open CPrimitives
-
let check_primitive_type env op_t t =
- match op_t with
- | OT_type PT_int63 ->
- (try
- default_conv ~l2r:false CUMUL env mkSet t
- with NotConvertible ->
- CErrors.user_err Pp.(str"Was expecting the sort of this primitive type to be Set"))
- | OT_op p ->
- (try
- default_conv ~l2r:false CUMUL env (type_of_prim env p) t
- with NotConvertible ->
- CErrors.user_err Pp.(str"Not the expected type for this primitive"))
+ let inft = type_of_prim_or_type env op_t in
+ try default_conv ~l2r:false CUMUL env inft t
+ with NotConvertible -> error_incorrect_primitive env (make_judge op_t inft) t
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 07:41:03 +0000