Skip to content

Add SpaceSepBy and SpacePrefixSepBy constructs + nonempty attribute #312

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
MikaelMayer merged 13 commits into from
Jan 15, 2026
Merged

Add SpaceSepBy and SpacePrefixSepBy constructs + nonempty attribute #312

MikaelMayer merged 13 commits into from
Jan 15, 2026

Conversation

@MikaelMayer
Copy link
Contributor

@MikaelMayer MikaelMayer commented Jan 9, 2026 •
edited
Loading

Add space-separated list constructs and @[nonempty] attribute to Strata DDM.

New DDM Constructs

SpaceSepBy - Space-separated lists (renders as a b c)
SpacePrefixSepBy - Space-prefix-separated lists (renders as a b c)

Both parse identically to Seq (whitespace-separated items) but differ in formatting.

@[nonempty] Attribute

Mark list arguments to require at least one element:

op indexed (s:Symbol, @[nonempty] si:SpaceSepBy Index) : SMTIdentifier =>
  "(" "_ " s " " si ")";

Parser enforces non-emptiness with error: "expected at least one element"

Usage

Works with CommaSepBy, SpaceSepBy, SpacePrefixSepBy, and Seq.

Example from SMT dialect:

op forall_smt (@[nonempty] svs: SpaceSepBy SortedVar, t:Term) : Term =>
  "(" "forall" "(" svs ")" t ")";

Tests in StrataTest/DDM/NonemptyAttribute.lean verify enforcement.

Base automatically changed from jlee/smt2 to main January 9, 2026 21:09
@MikaelMayer
Add SpaceSepBy and SpacePrefixedBy constructs to DDM
fbadfef 
- Implemented SpaceSepBy, SpaceSepByNonEmpty, SpacePrefixedBy, SpacePrefixedByNonEmpty
- Added support in AST, Parser, Format, Ion, Elab, and code generation
- Updated SMT dialect to use new constructs, removing manual list categories
- Simplified SMT dialect by eliminating IndexList, SMTSortList, TermList, etc.
- All constructs parse elements with automatic whitespace handling
- Formatting adds spaces between (SpaceSepBy) or before (SpacePrefixedBy) elements
- Fixed unused variable warnings
@MikaelMayer MikaelMayer force-pushed the feat-space-separated-lists branch from d3ab789 to fbadfef Compare January 9, 2026 21:27
aqjune-aws
aqjune-aws reviewed Jan 9, 2026
View reviewed changes
Copy link
Contributor

@aqjune-aws aqjune-aws left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Seems like a great direction to me.

What do you think about the following changes?

  • What do you think about marking non-emptiness using a new attribute, say @[nonempty]? This way, we can also decorate existing commaSepList. :)
  • I think the usefulness of SpacePrefixedBy and SpacePrefixedByNonEmptyis somewhat limited, since SpacePrefixedBy can always be replaced with " " SpaceSepBy (and similarly for SpacePrefixedByNonEmpty). What do you think about having this patch minimalistic and focusing on adding SpaceSepBy and SpaceSepByNonEmpty only? This will already be a very useful change.

@MikaelMayer
Copy link
Contributor Author

MikaelMayer commented Jan 12, 2026

  • What do you think about marking non-emptiness using a new attribute, say @[nonempty]? This way, we can also decorate existing commaSepList. :)

I love this idea. Let me try that.

  • I think the usefulness of SpacePrefixedBy and SpacePrefixedByNonEmptyis somewhat limited, since SpacePrefixedBy can always be replaced with " " SpaceSepBy (and similarly for SpacePrefixedByNonEmpty). What do you think about having this patch minimalistic and focusing on adding SpaceSepBy and SpaceSepByNonEmpty only? This will already be a very useful change.

SpacePrefixedBy is not equivalent to " " SpaceSepBy as in the case of an empty list, the former emits nothing, while the latter emits a space.

MikaelMayer and others added 2 commits January 13, 2026 14:16
@MikaelMayer
Implement @[nonempty] attribute to replace NonEmpty list variants
6072b82 
- Add @[nonempty] metadata attribute in StrataDDL
- Remove SpaceSepByNonEmpty and SpacePrefixedByNonEmpty categories
- Remove spaceSepListNonEmpty and spacePrefixedListNonEmpty AST constructors
- Update parser to check @[nonempty] metadata and use many1Parser/sepBy1Parser
- Update all supporting files (Format, Ion, ToExpr, OfAstM, Gen, Elab)
- Replace all SpaceSepByNonEmpty usage with @[nonempty] SpaceSepBy in SMT dialect
- Add comprehensive tests in StrataTest/DDM/NonemptyAttribute.lean
- Clarify that SpaceSepBy/SpacePrefixedBy/Seq parse identically, differ only in formatting
@MikaelMayer
Merge branch 'main' into feat-space-separated-lists
aa93117
@MikaelMayer MikaelMayer enabled auto-merge January 13, 2026 20:28
aqjune-aws
aqjune-aws requested changes Jan 13, 2026
View reviewed changes
Copy link
Contributor

@aqjune-aws aqjune-aws left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for your updates..! I believe the two categories spaceSepBy and spacePrefixedBy are indeed useful ones.

Two more comments:

  • Should we rename spacePrefixedBy to spaceSepPrefixedBy to represent that spacePrefixedBy also separates a list of items?
  • Let's add the two new categories as well as the nonempty attribute to docs/verso/DDMDoc.lean as well. :)

