improve 0.0.2 → 0.0.3

raw patch · 6 files changed

+458/−89 lines, 6 filesdep +yicesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: yices

API changes (from Hackage documentation)

Files

• Language/ImProve.hs +4/−2
• Language/ImProve/Code.hs +37/−63
• Language/ImProve/Core.hs +73/−15
• Language/ImProve/Examples.hs +24/−3
• Language/ImProve/Verify.hs +315/−2
• improve.cabal +5/−4

@@ -329,8 +329,10 @@ if_ name cond stmt = ifelse name cond stmt $ return ()  -- | Verify a program.-verify :: Stmt () -> IO (Maybe Bool)-verify program = V.verify $ snd $ evalStmt [] program+--+-- ^ verify pathToYices maxK program+verify :: FilePath -> Int -> Stmt () -> IO ()+verify yices maxK program = V.verify yices maxK $ snd $ evalStmt [] program  -- | Generate C code. code :: Name -> Stmt () -> IO ()

@@ -22,43 +22,37 @@     ++ 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+  [scope] = tree (\ (_, path, _) -> path) $ stmtVars stmt  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"+  AssignBool  a b -> pathName a ++ " = " ++ codeExpr b ++ ";\n"+  AssignInt   a b -> pathName a ++ " = " ++ codeExpr b ++ ";\n"+  AssignFloat a b -> pathName a ++ " = " ++ codeExpr b ++ ";\n"+  Branch path a b Null -> "// if_ "    ++ pathName path ++ "\nif (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt b) ++ "}\n"+  Branch path a b c    -> "// ifelse " ++ pathName 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"+  Assert path a -> "// assert " ++ pathName path ++ "\nassert(" ++ codeExpr a ++ ");\n"+  Assume path a -> "// assume " ++ pathName 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]+  Ref a     -> pathName a+  Const a   -> showConst $ const' a+  Add a b   -> group [codeExpr a, "+", codeExpr b]+  Sub a b   -> group [codeExpr a, "-", codeExpr b]+  Mul a b   -> group [codeExpr a, "*", showConst (const' b)]+  Div a b   -> group [codeExpr a, "/", showConst (const' b)]+  Mod a b   -> group [codeExpr a, "%", showConst (const' 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@@ -72,47 +66,27 @@   [] -> []   (a:b) -> a ++ "\n" ++ indent (unlines b) -codeVariables :: Bool -> (Tree Name ([Name], Bool, String, String)) -> String+codeVariables :: Bool -> (Tree Name (Bool, Path, Const)) -> 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 "")+    Leaf name (input, _, init) -> printf "%-5s %-25s;%s\n" (showConstType init) 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)+    Leaf name (_, _, init) -> printf "%-15s  // %s\n" (showConst init) name -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            -> []+showConst :: Const -> String+showConst a = case a of+  Bool  True  -> "1"+  Bool  False -> "0"+  Int   a     -> show a+  Float a     -> show a -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+showConstType :: Const -> String+showConstType a = case a of+  Bool  _ -> "int"+  Int   _ -> "int"+  Float _ -> "float" 

