{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE Unsafe #-}
module Data.Eliminator.TH (
deriveElim
, deriveElimNamed
, deriveTypeElim
, deriveTypeElimNamed
) where
import Control.Applicative
import Control.Monad
import Data.Char (isLetter, isUpper, toUpper)
import Data.Foldable
import qualified Data.Kind as Kind (Type)
import Data.Maybe
import Data.Proxy
import Data.Singletons.TH.Options
import Language.Haskell.TH
import Language.Haskell.TH.Datatype
import Language.Haskell.TH.Datatype.TyVarBndr
import Language.Haskell.TH.Desugar hiding (NewOrData(..))
import Prelude.Singletons
deriveElim :: Name -> Q [Dec]
deriveElim :: Name -> Q [Dec]
deriveElim Name
dataName = String -> Name -> Q [Dec]
deriveElimNamed (Name -> String
eliminatorName Name
dataName) Name
dataName
deriveElimNamed :: String -> Name -> Q [Dec]
deriveElimNamed :: String -> Name -> Q [Dec]
deriveElimNamed = Proxy 'IsTerm -> String -> Name -> Q [Dec]
forall (t :: TermOrType) (proxy :: TermOrType -> *).
Eliminator t =>
proxy t -> String -> Name -> Q [Dec]
deriveElimNamed' (forall {k} (t :: k). Proxy t
forall {t :: TermOrType}. Proxy t
Proxy @IsTerm)
deriveTypeElim :: Name -> Q [Dec]
deriveTypeElim :: Name -> Q [Dec]
deriveTypeElim Name
dataName = String -> Name -> Q [Dec]
deriveTypeElimNamed (String -> String
upcase (Name -> String
eliminatorName Name
dataName)) Name
dataName
deriveTypeElimNamed :: String -> Name -> Q [Dec]
deriveTypeElimNamed :: String -> Name -> Q [Dec]
deriveTypeElimNamed = Proxy 'IsType -> String -> Name -> Q [Dec]
forall (t :: TermOrType) (proxy :: TermOrType -> *).
Eliminator t =>
proxy t -> String -> Name -> Q [Dec]
deriveElimNamed' (forall {k} (t :: k). Proxy t
forall {t :: TermOrType}. Proxy t
Proxy @IsType)
deriveElimNamed' ::
Eliminator t
=> proxy t
-> String
-> Name
-> Q [Dec]
deriveElimNamed' :: forall (t :: TermOrType) (proxy :: TermOrType -> *).
Eliminator t =>
proxy t -> String -> Name -> Q [Dec]
deriveElimNamed' proxy t
prox String
funName Name
dataName = do
info :: DatatypeInfo
info@(DatatypeInfo { datatypeVars :: DatatypeInfo -> [TyVarBndrUnit]
datatypeVars = [TyVarBndrUnit]
dataVarBndrs
, datatypeVariant :: DatatypeInfo -> DatatypeVariant
datatypeVariant = DatatypeVariant
variant
, datatypeCons :: DatatypeInfo -> [ConstructorInfo]
datatypeCons = [ConstructorInfo]
cons
}) <- Name -> Q DatatypeInfo
reifyDatatype Name
dataName
let noDataFamilies :: Q a
noDataFamilies =
String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Eliminators for data family instances are currently not supported"
case DatatypeVariant
variant of
DatatypeVariant
DataInstance -> Q ()
forall {a}. Q a
noDataFamilies
DatatypeVariant
NewtypeInstance -> Q ()
forall {a}. Q a
noDataFamilies
DatatypeVariant
Datatype -> () -> Q ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
DatatypeVariant
Newtype -> () -> Q ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Name
predVar <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"p"
Name
singVar <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"s"
let elimName :: Name
elimName = String -> Name
mkName String
funName
promDataKind :: Type
promDataKind = DatatypeInfo -> Type
datatypeType DatatypeInfo
info
predVarBndr :: TyVarBndrUnit
predVarBndr = Name -> Type -> TyVarBndrUnit
kindedTV Name
predVar (Type -> Name -> Type -> Type
InfixT Type
promDataKind ''(~>) (Name -> Type
ConT ''Kind.Type))
singVarBndr :: TyVarBndrUnit
singVarBndr = Name -> Type -> TyVarBndrUnit
kindedTV Name
singVar Type
promDataKind
[Type]
caseTypes <- (ConstructorInfo -> Q Type) -> [ConstructorInfo] -> Q [Type]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (proxy t -> Name -> Name -> ConstructorInfo -> Q Type
forall (t :: TermOrType) (proxy :: TermOrType -> *).
Eliminator t =>
proxy t -> Name -> Name -> ConstructorInfo -> Q Type
caseType proxy t
prox Name
dataName Name
predVar) [ConstructorInfo]
cons
let returnType :: Type
returnType = Name -> Type -> Type
predType Name
predVar (Name -> Type
VarT Name
singVar)
elimType :: Type
elimType = proxy t
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> TyVarBndrUnit
-> [Type]
-> Type
-> Type
forall (t :: TermOrType) (proxy :: TermOrType -> *).
Eliminator t =>
proxy t
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> TyVarBndrUnit
-> [Type]
-> Type
-> Type
elimTypeSig proxy t
prox [TyVarBndrUnit]
dataVarBndrs TyVarBndrUnit
predVarBndr TyVarBndrUnit
singVarBndr
[Type]
caseTypes Type
returnType
Dec
elimEqns <- proxy t
-> Name
-> Name
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> TyVarBndrUnit
-> [Type]
-> [ConstructorInfo]
-> Q Dec
forall (t :: TermOrType) (proxy :: TermOrType -> *).
Eliminator t =>
proxy t
-> Name
-> Name
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> TyVarBndrUnit
-> [Type]
-> [ConstructorInfo]
-> Q Dec
qElimEqns proxy t
prox (String -> Name
mkName String
funName) Name
dataName
[TyVarBndrUnit]
dataVarBndrs TyVarBndrUnit
predVarBndr TyVarBndrUnit
singVarBndr
[Type]
caseTypes [ConstructorInfo]
cons
[Dec] -> Q [Dec]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [proxy t -> Name -> Type -> Dec
forall (t :: TermOrType) (proxy :: TermOrType -> *).
Eliminator t =>
proxy t -> Name -> Type -> Dec
elimSigD proxy t
prox Name
elimName Type
elimType, Dec
elimEqns]
caseType ::
Eliminator t
=> proxy t
-> Name
-> Name
-> ConstructorInfo
-> Q Type
caseType :: forall (t :: TermOrType) (proxy :: TermOrType -> *).
Eliminator t =>
proxy t -> Name -> Name -> ConstructorInfo -> Q Type
caseType proxy t
prox Name
dataName Name
predVar
(ConstructorInfo { constructorName :: ConstructorInfo -> Name
constructorName = Name
conName
, constructorVars :: ConstructorInfo -> [TyVarBndrUnit]
constructorVars = [TyVarBndrUnit]
conVars
, constructorContext :: ConstructorInfo -> [Type]
constructorContext = [Type]
conContext
, constructorFields :: ConstructorInfo -> [Type]
constructorFields = [Type]
fieldTypes })
= do Bool -> Q () -> Q ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([TyVarBndrUnit] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVarBndrUnit]
conVars Bool -> Bool -> Bool
&& [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
conContext) (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$
String -> Q ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
[ String
"Eliminators for GADTs or datatypes with existentially quantified"
, String
"data constructors currently not supported"
]
[Name]
vars <- String -> Int -> Q [Name]
newNameList String
"f" (Int -> Q [Name]) -> Int -> Q [Name]
forall a b. (a -> b) -> a -> b
$ [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
fieldTypes
let returnType :: Type
returnType = Name -> Type -> Type
predType Name
predVar
((Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Type -> Type -> Type
AppT (Name -> Type
ConT Name
conName) ((Name -> Type) -> [Name] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Type
VarT [Name]
vars))
Type -> Q Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> Q Type) -> Type -> Q Type
forall a b. (a -> b) -> a -> b
$ ((Name, Type) -> Type -> Type) -> Type -> [(Name, Type)] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr' (\(Name
var, Type
varType) Type
t ->
proxy t -> Name -> Name -> Name -> Type -> Type -> Type
forall (t :: TermOrType) (proxy :: TermOrType -> *).
Eliminator t =>
proxy t -> Name -> Name -> Name -> Type -> Type -> Type
prependElimCaseTypeVar proxy t
prox Name
dataName Name
predVar Name
var Type
varType Type
t)
Type
returnType
([Name] -> [Type] -> [(Name, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
vars [Type]
fieldTypes)
caseClause ::
Name
-> Name
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> Int
-> Int
-> ConstructorInfo
-> Q Clause
caseClause :: Name
-> Name
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> Int
-> Int
-> ConstructorInfo
-> Q Clause
caseClause Name
elimName Name
dataName [TyVarBndrUnit]
dataVarBndrs TyVarBndrUnit
predVarBndr Int
conIndex Int
numCons
(ConstructorInfo { constructorName :: ConstructorInfo -> Name
constructorName = Name
conName
, constructorFields :: ConstructorInfo -> [Type]
constructorFields = [Type]
fieldTypes })
= do let numFields :: Int
numFields = [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
fieldTypes
[Name]
singVars <- String -> Int -> Q [Name]
newNameList String
"s" Int
numFields
[Name]
singVarSigs <- String -> Int -> Q [Name]
newNameList String
"sTy" Int
numFields
Name
usedCaseVar <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"useThis"
[Name]
caseVars <- Int -> (Int -> Q Name) -> Q [Name]
forall (f :: * -> *) a.
Applicative f =>
Int -> (Int -> f a) -> f [a]
ireplicateA Int
numCons ((Int -> Q Name) -> Q [Name]) -> (Int -> Q Name) -> Q [Name]
forall a b. (a -> b) -> a -> b
$ \Int
i ->
if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
conIndex
then Name -> Q Name
forall (f :: * -> *) a. Applicative f => a -> f a
pure Name
usedCaseVar
else String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName (String
"_p" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i)
let singConName :: Name
singConName = Options -> Name -> Name
singledDataConName Options
defaultOptions Name
conName
mkSingVarPat :: Name -> Name -> Pat
mkSingVarPat Name
var Name
varSig = Pat -> Type -> Pat
SigP (Name -> Pat
VarP Name
var) (Name -> Type
singType Name
varSig)
singVarPats :: [Pat]
singVarPats = (Name -> Name -> Pat) -> [Name] -> [Name] -> [Pat]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> Name -> Pat
mkSingVarPat [Name]
singVars [Name]
singVarSigs
mbInductiveArg :: Name -> Name -> Type -> Maybe Exp
mbInductiveArg Name
singVar Name
singVarSig Type
varType =
let prefix :: Exp
prefix = Exp -> [Type] -> Exp
foldAppTypeE (Name -> Exp
VarE Name
elimName)
([Type] -> Exp) -> [Type] -> Exp
forall a b. (a -> b) -> a -> b
$ (TyVarBndrUnit -> Type) -> [TyVarBndrUnit] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type) -> (TyVarBndrUnit -> Name) -> TyVarBndrUnit -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndrUnit -> Name
forall flag. TyVarBndr_ flag -> Name
tvName) [TyVarBndrUnit]
dataVarBndrs
[Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Name -> Type
VarT (TyVarBndrUnit -> Name
forall flag. TyVarBndr_ flag -> Name
tvName TyVarBndrUnit
predVarBndr), Name -> Type
VarT Name
singVarSig]
inductiveArg :: Exp
inductiveArg = Exp -> [Exp] -> Exp
foldAppE Exp
prefix
([Exp] -> Exp) -> [Exp] -> Exp
forall a b. (a -> b) -> a -> b
$ Name -> Exp
VarE Name
singVarExp -> [Exp] -> [Exp]
forall a. a -> [a] -> [a]
:(Name -> Exp) -> [Name] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Exp
VarE [Name]
caseVars
in Name -> Type -> Exp -> Maybe Exp
forall a. Name -> Type -> a -> Maybe a
mbInductiveCase Name
dataName Type
varType Exp
inductiveArg
mkArg :: Exp -> (Name, Name, Type) -> Exp
mkArg Exp
f (Name
singVar, Name
singVarSig, Type
varType) =
Exp -> [Exp] -> Exp
foldAppE Exp
f ([Exp] -> Exp) -> [Exp] -> Exp
forall a b. (a -> b) -> a -> b
$ Name -> Exp
VarE Name
singVar
Exp -> [Exp] -> [Exp]
forall a. a -> [a] -> [a]
: Maybe Exp -> [Exp]
forall a. Maybe a -> [a]
maybeToList (Name -> Name -> Type -> Maybe Exp
mbInductiveArg Name
singVar Name
singVarSig Type
varType)
rhs :: Exp
rhs = (Exp -> (Name, Name, Type) -> Exp)
-> Exp -> [(Name, Name, Type)] -> Exp
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Exp -> (Name, Name, Type) -> Exp
mkArg (Name -> Exp
VarE Name
usedCaseVar) ([(Name, Name, Type)] -> Exp) -> [(Name, Name, Type)] -> Exp
forall a b. (a -> b) -> a -> b
$
[Name] -> [Name] -> [Type] -> [(Name, Name, Type)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Name]
singVars [Name]
singVarSigs [Type]
fieldTypes
Clause -> Q Clause
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Clause -> Q Clause) -> Clause -> Q Clause
forall a b. (a -> b) -> a -> b
$ [Pat] -> Body -> [Dec] -> Clause
Clause (Name -> [Pat] -> Pat
ConP Name
singConName [Pat]
singVarPats Pat -> [Pat] -> [Pat]
forall a. a -> [a] -> [a]
: (Name -> Pat) -> [Name] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Pat
VarP [Name]
caseVars)
(Exp -> Body
NormalB Exp
rhs)
[]
caseTySynEqn ::
Name
-> Name
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> Int
-> [Type]
-> ConstructorInfo
-> Q TySynEqn
caseTySynEqn :: Name
-> Name
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> Int
-> [Type]
-> ConstructorInfo
-> Q TySynEqn
caseTySynEqn Name
elimName Name
dataName [TyVarBndrUnit]
dataVarBndrs TyVarBndrUnit
predVarBndr Int
conIndex [Type]
caseTypes
(ConstructorInfo { constructorName :: ConstructorInfo -> Name
constructorName = Name
conName
, constructorFields :: ConstructorInfo -> [Type]
constructorFields = [Type]
fieldTypes })
= do let dataVarNames :: [Name]
dataVarNames = (TyVarBndrUnit -> Name) -> [TyVarBndrUnit] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map TyVarBndrUnit -> Name
forall flag. TyVarBndr_ flag -> Name
tvName [TyVarBndrUnit]
dataVarBndrs
predVarName :: Name
predVarName = TyVarBndrUnit -> Name
forall flag. TyVarBndr_ flag -> Name
tvName TyVarBndrUnit
predVarBndr
numFields :: Int
numFields = [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
fieldTypes
[Name]
singVars <- String -> Int -> Q [Name]
newNameList String
"s" Int
numFields
Name
usedCaseVar <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"useThis"
[TyVarBndrUnit]
caseVarBndrs <- ((Int -> Type -> Q TyVarBndrUnit) -> [Type] -> Q [TyVarBndrUnit])
-> [Type] -> (Int -> Type -> Q TyVarBndrUnit) -> Q [TyVarBndrUnit]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Int -> Type -> Q TyVarBndrUnit) -> [Type] -> Q [TyVarBndrUnit]
forall (f :: * -> *) a b.
Applicative f =>
(Int -> a -> f b) -> [a] -> f [b]
itraverse [Type]
caseTypes ((Int -> Type -> Q TyVarBndrUnit) -> Q [TyVarBndrUnit])
-> (Int -> Type -> Q TyVarBndrUnit) -> Q [TyVarBndrUnit]
forall a b. (a -> b) -> a -> b
$ \Int
i Type
caseTy ->
let mkVarName :: Q Name
mkVarName
| Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
conIndex = Name -> Q Name
forall (f :: * -> *) a. Applicative f => a -> f a
pure Name
usedCaseVar
| Bool
otherwise = String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName (String
"_p" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i)
in (Name -> Type -> TyVarBndrUnit)
-> Q Name -> Q Type -> Q TyVarBndrUnit
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Name -> Type -> TyVarBndrUnit
kindedTV Q Name
mkVarName (Type -> Q Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
caseTy)
let caseVarNames :: [Name]
caseVarNames = (TyVarBndrUnit -> Name) -> [TyVarBndrUnit] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map TyVarBndrUnit -> Name
forall flag. TyVarBndr_ flag -> Name
tvName [TyVarBndrUnit]
caseVarBndrs
prefix :: Type
prefix = Type -> [Type] -> Type
foldAppKindT (Name -> Type
ConT Name
elimName) ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ (Name -> Type) -> [Name] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Type
VarT [Name]
dataVarNames
mbInductiveArg :: Name -> Type -> Maybe Type
mbInductiveArg Name
singVar Type
varType =
let inductiveArg :: Type
inductiveArg = Type -> [Type] -> Type
foldAppT Type
prefix ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ Name -> Type
VarT Name
predVarName
Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: Name -> Type
VarT Name
singVar
Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: (Name -> Type) -> [Name] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Type
VarT [Name]
caseVarNames
in Name -> Type -> Type -> Maybe Type
forall a. Name -> Type -> a -> Maybe a
mbInductiveCase Name
dataName Type
varType Type
inductiveArg
mkArg :: Type -> (Name, Type) -> Type
mkArg Type
f (Name
singVar, Type
varType) =
Type -> [Type] -> Type
foldAppDefunT (Type
f Type -> Type -> Type
`AppT` Name -> Type
VarT Name
singVar)
([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ Maybe Type -> [Type]
forall a. Maybe a -> [a]
maybeToList (Name -> Type -> Maybe Type
mbInductiveArg Name
singVar Type
varType)
bndrs :: [TyVarBndrUnit]
bndrs = [TyVarBndrUnit]
dataVarBndrs [TyVarBndrUnit] -> [TyVarBndrUnit] -> [TyVarBndrUnit]
forall a. [a] -> [a] -> [a]
++ TyVarBndrUnit
predVarBndr TyVarBndrUnit -> [TyVarBndrUnit] -> [TyVarBndrUnit]
forall a. a -> [a] -> [a]
: [TyVarBndrUnit]
caseVarBndrs [TyVarBndrUnit] -> [TyVarBndrUnit] -> [TyVarBndrUnit]
forall a. [a] -> [a] -> [a]
++ (Name -> TyVarBndrUnit) -> [Name] -> [TyVarBndrUnit]
forall a b. (a -> b) -> [a] -> [b]
map Name -> TyVarBndrUnit
plainTV [Name]
singVars
lhs :: Type
lhs = Type -> [Type] -> Type
foldAppT Type
prefix ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ Name -> Type
VarT Name
predVarName
Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: Type -> [Type] -> Type
foldAppT (Name -> Type
ConT Name
conName) ((Name -> Type) -> [Name] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Type
VarT [Name]
singVars)
Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: (Name -> Type) -> [Name] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Type
VarT [Name]
caseVarNames
rhs :: Type
rhs = (Type -> (Name, Type) -> Type) -> Type -> [(Name, Type)] -> Type
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Type -> (Name, Type) -> Type
mkArg (Name -> Type
VarT Name
usedCaseVar) ([(Name, Type)] -> Type) -> [(Name, Type)] -> Type
forall a b. (a -> b) -> a -> b
$ [Name] -> [Type] -> [(Name, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
singVars [Type]
fieldTypes
TySynEqn -> Q TySynEqn
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TySynEqn -> Q TySynEqn) -> TySynEqn -> Q TySynEqn
forall a b. (a -> b) -> a -> b
$ Maybe [TyVarBndrUnit] -> Type -> Type -> TySynEqn
TySynEqn ([TyVarBndrUnit] -> Maybe [TyVarBndrUnit]
forall a. a -> Maybe a
Just [TyVarBndrUnit]
bndrs) Type
lhs Type
rhs
data TermOrType
= IsTerm
| IsType
class Eliminator (t :: TermOrType) where
elimSigD ::
proxy t
-> Name
-> Type
-> Dec
elimTypeSig ::
proxy t
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> TyVarBndrUnit
-> [Type]
-> Type
-> Type
prependElimCaseTypeVar ::
proxy t
-> Name
-> Name
-> Name
-> Kind
-> Type
-> Type
qElimEqns ::
proxy t
-> Name
-> Name
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> TyVarBndrUnit
-> [Type]
-> [ConstructorInfo]
-> Q Dec
instance Eliminator IsTerm where
elimSigD :: forall (proxy :: TermOrType -> *).
proxy 'IsTerm -> Name -> Type -> Dec
elimSigD proxy 'IsTerm
_ = Name -> Type -> Dec
SigD
elimTypeSig :: forall (proxy :: TermOrType -> *).
proxy 'IsTerm
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> TyVarBndrUnit
-> [Type]
-> Type
-> Type
elimTypeSig proxy 'IsTerm
_ [TyVarBndrUnit]
dataVarBndrs TyVarBndrUnit
predVarBndr TyVarBndrUnit
singVarBndr [Type]
caseTypes Type
returnType =
[TyVarBndr Specificity] -> [Type] -> Type -> Type
ForallT (Specificity -> [TyVarBndrUnit] -> [TyVarBndr Specificity]
forall newFlag oldFlag.
newFlag -> [TyVarBndr_ oldFlag] -> [TyVarBndr_ newFlag]
changeTVFlags Specificity
SpecifiedSpec ([TyVarBndrUnit] -> [TyVarBndr Specificity])
-> [TyVarBndrUnit] -> [TyVarBndr Specificity]
forall a b. (a -> b) -> a -> b
$
[TyVarBndrUnit]
dataVarBndrs [TyVarBndrUnit] -> [TyVarBndrUnit] -> [TyVarBndrUnit]
forall a. [a] -> [a] -> [a]
++ [TyVarBndrUnit
predVarBndr, TyVarBndrUnit
singVarBndr]) [] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
[Type] -> Type -> Type
ravel (Name -> Type
singType (TyVarBndrUnit -> Name
forall flag. TyVarBndr_ flag -> Name
tvName TyVarBndrUnit
singVarBndr)Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
caseTypes) Type
returnType
prependElimCaseTypeVar :: forall (proxy :: TermOrType -> *).
proxy 'IsTerm -> Name -> Name -> Name -> Type -> Type -> Type
prependElimCaseTypeVar proxy 'IsTerm
_ Name
dataName Name
predVar Name
var Type
varType Type
t =
[TyVarBndr Specificity] -> [Type] -> Type -> Type
ForallT [Name -> Type -> TyVarBndr Specificity
kindedTVSpecified Name
var Type
varType] [] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
[Type] -> Type -> Type
ravel (Name -> Type
singType Name
varType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:Maybe Type -> [Type]
forall a. Maybe a -> [a]
maybeToList (Name -> Name -> Name -> Type -> Maybe Type
mbInductiveType Name
dataName Name
predVar Name
var Type
varType)) Type
t
qElimEqns :: forall (proxy :: TermOrType -> *).
proxy 'IsTerm
-> Name
-> Name
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> TyVarBndrUnit
-> [Type]
-> [ConstructorInfo]
-> Q Dec
qElimEqns proxy 'IsTerm
_ Name
elimName Name
dataName [TyVarBndrUnit]
dataVarBndrs TyVarBndrUnit
predVarBndr TyVarBndrUnit
_singVarBndr [Type]
_caseTypes [ConstructorInfo]
cons
| [ConstructorInfo] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ConstructorInfo]
cons
= do Name
singVal <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"singVal"
Dec -> Q Dec
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dec -> Q Dec) -> Dec -> Q Dec
forall a b. (a -> b) -> a -> b
$ Name -> [Clause] -> Dec
FunD Name
elimName [[Pat] -> Body -> [Dec] -> Clause
Clause [Name -> Pat
VarP Name
singVal]
(Exp -> Body
NormalB (Exp -> [Match] -> Exp
CaseE (Name -> Exp
VarE Name
singVal) [])) []]
| Bool
otherwise
= do [Clause]
caseClauses
<- (Int -> ConstructorInfo -> Q Clause)
-> [ConstructorInfo] -> Q [Clause]
forall (f :: * -> *) a b.
Applicative f =>
(Int -> a -> f b) -> [a] -> f [b]
itraverse (\Int
i -> Name
-> Name
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> Int
-> Int
-> ConstructorInfo
-> Q Clause
caseClause Name
elimName Name
dataName
[TyVarBndrUnit]
dataVarBndrs TyVarBndrUnit
predVarBndr Int
i ([ConstructorInfo] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ConstructorInfo]
cons)) [ConstructorInfo]
cons
Dec -> Q Dec
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dec -> Q Dec) -> Dec -> Q Dec
forall a b. (a -> b) -> a -> b
$ Name -> [Clause] -> Dec
FunD Name
elimName [Clause]
caseClauses
instance Eliminator IsType where
elimSigD :: forall (proxy :: TermOrType -> *).
proxy 'IsType -> Name -> Type -> Dec
elimSigD proxy 'IsType
_ = Name -> Type -> Dec
KiSigD
elimTypeSig :: forall (proxy :: TermOrType -> *).
proxy 'IsType
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> TyVarBndrUnit
-> [Type]
-> Type
-> Type
elimTypeSig proxy 'IsType
_ [TyVarBndrUnit]
dataVarBndrs TyVarBndrUnit
predVarBndr TyVarBndrUnit
singVarBndr [Type]
caseTypes Type
returnType =
[TyVarBndr Specificity] -> [Type] -> Type -> Type
ForallT (Specificity -> [TyVarBndrUnit] -> [TyVarBndr Specificity]
forall newFlag oldFlag.
newFlag -> [TyVarBndr_ oldFlag] -> [TyVarBndr_ newFlag]
changeTVFlags Specificity
SpecifiedSpec [TyVarBndrUnit]
dataVarBndrs) [] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
[TyVarBndrUnit] -> Type -> Type
ForallVisT [TyVarBndrUnit
predVarBndr, TyVarBndrUnit
singVarBndr] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
[Type] -> Type -> Type
ravel [Type]
caseTypes Type
returnType
prependElimCaseTypeVar :: forall (proxy :: TermOrType -> *).
proxy 'IsType -> Name -> Name -> Name -> Type -> Type -> Type
prependElimCaseTypeVar proxy 'IsType
_ Name
dataName Name
predVar Name
var Type
varType Type
t =
[TyVarBndrUnit] -> Type -> Type
ForallVisT [Name -> Type -> TyVarBndrUnit
kindedTV Name
var Type
varType] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
[Type] -> Type -> Type
ravelDefun (Maybe Type -> [Type]
forall a. Maybe a -> [a]
maybeToList (Name -> Name -> Name -> Type -> Maybe Type
mbInductiveType Name
dataName Name
predVar Name
var Type
varType)) Type
t
qElimEqns :: forall (proxy :: TermOrType -> *).
proxy 'IsType
-> Name
-> Name
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> TyVarBndrUnit
-> [Type]
-> [ConstructorInfo]
-> Q Dec
qElimEqns proxy 'IsType
_ Name
elimName Name
dataName [TyVarBndrUnit]
dataVarBndrs TyVarBndrUnit
predVarBndr TyVarBndrUnit
singVarBndr [Type]
caseTypes [ConstructorInfo]
cons = do
[TyVarBndrUnit]
caseVarBndrs <- Int -> Q TyVarBndrUnit -> Q [TyVarBndrUnit]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM ([Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
caseTypes) (Name -> TyVarBndrUnit
plainTV (Name -> TyVarBndrUnit) -> Q Name -> Q TyVarBndrUnit
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"p")
let predVar :: Name
predVar = TyVarBndrUnit -> Name
forall flag. TyVarBndr_ flag -> Name
tvName TyVarBndrUnit
predVarBndr
singVar :: Name
singVar = TyVarBndrUnit -> Name
forall flag. TyVarBndr_ flag -> Name
tvName TyVarBndrUnit
singVarBndr
tyFamHead :: TypeFamilyHead
tyFamHead = Name
-> [TyVarBndrUnit]
-> FamilyResultSig
-> Maybe InjectivityAnn
-> TypeFamilyHead
TypeFamilyHead Name
elimName
(Name -> TyVarBndrUnit
plainTV Name
predVarTyVarBndrUnit -> [TyVarBndrUnit] -> [TyVarBndrUnit]
forall a. a -> [a] -> [a]
:Name -> TyVarBndrUnit
plainTV Name
singVarTyVarBndrUnit -> [TyVarBndrUnit] -> [TyVarBndrUnit]
forall a. a -> [a] -> [a]
:[TyVarBndrUnit]
caseVarBndrs)
FamilyResultSig
NoSig Maybe InjectivityAnn
forall a. Maybe a
Nothing
[TySynEqn]
caseEqns <- (Int -> ConstructorInfo -> Q TySynEqn)
-> [ConstructorInfo] -> Q [TySynEqn]
forall (f :: * -> *) a b.
Applicative f =>
(Int -> a -> f b) -> [a] -> f [b]
itraverse (\Int
i -> Name
-> Name
-> [TyVarBndrUnit]
-> TyVarBndrUnit
-> Int
-> [Type]
-> ConstructorInfo
-> Q TySynEqn
caseTySynEqn Name
elimName Name
dataName
[TyVarBndrUnit]
dataVarBndrs TyVarBndrUnit
predVarBndr Int
i [Type]
caseTypes) [ConstructorInfo]
cons
Dec -> Q Dec
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dec -> Q Dec) -> Dec -> Q Dec
forall a b. (a -> b) -> a -> b
$ TypeFamilyHead -> [TySynEqn] -> Dec
ClosedTypeFamilyD TypeFamilyHead
tyFamHead [TySynEqn]
caseEqns
mbInductiveType :: Name -> Name -> Name -> Kind -> Maybe Type
mbInductiveType :: Name -> Name -> Name -> Type -> Maybe Type
mbInductiveType Name
dataName Name
predVar Name
var Type
varType =
Name -> Type -> Type -> Maybe Type
forall a. Name -> Type -> a -> Maybe a
mbInductiveCase Name
dataName Type
varType (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Name -> Type -> Type
predType Name
predVar (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Name -> Type
VarT Name
var
mbInductiveCase :: Name -> Type -> a -> Maybe a
mbInductiveCase :: forall a. Name -> Type -> a -> Maybe a
mbInductiveCase Name
dataName Type
varType a
inductiveArg
= case Type -> (Type, [TypeArg])
unfoldType Type
varType of
(Type
headTy, [TypeArg]
_)
| Type
ListT <- Type
headTy
, Name
dataName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''[]
-> a -> Maybe a
forall a. a -> Maybe a
Just a
inductiveArg
| ConT Name
n <- Type
headTy
, Name
dataName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n
-> a -> Maybe a
forall a. a -> Maybe a
Just a
inductiveArg
| Bool
otherwise
-> Maybe a
forall a. Maybe a
Nothing
singType :: Name -> Type
singType :: Name -> Type
singType Name
x = Name -> Type
ConT ''Sing Type -> Type -> Type
`AppT` Name -> Type
VarT Name
x
predType :: Name -> Type -> Type
predType :: Name -> Type -> Type
predType Name
p Type
ty = Name -> Type
ConT ''Apply Type -> Type -> Type
`AppT` Name -> Type
VarT Name
p Type -> Type -> Type
`AppT` Type
ty
newNameList :: String -> Int -> Q [Name]
newNameList :: String -> Int -> Q [Name]
newNameList String
prefix Int
n = Int -> (Int -> Q Name) -> Q [Name]
forall (f :: * -> *) a.
Applicative f =>
Int -> (Int -> f a) -> f [a]
ireplicateA Int
n ((Int -> Q Name) -> Q [Name]) -> (Int -> Q Name) -> Q [Name]
forall a b. (a -> b) -> a -> b
$ String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName (String -> Q Name) -> (Int -> String) -> Int -> Q Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
prefix String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (Int -> String) -> Int -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show
eliminatorName :: Name -> String
eliminatorName :: Name -> String
eliminatorName Name
n
| Char
first:String
_ <- String
nStr
, Char -> Bool
isUpper Char
first
= String
"elim" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nStr
| Bool
otherwise
= String
"~>" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nStr
where
nStr :: String
nStr = Name -> String
nameBase Name
n
ravel :: [Type] -> Type -> Type
ravel :: [Type] -> Type -> Type
ravel [Type]
args Type
res = [Type] -> Type
go [Type]
args
where
go :: [Type] -> Type
go [] = Type
res
go (Type
h:[Type]
t) = Type -> Type -> Type
AppT (Type -> Type -> Type
AppT Type
ArrowT Type
h) ([Type] -> Type
go [Type]
t)
ravelDefun :: [Type] -> Type -> Type
ravelDefun :: [Type] -> Type -> Type
ravelDefun [Type]
args Type
res = [Type] -> Type
go [Type]
args
where
go :: [Type] -> Type
go [] = Type
res
go (Type
h:[Type]
t) = Type -> Type -> Type
AppT (Type -> Type -> Type
AppT (Name -> Type
ConT ''(~>)) Type
h) ([Type] -> Type
go [Type]
t)
foldAppE :: Exp -> [Exp] -> Exp
foldAppE :: Exp -> [Exp] -> Exp
foldAppE = (Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Exp -> Exp -> Exp
AppE
foldAppTypeE :: Exp -> [Type] -> Exp
foldAppTypeE :: Exp -> [Type] -> Exp
foldAppTypeE = (Exp -> Type -> Exp) -> Exp -> [Type] -> Exp
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Exp -> Type -> Exp
AppTypeE
foldAppT :: Type -> [Type] -> Type
foldAppT :: Type -> [Type] -> Type
foldAppT = (Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Type -> Type -> Type
AppT
foldAppDefunT :: Type -> [Type] -> Type
foldAppDefunT :: Type -> [Type] -> Type
foldAppDefunT = (Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Type
x Type
y -> Name -> Type
ConT ''Apply Type -> Type -> Type
`AppT` Type
x Type -> Type -> Type
`AppT` Type
y)
foldAppKindT :: Type -> [Type] -> Type
foldAppKindT :: Type -> [Type] -> Type
foldAppKindT = (Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Type -> Type -> Type
AppKindT
itraverse :: Applicative f => (Int -> a -> f b) -> [a] -> f [b]
itraverse :: forall (f :: * -> *) a b.
Applicative f =>
(Int -> a -> f b) -> [a] -> f [b]
itraverse Int -> a -> f b
f [a]
xs0 = [a] -> Int -> f [b]
go [a]
xs0 Int
0 where
go :: [a] -> Int -> f [b]
go [] Int
_ = [b] -> f [b]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
go (a
x:[a]
xs) Int
n = (:) (b -> [b] -> [b]) -> f b -> f ([b] -> [b])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> a -> f b
f Int
n a
x f ([b] -> [b]) -> f [b] -> f [b]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([a] -> Int -> f [b]
go [a]
xs (Int -> f [b]) -> Int -> f [b]
forall a b. (a -> b) -> a -> b
$! (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1))
ireplicateA :: Applicative f => Int -> (Int -> f a) -> f [a]
ireplicateA :: forall (f :: * -> *) a.
Applicative f =>
Int -> (Int -> f a) -> f [a]
ireplicateA Int
cnt0 Int -> f a
f =
Int -> Int -> f [a]
forall {t}. (Ord t, Num t) => t -> Int -> f [a]
loop Int
cnt0 Int
0
where
loop :: t -> Int -> f [a]
loop t
cnt Int
n
| t
cnt t -> t -> Bool
forall a. Ord a => a -> a -> Bool
<= t
0 = [a] -> f [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
| Bool
otherwise = (a -> [a] -> [a]) -> f a -> f [a] -> f [a]
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (:) (Int -> f a
f Int
n) (t -> Int -> f [a]
loop (t
cnt t -> t -> t
forall a. Num a => a -> a -> a
- t
1) (Int -> f [a]) -> Int -> f [a]
forall a b. (a -> b) -> a -> b
$! (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1))
upcase :: String -> String
upcase :: String -> String
upcase String
str
| Char -> Bool
isHsLetter Char
first
= Char -> Char
toUpper Char
first Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
forall a. [a] -> [a]
tail String
str
| Bool
otherwise
= String
str
where
first :: Char
first = String -> Char
forall a. [a] -> a
head String
str
isHsLetter :: Char -> Bool
isHsLetter :: Char -> Bool
isHsLetter Char
c = Char -> Bool
isLetter Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_'