(Low Priority) Basic type and size checks in the grammar #6

Activity

1. Trosper3

   changed the title [-]Basic type and size checks in the grammar (Nice to Have)[/-] [+](Low Priority) Basic type and size checks in the grammar[/+] on Oct 1, 2026
2. Trosper3 commented on Oct 1, 2026

   

   Trosper3

   on Oct 1, 2026

   ContributorAuthor

   More actions

   Design: type and size checks

   A proposal for this issue, for feedback before any code is written. It builds on #15 (is int / is set / is list now check their type) and #17 (is multiset).

   What exists today

   Check	Written as
   a single integer	K is int
   every element is an integer	S subset int
   a set / list / multiset	S is set, S is list, S is multiset (#17)

   Proposal

   1. More built-in value types

   These work like int today: x is T checks one value, and S subset T checks every element.

   Type	Accepts	Rejects
   number	3, -2, 1.5, 0.25	1,5, 1e3, abc
   bool	True, False, T, F, in any letter case	yes, 1
   identifier	a letter or _, then letters, digits or _: x1, node_3	3x, New York
   string	any single value	a set or list

   string matches how Redux already writes DFA and NFA grammars (S is string, I is string). Today those parts are parsed but never checked (#14).

   number uses a fixed format (digits, an optional sign and an optional decimal point) that doesn't change with the computer's language settings, so 1,5 is never read as one and a half.

   2. Non-empty and size

   {N | N is multiset, N subset int, N is nonempty}
   {(X,Y,Z,M) | X is set, Y is set, Z is set, size M >= 1}
   {(S,K) | S is set, K is int, size S <= K}
   

   • N is nonempty: at least one element. This is the common case, so it gets its own keyword.
   • size N <op> n, with <op> one of =, <, <=, >, >=, and n either a number or another integer field of the same instance (as in size S <= K).
   • Failure messages follow the existing style: Constraint size S <= K failed: S has 5 elements, K is 3.

   Grammar changes

   • number, bool, identifier and string join int as built-in sets (lexer).
   • nonempty joins set, list and multiset as is keywords (lexer).
   • A new constraint form 'size' TERM COMPARE (TERM | number) (parser).
   • Lexer and parser regenerated with ANTLR 4.13.2, as in feat(collections): add multisets #17.

   Redux impact

   Nothing breaks. Redux can then:

   • add N is nonempty to Partition and Subset Sum, replacing the checks hand-added in Backend bug fixes: clean 400s for bad input, solver fixes, parser hardening Redux#624;
   • describe certificate sizes inside the grammar where both sizes are in the same instance.

   Comparing a certificate's size with the instance's K still happens in Redux, because they're parsed separately.

   Open questions

   1. Keywords: nonempty and size? Or the set-builder style |S| <= K? That reads like the math, but | already separates the format from the constraints, which could be confusing.
   2. bool: accept any letter case, or only True / False / T / F exactly?
   3. Is identifier needed, or is string enough for Redux?
   4. Should number accept exponents such as 1e3?
3. Trosper3

   added this to the 0.3.0 milestone on Oct 13, 2026
4. Trosper3 commented on Oct 13, 2026

   

   Trosper3

   on Oct 13, 2026

   ContributorAuthor

   More actions

   Planning note: #10 (is int / is set), #22 (is string) and #23 (number) cover most of this in 0.2.0. Whatever is left (size checks) is planned for 0.3.0 alongside #14's definition checking.
5. Trosper3

   added a parent issue on Oct 15, 2026

   • Problems as Input, Output, Certificate and Definition: SPADE structures and verifies them #32