{- Data/Singletons/Util.hs

(c) Richard Eisenberg 2013
rae@cs.brynmawr.edu

This file contains helper functions internal to the singletons package.
Users of the package should not need to consult this file.
-}

{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, RankNTypes,
             TemplateHaskell, GeneralizedNewtypeDeriving,
             MultiParamTypeClasses, UndecidableInstances, MagicHash,
             LambdaCase, NoMonomorphismRestriction, ScopedTypeVariables,
             FlexibleContexts #-}

module Data.Singletons.Util where

import Prelude hiding ( exp, foldl, concat, mapM, any, pred )
import Language.Haskell.TH ( pprint )
import Language.Haskell.TH.Syntax hiding ( lift )
import Language.Haskell.TH.Desugar
import Data.Char
import Control.Monad hiding ( mapM )
import Control.Monad.Except hiding ( mapM )
import Control.Monad.Reader hiding ( mapM )
import Control.Monad.Writer hiding ( mapM )
import qualified Data.Map as Map
import Data.List.NonEmpty (NonEmpty(..))
import Data.Map ( Map )
import qualified Data.Monoid as Monoid
import Data.Semigroup as Semigroup
import Data.Foldable
import Data.Functor.Identity
import Data.Traversable
import Data.Generics
import Data.Maybe
import Data.Void

-- The list of types that singletons processes by default
basicTypes :: [Name]
basicTypes :: [Name]
basicTypes = [ ''Maybe
             , ''[]
             , ''Either
             , ''NonEmpty
             , ''Void
             ] [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
boundedBasicTypes

boundedBasicTypes :: [Name]
boundedBasicTypes :: [Name]
boundedBasicTypes =
            [ ''(,)
            , ''(,,)
            , ''(,,,)
            , ''(,,,,)
            , ''(,,,,,)
            , ''(,,,,,,)
            , ''Identity
            ] [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
enumBasicTypes

enumBasicTypes :: [Name]
enumBasicTypes :: [Name]
enumBasicTypes = [ ''Bool, ''Ordering, ''() ]

semigroupBasicTypes :: [Name]
semigroupBasicTypes :: [Name]
semigroupBasicTypes
  = [ ''Dual
    , ''All
    , ''Any
    , ''Sum
    , ''Product
    -- , ''Endo      see https://github.com/goldfirere/singletons/issues/82
    {- , ''Alt       singletons doesn't support higher kinds :(
                     see https://github.com/goldfirere/singletons/issues/150
    -}

    , ''Min
    , ''Max
    , ''Semigroup.First
    , ''Semigroup.Last
    , ''WrappedMonoid
    ]

monoidBasicTypes :: [Name]
monoidBasicTypes :: [Name]
monoidBasicTypes
  = [ ''Monoid.First
    , ''Monoid.Last
    ]

-- like reportWarning, but generalized to any Quasi
qReportWarning :: Quasi q => String -> q ()
qReportWarning :: String -> q ()
qReportWarning = Bool -> String -> q ()
forall (m :: * -> *). Quasi m => Bool -> String -> m ()
qReport Bool
False

-- like reportError, but generalized to any Quasi
qReportError :: Quasi q => String -> q ()
qReportError :: String -> q ()
qReportError = Bool -> String -> q ()
forall (m :: * -> *). Quasi m => Bool -> String -> m ()
qReport Bool
True

-- | Generate a new Unique
qNewUnique :: DsMonad q => q Uniq
qNewUnique :: q Uniq
qNewUnique = do
  Name OccName
_ NameFlavour
flav <- String -> q Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"x"
  case NameFlavour
flav of
    NameU Uniq
n -> Uniq -> q Uniq
forall (m :: * -> *) a. Monad m => a -> m a
return Uniq
n
    NameFlavour
_       -> String -> q Uniq
forall a. HasCallStack => String -> a
error String
"Internal error: `qNewName` didn't return a NameU"

checkForRep :: Quasi q => [Name] -> q ()
checkForRep :: [Name] -> q ()
checkForRep [Name]
names =
  Bool -> q () -> q ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((Name -> Bool) -> [Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"Rep") (String -> Bool) -> (Name -> String) -> Name -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
nameBase) [Name]
names)
    (String -> q ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> q ()) -> String -> q ()
forall a b. (a -> b) -> a -> b
$ String
"A data type named <<Rep>> is a special case.\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
            String
"Promoting it will not work as expected.\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
            String
"Please choose another name for your data type.")

checkForRepInDecls :: Quasi q => [DDec] -> q ()
checkForRepInDecls :: [DDec] -> q ()
checkForRepInDecls [DDec]
decls =
  [Name] -> q ()
forall (q :: * -> *). Quasi q => [Name] -> q ()
checkForRep ([DDec] -> [Name]
forall a. Data a => a -> [Name]
allNamesIn [DDec]
decls)

tysOfConFields :: DConFields -> [DType]
tysOfConFields :: DConFields -> [DType]
tysOfConFields (DNormalC Bool
_ [DBangType]
stys) = (DBangType -> DType) -> [DBangType] -> [DType]
forall a b. (a -> b) -> [a] -> [b]
map DBangType -> DType
forall a b. (a, b) -> b
snd [DBangType]
stys
tysOfConFields (DRecC [DVarBangType]
vstys)   = (DVarBangType -> DType) -> [DVarBangType] -> [DType]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
_,Bang
_,DType
ty) -> DType
ty) [DVarBangType]
vstys

recSelsOfConFields :: DConFields -> [Name]
recSelsOfConFields :: DConFields -> [Name]
recSelsOfConFields DNormalC{}    = []
recSelsOfConFields (DRecC [DVarBangType]
vstys) = (DVarBangType -> Name) -> [DVarBangType] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n,Bang
_,DType
_) -> Name
n) [DVarBangType]
vstys

-- Extract a data constructor's name and the number of arguments it accepts.
extractNameArgs :: DCon -> (Name, Int)
extractNameArgs :: DCon -> (Name, Int)
extractNameArgs (DCon [DTyVarBndr]
_ [DType]
_ Name
n DConFields
fields DType
_) = (Name
n, [DType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (DConFields -> [DType]
tysOfConFields DConFields
fields))

-- Extract a data constructor's name.
extractName :: DCon -> Name
extractName :: DCon -> Name
extractName (DCon [DTyVarBndr]
_ [DType]
_ Name
n DConFields
_ DType
_) = Name
n

-- Extract the names of a data constructor's record selectors.
extractRecSelNames :: DCon -> [Name]
extractRecSelNames :: DCon -> [Name]
extractRecSelNames (DCon [DTyVarBndr]
_ [DType]
_ Name
_ DConFields
fields DType
_) = DConFields -> [Name]
recSelsOfConFields DConFields
fields

-- | is a valid Haskell infix data constructor (i.e., does it begin with a colon?)
isInfixDataCon :: String -> Bool
isInfixDataCon :: String -> Bool
isInfixDataCon (Char
':':String
_) = Bool
True
isInfixDataCon String
_       = Bool
False

-- | Is an identifier a legal data constructor name in Haskell? That is, is its
-- first character an uppercase letter (prefix) or a colon (infix)?
isDataConName :: Name -> Bool
isDataConName :: Name -> Bool
isDataConName Name
n = let first :: Char
first = String -> Char
forall a. [a] -> a
head (Name -> String
nameBase Name
n) in Char -> Bool
isUpper Char
first Bool -> Bool -> Bool
|| Char
first Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
':'

-- | Is an identifier uppercase?
--
-- Note that this will always return 'False' for infix names, since the concept
-- of upper- and lower-case doesn't make sense for non-alphabetic characters.
-- If you want to check if a name is legal as a data constructor, use the
-- 'isDataConName' function.
isUpcase :: Name -> Bool
isUpcase :: Name -> Bool
isUpcase Name
n = let first :: Char
first = String -> Char
forall a. [a] -> a
head (Name -> String
nameBase Name
n) in Char -> Bool
isUpper Char
first

-- Make an identifier uppercase. If the identifier is infix, this acts as the
-- identity function.
upcase :: Name -> Name
upcase :: Name -> Name
upcase = String -> Name
mkName (String -> Name) -> (Name -> String) -> Name -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, String) -> Name -> String
toUpcaseStr (String, String)
noPrefix

-- make an identifier uppercase and return it as a String
toUpcaseStr :: (String, String)  -- (alpha, symb) prefixes to prepend
            -> Name -> String
toUpcaseStr :: (String, String) -> Name -> String
toUpcaseStr (String
alpha, String
symb) Name
n
  | Char -> Bool
isHsLetter Char
first
  = String
upcase_alpha

  | Bool
otherwise
  = String
upcase_symb

  where
    str :: String
str   = Name -> String
nameBase Name
n
    first :: Char
first = String -> Char
forall a. [a] -> a
head String
str

    upcase_alpha :: String
upcase_alpha = String
alpha String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Char -> Char
toUpper Char
first) Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
forall a. [a] -> [a]
tail String
str
    upcase_symb :: String
upcase_symb = String
symb String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str

noPrefix :: (String, String)
noPrefix :: (String, String)
noPrefix = (String
"", String
"")

-- Put an uppercase prefix on a constructor name. Takes two prefixes:
-- one for identifiers and one for symbols.
--
-- This is different from 'prefixName' in that infix constructor names always
-- start with a colon, so we must insert the prefix after the colon in order
-- for the new name to be syntactically valid.
prefixConName :: String -> String -> Name -> Name
prefixConName :: String -> String -> Name -> Name
prefixConName String
pre String
tyPre Name
n = case (Name -> String
nameBase Name
n) of
    (Char
':' : String
rest) -> String -> Name
mkName (Char
':' Char -> String -> String
forall a. a -> [a] -> [a]
: String
tyPre String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rest)
    String
alpha -> String -> Name
mkName (String
pre String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
alpha)

-- Put a prefix on a name. Takes two prefixes: one for identifiers
-- and one for symbols.
prefixName :: String -> String -> Name -> Name
prefixName :: String -> String -> Name -> Name
prefixName String
pre String
tyPre Name
n =
  let str :: String
