{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE Unsafe #-}
{-|
Module:      Data.Eliminator.TH
Copyright:   (C) 2017 Ryan Scott
License:     BSD-style (see the file LICENSE)
Maintainer:  Ryan Scott
Stability:   Experimental
Portability: GHC

Generate dependently typed elimination functions using Template Haskell.
-}
module Data.Eliminator.TH (
    -- * Eliminator generation
    -- ** Term-level eliminators
    -- $term-conventions
    deriveElim
  , deriveElimNamed
    -- ** Type-level eliminators
    -- $type-conventions
  , 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(..))

{- $term-conventions
'deriveElim' and 'deriveElimNamed' provide a way to automate the creation of
eliminator functions, which are mostly boilerplate. Here is a complete example
showing how one might use 'deriveElim':

@
$('singletons' [d| data MyList a = MyNil | MyCons a (MyList a) |])
$('deriveElim' ''MyList)
@

This will produce an eliminator function that looks roughly like the following:

@
elimMyList :: forall (a :: 'Type') (p :: MyList a '~>' 'Type') (l :: MyList a).
              'Sing' l
           -> 'Apply' p MyNil
           -> (forall (x :: a). 'Sing' x
                -> forall (xs :: MyList a). 'Sing' xs -> 'Apply' p xs
                -> 'Apply' p (MyCons x xs))
           -> 'Apply' p l
elimMyList SMyNil pMyNil _ = pMyNil
elimMyList (SMyCons (x' :: 'Sing' x) (xs' :: 'Sing' xs)) pMyNil pMyCons
  = pMyCons x' xs' (elimMyList \@a \@p \@xs pMyNil pMyCons)
@

There are some important things to note here:

* Because these eliminators use 'Sing' under the hood, in order for
  'deriveElim' to work, the 'Sing' instance for the data type given as an
  argument must be in scope. Moreover, 'deriveElim' assumes the naming
  conventions for singled constructors used by the @singletons@ library.
  (This is why the 'singletons' function is used in the example above).

* There is a convention for the order in which the arguments appear.
  The quantified type variables appear in this order:

    1. First, the type variables of the data type itself (@a@, in the above example).

    2. Second, a predicate type variable of kind @\<Datatype\> '~>' 'Type'@
       (@p@, in the above example).

    3. Finally, a type variable of kind @\<Datatype\>@ (@l@, in the above example).

  The function arguments appear in this order:

    1. First, a 'Sing' argument (@'Sing' l@, in the above example).

    2. Next, there are arguments that correspond to each constructor. More on this
       in a second.

  The return type is the predicate type variable applied to the data type
  (@'Apply' p (MyCons x xs)@, the above example).

  The type of each constructor argument also follows certain conventions:

    1. For each field, there will be a rank-2 type variable whose kind matches
       the type of the field, followed by a matching 'Sing' type. For instance,
       in the above example, @forall (x :: a). 'Sing' x@ corresponds to the
       first field of @MyCons@.

    2. In addition, if the field is a recursive occurrence of the data type,
       an additional argument will follow the 'Sing' type. This is best
       explained using the above example. In the @MyCons@ constructor, the second
       field (of type @MyCons a@) is a recursive occurrence of @MyCons@, so
       that corresponds to the type
       @forall (xs :: MyList a). 'Sing' xs -> 'Apply' p xs@, where @'Apply' p xs@
       is only present due to the recursion.

    3. Finally, the return type will be the predicate type variable applied
       to a saturated occurrence of the data constructor
       (@'Apply' p (MyCons x xs)@, in the above example).

* You'll need to enable lots of GHC extensions in order for the code generated
  by 'deriveElim' to typecheck. You'll need at least the following:

    * @AllowAmbiguousTypes@

    * @DataKinds@

    * @GADTs@

    * @PolyKinds@

    * @RankNTypes@

    * @ScopedTypeVariables@

    * @TemplateHaskell@

    * @TypeApplications@

* 'deriveElim' doesn't support every possible data type at the moment.
  It is known not to work for the following:

    * Data types defined using @GADTs@ or @ExistentialQuantification@

    * Data family instances

    * Data types which use polymorphic recursion
      (e.g., @data Foo a = Foo (Foo a)@)
-}

-- | @'deriveElim' dataName@ generates a top-level elimination function for the
-- datatype @dataName@. The eliminator will follow these naming conventions:
--
-- * If the datatype has an alphanumeric name, its eliminator will have that name
--   with @elim@ prepended.
--
-- * If the datatype has a symbolic name, its eliminator will have that name
--   with @~>@ prepended.
deriveElim :: Name -> Q [Dec]
deriveElim :: Name -> Q [Dec]
deriveElim Name
dataName = String -> Name -> Q [Dec]
deriveElimNamed (Name -> String
eliminatorName Name
dataName) Name
dataName

-- | @'deriveElimNamed' funName dataName@ generates a top-level elimination
-- function named @funName@ for the datatype @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)

