FlightTermination.hs

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wall #-}
-- The checks of inheritance (inheritFlightTermination') have a constraint that their body does not use, by design.
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- | The data type @FlightTermination'@: whether a type of RPA is fitted with a dedicated flight termination system, and its description.
module ReOC.Data.FlightTermination (
  FlightTermination' (..),
  FlightTermination'Like (..),
  lawNamesFlightTermination',
  FlightTermination,
  UnfilledFlightTermination,
  InheritFlightTermination',
  inheritFlightTermination',
) where

import Control.Lens (Choice, Optic, prism, prism', review)
import Data.Functor.Const (Const)
import Data.Text (Text)
import ReOC.Name.FlightTerminationSystem (FlightTerminationSystemLike (..))
import ReOC.Name.NoFlightTerminationSystem (NoFlightTerminationSystemLike (..))
import ReOC.Primitive.Text1 (Text1)

-- | Whether a type of RPA is fitted with a dedicated flight termination system, and its description. Its valid form is @FlightTermination@, and its unfilled form @UnfilledFlightTermination@.
data FlightTermination' a1
  = NoFlightTerminationSystem
  | FlightTerminationSystem a1
  deriving (Eq, Ord, Show)

-- | The name of the data type @FlightTermination'@.
class FlightTermination'Like p f x x' a1 a1' | x -> a1 where
  flightTermination' ::
    Optic p f x x' (FlightTermination' a1) (FlightTermination' a1')

-- | Identity
instance (x' ~ FlightTermination' a1') => FlightTermination'Like p f (FlightTermination' a1) x' a1 a1' where
  flightTermination' = id

-- | Prism
instance (Choice p, Applicative f, x' ~ FlightTermination' a1) => NoFlightTerminationSystemLike p f (FlightTermination' a1) x' where
  noFlightTerminationSystem = prism' (\() -> NoFlightTerminationSystem) (\case NoFlightTerminationSystem -> Just (); FlightTerminationSystem _ -> Nothing)

-- | Prism
instance (Choice p, Applicative f, x' ~ FlightTermination' a1') => FlightTerminationSystemLike p f (FlightTermination' a1) x' a1 a1' where
  flightTerminationSystem = prism FlightTerminationSystem (\case NoFlightTerminationSystem -> Left NoFlightTerminationSystem; FlightTerminationSystem x -> Right x)

{- | Rebuilds a value from the name of each field or constructor.

Laws:

> lawNamesFlightTermination' == id
-}
lawNamesFlightTermination' :: FlightTermination' a1 -> FlightTermination' a1
lawNamesFlightTermination' = \case
  NoFlightTerminationSystem -> review noFlightTerminationSystem ()
  FlightTerminationSystem x -> review flightTerminationSystem x

-- | A valid @FlightTermination'@.
type FlightTermination = FlightTermination' Text1

-- | An unfilled @FlightTermination'@: each field holds what has been entered, if anything, to be checked by @fillFlightTermination@.
type UnfilledFlightTermination = FlightTermination' (Maybe Text)

-- | The classes that a data type holding @FlightTermination'@ in one field, or in one or more constructors, inherits.
type InheritFlightTermination' s a1 =
  ( FlightTermination'Like (->) (Const ()) s s a1 a1
  , NoFlightTerminationSystemLike (->) (Const ()) s s
  , FlightTerminationSystemLike (->) (Const ()) s s a1 a1
  )

-- | Checks that a data type inherits every class of @InheritFlightTermination'@.
inheritFlightTermination' :: (InheritFlightTermination' s a1) => proxy s -> ()
inheritFlightTermination' _ = ()