-- FIXME: Introduce hyperlinks to type operators once this is supported by Haddock.
{-|
    This module provides records of signals and signal-related data.

    A record has a type of the following form:

    @
    (X :& /name_1/ ::: /signal_1/ `'Of'` /val_1/ :& ... :& /name_n/ ::: /signal_n/ `'Of'` /val_n/) /style/
    @

    A value of such a type is a list of /fields/ where the /i/th field has type @(/name_i/ :::
    /signal_i/ `'Of'` /val_i/) /style/@.

    @(:::)@ is a data family. Its @/style/@ parameter is a phantom type which selects the instance
    of the family. For a concrete @/style/@ type, the type @(/name/ ::: /signal/ `'Of'`
    /val/) /style/@ covers name-value pairs where the type of the values depends on @/signal/@ and
    @/val/@. For example, if @/style/@ is of the form @'SignalStyle' /era/@, the values have type
    @/signal/ /era/ /val/@. This leads to records of signals with identical era. With the styles
    @'Connector' 'Consumer'@ and @'Connector' 'Producer'@, it is possible to form records of
    consumers and producers.

    Field names are represented by types which are declared as follows:

    @
    data /Name/ = /Name/
    @

    This makes it possible to use names as types (allowing the use of names in compile-time checks)
    but also as expressions and patterns.
-}
module FRP.Grapefruit.Record (

    -- * Records
    Record (build),
    X (X),
    (:&) ((:&)),
    (:::) ((::=), (::~)), -- data constructors exported here to avoid (:::) double export warning

    -- * Catenation
    Cat,
    cat,

    -- * Subrecords
    Subrecord (narrow),

    -- * Signal records
    SignalRecord,
    SignalStyle,
    -- (:::) ((::=)),

    -- * Connector records
    ConsumerRecord,
    ProducerRecord,
    ConnectorRecord,
    ConnectorStyle,
    -- (:::) ((::~)),
    consume,
    produce

) where

    -- Control
    import Control.Arrow as Arrow

    -- Data
    import Data.TypeLevel.Bool
    import Data.TypeEq

    -- FRP.Grapefruit
    import           FRP.Grapefruit.Circuit as Circuit
    import           FRP.Grapefruit.Signal  as Signal (Of, Consumer, Producer)
    import qualified FRP.Grapefruit.Signal  as Signal

    -- Fixities
    infixl 2 :&
    infix  3 :::, ::=, ::~

    -- * Records
    {-|
        The class of all record types.

        A record type is a type of records without the style parameter. Therefore, it has kind @* ->
        *@.
    -}
    class Record record where

        {-|
            A general method for building record-related “things”.

            For each record type, this method constructs a value which is somehow related to this
            record type. Such a value is called a thing. The type parameter @thing@ maps record
            types to the types of their corresponding things. The first argument of @build@ gives
            the thing of the empty record type while the second argument tells how to transform a
            thing of an arbitrary record type into the thing of this record type extended
            with an arbitrary field type.

            @build@ is used, for example, to implement the function 'cat'.
        -}
        build :: thing X
              -> (forall record name signal val. (Record record) =>
                  thing record -> thing (record :& name ::: signal `Of` val))
              -> thing record

    instance Record X where

        build nilThing _ = nilThing

    instance (Record record) => Record (record :& name ::: signal `Of` val) where

        build nilThing consThing = consThing (build nilThing consThing)

    -- |The type of empty records.
    data X style = X

    -- |The type of non-empty records, consisting of an initial record and a last field.
    data (record :& field) style = !(record style) :& !(field style)

    {-|
        The family of record fields.

        Each instance of it matches arbitrary @name@ parameters and all @signalOfVal@ parameters
        which are of the form @/signal/ `'Of'` /val/@. The actual choice of the instance
        depends only on the @style@ parameter. The structure of fields of a specific style is
        documented together with the respective style type.
    -}
    data family (name ::: signalOfVal) style :: *

    undefinedName :: (name ::: val) style -> name
    undefinedName = undefined

    -- * Catenation
    -- |The catenation of two record types.
    type family Cat (record1 :: * -> *) (record2 :: * -> *) :: * -> *
    type instance Cat record1 X                   = record1
    type instance Cat record1 (record2 :& field2) = Cat record1 record2 :& field2

    -- |The catenation of two records.
    cat :: (Record record1, Record record2) =>
           record1 style -> record2 style -> Cat record1 record2 style
    cat record1 = case build (nilCatThing record1) consCatThing of CatThing attach -> attach

    newtype CatThing style record1 record2 = CatThing (record2 style -> Cat record1 record2 style)

    nilCatThing :: record1 style -> CatThing style record1 X
    nilCatThing record1 = CatThing $ \X -> record1

    consCatThing :: CatThing style record1 record2
                 -> CatThing style record1 (record2 :& name ::: val)
    consCatThing (CatThing attach) = CatThing $ \(record2 :& field2) -> attach record2 :& field2

    -- * Subrecords
    {-|
        The class of all pairs of record types where the first is a subrecord of the second.

        Currenty, the subrecord relation is only defined for records which do not have multiple
        occurences of the same name. A records is a subrecord of another record if all field types
        of the first record are also field types of the second, independently of order.

        The instance declarations of @Subrecord@ use several helper classes which are hidden. One of
        them is the class @Presence@. You get the error message that no instance of @Presence
        /name/@ could be found if the alleged subrecord contains a name which is not present in the
        alleged superrecord.
    -}
    class (Record subrecord, Record record) => Subrecord subrecord record where

        -- |Converts a record into a subrecord by dropping and reordering fields appropriately.
        narrow :: record style -> subrecord style

    instance (Record record) => Subrecord X record where

        narrow _ = X

    instance (Dissection record remainder subname subsignal subval,
              Subrecord subrecord remainder) =>
             Subrecord (subrecord :& subname ::: subsignal `Of` subval) record where

        narrow record = narrow remainder :& lookupField where

            (remainder,lookupField) = dissect record

    class (Record record, Record remainder) =>
          Dissection record remainder lookupName lookupSignal lookupVal
              | record lookupName -> remainder where

        dissect :: record style
                -> (remainder style,(lookupName ::: lookupSignal `Of` lookupVal) style)

    instance (Present lookupName, Record remainder) =>
             Dissection X remainder lookupName lookupSignal lookupVal where

        dissect = undefined

    instance (TypeEq name lookupName namesAreEq,
              NameMatchDep namesAreEq
                           record name signal val
                           remainder lookupName lookupSignal lookupVal) =>
             Dissection (record :& name ::: signal `Of` val)
                        remainder lookupName lookupSignal lookupVal where

        dissect (record :& field) = (remainder,lookupField) where

            (remainder,lookupField) = nameMatchDepExtract (typeEq name lookupName) record field

            name                    = undefinedName field

            lookupName              = undefinedName lookupField

    class (Record record, Record remainder) =>
          NameMatchDep namesAreEq record name signal val remainder lookupName lookupSignal lookupVal
              | namesAreEq record name signal val lookupName -> remainder where

        nameMatchDepExtract :: namesAreEq
                            -> record style
                            -> (name ::: signal `Of` val) style
                            -> (remainder style,(lookupName ::: lookupSignal `Of` lookupVal) style)

    instance (Dissection record remainder lookupName lookupSignal lookupVal) =>
             NameMatchDep False
                          record name signal val
                          remainder lookupName lookupSignal lookupVal where

        nameMatchDepExtract _ record _ = dissect record

    instance (Record record, lookupSignal ~ signal, lookupVal ~ val) =>
             NameMatchDep True
                          record lookupName signal val
                          record lookupName lookupSignal lookupVal where

        nameMatchDepExtract _ record field = (record,field)

    class Present lookupName

    -- * Signal records
    -- |Records which contain signals of a common era as values.
    type SignalRecord era record = record (SignalStyle era)

    {-|
        The style of signal records of a specific era.

        Fields of signal style records have the form @/name/ ::= /signal/@.
    -}
    data SignalStyle era

    data instance (name ::: signal `Of` val) (SignalStyle era) = !name ::= signal era val

    -- * Connector records
    -- ** Records
    -- |Records which contain signal consumers as values.
    type ConsumerRecord record = ConnectorRecord Consumer record

    -- |Records which contain signal producers as values.
    type ProducerRecord record = ConnectorRecord Producer record

    -- |Records which which contain signal connectors (producers or consumers) as values.
    type ConnectorRecord connector record = record (ConnectorStyle connector)

    {-|
        The consumer and producer record styles.

        @ConnectorStyle 'Consumer'@ is the style of consumer records and @ConnectorStyle 'Producer'@
        is the style of producer records. Fields of connector style records have the form @/name/
        ::~ /connector/@.
    -}
    data ConnectorStyle (connector :: (* -> * -> *) -> * -> *)

    data instance (:::) name
                        (signal `Of` val)
                        (ConnectorStyle connector) = !name ::~ connector signal val

    -- ** Consumption
    {-|
        Converts a record of consumers into a circuit that consumes a corresponding record of
        signals.
    -}
    consume :: (Record record) => ConsumerRecord record -> Circuit era (SignalRecord era record) ()
    consume = case build nilConsumeThing consConsumeThing of ConsumeThing result -> result

    newtype ConsumeThing era record = ConsumeThing (ConsumerRecord record ->
                                                    Circuit era (SignalRecord era record) ())

    nilConsumeThing :: ConsumeThing era X
    nilConsumeThing = ConsumeThing $ \X -> arr (\X -> ())

    consConsumeThing :: ConsumeThing era record
                     -> ConsumeThing era (record :& name ::: signal `Of` val)
    consConsumeThing (ConsumeThing consume) = ConsumeThing consume' where

        consume' (consumerRecord :& _ ::~ consumer) = proc (signalRecord :& _ ::= signal) -> do
            consume consumerRecord  -< signalRecord
            Signal.consume consumer -< signal

    -- ** Production
    {-|
        Converts a record of producers into a circuit that produces a corresponding record of
        signals.
    -}
    produce :: (Record record) => ProducerRecord record -> Circuit era () (SignalRecord era record)
    produce = case build nilProduceThing consProduceThing of ProduceThing result -> result

    newtype ProduceThing era record = ProduceThing (ProducerRecord record ->
                                                    Circuit era () (SignalRecord era record))

    nilProduceThing :: ProduceThing era X
    nilProduceThing = ProduceThing $ \X -> arr (const X)

    consProduceThing :: ProduceThing era record
                     -> ProduceThing era (record :& name ::: signal `Of` val)
    consProduceThing (ProduceThing produce) = ProduceThing produce' where

        produce' (producerRecord :& name ::~ producer) = proc () -> do
            signalRecord <- produce producerRecord  -< ()
            signal       <- Signal.produce producer -< ()
            returnA -< signalRecord :& name ::= signal