{- $type-conventions
'deriveTypeElim' and 'deriveTypeElimNamed' are like 'deriveElim' and
'deriveElimNamed' except that they create /type/-level eliminators instead of
term-level ones. Here is an example showing how one might use
'deriveTypeElim':

@
data MyList a = MyNil | MyCons a (MyList a)
$('deriveTypeElim' ''MyList)
@

This will produce an eliminator function that looks roughly like the following:

@
type ElimMyList :: forall (a :: 'Type').
                   forall (p :: MyList a '~>' 'Type') (l :: MyList a)
                -> 'Apply' p MyNil
                -> (forall (x :: a) (xs :: MyList a)
                     -> 'Apply' p xs '~>' 'Apply' p (MyCons x xs))
                -> 'Apply' p l
type family ElimMyList p l pMyNil pMyCons where
  forall (a :: 'Type')
         (p :: MyList a ~> 'Type')
         (pMyNil :: 'Apply' p MyNil)
         (pMyCons :: forall (x :: a) (xs :: MyList a)
                      -> 'Apply' p xs '~>' 'Apply' p (MyCons x xs)).
    ElimMyList @a p MyNil pMyNil pMyCons =
      pMyNil
  forall (a :: 'Type')
         (p :: MyList a ~> 'Type')
         (_pMyNil :: 'Apply' p MyNil)
         (pMyCons :: forall (x :: a) (xs :: MyList a)
                      -> 'Apply' p xs '~>' 'Apply' p (MyCons x xs))
         x' xs'.
    ElimMyList @a p (MyCons x' xs') pMyNil pMyCons =
      'Apply' (pMyCons x' xs') (ElimMyList @a p xs' pMyNil pMyCons)
@

Note the following differences from a term-level eliminator that 'deriveElim'
would generate:

* Type-level eliminators do not use 'Sing'. Instead, they use visible dependent
  quantification. That is, instead of generating
  @forall (x :: a). Sing x -> ...@ (as a term-level eliminator would do), a
  type-level eliminator would use @forall (x :: a) -> ...@.

* Term-level eliminators quantify @p@ with an invisible @forall@, whereas
  type-level eliminators quantify @p@ with a visible @forall@. (Really, @p@
  ought to be quantified visibly in both forms of eliminator, but GHC does not
  yet support visible dependent quantification at the term level.)

* Type-level eliminators use ('~>') in certain places where (@->@) would appear
  in term-level eliminators. For instance, note the use of
  @'Apply' p xs '~>' 'Apply' p (MyCons x xs)@ in @ElimMyList@ above. This is
  done to make it easier to use type-level eliminators with defunctionalization
  symbols (which aren't necessary for term-level eliminators).

  This comes with a notable drawback: type-level eliminators cannot support
  data constructors where recursive occurrences of the data type appear in a
  position other than the last field of a constructor. In other words,
  'deriveTypeElim' works on the @MyList@ example above, but not this variant:

  @
  data SnocList a = SnocNil | SnocCons (SnocList a) a
  @

  This is because @$('deriveTypeElim' ''SnocList)@ would generate an eliminator
  with the following kind:

  @
  type ElimSnocList :: forall (a :: 'Type').
                       forall (p :: SnocList a '~>' 'Type') (l :: SnocList a)
                    -> 'Apply' p SnocNil
                    -> (forall (xs :: SnocList a) -> 'Apply' p xs
                          '~>' (forall (x :: a) -> 'Apply' p (SnocCons x xs)))
                    -> 'Apply' p l
  @

  Unfortunately, the kind
  @'Apply' p xs '~>' (forall (x :: a) -> 'Apply' p (SnocCons x xs))@ is
  impredicative.

* In addition to the language extensions that 'deriveElim' requires, you'll need
  to enable these extensions in order to use 'deriveTypeElim':

    * @StandaloneKindSignatures@

    * @UndecidableInstances@
-}

-- | @'deriveTypeElim' dataName@ generates a type-level eliminator for the
-- datatype @dataName@. The eliminator will follow these naming conventions:
--
-- * If the datatype has an alphanumeric name, its eliminator will have that name
--   with @Elim@ prepended.
--
-- * If the datatype has a symbolic name, its eliminator will have that name
--   with @~>@ prepended.
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' funName dataName@ generates a type-level eliminator
-- named @funName@ for the datatype @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)

-- The workhorse for deriveElim(Named). This generates either a term- or
-- type-level eliminator, depending on which Eliminator instance is used.
deriveElimNamed' ::
     Eliminator t
  => proxy t
  -> String  -- The name of the eliminator function
  -> Name    -- The name of the data type
  -> Q [Dec] -- The eliminator's type signature and body
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]

