packages feed

open-typerep 0.3.3 → 0.4

raw patch · 21 files changed

+1736/−496 lines, 21 filesdep +base-orphansdep +template-haskelldep ~syntactic

Dependencies added: base-orphans, template-haskell

Dependency ranges changed: syntactic

Files

benchmarks/Dynamic.hs view
@@ -5,6 +5,8 @@ import Data.Monoid  import Data.TypeRep+import Data.TypeRep.Types.Basic+import Data.TypeRep.Types.Basic.Typeable ()  import qualified Data.Dynamic as Base  -- For comparison
+ examples/Custom.hs view
@@ -0,0 +1,49 @@+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}++-- This file demonstrates how to create one's own type universe++module Custom where++++import Control.Monad++++import Language.Syntactic++import Data.TypeRep.Representation+import Data.TypeRep.TH++++-- Universe of types built using 'Bool', 'Int' and '[]'+data Type sig+  where+    Bool_t :: Type (Full Bool)+    Int_t  :: Type (Full Int)+    List_t :: Type (a :-> Full [a])++instance (Type :<: t) => Typeable t Bool where typeRep' = sugarSym Bool_t+instance (Type :<: t) => Typeable t Int  where typeRep' = sugarSym Int_t++instance (Type :<: t, Typeable t a) => Typeable t [a] where typeRep' = sugarSym List_t typeRep'++deriveRender_forType ''Type+deriveTypeEq ''Type+deriveWitness ''Eq ''Type+derivePWitness ''Eq ''Type+deriveWitness ''Show ''Type+derivePWitness ''Show ''Type+deriveWitnessTypeable ''Type++hlist :: [Dynamic Type]+hlist = [toDyn True, toDyn (1 :: Int), toDyn [1,2,3,4 :: Int]]++main = do+    unless test $ fail "Test failed"+    putStrLn "Test passed"+  where+    test = show hlist == "[True,1,[1,2,3,4]]"+
examples/Simple.hs view
@@ -1,30 +1,40 @@+module Simple where+++ import Control.Monad  import Data.TypeRep+import Data.TypeRep.Types.Basic+import Data.TypeRep.Types.Basic.Typeable () -type MyUniverse = IntType :+: BoolType ++-- A universe of three types+type MyUniverse = IntType :+: FloatType :+: BoolType++-- A list with dynamically typed elements hlist :: [Dynamic MyUniverse] hlist = [toDyn True, toDyn (1 :: Int)]-  -- Prints: [True,1] +-- Dynamically typed addition for any numeric type addDyn :: (TypeEq ts ts, PWitness Num ts ts) =>     Dynamic ts -> Dynamic ts -> Either String (Dynamic ts) addDyn (Dyn ta a) (Dyn tb b) = do-    Dict <- typeEq ta tb+    Dict <- typeEqM ta tb     Dict <- pwit pNum ta     return (Dyn ta (a+b)) ---test1 = toDyn (1 :: Int) `addDyn` toDyn (2 :: Int)-  -- Prints: Just 3+test2 = toDyn (1 :: Int)   `addDyn` toDyn (2 :: Int)+test3 = toDyn (3 :: Float) `addDyn` toDyn (4 :: Float)  main = do     unless t1 $ fail "Test 1 failed"     unless t2 $ fail "Test 2 failed"+    unless t3 $ fail "Test 3 failed"     putStrLn "All tests passed"   where     t1 = show hlist == "[True,1]"-    t2 = show (test1 :: Either String (Dynamic MyUniverse)) == "Right 3"+    t2 = show (test2 :: Either String (Dynamic MyUniverse)) == "Right 3"+    t3 = show (test3 :: Either String (Dynamic MyUniverse)) == "Right 7.0"
open-typerep.cabal view
@@ -1,5 +1,5 @@ name:                open-typerep-version:             0.3.3+version:             0.4 synopsis:            Open type representations and dynamic types description:         This package uses Data Types à la Carte to provide open type representations                      and dynamic types/coercions for open type universes.@@ -51,20 +51,34 @@   hs-source-dirs: src    exposed-modules:-    Data.TypeRep.Internal-    Data.TypeRep+    Data.TypeRep.Representation+    Data.TypeRep.TH+    Data.TypeRep.Types.Basic+    Data.TypeRep.Types.Basic.Typeable+    Data.TypeRep.Types.Tuple+    Data.TypeRep.Types.Tuple.Typeable+    Data.TypeRep.Types.IntWord+    Data.TypeRep.Types.IntWord.Typeable     Data.TypeRep.VarArg+    Data.TypeRep+    Language.Syntactic.TypeRep+    Language.Syntactic.TypeRep.Sugar.BindingTR+    Language.Syntactic.TypeRep.Sugar.TupleTR+    Language.Syntactic.TypeRep.TupleConversion    other-modules:     Data.TypeRep.Sub    build-depends:     base        >=4 && <5,+    base-orphans,+      -- Only needed for GHC < 7.10     constraints >=0.3,     mtl         >=2.2.1,       -- Smallest version that has Control.Monad.Except-    syntactic   >=3,-    tagged      >=0.4+    syntactic   >=3.2,+    tagged      >=0.4,+    template-haskell    default-language: Haskell2010 @@ -86,21 +100,25 @@ test-suite examples   type: exitcode-stdio-1.0 -  hs-source-dirs: examples+  hs-source-dirs: examples tests -  main-is: Simple.hs+  main-is: Tests.hs    default-language: Haskell2010    build-depends:+    base,     open-typerep,-    base+    syntactic    default-language: Haskell2010    default-extensions:     FlexibleContexts+    FlexibleInstances     GADTs+    MultiParamTypeClasses+    ScopedTypeVariables     TypeOperators  benchmark dynamic-bench
src/Data/TypeRep.hs view
@@ -10,6 +10,7 @@     , TypeRep     , typeRep     , TypeEq+    , typeEqM     , typeEq     , matchCon     , matchConM@@ -17,35 +18,24 @@     , PWitness     , wit     , pwit+    , witTypeable+    , pwitTypeable       -- * Dynamic types     , cast     , gcast     , Dynamic (..)     , toDyn     , fromDyn-    , dynToInteger-      -- * Type class witnessing+      -- * Misc.     , Any-    , witTypeable-    , pwitTypeable+    , ShowClass (..)     , pAny+    , pDataTypeable     , pEq     , pOrd     , pShow     , pNum     , pIntegral-    , BoolType-    , CharType-    , IntType-    , FloatType-    , ListType-    , FunType-    , boolType-    , charType-    , intType-    , floatType-    , listType-    , funType       -- * Sub-universes     , module Data.TypeRep.Sub     ) where@@ -57,6 +47,6 @@  import Language.Syntactic ((:+:), Project (..), (:<:) (..), E (..)) -import Data.TypeRep.Internal+import Data.TypeRep.Representation import Data.TypeRep.Sub
− src/Data/TypeRep/Internal.hs 
@@ -1,448 +0,0 @@-{-# LANGUAGE UndecidableInstances #-}---- | Open type representations and dynamic types--module Data.TypeRep.Internal where----import Control.Monad.Except-import Data.Char (isAlphaNum)--import Data.Constraint (Constraint, Dict (..))-import Data.Proxy (Proxy (..))--import Language.Syntactic----------------------------------------------------------------------------------------------------------- * Type representations--------------------------------------------------------------------------------------------------------- | 'Full'-indexed type representation-type TR = AST---- | This class provides reification of type @a@ in a universe @t@. @`Typeable` t a@ means that @a@--- is in the type universe represented by @t@.-class Typeable t a-  where-    typeRep' :: TR t (Full a)---- | Representation of type @a@ in a type universe @t@------ This type can also be seen as a witness that @a@ is a member of @t@ (i.e. @`Typeable` t a@); see--- 'witTypeable'.-newtype TypeRep t a = TypeRep { unTypeRep :: TR t (Full a) }-  -- The newtype is mainly because 'TR' cannot be partially applied--instance Render t => Show (TypeRep t a)-  where-    show = render . desugar--instance Syntactic (TypeRep t a)-  where-    type Domain (TypeRep t a)   = t-    type Internal (TypeRep t a) = a-    desugar = unTypeRep-    sugar   = TypeRep---- | Reification of type @a@ in a type universe @t@-typeRep :: Typeable t a => TypeRep t a-typeRep = TypeRep typeRep'---- | Equality on type representations-class Render t => TypeEq t u-  where-    typeEqSym-        :: (t sig1, Args (AST u) sig1)-        -> (t sig2, Args (AST u) sig2)-        -> Either String (Dict (DenResult sig1 ~ DenResult sig2))-  -- The reason to have `Render` as a super class is not to leak unnecessary stuff in the type of-  -- `typeEq`.--instance (TypeEq t1 t, TypeEq t2 t) => TypeEq (t1 :+: t2) t-  where-    typeEqSym (InjL t1, as1) (InjL t2, as2) = typeEqSym (t1,as1) (t2,as2)-    typeEqSym (InjR t1, as1) (InjR t2, as2) = typeEqSym (t1,as1) (t2,as2)-    typeEqSym _ _ = throwError ""--instance TypeEq Empty t-  where-    typeEqSym = error "typeEqSym: Empty"---- | Equality on type representations-typeEq :: (TypeEq t t, MonadError String m) => TypeRep t a -> TypeRep t b -> m (Dict (a ~ b))-typeEq t1@(TypeRep s1) t2@(TypeRep s2) = case go (s1, Nil) (s2, Nil) of-    Left _     -> throwError $ "type mismatch: " ++ show t1 ++ " /= " ++ show t2-    Right Dict -> return Dict-  where-    go :: TypeEq t t-      => (AST t sig1, Args (AST t) sig1)-      -> (AST t sig2, Args (AST t) sig2)-      -> Either String (Dict ((DenResult sig1 ~ DenResult sig2)))-    go (Sym t1, as1)   (Sym t2, as2)   = typeEqSym (t1,as1) (t2,as2)-    go (s1 :$ a1, as1) (s2 :$ a2, as2) = go (s1, a1 :* as1) (s2, a2 :* as2)-    go _ _ = throwError ""---- | Type constructor matching. This function makes it possible to match on type representations--- without dealing with the underlying 'AST' representation.------ For example, to check that a 'TypeRep' represents the type @a -> Int@ for some @a@:------ > is_atoi :: (TypeEq t t, IntType :<: t) => TypeRep t a -> Bool--- > is_atoi t--- >     | [E ta, E tb] <- matchCon t--- >     , Just _       <- typeEq ta intType = True--- >     | otherwise                         = False-matchCon :: TypeRep t c -> [E (TypeRep t)]-matchCon = simpleMatch (\_ -> foldrArgs (\t -> (E (TypeRep t) :)) []) . unTypeRep---- | Monadic version of 'matchCon'------ > matchConM = return . matchCon------ 'matchConM' is convenient when matching types in a monad, e.g.:------ > do ...--- >    [E ta, E tb] <- matchConM t--- >    Dict         <- typeEq ta tb--- >    ...-matchConM :: Monad m => TypeRep t c -> m [E (TypeRep t)]-matchConM = return . matchCon---- | Show the name of type classes-class ShowClass (p :: * -> Constraint)-  where-    -- | Show the name of a type class-    showClass :: Proxy p -> String---- | Witness a type constraint for a reified type-class Witness p t u-  where-    witSym :: t sig -> Args (AST u) sig -> Dict (p (DenResult sig))--instance (Witness p t1 t, Witness p t2 t) => Witness p (t1 :+: t2) t-  where-    witSym (InjL s) as = witSym s as-    witSym (InjR s) as = witSym s as--instance Witness p t t => Witness p (AST t) t-  where-    witSym (Sym s)  as = witSym s as-    witSym (s :$ a) as = witSym s (a :* as)---- | Partially witness a type constraint for a reified type-class (ShowClass p, Render t) => PWitness p t u-  where-    pwitSym :: t sig -> Args (AST u) sig -> Either String (Dict (p (DenResult sig)))-    pwitSym _ _ = throwError ""-  -- The reason to have `Render` as a super class is not to leak unnecessary stuff in the type of-  -- `pwit`.--instance (PWitness p t1 t, PWitness p t2 t) => PWitness p (t1 :+: t2) t-  where-    pwitSym (InjL s) as = pwitSym s as-    pwitSym (InjR s) as = pwitSym s as---- | Default implementation of 'pwitSym' for types that have a 'Witness' instance-pwitSymDefault :: Witness p t u =>-    t sig -> Args (AST u) sig -> Either String (Dict (p (DenResult sig)))-pwitSymDefault t = return . witSym t---- | Witness a type constraint for a reified type-wit :: forall p t a . Witness p t t => Proxy p -> TypeRep t a -> Dict (p a)-wit _ (TypeRep a) = witSym a (Nil :: Args (AST t) (Full a))---- | Partially witness a type constraint for a reified type-pwit :: forall p t m a . (PWitness p t t, MonadError String m) =>-    Proxy p -> TypeRep t a -> m (Dict (p a))-pwit p t@(TypeRep a) = case go a Nil of-    Left _  -> throwError $ unwords ["cannot deduce", showClass p, classArg]-    Right a -> return a-  where-    st       = show t-    classArg = if all isAlphaNum st then st else "(" ++ st ++ ")"--    go :: AST t sig -> Args (AST t) sig -> Either String (Dict (p (DenResult sig)))-    go (Sym s)  as = pwitSym s as-    go (s :$ a) as = go s (a :* as)----------------------------------------------------------------------------------------------------------- * Dynamic types--------------------------------------------------------------------------------------------------------- | Safe cast (does not use @unsafeCoerce@)-cast :: forall t a b . (Typeable t a, Typeable t b, TypeEq t t) =>-    Proxy t -> a -> Either String b-cast _ a = do-    Dict <- typeEq (typeRep :: TypeRep t a) (typeRep :: TypeRep t b)-    return a---- | Safe generalized cast (does not use @unsafeCoerce@)-gcast :: forall t a b c . (Typeable t a, Typeable t b, TypeEq t t) =>-    Proxy t -> c a -> Either String (c b)-gcast _ a = do-    Dict <- typeEq (typeRep :: TypeRep t a) (typeRep :: TypeRep t b)-    return a---- | Dynamic type parameterized on a type universe-data Dynamic t-  where-    Dyn :: TypeRep t a -> a -> Dynamic t--toDyn :: Typeable t a => a -> Dynamic t-toDyn = Dyn typeRep--fromDyn :: forall t a . (Typeable t a, TypeEq t t) => Dynamic t -> Either String a-fromDyn (Dyn t a) = do-    Dict <- typeEq t (typeRep :: TypeRep t a)-    return a--instance (TypeEq t t, Witness Eq t t) => Eq (Dynamic t)-  where-    Dyn ta a == Dyn tb b-        | Right Dict <- typeEq ta tb-        , Dict       <- wit pEq ta-        = a == b-    _ == _ = False--instance Witness Show t t => Show (Dynamic t)-  where-    show (Dyn t a) | Dict <- wit pShow t = show a----------------------------------------------------------------------------------------------------------- * Specific types/classes--------------------------------------------------------------------------------------------------------- | The universal class-class    Any a-instance Any a--instance ShowClass Any          where showClass _ = "Any"-instance ShowClass Eq           where showClass _ = "Eq"-instance ShowClass Ord          where showClass _ = "Ord"-instance ShowClass Show         where showClass _ = "Show"-instance ShowClass Num          where showClass _ = "Num"-instance ShowClass Integral     where showClass _ = "Integral"-instance ShowClass (Typeable t) where showClass _ = "Typeable ..."---- | Witness a 'Typeable' constraint for a reified type-witTypeable :: Witness (Typeable t) t t => TypeRep t a -> Dict (Typeable t a)-witTypeable = wit Proxy---- | Partially witness a 'Typeable' constraint for a reified type-pwitTypeable :: PWitness (Typeable t) t t => TypeRep t a -> Either String (Dict (Typeable t a))-pwitTypeable = pwit Proxy--pAny :: Proxy Any-pAny = Proxy--pEq :: Proxy Eq-pEq = Proxy--pOrd :: Proxy Ord-pOrd = Proxy--pShow :: Proxy Show-pShow = Proxy--pNum :: Proxy Num-pNum = Proxy--pIntegral :: Proxy Integral-pIntegral = Proxy--data BoolType  a where BoolType  :: BoolType  (Full Bool)-data CharType  a where CharType  :: CharType  (Full Char)-data IntType   a where IntType   :: IntType   (Full Int)-data FloatType a where FloatType :: FloatType (Full Float)-data ListType  a where ListType  :: ListType  (a :-> Full [a])-data FunType   a where FunType   :: FunType   (a :-> b :-> Full (a -> b))--instance Render BoolType  where renderSym BoolType  = "Bool"-instance Render CharType  where renderSym CharType  = "Char"-instance Render IntType   where renderSym IntType   = "Int"-instance Render FloatType where renderSym FloatType = "Float"--instance Render ListType-  where-    renderSym ListType = "[]"-    renderArgs [a] ListType = "[" ++ a ++ "]"--instance Render FunType-  where-    renderSym FunType = "(->)"-    renderArgs [a,b] FunType = a ++ " -> " ++ b--boolType :: (Syntactic a, BoolType :<: Domain a, Internal a ~ Bool) => a-boolType = sugarSym BoolType--charType :: (Syntactic a, CharType :<: Domain a, Internal a ~ Char) => a-charType = sugarSym CharType--intType :: (Syntactic a, IntType :<: Domain a, Internal a ~ Int) => a-intType = sugarSym IntType--floatType :: (Syntactic a, FloatType :<: Domain a, Internal a ~ Float) => a-floatType = sugarSym FloatType--listType-    :: ( Syntactic list-       , Syntactic elem-       , Domain list ~ Domain elem-       , ListType :<: Domain list-       , Internal list ~ [Internal elem]-       , elem ~ c e-       , list ~ c l-           -- These last equalities are used to help type inference by forcing the representations-           -- to use the same type constructor (e.g. 'TR' or 'TypeRep')-       )-    => elem -> list-listType = sugarSym ListType--funType-    :: ( Syntactic fun-       , Syntactic a-       , Syntactic b-       , Domain fun ~ Domain a-       , Domain fun ~ Domain b-       , FunType :<: Domain fun-       , Internal fun ~ (Internal a -> Internal b)-       , a   ~ c x-       , b   ~ c y-       , fun ~ c z-       )-    => a -> b -> fun-funType = sugarSym FunType--instance (BoolType  :<: t)                             => Typeable t Bool     where typeRep' = boolType-instance (CharType  :<: t)                             => Typeable t Char     where typeRep' = charType-instance (IntType   :<: t)                             => Typeable t Int      where typeRep' = intType-instance (FloatType :<: t)                             => Typeable t Float    where typeRep' = floatType-instance (ListType  :<: t, Typeable t a)               => Typeable t [a]      where typeRep' = listType typeRep'-instance (FunType   :<: t, Typeable t a, Typeable t b) => Typeable t (a -> b) where typeRep' = funType typeRep' typeRep'--instance TypeEq BoolType  t where typeEqSym (BoolType, Nil)  (BoolType, Nil)  = return Dict-instance TypeEq CharType  t where typeEqSym (CharType, Nil)  (CharType, Nil)  = return Dict-instance TypeEq IntType   t where typeEqSym (IntType, Nil)   (IntType, Nil)   = return Dict-instance TypeEq FloatType t where typeEqSym (FloatType, Nil) (FloatType, Nil) = return Dict--instance TypeEq t t => TypeEq ListType t-  where-    typeEqSym (ListType, a :* Nil) (ListType, b :* Nil) = do-        Dict <- typeEq (TypeRep a) (TypeRep b)-        return Dict--instance TypeEq t t => TypeEq FunType t-  where-    typeEqSym (FunType, a1 :* b1 :* Nil) (FunType, a2 :* b2 :* Nil) = do-        Dict <- typeEq (TypeRep a1) (TypeRep a2)-        Dict <- typeEq (TypeRep b1) (TypeRep b2)-        return Dict--instance (BoolType  :<: t) => Witness (Typeable t) BoolType  t where witSym BoolType  Nil = Dict-instance (CharType  :<: t) => Witness (Typeable t) CharType  t where witSym CharType  Nil = Dict-instance (IntType   :<: t) => Witness (Typeable t) IntType   t where witSym IntType   Nil = Dict-instance (FloatType :<: t) => Witness (Typeable t) FloatType t where witSym FloatType Nil = Dict--instance (ListType :<: t, Witness (Typeable t) t t) => Witness (Typeable t) ListType t-  where-    witSym ListType (a :* Nil)-        | Dict <- witTypeable (TypeRep a) = Dict--instance (FunType :<: t, Witness (Typeable t) t t) => Witness (Typeable t) FunType t-  where-    witSym FunType (a :* b :* Nil)-        | Dict <- witTypeable (TypeRep a)-        , Dict <- witTypeable (TypeRep b)-        = Dict--instance (BoolType  :<: t)                            => PWitness (Typeable t) BoolType  t where pwitSym = pwitSymDefault-instance (CharType  :<: t)                            => PWitness (Typeable t) CharType  t where pwitSym = pwitSymDefault-instance (IntType   :<: t)                            => PWitness (Typeable t) IntType   t where pwitSym = pwitSymDefault-instance (FloatType :<: t)                            => PWitness (Typeable t) FloatType t where pwitSym = pwitSymDefault-instance (ListType  :<: t, PWitness (Typeable t) t t) => PWitness (Typeable t) ListType  t where pwitSym ListType (a :* Nil) = do Dict <- pwitTypeable (TypeRep a); return Dict-instance (FunType   :<: t, PWitness (Typeable t) t t) => PWitness (Typeable t) FunType   t where pwitSym FunType (a :* b :* Nil) = do Dict <- pwitTypeable (TypeRep a); Dict <- pwitTypeable (TypeRep b); return Dict--instance Witness Any BoolType  t where witSym _ _ = Dict-instance Witness Any CharType  t where witSym _ _ = Dict-instance Witness Any IntType   t where witSym _ _ = Dict-instance Witness Any FloatType t where witSym _ _ = Dict-instance Witness Any ListType  t where witSym _ _ = Dict-instance Witness Any FunType   t where witSym _ _ = Dict--instance PWitness Any BoolType  t where pwitSym _ _ = return Dict-instance PWitness Any CharType  t where pwitSym _ _ = return Dict-instance PWitness Any IntType   t where pwitSym _ _ = return Dict-instance PWitness Any FloatType t where pwitSym _ _ = return Dict-instance PWitness Any ListType  t where pwitSym _ _ = return Dict-instance PWitness Any FunType   t where pwitSym _ _ = return Dict--instance                   Witness Eq BoolType  t where witSym BoolType  Nil = Dict-instance                   Witness Eq CharType  t where witSym CharType  Nil = Dict-instance                   Witness Eq IntType   t where witSym IntType   Nil = Dict-instance                   Witness Eq FloatType t where witSym FloatType Nil = Dict-instance Witness Eq t t => Witness Eq ListType  t where witSym ListType (a :* Nil) | Dict <- wit pEq (TypeRep a) = Dict--instance                    PWitness Eq BoolType  t where pwitSym = pwitSymDefault-instance                    PWitness Eq CharType  t where pwitSym = pwitSymDefault-instance                    PWitness Eq IntType   t where pwitSym = pwitSymDefault-instance                    PWitness Eq FloatType t where pwitSym = pwitSymDefault-instance PWitness Eq t t => PWitness Eq ListType  t where pwitSym ListType (a :* Nil) = do Dict <- pwit pEq (TypeRep a); return Dict-instance PWitness Eq FunType t--instance                    Witness Ord BoolType  t where witSym BoolType  Nil = Dict-instance                    Witness Ord CharType  t where witSym CharType  Nil = Dict-instance                    Witness Ord IntType   t where witSym IntType   Nil = Dict-instance                    Witness Ord FloatType t where witSym FloatType Nil = Dict-instance Witness Ord t t => Witness Ord ListType  t where witSym ListType (a :* Nil) | Dict <- wit pOrd (TypeRep a) = Dict--instance                     PWitness Ord BoolType  t where pwitSym = pwitSymDefault-instance                     PWitness Ord CharType  t where pwitSym = pwitSymDefault-instance                     PWitness Ord IntType   t where pwitSym = pwitSymDefault-instance                     PWitness Ord FloatType t where pwitSym = pwitSymDefault-instance PWitness Ord t t => PWitness Ord ListType  t where pwitSym ListType (a :* Nil) = do Dict <- pwit pOrd (TypeRep a); return Dict-instance PWitness Ord FunType t--instance                     Witness Show BoolType  t where witSym BoolType  Nil = Dict-instance                     Witness Show CharType  t where witSym CharType  Nil = Dict-instance                     Witness Show IntType   t where witSym IntType   Nil = Dict-instance                     Witness Show FloatType t where witSym FloatType Nil = Dict-instance Witness Show t t => Witness Show ListType  t where witSym ListType (a :* Nil) | Dict <- wit pShow (TypeRep a) = Dict--instance                      PWitness Show BoolType  t where pwitSym = pwitSymDefault-instance                      PWitness Show CharType  t where pwitSym = pwitSymDefault-instance                      PWitness Show IntType   t where pwitSym = pwitSymDefault-instance                      PWitness Show FloatType t where pwitSym = pwitSymDefault-instance PWitness Show t t => PWitness Show ListType  t where pwitSym ListType (a :* Nil) = do Dict <- pwit pShow (TypeRep a); return Dict-instance PWitness Show FunType t--instance Witness Num IntType   t where witSym IntType   Nil = Dict-instance Witness Num FloatType t where witSym FloatType Nil = Dict--instance PWitness Num BoolType  t-instance PWitness Num CharType  t-instance PWitness Num IntType   t where pwitSym = pwitSymDefault-instance PWitness Num FloatType t where pwitSym = pwitSymDefault-instance PWitness Num ListType  t-instance PWitness Num FunType   t--instance Witness Integral IntType t where witSym IntType Nil = Dict--instance PWitness Integral BoolType  t-instance PWitness Integral CharType  t-instance PWitness Integral IntType   t where pwitSym = pwitSymDefault-instance PWitness Integral FloatType t-instance PWitness Integral ListType  t-instance PWitness Integral FunType   t--dynToInteger :: PWitness Integral t t => Dynamic t -> Either String Integer-dynToInteger (Dyn tr a) = do-    Dict <- pwit pIntegral tr-    return (toInteger a)-
+ src/Data/TypeRep/Representation.hs view
@@ -0,0 +1,277 @@+{-# LANGUAGE UndecidableInstances #-}++-- | Open type representations and dynamic types++module Data.TypeRep.Representation where++++import Control.Monad.Except+import Data.Char (isAlphaNum)+import qualified Data.Typeable as Typeable++import Data.Constraint (Constraint, Dict (..))+import Data.Proxy (Proxy (..))++import Language.Syntactic++++----------------------------------------------------------------------------------------------------+-- * Type representations+----------------------------------------------------------------------------------------------------++-- | 'Full'-indexed type representation+type TR = AST++-- | This class provides reification of type @a@ in a universe @t@. @`Typeable` t a@ means that @a@+-- is in the type universe represented by @t@.+class Typeable t a+  where+    typeRep' :: TR t (Full a)++-- | Representation of type @a@ in a type universe @t@+--+-- This type can also be seen as a witness that @a@ is a member of @t@ (i.e. @`Typeable` t a@); see+-- 'witTypeable'.+newtype TypeRep t a = TypeRep { unTypeRep :: TR t (Full a) }+  -- The newtype is mainly because 'TR' cannot be partially applied++instance Render t => Show (TypeRep t a)+  where+    show = render . desugar++instance Syntactic (TypeRep t a)+  where+    type Domain (TypeRep t a)   = t+    type Internal (TypeRep t a) = a+    desugar = unTypeRep+    sugar   = TypeRep++-- | Reification of type @a@ in a type universe @t@+typeRep :: Typeable t a => TypeRep t a+typeRep = TypeRep typeRep'++-- | Equality on type representations+class Render t => TypeEq t u+  where+    typeEqSym+        :: (t sig1, Args (AST u) sig1)+        -> (t sig2, Args (AST u) sig2)+        -> Either String (Dict (DenResult sig1 ~ DenResult sig2))+  -- The reason to have `Render` as a super class is not to leak unnecessary stuff in the type of+  -- `typeEqM`/`typeEq`.++instance (TypeEq t1 t, TypeEq t2 t) => TypeEq (t1 :+: t2) t+  where+    typeEqSym (InjL t1, as1) (InjL t2, as2) = typeEqSym (t1,as1) (t2,as2)+    typeEqSym (InjR t1, as1) (InjR t2, as2) = typeEqSym (t1,as1) (t2,as2)+    typeEqSym (t1,_) (t2,_) = throwError ""++instance TypeEq Empty t+  where+    typeEqSym = error "typeEqSym: Empty"++-- | Equality on type representations+typeEqM :: (TypeEq t t, MonadError String m) => TypeRep t a -> TypeRep t b -> m (Dict (a ~ b))+typeEqM t1@(TypeRep s1) t2@(TypeRep s2) = case go (s1, Nil) (s2, Nil) of+    Left _     -> throwError $ "type mismatch: " ++ show t1 ++ " /= " ++ show t2+    Right Dict -> return Dict+  where+    go :: TypeEq t t+      => (AST t sig1, Args (AST t) sig1)+      -> (AST t sig2, Args (AST t) sig2)+      -> Either String (Dict ((DenResult sig1 ~ DenResult sig2)))+    go (Sym t1, as1)   (Sym t2, as2)   = typeEqSym (t1,as1) (t2,as2)+    go (s1 :$ a1, as1) (s2 :$ a2, as2) = go (s1, a1 :* as1) (s2, a2 :* as2)+    go _ _ = throwError ""++-- | Equality on type representations+typeEq :: TypeEq t t => TypeRep t a -> TypeRep t b -> Maybe (Dict (a ~ b))+typeEq t1 t2 = either (const Nothing) Just $ typeEqM t1 t2++-- | Type constructor matching. This function makes it possible to match on type representations+-- without dealing with the underlying 'AST' representation.+--+-- For example, to check that a 'TypeRep' represents the type @a -> Int@ for some @a@:+--+-- > is_atoi :: (TypeEq t t, IntType :<: t) => TypeRep t a -> Bool+-- > is_atoi t+-- >     | [E ta, E tb] <- matchCon t+-- >     , Just _       <- typeEq ta intType = True+-- >     | otherwise                         = False+matchCon :: TypeRep t c -> [E (TypeRep t)]+matchCon = simpleMatch (\_ -> foldrArgs (\t -> (E (TypeRep t) :)) []) . unTypeRep++-- | Monadic version of 'matchCon'+--+-- > matchConM = return . matchCon+--+-- 'matchConM' is convenient when matching types in a monad, e.g.:+--+-- > do ...+-- >    [E ta, E tb] <- matchConM t+-- >    Dict         <- typeEq ta tb+-- >    ...+matchConM :: Monad m => TypeRep t c -> m [E (TypeRep t)]+matchConM = return . matchCon++-- | Witness a type constraint for a reified type+class Witness p t u+  where+    witSym :: t sig -> Args (AST u) sig -> Dict (p (DenResult sig))++instance (Witness p t1 t, Witness p t2 t) => Witness p (t1 :+: t2) t+  where+    witSym (InjL s) as = witSym s as+    witSym (InjR s) as = witSym s as++instance Witness p t t => Witness p (AST t) t+  where+    witSym (Sym s)  as = witSym s as+    witSym (s :$ a) as = witSym s (a :* as)++-- | Partially witness a type constraint for a reified type+class (ShowClass p, Render t) => PWitness p t u+  where+    pwitSym :: t sig -> Args (AST u) sig -> Either String (Dict (p (DenResult sig)))+    pwitSym _ _ = throwError ""+  -- The reason to have `Render` as a super class is not to leak unnecessary stuff in the type of+  -- `pwit`.++instance (PWitness p t1 t, PWitness p t2 t) => PWitness p (t1 :+: t2) t+  where+    pwitSym (InjL s) as = pwitSym s as+    pwitSym (InjR s) as = pwitSym s as++-- | Default implementation of 'pwitSym' for types that have a 'Witness' instance+pwitSymDefault :: Witness p t u =>+    t sig -> Args (AST u) sig -> Either String (Dict (p (DenResult sig)))+pwitSymDefault t = return . witSym t++-- | Witness a type constraint for a reified type+wit :: forall p t a . Witness p t t => Proxy p -> TypeRep t a -> Dict (p a)+wit _ (TypeRep a) = witSym a (Nil :: Args (AST t) (Full a))++-- | Partially witness a type constraint for a reified type+pwit :: forall p t m a . (PWitness p t t, MonadError String m) =>+    Proxy p -> TypeRep t a -> m (Dict (p a))+pwit p t@(TypeRep a) = case go a Nil of+    Left _  -> throwError $ unwords ["cannot deduce", showClass p, classArg]+    Right a -> return a+  where+    st       = show t+    classArg = if all isAlphaNum st then st else "(" ++ st ++ ")"++    go :: AST t sig -> Args (AST t) sig -> Either String (Dict (p (DenResult sig)))+    go (Sym s)  as = pwitSym s as+    go (s :$ a) as = go s (a :* as)++-- | Witness a 'Typeable' constraint for a reified type+witTypeable :: Witness (Typeable t) t t => TypeRep t a -> Dict (Typeable t a)+witTypeable = wit Proxy++-- | Partially witness a 'Typeable' constraint for a reified type+pwitTypeable :: PWitness (Typeable t) t t =>+    TypeRep t a -> Either String (Dict (Typeable t a))+pwitTypeable = pwit Proxy++++----------------------------------------------------------------------------------------------------+-- * Dynamic types+----------------------------------------------------------------------------------------------------++-- | Safe cast (does not use @unsafeCoerce@)+cast :: forall t a b . (Typeable t a, Typeable t b, TypeEq t t) =>+    Proxy t -> a -> Either String b+cast _ a = do+    Dict <- typeEqM (typeRep :: TypeRep t a) (typeRep :: TypeRep t b)+    return a++-- | Safe generalized cast (does not use @unsafeCoerce@)+gcast :: forall t a b c . (Typeable t a, Typeable t b, TypeEq t t) =>+    Proxy t -> c a -> Either String (c b)+gcast _ a = do+    Dict <- typeEqM (typeRep :: TypeRep t a) (typeRep :: TypeRep t b)+    return a++-- | Dynamic type parameterized on a type universe+data Dynamic t+  where+    Dyn :: TypeRep t a -> a -> Dynamic t++toDyn :: Typeable t a => a -> Dynamic t+toDyn = Dyn typeRep++fromDyn :: forall t a . (Typeable t a, TypeEq t t) => Dynamic t -> Either String a+fromDyn (Dyn t a) = do+    Dict <- typeEqM t (typeRep :: TypeRep t a)+    return a++instance (TypeEq t t, Witness Eq t t) => Eq (Dynamic t)+  where+    Dyn ta a == Dyn tb b+        | Just Dict <- typeEq ta tb+        , Dict      <- wit (Proxy :: Proxy Eq) ta+        = a == b+    _ == _ = False++instance Witness Show t t => Show (Dynamic t)+  where+    show (Dyn t a) | Dict <- wit (Proxy :: Proxy Show) t = show a++++----------------------------------------------------------------------------------------------------+-- * Misc.+----------------------------------------------------------------------------------------------------++-- | The universal class+class    Any a+instance Any a++-- | Show the name of type classes+class ShowClass (p :: * -> Constraint)+  where+    -- | Show the name of a type class+    showClass :: Proxy p -> String++instance ShowClass Any               where showClass _ = "Any"+instance ShowClass Typeable.Typeable where showClass _ = "Data.Typeable"+instance ShowClass Eq                where showClass _ = "Eq"+instance ShowClass Ord               where showClass _ = "Ord"+instance ShowClass Show              where showClass _ = "Show"+instance ShowClass Num               where showClass _ = "Num"+instance ShowClass Integral          where showClass _ = "Integral"+instance ShowClass (Typeable t)      where showClass _ = "Typeable t"++-- | Proxy of 'Any' class. Can be passed to 'wit' and 'pwit'.+pAny :: Proxy Any+pAny = Proxy++-- | Proxy of 'Typeable.Typeable' class (from the base library). Can be passed+-- to 'wit' and 'pwit'.+pDataTypeable :: Proxy Typeable.Typeable+pDataTypeable = Proxy++-- | Proxy of 'Eq' class. Can be passed to 'wit' and 'pwit'.+pEq :: Proxy Eq+pEq = Proxy++-- | Proxy of 'Ord' class. Can be passed to 'wit' and 'pwit'.+pOrd :: Proxy Ord+pOrd = Proxy++-- | Proxy of 'Show' class. Can be passed to 'wit' and 'pwit'.+pShow :: Proxy Show+pShow = Proxy++-- | Proxy of 'Num' class. Can be passed to 'wit' and 'pwit'.+pNum :: Proxy Num+pNum = Proxy++-- | Proxy of 'Integral' class. Can be passed to 'wit' and 'pwit'.+pIntegral :: Proxy Integral+pIntegral = Proxy+
src/Data/TypeRep/Sub.hs view
@@ -15,13 +15,13 @@  module Data.TypeRep.Sub where --- TODO Merge this module with `Data.TypeRep.Internal` when support for < 7.10 is dropped+-- TODO Merge this module with `Data.TypeRep.Representation` when support for < 7.10 is dropped    import Language.Syntactic -import Data.TypeRep.Internal+import Data.TypeRep.Representation
+ src/Data/TypeRep/TH.hs view
@@ -0,0 +1,398 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE TemplateHaskell #-}++module Data.TypeRep.TH+  ( deriveRender_forType+  , deriveTypeEq+  , deriveWitness+  , derivePWitness+  , deriveWitnessAny+  , derivePWitnessAny+  , deriveWitnessTypeable+  , derivePWitnessTypeable+  ) where++++import Data.Proxy+import Language.Haskell.TH++import Control.Monad.Except+import Data.Constraint (Dict (..))++import Language.Syntactic+import Language.Syntactic.TH++import Data.TypeRep.Representation++++-- | Match on a 'Pred' of the form @(t1 ~ t2)@+viewEqPred :: Pred -> Maybe (Type,Type)+#if MIN_VERSION_template_haskell(2,10,0)+viewEqPred (AppT (AppT EqualityT t1) t2) = Just (t1,t2)+#else+viewEqPred (EqualP t1 t2) = Just (t1,t2)+#endif+viewEqPred _ = Nothing+  -- This function is just here to provide compatibility with+  -- template-haskell < 2.10++-- | Construct a 'Pred' of the form @(Cl t1 t2 ...)@+mkClassPred :: Name -> [Type] -> Pred+#if MIN_VERSION_template_haskell(2,10,0)+mkClassPred cl ts = foldl1 AppT (ConT cl : ts)+#else+mkClassPred cl ts = ClassP cl ts+#endif+  -- This function is just here to provide compatibility with+  -- template-haskell < 2.10++tyVarName :: TyVarBndr -> Name+tyVarName (PlainTV v)    = v  -- Only needed on GHC < 7.10+tyVarName (KindedTV v _) = v++++indent :: Int -> String -> String+indent n = unlines . map (replicate n ' ' ++) . lines++-- | Throw an error stating that the given type wasn't declared on the form+--+-- > data SymType sig where+-- >   ...+-- >   ThisSym :: SymType (a :-> ... :-> Full x)+-- >   ...+errorDerive+    :: String  -- ^ Function where error occurred+    -> Info    -- ^ Info about type+    -> a+errorDerive fun info = error $ unlines+    [ "------ " ++ fun ++ ": can only handle types declared on the form ----"+    , ""+    , "        data SymType sig where"+    , "          ..."+    , "          ThisSym :: SymType (a :-> ... :-> Full x)"+    , "          ..."+    , ""+    , "      ------ This is what I got: ------"+    , ""+    , indent 8 $ pprint info+    ]++-- | Get the arity of a symbol. If the type is not declared according to what+-- is stated for 'errorDerive', 'Nothing' is returned.+symArity+    :: Name  -- ^ Type parameter+    -> Con   -- ^ Symbol+    -> Maybe Int+symArity sigVar (ForallC _ [cxt] (NormalC _ []))+    | Just (VarT sigVar', sig) <- viewEqPred cxt+    , sigVar == sigVar'+    = count sig+  where+    count :: Type -> Maybe Int+    count (AppT (AppT arrow _) res)+        | arrow == ConT ''(:->) = fmap (+1) $ count res+    count (AppT (ConT full) _)+        | full == ''Full        = Just 0+    count _ = Nothing+symArity _ _ = Nothing++-- | Construct a pattern @v `:*` pat@+argConsP :: Name -> Pat -> Pat+argConsP v rest = InfixP (VarP v) '(:*) rest++-- | Construct a predicate proxy @`Proxy` :: `Proxy` Pred@+mkPredProxy :: Type -> Exp+mkPredProxy pred = SigE (ConE 'Proxy) (AppT (ConT ''Proxy) pred)++-- Generate an expression of the form+--+-- > case wit (Proxy :: Proxy Pred) (TypeRep v) of Dict -> result+--+-- The class is given as a 'Type' because+support+    :: Type  -- ^ Type predicate (e.g. 'Eq' or @(`Typeable` t)@)+    -> Name  -- ^ Variable for type representation+    -> Exp   -- ^ Result+    -> Exp+support pred v res = CaseE+    (foldl1 AppE [VarE 'wit, mkPredProxy pred, AppE (ConE 'TypeRep) (VarE v)])+    [Match (ConP 'Dict []) (NormalB res) []]++-- | A type variable named @t@+tVar :: Type+tVar = VarT $ mkName "t"++-- | "abc_dfg" -> "abc"+typeName :: String -> String+typeName = takeWhile (/='_')++++--------------------------------------------------------------------------------+-- * Derivers+--------------------------------------------------------------------------------++-- | A version of 'deriveRender' that applies 'typeName' to each constructor+-- name. That is, e.g. the constructor @Int_t :: IntType (Full Int)@ will be+-- rendered as \"Int\".+deriveRender_forType+    :: Name  -- ^ Type name+    -> DecsQ+deriveRender_forType = deriveRender typeName++-- | Derive 'TypeEq' instance for a type representation+deriveTypeEq+    :: Name  -- ^ Type name+    -> DecsQ+deriveTypeEq ty = do+    info <- reify ty+    case info of+        TyConI (DataD _ _ [sigVarTV] cs _) -> do+            throwErrExp <- [| throwError "" |]+              -- `typeEq` will turn this into a proper error message+            let sigVar = tyVarName sigVarTV+            let maxArity = case mapM (symArity sigVar) cs of+                  Just as -> maximum (0:as)+                  Nothing -> errorDerive "deriveTypeEq" info+            let classCxt = if maxArity == 0+                  then []+                  else [mkClassPred ''TypeEq [tVar, tVar]]+            let typeEqSymFallThrough = if length cs > 1+                  then [Clause [WildP, WildP] (NormalB throwErrExp) []]+                  else []+            let mkClause c i n a = case typeEqSymClause sigVar c i n a of+                  Just clause -> clause+                  Nothing -> errorDerive "deriveTypeEq" info+            deriveClass classCxt ty+                (foldl1 AppT [ConT ''TypeEq, ConT ty, tVar])+                [MatchingMethod 'typeEqSym mkClause typeEqSymFallThrough]+        _ -> errorDerive "deriveTypeEq" info+  where+    typeEqSymClause sigVar con _ name 0 = do+        arity <- symArity sigVar con+        let vs1    = take arity varSupply+            vs2    = take arity $ drop arity varSupply+            argsP1 = foldr argConsP (ConP 'Nil []) vs1+            argsP2 = foldr argConsP (ConP 'Nil []) vs2+            checkArgs v1 v2 = foldl1 AppE+                  [ VarE 'typeEqM+                  , AppE (ConE 'TypeRep) (VarE v1), AppE (ConE 'TypeRep) (VarE v2)+                  ]+              -- typeEq (TypeRep v1) (TypeRep v2)+            eqArgs  = [BindS (ConP 'Dict []) $ checkArgs v1 v2 | (v1,v2) <- zip vs1 vs2]+            retStmt = NoBindS $ AppE (VarE 'return) (ConE 'Dict)+        return $ Clause+          [ TupP [ConP name [], argsP1]+          , TupP [ConP name [], argsP2]+          ]+          (NormalB $ DoE (eqArgs ++ [retStmt]))+          []+    typeEqSymClause _ _ _ _ _ = Nothing++-- | Derive 'Witness' instance for a type representation+--+-- > instance Witness Cl t t => Witness Cl Ty t where+-- >   witSym Con1 Nil = Dict+-- >   witSym Con2 (a :* b :* Nil) =+-- >       case wit (Proxy :: Proxy Cl) (TypeRep a) of+-- >         Dict -> case wit (Proxy :: Proxy Cl) (TypeRep b) of+-- >           Dict -> Dict+deriveWitness+    :: Name  -- ^ Class name+    -> Name  -- ^ Type name+    -> DecsQ+deriveWitness cl ty = do+    info <- reify ty+    case info of+        TyConI (DataD _ _ [sigVarTV] cs _) -> do+            let sigVar = tyVarName sigVarTV+            let maxArity = case mapM (symArity sigVar) cs of+                  Just as -> maximum (0:as)+                  Nothing -> errorDerive "deriveWitness" info+            let classCxt = if maxArity == 0+                  then []+                  else [mkClassPred ''Witness [ConT cl, tVar, tVar]]+            let mkClause c i n a = case witSymClause sigVar c i n a of+                  Just clause -> clause+                  Nothing -> errorDerive "deriveWitness" info+            deriveClass classCxt ty+              (foldl1 AppT [ConT ''Witness, ConT cl, ConT ty, tVar])+              [MatchingMethod 'witSym mkClause []]+  where+    pred = ConT cl+    witSymClause sigVar con _ name 0 = do+        arity <- symArity sigVar con+        let vs    = take arity varSupply+            argsP = foldr argConsP (ConP 'Nil []) vs+        return $ Clause+          [ConP name [], argsP]+          (NormalB $ foldr (support pred) (ConE 'Dict) vs)+          []++-- | Derive 'PWitness' instance for a type representation+--+-- > instance PWitness Cl t t => PWitness Cl Ty t where+-- >   pwitSym Con1 Nil = return Dict+-- >   pwitSym Con2 (a :* b :* Nil) = do+-- >       Dict <- pwit (Proxy :: Proxy Cl) (TypeRep a)+-- >       Dict <- pwit (Proxy :: Proxy Cl) (TypeRep b)+-- >       return Dict+derivePWitness+    :: Name  -- ^ Class name+    -> Name  -- ^ Type name+    -> DecsQ+derivePWitness cl ty = do+    info <- reify ty+    case info of+        TyConI (DataD _ _ [sigVarTV] cs _) -> do+            let sigVar = tyVarName sigVarTV+            let maxArity = case mapM (symArity sigVar) cs of+                  Just as -> maximum (0:as)+                  Nothing -> errorDerive "derivePWitness" info+            let classCxt = if maxArity == 0+                  then []+                  else [mkClassPred ''PWitness [ConT cl, tVar, tVar]]+            let mkClause c i n a = case pwitSymClause sigVar c i n a of+                  Just clause -> clause+                  Nothing -> errorDerive "derivePWitness" info+            deriveClass classCxt ty+              (foldl1 AppT [ConT ''PWitness, ConT cl, ConT ty, tVar])+              [MatchingMethod 'pwitSym mkClause []]+  where+    pred = ConT cl+    pwitSymClause sigVar con _ name 0 = do+        arity <- symArity sigVar con+        let vs        = take arity varSupply+            argsP     = foldr argConsP (ConP 'Nil []) vs+            pwitArg v = foldl1 AppE [VarE 'pwit, mkPredProxy pred, AppE (ConE 'TypeRep) (VarE v)]+            pwitArgs  = [BindS (ConP 'Dict []) $ pwitArg v | v <- vs]+            retStmt   = NoBindS $ AppE (VarE 'return) (ConE 'Dict)+        return $ Clause+          [ConP name [], argsP]+          (NormalB $ DoE (pwitArgs ++ [retStmt]))+          []++-- | Derive @`Witness` `Any`@ instance for a type representation+--+-- > instance Witness Any Ty t where+-- >   witSym _ _ = Dict+-- >   witSym _ _ = Dict+deriveWitnessAny+    :: Name  -- ^ Type name+    -> DecsQ+deriveWitnessAny ty = do+    deriveClass [] ty+      (foldl1 AppT [ConT ''Witness, ConT ''Any, ConT ty, tVar])+      [MatchingMethod 'witSym witSymClause []]+  where+    witSymClause _ _ con 0 = Clause+        [WildP, WildP]+        (NormalB $ ConE 'Dict)+        []++-- | Derive @`PWitness` `Any`@ instance for a type representation+--+-- > instance PWitness Any Ty t where+-- >   pwitSym _ _ = return Dict+-- >   pwitSym _ _ = return Dict+derivePWitnessAny+    :: Name  -- ^ Type name+    -> DecsQ+derivePWitnessAny ty = do+    deriveClass [] ty+      (foldl1 AppT [ConT ''PWitness, ConT ''Any, ConT ty, tVar])+      [MatchingMethod 'pwitSym witSymClause []]+  where+    witSymClause _ _ con 0 = Clause+        [WildP, WildP]+        (NormalB $ AppE (VarE 'return) (ConE 'Dict))+        []++-- | Derive @`Witness` (`Typeable` Ty)@ instance for a type representation+--+-- > instance (Ty :<: t) => Witness (Typeable t) Ty t where+-- >   witSym Con1 Nil = Dict+-- >   witSym Con2 (a :* b :* Nil) =+-- >       case wit (Proxy :: Proxy (Typeable t)) (TypeRep a) of+-- >         Dict -> case wit (Proxy :: Proxy (Typeable t)) (TypeRep b) of+-- >           Dict -> Dict+deriveWitnessTypeable+    :: Name  -- ^ Type name+    -> DecsQ+deriveWitnessTypeable ty = do+    info <- reify ty+    case info of+        TyConI (DataD _ _ [sigVarTV] cs _) -> do+            let sigVar = tyVarName sigVarTV+            let maxArity = case mapM (symArity sigVar) cs of+                  Just as -> maximum (0:as)+                  Nothing -> errorDerive "deriveWitnessTypeable" info+            let sub = mkClassPred ''(:<:) [ConT ty, tVar]+            let classCxt = if maxArity == 0+                  then [sub]+                  else [sub, mkClassPred ''Witness [AppT (ConT cl) tVar, tVar, tVar]]+            let mkClause c i n a = case witSymClause sigVar c i n a of+                  Just clause -> clause+                  Nothing -> errorDerive "deriveWitnessTypeable" info+            deriveClass classCxt ty+              (foldl1 AppT [ConT ''Witness, AppT (ConT cl) tVar, ConT ty, tVar])+              [MatchingMethod 'witSym mkClause []]+  where+    cl   = ''Typeable+    pred = AppT (ConT cl) tVar+    witSymClause sigVar con _ name 0 = do+        arity <- symArity sigVar con+        let vs    = take arity varSupply+            argsP = foldr argConsP (ConP 'Nil []) vs+        return $ Clause+          [ConP name [], argsP]+          (NormalB $ foldr (support pred) (ConE 'Dict) vs)+          []++-- | Derive @`PWitness` (`Typeable` Ty)@ instance for a type representation+--+-- > instance (Ty :<: t) => PWitness (Typeable t) Ty t where+-- >   pwitSym Con1 Nil = return Dict+-- >   pwitSym Con2 (a :* b :* Nil) = do+-- >       Dict <- pwit (Proxy :: Proxy (Typeable t)) (TypeRep a)+-- >       Dict <- pwit (Proxy :: Proxy (Typeable t)) (TypeRep b)+-- >       return Dict+derivePWitnessTypeable+    :: Name  -- ^ Type name+    -> DecsQ+derivePWitnessTypeable ty = do+    info <- reify ty+    case info of+        TyConI (DataD _ _ [sigVarTV] cs _) -> do+            let sigVar = tyVarName sigVarTV+            let maxArity = case mapM (symArity sigVar) cs of+                  Just as -> maximum (0:as)+                  Nothing -> errorDerive "derivePWitnessTypeable" info+            let sub = mkClassPred ''(:<:) [ConT ty, tVar]+            let classCxt = if maxArity == 0+                  then [sub]+                  else [sub, mkClassPred ''PWitness [AppT (ConT cl) tVar, tVar, tVar]]+            let mkClause c i n a = case pwitSymClause sigVar c i n a of+                  Just clause -> clause+                  Nothing -> errorDerive "derivePWitnessTypeable" info+            deriveClass classCxt ty+              (foldl1 AppT [ConT ''PWitness, AppT (ConT cl) tVar, ConT ty, tVar])+              [MatchingMethod 'pwitSym mkClause []]+  where+    cl   = ''Typeable+    pred = AppT (ConT cl) tVar+    pwitSymClause sigVar con _ name 0 = do+        arity <- symArity sigVar con+        let vs        = take arity varSupply+            argsP     = foldr argConsP (ConP 'Nil []) vs+            pwitArg v = foldl1 AppE [VarE 'pwit, mkPredProxy pred, AppE (ConE 'TypeRep) (VarE v)]+            pwitArgs  = [BindS (ConP 'Dict []) $ pwitArg v | v <- vs]+            retStmt   = NoBindS $ AppE (VarE 'return) (ConE 'Dict)+        return $ Clause+          [ConP name [], argsP]+          (NormalB $ DoE (pwitArgs ++ [retStmt]))+          []+
+ src/Data/TypeRep/Types/Basic.hs view
@@ -0,0 +1,205 @@+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}++-- | Representations for specific types+--+-- The reason for using symbol names ending with @_t@ is that 'deriveRender'+-- uses everything that comes before @_@ when rendering the constructor.++module Data.TypeRep.Types.Basic where++++import qualified Data.Typeable as Typeable++import Language.Syntactic++import Data.TypeRep.Representation+import Data.TypeRep.TH++++data BoolType   a where Bool_t   :: BoolType   (Full Bool)+data CharType   a where Char_t   :: CharType   (Full Char)+data IntType    a where Int_t    :: IntType    (Full Int)+data FloatType  a where Float_t  :: FloatType  (Full Float)+data DoubleType a where Double_t :: DoubleType (Full Double)+data ListType   a where List_t   :: ListType (a :-> Full [a])+data FunType    a where Fun_t    :: FunType  (a :-> b :-> Full (a -> b))++boolType :: (Syntactic a, BoolType :<: Domain a, Internal a ~ Bool) => a+boolType = sugarSym Bool_t++charType :: (Syntactic a, CharType :<: Domain a, Internal a ~ Char) => a+charType = sugarSym Char_t++intType :: (Syntactic a, IntType :<: Domain a, Internal a ~ Int) => a+intType = sugarSym Int_t++floatType :: (Syntactic a, FloatType :<: Domain a, Internal a ~ Float) => a+floatType = sugarSym Float_t++doubleType :: (Syntactic a, DoubleType :<: Domain a, Internal a ~ Double) => a+doubleType = sugarSym Double_t++listType+    :: ( Syntactic list+       , Syntactic elem+       , Domain list ~ Domain elem+       , ListType :<: Domain list+       , Internal list ~ [Internal elem]+       , elem ~ c e+       , list ~ c l+           -- These last equalities are used to help type inference by forcing the representations+           -- to use the same type constructor (e.g. 'TR' or 'TypeRep')+       )+    => elem -> list+listType = sugarSym List_t++funType+    :: ( Syntactic fun+       , Syntactic a+       , Syntactic b+       , Domain fun ~ Domain a+       , Domain fun ~ Domain b+       , FunType :<: Domain fun+       , Internal fun ~ (Internal a -> Internal b)+       , a   ~ c x+       , b   ~ c y+       , fun ~ c z+       )+    => a -> b -> fun+funType = sugarSym Fun_t++deriveRender_forType ''BoolType+deriveRender_forType ''CharType+deriveRender_forType ''IntType+deriveRender_forType ''FloatType+deriveRender_forType ''DoubleType++instance Render ListType+  where+    renderSym List_t = "[]"+    renderArgs [a] List_t = "[" ++ a ++ "]"++instance Render FunType+  where+    renderSym Fun_t = "(->)"+    renderArgs = renderArgsSmart++deriveTypeEq ''BoolType+deriveTypeEq ''CharType+deriveTypeEq ''IntType+deriveTypeEq ''FloatType+deriveTypeEq ''DoubleType+deriveTypeEq ''ListType+deriveTypeEq ''FunType++deriveWitnessAny ''BoolType+deriveWitnessAny ''CharType+deriveWitnessAny ''IntType+deriveWitnessAny ''FloatType+deriveWitnessAny ''DoubleType+deriveWitnessAny ''ListType+deriveWitnessAny ''FunType++derivePWitnessAny ''BoolType+derivePWitnessAny ''CharType+derivePWitnessAny ''IntType+derivePWitnessAny ''FloatType+derivePWitnessAny ''DoubleType+derivePWitnessAny ''ListType+derivePWitnessAny ''FunType++deriveWitness ''Typeable.Typeable ''BoolType+deriveWitness ''Typeable.Typeable ''CharType+deriveWitness ''Typeable.Typeable ''IntType+deriveWitness ''Typeable.Typeable ''FloatType+deriveWitness ''Typeable.Typeable ''DoubleType+deriveWitness ''Typeable.Typeable ''ListType+deriveWitness ''Typeable.Typeable ''FunType++derivePWitness ''Typeable.Typeable ''BoolType+derivePWitness ''Typeable.Typeable ''CharType+derivePWitness ''Typeable.Typeable ''IntType+derivePWitness ''Typeable.Typeable ''FloatType+derivePWitness ''Typeable.Typeable ''DoubleType+derivePWitness ''Typeable.Typeable ''ListType+derivePWitness ''Typeable.Typeable ''FunType++deriveWitness ''Eq ''BoolType+deriveWitness ''Eq ''CharType+deriveWitness ''Eq ''IntType+deriveWitness ''Eq ''FloatType+deriveWitness ''Eq ''DoubleType+deriveWitness ''Eq ''ListType++derivePWitness ''Eq ''BoolType+derivePWitness ''Eq ''CharType+derivePWitness ''Eq ''IntType+derivePWitness ''Eq ''FloatType+derivePWitness ''Eq ''DoubleType+derivePWitness ''Eq ''ListType++deriveWitness ''Ord ''BoolType+deriveWitness ''Ord ''CharType+deriveWitness ''Ord ''IntType+deriveWitness ''Ord ''FloatType+deriveWitness ''Ord ''DoubleType+deriveWitness ''Ord ''ListType++derivePWitness ''Ord ''BoolType+derivePWitness ''Ord ''CharType+derivePWitness ''Ord ''IntType+derivePWitness ''Ord ''FloatType+derivePWitness ''Ord ''DoubleType+derivePWitness ''Ord ''ListType++deriveWitness ''Show ''BoolType+deriveWitness ''Show ''CharType+deriveWitness ''Show ''IntType+deriveWitness ''Show ''FloatType+deriveWitness ''Show ''DoubleType+deriveWitness ''Show ''ListType++derivePWitness ''Show ''BoolType+derivePWitness ''Show ''CharType+derivePWitness ''Show ''IntType+derivePWitness ''Show ''FloatType+derivePWitness ''Show ''DoubleType+derivePWitness ''Show ''ListType++deriveWitness ''Num ''IntType+deriveWitness ''Num ''FloatType+deriveWitness ''Num ''DoubleType++derivePWitness ''Num ''IntType+derivePWitness ''Num ''FloatType+derivePWitness ''Num ''DoubleType++deriveWitness ''Integral ''IntType++derivePWitness ''Integral ''IntType++++-- 'PWitness' instances for non-members++instance PWitness Eq FunType t++instance PWitness Ord FunType t++instance PWitness Show FunType t++instance PWitness Num BoolType   t+instance PWitness Num CharType   t+instance PWitness Num ListType   t+instance PWitness Num FunType    t++instance PWitness Integral BoolType   t+instance PWitness Integral CharType   t+instance PWitness Integral FloatType  t+instance PWitness Integral DoubleType t+instance PWitness Integral ListType   t+instance PWitness Integral FunType    t+
+ src/Data/TypeRep/Types/Basic/Typeable.hs view
@@ -0,0 +1,52 @@+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}++-- | 'Typeable' instances for various types. The reason for having these in a+-- separate module is that it might be desired to have these instances with+-- other type representations.+--+-- For example, instead of the instance+--+-- > (BoolType :<: t) => Typeable t Bool+--+-- one might want to have+--+-- > Typeable MyTypeRep Bool++module Data.TypeRep.Types.Basic.Typeable where++++import Language.Syntactic++import Data.TypeRep.Representation+import Data.TypeRep.TH+import Data.TypeRep.Types.Basic++++instance (BoolType   :<: t) => Typeable t Bool   where typeRep' = boolType+instance (CharType   :<: t) => Typeable t Char   where typeRep' = charType+instance (IntType    :<: t) => Typeable t Int    where typeRep' = intType+instance (FloatType  :<: t) => Typeable t Float  where typeRep' = floatType+instance (DoubleType :<: t) => Typeable t Double where typeRep' = doubleType++instance (ListType :<: t, Typeable t a)               => Typeable t [a]      where typeRep' = listType typeRep'+instance (FunType  :<: t, Typeable t a, Typeable t b) => Typeable t (a -> b) where typeRep' = funType typeRep' typeRep'++deriveWitnessTypeable ''BoolType+deriveWitnessTypeable ''CharType+deriveWitnessTypeable ''IntType+deriveWitnessTypeable ''FloatType+deriveWitnessTypeable ''DoubleType+deriveWitnessTypeable ''ListType+deriveWitnessTypeable ''FunType++derivePWitnessTypeable ''BoolType+derivePWitnessTypeable ''CharType+derivePWitnessTypeable ''IntType+derivePWitnessTypeable ''FloatType+derivePWitnessTypeable ''DoubleType+derivePWitnessTypeable ''ListType+derivePWitnessTypeable ''FunType+
+ src/Data/TypeRep/Types/IntWord.hs view
@@ -0,0 +1,76 @@+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}++-- | Representations for signed and unsigned integer types+--+-- The reason for using symbol names ending with @_t@ is that 'deriveRender'+-- uses everything that comes before @_@ when rendering the constructor.++module Data.TypeRep.Types.IntWord where++++import Data.Int+import qualified Data.Typeable as Typeable+import Data.Word++import Language.Syntactic++import Data.TypeRep.TH++++data IntWordType a+  where+    Int8_t   :: IntWordType (Full Int8)+    Int16_t  :: IntWordType (Full Int16)+    Int32_t  :: IntWordType (Full Int32)+    Int64_t  :: IntWordType (Full Int64)+    Word8_t  :: IntWordType (Full Word8)+    Word16_t :: IntWordType (Full Word16)+    Word32_t :: IntWordType (Full Word32)+    Word64_t :: IntWordType (Full Word64)++int8Type :: (Syntactic a, IntWordType :<: Domain a, Internal a ~ Int8) => a+int8Type = sugarSym Int8_t++int16Type :: (Syntactic a, IntWordType :<: Domain a, Internal a ~ Int16) => a+int16Type = sugarSym Int16_t++int32Type :: (Syntactic a, IntWordType :<: Domain a, Internal a ~ Int32) => a+int32Type = sugarSym Int32_t++int64Type :: (Syntactic a, IntWordType :<: Domain a, Internal a ~ Int64) => a+int64Type = sugarSym Int64_t++word8Type :: (Syntactic a, IntWordType :<: Domain a, Internal a ~ Word8) => a+word8Type = sugarSym Word8_t++word16Type :: (Syntactic a, IntWordType :<: Domain a, Internal a ~ Word16) => a+word16Type = sugarSym Word16_t++word32Type :: (Syntactic a, IntWordType :<: Domain a, Internal a ~ Word32) => a+word32Type = sugarSym Word32_t++word64Type :: (Syntactic a, IntWordType :<: Domain a, Internal a ~ Word64) => a+word64Type = sugarSym Word64_t++deriveRender_forType ''IntWordType+deriveTypeEq         ''IntWordType+deriveWitnessAny     ''IntWordType+derivePWitnessAny    ''IntWordType++deriveWitness ''Typeable.Typeable ''IntWordType+deriveWitness ''Eq       ''IntWordType+deriveWitness ''Ord      ''IntWordType+deriveWitness ''Show     ''IntWordType+deriveWitness ''Num      ''IntWordType+deriveWitness ''Integral ''IntWordType++derivePWitness ''Typeable.Typeable ''IntWordType+derivePWitness ''Eq       ''IntWordType+derivePWitness ''Ord      ''IntWordType+derivePWitness ''Show     ''IntWordType+derivePWitness ''Num      ''IntWordType+derivePWitness ''Integral ''IntWordType+
+ src/Data/TypeRep/Types/IntWord/Typeable.hs view
@@ -0,0 +1,42 @@+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}++-- | 'Typeable' instances for signed and unsigned integer types. The reason for+-- having these in a separate module is that it might be desired to have these+-- instances with other type representations.+--+-- For example, instead of the instance+--+-- > (IntWordType :<: t) => Typeable t Int8+--+-- one might want to have+--+-- > Typeable MyTypeRep Int8++module Data.TypeRep.Types.IntWord.Typeable where++++import Data.Int+import Data.Word++import Language.Syntactic++import Data.TypeRep.Representation+import Data.TypeRep.TH+import Data.TypeRep.Types.IntWord++++instance (IntWordType :<: t) => Typeable t Int8   where typeRep' = int8Type+instance (IntWordType :<: t) => Typeable t Int16  where typeRep' = int16Type+instance (IntWordType :<: t) => Typeable t Int32  where typeRep' = int32Type+instance (IntWordType :<: t) => Typeable t Int64  where typeRep' = int64Type+instance (IntWordType :<: t) => Typeable t Word8  where typeRep' = word8Type+instance (IntWordType :<: t) => Typeable t Word16 where typeRep' = word16Type+instance (IntWordType :<: t) => Typeable t Word32 where typeRep' = word32Type+instance (IntWordType :<: t) => Typeable t Word64 where typeRep' = word64Type++deriveWitnessTypeable  ''IntWordType+derivePWitnessTypeable ''IntWordType+
+ src/Data/TypeRep/Types/Tuple.hs view
@@ -0,0 +1,163 @@+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}++-- | Representations for tuple types+--+-- The reason for using symbol names ending with @_t@ is that 'deriveRender'+-- uses everything that comes before @_@ when rendering the constructor.++module Data.TypeRep.Types.Tuple where++++import Data.List (intercalate)+import qualified Data.Typeable as Typeable++import Data.Orphans ()++import Language.Syntactic++import Data.TypeRep.Representation+import Data.TypeRep.TH++++data TupleType a+  where+    Tup2_t  :: TupleType (a :-> b :-> Full (a,b))+    Tup3_t  :: TupleType (a :-> b :-> c :-> Full (a,b,c))+    Tup4_t  :: TupleType (a :-> b :-> c :-> d :-> Full (a,b,c,d))+    Tup5_t  :: TupleType (a :-> b :-> c :-> d :-> e :-> Full (a,b,c,d,e))+    Tup6_t  :: TupleType (a :-> b :-> c :-> d :-> e :-> f :-> Full (a,b,c,d,e,f))+    Tup7_t  :: TupleType (a :-> b :-> c :-> d :-> e :-> f :-> g :-> Full (a,b,c,d,e,f,g))+    Tup8_t  :: TupleType (a :-> b :-> c :-> d :-> e :-> f :-> g :-> h :-> Full (a,b,c,d,e,f,g,h))+    Tup9_t  :: TupleType (a :-> b :-> c :-> d :-> e :-> f :-> g :-> h :-> i :-> Full (a,b,c,d,e,f,g,h,i))+    Tup10_t :: TupleType (a :-> b :-> c :-> d :-> e :-> f :-> g :-> h :-> i :-> j :-> Full (a,b,c,d,e,f,g,h,i,j))+    Tup11_t :: TupleType (a :-> b :-> c :-> d :-> e :-> f :-> g :-> h :-> i :-> j :-> k :-> Full (a,b,c,d,e,f,g,h,i,j,k))+    Tup12_t :: TupleType (a :-> b :-> c :-> d :-> e :-> f :-> g :-> h :-> i :-> j :-> k :-> l :-> Full (a,b,c,d,e,f,g,h,i,j,k,l))+    Tup13_t :: TupleType (a :-> b :-> c :-> d :-> e :-> f :-> g :-> h :-> i :-> j :-> k :-> l :-> m :-> Full (a,b,c,d,e,f,g,h,i,j,k,l,m))+    Tup14_t :: TupleType (a :-> b :-> c :-> d :-> e :-> f :-> g :-> h :-> i :-> j :-> k :-> l :-> m :-> n :-> Full (a,b,c,d,e,f,g,h,i,j,k,l,m,n))+    Tup15_t :: TupleType (a :-> b :-> c :-> d :-> e :-> f :-> g :-> h :-> i :-> j :-> k :-> l :-> m :-> n :-> o :-> Full (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o))++++-- The smart constructors are not overloaded using `Syntactic` as this would+-- lead to gigantic type signatures.++tup2Type :: (TupleType :<: t)+    => TypeRep t a -> TypeRep t b -> TypeRep t (a,b)+tup2Type = sugarSym Tup2_t++tup3Type :: (TupleType :<: t)+    => TypeRep t a -> TypeRep t b -> TypeRep t c -> TypeRep t (a,b,c)+tup3Type = sugarSym Tup3_t++tup4Type :: (TupleType :<: t)+    => TypeRep t a -> TypeRep t b -> TypeRep t c -> TypeRep t d -> TypeRep t (a,b,c,d)+tup4Type = sugarSym Tup4_t++tup5Type :: (TupleType :<: t)+    => TypeRep t a -> TypeRep t b -> TypeRep t c -> TypeRep t d -> TypeRep t e+    -> TypeRep t (a,b,c,d,e)+tup5Type = sugarSym Tup5_t++tup6Type :: (TupleType :<: t)+    => TypeRep t a -> TypeRep t b -> TypeRep t c -> TypeRep t d -> TypeRep t e+    -> TypeRep t f-> TypeRep t (a,b,c,d,e,f)+tup6Type = sugarSym Tup6_t++tup7Type :: (TupleType :<: t)+    => TypeRep t a -> TypeRep t b -> TypeRep t c -> TypeRep t d -> TypeRep t e+    -> TypeRep t f -> TypeRep t g -> TypeRep t (a,b,c,d,e,f,g)+tup7Type = sugarSym Tup7_t++tup8Type :: (TupleType :<: t)+    => TypeRep t a -> TypeRep t b -> TypeRep t c -> TypeRep t d -> TypeRep t e+    -> TypeRep t f -> TypeRep t g -> TypeRep t h -> TypeRep t (a,b,c,d,e,f,g,h)+tup8Type = sugarSym Tup8_t++tup9Type :: (TupleType :<: t)+    => TypeRep t a -> TypeRep t b -> TypeRep t c -> TypeRep t d -> TypeRep t e+    -> TypeRep t f -> TypeRep t g -> TypeRep t h -> TypeRep t i -> TypeRep t (a,b,c,d,e,f,g,h,i)+tup9Type = sugarSym Tup9_t++tup10Type :: (TupleType :<: t)+    => TypeRep t a -> TypeRep t b -> TypeRep t c -> TypeRep t d -> TypeRep t e+    -> TypeRep t f -> TypeRep t g -> TypeRep t h -> TypeRep t i -> TypeRep t j+    -> TypeRep t (a,b,c,d,e,f,g,h,i,j)+tup10Type = sugarSym Tup10_t++tup11Type :: (TupleType :<: t)+    => TypeRep t a -> TypeRep t b -> TypeRep t c -> TypeRep t d -> TypeRep t e+    -> TypeRep t f -> TypeRep t g -> TypeRep t h -> TypeRep t i -> TypeRep t j+    -> TypeRep t k -> TypeRep t (a,b,c,d,e,f,g,h,i,j,k)+tup11Type = sugarSym Tup11_t++tup12Type :: (TupleType :<: t)+    => TypeRep t a -> TypeRep t b -> TypeRep t c -> TypeRep t d -> TypeRep t e+    -> TypeRep t f -> TypeRep t g -> TypeRep t h -> TypeRep t i -> TypeRep t j+    -> TypeRep t k -> TypeRep t l -> TypeRep t (a,b,c,d,e,f,g,h,i,j,k,l)+tup12Type = sugarSym Tup12_t++tup13Type :: (TupleType :<: t)+    => TypeRep t a -> TypeRep t b -> TypeRep t c -> TypeRep t d -> TypeRep t e+    -> TypeRep t f -> TypeRep t g -> TypeRep t h -> TypeRep t i -> TypeRep t j+    -> TypeRep t k -> TypeRep t l -> TypeRep t m -> TypeRep t (a,b,c,d,e,f,g,h,i,j,k,l,m)+tup13Type = sugarSym Tup13_t++tup14Type :: (TupleType :<: t)+    => TypeRep t a -> TypeRep t b -> TypeRep t c -> TypeRep t d -> TypeRep t e+    -> TypeRep t f -> TypeRep t g -> TypeRep t h -> TypeRep t i -> TypeRep t j+    -> TypeRep t k -> TypeRep t l -> TypeRep t m -> TypeRep t n+    -> TypeRep t (a,b,c,d,e,f,g,h,i,j,k,l,m,n)+tup14Type = sugarSym Tup14_t++tup15Type :: (TupleType :<: t)+    => TypeRep t a -> TypeRep t b -> TypeRep t c -> TypeRep t d -> TypeRep t e+    -> TypeRep t f -> TypeRep t g -> TypeRep t h -> TypeRep t i -> TypeRep t j+    -> TypeRep t k -> TypeRep t l -> TypeRep t m -> TypeRep t n+    -> TypeRep t o -> TypeRep t (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o)+tup15Type = sugarSym Tup15_t++tupWidth :: TupleType a -> Int+tupWidth Tup2_t  = 2+tupWidth Tup3_t  = 3+tupWidth Tup4_t  = 4+tupWidth Tup5_t  = 5+tupWidth Tup6_t  = 6+tupWidth Tup7_t  = 7+tupWidth Tup8_t  = 8+tupWidth Tup9_t  = 9+tupWidth Tup10_t = 10+tupWidth Tup11_t = 11+tupWidth Tup12_t = 12+tupWidth Tup13_t = 13+tupWidth Tup14_t = 14+tupWidth Tup15_t = 15++instance Render TupleType+  where+    renderSym tup   = "(" ++ replicate (tupWidth tup - 1) ',' ++ ")"+    renderArgs as _ = "(" ++ intercalate "," as ++ ")"++deriveTypeEq ''TupleType++deriveWitnessAny ''TupleType++deriveWitness ''Typeable.Typeable ''TupleType++deriveWitness ''Eq   ''TupleType+deriveWitness ''Ord  ''TupleType+deriveWitness ''Show ''TupleType++derivePWitnessAny ''TupleType++derivePWitness ''Typeable.Typeable ''TupleType++derivePWitness ''Eq   ''TupleType+derivePWitness ''Ord  ''TupleType+derivePWitness ''Show ''TupleType++instance PWitness Num TupleType t+instance PWitness Integral TupleType t+
+ src/Data/TypeRep/Types/Tuple/Typeable.hs view
@@ -0,0 +1,86 @@+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}++-- | 'Typeable' instances for tuple types. The reason for having these in a+-- separate module is that it might be desired to have these instances with+-- other type representations.+--+-- For example, instead of the instance+--+-- > (BoolType :<: t) => Typeable t Bool+--+-- one might want to have+--+-- > Typeable MyTypeRep Bool++module Data.TypeRep.Types.Tuple.Typeable where++++import Language.Syntactic++import Data.TypeRep.Representation+import Data.TypeRep.TH+import Data.TypeRep.Types.Tuple++++instance (TupleType :<: t, Typeable t a, Typeable t b) =>+    Typeable t (a,b)+  where typeRep' = sugarSym Tup2_t typeRep' typeRep'++instance (TupleType :<: t, Typeable t a, Typeable t b, Typeable t c) =>+    Typeable t (a,b,c)+  where typeRep' = sugarSym Tup3_t typeRep' typeRep' typeRep'++instance (TupleType :<: t, Typeable t a, Typeable t b, Typeable t c, Typeable t d) =>+    Typeable t (a,b,c,d)+  where typeRep' = sugarSym Tup4_t typeRep' typeRep' typeRep' typeRep'++instance (TupleType :<: t, Typeable t a, Typeable t b, Typeable t c, Typeable t d, Typeable t e) =>+    Typeable t (a,b,c,d,e)+  where typeRep' = sugarSym Tup5_t typeRep' typeRep' typeRep' typeRep' typeRep'++instance (TupleType :<: t, Typeable t a, Typeable t b, Typeable t c, Typeable t d, Typeable t e, Typeable t f) =>+    Typeable t (a,b,c,d,e,f)+  where typeRep' = sugarSym Tup6_t typeRep' typeRep' typeRep' typeRep' typeRep' typeRep'++instance (TupleType :<: t, Typeable t a, Typeable t b, Typeable t c, Typeable t d, Typeable t e, Typeable t f, Typeable t g) =>+    Typeable t (a,b,c,d,e,f,g)+  where typeRep' = sugarSym Tup7_t typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep'++instance (TupleType :<: t, Typeable t a, Typeable t b, Typeable t c, Typeable t d, Typeable t e, Typeable t f, Typeable t g, Typeable t h) =>+    Typeable t (a,b,c,d,e,f,g,h)+  where typeRep' = sugarSym Tup8_t typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep'++instance (TupleType :<: t, Typeable t a, Typeable t b, Typeable t c, Typeable t d, Typeable t e, Typeable t f, Typeable t g, Typeable t h, Typeable t i) =>+    Typeable t (a,b,c,d,e,f,g,h,i)+  where typeRep' = sugarSym Tup9_t typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep'++instance (TupleType :<: t, Typeable t a, Typeable t b, Typeable t c, Typeable t d, Typeable t e, Typeable t f, Typeable t g, Typeable t h, Typeable t i, Typeable t j) =>+    Typeable t (a,b,c,d,e,f,g,h,i,j)+  where typeRep' = sugarSym Tup10_t typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep'++instance (TupleType :<: t, Typeable t a, Typeable t b, Typeable t c, Typeable t d, Typeable t e, Typeable t f, Typeable t g, Typeable t h, Typeable t i, Typeable t j, Typeable t k) =>+    Typeable t (a,b,c,d,e,f,g,h,i,j,k)+  where typeRep' = sugarSym Tup11_t typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep'++instance (TupleType :<: t, Typeable t a, Typeable t b, Typeable t c, Typeable t d, Typeable t e, Typeable t f, Typeable t g, Typeable t h, Typeable t i, Typeable t j, Typeable t k, Typeable t l) =>+    Typeable t (a,b,c,d,e,f,g,h,i,j,k,l)+  where typeRep' = sugarSym Tup12_t typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep'++instance (TupleType :<: t, Typeable t a, Typeable t b, Typeable t c, Typeable t d, Typeable t e, Typeable t f, Typeable t g, Typeable t h, Typeable t i, Typeable t j, Typeable t k, Typeable t l, Typeable t m) =>+    Typeable t (a,b,c,d,e,f,g,h,i,j,k,l,m)+  where typeRep' = sugarSym Tup13_t typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep'++instance (TupleType :<: t, Typeable t a, Typeable t b, Typeable t c, Typeable t d, Typeable t e, Typeable t f, Typeable t g, Typeable t h, Typeable t i, Typeable t j, Typeable t k, Typeable t l, Typeable t m, Typeable t n) =>+    Typeable t (a,b,c,d,e,f,g,h,i,j,k,l,m,n)+  where typeRep' = sugarSym Tup14_t typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep'++instance (TupleType :<: t, Typeable t a, Typeable t b, Typeable t c, Typeable t d, Typeable t e, Typeable t f, Typeable t g, Typeable t h, Typeable t i, Typeable t j, Typeable t k, Typeable t l, Typeable t m, Typeable t n, Typeable t o) =>+    Typeable t (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o)+  where typeRep' = sugarSym Tup15_t typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep' typeRep'++deriveWitnessTypeable ''TupleType+derivePWitnessTypeable ''TupleType+
src/Data/TypeRep/VarArg.hs view
@@ -8,7 +8,8 @@  import Language.Syntactic import Data.TypeRep-import Data.TypeRep.Internal+import Data.TypeRep.Representation+import Data.TypeRep.Types.Basic   @@ -54,33 +55,33 @@  instance VarArg BoolType   where-    aritySym BoolType Nil      = FunRes-    fromResInvSym BoolType Nil = Dict+    aritySym Bool_t Nil      = FunRes+    fromResInvSym Bool_t Nil = Dict  instance VarArg CharType   where-    aritySym CharType Nil      = FunRes-    fromResInvSym CharType Nil = Dict+    aritySym Char_t Nil      = FunRes+    fromResInvSym Char_t Nil = Dict  instance VarArg IntType   where-    aritySym IntType Nil      = FunRes-    fromResInvSym IntType Nil = Dict+    aritySym Int_t Nil      = FunRes+    fromResInvSym Int_t Nil = Dict  instance VarArg FloatType   where-    aritySym FloatType Nil      = FunRes-    fromResInvSym FloatType Nil = Dict+    aritySym Float_t Nil      = FunRes+    fromResInvSym Float_t Nil = Dict  instance VarArg ListType   where-    aritySym ListType _      = FunRes-    fromResInvSym ListType _ = Dict+    aritySym List_t _      = FunRes+    fromResInvSym List_t _ = Dict  instance VarArg FunType   where-    aritySym FunType (_ :* b :* Nil) = FunArg $ arity $ TypeRep b-    fromResInvSym FunType (_ :* b :* Nil)+    aritySym Fun_t (_ :* b :* Nil) = FunArg $ arity $ TypeRep b+    fromResInvSym Fun_t (_ :* b :* Nil)         | Dict <- fromResInv $ TypeRep b = Dict  -- | Get the 'Arity' of a type. The purpose is to be able to distinguish between functions and
+ src/Language/Syntactic/TypeRep.hs view
@@ -0,0 +1,94 @@+-- | Utilities for working with ASTs of the form @`AST` (sym `:&:` `TypeRep` t)@++module Language.Syntactic.TypeRep where++++import qualified Data.Typeable as Typeable++import Language.Syntactic+import Language.Syntactic.Functional+import Language.Syntactic.Functional.Sharing++import Data.TypeRep+import Data.TypeRep.Types.Basic++++mkVarSym :: Witness Typeable.Typeable t t =>+    TypeRep t a -> Name -> BindingT (Full a)+mkVarSym t v | Dict <- wit pDataTypeable t = VarT v++mkLamSym :: Witness Typeable.Typeable t t+    => TypeRep t a -> TypeRep t b -> Name+    -> BindingT (b :-> Full (a -> b))+mkLamSym ta _ v | Dict <- wit pDataTypeable ta = LamT v++-- | Inject a symbol in an 'AST' with a domain decorated by a type+-- representation+injTR :: (sub :<: sup, Typeable t (DenResult sig)) =>+    sub sig -> AST (sup :&: TypeRep t) sig+injTR s = Sym (inj s :&: typeRep)++-- | Make a smart constructor of a symbol. 'smartSymT' has any type of the form:+--+-- > smartSymTR :: (sub :<: AST (sup :&: TypeRep t), Typeable t x)+-- >     => sub (a :-> b :-> ... :-> Full x)+-- >     -> (ASTF sup a -> ASTF sup b -> ... -> ASTF sup x)+smartSymTR+    :: ( Signature sig+       , supT ~ (sup :&: TypeRep t)+       , f    ~ SmartFun supT sig+       , sig  ~ SmartSig f+       , supT ~ SmartSym f+       , sub :<: sup+       , Typeable t (DenResult sig)+       )+    => sub sig -> f+smartSymTR s = smartSym' (inj s :&: typeRep)++-- | \"Sugared\" symbol application+--+-- 'sugarSymTR' has any type of the form:+--+-- > sugarSymTR ::+-- >     ( sub :<: AST (sup :&: TypeRep t)+-- >     , Syntactic a+-- >     , Syntactic b+-- >     , ...+-- >     , Syntactic x+-- >     , Domain a ~ Domain b ~ ... ~ Domain x+-- >     , Typeable t (Internal x)+-- >     ) => sub (Internal a :-> Internal b :-> ... :-> Full (Internal x))+-- >       -> (a -> b -> ... -> x)+sugarSymTR+    :: ( Signature sig+       , supT ~ (sup :&: TypeRep t)+       , fi   ~ SmartFun supT sig+       , sig  ~ SmartSig fi+       , supT ~ SmartSym fi+       , SyntacticN f fi+       , sub :<: sup+       , Typeable t (DenResult sig)+       )+    => sub sig -> f+sugarSymTR = sugarN . smartSymTR++-- | Default 'CodeMotionInterface' for domains of the form+-- @((... `:+:` `BindingT` `:+:` ... ) `:&:` `TypeRep` t)@+defaultInterfaceTypeRep :: forall binding sym symT t+    .  ( BindingT :<: sym+       , Let      :<: sym+       , symT ~ (sym :&: TypeRep t)+       , FunType :<: t+       , TypeEq t t+       , Witness Typeable.Typeable t t+       )+    => (forall a b . ASTF symT a -> ASTF symT b -> Bool)+         -- ^ Can the expression represented by the first argument be shared in+         -- the second argument?+    -> (forall a . ASTF symT a -> Bool)+         -- ^ Can we hoist over this expression?+    -> CodeMotionInterface symT+defaultInterfaceTypeRep = defaultInterfaceDecor typeEq funType mkVarSym mkLamSym+
+ src/Language/Syntactic/TypeRep/Sugar/BindingTR.hs view
@@ -0,0 +1,53 @@+{-# LANGUAGE UndecidableInstances #-}++-- | 'Syntactic' instance for functions+--+-- This module is based on domains of the form+-- @((... `:+:` `BindingT` `:+:` ... ) `:&:` `TypeRep` t)@++module Language.Syntactic.TypeRep.Sugar.BindingTR where++++import qualified Data.Typeable as Typeable++import Language.Syntactic+import Language.Syntactic.Functional++import Data.TypeRep+import Data.TypeRep.Types.Basic+import Language.Syntactic.TypeRep++++instance+    ( sym ~ (s :&: TypeRep t)+    , Syntactic a, Domain a ~ sym+    , Syntactic b, Domain b ~ sym+    , BindingT :<: s+    , Typeable t (Internal a)+    , Typeable t (Internal b)+    , Witness Typeable.Typeable t t+    , FunType :<: t+    ) =>+      Syntactic (a -> b)+  where+    type Domain (a -> b)   = Domain a+    type Internal (a -> b) = Internal a -> Internal b++    desugar f = lamT_template mkVar mkLam (desugar . f . sugar)+      where+        ta :: TypeRep t (Internal a)+        ta = typeRep++        tb :: TypeRep t (Internal b)+        tb = typeRep++        mkVar :: Name -> sym (Full (Internal a))+        mkVar v = inj (mkVarSym ta v) :&: ta++        mkLam :: Name -> sym (Internal b :-> Full (Internal a -> Internal b))+        mkLam v = inj (mkLamSym ta tb v) :&: funType ta tb++    sugar = error "sugar not implemented for (a -> b)"+
+ src/Language/Syntactic/TypeRep/Sugar/TupleTR.hs view
@@ -0,0 +1,73 @@+{-# LANGUAGE UndecidableInstances #-}++-- | 'Syntactic' instances for tuples and symbol domains decorated with+-- 'TypeRep'++module Language.Syntactic.TypeRep.Sugar.TupleTR where++++import Language.Syntactic+import Language.Syntactic.Functional.Tuple++import Data.TypeRep+import Data.TypeRep.Types.Tuple+import Data.TypeRep.Types.Tuple.Typeable ()+import Language.Syntactic.TypeRep++++instance+    ( sym ~ (s :&: TypeRep t)+    , Syntactic a, Domain a ~ sym+    , Syntactic b, Domain b ~ sym+    , Tuple :<: s+    , Typeable t (Internal a)+    , Typeable t (Internal b)+    , TupleType :<: t+    ) =>+      Syntactic (a,b)+  where+    type Domain (a,b)   = Domain a+    type Internal (a,b) = (Internal a, Internal b)+    desugar (a,b) = sugarSymTR Tup2 a b+    sugar ab      = (sugarSymTR Sel1 ab, sugarSymTR Sel2 ab)++instance+    ( sym ~ (s :&: TypeRep t)+    , Syntactic a, Domain a ~ sym+    , Syntactic b, Domain b ~ sym+    , Syntactic c, Domain c ~ sym+    , Tuple :<: s+    , Typeable t (Internal a)+    , Typeable t (Internal b)+    , Typeable t (Internal c)+    , TupleType :<: t+    ) =>+      Syntactic (a,b,c)+  where+    type Domain (a,b,c)   = Domain a+    type Internal (a,b,c) = (Internal a, Internal b, Internal c)+    desugar (a,b,c) = sugarSymTR Tup3 a b c+    sugar abc       = (sugarSymTR Sel1 abc, sugarSymTR Sel2 abc, sugarSymTR Sel3 abc)++instance+    ( sym ~ (s :&: TypeRep t)+    , Syntactic a, Domain a ~ sym+    , Syntactic b, Domain b ~ sym+    , Syntactic c, Domain c ~ sym+    , Syntactic d, Domain d ~ sym+    , Tuple :<: s+    , Typeable t (Internal a)+    , Typeable t (Internal b)+    , Typeable t (Internal c)+    , Typeable t (Internal d)+    , TupleType :<: t+    ) =>+      Syntactic (a,b,c,d)+  where+    type Domain (a,b,c,d)   = Domain a+    type Internal (a,b,c,d) = (Internal a, Internal b, Internal c, Internal d)+    desugar (a,b,c,d) = sugarSymTR Tup4 a b c d+    sugar abcd        = (sugarSymTR Sel1 abcd, sugarSymTR Sel2 abcd, sugarSymTR Sel3 abcd, sugarSymTR Sel4 abcd)+
+ src/Language/Syntactic/TypeRep/TupleConversion.hs view
@@ -0,0 +1,82 @@+-- | Construction and elimination of tuples+--+-- Something similar can be achieved using the 'Syntactic' instances from+-- "Language.Syntactic.TypeRep.Sugar.TupleTR", e.g:+--+-- > sel1' :: forall sym t a b+-- >     .  ( Typeable t a+-- >        , Typeable t b+-- >        , Tuple     :<: sym+-- >        , TupleType :<: t+-- >        )+-- >     => ASTF (sym :&: TypeRep t) (a,b) -> ASTF (sym :&: TypeRep t) a+-- > sel1' ab = a+-- >   where+-- >     (a, _ :: ASTF (sym :&: TypeRep t) b) = sugar ab+--+-- But the point of this module is to do it without the 'Typeable' constraint.++module Language.Syntactic.TypeRep.TupleConversion where++++import Language.Syntactic+import Language.Syntactic.Functional.Tuple++import Data.TypeRep.Representation+import Data.TypeRep.Types.Tuple+import Language.Syntactic.TypeRep.Sugar.TupleTR () -- For documentation++++sel1 :: (Tuple :<: sym, TupleType :<: t) =>+    ASTF (sym :&: TypeRep t) tup -> ASTF (sym :&: TypeRep t) (Sel1 tup)+sel1 a = case unTypeRep $ getDecor a of+    tup :$ ta :$ tb             | Just Tup2_t <- prj tup -> Sym (inj Sel1 :&: TypeRep ta) :$ a+    tup :$ ta :$ tb :$ tc       | Just Tup3_t <- prj tup -> Sym (inj Sel1 :&: TypeRep ta) :$ a+    tup :$ ta :$ tb :$ tc :$ td | Just Tup4_t <- prj tup -> Sym (inj Sel1 :&: TypeRep ta) :$ a++sel2 :: (Tuple :<: sym, TupleType :<: t) =>+    ASTF (sym :&: TypeRep t) tup -> ASTF (sym :&: TypeRep t) (Sel2 tup)+sel2 a = case unTypeRep $ getDecor a of+    tup :$ ta :$ tb             | Just Tup2_t <- prj tup -> Sym (inj Sel2 :&: TypeRep tb) :$ a+    tup :$ ta :$ tb :$ tc       | Just Tup3_t <- prj tup -> Sym (inj Sel2 :&: TypeRep tb) :$ a+    tup :$ ta :$ tb :$ tc :$ td | Just Tup4_t <- prj tup -> Sym (inj Sel2 :&: TypeRep tb) :$ a++sel3 :: (Tuple :<: sym, TupleType :<: t) =>+    ASTF (sym :&: TypeRep t) tup -> ASTF (sym :&: TypeRep t) (Sel3 tup)+sel3 a = case unTypeRep $ getDecor a of+    tup :$ ta :$ tb :$ tc       | Just Tup3_t <- prj tup -> Sym (inj Sel3 :&: TypeRep tc) :$ a+    tup :$ ta :$ tb :$ tc :$ td | Just Tup4_t <- prj tup -> Sym (inj Sel3 :&: TypeRep tc) :$ a++sel4 :: (Tuple :<: sym, TupleType :<: t) =>+    ASTF (sym :&: TypeRep t) tup -> ASTF (sym :&: TypeRep t) (Sel4 tup)+sel4 a = case unTypeRep $ getDecor a of+    tup :$ ta :$ tb :$ tc :$ td | Just Tup4_t <- prj tup -> Sym (inj Sel4 :&: TypeRep td) :$ a++tup2+    :: (Tuple :<: sym, TupleType :<: t)+    => ASTF (sym :&: TypeRep t) a -> ASTF (sym :&: TypeRep t) b+    -> ASTF (sym :&: TypeRep t) (a,b)+tup2 a b =+    Sym (inj Tup2 :&: tup2Type (getDecor a) (getDecor b))+      :$ a :$ b++tup3+    :: (Tuple :<: sym, TupleType :<: t)+    => ASTF (sym :&: TypeRep t) a -> ASTF (sym :&: TypeRep t) b+    -> ASTF (sym :&: TypeRep t) c+    -> ASTF (sym :&: TypeRep t) (a,b,c)+tup3 a b c =+    Sym (inj Tup3 :&: tup3Type (getDecor a) (getDecor b) (getDecor c))+      :$ a :$ b :$ c++tup4+    :: (Tuple :<: sym, TupleType :<: t)+    => ASTF (sym :&: TypeRep t) a -> ASTF (sym :&: TypeRep t) b+    -> ASTF (sym :&: TypeRep t) c -> ASTF (sym :&: TypeRep t) d+    -> ASTF (sym :&: TypeRep t) (a,b,c,d)+tup4 a b c d =+    Sym (inj Tup4 :&: tup4Type (getDecor a) (getDecor b) (getDecor c) (getDecor d))+      :$ a :$ b :$ c :$ d+
+ tests/Tests.hs view
@@ -0,0 +1,17 @@+{-# LANGUAGE CPP #-}++import qualified Simple+#if __GLASGOW_HASKELL__ >= 710+import qualified Custom+#endif++++main = do+    Simple.main+#if __GLASGOW_HASKELL__ >= 710+    Custom.main+#endif++-- Importing both modules causes overlapping instances error on GHC < 7.10+