{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Ivory.Language.Area where
import Ivory.Language.Proxy
import Ivory.Language.Type
import qualified Ivory.Language.Syntax as I
import GHC.TypeLits (Nat, Symbol)
type AProxy a = Proxy (a :: Area *)
data Area k
= Struct Symbol
| Array Nat (Area k)
| CArray (Area k)
| Stored k
class IvoryArea (a :: Area *) where
ivoryArea :: Proxy a -> I.Type
instance (ANat len, IvoryArea area)
=> IvoryArea ('Array len area) where
ivoryArea _ = I.TyArr len area
where
len = fromInteger (fromTypeNat (aNat :: NatType len))
area = ivoryArea (Proxy :: Proxy area)
instance IvoryType a => IvoryArea ('Stored a) where
ivoryArea _ = ivoryType (Proxy :: Proxy a)