summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/LambdaCube/Compiler/CoreToIR.hs12
-rw-r--r--testdata/editor-examples/LambdaCube.out4
-rw-r--r--testdata/editor-examples/LambdaCube2.out4
-rw-r--r--testdata/editor-examples/RecLC.out4
-rw-r--r--testdata/example08.out96
5 files changed, 62 insertions, 58 deletions
diff --git a/src/LambdaCube/Compiler/CoreToIR.hs b/src/LambdaCube/Compiler/CoreToIR.hs
index 29a2ab39..ac78a6d0 100644
--- a/src/LambdaCube/Compiler/CoreToIR.hs
+++ b/src/LambdaCube/Compiler/CoreToIR.hs
@@ -816,6 +816,8 @@ type Ty = ExpTV
816tyOf :: ExpTV -> Ty 816tyOf :: ExpTV -> Ty
817tyOf (ExpTV _ t vs) = t .@ vs 817tyOf (ExpTV _ t vs) = t .@ vs
818 818
819expOf (ExpTV x _ _) = x
820
819mapVal f (ExpTV a b c) = ExpTV (f a) b c 821mapVal f (ExpTV a b c) = ExpTV (f a) b c
820 822
821toExp :: ExpType -> ExpTV 823toExp :: ExpType -> ExpTV
@@ -858,17 +860,19 @@ mkApp (ExpTV (Neut (I.App_ a b)) et vs) = Just (ExpTV (Neut a) t vs, head $ chai
858mkApp _ = Nothing 860mkApp _ = Nothing
859 861
860mkFunc r@(ExpTV (I.Func (show -> n) def nt xs) ty vs) | all (supType . tyOf) (r: xs') && n `notElem` ["typeAnn"] && all validChar n 862mkFunc r@(ExpTV (I.Func (show -> n) def nt xs) ty vs) | all (supType . tyOf) (r: xs') && n `notElem` ["typeAnn"] && all validChar n
861 = Just (untick n, toExp (def, nt), tyOf r, xs') 863 = Just (untick n +++ intercalate "_" (map (filter isAlphaNum . removeEscs . ppShow) hs), toExp (foldl app_ def hs, foldl appTy nt hs), tyOf r, xs')
862 where 864 where
863 xs' = chain vs nt $ reverse xs 865 a +++ [] = a
866 a +++ b = a ++ "_" ++ b
867 (map (expOf . snd) -> hs, map snd -> xs') = span ((==Hidden) . fst) $ chain' vs nt $ reverse xs
864 validChar = isAlphaNum 868 validChar = isAlphaNum
865mkFunc _ = Nothing 869mkFunc _ = Nothing
866 870
867chain vs t@(I.Pi Hidden at y) (a: as) = chain vs (appTy t a) as 871chain vs t@(I.Pi Hidden at y) (a: as) = chain vs (appTy t a) as
868chain vs t xs = chain' vs t xs 872chain vs t xs = map snd $ chain' vs t xs
869 873
870chain' vs t [] = [] 874chain' vs t [] = []
871chain' vs t@(I.Pi b at y) (a: as) = ExpTV a at vs: chain' vs (appTy t a) as 875chain' vs t@(I.Pi b at y) (a: as) = (b, ExpTV a at vs): chain' vs (appTy t a) as
872chain' vs t _ = error $ "chain: " ++ show t 876chain' vs t _ = error $ "chain: " ++ show t
873 877
874mkTVar i (ExpTV t _ vs) = ExpTV (I.Var i) t vs 878mkTVar i (ExpTV t _ vs) = ExpTV (I.Var i) t vs
diff --git a/testdata/editor-examples/LambdaCube.out b/testdata/editor-examples/LambdaCube.out
index 313c1fb5..d4438455 100644
--- a/testdata/editor-examples/LambdaCube.out
+++ b/testdata/editor-examples/LambdaCube.out
@@ -76,7 +76,7 @@ Pipeline
76 ,(dot (z0,vec2 (0.5,-0.5))) + (0.4) 76 ,(dot (z0,vec2 (0.5,-0.5))) + (0.4)
77 ,((z0).y) > (0.75) ? 0.0 : 1.0); 77 ,((z0).y) > (0.75) ? 0.0 : 1.0);
78 } 78 }
79 vec4 rightSide(vec2 z0) { 79 vec4 rightSide_2(vec2 z0) {
80 return vec4 (((z0).x) * ((z0).x) 80 return vec4 (((z0).x) * ((z0).x)
81 ,1.0 81 ,1.0
82 ,((1.0) - ((z0).x)) * ((1.0) - ((z0).x)) 82 ,((1.0) - ((z0).x)) * ((1.0) - ((z0).x))
@@ -90,7 +90,7 @@ Pipeline
90 (z0,vec2 (1.0,-1.0))) < (0.0)) ? 0.0 : 1.0); 90 (z0,vec2 (1.0,-1.0))) < (0.0)) ? 0.0 : 1.0);
91 } 91 }
92 void main() { 92 void main() {
93 f0 = (abs ((vo1).x)) > (0.99999) ? rightSide 93 f0 = (abs ((vo1).x)) > (0.99999) ? rightSide_2
94 (((((vo1).yz) * (sign ((vo1).x))) * (0.5)) + (0.5)) : (abs 94 (((((vo1).yz) * (sign ((vo1).x))) * (0.5)) + (0.5)) : (abs
95 ((vo1).y)) > (0.99999) ? topSide (((((vo1).zx) * (sign 95 ((vo1).y)) > (0.99999) ? topSide (((((vo1).zx) * (sign
96 ((vo1).y))) * (0.5)) + (0.5)) : (abs 96 ((vo1).y))) * (0.5)) + (0.5)) : (abs
diff --git a/testdata/editor-examples/LambdaCube2.out b/testdata/editor-examples/LambdaCube2.out
index 22c41e7e..a5aae340 100644
--- a/testdata/editor-examples/LambdaCube2.out
+++ b/testdata/editor-examples/LambdaCube2.out
@@ -49,7 +49,7 @@ Pipeline
49 uniform float Time; 49 uniform float Time;
50 smooth in vec4 vo1; 50 smooth in vec4 vo1;
51 out vec4 f0; 51 out vec4 f0;
52 float len2(vec4 z0) { 52 float len2_Float_TT_4_TT(vec4 z0) {
53 return ((((z0).x) * ((z0).x)) + (((z0).y) * ((z0).y))) + (((z0).z) * ((z0).z)); 53 return ((((z0).x) * ((z0).x)) + (((z0).y) * ((z0).y))) + (((z0).z) * ((z0).z));
54 } 54 }
55 void main() { 55 void main() {
@@ -57,7 +57,7 @@ Pipeline
57 (((((vo1).y) - ((vo1).x)) + ((vo1).z)) - (1.0))) > (0.25))) && (((((((vo1).y) + ((vo1).x)) - ((vo1).z)) > (1.0)) || ((abs 57 (((((vo1).y) - ((vo1).x)) + ((vo1).z)) - (1.0))) > (0.25))) && (((((((vo1).y) + ((vo1).x)) - ((vo1).z)) > (1.0)) || ((abs
58 (((((vo1).y) + ((vo1).x)) + ((vo1).z)) - (1.0))) > (0.25))) && (((((((vo1).y) - ((vo1).x)) - ((vo1).z)) > (1.0)) || ((abs 58 (((((vo1).y) + ((vo1).x)) + ((vo1).z)) - (1.0))) > (0.25))) && (((((((vo1).y) - ((vo1).x)) - ((vo1).z)) > (1.0)) || ((abs
59 (((((vo1).y) + ((vo1).x)) - ((vo1).z)) - (1.0))) > (0.25))) && (((((((vo1).y) - ((vo1).x)) + ((vo1).z)) > (1.0)) || ((abs 59 (((((vo1).y) + ((vo1).x)) - ((vo1).z)) - (1.0))) > (0.25))) && (((((((vo1).y) - ((vo1).x)) + ((vo1).z)) > (1.0)) || ((abs
60 (((((vo1).y) - ((vo1).x)) - ((vo1).z)) - (1.0))) > (0.25))) && ((len2 60 (((((vo1).y) - ((vo1).x)) - ((vo1).z)) - (1.0))) > (0.25))) && ((len2_Float_TT_4_TT
61 (sin ((vo1) * (20.0)))) > (abs ((3.0) * (sin 61 (sin ((vo1) * (20.0)))) > (abs ((3.0) * (sin
62 ((1.0) * (Time))))))))))) discard; 62 ((1.0) * (Time))))))))))) discard;
63 f0 = vo1; 63 f0 = vo1;
diff --git a/testdata/editor-examples/RecLC.out b/testdata/editor-examples/RecLC.out
index ca91c9c1..e8e220ca 100644
--- a/testdata/editor-examples/RecLC.out
+++ b/testdata/editor-examples/RecLC.out
@@ -154,7 +154,7 @@ Pipeline
154 uniform float Time; 154 uniform float Time;
155 smooth in vec4 vo1; 155 smooth in vec4 vo1;
156 out vec4 f0; 156 out vec4 f0;
157 float len2(vec4 z0) { 157 float len2_Float_TT_4_TT(vec4 z0) {
158 return ((((z0).x) * ((z0).x)) + (((z0).y) * ((z0).y))) + (((z0).z) * ((z0).z)); 158 return ((((z0).x) * ((z0).x)) + (((z0).y) * ((z0).y))) + (((z0).z) * ((z0).z));
159 } 159 }
160 void main() { 160 void main() {
@@ -162,7 +162,7 @@ Pipeline
162 (((((vo1).y) - ((vo1).x)) + ((vo1).z)) - (1.0))) > (0.25))) && (((((((vo1).y) + ((vo1).x)) - ((vo1).z)) > (1.0)) || ((abs 162 (((((vo1).y) - ((vo1).x)) + ((vo1).z)) - (1.0))) > (0.25))) && (((((((vo1).y) + ((vo1).x)) - ((vo1).z)) > (1.0)) || ((abs
163 (((((vo1).y) + ((vo1).x)) + ((vo1).z)) - (1.0))) > (0.25))) && (((((((vo1).y) - ((vo1).x)) - ((vo1).z)) > (1.0)) || ((abs 163 (((((vo1).y) + ((vo1).x)) + ((vo1).z)) - (1.0))) > (0.25))) && (((((((vo1).y) - ((vo1).x)) - ((vo1).z)) > (1.0)) || ((abs
164 (((((vo1).y) + ((vo1).x)) - ((vo1).z)) - (1.0))) > (0.25))) && (((((((vo1).y) - ((vo1).x)) + ((vo1).z)) > (1.0)) || ((abs 164 (((((vo1).y) + ((vo1).x)) - ((vo1).z)) - (1.0))) > (0.25))) && (((((((vo1).y) - ((vo1).x)) + ((vo1).z)) > (1.0)) || ((abs
165 (((((vo1).y) - ((vo1).x)) - ((vo1).z)) - (1.0))) > (0.25))) && ((len2 165 (((((vo1).y) - ((vo1).x)) - ((vo1).z)) - (1.0))) > (0.25))) && ((len2_Float_TT_4_TT
166 (sin ((vo1) * (20.0)))) > (abs ((3.0) * (sin 166 (sin ((vo1) * (20.0)))) > (abs ((3.0) * (sin
167 ((1.0) * (Time))))))))))) discard; 167 ((1.0) * (Time))))))))))) discard;
168 f0 = vo1; 168 f0 = vo1;
diff --git a/testdata/example08.out b/testdata/example08.out
index 9cb32d49..ca4354f3 100644
--- a/testdata/example08.out
+++ b/testdata/example08.out
@@ -47,19 +47,19 @@ Pipeline
47 vec4 scale(float z0,vec4 z1) { 47 vec4 scale(float z0,vec4 z1) {
48 return (z1) * (vec4 (z0,z0,z0,1.0)); 48 return (z1) * (vec4 (z0,z0,z0,1.0));
49 } 49 }
50 vec4 trMat(mat4 z0,vec4 z1) { 50 vec4 trMat_4_4_Float(mat4 z0,vec4 z1) {
51 return (z0) * (z1); 51 return (z0) * (z1);
52 } 52 }
53 vec4 trX(float z0,vec4 z1) { 53 vec4 trX(float z0,vec4 z1) {
54 return (vec4 (z0,0.0,0.0,0.0)) + (z1); 54 return (vec4 (z0,0.0,0.0,0.0)) + (z1);
55 } 55 }
56 void main() { 56 void main() {
57 gl_Position = trMat 57 gl_Position = trMat_4_4_Float
58 (rotMatrixZ ((Time) * (2.0)) 58 (rotMatrixZ ((Time) * (2.0))
59 ,(MVP) * (trX 59 ,(MVP) * (trX ((1.0) + ((sin (Time)) * (0.1))
60 ((1.0) + ((sin (Time)) * (0.1)) 60 ,scale (4.0e-2
61 ,scale 61 ,trMat_4_4_Float
62 (4.0e-2,trMat (rotMatrixX (((Time) * (2.0)) * (2.0)),vi1))))); 62 (rotMatrixX (((Time) * (2.0)) * (2.0)),vi1)))));
63 vo1 = vi1; 63 vo1 = vi1;
64 } 64 }
65 """ 65 """
@@ -110,19 +110,19 @@ Pipeline
110 vec4 scale(float z0,vec4 z1) { 110 vec4 scale(float z0,vec4 z1) {
111 return (z1) * (vec4 (z0,z0,z0,1.0)); 111 return (z1) * (vec4 (z0,z0,z0,1.0));
112 } 112 }
113 vec4 trMat(mat4 z0,vec4 z1) { 113 vec4 trMat_4_4_Float(mat4 z0,vec4 z1) {
114 return (z0) * (z1); 114 return (z0) * (z1);
115 } 115 }
116 vec4 trX(float z0,vec4 z1) { 116 vec4 trX(float z0,vec4 z1) {
117 return (vec4 (z0,0.0,0.0,0.0)) + (z1); 117 return (vec4 (z0,0.0,0.0,0.0)) + (z1);
118 } 118 }
119 void main() { 119 void main() {
120 gl_Position = trMat 120 gl_Position = trMat_4_4_Float
121 (rotMatrixZ ((Time) * (1.0)) 121 (rotMatrixZ ((Time) * (1.0))
122 ,(MVP) * (trX 122 ,(MVP) * (trX ((0.5) + ((sin (Time)) * (0.1))
123 ((0.5) + ((sin (Time)) * (0.1)) 123 ,scale (4.0e-2
124 ,scale 124 ,trMat_4_4_Float
125 (4.0e-2,trMat (rotMatrixX (((Time) * (2.0)) * (1.0)),vi1))))); 125 (rotMatrixX (((Time) * (2.0)) * (1.0)),vi1)))));
126 vo1 = vi1; 126 vo1 = vi1;
127 } 127 }
128 """ 128 """
@@ -173,19 +173,19 @@ Pipeline
173 vec4 scale(float z0,vec4 z1) { 173 vec4 scale(float z0,vec4 z1) {
174 return (z1) * (vec4 (z0,z0,z0,1.0)); 174 return (z1) * (vec4 (z0,z0,z0,1.0));
175 } 175 }
176 vec4 trMat(mat4 z0,vec4 z1) { 176 vec4 trMat_4_4_Float(mat4 z0,vec4 z1) {
177 return (z0) * (z1); 177 return (z0) * (z1);
178 } 178 }
179 vec4 trX(float z0,vec4 z1) { 179 vec4 trX(float z0,vec4 z1) {
180 return (vec4 (z0,0.0,0.0,0.0)) + (z1); 180 return (vec4 (z0,0.0,0.0,0.0)) + (z1);
181 } 181 }
182 void main() { 182 void main() {
183 gl_Position = trMat 183 gl_Position = trMat_4_4_Float
184 (rotMatrixZ ((Time) * (0.0)) 184 (rotMatrixZ ((Time) * (0.0))
185 ,(MVP) * (trX 185 ,(MVP) * (trX ((0.0) + ((sin (Time)) * (0.1))
186 ((0.0) + ((sin (Time)) * (0.1)) 186 ,scale (4.0e-2
187 ,scale 187 ,trMat_4_4_Float
188 (4.0e-2,trMat (rotMatrixX (((Time) * (2.0)) * (0.0)),vi1))))); 188 (rotMatrixX (((Time) * (2.0)) * (0.0)),vi1)))));
189 vo1 = vi1; 189 vo1 = vi1;
190 } 190 }
191 """ 191 """
@@ -236,19 +236,19 @@ Pipeline
236 vec4 scale(float z0,vec4 z1) { 236 vec4 scale(float z0,vec4 z1) {
237 return (z1) * (vec4 (z0,z0,z0,1.0)); 237 return (z1) * (vec4 (z0,z0,z0,1.0));
238 } 238 }
239 vec4 trMat(mat4 z0,vec4 z1) { 239 vec4 trMat_4_4_Float(mat4 z0,vec4 z1) {
240 return (z0) * (z1); 240 return (z0) * (z1);
241 } 241 }
242 vec4 trX(float z0,vec4 z1) { 242 vec4 trX(float z0,vec4 z1) {
243 return (vec4 (z0,0.0,0.0,0.0)) + (z1); 243 return (vec4 (z0,0.0,0.0,0.0)) + (z1);
244 } 244 }
245 void main() { 245 void main() {
246 gl_Position = trMat 246 gl_Position = trMat_4_4_Float
247 (rotMatrixZ ((Time) * (-1.0)) 247 (rotMatrixZ ((Time) * (-1.0))
248 ,(MVP) * (trX 248 ,(MVP) * (trX ((-0.5) + ((sin (Time)) * (0.1))
249 ((-0.5) + ((sin (Time)) * (0.1)) 249 ,scale (4.0e-2
250 ,scale 250 ,trMat_4_4_Float
251 (4.0e-2,trMat (rotMatrixX (((Time) * (2.0)) * (-1.0)),vi1))))); 251 (rotMatrixX (((Time) * (2.0)) * (-1.0)),vi1)))));
252 vo1 = vi1; 252 vo1 = vi1;
253 } 253 }
254 """ 254 """
@@ -299,19 +299,19 @@ Pipeline
299 vec4 scale(float z0,vec4 z1) { 299 vec4 scale(float z0,vec4 z1) {
300 return (z1) * (vec4 (z0,z0,z0,1.0)); 300 return (z1) * (vec4 (z0,z0,z0,1.0));
301 } 301 }
302 vec4 trMat(mat4 z0,vec4 z1) { 302 vec4 trMat_4_4_Float(mat4 z0,vec4 z1) {
303 return (z0) * (z1); 303 return (z0) * (z1);
304 } 304 }
305 vec4 trX(float z0,vec4 z1) { 305 vec4 trX(float z0,vec4 z1) {
306 return (vec4 (z0,0.0,0.0,0.0)) + (z1); 306 return (vec4 (z0,0.0,0.0,0.0)) + (z1);
307 } 307 }
308 void main() { 308 void main() {
309 gl_Position = trMat 309 gl_Position = trMat_4_4_Float
310 (rotMatrixZ ((Time) * (0.75)) 310 (rotMatrixZ ((Time) * (0.75))
311 ,(MVP) * (trX 311 ,(MVP) * (trX ((0.375) + ((sin (Time)) * (0.1))
312 ((0.375) + ((sin (Time)) * (0.1)) 312 ,scale (4.0e-2
313 ,scale 313 ,trMat_4_4_Float
314 (4.0e-2,trMat (rotMatrixX (((Time) * (2.0)) * (0.75)),vi1))))); 314 (rotMatrixX (((Time) * (2.0)) * (0.75)),vi1)))));
315 vo1 = vi1; 315 vo1 = vi1;
316 } 316 }
317 """ 317 """
@@ -362,19 +362,19 @@ Pipeline
362 vec4 scale(float z0,vec4 z1) { 362 vec4 scale(float z0,vec4 z1) {
363 return (z1) * (vec4 (z0,z0,z0,1.0)); 363 return (z1) * (vec4 (z0,z0,z0,1.0));
364 } 364 }
365 vec4 trMat(mat4 z0,vec4 z1) { 365 vec4 trMat_4_4_Float(mat4 z0,vec4 z1) {
366 return (z0) * (z1); 366 return (z0) * (z1);
367 } 367 }
368 vec4 trX(float z0,vec4 z1) { 368 vec4 trX(float z0,vec4 z1) {
369 return (vec4 (z0,0.0,0.0,0.0)) + (z1); 369 return (vec4 (z0,0.0,0.0,0.0)) + (z1);
370 } 370 }
371 void main() { 371 void main() {
372 gl_Position = trMat 372 gl_Position = trMat_4_4_Float
373 (rotMatrixZ ((Time) * (0.3)) 373 (rotMatrixZ ((Time) * (0.3))
374 ,(MVP) * (trX 374 ,(MVP) * (trX ((0.15) + ((sin (Time)) * (0.1))
375 ((0.15) + ((sin (Time)) * (0.1)) 375 ,scale (4.0e-2
376 ,scale 376 ,trMat_4_4_Float
377 (4.0e-2,trMat (rotMatrixX (((Time) * (2.0)) * (0.3)),vi1))))); 377 (rotMatrixX (((Time) * (2.0)) * (0.3)),vi1)))));
378 vo1 = vi1; 378 vo1 = vi1;
379 } 379 }
380 """ 380 """
@@ -425,19 +425,19 @@ Pipeline
425 vec4 scale(float z0,vec4 z1) { 425 vec4 scale(float z0,vec4 z1) {
426 return (z1) * (vec4 (z0,z0,z0,1.0)); 426 return (z1) * (vec4 (z0,z0,z0,1.0));
427 } 427 }
428 vec4 trMat(mat4 z0,vec4 z1) { 428 vec4 trMat_4_4_Float(mat4 z0,vec4 z1) {
429 return (z0) * (z1); 429 return (z0) * (z1);
430 } 430 }
431 vec4 trX(float z0,vec4 z1) { 431 vec4 trX(float z0,vec4 z1) {
432 return (vec4 (z0,0.0,0.0,0.0)) + (z1); 432 return (vec4 (z0,0.0,0.0,0.0)) + (z1);
433 } 433 }
434 void main() { 434 void main() {
435 gl_Position = trMat 435 gl_Position = trMat_4_4_Float
436 (rotMatrixZ ((Time) * (0.5)) 436 (rotMatrixZ ((Time) * (0.5))
437 ,(MVP) * (trX 437 ,(MVP) * (trX ((0.25) + ((sin (Time)) * (0.1))
438 ((0.25) + ((sin (Time)) * (0.1)) 438 ,scale (4.0e-2
439 ,scale 439 ,trMat_4_4_Float
440 (4.0e-2,trMat (rotMatrixX (((Time) * (2.0)) * (0.5)),vi1))))); 440 (rotMatrixX (((Time) * (2.0)) * (0.5)),vi1)))));
441 vo1 = vi1; 441 vo1 = vi1;
442 } 442 }
443 """ 443 """
@@ -488,19 +488,19 @@ Pipeline
488 vec4 scale(float z0,vec4 z1) { 488 vec4 scale(float z0,vec4 z1) {
489 return (z1) * (vec4 (z0,z0,z0,1.0)); 489 return (z1) * (vec4 (z0,z0,z0,1.0));
490 } 490 }
491 vec4 trMat(mat4 z0,vec4 z1) { 491 vec4 trMat_4_4_Float(mat4 z0,vec4 z1) {
492 return (z0) * (z1); 492 return (z0) * (z1);
493 } 493 }
494 vec4 trX(float z0,vec4 z1) { 494 vec4 trX(float z0,vec4 z1) {
495 return (vec4 (z0,0.0,0.0,0.0)) + (z1); 495 return (vec4 (z0,0.0,0.0,0.0)) + (z1);
496 } 496 }
497 void main() { 497 void main() {
498 gl_Position = trMat 498 gl_Position = trMat_4_4_Float
499 (rotMatrixZ ((Time) * (-0.5)) 499 (rotMatrixZ ((Time) * (-0.5))
500 ,(MVP) * (trX 500 ,(MVP) * (trX ((-0.25) + ((sin (Time)) * (0.1))
501 ((-0.25) + ((sin (Time)) * (0.1)) 501 ,scale (4.0e-2
502 ,scale 502 ,trMat_4_4_Float
503 (4.0e-2,trMat (rotMatrixX (((Time) * (2.0)) * (-0.5)),vi1))))); 503 (rotMatrixX (((Time) * (2.0)) * (-0.5)),vi1)))));
504 vo1 = vi1; 504 vo1 = vi1;
505 } 505 }
506 """ 506 """
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-29 16:34:39 +0000