From 732f7b079667644e1ea65af77ebd79aa34a322f4 Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Tue, 16 Jun 2026 14:02:45 +0200 Subject: [PATCH] feat(checker): add environment preamble this adds some builtin functions such as the builtin type constructors --- midas/checker/preamble.py | 121 ++++++++++++++++++++++++++++++++++++++ midas/checker/python.py | 3 +- midas/checker/types.py | 8 +-- 3 files changed, 127 insertions(+), 5 deletions(-) create mode 100644 midas/checker/preamble.py diff --git a/midas/checker/preamble.py b/midas/checker/preamble.py new file mode 100644 index 0000000..a543dd9 --- /dev/null +++ b/midas/checker/preamble.py @@ -0,0 +1,121 @@ +from dataclasses import dataclass + +from midas.checker.environment import Environment +from midas.checker.registry import TypesRegistry +from midas.checker.types import Function, GenericType, TopType, Type, TypeVar, UnitType + + +@dataclass(frozen=True) +class Param: + name: str + type: Type + required: bool = True + + +class Preamble(Environment): + def __init__(self, types: TypesRegistry) -> None: + super().__init__() + self._types: TypesRegistry = types + + self._def_type_constructor("object") + self._def_type_constructor("float") + self._def_type_constructor("int") + self._def_type_constructor("bool") + self._def_type_constructor("str") + self._def_function( + name="list", + pos=[Param("object", TopType())], + returns=self._list_of(TopType()), + ) + + # TODO: use sink + self._def_function( + name="print", + pos=[Param("object", TopType())], + returns=UnitType(), + ) + + map_in = TypeVar(name="T", bound=None) + map_out = TypeVar(name="U", bound=None) + mapper = self._make_function( + name="MapTransform", + pos=[Param("v", map_in)], + returns=map_out, + ) + self._def_function( + name="map", + pos=[ + Param("transform", mapper), + Param( + "iterable", + self._list_of(map_in), # TODO: replace with Iterable[T] + ), + ], + returns=self._list_of(map_out), # TODO: replace with Iterable[U] + ) + + def _list_of(self, item_type: Type) -> Type: + return self._types.apply_generic(self._types.get_type("list"), [item_type]) + + def _def_type_constructor(self, name: str): + # TODO: more specific arg types + self._def_function( + name=name, + pos=[Param("object", TopType())], + returns=self._types.get_type(name), + ) + + def _make_function( + self, + *, + name: str, + pos: list[Param] = [], + mixed: list[Param] = [], + kw: list[Param] = [], + returns: Type = UnitType(), + type_vars: list[TypeVar] = [], + ) -> Type: + def map_args(params: list[Param], offset: int) -> list[Function.Argument]: + return [ + Function.Argument( + pos=i + offset, + name=param.name, + type=param.type, + required=param.required, + ) + for i, param in enumerate(params) + ] + + function = Function( + pos_args=map_args(pos, 0), + args=map_args(mixed, len(pos)), + kw_args=map_args(kw, len(pos) + len(mixed)), + returns=returns, + ) + if len(type_vars) != 0: + function = GenericType( + name=name, + params=type_vars, + body=function, + ) + return function + + def _def_function( + self, + *, + name: str, + pos: list[Param] = [], + mixed: list[Param] = [], + kw: list[Param] = [], + returns: Type = UnitType(), + type_vars: list[TypeVar] = [], + ): + function: Type = self._make_function( + name=name, + pos=pos, + mixed=mixed, + kw=kw, + returns=returns, + type_vars=type_vars, + ) + self.define(name, function) diff --git a/midas/checker/python.py b/midas/checker/python.py index b4da4ba..6e6ea1a 100644 --- a/midas/checker/python.py +++ b/midas/checker/python.py @@ -7,6 +7,7 @@ import midas.ast.python as p from midas.ast.location import Location from midas.checker.environment import Environment from midas.checker.operators import COMPARATOR_METHODS, OPERATOR_METHODS, UNARY_METHODS +from midas.checker.preamble import Preamble from midas.checker.registry import TypesRegistry from midas.checker.reporter import FileReporter, Reporter from midas.checker.resolver import Resolver @@ -56,7 +57,7 @@ class PythonTyper( self.logger: logging.Logger = logging.getLogger("PythonTyper") self.reporter: FileReporter = reporter.for_file(None) self.types: TypesRegistry = types - self.global_env: Environment = Environment() + self.global_env: Environment = Preamble(self.types) self.env: Environment = self.global_env self.locals: dict[p.Expr, int] = {} self.judgements: list[tuple[p.Expr, Type]] = [] diff --git a/midas/checker/types.py b/midas/checker/types.py index c6d41d1..f2fef3b 100644 --- a/midas/checker/types.py +++ b/midas/checker/types.py @@ -1,6 +1,6 @@ from __future__ import annotations -from dataclasses import dataclass +from dataclasses import dataclass, field from typing import Optional @@ -41,9 +41,9 @@ class UnitType: @dataclass(frozen=True, kw_only=True) class Function: - pos_args: list[Argument] - args: list[Argument] - kw_args: list[Argument] + pos_args: list[Argument] = field(default_factory=list) + args: list[Argument] = field(default_factory=list) + kw_args: list[Argument] = field(default_factory=list) returns: Type def __str__(self) -> str: