1%if false
2  Copyright (c) 2009 ETH Zurich.
3  All rights reserved.
4
5  This file is distributed under the terms in the attached LICENSE file.
6  If you do not find this file, copies can be found by writing to:
7  ETH Zurich D-INFK, Haldeneggsteig 4, CH-8092 Zurich. Attn: Systems Group.
8%endif
9
10%include polycode.fmt
11
12%if false
13
14> {-# OPTIONS_GHC -fglasgow-exts #-}
15
16%endif
17
18%if false
19
20> module Main where
21
22> import Debug.Trace
23
24> import Semantics
25> import Expressions
26
27> import Arrays
28> import Conditionals
29> import Enumerations
30> import Functions
31> import References
32> import Strings
33> import Structures
34> import Typedef
35> import Unions
36
37> import Libc.Assert
38
39> import Run
40> import Compile
41
42%endif
43
44
45
46\section{Example}
47
48%if false
49
50> {-         
51
52> test3 :: Semantics (Ref :+: Conditionals) PureExpr
53> test3 = 
54>     do 
55>       ifc (do return (int32 1 .==. int32 0) :: Semantics Conditionals PureExpr)
56>           (do 
57>            x <- newRef $ int32 1
58>            xv <- readRef x
59>            writeRef x (xv .*. int32 2) :: Semantics (Ref :+: Conditionals) PureExpr)
60>          (do return Void :: Semantics Conditionals PureExpr)
61
62     
63
64> test5 :: [PureExpr] -> Semantics (Bot :+: Ref :+: Def) PureExpr
65> test5 (x : []) =
66>     do
67>       xv <- readRef x
68>       xvv <- readRef xv
69>       writeRef xv (xvv .+. int32 1)
70>       returnc $ int32 0
71
72> test7 :: [PureExpr] -> Semantics (Bot :+: Ref :+: Def) PureExpr
73> test7 (x : []) = 
74>     do
75>       y <- newRef $ int32 0
76>       xv <- readRef x
77>       writeRef xv y
78>       returnc $ int32 0
79
80
81\subsection{References Tests}
82
83\begin{verbatim}
84int x1 = 0;
85int x2 = x1;
86int *x3 = &x1;
87int *x4 = x3;
88int **x5 = &x4;
89int **x6 = x5;
90int ***x7 = &x5;
91int ***x8 = x7;
92\end{verbatim}
93
94> test100 :: Semantics Ref PureExpr
95> test100 = do
96>         a <- newRef $ int32 4
97>         a1 <- readRef a
98>         b <- newRef a
99>         b1 <- readRef b
100>         c <- newRef b
101>         c1 <- readRef c
102>         d <- newRef c
103>         d1 <- readRef d
104>         return d
105
106\begin{verbatim}
107int x1 = 0;
108int* x2 = &x1;
109int* x3 = x2;
110int x4 = *x3;
111int32_t* x5 = &*x3;
112x1 = 1;
113int x6 = 3
114x2 = &x6
115*x3 = 0
116\end{verbatim}
117
118> test101 :: Semantics Ref PureExpr
119> test101 = do
120>          x1 <- newRef $ int32 0
121>          x2 <- newRef x1
122>          x3 <- readRef x2
123>          x4 <- readRef x3
124>          x5 <- newRef x3
125>          writeRef x1 $ int32 1
126>          x6 <- newRef $ int32 3
127>          writeRef x2 x6
128>          writeRef x3 $ int32 0
129
130\begin{verbatim}
131int x1 = 0;
132x1 = 1;
133int *x2 = &x1;
134x2 = &x1;
135int **x3 = &x2;
136x3 = &x2;
137int ***x4 = &x3;
138x4 = &x3;
139int ***x5 = x4;
140*x5 = &x2;
141int **x6 = *x5;
142*x6 = &x1;
143int *x7 = *x6;
144*x7 = 2;
145int *x8 = &*x7;
146x8 = &*x7;
147int **x9 = &*x6;
148x9 = &*x6;
149\end{verbatim}
150
151> test102 :: Semantics Ref PureExpr
152> test102 = do
153>          x1 <- newRef $ int32 0
154>          writeRef x1 $ int32 1
155>          x2 <- newRef x1
156>          writeRef x2 x1
157>          x3 <- newRef x2
158>          writeRef x3 x2
159>          x4 <- newRef x3
160>          writeRef x4 x3
161>          x5 <- readRef x4
162>          writeRef x5 x2
163>          x6 <- readRef x5
164>          writeRef x6 x1
165>          x7 <- readRef x6
166>          writeRef x7 $ int32 2
167>          x8 <- newRef x7
168>          writeRef x8 x7
169>          x9 <- newRef x6
170>          writeRef x9 x6
171
172\begin{verbatim}
173int x1 = 0;
174int *x2 = &x1;
175int *x3 = &x1;
176int *x4 = x2;
177int *x5 = x3;
178*x4 = 2
179int *x6 = x3
180*x5 = 3
181int *x7 = x2;
182\end{verbatim}
183
184> test103 :: Semantics Ref PureExpr
185> test103 = do
186>          x1 <- newRef $ int32 0
187>          x2 <- newRef x1
188>          x3 <- newRef x1
189>          x2' <- readRef x2
190>          x3' <- readRef x3
191>          writeRef x2' $ int32 2
192>          x4 <- readRef x3
193>          writeRef x3' $ int32 3
194>          x5 <- readRef x2
195>          return Void
196
197
198\begin{verbatim}
199int x1 = 0;
200x1 = 1;
201int x2 = x1;
202// x2 == 1
203\end{verbatim}
204
205> test104 :: Semantics Ref PureExpr
206> test104 = do
207>          x1 <- newRef $ int32 0
208>          writeRef x1 $ int32 1
209>          y <- readRef x1
210>          return Void
211
212\begin{verbatim}
213int x1 = 0;
214int* x2 = &x1;
215int* x3 = x2;
216*x3 = 1;
217int x4 = x1;
218// x4 == 1
219\end{verbatim}
220
221> test105 :: Semantics Ref PureExpr
222> test105 = do
223>          x1 <- newRef $ int32 0
224>          x2 <- newRef x1
225>          x3 <- readRef x2
226>          writeRef x3 $ int32 1
227>          x4 <- readRef x1
228>          return Void
229
230\begin{verbatim}
231int x1 = 0;
232int* x2 = &x1;
233int** x3 = &x2;
234int** x4 = x3;
235int* x5 = *x4;
236*x5 = 1;
237int x6 = x1;
238\end{verbatim}
239
240> test106 :: Semantics Ref PureExpr
241> test106 = do
242>          x1 <- newRef $ int32 0
243>          x2 <- newRef x1
244>          x3 <- newRef x2
245>          x4 <- readRef x3
246>          x5 <- readRef x4
247>          writeRef x5 $ int32 1
248>          x6 <- readRef x1
249>          return Void
250
251\begin{verbatim}
252int32_t x1 = 0;
253int32_t* x2 = &x1;
254int32_t* x3 = x2;
255int32_t x4 = *x3;
256*x3 = ( x4 + 1 );
257\end{verbatim}
258
259> test107 :: Semantics Ref ()
260> test107 = do
261>           x1 <- newRef $ int32 0
262>           x2 <- newRef x1
263>           x3 <- readRef x2
264>           x4 <- readRef x3
265>           writeRef x3 (x4 .+. int32 1)
266>           return ()
267
268> test108 :: Semantics Ref ()
269> test108 = do
270>           x1 <- newRef $ int32 4
271>           x2 <- newRef $ int32 5
272>           x3 <- newRef x1
273>           x4 <- readRef x3
274>           writeRef x3 x2
275>           writeRef x4 $ int32 1
276>           x5 <- readRef x1
277>           x6 <- readRef x2
278>           return ()
279
280> test109 :: Semantics Ref ()
281> test109 = do
282>           x1 <- newRef $ int32 4
283>           x2 <- newRef $ int32 5
284>           x3 <- newRef x1
285>           x4 <- newRef x2
286>           x5 <- newRef x3
287>           x6 <- readRef x5
288>           x7 <- readRef x6
289>           writeRef x5 x4
290>           writeRef x7 $ int32 1
291>           return ()
292
293> test110 :: Semantics Ref ()
294> test110 = do
295>           x1 <- newRef $ int32 4
296>           x2 <- newRef x1
297>           x3 <- readRef x2
298>           x4 <- readRef x3
299>           x5 <- newRef x4
300>           return ()
301
302> test111 :: Semantics Ref ()
303> test111 = do
304>           x1 <- newRef $ int32 0
305>           x2 <- newRef x1
306>           writeRef x1 $ int32 1
307>           x3 <- newRef x1
308>           x4 <- readRef x1
309>           x5 <- newRef x4
310>           writeRef x5 x1
311>           writeRef x5 x4
312>           x6 <- readRef x4
313>           writeRef x4 $ int32 0
314>           x7 <- newRef x3
315>           x8 <- readRef x7
316>           x9 <- newRef x8
317>           x10 <- newRef x9
318>           x11 <- readRef x10
319>           x12 <- readRef x11
320>           x13 <- readRef x12
321>           writeRef x12 x1
322>           writeRef x12 x4
323>           writeRef x10 x9
324>           writeRef x7 x8
325>           writeRef x11 x5
326>           writeRef x11 x8
327>           return ()
328
329\subsection{Structures Test}
330
331\begin{verbatim}
332struct { int f; } s1;
333struct s1* d1 = (struct s1 *) malloc(sizeof(struct s1));
334d1->f = 0;
335
336struct { struct s1 *g } s2;
337struct s2* d2 = (struct s2 *) malloc(sizeof(struct s2));
338d2->g = d1;
339
340struct s2* d3 = (struct s2 *) malloc(sizeof(struct s2));
341d3->g = d1;
342
343struct s1 *d4 = d2->g;
344
345struct s1 *d5 = d3->g;
346
347d4->f = 1
348
349int d6 = d5->f
350
351d5->f = 2
352
353int d7 = d4->f
354\end{verbatim}
355
356> test200 :: Semantics Struct ()
357> test200 = do
358>          x1 <- newStruct "s1" [((TInt Signed TInt32), "f", int32 0)]
359>          x2 <- newStruct "s2" [(TStruct "s1" [("f", (TInt Signed TInt32))], "g", x1)]
360>          x3 <- newStruct "s2" [(TStruct "s1" [("f", (TInt Signed TInt32))], "g", x1)]
361>          x4 <- readStruct x2 "g"
362>          x5 <- readStruct x3 "g"
363>          writeStruct x4 "f" (int32 1)
364>          x6 <- readStruct x5 "f"
365>          writeStruct x5 "f" (int32 2)
366>          x7 <- readStruct x4 "f"
367>          return ()
368
369
370\begin{verbatim}
371struct { int32_t f1; float f2;  } s1;
372struct s1* d1 = (struct s1*) malloc(sizeof(struct s1));
373d1->f1 = 0;
374d1->f2 = 1.0;
375
376struct { int32_t g1; struct s1 * g2;  } s2;
377struct s2* d2 = (struct s2*) malloc(sizeof(struct s2));
378d2->g1 = 0;
379d2->g2 = d1;
380
381int32_t d3 = d1->f1;
382
383d1->f1 = 1;
384
385float d4 = d1->f2;
386
387d1->f2 = 4.0;
388
389int32_t d5 = d2->g1;
390
391d2->g1 = 2;
392
393struct s1 * d6 = d2->g2;
394
395d2->g2 = d1;
396
397int32_t d7 = d6->f1;
398
399d6->f1 = 1;
400
401float d8 = d6->f2;
402
403d6->f1 = 4.0;
404
405int32_t x9 = 2;
406
407struct { struct s2 * h1; int32_t* h2;  } s3;
408struct s3* d10 = (struct s3*) malloc(sizeof(struct s3));
409d10->h1 = d2;
410d10->h2 = &x9;
411
412int32_t* d11 = d10->h2;
413
414*d11 = 4;
415
416int size_x12 = 4;
417float* d12 = ( float* ) malloc( (size_x12 + 1)  * sizeof( float ));
418d12[0] = size_x12;
419for (int i = 1; i <= size_x12; i++){
420    d12[i] = 2.0;
421}
422
423struct { float* i1;  } s4;
424struct s4* d13 = (struct s4*) malloc(sizeof(struct s4));
425d13->i1 = d12;
426
427float* d14 = d13->i1;
428
429int index_x15 = 1;
430int size_d14_x15 = d14[0];
431if ( index_x15 < size_d14_x15 ){
432    d14[ 1 + index_x15] = 12.0;
433} else {
434    assert(! "Out of bound " );
435}
436\end{verbatim}
437
438> typeStruct1 :: TypeExpr
439> typeStruct1 = TStruct "s1" [("f1", (TInt Signed TInt32)), ("f2", TFloat)]
440
441> typeStruct2 :: TypeExpr
442> typeStruct2 = TStruct "s2" [("g1", (TInt Signed TInt32)), ("g2", typeStruct1)]
443
444> test201 :: Semantics (Ref :+: Struct :+: Array) ()
445> test201 = do
446>          x1 <- newStruct "s1" [((TInt Signed TInt32), "f1", int32 0),
447>                                (TFloat, "f2", float 1)]
448>          x2 <- newStruct "s2" [((TInt Signed TInt32), "g1", int32 0),
449>                                (typeStruct1, "g2", x1)]
450>          x3 <- readStruct x1 "f1"
451>          writeStruct x1 "f1" $ int32 1
452>          x4 <- readStruct x1 "f2"
453>          writeStruct x1 "f2" $ float 4
454>          x5 <- readStruct x2 "g1"
455>          writeStruct x2 "g1" $ int32 2
456>          x6 <- readStruct x2 "g2"
457>          writeStruct x2 "g2" x1
458>          x7 <- readStruct x6 "f1"
459>          writeStruct x6 "f1" $ int32 1
460>          x8 <- readStruct x6 "f2"
461>          writeStruct x6 "f1" $ float 4
462>          x9 <- newRef $ int32 2
463>          x10 <- newStruct "s3" [(typeStruct2, "h1", x2),
464>                                 (TPointer (TInt Signed TInt32) Avail, "h2", x9)]
465>          x11 <- readStruct x10 "h2"
466>          x12 <- writeRef x11 $ int32 4
467>          x13 <- newArray (float 2) (int32 4)
468>          x14 <- newStruct "s4" [(TArray TFloat, "i1", x13)]
469>          x15 <- readStruct x14 "i1"
470>          x16 <- writeArray x15 (int32 1) (float 12)
471>          return ()
472
473
474\begin{verbatim}
475struct { int f; } s1;
476struct s1* d1 = (struct s1 *) malloc(sizeof(struct s1))
477d1->f = 0
478
479struct { struct s1 *g; } s2;
480struct s2* d2 = (struct s2 *) malloc(sizeof(struct s2))
481d2->g = d1
482
483struct s1* d3 = d2->g
484
485struct s2* d4 = (struct s2 *) malloc(sizeof(struct s2))
486d4->g = d3
487\end{verbatim}
488
489> typeSt1 :: TypeExpr
490> typeSt1 = TStruct "s1" [("f", (TInt Signed TInt32))]
491
492> test202 :: Semantics Struct ()
493> test202 = do
494>           x1 <- newStruct "s1" [((TInt Signed TInt32), "f", int32 0)]
495>           x2 <- newStruct "s2" [(typeSt1, "g", x1)]
496>           x3 <- readStruct x2 "g" 
497>           x4 <- newStruct "s2" [(typeSt1, "g", x3)]
498>           return ()
499
500\begin{verbatim}
501int32_t x1 = 0;
502
503struct { int32_t* f;  } s1;
504struct s1* d2 = (struct s1*) malloc(sizeof(struct s1));
505d2->f = &x1;
506
507int32_t* d3 = d2->f;
508
509int32_t x4 = *d3;
510
511*d3 = 3;
512\end{verbatim}
513
514> test203 :: Semantics (Ref :+: Struct) ()
515> test203 = do
516>           x1 <- newRef $ int32 0
517>           x2 <- newStruct "s1" [(TPointer (TInt Signed TInt32) Avail,"f", x1)]
518>           x3 <- readStruct x2 "f"
519>           x4 <- readRef x3
520>           writeRef x3 $ int32 3
521>           return ()
522
523
524\subsection{Arrays Tests}
525
526\begin{verbatim}
527int size_x1 = 1;
528int32_t* d1 = ( int32_t* ) malloc( (size_x1 + 1)  * sizeof( int32_t ));
529d1[0] = size_x1;
530for (int i = 1; i <= size_x1; i++){
531    d1[i] = 0;
532}
533
534int size_x2 = 1;
535int32_t** d2 = ( int32_t** ) malloc( (size_x2 + 1)  * sizeof( int32_t* ));
536d2[0] = size_x2;
537for (int i = 1; i <= size_x2; i++){
538    d2[i] = d1;
539}
540
541int size_x3 = 1;
542int32_t** d3 = ( int32_t** ) malloc( (size_x3 + 1)  * sizeof( int32_t* ));
543d3[0] = size_x3;
544for (int i = 1; i <= size_x3; i++){
545    d3[i] = d1;
546}
547
548int index_x4 = 0;
549int size_d2_x4 = d2[0];
550int32_t* d4;
551if ( index_x4 < size_d2_x4 ){
552    d4 = d2[ index_x4 + 1];
553} else {
554    assert(! "Out of bound");
555    d4 = NULL;
556}
557
558int index_x5 = 0;
559int size_d3_x5 = d3[0];
560int32_t* d5;
561if ( index_x5 < size_d3_x5 ){
562    d5 = d3[ index_x5 + 1];
563} else {
564    assert(! "Out of bound");
565    d5 = NULL;
566}
567
568int index_x6 = 0;
569int size_d4_x6 = d4[0];
570if ( index_x6 < size_d4_x6 ){
571    d4[ 1 + index_x6] = 1;
572} else {
573    assert(! "Out of bound " );
574}
575
576int index_x7 = 0;
577int size_d5_x7 = d5[0];
578int32_t d7;
579if ( index_x7 < size_d5_x7 ){
580    d7 = d5[ index_x7 + 1];
581} else {
582    assert(! "Out of bound");
583    d7 = NULL;
584}
585
586int index_x8 = 0;
587int size_d5_x8 = d5[0];
588if ( index_x8 < size_d5_x8 ){
589    d5[ 1 + index_x8] = 2;
590} else {
591    assert(! "Out of bound " );
592}
593
594int index_x9 = 0;
595int size_d4_x9 = d4[0];
596int32_t d9;
597if ( index_x9 < size_d4_x9 ){
598    d9 = d4[ index_x9 + 1];
599} else {
600    assert(! "Out of bound");
601    d9 = NULL;
602}
603\end{verbatim}
604
605> test300 :: Semantics Array ()
606> test300 = do
607>          x1 <- newArray (int32 0) (int32 1)
608>          x2 <- newArray x1 (int32 1)
609>          x3 <- newArray x1 (int32 1)
610>          x4 <- readArray x2 (int32 0)
611>          x5 <- readArray x3 (int32 0)
612>          writeArray x4 (int32 0) (int32 1) 
613>          x6 <- readArray x5 (int32 0)
614>          writeArray x5 (int32 0) (int32 2)
615>          x7 <- readArray x4 (int32 0)
616>          return ()
617
618\begin{verbatim}
619int size_x1 = 4;
620float* d1 = ( float* ) malloc( (size_x1 + 1)  * sizeof( float ));
621d1[0] = size_x1;
622for (int i = 1; i <= size_x1; i++){
623    d1[i] = 2.0;
624}
625
626int index_x2 = ( 3 - 2 );
627int size_d1_x2 = d1[0];
628float d2;
629if ( index_x2 < size_d1_x2 ){
630    d2 = d1[ index_x2 + 1];
631} else {
632    assert(! "Out of bound");
633    d2 = NULL;
634}
635
636int index_x3 = 5;
637int size_d1_x3 = d1[0];
638float d3;
639if ( index_x3 < size_d1_x3 ){
640    d3 = d1[ index_x3 + 1];
641} else {
642    assert(! "Out of bound");
643    d3 = NULL;
644}
645
646int index_x4 = 3;
647int size_d1_x4 = d1[0];
648if ( index_x4 < size_d1_x4 ){
649    d1[ 1 + index_x4] = 19.0;
650} else {
651    assert(! "Out of bound " );
652}
653
654
655int size_x5 = 10;
656float** d5 = ( float** ) malloc( (size_x5 + 1)  * sizeof( float* ));
657d5[0] = size_x5;
658for (int i = 1; i <= size_x5; i++){
659    d5[i] = d1;
660}
661
662int index_x6 = 2;
663int size_d5_x6 = d5[0];
664if ( index_x6 < size_d5_x6 ){
665    d5[ 1 + index_x6] = d1;
666} else {
667    assert(! "Out of bound " );
668}
669
670int index_x7 = 4;
671int size_d5_x7 = d5[0];
672float* d7;
673if ( index_x7 < size_d5_x7 ){
674    d7 = d5[ index_x7 + 1];
675} else {
676    assert(! "Out of bound");
677    d7 = NULL;
678}
679
680int32_t x8 = 3;
681
682int size_x9 = 4;
683int32_t** d9 = ( int32_t** ) malloc( (size_x9 + 1)  * sizeof( int32_t* ));
684d9[0] = size_x9;
685for (int i = 1; i <= size_x9; i++){
686    d9[i] = &x8;
687}
688
689int32_t* x10 = &x8;
690
691int size_x11 = 3;
692int32_t*** d11 = ( int32_t*** ) malloc( (size_x11 + 1)  * sizeof( int32_t** ));
693d11[0] = size_x11;
694for (int i = 1; i <= size_x11; i++){
695    d11[i] = &x10;
696}
697\end{verbatim}
698
699> test301 :: Semantics (Ref :+: Array) ()
700> test301 = do
701>          x1 <- newArray (float 2) (int32 4)
702>          x10 <- readArray x1 (int32 3 .-. int32 2)
703>          x15 <- readArray x1 (int32 5)
704>          writeArray x1 (int32 3) (float 19)
705
706>          x2 <- newArray x1 (int32 10)
707>          writeArray x2 (int32 2) x1
708>          x21 <- readArray x2 (int32 4)
709>
710>          x3 <- newRef (int32 3)
711>          x4 <- newArray x3 (int32 4)
712>
713>          x5 <- newRef x3
714>          x6 <- newArray x5 (int32 3)
715>
716>          return ()
717
718\begin{verbatim}
719struct { int32_t f1; float f2;  } s1;
720struct s1* d1 = (struct s1*) malloc(sizeof(struct s1));
721d1->f1 = 0;
722d1->f2 = 1.0;
723
724int size_x2 = 5;
725struct s1 ** d2 = ( struct s1 ** ) malloc( (size_x2 + 1)  * sizeof( struct s1 * ));
726d2[0] = size_x2;
727for (int i = 1; i <= size_x2; i++){
728    d2[i] = d1;
729}
730
731int index_x3 = 2;
732int size_d2_x3 = d2[0];
733struct s1 * d3;
734if ( index_x3 < size_d2_x3 ){
735    d3 = d2[ index_x3 + 1];
736} else {
737    assert(! "Out of bound");
738    d3 = NULL;
739}
740
741int32_t d4 = d3->f1;
742
743d3->f1 = 0;
744\end{verbatim}
745
746> test302 :: Semantics (Struct :+: Array) ()
747> test302 = do
748>          x1 <- newStruct "s1" [((TInt Signed TInt32), "f1", int32 0),
749>                                (TFloat, "f2", float 1)]
750>          x2 <- newArray x1 (int32 5)
751>          x3 <- readArray x2 (int32 2)
752>          x4 <- readStruct x3 "f1"
753>          writeStruct x3 "f1" (int32 0)
754>          return ()
755
756\begin{verbatim}
757int x1 = 0
758
759int size_x2 = 4;
760int32_t** d2 = ( int32_t** ) malloc( (size_x2 + 1)  * sizeof( int32_t* ));
761d2[0] = size_x2;
762for (int i = 1; i <= size_x2; i++){
763    d2[i] = &x1;
764}
765
766int index_x3 = 1;
767int size_d2_x3 = d2[0];
768int32_t* d3;
769if ( index_x3 < size_d2_x3 ){
770    d3 = d2[ index_x3 + 1];
771} else {
772    assert(! "Out of bound");
773    d3 = NULL;
774}
775
776int32_t x4 = *d3;
777
778*d3 = 3;
779\end{verbatim}
780
781> test303 :: Semantics (Ref :+: Array) ()
782> test303 = do
783>           x1 <- newRef $ int32 0
784>           x2 <- newArray x1 (int32 4)
785>           x3 <- readArray x2 (int32 1)
786>           x4 <- readRef x3
787>           writeRef x3 $ int32 3
788>           return ()
789
790\begin{verbatim}
791int32_t x1 = 0;
792
793int32_t* x2 = &x1;
794
795int size_x3 = 3;
796int32_t*** d3 = ( int32_t*** ) malloc( (size_x3 + 1)  * sizeof( int32_t** ));
797d3[0] = size_x3;
798for (int i = 1; i <= size_x3; i++){
799    d3[i] = &x2;
800}
801
802int index_x4 = 1;
803int size_d3_x4 = d3[0];
804int32_t** d4;
805if ( index_x4 < size_d3_x4 ){
806    d4 = d3[ index_x4 + 1];
807} else {
808    assert(! "Out of bound");
809    d4 = NULL;
810}
811
812int32_t* x5 = *x4;
813
814*x5 = 4;
815\end{verbatim}
816
817> test304 :: Semantics (Ref :+: Array) ()
818> test304 = do
819>           x1 <- newRef $ int32 0
820>           x2 <- newRef x1
821>           x3 <- newArray x2 (int32 3)
822>           x4 <- readArray x3 (int32 1)
823>           x5 <- readRef x4
824>           writeRef x5 $ int32 4
825>           return ()
826
827
828\section{Functions}
829
830
831> body400 :: [PureExpr] ->  Semantics Bot PureExpr
832> body400 _ = do
833>        return $ int32 2
834
835
836> body401 :: [PureExpr] ->  Semantics (Bot :+: Def :+: Conditionals) PureExpr
837> body401 (_ : y : []) = do
838>           ifc (do return (y .==. int32 3) :: Semantics Bot PureExpr)
839>               (do
840>                returnc $ int32 2 :: Semantics Def PureExpr
841>               )
842>               (do
843>                returnc $ int32 4 :: Semantics Def PureExpr
844>               )
845>           returnc $ int32 5
846
847
848
849> unionTest :: TypeExpr
850> unionTest = TUnion "test_t" [("field1", TInt Signed TInt32), ("field2", TFloat), ("field3", TInt Signed TInt32)]
851
852> body402 :: [PureExpr] -> Semantics (Ref :+: Def :+: Assert :+: Conditionals) PureExpr
853> body402 (x : []) = 
854>      do
855>       y <- newRef $ x
856>       c <- newRef $ int32 1
857>       while (do yv <- readRef y; return (yv .>. (int32 0)) :: Semantics Ref PureExpr) 
858>           ((do
859>             yv <- readRef y
860>             writeRef y (yv .-. int32 1)
861>             cv <- readRef c
862>             writeRef c (cv .*. yv)) :: Semantics (Assert :+: Ref) PureExpr)
863>       cv <- readRef c
864>       returnc cv
865
866> test403 :: Semantics (Bot :+: Def :+: Conditionals) PureExpr
867> test403 =
868>     do
869>       f1 <- def [] "name" body401 int32T  [int32T, int32T]
870>       x <- call f1 [int32 3, int32 1]
871>       return Void
872
873> test404 :: Semantics (Bot :+: Ref :+: Def) PureExpr
874> test404 =
875>     do
876>       f1 <- def [] "bug" test7 voidT [ptrT (ptrT int32T)]
877>       
878>       x <- newRef $ int32 1
879>       xp <- newRef x
880>       
881>       _ <- call f1 [xp]
882>            
883>       returnc x
884
885> test405 :: Semantics (Bot :+: Ref :+: Def) PureExpr
886> test405 =
887>     do
888>       f1 <- def [] "inc" test5 voidT [ptrT (ptrT int32T)]
889>       
890>       x <- newRef $ int32 4
891>       y <- newRef $ x
892>       _ <- call f1 [y]
893>       _ <- call f1 [y]
894>       yv <- readRef y
895>       xv <- readRef yv
896>       returnc xv
897
898> test406 :: Semantics (Bot :+: Array :+: Def) PureExpr
899> test406 =
900>     do
901>       f1 <- def [] "f1" body407 voidT [arrayT int32T]
902>       x <- newArray (float 4) (int32 3)
903>       _ <- call f1 [x]
904>       return x
905
906> body407 :: [PureExpr] -> Semantics (Bot :+: Array :+: Def) PureExpr
907> body407 (x : [])= 
908>     do
909>       x1 <- readArray x (int32 1)
910>       return Void
911
912> test408 :: Semantics (Bot :+: Struct :+: Def) PureExpr
913> test408 =
914>     do
915>       f1 <- def [] "f1" body409 voidT [structT "s1" [("f1",(int32T))]]
916>       x <- newStruct "s1" [((TInt Signed TInt32), "f1", int32 4)]
917>       _ <- call f1 [x]
918>       return Void
919
920> body409 :: [PureExpr] -> Semantics (Bot :+: Struct :+: Def) PureExpr
921> body409 (x : [])= 
922>     do
923>       x1 <- readStruct x "f1"
924>       return Void
925
926> test410 :: Semantics (Bot :+: Ref :+: Assert :+: Conditionals :+: Def) PureExpr
927> test410 = do
928>           factorial <- def [] "factorial" body402 int32T [int32T]
929>           x <- call factorial [int32 4]
930>           return Void
931
932\section{Static Arrays}
933
934> test500 :: Semantics StaticArray PureExpr
935> test500 = do
936>          x1 <- newStaticArray [int32 1, int32 2, int32 3]
937>          x2 <- newStaticArray [x1, x1, x1, x1]
938>          x3 <- newStaticArray [x1, x1]
939>          x4 <- readStaticArray x2 (int32 0)
940>          x5 <- readStaticArray x3 (int32 1)
941>          writeStaticArray x4 (int32 0) (int32 1) 
942>          x6 <- readStaticArray x5 (int32 0)
943>          writeStaticArray x5 (int32 0) (int32 2)
944>          x7 <- readStaticArray x4 (int32 0)
945>          return void
946
947> test501 :: Semantics (Ref :+: StaticArray) PureExpr
948> test501 = do
949>          x1 <- newStaticArray [float 2, float 3, float 1]
950>          x10 <- readStaticArray x1 (int32 3 .-. int32 2)
951>          x15 <- readStaticArray x1 (int32 5)
952>          writeStaticArray x1 (int32 3) (float 19)
953
954>          x2 <- newStaticArray [x1, x1, x1]
955>          writeStaticArray x2 (int32 2) x1
956>          x21 <- readStaticArray x2 (int32 4)
957>
958>          x3 <- newRef (int32 3)
959>          x4 <- newStaticArray [x3, x3]
960>
961>          x5 <- newRef x3
962>          x6 <- newStaticArray [x5, x5, x5]
963>
964>          return void
965
966> test502 :: Semantics (Struct :+: StaticArray) PureExpr
967> test502 = do
968>          x1 <- newStruct "s1" [((TInt Signed TInt32), "f1", int32 0),
969>                                (TFloat, "f2", float 1)]
970>          x2 <- newStaticArray [x1, x1]
971>          x3 <- readStaticArray x2 (int32 2)
972>          x4 <- readStruct x3 "f1"
973>          writeStruct x3 "f1" (int32 0)
974>          return void
975
976> test503 :: Semantics (Ref :+: StaticArray) PureExpr
977> test503 = do
978>           x1 <- newRef $ int32 0
979>           x2 <- newStaticArray [x1, x1]
980>           x3 <- readStaticArray x2 (int32 1)
981>           x4 <- readRef x3
982>           writeRef x3 $ int32 3
983>           return void
984
985> test504 :: Semantics (Ref :+: StaticArray) PureExpr
986> test504 = do
987>           x1 <- newRef $ int32 0
988>           x2 <- newRef x1
989>           x3 <- newStaticArray [x2, x2, x2]
990>           x4 <- readStaticArray x3 (int32 1)
991>           x5 <- readRef x4
992>           writeRef x5 $ int32 4
993>           return void
994
995> -}
996
997%endif
998
999
1000
1001
1002> main :: IO ()
1003> main = do
1004>        putStrLn "Nothing done."
1005
1006%if false 
1007
1008> {- 
1009
1010>        let (s, _) = compile (test500) emptyBinding in
1011>            putStrLn $ show s 
1012
1013> --     let (v, h) = run (test6) emptyHeap in
1014> --        print $ show (symbEval v)
1015
1016> -}
1017
1018%endif