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 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 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 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 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 133312a1df1SDavid du Colombier repro_src(void) 134312a1df1SDavid du Colombier { 135312a1df1SDavid du Colombier repro_proc(rdy); 136312a1df1SDavid du Colombier } 137