{- Data/Singletons/Single/Type.hs

(c) Richard Eisenberg 2013
rae@cs.brynmawr.edu

Singletonizes types.
-}

module Data.Singletons.Single.Type where

import Language.Haskell.TH.Desugar
import qualified Language.Haskell.TH.Desugar.OSet as OSet
import Language.Haskell.TH.Desugar.OSet (OSet)
import Language.Haskell.TH.Syntax
import Data.Singletons.Names
import Data.Singletons.Single.Monad
import Data.Singletons.Promote.Type
import Data.Singletons.Util
import Control.Monad
import Data.Foldable

singType :: OSet Name      -- the set of bound kind variables in this scope
                           -- see Note [Explicitly binding kind variables]
                           -- in Data.Singletons.Promote.Monad
         -> DType          -- the promoted version of the thing classified by...
         -> DType          -- ... this type
         -> SgM ( DType    -- the singletonized type
                , Int      -- the number of arguments
                , [Name]   -- the names of the tyvars used in the sing'd type
                , DCxt     -- the context of the singletonized type
                , [DKind]  -- the kinds of the argument types
                , DKind )  -- the kind of the result type
singType :: OSet Name
-> DType -> DType -> SgM (DType, Int, [Name], DCxt, DCxt, DType)
singType bound_kvs :: OSet Name
bound_kvs prom :: DType
prom ty :: DType
ty = do
  let (_, cxt :: DCxt
cxt, args :: DCxt
args, res :: DType
res) = DType -> ([DTyVarBndr], DCxt, DCxt, DType)
unravel DType
ty
      num_args :: Int
num_args            = DCxt -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length DCxt
args
  DCxt
cxt' <- (DType -> SgM DType) -> DCxt -> SgM DCxt
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM DType -> SgM DType
singPred DCxt
cxt
  [Name]
arg_names <- Int -> SgM Name -> SgM [Name]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
num_args (String -> SgM Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName "t")
  DCxt
prom_args <- (DType -> SgM DType) -> DCxt -> SgM DCxt
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM DType -> SgM DType
forall (m :: * -> *). MonadFail m => DType -> m DType
promoteType DCxt
args
  DType
prom_res  <- DType -> SgM DType
forall (m :: * -> *). MonadFail m => DType -> m DType
promoteType DType
res
  let args' :: DCxt
args' = (Name -> DType) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map (\n :: Name
n -> DType
singFamily DType -> DType -> DType
`DAppT` (Name -> DType
DVarT Name
n)) [Name]
arg_names
      res' :: DType
res'  = DType
singFamily DType -> DType -> DType
`DAppT` ((DType -> DType -> DType) -> DType -> DCxt -> DType
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl DType -> DType -> DType
apply DType
prom ((Name -> DType) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map Name -> DType
DVarT [Name]
arg_names) DType -> DType -> DType
`DSigT` DType
prom_res)
      tau :: DType
tau   = DCxt -> DType -> DType
ravel DCxt
args' DType
res'
      -- Make sure to subtract out the bound variables currently in scope, lest we
      -- accidentally shadow them in this type signature.
      kv_names_to_bind :: OSet Name
kv_names_to_bind = (DType -> OSet Name) -> DCxt -> OSet Name
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap DType -> OSet Name
fvDType (DCxt
prom_args DCxt -> DCxt -> DCxt
forall a. [a] -> [a] -> [a]
++ DCxt
cxt' DCxt -> DCxt -> DCxt
forall a. [a] -> [a] -> [a]
++ [DType
prom_res])
                            OSet Name -> OSet Name -> OSet Name
forall a. Ord a => OSet a -> OSet a -> OSet a
OSet.\\ OSet Name
bound_kvs
      kvs_to_bind :: [Name]
kvs_to_bind      = OSet Name -> [Name]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList OSet Name
kv_names_to_bind
  let ty' :: DType
