{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators #-}

-- |
-- Module      :   Grisette.Internal.TH.Derivation.Common
-- Copyright   :   (c) Sirui Lu 2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.TH.Derivation.Common
  ( CheckArgsResult (..),
    checkArgs,
    ctxForVar,
    EvalModeConfig (..),
    DeriveConfig (..),
    extraEvalModeConstraint,
    extraBitSizeConstraint,
    extraFpBitSizeConstraint,
    extraExtraMergeableConstraint,
    extraConstraint,
    specializeResult,
    evalModeSpecializeList,
    isVarUsedInFields,
    freshenCheckArgsResult,
  )
where

import Control.Monad (foldM, unless, when, zipWithM)
import Data.Bifunctor (first)
import qualified Data.Map as M
import Data.Maybe (catMaybes, mapMaybe)
import qualified Data.Set as S
import GHC.TypeLits (KnownNat, Nat, type (<=))
import Grisette.Internal.Internal.Decl.Core.Data.Class.Mergeable
  ( Mergeable,
    Mergeable1,
    Mergeable2,
  )
import Grisette.Internal.SymPrim.FP (ValidFP)
import Grisette.Internal.Unified.EvalModeTag (EvalModeTag (C, S))
import Grisette.Internal.Unified.Util (DecideEvalMode)
import Language.Haskell.TH
  ( Kind,
    Name,
    Pred,
    Q,
    Type (AppT, ArrowT, ConT, PromotedT, StarT, VarT),
    conT,
    nameBase,
    newName,
  )
import Language.Haskell.TH.Datatype
  ( ConstructorInfo (constructorFields, constructorName, constructorVars),
    DatatypeInfo (datatypeCons, datatypeVars),
    TypeSubstitution (applySubstitution, freeVariables),
    reifyDatatype,
    tvName,
  )
import Language.Haskell.TH.Datatype.TyVarBndr (mapTVName, tvKind)

-- | Result of 'checkArgs' for a data type.
data CheckArgsResult = CheckArgsResult
  { CheckArgsResult -> [ConstructorInfo]
constructors :: [ConstructorInfo],
    CheckArgsResult -> [(Kind, Kind)]
keptVars :: [(Type, Kind)],
    CheckArgsResult -> [(Kind, Kind)]
argVars :: [(Type, Kind)]
  }

-- | Specialize the evaluation mode tags for the t'CheckArgsResult'.
specializeResult :: [(Int, EvalModeTag)] -> CheckArgsResult -> Q CheckArgsResult
specializeResult :: [(Int, EvalModeTag)] -> CheckArgsResult -> Q CheckArgsResult
specializeResult [(Int, EvalModeTag)]
evalModeConfigs CheckArgsResult
result = do
  let modeToName :: EvalModeTag -> Name
modeToName EvalModeTag
C = 'C
      modeToName EvalModeTag
S = 'S
  map <-
    ([(Kind, Kind)] -> (Int, EvalModeTag) -> Q [(Kind, Kind)])
-> [(Kind, Kind)] -> [(Int, EvalModeTag)] -> Q [(Kind, Kind)]
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM
      ( \[(Kind, Kind)]
lst (Int
n, EvalModeTag
tag) -> do
          let (Kind
_, Kind
knd) = [(Kind, Kind)]
lst [(Kind, Kind)] -> Int -> (Kind, Kind)
forall a. HasCallStack => [a] -> Int -> a
!! Int
n
          [(Kind, Kind)] -> Q [(Kind, Kind)]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Kind, Kind)] -> Q [(Kind, Kind)])
-> [(Kind, Kind)] -> Q [(Kind, Kind)]
forall a b. (a -> b) -> a -> b
$
            Int -> [(Kind, Kind)] -> [(Kind, Kind)]
forall a. Int -> [a] -> [a]
take Int
n [(Kind, Kind)]
lst
              [(Kind, Kind)] -> [(Kind, Kind)] -> [(Kind, Kind)]
forall a. [a] -> [a] -> [a]
++ [(Name -> Kind
PromotedT (Name -> Kind) -> Name -> Kind
forall a b. (a -> b) -> a -> b
$ EvalModeTag -> Name
modeToName EvalModeTag
tag, Kind
knd)]
              [(Kind, Kind)] -> [(Kind, Kind)] -> [(Kind, Kind)]
forall a. [a] -> [a] -> [a]
++ Int -> [(Kind, Kind)] -> [(Kind, Kind)]
forall a. Int -> [a] -> [a]
drop (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [(Kind, Kind)]
lst
      )
      (CheckArgsResult -> [(Kind, Kind)]
keptVars CheckArgsResult
result)
      [(Int, EvalModeTag)]
evalModeConfigs
  return $ result {keptVars = map}

freshenConstructorInfo :: ConstructorInfo -> Q ConstructorInfo
freshenConstructorInfo :: ConstructorInfo -> Q ConstructorInfo
freshenConstructorInfo ConstructorInfo
conInfo = do
  let vars :: [TyVarBndrUnit]
