packages feed

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