singletons (empty) → 0.8
raw patch · 10 files changed
+2056/−0 lines, 10 filesdep +basedep +containersdep +mtlsetup-changed
Dependencies added: base, containers, mtl, syb, template-haskell
Files
- LICENSE +27/−0
- README +404/−0
- Setup.hs +2/−0
- Singletons/CustomStar.hs +91/−0
- Singletons/Lib.hs +158/−0
- Singletons/Promote.hs +544/−0
- Singletons/Singletons.hs +599/−0
- Singletons/TypeRepStar.hs +31/−0
- Singletons/Util.hs +163/−0
- singletons.cabal +37/−0
+ LICENSE view
@@ -0,0 +1,27 @@+Copyright (c) 2012, Richard Eisenberg+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++1. Redistributions of source code must retain the above copyright notice, this+list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright notice,+this list of conditions and the following disclaimer in the documentation+and/or other materials provided with the distribution.++3. Neither the name of the author nor the names of its contributors may be+used to endorse or promote products derived from this software without+specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README view
@@ -0,0 +1,404 @@+singletons+==========++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 (June 2, 2012), 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.++The singletons library was written by Richard Eisenberg, eir@cis.upenn.edu.+See also /Dependently typed programming with singletons/, available at+<http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf>++---------------------------------+Purpose of the singletons library+---------------------------------++The library contains a definition of /singleton types/, which allow+programmers to use dependently typed techniques to enforce rich constraints+among the types in their programs. See the paper cited above for a+more thorough introduction.++-------------+Compatibility+-------------++The singletons library requires GHC version 7.5.20120529 or greater.+Any code that uses the singleton generation primitives will also need+to enable a long list of GHC extensions. This list includes, but+is not necessarily limited to, the following:++* TemplateHaskell+* TypeFamilies+* GADTs+* KindSignatures+* DataKinds+* PolyKinds+* TypeOperators+* FlexibleContexts+* RankNTypes+* UndecidableInstances+* FlexibleInstances++In addition, @ScopedTypeVariables@ is often very helpful.++--------------------------------+Functions to generate singletons+--------------------------------++There are four top-level functions used to generate the singleton definitions.+These functions should all be used within top-level Template Haskell splices.+See #supported-features# for a list of what Haskell constructs are supported.++These functions are all defined in Singletons.Lib.+++genPromotion :: [Name] -> Q [Dec]++Takes a list of names of types and promotes them to the kind level. Although+@DataKinds@ does this promotion automaticlly, the manual promotion also+handles generating instances of @:==:@, Boolean equality at the type level,+for type that derive @Eq@.++To use:++> $(genPromotion [''Bool, ''Maybe])+++genSingletons :: [Name] -> Q [Dec]++Takes a list of names of types and generates singleton type definitions+for them.++To use:++> $(genSingletons [''Bool, ''Maybe])+++promote :: Q [Dec] -> Q [Dec]++Promotes the declarations given.++To use:++> $(promote [d|+> data Nat = Zero | Succ Nat+> pred :: Nat -> Nat+> pred Zero = Zero+> pred (Succ n) = n+> |])+++singletons :: Q [Dec] -> Q [Dec]++Generates singletons from the definitions given. Because singleton generation+requires promotion, this also promotes all of the definitions given.++To use:+> $(singletons [d|+> data Nat = Zero | Succ Nat+> pred :: Nat -> Nat+> pred Zero = Zero+> pred (Succ n) = n+> |])+++--------------------------------------+Definitions used to support singletons+--------------------------------------++Please refer to the paper cited above for a more in-dpeth explanation of these+definitions.+++data family Sing (a :: k)++The data family of singleton types. A new instance of this data family is+generated for every new singleton type.+++class SingI (a :: k) where+ sing :: Sing a++A class used to pass singleton values implicitly. The 'sing' method produces+an explicit singleton value.+++class SingE (a :: k) where+ type Demote a :: *+ fromSing :: Sing a -> Demote (Any :: k)++This class is used to convert a singleton value back to a value in the+original, unrefined ADT. The 'fromSing' method converts, say, a+singleton @Nat@ back to an ordinary @Nat@. The 'Demote' associated+kind-indexed type family maps, for example, types of the kind @Nat@+back to the type @Nat@.+++class (SingI a, SingE a) => SingRep a+instance (SingI a, SingE a) => SingRep a++'SingRep' is a synonym for @('SingI' a, 'SingE' a)@.+++type family (a :: k) :==: (b :: k) :: Bool+type a :== b = a :==: b+type a :/=: b = Not (a :==: b)+type a :/= b = a :/=: b++These are two equivalent forms of Boolean equality and inequality at the type+level. When promoted a datatype that derives @Eq@, instances of this type+family are generated.++data SingInstance (a :: k) where+ SingInstance :: SingRep a => SingInstance a+class (b ~ Any) => SingKind (b :: k) where+ singInstance :: forall (a :: k). Sing a -> SingInstance a++The 'SingKind' class allows for easy access to implicit parameters. The+intuition here is that for any kind @k@ with an associated singleton definition,+@SingKind (Any :: k)@ is defined.+++class (t ~ Any) => SEq (t :: 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)++This is the equivalent of @Eq@ for singletons. It computes singleton Boolean+equality. Alternate spellings of the functions are provided: (%:==) is the+same as (%==%) and (%:/=) is the same as (%/=%). These synonyms are provided+for compatibility with generated code.+++type family If (a :: Bool) (b :: k) (c :: k) :: k++This type family is a Boolean conditional at the type level.+++sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)++This function is a conditional for singletons.+++type family Head (a :: [k]) :: k++Returns the head of a type-level list. Gets stuck when given @'[]@.+++type family Tail (a :: [k]) :: [k]++Returns the tail of a type-level list. Gets stuck when given @'[]@.+++-----------------------+Other utility functions+-----------------------++cases :: Name -- the type of the scrutinee+ -> Q Exp -- the scrutinee+ -> Q Exp -- the body of each branch+ -> Q Exp -- the resulting expression++It is sometimes necessary to get GHC to do case analysis on all possible+types for a given type parameter. No matter what the type variable is, though,+the resulting action is the same. This normally takes the form of a case+statement where every branch has the same expression. The 'cases' function+generates such a case statement. For example,++> $(cases ''Bool [| not foo |] [| doSomething foo |])++expands to++> case not foo of+> True -> doSomething foo+> False -> doSomething foo+++bugInGHC :: forall a. a++Currently, GHC will issue a warning for an incomplete pattern match, even+when all omitted cases can be statically proven to be impossible. For example:++> safePred :: Sing (Succ n) -> Sing n+> safePred (SSucc n) = n++With @-fwarn-incomplete-patterns@ (which we highly recommend using), GHC+warns that the pattern match is incomplete. The solution? Suppress the warning+with a wildcard pattern, using 'bugInGHC':++> safePred _ = bugInGHC++The 'bugInGHC' function just calls @error@ with an appropriate message. +++----------------------+Pre-defined singletons+----------------------++The singletons library defines a number of singleton types and functions+by default:++* @Bool@+* @Maybe@+* @Either@+* @()@+* tuples up to length 7+* @not@, @&&@, @||@+* lists+* @++@++--------+On names+--------++The singletons library has to produce new names for the new constructs it+generates. Here are some examples showing how this is done:++original datatype: Nat+promoted kind: Nat+singleton type: SNat (which is really a synonym for @Sing@)++original datatype: (:/\:)+promoted kind: (:/\:)+singleton type: (:%/\:)++original constructor: Zero+promoted type: 'Zero+singleton constructor: SZero+smart constructor: sZero (see paper cited above for more info)++original constructor: :+:+promoted type: ':+:+singleton constructor: :%+:+smart constructor: %:+:++original value: pred+promoted type: Pred+singleton value: sPred++original value: ++promoted type: :++singleton value: %:++++Special names+-------------++There are some special cases:++original datatype: []+singleton type: SList++original constructor: []+singleton constructor: SNil+smart constructor: sNil++original constructor: :+singleton constructor: SCons+smart constructor: sCons++original datatype: (,)+singleton type: STuple2++original constructor: (,)+singleton constructor: STuple2+smart constructor: sTuple2++All tuples (including the 0-tuple, unit) are treated similarly.++original value: undefined+promoted type: Any+singleton value: undefined+++----------------------------+Supported Haskell constructs+----------------------------++The following constructs are fully supported:++* variables+* tuples+* constructors+* infix expressions+* !, ~, and _ patterns+* aliased patterns (except at top-level)+* lists+* (+) sections+* (x +) sections+* undefined+* deriving Eq++The following constructs will be coming soon:++* unboxed tuples+* records+* scoped type variables+* overlapping patterns+* pattern guards+* (+ x) sections+* case+* let+* list comprehensions++The following constructs are problematic and are not planned to be+implemented:++* literals+* lambda expressions+* do+* arithmetic sequences++See the paper cited above for reasons why these are problematic.+++-------------+Support for *+-------------++The built-in Haskell promotion mechanism does not yet have a full story around+the kind * (the kind of types that have values). Ideally, promoting some form+of TypeRep would yield *, but the implementation of TypeRep would have to be+updated for this to really work out. In the meantime, users who wish to+experiment with this feature have two options:++1) The module Singletons.TypeRepStar has all the definitions possible for+making * the promoted version of TypeRep, as TypeRep is currently implemented.+The singleton associated with TypeRep has one constructor:++> data instance Sing (a :: *) where+> STypeRep :: Typeable a => Sing a++Thus, an implicit TypeRep is stored in the singleton constructor. However,+any datatypes that store TypeReps will not generally work as expected; the+built-in promotion mechanism will not promote TypeRep to *.++2) The module Singletons.CustomStar allows the programmer to define a subset+of types with which to work. A datatype @Rep@ is created, with one constructor+per type in the declared universe. When this type is promoted by the singletons+library, the constructors become full types in *, not just promoted data+constructors. The universe is specified with the @singletonStar@ function.++For example,++> $(singletonStar [''Nat, ''Bool, ''Maybe])++generates the following:++> data Rep = Nat | Bool | Maybe Rep deriving (Eq, Show, Read)++and its singleton. However, because @Rep@ is promoted to @*@, the singleton+is perhaps slightly unexpected:++> data instance Sing (a :: *) where+> SNat :: Sing Nat+> SBool :: Sing Bool+> SMaybe :: SingRep a => Sing a -> Sing (Maybe a)++The expected part is that @Nat@, @Bool@, and @Maybe@ above are the real @Nat@,+@Bool@, and @Maybe@, not just promoted data constructors.+++Please note that support for * is *very* experimental. Use at your own risk.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ Singletons/CustomStar.hs view
@@ -0,0 +1,91 @@+{- Singletons/CustomStar.hs++(c) Richard Eisenbeg 2012+eir@cis.upenn.edu++This file implements singletonStar, which generates a datatype Rep and associated+singleton from a list of types. The promoted version of Rep is kind * and the+Haskell types themselves. This is still very experimental, so expect unusual+results!+-} ++{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}++module Singletons.CustomStar where++import Language.Haskell.TH+import Singletons.Util+import Singletons.Promote+import Singletons.Singletons+import Control.Monad++-- Produce a representation and singleton for the collection of types given+singletonStar :: [Name] -> Q [Dec]+singletonStar names = do+ kinds <- mapM getKind names+ ctors <- zipWithM (mkCtor True) names kinds+ 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 ]+ singletonDecls <- singDataD True [] repName [] fakeCtors+ [mkName "Eq", mkName "Show", mkName "Read"]+ return $ repDecl :+ eqTypeInstances +++ singletonDecls+ where -- get the kinds of the arguments to the tycon with the given name+ getKind :: Name -> Q [Kind]+ getKind name = do+ info <- reifyWithWarning name+ case info of+ TyConI (DataD (_:_) _ _ _ _) ->+ fail "Cannot make a representation of a constrainted data type"+ TyConI (DataD [] _ tvbs _ _) ->+ return $ map extractTvbKind tvbs+ TyConI (NewtypeD (_:_) _ _ _ _) ->+ fail "Cannot make a representation of a constrainted newtype"+ TyConI (NewtypeD [] _ tvbs _ _) ->+ return $ map extractTvbKind tvbs+ TyConI (TySynD _ tvbs _) ->+ return $ map extractTvbKind tvbs+ PrimTyConI _ n _ ->+ return $ replicate n StarT+ _ -> fail $ "Invalid thing for representation: " ++ (show name)+ + -- first parameter is whether this is a real ctor (with a fresh name)+ -- or a fake ctor (when the name is actually a Haskell type)+ mkCtor :: Bool -> Name -> [Kind] -> Q Con+ mkCtor real name args = do+ (types, vars) <- evalForPair $ mapM kindToType args+ let ctor = NormalC ((if real then reinterpret else id) name)+ (map (\ty -> (NotStrict, ty)) types)+ if length vars > 0+ then return $ ForallC (map PlainTV vars) [] ctor+ else return ctor++ -- demote a kind back to a type, accumulating any unbound parameters+ kindToType :: Kind -> QWithAux [Name] Type+ kindToType (ForallT _ _ _) = fail "Explicit forall encountered in kind"+ kindToType (AppT k1 k2) = do+ t1 <- kindToType k1+ t2 <- kindToType k2+ return $ AppT t1 t2+ kindToType (SigT _ _) = fail "Sort signature encountered in kind"+ kindToType (VarT n) = do+ addElement n+ return $ VarT n+ kindToType (ConT n) = return $ ConT n+ kindToType (PromotedT _) = fail "Promoted type used as a kind"+ kindToType (TupleT n) = return $ TupleT n+ kindToType (UnboxedTupleT _) = fail "Unboxed tuple kind encountered"+ kindToType ArrowT = return ArrowT+ kindToType ListT = return ListT+ kindToType (PromotedTupleT _) = fail "Promoted tuple kind encountered"+ kindToType PromotedNilT = fail "Promoted nil kind encountered"+ kindToType PromotedConsT = fail "Promoted cons kind encountered"+ kindToType StarT = return $ ConT repName+ kindToType ConstraintT =+ fail $ "Cannot make a representation of a type that has " +++ "an argument of kind Constraint"+ kindToType (LitT _) = fail "Literal encountered at the kind level"
+ Singletons/Lib.hs view
@@ -0,0 +1,158 @@+{- Singletons/Lib.hs++(c) Richard Eisenberg 2012+eir@cis.upenn.edu++This is the public interface file to the singletons library. Please+see the accompanying README file for more information. Haddock is+not currently compatible with the features used here, so the documentation+is all in the README file and /Dependently typed programming with singletons/,+available at <http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf>+-}++{-# LANGUAGE TypeFamilies, GADTs, KindSignatures, TemplateHaskell,+ DataKinds, PolyKinds, TypeOperators, MultiParamTypeClasses,+ FlexibleContexts, RankNTypes, UndecidableInstances,+ FlexibleInstances, ScopedTypeVariables+ #-}++module Singletons.Lib (+ Any,+ Demote, Sing(..), SingI, sing, SingE, fromSing, SingRep, (:==), (:==:),+ SingInstance(..), SingKind, singInstance,+ sTrue, sFalse, SBool, sNothing, sJust, SMaybe, sLeft, sRight, SEither,+ sTuple0, sTuple2, sTuple3, sTuple4, sTuple5, sTuple6, sTuple7,+ STuple0, STuple2, STuple3, STuple4, STuple5, STuple6, STuple7,+ Not, sNot, (:&&), (%:&&), (:||), (%:||), (:&&:), (:||:), (:/=), (:/=:),+ SEq, (%==%), (%/=%), (%:==), (%:/=),+ If, sIf, + sNil, sCons, SList, (:++), (%:++), Head, Tail,+ cases, bugInGHC,+ genSingletons, singletons, genPromotions, promote,+ ) where++import Prelude hiding ((++))+import Singletons.Singletons+import Singletons.Promote+import Language.Haskell.TH+import GHC.Exts+import Singletons.Util++-- Declarations of singleton structures+data family Sing (a :: k)+class SingI (a :: k) where+ sing :: Sing a+class SingE (a :: k) where+ type Demote a :: *+ fromSing :: Sing a -> Demote (Any :: k)++-- SingRep is a synonym for (SingI, SingE)+class (SingI a, SingE a) => SingRep a+instance (SingI a, SingE a) => SingRep a++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 (b ~ Any) => SingKind (b :: k) where+ singInstance :: forall (a :: k). Sing a -> SingInstance a++-- provide a few useful singletons...+$(genSingletons [''Bool, ''Maybe, ''Either, ''[]])+$(genSingletons [''(), ''(,), ''(,,), ''(,,,), ''(,,,,), ''(,,,,,), ''(,,,,,,)])++-- ... with some functions over Booleans+$(singletons [d|+ not :: Bool -> Bool+ not False = True+ not True = False++ (&&) :: Bool -> Bool -> Bool+ False && a = False+ True && a = a++ (||) :: Bool -> Bool -> Bool+ False || a = a+ True || a = True+ |])++-- symmetric syntax synonyms+type a :&&: b = a :&& b+type a :||: b = a :|| b++type a :/=: b = Not (a :==: b)+type a :/= b = a :/=: b++-- the singleton analogue of @Eq@+class (t ~ Any) => SEq (t :: 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++-- singleton conditional+sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)+sIf STrue b c = b+sIf SFalse b c = c++type instance '[] :==: '[] = True+type instance '[] :==: (h ': t) = False+type instance (h ': t) :==: '[] = False+type instance (h ': t) :==: (h' ': t') = (h :==: h') :&&: (t :==: t')++instance SEq (Any :: k) => SEq (Any :: [k]) where+ SNil %==% SNil = STrue+ SNil %==% (SCons _ _) = SFalse+ (SCons _ _) %==% SNil = SFalse+ (SCons a b) %==% (SCons a' b') = (a %==% a') %:&& (b %==% b')++type family Head (a :: [k]) :: k+type instance Head (h ': t) = h++type family Tail (a :: [k]) :: [k]+type instance Tail (h ': t) = t++-- must handle (++) by hand because of bug in module interface system+-- when kind-polymorphic code is produced by Template Haskell+(++) :: [a] -> [a] -> [a]+[] ++ a = a+(h:t) ++ a = h:(t ++ a)++type family (a :: [k]) :++ (b :: [k]) :: [k]+type instance '[] :++ a = a+type instance (h ': t) :++ a = (h ': (t :++ a))++(%:++) :: Sing a -> Sing b -> Sing (a :++ b)+SNil %:++ a = a+(SCons h t) %:++ a = sCons h (t %:++ a)++-- allows for automatic checking of all constructors in a GADT for instance+-- inference+cases :: Name -> Q Exp -> Q Exp -> Q Exp+cases tyName expq bodyq = do+ info <- reifyWithWarning tyName+ case info of+ TyConI (DataD _ _ _ ctors _) -> buildCases ctors+ TyConI (NewtypeD _ _ _ ctor _) -> buildCases [ctor]+ _ -> fail $ "Using <<cases>> with something other than a type constructor: "+ ++ (show tyName)+ where buildCases :: [Con] -> Q Exp+ buildCases ctors =+ caseE expq (map ((flip (flip match (normalB bodyq)) []) . conToPat) ctors)++ conToPat :: Con -> Q Pat+ conToPat = ctor1Case+ (\name tys -> conP name (replicate (length tys) wildP))++-- useful when suppressing GHC's warnings about incomplete pattern matches+bugInGHC :: forall a. a+bugInGHC = error "Bug encountered in GHC -- this should never happen"
+ Singletons/Promote.hs view
@@ -0,0 +1,544 @@+{- Singletons/Promote.hs++(c) Richard Eisenberg 2012+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.+-}++{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}++module Singletons.Promote where++import Language.Haskell.TH+import Singletons.Util+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 Data.List++anyTypeName, falseName, trueName, andName, tyEqName, repName, ifName,+ headName, tailName :: Name+anyTypeName = mkName "Any"+falseName = mkName "False"+trueName = mkName "True"+andName = mkName "&&"+tyEqName = mkName ":==:"+repName = mkName "Rep"+ifName = mkName "If"+headName = mkName "Head"+tailName = mkName "Tail"++falseTy :: Type+falseTy = promoteDataCon falseName++trueTy :: Type+trueTy = promoteDataCon trueName++andTy :: Type+andTy = promoteVal andName++ifTyFam :: Type+ifTyFam = ConT ifName++headTyFam :: Type+headTyFam = ConT headName++tailTyFam :: Type+tailTyFam = ConT tailName++genPromotions :: [Name] -> Q [Dec]+genPromotions names = do+ checkForRep names+ infos <- mapM reifyWithWarning names+ decls <- mapM promoteInfo infos+ return $ concat decls++promoteInfo :: Info -> Q [Dec]+promoteInfo (ClassI dec instances) =+ fail "Promotion of class info not supported"+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) =+ fail "Promotion of type family info not yet supported" -- KindFams+promoteInfo (PrimTyConI name numArgs unlifted) =+ fail "Promotion of primitive type constructors not supported"+promoteInfo (DataConI name ty tyname fixity) =+ fail $ "Promotion of individual constructors not supported; " +++ "promote the type instead"+promoteInfo (VarI name ty mdec fixity) =+ fail "Promotion of value info not supported"+promoteInfo (TyVarI name ty) =+ fail "Promotion of type variable info not supported"++promoteDataCon :: Name -> Type+promoteDataCon name =+ if isTupleName name+ then PromotedTupleT (tupleDegree $ nameBase name)+ else PromotedT name++promoteValName :: Name -> Name+promoteValName n+ | nameBase n == "undefined" = anyTypeName+ | otherwise = upcase n++promoteVal :: Name -> Type+promoteVal = ConT . promoteValName++promoteType :: Type -> Q Kind+promoteType (ForallT tvbs [] ty) = promoteType ty -- ForallKinds+promoteType (ForallT _ (_:_) _) = fail "Cannot promote type with constrained variables"+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 ArrowT = return ArrowT+promoteType ListT = return ListT+promoteType (AppT (AppT ArrowT (ForallT (_:_) _ _)) _) =+ fail "Cannot promote types of rank above 1."+promoteType (AppT ty1 ty2) = do+ k1 <- promoteType ty1+ k2 <- promoteType ty2+ return $ AppT k1 k2+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"+promoteType PromotedNilT = fail "Cannot promote a nil that is already promoted"+promoteType PromotedConsT = fail "Cannot promote a cons that is already promoted"+promoteType StarT = fail "* used as a type"+promoteType ConstraintT = fail "Constraint used as a type"++-- a table to keep track of variable->type mappings+type TypeTable = Map.Map Name Type++-- Promote each declaration in a splice+promote :: Q [Dec] -> Q [Dec]+promote qdec = do+ decls <- qdec+ (promDecls, _) <- promoteDecs decls+ return $ decls ++ promDecls++checkForRep :: [Name] -> Q ()+checkForRep names =+ when (any ((== nameBase repName) . nameBase) names)+ (fail $ "A data type named <<Rep>> is a special case.\n" +++ "Promoting it will not work as expected.\n" +++ "Please choose another name for your data type.")++checkForRepInDecls :: [Dec] -> Q ()+checkForRepInDecls decls =+ checkForRep (map extractNameFromDec decls)+ where extractNameFromDec :: Dec -> Name+ extractNameFromDec (DataD _ name _ _ _) = name+ extractNameFromDec (NewtypeD _ name _ _ _) = name+ extractNameFromDec (TySynD name _ _) = name+ extractNameFromDec (FamilyD _ name _ _) = name+ extractNameFromDec _ = mkName "NotRep"++-- Promote a list of declarations; returns the promoted declarations+-- and a list of names of declarations without accompanying type signatures.+-- (This list is needed by singletons to strike such definitions.)++-- Promoting declarations proceeds in two stages:+-- 1) Promote everything except type signatures+-- 2) Promote type signatures. This must be done in a second pass because+-- a function type signature gets promoted to a type family declaration.+-- Although function signatures do not differentiate between uniform parameters+-- and non-uniform parameters, type family declarations do. We need+-- to process a function's definition to get the count of non-uniform+-- parameters before producing the type family declaration.+-- At this point, any function written without a type signature is rejected+-- and removed.+promoteDecs :: [Dec] -> Q ([Dec], [Name])+promoteDecs decls = do+ checkForRepInDecls decls+ let vartbl = Map.empty+ (newDecls, numArgsTable) <- evalForPair $ mapM (promoteDec vartbl) decls+ (declss, namess) <- mapAndUnzipM (promoteDec' numArgsTable) decls+ let moreNewDecls = concat declss+ names = concat namess+ noTypeSigs = Set.toList $ Set.difference (Map.keysSet $+ Map.filter (>= 0) numArgsTable)+ (Set.fromList names)+ noTypeSigsPro = map promoteValName noTypeSigs+ newDecls' = foldl (\decls name ->+ filter (not . (containsName name)) decls)+ (concat newDecls) (noTypeSigs ++ noTypeSigsPro)+ mapM_ (\n -> report False $ "No type binding for " ++ (show (nameBase n)) +++ "; removing all declarations including it")+ 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+ tyAll [] = trueTy+ tyAll [one] = one+ tyAll (h:t) = foldType andTy [h, (tyAll t)]++-- keeps track of the number of non-uniform parameters to promoted values+type NumArgsTable = Map.Map Name Int+type NumArgsQ = QWithAux NumArgsTable++-- used when a type is declared as a type synonym, not a type family+-- no need to declare "type family ..." for these+typeSynonymFlag :: Int+typeSynonymFlag = -1++promoteDec :: TypeTable -> Dec -> NumArgsQ [Dec]+promoteDec vars (FunD name clauses) = do+ let proName = promoteValName name+ 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+ addBinding name numArgs -- remember the number of parameters+ return $ concat instDecls+ where getNumPats :: Clause -> Int+ getNumPats (Clause pats _ _) = length pats+promoteDec vars (ValD pat body decs) = do+ -- see also the comment for promoteTopLevelPat+ when (length decs > 0)+ (fail $ "Promotion of global variable with <<where>> clause " +++ "not yet supported")+ (rhs, decls) <- lift $ evalForPair $ promoteBody vars body+ (lhss, decls') <- lift $ evalForPair $ promoteTopLevelPat pat+ 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) +++ decls ++ decls'+ else do -- definition is not recursive; just use "type" decls+ mapM (flip addBinding typeSynonymFlag) (map lhsRawName lhss)+ return $ (map (\(LHS _ nm hole) -> TySynD nm [] (hole rhs)) lhss) +++ decls ++ decls'+promoteDec vars (DataD cxt name tvbs ctors derivings) = + 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) =+ fail "Promotion of type synonym declaration not yet supported"+promoteDec vars (ClassD cxt name tvbs fundeps decs) =+ fail "Promotion of class declaration not yet supported"+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) =+ fail "Promotion of foreign function declaration not yet supported"+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) =+ fail "Promotion of pragmas not yet supported"+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) =+ fail "Promotion of data instances not yet supported"+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)"++-- 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 =+ if any (\n -> (nameBase n) == "Eq") derivings+ then do+ let pairs = [ (c1, c2) | c1 <- ctors, c2 <- ctors ]+ lift $ mapM mkEqTypeInstance pairs+ else return [] -- the actual promotion is automatic++-- second pass through declarations to deal with type signatures+-- returns the new declarations and the list of names that have been+-- processed+promoteDec' :: NumArgsTable -> Dec -> Q ([Dec], [Name])+promoteDec' nat (SigD name ty) = case Map.lookup name nat of+ Nothing -> fail $ "Type declaration is missing its binding: " ++ (show name)+ Just numArgs -> + -- if there are no args, then use a type synonym, not a type family+ -- in the type synonym case, we ignore the type signature+ if numArgs == typeSynonymFlag then return $ ([], [name]) else do + k <- promoteType ty+ let ks = unravel k+ (argKs, resultKs) = splitAt numArgs ks -- divide by uniformity+ resultK <- ravel resultKs -- rebuild the arrow kind+ tyvarNames <- mapM newName (replicate (length argKs) "a")+ return ([FamilyD TypeFam+ (promoteValName name)+ (zipWith KindedTV tyvarNames argKs)+ (Just resultK)], [name])+ where unravel :: Kind -> [Kind] -- get argument kinds from an arrow kind+ unravel (AppT (AppT ArrowT k1) k2) =+ let ks = unravel k2 in k1 : ks+ unravel k = [k]+ + ravel :: [Kind] -> Q Kind+ ravel [] = fail "Internal error: raveling nil"+ ravel [k] = return k+ ravel (h:t) = do+ k <- ravel t+ return $ (AppT (AppT ArrowT h) k)+promoteDec' _ _ = return ([], [])++promoteClause :: TypeTable -> Name -> Clause -> Q [Dec]+promoteClause vars name (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+ let vars' = Map.union vars vartbl+ (ty, decls) <- evalForPair $ promoteBody vars' body+ return $ decls ++ [TySynInstD name 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"+-- the hole is filled in by the RHS+data TopLevelLHS = LHS { lhsRawName :: Name -- the unpromoted name+ , lhsName :: Name+ , lhsHole :: Type -> Type+ }++-- Treatment of top-level patterns is different from other patterns+-- because type families have type patterns as their LHS. However,+-- it is not possible to use type patterns at the top level, so we+-- have to use other techniques.+promoteTopLevelPat :: Pat -> QWithDecs [TopLevelLHS]+promoteTopLevelPat (LitP _) = fail "Cannot declare a global literal."+promoteTopLevelPat (VarP name) = return [LHS name (promoteValName name) id]+promoteTopLevelPat (TupP pats) = case length pats of+ 0 -> return [] -- unit as LHS of pattern... ignore+ 1 -> fail "1-tuple encountered during top-level pattern promotion"+ n -> promoteTopLevelPat (ConP (tupleDataName n) pats)+promoteTopLevelPat (UnboxedTupP _) =+ fail "Promotion of unboxed tuples not supported"++-- to promote a constructor pattern, we need to create extraction type+-- families to pull out the individual arguments of the constructor+promoteTopLevelPat (ConP name pats) = do+ ctorInfo <- lift $ reifyWithWarning name+ (ctorType, argTypes) <- lift $ extractTypes ctorInfo+ when (length argTypes /= length pats) $+ fail $ "Inconsistent data constructor pattern: " ++ (show name) ++ " " +++ (show pats)+ kind <- lift $ promoteType ctorType+ argKinds <- lift $ mapM promoteType argTypes+ extractorNamesRaw <- lift $ replicateM (length pats) (newName "Extract")++ -- TH doesn't allow "newName"s to work at the top-level, so we have to+ -- do this trick to ensure the Extract functions are unique+ let extractorNames = map (mkName . show) extractorNamesRaw+ varName <- lift $ newName "a"+ zipWithM (\nm arg -> addElement $ FamilyD TypeFam+ nm+ [KindedTV varName kind]+ (Just arg))+ extractorNames argKinds+ componentNames <- lift $ replicateM (length pats) (newName "a")+ zipWithM (\extractorName componentName ->+ addElement $ TySynInstD extractorName+ [foldType (promoteDataCon name)+ (map VarT componentNames)]+ (VarT componentName))+ extractorNames componentNames++ -- now we have the extractor families. Use the appropriate families+ -- in the "holes"+ promotedPats <- mapM promoteTopLevelPat pats+ return $ concat $+ zipWith (\lhslist extractor ->+ map (\(LHS raw nm hole) -> LHS raw nm+ (hole . (AppT (ConT extractor))))+ lhslist)+ promotedPats extractorNames+ where extractTypes :: Info -> Q (Type, [Type])+ extractTypes (DataConI datacon _dataconTy tyname _fixity) = do+ tyinfo <- reifyWithWarning tyname+ extractTypesHelper datacon tyinfo+ extractTypes _ = fail "Internal error: unexpected Info in extractTypes"+ + extractTypesHelper :: Name -> Info -> Q (Type, [Type])+ extractTypesHelper datacon+ (TyConI (DataD _cxt tyname tvbs cons _derivs)) =+ let mcon = find ((== datacon) . fst . extractNameArgs) cons in+ case mcon of+ Nothing -> fail $ "Internal error reifying " ++ (show datacon)+ Just con -> return (foldType (ConT tyname)+ (map (VarT . extractTvbName) tvbs),+ extractConArgs con)+ extractTypesHelper datacon+ (TyConI (NewtypeD cxt tyname tvbs con derivs)) =+ extractTypesHelper datacon (TyConI (DataD cxt tyname tvbs [con] derivs))+ extractTypesHelper datacon _ =+ fail $ "Cannot promote data constructor " ++ (show datacon)++ extractConArgs :: Con -> [Type]+ extractConArgs = ctor1Case (\_ tys -> tys)+promoteTopLevelPat (InfixP l name r) = promoteTopLevelPat (ConP name [l, r])+promoteTopLevelPat (UInfixP _ _ _) =+ fail "Unresolved infix constructors not supported"+promoteTopLevelPat (ParensP _) = + fail "Unresolved infix constructors not supported"+promoteTopLevelPat (TildeP pat) = do+ lift $ report False "Lazy pattern converted into regular pattern in promotion"+ promoteTopLevelPat pat+promoteTopLevelPat (BangP pat) = do+ lift $ report False "Strict pattern converted into regular pattern in promotion"+ promoteTopLevelPat pat+promoteTopLevelPat (AsP name pat) =+ fail "Promotion of aliased patterns at top level not yet supported"+promoteTopLevelPat WildP = return []+promoteTopLevelPat (RecP _ _) =+ fail "Promotion of record patterns at top level not yet supported"++-- must do a similar trick as what is in the ConP case, but this is easier+-- because Lib defined Head and Tail+promoteTopLevelPat (ListP pats) = do+ promotedPats <- mapM promoteTopLevelPat pats+ return $ concat $ snd $+ mapAccumL (\extractFn lhss ->+ ((AppT tailTyFam) . extractFn,+ map (\(LHS raw nm hole) ->+ LHS raw nm (hole . (AppT headTyFam) . extractFn)) lhss))+ id promotedPats+promoteTopLevelPat (SigP pat _) = do+ lift $ report False $ "Promotion of explicit type annotation in pattern " +++ "not yet supported."+ promoteTopLevelPat pat+promoteTopLevelPat (ViewP _ _) =+ fail "Promotion of view patterns not yet supported"++type TypesQ = QWithAux TypeTable++-- promotes a term pattern into a type pattern, accumulating variable+-- binding in the auxiliary TypeTable+promotePat :: Pat -> TypesQ Type+promotePat (LitP lit) = fail $ "Promoting literals not supported: " ++ (show lit)+promotePat (VarP name) = do+ tyVar <- lift $ newName (nameBase name)+ addBinding name (VarT tyVar)+ return $ VarT tyVar+promotePat (TupP pats) = do+ types <- mapM promotePat pats+ let baseTup = PromotedTupleT (length types)+ tup = foldType baseTup types+ return tup+promotePat (UnboxedTupP _) = fail "Unboxed tuples not supported"+promotePat (ConP name pats) = do+ types <- mapM promotePat pats+ let tyCon = foldType (promoteDataCon name) types+ return tyCon+promotePat (InfixP pat1 name pat2) = promotePat (ConP name [pat1, pat2])+promotePat (UInfixP _ _ _) = fail "Unresolved infix constructions not supported"+promotePat (ParensP _) = fail "Unresolved infix constructions not supported"+promotePat (TildeP pat) = do+ lift $ report False "Lazy pattern converted into regular pattern in promotion"+ promotePat pat+promotePat (BangP pat) = do+ lift $ report False "Strict pattern converted into regular pattern in promotion"+ promotePat pat+promotePat (AsP name pat) = do+ ty <- promotePat pat+ addBinding name ty+ return ty+promotePat WildP = do+ name <- lift $ newName "z"+ return $ VarT name+promotePat (RecP _ _) = fail "Promotion of record patterns not yet supported"+promotePat (ListP pats) = do+ types <- mapM promotePat pats+ return $ foldr (\h t -> AppT (AppT PromotedConsT h) t) PromotedNilT types+promotePat (SigP pat _) = do+ lift $ report False $ "Promotion of explicit type annotation in pattern " +++ "not yet supported"+ promotePat pat+promotePat (ViewP _ _) = fail "View patterns not yet supported"++-- promoting a body may produce auxiliary declarations. Accumulate these.+type QWithDecs = QWithAux [Dec]++promoteBody :: TypeTable -> Body -> QWithDecs Type+promoteBody vars (NormalB exp) = promoteExp vars exp+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 (AppE exp1 exp2) = do+ ty1 <- promoteExp vars exp1+ ty2 <- promoteExp vars exp2+ return $ AppT ty1 ty2+promoteExp vars (InfixE mexp1 exp mexp2) =+ case (mexp1, mexp2) of+ (Nothing, Nothing) -> promoteExp vars exp+ (Just exp1, Nothing) -> promoteExp vars (AppE exp exp1)+ (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 _ _ _) =+ fail "Promotion of unresolved infix operators not supported"+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 (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 (CondE bexp texp fexp) = do+ tys <- mapM (promoteExp vars) [bexp, texp, fexp]+ return $ foldType ifTyFam tys+promoteExp vars (LetE decs exp) =+ fail "Promotion of let statements not yet supported"+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) =+ fail "Promotion of list comprehensions not yet 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) =+ fail "Promotion of explicit type annotations not yet supported"+promoteExp vars (RecConE name fields) =+ fail "Promotion of record construction not yet supported"+promoteExp vars (RecUpdE exp fields) =+ fail "Promotion of record updates not yet supported"
+ Singletons/Singletons.hs view
@@ -0,0 +1,599 @@+{- Singletons/Singletons.hs++(c) Richard Eisenberg 2012+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.+-}++{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}++module Singletons.Singletons where++import Language.Haskell.TH.Lib+import Language.Haskell.TH.Syntax hiding (lift)+import Singletons.Util+import Singletons.Promote+import qualified Data.Map as Map+import Control.Monad+import Control.Monad.Writer+import Data.List++-- map to track bound variables+type ExpTable = Map.Map Name Exp++-- translating a type gives a type with a hole in it,+-- represented here as a function+type TypeFn = Type -> Type++-- a list of argument types extracted from a type application+type TypeContext = [Type]++singFamilyName, isSingletonName, forgettableName, comboClassName, witnessName,+ demoteName, singKindClassName, singInstanceMethName, singInstanceName,+ sEqClassName, sEqMethName, sconsName, snilName, smartSconsName,+ smartSnilName, sIfName, undefinedName :: Name+singFamilyName = mkName "Sing"+isSingletonName = mkName "SingI"+forgettableName = mkName "SingE"+comboClassName = mkName "SingRep"+witnessName = mkName "sing"+forgetName = mkName "fromSing"+demoteName = mkName "Demote"+singKindClassName = mkName "SingKind"+singInstanceMethName = mkName "singInstance"+singInstanceName = mkName "SingInstance"+sEqClassName = mkName "SEq"+sEqMethName = mkName "%==%"+sconsName = mkName "SCons"+snilName = mkName "SNil"+smartSconsName = mkName "sCons"+smartSnilName = mkName "sNil"+sIfName = mkName "sIf"+undefinedName = mkName "undefined"++mkTupleName :: Int -> Name+mkTupleName n = mkName $ "STuple" ++ (show n)++singFamily :: Type+singFamily = ConT singFamilyName++singKindConstraint :: Kind -> Pred+singKindConstraint k = ClassP singKindClassName [SigT anyType k]++singInstanceMeth :: Exp+singInstanceMeth = VarE singInstanceMethName++singInstanceTyCon :: Type+singInstanceTyCon = ConT singInstanceName++singInstanceDataCon :: Exp+singInstanceDataCon = ConE singInstanceName++singInstancePat :: Pat+singInstancePat = ConP singInstanceName []++demote :: Type+demote = ConT demoteName++anyType :: Type+anyType = ConT anyTypeName++singDataConName :: Name -> Name+singDataConName nm = case nameBase nm of+ "[]" -> snilName+ ":" -> sconsName+ tuple | isTupleString tuple -> mkTupleName (tupleDegree tuple)+ _ -> prefixUCName "S" ":%" nm++singTyConName :: Name -> Name+singTyConName name | nameBase name == "[]" = mkName "SList"+ | isTupleName name = mkTupleName (tupleDegree $ nameBase name)+ | otherwise = prefixUCName "S" ":%" name++singDataCon :: Name -> Exp+singDataCon = ConE . singDataConName++smartConName :: Name -> Name+smartConName = locase . singDataConName++smartCon :: Name -> Exp+smartCon = VarE . smartConName++singValName :: Name -> Name+singValName n+ | nameBase n == "undefined" = undefinedName+ | otherwise = (prefixLCName "s" "%") $ upcase n++singVal :: Name -> Exp+singVal = VarE . singValName++-- generate singleton definitions from an ADT+genSingletons :: [Name] -> Q [Dec]+genSingletons names = do+ checkForRep names+ infos <- mapM reifyWithWarning names+ decls <- mapM singInfo infos+ return $ concat decls++singInfo :: Info -> Q [Dec]+singInfo (ClassI dec instances) =+ fail "Singling of class info not supported"+singInfo (ClassOpI name ty className fixity) =+ fail "Singling of class members info not supported"+singInfo (TyConI dec) = singDec dec+singInfo (FamilyI dec instances) =+ fail "Singling of type family info not yet supported" -- KindFams+singInfo (PrimTyConI name numArgs unlifted) =+ fail "Singling of primitive type constructors not supported"+singInfo (DataConI name ty tyname fixity) =+ fail $ "Singling of individual constructors not supported; " +++ "single the type instead"+singInfo (VarI name ty mdec fixity) =+ fail "Singling of value info not supported"+singInfo (TyVarI name ty) =+ fail "Singling of type variable info not supported"++-- refine a constructor. the first parameter is the type variable that+-- the singleton GADT is parameterized by+-- runs in the QWithDecs monad because auxiliary declarations are produced+singCtor :: Type -> Con -> QWithDecs Con +singCtor a = ctorCases+ (\name types -> do+ let sName = singDataConName name+ sCon = singDataCon name+ pCon = promoteDataCon name+ indexNames <- lift $ replicateM (length types) (newName "n")+ let indices = map VarT indexNames+ kinds <- lift $ mapM promoteType types+ args <- lift $ buildArgTypes types indices+ let tvbs = zipWith KindedTV indexNames kinds+ bareKindVars = filter isVarK kinds++ -- SingI instance+ addElement $ InstanceD ((map singKindConstraint bareKindVars) +++ (map (ClassP comboClassName . return) indices))+ (AppT (ConT isSingletonName)+ (foldType pCon (zipWith SigT indices kinds)))+ [ValD (VarP witnessName)+ (NormalB $ foldExp sCon (replicate (length types)+ (VarE witnessName)))+ []]++ -- smart constructor type signature+ smartConType <- lift $ conTypesToFunType indexNames args kinds+ (AppT singFamily (foldType pCon indices))+ addElement $ SigD (smartConName name) smartConType+ + -- smart constructor+ let vars = map VarE indexNames+ smartConBody = mkSingInstances vars (foldExp (singDataCon name) vars)+ addElement $ FunD (smartConName name)+ [Clause (map VarP indexNames)+ (NormalB smartConBody)+ []]++ return $ ForallC tvbs+ ((EqualP a (foldType (promoteDataCon name) indices)) :+ (map (ClassP comboClassName . return) indices) +++ (map singKindConstraint bareKindVars))+ (NormalC sName $ map (\ty -> (NotStrict,ty)) args))+ (\tvbs cxt ctor -> case cxt of+ _:_ -> fail "Singling of constrained constructors not yet supported"+ [] -> singCtor a ctor)+ where buildArgTypes :: [Type] -> [Type] -> Q [Type]+ buildArgTypes types indices = do+ typeFns <- mapM (singType False) types+ return $ zipWith id typeFns indices++ conTypesToFunType :: [Name] -> [Type] -> [Kind] -> Type -> Q Type+ conTypesToFunType [] [] [] ret = return ret+ conTypesToFunType (nm : nmtail) (ty : tytail) (k : ktail) ret = do+ rhs <- conTypesToFunType nmtail tytail ktail ret + let innerty = AppT (AppT ArrowT ty) rhs+ return $ ForallT [KindedTV nm k]+ (if isVarK k then [singKindConstraint k] else [])+ innerty+ conTypesToFunType _ _ _ _ =+ fail "Internal error in conTypesToFunType"++ mkSingInstances :: [Exp] -> Exp -> Exp+ mkSingInstances [] exp = exp+ mkSingInstances (var:tail) exp =+ CaseE (AppE singInstanceMeth var)+ [Match singInstancePat (NormalB $ mkSingInstances tail exp) []]++-- refine the declarations given+singletons :: Q [Dec] -> Q [Dec]+singletons qdec = do+ decls <- qdec+ singDecs decls++singDecs :: [Dec] -> Q [Dec]+singDecs decls = do+ (promDecls, badNames) <- promoteDecs decls+ -- need to remove the bad names returned from promoteDecs+ newDecls <- mapM singDec+ (filter (\dec ->+ not $ or (map (\f -> f dec)+ (map containsName badNames))) decls)+ return $ decls ++ promDecls ++ (concat newDecls)++singDec :: Dec -> Q [Dec]+singDec (FunD name clauses) = do+ let sName = singValName name+ vars = Map.singleton name (VarE sName)+ liftM return $ funD sName (map (singClause vars) clauses)+singDec (ValD _ (GuardedB _) _) =+ fail "Singling of definitions of values with a pattern guard not yet supported"+singDec (ValD _ _ (_:_)) =+ fail "Singling of definitions of values with a <<where>> clause not yet supported"+singDec (ValD pat (NormalB exp) []) = do+ (sPat, vartbl) <- evalForPair $ singPat TopLevel pat+ sExp <- singExp vartbl exp+ return [ValD sPat (NormalB sExp) []]+singDec (DataD (_:_) _ _ _ _) =+ fail "Singling of constrained datatypes not supported"+singDec (DataD cxt name tvbs ctors derivings) =+ 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) =+ fail "Singling of type synonyms not yet supported"+singDec (ClassD cxt name tvbs fundeps decs) =+ fail "Singling of class declaration not yet supported"+singDec (InstanceD cxt ty decs) =+ fail "Singling of class instance not yet supported"+singDec (SigD name ty) = do+ tyTrans <- singType True ty+ return [SigD (singValName name) (tyTrans (promoteVal name))]+singDec (ForeignD fgn) =+ let name = extractName fgn in do+ report False $ "Singling of foreign functions not supported -- " +++ (show name) ++ " ignored"+ return []+ where extractName :: Foreign -> Name+ extractName (ImportF _ _ _ n _) = n+ extractName (ExportF _ _ n _) = n+singDec (InfixD fixity name)+ | isUpcase name = return [InfixD fixity (singDataConName name)]+ | otherwise = return [InfixD fixity (singValName name)]+singDec (PragmaD prag) =+ let name = extractName prag in do+ report False $ "Singling of pragmas not supported -- " +++ (show name) ++ " ignored"+ return []+ where extractName :: Pragma -> Name+ extractName (InlineP n _) = n+ extractName (SpecialiseP n _ _) = n+singDec (FamilyD flavour name tvbs mkind) =+ fail "Singling of type and data families not yet supported"+singDec (DataInstD cxt name tys ctors derivings) = + fail "Singling of data instances not yet supported"+singDec (NewtypeInstD cxt name tys ctor derivings) =+ fail "Singling of newtype instances not yet supported"+singDec (TySynInstD name tys ty) =+ fail "Singling of type family instances not yet supported"++-- 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+ aName <- newName "a"+ let a = VarT aName+ let tvbNames = map extractTvbName tvbs+ k <- promoteType (foldType (ConT name) (map VarT tvbNames))+ (ctors', ctorInstDecls) <- evalForPair $ mapM (singCtor a) ctors+ + -- instance for SingKind+ let singKindInst =+ InstanceD []+ (AppT (ConT singKindClassName)+ (SigT anyType k))+ [FunD singInstanceMethName+ (map mkSingInstanceClause ctors')]+ + -- SEq instance+ let ctorPairs = [ (c1, c2) | c1 <- ctors', c2 <- ctors' ]+ sEqMethClauses <- mapM mkEqMethClause ctorPairs+ let sEqInst =+ InstanceD (map (\k -> ClassP sEqClassName [SigT anyType k])+ (getBareKinds ctors'))+ (AppT (ConT sEqClassName)+ (SigT anyType k))+ [FunD sEqMethName sEqMethClauses]+ + -- e.g. type SNat (a :: Nat) = Sing a+ let kindedSynInst =+ TySynD (singTyConName name)+ [KindedTV aName k]+ (AppT singFamily a)++ -- SingE instance+ forgetClauses <- mapM mkForgetClause ctors+ let singEInst =+ InstanceD []+ (AppT (ConT forgettableName) (SigT a k))+ [TySynInstD demoteName [a]+ (foldType (ConT name)+ (map (\kv -> AppT demote (SigT anyType (VarT kv)))+ tvbNames)),+ FunD forgetName+ forgetClauses]++ return $ (if (any (\n -> (nameBase n) == "Eq") derivings)+ then (sEqInst :)+ else id) $+ (DataInstD [] singFamilyName [SigT a k] ctors' []) :+ singEInst :+ kindedSynInst :+ singKindInst :+ ctorInstDecls+ where mkSingInstanceClause :: Con -> Clause+ mkSingInstanceClause = ctor1Case+ (\nm tys ->+ 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+ varNames <- replicateM numArgs (newName "a")+ return $ Clause [ConP (singDataConName name) (map VarP varNames)]+ (NormalB $ foldExp+ (ConE $ (if rep then reinterpret else id) name)+ (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"+singKind (VarT _) = fail "Singling of kind variables not yet supported"+singKind (ConT _) = fail "Singling of named kinds not yet supported"+singKind (TupleT _) = fail "Singling of tuple kinds not yet supported"+singKind (UnboxedTupleT _) = fail "Unboxed tuple used as kind"+singKind ArrowT = fail "Singling of unsaturated arrow kinds not yet supported"+singKind ListT = fail "Singling of list kinds not yet supported"+singKind (AppT (AppT ArrowT k1) k2) = do+ k1fn <- singKind k1+ k2fn <- singKind k2+ k <- newName "k"+ return $ \f -> AppT (AppT ArrowT (k1fn (VarT k))) (k2fn (AppT f (VarT k)))+singKind (AppT _ _) = fail "Singling of kind applications not yet supported"+singKind (SigT _ _) =+ fail "Singling of explicitly annotated kinds not yet supported"+singKind (LitT _) = fail "Type literal used as kind"+singKind (PromotedT _) = fail "Promoted data constructor used as kind"+singKind (PromotedTupleT _) = fail "Promoted tuple used as kind"+singKind PromotedNilT = fail "Promoted nil used as kind"+singKind PromotedConsT = fail "Promoted cons used as kind"+singKind StarT = return $ \k -> AppT (AppT ArrowT k) StarT+singKind ConstraintT = fail "Singling of constraint kinds not yet supported"++-- the first parameter is whether or not this type occurs in a positive position+singType :: Bool -> Type -> Q TypeFn+singType = singTypeRec []++-- 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 _ _ _) =+ 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 _) =+ fail "Singling of type variables of arrow kinds not yet supported"+singTypeRec [] pos (VarT name) = + return $ \ty -> AppT singFamily ty+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+ return $ \ty -> AppT singFamily ty+singTypeRec ctx pos (UnboxedTupleT n) =+ fail "Singling of unboxed tuple types not yet supported"+singTypeRec ctx pos ArrowT = case ctx of+ [ty1, ty2] -> do+ t <- newName "t"+ sty1 <- singTypeRec [] (not pos) ty1+ sty2 <- singTypeRec [] pos ty2+ k1 <- promoteType ty1+ -- need a SingKind constraint on all kind variables that appear+ -- outside of any kind constructor in a negative position (to the+ -- left of an odd number of arrows)+ let polykinds = extractPolyKinds (not pos) k1+ return (\f -> ForallT [KindedTV t k1]+ (map (\k -> ClassP singKindClassName [SigT anyType k]) polykinds)+ (AppT (AppT ArrowT (sty1 (VarT t)))+ (sty2 (AppT f (VarT t)))))+ where extractPolyKinds :: Bool -> Kind -> [Kind]+ extractPolyKinds pos (AppT (AppT ArrowT k1) k2) =+ (extractPolyKinds (not pos) k1) ++ (extractPolyKinds pos k2)+ extractPolyKinds False (VarT k) = [VarT k]+ extractPolyKinds _ _ = []+ _ -> fail "Internal error in Sing: converting ArrowT with improper context"+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) =+ 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 _) =+ fail "Singling of promoted data constructors not yet supported"+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"++singClause :: ExpTable -> Clause -> Q Clause+singClause vars (Clause pats (NormalB exp) []) = do+ (sPats, vartbl) <- evalForPair $ mapM (singPat Parameter) pats+ let vars' = Map.union vartbl vars+ sBody <- normalB $ singExp vars' exp+ return $ Clause sPats sBody []+singClause _ (Clause _ (GuardedB _) _) =+ fail "Singling of guarded patterns not yet supported"+singClause _ (Clause _ _ (_:_)) =+ fail "Singling of <<where>> declarations not yet supported"++type ExpsQ = QWithAux ExpTable++-- we need to know where a pattern is to anticipate when+-- GHC's brain might explode+data PatternContext = LetBinding+ | CaseStatement+ | TopLevel+ | Parameter+ | Statement+ deriving Eq++checkIfBrainWillExplode :: PatternContext -> ExpsQ ()+checkIfBrainWillExplode CaseStatement = return ()+checkIfBrainWillExplode Statement = return ()+checkIfBrainWillExplode Parameter = return ()+checkIfBrainWillExplode _ =+ fail $ "Can't use a singleton pattern outside of a case-statement or\n" +++ "do expression: GHC's brain will explode if you try. (Do try it!)"++-- convert a pattern, building up the lexical scope as we go+singPat :: PatternContext -> Pat -> ExpsQ Pat+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+ addBinding name (VarE newName)+ return $ VarP newName+singPat patCxt (TupP pats) =+ singPat patCxt (ConP (tupleDataName (length pats)) 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 _ _ _) =+ fail "Singling of unresolved infix patterns not supported"+singPat patCxt (ParensP _) =+ fail "Singling of unresolved paren patterns not supported"+singPat patCxt (TildeP pat) = do+ pat' <- singPat patCxt pat+ return $ TildeP pat'+singPat patCxt (BangP pat) = do+ pat' <- singPat patCxt pat+ return $ BangP pat'+singPat patCxt (AsP name pat) = do+ let newName = if patCxt == TopLevel then singValName name else name in do+ pat' <- singPat patCxt pat+ addBinding name (VarE newName)+ return $ AsP name pat'+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) =+ fail "Singling of annotated patterns not yet supported"+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) =+ fail "Singling of literal expressions not yet supported"+singExp vars (AppE exp1 exp2) = do+ exp1' <- singExp vars exp1+ exp2' <- singExp vars exp2+ return $ AppE exp1' exp2'+singExp vars (InfixE mexp1 exp mexp2) =+ case (mexp1, mexp2) of+ (Nothing, Nothing) -> singExp vars exp+ (Just exp1, Nothing) -> singExp vars (AppE exp exp1)+ (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 _ _ _) =+ fail "Singling of unresolved infix expressions not supported"+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 (TupE exps) = do+ sExps <- mapM (singExp vars) exps+ sTuple <- singExp vars (ConE (tupleDataName (length exps)))+ return $ foldExp sTuple sExps+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 (LetE decs exp) =+ fail "Singling of let expressions not yet supported"+singExp vars (CaseE exp matches) =+ fail "Singling of case expressions not yet supported"+singExp vars (DoE stmts) =+ fail "Singling of do expressions not yet supported"+singExp vars (CompE stmts) =+ fail "Singling of list comprehensions not yet supported"+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) =+ fail "Singling of annotated expressions not yet supported"+singExp vars (RecConE name fields) =+ fail "Singling of record construction not yet supported"+singExp vars (RecUpdE exp fields) =+ fail "Singling of record updates not yet supported"
+ Singletons/TypeRepStar.hs view
@@ -0,0 +1,31 @@+{- Singletons/TypeRepStar.hs++(c) Richard Eisenberg 2012+eir@cis.upenn.edu++This file contains the definitions for considering TypeRep to be the demotion+of *. This is still highly experimental, so expect unusual results!++-}++{-# LANGUAGE RankNTypes, TypeFamilies, KindSignatures, FlexibleInstances,+ GADTs, UndecidableInstances, ScopedTypeVariables #-}++module Singletons.TypeRepStar where++import Singletons.Lib+import Data.Typeable++data instance Sing (a :: *) where+ STypeRep :: Typeable a => Sing a++sTypeRep :: forall (a :: *). Typeable a => Sing a+sTypeRep = STypeRep++instance Typeable a => SingI (a :: *) where+ sing = STypeRep+instance SingE (a :: *) where+ type Demote a = TypeRep+ fromSing STypeRep = typeOf (undefined :: a)+instance SingKind (Any :: *) where+ singInstance STypeRep = SingInstance
+ Singletons/Util.hs view
@@ -0,0 +1,163 @@+{- Singletons/Util.hs++(c) Richard Eisenberg 2012+eir@cis.upenn.edu++This file contains helper functions internal to the singletons package.+Users of the package should not need to consult this file.+-}++module 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+import Data.Generics++-- reify a declaration, warning the user about splices if the reify fails+reifyWithWarning :: Name -> Q Info+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 " +++ "of the declaration. If this is the case, put\nthe reference to " +++ "the declaration in a new splice.")+ (reify name)++-- check if a string is the name of a tuple+isTupleString :: String -> Bool+isTupleString s =+ (length s > 1) &&+ (head s == '(') &&+ (last s == ')') &&+ ((length (takeWhile (== ',') (tail s))) == ((length s) - 2))++-- check if a name is a tuple name+isTupleName :: Name -> Bool+isTupleName = isTupleString . nameBase++-- extract the degree of a tuple+tupleDegree :: String -> Int+tupleDegree "()" = 0+tupleDegree s = length s - 1++-- reduce the four cases of a 'Con' to just two: monomorphic and polymorphic+-- and convert 'StrictType' to 'Type'+ctorCases :: (Name -> [Type] -> a) -> ([TyVarBndr] -> Cxt -> Con -> a) -> Con -> a+ctorCases genFun forallFun ctor = case ctor of+ NormalC name stypes -> genFun name (map snd stypes)+ RecC name vstypes -> genFun name (map (\(_,_,ty) -> ty) vstypes)+ InfixC (_,ty1) name (_,ty2) -> genFun name [ty1, ty2]+ ForallC [] [] ctor' -> ctorCases genFun forallFun ctor'+ ForallC tvbs cx ctor' -> forallFun tvbs cx ctor' ++-- reduce the four cases of a 'Con' to just 1: a polymorphic Con is treated+-- as a monomorphic one+ctor1Case :: (Name -> [Type] -> a) -> Con -> a+ctor1Case mono = ctorCases mono (\_ _ ctor -> ctor1Case mono ctor)++-- extract the name and number of arguments to a constructor+extractNameArgs :: Con -> (Name, Int)+extractNameArgs = ctor1Case (\name tys -> (name, length tys))++-- reinterpret a name. This is useful when a Name has an associated+-- namespace that we wish to forget+reinterpret :: Name -> Name+reinterpret = mkName . nameBase++-- is an identifier uppercase?+isUpcase :: Name -> Bool+isUpcase n = let first = head (nameBase n) in isUpper first || first == ':'++-- make an identifier uppercase+upcase :: Name -> Name+upcase n =+ let str = nameBase n + first = head str in+ if isLetter first+ then mkName ((toUpper first) : tail str)+ else mkName (':' : str)++-- make an identifier lowercase+locase :: Name -> Name+locase n =+ let str = nameBase n+ first = head str in+ if isLetter first+ then mkName ((toLower first) : tail str)+ else mkName (tail str) -- remove the ":"++-- put an uppercase prefix on a name. Takes two prefixes: one for identifiers+-- and one for symbols+prefixUCName :: String -> String -> Name -> Name+prefixUCName pre tyPre n = case (nameBase n) of+ (':' : rest) -> mkName (tyPre ++ rest)+ alpha -> mkName (pre ++ alpha)++-- put a lowercase prefix on a name. Takes two prefixes: one for identifiers+-- and one for symbols+prefixLCName :: String -> String -> Name -> Name+prefixLCName pre tyPre n =+ let str = nameBase n+ first = head str in+ if isLetter first+ then mkName (pre ++ str)+ else mkName (tyPre ++ str)++-- extract the name from a TyVarBndr+extractTvbName :: TyVarBndr -> Name+extractTvbName (PlainTV n) = n+extractTvbName (KindedTV n _) = n++-- extract the kind from a TyVarBndr. Returns '*' by default.+extractTvbKind :: TyVarBndr -> Kind+extractTvbKind (PlainTV _) = StarT -- FIXME: This seems wrong.+extractTvbKind (KindedTV _ k) = k++-- apply a type to a list of types+foldType :: Type -> [Type] -> Type+foldType = foldl AppT++-- apply an expression to a list of expressions+foldExp :: Exp -> [Exp] -> Exp+foldExp = foldl AppE++-- is a kind a variable?+isVarK :: Kind -> Bool+isVarK (VarT _) = True+isVarK _ = False++-- a monad transformer for writing a monoid alongside returning a Q+type QWithAux m = WriterT m Q++-- run a computation with an auxiliary monoid, discarding the monoid result+evalWithoutAux :: QWithAux m a -> Q a+evalWithoutAux = liftM fst . runWriterT++-- run a computation with an auxiliary monoid, returning only the monoid result+evalForAux :: QWithAux m a -> Q m+evalForAux = execWriterT++-- run a computation with an auxiliary monoid, return both the result+-- of the computation and the monoid result+evalForPair :: QWithAux m a -> Q (a, m)+evalForPair = runWriterT++-- in a computation with an auxiliary map, add a binding to the map+addBinding :: Ord k => k -> v -> QWithAux (Map.Map k v) ()+addBinding k v = tell (Map.singleton k v)++-- in a computation with an auxiliar list, add an element to the list+addElement :: elt -> QWithAux [elt] ()+addElement elt = tell [elt]++-- does a TH structure contain a name?+containsName :: Data a => Name -> a -> Bool+containsName n = everything (||) (mkQ False (== n))+
+ singletons.cabal view
@@ -0,0 +1,37 @@+name: singletons+version: 0.8+cabal-version: >= 1.8+synopsis: A framework for generating singleton types+homepage: http://www.cis.upenn.edu/~eir/packages/singletons+category: Dependent Types+author: Richard Eisenberg <eir@cis.upenn.edu>+maintainer: Richard Eisenberg <eir@cis.upenn.edu>+stability: experimental+extra-source-files: README+license: BSD3+license-file: LICENSE+build-type: Simple+description:+ This library generates singleton types, promoted functions, and singleton+ functions using Template Haskell. It is useful for programmers who wish+ to use dependently typed programming techniques. The library was originally+ presented in /Dependently typed programming with singletons/, submitted+ to the Haskell Symposium, 2012.+ (<http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf>)++ As of this release date, Haddock was not able to properly process the code+ and produce documentation. Hence, all of the documentation is in the+ README file distributed with the package. This README is also accessible+ from the project home page.++library+ build-depends: + base >= 4 && < 5,+ mtl >= 2.1.1,+ template-haskell,+ containers >= 0.5,+ syb >= 0.3+ exposed-modules: Singletons.Lib, Singletons.CustomStar,+ Singletons.TypeRepStar+ other-modules: Singletons.Promote, Singletons.Singletons,+ Singletons.Util