{-|
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.Classes
import           Data.Parameterized.Some

-- | A runtime representation of a GHC type-level symbol.
newtype SymbolRepr (nm::GHC.Symbol)
  = SymbolRepr { 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 Any -> Some SymbolRepr
forall k (f :: k -> *) (x :: k). f x -> Some f
Some (Text -> SymbolRepr Any
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 :: 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 :: 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 :: 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 :~: a) -> a :~: b
forall a b. a -> b
unsafeCoerce (a :~: a
forall k (a :: k). a :~: a
Refl :: x :~: x))
      | Bool
otherwise = Maybe (a :~: b)
forall a. Maybe a
Nothing
instance OrdF SymbolRepr where
   compareF :: 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 Ord (SymbolRepr x) where
   compare :: SymbolRepr x -> SymbolRepr x -> Ordering
compare SymbolRepr x
_ SymbolRepr x
_ = Ordering
EQ

instance HashableF SymbolRepr where
  hashWithSaltF :: 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 (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