Core.formatProgram to produce round-trip-parseable output for all constructs by MikaelMayer · Pull Request #1165 · strata-org/Strata

MikaelMayer · 2026-05-14T17:05:09Z

Fixes #1158

Summary

Fixes several issues with Core.formatProgram that prevented round-trip parsing:

inline function formatted without space — The inline grammar op now includes a trailing space, preventing inlinefunction concatenation. The formatter also now emits the inline attribute when present on functions.
Quantifier variable names — The formatter now uses the prettyName field from LExpr.quant instead of generating __qN names, preserving the original variable names through formatting.
Overflow predicates — Added grammar entries, formatter handling, parser entries, and Factory operations for all bitvector overflow predicates (SNegOverflow, UNegOverflow, SAddOverflow, SSubOverflow, SMulOverflow, SDivOverflow, UAddOverflow, USubOverflow, UMulOverflow). SNegOverflow and UNegOverflow use distinct grammar entries (Bv.SNegOverflow / Bv.UNegOverflow) to preserve their different semantics through roundtrip. The translate direction correctly dispatches overflow ops by type parameter (bv1/bv8/bv16/bv32/bv64).
Array assignment (lhsArray) — Implemented m[k] := v translation in both directions: the parser decomposes nested LHS into base identifier + indices and builds map_update expressions; the formatter detects the map_update(var, idx, val) pattern and produces lhsArray syntax.
Sequence.empty — Added grammar entry with explicit type annotation syntax (Sequence.empty<int>()), plus translate and format handling, resolving the 0-ary polymorphic function limitation for this operation.
Datatype roundtrip — Verified that datatype formatting roundtrips correctly (the extra-parentheses issue noted earlier is resolved).
Roundtrip test infrastructure — Added RoundtripTest.lean that verifies parse → format → re-parse → re-format produces stable output for types, functions, procedures, inline functions, parameterized type arguments, datatypes, array assignments, and Sequence.empty.

Testing

All existing tests pass (with expected output updates for the formatting improvements)
New roundtrip tests verify types, functions, procedures, inline functions, parameterized type arguments, datatypes, lhsArray, and Sequence.empty

Remaining limitations

Bitvector operations with widths beyond 1/8/16/32/64 still fall back to generic call (requires grammar-level type entries per width)

- Fix inline function formatting: add trailing space to 'inline' op in Grammar.lean to prevent 'inlinefunction' concatenation - Emit inline attribute when formatting functions that have it - Use prettyName for quantifier variables instead of generated __qN names - Add overflow predicate support: grammar entries, formatter handling, parser entries, and Factory operations for Bv32 overflow predicates - Add roundtrip test infrastructure for Core programs - Update test expected outputs to reflect prettyName fix

Resolve conflicts between the formatProgram roundtrip fix and main's refactoring (FormatCore extraction, recFnDeclToCST, procedure syntax). - Apply prettyName and inline? fixes to FormatCore.lean - Use proper overflow CST constructors instead of approximations - Remove duplicate overflow declarations in Factory.lean - Update test expected outputs for combined changes - Fix RoundtripTest to handle new 'program Core;' header

MikaelMayer

🔍 Good PR — the prettyName preservation, inline function formatting, and overflow predicate grammar entries are well-designed. The roundtrip test infrastructure is a valuable addition.

One substantive issue: the overflow ops in Translate.lean ignore the type parameter and hardcode bv32, which breaks roundtrip for non-32-bit overflow predicates.

Minor: the docstring on mkQuantVarName (line 86 of FormatCore.lean) says "In the future, we will store existing variable names in an extra field" — but this PR implements exactly that. Worth updating to reflect the current state.

… grammar entry - Overflow ops in translateFn now match on type parameter (.some .bv1, .some .bv8, etc.) instead of using wildcard _, consistent with all other type-parameterized BV ops. - Added bv_sdiv_overflow grammar entry so SDivOverflow formats as Bv.SDivOverflow(x, y) instead of the incorrect x <= y. - Added overflow ops to the polymorphic binary dispatch in translateExpr. - Updated editor syntax files with Bv.SDivOverflow.