vars = ConstructorInfo -> [TyVarBndrUnit]
constructorVars ConstructorInfo
conInfo
  newNames <- (TyVarBndrUnit -> Q Name) -> [TyVarBndrUnit] -> Q [Name]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName (String -> Q Name)
-> (TyVarBndrUnit -> String) -> TyVarBndrUnit -> Q Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
nameBase (Name -> String)
-> (TyVarBndrUnit -> Name) -> TyVarBndrUnit -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndrUnit -> Name
forall flag. TyVarBndr_ flag -> Name
tvName) [TyVarBndrUnit]
vars
  let newVars = (Name -> TyVarBndrUnit -> TyVarBndrUnit)
-> [Name] -> [TyVarBndrUnit] -> [TyVarBndrUnit]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ((Name -> Name) -> TyVarBndrUnit -> TyVarBndrUnit
forall flag. (Name -> Name) -> TyVarBndr_ flag -> TyVarBndr_ flag
mapTVName ((Name -> Name) -> TyVarBndrUnit -> TyVarBndrUnit)
-> (Name -> Name -> Name) -> Name -> TyVarBndrUnit -> TyVarBndrUnit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name -> Name
forall a b. a -> b -> a
const) [Name]
newNames [TyVarBndrUnit]
vars
  let substMap = [(Name, Kind)] -> Map Name Kind
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Name, Kind)] -> Map Name Kind)
-> [(Name, Kind)] -> Map Name Kind
forall a b. (a -> b) -> a -> b
$ [Name] -> [Kind] -> [(Name, Kind)]
forall a b. [a] -> [b] -> [(a, b)]
zip (TyVarBndrUnit -> Name
forall flag. TyVarBndr_ flag -> Name
tvName (TyVarBndrUnit -> Name) -> [TyVarBndrUnit] -> [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TyVarBndrUnit]
vars) ([Kind] -> [(Name, Kind)]) -> [Kind] -> [(Name, Kind)]
forall a b. (a -> b) -> a -> b
$ Name -> Kind
VarT (Name -> Kind) -> [Name] -> [Kind]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
newNames
  return $ applySubstitution substMap conInfo {constructorVars = newVars}

-- | Freshen the type variables in the t'CheckArgsResult'.
freshenCheckArgsResult :: Bool -> CheckArgsResult -> Q CheckArgsResult
freshenCheckArgsResult :: Bool -> CheckArgsResult -> Q CheckArgsResult
freshenCheckArgsResult Bool
freshenNats CheckArgsResult
result = do
  let genNewName :: (Type, Kind) -> Q (Maybe Name)
      genNewName :: (Kind, Kind) -> Q (Maybe Name)
genNewName (VarT Name
_, Kind
knd) =
        if Bool -> Bool
not Bool
freshenNats Bool -> Bool -> Bool
&& Kind
knd Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Kind
ConT ''Nat
          then Maybe Name -> Q (Maybe Name)
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Name
forall a. Maybe a
Nothing
          else Name -> Maybe Name
forall a. a -> Maybe a
Just (Name -> Maybe Name) -> Q Name -> Q (Maybe Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"a"
      genNewName (Kind, Kind)
_ = Maybe Name -> Q (Maybe Name)
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Name
forall a. Maybe a
Nothing
  keptNewNames <- ((Kind, Kind) -> Q (Maybe Name))
-> [(Kind, Kind)] -> Q [Maybe Name]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Kind, Kind) -> Q (Maybe Name)
genNewName (CheckArgsResult -> [(Kind, Kind)]
keptVars CheckArgsResult
result)
  argNewNames <- traverse genNewName (argVars result)

  let substMap =
        [(Name, Kind)] -> Map Name Kind
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
          ([(Name, Kind)] -> Map Name Kind)
-> [(Name, Kind)] -> Map Name Kind
forall a b. (a -> b) -> a -> b
$ ((Maybe Name, (Kind, Kind)) -> Maybe (Name, Kind))
-> [(Maybe Name, (Kind, Kind))] -> [(Name, Kind)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe
            ( \(Maybe Name
newName, (Kind, Kind)
oldVar) ->
                case (Maybe Name
newName, (Kind, Kind)
oldVar) of
                  (Just Name
newName, (VarT Name
oldName, Kind
_)) ->
                    (Name, Kind) -> Maybe (Name, Kind)
forall a. a -> Maybe a
Just (Name
oldName, Name -> Kind
VarT Name
newName)
                  (Maybe Name, (Kind, Kind))
_ -> Maybe (Name, Kind)
forall a. Maybe a
Nothing
            )
          ([(Maybe Name, (Kind, Kind))] -> [(Name, Kind)])
-> [(Maybe Name, (Kind, Kind))] -> [(Name, Kind)]
forall a b. (a -> b) -> a -> b
$ [Maybe Name] -> [(Kind, Kind)] -> [(Maybe Name, (Kind, Kind))]
forall a b. [a] -> [b] -> [(a, b)]
zip
            ([Maybe Name]
keptNewNames [Maybe Name] -> [Maybe Name] -> [Maybe Name]
forall a. [a] -> [a] -> [a]
++ [Maybe Name]
argNewNames)
            (CheckArgsResult -> [(Kind, Kind)]
keptVars CheckArgsResult
result [(Kind, Kind)] -> [(Kind, Kind)] -> [(Kind, Kind)]
forall a. [a] -> [a] -> [a]
++ CheckArgsResult -> [(Kind, Kind)]
argVars CheckArgsResult
result)
  constructors <-
    mapM freshenConstructorInfo $
      applySubstitution substMap $
        constructors result
  let newKeptVars = (Kind -> Kind) -> (Kind, Kind) -> (Kind, Kind)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Map Name Kind -> Kind -> Kind
forall a. TypeSubstitution a => Map Name Kind -> a -> a
applySubstitution Map Name Kind
substMap) ((Kind, Kind) -> (Kind, Kind)) -> [(Kind, Kind)] -> [(Kind, Kind)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CheckArgsResult -> [(Kind, Kind)]
keptVars CheckArgsResult
result)
  let newArgVars = (Kind -> Kind) -> (Kind, Kind) -> (Kind, Kind)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Map Name Kind -> Kind -> Kind
