Diagnose symbolic range overlap

Author: code5717

CHANGELOG.md

@@ -43,6 +43,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - `fall` now lowers in both Zig and C backends for its documented narrow form:
   the final direct statement of a non-final match case. Invalid placements are
   semantic errors.
+- Match range diagnostics now catch conservative runtime-symbolic interval
+  overlaps when two inclusive ranges share an endpoint symbol, such as
+  `low..high` followed by `high..top`.
 - Release-manifest verification rejects parent-directory traversal and unsafe
   absolute paths, while preserving the documented flat downloaded-assets flow.
 - File-backed module imports are now contained to configured search paths and

MISSING_FEATURES.md

@@ -56,7 +56,8 @@
    - Exact duplicate bool, enum, and scalar literal case patterns are diagnosed.
    - Wildcard-first and fully covered bool/enum cases make later case patterns and else branches unreachable.
    - Literal and compile-time constant numeric/char range overlaps are diagnosed.
-   - Non-constant symbolic interval range overlap remains incomplete.
+   - Conservative non-constant symbolic interval overlaps are diagnosed when
+     inclusive ranges share an endpoint symbol.
    - True variable-binding/capture patterns are not defined; plain identifier patterns currently refer to existing symbols.
 
 2. **Memory/lifetime model**

TODO.md

@@ -119,8 +119,11 @@ Features that are spec'd and partially implemented, or missing from one backend.
 - [x] Add constant/computed-constant range match overlap diagnostics.
   Notes: literal, constant identifier, and simple constant-expression numeric/char endpoints now participate in range overlap and covered-literal diagnostics.
 
-- [ ] Add non-constant symbolic interval match overlap diagnostics.
-  Notes: range overlap checks do not reason about runtime symbolic intervals.
+- [x] Add conservative non-constant symbolic interval match overlap diagnostics.
+  Files: `a7/passes/type_checker.py`, `test/test_semantic_control_flow.py`
+  Notes: range overlap checks now diagnose inclusive runtime-symbolic ranges
+  that share an endpoint symbol, such as `low..high` followed by `high..top`;
+  arbitrary runtime inequalities are still not guessed.
 
 - [ ] Define and implement true variable-binding match patterns.
   Files: `a7/passes/type_checker.py`, `a7/backends/zig.py`, `a7/backends/c.py`

a7/passes/type_checker.py