-- Generate the type for a "case alternative" in an eliminator function's type
-- signature, which is done on a constructor-by-constructor basis.
caseType ::
     Eliminator t
  => proxy t
  -> Name            -- The name of the data type
  -> Name            -- The predicate type variable
  -> ConstructorInfo -- The data constructor
  -> Q Type          -- The full case 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)

-- Generate a single clause for a term-level eliminator.
caseClause ::
     Name            -- The name of the eliminator function
  -> Name            -- The name of the data type
  -> [TyVarBndr]     -- The type variables bound by the data type
  -> TyVarBndr       -- The predicate type variable
  -> Int             -- The index of this constructor (0-indexed)
  -> Int             -- The total number of data constructors
  -> ConstructorInfo -- The data constructor
  -> Q Clause        -- The generated function 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)
                     []

-- Generate a single equation for a type-level eliminator.
--
-- This code is fairly similar in structure to caseClause, but different
-- enough in subtle ways that I did not attempt to de-duplicate this code as
-- a method of the Eliminator class.
caseTySynEqn ::
     Name            -- The name of the eliminator function
  -> Name            -- The name of the data type
  -> [TyVarBndr]     -- The type variables bound by the data type
  -> TyVarBndr       -- The predicate type variable
  -> Int             -- The index of this constructor (0-indexed)
  -> [Type]          -- The types of each "case alternative" in the eliminator
                     -- function's type signature
  -> ConstructorInfo -- The data constructor
  -> Q TySynEqn      -- The generated type family equation
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

-- Are we dealing with a term or a type?
data TermOrType
  = IsTerm
  | IsType

-- A class that abstracts out certain common operations that one must perform
-- for both term- and type-level eliminators.
class Eliminator (t :: TermOrType) where
  -- Create the Dec for an eliminator function's type signature.
  elimSigD ::
       proxy t
    -> Name -- The name of the eliminator function
    -> Type -- The type of the eliminator function
    -> Dec  -- The type signature Dec (SigD or KiSigD)

  -- Create an eliminator function's type.
  elimTypeSig ::
       proxy t
    -> [TyVarBndr] -- The type variables bound by the data type
    -> TyVarBndr   -- The predicate type variable
    -> TyVarBndr   -- The type variable whose kind is that of the data type itself
    -> [Type]      -- The types of each "case alternative" in the eliminator
                   -- function's type signature
    -> Type        -- The eliminator function's return type
    -> Type        -- The full type

  -- Take a data constructor's field type and prepend it to a "case
  -- alternative" in an eliminator function's type signature.
  prependElimCaseTypeVar ::
       proxy t
    -> Name -- The name of the data type
    -> Name -- The predicate type variable
    -> Name -- A fresh type variable name
    -> Kind -- The field type
    -> Type -- The rest of the "case alternative" type
    -> Type -- The "case alternative" type after prepending

  -- Generate the clauses/equations for the body of the eliminator function.
  qElimEqns ::
       proxy t
    -> Name              -- The name of the eliminator function
    -> Name              -- The name of the data type
    -> [TyVarBndr]       -- The type variables bound by the data type
    -> TyVarBndr         -- The predicate type variable
    -> TyVarBndr         -- The type variable whose kind is that of the data type itself
    -> [Type]            -- The types of each "case alternative" in the eliminator
                         -- function's type signature
    -> [ConstructorInfo] -- The data constructors
    -> Q Dec             -- The Dec containing the clauses/equations

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

-- TODO: Rule out polymorphic recursion
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]
_)
          -- Annoying special case for lists
        | 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

-- | Construct a type of the form @'Sing' x@ given @x@.
singType :: Name -> Type
singType :: Name -> Type
singType Name
x = Name -> Type
ConT ''Sing Type -> Type -> Type
`AppT` Name -> Type
VarT Name
x

-- | Construct a type of the form @'Apply' p ty@ given @p@ and @ty@.
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

-- | Generate a list of fresh names with a common prefix, and numbered suffixes.
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

-- Compute an eliminator function's name from the data type name.
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

-- Construct a function type, separating the arguments with ->
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)

-- Construct a function type, separating the arguments with ~>
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)

-- Apply an expression to a list of expressions using ordinary function applications.
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

-- Apply an expression to a list of types using visible type applications.
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

-- Apply a type to a list of types using ordinary function applications.
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

-- Apply a type to a list of types using defunctionalized applications
-- (i.e., using Apply from singletons).
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)

-- Apply a type to a list of types using visible kind applications.
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))

-----
-- Taken directly from singletons
-----

-- Make an identifier uppercase. If the identifier is infix, this acts as the
-- identity function.
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

-- is it a letter or underscore?
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
'_'