# Predicates and shapes

The predicates `geo.contains`, `geo.within` and `geo.intersects` answer
yes-or-no questions about where things are, and `geo.centroid` and
`geo.bounding_box` give a shape a place for its label and a view that
shows it. Here the bakery uses them on its delivery patches, its pins on
a map and its shops:

```jadpo
type Delivers = Bool {}

type InView = Bool {}

type WalkingReach = Length {
    min: 0metre
}

/// Whether a customer is inside one of the bakery's patches.
function delivers_to(patches: List<Polygon>, customer: Point) -> Delivers {
    return Delivers(list.any(patches, patch -> geo.contains(patch, customer)))
}

/// Whether a van's round passes through a patch.
function passes_through(van_round: LineString, patch: Polygon) -> Delivers {
    return Delivers(geo.intersects(van_round, patch))
}

/// Whether a shop's pin is inside the map a person is looking at.
function in_view(shop_pin: Point, view: BoundingBox) -> InView {
    return InView(geo.within(shop_pin, view))
}

/// Whether two shops are near enough to walk between.
function walkable(from: Point, to: Point, walking_distance: WalkingReach) -> InView {
    return InView(geo.within(from, to, distance: walking_distance))
}

/// Where a patch's name goes on the map.
function label_at(patch: Polygon) -> Point {
    return geo.centroid(patch)
}

/// The view that shows a whole patch.
function view_of(patch: Polygon) -> BoundingBox {
    return geo.bounding_box(patch)
}
```

A customer on a patch's edge is inside it. The patch's northern edge is a
great circle, so it bows north past 51.54° N between its corners. A box's
sides are parallels and meridians, so the box that shows the whole patch
reaches a little further north than its corners:

```jadpo
test "a customer on a patch's edge is delivered to" {
    var patch: Polygon = Polygon {
        outer: [
            Point {
                latitude: 51.49
                longitude: -0.2
                altitude: none
            },
            Point {
                latitude: 51.49
                longitude: -0.05
                altitude: none
            },
            Point {
                latitude: 51.54
                longitude: -0.05
                altitude: none
            },
            Point {
                latitude: 51.54
                longitude: -0.2
                altitude: none
            },
            Point {
                latitude: 51.49
                longitude: -0.2
                altitude: none
            }
        ]
        holes: []
    }
    var big_ben: Point = Point {
        latitude: 51.5007
        longitude: -0.1246
        altitude: none
    }
    var on_the_edge: Point = Point {
        latitude: 51.5
        longitude: -0.2
        altitude: none
    }
    var eiffel_tower: Point = Point {
        latitude: 48.8566
        longitude: 2.3522
        altitude: none
    }
    assert delivers_to([patch], big_ben)
    assert delivers_to([patch], on_the_edge)
    assert not delivers_to([patch], eiffel_tower)
    assert in_view(big_ben, view_of(patch))
    assert not in_view(eiffel_tower, view_of(patch))
    assert walkable(big_ben, on_the_edge, 6km)
    assert not walkable(big_ben, on_the_edge, 5km)
}

test "a patch's label and the view that shows it" {
    var patch: Polygon = Polygon {
        outer: [
            Point {
                latitude: 51.49
                longitude: -0.2
                altitude: none
            },
            Point {
                latitude: 51.49
                longitude: -0.05
                altitude: none
            },
            Point {
                latitude: 51.54
                longitude: -0.05
                altitude: none
            },
            Point {
                latitude: 51.54
                longitude: -0.2
                altitude: none
            },
            Point {
                latitude: 51.49
                longitude: -0.2
                altitude: none
            }
        ]
        holes: []
    }
    assert label_at(patch).latitude == 51.51501933808094
    assert label_at(patch).longitude == -0.12499999998684845
    assert view_of(patch).north == 51.54002390691161
    assert view_of(patch).south == 51.49
}
```

## Polygons are valid when built

Jadpo checks every polygon when it is built or read, so no operation,
query or other system ever meets one whose edges cross. A `Polygon` is
valid when, on the sphere:

- each ring is closed, with four points or more;
- no ring crosses or touches itself, except where its last point meets
  its first. A point repeated in a row, or a ring that turns straight
  back along an edge, touches itself;
- each hole lies inside the outer ring, and no two rings cross, overlap
  or share even one point. The OGC standard lets a hole touch the outer
  ring at one point; Jadpo doesn't, which also keeps a polygon's inside
  in one piece without a check of its own;
- every edge is shorter than half the globe (180° of arc), so the great
  circle it follows is the only one;
- the polygon covers less than half the globe. PostGIS's `geography`
  reads a ring wound either way as the same, smaller area (verified), so
  a ring meant to enclose the larger side couldn't be stored as meant.

A ring's inside is its smaller side, as PostGIS reads it, whichever way
the ring is wound. Jadpo picks the smaller side from the ring's area on
the sphere, added up by Van Oosterom and Strackee's formula in its whole
numbers. The choice is exact unless the two sides are within about
10⁻³⁵ of each other. A ring that lies exactly on one great circle, so
both sides are equal, breaks the rule. A `MultiPolygon` has no rule of
its own: each of its polygons is valid, and they may overlap.

