--------------------------------------------------------------------------------
-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
--------------------------------------------------------------------------------

-- | Typing for Core.
--
-- 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.

{-# LANGUAGE Safe #-}
{-# LANGUAGE  ExistentialQuantification
            , GADTs
            , KindSignatures
            , ScopedTypeVariables
            , UndecidableInstances
            , FlexibleContexts
            , DataKinds
            , FlexibleInstances
#-}

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)

-- | 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
  -- | 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 :: 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)

-- | 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 :: (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)

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

-- | 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
                         , Typed (InnerType t)
                         , Flatten t (InnerType t)
                         ) => Type t -> Type (Array n t)
  Struct  :: (Typed a, Struct a) => a -> Type a

-- | Return the length of an array from its type
tylength :: forall n t. KnownNat n => Type (Array n t) -> Int
tylength :: Type (Array n t) -> Int
tylength 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)

-- | Return the total (nested) size of an array from its type
tysize :: forall n t. KnownNat n => Type (Array n t) -> Int
tysize :: Type (Array n t) -> Int
tysize 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
tylength 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
tysize Type t
Type (Array n t)
ty'
tysize 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
tylength Type (Array n t)
ty

instance EqualType Type where
  =~= :: Type a -> Type b -> Maybe (Equal a b)
(=~=) Type a
Bool   Type b
Bool   = Equal a a -> Maybe (Equal a a)
forall a. a -> Maybe a
Just Equal a a
forall a. Equal a a
Refl
  (=~=) Type a
Int8   Type b
Int8   = Equal a a -> Maybe (Equal a a)
forall a. a -> Maybe a
Just Equal a a
forall a. Equal a a
Refl
  (=~=) Type a
Int16  Type b
Int16  = Equal a a -> Maybe (Equal a a)
forall a. a -> Maybe a
Just Equal a a
forall a. Equal a a
Refl
  (=~=) Type a
Int32  Type b
Int32  = Equal a a -> Maybe (Equal a a)
forall a. a -> Maybe a
Just Equal a a
forall a. Equal a a
Refl
  (=~=) Type a
Int64  Type b
Int64  = Equal a a -> Maybe (Equal a a)
forall a. a -> Maybe a
Just Equal a a
forall a. Equal a a
Refl
  (=~=) Type a
Word8  Type b
Word8  = Equal a a -> Maybe (Equal a a)
forall a. a -> Maybe a
Just Equal a a
forall a. Equal a a
Refl
  (=~=) Type a
Word16 Type b
Word16 = Equal a a -> Maybe (Equal a a)
forall a. a -> Maybe a
Just Equal a a
forall a. Equal a a
Refl
  (=~=) Type a
Word32 Type b
Word32 = Equal a a -> Maybe (Equal a a)
forall a. a -> Maybe a
Just Equal a a
forall a. Equal a a
Refl
  (=~=) Type a
Word64 Type b
Word64 = Equal a a -> Maybe (Equal a a)
forall a. a -> Maybe a
Just Equal a a
forall a. Equal a a
Refl
  (=~=) Type a
Float  Type b
Float  = Equal a a -> Maybe (Equal a a)
forall a. a -> Maybe a
Just Equal a a
forall a. Equal a a
Refl
  (=~=) Type a
Double Type b
Double = Equal a a -> Maybe (Equal a a)
forall a. a -> Maybe a
Just Equal a a
forall a. Equal a a
Refl
  (=~=) Type a
_ Type b
_ = Maybe (Equal a 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 Equal t t
Refl <- Type t
t1 Type t -> Type t -> Maybe (Equal t t)
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

--------------------------------------------------------------------------------

-- | 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
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, Flatten t (InnerType t), Typed (InnerType t)) => Typed (Array n t) where
  typeOf :: Type (Array n t)
typeOf                = Type t -> Type (Array n t)
forall (n :: Nat) t.
(KnownNat n, Typed t, Typed (InnerType t),
 Flatten t (InnerType t)) =>
Type t -> Type (Array n 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

--------------------------------------------------------------------------------

-- | 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 = 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

--------------------------------------------------------------------------------