improve 0.1.3 → 0.1.4

raw patch · 4 files changed

+13/−12 lines, 4 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Language/ImProve/Code.hs +9/−9
• Language/ImProve/Core.hs +1/−1
• Language/ImProve/Verify.hs +2/−1
• improve.cabal +1/−1

@@ -15,7 +15,7 @@     ++ "#include <assert.h>\n\n"     ++ codeVariables True scope ++ "\n"     ++ "void " ++ name ++ "()\n{\n"-    ++ indent (codeStmt stmt)+    ++ indent (codeStmt [] stmt)     ++ "}\n\n"   writeFile (name ++ ".h") $        "/* Generated by ImProve. */\n\n"@@ -26,17 +26,17 @@     [] -> error "program contains no usefull statements"     a  -> T.Branch (name ++ "_variables") a -  codeStmt :: Statement -> String-  codeStmt a = case a of+  codeStmt :: [Name] -> Statement -> String+  codeStmt path a = case a of     AssignBool  a b -> name ++ "_variables." ++ pathName a ++ " = " ++ codeExpr b ++ ";\n"     AssignInt   a b -> name ++ "_variables." ++ pathName a ++ " = " ++ codeExpr b ++ ";\n"     AssignFloat a b -> name ++ "_variables." ++ pathName 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 a -> "assert(" ++ codeExpr a ++ ");\n"-    Assume a -> "assert(" ++ codeExpr a ++ ");\n"-    Label  name a -> "/*" ++ name ++ "*/\n" ++ indent (codeStmt a)+    Branch a b Null -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt path b) ++ "}\n"+    Branch a b c    -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt path b) ++ "}\nelse {\n" ++ indent (codeStmt path c) ++ "}\n"+    Sequence a b -> codeStmt path a ++ codeStmt path b+    Assert a -> "assert((" ++ show (intercalate "." path) ++ ", " ++ codeExpr a ++ "));\n"+    Assume a -> "assert((" ++ show (intercalate "." path) ++ ", " ++ codeExpr a ++ "));\n"+    Label  name a -> "/*" ++ name ++ "*/\n" ++ indent (codeStmt (path ++ [name]) a)     Null -> ""      codeExpr :: E a -> String

@@ -100,7 +100,7 @@   = Bool  Bool   | Int   Int   | Float Float-  deriving (Eq, Ord)+  deriving (Show, Eq, Ord)  type VarInfo = (Bool, Path, Const) 

@@ -122,7 +122,7 @@   AssignBool  a b -> if elem (varInfo a) required then nub $ varInfo a : exprVars b ++ required else required   AssignInt   a b -> if elem (varInfo a) required then nub $ varInfo a : exprVars b ++ required else required   AssignFloat a b -> if elem (varInfo a) required then nub $ varInfo a : exprVars b ++ required else required-  Branch a b c    -> if any (flip elem $ modifiedVars b ++ modifiedVars c) required+  Branch a b c    -> if any (flip elem $ modifiedVars b ++ modifiedVars c) required || (not $ null $ requiredVars b []) || (not $ null $ requiredVars c [])     then nub $ exprVars a ++ requiredVars b (requiredVars c required)     else required   Sequence a b    -> requiredVars a (requiredVars b required)@@ -153,6 +153,7 @@   return ()   where   program = trimProgram program'+  --program = program'   name = pathName $ head' "a1" $ assertions program  head' msg a = if null a then error msg else head a

@@ -1,5 +1,5 @@ name:    improve-version: 0.1.3+version: 0.1.4  category: Language, Formal Methods, Embedded