{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RankNTypes #-}

-- | Internally used existential type for tracking of annotations
--
-- This module is re-exported in "Data.TypedEncoding" and it is best not to import it directly.

module Examples.TypedEncoding.SomeEnc.SomeAnnotation where

import           Data.TypedEncoding.Common.Types.Common
import           Data.TypedEncoding.Common.Class.Common
import           Data.TypedEncoding.Common.Util.TypeLits (withSomeSymbol, proxyCons)
import           Data.Proxy
import           GHC.TypeLits

-- |
-- @since 0.2.0.0
data SomeAnnotation where
    MkSomeAnnotation :: SymbolList xs => Proxy xs -> SomeAnnotation

-- |
-- @since 0.2.0.0
withSomeAnnotation :: SomeAnnotation -> (forall xs . SymbolList xs => Proxy xs -> r) -> r
withSomeAnnotation :: SomeAnnotation
-> (forall (xs :: [Symbol]).
    SymbolList xs =>
    Proxy @[Symbol] xs -> r)
-> r
withSomeAnnotation (MkSomeAnnotation Proxy @[Symbol] xs
p) forall (xs :: [Symbol]). SymbolList xs => Proxy @[Symbol] xs -> r
fn = Proxy @[Symbol] xs -> r
forall (xs :: [Symbol]). SymbolList xs => Proxy @[Symbol] xs -> r
fn Proxy @[Symbol] xs
p


-- | folds over SomeSymbol list 
-- @since 0.2.0.0
someAnnValue :: [EncAnn] -> SomeAnnotation
someAnnValue :: [EncAnn] -> SomeAnnotation
someAnnValue [EncAnn]
xs = 
     (EncAnn -> SomeAnnotation -> SomeAnnotation)
-> SomeAnnotation -> [EncAnn] -> SomeAnnotation
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (SomeSymbol -> SomeAnnotation -> SomeAnnotation
fn (SomeSymbol -> SomeAnnotation -> SomeAnnotation)
-> (EncAnn -> SomeSymbol)
-> EncAnn
-> SomeAnnotation
-> SomeAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EncAnn -> SomeSymbol
someSymbolVal) (Proxy @[Symbol] ('[] @Symbol) -> SomeAnnotation
forall (xs :: [Symbol]).
SymbolList xs =>
Proxy @[Symbol] xs -> SomeAnnotation
MkSomeAnnotation (forall k. Proxy @[k] ('[] @k)
forall k (t :: k). Proxy @k t
Proxy :: Proxy '[])) [EncAnn]
xs
     where 
         somesymbs :: [SomeSymbol]
somesymbs = (EncAnn -> SomeSymbol) -> [EncAnn] -> [SomeSymbol]
forall a b. (a -> b) -> [a] -> [b]
map EncAnn -> SomeSymbol
someSymbolVal [EncAnn]
xs
         fn :: SomeSymbol -> SomeAnnotation -> SomeAnnotation
fn SomeSymbol
ss (MkSomeAnnotation Proxy @[Symbol] xs
pxs) = SomeSymbol
-> (forall (x :: Symbol).
    KnownSymbol x =>
    Proxy @Symbol x -> SomeAnnotation)
-> SomeAnnotation
forall r.
SomeSymbol
-> (forall (x :: Symbol). KnownSymbol x => Proxy @Symbol x -> r)
-> r
withSomeSymbol SomeSymbol
ss (\Proxy @Symbol x
px -> Proxy @[Symbol] ((':) @Symbol x xs) -> SomeAnnotation
forall (xs :: [Symbol]).
SymbolList xs =>
Proxy @[Symbol] xs -> SomeAnnotation
MkSomeAnnotation  (Proxy @Symbol x
px Proxy @Symbol x
-> Proxy @[Symbol] xs -> Proxy @[Symbol] ((':) @Symbol x xs)
forall (x :: Symbol) (xs :: [Symbol]).
Proxy @Symbol x
-> Proxy @[Symbol] xs -> Proxy @[Symbol] ((':) @Symbol x xs)
`proxyCons` Proxy @[Symbol] xs
pxs))