joehendrix
joehendrix reviewed Jan 13, 2026
View reviewed changes
@MikaelMayer
Refactor list constructors to use unified SepFormat and rename SpaceP…
4c8bf64 
…refixedBy

- Unify commaSepList, spaceSepList, spacePrefixedList into single .seq constructor
- Add SepFormat enum (.none, .comma, .space, .spacePrefix) to specify formatting
- Rename SpacePrefixedBy to SpacePrefixSepBy throughout codebase
- Remove unused spacePrefixedParser and spacePrefixed1Parser functions
- Update all files to use new unified structure (AST, Format, Ion, ToExpr, OfAstM, Gen)
- Update dialect translation files (Boogie, C_Simp, SMT)
- Rename ofSpacePrefixedByM to ofSpacePrefixSepByM
- Update documentation in docs/verso/DDMDoc.lean:
  - Document SpaceSepBy and SpacePrefixSepBy categories
  - Document @[nonempty] attribute for enforcing non-empty lists
  - Clarify parsing vs formatting differences for list categories
@MikaelMayer
Merge origin/main and resolve conflicts
9c28fd7 
- Resolved conflict in StrataDDL.lean by keeping both nonempty and new constructor metadata
- Fixed remaining commaSepList reference in Boogie Translate
@MikaelMayer
Fix Java TestGen to use new seq constructor with SepFormat
1a20aa8
@MikaelMayer
Fix remaining .seq references in tests
196f13a 
- Update Java TestGen to use .seq with 3 arguments (ann, sep, array)
- Update DDM Gen test expected output to show SepFormat.comma instead of commaSepList
@MikaelMayer MikaelMayer changed the title Add SpaceSepBy and SpacePrefixedBy constructs Add SpaceSepBy and SpacePrefixSepBy constructs + nonempty attribute Jan 15, 2026
@MikaelMayer
Fix Laurel translator to use unified .seq constructor
0910cd2 
- Update translateParameters to match .seq _ .comma
- Update translateStmtExpr to match .seq _ .comma
- Update translateSeqCommand to match .seq _ .none
joehendrix
joehendrix reviewed Jan 15, 2026
View reviewed changes
joehendrix
joehendrix reviewed Jan 15, 2026
View reviewed changes
joehendrix
joehendrix reviewed Jan 15, 2026
View reviewed changes
joehendrix
joehendrix reviewed Jan 15, 2026
View reviewed changes
joehendrix
joehendrix reviewed Jan 15, 2026
View reviewed changes
joehendrix
joehendrix reviewed Jan 15, 2026
View reviewed changes
@MikaelMayer
Add @[nonempty] tests for Seq category
9abd1bd 
- Add seq1 operation with @[nonempty] Seq
- Add seq0 operation without @[nonempty]
- Verify @[nonempty] enforcement works with Seq
- Verify empty Seq is allowed without @[nonempty]
@MikaelMayer
Address reviewer feedback: extract helpers and centralize string defi…
6e1caca 
…nitions

- Added SepFormat.fromIonName? with roundtrip theorem
- Extracted toAstApplyArgSeq helper in Gen.lean to eliminate duplication
- Added ofSeqSeqM wrapper in OfAstM.lean for plain Seq category
- Refactored Ion.lean ArgF.fromIon to use SepFormat.fromIonName? instead of four separate cases
- Simplified Parser.lean checkLeftRec with consolidated if statement
- Extracted getOfIdentArgSeq helper in Gen.lean where clause
@MikaelMayer
Inline wrapper functions and call ofSeqM directly with SepFormat
cfc54c6 
- Removed ofCommaSepByM, ofSpaceSepByM, ofSpacePrefixSepByM, ofSeqSeqM wrappers
- Updated getOfIdentArgSeq to pass SepFormat directly to ofSeqM
- Simplifies code by eliminating unnecessary one-line wrapper functions
joehendrix
joehendrix reviewed Jan 15, 2026
View reviewed changes
@MikaelMayer
Unify sequence info structures and eliminate duplication
ae6349a 
- Replaced CommaSepInfo, SpaceSepInfo, SpacePrefixedInfo with single SeqInfo taking SepFormat parameter
- Removed duplicate Info constructors (ofCommaSepInfo, ofSpaceSepInfo, ofSpacePrefixedInfo)
- Updated asCommaSepInfo functions to check sep field
- Extracted elabSeqWith helper in Core.lean to consolidate four similar elaboration cases
- Reduces code duplication by ~50 lines across Tree.lean and Core.lean
joehendrix
joehendrix reviewed Jan 15, 2026
View reviewed changes
aqjune-aws
aqjune-aws approved these changes Jan 15, 2026
View reviewed changes
Copy link
Contributor

@aqjune-aws aqjune-aws left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks :)

@MikaelMayer MikaelMayer added this pull request to the merge queue Jan 15, 2026
Merged via the queue into main with commit cb0cb83 Jan 15, 2026
14 checks passed
@MikaelMayer MikaelMayer deleted the feat-space-separated-lists branch January 15, 2026 15:58
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@joehendrix joehendrix joehendrix approved these changes

@aqjune-aws aqjune-aws aqjune-aws approved these changes

@andrewmwells-amazon andrewmwells-amazon Awaiting requested review from andrewmwells-amazon

@atomb atomb Awaiting requested review from atomb

@shigoel shigoel Awaiting requested review from shigoel

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@MikaelMayer @joehendrix @aqjune-aws