diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/constr.ml | 9 | ||||
| -rw-r--r-- | kernel/constr.mli | 3 | ||||
| -rw-r--r-- | kernel/declarations.mli | 4 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 8 | ||||
| -rw-r--r-- | kernel/inductive.ml | 3 | ||||
| -rw-r--r-- | kernel/term.ml | 1 | ||||
| -rw-r--r-- | kernel/term.mli | 1 |
7 files changed, 22 insertions, 7 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index b1e3abbedd..e9e21d30d9 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 f2d9ac9f54..82a2de0945 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 e6025790a3..1e94e243c0 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 214aac5ec0..2defb66f4b 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 c0857566df..2b2caaf3bf 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 44a10aa355..24fe6d9622 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 dab1d2ceab..f2f5e8495d 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 } |