Encode shape information in `PmOracle`
[ghc.git] / testsuite / tests / pmcheck / should_compile / T17096.hs
1 {-# language PatternSynonyms #-}
2 -- Taken from the Dhall library
3 module T17096 where
4
5 data Expr s a
6 = Const String
7 | Var Int
8 | Lam String (Expr s a) (Expr s a)
9 | Pi String (Expr s a) (Expr s a)
10 | App (Expr s a) (Expr s a)
11 | Let String (Maybe (Expr s a)) (Expr s a) (Expr s a)
12 | Annot (Expr s a) (Expr s a)
13 | Bool
14 | BoolLit Bool
15 | BoolAnd (Expr s a) (Expr s a)
16 | BoolOr (Expr s a) (Expr s a)
17 | BoolEQ (Expr s a) (Expr s a)
18 | BoolNE (Expr s a) (Expr s a)
19 | BoolIf (Expr s a) (Expr s a) (Expr s a)
20 | Natural
21 | NaturalLit Integer
22 | NaturalFold
23 | NaturalBuild
24 | NaturalIsZero
25 | NaturalEven
26 | NaturalOdd
27 | NaturalToInteger
28 | NaturalShow
29 | NaturalSubtract
30 | NaturalPlus (Expr s a) (Expr s a)
31 | NaturalTimes (Expr s a) (Expr s a)
32 | Integer
33 | IntegerLit Integer
34 | IntegerShow
35 | IntegerToDouble
36 | Double
37 | DoubleLit Double
38 | DoubleShow
39 | String
40 | StringLit String
41 | StringAppend (Expr s a) (Expr s a)
42 | StringShow
43 | List
44 | ListLit (Maybe (Expr s a)) [Expr s a]
45 | ListAppend (Expr s a) (Expr s a)
46 | ListBuild
47 | ListFold
48 | ListLength
49 | ListHead
50 | ListLast
51 | ListIndexed
52 | ListReverse
53 | Optional
54 | Some (Expr s a)
55 | None
56 | OptionalFold
57 | OptionalBuild
58 | Record [(String, Expr s a)]
59 | RecordLit [(String, Expr s a)]
60 | Union [(String, Maybe (Expr s a))]
61 | Combine (Expr s a) (Expr s a)
62 | CombineTypes (Expr s a) (Expr s a)
63 | Prefer (Expr s a) (Expr s a)
64 | Merge (Expr s a) (Expr s a) (Maybe (Expr s a))
65 | ToMap (Expr s a) (Maybe (Expr s a))
66 | Field (Expr s a) String
67 | Project (Expr s a) (Either [String] (Expr s a))
68 | Assert (Expr s a)
69 | Equivalent (Expr s a) (Expr s a)
70 | Note s (Expr s a)
71 | ImportAlt (Expr s a) (Expr s a)
72 | Embed a
73
74 isNormalized :: Eq a => Expr s a -> Bool
75 isNormalized = loop
76 where
77 loop e = case e of
78 Const _ -> True
79 Var _ -> True
80 Lam _ a b -> loop a && loop b
81 Pi _ a b -> loop a && loop b
82 App f a -> loop f && loop a && case App f a of
83 App (Lam _ _ _) _ -> False
84 App (App ListBuild _) (App (App ListFold _) _) -> False
85 App NaturalBuild (App NaturalFold _) -> False
86 App (App OptionalBuild _) (App (App OptionalFold _) _) -> False
87 App (App (App (App NaturalFold (NaturalLit _)) _) _) _ -> False
88 App NaturalFold (NaturalLit _) -> False
89 App NaturalBuild _ -> False
90 App NaturalIsZero (NaturalLit _) -> False
91 App NaturalEven (NaturalLit _) -> False
92 App NaturalOdd (NaturalLit _) -> False
93 App NaturalShow (NaturalLit _) -> False
94 App (App NaturalSubtract (NaturalLit _)) (NaturalLit _) -> False
95 App (App NaturalSubtract (NaturalLit 0)) _ -> False
96 App (App NaturalSubtract _) (NaturalLit 0) -> False
97 App (App NaturalSubtract x) y -> not (undefined x y)
98 App NaturalToInteger (NaturalLit _) -> False
99 App IntegerShow (IntegerLit _) -> False
100 App IntegerToDouble (IntegerLit _) -> False
101 App DoubleShow (DoubleLit _) -> False
102 App (App OptionalBuild _) _ -> False
103 App (App ListBuild _) _ -> False
104 App (App (App (App (App ListFold _) (ListLit _ _)) _) _) _ ->
105 False
106 App (App ListLength _) (ListLit _ _) -> False
107 App (App ListHead _) (ListLit _ _) -> False
108 App (App ListLast _) (ListLit _ _) -> False
109 App (App ListIndexed _) (ListLit _ _) -> False
110 App (App ListReverse _) (ListLit _ _) -> False
111 App (App (App (App (App OptionalFold _) (Some _)) _) _) _ ->
112 False
113 App (App (App (App (App OptionalFold _) (App None _)) _) _) _ ->
114 False
115 App StringShow (StringLit _) ->
116 False
117 _ -> True
118 Let _ _ _ _ -> False
119 Annot _ _ -> False
120 Bool -> True
121 BoolLit _ -> True
122 BoolAnd x y -> loop x && loop y && decide x y
123 where
124 decide (BoolLit _) _ = False
125 decide _ (BoolLit _) = False
126 decide l r = not (undefined l r)
127 BoolOr x y -> loop x && loop y && decide x y
128 where
129 decide (BoolLit _) _ = False
130 decide _ (BoolLit _) = False
131 decide l r = not (undefined l r)
132 BoolEQ x y -> loop x && loop y && decide x y
133 where
134 decide (BoolLit True) _ = False
135 decide _ (BoolLit True) = False
136 decide l r = not (undefined l r)
137 BoolNE x y -> loop x && loop y && decide x y
138 where
139 decide (BoolLit False) _ = False
140 decide _ (BoolLit False ) = False
141 decide l r = not (undefined l r)
142 BoolIf x y z ->
143 loop x && loop y && loop z && decide x y z
144 where
145 decide (BoolLit _) _ _ = False
146 decide _ (BoolLit True) (BoolLit False) = False
147 decide _ l r = not (undefined l r)
148 Natural -> True
149 NaturalLit _ -> True
150 NaturalFold -> True
151 NaturalBuild -> True
152 NaturalIsZero -> True
153 NaturalEven -> True
154 NaturalOdd -> True
155 NaturalShow -> True
156 NaturalSubtract -> True
157 NaturalToInteger -> True
158 NaturalPlus x y -> loop x && loop y && decide x y
159 where
160 decide (NaturalLit 0) _ = False
161 decide _ (NaturalLit 0) = False
162 decide (NaturalLit _) (NaturalLit _) = False
163 decide _ _ = True
164 NaturalTimes x y -> loop x && loop y && decide x y
165 where
166 decide (NaturalLit 0) _ = False
167 decide _ (NaturalLit 0) = False
168 decide (NaturalLit 1) _ = False
169 decide _ (NaturalLit 1) = False
170 decide (NaturalLit _) (NaturalLit _) = False
171 decide _ _ = True
172 Integer -> True
173 IntegerLit _ -> True
174 IntegerShow -> True
175 IntegerToDouble -> True
176 Double -> True
177 DoubleLit _ -> True
178 DoubleShow -> True
179 String -> True
180 StringLit _ -> False
181 StringAppend _ _ -> False
182 StringShow -> True
183 List -> True
184 ListLit t es -> all loop t && all loop es
185 ListAppend x y -> loop x && loop y && decide x y
186 where
187 decide (ListLit _ m) _ | null m = False
188 decide _ (ListLit _ n) | null n = False
189 decide (ListLit _ _) (ListLit _ _) = False
190 decide _ _ = True
191 ListBuild -> True
192 ListFold -> True
193 ListLength -> True
194 ListHead -> True
195 ListLast -> True
196 ListIndexed -> True
197 ListReverse -> True
198 Optional -> True
199 Some a -> loop a
200 None -> True
201 OptionalFold -> True
202 OptionalBuild -> True
203 Record kts -> undefined kts && all loop (map snd kts)
204 RecordLit kvs -> undefined kvs && all loop (map snd kvs)
205 Union kts -> undefined kts && all (all loop) (map snd kts)
206 Combine x y -> loop x && loop y && decide x y
207 where
208 decide (RecordLit m) _ | null m = False
209 decide _ (RecordLit n) | null n = False
210 decide (RecordLit _) (RecordLit _) = False
211 decide _ _ = True
212 CombineTypes x y -> loop x && loop y && decide x y
213 where
214 decide (Record m) _ | null m = False
215 decide _ (Record n) | null n = False
216 decide (Record _) (Record _) = False
217 decide _ _ = True
218 Prefer x y -> loop x && loop y && decide x y
219 where
220 decide (RecordLit m) _ | null m = False
221 decide _ (RecordLit n) | null n = False
222 decide (RecordLit _) (RecordLit _) = False
223 decide l r = not (undefined l r)
224 Merge x y t -> loop x && loop y && all loop t
225 ToMap x t -> case x of
226 RecordLit _ -> False
227 _ -> loop x && all loop t
228 Field r k -> case r of
229 RecordLit _ -> False
230 Project _ _ -> False
231 Prefer (RecordLit m) _ -> map fst m == [k] && loop r
232 Prefer _ (RecordLit _) -> False
233 Combine (RecordLit m) _ -> map fst m == [k] && loop r
234 Combine _ (RecordLit m) -> map fst m == [k] && loop r
235 _ -> loop r
236 Project r p -> loop r &&
237 case p of
238 Left s -> case r of
239 RecordLit _ -> False
240 _ -> not (null s) && undefined s
241 Right e' -> case e' of
242 Record _ -> False
243 _ -> loop e'
244 Assert t -> loop t
245 Equivalent l r -> loop l && loop r
246 Note _ e' -> loop e'
247 ImportAlt l _r -> loop l
248 Embed _ -> True
249
250 {-# COMPLETE
251 Let'
252 , Const
253 , Var
254 , Lam
255 , Pi
256 , App
257 , Annot
258 , Bool
259 , BoolLit
260 , BoolAnd
261 , BoolOr
262 , BoolEQ
263 , BoolNE
264 , BoolIf
265 , Natural
266 , NaturalLit
267 , NaturalFold
268 , NaturalBuild
269 , NaturalIsZero
270 , NaturalEven
271 , NaturalOdd
272 , NaturalToInteger
273 , NaturalShow
274 , NaturalSubtract
275 , NaturalPlus
276 , NaturalTimes
277 , Integer
278 , IntegerLit
279 , IntegerShow
280 , IntegerToDouble
281 , Double
282 , DoubleLit
283 , DoubleShow
284 , String
285 , StringLit
286 , StringAppend
287 , StringShow
288 , List
289 , ListLit
290 , ListAppend
291 , ListBuild
292 , ListFold
293 , ListLength
294 , ListHead
295 , ListLast
296 , ListIndexed
297 , ListReverse
298 , Optional
299 , Some
300 , None
301 , OptionalFold
302 , OptionalBuild
303 , Record
304 , RecordLit
305 , Union
306 , Combine
307 , CombineTypes
308 , Prefer
309 , Merge
310 , ToMap
311 , Field
312 , Project
313 , Assert
314 , Equivalent
315 , Note
316 , ImportAlt
317 , Embed
318 #-}
319 pattern Let' x mA a b = Let x mA a b