diff --git a/CHANGES b/CHANGES --- a/CHANGES +++ b/CHANGES @@ -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 ----- diff --git a/Data/Singletons.hs b/Data/Singletons.hs --- a/Data/Singletons.hs +++ b/Data/Singletons.hs @@ -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] diff --git a/Data/Singletons/CustomStar.hs b/Data/Singletons/CustomStar.hs --- a/Data/Singletons/CustomStar.hs +++ b/Data/Singletons/CustomStar.hs @@ -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] diff --git a/Data/Singletons/Exports.hs b/Data/Singletons/Exports.hs new file mode 100644 --- /dev/null +++ b/Data/Singletons/Exports.hs @@ -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 diff --git a/Data/Singletons/Promote.hs b/Data/Singletons/Promote.hs --- a/Data/Singletons/Promote.hs +++ b/Data/Singletons/Promote.hs @@ -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 <> 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" diff --git a/Data/Singletons/Singletons.hs b/Data/Singletons/Singletons.hs --- a/Data/Singletons/Singletons.hs +++ b/Data/Singletons/Singletons.hs @@ -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" diff --git a/Data/Singletons/TypeRepStar.hs b/Data/Singletons/TypeRepStar.hs --- a/Data/Singletons/TypeRepStar.hs +++ b/Data/Singletons/TypeRepStar.hs @@ -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 diff --git a/Data/Singletons/Util.hs b/Data/Singletons/Util.hs --- a/Data/Singletons/Util.hs +++ b/Data/Singletons/Util.hs @@ -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 diff --git a/README b/README --- a/README +++ b/README @@ -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: diff --git a/singletons.cabal b/singletons.cabal --- a/singletons.cabal +++ b/singletons.cabal @@ -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