aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-03-25 11:26:21 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-03-25 12:11:50 +0100
commitc1729637d4fe32ebe0268eb338fcf4d032bb5df7 (patch)
treeea8b21f82964e360eb941d04fd8ce06c2fccc3a8 /pretyping
parent1a519fc37e703b014e3bcc77de01edd82aabea5f (diff)
Fully fixing bug #3491 (anomaly when building _rect scheme in the
presence of let-ins and recursively non-uniform parameters). The bug was in the List.chop of Inductiveops.get_arity which was wrong in the presence of let-ins and recursively non-uniform parameters. The bug #3491 showed up because, in addition to have let-ins, it was wrongly detected as having recursively non-uniform parameters. Also added some comments in declarations.mli.
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/inductiveops.ml16
-rw-r--r--pretyping/inductiveops.mli10
2 files changed, 17 insertions, 9 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 7f6a4a644..dfdc24d48 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -365,14 +365,16 @@ let get_arity env ((ind,u),params) =
let (mib,mip) = Inductive.lookup_mind_specif env ind in
let parsign =
(* Dynamically detect if called with an instance of recursively
- uniform parameter only or also of non recursively uniform
+ uniform parameter only or also of recursively non-uniform
parameters *)
- let parsign = mib.mind_params_ctxt in
- let nnonrecparams = mib.mind_nparams - mib.mind_nparams_rec in
- if Int.equal (List.length params) (rel_context_nhyps parsign - nnonrecparams) then
- snd (List.chop nnonrecparams mib.mind_params_ctxt)
- else
- parsign in
+ let nparams = List.length params in
+ if Int.equal nparams mib.mind_nparams then
+ mib.mind_params_ctxt
+ else begin
+ assert (Int.equal nparams mib.mind_nparams_rec);
+ let nnonrecparamdecls = List.length mib.mind_params_ctxt - mib.mind_nparams_rec in
+ snd (List.chop nnonrecparamdecls mib.mind_params_ctxt)
+ end in
let parsign = Vars.subst_instance_context u parsign in
let arproperlength = List.length mip.mind_arity_ctxt - List.length parsign in
let arsign,_ = List.chop arproperlength mip.mind_arity_ctxt in
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index af1783b70..7959759a3 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -25,7 +25,9 @@ val type_of_constructors : env -> pinductive -> types array
(** Return constructor types in normal form *)
val arities_of_constructors : env -> pinductive -> types array
-(** An inductive type with its parameters *)
+(** An inductive type with its parameters (transparently supports
+ reasoning either with only recursively uniform parameters or with all
+ parameters including the recursively non-uniform ones *)
type inductive_family
val make_ind_family : inductive puniverses * constr list -> inductive_family
val dest_ind_family : inductive_family -> inductive puniverses * constr list
@@ -138,10 +140,14 @@ val lift_constructor : int -> constructor_summary -> constructor_summary
val get_constructor :
pinductive * mutual_inductive_body * one_inductive_body * constr list ->
int -> constructor_summary
-val get_arity : env -> inductive_family -> rel_context * sorts_family
val get_constructors : env -> inductive_family -> constructor_summary array
val get_projections : env -> inductive_family -> constant array option
+(** [get_arity] returns the arity of the inductive family instantiated
+ with the parameters; if recursively non-uniform parameters are not
+ part of the inductive family, they appears in the arity *)
+val get_arity : env -> inductive_family -> rel_context * sorts_family
+
val build_dependent_constructor : constructor_summary -> constr
val build_dependent_inductive : env -> inductive_family -> constr
val make_arity_signature : env -> bool -> inductive_family -> rel_context