-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Analyze Haskell expressions using SBV/SMT
--   
--   GHC plugin for analyzing expressions using SMT solvers, based on the
--   <a>SBV</a> package.
--   
--   See <a>Data.SBV.Plugin</a> for a quick example.
@package sbvPlugin
@version 0.1


-- | (The sbvPlugin is hosted at
--   <a>http://github.com/LeventErkok/sbvPlugin</a>. Comments, bug reports,
--   and patches are always welcome.)
--   
--   SBVPlugin: A GHC Plugin for SBV, SMT Based Verification
--   
--   <a>SBV</a> is a library for express properties about Haskell programs
--   and automatically proving them using SMT solvers. The SBVPlugin allows
--   simple annotations on Haskell functions to prove them directly during
--   GHC compilation time.
--   
--   Consider the following simple program:
--   
--   <pre>
--   {-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}
--   
--   module Test where
--   
--   import Data.SBV.Plugin
--   
--   {-# ANN test theorem #-}
--   test :: Integer -&gt; Integer -&gt; Bool
--   test x y = x + y &gt;= x - y
--   </pre>
--   
--   We have:
--   
--   <pre>
--   $ ghc -c Test.hs
--   
--   [SBV] Test.hs:9:1-4 Proving "test", using Z3.
--   [Z3] Falsifiable. Counter-example:
--     x =  0 :: Integer
--     y = -1 :: Integer
--   [SBV] Failed. (Use option 'IgnoreFailure' to continue.)
--   </pre>
--   
--   Note that the compilation will be aborted, since the theorem doesn't
--   hold. As shown in the hint, GHC can be instructed to continue in that
--   case, using an annotation of the form:
--   
--   <pre>
--   {-# ANN test theorem {options = [IgnoreFailure]} #-}
--   </pre>
--   
--   The plugin should work from GHCi with no changes. Note that when run
--   from GHCi, the plugin will behave as if the <i>IgnoreFailure</i>
--   option is given on all annotations, so that failures do not stop the
--   load process.
module Data.SBV.Plugin

-- | Entry point to the plugin
plugin :: Plugin

-- | The actual annotation.
newtype SBVAnnotation
SBV :: [SBVOption] -> SBVAnnotation
[options] :: SBVAnnotation -> [SBVOption]

-- | A property annotation, using default options.
sbv :: SBVAnnotation

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

-- | Plugin options. Note that we allow picking multiple solvers, which
--   will all be run in parallel. If you want to run all available solvers,
--   use the option <a>AnySolver</a>. The default is to error-out on
--   failure, using the default-SMT solver picked by SBV, which is
--   currently Z3.
data SBVOption

-- | Continue even if proof fails
IgnoreFailure :: SBVOption

-- | Skip the proof. Can be handy for properties that we currently do not
--   want to focus on.
Skip :: String -> SBVOption

-- | Produce verbose output, good for debugging
Verbose :: SBVOption

-- | Check for safety
Safety :: SBVOption

-- | Perform quickCheck
QuickCheck :: SBVOption

-- | Uninterpret this binding for proof purposes
Uninterpret :: SBVOption

-- | Use these names for the arguments; need not be exhaustive
Names :: [String] -> SBVOption

-- | Use Z3
Z3 :: SBVOption

-- | Use Yices
Yices :: SBVOption

-- | Use Boolector
Boolector :: SBVOption

-- | Use CVC4
CVC4 :: SBVOption

-- | Use MathSAT
MathSAT :: SBVOption

-- | Use ABC
ABC :: SBVOption

-- | Use all installed solvers
AnySolver :: SBVOption