test-poly.why 2.06 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4


theory Mono

5 6
goal g0 : 2 = 3

7
use int.Int
MARCHE Claude's avatar
MARCHE Claude committed
8 9 10

goal g : 2+2 = 5

11 12 13 14

(* bin/why3prove.byte tests/test-poly.why --debug detect_poly -a detect_polymorphism -D why3 -T Mono -G g *)


MARCHE Claude's avatar
MARCHE Claude committed
15 16 17
end


18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34
theory MonoType

type t = A | B

goal g0 : A <> B

goal g1 : forall x. x = A \/ x = B

type u = C | D t

goal g2 : forall x y. y = D x

type a = E | F b
with b = G | H a

goal g3 : forall x. x <> F (H x)

35 36 37 38 39 40 41 42
type v = I (p:t) | J (p:t) u

constant x : v

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

goal g5 : match x with I y -> y | J y _ -> y end = A

43 44
(* bin/why3prove.byte tests/test-poly.why --debug detect_poly -a detect_polymorphism -D why3 -T MonoType -G g0 *)

45 46 47
end


MARCHE Claude's avatar
MARCHE Claude committed
48 49 50 51 52 53
theory PolyType

type t 'a = A 'a

goal g: forall x y:'a. A x = A y

54 55
(* bin/why3prove.byte tests/test-poly.why --debug detect_poly -a detect_polymorphism -D why3 -T PolyType -G g *)

MARCHE Claude's avatar
MARCHE Claude committed
56 57 58 59 60
end


theory TestList

61
use list.List
MARCHE Claude's avatar
MARCHE Claude committed
62 63 64 65

goal g : match Cons 42 Nil with Nil -> false | Cons x _ -> x=42 end

end
66 67


68 69 70 71 72 73 74 75 76 77
theory MonoSymb

function id (x:int) : int = x

goal g: forall x:int. id x = x

(* bin/why3prove.byte tests/test-poly.why --debug detect_poly -a detect_polymorphism -D why3 -T PolySymb -G g *)

end

78 79 80 81
theory PolySymb

function id (x:'a) : 'a = x

82 83
meta "encoding:ignore_polymorphism_ls" function id

84 85 86 87 88 89 90 91 92 93 94 95 96
goal g: forall x:int. id x = x

(* bin/why3prove.byte tests/test-poly.why --debug detect_poly -a detect_polymorphism -D why3 -T PolySymb -G g *)

end

theory PolyProp

goal g: forall x:'a. x = x

(* bin/why3prove.byte tests/test-poly.why --debug detect_poly -a detect_polymorphism -D why3 -T PolyProp -G g *)

end
97 98 99 100


theory Map

101 102
  use int.Int
  use map.Map
103 104 105 106 107 108 109 110 111 112

  goal g: forall m:map int int.
    let m' = m[0<-42][1<-42] in
    m'[0] + m'[1] >= 0

(* bin/why3prove.byte tests/test-poly.why --debug detect_poly -D why3_smt -T Map -G g *)

end


113 114
theory TestBool

115
  use bool.Bool
116 117 118 119 120 121 122 123 124 125 126

  goal g : forall b:bool.  b = b

(*

bin/why3prove tests/test-poly.why -D why3_smt -T TestBool -G g

*)

end

127 128 129

theory TestTuple

130 131
  use int.Int
  use bool.Bool
132 133 134 135 136 137

  type t = (int,bool)

  goal g: forall x:t. match x with (a,b) -> a >= 0 /\ b end

end