Merge pull request 'Tidy examples and minor housekeeping' (#39) from feat/tidy-examples into main
All checks were successful
Tests / tests (push) Successful in 5s

Reviewed-on: #39
This commit was merged in pull request #39.
This commit is contained in:
2026-07-09 21:41:48 +00:00
21 changed files with 240 additions and 504 deletions

View File

@@ -1,5 +1,7 @@
<h1>Midas</h1>
<img src="https://git.kb28.ch/HEL/midas/actions/workflows/tests.yaml/badge.svg">
*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.
*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.

View File

@@ -1,150 +0,0 @@
#import "@preview/cetz:0.5.2": canvas, draw
#let diagram-only = false
#set document(
title: [Midas Architecture],
//author: "Louis Heredero",
)
#set text(
font: "Source Sans 3",
)
#let diagram = canvas({
let framed = draw.content.with(
padding: (x: .8em, y: 1em),
frame: "rect",
stroke: black,
)
let arrow = draw.line.with(mark: (end: ">", fill: black))
framed(
(0, 0),
name: "python-parser",
)[Python parser]
draw.content(
(rel: (0, 1), to: "python-parser.north"),
padding: 5pt,
anchor: "south",
name: "source-py",
)[_`source.py`_]
arrow("source-py", "python-parser")
framed(
(rel: (3, 0), to: "python-parser.east"),
anchor: "west",
name: "custom-parser",
align(center)[Custom python\ parser],
)
arrow("python-parser", "custom-parser", name: "arrow-python-ast")
draw.content(
"arrow-python-ast",
anchor: "south",
padding: 5pt,
)[`ast.Module`]
framed(
(rel: (-3, -2), to: "custom-parser.south"),
anchor: "east",
name: "python-resolver",
)[Python Resolver]
arrow(
"custom-parser",
((), "|-", "python-resolver.east"),
"python-resolver",
name: "arrow-python-custom-ast",
)
draw.content(
(rel: (1.5, 0), to: "arrow-python-custom-ast.end"),
padding: 5pt,
anchor: "south",
)[P-AST#footnote[#strong[P]ython *AST*]<fn-past>]
draw.content(
"python-resolver.west",
padding: 5pt,
anchor: "south-east",
)[Resolved P-AST@fn-past]
draw.circle(
(rel: (1, -2), to: "custom-parser.south-east"),
radius: .4,
name: "midas-loader",
)
arrow(
"custom-parser",
"midas-loader",
name: "arrow-load-midas",
mark: (end: (symbol: ">", fill: black), start: "o"),
)
draw.content(
"arrow-load-midas",
anchor: "west",
padding: 5pt,
)[```python midas.using("types.midas")```]
framed(
(rel: (0, -2), to: "midas-loader.south"),
name: "midas-parser",
)[Midas lexer/parser]
arrow("midas-loader", "midas-parser", name: "arrow-midas-source")
draw.content(
"arrow-midas-source",
anchor: "west",
padding: 5pt,
)[_`types.midas`_]
framed(
(rel: (-2, 0), to: "midas-parser.west"),
anchor: "east",
name: "midas-resolver",
)[Midas Resolver]
arrow("midas-parser", "midas-resolver", name: "arrow-midas-ast")
draw.content(
"arrow-midas-ast",
anchor: "south",
padding: 5pt,
)[M-AST#footnote[#strong[M]idas *AST*]<fn-mast>]
framed(
(rel: (-3, 0), to: "midas-resolver.west"),
anchor: "east",
name: "checker",
)[Checker]
arrow("midas-resolver", "checker", name: "arrow-type-ctx")
arrow(
"python-resolver",
((), "-|", "checker.north"),
"checker",
)
draw.content(
"arrow-type-ctx",
anchor: "south",
padding: 5pt,
)[Types context]
})
#show: doc => if diagram-only {
set page(width: auto, height: auto, margin: .5cm)
diagram
} else { doc }
#align(center, title())
#v(1cm)
#figure(
diagram,
caption: [Midas type-checker architecture],
)
== Components
- *Python parser*: builtin Python AST parser, extracts abstract syntax from the raw Python source (```python ast.parse(...)```)
- *Custom python parser*: converts the raw Python AST into custom, more suitable constructs, especially for type annotations
- *Python resolver*: resolves bindings and references, tracks binding scopes
- *Midas lexer/parser*: parses a Midas type definition file and extracts its AST
- *Midas resolver*: walks the AST and fills the environment with the defined types and operations
- *Checker*: evaluates expressions and checks type coherence