A polygon read from GeoJSON or WKT that isn't valid is refused, `format`
at the ring's place, as the standard library's other checks on reading
are ([Every boundary through the contract](every-boundary-through-the-contract.md)).
A polygon built in code that isn't valid breaks a named rule,
`rings_valid`, which you map like any rule across fields
([Rules across fields](objects.md#rules-across-fields)).

Checking takes time in proportion to about n log n of the points, since
it sweeps over the edges: 0.6 ms for 100 points, 6.8 ms for 1,000 and
68 ms for a country's outline of 10,000 (measured natively on an Apple
M1 Pro).

## Altitudes are all or nothing

Every position in one geometry has an altitude, or none does. WKT can't
write a mix, and PostGIS refuses one ("can not mix dimensionality in a
geometry", verified), so a geometry that mixed them couldn't be stored or
exchanged. A `Point` has one position, so it always agrees. A
multi-geometry's parts must agree with each other.

A mixed geometry read from GeoJSON or WKT is refused, `format` at the
first position of the other size. One built in code breaks a named rule,
`altitudes_agree`, which you map as you map `rings_valid`.

- **Reading.** GeoJSON is checked once the whole geometry is read, every
  position in the order written, and refused `format` at the first of the
  other size (`coordinates.1.0.2`). A multi-geometry's parts are checked
  against each other. WKT's reader refuses a mix at that position too, as
  `malformed`, its one condition for text that isn't a geometry.
- **What a literal decides.** `altitudes_agree` reads each `Point`
  written out in a geometry literal, however deep: a line's points, a
  polygon's rings, a multi-polygon's polygons. An altitude written `none`
  is none. One written out, or of a type that can't be `none` (a
  distance), is one. Anything else, such as a point or a list held in a
  variable, is known only when the program runs. If some positions are
  known to have an altitude and others known to have none, the literal is
  `type.invalid_literal` at the part holding the first of the other size,
  whatever else is unknown. Otherwise the literal is attempted, as it is
  for `rings_valid`. So a line from points held in variables is
  attempted, even when each variable holds a literal: the checker doesn't
  follow a variable's value, here or for `rings_valid`.
- **A polygon's rules in order.** `rings_valid` is checked first, then
  `altitudes_agree`, so a literal or a value that breaks both names
  `rings_valid`. GeoJSON and WKT likewise check a ring before the
  positions' sizes.
- **Nothing later meets a mix.** Storage stores every geometry without
  checking it again, and `geo.to_wkt` never meets a geometry it can't
  write. A mixed geometry that somehow got past every check is the
  runtime's "value of a kind the checker would have refused". The
  PostgreSQL driver refuses to encode a shape that mixes them, since
  EWKB's type flag covers the whole geometry. Each geometry's examples
  under [Geospatial types](geospatial-types.md) hold
  every point at a height or none, and its refused examples include a
  mix.

A polygon built from values known only when the program runs is
attempted, and you map both rules:

```jadpo
type NotAPatch = Failure {
    kind: FailureKind.invalid_value
}

/// A patch from the corners a planner clicked, back to the first.
function patch_from(clicked: List<Point>, first: Point) fails NotAPatch -> Polygon {
    return attempt Polygon {
        outer: list.append(clicked, first)
        holes: []
    } {
        rings_valid: NotAPatch  // edges that cross, or a corner clicked twice
        altitudes_agree: NotAPatch  // corners at a height and on the ground
    }
}
```

```jadpo
test "a patch whose edges cross isn't one" {
    var bow_start: Point = Point {
        latitude: 0.0
        longitude: 0.0
        altitude: none
    }
    var bow_tie: List<Point> = [
        bow_start,
        Point {
            latitude: 10.0
            longitude: 10.0
            altitude: none
        },
        Point {
            latitude: 10.0
            longitude: 0.0
            altitude: none
        },
        Point {
            latitude: 0.0
            longitude: 10.0
            altitude: none
        }
    ]
    assert patch_from(bow_tie, bow_start) fails NotAPatch
}

test "a patch with one corner at a height isn't one" {
    var corner: Point = Point {
        latitude: 0.0
        longitude: 0.0
        altitude: none
    }
    var clicked: List<Point> = [
        corner,
        Point {
            latitude: 0.0
            longitude: 1.0
            altitude: 35metre
        },
        Point {
            latitude: 1.0
            longitude: 1.0
            altitude: none
        }
    ]
    assert patch_from(clicked, corner) fails NotAPatch
}
```

A polygon written out is checked while compiling:

```jadpo
/// The patch a planner drew, its edges crossing.
function drawn_patch() -> Polygon {
    return Polygon {
        outer: [
            Point {
                latitude: 51.49
                longitude: -0.2
                altitude: none
            },
            Point {
                latitude: 51.54
                longitude: -0.05
                altitude: none
            },
            Point {
                latitude: 51.49
                longitude: -0.05
                altitude: none
            },
            Point {
                latitude: 51.54
                longitude: -0.2
                altitude: none
            },
            Point {
                latitude: 51.49
                longitude: -0.2
                altitude: none
            }
        ]
        holes: []
    }
}
```

```text
error: This `Polygon` breaks its rule `rings_valid`
 --> main.jadpo:4:16
  |
4 |         outer: [
  |                ^ these rings don't make a valid polygon
  reason: A `Polygon`'s rings are closed with four points or more, never cross or meet themselves or each other, keep each hole inside the outer ring, and have every edge shorter than half the globe, so the polygon is the smaller side its outer ring bounds (area 20, "Polygons are valid when built"). A literal is checked while compiling.
  next: Close each ring and move its points so no edge meets another, with each hole inside the outer ring (agent)
  rule: type.invalid_literal
  help: https://jadpo.dev/docs/errors/type.invalid_literal

check failed: 1 error, 1 file
```