-- 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 programming language for high assurance
--   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.8


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

-- | A logical, arithmetic, comparative, or conditional expression.
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

-- | A mutable variable.
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 :: (E Bool) -> Statement -> Statement -> Statement
Sequence :: Statement -> Statement -> Statement
Assert :: (E Bool) -> Statement
Assume :: (E Bool) -> Statement
Label :: 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 Ord 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 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 ()


-- | ImProve is an imperative programming language for high assurance
--   applications.
--   
--   ImProve uses infinite state, unbounded model checking to verify
--   programs adhere to specifications, which are written in the form of
--   assertion statements. If it is unable to verify an assertion, ImProve
--   will emit a counter example that shows a precise program trace that
--   exercises the assertion violation.
--   
--   The following compares the syntax of C and ImProve:
--   
--   <i>Variable Declarations</i>
--   
--   <pre>
--   float a = 0.0;            a &lt;- <a>float</a> "a" 0
--   bool b = true;            b &lt;- <a>bool</a> "b" true
--   int c = d + e + 3;        c &lt;- <a>int'</a> "c" (d + e + 3)
--   </pre>
--   
--   <i>Variable Assignments</i>
--   
--   <pre>
--   a = 1;                    a <a>&lt;==</a> 1
--   </pre>
--   
--   <i>Conditional Statements</i>
--   
--   <pre>
--   if (condition) {          <a>if_</a> condition $ do 
--       a();                      a
--       b();                      b
--       c();                      c
--   }
--   
--   if (condition {           <a>ifelse</a> condition
--       a();                      (do a
--       b();                          b
--       c();                          c)
--   }                             (do d
--   else {                            e 
--       d();                          f)
--       e();
--       f();
--   }                                 
--   </pre>
--   
--   <i>Assertion Statements</i>
--   
--   <pre>
--   assert(condition);        <a>assert</a> condition
--   </pre>
--   
--   <i>Statement Labels</i>
--   
--   <pre>
--   hello: {                  <a>label</a> "hello" $ do
--       a();                      a
--       b();                      b
--   }
--   </pre>
--   
--   <i>Expressions</i>
--   
--   <pre>
--   <i>Constant Literals</i>
--   
--   true                      <a>true</a>
--   false                     <a>false</a>
--   0                         0
--   100                       100
--   1.0                       1     -- float
--   3.14                      3.14
--   
--   <i>Variable Reference</i>
--   
--   a                         <a>ref</a> a
--   
--   <i>Logical Expressions</i>
--   
--   ! a                       <a>not_</a> a
--   a &amp;&amp; b                    a <a>&amp;&amp;.</a> b
--   a || b                    a <a>||.</a> b
--   
--   <i>Comparison Expressions</i>
--   
--   a == b                    a <a>==.</a> b
--   a != b                    a <a>/=.</a> b
--   a &lt; b                     a <a>&lt;.</a> b
--   a &gt; b                     a <a>&gt;.</a> b
--   a &lt;= b                    a <a>&lt;=.</a> b
--   a &gt;= b                    a <a>&gt;=.</a> b
--   
--   <i>Arithmetic Expressions</i>
--   
--   a + b                     a <a>+</a> b
--   a * b                     a <a>*.</a> b
--   a / b                     a <a>/.</a> b     -- float
--   a / b                     a '<a>div_</a>' b -- int
--   a % b                     a '<a>mod_</a>' b
--   abs(a)                    <a>abs</a> a
--   min(a, b)                 <a>min_</a> a b
--   max(a, b)                 <a>max_</a> a b
--   
--   <i>Conditional Expression</i>
--   
--   a ? b : c                 <a>mux</a> a b c
--   </pre>
--   
--   <i>Function Definitions and Function Calls</i> (All ImProve functions
--   are Haskell functions that are inlined at compile time.)
--   
--   <pre>
--   int add(int a, int b) {                             add :: E Int -&gt; E Int -&gt; E Int
--     return a + b;                                     add a b = a + b
--   }
--   
--   three = add(1, 2);                                  three &lt;== add 1 2
--   
--   void incrCounter(int *counter, int amount) {        incrCounter :: V Int -&gt; E Int -&gt; Stmt ()
--     *counter = *counter + amount;                     incrCounter counter amount = counter &lt;== ref counter + amount
--   }
--   
--   incrCounter(&amp;counter, 22);                          incrCounter counter 22
--   </pre>
module Language.ImProve

-- | A logical, arithmetic, comparative, or conditional expression.
data E a

-- | A mutable variable.
data V a
class AllE 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 to be used in an expression (<a>E</a>).
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 for variable names.
scope :: Name -> Stmt a -> Stmt a

-- | Labels a statement. Labels are used in counter examples to trace the
--   program execution. And assertion names, and hence counter example file
--   names, are produce from labels.
label :: 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)
class Assign a
(<==) :: (Assign a) => V a -> E a -> Stmt ()

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

-- | Conditional if without the else.
if_ :: 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 :: E Bool -> Stmt ()

-- | Declare an assumption condition is true.
assume :: 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 ()