str = Name -> String
nameBase Name
n
      first :: Char
first = String -> Char
forall a. [a] -> a
head String
str in
    if Char -> Bool
isHsLetter Char
first
     then String -> Name
mkName (String
pre String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str)
     else String -> Name
mkName (String
tyPre String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str)

-- Put a suffix on a name. Takes two suffixes: one for identifiers
-- and one for symbols.
suffixName :: String -> String -> Name -> Name
suffixName :: String -> String -> Name -> Name
suffixName String
ident String
symb Name
n =
  let str :: String
str = Name -> String
nameBase Name
n
      first :: Char
first = String -> Char
forall a. [a] -> a
head String
str in
  if Char -> Bool
isHsLetter Char
first
  then String -> Name
mkName (String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ident)
  else String -> Name
mkName (String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
symb)

-- convert a number into both alphanumeric and symoblic forms
uniquePrefixes :: String   -- alphanumeric prefix
               -> String   -- symbolic prefix
               -> Uniq
               -> (String, String)  -- (alphanum, symbolic)
uniquePrefixes :: String -> String -> Uniq -> (String, String)
uniquePrefixes String
alpha String
symb Uniq
n = (String
alpha String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
n_str, String
symb String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
convert String
n_str)
  where
    n_str :: String
n_str = Uniq -> String
forall a. Show a => a -> String
show Uniq
n

    convert :: String -> String
convert [] = []
    convert (Char
d : String
ds) =
      let d' :: Char
d' = case Char
d of
                 Char
'0' -> Char
'!'
                 Char
'1' -> Char
'#'
                 Char
'2' -> Char
'$'
                 Char
'3' -> Char
'%'
                 Char
'4' -> Char
'&'
                 Char
'5' -> Char
'*'
                 Char
'6' -> Char
'+'
                 Char
'7' -> Char
'.'
                 Char
'8' -> Char
'/'
                 Char
'9' -> Char
'>'
                 Char
_   -> String -> Char
forall a. HasCallStack => String -> a
error String
"non-digit in show #"
      in Char
d' Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
convert String
ds

-- extract the kind from a TyVarBndr
extractTvbKind :: DTyVarBndr -> Maybe DKind
extractTvbKind :: DTyVarBndr -> Maybe DType
extractTvbKind (DPlainTV Name
_) = Maybe DType
forall a. Maybe a
Nothing
extractTvbKind (DKindedTV Name
_ DType
k) = DType -> Maybe DType
forall a. a -> Maybe a
Just DType
k

-- extract the name from a TyVarBndr.
extractTvbName :: DTyVarBndr -> Name
extractTvbName :: DTyVarBndr -> Name
extractTvbName (DPlainTV Name
n) = Name
n
extractTvbName (DKindedTV Name
n DType
_) = Name
n

tvbToType :: DTyVarBndr -> DType
tvbToType :: DTyVarBndr -> DType
tvbToType = Name -> DType
DVarT (Name -> DType) -> (DTyVarBndr -> Name) -> DTyVarBndr -> DType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DTyVarBndr -> Name
extractTvbName

-- If a type variable binder lacks an explicit kind, pick a default kind of
-- Type. Otherwise, leave the binder alone.
defaultTvbToTypeKind :: DTyVarBndr -> DTyVarBndr
defaultTvbToTypeKind :: DTyVarBndr -> DTyVarBndr
defaultTvbToTypeKind (DPlainTV Name
tvname) = Name -> DType -> DTyVarBndr
DKindedTV Name
tvname (DType -> DTyVarBndr) -> DType -> DTyVarBndr
forall a b. (a -> b) -> a -> b
$ Name -> DType
DConT Name
typeKindName
defaultTvbToTypeKind DTyVarBndr
tvb               = DTyVarBndr
tvb

-- If @Nothing@, return @Type@. If @Just k@, return @k@.
defaultMaybeToTypeKind :: Maybe DKind -> DKind
defaultMaybeToTypeKind :: Maybe DType -> DType
defaultMaybeToTypeKind (Just DType
k) = DType
k
defaultMaybeToTypeKind Maybe DType
Nothing  = Name -> DType
DConT Name
typeKindName

inferMaybeKindTV :: Name -> Maybe DKind -> DTyVarBndr
inferMaybeKindTV :: Name -> Maybe DType -> DTyVarBndr
inferMaybeKindTV Name
n Maybe DType
Nothing =  Name -> DTyVarBndr
DPlainTV Name
n
inferMaybeKindTV Name
n (Just DType
k) = Name -> DType -> DTyVarBndr
DKindedTV Name
n DType
k

resultSigToMaybeKind :: DFamilyResultSig -> Maybe DKind
resultSigToMaybeKind :: DFamilyResultSig -> Maybe DType
resultSigToMaybeKind DFamilyResultSig
DNoSig                      = Maybe DType
forall a. Maybe a
Nothing
resultSigToMaybeKind (DKindSig DType
k)                = DType -> Maybe DType
forall a. a -> Maybe a
Just DType
k
resultSigToMaybeKind (DTyVarSig (DPlainTV Name
_))    = Maybe DType
forall a. Maybe a
Nothing
resultSigToMaybeKind (DTyVarSig (DKindedTV Name
_ DType
k)) = DType -> Maybe DType
forall a. a -> Maybe a
Just DType
k

maybeKindToResultSig :: Maybe DKind -> DFamilyResultSig
maybeKindToResultSig :: Maybe DType -> DFamilyResultSig
maybeKindToResultSig = DFamilyResultSig
-> (DType -> DFamilyResultSig) -> Maybe DType -> DFamilyResultSig
forall b a. b -> (a -> b) -> Maybe a -> b
maybe DFamilyResultSig
DNoSig DType -> DFamilyResultSig
DKindSig

maybeSigT :: DType -> Maybe DKind -> DType
maybeSigT :: DType -> Maybe DType -> DType
maybeSigT DType
ty Maybe DType
Nothing   = DType
ty
maybeSigT DType
ty (Just DType
ki) = DType
ty DType -> DType -> DType
`DSigT` DType
ki

-- Reconstruct a vanilla function type from its individual type variable
-- binders, constraints, argument types, and result type. (See
-- Note [Vanilla-type validity checking during promotion] in
-- Data.Singletons.Promote.Type for what "vanilla" means.)
ravelVanillaDType :: [DTyVarBndr] -> DCxt -> [DType] -> DType -> DType
ravelVanillaDType :: [DTyVarBndr] -> [DType] -> [DType] -> DType -> DType
ravelVanillaDType [DTyVarBndr]
tvbs [DType]
ctxt [DType]
args DType
res =
  [DTyVarBndr] -> ([DTyVarBndr] -> DType -> DType) -> DType -> DType
forall a b. [a] -> ([a] -> b -> b) -> b -> b
ifNonEmpty [DTyVarBndr]
tvbs (ForallVisFlag -> [DTyVarBndr] -> DType -> DType
DForallT ForallVisFlag
ForallInvis) (DType -> DType) -> DType -> DType
forall a b. (a -> b) -> a -> b
$
  [DType] -> ([DType] -> DType -> DType) -> DType -> DType
forall a b. [a] -> ([a] -> b -> b) -> b -> b
ifNonEmpty [DType]
ctxt [DType] -> DType -> DType
DConstrainedT (DType -> DType) -> DType -> DType
forall a b. (a -> b) -> a -> b
$
  [DType] -> DType
go [DType]
args
  where
    ifNonEmpty :: [a] -> ([a] -> b -> b) -> b -> b
    ifNonEmpty :: [a] -> ([a] -> b -> b) -> b -> b
ifNonEmpty [] [a] -> b -> b
_ b
z = b
z
    ifNonEmpty [a]
l  [a] -> b -> b
f b
z = [a] -> b -> b
f [a]
l b
z

    go :: [DType] -> DType
    go :: [DType] -> DType
go []    = DType
res
    go (DType
h:[DType]
t) = DType -> DType -> DType
DAppT (DType -> DType -> DType
DAppT DType
DArrowT DType
h) ([DType] -> DType
go [DType]
t)

-- Decompose a vanilla function type into its type variables, its context, its
-- argument types, and its result type. (See
-- Note [Vanilla-type validity checking during promotion] in
-- Data.Singletons.Promote.Type for what "vanilla" means.)
-- If a non-vanilla construct is encountered while decomposing the function
-- type, an error is thrown monadically.
--
-- This should be contrasted with the 'unravelDType' function from
-- @th-desugar@, which supports the full gamut of function types. @singletons@
-- only supports a subset of these types, which is why this function is used
-- to decompose them instead.
unravelVanillaDType :: forall m. MonadFail m
                    => DType -> m ([DTyVarBndr], DCxt, [DType], DType)
unravelVanillaDType :: DType -> m ([DTyVarBndr], [DType], [DType], DType)
unravelVanillaDType DType
ty =
  case DType -> Either String ([DTyVarBndr], [DType], [DType], DType)
unravelVanillaDType_either DType
ty of
    Left String
err      -> String -> m ([DTyVarBndr], [DType], [DType], DType)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
err
    Right ([DTyVarBndr], [DType], [DType], DType)
