{-# LANGUAGE GeneralizedNewtypeDeriving #-}

module Dino.Types
  ( module Dino.Types
  , Inspectable
  ) where

import Dino.Prelude

import Data.Type.Equality ((:~:) (..), TestEquality (..))
import Data.Typeable (cast)
import Type.Reflection (typeRep)

import Dino.AST (Inspectable)

-- | Built-in Dino types
--
-- Whether or not a type is built-in is mostly an implementation detail.
type family BuiltIn a :: Bool where
  BuiltIn [a]    = 'True
  BuiltIn (a, b) = 'True
  BuiltIn a      = 'False

data DinoTypeRep a where
  ListType  :: DinoTypeRep a -> DinoTypeRep [a]
  PairType  :: DinoTypeRep a -> DinoTypeRep b -> DinoTypeRep (a, b)
  OtherType :: (BuiltIn a ~ 'False, DinoType a) => DinoTypeRep a
  -- The `BuiltIn` constraint ensures that `DinoTypeRep` is a canonical
  -- representation for built-in types. This allows us to give total definitions
  -- of functions like `listElemType`.

  -- The reason for having a separate constructor for list types is solely to be
  -- able to implement functions like `listElemType`.

  -- The constraints on `OtherType` are somewhat arbitrary. We may bring in
  -- other constraints in the future if that is needed by a particular back end.
  -- However, we should avoid using type classes from a back end directly.
  -- Rather use generic ones, such as `Data`. We can also have different
  -- constructors for different types; e.g. numeric types, enumerations, etc.

withType :: DinoTypeRep a -> (DinoType a => b) -> b
withType :: DinoTypeRep a -> (DinoType a => b) -> b
withType (ListType DinoTypeRep a
t)   DinoType a => b
b = DinoTypeRep a -> (DinoType a => b) -> b
forall a b. DinoTypeRep a -> (DinoType a => b) -> b
withType DinoTypeRep a
t DinoType a => b
DinoType a => b
b
withType (PairType DinoTypeRep a
t DinoTypeRep b
u) DinoType a => b
b = DinoTypeRep a -> (DinoType a => b) -> b
forall a b. DinoTypeRep a -> (DinoType a => b) -> b
withType DinoTypeRep a
t ((DinoType a => b) -> b) -> (DinoType a => b) -> b
forall a b. (a -> b) -> a -> b
$ DinoTypeRep b -> (DinoType b => b) -> b
forall a b. DinoTypeRep a -> (DinoType a => b) -> b
withType DinoTypeRep b
u DinoType a => b
DinoType b => b
b
withType DinoTypeRep a
OtherType      DinoType a => b
b = b
DinoType a => b
b

listTypeElem :: DinoTypeRep [a] -> DinoTypeRep a
listTypeElem :: DinoTypeRep [a] -> DinoTypeRep a
listTypeElem (ListType DinoTypeRep a
t) = DinoTypeRep a
DinoTypeRep a
t
  -- This function is total due to the `BuiltIn` constraint on `OtherType`.

-- | This instance is complete in the sense that if @t ~ u@, then
-- @`testEquality` (trep :: `DinoTypeRep` t) (urep :: `DinoTypeRep` u)@ returns
-- @`Just` `Refl`@.
--
-- For example, @`BoolType`@ and @`EnumType` :: `DinoTypeRep` `Bool`@ are
-- considered equal.
instance TestEquality DinoTypeRep where
  testEquality :: forall t u. DinoTypeRep t -> DinoTypeRep u -> Maybe (t :~: u)
  testEquality :: DinoTypeRep t -> DinoTypeRep u -> Maybe (t :~: u)
testEquality DinoTypeRep t
t DinoTypeRep u
u = DinoTypeRep t -> (DinoType t => Maybe (t :~: u)) -> Maybe (t :~: u)
forall a b. DinoTypeRep a -> (DinoType a => b) -> b
withType DinoTypeRep t
t ((DinoType t => Maybe (t :~: u)) -> Maybe (t :~: u))
-> (DinoType t => Maybe (t :~: u)) -> Maybe (t :~: u)
forall a b. (a -> b) -> a -> b
$ DinoTypeRep u -> (DinoType u => Maybe (t :~: u)) -> Maybe (t :~: u)
forall a b. DinoTypeRep a -> (DinoType a => b) -> b
withType DinoTypeRep u
u ((DinoType u => Maybe (t :~: u)) -> Maybe (t :~: u))
-> (DinoType u => Maybe (t :~: u)) -> Maybe (t :~: u)
forall a b. (a -> b) -> a -> b
$
    TypeRep t -> TypeRep u -> Maybe (t :~: u)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (Typeable t => TypeRep t
forall k (a :: k). Typeable a => TypeRep a
typeRep @t) (Typeable u => TypeRep u
forall k (a :: k). Typeable a => TypeRep a
typeRep @u)
    -- Note: Because `DinoTypeRep` is a canonical representation of Dino types,
    -- testing equality via `typeRep` should correspond to structural equality.

class (Eq a, Show a, Typeable a, Inspectable a) => DinoType a where
  dinoTypeRep :: DinoTypeRep a

  default dinoTypeRep :: (BuiltIn a ~ 'False) => DinoTypeRep a
  dinoTypeRep = DinoTypeRep a
forall a. (BuiltIn a ~ 'False, DinoType a) => DinoTypeRep a
OtherType

instance DinoType ()
instance DinoType Bool
instance DinoType Rational
instance DinoType Int
instance DinoType Integer
instance DinoType Float
instance DinoType Double
instance DinoType Text
instance DinoType a => DinoType (Maybe a)

instance DinoType a => DinoType [a] where
  dinoTypeRep :: DinoTypeRep [a]
dinoTypeRep = DinoTypeRep a -> DinoTypeRep [a]
forall a. DinoTypeRep a -> DinoTypeRep [a]
ListType DinoTypeRep a
forall a. DinoType a => DinoTypeRep a
dinoTypeRep

instance (DinoType a, DinoType b) => DinoType (a, b) where
  dinoTypeRep :: DinoTypeRep (a, b)
dinoTypeRep = DinoTypeRep a -> DinoTypeRep b -> DinoTypeRep (a, b)
forall a b. DinoTypeRep a -> DinoTypeRep b -> DinoTypeRep (a, b)
PairType DinoTypeRep a
forall a. DinoType a => DinoTypeRep a
dinoTypeRep DinoTypeRep b
forall a. DinoType a => DinoTypeRep a
dinoTypeRep

-- | Dynamic type based on 'DinoType'
data Dinamic where
  Dinamic :: DinoType a => a -> Dinamic

fromDinamic :: DinoType a => Dinamic -> Maybe a
fromDinamic :: Dinamic -> Maybe a
fromDinamic (Dinamic a
a) = a -> Maybe a
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast a
a