Skip to content

Extend pySpecs translator to handle all service specification constructs#537

Merged
shigoel merged 1 commit intomainfrom
jhx/pyspec_re
Mar 11, 2026
Merged

Extend pySpecs translator to handle all service specification constructs#537
shigoel merged 1 commit intomainfrom
jhx/pyspec_re

Conversation

@joehendrix
Copy link
Contributor

@joehendrix joehendrix commented Mar 10, 2026

Summary

Extend the Strata pySpecs Python-to-spec translator to handle the full
range of assertion patterns found across service specification files.
Before this change the translator emitted warnings on many common
patterns; after, it handles all constructs without warnings.

Builds on the robustness and API improvements from #512.

Details

  • F-string messages. Assertion messages that use Python f-strings
    are now preserved semantically (distinguishing literal text from
    interpolated expressions) rather than being flattened to a single
    string.
  • For-loop quantifiers. for item in kwargs["field"] loops are
    translated to forallList quantifiers. The element type is inferred
    from typing.List or typing.Sequence annotations in the
    corresponding TypedDict. for k, v in dict.items() tuple unpacking
    is handled similarly via forallDict, with key/value types inferred
    from Dict or Mapping annotations.
  • Conditional implication. When assertions appear inside an if
    block (e.g. if "Items" in kwargs:), the condition becomes an
    antecedent: implies(condition, assertion). Else-branch assertions
    receive the negated condition.
  • __init__ as class fields. Rather than treating __init__ as a
    regular method, the translator now extracts
    self.field = self._ClassName() assignments as typed class fields
    with an optional constant value. Unhandled __init__ patterns
    emit warnings.
  • Type-checked numeric comparisons. Comparison assertions
    (>=, <=) now use type inference to choose between integer and
    floating-point operators. When a float-typed field is compared
    against an integer literal (e.g. SampleSize >= 0), the bound is
    promoted to float automatically. Negative integer bounds (>= -1)
    are also supported.
  • Negative-integer DDM encoding. Fixed the negSucc round-trip in
    the DDM serialization layer so that -1 renders as "-1" rather
    than "-0".
  • DDM operator precedences. Subscript, comparison, and implication
    operators have explicit precedences so the pretty-printer no longer
    emits unnecessary parentheses.
  • Test coverage. Positive tests cover f-strings, for-loops, dict
    iteration, conditionals, __init__ fields, float/int comparisons,
    and negative bounds. A separate negative-test file (warnings.py)
    verifies that unsupported patterns produce the expected warnings.
    Test assertions now throw descriptive errors instead of panicking.

By submitting this pull request, I confirm that you can use, modify,
copy, and redistribute this contribution, under the terms of your choice.

@joehendrix joehendrix requested a review from a team March 10, 2026 06:00
@joehendrix joehendrix changed the title Extend pySpecs translator to handle all botomoog-python constructs Extend pySpecs translator to handle all service specification constructs Mar 10, 2026
@joehendrix joehendrix force-pushed the jhx/pyspec_re branch 2 times, most recently from 6a4f36f to 35aea85 Compare March 10, 2026 06:14
@shigoel shigoel enabled auto-merge March 10, 2026 22:41
@shigoel shigoel requested review from aqjune-aws and shigoel March 10, 2026 22:41
shigoel
shigoel previously approved these changes Mar 10, 2026
aqjune-aws
aqjune-aws previously approved these changes Mar 10, 2026
@joehendrix joehendrix dismissed stale reviews from aqjune-aws and shigoel via 8dfe875 March 10, 2026 23:03
- F-string assertion messages preserved as MessagePart arrays
- For-loop quantifiers: forallList (List/Sequence) and forallDict (Dict/Mapping)
- Conditional implication via assumeCondition for if/else blocks
- __init__ class field extraction with constValue support
- Type-checked float/int comparisons with fallback for mixed types
- Negative integer bounds via extractIntBound (ConNeg, UnaryOp USub)
- negInt DDM encoding with explicit 0 edge case handling
- DDM operator precedences: subscript@50, comparison@15, implication@10
- Warn on unrecognized if-conditions, for/else, type_comment, type_params
- Extract resolveBaseClasses and makeComparison helpers to reduce duplication
- Remove dead Pred and Iterable types
- Add positive tests (float, negative, __init__, else-branch, negative float)
- Add negative warning tests (unsupported assert, bad init, for/else, skipped stmts)
- Fix missing s! interpolation in 3 error messages
- DDM Int round-trip tests via #guard

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@joehendrix
Copy link
Contributor Author

Review fixes (force-pushed)

Addressed all 13 issues from code review, rebased on latest main, and squashed into a single commit.

Correctness

  • Fix missing s! string interpolation in 3 "{dialect} already loaded" error messages
  • Emit warning when transCondition drops unrecognized if-conditions (previously silent)
  • Fix negInt 0 DDM edge case: renamed negSuccInt to negInt, explicit 0 handling, added round-trip #guard tests

Safety

  • Replace assert! with specWarning in For handler (type_comment, for/else) and class-body FunctionDef (type_comment, type_params)

Structure

  • Remove dead Pred type (with stale FIXME) and Iterable type
  • Extract makeComparison helper to deduplicate GtE/LtE comparison arms (~30 lines removed)
  • Extract resolveBaseClasses helper to deduplicate base-class resolution in pySpecClassBody and translate

Test Coverage

  • Add else-branch test exercising the not() DDM path end-to-end
  • Add for_else_loop warning test using previously unused LoopRequest TypedDict
  • Add negative float bound test (>= -0.5) exercising extractFloatBound with UnaryOp(USub, ConFloat)
  • Warning test now verifies signatures are produced (not just warnings emitted)

Style

  • Wrap 2 long lines in DDM.lean to stay under 100 characters

@shigoel shigoel added this pull request to the merge queue Mar 11, 2026
Merged via the queue into main with commit 41b3e43 Mar 11, 2026
15 checks passed
@shigoel shigoel deleted the jhx/pyspec_re branch March 11, 2026 01:00
github-merge-queue bot pushed a commit that referenced this pull request Mar 11, 2026
## Summary

- Remove `review_notes.md` that was accidentally committed as part of PR
#537 review

## Test plan

- No functional changes; only deletes a non-code file

By submitting this pull request, I confirm that you can use, modify,
copy, and redistribute this contribution, under the terms of your
choice.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants