packages feed

improve 0.1.2 → 0.1.3

raw patch · 3 files changed

+69/−3 lines, 3 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

- Language.ImProve.Core: instance (Eq a) => Eq (V a)
+ Language.ImProve.Core: instance Eq a => Eq (V a)
+ Language.ImProve.Narrow: narrow :: Statement -> Statement
- Language.ImProve: (*.) :: (NumE a) => E a -> a -> E a
+ Language.ImProve: (*.) :: NumE a => E a -> a -> E a
- Language.ImProve: (/=.) :: (AllE a) => E a -> E a -> E Bool
+ Language.ImProve: (/=.) :: AllE a => E a -> E a -> E Bool
- Language.ImProve: (<.) :: (NumE a) => E a -> E a -> E Bool
+ Language.ImProve: (<.) :: NumE a => E a -> E a -> E Bool
- Language.ImProve: (<=.) :: (NumE a) => E a -> E a -> E Bool
+ Language.ImProve: (<=.) :: NumE a => E a -> E a -> E Bool
- Language.ImProve: (<==) :: (Assign a) => V a -> E a -> Stmt ()
+ Language.ImProve: (<==) :: Assign a => V a -> E a -> Stmt ()
- Language.ImProve: (==.) :: (AllE a) => E a -> E a -> E Bool
+ Language.ImProve: (==.) :: AllE a => E a -> E a -> E Bool
- Language.ImProve: (>.) :: (NumE a) => E a -> E a -> E Bool
+ Language.ImProve: (>.) :: NumE a => E a -> E a -> E Bool
- Language.ImProve: (>=.) :: (NumE a) => E a -> E a -> E Bool
+ Language.ImProve: (>=.) :: NumE a => E a -> E a -> E Bool
- Language.ImProve: class (AllE a) => NumE a
+ Language.ImProve: class AllE a => NumE a
- Language.ImProve: constant :: (AllE a) => a -> E a
+ Language.ImProve: constant :: AllE a => a -> E a
- Language.ImProve: global :: (AllE a) => (Name -> a -> Stmt (V a)) -> Path -> a -> V a
+ Language.ImProve: global :: AllE a => (Name -> a -> Stmt (V a)) -> Path -> a -> V a
- Language.ImProve: input :: (AllE a) => (Name -> a -> Stmt (V a)) -> Path -> E a
+ Language.ImProve: input :: AllE a => (Name -> a -> Stmt (V a)) -> Path -> E a
- Language.ImProve: limit :: (NumE a) => E a -> E a -> E a -> E a
+ Language.ImProve: limit :: NumE a => E a -> E a -> E a -> E a
- Language.ImProve: max_ :: (NumE a) => E a -> E a -> E a
+ Language.ImProve: max_ :: NumE a => E a -> E a -> E a
- Language.ImProve: maximum_ :: (NumE a) => [E a] -> E a
+ Language.ImProve: maximum_ :: NumE a => [E a] -> E a
- Language.ImProve: min_ :: (NumE a) => E a -> E a -> E a
+ Language.ImProve: min_ :: NumE a => E a -> E a -> E a
- Language.ImProve: minimum_ :: (NumE a) => [E a] -> E a
+ Language.ImProve: minimum_ :: NumE a => [E a] -> E a
- Language.ImProve: mux :: (AllE a) => E Bool -> E a -> E a -> E a
+ Language.ImProve: mux :: AllE a => E Bool -> E a -> E a -> E a
- Language.ImProve: ref :: (AllE a) => V a -> E a
+ Language.ImProve: ref :: AllE a => V a -> E a
- Language.ImProve.Core: class (AllE a) => NumE a
+ Language.ImProve.Core: class AllE a => NumE a
- Language.ImProve.Core: const' :: (AllE a) => a -> Const
+ Language.ImProve.Core: const' :: AllE a => a -> Const
- Language.ImProve.Core: pathName :: (PathName a) => a -> String
+ Language.ImProve.Core: pathName :: PathName a => a -> String
- Language.ImProve.Core: varInfo :: (AllE a) => V a -> VarInfo
+ Language.ImProve.Core: varInfo :: AllE a => V a -> VarInfo
- Language.ImProve.Core: zero :: (AllE a) => (Name -> a -> m (V a)) -> a
+ Language.ImProve.Core: zero :: AllE a => (Name -> a -> m (V a)) -> a

