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


-- | An imperative, verifiable programming language for high assurance applications.
--   
--   ImProve is an imperative DSL intended for high assurance, embedded
--   applications. ImProve uses infinite state, unbounded model checking to
--   verify programs adhere to specifications, which are written in the
--   form of assertion statements. Yices (required) is the backend SMT
--   solver.
@package improve
@version 0.0.5


-- | Building hierarchy from unstructured hierarchical paths.
module Language.ImProve.Tree
data Tree a b
Branch :: a -> [Tree a b] -> Tree a b
Leaf :: a -> b -> Tree a b
tree :: (Eq a, Ord a) => (b -> [a]) -> [b] -> [Tree a b]

module Language.ImProve.Core
data E a
Ref :: V a -> E a
Const :: a -> E a
Add :: E a -> E a -> E a
Sub :: E a -> E a -> E a
Mul :: E a -> a -> E a
Div :: E a -> a -> E a
Mod :: E Int -> Int -> E Int
Not :: E Bool -> E Bool
And :: E Bool -> E Bool -> E Bool
Or :: E Bool -> E Bool -> E Bool
Eq :: E a -> E a -> E Bool
Lt :: E a -> E a -> E Bool
Gt :: E a -> E a -> E Bool
Le :: E a -> E a -> E Bool
Ge :: E a -> E a -> E Bool
Mux :: E Bool -> E a -> E a -> E a
data V a
V :: Bool -> [Name] -> a -> V a
type Name = String
type Path = [Name]
class PathName a
pathName :: (PathName a) => a -> String
class AllE a
zero :: (AllE a) => (Name -> a -> m (V a)) -> a
const' :: (AllE a) => a -> Const
class (AllE a) => NumE a
data Const
Bool :: Bool -> Const
Int :: Int -> Const
Float :: Float -> Const
data Statement
AssignBool :: (V Bool) -> (E Bool) -> Statement
AssignInt :: (V Int) -> (E Int) -> Statement
AssignFloat :: (V Float) -> (E Float) -> Statement
Branch :: Path -> (E Bool) -> Statement -> Statement -> Statement
Sequence :: Statement -> Statement -> Statement
Assert :: Path -> (E Bool) -> Statement
Assume :: Path -> (E Bool) -> Statement
Annotate :: Name -> Statement -> Statement
Null :: Statement
type VarInfo = (Bool, Path, Const)
varInfo :: (AllE a) => V a -> VarInfo
stmtVars :: Statement -> [VarInfo]
exprVars :: E a -> [VarInfo]
instance Eq Const
instance (Eq a) => Eq (V a)
instance Fractional (E Float)
instance (Num a, AllE a, NumE a) => Num (E a)
instance Eq (E a)
instance Show (E a)
instance NumE Float
instance NumE Int
instance AllE Float
instance AllE Int
instance AllE Bool
instance PathName Statement
instance PathName VarInfo
instance PathName (V a)
instance PathName Path

module Language.ImProve.Verify

-- | Verify a program with k-induction.
verify :: FilePath -> Int -> Statement -> IO ()

module Language.ImProve.Code

-- | Generate C code.
code :: Name -> Statement -> IO ()

module Language.ImProve
data E a
data V a
class AllE a
zero :: (AllE a) => (Name -> a -> m (V a)) -> a
class (AllE a) => NumE a
type Name = String

-- | True term.
true :: E Bool

-- | False term.
false :: E Bool

-- | Arbitrary constants.
constant :: (AllE a) => a -> E a

-- | References a variable.
ref :: (AllE a) => V a -> E a

-- | Logical negation.
not_ :: E Bool -> E Bool

-- | Logical AND.
(&&.) :: E Bool -> E Bool -> E Bool

-- | Logical OR.
(||.) :: E Bool -> E Bool -> E Bool

-- | The conjunction of a E Bool list.
and_ :: [E Bool] -> E Bool

-- | The disjunction of a E Bool list.
or_ :: [E Bool] -> E Bool

-- | True iff the predicate is true for any element.
any_ :: (a -> E Bool) -> [a] -> E Bool

-- | True iff the predicate is true for all elements.
all_ :: (a -> E Bool) -> [a] -> E Bool
imply :: E Bool -> E Bool -> E Bool

-- | Equal.
(==.) :: (AllE a) => E a -> E a -> E Bool

-- | Not equal.
(/=.) :: (AllE a) => E a -> E a -> E Bool

