RePLOrigin.hs

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

-- | The data type @RePLOrigin'@: how the chief remote pilot obtained their initial RePL (CASA Form 101-02, question 9).
module ReOC.Data.RePLOrigin (
  RePLOrigin' (..),
  RePLOrigin'Like (..),
  lawNamesRePLOrigin',
  RePLOrigin,
  UnfilledRePLOrigin,
  InheritRePLOrigin',
  inheritRePLOrigin',
) where

import Control.Lens (Choice, Optic, prism, prism', review)
import Data.Functor.Const (Const)
import Data.Text (Text)
import ReOC.Name.PplTheory (PplTheoryLike (..))
import ReOC.Name.RePLTrainingOrganisation (RePLTrainingOrganisationLike (..))
import ReOC.Primitive.FormText (WideLine)

-- | How the chief remote pilot obtained their initial RePL (CASA Form 101-02, question 9). Its valid form is @RePLOrigin@, and its unfilled form @UnfilledRePLOrigin@.
data RePLOrigin' a1
  = PPLTheory
  | RePLTraining a1
  deriving (Eq, Ord, Show)

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

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

-- | Prism
instance (Choice p, Applicative f, x' ~ RePLOrigin' a1) => PplTheoryLike p f (RePLOrigin' a1) x' where
  pplTheory = prism' (\() -> PPLTheory) (\case PPLTheory -> Just (); RePLTraining _ -> Nothing)

-- | Prism
instance (Choice p, Applicative f, x' ~ RePLOrigin' a1') => RePLTrainingOrganisationLike p f (RePLOrigin' a1) x' a1 a1' where
  rePLTrainingOrganisation = prism RePLTraining (\case PPLTheory -> Left PPLTheory; RePLTraining x -> Right x)

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

Laws:

> lawNamesRePLOrigin' == id
-}
lawNamesRePLOrigin' :: RePLOrigin' a1 -> RePLOrigin' a1
lawNamesRePLOrigin' = \case
  PPLTheory -> review pplTheory ()
  RePLTraining x -> review rePLTrainingOrganisation x

-- | A valid @RePLOrigin'@.
type RePLOrigin = RePLOrigin' WideLine

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

-- | The classes that a data type holding @RePLOrigin'@ in one field, or in one or more constructors, inherits.
type InheritRePLOrigin' s a1 =
  ( RePLOrigin'Like (->) (Const ()) s s a1 a1
  , PplTheoryLike (->) (Const ()) s s
  , RePLTrainingOrganisationLike (->) (Const ()) s s a1 a1
  )

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