-- |Record core support.
module Data.Record (

    -- * Record basics
    -- $RecordBasics
    X        (X),
    (:&)     ((:&)),
    (:::)    ((:=)),
    Name     (name),
    Record   (fold),
    Expander (Expander),

    -- * Record conversion
    -- $RecordConversion
    Convertible (convert),

    -- * Field separation
    Separation (separate)

) where

    import Data.Kind    as Kind
    import Data.TypeFun as TypeFun

    -- * Record basics
    infixl 2 :&
    infix  3 :::, :=

    {-$RecordBasics
        A record is a list of name-value pairs. Such pairs are called fields and are constructed
        using the data constructor @(:=)@. Records are built from fields using the data
        constructors @X@ (for the empty record) and @(:&)@ (for non-empty records that
        consist of an initial record and a last field each). For example, the following expression
        denotes a record that contains some information about the author of these lines:

        @
    X :& Surname := \"Jeltsch\" :& Age := 33 :& Room := \"HG/2.39\"
        @

        The type of a record has the form @/r/ /s/@ where @/r/@ is a record scheme and
        @/s/@ is a representation of a type-level function, called the record style. A record
        scheme is a list of name-sort pairs, which correspond to the name-value pairs of the record.
        The type constructors @X@ and @(:&)@ are used to form record schemes. Name-sort
        pairs are constructed using the type constructor @(:::)@.

        The name of a name-sort pair equals the name of the corresponding record field. Applying the
        style to the sort yields the type of the corresponding field value. For example, the above
        record has the following type:

        @
    (X :& Surname ::: String :& Age ::: Int :& Room ::: String) ('Id' 'KindStar')
        @

        If we replace the type @Id KindStar@ by @Id KindStar :-> Id KindStar@, we get a type that
        covers all records with a @Surname@, an @Age@, and a @Room@ field that contain values of
        type @String -> String@, @Int -> Int@, and @String -> String@, respectively. So by varying
        the style, we can generate a family of related record types from a single record scheme.
    -}

    -- |The empty record scheme.
    data X style = X
                   -- ^The empty record.
         deriving (Show)

    {-|
        Non-empty record schemes.
    -}
    data (rec :& field)  style = !(rec style) :& !(field style)
                                 -- ^Non-empty records.

    {-
        We use an explicit instance declaration to avoid parantheses around the first arguments of
        (:&). Our instance declaration will lead to missing parantheses if a first argument of (:&)
        is an application of an operator that has the same fixity as :& and is right- or
        non-associative.
    -}
    instance (Show (rec style), Show name, Show (App style sort)) =>
             Show ((rec :& name ::: sort) style) where

        showsPrec enclPrec (rec :& field) = showParen (enclPrec > snocPrec) $
                                            showsPrec snocPrec rec          .
                                            showString " :& "               .
                                            showsPrec (succ snocPrec) field where

            snocPrec = 2

    -- |The type of record fields.
    data (name ::: sort) style = !name := App style sort
                                 -- ^Constructs a record field from a name and a value.

    {-
        We use an explicit instance declaration because the use of the type synonym family App
        makes deriving (currently) impossible.
    -}
    instance (Show name, Show (App style sort)) => Show ((name ::: sort) style) where

        showsPrec enclPrec (name := val) = showParen (enclPrec > assignPrec) $
                                           showsPrec (succ assignPrec) name .
                                           showString " := "                .
                                           showsPrec (succ assignPrec) val where

            assignPrec = 3

    {-|
        The class of name types. For each field name @/N/@, there should be a declaration of
        the following form:

        @
    data /N/ = /N/ deriving (Show)
        @

        That way, the name can be represented in types by the type constructor @/N/@, and in
        expressions and patterns by the data constructor @/N/@. Furthermore, the following
        instance declaration should be added:

        @
    instance Name /N/ where
     
        name = /N/
        @

        Such instance declarations allow record combinators to construct value-level representations
        of names from type-level representations.
    -}
    class Name name where

        -- |The sole inhabitant of the name type.
        name :: name

    {-|
        An instance @Record /k/ /r/@ exists if and only if @/r/@ is a record scheme whose sorts
        are of the subkind represented by @/k/@.
    -}
    class (Kind kind) => Record kind rec where

        {-|
            Folding of record schemes. This function can be used to define combinators whose types
            have the form @(Record rec) => /t/ rec@ by induction on the @rec@ parameter.
        -}
        fold :: thing X
                -- ^ the definition of the combinator for the empty record scheme
             -> (forall rec name. (Record kind rec, Name name) =>
                                  All kind (Expander thing rec name))
                {-^
                    turns the definition of the combinator for a record scheme @/r/@ into the
                    definition for any record scheme @/r/ :& /n/ ::: /s/@
                -}
             -> thing rec
                -- ^ the resulting combinator that works for all record schemes

    {-|
        Transformations from the definition of a record combinator for some record scheme into its
        definition for an expanded record scheme.
    -}
    newtype Expander thing rec name sort = Expander (thing rec -> thing (rec :& name ::: sort))

    instance (Kind kind) => Record kind X where

        fold nilAlt _ = nilAlt

    instance (Record kind rec, Name name, Inhabitant kind sort) =>
             Record kind (rec :& name ::: sort) where

        fold nilAlt expander = let

                                   Expander snocAlt = specialize expander

                               in snocAlt (fold nilAlt expander)

    -- * Record conversion
    {-$RecordConversion
        Records are lists, so their fields are totally ordered. This order can be used to
        distinguish fields that have the same name. For each name, we index the fields of this name
        from right to left. We identify a field by its name and its index. However, the order of
        fields with different names is superfluous. Therefore, it is worthwhile that it can be
        modified. Furthermore, it is often beneficial if unnecessary fields can be ignored. That
        way, record operations can be made more general since they can also work with records that
        contain more than the expected fields.

        Record conversion reorders and drops fields in such a way that all remaining fields keep
        their identification. So record conversion keeps the order of fields that share a common
        name, and it drops a field only if all preceding fields of the same name are also dropped.
        The scheme of the destination record is generated from the scheme of the source record by
        applying the same reorderings and droppings that are used to transform the source record
        into the destination record. The style is not changed.
    -}

    -- NOTE: Convertible does not ensure that all names in the source record are instances of Name.
    {-|
        An instance @Convertible /r/ /r'/@ exists if and only if @/r/@ and @/r'/@ are
        record schemes, and records of a type @/r/ /s/@ can be converted into records of the type
        @/r'/ /s/@.
    -}
    class Convertible rec rec' where

        -- |Converts a record into another record.
        convert :: rec style -> rec' style

    instance Convertible rec X where

        convert _ = X

    instance (Separation rec remain name' sort', Convertible remain rec') =>
             Convertible rec (rec' :& name' ::: sort') where

        convert rec = convert remain :& field' where

            (remain,field') = separate rec

    -- * Field separation
    -- NOTE: Separate does not ensure that all names in the source record are instances of Name.
    {-|
        An instance @Separation /r/ /r'/ /n/ /s/@ exists if and only if the following conditions are
        met:

        * @/r/@ is a record scheme that contains the name @/n/@.

        * The last name-sort pair with the name @/n/@ contains the sort @/s/@.

        * Removing that name-sort pair from @/r/@ yields @/r'/@.
    -}
    class (Name sepName) =>
          Separation rec remain sepName sepSort | rec sepName -> remain sepSort where

        {-|
            Extracts the last field of the respective name and returns the remaining record and the
            extracted field.
        -}
        separate :: rec style -> (remain style,(sepName ::: sepSort) style)

    instance (Name name, sort ~ sepSort) =>
             Separation (rec :& name ::: sort) rec name sepSort where

        separate (rec :& field) = (rec,field)

    instance (Separation rec remain sepName sepSort, (remain :& name ::: sort) ~ extRemain) =>
             Separation (rec :& name ::: sort) extRemain sepName sepSort where

        separate (rec :& field) = (remain :& field,sepField) where

            (remain,sepField) = separate rec