blob: d0077edbdb3995a43605473bb4a4385036d556ae (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
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
90
91
92
93
94
95
96
97
98
99
100
101
102
|
{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies #-}
module TcTypeNatSimple where
import GHC.TypeLits as L
import Data.Proxy
--------------------------------------------------------------------------------
-- Test evaluation
e1 :: Proxy (2 + 3) -> Proxy 5
e1 = id
e2 :: Proxy (2 L.* 3) -> Proxy 6
e2 = id
e3 :: Proxy (2 ^ 3) -> Proxy 8
e3 = id
e4 :: Proxy (0 + x) -> Proxy x
e4 = id
e5 :: Proxy (x + 0) -> Proxy x
e5 = id
e6 :: Proxy (x L.* 0) -> Proxy 0
e6 = id
e7 :: Proxy (0 L.* x) -> Proxy 0
e7 = id
e8 :: Proxy (x L.* 1) -> Proxy x
e8 = id
e9 :: Proxy (1 L.* x) -> Proxy x
e9 = id
e10 :: Proxy (x ^ 1) -> Proxy x
e10 = id
e11 :: Proxy (1 ^ x) -> Proxy 1
e11 = id
e12 :: Proxy (x ^ 0) -> Proxy 1
e12 = id
e13 :: Proxy (1 <=? 2) -> Proxy True
e13 = id
e14 :: Proxy (2 <=? 1) -> Proxy False
e14 = id
e15 :: Proxy (x <=? x) -> Proxy True
e15 = id
e16 :: Proxy (0 <=? x) -> Proxy True
e16 = id
e17 :: Proxy (3 - 2) -> Proxy 1
e17 = id
e18 :: Proxy (a - 0) -> Proxy a
e18 = id
e19 :: Proxy (Div 10 3) -> Proxy 3
e19 = id
e20 :: Proxy (Div x 1) -> Proxy x
e20 = id
e21 :: Proxy (Mod 10 3) -> Proxy 1
e21 = id
e22 :: Proxy (Mod x 1) -> Proxy 0
e22 = id
e23 :: Proxy (Log2 10) -> Proxy 3
e23 = id
--------------------------------------------------------------------------------
-- Test interactions with inerts
-- ti1 :: Proxy (x + y) -> Proxy x -> ()
-- ti1 _ _ = ()
ti2 :: Proxy (y + x) -> Proxy x -> ()
ti2 _ _ = ()
ti3 :: Proxy (2 L.* y) -> ()
ti3 _ = ()
ti4 :: Proxy (y L.* 2) -> ()
ti4 _ = ()
ti5 :: Proxy (2 ^ y) -> ()
ti5 _ = ()
ti6 :: Proxy (y ^ 2) -> ()
ti6 _ = ()
ti8 :: Proxy (x - y) -> Proxy x -> ()
ti8 _ _ = ()
ti9 :: Proxy (y - x) -> Proxy x -> ()
ti9 _ _ = ()
|