ty' = [DTyVarBndr] -> DCxt -> DType -> DType
DForallT ((Name -> DTyVarBndr) -> [Name] -> [DTyVarBndr]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DTyVarBndr
DPlainTV [Name]
kvs_to_bind [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr]
forall a. [a] -> [a] -> [a]
++ (Name -> DType -> DTyVarBndr) -> [Name] -> DCxt -> [DTyVarBndr]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> DType -> DTyVarBndr
DKindedTV [Name]
arg_names DCxt
prom_args)
                     DCxt
cxt' DType
tau
  (DType, Int, [Name], DCxt, DCxt, DType)
-> SgM (DType, Int, [Name], DCxt, DCxt, DType)
forall (m :: * -> *) a. Monad m => a -> m a
return (DType
ty', Int
num_args, [Name]
arg_names, DCxt
cxt, DCxt
prom_args, DType
prom_res)

singPred :: DPred -> SgM DPred
singPred :: DType -> SgM DType
singPred = [DTypeArg] -> DType -> SgM DType
singPredRec []

singPredRec :: [DTypeArg] -> DPred -> SgM DPred
singPredRec :: [DTypeArg] -> DType -> SgM DType
singPredRec _cxt :: [DTypeArg]
_cxt (DForallT {}) =
  String -> SgM DType
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Singling of quantified constraints not yet supported"
singPredRec ctx :: [DTypeArg]
ctx (DAppT pr :: DType
pr ty :: DType
ty) = [DTypeArg] -> DType -> SgM DType
singPredRec (DType -> DTypeArg
DTANormal DType
ty DTypeArg -> [DTypeArg] -> [DTypeArg]
forall a. a -> [a] -> [a]
: [DTypeArg]
ctx) DType
pr
singPredRec ctx :: [DTypeArg]
ctx (DAppKindT pr :: DType
pr ki :: DType
ki) = [DTypeArg] -> DType -> SgM DType
singPredRec (DType -> DTypeArg
DTyArg DType
ki DTypeArg -> [DTypeArg] -> [DTypeArg]
forall a. a -> [a] -> [a]
: [DTypeArg]
ctx) DType
pr
singPredRec _ctx :: [DTypeArg]
_ctx (DSigT _pr :: DType
_pr _ki :: DType
_ki) =
  String -> SgM DType
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Singling of constraints with explicit kinds not yet supported"
singPredRec _ctx :: [DTypeArg]
_ctx (DVarT _n :: Name
_n) =
  String -> SgM DType
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Singling of contraint variables not yet supported"
singPredRec ctx :: [DTypeArg]
ctx (DConT n :: Name
n)
  | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
equalityName
  = String -> SgM DType
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Singling of type equality constraints not yet supported"
  | Bool
otherwise = do
    [DTypeArg]
kis <- (DTypeArg -> SgM DTypeArg) -> [DTypeArg] -> SgM [DTypeArg]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM DTypeArg -> SgM DTypeArg
forall (m :: * -> *). MonadFail m => DTypeArg -> m DTypeArg
promoteTypeArg [DTypeArg]
ctx
    let sName :: Name
sName = Name -> Name
singClassName Name
n
    DType -> SgM DType
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> SgM DType) -> DType -> SgM DType
forall a b. (a -> b) -> a -> b
$ DType -> [DTypeArg] -> DType
applyDType (Name -> DType
DConT Name
sName) [DTypeArg]
kis
singPredRec _ctx :: [DTypeArg]
_ctx DWildCardT = DType -> SgM DType
forall (m :: * -> *) a. Monad m => a -> m a
return DType
DWildCardT  -- it just might work
singPredRec _ctx :: [DTypeArg]
_ctx DArrowT =
  String -> SgM DType
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "(->) spotted at head of a constraint"
singPredRec _ctx :: [DTypeArg]
_ctx (DLitT {}) =
  String -> SgM DType
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Type-level literal spotted at head of a constraint"