Tentative fix of the guardedness checker by Christine and me. All stdlib and test-suite pass.

5 files changed, 127 insertions, 56 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 3c7103ac5..fca72e3ae 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -532,6 +532,12 @@ let branches_specif renv c_spec ci =
 	 List.init nca (fun j -> lazy (Lazy.force lvra).(j)))
       car 
 
+let check_inductive_codomain env p =
+  let absctx, ar = dest_lam_assum env p in
+  let arctx, s = dest_prod_assum env ar in
+  let i,l' = decompose_app (whd_betadeltaiota env s) in
+    isInd i
+
 (* [subterm_specif renv t] computes the recursive structure of [t] and
    compare its size with the size of the initial recursive argument of
    the fixpoint we are checking. [renv] collects such information
@@ -542,67 +548,71 @@ 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 kind_of_term f with
-      | Rel k -> subterm_var k renv
-
-      | 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' =
+    | Rel k -> subterm_var k renv
+
+    | Case (ci,p,c,lbr) ->
+    let stack' = push_stack_closures renv l stack in
+      if not (check_inductive_codomain renv.env p) then Not_subterm
+      else
+        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
+      *)
+    if not (check_inductive_codomain renv.env typarray.(i)) then Not_subterm
+    else 
+      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) ->
-          let () = assert (List.is_empty l) in
-	  let spec,stack' = extract_stack renv a stack in
-	    subterm_specif (push_var renv (x,a,spec)) stack' b
+          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) ->
+      let () = assert (List.is_empty l) in
+      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
+    | (Meta _|Evar _) -> Dead_code
 
       (* Other terms are not subterms *)
-      | _ -> Not_subterm
+    | _ -> Not_subterm
 
 and lazy_subterm_specif renv stack t =
   lazy (subterm_specif renv stack t)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 40b8bd4cc..db858e0a0 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -564,6 +564,21 @@ let dest_prod_assum env =
   in
   prodec_rec env empty_rel_context
 
+let dest_lam_assum env =
+  let rec lamec_rec env l ty =
+    let rty = whd_betadeltaiota_nolet env ty in
+    match kind_of_term rty with
+    | Lambda (x,t,c)  ->
+        let d = (x,None,t) in
+	lamec_rec (push_rel d env) (add_rel_decl d l) c
+    | LetIn (x,b,t,c) ->
+        let d = (x,Some b,t) in
+	lamec_rec (push_rel d env) (add_rel_decl d l) c
+    | Cast (c,_,_)    -> lamec_rec env l c
+    | _               -> l,rty
+  in
+  lamec_rec env empty_rel_context
+
 exception NotArity
 
 let dest_arity env c =
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 3f958dc9d..6e4634194 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -79,6 +79,7 @@ val hnf_prod_applist : env -> types -> constr list -> types
 
 val dest_prod       : env -> types -> rel_context * types
 val dest_prod_assum : env -> types -> rel_context * types
+val dest_lam_assum  : env -> types -> rel_context * types
 
 exception NotArity
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index b2b6df392..0ad03d417 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -58,7 +58,7 @@ let handle_side_effects env body side_eff =
       Name (id_of_string name) in
     let rec sub c i x = match kind_of_term x with
       | Const c' when eq_constant c c' -> mkRel i
-      | _ -> map_constr_with_binders ((+) 1) (sub c) i x in
+      | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub c i x) i x in
     let fix_body (c,cb) t =
       match cb.const_body with
       | Undef _ -> assert false
diff --git a/test-suite/failure/subterm.v b/test-suite/failure/subterm.v
new file mode 100644
index 000000000..3798bc48f
--- /dev/null
+++ b/test-suite/failure/subterm.v
@@ -0,0 +1,45 @@
+Module Foo. 
+  Inductive True2:Prop:= I2: (False->True2)->True2.
+
+  Axiom Heq: (False->True2)=True2.
+  
+  Fail Fixpoint con (x:True2) :False :=
+    match x with
+        I2 f => con (match Heq with @eq_refl _ _ => f end)
+    end.
+End Foo.
+
+Require Import ClassicalFacts.
+
+Inductive True1 : Prop := I1 : True1
+with True2 : Prop := I2 : True1 -> True2.
+
+Section func_unit_discr.
+
+Hypothesis Heq : True1 = True2.
+
+Fail Fixpoint contradiction (u : True2) : False :=
+contradiction (
+    match u with
+      | I2 Tr =>
+         match Heq in (_ = T) return T with
+         | eq_refl => Tr
+         end
+    end).
+
+End func_unit_discr.
+
+Require Import Vectors.VectorDef.
+
+About caseS.
+About tl.
+Open Scope vector_scope.
+Local Notation "[]" := (@nil _).
+Local Notation "h :: t" := (@cons _ h _ t) (at level 60, right associativity).
+Definition is_nil {A n} (v : t A n) : bool := match v with [] => true | _ => false end.
+
+Fixpoint id {A n} (v : t A n) : t A n :=
+  match v in t _ n' return t A n' with
+    | (h :: t) as v' => h :: id (tl v')
+    |_ => []
+  end.