singletons-th-3.5: src/Data/Singletons/TH/Syntax.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{- Data/Singletons/TH/Syntax.hs
(c) Richard Eisenberg 2014
rae@cs.brynmawr.edu
Converts a list of DLetDecs into a LetDecEnv for easier processing,
and contains various other AST definitions.
-}
module Data.Singletons.TH.Syntax
( module Data.Singletons.TH.Syntax
, module Data.Singletons.TH.Syntax.LocalVar
) where
import Prelude hiding ( exp )
import Data.Kind (Constraint, Type)
import Language.Haskell.TH.Syntax hiding (Type)
import Language.Haskell.TH.Desugar
import qualified Language.Haskell.TH.Desugar.OMap.Strict as OMap
import Language.Haskell.TH.Desugar.OMap.Strict (OMap)
import Language.Haskell.TH.Desugar.OSet (OSet)
import Data.Singletons.TH.Syntax.LocalVar
-- | Pairs of term-level variable 'Name's and their corresponding type-level
-- names (encoded as 'LocalVar's).
type VarPromotions = [(Name, LocalVar)]
-- Information that is accumulated when promoting patterns.
data PromDPatInfos = PromDPatInfos
{ prom_dpat_vars :: VarPromotions
-- Maps term-level pattern variables to their promoted, type-level counterparts.
, prom_dpat_sig_kvs :: OSet LocalVar
-- Kind variables bound by DSigPas.
-- See Note [Scoped type variables] in Data.Singletons.TH.Promote.Monad.
}
instance Semigroup PromDPatInfos where
PromDPatInfos vars1 sig_kvs1 <> PromDPatInfos vars2 sig_kvs2
= PromDPatInfos (vars1 <> vars2) (sig_kvs1 <> sig_kvs2)
instance Monoid PromDPatInfos where
mempty = PromDPatInfos mempty mempty
-- A list of 'SingDSigPaInfos' is produced when singling pattern signatures, as we
-- must case on the 'DExp's and match on them using the supplied 'DType's to
-- bring the necessary singleton equality constraints into scope.
-- See @Note [Singling pattern signatures]@.
type SingDSigPaInfos = [(DExp, DType)]
-- The parts of data declarations that are relevant to singletons-th.
data DataDecl = DataDecl DataFlavor Name [DTyVarBndrVis] [DCon]
-- The parts of type synonyms that are relevant to singletons-th.
data TySynDecl = TySynDecl Name [DTyVarBndrVis] DType
-- The parts of open type families that are relevant to singletons-th.
type OpenTypeFamilyDecl = TypeFamilyDecl 'Open
-- The parts of closed type families that are relevant to singletons-th.
type ClosedTypeFamilyDecl = TypeFamilyDecl 'Closed
-- The parts of type families that are relevant to singletons-th.
newtype TypeFamilyDecl (info :: FamilyInfo)
= TypeFamilyDecl { getTypeFamilyDecl :: DTypeFamilyHead }
-- Whether a type family is open or closed.
data FamilyInfo = Open | Closed
data ClassDecl ann
= ClassDecl { cd_cxt :: DCxt
, cd_name :: Name
, cd_tvbs :: [DTyVarBndrVis]
, cd_fds :: [FunDep]
, cd_lde :: LetDecEnv ann
, cd_atfs :: [OpenTypeFamilyDecl]
-- Associated type families. Only recorded for
-- defunctionalization purposes.
-- See Note [Partitioning, type synonyms, and type families]
-- in D.S.TH.Partition.
}
data InstDecl ann = InstDecl { id_cxt :: DCxt
, id_name :: Name
, id_arg_tys :: [DType]
, id_sigs :: OMap Name DType
, id_meths :: [(Name, LetDecRHS ann)] }
type UClassDecl = ClassDecl Unannotated
type UInstDecl = InstDecl Unannotated
type AClassDecl = ClassDecl Annotated
type AInstDecl = InstDecl Annotated
{-
We see below several datatypes beginning with "A". These are annotated structures,
necessary for Promote to communicate key things to Single. In particular, promotion
of expressions is *not* deterministic, due to the necessity to create unique names
for lets, cases, and lambdas. So, we put these promotions into an annotated AST
so that Single can use the right promotions.
-}
-- A DExp with let, lambda, and type-signature nodes annotated with their
-- type-level equivalents
data ADExp = ADVarE Name
| ADConE Name
| ADLitE Lit
| ADAppE ADExp ADExp
| ADLamCasesE
Int
-- ^ The number of arguments in each clause. Although this can be
-- computed from the list of ADClauses, this information is used
-- multiple times during promotion and singling, so we cache this
-- number here as a convenience.
DType
-- ^ The promoted lambda.
[ADClause]
-- ^ The list of clauses in the @\\cases@ expression.
| ADLetE ALetDecEnv ADExp
| ADSigE DType -- the promoted expression
ADExp DType
-- A DPat with a pattern-signature node annotated with its type-level equivalent
data ADPat = ADLitP Lit
| ADVarP Name
| ADConP Name [DType] [ADPat]
| ADTildeP ADPat
| ADBangP ADPat
| ADSigP DType -- The promoted pattern. Will not contain any wildcards,
-- as per Note [Singling pattern signatures]
ADPat DType
| ADWildP
data ADClause = ADClause VarPromotions
[ADPat] ADExp
data AnnotationFlag = Annotated | Unannotated
-- These are used at the type-level exclusively
type Annotated = 'Annotated
type Unannotated = 'Unannotated
type family IfAnn (ann :: AnnotationFlag) (yes :: k) (no :: k) :: k where
IfAnn Annotated yes no = yes
IfAnn Unannotated yes no = no
data family LetDecRHS :: AnnotationFlag -> Type
data instance LetDecRHS Annotated
= -- A function definition. Invariant: each ADClause contains at least one
-- pattern.
AFunction
Int -- The number of arrows in the type. As a consequence of the invariant
-- above, this is always a positive number.
[ADClause]
| -- A value whose definition is given by the DExp. Invariant: the value is
-- not a function (i.e., there are no occurrences of (->) in the value's
-- type).
AValue
ADExp
data instance LetDecRHS Unannotated = UFunction [DClause]
| UValue DExp
type ALetDecRHS = LetDecRHS Annotated
type ULetDecRHS = LetDecRHS Unannotated
-- | A @let@-bound, term-level name that is promoted to the type level. The
-- first element of the pair (of type 'Name') is the promoted counterpart to the
-- term-level name, and the second element of the pair (of type @[Name]@) is the
-- list of local variables that this definition closes over after being
-- lambda-lifted. (See @Note [Tracking local variables]@ in
-- "Data.Singletons.TH.Promote.Monad".)
--
-- Note that the promoted Name in the first element of the pair is /not/ a
-- defunctionalization symbol, unlike 'LetBind' in
-- "Data.Singletons.TH.Promote.Monad". This is because it is sometimes
-- convenient to fully apply the promoted name to all of its arguments (e.g.,
-- when singling type signatures), in which case we can avoid needing to involve
-- defunctionalization symbols at all.
type LetDecProm = (Name, [LocalVar])
data LetDecEnv ann = LetDecEnv
{ lde_defns :: OMap Name (LetDecRHS ann)
, lde_types :: OMap Name DType -- type signatures
, lde_infix :: OMap Name (Fixity, NamespaceSpecifier) -- infix declarations
, lde_proms :: IfAnn ann (OMap Name LetDecProm) ()
-- ^ If annotated, this maps let-bound term 'Name's to
-- their promoted counterparts.
}
type ALetDecEnv = LetDecEnv Annotated
type ULetDecEnv = LetDecEnv Unannotated
instance Semigroup ULetDecEnv where
LetDecEnv defns1 types1 infx1 _ <> LetDecEnv defns2 types2 infx2 _ =
LetDecEnv (defns1 <> defns2) (types1 <> types2) (infx1 <> infx2) ()
instance Monoid ULetDecEnv where
mempty = LetDecEnv OMap.empty OMap.empty OMap.empty ()
valueBinding :: Name -> ULetDecRHS -> ULetDecEnv
valueBinding n v = emptyLetDecEnv { lde_defns = OMap.singleton n v }
typeBinding :: Name -> DType -> ULetDecEnv
typeBinding n t = emptyLetDecEnv { lde_types = OMap.singleton n t }
infixDecl :: Fixity -> NamespaceSpecifier -> Name -> ULetDecEnv
infixDecl f ns n = emptyLetDecEnv { lde_infix = OMap.singleton n (f, ns) }
emptyLetDecEnv :: ULetDecEnv
emptyLetDecEnv = mempty
buildLetDecEnv :: Quasi q => [DLetDec] -> q ULetDecEnv
buildLetDecEnv = go emptyLetDecEnv
where
go acc [] = return acc
go acc (DFunD name clauses : rest) =
go (valueBinding name (UFunction clauses) <> acc) rest
go acc (DValD (DVarP name) exp : rest) =
go (valueBinding name (UValue exp) <> acc) rest
go acc (dec@(DValD {}) : rest) = do
flattened <- flattenDValD dec
go acc (flattened ++ rest)
go acc (DSigD name ty : rest) =
go (typeBinding name ty <> acc) rest
go acc (DInfixD f ns n : rest) =
go (infixDecl f ns n <> acc) rest
go acc (DPragmaD{} : rest) = go acc rest
-- See Note [DerivedDecl]
data DerivedDecl (cls :: Type -> Constraint) = DerivedDecl
{ ded_mb_cxt :: Maybe DCxt
, ded_type :: DType
, ded_type_tycon :: Name
, ded_decl :: DataDecl
}
type DerivedEqDecl = DerivedDecl Eq
type DerivedOrdDecl = DerivedDecl Ord
type DerivedShowDecl = DerivedDecl Show
{- Note [DerivedDecl]
~~~~~~~~~~~~~~~~~~~~~
Most derived instances are wholly handled in
Data.Singletons.TH.Partition.partitionDecs. There are two notable exceptions to
this rule, however, that are partially handled outside of partitionDecs:
Eq and Show instances. For these instances, we use a DerivedDecl data type to
encode just enough information to recreate the derived instance:
1. Just the instance context, if it's standalone-derived, or Nothing if it's in
a deriving clause (ded_mb_cxt)
2. The datatype, applied to some number of type arguments, as in the
instance declaration (ded_type)
3. The datatype name (ded_type_tycon), cached for convenience
4. The datatype's constructors (ded_cons)
Why are these instances handled outside of partitionDecs?
* Deriving Eq in singletons-th not only derives PEq/SEq instances, but it also
derives SDecide, Eq, TestEquality, and TestCoercion instances.
* Deriving Ord in singletons-th not only derives POrd/SOrd instances, but it also
derives Ord instances for the singleton types themselves.
* Deriving Show in singletons-th not only derives PShow/SShow instances, but it
also derives Show instances for the singleton types themselves.
To make this work, we let partitionDecs handle the P{Eq,Show} and S{Eq,Show}
instances, but we also stick the relevant info into a DerivedDecl value for
later use in Data.Singletons.TH.Single, where we additionally generate
SDecide, Eq, TestEquality, TestCoercion and Show instances for singleton types.
-}