UnifiedSolvable.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}

-- |
-- Module      :   Grisette.Internal.Unified.Class.UnifiedSolvable
-- 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.Class.UnifiedSolvable
  ( UnifiedSolvable (withBaseSolvable),
    con,
    pattern Con,
    conView,
  )
where

import Data.Type.Bool (If)
import GHC.TypeLits (KnownNat, type (<=))
import Grisette.Internal.Core.Data.Class.Solvable (Solvable)
import qualified Grisette.Internal.Core.Data.Class.Solvable as Grisette
import Grisette.Internal.SymPrim.AlgReal (AlgReal)
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.FP (FP, ValidFP)
import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal)
import Grisette.Internal.SymPrim.SymBV (SymIntN, SymWordN)
import Grisette.Internal.SymPrim.SymBool (SymBool)
import Grisette.Internal.SymPrim.SymFP (SymFP)
import Grisette.Internal.SymPrim.SymInteger (SymInteger)
import Grisette.Internal.Unified.EvalModeTag (EvalModeTag (C, S), IsConMode)
import Grisette.Internal.Unified.Util (DecideEvalMode, withMode)

-- $setup
-- >>> import Grisette.Core (ssym)

-- | Wrap a concrete value in a symbolic value.
--
-- >>> con True :: Bool
-- True
--
-- >>> con True :: SymBool
-- true
con ::
  forall mode a con. (DecideEvalMode mode, UnifiedSolvable mode a con) => con -> a
con v =
  withMode @mode
    (withBaseSolvable @mode @a @con v)
    (withBaseSolvable @mode @a @con $ Grisette.con v)

-- | Extract the concrete value from a symbolic value.
--
-- >>> conView (con True :: SymBool)
-- Just True
--
-- >>> conView (ssym "a" :: SymBool)
-- Nothing
--
-- >>> conView True
-- Just True
conView ::
  forall mode a con.
  (DecideEvalMode mode, UnifiedSolvable mode a con) =>
  a ->
  Maybe con
conView v =
  withMode @mode
    (withBaseSolvable @mode @a @con $ Just v)
    (withBaseSolvable @mode @a @con $ Grisette.conView v)

-- | A pattern synonym for extracting the concrete value from a symbolic value.
--
-- >>> case con True :: SymBool of Con v -> v
-- True
--
-- >>> case ssym "a" :: SymBool of Con v -> Just v; _ -> Nothing
-- Nothing
pattern Con :: (DecideEvalMode mode, UnifiedSolvable mode a con) => con -> a
pattern Con v <-
  (conView -> Just v)
  where
    Con v = con v

-- | A class that provides the ability to extract/wrap the concrete value
-- from/into a symbolic value.
class UnifiedSolvable mode a con | a -> mode con, con mode -> a where
  withBaseSolvable ::
    ((If (IsConMode mode) (a ~ con) (Solvable con a)) => r) -> r

instance UnifiedSolvable 'C Bool Bool where
  withBaseSolvable r = r

instance UnifiedSolvable 'S SymBool Bool where
  withBaseSolvable r = r

instance UnifiedSolvable 'C Integer Integer where
  withBaseSolvable r = r

instance UnifiedSolvable 'S SymInteger Integer where
  withBaseSolvable r = r

instance UnifiedSolvable 'C AlgReal AlgReal where
  withBaseSolvable r = r

instance UnifiedSolvable 'S SymAlgReal AlgReal where
  withBaseSolvable r = r

instance (KnownNat n, 1 <= n) => UnifiedSolvable 'C (WordN n) (WordN n) where
  withBaseSolvable r = r

instance (KnownNat n, 1 <= n) => UnifiedSolvable 'S (SymWordN n) (WordN n) where
  withBaseSolvable r = r

instance (KnownNat n, 1 <= n) => UnifiedSolvable 'C (IntN n) (IntN n) where
  withBaseSolvable r = r

instance (KnownNat n, 1 <= n) => UnifiedSolvable 'S (SymIntN n) (IntN n) where
  withBaseSolvable r = r

instance (ValidFP eb sb) => UnifiedSolvable 'C (FP eb sb) (FP eb sb) where
  withBaseSolvable r = r

instance (ValidFP eb sb) => UnifiedSolvable 'S (SymFP eb sb) (FP eb sb) where
  withBaseSolvable r = r