Ensures that let-in's in arities of inductive types work well. Maybe not

very useful in practice but as soon as let-in's were not forbidden in
the internal data structure, better to do it. Moreover, this gets
closer to the view were inductive definitions are uniformly built from
"contexts". (checker not changed!)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12273 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 38 insertions, 11 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 725859321..8b2402bb5 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -135,6 +135,9 @@ type one_inductive_body = {
  (* Number of expected real arguments of the type (no let, no params) *)
     mind_nrealargs : int;
 
+ (* Length of realargs context (with let, no params) *)
+    mind_nrealargs_ctxt : int;
+
  (* List of allowed elimination sorts *)
     mind_kelim : sorts_family list;
 
@@ -223,6 +226,7 @@ let subst_mind_packet sub mbp =
     mind_arity = subst_arity sub mbp.mind_arity;
     mind_user_lc = array_smartmap (subst_mps sub) mbp.mind_user_lc;
     mind_nrealargs = mbp.mind_nrealargs;
+    mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt;
     mind_kelim = mbp.mind_kelim;
     mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*); 
     mind_nb_constant = mbp.mind_nb_constant;
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index fb8317cdc..454debd73 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -115,6 +115,9 @@ type one_inductive_body = {
  (* Number of expected real arguments of the type (no let, no params) *)
     mind_nrealargs : int;
 
+ (* Length of realargs context (with let, no params) *)
+    mind_nrealargs_ctxt : int;
+
  (* List of allowed elimination sorts *)
     mind_kelim : sorts_family list;
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 4aac096fc..ccf9b3f6c 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -588,6 +588,7 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
   (* Compute the set of used section variables *)
   let hyps =  used_section_variables env inds in
   let nparamargs = rel_context_nhyps params in
+  let nparamdecls = rel_context_length params in
   (* Check one inductive *)
   let build_one_packet (id,cnames,lc,(ar_sign,ar_kind)) recarg =
     (* Type of constructors in normal form *)
@@ -629,6 +630,7 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
 	mind_arity = arkind;
 	mind_arity_ctxt = ar_sign;
 	mind_nrealargs = rel_context_nhyps ar_sign - nparamargs;
+	mind_nrealargs_ctxt = rel_context_length ar_sign - nparamdecls;
 	mind_kelim = kelim;
 	mind_consnames = Array.of_list cnames;
 	mind_consnrealdecls = consnrealargs;
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 23cd99d1e..6da102a94 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -270,16 +270,20 @@ let get_instantiated_arity (mib,mip) params =
 
 let elim_sorts (_,mip) = mip.mind_kelim
 
-let rel_list n m = 
-  let rec reln l p = 
-    if p>m then l else reln (mkRel(n+p)::l) (p+1)
+let extended_rel_list n hyps =
+  let rec reln l p = function
+    | (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps
+    | (_,Some _,_) :: hyps -> reln l (p+1) hyps
+    | [] -> l
   in 
-  reln [] 1
+  reln [] 1 hyps
 
 let build_dependent_inductive ind (_,mip) params =
-  let nrealargs = mip.mind_nrealargs in
+  let realargs,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
   applist 
-    (mkInd ind, (List.map (lift nrealargs) params)@(rel_list 0 nrealargs))
+    (mkInd ind,
+       List.map (lift mip.mind_nrealargs_ctxt) params 
+       @ extended_rel_list 0 realargs)
 
 (* This exception is local *)
 exception LocalArity of (sorts_family * sorts_family * arity_error) option
@@ -309,6 +313,8 @@ let is_correct_arity env c pj ind specif params =
             with NotConvertible -> raise (LocalArity None) in
 	  check_allowed_sort ksort specif;
 	  Constraint.union u univ
+      | _, (_,Some _,_ as d)::ar' ->
+	  srec (push_rel d env) (lift 1 pt') ar' u
       | _ ->
 	  raise (LocalArity None)
   in 
@@ -339,8 +345,8 @@ let build_branches_type ind (_,mip as specif) params p =
 
 (* [p] is the predicate, [c] is the match object, [realargs] is the
    list of real args of the inductive type *)
-let build_case_type p c realargs =
-  beta_appvect p (Array.of_list (realargs@[c]))
+let build_case_type n p c realargs =
+  betazeta_appvect (n+1) p (Array.of_list (realargs@[c]))
 
 let type_case_branches env (ind,largs) pj c =
   let specif = lookup_mind_specif env ind in 
@@ -349,7 +355,7 @@ let type_case_branches env (ind,largs) pj c =
   let p = pj.uj_val in
   let univ = is_correct_arity env c pj ind specif params in
   let lc = build_branches_type ind specif params p in
-  let ty = build_case_type p c realargs in
+  let ty = build_case_type (snd specif).mind_nrealargs_ctxt p c realargs in
   (lc, ty, univ)
 
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index f1a44b5ca..89f1b443b 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -117,6 +117,15 @@ let beta_appvect c v =
       | _ -> applist (substl env t, stack) in
   stacklam [] c (Array.to_list v)
 
+let betazeta_appvect n c v =
+  let rec stacklam n env t stack =
+    if n = 0 then applist (substl env t, stack) else
+    match kind_of_term t, stack with
+        Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
+      | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack
+      | _ -> anomaly "Not enough lambda/let's" in
+  stacklam n [] c (Array.to_list v)
+
 (********************************************************************)
 (*                         Conversion                               *)
 (********************************************************************)
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index de926bd1d..996051329 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -66,6 +66,9 @@ val default_conv_leq : types conversion_function
 (* Builds an application node, reducing beta redexes it may produce. *) 
 val beta_appvect : constr -> constr array -> constr
 
+(* Builds an application node, reducing the [n] first beta-zeta redexes. *) 
+val betazeta_appvect : int -> constr -> constr array -> constr
+
 (* Pseudo-reduction rule  Prod(x,A,B) a --> B[x\a] *)
 val hnf_prod_applist : env -> types -> constr list -> types
 
diff --git a/kernel/term.ml b/kernel/term.ml
index da8a77883..8a2c3278c 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -26,7 +26,7 @@ type metavariable = int
 (* This defines Cases annotations *)
 type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
 type case_printing =
-  { ind_nargs : int; (* number of real args of the inductive type *)
+  { ind_nargs : int; (* length of the arity of the inductive type *)
     style     : case_style }
 type case_info =
   { ci_ind        : inductive;
diff --git a/kernel/term.mli b/kernel/term.mli
index 8f45e39f0..bc1cac44a 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -42,7 +42,7 @@ type metavariable = int
 (*s Case annotation *)
 type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
 type case_printing =
-  { ind_nargs : int; (* number of real args of the inductive type *)
+  { ind_nargs : int; (* length of the arity of the inductive type *)
     style     : case_style }
 (* the integer is the number of real args, needed for reduction *)
 type case_info =