Merge pull request 'Update README' (#14) from fix/update-readme into main

Reviewed-on: #14

README.md

@@ -1,4 +1,4 @@
-# Midas
+<h1>Midas</h1>
 
 *Midas* is a type system to _Maintain Integrity of Data with Annotated Structures_. In Greek mythology, [Midas](https://en.wikipedia.org/wiki/Midas) was a Phrygian king who was blessed with the gift of turning everything he touched into gold.
 
@@ -6,6 +6,24 @@
 
 This framework is being developed as part of a Bachelor's Thesis by Louis Heredero at HEI Sion.
 
+<details>
+<summary><strong>Table of Contents</strong></summary>
+
+- [Requirements](#requirements)
+- [Installation](#installation)
+- [Commands](#commands)
+  - [Type Checking](#type-checking)
+  - [Compiling](#compiling)
+  - [Formatting](#formatting)
+  - [Highlighting](#highlighting)
+  - [Dumping the AST](#dumping-the-ast)
+  - [Dumping the Registry](#dumping-the-registry)
+  - [Showing Type Judgements](#showing-type-judgements)
+  - [Validating Definitions](#validating-definitions)
+- [Tests](#tests)
+</details>
+
+
 ## Requirements
 
 - Python 3.11+
@@ -32,10 +50,26 @@ This framework is being developed as part of a Bachelor's Thesis by Louis Herede
 
 ## Commands
 
-### Compiling
+<!--
+check
+compile
+format
+highlight
+parse
+dump_registry
+types
+validate
+-->
 
-> [!NOTE]
+### Type Checking
-> 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 check -t types.midas source.py
+```
+
+This command parses the given files and run the type checkers against the Midas definitions and Python program. Diagnostics are then printed showing warnings and errors.
+
+### Compiling
 
 ```shell
 midas compile -t types.midas source.py
@@ -43,14 +77,22 @@ 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))
+### Formatting
+
+```shell
+midas format types.midas
+midas format types.midas -o formatted.midas
+```
+
+This command parses the given Midas file and outputs a pretty printed file from the AST.
 
 ### Highlighting
 
 ```shell
-midas utils highlight source.py
+midas highlight source.py
-# or
+midas highlight source.py -o highlighted.html
-midas utils highlight types.midas
+midas highlight types.midas
+midas highlight types.midas -o highlighted.html
 ```
 
 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.)
@@ -60,14 +102,35 @@ The optional `-o FILE` option can be used to specify an output path. By default,
 ### Dumping the AST
 
 ```shell
-midas utils dump-ast source.py
+midas parse source.py
-# or
+midas parse types.midas
-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.
+For debugging purposes, you can output the AST parsed from a Python or Midas file. For Python files, the `--raw` flags lets you toggle the custom AST parsing. With `--raw`, 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 -`).
+### Dumping the Registry
+
+```shell
+midas dump-registry -t types.midas
+```
+
+This command processes the given Midas definitions and dumps the contents of the types registry.
+
+### Showing Type Judgements
+
+```shell
+midas types -t types.midas source.py
+```
+
+This command type checks the given Python source file and logs all typing judgements made by the type checker.
+
+### Validating Definitions
+
+```shell
+midas validate types.midas
+```
+
+This command lets you validate a Midas definition file by running the parser and type checker, verifying syntax and references.
 
 ## Tests
 
@@ -77,6 +140,7 @@ Several snapshot tests are available to assert the good behaviour of the parsers
 uv run -m tests.midas run -a
 uv run -m tests.python run -a
 uv run -m tests.checker run -a
+uv run -m tests.generator run -a
 ```
 
 **Available subcommands:**

gen/python.py

@@ -157,6 +157,11 @@ class ListExpr:
     items: list[Expr]
 
 
+class DictExpr:
+    keys: list[Optional[Expr]]
+    values: list[Expr]
+
+
 class SubscriptExpr:
     object: Expr
     index: Expr

midas/ast/printer.py

@@ -745,6 +745,27 @@ class PythonAstPrinter(
                         self._mark_last()
                     item.accept(self)
 
+    def visit_dict_expr(self, expr: p.DictExpr) -> None:
+        self._write_line("DictExpr")
+        with self._child_level():
+            self._write_line("keys")
+            with self._child_level():
+                for i, key in enumerate(expr.keys):
+                    self._idx = i
+                    if i == len(expr.keys) - 1:
+                        self._mark_last()
+                    if key is None:
+                        self._write_line("None")
+                    else:
+                        key.accept(self)
+            self._write_line("values", last=True)
+            with self._child_level():
+                for i, value in enumerate(expr.values):
+                    self._idx = i
+                    if i == len(expr.values) - 1:
+                        self._mark_last()
+                    value.accept(self)
+
     def visit_subscript_expr(self, expr: p.SubscriptExpr) -> None:
         self._write_line("SubscriptExpr")
         with self._child_level():

midas/ast/python.py

@@ -259,6 +259,9 @@ class Expr(ABC):
         @abstractmethod
         def visit_list_expr(self, expr: ListExpr) -> T: ...
 
+        @abstractmethod
+        def visit_dict_expr(self, expr: DictExpr) -> T: ...
+
         @abstractmethod
         def visit_subscript_expr(self, expr: SubscriptExpr) -> T: ...
 
@@ -370,6 +373,15 @@ class ListExpr(Expr):
         return visitor.visit_list_expr(self)
 
 
+@dataclass(frozen=True)
+class DictExpr(Expr):
+    keys: list[Optional[Expr]]
+    values: list[Expr]
+
+    def accept(self, visitor: Expr.Visitor[T]) -> T:
+        return visitor.visit_dict_expr(self)
+
+
 @dataclass(frozen=True)
 class SubscriptExpr(Expr):
     object: Expr

midas/checker/builtins.midas

@@ -150,3 +150,32 @@ extend list[T] {
 
     prop __doc__: str
 }
+
+extend dict[K, V] {
+    def copy: fn() -> dict[K, V]
+    def keys: fn() -> list[K]  // TODO: use builtin types
+    def values: fn() -> list[V]  // TODO: use builtin types
+    // def items: fn() -> list[tuple[K, V]]  // TODO: use builtin types
+    
+    // def get: fn(key: K, default: None = None, /) -> V | None
+    def get: fn(key: K, default: V, /) -> V
+    // def get: fn[T](key: K, default: T, /) -> V | T
+    def pop: fn(key: K, /) -> V
+    def pop: fn(key: K, default: V, /) -> V
+    // def pop: fn[T](key: K, default: T, /) -> V | T
+    def __len__: fn() -> int
+    def __getitem__: fn(key: K, /) -> V
+    def __setitem__: fn(key: K, value: V, /) -> None
+    def __delitem__: fn(key: K, /) -> None
+    // def __iter__: fn() -> Iterator[K]
+    def __eq__: fn(value: object, /) -> bool
+    // def __reversed__: fn() -> Iterator[K]
+    
+    def __or__: fn(value: dict[K, V], /) -> dict[K, V]
+    // def __or__: fn[K2, V2](value: dict[K2, V2], /) -> dict[K | K2, V | V2]
+    def __ror__: fn(value: dict[K, V], /) -> dict[K, V]
+    // def __ror__: fn[K2, V2](value: dict[K2, V2], /) -> dict[K | K2, V | V2]
+    // def __ior__: fn(value: SupportsKeysAndGetItem[K, V], /) -> dict[K, V]
+    // def __ior__: fn(value: Iterable[tuple[K, V]], /) -> dict[K, V]
+
+}

midas/checker/builtins.py

@@ -39,3 +39,14 @@ def define_builtins(reg: TypesRegistry):
             body=BaseType(name="list"),
         ),
     )
+    dict = reg.define_type(
+        "dict",
+        GenericType(
+            name="dict",
+            params=[
+                TypeVar(name="K", bound=None),
+                TypeVar(name="V", bound=None),
+            ],
+            body=BaseType(name="dict"),
+        ),
+    )

midas/checker/preamble.py

@@ -61,7 +61,7 @@ class Preamble(Environment):
         # TODO: more specific arg types
         self._def_function(
             name=name,
-            pos=[Param("object", TopType())],
+            pos=[Param("object", TopType(), required=False)],
             returns=self._types.get_type(name),
         )
 

midas/checker/python.py

@@ -552,6 +552,46 @@ class PythonTyper(
         )
         return self.types.apply_generic(list_type, [UnknownType()])
 
+    def visit_dict_expr(self, expr: p.DictExpr) -> Type:
+        dict_type: Type = self.types.get_type("dict")
+
+        key_types: list[Type] = []
+        value_types: list[Type] = []
+        for key, value in zip(expr.keys, expr.values):
+            if key is None:
+                self.reporter.warning(
+                    value.location, "Dictionary unpacking not supported"
+                )
+                continue
+            key_types.append(self.type_of(key))
+            value_types.append(self.type_of(value))
+
+        key_types = self.types.reduce_types(key_types)
+        value_types = self.types.reduce_types(value_types)
+
+        if len(key_types) == 0 or len(value_types) == 0:
+            return dict_type
+
+        key_type: Type = UnknownType()
+        value_type: Type = UnknownType()
+
+        if len(key_types) == 1:
+            key_type = key_types[0]
+        else:
+            self.reporter.error(
+                expr.location,
+                f"Heterogeneous dict keys: {key_types}",
+            )
+
+        if len(value_types) == 1:
+            value_type = value_types[0]
+        else:
+            self.reporter.error(
+                expr.location,
+                f"Heterogeneous dict values: {value_types}",
+            )
+        return self.types.apply_generic(dict_type, [key_type, value_type])
+
     def visit_subscript_expr(self, expr: p.SubscriptExpr) -> Type:
         object: Type = self.type_of(expr.object)
         operation: Optional[Type] = self.types.lookup_member(object, "__getitem__")

midas/checker/resolver.py

@@ -213,6 +213,13 @@ class Resolver(p.Stmt.Visitor[None], p.Expr.Visitor[None]):
         for item in expr.items:
             self.resolve(item)
 
+    def visit_dict_expr(self, expr: p.DictExpr) -> None:
+        for key in expr.keys:
+            if key is not None:
+                self.resolve(key)
+        for value in expr.values:
+            self.resolve(value)
+
     def visit_subscript_expr(self, expr: p.SubscriptExpr) -> None:
         self.resolve(expr.object)
         self.resolve(expr.index)

midas/generator/generator.py

@@ -4,8 +4,8 @@ from dataclasses import dataclass, field
 from pathlib import Path
 from typing import Optional
 
-from midas.ast.location import Location
 import midas.ast.python as p
+from midas.ast.location import Location
 from midas.checker.types import (
     AliasType,
     AppliedType,
@@ -139,6 +139,12 @@ class Generator(p.Stmt.Visitor[ast.stmt], p.Expr.Visitor[ast.expr]):
             elts=[item.accept(self) for item in expr.items],
         )
 
+    def visit_dict_expr(self, expr: p.DictExpr) -> ast.expr:
+        return ast.Dict(
+            keys=[key.accept(self) if key is not None else None for key in expr.keys],
+            values=[value.accept(self) for value in expr.values],
+        )
+
     def visit_subscript_expr(self, expr: p.SubscriptExpr) -> ast.expr:
         return ast.Subscript(
             value=expr.object.accept(self),

midas/parser/python.py

@@ -10,6 +10,7 @@ from midas.ast.python import (
     CastExpr,
     CompareExpr,
     ConstraintType,
+    DictExpr,
     Expr,
     ExpressionStmt,
     ForStmt,
@@ -447,6 +448,16 @@ class PythonParser:
                     items=[self.parse_expr(item) for item in items],
                 )
 
+            case ast.Dict(keys=keys, values=values):
+                return DictExpr(
+                    location=location,
+                    keys=[
+                        self.parse_expr(key) if key is not None else None
+                        for key in keys
+                    ],
+                    values=[self.parse_expr(value) for value in values],
+                )
+
             case ast.Subscript(value=value, slice=index):
                 return SubscriptExpr(
                     location=location,

tests/serializer/python.py

@@ -9,6 +9,7 @@ from midas.ast.python import (
     CastExpr,
     CompareExpr,
     ConstraintType,
+    DictExpr,
     Expr,
     ExpressionStmt,
     ForStmt,
@@ -278,6 +279,13 @@ class PythonAstJsonSerializer(
             "items": [item.accept(self) for item in expr.items],
         }
 
+    def visit_dict_expr(self, expr: DictExpr) -> dict:
+        return {
+            "_type": "DictExpr",
+            "keys": [self._serialize_optional(key) for key in expr.keys],
+            "values": self._serialize_list(expr.values),
+        }
+
     def visit_subscript_expr(self, expr: SubscriptExpr) -> dict:
         return {
             "_type": "SubscriptExpr",