-- | Less than.
(<.) :: (NumE a) => E a -> E a -> E Bool

-- | Less than or equal.
(<=.) :: (NumE a) => E a -> E a -> E Bool

-- | Greater than.
(>.) :: (NumE a) => E a -> E a -> E Bool

-- | Greater than or equal.
(>=.) :: (NumE a) => E a -> E a -> E Bool

-- | Returns the minimum of two numbers.
min_ :: (NumE a) => E a -> E a -> E a

-- | Returns the minimum of a list of numbers.
minimum_ :: (NumE a) => [E a] -> E a

-- | Returns the maximum of two numbers.
max_ :: (NumE a) => E a -> E a -> E a

-- | Returns the maximum of a list of numbers.
maximum_ :: (NumE a) => [E a] -> E a

-- | Limits between min and max.
limit :: (NumE a) => E a -> E a -> E a -> E a

-- | Multiplication.
(*.) :: (NumE a) => E a -> a -> E a

-- | Floating point division.
(/.) :: E Float -> Float -> E Float

-- | Integer division.
div_ :: E Int -> Int -> E Int

-- | Modulo.
mod_ :: E Int -> Int -> E Int

-- | Conditional expression.
--   
--   <pre>
--   mux test onTrue onFalse
--   </pre>
mux :: (AllE a) => E Bool -> E a -> E a -> E a

-- | Linear interpolation and extrapolation between two points.
linear :: (Float, Float) -> (Float, Float) -> E Float -> E Float

-- | The Stmt monad holds variable declarations and statements.
data Stmt a

-- | Creates a hierarchical scope.
scope :: Name -> Stmt a -> Stmt a

-- | Add an annotation to a statement. Useful for requirement trace tags.
annotate :: Name -> Stmt a -> Stmt a

-- | Boolean variable declaration.
bool :: Name -> Bool -> Stmt (V Bool)

-- | Boolean variable declaration and immediate assignment.
bool' :: Name -> E Bool -> Stmt (E Bool)

-- | Int variable declaration.
int :: Name -> Int -> Stmt (V Int)

-- | Int variable declaration and immediate assignment.
int' :: Name -> E Int -> Stmt (E Int)

-- | Float variable declaration.
float :: Name -> Float -> Stmt (V Float)

-- | Float variable declaration and immediate assignment.
float' :: Name -> E Float -> Stmt (E Float)

-- | Input variable declaration. Input variables are initialized to 0.
input :: (AllE a) => (Name -> a -> Stmt (V a)) -> Name -> Stmt (E a)
(<==) :: (Assign a) => V a -> E a -> Stmt ()

-- | Conditional if-else.
ifelse :: Name -> E Bool -> Stmt () -> Stmt () -> Stmt ()

-- | Conditional if without the else.
if_ :: Name -> E Bool -> Stmt () -> Stmt ()

-- | Increments an E Int.
incr :: V Int -> Stmt ()

-- | Decrements an E Int.
decr :: V Int -> Stmt ()

-- | Assert that a condition is true.
assert :: Name -> E Bool -> Stmt ()

-- | Declare an assumption condition is true.
assume :: Name -> E Bool -> Stmt ()

-- | Verify a program.
--   
--   ^ verify pathToYices maxK program
verify :: FilePath -> Int -> Stmt () -> IO ()

-- | Generate C code.
code :: Name -> Stmt () -> IO ()
instance Assign Float
instance Assign Int
instance Assign Bool
instance Monad Stmt


-- | ImProve examples.
module Language.ImProve.Examples

-- | Build the gcdMain code (i.e. gcd.c, gcd.h).
buildGCD :: IO ()

-- | A rolling counter verification example.
counter :: Stmt ()

-- | Verify the <a>counter</a> example.
verifyCounter :: IO ()

-- | Arbiter specification.
arbiterSpec :: (E Bool, E Bool, E Bool) -> (E Bool, E Bool, E Bool) -> Stmt ()

-- | Binding an arbiter implemenation to the arbiter specification.
arbiter :: Name -> ((E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)) -> Stmt ()

-- | An arbiter implementation.
arbiter1 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)

-- | An another arbiter implementation.
arbiter2 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)

-- | Yet another arbiter implementation.
arbiter3 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)

-- | Verify the different arbiter implementations.
verifyArbiters :: IO ()

-- | Build the different arbiter implementations.
buildArbiters :: IO ()

-- | Run all examples.
runAll :: IO ()