forall a. TypeSubstitution a => Map Name Kind -> a -> a
applySubstitution Map Name Kind
substMap) ((Kind, Kind) -> (Kind, Kind)) -> [(Kind, Kind)] -> [(Kind, Kind)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CheckArgsResult -> [(Kind, Kind)]
argVars CheckArgsResult
result)
  return $
    result
      { constructors = constructors,
        keptVars = newKeptVars,
        argVars = newArgVars
      }

-- | Check if the number of type parameters is valid for a data type, and return
-- new names for the type variables, split into kept and arg parts.
checkArgs ::
  String ->
  Int ->
  Name ->
  Bool ->
  Int ->
  Q CheckArgsResult
checkArgs :: String -> Int -> Name -> Bool -> Int -> Q CheckArgsResult
checkArgs String
clsName Int
maxArgNum Name
typName Bool
allowExistential Int
n = do
  Bool -> Q () -> Q ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0) (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$
    String -> Q ()
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$
      [String] -> String
unlines
        [ String
"Cannot derive "
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
clsName
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" instance with negative type parameters",
          String
"\tRequested: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n,
          String
"\tHint: Use a non-negative number of type parameters"
        ]
  Bool -> Q () -> Q ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
maxArgNum) (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$
    String -> Q ()
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$
      [String] -> String
unlines
        [ String
"Cannot derive "
            String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
clsName
            String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" instance with more than "
            String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
maxArgNum
            String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" type parameters",
          String
"\tRequested: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
n
        ]
  d <- Name -> Q DatatypeInfo
reifyDatatype Name
typName
  let dvars = DatatypeInfo -> [TyVarBndrUnit]
datatypeVars DatatypeInfo
d
  when (length dvars < n) $
    fail $
      unlines
        [ "Cannot derive "
            <> clsName
            <> show n
            <> " instance for the type "
            <> show typName,
          "\tReason: The type "
            <> show typName
            <> " has only "
            <> show (length dvars)
            <> " type variables."
        ]
  let keptVars =
        (\TyVarBndrUnit
bndr -> (Name -> Kind
VarT (Name -> Kind) -> Name -> Kind
forall a b. (a -> b) -> a -> b
$ TyVarBndrUnit -> Name
forall flag. TyVarBndr_ flag -> Name
tvName TyVarBndrUnit
bndr, TyVarBndrUnit -> Kind
forall flag. TyVarBndr_ flag -> Kind
tvKind TyVarBndrUnit
bndr))
          (TyVarBndrUnit -> (Kind, Kind))
-> [TyVarBndrUnit] -> [(Kind, Kind)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> [TyVarBndrUnit] -> [TyVarBndrUnit]
forall a. Int -> [a] -> [a]
take ([TyVarBndrUnit] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TyVarBndrUnit]
dvars Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n) [TyVarBndrUnit]
dvars
  let argVars =
        (\TyVarBndrUnit
bndr -> (Name -> Kind
VarT (Name -> Kind) -> Name -> Kind
forall a b. (a -> b) -> a -> b
$ TyVarBndrUnit -> Name
forall flag. TyVarBndr_ flag -> Name
tvName TyVarBndrUnit
bndr, TyVarBndrUnit -> Kind
forall flag. TyVarBndr_ flag -> Kind
tvKind TyVarBndrUnit
bndr))
          (TyVarBndrUnit -> (Kind, Kind))
-> [TyVarBndrUnit] -> [(Kind, Kind)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> [TyVarBndrUnit] -> [TyVarBndrUnit]
forall a. Int -> [a] -> [a]
drop ([TyVarBndrUnit] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TyVarBndrUnit]
dvars Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n) [TyVarBndrUnit]
dvars
  let constructors = DatatypeInfo -> [ConstructorInfo]
datatypeCons DatatypeInfo
d
  unless allowExistential $
    mapM_
      ( \ConstructorInfo
c ->
          Bool -> Q () -> Q ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ConstructorInfo -> [TyVarBndrUnit]
constructorVars ConstructorInfo
c [TyVarBndrUnit] -> [TyVarBndrUnit] -> Bool
forall a. Eq a => a -> a -> Bool
/= []) (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$
            String -> Q ()
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$
              [String] -> String
unlines
                [ String
"Cannot derive "
                    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
clsName
                    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
n
                    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" instance for the type "
                    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Name -> String
forall a. Show a => a -> String
show Name
typName,
                  String
"\tReason: The constructor "
                    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Name -> String
nameBase (ConstructorInfo -> Name
constructorName ConstructorInfo
c)
                    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" has existential variables"
                ]
      )
      constructors
  mapM_
    ( \ConstructorInfo
c -> do
        let fields :: [Kind]
fields = ConstructorInfo -> [Kind]
constructorFields ConstructorInfo
c
        let existentialVars :: [Name]
existentialVars = TyVarBndrUnit -> Name
forall flag. TyVarBndr_ flag -> Name
tvName (TyVarBndrUnit -> Name) -> [TyVarBndrUnit] -> [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ConstructorInfo -> [TyVarBndrUnit]
constructorVars ConstructorInfo
c
        let fieldReferencedVars :: [Name]
fieldReferencedVars = [Kind] -> [Name]
forall a. TypeSubstitution a => a -> [Name]
freeVariables [Kind]
fields
        let notReferencedVars :: Set Name
notReferencedVars =
              [Name] -> Set Name
forall a. Ord a => [a] -> Set a
S.fromList [Name]
existentialVars Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
S.\\ [Name] -> Set Name
forall a. Ord a => [a] -> Set a
S.fromList [Name]
fieldReferencedVars
        Bool -> Q () -> Q ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set Name -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set Name
notReferencedVars) (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$
          String -> Q ()
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$
            [String] -> String
unlines
              [ String
"Cannot derive "
                  String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
clsName
                  String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
n
                  String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" instance for the type "
                  String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Name -> String
forall a. Show a => a -> String
show Name
typName,
                String
"Reason: Ambiguous existential variable in the constructor: "
                  String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Name -> String
nameBase (ConstructorInfo -> Name
constructorName ConstructorInfo
c)
                  String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
", this is not supported. Please consider binding the "
                  String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"existential variable to a field. You can use Proxy type to "
                  String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"do this."
              ]
    )
    constructors
  return $ CheckArgsResult {..}

isVarUsedInConstructorFields :: [ConstructorInfo] -> Name -> Bool
isVarUsedInConstructorFields :: [ConstructorInfo] -> Name -> Bool
isVarUsedInConstructorFields [ConstructorInfo]
constructors Name
var =
  let allFields :: [Kind]
allFields = (ConstructorInfo -> [Kind]) -> [ConstructorInfo] -> [Kind]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ConstructorInfo -> [Kind]
constructorFields [ConstructorInfo]
constructors
      allFieldsFreeVars :: Set Name
allFieldsFreeVars = [Name] -> Set Name
forall a. Ord a => [a] -> Set a
S.fromList ([Name] -> Set Name) -> [Name] -> Set Name
forall a b. (a -> b) -> a -> b
$ [Kind] -> [Name]
forall a. TypeSubstitution a => a -> [Name]
freeVariables [Kind]
allFields
   in Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member Name
var Set Name
allFieldsFreeVars

-- | Check if a variable is used in the fields of a constructor.
isVarUsedInFields :: CheckArgsResult -> Name -> Bool
isVarUsedInFields :: CheckArgsResult -> Name -> Bool
isVarUsedInFields CheckArgsResult {[(Kind, Kind)]
[ConstructorInfo]
constructors :: CheckArgsResult -> [ConstructorInfo]
keptVars :: CheckArgsResult -> [(Kind, Kind)]
argVars :: CheckArgsResult -> [(Kind, Kind)]
constructors :: [ConstructorInfo]
keptVars :: [(Kind, Kind)]
argVars :: [(Kind, Kind)]
..} =
  [ConstructorInfo] -> Name -> Bool
isVarUsedInConstructorFields [ConstructorInfo]
constructors

-- | Generate a context for a variable in a GADT.
ctxForVar :: [Type] -> Type -> Kind -> Q (Maybe Pred)
ctxForVar :: [Kind] -> Kind -> Kind -> Q (Maybe Kind)
ctxForVar [Kind]
instanceExps Kind
ty Kind
knd = case Kind
knd of
  Kind
StarT ->
    Kind -> Maybe Kind
forall a. a -> Maybe a
Just
      (Kind -> Maybe Kind) -> Q Kind -> Q (Maybe Kind)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [t|$(Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> Q Kind) -> Kind -> Q Kind
forall a b. (a -> b) -> a -> b
$ [Kind] -> Kind
forall a. HasCallStack => [a] -> a
head [Kind]
instanceExps) $(Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
ty)|]
  AppT (AppT Kind
ArrowT Kind
StarT) Kind
StarT ->
    Kind -> Maybe Kind
forall a. a -> Maybe a
Just
      (Kind -> Maybe Kind) -> Q Kind -> Q (Maybe Kind)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [t|$(Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> Q Kind) -> Kind -> Q Kind
forall a b. (a -> b) -> a -> b
$ [Kind]
instanceExps [Kind] -> Int -> Kind
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) $(Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
ty)|]
  AppT (AppT (AppT Kind
ArrowT Kind
StarT) Kind
StarT) Kind
StarT ->
    Kind -> Maybe Kind