MikaelMayer · 2026-05-14T21:32:47Z

Do all the follow-ups and update the PR description when done

… roundtrip - Implement lhsArray (m[k] := v) in Translate.lean by decomposing nested LHS into base identifier + indices and building map_update expressions - Add decomposeMapUpdate in FormatCore.lean to detect map_update patterns and format them back as lhsArray syntax for proper roundtrip - Add seq_empty grammar entry with explicit type annotation syntax (Sequence.empty<T>()) and corresponding translate/format handling - Add full roundtrip test for datatypes (parentheses issue is resolved) - Add roundtrip tests for lhsArray and Sequence.empty - Regenerate editor syntax files with Sequence.empty - Update AdvancedMaps expected output to match new lhsArray formatting

MikaelMayer · 2026-05-14T22:01:20Z

🤖 Done in 4683739. Addressed the follow-ups:

lhsArray (m[k] := v) — Implemented in Translate.lean (decomposes nested LHS into base + indices, builds map_update) and FormatCore.lean (detects map_update pattern to produce lhsArray syntax for roundtrip).
Sequence.empty — Added grammar entry with explicit type annotation syntax (Sequence.empty<int>()), plus translate and format handling.
Datatype roundtrip — The extra parentheses issue is already resolved; added a full roundtrip test confirming it works.
Bitvector widths beyond 1/8/16/32/64 — This remains a known limitation requiring grammar-level changes (new type entries per width). Not addressed in this PR.

All 598 test jobs pass.

…tprogram-does-not-produce-roun

MikaelMayer

🔍 Well-structured PR that addresses multiple formatting roundtrip issues. The roundtrip test infrastructure is a good addition. The quantifier pretty-name preservation, inline attribute emission, overflow predicate grammar entries, and lhsArray detection are all solid improvements.

A few items to address:

Dead code added in Factory.lean (bv32NegOverflowFunc/bv32NegOverflowOp) — the macro already generates these.
UNegOverflow is conflated with SNegOverflow in the formatter/parser roundtrip (they use different semantics: BitVec.negOverflow vs BitVec.unegOverflow).
decomposeMapUpdate docstring says "nested" but only handles single-level.

MikaelMayer · 2026-05-15T02:28:12Z

 def bv64Extract_15_0_Op  := bv64Extract_15_0_Func.opExpr
 def bv64Extract_7_0_Op   := bv64Extract_7_0_Func.opExpr

+def bv32NegOverflowFunc : WFLFunc CoreLParams :=


🔍 bv32NegOverflowFunc and bv32NegOverflowOp are dead code — they are never referenced anywhere. The macro DefBVOpFuncExprs [1, 8, 16, 32, 64] already generates bv32SNegOverflowOp (from the "SNegOverflow" spec in BVOpSpecs). These manual definitions should be removed.

🤖 Removed bv32NegOverflowFunc and bv32NegOverflowOp in c3b37cd.

MikaelMayer · 2026-05-15T02:28:12Z

-  -- Overflow predicates: approximated as Bool.Not for CST printing
-  | .bv ⟨_, .SNegOverflow⟩ | .bv ⟨_, .UNegOverflow⟩ => pure (.not default arg)
+  -- Overflow predicates
+  | .bv ⟨w, .SNegOverflow⟩ | .bv ⟨w, .UNegOverflow⟩ =>


🔍 SNegOverflow and UNegOverflow are mapped to the same grammar entry (bv_neg_overflow), but the parser always maps bv_neg_overflow back to Core.bv{N}SNegOverflowOp. Since these use different evaluation functions (BitVec.negOverflow vs BitVec.unegOverflow), a UNegOverflow expression loses its semantics after a roundtrip. Consider adding a separate bv_uneg_overflow grammar entry (e.g., "Bv.UNegOverflow") to preserve the distinction.

🤖 Added separate bv_uneg_overflow grammar entry (Bv.UNegOverflow) and updated FormatCore to use it for UNegOverflow, while bv_neg_overflow now formats as Bv.SNegOverflow. Parser mappings added in Translate.lean. c3b37cd

