On laisse les LetIn dans les types des constructeurs et des éliminations

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

4 files changed, 46 insertions, 14 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index ee58603117..c29d4385d5 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -272,9 +272,10 @@ let listrec_mconstr env ntypes nparams i indlc =
         | IsLetIn (na,b,t,d) -> 
 	    assert (largs = []);
             if not (noccur_between n ntypes b & noccur_between n ntypes t) then
-	      raise (IllFormedInd (LocalNonPos n));
-            let recarg = check_pos n b in 
-	    check_constr_rec lrec (n+1) d 
+	      check_constr_rec lrec n (subst1 b d)
+	    else
+              let recarg = check_pos n b in 
+	      check_constr_rec lrec (n+1) d 
 
 	| hd ->
 	    if check_head then
@@ -320,8 +321,9 @@ let cci_inductive env env_ar kind nparams finite inds cst =
 	Some (body_of_type ar) in
     let kelim = allowed_sorts issmall isunit ar_sort in
     let lc_bodies = Array.map body_of_type lc in
-    let splayed_lc = Array.map (splay_prod env Evd.empty) lc_bodies in
-    let nf_lc = Array.map (fun (d,b) -> prod_it b d) splayed_lc in
+    let splayed_lc = Array.map (splay_prod_assum env Evd.empty) lc_bodies in
+    let nf_lc = Array.map
+		  (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in
     let nf_typed_lc,user_lc =
       if nf_lc = lc_bodies then lc,None
       else
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index c353e47657..0e47053c62 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -169,12 +169,15 @@ let betaiotaevar = [BETA;IOTA;EVAR]
 (* Compact Implementation *)
 type flags = int
 let fbeta = 1 and fdelta = 2 and fevar = 4 and feta = 8 and fiota = 16
+							and fletin = 32
 
 let red_beta f = f land fbeta <> 0
 let red_delta f = f land fdelta <> 0
 let red_evar f = f land fevar <> 0
 let red_eta f = f land feta <> 0
 let red_iota f = f land fiota <> 0
+let red_letin f = f land fletin <> 0
+
 
 (* Local *)
 let beta = fbeta
@@ -183,10 +186,11 @@ let betaiota = fbeta lor fiota
 
 (* Contextual *)
 let delta = fdelta lor fevar
-let betadelta = fbeta lor fdelta lor fevar
-let betadeltaeta = fbeta lor fdelta lor fevar lor feta
-let betadeltaiota = fbeta lor fdelta lor fevar lor fiota
-let betadeltaiotaeta = fbeta lor fdelta lor fevar lor fiota lor feta
+let betadelta = fbeta lor fdelta lor fletin lor fevar
+let betadeltaeta = fbeta lor fdelta lor fletin lor fevar lor feta
+let betadeltaiota = fbeta lor fdelta lor fletin lor fevar lor fiota
+let betadeltaiota_nolet = fbeta lor fdelta lor fevar lor fiota
+let betadeltaiotaeta = fbeta lor fdelta lor fletin lor fevar lor fiota lor feta
 let betaiotaevar = fbeta lor fiota lor fevar
 
 (* Beta Reduction tools *)
@@ -271,7 +275,7 @@ let whd_state_gen flags env sigma =
 	  (match constant_opt_value env const with
 	     | Some  body -> whrec (body, stack)
 	     | None -> s)
-      | IsLetIn (_,b,_,c) when red_delta flags -> stacklam whrec [b] c stack
+      | IsLetIn (_,b,_,c) when red_letin flags -> stacklam whrec [b] c stack
       | IsCast (c,_) -> whrec (c, stack)
       | IsAppL (f,cl)  -> whrec (f, append_stack cl stack)
       | IsLambda (_,_,c) ->
@@ -660,12 +664,18 @@ let whd_betadeltaiotaeta_state env sigma =
   whrec
 *)
 
-let whd_betadeltaiotaeta_state e = whd_state_gen betadeltaiota e
+let whd_betadeltaiotaeta_state e = whd_state_gen betadeltaiotaeta e
 let whd_betadeltaiotaeta_stack env sigma x =
   appterm_of_stack (whd_betadeltaiotaeta_state env sigma (x, empty_stack))
 let whd_betadeltaiotaeta env sigma x = 
   app_stack (whd_betadeltaiotaeta_state env sigma (x, empty_stack))
 
