feat(checker): handle assignments to attributes

add type judgements to checker test results and update all tests (including the new subtyping rules)

README.md

@@ -5,3 +5,82 @@
 *Midas* aims at providing Python developers with a simple annotation system to enable compile-time integrity and data type checks, as well as generating runtime assertions.
 
 This framework is being developed as part of a Bachelor's Thesis by Louis Heredero at HEI Sion.
+
+## Requirements
+
+- Python 3.11+
+- [uv](https://docs.astral.sh/uv/getting-started/installation/)
+
+## Installation
+
+1. Clone the repository
+   ```shell
+   git clone https://git.kb28.ch/HEL/midas.git
+   ```
+2. Go in the project directory
+   ```shell
+   cd midas
+   ```
+3. Install the CLI as a user-wide tool
+   ```shell
+   uv tool install .
+   ```
+4. You can now run the `midas` command from anywhere
+   ```shell
+   midas --help
+   ```
+
+## Commands
+
+### Compiling
+
+> [!NOTE]
+> In the current state of the project, the `compile` command doesn't generate any runnable code, it only runs the parsers and type checker on the provided files
+
+```shell
+midas compile -t types.midas source.py
+```
+
+With the `compile` command, you can process a source Python file, with any number of custom type definition files (`-t FILE` option), and the type checker will verify the coherence of your program and generate the runnable code with valid syntax and runtime assertions.
+
+The optional `-l FILE` option lets you produce a highlighted version of the source code showing diagnostics from the type checker (see [Highlighting](#highlighting))
+
+### Highlighting
+
+```shell
+midas utils highlight source.py
+# or
+midas utils highlight types.midas
+```
+
+The `highlight` command takes in a source file (Python or Midas), runs the appropriate parser and outputs an HTML file containing the source code with added highlighting. This highlighting takes the form of hoverable annotations showing some of the parsed structures (e.g. a function definition, an assignment, a generic type, etc.)
+
+The optional `-o FILE` option can be used to specify an output path. By default, the file is printed in stdout (equivalent to `-o -`).
+
+### Dumping the AST
+
+```shell
+midas utils dump-ast source.py
+# or
+midas utils dump-ast types.midas
+```
+
+For debugging purposes, you can output the AST parsed from a Python or Midas file. For Python files, the `-p` flags lets you toggle the custom AST parsing. Without `-p`, the raw AST is returned, as produced by the builtin `ast` module. This flag has no effect on Midas files.
+
+The optional `-o FILE` option can be used to specify an output path. By default, the file is printed in stdout (equivalent to `-o -`).
+
+## Tests
+
+Several snapshot tests are available to assert the good behaviour of the parsers and type checker. They can be run as follows:
+
+```shell
+uv run -m tests.midas run -a
+uv run -m tests.python run -a
+uv run -m tests.checker run -a
+```
+
+**Available subcommands:**
+- Run all tests: `run -a`
+- Run specific tests: `run tests/cases/test1.py tests/cases/test2.py ...`
+- Update all tests: `update -a`
+- Update specific tests: `update tests/cases/test1.py tests/cases/test2.py ...`

examples/00_syntax_prototype/02_custom_types.py

@@ -2,10 +2,6 @@
 # ruff: disable[F821]
 from __future__ import annotations
 
-# Prototype of custom type import to use valid Python syntax
-import midas
-midas.using("02_custom_types.midas")
-
 # A data-frame using a custom type
 df: Frame[
     location: GeoLocation

examples/00_syntax_prototype/05_custom_types_v3.midas

@@ -0,0 +1,33 @@
+type Foo1 = float
+type Foo2 = float where (_ > 3)
+type Foo3 = int | float
+type Foo4 = int where (_ > 3) | float where (_ > 3)
+type Foo5 = (int | float) where (_ > 3)
+type Foo6 = {
+    foo: float
+    bar: float where (_ > 3)
+}
+
+type Foo7[T] = T where (_ > 3)
+type Foo8[A, B<:int] = {
+    a: A
+    b: B
+}
+
+type Complex = {
+    a: int
+    b: int
+}
+type Complex2 = Complex where (_.a > 3 & _.b < 5)
+
+predicate Positive(n: int) = n >= 0
+
+extend Foo1 {
+    op __add__(Foo1) -> Foo1
+}
+
+extend Foo7[T] {
+    op __add__(Foo7[T]) -> Foo7[T]
+}
+
+type Optional[T] = None | T

examples/01_simple_type_checking/02_simple_types.midas

@@ -1,6 +1,6 @@
-type Meter(float)
-type Second(float)
-type MeterPerSecond(float)
+type Meter = float
+type Second = float
+type MeterPerSecond = float
 
 extend Meter {
     op __add__(Meter) -> Meter

examples/01_simple_type_checking/02_simple_types.py

@@ -1,8 +1,6 @@
 # type: ignore
 # ruff: disable [F821]
 
-midas.using("02_simple_types.midas")
-
 distance: Meter = cast(Meter, 123.45)
 time: Second = cast(Second, 6.7)
 speed = distance / time

examples/01_simple_type_checking/03_control_flow.py

@@ -4,13 +4,20 @@ def minimum(x: int, y: int):
     else:
         return y
 
+
 a = 15
 b = 72
 c = minimum(a, b)
 
+
 def factorial(n: int) -> int:
     if n <= 1:
         return 1
     return n * factorial(n - 1)
 
-category = "Category 1" if a < 10 else "Category 2"
+
+category = "Category 1" if a < 10 else "Category 2"
+
+
+def foo() -> None:
+    pass

examples/01_simple_type_checking/04_complex_types.midas

@@ -0,0 +1,11 @@
+type Meter = float
+
+extend Meter {
+    op __add__(Meter) -> Meter
+    op __sub__(Meter) -> Meter
+}
+
+type Coordinate = {
+    x: Meter
+    y: Meter
+}

examples/01_simple_type_checking/04_complex_types.py

@@ -0,0 +1,11 @@
+# type: ignore
+# ruff: disable [F821]
+p1: Coordinate
+p2: Coordinate
+
+diff_x = p2.x - p1.x
+diff_y = p2.y - p1.y
+
+dist = diff_x + diff_y
+
+p2.x += cast(Meter, 1)

gen/midas.py

@@ -13,40 +13,38 @@ from midas.lexer.token import Token
 
 
 ###> Stmt | Statements
-class SimpleTypeStmt:
+class TypeStmt:
     name: Token
-    template: Optional[TemplateExpr]
-    base: TypeExpr
-    constraint: Optional[Expr]
+    params: list[Param]
+    type: Type
 
-
-class ComplexTypeStmt:
-    name: Token
-    template: Optional[TemplateExpr]
-    properties: list[PropertyStmt]
+    @dataclass(frozen=True, kw_only=True)
+    class Param:
+        location: Location
+        name: Token
+        bound: Optional[Type]
 
 
 class PropertyStmt:
     name: Token
-    type: TypeExpr
-    constraint: Optional[Expr]
+    type: Type
 
 
 class ExtendStmt:
-    type: TypeExpr
+    type: Type
     operations: list[OpStmt]
 
 
 class OpStmt:
     name: Token
-    operand: TypeExpr
-    result: TypeExpr
+    operand: Type
+    result: Type
 
 
 class PredicateStmt:
     name: Token
     subject: Token
-    type: TypeExpr
+    type: Type
     condition: Expr
 
 
@@ -54,9 +52,6 @@ class PredicateStmt:
 
 
 ###> Expr | Expressions
-class SimpleTypeExpr:
-    name: Token
-    optional: bool
 
 
 class LogicalExpr:
@@ -97,14 +92,27 @@ class WildcardExpr:
     token: Token
 
 
-class TemplateExpr:
-    type: TypeExpr
+###<
+
+###> Type | Types
 
 
-class TypeExpr:
+class NamedType:
     name: Token
-    template: Optional[TemplateExpr]
-    optional: bool
+
+
+class GenericType:
+    type: Type
+    params: list[Type]
+
+
+class ConstraintType:
+    type: Type
+    constraint: Expr
+
+
+class ComplexType:
+    properties: list[PropertyStmt]
 
 
 ###<

gen/python.py

@@ -128,12 +128,6 @@ class LogicalExpr:
     right: Expr
 
 
-class SetExpr:
-    object: Expr
-    name: str
-    value: Expr
-
-
 class CastExpr:
     type: MidasType
     expr: Expr

midas/ast/midas.py

@@ -28,10 +28,7 @@ class Stmt(ABC):
 
     class Visitor(ABC, Generic[T]):
         @abstractmethod
-        def visit_simple_type_stmt(self, stmt: SimpleTypeStmt) -> T: ...
-
-        @abstractmethod
-        def visit_complex_type_stmt(self, stmt: ComplexTypeStmt) -> T: ...
+        def visit_type_stmt(self, stmt: TypeStmt) -> T: ...
 
         @abstractmethod
         def visit_property_stmt(self, stmt: PropertyStmt) -> T: ...
@@ -47,31 +44,25 @@ class Stmt(ABC):
 
 
 @dataclass(frozen=True)
-class SimpleTypeStmt(Stmt):
+class TypeStmt(Stmt):
     name: Token
-    template: Optional[TemplateExpr]
-    base: TypeExpr
-    constraint: Optional[Expr]
+    params: list[Param]
+    type: Type
+
+    @dataclass(frozen=True, kw_only=True)
+    class Param:
+        location: Location
+        name: Token
+        bound: Optional[Type]
 
     def accept(self, visitor: Stmt.Visitor[T]) -> T:
-        return visitor.visit_simple_type_stmt(self)
-
-
-@dataclass(frozen=True)
-class ComplexTypeStmt(Stmt):
-    name: Token
-    template: Optional[TemplateExpr]
-    properties: list[PropertyStmt]
-
-    def accept(self, visitor: Stmt.Visitor[T]) -> T:
-        return visitor.visit_complex_type_stmt(self)
+        return visitor.visit_type_stmt(self)
 
 
 @dataclass(frozen=True)
 class PropertyStmt(Stmt):
     name: Token
-    type: TypeExpr
-    constraint: Optional[Expr]
+    type: Type
 
     def accept(self, visitor: Stmt.Visitor[T]) -> T:
         return visitor.visit_property_stmt(self)
@@ -79,7 +70,7 @@ class PropertyStmt(Stmt):
 
 @dataclass(frozen=True)
 class ExtendStmt(Stmt):
-    type: TypeExpr
+    type: Type
     operations: list[OpStmt]
 
     def accept(self, visitor: Stmt.Visitor[T]) -> T:
@@ -89,8 +80,8 @@ class ExtendStmt(Stmt):
 @dataclass(frozen=True)
 class OpStmt(Stmt):
     name: Token
-    operand: TypeExpr
-    result: TypeExpr
+    operand: Type
+    result: Type
 
     def accept(self, visitor: Stmt.Visitor[T]) -> T:
         return visitor.visit_op_stmt(self)
@@ -100,7 +91,7 @@ class OpStmt(Stmt):
 class PredicateStmt(Stmt):
     name: Token
     subject: Token
-    type: TypeExpr
+    type: Type
     condition: Expr
 
     def accept(self, visitor: Stmt.Visitor[T]) -> T:
@@ -120,9 +111,6 @@ class Expr(ABC):
     def accept(self, visitor: Visitor[T]) -> T: ...
 
     class Visitor(ABC, Generic[T]):
-        @abstractmethod
-        def visit_simple_type_expr(self, expr: SimpleTypeExpr) -> T: ...
-
         @abstractmethod
         def visit_logical_expr(self, expr: LogicalExpr) -> T: ...
 
@@ -147,21 +135,6 @@ class Expr(ABC):
         @abstractmethod
         def visit_wildcard_expr(self, expr: WildcardExpr) -> T: ...
 
-        @abstractmethod
-        def visit_template_expr(self, expr: TemplateExpr) -> T: ...
-
-        @abstractmethod
-        def visit_type_expr(self, expr: TypeExpr) -> T: ...
-
-
-@dataclass(frozen=True)
-class SimpleTypeExpr(Expr):
-    name: Token
-    optional: bool
-
-    def accept(self, visitor: Expr.Visitor[T]) -> T:
-        return visitor.visit_simple_type_expr(self)
-
 
 @dataclass(frozen=True)
 class LogicalExpr(Expr):
@@ -233,19 +206,61 @@ class WildcardExpr(Expr):
         return visitor.visit_wildcard_expr(self)
 
 
-@dataclass(frozen=True)
-class TemplateExpr(Expr):
-    type: TypeExpr
+#########
+# Types #
+#########
 
-    def accept(self, visitor: Expr.Visitor[T]) -> T:
-        return visitor.visit_template_expr(self)
+
+@dataclass(frozen=True, kw_only=True)
+class Type(ABC):
+    location: Location
+
+    @abstractmethod
+    def accept(self, visitor: Visitor[T]) -> T: ...
+
+    class Visitor(ABC, Generic[T]):
+        @abstractmethod
+        def visit_named_type(self, type: NamedType) -> T: ...
+
+        @abstractmethod
+        def visit_generic_type(self, type: GenericType) -> T: ...
+
+        @abstractmethod
+        def visit_constraint_type(self, type: ConstraintType) -> T: ...
+
+        @abstractmethod
+        def visit_complex_type(self, type: ComplexType) -> T: ...
 
 
 @dataclass(frozen=True)
-class TypeExpr(Expr):
+class NamedType(Type):
     name: Token
-    template: Optional[TemplateExpr]
-    optional: bool
 
-    def accept(self, visitor: Expr.Visitor[T]) -> T:
-        return visitor.visit_type_expr(self)
+    def accept(self, visitor: Type.Visitor[T]) -> T:
+        return visitor.visit_named_type(self)
+
+
+@dataclass(frozen=True)
+class GenericType(Type):
+    type: Type
+    params: list[Type]
+
+    def accept(self, visitor: Type.Visitor[T]) -> T:
+        return visitor.visit_generic_type(self)
+
+
+@dataclass(frozen=True)
+class ConstraintType(Type):
+    type: Type
+    constraint: Expr
+
+    def accept(self, visitor: Type.Visitor[T]) -> T:
+        return visitor.visit_constraint_type(self)
+
+
+@dataclass(frozen=True)
+class ComplexType(Type):
+    properties: list[PropertyStmt]
+
+    def accept(self, visitor: Type.Visitor[T]) -> T:
+        return visitor.visit_complex_type(self)

midas/ast/printer.py

@@ -85,40 +85,39 @@ class AstPrinter(Generic[T]):
                 child.accept(self)
 
 
-class MidasAstPrinter(AstPrinter, m.Expr.Visitor[None], m.Stmt.Visitor[None]):
+class MidasAstPrinter(
+    AstPrinter, m.Expr.Visitor[None], m.Stmt.Visitor[None], m.Type.Visitor[None]
+):
     # Statements
 
-    def visit_simple_type_stmt(self, stmt: m.SimpleTypeStmt):
-        self._write_line("SimpleTypeStmt")
+    def visit_type_stmt(self, stmt: m.TypeStmt) -> None:
+        self._write_line("TypeStmt")
         with self._child_level():
             self._write_line(f'name: "{stmt.name.lexeme}"')
-            self._write_optional_child("template", stmt.template)
-            self._write_line("base")
-            with self._child_level(single=True):
-                stmt.base.accept(self)
-            self._write_optional_child("constraint", stmt.constraint, last=True)
-
-    def visit_complex_type_stmt(self, stmt: m.ComplexTypeStmt):
-        self._write_line("ComplexTypeStmt")
-        with self._child_level():
-            self._write_line(f'name: "{stmt.name.lexeme}"')
-            self._write_optional_child("template", stmt.template)
-            self._write_line("properties", last=True)
+            self._write_line("params")
             with self._child_level():
-                for i, prop in enumerate(stmt.properties):
+                for i, param in enumerate(stmt.params):
                     self._idx = i
-                    if i == len(stmt.properties) - 1:
+                    if i == len(stmt.params) - 1:
                         self._mark_last()
-                    prop.accept(self)
+                    self._print_type_stmt_param(param)
+            self._write_line("type", last=True)
+            with self._child_level(single=True):
+                stmt.type.accept(self)
+
+    def _print_type_stmt_param(self, param: m.TypeStmt.Param) -> None:
+        self._write_line("Param")
+        with self._child_level():
+            self._write_line(f'name: "{param.name.lexeme}"')
+            self._write_optional_child("bound", param.bound, last=True)
 
     def visit_property_stmt(self, stmt: m.PropertyStmt):
         self._write_line("PropertyStmt")
         with self._child_level():
             self._write_line(f'name: "{stmt.name.lexeme}"')
-            self._write_line("type")
+            self._write_line("type", last=True)
             with self._child_level(single=True):
                 stmt.type.accept(self)
-            self._write_optional_child("constraint", stmt.constraint, last=True)
 
     def visit_extend_stmt(self, stmt: m.ExtendStmt) -> None:
         self._write_line("ExtendStmt")
@@ -161,12 +160,6 @@ class MidasAstPrinter(AstPrinter, m.Expr.Visitor[None], m.Stmt.Visitor[None]):
 
     # Expressions
 
-    def visit_simple_type_expr(self, expr: m.SimpleTypeExpr):
-        self._write_line("SimpleTypeExpr")
-        with self._child_level():
-            self._write_line(f'name: "{expr.name.lexeme}"')
-            self._write_line(f"optional: {expr.optional}", last=True)
-
     def visit_logical_expr(self, expr: m.LogicalExpr):
         self._write_line("LogicalExpr")
         with self._child_level():
@@ -230,22 +223,48 @@ class MidasAstPrinter(AstPrinter, m.Expr.Visitor[None], m.Stmt.Visitor[None]):
     def visit_wildcard_expr(self, expr: m.WildcardExpr) -> None:
         self._write_line("WildcardExpr")
 
-    def visit_template_expr(self, expr: m.TemplateExpr) -> None:
-        self._write_line("TemplateExpr")
-        with self._child_level(single=True):
+    def visit_named_type(self, type: m.NamedType) -> None:
+        self._write_line("NamedType")
+        with self._child_level():
+            self._write_line(f'name: "{type.name.lexeme}"', last=True)
+
+    def visit_generic_type(self, type: m.GenericType) -> None:
+        self._write_line("GenericType")
+        with self._child_level():
+            self._write_line("type")
+            with self._child_level():
+                type.type.accept(self)
+            self._write_line("params", last=True)
+            with self._child_level():
+                for i, param in enumerate(type.params):
+                    self._idx = i
+                    if i == len(type.params) - 1:
+                        self._mark_last()
+                    param.accept(self)
+
+    def visit_constraint_type(self, type: m.ConstraintType) -> None:
+        self._write_line("ConstraintType")
+        with self._child_level():
             self._write_line("type")
             with self._child_level(single=True):
-                expr.type.accept(self)
+                type.type.accept(self)
+            self._write_line("constraint", last=True)
+            with self._child_level(single=True):
+                type.constraint.accept(self)
 
-    def visit_type_expr(self, expr: m.TypeExpr):
-        self._write_line("TypeExpr")
+    def visit_complex_type(self, type: m.ComplexType) -> None:
+        self._write_line("ComplexType")
         with self._child_level():
-            self._write_line(f'name: "{expr.name.lexeme}"')
-            self._write_optional_child("template", expr.template)
-            self._write_line(f"optional: {expr.optional}", last=True)
+            self._write_line("properties", last=True)
+            with self._child_level():
+                for i, prop in enumerate(type.properties):
+                    self._idx = i
+                    if i == len(type.properties) - 1:
+                        self._mark_last()
+                    prop.accept(self)
 
 
-class MidasPrinter(m.Expr.Visitor[str], m.Stmt.Visitor[str]):
+class MidasPrinter(m.Expr.Visitor[str], m.Stmt.Visitor[str], m.Type.Visitor[str]):
     def __init__(self, indent: int = 4):
         self.indent: int = indent
         self.level: int = 0
@@ -253,33 +272,28 @@ class MidasPrinter(m.Expr.Visitor[str], m.Stmt.Visitor[str]):
     def indented(self, text: str) -> str:
         return " " * (self.level * self.indent) + text
 
-    def print(self, expr: m.Expr | m.Stmt):
+    def print(self, expr: m.Expr | m.Stmt | m.Type) -> str:
         self.level = 0
         return expr.accept(self)
 
-    def visit_simple_type_stmt(self, stmt: m.SimpleTypeStmt):
-        template: str = stmt.template.accept(self) if stmt.template is not None else ""
-        res: str = f"type {stmt.name.lexeme}{template}({stmt.base.accept(self)})"
-        if stmt.constraint is not None:
-            res += " where " + stmt.constraint.accept(self)
+    def visit_type_stmt(self, stmt: m.TypeStmt) -> str:
+        template: str = ""
+        if len(stmt.params) != 0:
+            params: list[str] = [
+                self._print_type_template_param(param) for param in stmt.params
+            ]
+            template = f"[{', '.join(params)}]"
+        res: str = f"type {stmt.name.lexeme}{template} = {stmt.type.accept(self)}"
         return self.indented(res)
 
-    def visit_complex_type_stmt(self, stmt: m.ComplexTypeStmt):
-        template: str = stmt.template.accept(self) if stmt.template is not None else ""
-        res: str = self.indented(f"type {stmt.name.lexeme}{template}")
-        res += " {\n"
-        self.level += 1
-        for prop in stmt.properties:
-            res += prop.accept(self)
-            res += "\n"
-        self.level -= 1
-        res += self.indented("}")
+    def _print_type_template_param(self, param: m.TypeStmt.Param) -> str:
+        res: str = param.name.lexeme
+        if param.bound is not None:
+            res += "<:" + param.bound.accept(self)
         return res
 
     def visit_property_stmt(self, stmt: m.PropertyStmt):
         res: str = f"{stmt.name.lexeme}: {stmt.type.accept(self)}"
-        if stmt.constraint is not None:
-            res += " where " + stmt.constraint.accept(self)
         return self.indented(res)
 
     def visit_extend_stmt(self, stmt: m.ExtendStmt):
@@ -289,13 +303,13 @@ class MidasPrinter(m.Expr.Visitor[str], m.Stmt.Visitor[str]):
         for op in stmt.operations:
             res += op.accept(self)
         self.level -= 1
-        res += "\n" + self.indented("}")
+        res += self.indented("}")
         return res
 
     def visit_op_stmt(self, stmt: m.OpStmt):
         operand: str = stmt.operand.accept(self)
         result: str = stmt.result.accept(self)
-        return self.indented(f"op {stmt.name.lexeme}({operand}) -> {result}")
+        return self.indented(f"op {stmt.name.lexeme}({operand}) -> {result}\n")
 
     def visit_predicate_stmt(self, stmt: m.PredicateStmt):
         name: str = stmt.name.lexeme
@@ -304,9 +318,6 @@ class MidasPrinter(m.Expr.Visitor[str], m.Stmt.Visitor[str]):
         condition: str = stmt.condition.accept(self)
         return self.indented(f"predicate {name}({subject}: {type}) = {condition}")
 
-    def visit_simple_type_expr(self, expr: m.SimpleTypeExpr):
-        return f"{expr.name.lexeme}{'?' if expr.optional else ''}"
-
     def visit_logical_expr(self, expr: m.LogicalExpr):
         left: str = expr.left.accept(self)
         operator: str = expr.operator.lexeme
@@ -342,12 +353,30 @@ class MidasPrinter(m.Expr.Visitor[str], m.Stmt.Visitor[str]):
     def visit_wildcard_expr(self, expr: m.WildcardExpr):
         return "_"
 
-    def visit_template_expr(self, expr: m.TemplateExpr):
-        return f"[{expr.type.accept(self)}]"
+    def visit_named_type(self, type: m.NamedType) -> str:
+        return type.name.lexeme
 
-    def visit_type_expr(self, expr: m.TypeExpr):
-        template: str = expr.template.accept(self) if expr.template is not None else ""
-        return f"{expr.name.lexeme}{template}{'?' if expr.optional else ''}"
+    def visit_generic_type(self, type: m.GenericType) -> str:
+        res: str = type.type.accept(self)
+        if len(type.params) != 0:
+            params: list[str] = [param.accept(self) for param in type.params]
+            res += f"[{', '.join(params)}]"
+        return res
+
+    def visit_constraint_type(self, type: m.ConstraintType) -> str:
+        res: str = type.type.accept(self)
+        res += " where " + type.constraint.accept(self)
+        return res
+
+    def visit_complex_type(self, type: m.ComplexType) -> str:
+        res: str = "{\n"
+        self.level += 1
+        for prop in type.properties:
+            res += prop.accept(self)
+            res += "\n"
+        self.level -= 1
+        res += self.indented("}")
+        return res
 
 
 class PythonAstPrinter(
@@ -573,17 +602,6 @@ class PythonAstPrinter(
             with self._child_level(single=True):
                 expr.right.accept(self)
 
-    def visit_set_expr(self, expr: p.SetExpr) -> None:
-        self._write_line("SetExpr")
-        with self._child_level():
-            self._write_line("object")
-            with self._child_level(single=True):
-                expr.object.accept(self)
-            self._write_line(f"name: {expr.name}")
-            self._write_line("value", last=True)
-            with self._child_level(single=True):
-                expr.value.accept(self)
-
     def visit_cast_expr(self, expr: p.CastExpr) -> None:
         self._write_line("CastExpr")
         with self._child_level():
@@ -600,11 +618,11 @@ class PythonAstPrinter(
             self._write_line("test")
             with self._child_level(single=True):
                 expr.test.accept(self)
-            
+
             self._write_line("if_true")
             with self._child_level(single=True):
                 expr.if_true.accept(self)
-            
+
             self._write_line("if_false", last=True)
             with self._child_level(single=True):
                 expr.if_false.accept(self)

midas/ast/python.py

@@ -214,9 +214,6 @@ class Expr(ABC):
         @abstractmethod
         def visit_logical_expr(self, expr: LogicalExpr) -> T: ...
 
-        @abstractmethod
-        def visit_set_expr(self, expr: SetExpr) -> T: ...
-
         @abstractmethod
         def visit_cast_expr(self, expr: CastExpr) -> T: ...
 
@@ -298,16 +295,6 @@ class LogicalExpr(Expr):
         return visitor.visit_logical_expr(self)
 
 
-@dataclass(frozen=True)
-class SetExpr(Expr):
-    object: Expr
-    name: str
-    value: Expr
-
-    def accept(self, visitor: Expr.Visitor[T]) -> T:
-        return visitor.visit_set_expr(self)
-
-
 @dataclass(frozen=True)
 class CastExpr(Expr):
     type: MidasType

midas/checker/builtins.py

@@ -0,0 +1,4 @@
+BUILTIN_SUBTYPES: dict[str, set[str]] = {
+    "float": {"int"},
+    "int": {"bool"},
+}

midas/checker/checker.py

@@ -6,10 +6,20 @@ from typing import Optional
 import midas.ast.midas as m
 import midas.ast.python as p
 from midas.ast.location import Location
+from midas.checker.builtins import BUILTIN_SUBTYPES
 from midas.checker.diagnostic import Diagnostic, DiagnosticType
 from midas.checker.environment import Environment
 from midas.checker.operators import COMPARATOR_METHODS, OPERATOR_METHODS
-from midas.checker.types import BaseType, Function, SimpleType, Type, UnitType, UnknownType
+from midas.checker.types import (
+    AliasType,
+    BaseType,
+    ComplexType,
+    Function,
+    Operation,
+    Type,
+    UnitType,
+    UnknownType,
+)
 from midas.lexer.midas import MidasLexer
 from midas.lexer.token import Token
 from midas.parser.midas import MidasParser
@@ -34,19 +44,26 @@ class Checker(
 ):
     """A type checker which can use custom type definitions"""
 
-    def __init__(self, locals: dict[p.Expr, int], file_path: Path):
+    def __init__(
+        self,
+        locals: dict[p.Expr, int],
+        source_path: Path,
+        types_paths: list[Path],
+    ):
         self.logger: logging.Logger = logging.getLogger("Checker")
-        self.file_path: Path = file_path
+        self.source_path: Path = source_path
+        self.types_paths: list[Path] = types_paths
         self.ctx: MidasResolver = MidasResolver()
         self.global_env: Environment = Environment()
         self.env: Environment = self.global_env
         self.locals: dict[p.Expr, int] = locals
         self.diagnostics: list[Diagnostic] = []
+        self.judgements: list[tuple[p.Expr, Type]] = []
 
     def diagnostic(self, type: DiagnosticType, location: Location, message: str):
         self.diagnostics.append(
             Diagnostic(
-                file_path=self.file_path,
+                file_path=self.source_path,
                 location=location,
                 type=type,
                 message=message,
@@ -74,7 +91,7 @@ class Checker(
             message=message,
         )
 
-    def evaluate(self, expr: p.Expr) -> Type:
+    def type_of(self, expr: p.Expr) -> Type:
         """Evaluate the type of an expression
 
         Args:
@@ -83,15 +100,17 @@ class Checker(
         Returns:
             Type: the type of the given expression
         """
-        return expr.accept(self)
+        type: Type = expr.accept(self)
+        self.judgements.append((expr, type))
+        return type
 
-    def evaluate_block(self, block: list[p.Stmt], env: Environment) -> bool:
+    def process_block(self, block: list[p.Stmt], env: Environment) -> bool:
         """Evaluate a sequence of statements
 
         Args:
             block (list[p.Stmt]): the statements to evaluate
             env (Environment): the environment in which to evaluate
-        
+
         Returns:
             bool: whether a return statement is present in the block
         """
@@ -119,6 +138,12 @@ class Checker(
             list[Diagnostic]: the list of diagnostics (errors, warning, etc.)
         """
         self.diagnostics = []
+
+        for path in self.types_paths:
+            self.import_midas(path)
+        self.logger.debug(f"Midas types: {self.ctx._types}")
+        self.logger.debug(f"Midas operations: {self.ctx._operations}")
+
         for stmt in statements:
             stmt.accept(self)
 
@@ -140,30 +165,6 @@ class Checker(
             return self.env.get_at(distance, name)
         return self.global_env.get(name)
 
-    def parse_midas_import(self, expr: p.CallExpr) -> Optional[Path]:
-        """Parse a Midas import statement
-
-        The statement should be written as `midas.using("path/to/types.midas")`
-
-        Args:
-            expr (p.CallExpr): the import call expression
-
-        Returns:
-            Optional[Path]: the path to the imported file, or None if the expression is malformed
-        """
-        match expr:
-            case p.CallExpr(
-                callee=p.GetExpr(
-                    object=p.VariableExpr(name="midas"),
-                    name="using",
-                ),
-                arguments=[
-                    p.LiteralExpr(value=path),
-                ],
-            ):
-                return Path(path)
-        return None
-
     def import_midas(self, path: Path) -> None:
         """Import Midas definitions from a path
 
@@ -171,17 +172,166 @@ class Checker(
             path (Path): the import path
         """
         self.logger.debug(f"Importing type definitions from {path}")
-        path = (self.file_path.parent / path).resolve()
         lexer: MidasLexer = MidasLexer(path.read_text())
         tokens: list[Token] = lexer.process()
         parser: MidasParser = MidasParser(tokens)
         stmts: list[m.Stmt] = parser.parse()
         self.ctx.resolve(stmts)
-        self.logger.debug(f"Midas types: {self.ctx._types}")
-        self.logger.debug(f"Midas operations: {self.ctx._operations}")
+
+    def unfold_type(self, type: Type) -> Type:
+        match type:
+            case AliasType(type=ref_type):
+                return self.unfold_type(ref_type)
+            case _:
+                return type
+
+    def is_subtype(self, type1: Type, type2: Type) -> bool:
+        """Check whether `type1` is a subtype of `type2`
+
+        For more details on the rules checked here, see TAPL Chap. 15-16-17
+
+        Args:
+            type1 (Type): the potential subtype
+            type2 (Type): the potential supertype
+
+        Returns:
+            bool: whether `type1` is a subtype of `type2`
+        """
+
+        if type1 == type2:
+            return True
+
+        match (type1, type2):
+            case (AliasType(type=base1), _):
+                return self.is_subtype(base1, type2)
+
+            case (BaseType(name=name1), BaseType(name=name2)):
+                return name1 in BUILTIN_SUBTYPES.get(name2, set())
+
+            case (ComplexType(properties=props1), ComplexType(properties=props2)):
+                for k, t in props2.items():
+                    if k not in props1:
+                        return False
+                    if not self.is_subtype(props1[k], t):
+                        return False
+                return True
+
+            case (Function(returns=return1), Function(returns=return2)):
+                if not self.is_func_subtype(type1, type2):
+                    return False
+                if not self.is_subtype(return1, return2):
+                    return False
+                return True
+
+        return False
+
+    # TODO: verify the logic in here
+    def is_func_subtype(self, func1: Function, func2: Function) -> bool:
+        """Check whether a function is a subtype of another
+
+        Args:
+            func1 (Function): the potential function subtype
+            func2 (Function): the potential function supertype
+
+        Returns:
+            bool: whether `func1` is a subtype of `func2`
+        """
+        if not self.is_subtype(func1.returns, func2.returns):
+            return False
+
+        pos1: list[Function.Argument] = func1.pos_args
+        mixed1: list[Function.Argument] = func1.args
+        kw1: dict[str, Function.Argument] = {a.name: a for a in func1.kw_args}
+        pos2: list[Function.Argument] = func2.pos_args
+        mixed2: list[Function.Argument] = func2.args
+        kw2: dict[str, Function.Argument] = {a.name: a for a in func2.kw_args}
+
+        mixed_by_pos: dict[int, Function.Argument] = {arg.pos: arg for arg in mixed2}
+        mixed_by_name: dict[str, Function.Argument] = {arg.name: arg for arg in mixed2}
+
+        def is_arg_subtype(sub: Function.Argument, sup: Function.Argument) -> bool:
+            if not self.is_subtype(sub.type, sup.type):
+                return False
+            if not sup.required and sub.required:
+                return False
+            return True
+
+        for arg1 in pos1:
+            arg2: Function.Argument
+            if arg1.pos < len(pos2):
+                arg2 = pos2[arg1.pos]
+            elif arg1.pos in mixed_by_pos:
+                arg2 = mixed_by_pos[arg1.pos]
+            elif not arg1.required:
+                continue
+            else:
+                return False
+            if not is_arg_subtype(arg2, arg1):
+                return False
+
+        for name, arg1 in kw1.items():
+            arg2: Function.Argument
+            if name in kw2:
+                arg2 = kw2[name]
+            elif name in mixed_by_name:
+                arg2 = mixed_by_name[name]
+            elif not arg1.required:
+                continue
+            else:
+                return False
+            if not is_arg_subtype(arg2, arg1):
+                return False
+
+        for arg1 in mixed1:
+            pos_arg2: Optional[Function.Argument] = None
+            kw_arg2: Optional[Function.Argument] = None
+            if arg1.name in kw2:
+                kw_arg2 = kw2[arg1.name]
+            elif arg1.name in mixed_by_name:
+                kw_arg2 = mixed_by_name[arg1.name]
+            if arg1.pos < len(pos2):
+                pos_arg2 = pos2[arg1.pos]
+            elif arg1.pos in mixed_by_pos:
+                pos_arg2 = mixed_by_pos[arg1.pos]
+
+            # No match in func2 and arg is required
+            if pos_arg2 is None and kw_arg2 is None and arg1.required:
+                return False
+
+            # Matching keyword argument
+            if kw_arg2 is not None and not is_arg_subtype(kw_arg2, arg1):
+                return False
+
+            # Matching positional argument
+            if pos_arg2 is not None and not is_arg_subtype(pos_arg2, arg1):
+                return False
+
+        mixed_positions: set[int] = {a.pos for a in mixed1}
+        mixed_names: set[str] = {a.name for a in mixed1}
+        for arg2 in pos2:
+            if not arg2.required:
+                continue
+            if arg2.pos >= len(pos1) and arg2.pos not in mixed_positions:
+                return False
+
+        for name, arg2 in kw2.items():
+            if not arg2.required:
+                continue
+            if name not in kw1 and name not in mixed_names:
+                return False
+
+        for arg2 in mixed2:
+            if arg2.required:
+                continue
+            pos_match: bool = arg2.pos < len(pos1) or arg2.pos in mixed_positions
+            kw_match: bool = arg2.name in kw1 or arg2.name in mixed_names
+            if not pos_match or not kw_match:
+                return False
+
+        return True
 
     def visit_expression_stmt(self, stmt: p.ExpressionStmt) -> None:
-        self.evaluate(stmt.expr)
+        self.type_of(stmt.expr)
 
     def visit_function(self, stmt: p.Function) -> None:
         env: Environment = Environment(self.env)
@@ -196,34 +346,41 @@ class Checker(
                 return arg.default.accept(self)
             return UnknownType()
 
+        pos: int = 0
         for arg in stmt.posonlyargs:
             pos_args.append(
                 Function.Argument(
+                    pos=pos,
                     name=arg.name,
                     type=eval_arg_type(arg),
                     required=arg.default is None,
                 )
             )
+            pos += 1
         for arg in stmt.args:
             args.append(
                 Function.Argument(
+                    pos=pos,
                     name=arg.name,
                     type=eval_arg_type(arg),
                     required=arg.default is None,
                 )
             )
+            pos += 1
         for arg in stmt.kwonlyargs:
             kw_args.append(
                 Function.Argument(
+                    pos=pos,  # not relevant
                     name=arg.name,
                     type=eval_arg_type(arg),
                     required=arg.default is None,
                 )
             )
+            pos += 1
 
         for arg in pos_args + args + kw_args:
             env.define(arg.name, arg.type)
-        
+
         returns_hint: Optional[Type] = None
         if stmt.returns is not None:
             returns_hint = stmt.returns.accept(self)
@@ -237,7 +394,7 @@ class Checker(
             )
             self.env.define(stmt.name, inside_function)
 
-        returned: bool = self.evaluate_block(stmt.body, env)
+        returned: bool = self.process_block(stmt.body, env)
         inferred_return: Type = UnknownType()
         if not returned:
             env.return_types.append(UnitType())
@@ -278,24 +435,66 @@ class Checker(
         self.env.define(stmt.name, type)
 
     def visit_assign_stmt(self, stmt: p.AssignStmt) -> None:
-        value: Type = self.evaluate(stmt.value)
+        value_type: Type = self.type_of(stmt.value)
         for target in stmt.targets:
-            if not isinstance(target, p.VariableExpr):
-                self.logger.warning(f"Unsupported assignment to {target}")
-                self.warning(target.location, f"Unsupported assignment to {target}")
-                continue
-            name: str = target.name
-            var_type: Optional[Type] = self.look_up_variable(name, target)
+            self._assign(stmt.location, target, value_type)
 
-            if var_type is None:
-                self.env.define(name, value)
-            else:
-                # TODO: implement real comparison method
-                if var_type != value:
+    def _assign(self, location: Location, target: p.Expr, value_type: Type):
+        match target:
+            case p.VariableExpr():
+                self._assign_var(location, target, value_type)
+
+            case p.GetExpr():
+                self._assign_attr(location, target, value_type)
+
+            case _:
+                if not isinstance(target, p.VariableExpr):
+                    self.logger.warning(f"Unsupported assignment to {target}")
+                    self.warning(target.location, f"Unsupported assignment to {target}")
+
+    def _assign_var(self, location: Location, target: p.VariableExpr, value_type: Type):
+        name: str = target.name
+        var_type: Optional[Type] = self.look_up_variable(name, target)
+
+        if var_type is None:
+            self.env.define(name, value_type)
+        else:
+            # S <: T
+            # Γ, x: T   v: S
+            # x = v
+            if not self.is_subtype(value_type, var_type):
+                self.error(
+                    location,
+                    f"Cannot assign {value_type} to {name} of type {var_type}",
+                )
+
+    def _assign_attr(self, location: Location, target: p.GetExpr, value_type: Type):
+        object: Type = self.type_of(target.object)
+        base_object: Type = self.unfold_type(object)
+        match base_object:
+            case ComplexType(properties=properties):
+                if target.name not in properties:
                     self.error(
-                        stmt.location,
-                        f"Cannot assign {value} to {name} of type {var_type}",
+                        target.location, f"Unknown property '{target.name} on {object}"
                     )
+                    return
+
+                prop_type: Type = properties[target.name]
+                if not self.is_subtype(value_type, prop_type):
+                    self.error(
+                        location,
+                        f"Cannot assign {value_type} to property '{target.name}' of type {prop_type} on {object}",
+                    )
+                    return
+
+            case UnknownType():
+                pass
+
+            case _:
+                self.error(
+                    target.location,
+                    f"Cannot assign {value_type} to unknown property '{target.name}' on {object}",
+                )
 
     def visit_return_stmt(self, stmt: p.ReturnStmt) -> None:
         type: Type = stmt.value.accept(self) if stmt.value is not None else UnitType()
@@ -317,8 +516,8 @@ class Checker(
             )
 
         env: Environment = Environment(self.env)
-        body_returned: bool = self.evaluate_block(stmt.body, env)
-        else_returned: bool = self.evaluate_block(stmt.orelse, env)
+        body_returned: bool = self.process_block(stmt.body, env)
+        else_returned: bool = self.process_block(stmt.orelse, env)
         self.env.return_types.extend(env.return_types)
         if body_returned and else_returned:
             raise ReturnException()
@@ -329,17 +528,51 @@ class Checker(
             self.logger.warning(f"Unsupported operator {expr.operator}")
             self.warning(expr.location, f"Unsupported operator {expr.operator}")
             return UnknownType()
-        left: Type = self.evaluate(expr.left)
-        right: Type = self.evaluate(expr.right)
+        left: Type = self.type_of(expr.left)
+        right: Type = self.type_of(expr.right)
 
-        result: Optional[Type] = self.ctx.get_operation_result(left, method, right)
-        if result is None:
+        operations: list[Operation] = self.ctx.get_operations_by_name(method)
+        valid_operations: list[Operation] = []
+        for op in operations:
+            sig: Operation.CallSignature = op.signature
+            if self.is_subtype(left, sig.left) and self.is_subtype(right, sig.right):
+                valid_operations.append(op)
+
+        if len(valid_operations) == 0:
             self.error(
                 expr.location,
                 f"Undefined operation {method} between {left} and {right}",
             )
             return UnknownType()
-        return result
+        elif len(valid_operations) == 1:
+            self.logger.debug(f"Unique operation {method} between {left} and {right}")
+            return valid_operations[0].result
+
+        for i, op1 in enumerate(valid_operations):
+            sig1: Operation.CallSignature = op1.signature
+            best_match: bool = True
+            for j, op2 in enumerate(valid_operations):
+                if i == j:
+                    continue
+                sig2: Operation.CallSignature = op2.signature
+                if not self.is_subtype(sig1.left, sig2.left) or not self.is_subtype(
+                    sig1.right, sig2.right
+                ):
+                    best_match = False
+                    break
+                self.logger.debug(f"{op1} is a full overload of {op2}")
+            if best_match:
+                return op1.result
+
+        overloads: list[str] = [
+            f"({op.signature.left} {op.signature.method} {op.signature.right}) -> {op.result}"
+            for op in valid_operations
+        ]
+        self.error(
+            expr.location,
+            f"Ambiguous operation {method} between {left} and {right}, multiple matching overloads: {', '.join(overloads)}",
+        )
+        return UnknownType()
 
     def visit_compare_expr(self, expr: p.CompareExpr) -> Type:
         method: Optional[str] = COMPARATOR_METHODS.get(expr.operator.__class__)
@@ -347,8 +580,8 @@ class Checker(
             self.logger.warning(f"Unsupported operator {expr.operator}")
             self.warning(expr.location, f"Unsupported operator {expr.operator}")
             return UnknownType()
-        left: Type = self.evaluate(expr.left)
-        right: Type = self.evaluate(expr.right)
+        left: Type = self.type_of(expr.left)
+        right: Type = self.type_of(expr.right)
 
         result: Optional[Type] = self.ctx.get_operation_result(left, method, right)
         if result is None:
@@ -362,24 +595,40 @@ class Checker(
     def visit_unary_expr(self, expr: p.UnaryExpr) -> Type: ...
 
     def visit_call_expr(self, expr: p.CallExpr) -> Type:
-        if path := self.parse_midas_import(expr):
-            self.import_midas(path)
-            return UnknownType()
-        callee: Type = self.evaluate(expr.callee)
+        callee: Type = self.type_of(expr.callee)
         if not isinstance(callee, Function):
             self.error(expr.callee.location, "Callee is not a function")
             return UnknownType()
         function: Function = callee
         mapped: list[MappedArgument] = self.map_call_arguments(function, expr)
         for arg in mapped:
-            if arg.type != arg.argument.type:
+            if not self.is_subtype(arg.type, arg.argument.type):
                 self.error(
                     arg.expr.location,
                     f"Wrong type for argument '{arg.argument.name}', expected {arg.argument.type}, got {arg.type}",
                 )
         return function.returns
 
-    def visit_get_expr(self, expr: p.GetExpr) -> Type: ...
+    def visit_get_expr(self, expr: p.GetExpr) -> Type:
+        object: Type = self.type_of(expr.object)
+        base_object: Type = self.unfold_type(object)
+        match base_object:
+            case ComplexType(properties=properties):
+                if expr.name not in properties:
+                    self.error(
+                        expr.location, f"Unknown property '{expr.name} on {object}"
+                    )
+                    return UnknownType()
+                return properties[expr.name]
+
+            case UnknownType():
+                return UnknownType()
+
+            case _:
+                self.error(
+                    expr.location, f"Cannot get property '{expr.name}' on {object}"
+                )
+                return UnknownType()
 
     def visit_literal_expr(self, expr: p.LiteralExpr) -> Type:
         match expr.value:
@@ -398,9 +647,20 @@ class Checker(
     def visit_variable_expr(self, expr: p.VariableExpr) -> Type:
         return self.look_up_variable(expr.name, expr) or UnknownType()
 
-    def visit_logical_expr(self, expr: p.LogicalExpr) -> Type: ...
+    def visit_logical_expr(self, expr: p.LogicalExpr) -> Type:
+        left: Type = expr.left.accept(self)
+        right: Type = expr.right.accept(self)
 
-    def visit_set_expr(self, expr: p.SetExpr) -> Type: ...
+        if self.is_subtype(left, right):
+            return right
+        if self.is_subtype(right, left):
+            return left
+
+        self.error(
+            expr.location,
+            f"Incompatible operand types, {left=} and {right=}",
+        )
+        return UnknownType()
 
     def visit_cast_expr(self, expr: p.CastExpr) -> Type:
         return expr.type.accept(self)
@@ -416,10 +676,16 @@ class Checker(
 
         true_type: Type = expr.if_true.accept(self)
         false_type: Type = expr.if_false.accept(self)
-        if true_type != false_type:
-            self.error(expr.location, f"Type mismatch in ternary if branches: true={true_type} != false={false_type}")
-            return UnknownType()
-        return true_type
+        if self.is_subtype(true_type, false_type):
+            return false_type
+        if self.is_subtype(false_type, true_type):
+            return true_type
+
+        self.error(
+            expr.location,
+            f"Incompatible types in ternary if branches: true={true_type} and false={false_type}",
+        )
+        return UnknownType()
 
     def visit_base_type(self, node: p.BaseType) -> Type:
         return self.ctx.get_type(node.base)
@@ -448,10 +714,10 @@ class Checker(
             list[MappedArgument]: the list of mapped arguments
         """
         positional: list[tuple[p.Expr, Type]] = [
-            (arg, self.evaluate(arg)) for arg in call.arguments
+            (arg, self.type_of(arg)) for arg in call.arguments
         ]
         keywords: dict[str, tuple[p.Expr, Type]] = {
-            name: (arg, self.evaluate(arg)) for name, arg in call.keywords.items()
+            name: (arg, self.type_of(arg)) for name, arg in call.keywords.items()
         }
         set_args: set[str] = set()
 

midas/checker/diagnostic.py

@@ -19,7 +19,8 @@ class Diagnostic:
     type: DiagnosticType
     message: str
 
-    def __str__(self) -> str:
+    @property
+    def location_str(self) -> str:
         start_loc: str = f"L{self.location.lineno}:{self.location.col_offset+1}"
         end_loc: Optional[str] = ""
         if (
@@ -30,4 +31,7 @@ class Diagnostic:
         loc: str = (
             f"at {start_loc}" if end_loc is None else f"from {start_loc} to {end_loc}"
         )
-        return f"{self.type} in {self.file_path} {loc}: {self.message}"
+        return f"{self.type} in {self.file_path} {loc}"
+
+    def __str__(self) -> str:
+        return f"{self.location_str}: {self.message}"

midas/checker/types.py

@@ -9,9 +9,9 @@ class BaseType:
 
 
 @dataclass(frozen=True, kw_only=True)
-class SimpleType:
+class AliasType:
     name: str
-    base: BaseType | SimpleType
+    type: Type
 
 
 @dataclass(frozen=True, kw_only=True)
@@ -34,9 +34,27 @@ class Function:
 
     @dataclass(frozen=True, kw_only=True)
     class Argument:
+        pos: int
         name: str
         type: Type
         required: bool
 
 
-Type = BaseType | SimpleType | UnknownType | UnitType | Function
+@dataclass(frozen=True, kw_only=True)
+class ComplexType:
+    properties: dict[str, Type]
+
+
+@dataclass(frozen=True, kw_only=True)
+class Operation:
+    signature: CallSignature
+    result: Type
+
+    @dataclass(frozen=True, kw_only=True)
+    class CallSignature:
+        left: Type
+        method: str
+        right: Type
+
+
+Type = BaseType | AliasType | UnknownType | UnitType | Function | ComplexType

midas/cli/ansi.py

@@ -0,0 +1,41 @@
+class Ansi:
+    CTRL = "\x1b["
+    RESET = CTRL + "0m"
+    BOLD = CTRL + "1m"
+    DIM = CTRL + "2m"
+    ITALIC = CTRL + "3m"
+    UNDERLINE = CTRL + "4m"
+
+    BLACK = 0
+    RED = 1
+    GREEN = 2
+    YELLOW = 3
+    BLUE = 4
+    MAGENTA = 5
+    CYAN = 6
+    WHITE = 7
+
+    BRIGHT_BLACK = 60
+    BRIGHT_RED = 61
+    BRIGHT_GREEN = 62
+    BRIGHT_YELLOW = 63
+    BRIGHT_BLUE = 64
+    BRIGHT_MAGENTA = 65
+    BRIGHT_CYAN = 66
+    BRIGHT_WHITE = 67
+
+    @classmethod
+    def FG(cls, col: int) -> str:
+        return f"{cls.CTRL}{30 + col}m"
+
+    @classmethod
+    def BG(cls, col: int) -> str:
+        return f"{cls.CTRL}{40 + col}m"
+
+    @classmethod
+    def FG_RGB(cls, r: int, g: int, b: int) -> str:
+        return f"{cls.CTRL}38;2;{r};{g};{b}m"
+
+    @classmethod
+    def BG_RGB(cls, r: int, g: int, b: int) -> str:
+        return f"{cls.CTRL}48;2;{r};{g};{b}m"

midas/cli/highlight.css

@@ -53,5 +53,6 @@ span {
 
     &.keyword {
         color: rgb(211, 72, 9);
+        pointer-events: none;
     }
 }

midas/cli/highlighter.py

@@ -1,6 +1,7 @@
 from __future__ import annotations
 
 from abc import ABC, abstractmethod
+from dataclasses import dataclass
 from pathlib import Path
 from typing import Generic, Optional, Protocol, TextIO, TypeVar
 
@@ -8,6 +9,7 @@ import midas.ast.midas as m
 import midas.ast.python as p
 from midas.ast.location import Location
 from midas.checker.diagnostic import Diagnostic
+from midas.lexer.token import Token
 
 H = TypeVar("H", bound="Highlighter", contravariant=True)
 
@@ -22,6 +24,15 @@ class Locatable(Protocol):
     def location(self) -> Optional[Location]: ...
 
 
+@dataclass(frozen=True)
+class LocatableToken:
+    token: Token
+
+    @property
+    def location(self) -> Location:
+        return self.token.get_location()
+
+
 class Highlighter(ABC):
     BASE_CSS_PATH: Path = Path(__file__).parent / "highlight.css"
     EXTRA_CSS_PATH: Optional[Path] = None
@@ -199,41 +210,27 @@ class PythonHighlighter(
 
     def visit_logical_expr(self, expr: p.LogicalExpr) -> None: ...
 
-    def visit_set_expr(self, expr: p.SetExpr) -> None: ...
-
     def visit_cast_expr(self, expr: p.CastExpr) -> None: ...
 
     def visit_ternary_expr(self, expr: p.TernaryExpr) -> None: ...
 
 
-class MidasHighlighter(Highlighter, m.Stmt.Visitor[None], m.Expr.Visitor[None]):
+class MidasHighlighter(
+    Highlighter, m.Stmt.Visitor[None], m.Expr.Visitor[None], m.Type.Visitor[None]
+):
     EXTRA_CSS_PATH: Optional[Path] = Path(__file__).parent / "hl_midas.css"
 
     def highlight(self, node: Highlightable[MidasHighlighter]):
         node.accept(self)
 
-    def visit_simple_type_stmt(self, stmt: m.SimpleTypeStmt) -> None:
-        self.wrap(stmt, "simple-type")
-        if stmt.template is not None:
-            stmt.template.accept(self)
-        stmt.base.accept(self)
-        if stmt.constraint is not None:
-            self.wrap(stmt.constraint, "constraint")
-            stmt.constraint.accept(self)
-
-    def visit_complex_type_stmt(self, stmt: m.ComplexTypeStmt) -> None:
-        self.wrap(stmt, "complex-type")
-        if stmt.template is not None:
-            stmt.template.accept(self)
-        for prop in stmt.properties:
-            prop.accept(self)
+    def visit_type_stmt(self, stmt: m.TypeStmt) -> None:
+        self.wrap(stmt, "type-stmt")
+        self.wrap(LocatableToken(stmt.name), "type-name")
+        stmt.type.accept(self)
 
     def visit_property_stmt(self, stmt: m.PropertyStmt) -> None:
         self.wrap(stmt, "property")
         stmt.type.accept(self)
-        if stmt.constraint is not None:
-            self.wrap(stmt.constraint, "constraint")
-            stmt.constraint.accept(self)
 
     def visit_extend_stmt(self, stmt: m.ExtendStmt) -> None:
         self.wrap(stmt, "extend")
@@ -243,17 +240,16 @@ class MidasHighlighter(Highlighter, m.Stmt.Visitor[None], m.Expr.Visitor[None]):
 
     def visit_op_stmt(self, stmt: m.OpStmt) -> None:
         self.wrap(stmt, "op")
+        self.wrap(LocatableToken(stmt.name), "op-name")
         stmt.operand.accept(self)
         stmt.result.accept(self)
 
     def visit_predicate_stmt(self, stmt: m.PredicateStmt) -> None:
         self.wrap(stmt, "predicate")
+        self.wrap(LocatableToken(stmt.name), "predicate-name")
         stmt.type.accept(self)
         stmt.condition.accept(self)
 
-    def visit_simple_type_expr(self, expr: m.SimpleTypeExpr) -> None:
-        self.wrap(expr, "simple-type-expr")
-
     def visit_logical_expr(self, expr: m.LogicalExpr) -> None:
         self.wrap(expr, "logical-expr")
         expr.left.accept(self)
@@ -282,14 +278,24 @@ class MidasHighlighter(Highlighter, m.Stmt.Visitor[None], m.Expr.Visitor[None]):
 
     def visit_wildcard_expr(self, expr: m.WildcardExpr) -> None: ...
 
-    def visit_template_expr(self, expr: m.TemplateExpr) -> None:
-        self.wrap(expr, "template")
-        expr.type.accept(self)
+    def visit_named_type(self, type: m.NamedType) -> None:
+        self.wrap(type, "named-type")
 
-    def visit_type_expr(self, expr: m.TypeExpr) -> None:
-        self.wrap(expr, "type")
-        if expr.template is not None:
-            expr.template.accept(self)
+    def visit_generic_type(self, type: m.GenericType) -> None:
+        self.wrap(type, "generic-type")
+        type.type.accept(self)
+        for param in type.params:
+            param.accept(self)
+
+    def visit_constraint_type(self, type: m.ConstraintType) -> None:
+        self.wrap(type, "constraint-type")
+        type.type.accept(self)
+        type.constraint.accept(self)
+
+    def visit_complex_type(self, type: m.ComplexType) -> None:
+        self.wrap(type, "complex-type")
+        for prop in type.properties:
+            prop.accept(self)
 
 
 class DiagnosticsHighlighter(Highlighter):

midas/cli/hl_midas.css

@@ -5,12 +5,11 @@ span {
         font-style: italic;
     }
 
-    &.simple-type {
-        --col: 108, 233, 108;
-    }
-
+    &.named-type,
+    &.generic-type,
+    &.constraint-type,
     &.complex-type {
-        --col: 233, 206, 108;
+        --col: 150, 150, 150;
     }
 
     &.constraint {
@@ -33,10 +32,6 @@ span {
         --col: 193, 108, 233;
     }
 
-    &.simple-type-expr {
-        --col: 150, 150, 150;
-    }
-
     &.logical-expr,
     &.binary-expr,
     &.unary-expr,
@@ -48,7 +43,9 @@ span {
         --col: 163, 117, 71;
     }
 
-    &.type {
+    &.type-name,
+    &.op-name,
+    &.predicate-name {
         --col: 200, 200, 200;
         font-weight: bold;
     }

midas/cli/main.py

@@ -1,7 +1,6 @@
 import ast
 import json
 import logging
-from dataclasses import dataclass
 from pathlib import Path
 from typing import Optional, TextIO, get_args
 
@@ -10,13 +9,15 @@ import click
 import midas.ast.midas as m
 import midas.ast.python as p
 from midas.ast.location import Location
-from midas.ast.printer import MidasAstPrinter, PythonAstPrinter
+from midas.ast.printer import MidasAstPrinter, MidasPrinter, PythonAstPrinter
 from midas.checker.checker import Checker
-from midas.checker.diagnostic import Diagnostic
+from midas.checker.diagnostic import Diagnostic, DiagnosticType
 from midas.checker.types import Type
+from midas.cli.ansi import Ansi
 from midas.cli.highlighter import (
     DiagnosticsHighlighter,
     Highlighter,
+    LocatableToken,
     MidasHighlighter,
     PythonHighlighter,
 )
@@ -30,35 +31,100 @@ from midas.utils import UniversalJSONDumper
 
 @click.group()
 def midas():
-    click.echo("Welcome to Midas!")
+    pass
+
+
+def print_diagnostic(lines: list[str], diagnostic: Diagnostic, indent: int = 4):
+    """Pretty-print a diagnostic, showing some context if possible
+
+    If the diagnostic concerns a specific part of one line, the line is shown
+    with the affected part highlighted. The message is clearly printed under the
+    line with an underline further indicating the target expression.
+
+    If multiple lines are concerned, no context is shown, only the
+    diagnostic type, location and message
+
+    Args:
+        lines (list[str]): source code lines
+        diagnostic (Diagnostic): the diagnostic to print
+        indent (int, optional): the number of spaces added before the target line to indent if from the location header. Defaults to 4.
+    """
+
+    loc: Location = diagnostic.location
+    if loc.lineno != loc.end_lineno:
+        print(diagnostic)
+        return
+
+    start_offset: int = loc.col_offset
+    end_offset: int = loc.end_col_offset or (start_offset + 1)
+
+    line: str = lines[loc.lineno - 1]
+    before: str = line[:start_offset]
+    after: str = line[end_offset:]
+
+    color: int = {
+        DiagnosticType.ERROR: Ansi.RED,
+        DiagnosticType.WARNING: Ansi.YELLOW,
+        DiagnosticType.INFO: Ansi.CYAN,
+    }.get(diagnostic.type, Ansi.WHITE)
+
+    subject: str = Ansi.FG(color) + line[start_offset:end_offset] + Ansi.RESET
+    cursor: str = (
+        " " * start_offset
+        + Ansi.FG(color)
+        + "~" * (end_offset - start_offset)
+        + "> "
+        + diagnostic.message
+        + Ansi.RESET
+    )
+
+    indent_str: str = " " * indent
+    print(diagnostic.location_str + ":")
+    print(indent_str + before + subject + after)
+    print(indent_str + cursor)
+    print()
 
 
 @midas.command()
 @click.option("-l", "--highlight", type=click.File("w"))
+@click.option("-t", "--types", type=click.File("r"), multiple=True)
+@click.option("-v", "--verbose", is_flag=True)
 @click.argument("file", type=click.File("r"))
-def compile(highlight: Optional[TextIO], file: TextIO):
-    logging.basicConfig(level=logging.DEBUG)
+def compile(
+    highlight: Optional[TextIO],
+    types: tuple[TextIO],
+    verbose: bool,
+    file: TextIO,
+):
+    logging.basicConfig(level=logging.DEBUG if verbose else logging.WARN)
     source: str = file.read()
     tree: ast.Module = ast.parse(source, filename=file.name)
     parser = PythonParser()
     stmts: list[p.Stmt] = parser.parse_module(tree)
     resolver = Resolver()
     resolver.resolve(*stmts)
-    checker = Checker(resolver.locals, file_path=Path(file.name).resolve())
-    diagnostics: list[Diagnostic] = checker.check(stmts)
-    for diagnostic in diagnostics:
-        print(diagnostic)
-
-    print(
-        json.dumps(
-            UniversalJSONDumper.dump(
-                checker.global_env,
-                [("Environment", "_children")],
-                lambda obj: isinstance(obj, get_args(Type)),
-            ),
-            indent=4,
-        )
+    types_paths: list[Path] = [Path(t.name).resolve() for t in types]
+    checker = Checker(
+        resolver.locals,
+        source_path=Path(file.name).resolve(),
+        types_paths=types_paths,
     )
+    diagnostics: list[Diagnostic] = checker.check(stmts)
+    lines: list[str] = source.split("\n")
+    for diagnostic in diagnostics:
+        print_diagnostic(lines, diagnostic)
+
+    if verbose:
+        print(
+            json.dumps(
+                UniversalJSONDumper.dump(
+                    checker.global_env,
+                    [("Environment", "_children")],
+                    lambda obj: isinstance(obj, get_args(Type)),
+                ),
+                indent=4,
+            )
+        )
     if highlight is not None:
         highlighter = DiagnosticsHighlighter(source)
         highlighter.highlight(diagnostics)
@@ -142,14 +208,6 @@ def highlight_midas(source: str, path: str) -> Highlighter:
     for err in parser.errors:
         print(err.get_report())
 
-    @dataclass(frozen=True)
-    class LocatableToken:
-        token: Token
-
-        @property
-        def location(self) -> Location:
-            return self.token.get_location()
-
     for stmt in stmts:
         highlighter.highlight(stmt)
     for token in tokens:
@@ -176,5 +234,21 @@ def highlight(output: TextIO, file: TextIO):
     highlighter.dump(output)
 
 
+@midas.command()
+@click.option("-o", "--output", type=click.File("w"), default="-")
+@click.argument("file", type=click.File("r"))
+def format(output: TextIO, file: TextIO):
+    source: str = file.read()
+    printer = MidasPrinter()
+    lexer = MidasLexer(source, file=file.name)
+    tokens: list[Token] = lexer.process()
+    parser = MidasParser(tokens)
+    stmts: list[m.Stmt] = parser.parse()
+    for err in parser.errors:
+        print(err.get_report())
+    for stmt in stmts:
+        output.write(printer.print(stmt) + "\n")
+
+
 if __name__ == "__main__":
     midas()

midas/lexer/midas.py

@@ -40,8 +40,8 @@ class MidasLexer(Lexer):
                 self.add_token(TokenType.AND)
             case "?":
                 self.add_token(TokenType.QMARK)
-            # case ",":
-            #     self.add_token(TokenType.COMMA)
+            case ",":
+                self.add_token(TokenType.COMMA)
             case "_" if not self.is_identifier_char(self.peek_next(), start=False):
                 self.add_token(TokenType.UNDERSCORE)
             case "-" if self.match(">"):

midas/lexer/token.py

@@ -17,7 +17,7 @@ class TokenType(Enum):
     LEFT_BRACE = auto()
     RIGHT_BRACE = auto()
     COLON = auto()
-    # COMMA = auto()
+    COMMA = auto()
     UNDERSCORE = auto()
     ARROW = auto()
     AND = auto()

midas/parser/midas.py

@@ -3,21 +3,22 @@ from typing import Optional
 from midas.ast.location import Location
 from midas.ast.midas import (
     BinaryExpr,
-    ComplexTypeStmt,
+    ComplexType,
+    ConstraintType,
     Expr,
     ExtendStmt,
+    GenericType,
     GetExpr,
     GroupingExpr,
     LiteralExpr,
     LogicalExpr,
+    NamedType,
     OpStmt,
     PredicateStmt,
     PropertyStmt,
-    SimpleTypeExpr,
-    SimpleTypeStmt,
     Stmt,
-    TemplateExpr,
-    TypeExpr,
+    Type,
+    TypeStmt,
     UnaryExpr,
     VariableExpr,
     WildcardExpr,
@@ -81,7 +82,7 @@ class MidasParser(Parser):
             self.synchronize()
             return None
 
-    def type_declaration(self) -> SimpleTypeStmt | ComplexTypeStmt:
+    def type_declaration(self) -> TypeStmt:
         """Parse a type declaration
 
         A type declaration can either be a simple type alias or a new complex type.
@@ -107,33 +108,22 @@ class MidasParser(Parser):
         """
         keyword: Token = self.previous()
         name: Token = self.consume(TokenType.IDENTIFIER, "Expected type name")
-        template: Optional[TemplateExpr] = None
+        params: list[TypeStmt.Param] = []
         if self.check(TokenType.LEFT_BRACKET):
-            template = self.template_expr()
+            params = self.type_stmt_params()
 
-        if self.match(TokenType.LEFT_PAREN):
-            base: TypeExpr = self.type_expr()
-            self.consume(TokenType.RIGHT_PAREN, "Unclosed base type parenthesis")
-            constraint: Optional[Expr] = None
-            if self.match(TokenType.WHERE):
-                constraint = self.constraint()
-            return SimpleTypeStmt(
-                location=keyword.location_to(self.previous()),
-                name=name,
-                template=template,
-                base=base,
-                constraint=constraint,
-            )
-        else:
-            properties: list[PropertyStmt] = self.type_properties()
-            return ComplexTypeStmt(
-                location=keyword.location_to(self.previous()),
-                name=name,
-                template=template,
-                properties=properties,
-            )
+        self.consume(TokenType.EQUAL, "Expected '=' before type definition")
 
-    def template_expr(self) -> TemplateExpr:
+        type: Type = self.type_expr()
+
+        return TypeStmt(
+            location=keyword.location_to(self.previous()),
+            name=name,
+            params=params,
+            type=type,
+        )
+
+    def type_stmt_params(self) -> list[TypeStmt.Param]:
         """Parse a generic template expression
 
         A template is written `[TypeExpr]`
@@ -141,16 +131,27 @@ class MidasParser(Parser):
         Returns:
             TemplateExpr: the parsed template expression
         """
-        left: Token = self.consume(
-            TokenType.LEFT_BRACKET, "Missing '[' before template expression"
-        )
-        type: TypeExpr = self.type_expr()
-        right: Token = self.consume(
-            TokenType.RIGHT_BRACKET, "Missing ']' after template expression"
-        )
-        return TemplateExpr(location=left.location_to(right), type=type)
+        self.consume(TokenType.LEFT_BRACKET, "Missing '[' before template expression")
+        params: list[TypeStmt.Param] = []
+        while not self.is_at_end() and not self.check(TokenType.RIGHT_BRACKET):
+            name: Token = self.consume(TokenType.IDENTIFIER, "Expected type variable")
+            bound: Optional[Type] = None
+            if self.match(TokenType.LESS):
+                self.consume(TokenType.COLON, "Expected ':' after '<'")
+                bound = self.type_expr()
+            params.append(
+                TypeStmt.Param(
+                    location=name.location_to(self.previous()),
+                    name=name,
+                    bound=bound,
+                )
+            )
+            if not self.match(TokenType.COMMA):
+                break
+        self.consume(TokenType.RIGHT_BRACKET, "Missing ']' after template expression")
+        return params
 
-    def type_expr(self) -> TypeExpr:
+    def type_expr(self) -> Type:
         """Parse a type expression
 
         A type is an identifier, optionally followed by a template expression.
@@ -159,30 +160,82 @@ class MidasParser(Parser):
         Returns:
             TypeExpr: the parsed type expression
         """
-        name: Token = self.consume(TokenType.IDENTIFIER, "Expected type name")
-        template: Optional[TemplateExpr] = None
+        return self.constraint_type()
+
+    def constraint_type(self) -> Type:
+        type: Type = self.base_type()
+        if self.match(TokenType.WHERE):
+            constraint: Expr = self.constraint()
+            return ConstraintType(
+                location=Location.span(type.location, constraint.location),
+                type=type,
+                constraint=constraint,
+            )
+        return type
+
+    def base_type(self) -> Type:
+        if self.match(TokenType.LEFT_PAREN):
+            type: Type = self.type_expr()
+            self.consume(TokenType.RIGHT_PAREN, "Unclosed parenthesis")
+            return type
+
+        if self.check(TokenType.LEFT_BRACE):
+            return self.complex_type()
+
+        return self.generic_type()
+
+    def generic_type(self) -> Type:
+        type: Type = self.named_type()
         if self.check(TokenType.LEFT_BRACKET):
-            template = self.template_expr()
-        optional: bool = self.match(TokenType.QMARK)
-        return TypeExpr(
-            location=name.location_to(self.previous()),
+            params: list[Type] = self.type_params()
+            return GenericType(
+                location=Location.span(type.location, self.previous().get_location()),
+                type=type,
+                params=params,
+            )
+        return type
+
+    def type_params(self) -> list[Type]:
+        params: list[Type] = []
+        self.consume(TokenType.LEFT_BRACKET, "Missing '[' before generic parameters")
+        while not self.is_at_end() and not self.check(TokenType.RIGHT_BRACKET):
+            params.append(self.type_expr())
+            if not self.match(TokenType.COMMA):
+                break
+        self.consume(TokenType.RIGHT_BRACKET, "Missing ']' after generic parameters")
+        return params
+
+    def named_type(self) -> Type:
+        name: Token = self.consume(TokenType.IDENTIFIER, "Expected type name")
+        return NamedType(
+            location=name.get_location(),
             name=name,
-            template=template,
-            optional=optional,
         )
 
-    def simple_type_expr(self) -> SimpleTypeExpr:
-        """Parse a simple type expression
+    def complex_type(self) -> Type:
+        """Parse a type definition body
 
-        A simple type is just an identifier optionally followed by a '?'
+        A type definition body is a set of whitespace-separated
+        property statements enclosed in curly braces
 
         Returns:
-            SimpleTypeExpr: the parsed simple type expression
+            list[PropertyStmt]: the parsed type properties
         """
-        name: Token = self.consume(TokenType.IDENTIFIER, "Expected type name")
-        optional: bool = self.match(TokenType.QMARK)
-        return SimpleTypeExpr(
-            location=name.location_to(self.previous()), name=name, optional=optional
+        left: Token = self.consume(
+            TokenType.LEFT_BRACE, "Expected '{' to start type body"
+        )
+        properties: list[PropertyStmt] = []
+        names: set[str] = set()
+        while not self.check(TokenType.RIGHT_BRACE) and not self.is_at_end():
+            prop: PropertyStmt = self.property_stmt()
+            if prop.name.lexeme in names:
+                raise self.error(prop.name, "Duplicate property")
+            names.add(prop.name.lexeme)
+            properties.append(prop)
+        right: Token = self.consume(TokenType.RIGHT_BRACE, "Unclosed type body")
+        return ComplexType(
+            location=left.location_to(right),
+            properties=properties,
         )
 
     def constraint(self) -> Expr:
@@ -308,27 +361,6 @@ class MidasParser(Parser):
 
         raise self.error(self.peek(), "Expected expression")
 
-    def type_properties(self) -> list[PropertyStmt]:
-        """Parse a type definition body
-
-        A type definition body is a set of whitespace-separated
-        property statements enclosed in curly braces
-
-        Returns:
-            list[PropertyStmt]: the parsed type properties
-        """
-        self.consume(TokenType.LEFT_BRACE, "Expected '{' to start type body")
-        properties: list[PropertyStmt] = []
-        names: set[str] = set()
-        while not self.check(TokenType.RIGHT_BRACE) and not self.is_at_end():
-            prop: PropertyStmt = self.property_stmt()
-            if prop.name.lexeme in names:
-                raise self.error(prop.name, "Duplicate property")
-            names.add(prop.name.lexeme)
-            properties.append(prop)
-        self.consume(TokenType.RIGHT_BRACE, "Unclosed type body")
-        return properties
-
     def property_stmt(self) -> PropertyStmt:
         """Parse a property statement
 
@@ -339,15 +371,11 @@ class MidasParser(Parser):
         """
         name: Token = self.consume(TokenType.IDENTIFIER, "Expected property name")
         self.consume(TokenType.COLON, "Expected ':' after property name")
-        type: TypeExpr = self.type_expr()
-        constraint: Optional[Expr] = None
-        if self.match(TokenType.WHERE):
-            constraint = self.constraint()
+        type: Type = self.type_expr()
         return PropertyStmt(
             location=name.location_to(self.previous()),
             name=name,
             type=type,
-            constraint=constraint,
         )
 
     def extend_declaration(self) -> ExtendStmt:
@@ -359,7 +387,7 @@ class MidasParser(Parser):
             ExtendStmt: the parsed extension statement
         """
         keyword: Token = self.previous()
-        type: TypeExpr = self.type_expr()
+        type: Type = self.type_expr()
         self.consume(TokenType.LEFT_BRACE, "Expected '{' to start extend body")
         operations: list[OpStmt] = []
         while not self.is_at_end() and not self.check(TokenType.RIGHT_BRACE):
@@ -380,11 +408,11 @@ class MidasParser(Parser):
 
         name: Token = self.consume(TokenType.IDENTIFIER, "Expected operation name")
         self.consume(TokenType.LEFT_PAREN, "Expected '(' before operand type")
-        operand: TypeExpr = self.type_expr()
+        operand: Type = self.type_expr()
         self.consume(TokenType.RIGHT_PAREN, "Expected ')' after operand type")
 
         self.consume(TokenType.ARROW, "Expected '->' before result type")
-        result: TypeExpr = self.type_expr()
+        result: Type = self.type_expr()
 
         return OpStmt(
             location=keyword.location_to(self.previous()),
@@ -406,7 +434,7 @@ class MidasParser(Parser):
         self.consume(TokenType.LEFT_PAREN, "Expected '(' before predicate subject")
         subject: Token = self.consume(TokenType.IDENTIFIER, "Expected subject name")
         self.consume(TokenType.COLON, "Expected ':' after subject name")
-        type: TypeExpr = self.type_expr()
+        type: Type = self.type_expr()
         self.consume(TokenType.RIGHT_PAREN, "Expected ')' after predicate subject")
         self.consume(TokenType.EQUAL, "Expected '=' after predicate subject")
         condition: Expr = self.constraint()

midas/parser/python.py

@@ -87,6 +87,9 @@ class PythonParser:
             case ast.If():
                 return self.parse_if(node)
 
+            case ast.Pass():
+                return None
+
             case _:
                 print(f"Unsupported statement: {ast.unparse(node)}")
                 return None
@@ -311,6 +314,13 @@ class PythonParser:
                             constraint=right_expr,
                         )
 
+            case ast.Constant(value=None):
+                return BaseType(
+                    location=loc,
+                    base="None",
+                    param=None,
+                )
+
             case _:
                 raise UnsupportedSyntaxError(type_expr)
 

midas/resolver/builtin.py

@@ -16,6 +16,7 @@ def op(ctx: MidasResolver, t1: Type, operator: str, t2: Type, t3: Type):
         result=t3,
     )
 
+
 def basic_op(ctx: MidasResolver, type: Type, op: str):
     ctx.define_operation(
         left=type,
@@ -68,4 +69,4 @@ def define_builtins(ctx: MidasResolver):
     op(ctx, float, "__gt__", int, bool)  # float > int = bool
     op(ctx, float, "__le__", int, bool)  # float <= int = bool
     op(ctx, float, "__ge__", int, bool)  # float >= int = bool
-    op(ctx, float, "__eq__", int, bool)  # float == int = bool
+    op(ctx, float, "__eq__", int, bool)  # float == int = bool

midas/resolver/midas.py

@@ -1,16 +1,22 @@
 from typing import Optional
 
 import midas.ast.midas as m
-from midas.checker.types import BaseType, SimpleType, Type
+from midas.checker.types import (
+    AliasType,
+    ComplexType,
+    Operation,
+    Type,
+    UnknownType,
+)
 from midas.resolver.builtin import define_builtins
 
 
-class MidasResolver(m.Stmt.Visitor[None], m.Expr.Visitor[Type]):
+class MidasResolver(m.Stmt.Visitor[None], m.Expr.Visitor[None], m.Type.Visitor[Type]):
     """A resolver which evaluates Midas type definitions and build a registry"""
 
     def __init__(self) -> None:
         self._types: dict[str, Type] = {}
-        self._operations: dict[tuple[Type, str, Type], Type] = {}
+        self._operations: dict[Operation.CallSignature, Type] = {}
 
         define_builtins(self)
 
@@ -44,10 +50,26 @@ class MidasResolver(m.Stmt.Visitor[None], m.Expr.Visitor[Type]):
         Returns:
             Optional[Type]: the result type, or None if no matching operation was found
         """
-        operation: tuple[Type, str, Type] = (left, operator, right)
-        result: Optional[Type] = self._operations.get(operation)
+        signature: Operation.CallSignature = Operation.CallSignature(
+            left=left,
+            method=operator,
+            right=right,
+        )
+        result: Optional[Type] = self._operations.get(signature)
         return result
 
+    def get_operations_by_name(self, name: str) -> list[Operation]:
+        operations: list[Operation] = []
+        for signature, result in self._operations.items():
+            if signature.method == name:
+                operations.append(
+                    Operation(
+                        signature=signature,
+                        result=result,
+                    )
+                )
+        return operations
+
     def define_type(self, name: str, type: Type) -> Type:
         """Define a type in the registry
 
@@ -78,12 +100,16 @@ class MidasResolver(m.Stmt.Visitor[None], m.Expr.Visitor[Type]):
         Raises:
             ValueError: if an operation is already defined with these operands and name
         """
-        operation: tuple[Type, str, Type] = (left, operator, right)
-        if operation in self._operations:
+        signature: Operation.CallSignature = Operation.CallSignature(
+            left=left,
+            method=operator,
+            right=right,
+        )
+        if signature in self._operations:
             raise ValueError(
                 f"Operation {operator} already defined between {left} and {right}"
             )
-        self._operations[operation] = result
+        self._operations[signature] = result
 
     def resolve(self, stmts: list[m.Stmt]):
         """Process a sequence of statements
@@ -94,20 +120,13 @@ class MidasResolver(m.Stmt.Visitor[None], m.Expr.Visitor[Type]):
         for stmt in stmts:
             stmt.accept(self)
 
-    def visit_simple_type_stmt(self, stmt: m.SimpleTypeStmt) -> None:
-        # TODO generics, optional, constraint
-        base: Type = self.get_type(stmt.base.name.lexeme)
-        match base:
-            case BaseType() | SimpleType():
-                type = SimpleType(
-                    name=stmt.name.lexeme,
-                    base=base,
-                )
-                self.define_type(type.name, type)
-            case _:
-                raise TypeError(f"Invalid base {base} for simple type")
-
-    def visit_complex_type_stmt(self, stmt: m.ComplexTypeStmt) -> None: ...
+    def visit_type_stmt(self, stmt: m.TypeStmt) -> None:
+        type: Type = stmt.type.accept(self)
+        for param in stmt.params:
+            if param.bound is not None:
+                param.bound.accept(self)
+        name: str = stmt.name.lexeme
+        self.define_type(name, AliasType(name=name, type=type))
 
     def visit_property_stmt(self, stmt: m.PropertyStmt) -> None: ...
 
@@ -127,27 +146,41 @@ class MidasResolver(m.Stmt.Visitor[None], m.Expr.Visitor[Type]):
 
     def visit_predicate_stmt(self, stmt: m.PredicateStmt) -> None: ...
 
-    def visit_simple_type_expr(self, expr: m.SimpleTypeExpr) -> Type:
-        return self.get_type(expr.name.lexeme)
+    def visit_logical_expr(self, expr: m.LogicalExpr) -> None: ...
 
-    def visit_logical_expr(self, expr: m.LogicalExpr) -> Type: ...
+    def visit_binary_expr(self, expr: m.BinaryExpr) -> None: ...
 
-    def visit_binary_expr(self, expr: m.BinaryExpr) -> Type: ...
+    def visit_unary_expr(self, expr: m.UnaryExpr) -> None: ...
 
-    def visit_unary_expr(self, expr: m.UnaryExpr) -> Type: ...
+    def visit_get_expr(self, expr: m.GetExpr) -> None: ...
 
-    def visit_get_expr(self, expr: m.GetExpr) -> Type: ...
+    def visit_variable_expr(self, expr: m.VariableExpr) -> None: ...
 
-    def visit_variable_expr(self, expr: m.VariableExpr) -> Type: ...
-
-    def visit_grouping_expr(self, expr: m.GroupingExpr) -> Type:
+    def visit_grouping_expr(self, expr: m.GroupingExpr) -> None:
         return expr.expr.accept(self)
 
-    def visit_literal_expr(self, expr: m.LiteralExpr) -> Type: ...
+    def visit_literal_expr(self, expr: m.LiteralExpr) -> None: ...
 
-    def visit_wildcard_expr(self, expr: m.WildcardExpr) -> Type: ...
+    def visit_wildcard_expr(self, expr: m.WildcardExpr) -> None: ...
 
-    def visit_template_expr(self, expr: m.TemplateExpr) -> Type: ...
+    def visit_named_type(self, type: m.NamedType) -> Type:
+        return self.get_type(type.name.lexeme)
 
-    def visit_type_expr(self, expr: m.TypeExpr) -> Type:
-        return self.get_type(expr.name.lexeme)
+    def visit_generic_type(self, type: m.GenericType) -> Type:
+        type_: Type = type.type.accept(self)
+        params: list[Type] = [param.accept(self) for param in type.params]
+        # TODO
+        return UnknownType()
+
+    def visit_constraint_type(self, type: m.ConstraintType) -> Type:
+        type_: Type = type.type.accept(self)
+        type.constraint.accept(self)
+        # TODO
+        return UnknownType()
+
+    def visit_complex_type(self, type: m.ComplexType) -> Type:
+        return ComplexType(
+            properties={
+                prop.name.lexeme: prop.type.accept(self) for prop in type.properties
+            }
+        )

midas/resolver/resolver.py

@@ -111,9 +111,8 @@ class Resolver(p.Stmt.Visitor[None], p.Expr.Visitor[None]):
         self.resolve(stmt.value)
         for target in stmt.targets:
             match target:
-                case p.VariableExpr(name=name):
-                    self.resolve_local(target, name)
-                    # TODO: declare if not found
+                case p.VariableExpr() | p.GetExpr():
+                    target.accept(self)
                 case _:
                     raise Exception(f"Unsupported assignment to {target}")
 
@@ -174,10 +173,6 @@ class Resolver(p.Stmt.Visitor[None], p.Expr.Visitor[None]):
         self.resolve(expr.left)
         self.resolve(expr.right)
 
-    def visit_set_expr(self, expr: p.SetExpr) -> None:
-        self.resolve(expr.value)
-        self.resolve(expr.object)
-
     def visit_cast_expr(self, expr: p.CastExpr) -> None:
         self.resolve(expr.expr)
 

syntax/midas.ebnf

@@ -19,16 +19,24 @@ Comparison ::= Unary (ComparisonOp Unary)*
 Equality ::= Comparison (EqualityOp Comparison)*
 Constraint ::= Equality ("&" Equality)*
 
-SimpleType ::= Identifier "?"?
-Template ::= "[" Type "]"
-Type ::= Identifier Template? "?"?
+TemplateParam ::= Identifier ("<:" Type)?
+Template ::= "[" (TemplateParam ("," TemplateParam)*)? "]"
+
+
+TypeProperty ::= Identifier ":" Type
+ComplexType ::= "{" TypeProperty* "}"
+NamedType ::= Identifier
+TypeParams ::= "[" (Type ("," Type)*)? "]"
+GenericType ::= NamedType TypeParams?
+GroupedType ::= "(" Type ")"
+BaseType ::= GroupedType | ComplexType | GenericType
+ConstraintType ::= BaseType ("where" Constraint)?
+Type ::= ConstraintType
 
-TypeProperty ::= Identifier ":" Type ("where" Constraints)?
-ComplexTypeBody ::= "{" TypeProperty* "}"
 OpDefinition ::= "op" Identifier "(" Type ")" "->" Type
 ExtendBody ::= "{" OpDefinition* "}"
 
-TypeStatement ::= "type" Identifier Template? ("(" Type ")" ("where" Constraint)? | ComplexTypeBody)
+TypeStatement ::= "type" Identifier Template? "=" Type
 ExtendStatement ::= "extend" Type ExtendBody
 PredicateStatement ::= "predicate" Identifier "(" Identifier ":" Type ")" "=" Constraint
 

syntax/midas.typ

@@ -43,28 +43,52 @@ svg.railroad .terminal rect {
 {[`constraint` 'equality'*"&"]}
 ```
 
-#let simple-type = ```
-{[`simple-type` 'identifier' <!, "?">]}
+#let template-param = ```
+{[`template-param` 'identifier' <!, ["<:" 'type']>]}
 ```
 
 #let template = ```
-{[`template` "[" 'type' "]"]}
-```
-
-#let type = ```
-{[`type` 'identifier' <!, 'template'> <!, "?">]}
+{[`template` "[" <!, 'template-param'*","> "]"]}
 ```
 
 #let type-property = ```
-{[`type-property` 'identifier' ":" 'type' <!, ["where" 'constraint']>]}
+{[`type-property` 'identifier' ":" 'type']}
 ```
 
-#let type-body = ```
-{[`type-body` "{" <!, 'type-property'*!> "}"]}
+#let complex-type = ```
+{[`complex-type` "{" <!, 'type-property'*!> "}"]}
+```
+
+#let named-type = ```
+{[`named-type` 'identifier']}
+```
+
+#let type-params = ```
+{[`type-params` "[" <!, 'type'*","> "]"]}
+```
+
+#let generic-type = ```
+{[`generic-type` 'named-type' <!, 'type-params'>]}
+```
+
+#let grouped-type = ```
+{[`grouped-type` "(" 'type' ")"]}
+```
+
+#let base-type = ```
+{[`base-type` <'grouped-type', 'complex-type', 'generic-type'>]}
+```
+
+#let constraint-type = ```
+{[`constraint-type` 'base-type' <!, ["where" 'constraint']>]}
+```
+
+#let type = ```
+{[`type` 'constraint-type']}
 ```
 
 #let type-statement = ```
-{[`type-statement` "type" 'identifier' <!, 'template'> <[["(" 'type' ")"] <!, ["where" 'constraint']>], 'type-body'>]}
+{[`type-statement` "type" 'identifier' <!, 'template'> "=" 'type']}
 ```
 
 #let op-definition = ```
@@ -92,11 +116,17 @@ svg.railroad .terminal rect {
   comparison: comparison,
   equality: equality,
   constraint: constraint,
-  simple-type: simple-type,
+  template-param: template-param,
   template: template,
-  type: type,
   type-property: type-property,
-  type-body: type-body,
+  complex-type: complex-type,
+  named-type: named-type,
+  type-params: type-params,
+  generic-type: generic-type,
+  grouped-type: grouped-type,
+  base-type: base-type,
+  constraint-type: constraint-type,
+  type: type,
   type-statement: type-statement,
   op-definition: op-definition,
   extend-statement: extend-statement,
@@ -107,10 +137,16 @@ svg.railroad .terminal rect {
 #let inline = (
   "grouping",
   "value",
+  "template-param",
   "template",
-  "simple-type",
   "type-property",
-  "type-body",
+  "complex-type",
+  "type-params",
+  "named-type",
+  "grouped-type",
+  "generic-type",
+  "base-type",
+  "constraint-type",
   "op-definition",
   "type-statement",
   "extend-statement",

tests/base.py

@@ -29,7 +29,7 @@ class Tester(ABC):
     def _list_tests(self) -> list[Path]: ...
 
     def run_all_tests(self) -> bool:
-        paths: list[Path] = self._list_tests()
+        paths: list[Path] = sorted(self._list_tests())
         return self.run_tests(paths)
 
     def run_tests(self, tests: list[Path]) -> bool:
@@ -40,7 +40,7 @@ class Tester(ABC):
 
         print(rule)
         for i, test in enumerate(tests):
-            print(f"Case {i+1}/{n}: {test.relative_to(self.CASES_DIR)}")
+            print(f"Case {i+1}/{n}: {test.resolve().relative_to(self.CASES_DIR)}")
             success: bool = self._run_test(test)
             if success:
                 successes += 1
@@ -78,7 +78,7 @@ class Tester(ABC):
     def _exec_case(self, path: Path) -> CaseResult: ...
 
     def update_all_tests(self):
-        paths: list[Path] = self._list_tests()
+        paths: list[Path] = sorted(self._list_tests())
         return self.update_tests(paths)
 
     def update_tests(self, tests: list[Path]):
@@ -141,3 +141,9 @@ class Tester(ABC):
                     success = tester.run_tests(args.FILE)
                 if not success:
                     sys.exit(1)
+            case None:
+                print("No subcommand provided. Available subcommands: run, update")
+                sys.exit(1)
+            case _:
+                print(f"Unknown subcommand '{args.subcommand}'")
+                sys.exit(1)

tests/cases/checker/01_simple_types.py.ref.json

@@ -1,3 +1,4 @@
 {
-  "diagnostics": []
+  "diagnostics": [],
+  "judgments": []
 }

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

@@ -13,34 +13,167 @@
         ]
       },
       "message": "Cannot assign BaseType(name='str') to c of type BaseType(name='int')"
+    }
+  ],
+  "judgments": [
+    {
+      "location": {
+        "from": "L1:9",
+        "to": "L1:10"
+      },
+      "expr": {
+        "_type": "LiteralExpr",
+        "value": 3
+      },
+      "type": {
+        "name": "int"
+      }
     },
     {
-      "type": "Error",
       "location": {
-        "start": [
-          9,
-          4
-        ],
-        "end": [
-          9,
-          9
-        ]
+        "from": "L2:9",
+        "to": "L2:10"
       },
-      "message": "Undefined operation __add__ between BaseType(name='bool') and BaseType(name='bool')"
+      "expr": {
+        "_type": "LiteralExpr",
+        "value": 4
+      },
+      "type": {
+        "name": "int"
+      }
     },
     {
-      "type": "Error",
       "location": {
-        "start": [
-          11,
-          0
-        ],
-        "end": [
-          11,
-          12
-        ]
+        "from": "L4:4",
+        "to": "L4:5"
       },
-      "message": "Cannot assign BaseType(name='int') to f of type BaseType(name='float')"
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "a"
+      },
+      "type": {
+        "name": "int"
+      }
+    },
+    {
+      "location": {
+        "from": "L4:8",
+        "to": "L4:9"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "b"
+      },
+      "type": {
+        "name": "int"
+      }
+    },
+    {
+      "location": {
+        "from": "L4:4",
+        "to": "L4:9"
+      },
+      "expr": {
+        "_type": "BinaryExpr",
+        "left": {
+          "_type": "VariableExpr",
+          "name": "a"
+        },
+        "operator": "+",
+        "right": {
+          "_type": "VariableExpr",
+          "name": "b"
+        }
+      },
+      "type": {
+        "name": "int"
+      }
+    },
+    {
+      "location": {
+        "from": "L6:4",
+        "to": "L6:13"
+      },
+      "expr": {
+        "_type": "LiteralExpr",
+        "value": "invalid"
+      },
+      "type": {
+        "name": "str"
+      }
+    },
+    {
+      "location": {
+        "from": "L8:4",
+        "to": "L8:8"
+      },
+      "expr": {
+        "_type": "LiteralExpr",
+        "value": true
+      },
+      "type": {
+        "name": "bool"
+      }
+    },
+    {
+      "location": {
+        "from": "L9:4",
+        "to": "L9:5"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "d"
+      },
+      "type": {
+        "name": "bool"
+      }
+    },
+    {
+      "location": {
+        "from": "L9:8",
+        "to": "L9:9"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "d"
+      },
+      "type": {
+        "name": "bool"
+      }
+    },
+    {
+      "location": {
+        "from": "L9:4",
+        "to": "L9:9"
+      },
+      "expr": {
+        "_type": "BinaryExpr",
+        "left": {
+          "_type": "VariableExpr",
+          "name": "d"
+        },
+        "operator": "+",
+        "right": {
+          "_type": "VariableExpr",
+          "name": "d"
+        }
+      },
+      "type": {
+        "name": "int"
+      }
+    },
+    {
+      "location": {
+        "from": "L11:11",
+        "to": "L11:12"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "a"
+      },
+      "type": {
+        "name": "int"
+      }
     }
   ]
 }

tests/cases/checker/04_custom_types.midas

@@ -1,6 +1,6 @@
-type Meter(float)
-type Second(float)
-type MeterPerSecond(float)
+type Meter = float
+type Second = float
+type MeterPerSecond = float
 
 extend Meter {
     op __add__(Meter) -> Meter

tests/cases/checker/04_custom_types.py

@@ -1,8 +1,6 @@
 # type: ignore
 # ruff: disable [F821]
 
-midas.using("04_custom_types.midas")
-
 distance: Meter = cast(Meter, 123.45)
 time: Second = cast(Second, 6.7)
 speed = distance / time

tests/cases/checker/04_custom_types.py.ref.json

@@ -1,3 +1,109 @@
 {
-  "diagnostics": []
+  "diagnostics": [],
+  "judgments": [
+    {
+      "location": {
+        "from": "L4:18",
+        "to": "L4:37"
+      },
+      "expr": {
+        "_type": "CastExpr",
+        "type": {
+          "_type": "BaseType",
+          "base": "Meter",
+          "param": null
+        },
+        "expr": {
+          "_type": "LiteralExpr",
+          "value": 123.45
+        }
+      },
+      "type": {
+        "name": "Meter",
+        "type": {
+          "name": "float"
+        }
+      }
+    },
+    {
+      "location": {
+        "from": "L5:15",
+        "to": "L5:32"
+      },
+      "expr": {
+        "_type": "CastExpr",
+        "type": {
+          "_type": "BaseType",
+          "base": "Second",
+          "param": null
+        },
+        "expr": {
+          "_type": "LiteralExpr",
+          "value": 6.7
+        }
+      },
+      "type": {
+        "name": "Second",
+        "type": {
+          "name": "float"
+        }
+      }
+    },
+    {
+      "location": {
+        "from": "L6:8",
+        "to": "L6:16"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "distance"
+      },
+      "type": {
+        "name": "Meter",
+        "type": {
+          "name": "float"
+        }
+      }
+    },
+    {
+      "location": {
+        "from": "L6:19",
+        "to": "L6:23"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "time"
+      },
+      "type": {
+        "name": "Second",
+        "type": {
+          "name": "float"
+        }
+      }
+    },
+    {
+      "location": {
+        "from": "L6:8",
+        "to": "L6:23"
+      },
+      "expr": {
+        "_type": "BinaryExpr",
+        "left": {
+          "_type": "VariableExpr",
+          "name": "distance"
+        },
+        "operator": "/",
+        "right": {
+          "_type": "VariableExpr",
+          "name": "time"
+        }
+      },
+      "type": {
+        "name": "MeterPerSecond",
+        "type": {
+          "name": "float"
+        }
+      }
+    }
+  ]
 }

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

@@ -42,5 +42,215 @@
       },
       "message": "Mixed return types: [BaseType(name='int'), BaseType(name='str')]"
     }
+  ],
+  "judgments": [
+    {
+      "location": {
+        "from": "L2:11",
+        "to": "L2:12"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "a"
+      },
+      "type": {
+        "name": "int"
+      }
+    },
+    {
+      "location": {
+        "from": "L2:15",
+        "to": "L2:16"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "b"
+      },
+      "type": {
+        "name": "int"
+      }
+    },
+    {
+      "location": {
+        "from": "L5:7",
+        "to": "L5:8"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "a"
+      },
+      "type": {
+        "name": "int"
+      }
+    },
+    {
+      "location": {
+        "from": "L5:11",
+        "to": "L5:12"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "b"
+      },
+      "type": {
+        "name": "int"
+      }
+    },
+    {
+      "location": {
+        "from": "L6:15",
+        "to": "L6:16"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "b"
+      },
+      "type": {
+        "name": "int"
+      }
+    },
+    {
+      "location": {
+        "from": "L6:19",
+        "to": "L6:20"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "a"
+      },
+      "type": {
+        "name": "int"
+      }
+    },
+    {
+      "location": {
+        "from": "L8:15",
+        "to": "L8:16"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "a"
+      },
+      "type": {
+        "name": "int"
+      }
+    },
+    {
+      "location": {
+        "from": "L8:19",
+        "to": "L8:20"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "b"
+      },
+      "type": {
+        "name": "int"
+      }
+    },
+    {
+      "location": {
+        "from": "L15:7",
+        "to": "L15:8"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "a"
+      },
+      "type": {
+        "name": "int"
+      }
+    },
+    {
+      "location": {
+        "from": "L15:11",
+        "to": "L15:13"
+      },
+      "expr": {
+        "_type": "LiteralExpr",
+        "value": 10
+      },
+      "type": {
+        "name": "int"
+      }
+    },
+    {
+      "location": {
+        "from": "L16:15",
+        "to": "L16:16"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "a"
+      },
+      "type": {
+        "name": "int"
+      }
+    },
+    {
+      "location": {
+        "from": "L16:19",
+        "to": "L16:21"
+      },
+      "expr": {
+        "_type": "LiteralExpr",
+        "value": 10
+      },
+      "type": {
+        "name": "int"
+      }
+    },
+    {
+      "location": {
+        "from": "L22:7",
+        "to": "L22:8"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "a"
+      },
+      "type": {
+        "name": "int"
+      }
+    },
+    {
+      "location": {
+        "from": "L22:11",
+        "to": "L22:12"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "b"
+      },
+      "type": {
+        "name": "int"
+      }
+    },
+    {
+      "location": {
+        "from": "L23:15",
+        "to": "L23:16"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "b"
+      },
+      "type": {
+        "name": "int"
+      }
+    },
+    {
+      "location": {
+        "from": "L23:19",
+        "to": "L23:20"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "a"
+      },
+      "type": {
+        "name": "int"
+      }
+    }
   ]
 }

tests/cases/checker/06_subtyping.py

@@ -0,0 +1,12 @@
+v1: int = 3
+v2: float = 4
+
+
+def maximum(a: float, b: float):
+    if b > a:
+        return b
+    return a
+
+
+v3 = maximum(v1, v2)
+v3 = v1 + v2

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

@@ -0,0 +1,193 @@
+{
+  "diagnostics": [],
+  "judgments": [
+    {
+      "location": {
+        "from": "L1:10",
+        "to": "L1:11"
+      },
+      "expr": {
+        "_type": "LiteralExpr",
+        "value": 3
+      },
+      "type": {
+        "name": "int"
+      }
+    },
+    {
+      "location": {
+        "from": "L2:12",
+        "to": "L2:13"
+      },
+      "expr": {
+        "_type": "LiteralExpr",
+        "value": 4
+      },
+      "type": {
+        "name": "int"
+      }
+    },
+    {
+      "location": {
+        "from": "L6:7",
+        "to": "L6:8"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "b"
+      },
+      "type": {
+        "name": "float"
+      }
+    },
+    {
+      "location": {
+        "from": "L6:11",
+        "to": "L6:12"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "a"
+      },
+      "type": {
+        "name": "float"
+      }
+    },
+    {
+      "location": {
+        "from": "L11:5",
+        "to": "L11:12"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "maximum"
+      },
+      "type": {
+        "name": "maximum",
+        "pos_args": [],
+        "args": [
+          {
+            "pos": 0,
+            "name": "a",
+            "type": {
+              "name": "float"
+            },
+            "required": true
+          },
+          {
+            "pos": 1,
+            "name": "b",
+            "type": {
+              "name": "float"
+            },
+            "required": true
+          }
+        ],
+        "kw_args": [],
+        "returns": {
+          "name": "float"
+        }
+      }
+    },
+    {
+      "location": {
+        "from": "L11:13",
+        "to": "L11:15"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "v1"
+      },
+      "type": {
+        "name": "int"
+      }
+    },
+    {
+      "location": {
+        "from": "L11:17",
+        "to": "L11:19"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "v2"
+      },
+      "type": {
+        "name": "float"
+      }
+    },
+    {
+      "location": {
+        "from": "L11:5",
+        "to": "L11:20"
+      },
+      "expr": {
+        "_type": "CallExpr",
+        "callee": {
+          "_type": "VariableExpr",
+          "name": "maximum"
+        },
+        "arguments": [
+          {
+            "_type": "VariableExpr",
+            "name": "v1"
+          },
+          {
+            "_type": "VariableExpr",
+            "name": "v2"
+          }
+        ],
+        "keywords": {}
+      },
+      "type": {
+        "name": "float"
+      }
+    },
+    {
+      "location": {
+        "from": "L12:5",
+        "to": "L12:7"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "v1"
+      },
+      "type": {
+        "name": "int"
+      }
+    },
+    {
+      "location": {
+        "from": "L12:10",
+        "to": "L12:12"
+      },
+      "expr": {
+        "_type": "VariableExpr",
+        "name": "v2"
+      },
+      "type": {
+        "name": "float"
+      }
+    },
+    {
+      "location": {
+        "from": "L12:5",
+        "to": "L12:12"
+      },
+      "expr": {
+        "_type": "BinaryExpr",
+        "left": {
+          "_type": "VariableExpr",
+          "name": "v1"
+        },
+        "operator": "+",
+        "right": {
+          "_type": "VariableExpr",
+          "name": "v2"
+        }
+      },
+      "type": {
+        "name": "float"
+      }
+    }
+  ]
+}

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

@@ -1,15 +1,15 @@
 // Simple custom type derived from float
-type Custom(float)
+type Custom = float
 
 // Simple custom types with constraints
-type Latitude(float) where (-90 <= _ <= 90)
-type Longitude(float) where (-180 <= _ <= 180)
+type Latitude = float where (-90 <= _ <= 90)
+type Longitude = float where (-180 <= _ <= 180)
 
 // Generic custom type (a Difference of T is derived from T, e.g. a difference of floats is a float
-type Difference[T](T)
+type Difference[T] = T
 
 // Complex custom type, containing two values accessible through properties
-type GeoLocation {
+type GeoLocation = {
     lat: Latitude
     lon: Longitude
 }
@@ -24,7 +24,7 @@ extend GeoLocation {
 
 // For complex generics, you need to specify how the genericity the properties
 // are handled
-type Difference[GeoLocation] {
+type Difference[GeoLocation] = {
     lat: Difference[Latitude]
     lon: Difference[Longitude]
 }
@@ -44,11 +44,11 @@ predicate StrictlyPositive(v: float) = v > 0
 predicate Equatorial(loc: GeoLocation) = (-10 <= loc.lat <= 10)
 predicate Arctic(loc: GeoLocation) = (loc.lat >= 66)
 
-type Person {
+type Person = {
     name: str
 
     // Property with an inline constraint
-    age: int? where (0 <= _ < 150)
+    age: Optional[int where (0 <= _ < 150)]
 
     // Property referencing a predicate
     height: float where StrictlyPositive

tests/cases/python-parser/02_custom_types.py

@@ -2,10 +2,6 @@
 # ruff: disable[F821]
 from __future__ import annotations
 
-import midas
-
-midas.using("02_custom_types.midas")
-
 df: Frame[
     location: GeoLocation
 ]

tests/cases/python-parser/02_custom_types.py.ref.json

@@ -1,26 +1,5 @@
 {
   "stmts": [
-    {
-      "_type": "ExpressionStmt",
-      "expr": {
-        "_type": "CallExpr",
-        "callee": {
-          "_type": "GetExpr",
-          "object": {
-            "_type": "VariableExpr",
-            "name": "midas"
-          },
-          "name": "using"
-        },
-        "arguments": [
-          {
-            "_type": "LiteralExpr",
-            "value": "02_custom_types.midas"
-          }
-        ],
-        "keywords": {}
-      }
-    },
     {
       "_type": "TypeAssign",
       "name": "df",

tests/checker.py

@@ -6,14 +6,17 @@ from pathlib import Path
 import midas.ast.python as p
 from midas.checker.checker import Checker
 from midas.checker.diagnostic import Diagnostic
+from midas.checker.types import Type
 from midas.parser.python import PythonParser
 from midas.resolver.resolver import Resolver
 from tests.base import Tester
+from tests.serializer.python import PythonAstJsonSerializer
 
 
 @dataclass
 class CaseResult:
     diagnostics: list[dict] = field(default_factory=list)
+    judgments: list = field(default_factory=list)
 
     def dumps(self) -> str:
         return json.dumps(asdict(self), indent=2)
@@ -33,6 +36,10 @@ class CheckerTester(Tester):
         if not path.is_file():
             raise TypeError(f"Test '{path}' is not a file")
 
+        types_paths: list[Path] = []
+        types_path: Path = path.with_suffix(".midas")
+        if types_path.exists():
+            types_paths.append(types_path)
         source: str = path.read_text()
         tree: ast.Module = ast.parse(source, filename=path)
         parser = PythonParser()
@@ -40,7 +47,12 @@ class CheckerTester(Tester):
         resolver = Resolver()
         resolver.resolve(*stmts)
         result: CaseResult = CaseResult()
-        checker = Checker(resolver.locals, file_path=path)
+        checker = Checker(
+            resolver.locals,
+            source_path=path,
+            types_paths=types_paths,
+        )
+
         diagnostics: list[Diagnostic] = checker.check(stmts)
         for diagnostic in diagnostics:
             result.diagnostics.append(
@@ -60,6 +72,21 @@ class CheckerTester(Tester):
                 }
             )
 
+        judgements: list[tuple[p.Expr, Type]] = checker.judgements
+        serializer = PythonAstJsonSerializer()
+        for expr, type in judgements:
+            loc = expr.location
+            result.judgments.append(
+                {
+                    "location": {
+                        "from": f"L{loc.lineno}:{loc.col_offset}",
+                        "to": f"L{loc.end_lineno}:{loc.end_col_offset}",
+                    },
+                    "expr": expr.accept(serializer),
+                    "type": asdict(type),
+                }
+            )
+
         return result
 
 

tests/serializer/midas.py

@@ -2,56 +2,60 @@ from typing import Optional, Sequence
 
 from midas.ast.midas import (
     BinaryExpr,
-    ComplexTypeStmt,
+    ComplexType,
+    ConstraintType,
     Expr,
     ExtendStmt,
+    GenericType,
     GetExpr,
     GroupingExpr,
     LiteralExpr,
     LogicalExpr,
+    NamedType,
     OpStmt,
     PredicateStmt,
     PropertyStmt,
-    SimpleTypeExpr,
-    SimpleTypeStmt,
     Stmt,
-    TemplateExpr,
-    TypeExpr,
+    Type,
+    TypeStmt,
     UnaryExpr,
     VariableExpr,
     WildcardExpr,
 )
 
 
-class MidasAstJsonSerializer(Stmt.Visitor[dict], Expr.Visitor[dict]):
+class MidasAstJsonSerializer(
+    Stmt.Visitor[dict], Expr.Visitor[dict], Type.Visitor[dict]
+):
     """An AST serializer which produces a JSON-compatible structure"""
 
     def serialize(self, stmts: list[Stmt]) -> list[dict]:
         return [stmt.accept(self) for stmt in stmts]
 
-    def _serialize_optional(self, element: Optional[Stmt | Expr]) -> Optional[dict]:
+    def _serialize_optional(
+        self, element: Optional[Stmt | Expr | Type]
+    ) -> Optional[dict]:
         if element is None:
             return None
         return element.accept(self)
 
-    def _serialize_list(self, elements: Sequence[Stmt | Expr]) -> list[dict]:
+    def _serialize_list(self, elements: Sequence[Stmt | Expr | Type]) -> list[dict]:
         return [element.accept(self) for element in elements]
 
-    def visit_simple_type_stmt(self, stmt: SimpleTypeStmt) -> dict:
+    def visit_type_stmt(self, stmt: TypeStmt) -> dict:
         return {
-            "_type": "SimpleTypeStmt",
+            "_type": "TypeStmt",
             "name": stmt.name.lexeme,
-            "template": self._serialize_optional(stmt.template),
-            "base": stmt.base.accept(self),
-            "constraint": self._serialize_optional(stmt.constraint),
+            "params": [
+                self._serialize_type_stmt_template_param(param) for param in stmt.params
+            ],
+            "type": stmt.type.accept(self),
         }
 
-    def visit_complex_type_stmt(self, stmt: ComplexTypeStmt) -> dict:
+    def _serialize_type_stmt_template_param(self, param: TypeStmt.Param) -> dict:
         return {
-            "_type": "ComplexTypeStmt",
-            "name": stmt.name.lexeme,
-            "template": self._serialize_optional(stmt.template),
-            "properties": self._serialize_list(stmt.properties),
+            "name": param.name.lexeme,
+            "bound": self._serialize_optional(param.bound),
         }
 
     def visit_property_stmt(self, stmt: PropertyStmt) -> dict:
@@ -59,7 +63,6 @@ class MidasAstJsonSerializer(Stmt.Visitor[dict], Expr.Visitor[dict]):
             "_type": "PropertyStmt",
             "name": stmt.name.lexeme,
             "type": stmt.type.accept(self),
-            "constraint": self._serialize_optional(stmt.constraint),
         }
 
     def visit_extend_stmt(self, stmt: ExtendStmt) -> dict:
@@ -86,13 +89,6 @@ class MidasAstJsonSerializer(Stmt.Visitor[dict], Expr.Visitor[dict]):
             "condition": stmt.condition.accept(self),
         }
 
-    def visit_simple_type_expr(self, expr: SimpleTypeExpr) -> dict:
-        return {
-            "_type": "SimpleTypeExpr",
-            "name": expr.name.lexeme,
-            "optional": expr.optional,
-        }
-
     def visit_logical_expr(self, expr: LogicalExpr) -> dict:
         return {
             "_type": "LogicalExpr",
@@ -144,16 +140,28 @@ class MidasAstJsonSerializer(Stmt.Visitor[dict], Expr.Visitor[dict]):
     def visit_wildcard_expr(self, expr: WildcardExpr) -> dict:
         return {"_type": "WildcardExpr"}
 
-    def visit_template_expr(self, expr: TemplateExpr) -> dict:
+    def visit_named_type(self, type: NamedType) -> dict:
         return {
-            "_type": "TemplateExpr",
-            "type": expr.type.accept(self),
+            "_type": "NamedType",
+            "name": type.name.lexeme,
         }
 
-    def visit_type_expr(self, expr: TypeExpr) -> dict:
+    def visit_generic_type(self, type: GenericType) -> dict:
         return {
-            "_type": "TypeExpr",
-            "name": expr.name.lexeme,
-            "template": self._serialize_optional(expr.template),
-            "optional": expr.optional,
+            "_type": "GenericType",
+            "type": type.type.accept(self),
+            "params": self._serialize_list(type.params),
+        }
+
+    def visit_constraint_type(self, type: ConstraintType) -> dict:
+        return {
+            "_type": "ConstraintType",
+            "type": type.type.accept(self),
+            "constraint": type.constraint.accept(self),
+        }
+
+    def visit_complex_type(self, type: ComplexType) -> dict:
+        return {
+            "_type": "ComplexType",
+            "properties": self._serialize_list(type.properties),
         }

tests/serializer/python.py

@@ -20,8 +20,8 @@ from midas.ast.python import (
     LogicalExpr,
     MidasType,
     ReturnStmt,
-    SetExpr,
     Stmt,
+    TernaryExpr,
     TypeAssign,
     UnaryExpr,
     VariableExpr,
@@ -231,17 +231,17 @@ class PythonAstJsonSerializer(
             "right": expr.right.accept(self),
         }
 
-    def visit_set_expr(self, expr: SetExpr) -> dict:
-        return {
-            "_type": "SetExpr",
-            "object": expr.object.accept(self),
-            "name": expr.name,
-            "value": expr.value.accept(self),
-        }
-
     def visit_cast_expr(self, expr: CastExpr) -> dict:
         return {
             "_type": "CastExpr",
             "type": expr.type.accept(self),
             "expr": expr.expr.accept(self),
         }
+
+    def visit_ternary_expr(self, expr: TernaryExpr) -> dict:
+        return {
+            "_type": "TernaryExpr",
+            "test": expr.test.accept(self),
+            "if_true": expr.if_true.accept(self),
+            "if_false": expr.if_false.accept(self),
+        }