forall a. a -> Maybe a
Just
      (Kind -> Maybe Kind) -> Q Kind -> Q (Maybe Kind)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [t|$(Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> Q Kind) -> Kind -> Q Kind
forall a b. (a -> b) -> a -> b
$ [Kind]
instanceExps [Kind] -> Int -> Kind
forall a. HasCallStack => [a] -> Int -> a
!! Int
2) $(Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
ty)|]
  AppT (AppT (AppT (AppT Kind
ArrowT Kind
StarT) Kind
StarT) Kind
StarT) Kind
StarT ->
    Kind -> Maybe Kind
forall a. a -> Maybe a
Just
      (Kind -> Maybe Kind) -> Q Kind -> Q (Maybe Kind)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [t|$(Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> Q Kind) -> Kind -> Q Kind
forall a b. (a -> b) -> a -> b
$ [Kind]
instanceExps [Kind] -> Int -> Kind
forall a. HasCallStack => [a] -> Int -> a
!! Int
3) $(Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
ty)|]
  AppT (AppT (AppT (AppT Kind
ArrowT Kind
StarT) Kind
StarT) Kind
StarT) Kind
_ ->
    String -> Q (Maybe Kind)
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Q (Maybe Kind)) -> String -> Q (Maybe Kind)
forall a b. (a -> b) -> a -> b
$ String
"Unsupported kind: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Kind -> String
forall a. Show a => a -> String
show Kind
knd
  Kind
