prop-src/setltype.cc

   1 ///////////////////////////////////////////////////////////////////////////////
   2 //  This file is generated automatically using Prop (version 2.3.6),
   3 //  last updated on Nov 2, 1999.
   4 //  The original source file is "setltype.pcc".
   5 ///////////////////////////////////////////////////////////////////////////////
   6
   7 #define PROP_TUPLE2_USED
   8 #include <propdefs.h>
   9 #line 1 "setltype.pcc"
  10 ///////////////////////////////////////////////////////////////////////////////
  11 //
  12 //  This file implements the type checker for the SETL-like sublanguage.
  13 //
  14 ///////////////////////////////////////////////////////////////////////////////
  15 #include "ir.h"
  16 #include "ast.h"
  17 #include "setl-ast.h"
  18 #include "setlgen.h"
  19 #include "type.h"
  20 #include "env.h"
  21
  22 ///////////////////////////////////////////////////////////////////////////////
  23 //
  24 //  Method to elaborate a definition.
  25 //
  26 ///////////////////////////////////////////////////////////////////////////////
  27 Env type_of (Def def, const Env& E)
  28 {
  29    return E;
  30 }
  31
  32 ///////////////////////////////////////////////////////////////////////////////
  33 //
  34 //  Method to elaborate a definition list.
  35 //
  36 ///////////////////////////////////////////////////////////////////////////////
  37 Env type_of (Defs defs, const Env& E)
  38 {
  39    return E;
  40 }
  41
  42 ///////////////////////////////////////////////////////////////////////////////
  43 //
  44 //  Method to unify two expressions type.
  45 //
  46 ///////////////////////////////////////////////////////////////////////////////
  47 Bool unify (Exp exp, Ty a, Ty b)
  48 {  if (! unify(a,b))
  49    {  error("%Ltype mismatch in expression: %f\n"
  50             "%Lexpecting '%T' but found '%T'\n",exp,a,b);
  51       return false;
  52    }
  53    return true;
  54 }
  55
  56 ///////////////////////////////////////////////////////////////////////////////
  57 //
  58 //  Method to infer the type of an expression.
  59 //
  60 ///////////////////////////////////////////////////////////////////////////////
  61 Ty type_of (Exp exp, const Env& E)
  62 {  Ty ty = NOty;
  63
  64 #line 54 "setltype.pcc"
  65 #line 111 "setltype.pcc"
  66 {
  67    if (exp) {
  68       switch (exp->tag__) {
  69          case a_Exp::tag_LITERALexp: {
  70 #line 56 "setltype.pcc"
  71            ty = type_of(((Exp_LITERALexp *)exp)->LITERALexp);
  72 #line 56 "setltype.pcc"
  73             } break;
  74          case a_Exp::tag_IDexp: {
  75 #line 57 "setltype.pcc"
  76            ty = mkvar();
  77 #line 57 "setltype.pcc"
  78             } break;
  79          case a_Exp::tag_RELexp: {
  80 #line 66 "setltype.pcc"
  81            ty = mkvar();
  82 #line 66 "setltype.pcc"
  83             } break;
  84          case a_Exp::tag_DOTexp: {
  85 #line 67 "setltype.pcc"
  86            ty = component_ty(type_of(((Exp_DOTexp *)exp)->_1,E),((Exp_DOTexp *)exp)->_2);
  87 #line 67 "setltype.pcc"
  88             } break;
  89          case a_Exp::tag_SELECTORexp: {
  90 #line 68 "setltype.pcc"
  91            ty = component_ty(type_of(((Exp_SELECTORexp *)exp)->_1,E),((Exp_SELECTORexp *)exp)->_2);
  92 #line 68 "setltype.pcc"
  93             } break;
  94          case a_Exp::tag_DEREFexp: {
  95 #line 69 "setltype.pcc"
  96            ty = mkvar();
  97 #line 69 "setltype.pcc"
  98             } break;
  99          case a_Exp::tag_ARROWexp: {
 100 #line 70 "setltype.pcc"
 101            ty = mkvar();
 102 #line 70 "setltype.pcc"
 103             } break;
 104          case a_Exp::tag_INDEXexp: {
 105 #line 71 "setltype.pcc"
 106            ty = mkvar();
 107 #line 71 "setltype.pcc"
 108             } break;
 109          case a_Exp::tag_BINOPexp: {
 110 #line 72 "setltype.pcc"
 111            ty = mkvar();
 112 #line 72 "setltype.pcc"
 113             } break;
 114          case a_Exp::tag_PREFIXexp: {
 115 #line 73 "setltype.pcc"
 116            ty = mkvar();
 117 #line 73 "setltype.pcc"
 118             } break;
 119          case a_Exp::tag_POSTFIXexp: {
 120 #line 74 "setltype.pcc"
 121            ty = mkvar();
 122 #line 74 "setltype.pcc"
 123             } break;
 124          case a_Exp::tag_APPexp: {
 125 #line 75 "setltype.pcc"
 126            ty = mkvar();
 127 #line 75 "setltype.pcc"
 128             } break;
 129          case a_Exp::tag_ASSIGNexp: {
 130 #line 76 "setltype.pcc"
 131            ty = mkvar();
 132 #line 76 "setltype.pcc"
 133             } break;
 134          case a_Exp::tag_IFexp: {
 135 #line 77 "setltype.pcc"
 136            ty = mkvar();
 137 #line 77 "setltype.pcc"
 138             } break;
 139          case a_Exp::tag_TUPLEexp: {
 140 #line 78 "setltype.pcc"
 141            return mktuplety(type_of(((Exp_TUPLEexp *)exp)->TUPLEexp,E));
 142 #line 78 "setltype.pcc"
 143             } break;
 144          case a_Exp::tag_EXTUPLEexp: {
 145 #line 79 "setltype.pcc"
 146            return extuplety(type_of(((Exp_EXTUPLEexp *)exp)->EXTUPLEexp,E));
 147 #line 79 "setltype.pcc"
 148             } break;
 149          case a_Exp::tag_RECORDexp: {
 150 #line 81 "setltype.pcc"
 151
 152 #line 81 "setltype.pcc"
 153 Tuple2<Ids, Tys>
 154 #line 81 "setltype.pcc"
 155            t = type_of(((Exp_RECORDexp *)exp)->RECORDexp,E);
 156             return mkrecordty(t._1,t._2,false);
 157             } break;
 158          case a_Exp::tag_LISTexp: {
 159             if (((Exp_LISTexp *)exp)->_1) {
 160 #line 86 "setltype.pcc"
 161              Tys head_tys = type_of(((Exp_LISTexp *)exp)->_3,E);
 162                 Ty  tail_ty  = type_of(((Exp_LISTexp *)exp)->_4,E);
 163                 Ty  arg_ty   = mkvar();
 164                 for_each (Ty, one_ty, head_tys)
 165                    unify(exp, one_ty, arg_ty);
 166                        Ty fun_ty   = inst(((Exp_LISTexp *)exp)->_1->cons_ty);
 167                 ty = mkvar();
 168                 unify(exp,fun_ty,mkfunty(mktuplety(
 169 #line 93 "setltype.pcc"
 170 #line 93 "setltype.pcc"
 171                list_1_(arg_ty,list_1_(mkvar()))
 172 #line 93 "setltype.pcc"
 173 #line 93 "setltype.pcc"
 174                ),ty));
 175                if (((Exp_LISTexp *)exp)->_4 != NOexp) unify(exp, tail_ty, ty);
 176
 177 #line 95 "setltype.pcc"
 178             } else {
 179                L1:;
 180 #line 111 "setltype.pcc"
 181               ty = NOty;
 182 #line 111 "setltype.pcc"
 183             }
 184             } break;
 185          case a_Exp::tag_VECTORexp: {
 186 #line 96 "setltype.pcc"
 187            return mkvar();
 188 #line 96 "setltype.pcc"
 189             } break;
 190          case a_Exp::tag_CONSexp: {
 191             if (((Exp_CONSexp *)exp)->_1) {
 192                if (((Exp_CONSexp *)exp)->_3) {
 193 #line 62 "setltype.pcc"
 194                 Ty fun_ty   = inst(((Exp_CONSexp *)exp)->_1->cons_ty);
 195                         ty = mkvar();
 196                         unify(exp,fun_ty,mkfunty(type_of(((Exp_CONSexp *)exp)->_3,E),ty));
 197
 198 #line 65 "setltype.pcc"
 199                } else {
 200 #line 60 "setltype.pcc"
 201                 ty = inst(((Exp_CONSexp *)exp)->_1->cons_ty);
 202 #line 60 "setltype.pcc"
 203                }
 204             } else { goto L1; }
 205             } break;
 206          case a_Exp::tag_CASTexp: {
 207 #line 97 "setltype.pcc"
 208            type_of(((Exp_CASTexp *)exp)->_2,E); return ((Exp_CASTexp *)exp)->_1;
 209 #line 97 "setltype.pcc"
 210             } break;
 211          case a_Exp::tag_QUALexp: {
 212 #line 98 "setltype.pcc"
 213            return mkvar();
 214 #line 98 "setltype.pcc"
 215             } break;
 216          case a_Exp::tag_EQexp: {
 217 #line 99 "setltype.pcc"
 218            return bool_ty;
 219 #line 99 "setltype.pcc"
 220             } break;
 221          case a_Exp::tag_UNIFYexp: {
 222 #line 100 "setltype.pcc"
 223            return NOty;
 224 #line 100 "setltype.pcc"
 225             } break;
 226          case a_Exp::tag_LTexp: {
 227 #line 101 "setltype.pcc"
 228            return bool_ty;
 229 #line 101 "setltype.pcc"
 230             } break;
 231          case a_Exp::tag_HASHexp: {
 232 #line 102 "setltype.pcc"
 233            return integer_ty;
 234 #line 102 "setltype.pcc"
 235             } break;
 236          case a_Exp::tag_THISCOSTexp: {
 237 #line 103 "setltype.pcc"
 238            return integer_ty;
 239 #line 103 "setltype.pcc"
 240             } break;
 241          case a_Exp::tag_COSTexp: {
 242 #line 104 "setltype.pcc"
 243            return integer_ty;
 244 #line 104 "setltype.pcc"
 245             } break;
 246          case a_Exp::tag_THISSYNexp: {
 247 #line 105 "setltype.pcc"
 248            return ((Exp_THISSYNexp *)exp)->_2;
 249 #line 105 "setltype.pcc"
 250             } break;
 251          case a_Exp::tag_SYNexp: {
 252 #line 106 "setltype.pcc"
 253            return ((Exp_SYNexp *)exp)->_3;
 254 #line 106 "setltype.pcc"
 255             } break;
 256          case a_Exp::tag_SENDexp: {
 257 #line 84 "setltype.pcc"
 258            return mkvar();
 259 #line 84 "setltype.pcc"
 260             } break;
 261          case a_Exp::tag_SETLexp: {
 262 #line 107 "setltype.pcc"
 263            ty = NOty;
 264 #line 107 "setltype.pcc"
 265             } break;
 266          case a_Exp::tag_LISTCOMPexp: {
 267 #line 108 "setltype.pcc"
 268            ty = NOty;
 269 #line 108 "setltype.pcc"
 270             } break;
 271          case a_Exp::tag_FORALLexp: {
 272 #line 109 "setltype.pcc"
 273            ty = NOty;
 274 #line 109 "setltype.pcc"
 275             } break;
 276          case a_Exp::tag_EXISTSexp: {
 277 #line 110 "setltype.pcc"
 278            ty = NOty;
 279 #line 110 "setltype.pcc"
 280             } break;
 281          default: {
 282 #line 58 "setltype.pcc"
 283            ((Exp_MARKEDexp *)exp)->_1.set_loc(); ty = type_of(((Exp_MARKEDexp *)exp)->_2,E);
 284 #line 58 "setltype.pcc"
 285             } break;
 286       }
 287    } else {
 288 #line 55 "setltype.pcc"
 289      ty = NOty;
 290 #line 55 "setltype.pcc"
 291    }
 292 }
 293 #line 112 "setltype.pcc"
 294 #line 112 "setltype.pcc"
 295
 296    ty = deref(ty);
 297    if (boxed(exp)) exp->ty = ty;
 298    return ty;
 299 }
 300
 301 ///////////////////////////////////////////////////////////////////////////////
 302 //
 303 //  Method to infer the type of an expression list.
 304 //
 305 ///////////////////////////////////////////////////////////////////////////////
 306 Tys type_of (Exps es, const Env& E)
 307 {
 308 #line 124 "setltype.pcc"
 309 #line 126 "setltype.pcc"
 310 {
 311    if (es) {
 312 #line 126 "setltype.pcc"
 313       return list_1_(type_of(es->_1,E),type_of(es->_2,E));
 314 #line 126 "setltype.pcc"
 315    } else {
 316 #line 125 "setltype.pcc"
 317       return nil_1_;
 318 #line 125 "setltype.pcc"
 319    }
 320 }
 321 #line 127 "setltype.pcc"
 322 #line 127 "setltype.pcc"
 323
 324 }
 325
 326 ///////////////////////////////////////////////////////////////////////////////
 327 //
 328 //  Method to infer the type of an labeled expression list.
 329 //
 330 ///////////////////////////////////////////////////////////////////////////////
 331 #line 135 "setltype.pcc"
 332 Tuple2<Ids, Tys>
 333 #line 135 "setltype.pcc"
 334  type_of (LabExps es, const Env& E)
 335 {  Ids labels =
 336 #line 136 "setltype.pcc"
 337 nil_1_
 338 #line 136 "setltype.pcc"
 339 #line 136 "setltype.pcc"
 340 ;
 341    Tys tys    =
 342 #line 137 "setltype.pcc"
 343 #line 137 "setltype.pcc"
 344 nil_1_
 345 #line 137 "setltype.pcc"
 346 #line 137 "setltype.pcc"
 347 ;
 348
 349 #line 138 "setltype.pcc"
 350 #line 143 "setltype.pcc"
 351 {
 352    for (;;) {
 353       if (es) {
 354 #line 140 "setltype.pcc"
 355         labels =
 356 #line 140 "setltype.pcc"
 357 #line 140 "setltype.pcc"
 358          list_1_(es->_1.label,labels)
 359 #line 140 "setltype.pcc"
 360 #line 140 "setltype.pcc"
 361          ;
 362                 tys    =
 363 #line 141 "setltype.pcc"
 364 #line 141 "setltype.pcc"
 365          list_1_(type_of(es->_1.exp,E),tys)
 366 #line 141 "setltype.pcc"
 367 #line 141 "setltype.pcc"
 368          ;
 369                 es = es->_2;
 370
 371 #line 143 "setltype.pcc"
 372       } else { goto L2; }
 373    }
 374    L2:;
 375 }
 376 #line 144 "setltype.pcc"
 377 #line 144 "setltype.pcc"
 378
 379    return
 380 #line 145 "setltype.pcc"
 381 #line 145 "setltype.pcc"
 382 mkTuple2(labels,tys)
 383 #line 145 "setltype.pcc"
 384 #line 145 "setltype.pcc"
 385 ;
 386 }
 387
 388 ///////////////////////////////////////////////////////////////////////////////
 389 //
 390 //  Method to infer the type of a statement.
 391 //
 392 ///////////////////////////////////////////////////////////////////////////////
 393 void type_of (Stmt s, const Env& E)
 394 {
 395 #line 154 "setltype.pcc"
 396 #line 165 "setltype.pcc"
 397 {
 398    if (s) {
 399       switch (s->tag__) {
 400          case a_Stmt::tag_ASSIGNstmt: {} break;
 401          case a_Stmt::tag_BLOCKstmt: {} break;
 402          case a_Stmt::tag_WHILEstmt: {} break;
 403          case a_Stmt::tag_IFstmt: {} break;
 404          case a_Stmt::tag_MATCHstmt: {} break;
 405          case a_Stmt::tag_REWRITEstmt: {} break;
 406          case a_Stmt::tag_REPLACEMENTstmt: {} break;
 407          case a_Stmt::tag_FORALLstmt: {} break;
 408          default: {} break;
 409       }
 410    } else {}
 411 }
 412 #line 165 "setltype.pcc"
 413 #line 165 "setltype.pcc"
 414
 415 }
 416
 417 ///////////////////////////////////////////////////////////////////////////////
 418 //
 419 //  Method to infer the type of a list of statements.
 420 //
 421 ///////////////////////////////////////////////////////////////////////////////
 422 void type_of (Stmts ss, const Env& E)
 423 {
 424 #line 174 "setltype.pcc"
 425 #line 175 "setltype.pcc"
 426 {
 427    for (;;) {
 428       if (ss) {
 429 #line 175 "setltype.pcc"
 430         type_of(ss->_1,E); ss = ss->_2;
 431 #line 175 "setltype.pcc"
 432       } else { goto L3; }
 433    }
 434    L3:;
 435 }
 436 #line 176 "setltype.pcc"
 437 #line 176 "setltype.pcc"
 438
 439 }
 440 #line 178 "setltype.pcc"
 441 /*
 442 ------------------------------- Statistics -------------------------------
 443 Merge matching rules         = yes
 444 Number of DFA nodes merged   = 43
 445 Number of ifs generated      = 8
 446 Number of switches generated = 2
 447 Number of labels             = 1
 448 Number of gotos              = 1
 449 Adaptive matching            = enabled
 450 Fast string matching         = disabled
 451 Inline downcasts             = enabled
 452 --------------------------------------------------------------------------
 453 */