    {-|
    Copyright        : (c) Galois, Inc 2014-2019
    Maintainer       : Joe Hendrix <jhendrix@galois.com>
    Description : a type family for representing a type-level string (AKA symbol) at runtime

    This defines a type family 'SymbolRepr' for representing a type-level string
    (AKA symbol) at runtime.  This can be used to branch on a type-level value.

    The 'TestEquality' and 'OrdF' instances for 'SymbolRepr' are implemented using
    'unsafeCoerce'.  This should be typesafe because we maintain the invariant
    that the string value contained in a SymbolRepr value matches its static type.

    At the type level, symbols have very few operations, so SymbolRepr
    correspondingly has very few functions that manipulate them.
    -}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE ExplicitNamespaces #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE Trustworthy #-}
    module Data.Parameterized.SymbolRepr
      ( -- * SymbolRepr
        SymbolRepr
      , symbolRepr
      , knownSymbol
      , someSymbol
      , SomeSym(SomeSym)
      , viewSomeSym
        -- * Re-exports
      , type GHC.Symbol
      , GHC.KnownSymbol
      ) where

    import           GHC.TypeLits as GHC
    import           Unsafe.Coerce (unsafeCoerce)

    import           Data.Hashable
    import           Data.Kind ( Type )
    import           Data.Proxy
    import qualified Data.Text as Text

    import           Data.Parameterized.Axiom
    import           Data.Parameterized.Classes
    import           Data.Parameterized.Some

    -- | A runtime representation of a GHC type-level symbol.
    newtype SymbolRepr (nm::GHC.Symbol)
      = SymbolRepr { forall (nm :: Symbol). SymbolRepr nm -> Text
    symbolRepr :: Text.Text
                     -- ^ The underlying text representation of the symbol
                   }
    -- INVARIANT: The contained runtime text value matches the value
    -- of the type level symbol.  The SymbolRepr constructor
    -- is not exported so we can maintain this invariant in this
    -- module.

    -- | Generate a symbol representative at runtime.  The type-level
    --   symbol will be abstract, as it is hidden by the 'Some' constructor.
    someSymbol :: Text.Text -> Some SymbolRepr
    someSymbol :: Text -> Some SymbolRepr
    someSymbol Text
    nm = SymbolRepr (ZonkAny 0) -> Some SymbolRepr
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some (Text -> SymbolRepr (ZonkAny 0)
    forall (nm :: Symbol). Text -> SymbolRepr nm
    SymbolRepr Text
    nm)

    -- | Generate a value representative for the type level symbol.
    knownSymbol :: GHC.KnownSymbol s => SymbolRepr s
    knownSymbol :: forall (s :: Symbol). KnownSymbol s => SymbolRepr s
    knownSymbol = Proxy s -> SymbolRepr s
    forall (s :: Symbol). KnownSymbol s => Proxy s -> SymbolRepr s
    go Proxy s
    forall {k} (t :: k). Proxy t
    Proxy
      where go :: GHC.KnownSymbol s => Proxy s -> SymbolRepr s
            go :: forall (s :: Symbol). KnownSymbol s => Proxy s -> SymbolRepr s
    go Proxy s
    p = Text -> SymbolRepr s
    forall (nm :: Symbol). Text -> SymbolRepr nm
    SymbolRepr (Text -> SymbolRepr s) -> Text -> SymbolRepr s
    forall a b. (a -> b) -> a -> b
    $! String -> Text
    packSymbol (Proxy s -> String
    forall (n :: Symbol) (proxy :: Symbol -> *).
    KnownSymbol n =>
    proxy n -> String
    GHC.symbolVal Proxy s
    p)

            -- NOTE here we explicitly test that unpacking the packed text value
            -- gives the desired string.  This is to avoid pathological corner cases
            -- involving string values that have no text representation.
            packSymbol :: String -> Text
    packSymbol String
    str
               | Text -> String
    Text.unpack Text
    txt String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    str = Text
    txt
               | Bool
    otherwise = String -> Text
    forall a. HasCallStack => String -> a
    error (String -> Text) -> String -> Text
    forall a b. (a -> b) -> a -> b
    $ String
    "Unrepresentable symbol! "String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    str
             where txt :: Text
    txt = String -> Text
    Text.pack String
    str

    instance (GHC.KnownSymbol s) => KnownRepr SymbolRepr s where
      knownRepr :: SymbolRepr s
    knownRepr = SymbolRepr s
    forall (s :: Symbol). KnownSymbol s => SymbolRepr s
    knownSymbol

    instance TestEquality SymbolRepr where
       testEquality :: forall (a :: Symbol) (b :: Symbol).
    SymbolRepr a -> SymbolRepr b -> Maybe (a :~: b)
    testEquality (SymbolRepr Text
    x :: SymbolRepr x) (SymbolRepr Text
    y)
          | Text
    x Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    y    = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: b
    forall {k} (a :: k) (b :: k). a :~: b
    unsafeAxiom
          | Bool
    otherwise = Maybe (a :~: b)
    forall a. Maybe a
    Nothing
    instance OrdF SymbolRepr where
       compareF :: forall (x :: Symbol) (y :: Symbol).
    SymbolRepr x -> SymbolRepr y -> OrderingF x y
    compareF (SymbolRepr Text
    x :: SymbolRepr x) (SymbolRepr Text
    y)
          | Text
    x Text -> Text -> Bool
    forall a. Ord a => a -> a -> Bool
    <  Text
    y    = OrderingF x y
    forall {k} (x :: k) (y :: k). OrderingF x y
    LTF
          | Text
    x Text -> Text -> Bool
    forall a. Eq a => a -> a -> Bool
    == Text
    y    = OrderingF x x -> OrderingF x y
    forall a b. a -> b
    unsafeCoerce (OrderingF x x
    forall {k} (x :: k). OrderingF x x
    EQF :: OrderingF x x)
          | Bool
    otherwise = OrderingF x y
    forall {k} (x :: k) (y :: k). OrderingF x y
    GTF

    -- These instances are trivial by the invariant
    -- that the contained string matches the type-level
    -- symbol
    instance Eq (SymbolRepr x) where
       SymbolRepr x
    _ == :: SymbolRepr x -> SymbolRepr x -> Bool
    == SymbolRepr x
    _ = Bool
    True
    instance EqF SymbolRepr where
       eqF :: forall (x :: Symbol). SymbolRepr x -> SymbolRepr x -> Bool
    eqF SymbolRepr a
    _ SymbolRepr a
    _ = Bool
    True
    instance Ord (SymbolRepr x) where
       compare :: SymbolRepr x -> SymbolRepr x -> Ordering
    compare SymbolRepr x
    _ SymbolRepr x
    _ = Ordering
    EQ

    instance HashableF SymbolRepr where
      hashWithSaltF :: forall (tp :: Symbol). Int -> SymbolRepr tp -> Int
    hashWithSaltF = Int -> SymbolRepr tp -> Int
    forall a. Hashable a => Int -> a -> Int
    hashWithSalt
    instance Hashable (SymbolRepr nm) where
      hashWithSalt :: Int -> SymbolRepr nm -> Int
    hashWithSalt Int
    s (SymbolRepr Text
    nm) = Int -> Text -> Int
    forall a. Hashable a => Int -> a -> Int
    hashWithSalt Int
    s Text
    nm

    instance Show (SymbolRepr nm) where
      show :: SymbolRepr nm -> String
    show (SymbolRepr Text
    nm) = Text -> String
    Text.unpack Text
    nm

    instance ShowF SymbolRepr

    -- | The SomeSym hides a Symbol parameter but preserves a
    -- KnownSymbol constraint on the hidden parameter.

    data SomeSym (c :: GHC.Symbol -> Type) =
      forall (s :: GHC.Symbol) . GHC.KnownSymbol s => SomeSym (c s)

    -- | Projects a value out of a SomeSym into a function, re-ifying the
    -- Symbol type parameter to the called function, along with the
    -- KnownSymbol constraint on that Symbol value.

    viewSomeSym :: (forall (s :: GHC.Symbol) . GHC.KnownSymbol s => c s -> r) ->
                   SomeSym c -> r
    viewSomeSym :: forall (c :: Symbol -> *) r.
    (forall (s :: Symbol). KnownSymbol s => c s -> r) -> SomeSym c -> r
    viewSomeSym forall (s :: Symbol). KnownSymbol s => c s -> r
    f (SomeSym c s
    x) = c s -> r
    forall (s :: Symbol). KnownSymbol s => c s -> r
    f c s
    x