diff options
author | Péter Diviánszky <divipp@gmail.com> | 2016-05-03 16:34:31 +0200 |
---|---|---|
committer | Péter Diviánszky <divipp@gmail.com> | 2016-05-03 16:34:31 +0200 |
commit | fa47957b930c53d78d2da0bcb948e2fbff11f59d (patch) | |
tree | 25ba37580c8a73e9a8cc7fce31030c8a1a7dbf72 /testdata | |
parent | 9c258737a3a4cfabec6804947ccf64a552db4c27 (diff) |
refactoring
Diffstat (limited to 'testdata')
-rw-r--r-- | testdata/Builtins.out | 724 | ||||
-rw-r--r-- | testdata/Internals.out | 160 | ||||
-rw-r--r-- | testdata/Material.out | 57 | ||||
-rw-r--r-- | testdata/Prelude.out | 264 | ||||
-rw-r--r-- | testdata/complex.out | 126 | ||||
-rw-r--r-- | testdata/language-features/basic-values/typesig01.out | 6 | ||||
-rw-r--r-- | testdata/language-features/basic-values/typesig03.out | 10 | ||||
-rw-r--r-- | testdata/language-features/basic-values/typesig04.out | 10 | ||||
-rw-r--r-- | testdata/language-features/basic-values/typesig05.out | 6 | ||||
-rw-r--r-- | testdata/language-features/basic-values/typesig07.out | 18 | ||||
-rw-r--r-- | testdata/language-features/basic-values/typesyn02.out | 5 | ||||
-rw-r--r-- | testdata/language-features/module/import05.out | 3 | ||||
-rw-r--r-- | testdata/language-features/module/import08.out | 9 | ||||
-rw-r--r-- | testdata/language-features/module/import09.out | 5 | ||||
-rw-r--r-- | testdata/performance/Material.out | 57 | ||||
-rw-r--r-- | testdata/traceTest.out | 3 | ||||
-rw-r--r-- | testdata/typeclass.out | 28 | ||||
-rw-r--r-- | testdata/zip01.out | 16 |
18 files changed, 758 insertions, 749 deletions
diff --git a/testdata/Builtins.out b/testdata/Builtins.out index 469a2a39..ffe2badf 100644 --- a/testdata/Builtins.out +++ b/testdata/Builtins.out | |||
@@ -4,26 +4,27 @@ data VecS (_ :: Type) :: Nat -> Type where | |||
4 | V2 :: forall a . a -> a -> VecS a (fromInt 2) | 4 | V2 :: forall a . a -> a -> VecS a (fromInt 2) |
5 | V3 :: forall b . b -> b -> b -> VecS b (fromInt 3) | 5 | V3 :: forall b . b -> b -> b -> VecS b (fromInt 3) |
6 | V4 :: forall c . c -> c -> c -> c -> VecS c (fromInt 4) | 6 | V4 :: forall c . c -> c -> c -> c -> VecS c (fromInt 4) |
7 | mapVec :: forall (a :: _) (b :: _) (c :: _) . (a -> b) -> VecS a c -> VecS b c | ||
7 | mapVec | 8 | mapVec |
8 | = (\(a :: _) (b :: _) -> case'VecS | 9 | = \(a :: _) (b :: _) -> case'VecS |
9 | (\_ _ -> _) | 10 | (\_ _ -> _) |
10 | (\(c :: _) (d :: _) -> _rhs (V2 (a c) (a d))) | 11 | (\(c :: _) (d :: _) -> _rhs (V2 (a c) (a d))) |
11 | (\(e :: _) (f :: _) (g :: _) -> _rhs (V3 (a e) (a f) (a g))) | 12 | (\(e :: _) (f :: _) (g :: _) -> _rhs (V3 (a e) (a f) (a g))) |
12 | (\(h :: _) (i :: _) (j :: _) (k :: _) -> _rhs (V4 (a h) (a i) (a j) (a k))) | 13 | (\(h :: _) (i :: _) (j :: _) (k :: _) -> _rhs (V4 (a h) (a i) (a j) (a k))) |
13 | b) | 14 | b |
14 | :: forall (l :: _) (m :: _) (n :: _) . (l -> m) -> VecS l n -> VecS m n | 15 | 'Vec :: Nat -> Type -> Type |
15 | 'Vec = (\(a :: _) (b :: _) -> _rhs ('VecS b a)) :: Nat -> Type -> Type | 16 | 'Vec = \(a :: _) (b :: _) -> _rhs ('VecS b a) |
17 | 'VecScalar :: Nat -> Type -> Type | ||
16 | 'VecScalar | 18 | 'VecScalar |
17 | = (\(a :: _) (b :: _) -> case'Nat | 19 | = \(a :: _) (b :: _) -> case'Nat |
20 | (\_ -> _) | ||
21 | undefined | ||
22 | (\(c :: _) -> case'Nat | ||
18 | (\_ -> _) | 23 | (\_ -> _) |
19 | undefined | 24 | (_rhs b) |
20 | (\(c :: _) -> case'Nat | 25 | (\(d :: _) -> _rhs ('Vec (Succ (Succ d)) b)) |
21 | (\_ -> _) | 26 | c) |
22 | (_rhs b) | 27 | a |
23 | (\(d :: _) -> _rhs ('Vec (Succ (Succ d)) b)) | ||
24 | c) | ||
25 | a) | ||
26 | :: Nat -> Type -> Type | ||
27 | data Mat :: Nat -> Nat -> Type -> Type where | 28 | data Mat :: Nat -> Nat -> Type -> Type where |
28 | M22F | 29 | M22F |
29 | :: Vec (fromInt 2) Float | 30 | :: Vec (fromInt 2) Float |
@@ -61,316 +62,352 @@ data Mat :: Nat -> Nat -> Type -> Type where | |||
61 | -> Vec (fromInt 4) Float | 62 | -> Vec (fromInt 4) Float |
62 | -> Vec (fromInt 4) Float | 63 | -> Vec (fromInt 4) Float |
63 | -> Vec (fromInt 4) Float -> Mat (fromInt 4) (fromInt 4) Float | 64 | -> Vec (fromInt 4) Float -> Mat (fromInt 4) (fromInt 4) Float |
65 | 'MatVecScalarElem :: Type -> Type | ||
64 | 'MatVecScalarElem | 66 | 'MatVecScalarElem |
65 | = (\(a :: _) -> match'Float | 67 | = \(a :: _) -> match'Float |
68 | (\_ -> _) | ||
69 | (_rhs 'Float) | ||
70 | a | ||
71 | (match'Bool | ||
66 | (\_ -> _) | 72 | (\_ -> _) |
67 | (_rhs 'Float) | 73 | (_rhs 'Bool) |
68 | a | 74 | a |
69 | (match'Bool | 75 | (match'Int |
70 | (\_ -> _) | 76 | (\_ -> _) |
71 | (_rhs 'Bool) | 77 | (_rhs 'Int) |
72 | a | 78 | a |
73 | (match'Int | 79 | (match'VecS |
74 | (\_ -> _) | 80 | (\_ -> _) |
75 | (_rhs 'Int) | 81 | (\(b :: _) _ -> _rhs b) |
76 | a | 82 | a |
77 | (match'VecS | 83 | (match'Mat (\_ -> _) (\_ _ (c :: _) -> _rhs c) a undefined)))) |
78 | (\_ -> _) | 84 | 'Signed :: Type -> Type |
79 | (\(b :: _) _ -> _rhs b) | ||
80 | a | ||
81 | (match'Mat (\_ -> _) (\_ _ (c :: _) -> _rhs c) a undefined))))) | ||
82 | :: Type -> Type | ||
83 | 'Signed | 85 | 'Signed |
84 | = (\(a :: _) -> match'Int | 86 | = \(a :: _) -> match'Int |
87 | (\_ -> _) | ||
88 | (_rhs 'Unit) | ||
89 | a | ||
90 | (match'Float | ||
85 | (\_ -> _) | 91 | (\_ -> _) |
86 | (_rhs 'Unit) | 92 | (_rhs 'Unit) |
87 | a | 93 | a |
88 | (match'Float | 94 | (_rhs ('Empty "no instance of 'Signed on ???"))) |
89 | (\_ -> _) | 95 | 'Component :: Type -> Type |
90 | (_rhs 'Unit) | ||
91 | a | ||
92 | (_rhs ('Empty "no instance of 'Signed on ???")))) | ||
93 | :: Type -> Type | ||
94 | 'Component | 96 | 'Component |
95 | = (\(a :: _) -> match'Int | 97 | = \(a :: _) -> match'Int |
98 | (\_ -> _) | ||
99 | (_rhs 'Unit) | ||
100 | a | ||
101 | (match'Word | ||
96 | (\_ -> _) | 102 | (\_ -> _) |
97 | (_rhs 'Unit) | 103 | (_rhs 'Unit) |
98 | a | 104 | a |
99 | (match'Word | 105 | (match'Float |
100 | (\_ -> _) | 106 | (\_ -> _) |
101 | (_rhs 'Unit) | 107 | (_rhs 'Unit) |
102 | a | 108 | a |
103 | (match'Float | 109 | (match'VecS |
104 | (\_ -> _) | 110 | (\_ -> _) |
105 | (_rhs 'Unit) | 111 | (\(b :: _) (c :: _) -> match'Float |
106 | a | ||
107 | (match'VecS | ||
108 | (\_ -> _) | 112 | (\_ -> _) |
109 | (\(b :: _) (c :: _) -> match'Float | 113 | (case'Nat |
110 | (\_ -> _) | 114 | (\_ -> _) |
111 | (case'Nat | 115 | (_rhs ('Empty "no instance of 'Component on ???")) |
116 | (\(d :: _) -> case'Nat | ||
112 | (\_ -> _) | 117 | (\_ -> _) |
113 | (_rhs ('Empty "no instance of 'Component on ???")) | 118 | (_rhs ('Empty "no instance of 'Component on ???")) |
114 | (\(d :: _) -> case'Nat | 119 | (\(e :: _) -> case'Nat |
115 | (\_ -> _) | 120 | (\_ -> _) |
116 | (_rhs ('Empty "no instance of 'Component on ???")) | 121 | (_rhs 'Unit) |
117 | (\(e :: _) -> case'Nat | 122 | (\(f :: _) -> case'Nat |
118 | (\_ -> _) | 123 | (\_ -> _) |
119 | (_rhs 'Unit) | 124 | (_rhs 'Unit) |
120 | (\(f :: _) -> case'Nat | 125 | (\(g :: _) -> case'Nat |
121 | (\_ -> _) | 126 | (\_ -> _) |
122 | (_rhs 'Unit) | 127 | (_rhs 'Unit) |
123 | (\(g :: _) -> case'Nat | 128 | (\_ -> _rhs ('Empty "no instance of 'Component on ???")) |
124 | (\_ -> _) | 129 | g) |
125 | (_rhs 'Unit) | 130 | f) |
126 | (\_ -> _rhs ('Empty "no instance of 'Component on ???")) | 131 | e) |
127 | g) | 132 | d) |
128 | f) | 133 | c) |
129 | e) | 134 | b |
130 | d) | 135 | (match'Bool |
131 | c) | 136 | (\_ -> _) |
132 | b | 137 | (case'Nat |
133 | (match'Bool | ||
134 | (\_ -> _) | 138 | (\_ -> _) |
135 | (case'Nat | 139 | (_rhs ('Empty "no instance of 'Component on ???")) |
140 | (\(h :: _) -> case'Nat | ||
136 | (\_ -> _) | 141 | (\_ -> _) |
137 | (_rhs ('Empty "no instance of 'Component on ???")) | 142 | (_rhs ('Empty "no instance of 'Component on ???")) |
138 | (\(h :: _) -> case'Nat | 143 | (\(i :: _) -> case'Nat |
139 | (\_ -> _) | 144 | (\_ -> _) |
140 | (_rhs ('Empty "no instance of 'Component on ???")) | 145 | (_rhs 'Unit) |
141 | (\(i :: _) -> case'Nat | 146 | (\(j :: _) -> case'Nat |
142 | (\_ -> _) | 147 | (\_ -> _) |
143 | (_rhs 'Unit) | 148 | (_rhs 'Unit) |
144 | (\(j :: _) -> case'Nat | 149 | (\(k :: _) -> case'Nat |
145 | (\_ -> _) | 150 | (\_ -> _) |
146 | (_rhs 'Unit) | 151 | (_rhs 'Unit) |
147 | (\(k :: _) -> case'Nat | 152 | (\_ -> _rhs ('Empty "no instance of 'Component on ???")) |
148 | (\_ -> _) | 153 | k) |
149 | (_rhs 'Unit) | 154 | j) |
150 | (\_ -> _rhs ('Empty "no instance of 'Component on ???")) | 155 | i) |
151 | k) | 156 | h) |
152 | j) | 157 | c) |
153 | i) | 158 | b |
154 | h) | 159 | (_rhs ('Empty "no instance of 'Component on ???")))) |
155 | c) | 160 | a |
156 | b | 161 | (match'Bool |
157 | (_rhs ('Empty "no instance of 'Component on ???")))) | 162 | (\_ -> _) |
163 | (_rhs 'Unit) | ||
158 | a | 164 | a |
159 | (match'Bool | 165 | (_rhs ('Empty "no instance of 'Component on ???")))))) |
160 | (\_ -> _) | 166 | zero :: forall a . Component a => a |
161 | (_rhs 'Unit) | ||
162 | a | ||
163 | (_rhs ('Empty "no instance of 'Component on ???"))))))) | ||
164 | :: Type -> Type | ||
165 | zero | 167 | zero |
166 | = (\ @a @_ -> match'Int | 168 | = \ @a @_ -> match'Int |
169 | (\_ -> _) | ||
170 | (_rhs \(b := _rhs (fromInt 0 :: Int)) -> b) | ||
171 | a | ||
172 | (match'Word | ||
167 | (\_ -> _) | 173 | (\_ -> _) |
168 | (_rhs \(b := _rhs (fromInt 0 :: Int)) -> b) | 174 | (_rhs \(c := _rhs (fromInt 0 :: Word)) -> c) |
169 | a | 175 | a |
170 | (match'Word | 176 | (match'Float |
171 | (\_ -> _) | 177 | (\_ -> _) |
172 | (_rhs \(c := _rhs (fromInt 0 :: Word)) -> c) | 178 | (_rhs \(d := _rhs 0.0) -> d) |
173 | a | 179 | a |
174 | (match'Float | 180 | (match'VecS |
175 | (\_ -> _) | 181 | (\_ -> _) |
176 | (_rhs \(d := _rhs 0.0) -> d) | 182 | (\(e :: _) (f :: _) -> match'Float |
177 | a | ||
178 | (match'VecS | ||
179 | (\_ -> _) | 183 | (\_ -> _) |
180 | (\(e :: _) (f :: _) -> match'Float | 184 | (case'Nat |
181 | (\_ -> _) | 185 | (\_ -> _) |
182 | (case'Nat | 186 | (_rhs undefined) |
187 | (\(g :: _) -> case'Nat | ||
183 | (\_ -> _) | 188 | (\_ -> _) |
184 | (_rhs undefined) | 189 | (_rhs undefined) |
185 | (\(g :: _) -> case'Nat | 190 | (\(h :: _) -> case'Nat |
186 | (\_ -> _) | 191 | (\_ -> _) |
187 | (_rhs undefined) | 192 | (_rhs \(i := _rhs (V2 0.0 0.0)) -> i) |
188 | (\(h :: _) -> case'Nat | 193 | (\(j :: _) -> case'Nat |
189 | (\_ -> _) | 194 | (\_ -> _) |
190 | (_rhs \(i := _rhs (V2 0.0 0.0)) -> i) | 195 | (_rhs \(k := _rhs (V3 0.0 0.0 0.0)) -> k) |
191 | (\(j :: _) -> case'Nat | 196 | (\(l :: _) -> case'Nat |
192 | (\_ -> _) | 197 | (\_ -> _) |
193 | (_rhs \(k := _rhs (V3 0.0 0.0 0.0)) -> k) | 198 | (_rhs \(m := _rhs (V4 0.0 0.0 0.0 0.0)) -> m) |
194 | (\(l :: _) -> case'Nat | 199 | (\_ -> _rhs undefined) |
195 | (\_ -> _) | 200 | l) |
196 | (_rhs \(m := _rhs (V4 0.0 0.0 0.0 0.0)) -> m) | 201 | j) |
197 | (\_ -> _rhs undefined) | 202 | h) |
198 | l) | 203 | g) |
199 | j) | 204 | f) |
200 | h) | 205 | e |
201 | g) | 206 | (match'Bool |
202 | f) | 207 | (\_ -> _) |
203 | e | 208 | (case'Nat |
204 | (match'Bool | ||
205 | (\_ -> _) | 209 | (\_ -> _) |
206 | (case'Nat | 210 | (_rhs undefined) |
211 | (\(n :: _) -> case'Nat | ||
207 | (\_ -> _) | 212 | (\_ -> _) |
208 | (_rhs undefined) | 213 | (_rhs undefined) |
209 | (\(n :: _) -> case'Nat | 214 | (\(o :: _) -> case'Nat |
210 | (\_ -> _) | 215 | (\_ -> _) |
211 | (_rhs undefined) | 216 | (_rhs \(p := _rhs (V2 False False)) -> p) |
212 | (\(o :: _) -> case'Nat | 217 | (\(q :: _) -> case'Nat |
213 | (\_ -> _) | 218 | (\_ -> _) |
214 | (_rhs \(p := _rhs (V2 False False)) -> p) | 219 | (_rhs \(r := _rhs (V3 False False False)) -> r) |
215 | (\(q :: _) -> case'Nat | 220 | (\(s :: _) -> case'Nat |
216 | (\_ -> _) | 221 | (\_ -> _) |
217 | (_rhs \(r := _rhs (V3 False False False)) -> r) | 222 | (_rhs \(t := _rhs (V4 False False False False)) -> t) |
218 | (\(s :: _) -> case'Nat | 223 | (\_ -> _rhs undefined) |
219 | (\_ -> _) | 224 | s) |
220 | (_rhs \(t := _rhs (V4 False False False False)) -> t) | 225 | q) |
221 | (\_ -> _rhs undefined) | 226 | o) |
222 | s) | 227 | n) |
223 | q) | 228 | f) |
224 | o) | 229 | e |
225 | n) | 230 | (_rhs undefined))) |
226 | f) | 231 | a |
227 | e | 232 | (match'Bool (\_ -> _) (_rhs \(u := _rhs False) -> u) a (_rhs undefined))))) |
228 | (_rhs undefined))) | 233 | one :: forall a . Component a => a |
229 | a | ||
230 | (match'Bool (\_ -> _) (_rhs \(u := _rhs False) -> u) a (_rhs undefined)))))) | ||
231 | :: forall v . Component v => v | ||
232 | one | 234 | one |
233 | = (\ @a @_ -> match'Int | 235 | = \ @a @_ -> match'Int |
236 | (\_ -> _) | ||
237 | (_rhs \(b := _rhs (fromInt 1 :: Int)) -> b) | ||
238 | a | ||
239 | (match'Word | ||
234 | (\_ -> _) | 240 | (\_ -> _) |
235 | (_rhs \(b := _rhs (fromInt 1 :: Int)) -> b) | 241 | (_rhs \(c := _rhs (fromInt 1 :: Word)) -> c) |
236 | a | 242 | a |
237 | (match'Word | 243 | (match'Float |
238 | (\_ -> _) | 244 | (\_ -> _) |
239 | (_rhs \(c := _rhs (fromInt 1 :: Word)) -> c) | 245 | (_rhs \(d := _rhs 1.0) -> d) |
240 | a | 246 | a |
241 | (match'Float | 247 | (match'VecS |
242 | (\_ -> _) | 248 | (\_ -> _) |
243 | (_rhs \(d := _rhs 1.0) -> d) | 249 | (\(e :: _) (f :: _) -> match'Float |
244 | a | ||
245 | (match'VecS | ||
246 | (\_ -> _) | 250 | (\_ -> _) |
247 | (\(e :: _) (f :: _) -> match'Float | 251 | (case'Nat |
248 | (\_ -> _) | 252 | (\_ -> _) |
249 | (case'Nat | 253 | (_rhs undefined) |
254 | (\(g :: _) -> case'Nat | ||
250 | (\_ -> _) | 255 | (\_ -> _) |
251 | (_rhs undefined) | 256 | (_rhs undefined) |
252 | (\(g :: _) -> case'Nat | 257 | (\(h :: _) -> case'Nat |
253 | (\_ -> _) | 258 | (\_ -> _) |
254 | (_rhs undefined) | 259 | (_rhs \(i := _rhs (V2 1.0 1.0)) -> i) |
255 | (\(h :: _) -> case'Nat | 260 | (\(j :: _) -> case'Nat |
256 | (\_ -> _) | 261 | (\_ -> _) |
257 | (_rhs \(i := _rhs (V2 1.0 1.0)) -> i) | 262 | (_rhs \(k := _rhs (V3 1.0 1.0 1.0)) -> k) |
258 | (\(j :: _) -> case'Nat | 263 | (\(l :: _) -> case'Nat |
259 | (\_ -> _) | 264 | (\_ -> _) |
260 | (_rhs \(k := _rhs (V3 1.0 1.0 1.0)) -> k) | 265 | (_rhs \(m := _rhs (V4 1.0 1.0 1.0 1.0)) -> m) |
261 | (\(l :: _) -> case'Nat | 266 | (\_ -> _rhs undefined) |
262 | (\_ -> _) | 267 | l) |
263 | (_rhs \(m := _rhs (V4 1.0 1.0 1.0 1.0)) -> m) | 268 | j) |
264 | (\_ -> _rhs undefined) | 269 | h) |
265 | l) | 270 | g) |
266 | j) | 271 | f) |
267 | h) | 272 | e |
268 | g) | 273 | (match'Bool |
269 | f) | 274 | (\_ -> _) |
270 | e | 275 | (case'Nat |
271 | (match'Bool | ||
272 | (\_ -> _) | 276 | (\_ -> _) |
273 | (case'Nat | 277 | (_rhs undefined) |
278 | (\(n :: _) -> case'Nat | ||
274 | (\_ -> _) | 279 | (\_ -> _) |
275 | (_rhs undefined) | 280 | (_rhs undefined) |
276 | (\(n :: _) -> case'Nat | 281 | (\(o :: _) -> case'Nat |
277 | (\_ -> _) | 282 | (\_ -> _) |
278 | (_rhs undefined) | 283 | (_rhs \(p := _rhs (V2 True True)) -> p) |
279 | (\(o :: _) -> case'Nat | 284 | (\(q :: _) -> case'Nat |
280 | (\_ -> _) | 285 | (\_ -> _) |
281 | (_rhs \(p := _rhs (V2 True True)) -> p) | 286 | (_rhs \(r := _rhs (V3 True True True)) -> r) |
282 | (\(q :: _) -> case'Nat | 287 | (\(s :: _) -> case'Nat |
283 | (\_ -> _) | 288 | (\_ -> _) |
284 | (_rhs \(r := _rhs (V3 True True True)) -> r) | 289 | (_rhs \(t := _rhs (V4 True True True True)) -> t) |
285 | (\(s :: _) -> case'Nat | 290 | (\_ -> _rhs undefined) |
286 | (\_ -> _) | 291 | s) |
287 | (_rhs \(t := _rhs (V4 True True True True)) -> t) | 292 | q) |
288 | (\_ -> _rhs undefined) | 293 | o) |
289 | s) | 294 | n) |
290 | q) | 295 | f) |
291 | o) | 296 | e |
292 | n) | 297 | (_rhs undefined))) |
293 | f) | 298 | a |
294 | e | 299 | (match'Bool (\_ -> _) (_rhs \(u := _rhs True) -> u) a (_rhs undefined))))) |
295 | (_rhs undefined))) | 300 | 'Integral :: Type -> Type |
296 | a | ||
297 | (match'Bool (\_ -> _) (_rhs \(u := _rhs True) -> u) a (_rhs undefined)))))) | ||
298 | :: forall v . Component v => v | ||
299 | 'Integral | 301 | 'Integral |
300 | = (\(a :: _) -> match'Int | 302 | = \(a :: _) -> match'Int |
303 | (\_ -> _) | ||
304 | (_rhs 'Unit) | ||
305 | a | ||
306 | (match'Word | ||
301 | (\_ -> _) | 307 | (\_ -> _) |
302 | (_rhs 'Unit) | 308 | (_rhs 'Unit) |
303 | a | 309 | a |
304 | (match'Word | 310 | (_rhs ('Empty "no instance of 'Integral on ???"))) |
305 | (\_ -> _) | 311 | 'Floating :: Type -> Type |
306 | (_rhs 'Unit) | ||
307 | a | ||
308 | (_rhs ('Empty "no instance of 'Integral on ???")))) | ||
309 | :: Type -> Type | ||
310 | 'Floating | 312 | 'Floating |
311 | = (\(a :: _) -> match'Float | 313 | = \(a :: _) -> match'Float |
314 | (\_ -> _) | ||
315 | (_rhs 'Unit) | ||
316 | a | ||
317 | (match'VecS | ||
312 | (\_ -> _) | 318 | (\_ -> _) |
313 | (_rhs 'Unit) | 319 | (\(b :: _) (c :: _) -> match'Float |
314 | a | ||
315 | (match'VecS | ||
316 | (\_ -> _) | 320 | (\_ -> _) |
317 | (\(b :: _) (c :: _) -> match'Float | 321 | (case'Nat |
318 | (\_ -> _) | 322 | (\_ -> _) |
319 | (case'Nat | 323 | (_rhs ('Empty "no instance of 'Floating on ???")) |
324 | (\(d :: _) -> case'Nat | ||
320 | (\_ -> _) | 325 | (\_ -> _) |
321 | (_rhs ('Empty "no instance of 'Floating on ???")) | 326 | (_rhs ('Empty "no instance of 'Floating on ???")) |
322 | (\(d :: _) -> case'Nat | 327 | (\(e :: _) -> case'Nat |
323 | (\_ -> _) | 328 | (\_ -> _) |
324 | (_rhs ('Empty "no instance of 'Floating on ???")) | 329 | (_rhs 'Unit) |
325 | (\(e :: _) -> case'Nat | 330 | (\(f :: _) -> case'Nat |
326 | (\_ -> _) | 331 | (\_ -> _) |
327 | (_rhs 'Unit) | 332 | (_rhs 'Unit) |
328 | (\(f :: _) -> case'Nat | 333 | (\(g :: _) -> case'Nat |
329 | (\_ -> _) | 334 | (\_ -> _) |
330 | (_rhs 'Unit) | 335 | (_rhs 'Unit) |
331 | (\(g :: _) -> case'Nat | 336 | (\_ -> _rhs ('Empty "no instance of 'Floating on ???")) |
332 | (\_ -> _) | 337 | g) |
333 | (_rhs 'Unit) | 338 | f) |
334 | (\_ -> _rhs ('Empty "no instance of 'Floating on ???")) | 339 | e) |
335 | g) | 340 | d) |
336 | f) | 341 | c) |
337 | e) | 342 | b |
338 | d) | 343 | (_rhs ('Empty "no instance of 'Floating on ???"))) |
339 | c) | 344 | a |
340 | b | 345 | (match'Mat |
341 | (_rhs ('Empty "no instance of 'Floating on ???"))) | 346 | (\_ -> _) |
342 | a | 347 | (\(h :: _) (i :: _) (j :: _) -> case'Nat |
343 | (match'Mat | ||
344 | (\_ -> _) | 348 | (\_ -> _) |
345 | (\(h :: _) (i :: _) (j :: _) -> case'Nat | 349 | (_rhs ('Empty "no instance of 'Floating on ???")) |
350 | (\(k :: _) -> case'Nat | ||
346 | (\_ -> _) | 351 | (\_ -> _) |
347 | (_rhs ('Empty "no instance of 'Floating on ???")) | 352 | (_rhs ('Empty "no instance of 'Floating on ???")) |
348 | (\(k :: _) -> case'Nat | 353 | (\(l :: _) -> case'Nat |
349 | (\_ -> _) | 354 | (\_ -> _) |
350 | (_rhs ('Empty "no instance of 'Floating on ???")) | 355 | (case'Nat |
351 | (\(l :: _) -> case'Nat | 356 | (\_ -> _) |
357 | (_rhs ('Empty "no instance of 'Floating on ???")) | ||
358 | (\(m :: _) -> case'Nat | ||
359 | (\_ -> _) | ||
360 | (_rhs ('Empty "no instance of 'Floating on ???")) | ||
361 | (\(n :: _) -> case'Nat | ||
362 | (\_ -> _) | ||
363 | (match'Float | ||
364 | (\_ -> _) | ||
365 | (_rhs 'Unit) | ||
366 | j | ||
367 | (_rhs ('Empty "no instance of 'Floating on ???"))) | ||
368 | (\(o :: _) -> case'Nat | ||
369 | (\_ -> _) | ||
370 | (match'Float | ||
371 | (\_ -> _) | ||
372 | (_rhs 'Unit) | ||
373 | j | ||
374 | (_rhs ('Empty "no instance of 'Floating on ???"))) | ||
375 | (\(p :: _) -> case'Nat | ||
376 | (\_ -> _) | ||
377 | (match'Float | ||
378 | (\_ -> _) | ||
379 | (_rhs 'Unit) | ||
380 | j | ||
381 | (_rhs ('Empty "no instance of 'Floating on ???"))) | ||
382 | (\_ -> _rhs ('Empty "no instance of 'Floating on ???")) | ||
383 | p) | ||
384 | o) | ||
385 | n) | ||
386 | m) | ||
387 | i) | ||
388 | (\(q :: _) -> case'Nat | ||
352 | (\_ -> _) | 389 | (\_ -> _) |
353 | (case'Nat | 390 | (case'Nat |
354 | (\_ -> _) | 391 | (\_ -> _) |
355 | (_rhs ('Empty "no instance of 'Floating on ???")) | 392 | (_rhs ('Empty "no instance of 'Floating on ???")) |
356 | (\(m :: _) -> case'Nat | 393 | (\(r :: _) -> case'Nat |
357 | (\_ -> _) | 394 | (\_ -> _) |
358 | (_rhs ('Empty "no instance of 'Floating on ???")) | 395 | (_rhs ('Empty "no instance of 'Floating on ???")) |
359 | (\(n :: _) -> case'Nat | 396 | (\(s :: _) -> case'Nat |
360 | (\_ -> _) | 397 | (\_ -> _) |
361 | (match'Float | 398 | (match'Float |
362 | (\_ -> _) | 399 | (\_ -> _) |
363 | (_rhs 'Unit) | 400 | (_rhs 'Unit) |
364 | j | 401 | j |
365 | (_rhs ('Empty "no instance of 'Floating on ???"))) | 402 | (_rhs ('Empty "no instance of 'Floating on ???"))) |
366 | (\(o :: _) -> case'Nat | 403 | (\(t :: _) -> case'Nat |
367 | (\_ -> _) | 404 | (\_ -> _) |
368 | (match'Float | 405 | (match'Float |
369 | (\_ -> _) | 406 | (\_ -> _) |
370 | (_rhs 'Unit) | 407 | (_rhs 'Unit) |
371 | j | 408 | j |
372 | (_rhs ('Empty "no instance of 'Floating on ???"))) | 409 | (_rhs ('Empty "no instance of 'Floating on ???"))) |
373 | (\(p :: _) -> case'Nat | 410 | (\(u :: _) -> case'Nat |
374 | (\_ -> _) | 411 | (\_ -> _) |
375 | (match'Float | 412 | (match'Float |
376 | (\_ -> _) | 413 | (\_ -> _) |
@@ -378,34 +415,34 @@ one | |||
378 | j | 415 | j |
379 | (_rhs ('Empty "no instance of 'Floating on ???"))) | 416 | (_rhs ('Empty "no instance of 'Floating on ???"))) |
380 | (\_ -> _rhs ('Empty "no instance of 'Floating on ???")) | 417 | (\_ -> _rhs ('Empty "no instance of 'Floating on ???")) |
381 | p) | 418 | u) |
382 | o) | 419 | t) |
383 | n) | 420 | s) |
384 | m) | 421 | r) |
385 | i) | 422 | i) |
386 | (\(q :: _) -> case'Nat | 423 | (\(v :: _) -> case'Nat |
387 | (\_ -> _) | 424 | (\_ -> _) |
388 | (case'Nat | 425 | (case'Nat |
389 | (\_ -> _) | 426 | (\_ -> _) |
390 | (_rhs ('Empty "no instance of 'Floating on ???")) | 427 | (_rhs ('Empty "no instance of 'Floating on ???")) |
391 | (\(r :: _) -> case'Nat | 428 | (\(w :: _) -> case'Nat |
392 | (\_ -> _) | 429 | (\_ -> _) |
393 | (_rhs ('Empty "no instance of 'Floating on ???")) | 430 | (_rhs ('Empty "no instance of 'Floating on ???")) |
394 | (\(s :: _) -> case'Nat | 431 | (\(x :: _) -> case'Nat |
395 | (\_ -> _) | 432 | (\_ -> _) |
396 | (match'Float | 433 | (match'Float |
397 | (\_ -> _) | 434 | (\_ -> _) |
398 | (_rhs 'Unit) | 435 | (_rhs 'Unit) |
399 | j | 436 | j |
400 | (_rhs ('Empty "no instance of 'Floating on ???"))) | 437 | (_rhs ('Empty "no instance of 'Floating on ???"))) |
401 | (\(t :: _) -> case'Nat | 438 | (\(y :: _) -> case'Nat |
402 | (\_ -> _) | 439 | (\_ -> _) |
403 | (match'Float | 440 | (match'Float |
404 | (\_ -> _) | 441 | (\_ -> _) |
405 | (_rhs 'Unit) | 442 | (_rhs 'Unit) |
406 | j | 443 | j |
407 | (_rhs ('Empty "no instance of 'Floating on ???"))) | 444 | (_rhs ('Empty "no instance of 'Floating on ???"))) |
408 | (\(u :: _) -> case'Nat | 445 | (\(z :: _) -> case'Nat |
409 | (\_ -> _) | 446 | (\_ -> _) |
410 | (match'Float | 447 | (match'Float |
411 | (\_ -> _) | 448 | (\_ -> _) |
@@ -413,55 +450,19 @@ one | |||
413 | j | 450 | j |
414 | (_rhs ('Empty "no instance of 'Floating on ???"))) | 451 | (_rhs ('Empty "no instance of 'Floating on ???"))) |
415 | (\_ -> _rhs ('Empty "no instance of 'Floating on ???")) | 452 | (\_ -> _rhs ('Empty "no instance of 'Floating on ???")) |
416 | u) | 453 | z) |
417 | t) | 454 | y) |
418 | s) | 455 | x) |
419 | r) | 456 | w) |
420 | i) | 457 | i) |
421 | (\(v :: _) -> case'Nat | 458 | (\_ -> _rhs ('Empty "no instance of 'Floating on ???")) |
422 | (\_ -> _) | 459 | v) |
423 | (case'Nat | 460 | q) |
424 | (\_ -> _) | 461 | l) |
425 | (_rhs ('Empty "no instance of 'Floating on ???")) | 462 | k) |
426 | (\(w :: _) -> case'Nat | 463 | h) |
427 | (\_ -> _) | 464 | a |
428 | (_rhs ('Empty "no instance of 'Floating on ???")) | 465 | (_rhs ('Empty "no instance of 'Floating on ???")))) |
429 | (\(x :: _) -> case'Nat | ||
430 | (\_ -> _) | ||
431 | (match'Float | ||
432 | (\_ -> _) | ||
433 | (_rhs 'Unit) | ||
434 | j | ||
435 | (_rhs ('Empty "no instance of 'Floating on ???"))) | ||
436 | (\(y :: _) -> case'Nat | ||
437 | (\_ -> _) | ||
438 | (match'Float | ||
439 | (\_ -> _) | ||
440 | (_rhs 'Unit) | ||
441 | j | ||
442 | (_rhs ('Empty "no instance of 'Floating on ???"))) | ||
443 | (\(z :: _) -> case'Nat | ||
444 | (\_ -> _) | ||
445 | (match'Float | ||
446 | (\_ -> _) | ||
447 | (_rhs 'Unit) | ||
448 | j | ||
449 | (_rhs ('Empty "no instance of 'Floating on ???"))) | ||
450 | (\_ -> _rhs ('Empty "no instance of 'Floating on ???")) | ||
451 | z) | ||
452 | y) | ||
453 | x) | ||
454 | w) | ||
455 | i) | ||
456 | (\_ -> _rhs ('Empty "no instance of 'Floating on ???")) | ||
457 | v) | ||
458 | q) | ||
459 | l) | ||
460 | k) | ||
461 | h) | ||
462 | a | ||
463 | (_rhs ('Empty "no instance of 'Floating on ???"))))) | ||
464 | :: Type -> Type | ||
465 | PrimAdd :: forall (a :: _) . Num (MatVecScalarElem a) => a -> a -> a | 466 | PrimAdd :: forall (a :: _) . Num (MatVecScalarElem a) => a -> a -> a |
466 | PrimSub :: forall (a :: _) . Num (MatVecScalarElem a) => a -> a -> a | 467 | PrimSub :: forall (a :: _) . Num (MatVecScalarElem a) => a -> a -> a |
467 | PrimMul :: forall (a :: _) . Num (MatVecScalarElem a) => a -> a -> a | 468 | PrimMul :: forall (a :: _) . Num (MatVecScalarElem a) => a -> a -> a |
@@ -665,9 +666,8 @@ map | |||
665 | (_rhs []) | 666 | (_rhs []) |
666 | (\(c :: _) (d :: _) -> _rhs (a c : map a d)) | 667 | (\(c :: _) (d :: _) -> _rhs (a c : map a d)) |
667 | b | 668 | b |
668 | concatMap | 669 | concatMap :: forall (a :: _) (b :: _) . (a -> [b]) -> [a] -> [b] |
669 | = (\(a :: _) (b :: _) -> _rhs (concat (map a b))) | 670 | concatMap = \(a :: _) (b :: _) -> _rhs (concat (map a b)) |
670 | :: forall (c :: _) (d :: _) . (c -> [d]) -> [c] -> [d] | ||
671 | len | 671 | len |
672 | = \(a :: _) -> case'List | 672 | = \(a :: _) -> case'List |
673 | (\_ -> _) | 673 | (\_ -> _) |
@@ -694,12 +694,11 @@ mapPrimitive | |||
694 | . (a -> b) -> Primitive a c -> Primitive b c | 694 | . (a -> b) -> Primitive a c -> Primitive b c |
695 | 'PrimitiveStream = \(a :: _) (b :: _) -> _rhs ['Primitive b a] | 695 | 'PrimitiveStream = \(a :: _) (b :: _) -> _rhs ['Primitive b a] |
696 | mapPrimitives | 696 | mapPrimitives |
697 | = (\(a :: _) -> _rhs (map (mapPrimitive a))) | 697 | :: forall (a :: _) (b :: _) (c :: _) |
698 | :: forall (b :: _) (c :: _) (d :: _) | 698 | . (a -> b) -> PrimitiveStream c a -> PrimitiveStream c b |
699 | . (b -> c) -> PrimitiveStream d b -> PrimitiveStream d c | 699 | mapPrimitives = \(a :: _) -> _rhs (map (mapPrimitive a)) |
700 | 'ListElem | 700 | 'ListElem :: Type -> Type |
701 | = (\(a :: _) -> match'List (\_ -> _) (\(b :: _) -> _rhs b) a undefined) | 701 | 'ListElem = \(a :: _) -> match'List (\_ -> _) (\(b :: _) -> _rhs b) a undefined |
702 | :: Type -> Type | ||
703 | fetchArrays | 702 | fetchArrays |
704 | :: forall (a :: _) (b :: _) (c :: _) | 703 | :: forall (a :: _) (b :: _) (c :: _) |
705 | . (b ~ map ListElem c) => HList c -> PrimitiveStream a (HList b) | 704 | . (b ~ map ListElem c) => HList c -> PrimitiveStream a (HList b) |
@@ -721,33 +720,33 @@ sFragmentValue | |||
721 | customizeDepth | 720 | customizeDepth |
722 | :: forall (a :: _) (b :: _) . (a -> Float) -> Fragment b a -> Fragment b a | 721 | :: forall (a :: _) (b :: _) . (a -> Float) -> Fragment b a -> Fragment b a |
723 | customizeDepths | 722 | customizeDepths |
724 | = (\(a :: _) -> _rhs (map (customizeDepth a))) | 723 | :: forall (a :: _) (b :: _) |
725 | :: forall (b :: _) (c :: _) | 724 | . (a -> Float) -> FragmentStream b a -> FragmentStream b a |
726 | . (b -> Float) -> FragmentStream c b -> FragmentStream c b | 725 | customizeDepths = \(a :: _) -> _rhs (map (customizeDepth a)) |
727 | filterFragment | 726 | filterFragment |
728 | :: forall (a :: _) (b :: _) . (a -> Bool) -> Fragment b a -> Fragment b a | 727 | :: forall (a :: _) (b :: _) . (a -> Bool) -> Fragment b a -> Fragment b a |
729 | filterFragments | 728 | filterFragments |
730 | = (\(a :: _) -> _rhs (map (filterFragment a))) | 729 | :: forall (a :: _) (b :: _) |
731 | :: forall (b :: _) (c :: _) | 730 | . (a -> Bool) -> FragmentStream b a -> FragmentStream b a |
732 | . (b -> Bool) -> FragmentStream c b -> FragmentStream c b | 731 | filterFragments = \(a :: _) -> _rhs (map (filterFragment a)) |
733 | mapFragment | 732 | mapFragment |
734 | :: forall (a :: _) (b :: _) (c :: _) . (a -> b) -> Fragment c a -> Fragment c b | 733 | :: forall (a :: _) (b :: _) (c :: _) . (a -> b) -> Fragment c a -> Fragment c b |
735 | mapFragments | 734 | mapFragments |
736 | = (\(a :: _) -> _rhs (map (mapFragment a))) | 735 | :: forall (a :: _) (b :: _) (c :: _) |
737 | :: forall (b :: _) (c :: _) (d :: _) | 736 | . (a -> b) -> FragmentStream c a -> FragmentStream c b |
738 | . (b -> c) -> FragmentStream d b -> FragmentStream d c | 737 | mapFragments = \(a :: _) -> _rhs (map (mapFragment a)) |
739 | data ImageKind :: Type where | 738 | data ImageKind :: Type where |
740 | Color :: Type -> ImageKind | 739 | Color :: Type -> ImageKind |
741 | Depth :: ImageKind | 740 | Depth :: ImageKind |
742 | Stencil :: ImageKind | 741 | Stencil :: ImageKind |
742 | imageType :: ImageKind -> Type | ||
743 | imageType | 743 | imageType |
744 | = (\(a :: _) -> case'ImageKind | 744 | = \(a :: _) -> case'ImageKind |
745 | (\_ -> _) | 745 | (\_ -> _) |
746 | (\(b :: _) -> _rhs b) | 746 | (\(b :: _) -> _rhs b) |
747 | (_rhs 'Float) | 747 | (_rhs 'Float) |
748 | (_rhs 'Int) | 748 | (_rhs 'Int) |
749 | a) | 749 | a |
750 | :: ImageKind -> Type | ||
751 | data Image (_ :: Nat) (_ :: ImageKind) :: Type where | 750 | data Image (_ :: Nat) (_ :: ImageKind) :: Type where |
752 | 751 | ||
753 | ColorImage | 752 | ColorImage |
@@ -762,47 +761,48 @@ data Swizz :: Type where | |||
762 | Sy :: Swizz | 761 | Sy :: Swizz |
763 | Sz :: Swizz | 762 | Sz :: Swizz |
764 | Sw :: Swizz | 763 | Sw :: Swizz |
764 | swizzscalar :: forall (a :: _) (b :: _) . Vec b a -> Swizz -> a | ||
765 | swizzscalar | 765 | swizzscalar |
766 | = (\(a :: _) (b :: _) -> case'VecS | 766 | = \(a :: _) (b :: _) -> case'VecS |
767 | (\_ _ -> _) | 767 | (\_ _ -> _) |
768 | (\(c :: _) (d :: _) -> case'Swizz | 768 | (\(c :: _) (d :: _) -> case'Swizz |
769 | (\_ -> _) | 769 | (\_ -> _) |
770 | (_rhs c) | 770 | (_rhs c) |
771 | (_rhs d) | 771 | (_rhs d) |
772 | (_rhs undefined) | 772 | (_rhs undefined) |
773 | (_rhs undefined) | 773 | (_rhs undefined) |
774 | b) | 774 | b) |
775 | (\(e :: _) (f :: _) (g :: _) -> case'Swizz | 775 | (\(e :: _) (f :: _) (g :: _) -> case'Swizz |
776 | (\_ -> _) | ||
777 | (_rhs e) | ||
778 | (_rhs f) | ||
779 | (_rhs g) | ||
780 | (_rhs undefined) | ||
781 | b) | ||
782 | (\(h :: _) (i :: _) (j :: _) (k :: _) -> case'Swizz | ||
783 | (\_ -> _) | ||
784 | (_rhs h) | ||
785 | (_rhs i) | ||
786 | (_rhs j) | ||
787 | (_rhs k) | ||
788 | b) | ||
789 | a) | ||
790 | :: forall (l :: _) (m :: _) . Vec m l -> Swizz -> l | ||
791 | definedVec | ||
792 | = (\(a :: _) -> case'VecS | ||
793 | (\_ _ -> _) | ||
794 | (\_ _ -> _rhs True) | ||
795 | (\_ _ _ -> _rhs True) | ||
796 | (\_ _ _ _ -> _rhs True) | ||
797 | a) | ||
798 | :: forall (b :: _) (c :: _) . Vec c b -> Bool | ||
799 | swizzvector | ||
800 | = (\(a :: _) (b :: _) -> case'Bool | ||
801 | (\_ -> _) | 776 | (\_ -> _) |
777 | (_rhs e) | ||
778 | (_rhs f) | ||
779 | (_rhs g) | ||
802 | (_rhs undefined) | 780 | (_rhs undefined) |
803 | (_rhs (mapVec (swizzscalar a) b)) | 781 | b) |
804 | (definedVec a)) | 782 | (\(h :: _) (i :: _) (j :: _) (k :: _) -> case'Swizz |
805 | :: forall (c :: _) (d :: _) (e :: _) . Vec d c -> Vec e Swizz -> Vec e c | 783 | (\_ -> _) |
784 | (_rhs h) | ||
785 | (_rhs i) | ||
786 | (_rhs j) | ||
787 | (_rhs k) | ||
788 | b) | ||
789 | a | ||
790 | definedVec :: forall (a :: _) (b :: _) . Vec b a -> Bool | ||
791 | definedVec | ||
792 | = \(a :: _) -> case'VecS | ||
793 | (\_ _ -> _) | ||
794 | (\_ _ -> _rhs True) | ||
795 | (\_ _ _ -> _rhs True) | ||
796 | (\_ _ _ _ -> _rhs True) | ||
797 | a | ||
798 | swizzvector | ||
799 | :: forall (a :: _) (b :: _) (c :: _) . Vec b a -> Vec c Swizz -> Vec c a | ||
800 | swizzvector | ||
801 | = \(a :: _) (b :: _) -> case'Bool | ||
802 | (\_ -> _) | ||
803 | (_rhs undefined) | ||
804 | (_rhs (mapVec (swizzscalar a) b)) | ||
805 | (definedVec a) | ||
806 | data BlendingFactor :: Type where | 806 | data BlendingFactor :: Type where |
807 | ZeroBF :: BlendingFactor | 807 | ZeroBF :: BlendingFactor |
808 | OneBF :: BlendingFactor | 808 | OneBF :: BlendingFactor |
@@ -924,42 +924,42 @@ rasterizePrimitive | |||
924 | -> Primitive (HList c) d -> FragmentStream (fromInt 1) (HList a) | 924 | -> Primitive (HList c) d -> FragmentStream (fromInt 1) (HList a) |
925 | rasterizePrimitives | 925 | rasterizePrimitives |
926 | = \(a :: _) (b :: _) (c :: _) -> _rhs (concat (map (rasterizePrimitive b a) c)) | 926 | = \(a :: _) (b :: _) (c :: _) -> _rhs (concat (map (rasterizePrimitive b a) c)) |
927 | 'ImageLC :: Type -> Nat | ||
927 | 'ImageLC | 928 | 'ImageLC |
928 | = (\(a :: _) -> match'Image (\_ -> _) (\(b :: _) _ -> _rhs b) a undefined) | 929 | = \(a :: _) -> match'Image (\_ -> _) (\(b :: _) _ -> _rhs b) a undefined |
929 | :: Type -> Nat | 930 | allSame :: forall (a :: _) . [a] -> Type |
930 | allSame | 931 | allSame |
931 | = (\(a :: _) -> case'List | 932 | = \(a :: _) -> case'List |
933 | (\_ -> _) | ||
934 | (_rhs 'Unit) | ||
935 | (\(b :: _) (c :: _) -> case'List | ||
932 | (\_ -> _) | 936 | (\_ -> _) |
933 | (_rhs 'Unit) | 937 | (_rhs 'Unit) |
934 | (\(b :: _) (c :: _) -> case'List | 938 | (\(d :: _) (e :: _) -> _rhs ('T2 (b `'EqCTt` d) (allSame (d : e)))) |
935 | (\_ -> _) | 939 | c) |
936 | (_rhs 'Unit) | 940 | a |
937 | (\(d :: _) (e :: _) -> _rhs ('T2 (b `'EqCTt` d) (allSame (d : e)))) | ||
938 | c) | ||
939 | a) | ||
940 | :: forall (f :: _) . [f] -> Type | ||
941 | sameLayerCounts = \(a :: _) -> _rhs (allSame (map 'ImageLC a)) | 941 | sameLayerCounts = \(a :: _) -> _rhs (allSame (map 'ImageLC a)) |
942 | data FrameBuffer (_ :: Nat) (_ :: [ImageKind]) :: Type where | 942 | data FrameBuffer (_ :: Nat) (_ :: [ImageKind]) :: Type where |
943 | 943 | ||
944 | imageType' :: [ImageKind] -> [Type] | ||
944 | imageType' | 945 | imageType' |
945 | = (\(a :: _) -> case'List | 946 | = \(a :: _) -> case'List |
947 | (\_ -> _) | ||
948 | (_rhs (map imageType a)) | ||
949 | (\(b :: _) (c :: _) -> case'ImageKind | ||
946 | (\_ -> _) | 950 | (\_ -> _) |
951 | (\_ -> _rhs (map imageType a)) | ||
952 | (_rhs (map imageType c)) | ||
947 | (_rhs (map imageType a)) | 953 | (_rhs (map imageType a)) |
948 | (\(b :: _) (c :: _) -> case'ImageKind | 954 | b) |
949 | (\_ -> _) | 955 | a |
950 | (\_ -> _rhs (map imageType a)) | 956 | 'FragmentOperationKind :: Type -> ImageKind |
951 | (_rhs (map imageType c)) | ||
952 | (_rhs (map imageType a)) | ||
953 | b) | ||
954 | a) | ||
955 | :: [ImageKind] -> [Type] | ||
956 | 'FragmentOperationKind | 957 | 'FragmentOperationKind |
957 | = (\(a :: _) -> match'FragmentOperation | 958 | = \(a :: _) -> match'FragmentOperation |
958 | (\_ -> _) | 959 | (\_ -> _) |
959 | (\(b :: _) -> _rhs b) | 960 | (\(b :: _) -> _rhs b) |
960 | a | 961 | a |
961 | undefined) | 962 | undefined |
962 | :: Type -> ImageKind | ||
963 | Accumulate | 963 | Accumulate |
964 | :: forall (a :: _) (b :: Nat) (c :: [Type]) | 964 | :: forall (a :: _) (b :: Nat) (c :: [Type]) |
965 | . (a ~ map FragmentOperationKind c) | 965 | . (a ~ map FragmentOperationKind c) |
@@ -975,9 +975,9 @@ overlay | |||
975 | d) | 975 | d) |
976 | b | 976 | b |
977 | infixl 0 overlay | 977 | infixl 0 overlay |
978 | 'GetImageKind :: Type -> ImageKind | ||
978 | 'GetImageKind | 979 | 'GetImageKind |
979 | = (\(a :: _) -> match'Image (\_ -> _) (\_ (b :: _) -> _rhs b) a undefined) | 980 | = \(a :: _) -> match'Image (\_ -> _) (\_ (b :: _) -> _rhs b) a undefined |
980 | :: Type -> ImageKind | ||
981 | FrameBuffer | 981 | FrameBuffer |
982 | :: forall (a :: [Type]) | 982 | :: forall (a :: [Type]) |
983 | . sameLayerCounts a | 983 | . sameLayerCounts a |
diff --git a/testdata/Internals.out b/testdata/Internals.out index 9ae0f3e1..b3eac04a 100644 --- a/testdata/Internals.out +++ b/testdata/Internals.out | |||
@@ -50,145 +50,141 @@ primSubInt :: Int -> Int -> Int | |||
50 | primModInt :: Int -> Int -> Int | 50 | primModInt :: Int -> Int -> Int |
51 | primSqrtFloat :: Float -> Float | 51 | primSqrtFloat :: Float -> Float |
52 | primRound :: Float -> Int | 52 | primRound :: Float -> Int |
53 | primIfThenElse :: forall (a :: _) . Bool -> a -> a -> a | ||
53 | primIfThenElse | 54 | primIfThenElse |
54 | = (\(a :: _) (b :: _) (c :: _) -> case'Bool (\_ -> _) (_rhs c) (_rhs b) a) | 55 | = \(a :: _) (b :: _) (c :: _) -> case'Bool (\_ -> _) (_rhs c) (_rhs b) a |
55 | :: forall (d :: _) . Bool -> d -> d -> d | ||
56 | isEQ | 56 | isEQ |
57 | = \(a :: _) -> case'Ordering (\_ -> _) (_rhs False) (_rhs True) (_rhs False) a | 57 | = \(a :: _) -> case'Ordering (\_ -> _) (_rhs False) (_rhs True) (_rhs False) a |
58 | 'Num :: Type -> Type | ||
58 | 'Num | 59 | 'Num |
59 | = (\(a :: _) -> match'Int | 60 | = \(a :: _) -> match'Int |
61 | (\_ -> _) | ||
62 | (_rhs 'Unit) | ||
63 | a | ||
64 | (match'Word | ||
60 | (\_ -> _) | 65 | (\_ -> _) |
61 | (_rhs 'Unit) | 66 | (_rhs 'Unit) |
62 | a | 67 | a |
63 | (match'Word | 68 | (match'Float |
64 | (\_ -> _) | 69 | (\_ -> _) |
65 | (_rhs 'Unit) | 70 | (_rhs 'Unit) |
66 | a | 71 | a |
67 | (match'Float | 72 | (match'Nat |
68 | (\_ -> _) | 73 | (\_ -> _) |
69 | (_rhs 'Unit) | 74 | (_rhs 'Unit) |
70 | a | 75 | a |
71 | (match'Nat | 76 | (_rhs ('Empty "no instance of 'Num on ???"))))) |
72 | (\_ -> _) | 77 | fromInt :: forall a . Num a => Int -> a |
73 | (_rhs 'Unit) | ||
74 | a | ||
75 | (_rhs ('Empty "no instance of 'Num on ???")))))) | ||
76 | :: Type -> Type | ||
77 | fromInt | 78 | fromInt |
78 | = (\ @a @_ -> match'Int | 79 | = \ @a @_ -> match'Int |
80 | (\_ -> _) | ||
81 | (_rhs \(b := _rhs \(c :: _) -> c) -> b) | ||
82 | a | ||
83 | (match'Word | ||
79 | (\_ -> _) | 84 | (\_ -> _) |
80 | (_rhs \(b := _rhs \(c :: _) -> c) -> b) | 85 | (_rhs \(d := _rhs primIntToWord) -> d) |
81 | a | 86 | a |
82 | (match'Word | 87 | (match'Float |
83 | (\_ -> _) | 88 | (\_ -> _) |
84 | (_rhs \(d := _rhs primIntToWord) -> d) | 89 | (_rhs \(e := _rhs primIntToFloat) -> e) |
85 | a | 90 | a |
86 | (match'Float | 91 | (match'Nat (\_ -> _) (_rhs \(f := _rhs primIntToNat) -> f) a (_rhs undefined)))) |
87 | (\_ -> _) | 92 | compare :: forall a . Num a => a -> a -> Ordering |
88 | (_rhs \(e := _rhs primIntToFloat) -> e) | ||
89 | a | ||
90 | (match'Nat | ||
91 | (\_ -> _) | ||
92 | (_rhs \(f := _rhs primIntToNat) -> f) | ||
93 | a | ||
94 | (_rhs undefined))))) | ||
95 | :: forall g . Num g => Int -> g | ||
96 | compare | 93 | compare |
97 | = (\ @a @_ -> match'Int | 94 | = \ @a @_ -> match'Int |
95 | (\_ -> _) | ||
96 | (_rhs \(b := _rhs primCompareInt) -> b) | ||
97 | a | ||
98 | (match'Word | ||
98 | (\_ -> _) | 99 | (\_ -> _) |
99 | (_rhs \(b := _rhs primCompareInt) -> b) | 100 | (_rhs \(c := _rhs primCompareWord) -> c) |
100 | a | 101 | a |
101 | (match'Word | 102 | (match'Float |
102 | (\_ -> _) | 103 | (\_ -> _) |
103 | (_rhs \(c := _rhs primCompareWord) -> c) | 104 | (_rhs \(d := _rhs primCompareFloat) -> d) |
104 | a | 105 | a |
105 | (match'Float | 106 | (match'Nat (\_ -> _) (_rhs \(e := _rhs undefined) -> e) a (_rhs undefined)))) |
106 | (\_ -> _) | 107 | negate :: forall a . Num a => a -> a |
107 | (_rhs \(d := _rhs primCompareFloat) -> d) | ||
108 | a | ||
109 | (match'Nat (\_ -> _) (_rhs \(e := _rhs undefined) -> e) a (_rhs undefined))))) | ||
110 | :: forall f . Num f => f -> f -> Ordering | ||
111 | negate | 108 | negate |
112 | = (\ @a @_ -> match'Int | 109 | = \ @a @_ -> match'Int |
110 | (\_ -> _) | ||
111 | (_rhs \(b := _rhs primNegateInt) -> b) | ||
112 | a | ||
113 | (match'Word | ||
113 | (\_ -> _) | 114 | (\_ -> _) |
114 | (_rhs \(b := _rhs primNegateInt) -> b) | 115 | (_rhs \(c := _rhs primNegateWord) -> c) |
115 | a | 116 | a |
116 | (match'Word | 117 | (match'Float |
117 | (\_ -> _) | 118 | (\_ -> _) |
118 | (_rhs \(c := _rhs primNegateWord) -> c) | 119 | (_rhs \(d := _rhs primNegateFloat) -> d) |
119 | a | 120 | a |
120 | (match'Float | 121 | (match'Nat (\_ -> _) (_rhs \(e := _rhs undefined) -> e) a (_rhs undefined)))) |
121 | (\_ -> _) | 122 | 'Eq :: Type -> Type |
122 | (_rhs \(d := _rhs primNegateFloat) -> d) | ||
123 | a | ||
124 | (match'Nat (\_ -> _) (_rhs \(e := _rhs undefined) -> e) a (_rhs undefined))))) | ||
125 | :: forall f . Num f => f -> f | ||
126 | 'Eq | 123 | 'Eq |
127 | = (\(a :: _) -> match'String | 124 | = \(a :: _) -> match'String |
125 | (\_ -> _) | ||
126 | (_rhs 'Unit) | ||
127 | a | ||
128 | (match'Char | ||
128 | (\_ -> _) | 129 | (\_ -> _) |
129 | (_rhs 'Unit) | 130 | (_rhs 'Unit) |
130 | a | 131 | a |
131 | (match'Char | 132 | (match'Int |
132 | (\_ -> _) | 133 | (\_ -> _) |
133 | (_rhs 'Unit) | 134 | (_rhs 'Unit) |
134 | a | 135 | a |
135 | (match'Int | 136 | (match'Float |
136 | (\_ -> _) | 137 | (\_ -> _) |
137 | (_rhs 'Unit) | 138 | (_rhs 'Unit) |
138 | a | 139 | a |
139 | (match'Float | 140 | (match'Bool |
140 | (\_ -> _) | 141 | (\_ -> _) |
141 | (_rhs 'Unit) | 142 | (_rhs 'Unit) |
142 | a | 143 | a |
143 | (match'Bool | 144 | (match'Nat |
144 | (\_ -> _) | 145 | (\_ -> _) |
145 | (_rhs 'Unit) | 146 | (_rhs 'Unit) |
146 | a | 147 | a |
147 | (match'Nat | 148 | (_rhs ('Empty "no instance of 'Eq on ???"))))))) |
148 | (\_ -> _) | 149 | (==) :: forall a . Eq a => a -> a -> Bool |
149 | (_rhs 'Unit) | ||
150 | a | ||
151 | (_rhs ('Empty "no instance of 'Eq on ???")))))))) | ||
152 | :: Type -> Type | ||
153 | (==) | 150 | (==) |
154 | = (\ @a @_ -> match'String | 151 | = \ @a @_ -> match'String |
152 | (\_ -> _) | ||
153 | (_rhs \(b := \(c :: _) (d :: _) -> _rhs (isEQ (primCompareString c d))) -> b) | ||
154 | a | ||
155 | (match'Char | ||
155 | (\_ -> _) | 156 | (\_ -> _) |
156 | (_rhs \(b := \(c :: _) (d :: _) -> _rhs (isEQ (primCompareString c d))) -> b) | 157 | (_rhs \(e := \(f :: _) (g :: _) -> _rhs (isEQ (primCompareChar f g))) -> e) |
157 | a | 158 | a |
158 | (match'Char | 159 | (match'Int |
159 | (\_ -> _) | 160 | (\_ -> _) |
160 | (_rhs \(e := \(f :: _) (g :: _) -> _rhs (isEQ (primCompareChar f g))) -> e) | 161 | (_rhs \(h := \(i :: _) (j :: _) -> _rhs (isEQ (primCompareInt i j))) -> h) |
161 | a | 162 | a |
162 | (match'Int | 163 | (match'Float |
163 | (\_ -> _) | 164 | (\_ -> _) |
164 | (_rhs \(h := \(i :: _) (j :: _) -> _rhs (isEQ (primCompareInt i j))) -> h) | 165 | (_rhs \(k := \(l :: _) (m :: _) -> _rhs (isEQ (primCompareFloat l m))) -> k) |
165 | a | 166 | a |
166 | (match'Float | 167 | (match'Bool |
167 | (\_ -> _) | 168 | (\_ -> _) |
168 | (_rhs \(k := \(l :: _) (m :: _) -> _rhs (isEQ (primCompareFloat l m))) -> k) | 169 | (_rhs |
170 | \(n | ||
171 | := \(o :: _) (p :: _) -> case'Bool | ||
172 | (\_ -> _) | ||
173 | (case'Bool (\_ -> _) (_rhs True) (_rhs False) p) | ||
174 | (case'Bool (\_ -> _) (_rhs False) (_rhs True) p) | ||
175 | o) -> n) | ||
169 | a | 176 | a |
170 | (match'Bool | 177 | (match'Nat |
171 | (\_ -> _) | 178 | (\_ -> _) |
172 | (_rhs | 179 | (_rhs |
173 | \(n | 180 | \(q |
174 | := \(o :: _) (p :: _) -> case'Bool | 181 | := \(r :: _) (s :: _) -> case'Nat |
175 | (\_ -> _) | 182 | (\_ -> _) |
176 | (case'Bool (\_ -> _) (_rhs True) (_rhs False) p) | 183 | (case'Nat (\_ -> _) (_rhs True) (\_ -> _rhs False) s) |
177 | (case'Bool (\_ -> _) (_rhs False) (_rhs True) p) | 184 | (\(t :: _) -> case'Nat (\_ -> _) (_rhs False) (\(u :: _) -> _rhs (t == u)) s) |
178 | o) -> n) | 185 | r) -> q) |
179 | a | 186 | a |
180 | (match'Nat | 187 | (_rhs undefined)))))) |
181 | (\_ -> _) | ||
182 | (_rhs | ||
183 | \(q | ||
184 | := \(r :: _) (s :: _) -> case'Nat | ||
185 | (\_ -> _) | ||
186 | (case'Nat (\_ -> _) (_rhs True) (\_ -> _rhs False) s) | ||
187 | (\(t :: _) -> case'Nat (\_ -> _) (_rhs False) (\(u :: _) -> _rhs (t == u)) s) | ||
188 | r) -> q) | ||
189 | a | ||
190 | (_rhs undefined))))))) | ||
191 | :: forall v . Eq v => v -> v -> Bool | ||
192 | infix 4 == | 188 | infix 4 == |
193 | data List (_ :: Type) :: Type where | 189 | data List (_ :: Type) :: Type where |
194 | [] :: forall a . [a] | 190 | [] :: forall a . [a] |
diff --git a/testdata/Material.out b/testdata/Material.out index fa9c9eb4..360c8021 100644 --- a/testdata/Material.out +++ b/testdata/Material.out | |||
@@ -1,5 +1,6 @@ | |||
1 | ------------ desugared source code | 1 | ------------ desugared source code |
2 | identityLight = _rhs (fromInt 1) :: Float | 2 | identityLight :: Float |
3 | identityLight = _rhs (fromInt 1) | ||
3 | data Entity :: Type where | 4 | data Entity :: Type where |
4 | Entity | 5 | Entity |
5 | :: Vec (fromInt 4) Float | 6 | :: Vec (fromInt 4) Float |
@@ -164,21 +165,21 @@ saTextureUniform | |||
164 | (\_ -> _) | 165 | (\_ -> _) |
165 | (\_ _ _ _ _ _ _ _ _ _ (b :: _) -> _rhs b) | 166 | (\_ _ _ _ _ _ _ _ _ _ (b :: _) -> _rhs b) |
166 | a | 167 | a |
168 | defaultStageAttrs :: StageAttrs | ||
167 | defaultStageAttrs | 169 | defaultStageAttrs |
168 | = _rhs | 170 | = _rhs |
169 | (StageAttrs | 171 | (StageAttrs |
170 | Nothing | 172 | Nothing |
171 | RGB_Undefined | 173 | RGB_Undefined |
172 | A_Identity | 174 | A_Identity |
173 | TG_Undefined | 175 | TG_Undefined |
174 | [] | 176 | [] |
175 | ST_WhiteImage | 177 | ST_WhiteImage |
176 | True | 178 | True |
177 | D_Lequal | 179 | D_Lequal |
178 | Nothing | 180 | Nothing |
179 | False | 181 | False |
180 | "") | 182 | "") |
181 | :: StageAttrs | ||
182 | data CommonAttrs :: Type where | 183 | data CommonAttrs :: Type where |
183 | CommonAttrs | 184 | CommonAttrs |
184 | :: HList '[] | 185 | :: HList '[] |
@@ -248,22 +249,22 @@ caIsSky | |||
248 | (\_ -> _) | 249 | (\_ -> _) |
249 | (\_ _ _ _ _ _ _ _ _ _ _ (b :: _) -> _rhs b) | 250 | (\_ _ _ _ _ _ _ _ _ _ _ (b :: _) -> _rhs b) |
250 | a | 251 | a |
252 | defaultCommonAttrs :: CommonAttrs | ||
251 | defaultCommonAttrs | 253 | defaultCommonAttrs |
252 | = _rhs | 254 | = _rhs |
253 | (CommonAttrs | 255 | (CommonAttrs |
254 | HNil | 256 | HNil |
255 | HNil | 257 | HNil |
256 | False | 258 | False |
257 | (fromInt 0) | 259 | (fromInt 0) |
258 | False | 260 | False |
259 | False | 261 | False |
260 | CT_FrontSided | 262 | CT_FrontSided |
261 | [] | 263 | [] |
262 | False | 264 | False |
263 | False | 265 | False |
264 | [] | 266 | [] |
265 | False) | 267 | False) |
266 | :: CommonAttrs | ||
267 | main is not found | 268 | main is not found |
268 | ------------ trace | 269 | ------------ trace |
269 | identityLight :: Float | 270 | identityLight :: Float |
diff --git a/testdata/Prelude.out b/testdata/Prelude.out index 56e17569..3e8b2b17 100644 --- a/testdata/Prelude.out +++ b/testdata/Prelude.out | |||
@@ -27,48 +27,49 @@ uncurry | |||
27 | e) | 27 | e) |
28 | c | 28 | c |
29 | pi = _rhs 3.141592653589793 | 29 | pi = _rhs 3.141592653589793 |
30 | zip :: forall (a :: _) (b :: _) . [a] -> [b] -> [HList (a : b : '[])] | ||
30 | zip | 31 | zip |
31 | = (\(a :: _) (b :: _) -> case'List | 32 | = \(a :: _) (b :: _) -> case'List |
33 | (\_ -> _) | ||
34 | (_rhs []) | ||
35 | (\(c :: _) (d :: _) -> case'List | ||
32 | (\_ -> _) | 36 | (\_ -> _) |
33 | (_rhs []) | 37 | (_rhs []) |
34 | (\(c :: _) (d :: _) -> case'List | 38 | (\(e :: _) (f :: _) -> _rhs (HCons c (HCons e HNil) : zip d f)) |
35 | (\_ -> _) | 39 | b) |
36 | (_rhs []) | 40 | a |
37 | (\(e :: _) (f :: _) -> _rhs (HCons c (HCons e HNil) : zip d f)) | ||
38 | b) | ||
39 | a) | ||
40 | :: forall (g :: _) (h :: _) . [g] -> [h] -> [HList (g : h : '[])] | ||
41 | unzip | 41 | unzip |
42 | = (\(a :: _) -> case'List | 42 | :: forall (a :: _) (b :: _) . [HList (a : b : '[])] -> HList ([a] : [b] : '[]) |
43 | (\_ -> _) | 43 | unzip |
44 | (_rhs (HCons [] (HCons [] HNil))) | 44 | = \(a :: _) -> case'List |
45 | (\(b :: _) (c :: _) -> hlistConsCase | 45 | (\_ -> _) |
46 | (_rhs (HCons [] (HCons [] HNil))) | ||
47 | (\(b :: _) (c :: _) -> hlistConsCase | ||
48 | _ | ||
49 | (\(d :: _) (e :: _) -> hlistConsCase | ||
46 | _ | 50 | _ |
47 | (\(d :: _) (e :: _) -> hlistConsCase | 51 | (\(f :: _) (g :: _) -> hlistNilCase |
48 | _ | 52 | _ |
49 | (\(f :: _) (g :: _) -> hlistNilCase | 53 | (_rhs |
50 | _ | 54 | \(h := _rhs (unzip c)) |
51 | (_rhs | 55 | (i |
52 | \(h := _rhs (unzip c)) | 56 | := _rhs |
53 | (i | 57 | ((\(k :: _) -> hlistConsCase |
54 | := _rhs | 58 | _ |
55 | ((\(k :: _) -> hlistConsCase | 59 | (\_ (l :: _) -> hlistConsCase _ (\(m :: _) (n :: _) -> hlistNilCase _ m n) l) |
56 | _ | 60 | k) |
57 | (\_ (l :: _) -> hlistConsCase _ (\(m :: _) (n :: _) -> hlistNilCase _ m n) l) | 61 | h)) |
58 | k) | 62 | (j |
59 | h)) | 63 | := _rhs |
60 | (j | 64 | ((\(o :: _) -> hlistConsCase |
61 | := _rhs | 65 | _ |
62 | ((\(o :: _) -> hlistConsCase | 66 | (\(p :: _) (q :: _) -> hlistConsCase _ (\_ (r :: _) -> hlistNilCase _ p r) q) |
63 | _ | 67 | o) |
64 | (\(p :: _) (q :: _) -> hlistConsCase _ (\_ (r :: _) -> hlistNilCase _ p r) q) | 68 | h)) -> HCons (d : j) (HCons (f : i) HNil)) |
65 | o) | 69 | g) |
66 | h)) -> HCons (d : j) (HCons (f : i) HNil)) | 70 | e) |
67 | g) | 71 | b) |
68 | e) | 72 | a |
69 | b) | ||
70 | a) | ||
71 | :: forall (s :: _) (t :: _) . [HList (s : t : '[])] -> HList ([s] : [t] : '[]) | ||
72 | filter | 73 | filter |
73 | = \(a :: _) (b :: _) -> case'List | 74 | = \(a :: _) (b :: _) -> case'List |
74 | (\_ -> _) | 75 | (\_ -> _) |
@@ -76,12 +77,11 @@ filter | |||
76 | (\(c :: _) (d :: _) -> _rhs | 77 | (\(c :: _) (d :: _) -> _rhs |
77 | ((\(e :: _) -> case'Bool (\_ -> _) (filter a d) (c : filter a d) e) (a c))) | 78 | ((\(e :: _) -> case'Bool (\_ -> _) (filter a d) (c : filter a d) e) (a c))) |
78 | b | 79 | b |
80 | tail :: forall (a :: _) . [a] -> [a] | ||
79 | tail | 81 | tail |
80 | = (\(a :: _) -> case'List (\_ -> _) (_rhs undefined) (\_ (b :: _) -> _rhs b) a) | 82 | = \(a :: _) -> case'List (\_ -> _) (_rhs undefined) (\_ (b :: _) -> _rhs b) a |
81 | :: forall (c :: _) . [c] -> [c] | 83 | pairs :: forall (a :: _) . [a] -> [HList (a : a : '[])] |
82 | pairs | 84 | pairs = \(a :: _) -> _rhs (zip a (tail a)) |
83 | = (\(a :: _) -> _rhs (zip a (tail a))) | ||
84 | :: forall (b :: _) . [b] -> [HList (b : b : '[])] | ||
85 | foldl' | 85 | foldl' |
86 | = \(a :: _) (b :: _) (c :: _) -> case'List | 86 | = \(a :: _) (b :: _) (c :: _) -> case'List |
87 | (\_ -> _) | 87 | (\_ -> _) |
@@ -142,9 +142,8 @@ sortBy | |||
142 | (\_ _ -> _rhs (uncurry (mergeBy a) ((sortBy a *** sortBy a) (split b)))) | 142 | (\_ _ -> _rhs (uncurry (mergeBy a) ((sortBy a *** sortBy a) (split b)))) |
143 | d) | 143 | d) |
144 | b | 144 | b |
145 | iterate | 145 | iterate :: forall (a :: _) . (a -> a) -> a -> [a] |
146 | = (\(a :: _) (b :: _) -> _rhs (b : iterate a (a b))) | 146 | iterate = \(a :: _) (b :: _) -> _rhs (b : iterate a (a b)) |
147 | :: forall (c :: _) . (c -> c) -> c -> [c] | ||
148 | fst | 147 | fst |
149 | = \(a :: _) -> hlistConsCase | 148 | = \(a :: _) -> hlistConsCase |
150 | _ | 149 | _ |
@@ -183,30 +182,31 @@ isKeyC | |||
183 | fstTup = _rhs (hlistConsCase (_ :: _) \(a :: _) _ -> a) | 182 | fstTup = _rhs (hlistConsCase (_ :: _) \(a :: _) _ -> a) |
184 | sndTup = _rhs (hlistConsCase (_ :: _) \_ (a :: _) -> a) | 183 | sndTup = _rhs (hlistConsCase (_ :: _) \_ (a :: _) -> a) |
185 | project | 184 | project |
186 | = (\ @(a :: _) @(b :: _) (c :: _) @_ (d :: _) -> case'List | 185 | :: forall (a :: _) (b :: [RecItem]) |
186 | . forall (c :: String) -> isKeyC c a b => RecordC b -> a | ||
187 | project | ||
188 | = \ @(a :: _) @(b :: _) (c :: _) @_ (d :: _) -> case'List | ||
189 | (\_ -> _) | ||
190 | (_rhs undefined) | ||
191 | (\(e :: _) (f :: _) -> case'RecItem | ||
187 | (\_ -> _) | 192 | (\_ -> _) |
188 | (_rhs undefined) | 193 | (\(g :: _) _ -> case'RecordC |
189 | (\(e :: _) (f :: _) -> case'RecItem | ||
190 | (\_ -> _) | 194 | (\_ -> _) |
191 | (\(g :: _) _ -> case'RecordC | 195 | (\(h :: _) -> case'Bool |
192 | (\_ -> _) | 196 | (\_ -> _) |
193 | (\(h :: _) -> case'Bool | 197 | (_rhs |
194 | (\_ -> _) | 198 | (project |
195 | (_rhs | 199 | @a |
196 | (project | 200 | @f |
197 | @a | 201 | c |
198 | @f | 202 | @(undefined @(isKeyC c a f)) |
199 | c | 203 | (RecordCons |
200 | @(undefined @(isKeyC c a f)) | 204 | (sndTup (unsafeCoerce @(_ :: _) @('HList (a : map recItemType f)) h))))) |
201 | (RecordCons | 205 | (_rhs (fstTup (unsafeCoerce @(_ :: _) @('HList (a : map recItemType f)) h))) |
202 | (sndTup (unsafeCoerce @(_ :: _) @('HList (a : map recItemType f)) h))))) | 206 | (c == g)) |
203 | (_rhs (fstTup (unsafeCoerce @(_ :: _) @('HList (a : map recItemType f)) h))) | 207 | d) |
204 | (c == g)) | 208 | e) |
205 | d) | 209 | b |
206 | e) | ||
207 | b) | ||
208 | :: forall (i :: _) (j :: [RecItem]) | ||
209 | . forall (k :: String) -> isKeyC k i j => RecordC j -> i | ||
210 | rgb = \(a :: _) (b :: _) (c :: _) -> _rhs (V4 a b c 1.0) | 210 | rgb = \(a :: _) (b :: _) (c :: _) -> _rhs (V4 a b c 1.0) |
211 | black = _rhs (rgb 0.0 0.0 0.0) | 211 | black = _rhs (rgb 0.0 0.0 0.0) |
212 | gray = _rhs (rgb 0.5 0.5 0.5) | 212 | gray = _rhs (rgb 0.5 0.5 0.5) |
@@ -227,10 +227,10 @@ fuchsia = _rhs (rgb 1.0 0.0 1.0) | |||
227 | colorImage1 = _rhs (ColorImage @(fromInt 1)) | 227 | colorImage1 = _rhs (ColorImage @(fromInt 1)) |
228 | colorImage2 = _rhs (ColorImage @(fromInt 2)) | 228 | colorImage2 = _rhs (ColorImage @(fromInt 2)) |
229 | depthImage1 = _rhs (DepthImage @(fromInt 1)) | 229 | depthImage1 = _rhs (DepthImage @(fromInt 1)) |
230 | v3FToV4F :: Vec (fromInt 3) Float -> Vec (fromInt 4) Float | ||
230 | v3FToV4F | 231 | v3FToV4F |
231 | = (\(a :: _) -> _rhs | 232 | = \(a :: _) -> _rhs |
232 | (V4 (swizzscalar a Sx) (swizzscalar a Sy) (swizzscalar a Sz) (fromInt 1))) | 233 | (V4 (swizzscalar a Sx) (swizzscalar a Sy) (swizzscalar a Sz) (fromInt 1)) |
233 | :: Vec (fromInt 3) Float -> Vec (fromInt 4) Float | ||
234 | radians = _rhs PrimRadians | 234 | radians = _rhs PrimRadians |
235 | degrees = _rhs PrimDegrees | 235 | degrees = _rhs PrimDegrees |
236 | sin = _rhs PrimSin | 236 | sin = _rhs PrimSin |
@@ -358,23 +358,24 @@ infixl 6 -! | |||
358 | (/!) = \(a :: _) (b :: _) -> _rhs (PrimDivS a b) | 358 | (/!) = \(a :: _) (b :: _) -> _rhs (PrimDivS a b) |
359 | (%!) = \(a :: _) (b :: _) -> _rhs (PrimModS a b) | 359 | (%!) = \(a :: _) (b :: _) -> _rhs (PrimModS a b) |
360 | perspective | 360 | perspective |
361 | = (\(a :: _) (b :: _) (c :: _) (d :: _) -> _rhs | 361 | :: Float -> Float -> Float -> Float -> Mat (fromInt 4) (fromInt 4) Float |
362 | \(e := _rhs (a * tan (c / fromInt 2))) | 362 | perspective |
363 | (f := _rhs (fromInt 0 - e)) | 363 | = \(a :: _) (b :: _) (c :: _) (d :: _) -> _rhs |
364 | (g := _rhs (d * e)) (h := _rhs (fromInt 0 - g)) -> M44F | 364 | \(e := _rhs (a * tan (c / fromInt 2))) |
365 | (V4 (fromInt 2 * a / (g - h)) (fromInt 0) (fromInt 0) (fromInt 0)) | 365 | (f := _rhs (fromInt 0 - e)) |
366 | (V4 (fromInt 0) (fromInt 2 * a / (e - f)) (fromInt 0) (fromInt 0)) | 366 | (g := _rhs (d * e)) (h := _rhs (fromInt 0 - g)) -> M44F |
367 | (V4 | 367 | (V4 (fromInt 2 * a / (g - h)) (fromInt 0) (fromInt 0) (fromInt 0)) |
368 | ((g + h) / (g - h)) | 368 | (V4 (fromInt 0) (fromInt 2 * a / (e - f)) (fromInt 0) (fromInt 0)) |
369 | ((e + f) / (e - f)) | 369 | (V4 |
370 | (fromInt 0 - (b + a) / (b - a)) | 370 | ((g + h) / (g - h)) |
371 | (fromInt 0 - fromInt 1)) | 371 | ((e + f) / (e - f)) |
372 | (V4 | 372 | (fromInt 0 - (b + a) / (b - a)) |
373 | (fromInt 0) | 373 | (fromInt 0 - fromInt 1)) |
374 | (fromInt 0) | 374 | (V4 |
375 | (fromInt 0 - fromInt 2 * b * a / (b - a)) | 375 | (fromInt 0) |
376 | (fromInt 0))) | 376 | (fromInt 0) |
377 | :: Float -> Float -> Float -> Float -> Mat (fromInt 4) (fromInt 4) Float | 377 | (fromInt 0 - fromInt 2 * b * a / (b - a)) |
378 | (fromInt 0)) | ||
378 | rotMatrixZ | 379 | rotMatrixZ |
379 | = \(a :: _) -> _rhs | 380 | = \(a :: _) -> _rhs |
380 | \(b := _rhs (cos a)) (c := _rhs (sin a)) -> M44F | 381 | \(b := _rhs (cos a)) (c := _rhs (sin a)) -> M44F |
@@ -399,58 +400,59 @@ rotMatrixX | |||
399 | rotationEuler | 400 | rotationEuler |
400 | = \(a :: _) (b :: _) (c :: _) -> _rhs | 401 | = \(a :: _) (b :: _) (c :: _) -> _rhs |
401 | (rotMatrixY a .*. rotMatrixX b .*. rotMatrixZ c) | 402 | (rotMatrixY a .*. rotMatrixX b .*. rotMatrixZ c) |
403 | translateBefore4 :: Vec (fromInt 3) Float -> Mat (fromInt 4) (fromInt 4) Float | ||
402 | translateBefore4 | 404 | translateBefore4 |
403 | = (\(a :: _) -> _rhs | 405 | = \(a :: _) -> _rhs |
404 | \(b := _rhs (V4 (fromInt 1) (fromInt 0) (fromInt 0) (fromInt 0))) | 406 | \(b := _rhs (V4 (fromInt 1) (fromInt 0) (fromInt 0) (fromInt 0))) |
405 | (c := _rhs (V4 (fromInt 0) (fromInt 1) (fromInt 0) (fromInt 0))) | 407 | (c := _rhs (V4 (fromInt 0) (fromInt 1) (fromInt 0) (fromInt 0))) |
406 | (d := _rhs (V4 (fromInt 0) (fromInt 0) (fromInt 1) (fromInt 0))) | 408 | (d := _rhs (V4 (fromInt 0) (fromInt 0) (fromInt 1) (fromInt 0))) |
407 | (e | 409 | (e |
408 | := _rhs | 410 | := _rhs |
409 | (V4 | 411 | (V4 |
410 | (swizzscalar a Sx) | 412 | (swizzscalar a Sx) |
411 | (swizzscalar a Sy) | 413 | (swizzscalar a Sy) |
412 | (swizzscalar a Sz) | 414 | (swizzscalar a Sz) |
413 | (fromInt 1))) -> M44F b c d e) | 415 | (fromInt 1))) -> M44F b c d e |
414 | :: Vec (fromInt 3) Float -> Mat (fromInt 4) (fromInt 4) Float | ||
415 | lookat | 416 | lookat |
416 | = (\(a :: _) (b :: _) (c :: _) -> _rhs | 417 | :: Vec (fromInt 3) Float |
417 | \(d | 418 | -> Vec (fromInt 3) Float |
418 | := \(i :: _) -> _rhs | 419 | -> Vec (fromInt 3) Float -> Mat (fromInt 4) (fromInt 4) Float |
419 | (V4 (swizzscalar i Sx) (swizzscalar i Sy) (swizzscalar i Sz) (fromInt 0))) | 420 | lookat |
420 | (e := _rhs (normalize $ a - b)) | 421 | = \(a :: _) (b :: _) (c :: _) -> _rhs |
421 | (f := _rhs (normalize $ c `cross` e)) | 422 | \(d |
422 | (g := _rhs (e `cross` f)) | 423 | := \(i :: _) -> _rhs |
423 | (h | 424 | (V4 (swizzscalar i Sx) (swizzscalar i Sy) (swizzscalar i Sz) (fromInt 0))) |
424 | := _rhs | 425 | (e := _rhs (normalize $ a - b)) |
425 | (transpose | 426 | (f := _rhs (normalize $ c `cross` e)) |
426 | $ M44F | 427 | (g := _rhs (e `cross` f)) |
427 | (d f) | 428 | (h |
428 | (d g) | 429 | := _rhs |
429 | (d e) | 430 | (transpose |
430 | (V4 (fromInt 0) (fromInt 0) (fromInt 0) (fromInt 1)))) -> h | 431 | $ M44F |
431 | .*. translateBefore4 (neg a)) | 432 | (d f) |
432 | :: Vec (fromInt 3) Float | 433 | (d g) |
433 | -> Vec (fromInt 3) Float | 434 | (d e) |
434 | -> Vec (fromInt 3) Float -> Mat (fromInt 4) (fromInt 4) Float | 435 | (V4 (fromInt 0) (fromInt 0) (fromInt 0) (fromInt 1)))) -> h |
436 | .*. translateBefore4 (neg a) | ||
435 | scale = \(a :: _) (b :: _) -> _rhs (b * V4 a a a 1.0) | 437 | scale = \(a :: _) (b :: _) -> _rhs (b * V4 a a a 1.0) |
438 | fromTo :: Float -> Float -> [Float] | ||
436 | fromTo | 439 | fromTo |
437 | = (\(a :: _) (b :: _) -> case'Bool | 440 | = \(a :: _) (b :: _) -> case'Bool |
438 | (\_ -> _) | 441 | (\_ -> _) |
439 | (_rhs (a : fromTo (a + fromInt 1) b)) | 442 | (_rhs (a : fromTo (a + fromInt 1) b)) |
440 | (_rhs []) | 443 | (_rhs []) |
441 | (a > b)) | 444 | (a > b) |
442 | :: Float -> Float -> [Float] | 445 | (!!) :: forall (a :: _) . [a] -> Int -> a |
443 | (!!) | 446 | (!!) |
444 | = (\(a :: _) (b :: _) -> case'List | 447 | = \(a :: _) (b :: _) -> case'List |
448 | (\_ -> _) | ||
449 | (_rhs undefined) | ||
450 | (\(c :: _) (d :: _) -> case'Bool | ||
445 | (\_ -> _) | 451 | (\_ -> _) |
446 | (_rhs undefined) | 452 | (_rhs (d !! (b - fromInt 1))) |
447 | (\(c :: _) (d :: _) -> case'Bool | 453 | (_rhs c) |
448 | (\_ -> _) | 454 | (fromInt 0 == b)) |
449 | (_rhs (d !! (b - fromInt 1))) | 455 | a |
450 | (_rhs c) | ||
451 | (fromInt 0 == b)) | ||
452 | a) | ||
453 | :: forall (e :: _) . [e] -> Int -> e | ||
454 | main is not found | 456 | main is not found |
455 | ------------ trace | 457 | ------------ trace |
456 | const :: forall a b . a -> b -> a | 458 | const :: forall a b . a -> b -> a |
diff --git a/testdata/complex.out b/testdata/complex.out index fa122fcc..1ae39c8d 100644 --- a/testdata/complex.out +++ b/testdata/complex.out | |||
@@ -4,84 +4,84 @@ data Repr :: Type where | |||
4 | Polar :: Repr | 4 | Polar :: Repr |
5 | data Complex :: Repr -> Type where | 5 | data Complex :: Repr -> Type where |
6 | Complex :: forall (a :: _) . Float -> Float -> Complex a | 6 | Complex :: forall (a :: _) . Float -> Float -> Complex a |
7 | repr = (\ @(a :: _) _ -> _rhs a) :: forall (b :: _) . Complex b -> Repr | 7 | repr :: forall (a :: _) . Complex a -> Repr |
8 | normal | 8 | repr = \ @(a :: _) _ -> _rhs a |
9 | = (\(a :: _) (b :: _) -> _rhs (Complex a b)) :: Float -> Float -> Complex Normal | 9 | normal :: Float -> Float -> Complex Normal |
10 | polar | 10 | normal = \(a :: _) (b :: _) -> _rhs (Complex a b) |
11 | = (\(a :: _) (b :: _) -> _rhs (Complex a b)) :: Float -> Float -> Complex Polar | 11 | polar :: Float -> Float -> Complex Polar |
12 | polar = \(a :: _) (b :: _) -> _rhs (Complex a b) | ||
13 | cabs :: forall (a :: _) . Complex a -> Float | ||
12 | cabs | 14 | cabs |
13 | = (\ @(a :: _) (b :: _) -> case'Repr | 15 | = \ @(a :: _) (b :: _) -> case'Repr |
14 | (\_ -> _) | 16 | (\_ -> _) |
15 | (case'Complex (\_ _ -> _) (\(c :: _) (d :: _) -> _rhs (sqrt (c * c + d * d))) b) | 17 | (case'Complex (\_ _ -> _) (\(c :: _) (d :: _) -> _rhs (sqrt (c * c + d * d))) b) |
16 | (case'Complex (\_ _ -> _) (\(e :: _) _ -> _rhs e) b) | 18 | (case'Complex (\_ _ -> _) (\(e :: _) _ -> _rhs e) b) |
17 | a) | 19 | a |
18 | :: forall (f :: _) . Complex f -> Float | 20 | toPolar :: Complex Normal -> Complex Polar |
19 | toPolar | 21 | toPolar |
20 | = (\(a :: _) -> case'Complex | 22 | = \(a :: _) -> case'Complex |
21 | (\_ _ -> _) | 23 | (\_ _ -> _) |
22 | (\(b :: _) (c :: _) -> _rhs | 24 | (\(b :: _) (c :: _) -> _rhs |
23 | \(d := _rhs (sqrt (b * b + c * c))) -> primIfThenElse | 25 | \(d := _rhs (sqrt (b * b + c * c))) -> primIfThenElse |
24 | (b > 0.0) | 26 | (b > 0.0) |
25 | (polar d (atan (c / b))) | 27 | (polar d (atan (c / b))) |
28 | (primIfThenElse | ||
29 | (b < 0.0 && c >= 0.0) | ||
30 | (polar d (atan (c / b) + pi)) | ||
26 | (primIfThenElse | 31 | (primIfThenElse |
27 | (b < 0.0 && c >= 0.0) | 32 | (b < 0.0 && c < 0.0) |
28 | (polar d (atan (c / b) + pi)) | 33 | (polar d (atan (c / b) - pi)) |
29 | (primIfThenElse | 34 | (primIfThenElse |
30 | (b < 0.0 && c < 0.0) | 35 | (b == 0.0 && c >= 0.0) |
31 | (polar d (atan (c / b) - pi)) | 36 | (polar d (pi / 2.0)) |
32 | (primIfThenElse | 37 | (primIfThenElse |
33 | (b == 0.0 && c >= 0.0) | 38 | (b == 0.0 && c < 0.0) |
34 | (polar d (pi / 2.0)) | 39 | (polar d (fromInt 0 - pi / 2.0)) |
35 | (primIfThenElse | 40 | undefined))))) |
36 | (b == 0.0 && c < 0.0) | 41 | a |
37 | (polar d (fromInt 0 - pi / 2.0)) | 42 | toNormal :: Complex Polar -> Complex Normal |
38 | undefined))))) | ||
39 | a) | ||
40 | :: Complex Normal -> Complex Polar | ||
41 | toNormal | 43 | toNormal |
42 | = (\(a :: _) -> case'Complex | 44 | = \(a :: _) -> case'Complex |
43 | (\_ _ -> _) | 45 | (\_ _ -> _) |
44 | (\(b :: _) (c :: _) -> _rhs (Complex (b * cos c) (b * sin c))) | 46 | (\(b :: _) (c :: _) -> _rhs (Complex (b * cos c) (b * sin c))) |
45 | a) | 47 | a |
46 | :: Complex Polar -> Complex Normal | ||
47 | it_should_fail = \(a :: _) -> case'Complex (\_ _ -> _) (\(b :: _) _ -> _rhs b) a | 48 | it_should_fail = \(a :: _) -> case'Complex (\_ _ -> _) (\(b :: _) _ -> _rhs b) a |
49 | add :: forall (a :: _) (b :: _) . Complex a -> Complex b -> Complex a | ||
48 | add | 50 | add |
49 | = (\ @(a :: _) @(b :: _) (c :: _) (d :: _) -> case'Repr | 51 | = \ @(a :: _) @(b :: _) (c :: _) (d :: _) -> case'Repr |
52 | (\_ -> _) | ||
53 | (case'Repr | ||
50 | (\_ -> _) | 54 | (\_ -> _) |
51 | (case'Repr | 55 | (case'Complex |
52 | (\_ -> _) | 56 | (\_ _ -> _) |
53 | (case'Complex | 57 | (\(e :: _) (f :: _) -> case'Complex |
54 | (\_ _ -> _) | 58 | (\_ _ -> _) |
55 | (\(e :: _) (f :: _) -> case'Complex | 59 | (\(g :: _) (h :: _) -> _rhs (Complex (e + g) (f + h))) |
56 | (\_ _ -> _) | 60 | d) |
57 | (\(g :: _) (h :: _) -> _rhs (Complex (e + g) (f + h))) | 61 | c) |
58 | d) | ||
59 | c) | ||
60 | (_rhs undefined) | ||
61 | b) | ||
62 | (_rhs undefined) | 62 | (_rhs undefined) |
63 | a) | 63 | b) |
64 | :: forall (i :: _) (j :: _) . Complex i -> Complex j -> Complex i | 64 | (_rhs undefined) |
65 | a | ||
66 | mul :: forall (a :: _) (b :: _) . Complex a -> Complex b -> Complex a | ||
65 | mul | 67 | mul |
66 | = (\ @(a :: _) @(b :: _) (c :: _) (d :: _) -> case'Repr | 68 | = \ @(a :: _) @(b :: _) (c :: _) (d :: _) -> case'Repr |
69 | (\_ -> _) | ||
70 | (case'Repr | ||
67 | (\_ -> _) | 71 | (\_ -> _) |
68 | (case'Repr | 72 | (case'Complex |
69 | (\_ -> _) | 73 | (\_ _ -> _) |
70 | (case'Complex | 74 | (\(e :: _) (f :: _) -> case'Complex |
71 | (\_ _ -> _) | 75 | (\_ _ -> _) |
72 | (\(e :: _) (f :: _) -> case'Complex | 76 | (\(g :: _) (h :: _) -> _rhs (Complex (e * g - f * h) (f * g + e * h))) |
73 | (\_ _ -> _) | 77 | d) |
74 | (\(g :: _) (h :: _) -> _rhs (Complex (e * g - f * h) (f * g + e * h))) | 78 | c) |
75 | d) | ||
76 | c) | ||
77 | (_rhs undefined) | ||
78 | b) | ||
79 | (_rhs undefined) | 79 | (_rhs undefined) |
80 | a) | 80 | b) |
81 | :: forall (i :: _) (j :: _) . Complex i -> Complex j -> Complex i | 81 | (_rhs undefined) |
82 | s | 82 | a |
83 | = (\(a :: _) -> _rhs (mul a a `add` a)) | 83 | s :: forall (a :: _) . Complex a -> Complex a |
84 | :: forall (b :: _) . Complex b -> Complex b | 84 | s = \(a :: _) -> _rhs (mul a a `add` a) |
85 | s4 = \(a :: _) -> _rhs (s (s (s (s a)))) | 85 | s4 = \(a :: _) -> _rhs (s (s (s (s a)))) |
86 | iter = _rhs s4 | 86 | iter = _rhs s4 |
87 | mandel = \(a :: _) -> _rhs (cabs (iter a) < 2.0) | 87 | mandel = \(a :: _) -> _rhs (cabs (iter a) < 2.0) |
diff --git a/testdata/language-features/basic-values/typesig01.out b/testdata/language-features/basic-values/typesig01.out index 0daccfb4..9936930a 100644 --- a/testdata/language-features/basic-values/typesig01.out +++ b/testdata/language-features/basic-values/typesig01.out | |||
@@ -1,6 +1,8 @@ | |||
1 | ------------ desugared source code | 1 | ------------ desugared source code |
2 | value1 = _rhs 'a' :: Char | 2 | value1 :: Char |
3 | value2 = _rhs 'a' :: Char | 3 | value1 = _rhs 'a' |
4 | value2 :: Char | ||
5 | value2 = _rhs 'a' | ||
4 | main is not found | 6 | main is not found |
5 | ------------ trace | 7 | ------------ trace |
6 | value1 :: Char | 8 | value1 :: Char |
diff --git a/testdata/language-features/basic-values/typesig03.out b/testdata/language-features/basic-values/typesig03.out index 59bcaa12..8a2f8bbb 100644 --- a/testdata/language-features/basic-values/typesig03.out +++ b/testdata/language-features/basic-values/typesig03.out | |||
@@ -1,10 +1,8 @@ | |||
1 | ------------ desugared source code | 1 | ------------ desugared source code |
2 | fun1 | 2 | fun1 :: forall (a :: _) (b :: _) (c :: _) . a -> b -> c -> HList '[] |
3 | = (\_ _ _ -> _rhs HNil) | 3 | fun1 = \_ _ _ -> _rhs HNil |
4 | :: forall (a :: _) (b :: _) (c :: _) . a -> b -> c -> HList '[] | 4 | fun2 :: forall (a :: _) (b :: _) (c :: _) . a -> b -> c -> HList '[] |
5 | fun2 | 5 | fun2 = \_ _ _ -> _rhs HNil |
6 | = (\_ _ _ -> _rhs HNil) | ||
7 | :: forall (a :: _) (b :: _) (c :: _) . a -> b -> c -> HList '[] | ||
8 | main is not found | 6 | main is not found |
9 | ------------ trace | 7 | ------------ trace |
10 | fun1 :: forall a b c . a -> b -> c -> () | 8 | fun1 :: forall a b c . a -> b -> c -> () |
diff --git a/testdata/language-features/basic-values/typesig04.out b/testdata/language-features/basic-values/typesig04.out index 15b67c43..0c98ffa1 100644 --- a/testdata/language-features/basic-values/typesig04.out +++ b/testdata/language-features/basic-values/typesig04.out | |||
@@ -1,10 +1,8 @@ | |||
1 | ------------ desugared source code | 1 | ------------ desugared source code |
2 | fun1 | 2 | fun1 :: forall (a :: _) (b :: _) (c :: _) . a -> (b -> c) -> HList '[] |
3 | = (\_ _ -> _rhs HNil) | 3 | fun1 = \_ _ -> _rhs HNil |
4 | :: forall (a :: _) (b :: _) (c :: _) . a -> (b -> c) -> HList '[] | 4 | fun2 :: forall (a :: _) (b :: _) (c :: _) . a -> (b -> c) -> HList '[] |
5 | fun2 | 5 | fun2 = \_ _ -> _rhs HNil |
6 | = (\_ _ -> _rhs HNil) | ||
7 | :: forall (a :: _) (b :: _) (c :: _) . a -> (b -> c) -> HList '[] | ||
8 | main is not found | 6 | main is not found |
9 | ------------ trace | 7 | ------------ trace |
10 | fun1 :: forall a b c . a -> (b -> c) -> () | 8 | fun1 :: forall a b c . a -> (b -> c) -> () |
diff --git a/testdata/language-features/basic-values/typesig05.out b/testdata/language-features/basic-values/typesig05.out index 06c14130..edceee72 100644 --- a/testdata/language-features/basic-values/typesig05.out +++ b/testdata/language-features/basic-values/typesig05.out | |||
@@ -3,8 +3,10 @@ funL = \(a :: _) _ -> _rhs a | |||
3 | funR = \_ (a :: _) -> _rhs a | 3 | funR = \_ (a :: _) -> _rhs a |
4 | value1 = _rhs (funL 'a' "b" :: Char) | 4 | value1 = _rhs (funL 'a' "b" :: Char) |
5 | value2 = _rhs (funR 'a' "b" :: String) | 5 | value2 = _rhs (funR 'a' "b" :: String) |
6 | value3 = _rhs (funL 'a' "b") :: Char | 6 | value3 :: Char |
7 | value4 = _rhs (funR 'a' "b") :: String | 7 | value3 = _rhs (funL 'a' "b") |
8 | value4 :: String | ||
9 | value4 = _rhs (funR 'a' "b") | ||
8 | main is not found | 10 | main is not found |
9 | ------------ trace | 11 | ------------ trace |
10 | funL :: forall a b . a -> b -> a | 12 | funL :: forall a b . a -> b -> a |
diff --git a/testdata/language-features/basic-values/typesig07.out b/testdata/language-features/basic-values/typesig07.out index 172e6819..07a8d0b9 100644 --- a/testdata/language-features/basic-values/typesig07.out +++ b/testdata/language-features/basic-values/typesig07.out | |||
@@ -1,10 +1,16 @@ | |||
1 | ------------ desugared source code | 1 | ------------ desugared source code |
2 | value1 = _rhs (fromInt 1) :: Int | 2 | value1 :: Int |
3 | value2 = _rhs (fromInt 2) :: Int | 3 | value1 = _rhs (fromInt 1) |
4 | value3 = _rhs (fromInt 3) :: Int | 4 | value2 :: Int |
5 | value4 = (\_ _ -> _rhs HNil) :: HList '[] -> HList '[] -> HList '[] | 5 | value2 = _rhs (fromInt 2) |
6 | (@@@) = (\_ _ -> _rhs HNil) :: HList '[] -> HList '[] -> HList '[] | 6 | value3 :: Int |
7 | value6 = (\_ _ -> _rhs HNil) :: HList '[] -> HList '[] -> HList '[] | 7 | value3 = _rhs (fromInt 3) |
8 | value4 :: HList '[] -> HList '[] -> HList '[] | ||
9 | value4 = \_ _ -> _rhs HNil | ||
10 | (@@@) :: HList '[] -> HList '[] -> HList '[] | ||
11 | (@@@) = \_ _ -> _rhs HNil | ||
12 | value6 :: HList '[] -> HList '[] -> HList '[] | ||
13 | value6 = \_ _ -> _rhs HNil | ||
8 | main is not found | 14 | main is not found |
9 | ------------ trace | 15 | ------------ trace |
10 | value1 :: Int | 16 | value1 :: Int |
diff --git a/testdata/language-features/basic-values/typesyn02.out b/testdata/language-features/basic-values/typesyn02.out index 44bc99c8..7713c92a 100644 --- a/testdata/language-features/basic-values/typesyn02.out +++ b/testdata/language-features/basic-values/typesyn02.out | |||
@@ -1,8 +1,7 @@ | |||
1 | ------------ desugared source code | 1 | ------------ desugared source code |
2 | 'MyUnit = _rhs ('HList []) | 2 | 'MyUnit = _rhs ('HList []) |
3 | fun | 3 | fun :: forall (a :: _) . a -> MyUnit -> MyUnit |
4 | = (\_ (a :: _) -> hlistNilCase _ (_rhs HNil) a) | 4 | fun = \_ (a :: _) -> hlistNilCase _ (_rhs HNil) a |
5 | :: forall (b :: _) . b -> MyUnit -> MyUnit | ||
6 | main is not found | 5 | main is not found |
7 | ------------ trace | 6 | ------------ trace |
8 | 'MyUnit :: Type | 7 | 'MyUnit :: Type |
diff --git a/testdata/language-features/module/import05.out b/testdata/language-features/module/import05.out index 96f021c2..4cb3a2f4 100644 --- a/testdata/language-features/module/import05.out +++ b/testdata/language-features/module/import05.out | |||
@@ -1,5 +1,6 @@ | |||
1 | ------------ desugared source code | 1 | ------------ desugared source code |
2 | x = _rhs hello :: String | 2 | x :: String |
3 | x = _rhs hello | ||
3 | main is not found | 4 | main is not found |
4 | ------------ trace | 5 | ------------ trace |
5 | x :: String | 6 | x :: String |
diff --git a/testdata/language-features/module/import08.out b/testdata/language-features/module/import08.out index 24006b18..ce0235db 100644 --- a/testdata/language-features/module/import08.out +++ b/testdata/language-features/module/import08.out | |||
@@ -1,8 +1,11 @@ | |||
1 | ------------ desugared source code | 1 | ------------ desugared source code |
2 | value = _rhs HNil | 2 | value = _rhs HNil |
3 | g = _rhs greeting :: Char | 3 | g :: Char |
4 | h = _rhs hello :: String | 4 | g = _rhs greeting |
5 | w = _rhs world :: String | 5 | h :: String |
6 | h = _rhs hello | ||
7 | w :: String | ||
8 | w = _rhs world | ||
6 | main is not found | 9 | main is not found |
7 | ------------ trace | 10 | ------------ trace |
8 | value :: () | 11 | value :: () |
diff --git a/testdata/language-features/module/import09.out b/testdata/language-features/module/import09.out index e7df6502..42b1de3a 100644 --- a/testdata/language-features/module/import09.out +++ b/testdata/language-features/module/import09.out | |||
@@ -1,7 +1,6 @@ | |||
1 | ------------ desugared source code | 1 | ------------ desugared source code |
2 | fun | 2 | fun :: forall (a :: _) . a -> MyUnit -> MyUnit |
3 | = (\_ (a :: _) -> hlistNilCase _ (_rhs HNil) a) | 3 | fun = \_ (a :: _) -> hlistNilCase _ (_rhs HNil) a |
4 | :: forall (b :: _) . b -> MyUnit -> MyUnit | ||
5 | main is not found | 4 | main is not found |
6 | ------------ trace | 5 | ------------ trace |
7 | fun :: forall a . a -> () -> () | 6 | fun :: forall a . a -> () -> () |
diff --git a/testdata/performance/Material.out b/testdata/performance/Material.out index ea52e563..a9cebf12 100644 --- a/testdata/performance/Material.out +++ b/testdata/performance/Material.out | |||
@@ -1,5 +1,6 @@ | |||
1 | ------------ desugared source code | 1 | ------------ desugared source code |
2 | identityLight = _rhs (fromInt 1) :: Float | 2 | identityLight :: Float |
3 | identityLight = _rhs (fromInt 1) | ||
3 | data Entity :: Type where | 4 | data Entity :: Type where |
4 | Entity | 5 | Entity |
5 | :: Vec (fromInt 4) Float | 6 | :: Vec (fromInt 4) Float |
@@ -164,21 +165,21 @@ saTextureUniform | |||
164 | (\_ -> _) | 165 | (\_ -> _) |
165 | (\_ _ _ _ _ _ _ _ _ _ (b :: _) -> _rhs b) | 166 | (\_ _ _ _ _ _ _ _ _ _ (b :: _) -> _rhs b) |
166 | a | 167 | a |
168 | defaultStageAttrs :: StageAttrs | ||
167 | defaultStageAttrs | 169 | defaultStageAttrs |
168 | = _rhs | 170 | = _rhs |
169 | (StageAttrs | 171 | (StageAttrs |
170 | Nothing | 172 | Nothing |
171 | RGB_Undefined | 173 | RGB_Undefined |
172 | A_Identity | 174 | A_Identity |
173 | TG_Undefined | 175 | TG_Undefined |
174 | [] | 176 | [] |
175 | ST_WhiteImage | 177 | ST_WhiteImage |
176 | True | 178 | True |
177 | D_Lequal | 179 | D_Lequal |
178 | Nothing | 180 | Nothing |
179 | False | 181 | False |
180 | "") | 182 | "") |
181 | :: StageAttrs | ||
182 | data CommonAttrs :: Type where | 183 | data CommonAttrs :: Type where |
183 | CommonAttrs | 184 | CommonAttrs |
184 | :: HList '[] | 185 | :: HList '[] |
@@ -248,22 +249,22 @@ caIsSky | |||
248 | (\_ -> _) | 249 | (\_ -> _) |
249 | (\_ _ _ _ _ _ _ _ _ _ _ (b :: _) -> _rhs b) | 250 | (\_ _ _ _ _ _ _ _ _ _ _ (b :: _) -> _rhs b) |
250 | a | 251 | a |
252 | defaultCommonAttrs :: CommonAttrs | ||
251 | defaultCommonAttrs | 253 | defaultCommonAttrs |
252 | = _rhs | 254 | = _rhs |
253 | (CommonAttrs | 255 | (CommonAttrs |
254 | HNil | 256 | HNil |
255 | HNil | 257 | HNil |
256 | False | 258 | False |
257 | (fromInt 0) | 259 | (fromInt 0) |
258 | False | 260 | False |
259 | False | 261 | False |
260 | CT_FrontSided | 262 | CT_FrontSided |
261 | [] | 263 | [] |
262 | False | 264 | False |
263 | False | 265 | False |
264 | [] | 266 | [] |
265 | False) | 267 | False) |
266 | :: CommonAttrs | ||
267 | main is not found | 268 | main is not found |
268 | ------------ trace | 269 | ------------ trace |
269 | identityLight :: Float | 270 | identityLight :: Float |
diff --git a/testdata/traceTest.out b/testdata/traceTest.out index be79b652..d796730f 100644 --- a/testdata/traceTest.out +++ b/testdata/traceTest.out | |||
@@ -2,7 +2,8 @@ | |||
2 | id = \(a :: _) -> _rhs a | 2 | id = \(a :: _) -> _rhs a |
3 | data X (_ :: Type) (_ :: _a) :: Type where | 3 | data X (_ :: Type) (_ :: _a) :: Type where |
4 | 4 | ||
5 | x = _rhs undefined :: X \(a :: _) (b :: _) -> HList (a : b : '[]) | 5 | x :: X \(a :: _) (b :: _) -> HList (a : b : '[]) |
6 | x = _rhs undefined | ||
6 | main is not found | 7 | main is not found |
7 | ------------ trace | 8 | ------------ trace |
8 | id :: forall a . a -> a | 9 | id :: forall a . a -> a |
diff --git a/testdata/typeclass.out b/testdata/typeclass.out index dcc242da..b74a7e31 100644 --- a/testdata/typeclass.out +++ b/testdata/typeclass.out | |||
@@ -7,22 +7,22 @@ infixr 2 || | |||
7 | not = \(a :: _) -> case'Bool (\_ -> _) (_rhs True) (_rhs False) a | 7 | not = \(a :: _) -> case'Bool (\_ -> _) (_rhs True) (_rhs False) a |
8 | (&&) = \(a :: _) (b :: _) -> case'Bool (\_ -> _) (_rhs False) (_rhs b) a | 8 | (&&) = \(a :: _) (b :: _) -> case'Bool (\_ -> _) (_rhs False) (_rhs b) a |
9 | (||) = \(a :: _) (b :: _) -> case'Bool (\_ -> _) (_rhs b) (_rhs True) a | 9 | (||) = \(a :: _) (b :: _) -> case'Bool (\_ -> _) (_rhs b) (_rhs True) a |
10 | 'Eq :: Type -> Type | ||
10 | 'Eq | 11 | 'Eq |
11 | = (\(a :: _) -> match'Bool | 12 | = \(a :: _) -> match'Bool |
12 | (\_ -> _) | 13 | (\_ -> _) |
13 | (_rhs 'Unit) | 14 | (_rhs 'Unit) |
14 | a | 15 | a |
15 | (_rhs ('Empty "no instance of 'Eq on ???"))) | 16 | (_rhs ('Empty "no instance of 'Eq on ???")) |
16 | :: Type -> Type | 17 | (==) :: forall a . Eq a => a -> a -> Bool |
17 | (==) | 18 | (==) |
18 | = (\ @a @_ -> match'Bool | 19 | = \ @a @_ -> match'Bool |
19 | (\_ -> _) | 20 | (\_ -> _) |
20 | (_rhs | 21 | (_rhs |
21 | \(b | 22 | \(b |
22 | := \(c :: _) (d :: _) -> case'Bool (\_ -> _) (_rhs (not d)) (_rhs d) c) -> b) | 23 | := \(c :: _) (d :: _) -> case'Bool (\_ -> _) (_rhs (not d)) (_rhs d) c) -> b) |
23 | a | 24 | a |
24 | (_rhs undefined)) | 25 | (_rhs undefined) |
25 | :: forall e . Eq e => e -> e -> Bool | ||
26 | (/=) = \(a :: _) (b :: _) -> _rhs (not (a == b)) | 26 | (/=) = \(a :: _) (b :: _) -> _rhs (not (a == b)) |
27 | main is not found | 27 | main is not found |
28 | ------------ trace | 28 | ------------ trace |
diff --git a/testdata/zip01.out b/testdata/zip01.out index 8ba64e69..582866bb 100644 --- a/testdata/zip01.out +++ b/testdata/zip01.out | |||
@@ -1,15 +1,15 @@ | |||
1 | ------------ desugared source code | 1 | ------------ desugared source code |
2 | zip2 :: forall (a :: _) (b :: _) . [a] -> [b] -> [HList (a : b : '[])] | ||
2 | zip2 | 3 | zip2 |
3 | = (\(a :: _) (b :: _) -> case'List | 4 | = \(a :: _) (b :: _) -> case'List |
5 | (\_ -> _) | ||
6 | (_rhs []) | ||
7 | (\(c :: _) (d :: _) -> case'List | ||
4 | (\_ -> _) | 8 | (\_ -> _) |
5 | (_rhs []) | 9 | (_rhs []) |
6 | (\(c :: _) (d :: _) -> case'List | 10 | (\(e :: _) (f :: _) -> _rhs (HCons c (HCons e HNil) : zip2 d f)) |
7 | (\_ -> _) | 11 | b) |
8 | (_rhs []) | 12 | a |
9 | (\(e :: _) (f :: _) -> _rhs (HCons c (HCons e HNil) : zip2 d f)) | ||
10 | b) | ||
11 | a) | ||
12 | :: forall (g :: _) (h :: _) . [g] -> [h] -> [HList (g : h : '[])] | ||
13 | main is not found | 13 | main is not found |
14 | ------------ trace | 14 | ------------ trace |
15 | zip2 :: forall a b . [a] -> [b] -> [(a, b)] | 15 | zip2 :: forall a b . [a] -> [b] -> [(a, b)] |