@@ -11,26 +11,43 @@ import {
1111 * Extracted from logic.ts for better code organization.
1212 */
1313
14+ /**
15+ * Result of extracting a finite domain from an Element expression.
16+ * - `status: 'success'` - Domain was successfully extracted
17+ * - `status: 'non-enumerable'` - Domain exists but cannot be enumerated (e.g., infinite set, unknown symbol)
18+ * - `status: 'error'` - Invalid Element expression (missing variable, malformed domain)
19+ */
20+ export type ExtractDomainResult =
21+ | { status : 'success' ; variable : string ; values : BoxedExpression [ ] }
22+ | { status : 'non-enumerable' ; variable : string ; domain : BoxedExpression ; reason : string }
23+ | { status : 'error' ; reason : string } ;
24+
1425/**
1526 * Extract the finite domain from a quantifier's condition.
1627 * Supports:
1728 * - ["Element", "x", ["Set", 1, 2, 3]] → [1, 2, 3]
1829 * - ["Element", "x", ["Range", 1, 5]] → [1, 2, 3, 4, 5]
1930 * - ["Element", "x", ["Interval", 1, 5]] → [1, 2, 3, 4, 5] (integers only)
20- * Returns null if the domain is not finite or not recognized .
31+ * Returns detailed result indicating success, non-enumerable domain, or error .
2132 */
22- export function extractFiniteDomain (
33+ export function extractFiniteDomainWithReason (
2334 condition : BoxedExpression ,
2435 ce : ComputeEngine
25- ) : { variable : string ; values : BoxedExpression [ ] } | null {
36+ ) : ExtractDomainResult {
2637 // Check for ["Element", var, set] pattern
27- if ( condition . operator !== 'Element' ) return null ;
38+ if ( condition . operator !== 'Element' ) {
39+ return { status : 'error' , reason : 'expected-element-expression' } ;
40+ }
2841
2942 const variable = condition . op1 ?. symbol ;
30- if ( ! variable ) return null ;
43+ if ( ! variable ) {
44+ return { status : 'error' , reason : 'expected-index-variable' } ;
45+ }
3146
3247 const domain = condition . op2 ;
33- if ( ! domain ) return null ;
48+ if ( ! domain ) {
49+ return { status : 'error' , reason : 'expected-domain' } ;
50+ }
3451
3552 // Handle explicit sets: ["Set", 1, 2, 3]
3653 if ( domain . operator === 'Set' || domain . operator === 'List' ) {
@@ -49,13 +66,19 @@ export function extractFiniteDomain(
4966 for ( let i = start ; i <= end ; i ++ ) {
5067 rangeValues . push ( ce . number ( i ) ) ;
5168 }
52- return { variable, values : rangeValues } ;
69+ return { status : 'success' , variable, values : rangeValues } ;
70+ }
71+ if ( count > 1000 ) {
72+ return { status : 'non-enumerable' , variable, domain, reason : 'domain-too-large' } ;
5373 }
5474 }
5575 }
56- return { variable, values : [ ...values ] } ;
76+ return { status : 'success' , variable, values : [ ...values ] } ;
5777 }
58- return null ;
78+ if ( values && values . length > 1000 ) {
79+ return { status : 'non-enumerable' , variable, domain, reason : 'domain-too-large' } ;
80+ }
81+ return { status : 'error' , reason : 'empty-domain' } ;
5982 }
6083
6184 // Handle Range: ["Range", start, end] or ["Range", start, end, step]
@@ -75,10 +98,14 @@ export function extractFiniteDomain(
7598 for ( let i = start ; step > 0 ? i <= end : i >= end ; i += step ) {
7699 values . push ( ce . number ( i ) ) ;
77100 }
78- return { variable, values } ;
101+ return { status : 'success' , variable, values } ;
102+ }
103+ if ( count > 1000 ) {
104+ return { status : 'non-enumerable' , variable, domain, reason : 'domain-too-large' } ;
79105 }
80106 }
81- return null ;
107+ // Range with non-integer or symbolic bounds
108+ return { status : 'non-enumerable' , variable, domain, reason : 'non-integer-bounds' } ;
82109 }
83110
84111 // Handle finite integer Interval: ["Interval", start, end]
@@ -120,12 +147,52 @@ export function extractFiniteDomain(
120147 for ( let i = start ; i <= end ; i ++ ) {
121148 values . push ( ce . number ( i ) ) ;
122149 }
123- return { variable, values } ;
150+ return { status : 'success' , variable, values } ;
124151 }
152+ if ( count > 1000 ) {
153+ return { status : 'non-enumerable' , variable, domain, reason : 'domain-too-large' } ;
154+ }
155+ }
156+ // Interval with non-integer or symbolic bounds
157+ return { status : 'non-enumerable' , variable, domain, reason : 'non-integer-bounds' } ;
158+ }
159+
160+ // Check for known infinite sets (e.g., NonNegativeIntegers, Integers, Reals, etc.)
161+ if ( domain . symbol ) {
162+ const knownInfiniteSets = [
163+ 'Integers' , 'NonNegativeIntegers' , 'PositiveIntegers' , 'NegativeIntegers' ,
164+ 'Rationals' , 'Reals' , 'PositiveReals' , 'NonNegativeReals' , 'NegativeReals' ,
165+ 'NonPositiveReals' , 'ExtendedReals' , 'Complexes' , 'ImaginaryNumbers' ,
166+ 'Numbers' , 'ExtendedComplexes' , 'AlgebraicNumbers' , 'TranscendentalNumbers' ,
167+ ] ;
168+ if ( knownInfiniteSets . includes ( domain . symbol ) ) {
169+ return { status : 'non-enumerable' , variable, domain, reason : 'infinite-domain' } ;
125170 }
126- return null ;
171+ // Unknown symbol - could be a finite set, but we can't determine
172+ return { status : 'non-enumerable' , variable, domain, reason : 'unknown-domain' } ;
127173 }
128174
175+ // Unknown domain structure
176+ return { status : 'non-enumerable' , variable, domain, reason : 'unrecognized-domain-type' } ;
177+ }
178+
179+ /**
180+ * Extract the finite domain from a quantifier's condition.
181+ * Supports:
182+ * - ["Element", "x", ["Set", 1, 2, 3]] → [1, 2, 3]
183+ * - ["Element", "x", ["Range", 1, 5]] → [1, 2, 3, 4, 5]
184+ * - ["Element", "x", ["Interval", 1, 5]] → [1, 2, 3, 4, 5] (integers only)
185+ * Returns null if the domain is not finite or not recognized.
186+ * @deprecated Use extractFiniteDomainWithReason for better error handling
187+ */
188+ export function extractFiniteDomain (
189+ condition : BoxedExpression ,
190+ ce : ComputeEngine
191+ ) : { variable : string ; values : BoxedExpression [ ] } | null {
192+ const result = extractFiniteDomainWithReason ( condition , ce ) ;
193+ if ( result . status === 'success' ) {
194+ return { variable : result . variable , values : result . values } ;
195+ }
129196 return null ;
130197}
131198
0 commit comments