adpated the checker to handle coomutative cuts and lazyness

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

13 files changed, 317 insertions, 249 deletions

diff --git a/checker/declarations.ml b/checker/declarations.ml
index 699f6c90ee..df8abb2567 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -20,7 +20,7 @@ type polymorphic_arity = {
   poly_level : Univ.universe;
 }
 let val_pol_arity =
-  val_tuple"polyorphic_arity"[|val_list(val_opt val_univ);val_univ|]
+  val_tuple ~name:"polyorphic_arity"[|val_list(val_opt val_univ);val_univ|]
 
 type constant_type =
   | NonPolymorphicType of constr
@@ -74,7 +74,7 @@ let val_res =
 
 let val_subst =
   val_map ~name:"substitution"
-    val_subst_dom (val_tuple "substition range" [|val_mp;val_res|])
+    val_subst_dom (val_tuple ~name:"substition range" [|val_mp;val_res|])
 
 
 let fold_subst fb fp =
@@ -660,7 +660,7 @@ type constant_body = {
     const_opaque : bool;
     const_inline : bool}
 
-let val_cb = val_tuple "constant_body"
+let val_cb = val_tuple ~name:"constant_body"
   [|val_nctxt;
     val_opt val_cstr_subst;
     val_cst_type;
@@ -679,14 +679,14 @@ let subst_rel_context sub = list_smartmap (subst_rel_declaration sub)
 
 type recarg =
   | Norec
-  | Mrec of int
+  | Mrec of inductive
   | Imbr of inductive
 let val_recarg = val_sum "recarg" 1 (* Norec *)
-  [|[|val_int|] (* Mrec *);[|val_ind|] (* Imbr *)|]
+  [|[|val_ind|] (* Mrec *);[|val_ind|] (* Imbr *)|]
 
 let subst_recarg sub r = match r with
-  | Norec | Mrec _  -> r
-  | Imbr (kn,i) -> let kn' = subst_ind sub kn in
+  | Norec  -> r
+  | (Mrec(kn,i)|Imbr (kn,i)) -> let kn' = subst_ind sub kn in
       if kn==kn' then r else Imbr (kn',i)
 
 type wf_paths = recarg Rtree.t
@@ -724,7 +724,7 @@ type monomorphic_inductive_arity = {
   mind_sort : sorts;
 }
 let val_mono_ind_arity =
-  val_tuple"monomorphic_inductive_arity"[|val_constr;val_sort|]
+  val_tuple ~name:"monomorphic_inductive_arity"[|val_constr;val_sort|]
 
 type inductive_arity =
 | Monomorphic of monomorphic_inductive_arity
@@ -784,7 +784,7 @@ type one_inductive_body = {
     mind_reloc_tbl :  reloc_table;
   }
 
-let val_one_ind = val_tuple "one_inductive_body"
+let val_one_ind = val_tuple ~name:"one_inductive_body"
   [|val_id;val_rctxt;val_ind_arity;val_array val_id;val_array val_constr;
     val_int;val_int;val_list val_sortfam;val_array val_constr;val_array val_int;
     val_wfp;val_int;val_int;no_val|]
@@ -820,7 +820,7 @@ type mutual_inductive_body = {
     mind_constraints : Univ.constraints;
 
   }
-let val_ind_pack = val_tuple "mutual_inductive_body"
+let val_ind_pack = val_tuple ~name:"mutual_inductive_body"
   [|val_array val_one_ind;val_bool;val_bool;val_int;val_nctxt;
     val_int; val_int; val_rctxt;val_cstrs|]
 
@@ -923,7 +923,7 @@ let rec val_sfb o = val_sum "struct_field_body" 0
     [|val_module|];   (* SFBmodule *)
     [|val_modtype|]   (* SFBmodtype *)
   |] o
