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


-- | k-induction for Copilot.
--   
--   Some tools to prove properties on Copilot programs with k-induction
--   model checking.
--   
--   Copilot is a stream (i.e., infinite lists) domain-specific language
--   (DSL) in Haskell that compiles into embedded C. Copilot contains an
--   interpreter, multiple back-end compilers, and other verification
--   tools.
--   
--   A tutorial, examples, and other information are available at
--   <a>https://copilot-language.github.io</a>.
@package copilot-theorem
@version 3.2

module Copilot.Theorem.Prove
data Output
Output :: Status -> [String] -> Output
data Status
Sat :: Status
Valid :: Status
Invalid :: Status
Unknown :: Status
Error :: Status
data Prover
Prover :: String -> (Spec -> IO r) -> (r -> [PropId] -> [PropId] -> IO Output) -> (r -> IO ()) -> Prover
[proverName] :: Prover -> String
[startProver] :: Prover -> Spec -> IO r
[askProver] :: Prover -> r -> [PropId] -> [PropId] -> IO Output
[closeProver] :: Prover -> r -> IO ()
type PropId = String
data PropRef a
[PropRef] :: PropId -> PropRef a
type Proof a = ProofScheme a ()
type UProof = Writer [Action] ()
data ProofScheme a b
[Proof] :: Writer [Action] b -> ProofScheme a b
data Action
[Check] :: Prover -> Action
[Assume] :: PropId -> Action
[Admit] :: Action
data Universal
data Existential
check :: Prover -> Proof a
prove :: Spec -> PropId -> UProof -> IO Bool
combine :: Prover -> Prover -> Prover
instance GHC.Base.Functor (Copilot.Theorem.Prove.ProofScheme a)
instance GHC.Base.Applicative (Copilot.Theorem.Prove.ProofScheme a)
instance GHC.Base.Monad (Copilot.Theorem.Prove.ProofScheme a)

module Copilot.Theorem.Prover.SMT

-- | A class for types with a default value.
class Default a

-- | The default value for this type.
def :: Default a => a

-- | Tactics
data Options
Options :: Word32 -> Word32 -> Bool -> Options
[startK] :: Options -> Word32
[maxK] :: Options -> Word32
[debug] :: Options -> Bool
induction :: SmtFormat a => Options -> Backend a -> Proof Universal
kInduction :: SmtFormat a => Options -> Backend a -> Proof Universal
onlySat :: SmtFormat a => Options -> Backend a -> Proof Existential
onlyValidity :: SmtFormat a => Options -> Backend a -> Proof Universal

-- | Backends
yices :: Backend SmtLib
dReal :: Backend SmtLib
altErgo :: Backend SmtLib
metit :: String -> Backend Tptp
z3 :: Backend SmtLib
cvc4 :: Backend SmtLib
mathsat :: Backend SmtLib
data Backend a
class Show a => SmtFormat a
data SmtLib
data Tptp
instance GHC.Classes.Eq Copilot.Theorem.Prover.SMT.SolverId
instance GHC.Classes.Ord Copilot.Theorem.Prover.SMT.SolverId
instance GHC.Show.Show Copilot.Theorem.Prover.SMT.SolverId
instance Data.Default.Class.Default Copilot.Theorem.Prover.SMT.Options

module Copilot.Theorem
instantiate :: Proof Universal -> Proof Existential
assume :: PropRef Universal -> Proof a
admit :: Proof a
type Proof a = ProofScheme a ()
type PropId = String
data PropRef a
data Universal
data Existential

module Copilot.Theorem.Kind2.Prover
data Options
Options :: Int -> Options
[bmcMax] :: Options -> Int
kind2Prover :: Options -> Prover
instance Data.Default.Class.Default Copilot.Theorem.Kind2.Prover.Options

module Copilot.Theorem.Kind2
prettyPrint :: File -> String
toKind2 :: Style -> [PropId] -> [PropId] -> TransSys -> File
data Style
Inlined :: Style
Modular :: Style
data File
File :: [PredDef] -> [Prop] -> File
[filePreds] :: File -> [PredDef]
[fileProps] :: File -> [Prop]
data Prop
Prop :: String -> Term -> Prop
[propName] :: Prop -> String
[propTerm] :: Prop -> Term
data PredDef
PredDef :: String -> [StateVarDef] -> Term -> Term -> PredDef
[predId] :: PredDef -> String
[predStateVars] :: PredDef -> [StateVarDef]
[predInit] :: PredDef -> Term
[predTrans] :: PredDef -> Term
data StateVarDef
StateVarDef :: String -> Type -> [StateVarFlag] -> StateVarDef
[varId] :: StateVarDef -> String
[varType] :: StateVarDef -> Type
[varFlags] :: StateVarDef -> [StateVarFlag]
data Type
Int :: Type
Real :: Type
Bool :: Type
data StateVarFlag
FConst :: StateVarFlag
data PredType
Init :: PredType
Trans :: PredType
data Term
ValueLiteral :: String -> Term
PrimedStateVar :: String -> Term
StateVar :: String -> Term
FunApp :: String -> [Term] -> Term
PredApp :: String -> PredType -> [Term] -> Term