{-# 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.Prelude
import Data.Singletons.TH.Options
import Language.Haskell.TH
import Language.Haskell.TH.Datatype
import Language.Haskell.TH.Desugar hiding (NewOrData(..))
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' (Proxy 'IsTerm
forall k (t :: k). 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' (Proxy 'IsType
forall k (t :: k). Proxy t
Proxy @IsType)
deriveElimNamed' ::
Eliminator t
=> proxy t
-> String
-> Name
-> Q [Dec]
deriveElimNamed' :: proxy t -> String -> Name -> Q [Dec]
deriveElimNamed' proxy t
prox String
funName Name
dataName = do
info :: DatatypeInfo
info@(DatatypeInfo { datatypeVars :: DatatypeInfo -> [TyVarBndr]
datatypeVars = [TyVarBndr]
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
newName String
"p"
Name
singVar <- String -> Q Name
newName String
"s"
let elimName :: Name
elimName = String -> Name
mkName String
funName
promDataKind :: Type
promDataKind = DatatypeInfo -> Type
datatypeType DatatypeInfo
info
predVarBndr :: TyVarBndr
predVarBndr = Name -> Type -> TyVarBndr
KindedTV Name
predVar (Type -> Name -> Type -> Type
InfixT Type
promDataKind ''(~>) (Name -> Type
ConT ''Kind.Type))
singVarBndr :: TyVarBndr
singVarBndr = Name -> Type -> TyVarBndr
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
-> [TyVarBndr] -> TyVarBndr -> TyVarBndr -> [Type] -> Type -> Type
forall (t :: TermOrType) (proxy :: TermOrType -> *).
Eliminator t =>
proxy t
-> [TyVarBndr] -> TyVarBndr -> TyVarBndr -> [Type] -> Type -> Type
elimTypeSig proxy t
prox [TyVarBndr]
dataVarBndrs TyVarBndr
predVarBndr TyVarBndr
singVarBndr
[Type]
caseTypes Type
returnType
Dec
elimEqns <- proxy t
-> Name
-> Name
-> [TyVarBndr]
-> TyVarBndr
-> TyVarBndr
-> [Type]
-> [ConstructorInfo]
-> Q Dec
forall (t :: TermOrType) (proxy :: TermOrType -> *).
Eliminator t =>
proxy t
-> Name
-> Name
-> [TyVarBndr]
-> TyVarBndr
-> TyVarBndr
-> [Type]
-> [ConstructorInfo]
-> Q Dec
qElimEqns proxy t
prox (String -> Name
mkName String
funName) Name
dataName
[TyVarBndr]
dataVarBndrs TyVarBndr
predVarBndr TyVarBndr
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 :: proxy t -> Name -> Name -> ConstructorInfo -> Q Type
caseType proxy t
prox Name
dataName Name
predVar
(ConstructorInfo { constructorName :: ConstructorInfo -> Name
constructorName = Name
conName
, constructorVars :: ConstructorInfo -> [TyVarBndr]
constructorVars = [TyVarBndr]
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 ([TyVarBndr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVarBndr]
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
-> [TyVarBndr]
-> TyVarBndr
-> Int
-> Int
-> ConstructorInfo
-> Q Clause
caseClause :: Name
-> Name
-> [TyVarBndr]
-> TyVarBndr
-> Int
-> Int
-> ConstructorInfo
-> Q Clause
caseClause Name
elimName Name
dataName [TyVarBndr]
dataVarBndrs TyVarBndr
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
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
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
$ (TyVarBndr -> Type) -> [TyVarBndr] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Type
VarT (Name -> Type) -> (TyVarBndr -> Name) -> TyVarBndr -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr -> Name
tvName) [TyVarBndr]
dataVarBndrs
[Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Name -> Type
VarT (TyVarBndr -> Name
tvName TyVarBndr
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
-> [TyVarBndr]
-> TyVarBndr
-> Int
-> [Type]
-> ConstructorInfo
-> Q TySynEqn
caseTySynEqn :: Name
-> Name
-> [TyVarBndr]
-> TyVarBndr
-> Int
-> [Type]
-> ConstructorInfo
-> Q TySynEqn
caseTySynEqn Name
elimName Name
dataName [TyVarBndr]
dataVarBndrs TyVarBndr
predVarBndr Int
conIndex [Type]
caseTypes
(ConstructorInfo { constructorName :: ConstructorInfo -> Name
constructorName = Name
conName
, constructorFields :: ConstructorInfo -> [Type]
constructorFields = [Type]
fieldTypes })
= do let dataVarNames :: [Name]
dataVarNames = (TyVarBndr -> Name) -> [TyVarBndr] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map TyVarBndr -> Name
tvName [TyVarBndr]
dataVarBndrs
predVarName :: Name
predVarName = TyVarBndr -> Name
tvName TyVarBndr
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
newName String
"useThis"
[TyVarBndr]
caseVarBndrs <- ((Int -> Type -> Q TyVarBndr) -> [Type] -> Q [TyVarBndr])
-> [Type] -> (Int -> Type -> Q TyVarBndr) -> Q [TyVarBndr]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Int -> Type -> Q TyVarBndr) -> [Type] -> Q [TyVarBndr]
forall (f :: * -> *) a b.
Applicative f =>
(Int -> a -> f b) -> [a] -> f [b]
itraverse [Type]
caseTypes ((Int -> Type -> Q TyVarBndr) -> Q [TyVarBndr])
-> (Int -> Type -> Q TyVarBndr) -> Q [TyVarBndr]
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
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 -> TyVarBndr) -> Q Name -> Q Type -> Q TyVarBndr
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Name -> Type -> TyVarBndr
KindedTV Q Name
mkVarName (Type -> Q Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
caseTy)
let caseVarNames :: [Name]
caseVarNames = (TyVarBndr -> Name) -> [TyVarBndr] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map TyVarBndr -> Name
tvName [TyVarBndr]
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 :: [TyVarBndr]
bndrs = [TyVarBndr]
dataVarBndrs [TyVarBndr] -> [TyVarBndr] -> [TyVarBndr]
forall a. [a] -> [a] -> [a]
++ TyVarBndr
predVarBndr TyVarBndr -> [TyVarBndr] -> [TyVarBndr]
forall a. a -> [a] -> [a]
: [TyVarBndr]
caseVarBndrs [TyVarBndr] -> [TyVarBndr] -> [TyVarBndr]
forall a. [a] -> [a] -> [a]
++ (Name -> TyVarBndr) -> [Name] -> [TyVarBndr]
forall a b. (a -> b) -> [a] -> [b]
map Name -> TyVarBndr
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 [TyVarBndr] -> Type -> Type -> TySynEqn
TySynEqn ([TyVarBndr] -> Maybe [TyVarBndr]
forall a. a -> Maybe a
Just [TyVarBndr]
bndrs) Type
lhs Type
rhs
data TermOrType
= IsTerm
| IsType
class Eliminator (t :: TermOrType) where
elimSigD ::
proxy t
-> Name
-> Type
-> Dec
elimTypeSig ::
proxy t
-> [TyVarBndr]
-> TyVarBndr
-> TyVarBndr
-> [Type]
-> Type
-> Type
prependElimCaseTypeVar ::
proxy t
-> Name
-> Name
-> Name
-> Kind
-> Type
-> Type
qElimEqns ::
proxy t
-> Name
-> Name
-> [TyVarBndr]
-> TyVarBndr
-> TyVarBndr
-> [Type]
-> [ConstructorInfo]
-> Q Dec
instance Eliminator IsTerm where
elimSigD :: proxy 'IsTerm -> Name -> Type -> Dec
elimSigD proxy 'IsTerm
_ = Name -> Type -> Dec
SigD
elimTypeSig :: proxy 'IsTerm
-> [TyVarBndr] -> TyVarBndr -> TyVarBndr -> [Type] -> Type -> Type
elimTypeSig proxy 'IsTerm
_ [TyVarBndr]
dataVarBndrs TyVarBndr
predVarBndr TyVarBndr
singVarBndr [Type]
caseTypes Type
returnType =
[TyVarBndr] -> [Type] -> Type -> Type
ForallT ([TyVarBndr]
dataVarBndrs [TyVarBndr] -> [TyVarBndr] -> [TyVarBndr]
forall a. [a] -> [a] -> [a]
++ [TyVarBndr
predVarBndr, TyVarBndr
singVarBndr]) [] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
[Type] -> Type -> Type
ravel (Name -> Type
singType (TyVarBndr -> Name
tvName TyVarBndr
singVarBndr)Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
caseTypes) Type
returnType
prependElimCaseTypeVar :: proxy 'IsTerm -> Name -> Name -> Name -> Type -> Type -> Type
prependElimCaseTypeVar proxy 'IsTerm
_ Name
dataName Name
predVar Name
var Type
varType Type
t =
[TyVarBndr] -> [Type] -> Type -> Type
ForallT [Name -> Type -> TyVarBndr
KindedTV 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 :: proxy 'IsTerm
-> Name
-> Name
-> [TyVarBndr]
-> TyVarBndr
-> TyVarBndr
-> [Type]
-> [ConstructorInfo]
-> Q Dec
qElimEqns proxy 'IsTerm
_ Name
elimName Name
dataName [TyVarBndr]
dataVarBndrs TyVarBndr
predVarBndr TyVarBndr
_singVarBndr [Type]
_caseTypes [ConstructorInfo]
cons
| [ConstructorInfo] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ConstructorInfo]
cons
= do Name
singVal <- String -> Q 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
-> [TyVarBndr]
-> TyVarBndr
-> Int
-> Int
-> ConstructorInfo
-> Q Clause
caseClause Name
elimName Name
dataName
[TyVarBndr]
dataVarBndrs TyVarBndr
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 :: proxy 'IsType -> Name -> Type -> Dec
elimSigD proxy 'IsType
_ = Name -> Type -> Dec
KiSigD
elimTypeSig :: proxy 'IsType
-> [TyVarBndr] -> TyVarBndr -> TyVarBndr -> [Type] -> Type -> Type
elimTypeSig proxy 'IsType
_ [TyVarBndr]
dataVarBndrs TyVarBndr
predVarBndr TyVarBndr
singVarBndr [Type]
caseTypes Type
returnType =
[TyVarBndr] -> [Type] -> Type -> Type
ForallT [TyVarBndr]
dataVarBndrs [] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
[TyVarBndr] -> Type -> Type
ForallVisT [TyVarBndr
predVarBndr, TyVarBndr
singVarBndr] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
[Type] -> Type -> Type
ravel [Type]
caseTypes Type
returnType
prependElimCaseTypeVar :: proxy 'IsType -> Name -> Name -> Name -> Type -> Type -> Type
prependElimCaseTypeVar proxy 'IsType
_ Name
dataName Name
predVar Name
var Type
varType Type
t =
[TyVarBndr] -> Type -> Type
ForallVisT [Name -> Type -> TyVarBndr
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 :: proxy 'IsType
-> Name
-> Name
-> [TyVarBndr]
-> TyVarBndr
-> TyVarBndr
-> [Type]
-> [ConstructorInfo]
-> Q Dec
qElimEqns proxy 'IsType
_ Name
elimName Name
dataName [TyVarBndr]
dataVarBndrs TyVarBndr
predVarBndr TyVarBndr
singVarBndr [Type]
caseTypes [ConstructorInfo]
cons = do
[TyVarBndr]
caseVarBndrs <- Int -> Q TyVarBndr -> Q [TyVarBndr]
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 -> TyVarBndr
PlainTV (Name -> TyVarBndr) -> Q Name -> Q TyVarBndr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Q Name
newName String
"p")
let predVar :: Name
predVar = TyVarBndr -> Name
tvName TyVarBndr
predVarBndr
singVar :: Name
singVar = TyVarBndr -> Name
tvName TyVarBndr
singVarBndr
tyFamHead :: TypeFamilyHead
tyFamHead = Name
-> [TyVarBndr]
-> FamilyResultSig
-> Maybe InjectivityAnn
-> TypeFamilyHead
TypeFamilyHead Name
elimName
(Name -> TyVarBndr
PlainTV Name
predVarTyVarBndr -> [TyVarBndr] -> [TyVarBndr]
forall a. a -> [a] -> [a]
:Name -> TyVarBndr
PlainTV Name
singVarTyVarBndr -> [TyVarBndr] -> [TyVarBndr]
forall a. a -> [a] -> [a]
:[TyVarBndr]
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
-> [TyVarBndr]
-> TyVarBndr
-> Int
-> [Type]
-> ConstructorInfo
-> Q TySynEqn
caseTySynEqn Name
elimName Name
dataName
[TyVarBndr]
dataVarBndrs TyVarBndr
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 :: 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
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 :: (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 :: 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
'_'