Changed the way to detect if an "as" patterns is expanded or not. The

main criterion is to look at whether the alias to the term to match is
dependent in the return predicate or not.  Since the exact return
predicate is often found late, the detection is done after the
subproblem is fully compiled, when a maximum amount of (local)
information on typing is known.

Eventually, we should go to a model where all possible partial
expansions of an alias are usable at typing time. Indeed the current
heuristic (like the previous one) is not fully safe since it might
decide not to expand an alias in a branch whose type does not depend
of the alias but the typing of the branch internally needs the
expansion (as e.g. in "fun (H:forall n, n=0->Prop) n => match n with 0
as x => H x eq_refl | _ => True end").

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

1 files changed, 70 insertions, 0 deletions

diff --git a/test-suite/success/CaseAlias.v b/test-suite/success/CaseAlias.v
index 32d85779f..a92490862 100644
--- a/test-suite/success/CaseAlias.v
+++ b/test-suite/success/CaseAlias.v
@@ -1,3 +1,4 @@
+(*********************************************)
 (* This has been a bug reported by Y. Bertot *)
 Inductive expr : Set :=
   | b : expr -> expr -> expr
@@ -19,3 +20,72 @@ Fixpoint f2 (t : expr) : expr :=
   | x => b x a
   end.
 
+(*********************************************)
+(* Test expansion of aliases                 *)
+(* Originally taken from NMake_gen.v         *)
+
+ Local Notation SizePlus n := (S (S (S (S (S (S n)))))).
+ Local Notation Size := (SizePlus O).
+
+ Parameter zn2z : Type -> Type.
+ Parameter w0 : Type.
+ Fixpoint word (w : Type) (n : nat) {struct n} : Type :=
+  match n with
+  | 0 => w
+  | S n0 => zn2z (word w n0)
+  end.
+
+ Definition w1 := zn2z w0.
+ Definition w2 := zn2z w1.
+ Definition w3 := zn2z w2.
+ Definition w4 := zn2z w3.
+ Definition w5 := zn2z w4.
+ Definition w6 := zn2z w5.
+
+ Definition dom_t n := match n with
+  | 0 => w0
+  | 1 => w1
+  | 2 => w2
+  | 3 => w3
+  | 4 => w4
+  | 5 => w5
+  | 6 => w6
+  | SizePlus n => word w6 n
+ end.
+Parameter plus_t : forall n m : nat, word (dom_t n) m -> dom_t (m + n).
+
+(* This used to fail because of a bug in expansion of SizePlus wrongly
+   reusing n as an alias for the subpattern *)
+Definition plus_t1 n : forall m, word (dom_t n) m -> dom_t (m+n) :=
+   match n return (forall m, word (dom_t n) m -> dom_t (m+n)) with
+     | SizePlus (S n') as n => plus_t n
+     | _ as n =>
+         fun m => match m return (word (dom_t n) m -> dom_t (m+n)) with
+                    | SizePlus (S (S m')) as m => plus_t n m
+                    | _ => fun x => x
+                  end
+   end.
+
+(* Test (useless) intermediate alias *)
+Definition plus_t2 n : forall m, word (dom_t n) m -> dom_t (m+n) :=
+   match n return (forall m, word (dom_t n) m -> dom_t (m+n)) with
+     | S (S (S (S (S (S (S n'))))) as n) as n'' => plus_t n''
+     | _ as n =>
+         fun m => match m return (word (dom_t n) m -> dom_t (m+n)) with
+                    | SizePlus (S (S m')) as m => plus_t n m
+                    | _ => fun x => x
+                  end
+   end.
+
+(*****************************************************************************)
+(* Check that alias expansion behaves consistently from versions to versions *)
+
+Definition g m :=
+  match pred m with
+  | 0 => 0
+  | n => n (* For compatibility, right-hand side should be (S n), not (pred m) *)
+  end.
+
+Goal forall m, g m = match pred m with 0 => 0 | S n => S n end.
+intro; reflexivity.
+Abort.