Subtask of #56.
The @bv.expr decorator needs to handle Python control flow that can't be reified through operator overloading alone — if/else, ternary, and/or short-circuit, comparison chains (a < b < c), in / not in, match.
At decoration time: inspect.getsource(fn) → ast.parse → walk → rewrite into symbolic-IR builder calls (if_else, when, in_, ...). Then the rewritten function gets called with _SymbolicCol placeholders by the tracer (sibling subtask).
Done when:
- An
@bv.expr function with nested if/elif/else lowers correctly, verified by a unit test against the IR tree shape.
a and b and c rewrites to _and(_and(a, b), c) so Python's short-circuit semantics survive.x in {a, b, c} rewrites to _in(x, frozenset({a, b, c})) with the literal set captured.match is rejected at decoration time with a clear line-pointing error (defer to v0.2).- Unit tests under
python/tests/v0/test_expr_ast_rewriter.py.
~300 LOC Python.
Related: #67 — the AST rewriter handles if x is None: ... by lowering to IfElse(IsNull(x), then_branch, else_branch). Lands as part of this issue scope, with semantics specified in #67.
Subtask of #56.
The
@bv.exprdecorator needs to handle Python control flow that can't be reified through operator overloading alone —if/else, ternary,and/orshort-circuit, comparison chains (a < b < c),in/not in,match.At decoration time:
inspect.getsource(fn) → ast.parse → walk → rewrite into symbolic-IR builder calls (if_else, when, in_, ...). Then the rewritten function gets called with_SymbolicColplaceholders by the tracer (sibling subtask).Done when:
@bv.exprfunction with nestedif/elif/elselowers correctly, verified by a unit test against the IR tree shape.a and b and crewrites to_and(_and(a, b), c)so Python's short-circuit semantics survive.x in {a, b, c}rewrites to_in(x, frozenset({a, b, c}))with the literal set captured.matchis rejected at decoration time with a clear line-pointing error (defer to v0.2).python/tests/v0/test_expr_ast_rewriter.py.~300 LOC Python.
Related: #67 — the AST rewriter handles
if x is None: ...by lowering toIfElse(IsNull(x), then_branch, else_branch). Lands as part of this issue scope, with semantics specified in #67.