improve 0.0.9 → 0.0.10

raw patch · 3 files changed

+41/−35 lines, 3 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• Language/ImProve.hs +19/−13
• Language/ImProve/Examples.hs +21/−21
• improve.cabal +1/−1

@@ -12,7 +12,7 @@  @ float a = 0.0;            a <- 'float' \"a\" 0-bool b = true;            b <- 'bool' \"b\" true+bool b = true;            b <- 'bool' \"b\" True int c = d + e + 3;        c <- 'int'' \"c\" (d + e + 3) @ @@ -52,7 +52,7 @@ /Statement Labels/  @-hello: {                  \"hello\" '-:' do+label: {                  \"label\" '|-' do     a();                      a     b();                      b }@@ -94,8 +94,8 @@ a + b                     a '+' b a * b                     a '*.' b a \/ b                     a '/.' b     -- float-a \/ b                     a '`div_`' b -- int-a % b                     a '`mod_`' b+a \/ b                     'div_' a b   -- int+a % b                     'mod_' a b abs(a)                    'abs' a min(a, b)                 'min_' a b max(a, b)                 'max_' a b@@ -106,7 +106,7 @@ @  /Function Definitions and Function Calls/-(All ImProve functions are Haskell functions that are inlined at compile time.)+(All ImProve functions are Haskell functions, which are inlined at code generation.)  @ int add(int a, int b) {                             add :: E Int -> E Int -> E Int@@ -123,6 +123,12 @@ @  -}++-- hello: \{                  hello '+++' do+--     a();                      a+--     b();                      b+--+ module Language.ImProve   (   -- * Types@@ -172,8 +178,8 @@   -- * Statements   , Stmt   -- ** Statement Labeling and Hierarchical Scope-  , (-:)-  , (!)+  , (|=)+  , (|-)   -- ** Variable Declarations   , bool   , bool'@@ -210,7 +216,7 @@ infixl 3 &&. infixl 2 ||. infixr 1 -->-infixr 0 <==, -:, !+infixr 0 <==, |-, |=  -- | True term. true :: E Bool@@ -252,7 +258,7 @@ any_ :: (a -> E Bool) -> [a] -> E Bool any_ f a = or_ $ map f a --- Logical implication (if a then b).+-- | Logical implication. (-->) :: E Bool -> E Bool -> E Bool  a --> b = not_ a ||. b @@ -342,8 +348,8 @@ -- | 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+(|-) :: Name -> Stmt a -> Stmt a+name |- stmt = do   (path0, stmt0) <- get   put (path0, Null)   a <- stmt@@ -353,8 +359,8 @@   return a  -- | Creates a new hierarcical scope for variable names.-(!) :: Name -> Stmt a -> Stmt a-name ! stmt = do+(|=) :: Name -> Stmt a -> Stmt a+name |= stmt = do   (path0, stmt0) <- get   put (path0 ++ [name], stmt0)   a <- stmt

@@ -25,18 +25,18 @@   b1 <- int "b1" 0  -- Working copy of 'b'.    -- A new input to process.-  "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.-  "reduceA" -: if_ (ref a1 >. ref b1) $ do+  "reduceA" |- if_ (ref a1 >. ref b1) $ do     a1 <== ref a1 - ref b1    -- Reduce b1.-  "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') <- "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.-  "GreaterThanOrEqualTo0" -: assert $ ref counter >=. 0-  "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.-  "OneHot" -: assert $      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.-  "NotRequestedA" -: assert $ not_ requestA --> not_ grantA-  "NotRequestedB" -: assert $ not_ requestB --> not_ grantB-  "NotRequestedC" -: assert $ 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.-  "OnlyRequestA" -: assert $ (     requestA &&. not_ requestB &&. not_ requestC) --> grantA-  "OnlyRequestB" -: assert $ (not_ requestA &&.      requestB &&. not_ requestC) --> grantB-  "OnlyRequestC" -: assert $ (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.-  "Highest" -: assert $ requestA --> grantA-  "Medium"  -: assert $ (not_ requestA &&. requestB) --> grantB-  "Lowest"  -: assert $ (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 -  "GrantA" -: if_ (requestA)                                     (grantA <== true)-  "GrantB" -: if_ (not_ requestA &&. requestB)                   (grantB <== true)-  "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 = 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) <- "impl" -: implementation requests+  grants@(grantA, grantB, grantC) <- "impl" |- implementation requests    -- Bind specification.   arbiterSpec requests grants

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