improve 0.0.1 → 0.0.2

raw patch · 7 files changed

+361/−201 lines, 7 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• Language/ImProve.hs +40/−199
• Language/ImProve/Code.hs +118/−0
• Language/ImProve/Core.hs +86/−0
• Language/ImProve/Examples.hs +57/−0
• Language/ImProve/Tree.hs +46/−0
• Language/ImProve/Verify.hs +7/−0
• improve.cabal +7/−2

@@ -11,6 +11,7 @@   , true   , false   , constant+  , zero   -- ** Variable Reference   , ref   -- ** Logical Operations@@ -29,7 +30,7 @@   , (<=.)   , (>.)   , (>=.)-  -- ** Min, max, and limiting.+  -- ** Min, Max, and Limiting   , min_   , minimum_   , max_@@ -46,7 +47,9 @@   , linear   -- * Hierarchical Scope   , scope-  -- * Variable Declarations+  -- * Statements+  , Stmt+  -- ** Variable Declarations   , bool   , bool'   , int@@ -54,8 +57,6 @@   , float   , float'   , input-  -- * Statements-  , Stmt   -- ** Variable Assignment   , (<==)   -- ** Conditional Execution@@ -67,91 +68,24 @@   -- ** Assertions and  Assumptions   , assert   , assume-  -- * Compilation-  , compile+  -- * Verification+  , verify+  -- * Code Generation+  , code   ) where  import Control.Monad-import Data.List-import Data.Ratio +import Language.ImProve.Core+import qualified Language.ImProve.Verify as V+import qualified Language.ImProve.Code   as C+ infixl 7 *., /., `div_`, `mod_` infix  4 ==., /=., <., <=., >., >=. infixl 3 &&. infixl 2 ||. infixr 1 <== -type Name = String---- | Variables.-data V a-  = V   [Name] a-  | VIn [Name]---- | All types.-class AllE a where-  showConst :: a -> String-  showType  :: a -> String-  zero      :: (Name -> a -> Stmt (V a)) -> a--instance AllE Bool where-  showConst a = case a of-    True  -> "1"-    False -> "0"-  showType _ = "int"-  zero = const False--instance AllE Int where-  showConst = show-  showType _ = "int"-  zero = const 0-  -instance AllE Float where-  showConst = show-  showType _ = "float"-  zero = const 0---- | Number types.-class    AllE a => NumE a-instance NumE Int-instance NumE Float---- | Core expressions.-data E a where-  Ref   :: AllE a => V a -> E a-  Const :: AllE a => a -> E a-  Add   :: NumE a => E a -> E a -> E a-  Sub   :: NumE a => E a -> E a -> E a-  Mul   :: NumE a => E a -> a -> E a-  Div   :: NumE a => 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    :: AllE a => E a -> E a -> E Bool-  Lt    :: NumE a => E a -> E a -> E Bool-  Gt    :: NumE a => E a -> E a -> E Bool-  Le    :: NumE a => E a -> E a -> E Bool-  Ge    :: NumE a => E a -> E a -> E Bool-  Mux   :: AllE a => E Bool -> E a -> E a -> E a--instance Show (E a) where show = undefined -instance Eq   (E a) where (==) = undefined--instance (Num a, AllE a, NumE a) => Num (E a) where-  (+) = Add-  (-) = Sub-  (*) = error "general multiplication not supported, use (*.)"-  negate a = 0 - a-  abs a = mux (a <. 0) (negate a) a-  signum a = mux (a ==. 0) 0 $ mux (a <. 0) (-1) 1-  fromInteger = Const . fromInteger--instance Fractional (E Float) where-  (/) = error "general division not supported, use (/.)"-  recip a = 1 / a-  fromRational r = Const $ fromInteger (numerator r) / fromInteger (denominator r)- -- | True term. true :: E Bool true = Const True@@ -283,33 +217,28 @@ scope :: Name -> Stmt a -> Stmt a scope name (Stmt f0) = Stmt f1   where-  f1 (path, items, statement) = (a, (path, Scope name items0 : items, statement1))+  f1 (path, statement) = (a, (path, statement1))     where-    (a, (_, items0, statement1)) = f0 (path ++ [name], [], statement)+    (a, (_, statement1)) = f0 (path ++ [name], statement)   -get :: Stmt ([Name], [Scope], Statement)+get :: Stmt ([Name], Statement) get = Stmt $ \ a -> (a, a)  getPath :: Stmt [Name] getPath = do-  (path, _, _) <- get+  (path, _) <- get   return path -put :: ([Name], [Scope], Statement) -> Stmt ()-put a = Stmt $ \ _ -> ((), a)- var :: AllE a => Name -> a -> Stmt (V a) var name init = do-  (path, items, stmt) <- get-  put (path, Variable name (showType init) (showConst init) : items, stmt)-  return $ V (path ++ [name]) init+  path <- getPath+  return $ V False (path ++ [name]) init  -- | Input variable declaration.  Input variables are initialized to 0. input  :: AllE a => (Name -> a -> Stmt (V a)) -> Name -> Stmt (E a) input f name = do-  (path, items, stmt) <- get-  put (path, Variable name (showType $ zero f) (showConst $ zero f) : items, stmt)-  return $ ref $ VIn (path ++ [name])+  path <- getPath+  return $ ref $ V True (path ++ [name]) $ zero f  -- | Boolean variable declaration. bool :: Name -> Bool -> Stmt (V Bool)@@ -352,18 +281,8 @@ decr :: V Int -> Stmt () decr a = a <== ref a - 1 -data Statement-  = AssignBool  (V Bool ) (E Bool )-  | AssignInt   (V Int  ) (E Int  )-  | AssignFloat (V Float) (E Float)-  | Branch (E Bool) Statement Statement-  | Sequence Statement Statement-  | Assert [Name] (E Bool)-  | Assume [Name] (E Bool)-  | Null- -- | The Stmt monad holds variable declarations and statements.-data Stmt a = Stmt (([Name], [Scope], Statement) -> (a, ([Name], [Scope], Statement)))+data Stmt a = Stmt (([Name], Statement) -> (a, ([Name], Statement)))  instance Monad Stmt where   return a = Stmt $ \ s -> (a, s)@@ -375,10 +294,10 @@       Stmt f4 = f2 a  statement :: Statement -> Stmt ()-statement a = Stmt $ \ (path, scope, statement) -> ((), (path, scope, Sequence statement a))+statement a = Stmt $ \ (path, statement) -> ((), (path, Sequence statement a)) -evalStmt :: [Name] -> [Scope] -> Stmt () -> ([Name], [Scope], Statement)-evalStmt path items (Stmt f) = snd $ f (path, items, Null)+evalStmt :: [Name] -> Stmt () -> ([Name], Statement)+evalStmt path (Stmt f) = snd $ f (path, Null)  class    Assign a     where (<==) :: V a -> E a -> Stmt () instance Assign Bool  where a <== b = statement $ AssignBool  a b@@ -398,100 +317,22 @@   statement $ Assume (path ++ [a]) b  -- | Conditional if-else.-ifelse :: E Bool -> Stmt () -> Stmt () -> Stmt ()-ifelse cond onTrue onFalse = do-  (path, items, stmt) <- get-  let (_, items1, stmt1) = evalStmt path items  onTrue-      (_, items2, stmt2) = evalStmt path items1 onFalse-  put (path, items2, stmt)-  statement $ Branch cond stmt1 stmt2---- | Conditional without the else.-if_ :: E Bool -> Stmt () -> Stmt()-if_ cond stmt = ifelse cond stmt $ return ()---- | Generate C code.-compile :: Name -> Stmt () -> IO ()-compile name program = do-  writeFile (name ++ ".c") $-       "// Generated by ImProve.\n\n"-    ++ "#include <assert.h>\n\n"-    ++ codeVariables True scope ++ "\n"-    ++ "void " ++ name ++ "() {\n"-    ++ indent (codeStmt stmt)-    ++ "}\n\n"-  writeFile (name ++ ".h") $-       "// Generated by ImProve.\n\n"-    ++ codeVariables False scope ++ "\n"-    ++ "void " ++ name ++ "(void);\n\n"-  where-  (_, items, stmt) = evalStmt [name ++ "Variables"] [] program-  scope = Scope (name ++ "Variables") items--varName :: V a -> String-varName a = intercalate "." names-  where-  names = case a of-    V   names _ -> names-    VIn names   -> names--codeStmt :: Statement -> String-codeStmt a = case a of-  AssignBool  a b -> varName a ++ " = " ++ codeExpr b ++ ";\n"-  AssignInt   a b -> varName a ++ " = " ++ codeExpr b ++ ";\n"-  AssignFloat a b -> varName a ++ " = " ++ codeExpr b ++ ";\n"-  Branch a b Null -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt b) ++ "}\n"-  Branch a b c    -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt b) ++ "}\nelse {\n" ++ indent (codeStmt c) ++ "}\n"-  Sequence a b -> codeStmt a ++ codeStmt b-  Assert names a -> "// assert " ++ intercalate "." names ++ "\nassert(" ++ codeExpr a ++ ");\n"-  Assume names a -> "// assume " ++ intercalate "." names ++ "\nassert(" ++ codeExpr a ++ ");\n"-  Null -> ""--codeExpr :: E a -> String-codeExpr a = case a of-  Ref a -> varName a-  Const a -> showConst a-  Add a b -> group [codeExpr a, "+", codeExpr b]-  Sub a b -> group [codeExpr a, "-", codeExpr b]-  Mul a b -> group [codeExpr a, "*", showConst b]-  Div a b -> group [codeExpr a, "/", showConst b]-  Mod a b -> group [codeExpr a, "%", showConst b]-  Not a   -> group ["!", codeExpr a]-  And a b -> group [codeExpr a, "&&",  codeExpr b]-  Or  a b -> group [codeExpr a, "||",  codeExpr b]-  Eq  a b -> group [codeExpr a, "==",  codeExpr b]-  Lt  a b -> group [codeExpr a, "<",   codeExpr b]-  Gt  a b -> group [codeExpr a, ">",   codeExpr b]-  Le  a b -> group [codeExpr a, "<=",  codeExpr b]-  Ge  a b -> group [codeExpr a, ">=",  codeExpr b]-  Mux a b c -> group [codeExpr a, "?", codeExpr b, ":", codeExpr c] -  where-  group :: [String] -> String-  group a = "(" ++ intercalate " " a ++ ")"--indent :: String -> String-indent = unlines . map ("  " ++) . lines--data Scope-  = Scope Name [Scope]-  | Variable Name String String  -- name type init-  deriving Eq+ifelse :: Name -> E Bool -> Stmt () -> Stmt () -> Stmt ()+ifelse name cond onTrue onFalse = do+  path <- getPath+  let (_, stmt1) = evalStmt path onTrue+      (_, stmt2) = evalStmt path onFalse+  statement $ Branch (path ++ [name]) cond stmt1 stmt2 -instance Ord Scope where-  compare a b = case (a, b) of-    (Scope a _, Scope b _) -> compare a b-    (Variable a _ _, Variable b _ _) -> compare a b-    (Variable _ _ _, Scope _ _) -> LT-    (Scope _ _, Variable _ _ _) -> GT+-- | Conditional if without the else.+if_ :: Name -> E Bool -> Stmt () -> Stmt()+if_ name cond stmt = ifelse name cond stmt $ return () -codeVariables :: Bool -> Scope -> String-codeVariables define a = (if define then "" else "extern ") ++ init (init (f1 a)) ++ (if define then " =\n" ++ f2 a else "") ++ ";\n"-  where-  f1 a = case a of-    Scope     name items -> "struct {  // " ++ name ++ "\n" ++ indent (concatMap f1 $ sort items) ++ "} " ++ name ++ ";\n"-    Variable  name typ _ -> typ ++ " " ++ name ++ ";\n"+-- | Verify a program.+verify :: Stmt () -> IO (Maybe Bool)+verify program = V.verify $ snd $ evalStmt [] program -  f2 a = case a of-    Scope    name items  -> "{  // " ++ name ++ "\n" ++ indent (intercalate ",\n" (map f2 $ sort items)) ++ "\n}"-    Variable name _ init -> "/* " ++ name ++ " */  " ++ init+-- | Generate C code.+code :: Name -> Stmt () -> IO ()+code name program = C.code name $ snd $ evalStmt [name ++ "Variables"] program 

