Solvable.hs

{-# 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 = sym . 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 nm idx = sym $ IndexedSymbol nm 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 Con c <-
  (conView -> Just c)
  where
    Con c = con 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 nm = [||ssym $$(withLocation 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 nm idx = [||isym $$(withLocation nm) idx||]

instance (Solvable c s) => Solvable c (AsKey s) where
  con = AsKey . con
  conView (AsKey s) = conView s
  sym = AsKey . sym
  ssym = AsKey . ssym
  isym ident = AsKey . isym ident

instance (Solvable c (f s)) => Solvable c (AsKey1 f s) where
  con = AsKey1 . con
  conView (AsKey1 s) = conView s
  sym = AsKey1 . sym
  ssym = AsKey1 . ssym
  isym ident = AsKey1 . isym ident