Vérification de la prise en compte des termes de type non inductif

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

1 files changed, 45 insertions, 0 deletions

diff --git a/test-suite/success/Case15.v b/test-suite/success/Case15.v
new file mode 100644
index 000000000..19579d555
--- /dev/null
+++ b/test-suite/success/Case15.v
@@ -0,0 +1,45 @@
+(* Check compilation of multiple pattern-matching on terms non
+   apparently of inductive type *)
+
+(* Check that the non dependency in y is OK both in V7 and V8 *)
+Check ([x;y:Prop;z]<[x][z]x=x \/ z=z>Cases x y z of
+           | O y z' => (or_introl ? (z'=z') (refl_equal ? O))
+           | _ y O => (or_intror ?? (refl_equal ? O))
+           | x y _ => (or_introl ?? (refl_equal ? x))
+           end).
+
+(* Check lazyness of compilation ... future work
+Inductive I : Set := c : (b:bool)(if b then bool else nat)->I.
+
+Check [x]
+  Cases x of
+    (c (true as y) (true as x)) => (if x then y else true)
+  | (c false O) => true | _ => false
+  end.
+
+Check [x]
+  Cases x of 
+    (c true true) => true
+  | (c false O) => true
+  | _ => false
+  end.
+
+(* Devrait produire ceci mais trouver le type intermediaire est coton ! *)
+Check
+  [x:I]
+   Cases x of
+     (c b y) => 
+      (<[b:bool](if b then bool else nat)->bool>if b
+       then [y](if y then true else false)
+       else [y]Cases y of
+              O => true
+            | (S _) => false
+            end y)
+   end.
+
+(* Suggested by Pierre Letouzey (PR#207) *)
+Definition test := [B:Boite]<nat>Cases B of 
+  (boite true n) => n 
+| (boite false (n,m)) => (plus n m)
+end.
+*)