@@ -2,38 +2,53 @@   ( E (..)   , V (..)   , Name+  , Path+  , PathName (..)   , AllE (..)   , NumE+  , Const (..)   , Statement (..)+  , VarInfo+  , varInfo+  , stmtVars+  , exprVars   ) where +import Data.List import Data.Ratio  type Name = String -data V a = V Bool [Name] a+type Path = [Name] +data V a = V Bool [Name] a deriving Eq++class    PathName a         where pathName :: a -> String+instance PathName Path      where pathName = intercalate "."+instance PathName (V a)     where pathName (V _ path _) = pathName path+instance PathName VarInfo   where pathName (_, path, _) = pathName path+instance PathName Statement where+  pathName a = case a of+    Branch p _ _ _ -> pathName p+    Assert p _     -> pathName p+    Assume p _     -> pathName p+    _ -> undefined+ class AllE a where-  showConst :: a -> String-  showType  :: a -> String-  zero      :: (Name -> a -> m (V a)) -> a+  zero   :: (Name -> a -> m (V a)) -> a+  const' :: a -> Const  instance AllE Bool where-  showConst a = case a of-    True  -> "1"-    False -> "0"-  showType _ = "int"   zero = const False+  const' = Bool  instance AllE Int where-  showConst = show-  showType _ = "int"   zero = const 0+  const' = Int    instance AllE Float where-  showConst = show-  showType _ = "float"   zero = const 0+  const' = Float  class    AllE a => NumE a instance NumE Int@@ -78,9 +93,52 @@   = AssignBool  (V Bool ) (E Bool )   | AssignInt   (V Int  ) (E Int  )   | AssignFloat (V Float) (E Float)-  | Branch      [Name] (E Bool) Statement Statement+  | Branch      Path (E Bool) Statement Statement   | Sequence    Statement Statement-  | Assert      [Name] (E Bool)-  | Assume      [Name] (E Bool)+  | Assert      Path (E Bool)+  | Assume      Path (E Bool)   | Null++data Const+  = Bool  Bool+  | Int   Int+  | Float Float+  deriving Eq++type VarInfo = (Bool, Path, Const)++varInfo :: AllE a => V a -> VarInfo+varInfo (V input path init) = (input, path, const' init)++-- Information about all of a program's variables.+stmtVars :: Statement -> [VarInfo]+stmtVars a = case a of+  AssignBool  a b -> nub $ varInfo a : exprVars b+  AssignInt   a b -> nub $ varInfo a : exprVars b+  AssignFloat a b -> nub $ varInfo a : exprVars b+  Branch _ a b c  -> nub $ exprVars a ++ stmtVars b ++ stmtVars c+  Sequence a b    -> nub $ stmtVars a ++ stmtVars b+  Assert _ a      -> exprVars a+  Assume _ a      -> exprVars a+  Null            -> []++-- Information about all of an expressions's variables.+exprVars :: E a -> [VarInfo]+exprVars a = case a of+  Ref a     -> [varInfo a]+  Const _   -> []+  Add a b   -> exprVars a ++ exprVars b+  Sub a b   -> exprVars a ++ exprVars b+  Mul a _   -> exprVars a+  Div a _   -> exprVars a+  Mod a _   -> exprVars a+  Not a     -> exprVars a+  And a b   -> exprVars a ++ exprVars b+  Or  a b   -> exprVars a ++ exprVars b+  Eq  a b   -> exprVars a ++ exprVars b+  Lt  a b   -> exprVars a ++ exprVars b+  Gt  a b   -> exprVars a ++ exprVars b+  Le  a b   -> exprVars a ++ exprVars b+  Ge  a b   -> exprVars a ++ exprVars b+  Mux a b c -> exprVars a ++ exprVars b ++ exprVars c 

@@ -2,7 +2,9 @@ module Language.ImProve.Examples   ( gcd'   , gcdMain-  , gcdBuild+  , buildGCD+  , counter+  , verifyCounter   ) where  import Language.ImProve@@ -52,6 +54,25 @@   -- | Build the gcdMain code (i.e. gcd.c, gcd.h).-gcdBuild :: IO ()-gcdBuild = code "gcd" gcdMain+buildGCD :: IO ()+buildGCD = code "gcd" gcdMain++++-- | A rolling counter verification example.+counter :: Stmt ()+counter = do+  -- The counter variable.+  counter <- int "counter" 0++  -- Specification.+  assert "GreaterThanOrEqualTo0" $ ref counter >=. 0+  assert "LessThan10"            $ ref counter <.  10++  -- Implementation.+  ifelse "ResetCounter" (ref counter ==. 10) (counter <== 0) (incr counter)++-- Verify the 'counter' example.+verifyCounter :: IO ()+verifyCounter = verify "yices" 20 counter 

@@ -1,7 +1,320 @@ module Language.ImProve.Verify (verify) where +import Control.Monad.State hiding (State)+import Math.SMT.Yices.Pipe+import Math.SMT.Yices.Syntax+import System.IO+import Text.Printf+ import Language.ImProve.Core -verify :: Statement -> IO (Maybe Bool)-verify _ = putStrLn "verification not implemented yet" >> return Nothing+-- | Verify a program with k-induction.+verify :: FilePath -> Int -> Statement -> IO ()+verify _ maxK _ | maxK < 1 = error "max k can not be less than 1"+verify yices maxK program = do+  mapM_ (verifyProgram yices format maxK) $ trimAssertions program+  where+  format = "verifying %-" ++ show (maximum [ length $ pathName path | path <- assertions program ]) ++ "s    "++-- | Set of statements containing only one assertion.+trimAssertions :: Statement -> [Statement]+trimAssertions program = [ a | a <- trimAssertions' program, length (assertions a) == 1 ]++trimAssertions' :: Statement -> [Statement]+trimAssertions' a = case a of+  Sequence a b -> [ Sequence a (removeAssertions b) | a <- trimAssertions' a ]+               ++ [ Sequence (removeAssertions a) b | b <- trimAssertions' b ]+  Branch path cond a b -> [ Branch path cond a (removeAssertions b) | a <- trimAssertions' a ]+                       ++ [ Branch path cond (removeAssertions a) b | b <- trimAssertions' b ]+  a -> [a]++-- | Remove all assertions.+removeAssertions :: Statement -> Statement+removeAssertions a = case a of+  Assert _ _ -> Null+  Sequence a b -> Sequence (removeAssertions a) (removeAssertions b)+  Branch path cond a b -> Branch path cond (removeAssertions a) (removeAssertions b)+  a -> a++-- | Paths of all assertions.+assertions :: Statement -> [Path]+assertions a = case a of+  Assert path _  -> [path]+  Sequence a b   -> assertions a ++ assertions b+  Branch _ _ a b -> assertions a ++ assertions b+  _ -> []++-- | Trim all unneeded stuff from a program.+trimProgram :: Statement -> Statement+trimProgram = id --XXX++-- | Verify a trimmed program.+verifyProgram :: FilePath -> String -> Int -> Statement -> IO ()+verifyProgram yices format maxK program' = do+  printf format name+  hFlush stdout+  env0 <- initEnv program+  execStateT (check yices name maxK program env0 1) env0+  return ()+  where+  program = trimProgram program'+  name = pathName $ head' "a1" $ assertions program++head' msg a = if null a then error msg else head a++data Result = Pass | Fail [ExpY] | Problem++-- | k-induction.+check :: FilePath -> Name -> Int -> Statement -> Env -> Int -> Y ()+check yices name maxK program env0 k = do+  addTrace $ Cycle' $ k - 1+  inputs program+  evalStmt (LitB True) program+  resultBasis <- checkBasis yices program env0+  case resultBasis of+    Fail a  -> liftIO (printf "FAILED: disproved basis in k = %d (see trace)\n" k) >> writeTrace name a+    Problem -> error "Verify.check1"+    Pass -> do+      resultStep <- checkStep yices+      case resultStep of+        Fail a | k < maxK  -> check yices name maxK program env0 (k + 1)+               | otherwise -> liftIO (printf "inconclusive: unable to proved step up to max k = %d (see trace)\n" k) >> writeTrace name a+        Problem -> error "Verify.check2"+        Pass    -> liftIO $ printf "passed: proved step in k = %d\n" k+        +-- | Check induction step.+checkStep :: FilePath -> Y Result+checkStep yices = do+  env <- get+  r <- liftIO $ quickCheckY' yices [] $ reverse (cmds env) ++ [ASSERT $ NOT $ head' "a2" $ asserts env] ++ [CHECK]+  return $ result r++-- | Check induction basis.+checkBasis :: FilePath -> Statement -> Env -> Y Result+checkBasis yices program env0 = do+  env <- get+  r <- liftIO $ quickCheckY' yices [] $ reverse (cmds env)+          ++ [ASSERT $ NOT $ AND $ asserts env]+          ++ [ ASSERT $ VarE (var env0 a) := evalConst' c | a@(input, _, c) <- stmtVars program, not input ]+          ++ [CHECK]+  return $ result r++-- | Insert new input variables.+inputs :: Statement -> Y ()+inputs program = sequence_ [ addVar' a >>= addTrace . Input' (pathName path) | a@(input, path, _) <- stmtVars program, input ]++result :: ResY -> Result+result a = case a of+  Sat a   -> Fail a+  UnSat _ -> Pass+  InCon _ -> Problem+  _ -> error $ "unexpected yices results: " ++ show a+++evalStmt :: ExpY -> Statement -> Y ()+evalStmt enabled a = case a of+  Null -> return ()+  Sequence a b -> evalStmt enabled a >> evalStmt enabled b+  AssignBool  a b -> assign a b+  AssignInt   a b -> assign a b+  AssignFloat a b -> assign a b+  Assert path a -> do+    a <- evalExpr a+    b <- newBoolVar+    addCmd $ ASSERT (VarE b := (enabled :=> a))+    env <- get+    put env { asserts = VarE b : asserts env }+    addTrace $ Assert' (pathName path) b+  Assume _ a -> do+    a <- evalExpr a+    addCmd $ ASSERT (enabled :=> a)+  Branch path a onTrue onFalse -> do+    a <- evalExpr a+    b <- newBoolVar+    addCmd $ ASSERT (VarE b := a)+    env0 <- get+    put env0 { trace = [] }+    evalStmt (AND [enabled, a]) onTrue+    env1 <- get+    put env1 { trace = [] }+    evalStmt (AND [enabled, NOT a]) onFalse+    env2 <- get+    put env2 { trace = Branch' (pathName path) b (reverse $ trace env1) (reverse $ trace env2) : trace env0 }+  where+  assign :: AllE a => V a -> E a -> Y ()+  assign a b = do+    b <- evalExpr b+    aPrev <- getVar a+    aNext <- addVar a+    addCmd $ ASSERT (VarE aNext := IF enabled b (VarE aPrev))+    addTrace $ Assign' (pathName a) aNext++evalExpr :: AllE a => E a -> Y ExpY+evalExpr a = case a of+  Ref a -> getVar a >>= return . VarE+  Const a -> return $ evalConst a+  Add a b ->  do+    a <- evalExpr a+    b <- evalExpr b+    return $ a :+: b+  Sub a b ->  do+    a <- evalExpr a+    b <- evalExpr b+    return $ a :-: b+  Mul a b ->  do+    a <- evalExpr a+    return $ a :*: evalConst b+  Div a b -> do+    a <- evalExpr a+    return $ op a $ evalConst b+    where+    op = case const' b of+      Bool  _ -> undefined+      Int   _ -> DIV+      Float _ -> (:/:)+  Mod a b -> do+    a <- evalExpr a+    return $ MOD a $ evalConst b+  Not a -> evalExpr a >>= return . NOT+  And a b -> do+    a <- evalExpr a+    b <- evalExpr b+    return $ AND [a, b]+  Or a b -> do+    a <- evalExpr a+    b <- evalExpr b+    return $ OR [a, b]+  Eq a b -> do  +    a <- evalExpr a+    b <- evalExpr b+    return $ a := b+  Lt a b -> do  +    a <- evalExpr a+    b <- evalExpr b+    return $ a :< b+  Gt a b -> do  +    a <- evalExpr a+    b <- evalExpr b+    return $ a :> b+  Le a b -> do  +    a <- evalExpr a+    b <- evalExpr b+    return $ a :<= b+  Ge a b -> do  +    a <- evalExpr a+    b <- evalExpr b+    return $ a :>= b+  Mux a b c -> do+    a <- evalExpr a+    b <- evalExpr b+    c <- evalExpr c+    return $ IF a b c++evalConst :: AllE a => a -> ExpY+evalConst = evalConst' . const'++evalConst' :: Const -> ExpY+evalConst' a = case a of+  Bool  a -> LitB a+  Int   a -> LitI $ fromIntegral a+  Float a -> LitR $ toRational a++type Y = StateT Env IO++type Var = String++data Env = Env+  { nextId    :: Int+  , var       :: VarInfo -> Var+  , cmds      :: [CmdY]  -- Commands and variable declarations in reverse order.+  , asserts   :: [ExpY]  -- Assumes 1 assert in a program under verification.+  , trace     :: [Trace] -- Program trace in reverse order.+  }+ +initEnv :: Statement -> IO Env+initEnv program = execStateT (sequence_ [ addVar' a >>= addTrace . Init' (pathName path) | a@(input, path, _) <- stmtVars program, not input ]) Env+  { nextId  = 0+  , var     = \ v -> error $ "variable not found in environment: " ++ pathName v+  , cmds    = []+  , asserts = []+  , trace   = []+  }++data Trace+  = Init'   Name Var+  | Cycle'  Int+  | Input'  Name Var+  | Assign' Name Var+  | Assert' Name Var+  | Branch' Name Var [Trace] [Trace] ++addVar' :: VarInfo -> Y String+addVar' v = do+  env <- get+  let name = printf "n%d" $ nextId env+  put env { nextId = nextId env + 1, var = \ a -> if a == v then name else var env a, cmds = DEFINE (name, VarT typ) Nothing : cmds env }+  return name+  where+  typ = case v of+    (_, _, Bool  _) -> "bool"+    (_, _, Int   _) -> "int"+    (_, _, Float _) -> "real"++addVar :: AllE a => V a -> Y String+addVar = addVar' . varInfo++-- | Creates a new boolean variable.  Use for assertions.+newBoolVar :: Y String+newBoolVar = do+  env <- get+  let name = printf "n%d" $ nextId env+  put env { nextId = nextId env + 1, cmds = DEFINE (name, VarT "bool") Nothing : cmds env }+  return name++addCmd :: CmdY -> Y ()+addCmd cmd = do+  env <- get+  put env { cmds = cmd : cmds env }++addTrace :: Trace -> Y ()+addTrace t = do+  env <- get+  put env { trace = t : trace env }++getVar :: AllE a => V a -> Y String+getVar v = do+  env <- get+  return $ var env $ varInfo v++writeTrace :: String -> [ExpY] -> Y ()+writeTrace name table' = do+  env <- get+  liftIO $ writeFile (name ++ ".trace") $ concatMap f $ reverse $ trace env+  where+  table = [ (n, if v then "true" else "false") | VarE n := LitB v <- table' ]+       ++ [ (n, show v) | VarE n := LitI v <- table' ]+       ++ [ (n, show v) | VarE n := LitR v <- table' ]+  f :: Trace -> String+  f a = case a of+    Init' path var -> case lookup var table of+      Nothing -> ""+      Just value -> "initialize " ++ path ++ " := " ++ value ++ "\n"+    Cycle' n -> "cycle " ++ show n ++ "\n"+    Input' path var -> case lookup var table of+      Nothing -> ""+      Just value -> "input " ++ path ++ " <== " ++ value ++ "\n"+    Assign' path var -> case lookup var table of+      Nothing -> ""+      Just value -> path ++ " <== " ++ value ++ "\n"+    Assert' path var -> case lookup var table of+      Just "true"  -> "assertion passed: " ++ path ++ "\n"+      Just "false" -> "assertion FAILED: " ++ path ++ "\n"+      _ -> ""+    Branch' path cond onTrue onFalse -> case lookup cond table of+      Just "true"  -> "branch true: "  ++ path ++ "\n" ++ indent (concatMap f onTrue)+      Just "false" -> "branch false: " ++ path ++ "\n" ++ indent (concatMap f onFalse)+      _ -> ""++indent :: String -> String+indent = unlines . map ("  " ++) . lines 

@@ -1,5 +1,5 @@ name:    improve-version: 0.0.2+version: 0.0.3  category: Language @@ -21,8 +21,9 @@  library     build-depends:-        base       >= 4.2     && < 5,-        mtl        >= 1.1.0.1 && < 1.2+        base  >= 4.2     && < 5,+        mtl   >= 1.1.0.1 && < 1.2,+        yices >= 0.0.0.7 && < 0.0.1      exposed-modules:         Language.ImProve@@ -32,7 +33,7 @@         Language.ImProve.Tree         Language.ImProve.Verify -    extensions: GADTs, FlexibleInstances+    extensions: GADTs, FlexibleInstances, TypeSynonymInstances      ghc-options: -W