aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2014-04-05 16:10:47 -0400
committerGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2014-04-10 14:42:55 +0200
commitd464e101f4a26d26cc60d9edaa430cb131f85065 (patch)
treea072c358ad2627c24acf2d087d784382d8155f00
parentf2b60f5911d7e881ff369663a7ed1f1bddfddb1d (diff)
Test case for bug 3262
Closed in f65fa9de8a4c9c12d933188a755b51508bd51921 I used [Timeout 2 Fail] to test the difference between immediate failure and stack overflow. Hopefully this is robust enough.
-rw-r--r--test-suite/bugs/closed/3262.v78
1 files changed, 78 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3262.v b/test-suite/bugs/closed/3262.v
new file mode 100644
index 000000000..70bfde299
--- /dev/null
+++ b/test-suite/bugs/closed/3262.v
@@ -0,0 +1,78 @@
+(* Not having a [return] clause causes the [refine] at the bottom to stack overflow before f65fa9de8a4c9c12d933188a755b51508bd51921 *)
+
+Require Import Coq.Lists.List.
+Require Import Relations RelationClasses.
+
+Set Implicit Arguments.
+Set Strict Implicit.
+Set Asymmetric Patterns.
+
+Section hlist.
+ Context {iT : Type}.
+ Variable F : iT -> Type.
+
+ Inductive hlist : list iT -> Type :=
+ | Hnil : hlist nil
+ | Hcons : forall l ls, F l -> hlist ls -> hlist (l :: ls).
+
+ Definition hlist_hd {a b} (hl : hlist (a :: b)) : F a :=
+ match hl in hlist x return match x with
+ | nil => unit
+ | l :: _ => F l
+ end with
+ | Hnil => tt
+ | Hcons _ _ x _ => x
+ end.
+
+ Definition hlist_tl {a b} (hl : hlist (a :: b)) : hlist b :=
+ match hl in hlist x return match x with
+ | nil => unit
+ | _ :: ls => hlist ls
+ end with
+ | Hnil => tt
+ | Hcons _ _ _ x => x
+ end.
+
+ Lemma hlist_eta : forall ls (h : hlist ls),
+ h = match ls as ls return hlist ls -> hlist ls with
+ | nil => fun _ => Hnil
+ | a :: b => fun h => Hcons (hlist_hd h) (hlist_tl h)
+ end h.
+ Proof.
+ intros. destruct h; auto.
+ Qed.
+
+ Variable eqv : forall x, relation (F x).
+
+ Inductive equiv_hlist : forall ls, hlist ls -> hlist ls -> Prop :=
+ | hlist_eqv_nil : equiv_hlist Hnil Hnil
+ | hlist_eqv_cons : forall l ls x y h1 h2, eqv x y -> equiv_hlist h1 h2 ->
+ @equiv_hlist (l :: ls) (Hcons x h1) (Hcons y h2).
+
+ Global Instance Reflexive_equiv_hlist (R : forall t, Reflexive (@eqv t)) ls
+ : Reflexive (@equiv_hlist ls).
+ Proof.
+ red. induction x; constructor; auto. reflexivity.
+ Qed.
+
+ Global Instance Transitive_equiv_hlist (R : forall t, Transitive (@eqv t)) ls
+ : Transitive (@equiv_hlist ls).
+ Proof.
+ red. induction 1.
+ { intro; assumption. }
+ { rewrite (hlist_eta z).
+ Timeout 2 Fail refine
+ (fun H =>
+ match H in @equiv_hlist ls X Y
+ return
+ (* Uncommenting the following gives an immediate error in 8.4pl3; commented out results in a stack overflow *)
+ match ls (*as ls return hlist ls -> hlist ls -> Type*) with
+ | nil => fun _ _ : hlist nil => True
+ | l :: ls => fun (X Y : hlist (l :: ls)) =>
+ equiv_hlist (Hcons x h1) Y
+ end X Y
+ with
+ | hlist_eqv_nil => I
+ | hlist_eqv_cons l ls x y h1 h2 pf pf' =>
+ _
+ end).