diff options
Diffstat (limited to 'test-suite/success/coercions.v')
-rw-r--r-- | test-suite/success/coercions.v | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v index 908b5f77..4292ecb6 100644 --- a/test-suite/success/coercions.v +++ b/test-suite/success/coercions.v @@ -81,3 +81,53 @@ Coercion irrelevent := (fun _ => I) : True -> car (Build_Setoid True). Definition ClaimB := forall (X Y:Setoid) (f: extSetoid X Y) (x:X), f x= f x. +(* Check that coercions are made visible only when modules are imported *) + +Module A. + Module B. Coercion b2n (b:bool) := if b then 0 else 1. End B. + Fail Check S true. +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 |