diff --git a/Language/ImProve.hs b/Language/ImProve.hs
--- a/Language/ImProve.hs
+++ b/Language/ImProve.hs
@@ -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
 
diff --git a/Language/ImProve/Code.hs b/Language/ImProve/Code.hs
--- a/Language/ImProve/Code.hs
+++ b/Language/ImProve/Code.hs
@@ -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
diff --git a/Language/ImProve/Examples.hs b/Language/ImProve/Examples.hs
--- a/Language/ImProve/Examples.hs
+++ b/Language/ImProve/Examples.hs
@@ -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
diff --git a/improve.cabal b/improve.cabal
--- a/improve.cabal
+++ b/improve.cabal
@@ -1,5 +1,5 @@
 name:    improve
-version: 0.1.0
+version: 0.1.2
 
 category: Language, Formal Methods, Embedded