1312a1df1SDavid du Colombier /***** spin: reprosrc.c *****/
2312a1df1SDavid du Colombier
3312a1df1SDavid du Colombier /* Copyright (c) 2002-2003 by Lucent Technologies, Bell Laboratories. */
4312a1df1SDavid du Colombier /* All Rights Reserved. This software is for educational purposes only. */
5312a1df1SDavid du Colombier /* No guarantee whatsoever is expressed or implied by the distribution of */
6312a1df1SDavid du Colombier /* this code. Permission is given to distribute this code provided that */
7312a1df1SDavid du Colombier /* this introductory message is not removed and no monies are exchanged. */
8312a1df1SDavid du Colombier /* Software written by Gerard J. Holzmann. For tool documentation see: */
9312a1df1SDavid du Colombier /* http://spinroot.com/ */
10312a1df1SDavid du Colombier /* Send all bug-reports and/or questions to: bugs@spinroot.com */
11312a1df1SDavid du Colombier
12312a1df1SDavid du Colombier #include <stdio.h>
13312a1df1SDavid du Colombier #include "spin.h"
14312a1df1SDavid du Colombier #include "y.tab.h"
15312a1df1SDavid du Colombier
16312a1df1SDavid du Colombier static int indent = 1;
17312a1df1SDavid du Colombier
18312a1df1SDavid du Colombier extern ProcList *rdy;
19312a1df1SDavid du Colombier void repro_seq(Sequence *);
20312a1df1SDavid du Colombier
21312a1df1SDavid du Colombier void
doindent(void)22312a1df1SDavid du Colombier doindent(void)
23312a1df1SDavid du Colombier { int i;
24312a1df1SDavid du Colombier for (i = 0; i < indent; i++)
25312a1df1SDavid du Colombier printf(" ");
26312a1df1SDavid du Colombier }
27312a1df1SDavid du Colombier
28312a1df1SDavid du Colombier void
repro_sub(Element * e)29312a1df1SDavid du Colombier repro_sub(Element *e)
30312a1df1SDavid du Colombier {
31312a1df1SDavid du Colombier doindent();
32312a1df1SDavid du Colombier switch (e->n->ntyp) {
33312a1df1SDavid du Colombier case D_STEP:
34312a1df1SDavid du Colombier printf("d_step {\n");
35312a1df1SDavid du Colombier break;
36312a1df1SDavid du Colombier case ATOMIC:
37312a1df1SDavid du Colombier printf("atomic {\n");
38312a1df1SDavid du Colombier break;
39312a1df1SDavid du Colombier case NON_ATOMIC:
40312a1df1SDavid du Colombier printf(" {\n");
41312a1df1SDavid du Colombier break;
42312a1df1SDavid du Colombier }
43312a1df1SDavid du Colombier indent++;
44312a1df1SDavid du Colombier repro_seq(e->n->sl->this);
45312a1df1SDavid du Colombier indent--;
46312a1df1SDavid du Colombier
47312a1df1SDavid du Colombier doindent();
48312a1df1SDavid du Colombier printf(" };\n");
49312a1df1SDavid du Colombier }
50312a1df1SDavid du Colombier
51312a1df1SDavid du Colombier void
repro_seq(Sequence * s)52312a1df1SDavid du Colombier repro_seq(Sequence *s)
53312a1df1SDavid du Colombier { Element *e;
54312a1df1SDavid du Colombier Symbol *v;
55312a1df1SDavid du Colombier SeqList *h;
56312a1df1SDavid du Colombier
57312a1df1SDavid du Colombier for (e = s->frst; e; e = e->nxt)
58312a1df1SDavid du Colombier {
59312a1df1SDavid du Colombier v = has_lab(e, 0);
60312a1df1SDavid du Colombier if (v) printf("%s:\n", v->name);
61312a1df1SDavid du Colombier
62312a1df1SDavid du Colombier if (e->n->ntyp == UNLESS)
63312a1df1SDavid du Colombier { printf("/* normal */ {\n");
64312a1df1SDavid du Colombier repro_seq(e->n->sl->this);
65312a1df1SDavid du Colombier doindent();
66312a1df1SDavid du Colombier printf("} unless {\n");
67312a1df1SDavid du Colombier repro_seq(e->n->sl->nxt->this);
68312a1df1SDavid du Colombier doindent();
69312a1df1SDavid du Colombier printf("}; /* end unless */\n");
70312a1df1SDavid du Colombier } else if (e->sub)
71312a1df1SDavid du Colombier {
72312a1df1SDavid du Colombier switch (e->n->ntyp) {
73312a1df1SDavid du Colombier case DO: doindent(); printf("do\n"); indent++; break;
74312a1df1SDavid du Colombier case IF: doindent(); printf("if\n"); indent++; break;
75312a1df1SDavid du Colombier }
76312a1df1SDavid du Colombier
77312a1df1SDavid du Colombier for (h = e->sub; h; h = h->nxt)
78312a1df1SDavid du Colombier { indent--; doindent(); indent++; printf("::\n");
79312a1df1SDavid du Colombier repro_seq(h->this);
80312a1df1SDavid du Colombier printf("\n");
81312a1df1SDavid du Colombier }
82312a1df1SDavid du Colombier
83312a1df1SDavid du Colombier switch (e->n->ntyp) {
84312a1df1SDavid du Colombier case DO: indent--; doindent(); printf("od;\n"); break;
85312a1df1SDavid du Colombier case IF: indent--; doindent(); printf("fi;\n"); break;
86312a1df1SDavid du Colombier }
87312a1df1SDavid du Colombier } else
88312a1df1SDavid du Colombier { if (e->n->ntyp == ATOMIC
89312a1df1SDavid du Colombier || e->n->ntyp == D_STEP
90312a1df1SDavid du Colombier || e->n->ntyp == NON_ATOMIC)
91312a1df1SDavid du Colombier repro_sub(e);
92312a1df1SDavid du Colombier else if (e->n->ntyp != '.'
93312a1df1SDavid du Colombier && e->n->ntyp != '@'
94312a1df1SDavid du Colombier && e->n->ntyp != BREAK)
95312a1df1SDavid du Colombier {
96312a1df1SDavid du Colombier doindent();
97312a1df1SDavid du Colombier if (e->n->ntyp == C_CODE)
98312a1df1SDavid du Colombier { printf("c_code ");
99*00d97012SDavid du Colombier plunk_inline(stdout, e->n->sym->name, 1, 1);
100312a1df1SDavid du Colombier } else if (e->n->ntyp == 'c'
101312a1df1SDavid du Colombier && e->n->lft->ntyp == C_EXPR)
102312a1df1SDavid du Colombier { printf("c_expr { ");
103312a1df1SDavid du Colombier plunk_expr(stdout, e->n->lft->sym->name);
104312a1df1SDavid du Colombier printf("} ->\n");
105312a1df1SDavid du Colombier } else
106312a1df1SDavid du Colombier { comment(stdout, e->n, 0);
107312a1df1SDavid du Colombier printf(";\n");
108312a1df1SDavid du Colombier } }
109312a1df1SDavid du Colombier }
110312a1df1SDavid du Colombier if (e == s->last)
111312a1df1SDavid du Colombier break;
112312a1df1SDavid du Colombier }
113312a1df1SDavid du Colombier }
114312a1df1SDavid du Colombier
115312a1df1SDavid du Colombier void
repro_proc(ProcList * p)116312a1df1SDavid du Colombier repro_proc(ProcList *p)
117312a1df1SDavid du Colombier {
118312a1df1SDavid du Colombier if (!p) return;
119312a1df1SDavid du Colombier if (p->nxt) repro_proc(p->nxt);
120312a1df1SDavid du Colombier
121312a1df1SDavid du Colombier if (p->det) printf("D"); /* deterministic */
122312a1df1SDavid du Colombier printf("proctype %s()", p->n->name);
123312a1df1SDavid du Colombier if (p->prov)
124312a1df1SDavid du Colombier { printf(" provided ");
125312a1df1SDavid du Colombier comment(stdout, p->prov, 0);
126312a1df1SDavid du Colombier }
127312a1df1SDavid du Colombier printf("\n{\n");
128312a1df1SDavid du Colombier repro_seq(p->s);
129312a1df1SDavid du Colombier printf("}\n");
130312a1df1SDavid du Colombier }
131312a1df1SDavid du Colombier
132312a1df1SDavid du Colombier void
repro_src(void)133312a1df1SDavid du Colombier repro_src(void)
134312a1df1SDavid du Colombier {
135312a1df1SDavid du Colombier repro_proc(rdy);
136312a1df1SDavid du Colombier }
137