{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE KindSignatures            #-}
{-# LANGUAGE Safe                      #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE TypeOperators             #-}
{-# LANGUAGE UndecidableInstances      #-}
-- |
-- Description: Typing for Core.
-- Copyright:   (c) 2011 National Institute of Aerospace / Galois, Inc.
--
-- All expressions and streams in Core are accompanied by a representation of
-- the types of the underlying expressions used or carried by the streams.
-- This information is needed by the compiler to generate code, since it must
-- initialize variables and equivalent representations for those types in
-- the target languages.
module Copilot.Core.Type
    ( Type (..)
    , Typed (..)
    , UType (..)
    , SimpleType (..)

    , typeSize
    , tysize
    , typeLength
    , tylength

    , Value (..)
    , toValues
    , Field (..)
    , typeName
    , typename

    , Struct
    , fieldName
    , fieldname
    , accessorName
    , accessorname
    )
  where

-- External imports
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)

-- Internal imports
import Copilot.Core.Type.Array (Array)

{-# DEPRECATED typename "Use typeName instead." #-}

-- | The value of that is a product or struct, defined as a constructor with
-- several fields.
class Struct a where
  -- | Returns the name of struct in the target language.
  typeName :: a -> String
  typeName = forall a. Struct a => a -> String
typename

  -- | Returns the name of struct in the target language.
  typename :: a -> String
  typename = forall a. Struct a => a -> String
typeName

  -- | Transforms all the struct's fields into a list of values.
  toValues :: a -> [Value a]

-- | The field of a struct, together with a representation of its type.
data Value a =
  forall s t . (Typeable t, KnownSymbol s, Show t) => Value (Type t) (Field s t)

-- | A field in a struct. The name of the field is a literal at the type
-- level.
data Field (s :: Symbol) t = Field t

-- | Extract the name of a field.
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." #-}
-- | Extract the name of a field.
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

-- | Extract the name of an accessor (a function that returns a field of a
-- struct).
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." #-}
-- | Extract the name of an accessor (a function that returns a field of a
-- struct).
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

-- | A Type representing the types of expressions or values handled by
-- Copilot Core.
--
-- Note that both arrays and structs use dependently typed features. In the
-- former, the length of the array is part of the type. In the latter, the
-- names of the fields are part of the type.
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

-- | Return the length of an array from its type
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." #-}
-- | Return the length of an array from its type
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

-- | Return the total (nested) size of an array from its type
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." #-}
-- | Return the total (nested) size of an array from its type
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

-- | A simple, monomorphic representation of types that facilitates putting
-- variables in heterogeneous lists and environments in spite of their types
-- being different.
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

-- | Type equality, used to help type inference.

-- This instance is necessary, otherwise the type of SArray can't be inferred.
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

-- | A typed expression, from which we can obtain the two type representations
-- used by Copilot: 'Type' and 'SimpleType'.
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

-- | A untyped type (no phantom type).
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