@@ -0,0 +1,118 @@+module Language.ImProve.Code (code) where++import Data.List+import Text.Printf++import Language.ImProve.Core+import Language.ImProve.Tree hiding (Branch)+import qualified Language.ImProve.Tree as T++-- | Generate C code.+code :: Name -> Statement -> IO ()+code name stmt = do+  writeFile (name ++ ".c") $+       "// Generated by ImProve.\n\n"+    ++ "#include <assert.h>\n\n"+    ++ codeVariables True scope ++ "\n"+    ++ "void " ++ name ++ "() {\n"+    ++ indent (codeStmt stmt)+    ++ "}\n\n"+  writeFile (name ++ ".h") $+       "// Generated by ImProve.\n\n"+    ++ codeVariables False scope ++ "\n"+    ++ "void " ++ name ++ "(void);\n\n"+  where+  [scope] = tree (\ (path, _, _, _) -> path) $ varsInStmt stmt++varName :: V a -> String+varName a = intercalate "." names+  where+  names = case a of+    V _ names _ -> names++codeStmt :: Statement -> String+codeStmt a = case a of+  AssignBool  a b -> varName a ++ " = " ++ codeExpr b ++ ";\n"+  AssignInt   a b -> varName a ++ " = " ++ codeExpr b ++ ";\n"+  AssignFloat a b -> varName a ++ " = " ++ codeExpr b ++ ";\n"+  Branch path a b Null -> "// if_ "    ++ intercalate "." path ++ "\nif (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt b) ++ "}\n"+  Branch path a b c    -> "// ifelse " ++ intercalate "." path ++ "\nif (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt b) ++ "}\nelse {\n" ++ indent (codeStmt c) ++ "}\n"+  Sequence a b -> codeStmt a ++ codeStmt b+  Assert path a -> "// assert " ++ intercalate "." path ++ "\nassert(" ++ codeExpr a ++ ");\n"+  Assume path a -> "// assume " ++ intercalate "." path ++ "\nassert(" ++ codeExpr a ++ ");\n"+  Null -> ""++codeExpr :: E a -> String+codeExpr a = case a of+  Ref a -> varName a+  Const a -> showConst a+  Add a b -> group [codeExpr a, "+", codeExpr b]+  Sub a b -> group [codeExpr a, "-", codeExpr b]+  Mul a b -> group [codeExpr a, "*", showConst b]+  Div a b -> group [codeExpr a, "/", showConst b]+  Mod a b -> group [codeExpr a, "%", showConst b]+  Not a   -> group ["!", codeExpr a]+  And a b -> group [codeExpr a, "&&",  codeExpr b]+  Or  a b -> group [codeExpr a, "||",  codeExpr b]+  Eq  a b -> group [codeExpr a, "==",  codeExpr b]+  Lt  a b -> group [codeExpr a, "<",   codeExpr b]+  Gt  a b -> group [codeExpr a, ">",   codeExpr b]+  Le  a b -> group [codeExpr a, "<=",  codeExpr b]+  Ge  a b -> group [codeExpr a, ">=",  codeExpr b]+  Mux a b c -> group [codeExpr a, "?", codeExpr b, ":", codeExpr c] +  where+  group :: [String] -> String+  group a = "(" ++ intercalate " " a ++ ")"++indent :: String -> String+indent = unlines . map ("  " ++) . lines++indent' :: String -> String+indent' a = case lines a of+  [] -> []+  (a:b) -> a ++ "\n" ++ indent (unlines b)++codeVariables :: Bool -> (Tree Name ([Name], Bool, String, String)) -> String+codeVariables define a = (if define then "" else "extern ") ++ init (init (f1 a)) ++ (if define then " =\n  " ++ f2 a else "") ++ ";\n"+  where+  f1 a = case a of+    T.Branch name items -> "struct {  // " ++ name ++ "\n" ++ indent (concatMap f1 items) ++ "} " ++ name ++ ";\n"+    Leaf name (_, input, typ, _) -> printf "%-5s %-25s;%s\n" typ name (if input then "  // input" else "")++  f2 a = case a of+    T.Branch name items -> indent' $ "{ " ++ (intercalate ", " $ map f2 items) ++ "}  // " ++ name ++ "\n"+    Leaf name (_, _, _, init) -> printf "%-15s  // %s\n" init name++varInfo :: AllE a => V a -> ([Name], Bool, String, String)+varInfo (V input path a) = (path, input, showType a, showConst a)++varsInStmt :: Statement -> [([Name], Bool, String, String)] -- (path, isInput, type, init)+varsInStmt a = case a of+  AssignBool  a b -> nub $ varInfo a : varsInExpr b+  AssignInt   a b -> nub $ varInfo a : varsInExpr b+  AssignFloat a b -> nub $ varInfo a : varsInExpr b+  Branch _ a b c  -> nub $ varsInExpr a ++ varsInStmt b ++ varsInStmt c+  Sequence a b    -> nub $ varsInStmt a ++ varsInStmt b+  Assert _ a      -> varsInExpr a+  Assume _ a      -> varsInExpr a+  Null            -> []++varsInExpr :: E a -> [([Name], Bool, String, String)] -- (path, isInput, type, init)+varsInExpr a = case a of+  Ref a     -> [varInfo a]+  Const _   -> []+  Add a b   -> varsInExpr a ++ varsInExpr b+  Sub a b   -> varsInExpr a ++ varsInExpr b+  Mul a _   -> varsInExpr a+  Div a _   -> varsInExpr a+  Mod a _   -> varsInExpr a+  Not a     -> varsInExpr a+  And a b   -> varsInExpr a ++ varsInExpr b+  Or  a b   -> varsInExpr a ++ varsInExpr b+  Eq  a b   -> varsInExpr a ++ varsInExpr b+  Lt  a b   -> varsInExpr a ++ varsInExpr b+  Gt  a b   -> varsInExpr a ++ varsInExpr b+  Le  a b   -> varsInExpr a ++ varsInExpr b+  Ge  a b   -> varsInExpr a ++ varsInExpr b+  Mux a b c -> varsInExpr a ++ varsInExpr b ++ varsInExpr c+

