moonlight-triangulation-1.2.0.1: src-embedding/Moonlight/Triangulation/Internal/Overlay/Embedding.hs
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
-- | Bounded certification of local binary64 embedding obligations for a
-- declared exact arrangement draft.
module Moonlight.Triangulation.Internal.Overlay.Embedding
( DraftVertexId (..)
, DraftSegmentId (..)
, DraftSourceId (..)
, DraftIncidence (..)
, DraftNeighborhood (..)
, ExactArrangementDraft (..)
, DraftReference (..)
, OverlayEmbeddingObstruction (..)
, EmbeddingObligation (..)
, EmbeddingResidual
, residualUndischargedObligations
, milestoneOneResidual
, LocalEmbeddingCertificate (..)
, certifyLocalEmbedding
) where
import Control.DeepSeq (NFData)
import Data.List (sort, tails)
import qualified Data.List as List
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty as NonEmpty
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import GHC.Generics (Generic)
import Moonlight.Triangulation.Exact
( ExactPoint
, SegmentRelation
, exactOrient2d
, exactPointToEmbeddingCandidate
, exactSegmentRelation
)
import Moonlight.Triangulation.Internal.BoundaryCycle (cyclePairs)
import Moonlight.Triangulation.Internal.ExactRational (ExactRational)
import qualified Moonlight.Triangulation.Math as Math
( orient2d
, segmentRelation
)
import Moonlight.Triangulation.Types
( Point (..)
, PointValidationError
)
-- | Draft-local vertex label.
newtype DraftVertexId = DraftVertexId Int
deriving stock (Eq, Ord, Show, Generic)
deriving anyclass (NFData)
-- | Draft-local atomic-segment label.
newtype DraftSegmentId = DraftSegmentId Int
deriving stock (Eq, Ord, Show, Generic)
deriving anyclass (NFData)
-- | Draft-local source-segment label.
newtype DraftSourceId = DraftSourceId Int
deriving stock (Eq, Ord, Show, Generic)
deriving anyclass (NFData)
-- | A declared relation between two atomic draft segments.
data DraftIncidence = DraftIncidence
{ -- | First declared atomic segment.
draftIncidenceFirstSegment :: !DraftSegmentId
, -- | Second declared atomic segment.
draftIncidenceSecondSegment :: !DraftSegmentId
, -- | Relation declared to hold in both exact and rounded geometry.
draftIncidenceRelation :: !SegmentRelation
}
deriving stock (Eq, Ord, Show, Generic)
deriving anyclass (NFData)
-- | One exact vertex and the cyclic neighbor order declared around it.
data DraftNeighborhood = DraftNeighborhood
{ -- | Center of the declared local rotation.
draftNeighborhoodCenter :: !DraftVertexId
, -- | Neighbors in cyclic rotation order.
draftNeighborhoodNeighbors :: !(NonEmpty DraftVertexId)
}
deriving stock (Eq, Ord, Show, Generic)
deriving anyclass (NFData)
-- | A hand-built exact arrangement draft. It contains only declared local
-- structure; no arrangement or global crossing search is derived here.
data ExactArrangementDraft = ExactArrangementDraft
{ -- | Exact coordinates keyed by draft-local vertex identity.
draftVertices :: !(Map DraftVertexId ExactPoint)
, -- | Atomic segment endpoint identities.
draftSegments :: !(Map DraftSegmentId (DraftVertexId, DraftVertexId))
, -- | Exact split parameters and vertices in source-segment order.
draftSourceMemberships :: !(Map DraftSourceId [(ExactRational, DraftVertexId)])
, -- | Segment relations declared to remain invariant under projection.
draftIncidences :: ![DraftIncidence]
, -- | Cyclic local rotations declared to remain orientation-stable.
draftNeighborhoods :: ![DraftNeighborhood]
}
deriving stock (Eq, Show, Generic)
deriving anyclass (NFData)
-- | The typed identity of a missing draft reference.
data DraftReference
= DraftVertexReference !DraftVertexId
| DraftSegmentReference !DraftSegmentId
deriving stock (Eq, Ord, Show, Generic)
deriving anyclass (NFData)
-- | A witness that prevents local embedding certification.
data OverlayEmbeddingObstruction
= DraftReferenceMissing !DraftReference
| VertexProjectionRefused !DraftVertexId !PointValidationError
| RoundedVerticesCollide !DraftVertexId !DraftVertexId !Point
| SplitOrderNotPreserved !DraftSourceId !DraftVertexId !DraftVertexId
| IncidenceRelationChanged
!DraftSegmentId
!DraftSegmentId
!SegmentRelation
!SegmentRelation
!SegmentRelation
| NeighborhoodOrientationChanged
!DraftVertexId
!DraftVertexId
!DraftVertexId
!Ordering
!Ordering
| GlobalRelationAdded
!DraftSegmentId
!DraftSegmentId
!SegmentRelation
| GlobalRelationRemoved
!DraftSegmentId
!DraftSegmentId
!SegmentRelation
| GlobalRelationChanged
!DraftSegmentId
!DraftSegmentId
!SegmentRelation
!SegmentRelation
| ProjectedSegmentCollapsed
!DraftSegmentId
!DraftVertexId
!DraftVertexId
deriving stock (Eq, Show, Generic)
deriving anyclass (NFData)
-- | An embedding obligation not discharged by the bounded local certifier.
data EmbeddingObligation
= GlobalNoNewCrossing
deriving stock (Bounded, Enum, Eq, Ord, Show, Generic)
deriving anyclass (NFData)
-- | A nonempty collection of obligations deferred to a later owner.
newtype EmbeddingResidual = EmbeddingResidual (NonEmpty EmbeddingObligation)
deriving stock (Eq, Ord, Show, Generic)
deriving anyclass (NFData)
-- | Read the obligations that remain explicitly undischarged.
residualUndischargedObligations
:: EmbeddingResidual
-> NonEmpty EmbeddingObligation
residualUndischargedObligations (EmbeddingResidual obligations) = obligations
-- | The Milestone 1 residual: the arrangement sweep has not yet proved global
-- absence of new crossings.
milestoneOneResidual :: EmbeddingResidual
milestoneOneResidual = EmbeddingResidual (GlobalNoNewCrossing :| [])
-- | A certificate for exactly four local obligations on a declared draft:
-- vertex distinctness, source split order, declared incidences, and local
-- neighborhood orientation. Global absence of new crossings is unproved until
-- the Milestone 2 arrangement sweep supplies the complete obligation set.
data LocalEmbeddingCertificate = LocalEmbeddingCertificate
{ -- | Number of rounded vertex-pair distinctness checks discharged.
certificateRoundedVertexDistinctnessCount :: !Int
, -- | Number of adjacent source split-order checks discharged.
certificateSplitOrderPreservationCount :: !Int
, -- | Number of declared incidence checks discharged.
certificateIncidenceRelationPreservationCount :: !Int
, -- | Number of consecutive neighborhood orientation checks discharged.
certificateNeighborhoodOrientationStabilityCount :: !Int
, -- | The candidate projection certified by the four local obligations.
certificateRoundedVertices :: !(Map DraftVertexId Point)
, -- | The necessarily nonempty global obligation residual.
certificateResidual :: !EmbeddingResidual
}
deriving stock (Eq, Show, Generic)
deriving anyclass (NFData)
-- | Certify the four bounded local embedding obligations, collecting every
-- witness within each obligation and preserving obligation order.
certifyLocalEmbedding
:: ExactArrangementDraft
-> Either (NonEmpty OverlayEmbeddingObstruction) LocalEmbeddingCertificate
certifyLocalEmbedding draft =
case NonEmpty.nonEmpty (structuralObstructions draft) of
Just obstructions -> Left obstructions
Nothing ->
case projectVertices (draftVertices draft) of
Invalid obstructions -> Left obstructions
Valid projectedVertices ->
certifyProjectedDraft draft projectedVertices
data Validation value
= Invalid !(NonEmpty OverlayEmbeddingObstruction)
| Valid value
instance Functor Validation where
fmap _ (Invalid obstructions) = Invalid obstructions
fmap transform (Valid value) = Valid (transform value)
instance Applicative Validation where
pure = Valid
Invalid left <*> Invalid right = Invalid (left <> right)
Invalid obstructions <*> Valid _ = Invalid obstructions
Valid _ <*> Invalid obstructions = Invalid obstructions
Valid transform <*> Valid value = Valid (transform value)
invalid :: OverlayEmbeddingObstruction -> Validation value
invalid obstruction = Invalid (obstruction :| [])
data ProjectedVertex = ProjectedVertex
{ projectedExactPoint :: !ExactPoint
, projectedRoundedPoint :: !Point
}
data ResolvedSegment = ResolvedSegment
{ resolvedSegmentId :: !DraftSegmentId
, resolvedSegmentFrom :: !ResolvedVertex
, resolvedSegmentTo :: !ResolvedVertex
}
data ResolvedVertex = ResolvedVertex
{ resolvedVertexId :: !DraftVertexId
, resolvedProjectedVertex :: !ProjectedVertex
}
data ResolvedMembership = ResolvedMembership
{ resolvedMembershipParameter :: !ExactRational
, resolvedMembershipVertex :: !ResolvedVertex
}
structuralObstructions
:: ExactArrangementDraft
-> [OverlayEmbeddingObstruction]
structuralObstructions draft =
segmentEndpointObstructions
<> sourceMembershipObstructions
<> incidenceObstructions
<> neighborhoodObstructions
where
vertices = draftVertices draft
segments = draftSegments draft
missingVertex vertexId =
[ DraftReferenceMissing (DraftVertexReference vertexId)
| Map.notMember vertexId vertices
]
missingSegment segmentId =
[ DraftReferenceMissing (DraftSegmentReference segmentId)
| Map.notMember segmentId segments
]
segmentEndpointObstructions =
concatMap
(\(_, (from, to)) -> missingVertex from <> missingVertex to)
(Map.toAscList segments)
sourceMembershipObstructions =
concatMap
(concatMap (missingVertex . snd) . snd)
(Map.toAscList (draftSourceMemberships draft))
incidenceObstructions =
concatMap
( \incidence ->
missingSegment (draftIncidenceFirstSegment incidence)
<> missingSegment (draftIncidenceSecondSegment incidence)
)
(draftIncidences draft)
neighborhoodObstructions =
concatMap
( \neighborhood ->
missingVertex (draftNeighborhoodCenter neighborhood)
<> concatMap missingVertex (draftNeighborhoodNeighbors neighborhood)
)
(draftNeighborhoods draft)
projectVertices
:: Map DraftVertexId ExactPoint
-> Validation (Map DraftVertexId ProjectedVertex)
projectVertices =
Map.traverseWithKey
( \vertexId point ->
case exactPointToEmbeddingCandidate point of
Left projectionError ->
invalid (VertexProjectionRefused vertexId projectionError)
Right roundedPoint -> Valid (ProjectedVertex point roundedPoint)
)
certifyProjectedDraft
:: ExactArrangementDraft
-> Map DraftVertexId ProjectedVertex
-> Either (NonEmpty OverlayEmbeddingObstruction) LocalEmbeddingCertificate
certifyProjectedDraft draft projectedVertices =
case resolvedFailures of
Left obstruction -> Left (obstruction :| [])
Right localFailures ->
case NonEmpty.nonEmpty (collisionFailures <> localFailures) of
Just obstructions -> Left obstructions
Nothing ->
Right
LocalEmbeddingCertificate
{ certificateRoundedVertexDistinctnessCount = distinctnessCount
, certificateSplitOrderPreservationCount = splitOrderCount
, certificateIncidenceRelationPreservationCount = incidenceCount
, certificateNeighborhoodOrientationStabilityCount = neighborhoodCount
, certificateRoundedVertices = Map.map projectedRoundedPoint projectedVertices
, certificateResidual = milestoneOneResidual
}
where
collisionFailures = roundedVertexCollisionObstructions projectedVertices
resolvedFailures = do
splitFailures <- traverse (uncurry resolveSource) (Map.toAscList (draftSourceMemberships draft))
incidenceFailures <- traverse resolveIncidence (draftIncidences draft)
neighborhoodFailures <- traverse resolveNeighborhood (draftNeighborhoods draft)
pure (concat splitFailures <> concat incidenceFailures <> concat neighborhoodFailures)
resolveVertex vertexId =
case Map.lookup vertexId projectedVertices of
Nothing -> Left (DraftReferenceMissing (DraftVertexReference vertexId))
Just projectedVertex -> Right (ResolvedVertex vertexId projectedVertex)
resolveSegment segmentId =
case Map.lookup segmentId (draftSegments draft) of
Nothing -> Left (DraftReferenceMissing (DraftSegmentReference segmentId))
Just (from, to) ->
ResolvedSegment segmentId
<$> resolveVertex from
<*> resolveVertex to
resolveSource sourceId memberships =
splitOrderObstructions sourceId
<$> traverse
( \(parameter, vertexId) ->
ResolvedMembership parameter <$> resolveVertex vertexId
)
memberships
resolveIncidence incidence =
incidenceRelationObstructions
(draftIncidenceRelation incidence)
<$> resolveSegment (draftIncidenceFirstSegment incidence)
<*> resolveSegment (draftIncidenceSecondSegment incidence)
resolveNeighborhood neighborhood =
neighborhoodOrientationObstructions
<$> resolveVertex (draftNeighborhoodCenter neighborhood)
<*> traverse resolveVertex (draftNeighborhoodNeighbors neighborhood)
vertexCount = Map.size projectedVertices
distinctnessCount = vertexCount * (vertexCount - 1) `quot` 2
splitOrderCount =
sum
( map
(max 0 . subtract 1 . length)
(Map.elems (draftSourceMemberships draft))
)
incidenceCount = length (draftIncidences draft)
neighborhoodCount =
sum
( map
(length . draftNeighborhoodNeighbors)
(draftNeighborhoods draft)
)
roundedVertexCollisionObstructions
:: Map DraftVertexId ProjectedVertex
-> [OverlayEmbeddingObstruction]
roundedVertexCollisionObstructions projectedVertices =
[ RoundedVerticesCollide leftId rightId roundedPoint
| (roundedPoint, vertexIds) <- Map.toAscList verticesByRoundedPoint
, (leftId : remainingIds) <- tails (sort vertexIds)
, rightId <- remainingIds
]
where
verticesByRoundedPoint =
Map.fromListWith (<>)
[ (projectedRoundedPoint projectedVertex, [vertexId])
| (vertexId, projectedVertex) <- Map.toAscList projectedVertices
]
splitOrderObstructions
:: DraftSourceId
-> [ResolvedMembership]
-> [OverlayEmbeddingObstruction]
splitOrderObstructions sourceId memberships =
case memberships of
firstMembership : secondMembership : remainingMemberships ->
let finalMembership =
List.foldl' (\_ current -> current) secondMembership remainingMemberships
sourceFrom = roundedMembershipPoint firstMembership
sourceTo = roundedMembershipPoint finalMembership
in [ SplitOrderNotPreserved
sourceId
(resolvedVertexId (resolvedMembershipVertex leftMembership))
(resolvedVertexId (resolvedMembershipVertex rightMembership))
| (leftMembership, rightMembership) <-
zip
memberships
(drop 1 memberships)
, compare
(resolvedMembershipParameter leftMembership)
(resolvedMembershipParameter rightMembership)
/= roundedOrderAlong
sourceFrom
sourceTo
(roundedMembershipPoint leftMembership)
(roundedMembershipPoint rightMembership)
]
_ -> []
roundedMembershipPoint :: ResolvedMembership -> Point
roundedMembershipPoint =
projectedRoundedPoint
. resolvedProjectedVertex
. resolvedMembershipVertex
roundedOrderAlong :: Point -> Point -> Point -> Point -> Ordering
roundedOrderAlong
(Point sourceFromX sourceFromY)
(Point sourceToX sourceToY)
(Point leftX leftY)
(Point rightX rightY) =
let directionX = sourceToX - sourceFromX
directionY = sourceToY - sourceFromY
in if abs directionX >= abs directionY
then
if directionX >= 0
then compare leftX rightX
else compare rightX leftX
else
if directionY >= 0
then compare leftY rightY
else compare rightY leftY
incidenceRelationObstructions
:: SegmentRelation
-> ResolvedSegment
-> ResolvedSegment
-> [OverlayEmbeddingObstruction]
incidenceRelationObstructions declaredRelation firstSegment secondSegment =
[ IncidenceRelationChanged
(resolvedSegmentId firstSegment)
(resolvedSegmentId secondSegment)
declaredRelation
exactRelation
roundedRelation
| exactRelation /= declaredRelation || roundedRelation /= declaredRelation
]
where
exactRelation =
relationFor exactSegmentRelation projectedExactPoint firstSegment secondSegment
roundedRelation =
relationFor Math.segmentRelation projectedRoundedPoint firstSegment secondSegment
relationFor
:: (point -> point -> point -> point -> SegmentRelation)
-> (ProjectedVertex -> point)
-> ResolvedSegment
-> ResolvedSegment
-> SegmentRelation
relationFor relation project firstSegment secondSegment =
relation
(project (resolvedProjectedVertex (resolvedSegmentFrom firstSegment)))
(project (resolvedProjectedVertex (resolvedSegmentTo firstSegment)))
(project (resolvedProjectedVertex (resolvedSegmentFrom secondSegment)))
(project (resolvedProjectedVertex (resolvedSegmentTo secondSegment)))
neighborhoodOrientationObstructions
:: ResolvedVertex
-> NonEmpty ResolvedVertex
-> [OverlayEmbeddingObstruction]
neighborhoodOrientationObstructions center neighbors =
[ NeighborhoodOrientationChanged
(resolvedVertexId center)
(resolvedVertexId leftNeighbor)
(resolvedVertexId rightNeighbor)
exactOrientation
roundedOrientation
| (leftNeighbor, rightNeighbor) <-
cyclePairs neighbors
, let exactOrientation =
exactOrient2d
(exactVertexPoint center)
(exactVertexPoint leftNeighbor)
(exactVertexPoint rightNeighbor)
roundedOrientation =
Math.orient2d
(roundedVertexPoint center)
(roundedVertexPoint leftNeighbor)
(roundedVertexPoint rightNeighbor)
, exactOrientation /= roundedOrientation
]
exactVertexPoint :: ResolvedVertex -> ExactPoint
exactVertexPoint = projectedExactPoint . resolvedProjectedVertex
roundedVertexPoint :: ResolvedVertex -> Point
roundedVertexPoint = projectedRoundedPoint . resolvedProjectedVertex