-and val_sb o = val_list (val_tuple"label*sfb"[|val_id;val_sfb|]) o
+and val_sb o = val_list (val_tuple ~name:"label*sfb"[|val_id;val_sfb|]) o
 and val_seb o = val_sum "struct_expr_body" 0
   [|[|val_mp|];                      (* SEBident *)
     [|val_uid;val_modtype;val_seb|]; (* SEBfunctor *)
@@ -934,10 +934,10 @@ and val_seb o = val_sum "struct_expr_body" 0
 and val_with o = val_sum "with_declaration_body" 0
   [|[|val_list val_id;val_mp|];
     [|val_list val_id;val_cb|]|] o
-and val_module o = val_tuple "module_body"
+and val_module o = val_tuple ~name:"module_body"
   [|val_mp;val_opt val_seb;val_seb;
     val_opt val_seb;val_cstrs;val_res;no_val|] o
-and val_modtype o = val_tuple "module_type_body"
+and val_modtype o = val_tuple ~name:"module_type_body"
   [|val_mp;val_seb;val_opt val_seb;val_cstrs;val_res|] o
 
 
diff --git a/checker/declarations.mli b/checker/declarations.mli
index b39fd6f2f4..b356ede17c 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -42,13 +42,14 @@ type constant_body = {
 
 type recarg =
   | Norec
-  | Mrec of int
+  | Mrec of inductive
   | Imbr of inductive
 
 type wf_paths = recarg Rtree.t
 
 val mk_norec : wf_paths
 val mk_paths : recarg -> wf_paths list array -> wf_paths
+val dest_recarg : wf_paths -> recarg
 val dest_subterms : wf_paths -> wf_paths list array
 
 type monomorphic_inductive_arity = {
@@ -211,6 +212,6 @@ val subst_module : substitution -> module_body -> module_body
 val join : substitution -> substitution -> substitution
 
 (* Validation *)
-val val_eng : Obj.t -> unit
-val val_module : Obj.t -> unit
-val val_modtype : Obj.t -> unit
+val val_eng : Validate.func
+val val_module : Validate.func
+val val_modtype : Validate.func
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 3ad39f1de6..5de03b16d5 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -392,7 +392,7 @@ let rec ienv_decompose_prod (env,_,_,_ as ienv) n c =
 
 (* The recursive function that checks positivity and builds the list
    of recursive arguments *)
-let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc =
+let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc =
   let lparams = rel_context_length hyps in
   (* check the inductive types occur positively in [c] *)
   let rec check_pos (env, n, ntypes, ra_env as ienv) c =
@@ -494,7 +494,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc =
           with IllFormedInd err ->
             explain_ind_err (ntypes-i) env lparams c err)
       indlc
-  in mk_paths (Mrec i) irecargs
+  in mk_paths (Mrec ind) irecargs
 
 let check_subtree (t1:'a) (t2:'a) =
   if not (Rtree.compare_rtree (fun t1 t2 ->
@@ -505,16 +505,17 @@ let check_subtree (t1:'a) (t2:'a) =
     failwith "bad recursive trees"
 (* if t1=t2 then () else msg_warning (str"TODO: check recursive positions")*)
 
-let check_positivity env_ar params nrecp inds =
+let check_positivity env_ar mind params nrecp inds =
   let ntypes = Array.length inds in
-  let rc = Array.mapi (fun j t -> (Mrec j,t)) (Rtree.mk_rec_calls ntypes) in
+  let rc =
+    Array.mapi (fun j t -> (Mrec(mind,j),t)) (Rtree.mk_rec_calls ntypes) in
   let lra_ind = List.rev (Array.to_list rc) in
   let lparams = rel_context_length params in
   let check_one i mip =
     let ra_env =
       list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in
     let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
-      check_positivity_one ienv params nrecp i mip.mind_nf_lc
+      check_positivity_one ienv params nrecp (mind,i) mip.mind_nf_lc
   in
   let irecargs = Array.mapi check_one inds in
   let wfp = Rtree.mk_rec irecargs in
@@ -547,7 +548,7 @@ let check_inductive env kn mib =
   (*  - check constructor types *)
   Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets;
   (* check mind_nparams_rec: positivity condition *)
-  check_positivity env_ar params mib.mind_nparams_rec mib.mind_packets;
+  check_positivity env_ar kn params mib.mind_nparams_rec mib.mind_packets;
   (* check mind_equiv... *)
   (* Now we can add the inductive *)
   add_mind kn mib env
diff --git a/checker/inductive.ml b/checker/inductive.ml
index c1cee60639..756f434104 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -402,8 +402,10 @@ type subterm_spec =
   | Dead_code
   | Not_subterm
 
-let spec_of_tree t =
-  if Rtree.eq_rtree (=) t mk_norec then Not_subterm else Subterm(Strict,t)
+let spec_of_tree t = lazy
+  (if Rtree.eq_rtree (=) (Lazy.force t) mk_norec
+   then Not_subterm
+   else Subterm(Strict,Lazy.force t))
 
 let subterm_spec_glb =
   let glb2 s1 s2 =
@@ -427,7 +429,7 @@ type guard_env =
     (* the recarg information of inductive family *)
     recvec  : wf_paths array;
     (* dB of variables denoting subterms *)
-    genv    : subterm_spec list;
+    genv    : subterm_spec Lazy.t list;
   }
 
 let make_renv env minds recarg (kn,tyi) =
@@ -438,7 +440,7 @@ let make_renv env minds recarg (kn,tyi) =
     rel_min = recarg+2;
     inds = minds;
     recvec = mind_recvec;
-    genv = [Subterm(Large,mind_recvec.(tyi))] }
+    genv = [Lazy.lazy_from_val(Subterm(Large,mind_recvec.(tyi)))] }
 
 let push_var renv (x,ty,spec) =
   { renv with
@@ -450,11 +452,11 @@ let assign_var_spec renv (i,spec) =
   { renv with genv = list_assign renv.genv (i-1) spec }
 
 let push_var_renv renv (x,ty) =
-  push_var renv (x,ty,Not_subterm)
+  push_var renv (x,ty,Lazy.lazy_from_val Not_subterm)
 
 (* Fetch recursive information about a variable p *)
 let subterm_var p renv =
-  try List.nth renv.genv (p-1)
+  try Lazy.force (List.nth renv.genv (p-1))
   with Failure _ | Invalid_argument _ -> Not_subterm
 
 (* Add a variable and mark it as strictly smaller with information [spec]. *)
@@ -466,16 +468,25 @@ let push_ctxt_renv renv ctxt =
   { renv with
     env = push_rel_context ctxt renv.env;
     rel_min = renv.rel_min+n;
-    genv = iterate (fun ge -> Not_subterm::ge) n renv.genv }
+    genv = iterate (fun ge -> Lazy.lazy_from_val Not_subterm::ge) n renv.genv }
 
 let push_fix_renv renv (_,v,_ as recdef) =
   let n = Array.length v in
   { renv with
     env = push_rec_types recdef renv.env;
     rel_min = renv.rel_min+n;
-    genv = iterate (fun ge -> Not_subterm::ge) n renv.genv }
+    genv = iterate (fun ge -> Lazy.lazy_from_val Not_subterm::ge) n renv.genv }
 
 
+(* Definition and manipulation of the stack *)
+type stack_element = |SClosure of guard_env*constr |SArg of subterm_spec Lazy.t
+
+let push_stack_closures renv l stack = 
+  List.fold_right (fun h b -> (SClosure (renv,h))::b) l stack
+
+let push_stack_args l stack = 
+  List.fold_right (fun h b -> (SArg h)::b) l stack
+
 (******************************)
 (* Computing the recursive subterms of a term (propagation of size
    information through Cases). *)
@@ -495,36 +506,38 @@ let lookup_subterms env ind =
   let (_,mip) = lookup_mind_specif env ind in
   mip.mind_recargs
 
