content: {-|
  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 { 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 nm = Some (SymbolRepr nm)
  
  -- | Generate a value representative for the type level symbol.
  knownSymbol :: GHC.KnownSymbol s => SymbolRepr s
  knownSymbol = go Proxy
    where go :: GHC.KnownSymbol s => Proxy s -> SymbolRepr s
          go p = SymbolRepr $! packSymbol (GHC.symbolVal 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 str
             | Text.unpack txt == str = txt
             | otherwise = error $ "Unrepresentable symbol! "++ str
           where txt = Text.pack str
  
  instance (GHC.KnownSymbol s) => KnownRepr SymbolRepr s where
    knownRepr = knownSymbol
  
  instance TestEquality SymbolRepr where
     testEquality (SymbolRepr x :: SymbolRepr x) (SymbolRepr y)
        | x == y    = Just unsafeAxiom
        | otherwise = Nothing
  instance OrdF SymbolRepr where
     compareF (SymbolRepr x :: SymbolRepr x) (SymbolRepr y)
        | x <  y    = LTF
        | x == y    = unsafeCoerce (EQF :: OrderingF x x)
        | otherwise = GTF
  
  -- These instances are trivial by the invariant
  -- that the contained string matches the type-level
  -- symbol
  instance Eq (SymbolRepr x) where
     _ == _ = True
  instance EqF SymbolRepr where
     eqF _ _ = True
  instance Ord (SymbolRepr x) where
     compare _ _ = EQ
  
  instance HashableF SymbolRepr where
    hashWithSaltF = hashWithSalt
  instance Hashable (SymbolRepr nm) where
    hashWithSalt s (SymbolRepr nm) = hashWithSalt s nm
  
  instance Show (SymbolRepr nm) where
    show (SymbolRepr nm) = Text.unpack 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 f (SomeSym x) = f x
  