tests/test-poly.why

   1
   2
   3 theory Mono
   4
   5 goal g0 : 2 = 3
   6
   7 use int.Int
   8
   9 goal g : 2+2 = 5
  10
  11
  12 (* bin/why3prove.byte tests/test-poly.why --debug detect_poly -a detect_polymorphism -D why3 -T Mono -G g *)
  13
  14
  15 end
  16
  17
  18 theory MonoType
  19
  20 type t = A | B
  21
  22 goal g0 : A <> B
  23
  24 goal g1 : forall x. x = A \/ x = B
  25
  26 type u = C | D t
  27
  28 goal g2 : forall x y. y = D x
  29
  30 type a = E | F b
  31 with b = G | H a
  32
  33 goal g3 : forall x. x <> F (H x)
  34
  35 type v = I (p:t) | J (p:t) u
  36
  37 constant x : v
  38
  39 goal g4 : match x with I y -> y=A | J y (D z) -> z=A | J B z -> z=C | J A C -> true end
  40
  41 goal g5 : match x with I y -> y | J y _ -> y end = A
  42
  43 (* bin/why3prove.byte tests/test-poly.why --debug detect_poly -a detect_polymorphism -D why3 -T MonoType -G g0 *)
  44
  45 end
  46
  47
  48 theory PolyType
  49
  50 type t 'a = A 'a
  51
  52 goal g: forall x y:'a. A x = A y
  53
  54 (* bin/why3prove.byte tests/test-poly.why --debug detect_poly -a detect_polymorphism -D why3 -T PolyType -G g *)
  55
  56 end
  57
  58
  59 theory TestList
  60
  61 use list.List
  62
  63 goal g : match Cons 42 Nil with Nil -> false | Cons x _ -> x=42 end
  64
  65 end
  66
  67
  68 theory MonoSymb
  69
  70 function id (x:int) : int = x
  71
  72 goal g: forall x:int. id x = x
  73
  74 (* bin/why3prove.byte tests/test-poly.why --debug detect_poly -a detect_polymorphism -D why3 -T PolySymb -G g *)
  75
  76 end
  77
  78 theory PolySymb
  79
  80 function id (x:'a) : 'a = x
  81
  82 meta "encoding:ignore_polymorphism_ls" function id
  83
  84 goal g: forall x:int. id x = x
  85
  86 (* bin/why3prove.byte tests/test-poly.why --debug detect_poly -a detect_polymorphism -D why3 -T PolySymb -G g *)
  87
  88 end
  89
  90 theory PolyProp
  91
  92 goal g: forall x:'a. x = x
  93
  94 (* bin/why3prove.byte tests/test-poly.why --debug detect_poly -a detect_polymorphism -D why3 -T PolyProp -G g *)
  95
  96 end
  97
  98
  99 theory Map
 100
 101   use int.Int
 102   use map.Map
 103
 104   goal g: forall m:map int int.
 105     let m' = m[0<-42][1<-42] in
 106     m'[0] + m'[1] >= 0
 107
 108 (* bin/why3prove.byte tests/test-poly.why --debug detect_poly -D why3_smt -T Map -G g *)
 109
 110 end
 111
 112
 113 theory TestBool
 114
 115   use bool.Bool
 116
 117   goal g : forall b:bool.  b = b
 118
 119 (*
 120
 121 bin/why3prove tests/test-poly.why -D why3_smt -T TestBool -G g
 122
 123 *)
 124
 125 end
 126
 127
 128 theory TestTuple
 129
 130   use int.Int
 131   use bool.Bool
 132
 133   type t = (int,bool)
 134
 135   goal g: forall x:t. match x with (a,b) -> a >= 0 /\ b end
 136
 137 end