module Data.Type.Witness.Specific.Symbol
    ( module Data.Type.Witness.Specific.Symbol
    , Symbol
    , KnownSymbol
    ) where

import Data.Type.Witness.General.AllConstraint
import Data.Type.Witness.General.Order
import Data.Type.Witness.General.Representative
import Data.Type.Witness.General.WitnessValue
import GHC.TypeLits
import Import

type SymbolType :: Symbol -> Type
type role SymbolType nominal
data SymbolType symbol where
    MkSymbolType :: KnownSymbol symbol => SymbolType symbol

instance WitnessValue SymbolType where
    type WitnessValueType SymbolType = String
    witnessToValue :: forall t. SymbolType t -> String
    witnessToValue :: forall (t :: Symbol). SymbolType t -> String
witnessToValue SymbolType t
MkSymbolType = Proxy t -> String
forall (n :: Symbol) (proxy :: Symbol -> Type).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy t
forall {k} (t :: k). Proxy t
Proxy :: Proxy t)
    valueToWitness :: forall r.
WitnessValueType SymbolType
-> (forall (t :: Symbol). SymbolType t -> r) -> r
valueToWitness WitnessValueType SymbolType
s forall (t :: Symbol). SymbolType t -> r
cont =
        case String -> SomeSymbol
someSymbolVal String
WitnessValueType SymbolType
s of
            SomeSymbol Proxy n
p -> let
                psw :: forall (t :: Symbol). KnownSymbol t
                    => Proxy t
                    -> SymbolType t
                psw :: forall (t :: Symbol). KnownSymbol t => Proxy t -> SymbolType t
psw Proxy t
_ = SymbolType t
forall (symbol :: Symbol). KnownSymbol symbol => SymbolType symbol
MkSymbolType
                in SymbolType n -> r
forall (t :: Symbol). SymbolType t -> r
cont (SymbolType n -> r) -> SymbolType n -> r
forall a b. (a -> b) -> a -> b
$ Proxy n -> SymbolType n
forall (t :: Symbol). KnownSymbol t => Proxy t -> SymbolType t
psw Proxy n
p

instance TestEquality SymbolType where
    testEquality :: forall (a :: Symbol) (b :: Symbol).
SymbolType a -> SymbolType b -> Maybe (a :~: b)
testEquality (SymbolType a
MkSymbolType :: SymbolType a) (SymbolType b
MkSymbolType :: SymbolType b) = Proxy a -> Proxy b -> Maybe (a :~: b)
forall (a :: Symbol) (b :: Symbol) (proxy1 :: Symbol -> Type)
       (proxy2 :: Symbol -> Type).
(KnownSymbol a, KnownSymbol b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameSymbol (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @a) (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @b)

instance TestOrder SymbolType where
    testCompare :: forall (a :: Symbol) (b :: Symbol).
SymbolType a -> SymbolType b -> WOrdering a b
testCompare SymbolType a
a SymbolType b
b =
        case SymbolType a -> SymbolType b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Symbol) (b :: Symbol).
SymbolType a -> SymbolType b -> Maybe (a :~: b)
testEquality SymbolType a
a SymbolType b
b of
            Just a :~: b
Refl -> WOrdering a a
WOrdering a b
forall k (a :: k). WOrdering a a
WEQ
            Maybe (a :~: b)
Nothing ->
                if SymbolType a -> WitnessValueType SymbolType
forall k (w :: k -> Type) (t :: k).
WitnessValue w =>
w t -> WitnessValueType w
forall (t :: Symbol). SymbolType t -> WitnessValueType SymbolType
witnessToValue SymbolType a
a String -> String -> Bool
forall a. Ord a => a -> a -> Bool
> SymbolType b -> WitnessValueType SymbolType
forall k (w :: k -> Type) (t :: k).
WitnessValue w =>
w t -> WitnessValueType w
forall (t :: Symbol). SymbolType t -> WitnessValueType SymbolType
witnessToValue SymbolType b
b
                    then WOrdering a b
forall k (a :: k) (b :: k). WOrdering a b
WGT
                    else WOrdering a b
forall k (a :: k) (b :: k). WOrdering a b
WLT

instance Representative SymbolType where
    getRepWitness :: Subrepresentative SymbolType SymbolType
getRepWitness SymbolType a
MkSymbolType = Dict (Is SymbolType a)
forall (a :: Constraint). a => Dict a
Dict

instance KnownSymbol symbol => Is SymbolType symbol where
    representative :: SymbolType symbol
representative = SymbolType symbol
forall (symbol :: Symbol). KnownSymbol symbol => SymbolType symbol
MkSymbolType

instance Show (SymbolType symbol) where
    show :: SymbolType symbol -> String
show = SymbolType symbol -> String
SymbolType symbol -> WitnessValueType SymbolType
forall k (w :: k -> Type) (t :: k).
WitnessValue w =>
w t -> WitnessValueType w
forall (t :: Symbol). SymbolType t -> WitnessValueType SymbolType
witnessToValue

instance AllConstraint Show SymbolType where
    allConstraint :: forall (t :: Symbol). Dict (Show (SymbolType t))
allConstraint = Dict (Show (SymbolType t))
forall (a :: Constraint). a => Dict a
Dict