-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Client
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Cross-cutting toplevel client functions
-----------------------------------------------------------------------------

{-# LANGUAGE CPP                 #-}
{-# LANGUAGE PackageImports      #-}
{-# LANGUAGE QuasiQuotes         #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE TemplateHaskell     #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Client
  ( sbvCheckSolverInstallation
  , defaultSolverConfig
  , getAvailableSolvers
  , mkSymbolicEnumeration
  , mkUninterpretedSort
  ) where

import Control.Monad (filterM)
import Data.Generics

import qualified Control.Exception as C

import qualified "template-haskell" Language.Haskell.TH        as TH
#if MIN_VERSION_template_haskell(2,18,0)
import qualified "template-haskell" Language.Haskell.TH.Syntax as TH
#endif

import Data.SBV.Core.Data
import Data.SBV.Core.Model
import Data.SBV.Provers.Prover

-- | Check whether the given solver is installed and is ready to go. This call does a
-- simple call to the solver to ensure all is well.
sbvCheckSolverInstallation :: SMTConfig -> IO Bool
sbvCheckSolverInstallation :: SMTConfig -> IO Bool
sbvCheckSolverInstallation SMTConfig
cfg = IO Bool
check forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`C.catch` (\(SomeException
_ :: C.SomeException) -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)
  where check :: IO Bool
check = do ThmResult SMTResult
r <- forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m ThmResult
proveWith SMTConfig
cfg forall a b. (a -> b) -> a -> b
$ \SBool
x -> SBool -> SBool
sNot (SBool -> SBool
sNot SBool
x) forall a. EqSymbolic a => a -> a -> SBool
.== (SBool
x :: SBool)
                   case SMTResult
r of
                     Unsatisfiable{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                     SMTResult
_               -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

-- | The default configs corresponding to supported SMT solvers
defaultSolverConfig :: Solver -> SMTConfig
defaultSolverConfig :: Solver -> SMTConfig
defaultSolverConfig Solver
ABC       = SMTConfig
abc
defaultSolverConfig Solver
Boolector = SMTConfig
boolector
defaultSolverConfig Solver
Bitwuzla  = SMTConfig
bitwuzla
defaultSolverConfig Solver
CVC4      = SMTConfig
cvc4
defaultSolverConfig Solver
CVC5      = SMTConfig
cvc5
defaultSolverConfig Solver
DReal     = SMTConfig
dReal
defaultSolverConfig Solver
MathSAT   = SMTConfig
mathSAT
defaultSolverConfig Solver
Yices     = SMTConfig
yices
defaultSolverConfig Solver
Z3        = SMTConfig
z3

-- | Return the known available solver configs, installed on your machine.
getAvailableSolvers :: IO [SMTConfig]
getAvailableSolvers :: IO [SMTConfig]
getAvailableSolvers = forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM SMTConfig -> IO Bool
sbvCheckSolverInstallation (forall a b. (a -> b) -> [a] -> [b]
map Solver -> SMTConfig
defaultSolverConfig [forall a. Bounded a => a
minBound .. forall a. Bounded a => a
maxBound])

-- | Turn a name into a symbolic type. If first argument is true, we'll also derive Eq and Ord instances.
declareSymbolic :: Bool -> TH.Name -> TH.Q [TH.Dec]
declareSymbolic :: Bool -> Name -> Q [Dec]
declareSymbolic Bool
isEnum Name
typeName = do
    let typeCon :: Q Type
typeCon = forall (m :: * -> *). Quote m => Name -> m Type
TH.conT Name
typeName

    [Name]
cstrs <- if Bool
isEnum then Name -> Q [Name]
ensureEnumeration Name
typeName
                       else Name -> Q [Name]
ensureEmptyData   Name
typeName

    [Dec]
deriveEqOrds <- if Bool
isEnum
                       then [d| deriving instance Eq       $typeCon
                                deriving instance Ord      $typeCon
                            |]
                       else forall (f :: * -> *) a. Applicative f => a -> f a
pure []

    [Dec]
derives <- [d| deriving instance Show     $typeCon
                   deriving instance Read     $typeCon
                   deriving instance Data     $typeCon
                   deriving instance SymVal   $typeCon
                   deriving instance HasKind  $typeCon
                   deriving instance SatModel $typeCon
               |]


    Type
sType <- forall (m :: * -> *). Quote m => Name -> m Type
TH.conT ''SBV forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
`TH.appT` Q Type
typeCon

    let declConstructor :: Name -> ((Name, String), [Dec])
declConstructor Name
c = ((Name
nm, String
bnm), [Dec
sig, Dec
def])
          where bnm :: String
bnm  = Name -> String
TH.nameBase Name
c
                nm :: Name
nm   = String -> Name
TH.mkName forall a b. (a -> b) -> a -> b
$ Char
's' forall a. a -> [a] -> [a]
: String
bnm
                def :: Dec
def  = Name -> [Clause] -> Dec
TH.FunD Name
nm [[Pat] -> Body -> [Dec] -> Clause
TH.Clause [] (Exp -> Body
TH.NormalB Exp
body) []]
                body :: Exp
body = Exp -> Exp -> Exp
TH.AppE (Name -> Exp
TH.VarE 'literal) (Name -> Exp
TH.ConE Name
c)
                sig :: Dec
sig  = Name -> Type -> Dec
TH.SigD Name
nm Type
sType

        ([(Name, String)]
constrNames, [[Dec]]
cdecls) = forall a b. [(a, b)] -> ([a], [b])
unzip (forall a b. (a -> b) -> [a] -> [b]
map Name -> ((Name, String), [Dec])
declConstructor [Name]
cstrs)

    let btname :: String
btname = Name -> String
TH.nameBase Name
typeName
        tname :: Name
tname  = String -> Name
TH.mkName (Char
'S' forall a. a -> [a] -> [a]
: String
btname)
        tdecl :: Dec
tdecl  = Name -> [TyVarBndr ()] -> Type -> Dec
TH.TySynD Name
tname [] Type
sType

    (Name, String) -> [(Name, String)] -> Q ()
addDocs (Name
tname, String
btname) [(Name, String)]
constrNames

    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ [Dec]
deriveEqOrds forall a. [a] -> [a] -> [a]
++ [Dec]
derives forall a. [a] -> [a] -> [a]
++ [Dec
tdecl] forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Dec]]
cdecls

 where addDocs :: (TH.Name, String) -> [(TH.Name, String)] -> TH.Q ()
#if MIN_VERSION_template_haskell(2,18,0)
       addDocs :: (Name, String) -> [(Name, String)] -> Q ()
addDocs (Name
tnm, String
ts) [(Name, String)]
cnms = do Bool -> (Name, String) -> Q ()
addDoc Bool
True (Name
tnm, String
ts)
                                   forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_  (Bool -> (Name, String) -> Q ()
addDoc Bool
False) [(Name, String)]
cnms
          where addDoc :: Bool -> (Name, String) -> Q ()
addDoc Bool
True  (Name
cnm, String
cs) = Q () -> Q ()
TH.addModFinalizer forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
TH.putDoc (Name -> DocLoc
TH.DeclDoc Name
cnm) forall a b. (a -> b) -> a -> b
$ String
"Symbolic version of the type '"        forall a. [a] -> [a] -> [a]
++ String
cs forall a. [a] -> [a] -> [a]
++ String
"'."
                addDoc Bool
False (Name
cnm, String
cs) = Q () -> Q ()
TH.addModFinalizer forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
TH.putDoc (Name -> DocLoc
TH.DeclDoc Name
cnm) forall a b. (a -> b) -> a -> b
$ String
"Symbolic version of the constructor '" forall a. [a] -> [a] -> [a]
++ String
cs forall a. [a] -> [a] -> [a]
++ String
"'."
#else
       addDocs _ _ = pure ()
#endif

-- | Make an enumeration a symbolic type.
mkSymbolicEnumeration :: TH.Name -> TH.Q [TH.Dec]
mkSymbolicEnumeration :: Name -> Q [Dec]
mkSymbolicEnumeration = Bool -> Name -> Q [Dec]
declareSymbolic Bool
True

-- | Make an uninterpred sort.
mkUninterpretedSort :: TH.Name -> TH.Q [TH.Dec]
mkUninterpretedSort :: Name -> Q [Dec]
mkUninterpretedSort = Bool -> Name -> Q [Dec]
declareSymbolic Bool
False

-- | Make sure the given type is an enumeration
ensureEnumeration :: TH.Name -> TH.Q [TH.Name]
ensureEnumeration :: Name -> Q [Name]
ensureEnumeration Name
nm = do
        Info
c <- Name -> Q Info
TH.reify Name
nm
        case Info
c of
          TH.TyConI Dec
d -> case Dec
d of
                           TH.DataD Cxt
_ Name
_ [TyVarBndr ()]
_ Maybe Type
_ [Con]
cons [DerivClause]
_ -> case [Con]
cons of
                                                        [] -> forall {a}. String -> Q [a]
bad String
"The datatype given has no constructors."
                                                        [Con]
xs -> forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Con -> Q [Name]
check [Con]
xs
                           Dec
_                       -> forall {a}. String -> Q [a]
bad String
"The name given is not a datatype."

          Info
_        -> forall {a}. String -> Q [a]
bad String
"The name given is not a datatype."
 where n :: String
n = Name -> String
TH.nameBase Name
nm

       check :: Con -> Q [Name]
check (TH.NormalC Name
c [BangType]
xs) = case [BangType]
xs of
                                   [] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure [Name
c]
                                   [BangType]
_  -> forall {a}. String -> Q [a]
bad forall a b. (a -> b) -> a -> b
$ String
"Constructor " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
c forall a. [a] -> [a] -> [a]
++ String
" has arguments."

       check Con
c                 = forall {a}. String -> Q [a]
bad forall a b. (a -> b) -> a -> b
$ String
"Constructor " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Con
c forall a. [a] -> [a] -> [a]
++ String
" is not an enumeration value."

       bad :: String -> Q [a]
bad String
m = do String -> Q ()
TH.reportError forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"Data.SBV.mkSymbolicEnumeration: Invalid argument " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
n
                                           , String
""
                                           , String
"    Expected an enumeration. " forall a. [a] -> [a] -> [a]
++ String
m
                                           , String
""
                                           , String
"    To create an enumerated sort, use a simple Haskell enumerated type."
                                           ]
                  forall (f :: * -> *) a. Applicative f => a -> f a
pure []

-- | Make sure the given type is an empty data
ensureEmptyData :: TH.Name -> TH.Q [TH.Name]
ensureEmptyData :: Name -> Q [Name]
ensureEmptyData Name
nm = do
        Info
c <- Name -> Q Info
TH.reify Name
nm
        case Info
c of
          TH.TyConI Dec
d -> case Dec
d of
                           TH.DataD Cxt
_ Name
_ [TyVarBndr ()]
_ Maybe Type
_ [Con]
cons [DerivClause]
_ -> case [Con]
cons of
                                                        [] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure []
                                                        [Con]
_  -> forall {a}. String -> Q [a]
bad String
"The datatype given has constructors."
                           Dec
_                       -> forall {a}. String -> Q [a]
bad String
"The name given is not a datatype."

          Info
_        -> forall {a}. String -> Q [a]
bad String
"The name given is not a datatype."
 where n :: String
n = Name -> String
TH.nameBase Name
nm
       bad :: String -> Q [a]
bad String
m = do String -> Q ()
TH.reportError forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"Data.SBV.mkUninterpretedSort: Invalid argument " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
n
                                           , String
""
                                           , String
"    Expected an empty datatype. " forall a. [a] -> [a] -> [a]
++ String
m
                                           , String
""
                                           , String
"    To create an uninterpreted sort, use an empty datatype declaration."
                                           ]
                  forall (f :: * -> *) a. Applicative f => a -> f a
pure []