-- 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. Yices (required) is the
--   backend SMT solver. ImProve compiles to C, Ada, Simulink, and
--   Modelica.
@package improve
@version 0.3.4

module Language.ImProve.Code.Common
indent :: String -> String


-- | 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 -> Path -> a -> V a

-- | A mutable array.
data A a
A :: Bool -> Path -> [a] -> A a
type Name = String
type Path = [Name]
type UID = Int
class PathName a
pathName :: PathName a => a -> String
class Eq a => AllE a
zero :: AllE 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
Assign :: V a -> E a -> Statement
Branch :: E Bool -> Statement -> Statement -> Statement
Sequence :: Statement -> Statement -> Statement
Theorem :: Int -> Int -> [Int] -> E Bool -> Statement
Assume :: Int -> E Bool -> Statement
Label :: Name -> Statement -> Statement
Null :: Statement
type VarInfo = (Bool, Path, Const)
varInfo :: AllE a => V a -> VarInfo

-- | Variables in a program.
stmtVars :: Statement -> [VarInfo]

-- | Length of array.
arrayLength :: A a -> Int

-- | Theorems in a program.
theorems :: Statement -> [(Int, Int, [Int], E Bool)]
instance Eq a => Eq (V a)
instance Eq a => Eq (A a)
instance Ord a => Ord (A a)
instance Show Const
instance Eq Const
instance Ord Const
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 (A a)
instance PathName (V a)
instance PathName Path

module Language.ImProve.Code.Ada

-- | Generate Ada.
codeAda :: Name -> Statement -> IO ()
instance Show Statement

module Language.ImProve.Code.C

-- | Generate C.
codeC :: Name -> Statement -> IO ()
instance Show Statement

module Language.ImProve.Code.Simulink
codeSimulink :: Name -> Statement -> IO ()
data Netlist
Netlist :: Int -> Path -> [Path] -> [Name] -> [(Name, Block)] -> [(Name, (Name, Int))] -> Netlist
nextId :: Netlist -> Int
path :: Netlist -> Path
vars :: Netlist -> [Path]
env :: Netlist -> [Name]
blocks :: Netlist -> [(Name, Block)]
nets :: Netlist -> [(Name, (Name, Int))]
data Block
Inport :: Const -> Block
Outport :: Const -> Block
UnitDelay :: Const -> Block
Cast :: String -> Block
Assertion :: Block
Const' :: Const -> Block
Add' :: Block
Sub' :: Block
Mul' :: Block
Div' :: Block
Mod' :: Block
Not' :: Block
And' :: Block
Or' :: Block
Eq' :: Block
Lt' :: Block
Gt' :: Block
Le' :: Block
Ge' :: Block
Mux' :: Block

-- | Builds a netlist.
netlist :: Statement -> IO Netlist
instance Show Mdl

module Language.ImProve.Code.Modelica
codeModelica :: Name -> Statement -> IO ()

module Language.ImProve.Code

-- | Code generation targets.
data Target
Ada :: Target
C :: Target
Modelica :: Target
Simulink :: Target

-- | Generate target code.
code :: Target -> Name -> Statement -> IO ()
instance Eq Target

module Language.ImProve.Verify

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

module Language.ImProve.Path
totalPaths :: 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();
--   }
--   
--   switch (a) {              <a>case_</a> $ do
--       case 1:                   a ==. 1 ==&gt; do1
--           do1();                a ==. 2 ==&gt; do2
--           break;                true    ==&gt; do3
--       case 2:
--           do2();
--           break;
--       default:
--           do3();
--   }
--   </pre>
--   
--   <i>Assertion Statements</i>
--   
--   <pre>
--   assert(condition);        <a>theorem</a> name k lemmas condition
--   </pre>
--   
--   <i>Statement Labels</i>
--   
--   <pre>
--   label: {                  "label" <a>-|</a> 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
--   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>div_</a> a b   -- int
--   a % b                     <a>mod_</a> 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, which are inlined at code generation.)
--   
--   <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 Eq a => AllE a
zero :: AllE a => a
class AllE a => NumE a
type Name = String

-- | Theorem to be proven or used as lemmas to assist proofs of other
--   theorems.
data Theorem

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

-- | Logical implication.
(-->) :: 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 of two points.
linear :: (Float, Float) -> (Float, Float) -> E Float -> E Float

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

-- | Labels a statement and creates a new variable scope. Labels are used
--   in counter examples to help trace the program execution.
(-|) :: Name -> Stmt a -> Stmt a

-- | Generic variable declaration.
var :: AllE a => Name -> a -> Stmt (V a)

-- | Generic variable declaration and immediate assignment.
var' :: AllE a => Name -> E a -> Stmt (E 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)) -> Path -> E a

-- | Global variable declaration.
global :: AllE a => (Name -> a -> Stmt (V a)) -> Path -> a -> V 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 ()

-- | Condition case statement.
case_ :: Case () -> Stmt ()
(==>) :: E Bool -> Stmt () -> Case ()

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

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

-- | Assume a condition is true. Assumptions are used as lemmas to other
--   theorems.
assume :: Name -> E Bool -> Stmt Theorem

-- | Defines a new theorem.
--   
--   <pre>
--   theorem name k lemmas proposition
--   </pre>
theorem :: Name -> Int -> [Theorem] -> E Bool -> Stmt Theorem

-- | Verify a program.
--   
--   <pre>
--   verify pathToYices program
--   </pre>
verify :: FilePath -> Stmt () -> IO ()

-- | Code generation targets.
data Target
Ada :: Target
C :: Target
Modelica :: Target
Simulink :: Target

-- | Generate code.
code :: Target -> Name -> Stmt () -> IO ()

-- | Generic program analysis.
analyze :: (Statement -> IO a) -> Stmt () -> IO a
instance Monad Case
instance AllE a => Assign a
instance Monad Stmt