_ -> Maybe Kind -> Q (Maybe Kind)
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Kind
forall a. Maybe a
Nothing

-- | Configuration for constraints for evaluation modes tag.
--
-- * 'EvalModeConstraints' specifies a list of constraints for the tag, for
--   example, we may use 'Grisette.Unified.EvalModeBase' and
--   'Grisette.Unified.EvalModeBV' to specify that the evaluation mode must
--   support both base (boolean and data types) and bit vectors. This should be
--   used when the data type uses bit vectors.
--
-- * 'EvalModeSpecified' specifies a that an evaluation mode tag should be
--   specialized to a specific tag for all the instances.
data EvalModeConfig
  = EvalModeConstraints [Name]
  | EvalModeSpecified EvalModeTag

-- | Configuration for deriving instances for a data type.
data DeriveConfig = DeriveConfig
  { DeriveConfig -> [(Int, EvalModeConfig)]
evalModeConfig :: [(Int, EvalModeConfig)],
    DeriveConfig -> [Int]
bitSizePositions :: [Int],
    DeriveConfig -> [(Int, Int)]
fpBitSizePositions :: [(Int, Int)],
    DeriveConfig -> [Int]
unconstrainedPositions :: [Int],
    DeriveConfig -> Bool
needExtraMergeableUnderEvalMode :: Bool,
    DeriveConfig -> Bool
needExtraMergeableWithConcretizedEvalMode :: Bool,
    DeriveConfig -> Bool
useNoStrategy :: Bool,
    DeriveConfig -> Bool
useSerialForCerealAndBinary :: Bool
  }

-- | Get all the evaluation modes to specialize in the t'DeriveConfig'.
evalModeSpecializeList :: DeriveConfig -> [(Int, EvalModeTag)]
evalModeSpecializeList :: DeriveConfig -> [(Int, EvalModeTag)]
evalModeSpecializeList DeriveConfig {Bool
[Int]
[(Int, Int)]
[(Int, EvalModeConfig)]
evalModeConfig :: DeriveConfig -> [(Int, EvalModeConfig)]
bitSizePositions :: DeriveConfig -> [Int]
fpBitSizePositions :: DeriveConfig -> [(Int, Int)]
unconstrainedPositions :: DeriveConfig -> [Int]
needExtraMergeableUnderEvalMode :: DeriveConfig -> Bool
needExtraMergeableWithConcretizedEvalMode :: DeriveConfig -> Bool
useNoStrategy :: DeriveConfig -> Bool
useSerialForCerealAndBinary :: DeriveConfig -> Bool
evalModeConfig :: [(Int, EvalModeConfig)]
bitSizePositions :: [Int]
fpBitSizePositions :: [(Int, Int)]
unconstrainedPositions :: [Int]
needExtraMergeableUnderEvalMode :: Bool
needExtraMergeableWithConcretizedEvalMode :: Bool
useNoStrategy :: Bool
useSerialForCerealAndBinary :: Bool
..} =
  ((Int, EvalModeConfig) -> Maybe (Int, EvalModeTag))