-(*********************************)
-
-(* Propagation of size information through Cases: if the matched
-   object is a recursive subterm then compute the information
-   associated to its own subterms.
-   Rq: if branch is not eta-long, then the recursive information
-   is not propagated to the missing abstractions *)
-let case_branches_specif renv c_spec ind lbr =
-  let rec push_branch_args renv lrec c =
-    match lrec with
-        ra::lr ->
-          let c' = whd_betadeltaiota renv.env c in
-          (match c' with
-              Lambda(x,a,b) ->
-                let renv' = push_var renv (x,a,ra) in
-                push_branch_args renv' lr b
-            | _ -> (* branch not in eta-long form: cannot perform rec. calls *)
-                (renv,c'))
-      | [] -> (renv, c) in
-  match c_spec with
-      Subterm (_,t) ->
-        let sub_spec = Array.map (List.map spec_of_tree) (dest_subterms t) in
-        assert (Array.length sub_spec = Array.length lbr);
-        array_map2 (push_branch_args renv) sub_spec lbr
-    | Dead_code ->
-        let t = dest_subterms (lookup_subterms renv.env ind) in
-        let sub_spec = Array.map (List.map (fun _ -> Dead_code)) t in
-        assert (Array.length sub_spec = Array.length lbr);
-        array_map2 (push_branch_args renv) sub_spec lbr
-    | Not_subterm -> Array.map (fun c -> (renv,c)) lbr
+let match_inductive ind ra =
+  match ra with
+    | (Mrec i | Imbr i) -> eq_ind ind i
+    | Norec -> false
+
+(* In {match c as z in ci y_s return P with |C_i x_s => t end}
+   [branches_specif renv c_spec ci] returns an array of x_s specs knowing
+   c_spec. *)
+let branches_specif renv c_spec ci =
+  let car = 
+    (* We fetch the regular tree associated to the inductive of the match.
+       This is just to get the number of constructors (and constructor
+       arities) that fit the match branches without forcing c_spec.
+       Note that c_spec might be more precise than [v] below, because of
+       nested inductive types. *)
+    let (_,mip) = lookup_mind_specif renv.env ci.ci_ind in
+    let v = dest_subterms mip.mind_recargs in
+      Array.map List.length v in
+    Array.mapi
+      (fun i nca -> (* i+1-th cstructor has arity nca *)
+	 let lvra = lazy 
+	   (match Lazy.force c_spec with
+		Subterm (_,t) when match_inductive ci.ci_ind (dest_recarg t) ->
+		  let vra = Array.of_list (dest_subterms t).(i) in
+		  assert (nca = Array.length vra);
+		  Array.map
+		    (fun t -> Lazy.force (spec_of_tree (lazy t)))
+		    vra
+	      | Dead_code -> Array.create nca Dead_code
+	      | _ -> Array.create nca Not_subterm) in
+	 list_tabulate (fun j -> lazy (Lazy.force lvra).(j)) nca)
+      car 
 
 (* [subterm_specif renv t] computes the recursive structure of [t] and
    compare its size with the size of the initial recursive argument of
@@ -532,72 +545,88 @@ let case_branches_specif renv c_spec ind lbr =
    about variables.
 *)
 
-let rec subterm_specif renv t =
+
+let rec subterm_specif renv stack t =
   (* maybe reduction is not always necessary! *)
   let f,l = decompose_app (whd_betadeltaiota renv.env t) in
-  match f with
-    | Rel k -> subterm_var k renv
-
-    | Case (ci,_,c,lbr) ->
-        if Array.length lbr = 0 then Dead_code
-        else
-          let c_spec = subterm_specif renv c in
-          let lbr_spec = case_branches_specif renv c_spec ci.ci_ind lbr in
-          let stl  =
-            Array.map (fun (renv',br') -> subterm_specif renv' br')
-              lbr_spec in
-          subterm_spec_glb stl
-
-    | Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
-(* when proving that the fixpoint f(x)=e is less than n, it is enough
-   to prove that e is less than n assuming f is less than n
-   furthermore when f is applied to a term which is strictly less than
-   n, one may assume that x itself is strictly less than n
-*)
-        let (ctxt,clfix) = dest_prod renv.env typarray.(i) in
-        let oind =
-          let env' = push_rel_context ctxt renv.env in
-          try Some(fst(find_inductive env' clfix))
-          with Not_found -> None in
-        (match oind with
-            None -> Not_subterm (* happens if fix is polymorphic *)
-          | Some ind ->
-              let nbfix = Array.length typarray in
-              let recargs = lookup_subterms renv.env ind in
-              (* pushing the fixpoints *)
-              let renv' = push_fix_renv renv recdef in
-              let renv' =
-                (* Why Strict here ? To be general, it could also be
-                   Large... *)
-                assign_var_spec renv' (nbfix-i, Subterm(Strict,recargs)) in
-              let decrArg = recindxs.(i) in
-              let theBody = bodies.(i)   in
-              let nbOfAbst = decrArg+1 in
-              let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in
-              (* pushing the fix parameters *)
-              let renv'' = push_ctxt_renv renv' sign in
-              let renv'' =
-                if List.length l < nbOfAbst then renv''
-                else
-                  let theDecrArg  = List.nth l decrArg in
-	          let arg_spec    = subterm_specif renv theDecrArg in
-                  assign_var_spec renv'' (1, arg_spec) in
-	      subterm_specif renv'' strippedBody)
-
-    | Lambda (x,a,b) ->
-        assert (l=[]);
-        subterm_specif (push_var_renv renv (x,a)) b
-
-    (* Metas and evars are considered OK *)
-    | (Meta _|Evar _) -> Dead_code
+    match f with
+      | Rel k -> subterm_var k renv
 
-    (* Other terms are not subterms *)
-    | _ -> Not_subterm
-
-
-(* Check term c can be applied to one of the mutual fixpoints. *)
-let check_is_subterm renv c =
-  match subterm_specif renv c with
+      | Case (ci,_,c,lbr) ->
+	  let stack' = push_stack_closures renv l stack in
+          let cases_spec = branches_specif renv 
+	    (lazy_subterm_specif renv [] c) ci in
+          let stl  =
+            Array.mapi (fun i br' ->
+			  let stack_br = push_stack_args (cases_spec.(i)) stack' in
+			    subterm_specif renv stack_br br')
+              lbr in
+            subterm_spec_glb stl
+
+      | Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
+	  (* when proving that the fixpoint f(x)=e is less than n, it is enough
+	     to prove that e is less than n assuming f is less than n
+	     furthermore when f is applied to a term which is strictly less than
+	     n, one may assume that x itself is strictly less than n
+	  *)
+          let (ctxt,clfix) = dest_prod renv.env typarray.(i) in
+          let oind =
+            let env' = push_rel_context ctxt renv.env in
+              try Some(fst(find_inductive env' clfix))
+              with Not_found -> None in
+            (match oind with
+		 None -> Not_subterm (* happens if fix is polymorphic *)
+               | Some ind ->
+		   let nbfix = Array.length typarray in
+		   let recargs = lookup_subterms renv.env ind in
+		     (* pushing the fixpoints *)
+		   let renv' = push_fix_renv renv recdef in
+		   let renv' =
+                     (* Why Strict here ? To be general, it could also be
+			Large... *)
+                     assign_var_spec renv'
+		       (nbfix-i, lazy (Subterm(Strict,recargs))) in
+		   let decrArg = recindxs.(i) in
+		   let theBody = bodies.(i)   in
+		   let nbOfAbst = decrArg+1 in
+		   let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in
+		     (* pushing the fix parameters *)
+		   let stack' = push_stack_closures renv l stack in
+		   let renv'' = push_ctxt_renv renv' sign in
+		   let renv'' =
+                     if List.length stack' < nbOfAbst then renv''
+                     else
+		       let decrArg = List.nth stack' decrArg in
+                       let arg_spec = stack_element_specif decrArg in
+			 assign_var_spec renv'' (1, arg_spec) in
+		     subterm_specif renv'' [] strippedBody)
+
+      | Lambda (x,a,b) ->
+          assert (l=[]);
+	  let spec,stack' = extract_stack renv a stack in
+	    subterm_specif (push_var renv (x,a,spec)) stack' b
+
+      (* Metas and evars are considered OK *)
+      | (Meta _|Evar _) -> Dead_code
+
+      (* Other terms are not subterms *)
+      | _ -> Not_subterm
+
+and lazy_subterm_specif renv stack t =
+  lazy (subterm_specif renv stack t)
+
+and stack_element_specif = function
+  |SClosure (h_renv,h) -> lazy_subterm_specif h_renv [] h
+  |SArg x -> x
+
+and extract_stack renv a = function
+  | [] -> Lazy.lazy_from_val Not_subterm , []
+  | h::t -> stack_element_specif h, t
+
+
+(* Check size x is a correct size for recursive calls. *)
+let check_is_subterm x =
+  match Lazy.force x with
     Subterm (Strict,_) | Dead_code -> true
   |  _ -> false
 
@@ -605,17 +634,18 @@ let check_is_subterm renv c =
 
 exception FixGuardError of env * guard_error
 
-let error_illegal_rec_call renv fx arg =
+let error_illegal_rec_call renv fx (arg_renv,arg) =
   let (_,le_vars,lt_vars) =
     List.fold_left
       (fun (i,le,lt) sbt ->
-        match sbt with
+        match Lazy.force sbt with
             (Subterm(Strict,_) | Dead_code) -> (i+1, le, i::lt)
           | (Subterm(Large,_)) -> (i+1, i::le, lt)
           | _ -> (i+1, le ,lt))
       (1,[],[]) renv.genv in
   raise (FixGuardError (renv.env,
-                        RecursionOnIllegalTerm(fx,arg,le_vars,lt_vars)))
+                        RecursionOnIllegalTerm(fx,(arg_renv.env, arg),
+					       le_vars,lt_vars)))
 
 let error_partial_apply renv fx =
   raise (FixGuardError (renv.env,NotEnoughArgumentsForFixCall fx))
@@ -627,49 +657,57 @@ let check_one_fix renv recpos def =
   let nfi = Array.length recpos in
 
   (* Checks if [t] only make valid recursive calls *)
-  let rec check_rec_call renv t =
+  let rec check_rec_call renv stack t =
     (* if [t] does not make recursive calls, it is guarded: *)
     if noccur_with_meta renv.rel_min nfi t then ()
     else
-      let (f,l) = decompose_app (whd_betaiotazeta renv.env t) in
+      let (f,l) = decompose_app (whd_betaiotazeta t) in
       match f with
         | Rel p ->
             (* Test if [p] is a fixpoint (recursive call) *)
 	    if renv.rel_min <= p & p < renv.rel_min+nfi then
               begin
-                List.iter (check_rec_call renv) l;
+                List.iter (check_rec_call renv []) l;
                 (* the position of the invoked fixpoint: *)
 	        let glob = renv.rel_min+nfi-1-p in
                 (* the decreasing arg of the rec call: *)
 	        let np = recpos.(glob) in
-                if List.length l <= np then error_partial_apply renv glob
+		let stack' = push_stack_closures renv l stack in
+                if List.length stack' <= np then error_partial_apply renv glob
                 else
                   (* Check the decreasing arg is smaller *)
-                  let z = List.nth l np in
-	          if not (check_is_subterm renv z) then
-                    error_illegal_rec_call renv glob z
+                  let z = List.nth stack' np in
+	          if not (check_is_subterm (stack_element_specif z)) then
+                    begin match z with
+		      |SClosure (z,z') -> error_illegal_rec_call renv glob (z,z') 
+		      |SArg _ -> error_partial_apply renv glob
+		    end
               end
             else
               begin
                 match pi2 (lookup_rel p renv.env) with
                 | None ->
-                    List.iter (check_rec_call renv) l
+                    List.iter (check_rec_call renv []) l
                 | Some c ->
-                    try List.iter (check_rec_call renv) l
-                    with FixGuardError _ -> check_rec_call renv (applist(c,l))
+                    try List.iter (check_rec_call renv []) l
+                    with FixGuardError _ ->
+                      check_rec_call renv stack (applist(lift p c,l))
               end
-
+		
         | Case (ci,p,c_0,lrest) ->
-            List.iter (check_rec_call renv) (c_0::p::l);
+            List.iter (check_rec_call renv []) (c_0::p::l);
             (* compute the recarg information for the arguments of
                each branch *)
-            let c_spec = subterm_specif renv c_0 in
-            let lbr = case_branches_specif renv c_spec ci.ci_ind lrest in
-            Array.iter (fun (renv',br') -> check_rec_call renv' br') lbr
+            let case_spec = branches_specif renv 
+	      (lazy_subterm_specif renv [] c_0) ci in
+	    let stack' = push_stack_closures renv l stack in
+              Array.iteri (fun k br' -> 
+			     let stack_br = push_stack_args case_spec.(k) stack' in
+			     check_rec_call renv stack_br br') lrest
 
         (* Enables to traverse Fixpoint definitions in a more intelligent
            way, ie, the rule :
-           if - g = Fix g/p := [y1:T1]...[yp:Tp]e &
+           if - g = fix g (y1:T1)...(yp:Tp) {struct yp} := e &
               - f is guarded with respect to the set of pattern variables S
                 in a1 ... am        &
               - f is guarded with respect to the set of pattern variables S
@@ -679,81 +717,80 @@ let check_one_fix renv recpos def =
                 S+{yp} in e
            then f is guarded with respect to S in (g a1 ... am).
            Eduardo 7/9/98 *)
-
         | Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
-            List.iter (check_rec_call renv) l;
-            Array.iter (check_rec_call renv) typarray;
+            List.iter (check_rec_call renv []) l;
+            Array.iter (check_rec_call renv []) typarray;
             let decrArg = recindxs.(i) in
             let renv' = push_fix_renv renv recdef in
-            if (List.length l < (decrArg+1)) then
-	      Array.iter (check_rec_call renv') bodies
-            else
+	    let stack' = push_stack_closures renv l stack in
               Array.iteri
                 (fun j body ->
-                  if i=j then
-                    let theDecrArg  = List.nth l decrArg in
-	            let arg_spec = subterm_specif renv theDecrArg in
-	            check_nested_fix_body renv' (decrArg+1) arg_spec body
-                  else check_rec_call renv' body)
+                   if i=j && (List.length stack' > decrArg) then
+		     let recArg = List.nth stack' decrArg in
+	             let arg_sp = stack_element_specif recArg in
+	             check_nested_fix_body renv' (decrArg+1) arg_sp body
+                   else check_rec_call renv' [] body)
                 bodies
 
         | Const kn ->
             if evaluable_constant kn renv.env then
-              try List.iter (check_rec_call renv) l
+              try List.iter (check_rec_call renv []) l
               with (FixGuardError _ ) ->
-	        check_rec_call renv(applist(constant_value renv.env kn, l))
-	    else List.iter (check_rec_call renv) l
-
-        (* The cases below simply check recursively the condition on the
-           subterms *)
-        | Cast (a,_, b) ->
-            List.iter (check_rec_call renv) (a::b::l)
+		let value = (applist(constant_value renv.env kn, l)) in
+	        check_rec_call renv stack value
+	    else List.iter (check_rec_call renv []) l
 
         | Lambda (x,a,b) ->
-            List.iter (check_rec_call renv) (a::l);
-            check_rec_call (push_var_renv renv (x,a)) b
+	    assert (l = []);
+	    check_rec_call renv [] a ;
+	    let spec, stack' = extract_stack renv a stack in
+	    check_rec_call (push_var renv (x,a,spec)) stack' b
 
         | Prod (x,a,b) ->
-            List.iter (check_rec_call renv) (a::l);
-            check_rec_call (push_var_renv renv (x,a)) b
+	    assert (l = [] && stack = []);
+            check_rec_call renv [] a;
+            check_rec_call (push_var_renv renv (x,a)) [] b
 
         | CoFix (i,(_,typarray,bodies as recdef)) ->
-            List.iter (check_rec_call renv) l;
-	    Array.iter (check_rec_call renv) typarray;
+            List.iter (check_rec_call renv []) l;
+	    Array.iter (check_rec_call renv []) typarray;
 	    let renv' = push_fix_renv renv recdef in
-	    Array.iter (check_rec_call renv') bodies
+	    Array.iter (check_rec_call renv' []) bodies
 
-        | (Ind _ | Construct _ | Sort _) ->
-            List.iter (check_rec_call renv) l
+        | (Ind _ | Construct _) ->
+            List.iter (check_rec_call renv []) l
 
         | Var id ->
             begin
               match pi2 (lookup_named id renv.env) with
               | None ->
-                  List.iter (check_rec_call renv) l
+                  List.iter (check_rec_call renv []) l
               | Some c ->
-                  try List.iter (check_rec_call renv) l
-                  with (FixGuardError _) -> check_rec_call renv (applist(c,l))
+                  try List.iter (check_rec_call renv []) l
+                  with (FixGuardError _) -> 
+		    check_rec_call renv stack (applist(c,l))
             end
 
+	| Sort _ -> assert (l = [])
+
         (* l is not checked because it is considered as the meta's context *)
         | (Evar _ | Meta _) -> ()
 
-        | (App _|LetIn _) -> assert false (* beta zeta reduction *)
+        | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *)
 
   and check_nested_fix_body renv decr recArgsDecrArg body =
     if decr = 0 then
-      check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) body
+      check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body
     else
       match body with
 	| Lambda (x,a,b) ->
-	    check_rec_call renv a;
+	    check_rec_call renv [] a;
             let renv' = push_var_renv renv (x,a) in
-	    check_nested_fix_body renv' (decr-1) recArgsDecrArg b
+	      check_nested_fix_body renv' (decr-1) recArgsDecrArg b
 	| _ -> anomaly "Not enough abstractions in fix body"
-
+	    
   in
-  check_rec_call renv def
+  check_rec_call renv [] def
 
 
 let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
diff --git a/checker/inductive.mli b/checker/inductive.mli
index 35e040a66f..2cf7c70df1 100644
--- a/checker/inductive.mli
+++ b/checker/inductive.mli
@@ -75,9 +75,10 @@ type guard_env =
     (* the recarg information of inductive family *)
     recvec  : wf_paths array;
     (* dB of variables denoting subterms *)
-    genv    : subterm_spec list;
+    genv    : subterm_spec Lazy.t list;
   }
 
-val subterm_specif : guard_env -> constr -> subterm_spec
-val case_branches_specif : guard_env -> subterm_spec -> inductive ->
-  constr array -> (guard_env * constr) array
+type stack_element = |SClosure of guard_env*constr |SArg of subterm_spec Lazy.t
+val subterm_specif : guard_env -> stack_element list -> constr -> subterm_spec
+val branches_specif : guard_env -> subterm_spec Lazy.t -> case_info ->
+  subterm_spec Lazy.t list array
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 1bbeb6cf8e..1f963d125a 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -78,11 +78,11 @@ let pure_stack lfts stk =
 (*                   Reduction Functions                                    *)
 (****************************************************************************)
 
-let whd_betaiotazeta env x =
+let whd_betaiotazeta x =
   match x with
     | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _|
        Prod _|Lambda _|Fix _|CoFix _) -> x
-    | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x)
+    | _ -> whd_val (create_clos_infos betaiotazeta empty_env) (inject x)
 
 let whd_betadeltaiota env t =
   match t with
diff --git a/checker/reduction.mli b/checker/reduction.mli
index 049bbad9b2..0ca5f83681 100644
--- a/checker/reduction.mli
+++ b/checker/reduction.mli
@@ -14,7 +14,7 @@ open Environ
 (************************************************************************)
 (*s Reduction functions *)
 
-val whd_betaiotazeta        : env -> constr -> constr
+val whd_betaiotazeta        : constr -> constr
 val whd_betadeltaiota       : env -> constr -> constr
 val whd_betadeltaiota_nolet : env -> constr -> constr
 
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 878e1975e2..6cd47d85d7 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -104,8 +104,8 @@ type compiled_library =
     engagement option
 
 open Validate
-let val_deps = val_list (val_tuple"dep"[|val_dp;no_val|])
-let val_vo = val_tuple "vo" [|val_dp;val_module;val_deps;val_opt val_eng|]
+let val_deps = val_list (val_tuple ~name:"dep"[|val_dp;no_val|])
+let val_vo = val_tuple ~name:"vo" [|val_dp;val_module;val_deps;val_opt val_eng|]
 
 (* This function should append a certificate to the .vo file.
    The digest must be part of the certicate to rule out attackers
diff --git a/checker/term.ml b/checker/term.ml
index 72cb6a67ed..403fd7aa09 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -36,8 +36,8 @@ type case_info =
   }
 let val_ci =
   let val_cstyle = val_enum "case_style" 5 in
-  let val_cprint = val_tuple "case_printing" [|val_int;val_cstyle|] in
-  val_tuple "case_info" [|val_ind;val_int;val_array val_int;val_cprint|]
+  let val_cprint = val_tuple ~name:"case_printing" [|val_int;val_cstyle|] in
+  val_tuple ~name:"case_info" [|val_ind;val_int;val_array val_int;val_cprint|]
 
 (* Sorts. *)
 
@@ -71,13 +71,14 @@ type 'constr pfixpoint =
 type 'constr pcofixpoint =
     int * 'constr prec_declaration
 
-let val_evar f = val_tuple "pexistential" [|val_int;val_array f|]
+let val_evar f = val_tuple ~name:"pexistential" [|val_int;val_array f|]
 let val_prec f =
-  val_tuple "prec_declaration"[|val_array val_name; val_array f; val_array f|]
+  val_tuple ~name:"prec_declaration"
+    [|val_array val_name; val_array f; val_array f|]
 let val_fix f =
-  val_tuple"pfixpoint"
-    [|val_tuple"fix2"[|val_array val_int;val_int|];val_prec f|]
-let val_cofix f = val_tuple"pcofixpoint"[|val_int;val_prec f|]
+  val_tuple ~name:"pfixpoint"
+    [|val_tuple~name:"fix2"[|val_array val_int;val_int|];val_prec f|]
+let val_cofix f = val_tuple ~name:"pcofixpoint"[|val_int;val_prec f|]
 
 type cast_kind = VMcast | DEFAULTcast
 let val_cast = val_enum "cast_kind" 2
@@ -311,9 +312,9 @@ let subst1 lam = substl [lam]
 (***************************************************************************)
 
 let val_ndecl =
-  val_tuple"named_declaration"[|val_id;val_opt val_constr;val_constr|]
+  val_tuple ~name:"named_declaration"[|val_id;val_opt val_constr;val_constr|]
 let val_rdecl =
-  val_tuple"rel_declaration"[|val_name;val_opt val_constr;val_constr|]
+  val_tuple ~name:"rel_declaration"[|val_name;val_opt val_constr;val_constr|]
 let val_nctxt = val_list val_ndecl
 let val_rctxt = val_list val_rdecl
 
@@ -437,7 +438,7 @@ let decompose_prod_n_assum n =
 (***************************)
 
 type arity = rel_context * sorts
-let val_arity = val_tuple"arity"[|val_rctxt;val_constr|]
+let val_arity = val_tuple ~name:"arity"[|val_rctxt;val_constr|]
 
 let mkArity (sign,s) = it_mkProd_or_LetIn (Sort s) sign
 
diff --git a/checker/term.mli b/checker/term.mli
index 66ba96cc5b..46ee12eca4 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -111,8 +111,8 @@ val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
 val eq_constr : constr -> constr -> bool
 
 (* Validation *)
-val val_sortfam : Obj.t -> unit
-val val_sort : Obj.t -> unit
-val val_constr : Obj.t -> unit
-val val_rctxt : Obj.t -> unit
-val val_nctxt : Obj.t -> unit
+val val_sortfam : Validate.func
+val val_sort : Validate.func
+val val_constr : Validate.func
+val val_rctxt : Validate.func
+val val_nctxt : Validate.func
diff --git a/checker/type_errors.ml b/checker/type_errors.ml
index 9a4d06d787..2963b3ba3d 100644
--- a/checker/type_errors.ml
+++ b/checker/type_errors.ml
@@ -20,7 +20,7 @@ type guard_error =
   (* Fixpoints *)
   | NotEnoughAbstractionInFixBody
   | RecursionNotOnInductiveType of constr
-  | RecursionOnIllegalTerm of int * constr * int list * int list
+  | RecursionOnIllegalTerm of int * (env * constr) * int list * int list
   | NotEnoughArgumentsForFixCall of int
   (* CoFixpoints *)
   | CodomainNotInductiveType of constr
diff --git a/checker/type_errors.mli b/checker/type_errors.mli
index 28bce35620..0367135383 100644
--- a/checker/type_errors.mli
+++ b/checker/type_errors.mli
@@ -22,7 +22,7 @@ type guard_error =
   (* Fixpoints *)
   | NotEnoughAbstractionInFixBody
   | RecursionNotOnInductiveType of constr
-  | RecursionOnIllegalTerm of int * constr * int list * int list
+  | RecursionOnIllegalTerm of int * (env * constr) * int list * int list
   | NotEnoughArgumentsForFixCall of int
   (* CoFixpoints *)
   | CodomainNotInductiveType of constr
diff --git a/checker/validate.ml b/checker/validate.ml
index ae4b9212c3..36c668af38 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -36,44 +36,59 @@ let pr_obj o = pr_obj_rec o; Format.print_newline()
 (**************************************************************************)
 (* Obj low-level validators *)
 
-exception ValidObjError of string * Obj.t
-let fail o s = raise (ValidObjError(s,o))
+type error_context = string list
+let mt_ec : error_context = []
+let (/) (ctx:error_context) s : error_context = s::ctx
+let overr (ctx:error_context) f = (fun (_:error_context) -> f ctx) 
+let ext s f (ctx:error_context) = f (ctx/s)
 
-let ep s1 f s2 = f (s1^"/"^s2) 
+
+exception ValidObjError of string * error_context * Obj.t
+let fail ctx o s = raise (ValidObjError(s,ctx,o))
+
+type func = error_context -> Obj.t -> unit
 
 let apply debug f x =
   let o = Obj.repr x in
-  try f o
-  with ValidObjError(msg,obj) ->
+  try f mt_ec o
+  with ValidObjError(msg,ctx,obj) ->
     if debug then begin
       print_endline ("Validation failed: "^msg);
+      print_endline ("Context: "^String.concat"/"(List.rev ctx));
       pr_obj obj
     end;
     failwith "vo structure validation failed"
 
 (* data not validated *)
-let no_val (o:Obj.t) = ()
+let no_val (c:error_context) (o:Obj.t) = ()
 
 (* Check that object o is a block with tag t *)
-let val_tag t o =
+let val_tag t ctx o =
   if Obj.is_block o && Obj.tag o = t then ()
-  else fail o ("expected tag "^string_of_int t)
+  else fail ctx o ("expected tag "^string_of_int t)
 
-let val_block s o =
+let val_block ctx o =
   if Obj.is_block o then
     (if Obj.tag o > Obj.no_scan_tag then
-      fail o (s^": found no scan tag"))
-  else fail o (s^": expected block obj")
+      fail ctx o "block: found no scan tag")
+  else fail ctx o "expected block obj"
 
 (* Check that an object is a tuple (or a record). v is an array of
    validation functions for each field. Its size corresponds to the
    expected size of the object. *)
-let val_tuple s v o =
+let val_tuple ?name v ctx o =
+  let ctx = match name with
+      Some n -> ctx/n
+    | _ -> ctx in
   let n = Array.length v in
-  val_block ("tuple: "^s) o;
-  if Obj.size o = n then Array.iteri (fun i f -> f (Obj.field o i)) v
+  let val_fld i f =
+    f (ctx/("fld="^string_of_int i)) (Obj.field o i) in
+  val_block ctx o;
+  if Obj.size o = n then Array.iteri val_fld v
   else
-    fail o ("tuple:" ^s^" size found:"^string_of_int (Obj.size o))
+    fail ctx o
+      ("tuple size: found "^string_of_int (Obj.size o)^
+	 ", expected "^string_of_int n)
 
 (* Check that the object is either a constant constructor of tag < cc,
    or a constructed variant. each element of vv is an array of
@@ -81,24 +96,26 @@ let val_tuple s v o =
    The size of vv corresponds to the number of non-constant
    constructors, and the size of vv.(i) is the expected arity of the
    i-th non-constant constructor. *)
-let val_sum s cc vv o =
+let val_sum name cc vv ctx o =
+  let ctx = ctx/name in
   if Obj.is_block o then
-    (val_block s o;
+    (val_block (ctx/name) o;
     let n = Array.length vv in
     let i = Obj.tag o in
-    if i < n then val_tuple (s^"(tag "^string_of_int i^")") vv.(i) o
-    else fail o ("bad tag in (sum type) "^s^": found "^string_of_int i))
+    let ctx' = if n=1 then ctx else ctx/("tag="^string_of_int i) in
+    if i < n then val_tuple vv.(i) ctx' o
+    else fail ctx' o ("sum: unexpected tag"))
   else if Obj.is_int o then
     let (n:int) = Obj.magic o in
     (if n<0 || n>=cc then
-      fail o (s^": bad constant constructor "^string_of_int n))
-  else fail o ("not a sum ("^s^")")
+      fail ctx o ("bad constant constructor "^string_of_int n))
+  else fail ctx o "not a sum"
 
 let val_enum s n = val_sum s n [||]
 
 (* Recursive types: avoid looping by eta-expansion *)
-let rec val_rec_sum s cc f o =
-  val_sum s cc (f (val_rec_sum s cc f)) o
+let rec val_rec_sum name cc f ctx o =
+  val_sum name cc (f (overr (ctx/name) (val_rec_sum name cc f))) ctx o
 
 let rec val_rectype f o =
   f (val_rectype f) o
@@ -107,44 +124,54 @@ let rec val_rectype f o =
 (* Builtin types *)
 
 (* Check the o is an array of values satisfying f. *)
-let val_array ?(name="array") f o =
-  val_block name o;
+let val_array ?(pos=false) f ctx o =
+  let upd_ctx =
+    if pos then (fun i -> ctx/string_of_int i) else (fun _ -> ctx) in
+  val_block (ctx/"array") o;
   for i = 0 to Obj.size o - 1 do
-    (f (Obj.field o i):unit)
+    (f (upd_ctx i) (Obj.field o i):unit)
   done
 
 (* Integer validator *)
-let val_int o =
-  if not (Obj.is_int o) then fail o "expected an int"
+let val_int ctx o =
+  if not (Obj.is_int o) then fail ctx o "expected an int"
 
 (* String validator *)
-let val_str o =
-  try val_tag Obj.string_tag o
-  with Failure _ -> fail o "expected a string"
+let val_str ctx o =
+  try val_tag Obj.string_tag ctx o
+  with Failure _ -> fail ctx o "expected a string"
 
 (* Booleans *)
 let val_bool = val_enum "bool" 2
 
 (* Option type *)
-let val_opt ?(name="option") f = val_sum name 1 [|[|f|]|]
+let val_opt ?(name="option") f =
+  val_sum name 1 [|[|f|]|]
 
 (* Lists *)
-let val_list ?(name="list") f =
-  val_rec_sum name 1 (fun vlist -> [|[|f;vlist|]|])
+let val_list ?(name="list") f ctx =
+  val_rec_sum name 1 (fun vlist -> [|[|ext "elem" f;vlist|]|])
+    ctx
 
 (* Reference *)
-let val_ref ?(name="ref") f = val_tuple name [|f|]
+let val_ref ?(name="ref") f ctx =
+  val_tuple [|f|] (ctx/name)
 
 (**************************************************************************)
 (* Standard library types *)
 
 (* Sets *)
 let val_set ?(name="Set.t") f =
-  val_rec_sum name 1 (fun vset -> [|[|vset;f;vset;val_int|]|])
+  val_rec_sum name 1
+    (fun vset -> [|[|vset;ext "elem" f;
+		     vset;ext "bal" val_int|]|])
 
 (* Maps *)
 let rec val_map ?(name="Map.t") fk fv =
-  val_rec_sum name 1 (fun vmap -> [|[|vmap;fk;fv;vmap;val_int|]|])
+  val_rec_sum name 1
+    (fun vmap ->
+       [|[|vmap; ext "key" fk; ext "value" fv;
+	   vmap; ext "bal" val_int|]|])
 
 (**************************************************************************)
 (* Coq types *)
@@ -156,19 +183,19 @@ let val_dp = val_list ~name:"dirpath" val_id
 
 let val_name = val_sum "name" 1 [|[|val_id|]|]
 
-let val_uid = val_tuple "uniq_ident" [|val_int;val_str;val_dp|]
+let val_uid = val_tuple ~name:"uniq_ident" [|val_int;val_str;val_dp|]
 
 let val_mp =
   val_rec_sum "module_path" 0
     (fun vmp -> [|[|val_dp|];[|val_uid|];[|vmp;val_id|]|])
 
-let val_kn = val_tuple "kernel_name" [|val_mp;val_dp;val_id|]
+let val_kn = val_tuple ~name:"kernel_name" [|val_mp;val_dp;val_id|]
 
 let val_con =
-  val_tuple "constant/mutind" [|val_kn;val_kn|]
+  val_tuple ~name:"constant/mutind" [|val_kn;val_kn|]
 
-let val_ind = val_tuple "inductive"[|val_con;val_int|]
-let val_cstr = val_tuple "constructor"[|val_ind;val_int|]
+let val_ind = val_tuple ~name:"inductive"[|val_con;val_int|]
+let val_cstr = val_tuple ~name:"constructor"[|val_ind;val_int|]
 
 (* univ *)
 let val_level = val_sum "level" 1 [|[|val_dp;val_int|]|]
@@ -177,5 +204,5 @@ let val_univ = val_sum "univ" 0
 
 let val_cstrs =
   val_set ~name:"Univ.constraints"
-   (val_tuple "univ_constraint"
+   (val_tuple ~name:"univ_constraint"
      [|val_level;val_enum "order_request" 3;val_level|])