prop-src/setltype.pcc

   1 ///////////////////////////////////////////////////////////////////////////////
   2 //
   3 //  This file implements the type checker for the SETL-like sublanguage.
   4 //
   5 ///////////////////////////////////////////////////////////////////////////////
   6 #include "ir.ph"
   7 #include "ast.ph"
   8 #include "setl-ast.ph"
   9 #include "setlgen.h"
  10 #include "type.h"
  11 #include "env.h"
  12
  13 ///////////////////////////////////////////////////////////////////////////////
  14 //
  15 //  Method to elaborate a definition.
  16 //
  17 ///////////////////////////////////////////////////////////////////////////////
  18 Env type_of (Def def, const Env& E)
  19 {
  20    return E;
  21 }
  22
  23 ///////////////////////////////////////////////////////////////////////////////
  24 //
  25 //  Method to elaborate a definition list.
  26 //
  27 ///////////////////////////////////////////////////////////////////////////////
  28 Env type_of (Defs defs, const Env& E)
  29 {
  30    return E;
  31 }
  32
  33 ///////////////////////////////////////////////////////////////////////////////
  34 //
  35 //  Method to unify two expressions type.
  36 //
  37 ///////////////////////////////////////////////////////////////////////////////
  38 Bool unify (Exp exp, Ty a, Ty b)
  39 {  if (! unify(a,b))
  40    {  error("%Ltype mismatch in expression: %f\n"
  41             "%Lexpecting '%T' but found '%T'\n",exp,a,b);
  42       return false;
  43    }
  44    return true;
  45 }
  46
  47 ///////////////////////////////////////////////////////////////////////////////
  48 //
  49 //  Method to infer the type of an expression.
  50 //
  51 ///////////////////////////////////////////////////////////////////////////////
  52 Ty type_of (Exp exp, const Env& E)
  53 {  Ty ty = NOty;
  54    match (exp) of
  55      NOexp:                   { ty = NOty; }
  56    | LITERALexp l:            { ty = type_of(l); }
  57    | IDexp id:                { ty = mkvar(); }
  58    | MARKEDexp(l, e):         { l.set_loc(); ty = type_of(e,E); }
  59    | CONSexp(ONEcons { cons_ty ... }, _, NOexp):
  60      {  ty = inst(cons_ty); }
  61    | CONSexp(ONEcons { cons_ty ... }, _, e):
  62      {  Ty fun_ty   = inst(cons_ty);
  63         ty = mkvar();
  64         unify(exp,fun_ty,mkfunty(type_of(e,E),ty));
  65      }
  66    | RELexp     i:            { ty = mkvar(); }
  67    | DOTexp     (e, id):      { ty = component_ty(type_of(e,E),id); }
  68    | SELECTORexp(e, cons,t):  { ty = component_ty(type_of(e,E),cons); }
  69    | DEREFexp   (e):          { ty = mkvar(); }
  70    | ARROWexp   (e, id):      { ty = mkvar(); }
  71    | INDEXexp   (e, i):       { ty = mkvar(); }
  72    | BINOPexp   (id, a, b):   { ty = mkvar(); }
  73    | PREFIXexp  (id, e):      { ty = mkvar(); }
  74    | POSTFIXexp (id, e):      { ty = mkvar(); }
  75    | APPexp     (f, a):       { ty = mkvar(); }
  76    | ASSIGNexp  (a, b):       { ty = mkvar(); }
  77    | IFexp      (c, yes, no): { ty = mkvar(); }
  78    | TUPLEexp   (es):         { return mktuplety(type_of(es,E)); }
  79    | EXTUPLEexp (es):         { return extuplety(type_of(es,E)); }
  80    | RECORDexp  (es):
  81      { .[Ids, Tys] t = type_of(es,E);
  82        return mkrecordty(t.#1,t.#2,false);
  83      }
  84    | SENDexp    (id, es):     { return mkvar(); }
  85    | LISTexp    (ONEcons { cons_ty = cons_ty ... }, _, hd, tl):
  86      {  Tys head_tys = type_of(hd,E);
  87         Ty  tail_ty  = type_of(tl,E);
  88         Ty  arg_ty   = mkvar();
  89         for_each (Ty, one_ty, head_tys)
  90            unify(exp, one_ty, arg_ty);
  91         Ty fun_ty   = inst(cons_ty);
  92         ty = mkvar();
  93         unify(exp,fun_ty,mkfunty(mktuplety(#[arg_ty,mkvar()]),ty));
  94         if (tl != NOexp) unify(exp, tail_ty, ty);
  95      }
  96    | VECTORexp  (c, es):      { return mkvar(); }
  97    | CASTexp    (ty,e):       { type_of(e,E); return ty; }
  98    | QUALexp    (ty,id):      { return mkvar(); }
  99    | EQexp      (ty, a, b):   { return bool_ty; }
 100    | UNIFYexp   (ty, a, b):   { return NOty; }
 101    | LTexp      (ty, a, b):   { return bool_ty; }
 102    | HASHexp    (ty, e):      { return integer_ty; }
 103    | THISCOSTexp _:           { return integer_ty; }
 104    | COSTexp    (childno):    { return integer_ty; }
 105    | THISSYNexp (ruleno,ty,_):          { return ty; }
 106    | SYNexp     (childno, ruleno,ty,_): { return ty; }
 107    | SETLexp    (op,es):      { ty = NOty; }
 108    | LISTCOMPexp{ ... }:      { ty = NOty; }
 109    | FORALLexp  (id,exp):     { ty = NOty; }
 110    | EXISTSexp  (id,exp):     { ty = NOty; }
 111    | _:                       { ty = NOty; }
 112    end match;
 113    ty = deref(ty);
 114    if (boxed(exp)) exp->ty = ty;
 115    return ty;
 116 }
 117
 118 ///////////////////////////////////////////////////////////////////////////////
 119 //
 120 //  Method to infer the type of an expression list.
 121 //
 122 ///////////////////////////////////////////////////////////////////////////////
 123 Tys type_of (Exps es, const Env& E)
 124 {  match (es) of
 125       #[]:         return #[];
 126    |  #[h ... t]:  return #[type_of(h,E) ... type_of(t,E)];
 127    end match;
 128 }
 129
 130 ///////////////////////////////////////////////////////////////////////////////
 131 //
 132 //  Method to infer the type of an labeled expression list.
 133 //
 134 ///////////////////////////////////////////////////////////////////////////////
 135 .[Ids,Tys] type_of (LabExps es, const Env& E)
 136 {  Ids labels = #[];
 137    Tys tys    = #[];
 138    match while (es)
 139    {  #[{ label, exp } ... t]:
 140       { labels = #[ label ... labels ];
 141         tys    = #[ type_of(exp,E) ... tys ];
 142         es = t;
 143       }
 144    }
 145    return .(labels,tys);
 146 }
 147
 148 ///////////////////////////////////////////////////////////////////////////////
 149 //
 150 //  Method to infer the type of a statement.
 151 //
 152 ///////////////////////////////////////////////////////////////////////////////
 153 void type_of (Stmt s, const Env& E)
 154 {  match (s)
 155    {  NOstmt:
 156    |  ASSIGNstmt  (a, b):
 157    |  BLOCKstmt   (_,stmts):
 158    |  WHILEstmt   (e, s):
 159    |  IFstmt      (e, yes, no):
 160    |  FORALLstmt  (bindings, s):
 161    |  RETURNstmt e:
 162    |  MATCHstmt  d:
 163    |  REWRITEstmt d:
 164    |  REPLACEMENTstmt d:
 165    }
 166 }
 167
 168 ///////////////////////////////////////////////////////////////////////////////
 169 //
 170 //  Method to infer the type of a list of statements.
 171 //
 172 ///////////////////////////////////////////////////////////////////////////////
 173 void type_of (Stmts ss, const Env& E)
 174 {  match while (ss)
 175    {  #[h ... t]:  { type_of(h,E); ss = t; }
 176    }
 177 }