small improvements to typechecking, especially of C tails

Author: AndrewTolmach

interp_Lint.py

@@ -24,12 +24,16 @@ def interp_stmt(s):
             print(interp_exp(arg))
         case Expr(value):
             interp_exp(value)
+        case _:
+            raise Exception('error in interp_stmt, unexpected ' + repr(s))
 
 def interp(p):
     match p:
         case Module(body):
             for s in body:
                 interp_stmt(s)
+        case _:
+            raise Exception('error in interp, unexpected ' + repr(p))
 
 # This version is for InterpLvar to inherit from 
 class InterpLint:
@@ -77,6 +81,8 @@ def interp(self, p):
     match p:
       case Module(body):
         self.interp_stmts(body, {})
+      case _:
+        raise Exception('error in interp, unexpected ' + repr(p))
 
 if __name__ == "__main__":
   eight = Constant(8)

type_check_Cfun.py

@@ -31,7 +31,11 @@ def type_check_exp(self, e, env):
         return super().type_check_exp(e, env)      
       case Call(Name('len'), [tup]):
         return super().type_check_exp(e, env)      
-      case Call(Name('array_len'), [tup]):
+      case Call(Name('array_len'), _):
+        return super().type_check_exp(e, env)      
+      case Call(Name('array_store'), _):
+        return super().type_check_exp(e, env)      
+      case Call(Name('array_load'), _):
         return super().type_check_exp(e, env)      
       case Call(func, args):
         func_t = self.type_check_exp(func, env)
@@ -49,6 +53,15 @@ def type_check_exp(self, e, env):
       case _:
         return super().type_check_exp(e, env)
 
+  def type_check_tail(self, s, env):
+    match s:
+      case Return(value):
+        return self.type_check_exp(value, env)
+      case TailCall(func, args):
+        return self.type_check_exp(Call(func, args), env)
+      case _:
+        super().type_check_tail(s, env)
+
   def type_check_def(self, d, env):
     match d:
       case FunctionDef(name, params, blocks, dl, returns, comment):
@@ -58,26 +71,24 @@ def type_check_def(self, d, env):
         while True:
             old_env = copy.deepcopy(new_env)
             for (l,ss) in blocks.items():
-                self.type_check_stmts(ss, new_env)
+                self.type_check_stmts(ss[:-1], new_env)
+                if len(ss) > 0:  # blocks should only be empty if they are unreachable, but we don't check this 
+                    t = self.type_check_tail(ss[-1], new_env)
+                    if t != None:  # block ended in Return with this type
+                       self.check_type_equal(returns,t,ss[-1])
             # trace('type_check_Cfun iterating ' + repr(new_env))
             if new_env == old_env:
                 break
-        # todo check return type
+        # following is too strong, because in some variants unused variables may never get assigned a type              
+        # undefs = [x for x,t in new_env.items() if t == Bottom()]
+        # if undefs:
+        #    raise Exception('type_check_def: undefined type for ' + str(undefs)) 
         d.var_types = new_env
         # trace('type_check_Cfun var_types for ' + name)
         # trace(d.var_types)
       case _:
         raise Exception('type_check_def: unexpected ' + repr(d))
 
-  def type_check_stmt(self, s, env):
-    match s:
-      case Return(value):
-        self.type_check_exp(value, env)
-      case TailCall(func, args):
-        self.type_check_exp(Call(func, args), env)
-      case _:
-        super().type_check_stmt(s, env)
-    
   def type_check(self, p):
     match p:
       case CProgramDefs(defs):

type_check_Cif.py

@@ -23,7 +23,9 @@ def combine_types(self, t1, t2):
   def type_check_atm(self, e, env):
     match e:
       case Name(id):
-        return env.get(id, Bottom())
+        t = env.get(id, Bottom())
+        env[id] = t    # make sure this gets into the environment for later definedness checking
+        return t
       case Constant(value) if isinstance(value, bool):
         return BoolType()
       case Constant(value) if isinstance(value, int):
@@ -37,13 +39,6 @@ def type_check_exp(self, e, env):
         return self.type_check_atm(e, env)
       case Constant(value):
         return self.type_check_atm(e, env)
-      case IfExp(test, body, orelse):
-        test_t = self.type_check_exp(test, env)
-        self.check_type_equal(BoolType(), test_t, test)
-        body_t = self.type_check_exp(body, env)
-        orelse_t = self.type_check_exp(orelse, env)
-        self.check_type_equal(body_t, orelse_t, e)
-        return body_t
       case BinOp(left, op, right) if isinstance(op, Add) or isinstance(op, Sub):
         l = self.type_check_atm(left, env)
         self.check_type_equal(l, IntType(), e)
@@ -72,11 +67,6 @@ def type_check_exp(self, e, env):
         return BoolType()
       case Call(Name('input_int'), []):
         return IntType()
-      # case Let(Name(x), rhs, body):
-      #   t = self.type_check_exp(rhs, env)
-      #   new_env = dict(env)
-      #   new_env[x] = t
-      #   return self.type_check_exp(body, new_env)
       case Begin(ss, e):
         self.type_check_stmts(ss, env)
         return self.type_check_exp(e, env)
