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,SingI,Sing,sing)
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 (SingI len, IvoryArea area) => IvoryArea (Array len area) where
ivoryArea _ = I.TyArr len area
where
len = fromInteger (fromTypeNat (sing :: Sing len))
area = ivoryArea (Proxy :: Proxy area)
instance IvoryType a => IvoryArea (Stored a) where
ivoryArea _ = ivoryType (Proxy :: Proxy a)