{-# LANGUAGE TypeFamilies, GADTs, MultiParamTypeClasses, TypeOperators, FlexibleContexts, ScopedTypeVariables, ViewPatterns, FlexibleInstances, QuasiQuotes, UndecidableInstances, Rank2Types #-} {- | Module : Data.Yoko.ReflectBase Copyright : (c) The University of Kansas 2011 License : BSD3 Maintainer : nicolas.frisby@gmail.com Stability : experimental Portability : see LANGUAGE pragmas (... GHC) The basic @yoko@ reflection concepts. -} module Data.Yoko.ReflectBase where import Type.Yoko import Data.Yoko.Generic -- | The @Tag@ of a constructor type is a type-level reflection of its -- constructor name. type family Tag dc -- | The @Recurs@ of a constructor type is the type-"Type.Yoko.Sum" of types -- that occur in this constructor. NB: @Recurs t `isSubsumedBy` Siblings (Range -- dc)@. type family Recurs t -- | The \"Datatype Constructor\" class. class (DT (Range dc), dc ::: DCU (Range dc), Generic dc) => DC dc where -- | The string name of this constructor. occName :: [qP|dc|] -> String -- | The range of this constructor. type Range dc -- | The evidence that this constructor inhabits the datatype constructor -- universe of its range. tag :: DCOf (Range dc) dc; tag = inhabits -- | Project this constructor from its range. to :: Range dc -> Maybe (RMNI dc) to (disband -> NP tg fds) = case eqT tg (tag :: DCOf (Range dc) dc) of Just Refl -> Just fds _ -> Nothing -- | Embed this constructor in its range. fr :: RMNI dc -> Range dc -- | Evidence that @t@ is the range of the constructor type @dc@. data DCOf t dc where DCOf :: (DC dc, t ~ Range dc) => DCU t dc -> DCOf t dc instance (DC dc, t ~ Range dc) => dc ::: DCOf t where inhabits = DCOf inhabits type instance Inhabitants (DCOf t) = Inhabitants (DCU t) instance Finite (DCU t) => Finite (DCOf t) where toUni (DCOf x) = toUni x type instance Pred (DCOf t) dc = Elem dc (DCs t) instance EqT (DCU t) => EqT (DCOf t) where eqT (DCOf x) (DCOf y) = eqT x y data SiblingOf t s where SiblingOf :: (s ::: Uni (Siblings t), Siblings s ~ Siblings t, DT s) => Uni (Siblings t) s -> SiblingOf t s instance (s ::: Uni (Siblings t), Siblings s ~ Siblings t, DT s) => s ::: SiblingOf t where inhabits = SiblingOf inhabits type instance Inhabitants (SiblingOf t) = Siblings t instance Finite (SiblingOf t) where toUni (SiblingOf x) = x type instance Pred (SiblingOf t) s = Elem s (Siblings t) instance EqT (SiblingOf t) where eqT (SiblingOf x) (SiblingOf y) = eqT x y type AnRMN m u = NP u (RM m :. N) type Disbanded m t = AnRMN m (DCOf t) disbanded :: DC dc => RMN m dc -> Disbanded m (Range dc) disbanded fds = NP tag fds band :: Disbanded IdM t -> t band (NP (DCOf _) fds) = fr fds -- @LeftmostRange@ returns the @Range@ of the leftmost type in a type-sum. type family LeftmostRange dcs type instance LeftmostRange (N dc) = Range dc type instance LeftmostRange (c :+ d) = LeftmostRange c type DCs t = Inhabitants (DCOf t) -- | The "DataType" class. class (Finite (DCU t), EqT (DCU t), DCs t ::: All (DCOf t), -- DCs t ::: All (AsRep GistU), Siblings t ::: All (SiblingOf t) ) => DT t where -- | The string name of this datatype's original package. packageName :: [qP|t|] -> String -- | The string name of this datatype's original module. moduleName :: [qP|t|] -> String -- | A type-sum of the types in this type's binding group, including -- itself. @Siblings t@ ought to be the same for every type @t@ in the -- binding group. (It also ought to be equivalent to the transitive closure -- of @Recurs . DCs@, by definition.) type Siblings t -- | The data constructor universe. 'DCOf' is to be preferred as much as -- possible. data DCU t :: * -> * -- universe of constructor types -- | /Disband/ this type into one of its data constructors. disband :: t -> Disbanded IdM t