singletons 0.8.1 → 0.8.2

raw patch · 15 files changed

+1633/−1609 lines, 15 filesdep ~base

Dependency ranges changed: base

Files

• CHANGES +25/−0
• Data/Singletons.hs +151/−0
• Data/Singletons/CustomStar.hs +91/−0
• Data/Singletons/Promote.hs +548/−0
• Data/Singletons/Singletons.hs +597/−0
• Data/Singletons/TypeRepStar.hs +31/−0
• Data/Singletons/Util.hs +165/−0
• README +17/−5
• Singletons/CustomStar.hs +0/−91
• Singletons/Lib.hs +0/−159
• Singletons/Promote.hs +0/−548
• Singletons/Singletons.hs +0/−602
• Singletons/TypeRepStar.hs +0/−31
• Singletons/Util.hs +0/−165
• singletons.cabal +8/−8

@@ -0,0 +1,25 @@+Changelog for singletons project+================================++0.8.2+-----++Added this changelog++Update to work with latest version of GHC (7.6.1). (There was a change to+Template Haskell).++Moved library into Data.Singletons.++0.8.1+-----++Update to work with latest version of GHC. (There was a change to+Template Haskell).++Updated dependencies in cabal to include the newer version of TH.++0.8+---++Initial public release

@@ -0,0 +1,151 @@+{- Data/Singletons.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+ #-}+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}++module Data.Singletons (+  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 Data.Singletons.Singletons+import Data.Singletons.Promote+import Language.Haskell.TH+import GHC.Exts+import Data.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++$(singletons [d|+  (++) :: [a] -> [a] -> [a]+  [] ++ a = a+  (h:t) ++ a = 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"

@@ -0,0 +1,91 @@+{- Data/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 Data.Singletons.CustomStar where++import Language.Haskell.TH+import Data.Singletons.Util+import Data.Singletons.Promote+import Data.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"

@@ -0,0 +1,548 @@+{- Data/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 Data.Singletons.Promote where++import Language.Haskell.TH+import Data.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 -> reportWarning $ "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 $ reportWarning "Lazy pattern converted into regular pattern in promotion"+  promoteTopLevelPat pat+promoteTopLevelPat (BangP pat) = do+  lift $ reportWarning "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 $ reportWarning $ "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 $ reportWarning "Lazy pattern converted into regular pattern in promotion"+  promotePat pat+promotePat (BangP pat) = do+  lift $ reportWarning "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 $ reportWarning $ "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 (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 (CondE bexp texp fexp) = do+  tys <- mapM (promoteExp vars) [bexp, texp, fexp]+  return $ foldType ifTyFam tys+promoteExp vars (MultiIfE alts) =+  fail "Promotion of multi-way if not yet supported"+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"

@@ -0,0 +1,597 @@+{- Data/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 Data.Singletons.Singletons where++import Language.Haskell.TH+import Data.Singletons.Util+import Data.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+    reportWarning $ "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) = do+    reportWarning "Singling of pragmas not supported"+    return []+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 (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) =+  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) =+  fail "Singling of multi-way if statements not yet supported"+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"

@@ -0,0 +1,31 @@+{- Data/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 Data.Singletons.TypeRepStar where++import Data.Singletons+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

@@ -0,0 +1,165 @@+{- Data/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.+-}++{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}++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+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))+

@@ -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 (June 2, 2012), haddock has not quite caught up with GHC in+of this writing (September 12, 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.@@ -25,7 +25,7 @@ Compatibility ------------- -The singletons library requires GHC version 7.5.20120529 or greater.+The singletons library requires GHC version 7.6.1 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:@@ -52,7 +52,7 @@ 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.+These functions are all defined in Data.Singletons.   genPromotion :: [Name] -> Q [Dec]@@ -316,12 +316,14 @@ ---------------------------- Supported Haskell constructs ----------------------------+#supported-features#  The following constructs are fully supported:  * variables * tuples * constructors+* if statements * infix expressions * !, ~, and _ patterns * aliased patterns (except at top-level)@@ -353,7 +355,17 @@  See the paper cited above for reasons why these are problematic. +As described briefly in the paper, the singletons generation mechanism does not+currently work for higher-order datatypes (though higher-order functions are+just peachy). So, if you have a declaration such as +> data Foo = Bar (Bool -> Maybe Bool)++, its singleton will not work correctly. It turns out that getting this to work+requires fairly thorough changes to the whole singleton generation scheme.+Please shout (to eir@cis.upenn.edu) if you have a compelling use case for this+and I can take a look at it. No promises, though.+ ------------- Support for * -------------@@ -364,7 +376,7 @@ 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+1) The module Data.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: @@ -397,7 +409,7 @@ >   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@,+The unexpected part is that @Nat@, @Bool@, and @Maybe@ above are the real @Nat@, @Bool@, and @Maybe@, not just promoted data constructors.  

@@ -1,91 +0,0 @@-{- 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"

@@ -1,159 +0,0 @@-{- 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- #-}-{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}--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"

@@ -1,548 +0,0 @@-{- 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 -> reportWarning $ "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 $ reportWarning "Lazy pattern converted into regular pattern in promotion"-  promoteTopLevelPat pat-promoteTopLevelPat (BangP pat) = do-  lift $ reportWarning "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 $ reportWarning $ "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 $ reportWarning "Lazy pattern converted into regular pattern in promotion"-  promotePat pat-promotePat (BangP pat) = do-  lift $ reportWarning "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 $ reportWarning $ "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 (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 (CondE bexp texp fexp) = do-  tys <- mapM (promoteExp vars) [bexp, texp, fexp]-  return $ foldType ifTyFam tys-promoteExp vars (MultiIfE alts) =-  fail "Promotion of multi-way if not yet supported"-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"

@@ -1,602 +0,0 @@-{- 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-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-    reportWarning $ "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-    reportWarning $ "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 (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) =-  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) =-  fail "Singling of multi-way if statements not yet supported"-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"

@@ -1,31 +0,0 @@-{- 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

@@ -1,165 +0,0 @@-{- 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.--}--{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}--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))-

@@ -1,5 +1,5 @@ name:           singletons-version:        0.8.1+version:        0.8.2 cabal-version:  >= 1.8 synopsis:       A framework for generating singleton types homepage:       http://www.cis.upenn.edu/~eir/packages/singletons@@ -7,7 +7,7 @@ author:         Richard Eisenberg <eir@cis.upenn.edu> maintainer:     Richard Eisenberg <eir@cis.upenn.edu> stability:      experimental-extra-source-files: README+extra-source-files: README, CHANGES license:        BSD3 license-file:   LICENSE build-type:     Simple@@ -15,8 +15,8 @@     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.+    presented in /Dependently Typed Programming with Singletons/, published+    at 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@@ -31,7 +31,7 @@       template-haskell >= 2.8,       containers >= 0.5,       syb >= 0.3-  exposed-modules:    Singletons.Lib, Singletons.CustomStar,-                      Singletons.TypeRepStar-  other-modules:      Singletons.Promote, Singletons.Singletons,-                      Singletons.Util+  exposed-modules:    Data.Singletons, Data.Singletons.CustomStar,+                      Data.Singletons.TypeRepStar+  other-modules:      Data.Singletons.Promote, Data.Singletons.Singletons,+                      Data.Singletons.Util