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

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

import Language.Haskell.TH.Syntax (Lift)

-- | Evaluation mode for unified types. 'Con' means concrete evaluation, 'Sym'
-- means symbolic evaluation.
data EvalModeTag = Con | Sym 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)

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