{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TemplateHaskellQuotes #-}
{-# 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
, datatypeInstTypes :: DatatypeInfo -> [Type]
datatypeInstTypes = [Type]
instTys
, 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 a. 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 a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
DatatypeVariant
Newtype -> () -> Q ()
forall a. a -> Q a
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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [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
Bool -> Q () -> Q ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Int] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (DatatypeInfo -> [Int]
findParams DatatypeInfo
info) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
instTys) (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$
String -> Q ()
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Eliminators for polymorphically recursive data types are currently not supported"
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
forall (proxy :: TermOrType -> *).
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
forall (proxy :: TermOrType -> *).
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 a. a -> Q a
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
forall (proxy :: TermOrType -> *). 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 a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVarBndrUnit]
conVars Bool -> Bool -> Bool
&& [Type] -> Bool
forall a. [a] -> 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 a. String -> Q a
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 a. [a] -> 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 b a. (b -> a -> b) -> b -> [a] -> b
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 a. a -> Q a
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 a b. (a -> b -> b) -> b -> [a] -> b
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
forall (proxy :: TermOrType -> *).
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)
goCaseClause ::
Name
-> Name
-> Name
-> ConstructorInfo
-> Q Clause
goCaseClause :: Name -> Name -> Name -> ConstructorInfo -> Q Clause
goCaseClause Name
goName Name
dataName Name
usedCaseVar
(ConstructorInfo { constructorName :: ConstructorInfo -> Name
constructorName = Name
conName
, constructorFields :: ConstructorInfo -> [Type]
constructorFields = [Type]
fieldTypes })
= do let numFields :: Int
numFields = [Type] -> Int
forall a. [a] -> 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
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 inductiveArg :: Exp
inductiveArg = Name -> Exp
VarE Name
goName Exp -> Type -> Exp
`AppTypeE` Name -> Type
VarT Name
singVarSig
Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
singVar
in Name -> Type -> ([TypeArg] -> Exp) -> Maybe Exp
forall a. Name -> Type -> ([TypeArg] -> a) -> Maybe a
mbInductiveCase Name
dataName Type
varType (([TypeArg] -> Exp) -> Maybe Exp)
-> ([TypeArg] -> Exp) -> Maybe Exp
forall a b. (a -> b) -> a -> b
$ Exp -> [TypeArg] -> Exp
forall a b. a -> b -> a
const 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 b a. (b -> a -> b) -> b -> [a] -> b
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 a. a -> Q a
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 -> [Type] -> [Pat] -> Pat
ConP Name
singConName [] [Pat]
singVarPats]
(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 a. [a] -> 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 a. a -> Q a
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 a b c. (a -> b -> c) -> Q a -> Q b -> Q c
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 a. a -> Q a
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 -> ([TypeArg] -> Type) -> Maybe Type
forall a. Name -> Type -> ([TypeArg] -> a) -> Maybe a
mbInductiveCase Name
dataName Type
varType (([TypeArg] -> Type) -> Maybe Type)
-> ([TypeArg] -> Type) -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Type -> [TypeArg] -> Type
forall a b. a -> b -> a
const 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 b a. (b -> a -> b) -> b -> [a] -> b
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 a. a -> Q a
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 = do
Name
singTermVar <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"s"
[Name]
caseVars <- String -> Int -> Q [Name]
newNameList String
"p" (Int -> Q [Name]) -> Int -> Q [Name]
forall a b. (a -> b) -> a -> b
$ [ConstructorInfo] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ConstructorInfo]
cons
Name
goName <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"go"
let singTypeVar :: Name
singTypeVar = TyVarBndrUnit -> Name
forall flag. TyVarBndr_ flag -> Name
tvName TyVarBndrUnit
singVarBndr
Name
goSingTypeVar <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName (String -> Q Name) -> String -> Q Name
forall a b. (a -> b) -> a -> b
$ Name -> String
nameBase Name
singTypeVar
let elimRHS :: Exp
elimRHS = Name -> Exp
VarE Name
goName Exp -> Type -> Exp
`AppTypeE` Name -> Type
VarT Name
singTypeVar Exp -> Exp -> Exp
`AppE` Name -> Exp
VarE Name
singTermVar
goSingVarBndr :: TyVarBndrUnit
goSingVarBndr = (Name -> Name) -> TyVarBndrUnit -> TyVarBndrUnit
forall flag. (Name -> Name) -> TyVarBndr_ flag -> TyVarBndr_ flag
mapTVName (Name -> Name -> Name
forall a b. a -> b -> a
const Name
goSingTypeVar) TyVarBndrUnit
singVarBndr
goReturnType :: Type
goReturnType = Name -> Type -> Type
predType (TyVarBndrUnit -> Name
forall flag. TyVarBndr_ flag -> Name
tvName TyVarBndrUnit
predVarBndr) (Name -> Type
VarT Name
goSingTypeVar)
goType :: Type
goType = [TyVarBndr Specificity] -> [Type] -> Type -> Type
ForallT (Specificity -> [TyVarBndrUnit] -> [TyVarBndr Specificity]
forall newFlag oldFlag.
newFlag -> [TyVarBndr_ oldFlag] -> [TyVarBndr_ newFlag]
changeTVFlags Specificity
SpecifiedSpec [TyVarBndrUnit
goSingVarBndr]) [] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
Type
ArrowT Type -> Type -> Type
`AppT` Name -> Type
singType Name
goSingTypeVar Type -> Type -> Type
`AppT` Type
goReturnType
[Clause]
goClauses
<- if [ConstructorInfo] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ConstructorInfo]
cons
then [Clause] -> Q [Clause]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [[Pat] -> Body -> [Dec] -> Clause
Clause [Name -> Pat
VarP Name
singTermVar] (Exp -> Body
NormalB (Exp -> [Match] -> Exp
CaseE (Name -> Exp
VarE Name
singTermVar) [])) []]
else (Name -> ConstructorInfo -> Q Clause)
-> [Name] -> [ConstructorInfo] -> Q [Clause]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (Name -> Name -> Name -> ConstructorInfo -> Q Clause
goCaseClause Name
goName Name
dataName) [Name]
caseVars [ConstructorInfo]
cons
Dec -> Q Dec
forall a. a -> Q a
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) -> [Name] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Pat
VarP (Name
singTermVarName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
caseVars)) (Exp -> Body
NormalB Exp
elimRHS)
[Name -> Type -> Dec
SigD Name
goName Type
goType, Name -> [Clause] -> Dec
FunD Name
goName [Clause]
goClauses] ]
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 a. [a] -> 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 a. a -> Q a
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 -> ([TypeArg] -> Type) -> Maybe Type
forall a. Name -> Type -> ([TypeArg] -> a) -> Maybe a
mbInductiveCase Name
dataName Type
varType (([TypeArg] -> Type) -> Maybe Type)
-> ([TypeArg] -> Type) -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Type -> [TypeArg] -> Type
forall a b. a -> b -> a
const (Type -> [TypeArg] -> Type) -> Type -> [TypeArg] -> 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 -> ([TypeArg] -> a) -> Maybe a
mbInductiveCase :: forall a. Name -> Type -> ([TypeArg] -> a) -> Maybe a
mbInductiveCase Name
dataName Type
varType [TypeArg] -> a
inductiveArg
= case Type -> (Type, [TypeArg])
unfoldType Type
varType of
(Type
headTy, [TypeArg]
argTys)
| 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 -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ [TypeArg] -> a
inductiveArg [TypeArg]
argTys
| 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 -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ [TypeArg] -> a
inductiveArg [TypeArg]
argTys
| 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) -> (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 b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Exp -> Exp -> Exp
AppE
foldAppT :: Type -> [Type] -> Type
foldAppT :: Type -> [Type] -> Type
foldAppT = (Type -> Type -> Type) -> Type -> [Type] -> Type
forall b a. (b -> a -> b) -> b -> [a] -> b
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 b a. (b -> a -> b) -> b -> [a] -> b
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 b a. (b -> a -> b) -> b -> [a] -> b
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 a. a -> f a
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 a b. f (a -> b) -> f a -> 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 a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
| Bool
otherwise = (a -> [a] -> [a]) -> f a -> f [a] -> f [a]
forall a b c. (a -> b -> c) -> f a -> f b -> f c
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))
findParams :: DatatypeInfo -> [Int]
findParams :: DatatypeInfo -> [Int]
findParams (DatatypeInfo { datatypeName :: DatatypeInfo -> Name
datatypeName = Name
dataName
, datatypeInstTypes :: DatatypeInfo -> [Type]
datatypeInstTypes = [Type]
instTys
, datatypeCons :: DatatypeInfo -> [ConstructorInfo]
datatypeCons = [ConstructorInfo]
cons
}) =
let allapps :: [[[Maybe Name]]]
allapps = (ConstructorInfo -> [[Maybe Name]])
-> [ConstructorInfo] -> [[[Maybe Name]]]
forall a b. (a -> b) -> [a] -> [b]
map ConstructorInfo -> [[Maybe Name]]
getDataApp [ConstructorInfo]
cons
conParams :: [[Int]]
conParams = ([[Maybe Name]] -> [Int]) -> [[[Maybe Name]]] -> [[Int]]
forall a b. (a -> b) -> [a] -> [b]
map [[Maybe Name]] -> [Int]
forall name. Eq name => [[Maybe name]] -> [Int]
paramPos [[[Maybe Name]]]
allapps
in [[Int]] -> [Int]
forall pos. Eq pos => [[pos]] -> [pos]
inAll [[Int]]
conParams
where
inAll :: Eq pos => [[pos]] -> [pos]
inAll :: forall pos. Eq pos => [[pos]] -> [pos]
inAll [] = []
inAll ([pos]
x : [[pos]]
xs) = (pos -> Bool) -> [pos] -> [pos]
forall a. (a -> Bool) -> [a] -> [a]
filter (\pos
p -> ([pos] -> Bool) -> [[pos]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\[pos]
ps -> pos
p pos -> [pos] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [pos]
ps) [[pos]]
xs) [pos]
x
paramPos :: Eq name => [[Maybe name]] -> [Int]
paramPos :: forall name. Eq name => [[Maybe name]] -> [Int]
paramPos [] = []
paramPos ([Maybe name]
args : [[Maybe name]]
rest)
= [(Int, Maybe name)] -> [Int]
forall pos name. [(pos, Maybe name)] -> [pos]
dropNothing ([(Int, Maybe name)] -> [Int]) -> [(Int, Maybe name)] -> [Int]
forall a b. (a -> b) -> a -> b
$ [(Int, Maybe name)] -> [[Maybe name]] -> [(Int, Maybe name)]
forall name pos.
Eq name =>
[(pos, Maybe name)] -> [[Maybe name]] -> [(pos, Maybe name)]
keepSame ([Int] -> [Maybe name] -> [(Int, Maybe name)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [Maybe name]
args) [[Maybe name]]
rest
dropNothing :: [(pos, Maybe name)] -> [pos]
dropNothing :: forall pos name. [(pos, Maybe name)] -> [pos]
dropNothing [] = []
dropNothing ((pos
_, Maybe name
Nothing) : [(pos, Maybe name)]
ts) = [(pos, Maybe name)] -> [pos]
forall pos name. [(pos, Maybe name)] -> [pos]
dropNothing [(pos, Maybe name)]
ts
dropNothing ((pos
x, Maybe name
_) : [(pos, Maybe name)]
ts) = pos
x pos -> [pos] -> [pos]
forall a. a -> [a] -> [a]
: [(pos, Maybe name)] -> [pos]
forall pos name. [(pos, Maybe name)] -> [pos]
dropNothing [(pos, Maybe name)]
ts
keepSame :: Eq name =>
[(pos, Maybe name)] -> [[Maybe name]] ->
[(pos, Maybe name)]
keepSame :: forall name pos.
Eq name =>
[(pos, Maybe name)] -> [[Maybe name]] -> [(pos, Maybe name)]
keepSame [(pos, Maybe name)]
as [] = [(pos, Maybe name)]
as
keepSame [(pos, Maybe name)]
as ([Maybe name]
args : [[Maybe name]]
rest) = [(pos, Maybe name)] -> [[Maybe name]] -> [(pos, Maybe name)]
forall name pos.
Eq name =>
[(pos, Maybe name)] -> [[Maybe name]] -> [(pos, Maybe name)]
keepSame ([(pos, Maybe name)] -> [Maybe name] -> [(pos, Maybe name)]
forall name pos.
Eq name =>
[(pos, Maybe name)] -> [Maybe name] -> [(pos, Maybe name)]
update [(pos, Maybe name)]
as [Maybe name]
args) [[Maybe name]]
rest
update :: Eq name => [(pos, Maybe name)] -> [Maybe name] -> [(pos, Maybe name)]
update :: forall name pos.
Eq name =>
[(pos, Maybe name)] -> [Maybe name] -> [(pos, Maybe name)]
update [] [Maybe name]
_ = []
update [(pos, Maybe name)]
_ [] = []
update ((pos
n, Just name
x) : [(pos, Maybe name)]
as) (Just name
x' : [Maybe name]
args)
| name
x name -> name -> Bool
forall a. Eq a => a -> a -> Bool
== name
x' = (pos
n, name -> Maybe name
forall a. a -> Maybe a
Just name
x) (pos, Maybe name) -> [(pos, Maybe name)] -> [(pos, Maybe name)]
forall a. a -> [a] -> [a]
: [(pos, Maybe name)] -> [Maybe name] -> [(pos, Maybe name)]
forall name pos.
Eq name =>
[(pos, Maybe name)] -> [Maybe name] -> [(pos, Maybe name)]
update [(pos, Maybe name)]
as [Maybe name]
args
update ((pos
n, Maybe name
_) : [(pos, Maybe name)]
as) (Maybe name
_ : [Maybe name]
args) = (pos
n, Maybe name
forall a. Maybe a
Nothing) (pos, Maybe name) -> [(pos, Maybe name)] -> [(pos, Maybe name)]
forall a. a -> [a] -> [a]
: [(pos, Maybe name)] -> [Maybe name] -> [(pos, Maybe name)]
forall name pos.
Eq name =>
[(pos, Maybe name)] -> [Maybe name] -> [(pos, Maybe name)]
update [(pos, Maybe name)]
as [Maybe name]
args
getDataApp :: ConstructorInfo -> [[Maybe Name]]
getDataApp :: ConstructorInfo -> [[Maybe Name]]
getDataApp (ConstructorInfo { constructorFields :: ConstructorInfo -> [Type]
constructorFields = [Type]
fields }) =
(Type -> [[Maybe Name]]) -> [Type] -> [[Maybe Name]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [[Maybe Name]]
getThem ([Type] -> [[Maybe Name]]) -> [Type] -> [[Maybe Name]]
forall a b. (a -> b) -> a -> b
$
[Type]
fields [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [ Type -> [TypeArg] -> Type
applyType (Name -> Type
ConT Name
dataName) ([TypeArg] -> Type) -> [TypeArg] -> Type
forall a b. (a -> b) -> a -> b
$ (Type -> TypeArg) -> [Type] -> [TypeArg]
forall a b. (a -> b) -> [a] -> [b]
map Type -> TypeArg
TANormal
([Type] -> [TypeArg]) -> [Type] -> [TypeArg]
forall a b. (a -> b) -> a -> b
$ (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
unSigType [Type]
instTys
]
where
getThem :: Type -> [[Maybe Name]]
getThem :: Type -> [[Maybe Name]]
getThem Type
ty = Maybe [Maybe Name] -> [[Maybe Name]]
forall a. Maybe a -> [a]
maybeToList (Maybe [Maybe Name] -> [[Maybe Name]])
-> Maybe [Maybe Name] -> [[Maybe Name]]
forall a b. (a -> b) -> a -> b
$ Name -> Type -> ([TypeArg] -> [Maybe Name]) -> Maybe [Maybe Name]
forall a. Name -> Type -> ([TypeArg] -> a) -> Maybe a
mbInductiveCase Name
dataName Type
ty [TypeArg] -> [Maybe Name]
inductiveArg
inductiveArg :: [TypeArg] -> [Maybe Name]
inductiveArg :: [TypeArg] -> [Maybe Name]
inductiveArg [TypeArg]
argTys =
let visArgTys :: [Type]
visArgTys = [TypeArg] -> [Type]
filterTANormals [TypeArg]
argTys
in [Type] -> [Type] -> [Maybe Name]
mParam [Type]
visArgTys [Type]
visArgTys
mParam :: [Type] -> [Type] -> [Maybe Name]
mParam :: [Type] -> [Type] -> [Maybe Name]
mParam [Type]
_ [] = []
mParam [Type]
args (VarT Name
n:[Type]
rest)
| Bool -> Name -> [Type] -> Bool
paramIn Bool
False Name
n [Type]
args
= Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n Maybe Name -> [Maybe Name] -> [Maybe Name]
forall a. a -> [a] -> [a]
: [Type] -> [Type] -> [Maybe Name]
mParam ((Type -> Bool) -> [Type] -> [Type]
forall a. (a -> Bool) -> [a] -> [a]
filter (Name -> Type -> Bool
noN Name
n) [Type]
args) [Type]
rest
mParam [Type]
args (Type
_:[Type]
rest) = Maybe Name
forall a. Maybe a
Nothing Maybe Name -> [Maybe Name] -> [Maybe Name]
forall a. a -> [a] -> [a]
: [Type] -> [Type] -> [Maybe Name]
mParam [Type]
args [Type]
rest
paramIn :: Bool -> Name -> [Type] -> Bool
paramIn :: Bool -> Name -> [Type] -> Bool
paramIn Bool
ok Name
_ [] = Bool
ok
paramIn Bool
ok Name
n (VarT Name
t:[Type]
ts) = Bool -> Name -> [Type] -> Bool
paramIn (Bool
ok Bool -> Bool -> Bool
|| Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
t) Name
n [Type]
ts
paramIn Bool
ok Name
n (Type
t:[Type]
ts)
| Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Type -> [Name]
forall a. TypeSubstitution a => a -> [Name]
freeVariables Type
t = Bool
False
| Bool
otherwise = Bool -> Name -> [Type] -> Bool
paramIn Bool
ok Name
n [Type]
ts
noN :: Name -> Type -> Bool
noN :: Name -> Type -> Bool
noN Name
n (VarT Name
t) = Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
t
noN Name
_ Type
_ = Bool
False
unSigType :: Type -> Type
unSigType :: Type -> Type
unSigType (SigT Type
t Type
_) = Type
t
unSigType (AppT Type
f Type
x) = Type -> Type -> Type
AppT (Type -> Type
unSigType Type
f) (Type -> Type
unSigType Type
x)
unSigType (ForallT [TyVarBndr Specificity]
tvbs [Type]
ctxt Type
t) = [TyVarBndr Specificity] -> [Type] -> Type -> Type
ForallT [TyVarBndr Specificity]
tvbs ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
unSigType [Type]
ctxt) (Type -> Type
unSigType Type
t)
unSigType (InfixT Type
t1 Name
n Type
t2) = Type -> Name -> Type -> Type
InfixT (Type -> Type
unSigType Type
t1) Name
n (Type -> Type
unSigType Type
t2)
unSigType (UInfixT Type
t1 Name
n Type
t2) = Type -> Name -> Type -> Type
UInfixT (Type -> Type
unSigType Type
t1) Name
n (Type -> Type
unSigType Type
t2)
unSigType (ParensT Type
t) = Type -> Type
ParensT (Type -> Type
unSigType Type
t)
unSigType (AppKindT Type
t Type
k) = Type -> Type -> Type
AppKindT (Type -> Type
unSigType Type
t) (Type -> Type
unSigType Type
k)
unSigType (ImplicitParamT String
n Type
t) = String -> Type -> Type
ImplicitParamT String
n (Type -> Type
unSigType Type
t)
unSigType Type
t = Type
t
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. HasCallStack => [a] -> [a]
tail String
str
| Bool
otherwise
= String
str
where
first :: Char
first = String -> Char
forall a. HasCallStack => [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
'_'