docs+oracle: SQL/MM type honesty packet + SQLMM_WKT - #660
Open
grootstebozewolf wants to merge 5 commits into
Open
docs+oracle: SQL/MM type honesty packet + SQLMM_WKT#660grootstebozewolf wants to merge 5 commits into
grootstebozewolf wants to merge 5 commits into
Conversation
Fold the four sibling type-honesty letters into one packet so TRIAGE, the prose gate, and the ticket index stop colliding. Four leftovers stay distinct. HOLD implement stays lifted only for ticket 30. Co-authored-by: jbloemscheer <jbloemscheer@gmail.com>
This was referenced Sep 1, 2026
grootstebozewolf
marked this pull request as ready for review
September 1, 2026 02:13
GEOS named the four leftovers. Ticket 30 refuses via ensureNoCurvedComponents and stamps via getLinearized. Ticket 36 stamps via restrictToSurfaces hasCurvedTypes. Tickets 32/34 pin OverlayNG type identity. No new Coq lemma. F-CP / F-MC / F-MS / V-CP do not flip. Co-authored-by: jbloemscheer <jbloemscheer@gmail.com>
ST_Clothoid, ST_Circle, ST_GeodesicString, ST_NURBSCurve, and ST_SpiralCurve sit in the ISO/IEC 13249-3 hierarchy. GEOS WKT refuses them as SQL/MM types. Do not remint 508. Not leftover XI. Co-authored-by: jbloemscheer <jbloemscheer@gmail.com>
Structural I/O identity for CLOTHOID, CIRCLE, GEODESICSTRING, NURBSCURVE, and SPIRALCURVE (plus instantiable ELLIPTICALCURVE). SPIRALTYPE is an open set: the text lexer reads up to comma or parenthesis and keeps interior spaces, so Wiener Bogen parses. No length mint, no CurveSegment growth, no 508 remint. Co-authored-by: jbloemscheer <jbloemscheer@gmail.com>
NTS WKTReader now matches GEOS: CLOTHOID / CIRCLE / GEODESICSTRING / NURBSCURVE / SPIRALCURVE are instantiable, not Unknown type. Co-authored-by: jbloemscheer <jbloemscheer@gmail.com>
4 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Wayfinder packet plus the GEOS implement letter for the four SQL/MM type-honesty leftovers (ISO/IEC 13249-3), the structural
SQLMM_WKToracle, and the NTS named refuse. One Proofs PR so TRIAGE, the prose gate, and the ticket index do not collide.Merge comment (one sentence). COMPOUNDCURVE, CURVEPOLYGON, MULTICURVE, and MULTISURFACE stay first-class SQL/MM types; GEOS now names the leftover (hull refuse +
getLinearized, OverlayNG type identity,restrictToSurfacesviahasCurvedTypes) and named linear fallback stays named. ST_Clothoid, ST_Circle, ST_GeodesicString, ST_NURBSCurve, and ST_SpiralCurve are instantiable in §4.2.1 — not optional extras — oracleSQLMM_WKTparses their type identity, and NTS WKT names them and refuses (matching GEOS).Destination
Name the four leftovers so a later session cannot steal a closed letter, steal tracker 509, or treat WKT/WKB round-trip as overlay honesty.
/implement 660on GEOS pointed at one named site per leftover.Living files:
docs/scout/map-compoundcurve.md(WKB 9)docs/scout/map-curvepolygon.md(WKB 10)docs/scout/map-multicurve.md(WKB 11)docs/scout/map-multisurface.md(WKB 12)Tickets
ensureNoCurvedComponentsrefuses and namesgetLinearized.createSurfacekeep CURVEPOLYGON.CascadedPolygonUnion::restrictToSurfacescheckshasCurvedTypes.SQLMM_WKT(oracle/sqlmm_wkt.ml) parses CLOTHOID, CIRCLE, GEODESICSTRING, NURBSCURVE, SPIRALCURVE (and instantiable ELLIPTICALCURVE). Red tests inoracle/red_sqlmm_wkt_tests.py.WKTReadernames those types and refuses. Genuine unknown tokens still sayUnknown type. CIRCLE does not steal CIRCULARSTRING.Engine letters: grootstebozewolf/geos PR 9; grootstebozewolf/NetTopologySuite PR 21.
§4.2.1 + SQLMM_WKT + NTS refuse
ST_Clothoid,ST_Circle,ST_GeodesicString,ST_NURBSCurve, andST_SpiralCurveare instantiable ST_Curve subtypes in ISO/IEC 13249-3 §4.2.1. They are not optional extras. GEOS and NTS WKT name them and refuse. The Proofs oracle parses type identity; it does not growCurveSegmentand does not remint 508.SPIRALTYPE deviation. The standard writes
<spiraltype text>as free-form<letters>, 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, so the lexer reads up to the comma or parenthesis that terminates the value. Interior spaces are preserved (SPIRALTYPE Wiener Bogenparses as an open-set extension). A name containing a comma or a parenthesis is the one case this grammar cannot represent.Other documented deviations pinned by the same mode: keyword case-fold (
CASEFOLD) and tagged LINESTRING inside COMPOUNDCURVE (DEVIATION TAGGED_LINESTRING).Honesty
Four leftovers, four types:
COMPOUNDCURVE— ticket 30. GEOS refuse + named stamp.POLYGON/LinearRingemit ofCURVEPOLYGON— ticket 32. GEOS OverlayNG keeps the type.MULTILINESTRINGemit ofMULTICURVE— ticket 34. GEOS OverlayNG keeps the type. Coq has no MultiCurve carrier.MULTIPOLYGONemit ofMULTISURFACE— ticket 36. GEOSrestrictToSurfacesno longer packs all-linear CurvePolygon into MultiPolygon.CurveGeometry.v : valid_curve_geometryis structural F-MS, not overlay honesty.Named
Linearize/toLinear/chord_approx_ring/to_geometry/ OverlayNGCurveAPPROX+isApproximate()/ GEOSgetLinearizedstays named.Jordan true-region stays on tracker 509. F-CP / F-MC / F-MS / V-CP TRIAGE rows do not flip. JTS #27 is out. JTS #38 (Option C DCEL) stays off JTS 7. No public noder. No type-9/10/11/12 reader PR. No GEO-TIN 15–17. Cite 13249-3. No DOI. JTS leftover overlay sites stay an engine grill and are not reminted here.
Supersedes the four colliding letters on
cursor/compoundcurve-wayfinder-ccfa,cursor/curvepolygon-wayfinder-ccfa,cursor/multicurve-wayfinder-ccfa, andcursor/multisurface-wayfinder-ccfa.topics: arc, wkt
claimId: none
witness: none