Skip to content

Commit

Permalink
Use DsMonad. Still failing a bunch of tests. Needs more time.
Browse files Browse the repository at this point in the history
  • Loading branch information
Richard Eisenberg committed Sep 23, 2014
1 parent 4610fc5 commit 0c85cf8
Show file tree
Hide file tree
Showing 13 changed files with 83 additions and 85 deletions.
2 changes: 1 addition & 1 deletion singletons.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ library
mtl >= 2.1.2,
template-haskell,
containers >= 0.5,
th-desugar >= 1.4.3
th-desugar >= 1.5 && < 1.6
default-language: Haskell2010
other-extensions: TemplateHaskell
-- TemplateHaskell must be listed in cabal file to work with
Expand Down
3 changes: 1 addition & 2 deletions src/Data/Promotion/Prelude/List.hs
Original file line number Diff line number Diff line change
Expand Up @@ -225,7 +225,6 @@ module Data.Promotion.Prelude.List (
) where

import Data.Singletons.Prelude.Base
import Data.Singletons.Prelude.Bool
import Data.Singletons.Prelude.Eq
import Data.Promotion.Prelude.Ord
import Data.Singletons.Prelude.List
Expand All @@ -238,7 +237,7 @@ import Data.Singletons.Prelude.Num
import Data.Maybe (listToMaybe)
-- these imports are required fir functions that singletonize but are used
-- in this module by a function that can't be singletonized
import Data.List (deleteBy, sortBy, insertBy)
import Data.List (sortBy, insertBy)

