Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
31 changes: 25 additions & 6 deletions dag/std/orthogonal_geometry.dag
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ import std.nat { Nat }
import std.measure { Millimeter, millimeter, SignedMillimeterComponent, signed_millimeter_component, signed_millimeter_component_count }
import std.checked_arithmetic { IntegerOverflow }
import std.coordinate_frame { CoordinateFrameIdentity, coordinate_frame_identity_eq }
import std.spatial_frame { FrameExtent, SpatialFrameRegistry, extent_in_frame }
import std.affine_space { Point2, Point3, point2, point3 }
import std.euclidean_geometry {
AxisDirection3, PositiveX, NegativeX, PositiveY, NegativeY, PositiveZ, NegativeZ,
Expand Down Expand Up @@ -177,11 +178,21 @@ fn segment2_frame(s: AxisAlignedSegment2) -> CoordinateFrameIdentity { s.frame }

// Length is exact and nonnegative: one coordinate difference, magnitude taken. No root is involved
// precisely because the segment is axis-aligned, which is the property the carrier guarantees.
fn segment2_length(s: AxisAlignedSegment2) -> Millimeter {
//
// THE UNIT IS THE FRAME'S, NOT THIS FUNCTION'S. An earlier revision returned Millimeter, which was
// true only because every frame the layer had been asked to hold was a millimetre frame. It is the
// reader that committed, never the carrier: a segment holds signed components and does not know
// what they measure. Handed a board frame the old reader answered a whole-millimetre count of a
// micrometre extent — 0 for a 500 um pitch — so the shape did not lose accuracy, it lost the
// distinction between two adjacent pins. The extent is now read in the frame's registered unit and
// an unregistered frame refuses rather than defaulting. The millimetre answer is still available
// and is now DERIVED: frame_length_as_millimeter over this, which refuses when the frame is not a
// millimetre frame instead of truncating into one.
fn segment2_extent(registry: SpatialFrameRegistry, s: AxisAlignedSegment2) -> FrameExtent {
let dx = signed_millimeter_component_count(m: s.end.x) - signed_millimeter_component_count(m: s.start.x)
let dy = signed_millimeter_component_count(m: s.end.y) - signed_millimeter_component_count(m: s.start.y)
let d = dx + dy
millimeter(count: if d < 0 { 0 - d } else { d })
extent_in_frame(registry: registry, identity: s.frame, count: if d < 0 { 0 - d } else { d })
}

// AN AXIS-ALIGNED RECTANGLE, held as its two extreme corners rather than as an origin plus a width
Expand Down Expand Up @@ -215,12 +226,20 @@ fn rectangle2_min(r: AxisAlignedRectangle2) -> Point2 { r.min }
fn rectangle2_max(r: AxisAlignedRectangle2) -> Point2 { r.max }
fn rectangle2_frame(r: AxisAlignedRectangle2) -> CoordinateFrameIdentity { r.frame }

fn rectangle2_width(r: AxisAlignedRectangle2) -> Millimeter {
millimeter(count: signed_millimeter_component_count(m: r.max.x) - signed_millimeter_component_count(m: r.min.x))
fn rectangle2_width(registry: SpatialFrameRegistry, r: AxisAlignedRectangle2) -> FrameExtent {
extent_in_frame(
registry: registry,
identity: r.frame,
count: signed_millimeter_component_count(m: r.max.x) - signed_millimeter_component_count(m: r.min.x)
)
}

fn rectangle2_height(r: AxisAlignedRectangle2) -> Millimeter {
millimeter(count: signed_millimeter_component_count(m: r.max.y) - signed_millimeter_component_count(m: r.min.y))
fn rectangle2_height(registry: SpatialFrameRegistry, r: AxisAlignedRectangle2) -> FrameExtent {
extent_in_frame(
registry: registry,
identity: r.frame,
count: signed_millimeter_component_count(m: r.max.y) - signed_millimeter_component_count(m: r.min.y)
)
}

// AN AXIS-PERPENDICULAR PLANE, named by the axis it is perpendicular TO and the coordinate at which
Expand Down
21 changes: 21 additions & 0 deletions dag/std/spatial_frame.dag
Original file line number Diff line number Diff line change
Expand Up @@ -163,3 +163,24 @@ fn frame_length_as_micrometer(l: FrameLength) -> LengthProjection<Micrometer> {
LengthProjectionRefused { cause: LengthScaleMismatch { held: l.scale, requested: Micro } }
}
}

// READING AN EXTENT OUT OF A SHAPE, IN THE UNIT THE SHAPE'S OWN FRAME WAS REGISTERED WITH. This
// is the join the geometry layer was missing. Its shape carriers are scale-AGNOSTIC — a rectangle
// holds signed components and never commits to what they measure — so the commitment lived
// entirely in the readers, which named millimetres and were right only because every frame in the
// corpus happened to be a millimetre frame. A board is the counterexample, and the repair is to
// derive the unit from the frame rather than to assert it.
//
// UNREGISTERED REFUSES, and it matters more here than at the lookup: a reader that fell back to
// millimetres would answer 20 for a package body that is 20000 micrometres across, which is a
// plausible number for a real question and would be believed.
type FrameExtent
= ExtentInFrame { length: FrameLength }
| ExtentFrameUnregistered { identity: CoordinateFrameIdentity }

fn extent_in_frame(registry: SpatialFrameRegistry, identity: CoordinateFrameIdentity, count: Nat) -> FrameExtent {
match frame_length_scale(r: registry, identity: identity) {
Absent => ExtentFrameUnregistered { identity: identity }
Present { value: s } => ExtentInFrame { length: frame_length(scale: s, count: count) }
}
}
119 changes: 113 additions & 6 deletions dag/test/claim/orthogonal_geometry_witness_test.dag
Original file line number Diff line number Diff line change
@@ -1,8 +1,25 @@
module test.claim.orthogonal_geometry_witness

import std.types { Bool, Int, List }
import std.measure { millimeter_count, signed_millimeter_component_count }
import std.measure { millimeter_count, signed_millimeter_component_count, measure_count }
import std.coordinate_frame { CoordinateFrameIdentity, coordinate_frame_identity, coordinate_frame_identity_eq }
import std.measure { Micro, Milli }
import std.nat { Nat }
import std.spatial_frame {
ExtentFrameUnregistered,
ExtentInFrame,
FrameExtent,
FrameRegistered,
FrameRegistrationRefused,
LengthProjected,
LengthProjectionRefused,
SpatialFrameRegistry,
empty_frame_registry,
frame_length_as_micrometer,
frame_length_as_millimeter,
register_frame,
registry_with,
}
import std.affine_space { Point2, Point3, point2, point3 }
import std.euclidean_geometry {
AxisDirection3, PositiveX, NegativeX, PositiveY, NegativeY, PositiveZ, NegativeZ,
Expand All @@ -16,7 +33,7 @@ import std.orthogonal_geometry {
LoopEdgesNotPerpendicular, LoopSelfIntersects, RotationAxesParallel,
BoundingBoxHasNoPoints,
OrthogonalRotation3, orthogonal_rotation3, rotation_x_image, rotation_y_image, rotation_z_image,
AxisAlignedSegment2, axis_aligned_segment2, segment2_axis, segment2_length,
AxisAlignedSegment2, axis_aligned_segment2, segment2_axis, segment2_extent,
AxisAlignedRectangle2, axis_aligned_rectangle2, rectangle2_width, rectangle2_height,
Plane3, plane3, plane3_contains_point, plane3_normal_axis,
AxisAlignedBox3, axis_aligned_box3, box3_contains_point, box3_overlaps,
Expand All @@ -33,6 +50,35 @@ fn room() -> CoordinateFrameIdentity { coordinate_frame_identity(occurrence: 1)
fn building() -> CoordinateFrameIdentity { coordinate_frame_identity(occurrence: 2) }

fn p2(x: Int, y: Int) -> Point2 { point2(frame: room(), x: x, y: y) }

// Both frames these tests draw in are millimetre frames, which is exactly the fact the readers
// used to assume and now have to be told. Registering them is what keeps every length assertion
// below meaning what it always meant.
fn mm_registry() -> SpatialFrameRegistry {
let r0 = empty_frame_registry()
let r1 = match register_frame(r: r0, identity: room(), length_scale: Milli) {
FrameRegistered { frame: f } => registry_with(r: r0, f: f)
FrameRegistrationRefused { cause: _ } => r0
}
match register_frame(r: r1, identity: building(), length_scale: Milli) {
FrameRegistered { frame: f } => registry_with(r: r1, f: f)
FrameRegistrationRefused { cause: _ } => r1
}
}

// An extent measures a stated number of millimetres. Every arm other than the one that projects
// answers false, so an unregistered frame or a non-millimetre frame fails the assertion rather
// than being quietly read as a count.
fn extent_is_mm(e: FrameExtent, want: Nat) -> Bool {
match e {
ExtentFrameUnregistered { identity: _ } => false
ExtentInFrame { length: l } =>
match frame_length_as_millimeter(l: l) {
LengthProjectionRefused { cause: _ } => false
LengthProjected { value: v } => millimeter_count(m: v) == want
}
}
}
fn p3(x: Int, y: Int, z: Int) -> Point3 { point3(frame: room(), x: x, y: y, z: z) }

// EVERY NEGATIVE CONTROL BELOW HAS A POSITIVE SIBLING IN THE SAME WITNESS. A mint that refused
Expand Down Expand Up @@ -75,11 +121,11 @@ test fn segment_walls_hold() -> Bool {
let axis_aligned = match axis_aligned_segment2(start: p2(x: 0, y: 0), end: p2(x: 3000, y: 0)) {
OrthogonalReady { value: s } =>
match segment2_axis(s: s) { Axis2X => true Axis2Y => false }
&& millimeter_count(m: segment2_length(s: s)) == 3000
&& extent_is_mm(e: segment2_extent(registry: mm_registry(), s: s), want: 3000)
OrthogonalRefused { cause: _ } => false
}
let negative_direction_still_positive_length = match axis_aligned_segment2(start: p2(x: 0, y: 500), end: p2(x: 0, y: 0 - 500)) {
OrthogonalReady { value: s } => millimeter_count(m: segment2_length(s: s)) == 1000
OrthogonalReady { value: s } => extent_is_mm(e: segment2_extent(registry: mm_registry(), s: s), want: 1000)
OrthogonalRefused { cause: _ } => false
}
let degenerate = match axis_aligned_segment2(start: p2(x: 7, y: 7), end: p2(x: 7, y: 7)) {
Expand Down Expand Up @@ -117,7 +163,7 @@ test fn box_and_rectangle_walls_hold() -> Bool {
let flat_z = refusal_is_extent_not_positive(r: axis_aligned_box3(min: p3(x: 0, y: 0, z: 0), max: p3(x: 4000, y: 3000, z: 0)), axis: Axis3Z)
let inverted = refusal_is_extent_not_positive(r: axis_aligned_box3(min: p3(x: 0, y: 0, z: 0), max: p3(x: 0 - 10, y: 3000, z: 2400)), axis: Axis3X)
let good_rect = match axis_aligned_rectangle2(min: p2(x: 0, y: 0), max: p2(x: 1200, y: 800)) {
OrthogonalReady { value: r } => millimeter_count(m: rectangle2_width(r: r)) == 1200 && millimeter_count(m: rectangle2_height(r: r)) == 800
OrthogonalReady { value: r } => extent_is_mm(e: rectangle2_width(registry: mm_registry(), r: r), want: 1200) && extent_is_mm(e: rectangle2_height(registry: mm_registry(), r: r), want: 800)
OrthogonalRefused { cause: _ } => false
}
let thin_rect = match axis_aligned_rectangle2(min: p2(x: 0, y: 0), max: p2(x: 1200, y: 0)) {
Expand Down Expand Up @@ -271,7 +317,7 @@ test fn plane_surface_and_prism_hold() -> Bool {
let surface = match axis_aligned_rectangle2(min: p2(x: 0, y: 0), max: p2(x: 4000, y: 3000)) {
OrthogonalRefused { cause: _ } => false
OrthogonalReady { value: rect } =>
millimeter_count(m: rectangle2_width(r: surface3_extent(s: axis_aligned_surface3(offset: 0, extent: rect)))) == 4000
extent_is_mm(e: rectangle2_width(registry: mm_registry(), r: surface3_extent(s: axis_aligned_surface3(offset: 0, extent: rect))), want: 4000)
}
let surface_plane_is_derived = match axis_aligned_rectangle2(min: point2(frame: building(), x: 0, y: 0), max: point2(frame: building(), x: 10, y: 10)) {
OrthogonalRefused { cause: _ } => false
Expand Down Expand Up @@ -299,3 +345,64 @@ test fn plane_surface_and_prism_hold() -> Bool {
}
on_plane && off_plane && other_frame_not_on_plane && surface && surface_plane_is_derived && prism && flat_prism
}

// THE CASE THE OLD READER ANSWERED WRONGLY, and the reason this reader takes a registry at all.
// The board frame is registered in micrometres. The SAME rectangle carrier, holding the same
// components, is a 20000 um package body — 20 mm — and the old reader would have called it 20000
// millimetres, a twenty-metre chip. Nothing about the carrier changed; the reader stopped
// asserting a unit it was never told.
//
// Read as micrometres it answers. Read as millimetres it REFUSES rather than dividing, because
// this reader is not a converter: the caller asked what the shape measures, not for a change of
// unit, and a 500 um pitch has no whole-millimetre answer at all.
fn board() -> CoordinateFrameIdentity { coordinate_frame_identity(occurrence: 77) }

fn micro_registry() -> SpatialFrameRegistry {
let r0 = empty_frame_registry()
match register_frame(r: r0, identity: board(), length_scale: Micro) {
FrameRegistered { frame: f } => registry_with(r: r0, f: f)
FrameRegistrationRefused { cause: _ } => r0
}
}

test fn a_reader_takes_the_unit_from_the_frame_not_from_itself() -> Bool {
match axis_aligned_rectangle2(
min: point2(frame: board(), x: 0, y: 0),
max: point2(frame: board(), x: 20000, y: 20000)
) {
OrthogonalRefused { cause: _ } => false
OrthogonalReady { value: rect } =>
match rectangle2_width(registry: micro_registry(), r: rect) {
ExtentFrameUnregistered { identity: _ } => false
ExtentInFrame { length: l } =>
// BOTH HALVES, AND THE FIRST IS THE DELIVERABLE. An earlier revision of this test
// asserted only that the millimetre projection refuses, which every wrong answer also
// satisfies: a reader returning 200 instead of 20000 would have passed it, and the
// reader's actual job — returning the extent in the frame's registered unit — went
// unwitnessed. The count is asserted first, then the refusal.
match frame_length_as_micrometer(l: l) {
LengthProjectionRefused { cause: _ } => false
LengthProjected { value: um } =>
measure_count(m: um) == 20000
&& match frame_length_as_millimeter(l: l) {
LengthProjected { value: _ } => false
LengthProjectionRefused { cause: _ } => true
}
}
}
}
}

// An unregistered frame has no unit, and a reader that fell back to millimetres would answer a
// plausible number for a real question. The registry above holds the board frame only.
test fn an_unregistered_frame_refuses_rather_than_measuring() -> Bool {
match axis_aligned_rectangle2(min: p2(x: 0, y: 0), max: p2(x: 1200, y: 800)) {
OrthogonalRefused { cause: _ } => false
OrthogonalReady { value: rect } =>
match rectangle2_width(registry: micro_registry(), r: rect) {
ExtentInFrame { length: _ } => false
ExtentFrameUnregistered { identity: _ } => true
}
}
}