singletons 0.8.3 → 0.8.4
raw patch · 10 files changed
+426/−310 lines, 10 filesdep ~basedep ~template-haskell
Dependency ranges changed: base, template-haskell
Files
- CHANGES +10/−0
- Data/Singletons.hs +26/−73
- Data/Singletons/CustomStar.hs +4/−5
- Data/Singletons/Exports.hs +64/−0
- Data/Singletons/Promote.hs +111/−92
- Data/Singletons/Singletons.hs +175/−129
- Data/Singletons/TypeRepStar.hs +1/−1
- Data/Singletons/Util.hs +24/−5
- README +8/−2
- singletons.cabal +3/−3
CHANGES view
@@ -1,6 +1,16 @@ Changelog for singletons project ================================ +0.8.4+-----++Update to work with latest version of GHC (7.7.20130114).++Now use branched type family instances to allow for promotion of functions+with overlapping patterns.++Permit promotion of functions with constraints by omitting constraints.+ 0.8.3 -----
Data/Singletons.hs view
@@ -1,6 +1,6 @@ {- Data/Singletons.hs -(c) Richard Eisenberg 2012+(c) Richard Eisenberg 2013 eir@cis.upenn.edu This is the public interface file to the singletons library. Please@@ -15,7 +15,8 @@ FlexibleContexts, RankNTypes, UndecidableInstances, FlexibleInstances, ScopedTypeVariables, CPP #-}-{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}+{-# OPTIONS_GHC -fwarn-incomplete-patterns -fno-warn-unused-binds #-}+-- We make unused bindings for (||), (&&), and not. module Data.Singletons ( OfKind(..), Sing(..), SingI(..), SingE(..), SingRep, KindOf, Demote,@@ -26,58 +27,22 @@ sTuple0, sTuple2, sTuple3, sTuple4, sTuple5, sTuple6, sTuple7, STuple0, STuple2, STuple3, STuple4, STuple5, STuple6, STuple7, Not, sNot, (:&&), (%:&&), (:||), (%:||), (:&&:), (:||:), (:/=), (:/=:),- SEq((%==%), (%/=%), (%:==), (%:/=)),+ SEq((%==%), (%/=%)), (%:==), (%:/=), If, sIf, sNil, sCons, SList, (:++), (%:++), Head, Tail, cases, bugInGHC, genSingletons, singletons, genPromotions, promote,+ promoteEqInstances, promoteEqInstance, singEqInstance, singEqInstances ) where import Prelude hiding ((++)) import Data.Singletons.Singletons import Data.Singletons.Promote+import Data.Singletons.Exports import Language.Haskell.TH import Data.Singletons.Util import GHC.Exts (Any) -#if __GLASGOW_HASKELL__ >= 707--import GHC.TypeLits ( OfKind(..), Sing(..), SingI(..), SingE(..),- SingRep, KindOf, Demote )--#else---- Kind-level proxy-data OfKind (k :: *) = KindParam---- Access the kind of a type variable-type KindOf (a :: k) = (KindParam :: OfKind k)---- Declarations of singleton structures-data family Sing (a :: k)-class SingI (a :: k) where- sing :: Sing a-class (kparam ~ KindParam) => SingE (kparam :: OfKind k) where- type DemoteRep kparam :: *- fromSing :: Sing (a :: k) -> DemoteRep kparam---- SingRep is a synonym for (SingI, SingE)-class (SingI a, SingE (KindOf a)) => SingRep (a :: k)-instance (SingI a, SingE (KindOf a)) => SingRep (a :: k)---- Abbreviation for DemoteRep-type Demote (a :: k) = DemoteRep (KindParam :: OfKind k)--#endif--type family (a :: k) :==: (b :: k) :: Bool-type a :== b = a :==: b -- :== and :==: are synonyms--data SingInstance (a :: k) where- SingInstance :: SingRep a => SingInstance a-class (kparam ~ KindParam) => SingKind (kparam :: OfKind k) where- singInstance :: forall (a :: k). Sing a -> SingInstance a- -- provide a few useful singletons... $(genSingletons [''Bool, ''Maybe, ''Either, ''[]]) $(genSingletons [''(), ''(,), ''(,,), ''(,,,), ''(,,,,), ''(,,,,,), ''(,,,,,,)])@@ -89,17 +54,16 @@ not True = False (&&) :: Bool -> Bool -> Bool- False && a = False+ False && _ = False True && a = a (||) :: Bool -> Bool -> Bool False || a = a- True || a = True+ True || _ = True |]) --- symmetric syntax synonyms-type a :&&: b = a :&& b-type a :||: b = a :|| b+type family (a :: k) :==: (b :: k) :: Bool+type a :== b = a :==: b -- :== and :==: are synonyms type a :/=: b = Not (a :==: b) type a :/= b = a :/=: b@@ -107,39 +71,28 @@ -- the singleton analogue of @Eq@ class (kparam ~ KindParam) => SEq (kparam :: OfKind k) where (%==%) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :==: b)- (%:==) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :==: b)- (%:==) = (%==%)- (%:/=) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :/=: b)- a %:/= b = sNot (a %==% b) (%/=%) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :/=: b)- (%/=%) = (%:/=)---- type-level conditional-type family If (a :: Bool) (b :: k) (c :: k) :: k-type instance If 'True b c = b-type instance If 'False b c = c+ a %/=% b = sNot (a %==% b) --- singleton conditional-sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)-sIf STrue b c = b-sIf SFalse b c = c+(%:==) :: forall (a :: k) (b :: k). SEq (KindParam :: OfKind k)+ => Sing a -> Sing b -> Sing (a :==: b)+(%:==) = (%==%) -type instance '[] :==: '[] = True-type instance '[] :==: (h ': t) = False-type instance (h ': t) :==: '[] = False-type instance (h ': t) :==: (h' ': t') = (h :==: h') :&&: (t :==: t')+(%:/=) :: forall (a :: k) (b :: k). SEq (KindParam :: OfKind k)+ => Sing a -> Sing b -> Sing (a :/=: b)+(%:/=) = (%/=%) -instance SEq (KindParam :: OfKind k) => SEq (KindParam :: OfKind [k]) where- SNil %==% SNil = STrue- SNil %==% (SCons _ _) = SFalse- (SCons _ _) %==% SNil = SFalse- (SCons a b) %==% (SCons a' b') = (a %==% a') %:&& (b %==% b')+$(singEqInstances [''Bool, ''Maybe, ''Either, ''[]])+$(singEqInstances [''(), ''(,), ''(,,), ''(,,,), ''(,,,,), ''(,,,,,), ''(,,,,,,)]) -type family Head (a :: [k]) :: k-type instance Head (h ': t) = h+-- singleton conditional+sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)+sIf STrue b _ = b+sIf SFalse _ c = c -type family Tail (a :: [k]) :: [k]-type instance Tail (h ': t) = t+-- symmetric syntax synonyms+type a :&&: b = a :&& b+type a :||: b = a :|| b $(singletons [d| (++) :: [a] -> [a] -> [a]
Data/Singletons/CustomStar.hs view
@@ -1,6 +1,6 @@ {- Data/Singletons/CustomStar.hs -(c) Richard Eisenbeg 2012+(c) Richard Eisenbeg 2013 eir@cis.upenn.edu This file implements singletonStar, which generates a datatype Rep and associated@@ -8,7 +8,7 @@ Haskell types themselves. This is still very experimental, so expect unusual results! -} -+{-# LANGUAGE DataKinds, TypeFamilies, KindSignatures #-} {-# OPTIONS_GHC -fwarn-incomplete-patterns #-} module Data.Singletons.CustomStar where@@ -27,12 +27,11 @@ let repDecl = DataD [] repName [] ctors [mkName "Eq", mkName "Show", mkName "Read"] fakeCtors <- zipWithM (mkCtor False) names kinds- eqTypeInstances <- mapM mkEqTypeInstance [ (c1, c2) | c1 <- fakeCtors,- c2 <- fakeCtors ]+ eqInstance <- mkEqTypeInstance StarT fakeCtors singletonDecls <- singDataD True [] repName [] fakeCtors [mkName "Eq", mkName "Show", mkName "Read"] return $ repDecl :- eqTypeInstances +++ eqInstance : singletonDecls where -- get the kinds of the arguments to the tycon with the given name getKind :: Name -> Q [Kind]
+ Data/Singletons/Exports.hs view
@@ -0,0 +1,64 @@+{- Data/Singletons/Exports.hs++(c) Richard Eienberg 2013+eir@cis.upenn.edu++This file contains the fundamental datatype definitions for the singletons+package. These are all re-exported in Data/Singletons.hs+-}++{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, RankNTypes, + TypeOperators, GADTs, CPP #-}++module Data.Singletons.Exports (+ OfKind(..), Sing, SingI(..), SingE(..), SingRep, KindOf, Demote,++ SingInstance(..), SingKind(..), If, Head, Tail+ ) where++#if __GLASGOW_HASKELL__ >= 707++import GHC.TypeLits ( OfKind(..), Sing, SingI(..), SingE(..),+ SingRep, KindOf, Demote )++#else++-- Kind-level proxy+data OfKind (k :: *) = KindParam++-- Access the kind of a type variable+type KindOf (a :: k) = (KindParam :: OfKind k)++-- Declarations of singleton structures+data family Sing (a :: k)+class SingI (a :: k) where+ sing :: Sing a+class (kparam ~ KindParam) => SingE (kparam :: OfKind k) where+ type DemoteRep kparam :: *+ fromSing :: Sing (a :: k) -> DemoteRep kparam++-- SingRep is a synonym for (SingI, SingE)+class (SingI a, SingE (KindOf a)) => SingRep (a :: k)+instance (SingI a, SingE (KindOf a)) => SingRep (a :: k)++-- Abbreviation for DemoteRep+type Demote (a :: k) = DemoteRep (KindParam :: OfKind k)++#endif++data SingInstance (a :: k) where+ SingInstance :: SingRep a => SingInstance a+class (kparam ~ KindParam) => SingKind (kparam :: OfKind k) where+ singInstance :: forall (a :: k). Sing a -> SingInstance a++-- type-level conditional+type family If (a :: Bool) (b :: k) (c :: k) :: k+type instance If 'True b c = b+type instance If 'False b c = c++-- operate on type-level lists+type family Head (a :: [k]) :: k+type instance Head (h ': t) = h++type family Tail (a :: [k]) :: [k]+type instance Tail (h ': t) = t
Data/Singletons/Promote.hs view
@@ -1,37 +1,39 @@ {- Data/Singletons/Promote.hs -(c) Richard Eisenberg 2012+(c) Richard Eisenberg 2013 eir@cis.upenn.edu This file contains functions to promote term-level constructs to the type level. It is an internal module to the singletons package. -} +{-# LANGUAGE TemplateHaskell #-} {-# OPTIONS_GHC -fwarn-incomplete-patterns #-} module Data.Singletons.Promote where import Language.Haskell.TH import Data.Singletons.Util+import Data.Singletons.Exports+import GHC.Exts (Any) import Prelude hiding (exp) import qualified Data.Map as Map import qualified Data.Set as Set import Control.Monad-import Data.Maybe-import Control.Monad.Writer+import Control.Monad.Writer hiding (Any) import Data.List anyTypeName, falseName, trueName, andName, tyEqName, repName, ifName, headName, tailName :: Name-anyTypeName = mkName "Any"-falseName = mkName "False"-trueName = mkName "True"+anyTypeName = ''Any+falseName = 'False+trueName = 'True andName = mkName "&&" tyEqName = mkName ":==:" repName = mkName "Rep"-ifName = mkName "If"-headName = mkName "Head"-tailName = mkName "Tail"+ifName = ''If+headName = ''Head+tailName = ''Tail falseTy :: Type falseTy = promoteDataCon falseName@@ -59,21 +61,21 @@ return $ concat decls promoteInfo :: Info -> Q [Dec]-promoteInfo (ClassI dec instances) =+promoteInfo (ClassI _dec _instances) = fail "Promotion of class info not supported"-promoteInfo (ClassOpI name ty className fixity) =+promoteInfo (ClassOpI _name _ty _className _fixity) = fail "Promotion of class members info not supported" promoteInfo (TyConI dec) = evalWithoutAux $ promoteDec Map.empty dec-promoteInfo (FamilyI dec instances) =+promoteInfo (FamilyI _dec _instances) = fail "Promotion of type family info not yet supported" -- KindFams-promoteInfo (PrimTyConI name numArgs unlifted) =+promoteInfo (PrimTyConI _name _numArgs _unlifted) = fail "Promotion of primitive type constructors not supported"-promoteInfo (DataConI name ty tyname fixity) =+promoteInfo (DataConI _name _ty _tyname _fixity) = fail $ "Promotion of individual constructors not supported; " ++ "promote the type instead"-promoteInfo (VarI name ty mdec fixity) =+promoteInfo (VarI _name _ty _mdec _fixity) = fail "Promotion of value info not supported"-promoteInfo (TyVarI name ty) =+promoteInfo (TyVarI _name _ty) = fail "Promotion of type variable info not supported" promoteDataCon :: Name -> Type@@ -91,14 +93,17 @@ promoteVal = ConT . promoteValName promoteType :: Type -> Q Kind-promoteType (ForallT tvbs [] ty) = promoteType ty -- ForallKinds-promoteType (ForallT _ (_:_) _) = fail "Cannot promote type with constrained variables"+-- We don't need to worry about constraints: they are used to express+-- static guarantees at runtime. But, because we don't need to do+-- anything special to keep static guarantees at compile time, we don't+-- need to promote them.+promoteType (ForallT _tvbs _ ty) = promoteType ty -- ForallKinds promoteType (VarT name) = return $ VarT name promoteType (ConT name) = return $ if (nameBase name) == "TypeRep" || (nameBase name) == (nameBase repName) then StarT else ConT name promoteType (TupleT n) = return $ TupleT n-promoteType (UnboxedTupleT n) = fail "Promotion of unboxed tuples not supported"+promoteType (UnboxedTupleT _n) = fail "Promotion of unboxed tuples not supported" promoteType ArrowT = return ArrowT promoteType ListT = return ListT promoteType (AppT (AppT ArrowT (ForallT (_:_) _ _)) _) =@@ -107,7 +112,7 @@ k1 <- promoteType ty1 k2 <- promoteType ty2 return $ AppT k1 k2-promoteType (SigT ty _) = fail "Cannot promote type of kind other than *"+promoteType (SigT _ty _) = fail "Cannot promote type of kind other than *" promoteType (LitT _) = fail "Cannot promote a type-level literal" promoteType (PromotedT _) = fail "Cannot promote a promoted data constructor" promoteType (PromotedTupleT _) = fail "Cannot promote tuples that are already promoted"@@ -177,33 +182,44 @@ noTypeSigs return (newDecls' ++ moreNewDecls, noTypeSigs) --- produce the type instance for (:==:) for the given pair of constructors-mkEqTypeInstance :: (Con, Con) -> Q Dec-mkEqTypeInstance (c1, c2) =- if c1 == c2- then do- let (name, numArgs) = extractNameArgs c1- lnames <- replicateM numArgs (newName "a")- rnames <- replicateM numArgs (newName "b")- let lvars = map VarT lnames- rvars = map VarT rnames- return $ TySynInstD- tyEqName- [foldType (PromotedT name) lvars,- foldType (PromotedT name) rvars]- (tyAll (zipWith (\l r -> foldType (ConT tyEqName) [l, r])- lvars rvars))- else do- let (lname, lNumArgs) = extractNameArgs c1- (rname, rNumArgs) = extractNameArgs c2- lnames <- replicateM lNumArgs (newName "a")- rnames <- replicateM rNumArgs (newName "b")- return $ TySynInstD- tyEqName- [foldType (PromotedT lname) (map VarT lnames),- foldType (PromotedT rname) (map VarT rnames)]- falseTy- where tyAll :: [Type] -> Type -- "all" at the type level+-- produce instances for (:==:) from the given types+promoteEqInstances :: [Name] -> Q [Dec]+promoteEqInstances = concatMapM promoteEqInstance++-- produce instance for (:==:) from the given type+promoteEqInstance :: Name -> Q [Dec]+promoteEqInstance name = do+ (tvbs, cons) <- getDataD "I cannot make an instance of (:==:) for it." name+ vars <- replicateM (length tvbs) (newName "k")+ let tyvars = map VarT vars+ kind = foldType (ConT name) tyvars+ inst <- mkEqTypeInstance kind cons+ return [inst]++-- produce the branched type instance for (:==:) over the given list of ctors+mkEqTypeInstance :: Kind -> [Con] -> Q Dec+mkEqTypeInstance kind cons = do+ tySynInstD tyEqName (map mk_branch cons ++ [false_case])+ where mk_branch :: Con -> Q TySynEqn+ mk_branch con = do+ let (name, numArgs) = extractNameArgs con+ lnames <- replicateM numArgs (newName "a")+ rnames <- replicateM numArgs (newName "b")+ let lvars = map VarT lnames+ rvars = map VarT rnames+ ltype = foldType (PromotedT name) lvars+ rtype = foldType (PromotedT name) rvars+ results = zipWith (\l r -> foldType (ConT tyEqName) [l, r]) lvars rvars+ result = tyAll results+ return $ TySynEqn [ltype, rtype] result++ false_case :: Q TySynEqn+ false_case = do+ lvar <- newName "a"+ rvar <- newName "b"+ return $ TySynEqn [SigT (VarT lvar) kind, SigT (VarT rvar) kind] falseTy++ tyAll :: [Type] -> Type -- "all" at the type level tyAll [] = trueTy tyAll [one] = one tyAll (h:t) = foldType andTy [h, (tyAll t)]@@ -223,9 +239,10 @@ vars' = Map.insert name (promoteVal name) vars numArgs = getNumPats (head clauses) -- count the parameters -- Haskell requires all clauses to have the same number of parameters- instDecls <- lift $ mapM (promoteClause vars' proName) clauses+ (eqns, instDecls) <- lift $ evalForPair $+ mapM (promoteClause vars') clauses addBinding name numArgs -- remember the number of parameters- return $ concat instDecls+ return $ (TySynInstD proName eqns) : instDecls where getNumPats :: Clause -> Int getNumPats (Clause pats _ _) = length pats promoteDec vars (ValD pat body decs) = do@@ -238,7 +255,7 @@ if any (flip containsName rhs) (map lhsName lhss) then do -- definition is recursive. use type families & require ty sigs mapM (flip addBinding 0) (map lhsRawName lhss)- return $ (map (\(LHS _ nm hole) -> TySynInstD nm [] (hole rhs)) lhss) +++ return $ (map (\(LHS _ nm hole) -> TySynInstD nm [TySynEqn [] (hole rhs)]) lhss) ++ decls ++ decls' else do -- definition is not recursive; just use "type" decls mapM (flip addBinding typeSynonymFlag) (map lhsRawName lhss)@@ -248,37 +265,38 @@ promoteDataD vars cxt name tvbs ctors derivings promoteDec vars (NewtypeD cxt name tvbs ctor derivings) = promoteDataD vars cxt name tvbs [ctor] derivings-promoteDec vars (TySynD name tvbs ty) =+promoteDec _vars (TySynD _name _tvbs _ty) = fail "Promotion of type synonym declaration not yet supported"-promoteDec vars (ClassD cxt name tvbs fundeps decs) =+promoteDec _vars (ClassD _cxt _name _tvbs _fundeps _decs) = fail "Promotion of class declaration not yet supported"-promoteDec vars (InstanceD cxt ty decs) =+promoteDec _vars (InstanceD _cxt _ty _decs) = fail "Promotion of instance declaration not yet supported"-promoteDec vars (SigD name ty) = return [] -- handle in promoteDec'-promoteDec vars (ForeignD fgn) =+promoteDec _vars (SigD _name _ty) = return [] -- handle in promoteDec'+promoteDec _vars (ForeignD _fgn) = fail "Promotion of foreign function declaration not yet supported"-promoteDec vars (InfixD fixity name)+promoteDec _vars (InfixD fixity name) | isUpcase name = return [] -- automatic: promoting a type or data ctor | otherwise = return [InfixD fixity (promoteValName name)] -- value-promoteDec vars (PragmaD prag) =+promoteDec _vars (PragmaD _prag) = fail "Promotion of pragmas not yet supported"-promoteDec vars (FamilyD flavour name tvbs mkind) =+promoteDec _vars (FamilyD _flavour _name _tvbs _mkind) = fail "Promotion of type and data families not yet supported"-promoteDec vars (DataInstD cxt name tys ctors derivings) =+promoteDec _vars (DataInstD _cxt _name _tys _ctors _derivings) = fail "Promotion of data instances not yet supported"-promoteDec vars (NewtypeInstD cxt name tys ctors derivings) =+promoteDec _vars (NewtypeInstD _cxt _name _tys _ctors _derivings) = fail "Promotion of newtype instances not yet supported"-promoteDec vars (TySynInstD name tys ty) =- fail "Promotion of type synonym instances not yet supported)"+promoteDec _vars (TySynInstD _name _eqns) =+ fail "Promotion of type synonym instances not yet supported" -- only need to check if the datatype derives Eq. The rest is automatic. promoteDataD :: TypeTable -> Cxt -> Name -> [TyVarBndr] -> [Con] -> [Name] -> NumArgsQ [Dec]-promoteDataD vars cxt name tvbs ctors derivings =+promoteDataD _vars _cxt name tvbs ctors derivings = if any (\n -> (nameBase n) == "Eq") derivings then do- let pairs = [ (c1, c2) | c1 <- ctors, c2 <- ctors ]- lift $ mapM mkEqTypeInstance pairs+ kvs <- replicateM (length tvbs) (lift $ newName "k")+ inst <- lift $ mkEqTypeInstance (foldType (ConT name) (map VarT kvs)) ctors+ return [inst] else return [] -- the actual promotion is automatic -- second pass through declarations to deal with type signatures@@ -313,15 +331,15 @@ return $ (AppT (AppT ArrowT h) k) promoteDec' _ _ = return ([], []) -promoteClause :: TypeTable -> Name -> Clause -> Q [Dec]-promoteClause vars name (Clause pats body []) = do+promoteClause :: TypeTable -> Clause -> QWithDecs TySynEqn+promoteClause vars (Clause pats body []) = do -- promoting the patterns creates variable bindings. These are passed -- to the function promoted the RHS- (types, vartbl) <- evalForPair $ mapM promotePat pats+ (types, vartbl) <- lift $ evalForPair $ mapM promotePat pats let vars' = Map.union vars vartbl- (ty, decls) <- evalForPair $ promoteBody vars' body- return $ decls ++ [TySynInstD name types ty]-promoteClause _ _ (Clause _ _ (_:_)) =+ ty <- promoteBody vars' body+ return $ TySynEqn types ty+promoteClause _ (Clause _ _ (_:_)) = fail "A <<where>> clause in a function definition is not yet supported" -- the LHS of a top-level expression is a name and "type with hole"@@ -369,9 +387,10 @@ componentNames <- lift $ replicateM (length pats) (newName "a") zipWithM (\extractorName componentName -> addElement $ TySynInstD extractorName- [foldType (promoteDataCon name)+ [TySynEqn+ [foldType (promoteDataCon name) (map VarT componentNames)]- (VarT componentName))+ (VarT componentName)]) extractorNames componentNames -- now we have the extractor families. Use the appropriate families@@ -417,7 +436,7 @@ promoteTopLevelPat (BangP pat) = do lift $ reportWarning "Strict pattern converted into regular pattern in promotion" promoteTopLevelPat pat-promoteTopLevelPat (AsP name pat) =+promoteTopLevelPat (AsP _name _pat) = fail "Promotion of aliased patterns at top level not yet supported" promoteTopLevelPat WildP = return [] promoteTopLevelPat (RecP _ _) =@@ -491,15 +510,15 @@ promoteBody :: TypeTable -> Body -> QWithDecs Type promoteBody vars (NormalB exp) = promoteExp vars exp-promoteBody vars (GuardedB _) =+promoteBody _vars (GuardedB _) = fail "Promoting guards in patterns not yet supported" promoteExp :: TypeTable -> Exp -> QWithDecs Type promoteExp vars (VarE name) = case Map.lookup name vars of Just ty -> return ty Nothing -> return $ promoteVal name-promoteExp vars (ConE name) = return $ promoteDataCon name-promoteExp vars (LitE lit) = fail "Promotion of literal expressions not supported"+promoteExp _vars (ConE name) = return $ promoteDataCon name+promoteExp _vars (LitE _lit) = fail "Promotion of literal expressions not supported" promoteExp vars (AppE exp1 exp2) = do ty1 <- promoteExp vars exp1 ty2 <- promoteExp vars exp2@@ -508,41 +527,41 @@ case (mexp1, mexp2) of (Nothing, Nothing) -> promoteExp vars exp (Just exp1, Nothing) -> promoteExp vars (AppE exp exp1)- (Nothing, Just exp2) ->+ (Nothing, Just _exp2) -> fail "Promotion of right-only sections not yet supported" (Just exp1, Just exp2) -> promoteExp vars (AppE (AppE exp exp1) exp2)-promoteExp vars (UInfixE _ _ _) =+promoteExp _vars (UInfixE _ _ _) = fail "Promotion of unresolved infix operators not supported"-promoteExp vars (ParensE _) = fail "Promotion of unresolved parens not supported"-promoteExp vars (LamE pats exp) =+promoteExp _vars (ParensE _) = fail "Promotion of unresolved parens not supported"+promoteExp _vars (LamE _pats _exp) = fail "Promotion of lambda expressions not yet supported"-promoteExp vars (LamCaseE alts) =+promoteExp _vars (LamCaseE _alts) = fail "Promotion of lambda-case expressions not yet supported" promoteExp vars (TupE exps) = do tys <- mapM (promoteExp vars) exps let tuple = PromotedTupleT (length tys) tup = foldType tuple tys return tup-promoteExp vars (UnboxedTupE _) = fail "Promotion of unboxed tuples not supported"+promoteExp _vars (UnboxedTupE _) = fail "Promotion of unboxed tuples not supported" promoteExp vars (CondE bexp texp fexp) = do tys <- mapM (promoteExp vars) [bexp, texp, fexp] return $ foldType ifTyFam tys-promoteExp vars (MultiIfE alts) =+promoteExp _vars (MultiIfE _alts) = fail "Promotion of multi-way if not yet supported"-promoteExp vars (LetE decs exp) =+promoteExp _vars (LetE _decs _exp) = fail "Promotion of let statements not yet supported"-promoteExp vars (CaseE exp matches) =+promoteExp _vars (CaseE _exp _matches) = fail "Promotion of case statements not yet supported"-promoteExp vars (DoE stmts) = fail "Promotion of do statements not supported"-promoteExp vars (CompE stmts) =+promoteExp _vars (DoE _stmts) = fail "Promotion of do statements not supported"+promoteExp _vars (CompE _stmts) = fail "Promotion of list comprehensions not yet supported"-promoteExp vars (ArithSeqE _) = fail "Promotion of ranges not supported"+promoteExp _vars (ArithSeqE _) = fail "Promotion of ranges not supported" promoteExp vars (ListE exps) = do tys <- mapM (promoteExp vars) exps return $ foldr (\ty lst -> AppT (AppT PromotedConsT ty) lst) PromotedNilT tys-promoteExp vars (SigE exp ty) =+promoteExp _vars (SigE _exp _ty) = fail "Promotion of explicit type annotations not yet supported"-promoteExp vars (RecConE name fields) =+promoteExp _vars (RecConE _name _fields) = fail "Promotion of record construction not yet supported"-promoteExp vars (RecUpdE exp fields) =+promoteExp _vars (RecUpdE _exp _fields) = fail "Promotion of record updates not yet supported"
Data/Singletons/Singletons.hs view
@@ -1,17 +1,18 @@ {- Data/Singletons/Singletons.hs -(c) Richard Eisenberg 2012+(c) Richard Eisenberg 2013 eir@cis.upenn.edu This file contains functions to refine constructs to work with singleton types. It is an internal module to the singletons package. -}-+{-# LANGUAGE PatternGuards, TemplateHaskell #-} {-# OPTIONS_GHC -fwarn-incomplete-patterns #-} module Data.Singletons.Singletons where import Language.Haskell.TH+import Data.Singletons.Exports import Data.Singletons.Util import Data.Singletons.Promote import qualified Data.Map as Map@@ -30,19 +31,21 @@ type TypeContext = [Type] singFamilyName, isSingletonName, forgettableName, comboClassName, witnessName,- demoteName, singKindClassName, singInstanceMethName, singInstanceName,- sEqClassName, sEqMethName, sconsName, snilName, smartSconsName,- smartSnilName, sIfName, undefinedName, kindParamName, ofKindName :: Name-singFamilyName = mkName "Sing"-isSingletonName = mkName "SingI"-forgettableName = mkName "SingE"-comboClassName = mkName "SingRep"-witnessName = mkName "sing"-forgetName = mkName "fromSing"-demoteName = mkName "DemoteRep"-singKindClassName = mkName "SingKind"-singInstanceMethName = mkName "singInstance"-singInstanceName = mkName "SingInstance"+ demoteName, singKindClassName, singInstanceMethName, singInstanceTyConName,+ singInstanceDataConName, sEqClassName, sEqMethName, sconsName, snilName,+ smartSconsName, smartSnilName, sIfName, undefinedName, kindParamName,+ ofKindName :: Name+singFamilyName = ''Sing+isSingletonName = ''SingI+forgettableName = ''SingE+comboClassName = ''SingRep+witnessName = 'sing+forgetName = 'fromSing+demoteName = ''DemoteRep+singKindClassName = ''SingKind+singInstanceMethName = 'singInstance+singInstanceTyConName = ''SingInstance+singInstanceDataConName = 'SingInstance sEqClassName = mkName "SEq" sEqMethName = mkName "%==%" sconsName = mkName "SCons"@@ -50,9 +53,9 @@ smartSconsName = mkName "sCons" smartSnilName = mkName "sNil" sIfName = mkName "sIf"-undefinedName = mkName "undefined"-kindParamName = mkName "KindParam"-ofKindName = mkName "OfKind"+undefinedName = 'undefined+kindParamName = 'KindParam+ofKindName = ''OfKind mkTupleName :: Int -> Name mkTupleName n = mkName $ "STuple" ++ (show n)@@ -67,13 +70,13 @@ singInstanceMeth = VarE singInstanceMethName singInstanceTyCon :: Type-singInstanceTyCon = ConT singInstanceName+singInstanceTyCon = ConT singInstanceTyConName singInstanceDataCon :: Exp-singInstanceDataCon = ConE singInstanceName+singInstanceDataCon = ConE singInstanceDataConName singInstancePat :: Pat-singInstancePat = ConP singInstanceName []+singInstancePat = ConP singInstanceDataConName [] demote :: Type demote = ConT demoteName@@ -90,6 +93,9 @@ | isTupleName name = mkTupleName (tupleDegree $ nameBase name) | otherwise = prefixUCName "S" ":%" name +singClassName :: Name -> Name+singClassName = singTyConName+ singDataCon :: Name -> Exp singDataCon = ConE . singDataConName @@ -119,21 +125,21 @@ return $ concat decls singInfo :: Info -> Q [Dec]-singInfo (ClassI dec instances) =+singInfo (ClassI _dec _instances) = fail "Singling of class info not supported"-singInfo (ClassOpI name ty className fixity) =+singInfo (ClassOpI _name _ty _className _fixity) = fail "Singling of class members info not supported" singInfo (TyConI dec) = singDec dec-singInfo (FamilyI dec instances) =+singInfo (FamilyI _dec _instances) = fail "Singling of type family info not yet supported" -- KindFams-singInfo (PrimTyConI name numArgs unlifted) =+singInfo (PrimTyConI _name _numArgs _unlifted) = fail "Singling of primitive type constructors not supported"-singInfo (DataConI name ty tyname fixity) =+singInfo (DataConI _name _ty _tyname _fixity) = fail $ "Singling of individual constructors not supported; " ++ "single the type instead"-singInfo (VarI name ty mdec fixity) =+singInfo (VarI _name _ty _mdec _fixity) = fail "Singling of value info not supported"-singInfo (TyVarI name ty) =+singInfo (TyVarI _name _ty) = fail "Singling of type variable info not supported" -- refine a constructor. the first parameter is the type variable that@@ -180,7 +186,7 @@ (map (ClassP comboClassName . return) indices) ++ (map singKindConstraint bareKindVars)) (NormalC sName $ map (\ty -> (NotStrict,ty)) args))- (\tvbs cxt ctor -> case cxt of+ (\_tvbs cxt ctor -> case cxt of _:_ -> fail "Singling of constrained constructors not yet supported" [] -> singCtor a ctor) where buildArgTypes :: [Type] -> [Type] -> Q [Type]@@ -240,11 +246,11 @@ singDataD False cxt name tvbs ctors derivings singDec (NewtypeD cxt name tvbs ctor derivings) = singDataD False cxt name tvbs [ctor] derivings-singDec (TySynD name tvbs ty) =+singDec (TySynD _name _tvbs _ty) = fail "Singling of type synonyms not yet supported"-singDec (ClassD cxt name tvbs fundeps decs) =+singDec (ClassD _cxt _name _tvbs _fundeps _decs) = fail "Singling of class declaration not yet supported"-singDec (InstanceD cxt ty decs) =+singDec (InstanceD _cxt _ty _decs) = fail "Singling of class instance not yet supported" singDec (SigD name ty) = do tyTrans <- singType True ty@@ -260,23 +266,90 @@ singDec (InfixD fixity name) | isUpcase name = return [InfixD fixity (singDataConName name)] | otherwise = return [InfixD fixity (singValName name)]-singDec (PragmaD prag) = do+singDec (PragmaD _prag) = do reportWarning "Singling of pragmas not supported" return []-singDec (FamilyD flavour name tvbs mkind) =+singDec (FamilyD _flavour _name _tvbs _mkind) = fail "Singling of type and data families not yet supported"-singDec (DataInstD cxt name tys ctors derivings) = +singDec (DataInstD _cxt _name _tys _ctors _derivings) = fail "Singling of data instances not yet supported"-singDec (NewtypeInstD cxt name tys ctor derivings) =+singDec (NewtypeInstD _cxt _name _tys _ctor _derivings) = fail "Singling of newtype instances not yet supported"-singDec (TySynInstD name tys ty) =+singDec (TySynInstD _name _eqns) = fail "Singling of type family instances not yet supported" +-- create instances of SEq for each type in the list+singEqInstances :: [Name] -> Q [Dec]+singEqInstances = concatMapM singEqInstance++-- create instance of SEq for the given *singleton* type+singEqInstance :: Name -> Q [Dec]+singEqInstance name = do+ promotion <- promoteEqInstance name+ (tvbs, cons) <- getDataD "I cannot make an instance of SEq for it." name+ let tyvars = map (VarT . extractTvbName) tvbs+ kind = foldType (ConT name) tyvars+ aName <- newName "a"+ let aVar = VarT aName+ scons <- mapM (evalWithoutAux . singCtor aVar) cons+ dec <- mkSingEqInstance kind scons+ return $ dec : promotion++-- create an SEq instance for singletons of the given kind,+-- with the given *singleton* constructors +mkSingEqInstance :: Kind -> [Con] -> Q Dec+mkSingEqInstance k ctors = do+ let ctorPairs = [ (c1, c2) | c1 <- ctors, c2 <- ctors ]+ sEqMethClauses <- mapM mkEqMethClause ctorPairs+ return $ InstanceD (map (\k -> ClassP sEqClassName [kindParam k])+ (getBareKinds ctors))+ (AppT (ConT sEqClassName)+ (kindParam k))+ [FunD sEqMethName sEqMethClauses]+ where mkEqMethClause :: (Con, Con) -> Q Clause+ mkEqMethClause (c1, c2) =+ if c1 == c2+ then do+ let (name, numArgs) = extractNameArgs c1+ lnames <- replicateM numArgs (newName "a")+ rnames <- replicateM numArgs (newName "b")+ let lpats = map VarP lnames+ rpats = map VarP rnames+ lvars = map VarE lnames+ rvars = map VarE rnames+ return $ Clause+ [ConP name lpats, ConP name rpats]+ (NormalB $+ allExp (zipWith (\l r -> foldExp (VarE sEqMethName) [l, r])+ lvars rvars))+ []+ else do+ let (lname, lNumArgs) = extractNameArgs c1+ (rname, rNumArgs) = extractNameArgs c2+ return $ Clause+ [ConP lname (replicate lNumArgs WildP),+ ConP rname (replicate rNumArgs WildP)]+ (NormalB (singDataCon falseName))+ []++ getBareKinds :: [Con] -> [Kind]+ getBareKinds = foldl (\res -> ctorCases+ (\_ _ -> res) -- must be a constant constructor+ (\tvbs _ _ -> union res (filter isVarK $ map extractTvbKind tvbs)))+ []++ allExp :: [Exp] -> Exp+ allExp [] = singDataCon trueName+ allExp [one] = one+ allExp (h:t) = AppE (AppE (singVal andName) h) (allExp t)+ -- the first parameter is True when we're refining the special case "Rep" -- and false otherwise. We wish to consider the promotion of "Rep" to be * -- not a promoted data constructor. singDataD :: Bool -> Cxt -> Name -> [TyVarBndr] -> [Con] -> [Name] -> Q [Dec]-singDataD rep cxt name tvbs ctors derivings = do+singDataD rep cxt name tvbs ctors derivings+ | (_:_) <- cxt = fail "Singling of constrained datatypes is not supported"+ | otherwise = do aName <- newName "a" let a = VarT aName let tvbNames = map extractTvbName tvbs@@ -292,14 +365,7 @@ (map mkSingInstanceClause ctors')] -- SEq instance- let ctorPairs = [ (c1, c2) | c1 <- ctors', c2 <- ctors' ]- sEqMethClauses <- mapM mkEqMethClause ctorPairs- let sEqInst =- InstanceD (map (\k -> ClassP sEqClassName [kindParam k])- (getBareKinds ctors'))- (AppT (ConT sEqClassName)- (kindParam k))- [FunD sEqMethName sEqMethClauses]+ sEqInst <- mkSingEqInstance k ctors' -- e.g. type SNat (a :: Nat) = Sing a let kindedSynInst =@@ -312,10 +378,12 @@ let singEInst = InstanceD [] (AppT (ConT forgettableName) (kindParam k))- [TySynInstD demoteName [kindParam k]- (foldType (ConT name)- (map (\kv -> AppT demote (kindParam (VarT kv)))- tvbNames)),+ [TySynInstD demoteName+ [TySynEqn+ [kindParam k]+ (foldType (ConT name)+ (map (\kv -> AppT demote (kindParam (VarT kv)))+ tvbNames))], FunD forgetName forgetClauses] @@ -333,32 +401,6 @@ Clause [ConP nm (replicate (length tys) WildP)] (NormalB singInstanceDataCon) []) - mkEqMethClause :: (Con, Con) -> Q Clause- mkEqMethClause (c1, c2) =- if c1 == c2- then do- let (name, numArgs) = extractNameArgs c1- lnames <- replicateM numArgs (newName "a")- rnames <- replicateM numArgs (newName "b")- let lpats = map VarP lnames- rpats = map VarP rnames- lvars = map VarE lnames- rvars = map VarE rnames- return $ Clause- [ConP name lpats, ConP name rpats]- (NormalB $- allExp (zipWith (\l r -> foldExp (VarE sEqMethName) [l, r])- lvars rvars))- []- else do- let (lname, lNumArgs) = extractNameArgs c1- (rname, rNumArgs) = extractNameArgs c2- return $ Clause- [ConP lname (replicate lNumArgs WildP),- ConP rname (replicate rNumArgs WildP)]- (NormalB (singDataCon falseName))- []- mkForgetClause :: Con -> Q Clause mkForgetClause c = do let (name, numArgs) = extractNameArgs c@@ -369,17 +411,6 @@ (map (AppE (VarE forgetName) . VarE) varNames)) [] - getBareKinds :: [Con] -> [Kind]- getBareKinds = foldl (\res -> ctorCases- (\_ _ -> res) -- must be a constant constructor- (\tvbs _ _ -> union res (filter isVarK $ map extractTvbKind tvbs)))- []-- allExp :: [Exp] -> Exp- allExp [] = singDataCon trueName- allExp [one] = one- allExp (h:t) = AppE (AppE (singVal andName) h) (allExp t)- singKind :: Kind -> Q (Kind -> Kind) singKind (ForallT _ _ _) = fail "Singling of explicitly quantified kinds not yet supported"@@ -412,21 +443,23 @@ -- the first parameter is the list of types the current type is applied to -- the second parameter is whether or not this type occurs in a positive position singTypeRec :: TypeContext -> Bool -> Type -> Q TypeFn-singTypeRec ctx pos (ForallT tvbs (_:_) ty) =- fail "Singling of constrained functions not yet supported"-singTypeRec (_:_) pos (ForallT _ _ _) =+singTypeRec (_:_) _pos (ForallT _ _ _) = fail "I thought this was impossible in Haskell. Email me at eir@cis.upenn.edu with your code if you see this message." singTypeRec [] pos (ForallT _ [] ty) = -- Sing makes handling foralls automatic singTypeRec [] pos ty-singTypeRec (_:_) pos (VarT _) =+singTypeRec ctx pos (ForallT _tvbs cxt innerty) = do+ cxt' <- singContext cxt+ innerty' <- singTypeRec ctx pos innerty+ return $ \ty -> ForallT [] cxt' (innerty' ty)+singTypeRec (_:_) _pos (VarT _) = fail "Singling of type variables of arrow kinds not yet supported"-singTypeRec [] pos (VarT name) = +singTypeRec [] _pos (VarT _name) = return $ \ty -> AppT singFamily ty-singTypeRec ctx pos (ConT name) = -- we don't need to process the context with Sing+singTypeRec _ctx _pos (ConT _name) = -- we don't need to process the context with Sing return $ \ty -> AppT singFamily ty-singTypeRec ctx pos (TupleT n) = -- just like ConT+singTypeRec _ctx _pos (TupleT _n) = -- just like ConT return $ \ty -> AppT singFamily ty-singTypeRec ctx pos (UnboxedTupleT n) =+singTypeRec _ctx _pos (UnboxedTupleT _n) = fail "Singling of unboxed tuple types not yet supported" singTypeRec ctx pos ArrowT = case ctx of [ty1, ty2] -> do@@ -448,22 +481,34 @@ extractPolyKinds False (VarT k) = [VarT k] extractPolyKinds _ _ = [] _ -> fail "Internal error in Sing: converting ArrowT with improper context"-singTypeRec ctx pos ListT =+singTypeRec _ctx _pos ListT = return $ \ty -> AppT singFamily ty singTypeRec ctx pos (AppT ty1 ty2) = singTypeRec (ty2 : ctx) pos ty1 -- recur with the ty2 in the applied context-singTypeRec ctx pos (SigT ty knd) =+singTypeRec _ctx _pos (SigT _ty _knd) = fail "Singling of types with explicit kinds not yet supported"-singTypeRec ctx pos (LitT _) = fail "Singling of type-level literals not yet supported"-singTypeRec ctx pos (PromotedT _) =+singTypeRec _ctx _pos (LitT _) = fail "Singling of type-level literals not yet supported"+singTypeRec _ctx _pos (PromotedT _) = fail "Singling of promoted data constructors not yet supported"-singTypeRec ctx pos (PromotedTupleT _) =+singTypeRec _ctx _pos (PromotedTupleT _) = fail "Singling of type-level tuples not yet supported"-singTypeRec ctx pos PromotedNilT = fail "Singling of promoted nil not yet supported"-singTypeRec ctx pos PromotedConsT = fail "Singling of type-level cons not yet supported"-singTypeRec ctx pos StarT = fail "* used as type"-singTypeRec ctx pos ConstraintT = fail "Constraint used as type"+singTypeRec _ctx _pos PromotedNilT = fail "Singling of promoted nil not yet supported"+singTypeRec _ctx _pos PromotedConsT = fail "Singling of type-level cons not yet supported"+singTypeRec _ctx _pos StarT = fail "* used as type"+singTypeRec _ctx _pos ConstraintT = fail "Constraint used as type" +-- refine a constraint context+singContext :: Cxt -> Q Cxt+singContext = mapM singPred++singPred :: Pred -> Q Pred+singPred (ClassP name tys) = do+ kis <- mapM promoteType tys+ let sName = singClassName name+ return $ ClassP sName (map kindParam kis)+singPred (EqualP _ty1 _ty2) =+ fail "Singling of type equality constraints not yet supported"+ singClause :: ExpTable -> Clause -> Q Clause singClause vars (Clause pats (NormalB exp) []) = do (sPats, vartbl) <- evalForPair $ mapM (singPat Parameter) pats@@ -496,7 +541,7 @@ -- convert a pattern, building up the lexical scope as we go singPat :: PatternContext -> Pat -> ExpsQ Pat-singPat patCxt (LitP lit) =+singPat _patCxt (LitP _lit) = fail "Singling of literal patterns not yet supported" singPat patCxt (VarP name) = let newName = if patCxt == TopLevel then singValName name else name in do@@ -504,16 +549,16 @@ return $ VarP newName singPat patCxt (TupP pats) = singPat patCxt (ConP (tupleDataName (length pats)) pats)-singPat patCxt (UnboxedTupP pats) =+singPat _patCxt (UnboxedTupP _pats) = fail "Singling of unboxed tuples not supported" singPat patCxt (ConP name pats) = do checkIfBrainWillExplode patCxt pats' <- mapM (singPat patCxt) pats return $ ConP (singDataConName name) pats' singPat patCxt (InfixP pat1 name pat2) = singPat patCxt (ConP name [pat1, pat2])-singPat patCxt (UInfixP _ _ _) =+singPat _patCxt (UInfixP _ _ _) = fail "Singling of unresolved infix patterns not supported"-singPat patCxt (ParensP _) =+singPat _patCxt (ParensP _) = fail "Singling of unresolved paren patterns not supported" singPat patCxt (TildeP pat) = do pat' <- singPat patCxt pat@@ -526,24 +571,24 @@ pat' <- singPat patCxt pat addBinding name (VarE newName) return $ AsP name pat'-singPat patCxt WildP = return WildP-singPat patCxt (RecP name fields) =+singPat _patCxt WildP = return WildP+singPat _patCxt (RecP _name _fields) = fail "Singling of record patterns not yet supported" singPat patCxt (ListP pats) = do checkIfBrainWillExplode patCxt sPats <- mapM (singPat patCxt) pats return $ foldr (\elt lst -> ConP sconsName [elt, lst]) (ConP snilName []) sPats-singPat patCxt (SigP pat ty) =+singPat _patCxt (SigP _pat _ty) = fail "Singling of annotated patterns not yet supported"-singPat patCxt (ViewP exp pat) =+singPat _patCxt (ViewP _exp _pat) = fail "Singling of view patterns not yet supported" singExp :: ExpTable -> Exp -> Q Exp singExp vars (VarE name) = case Map.lookup name vars of Just exp -> return exp Nothing -> return (singVal name)-singExp vars (ConE name) = return $ smartCon name-singExp vars (LitE lit) =+singExp _vars (ConE name) = return $ smartCon name+singExp _vars (LitE _lit) = fail "Singling of literal expressions not yet supported" singExp vars (AppE exp1 exp2) = do exp1' <- singExp vars exp1@@ -553,47 +598,48 @@ case (mexp1, mexp2) of (Nothing, Nothing) -> singExp vars exp (Just exp1, Nothing) -> singExp vars (AppE exp exp1)- (Nothing, Just exp2) ->+ (Nothing, Just _exp2) -> fail "Singling of right-only sections not yet supported" (Just exp1, Just exp2) -> singExp vars (AppE (AppE exp exp1) exp2)-singExp vars (UInfixE _ _ _) =+singExp _vars (UInfixE _ _ _) = fail "Singling of unresolved infix expressions not supported"-singExp vars (ParensE _) =+singExp _vars (ParensE _) = fail "Singling of unresolved paren expressions not supported" singExp vars (LamE pats exp) = do (pats', vartbl) <- evalForPair $ mapM (singPat Parameter) pats let vars' = Map.union vartbl vars -- order matters; union is left-biased- singExp vars' exp-singExp vars (LamCaseE matches) = + exp' <- singExp vars' exp+ return $ LamE pats' exp'+singExp _vars (LamCaseE _matches) = fail "Singling of case expressions not yet supported" singExp vars (TupE exps) = do sExps <- mapM (singExp vars) exps sTuple <- singExp vars (ConE (tupleDataName (length exps))) return $ foldExp sTuple sExps-singExp vars (UnboxedTupE exps) =+singExp _vars (UnboxedTupE _exps) = fail "Singling of unboxed tuple not supported" singExp vars (CondE bexp texp fexp) = do exps <- mapM (singExp vars) [bexp, texp, fexp] return $ foldExp (VarE sIfName) exps-singExp vars (MultiIfE alts) =+singExp _vars (MultiIfE _alts) = fail "Singling of multi-way if statements not yet supported"-singExp vars (LetE decs exp) =+singExp _vars (LetE _decs _exp) = fail "Singling of let expressions not yet supported"-singExp vars (CaseE exp matches) =+singExp _vars (CaseE _exp _matches) = fail "Singling of case expressions not yet supported"-singExp vars (DoE stmts) =+singExp _vars (DoE _stmts) = fail "Singling of do expressions not yet supported"-singExp vars (CompE stmts) =+singExp _vars (CompE _stmts) = fail "Singling of list comprehensions not yet supported"-singExp vars (ArithSeqE range) =+singExp _vars (ArithSeqE _range) = fail "Singling of ranges not yet supported" singExp vars (ListE exps) = do sExps <- mapM (singExp vars) exps return $ foldr (\x -> (AppE (AppE (VarE smartSconsName) x))) (VarE smartSnilName) sExps-singExp vars (SigE exp ty) =+singExp _vars (SigE _exp _ty) = fail "Singling of annotated expressions not yet supported"-singExp vars (RecConE name fields) =+singExp _vars (RecConE _name _fields) = fail "Singling of record construction not yet supported"-singExp vars (RecUpdE exp fields) =+singExp _vars (RecUpdE _exp _fields) = fail "Singling of record updates not yet supported"
Data/Singletons/TypeRepStar.hs view
@@ -1,6 +1,6 @@ {- Data/Singletons/TypeRepStar.hs -(c) Richard Eisenberg 2012+(c) Richard Eisenberg 2013 eir@cis.upenn.edu This file contains the definitions for considering TypeRep to be the demotion
Data/Singletons/Util.hs view
@@ -1,6 +1,6 @@ {- Data/Singletons/Util.hs -(c) Richard Eisenberg 2012+(c) Richard Eisenberg 2013 eir@cis.upenn.edu This file contains helper functions internal to the singletons package.@@ -12,11 +12,8 @@ module Data.Singletons.Util where import Language.Haskell.TH-import Language.Haskell.TH.Syntax import Data.Char-import Data.Maybe import Data.Data-import Data.List import Control.Monad import Control.Monad.Writer import qualified Data.Map as Map@@ -27,7 +24,7 @@ reifyWithWarning name = recover (fail $ "Looking up " ++ (show name) ++ " in the list of available " ++ "declarations failed.\nThis lookup fails if the declaration " ++- "referenced was made in same Template\nHaskell splice as the use " +++ "referenced was made in the same Template\nHaskell splice as the use " ++ "of the declaration. If this is the case, put\nthe reference to " ++ "the declaration in a new splice.") (reify name)@@ -162,4 +159,26 @@ -- does a TH structure contain a name? containsName :: Data a => Name -> a -> Bool containsName n = everything (||) (mkQ False (== n))++-- lift concatMap into a monad+concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]+concatMapM fn list = do+ bss <- mapM fn list+ return $ concat bss++-- extract the tyvars and constructors from a name of a type,+-- printing out the string upon failure+getDataD :: String -> Name -> Q ([TyVarBndr], [Con])+getDataD error name = do+ info <- reifyWithWarning name+ dec <- case info of+ TyConI dec -> return dec+ _ -> badDeclaration+ case dec of+ DataD _cxt _name tvbs cons _derivings -> return (tvbs, cons)+ NewtypeD _cxt _name tvbs con _derivings -> return (tvbs, [con])+ _ -> badDeclaration+ where badDeclaration =+ fail $ "The name (" ++ (show name) ++ ") refers to something " +++ "other than a datatype. " ++ error
README view
@@ -3,7 +3,7 @@ This is the README file for the singletons library. This file contains all the documentation for the definitions and functions in the library. As of the time-of this writing (September 12, 2012), haddock has not quite caught up with GHC in+of this writing (January 16, 2013), haddock has not quite caught up with GHC in handling kind-polymorphic code, and the HEAD version of haddock cannot process Template Haskell. Thus, the documentation is in here. In the future, it will be generated by haddock.@@ -193,7 +193,12 @@ type family If (a :: Bool) (b :: k) (c :: k) :: k -This type family is a Boolean conditional at the type level.+This type family is a Boolean conditional at the type level. Note that type-+level computation is *strict* in GHC. Thus, you cannot use If to check a+termination condition in a recursive type family -- the type checker will+loop if you try. Corollary: you cannot use plain old 'if' to check a+termination condition in a term-level function you wish to promote or refine+into a singleton. sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)@@ -351,6 +356,7 @@ * (x +) sections * undefined * deriving Eq+* class constraints The following constructs will be coming soon:
singletons.cabal view
@@ -1,5 +1,5 @@ name: singletons-version: 0.8.3+version: 0.8.4 cabal-version: >= 1.8 synopsis: A framework for generating singleton types homepage: http://www.cis.upenn.edu/~eir/packages/singletons@@ -28,10 +28,10 @@ build-depends: base >= 4 && < 5, mtl >= 2.1.1,- template-haskell >= 2.8,+ template-haskell, containers >= 0.5, syb >= 0.3 exposed-modules: Data.Singletons, Data.Singletons.CustomStar, Data.Singletons.TypeRepStar other-modules: Data.Singletons.Promote, Data.Singletons.Singletons,- Data.Singletons.Util+ Data.Singletons.Util, Data.Singletons.Exports