improve 0.0.8 → 0.0.9

raw patch · 4 files changed

+54/−49 lines, 4 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• Language/ImProve.hs +27/−22
• Language/ImProve/Examples.hs +24/−24
• Language/ImProve/Verify.hs +2/−2
• improve.cabal +1/−1

@@ -52,7 +52,7 @@ /Statement Labels/  @-hello: {                  'label' \"hello\" $ do+hello: {                  \"hello\" '-:' do     a();                      a     b();                      b }@@ -146,7 +146,7 @@   , or_   , any_   , all_-  , imply+  , (-->)   -- ** Equality and Comparison   , (==.)   , (/=.)@@ -171,9 +171,9 @@   , linear   -- * Statements   , Stmt-  -- ** Hierarchical Scope and Annotations-  , scope-  , label+  -- ** Statement Labeling and Hierarchical Scope+  , (-:)+  , (!)   -- ** Variable Declarations   , bool   , bool'@@ -209,7 +209,8 @@ infix  4 ==., /=., <., <=., >., >=. infixl 3 &&. infixl 2 ||.-infixr 1 <==+infixr 1 -->+infixr 0 <==, -:, !  -- | True term. true :: E Bool@@ -252,8 +253,8 @@ any_ f a = or_ $ map f a  -- Logical implication (if a then b).-imply :: E Bool -> E Bool -> E Bool -imply a b = not_ a ||. b+(-->) :: E Bool -> E Bool -> E Bool +a --> b = not_ a ||. b  -- | Equal. (==.) :: AllE a => E a -> E a -> E Bool@@ -338,28 +339,30 @@ mux :: AllE a => E Bool -> E a -> E a -> E a mux = Mux --- | Creates a hierarchical scope for variable names.-scope :: Name -> Stmt a -> Stmt a-scope name stmt = do+-- | Labels a statement.+--   Labels are used in counter examples to trace the program execution.+--   And assertion names, and hence counter example trace file names, are produce from labels.+(-:) :: Name -> Stmt a -> Stmt a+name -: stmt = do   (path0, stmt0) <- get-  put (path0 ++ [name], stmt0)+  put (path0, Null)   a <- stmt   (_, stmt1) <- get-  put (path0, stmt1)+  put (path0, stmt0)+  statement $ Label name stmt1   return a --- | Labels a statement.  Labels are used in counter examples to trace the program execution.---   And assertion names, and hence counter example file names, are produce from labels.-label :: Name -> Stmt a -> Stmt a-label name stmt = do+-- | Creates a new hierarcical scope for variable names.+(!) :: Name -> Stmt a -> Stmt a+name ! stmt = do   (path0, stmt0) <- get-  put (path0, Null)+  put (path0 ++ [name], stmt0)   a <- stmt   (_, stmt1) <- get-  put (path0, stmt0)-  statement $ Label name stmt1+  put (path0, stmt1)   return a-  ++ get :: Stmt ([Name], Statement) get = Stmt $ \ a -> (a, a) @@ -452,8 +455,10 @@ assert = statement . Assert  -- | Declare an assumption condition is true.+--   Assumptions expressions must contain variables directly or indirectly related+--   to the assertion under verification, otherwise they will be ignored. assume :: E Bool -> Stmt ()-assume = statement . Assume+assume a = statement $ Assume a  -- | Conditional if-else. ifelse :: E Bool -> Stmt () -> Stmt () -> Stmt ()

@@ -25,18 +25,18 @@   b1 <- int "b1" 0  -- Working copy of 'b'.    -- A new input to process.-  label "startNew" $ if_ (a /=. ref a0 ||. b /=. ref b0) $ do+  "startNew" -: if_ (a /=. ref a0 ||. b /=. ref b0) $ do     a0 <== a     b0 <== b     a1 <== a     b1 <== b    -- Reduce a1.-  label "reduceA" $ if_ (ref a1 >. ref b1) $ do+  "reduceA" -: if_ (ref a1 >. ref b1) $ do     a1 <== ref a1 - ref b1    -- Reduce b1.-  label "reduceB" $ if_ (ref b1 >. ref a1) $ do+  "reduceB" -: if_ (ref b1 >. ref a1) $ do     b1 <== ref b1 - ref a1    -- Done if a1 == b1.@@ -52,7 +52,7 @@   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+  (done', result') <- "gcd" ! gcd' a b    -- Bind the results to the output variables.   done   <== done'@@ -72,8 +72,8 @@   counter <- int "counter" 0    -- Specification.-  label "GreaterThanOrEqualTo0" $ assert $ ref counter >=. 0-  label "LessThan10"            $ assert $ ref counter <.  10+  "GreaterThanOrEqualTo0" -: assert $ ref counter >=. 0+  "LessThan10"            -: assert $ ref counter <.  10    -- Implementation.   ifelse (ref counter ==. 10) (counter <== 0) (counter <== ref counter + 1)@@ -93,25 +93,25 @@ arbiterSpec (requestA, requestB, requestC) (grantA, grantB, grantC) = do    -- Mutual exclusion.  At most, only one requester granted at a time.-  label "OneHot" $ assert $      grantA &&. not_ grantB &&. not_ grantC-                        ||. not_ grantA &&.      grantB &&. not_ grantC-                        ||. not_ grantA &&. not_ grantB &&.      grantC-                        ||. not_ grantA &&. not_ grantB &&. not_ grantC+  "OneHot" -: assert $      grantA &&. not_ grantB &&. not_ grantC+                   ||. not_ grantA &&.      grantB &&. not_ grantC+                   ||. not_ grantA &&. not_ grantB &&.      grantC+                   ||. not_ grantA &&. not_ grantB &&. not_ grantC      -- No grants without requests.-  label "NotRequestedA" $ assert $ imply (not_ requestA) (not_ grantA)-  label "NotRequestedB" $ assert $ imply (not_ requestB) (not_ grantB)-  label "NotRequestedC" $ assert $ imply (not_ requestC) (not_ grantC)+  "NotRequestedA" -: assert $ not_ requestA --> not_ grantA+  "NotRequestedB" -: assert $ not_ requestB --> not_ grantB+  "NotRequestedC" -: assert $ not_ requestC --> not_ grantC    -- Grants to single requests.-  label "OnlyRequestA" $ assert $ imply (     requestA &&. not_ requestB &&. not_ requestC) grantA-  label "OnlyRequestB" $ assert $ imply (not_ requestA &&.      requestB &&. not_ requestC) grantB-  label "OnlyRequestC" $ assert $ imply (not_ requestA &&. not_ requestB &&.      requestC) grantC+  "OnlyRequestA" -: assert $ (     requestA &&. not_ requestB &&. not_ requestC) --> grantA+  "OnlyRequestB" -: assert $ (not_ requestA &&.      requestB &&. not_ requestC) --> grantB+  "OnlyRequestC" -: assert $ (not_ requestA &&. not_ requestB &&.      requestC) --> grantC    -- Priority.-  label "Highest" $ assert $ imply requestA grantA-  label "Medium"  $ assert $ imply (not_ requestA &&. requestB) grantB-  label "Lowest"  $ assert $ imply (not_ requestA &&. not_ requestB &&. requestC) grantC+  "Highest" -: assert $ requestA --> grantA+  "Medium"  -: assert $ (not_ requestA &&. requestB) --> grantB+  "Lowest"  -: assert $ (not_ requestA &&. not_ requestB &&. requestC) --> grantC  -- | An arbiter implementation. arbiter1 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)@@ -128,9 +128,9 @@   grantB <- bool "grantB" False   grantC <- bool "grantC" False -  label "GrantA" $ if_ (requestA)                                     (grantA <== true)-  label "GrantB" $ if_ (not_ requestA &&. requestB)                   (grantB <== true)-  label "GrantC" $ if_ (not_ requestA &&. not_ requestB &&. requestC) (grantC <== true)+  "GrantA" -: if_ (requestA)                                     (grantA <== true)+  "GrantB" -: if_ (not_ requestA &&. requestB)                   (grantB <== true)+  "GrantC" -: if_ (not_ requestA &&. not_ requestB &&. requestC) (grantC <== true)    return (ref grantA, ref grantB, ref grantC) @@ -144,7 +144,7 @@  -- | Binding an arbiter implemenation to the arbiter specification. arbiter :: Name -> ((E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)) -> Stmt ()-arbiter name implementation = scope name $ do+arbiter name implementation = name -: do   -- Create input variables.   requestA <- input bool "requestA"   requestB <- input bool "requestB"@@ -152,7 +152,7 @@   let requests = (requestA, requestB, requestC)    -- Instantiate implementation.-  grants@(grantA, grantB, grantC) <- scope "impl" $ implementation requests+  grants@(grantA, grantB, grantC) <- "impl" -: implementation requests    -- Bind specification.   arbiterSpec requests grants

@@ -107,7 +107,7 @@       (Null, a) -> a       (a, Null) -> a       (a, b)    -> Sequence a b-    Assert a -> if any (flip elem vars) (exprVars a) then Assert a else Null+    Assert a -> Assert a     Assume a -> if any (flip elem vars) (exprVars a) then Assume a else Null     Label name a -> case trim a of       Null -> Null@@ -404,7 +404,7 @@       Just "true"  -> "ifelse true:\n"  ++ indent (concatMap f onTrue)       Just "false" -> "ifelse false:\n" ++ indent (concatMap f onFalse)       _ -> ""-    Label' name traces -> name ++ ":\n" ++ indent (concatMap f traces)+    Label' name traces -> name ++ " -:\n" ++ indent (concatMap f traces)  indent :: String -> String indent = unlines . map ("    " ++) . lines

@@ -1,5 +1,5 @@ name:    improve-version: 0.0.8+version: 0.0.9  category: Language