From 0b91de75a8ec17b9560cfa17e996c8f02263996e Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Mon, 22 Jun 2026 14:13:25 +0200 Subject: [PATCH 01/14] feat(checker): handle type vars in python functions --- midas/checker/python.py | 78 +++++++++++++++++++++++++++++++++++- midas/generator/generator.py | 3 +- 2 files changed, 78 insertions(+), 3 deletions(-) diff --git a/midas/checker/python.py b/midas/checker/python.py index e1fb788..6a00249 100644 --- a/midas/checker/python.py +++ b/midas/checker/python.py @@ -22,8 +22,10 @@ from midas.checker.types import ( GenericType, OverloadedFunction, Type, + TypeVar, UnitType, UnknownType, + Variance, unfold_type, ) from midas.checker.unifier import Unifier @@ -229,7 +231,8 @@ class PythonTyper( ) pos += 1 - for arg in pos_args + args + kw_args: + all_args: list[Function.Argument] = pos_args + args + kw_args + for arg in all_args: env.define(arg.name, arg.type) returns_hint: Optional[Type] = None @@ -270,12 +273,25 @@ class PythonTyper( returns = inferred_return # TODO: handle *args and **kwargs sinks - function: Function = Function( + function: Type = Function( pos_args=pos_args, args=args, kw_args=kw_args, returns=returns, ) + generic_params: list[TypeVar] = [] + all_types: list[Type] = [arg.type for arg in all_args] + [returns] + for type in all_types: + if isinstance(type, TypeVar): + if type not in generic_params: + generic_params.append(type) + + if len(generic_params) != 0: + function = GenericType( + name=stmt.name, + params=generic_params, + body=function, + ) self.env.define(stmt.name, function) def visit_type_assign(self, stmt: p.TypeAssign) -> None: @@ -453,6 +469,10 @@ class PythonTyper( return result or UnknownType() def visit_call_expr(self, expr: p.CallExpr) -> Type: + match expr.callee: + case p.VariableExpr(name="TypeVar"): + return self.define_typevar(expr) or UnknownType() + callee: Type = self.type_of(expr.callee) positional: list[TypedExpr] = [ (arg, self.type_of(arg)) for arg in expr.arguments @@ -1033,3 +1053,57 @@ class PythonTyper( report_errors=False, ) return result + + def define_typevar(self, call: p.CallExpr) -> Optional[TypeVar]: + def is_kw_true(name: str) -> bool: + match call.keywords.get(name): + case p.LiteralExpr(value=True): + return True + case _: + return False + + match call: + case p.CallExpr( + arguments=[p.LiteralExpr(value=str() as name)], + ): + bound: Optional[Type] = None + variance: Variance = Variance.INVARIANT + if "bound" in call.keywords: + bound_type: p.MidasType = self._parse_type_from_expr( + call.keywords["bound"] + ) + bound = self.resolve_type_expr(bound_type) + + if is_kw_true("covariant"): + variance = Variance.COVARIANT + + if is_kw_true("contravariant"): + if variance == Variance.COVARIANT: + self.reporter.warning( + call.keywords["contravariant"].location, + "TypeVar cannot be covariant and contravariant at the same time. Marked as invariant", + ) + variance = Variance.INVARIANT + else: + variance = Variance.CONTRAVARIANT + var: TypeVar = TypeVar(name=name, bound=bound, variance=variance) + self.types.define_type(name, var) + return var + + case _: + self.reporter.warning( + call.location, "Invalid usage of 'TypeVar', skipping" + ) + return None + + def _parse_type_from_expr(self, expr: p.Expr) -> p.MidasType: + location: Location = expr.location + parser = PythonParser() + match expr: + case p.LiteralExpr(value=str() as value): + node: ast.Expression = ast.parse(value, mode="eval") + return parser._parse_type(node.body) + case p.VariableExpr(name=name): + return p.BaseType(location=location, base=name, param=None) + case _: + raise NotImplementedError diff --git a/midas/generator/generator.py b/midas/generator/generator.py index 22eab41..88065d2 100644 --- a/midas/generator/generator.py +++ b/midas/generator/generator.py @@ -323,7 +323,8 @@ class Generator(p.Stmt.Visitor[ast.stmt], p.Expr.Visitor[ast.expr]): self._make_constraint_assert(src_location, expr, constraint) case TypeVar(): - raise RuntimeError("Unexpected TypeVar") + # TODO: check with type from arguments / use call-site context + pass case ( TopType() From 878693383e823b2dfb200b99b3b7d7a14162ea68 Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Mon, 22 Jun 2026 14:14:05 +0200 Subject: [PATCH 02/14] feat(cli): add watch option to stubs command --- midas/cli/commands/stubs.py | 59 ++++++++++++++++++++++++++++++------- pyproject.toml | 6 +++- 2 files changed, 53 insertions(+), 12 deletions(-) diff --git a/midas/cli/commands/stubs.py b/midas/cli/commands/stubs.py index 98b3cd4..a5267c9 100644 --- a/midas/cli/commands/stubs.py +++ b/midas/cli/commands/stubs.py @@ -1,27 +1,64 @@ import ast +import time from pathlib import Path from typing import TextIO +import black import click +from watchdog.events import DirModifiedEvent, FileModifiedEvent, FileSystemEventHandler +from watchdog.observers import Observer from midas.checker.checker import TypeChecker from midas.generator.stubs import StubsGenerator -@click.command(help="Generate stubs from Midas definitions") -@click.argument("file", type=click.File("r")) -@click.option("-o", "--output", type=click.File("w"), default="-") -def stubs( - file: TextIO, - output: TextIO, -): - source_path: Path = Path(file.name).resolve() - +def generate_stubs(in_path: Path, out_path: Path): checker = TypeChecker() - checker.import_midas(source_path) + checker.import_midas(in_path) generator = StubsGenerator(checker.types) module: ast.Module = generator.generate_stubs() module = ast.fix_missing_locations(module) - output.write(ast.unparse(module)) + output: str = ast.unparse(module) + output = black.format_str(output, mode=black.Mode(is_pyi=True)) + + out_path.write_text(output) + + +class Handler(FileSystemEventHandler): + def __init__(self, in_path: Path, out_path: Path) -> None: + super().__init__() + self.in_path: Path = in_path + self.out_path: Path = out_path + + def on_modified(self, event: DirModifiedEvent | FileModifiedEvent) -> None: + generate_stubs(self.in_path, self.out_path) + + +@click.command(help="Generate stubs from Midas definitions") +@click.argument("file", type=click.File("r")) +@click.option("-o", "--output", type=click.File("w"), default="-") +@click.option("-w", "--watch", is_flag=True) +def stubs( + file: TextIO, + output: TextIO, + watch: bool, +): + source_path: Path = Path(file.name).resolve() + out_path: Path = Path(output.name).resolve() + generate_stubs(source_path, out_path) + + if watch: + print(f"Watching {source_path}...") + print("Press CTRL+C to stop") + handler = Handler(source_path, out_path) + observer = Observer() + observer.schedule(handler, str(source_path)) + observer.start() + try: + while True: + time.sleep(1) + except KeyboardInterrupt: + observer.stop() + observer.join() diff --git a/pyproject.toml b/pyproject.toml index 69a9f7e..48f3b21 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -8,7 +8,11 @@ authors = [ { name = "Louis Heredero", email = "louis.heredero@students.hevs.ch" }, ] classifiers = ["Programming Language :: Python :: 3"] -dependencies = ["click>=8.4.1"] +dependencies = [ + "black>=26.5.1", + "click>=8.4.1", + "watchdog>=6.0.0", +] [project.urls] Homepage = "https://git.kbk28.ch/HEL/midas" From 577454ee7e9ef60cdd22dc2ad24b991c4f1848a7 Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Mon, 22 Jun 2026 14:15:04 +0200 Subject: [PATCH 03/14] fix(checker): make UnknownType a top type for subtyping --- midas/checker/registry.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/midas/checker/registry.py b/midas/checker/registry.py index b787f20..606c268 100644 --- a/midas/checker/registry.py +++ b/midas/checker/registry.py @@ -130,6 +130,9 @@ class TypesRegistry: case (_, TopType()): return True + case (_, UnknownType()): + return True + case (AliasType(type=base1), _): return self.is_subtype(base1, type2) From 80af2b904815882e3aa9cd37688bda81e9f84ce0 Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Mon, 22 Jun 2026 14:44:51 +0200 Subject: [PATCH 04/14] fix(checker): handle is_subtype of TypeVar --- midas/checker/registry.py | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/midas/checker/registry.py b/midas/checker/registry.py index 606c268..8259b93 100644 --- a/midas/checker/registry.py +++ b/midas/checker/registry.py @@ -133,6 +133,16 @@ class TypesRegistry: case (_, UnknownType()): return True + case (TypeVar(bound=bound), _): + if bound is None: + return False + return self.is_subtype(bound, type2) + + case (_, TypeVar(bound=bound)): + if bound is None: + return True + return self.is_subtype(type1, bound) + case (AliasType(type=base1), _): return self.is_subtype(base1, type2) @@ -150,11 +160,6 @@ class TypesRegistry: case (Function(), Function()): return self.is_func_subtype(type1, type2) - case (TypeVar(bound=bound), _): - if bound is None: - return False - return self.is_subtype(bound, type2) - case (ConstraintType(type=base1), _): return self.is_subtype(base1, type2) From 2f29c4727437dcff7f1920914999fc5a951a5246 Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Mon, 22 Jun 2026 15:23:53 +0200 Subject: [PATCH 05/14] fix(gen): assert type var bound --- midas/generator/generator.py | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/midas/generator/generator.py b/midas/generator/generator.py index 88065d2..e66f532 100644 --- a/midas/generator/generator.py +++ b/midas/generator/generator.py @@ -322,9 +322,10 @@ class Generator(p.Stmt.Visitor[ast.stmt], p.Expr.Visitor[ast.expr]): self._make_cast_asserts(src_location, expr, base) self._make_constraint_assert(src_location, expr, constraint) - case TypeVar(): + case TypeVar(bound=bound): # TODO: check with type from arguments / use call-site context - pass + if bound is not None: + self._make_cast_asserts(src_location, expr, bound) case ( TopType() From f75d7722a17269315ac9f605b5eb5c04dcf26bf2 Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Mon, 22 Jun 2026 15:24:18 +0200 Subject: [PATCH 06/14] fix(checker): look up members on constraint type --- midas/checker/registry.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/midas/checker/registry.py b/midas/checker/registry.py index 8259b93..e52fb40 100644 --- a/midas/checker/registry.py +++ b/midas/checker/registry.py @@ -397,6 +397,9 @@ class TypesRegistry: ) return self.lookup_member(base, member_name) + case ConstraintType(type=base): + return self.lookup_member(base, member_name) + case UnknownType(): return UnknownType() From 216c80f08cdc30d312798ddec94121bb9e13b21b Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Mon, 22 Jun 2026 15:24:51 +0200 Subject: [PATCH 07/14] fix(checker): produce judgement for expression in cast --- midas/checker/python.py | 1 + 1 file changed, 1 insertion(+) diff --git a/midas/checker/python.py b/midas/checker/python.py index 6a00249..435f6f1 100644 --- a/midas/checker/python.py +++ b/midas/checker/python.py @@ -538,6 +538,7 @@ class PythonTyper( return UnknownType() def visit_cast_expr(self, expr: p.CastExpr) -> Type: + _ = self.type_of(expr.expr) return self.resolve_type_expr(expr.type) def visit_ternary_expr(self, expr: p.TernaryExpr) -> Type: From 0ba0266baee6b9bed00008c870236ced405a3bae Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Mon, 22 Jun 2026 15:27:06 +0200 Subject: [PATCH 08/14] fix(checker): check general subtype case for AppliedType this adds the case where we check whether AppliedType <: Type, and delegates to the body this may not be a legitimate rule, or may need to be refined --- midas/checker/registry.py | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/midas/checker/registry.py b/midas/checker/registry.py index e52fb40..93221af 100644 --- a/midas/checker/registry.py +++ b/midas/checker/registry.py @@ -181,6 +181,10 @@ class TypesRegistry: return False return True + # TODO: verify legitimacy + case (AppliedType(body=body), _): + return self.is_subtype(body, type2) + return False # TODO: verify the logic in here From 7e5ea5e41432e719ab7b9ef8d408a8a91036d5e2 Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Mon, 22 Jun 2026 15:29:39 +0200 Subject: [PATCH 09/14] chore: add example to demonstrate some features --- examples/02_demonstration/demo.midas | 10 ++++++++++ examples/02_demonstration/demo.py | 19 +++++++++++++++++++ 2 files changed, 29 insertions(+) create mode 100644 examples/02_demonstration/demo.midas create mode 100644 examples/02_demonstration/demo.py diff --git a/examples/02_demonstration/demo.midas b/examples/02_demonstration/demo.midas new file mode 100644 index 0000000..394cc15 --- /dev/null +++ b/examples/02_demonstration/demo.midas @@ -0,0 +1,10 @@ +predicate in_range(min: float, max: float)(v: float) = min <= v & v <= max +predicate is_ratio = in_range(0, 1) + +type Money = float +type Price[T <: Money] = T where _ >= 0 + +type EUR = Money +type USD = Money + +type Reduction = float where is_ratio(_) diff --git a/examples/02_demonstration/demo.py b/examples/02_demonstration/demo.py new file mode 100644 index 0000000..20e5bb5 --- /dev/null +++ b/examples/02_demonstration/demo.py @@ -0,0 +1,19 @@ +from typing import TypeVar, cast + +from demo_stubs import EUR, USD, Money, Price, Reduction + +T = TypeVar("T", bound=Money) + + +def apply_reduction(amount: Price[T], reduction: Reduction) -> Price[T]: + return cast(Price[T], (1.0 - reduction) * amount) + + +a1 = cast(Price[EUR], 3.2) +a2 = cast(Price[USD], 10.4) +r1: Reduction = cast(Reduction, 0.2) + +print(apply_reduction(a1, r1)) +print(apply_reduction(a2, r1)) + +# a3 = a1 + a2 From a50a2073855633cba0ee67194f103e8708dc19aa Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Mon, 22 Jun 2026 15:40:31 +0200 Subject: [PATCH 10/14] fix(gen): don't generate stubs for builtin types --- midas/generator/stubs.py | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/midas/generator/stubs.py b/midas/generator/stubs.py index d54c948..d148c49 100644 --- a/midas/generator/stubs.py +++ b/midas/generator/stubs.py @@ -39,6 +39,18 @@ class StubsGenerator: self.stubs = [] self.typing_imports = set() for name, type in self.types._types.items(): + # Skip builtin types, not just based on name so the user can override + # TODO: check if added members on builtin type + match type: + case BaseType(name=name_) if name == name_: + continue + case GenericType( + name=name1, + body=BaseType(name=name2), + ) if ( + name == name1 == name2 + ): + continue self.generate_stub(name, type) imports = [ From 7c771c4070b9a1a7fcebcda3d05b201728cdc013 Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Tue, 23 Jun 2026 00:22:38 +0200 Subject: [PATCH 11/14] feat(checker): add input function to preamble --- midas/checker/preamble.py | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/midas/checker/preamble.py b/midas/checker/preamble.py index 96a4ef7..1dcd157 100644 --- a/midas/checker/preamble.py +++ b/midas/checker/preamble.py @@ -54,6 +54,11 @@ class Preamble(Environment): returns=self._list_of(map_out), # TODO: replace with Iterable[U] type_vars=[map_in, map_out], ) + self._def_function( + name="input", + pos=[Param("prompt", TopType(), required=False)], + returns=self._types.get_type("str"), + ) def _list_of(self, item_type: Type) -> Type: return self._types.apply_generic(self._types.get_type("list"), [item_type]) From 093f2bc4776109cf1c98139732ac86c54e11849e Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Tue, 23 Jun 2026 00:24:37 +0200 Subject: [PATCH 12/14] fix(checker): lookup member on typevar bound --- midas/checker/registry.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/midas/checker/registry.py b/midas/checker/registry.py index 93221af..bbd3d85 100644 --- a/midas/checker/registry.py +++ b/midas/checker/registry.py @@ -404,6 +404,9 @@ class TypesRegistry: case ConstraintType(type=base): return self.lookup_member(base, member_name) + case TypeVar(bound=bound) if bound is not None: + return self.lookup_member(bound, member_name) + case UnknownType(): return UnknownType() From b290c59ac41ca35a178c28755fda97074c45fa9f Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Tue, 23 Jun 2026 00:25:43 +0200 Subject: [PATCH 13/14] fix(gen): add bases for ConstraintType and TypeVar --- midas/generator/stubs.py | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/midas/generator/stubs.py b/midas/generator/stubs.py index d148c49..c9a3804 100644 --- a/midas/generator/stubs.py +++ b/midas/generator/stubs.py @@ -127,6 +127,12 @@ class StubsGenerator: body_subsitutions | substitutions, ) + case ConstraintType(type=base): + return self.get_bases(base) + + case TypeVar(bound=bound) if bound is not None: + return [self.dump_type(bound)], {} + case _: return [], {} From d6b8fbfb60636b05603caa8eda8d30ef0dbe463f Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Tue, 23 Jun 2026 10:03:24 +0200 Subject: [PATCH 14/14] chore: improve demo example --- examples/02_demonstration/demo.midas | 15 ++++++++----- examples/02_demonstration/demo.py | 27 +++++++++++++++++------- examples/02_demonstration/demo_stubs.pyi | 14 ++++++++++++ 3 files changed, 43 insertions(+), 13 deletions(-) create mode 100644 examples/02_demonstration/demo_stubs.pyi diff --git a/examples/02_demonstration/demo.midas b/examples/02_demonstration/demo.midas index 394cc15..661a583 100644 --- a/examples/02_demonstration/demo.midas +++ b/examples/02_demonstration/demo.midas @@ -1,10 +1,15 @@ predicate in_range(min: float, max: float)(v: float) = min <= v & v <= max predicate is_ratio = in_range(0, 1) -type Money = float -type Price[T <: Money] = T where _ >= 0 +type Currency = float +type Price[T <: Currency] = T where _ >= 0 -type EUR = Money -type USD = Money +extend Price[T <: Currency] { + def __add__: fn(Price[T], /) -> Price[T] +} -type Reduction = float where is_ratio(_) +type EUR = Currency +type USD = Currency +type CHF = Currency + +type Discount = float where is_ratio(_) diff --git a/examples/02_demonstration/demo.py b/examples/02_demonstration/demo.py index 20e5bb5..c4ec322 100644 --- a/examples/02_demonstration/demo.py +++ b/examples/02_demonstration/demo.py @@ -1,19 +1,30 @@ from typing import TypeVar, cast -from demo_stubs import EUR, USD, Money, Price, Reduction +from demo_stubs import CHF, EUR, USD, Currency, Price, Discount -T = TypeVar("T", bound=Money) +T = TypeVar("T", bound=Currency) -def apply_reduction(amount: Price[T], reduction: Reduction) -> Price[T]: - return cast(Price[T], (1.0 - reduction) * amount) +def apply_discount(amount: Price[T], discount: Discount) -> Price[T]: + return cast(Price[T], (1.0 - discount) * amount) a1 = cast(Price[EUR], 3.2) a2 = cast(Price[USD], 10.4) -r1: Reduction = cast(Reduction, 0.2) +r1 = cast(Discount, 0.2) -print(apply_reduction(a1, r1)) -print(apply_reduction(a2, r1)) +print(apply_discount(a1, r1)) +print(apply_discount(a2, r1)) -# a3 = a1 + a2 +a3 = a1 + a1 +a4 = a1 + a2 # cannot add euros and dollars +a3 = a2 # cannot change variable type + +dyn_price = float(input("Price (CHF): ")) +dyn_discount = float(input("Discount (0.0-1.0): ")) +discounted = apply_discount( + cast(Price[CHF], dyn_price), + cast(Discount, dyn_discount), +) + +print(f"Discounted: CHF {discounted}") diff --git a/examples/02_demonstration/demo_stubs.pyi b/examples/02_demonstration/demo_stubs.pyi new file mode 100644 index 0000000..6615018 --- /dev/null +++ b/examples/02_demonstration/demo_stubs.pyi @@ -0,0 +1,14 @@ +from __future__ import annotations +from typing import Generic, TypeVar + +class Currency(float): ... + +_T0 = TypeVar("_T0", bound=Currency, covariant=True) + +class Price(Currency, Generic[_T0]): + def __add__(self, _0: Price[_T0], /) -> Price[_T0]: ... + +class EUR(Currency): ... +class USD(Currency): ... +class CHF(Currency): ... +class Discount(float): ...