1: /* Copyright (c) Stichting Mathematisch Centrum, Amsterdam, 1985. */ 2: 3: /* 4: $Header: b2stc.c,v 1.4 85/08/22 16:55:56 timo Exp $ 5: */ 6: 7: /* B (intra-unit) type check */ 8: 9: #include "b.h" 10: #include "b1obj.h" 11: #include "b2nod.h" 12: #include "b2syn.h" /* temporary? for Cap in tc_refinement */ 13: #include "b2tcP.h" 14: #include "b2tcU.h" 15: #include "b2tcE.h" 16: #include "b3err.h" 17: 18: /* ******************************************************************** */ 19: 20: Hidden value refname; 21: 22: /* 23: * if in commandsuite of refinement: 24: * holds refinement name; 25: * if in commandsuite of yield unit: 26: * holds B-text "returned value" 27: * (used in error messages, no confusion possible) 28: * else 29: * Vnil 30: * To be used in tc_return() 31: */ 32: 33: /* ******************************************************************** */ 34: 35: Forward polytype pt_expr(); 36: 37: Visible Procedure type_check(v) parsetree v; { 38: typenode n; 39: extern bool extcmds; /* Set in main by -E option */ 40: 41: if (extcmds || !still_ok || v EQ NilTree) 42: return; 43: n = nodetype(v); 44: curline= v; curlino= one; 45: start_vars(); 46: refname = Vnil; 47: usetypetable(mk_elt()); 48: if (Unit(n)) tc_unit(v); 49: else if (Command(n)) tc_command(v); 50: else if (Expression(n)) p_release(pt_expr(v)); 51: else syserr(MESS(2300, "wrong argument of 'type_check'")); 52: end_vars(); 53: deltypetable(); 54: } 55: 56: #define TABSIZE 72 57: 58: Hidden Procedure (*(uni_tab[TABSIZE]))(); /*Units*/ 59: Hidden Procedure (*(cmd_tab[TABSIZE]))(); /*Commands*/ 60: Hidden polytype (*(exp_tab[TABSIZE]))(); /*Expressions*/ 61: Hidden Procedure (*(tes_tab[TABSIZE]))(); /*Tests*/ 62: 63: #define FF First_fieldnr 64: 65: Hidden Procedure tc_node(v, tab) parsetree v; int (*(tab[]))(); { 66: auto (*f)()= tab[nodetype(v)]; 67: switch (Nbranches(v)) { 68: case 0: (*f)(); break; 69: case 1: (*f)(*Branch(v,FF)); break; 70: case 2: (*f)(*Branch(v,FF), *Branch(v,FF+1)); break; 71: case 3: (*f)(*Branch(v,FF), *Branch(v,FF+1), 72: *Branch(v,FF+2)); break; 73: case 4: (*f)(*Branch(v,FF), *Branch(v,FF+1), 74: *Branch(v,FF+2), *Branch(v,FF+3)); break; 75: case 5: (*f)(*Branch(v,FF), *Branch(v,FF+1), 76: *Branch(v,FF+2), *Branch(v,FF+3), 77: *Branch(v,FF+4)); break; 78: case 6: (*f)(*Branch(v,FF), *Branch(v,FF+1), 79: *Branch(v,FF+2), *Branch(v,FF+3), 80: *Branch(v,FF+4), *Branch(v,FF+5)); break; 81: case 7: (*f)(*Branch(v,FF), *Branch(v,FF+1), 82: *Branch(v,FF+2), *Branch(v,FF+3), 83: *Branch(v,FF+4), *Branch(v,FF+5), 84: *Branch(v,FF+6)); break; 85: case 8: (*f)(*Branch(v,FF), *Branch(v,FF+1), 86: *Branch(v,FF+2), *Branch(v,FF+3), 87: *Branch(v,FF+4), *Branch(v,FF+5), 88: *Branch(v,FF+6), *Branch(v,FF+7)); break; 89: case 9: (*f)(*Branch(v,FF), *Branch(v,FF+1), 90: *Branch(v,FF+2), *Branch(v,FF+3), 91: *Branch(v,FF+4), *Branch(v,FF+5), 92: *Branch(v,FF+6), *Branch(v,FF+7), 93: *Branch(v,FF+8)); break; 94: default: syserr(MESS(2301, "Wrong size node in tc_node")); 95: } 96: } 97: 98: Hidden polytype pt_node(v, tab) parsetree v; polytype (*(tab[]))(); { 99: polytype (*f)()= tab[nodetype(v)]; 100: switch (Nbranches(v)) { 101: case 0: (*f)(); break; 102: case 1: (*f)(*Branch(v,FF)); break; 103: case 2: (*f)(*Branch(v,FF), *Branch(v,FF+1)); break; 104: case 3: (*f)(*Branch(v,FF), *Branch(v,FF+1), 105: *Branch(v,FF+2)); break; 106: case 4: (*f)(*Branch(v,FF), *Branch(v,FF+1), 107: *Branch(v,FF+2), *Branch(v,FF+3)); break; 108: case 5: (*f)(*Branch(v,FF), *Branch(v,FF+1), 109: *Branch(v,FF+2), *Branch(v,FF+3), 110: *Branch(v,FF+4)); break; 111: case 6: (*f)(*Branch(v,FF), *Branch(v,FF+1), 112: *Branch(v,FF+2), *Branch(v,FF+3), 113: *Branch(v,FF+4), *Branch(v,FF+5)); break; 114: case 7: (*f)(*Branch(v,FF), *Branch(v,FF+1), 115: *Branch(v,FF+2), *Branch(v,FF+3), 116: *Branch(v,FF+4), *Branch(v,FF+5), 117: *Branch(v,FF+6)); break; 118: case 8: (*f)(*Branch(v,FF), *Branch(v,FF+1), 119: *Branch(v,FF+2), *Branch(v,FF+3), 120: *Branch(v,FF+4), *Branch(v,FF+5), 121: *Branch(v,FF+6), *Branch(v,FF+7)); break; 122: case 9: (*f)(*Branch(v,FF), *Branch(v,FF+1), 123: *Branch(v,FF+2), *Branch(v,FF+3), 124: *Branch(v,FF+4), *Branch(v,FF+5), 125: *Branch(v,FF+6), *Branch(v,FF+7), 126: *Branch(v,FF+8)); break; 127: default: syserr(MESS(2302, "Wrong size node in pt_node")); 128: /* NOTREACHED */ 129: } 130: } 131: 132: /* ******************************************************************** */ 133: /* Type Check units */ 134: /* ******************************************************************** */ 135: 136: Hidden Procedure tc_unit(v) parsetree v; { 137: if (v != NilTree) tc_node(v, uni_tab); 138: } 139: 140: Hidden Procedure tc_howto_unit(name, formals, cmt, 141: suite, refinement, reftab, nlocals) 142: parsetree suite, refinement; 143: value name, formals, cmt, reftab, nlocals; { 144: 145: tc_command(suite); 146: tc_unit(refinement); 147: } 148: 149: Hidden Procedure tc_yield_unit(name, adic, formals, cmt, 150: suite, refinement, reftab, nlocals) 151: parsetree suite, refinement; 152: value name, adic, formals, cmt, reftab, nlocals; { 153: 154: refname = mk_text("returned value"); 155: tc_command(suite); 156: release(refname); refname = Vnil; 157: tc_unit(refinement); 158: } 159: 160: Hidden Procedure tc_test_unit(name, adic, formals, cmt, 161: suite, refinement, reftab, nlocals) 162: parsetree suite, refinement; 163: value name, adic, formals, cmt, reftab, nlocals; { 164: 165: tc_command(suite); 166: tc_unit(refinement); 167: } 168: 169: Hidden Procedure tc_refinement(name, cmt, suite, next) 170: parsetree suite, next; value name, cmt; { 171: value n1 = curtail(name, one); 172: 173: if (!Cap(charval(n1))) /* should test for expression refinement */ 174: refname = copy(name); 175: release(n1); 176: tc_command(suite); 177: if (refname NE Vnil) { 178: release(refname); refname = Vnil; 179: } 180: 181: tc_unit(next); 182: } 183: 184: /* ******************************************************************** */ 185: /* TypeCheck commands */ 186: /* ******************************************************************** */ 187: 188: Hidden Procedure tc_command(v) parsetree v; { 189: curline= v; 190: end_vars(); 191: start_vars(); 192: if (v != NilTree) tc_node(v, cmd_tab); 193: } 194: 195: Hidden Procedure tc_suite(lino, cmd, cmt, next) 196: parsetree cmd, next; value lino, cmt; { 197: 198: curlino= lino; 199: tc_command(cmd); 200: tc_command(next); 201: } 202: 203: Hidden Procedure tc_put(e, t) parsetree e, t; { 204: polytype te, tt, u; 205: te = pt_expr(e); 206: tt = pt_expr(t); 207: unify(te, tt, &u); 208: p_release(te); p_release(tt); p_release(u); 209: } 210: 211: Hidden Procedure tc_ins_rem(e, t) parsetree e, t; { 212: polytype t_list_e, tt, u; 213: t_list_e = mkt_list(pt_expr(e)); 214: tt = pt_expr(t); 215: unify(tt, t_list_e, &u); 216: p_release(t_list_e); p_release(tt); p_release(u); 217: } 218: 219: Hidden Procedure tc_choose(t, e) parsetree t, e; { 220: polytype t_tlt_t, te, u; 221: t_tlt_t = mkt_tlt(pt_expr(t)); 222: te = pt_expr(e); 223: unify(te, t_tlt_t, &u); 224: p_release(te); p_release(t_tlt_t); p_release(u); 225: } 226: 227: Hidden Procedure tc_draw(t) parsetree t; { 228: polytype t_number, tt, u; 229: tt = pt_expr(t); 230: t_number = mkt_number(); 231: unify(tt, t_number, &u); 232: p_release(t_number); p_release(tt); p_release(u); 233: } 234: 235: Hidden Procedure tc_set_random(e) parsetree e; { 236: p_release(pt_expr(e)); 237: } 238: 239: Hidden Procedure tc_delete(t) parsetree t; { 240: p_release(pt_expr(t)); 241: } 242: 243: Hidden Procedure tc_check(c) parsetree c; { 244: tc_test(c); 245: } 246: 247: Hidden Procedure tc_nothing(t) parsetree t; {} 248: 249: Hidden Procedure tc_write(nl1, e, nl2) parsetree e; value nl1, nl2; { 250: if (e != NilTree) 251: p_release(pt_expr(e)); 252: } 253: 254: Hidden Procedure tc_read(t, e) parsetree t, e; { 255: polytype te, tt, u; 256: te = pt_expr(e); 257: tt = pt_expr(t); 258: unify(tt, te, &u); 259: p_release(te); p_release(tt); p_release(u); 260: } 261: 262: Hidden Procedure tc_raw_read(t) parsetree t; { 263: polytype t_text, tt, u; 264: t_text = mkt_text(); 265: tt = pt_expr(t); 266: unify(tt, t_text, &u); 267: p_release(t_text); p_release(tt); p_release(u); 268: } 269: 270: Hidden Procedure tc_ifwhile(c, cmt, s) parsetree c, s; value cmt; { 271: tc_test(c); 272: tc_command(s); 273: } 274: 275: Hidden Procedure tc_for(t, e, cmt, s) parsetree t, e, s; value cmt; { 276: polytype t_tlt_t, te, u; 277: 278: t_tlt_t = mkt_tlt(pt_expr(t)); 279: te = pt_expr(e); 280: unify(te, t_tlt_t, &u); 281: p_release(te); p_release(t_tlt_t); p_release(u); 282: 283: tc_command(s); 284: } 285: 286: Hidden Procedure tc_select(cmt, s) parsetree s; value cmt; { 287: tc_command(s); 288: } 289: 290: Hidden Procedure tc_tes_suite(lino, c, cmt, s, next) 291: parsetree c, s, next; value lino, cmt; { 292: curlino= lino; 293: if (c != NilTree) { 294: tc_test(c); 295: tc_command(s); 296: } 297: tc_command(next); 298: } 299: 300: Hidden Procedure tc_else(lino, cmt, s) parsetree s; value lino, cmt; { 301: curlino= lino; 302: tc_command(s); 303: } 304: 305: Hidden Procedure tc_return(e) parsetree e; { 306: polytype te, tt, u; 307: te = pt_expr(e); 308: if (refname EQ Vnil) 309: error(MESS(2303, "RETURN not in YIELD unit or expression refinement")); 310: else { 311: tt = mkt_var(copy(refname)); 312: unify(tt, te, &u); 313: p_release(tt); p_release(u); 314: } 315: p_release(te); 316: } 317: 318: Hidden Procedure tc_report(c) parsetree c; { 319: tc_test(c); 320: } 321: 322: Hidden Procedure tc_user_command(name, v) value name, v; { 323: parsetree e; value w= v; 324: while (w != Vnil) { 325: e= *Branch(w, ACT_EXPR); 326: if (e != NilTree) 327: p_release(pt_expr(e)); 328: w= *Branch(w, ACT_NEXT); 329: } 330: } 331: 332: /* ******************************************************************** */ 333: /* calculate PolyType of EXPRessions 334: /* ******************************************************************** */ 335: 336: Hidden polytype pt_expr(v) parsetree v; { 337: return pt_node(v, exp_tab); 338: } 339: 340: Hidden polytype pt_compound(e) parsetree e; { 341: return pt_expr(e); 342: } 343: 344: Hidden polytype pt_collateral(e) value e; { 345: intlet k, len= Nfields(e); 346: polytype tc; 347: tc = mkt_compound(len); 348: for (k = 0; k < len; k++) 349: putsubtype(pt_expr(*Field(e, k)), tc, k); 350: return tc; 351: } 352: 353: Hidden bool is_string(v, s) value v; string s; { 354: value t; 355: relation rel; 356: 357: rel = compare(v, t= mk_text(s)); 358: release(t); 359: return (rel EQ 0 ? Yes : No); 360: } 361: 362: Hidden bool monf_on_number(n) value n; { 363: return (is_string(n, "~") || 364: is_string(n, "+") || 365: is_string(n, "-") || 366: is_string(n, "*/") || 367: is_string(n, "/*") || 368: is_string(n, "root") || 369: is_string(n, "abs") || 370: is_string(n, "sign") || 371: is_string(n, "floor") || 372: is_string(n, "ceiling") || 373: is_string(n, "round") || 374: is_string(n, "sin") || 375: is_string(n, "cos") || 376: is_string(n, "tan") || 377: is_string(n, "atan") || 378: is_string(n, "exp") || 379: is_string(n, "log") 380: ); 381: } 382: 383: Hidden bool dyaf_on_number(n) value n; { 384: return (is_string(n, "+") || 385: is_string(n, "-") || 386: is_string(n, "*") || 387: is_string(n, "/") || 388: is_string(n, "**") || 389: is_string(n, "root") || 390: is_string(n, "round") || 391: is_string(n, "mod") || 392: is_string(n, "atan") || 393: is_string(n, "log") 394: ); 395: } 396: 397: Hidden polytype pt_monf(name, r, fct) parsetree r; value name, fct; { 398: polytype tr, tf, u; 399: 400: tr = pt_expr(r); 401: 402: if (monf_on_number(name)) { 403: polytype t_number = mkt_number(); 404: unify(tr, t_number, &u); 405: p_release(u); 406: tf = t_number; 407: } 408: else if (is_string(name, "keys")) { 409: polytype t_table, t_keys; 410: t_keys = mkt_newvar(); 411: t_table = mkt_table(p_copy(t_keys), mkt_newvar()); 412: unify(tr, t_table, &u); 413: p_release(t_table); p_release(u); 414: tf = mkt_list(t_keys); 415: } 416: else if (is_string(name, "#")) { 417: polytype t_tlt = mkt_tlt(mkt_newvar()); 418: unify(tr, t_tlt, &u); 419: p_release(t_tlt); p_release(u); 420: tf = mkt_number(); 421: } 422: else if (is_string(name, "min") || is_string(name, "max")) { 423: polytype t_tlt_x, t_x; 424: t_x = mkt_newvar(); 425: t_tlt_x = mkt_tlt(p_copy(t_x)); 426: unify(tr, t_tlt_x, &u); 427: p_release(t_tlt_x); p_release(u); 428: tf = t_x; 429: } 430: else { 431: tf = mkt_newvar(); 432: } 433: 434: p_release(tr); 435: return tf; 436: } 437: 438: Hidden polytype pt_dyaf(l, name, r, fct) parsetree l, r; value name, fct; { 439: polytype tl, tr, tf, u; 440: 441: tl = pt_expr(l); 442: tr = pt_expr(r); 443: if (dyaf_on_number(name)){ 444: polytype t_number = mkt_number(); 445: unify(tl, t_number, &u); 446: p_release(u); 447: unify(tr, t_number, &u); 448: p_release(u); 449: tf = t_number; 450: } 451: else if (is_string(name, "^")) { 452: polytype t_text = mkt_text(); 453: unify(tl, t_text, &u); 454: p_release(u); 455: unify(tr, t_text, &u); 456: p_release(u); 457: tf = t_text; 458: } 459: else if (is_string(name, "^^")) { 460: polytype t_text = mkt_text(), t_number = mkt_number(); 461: unify(tl, t_text, &u); 462: p_release(u); 463: unify(tr, t_number, &u); 464: p_release(u); p_release(t_number); 465: tf = t_text; 466: } 467: else if (is_string(name, "<<") 468: || 469: is_string(name, "><") 470: || 471: is_string(name, ">>")) 472: { 473: polytype t_number = mkt_number(); 474: unify(tr, t_number, &u); 475: p_release(u); p_release(t_number); 476: tf = mkt_text(); 477: } 478: else if (is_string(name, "#")) { 479: polytype t_tlt_l = mkt_tlt(p_copy(tl)); 480: unify(tr, t_tlt_l, &u); 481: p_release(t_tlt_l); p_release(u); 482: tf = mkt_number(); 483: } 484: else if (is_string(name, "min") || is_string(name, "max")) { 485: polytype t_tlt_l = mkt_tlt(p_copy(tl)); 486: unify(tr, t_tlt_l, &u); 487: tf = p_copy(asctype(u)); 488: p_release(t_tlt_l); p_release(u); 489: } 490: else if (is_string(name, "th'of")) { 491: polytype t_number, t_tlt_x, t_x; 492: t_number = mkt_number(); 493: unify(tl, t_number, &u); 494: p_release(t_number); p_release(u); 495: t_x = mkt_newvar(); 496: t_tlt_x = mkt_tlt(p_copy(t_x)); 497: unify(tr, t_tlt_x, &u); 498: p_release(t_tlt_x); p_release(u); 499: tf = t_x; 500: } 501: else { 502: tf = mkt_newvar(); 503: } 504: 505: p_release(tl); 506: p_release(tr); 507: 508: return tf; 509: } 510: 511: Hidden polytype pt_tag(name) value name; { 512: polytype var; 513: /* 514: * if (is_globalstring(name, "pi") || is_globalstring(name, "e")) 515: * return mkt_number(); 516: * else 517: */ 518: var = mkt_var(copy(name)); 519: add_var(var); 520: return var; 521: } 522: 523: Hidden polytype pt_tformal(name, number) value name, number; { 524: return pt_tag(name); 525: } 526: 527: Hidden polytype pt_tlocal(name, number) value name, number; { 528: return pt_tag(name); 529: } 530: 531: Hidden polytype pt_tglobal(name) value name; { 532: return pt_tag(name); 533: } 534: 535: Hidden polytype pt_tmystery(name, number) value name, number; { 536: return pt_tag(name); 537: } 538: 539: Hidden polytype pt_trefinement(name) value name; { 540: return pt_tag(name); 541: } 542: 543: Hidden polytype pt_tfun(name, fct) value name, fct; { 544: return pt_tag(name); 545: } 546: 547: Hidden polytype pt_tprd(name, fct) value name, fct; { 548: return pt_tag(name); 549: } 550: 551: Hidden polytype pt_number(v, t) value v, t; { 552: return mkt_number(); 553: } 554: 555: Hidden polytype pt_text_dis(q, v) parsetree v; value q; { 556: while(v NE NilTree) { 557: switch (nodetype(v)) { 558: case TEXT_LIT: 559: v = *Branch(v, XLIT_NEXT); 560: break; 561: case TEXT_CONV: 562: p_release(pt_expr(*Branch(v, XCON_EXPR))); 563: v = *Branch(v, XCON_NEXT); 564: break; 565: default: 566: v = NilTree; 567: } 568: } 569: return mkt_text(); 570: } 571: 572: Hidden polytype pt_elt_dis() { 573: return mkt_lt(mkt_newvar()); 574: } 575: 576: Hidden polytype pt_list_dis(e) value e; { 577: intlet k, len= Nfields(e); 578: polytype tres = pt_expr(*Field(e, 0)); 579: for (k = 1; k < len; k++) { 580: polytype te, u; 581: te = pt_expr(*Field(e, k)); 582: unify(te, tres, &u); 583: p_release(te); p_release(tres); 584: tres = u; 585: } 586: return mkt_list(tres); 587: } 588: 589: Hidden polytype pt_range_dis(l, h) parsetree l, h; { 590: polytype tl, th, t_tn, tres, u; 591: t_tn = mkt_tn(); 592: tl = pt_expr(l); 593: unify(tl, t_tn, &tres); 594: p_release(tl); p_release(t_tn); 595: th = pt_expr(h); 596: unify(th, tres, &u); 597: release(th); release(tres); 598: return mkt_list(u); 599: } 600: 601: Hidden polytype pt_tab_dis(e) value e; { 602: intlet k, len= Nfields(e); 603: polytype tresk, tresa; 604: tresk = pt_expr(*Field(e, 0)); 605: tresa = pt_expr(*Field(e, 1)); 606: for (k = 2; k < len; k += 2) { 607: polytype tk, ta, u; 608: tk = pt_expr(*Field(e, k)); 609: unify(tk, tresk, &u); 610: p_release(tk); p_release(tresk); 611: tresk = u; 612: ta = pt_expr(*Field(e, k+1)); 613: unify(ta, tresa, &u); 614: p_release(ta); p_release(tresa); 615: tresa = u; 616: } 617: return mkt_table(tresk, tresa); 618: } 619: 620: Hidden polytype pt_selection(t, k) parsetree t, k; { 621: polytype tt, ta, ttab, u; 622: tt = pt_expr(t); 623: ta = mkt_newvar(); 624: ttab = mkt_table(pt_expr(k), p_copy(ta)); 625: unify(tt, ttab, &u); 626: p_release(tt); p_release(ttab); p_release(u); 627: return ta; 628: } 629: 630: Hidden polytype pt_trim(l, r) parsetree l, r; { 631: polytype tl, tr, t_text, t_number, u; 632: 633: tl = pt_expr(l); 634: t_text = mkt_text(); 635: unify(tl, t_text, &u); 636: p_release(tl); p_release(u); 637: tr = pt_expr(r); 638: t_number = mkt_number(); 639: unify(tr, t_number, &u); 640: p_release(tr); p_release(t_number); p_release(u); 641: return t_text; 642: } 643: 644: Hidden polytype pt_unparsed(v, t) parsetree v, t; { 645: return mkt_newvar(); 646: } 647: 648: /* ******************************************************************** */ 649: /* Type Check tests */ 650: /* ******************************************************************** */ 651: 652: Hidden Procedure tc_test(v) parsetree v; { 653: tc_node(v, tes_tab); 654: } 655: 656: Hidden Procedure tc_compound(c) parsetree c; { 657: tc_test(c); 658: } 659: 660: Hidden Procedure tc_junction(l, r) parsetree l, r; { 661: tc_test(l); 662: tc_test(r); 663: } 664: 665: Hidden Procedure tc_not(r) parsetree r; { 666: tc_test(r); 667: } 668: 669: Hidden Procedure tc_in_quantification(t, e, c) parsetree t, e, c; { 670: polytype t_tlt_t, te, u; 671: 672: t_tlt_t = mkt_tlt(pt_expr(t)); 673: te = pt_expr(e); 674: unify(te, t_tlt_t, &u); 675: p_release(te); p_release(t_tlt_t); p_release(u); 676: 677: tc_test(c); 678: } 679: 680: Hidden Procedure tc_p_quantification(t, e, c) parsetree t, e, c; { 681: intlet k, len; 682: value ct; /* the Collateral Tag in t */ 683: polytype t_text, te, u; 684: 685: t_text = mkt_text(); 686: 687: ct = *Branch(t, COLL_SEQ); 688: len = Nfields(ct); 689: k_Over_len { 690: polytype ttag; 691: ttag = mkt_var(copy(*Branch(*Field(ct, k), TAG_NAME))); 692: add_var(ttag); 693: unify(ttag, t_text, &u); 694: p_release(ttag); p_release(u); 695: } 696: 697: te = pt_expr(e); 698: unify(te, t_text, &u); 699: p_release(te); p_release(t_text); p_release(u); 700: 701: tc_test(c); 702: } 703: 704: Hidden Procedure tc_tag(name) value name; {} 705: 706: Hidden Procedure tc_tformal(name, number) value name, number; { 707: tc_tag(name); 708: } 709: 710: Hidden Procedure tc_tlocal(name, number) value name, number; { 711: tc_tag(name); 712: } 713: 714: Hidden Procedure tc_tglobal(name) value name; { 715: tc_tag(name); 716: } 717: 718: Hidden Procedure tc_tmystery(name, number) value name, number; { 719: tc_tag(name); 720: } 721: 722: Hidden Procedure tc_trefinement(name) value name; { 723: tc_tag(name); 724: } 725: 726: Hidden Procedure tc_tfun(name, fct) value name, fct; { 727: tc_tag(name); 728: } 729: 730: Hidden Procedure tc_tprd(name, fct) value name, fct; { 731: tc_tag(name); 732: } 733: 734: Hidden Procedure tc_monprd(name, r, pred) parsetree r; value name, pred; { 735: p_release(pt_expr(r)); 736: } 737: 738: Hidden Procedure tc_dyaprd(l, name, r, pred) parsetree l, r; value name, pred; { 739: polytype tl, tr; 740: tl = pt_expr(l); 741: tr = pt_expr(r); 742: if (is_string(name, "in") || is_string(name, "not'in")) { 743: polytype t_tlt_l, u; 744: t_tlt_l = mkt_tlt(p_copy(tl)); 745: unify(tr, t_tlt_l, &u); 746: p_release(t_tlt_l); p_release(u); 747: } 748: p_release(tl); p_release(tr); 749: } 750: 751: Forward polytype pt_relop(); 752: 753: Hidden Procedure tc_relop(l, r) parsetree l, r; { 754: p_release(pt_relop(l, r)); 755: } 756: 757: Hidden polytype pt_relop(l, r) parsetree l, r; { 758: polytype tl, tr, u; 759: 760: if (Comparison(nodetype(l))) 761: tl = pt_relop(*Branch(l, REL_LEFT), *Branch(l, REL_RIGHT)); 762: else 763: tl = pt_expr(l); 764: tr = pt_expr(r); 765: unify(tl, tr, &u); 766: p_release(tl); p_release(tr); 767: return u; 768: } 769: 770: Hidden Procedure tc_unparsed(c, t) parsetree c, t; {} 771: 772: Hidden Procedure uni_bad() { syserr(MESS(2304, "bad uni node in type check")); } 773: Hidden Procedure cmd_bad() { syserr(MESS(2305, "bad cmd node in type check")); } 774: Hidden polytype exp_bad() { syserr(MESS(2306, "bad exp node in type check")); 775: return (polytype) 0; } 776: Hidden Procedure tes_bad() { syserr(MESS(2307, "bad tes node in type check")); } 777: 778: Visible Procedure inittyp() { 779: int i; 780: for (i= 0; i<TABSIZE; i++) { 781: uni_tab[i]= uni_bad; 782: cmd_tab[i]= cmd_bad; 783: exp_tab[i]= exp_bad; 784: tes_tab[i]= tes_bad; 785: } 786: 787: uni_tab[HOW_TO]= tc_howto_unit; 788: uni_tab[YIELD]= tc_yield_unit; 789: uni_tab[TEST]= tc_test_unit; 790: uni_tab[REFINEMENT]= tc_refinement; 791: 792: cmd_tab[SUITE]= tc_suite; 793: cmd_tab[PUT]= tc_put; 794: cmd_tab[INSERT]= tc_ins_rem; 795: cmd_tab[REMOVE]= tc_ins_rem; 796: cmd_tab[CHOOSE]= tc_choose; 797: cmd_tab[DRAW]= tc_draw; 798: cmd_tab[SET_RANDOM]= tc_set_random; 799: cmd_tab[DELETE]= tc_delete; 800: cmd_tab[CHECK]= tc_check; 801: cmd_tab[SHARE]= tc_nothing; 802: cmd_tab[WRITE]= tc_write; 803: cmd_tab[READ]= tc_read; 804: cmd_tab[READ_RAW]= tc_raw_read; 805: cmd_tab[IF]= tc_ifwhile; 806: cmd_tab[WHILE]= tc_ifwhile; 807: cmd_tab[FOR]= tc_for; 808: cmd_tab[SELECT]= tc_select; 809: cmd_tab[TEST_SUITE]= tc_tes_suite; 810: cmd_tab[ELSE]= tc_else; 811: cmd_tab[QUIT]= tc_nothing; 812: cmd_tab[RETURN]= tc_return; 813: cmd_tab[REPORT]= tc_report; 814: cmd_tab[SUCCEED]= tc_nothing; 815: cmd_tab[FAIL]= tc_nothing; 816: cmd_tab[USER_COMMAND]= tc_user_command; 817: cmd_tab[EXTENDED_COMMAND]= tc_nothing; 818: exp_tab[TAG]= pt_tag; 819: tes_tab[TAG]= tc_tag; 820: exp_tab[TAGformal]= pt_tformal; 821: tes_tab[TAGformal]= tc_tformal; 822: exp_tab[TAGlocal]= pt_tlocal; 823: tes_tab[TAGlocal]= tc_tlocal; 824: exp_tab[TAGglobal]= pt_tglobal; 825: tes_tab[TAGglobal]= tc_tglobal; 826: exp_tab[TAGmystery]= pt_tmystery; 827: tes_tab[TAGmystery]= tc_tmystery; 828: exp_tab[TAGrefinement]= pt_trefinement; 829: tes_tab[TAGrefinement]= tc_trefinement; 830: exp_tab[TAGzerfun]= pt_tfun; 831: tes_tab[TAGzerfun]= tc_tfun; 832: exp_tab[TAGzerprd]= pt_tprd; 833: tes_tab[TAGzerprd]= tc_tprd; 834: 835: exp_tab[COMPOUND]= pt_compound; 836: tes_tab[COMPOUND]= tc_compound; 837: exp_tab[COLLATERAL]= pt_collateral; 838: exp_tab[SELECTION]= pt_selection; 839: exp_tab[BEHEAD]= pt_trim; 840: exp_tab[CURTAIL]= pt_trim; 841: 842: exp_tab[UNPARSED]= pt_unparsed; 843: tes_tab[UNPARSED]= tc_unparsed; 844: 845: exp_tab[MONF]= pt_monf; 846: exp_tab[DYAF]= pt_dyaf; 847: exp_tab[NUMBER]= pt_number; 848: exp_tab[TEXT_DIS]= pt_text_dis; 849: exp_tab[ELT_DIS]= pt_elt_dis; 850: exp_tab[LIST_DIS]= pt_list_dis; 851: exp_tab[RANGE_DIS]= pt_range_dis; 852: exp_tab[TAB_DIS]= pt_tab_dis; 853: 854: tes_tab[AND]= tc_junction; 855: tes_tab[OR]= tc_junction; 856: tes_tab[NOT]= tc_not; 857: tes_tab[SOME_IN]= tc_in_quantification; 858: tes_tab[EACH_IN]= tc_in_quantification; 859: tes_tab[NO_IN]= tc_in_quantification; 860: tes_tab[SOME_PARSING]= tc_p_quantification; 861: tes_tab[EACH_PARSING]= tc_p_quantification; 862: tes_tab[NO_PARSING]= tc_p_quantification; 863: tes_tab[MONPRD]= tc_monprd; 864: tes_tab[DYAPRD]= tc_dyaprd; 865: tes_tab[LESS_THAN]= tc_relop; 866: tes_tab[AT_MOST]= tc_relop; 867: tes_tab[GREATER_THAN]= tc_relop; 868: tes_tab[AT_LEAST]= tc_relop; 869: tes_tab[EQUAL]= tc_relop; 870: tes_tab[UNEQUAL]= tc_relop; 871: }