@@ -0,0 +1,86 @@+module Language.ImProve.Core+  ( E (..)+  , V (..)+  , Name+  , AllE (..)+  , NumE+  , Statement (..)+  ) where++import Data.Ratio++type Name = String++data V a = V Bool [Name] a++class AllE a where+  showConst :: a -> String+  showType  :: a -> String+  zero      :: (Name -> a -> m (V a)) -> a++instance AllE Bool where+  showConst a = case a of+    True  -> "1"+    False -> "0"+  showType _ = "int"+  zero = const False++instance AllE Int where+  showConst = show+  showType _ = "int"+  zero = const 0+  +instance AllE Float where+  showConst = show+  showType _ = "float"+  zero = const 0++class    AllE a => NumE a+instance NumE Int+instance NumE Float++data E a where+  Ref   :: AllE a => V a -> E a+  Const :: AllE a => a -> E a+  Add   :: NumE a => E a -> E a -> E a+  Sub   :: NumE a => E a -> E a -> E a+  Mul   :: NumE a => E a -> a -> E a+  Div   :: NumE a => 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    :: AllE a => E a -> E a -> E Bool+  Lt    :: NumE a => E a -> E a -> E Bool+  Gt    :: NumE a => E a -> E a -> E Bool+  Le    :: NumE a => E a -> E a -> E Bool+  Ge    :: NumE a => E a -> E a -> E Bool+  Mux   :: AllE a => E Bool -> E a -> E a -> E a++instance Show (E a) where show = undefined +instance Eq   (E a) where (==) = undefined++instance (Num a, AllE a, NumE a) => Num (E a) where+  (+) = Add+  (-) = Sub+  (*) = error "general multiplication not supported, use (*.)"+  negate a = 0 - a+  abs a = Mux (Lt a 0) (negate a) a+  signum a = Mux (Eq a 0) 0 $ Mux (Lt a 0) (-1) 1+  fromInteger = Const . fromInteger++instance Fractional (E Float) where+  (/) = error "general division not supported, use (/.)"+  recip a = 1 / a+  fromRational r = Const $ fromInteger (numerator r) / fromInteger (denominator r)++data Statement+  = AssignBool  (V Bool ) (E Bool )+  | AssignInt   (V Int  ) (E Int  )+  | AssignFloat (V Float) (E Float)+  | Branch      [Name] (E Bool) Statement Statement+  | Sequence    Statement Statement+  | Assert      [Name] (E Bool)+  | Assume      [Name] (E Bool)+  | Null+

