improve 0.0.4 → 0.0.5

raw patch · 5 files changed

+51/−20 lines, 5 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Language/ImProve.hs +24/−7
• Language/ImProve/Code.hs +2/−1
• Language/ImProve/Core.hs +2/−0
• Language/ImProve/Verify.hs +22/−11
• improve.cabal +1/−1

@@ -45,10 +45,11 @@   , mux   -- ** Lookups   , linear-  -- * Hierarchical Scope-  , scope   -- * Statements   , Stmt+  -- ** Hierarchical Scope and Annotations+  , scope+  , annotate   -- ** Variable Declarations   , bool   , bool'@@ -215,14 +216,30 @@  -- | Creates a hierarchical scope. scope :: Name -> Stmt a -> Stmt a-scope name (Stmt f0) = Stmt f1-  where-  f1 (path, statement) = (a, (path, statement1))-    where-    (a, (_, statement1)) = f0 (path ++ [name], statement)+scope name stmt = do+  (path0, stmt0) <- get+  put (path0 ++ [name], stmt0)+  a <- stmt+  (_, stmt1) <- get+  put (path0, stmt1)+  return a++-- | Add an annotation to a statement.  Useful for requirement trace tags.+annotate :: Name -> Stmt a -> Stmt a+annotate name stmt = do+  (path0, stmt0) <- get+  put (path0, Null)+  a <- stmt+  (_, stmt1) <- get+  put (path0, stmt0)+  statement $ Annotate name stmt1+  return a    get :: Stmt ([Name], Statement) get = Stmt $ \ a -> (a, a)++put :: ([Name], Statement) -> Stmt ()+put s = Stmt $ \ _ -> ((), s)  getPath :: Stmt [Name] getPath = do

@@ -34,6 +34,7 @@   Sequence a b -> codeStmt a ++ codeStmt b   Assert path a -> "// assert " ++ pathName path ++ "\nassert(" ++ codeExpr a ++ ");\n"   Assume path a -> "// assume " ++ pathName path ++ "\nassert(" ++ codeExpr a ++ ");\n"+  Annotate name a -> "// annotate " ++ name ++ "\n" ++ indent (codeStmt a)   Null -> ""  codeExpr :: E a -> String@@ -59,7 +60,7 @@   group a = "(" ++ intercalate " " a ++ ")"  indent :: String -> String-indent = unlines . map ("  " ++) . lines+indent = unlines . map ("    " ++) . lines  indent' :: String -> String indent' a = case lines a of

@@ -97,6 +97,7 @@   | Sequence    Statement Statement   | Assert      Path (E Bool)   | Assume      Path (E Bool)+  | Annotate    Name Statement   | Null  data Const@@ -120,6 +121,7 @@   Sequence a b    -> nub $ stmtVars a ++ stmtVars b   Assert _ a      -> exprVars a   Assume _ a      -> exprVars a+  Annotate _ a    -> stmtVars a   Null            -> []  -- Information about all of an expressions's variables.

@@ -26,6 +26,7 @@                ++ [ 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 ]+  Annotate name a -> [ Annotate name a | a <- trimAssertions a ]   a -> [a]  -- | Remove all assertions.@@ -34,6 +35,7 @@   Assert _ _ -> Null   Sequence a b -> Sequence (removeAssertions a) (removeAssertions b)   Branch path cond a b -> Branch path cond (removeAssertions a) (removeAssertions b)+  Annotate name a -> Annotate name $ removeAssertions a   a -> a  -- | Paths of all assertions.@@ -42,6 +44,7 @@   Assert path _  -> [path]   Sequence a b   -> assertions a ++ assertions b   Branch _ _ a b -> assertions a ++ assertions b+  Annotate _ a   -> assertions a   _ -> []  -- | Trim all unneeded stuff from a program.@@ -140,6 +143,12 @@     evalStmt (AND [enabled, NOT a]) onFalse     env2 <- get     put env2 { trace = Branch' (pathName path) b (reverse $ trace env1) (reverse $ trace env2) : trace env0 }+  Annotate name a -> do+    env0 <- get+    put env0 { trace = [] }+    evalStmt enabled a+    env1 <- get+    put env1 { trace = Annotate' name (reverse $ trace env1) : trace env0 }   where   assign :: AllE a => V a -> E a -> Y ()   assign a b = do@@ -241,12 +250,13 @@   }  data Trace-  = Init'   Name Var-  | Cycle'  Int-  | Input'  Name Var-  | Assign' Name Var-  | Assert' Name Var-  | Branch' Name Var [Trace] [Trace] +  = Init'     Name Var+  | Cycle'    Int+  | Input'    Name Var+  | Assign'   Name Var+  | Assert'   Name Var+  | Branch'   Name Var [Trace] [Trace] +  | Annotate' Name [Trace]  addVar' :: VarInfo -> Y String addVar' v = do@@ -298,8 +308,8 @@   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"+      Just value -> "initialize " ++ path ++ " <== " ++ value ++ "\n"+    Cycle' n -> "\nstep " ++ show n ++ "\n"     Input' path var -> case lookup var table of       Nothing -> ""       Just value -> "input " ++ path ++ " <== " ++ value ++ "\n"@@ -311,10 +321,11 @@       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)+      Just "true"  -> "ifelse " ++ path ++ " true\n"  ++ indent (concatMap f onTrue)+      Just "false" -> "ifelse " ++ path ++ " false\n" ++ indent (concatMap f onFalse)       _ -> ""+    Annotate' name traces -> "annotate " ++ name ++ "\n" ++ indent (concatMap f traces)  indent :: String -> String-indent = unlines . map ("  " ++) . lines+indent = unlines . map ("    " ++) . lines 

@@ -1,5 +1,5 @@ name:    improve-version: 0.0.4+version: 0.0.5  category: Language