Transfers to checker ("let"s in inductive arities + Coq root read-only).

- Support for let's in the signature of the arity of an inductive type was
  in the kernel part of commit 12273,
- Support for binding Coq root read-only in -R option was in commit 12220.

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

8 files changed, 36 insertions, 15 deletions

diff --git a/checker/checker.ml b/checker/checker.ml
index b982456aa..85ad129c9 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -90,23 +90,16 @@ let includes = ref []
 let push_include (s, alias) = includes := (s,alias,false) :: !includes
 let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes
 
-let check_coq_overwriting p = 
-  if string_of_id (list_last (repr_dirpath p)) = "Coq" then
-    error "The \"Coq\" logical root directory is reserved for the Coq library"
-
 let set_default_include d =
   push_include (d, Check.default_root_prefix)
 let set_default_rec_include d =
   let p = Check.default_root_prefix in
-  check_coq_overwriting p; 
   push_rec_include (d, p)
 let set_include d p =
   let p = dirpath_of_string p in
-  check_coq_overwriting p;
   push_include (d,p)
 let set_rec_include d p =
   let p = dirpath_of_string p in
-  check_coq_overwriting p;
   push_rec_include(d,p)
 
 (* Initializes the LoadPath *)
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 1ccdf8ea4..67f44c4d3 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -486,6 +486,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;
 
@@ -584,6 +587,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/checker/declarations.mli b/checker/declarations.mli
index b376151ca..c5b676bda 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -86,6 +86,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/checker/indtypes.ml b/checker/indtypes.ml
index 4c9b3d61d..9ff21bc3f 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -136,6 +136,7 @@ let small_unit constrsinfos =
 (* check information related to inductive arity *)
 let typecheck_arity env params inds =
   let nparamargs = rel_context_nhyps params in
+  let nparamdecls = rel_context_length params in
   let check_arity arctxt = function
       Monomorphic mar ->
         let ar = mar.mind_user_arity in
@@ -154,8 +155,12 @@ let typecheck_arity env params inds =
         (* Arities (with params) are typed-checked here *)
         let arity = check_arity ar_ctxt ind.mind_arity in
         (* mind_nrealargs *)
-        if ind.mind_nrealargs <> rel_context_nhyps ar_ctxt - nparamargs then
+	let nrealargs = rel_context_nhyps ar_ctxt - nparamargs in
+        if ind.mind_nrealargs <> nrealargs then
              failwith "bad number of real inductive arguments";
+	let nrealargs_ctxt = rel_context_length ar_ctxt - nparamdecls in
+        if ind.mind_nrealargs_ctxt <> nrealargs_ctxt then
+             failwith "bad length of real inductive arguments signature";
 	(* We do not need to generate the universe of full_arity; if
 	   later, after the validation of the inductive definition,
 	   full_arity is used as argument or subject to cast, an
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 05ab5a846..f1c8bea2a 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -253,16 +253,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 (Rel(n+p)::l) (p+1)
+let extended_rel_list n hyps =
+  let rec reln l p = function
+    | (_,None,_) :: hyps -> reln (Rel (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 
-    (Ind ind, (List.map (lift nrealargs) params)@(rel_list 0 nrealargs))
+    (Ind 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
diff --git a/checker/reduction.ml b/checker/reduction.ml
index c398f0a41..d81cfe352 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -107,6 +107,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 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/checker/reduction.mli b/checker/reduction.mli
index eb50ae32e..47590edb3 100644
--- a/checker/reduction.mli
+++ b/checker/reduction.mli
@@ -40,6 +40,9 @@ val vm_conv : conv_pb -> constr 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 -> constr -> constr list -> constr
 
diff --git a/checker/term.ml b/checker/term.ml
index f245d1551..f5b2496c8 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -28,7 +28,7 @@ type metavariable = int
 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;