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
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 = forall (n :: Symbol) (proxy :: Symbol -> Type).
KnownSymbol n =>
proxy n -> String
symbolVal (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 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
_ = forall (symbol :: Symbol). KnownSymbol symbol => SymbolType symbol
MkSymbolType
                in forall (t :: Symbol). SymbolType t -> r
cont forall a b. (a -> b) -> a -> b
$ 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) = 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
Proxy @a) (forall {k} (t :: k). 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 forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality SymbolType a
a SymbolType b
b of
            Just a :~: b
Refl -> forall k (a :: k). WOrdering a a
WEQ
            Maybe (a :~: b)
Nothing ->
                if forall k (w :: k -> Type) (t :: k).
WitnessValue w =>
w t -> WitnessValueType w
witnessToValue SymbolType a
a forall a. Ord a => a -> a -> Bool
> forall k (w :: k -> Type) (t :: k).
WitnessValue w =>
w t -> WitnessValueType w
witnessToValue SymbolType b
b
                    then forall k (a :: k) (b :: k). WOrdering a b
WGT
                    else forall k (a :: k) (b :: k). WOrdering a b
WLT

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

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

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

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