{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE PolyKinds            #-}

--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Comp.SubsumeCommon
-- Copyright   :  (c) 2014 Patrick Bahr
-- License     :  BSD3
-- Maintainer  :  Patrick Bahr <paba@diku.dk>
-- Stability   :  experimental
-- Portability :  non-portable (GHC Extensions)
--
-- Shared parts of the implementation of signature subsumption for
-- both the base and the multi library.
--
--------------------------------------------------------------------------------

module Data.Comp.SubsumeCommon
    ( ComprEmb
    , Pos (..)
    , Emb (..)
    , Choose
    , Sum'
    , Proxy (..)
    ) where

-- | This type is used in its promoted form only. It represents
-- pointers from the left-hand side of a subsumption to the right-hand
-- side.
data Pos = Here | Le Pos | Ri Pos | Sum Pos Pos

-- | This type is used in its promoted form only. It represents
-- possible results for checking for subsumptions. 'Found' indicates a
-- subsumption was found; 'NotFound' indicates no such subsumption was
-- found. 'Ambiguous' indicates that there are duplicates on the left-
-- or the right-hand side.
data Emb = Found Pos | NotFound | Ambiguous

data Proxy a = P


type family Choose (e1 :: Emb) (r :: Emb) :: Emb where
    Choose (Found x) (Found y) = Ambiguous
    Choose Ambiguous y = Ambiguous
    Choose x Ambiguous = Ambiguous
    Choose (Found x) y = Found (Le x)
    Choose x (Found y) = Found (Ri y)
    Choose x y = NotFound


type family Sum' (e1 :: Emb) (r :: Emb) :: Emb where
    Sum' (Found x) (Found y) = Found (Sum x y)
    Sum' Ambiguous y = Ambiguous
    Sum' x Ambiguous = Ambiguous
    Sum' NotFound y = NotFound
    Sum' x NotFound = NotFound


-- | This type family takes a position type and compresses it. That
-- means it replaces each nested occurrence of
--
-- @
--   Sum (prefix (Le Here)) (prefix (Ri Here))@
-- @
---
-- with
--
-- @
--   prefix Here@
-- @
--
-- where @prefix@ is some composition of @Le@ and @Ri@. The rational
-- behind this type family is that it provides a more compact proof
-- term of a subsumption, and thus yields more efficient
-- implementations of 'inj' and 'prj'.

type family ComprPos (p :: Pos) :: Pos where
    ComprPos Here = Here
    ComprPos (Le p) = Le (ComprPos p)
    ComprPos (Ri p) = Ri (ComprPos p)
    ComprPos (Sum l r) = CombineRec (ComprPos l) (ComprPos r)


-- | Helper type family for 'ComprPos'. Note that we could have
-- defined this as a type synonym. But if we do that, performance
-- becomes abysmal. I presume that the reason for this huge impact on
-- performance lies in the fact that right-hand side of the defining
-- equation duplicates the two arguments @l@ and @r@.
type family CombineRec l r where
    CombineRec l r = CombineMaybe (Sum l r) (Combine l r)

-- | Helper type family for 'ComprPos'.
type family CombineMaybe (p :: Pos) (p' :: Maybe Pos) where
    CombineMaybe p (Just p') = p'
    CombineMaybe p p'        = p


-- | Helper type family for 'ComprPos'.
type family Combine (l :: Pos) (r :: Pos) :: Maybe Pos where
    Combine (Le l) (Le r) = Le' (Combine l r)
    Combine (Ri l) (Ri r) = Ri' (Combine l r)
    Combine (Le Here) (Ri Here) = Just Here
    Combine l r = Nothing

-- | 'Ri' lifted to 'Maybe'.
type family Ri' (p :: Maybe Pos) :: Maybe Pos where
    Ri' Nothing = Nothing
    Ri' (Just p) = Just (Ri p)

-- | 'Le' lifted to 'Maybe'.
type family Le' (p :: Maybe Pos) :: Maybe Pos where
    Le' Nothing = Nothing
    Le' (Just p) = Just (Le p)


-- | If the argument is not 'Found', this type family is the
-- identity. Otherwise, the argument is of the form @Found p@, and
-- this type family does two things: (1) it checks whether @p@ the
-- contains duplicates; and (2) it compresses @p@ using 'ComprPos'. If
-- (1) finds no duplicates, @Found (ComprPos p)@ is returned;
-- otherwise @Ambiguous@ is returned.
--
-- For (1) it is assumed that @p@ does not contain 'Sum' nested
-- underneath a 'Le' or 'Ri' (i.e. only at the root or underneath a
-- 'Sum'). We will refer to such positions below as /atomic position/.
-- Positions not containing 'Sum' are called /simple positions/.
type family ComprEmb (e :: Emb) :: Emb where
    ComprEmb (Found p) = Check (Dupl p) (ComprPos p)
    ComprEmb e = e

-- | Helper type family for 'ComprEmb'.
type family Check (b :: Bool) (p :: Pos) where
    Check False p = Found p
    Check True  p = Ambiguous

-- | This type family turns a list of /atomic position/ into a list of
-- /simple positions/ by recursively splitting each position of the
-- form @Sum p1 p2@ into @p1@ and @p2@.
type family ToList (s :: [Pos]) :: [Pos] where
    ToList (Sum p1 p2 ': s) = ToList (p1 ': p2 ': s)
    ToList (p ': s) = p ': ToList s
    ToList '[] = '[]

-- | This type checks whether the argument (atomic) position has
-- duplicates.
type Dupl s = Dupl' (ToList '[s])

-- | This type family checks whether the list of positions given as an
-- argument contains any duplicates.
type family Dupl' (s :: [Pos]) :: Bool where
    Dupl' (p ': r) = OrDupl' (Find p r) r
    Dupl' '[] = False

-- | This type family checks whether its first argument is contained
-- its second argument.
type family Find (p :: Pos) (s :: [Pos]) :: Bool where
    Find p (p ': r)  = True
    Find p (p' ': r) = Find p r
    Find p '[] = False

-- | This type family returns @True@ if the first argument is true;
-- otherwise it checks the second argument for duplicates.
type family OrDupl' (a :: Bool) (b :: [Pos]) :: Bool where
    OrDupl'  True  c  = True
    OrDupl'  False c  = Dupl' c