View File

@@ -1,16 +0,0 @@
# type: ignore
# ruff: disable[F821]
from __future__ import annotations
# A simple data-frame with different column of various simple types
# Columns can be named and/or typed
df: Frame[
verified: bool,
birth_year: int,
height: float + ( _ > 0 ) + ( _ < 250 ),
name: str,
date: datetime,
float, # unnamed
unknown: _, # untyped
_ # unnamed and untyped
]

View File

@@ -1,24 +0,0 @@
// Simple custom type derived from floats
type Latitude<float>
type Longitude<float>
// Complex custom type, containing two values accessible through properties
type GeoLocation<Latitude, Longitude> {
lat: Latitude
lon: Longitude
}
type LatitudeDiff<float>
type LongitudeDiff<float>
// Simple operation defined on our custom types
op <Latitude> - <Latitude> = <LatitudeDiff>
op <Longitude> - <Longitude> = <LongitudeDiff>
// Simple custom type with a constraint
type Age<int + (0 <= _) + (_ < 150)>
// Predefined custom constraints that can be referenced in other definitions
constraint Positive = _ >= 0
constraint StrictlyPositive = _ > 0
//constraint Even = _ % 2 == 0

View File

@@ -1,30 +0,0 @@
# type: ignore
# ruff: disable[F821]
from __future__ import annotations
# A data-frame using a custom type
df: Frame[
location: GeoLocation
]
# Properties of a type can be used on a column of that type
lat: Column[GeoLocation] = df["location"].lat
lon: Column[GeoLocation] = df["location"].lon
# Unregistered operations between types are not permitted
lat + lon # Invalid operation
# Registered operations are permitted
lat1: Latitude = lat[0]
lat2: Latitude = lat[1]
lat_diff: Difference[Latitude] = lat2 - lat1 # Valid operation
# In addition to the type, a column can have one or more constraints, either defined inline or in a separate file
df2: Frame[
age: int + (_ >= 0),
height: float + (_ >= 0),
]
df2_bis: Frame[
age: int + Positive,
height: float + Positive,
]

View File

@@ -1,73 +0,0 @@
// Simple custom type derived from float
type Custom(float)
// Simple custom types with constraints
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)
// Complex custom type, containing two values accessible through properties
type GeoLocation {
lat: Latitude
lon: Longitude
}
// Define operations on our custom type
extend GeoLocation {
// This type is compatible with the `-` operation with another GeoLocation
// i.e. you can subtract a GeoLocation from another GeoLocation, resulting
// in a Difference of GeoLocations
op __sub__(GeoLocation) -> Difference[GeoLocation]
}
// For complex generics, you need to specify how the genericity the properties
// are handled
type Difference[GeoLocation] {
lat: Difference[Latitude]
lon: Difference[Longitude]
}
// Simple operation defined on our custom types
extend Latitude {
op __sub__(Latitude) -> Difference[Latitude]
}
extend Longitude {
op __sub__(Longitude) -> Difference[Longitude]
}
// Predefined custom predicates that can be referenced in other definitions
predicate Positive(v: float) = v >= 0
predicate StrictlyPositive(v: float) = v > 0
predicate Equatorial(loc: GeoLocation) = (-10 <= loc.lat <= 10)
predicate Arctic(loc: GeoLocation) = (loc.lat >= 66)
type Person {
name: str
// Property with an inline constraint
age: int? where (0 <= _ < 150)
// Property referencing a predicate
height: float where StrictlyPositive
home: GeoLocation
}
// Custom complex type derived from another complex type, with a constraint
// on a property
// Multiple proposed syntaxes, not yet defined
// Explicit, but new keyword
type EquatorialPerson refines Person where Equatorial(_.home)
// Explicit with existing keyword, might be confusing if expectations regarding 'is'
type EquatorialPerson is Person where Equatorial(_.home)
// Consistent and Python-friendly but can be confused with structural extension
type EquatorialPerson(Person) where Equatorial(_.home)
// Allow new properties, probably not useful
type EquatorialPerson extends Person where Equatorial(_.home)

View File

@@ -1,15 +0,0 @@
# type: ignore
# ruff: disable[F821]
from __future__ import annotations
def func(
col1: Column[float + (0 <= _ <= 1)],
col2: Column[float + (0 <= _ <= 1)],
) -> Column[float + (0 <= _ <= 2)]:
result: Column[float + (0 <= _ <= 2)] = col1 + col2
return result
def func2(a: int, /, b: float, *, c: str):
pass

