From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 12:07:52 +0200 Subject: Imported Upstream version 8.4~gamma0+really8.4beta2 --- test-suite/success/coercions.v | 42 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) (limited to 'test-suite/success/coercions.v') diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v index 001beae7..4292ecb6 100644 --- a/test-suite/success/coercions.v +++ b/test-suite/success/coercions.v @@ -89,3 +89,45 @@ Module A. End A. Import A. Fail Check S true. + +(* Tests after the inheritance condition constraint is relaxed *) + +Inductive list (A : Type) : Type := + nil : list A | cons : A -> list A -> list A. +Inductive vect (A : Type) : nat -> Type := + vnil : vect A 0 | vcons : forall n, A -> vect A n -> vect A (1+n). +Fixpoint size A (l : list A) : nat := match l with nil => 0 | cons _ tl => 1+size _ tl end. + +Section test_non_unif_but_complete. +Fixpoint l2v A (l : list A) : vect A (size A l) := + match l as l return vect A (size A l) with + | nil => vnil A + | cons x xs => vcons A (size A xs) x (l2v A xs) + end. + +Local Coercion l2v : list >-> vect. +Check (fun l : list nat => (l : vect _ _)). + +End test_non_unif_but_complete. + +Section what_we_could_do. +Variables T1 T2 : Type. +Variable c12 : T1 -> T2. + +Class coercion (A B : Type) : Type := cast : A -> B. +Instance atom : coercion T1 T2 := c12. +Instance pair A B C D (c1 : coercion A B) (c2 : coercion C D) : coercion (A * C) (B * D) := + fun x => (c1 (fst x), c2 (snd x)). + +Fixpoint l2v2 {A B} {c : coercion A B} (l : list A) : (vect B (size A l)) := + match l as l return vect B (size A l) with + | nil => vnil B + | cons x xs => vcons _ _ (c x) (l2v2 xs) end. + +Local Coercion l2v2 : list >-> vect. + +(* This shows that there is still something to do to take full profit + of coercions *) +Fail Check (fun l : list (T1 * T1) => (l : vect _ _)). +Check (fun l : list (T1 * T1) => (l2v2 l : vect _ _)). +Section what_we_could_do. \ No newline at end of file -- cgit v1.2.3