{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE DeriveDataTypeable         #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures             #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE PolyKinds                  #-}
{-# LANGUAGE RankNTypes                 #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE CPP                        #-}

{-# OPTIONS_GHC -Wall #-}

-- TODO: Complex Numbers

{-|

Embeds Fortran's type system in Haskell via the 'D' GADT.

== Note: Phantom Types and GADTs

Lots of the data types in this module are parameterised by phantom types. These
are types which appear at the type-level, but not at the value level. They are
there to make things more type-safe.

In addition, a lot of the data types are GADTs. In a phantom-type-indexed GADT,
the phantom type often restricts which GADT constructors a particular value may
be an instance of. This is very useful for restricting value-level terms based
on type-level information.

-}

module Language.Fortran.Model.Types where

import           Data.Int                              (Int16, Int32, Int64,
                                                        Int8)
import           Data.List                             (intersperse)
import           Data.Monoid                           (Endo (..))
import           Data.Typeable                         (Typeable)
import           Data.Word                             (Word8)

#if MIN_VERSION_singletons(3,0,0)
import           GHC.TypeLits.Singletons
#else
import           Data.Singletons.TypeLits
#endif

import           Data.Vinyl                            hiding (Field)
import           Data.Vinyl.Functor                    hiding (Field)

import           Language.Expression.Pretty

import           Language.Fortran.Model.Singletons

--------------------------------------------------------------------------------
-- * Fortran Types

{-|

This is the main embedding of Fortran types. A value of type @D a@ represents
the Fortran type which corresponds to the Haskell type @a@. @a@ is a phantom
type parameter. There is at most one instance of @D a@ for each @a@. This means
that a value of type @D a@ acts as a kind of proof that it possible to have a
Fortran type corresponding to the Haskell type @a@ -- and that when you match on
@D a@ knowing the particular @a@ you have, you know which constructor you will
get. This is a nice property because it means that GHC (with
@-fwarn-incomplete-patterns@) will not warn when you match on an impossible
case. It eliminates situations where you'd otherwise write @error "impossible:
..."@.

* @'DPrim' p :: D ('PrimS' a)@ is for primitive types. It contains a value @p@
  of type @'Prim' p k a@ for some @p@, @k@, @a@. When matching on something of
  type @D ('PrimS' a)@, you know it can only contain a primitive type.

* @'DArray' i v :: D ('Array' i v)@ is for arrays. It contains instances of @'Index'
  i@ and @'ArrValue' a@. @'Index' i@ is a proof that @i@ can be used as an index,
  and @'ArrValue' a@ is a proof that @a@ can be stored in arrays.

* @'DData' s xs :: D ('Record' name fs)@ is for user-defined data types. The
  type has a name, represented at the type level by the type parameter @name@ of
  kind 'Symbol'. The constructor contains @s :: 'SSymbol' name@, which acts as a
  sort of value-level representation of the name. 'SSymbol' is from the
  @singletons@ library. It also contains @xs :: 'Rec' ('Field' D) fs@. @fs@ is a
  type-level list of pairs, pairing field names with field types. @'Field' D
  '(fname, b)@ is a value-level pair of @'SSymbol' fname@ and @D b@. The vinyl
  record is a list of fields, one for each pair in @fs@.

-}
data D a where
  DPrim :: Prim p k a -> D (PrimS a)
  DArray :: Index i -> ArrValue a -> D (Array i a)
  DData :: (RMap fs, RecordToList fs, RApply fs) => SSymbol name -> Rec (Field D) fs -> D (Record name fs)

--------------------------------------------------------------------------------
-- * Semantic Types

newtype Bool8  = Bool8 { getBool8 :: Int8 } deriving (Show, Num, Eq, Typeable)
newtype Bool16 = Bool16 { getBool16 :: Int16 } deriving (Show, Num, Eq, Typeable)
newtype Bool32 = Bool32 { getBool32 :: Int32 } deriving (Show, Num, Eq, Typeable)
newtype Bool64 = Bool64 { getBool64 :: Int64 } deriving (Show, Num, Eq, Typeable)
newtype Char8  = Char8 { getChar8 :: Word8 } deriving (Show, Num, Eq, Typeable)

{-|

This newtype wrapper is used in 'DPrim' for semantic primitive types. This means
that when matching on something of type @'D' ('PrimS' a)@, we know it can't be
an array or a record.

-}
newtype PrimS a = PrimS { getPrimS :: a }
  deriving (Show, Eq, Typeable)

--------------------------------------------------------------------------------
-- * Primitive Types

{-|

Lists the allowed primitive Fortran types. For example, @'PInt8' :: 'Prim' 'P8
''BTInt' 'Int8'@ represents 8-bit integers. 'Prim' has three phantom type
parameters: precision, base type and semantic Haskell type. Precision is the
number of bits used to store values of that type. The base type represents the
corresponding Fortran base type, e.g. @integer@ or @real@. Constructors are only
provided for those Fortran types which are semantically valid, so for example no
constructor is provided for a 16-bit real. A value of type @'Prim' p k a@ can be
seen as a proof that there is some Fortran primitive type with those parameters.

-}
data Prim p k a where
  PInt8          :: Prim 'P8   'BTInt     Int8
  PInt16         :: Prim 'P16  'BTInt     Int16
  PInt32         :: Prim 'P32  'BTInt     Int32
  PInt64         :: Prim 'P64  'BTInt     Int64

  PBool8         :: Prim 'P8   'BTLogical Bool8
  PBool16        :: Prim 'P16  'BTLogical Bool16
  PBool32        :: Prim 'P32  'BTLogical Bool32
  PBool64        :: Prim 'P64  'BTLogical Bool64

  PFloat         :: Prim 'P32  'BTReal    Float
  PDouble        :: Prim 'P64  'BTReal    Double

  PChar          :: Prim 'P8   'BTChar    Char8

--------------------------------------------------------------------------------
-- * Arrays

-- | Specifies which types can be used as array indices.
data Index a where
  Index :: Prim p 'BTInt a -> Index (PrimS a)

-- | Specifies which types can be stored in arrays. Currently arrays of arrays
-- are not supported.
data ArrValue a where
  ArrPrim :: Prim p k a -> ArrValue (PrimS a)
  ArrData :: (RMap fs, RecordToList fs, RApply fs) => SSymbol name -> Rec (Field ArrValue) fs -> ArrValue (Record name fs)


-- | An array with a phantom index type. Mostly used at the type-level to
-- constrain instances of @'D' (Array i a)@ etc.
newtype Array i a = Array [a]

--------------------------------------------------------------------------------
-- * Records

-- | A field over a pair of name and value type.
data Field f field where
  Field :: SSymbol name -> f a -> Field f '(name, a)

-- | A type of records with the given @name@ and @fields@. Mostly used at the
-- type level to constrain instances of @'D' (Record name fields)@ etc.
data Record name fields where
  Record :: RMap fields => SSymbol name -> Rec (Field Identity) fields -> Record name fields

--------------------------------------------------------------------------------
-- * Combinators

-- | Any Fortran index type is a valid Fortran type.
dIndex :: Index i -> D i
dIndex (Index p) = DPrim p

-- | Anything that can be stored in Fortran arrays is a valid Fortran type.
dArrValue :: ArrValue a -> D a
dArrValue (ArrPrim p) = DPrim p
dArrValue (ArrData nameSym fieldArrValues) =
  DData nameSym (rmap (overField' dArrValue) fieldArrValues)

-- | Given a field with known contents, we can change the functor and value
-- type.
overField :: (f a -> g b) -> Field f '(name, a) -> Field g '(name, b)
overField f (Field n x) = Field n (f x)

-- | Given a field with unknown contents, we can change the functor but not the
-- value type.
overField' :: (forall a. f a -> g a) -> Field f nv -> Field g nv
overField' f (Field n x) = Field n (f x)

traverseField' :: (Functor t) => (forall a. f a -> t (g a)) -> Field f nv -> t (Field g nv)
traverseField' f (Field n x) = Field n <$> f x

-- | Combine two fields over the same name-value pair but (potentially)
-- different functors.
zipFieldsWith :: (forall a. f a -> g a -> h a) -> Field f nv -> Field g nv -> Field h nv
zipFieldsWith f (Field _ x) (Field n y) = Field n (f x y)

zip3FieldsWith
  :: (forall a. f a -> g a -> h a -> i a)
  -> Field f nv
  -> Field g nv
  -> Field h nv
  -> Field i nv
zip3FieldsWith f (Field _ x) (Field _ y) (Field n z) = Field n (f x y z)

--------------------------------------------------------------------------------
--  Pretty Printing

instance Pretty1 (Prim p k) where
  prettys1Prec p = \case
    PInt8   -> showString "integer8"
    PInt16  -> showString "integer16"
    PInt32  -> showString "integer32"
    PInt64  -> showString "integer64"
    PFloat  -> showString "real"
    PDouble -> showParen (p > 8) $ showString "double precision"
    PBool8  -> showString "logical8"
    PBool16 -> showString "logical16"
    PBool32 -> showString "logical32"
    PBool64 -> showString "logical64"
    PChar   -> showString "character"

instance Pretty1 ArrValue where
  prettys1Prec p = prettys1Prec p . dArrValue

instance (Pretty1 f) => Pretty1 (Field f) where
  prettys1Prec _ = \case
    Field fname x ->
      prettys1Prec 0 x .
      showString " " .
      withKnownSymbol fname (showString (symbolVal fname))

-- | e.g. "type custom_type { character a, integer array b }"
instance Pretty1 D where
  prettys1Prec p = \case
    DPrim px -> prettys1Prec p px
    DArray _ pv -> prettys1Prec p pv . showString " array"
    DData rname fields ->
        showParen (p > 8)
      $ showString "type "
      . withKnownSymbol rname (showString (symbolVal rname))
      . showString "{ "
      . appEndo ( mconcat
              . intersperse (Endo $ showString ", ")
              . recordToList
              . rmap (Const . Endo . prettys1Prec 0)
              $ fields)
      . showString " }"