@@ -0,0 +1,57 @@+-- | ImProve examples.+module Language.ImProve.Examples+  ( gcd'+  , gcdMain+  , gcdBuild+  ) where++import Language.ImProve++-- | 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)+gcd' a b = do+  a0 <- int "a0" 0  -- Copy of input 'a'.+  b0 <- int "b0" 0  -- Copy of input 'b'.+  a1 <- int "a1" 0  -- Working copy of 'a'.+  b1 <- int "b1" 0  -- Working copy of 'b'.++  -- A new input to process.+  if_ "startNew" (a /=. ref a0 ||. b /=. ref b0) $ do+    a0 <== a+    b0 <== b+    a1 <== a+    b1 <== b++  -- Reduce a1.+  if_ "reduceA" (ref a1 >. ref b1) $ do+    a1 <== ref a1 - ref b1++  -- Reduce b1.+  if_ "reduceB" (ref b1 >. ref a1) $ do+    b1 <== ref b1 - ref a1++  -- Done if a1 == b1.+  return (ref a1 ==. ref b1, ref a1)+++-- | A top level wrapper for gcd'.+gcdMain :: Stmt ()+gcdMain = do+  a <- input int "a"  -- Input variable 'a'.+  b <- input int "b"  -- Input variable 'b'.+  done   <- bool "done"   False  -- Variable signalling completion.+  result <- int  "result" 0      -- Result of GCD.++  -- Call gcd' in its own scope.  (Scopes prevent variable name collisions.)+  (done', result') <- scope "gcd" $ gcd' a b++  -- Bind the results to the output variables.+  done   <== done'+  result <== result'+++-- | Build the gcdMain code (i.e. gcd.c, gcd.h).+gcdBuild :: IO ()+gcdBuild = code "gcd" gcdMain+

@@ -0,0 +1,46 @@+-- | Building hierarchy from unstructured hierarchical paths.+module Language.ImProve.Tree+  ( Tree (..)+  , tree+  ) where++import Data.Function+import Data.List++data Tree a b+  = Branch a [Tree a b]+  | Leaf   a b++tree :: (Eq a, Ord a) => (b -> [a]) -> [b] -> [Tree a b]+tree path leaves = foldl mergeTrees [] [ singleTree (path leaf) leaf | leaf <- leaves ]++label :: Tree a b -> a+label (Branch a _) = a+label (Leaf   a _) = a++isBranch :: Tree a b -> Bool+isBranch (Branch _ _) = True+isBranch _ = False++singleTree :: [a] -> b -> Tree a b+singleTree [] _ = undefined+singleTree [a] b = Leaf a b+singleTree (a:b) c = Branch a [singleTree b c]++mergeTrees :: (Eq a, Ord a) => [Tree a b] -> Tree a b -> [Tree a b]+mergeTrees trees t@(Leaf _ _) = insertTree t trees+mergeTrees trees t@(Branch n branches) = case find' (\ t -> isBranch t && label t == n) trees of+    Nothing -> insertTree t trees+    Just (Branch n trees1, trees2) -> insertTree (Branch n (foldl mergeTrees trees1 branches)) trees2+    Just (Leaf _ _, _) -> undefined++insertTree :: Ord a => Tree a b -> [Tree a b] -> [Tree a b]+insertTree a b = insertBy (compare `on` label) a b++find' :: (a -> Bool) -> [a] -> Maybe (a, [a])+find' _ [] = Nothing+find' f (a:b) | f a = Just (a, b)+              | otherwise = do+  (found, rest) <- find' f b+  return (found, a : rest)+

@@ -0,0 +1,7 @@+module Language.ImProve.Verify (verify) where++import Language.ImProve.Core++verify :: Statement -> IO (Maybe Bool)+verify _ = putStrLn "verification not implemented yet" >> return Nothing+

@@ -1,9 +1,9 @@ name:    improve-version: 0.0.1+version: 0.0.2  category: Language -synopsis: A simple imperative programming language for embedded applications.+synopsis: An imperative, verifiable programming language for embedded applications.  description:     TODO@@ -26,6 +26,11 @@      exposed-modules:         Language.ImProve+        Language.ImProve.Code+        Language.ImProve.Core+        Language.ImProve.Examples+        Language.ImProve.Tree+        Language.ImProve.Verify      extensions: GADTs, FlexibleInstances