-> [(Int, EvalModeConfig)] -> [(Int, EvalModeTag)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe
    ( \(Int
n, EvalModeConfig
cfg) ->
        case EvalModeConfig
cfg of
          EvalModeConstraints [Name]
_ -> Maybe (Int, EvalModeTag)
forall a. Maybe a
Nothing
          EvalModeSpecified EvalModeTag
tag -> (Int, EvalModeTag) -> Maybe (Int, EvalModeTag)
forall a. a -> Maybe a
Just (Int
n, EvalModeTag
tag)
    )
    [(Int, EvalModeConfig)]
evalModeConfig

instance Semigroup DeriveConfig where
  DeriveConfig
l <> :: DeriveConfig -> DeriveConfig -> DeriveConfig
<> DeriveConfig
r =
    DeriveConfig
      { evalModeConfig :: [(Int, EvalModeConfig)]
evalModeConfig = DeriveConfig -> [(Int, EvalModeConfig)]
evalModeConfig DeriveConfig
l [(Int, EvalModeConfig)]
-> [(Int, EvalModeConfig)] -> [(Int, EvalModeConfig)]
forall a. Semigroup a => a -> a -> a
<> DeriveConfig -> [(Int, EvalModeConfig)]
evalModeConfig DeriveConfig
r,
        bitSizePositions :: [Int]
bitSizePositions = DeriveConfig -> [Int]
bitSizePositions DeriveConfig
l [Int] -> [Int] -> [Int]
forall a. Semigroup a => a -> a -> a
<> DeriveConfig -> [Int]
bitSizePositions DeriveConfig
r,
        fpBitSizePositions :: [(Int, Int)]
fpBitSizePositions = DeriveConfig -> [(Int, Int)]
fpBitSizePositions DeriveConfig
l [(Int, Int)] -> [(Int, Int)] -> [(Int, Int)]
forall a. Semigroup a => a -> a -> a
<> DeriveConfig -> [(Int, Int)]
fpBitSizePositions DeriveConfig
r,
        unconstrainedPositions :: [Int]
unconstrainedPositions = DeriveConfig -> [Int]
unconstrainedPositions DeriveConfig
l [Int] -> [Int] -> [Int]
forall a. Semigroup a => a -> a -> a
<> DeriveConfig -> [Int]
unconstrainedPositions DeriveConfig
r,
        needExtraMergeableUnderEvalMode :: Bool
needExtraMergeableUnderEvalMode =
          DeriveConfig -> Bool
needExtraMergeableUnderEvalMode DeriveConfig
l
            Bool -> Bool -> Bool
|| DeriveConfig -> Bool
needExtraMergeableUnderEvalMode DeriveConfig
r,
        needExtraMergeableWithConcretizedEvalMode :: Bool
needExtraMergeableWithConcretizedEvalMode =
          DeriveConfig -> Bool
needExtraMergeableWithConcretizedEvalMode DeriveConfig
l
            Bool -> Bool -> Bool
|| DeriveConfig -> Bool
needExtraMergeableWithConcretizedEvalMode DeriveConfig
r,
        useNoStrategy :: Bool
useNoStrategy = DeriveConfig -> Bool
useNoStrategy DeriveConfig
l Bool -> Bool -> Bool
|| DeriveConfig -> Bool
useNoStrategy DeriveConfig
r,
        useSerialForCerealAndBinary :: Bool
useSerialForCerealAndBinary =
          DeriveConfig -> Bool
useSerialForCerealAndBinary DeriveConfig
l Bool -> Bool -> Bool
&& DeriveConfig -> Bool
useSerialForCerealAndBinary DeriveConfig
r
      }

instance Monoid DeriveConfig where
  mempty :: DeriveConfig
mempty = [(Int, EvalModeConfig)]
-> [Int]
-> [(Int, Int)]
-> [Int]
-> Bool
-> Bool
-> Bool
-> Bool
-> DeriveConfig
DeriveConfig [] [] [] [] Bool
False Bool
False Bool
False Bool
True
  mappend :: DeriveConfig -> DeriveConfig -> DeriveConfig
mappend = DeriveConfig -> DeriveConfig -> DeriveConfig
forall a. Semigroup a => a -> a -> a
(<>)

-- | Generate extra constraints for evaluation modes.
extraEvalModeConstraint ::
  Name -> Name -> [(Type, Kind)] -> (Int, EvalModeConfig) -> Q [Pred]
extraEvalModeConstraint :: Name -> Name -> [(Kind, Kind)] -> (Int, EvalModeConfig) -> Q [Kind]
extraEvalModeConstraint
  Name
tyName
  Name
instanceName
  [(Kind, Kind)]
args
  (Int
n, EvalModeConstraints [Name]
names)
    | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [(Kind, Kind)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Kind, Kind)]
args = [Kind] -> Q [Kind]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    | Bool
otherwise = do
        let (Kind
arg, Kind
argKind) = [(Kind, Kind)]
args [(Kind, Kind)] -> Int -> (Kind, Kind)
forall a. HasCallStack => [a] -> Int -> a
!! Int
n
        Bool -> Q () -> Q ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Kind
