diff options
Diffstat (limited to 'test-suite/success/CasesDep.v')
-rw-r--r-- | test-suite/success/CasesDep.v | 76 |
1 files changed, 70 insertions, 6 deletions
diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v index 29721843..bfead53c 100644 --- a/test-suite/success/CasesDep.v +++ b/test-suite/success/CasesDep.v @@ -26,6 +26,40 @@ Fixpoint foldrn (n : nat) (bs : listn B n) {struct bs} : C := end. End Folding. +(** Testing post-processing of nested dependencies *) + +Check fun x:{x|x=0}*nat+nat => match x with + | inl ((exist 0 eq_refl),0) => None + | _ => Some 0 + end. + +Check fun x:{_:{x|x=0}|True}+nat => match x with + | inl (exist (exist 0 eq_refl) I) => None + | _ => Some 0 + end. + +Check fun x:{_:{x|x=0}|True}+nat => match x with + | inl (exist (exist 0 eq_refl) I) => None + | _ => Some 0 + end. + +Check fun x:{_:{x|x=0}|True}+nat => match x return option nat with + | inl (exist (exist 0 eq_refl) I) => None + | _ => Some 0 + end. + + (* the next two examples were failing from r14703 (Nov 22 2011) to r14732 *) + (* due to a bug in dependencies postprocessing (revealed by CoLoR) *) + +Check fun x:{x:nat*nat|fst x = 0 & True} => match x return option nat with + | exist2 (x,y) eq_refl I => None + end. + +Check fun x:{_:{x:nat*nat|fst x = 0 & True}|True}+nat => match x return option nat with + | inl (exist (exist2 (x,y) eq_refl I) I) => None + | _ => Some 0 + end. + (* -------------------------------------------------------------------- *) (* Example to test patterns matching on dependent families *) (* This exemple extracted from the developement done by Nacira Chabane *) @@ -188,7 +222,7 @@ Definition Dposint := Build_DSetoid Set_of_posint Eq_posint_deci. de l'arite de chaque operateur *) -Section Sig. +Module Sig. Record Signature : Type := {Sigma : DSetoid; Arity : Map (Set_of Sigma) (Set_of Dposint)}. @@ -243,7 +277,7 @@ Type | _, _ => False end. - +Module Type Version1. Definition equalT (t1 t2 : TERM) : Prop := match t1, t2 with @@ -260,12 +294,15 @@ Definition EqListT (n1 : posint) (l1 : LTERM n1) (n2 : posint) | _, _ => False end. +End Version1. + -Reset equalT. (* ------------------------------------------------------------------*) (* Initial exemple (without patterns) *) (*-------------------------------------------------------------------*) +Module Version2. + Fixpoint equalT (t1 : TERM) : TERM -> Prop := match t1 return (TERM -> Prop) with | var v1 => @@ -313,11 +350,13 @@ Fixpoint equalT (t1 : TERM) : TERM -> Prop := end end. +End Version2. (* ---------------------------------------------------------------- *) (* Version with simple patterns *) (* ---------------------------------------------------------------- *) -Reset equalT. + +Module Version3. Fixpoint equalT (t1 : TERM) : TERM -> Prop := match t1 with @@ -354,8 +393,9 @@ Fixpoint equalT (t1 : TERM) : TERM -> Prop := end end. +End Version3. -Reset equalT. +Module Version4. Fixpoint equalT (t1 : TERM) : TERM -> Prop := match t1 with @@ -389,10 +429,13 @@ Fixpoint equalT (t1 : TERM) : TERM -> Prop := end end. +End Version4. + (* ---------------------------------------------------------------- *) (* Version with multiple patterns *) (* ---------------------------------------------------------------- *) -Reset equalT. + +Module Version5. Fixpoint equalT (t1 t2 : TERM) {struct t1} : Prop := match t1, t2 with @@ -411,6 +454,7 @@ Fixpoint equalT (t1 t2 : TERM) {struct t1} : Prop := | _, _ => False end. +End Version5. (* ------------------------------------------------------------------ *) @@ -506,3 +550,23 @@ Definition test (s:step E E) := | Step nil _ (cons E nil) _ Plus l l' => true | _ => false end. + +(* Testing regression of bug 2454 ("get" used not be type-checkable when + defined with its type constraint) *) + +Inductive K : nat -> Type := KC : forall (p q:nat), K p. + +Definition get : K O -> nat := fun x => match x with KC p q => q end. + +(* Checking correct order of substitution of realargs *) +(* (was broken from revision 14664 to 14669) *) +(* Example extracted from contrib CoLoR *) + +Inductive EQ : nat -> nat -> Prop := R x y : EQ x y. + +Check fun e t (d1 d2:EQ e t) => + match d1 in EQ e1 t1, d2 in EQ e2 t2 return + (e1,t1) = (e2,t2) -> (e1,t1) = (e,t) -> 0=0 + with + | R _ _, R _ _ => fun _ _ => eq_refl + end. |