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)] |