{-|
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 = forall k (f :: k -> *) (x :: k). f x -> Some f
Some (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 = forall (s :: Symbol). KnownSymbol s => Proxy s -> SymbolRepr s
go 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 = forall (nm :: Symbol). Text -> SymbolRepr nm
SymbolRepr forall a b. (a -> b) -> a -> b
$! String -> Text
packSymbol (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 forall a. Eq a => a -> a -> Bool
== String
str = Text
txt
           | Bool
otherwise = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Unrepresentable symbol! "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 = 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 forall a. Eq a => a -> a -> Bool
== Text
y    = forall a. a -> Maybe a
Just forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom
      | Bool
otherwise = 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 forall a. Ord a => a -> a -> Bool
<  Text
y    = forall {k} (x :: k) (y :: k). OrderingF x y
LTF
      | Text
x forall a. Eq a => a -> a -> Bool
== Text
y    = forall a b. a -> b
unsafeCoerce (forall {k} (x :: k). OrderingF x x
EQF :: OrderingF x x)
      | Bool
otherwise = 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 :: forall (tp :: Symbol). Int -> SymbolRepr tp -> Int
hashWithSaltF = forall a. Hashable a => Int -> a -> Int
hashWithSalt
instance Hashable (SymbolRepr nm) where
  hashWithSalt :: Int -> SymbolRepr nm -> Int
hashWithSalt Int
s (SymbolRepr Text
nm) = 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) = forall (s :: Symbol). KnownSymbol s => c s -> r
f c s
x