$(promoteOnly [d|
-- Can't be promoted because of limitations of Int promotion
Expand Down
14 changes: 6 additions & 8 deletions src/Data/Singletons/CustomStar.hs
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,6 @@ module Data.Singletons.CustomStar (
) where

import Language.Haskell.TH
import Language.Haskell.TH.Syntax ( Quasi(..) )
import Data.Singletons.Util
import Data.Singletons.Promote
import Data.Singletons.Promote.Monad
Expand All @@ -36,7 +35,6 @@ import Control.Monad
import Data.Maybe
import Control.Applicative
import Language.Haskell.TH.Desugar
import Language.Haskell.TH.Desugar.Sweeten
import Data.Singletons.Prelude.Eq
import Data.Singletons.Prelude.Bool

Expand Down Expand Up @@ -66,7 +64,7 @@ import Data.Singletons.Prelude.Bool
-- @Bool@, and @Maybe@, not just promoted data constructors.
--
-- Please note that this function is /very/ experimental. Use at your own risk.
singletonStar :: Quasi q
singletonStar :: DsMonad q
=> [Name] -- ^ A list of Template Haskell @Name@s for types
-> q [Dec]
singletonStar names = do
Expand All @@ -76,13 +74,13 @@ singletonStar names = do
[''Eq, ''Show, ''Read]
fakeCtors <- zipWithM (mkCtor False) names kinds
let dataDecl = DataDecl Data repName [] fakeCtors [''Show, ''Read , ''Eq, ''Ord]
promDecls <- promoteM_ $ promoteDataDec dataDecl
singletonDecls <- singDecsM $ singDataD dataDecl
promDecls <- promoteM_ [] $ promoteDataDec dataDecl
singletonDecls <- singDecsM [] $ singDataD dataDecl
return $ decsToTH $ repDecl :
promDecls ++
singletonDecls
where -- get the kinds of the arguments to the tycon with the given name
getKind :: Quasi q => Name -> q [DKind]
getKind :: DsMonad q => Name -> q [DKind]
getKind name = do
info <- reifyWithWarning name
dinfo <- dsInfo info
Expand All @@ -99,15 +97,15 @@ singletonStar names = do

-- 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 :: Quasi q => Bool -> Name -> [DKind] -> q DCon
mkCtor :: DsMonad q => Bool -> Name -> [DKind] -> q DCon
mkCtor real name args = do
(types, vars) <- evalForPair $ mapM kindToType args
dataName <- if real then mkDataName (nameBase name) else return name
return $ DCon (map DPlainTV vars) [] dataName $
DNormalC (map (\ty -> (NotStrict, ty)) types)

-- demote a kind back to a type, accumulating any unbound parameters
kindToType :: Quasi q => DKind -> QWithAux [Name] q DType
kindToType :: DsMonad q => DKind -> QWithAux [Name] q DType
kindToType (DForallK _ _) = fail "Explicit forall encountered in kind"
kindToType (DVarK n) = do
addElement n
Expand Down
23 changes: 11 additions & 12 deletions src/Data/Singletons/Prelude/List.hs
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@
--
----------------------------------------------------------------------------

module Data.Singletons.Prelude.List {-(
module Data.Singletons.Prelude.List (
-- * The singleton for lists
Sing(SNil, SCons),
-- | Though Haddock doesn't show it, the 'Sing' instance above declares
Expand Down Expand Up @@ -75,7 +75,7 @@ module Data.Singletons.Prelude.List {-(
-- * Searching lists

-- ** Searching by equality
{- Elem, sElem, -} NotElem, sNotElem, Lookup, sLookup,
Elem, sElem, NotElem, sNotElem, Lookup, sLookup,

-- ** Searching with a predicate
Find, sFind, Filter, sFilter, Partition, sPartition,
Expand All @@ -90,7 +90,7 @@ module Data.Singletons.Prelude.List {-(
-- * Special lists

-- ** \"Set\" operations
{- Nub, sNub, -} Delete, sDelete, (:\\), (%:\\), Union, sUnion,
Nub, sNub, Delete, sDelete, (:\\), (%:\\), Union, sUnion,
Intersect, sIntersect,

-- ** Ordered lists
Expand Down Expand Up @@ -148,7 +148,7 @@ module Data.Singletons.Prelude.List {-(
IsSuffixOfSym0, IsSuffixOfSym1, IsSuffixOfSym2,
IsInfixOfSym0, IsInfixOfSym1, IsInfixOfSym2,

{- ElemSym0, ElemSym1, ElemSym2, -}
ElemSym0, ElemSym1, ElemSym2,
NotElemSym0, NotElemSym1, NotElemSym2,

ZipSym0, ZipSym1, ZipSym2,
Expand Down Expand Up @@ -188,7 +188,7 @@ module Data.Singletons.Prelude.List {-(
FindSym0, FindSym1, FindSym2,
FilterSym0, FilterSym1, FilterSym2,
PartitionSym0, PartitionSym1, PartitionSym2,
{-

Zip4Sym0, Zip4Sym1, Zip4Sym2, Zip4Sym3, Zip4Sym4,
Zip5Sym0, Zip5Sym1, Zip5Sym2, Zip5Sym3, Zip5Sym4, Zip5Sym5,
Zip6Sym0, Zip6Sym1, Zip6Sym2, Zip6Sym3, Zip6Sym4, Zip6Sym5, Zip6Sym6,
Expand All @@ -203,16 +203,16 @@ module Data.Singletons.Prelude.List {-(
ZipWith6Sym5, ZipWith6Sym6, ZipWith6Sym7,
ZipWith7Sym0, ZipWith7Sym1, ZipWith7Sym2, ZipWith7Sym3, ZipWith7Sym4,
ZipWith7Sym5, ZipWith7Sym6, ZipWith7Sym7, ZipWith7Sym8,
-}

{- NubSym0, NubSym1, -}

NubSym0, NubSym1,
NubBySym0, NubBySym1, NubBySym2,
UnionBySym0, UnionBySym1, UnionBySym2, UnionBySym3,
UnionSym0, UnionSym1, UnionSym2,
IntersectSym0, IntersectSym1, IntersectSym2,
IntersectBySym0, IntersectBySym1, IntersectBySym2, IntersectBySym3

)-} where
) where

import Data.Singletons
import Data.Singletons.Prelude.Instances
Expand Down Expand Up @@ -444,7 +444,7 @@ $(singletonsOnly [d|

unzip :: [(a,b)] -> ([a],[b])
unzip xs = foldr (\(a,b) (as,bs) -> (a:as,b:bs)) ([],[]) xs
{-

-- Lazy patterns removed from unzip
unzip3 :: [(a,b,c)] -> ([a],[b],[c])
unzip3 xs = foldr (\(a,b,c) (as,bs,cs) -> (a:as,b:bs,c:cs))
Expand All @@ -469,7 +469,7 @@ $(singletonsOnly [d|
unzip7 xs = foldr (\(a,b,c,d,e,f,g) (as,bs,cs,ds,es,fs,gs) ->
(a:as,b:bs,c:cs,d:ds,e:es,f:fs,g:gs))
([],[],[],[],[],[],[]) xs
-}

-- We can't promote any of these functions because at the type level
-- String literals are no longer considered to be lists of Chars, so
-- there is mismatch between term-level and type-level semantics
Expand Down Expand Up @@ -603,7 +603,7 @@ $(singletonsOnly [d|
select :: (a -> Bool) -> a -> ([a], [a]) -> ([a], [a])
select p x ~(ts,fs) | p x = (x:ts,fs)
| otherwise = (ts, x:fs)
{-

zip4 :: [a] -> [b] -> [c] -> [d] -> [(a,b,c,d)]
zip4 = zipWith4 (,,,)

Expand Down Expand Up @@ -640,7 +640,6 @@ $(singletonsOnly [d|
zipWith7 z (a:as) (b:bs) (c:cs) (d:ds) (e:es) (f:fs) (g:gs)
= z a b c d e f g : zipWith7 z as bs cs ds es fs gs
zipWith7 _ _ _ _ _ _ _ _ = []
-}

nub :: (Eq a) => [a] -> [a]
nub l = nub' l []
Expand Down
31 changes: 15 additions & 16 deletions src/Data/Singletons/Promote.hs
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,6 @@ module Data.Singletons.Promote where
import Language.Haskell.TH hiding ( Q, cxt )
import Language.Haskell.TH.Syntax ( Quasi(..), lift )
import Language.Haskell.TH.Desugar
import Language.Haskell.TH.Desugar.Sweeten
import Language.Haskell.TH.Desugar.Lift ()
import Data.Singletons.Names
import Data.Singletons.Promote.Monad
Expand All @@ -33,52 +32,52 @@ import Data.Map.Strict ( Map )

-- | Generate promoted definitions from a type that is already defined.
-- This is generally only useful with classes.
genPromotions :: Quasi q => [Name] -> q [Dec]
genPromotions :: DsMonad q => [Name] -> q [Dec]
genPromotions names = do
checkForRep names
infos <- mapM reifyWithWarning names
dinfos <- mapM dsInfo infos
ddecs <- promoteM_ $ mapM_ promoteInfo dinfos
ddecs <- promoteM_ [] $ mapM_ promoteInfo dinfos
return $ decsToTH ddecs

-- | Promote every declaration given to the type level, retaining the originals.
promote :: Quasi q => q [Dec] -> q [Dec]
promote :: DsMonad q => q [Dec] -> q [Dec]
promote qdec = do
decls <- qdec
ddecls <- dsDecs decls
promDecls <- promoteM_ $ promoteDecs ddecls
ddecls <- withLocalDeclarations decls $ dsDecs decls
promDecls <- promoteM_ decls $ promoteDecs ddecls
return $ decls ++ decsToTH promDecls

-- | Promote each declaration, discarding the originals.
promoteOnly :: Quasi q => q [Dec] -> q [Dec]
promoteOnly :: DsMonad q => q [Dec] -> q [Dec]
promoteOnly qdec = do
decls <- qdec
ddecls <- dsDecs decls
promDecls <- promoteM_ $ promoteDecs ddecls
promDecls <- promoteM_ decls $ promoteDecs ddecls
return $ decsToTH promDecls

-- | Generate defunctionalization symbols for existing type family
genDefunSymbols :: Quasi q => [Name] -> q [Dec]
genDefunSymbols :: DsMonad q => [Name] -> q [Dec]
genDefunSymbols names = do
checkForRep names
infos <- mapM (dsInfo <=< reifyWithWarning) names
decs <- promoteMDecs $ concatMapM defunInfo infos
decs <- promoteMDecs [] $ concatMapM defunInfo infos
return $ decsToTH decs

-- | Produce instances for '(:==)' (type-level equality) from the given types
promoteEqInstances :: Quasi q => [Name] -> q [Dec]
promoteEqInstances :: DsMonad q => [Name] -> q [Dec]
promoteEqInstances = concatMapM promoteEqInstance

-- | Produce instances for 'Compare' from the given types
promoteOrdInstances :: Quasi q => [Name] -> q [Dec]
promoteOrdInstances :: DsMonad q => [Name] -> q [Dec]
promoteOrdInstances = concatMapM promoteOrdInstance

-- | Produce instances for 'MinBound' and 'MaxBound' from the given types
promoteBoundedInstances :: Quasi q => [Name] -> q [Dec]
promoteBoundedInstances :: DsMonad q => [Name] -> q [Dec]
promoteBoundedInstances = concatMapM promoteBoundedInstance

-- | Produce an instance for '(:==)' (type-level equality) from the given type
promoteEqInstance :: Quasi q => Name -> q [Dec]
promoteEqInstance :: DsMonad q => Name -> q [Dec]
promoteEqInstance name = do
(_tvbs, cons) <- getDataD "I cannot make an instance of (:==) for it." name
cons' <- mapM dsCon cons
Expand All @@ -88,7 +87,7 @@ promoteEqInstance name = do
return $ decsToTH inst_decs

-- | Produce an instance for 'Compare' from the given type
promoteOrdInstance :: Quasi q => Name -> q [Dec]
promoteOrdInstance :: DsMonad q => Name -> q [Dec]
promoteOrdInstance name = do
(_tvbs, cons) <- getDataD "I cannot make an instance of Ord for it." name
cons' <- mapM dsCon cons
Expand All @@ -98,7 +97,7 @@ promoteOrdInstance name = do
return $ decsToTH inst_decs

-- | Produce an instance for 'MinBound' and 'MaxBound' from the given type
promoteBoundedInstance :: Quasi q => Name -> q [Dec]
promoteBoundedInstance :: DsMonad q => Name -> q [Dec]
promoteBoundedInstance name = do
(_tvbs, cons) <- getDataD "I cannot make an instance of Bounded for it." name
cons' <- mapM dsCon cons
Expand Down
27 changes: 16 additions & 11 deletions src/Data/Singletons/Promote/Monad.hs
Original file line number Diff line number Diff line change
Expand Up @@ -35,11 +35,13 @@ type LetExpansions = Map Name DType -- from **term-level** name
data PrEnv =
PrEnv { pr_lambda_bound :: Map Name Name
, pr_let_bound :: LetExpansions
, pr_local_decls :: [Dec]
}

emptyPrEnv :: PrEnv
emptyPrEnv = PrEnv { pr_lambda_bound = Map.empty
, pr_let_bound = Map.empty }
, pr_let_bound = Map.empty
, pr_local_decls = [] }

-- the promotion monad
newtype PrM a = PrM (ReaderT PrEnv (WriterT [DDec] Q) a)
Expand Down Expand Up @@ -74,6 +76,9 @@ instance Quasi PrM where
tell aux
return result

instance DsMonad PrM where
localDeclarations = asks pr_local_decls

-- return *type-level* names
allLocals :: MonadReader PrEnv m => m [Name]
allLocals = do
Expand Down Expand Up @@ -117,20 +122,20 @@ lookupVarE n = do
Just ty -> return ty
Nothing -> return $ promoteValRhs n

promoteM :: Quasi q => PrM a -> q (a, [DDec])
promoteM (PrM rdr) =
let wr = runReaderT rdr emptyPrEnv
promoteM :: DsMonad q => [Dec] -> PrM a -> q (a, [DDec])
promoteM locals (PrM rdr) = do
other_locals <- localDeclarations
let wr = runReaderT rdr (emptyPrEnv { pr_local_decls = other_locals ++ locals })
q = runWriterT wr
in
runQ q

promoteM_ :: Quasi q => PrM () -> q [DDec]
promoteM_ thing = do
((), decs) <- promoteM thing
promoteM_ :: DsMonad q => [Dec] -> PrM () -> q [DDec]
promoteM_ locals thing = do
((), decs) <- promoteM locals thing
return decs

-- promoteM specialized to [DDec]
promoteMDecs :: Quasi q => PrM [DDec] -> q [DDec]
promoteMDecs thing = do
(decs1, decs2) <- promoteM thing
promoteMDecs :: DsMonad q => [Dec] -> PrM [DDec] -> q [DDec]
promoteMDecs locals thing = do
(decs1, decs2) <- promoteM locals thing
return $ decs1 ++ decs2
16 changes: 8 additions & 8 deletions src/Data/Singletons/Single.hs
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,6 @@ import Data.Singletons.Single.Eq
import Data.Singletons.Single.Squash
import Data.Singletons.Syntax
import Language.Haskell.TH.Desugar
import Language.Haskell.TH.Desugar.Sweeten
import qualified Data.Map.Strict as Map
import Data.Map.Strict ( Map )
import Control.Monad
Expand Down Expand Up @@ -131,13 +130,13 @@ singEqualityInstance desc@(_, className, _) name = do
kind = DConK name tyvars
aName <- qNewName "a"
let aVar = DVarT aName
(scons, _) <- singM $ mapM (singCtor aVar) dcons
(scons, _) <- singM [] $ mapM (singCtor aVar) dcons
eqInstance <- mkEqualityInstance kind scons desc
return $ decToTH eqInstance

singInfo :: DsMonad q => DInfo -> q [DDec]
singInfo (DTyConI dec Nothing) = do -- TODO: document this special case
singTopLevelDecs [dec]
singTopLevelDecs [] [dec]
singInfo (DTyConI {}) =
fail "Singling of things with instances not yet supported" -- TODO: fix
singInfo (DPrimTyConI _name _numArgs _unlifted) =
Expand All @@ -147,8 +146,8 @@ singInfo (DVarI _name _ty _mdec _fixity) =
singInfo (DTyVarI _name _ty) =
fail "Singling of type variable info not supported"

singTopLevelDecs :: DsMonad q => [DDec] -> q [DDec]
singTopLevelDecs decls = do
singTopLevelDecs :: DsMonad q => [Dec] -> [DDec] -> q [DDec]
singTopLevelDecs locals decls = do
PDecs { pd_let_decs = letDecls
, pd_class_decs = classes
, pd_instance_decs = insts
Expand All @@ -159,9 +158,10 @@ singTopLevelDecs decls = do
when (not (null classes) || not (null insts)) $
qReportError "Classes and instances may not yet be made into singletons."

dataDecls' <- promoteM_ $ promoteDataDecs datas
((_, letDecEnv), letDecls') <- promoteM $ promoteLetDecs noPrefix squashedLetDecls
singDecsM $ do
dataDecls' <- promoteM_ locals $ promoteDataDecs datas
((_, letDecEnv), letDecls') <- promoteM locals $
promoteLetDecs noPrefix squashedLetDecls
singDecsM locals $ do
let letBinds = concatMap buildDataLets datas
++ concatMap buildMethLets classes
(newLetDecls, newDataDecls) <- bindLets letBinds $
Expand Down
Loading

0 comments on commit 0c85cf8

Please sign in to comment.