payload -> ([DTyVarBndr], [DType], [DType], DType)
-> m ([DTyVarBndr], [DType], [DType], DType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([DTyVarBndr], [DType], [DType], DType)
payload

-- Ensures that a 'DType' is a vanilla type. (See
-- Note [Vanilla-type validity checking during promotion] in
-- Data.Singletons.Promote.Type for what "vanilla" means.)
--
-- The only monadic thing that this function can do is 'fail', which it does
-- if a non-vanilla construct is encountered.
checkVanillaDType :: forall m. MonadFail m => DType -> m ()
checkVanillaDType :: DType -> m ()
checkVanillaDType DType
ty =
  case DType -> Either String ([DTyVarBndr], [DType], [DType], DType)
unravelVanillaDType_either DType
ty of
    Left String
err -> String -> m ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
err
    Right ([DTyVarBndr], [DType], [DType], DType)
_  -> () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- The workhorse that powers unravelVanillaDType and checkVanillaDType.
-- Returns @Right payload@ upon success, and @Left error_msg@ upon failure.
unravelVanillaDType_either ::
  DType -> Either String ([DTyVarBndr], DCxt, [DType], DType)
unravelVanillaDType_either :: DType -> Either String ([DTyVarBndr], [DType], [DType], DType)
unravelVanillaDType_either DType
ty =
  Identity (Either String ([DTyVarBndr], [DType], [DType], DType))
-> Either String ([DTyVarBndr], [DType], [DType], DType)
forall a. Identity a -> a
runIdentity (Identity (Either String ([DTyVarBndr], [DType], [DType], DType))
 -> Either String ([DTyVarBndr], [DType], [DType], DType))
-> Identity (Either String ([DTyVarBndr], [DType], [DType], DType))
-> Either String ([DTyVarBndr], [DType], [DType], DType)
forall a b. (a -> b) -> a -> b
$ (ReaderT
   Bool
   Identity
   (Either String ([DTyVarBndr], [DType], [DType], DType))
 -> Bool
 -> Identity
      (Either String ([DTyVarBndr], [DType], [DType], DType)))
-> Bool
-> ReaderT
     Bool
     Identity
     (Either String ([DTyVarBndr], [DType], [DType], DType))
-> Identity (Either String ([DTyVarBndr], [DType], [DType], DType))
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT
  Bool
  Identity
  (Either String ([DTyVarBndr], [DType], [DType], DType))
-> Bool
-> Identity (Either String ([DTyVarBndr], [DType], [DType], DType))
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT Bool
True (ReaderT
   Bool
   Identity
   (Either String ([DTyVarBndr], [DType], [DType], DType))
 -> Identity
      (Either String ([DTyVarBndr], [DType], [DType], DType)))
-> ReaderT
     Bool
     Identity
     (Either String ([DTyVarBndr], [DType], [DType], DType))
-> Identity (Either String ([DTyVarBndr], [DType], [DType], DType))
forall a b. (a -> b) -> a -> b
$ ExceptT
  String (Reader Bool) ([DTyVarBndr], [DType], [DType], DType)
-> ReaderT
     Bool
     Identity
     (Either String ([DTyVarBndr], [DType], [DType], DType))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT
   String (Reader Bool) ([DTyVarBndr], [DType], [DType], DType)
 -> ReaderT
      Bool
      Identity
      (Either String ([DTyVarBndr], [DType], [DType], DType)))
-> ExceptT
     String (Reader Bool) ([DTyVarBndr], [DType], [DType], DType)
-> ReaderT
     Bool
     Identity
     (Either String ([DTyVarBndr], [DType], [DType], DType))
forall a b. (a -> b) -> a -> b
$ UnravelM ([DTyVarBndr], [DType], [DType], DType)
-> ExceptT
     String (Reader Bool) ([DTyVarBndr], [DType], [DType], DType)
forall a. UnravelM a -> ExceptT String (Reader Bool) a
runUnravelM (UnravelM ([DTyVarBndr], [DType], [DType], DType)
 -> ExceptT
      String (Reader Bool) ([DTyVarBndr], [DType], [DType], DType))
-> UnravelM ([DTyVarBndr], [DType], [DType], DType)
-> ExceptT
     String (Reader Bool) ([DTyVarBndr], [DType], [DType], DType)
forall a b. (a -> b) -> a -> b
$ DType -> UnravelM ([DTyVarBndr], [DType], [DType], DType)
go_ty DType
ty
  where
    go_ty :: DType -> UnravelM ([DTyVarBndr], DCxt, [DType], DType)
    go_ty :: DType -> UnravelM ([DTyVarBndr], [DType], [DType], DType)
go_ty DType
typ = do
      let (DFunArgs
args1, DType
res) = DType -> (DFunArgs, DType)
unravelDType DType
typ
      (DFunArgs
args2, [DTyVarBndr]
tvbs) <- DFunArgs -> UnravelM (DFunArgs, [DTyVarBndr])
take_tvbs  DFunArgs
args1
      (DFunArgs
args3, [DType]
ctxt) <- DFunArgs -> UnravelM (DFunArgs, [DType])
take_ctxt  DFunArgs
args2
      [DType]
anons         <- DFunArgs -> UnravelM [DType]
take_anons DFunArgs
args3
      ([DTyVarBndr], [DType], [DType], DType)
-> UnravelM ([DTyVarBndr], [DType], [DType], DType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([DTyVarBndr]
tvbs, [DType]
ctxt, [DType]
anons, DType
res)

    -- Process a type in a higher-order position (e.g., the @forall a. a -> a@ in
    -- @(forall a. a -> a) -> b -> b@). This is only done to check for the
    -- presence of higher-rank foralls or constraints, which are not permitted
    -- in vanilla types.
    go_higher_order_ty :: DType -> UnravelM ()
    go_higher_order_ty :: DType -> UnravelM ()
go_higher_order_ty DType
typ = () ()
-> UnravelM ([DTyVarBndr], [DType], [DType], DType) -> UnravelM ()
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (Bool -> Bool)
-> UnravelM ([DTyVarBndr], [DType], [DType], DType)
-> UnravelM ([DTyVarBndr], [DType], [DType], DType)
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
False) (DType -> UnravelM ([DTyVarBndr], [DType], [DType], DType)
go_ty DType
typ)

    take_tvbs :: DFunArgs -> UnravelM (DFunArgs, [DTyVarBndr])
    take_tvbs :: DFunArgs -> UnravelM (DFunArgs, [DTyVarBndr])
take_tvbs (DFAForalls ForallVisFlag
ForallInvis [DTyVarBndr]
tvbs DFunArgs
args) = do
      Bool
rank_1 <- UnravelM Bool
forall r (m :: * -> *). MonadReader r m => m r
ask
      Bool -> UnravelM () -> UnravelM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
rank_1 (UnravelM () -> UnravelM ()) -> UnravelM () -> UnravelM ()
forall a b. (a -> b) -> a -> b
$ String -> UnravelM ()
forall (m :: * -> *) a. MonadError String m => String -> m a
fail_forall String
"higher-rank"
      ()
_ <- (DTyVarBndr -> UnravelM ()) -> [DTyVarBndr] -> UnravelM ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ ((DType -> UnravelM ()) -> Maybe DType -> UnravelM ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ DType -> UnravelM ()
go_higher_order_ty (Maybe DType -> UnravelM ())
-> (DTyVarBndr -> Maybe DType) -> DTyVarBndr -> UnravelM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DTyVarBndr -> Maybe DType
extractTvbKind) [DTyVarBndr]
tvbs
      (DFunArgs
args', [DTyVarBndr]
tvbs') <- DFunArgs -> UnravelM (DFunArgs, [DTyVarBndr])
take_tvbs DFunArgs
args
      (DFunArgs, [DTyVarBndr]) -> UnravelM (DFunArgs, [DTyVarBndr])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DFunArgs
args', [DTyVarBndr]
tvbs [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr]
forall a. [a] -> [a] -> [a]
++ [DTyVarBndr]
tvbs')
    take_tvbs (DFAForalls ForallVisFlag
ForallVis [DTyVarBndr]
_ DFunArgs
_) = UnravelM (DFunArgs, [DTyVarBndr])
forall (m :: * -> *) a. MonadError String m => m a
fail_vdq
    take_tvbs DFunArgs
args = (DFunArgs, [DTyVarBndr]) -> UnravelM (DFunArgs, [DTyVarBndr])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DFunArgs
args, [])

    take_ctxt :: DFunArgs -> UnravelM (DFunArgs, DCxt)
    take_ctxt :: DFunArgs -> UnravelM (DFunArgs, [DType])
take_ctxt (DFACxt [DType]
ctxt DFunArgs
args) = do
      Bool
rank_1 <- UnravelM Bool
forall r (m :: * -> *). MonadReader r m => m r
ask
      Bool -> UnravelM () -> UnravelM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
rank_1 (UnravelM () -> UnravelM ()) -> UnravelM () -> UnravelM ()
forall a b. (a -> b) -> a -> b
$ String -> UnravelM ()
forall (m :: * -> *) a. MonadError String m => String -> m a
fail_ctxt String
"higher-rank"
      (DType -> UnravelM ()) -> [DType] -> UnravelM ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ DType -> UnravelM ()
go_higher_order_ty [DType]
ctxt
      (DFunArgs
args', [DType]
ctxt') <- DFunArgs -> UnravelM (DFunArgs, [DType])
take_ctxt DFunArgs
args
      (DFunArgs, [DType]) -> UnravelM (DFunArgs, [DType])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DFunArgs
args', [DType]
ctxt [DType] -> [DType] -> [DType]
forall a. [a] -> [a] -> [a]
++ [DType]
ctxt')
    take_ctxt (DFAForalls ForallVisFlag
fvf [DTyVarBndr]
_ DFunArgs
_) =
      case ForallVisFlag
fvf of
        ForallVisFlag
ForallInvis -> String -> UnravelM (DFunArgs, [DType])
forall (m :: * -> *) a. MonadError String m => String -> m a
fail_forall String
"nested"
        ForallVisFlag
ForallVis   -> UnravelM (DFunArgs, [DType])
forall (m :: * -> *) a. MonadError String m => m a
fail_vdq
    take_ctxt DFunArgs
args = (DFunArgs, [DType]) -> UnravelM (DFunArgs, [DType])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DFunArgs
args, [])

    take_anons :: DFunArgs -> UnravelM [DType]
    take_anons :: DFunArgs -> UnravelM [DType]
take_anons (DFAAnon DType
anon DFunArgs
args) = do
      DType -> UnravelM ()
go_higher_order_ty DType
anon
      [DType]
anons <- DFunArgs -> UnravelM [DType]
take_anons DFunArgs
args
      [DType] -> UnravelM [DType]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DType