+let whd_betadeltaiota_nolet_state e = whd_state_gen betadeltaiota_nolet e
+let whd_betadeltaiota_nolet_stack env sigma x =
+  appterm_of_stack (whd_betadeltaiota_nolet_state env sigma (x, empty_stack))
+let whd_betadeltaiota_nolet env sigma x = 
+  app_stack (whd_betadeltaiota_nolet_state env sigma (x, empty_stack))
+
 (********************************************************************)
 (*                         Conversion                               *)
 (********************************************************************)
@@ -949,6 +959,17 @@ let splay_prod env sigma =
   in 
   decrec []
 
+let splay_prod_assum env sigma = 
+  let rec prodec_rec l c =
+    let t = whd_betadeltaiota_nolet env sigma c in
+    match kind_of_term c with
+    | IsProd (x,t,c)  -> prodec_rec (Sign.add_rel_decl (x,outcast_type t) l) c
+    | IsLetIn (x,b,t,c) -> prodec_rec (Sign.add_rel_def (x,b,outcast_type t) l) c
+    | IsCast (c,_)    -> prodec_rec l c
+    | _               -> l,c
+  in 
+  prodec_rec Sign.empty_rel_context
+
 let splay_arity env sigma c =
   let l, c = splay_prod env sigma c in
   match kind_of_term c with
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index d1a092ae7f..7bb43b0556 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -115,6 +115,8 @@ val splay_arity : env -> 'a evar_map -> constr -> (name * constr) list * sorts
 val sort_of_arity : env -> constr -> sorts
 val decomp_n_prod : 
   env -> 'a evar_map -> int -> constr -> Sign.rel_context * constr
+val splay_prod_assum :
+  env -> 'a evar_map -> constr -> Sign.rel_context * constr
 
 type 'a miota_args = {
   mP      : constr;     (* the result type *)
diff --git a/library/indrec.ml b/library/indrec.ml
index b39f834f4e..2a2e83721d 100644
--- a/library/indrec.ml
+++ b/library/indrec.ml
@@ -78,7 +78,7 @@ let mis_make_case_com depopt env sigma mispec kind =
 
 (*
  * t is the type of the constructor co and recargs is the information on 
- * the recursive calls.                                                  
+ * the recursive calls. (It is assumed to be in form given by the user).
  * build the type of the corresponding branch of the recurrence principle
  * assuming f has this type, branch_rec gives also the term 
  *   [x1]..[xk](f xi (F xi) ...) to be put in the corresponding branch of 
@@ -108,7 +108,7 @@ let type_rec_branch dep env sigma (vargs,depPvect,decP) co t recargs =
     prec 0 
   in
   let rec process_constr i c recargs co = 
-    let c', largs = whd_betadeltaiota_stack env sigma c in
+    let c', largs = whd_stack c in
     match kind_of_term c' with 
       | IsProd (n,t,c_0) ->
 	  assert (largs = []);
@@ -131,6 +131,10 @@ let type_rec_branch dep env sigma (vargs,depPvect,decP) co t recargs =
 		 make_prod_dep (dep or dep') env
                    (n,t,mkArrow t_0 (process_constr (i+2) (lift 1 c_0) rest
 				       (mkAppL (lift 2 co, [|mkRel 2|])))))
+      | IsLetIn (n,b,t,c_0) ->
+	  assert (largs = []);
+	  mkLetIn (n,b,t,process_constr (i+1) c_0 recargs (lift 1 co))
+
       | IsMutInd ((_,tyi),_) -> 
       	  let nP = match depPvect.(tyi) with 
 	    | Some(_,p) -> lift (i+decP) p
@@ -179,7 +183,10 @@ let make_rec_branch_arg env sigma (nparams,fvect,decF) f cstr recargs =
 		 (n,incast_type t,process_constr (i+1)
 		    (whd_beta (applist (lift 1 f, [(mkRel 1); arg])))
 		    (cprest,rest)))
-    | (n,Some c,t)::cprest, rest -> failwith "TODO"
+    | (n,Some c,t)::cprest, rest ->
+	       mkLetIn
+		 (n,c,incast_type t,
+		  process_constr (i+1) (lift 1 f) (cprest,rest))
     | [],[] -> f
     | _,[] | [],_ -> anomaly "process_constr"