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
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
|
pattern Q1 x1_0 x2_1 x3_2 <- ((x1_0, x2_1), [x3_2], _, _)
pattern x1_0 Q2 x2_1 = GHC.Tuple.Solo (x1_0, x2_1)
pattern Q3 {qx3, qy3, qz3} <- ((qx3, qy3), [qz3]) where
Q3 qx3 qy3 qz3 = ((qx3, qy3), [qz3])
T8761.hs:(16,1)-(39,13): Splicing declarations
do [qx1, qy1, qz1] <- mapM
(\ i -> newName $ "x" ++ show i) [1, 2, 3]
let nm1 = mkName "Q1"
prefixPat
= patSynD
nm1 (prefixPatSyn [qx1, qy1, qz1]) unidir
(tupP [tupP [varP qx1, varP qy1], listP [varP qz1], wildP, wildP])
[qx2, qy2] <- mapM (\ i -> newName $ "x" ++ show i) [1, 2]
let nm2 = mkName "Q2"
infixPat
= patSynD
nm2 (infixPatSyn qx2 qy2) implBidir
(tupP [tupP [varP qx2, varP qy2]])
let nm3 = mkName "Q3"
[qx3, qy3, qz3] = map mkName ["qx3", "qy3", "qz3"]
patP = tupP [tupP [varP qx3, varP qy3], listP [varP qz3]]
patE = tupE [tupE [varE qx3, varE qy3], listE [varE qz3]]
cls = clause [varP qx3, varP qy3, varP qz3] (normalB patE) []
recordPat
= patSynD nm3 (recordPatSyn [qx3, qy3, qz3]) (explBidir [cls]) patP
pats <- sequence [prefixPat, infixPat, recordPat]
mapM_ (runIO . hPutStrLn stderr . pprint) pats
return pats
======>
pattern Q1 x1 x2 x3 <- ((x1, x2), [x3], _, _)
pattern x1 `Q2` x2 = Solo(x1, x2)
pattern Q3{qx3, qy3, qz3} <- ((qx3, qy3), [qz3]) where
Q3 qx3 qy3 qz3 = ((qx3, qy3), [qz3])
T8761.hs:(42,1)-(46,29): Splicing declarations
[d| pattern P1 x y z <- ((x, y), [z], _, _)
pattern P2 x y z = ((x, y), [z])
pattern P3 x y z <- ((x, y), [z]) where
P3 x y z = ((x, y), [z]) |]
======>
pattern P1 x y z <- ((x, y), [z], _, _)
pattern P2 x y z = ((x, y), [z])
pattern P3 x y z <- ((x, y), [z]) where
P3 x y z = ((x, y), [z])
T8761.hs:(49,1)-(53,21): Splicing declarations
[d| pattern x :*: y <- ((x, _), [y])
pattern x :+: y = (x, y)
pattern x :~: y <- (x, y) where
x :~: y = (x, y) |]
======>
pattern x :*: y <- ((x, _), [y])
pattern x :+: y = (x, y)
pattern x :~: y <- (x, y) where
(:~:) x y = (x, y)
T8761.hs:(56,1)-(62,23): Splicing declarations
[d| pattern R1{x1, y1} <- ((x1, _), [y1])
getX1 = x1 ((1, 2), [3])
getY1 = y1 ((1, 2), [3])
pattern R2{x2, y2} = (x2, [y2])
pattern R3{x3, y3} <- (x3, [y3]) where
R3 x y = (x, [y]) |]
======>
pattern R1{x1, y1} <- ((x1, _), [y1])
getX1 = x1 ((1, 2), [3])
getY1 = y1 ((1, 2), [3])
pattern R2{x2, y2} = (x2, [y2])
pattern R3{x3, y3} <- (x3, [y3]) where
R3 x y = (x, [y])
T8761.hs:(71,1)-(105,39): Splicing declarations
[d| pattern P :: Bool
pattern P <- True
pattern Pe :: () => forall a. a -> Ex
pattern Pe x <- MkEx x
pattern Pu :: forall a. a -> a
pattern Pu x <- x
pattern Pue :: forall a. () => forall b. a -> b -> (a, Ex)
pattern Pue x y <- (x, MkEx y)
pattern Pur :: forall a. (Num a, Eq a) => a -> [a]
pattern Pur x <- [x, 1]
pattern Purp ::
forall a b. (Num a, Eq a) => Show b => a -> b -> ([a], UnivProv b)
pattern Purp x y <- ([x, 1], MkUnivProv y)
pattern Pure ::
forall a. (Num a, Eq a) => forall b. a -> b -> ([a], Ex)
pattern Pure x y <- ([x, 1], MkEx y)
pattern Purep ::
forall a.
(Num a, Eq a) => forall b. Show b => a -> b -> ([a], ExProv)
pattern Purep x y <- ([x, 1], MkExProv y)
pattern Pep :: () => forall a. Show a => a -> ExProv
pattern Pep x <- MkExProv x
pattern Pup :: forall a. () => Show a => a -> UnivProv a
pattern Pup x <- MkUnivProv x
pattern Puep ::
forall a. () => forall b. (Show b) => a -> b -> (ExProv, a)
pattern Puep x y <- (MkExProv y, x) |]
======>
pattern P :: Bool
pattern P <- True
pattern Pe :: () => forall a. a -> Ex
pattern Pe x <- MkEx x
pattern Pu :: forall a. a -> a
pattern Pu x <- x
pattern Pue :: forall a. () => forall b. a -> b -> (a, Ex)
pattern Pue x y <- (x, MkEx y)
pattern Pur :: forall a. (Num a, Eq a) => a -> [a]
pattern Pur x <- [x, 1]
pattern Purp ::
forall a b. (Num a, Eq a) => Show b => a -> b -> ([a], UnivProv b)
pattern Purp x y <- ([x, 1], MkUnivProv y)
pattern Pure ::
forall a. (Num a, Eq a) => forall b. a -> b -> ([a], Ex)
pattern Pure x y <- ([x, 1], MkEx y)
pattern Purep ::
forall a.
(Num a, Eq a) => forall b. Show b => a -> b -> ([a], ExProv)
pattern Purep x y <- ([x, 1], MkExProv y)
pattern Pep :: () => forall a. Show a => a -> ExProv
pattern Pep x <- MkExProv x
pattern Pup :: forall a. () => Show a => a -> UnivProv a
pattern Pup x <- MkUnivProv x
pattern Puep ::
forall a. () => forall b. Show b => a -> b -> (ExProv, a)
pattern Puep x y <- (MkExProv y, x)
pattern T8761.P :: GHC.Types.Bool
pattern T8761.Pe :: () => forall (a_0 :: *) . a_0 -> T8761.Ex
pattern T8761.Pu :: forall (a_0 :: *) . a_0 -> a_0
pattern T8761.Pue :: forall (a_0 :: *) . () => forall (b_1 :: *) .
a_0 -> b_1 -> (a_0, T8761.Ex)
pattern T8761.Pur :: forall (a_0 :: *) . (GHC.Num.Num a_0,
GHC.Classes.Eq a_0) =>
a_0 -> [a_0]
pattern T8761.Purp :: forall (a_0 :: *) (b_1 :: *) . (GHC.Num.Num a_0,
GHC.Classes.Eq a_0) =>
GHC.Show.Show b_1 => a_0 -> b_1 -> ([a_0], T8761.UnivProv b_1)
pattern T8761.Pure :: forall (a_0 :: *) . (GHC.Num.Num a_0,
GHC.Classes.Eq a_0) =>
forall (b_1 :: *) . a_0 -> b_1 -> ([a_0], T8761.Ex)
pattern T8761.Purep :: forall (a_0 :: *) . (GHC.Num.Num a_0,
GHC.Classes.Eq a_0) =>
forall (b_1 :: *) . GHC.Show.Show b_1 =>
a_0 -> b_1 -> ([a_0], T8761.ExProv)
pattern T8761.Pep :: () => forall (a_0 :: *) . GHC.Show.Show a_0 =>
a_0 -> T8761.ExProv
pattern T8761.Pup :: forall (a_0 :: *) . () => GHC.Show.Show a_0 =>
a_0 -> T8761.UnivProv a_0
pattern T8761.Puep :: forall (a_0 :: *) . () => forall (b_1 :: *) . GHC.Show.Show b_1 =>
a_0 -> b_1 -> (T8761.ExProv, a_0)
T8761.hs:(108,1)-(117,25): Splicing declarations
do infos <- mapM
reify
['P, 'Pe, 'Pu, 'Pue, 'Pur, 'Purp, 'Pure, 'Purep, 'Pep, 'Pup, 'Puep]
mapM_ (runIO . hPutStrLn stderr . pprint) infos
[d| theAnswerIs = 42 |]
======>
theAnswerIs = 42
|
