diff --git a/.github/workflows/build-oracle.yml b/.github/workflows/build-oracle.yml index f78851ed..a93f3b5d 100644 --- a/.github/workflows/build-oracle.yml +++ b/.github/workflows/build-oracle.yml @@ -234,6 +234,7 @@ jobs: > oracle/obstacle_distance_tests.txt ORACLE_BIN=oracle/oracle_bin python3 oracle/gen_arc_distance_tests.py \ > oracle/arc_distance_tests.txt + ORACLE_BIN=oracle/oracle_bin python3 oracle/red_sqlmm_wkt_tests.py - name: Upload oracle_bin artifact (90-day retention) uses: actions/upload-artifact@v4 diff --git a/.gitignore b/.gitignore index 5cb9116c..ee470b95 100644 --- a/.gitignore +++ b/.gitignore @@ -40,6 +40,7 @@ __pycache__/ # Prebuilt oracle binary (from CI artifacts for local harden/vector gen; reproducible via Dockerfile+make) oracle/oracle_bin +oracle/sqlmm_wkt_bin oracle/extracted.ml # Local agent / MCP scratch (not part of the corpus) diff --git a/TRIAGE_NTS_JTS_ISSUES.md b/TRIAGE_NTS_JTS_ISSUES.md index 032c6f20..4d6faf7d 100644 --- a/TRIAGE_NTS_JTS_ISSUES.md +++ b/TRIAGE_NTS_JTS_ISSUES.md @@ -103,6 +103,10 @@ proven, soundness or coordinates open) · **⬜ planned** (not yet started) · | **AT-\*** | Affine transforms (non-similarity → detect-and-densify, §7 risk) | TRIAGE park | — | ⬜ research park (no statement; `docs/scout/69-closing-summary.md`) | | **LRF-\*** | Linear referencing on curves | TRIAGE park | — | ⬜ research park (no statement; `docs/scout/69-closing-summary.md`) | | **DSF** | Densifier (curve → chords internally) | #64, #65 | `ArcChordApprox.v` (sagitta bound), `ArcChord{Density,Subdivision,Length,Sound}.v`, `CurveLinearise.v` (`chord_approx_ring_closed`); oracle `CP_BOUNDARY_SIMPLIFY` densify (`densify_arc`) | ✅ chord-approx faithfulness (closure); sagitta/`ring_simple` open | +| **CRV-CC** | SQL/MM `COMPOUNDCURVE` stays a compound (ISO/IEC 13249-3; no silent chord Flatten) | board CRV-CC · no Proofs epic | [`docs/scout/map-compoundcurve.md`](docs/scout/map-compoundcurve.md); `CurveGeometry.v : CurveSegment`; `CurveLinearise.v : chord_approx_ring_closed`; `HullExactExtrema.v : h_cc_still_densify` (H-CC stays on #424); `LECFlattenRow.v : empty_disk_flatten_iff` is member-min, not chords | 🟡 type + named linearise + I/O identity landed; GEOS leftover named (`ensureNoCurvedComponents` refuse + `getLinearized`). Ticket 30 closed on GEOS. NTS/JTS overlay still `Coordinate[]`. HOLD merge into JTS #7. HOLD a second CompoundCurve type. Do not remint `424-b` / `615-b` | +| **CRV-CP** | SQL/MM `CURVEPOLYGON` stays a curve polygon (ISO/IEC 13249-3; no silent POLYGON / LinearRing emit) | TRIAGE park · no Proofs epic · `#509` owns Jordan | [`docs/scout/map-curvepolygon.md`](docs/scout/map-curvepolygon.md); `CurveGeometry.v : valid_curve_polygon` (structural); `CurvePolygonSimple.v : curve_polygon_outer_not_simple_of_witness`; `CurvePolygonValid.v : valid_curve_polygon_cp`; `CurveLinearise.v : to_geometry_outer_ring_closed`; `WindingNumber.v : winding_decides_membership` is linear, not curve Jordan; `OverlayTouchRow.v : phase0_relation_complete_hypothesis_refuted` keeps kit-completeness fog | 🟡 type + named linearise + I/O identity landed; GEOS leftover named (OverlayNG + `createSurface` keep CURVEPOLYGON). Ticket 32 closed on GEOS. HOLD merge into JTS #7. HOLD a second CurvePolygon type. Do not remint `#509`. Do not steal ticket 30. Do not flip F-CP / V-CP | +| **CRV-MC** | SQL/MM `MULTICURVE` stays a multicurve (ISO/IEC 13249-3 §4.2.25; no silent MULTILINESTRING emit) | TRIAGE park · no Proofs epic | [`docs/scout/map-multicurve.md`](docs/scout/map-multicurve.md); `CurveGeometry.v : CurveSegment` is the member alphabet, not the collection; `CurveGeometry.v : valid_curve_geometry` is `list CurvePolygon` (F-MS-shaped), not MultiCurve; `CurveLinearise.v : chord_approx_ring_closed` is named linearise; `WktGeoJsonRoundtrip.v : wkt_geojson_wkt_roundtrip` has `GTMultiLineString` only; `OverlayTouchRow.v : phase0_relation_complete_hypothesis_refuted` keeps kit-completeness fog | 🟡 JTS type + NTS enum + I/O type 11 landed; Coq has no MultiCurve carrier; GEOS leftover named (OverlayNG keeps MULTICURVE). Ticket 34 closed on GEOS. HOLD merge into JTS #7. HOLD a second MultiCurve type. Do not steal tickets 30 / 32. Do not remint `#509`. Do not flip F-CP / F-MC / F-MS | +| **CRV-MS** | SQL/MM `MULTISURFACE` stays a multisurface (ISO/IEC 13249-3 §4.2.27; no silent MULTIPOLYGON emit) | TRIAGE park · no Proofs epic · `#509` owns per-member Jordan | [`docs/scout/map-multisurface.md`](docs/scout/map-multisurface.md); `CurveGeometry.v : valid_curve_geometry` is `list CurvePolygon` (structural F-MS); `CurveGeometry.v : valid_curve_geometry_nil` / `CurveGeometry.v : valid_curve_geometry_cons`; `CurveGeometry.v : to_geometry` is named collection linearise; `CurveLinearise.v : to_geometry_outer_ring_closed`; `WktGeoJsonRoundtrip.v : wkt_geojson_wkt_roundtrip` has `GTMultiPolygon` only; `OverlayTouchRow.v : phase0_relation_complete_hypothesis_refuted` keeps kit-completeness fog | 🟡 Coq structural collection + JTS type + NTS enum + I/O type 12 landed; GEOS leftover named (`restrictToSurfaces` checks `hasCurvedTypes`). Ticket 36 closed on GEOS. HOLD merge into JTS #7. HOLD a second MultiSurface type. Do not steal tickets 30 / 32 / 34. Do not remint `#509`. Do not flip F-CP / F-MC / F-MS | | **BUF-1 / BUF-N** | Single-/multi-arc buffer → `CurvePolygon` | #65 | 18× `Buffer*.v` (linear), `ExtractBufferRings.v`; `CurveBufferArea.v`, `CurveRingOffset.v`, `CurveOffsetAssembly{,Total}.v`, `CurveRoundJoin.v`, **`ClothoidBufferBridge.v`, `ClothoidOffsetContact.v`, `ClothoidBufferAssembly.v`, `CurveRingOffsetSimple.v`** (clothoid chain); oracle `BUFFER_REGION` (+ `ARC_BUFFER_SIMPLE/FULL` pins); **oracle pilot for unified segments + NTS sketch (2026-06)** | 🟡 arc buffer-region boundary+area cert ✅ (3-ax) + d=0 + helpers; **clothoid buffer-ring chain ✅ (2026-06-30): validity → adjacent offset contact → whole-ring assembly cleanliness → non-adjacent simplicity under clearance > 2·\|d\| = simple-closed-curve cert**; oracle pilot + dispatcher sketch for Arc/CS/CC/CP; pure-linear regression zero; Minkowski + unconditional simplicity deferred. | | **OFF** | Offset curve (arc-preserving) | #65 | `BufferOffset.v`, `ArcOffset.v`, `ArcOffsetThreePoint.v` (`arc_offset_preserves_arc`), `CurvePolygonOffset.v`, `CurveRingOffset.v`, `ClothoidBufferBridge.v` (`clothoid_ring_offset_valid` + sharpness), `ClothoidOffsetContact.v`, `ClothoidBufferAssembly.v`, `CurveRingOffsetSimple.v`; oracle `ARC_OFFSET_XY` | 🟡 arc offset ✅ (valid arc → valid arc, radius r+d); **clothoid ring offset now soundness-complete at the adjacency level + non-adjacent simplicity gated on a clearance hypothesis (2026-06-30)** | | **VBF** | Variable-distance buffer | #65 | — | ⬜ | @@ -117,6 +121,15 @@ proven, soundness or coordinates open) · **⬜ planned** (not yet started) · | **TRI-VR** | Voronoi on curved input | #68 | — | ⬜ | | **TB-\* / F-RD** | TestBuilder rendering / `ShapeWriter` hooks | — | — | — not proof-relevant | +**§4.2.1 types that are not optional extras.** `ST_Clothoid`, +`ST_Circle`, `ST_GeodesicString`, `ST_NURBSCurve`, `ST_SpiralCurve` +are instantiable ST_Curve subtypes in ISO/IEC 13249-3 §4.2.1. GEOS +WKT names them and refuses. Oracle mode `SQLMM_WKT` parses type +identity (including the SPIRALTYPE open-set lexer deviation). NTS +WKT names them and refuses (ticket 38). Not leftover `Ⅺ`. Do not +remint `508-*`. Do not grow `CurveSegment`. Do not flip F-CP / F-MC +/ F-MS / V-CP. + **Reading the table against the EPIC's Definition of Done (§10).** JTS#1195's DoD requires curve-preserving output "**where mathematically sound**" — which is exactly what the ✅ rows certify and the 🟡 rows bound. The §7 "arc intersection diff --git a/docs/gated-prose-docs.txt b/docs/gated-prose-docs.txt index 8d14264a..4587322f 100644 --- a/docs/gated-prose-docs.txt +++ b/docs/gated-prose-docs.txt @@ -16,3 +16,7 @@ docs/scout/spec-interior-side.md docs/scout/map-523.md docs/scout/spec-523.md docs/scout/map-iso-st-relate-qex.md +docs/scout/map-compoundcurve.md +docs/scout/map-curvepolygon.md +docs/scout/map-multicurve.md +docs/scout/map-multisurface.md diff --git a/docs/iso13249-3-curve-type-bindings-2026-08.md b/docs/iso13249-3-curve-type-bindings-2026-08.md index 91f45da9..38c882de 100644 --- a/docs/iso13249-3-curve-type-bindings-2026-08.md +++ b/docs/iso13249-3-curve-type-bindings-2026-08.md @@ -40,6 +40,12 @@ TYPE` definitions in clauses 5–8): | ST_Curve | ST_Geometry | **no** (`NOT INSTANTIABLE`) | §4.2.4 / §7.1.1 | `Curve` (abstract), `Geometries/Curve.cs:10` | | ST_LineString | ST_Curve | yes | §4.2.5 / §7.2.1 | `LineString` | | ST_CircularString | ST_Curve | yes | §4.2.6 / §7.3.1 | `Curves/CircularString.cs:36` | +| ST_Circle | ST_Curve | yes | §4.2.7 | absent — **not an optional extra** | +| ST_GeodesicString | ST_Curve | yes | §4.2.8 | absent — **not an optional extra** | +| ST_EllipticalCurve | ST_Curve | yes | §4.2.9 | absent — **not an optional extra** | +| ST_NURBSCurve | ST_Curve | yes | §4.2.10 | absent — **not an optional extra** | +| ST_Clothoid | ST_Curve | yes | §4.2.11 | absent — **not an optional extra** | +| ST_SpiralCurve | ST_Curve | yes | §4.2.12 | absent — **not an optional extra** | | ST_CompoundCurve | ST_Curve | yes | §4.2.13 / §7.10.1 | `Curves/CompoundCurve.cs:36` | | ST_Surface | ST_Geometry | **no** | §4.2.14 / §8.1.1 | `Surface` (abstract), `Geometries/Surface.cs:16` | | ST_CurvePolygon | ST_Surface | yes | §4.2.15 / §8.2.1 | `Curves/CurvePolygon.cs:38` (`Surface`) | @@ -47,14 +53,17 @@ TYPE` definitions in clauses 5–8): | ST_MultiCurve | ST_GeomCollection | "may be instantiable" | §4.2.25 | `Curves/MultiCurve.cs:19` | | ST_MultiSurface | ST_GeomCollection | "may be instantiable" | §4.2.27 | `Curves/MultiSurface.cs:19` | -The spec also defines further instantiable ST_Curve subtypes the branch does not -model: ST_Circle (§4.2.7), ST_GeodesicString (§4.2.8), ST_EllipticalCurve -(§4.2.9), ST_NURBSCurve (§4.2.10), ST_Clothoid (§4.2.11), ST_SpiralCurve -(§4.2.12 — spiral types "initially limited to" clothoid, bloss, biquadratic, -sine, cosine). These are the CONTEXT.md "expansion backlog", verified present in -the spec. §4.2.1 also explicitly permits an implementation to add subtypes and -to interpose types, provided subtype relationships are preserved — this is the -clause that legitimises `Curve`/`Surface` as interposed abstractions. +ST_Circle, ST_GeodesicString, ST_EllipticalCurve, ST_NURBSCurve, +ST_Clothoid, and ST_SpiralCurve (spiral types "initially limited to" +clothoid, bloss, biquadratic, sine, cosine) are instantiable ST_Curve +subtypes in the §4.2.1 hierarchy. They are **not optional extras**. +The NTS curve-foundation branch does not yet carry them. GEOS and +NTS WKT name them and refuse; calling them "Unknown type" is a lie. +§4.2.1 also permits an implementation to add subtypes and to interpose +types, provided subtype relationships are preserved — that clause +legitimises `Curve`/`Surface` as interposed abstractions, not a +licence to drop these types from the model. Do not remint `508-*`. +Do not grow `CurveSegment`. ST_Curve semantics that bind every curve subtype (§4.2.4): @@ -267,6 +276,25 @@ items that follow it): itself admits any count ≥ 1; the odd-count ≥ 3 rule is semantic well-formedness (§7.3.1 Desc 7), enforced when the produced point array feeds `NEW ST_CircularString` (§5.1.67 item e). +- `CIRCLE [ ] ` — `EMPTY` or exactly three points + (§4.2.7). Oracle mode `SQLMM_WKT` parses this as type identity. +- `GEODESICSTRING [ ] ` — `EMPTY` or a + parenthesised point list, count ≥ 2 (§4.2.8). Same oracle mode. +- `ELLIPTICALCURVE [ ] ` — `EMPTY` or named + fields `AFFINEPLACEMENT`, `UAXISLENGTH`, `VAXISLENGTH` (and the + start/end angles when present) (§4.2.9). Instantiable; not UNKNOWN. +- `NURBSCURVE [ ] ` — `EMPTY` or `DEGREE`, `KNOTS`, + `CONTROLPOINTS` as weighted points (§4.2.10 / §7.7). Structural + parse only; the `N` length token stays a projection, not this mode. +- `CLOTHOID [ ] ` — `EMPTY` or `AFFINEPLACEMENT` + (`LOCATION`, `REFERENCEDIRECTIONS`), `SCALEFACTOR`, `STARTDISTANCE`, + `ENDDISTANCE` (§4.2.11 / §7.8). Structural parse only; the `K` + length token stays a projection. +- `SPIRALCURVE [ ] ` — `EMPTY` or `SPIRALTYPE` + `` plus optional `AFFINEPLACEMENT` / `LENGTH` / + `STARTCURVATURE` / `ENDCURVATURE` (§4.2.12 / §7.9 / ST_SpiralType + §7.9.7). The text lexer for `` is a documented + deviation: see §8. - `COMPOUNDCURVE [ ] `, components are `` ::= **bare** `` (a parenthesised point list with *no* LINESTRING keyword) | tagged `` | @@ -549,6 +577,19 @@ spec-adjacent statements, checked: - **Published-IS wording**: citations are from the DIS ballot text of the 5th edition (N 2593). No claim here was found only in ballot-specific front matter, but clause-item numbering in the published 2016 IS could differ. +- **SPIRALTYPE text lexer**: the standard defines `` as + free-form ``, and §5.1.68 length-prefixes the value in WKB, so + the value set is open — §4.2.12 lists `clothoid`, `bloss`, + `biquadratic`, `sine` and `cosine` only as the *initial* set. Text has + no length prefix, and `` admits the characters that would end + the value, so oracle `SQLMM_WKT` reads a spiral type up to the comma + or parenthesis that terminates it. Interior spaces are preserved: + `SPIRALTYPE Wiener Bogen` parses as an open-set extension (LandXML / + railway alignment name; not a new SQL/MM type and not Koc compound). + A name containing a comma or a parenthesis is the one case this + grammar cannot represent — the leftover token after the terminator + is `REFUSE`, not a type value. Pinned by `oracle/red_sqlmm_wkt_tests.py`. + Do not remint `508-*`. Do not grow `CurveSegment`. --- diff --git a/docs/scout/map-compoundcurve.md b/docs/scout/map-compoundcurve.md new file mode 100644 index 00000000..8c50f74d --- /dev/null +++ b/docs/scout/map-compoundcurve.md @@ -0,0 +1,155 @@ +# Map — COMPOUNDCURVE flatten-elimination + +A wayfinder map. Charted 2026-09-01. This is **not** a `wayfinder:map` +GitHub issue, **not** a remint of `424-b` / `69-a` / `508-*` / +`615-b`, and **not** leftover `Ⅰ`–`Ⅹ`. It does **not** implement +flatten-elimination. It does **not** mint a second CompoundCurve type. +It does **not** merge into JTS #7. Board card: Notion **CRV-CC**. + +> Architect SIGN 16 Aug 2026: HOLD implement is lifted for +> flatten-elimination only. HOLD merge into #7. Keep COMPOUNDCURVE / +> CIRCULARSTRING (ISO/IEC 13249-3). Do not silently flatten. Named +> linear fallback stays named. Option C / curve DCEL. No public noder. +> #27 out. #38 off #7. No type-9 reader PR. No GEO-TIN 15–17. Cite +> 13249-3. No DOI. HOLD a second CompoundCurve type. No priority. + +topics: arc, wkt +claimId: none +witness: none + +## Destination + +**Name the flatten-elimination leftover so the next `/implement` cannot +steal a closed letter, invent a second CompoundCurve type, or treat I/O +round-trip as overlay honesty.** + +SQL/MM `ST_CompoundCurve` (ISO/IEC 13249-3 §4.2.13 / §7.10.1; WKB type +9) is already a first-class type. The ask is honesty: a compound stays +a compound. Silent chord densify for overlay, hull, or TestBuilder is +a refuse. Named `Linearize` / `toLinear` / `chord_approx_ring` is not +that refuse. + +This letter does not retire a tracker and does not mint an epic. +Epic creation stays owner-scope. + +## Three words that say "flatten" + +| Word | What it is | Park | Status | +|---|---|---|---| +| Silent chord Flatten | Overlay / hull / TestBuilder eat `COMPOUNDCURVE` as `Coordinate[]` / `LineString` chords with no stamp | leftover **flatten-elimination** | Named on GEOS. Ticket 30 closed. `ensureNoCurvedComponents` refuses and names `getLinearized`. NTS/JTS overlay path still `Coordinate[]`. | +| Named linear fallback | `Linearize` / `toLinear` / `chord_approx_ring` / OverlayNGCurve `APPROX` + `isApproximate()` | technique (named) | Allowed. NTS `ILinearizable.Linearize`. JTS `toLinear`. Coq `CurveLinearise.v : chord_approx_ring_closed`. Clothoid / uncertified mix stays named. | +| Member / splice flatten | LEC min-over-members; ISO nested-CC splice into the component list | already landed | `LECFlattenRow.v : empty_disk_flatten_iff`. #615-b nested-CC splice (`2c4c7bc`) is §7.10.1, not chord densify. Do not remint `615-b`. | + +I/O type identity is not op honesty. JTS `SqlMmTypes.refuseFlatten` and +`IoFlattenHonestyTest` keep WKT/WKB/GML/KML/GeoJSON from writing a +control polygon. WKB/WKT may round-trip type 9 and still lie in +overlay unless the op carries a path stamp (sibling card QG-CURVE-CHORD; +HOLD implement; does not join this leftover). + +## What is already true + +| Surface | Pin | Honesty | +|---|---|---| +| 60s reader | `docs/HELP.md` BIM Bea card; `docs/READING-GUIDE.md` | Names CIRCULARSTRING / COMPOUNDCURVE / CURVEPOLYGON and that Flatten-to-chords is lossy. Joost card JOOST-CC-HELP is met on Proofs. Method name on the NTS tree is now `Linearize`, not `Flatten` — name drift, not a drop. | +| SQL/MM type | `CurveGeometry.v` (`CurveRing` = `CSChord` \| `CSArc`) | All-arc ring is CIRCULARSTRING; mixed ring is COMPOUNDCURVE. Clause book: `docs/iso13249-3-curve-type-bindings-2026-08.md` §2.2. Cite 13249-3, not 19125-2. | +| Named Option B bridge | `CurveLinearise.v : chord_approx_ring_closed` | Combinatorial faithfulness of the *named* linearise. Not silent Flatten. | +| Length additivity | `CurveLength.v : curve_length_additive` | Compound = member sum. TRIAGE M-LEN-CC. Do not remint `508-*`. | +| Offset keeps structure | `CurveRingOffset.v : curve_ring_offset_arcs_valid` | Segment count survives. Not overlay honesty. | +| Hull leftover already named | `HullExactExtrema.v : h_cc_still_densify` | CompoundCurve (`h_cc_input`) is not the PR #8 CurveExact cell. H-CC stays on **#424** (JTS #6). Do not remint `424-b`. | +| OverlayNGCurve Phase 0 | `OverlayNGCurve.v : overlayng_curve_phase0_exact_cells` | Self / empty / disjoint / covers collapse without densify. APPROX cells stay named. | +| LEC member flatten | `LECFlattenRow.v : empty_disk_flatten_iff` | Typed min-fold, not chords. | +| Koc railway assembly | `CompoundCurveKoc.v` / `CompoundCurveAssembly.v` | Surveyor's clothoid+arc alignment (EN 13803-1). **Not** SQL/MM `ST_CompoundCurve`. Do not join them. | +| NTS I/O | `WKTReader` / `WKTWriter` / `OgcGeometryType.CompoundCurve = 9` | Type identity. Nested COMPOUNDCURVE rejected as a *member of another* (`ReadRejectsNestedCompoundCurves`); #615-b splices on the foundation branch. Off #7. | +| JTS I/O refuse | `SqlMmTypes.refuseFlatten`; `IoFlattenHonestyTest` | Core writers refuse a CompoundCurve control polygon. Already on the curve branch. No type-9 reader PR from this letter. | + +## Leftover table + +Parks follow ADR-0002. Value and priority are orthogonal. This letter +does not set WSJF. + +| Id | Leftover | Kind | Park | Status | Do not | +|---|---|---|---|---|---| +| flatten-elimination | Silent chord path at overlay / hull / TestBuilder | CRV-CC | technique | Named on GEOS (`ensureNoCurvedComponents` refuse + `getLinearized`). Ticket 30 closed. NTS `Operation/` has no `CompoundCurve` overlay path — the data plane is still `Coordinate[]` (`docs/audit-phase4-curves.md`). JTS OverlayNGCurve kits exist for some CompoundCurve shells; unnamed cells densify with `isApproximate()`. | steal `424-b`; treat I/O refuse as overlay honesty; merge into JTS #7; mint a second CompoundCurve type; remint `615-b` / LEC flatten as this leftover | +| — | H-CC CompoundCurve hull | #424 | technique | Already a leftover of `424-b`. JTS #6. | remint `424-b`; pull H-CC into CRV-CC | +| — | QG-CURVE-CHORD path stamp | sibling board card | sequencing | HOLD implement. Does not join flatten-elimination. | invent EXACT / NAMED-APPROX / CHORD-PATH CI on this letter | +| — | TestBuilder draw CompoundCurve | sibling TB card | sequencing | tb-t-1/2 not SIGNed. TB-\* is not proof-relevant in TRIAGE. | open a type-9 reader PR to "see" it | +| — | JTS #27 OverlayNG-for-circles (Option B, OV-P2) | JTS #27 | sequencing | **Out.** | fold into this map; merge into #7 | +| — | JTS #38 package-private curve DCEL (Option C, OV-P2) | JTS #38 | sequencing | Off #7 unless PO says merge. No public noder. | make the DCEL public; steal leftover kits as this leftover | +| — | Second CompoundCurve type | board HOLD | sequencing | The existing NTS / JTS / Coq carriers stay. | mint a parallel type; join GEO-TIN 15–17 | +| — | WKB type-9 reader PR | I/O | sequencing | Type 9 is already named on #7 I/O 8–12. | open a reader-only PR from this letter | + +## Decisions so far + +- COMPOUNDCURVE is SQL/MM ISO/IEC 13249-3, WKB 9. Cite that standard. + There is no DOI. Do not cite ISO 19125-2. +- Joost / Bea 60s reader is met on Proofs HELP + READING-GUIDE. +- Flatten-elimination is the one leftover this card owns. It is not + leftover `Ⅵ`, not `CRV-CC` as a Proofs claimId, and not a new epic. +- Named linear fallback stays named. Silent Flatten is a refuse. +- Member-min flatten and nested-CC splice are other words. They stay + where they landed. +- Koc compound curves stay a railway-alignment satellite. They do not + satisfy CRV-CC. +- JTS #27 is out. JTS #38 stays off #7. No public noder. +- HOLD merge into #7. HOLD a second CompoundCurve type. No priority + from this letter. +- `/implement 660` on GEOS named the leftover: hull / centroid / + buffer refuse via `ensureNoCurvedComponents` and stamp via + `getLinearized`. Ticket 30 closed. See + [`closed/30-compoundcurve-flatten-elimination.md`](tickets/closed/30-compoundcurve-flatten-elimination.md). +- ST_Clothoid, ST_Circle, ST_GeodesicString, ST_NURBSCurve, and + ST_SpiralCurve are instantiable in ISO/IEC 13249-3 §4.2.1. They + are not optional extras. GEOS WKT refuses them as SQL/MM types. + Oracle mode `SQLMM_WKT` parses type identity (ticket 37). NTS WKT + names them and refuses (ticket 38), matching GEOS. Do not remint + `508-*`. Do not grow `CurveSegment`. Not leftover `Ⅺ`. + +## Fog + +- **Which NTS overlay entry still densifies without a stamp** is an + NTS/JTS engine leftover, not a Coq lemma. GEOS named the refuse + (`ensureNoCurvedComponents`) and the stamp (`getLinearized`). The + audit-phase4 `Flatten()` at `CurveGeometryOverlay.cs:36` names the + historical `.Curve` extension; this NTS clone has `Linearize` and no + `Flatten()` on curve types. +- **HELP still says `Flatten()`** while the NTS method is `Linearize`. + Name drift. Do not treat it as Bea dropping COMPOUNDCURVE again. +- **Option C leftover kits** wait on JTS #38. This map does not level + them. +- **QG-CURVE-CHORD** stays a separate card. + +## Frontier + +Ticket 29 (this chart) is closed. Ticket 30 is closed on GEOS: +`ensureNoCurvedComponents` refuses and names `getLinearized`. +Ticket 38 is closed on NTS: `WKTReader` names the §4.2.1 types and +refuses (not `Unknown type`). JTS overlay still has no CompoundCurve +path. Next useful session is a JTS letter, or stop. + +Sibling CURVEPOLYGON / MULTICURVE / MULTISURFACE leftovers +(tickets 32 / 34 / 36) are also closed on GEOS in this packet. + +``` +HELP / READING-GUIDE ════════════ COMPOUNDCURVE named ── Joost met +CurveGeometry + CurveLinearise ═ named Option B bridge +I/O type 9 ════════════════════ identity, not op honesty ── off #7 +LEC / #615-b ══════════════════ member/splice flatten ── not this leftover +424-b h_cc_still_densify ══════ H-CC stays on #424 + +flatten-elimination ────────── ticket 30 closed on GEOS +#27 ── out +#38 ── Option C DCEL ── off #7 ── no public noder +second type / type-9 reader / GEO-TIN 15–17 ── HOLD +``` + +## Do not + +- Remint `424-b` / `69-a` / `508-*` / `522-*` / `615-b`. +- Mint leftover `Ⅵ` or `CRV-CC` as a Proofs claimId. +- Mint a GitHub child from this map. +- Implement flatten-elimination in this letter. +- Merge into JTS #7. Open a type-9 reader PR. Join GEO-TIN 15–17. +- Invent a DOI. Cite 19125-2. Copy clothoid Zenodo. +- Conflate Koc railway compound with SQL/MM COMPOUNDCURVE. +- Treat `LECFlattenRow.v : empty_disk_flatten_iff` as chord honesty. +- Set backlog priority. diff --git a/docs/scout/map-curvepolygon.md b/docs/scout/map-curvepolygon.md new file mode 100644 index 00000000..54b83e4d --- /dev/null +++ b/docs/scout/map-curvepolygon.md @@ -0,0 +1,162 @@ +# Map — CURVEPOLYGON type honesty + +A wayfinder map. Charted 2026-09-01. This is **not** a `wayfinder:map` +GitHub issue, **not** a remint of `#509` / `69-a` / `508-*` / leftover +`Ⅰ`–`Ⅹ`, and **not** COMPOUNDCURVE ticket 30. It does **not** implement +silent-POLYGON elimination. It does **not** mint a second CurvePolygon +type. It does **not** merge into JTS #7. No dedicated board card; sibling +cards FCP-S (I/O) and TB-T (draw) stay where they are. + +> Architect SIGN 16 Aug 2026 on FCP-S: HOLD type I/O 13–17 / 18–20. +> Off #7 for anything not already landed. Do not mark pass. Cite 13249-3 +> for types 8–12 only. No invented DOI. **No SIGN lifts HOLD implement +> for this leftover.** Named linear fallback stays named. No GEO-TIN +> 15–17. No type-10 reader PR. No second CurvePolygon type. No priority. + +topics: arc, wkt +claimId: none +witness: none + +## Destination + +**Name the silent POLYGON-collapse leftover so the next `/implement` +cannot steal `#509`, steal COMPOUNDCURVE ticket 30, invent a second +CurvePolygon type, or treat I/O round-trip as overlay honesty.** + +SQL/MM `ST_CurvePolygon` (ISO/IEC 13249-3 §4.2.15 / §8.2.1; WKB type +10) is already a first-class type. Rings are ST_Curve values that are +rings (closed ∧ simple). The ask is honesty: a curve polygon stays a +curve polygon. Silent emit of `POLYGON` / `LinearRing` for overlay, +hull, or TestBuilder is a refuse. Named `Linearize` / `toLinear` / +`chord_approx_ring` is not that refuse. JTS +`Polygon.getExteriorRing()` returning a derived `LinearRing` is the +named Option-A contract, not the leftover — the true shell is +`getExteriorCurve()`. + +This letter does not retire a tracker and does not mint an epic. +Epic creation stays owner-scope. `#509` stays OPEN. + +## Three words that say "collapse" + +| Word | What it is | Park | Status | +|---|---|---|---| +| Silent POLYGON collapse | Overlay / hull / TestBuilder eat `CURVEPOLYGON` and emit `POLYGON` / `LinearRing` chords with no stamp; or treat JTS `getExteriorRing()` as if it were the curve | leftover **silent-polygon-collapse** | Named on GEOS OverlayNG + `createSurface`. Ticket 32 closed. Distinct from COMPOUNDCURVE ticket 30 (lineal chord Flatten). | +| Named linear fallback | `Linearize` / `toLinear` / `chord_approx_ring` / OverlayNGCurve `APPROX` + `isApproximate()` | technique (named) | Allowed. NTS `ILinearizable.Linearize`. JTS `toLinear`. Coq `CurveLinearise.v : to_geometry_outer_ring_closed` and `CurveLinearise.v : chord_approx_ring_closed`. | +| Structural F-CP / Jordan | Rings stay `Curve` on NTS; Coq `CurvePolygon` is structural; true-region waits on `#509` | already landed / `#509` | NTS `CurvePolygon.ExteriorRing => _shell` (`Curve`). `CurveGeometry.v : valid_curve_polygon` is structural only. V-CP Jordan is `#509`. Do not remint `#509`. | + +I/O type identity is not op honesty. FCP-S keeps WKT +`CURVEPOLYGON((CIRCULARSTRING …))` exposing `getExteriorCurve()` as a +curve and writing CIRCULARSTRING back. WKB/WKT may round-trip type 10 +and still lie in overlay unless the op carries a path stamp (sibling +card QG-CURVE-CHORD; HOLD implement; does not join this leftover). + +## What is already true + +| Surface | Pin | Honesty | +|---|---|---| +| 60s reader | `docs/HELP.md` BIM Bea card; `docs/READING-GUIDE.md` | Names CIRCULARSTRING / COMPOUNDCURVE / CURVEPOLYGON and that Flatten-to-chords is lossy. Method name on the NTS tree is now `Linearize`, not `Flatten` — name drift, not a drop. | +| SQL/MM type | `CurveGeometry.v : valid_curve_polygon` | Structural only (each ring's arcs valid). Clause book: `docs/iso13249-3-curve-type-bindings-2026-08.md` §2.3. Cite 13249-3, not 19125-2. Rings are ST_Curve, closed ∧ simple. | +| Ring simplicity | `CurvePolygonSimple.v : curve_polygon_outer_not_simple_of_witness` | Witness-sound outer not-simple. Not Jordan. | +| Holes-inside-shell floor | `CurvePolygonValid.v : valid_curve_polygon_cp` / `CurvePolygonValid.v : valid_curve_polygon_cp_hole_witness` | Conservative inscribed control polygon. True-region waits on `#509`. | +| Named Option B bridge | `CurveLinearise.v : to_geometry_outer_ring_closed` | Combinatorial faithfulness of the *named* linearise of the outer ring. Not silent POLYGON emit. | +| Chord-only rect | `RelateCurveAreaPoint.v : valid_rect_curve_polygon` | A rectangular `CurvePolygon` of chords. No curve→matrix soundness. | +| Linear winding | `WindingNumber.v : winding_decides_membership` | Linear ring. Not curve Jordan. Do not treat as `#509`. | +| Kit-completeness fog | `OverlayTouchRow.v : phase0_relation_complete_hypothesis_refuted` | CUP/CAP/XOR/SUB + T-in/T-out stays fog. T-in/T-out is vocabulary this corpus does not have. "Complete" has a refuted ancestor. | +| NTS F-CP contract | `CurvePolygon` extends `Surface` | `ExteriorRing => _shell` stays `Curve`. Never collapsed to `LinearRing` at the accessor. Off `develop` without further design. | +| JTS Option A | `CurvePolygon` extends `Polygon` | Legacy `getExteriorRing()` is a derived `LinearRing` from control points (not `toLinear`). True arc is `getExteriorCurve()`. Named, not silent. | +| FCP-S I/O | Notion FCP-S; WKB type 10 | Exterior stays a curve on WKT read. HOLD type I/O 13–17 / 18–20. Off #7. Do not mark pass. | +| F-CP / V-CP TRIAGE | `#64` residue / `#509` | Structural model + validity/simplicity witness-sound; true-region deferred. This letter does not flip those rows. | + +## Leftover table + +Parks follow ADR-0002. Value and priority are orthogonal. This letter +does not set WSJF. + +| Id | Leftover | Kind | Park | Status | Do not | +|---|---|---|---|---|---| +| silent-polygon-collapse | Silent emit of `POLYGON` / `LinearRing` at overlay / hull / TestBuilder, or treating `getExteriorRing()` as the curve | CRV-CP | technique | Named on GEOS OverlayNG + `createSurface` (all-linear rings stay CURVEPOLYGON). Ticket 32 closed. NTS/JTS leftover sites stay an engine grill. | steal `#509`; steal COMPOUNDCURVE ticket 30; treat FCP-S I/O as overlay honesty; merge into JTS #7; mint a second CurvePolygon type | +| — | V-CP Jordan true-region | `#509` | technique | Already the V-CP true-region epic. Stays OPEN. | remint `#509`; pull Jordan into CRV-CP | +| — | COMPOUNDCURVE flatten-elimination | CRV-CC / ticket 30 | technique | Sibling in this packet. Lineal compound chord Flatten. | steal ticket 30 for a CURVEPOLYGON site | +| — | QG-CURVE-CHORD path stamp | sibling board card | sequencing | HOLD implement. Does not join silent-polygon-collapse. | invent EXACT / NAMED-APPROX / CHORD-PATH CI on this letter | +| — | FCP-S WKT shell | sibling visual case | sequencing | I/O identity. HOLD type I/O 13–17 / 18–20. Do not mark pass. | open a type-10 reader PR to "see" it | +| — | TestBuilder draw CurvePolygon | sibling TB-T card | sequencing | Never POLYGON. TB-\* is not proof-relevant in TRIAGE. | treat draw UX as this leftover | +| — | Kit-completeness (CUP/CAP/XOR/SUB + T-in/T-out) | fog | research | T-in/T-out is missing vocabulary. Completeness has a refuted ancestor. | mint a completeness epic; remint leftover `Ⅰ`–`Ⅹ` | +| — | JTS #27 OverlayNG-for-circles (Option B) | JTS #27 | sequencing | **Out.** | fold into this map; merge into #7 | +| — | JTS #38 package-private curve DCEL (Option C) | JTS #38 | sequencing | Off #7 unless PO says merge. No public noder. | make the DCEL public | +| — | Second CurvePolygon type | board HOLD | sequencing | The existing NTS / JTS / Coq carriers stay. | mint a parallel type; join GEO-TIN 15–17 | +| — | WKB type-10 reader PR | I/O | sequencing | Type 10 is already named on #7 I/O 8–12. | open a reader-only PR from this letter | + +## Decisions so far + +- CURVEPOLYGON is SQL/MM ISO/IEC 13249-3, WKB 10. Cite that standard. + There is no DOI. Do not cite ISO 19125-2. +- Bea 60s reader is met on Proofs HELP + READING-GUIDE. +- Silent POLYGON collapse is the one leftover this card owns. It is not + leftover `Ⅵ`, not `CRV-CP` as a Proofs claimId, not `#509`, and not + a new epic. +- Named linear fallback stays named. Silent POLYGON emit is a refuse. +- JTS `getExteriorRing()` → `LinearRing` is named Option A. The + leftover is treating that accessor as the curve, or emitting + `POLYGON` from an op with no stamp. +- NTS F-CP (`ExteriorRing` typed `Curve`) is already the structural + contract. This letter does not remint it. +- `#509` owns Jordan true-region. F-CP / V-CP TRIAGE rows do not flip. +- Kit-completeness stays fog. +- COMPOUNDCURVE ticket 30 stays a lineal Flatten leftover. +- JTS #27 is out. JTS #38 stays off #7. No public noder. +- HOLD merge into #7. HOLD a second CurvePolygon type. No priority + from this letter. +- `/implement 660` on GEOS named the leftover: OverlayNG keeps + CURVEPOLYGON (including all-linear LineString rings via + `createSurface`). Ticket 32 closed. See + [`closed/32-curvepolygon-silent-polygon-collapse.md`](tickets/closed/32-curvepolygon-silent-polygon-collapse.md). + +## Fog + +- **Which NTS / JTS overlay entry still emits POLYGON without a stamp** + is an NTS/JTS engine leftover, not a Coq lemma. GEOS OverlayNG + already keeps CURVEPOLYGON. +- **HELP still says `Flatten()`** while the NTS method is `Linearize`. + Name drift. Do not treat it as Bea dropping CURVEPOLYGON again. +- **T-in / T-out** is vocabulary this corpus does not have. +- **QG-CURVE-CHORD** stays a separate card. + +## Frontier + +Ticket 31 (this chart) is closed. Ticket 32 is closed on GEOS: +OverlayNG + `createSurface` keep CURVEPOLYGON. NTS/JTS overlay +sites stay an engine grill. Next useful session is an NTS or JTS +letter, or stop. + +Sibling COMPOUNDCURVE tickets 29 / 30 live in this packet +(`map-compoundcurve.md`). Numbered 31 / 32 so the leftovers stay +distinct. + +``` +HELP / READING-GUIDE ════════════ CURVEPOLYGON named ── Bea met +CurveGeometry + CurvePolygon* ══ structural F-CP / V-CP floor +I/O type 10 / FCP-S ════════════ identity, not op honesty ── off #7 +#509 V-CP Jordan ══════════════ true-region ── stays OPEN +CRV-CC ticket 30 ══════════════ lineal Flatten ── sibling, closed on GEOS + +silent-polygon-collapse ────── ticket 32 closed on GEOS +#27 ── out +#38 ── Option C DCEL ── off #7 ── no public noder +second type / type-10 reader / GEO-TIN 15–17 ── HOLD +kit-completeness ── fog +``` + +## Do not + +- Remint `#509` / `69-a` / `508-*` / `522-*` / leftover `Ⅰ`–`Ⅹ`. +- Mint leftover `Ⅺ` or `CRV-CP` as a Proofs claimId. +- Mint a GitHub child from this map. +- Implement silent-polygon-collapse in this letter. +- `/implement` ticket 32 while HOLD implement stands. +- Steal COMPOUNDCURVE ticket 30. +- Merge into JTS #7. Open a type-10 reader PR. Join GEO-TIN 15–17. +- Invent a DOI. Cite 19125-2. Copy clothoid Zenodo. +- Treat `WindingNumber.v : winding_decides_membership` as curve Jordan. +- Treat FCP-S I/O as overlay honesty. +- Flip F-CP / V-CP TRIAGE status. +- Set backlog priority. diff --git a/docs/scout/map-multicurve.md b/docs/scout/map-multicurve.md new file mode 100644 index 00000000..fbd8cf9b --- /dev/null +++ b/docs/scout/map-multicurve.md @@ -0,0 +1,178 @@ +# Map — MULTICURVE type honesty + +A wayfinder map. Charted 2026-09-01. This is **not** a `wayfinder:map` +GitHub issue, **not** a remint of `#509` / `69-a` / `508-*` / leftover +`Ⅰ`–`Ⅹ`, **not** COMPOUNDCURVE ticket 30, and **not** CURVEPOLYGON +ticket 32. It does **not** implement silent-MultiLineString +elimination. It does **not** mint a second MultiCurve type. It does +**not** merge into JTS #7. No dedicated board card; sibling WKB-8-12 +is I/O (type 11). + +> Architect SIGN 16 Aug 2026 on FCP-S / WKB-8-12: HOLD type I/O 13–17 +> / 18–20. Off #7 for anything not already landed. Do not mark pass. +> Cite 13249-3 for types 8–12 only. No invented DOI. **No SIGN lifts +> HOLD implement for this leftover.** Named linear fallback stays +> named. No GEO-TIN 15–17. No type-11 reader PR. No second MultiCurve +> type. No priority. + +topics: arc, wkt +claimId: none +witness: none + +## Destination + +**Name the silent MultiLineString-collapse leftover so the next +`/implement` cannot steal ticket 30, steal ticket 32, steal `#509`, +invent a Coq MultiCurve carrier as "already true", or treat I/O +round-trip as overlay honesty.** + +SQL/MM `ST_MultiCurve` (ISO/IEC 13249-3 §4.2.25; WKB type 11) is a +collection of ST_Curve members. Members need not be contiguous — that +is COMPOUNDCURVE (§4.2.13 / §7.10.1). The ask is honesty: a multicurve +stays a multicurve. Silent emit of `MULTILINESTRING` / `LineString[]` +chords for overlay, hull, or TestBuilder is a refuse. Named +`Linearize` / `toLinear` / `chord_approx_ring` is not that refuse. +JTS `MultiCurve` extending `MultiLineString` is the named Option-A +contract, not the leftover — `toLinear` is the named collapse to +`MultiLineString`. + +This letter does not retire a tracker and does not mint an epic. +Epic creation stays owner-scope. `#509` stays OPEN (Jordan is a +surface leftover; it is not this collection). + +## Three words that say "collapse" + +| Word | What it is | Park | Status | +|---|---|---|---| +| Silent MultiLineString collapse | Overlay / hull / TestBuilder eat `MULTICURVE` and emit `MULTILINESTRING` / `LineString[]` chords with no stamp; or treat the JTS `MultiLineString` supertype as if members were linearized | leftover **silent-multilinestring-collapse** | Named on GEOS OverlayNG. Ticket 34 closed. Distinct from ticket 30 (single compound Flatten) and ticket 32 (CURVEPOLYGON → POLYGON). | +| Named linear fallback | `Linearize` / `toLinear` / `chord_approx_ring` / OverlayNGCurve `APPROX` + `isApproximate()` | technique (named) | Allowed. JTS `MultiCurve.toLinear` returns `MultiLineString` and is named. Coq `CurveLinearise.v : chord_approx_ring_closed` is the named ring bridge, not a MultiCurve pin. | +| Collection / member list | Members stay ST_Curve; the collection is not a COMPOUNDCURVE splice | already named on the engine; **missing in Coq** | JTS type exists. NTS `OgcGeometryType.MultiCurve = 11`. Coq has `CurveGeometry.v : CurveSegment` (`CSChord` \| `CSArc`) as a *member* alphabet and no MultiCurve carrier. `CurveGeometry.v : valid_curve_geometry` is `list CurvePolygon` (F-MS-shaped). Do not cite it as MultiCurve. | + +I/O type identity is not op honesty. WKB-8-12 names type 11. GML +`MultiCurve` in NTS core `GMLReader.ReadMultiCurve` returns +`MultiLineString` — SFSQL/GML3 name, not SQL/MM `ST_MultiCurve`. +WKB/WKT may round-trip type 11 and still lie in overlay unless the +op carries a path stamp (sibling QG-CURVE-CHORD; HOLD implement; +does not join this leftover). + +## What is already true + +| Surface | Pin | Honesty | +|---|---|---| +| 60s reader | `docs/HELP.md` BIM Bea card; `docs/READING-GUIDE.md` | Names CIRCULARSTRING / COMPOUNDCURVE / CURVEPOLYGON. **Does not name MULTICURVE.** Name gap, not a drop of a type that was never on the card. | +| SQL/MM type | ISO/IEC 13249-3 §4.2.25; clause book §1 | Instantiable collection of ST_Curve. WKB 11 (`docs/iso13249-3-curve-type-bindings-2026-08.md` Table 15). Cite 13249-3, not 19125-2. | +| Member alphabet | `CurveGeometry.v : CurveSegment` | `CSChord` \| `CSArc`. A MultiCurve *member* may be those. The collection type is not in Coq. | +| Not a MultiCurve pin | `CurveGeometry.v : valid_curve_geometry` | `Forall valid_curve_polygon`. That is a list of curve polygons (F-MS-shaped), not ST_MultiCurve. | +| Named Option B bridge | `CurveLinearise.v : chord_approx_ring_closed` | Combinatorial faithfulness of the *named* linearise of a ring. Not silent MultiLineString emit. | +| Linear WKT/GeoJSON alphabet | `WktGeoJsonRoundtrip.v : wkt_geojson_wkt_roundtrip` | `GTMultiLineString` / `OgcMultiLineString` only. No MULTICURVE constructor. | +| Compound length additivity | `CurveLength.v : curve_length_additive` | Contiguous COMPOUNDCURVE member sum. Not a MultiCurve collection sum. Do not remint `508-*`. | +| Completeness fog | `OverlayTouchRow.v : phase0_relation_complete_hypothesis_refuted` | Kit-completeness stays fog. Same ancestor as the CURVEPOLYGON letter. | +| JTS Option A | `org.locationtech.jts.geom.curve.MultiCurve` | Extends `MultiLineString`. `toText` uses `CurveWKTWriter` (refuse flatten of members). `toLinear` is named. Ops route `CurveOps`. | +| NTS type code | `OgcGeometryType.MultiCurve = 11` | Enum exists on `develop`. Dedicated `MultiCurve.cs` is on the curve-foundation branch (clause book §1); this `develop` tree still returns a `GeometryCollection` of `Curve` from `CurvePolygon.Boundary` and calls a dedicated MultiCurve type "roadmap". | +| WKB-8-12 I/O | Notion WKB-8-12; type 11 | Writers must not call `toLinear`. Readers must emit first-class types. I/O identity, not op honesty. Off #7. | +| F-CP / F-MC / F-MS TRIAGE | `#64` residue / `#509` | Bundled row says "structural model exists". For MultiCurve that overclaims Coq. This letter does not flip the bundled row. | +| Rung-1 IsValid | clause book §6.2 | MultiCurve has no rung-1 override. Members fail-closed. Wiring is `615-h`-lane. Do not steal `615-h`. | + +## Leftover table + +Parks follow ADR-0002. Value and priority are orthogonal. This letter +does not set WSJF. + +| Id | Leftover | Kind | Park | Status | Do not | +|---|---|---|---|---|---| +| silent-multilinestring-collapse | Silent emit of `MULTILINESTRING` / `LineString[]` at overlay / hull / TestBuilder, or treating the `MultiLineString` supertype as linearized members | CRV-MC | technique | Named on GEOS OverlayNG (MULTICURVE ∪ POINT does not emit MULTILINESTRING). Ticket 34 closed. Coq still has no MultiCurve carrier. NTS/JTS leftover sites stay an engine grill. | steal ticket 30; steal ticket 32; steal `#509`; treat WKB-8-12 as overlay honesty; merge into JTS #7; mint a Coq MultiCurve carrier as this leftover; mint a second MultiCurve type | +| — | COMPOUNDCURVE flatten-elimination | CRV-CC / ticket 30 | technique | Sibling in this packet. Single contiguous compound. | steal ticket 30 for a MultiCurve site | +| — | CURVEPOLYGON silent POLYGON collapse | CRV-CP / ticket 32 | technique | Sibling in this packet. Surface type. | steal ticket 32 | +| — | F-MS / MULTISURFACE | sibling | sequencing | `CurveGeometry.v : valid_curve_geometry` is closer to this than to MultiCurve. Not this letter. | pull F-MS into CRV-MC; remint the bundled F-CP / F-MC / F-MS row as done | +| — | V-CP Jordan true-region | `#509` | technique | Surface leftover. Stays OPEN. | remint `#509`; pull Jordan into CRV-MC | +| — | Coq MultiCurve carrier | missing type | technique | Honest gap. Not a proof in this letter. HOLD implement stands. | invent `valid_multi_curve` and call ticket 33 done | +| — | HELP name gap | 60s reader | sequencing | Bea card does not name MULTICURVE. | treat a HELP edit as overlay honesty | +| — | GML3 `MultiCurve` → `MultiLineString` | NTS core I/O | sequencing | SFSQL/GML3 name. Not SQL/MM type 11. | open a type-11 reader PR to "fix" GML | +| — | WKB type-11 reader PR | I/O | sequencing | Type 11 is already named on #7 I/O 8–12. | open a reader-only PR from this letter | +| — | QG-CURVE-CHORD path stamp | sibling board card | sequencing | HOLD implement. Does not join this leftover. | invent EXACT / NAMED-APPROX / CHORD-PATH CI on this letter | +| — | MultiCurve IsValid rung-1 | `615-h` lane | sequencing | Clause book §6.2. | steal `615-h` | +| — | JTS #27 OverlayNG-for-circles | JTS #27 | sequencing | **Out.** | fold into this map; merge into #7 | +| — | JTS #38 package-private curve DCEL | JTS #38 | sequencing | Off #7 unless PO says merge. No public noder. | make the DCEL public | +| — | Second MultiCurve type | board HOLD | sequencing | The existing JTS / NTS-enum / clause-book carriers stay. | mint a parallel type; join GEO-TIN 15–17 | +| — | 3-D Multi* / GEO-TIN | sibling TIN card | sequencing | Do not confuse with WKB 11. HOLD implement. | join GEO-TIN 15–17 | + +## Decisions so far + +- MULTICURVE is SQL/MM ISO/IEC 13249-3, WKB 11. Cite that standard. + There is no DOI. Do not cite ISO 19125-2. +- A MultiCurve is a collection. A CompoundCurve is a contiguous splice. + They are different types. +- Bea 60s reader names CS / CC / CP and does not name MULTICURVE. + That is a name gap, not this leftover. +- Silent MultiLineString collapse is the one leftover this card owns. + It is not leftover `Ⅵ`, not `CRV-MC` as a Proofs claimId, not + `#509`, and not a new epic. +- Named linear fallback stays named. Silent MultiLineString emit is + a refuse. +- JTS `MultiCurve extends MultiLineString` is named Option A. + `toLinear` → `MultiLineString` is named. +- Coq has no MultiCurve carrier. `valid_curve_geometry` is not one. +- `#509` owns Jordan. F-CP / F-MC / F-MS TRIAGE rows do not flip. +- COMPOUNDCURVE ticket 30 and CURVEPOLYGON ticket 32 stay siblings. +- JTS #27 is out. JTS #38 stays off #7. No public noder. +- HOLD merge into #7. HOLD a second MultiCurve type. No priority + from this letter. +- `/implement 660` on GEOS named the leftover: OverlayNG keeps + MULTICURVE. Ticket 34 closed. See + [`closed/34-multicurve-silent-multilinestring-collapse.md`](tickets/closed/34-multicurve-silent-multilinestring-collapse.md). + +## Fog + +- **Which NTS / JTS overlay entry still emits MultiLineString without + a stamp** is an NTS/JTS engine leftover, not a Coq lemma. GEOS + OverlayNG already keeps MULTICURVE. +- **NTS `develop` has the enum and not the class.** The clause-book + path is the curve-foundation branch. Do not treat the missing + `.cs` file on `develop` as Bea dropping the type. +- **HELP still says `Flatten()`** while the NTS method is `Linearize`. + Name drift on CS / CC / CP. MULTICURVE was never on that card. +- **QG-CURVE-CHORD** stays a separate card. + +## Frontier + +Ticket 33 (this chart) is closed. Ticket 34 is closed on GEOS: +OverlayNG keeps MULTICURVE. Coq still has no MultiCurve carrier. +NTS/JTS overlay sites stay an engine grill. Next useful session +is an NTS or JTS letter, or stop. + +Sibling COMPOUNDCURVE tickets 29 / 30 live in this packet +(`map-compoundcurve.md`). Sibling CURVEPOLYGON tickets 31 / 32 +live in this packet (`map-curvepolygon.md`). Numbered 33 / 34 +so the leftovers stay distinct. + +``` +HELP / READING-GUIDE ════════════ CS / CC / CP named ── MULTICURVE absent +CurveSegment ══════════════════ member alphabet, not the collection +valid_curve_geometry ══════════ list CurvePolygon ── F-MS-shaped, not this +I/O type 11 / WKB-8-12 ════════ identity, not op honesty ── off #7 +JTS MultiCurve ════════════════ Option A + named toLinear +#509 V-CP Jordan ══════════════ surface ── stays OPEN +CRV-CC ticket 30 ══════════════ lineal Flatten ── sibling, closed on GEOS +CRV-CP ticket 32 ══════════════ POLYGON emit ── sibling, closed on GEOS + +silent-multilinestring-collapse ── ticket 34 closed on GEOS +#27 ── out +#38 ── Option C DCEL ── off #7 ── no public noder +second type / type-11 reader / GEO-TIN 15–17 ── HOLD +Coq MultiCurve carrier ── missing ── not this leftover +``` + +## Do not + +- Remint `#509` / `69-a` / `508-*` / `522-*` / leftover `Ⅰ`–`Ⅹ` / `615-h`. +- Mint leftover `Ⅺ` or `CRV-MC` as a Proofs claimId. +- Mint a GitHub child from this map. +- Implement silent-multilinestring-collapse in this letter. +- `/implement` ticket 34 while HOLD implement stands. +- Steal COMPOUNDCURVE ticket 30 or CURVEPOLYGON ticket 32. +- Cite `CurveGeometry.v : valid_curve_geometry` as a MultiCurve pin. +- Merge into JTS #7. Open a type-11 reader PR. Join GEO-TIN 15–17. +- Invent a DOI. Cite 19125-2. Copy clothoid Zenodo. +- Treat GML3 `MultiCurve` as SQL/MM type 11. +- Flip F-CP / F-MC / F-MS TRIAGE status. +- Set backlog priority. diff --git a/docs/scout/map-multisurface.md b/docs/scout/map-multisurface.md new file mode 100644 index 00000000..55e0ce47 --- /dev/null +++ b/docs/scout/map-multisurface.md @@ -0,0 +1,185 @@ +# Map — MULTISURFACE type honesty + +A wayfinder map. Charted 2026-09-01. This is **not** a `wayfinder:map` +GitHub issue, **not** a remint of `#509` / `69-a` / `508-*` / leftover +`Ⅰ`–`Ⅹ`, **not** COMPOUNDCURVE ticket 30, **not** CURVEPOLYGON ticket +32, and **not** MULTICURVE ticket 34. It does **not** implement +silent-MultiPolygon elimination. It does **not** mint a second +MultiSurface type. It does **not** merge into JTS #7. No dedicated +board card; sibling WKB-8-12 is I/O (type 12). + +> Architect SIGN 16 Aug 2026 on FCP-S / WKB-8-12: HOLD type I/O 13–17 +> / 18–20. Off #7 for anything not already landed. Do not mark pass. +> Cite 13249-3 for types 8–12 only. No invented DOI. **No SIGN lifts +> HOLD implement for this leftover.** Named linear fallback stays +> named. No GEO-TIN 15–17. No type-12 reader PR. No second MultiSurface +> type. No priority. + +topics: arc, wkt +claimId: none +witness: none + +## Destination + +**Name the silent MultiPolygon-collapse leftover so the next +`/implement` cannot steal ticket 32, steal ticket 34, steal `#509`, +treat `valid_curve_geometry` as overlay honesty, or treat I/O +round-trip as op honesty.** + +SQL/MM `ST_MultiSurface` (ISO/IEC 13249-3 §4.2.27; WKB type 12) is a +collection of ST_Surface members. Members may be ST_CurvePolygon / +ST_Polygon. The ask is honesty: a multisurface stays a multisurface. +Silent emit of `MULTIPOLYGON` / `Polygon[]` chords for overlay, hull, +or TestBuilder is a refuse. Named `Linearize` / `toLinear` / +`to_geometry` is not that refuse. JTS `MultiSurface` extending +`MultiPolygon` is the named Option-A contract, not the leftover — +`toLinear` is the named collapse to `MultiPolygon`. + +This letter does not retire a tracker and does not mint an epic. +Epic creation stays owner-scope. `#509` stays OPEN (Jordan is a +per-member true-region leftover; it is not this collection). + +## Three words that say "collapse" + +| Word | What it is | Park | Status | +|---|---|---|---| +| Silent MultiPolygon collapse | Overlay / hull / TestBuilder eat `MULTISURFACE` and emit `MULTIPOLYGON` / `Polygon[]` chords with no stamp; or treat the JTS `MultiPolygon` supertype as if members were linearized | leftover **silent-multipolygon-collapse** | Named on GEOS `restrictToSurfaces` (`hasCurvedTypes`). Ticket 36 closed. Distinct from ticket 32 (single CURVEPOLYGON → POLYGON) and ticket 34 (MULTICURVE → MULTILINESTRING). | +| Named linear fallback | `Linearize` / `toLinear` / `to_geometry` / `chord_approx_ring` / OverlayNGCurve `APPROX` + `isApproximate()` | technique (named) | Allowed. JTS `MultiSurface.toLinear` returns `MultiPolygon` and is named. Coq `CurveGeometry.v : to_geometry` maps `list CurvePolygon` to linear `Geometry`. `CurveLinearise.v : to_geometry_outer_ring_closed` is the named ring bridge. | +| Collection / member list | Members stay ST_Surface / CurvePolygon; the collection is not one CurvePolygon | already landed (structural) | Coq `CurveGeometry.v : valid_curve_geometry` is `Forall valid_curve_polygon` on `list CurvePolygon`. Nil/cons: `CurveGeometry.v : valid_curve_geometry_nil` / `CurveGeometry.v : valid_curve_geometry_cons`. Structural only. Not Jordan. Not overlay honesty. | + +I/O type identity is not op honesty. WKB-8-12 names type 12. GML +`MultiSurface` in NTS core `GMLReader.ReadMultiSurface` returns +`MultiPolygon` — SFSQL/GML3 name, not SQL/MM `ST_MultiSurface`. +JTS curve README notes a written `MULTISURFACE(CURVEPOLYGON(…))` can +re-read as `MultiSurface[Polygon]` because inner-member tags are not +yet emitted — I/O member-tag degrade, sibling of WKB-8-12, not this +leftover. Do not cite ISO 19125-2 (a JTS test file comment does; this +corpus cites 13249-3 only). + +## What is already true + +| Surface | Pin | Honesty | +|---|---|---| +| 60s reader | `docs/HELP.md` BIM Bea card; `docs/READING-GUIDE.md` | Names CIRCULARSTRING / COMPOUNDCURVE / CURVEPOLYGON. **Does not name MULTISURFACE.** Name gap, not a drop. | +| SQL/MM type | ISO/IEC 13249-3 §4.2.27; clause book §1 | Instantiable collection of ST_Surface. WKB 12 (`docs/iso13249-3-curve-type-bindings-2026-08.md` Table 15). Cite 13249-3, not 19125-2. | +| Structural collection | `CurveGeometry.v : valid_curve_geometry` | `list CurvePolygon`. This is the F-MS-shaped Coq carrier the MULTICURVE letter refused to steal. Structural `Forall` only. | +| Nil / cons | `CurveGeometry.v : valid_curve_geometry_nil` / `CurveGeometry.v : valid_curve_geometry_cons` | Empty collection and cons of a valid member. Not overlay honesty. | +| Member structural | `CurveGeometry.v : valid_curve_polygon` | Each member is a structural CurvePolygon. True-region waits on `#509`. | +| Named collection linearise | `CurveGeometry.v : to_geometry` | Option B map of every member ring to a linear `Geometry`. Named. Not silent MULTIPOLYGON emit. | +| Named ring linearise | `CurveLinearise.v : to_geometry_outer_ring_closed` | Combinatorial faithfulness of the *named* linearise of one outer ring. | +| Linear WKT/GeoJSON alphabet | `WktGeoJsonRoundtrip.v : wkt_geojson_wkt_roundtrip` | `GTMultiPolygon` / `OgcMultiPolygon` only. No MULTISURFACE constructor. | +| Completeness fog | `OverlayTouchRow.v : phase0_relation_complete_hypothesis_refuted` | Kit-completeness stays fog. CUP/CAP/XOR/SUB + T-in/T-out is not this leftover. | +| JTS Option A | `org.locationtech.jts.geom.curve.MultiSurface` | Extends `MultiPolygon`. `toText` uses `CurveWKTWriter` (refuse flatten of members). `toLinear` is named. Ops route `CurveOps`. OverlayNGCurve may return an exact `MultiSurface` of operands (disjoint CUP / XOR) — named exact collection, not collapse. | +| NTS type code | `OgcGeometryType.MultiSurface = 12` | Enum exists on `develop`. Dedicated `MultiSurface.cs` is on the curve-foundation branch (clause book §1). | +| WKB-8-12 I/O | Notion WKB-8-12; type 12 | Writers must not call `toLinear`. Readers must emit first-class types. I/O identity, not op honesty. Off #7. | +| F-CP / F-MC / F-MS TRIAGE | `#64` residue / `#509` | Bundled row says "structural model exists; true-region deferred". Structural collection is this pin. Jordan stays on `#509`. This letter does not flip the bundled row. | +| Rung-1 IsValid | clause book §6.2 | MultiSurface has no rung-1 override. Members fail-closed. Wiring is `615-h`-lane. Do not steal `615-h`. | + +## Leftover table + +Parks follow ADR-0002. Value and priority are orthogonal. This letter +does not set WSJF. + +| Id | Leftover | Kind | Park | Status | Do not | +|---|---|---|---|---|---| +| silent-multipolygon-collapse | Silent emit of `MULTIPOLYGON` / `Polygon[]` at overlay / hull / TestBuilder, or treating the `MultiPolygon` supertype as linearized members | CRV-MS | technique | Named on GEOS `CascadedPolygonUnion::restrictToSurfaces` (`hasCurvedTypes`, not `hasCurvedComponents`). Ticket 36 closed. OverlayNG already kept MULTISURFACE. NTS/JTS leftover sites stay an engine grill. | steal ticket 32; steal ticket 34; steal `#509`; treat `to_geometry` / WKB-8-12 as overlay honesty; merge into JTS #7; mint a second MultiSurface type | +| — | CURVEPOLYGON silent POLYGON collapse | CRV-CP / ticket 32 | technique | Sibling in this packet. One surface. | steal ticket 32 for a MultiSurface site | +| — | MULTICURVE silent MultiLineString collapse | CRV-MC / ticket 34 | technique | Sibling in this packet. Lineal collection. | steal ticket 34 | +| — | COMPOUNDCURVE flatten-elimination | CRV-CC / ticket 30 | technique | Sibling in this packet. Single contiguous compound. | steal ticket 30 | +| — | V-CP Jordan true-region | `#509` | technique | Per-member true-region. Stays OPEN. | remint `#509`; pull Jordan into CRV-MS | +| — | I/O member-tag degrade | WKB-8-12 / JTS README | sequencing | Written `MULTISURFACE(CURVEPOLYGON(…))` can re-read as `MultiSurface[Polygon]`. I/O, not overlay. | open a type-12 reader PR from this letter | +| — | GML3 `MultiSurface` → `MultiPolygon` | NTS core I/O | sequencing | SFSQL/GML3 name. Not SQL/MM type 12. | treat GML as this leftover | +| — | HELP name gap | 60s reader | sequencing | Bea card does not name MULTISURFACE. | treat a HELP edit as overlay honesty | +| — | Kit-completeness (CUP/CAP/XOR/SUB + T-in/T-out) | fog | research | OverlayNGCurve already names some exact MultiSurface cells. Completeness has a refuted ancestor. | mint a completeness epic | +| — | QG-CURVE-CHORD path stamp | sibling board card | sequencing | HOLD implement. Does not join this leftover. | invent EXACT / NAMED-APPROX / CHORD-PATH CI on this letter | +| — | MultiSurface IsValid rung-1 | `615-h` lane | sequencing | Clause book §6.2. | steal `615-h` | +| — | JTS #27 OverlayNG-for-circles | JTS #27 | sequencing | **Out.** | fold into this map; merge into #7 | +| — | JTS #38 package-private curve DCEL | JTS #38 | sequencing | Off #7 unless PO says merge. No public noder. | make the DCEL public | +| — | Second MultiSurface type | board HOLD | sequencing | The existing JTS / NTS-enum / Coq `CurveGeometry` carriers stay. | mint a parallel type; join GEO-TIN 15–17 | +| — | 3-D Multi* / GEO-TIN / PRF-TIN15 | sibling TIN cards | sequencing | Types 15–17 are not type 12. HOLD implement. | join GEO-TIN 15–17 | + +## Decisions so far + +- MULTISURFACE is SQL/MM ISO/IEC 13249-3, WKB 12. Cite that standard. + There is no DOI. Do not cite ISO 19125-2. +- A MultiSurface is a collection of surfaces. A CurvePolygon is one + surface. They are different types. +- Bea 60s reader names CS / CC / CP and does not name MULTISURFACE. + That is a name gap, not this leftover. +- Silent MultiPolygon collapse is the one leftover this card owns. + It is not leftover `Ⅵ`, not `CRV-MS` as a Proofs claimId, not + `#509`, and not a new epic. +- Named linear fallback stays named. Silent MultiPolygon emit is a + refuse. +- JTS `MultiSurface extends MultiPolygon` is named Option A. + `toLinear` → `MultiPolygon` is named. +- `CurveGeometry.v : valid_curve_geometry` is the structural + collection pin. `to_geometry` is the named linearise of that + collection. Neither is overlay honesty. +- `#509` owns Jordan. F-CP / F-MC / F-MS TRIAGE rows do not flip. +- Tickets 30 / 32 / 34 stay siblings. +- JTS #27 is out. JTS #38 stays off #7. No public noder. +- HOLD merge into #7. HOLD a second MultiSurface type. No priority + from this letter. +- `/implement 660` on GEOS named the leftover: + `CascadedPolygonUnion::restrictToSurfaces` now checks + `hasCurvedTypes()`. Ticket 36 closed. See + [`closed/36-multisurface-silent-multipolygon-collapse.md`](tickets/closed/36-multisurface-silent-multipolygon-collapse.md). + +## Fog + +- **Which NTS / JTS overlay entry still emits MultiPolygon without a + stamp** is an NTS/JTS engine leftover, not a Coq lemma. GEOS + OverlayNG already keeps MULTISURFACE; + `restrictToSurfaces` now keeps all-linear CurvePolygon members. + OverlayNGCurve already has named exact MultiSurface cells; unnamed + cells still densify. +- **NTS `develop` has the enum and not the class.** The clause-book + path is the curve-foundation branch. +- **HELP still says `Flatten()`** while the NTS method is `Linearize`. + Name drift on CS / CC / CP. MULTISURFACE was never on that card. +- **QG-CURVE-CHORD** stays a separate card. + +## Frontier + +Ticket 35 (this chart) is closed. Ticket 36 is closed on GEOS: +`restrictToSurfaces` checks `hasCurvedTypes()`. NTS/JTS overlay +sites stay an engine grill. Next useful session is an NTS or JTS +letter, or stop. + +Sibling COMPOUNDCURVE tickets 29 / 30 live in this packet +(`map-compoundcurve.md`). Sibling CURVEPOLYGON tickets 31 / 32 +live in this packet (`map-curvepolygon.md`). Sibling MULTICURVE +tickets 33 / 34 live in this packet (`map-multicurve.md`). +Numbered 35 / 36 so the leftovers stay distinct. + +``` +HELP / READING-GUIDE ════════════ CS / CC / CP named ── MULTISURFACE absent +valid_curve_geometry ══════════ list CurvePolygon ── structural F-MS +to_geometry ══════════════════ named collection linearise ── not this leftover +I/O type 12 / WKB-8-12 ════════ identity, not op honesty ── off #7 +JTS MultiSurface ══════════════ Option A + named toLinear +#509 V-CP Jordan ══════════════ per-member true-region ── stays OPEN +CRV-CP ticket 32 ══════════════ one-surface POLYGON emit ── sibling, closed on GEOS +CRV-MC ticket 34 ══════════════ lineal MULTILINESTRING emit ── sibling, closed on GEOS + +silent-multipolygon-collapse ── ticket 36 closed on GEOS +#27 ── out +#38 ── Option C DCEL ── off #7 ── no public noder +second type / type-12 reader / GEO-TIN 15–17 ── HOLD +``` + +## Do not + +- Remint `#509` / `69-a` / `508-*` / `522-*` / leftover `Ⅰ`–`Ⅹ` / `615-h`. +- Mint leftover `Ⅺ` or `CRV-MS` as a Proofs claimId. +- Mint a GitHub child from this map. +- Implement silent-multipolygon-collapse in this letter. +- `/implement` ticket 36 while HOLD implement stands. +- Steal tickets 30 / 32 / 34. +- Treat `CurveGeometry.v : to_geometry` as silent collapse. +- Merge into JTS #7. Open a type-12 reader PR. Join GEO-TIN 15–17. +- Invent a DOI. Cite 19125-2. Copy clothoid Zenodo. +- Treat GML3 `MultiSurface` as SQL/MM type 12. +- Flip F-CP / F-MC / F-MS TRIAGE status. +- Set backlog priority. diff --git a/docs/scout/tickets/README.md b/docs/scout/tickets/README.md index ce19048b..9fa428e0 100644 --- a/docs/scout/tickets/README.md +++ b/docs/scout/tickets/README.md @@ -27,6 +27,16 @@ Order of work: top-down from #64, with the freebie first. | 08 | ~~[Retire #68 — Delaunay triangulation and Voronoi diagrams](closed/08-retire-68-delaunay-voronoi.md)~~ **closed** → #525 (global tier), #526 | grilling | — | | 09 | ~~[End #69's umbrella role and re-parent the standing epics](closed/09-end-69-umbrella.md)~~ **closed** → [`69-closing-summary.md`](../69-closing-summary.md); no replacement umbrella | grilling | 11 (04–08 all closed) | | 10 | [Resync surviving issue bodies to corpus state](10-resync-surviving-bodies.md) | task | **#506 queue empty** · 09 done | +| 29 | ~~[Chart COMPOUNDCURVE flatten-elimination](closed/29-compoundcurve-flatten-chart.md)~~ **closed** → [`map-compoundcurve.md`](../map-compoundcurve.md) | grilling | — | +| 30 | ~~[Flatten-elimination — silent COMPOUNDCURVE chord path](closed/30-compoundcurve-flatten-elimination.md)~~ **closed** → GEOS `ensureNoCurvedComponents` + `getLinearized` | implement | 29 | +| 31 | ~~[Chart CURVEPOLYGON type honesty](closed/31-curvepolygon-type-chart.md)~~ **closed** → [`map-curvepolygon.md`](../map-curvepolygon.md) | grilling | — | +| 32 | ~~[Silent POLYGON collapse — CURVEPOLYGON type honesty](closed/32-curvepolygon-silent-polygon-collapse.md)~~ **closed** → GEOS OverlayNG + `createSurface` | implement | 31 | +| 33 | ~~[Chart MULTICURVE type honesty](closed/33-multicurve-type-chart.md)~~ **closed** → [`map-multicurve.md`](../map-multicurve.md) | grilling | — | +| 34 | ~~[Silent MultiLineString collapse — MULTICURVE type honesty](closed/34-multicurve-silent-multilinestring-collapse.md)~~ **closed** → GEOS OverlayNG | implement | 33 | +| 35 | ~~[Chart MULTISURFACE type honesty](closed/35-multisurface-type-chart.md)~~ **closed** → [`map-multisurface.md`](../map-multisurface.md) | grilling | — | +| 36 | ~~[Silent MultiPolygon collapse — MULTISURFACE type honesty](closed/36-multisurface-silent-multipolygon-collapse.md)~~ **closed** → GEOS `restrictToSurfaces` | implement | 35 | +| 37 | ~~[SQL/MM WKT oracle — CLOTHOID / CIRCLE / GEODESICSTRING / NURBSCURVE / SPIRALCURVE](closed/37-sqlmm-wkt-oracle.md)~~ **closed** → oracle `SQLMM_WKT` | implement | 30 / 32 / 34 / 36 | +| 38 | ~~[NTS WKT named refuse for §4.2.1 curve types](closed/38-nts-sqlmm-named-refuse.md)~~ **closed** → NTS `WKTReader` named refuse | implement | 37 | ``` 01 ══════════════════════════════════════ closed 2026-08-22 (#482) @@ -45,7 +55,20 @@ Order of work: top-down from #64, with the freebie first. (69-closing-summary.md) ``` -**Related living maps.** The #522 children (bar 1 → bar 2) have their own +**Related living maps.** SQL/MM type-honesty packet (one PR; four maps): +COMPOUNDCURVE [`map-compoundcurve.md`](../map-compoundcurve.md) (tickets 29 / 30; 30 closed on GEOS), +CURVEPOLYGON [`map-curvepolygon.md`](../map-curvepolygon.md) (tickets 31 / 32; 32 closed on GEOS), +MULTICURVE [`map-multicurve.md`](../map-multicurve.md) (tickets 33 / 34; 34 closed on GEOS), +MULTISURFACE [`map-multisurface.md`](../map-multisurface.md) (tickets 35 / 36; 36 closed on GEOS). +Do not remint `#509`. Off JTS #7. Do not steal across leftovers. NTS/JTS leftover sites stay an engine grill. +ST_Clothoid / ST_Circle / ST_GeodesicString / ST_NURBSCurve / ST_SpiralCurve +are instantiable in ISO/IEC 13249-3 §4.2.1 — not optional extras. GEOS WKT +refuses them as SQL/MM types. Oracle mode `SQLMM_WKT` parses type identity +(ticket 37; SPIRALTYPE open-set lexer deviation in the clause-book §8). +NTS WKT names them and refuses (ticket 38), matching GEOS. Do not remint +`508-*`. Not leftover `Ⅺ`. + +The #522 children (bar 1 → bar 2) have their own frontier: [`docs/scout/map-522.md`](../map-522.md). Wrap-up leftovers: [`docs/scout/map-522-leftovers.md`](../map-522-leftovers.md). `/wayfinder 522 leftovers` refreshes the leftovers chart. Leftover `Ⅰ` is the mutual vertex-in-open-edge sliver. Leftover `Ⅱ` is @@ -72,6 +95,16 @@ on the #506 queue. Ticket 523 stays open, not accepted. | 11 · second pass at #67 | closed: overtaken | | 09 · end #69's umbrella | closed — owner-retire packet written; GitHub object stays for owner review | | 10 · resync surviving bodies | #506's split queue emptying | +| 29 · COMPOUNDCURVE chart | closed — [`map-compoundcurve.md`](../map-compoundcurve.md) | +| 30 · flatten-elimination | closed on GEOS — `ensureNoCurvedComponents` refuse + `getLinearized` | +| 31 · CURVEPOLYGON chart | closed — [`map-curvepolygon.md`](../map-curvepolygon.md) | +| 32 · silent-polygon-collapse | closed on GEOS — OverlayNG + `createSurface` | +| 33 · MULTICURVE chart | closed — [`map-multicurve.md`](../map-multicurve.md) | +| 34 · silent-multilinestring-collapse | closed on GEOS — OverlayNG | +| 35 · MULTISURFACE chart | closed — [`map-multisurface.md`](../map-multisurface.md) | +| 36 · silent-multipolygon-collapse | closed on GEOS — `restrictToSurfaces` `hasCurvedTypes` | +| 37 · SQLMM_WKT oracle | closed — `oracle/sqlmm_wkt.ml` | +| 38 · NTS named refuse | closed on NTS — `WKTReader` names §4.2.1 types and refuses | The next useful session on this map is not another wayfinder letter. Owner review of [`69-closing-summary.md`](../69-closing-summary.md) diff --git a/docs/scout/tickets/closed/29-compoundcurve-flatten-chart.md b/docs/scout/tickets/closed/29-compoundcurve-flatten-chart.md new file mode 100644 index 00000000..0f88bce9 --- /dev/null +++ b/docs/scout/tickets/closed/29-compoundcurve-flatten-chart.md @@ -0,0 +1,41 @@ +# Chart COMPOUNDCURVE flatten-elimination + +**Type:** grilling · **Map:** [COMPOUNDCURVE](../../map-compoundcurve.md) +**Claimed:** wayfinder 2026-09-01 · **Closed:** 2026-09-01 +**Blocked by:** — +**claimId:** none · **GitHub:** none · **witness:** none + +Board card: Notion CRV-CC. + +## Question + +What does `/wayfinder COMPOUNDCURVE` own? The board lifted HOLD +implement for flatten-elimination only. Name what is already true, +park what is HOLD, and leave one takeable leftover so the next +`/implement` cannot steal a closed letter or invent a second type. + +## Resolution + +**Grilled 2026-09-01. Living record: +[`docs/scout/map-compoundcurve.md`](../../map-compoundcurve.md).** +This ticket does not implement flatten-elimination. + +**Already true.** HELP and READING-GUIDE name COMPOUNDCURVE (ISO/IEC +13249-3) and that Flatten-to-chords is lossy. The Coq carrier is +`CurveGeometry.v`. Named linearise is +`CurveLinearise.v : chord_approx_ring_closed`. CompoundCurve is not +the PR #8 CurveExact cell +(`HullExactExtrema.v : h_cc_still_densify`) — H-CC stays on #424. +LEC member flatten is `LECFlattenRow.v : empty_disk_flatten_iff`. +Koc files are railway alignment, not SQL/MM. + +**Three words.** Silent chord Flatten is the leftover. Named +`Linearize` / `toLinear` / `chord_approx_ring` is allowed. Member / +splice flatten is already landed (`615-b` nested-CC splice is +§7.10.1). + +**Parks.** JTS #27 out. JTS #38 (Option C DCEL) off #7. No public +noder. HOLD merge into #7. HOLD a second CompoundCurve type. No +type-9 reader PR. No GEO-TIN 15–17. No DOI. Cite 13249-3 only. + +**Frontier.** Ticket 30 is the one takeable implement leftover. diff --git a/docs/scout/tickets/closed/30-compoundcurve-flatten-elimination.md b/docs/scout/tickets/closed/30-compoundcurve-flatten-elimination.md new file mode 100644 index 00000000..dd8d3b34 --- /dev/null +++ b/docs/scout/tickets/closed/30-compoundcurve-flatten-elimination.md @@ -0,0 +1,61 @@ +# Flatten-elimination — silent COMPOUNDCURVE chord path + +**Type:** implement · **Map:** [COMPOUNDCURVE](../../map-compoundcurve.md) +**Claimed:** implement 2026-09-01 · **Closed:** 2026-09-01 (GEOS named the leftover) +**Blocked by:** ~~[Chart COMPOUNDCURVE flatten-elimination](29-compoundcurve-flatten-chart.md)~~ ✔ +**claimId:** none · **GitHub:** none · **witness:** none + +Board card: Notion CRV-CC. Architect SIGN lifted HOLD implement for +**this leftover only**. + +## Ask + +Name or refuse the silent chord path that still eats +`COMPOUNDCURVE` at overlay, hull, or TestBuilder without a stamp. +A compound stays a compound. Named `Linearize` / `toLinear` / +`chord_approx_ring` / OverlayNGCurve `APPROX` + `isApproximate()` +stays named. I/O type identity is not op honesty. + +Cite ISO/IEC 13249-3. No DOI. No 19125-2. + +## In scope + +- Engine grill: NTS overlay / hull / TestBuilder sites that still + consume `CompoundCurve` as `Coordinate[]` without calling + `Linearize`. JTS OverlayNGCurve cells that densify with + `isApproximate()=false`. +- One Proofs honesty pin **only if** it is a new statement. Do not + remint `HullExactExtrema.v : h_cc_still_densify`. +- Keep the result type named (COMPOUNDCURVE vs LineString of chords). + +## Out of scope + +- Merge into JTS #7. Type-9 reader PR. GEO-TIN 15–17. +- A second CompoundCurve type. Public noder. JTS #27. JTS #38. +- H-CC hull (`424-b` / #424 / JTS #6). QG-CURVE-CHORD path-stamp CI. +- Remint `615-b`, `LECFlattenRow.v : empty_disk_flatten_iff`, + `508-*`, leftover `Ⅰ`–`Ⅹ`, `69-a`. +- Koc railway compound. Setting WSJF. + +## Done when + +A later `/implement` can point at one named site (engine or Coq) +and say whether it refused or stamped. This ticket stays open until +that letter lands. Do not mint `CRV-CC` as a Proofs claimId unless +that letter names a new lemma. + +## Resolution + +**Implemented 2026-09-01 on GEOS** (`cursor/sqlmm-type-honesty-ccfa`). + +Named site: `geos::util::ensureNoCurvedComponents` (hull / centroid / +buffer / …). It **refuses** a `COMPOUNDCURVE` with curved components +and names `getLinearized` as the only allowed linear fallback. + +GEOS OverlayNG already keeps `COMPOUNDCURVE` / `CIRCULARSTRING` when +`CurveToLineParams` is unset. C API overlay does not flatten just +because those params are registered. + +H-CC exact hull stays on tracker 424 +(`HullExactExtrema.v : h_cc_still_densify`). No new Coq lemma. +claimId: none. witness: none. diff --git a/docs/scout/tickets/closed/31-curvepolygon-type-chart.md b/docs/scout/tickets/closed/31-curvepolygon-type-chart.md new file mode 100644 index 00000000..2335e44a --- /dev/null +++ b/docs/scout/tickets/closed/31-curvepolygon-type-chart.md @@ -0,0 +1,41 @@ +# Chart CURVEPOLYGON type honesty + +**Type:** grilling · **Map:** [CURVEPOLYGON](../../map-curvepolygon.md) +**Claimed:** wayfinder 2026-09-01 · **Closed:** 2026-09-01 +**Blocked by:** — +**claimId:** none · **GitHub:** none · **witness:** none + +No dedicated board card. Sibling FCP-S is I/O. Sibling CRV-CC is +COMPOUNDCURVE flatten-elimination (this packet; tickets 29 / 30). + +## Question + +What does `/wayfinder CURVEPOLYGON` own? Name what is already true, +park what is HOLD, and leave one named leftover so the next session +cannot steal `#509`, steal ticket 30, or invent a second type. + +## Resolution + +**Grilled 2026-09-01. Living record: +[`docs/scout/map-curvepolygon.md`](../../map-curvepolygon.md).** +This ticket does not implement silent-polygon-collapse. + +**Already true.** HELP and READING-GUIDE name CURVEPOLYGON (ISO/IEC +13249-3) and that Flatten-to-chords is lossy. The Coq carrier is +`CurveGeometry.v : valid_curve_polygon` (structural). Named linearise +is `CurveLinearise.v : to_geometry_outer_ring_closed`. NTS rings stay +`Curve`. JTS `getExteriorRing()` is named Option A; the true shell is +`getExteriorCurve()`. V-CP Jordan stays on `#509`. Kit-completeness +stays fog (`OverlayTouchRow.v : phase0_relation_complete_hypothesis_refuted`). + +**Three words.** Silent POLYGON collapse is the leftover. Named +`Linearize` / `toLinear` / `chord_approx_ring` is allowed. Structural +F-CP / Jordan true-region is already named (`#509`). + +**Parks.** JTS #27 out. JTS #38 (Option C DCEL) off #7. No public +noder. HOLD merge into #7. HOLD a second CurvePolygon type. HOLD +implement for ticket 32 (no Architect SIGN). No type-10 reader PR. +No GEO-TIN 15–17. No DOI. Cite 13249-3 only. + +**Frontier.** Ticket 32 names the leftover. HOLD implement stands. +Do not `/implement` from this letter. diff --git a/docs/scout/tickets/closed/32-curvepolygon-silent-polygon-collapse.md b/docs/scout/tickets/closed/32-curvepolygon-silent-polygon-collapse.md new file mode 100644 index 00000000..bd841003 --- /dev/null +++ b/docs/scout/tickets/closed/32-curvepolygon-silent-polygon-collapse.md @@ -0,0 +1,67 @@ +# Silent POLYGON collapse — CURVEPOLYGON type honesty + +**Type:** implement · **Map:** [CURVEPOLYGON](../../map-curvepolygon.md) +**Claimed:** implement 2026-09-01 · **Closed:** 2026-09-01 (GEOS named the leftover) +**Blocked by:** ~~[Chart CURVEPOLYGON type honesty](31-curvepolygon-type-chart.md)~~ ✔ +**claimId:** none · **GitHub:** none · **witness:** none + +HOLD implement stood until `/implement 660` on GEOS. +Sibling COMPOUNDCURVE ticket 30 (this packet) is lineal Flatten, not this. + +## Ask + +Name or refuse the silent path that still eats `CURVEPOLYGON` at +overlay, hull, or TestBuilder and emits `POLYGON` / `LinearRing` +without a stamp, or treats JTS `getExteriorRing()` as the curve. +A curve polygon stays a curve polygon. Named `Linearize` / `toLinear` +/ `chord_approx_ring` / OverlayNGCurve `APPROX` + `isApproximate()` +stays named. I/O type identity is not op honesty. + +Cite ISO/IEC 13249-3. No DOI. No 19125-2. + +Do not start this ticket until Architect SIGN lifts HOLD implement. + +## In scope + +- Engine grill: NTS overlay / hull / TestBuilder sites that still + consume `CurvePolygon` and emit `Polygon` / `LinearRing` without + calling `Linearize`. JTS OverlayNGCurve cells that densify with + `isApproximate()=false`, or that hand `getExteriorRing()` to a + caller as if it were `getExteriorCurve()`. +- One Proofs honesty pin **only if** it is a new statement. Do not + remint `CurveGeometry.v : valid_curve_polygon`, + `CurveLinearise.v : to_geometry_outer_ring_closed`, or + `WindingNumber.v : winding_decides_membership`. +- Keep the result type named (CURVEPOLYGON vs POLYGON of chords). + +## Out of scope + +- Merge into JTS #7. Type-10 reader PR. GEO-TIN 15–17. +- A second CurvePolygon type. Public noder. JTS #27. JTS #38. +- `#509` Jordan true-region. FCP-S WKT shell. QG-CURVE-CHORD path-stamp CI. +- COMPOUNDCURVE ticket 30 / flatten-elimination. +- Remint `69-a`, `508-*`, leftover `Ⅰ`–`Ⅹ`. +- Kit-completeness (CUP/CAP/XOR/SUB + T-in/T-out). +- Setting WSJF. + +## Done when + +A later `/implement`, **after** Architect SIGN, can point at one named +site (engine or Coq) and say whether it refused or stamped. This ticket +stays open until that letter lands. Do not mint `CRV-CP` as a Proofs +claimId unless that letter names a new lemma. + +## Resolution + +**Implemented 2026-09-01 on GEOS** after `/implement 660` SIGN. + +Named site: GEOS OverlayNG + C API overlay. A `CURVEPOLYGON` stays a +`CURVEPOLYGON` (including all-linear LineString rings via +`GeometryFactory::createSurface`). Silent `POLYGON` emit is a refuse +unless the caller used `getLinearized`. + +`getExteriorRing()` on GEOS `Surface` is already `Curve*`, not a +`LinearRing` collapse. + +Jordan stays on tracker 509. F-CP / V-CP TRIAGE rows do not flip. +No new Coq lemma. claimId: none. witness: none. diff --git a/docs/scout/tickets/closed/33-multicurve-type-chart.md b/docs/scout/tickets/closed/33-multicurve-type-chart.md new file mode 100644 index 00000000..66a3ce10 --- /dev/null +++ b/docs/scout/tickets/closed/33-multicurve-type-chart.md @@ -0,0 +1,46 @@ +# Chart MULTICURVE type honesty + +**Type:** grilling · **Map:** [MULTICURVE](../../map-multicurve.md) +**Claimed:** wayfinder 2026-09-01 · **Closed:** 2026-09-01 +**Blocked by:** — +**claimId:** none · **GitHub:** none · **witness:** none + +No dedicated board card. Sibling WKB-8-12 is I/O (type 11). Sibling +CRV-CC is COMPOUNDCURVE flatten-elimination (this packet; tickets 29 / 30). +Sibling CRV-CP is CURVEPOLYGON silent POLYGON collapse (this packet; +tickets 31 / 32). + +## Question + +What does `/wayfinder MULTICURVE` own? Name what is already true, +park what is HOLD, and leave one named leftover so the next session +cannot steal ticket 30, steal ticket 32, steal `#509`, or invent a +Coq MultiCurve carrier as already true. + +## Resolution + +**Grilled 2026-09-01. Living record: +[`docs/scout/map-multicurve.md`](../../map-multicurve.md).** +This ticket does not implement silent-multilinestring-collapse. + +**Already true.** SQL/MM `ST_MultiCurve` is ISO/IEC 13249-3 §4.2.25, +WKB 11. JTS has Option A (`MultiCurve extends MultiLineString`) and +named `toLinear`. NTS has `OgcGeometryType.MultiCurve = 11`. Coq +member alphabet is `CurveGeometry.v : CurveSegment`. Named linearise +is `CurveLinearise.v : chord_approx_ring_closed`. Linear WKT/GeoJSON +is `WktGeoJsonRoundtrip.v : wkt_geojson_wkt_roundtrip` (no MULTICURVE +constructor). `CurveGeometry.v : valid_curve_geometry` is a list of +curve polygons — not MultiCurve. HELP names CS / CC / CP and does +not name MULTICURVE. + +**Three words.** Silent MultiLineString collapse is the leftover. +Named `Linearize` / `toLinear` / `chord_approx_ring` is allowed. +Collection / member list is named on the engine and missing in Coq. + +**Parks.** JTS #27 out. JTS #38 off #7. No public noder. HOLD merge +into #7. HOLD a second MultiCurve type. HOLD implement for ticket 34 +(no Architect SIGN). No type-11 reader PR. No GEO-TIN 15–17. No DOI. +Cite 13249-3 only. Do not steal `615-h`. Do not remint `#509`. + +**Frontier.** Ticket 34 names the leftover. HOLD implement stands. +Do not `/implement` from this letter. diff --git a/docs/scout/tickets/closed/34-multicurve-silent-multilinestring-collapse.md b/docs/scout/tickets/closed/34-multicurve-silent-multilinestring-collapse.md new file mode 100644 index 00000000..0be3ff4f --- /dev/null +++ b/docs/scout/tickets/closed/34-multicurve-silent-multilinestring-collapse.md @@ -0,0 +1,72 @@ +# Silent MultiLineString collapse — MULTICURVE type honesty + +**Type:** implement · **Map:** [MULTICURVE](../../map-multicurve.md) +**Claimed:** implement 2026-09-01 · **Closed:** 2026-09-01 (GEOS named the leftover) +**Blocked by:** ~~[Chart MULTICURVE type honesty](33-multicurve-type-chart.md)~~ ✔ +**claimId:** none · **GitHub:** none · **witness:** none + +HOLD implement stood until `/implement 660` on GEOS. +Sibling COMPOUNDCURVE ticket 30 (this packet) is lineal Flatten, not this. +Sibling CURVEPOLYGON ticket 32 (this packet) is POLYGON emit, not this. + +## Ask + +Name or refuse the silent path that still eats `MULTICURVE` at +overlay, hull, or TestBuilder and emits `MULTILINESTRING` / +`LineString[]` without a stamp, or treats the JTS `MultiLineString` +supertype as linearized members. A multicurve stays a multicurve. +Named `Linearize` / `toLinear` / `chord_approx_ring` / OverlayNGCurve +`APPROX` + `isApproximate()` stays named. I/O type identity is not +op honesty. + +Cite ISO/IEC 13249-3. No DOI. No 19125-2. + +Do not start this ticket until Architect SIGN lifts HOLD implement. + +## In scope + +- Engine grill: NTS overlay / hull / TestBuilder sites that still + consume `MultiCurve` (or WKB type 11) and emit `MultiLineString` + without calling `Linearize` / `toLinear`. JTS OverlayNGCurve cells + that densify with `isApproximate()=false`, or that hand a + `MultiLineString` view to a caller as if it were the curve + collection. +- One Proofs honesty pin **only if** it is a new statement. Do not + remint `CurveGeometry.v : CurveSegment`, + `CurveGeometry.v : valid_curve_geometry`, + `CurveLinearise.v : chord_approx_ring_closed`, + `WktGeoJsonRoundtrip.v : wkt_geojson_wkt_roundtrip`, or + `CurveLength.v : curve_length_additive`. +- Keep the result type named (MULTICURVE vs MULTILINESTRING of chords). + +## Out of scope + +- Merge into JTS #7. Type-11 reader PR. GEO-TIN 15–17. +- A second MultiCurve type. Public noder. JTS #27. JTS #38. +- Minting a Coq MultiCurve carrier as the leftover (that is a + different missing type; HOLD implement stands here too). +- `#509` Jordan true-region. F-MS / MULTISURFACE. WKB-8-12 I/O. +- QG-CURVE-CHORD path-stamp CI. `615-h` IsValid rung. +- COMPOUNDCURVE ticket 30. CURVEPOLYGON ticket 32. +- Remint `69-a`, `508-*`, leftover `Ⅰ`–`Ⅹ`. +- Setting WSJF. + +## Done when + +A later `/implement`, **after** Architect SIGN, can point at one named +site (engine or Coq) and say whether it refused or stamped. This ticket +stays open until that letter lands. Do not mint `CRV-MC` as a Proofs +claimId unless that letter names a new lemma. + +## Resolution + +**Implemented 2026-09-01 on GEOS** after `/implement 660` SIGN. + +Named site: GEOS OverlayNG + C API overlay. A `MULTICURVE` overlay +result keeps curved types; silent `MULTILINESTRING` emit is a refuse +unless the caller used `getLinearized`. + +Coq still has no MultiCurve carrier +(`CurveGeometry.v : valid_curve_geometry` is F-MS-shaped). That +missing type is not this leftover. No new Coq lemma. +claimId: none. witness: none. diff --git a/docs/scout/tickets/closed/35-multisurface-type-chart.md b/docs/scout/tickets/closed/35-multisurface-type-chart.md new file mode 100644 index 00000000..6b32fc12 --- /dev/null +++ b/docs/scout/tickets/closed/35-multisurface-type-chart.md @@ -0,0 +1,47 @@ +# Chart MULTISURFACE type honesty + +**Type:** grilling · **Map:** [MULTISURFACE](../../map-multisurface.md) +**Claimed:** wayfinder 2026-09-01 · **Closed:** 2026-09-01 +**Blocked by:** — +**claimId:** none · **GitHub:** none · **witness:** none + +No dedicated board card. Sibling WKB-8-12 is I/O (type 12). Sibling +tickets: COMPOUNDCURVE 29 / 30, CURVEPOLYGON 31 / 32, +MULTICURVE 33 / 34 — all siblings in this packet. + +## Question + +What does `/wayfinder MULTISURFACE` own? Name what is already true, +park what is HOLD, and leave one named leftover so the next session +cannot steal ticket 32, steal ticket 34, steal `#509`, or treat +`valid_curve_geometry` as overlay honesty. + +## Resolution + +**Grilled 2026-09-01. Living record: +[`docs/scout/map-multisurface.md`](../../map-multisurface.md).** +This ticket does not implement silent-multipolygon-collapse. + +**Already true.** SQL/MM `ST_MultiSurface` is ISO/IEC 13249-3 §4.2.27, +WKB 12. Coq structural collection is +`CurveGeometry.v : valid_curve_geometry` (`list CurvePolygon`) with +`CurveGeometry.v : valid_curve_geometry_nil` / +`CurveGeometry.v : valid_curve_geometry_cons`. Named collection +linearise is `CurveGeometry.v : to_geometry`. Named ring linearise is +`CurveLinearise.v : to_geometry_outer_ring_closed`. JTS has Option A +(`MultiSurface extends MultiPolygon`) and named `toLinear`. NTS has +`OgcGeometryType.MultiSurface = 12`. Linear WKT/GeoJSON is +`WktGeoJsonRoundtrip.v : wkt_geojson_wkt_roundtrip` (no MULTISURFACE +constructor). HELP names CS / CC / CP and does not name MULTISURFACE. + +**Three words.** Silent MultiPolygon collapse is the leftover. Named +`Linearize` / `toLinear` / `to_geometry` is allowed. Collection / +member list is already the structural pin. + +**Parks.** JTS #27 out. JTS #38 off #7. No public noder. HOLD merge +into #7. HOLD a second MultiSurface type. HOLD implement for ticket 36 +(no Architect SIGN). No type-12 reader PR. No GEO-TIN 15–17. No DOI. +Cite 13249-3 only. Do not steal `615-h`. Do not remint `#509`. + +**Frontier.** Ticket 36 names the leftover. HOLD implement stands. +Do not `/implement` from this letter. diff --git a/docs/scout/tickets/closed/36-multisurface-silent-multipolygon-collapse.md b/docs/scout/tickets/closed/36-multisurface-silent-multipolygon-collapse.md new file mode 100644 index 00000000..30671c5a --- /dev/null +++ b/docs/scout/tickets/closed/36-multisurface-silent-multipolygon-collapse.md @@ -0,0 +1,69 @@ +# Silent MultiPolygon collapse — MULTISURFACE type honesty + +**Type:** implement · **Map:** [MULTISURFACE](../../map-multisurface.md) +**Claimed:** implement 2026-09-01 · **Closed:** 2026-09-01 (GEOS named the leftover) +**Blocked by:** ~~[Chart MULTISURFACE type honesty](35-multisurface-type-chart.md)~~ ✔ +**claimId:** none · **GitHub:** none · **witness:** none + +HOLD implement stood until `/implement 660` on GEOS. +Sibling CURVEPOLYGON ticket 32 (this packet) is one-surface POLYGON emit, +not this. Sibling MULTICURVE ticket 34 (this packet) is lineal +MULTILINESTRING emit, not this. + +## Ask + +Name or refuse the silent path that still eats `MULTISURFACE` at +overlay, hull, or TestBuilder and emits `MULTIPOLYGON` / `Polygon[]` +without a stamp, or treats the JTS `MultiPolygon` supertype as +linearized members. A multisurface stays a multisurface. Named +`Linearize` / `toLinear` / `to_geometry` / `chord_approx_ring` / +OverlayNGCurve `APPROX` + `isApproximate()` stays named. I/O type +identity is not op honesty. + +Cite ISO/IEC 13249-3. No DOI. No 19125-2. + +Do not start this ticket until Architect SIGN lifts HOLD implement. + +## In scope + +- Engine grill: NTS overlay / hull / TestBuilder sites that still + consume `MultiSurface` (or WKB type 12) and emit `MultiPolygon` + without calling `Linearize` / `toLinear`. JTS OverlayNGCurve cells + that densify with `isApproximate()=false`, or that hand a + `MultiPolygon` view to a caller as if it were the curve collection. +- One Proofs honesty pin **only if** it is a new statement. Do not + remint `CurveGeometry.v : valid_curve_geometry`, + `CurveGeometry.v : to_geometry`, + `CurveLinearise.v : to_geometry_outer_ring_closed`, or + `WktGeoJsonRoundtrip.v : wkt_geojson_wkt_roundtrip`. +- Keep the result type named (MULTISURFACE vs MULTIPOLYGON of chords). + +## Out of scope + +- Merge into JTS #7. Type-12 reader PR. GEO-TIN 15–17. +- A second MultiSurface type. Public noder. JTS #27. JTS #38. +- `#509` Jordan true-region. I/O member-tag degrade. WKB-8-12 I/O. +- QG-CURVE-CHORD path-stamp CI. `615-h` IsValid rung. +- COMPOUNDCURVE ticket 30. CURVEPOLYGON ticket 32. MULTICURVE ticket 34. +- Remint `69-a`, `508-*`, leftover `Ⅰ`–`Ⅹ`. +- Setting WSJF. + +## Done when + +A later `/implement`, **after** Architect SIGN, can point at one named +site (engine or Coq) and say whether it refused or stamped. This ticket +stays open until that letter lands. Do not mint `CRV-MS` as a Proofs +claimId unless that letter names a new lemma. + +## Resolution + +**Implemented 2026-09-01 on GEOS** after `/implement 660` SIGN. + +Named site: `CascadedPolygonUnion::restrictToSurfaces`. It used +`hasCurvedComponents()`, so an all-linear `CurvePolygon` (no arcs) +was packed into `MultiPolygon`. It now checks `hasCurvedTypes()`. +That is the refuse of silent `MULTIPOLYGON` emit. + +`CurveGeometry.v : valid_curve_geometry` stays structural F-MS. +`CurveGeometry.v : to_geometry` stays named linearise. No new Coq +lemma. Do not remint tracker 509. claimId: none. witness: none. diff --git a/docs/scout/tickets/closed/37-sqlmm-wkt-oracle.md b/docs/scout/tickets/closed/37-sqlmm-wkt-oracle.md new file mode 100644 index 00000000..f2c16149 --- /dev/null +++ b/docs/scout/tickets/closed/37-sqlmm-wkt-oracle.md @@ -0,0 +1,53 @@ +# SQL/MM WKT oracle — CLOTHOID / CIRCLE / GEODESICSTRING / NURBSCURVE / SPIRALCURVE + +**Type:** implement · **Map:** [COMPOUNDCURVE](../../map-compoundcurve.md) (packet-wide I/O) +**Claimed:** implement 2026-09-01 · **Closed:** 2026-09-01 +**Blocked by:** tickets 30 / 32 / 34 / 36 (type honesty named on GEOS) +**claimId:** none · **GitHub:** none · **witness:** none + +## Ask + +Implement the structural oracle for the §4.2.1 instantiable ST_Curve +subtypes that the engines do not yet carry, and for optional +extensions such as the documented deviations from the standard. + +A `SPIRALTYPE` value may contain anything but a comma or a +parenthesis. The standard defines `` as free-form +``, and §5.1.68 length-prefixes the value in WKB, so the +value set is open — §4.2.12 lists `clothoid`, `bloss`, +`biquadratic`, `sine` and `cosine` only as the *initial* set. Text +has no length prefix, and `` admits the characters that +would end the value, so the lexer reads a spiral type up to the +comma or closing parenthesis that terminates it. Interior spaces +are preserved, so `SPIRALTYPE Wiener Bogen` parses. A name +containing a comma or a parenthesis is the one case this grammar +cannot represent. + +Cite ISO/IEC 13249-3. No DOI. No 19125-2. + +## In scope + +- Oracle mode `SQLMM_WKT` (structural parse / refuse / type identity). +- SPIRALTYPE open-set lexer deviation, pinned by red tests. +- Documented deviations: keyword case-fold, tagged LINESTRING in + COMPOUNDCURVE. +- ELLIPTICALCURVE as instantiable §4.2.9 (not UNKNOWN). + +## Out of scope + +- GEOS / NTS / JTS carriers. `CurveSegment` growth. `508-*` remint. +- Leftover `Ⅺ`. Length mint of `K` / `N` tokens (M-LEN-ZOO stays). +- Type-9/10/11/12 reader PRs. JTS #7 CLOTHOID-in-COMPOUNDCURVE + 3-arg proposal. Koc railway compound. +- Inventing WKB codes (Table 15 lists 8–12 only). + +## Resolution + +**Implemented 2026-09-01** on Proofs (`cursor/sqlmm-type-honesty-ccfa`). + +Named site: `oracle/sqlmm_wkt.ml` + driver mode `SQLMM_WKT`. +Red tests: `oracle/red_sqlmm_wkt_tests.py`. Clause-book §4.1 / §8 +record the productions and the SPIRALTYPE lexer deviation. + +No new Coq lemma. claimId: none. witness: none. +Do not remint `508-*`. Do not grow `CurveSegment`. diff --git a/docs/scout/tickets/closed/38-nts-sqlmm-named-refuse.md b/docs/scout/tickets/closed/38-nts-sqlmm-named-refuse.md new file mode 100644 index 00000000..459d166c --- /dev/null +++ b/docs/scout/tickets/closed/38-nts-sqlmm-named-refuse.md @@ -0,0 +1,49 @@ +# NTS WKT named refuse for §4.2.1 curve types + +**Type:** implement · **Map:** [COMPOUNDCURVE](../../map-compoundcurve.md) (packet-wide I/O) +**Claimed:** implement 2026-09-02 · **Closed:** 2026-09-02 (NTS named refuse) +**Blocked by:** ~~[SQL/MM WKT oracle](closed/37-sqlmm-wkt-oracle.md)~~ ✔ +**claimId:** none · **GitHub:** none · **witness:** none + +## Ask + +GEOS already names `CLOTHOID`, `CIRCLE`, `GEODESICSTRING`, +`NURBSCURVE`, and `SPIRALCURVE` and refuses. NTS WKT still says +`Unknown type`, which is a lie: they are instantiable ST_Curve +subtypes in ISO/IEC 13249-3 §4.2.1, not optional extras. + +Name them and refuse. Do not grow a carrier. Do not flatten to +`LINESTRING`. A genuine unknown token still says `Unknown type`. +`COMPOUNDCURVE (CLOTHOID …)` must hit the same named refuse, not +`Unexpected token`. + +Cite ISO/IEC 13249-3. No DOI. No 19125-2. + +## In scope + +- NTS `WKTReader` top-level dispatch and `ReadCurveText` members. +- Tests that the five types (and Z form) refuse with §4.2.1 in the + message, and that `NOTATYPE` stays `Unknown type`. +- ELLIPTICALCURVE (§4.2.9) is instantiable too — same named refuse. + +## Out of scope + +- Carriers. `CurveSegment` growth. `508-*` remint. Leftover `Ⅺ`. +- Type-9/10/11/12 reader PRs. JTS #7 3-arg CLOTHOID-in-COMPOUNDCURVE + (SFA, not ST_Clothoid). Koc railway compound. +- Inventing WKB codes. Parsing SPIRALTYPE (that is oracle + `SQLMM_WKT`, ticket 37). +- Ticket 10 / #506. + +## Resolution + +**Implemented 2026-09-02 on NTS** (`cursor/sqlmm-type-honesty-ccfa`). + +Named site: `WKTReader` dispatch + `ReadCurveText`. Message: +`SQL/MM type is not optional (ISO/IEC 13249-3 §4.2.1) and is not +implemented`. `NOTATYPE` still says `Unknown type`. CIRCLE does not +steal CIRCULARSTRING (dim-suffix matcher, not `IsTypeName`). + +Pins: `CurveWktTest.SqlMmSection421TypesAreNamedRefusesNotUnknown` +(31 CurveWktTest passed). No carrier. Do not remint `508-*`. +claimId: none. witness: none. diff --git a/oracle/Makefile b/oracle/Makefile index e573b645..1f71d62d 100644 --- a/oracle/Makefile +++ b/oracle/Makefile @@ -45,7 +45,7 @@ FFI_LDLIBS := -L$(OCAML_WHERE) -lasmrun_pic -lm -ldl -lpthread SCOUT_IC_LIB := libscout_incircle.$(FFI_SOEXT) SCOUT_IC_PROBE := scout_incircle_probe -.PHONY: all clean ffi ffi-parity jts1093-orient-scout scout-incircle-ffi jts1094-scout arc-arc-tests arc-segment-tests arc-arc-distance-tests arc-segment-distance-tests ring-simple-tests cp-ring-simple-tests cp-boundary-simplify-tests cp-boundary-simplify-test arc-offset-tests point-in-curve-ring-tests ring-orientation-tests holes-disjoint-tests curve-relate-matrix-tests buffer-region-tests arc-centroid-tests arc-area-centroid-tests arc-distance-tests arc-area-tests arc-buffer-simple-tests arc-simplify-decision-tests arc-offset-filtered-tests curve-adversarial-hunt elliptic-hunt bezier-hunt winding-number-tests disc-overlay-tests lec-circle-tests obstacle-distance-tests +.PHONY: all clean ffi ffi-parity jts1093-orient-scout scout-incircle-ffi jts1094-scout arc-arc-tests arc-segment-tests arc-arc-distance-tests arc-segment-distance-tests ring-simple-tests cp-ring-simple-tests cp-boundary-simplify-tests cp-boundary-simplify-test arc-offset-tests point-in-curve-ring-tests ring-orientation-tests holes-disjoint-tests curve-relate-matrix-tests buffer-region-tests arc-centroid-tests arc-area-centroid-tests arc-distance-tests arc-area-tests arc-buffer-simple-tests arc-simplify-decision-tests arc-offset-filtered-tests curve-adversarial-hunt elliptic-hunt bezier-hunt winding-number-tests disc-overlay-tests lec-circle-tests obstacle-distance-tests sqlmm-wkt-tests all: $(TARGET) @@ -221,11 +221,22 @@ extracted.cmx: extracted.ml extracted.cmi relate_matrix.cmx: relate_matrix.ml $(OCAMLOPT) -c $< -driver.cmx: driver.ml extracted.cmi relate_matrix.cmx +sqlmm_wkt.cmx: sqlmm_wkt.ml + $(OCAMLOPT) -c $< + +driver.cmx: driver.ml extracted.cmi relate_matrix.cmx sqlmm_wkt.cmx $(OCAMLOPT) -package zarith -c driver.ml -$(TARGET): extracted.cmx driver.cmx relate_matrix.cmx - $(OCAMLOPT) -package str,zarith -linkpkg extracted.cmx relate_matrix.cmx driver.cmx -o $@ +$(TARGET): extracted.cmx driver.cmx relate_matrix.cmx sqlmm_wkt.cmx + $(OCAMLOPT) -package str,zarith -linkpkg extracted.cmx relate_matrix.cmx sqlmm_wkt.cmx driver.cmx -o $@ + +# Structural SQL/MM WKT oracle (no extracted.ml). Same SQLMM_WKT protocol +# as oracle_bin; used to run red_sqlmm_wkt_tests.py without a full rebuild. +sqlmm_wkt_bin: sqlmm_wkt.ml sqlmm_wkt_main.ml + ocamlopt -o sqlmm_wkt_bin sqlmm_wkt.ml sqlmm_wkt_main.ml + +sqlmm-wkt-tests: sqlmm_wkt_bin + cd .. && ORACLE_BIN=oracle/sqlmm_wkt_bin python3 oracle/red_sqlmm_wkt_tests.py # ---- Phase 5: in-process C ABI (libntsrocq) -------------------------------- @@ -287,4 +298,5 @@ jts1094-scout: scout-incircle-ffi $(TARGET) clean: rm -f *.cmi *.cmo *.cmx *.o $(TARGET) $(FFI_LIB) $(FFI_PROBE) \ - $(SCOUT_IC_LIB) $(SCOUT_IC_PROBE) scout_incircle_ml.o scout_incircle_stubs.o + $(SCOUT_IC_LIB) $(SCOUT_IC_PROBE) scout_incircle_ml.o scout_incircle_stubs.o \ + sqlmm_wkt_bin diff --git a/oracle/driver.ml b/oracle/driver.ml index 90c17fb3..1e7be8e0 100644 --- a/oracle/driver.ml +++ b/oracle/driver.ml @@ -4656,6 +4656,15 @@ let run_cp_boundary_simplify () = (if triple_int_safe a b c then "INTSAFE" else "APPROX") done +(* ----- SQLMM_WKT (structural I/O identity; no binary64). + ISO/IEC 13249-3 §4.2.1 instantiable ST_Curve subtypes that the engines + do not yet carry, plus the SPIRALTYPE open-set lexer deviation. + Implementation lives in sqlmm_wkt.ml so this mode cannot grow a + hand-rolled float kernel. See oracle/red_sqlmm_wkt_tests.py. *) +let run_sqlmm_wkt () = + let line = input_line stdin in + print_endline (Sqlmm_wkt.parse_line line) + (* ----- Mode dispatch. ----------------------------------------------------- *) (* Persistent loop: SIMPLIFY exits after one call (it reads its input @@ -4736,6 +4745,7 @@ let () = | "ARC_BUFFER_SIMPLE" -> run_arc_buffer_simple () | "ARC_SIMPLIFY_DECISION" -> run_arc_simplify_decision () | "ARC_OFFSET_FILTERED" -> run_arc_offset_filtered () + | "SQLMM_WKT" -> run_sqlmm_wkt () | other -> failwith (Printf.sprintf "oracle: unknown mode: %s" other)); flush stdout; loop () diff --git a/oracle/red_sqlmm_wkt_tests.py b/oracle/red_sqlmm_wkt_tests.py new file mode 100644 index 00000000..120af5b5 --- /dev/null +++ b/oracle/red_sqlmm_wkt_tests.py @@ -0,0 +1,198 @@ +#!/usr/bin/env python3 +# ============================================================================= +# oracle/red_sqlmm_wkt_tests.py +# coverage: feat:sqlmm-wkt geom:clothoid,circle,geodesicstring,nurbscurve,spiralcurve +# ----------------------------------------------------------------------------- +# Assert-style red tests for the SQLMM_WKT oracle mode. +# Structural I/O identity only — no length, no CurveSegment growth, no 508-*. +# +# Run (from repo root): +# make -C oracle sqlmm-wkt-tests +# ORACLE_BIN=oracle/oracle_bin python3 oracle/red_sqlmm_wkt_tests.py +# Exit status: 0 iff every assertion passes. +# +# Backing notes: ISO/IEC 13249-3 §4.2.1 / §4.2.7–§4.2.12 / §5.1.67 / §5.1.68. +# SPIRALTYPE lexer deviation: docs/iso13249-3-curve-type-bindings-2026-08.md §8. +# ============================================================================= +import os +import subprocess +import sys + +_HERE = os.path.dirname(os.path.abspath(__file__)) +_CANDIDATES = [ + os.environ.get("ORACLE_BIN"), + os.path.join(_HERE, "oracle_bin"), + os.path.join(_HERE, "sqlmm_wkt_bin"), +] +BIN = next((p for p in _CANDIDATES if p and os.path.isfile(p) and os.access(p, os.X_OK)), None) +failures = 0 + + +def sqlmm(wkt): + if BIN is None: + raise SystemExit("!! no SQLMM_WKT binary (oracle_bin or sqlmm_wkt_bin)") + inp = f"SQLMM_WKT\n{wkt}\n" + proc = subprocess.run([BIN], input=inp, capture_output=True, text=True) + if proc.returncode != 0: + return f"EXIT {proc.returncode}: {proc.stderr.strip()}" + return proc.stdout.strip().splitlines()[-1] if proc.stdout.strip() else "" + + +def assert_eq(name, got, expected): + global failures + status = "PASS" if got == expected else "FAIL" + print(f" [{status}] {name}: got {got!r} expected {expected!r}") + if got != expected: + failures += 1 + + +def assert_true(name, cond, detail=""): + global failures + status = "PASS" if cond else "FAIL" + print(f" [{status}] {name}{': ' + detail if detail else ''}") + if not cond: + failures += 1 + + +print("SQLMM_WKT — §4.2.1 instantiable types") +for typ in ("CLOTHOID", "CIRCLE", "GEODESICSTRING", "NURBSCURVE", "SPIRALCURVE"): + assert_eq(f"{typ} EMPTY", sqlmm(f"{typ} EMPTY"), f"OK {typ} XY EMPTY") + +assert_eq( + "CIRCLE three points", + sqlmm("CIRCLE (0 0, 1 0, 0 1)"), + "OK CIRCLE XY POINTS 3", +) +assert_true("CIRCLE arity 2 refuses", sqlmm("CIRCLE (0 0, 1 0)").startswith("REFUSE")) +assert_eq( + "CIRCLE Z three points", + sqlmm("CIRCLE Z (0 0 1, 1 0 1, 0 1 1)"), + "OK CIRCLE Z POINTS 3", +) +assert_true( + "CIRCLE Z with XY points refuses", + sqlmm("CIRCLE Z (0 0, 1 0, 0 1)").startswith("REFUSE"), +) + +assert_eq( + "GEODESICSTRING three points", + sqlmm("GEODESICSTRING (0 0, 1 1, 2 0)"), + "OK GEODESICSTRING XY POINTS 3", +) +assert_true( + "GEODESICSTRING one point refuses", + sqlmm("GEODESICSTRING (0 0)").startswith("REFUSE"), +) + +assert_eq( + "CLOTHOID keyword form", + sqlmm( + "CLOTHOID (AFFINEPLACEMENT (LOCATION (0 0), REFERENCEDIRECTIONS (1 0)), " + "SCALEFACTOR 1, STARTDISTANCE 0, ENDDISTANCE 2)" + ), + "OK CLOTHOID XY SCALEFACTOR 1 STARTDISTANCE 0 ENDDISTANCE 2", +) +assert_true( + "CLOTHOID missing SCALEFACTOR refuses", + sqlmm( + "CLOTHOID (AFFINEPLACEMENT (LOCATION (0 0), REFERENCEDIRECTIONS (1 0)), " + "STARTDISTANCE 0, ENDDISTANCE 2)" + ).startswith("REFUSE"), +) + +assert_eq( + "NURBSCURVE single-span", + sqlmm( + "NURBSCURVE (DEGREE 2, KNOTS (0, 0, 0, 1, 1, 1), " + "CONTROLPOINTS ((0 0, 1), (1 1, 1), (2 0, 1)))" + ), + "OK NURBSCURVE XY DEGREE 2 CONTROLPOINTS 3 KNOTS 6", +) + +print("SQLMM_WKT — SPIRALTYPE initial set and open-set extension") +for name in ("clothoid", "bloss", "biquadratic", "sine", "cosine"): + assert_eq( + f"SPIRALTYPE {name} INITIAL", + sqlmm(f"SPIRALCURVE (SPIRALTYPE {name})"), + f"OK SPIRALCURVE XY SPIRALTYPE {name} INITIAL", + ) + +assert_eq( + "SPIRALTYPE Wiener Bogen preserves interior space", + sqlmm("SPIRALCURVE (SPIRALTYPE Wiener Bogen)"), + "OK SPIRALCURVE XY SPIRALTYPE Wiener Bogen EXTENSION", +) +assert_eq( + "SPIRALTYPE Wiener Bogen with LENGTH", + sqlmm("SPIRALCURVE (SPIRALTYPE Wiener Bogen, LENGTH 10)"), + "OK SPIRALCURVE XY SPIRALTYPE Wiener Bogen EXTENSION LENGTH 10", +) + +print("SQLMM_WKT — deviations from the standard") +# A name containing a comma cannot be represented: the lexer ends at the comma. +got = sqlmm("SPIRALCURVE (SPIRALTYPE Wiener, Bogen)") +assert_true( + "comma in SPIRALTYPE is unrepresentable (does not parse as 'Wiener, Bogen')", + (not got.startswith("OK ")) or "Wiener, Bogen" not in got, + got, +) +assert_true( + "comma in SPIRALTYPE refuses the leftover field", + got.startswith("REFUSE"), + got, +) + +# A name containing a parenthesis cannot be represented. +got = sqlmm("SPIRALCURVE (SPIRALTYPE foo(bar))") +assert_true( + "parenthesis in SPIRALTYPE is unrepresentable", + (not got.startswith("OK ")) or "foo(bar)" not in got, + got, +) +assert_true( + "parenthesis in SPIRALTYPE refuses", + got.startswith("REFUSE"), + got, +) + +assert_eq( + "empty SPIRALTYPE refuses", + sqlmm("SPIRALCURVE (SPIRALTYPE )"), + "REFUSE EMPTY_SPIRALTYPE", +) + +assert_eq( + "lowercase type keyword is CASEFOLD deviation", + sqlmm("circle (0 0, 1 0, 0 1)"), + "OK CIRCLE XY POINTS 3 CASEFOLD", +) + +assert_eq( + "tagged LINESTRING in COMPOUNDCURVE is documented deviation", + sqlmm("COMPOUNDCURVE (LINESTRING (0 0, 1 0), CIRCULARSTRING (1 0, 2 1, 3 0))"), + "OK COMPOUNDCURVE XY MEMBERS 2 [LINESTRING,CIRCULARSTRING] DEVIATION TAGGED_LINESTRING", +) + +print("SQLMM_WKT — named vs unknown; compound members") +assert_eq("unknown token stays UNKNOWN", sqlmm("FOOBAR (0 0)"), "UNKNOWN FOOBAR") +assert_eq( + "ELLIPTICALCURVE is instantiable §4.2.9, not UNKNOWN", + sqlmm("ELLIPTICALCURVE EMPTY"), + "OK ELLIPTICALCURVE XY EMPTY", +) +assert_eq( + "COMPOUNDCURVE may carry CIRCLE + bare linestring", + sqlmm("COMPOUNDCURVE (CIRCLE (0 0, 1 0, 0 1), (1 0, 2 0))"), + "OK COMPOUNDCURVE XY MEMBERS 2 [CIRCLE,LINESTRING_BARE]", +) +assert_eq( + "COMPOUNDCURVE may carry CLOTHOID + GEODESICSTRING", + sqlmm("COMPOUNDCURVE (CLOTHOID EMPTY, GEODESICSTRING (0 0, 1 0))"), + "OK COMPOUNDCURVE XY MEMBERS 2 [CLOTHOID,GEODESICSTRING]", +) + +print() +if failures: + print(f"!! {failures} test(s) FAILED", file=sys.stderr) + sys.exit(1) +print("SQLMM_WKT red tests: all passed") diff --git a/oracle/sqlmm_wkt.ml b/oracle/sqlmm_wkt.ml new file mode 100644 index 00000000..36d5de54 --- /dev/null +++ b/oracle/sqlmm_wkt.ml @@ -0,0 +1,558 @@ +(* ============================================================================= + oracle/sqlmm_wkt.ml + ----------------------------------------------------------------------------- + Structural WKT oracle for the ISO/IEC 13249-3 §4.2.1 instantiable ST_Curve + subtypes that the engines do not yet carry: CLOTHOID, CIRCLE, + GEODESICSTRING, NURBSCURVE, SPIRALCURVE (plus ELLIPTICALCURVE, also + instantiable at §4.2.9, so it is not UNKNOWN). + + This is I/O type identity. It does not evaluate length, does not grow + CurveSegment, and does not remint 508-*. Numbers stay decimal tokens; + there is no binary64 arithmetic here. + + SPIRALTYPE deviation (documented in + docs/iso13249-3-curve-type-bindings-2026-08.md §8): + The standard writes as free-form , and + §5.1.68 length-prefixes the value in WKB, so the value set is open — + §4.2.12 lists clothoid, bloss, biquadratic, sine and cosine only as + the *initial* set. Text has no length prefix, and admits + the characters that would end the value, so this lexer reads a spiral + type up to the comma or parenthesis that terminates it. Interior + spaces are preserved (SPIRALTYPE Wiener Bogen parses). A name + containing a comma or a parenthesis is the one case this grammar + cannot represent. + + Protocol (driver mode SQLMM_WKT): + SQLMM_WKT + + Output: one line + OK ... + REFUSE + UNKNOWN + A successful parse of a lowercase type keyword adds CASEFOLD (the + spec is silent on keyword case; tolerant-in is the documented + deviation). A tagged LINESTRING member inside COMPOUNDCURVE / + CURVEPOLYGON adds DEVIATION TAGGED_LINESTRING. + ========================================================================== *) + +type dim = XY | Z | M | ZM + +exception Parse of string + +type cursor = { s : string; mutable i : int } + +let slen c = String.length c.s +let eof c = c.i >= slen c +let peek c = if eof c then None else Some c.s.[c.i] + +let rec skip_ws c = + match peek c with + | Some (' ' | '\t' | '\n' | '\r') -> c.i <- c.i + 1; skip_ws c + | _ -> () + +let is_digit ch = ch >= '0' && ch <= '9' +let is_letter ch = + (ch >= 'A' && ch <= 'Z') || (ch >= 'a' && ch <= 'z') + +let ieq a b = + String.uppercase_ascii a = String.uppercase_ascii b + +let rtrim s = + let n = String.length s in + let rec last i = + if i < 0 then -1 + else + match s.[i] with + | ' ' | '\t' | '\n' | '\r' -> last (i - 1) + | _ -> i + in + let e = last (n - 1) in + if e < 0 then "" else String.sub s 0 (e + 1) + +let dim_string = function + | XY -> "XY" + | Z -> "Z" + | M -> "M" + | ZM -> "ZM" + +let expect_char c ch = + skip_ws c; + match peek c with + | Some x when x = ch -> c.i <- c.i + 1 + | Some x -> + raise (Parse (Printf.sprintf "expected '%c', got '%c'" ch x)) + | None -> + raise (Parse (Printf.sprintf "expected '%c', got EOF" ch)) + +let read_word c = + skip_ws c; + match peek c with + | Some ch when is_letter ch -> + let start = c.i in + c.i <- c.i + 1; + while not (eof c) + && (is_letter c.s.[c.i] || is_digit c.s.[c.i] || c.s.[c.i] = '_') + do + c.i <- c.i + 1 + done; + String.sub c.s start (c.i - start) + | _ -> raise (Parse "expected word") + +let looks_like_number c = + skip_ws c; + match peek c with + | Some ('+' | '-') -> + let j = c.i + 1 in + j < slen c && (is_digit c.s.[j] || c.s.[j] = '.') + | Some '.' -> + let j = c.i + 1 in + j < slen c && is_digit c.s.[j] + | Some ch -> is_digit ch + | None -> false + +let read_number c = + skip_ws c; + let start = c.i in + (match peek c with + | Some ('+' | '-') -> c.i <- c.i + 1 + | _ -> ()); + let saw_digit = ref false in + while not (eof c) && is_digit c.s.[c.i] do + saw_digit := true; + c.i <- c.i + 1 + done; + if not (eof c) && c.s.[c.i] = '.' then begin + c.i <- c.i + 1; + while not (eof c) && is_digit c.s.[c.i] do + saw_digit := true; + c.i <- c.i + 1 + done + end; + if not !saw_digit then raise (Parse "expected number"); + if not (eof c) && (c.s.[c.i] = 'e' || c.s.[c.i] = 'E') then begin + c.i <- c.i + 1; + (match peek c with + | Some ('+' | '-') -> c.i <- c.i + 1 + | _ -> ()); + let exp = ref false in + while not (eof c) && is_digit c.s.[c.i] do + exp := true; + c.i <- c.i + 1 + done; + if not !exp then raise (Parse "expected exponent") + end; + String.sub c.s start (c.i - start) + +(* SPIRALTYPE value: anything but comma or parenthesis. Interior spaces + stay. Trailing whitespace before the terminator is not interior. *) +let read_spiraltype_value c = + skip_ws c; + let start = c.i in + let rec scan () = + match peek c with + | Some (',' | '(' | ')') | None -> () + | Some _ -> c.i <- c.i + 1; scan () + in + scan (); + rtrim (String.sub c.s start (c.i - start)) + +let initial_spiraltype s = + match String.lowercase_ascii s with + | "clothoid" | "bloss" | "biquadratic" | "sine" | "cosine" -> true + | _ -> false + +let split_type_and_dim raw = + let u = String.uppercase_ascii raw in + let n = String.length u in + if n >= 2 && String.sub u (n - 2) 2 = "ZM" then + (String.sub raw 0 (n - 2), Some ZM) + else if n >= 1 && String.sub u (n - 1) 1 = "Z" then + (String.sub raw 0 (n - 1), Some Z) + else if n >= 1 && String.sub u (n - 1) 1 = "M" then + (String.sub raw 0 (n - 1), Some M) + else + (raw, None) + +let read_optional_dim c attached = + match attached with + | Some d -> d + | None -> + skip_ws c; + match peek c with + | Some ch when is_letter ch -> + let save = c.i in + let w = read_word c in + begin match String.uppercase_ascii w with + | "ZM" -> ZM + | "Z" -> Z + | "M" -> M + | _ -> c.i <- save; XY + end + | _ -> XY + +let at_empty c = + skip_ws c; + match peek c with + | Some ch when is_letter ch -> + let save = c.i in + let w = read_word c in + if ieq w "EMPTY" then true else (c.i <- save; false) + | _ -> false + +let finish c = + skip_ws c; + if not (eof c) then raise (Parse "trailing input") + +let comma_or_rparen c = + skip_ws c; + match peek c with + | Some ',' -> c.i <- c.i + 1; `Comma + | Some ')' -> `RParen + | Some x -> raise (Parse (Printf.sprintf "expected ',' or ')', got '%c'" x)) + | None -> raise (Parse "expected ',' or ')', got EOF") + +let expect_word c name = + let w = read_word c in + if not (ieq w name) then + raise (Parse (Printf.sprintf "expected %s, got %s" name w)) + +let read_point_nums c = + if not (looks_like_number c) then raise (Parse "expected point"); + let rec more acc = + if looks_like_number c then more (read_number c :: acc) else List.rev acc + in + more [read_number c] + +let read_point_list c = + expect_char c '('; + skip_ws c; + if peek c = Some ')' then begin + c.i <- c.i + 1; + [] + end else + let rec rest acc = + match comma_or_rparen c with + | `RParen -> expect_char c ')'; List.rev acc + | `Comma -> rest (read_point_nums c :: acc) + in + rest [read_point_nums c] + +let expected_ords = function + | XY -> 2 + | Z | M -> 3 + | ZM -> 4 + +let check_point_dim dim pts = + let n = expected_ords dim in + List.iter + (fun p -> if List.length p <> n then raise (Parse "POINT_DIM")) + pts + +let read_balanced_group c = + skip_ws c; + expect_char c '('; + let start = c.i in + let rec walk depth = + if eof c then raise (Parse "unbalanced parenthesis"); + let ch = c.s.[c.i] in + c.i <- c.i + 1; + match ch with + | '(' -> walk (depth + 1) + | ')' -> if depth = 1 then () else walk (depth - 1) + | _ -> walk depth + in + walk 1; + rtrim (String.sub c.s start (c.i - start - 1)) + +let skip_optional_comma c = + skip_ws c; + match peek c with + | Some ',' -> c.i <- c.i + 1 + | _ -> () + +type field = { name : string; value : string } + +let rec read_named_fields c acc = + skip_ws c; + match peek c with + | Some ')' -> List.rev acc + | Some ch when is_letter ch -> + let name = read_word c in + skip_ws c; + let value = + match peek c with + | Some '(' -> read_balanced_group c + | _ when looks_like_number c -> read_number c + | Some ch when is_letter ch -> read_word c + | _ -> raise (Parse (Printf.sprintf "bad field %s" name)) + in + skip_optional_comma c; + read_named_fields c ({ name; value } :: acc) + | Some x -> + raise (Parse (Printf.sprintf "expected field or ')', got '%c'" x)) + | None -> raise (Parse "unterminated field list") + +let field_find fields name = + try Some (List.find (fun f -> ieq f.name name) fields).value + with Not_found -> None + +let require_field fields name = + match field_find fields name with + | Some v -> v + | None -> raise (Parse (Printf.sprintf "missing %s" name)) + +let parse_point_body dim c ~arity_min ~arity_exact ~empty_ok = + if at_empty c then + if empty_ok then "EMPTY" else raise (Parse "EMPTY_FORBIDDEN") + else begin + let pts = read_point_list c in + check_point_dim dim pts; + let n = List.length pts in + (match arity_exact with + | Some k when n <> k -> raise (Parse "ARITY") + | _ -> ()); + if n < arity_min then raise (Parse "ARITY"); + Printf.sprintf "POINTS %d" n + end + +let parse_clothoid _dim c = + if at_empty c then "EMPTY" + else begin + expect_char c '('; + let fields = read_named_fields c [] in + expect_char c ')'; + ignore (require_field fields "AFFINEPLACEMENT"); + let a = require_field fields "SCALEFACTOR" in + let sd = require_field fields "STARTDISTANCE" in + let ed = require_field fields "ENDDISTANCE" in + Printf.sprintf "SCALEFACTOR %s STARTDISTANCE %s ENDDISTANCE %s" a sd ed + end + +let parse_elliptical _dim c = + if at_empty c then "EMPTY" + else begin + expect_char c '('; + let fields = read_named_fields c [] in + expect_char c ')'; + ignore (require_field fields "AFFINEPLACEMENT"); + let rx = require_field fields "UAXISLENGTH" in + let ry = require_field fields "VAXISLENGTH" in + Printf.sprintf "UAXISLENGTH %s VAXISLENGTH %s" rx ry + end + +let read_number_list_group c = + expect_char c '('; + skip_ws c; + if peek c = Some ')' then begin + c.i <- c.i + 1; + [] + end else + let rec rest acc = + match comma_or_rparen c with + | `RParen -> expect_char c ')'; List.rev acc + | `Comma -> rest (read_number c :: acc) + in + rest [read_number c] + +let rec read_control_points c = + expect_char c '('; + skip_ws c; + if peek c = Some ')' then begin + c.i <- c.i + 1; + 0 + end else + let rec one n = + skip_ws c; + match peek c with + | Some ')' -> n + | Some '(' -> + ignore (read_balanced_group c); + skip_optional_comma c; + one (n + 1) + | _ when looks_like_number c -> + ignore (read_number c); + while looks_like_number c do ignore (read_number c) done; + skip_optional_comma c; + one (n + 1) + | Some x -> raise (Parse (Printf.sprintf "bad control point '%c'" x)) + | None -> raise (Parse "unterminated CONTROLPOINTS") + in + let n = one 0 in + expect_char c ')'; + n + +let parse_nurbs _dim c = + if at_empty c then "EMPTY" + else begin + expect_char c '('; + skip_ws c; + expect_word c "DEGREE"; + skip_optional_comma c; + let deg = read_number c in + skip_optional_comma c; + expect_word c "KNOTS"; + skip_optional_comma c; + let knots = read_number_list_group c in + skip_optional_comma c; + expect_word c "CONTROLPOINTS"; + skip_optional_comma c; + let ncp = read_control_points c in + skip_ws c; + skip_optional_comma c; + expect_char c ')'; + if ncp < 1 then raise (Parse "NURBSCURVE_CONTROLPOINTS"); + Printf.sprintf "DEGREE %s CONTROLPOINTS %d KNOTS %d" deg ncp (List.length knots) + end + +let parse_spiral _dim c = + if at_empty c then "EMPTY" + else begin + expect_char c '('; + skip_ws c; + expect_word c "SPIRALTYPE"; + let typ = read_spiraltype_value c in + if typ = "" then raise (Parse "EMPTY_SPIRALTYPE"); + skip_optional_comma c; + let fields = read_named_fields c [] in + expect_char c ')'; + let kind = if initial_spiraltype typ then "INITIAL" else "EXTENSION" in + let extra = + match field_find fields "LENGTH" with + | Some l -> " LENGTH " ^ l + | None -> "" + in + Printf.sprintf "SPIRALTYPE %s %s%s" typ kind extra + end + +type member_info = { kind : string; deviation : string list } + +let rec parse_tagged_body typ dim c = + match String.uppercase_ascii typ with + | "CIRCLE" -> + parse_point_body dim c ~arity_min:3 ~arity_exact:(Some 3) ~empty_ok:true + | "GEODESICSTRING" -> + parse_point_body dim c ~arity_min:2 ~arity_exact:None ~empty_ok:true + | "CIRCULARSTRING" | "LINESTRING" -> + parse_point_body dim c ~arity_min:1 ~arity_exact:None ~empty_ok:true + | "CLOTHOID" -> parse_clothoid dim c + | "NURBSCURVE" -> parse_nurbs dim c + | "SPIRALCURVE" -> parse_spiral dim c + | "ELLIPTICALCURVE" -> parse_elliptical dim c + | "COMPOUNDCURVE" | "CURVEPOLYGON" -> parse_compound dim c + | other -> raise (Parse ("unsupported member " ^ other)) + +and parse_one_member dim c = + skip_ws c; + match peek c with + | Some '(' -> + let pts = read_point_list c in + check_point_dim dim pts; + { kind = "LINESTRING_BARE"; deviation = [] } + | Some ch when is_letter ch -> + let raw = read_word c in + let typ0, attached = split_type_and_dim raw in + let typ = String.uppercase_ascii typ0 in + let mdim = read_optional_dim c attached in + if mdim <> XY && mdim <> dim then raise (Parse "DIM_CONFLICT"); + let use_dim = if mdim = XY then dim else mdim in + ignore (parse_tagged_body typ use_dim c); + let deviation = if typ = "LINESTRING" then ["TAGGED_LINESTRING"] else [] in + { kind = typ; deviation } + | _ -> raise (Parse "expected compound member") + +and parse_member_list dim c = + expect_char c '('; + skip_ws c; + if peek c = Some ')' then begin + c.i <- c.i + 1; + [] + end else + let rec rest acc = + skip_ws c; + match peek c with + | Some ')' -> c.i <- c.i + 1; List.rev acc + | Some ',' -> + c.i <- c.i + 1; + rest (parse_one_member dim c :: acc) + | Some x -> raise (Parse (Printf.sprintf "expected ',' or ')', got '%c'" x)) + | None -> raise (Parse "unterminated member list") + in + rest [parse_one_member dim c] + +and parse_compound dim c = + if at_empty c then "EMPTY" + else + let ms = parse_member_list dim c in + let n = List.length ms in + let devs = + List.concat (List.map (fun m -> m.deviation) ms) + |> List.sort_uniq String.compare + in + let kinds = String.concat "," (List.map (fun m -> m.kind) ms) in + let extra = + if devs = [] then "" else " DEVIATION " ^ String.concat "," devs + in + Printf.sprintf "MEMBERS %d [%s]%s" n kinds extra + +let recognized = function + | "POINT" | "LINESTRING" | "POLYGON" | "MULTIPOINT" + | "MULTILINESTRING" | "MULTIPOLYGON" | "GEOMETRYCOLLECTION" + | "CIRCULARSTRING" | "COMPOUNDCURVE" | "CURVEPOLYGON" + | "MULTICURVE" | "MULTISURFACE" | "TRIANGLE" | "TIN" + | "POLYHEDRALSURFACE" -> true + | _ -> false + +let instantiable_zoo = function + | "CIRCLE" | "GEODESICSTRING" | "ELLIPTICALCURVE" + | "NURBSCURVE" | "CLOTHOID" | "SPIRALCURVE" -> true + | _ -> false + +let skip_balanced_or_empty c = + if at_empty c then () + else begin + skip_ws c; + match peek c with + | Some '(' -> ignore (read_balanced_group c) + | _ -> raise (Parse "expected EMPTY or '('") + end + +let type_letters_casefold raw = + let buf = Buffer.create 16 in + String.iter (fun ch -> if is_letter ch then Buffer.add_char buf ch) raw; + let letters = Buffer.contents buf in + letters <> "" && letters <> String.uppercase_ascii letters + +let parse_line raw = + try + let c = { s = raw; i = 0 } in + skip_ws c; + if eof c then raise (Parse "empty input"); + let raw_typ = read_word c in + let typ0, attached = split_type_and_dim raw_typ in + let typ = String.uppercase_ascii typ0 in + if typ = "" then raise (Parse ("UNKNOWN " ^ String.uppercase_ascii raw_typ)); + let dim = read_optional_dim c attached in + let specialized = + instantiable_zoo typ || typ = "CIRCULARSTRING" + || typ = "COMPOUNDCURVE" || typ = "CURVEPOLYGON" + in + if not specialized && not (recognized typ) then + "UNKNOWN " ^ typ + else begin + let body = + if specialized then parse_tagged_body typ dim c + else begin + skip_balanced_or_empty c; + "RECOGNIZED" + end + in + finish c; + let fold = if type_letters_casefold raw_typ then " CASEFOLD" else "" in + Printf.sprintf "OK %s %s %s%s" typ (dim_string dim) body fold + end + with + | Parse msg -> + if String.length msg >= 8 && String.sub msg 0 8 = "UNKNOWN " then msg + else "REFUSE " ^ msg + | Invalid_argument _ -> + "REFUSE PARSE" diff --git a/oracle/sqlmm_wkt_main.ml b/oracle/sqlmm_wkt_main.ml new file mode 100644 index 00000000..7d189555 --- /dev/null +++ b/oracle/sqlmm_wkt_main.ml @@ -0,0 +1,20 @@ +(* Standalone stdin protocol for SQLMM_WKT — used when oracle_bin is not + rebuilt locally. Same request/reply as driver.ml mode SQLMM_WKT. *) + +let rec loop () = + match try Some (input_line stdin) with End_of_file -> None with + | None -> () + | Some raw -> + let line = String.trim raw in + if line = "" then loop () + else if line = "SQLMM_WKT" then begin + let wkt = input_line stdin in + print_endline (Sqlmm_wkt.parse_line wkt); + flush stdout; + loop () + end else begin + prerr_endline ("sqlmm_wkt_bin: expected SQLMM_WKT, got " ^ line); + exit 2 + end + +let () = loop ()