Files

+ Language/ImProve/Narrow.hs view
@@ -0,0 +1,61 @@+module Language.ImProve.Narrow (narrow) where++import Data.List+import Data.Maybe++import Language.ImProve.Core++narrow :: Statement -> Statement+narrow stmt = assumes+  where+  assumes = foldl Sequence Null [ Label lab $ Assume assume | (lab, opt) <- optimizations, assume <- opt stmt ]+  optimizations =+    [ ("constantAssigns", constantAssigns)+    ]++constantAssigns :: Statement -> [E Bool]+constantAssigns stmt = mapMaybe f1 $ stmtVars stmt+  where+  f1 :: VarInfo -> Maybe (E Bool)+  f1 info@(input, path, init)+    | input = Nothing+    | otherwise = do+      assigns <- lastConstAssign info stmt+      case (init, nub $ init : assigns) of+        (Bool _, [_, _]) -> Nothing+	(_, a) -> return $ foldl1 Or $ map f2 a+      where+      f2 :: Const -> E Bool+      f2 assign = case (init, assign) of+        (Bool  a, Bool  b) -> Eq (Ref (V input path a)) (Const b)+        (Int   a, Int   b) -> Eq (Ref (V input path a)) (Const b)+        (Float a, Float b) -> Eq (Ref (V input path a)) (Const b)+        _ -> undefined++lastConstAssign :: VarInfo -> Statement -> Maybe [Const]+lastConstAssign info a = do+  (_, a) <- lastConstAssign a+  return $ nub a+  where+  lastConstAssign :: Statement -> Maybe (Bool, [Const])+  lastConstAssign a = case a of+    AssignBool  v (Const a) | varInfo v == info -> Just (True, [const' a])+    AssignInt   v (Const a) | varInfo v == info -> Just (True, [const' a])+    AssignFloat v (Const a) | varInfo v == info -> Just (True, [const' a])+    AssignBool  v _ | varInfo v == info -> Nothing+    AssignInt   v _ | varInfo v == info -> Nothing+    AssignFloat v _ | varInfo v == info -> Nothing+    Branch _ a b -> do+      (aDone, a) <- lastConstAssign a+      (bDone, b) <- lastConstAssign b+      return (aDone && bDone, a ++ b)+    Sequence a b -> do+      (bDone, b) <- lastConstAssign b+      if bDone+        then return (True, b)+	else do+          (aDone, a) <- lastConstAssign a+          return (aDone, a ++ b)+    Label  _ a -> lastConstAssign a+    _ -> Just (False, [])+
Language/ImProve/Verify.hs view
@@ -7,17 +7,21 @@ import System.IO import Text.Printf +import Language.ImProve.Code import Language.ImProve.Core+import Language.ImProve.Narrow  -- | 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+  code "narrowing" narrowing   mapM_ (verifyProgram yices format maxK) $ trimAssertions program   where-  program = labelAssertions program'+  --XXX Not efficient.  Constraints will get added on every stage.  Only needed at the begining.+  narrowing = narrow program'+  program = labelAssertions $ Sequence narrowing program'   format = "verifying %-" ++ show (maximum [ length $ pathName path | path <- assertions program ]) ++ "s    "-  -- | Set of statements containing only one assertion. trimAssertions :: Statement -> [Statement]
improve.cabal view
@@ -1,5 +1,5 @@ name:    improve-version: 0.1.2+version: 0.1.3  category: Language, Formal Methods, Embedded @@ -33,6 +33,7 @@         Language.ImProve.Code         Language.ImProve.Core         Language.ImProve.Examples+        Language.ImProve.Narrow         Language.ImProve.Tree         Language.ImProve.Verify