argKind Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
/= Name -> Kind
ConT ''EvalModeTag) (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$
          String -> Q ()
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$
            String
"Cannot introduce EvalMode constraint for the "
              String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
n
              String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"th argument of "
              String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Name -> String
forall a. Show a => a -> String
show Name
tyName
              String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" when deriving the "
              String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Name -> String
forall a. Show a => a -> String
show Name
instanceName
              String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" instance because it is not an EvalModeTag."
        (Name -> Q Kind) -> [Name] -> Q [Kind]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (\Name
nm -> [t|$(Name -> Q Kind
forall (m :: * -> *). Quote m => Name -> m Kind
conT Name
nm) $(Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
arg)|]) [Name]
names
extraEvalModeConstraint Name
_ Name
_ [(Kind, Kind)]
_ (Int
_, EvalModeSpecified EvalModeTag
_) = [Kind] -> Q [Kind]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return []

-- | Generate extra constraints for bit vectors.
extraBitSizeConstraint :: Name -> Name -> [(Type, Kind)] -> Int -> Q [Pred]
extraBitSizeConstraint :: Name -> Name -> [(Kind, Kind)] -> Int -> Q [Kind]
extraBitSizeConstraint Name
tyName Name
instanceName [(Kind, Kind)]
args Int
n
  | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [(Kind, Kind)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Kind, Kind)]
args = [Kind] -> Q [Kind]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return []
  | Bool
otherwise = do
      let (Kind
arg, Kind
argKind) = [(Kind, Kind)]
args [(Kind, Kind)] -> Int -> (Kind, Kind)
forall a. HasCallStack => [a] -> Int -> a
!! Int
n
      Bool -> Q () -> Q ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Kind
argKind Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
/= Name -> Kind
ConT ''Nat) (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$
        String -> Q ()
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$
          String
"Cannot introduce BitSize constraint for the "
            String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
n
            String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"th argument of "
            String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Name -> String
forall a. Show a => a -> String
show Name
tyName
            String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" when deriving the "
            String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Name -> String
forall a. Show a => a -> String
show Name
instanceName
            String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" instance because it is not a Nat."
      predKnown <- [t|KnownNat $(Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
arg)|]
      predPositive <- [t|1 <= $(return arg)|]
      return [predKnown, predPositive]

-- | Generate extra constraints for floating point exponents and significands.
extraFpBitSizeConstraint ::
  Name -> Name -> [(Type, Kind)] -> (Int, Int) -> Q [Pred]
extraFpBitSizeConstraint :: Name -> Name -> [(Kind, Kind)] -> (Int, Int) -> Q [Kind]
extraFpBitSizeConstraint Name
tyName Name
instanceName [(Kind, Kind)]
args (Int
eb, Int
sb)
  | Int
eb Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [(Kind, Kind)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Kind, Kind)]
args Bool -> Bool -> Bool
|| Int
sb Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [(Kind, Kind)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Kind, Kind)]
args = [Kind] -> Q [Kind]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return []
  | Bool
otherwise = do
      let (Kind
argEb, Kind
argEbKind) = [(Kind, Kind)]
args [(Kind, Kind)] -> Int -> (Kind, Kind)
forall a. HasCallStack => [a] -> Int -> a
!! Int
eb
      let (Kind
argSb, Kind
argSbKind) = [(Kind, Kind)]
args [(Kind, Kind)] -> Int -> (Kind, Kind)
forall a. HasCallStack => [a] -> Int -> a
!! Int
sb
      Bool -> Q () -> Q ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Kind
argEbKind Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
/= Name -> Kind
ConT ''Nat Bool -> Bool -> Bool
|| Kind
argSbKind Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
/= Name -> Kind
ConT ''Nat) (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$
        String -> Q ()
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$
          String
"Cannot introduce ValidFP constraint for the "
            String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
eb
            String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"th and "
            String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
sb
            String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"th arguments of "
            String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Name -> String
forall a. Show a => a -> String
show Name
tyName
            String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" when deriving the "
            String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Name -> String
forall a. Show a => a -> String
show Name
instanceName
            String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" instance because they are not Nats."
      pred <- [t|ValidFP $(Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
argEb) $(Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
argSb)|]
      return [pred]

-- | Generate extra constraints for 'Mergeable' instances.
extraExtraMergeableConstraint ::
  DeriveConfig -> [ConstructorInfo] -> [(Type, Kind)] -> Q [Pred]
extraExtraMergeableConstraint :: DeriveConfig -> [ConstructorInfo] -> [(Kind, Kind)] -> Q [Kind]
extraExtraMergeableConstraint DeriveConfig
deriveConfig [ConstructorInfo]
constructors [(Kind, Kind)]
args = do
  let isTypeUsedInFields' :: Kind -> Bool
isTypeUsedInFields' (VarT Name
nm) =
        [ConstructorInfo] -> Name -> Bool
