{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
module Copilot.Core.Type
( Type (..)
, Typed (..)
, UType (..)
, SimpleType (..)
, tysize
, tylength
, Value (..)
, toValues
, Field (..)
, typename
, Struct
, fieldname
, accessorname
) where
import Data.Int
import Data.Word
import Copilot.Core.Type.Equality
import Copilot.Core.Type.Array
import Data.Typeable (Typeable, typeRep)
import GHC.TypeLits (KnownNat, natVal, Symbol, KnownSymbol, symbolVal)
import Data.Proxy (Proxy (..))
import Data.List (intercalate)
class Struct a where
typename :: a -> String
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)
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)
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
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)
_ = 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)
tysize :: forall n t. KnownNat n => Type (Array n t) -> Int
tysize :: forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
tysize 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
tylength Type (Array n t)
ty forall a. Num a => a -> a -> a
* forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
tysize Type t
ty'
tysize ty :: Type (Array n t)
ty@(Array Type t
_ ) = forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
tylength Type (Array n t)
ty
instance EqualType Type where
=~= :: forall a b. Type a -> Type b -> Maybe (Equal a b)
(=~=) Type a
Bool Type b
Bool = forall a. a -> Maybe a
Just forall a. Equal a a
Refl
(=~=) Type a
Int8 Type b
Int8 = forall a. a -> Maybe a
Just forall a. Equal a a
Refl
(=~=) Type a
Int16 Type b
Int16 = forall a. a -> Maybe a
Just forall a. Equal a a
Refl
(=~=) Type a
Int32 Type b
Int32 = forall a. a -> Maybe a
Just forall a. Equal a a
Refl
(=~=) Type a
Int64 Type b
Int64 = forall a. a -> Maybe a
Just forall a. Equal a a
Refl
(=~=) Type a
Word8 Type b
Word8 = forall a. a -> Maybe a
Just forall a. Equal a a
Refl
(=~=) Type a
Word16 Type b
Word16 = forall a. a -> Maybe a
Just forall a. Equal a a
Refl
(=~=) Type a
Word32 Type b
Word32 = forall a. a -> Maybe a
Just forall a. Equal a a
Refl
(=~=) Type a
Word64 Type b
Word64 = forall a. a -> Maybe a
Just forall a. Equal a a
Refl
(=~=) Type a
Float Type b
Float = forall a. a -> Maybe a
Just forall a. Equal a a
Refl
(=~=) Type a
Double Type b
Double = forall a. a -> Maybe a
Just forall a. Equal a a
Refl
(=~=) 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 Equal t t
Refl <- Type t
t1 forall (t :: * -> *) a b.
EqualType t =>
t a -> t b -> Maybe (Equal a b)
=~= 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
SBool
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