---------------------------------------------------------------------------
-- |
-- Module      :  Data.SBV.Plugin.Data
-- Copyright   :  (c) Levent Erkok
-- License     :  BSD3
-- Maintainer  :  erkokl@gmail.com
-- Stability   :  experimental
--
-- Internal data-structures for the sbvPlugin
-----------------------------------------------------------------------------

{-# LANGUAGE DeriveDataTypeable #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Plugin.Data where

import Data.Data  (Data, Typeable)

-- | Plugin options. Note that we allow picking multiple solvers, which
-- will all be run in parallel. You can pick and choose any number of them,
-- or if you want to run all available solvers, then use the option 'AnySolver'.
-- The default behavior is to error-out on failure, using the default-SMT solver picked by SBV, which is currently Z3.
data SBVOption = IgnoreFailure  -- ^ Continue even if proof fails
               | Skip String    -- ^ Skip the proof. Can be handy for properties that we currently do not want to focus on.
               | Verbose        -- ^ Produce verbose output, good for debugging
               | Debug          -- ^ Produce really verbose output, use only when things go really wrong!
               | QuickCheck     -- ^ Perform quickCheck
               | Uninterpret    -- ^ Uninterpret this binding for proof purposes
               | Names [String] -- ^ Use these names for the arguments; need not be exhaustive
               | ListSize Int   -- ^ If a list-input is found, use this length. If not specified, we will complain!
               | Z3             -- ^ Use Z3
               | Yices          -- ^ Use Yices
               | Boolector      -- ^ Use Boolector
               | CVC4           -- ^ Use CVC4
               | MathSAT        -- ^ Use MathSAT
               | ABC            -- ^ Use ABC
               | AnySolver      -- ^ Run all installed solvers in parallel, and report the result from the first to finish
               deriving (Int -> SBVOption -> ShowS
[SBVOption] -> ShowS
SBVOption -> String
(Int -> SBVOption -> ShowS)
-> (SBVOption -> String)
-> ([SBVOption] -> ShowS)
-> Show SBVOption
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SBVOption -> ShowS
showsPrec :: Int -> SBVOption -> ShowS
$cshow :: SBVOption -> String
show :: SBVOption -> String
$cshowList :: [SBVOption] -> ShowS
showList :: [SBVOption] -> ShowS
Show, SBVOption -> SBVOption -> Bool
(SBVOption -> SBVOption -> Bool)
-> (SBVOption -> SBVOption -> Bool) -> Eq SBVOption
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SBVOption -> SBVOption -> Bool
== :: SBVOption -> SBVOption -> Bool
$c/= :: SBVOption -> SBVOption -> Bool
/= :: SBVOption -> SBVOption -> Bool
Eq, Typeable SBVOption
Typeable SBVOption =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> SBVOption -> c SBVOption)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SBVOption)
-> (SBVOption -> Constr)
-> (SBVOption -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c SBVOption))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SBVOption))
-> ((forall b. Data b => b -> b) -> SBVOption -> SBVOption)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SBVOption -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SBVOption -> r)
-> (forall u. (forall d. Data d => d -> u) -> SBVOption -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> SBVOption -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> SBVOption -> m SBVOption)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SBVOption -> m SBVOption)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SBVOption -> m SBVOption)
-> Data SBVOption
SBVOption -> Constr
SBVOption -> DataType
(forall b. Data b => b -> b) -> SBVOption -> SBVOption
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> SBVOption -> u
forall u. (forall d. Data d => d -> u) -> SBVOption -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SBVOption -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SBVOption -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SBVOption -> m SBVOption
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SBVOption -> m SBVOption
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SBVOption
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SBVOption -> c SBVOption
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SBVOption)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SBVOption)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SBVOption -> c SBVOption
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SBVOption -> c SBVOption
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SBVOption
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SBVOption
$ctoConstr :: SBVOption -> Constr
toConstr :: SBVOption -> Constr
$cdataTypeOf :: SBVOption -> DataType
dataTypeOf :: SBVOption -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SBVOption)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SBVOption)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SBVOption)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SBVOption)
$cgmapT :: (forall b. Data b => b -> b) -> SBVOption -> SBVOption
gmapT :: (forall b. Data b => b -> b) -> SBVOption -> SBVOption
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SBVOption -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SBVOption -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SBVOption -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SBVOption -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SBVOption -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> SBVOption -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SBVOption -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SBVOption -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SBVOption -> m SBVOption
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SBVOption -> m SBVOption
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SBVOption -> m SBVOption
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SBVOption -> m SBVOption
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SBVOption -> m SBVOption
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SBVOption -> m SBVOption
Data, Typeable)

-- | The actual annotation.
newtype SBVAnnotation = SBV {SBVAnnotation -> [SBVOption]
options :: [SBVOption]}
                      deriving (SBVAnnotation -> SBVAnnotation -> Bool
(SBVAnnotation -> SBVAnnotation -> Bool)
-> (SBVAnnotation -> SBVAnnotation -> Bool) -> Eq SBVAnnotation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SBVAnnotation -> SBVAnnotation -> Bool
== :: SBVAnnotation -> SBVAnnotation -> Bool
$c/= :: SBVAnnotation -> SBVAnnotation -> Bool
/= :: SBVAnnotation -> SBVAnnotation -> Bool
Eq, Typeable SBVAnnotation
Typeable SBVAnnotation =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> SBVAnnotation -> c SBVAnnotation)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SBVAnnotation)
-> (SBVAnnotation -> Constr)
-> (SBVAnnotation -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c SBVAnnotation))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c SBVAnnotation))
-> ((forall b. Data b => b -> b) -> SBVAnnotation -> SBVAnnotation)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SBVAnnotation -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SBVAnnotation -> r)
-> (forall u. (forall d. Data d => d -> u) -> SBVAnnotation -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> SBVAnnotation -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation)
-> Data SBVAnnotation
SBVAnnotation -> Constr
SBVAnnotation -> DataType
(forall b. Data b => b -> b) -> SBVAnnotation -> SBVAnnotation
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> SBVAnnotation -> u
forall u. (forall d. Data d => d -> u) -> SBVAnnotation -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SBVAnnotation -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SBVAnnotation -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SBVAnnotation
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SBVAnnotation -> c SBVAnnotation
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SBVAnnotation)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SBVAnnotation)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SBVAnnotation -> c SBVAnnotation
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SBVAnnotation -> c SBVAnnotation
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SBVAnnotation
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SBVAnnotation
$ctoConstr :: SBVAnnotation -> Constr
toConstr :: SBVAnnotation -> Constr
$cdataTypeOf :: SBVAnnotation -> DataType
dataTypeOf :: SBVAnnotation -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SBVAnnotation)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SBVAnnotation)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SBVAnnotation)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SBVAnnotation)
$cgmapT :: (forall b. Data b => b -> b) -> SBVAnnotation -> SBVAnnotation
gmapT :: (forall b. Data b => b -> b) -> SBVAnnotation -> SBVAnnotation
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SBVAnnotation -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SBVAnnotation -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SBVAnnotation -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SBVAnnotation -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SBVAnnotation -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> SBVAnnotation -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SBVAnnotation -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SBVAnnotation -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation
Data, Typeable)

-- | A property annotation, using default options.
sbv :: SBVAnnotation
sbv :: SBVAnnotation
sbv = SBV {options :: [SBVOption]
options = []}

-- | Synonym for sbv really, just looks cooler
theorem :: SBVAnnotation
theorem :: SBVAnnotation
theorem = SBVAnnotation
sbv

-- | Importable type as an annotation alternative
type Proved a = a