{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilyDependencies #-}

-- |
-- Module      :   Grisette.Internal.Unified.EvalModeTag
-- 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.Unified.EvalModeTag
  ( EvalModeTag (..),
    IsConMode,
  )
where

import Language.Haskell.TH.Syntax (Lift)

-- | Evaluation mode for unified types. 'C' means concrete evaluation, 'S'
-- means symbolic evaluation.
data EvalModeTag = C | S deriving ((forall (m :: * -> *). Quote m => EvalModeTag -> m Exp)
-> (forall (m :: * -> *).
    Quote m =>
    EvalModeTag -> Code m EvalModeTag)
-> Lift EvalModeTag
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => EvalModeTag -> m Exp
forall (m :: * -> *). Quote m => EvalModeTag -> Code m EvalModeTag
$clift :: forall (m :: * -> *). Quote m => EvalModeTag -> m Exp
lift :: forall (m :: * -> *). Quote m => EvalModeTag -> m Exp
$cliftTyped :: forall (m :: * -> *). Quote m => EvalModeTag -> Code m EvalModeTag
liftTyped :: forall (m :: * -> *). Quote m => EvalModeTag -> Code m EvalModeTag
Lift, Int -> EvalModeTag -> ShowS
[EvalModeTag] -> ShowS
EvalModeTag -> String
(Int -> EvalModeTag -> ShowS)
-> (EvalModeTag -> String)
-> ([EvalModeTag] -> ShowS)
-> Show EvalModeTag
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> EvalModeTag -> ShowS
showsPrec :: Int -> EvalModeTag -> ShowS
$cshow :: EvalModeTag -> String
show :: EvalModeTag -> String
$cshowList :: [EvalModeTag] -> ShowS
showList :: [EvalModeTag] -> ShowS
Show, EvalModeTag -> EvalModeTag -> Bool
(EvalModeTag -> EvalModeTag -> Bool)
-> (EvalModeTag -> EvalModeTag -> Bool) -> Eq EvalModeTag
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: EvalModeTag -> EvalModeTag -> Bool
== :: EvalModeTag -> EvalModeTag -> Bool
$c/= :: EvalModeTag -> EvalModeTag -> Bool
/= :: EvalModeTag -> EvalModeTag -> Bool
Eq)

-- | Type family to check if a mode is 'C'.
type family IsConMode (mode :: EvalModeTag) = (r :: Bool) | r -> mode where
  IsConMode 'C = 'True
  IsConMode 'S = 'False