{-# 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 = forall a. Struct a => a -> String
typename
typename :: a -> String
typename = 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
_ = forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (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 = 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
_ = forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (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 = 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) = forall (s :: Symbol) t. KnownSymbol s => Field s t -> String
fieldName Field s t
f forall a. [a] -> [a] -> [a]
++ String
":" forall a. [a] -> [a] -> [a]
++ 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
"<" forall a. [a] -> [a] -> [a]
++ String
fields forall a. [a] -> [a] -> [a]
++ String
">"
where
fields :: String
fields = forall a. [a] -> [[a]] -> [a]
intercalate String
"," forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall {a}. Value a -> String
showfield (forall a. Struct a => a -> [Value a]
toValues t
t)
showfield :: Value a -> String
showfield (Value Type t
_ Field s t
field) = 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)
_ = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (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 = 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
_)) = forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
typeLength Type (Array n t)
ty forall a. Num a => a -> a -> a
* forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
typeSize Type t
ty'
typeSize ty :: Type (Array n t)
ty@(Array Type t
_ ) = 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 = 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 = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
DE.Refl
testEquality Type a
Int8 Type b
Int8 = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
DE.Refl
testEquality Type a
Int16 Type b
Int16 = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
DE.Refl
testEquality Type a
Int32 Type b
Int32 = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
DE.Refl
testEquality Type a
Int64 Type b
Int64 = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
DE.Refl
testEquality Type a
Word8 Type b
Word8 = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
DE.Refl
testEquality Type a
Word16 Type b
Word16 = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
DE.Refl
testEquality Type a
Word32 Type b
Word32 = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
DE.Refl
testEquality Type a
Word64 Type b
Word64 = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
DE.Refl
testEquality Type a
Float Type b
Float = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
DE.Refl
testEquality Type a
Double Type b
Double = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
DE.Refl
testEquality (Array Type t
t1) (Array Type t
t2) =
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 <- forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
(proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy :: Proxy n1) (forall {k} (t :: k). Proxy t
Proxy :: Proxy n2)
, Just a1 :~: a2
DE.Refl <- forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Type a1
ty1 Type a2
ty2
= forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
DE.Refl
| Bool
otherwise
= forall a. Maybe a
Nothing
testEquality (Struct a
_) (Struct b
_) = forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT
testEquality Type a
_ Type 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 <- 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 = forall (t :: Nat) t.
(KnownNat t, Typed t) =>
Type t -> Type (Array t t)
Array forall a. Typed a => Type a
typeOf
simpleType :: Type (Array n t) -> SimpleType
simpleType (Array Type t
t) = 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 = forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Type a
ty1 forall a. Eq a => a -> a -> Bool
== forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Type a
ty2