isVarUsedInConstructorFields [ConstructorInfo]
constructors Name
nm
      isTypeUsedInFields' Kind
_ = Bool
False
  [Maybe Kind] -> [Kind]
forall a. [Maybe a] -> [a]
catMaybes
    ([Maybe Kind] -> [Kind]) -> Q [Maybe Kind] -> Q [Kind]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> (Kind, Kind) -> Q (Maybe Kind))
-> [Int] -> [(Kind, Kind)] -> Q [Maybe Kind]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM
      ( \Int
position (Kind
arg, Kind
knd) ->
          if Kind -> Bool
isTypeUsedInFields' Kind
arg
            Bool -> Bool -> Bool
&& Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem Int
position (DeriveConfig -> [Int]
unconstrainedPositions DeriveConfig
deriveConfig)
            then
              [Kind] -> Kind -> Kind -> Q (Maybe Kind)
ctxForVar
                [ Name -> Kind
ConT ''Mergeable,
                  Name -> Kind
ConT ''Mergeable1,
                  Name -> Kind
ConT ''Mergeable2
                ]
                Kind
arg
                Kind
knd
            else Maybe Kind -> Q (Maybe Kind)
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Kind
forall a. Maybe a
Nothing
      )
      [Int
0 ..]
      [(Kind, Kind)]
args

-- | Generate extra constraints for a data type.
extraConstraint ::
  DeriveConfig ->
  Name ->
  Name ->
  [(Type, Kind)] ->
  [(Type, Kind)] ->
  [ConstructorInfo] ->
  Q [Pred]
extraConstraint :: DeriveConfig
-> Name
-> Name
-> [(Kind, Kind)]
-> [(Kind, Kind)]
-> [ConstructorInfo]
-> Q [Kind]
extraConstraint
  deriveConfig :: DeriveConfig
deriveConfig@DeriveConfig {Bool
[Int]
[(Int, Int)]
[(Int, EvalModeConfig)]
evalModeConfig :: DeriveConfig -> [(Int, EvalModeConfig)]
bitSizePositions :: DeriveConfig -> [Int]
fpBitSizePositions :: DeriveConfig -> [(Int, Int)]
unconstrainedPositions :: DeriveConfig -> [Int]
needExtraMergeableUnderEvalMode :: DeriveConfig -> Bool
needExtraMergeableWithConcretizedEvalMode :: DeriveConfig -> Bool
useNoStrategy :: DeriveConfig -> Bool
useSerialForCerealAndBinary :: DeriveConfig -> Bool
evalModeConfig :: [(Int, EvalModeConfig)]
bitSizePositions :: [Int]
fpBitSizePositions :: [(Int, Int)]
unconstrainedPositions :: [Int]
needExtraMergeableUnderEvalMode :: Bool
needExtraMergeableWithConcretizedEvalMode :: Bool
useNoStrategy :: Bool
useSerialForCerealAndBinary :: Bool
..}
  Name
tyName
  Name
instanceName
  [(Kind, Kind)]
extraArgs
  [(Kind, Kind)]
keptArgs
  [ConstructorInfo]
constructors = do
    evalModePreds <-
      ((Int, EvalModeConfig) -> Q [Kind])
-> [(Int, EvalModeConfig)] -> Q [[Kind]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse
        (Name -> Name -> [(Kind, Kind)] -> (Int, EvalModeConfig) -> Q [Kind]
extraEvalModeConstraint Name
tyName Name
instanceName [(Kind, Kind)]
keptArgs)
        [(Int, EvalModeConfig)]
evalModeConfig
    extraArgEvalModePreds <-
      if null evalModeConfig
        then
          traverse
            ( \(Kind
arg, Kind
kind) ->
                if Kind
kind Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Kind
ConT ''EvalModeTag
                  then (Kind -> [Kind] -> [Kind]
forall a. a -> [a] -> [a]
: []) (Kind -> [Kind]) -> Q Kind -> Q [Kind]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [t|DecideEvalMode $(Kind -> Q Kind
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
arg)|]
                  else [Kind] -> Q [Kind]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return []
            )
            extraArgs
        else return []
    bitSizePreds <-
      traverse
        (extraBitSizeConstraint tyName instanceName keptArgs)
        bitSizePositions
    fpBitSizePreds <-
      traverse
        (extraFpBitSizeConstraint tyName instanceName keptArgs)
        fpBitSizePositions
    extraMergeablePreds <-
      if needExtraMergeableUnderEvalMode
        && ( any
               ( \case
                   (Int
_, EvalModeConstraints [Name]
_) -> Bool
True
                   (Int
_, EvalModeSpecified EvalModeTag
_) -> Bool
False
               )
               evalModeConfig
               || needExtraMergeableWithConcretizedEvalMode
           )
        then extraExtraMergeableConstraint deriveConfig constructors keptArgs
        else return []
    return $
      concat (extraArgEvalModePreds ++ evalModePreds)
        ++ if null constructors
          then []
          else extraMergeablePreds ++ concat (bitSizePreds ++ fpBitSizePreds)