-- 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.2


-- | (The sbvPlugin is hosted at
--   <a>http://github.com/LeventErkok/sbvPlugin</a>. Comments, bug reports,
--   and patches are always welcome.)
--   
--   <h2>SBVPlugin: A GHC Plugin for SBV, SMT Based Verification</h2>
--   
--   <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.
--   
--   <h3><i>Example</i></h3>
--   
--   <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>
--   
--   When compiled via GHC or loaded into GHCi, we get:
--   
--   <pre>
--   [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>
--   
--   <h3><i>Using the plugin from GHCi</i></h3>
--   
--   The plugin should work from GHCi with no changes. Note that when run
--   from GHCi, the plugin will behave as if the <tt>IgnoreFailure</tt>
--   option is given on all annotations, so that failures do not stop the
--   load process.
--   
--   <h3><i>Plugin order</i></h3>
--   
--   By default, sbvPlugin runs before GHCs optimizer passes. While the
--   order of the run should not matter in general, the simplifier can
--   rearrange the core in various ways that can have an impact on the
--   verification conditions generated by the plugin. As an experiment, you
--   can pass the argument <tt>runLast</tt> to the plugin to see if it
--   makes any difference, using the following argument to GHC:
--   
--   <pre>
--   -fplugin-opt Data.SBV.Plugin:runLast
--   </pre>
--   
--   Please report if you find any crucial differences when the plugin is
--   run first or last, especially if the outputs are different.
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

-- | Produce really verbose output, use only when things go really wrong!
Debug :: 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

-- | If a list-input is found, use this length. If not specified, we will
--   complain!
ListSize :: Int -> 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