View File

@@ -1,33 +0,0 @@
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

View File

@@ -6,7 +6,7 @@ c = a + b # -> int
c = "invalid" # -> can't assign str to int variable
d = True
e = d + d
e = d + d # -> addition not defined between booleans
f: float = a

View File

@@ -1,6 +1,7 @@
# type: ignore
# ruff: disable [F821]
distance: Meter = cast(Meter, 123.45)
time: Second = cast(Second, 6.7)
distance = cast(Meter, 123.45)
time = cast(Second, 6.7)
speed = distance / time
print(speed)

View File

@@ -1,3 +1,5 @@
# Return types must have a LUB
# Valid
def minimum(x: int, y: int):
if x < y:
return x
@@ -5,18 +7,28 @@ def minimum(x: int, y: int):
return y
# Invalid
def func(a: int):
if a < 5:
return "Oops"
return True
a = 15
b = 72
c = minimum(a, b)
# Recursive but typable thanks to return hint
def factorial(n: int) -> int:
if n <= 1:
return 1
return n * factorial(n - 1)
category = "Category 1" if a < 10 else "Category 2"
# Branches must be of the same type
category = "Category 1" if a < 10 else "Category 2" # Valid
category = "Category 1" if a < 10 else 3 # Invalid
def foo() -> None:

View File

