improve 0.1.0 → 0.1.2

raw patch · 4 files changed

+102/−108 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 +32/−36
• Language/ImProve/Code.hs +43/−44
• Language/ImProve/Examples.hs +26/−27
• improve.cabal +1/−1

@@ -42,11 +42,11 @@     f(); } -switch (a) {              'case_' a-    case 1:                   [ (a ==. 1, do1)-        do1();                , (a ==. 2, do2)-        break;                , (true   , do3)-    case 2:                   ]+switch (a) {              'case_' $ do+    case 1:                   a ==. 1 ==> do1+        do1();                a ==. 2 ==> do2+        break;                true    ==> do3+    case 2:         do2();         break;     default:@@ -63,7 +63,7 @@ /Statement Labels/  @-label: {                  \"label\" '|-' do+label: {                  \"label\" '|' do     a();                      a     b();                      b }@@ -189,9 +189,7 @@   -- * Statements   , Stmt   -- ** Variable Hierarchical Scope and Statement Labeling -  , (|=)-  , (|-)-  , (|=-)+  , (-|)   -- ** Variable Declarations   , bool   , bool'@@ -200,12 +198,14 @@   , float   , float'   , input+  , global   -- ** Variable Assignment   , Assign (..)   -- ** Conditional Execution   , ifelse   , if_   , case_+  , (==>)   -- ** Incrementing and decrementing.   , incr   , decr@@ -229,7 +229,7 @@ infixl 3 &&. infixl 2 ||. infixr 1 -->-infixr 0 <==, |=, |-, |=-+infixr 0 <==, ==>, -|  -- | True term. true :: E Bool@@ -358,33 +358,19 @@ mux :: AllE a => E Bool -> E a -> E a -> E a mux = Mux --- | Labels a statement.+-- | Labels a statement and creates a variable scope. --   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)+  put (path0 ++ [name], Null)   a <- stmt   (_, stmt1) <- get   put (path0, stmt0)   statement $ Label name stmt1   return a --- | Creates a new hierarchical scope for variable names.-(|=) :: Name -> Stmt a -> Stmt a-name |= stmt = do-  (path0, stmt0) <- get-  put (path0 ++ [name], stmt0)-  a <- stmt-  (_, stmt1) <- get-  put (path0, stmt1)-  return a---- | Creates a new hierarchical scope and labels a statement with the same name.-(|=-) :: Name -> Stmt a -> Stmt a-name |=- stmt = name |= name |- stmt- get :: Stmt ([Name], Statement) get = Stmt $ \ a -> (a, a) @@ -402,11 +388,13 @@   return $ V False (path ++ [name]) init  -- | Input variable declaration.  Input variables are initialized to 0.-input  :: AllE a => (Name -> a -> Stmt (V a)) -> Name -> Stmt (E a)-input f name = do-  path <- getPath-  return $ ref $ V True (path ++ [name]) $ zero f+input  :: AllE a => (Name -> a -> Stmt (V a)) -> Path -> E a+input f path = ref $ V True path $ zero f +-- | Global variable declaration.+global  :: AllE a => (Name -> a -> Stmt (V a)) -> Path -> a -> V a+global _ path init = V False path init+ -- | Boolean variable declaration. bool :: Name -> Bool -> Stmt (V Bool) bool = var@@ -495,10 +483,18 @@ if_ cond stmt = ifelse cond stmt $ return ()  -- | Condition case statement.-case_ :: [(E Bool, Stmt ())] -> Stmt ()-case_ [] = return ()-case_ ((cond, action) : b) = ifelse cond action $ case_ b+case_ :: Case () -> Stmt ()+case_ (Case f) = f $ return () +data Case a = Case (Stmt () -> Stmt ())+instance Monad Case where+  return _ = Case id+  (>>=) = undefined+  (Case f1) >> (Case f2) = Case $ f1 . f2++(==>) :: E Bool -> Stmt () -> Case ()+a ==> s = Case $ ifelse a s+ -- | Verify a program. -- -- ^ verify pathToYices maxK program@@ -507,5 +503,5 @@  -- | Generate C code. code :: Name -> Stmt () -> IO ()-code name program = C.code name $ snd $ evalStmt [name ++ "Variables"] program+code name program = C.code name $ snd $ evalStmt [] program 

@@ -11,59 +11,58 @@ code :: Name -> Statement -> IO () code name stmt = do   writeFile (name ++ ".c") $-       "// Generated by ImProve.\n\n"+       "/* Generated by ImProve. */\n\n"     ++ "#include <assert.h>\n\n"     ++ codeVariables True scope ++ "\n"-    ++ "void " ++ name ++ "() {\n"+    ++ "void " ++ name ++ "()\n{\n"     ++ indent (codeStmt stmt)     ++ "}\n\n"   writeFile (name ++ ".h") $-       "// Generated by ImProve.\n\n"+       "/* Generated by ImProve. */\n\n"     ++ codeVariables False scope ++ "\n"     ++ "void " ++ name ++ "(void);\n\n"   where   scope = case tree (\ (_, path, _) -> path) $ stmtVars stmt of     [] -> error "program contains no usefull statements"-    [a] -> a-    _ -> error "unexpected: muliple scope items"--codeStmt :: Statement -> String-codeStmt a = case a of-  AssignBool  a b -> pathName a ++ " = " ++ codeExpr b ++ ";\n"-  AssignInt   a b -> pathName a ++ " = " ++ codeExpr b ++ ";\n"-  AssignFloat a b -> 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)-  Null -> ""+    a  -> T.Branch (name ++ "_variables") a -codeExpr :: E a -> String-codeExpr a = case a of-  Ref a     -> pathName a-  Const a   -> showConst $ const' a-  Add a b   -> group [codeExpr a, "+", codeExpr b]-  Sub a b   -> group [codeExpr a, "-", codeExpr b]-  Mul a b   -> group [codeExpr a, "*", showConst (const' b)]-  Div a b   -> group [codeExpr a, "/", showConst (const' b)]-  Mod a b   -> group [codeExpr a, "%", showConst (const' b)]-  Not a     -> group ["!", codeExpr a]-  And a b   -> group [codeExpr a, "&&",  codeExpr b]-  Or  a b   -> group [codeExpr a, "||",  codeExpr b]-  Eq  a b   -> group [codeExpr a, "==",  codeExpr b]-  Lt  a b   -> group [codeExpr a, "<",   codeExpr b]-  Gt  a b   -> group [codeExpr a, ">",   codeExpr b]-  Le  a b   -> group [codeExpr a, "<=",  codeExpr b]-  Ge  a b   -> group [codeExpr a, ">=",  codeExpr b]-  Mux a b c -> group [codeExpr a, "?", codeExpr b, ":", codeExpr c] -  where-  group :: [String] -> String-  group a = "(" ++ intercalate " " a ++ ")"+  codeStmt :: Statement -> String+  codeStmt 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)+    Null -> ""+  +  codeExpr :: E a -> String+  codeExpr a = case a of+    Ref a     -> name ++ "_variables." ++ pathName a+    Const a   -> showConst $ const' a+    Add a b   -> group [codeExpr a, "+", codeExpr b]+    Sub a b   -> group [codeExpr a, "-", codeExpr b]+    Mul a b   -> group [codeExpr a, "*", showConst (const' b)]+    Div a b   -> group [codeExpr a, "/", showConst (const' b)]+    Mod a b   -> group [codeExpr a, "%", showConst (const' b)]+    Not a     -> group ["!", codeExpr a]+    And a b   -> group [codeExpr a, "&&",  codeExpr b]+    Or  a b   -> group [codeExpr a, "||",  codeExpr b]+    Eq  a b   -> group [codeExpr a, "==",  codeExpr b]+    Lt  a b   -> group [codeExpr a, "<",   codeExpr b]+    Gt  a b   -> group [codeExpr a, ">",   codeExpr b]+    Le  a b   -> group [codeExpr a, "<=",  codeExpr b]+    Ge  a b   -> group [codeExpr a, ">=",  codeExpr b]+    Mux a b c -> group [codeExpr a, "?", codeExpr b, ":", codeExpr c] +    where+    group :: [String] -> String+    group a = "(" ++ intercalate " " a ++ ")"  indent :: String -> String-indent = unlines . map ("    " ++) . lines+indent = unlines . map ("\t" ++) . lines  indent' :: String -> String indent' a = case lines a of@@ -74,12 +73,12 @@ codeVariables define a = (if define then "" else "extern ") ++ init (init (f1 a)) ++ (if define then " =\n    " ++ f2 a else "") ++ ";\n"   where   f1 a = case a of-    T.Branch name items -> "struct {  // " ++ name ++ "\n" ++ indent (concatMap f1 items) ++ "} " ++ name ++ ";\n"-    Leaf name (input, _, init) -> printf "%-5s %-25s;%s\n" (showConstType init) name (if input then "  // input" else "")+    T.Branch name items -> "struct {  /* " ++ name ++ " */\n" ++ indent (concatMap f1 items) ++ "} " ++ name ++ ";\n"+    Leaf name (input, _, init) -> printf "%-5s %-25s;%s\n" (showConstType init) name (if input then "  /* input */" else "")    f2 a = case a of-    T.Branch name items -> indent' $ "{   " ++ (intercalate ",   " $ map f2 items) ++ "}  // " ++ name ++ "\n"-    Leaf name (_, _, init) -> printf "%-15s  // %s\n" (showConst init) name+    T.Branch name items -> indent' $ "{   " ++ (intercalate ",   " $ map f2 items) ++ "}  /* " ++ name ++ " */\n"+    Leaf name (_, _, init) -> printf "%-15s  /* %s */\n" (showConst init) name  showConst :: Const -> String showConst a = case a of

@@ -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.@@ -46,19 +46,18 @@ -- | A top level wrapper for gcd'. gcdMain :: Stmt () gcdMain = do-  a <- input int "a"  -- Input variable 'a'.-  b <- input int "b"  -- Input variable 'b'.+  let a = input int ["a"]  -- Input variable 'a'.+      b = input int ["b"]  -- Input variable 'b'.   done   <- bool "done"   False  -- Variable signalling completion.   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'   result <== result' - -- | Build the gcdMain code (i.e. gcd.c, gcd.h). buildGCD :: IO () buildGCD = code "gcd" gcdMain@@ -72,8 +71,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 +92,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 +127,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,15 +143,15 @@  -- | 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"-  requestC <- input bool "requestC"+  let requestA = input bool ["requestA"]+      requestB = input bool ["requestB"]+      requestC = input bool ["requestC"]   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.1.0+version: 0.1.2  category: Language, Formal Methods, Embedded