@@ -91,40 +81,44 @@ def type_check_stmt(self, s, env):
     match s:      
       case Assign([lhs], value):
         t = self.type_check_exp(value, env)
-        if lhs.id in env:
-          lhs_ty = env.get(lhs.id, Bottom())
-          self.check_type_equal(lhs_ty, t, s)
-          env[lhs.id] = self.combine_types(t, lhs_ty)
-        else:
-          env[lhs.id] = t
+        lhs_ty = env.get(lhs.id, Bottom())
+        self.check_type_equal(lhs_ty, t, s)
+        env[lhs.id] = self.combine_types(t, lhs_ty)
       case Expr(Call(Name('print'), [arg])):
         t = self.type_check_exp(arg, env)
         self.check_type_equal(t, IntType(), s)
       case Expr(value):
         self.type_check_exp(value, env)
-      case If(Compare(left, [cmp], [right]), body, orelse):
+      case _:
+        raise Exception('error in type_check_stmt, unexpected ' + repr(s))
+    
+  def type_check_tail(self, s, env):
+    match s:      
+      case If(Compare(left, [cmp], [right]), [Goto(_)], [Goto(_)]):
         left_t = self.type_check_atm(left, env)
         right_t = self.type_check_atm(right, env)
         self.check_type_equal(left_t, right_t, s) # not quite strict enough
-        self.type_check_stmts(body, env)
-        self.type_check_stmts(orelse, env)
       case Goto(label):
         pass
       case Return(value):
         value_t = self.type_check_exp(value, env)
       case _:
-        raise Exception('error in type_check_stmt, unexpected ' + repr(s))
-    
+        raise Exception('error in type_check_tail, unexpected' + repr(s))
+
   def type_check(self, p):
     match p:
       case CProgram(body):
           env = {}
           while True:
               old_env = copy.deepcopy(env)
               for (l, ss) in body.items():
-                  self.type_check_stmts(ss, env)
+                  self.type_check_stmts(ss[:-1], env)
+              self.type_check_tail(ss[-1], env)
               if env == old_env:
                   break
+          undefs = [x for x,t in env.items() if t == Bottom()]
+          if undefs:
+              raise Exception('error: undefined type for ' + str(undefs)) 
           p.var_types = env
       case _:
         raise Exception('error in type_check, unexpected ' + repr(p))

type_check_Ctup.py

@@ -57,7 +57,7 @@ def type_check_stmt(self, s, env):
       case Collect(size):
         pass
       case Assign([Subscript(tup, Constant(index), Store())], value):
-        tup_t = self.type_check_atm(tup, env)
+        tup_t = self.type_check_exp(tup, env)
         value_t = self.type_check_atm(value, env)
         match tup_t:
           case TupleType(ts):

type_check_Lfun.py

@@ -99,7 +99,10 @@ def type_check_stmts(self, ss, env):
         else:
             new_params = params
             new_returns = returns
-        for (x,t) in new_params:
+        unique_names = {x for x,_ in new_params}             
+        if len(unique_names) != len(new_params):
+            raise Exception('type_check: duplicate parameter name in function ' + repr(name))
+        for x,t in new_params:
             new_env[x] = t
         rt = self.type_check_stmts(body, new_env)
         self.check_type_equal(new_returns, rt, ss[0])
@@ -121,6 +124,8 @@ def type_check(self, p):
                                 for p in params.args]
                 else:
                     params_t = [t for (x,t) in params]
+                if name in env:
+                    raise Exception('type_check: duplicate function name ' + name)
                 env[name] = FunctionType(params_t, self.parse_type_annot(returns))
         self.type_check_stmts(body, env)
       case _:

type_check_Llambda.py

@@ -19,7 +19,7 @@ def type_check_exp(self, e, env):
       case Closure(arity, es):
         ts = [self.type_check_exp(e, env) for e in es]
         e.has_type = TupleType(ts)
-        return e.has_type
+        return e.has_type  # this is just wrong: closure values with different shapes must be given compatible types
       case Lambda(params, body):
         raise Exception('cannot synthesize a type for lambda: ' + str(e))
       case AllocateClosure(length, typ, arity):

type_check_Ltup.py

@@ -9,7 +9,7 @@ def check_type_equal(self, t1, t2, e):
     match t1:
       case TupleType(ts1):
         match t2:
-          case TupleType(ts2):
+          case TupleType(ts2):  # if len(ts1) == len(ts2):  -- including this breaks Llambda type checking because of bogus treatment of closure types there
             for (ty1, ty2) in zip(ts1,ts2):
               self.check_type_equal(ty1, ty2, e)
           case _:
@@ -51,6 +51,12 @@ def type_check_exp(self, e, env):
       case GlobalValue(name):
         return IntType()
       case Allocate(length, typ):
+        match typ:
+          case TupleType(_):
+            e.has_type = typ
+            return typ
+          case _:
+            raise Exception('type_check_exp: Allocate expected a tuple, not ' + repr(typ))
         return typ
       case _:
         return super().type_check_exp(e, env)