{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

{-# HLINT ignore "Unused LANGUAGE pragma" #-}

-- |
-- Module      :   Grisette.Internal.Core.Data.Class.Solvable
-- Copyright   :   (c) Sirui Lu 2021-2023
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.Core.Data.Class.Solvable
  ( -- * Solvable type interface
    Solvable (..),
    pattern Con,
    slocsym,
    ilocsym,
  )
where

import Data.String (IsString)
import qualified Data.Text as T
import Grisette.Internal.Core.Data.Symbol
  ( Identifier,
    Symbol (IndexedSymbol, SimpleSymbol),
    withLocation,
  )
import Language.Haskell.TH.Syntax.Compat (SpliceQ)

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.SymPrim

-- | The class defines the creation and pattern matching of solvable type
-- values.
class (IsString t) => Solvable c t | t -> c where
  -- | Wrap a concrete value in a symbolic value.
  --
  -- >>> con True :: SymBool
  -- true
  con :: c -> t

  -- | Extract the concrete value from a symbolic value.
  --
  -- >>> conView (con True :: SymBool)
  -- Just True
  --
  -- >>> conView (ssym "a" :: SymBool)
  -- Nothing
  conView :: t -> Maybe c

  -- | Generate symbolic constants.
  --
  -- Two symbolic constants with the same symbol are the same symbolic constant,
  -- and will always be assigned with the same value by the solver.
  --
  -- >>> sym "a" :: SymBool
  -- a
  -- >>> (sym "a" :: SymBool) == sym "a"
  -- True
  -- >>> (sym "a" :: SymBool) == sym "b"
  -- False
  -- >>> (sym "a" :: SymBool) .&& sym "a"
  -- a
  -- >>> (sym "a" :: SymBool) == isym "a" 1
  -- False
  sym :: Symbol -> t

  -- | Generate simply-named symbolic constants.
  --
  -- Two symbolic constants with the same identifier are the same symbolic
  -- constant, and will always be assigned with the same value by the solver.
  --
  -- >>> ssym "a" :: SymBool
  -- a
  -- >>> (ssym "a" :: SymBool) == ssym "a"
  -- True
  -- >>> (ssym "a" :: SymBool) == ssym "b"
  -- False
  -- >>> (ssym "a" :: SymBool) .&& ssym "a"
  -- a
  ssym :: Identifier -> t
  ssym = Symbol -> t
forall c t. Solvable c t => Symbol -> t
sym (Symbol -> t) -> (Identifier -> Symbol) -> Identifier -> t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identifier -> Symbol
SimpleSymbol

  -- | Generate indexed symbolic constants.
  --
  -- Two symbolic constants with the same identifier but different indices are
  -- not the same symbolic constants.
  --
  -- >>> isym "a" 1 :: SymBool
  -- a@1
  isym :: Identifier -> Int -> t
  isym Identifier
nm Int
idx = Symbol -> t
forall c t. Solvable c t => Symbol -> t
sym (Symbol -> t) -> Symbol -> t
forall a b. (a -> b) -> a -> b
$ Identifier -> Int -> Symbol
IndexedSymbol Identifier
nm Int
idx

-- | Extract the concrete value from a solvable value with 'conView'.
--
-- >>> case con True :: SymBool of Con v -> v
-- True
pattern Con :: (Solvable c t) => c -> t
pattern $mCon :: forall {r} {c} {t}.
Solvable c t =>
t -> (c -> r) -> ((# #) -> r) -> r
$bCon :: forall c t. Solvable c t => c -> t
Con c <-
  (conView -> Just c)
  where
    Con c
c = c -> t
forall c t. Solvable c t => c -> t
con c
c

-- | Generate simply-named symbolic variables. The file location will be
-- attached to the identifier.
--
-- >>> $$(slocsym "a") :: SymBool
-- a:[grisette-file-location <interactive>...]
--
-- Calling 'slocsym' with the same name at different location will always
-- generate different symbolic constants. Calling 'slocsym' at the same
-- location for multiple times will generate the same symbolic constants.
--
-- >>> ($$(slocsym "a") :: SymBool) == $$(slocsym "a")
-- False
-- >>> let f _ = $$(slocsym "a") :: SymBool
-- >>> f () == f ()
-- True
slocsym :: (Solvable c s) => T.Text -> SpliceQ s
slocsym :: forall c s. Solvable c s => Text -> SpliceQ s
slocsym Text
nm = [||Identifier -> t
forall c t. Solvable c t => Identifier -> t
ssym $$(Text -> SpliceQ Identifier
withLocation Text
nm)||]

-- | Generate indexed symbolic variables. The file location will be attached to
-- the identifier.
--
-- >>> $$(ilocsym "a" 1) :: SymBool
-- a:[grisette-file-location <interactive>...]@1
--
-- Calling 'ilocsym' with the same name and index at different location will
-- always generate different symbolic constants. Calling 'slocsym' at the same
-- location for multiple times will generate the same symbolic constants.
ilocsym :: (Solvable c s) => T.Text -> Int -> SpliceQ s
ilocsym :: forall c s. Solvable c s => Text -> Int -> SpliceQ s
ilocsym Text
nm Int
idx = [||Identifier -> Int -> t
forall c t. Solvable c t => Identifier -> Int -> t
isym $$(Text -> SpliceQ Identifier
withLocation Text
nm) Int
idx||]