@@ -15,7 +15,9 @@ extend Coordinate {
type Difference[T <: float] = T
type MeterDifference = Difference[Meter]
type CompDiff[T <: float] = {
type CompDiff[T <: float] = object
extend CompDiff[T <: float] {
prop d1: Difference[T]
prop d2: Difference[T]
}

View File

@@ -1,20 +1,20 @@
# type: ignore
# ruff: disable [F821]
p1: Coordinate
p2: Coordinate
p1 = cast(Coordinate, object())
p2 = cast(Coordinate, object())
diff_x = p2.x - p1.x
diff_y = p2.y - p1.y
dist = diff_x + diff_y
p2.x += cast(Meter, 1)
p2.x += cast(Meter, 1.0)
p2.y = True # invalid, wrong type
p2.z = 3 # invalid, no property 'z' on Coordinate
p2.x.a = 3 # invalid, no properties on Meter
foo: list[float] = []
foo = cast(list[float], [])
append = foo.append
@@ -23,7 +23,7 @@ foo.append(2)
append(True) # invalid, must be float
append(2)
bar: list[list[Meter]]
bar = cast(list[list[Meter]], [])
bar.append([p2.x])

View File

@@ -1,9 +1,9 @@
# type: ignore
# ruff: disable [F821]
foo: Foo
t1: T1
t2: T2
foo = cast(Foo, object())
t1 = cast(T1, object())
t2 = cast(T2, object())
a = foo.bar(t1)
b = foo.bar(t2)
@@ -13,6 +13,6 @@ func = foo.bar
c = func(t1)
d = func(t2)
t2b: T2b
t2b = cast(T2b, object())
e = foo.bar(t2b)

View File

@@ -1,14 +0,0 @@
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): ...

14
justfile Normal file
View File

@@ -0,0 +1,14 @@
# Local Variables:
# mode: makefile
# End:
set shell := ["bash", "-uc"]
build-docs:
typst c --root . docs/manual.typ
typst c --root . docs/function_subtyping.typ
tests:
uv run -m tests
check-docstrings:
uv run scripts/docstring_checker.py

33
test.py
View File

@@ -1,33 +0,0 @@
import json
from pathlib import Path
from midas.ast.printer import MidasAstPrinter
from midas.lexer.midas import MidasLexer
from midas.lexer.token import Token
from midas.parser.midas import MidasParser
def test_midas():
# Midas type definitions
path: Path = Path("examples") / "00_syntax_prototype" / "03_custom_types_v2.midas"
definitions: str = path.read_text()
midas_lexer: MidasLexer = MidasLexer(definitions, path.name)
tokens: list[Token] = midas_lexer.process()
# print([f"{t.type.name}('{t.lexeme}')" for t in tokens])
with open("tokens.json", "w") as f:
json.dump([f"{t.type.name}('{t.lexeme}')" for t in tokens], f, indent=4)
parser = MidasParser(tokens)
parsed = parser.parse()
print(parsed)
for err in parser.errors:
print(err.get_report())
printer = MidasAstPrinter()
for stmt in parsed:
if stmt is None:
print("None")
continue
print(printer.print(stmt))
test_midas()

View File

@@ -2,8 +2,8 @@
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
@@ -54,10 +54,10 @@ extend Person {
prop name: str
// Property with an inline constraint
prop age: Optional[int where (0 <= _ < 150)]
prop age: int where (0 <= _ & _ < 150)
// Property referencing a predicate
prop height: float where StrictlyPositive
prop height: float where StrictlyPositive(_)
prop home: GeoLocation
}

View File

@@ -187,8 +187,8 @@
"column": 38
},
{
"type": "LESS_EQUAL",
"lexeme": "<=",
"type": "AND",
"lexeme": "&",
"line": 5,
"column": 39
},
@@ -196,25 +196,49 @@
"type": "WHITESPACE",
"lexeme": " ",
"line": 5,
"column": 40
},
{
"type": "UNDERSCORE",
"lexeme": "_",
"line": 5,
"column": 41
},
{
"type": "WHITESPACE",
"lexeme": " ",
"line": 5,
"column": 42
},
{
"type": "LESS_EQUAL",
"lexeme": "<=",
"line": 5,
"column": 43
},
{
"type": "WHITESPACE",
"lexeme": " ",
"line": 5,
"column": 45
},
{
"type": "NUMBER",
"lexeme": "90",
"line": 5,
"column": 42
"column": 46
},
{
"type": "RIGHT_PAREN",
"lexeme": ")",
"line": 5,
"column": 44
"column": 48
},
{
"type": "NEWLINE",
"lexeme": "\n",
"line": 5,
"column": 45
"column": 49
},
{
"type": "TYPE",
@@ -325,8 +349,8 @@
"column": 40
},
{
"type": "LESS_EQUAL",
"lexeme": "<=",
"type": "AND",
"lexeme": "&",
"line": 6,
"column": 41
},
@@ -334,25 +358,49 @@
"type": "WHITESPACE",
"lexeme": " ",
"line": 6,
"column": 42
},
{
"type": "UNDERSCORE",
"lexeme": "_",
"line": 6,
"column": 43
},
{
"type": "WHITESPACE",
"lexeme": " ",
"line": 6,
"column": 44
},
{
"type": "LESS_EQUAL",
"lexeme": "<=",
"line": 6,
"column": 45
},
{
"type": "WHITESPACE",
"lexeme": " ",
"line": 6,
"column": 47
},
{
"type": "NUMBER",
"lexeme": "180",
"line": 6,
"column": 44
"column": 48
},
{
"type": "RIGHT_PAREN",
"lexeme": ")",
"line": 6,
"column": 47
"column": 51
},
{
"type": "NEWLINE",
"lexeme": "\n",
"line": 6,
"column": 48
"column": 52
},
{
"type": "NEWLINE",
@@ -2240,22 +2288,40 @@
},
{
"type": "IDENTIFIER",
"lexeme": "Optional",
"lexeme": "int",
"line": 57,
"column": 15
},
{
"type": "LEFT_BRACKET",
"lexeme": "[",
"type": "WHITESPACE",
"lexeme": " ",
"line": 57,
"column": 23
"column": 18
},
{
"type": "IDENTIFIER",
"lexeme": "int",
"type": "WHERE",
"lexeme": "where",
"line": 57,
"column": 19
},
{
"type": "WHITESPACE",
"lexeme": " ",
"line": 57,
"column": 24
},
{
"type": "LEFT_PAREN",
"lexeme": "(",
"line": 57,
"column": 25
},
{
"type": "NUMBER",
"lexeme": "0",
"line": 57,
"column": 26
},
{
"type": "WHITESPACE",
"lexeme": " ",
@@ -2263,8 +2329,8 @@
"column": 27
},
{
"type": "WHERE",
"lexeme": "where",
"type": "LESS_EQUAL",
"lexeme": "<=",
"line": 57,
"column": 28
},
@@ -2272,17 +2338,35 @@
"type": "WHITESPACE",
"lexeme": " ",
"line": 57,
"column": 30
},
{
"type": "UNDERSCORE",
"lexeme": "_",
"line": 57,
"column": 31
},
{
"type": "WHITESPACE",
"lexeme": " ",
"line": 57,
"column": 32
},
{
"type": "AND",
"lexeme": "&",
"line": 57,
"column": 33
},
{
"type": "LEFT_PAREN",
"lexeme": "(",
"type": "WHITESPACE",
"lexeme": " ",
"line": 57,
"column": 34
},
{
"type": "NUMBER",
"lexeme": "0",
"type": "UNDERSCORE",
"lexeme": "_",
"line": 57,
"column": 35
},
@@ -2293,8 +2377,8 @@
"column": 36
},
{
"type": "LESS_EQUAL",
"lexeme": "<=",
"type": "LESS",
"lexeme": "<",
"line": 57,
"column": 37
},
@@ -2302,55 +2386,25 @@
"type": "WHITESPACE",
"lexeme": " ",
"line": 57,
"column": 39
},
{
"type": "UNDERSCORE",
"lexeme": "_",
"line": 57,
"column": 40
},
{
"type": "WHITESPACE",
"lexeme": " ",
"line": 57,
"column": 41
},
{
"type": "LESS",
"lexeme": "<",
"line": 57,
"column": 42
},
{
"type": "WHITESPACE",
"lexeme": " ",
"line": 57,
"column": 43
"column": 38
},
{
"type": "NUMBER",
"lexeme": "150",
"line": 57,
"column": 44
"column": 39
},
{
"type": "RIGHT_PAREN",
"lexeme": ")",
"line": 57,
"column": 47
},
{
"type": "RIGHT_BRACKET",
"lexeme": "]",
"line": 57,
"column": 48
"column": 42
},
{
"type": "NEWLINE",
"lexeme": "\n",
"line": 57,
"column": 49
"column": 43
},
{
"type": "NEWLINE",
@@ -2442,11 +2496,29 @@
"line": 60,
"column": 30
},
{
"type": "LEFT_PAREN",
"lexeme": "(",
"line": 60,
"column": 46
},
{
"type": "UNDERSCORE",
"lexeme": "_",
"line": 60,
"column": 47
},
{
"type": "RIGHT_PAREN",
"lexeme": ")",
"line": 60,
"column": 48
},
{
"type": "NEWLINE",
"lexeme": "\n",
"line": 60,
"column": 46
"column": 49
},
{
"type": "NEWLINE",
@@ -2544,7 +2616,7 @@
"constraint": {
"_type": "GroupingExpr",
"expr": {
"_type": "BinaryExpr",
"_type": "LogicalExpr",
"left": {
"_type": "BinaryExpr",
"left": {
@@ -2560,6 +2632,12 @@
"_type": "WildcardExpr"
}
},
"operator": "&",
"right": {
"_type": "BinaryExpr",
"left": {
"_type": "WildcardExpr"
},
"operator": "<=",
"right": {
"_type": "LiteralExpr",
@@ -2568,6 +2646,7 @@
}
}
}
}
},
{
"_type": "TypeStmt",
@@ -2582,7 +2661,7 @@
"constraint": {
"_type": "GroupingExpr",
"expr": {
"_type": "BinaryExpr",
"_type": "LogicalExpr",
"left": {
"_type": "BinaryExpr",
"left": {
@@ -2598,6 +2677,12 @@
"_type": "WildcardExpr"
}
},
"operator": "&",
"right": {
"_type": "BinaryExpr",
"left": {
"_type": "WildcardExpr"
},
"operator": "<=",
"right": {
"_type": "LiteralExpr",
@@ -2606,6 +2691,7 @@
}
}
}
}
},
{
"_type": "TypeStmt",
@@ -3013,13 +3099,6 @@
"kind": "PROPERTY",
"name": "age",
"type": {
"_type": "GenericType",
"type": {
"_type": "NamedType",
"name": "Optional"
},
"args": [
{
"_type": "ConstraintType",
"type": {
"_type": "NamedType",
@@ -3028,7 +3107,7 @@
"constraint": {
"_type": "GroupingExpr",
"expr": {
"_type": "BinaryExpr",
"_type": "LogicalExpr",
"left": {
"_type": "BinaryExpr",
"left": {
@@ -3040,6 +3119,12 @@
"_type": "WildcardExpr"
}
},
"operator": "&",
"right": {
"_type": "BinaryExpr",
"left": {
"_type": "WildcardExpr"
},
"operator": "<",
"right": {
"_type": "LiteralExpr",
@@ -3048,7 +3133,6 @@
}
}
}
]
}
},
{
@@ -3062,8 +3146,17 @@
"name": "float"
},
"constraint": {
"_type": "CallExpr",
"callee": {
"_type": "VariableExpr",
"name": "StrictlyPositive"
},
"arguments": [
{
"_type": "WildcardExpr"
}
],
"keywords": {}
}
}
},