tests: update with newly reported judgements

make visitor accept calls more explicit with type_of(), resolve_type_expr() and process_stmt()

examples/01_simple_type_checking/04_complex_types.midas

@@ -1,8 +1,8 @@
 type Meter = float
 
 extend Meter {
-    def __add__: fn(Meter) -> Meter
-    def __sub__: fn(Meter) -> Meter
+    def __add__: fn(Meter, /) -> Meter
+    def __sub__: fn(Meter, /) -> Meter
 }
 
 type Coordinate = object

midas/checker/builtins.midas

@@ -57,7 +57,7 @@ extend int {
     def conjugate: fn() -> int
     def bit_length: fn() -> int
     def bit_count: fn() -> int
-    def to_bytes: fn(length: int?, byteorder: str?, *, signed: bool?) -> bytes
+    // def to_bytes: fn(length: int?, byteorder: str?, *, signed: bool?) -> bytes
 
     def __add__: fn(value: int, /) -> int
     def __sub__: fn(value: int, /) -> int

midas/checker/python.py

@@ -78,6 +78,12 @@ class PythonTyper(
         self.judgements.append((expr, type))
         return type
 
+    def resolve_type_expr(self, expr: p.MidasType) -> Type:
+        return expr.accept(self)
+
+    def process_stmt(self, stmt: p.Stmt) -> None:
+        stmt.accept(self)
+
     def process_block(self, block: list[p.Stmt], env: Environment) -> bool:
         """Evaluate a sequence of statements
 
@@ -93,7 +99,7 @@ class PythonTyper(
         returned: bool = False
         for i, stmt in enumerate(block):
             try:
-                stmt.accept(self)
+                self.process_stmt(stmt)
             except ReturnException:
                 returned = True
                 if i < len(block) - 1:
@@ -111,7 +117,7 @@ class PythonTyper(
             statements (list[p.Stmt]): the statements to evaluate and check
         """
         for stmt in statements:
-            stmt.accept(self)
+            self.process_stmt(stmt)
 
         self.logger.debug(f"Final environment: {self.env.flat_dict()}")
 
@@ -144,9 +150,9 @@ class PythonTyper(
 
         def eval_arg_type(arg: p.Function.Argument) -> Type:
             if arg.type is not None:
-                return arg.type.accept(self)
+                return self.resolve_type_expr(arg.type)
             if arg.default is not None:
-                return arg.default.accept(self)
+                return self.type_of(arg.default)
             return UnknownType()
 
         pos: int = 0
@@ -186,7 +192,7 @@ class PythonTyper(
 
         returns_hint: Optional[Type] = None
         if stmt.returns is not None:
-            returns_hint = stmt.returns.accept(self)
+            returns_hint = self.resolve_type_expr(stmt.returns)
             # Early define to handle simple fully-typed recursion
             inside_function: Function = Function(
                 pos_args=pos_args,
@@ -232,7 +238,7 @@ class PythonTyper(
 
     def visit_type_assign(self, stmt: p.TypeAssign) -> None:
         # TODO check not yet defined locally
-        type: Type = stmt.type.accept(self)
+        type: Type = self.resolve_type_expr(stmt.type)
         self.env.define(stmt.name, type)
 
     def visit_assign_stmt(self, stmt: p.AssignStmt) -> None:
@@ -287,7 +293,7 @@ class PythonTyper(
             )
 
     def visit_return_stmt(self, stmt: p.ReturnStmt) -> None:
-        type: Type = stmt.value.accept(self) if stmt.value is not None else UnitType()
+        type: Type = self.type_of(stmt.value) if stmt.value is not None else UnitType()
         self.env.return_types.append(type)
         raise ReturnException()
 
@@ -297,7 +303,7 @@ class PythonTyper(
         # if (m := 1 + 1) < 2:
         #     ...
         # print(m)  # <- m is still defined
-        test_type: Type = stmt.test.accept(self)
+        test_type: Type = self.type_of(stmt.test)
 
         # TODO Allow subtypes or any type
         if test_type != self.types.get_type("bool"):
@@ -320,39 +326,8 @@ class PythonTyper(
                 expr.location, f"Unsupported operator {expr.operator}"
             )
             return UnknownType()
-        left: Type = self.type_of(expr.left)
-        right: Type = self.type_of(expr.right)
 
-        operation: Optional[Type] = self.types.lookup_member(left, method)
-        if operation is None:
-            self.reporter.error(
-                expr.location,
-                f"Undefined operation {method} between {left} and {right}",
-            )
-            return UnknownType()
-
-        match operation:
-            case Function() as function:
-                if not self._is_binary_function(function):
-                    self.reporter.error(
-                        expr.location,
-                        f"Wrong definition of binary operation. Expected function with 1 positional-only parameters, got {function}",
-                    )
-                    return UnknownType()
-
-                rhs: Function.Argument = function.pos_args[0]
-                if not self.is_subtype(right, rhs.type):
-                    self.reporter.error(
-                        expr.location,
-                        f"Wrong type for right-hand side, expected {rhs.type}, got {right}",
-                    )
-                    return UnknownType()
-                return function.returns
-            case _:
-                self.reporter.warning(
-                    expr.location, f"Unsupported operation {operation}"
-                )
-                return UnknownType()
+        return self._visit_binary_expr(expr.location, expr.left, expr.right, method)
 
     def visit_compare_expr(self, expr: p.CompareExpr) -> Type:
         method: Optional[str] = COMPARATOR_METHODS.get(expr.operator.__class__)
@@ -362,17 +337,43 @@ class PythonTyper(
                 expr.location, f"Unsupported operator {expr.operator}"
             )
             return UnknownType()
-        left: Type = self.type_of(expr.left)
-        right: Type = self.type_of(expr.right)
 
-        result: Optional[Type] = self.types.get_operation_result(left, method, right)
-        if result is None:
+        return self._visit_binary_expr(expr.location, expr.left, expr.right, method)
+
+    def _visit_binary_expr(
+        self, location: Location, left_expr: p.Expr, right_expr: p.Expr, method: str
+    ) -> Type:
+        left: Type = self.type_of(left_expr)
+        right: Type = self.type_of(right_expr)
+
+        operation: Optional[Type] = self.types.lookup_member(left, method)
+        if operation is None:
             self.reporter.error(
-                expr.location,
+                location,
                 f"Undefined operation {method} between {left} and {right}",
             )
             return UnknownType()
-        return result
+
+        match operation:
+            case Function() as function:
+                if not self._is_binary_function(function):
+                    self.reporter.error(
+                        location,
+                        f"Wrong definition of binary operation. Expected function with 1 positional-only parameters, got {function}",
+                    )
+                    return UnknownType()
+
+                rhs: Function.Argument = function.pos_args[0]
+                if not self.is_subtype(right, rhs.type):
+                    self.reporter.error(
+                        location,
+                        f"Wrong type for right-hand side, expected {rhs.type}, got {right}",
+                    )
+                    return UnknownType()
+                return function.returns
+            case _:
+                self.reporter.warning(location, f"Unsupported operation {operation}")
+                return UnknownType()
 
     def visit_unary_expr(self, expr: p.UnaryExpr) -> Type: ...
 
@@ -424,8 +425,8 @@ class PythonTyper(
         return type or UnknownType()
 
     def visit_logical_expr(self, expr: p.LogicalExpr) -> Type:
-        left: Type = expr.left.accept(self)
-        right: Type = expr.right.accept(self)
+        left: Type = self.type_of(expr.left)
+        right: Type = self.type_of(expr.right)
 
         if self.is_subtype(left, right):
             return right
@@ -439,10 +440,10 @@ class PythonTyper(
         return UnknownType()
 
     def visit_cast_expr(self, expr: p.CastExpr) -> Type:
-        return expr.type.accept(self)
+        return self.resolve_type_expr(expr.type)
 
     def visit_ternary_expr(self, expr: p.TernaryExpr) -> Type:
-        test_type: Type = expr.test.accept(self)
+        test_type: Type = self.type_of(expr.test)
 
         # TODO Allow subtypes or any type
         if test_type != self.types.get_type("bool"):
@@ -450,8 +451,8 @@ class PythonTyper(
                 expr.test.location, f"If test must be a boolean, got {test_type}"
             )
 
-        true_type: Type = expr.if_true.accept(self)
-        false_type: Type = expr.if_false.accept(self)
+        true_type: Type = self.type_of(expr.if_true)
+        false_type: Type = self.type_of(expr.if_false)
         if self.is_subtype(true_type, false_type):
             return false_type
         if self.is_subtype(false_type, true_type):
@@ -489,7 +490,7 @@ class PythonTyper(
             return UnknownType()
 
         if node.param is not None:
-            param: Type = node.param.accept(self)
+            param: Type = self.resolve_type_expr(node.param)
             return self.types.apply_generic(base, [param])
         return base
 

midas/checker/registry.py

@@ -352,6 +352,12 @@ class TypesRegistry:
 
     def lookup_member(self, type: Type, member_name: str) -> Optional[Type]:
         match type:
+            case BaseType(name=name):
+                if name in self._members:
+                    if member_name in self._members[name]:
+                        return self._members[name][member_name]
+                return None
+
             case AliasType(name=name, type=base):
                 if name in self._members:
                     if member_name in self._members[name]:

tests/cases/checker/02_simple_operations.py.ref.json

@@ -13,6 +13,20 @@
         ]
       },
       "message": "Cannot assign str to variable 'c' of type int"
+    },
+    {
+      "type": "Error",
+      "location": {
+        "start": [
+          9,
+          4
+        ],
+        "end": [
+          9,
+          9
+        ]
+      },
+      "message": "Undefined operation __add__ between bool and bool"
     }
   ],
   "judgments": [
@@ -158,9 +172,7 @@
           "name": "d"
         }
       },
-      "type": {
-        "name": "int"
-      }
+      "type": {}
     },
     {
       "location": {

tests/cases/checker/03_functions.py.ref.json

@@ -254,6 +254,19 @@
     }
   ],
   "judgments": [
+    {
+      "location": {
+        "from": "L2:11",
+        "to": "L2:15"
+      },
+      "expr": {
+        "_type": "LiteralExpr",
+        "value": true
+      },
+      "type": {
+        "name": "bool"
+      }
+    },
     {
       "location": {
         "from": "L5:5",
@@ -264,7 +277,6 @@
         "name": "foo"
       },
       "type": {
-        "name": "foo",
         "pos_args": [
           {
             "pos": 0,
@@ -328,7 +340,6 @@
         "name": "foo"
       },
       "type": {
-        "name": "foo",
         "pos_args": [
           {
             "pos": 0,
@@ -410,7 +421,6 @@
         "name": "foo"
       },
       "type": {
-        "name": "foo",
         "pos_args": [
           {
             "pos": 0,
@@ -509,7 +519,6 @@
         "name": "foo"
       },
       "type": {
-        "name": "foo",
         "pos_args": [
           {
             "pos": 0,
@@ -609,7 +618,6 @@
         "name": "foo"
       },
       "type": {
-        "name": "foo",
         "pos_args": [
           {
             "pos": 0,
@@ -725,7 +733,6 @@
         "name": "foo"
       },
       "type": {
-        "name": "foo",
         "pos_args": [
           {
             "pos": 0,
@@ -842,7 +849,6 @@
         "name": "foo"
       },
       "type": {
-        "name": "foo",
         "pos_args": [
           {
             "pos": 0,
@@ -924,7 +930,6 @@
         "name": "foo"
       },
       "type": {
-        "name": "foo",
         "pos_args": [
           {
             "pos": 0,
@@ -1006,7 +1011,6 @@
         "name": "foo"
       },
       "type": {
-        "name": "foo",
         "pos_args": [
           {
             "pos": 0,
@@ -1123,7 +1127,6 @@
         "name": "foo"
       },
       "type": {
-        "name": "foo",
         "pos_args": [
           {
             "pos": 0,
@@ -1240,7 +1243,6 @@
         "name": "foo"
       },
       "type": {
-        "name": "foo",
         "pos_args": [
           {
             "pos": 0,
@@ -1357,7 +1359,6 @@
         "name": "foo"
       },
       "type": {
-        "name": "foo",
         "pos_args": [
           {
             "pos": 0,

tests/cases/checker/04_custom_types.midas

@@ -3,12 +3,12 @@ type Second = float
 type MeterPerSecond = float
 
 extend Meter {
-    op __add__(Meter) -> Meter
-    op __sub__(Meter) -> Meter
-    op __truediv__(Second) -> MeterPerSecond
+    def __add__: fn(Meter, /) -> Meter
+    def __sub__: fn(Meter, /) -> Meter
+    def __truediv__: fn(Second, /) -> MeterPerSecond
 }
 
 extend Second {
-    op __add__(Second) -> Second
-    op __sub__(Second) -> Second
+    def __add__: fn(Second, /) -> Second
+    def __sub__: fn(Second, /) -> Second
 }

tests/cases/checker/05_control_flow.py.ref.json

@@ -70,6 +70,27 @@
         "name": "int"
       }
     },
+    {
+      "location": {
+        "from": "L2:11",
+        "to": "L2:16"
+      },
+      "expr": {
+        "_type": "BinaryExpr",
+        "left": {
+          "_type": "VariableExpr",
+          "name": "a"
+        },
+        "operator": "+",
+        "right": {
+          "_type": "VariableExpr",
+          "name": "b"
+        }
+      },
+      "type": {
+        "name": "int"
+      }
+    },
     {
       "location": {
         "from": "L5:7",
@@ -96,6 +117,27 @@
         "name": "int"
       }
     },
+    {
+      "location": {
+        "from": "L5:7",
+        "to": "L5:12"
+      },
+      "expr": {
+        "_type": "CompareExpr",
+        "left": {
+          "_type": "VariableExpr",
+          "name": "a"
+        },
+        "operator": "<",
+        "right": {
+          "_type": "VariableExpr",
+          "name": "b"
+        }
+      },
+      "type": {
+        "name": "bool"
+      }
+    },
     {
       "location": {
         "from": "L6:15",
@@ -122,6 +164,27 @@
         "name": "int"
       }
     },
+    {
+      "location": {
+        "from": "L6:15",
+        "to": "L6:20"
+      },
+      "expr": {
+        "_type": "BinaryExpr",
+        "left": {
+          "_type": "VariableExpr",
+          "name": "b"
+        },
+        "operator": "-",
+        "right": {
+          "_type": "VariableExpr",
+          "name": "a"
+        }
+      },
+      "type": {
+        "name": "int"
+      }
+    },
     {
       "location": {
         "from": "L8:15",
@@ -148,6 +211,27 @@
         "name": "int"
       }
     },
+    {
+      "location": {
+        "from": "L8:15",
+        "to": "L8:20"
+      },
+      "expr": {
+        "_type": "BinaryExpr",
+        "left": {
+          "_type": "VariableExpr",
+          "name": "a"
+        },
+        "operator": "-",
+        "right": {
+          "_type": "VariableExpr",
+          "name": "b"
+        }
+      },
+      "type": {
+        "name": "int"
+      }
+    },
     {
       "location": {
         "from": "L15:7",
@@ -174,6 +258,27 @@
         "name": "int"
       }
     },
+    {
+      "location": {
+        "from": "L15:7",
+        "to": "L15:13"
+      },
+      "expr": {
+        "_type": "CompareExpr",
+        "left": {
+          "_type": "VariableExpr",
+          "name": "a"
+        },
+        "operator": ">",
+        "right": {
+          "_type": "LiteralExpr",
+          "value": 10
+        }
+      },
+      "type": {
+        "name": "bool"
+      }
+    },
     {
       "location": {
         "from": "L16:15",
@@ -200,6 +305,40 @@
         "name": "int"
       }
     },
+    {
+      "location": {
+        "from": "L16:15",
+        "to": "L16:21"
+      },
+      "expr": {
+        "_type": "BinaryExpr",
+        "left": {
+          "_type": "VariableExpr",
+          "name": "a"
+        },
+        "operator": "-",
+        "right": {
+          "_type": "LiteralExpr",
+          "value": 10
+        }
+      },
+      "type": {
+        "name": "int"
+      }
+    },
+    {
+      "location": {
+        "from": "L18:15",
+        "to": "L18:16"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "a"
+      },
+      "type": {
+        "name": "int"
+      }
+    },
     {
       "location": {
         "from": "L22:7",
@@ -226,6 +365,27 @@
         "name": "int"
       }
     },
+    {
+      "location": {
+        "from": "L22:7",
+        "to": "L22:12"
+      },
+      "expr": {
+        "_type": "CompareExpr",
+        "left": {
+          "_type": "VariableExpr",
+          "name": "a"
+        },
+        "operator": "<",
+        "right": {
+          "_type": "VariableExpr",
+          "name": "b"
+        }
+      },
+      "type": {
+        "name": "bool"
+      }
+    },
     {
       "location": {
         "from": "L23:15",
@@ -251,6 +411,40 @@
       "type": {
         "name": "int"
       }
+    },
+    {
+      "location": {
+        "from": "L23:15",
+        "to": "L23:20"
+      },
+      "expr": {
+        "_type": "BinaryExpr",
+        "left": {
+          "_type": "VariableExpr",
+          "name": "b"
+        },
+        "operator": "-",
+        "right": {
+          "_type": "VariableExpr",
+          "name": "a"
+        }
+      },
+      "type": {
+        "name": "int"
+      }
+    },
+    {
+      "location": {
+        "from": "L25:15",
+        "to": "L25:21"
+      },
+      "expr": {
+        "_type": "LiteralExpr",
+        "value": "oops"
+      },
+      "type": {
+        "name": "str"
+      }
     }
   ]
 }

tests/cases/checker/06_subtyping.py

@@ -9,4 +9,4 @@ def maximum(a: float, b: float):
 
 
 v3 = maximum(v1, v2)
-v3 = v1 + v2
+v3 = v2 + v1

tests/cases/checker/06_subtyping.py.ref.json

@@ -53,6 +53,53 @@
         "name": "float"
       }
     },
+    {
+      "location": {
+        "from": "L6:7",
+        "to": "L6:12"
+      },
+      "expr": {
+        "_type": "CompareExpr",
+        "left": {
+          "_type": "VariableExpr",
+          "name": "b"
+        },
+        "operator": ">",
+        "right": {
+          "_type": "VariableExpr",
+          "name": "a"
+        }
+      },
+      "type": {
+        "name": "bool"
+      }
+    },
+    {
+      "location": {
+        "from": "L7:15",
+        "to": "L7:16"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "b"
+      },
+      "type": {
+        "name": "float"
+      }
+    },
+    {
+      "location": {
+        "from": "L8:11",
+        "to": "L8:12"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "a"
+      },
+      "type": {
+        "name": "float"
+      }
+    },
     {
       "location": {
         "from": "L11:5",
@@ -63,7 +110,6 @@
         "name": "maximum"
       },
       "type": {
-        "name": "maximum",
         "pos_args": [],
         "args": [
           {
@@ -149,10 +195,10 @@
       },
       "expr": {
         "_type": "VariableExpr",
-        "name": "v1"
+        "name": "v2"
       },
       "type": {
-        "name": "int"
+        "name": "float"
       }
     },
     {
@@ -162,10 +208,10 @@
       },
       "expr": {
         "_type": "VariableExpr",
-        "name": "v2"
+        "name": "v1"
       },
       "type": {
-        "name": "float"
+        "name": "int"
       }
     },
     {
@@ -177,12 +223,12 @@
         "_type": "BinaryExpr",
         "left": {
           "_type": "VariableExpr",
-          "name": "v1"
+          "name": "v2"
         },
         "operator": "+",
         "right": {
           "_type": "VariableExpr",
-          "name": "v2"
+          "name": "v1"
         }
       },
       "type": {

tests/cases/midas-parser/01_simple_types.midas

@@ -10,8 +10,8 @@ type Difference[T] = T
 
 // Complex custom type, containing two values accessible through properties
 type GeoLocation = {
-    lat: Latitude
-    lon: Longitude
+    prop lat: Latitude
+    prop lon: Longitude
 }
 
 // Define operations on our custom type
@@ -19,23 +19,23 @@ extend GeoLocation {
     // This type is compatible with the `-` operation with another GeoLocation
     // i.e. you can subtract a GeoLocation from another GeoLocation, resulting
     // in a Difference of GeoLocations
-    op __sub__(GeoLocation) -> Difference[GeoLocation]
+    def __sub__: fn(GeoLocation, /) -> Difference[GeoLocation]
 }
 
 // For complex generics, you need to specify how the genericity the properties
 // are handled
 type Difference[GeoLocation] = {
-    lat: Difference[Latitude]
-    lon: Difference[Longitude]
+    prop lat: Difference[Latitude]
+    prop lon: Difference[Longitude]
 }
 
 // Simple operation defined on our custom types
 extend Latitude {
-    op __sub__(Latitude) -> Difference[Latitude]
+    def __sub__: fn(Latitude, /) -> Difference[Latitude]
 }
 
 extend Longitude {
-    op __sub__(Longitude) -> Difference[Longitude]
+    def __sub__: fn(Longitude, /) -> Difference[Longitude]
 }
 
 // Predefined custom predicates that can be referenced in other definitions
@@ -45,13 +45,13 @@ predicate Equatorial(loc: GeoLocation) = (-10 <= loc.lat <= 10)
 predicate Arctic(loc: GeoLocation) = (loc.lat >= 66)
 
 type Person = {
-    name: str
+    prop name: str
 
     // Property with an inline constraint
-    age: Optional[int where (0 <= _ < 150)]
+    prop age: Optional[int where (0 <= _ < 150)]
 
     // Property referencing a predicate
-    height: float where StrictlyPositive
+    prop height: float where StrictlyPositive
 
-    home: GeoLocation
+    prop home: GeoLocation
 }