From e7c9f5f130f5187e5d9b43c8f0ed15deb49e4b2c Mon Sep 17 00:00:00 2001
From: pboutill
Date: Tue, 18 May 2010 15:57:18 +0000
Subject: Applicative commutative cuts in Fixpoint guard condition

In "(match ... with |... -> fun x -> t end) u", "x" has now the subterm
property of "u" in the analysis of "t".

Commutative cuts aren't compatible with typing so we need to ensure that
term of "x"'s type and term of "u"'s have the same subterm_spec.
Consequently,declaration.MRec argument has changed to the inductive name
instead of only the number of the inductive in the mutual_inductive
family.

In subterm_specif and check_rec_call, arguments are stored in a stack.
At each lambda, one element is popped to add in renv a smarter
subterm_spec for the variable. subterm_spec of constructor's argument
was added this way, the job is now done more often.

Some eta contracted match branches are now accepted but enforcing
eta-expansion of branches might be anyway a recommended invariant.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13012 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/indrec.ml       | 4 ++--
 pretyping/inductiveops.ml | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 1daae0236a..a6f5a729a7 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -153,7 +153,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
 	      | [] -> None,[]
               | ra::rest ->
                   (match dest_recarg ra with
-	            | Mrec j when is_rec -> (depPvect.(j),rest)
+	            | Mrec (_,j) when is_rec -> (depPvect.(j),rest)
 	            | Imbr _  ->
 		        Flags.if_verbose warning "Ignoring recursive call";
 		        (None,rest)
@@ -223,7 +223,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
 	  match dest_recarg recarg with
             | Norec   -> None
             | Imbr _  -> None
-            | Mrec i  -> fvect.(i)
+            | Mrec (_,i)  -> fvect.(i)
 	in
         (match optionpos with
            | None ->
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 07447c5404..1a5882f4fb 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -76,7 +76,7 @@ let mis_is_recursive_subset listind rarg =
     List.exists
       (fun ra ->
         match dest_recarg ra with
-	  | Mrec i -> List.mem i listind
+	  | Mrec (_,i) -> List.mem i listind
           | _ -> false) rvec
   in
   array_exists one_is_rec (dest_subterms rarg)
-- 
cgit v1.2.3