{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Data.Type.Row (
    Row (..), (:++),
    Length, KnownLength,
    IndexOf, Member,
    Inclusive,
    Is, InstanceOf
) where

import Data.Type.Nat
import Data.Type.Bool (If)

infixr 5 :+, :-, :++

-- | A type level list with explicit removals.
data Row a
    = Nil        -- ^ The empty list.
    | a :+ Row a -- ^ Prepends an element (cons).
    | a :- Row a -- ^ Deletes the first instance an element.

-- | Appends two type level `Row`s.
type family l :++ m where
    'Nil :++ l = l
    (e ':+ l) :++ m = e ':+ l :++ m
    (e ':- l) :++ m = e ':- l :++ m

-- | Returns the length of the `Row` @l@.
type family Length l where
    Length 'Nil = 'Zero
    Length (h ':+ t) = 'Succ (Length t)
    Length (h ':- t) = 'Succ (Length t)

-- | The class of `Row`s with statically known lengths.
class KnownNat (Length l) => KnownLength l
instance KnownNat (Length l) => KnownLength l

-- | Returns the index of the first instance of @e@ in the `Row` @l@.
type IndexOf e l = NthIndexOf 'Zero e l

type family NthIndexOf n e l where
    NthIndexOf 'Zero     e (e ':+ l) = 'Zero
    NthIndexOf ('Succ n) e (e ':+ l) = 'Succ (NthIndexOf n e l)
    NthIndexOf n         e (f ':+ l) = 'Succ (NthIndexOf n e l)
    NthIndexOf n         e (e ':- l) = 'Succ (NthIndexOf ('Succ n) e l)
    NthIndexOf n         e (f ':- l) = 'Succ (NthIndexOf n e l)

-- | A constraint specifying that @e@ is a member of the `Row` @l@.
class KnownNat (IndexOf e l) => Member e l
instance KnownNat (IndexOf e l) => Member e l

-- | The class of `Row`s that do not contain deletions (`':-`).
class KnownLength l => Inclusive l
instance Inclusive 'Nil
instance Inclusive l => Inclusive (e ':+ l)

-- | Returns a boolean value indicating whether @f@ belongs to the group of
-- effects identified by @name@. This allows `MemberEffect` to infer the
-- associated types for arbitrary effects.
type family Is (name :: k) (f :: * -> *) :: Bool

type InstanceOf name l = InstanceOfNone name '[] l

-- Any instance of name in l but not in ex.
type family InstanceOfNone name ex l where
    InstanceOfNone name ex (f ':- l) = InstanceOfNone name (f ': ex) l
    InstanceOfNone name ex (f ':+ l) =
        If (Is name f)
            (If (Elem f ex) (InstanceOfNone name (Remove f ex) l) f)
            (InstanceOfNone name ex l)

type family Elem e l where
    Elem e '[] = 'False
    Elem e (e ': l) = 'True
    Elem e (f ': l) = Elem e l

type family Remove e l where
    Remove e (e ': l) = l
    Remove e (f ': l) = f ': Remove e l