{-|
Module      : Language.Grammars.AspectAG.HList
Description : Heterogeneous Lists for AAG, inspired on HList
Copyright   : (c) Juan García Garland, 2018 
License     : LGPL
Maintainer  : jpgarcia@fing.edu.uy
Stability   : experimental
Portability : POSIX

Implementation of strongly typed heterogeneous lists.
-}

{-# LANGUAGE TypeInType,
             GADTs,
             KindSignatures,
             TypeOperators,
             TypeFamilies,
             MultiParamTypeClasses,
             FlexibleInstances,
             FlexibleContexts,
             StandaloneDeriving,
             UndecidableInstances,
             FunctionalDependencies,
             ConstraintKinds,
             ScopedTypeVariables
#-}

module Language.Grammars.AspectAG.HList where

import Data.Type.Bool
import Data.GenRec.Label
import Data.Proxy
import Data.Type.Equality
import Data.Kind
import GHC.Exts

-- |Heterogeneous lists are implemented as a GADT
data HList (l :: [Type]) :: Type  where
  HNil :: HList '[]
  HCons :: x -> HList xs -> HList (x ': xs)


-- | HMember is a test membership function.
--Since we are in Haskell the value level function computes with the evidence 
class HMember (t :: Type) (l :: [Type]) where
  type HMemberRes t l :: Bool
  hMember :: Label t -> HList l -> Proxy (HMemberRes t l)

instance HMember t '[] where
  type HMemberRes t '[] = 'False
  hMember :: Label t -> HList '[] -> Proxy (HMemberRes t '[])
hMember Label t
_ HList '[]
_ = Proxy (HMemberRes t '[])
forall k (t :: k). Proxy t
Proxy

instance HMember t (t' ': ts) where
  type HMemberRes t (t' ': ts) = t == t' || HMemberRes t ts
  hMember :: Label t -> HList (t' : ts) -> Proxy (HMemberRes t (t' : ts))
hMember Label t
_ HList (t' : ts)
_ = Proxy (HMemberRes t (t' : ts))
forall k (t :: k). Proxy t
Proxy

-- | HMember' is a test membership function.
-- But looking up in a list of Labels
class HMember' (t :: k) (l :: [k]) where
  type HMemberRes' t l :: Bool
  hMember' :: f t -> KList l -> Proxy (HMemberRes' t l)

instance HMember' t '[] where
  type HMemberRes' t '[] = 'False
  hMember' :: f t -> KList '[] -> Proxy (HMemberRes' t '[])
hMember' f t
_ KList '[]
_ = Proxy (HMemberRes' t '[])
forall k (t :: k). Proxy t
Proxy

instance HMember' t (t' ': ts) where
  type HMemberRes' t (t' ': ts) = t == t' || HMemberRes' t ts
  hMember' :: f t -> KList (t' : ts) -> Proxy (HMemberRes' t (t' : ts))
hMember' f t
_ KList (t' : ts)
_ = Proxy (HMemberRes' t (t' : ts))
forall k (t :: k). Proxy t
Proxy


-- | No other functionality is needed for AAG

infixr 2 .:
.: :: x -> HList xs -> HList (x : xs)
(.:) = x -> HList xs -> HList (x : xs)
forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons
ε :: HList '[]
ε = HList '[]
HNil

-- | a polykinded heteogeneous list
data KList (l :: [k]) :: Type where
  KNil :: KList '[]
  KCons :: Label h -> KList l -> KList (h ': l)

infixr 2 .:.
.:. :: Label h -> KList l -> KList (h : l)
(.:.) = Label h -> KList l -> KList (h : l)
forall k (h :: k) (l :: [k]). Label h -> KList l -> KList (h : l)
KCons
eL :: KList '[]
eL = KList '[]
forall k. KList '[]
KNil