Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

coercions.mlw 1.74 KB
 Jean-Christophe Filliâtre committed Feb 09, 2017 1 `````` `````` 2 ``````module Simple `````` Jean-Christophe Filliâtre committed Feb 09, 2017 3 `````` `````` 4 `````` type t `````` Jean-Christophe Filliâtre committed Feb 09, 2017 5 `````` `````` 6 7 `````` function f t : int meta coercion function f `````` Jean-Christophe Filliâtre committed Feb 09, 2017 8 `````` `````` 9 `````` goal G: forall x: t. x = 42 `````` Jean-Christophe Filliâtre committed Feb 09, 2017 10 `````` `````` 11 ``````end `````` Jean-Christophe Filliâtre committed Feb 09, 2017 12 `````` `````` 13 ``````module SameOne `````` Jean-Christophe Filliâtre committed Feb 13, 2017 14 `````` `````` 15 `````` use import Simple `````` Jean-Christophe Filliâtre committed Feb 09, 2017 16 `````` `````` 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 ``````end module Same use import Simple use import SameOne goal G: forall x: t. x = 42 end module SimplePolymorphic type t 'a function f (t 'a) : int meta coercion function f `````` Jean-Christophe Filliâtre committed Feb 13, 2017 35 `````` goal G: forall x: t (bool,bool). x = 42 `````` 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 `````` end module Transitivity type a type b type c function b_to_c b : c meta coercion function b_to_c function a_to_b a : b meta coercion function a_to_b predicate is_c c goal G2: forall x: a. is_c x end module SameTransitivity `````` Jean-Christophe Filliâtre committed Feb 13, 2017 57 `````` `````` 58 59 60 61 62 `````` use import Transitivity end module SameTransitivityCheck `````` Jean-Christophe Filliâtre committed Feb 13, 2017 63 `````` `````` 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 `````` use import Transitivity use import SameTransitivity goal G2: forall x: a. is_c x end module CoercionIf function is_zero int : bool meta coercion function is_zero goal G3: if 42 then 1=2 else 3=4 end module TrickyPolymorphicAlpha use import list.List type t 'a type t1 'a type t2 'a `````` Jean-Christophe Filliâtre committed Feb 13, 2017 90 91 `````` function f (t 'a) : t1 (list 'a) meta coercion function f `````` 92 `````` `````` Jean-Christophe Filliâtre committed Feb 13, 2017 93 94 `````` function g (t1 'a) : t2 (list 'a) meta coercion function g `````` 95 `````` `````` Jean-Christophe Filliâtre committed Feb 13, 2017 96 `````` goal a : forall x:t int, y:t2 (list (list int)). x = y `````` 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 `````` end module TrickyPolymorphicBeta use import list.List type t 'a type t1 'a type t2 'a function f (t 'a) : t1 (list 'b) meta coercion function f function g (t1 'a) : t2 (list 'a) meta coercion function g goal a : forall x:t int, y:t2 (list (list int)). x = y end module InTypeArgs `````` Jean-Christophe Filliâtre committed Feb 13, 2017 120 121 122 `````` type t1 'a type t2 'a type t3 'a `````` 123 `````` `````` Jean-Christophe Filliâtre committed Feb 13, 2017 124 125 `````` function t2_of_t1 (t1 'a) : t2 'a meta coercion function t2_of_t1 `````` 126 `````` `````` Jean-Christophe Filliâtre committed Feb 13, 2017 127 128 `````` function bool_of_int bool : int meta coercion function bool_of_int `````` 129 `````` `````` Jean-Christophe Filliâtre committed Feb 13, 2017 130 `````` function h (x: t1 'a) (b: int) : t1 int `````` 131 `````` `````` Jean-Christophe Filliâtre committed Feb 13, 2017 132 `````` goal G: forall x: t1 'a, y: t2 int. h x true = y `````` 133 134 `````` end``````