{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

-- |
-- Module      :   Grisette.Unified.Internal.Util
-- 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.Util (withMode) where

import Data.Typeable (Typeable, eqT, type (:~:) (Refl))
import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (C, S))

-- | Case analysis on the mode.
withMode ::
  forall mode r.
  (Typeable mode) =>
  ((mode ~ 'C) => r) ->
  ((mode ~ 'S) => r) ->
  r
withMode :: forall (mode :: EvalModeTag) r.
Typeable mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode (mode ~ 'C) => r
con (mode ~ 'S) => r
sym = case (forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall (a :: EvalModeTag) (b :: EvalModeTag).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @mode @'C, forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall (a :: EvalModeTag) (b :: EvalModeTag).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @mode @'S) of
  (Just mode :~: 'C
Refl, Maybe (mode :~: 'S)
_) -> r
(mode ~ 'C) => r
con
  (Maybe (mode :~: 'C)
_, Just mode :~: 'S
Refl) -> r
(mode ~ 'S) => r
sym
  (Maybe (mode :~: 'C), Maybe (mode :~: 'S))
_ -> [Char] -> r
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible"
{-# INLINE withMode #-}