content: {-# LANGUAGE CPP #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE NoImplicitPrelude #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE UndecidableInstances #-}
  
  -- GHC >=7.10 deprecated OverlappingInstances in favour of instance by instance
  -- annotation using OVERLAPPABLE and OVERLAPPING pragmas.
  #ifdef DEPRECATED_LANGUAGE_OVERLAPPING_INSTANCES
  #define PRAGMA_OVERLAPPABLE {-# OVERLAPPABLE #-}
  #else
  {-# LANGUAGE OverlappingInstances #-}
  #define PRAGMA_OVERLAPPABLE
  #endif
  
  -- |
  -- Module:       Data.OpenUnion.Internal
  -- Description:  Open unions (type-indexed co-products) for extensible effects.
  --
  -- Copyright:    (c) 2016 Allele Dev; 2017 Ixperta Solutions s.r.o.
  -- License:      BSD3
  -- Maintainer:   ixcom-core@ixperta.com
  -- Stability:    experimental
  -- Portability:  GHC specific language extensions.
  --
  -- These are internal definitions and should be used with caution. There are no
  -- guarantees that the API of this module will be preserved between minor
  -- versions of this package.
  --
  -- Open unions (type-indexed co-products, i.e. type-indexed sums) for
  -- extensible effects All operations are constant-time.
  --
  -- Based on
  -- <http://okmij.org/ftp/Haskell/extensible/OpenUnion51.hs OpenUnion51.hs>.
  --
  -- Type-list @r :: [* -> *]@ of open union components is a small Universe.
  -- Therefore, we can use a @Typeable@-like evidence in that universe. In our
  -- case a simple index of an element in the type-list is sufficient
  -- substitution for @Typeable@.
  module Data.OpenUnion.Internal (module Data.OpenUnion.Internal)
    where
  
  import Prelude ((+), (-))
  
  import Data.Bool (otherwise)
  import Data.Either (Either(Left, Right))
  import Data.Eq ((==))
  import Data.Function (($))
  import Data.Maybe (Maybe(Just, Nothing))
  import Data.Word (Word)
  import Unsafe.Coerce (unsafeCoerce)
  
  
  -- | Open union is a strong sum (existential with an evidence).
  data Union (r :: [ * -> * ]) a where
      Union :: {-# UNPACK #-} !Word -> t a -> Union r a
  
  -- | Takes a request of type @t :: * -> *@, and injects it into the 'Union'.
  --
  -- Summand is assigning a specified 'Word' value, which is a position in the
  -- type-list @(t ': r) :: * -> *@.
  --
  -- __This function is unsafe.__
  --
  -- /O(1)/
  unsafeInj :: Word -> t a -> Union r a
  unsafeInj = Union
  {-# INLINE unsafeInj #-}
  
  -- | Project a value of type @'Union' (t ': r) :: * -> *@ into a possible
  -- summand of the type @t :: * -> *@. 'Nothing' means that @t :: * -> *@ is not
  -- the value stored in the @'Union' (t ': r) :: * -> *@.
  --
  -- It is assumed that summand is stored in the 'Union' when the 'Word' value is
  -- the same value as is stored in the 'Union'.
  --
  -- __This function is unsafe.__
  --
  -- /O(1)/
  unsafePrj :: Word -> Union r a -> Maybe (t a)
  unsafePrj n (Union n' x)
    | n == n'   = Just (unsafeCoerce x)
    | otherwise = Nothing
  {-# INLINE unsafePrj #-}
  
  -- | Represents position of element @t :: * -> *@ in a type list
  -- @r :: [* -> *]@.
  newtype P t r = P {unP :: Word}
  
  -- | Find an index of an element @t :: * -> *@ in a type list @r :: [* -> *]@.
  -- The element must exist.
  --
  -- This is essentially a compile-time computation without run-time overhead.
  class FindElem (t :: * -> *) (r :: [* -> *]) where
      -- | Position of the element @t :: * -> *@ in a type list @r :: [* -> *]@.
      --
      -- Position is computed during compilation, i.e. there is no run-time
      -- overhead.
      --
      -- /O(1)/
      elemNo :: P t r
  
  -- | Base case; element is at the current position in the list.
  instance FindElem t (t ': r) where
      elemNo = P 0
  
  -- | Recursion; element is not at the current position, but is somewhere in the
  -- list.
  instance PRAGMA_OVERLAPPABLE FindElem t r => FindElem t (t' ': r) where
      elemNo = P $ 1 + unP (elemNo :: P t r)
  
  -- | This type class is used for two following purposes:
  --
  -- * As a @Constraint@ it guarantees that @t :: * -> *@ is a member of a
  --   type-list @r :: [* -> *]@.
  --
  -- * Provides a way how to inject\/project @t :: * -> *@ into\/from a 'Union',
  --   respectively.
  --
  -- Following law has to hold:
  --
  -- @
  -- 'prj' . 'inj' === 'Just'
  -- @
  class FindElem t r => Member (t :: * -> *) r where
      -- | Takes a request of type @t :: * -> *@, and injects it into the
      -- 'Union'.
      --
      -- /O(1)/
      inj :: t a -> Union r a
  
      -- | Project a value of type @'Union' (t ': r) :: * -> *@ into a possible
      -- summand of the type @t :: * -> *@. 'Nothing' means that @t :: * -> *@ is
      -- not the value stored in the @'Union' (t ': r) :: * -> *@.
      --
      -- /O(1)/
      prj :: Union r a -> Maybe (t a)
  
  instance FindElem t r => Member t r where
      inj = unsafeInj $ unP (elemNo :: P t r)
      {-# INLINE inj #-}
  
      prj = unsafePrj $ unP (elemNo :: P t r)
      {-# INLINE prj #-}
  
  -- | Orthogonal decomposition of a @'Union' (t ': r) :: * -> *@. 'Right' value
  -- is returned if the @'Union' (t ': r) :: * -> *@ contains @t :: * -> *@, and
  -- 'Left' when it doesn't. Notice that 'Left' value contains
  -- @Union r :: * -> *@, i.e. it can not contain @t :: * -> *@.
  --
  -- /O(1)/
  decomp :: Union (t ': r) a -> Either (Union r a) (t a)
  decomp (Union 0 a) = Right $ unsafeCoerce a
  decomp (Union n a) = Left  $ Union (n - 1) a
  {-# INLINE [2] decomp #-}
  
  -- | Specialized version of 'decomp' for efficiency.
  --
  -- /O(1)/
  --
  -- TODO: Check that it actually adds on efficiency.
  decomp0 :: Union '[t] a -> Either (Union '[] a) (t a)
  decomp0 (Union _ a) = Right $ unsafeCoerce a
  {-# INLINE decomp0 #-}
  {-# RULES "decomp/singleton"  decomp = decomp0 #-}
  
  -- | Specialised version of 'prj'\/'decomp' that works on an
  -- @'Union' '[t] :: * -> *@ which contains only one specific summand. Hence the
  -- absence of 'Maybe', and 'Either'.
  --
  -- /O(1)/
  extract :: Union '[t] a -> t a
  extract (Union _ a) = unsafeCoerce a
  {-# INLINE extract #-}
  
  -- | Inject whole @'Union' r@ into a weaker @'Union' (any ': r)@ that has one
  -- more summand.
  --
  -- /O(1)/
  weaken :: Union r a -> Union (any ': r) a
  weaken (Union n a) = Union (n + 1) a
  {-# INLINE weaken #-}
  