{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

{-# HLINT ignore "Eta reduce" #-}

-- |
-- Module      :   Grisette.Internal.Internal.Impl.Unified.Class.UnifiedITEOp
-- 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.Internal.Impl.Unified.Class.UnifiedITEOp
  ( symIte,
    symIteMerge,
  )
where

import Data.Kind (Constraint)
import Data.Type.Bool (If)
import Grisette.Internal.Core.Control.Monad.Union (Union)
import Grisette.Internal.Core.Data.Class.ITEOp (ITEOp)
import qualified Grisette.Internal.Core.Data.Class.ITEOp
import Grisette.Internal.Core.Data.Class.Mergeable (Mergeable)
import Grisette.Internal.Core.Data.Class.UnionView
  ( UnionView,
    pattern If,
    pattern Single,
  )
import qualified Grisette.Internal.Core.Data.Class.UnionView
import Grisette.Internal.Internal.Decl.Unified.Class.UnifiedITEOp
  ( UnifiedITEOp (withBaseITEOp),
  )
import Grisette.Internal.Unified.Class.UnionViewMode (UnionViewMode)
import Grisette.Internal.Unified.EvalModeTag (EvalModeTag (S), IsConMode)
import Grisette.Internal.Unified.UnifiedBool (UnifiedBool (GetBool))
import Grisette.Internal.Unified.Util (DecideEvalMode, withMode)

-- | Unified `Grisette.Internal.Core.Data.Class.ITEOp.symIte` operation.
--
-- This function isn't able to infer the mode of the boolean variable, so you
-- need to provide the mode explicitly. For example:
--
-- > symIte @mode (a .== b) ...
-- > symIte (a .== b :: SymBool) ...
-- > symIte (a .== b :: GetBool mode) ...
symIte ::
  forall mode v.
  (DecideEvalMode mode, UnifiedITEOp mode v) =>
  GetBool mode ->
  v ->
  v ->
  v
symIte :: forall (mode :: EvalModeTag) v.
(DecideEvalMode mode, UnifiedITEOp mode v) =>
GetBool mode -> v -> v -> v
symIte GetBool mode
c v
a v
b =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    (forall (mode :: EvalModeTag) v r.
UnifiedITEOp mode v =>
(If (IsConMode mode) (() :: Constraint) (ITEOp v) => r) -> r
withBaseITEOp @mode @v ((If (IsConMode mode) (() :: Constraint) (ITEOp v) => v) -> v)
-> (If (IsConMode mode) (() :: Constraint) (ITEOp v) => v) -> v
forall a b. (a -> b) -> a -> b
$ if Bool
GetBool mode
c then v
a else v
b)
    ( forall (mode :: EvalModeTag) v r.
UnifiedITEOp mode v =>
(If (IsConMode mode) (() :: Constraint) (ITEOp v) => r) -> r
withBaseITEOp @mode @v ((If (IsConMode mode) (() :: Constraint) (ITEOp v) => v) -> v)
-> (If (IsConMode mode) (() :: Constraint) (ITEOp v) => v) -> v
forall a b. (a -> b) -> a -> b
$
        SymBool -> v -> v -> v
forall v. ITEOp v => SymBool -> v -> v -> v
Grisette.Internal.Core.Data.Class.ITEOp.symIte SymBool
GetBool mode
c v
a v
b
    )

-- | Unified `Grisette.Internal.Core.Data.Class.PlainUnion.symIteMerge`
-- operation.
--
-- This function isn't able to infer the mode of the base monad from the result,
-- so you need to provide the mode explicitly. For example:
--
-- > symIteMerge @mode ...
-- > symIteMerge (... :: GetData mode v) ...
symIteMerge ::
  forall mode u v.
  ( DecideEvalMode mode,
    UnifiedITEOp mode v,
    Mergeable v,
    UnionViewMode mode u,
    UnionView u
  ) =>
  u v ->
  v
symIteMerge :: forall (mode :: EvalModeTag) (u :: * -> *) v.
(DecideEvalMode mode, UnifiedITEOp mode v, Mergeable v,
 UnionViewMode mode u, UnionView u) =>
u v -> v
symIteMerge u v
m =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    ( forall (mode :: EvalModeTag) v r.
UnifiedITEOp mode v =>
(If (IsConMode mode) (() :: Constraint) (ITEOp v) => r) -> r
withBaseITEOp @mode @v ((If (IsConMode mode) (() :: Constraint) (ITEOp v) => v) -> v)
-> (If (IsConMode mode) (() :: Constraint) (ITEOp v) => v) -> v
forall a b. (a -> b) -> a -> b
$ case u v
m of
        Single v
x -> v
x
        If {} ->
          [Char] -> v
forall a. HasCallStack => [Char] -> a
error [Char]
"symIteMerge: If case should not happen under concrete mode"
    )
    ( forall (mode :: EvalModeTag) v r.
UnifiedITEOp mode v =>
(If (IsConMode mode) (() :: Constraint) (ITEOp v) => r) -> r
withBaseITEOp @mode @v ((If (IsConMode mode) (() :: Constraint) (ITEOp v) => v) -> v)
-> (If (IsConMode mode) (() :: Constraint) (ITEOp v) => v) -> v
forall a b. (a -> b) -> a -> b
$
        u v -> v
forall a (u :: * -> *).
(ITEOp a, Mergeable a, UnionView u) =>
u a -> a
Grisette.Internal.Core.Data.Class.UnionView.symIteMerge u v
m
    )

instance
  {-# INCOHERENT #-}
  ( DecideEvalMode mode,
    If (IsConMode mode) (() :: Constraint) (ITEOp a)
  ) =>
  UnifiedITEOp mode a
  where
  withBaseITEOp :: forall r.
(If (IsConMode mode) (() :: Constraint) (ITEOp a) => r) -> r
withBaseITEOp If (IsConMode mode) (() :: Constraint) (ITEOp a) => r
r = forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode r
(mode ~ 'C) => r
If (IsConMode mode) (() :: Constraint) (ITEOp a) => r
r r
(mode ~ 'S) => r
If (IsConMode mode) (() :: Constraint) (ITEOp a) => r
r
  {-# INLINE withBaseITEOp #-}

instance (UnifiedITEOp 'S v, Mergeable v) => UnifiedITEOp 'S (Union v) where
  withBaseITEOp :: forall r.
(If (IsConMode 'S) (() :: Constraint) (ITEOp (Union v)) => r) -> r
withBaseITEOp If (IsConMode 'S) (() :: Constraint) (ITEOp (Union v)) => r
r = forall (mode :: EvalModeTag) v r.
UnifiedITEOp mode v =>
(If (IsConMode mode) (() :: Constraint) (ITEOp v) => r) -> r
withBaseITEOp @'S @v r
If (IsConMode 'S) (() :: Constraint) (ITEOp v) => r
If (IsConMode 'S) (() :: Constraint) (ITEOp (Union v)) => r
r
  {-# INLINE withBaseITEOp #-}