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

{-# 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

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 IO Bool -> (SomeException -> IO Bool) -> IO Bool
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`C.catch` (\(SomeException
_ :: C.SomeException) -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)
  where check :: IO Bool
check = do ThmResult SMTResult
r <- SMTConfig -> (SBool -> SBool) -> IO ThmResult
forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m ThmResult
proveWith SMTConfig
cfg ((SBool -> SBool) -> IO ThmResult)
-> (SBool -> SBool) -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ \SBool
x -> SBool -> SBool
sNot (SBool -> SBool
sNot SBool
x) SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBool
x :: SBool)
                   case SMTResult
r of
                     Unsatisfiable{} -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                     SMTResult
_               -> Bool -> IO Bool
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
CVC4      = SMTConfig
cvc4
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 = (SMTConfig -> IO Bool) -> [SMTConfig] -> IO [SMTConfig]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM SMTConfig -> IO Bool
sbvCheckSolverInstallation ((Solver -> SMTConfig) -> [Solver] -> [SMTConfig]
forall a b. (a -> b) -> [a] -> [b]
map Solver -> SMTConfig
defaultSolverConfig [Solver
forall a. Bounded a => a
minBound .. Solver
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 :: TypeQ
typeCon = Name -> TypeQ
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 [Dec] -> Q [Dec]
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 <- Name -> TypeQ
TH.conT ''SBV TypeQ -> TypeQ -> TypeQ
`TH.appT` TypeQ
typeCon

    let declConstructor :: Name -> [Dec]
declConstructor Name
c = [Dec
sig, Dec
def]
          where nm :: Name
nm   = String -> Name
TH.mkName (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ Char
's' Char -> String -> String
forall a. a -> [a] -> [a]
: Name -> String
TH.nameBase Name
c
                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

        cdecl :: [Dec]
cdecl = (Name -> [Dec]) -> [Name] -> [Dec]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Name -> [Dec]
declConstructor [Name]
cstrs

    let tdecl :: Dec
tdecl = Name -> [TyVarBndr] -> Type -> Dec
TH.TySynD (String -> Name
TH.mkName (Char
'S' Char -> String -> String
forall a. a -> [a] -> [a]
: Name -> String
TH.nameBase Name
typeName)) [] Type
sType
    [Dec] -> Q [Dec]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Dec] -> Q [Dec]) -> [Dec] -> Q [Dec]
forall a b. (a -> b) -> a -> b
$ [Dec]
deriveEqOrds [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++ [Dec]
derives [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++ [Dec
tdecl] [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++ [Dec]
cdecl

-- | 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
                                                        [] -> String -> Q [Name]
forall a. String -> Q [a]
bad String
"The datatype given has no constructors."
                                                        [Con]
xs -> [[Name]] -> [Name]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Name]] -> [Name]) -> Q [[Name]] -> Q [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Con -> Q [Name]) -> [Con] -> Q [[Name]]
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
_                       -> String -> Q [Name]
forall a. String -> Q [a]
bad String
"The name given is not a datatype."

          Info
_        -> String -> Q [Name]
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
                                   [] -> [Name] -> Q [Name]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Name
c]
                                   [BangType]
_  -> String -> Q [Name]
forall a. String -> Q [a]
bad (String -> Q [Name]) -> String -> Q [Name]
forall a b. (a -> b) -> a -> b
$ String
"Constructor " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" has arguments."

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

       bad :: String -> Q [a]
bad String
m = do String -> Q ()
TH.reportError (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"Data.SBV.mkSymbolicEnumeration: Invalid argument " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
n
                                           , String
""
                                           , String
"    Expected an enumeration. " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
m
                                           , String
""
                                           , String
"    To create an enumerated sort, use a simple Haskell enumerated type."
                                           ]
                  [a] -> Q [a]
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
                                                        [] -> [Name] -> Q [Name]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
                                                        [Con]
_  -> String -> Q [Name]
forall a. String -> Q [a]
bad String
"The datatype given has constructors."
                           Dec
_                       -> String -> Q [Name]
forall a. String -> Q [a]
bad String
"The name given is not a datatype."

          Info
_        -> String -> Q [Name]
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 (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"Data.SBV.mkUninterpretedSort: Invalid argument " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
n
                                           , String
""
                                           , String
"    Expected an empty datatype. " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
m
                                           , String
""
                                           , String
"    To create an uninterpreted sort, use an empty datatype declaration."
                                           ]
                  [a] -> Q [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []