{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# HLINT ignore "Unused LANGUAGE pragma" #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

-- |
-- 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.Class.AsKey (AsKey (AsKey), AsKey1 (AsKey1))
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.
  --
  -- In the examples, we use 'AsKey' to check if two symbolic constants are the
  -- same term, concretely.
  --
  -- >>> sym "a" :: SymBool
  -- a
  -- >>> AsKey (sym "a" :: SymBool) == AsKey (sym "a" :: SymBool)
  -- True
  -- >>> AsKey (sym "a" :: SymBool) == AsKey (sym "b")
  -- False
  -- >>> (sym "a" :: SymBool) .&& sym "a"
  -- a
  -- >>> AsKey (sym "a" :: SymBool) == AsKey (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.
  --
  -- In the examples, we use 'AsKey' to check if two symbolic constants are the
  -- same term, concretely.
  --
  -- >>> ssym "a" :: SymBool
  -- a
  -- >>> AsKey (ssym "a" :: SymBool) == AsKey (ssym "a" :: SymBool)
  -- True
  -- >>> AsKey (ssym "a" :: SymBool) == AsKey (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.
--
-- In the examples, we use 'AsKey' to check if two symbolic constants are the
-- same term, concretely.
--
-- >>> AsKey ($$(slocsym "a") :: SymBool) == AsKey ($$(slocsym "a") :: SymBool)
-- False
-- >>> let f _ = $$(slocsym "a") :: SymBool
-- >>> AsKey (f ()) == AsKey (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||]

instance (Solvable c s) => Solvable c (AsKey s) where
  con :: c -> AsKey s
con = s -> AsKey s
forall a. a -> AsKey a
AsKey (s -> AsKey s) -> (c -> s) -> c -> AsKey s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> s
forall c t. Solvable c t => c -> t
con
  conView :: AsKey s -> Maybe c
conView (AsKey s
s) = s -> Maybe c
forall c t. Solvable c t => t -> Maybe c
conView s
s
  sym :: Symbol -> AsKey s
sym = s -> AsKey s
forall a. a -> AsKey a
AsKey (s -> AsKey s) -> (Symbol -> s) -> Symbol -> AsKey s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> s
forall c t. Solvable c t => Symbol -> t
sym
  ssym :: Identifier -> AsKey s
ssym = s -> AsKey s
forall a. a -> AsKey a
AsKey (s -> AsKey s) -> (Identifier -> s) -> Identifier -> AsKey s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identifier -> s
forall c t. Solvable c t => Identifier -> t
ssym
  isym :: Identifier -> Int -> AsKey s
isym Identifier
ident = s -> AsKey s
forall a. a -> AsKey a
AsKey (s -> AsKey s) -> (Int -> s) -> Int -> AsKey s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identifier -> Int -> s
forall c t. Solvable c t => Identifier -> Int -> t
isym Identifier
ident

instance (Solvable c (f s)) => Solvable c (AsKey1 f s) where
  con :: c -> AsKey1 f s
con = f s -> AsKey1 f s
forall (f :: * -> *) a. f a -> AsKey1 f a
AsKey1 (f s -> AsKey1 f s) -> (c -> f s) -> c -> AsKey1 f s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> f s
forall c t. Solvable c t => c -> t
con
  conView :: AsKey1 f s -> Maybe c
conView (AsKey1 f s
s) = f s -> Maybe c
forall c t. Solvable c t => t -> Maybe c
conView f s
s
  sym :: Symbol -> AsKey1 f s
sym = f s -> AsKey1 f s
forall (f :: * -> *) a. f a -> AsKey1 f a
AsKey1 (f s -> AsKey1 f s) -> (Symbol -> f s) -> Symbol -> AsKey1 f s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> f s
forall c t. Solvable c t => Symbol -> t
sym
  ssym :: Identifier -> AsKey1 f s
ssym = f s -> AsKey1 f s
forall (f :: * -> *) a. f a -> AsKey1 f a
AsKey1 (f s -> AsKey1 f s)
-> (Identifier -> f s) -> Identifier -> AsKey1 f s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identifier -> f s
forall c t. Solvable c t => Identifier -> t
ssym
  isym :: Identifier -> Int -> AsKey1 f s
isym Identifier
ident = f s -> AsKey1 f s
forall (f :: * -> *) a. f a -> AsKey1 f a
AsKey1 (f s -> AsKey1 f s) -> (Int -> f s) -> Int -> AsKey1 f s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identifier -> Int -> f s
forall c t. Solvable c t => Identifier -> Int -> t
isym Identifier
ident