summaryrefslogtreecommitdiff
path: root/testdata/language-features/adt/gadt01.out
diff options
context:
space:
mode:
Diffstat (limited to 'testdata/language-features/adt/gadt01.out')
-rw-r--r--testdata/language-features/adt/gadt01.out377
1 files changed, 376 insertions, 1 deletions
diff --git a/testdata/language-features/adt/gadt01.out b/testdata/language-features/adt/gadt01.out
index 4791ed55..5c850279 100644
--- a/testdata/language-features/adt/gadt01.out
+++ b/testdata/language-features/adt/gadt01.out
@@ -1 +1,376 @@
1True \ No newline at end of file 1main :: Bool
2main = True
3------------ desugared source code
4data V :: Nat -> Type -> Type where
5 V1_ :: forall (a :: _) . a -> V (fromInt 1) a
6 V2_ :: forall (b :: _) . b -> b -> V (fromInt 2) b
7
8data M :: Type -> String -> Type where
9 Value :: forall (a :: _) . a -> forall (b :: _) . M a b
10
11data M2 (_ :: Type) :: String -> Type where
12 Value2 :: forall a . a -> forall (b :: _) . M2 a b
13
14data M3 (_ :: Type) :: String -> Type where
15 Value3 :: forall a (b :: _) . a -> M3 a b
16
17g
18 = _lhs
19 g
20 (_rhs (case'M2 (\(_ :: _) (_ :: _) -> _ :: _) \(a :: _) @(_ :: _) -> a))
21
22h
23 = _lhs h \(a :: _) -> case'M3 (\(_ :: _) (_ :: _) -> _) (\(b :: _) -> _rhs b) a
24
25value1 :: M Bool "m"
26value1 = _lhs value1 (_rhs (Value True))
27
28value2 :: M2 Bool "s"
29value2 = _lhs value2 (_rhs (Value2 True))
30
31value3 :: M3 Bool "t"
32value3 = _lhs value3 (_rhs (Value3 True))
33
34main = _lhs main (_rhs (g value2 && h value3))
35------------ core code
36'M :: Type -> String -> Type
37'M = <<type constructor with 2 indices; constructors: Value>>
38
39'M2 :: Type -> String -> Type
40'M2 = <<type constructor with 1 indices; constructors: Value2>>
41
42'M3 :: Type -> String -> Type
43'M3 = <<type constructor with 1 indices; constructors: Value3>>
44
45'V :: Nat -> Type -> Type
46'V = <<type constructor with 2 indices; constructors: V1_, V2_>>
47
48V1_ :: forall a . a -> V 1 a
49V1_ = <<0th constructor of 'V>>
50
51V2_ :: forall a . a -> a -> V 2 a
52V2_ = <<1st constructor of 'V>>
53
54Value :: forall a . a -> forall (b :: String) . M a b
55Value = <<0th constructor of 'M>>
56
57Value2 :: forall a . a -> forall (b :: String) . M2 a b
58Value2 = <<0th constructor of 'M2>>
59
60Value3 :: forall a (b :: String) . a -> M3 a b
61Value3 = <<0th constructor of 'M3>>
62
63case'M
64 :: forall (a :: forall b (c :: String) -> M b c -> Type)
65 -> (forall d . forall (e :: d) -> forall (f :: String) . a d f ('Value d e f))
66 -> forall g (h :: String) . forall (i :: M g h) -> a g h i
67case'M = \a b c d e -> <<case function of a type with 0 parameters>>
68
69case'M2
70 :: forall a
71 . forall (b :: forall (c :: String) -> M2 a c -> Type)
72 -> (forall (d :: a) -> forall (e :: String) . b e ('Value2 d e))
73 -> forall (f :: String) . forall (g :: M2 a f) -> b f g
74case'M2 = \_ a b c d -> <<case function of a type with 1 parameters>>
75
76case'M3
77 :: forall a
78 . forall (b :: forall (c :: String) -> M3 a c -> Type)
79 -> (forall (d :: String) . forall (e :: a) -> b d ('Value3 d e))
80 -> forall (f :: String) . forall (g :: M3 a f) -> b f g
81case'M3 = \_ a b c d -> <<case function of a type with 1 parameters>>
82
83case'V
84 :: forall (a :: forall (b :: Nat) c -> V b c -> Type)
85 -> (forall d . forall (e :: d) -> a 1 d ('V1_ d e))
86 -> (forall f . forall (g :: f) (h :: f) -> a 2 f ('V2_ f g h))
87 -> forall (i :: Nat) j . forall (k :: V i j) -> a i j k
88case'V = \a b c d e f -> <<case function of a type with 0 parameters>>
89
90g :: forall a (b :: String) . M2 a b -> a
91g = \a -> _rhs \b c -> case'M2 (\_ _ -> a) (\d _ -> d) b c
92
93h :: forall a (b :: String) . M3 a b -> a
94h = \a b c -> case'M3 (\_ _ -> a) (\_ d -> _rhs d) b c
95
96main :: Bool
97main = _rhs True
98
99match'M
100 :: forall (a :: Type -> Type)
101 -> (forall b (c :: String) -> a (M b c)) -> forall d -> a d -> a d
102match'M = \a b c d -> <<type case function>>
103
104match'M2
105 :: forall (a :: Type -> Type)
106 -> (forall b (c :: String) -> a (M2 b c)) -> forall d -> a d -> a d
107match'M2 = \a b c d -> <<type case function>>
108
109match'M3
110 :: forall (a :: Type -> Type)
111 -> (forall b (c :: String) -> a (M3 b c)) -> forall d -> a d -> a d
112match'M3 = \a b c d -> <<type case function>>
113
114match'V
115 :: forall (a :: Type -> Type)
116 -> (forall (b :: Nat) c -> a (V b c)) -> forall d -> a d -> a d
117match'V = \a b c d -> <<type case function>>
118
119value1 :: M Bool "m"
120value1 = _rhs (Value 'Bool True "m")
121
122value2 :: M2 Bool "s"
123value2 = _rhs (Value2 True "s")
124
125value3 :: M3 Bool "t"
126value3 = _rhs (Value3 "t" True)
127------------ tooltips
128testdata/language-features/adt/gadt01.lc 2:6-2:7
129 Nat -> Type -> Type | Nat -> Type -> Type | Type | Type | Nat
130 -> Type -> Type | Type | Type | Type
131testdata/language-features/adt/gadt01.lc 2:6-4:25
132 Type | Type
133testdata/language-features/adt/gadt01.lc 2:11-2:14
134 Type
135testdata/language-features/adt/gadt01.lc 2:18-2:22
136 Type
137testdata/language-features/adt/gadt01.lc 2:18-2:30
138 Type
139testdata/language-features/adt/gadt01.lc 2:26-2:30
140 Type | Type
141testdata/language-features/adt/gadt01.lc 3:3-3:6
142 forall a . a -> V 1 a | V 1 _b
143testdata/language-features/adt/gadt01.lc 3:3-3:20
144 Type | Type | Type
145testdata/language-features/adt/gadt01.lc 3:10-3:11
146 _b
147testdata/language-features/adt/gadt01.lc 3:10-3:20
148 Type
149testdata/language-features/adt/gadt01.lc 3:15-3:16
150 Nat -> Type -> Type
151testdata/language-features/adt/gadt01.lc 3:15-3:18
152 Type -> Type
153testdata/language-features/adt/gadt01.lc 3:15-3:20
154 Type | Type
155testdata/language-features/adt/gadt01.lc 3:17-3:18
156 _b | _b
157testdata/language-features/adt/gadt01.lc 3:17-3:20
158 V 1 _b -> Type
159testdata/language-features/adt/gadt01.lc 3:19-3:20
160 Type | Type
161testdata/language-features/adt/gadt01.lc 4:3-4:6
162 forall a . a -> a -> V 2 a | V 2 _c
163testdata/language-features/adt/gadt01.lc 4:3-4:25
164 Type | Type | Type | Type
165testdata/language-features/adt/gadt01.lc 4:10-4:11
166 _b
167testdata/language-features/adt/gadt01.lc 4:10-4:25
168 Type
169testdata/language-features/adt/gadt01.lc 4:15-4:16
170 Type
171testdata/language-features/adt/gadt01.lc 4:15-4:25
172 Type
173testdata/language-features/adt/gadt01.lc 4:20-4:21
174 Nat -> Type -> Type
175testdata/language-features/adt/gadt01.lc 4:20-4:23
176 Type -> Type
177testdata/language-features/adt/gadt01.lc 4:20-4:25
178 Type | Type
179testdata/language-features/adt/gadt01.lc 4:22-4:23
180 _b | _b
181testdata/language-features/adt/gadt01.lc 4:22-4:25
182 V 2 _c -> Type
183testdata/language-features/adt/gadt01.lc 4:24-4:25
184 Type | Type
185testdata/language-features/adt/gadt01.lc 6:6-6:7
186 Type -> String -> Type | Type -> String -> Type | Type | Type | Type
187 -> String -> Type | Type | Type | Type
188testdata/language-features/adt/gadt01.lc 6:6-7:33
189 Type
190testdata/language-features/adt/gadt01.lc 6:11-6:15
191 Type
192testdata/language-features/adt/gadt01.lc 6:19-6:25
193 Type
194testdata/language-features/adt/gadt01.lc 6:19-6:33
195 Type
196testdata/language-features/adt/gadt01.lc 6:29-6:33
197 Type | Type
198testdata/language-features/adt/gadt01.lc 7:3-7:8
199 forall a . a -> forall (b :: String) . M a b | M _c _a
200testdata/language-features/adt/gadt01.lc 7:3-7:33
201 Type | Type | Type | Type
202testdata/language-features/adt/gadt01.lc 7:12-7:13
203 _b
204testdata/language-features/adt/gadt01.lc 7:12-7:33
205 Type
206testdata/language-features/adt/gadt01.lc 7:17-7:33
207 Type
208testdata/language-features/adt/gadt01.lc 7:28-7:29
209 Type -> String -> Type
210testdata/language-features/adt/gadt01.lc 7:28-7:31
211 String -> Type
212testdata/language-features/adt/gadt01.lc 7:28-7:33
213 Type | Type
214testdata/language-features/adt/gadt01.lc 7:30-7:31
215 Type | Type
216testdata/language-features/adt/gadt01.lc 7:30-7:33
217 M _c _a -> Type
218testdata/language-features/adt/gadt01.lc 7:32-7:33
219 _b | String
220testdata/language-features/adt/gadt01.lc 9:6-9:8
221 Type -> String -> Type | Type -> String -> Type | Type | Type
222 -> String -> Type | Type | Type
223testdata/language-features/adt/gadt01.lc 9:6-10:35
224 Type | Type
225testdata/language-features/adt/gadt01.lc 9:15-9:19
226 Type | Type | Type
227testdata/language-features/adt/gadt01.lc 9:24-9:30
228 Type
229testdata/language-features/adt/gadt01.lc 9:24-9:38
230 Type
231testdata/language-features/adt/gadt01.lc 9:34-9:38
232 Type | Type
233testdata/language-features/adt/gadt01.lc 10:3-10:9
234 forall a . a -> forall (b :: String) . M2 a b | M2 _d _a
235testdata/language-features/adt/gadt01.lc 10:3-10:35
236 Type | Type | Type
237testdata/language-features/adt/gadt01.lc 10:13-10:14
238 Type
239testdata/language-features/adt/gadt01.lc 10:13-10:35
240 Type
241testdata/language-features/adt/gadt01.lc 10:18-10:35
242 Type
243testdata/language-features/adt/gadt01.lc 10:29-10:31
244 Type -> String -> Type
245testdata/language-features/adt/gadt01.lc 10:29-10:33
246 String -> Type
247testdata/language-features/adt/gadt01.lc 10:29-10:35
248 Type | Type
249testdata/language-features/adt/gadt01.lc 10:32-10:33
250 Type
251testdata/language-features/adt/gadt01.lc 10:34-10:35
252 _b | String
253testdata/language-features/adt/gadt01.lc 12:6-12:8
254 Type -> String -> Type | Type -> String -> Type | Type | Type
255 -> String -> Type | Type | Type
256testdata/language-features/adt/gadt01.lc 12:6-13:35
257 Type | Type
258testdata/language-features/adt/gadt01.lc 12:15-12:19
259 Type | Type | Type
260testdata/language-features/adt/gadt01.lc 12:24-12:30
261 Type
262testdata/language-features/adt/gadt01.lc 12:24-12:38
263 Type
264testdata/language-features/adt/gadt01.lc 12:34-12:38
265 Type | Type
266testdata/language-features/adt/gadt01.lc 13:3-13:9
267 forall a (b :: String) . a -> M3 a b | M3 _d _b
268testdata/language-features/adt/gadt01.lc 13:3-13:35
269 Type | Type | Type
270testdata/language-features/adt/gadt01.lc 13:13-13:35
271 Type
272testdata/language-features/adt/gadt01.lc 13:24-13:25
273 Type
274testdata/language-features/adt/gadt01.lc 13:24-13:35
275 Type
276testdata/language-features/adt/gadt01.lc 13:29-13:31
277 Type -> String -> Type
278testdata/language-features/adt/gadt01.lc 13:29-13:33
279 String -> Type
280testdata/language-features/adt/gadt01.lc 13:29-13:35
281 Type | Type
282testdata/language-features/adt/gadt01.lc 13:32-13:33
283 Type
284testdata/language-features/adt/gadt01.lc 13:34-13:35
285 _c | String
286testdata/language-features/adt/gadt01.lc 17:1-17:2
287 forall a (b :: String) . M2 a b -> a
288testdata/language-features/adt/gadt01.lc 17:5-17:12
289 forall a
290 . forall (b :: forall (c :: String) -> M2 a c -> Type)
291 -> (forall (d :: a) -> forall (e :: String) . b e ('Value2 d e))
292 -> forall (f :: String) . forall (g :: M2 a f) -> b f g
293testdata/language-features/adt/gadt01.lc 17:5-17:24
294 (forall (a :: _b) -> @String -> _a) -> forall (b :: String) . M2 _b b -> _a
295testdata/language-features/adt/gadt01.lc 17:5-17:37
296 forall (a :: String) . M2 _a a -> _a
297testdata/language-features/adt/gadt01.lc 17:35-17:36
298 _d
299testdata/language-features/adt/gadt01.lc 19:1-19:2
300 forall a (b :: String) . M3 a b -> a
301testdata/language-features/adt/gadt01.lc 19:16-19:17
302 _d
303testdata/language-features/adt/gadt01.lc 21:11-21:12
304 Type -> String -> Type
305testdata/language-features/adt/gadt01.lc 21:11-21:17
306 String -> Type
307testdata/language-features/adt/gadt01.lc 21:11-21:21
308 Type
309testdata/language-features/adt/gadt01.lc 21:13-21:17
310 Type
311testdata/language-features/adt/gadt01.lc 21:18-21:21
312 String
313testdata/language-features/adt/gadt01.lc 22:1-22:7
314 M Bool "m"
315testdata/language-features/adt/gadt01.lc 22:10-22:15
316 forall a . a -> forall (b :: String) . M a b
317testdata/language-features/adt/gadt01.lc 22:10-22:20
318 forall (a :: String) . M Bool a
319testdata/language-features/adt/gadt01.lc 22:16-22:20
320 Bool
321testdata/language-features/adt/gadt01.lc 24:11-24:13
322 Type -> String -> Type
323testdata/language-features/adt/gadt01.lc 24:11-24:18
324 String -> Type
325testdata/language-features/adt/gadt01.lc 24:11-24:22
326 Type
327testdata/language-features/adt/gadt01.lc 24:14-24:18
328 Type
329testdata/language-features/adt/gadt01.lc 24:19-24:22
330 String
331testdata/language-features/adt/gadt01.lc 25:1-25:7
332 M2 Bool "s"
333testdata/language-features/adt/gadt01.lc 25:10-25:16
334 forall a . a -> forall (b :: String) . M2 a b
335testdata/language-features/adt/gadt01.lc 25:10-25:21
336 forall (a :: String) . M2 Bool a
337testdata/language-features/adt/gadt01.lc 25:17-25:21
338 Bool
339testdata/language-features/adt/gadt01.lc 27:11-27:13
340 Type -> String -> Type
341testdata/language-features/adt/gadt01.lc 27:11-27:18
342 String -> Type
343testdata/language-features/adt/gadt01.lc 27:11-27:22
344 Type
345testdata/language-features/adt/gadt01.lc 27:14-27:18
346 Type
347testdata/language-features/adt/gadt01.lc 27:19-27:22
348 String
349testdata/language-features/adt/gadt01.lc 28:1-28:7
350 M3 Bool "t"
351testdata/language-features/adt/gadt01.lc 28:10-28:16
352 forall a (b :: String) . a -> M3 a b
353testdata/language-features/adt/gadt01.lc 28:10-28:21
354 M3 Bool _a
355testdata/language-features/adt/gadt01.lc 28:17-28:21
356 Bool
357testdata/language-features/adt/gadt01.lc 30:1-30:5
358 Bool
359testdata/language-features/adt/gadt01.lc 30:8-30:9
360 forall a (b :: String) . M2 a b -> a
361testdata/language-features/adt/gadt01.lc 30:8-30:16
362 Bool
363testdata/language-features/adt/gadt01.lc 30:8-30:19
364 Bool -> Bool
365testdata/language-features/adt/gadt01.lc 30:8-30:28
366 Bool
367testdata/language-features/adt/gadt01.lc 30:10-30:16
368 M2 Bool "s"
369testdata/language-features/adt/gadt01.lc 30:17-30:19
370 Bool -> Bool -> Bool
371testdata/language-features/adt/gadt01.lc 30:20-30:21
372 forall a (b :: String) . M3 a b -> a
373testdata/language-features/adt/gadt01.lc 30:20-30:28
374 Bool
375testdata/language-features/adt/gadt01.lc 30:22-30:28
376 M3 Bool "t" \ No newline at end of file
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-29 20:14:43 +0000