anonDType -> [DType] -> [DType]
forall a. a -> [a] -> [a]
:[DType]
anons)
    take_anons (DFAForalls ForallVisFlag
fvf [DTyVarBndr]
_ DFunArgs
_) =
      case ForallVisFlag
fvf of
        ForallVisFlag
ForallInvis -> String -> UnravelM [DType]
forall (m :: * -> *) a. MonadError String m => String -> m a
fail_forall String
"nested"
        ForallVisFlag
ForallVis   -> UnravelM [DType]
forall (m :: * -> *) a. MonadError String m => m a
fail_vdq
    take_anons (DFACxt [DType]
_ DFunArgs
_) = String -> UnravelM [DType]
forall (m :: * -> *) a. MonadError String m => String -> m a
fail_ctxt String
"nested"
    take_anons DFunArgs
DFANil = [DType] -> UnravelM [DType]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

    failWith :: MonadError String m => String -> m a
    failWith :: String -> m a
failWith String
thing = String -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
      [ String
"`singletons` does not support " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
thing
      , String
"In the type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Ppr a => a -> String
pprint (DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten DType
ty)
      ]

    fail_forall :: MonadError String m => String -> m a
    fail_forall :: String -> m a
fail_forall String
sort = String -> m a
forall (m :: * -> *) a. MonadError String m => String -> m a
failWith (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ String
sort String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" `forall`s"

    fail_vdq :: MonadError String m => m a
    fail_vdq :: m a
fail_vdq = String -> m a
forall (m :: * -> *) a. MonadError String m => String -> m a
failWith String
"visible dependent quantification"

    fail_ctxt :: MonadError String m => String -> m a
    fail_ctxt :: String -> m a
fail_ctxt String
sort = String -> m a
forall (m :: * -> *) a. MonadError String m => String -> m a
failWith (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ String
sort String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" contexts"

-- The monad that powers the internals of unravelVanillaDType_either.
--
-- * ExceptT String: records the error message upon failure.
--
-- * Reader Bool: True if we are in a rank-1 position in a type, False otherwise
newtype UnravelM a = UnravelM { UnravelM a -> ExceptT String (Reader Bool) a
runUnravelM :: ExceptT String (Reader Bool) a }
  deriving (a -> UnravelM b -> UnravelM a
(a -> b) -> UnravelM a -> UnravelM b
(forall a b. (a -> b) -> UnravelM a -> UnravelM b)
-> (forall a b. a -> UnravelM b -> UnravelM a) -> Functor UnravelM
forall a b. a -> UnravelM b -> UnravelM a
forall a b. (a -> b) -> UnravelM a -> UnravelM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> UnravelM b -> UnravelM a
$c<$ :: forall a b. a -> UnravelM b -> UnravelM a
fmap :: (a -> b) -> UnravelM a -> UnravelM b
$cfmap :: forall a b. (a -> b) -> UnravelM a -> UnravelM b
Functor, Functor UnravelM
a -> UnravelM a
Functor UnravelM
-> (forall a. a -> UnravelM a)
-> (forall a b. UnravelM (a -> b) -> UnravelM a -> UnravelM b)
-> (forall a b c.
    (a -> b -> c) -> UnravelM a -> UnravelM b -> UnravelM c)
-> (forall a b. UnravelM a -> UnravelM b -> UnravelM b)
-> (forall a b. UnravelM a -> UnravelM b -> UnravelM a)
-> Applicative UnravelM
UnravelM a -> UnravelM b -> UnravelM b
UnravelM a -> UnravelM b -> UnravelM a
UnravelM (a -> b) -> UnravelM a -> UnravelM b
(a -> b -> c) -> UnravelM a -> UnravelM b -> UnravelM c
forall a. a -> UnravelM a
forall a b. UnravelM a -> UnravelM b -> UnravelM a
forall a b. UnravelM a -> UnravelM b -> UnravelM b
forall a b. UnravelM (a -> b) -> UnravelM a -> UnravelM b
forall a b c.
(a -> b -> c) -> UnravelM a -> UnravelM b -> UnravelM c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: UnravelM a -> UnravelM b -> UnravelM a
$c<* :: forall a b. UnravelM a -> UnravelM b -> UnravelM a
*> :: UnravelM a -> UnravelM b -> UnravelM b
$c*> :: forall a b. UnravelM a -> UnravelM b -> UnravelM b
liftA2 :: (a -> b -> c) -> UnravelM a -> UnravelM b -> UnravelM c
$cliftA2 :: forall a b c.
(a -> b -> c) -> UnravelM a -> UnravelM b -> UnravelM c
<*> :: UnravelM (a -> b) -> UnravelM a -> UnravelM b
$c<*> :: forall a b. UnravelM (a -> b) -> UnravelM a -> UnravelM b
pure :: a -> UnravelM a
$cpure :: forall a. a -> UnravelM a
$cp1Applicative :: Functor UnravelM
Applicative, Applicative UnravelM
a -> UnravelM a
Applicative UnravelM
-> (forall a b. UnravelM a -> (a -> UnravelM b) -> UnravelM b)
-> (forall a b. UnravelM a -> UnravelM b -> UnravelM b)
-> (forall a. a -> UnravelM a)
-> Monad UnravelM
UnravelM a -> (a -> UnravelM b) -> UnravelM b
UnravelM a -> UnravelM b -> UnravelM b
forall a. a -> UnravelM a
forall a b. UnravelM a -> UnravelM b -> UnravelM b
forall a b. UnravelM a -> (a -> UnravelM b) -> UnravelM b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> UnravelM a
$creturn :: forall a. a -> UnravelM a
>> :: UnravelM a -> UnravelM b -> UnravelM b
$c>> :: forall a b. UnravelM a -> UnravelM b -> UnravelM b
>>= :: UnravelM a -> (a -> UnravelM b) -> UnravelM b
$c>>= :: forall a b. UnravelM a -> (a -> UnravelM b) -> UnravelM b
$cp1Monad :: Applicative UnravelM
Monad, MonadError String, MonadReader Bool)

-- count the number of arguments in a type
countArgs :: DType -> Int
countArgs :: DType -> Int
countArgs DType
ty = [DVisFunArg] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([DVisFunArg] -> Int) -> [DVisFunArg] -> Int
forall a b. (a -> b) -> a -> b
$ DFunArgs -> [DVisFunArg]
filterDVisFunArgs DFunArgs
args
  where (DFunArgs
args, DType
_) = DType -> (DFunArgs, DType)
unravelDType DType
ty

-- Collect the invisible type variable binders from a sequence of DFunArgs.
filterInvisTvbArgs :: DFunArgs -> [DTyVarBndr]
filterInvisTvbArgs :: DFunArgs -> [DTyVarBndr]
filterInvisTvbArgs DFunArgs
DFANil           = []
filterInvisTvbArgs (DFACxt  [DType]
_ DFunArgs
args) = DFunArgs -> [DTyVarBndr]
filterInvisTvbArgs DFunArgs
args
filterInvisTvbArgs (DFAAnon DType
_ DFunArgs
args) = DFunArgs -> [DTyVarBndr]
filterInvisTvbArgs DFunArgs
args
filterInvisTvbArgs (DFAForalls ForallVisFlag
fvf [DTyVarBndr]
tvbs' DFunArgs
args) =
  let res :: [DTyVarBndr]
res = DFunArgs -> [DTyVarBndr]
filterInvisTvbArgs DFunArgs
args in
  case ForallVisFlag
fvf of
    ForallVisFlag
ForallVis   -> [DTyVarBndr]
res
    ForallVisFlag
ForallInvis -> [DTyVarBndr]
tvbs' [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr]
forall a. [a] -> [a] -> [a]
++ [DTyVarBndr]
res

-- Infer the kind of a DTyVarBndr by using information from a DVisFunArg.
replaceTvbKind :: DVisFunArg -> DTyVarBndr -> DTyVarBndr
replaceTvbKind :: DVisFunArg -> DTyVarBndr -> DTyVarBndr
replaceTvbKind (DVisFADep DTyVarBndr
tvb) DTyVarBndr
_   = DTyVarBndr
tvb
replaceTvbKind (DVisFAAnon DType
k)  DTyVarBndr
tvb = Name -> DType -> DTyVarBndr
DKindedTV (DTyVarBndr -> Name
extractTvbName DTyVarBndr
tvb) DType
k

-- changes all TyVars not to be NameU's. Workaround for GHC#11812/#17537
noExactTyVars :: Data a => a -> a
noExactTyVars :: a -> a
noExactTyVars = (forall a. Data a => a -> a) -> forall a. Data a => a -> a
everywhere forall a. Data a => a -> a
go
  where
    go :: Data a => a -> a
    go :: a -> a
go = (DTyVarBndr -> DTyVarBndr) -> a -> a
forall a b. (Typeable a, Typeable b) => (b -> b) -> a -> a
mkT DTyVarBndr -> DTyVarBndr
fix_tvb (a -> a) -> (DType -> DType) -> a -> a
forall a b.
(Typeable a, Typeable b) =>
(a -> a) -> (b -> b) -> a -> a
`extT` DType -> DType
fix_ty (a -> a) -> (InjectivityAnn -> InjectivityAnn) -> a -> a
forall a b.
(Typeable a, Typeable b) =>
(a -> a) -> (b -> b) -> a -> a
`extT` InjectivityAnn -> InjectivityAnn
fix_inj_ann

    fix_tvb :: DTyVarBndr -> DTyVarBndr
fix_tvb (DPlainTV Name
n)    = Name -> DTyVarBndr
DPlainTV (Name -> Name
noExactName Name
n)
    fix_tvb (DKindedTV Name
n DType
k) = Name -> DType -> DTyVarBndr
DKindedTV (Name -> Name
noExactName Name
n) DType
k

    fix_ty :: DType -> DType
fix_ty (DVarT Name
n)           = Name -> DType
DVarT (Name -> Name
noExactName Name
n)
    fix_ty DType
ty                  = DType
ty

    fix_inj_ann :: InjectivityAnn -> InjectivityAnn
fix_inj_ann (InjectivityAnn Name
lhs [Name]
rhs)
      = Name -> [Name] -> InjectivityAnn
InjectivityAnn (Name -> Name
noExactName Name
lhs) ((Name -> Name) -> [Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Name
noExactName [Name]
rhs)

-- changes a Name not to be a NameU. Workaround for GHC#11812/#17537
noExactName :: Name -> Name
noExactName :: Name -> Name
noExactName (Name (OccName String
occ) (NameU Uniq
unique)) = String -> Name
mkName (String
occ String -> String -> String
forall a. [a] -> [a] -> [a]
++ Uniq -> String
forall a. Show a => a -> String
show Uniq
unique)
noExactName Name
n                                   = Name
n

substKind :: Map Name DKind -> DKind -> DKind
substKind :: Map Name DType -> DType -> DType
substKind = Map Name DType -> DType -> DType
substType

-- | Non–capture-avoiding substitution. (If you want capture-avoiding
-- substitution, use @substTy@ from "Language.Haskell.TH.Desugar.Subst".
substType :: Map Name DType -> DType -> DType
substType :: Map Name DType -> DType -> DType
substType Map Name DType
subst DType
ty | Map Name DType -> Bool
forall k a. Map k a -> Bool
Map.null Map Name DType
subst = DType
ty
substType Map Name DType
subst (DForallT ForallVisFlag
fvf [DTyVarBndr]
tvbs DType
inner_ty)
  = ForallVisFlag -> [DTyVarBndr] -> DType -> DType
DForallT ForallVisFlag
fvf [DTyVarBndr]
tvbs' DType
inner_ty'
  where
    (Map Name DType
subst', [DTyVarBndr]
tvbs') = (Map Name DType -> DTyVarBndr -> (Map Name DType, DTyVarBndr))
-> Map Name DType -> [DTyVarBndr] -> (Map Name DType, [DTyVarBndr])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL Map Name DType -> DTyVarBndr -> (Map Name DType, DTyVarBndr)
subst_tvb Map Name DType
subst [DTyVarBndr]
tvbs
    inner_ty' :: DType
inner_ty'       = Map Name DType -> DType -> DType
substType Map Name DType
subst' DType
inner_ty
substType Map Name DType
subst (DConstrainedT [DType]
cxt DType
inner_ty) =
  [DType] -> DType -> DType
DConstrainedT ((DType -> DType) -> [DType] -> [DType]
forall a b. (a -> b) -> [a] -> [b]
map (Map Name DType -> DType -> DType
substType Map Name DType
subst) [DType]
cxt) (Map Name DType -> DType -> DType
substType Map Name DType
subst DType
inner_ty)
substType Map Name DType
subst (DAppT DType
ty1 DType
ty2) = Map Name DType -> DType -> DType
substType Map Name DType
subst DType
ty1 DType -> DType -> DType
`DAppT` Map Name DType -> DType -> DType
substType Map Name DType
subst DType
ty2
substType Map Name DType
subst (DAppKindT DType
ty DType
ki) = Map Name DType -> DType -> DType
substType Map Name DType
subst DType
ty DType -> DType -> DType
`DAppKindT` Map Name DType -> DType -> DType
substType Map Name DType
subst DType
ki
substType Map Name DType
subst (DSigT DType
ty DType
ki) = Map Name DType -> DType -> DType
substType Map Name DType
subst DType
ty DType -> DType -> DType
`DSigT` Map Name DType -> DType -> DType
substType Map Name DType
subst DType
ki
substType Map Name DType
subst (DVarT Name
n) =
  case Name -> Map Name DType -> Maybe DType
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
n Map Name DType
subst of
    Just DType
ki -> DType
ki
    Maybe DType
Nothing -> Name -> DType
DVarT Name
n
substType Map Name DType
_ ty :: DType
ty@(DConT {}) = DType
ty
substType Map Name DType
_ ty :: DType
ty@(DType
DArrowT)  = DType
ty
substType Map Name DType
_ ty :: DType
ty@(DLitT {}) = DType
ty
substType Map Name DType
_ ty :: DType
ty@DType
DWildCardT = DType
ty

subst_tvb :: Map Name DKind -> DTyVarBndr -> (Map Name DKind, DTyVarBndr)
subst_tvb :: Map Name DType -> DTyVarBndr -> (Map Name DType, DTyVarBndr)
subst_tvb Map Name DType
s tvb :: DTyVarBndr
tvb@(DPlainTV Name
n) = (Name -> Map Name DType -> Map Name DType
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Name
n Map Name DType
s, DTyVarBndr
tvb)
subst_tvb Map Name DType
s (DKindedTV Name
n DType
k)  = (Name -> Map Name DType -> Map Name DType
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Name
n Map Name DType
s, Name -> DType -> DTyVarBndr
DKindedTV Name
n (Map Name DType -> DType -> DType
substKind Map Name DType
s DType
k))

dropTvbKind :: DTyVarBndr -> DTyVarBndr
dropTvbKind :: DTyVarBndr -> DTyVarBndr
dropTvbKind tvb :: DTyVarBndr
tvb@(DPlainTV {}) = DTyVarBndr
tvb
dropTvbKind (DKindedTV Name
n DType
_)   = Name -> DTyVarBndr
DPlainTV Name
n

-- apply a type to a list of types
foldType :: DType -> [DType] -> DType
foldType :: DType -> [DType] -> DType
foldType = (DType -> DType -> DType) -> DType -> [DType] -> DType
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl DType -> DType -> DType
DAppT

-- apply a type to a list of type variable binders
foldTypeTvbs :: DType -> [DTyVarBndr] -> DType
foldTypeTvbs :: DType -> [DTyVarBndr] -> DType
foldTypeTvbs DType
ty = DType -> [DType] -> DType
foldType DType
ty ([DType] -> DType)
-> ([DTyVarBndr] -> [DType]) -> [DTyVarBndr] -> DType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DTyVarBndr -> DType) -> [DTyVarBndr] -> [DType]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndr -> DType
tvbToType

-- Construct a data type's variable binders, possibly using fresh variables
-- from the data type's kind signature.
buildDataDTvbs :: DsMonad q => [DTyVarBndr] -> Maybe DKind -> q [DTyVarBndr]
buildDataDTvbs :: [DTyVarBndr] -> Maybe DType -> q [DTyVarBndr]
buildDataDTvbs [DTyVarBndr]
tvbs Maybe DType
mk = do
  [DTyVarBndr]
extra_tvbs <- DType -> q [DTyVarBndr]
forall (q :: * -> *). DsMonad q => DType -> q [DTyVarBndr]
mkExtraDKindBinders (DType -> q [DTyVarBndr]) -> DType -> q [DTyVarBndr]
forall a b. (a -> b) -> a -> b
$ DType -> Maybe DType -> DType
forall a. a -> Maybe a -> a
fromMaybe (Name -> DType
DConT Name
typeKindName) Maybe DType
mk
  [DTyVarBndr] -> q [DTyVarBndr]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([DTyVarBndr] -> q [DTyVarBndr]) -> [DTyVarBndr] -> q [DTyVarBndr]
forall a b. (a -> b) -> a -> b
$ [DTyVarBndr]
tvbs [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr]
forall a. [a] -> [a] -> [a]
++ [DTyVarBndr]
extra_tvbs

-- apply an expression to a list of expressions
foldExp :: DExp -> [DExp] -> DExp
foldExp :: DExp -> [DExp] -> DExp
foldExp = (DExp -> DExp -> DExp) -> DExp -> [DExp] -> DExp
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl DExp -> DExp -> DExp
DAppE

-- is a function type?
isFunTy :: DType -> Bool
isFunTy :: DType -> Bool
isFunTy (DAppT (DAppT DType
DArrowT DType
_) DType
_) = Bool
True
isFunTy (DForallT ForallVisFlag
_ [DTyVarBndr]
_ DType
_)            = Bool
True
isFunTy DType
_                           = Bool
False

-- choose the first non-empty list
orIfEmpty :: [a] -> [a] -> [a]
orIfEmpty :: [a] -> [a] -> [a]
orIfEmpty [] [a]
x = [a]
x
orIfEmpty [a]
x  [a]
_ = [a]
x

-- build a pattern match over several expressions, each with only one pattern
multiCase :: [DExp] -> [DPat] -> DExp -> DExp
multiCase :: [DExp] -> [DPat] -> DExp -> DExp
multiCase [] [] DExp
body = DExp
body
multiCase [DExp]
scruts [DPat]
pats DExp
body =
  DExp -> [DMatch] -> DExp
DCaseE ([DExp] -> DExp
mkTupleDExp [DExp]
scruts) [DPat -> DExp -> DMatch
DMatch ([DPat] -> DPat
mkTupleDPat [DPat]
pats) DExp
body]

-- a monad transformer for writing a monoid alongside returning a Q
newtype QWithAux m q a = QWA { QWithAux m q a -> WriterT m q a
runQWA :: WriterT m q a }
  deriving ( a -> QWithAux m q b -> QWithAux m q a
(a -> b) -> QWithAux m q a -> QWithAux m q b
(forall a b. (a -> b) -> QWithAux m q a -> QWithAux m q b)
-> (forall a b. a -> QWithAux m q b -> QWithAux m q a)
-> Functor (QWithAux m q)
forall a b. a -> QWithAux m q b -> QWithAux m q a
forall a b. (a -> b) -> QWithAux m q a -> QWithAux m q b
forall m (q :: * -> *) a b.
Functor q =>
a -> QWithAux m q b -> QWithAux m q a
forall m (q :: * -> *) a b.
Functor q =>
(a -> b) -> QWithAux m q a -> QWithAux m q b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> QWithAux m q b -> QWithAux m q a
$c<$ :: forall m (q :: * -> *) a b.
Functor q =>
a -> QWithAux m q b -> QWithAux m q a
fmap :: (a -> b) -> QWithAux m q a -> QWithAux m q b
$cfmap :: forall m (q :: * -> *) a b.
Functor q =>
(a -> b) -> QWithAux m q a -> QWithAux m q b
Functor, Functor (QWithAux m q)
a -> QWithAux m q a
Functor (QWithAux m q)
-> (forall a. a -> QWithAux m q a)
-> (forall a b.
    QWithAux m q (a -> b) -> QWithAux m q a -> QWithAux m q b)
-> (forall a b c.
    (a -> b -> c)
    -> QWithAux m q a -> QWithAux m q b -> QWithAux m q c)
-> (forall a b. QWithAux m q a -> QWithAux m q b -> QWithAux m q b)
-> (forall a b. QWithAux m q a -> QWithAux m q b -> QWithAux m q a)
-> Applicative (QWithAux m q)
QWithAux m q a -> QWithAux m q b -> QWithAux m q b
QWithAux m q a -> QWithAux m q b -> QWithAux m q a
QWithAux m q (a -> b) -> QWithAux m q a -> QWithAux m q b
(a -> b -> c) -> QWithAux m q a -> QWithAux m q b -> QWithAux m q c
forall a. a -> QWithAux m q a
forall a b. QWithAux m q a -> QWithAux m q b -> QWithAux m q a
forall a b. QWithAux m q a -> QWithAux m q b -> QWithAux m q b
forall a b.
QWithAux m q (a -> b) -> QWithAux m q a -> QWithAux m q b
forall a b c.
(a -> b -> c) -> QWithAux m q a -> QWithAux m q b -> QWithAux m q c
forall m (q :: * -> *).
(Monoid m, Applicative q) =>
Functor (QWithAux m q)
forall m (q :: * -> *) a.
(Monoid m, Applicative q) =>
a -> QWithAux m q a
forall m (q :: * -> *) a b.
(Monoid m, Applicative q) =>
QWithAux m q a -> QWithAux m q b -> QWithAux m q a
forall m (q :: * -> *) a b.
(Monoid m, Applicative q) =>
QWithAux m q a -> QWithAux m q b -> QWithAux m q b
forall m (q :: * -> *) a b.
(Monoid m, Applicative q) =>
QWithAux m q (a -> b) -> QWithAux m q a -> QWithAux m q b
forall m (q :: * -> *) a b c.
(Monoid m, Applicative q) =>
(a -> b -> c) -> QWithAux m q a -> QWithAux m q b -> QWithAux m q c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: QWithAux m q a -> QWithAux m q b -> QWithAux m q a
$c<* :: forall m (q :: * -> *) a b.
(Monoid m, Applicative q) =>
QWithAux m q a -> QWithAux m q b -> QWithAux m q a
*> :: QWithAux m q a -> QWithAux m q b -> QWithAux m q b
$c*> :: forall m (q :: * -> *) a b.
(Monoid m, Applicative q) =>
QWithAux m q a -> QWithAux m q b -> QWithAux m q b
liftA2 :: (a -> b -> c) -> QWithAux m q a -> QWithAux m q b -> QWithAux m q c
$cliftA2 :: forall m (q :: * -> *) a b c.
(Monoid m, Applicative q) =>
(a -> b -> c) -> QWithAux m q a -> QWithAux m q b -> QWithAux m q c
<*> :: QWithAux m q (a -> b) -> QWithAux m q a -> QWithAux m q b
$c<*> :: forall m (q :: * -> *) a b.
(Monoid m, Applicative q) =>
QWithAux m q (a -> b) -> QWithAux m q a -> QWithAux m q b
pure :: a -> QWithAux m q a
$cpure :: forall m (q :: * -> *) a.
(Monoid m, Applicative q) =>
a -> QWithAux m q a
$cp1Applicative :: forall m (q :: * -> *).
(Monoid m, Applicative q) =>
Functor (QWithAux m q)
Applicative, Applicative (QWithAux m q)
a -> QWithAux m q a
Applicative (QWithAux m q)
-> (forall a b.
    QWithAux m q a -> (a -> QWithAux m q b) -> QWithAux m q b)
-> (forall a b. QWithAux m q a -> QWithAux m q b -> QWithAux m q b)
-> (forall a. a -> QWithAux m q a)
-> Monad (QWithAux m q)
QWithAux m q a -> (a -> QWithAux m q b) -> QWithAux m q b
QWithAux m q a -> QWithAux m q b -> QWithAux m q b
forall a. a -> QWithAux m q a
forall a b. QWithAux m q a -> QWithAux m q b -> QWithAux m q b
forall a b.
QWithAux m q a -> (a -> QWithAux m q b) -> QWithAux m q b
forall m (q :: * -> *).
(Monoid m, Monad q) =>
Applicative (QWithAux m q)
forall m (q :: * -> *) a.
(Monoid m, Monad q) =>
a -> QWithAux m q a
forall m (q :: * -> *) a b.
(Monoid m, Monad q) =>
QWithAux m q a -> QWithAux m q b -> QWithAux m q b
forall m (q :: * -> *) a b.
(Monoid m, Monad q) =>
QWithAux m q a -> (a -> QWithAux m q b) -> QWithAux m q b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> QWithAux m q a
$creturn :: forall m (q :: * -> *) a.
(Monoid m, Monad q) =>
a -> QWithAux m q a
>> :: QWithAux m q a -> QWithAux m q b -> QWithAux m q b
$c>> :: forall m (q :: * -> *) a b.
(Monoid m, Monad q) =>
QWithAux m q a -> QWithAux m q b -> QWithAux m q b
>>= :: QWithAux m q a -> (a -> QWithAux m q b) -> QWithAux m q b
$c>>= :: forall m (q :: * -> *) a b.
(Monoid m, Monad q) =>
QWithAux m q a -> (a -> QWithAux m q b) -> QWithAux m q b
$cp1Monad :: forall m (q :: * -> *).
(Monoid m, Monad q) =>
Applicative (QWithAux m q)
Monad, m a -> QWithAux m m a
(forall (m :: * -> *) a. Monad m => m a -> QWithAux m m a)
-> MonadTrans (QWithAux m)
forall m (m :: * -> *) a.
(Monoid m, Monad m) =>
m a -> QWithAux m m a
forall (m :: * -> *) a. Monad m => m a -> QWithAux m m a
forall (t :: (* -> *) -> * -> *).
(forall (m :: * -> *) a. Monad m => m a -> t m a) -> MonadTrans t
lift :: m a -> QWithAux m m a
$clift :: forall m (m :: * -> *) a.
(Monoid m, Monad m) =>
m a -> QWithAux m m a
MonadTrans
           , MonadWriter m, MonadReader r
           , Monad (QWithAux m q)
Monad (QWithAux m q)
-> (forall a. String -> QWithAux m q a) -> MonadFail (QWithAux m q)
String -> QWithAux m q a
forall a. String -> QWithAux m q a
forall m (q :: * -> *).
(Monoid m, MonadFail q) =>
Monad (QWithAux m q)
forall m (q :: * -> *) a.
(Monoid m, MonadFail q) =>
String -> QWithAux m q a
forall (m :: * -> *).
Monad m -> (forall a. String -> m a) -> MonadFail m
fail :: String -> QWithAux m q a
$cfail :: forall m (q :: * -> *) a.
(Monoid m, MonadFail q) =>
String -> QWithAux m q a
$cp1MonadFail :: forall m (q :: * -> *).
(Monoid m, MonadFail q) =>
Monad (QWithAux m q)
MonadFail, Monad (QWithAux m q)
Monad (QWithAux m q)
-> (forall a. IO a -> QWithAux m q a) -> MonadIO (QWithAux m q)
IO a -> QWithAux m q a
forall a. IO a -> QWithAux m q a
forall m (q :: * -> *).
(Monoid m, MonadIO q) =>
Monad (QWithAux m q)
forall m (q :: * -> *) a.
(Monoid m, MonadIO q) =>
IO a -> QWithAux m q a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: IO a -> QWithAux m q a
$cliftIO :: forall m (q :: * -> *) a.
(Monoid m, MonadIO q) =>
IO a -> QWithAux m q a
$cp1MonadIO :: forall m (q :: * -> *).
(Monoid m, MonadIO q) =>
Monad (QWithAux m q)
MonadIO, MonadFail (QWithAux m q)
MonadIO (QWithAux m q)
QWithAux m q [Extension]
QWithAux m q (Maybe a)
QWithAux m q Loc
a -> QWithAux m q ()
Bool -> String -> QWithAux m q (Maybe Name)
Bool -> String -> QWithAux m q ()
String -> QWithAux m q String
String -> QWithAux m q Name
String -> QWithAux m q ()
[Dec] -> QWithAux m q ()
IO a -> QWithAux m q a
Q () -> QWithAux m q ()
Name -> QWithAux m q [DecidedStrictness]
Name -> QWithAux m q [Role]
Name -> QWithAux m q (Maybe Fixity)
Name -> QWithAux m q Type
Name -> QWithAux m q Info
Name -> [Type] -> QWithAux m q [Dec]
MonadIO (QWithAux m q)
-> MonadFail (QWithAux m q)
-> (String -> QWithAux m q Name)
-> (Bool -> String -> QWithAux m q ())
-> (forall a. QWithAux m q a -> QWithAux m q a -> QWithAux m q a)
-> (Bool -> String -> QWithAux m q (Maybe Name))
-> (Name -> QWithAux m q Info)
-> (Name -> QWithAux m q (Maybe Fixity))
-> (Name -> QWithAux m q Type)
-> (Name -> [Type] -> QWithAux m q [Dec])
-> (Name -> QWithAux m q [Role])
-> (forall a. Data a => AnnLookup -> QWithAux m q [a])
-> (Module -> QWithAux m q ModuleInfo)
-> (Name -> QWithAux m q [DecidedStrictness])
-> QWithAux m q Loc
-> (forall a. IO a -> QWithAux m q a)
-> (String -> QWithAux m q ())
-> (String -> QWithAux m q String)
-> ([Dec] -> QWithAux m q ())
-> (ForeignSrcLang -> String -> QWithAux m q ())
-> (Q () -> QWithAux m q ())
-> (String -> QWithAux m q ())
-> (forall a. Typeable a => QWithAux m q (Maybe a))
-> (forall a. Typeable a => a -> QWithAux m q ())
-> (Extension -> QWithAux m q Bool)
-> QWithAux m q [Extension]
-> Quasi (QWithAux m q)
Extension -> QWithAux m q Bool
ForeignSrcLang -> String -> QWithAux m q ()
Module -> QWithAux m q ModuleInfo
AnnLookup -> QWithAux m q [a]
QWithAux m q a -> QWithAux m q a -> QWithAux m q a
forall a. Data a => AnnLookup -> QWithAux m q [a]
forall a. Typeable a => QWithAux m q (Maybe a)
forall a. Typeable a => a -> QWithAux m q ()
forall a. IO a -> QWithAux m q a
forall a. QWithAux m q a -> QWithAux m q a -> QWithAux m q a
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
MonadFail (QWithAux m q)
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
MonadIO (QWithAux m q)
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
QWithAux m q [Extension]
forall m (q :: * -> *). (Quasi q, Monoid m) => QWithAux m q Loc
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Bool -> String -> QWithAux m q (Maybe Name)
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Bool -> String -> QWithAux m q ()
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
String -> QWithAux m q String
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
String -> QWithAux m q Name
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
String -> QWithAux m q ()
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
[Dec] -> QWithAux m q ()
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Q () -> QWithAux m q ()
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Name -> QWithAux m q [DecidedStrictness]
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Name -> QWithAux m q [Role]
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Name -> QWithAux m q (Maybe Fixity)
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Name -> QWithAux m q Type
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Name -> QWithAux m q Info
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Name -> [Type] -> QWithAux m q [Dec]
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Extension -> QWithAux m q Bool
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
ForeignSrcLang -> String -> QWithAux m q ()
forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Module -> QWithAux m q ModuleInfo
forall m (q :: * -> *) a.
(Quasi q, Monoid m, Data a) =>
AnnLookup -> QWithAux m q [a]
forall m (q :: * -> *) a.
(Quasi q, Monoid m, Typeable a) =>
QWithAux m q (Maybe a)
forall m (q :: * -> *) a.
(Quasi q, Monoid m, Typeable a) =>
a -> QWithAux m q ()
forall m (q :: * -> *) a.
(Quasi q, Monoid m) =>
IO a -> QWithAux m q a
forall m (q :: * -> *) a.
(Quasi q, Monoid m) =>
QWithAux m q a -> QWithAux m q a -> QWithAux m q a
forall (m :: * -> *).
MonadIO m
-> MonadFail m
-> (String -> m Name)
-> (Bool -> String -> m ())
-> (forall a. m a -> m a -> m a)
-> (Bool -> String -> m (Maybe Name))
-> (Name -> m Info)
-> (Name -> m (Maybe Fixity))
-> (Name -> m Type)
-> (Name -> [Type] -> m [Dec])
-> (Name -> m [Role])
-> (forall a. Data a => AnnLookup -> m [a])
-> (Module -> m ModuleInfo)
-> (Name -> m [DecidedStrictness])
-> m Loc
-> (forall a. IO a -> m a)
-> (String -> m ())
-> (String -> m String)
-> ([Dec] -> m ())
-> (ForeignSrcLang -> String -> m ())
-> (Q () -> m ())
-> (String -> m ())
-> (forall a. Typeable a => m (Maybe a))
-> (forall a. Typeable a => a -> m ())
-> (Extension -> m Bool)
-> m [Extension]
-> Quasi m
qExtsEnabled :: QWithAux m q [Extension]
$cqExtsEnabled :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
QWithAux m q [Extension]
qIsExtEnabled :: Extension -> QWithAux m q Bool
$cqIsExtEnabled :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Extension -> QWithAux m q Bool
qPutQ :: a -> QWithAux m q ()
$cqPutQ :: forall m (q :: * -> *) a.
(Quasi q, Monoid m, Typeable a) =>
a -> QWithAux m q ()
qGetQ :: QWithAux m q (Maybe a)
$cqGetQ :: forall m (q :: * -> *) a.
(Quasi q, Monoid m, Typeable a) =>
QWithAux m q (Maybe a)
qAddCorePlugin :: String -> QWithAux m q ()
$cqAddCorePlugin :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
String -> QWithAux m q ()
qAddModFinalizer :: Q () -> QWithAux m q ()
$cqAddModFinalizer :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Q () -> QWithAux m q ()
qAddForeignFilePath :: ForeignSrcLang -> String -> QWithAux m q ()
$cqAddForeignFilePath :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
ForeignSrcLang -> String -> QWithAux m q ()
qAddTopDecls :: [Dec] -> QWithAux m q ()
$cqAddTopDecls :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
[Dec] -> QWithAux m q ()
qAddTempFile :: String -> QWithAux m q String
$cqAddTempFile :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
String -> QWithAux m q String
qAddDependentFile :: String -> QWithAux m q ()
$cqAddDependentFile :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
String -> QWithAux m q ()
qRunIO :: IO a -> QWithAux m q a
$cqRunIO :: forall m (q :: * -> *) a.
(Quasi q, Monoid m) =>
IO a -> QWithAux m q a
qLocation :: QWithAux m q Loc
$cqLocation :: forall m (q :: * -> *). (Quasi q, Monoid m) => QWithAux m q Loc
qReifyConStrictness :: Name -> QWithAux m q [DecidedStrictness]
$cqReifyConStrictness :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Name -> QWithAux m q [DecidedStrictness]
qReifyModule :: Module -> QWithAux m q ModuleInfo
$cqReifyModule :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Module -> QWithAux m q ModuleInfo
qReifyAnnotations :: AnnLookup -> QWithAux m q [a]
$cqReifyAnnotations :: forall m (q :: * -> *) a.
(Quasi q, Monoid m, Data a) =>
AnnLookup -> QWithAux m q [a]
qReifyRoles :: Name -> QWithAux m q [Role]
$cqReifyRoles :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Name -> QWithAux m q [Role]
qReifyInstances :: Name -> [Type] -> QWithAux m q [Dec]
$cqReifyInstances :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Name -> [Type] -> QWithAux m q [Dec]
qReifyType :: Name -> QWithAux m q Type
$cqReifyType :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Name -> QWithAux m q Type
qReifyFixity :: Name -> QWithAux m q (Maybe Fixity)
$cqReifyFixity :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Name -> QWithAux m q (Maybe Fixity)
qReify :: Name -> QWithAux m q Info
$cqReify :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Name -> QWithAux m q Info
qLookupName :: Bool -> String -> QWithAux m q (Maybe Name)
$cqLookupName :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Bool -> String -> QWithAux m q (Maybe Name)
qRecover :: QWithAux m q a -> QWithAux m q a -> QWithAux m q a
$cqRecover :: forall m (q :: * -> *) a.
(Quasi q, Monoid m) =>
QWithAux m q a -> QWithAux m q a -> QWithAux m q a
qReport :: Bool -> String -> QWithAux m q ()
$cqReport :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
Bool -> String -> QWithAux m q ()
qNewName :: String -> QWithAux m q Name
$cqNewName :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
String -> QWithAux m q Name
$cp2Quasi :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
MonadFail (QWithAux m q)
$cp1Quasi :: forall m (q :: * -> *).
(Quasi q, Monoid m) =>
MonadIO (QWithAux m q)
Quasi, MonadFail (QWithAux m q)
Quasi (QWithAux m q)
QWithAux m q [Dec]
Quasi (QWithAux m q)
-> MonadFail (QWithAux m q)
-> QWithAux m q [Dec]
-> DsMonad (QWithAux m q)
forall m (q :: * -> *).
(DsMonad q, Monoid m) =>
MonadFail (QWithAux m q)
forall m (q :: * -> *).
(DsMonad q, Monoid m) =>
Quasi (QWithAux m q)
forall m (q :: * -> *). (DsMonad q, Monoid m) => QWithAux m q [Dec]
forall (m :: * -> *).
Quasi m -> MonadFail m -> m [Dec] -> DsMonad m
localDeclarations :: QWithAux m q [Dec]
$clocalDeclarations :: forall m (q :: * -> *). (DsMonad q, Monoid m) => QWithAux m q [Dec]
$cp2DsMonad :: forall m (q :: * -> *).
(DsMonad q, Monoid m) =>
MonadFail (QWithAux m q)
$cp1DsMonad :: forall m (q :: * -> *).
(DsMonad q, Monoid m) =>
Quasi (QWithAux m q)
DsMonad )

-- run a computation with an auxiliary monoid, discarding the monoid result
evalWithoutAux :: Quasi q => QWithAux m q a -> q a
evalWithoutAux :: QWithAux m q a -> q a
evalWithoutAux = ((a, m) -> a) -> q (a, m) -> q a
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (a, m) -> a
forall a b. (a, b) -> a
fst (q (a, m) -> q a)
-> (QWithAux m q a -> q (a, m)) -> QWithAux m q a -> q a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WriterT m q a -> q (a, m)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT m q a -> q (a, m))
-> (QWithAux m q a -> WriterT m q a) -> QWithAux m q a -> q (a, m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QWithAux m q a -> WriterT m q a
forall m (q :: * -> *) a. QWithAux m q a -> WriterT m q a
runQWA

-- run a computation with an auxiliary monoid, returning only the monoid result
evalForAux :: Quasi q => QWithAux m q a -> q m
evalForAux :: QWithAux m q a -> q m
evalForAux = WriterT m q a -> q m
forall (m :: * -> *) w a. Monad m => WriterT w m a -> m w
execWriterT (WriterT m q a -> q m)
-> (QWithAux m q a -> WriterT m q a) -> QWithAux m q a -> q m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QWithAux m q a -> WriterT m q a
forall m (q :: * -> *) a. QWithAux m q a -> WriterT m q a
runQWA

-- run a computation with an auxiliary monoid, return both the result
-- of the computation and the monoid result
evalForPair :: QWithAux m q a -> q (a, m)
evalForPair :: QWithAux m q a -> q (a, m)
evalForPair = WriterT m q a -> q (a, m)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT m q a -> q (a, m))
-> (QWithAux m q a -> WriterT m q a) -> QWithAux m q a -> q (a, m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QWithAux m q a -> WriterT m q a
forall m (q :: * -> *) a. QWithAux m q a -> WriterT m q a
runQWA

-- in a computation with an auxiliary map, add a binding to the map
addBinding :: (Quasi q, Ord k) => k -> v -> QWithAux (Map.Map k v) q ()
addBinding :: k -> v -> QWithAux (Map k v) q ()
addBinding k
k v
v = Map k v -> QWithAux (Map k v) q ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (k -> v -> Map k v
forall k a. k -> a -> Map k a
Map.singleton k
k v
v)

-- in a computation with an auxiliar list, add an element to the list
addElement :: Quasi q => elt -> QWithAux [elt] q ()
addElement :: elt -> QWithAux [elt] q ()
addElement elt
elt = [elt] -> QWithAux [elt] q ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [elt
elt]

-- | Call 'lookupTypeNameWithLocals' first to ensure we have a 'Name' in the
-- type namespace, then call 'dsReify'.

-- See also Note [Using dsReifyTypeNameInfo when promoting instances]
-- in Data.Singletons.Promote.
dsReifyTypeNameInfo :: DsMonad q => Name -> q (Maybe DInfo)
dsReifyTypeNameInfo :: Name -> q (Maybe DInfo)
dsReifyTypeNameInfo Name
ty_name = do
  Maybe Name
mb_name <- String -> q (Maybe Name)
forall (q :: * -> *). DsMonad q => String -> q (Maybe Name)
lookupTypeNameWithLocals (Name -> String
nameBase Name
ty_name)
  case Maybe Name
mb_name of
    Just Name
n  -> Name -> q (Maybe DInfo)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
dsReify Name
n
    Maybe Name
Nothing -> Maybe DInfo -> q (Maybe DInfo)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe DInfo
forall a. Maybe a
Nothing

-- lift concatMap into a monad
-- could this be more efficient?
concatMapM :: (Monad monad, Monoid monoid, Traversable t)
           => (a -> monad monoid) -> t a -> monad monoid
concatMapM :: (a -> monad monoid) -> t a -> monad monoid
concatMapM a -> monad monoid
fn t a
list = do
  t monoid
bss <- (a -> monad monoid) -> t a -> monad (t monoid)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM a -> monad monoid
fn t a
list
  monoid -> monad monoid
forall (m :: * -> *) a. Monad m => a -> m a
return (monoid -> monad monoid) -> monoid -> monad monoid
forall a b. (a -> b) -> a -> b
$ t monoid -> monoid
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold t monoid
bss

-- like GHC's
mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM :: (a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM a -> m (Maybe b)
_ [] = [b] -> m [b]
forall (m :: * -> *) a. Monad m => a -> m a
return []
mapMaybeM a -> m (Maybe b)
f (a
x:[a]
xs) = do
  Maybe b
y <- a -> m (Maybe b)
f a
x
  [b]
ys <- (a -> m (Maybe b)) -> [a] -> m [b]
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM a -> m (Maybe b)
f [a]
xs
  [b] -> m [b]
forall (m :: * -> *) a. Monad m => a -> m a
return ([b] -> m [b]) -> [b] -> m [b]
forall a b. (a -> b) -> a -> b
$ case Maybe b
y of
    Maybe b
Nothing -> [b]
ys
    Just b
z  -> b
z b -> [b] -> [b]
forall a. a -> [a] -> [a]
: [b]
ys

-- make a one-element list
listify :: a -> [a]
listify :: a -> [a]
listify = (a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[])

fstOf3 :: (a,b,c) -> a
fstOf3 :: (a, b, c) -> a
fstOf3 (a
a,b
_,c
_) = a
a

liftFst :: (a -> b) -> (a, c) -> (b, c)
liftFst :: (a -> b) -> (a, c) -> (b, c)
liftFst a -> b
f (a
a, c
c) = (a -> b
f a
a, c
c)

liftSnd :: (a -> b) -> (c, a) -> (c, b)
liftSnd :: (a -> b) -> (c, a) -> (c, b)
liftSnd a -> b
f (c
c, a
a) = (c
c, a -> b
f a
a)

snocView :: [a] -> ([a], a)
snocView :: [a] -> ([a], a)
snocView [] = String -> ([a], a)
forall a. HasCallStack => String -> a
error String
"snocView nil"
snocView [a
x] = ([], a
x)
snocView (a
x : [a]
xs) = ([a] -> [a]) -> ([a], a) -> ([a], a)
forall a b c. (a -> b) -> (a, c) -> (b, c)
liftFst (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:) ([a] -> ([a], a)
forall a. [a] -> ([a], a)
snocView [a]
xs)

partitionWith :: (a -> Either b c) -> [a] -> ([b], [c])
partitionWith :: (a -> Either b c) -> [a] -> ([b], [c])
partitionWith a -> Either b c
f = [b] -> [c] -> [a] -> ([b], [c])
go [] []
  where go :: [b] -> [c] -> [a] -> ([b], [c])
go [b]
bs [c]
cs []     = ([b] -> [b]
forall a. [a] -> [a]
reverse [b]
bs, [c] -> [c]
forall a. [a] -> [a]
reverse [c]
cs)
        go [b]
bs [c]
cs (a
a:[a]
as) =
          case a -> Either b c
f a
a of
            Left b
b  -> [b] -> [c] -> [a] -> ([b], [c])
go (b
bb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
bs) [c]
cs [a]
as
            Right c
c -> [b] -> [c] -> [a] -> ([b], [c])
go [b]
bs (c
cc -> [c] -> [c]
forall a. a -> [a] -> [a]
:[c]
cs) [a]
as

partitionWithM :: Monad m => (a -> m (Either b c)) -> [a] -> m ([b], [c])
partitionWithM :: (a -> m (Either b c)) -> [a] -> m ([b], [c])
partitionWithM a -> m (Either b c)
f = [b] -> [c] -> [a] -> m ([b], [c])
go [] []
  where go :: [b] -> [c] -> [a] -> m ([b], [c])
go [b]
bs [c]
cs []     = ([b], [c]) -> m ([b], [c])
forall (m :: * -> *) a. Monad m => a -> m a
return ([b] -> [b]
forall a. [a] -> [a]
reverse [b]
bs, [c] -> [c]
forall a. [a] -> [a]
reverse [c]
cs)
        go [b]
bs [c]
cs (a
a:[a]
as) = do
          Either b c
fa <- a -> m (Either b c)
f a
a
          case Either b c
fa of
            Left b
b  -> [b] -> [c] -> [a] -> m ([b], [c])
go (b
bb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
bs) [c]
cs [a]
as
            Right c
c -> [b] -> [c] -> [a] -> m ([b], [c])
go [b]
bs (c
cc -> [c] -> [c]
forall a. a -> [a] -> [a]
:[c]
cs) [a]
as

partitionLetDecs :: [DDec] -> ([DLetDec], [DDec])
partitionLetDecs :: [DDec] -> ([DLetDec], [DDec])
partitionLetDecs = (DDec -> Either DLetDec DDec) -> [DDec] -> ([DLetDec], [DDec])
forall a b c. (a -> Either b c) -> [a] -> ([b], [c])
partitionWith (\case DLetDec DLetDec
ld -> DLetDec -> Either DLetDec DDec
forall a b. a -> Either a b
Left DLetDec
ld
                                        DDec
dec        -> DDec -> Either DLetDec DDec
forall a b. b -> Either a b
Right DDec
dec)

{-# INLINEABLE zipWith3M #-}
zipWith3M :: Monad m => (a -> b -> m c) -> [a] -> [b] -> m [c]
zipWith3M :: (a -> b -> m c) -> [a] -> [b] -> m [c]
zipWith3M a -> b -> m c
f (a
a:[a]
as) (b
b:[b]
bs) = (:) (c -> [c] -> [c]) -> m c -> m ([c] -> [c])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> b -> m c
f a
a b
b m ([c] -> [c]) -> m [c] -> m [c]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (a -> b -> m c) -> [a] -> [b] -> m [c]
forall (m :: * -> *) a b c.
Monad m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWith3M a -> b -> m c
f [a]
as [b]
bs
zipWith3M a -> b -> m c
_ [a]
_ [b]
_ = [c] -> m [c]
forall (m :: * -> *) a. Monad m => a -> m a
return []

mapAndUnzip3M :: Monad m => (a -> m (b,c,d)) -> [a] -> m ([b],[c],[d])
mapAndUnzip3M :: (a -> m (b, c, d)) -> [a] -> m ([b], [c], [d])
mapAndUnzip3M a -> m (b, c, d)
_ []     = ([b], [c], [d]) -> m ([b], [c], [d])
forall (m :: * -> *) a. Monad m => a -> m a
return ([],[],[])
mapAndUnzip3M a -> m (b, c, d)
f (a
x:[a]
xs) = do
    (b
r1,  c
r2,  d
r3)  <- a -> m (b, c, d)
f a
x
    ([b]
rs1, [c]
rs2, [d]
rs3) <- (a -> m (b, c, d)) -> [a] -> m ([b], [c], [d])
forall (m :: * -> *) a b c d.
Monad m =>
(a -> m (b, c, d)) -> [a] -> m ([b], [c], [d])
mapAndUnzip3M a -> m (b, c, d)
f [a]
xs
    ([b], [c], [d]) -> m ([b], [c], [d])
forall (m :: * -> *) a. Monad m => a -> m a
return (b
r1b -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
rs1, c
r2c -> [c] -> [c]
forall a. a -> [a] -> [a]
:[c]
rs2, d
r3d -> [d] -> [d]
forall a. a -> [a] -> [a]
:[d]
rs3)

-- 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
'_'