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


-- | An imperative, verifiable programming language for embedded applications.
--   
--   TODO
@package improve
@version 0.0.2


-- | 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
class AllE a
showConst :: (AllE a) => a -> String
showType :: (AllE a) => a -> String
zero :: (AllE a) => (Name -> a -> m (V a)) -> a
class (AllE a) => NumE a
data Statement
AssignBool :: (V Bool) -> (E Bool) -> Statement
AssignInt :: (V Int) -> (E Int) -> Statement
AssignFloat :: (V Float) -> (E Float) -> Statement
Branch :: [Name] -> (E Bool) -> Statement -> Statement -> Statement
Sequence :: Statement -> Statement -> Statement
Assert :: [Name] -> (E Bool) -> Statement
Assume :: [Name] -> (E Bool) -> Statement
Null :: Statement
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

module Language.ImProve.Verify
verify :: Statement -> IO (Maybe Bool)

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

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

-- | The Stmt monad holds variable declarations and statements.
data 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 :: Stmt () -> IO (Maybe Bool)

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

-- | Computes the greatest common divison of two integers. Returns true if
--   the computation is done, and the result.
gcd' :: E Int -> E Int -> Stmt (E Bool, E Int)

-- | A top level wrapper for gcd'.
gcdMain :: Stmt ()

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