tests: add predicates and constraints test

This commit is contained in:
2026-06-19 22:09:16 +02:00
parent 1f0bcab2ca
commit 0aba134290
4 changed files with 359 additions and 4 deletions

View File

@@ -39,9 +39,6 @@ class Generator(p.Stmt.Visitor[ast.stmt], p.Expr.Visitor[ast.expr]):
def __init__(self, workdir: Path, types: TypesRegistry) -> None:
self.workdir: Path = workdir.resolve()
self.build_dir: Path = self.workdir / "build" / "midas"
if self.build_dir.exists():
shutil.rmtree(self.build_dir)
self.build_dir.mkdir(parents=True, exist_ok=True)
self.rel_src_path: Path = Path()
self._typed_ast: TypedAST = TypedAST(
@@ -56,7 +53,7 @@ class Generator(p.Stmt.Visitor[ast.stmt], p.Expr.Visitor[ast.expr]):
self._constraints: list[tuple[m.Expr, ast.expr]] = []
def generate_ast(self, typed_ast: TypedAST, src_path: Path) -> ast.AST:
self.rel_src_path = src_path.relative_to(self.workdir)
self.rel_src_path = src_path.resolve().relative_to(self.workdir)
self._typed_ast = typed_ast
body: list[ast.stmt] = self._visit_body(typed_ast.stmts)
predicates: list[ast.stmt] = self._constraint_generator.get_definitions()
@@ -70,6 +67,9 @@ class Generator(p.Stmt.Visitor[ast.stmt], p.Expr.Visitor[ast.expr]):
module: ast.AST = self.generate_ast(typed_ast, src_path)
compiled: str = ast.unparse(module)
if out_path is None:
if self.build_dir.exists():
shutil.rmtree(self.build_dir)
self.build_dir.mkdir(parents=True, exist_ok=True)
out_path = (self.build_dir / self.rel_src_path).resolve()
try:
_ = out_path.relative_to(self.build_dir)

View File

@@ -0,0 +1,14 @@
// Inline
type T1 = float where _ > 0
// Named
predicate is_positive(v: float) = v > 0
type T2 = float where is_positive(_)
// Curried
predicate in_range(mn: float, mx: float)(v: float) = v >= mn & v < mx
type T3 = float where in_range(100, 200)(_)
// Alias
predicate minor = in_range(0, 18)
type T4 = float where minor(_)

View File

@@ -0,0 +1,8 @@
from midas import T1, T2, T3, T4, cast
t: float = 12.5
t1: T1 = cast(T1, t)
t2: T2 = cast(T2, t)
t3: T3 = cast(T3, t)
t4: T4 = cast(T4, t)

View File

@@ -0,0 +1,333 @@
Module(
body=[
FunctionDef(
name='__midas_p0__',
args=arguments(
posonlyargs=[],
args=[
arg(
arg='_',
annotation=Constant(value='Any'))],
kwonlyargs=[],
kw_defaults=[],
defaults=[]),
body=[
Return(
value=Compare(
left=Name(id='_'),
ops=[
Gt()],
comparators=[
Constant(value=0.0)]))],
decorator_list=[],
returns=Constant(value='bool')),
FunctionDef(
name='__midas_is_positive__',
args=arguments(
posonlyargs=[],
args=[
arg(
arg='v',
annotation=Constant(value='float'))],
kwonlyargs=[],
kw_defaults=[],
defaults=[]),
body=[
Return(
value=Compare(
left=Name(id='v'),
ops=[
Gt()],
comparators=[
Constant(value=0.0)]))],
decorator_list=[],
returns=Constant(value='bool')),
FunctionDef(
name='__midas_p1__',
args=arguments(
posonlyargs=[],
args=[
arg(
arg='_',
annotation=Constant(value='Any'))],
kwonlyargs=[],
kw_defaults=[],
defaults=[]),
body=[
Return(
value=Call(
func=Name(id='__midas_is_positive__'),
args=[
Name(id='_')],
keywords=[]))],
decorator_list=[],
returns=Constant(value='bool')),
FunctionDef(
name='__midas_in_range__',
args=arguments(
posonlyargs=[],
args=[
arg(
arg='mn',
annotation=Constant(value='float')),
arg(
arg='mx',
annotation=Constant(value='float'))],
kwonlyargs=[],
kw_defaults=[],
defaults=[]),
body=[
FunctionDef(
name='inner0',
args=arguments(
posonlyargs=[],
args=[
arg(
arg='v',
annotation=Constant(value='float'))],
kwonlyargs=[],
kw_defaults=[],
defaults=[]),
body=[
Return(
value=BoolOp(
op=And(),
values=[
Compare(
left=Name(id='v'),
ops=[
GtE()],
comparators=[
Name(id='mn')]),
Compare(
left=Name(id='v'),
ops=[
Lt()],
comparators=[
Name(id='mx')])]))],
decorator_list=[],
returns=Constant(value='bool')),
Return(
value=Name(id='inner0'))],
decorator_list=[],
returns=Constant(value='Callable[[float], bool]')),
FunctionDef(
name='__midas_p2__',
args=arguments(
posonlyargs=[],
args=[
arg(
arg='_',
annotation=Constant(value='Any'))],
kwonlyargs=[],
kw_defaults=[],
defaults=[]),
body=[
Return(
value=Call(
func=Call(
func=Name(id='__midas_in_range__'),
args=[
Constant(value=100.0),
Constant(value=200.0)],
keywords=[]),
args=[
Name(id='_')],
keywords=[]))],
decorator_list=[],
returns=Constant(value='bool')),
Assign(
targets=[
Name(id='__midas_minor__')],
value=Call(
func=Name(id='__midas_in_range__'),
args=[
Constant(value=0.0),
Constant(value=18.0)],
keywords=[])),
FunctionDef(
name='__midas_p3__',
args=arguments(
posonlyargs=[],
args=[
arg(
arg='_',
annotation=Constant(value='Any'))],
kwonlyargs=[],
kw_defaults=[],
defaults=[]),
body=[
Return(
value=Call(
func=Name(id='__midas_minor__'),
args=[
Name(id='_')],
keywords=[]))],
decorator_list=[],
returns=Constant(value='bool')),
ImportFrom(
module='midas',
names=[
alias(name='T1'),
alias(name='T2'),
alias(name='T3'),
alias(name='T4'),
alias(name='cast')],
level=0),
Assign(
targets=[
Name(id='t')],
value=Constant(value=12.5)),
Assign(
targets=[
Name(id='__midas_a0__')],
value=Name(id='t')),
Assert(
test=Call(
func=Name(id='isinstance'),
args=[
Name(id='__midas_a0__'),
Name(id='float')],
keywords=[]),
msg=JoinedStr(
values=[
Constant(value='02_constraints.py:L5:10: CastError: Cannot cast '),
FormattedValue(
value=Attribute(
value=Call(
func=Name(id='type'),
args=[
Name(id='__midas_a0__')],
keywords=[]),
attr='__name__'),
conversion=-1),
Constant(value=' to float')])),
Assert(
test=Call(
func=Name(id='__midas_p0__'),
args=[
Name(id='__midas_a0__')],
keywords=[]),
msg=Constant(value="02_constraints.py:L5:10: ConstraintError: Value does not fit constraint '_ > 0.0'")),
Assign(
targets=[
Name(id='t1')],
value=Name(id='__midas_a0__')),
Delete(
targets=[
Name(id='__midas_a0__')]),
Assign(
targets=[
Name(id='__midas_a1__')],
value=Name(id='t')),
Assert(
test=Call(
func=Name(id='isinstance'),
args=[
Name(id='__midas_a1__'),
Name(id='float')],
keywords=[]),
msg=JoinedStr(
values=[
Constant(value='02_constraints.py:L6:10: CastError: Cannot cast '),
FormattedValue(
value=Attribute(
value=Call(
func=Name(id='type'),
args=[
Name(id='__midas_a1__')],
keywords=[]),
attr='__name__'),
conversion=-1),
Constant(value=' to float')])),
Assert(
test=Call(
func=Name(id='__midas_p1__'),
args=[
Name(id='__midas_a1__')],
keywords=[]),
msg=Constant(value="02_constraints.py:L6:10: ConstraintError: Value does not fit constraint 'is_positive(_)'")),
Assign(
targets=[
Name(id='t2')],
value=Name(id='__midas_a1__')),
Delete(
targets=[
Name(id='__midas_a1__')]),
Assign(
targets=[
Name(id='__midas_a2__')],
value=Name(id='t')),
Assert(
test=Call(
func=Name(id='isinstance'),
args=[
Name(id='__midas_a2__'),
Name(id='float')],
keywords=[]),
msg=JoinedStr(
values=[
Constant(value='02_constraints.py:L7:10: CastError: Cannot cast '),
FormattedValue(
value=Attribute(
value=Call(
func=Name(id='type'),
args=[
Name(id='__midas_a2__')],
keywords=[]),
attr='__name__'),
conversion=-1),
Constant(value=' to float')])),
Assert(
test=Call(
func=Name(id='__midas_p2__'),
args=[
Name(id='__midas_a2__')],
keywords=[]),
msg=Constant(value="02_constraints.py:L7:10: ConstraintError: Value does not fit constraint 'in_range(100.0, 200.0)(_)'")),
Assign(
targets=[
Name(id='t3')],
value=Name(id='__midas_a2__')),
Delete(
targets=[
Name(id='__midas_a2__')]),
Assign(
targets=[
Name(id='__midas_a3__')],
value=Name(id='t')),
Assert(
test=Call(
func=Name(id='isinstance'),
args=[
Name(id='__midas_a3__'),
Name(id='float')],
keywords=[]),
msg=JoinedStr(
values=[
Constant(value='02_constraints.py:L8:10: CastError: Cannot cast '),
FormattedValue(
value=Attribute(
value=Call(
func=Name(id='type'),
args=[
Name(id='__midas_a3__')],
keywords=[]),
attr='__name__'),
conversion=-1),
Constant(value=' to float')])),
Assert(
test=Call(
func=Name(id='__midas_p3__'),
args=[
Name(id='__midas_a3__')],
keywords=[]),
msg=Constant(value="02_constraints.py:L8:10: ConstraintError: Value does not fit constraint 'minor(_)'")),
Assign(
targets=[
Name(id='t4')],
value=Name(id='__midas_a3__')),
Delete(
targets=[
Name(id='__midas_a3__')])],
type_ignores=[])