{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Copilot.Core.Type
( Type (..)
, Typed (..)
, UType (..)
, SimpleType (..)
, typeSize
, tysize
, typeLength
, tylength
, Value (..)
, toValues
, Field (..)
, typeName
, typename
, Struct
, fieldName
, fieldname
, accessorName
, accessorname
)
where
import Data.Int (Int16, Int32, Int64, Int8)
import Data.List (intercalate)
import Data.Proxy (Proxy (..))
import Data.Type.Equality as DE
import Data.Typeable (Typeable, eqT, typeRep)
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.TypeLits (KnownNat, KnownSymbol, Symbol, natVal, sameNat,
symbolVal)
import Copilot.Core.Type.Array (Array)
{-# DEPRECATED typename "Use typeName instead." #-}
class Struct a where
typeName :: a -> String
typeName = a -> String
forall a. Struct a => a -> String
typename
typename :: a -> String
typename = a -> String
forall a. Struct a => a -> String
typeName
toValues :: a -> [Value a]
data Value a =
forall s t . (Typeable t, KnownSymbol s, Show t) => Value (Type t) (Field s t)
data Field (s :: Symbol) t = Field t
fieldName :: forall s t . KnownSymbol s => Field s t -> String
fieldName :: forall (s :: Symbol) t. KnownSymbol s => Field s t -> String
fieldName Field s t
_ = Proxy s -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy s
forall {k} (t :: k). Proxy t
Proxy :: Proxy s)
{-# DEPRECATED fieldname "Use fieldName instead." #-}
fieldname :: forall s t . KnownSymbol s => Field s t -> String
fieldname :: forall (s :: Symbol) t. KnownSymbol s => Field s t -> String
fieldname = Field s t -> String
forall (s :: Symbol) t. KnownSymbol s => Field s t -> String
fieldName
accessorName :: forall a s t . (Struct a, KnownSymbol s)
=> (a -> Field s t) -> String
accessorName :: forall a (s :: Symbol) t.
(Struct a, KnownSymbol s) =>
(a -> Field s t) -> String
accessorName a -> Field s t
_ = Proxy s -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy s
forall {k} (t :: k). Proxy t
Proxy :: Proxy s)
{-# DEPRECATED accessorname "Use accessorName instead." #-}
accessorname :: forall a s t . (Struct a, KnownSymbol s)
=> (a -> Field s t) -> String
accessorname :: forall a (s :: Symbol) t.
(Struct a, KnownSymbol s) =>
(a -> Field s t) -> String
accessorname = (a -> Field s t) -> String
forall a (s :: Symbol) t.
(Struct a, KnownSymbol s) =>
(a -> Field s t) -> String
accessorName
instance (KnownSymbol s, Show t) => Show (Field s t) where
show :: Field s t -> String
show f :: Field s t
f@(Field t
v) = Field s t -> String
forall (s :: Symbol) t. KnownSymbol s => Field s t -> String
fieldName Field s t
f String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
v
instance {-# OVERLAPPABLE #-} (Typed t, Struct t) => Show t where
show :: t -> String
show t
t = String
"<" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
fields String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
">"
where
fields :: String
fields = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Value t -> String) -> [Value t] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Value t -> String
forall {a}. Value a -> String
showfield (t -> [Value t]
forall a. Struct a => a -> [Value a]
toValues t
t)
showfield :: Value a -> String
showfield (Value Type t
_ Field s t
field) = Field s t -> String
forall a. Show a => a -> String
show Field s t
field
data Type :: * -> * where
Bool :: Type Bool
Int8 :: Type Int8
Int16 :: Type Int16
Int32 :: Type Int32
Int64 :: Type Int64
Word8 :: Type Word8
Word16 :: Type Word16
Word32 :: Type Word32
Word64 :: Type Word64
Float :: Type Float
Double :: Type Double
Array :: forall n t . ( KnownNat n
, Typed t
) => Type t -> Type (Array n t)
Struct :: (Typed a, Struct a) => a -> Type a
typeLength :: forall n t . KnownNat n => Type (Array n t) -> Int
typeLength :: forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
typeLength Type (Array n t)
_ = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
{-# DEPRECATED tylength "Use typeLength instead." #-}
tylength :: forall n t . KnownNat n => Type (Array n t) -> Int
tylength :: forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
tylength = Type (Array n t) -> Int
forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
typeLength
typeSize :: forall n t . KnownNat n => Type (Array n t) -> Int
typeSize :: forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
typeSize ty :: Type (Array n t)
ty@(Array ty' :: Type t
ty'@(Array Type t
_)) = Type (Array n t) -> Int
forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
typeLength Type (Array n t)
ty Int -> Int -> Int
forall a. Num a => a -> a -> a
* Type (Array n t) -> Int
forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
typeSize Type t
Type (Array n t)
ty'
typeSize ty :: Type (Array n t)
ty@(Array Type t
_ ) = Type (Array n t) -> Int
forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
typeLength Type (Array n t)
ty
{-# DEPRECATED tysize "Use typeSize instead." #-}
tysize :: forall n t . KnownNat n => Type (Array n t) -> Int
tysize :: forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
tysize = Type (Array n t) -> Int
forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
typeSize
instance TestEquality Type where
testEquality :: forall a b. Type a -> Type b -> Maybe (a :~: b)
testEquality Type a
Bool Type b
Bool = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
DE.Refl
testEquality Type a
Int8 Type b
Int8 = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
DE.Refl
testEquality Type a
Int16 Type b
Int16 = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
DE.Refl
testEquality Type a
Int32 Type b
Int32 = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
DE.Refl
testEquality Type a
Int64 Type b
Int64 = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
DE.Refl
testEquality Type a
Word8 Type b
Word8 = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
DE.Refl
testEquality Type a
Word16 Type b
Word16 = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
DE.Refl
testEquality Type a
Word32 Type b
Word32 = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
DE.Refl
testEquality Type a
Word64 Type b
Word64 = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
DE.Refl
testEquality Type a
Float Type b
Float = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
DE.Refl
testEquality Type a
Double Type b
Double = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
DE.Refl
testEquality (Array Type t
t1) (Array Type t
t2) =
Type t -> Type t -> Maybe (Array n t :~: Array n t)
forall (n1 :: Nat) a1 (n2 :: Nat) a2.
(KnownNat n1, KnownNat n2) =>
Type a1 -> Type a2 -> Maybe (Array n1 a1 :~: Array n2 a2)
testArrayEquality Type t
t1 Type t
t2
where
testArrayEquality :: forall n1 a1 n2 a2.
(KnownNat n1, KnownNat n2)
=> Type a1
-> Type a2
-> Maybe (Array n1 a1 :~: Array n2 a2)
testArrayEquality :: forall (n1 :: Nat) a1 (n2 :: Nat) a2.
(KnownNat n1, KnownNat n2) =>
Type a1 -> Type a2 -> Maybe (Array n1 a1 :~: Array n2 a2)
testArrayEquality Type a1
ty1 Type a2
ty2
| Just n1 :~: n2
DE.Refl <- Proxy n1 -> Proxy n2 -> Maybe (n1 :~: n2)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
(proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (Proxy n1
forall {k} (t :: k). Proxy t
Proxy :: Proxy n1) (Proxy n2
forall {k} (t :: k). Proxy t
Proxy :: Proxy n2)
, Just a1 :~: a2
DE.Refl <- Type a1 -> Type a2 -> Maybe (a1 :~: a2)
forall a b. Type a -> Type b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Type a1
ty1 Type a2
ty2
= (Array n1 a1 :~: Array n2 a2)
-> Maybe (Array n1 a1 :~: Array n2 a2)
forall a. a -> Maybe a
Just Array n1 a1 :~: Array n1 a1
Array n1 a1 :~: Array n2 a2
forall {k} (a :: k). a :~: a
DE.Refl
| Bool
otherwise
= Maybe (Array n1 a1 :~: Array n2 a2)
forall a. Maybe a
Nothing
testEquality (Struct a
_) (Struct b
_) = Maybe (a :~: b)
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT
testEquality Type a
_ Type b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing
data SimpleType where
SBool :: SimpleType
SInt8 :: SimpleType
SInt16 :: SimpleType
SInt32 :: SimpleType
SInt64 :: SimpleType
SWord8 :: SimpleType
SWord16 :: SimpleType
SWord32 :: SimpleType
SWord64 :: SimpleType
SFloat :: SimpleType
SDouble :: SimpleType
SArray :: Type t -> SimpleType
SStruct :: SimpleType
instance Eq SimpleType where
SimpleType
SBool == :: SimpleType -> SimpleType -> Bool
== SimpleType
SBool = Bool
True
SimpleType
SInt8 == SimpleType
SInt8 = Bool
True
SimpleType
SInt16 == SimpleType
SInt16 = Bool
True
SimpleType
SInt32 == SimpleType
SInt32 = Bool
True
SimpleType
SInt64 == SimpleType
SInt64 = Bool
True
SimpleType
SWord8 == SimpleType
SWord8 = Bool
True
SimpleType
SWord16 == SimpleType
SWord16 = Bool
True
SimpleType
SWord32 == SimpleType
SWord32 = Bool
True
SimpleType
SWord64 == SimpleType
SWord64 = Bool
True
SimpleType
SFloat == SimpleType
SFloat = Bool
True
SimpleType
SDouble == SimpleType
SDouble = Bool
True
(SArray Type t
t1) == (SArray Type t
t2) | Just t :~: t
DE.Refl <- Type t -> Type t -> Maybe (t :~: t)
forall a b. Type a -> Type b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Type t
t1 Type t
t2 = Bool
True
| Bool
otherwise = Bool
False
SimpleType
SStruct == SimpleType
SStruct = Bool
True
SimpleType
_ == SimpleType
_ = Bool
False
class (Show a, Typeable a) => Typed a where
typeOf :: Type a
simpleType :: Type a -> SimpleType
simpleType Type a
_ = SimpleType
SStruct
instance Typed Bool where
typeOf :: Type Bool
typeOf = Type Bool
Bool
simpleType :: Type Bool -> SimpleType
simpleType Type Bool
_ = SimpleType
SBool
instance Typed Int8 where
typeOf :: Type Int8
typeOf = Type Int8
Int8
simpleType :: Type Int8 -> SimpleType
simpleType Type Int8
_ = SimpleType
SInt8
instance Typed Int16 where
typeOf :: Type Int16
typeOf = Type Int16
Int16
simpleType :: Type Int16 -> SimpleType
simpleType Type Int16
_ = SimpleType
SInt16
instance Typed Int32 where
typeOf :: Type Int32
typeOf = Type Int32
Int32
simpleType :: Type Int32 -> SimpleType
simpleType Type Int32
_ = SimpleType
SInt32
instance Typed Int64 where
typeOf :: Type Int64
typeOf = Type Int64
Int64
simpleType :: Type Int64 -> SimpleType
simpleType Type Int64
_ = SimpleType
SInt64
instance Typed Word8 where
typeOf :: Type Word8
typeOf = Type Word8
Word8
simpleType :: Type Word8 -> SimpleType
simpleType Type Word8
_ = SimpleType
SWord8
instance Typed Word16 where
typeOf :: Type Word16
typeOf = Type Word16
Word16
simpleType :: Type Word16 -> SimpleType
simpleType Type Word16
_ = SimpleType
SWord16
instance Typed Word32 where
typeOf :: Type Word32
typeOf = Type Word32
Word32
simpleType :: Type Word32 -> SimpleType
simpleType Type Word32
_ = SimpleType
SWord32
instance Typed Word64 where
typeOf :: Type Word64
typeOf = Type Word64
Word64
simpleType :: Type Word64 -> SimpleType
simpleType Type Word64
_ = SimpleType
SWord64
instance Typed Float where
typeOf :: Type Float
typeOf = Type Float
Float
simpleType :: Type Float -> SimpleType
simpleType Type Float
_ = SimpleType
SFloat
instance Typed Double where
typeOf :: Type Double
typeOf = Type Double
Double
simpleType :: Type Double -> SimpleType
simpleType Type Double
_ = SimpleType
SDouble
instance (Typeable t, Typed t, KnownNat n) => Typed (Array n t) where
typeOf :: Type (Array n t)
typeOf = Type t -> Type (Array n t)
forall (t :: Nat) t.
(KnownNat t, Typed t) =>
Type t -> Type (Array t t)
Array Type t
forall a. Typed a => Type a
typeOf
simpleType :: Type (Array n t) -> SimpleType
simpleType (Array Type t
t) = Type t -> SimpleType
forall t. Type t -> SimpleType
SArray Type t
t
data UType = forall a . Typeable a => UType { ()
uTypeType :: Type a }
instance Eq UType where
UType Type a
ty1 == :: UType -> UType -> Bool
== UType Type a
ty2 = Type a -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Type a
ty1 TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== Type a -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Type a
ty2