ReflectBase.hs

{-# 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 :: DCU (Range dc) dc; tag = inhabits

  -- | Project this constructor from its range.
  to :: Range dc -> Maybe (RMNI dc)
  to (disband -> NP tg fds) = case tg of
    DCOf (eqT (tag :: DCU (Range dc) dc) -> 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)

-- | @UniqueDC@ is for newtypes and GADT constructors where the type @dc@
-- determines the constructor.
class UniqueDC dc where uniqueTo :: Range dc -> RMNI dc




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 (DCOf 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 (DCU t)

-- | The "DataType" class.
class (Finite (DCU t), EqT (DCU t),
       DCs t ::: All (DCOf t), -- DCs t ::: All (AsRep GistD),
       Siblings t ::: TSum -- need GHC 7.2: , t ~ LeftmostRange (DCs 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.
  data DCU t :: * -> * -- universe of constructor types

  -- | /Disband/ this type into one of its data constructors.
  disband :: t -> Disbanded IdM t