@@ -1771,10 +1771,16 @@ def _match_pattern_range(self, pattern: ASTNode) -> Optional[Tuple[str, float, f
         start = self._range_pattern_value(pattern.start, set()) if pattern.start else None
         end = self._range_pattern_value(pattern.end, set()) if pattern.end else None
         if start is None or end is None:
-            return None
+            start = self._range_symbolic_value(pattern.start) if pattern.start else None
+            end = self._range_symbolic_value(pattern.end) if pattern.end else None
+            if start is None or end is None:
+                return None
 
         start_kind, start_value = start
         end_kind, end_value = end
+        if start_kind.startswith("symbol:") and end_kind.startswith("symbol:"):
+            symbols = sorted({start_kind.removeprefix("symbol:"), end_kind.removeprefix("symbol:")})
+            return (f"symbolic:{'|'.join(symbols)}", 0, 0)
         if start_kind != end_kind:
             return None
 
@@ -1855,6 +1861,25 @@ def _range_const_expr_value(self, node: Optional[ASTNode], resolving: Set[str])
 
         return None
 
+    def _range_symbolic_value(self, node: Optional[ASTNode]) -> Optional[Tuple[str, int | float]]:
+        """Resolve runtime-symbolic range endpoints backed by local variables."""
+        if node is None:
+            return None
+
+        if node.kind in {NodeKind.IDENTIFIER, NodeKind.PATTERN_IDENTIFIER}:
+            name = node.name or ""
+            if not name:
+                return None
+            symbol = self.symbols.lookup(name)
+            if symbol is None or symbol.kind != SymbolKind.VARIABLE:
+                return None
+            symbol_type = symbol.type
+            if symbol_type.kind != TypeKind.UNKNOWN and not self._is_numeric_compatible(symbol_type):
+                return None
+            return (f"symbol:{name}", 0)
+
+        return None
+
     def _range_literal_value(self, literal: ASTNode) -> Optional[Tuple[str, int | float]]:
         """Normalize literal values that can participate in range overlap checks."""
         if literal.literal_kind == LiteralKind.INTEGER:
@@ -1914,6 +1939,12 @@ def _find_overlapping_match_range(
         """Return a previous range pattern that overlaps this range, if any."""
         current_kind, current_low, current_high = range_key
         for seen_kind, seen_low, seen_high, seen_pattern in seen_ranges:
+            if current_kind.startswith("symbolic:") and seen_kind.startswith("symbolic:"):
+                current_symbols = set(current_kind.removeprefix("symbolic:").split("|"))
+                seen_symbols = set(seen_kind.removeprefix("symbolic:").split("|"))
+                if current_symbols & seen_symbols:
+                    return seen_pattern
+                continue
             if current_kind != seen_kind:
                 continue
             if current_low <= seen_high and seen_low <= current_high:

docs/SPEC.md

@@ -2133,7 +2133,8 @@ Status snapshot (2026-05-08):
    - Exact duplicate bool, enum, and scalar literal patterns are diagnosed.
    - Wildcard-first and fully covered bool/enum cases make later cases and else branches unreachable.
    - Literal and compile-time constant numeric/char range overlaps are diagnosed.
-   - Non-constant symbolic interval range overlap diagnostics are still incomplete.
+   - Conservative non-constant symbolic interval overlaps are diagnosed when
+     inclusive ranges share an endpoint symbol.
    - True variable-binding/capture patterns are not implemented; plain identifier patterns refer to existing symbols.
 
 3. **Memory/lifetime model depth**

site/public/docs/features.md

@@ -28,4 +28,4 @@
 
 ## Current Limits
 
-The status page is canonical for remaining gaps. Key limits include complete memory/lifetime guarantees, full generic specialization beyond simple top-level functions, tagged union workflows, and symbolic match-range diagnostics.
+The status page is canonical for remaining gaps. Key limits include complete memory/lifetime guarantees, full generic specialization beyond simple top-level functions, tagged union workflows, true match capture patterns, and arbitrary symbolic inequality reasoning.

site/public/docs/guide/features.md

@@ -28,4 +28,4 @@
 
 ## Current Limits
 
-The status page is canonical for remaining gaps. Key limits include complete memory/lifetime guarantees, full generic specialization beyond simple top-level functions, tagged union workflows, and symbolic match-range diagnostics.
+The status page is canonical for remaining gaps. Key limits include complete memory/lifetime guarantees, full generic specialization beyond simple top-level functions, tagged union workflows, true match capture patterns, and arbitrary symbolic inequality reasoning.

site/public/docs/status.md

@@ -15,7 +15,9 @@
 
 ## Known Gaps
 
-- Advanced match diagnostics still have incomplete symbolic interval overlap handling.
+- Advanced match diagnostics still lack true capture patterns and arbitrary
+  symbolic inequality reasoning; shared-endpoint symbolic range overlaps are
+  diagnosed.
 - Ownership/borrow-style lifetime guarantees are not implemented.
 - Heap fixed arrays (`new [N]T`) are rejected until their language and backend representation is defined.
 - Full generic specialization is incomplete beyond simple top-level generic functions.

site/public/llms-full.txt

@@ -39,7 +39,8 @@ Implemented:
 
 Known gaps:
 
-- Advanced match diagnostics do not reason about non-constant symbolic intervals.
+- Advanced match diagnostics catch shared-endpoint symbolic range overlaps, but
+  do not infer arbitrary symbolic inequalities.
 - True identifier-binding/capture match patterns are not defined.
 - Ownership, borrowing, lifetime, use-after-free, and double-free guarantees are not implemented.
 - Heap fixed arrays (`new [N]T`) are rejected until representation is defined.

site/src/pages/Status.tsx

@@ -13,7 +13,7 @@ const done = [
 ]
 
 const missing = [
-  { name: 'Advanced match diagnostics', desc: 'Exact duplicate, wildcard-first, full bool/enum coverage, and literal plus compile-time constant range overlaps are diagnosed. Non-constant symbolic intervals and true capture patterns remain open.' },
+  { name: 'Advanced match diagnostics', desc: 'Exact duplicate, wildcard-first, full bool/enum coverage, literal plus compile-time constant ranges, and shared-endpoint symbolic ranges are diagnosed. True capture patterns and arbitrary symbolic inequalities remain open.' },
   { name: 'Memory/lifetime model', desc: 'Only basic del reference checks. No ownership/borrow-style lifetime analysis.' },
   { name: 'Backend semantic parity hardening', desc: 'Core conformance is green, but differential backend checks should expand for every new language feature.' },
   { name: 'Package-registry publishing', desc: 'The current release workflow deliberately stops at package artifacts attached to draft GitHub releases. Registry publishing should be a separate reviewed change if it is added later.' },
@@ -57,8 +57,8 @@ export default function Status() {
 
       <SectionPanel title="Next priorities">
         <ol className="doc-list">
-          <li>Add non-constant symbolic interval range-overlap match diagnostics.</li>
-          <li>Improve type checker: control-flow narrowing and deeper assignment compatibility.</li>
+          <li>Define and implement true variable-binding match patterns.</li>
+          <li>Improve type checker: control-flow narrowing, arbitrary symbolic range reasoning, and deeper assignment compatibility.</li>
           <li>Expand differential/backend-equivalence checks for new language features.</li>
           <li>Decide whether package-registry publishing belongs in the release workflow; keep it out until that design is explicit.</li>
         </ol>