-- | Finite, explicitly declared maps from abstract labels to realized labels.
module Foundational.Realization
  ( Realization
  , mkRealization
  , realize
  , realizationMappings
  , genRealization
  , RealizationStage (..)
  , StageRecord
  , verifiedStage
  , unverifiedStage
  , reconstructionPlanValid
  , ConnectionPolicy (..)
  , allConnectionPolicies
  , BoundaryClass (..)
  , BoundaryTerm (..)
  , requiredBoundaryTerms
  , boundaryTermsComplete
  , ConservationLedger (..)
  , supportsMatterConservation
  , AlternativeDynamicsWitness (..)
  , validAlternative
  , antisymmetricPairCancellation
  ) where

import Data.List (nub, sort)
import Test.QuickCheck (Gen, chooseInt)

-- | A source-label-unique realization map.
newtype Realization = Realization [(String, String)]
  deriving (Eq, Show)

-- | Construct a realization only when each source label has one image.
mkRealization :: [(String, String)] -> Maybe Realization
mkRealization mappings
  | unique (map fst mappings) = Just (Realization mappings)
  | otherwise = Nothing

-- | Look up the realized label for one declared abstract label.
realize :: Realization -> String -> Maybe String
realize (Realization mappings) source = lookup source mappings

-- | Expose the finite mapping list for inspection and generator properties.
realizationMappings :: Realization -> [(String, String)]
realizationMappings (Realization mappings) = mappings

-- | Generate a source-label-unique finite realization map.
genRealization :: Gen Realization
genRealization = do
  size <- chooseInt (0, 4)
  let names = take size ["a", "b", "c", "d"]
  pure (Realization [(name, "realized-" <> name) | name <- names])

unique :: Eq value => [value] -> Bool
unique values = length values == length (nub values)

-- | Symbolic stages in the conditional realization ladder.
data RealizationStage
  = Events
  | Chronology
  | SmoothStructure
  | ConformalStructure
  | ProjectiveStructure
  | WeylCompatibility
  | MetricScale
  | LocalCoframe
  | Connection
  | Curvature
  | Action
  | FieldEquation
  deriving (Bounded, Enum, Eq, Ord, Show)

-- | One finite dependency declaration. Verification is supplied, not inferred.
data StageRecord = StageRecord
  { stage :: RealizationStage
  , dependencies :: [RealizationStage]
  , verified :: Bool
  }
  deriving (Eq, Show)

verifiedStage :: RealizationStage -> [RealizationStage] -> StageRecord
verifiedStage stageName stageDependencies =
  StageRecord stageName stageDependencies True

unverifiedStage :: RealizationStage -> [RealizationStage] -> StageRecord
unverifiedStage stageName stageDependencies =
  StageRecord stageName stageDependencies False

-- | Check only finite ordering and certificate bookkeeping.
reconstructionPlanValid :: [StageRecord] -> Bool
reconstructionPlanValid records =
  unique (map stage records) && go [] records
  where
    go _ [] = True
    go completed (record : remaining) =
      verified record
        && stage record `notElem` dependencies record
        && unique (dependencies record)
        && all (`elem` completed) (dependencies record)
        && go (stage record : completed) remaining

data ConnectionPolicy
  = LeviCivita
  | Weyl
  | RiemannCartan
  | MetricAffine
  deriving (Bounded, Enum, Eq, Ord, Show)

allConnectionPolicies :: [ConnectionPolicy]
allConnectionPolicies = [minBound .. maxBound]

data BoundaryClass
  = Closed
  | SmoothNonNullDirichlet
  | NullSegments
  | PiecewiseSmoothWithJoints
  deriving (Bounded, Enum, Eq, Ord, Show)

data BoundaryTerm
  = GHY
  | NullSegment
  | NullJoint
  | Joint
  deriving (Bounded, Enum, Eq, Ord, Show)

requiredBoundaryTerms :: BoundaryClass -> [BoundaryTerm]
requiredBoundaryTerms boundaryClass = case boundaryClass of
  Closed -> []
  SmoothNonNullDirichlet -> [GHY]
  NullSegments -> [NullSegment, NullJoint]
  PiecewiseSmoothWithJoints -> [GHY, Joint]

boundaryTermsComplete :: BoundaryClass -> [BoundaryTerm] -> Bool
boundaryTermsComplete boundaryClass supplied =
  unique supplied
    && sort supplied == sort (requiredBoundaryTerms boundaryClass)

data ConservationLedger = ConservationLedger
  { bianchiIdentity :: Bool
  , matterDiffeomorphismInvariant :: Bool
  , matterOnShell :: Bool
  , conservationConnectionPolicy :: ConnectionPolicy
  }
  deriving (Eq, Show)

supportsMatterConservation :: ConservationLedger -> Bool
supportsMatterConservation ledger =
  bianchiIdentity ledger
    && matterDiffeomorphismInvariant ledger
    && matterOnShell ledger
    && conservationConnectionPolicy ledger == LeviCivita

data AlternativeDynamicsWitness = AlternativeDynamicsWitness
  { actionTag :: String
  , local :: Bool
  , diffeomorphismCovariant :: Bool
  , differsFromEinstein :: Bool
  , relaxedHypothesis :: String
  }
  deriving (Eq, Show)

validAlternative :: AlternativeDynamicsWitness -> Bool
validAlternative witness =
  not (null (actionTag witness))
    && local witness
    && diffeomorphismCovariant witness
    && differsFromEinstein witness
    && not (null (relaxedHypothesis witness))

antisymmetricPairCancellation :: Integer -> Integer -> Maybe Integer
antisymmetricPairCancellation value transpose
  | transpose == negate value = Just (value + transpose)
  | otherwise = Nothing