MikaelMayer · 2026-05-15T02:28:12Z

  modify (·.pushBoundVar name.val)
  pure (.funcDecl_statement default name typeArgs b r preconds bodyExpr inline?)

+/-- Decompose nested `map_update(base, idx, val)` where `base` is (or starts


🔍 The docstring says "Decompose nested map_update" but the implementation only handles single-level (base must be an fvar). For nested m[k1][k2] := v, this returns some ([k1], update(select(m, k1), k2, v)) which formats as m[k1] := (m[k1])[k2:=v] rather than m[k1][k2] := v. Consider updating the docstring to say "single-level" to match the actual behavior, or implementing the recursive case by checking if val is itself a map_update whose base is a select on the same variable.

🤖 Updated docstring to say "single-level" in c3b37cd.

…de, fix docstring - Add separate bv_uneg_overflow grammar entry so UNegOverflow roundtrips correctly (previously both mapped to bv_neg_overflow losing semantics) - Remove dead bv32NegOverflowFunc/bv32NegOverflowOp definitions - Fix decomposeMapUpdate docstring to say single-level instead of nested - Regenerate editor syntax files

github-actions Bot added Core Git conflicts labels May 14, 2026

github-actions Bot removed the Git conflicts label May 14, 2026

MikaelMayer added 2 commits May 14, 2026 18:20

chore: regenerate editor syntax files with Bv overflow functions

eb37eca

fix: update expected transform output to match preserved variable names

2f3045a

MikaelMayer commented May 14, 2026

View reviewed changes

Comment thread Strata/Languages/Core/DDMTransform/Translate.lean Outdated

Comment thread Strata/Languages/Core/DDMTransform/FormatCore.lean Outdated

MikaelMayer added 2 commits May 14, 2026 19:42

chore: regenerate emacs syntax file to match GenSyntax output

e74350b

MikaelMayer changed the title ~~Core.formatProgram does not produce round-trip-parseable output for all constructs~~ Core.formatProgram to produce round-trip-parseable output for all constructs May 14, 2026

Merge remote-tracking branch 'origin/main' into issue-1158-core-forma…

0af4a85

…tprogram-does-not-produce-roun

MikaelMayer commented May 15, 2026

View reviewed changes

MikaelMayer added 2 commits May 15, 2026 02:41

ci: retry after transient infrastructure failures

28aa718

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Core.formatProgram to produce round-trip-parseable output for all constructs#1165

Core.formatProgram to produce round-trip-parseable output for all constructs#1165
MikaelMayer wants to merge 10 commits into
mainfrom
issue-1158-core-formatprogram-does-not-produce-roun

MikaelMayer commented May 14, 2026 •

edited

Loading

Uh oh!

MikaelMayer left a comment

Uh oh!

Uh oh!

Uh oh!

MikaelMayer commented May 14, 2026

Uh oh!

MikaelMayer commented May 14, 2026

Uh oh!

MikaelMayer left a comment

Uh oh!

MikaelMayer May 15, 2026

Uh oh!

MikaelMayer May 15, 2026

Uh oh!

MikaelMayer May 15, 2026

Uh oh!

MikaelMayer May 15, 2026

Uh oh!

MikaelMayer May 15, 2026

Uh oh!

MikaelMayer May 15, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

MikaelMayer commented May 14, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Testing

Remaining limitations

Uh oh!

MikaelMayer left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

MikaelMayer commented May 14, 2026

Uh oh!

MikaelMayer commented May 14, 2026

Uh oh!

MikaelMayer left a comment

Choose a reason for hiding this comment

Uh oh!

MikaelMayer May 15, 2026

Choose a reason for hiding this comment

Uh oh!

MikaelMayer May 15, 2026

Choose a reason for hiding this comment

Uh oh!

MikaelMayer May 15, 2026

Choose a reason for hiding this comment

Uh oh!

MikaelMayer May 15, 2026

Choose a reason for hiding this comment

Uh oh!

MikaelMayer May 15, 2026

Choose a reason for hiding this comment

Uh oh!

MikaelMayer May 15, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

MikaelMayer commented May 14, 2026 •

edited

Loading