aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/cic.mli7
-rw-r--r--checker/declarations.ml1
-rw-r--r--checker/inductive.ml3
-rw-r--r--kernel/constr.ml9
-rw-r--r--kernel/constr.mli3
-rw-r--r--kernel/declarations.mli4
-rw-r--r--kernel/indtypes.ml8
-rw-r--r--kernel/inductive.ml3
-rw-r--r--kernel/term.ml1
-rw-r--r--kernel/term.mli1
-rw-r--r--lib/hashset.ml1
-rw-r--r--lib/hashset.mli1
-rw-r--r--pretyping/inductiveops.ml1
-rw-r--r--pretyping/term_dnet.ml5
14 files changed, 38 insertions, 10 deletions
diff --git a/checker/cic.mli b/checker/cic.mli
index bfea85327..380093c57 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -60,7 +60,8 @@ type case_printing =
type case_info =
{ ci_ind : inductive;
ci_npar : int;
- ci_cstr_ndecls : int array; (** number of real args of each constructor *)
+ ci_cstr_ndecls : int array; (* number of pattern vars of each constructor (with let's)*)
+ ci_cstr_nargs : int array; (* number of pattern vars of each constructor (w/o let's) *)
ci_pp_info : case_printing (** not interpreted by the kernel *)
}
@@ -241,6 +242,10 @@ type one_inductive_body = {
(** Length of the signature of the constructors (with let, w/o params)
(not used in the kernel) *)
+ mind_consnrealargs : int array;
+ (** Length of the signature of the constructors (w/o let, w/o params)
+ (not used in the kernel) *)
+
mind_recargs : wf_paths; (** Signature of recursive arguments in the constructors *)
(** {8 Datas for bytecode compilation } *)
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 79ba6de22..baf2e57db 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -510,6 +510,7 @@ let subst_arity sub = function
let subst_mind_packet sub mbp =
{ mind_consnames = mbp.mind_consnames;
mind_consnrealdecls = mbp.mind_consnrealdecls;
+ mind_consnrealargs = mbp.mind_consnrealargs;
mind_typename = mbp.mind_typename;
mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc;
mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt;
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 40a9bc316..e6a24f705 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -352,7 +352,8 @@ let check_case_info env indsp ci =
if
not (eq_ind indsp ci.ci_ind) ||
(mib.mind_nparams <> ci.ci_npar) ||
- (mip.mind_consnrealdecls <> ci.ci_cstr_ndecls)
+ (mip.mind_consnrealdecls <> ci.ci_cstr_ndecls) ||
+ (mip.mind_consnrealargs <> ci.ci_cstr_nargs)
then raise (TypeError(env,WrongCaseInfo(indsp,ci)))
(************************************************************************)
diff --git a/kernel/constr.ml b/kernel/constr.ml
index b1e3abbed..e9e21d30d 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -43,7 +43,8 @@ type case_printing =
type case_info =
{ ci_ind : inductive;
ci_npar : int;
- ci_cstr_ndecls : int array; (* number of pattern vars of each constructor *)
+ ci_cstr_ndecls : int array; (* number of pattern vars of each constructor (with let's)*)
+ ci_cstr_nargs : int array; (* number of pattern vars of each constructor (w/o let's) *)
ci_pp_info : case_printing (* not interpreted by the kernel *)
}
@@ -773,6 +774,7 @@ struct
ci.ci_ind == ci'.ci_ind &&
Int.equal ci.ci_npar ci'.ci_npar &&
Array.equal Int.equal ci.ci_cstr_ndecls ci'.ci_cstr_ndecls && (* we use [Array.equal] on purpose *)
+ Array.equal Int.equal ci.ci_cstr_nargs ci'.ci_cstr_nargs && (* we use [Array.equal] on purpose *)
pp_info_equal ci.ci_pp_info ci'.ci_pp_info (* we use (=) on purpose *)
open Hashset.Combine
let hash_pp_info info =
@@ -788,8 +790,9 @@ struct
let h1 = ind_hash ci.ci_ind in
let h2 = Int.hash ci.ci_npar in
let h3 = Array.fold_left combine 0 ci.ci_cstr_ndecls in
- let h4 = hash_pp_info ci.ci_pp_info in
- combine4 h1 h2 h3 h4
+ let h4 = Array.fold_left combine 0 ci.ci_cstr_nargs in
+ let h5 = hash_pp_info ci.ci_pp_info in
+ combine5 h1 h2 h3 h4 h5
end
module Hcaseinfo = Hashcons.Make(CaseinfoHash)
diff --git a/kernel/constr.mli b/kernel/constr.mli
index f2d9ac9f5..82a2de094 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -25,7 +25,8 @@ type case_printing =
type case_info =
{ ci_ind : inductive;
ci_npar : int;
- ci_cstr_ndecls : int array; (** number of real args of each constructor *)
+ ci_cstr_ndecls : int array; (* number of pattern vars of each constructor (with let's)*)
+ ci_cstr_nargs : int array; (* number of pattern vars of each constructor (w/o let's) *)
ci_pp_info : case_printing (** not interpreted by the kernel *)
}
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index e6025790a..1e94e243c 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -110,6 +110,10 @@ type one_inductive_body = {
(** Length of the signature of the constructors (with let, w/o params)
(not used in the kernel) *)
+ mind_consnrealargs : int array;
+ (** Length of the signature of the constructors (w/o let, w/o params)
+ (not used in the kernel) *)
+
mind_recargs : wf_paths; (** Signature of recursive arguments in the constructors *)
(** {8 Datas for bytecode compilation } *)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 214aac5ec..2defb66f4 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -630,9 +630,12 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
(* Type of constructors in normal form *)
let splayed_lc = Array.map (dest_prod_assum env_ar) lc in
let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in
- let consnrealargs =
+ let consnrealdecls =
Array.map (fun (d,_) -> rel_context_length d - rel_context_length params)
splayed_lc in
+ let consnrealargs =
+ Array.map (fun (d,_) -> rel_context_nhyps d - rel_context_nhyps params)
+ splayed_lc in
(* Elimination sorts *)
let arkind,kelim = match ar_kind with
| Inr (param_levels,lev) ->
@@ -668,7 +671,8 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
mind_nrealargs_ctxt = rel_context_length ar_sign - nparamdecls;
mind_kelim = kelim;
mind_consnames = Array.of_list cnames;
- mind_consnrealdecls = consnrealargs;
+ mind_consnrealdecls = consnrealdecls;
+ mind_consnrealargs = consnrealargs;
mind_user_lc = lc;
mind_nf_lc = nf_lc;
mind_recargs = recarg;
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index c0857566d..2b2caaf3b 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -370,7 +370,8 @@ let check_case_info env indsp ci =
if
not (eq_ind indsp ci.ci_ind) ||
not (Int.equal mib.mind_nparams ci.ci_npar) ||
- not (Array.equal Int.equal mip.mind_consnrealdecls ci.ci_cstr_ndecls)
+ not (Array.equal Int.equal mip.mind_consnrealdecls ci.ci_cstr_ndecls) ||
+ not (Array.equal Int.equal mip.mind_consnrealargs ci.ci_cstr_nargs)
then raise (TypeError(env,WrongCaseInfo(indsp,ci)))
(************************************************************************)
diff --git a/kernel/term.ml b/kernel/term.ml
index 44a10aa35..24fe6d962 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -47,6 +47,7 @@ type case_info = Constr.case_info =
{ ci_ind : inductive;
ci_npar : int;
ci_cstr_ndecls : int array;
+ ci_cstr_nargs : int array;
ci_pp_info : case_printing
}
diff --git a/kernel/term.mli b/kernel/term.mli
index dab1d2cea..f2f5e8495 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -46,6 +46,7 @@ type case_info = Constr.case_info =
{ ci_ind : inductive;
ci_npar : int;
ci_cstr_ndecls : int array;
+ ci_cstr_nargs : int array;
ci_pp_info : case_printing
}
diff --git a/lib/hashset.ml b/lib/hashset.ml
index 8c40e5500..f8d4274de 100644
--- a/lib/hashset.ml
+++ b/lib/hashset.ml
@@ -202,5 +202,6 @@ module Combine = struct
let combine x y = x * alpha + y
let combine3 x y z = combine x (combine y z)
let combine4 x y z t = combine x (combine3 y z t)
+ let combine5 x y z t u = combine x (combine4 y z t u)
let combinesmall x y = beta * x + y
end
diff --git a/lib/hashset.mli b/lib/hashset.mli
index 2041b2ec2..2e5b814a7 100644
--- a/lib/hashset.mli
+++ b/lib/hashset.mli
@@ -43,4 +43,5 @@ module Combine : sig
val combinesmall : int -> int -> int
val combine3 : int -> int -> int -> int
val combine4 : int -> int -> int -> int -> int
+ val combine5 : int -> int -> int -> int -> int -> int
end
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 812900ea8..775795ce0 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -183,6 +183,7 @@ let make_case_info env ind style =
{ ci_ind = ind;
ci_npar = mib.mind_nparams;
ci_cstr_ndecls = mip.mind_consnrealdecls;
+ ci_cstr_nargs = mip.mind_consnrealargs;
ci_pp_info = print_info }
(*s Useful functions *)
diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml
index d22e032df..10ec651fa 100644
--- a/pretyping/term_dnet.ml
+++ b/pretyping/term_dnet.ml
@@ -86,7 +86,10 @@ struct
if c = 0 then
let c = Int.compare ci1.ci_npar ci2.ci_npar in
if c = 0 then
- Array.compare Int.compare ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls
+ let c = Array.compare Int.compare ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls in
+ if c = 0 then
+ Array.compare Int.compare ci1.ci_cstr_nargs ci2.ci_cstr_nargs
+ else c
else c
else c
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 01:14:37 +0000