{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, GADTs, ScopedTypeVariables, FlexibleContexts, UndecidableInstances, QuasiQuotes, TypeOperators, TypeSynonymInstances, Rank2Types, ViewPatterns #-} {- | Module : Data.Yoko.Reflect Copyright : (c) The University of Kansas 2011 License : BSD3 Maintainer : nicolas.frisby@gmail.com Stability : experimental Portability : see LANGUAGE pragmas (... GHC) Definitions on top of the basic @yoko@ reflection concepts "Data.Yoko.ReflectBase". -} module Data.Yoko.Reflect (module Data.Yoko.Reflect, module Data.Yoko.ReflectBase) where import Type.Yoko import Data.Yoko.Generic import Data.Yoko.ReflectBase type instance Tag (N dc) = Tag dc type instance Recurs (D a) = V type instance Recurs (F f c) = Recurs c type instance Recurs (FF ff c d) = NormW (Recurs c) (Recurs d) -- NormW avoiding duplication type instance Recurs (M i c) = Recurs c type instance Recurs (N t) = Recurs (Rep t) type instance Recurs (R t) = N t type instance Recurs U = V type instance Recurs V = V type SiblingsU t = Uni (Siblings t) data IsDC dc where IsDC :: DC dc => IsDC dc type instance Pred IsDC t = True instance DC dc => dc ::: IsDC where inhabits = IsDC newtype RMNTo m b dc = RMNTo {rmnTo :: RMN m dc -> b} type instance Unwrap (RMNTo m b) dc = RMN m dc -> b instance Wrapper (RMNTo m b) where wrap = RMNTo; unwrap = rmnTo -- | Just a specialization: @dcDispatch = (. disband) . dcDispatch'@. dcDispatch :: DT t => NT (DCU t) (RMNTo IdM b) -> t -> b dcDispatch = (. disband) . dcDispatch' -- | Just a specialization: @dcDispatch' nt ('NP' ('DCOf' tag) fds) = 'appNT' -- nt tag fds@. dcDispatch' :: DT t => NT (DCU t) (RMNTo IdM b) -> Disbanded IdM t -> b dcDispatch' nt (NP (DCOf tag) fds) = appNT nt tag fds {- | A fundamental notion of identity in @yoko@, the @TagRepIs tag c@ universe contains all constructor types @dc@ where @(Tag dc ~ tag, c ~ Rep dc)@. @ type instance Pred (TagRepIs tag c) dc = And (IsEQ (Compare (Tag dc) tag)) (IsEQ (Compare (Rep dc) c)) @ -} data TagRepIs tag c dc where TagRepIs :: (Tag dc ~ tag, c ~ Rep dc) => TagRepIs tag c dc instance (Tag dc ~ tag, c ~ Rep dc) => dc ::: TagRepIs tag c where inhabits = TagRepIs type instance Pred (TagRepIs tag c) dc = And (IsEQ (Compare (Tag dc) tag)) (IsEQ (Compare (Rep dc) c)) {-data TagGistEQ tag gst m dc where TagGistEQ :: (Tag dc ~ tag, Gist (N dc), Gst (N dc) m ~ gst ) => TagGistEQ tag gst m dc instance (Tag dc ~ tag, Gist (N dc), Gst (N dc) m ~ gst ) => dc ::: TagGistEQ tag gst m where inhabits = TagGistEQ type instance Pred (TagGistEQ tag gst m) dc = And (IsEQ (Compare (Tag dc) tag)) (IsEQ (Compare (Gst (N dc) m) gst))-} -- | Just a specialization: @bandDCs = band@. bandDCs :: DT t => Disbanded IdM t -> t; bandDCs = band fr_DCOf :: DCOf t dc -> RMNI dc -> t; fr_DCOf (DCOf _) = fr