From 154de140ac9bce62c964e30d1bc30ed6a942b344 Mon Sep 17 00:00:00 2001
From: pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 11 May 2012 20:24:07 +0000
Subject: Vectors takes advantage of pattern matching compiler fixup

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15308 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Vectors/Fin.v       | 12 +++---------
 theories/Vectors/VectorDef.v | 37 ++++++++++++++++---------------------
 2 files changed, 19 insertions(+), 30 deletions(-)

(limited to 'theories/Vectors')

diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v
index b5736f22d..3c46ebb9a 100644
--- a/theories/Vectors/Fin.v
+++ b/theories/Vectors/Fin.v
@@ -23,10 +23,7 @@ Inductive t : nat -> Set :=
 
 Section SCHEMES.
 Definition case0 P (p: t 0): P p :=
-  match p as p' in t n return
-    match n as n' return t n' -> Type
-  with |0 => fun f0 => P f0 |S _ => fun _ => @ID end p'
-  with |F1 _ => @id |FS _ _ => @id end.
+  match p with | F1 _ | FS _ _ => fun devil => False_rect (@ID) devil (* subterm !!! *) end.
 
 Definition caseS (P: forall {n}, t (S n) -> Type)
   (P1: forall n, @P n F1) (PS : forall {n} (p: t n), P (FS p))
@@ -54,11 +51,8 @@ Definition rect2 (P: forall {n} (a b: t n), Type)
     forall {n} (a b: t n), P a b :=
 fix rect2_fix {n} (a: t n): forall (b: t n), P a b :=
 match a with
-  |F1 m => fun (b: t (S m)) => match b as b' in t n'
-                   return match n',b' with
-                            |0,_ => @ID
-                            |S n0,b0 => P F1 b0
-                          end with
+  |F1 m => fun (b: t (S m)) => match b as b' in t (S n')
+                   return P F1 b' with
                      |F1 m' => H0 m'
                      |FS m' b' => H1 b'
                    end
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 30c0d4c0e..23427eb86 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -40,19 +40,13 @@ Definition rectS {A} (P:forall {n}, t A (S n) -> Type)
  (rect: forall a {n} (v: t A (S n)), P v -> P (a :: v)) :=
  fix rectS_fix {n} (v: t A (S n)) : P v :=
  match v with
- |nil => fun devil => False_rect (@ID) devil
  |cons a 0 v =>
-   match v as vnn in t _ nn
-       return
-         match nn,vnn with
-         |0,vm =>  P (a :: vm)
-         |S _,_ => _
-         end
-     with
+   match v with
      |nil => bas a
-     |_ :: _ => fun devil => False_rect (@ID) devil
-     end
+     |_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
+   end
  |cons a (S nn') v => rect a v (rectS_fix v)
+ |_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
  end.
 
 (** An induction scheme for 2 vectors of same length *)
@@ -66,13 +60,13 @@ match v1 as v1' in t _ n1
   |[] => fun v2 =>
      match v2 with
        |[] => bas
-       |_ :: _ => fun devil => False_rect (@ID) devil
+       |_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
      end
   |h1 :: t1 => fun v2 =>
     match v2 with
-      |[] => fun devil => False_rect (@ID) devil
       |h2 :: t2 => fun t1' =>
         rect (rect2_fix t1' t2) h1 h2
+      |_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
     end t1
 end.
 
@@ -80,14 +74,15 @@ end.
 Definition case0 {A} (P:t A 0 -> Type) (H:P (nil A)) v:P v :=
 match v with
   |[] => H
+  |_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
 end.
 
 (** A vector of length [S _] is [cons] *)
 Definition caseS {A} (P : forall {n}, t A (S n) -> Type)
   (H : forall h {n} t, @P n (h :: t)) {n} (v: t A (S n)) : P v :=
-match v as v' in t _ m return match m, v' with |0, _ => False -> True |S _, v0 => P v' end with
-  |[] => fun devil => False_rect _ devil (* subterm !!! *)
+match v with
   |h :: t => H h t
+  |_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
 end.
 End SCHEMES.
 
@@ -252,14 +247,14 @@ Eval cbv delta beta in rect2 (fun _ _ _ => C) c
 Definition fold_left2 {A B C: Type} (f : A -> B -> C -> A) :=
 fix fold_left2_fix (a : A) {n} (v : t B n) : t C n -> A :=
 match v in t _ n0 return t C n0 -> A with
-  |[] => fun w => match w in t _ n1
-    return match n1 with |0 => A |S _ => @ID end with
+  |[] => fun w => match w with
     |[] => a
-    |_ :: _ => @id end
-  |cons vh vn vt => fun w => match w in t _ n1
-    return match n1 with |0 => @ID |S n => t B n -> A end with
-    |[] => @id
-    |wh :: wt => fun vt' => fold_left2_fix (f a vh wh) vt' wt end vt
+    |_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
+  end
+  |cons vh vn vt => fun w => match w with
+    |wh :: wt => fun vt' => fold_left2_fix (f a vh wh) vt' wt
+    |_ => fun devil => False_rect (@ID) devil (* subterm !!! *)
+  end vt
 end.
 
 End ITERATORS.
-- 
cgit v1.2.3