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
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1

2
module Simple
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
3

4
  type t
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
5

6 7
  function f t : int
  meta coercion function f
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
8

9
  goal G: forall x: t. x = 42
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
10

11
end
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
12

13
module SameOne
14

15
  use import Simple
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
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

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
57

58 59 60 61 62
  use import Transitivity

end

module SameTransitivityCheck
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

90 91
  function f (t 'a) : t1 (list 'a)
  meta coercion function f
92

93 94
  function g (t1 'a) : t2 (list 'a)
  meta coercion function g
95

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

120 121 122
  type t1 'a
  type t2 'a
  type t3 'a
123

124 125
  function t2_of_t1 (t1 'a) : t2 'a
  meta coercion function t2_of_t1
126

127 128
  function bool_of_int bool : int
  meta coercion function bool_of_int
129

130
  function h (x: t1 'a) (b: int) : t1 int
131

132
  goal G: forall x: t1 'a, y: t2 int. h x true = y
133 134

end