diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2015, Anders Persson, Emil Axelsson, Markus Aronsson
+Copyright (c) 2015-2016, Anders Persson, Emil Axelsson, Markus Aronsson
 
 All rights reserved.
 
diff --git a/examples/C.hs b/examples/C.hs
new file mode 100644
--- /dev/null
+++ b/examples/C.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE TypeOperators #-}
+
+module C where
+
+import Prelude hiding (break)
+
+import Language.C.Quote.C
+import Language.Embedded.Imperative
+import Language.Embedded.Concurrent
+import Language.Embedded.Backend.C
+import Language.Embedded.CExp
+
+type L =
+  C_CMD CExp :+:
+  FileCMD CExp
+
+-- | Define a function in another module and call it.
+multiModule :: Program L ()
+multiModule = do
+  addInclude "<stdlib.h>"
+  addExternProc "func_in_other" []
+  inModule "other" $ do
+    addDefinition [cedecl|
+      void func_in_other(void) {
+        puts("Hello from the other module!");
+      } |]
+    addInclude "<stdio.h>"
+  callProc "func_in_other" []
+
+----------------------------------------
+
+testAll = do
+    icompileAll multiModule
diff --git a/examples/Concurrent.hs b/examples/Concurrent.hs
--- a/examples/Concurrent.hs
+++ b/examples/Concurrent.hs
@@ -11,16 +11,19 @@
 
 import Language.Embedded.Imperative
 import Language.Embedded.Concurrent
+import Language.Embedded.Backend.C
 import Language.Embedded.CExp
 
-type L =
+type CMD =
   ThreadCMD :+:
-  ChanCMD CExp :+:
-  ControlCMD CExp :+:
-  FileCMD CExp
+  ChanCMD :+:
+  ControlCMD :+:
+  FileCMD
 
+type Prog = Program CMD (Param2 CExp CType)
+
 -- | Deadlocks due to channel becoming full.
-deadlock :: Program L ()
+deadlock :: Prog ()
 deadlock = do
   c <- newChan 1
   t <- fork $ readChan c >>= printf "%d\n"
@@ -31,7 +34,7 @@
 
 -- | Map a function over a file, then print the results. Mapping and printing
 --   happen in separate threads.
-mapFile :: (CExp Float -> CExp Float) -> FilePath -> Program L ()
+mapFile :: (CExp Float -> CExp Float) -> FilePath -> Prog ()
 mapFile f i = do
   c1 <- newCloseableChan 5
   c2 <- newCloseableChan 5
@@ -57,14 +60,14 @@
   waitThread t2
 
 -- | Waiting for thread completion.
-waiting :: Program L ()
+waiting :: Prog ()
 waiting = do
   t <- fork $ printf "Forked thread printing %d\n" (0 :: CExp Int32)
   waitThread t
   printf "Main thread printing %d\n" (1 :: CExp Int32)
 
 -- | A thread kills itself using its own thread ID.
-suicide :: Program L ()
+suicide :: Prog ()
 suicide = do
   tid <- forkWithId $ \tid -> do
     printf "This is printed. %d\n" (0 :: CExp Int32)
@@ -72,4 +75,15 @@
     printf "This is not. %d\n" (0 :: CExp Int32)
   waitThread tid
   printf "The thread is dead, long live the thread! %d\n" (0 :: CExp Int32)
+
+
+
+----------------------------------------
+
+testAll = do
+    tag "waiting" >> compareCompiled' opts waiting (runIO waiting) ""
+    tag "suicide" >> compareCompiled' opts suicide (runIO suicide) ""
+  where
+    tag str = putStrLn $ "---------------- examples/Concurrent.hs/" ++ str ++ "\n"
+    opts = defaultExtCompilerOpts {externalFlagsPost = ["-lpthread"]}
 
diff --git a/examples/Demo.hs b/examples/Demo.hs
new file mode 100644
--- /dev/null
+++ b/examples/Demo.hs
@@ -0,0 +1,43 @@
+{-# LANGUAGE TypeOperators #-}
+
+module Demo where
+
+
+
+import Control.Applicative ((<$>))
+import Data.Word
+
+import Language.Embedded.Imperative
+import Language.Embedded.Backend.C
+import Language.Embedded.CExp
+
+
+
+-- | Custom instruction type with: references, control structures and file I/O
+type CMD
+    =   RefCMD
+    :+: ControlCMD
+    :+: FileCMD
+
+-- | Program that asks the user for numbers and prints their sum
+sumInput :: Program CMD (Param2 CExp CType) ()
+sumInput = do
+    done <- initRef false
+    sum  <- initRef (0 :: CExp Word32)
+    while (not_ <$> getRef done) $ do
+        printf "Enter a number (0 means done): "
+        n <- fget stdin
+        iff (n #== 0)
+          (setRef done true)
+          (modifyRef sum (+n))
+    printf "The sum of your numbers is %d.\n" =<< getRef sum
+
+run_sumInput = runCompiled sumInput
+
+
+
+testAll = do
+    tag "sumInput" >> compareCompiled sumInput (runIO sumInput) (unlines $ map show $ reverse [0..20])
+  where
+    tag str = putStrLn $ "---------------- examples/Demo.hs/" ++ str ++ "\n"
+
diff --git a/examples/Imperative.hs b/examples/Imperative.hs
deleted file mode 100644
--- a/examples/Imperative.hs
+++ /dev/null
@@ -1,80 +0,0 @@
-{-# LANGUAGE TypeOperators #-}
-
-module Imperative where
-
-
-
-import Data.Int
-import Data.Word
-
-import Language.Embedded.Expression (evalExp)
-import Language.Embedded.Imperative
-import Language.Embedded.Backend.C
-import Language.Embedded.CExp
-
-
-
-refProg :: Program (RefCMD CExp) (CExp Int32)
-refProg = do
-    r1 <- initRef 4
-    r2 <- initRef 5
-    a  <- unsafeFreezeRef r1
-    b  <- getRef r2
-    let c = (a #== 10 ? a+b $ b+a) + 3
-    setRef r2 c
-    return c
-
-type CMD1
-    =   RefCMD CExp
-    :+: ArrCMD CExp
-    :+: ControlCMD CExp
-
-arrProg :: Program CMD1 (CExp Int32)
-arrProg = do
-    ref <- initRef 4
-    arr <- newArr (10 :: CExp Word8)
-    setArr 3 45 arr
-    a   <- unsafeFreezeRef ref
-    b   <- getArr 3 arr
-    let c = a+b
-    iff (a #== 4)
-      (setRef ref c)
-      (setRef ref b)
-    return c
-
-evalRef :: IO Int32
-evalRef = fmap evalExp $ runIO refProg
-
-compRef = icompile refProg
-
-evalArr :: IO Int32
-evalArr = fmap evalExp $ runIO arrProg
-
-compArr = icompile arrProg
-
-
-
-type CMD2
-    =   RefCMD CExp
-    :+: ControlCMD CExp
-    :+: FileCMD CExp
-
-summer :: Program CMD2 ()
-summer = do
-    inp <- fopen "input" ReadMode
-    let cont = fmap not_ $ feof inp
-    sum <- initRef (0 :: CExp Float)
-    while cont $ do
-        f <- fget inp
-        s <- getRef sum
-        setRef sum (s+f+(3+4+5+6))
-    s <- getRef sum
-    printf "The sum is: %f\n" s
-
-runSummer :: IO ()
-runSummer = do
-    writeFile "input" $ unwords $ map show ([-5..4] :: [Float])
-    runIO summer
-
-compSummer = icompile summer
-
diff --git a/imperative-edsl.cabal b/imperative-edsl.cabal
--- a/imperative-edsl.cabal
+++ b/imperative-edsl.cabal
@@ -1,11 +1,11 @@
 name:                imperative-edsl
-version:             0.4.1
+version:             0.5
 synopsis:            Deep embedding of imperative programs with code generation
 description:         Deep embedding of imperative programs with code generation.
                      .
                      The main module for users who want to write imperative
                      programs is "Language.Embedded.Imperative" (and optionally
-                     "Language.Embedded.Expr" which provides a simple expression
+                     "Language.Embedded.CExp" which provides a simple expression
                      language).
                      .
                      Examples can be found in the @examples@ directory.
@@ -13,13 +13,17 @@
 license-file:        LICENSE
 author:              Anders Persson, Emil Axelsson, Markus Aronsson
 maintainer:          emax@chalmers.se
-copyright:           Copyright 2015 Anders Persson, Emil Axelsson, Markus Aronsson
+copyright:           Copyright (c) 2015-2016, Anders Persson, Emil Axelsson, Markus Aronsson
 homepage:            https://github.com/emilaxelsson/imperative-edsl
 bug-reports:         https://github.com/emilaxelsson/imperative-edsl/issues
 category:            Language
 build-type:          Simple
 cabal-version:       >=1.10
 
+extra-source-files:
+  examples/*.hs
+  tests/*.hs
+
 source-repository head
   type:     git
   location: git@github.com:emilaxelsson/imperative-edsl.git
@@ -31,11 +35,12 @@
 library
   exposed-modules:
     Control.Monads
+    System.IO.Fake
     Language.C.Monad
     Language.Embedded.Expression
     Language.Embedded.Traversal
-    Language.Embedded.Imperative.Args
     Language.Embedded.Imperative.CMD
+    Language.Embedded.Imperative.Args
     Language.Embedded.Imperative.Frontend.General
     Language.Embedded.Imperative.Frontend
     Language.Embedded.Imperative
@@ -43,6 +48,7 @@
     Language.Embedded.Concurrent
     Language.Embedded.Signature
     Language.Embedded.Backend.C
+    Language.Embedded.Backend.C.Expression
     Language.Embedded.CExp
 
   other-modules:
@@ -54,42 +60,51 @@
 
   default-extensions:
     ConstraintKinds
+    DataKinds
     DefaultSignatures
     DeriveDataTypeable
+    DeriveFoldable
     DeriveFunctor
+    DeriveTraversable
     FlexibleContexts
     FlexibleInstances
     GADTs
     GeneralizedNewtypeDeriving
     MultiParamTypeClasses
+    PatternSynonyms
+    PolyKinds
     Rank2Types
+    RecordWildCards
     ScopedTypeVariables
     StandaloneDeriving
     TypeFamilies
     TypeOperators
+    ViewPatterns
 
   other-extensions:
-    PolyKinds
+    CPP
     QuasiQuotes
     UndecidableInstances
 
   build-depends:
     array,
     base >=4 && <5,
-    constraints,
     containers,
+    deepseq,
+    directory,
     exception-transformers,
+    ghc-prim,
     language-c-quote >= 0.11 && < 0.12,
     mainland-pretty >= 0.4 && < 0.5,
     microlens >= 0.3.0.0,
     microlens-mtl,
     microlens-th,
     mtl,
-    operational-alacarte,
-    tagged,
-      -- tagged needed for GHC 7.6
+    process,
+    operational-alacarte >= 0.2,
     BoundedChan,
-    srcloc
+    srcloc,
+    time >= 1.5.0.1
 
   if flag(old-syntactic)
     build-depends:
@@ -101,35 +116,19 @@
 
   hs-source-dirs: src
 
-test-suite Examples
+test-suite Tests
   type: exitcode-stdio-1.0
 
   hs-source-dirs: tests examples
 
-  main-is: Examples.hs
-
-  other-modules:
-    Concurrent
-    Imperative
+  main-is: Tests.hs
 
   default-language: Haskell2010
 
   build-depends:
     base,
     imperative-edsl,
-    mainland-pretty,
-    directory,
-    process
-
-test-suite Semantics
-  type: exitcode-stdio-1.0
-
-  hs-source-dirs: tests
-
-  main-is: Semantics.hs
-
-  default-language: Haskell2010
+    syntactic,
+    tasty-quickcheck,
+    tasty-th
 
-  build-depends:
-    base,
-    imperative-edsl
diff --git a/src/Control/Monads.hs b/src/Control/Monads.hs
--- a/src/Control/Monads.hs
+++ b/src/Control/Monads.hs
@@ -15,11 +15,9 @@
 import Control.Monad.State.Strict
 import Control.Monad.Writer
 
-import Language.Embedded.Expression
 
 
-
-newtype SupplyT m a = SupplyT { unSupplyT :: StateT VarId m a }
+newtype SupplyT m a = SupplyT { unSupplyT :: StateT Integer m a }
   deriving (Functor, Applicative, Monad, MonadFix, MonadIO, MonadTrans)
 
 type Supply = SupplyT Identity
@@ -27,8 +25,8 @@
 class Monad m => MonadSupply m
   where
     -- | Create a fresh variable identifier
-    fresh :: m VarId
-    default fresh :: (m ~ t n, MonadTrans t, MonadSupply n) => m VarId
+    fresh :: m Integer
+    default fresh :: (m ~ t n, MonadTrans t, MonadSupply n) => m Integer
     fresh = lift fresh
 
 instance Monad m => MonadSupply (SupplyT m)
diff --git a/src/Language/C/Monad.hs b/src/Language/C/Monad.hs
--- a/src/Language/C/Monad.hs
+++ b/src/Language/C/Monad.hs
@@ -211,13 +211,14 @@
     protos = nub $ reverse $ _prototypes env
     globs  = nub $ reverse $ _globals env
 
--- | Generate a C document
-prettyCGenT :: Monad m => CGenT m a -> m Doc
+-- | Generate C documents for each module
+prettyCGenT :: Monad m => CGenT m a -> m [(String, Doc)]
 prettyCGenT ma = do
     (_,cenv) <- runCGenT ma (defaultCEnv Flags)
-    return $ ppr $ cenvToCUnit cenv
+    return $ map (("", ppr) <*>)
+           $ ("main", cenvToCUnit cenv) : Map.toList (_modules cenv)
 
-prettyCGen :: CGen a -> Doc
+prettyCGen :: CGen a -> [(String, Doc)]
 prettyCGen = runIdentity . prettyCGenT
 
 -- | Retrieve a fresh identifier
@@ -414,7 +415,10 @@
     let (globs, shared) = unzip $ map (extractDecls (`Set.member` uvs)) oldglobs
         sharedList = Set.toList $ Set.unions shared
         sharedDecls = map (\ig -> C.DecDef ig (SrcLoc NoLoc)) sharedList
-    void $ globals <<.= (globs ++ sharedDecls)
+    -- Reverse is a trick that ensures the correct order of declarations for arrays
+    -- and their wrapper pointers. It depends on the naming schema of identifiers:
+    -- arrays are prefixed with underscores, while their wrappers are not.
+    void $ globals <<.= (globs ++ reverse sharedDecls)
   where
     -- Only keep vars shared between functions by intersecting with the union
     -- of all other funs' uvs. TODO: optimize.
diff --git a/src/Language/Embedded/Backend/C.hs b/src/Language/Embedded/Backend/C.hs
--- a/src/Language/Embedded/Backend/C.hs
+++ b/src/Language/Embedded/Backend/C.hs
@@ -3,21 +3,33 @@
 
 -- | C code generation for 'Program'
 
-module Language.Embedded.Backend.C where
+module Language.Embedded.Backend.C
+  ( module Language.Embedded.Backend.C.Expression
+  , module Language.Embedded.Backend.C
+  ) where
 
 
 
 #if __GLASGOW_HASKELL__ < 710
 import Control.Applicative
+import Data.Monoid
 #endif
+import Control.Exception
+import Data.Time (getCurrentTime, formatTime, defaultTimeLocale)
+import System.Directory (getTemporaryDirectory, removeFile)
+import System.Exit (ExitCode (..))
+import System.IO
+import System.Process (system)
 
 import Data.Loc (noLoc)
 import qualified Language.C.Syntax as C
+import Text.PrettyPrint.Mainland (pretty)
 
 import Control.Monad.Operational.Higher
+import System.IO.Fake
 import Language.C.Monad
 
-import Text.PrettyPrint.Mainland (pretty)
+import Language.Embedded.Backend.C.Expression
 
 
 
@@ -39,29 +51,191 @@
   -- Apparently this is what `!` parses to
 viewNotExp _ = Nothing
 
+arrayInit :: [C.Exp] -> C.Initializer
+arrayInit as = C.CompoundInitializer
+    [(Nothing, C.ExpInitializer a noLoc) | a <- as]
+    noLoc
 
 
+
 --------------------------------------------------------------------------------
 -- * Code generation user interface
 --------------------------------------------------------------------------------
 
 -- | Compile a program to C code represented as a string
 --
+-- This function returns only the first (main) module.
+-- To get every C translation units, use `compileAll`.
+--
 -- For programs that make use of the primitives in
 -- "Language.Embedded.Concurrent", the resulting C code can be compiled as
 -- follows:
 --
 -- > gcc -Iinclude csrc/chan.c -lpthread YOURPROGRAM.c
-compile :: (Interp instr CGen, HFunctor instr) => Program instr a -> String
-compile = pretty 80 . prettyCGen . liftSharedLocals . wrapMain . interpret
+compile :: (Interp instr CGen (Param2 exp pred), HFunctor instr) =>
+    Program instr (Param2 exp pred) a -> String
+compile = snd . head . compileAll
 
+compileAll :: (Interp instr CGen (Param2 exp pred), HFunctor instr) =>
+    Program instr (Param2 exp pred) a -> [(String, String)]
+compileAll = map (("", pretty 80) <*>) . prettyCGen . liftSharedLocals . wrapMain . interpret
+
 -- | Compile a program to C code and print it on the screen
 --
+-- This function returns only the first (main) module.
+-- To get every C translation units, use `icompileAll`.
+--
 -- For programs that make use of the primitives in
 -- "Language.Embedded.Concurrent", the resulting C code can be compiled as
 -- follows:
 --
 -- > gcc -Iinclude csrc/chan.c -lpthread YOURPROGRAM.c
-icompile :: (Interp instr CGen, HFunctor instr) => Program instr a -> IO ()
+icompile :: (Interp instr CGen (Param2 exp pred), HFunctor instr) =>
+    Program instr (Param2 exp pred) a -> IO ()
 icompile = putStrLn . compile
+
+icompileAll :: (Interp instr CGen (Param2 exp pred), HFunctor instr) =>
+    Program instr (Param2 exp pred) a -> IO ()
+icompileAll = mapM_ (\(n, m) -> putStrLn ("// module " ++ n) >> putStrLn m) . compileAll
+
+removeFileIfPossible :: FilePath -> IO ()
+removeFileIfPossible file =
+    catch (removeFile file) (\(_ :: SomeException) -> return ())
+
+data ExternalCompilerOpts = ExternalCompilerOpts
+      { externalKeepFiles  :: Bool      -- ^ Keep generated files?
+      , externalFlagsPre   :: [String]  -- ^ External compiler flags (e.g. @["-Ipath"]@)
+      , externalFlagsPost  :: [String]  -- ^ External compiler flags after C source (e.g. @["-lm","-lpthread"]@)
+      , externalSilent     :: Bool      -- ^ Don't print anything besides what the program prints
+      }
+
+defaultExtCompilerOpts :: ExternalCompilerOpts
+defaultExtCompilerOpts = ExternalCompilerOpts
+    { externalKeepFiles = False
+    , externalFlagsPre  = []
+    , externalFlagsPost = []
+    , externalSilent    = False
+    }
+
+instance Monoid ExternalCompilerOpts
+  where
+    mempty = defaultExtCompilerOpts
+    mappend
+        (ExternalCompilerOpts keep1 pre1 post1 silent1)
+        (ExternalCompilerOpts keep2 pre2 post2 silent2) =
+            ExternalCompilerOpts keep2 (pre1 ++ pre2) (post1 ++ post2) silent2
+
+maybePutStrLn :: Bool -> String -> IO ()
+maybePutStrLn False str = putStrLn str
+maybePutStrLn _ _ = return ()
+
+-- TODO: it would be nice to have a version that compiles all modules of a program,
+-- as it currently compiles only the first (main) module.
+-- | Generate C code and use GCC to compile it
+compileC :: (Interp instr CGen (Param2 exp pred), HFunctor instr)
+    => ExternalCompilerOpts
+    -> Program instr (Param2 exp pred) a  -- ^ Program to compile
+    -> IO FilePath                        -- ^ Path to the generated executable
+compileC (ExternalCompilerOpts {..}) prog = do
+    tmp <- getTemporaryDirectory
+    t   <- fmap (formatTime defaultTimeLocale format) getCurrentTime
+    (exeFile,exeh) <- openTempFile tmp ("edsl_" ++ t)
+    hClose exeh
+    let cFile = exeFile ++ ".c"
+    writeFile cFile $ compile prog
+    when externalKeepFiles $ maybePutStrLn externalSilent $
+        "Created temporary file: " ++ cFile
+    let compileCMD = unwords
+          $  ["gcc", "-std=c99"]
+          ++ externalFlagsPre
+          ++ [cFile, "-o", exeFile]
+          ++ externalFlagsPost
+    maybePutStrLn externalSilent compileCMD
+    exit <- system compileCMD
+    unless externalKeepFiles $ removeFileIfPossible cFile
+    case exit of
+      ExitSuccess -> return exeFile
+      err -> do removeFileIfPossible exeFile
+                error "compileC: failed to compile generated C code"
+  where
+    format = if externalKeepFiles then "%a-%H-%M-%S_" else ""
+
+-- | Generate C code and use GCC to check that it compiles (no linking)
+compileAndCheck' :: (Interp instr CGen (Param2 exp pred), HFunctor instr) =>
+    ExternalCompilerOpts -> Program instr (Param2 exp pred) a -> IO ()
+compileAndCheck' opts prog = do
+    let opts' = opts {externalFlagsPre = "-c" : externalFlagsPre opts}
+    exe <- compileC opts' prog
+    removeFileIfPossible exe
+
+-- | Generate C code and use GCC to check that it compiles (no linking)
+compileAndCheck :: (Interp instr CGen (Param2 exp pred), HFunctor instr) =>
+    Program instr (Param2 exp pred) a -> IO ()
+compileAndCheck = compileAndCheck' mempty
+
+-- | Generate C code, use GCC to compile it, and run the resulting executable
+runCompiled' :: (Interp instr CGen (Param2 exp pred), HFunctor instr) =>
+    ExternalCompilerOpts -> Program instr (Param2 exp pred) a -> IO ()
+runCompiled' opts@(ExternalCompilerOpts {..}) prog = do
+    exe <- compileC opts prog
+    maybePutStrLn externalSilent ""
+    maybePutStrLn externalSilent "#### Running:"
+    system exe
+    removeFileIfPossible exe
+    return ()
+
+-- | Generate C code, use GCC to compile it, and run the resulting executable
+runCompiled :: (Interp instr CGen (Param2 exp pred), HFunctor instr) =>
+    Program instr (Param2 exp pred) a -> IO ()
+runCompiled = runCompiled' mempty
+
+-- | Like 'runCompiled'' but with explicit input/output connected to
+-- @stdin@/@stdout@
+captureCompiled' :: (Interp instr CGen (Param2 exp pred), HFunctor instr)
+    => ExternalCompilerOpts
+    -> Program instr (Param2 exp pred) a  -- ^ Program to run
+    -> String                             -- ^ Input to send to @stdin@
+    -> IO String                          -- ^ Result from @stdout@
+captureCompiled' opts prog inp = do
+    exe <- compileC opts prog
+    out <- fakeIO (system exe) inp
+    removeFileIfPossible exe
+    return out
+
+-- | Like 'runCompiled' but with explicit input/output connected to
+-- @stdin@/@stdout@
+captureCompiled :: (Interp instr CGen (Param2 exp pred), HFunctor instr)
+    => Program instr (Param2 exp pred) a  -- ^ Program to run
+    -> String                             -- ^ Input to send to @stdin@
+    -> IO String                          -- ^ Result from @stdout@
+captureCompiled = captureCompiled' defaultExtCompilerOpts
+
+-- | Compare the content written to @stdout@ from the reference program and from
+-- running the compiled C code
+compareCompiled' :: (Interp instr CGen (Param2 exp pred), HFunctor instr)
+    => ExternalCompilerOpts
+    -> Program instr (Param2 exp pred) a  -- ^ Program to run
+    -> IO a                               -- ^ Reference program
+    -> String                             -- ^ Input to send to @stdin@
+    -> IO ()
+compareCompiled' opts@(ExternalCompilerOpts {..}) prog ref inp = do
+    maybePutStrLn externalSilent "#### Reference program:"
+    outRef <- fakeIO ref inp
+    maybePutStrLn externalSilent outRef
+    maybePutStrLn externalSilent "#### runCompiled:"
+    outComp <- captureCompiled' opts prog inp
+    maybePutStrLn externalSilent outComp
+    if outRef /= outComp
+      then error "runCompiled differs from reference program"
+      else maybePutStrLn externalSilent
+             "  -- runCompiled is consistent with reference program\n\n\n\n"
+
+-- | Compare the content written to @stdout@ from the reference program and from
+-- running the compiled C code
+compareCompiled :: (Interp instr CGen (Param2 exp pred), HFunctor instr)
+    => Program instr (Param2 exp pred) a  -- ^ Program to run
+    -> IO a                               -- ^ Reference program
+    -> String                             -- ^ Input to send to @stdin@
+    -> IO ()
+compareCompiled = compareCompiled' defaultExtCompilerOpts
 
diff --git a/src/Language/Embedded/Backend/C/Expression.hs b/src/Language/Embedded/Backend/C/Expression.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Embedded/Backend/C/Expression.hs
@@ -0,0 +1,118 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+module Language.Embedded.Backend.C.Expression where
+
+
+
+import Data.Int
+import Data.Word
+import Data.Proxy
+import Data.Typeable
+#if __GLASGOW_HASKELL__ < 710
+import Data.Monoid
+#endif
+
+#if MIN_VERSION_syntactic(3,0,0)
+import Data.TypeRep hiding (Typeable, gcast)
+import Data.TypeRep.TH
+import Data.TypeRep.Types.Basic
+import Data.TypeRep.Types.Tuple
+import Data.TypeRep.Types.IntWord
+#endif
+
+import Language.C.Monad
+import Language.C.Quote.C
+import Language.C.Syntax (Exp,Type)
+import qualified Language.C.Syntax as C
+
+import Language.Embedded.Expression
+
+
+
+-- | General interface for compiling expressions
+class FreeExp exp => CompExp exp
+  -- The super class is motivated by the fact that compilation of functions
+  -- `exp a -> exp b` can be done by constructing an argument using `varExp`.
+  where
+    -- | Compilation of expressions
+    compExp :: MonadC m => exp a -> m Exp
+
+instance ToExp Int8   where toExp = toExp . toInteger
+instance ToExp Int16  where toExp = toExp . toInteger
+instance ToExp Int32  where toExp = toExp . toInteger
+instance ToExp Int64  where toExp = toExp . toInteger
+instance ToExp Word8  where toExp = toExp . toInteger
+instance ToExp Word16 where toExp = toExp . toInteger
+instance ToExp Word32 where toExp = toExp . toInteger
+instance ToExp Word64 where toExp = toExp . toInteger
+  -- See <https://github.com/mainland/language-c-quote/pull/63>
+
+-- | Types supported by C
+class (Show a, Eq a, Typeable a) => CType a
+  where
+    cType :: MonadC m => proxy a -> m Type
+
+    cLit         :: MonadC m => a -> m Exp
+    default cLit :: (ToExp a, MonadC m) => a -> m Exp
+    cLit = return . flip toExp mempty
+
+instance CType Bool
+  where
+    cType _ = do
+        addSystemInclude "stdbool.h"
+        return [cty| typename bool |]
+    cLit b = do
+        addSystemInclude "stdbool.h"
+        return $ if b then [cexp| true |] else [cexp| false |]
+
+instance CType Int8   where cType _ = addSystemInclude "stdint.h"  >> return [cty| typename int8_t   |]
+instance CType Int16  where cType _ = addSystemInclude "stdint.h"  >> return [cty| typename int16_t  |]
+instance CType Int32  where cType _ = addSystemInclude "stdint.h"  >> return [cty| typename int32_t  |]
+instance CType Int64  where cType _ = addSystemInclude "stdint.h"  >> return [cty| typename int64_t  |]
+instance CType Word8  where cType _ = addSystemInclude "stdint.h"  >> return [cty| typename uint8_t  |]
+instance CType Word16 where cType _ = addSystemInclude "stdint.h"  >> return [cty| typename uint16_t |]
+instance CType Word32 where cType _ = addSystemInclude "stdint.h"  >> return [cty| typename uint32_t |]
+instance CType Word64 where cType _ = addSystemInclude "stdint.h"  >> return [cty| typename uint64_t |]
+
+instance CType Float  where cType _ = return [cty| float |]
+instance CType Double where cType _ = return [cty| double |]
+
+#if MIN_VERSION_syntactic(3,0,0)
+instance ShowClass CType where showClass _ = "CType"
+
+pCType :: Proxy CType
+pCType = Proxy
+
+deriveWitness ''CType ''BoolType
+deriveWitness ''CType ''FloatType
+deriveWitness ''CType ''DoubleType
+deriveWitness ''CType ''IntWordType
+
+derivePWitness ''CType ''BoolType
+derivePWitness ''CType ''FloatType
+derivePWitness ''CType ''DoubleType
+derivePWitness ''CType ''IntWordType
+
+instance PWitness CType CharType t
+instance PWitness CType ListType t
+instance PWitness CType TupleType t
+instance PWitness CType FunType t
+#endif
+
+-- | Remove one layer of a nested proxy
+proxyArg :: proxy1 (proxy2 a) -> Proxy a
+proxyArg _ = Proxy
+
+-- | Create and declare a fresh variable
+freshVar :: forall m a . (MonadC m, CType a) => m (Val a)
+freshVar = do
+    v <- gensym "v"
+    touchVar v
+    t <- cType (Proxy :: Proxy a)
+    case t of
+      C.Type _ C.Ptr{} _ -> addLocal [cdecl| $ty:t $id:v = NULL; |]
+      _                  -> addLocal [cdecl| $ty:t $id:v; |]
+    return (ValComp v)
+
diff --git a/src/Language/Embedded/CExp.hs b/src/Language/Embedded/CExp.hs
--- a/src/Language/Embedded/CExp.hs
+++ b/src/Language/Embedded/CExp.hs
@@ -14,9 +14,8 @@
 
 
 
-import Data.Int
+import Data.Array
 import Data.Maybe
-import Data.Word
 #if __GLASGOW_HASKELL__ < 710
 import Data.Monoid
 #endif
@@ -30,105 +29,110 @@
 import Language.Syntactic
 #endif
 
-#if MIN_VERSION_syntactic(3,0,0)
-import Data.TypeRep hiding (Typeable, gcast)
-import Data.TypeRep.TH
-import Data.TypeRep.Types.Basic
-import Data.TypeRep.Types.Tuple
-import Data.TypeRep.Types.IntWord
-#endif
-
 import Language.C.Quote.C
 import Language.C.Syntax (Type, UnOp (..), BinOp (..), Exp (UnOp, BinOp))
 import qualified Language.C.Syntax as C
 
 import Language.C.Monad
 import Language.Embedded.Expression
+import Language.Embedded.Backend.C
+import Language.Embedded.Imperative.CMD (IArr (..))
 
 
 
 --------------------------------------------------------------------------------
--- * Types
+-- * Expressions
 --------------------------------------------------------------------------------
 
--- | Types supported by C
-class (Show a, Eq a, Typeable a) => CType a
+data Unary a
   where
-    cType :: MonadC m => proxy a -> m Type
-
-instance CType Bool   where cType _ = addSystemInclude "stdbool.h" >> return [cty| typename bool     |]
-instance CType Int8   where cType _ = addSystemInclude "stdint.h"  >> return [cty| typename int8_t   |]
-instance CType Int16  where cType _ = addSystemInclude "stdint.h"  >> return [cty| typename int16_t  |]
-instance CType Int32  where cType _ = addSystemInclude "stdint.h"  >> return [cty| typename int32_t  |]
-instance CType Int64  where cType _ = addSystemInclude "stdint.h"  >> return [cty| typename int64_t  |]
-instance CType Word8  where cType _ = addSystemInclude "stdint.h"  >> return [cty| typename uint8_t  |]
-instance CType Word16 where cType _ = addSystemInclude "stdint.h"  >> return [cty| typename uint16_t |]
-instance CType Word32 where cType _ = addSystemInclude "stdint.h"  >> return [cty| typename uint32_t |]
-instance CType Word64 where cType _ = addSystemInclude "stdint.h"  >> return [cty| typename uint64_t |]
-
-instance CType Float  where cType _ = return [cty| float |]
-instance CType Double where cType _ = return [cty| double |]
-
-#if MIN_VERSION_syntactic(3,0,0)
-instance ShowClass CType where showClass _ = "CType"
-
-pCType :: Proxy CType
-pCType = Proxy
-
-deriveWitness ''CType ''BoolType
-deriveWitness ''CType ''FloatType
-deriveWitness ''CType ''DoubleType
-deriveWitness ''CType ''IntWordType
+    UnNeg :: Num a => Unary (a -> a)
+    UnNot :: Unary (Bool -> Bool)
 
-derivePWitness ''CType ''BoolType
-derivePWitness ''CType ''FloatType
-derivePWitness ''CType ''DoubleType
-derivePWitness ''CType ''IntWordType
+evalUnary :: Unary a -> a
+evalUnary UnNeg = negate
+evalUnary UnNot = not
 
-instance PWitness CType CharType t
-instance PWitness CType ListType t
-instance PWitness CType TupleType t
-instance PWitness CType FunType t
-#endif
+unaryOp :: Unary a -> UnOp
+unaryOp UnNeg = Negate
+unaryOp UnNot = Lnot
 
--- | Return whether the type of the expression is a floating-point numeric type
-isFloat :: forall a . CType a => CExp a -> Bool
-isFloat a
-    | t == typeOf (undefined :: Float)  = True
-    | t == typeOf (undefined :: Double) = True
-    | otherwise = False
+data Binary a
   where
-    t = typeOf (undefined :: a)
-
--- | Return whether the type of the expression is a non-floating-point type
-isExact :: CType a => CExp a -> Bool
-isExact = not . isFloat
+    BiAdd  :: Num a            => Binary (a -> a -> a)
+    BiSub  :: Num a            => Binary (a -> a -> a)
+    BiMul  :: Num a            => Binary (a -> a -> a)
+    BiDiv  :: Fractional a     => Binary (a -> a -> a)
+    BiQuot :: Integral a       => Binary (a -> a -> a)
+    BiRem  :: Integral a       => Binary (a -> a -> a)
+    BiAnd  ::                     Binary (Bool -> Bool -> Bool)
+    BiOr   ::                     Binary (Bool -> Bool -> Bool)
+    BiEq   :: CType a          => Binary (a -> a -> Bool)
+    BiNEq  :: CType a          => Binary (a -> a -> Bool)
+    BiLt   :: (Ord a, CType a) => Binary (a -> a -> Bool)
+    BiGt   :: (Ord a, CType a) => Binary (a -> a -> Bool)
+    BiLe   :: (Ord a, CType a) => Binary (a -> a -> Bool)
+    BiGe   :: (Ord a, CType a) => Binary (a -> a -> Bool)
 
+evalBinary :: Binary a -> a
+evalBinary BiAdd  = (+)
+evalBinary BiSub  = (-)
+evalBinary BiMul  = (*)
+evalBinary BiDiv  = (/)
+evalBinary BiQuot = quot
+evalBinary BiRem  = rem
+evalBinary BiAnd  = (&&)
+evalBinary BiOr   = (||)
+evalBinary BiEq   = (==)
+evalBinary BiNEq  = (/=)
+evalBinary BiLt   = (<)
+evalBinary BiGt   = (>)
+evalBinary BiLe   = (<=)
+evalBinary BiGe   = (>=)
 
+binaryOp :: Binary a -> BinOp
+binaryOp BiAdd  = Add
+binaryOp BiSub  = Sub
+binaryOp BiMul  = Mul
+binaryOp BiDiv  = Div
+binaryOp BiQuot = Div
+binaryOp BiRem  = Mod
+binaryOp BiAnd  = Land
+binaryOp BiOr   = Lor
+binaryOp BiEq   = Eq
+binaryOp BiNEq  = Ne
+binaryOp BiLt   = Lt
+binaryOp BiGt   = Gt
+binaryOp BiLe   = Le
+binaryOp BiGe   = Ge
 
---------------------------------------------------------------------------------
--- * Expressions
---------------------------------------------------------------------------------
+type SupportCode = forall m . MonadC m => m ()
 
 -- | Syntactic symbols for C
 data Sym sig
   where
-    -- Function or literal
+    -- Literal
+    Lit   :: String -> a -> Sym (Full a)
+    -- Predefined constant
+    Const :: SupportCode -> String -> a -> Sym (Full a)
+    -- Function call
+    Fun   ::
 #if MIN_VERSION_syntactic(3,0,0)
-    Fun  :: Signature sig => String -> Denotation sig -> Sym sig
-#else
-    Fun  :: String -> Denotation sig -> Sym sig
+             Signature sig =>
 #endif
+             SupportCode -> String -> Denotation sig -> Sym sig
     -- Unary operator
-    UOp  :: UnOp -> (a -> b) -> Sym (a :-> Full b)
+    UOp   :: Unary (a -> b) -> Sym (a :-> Full b)
     -- Binary operator
-    Op   :: BinOp -> (a -> b -> c) -> Sym (a :-> b :-> Full c)
+    Op    :: Binary (a -> b -> c) -> Sym (a :-> b :-> Full c)
     -- Type casting (ignored when generating code)
-    Cast :: (a -> b) -> Sym (a :-> Full b)
+    Cast  :: (a -> b) -> Sym (a :-> Full b)
     -- Conditional
-    Cond :: Sym (Bool :-> a :-> a :-> Full a)
+    Cond  :: Sym (Bool :-> a :-> a :-> Full a)
     -- Variable (only for compilation)
-    Var  :: String -> Sym (Full a)
+    Var   :: VarId -> Sym (Full a)
+    -- Unsafe array indexing
+    ArrIx :: (Integral i, Ix i) => IArr i a -> Sym (i :-> Full a)
 
 data T sig
   where
@@ -144,15 +148,24 @@
     desugar = unCExp
     sugar   = CExp
 
-type instance VarPred CExp = CType
-
 evalSym :: Sym sig -> Denotation sig
-evalSym (Fun _ a) = a
-evalSym (UOp _ f) = f
-evalSym (Op  _ f) = f
-evalSym (Cast f)  = f
-evalSym Cond      = \c t f -> if c then t else f
-evalSym (Var v)   = error $ "evalCExp: cannot evaluate variable " ++ v
+evalSym (Lit _ a)     = a
+evalSym (Const _ _ a) = a
+evalSym (Fun _ _ f)   = f
+evalSym (UOp uop)     = evalUnary uop
+evalSym (Op bop)      = evalBinary bop
+evalSym (Cast f)      = f
+evalSym Cond          = \c t f -> if c then t else f
+evalSym (ArrIx (IArrEval arr)) = \i ->
+    if i<l || i>h
+      then error $ "index "
+                ++ show (toInteger i)
+                ++ " out of bounds "
+                ++ show (toInteger l, toInteger h)
+      else arr!i
+  where
+    (l,h) = bounds arr
+evalSym (Var v) = error $ "evalCExp: cannot evaluate variable " ++ v
 
 -- | Evaluate an expression
 evalCExp :: CExp a -> a
@@ -162,49 +175,66 @@
     go (Sym (T s)) = evalSym s
     go (f :$ a)    = go f $ go a
 
-instance EvalExp CExp
+instance FreeExp CExp
   where
-    litExp a = CExp $ Sym $ T $ Fun (show a) a
-    evalExp  = evalCExp
+    type VarPred CExp = CType
+    valExp a = CExp $ Sym $ T $ Lit (show a) a
+    varExp = CExp . Sym . T . Var
 
+instance EvalExp CExp where evalExp = evalCExp
+
 -- | Compile an expression
 compCExp :: forall m a . MonadC m => CExp a -> m Exp
-compCExp = simpleMatch (go . unT) . unCExp
+compCExp = simpleMatch (\(T s) -> go s) . unCExp
   where
     compCExp' :: ASTF T b -> m Exp
     compCExp' = compCExp . CExp
 
-    go :: Sym sig -> Args (AST T) sig -> m Exp
-    go (Var v) Nil = return [cexp| $id:v |]
-    go (Fun lit _) Nil = case lit of
-      "True"  -> addSystemInclude "stdbool.h" >> return [cexp| true |]
-      "False" -> addSystemInclude "stdbool.h" >> return [cexp| false |]
-      l       -> return [cexp| $id:l |]
-    go (Fun fun _) args = do
+    typeOfSym :: forall sig m . MonadC m =>
+        CType (DenResult sig) => Sym sig -> m Type
+    typeOfSym _ = cType (Proxy :: Proxy (DenResult sig))
+
+    go :: CType (DenResult sig) => Sym sig -> Args (AST T) sig -> m Exp
+    go (Var v) Nil   = touchVar v >> return [cexp| $id:v |]
+    go (Lit _ a) Nil = cLit a
+    go (Const code const _) Nil = do
+      code
+      touchVar const
+      return [cexp| $id:const |]
+    go (Fun code fun _) args = do
+      code
       as <- sequence $ listArgs compCExp' args
       return [cexp| $id:fun($args:as) |]
-    go (UOp op _) (a :* Nil) = do
+    go (UOp uop) (a :* Nil) = do
       a' <- compCExp' a
-      return $ UnOp op a' mempty
-    go (Op op _) (a :* b :* Nil) = do
+      return $ UnOp (unaryOp uop) a' mempty
+    go (Op bop) (a :* b :* Nil) = do
       a' <- compCExp' a
       b' <- compCExp' b
-      return $ BinOp op a' b' mempty
-    go (Cast f) (a :* Nil) = do
+      return $ BinOp (binaryOp bop) a' b' mempty
+    go s@(Cast f) (a :* Nil) = do
       a' <- compCExp' a
-      return [cexp| $a' |]
+      t <- typeOfSym s
+      return [cexp|($ty:t) $a'|]
+          -- Explicit casting is usually not needed. But sometimes it is. For
+          -- example
+          --
+          --     printf("%f",i);
+          --
+          -- gives an error if `i` is an integer. The most robust option is
+          -- probably to always have explicit casts. In many cases it probably
+          -- also makes the generated code more readable.
     go Cond (c :* t :* f :* Nil) = do
       c' <- compCExp' c
       t' <- compCExp' t
       f' <- compCExp' f
       return $ C.Cond c' t' f' mempty
+    go (ArrIx arr) (i :* Nil) = do
+      i' <- compCExp' i
+      touchVar arr
+      return [cexp| $id:arr[$i'] |]
 
-instance CompExp CExp
-  where
-    varExp = CExp . Sym . T . Var . showVar
-      where showVar v = 'v' : show v
-    compExp  = compCExp
-    compType = cType
+instance CompExp CExp where compExp = compCExp
 
 -- | One-level constant folding: if all immediate sub-expressions are literals,
 -- the expression is reduced to a single literal
@@ -222,129 +252,213 @@
   -- sub-expressions. This is certainly doable, but seems to complicate things
   -- for not much gain (currently).
 
--- | Get the value of a literal expression
-viewLit :: CExp a -> Maybe a
-viewLit (CExp (Sym (T (Fun _ a)))) = Just a
-viewLit _ = Nothing
-
 castAST :: forall a b . Typeable b => ASTF T a -> Maybe (ASTF T b)
 castAST a = simpleMatch go a
   where
     go :: (DenResult sig ~ a) => T sig -> Args (AST T) sig -> Maybe (ASTF T b)
     go (T _) _ = gcast a
 
+-- | Get the value of a literal expression
+viewLit :: CExp a -> Maybe a
+viewLit (CExp (Sym (T (Lit _ a)))) = Just a
+viewLit _ = Nothing
 
+pattern LitP a      <- CExp (Sym (T (Lit _ a)))
+pattern LitP' a     <- Sym (T (Lit _ a))
+pattern NonLitP     <- (viewLit -> Nothing)
+pattern NonLitP'    <- (CExp -> (viewLit -> Nothing))
+pattern OpP op a b  <- CExp (Sym (T (Op op)) :$ a :$ b)
+pattern OpP' op a b <- Sym (T (Op op)) :$ a :$ b
+pattern UOpP op a   <- CExp (Sym (T (UOp op)) :$ a)
+pattern UOpP' op a  <- Sym (T (UOp op)) :$ a
 
+-- | Return whether the type of the expression is a floating-point numeric type
+isFloat :: forall a . CType a => CExp a -> Bool
+isFloat a = t == typeOf (undefined :: Float) || t == typeOf (undefined :: Double)
+  where
+    t = typeOf (undefined :: a)
+
+-- | Return whether the type of the expression is a non-floating-point type
+isExact :: CType a => CExp a -> Bool
+isExact = not . isFloat
+
+-- | Return whether the type of the expression is a non-floating-point type
+isExact' :: CType a => ASTF T a -> Bool
+isExact' = isExact . CExp
+
+
+
 --------------------------------------------------------------------------------
 -- * User interface
 --------------------------------------------------------------------------------
 
--- | Create a named variable
-variable :: CType a => String -> CExp a
-variable = CExp . Sym . T . Var
-
 -- | Construct a literal expression
 value :: CType a => a -> CExp a
-value a = CExp $ Sym $ T $ Fun (show a) a
+value a = CExp $ Sym $ T $ Lit (show a) a
 
+-- | Predefined constant
+constant :: CType a
+    => SupportCode  -- ^ Supporting C code
+    -> String       -- ^ Name of constant
+    -> a            -- ^ Value of constant
+    -> CExp a
+constant code const val = CExp $ Sym $ T $ Const code const val
+
+-- | Create a named variable
+variable :: CType a => VarId -> CExp a
+variable = CExp . Sym . T . Var
+
 true, false :: CExp Bool
-true  = value True
-false = value False
+true  = constant (addInclude "<stdbool.h>") "true" True
+false = constant (addInclude "<stdbool.h>") "false" False
 
-instance (Num a, CType a) => Num (CExp a)
+instance (Num a, Ord a, CType a) => Num (CExp a)
   where
     fromInteger = value . fromInteger
 
-    a + b
-      | Just 0 <- viewLit a, isExact a = b
-      | Just 0 <- viewLit b, isExact a = a
-      | otherwise = constFold $ sugarSym (T $ Op Add (+)) a b
+    LitP 0 + b | isExact b = b
+    a + LitP 0 | isExact a = a
+    a@(LitP _) + b@NonLitP | isExact a = b+a  -- Move literals to the right
+    OpP BiAdd a (LitP' b) + LitP c | isExact' a = CExp a + value (b+c)
+    OpP BiSub a (LitP' b) + LitP c | isExact' a = CExp a + value (c-b)
+    a + LitP b | b < 0, isExact a = a - value (negate b)
+    a + b = constFold $ sugarSym (T $ Op BiAdd) a b
 
-    a - b
-      | Just 0 <- viewLit a, isExact a = negate b
-      | Just 0 <- viewLit b, isExact a = a
-      | a == b,              isExact a = 0
-      | otherwise = constFold $ sugarSym (T $ Op Sub (-)) a b
+    LitP 0 - b | isExact b = negate b
+    a - LitP 0 | isExact a = a
+    a@(LitP _) - b@NonLitP | isExact a = negate b - negate a  -- Move literals to the right
+    OpP BiAdd a (LitP' b) - LitP c | isExact' a = CExp a + value (b-c)
+    OpP BiSub a (LitP' b) - LitP c | isExact' a = CExp a - value (b+c)
+    a - LitP b | b < 0, isExact a = a + value (negate b)
+    a - b = constFold $ sugarSym (T $ Op BiSub) a b
 
-    a * b
-      | Just 0 <- viewLit a, isExact a = value 0
-      | Just 0 <- viewLit b, isExact a = value 0
-      | Just 1 <- viewLit a, isExact a = b
-      | Just 1 <- viewLit b, isExact a = a
-      | otherwise = constFold $ sugarSym (T $ Op Mul (*)) a b
+    LitP 0 * b | isExact b = value 0
+    a * LitP 0 | isExact a = value 0
+    LitP 1 * b | isExact b = b
+    a * LitP 1 | isExact a = a
+    a@(LitP _) * b@NonLitP | isExact a = b*a  -- Move literals to the right
+    OpP BiMul a (LitP' b) * LitP c | isExact' a = CExp a * value (b*c)
+    a * b = constFold $ sugarSym (T $ Op BiMul) a b
 
-    negate a = constFold $ sugarSym (T $ UOp Negate negate) a
+    negate (UOpP UnNeg a)  | isExact' a = CExp a
+    negate (OpP BiAdd a b) | isExact' a = negate (CExp a) - CExp b
+    negate (OpP BiSub a b) | isExact' a = CExp b - CExp a
+    negate (OpP BiMul a b) | isExact' a = CExp a * negate (CExp b)
+      -- Negate the right operand, because literals are moved to the right
+      -- in multiplications
+    negate a = constFold $ sugarSym (T $ UOp UnNeg) a
 
     abs    = error "abs not implemented for CExp"
     signum = error "signum not implemented for CExp"
 
-instance (Fractional a, CType a) => Fractional (CExp a)
+instance (Fractional a, Ord a, CType a) => Fractional (CExp a)
   where
     fromRational = value . fromRational
-    a / b = constFold $ sugarSym (T $ Op Div (/)) a b
+    a / b = constFold $ sugarSym (T $ Op BiDiv) a b
 
     recip = error "recip not implemented for CExp"
 
+instance (Floating a, Ord a, CType a) => Floating (CExp a)
+  where
+    pi = constant (addGlobal pi_def) "EDSL_PI" pi
+      where
+        pi_def = [cedecl|$esc:("#define EDSL_PI 3.141592653589793")|]
+          -- This is the value of `pi :: Double`.
+          -- Apparently there is no standard C99 definition of pi.
+    a ** b = constFold $ sugarSym (T $ Fun (addInclude "<math.h>") "pow" (**)) a b
+    sin a  = constFold $ sugarSym (T $ Fun (addInclude "<math.h>") "sin" sin) a
+    cos a  = constFold $ sugarSym (T $ Fun (addInclude "<math.h>") "cos" cos) a
+
 -- | Integer division truncated toward zero
 quot_ :: (Integral a, CType a) => CExp a -> CExp a -> CExp a
+quot_ (LitP 0) b = 0
+quot_ a (LitP 1) = a
 quot_ a b
-    | Just 0 <- viewLit a = 0
-    | Just 1 <- viewLit b = a
-    | a == b              = 1
-    | otherwise           = constFold $ sugarSym (T $ Op Div quot) a b
+    | a == b     = 1
+quot_ a b        = constFold $ sugarSym (T $ Op BiQuot) a b
 
 -- | Integer remainder satisfying
 --
 -- > (x `quot_` y)*y + (x #% y) == x
 (#%) :: (Integral a, CType a) => CExp a -> CExp a -> CExp a
-a #% b
-    | Just 0 <- viewLit a = 0
-    | Just 1 <- viewLit b = 0
-    | a == b              = 0
-    | otherwise           = constFold $ sugarSym (T $ Op Mod rem) a b
+LitP 0 #% _          = 0
+_      #% LitP 1     = 0
+a      #% b | a == b = 0
+a      #% b          = constFold $ sugarSym (T $ Op BiRem) a b
 
+round_ :: (RealFrac a, Integral b, CType b) => CExp a -> CExp b
+round_ = constFold . sugarSym (T $ Fun (addInclude "<math.h>") "lround" round)
+
 -- | Integral type casting
 i2n :: (Integral a, Num b, CType b) => CExp a -> CExp b
 i2n a = constFold $ sugarSym (T $ Cast (fromInteger . toInteger)) a
 
+-- | Cast integer to 'Bool'
+i2b :: Integral a => CExp a -> CExp Bool
+i2b a = constFold $ sugarSym (T $ Cast (/=0)) a
+
+-- | Cast 'Bool' to integer
+b2i :: (Integral a, CType a) => CExp Bool -> CExp a
+b2i a = constFold $ sugarSym (T $ Cast (\c -> if c then 1 else 0)) a
+
 -- | Boolean negation
 not_ :: CExp Bool -> CExp Bool
-not_ (CExp (nt :$ a))
-    | Just (T (UOp Lnot _)) <- prj nt
-    , Just a' <- castAST a = CExp a'
-not_ a = constFold $ sugarSym (T $ UOp Lnot not) a
+not_ (UOpP UnNot a)  = CExp a
+not_ (OpP BiEq a b)  = CExp a #!= CExp b
+not_ (OpP BiNEq a b) = CExp a #== CExp b
+not_ (OpP BiLt a b)  = CExp a #>= CExp b
+not_ (OpP BiGt a b)  = CExp a #<= CExp b
+not_ (OpP BiLe a b)  = CExp a #> CExp b
+not_ (OpP BiGe a b)  = CExp a #< CExp b
+not_ a = constFold $ sugarSym (T $ UOp UnNot) a
 
+-- | Logical and
+(#&&) :: CExp Bool -> CExp Bool -> CExp Bool
+LitP True  #&& b          = b
+LitP False #&& b          = false
+a          #&& LitP True  = a
+a          #&& LitP False = false
+a          #&& b          = constFold $ sugarSym (T $ Op BiAnd) a b
+
+-- | Logical or
+(#||) :: CExp Bool -> CExp Bool -> CExp Bool
+LitP True  #|| b          = true
+LitP False #|| b          = b
+a          #|| LitP True  = true
+a          #|| LitP False = a
+a          #|| b          = constFold $ sugarSym (T $ Op BiOr) a b
+
 -- | Equality
 (#==) :: (Eq a, CType a) => CExp a -> CExp a -> CExp Bool
 a #== b
     | a == b, isExact a = true
-    | otherwise         = constFold $ sugarSym (T $ Op Eq (==)) a b
+    | otherwise         = constFold $ sugarSym (T $ Op BiEq) a b
 
 -- | In-equality
 (#!=) :: (Eq a, CType a) => CExp a -> CExp a -> CExp Bool
 a #!= b
     | a == b, isExact a = false
-    | otherwise         = constFold $ sugarSym (T $ Op Ne (/=)) a b
+    | otherwise         = constFold $ sugarSym (T $ Op BiNEq) a b
 
 (#<) :: (Ord a, CType a) => CExp a -> CExp a -> CExp Bool
 a #< b
     | a == b, isExact a = false
-    | otherwise         = constFold $ sugarSym (T $ Op Lt (<)) a b
+    | otherwise         = constFold $ sugarSym (T $ Op BiLt) a b
 
 (#>) :: (Ord a, CType a) => CExp a -> CExp a -> CExp Bool
 a #> b
     | a == b, isExact a = false
-    | otherwise         = constFold $ sugarSym (T $ Op Gt (>)) a b
+    | otherwise         = constFold $ sugarSym (T $ Op BiGt) a b
 
 (#<=) :: (Ord a, CType a) => CExp a -> CExp a -> CExp Bool
 a #<= b
     | a == b, isExact a = true
-    | otherwise         = constFold $ sugarSym (T $ Op Le (<=)) a b
+    | otherwise         = constFold $ sugarSym (T $ Op BiLe) a b
 
 (#>=) :: (Ord a, CType a) => CExp a -> CExp a -> CExp Bool
 a #>= b
     | a == b, isExact a = true
-    | otherwise         = constFold $ sugarSym (T $ Op Ge (>=)) a b
+    | otherwise         = constFold $ sugarSym (T $ Op BiGe) a b
 
 infix 4 #==, #!=, #<, #>, #<=, #>=
 
@@ -354,12 +468,10 @@
     -> CExp a     -- ^ True branch
     -> CExp a     -- ^ False branch
     -> CExp a
+cond (LitP c) t f = if c then t else f
 cond c t f
-    | Just c' <- viewLit c = if c' then t else f
     | t == f = t
-cond (CExp (nt :$ a)) t f
-    | Just (T (UOp Lnot _)) <- prj nt
-    , Just a' <- castAST a = cond (CExp a') f t
+cond (UOpP UnNot a) t f = cond (CExp a) f t
 cond c t f = constFold $ sugarSym (T Cond) c t f
 
 -- | Condition operator; use as follows:
@@ -377,8 +489,12 @@
 
 infixl 1 ?
 
+-- | Array indexing
+(#!) :: (CType a, Integral i, Ix i) => IArr i a -> CExp i -> CExp a
+arr #! i = sugarSym (T $ ArrIx arr) i
 
 
+
 --------------------------------------------------------------------------------
 -- Instances
 --------------------------------------------------------------------------------
@@ -387,14 +503,20 @@
 deriveSymbol ''Sym
 #endif
 
-#if MIN_VERSION_syntactic(3,0,0)
 instance Render Sym
   where
-    renderSym (Fun name _) = name
-    renderSym (UOp op _)   = show op
-    renderSym (Op op _)    = show op
-    renderSym (Cast _)     = "cast"
-    renderSym (Var v)      = v
+    renderSym (Lit a _)      = a
+    renderSym (Const _ a _)  = a
+    renderSym (Fun _ name _) = name
+    renderSym (UOp op)       = show $ unaryOp op
+    renderSym (Op op)        = show $ binaryOp op
+    renderSym (Cast _)       = "cast"
+    renderSym (Var v)        = v
+    renderSym (ArrIx (IArrComp arr)) = "ArrIx " ++ arr
+    renderSym (ArrIx _)              = "ArrIx ..."
+
+#if MIN_VERSION_syntactic(3,0,0)
+
     renderArgs = renderArgsSmart
 
 instance Equality Sym
@@ -424,11 +546,7 @@
 
 instance Semantic Sym
   where
-    semantics (Fun name f) = Sem name f
-    semantics (UOp op f)   = Sem (show op) f
-    semantics (Op op f)    = Sem (show op) f
-    semantics (Cast f)     = Sem "cast" f
-    semantics (Var v)      = Sem v undefined
+    semantics s = Sem (renderSym s) (evalSym s)
 
 instance Equality Sym
   where
diff --git a/src/Language/Embedded/Concurrent.hs b/src/Language/Embedded/Concurrent.hs
--- a/src/Language/Embedded/Concurrent.hs
+++ b/src/Language/Embedded/Concurrent.hs
@@ -17,28 +17,31 @@
 
 -- | Fork off a computation as a new thread.
 fork :: (ThreadCMD :<: instr)
-     => ProgramT instr m ()
-     -> ProgramT instr m ThreadId
+     => ProgramT instr (Param2 exp pred) m ()
+     -> ProgramT instr (Param2 exp pred) m ThreadId
 fork = forkWithId . const
 
 -- | Fork off a computation as a new thread, with access to its own thread ID.
 forkWithId :: (ThreadCMD :<: instr)
-           => (ThreadId -> ProgramT instr m ())
-           -> ProgramT instr m ThreadId
+           => (ThreadId -> ProgramT instr (Param2 exp pred) m ())
+           -> ProgramT instr (Param2 exp pred) m ThreadId
 forkWithId = singleton . inj . ForkWithId
 
 -- | Forcibly terminate a thread, then continue execution immediately.
-asyncKillThread :: (ThreadCMD :<: instr) => ThreadId -> ProgramT instr m ()
+asyncKillThread :: (ThreadCMD :<: instr)
+                => ThreadId -> ProgramT instr (Param2 exp pred) m ()
 asyncKillThread = singleton . inj . Kill
 
 -- | Forcibly terminate a thread. Blocks until the thread is actually dead.
-killThread :: (ThreadCMD :<: instr, Monad m) => ThreadId -> ProgramT instr m ()
+killThread :: (ThreadCMD :<: instr, Monad m)
+           => ThreadId -> ProgramT instr (Param2 exp pred) m ()
 killThread t = do
   singleton . inj $ Kill t
   waitThread t
 
 -- | Wait for a thread to terminate.
-waitThread :: (ThreadCMD :<: instr) => ThreadId -> ProgramT instr m ()
+waitThread :: (ThreadCMD :<: instr)
+           => ThreadId -> ProgramT instr (Param2 exp pred) m ()
 waitThread = singleton . inj . Wait
 
 -- | Create a new channel. Writing a reference type to a channel will copy the
@@ -46,50 +49,53 @@
 --
 --   We'll likely want to change this, actually copying arrays and the like
 --   into the queue instead of sharing them across threads.
-newChan :: (VarPred (IExp instr) a, ChanCMD (IExp instr) :<: instr)
-        => IExp instr ChanBound
-        -> ProgramT instr m (Chan Uncloseable a)
-newChan = singleE . NewChan
+newChan :: (pred a, ChanCMD :<: instr)
+        => exp ChanBound
+        -> ProgramT instr (Param2 exp pred) m (Chan Uncloseable a)
+newChan = singleInj . NewChan
 
-newCloseableChan :: (VarPred (IExp instr) a, ChanCMD (IExp instr) :<: instr)
-        => IExp instr ChanBound
-        -> ProgramT instr m (Chan Closeable a)
-newCloseableChan = singleE . NewChan
+newCloseableChan :: (pred a, ChanCMD :<: instr)
+        => exp ChanBound
+        -> ProgramT instr (Param2 exp pred) m (Chan Closeable a)
+newCloseableChan = singleInj . NewChan
 
 -- | Read an element from a channel. If channel is empty, blocks until there
 --   is an item available.
 --   If 'closeChan' has been called on the channel *and* if the channel is
 --   empty, @readChan@ returns an undefined value immediately.
-readChan :: (VarPred (IExp instr) a, ChanCMD (IExp instr) :<: instr)
+readChan :: (pred a, FreeExp exp, VarPred exp a, ChanCMD :<: instr, Monad m)
          => Chan t a
-         -> ProgramT instr m (IExp instr a)
-readChan = singleE . ReadChan
+         -> ProgramT instr (Param2 exp pred) m (exp a)
+readChan = fmap valToExp . singleInj . ReadChan
 
 -- | Write a data element to a channel.
 --   If 'closeChan' has been called on the channel, all calls to @writeChan@
 --   become non-blocking no-ops and return @False@, otherwise returns @True@.
-writeChan :: (VarPred (IExp instr) a,
-              VarPred (IExp instr) Bool,
-              ChanCMD (IExp instr) :<: instr)
+writeChan :: (pred a,
+              FreeExp exp,
+              VarPred exp Bool,
+              ChanCMD :<: instr,
+              Monad m
+             )
         => Chan t a
-        -> IExp instr a
-        -> ProgramT instr m (IExp instr Bool)
-writeChan c = singleE . WriteChan c
+        -> exp a
+        -> ProgramT instr (Param2 exp pred) m (exp Bool)
+writeChan c = fmap valToExp . singleInj . WriteChan c
 
 -- | When 'readChan' was last called on the given channel, did the read
 --   succeed?
 --   Always returns @True@ unless 'closeChan' has been called on the channel.
 --   Always returns @True@ if the channel has never been read.
-lastChanReadOK :: (VarPred (IExp instr) Bool, ChanCMD (IExp instr) :<: instr)
+lastChanReadOK :: (FreeExp exp, VarPred exp Bool, ChanCMD :<: instr, Monad m)
                => Chan Closeable a
-               -> ProgramT instr m (IExp instr Bool)
-lastChanReadOK = singleE . ReadOK
+               -> ProgramT instr (Param2 exp pred) m (exp Bool)
+lastChanReadOK = fmap valToExp . singleInj . ReadOK
 
 -- | Close a channel. All subsequent write operations will be no-ops.
 --   After the channel is drained, all subsequent read operations will be
 --   no-ops as well.
-closeChan :: (ChanCMD (IExp instr) :<: instr)
+closeChan :: (ChanCMD :<: instr)
           => Chan Closeable a
-          -> ProgramT instr m ()
-closeChan = singleE . CloseChan
+          -> ProgramT instr (Param2 exp pred) m ()
+closeChan = singleInj . CloseChan
 
diff --git a/src/Language/Embedded/Concurrent/Backend/C.hs b/src/Language/Embedded/Concurrent/Backend/C.hs
--- a/src/Language/Embedded/Concurrent/Backend/C.hs
+++ b/src/Language/Embedded/Concurrent/Backend/C.hs
@@ -9,9 +9,9 @@
 import Control.Applicative
 #endif
 import Control.Monad.Operational.Higher
-import Data.Proxy
 import Language.Embedded.Expression
 import Language.Embedded.Concurrent.CMD
+import Language.Embedded.Backend.C.Expression
 import Language.C.Quote.C
 import Language.C.Monad
 import qualified Language.C.Syntax as C
@@ -19,19 +19,19 @@
 
 
 instance ToIdent ThreadId where
-  toIdent (TIDComp tid) = C.Id $ "t" ++ show tid
+  toIdent (TIDComp tid) = C.Id tid
 
 instance ToIdent (Chan t a) where
-  toIdent (ChanComp c) = C.Id $ "chan" ++ show c
+  toIdent (ChanComp c) = C.Id c
 
 threadFun :: ThreadId -> String
 threadFun tid = "thread_" ++ show tid
 
 -- | Compile `ThreadCMD`.
 --   TODO: sharing for threads with the same body
-compThreadCMD :: ThreadCMD CGen a -> CGen a
+compThreadCMD :: ThreadCMD (Param3 CGen exp pred) a -> CGen a
 compThreadCMD (ForkWithId body) = do
-  tid <- TIDComp <$> freshId
+  tid <- TIDComp <$> gensym "t"
   let funName = threadFun tid
   _ <- inFunctionTy [cty|void*|] funName $ do
     addParam [cparam| void* unused |]
@@ -50,38 +50,37 @@
   addStm [cstm| pthread_join($id:tid, NULL); |]
 
 -- | Compile `ChanCMD`.
-compChanCMD :: forall exp prog a. CompExp exp
-            => ChanCMD exp prog a
+compChanCMD :: CompExp exp
+            => ChanCMD (Param3 CGen exp CType) a
             -> CGen a
 compChanCMD cmd@(NewChan sz) = do
   addLocalInclude "chan.h"
-  t <- compTypePP2 (Proxy :: Proxy exp) cmd
+  t <- cType (proxyArg cmd)
   sz' <- compExp sz
-  c <- ChanComp <$> freshId
+  c <- ChanComp <$> gensym "chan"
   addGlobal [cedecl| typename chan_t $id:c; |]
   addStm [cstm| $id:c = chan_new(sizeof($ty:t), $sz'); |]
   return c
-compChanCMD (WriteChan c x) = do
-  x' <- compExp x
-  (v,name) <- freshVar
-  (ok,okname) <- freshVar
-  let _ = v `asTypeOf` x
-  addStm [cstm| $id:name = $x'; |]
-  addStm [cstm| $id:okname = chan_write($id:c, &$id:name); |]
+compChanCMD (WriteChan c (x :: exp a)) = do
+  x'         <- compExp x
+  v :: Val a <- freshVar
+  ok         <- freshVar
+  addStm [cstm| $id:v = $x'; |]
+  addStm [cstm| $id:ok = chan_write($id:c, &$id:v); |]
   return ok
 compChanCMD (ReadChan c) = do
-  (var,name) <- freshVar
-  addStm [cstm| chan_read($id:c, &$id:name); |]
+  var <- freshVar
+  addStm [cstm| chan_read($id:c, &$id:var); |]
   return var
 compChanCMD (CloseChan c) = do
   addStm [cstm| chan_close($id:c); |]
 compChanCMD (ReadOK c) = do
-  (var,name) <- freshVar
-  addStm [cstm| $id:name = chan_last_read_ok($id:c); |]
+  var <- freshVar
+  addStm [cstm| $id:var = chan_last_read_ok($id:c); |]
   return var
 
-instance Interp ThreadCMD CGen where
+instance Interp ThreadCMD CGen (Param2 exp pred) where
   interp = compThreadCMD
-instance CompExp exp => Interp (ChanCMD exp) CGen where
+instance CompExp exp => Interp ChanCMD CGen (Param2 exp CType) where
   interp = compChanCMD
 
diff --git a/src/Language/Embedded/Concurrent/CMD.hs b/src/Language/Embedded/Concurrent/CMD.hs
--- a/src/Language/Embedded/Concurrent/CMD.hs
+++ b/src/Language/Embedded/Concurrent/CMD.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE CPP #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 module Language.Embedded.Concurrent.CMD (
     TID, ThreadId (..),
@@ -13,8 +14,8 @@
 #if __GLASGOW_HASKELL__ < 710
 import Control.Applicative
 #endif
-import Control.Monad
 import Control.Monad.Operational.Higher
+import Control.Monad.Reader
 import Data.IORef
 import Data.Typeable
 import Language.Embedded.Expression
@@ -61,7 +62,7 @@
 
 instance Show ThreadId where
   show (TIDEval tid _) = show tid
-  show (TIDComp tid)   = show tid
+  show (TIDComp tid)   = tid
 
 data Closeable
 data Uncloseable
@@ -71,38 +72,57 @@
   = ChanEval (Bounded.BoundedChan a) (IORef Bool) (IORef Bool)
   | ChanComp CID
 
-data ThreadCMD (prog :: * -> *) a where
-  ForkWithId :: (ThreadId -> prog ()) -> ThreadCMD prog ThreadId
-  Kill       :: ThreadId -> ThreadCMD prog ()
-  Wait       :: ThreadId -> ThreadCMD prog ()
+data ThreadCMD fs a where
+  ForkWithId :: (ThreadId -> prog ()) -> ThreadCMD (Param3 prog exp pred) ThreadId
+  Kill       :: ThreadId -> ThreadCMD (Param3 prog exp pred) ()
+  Wait       :: ThreadId -> ThreadCMD (Param3 prog exp pred) ()
 
-data ChanCMD exp (prog :: * -> *) a where
-  NewChan   :: VarPred exp a => exp ChanBound -> ChanCMD exp prog (Chan t a)
-  ReadChan  :: VarPred exp a => Chan t a -> ChanCMD exp prog (exp a)
-  WriteChan :: (VarPred exp a, VarPred exp Bool)
-            => Chan t a -> exp a -> ChanCMD exp prog (exp Bool)
-  CloseChan :: Chan Closeable a -> ChanCMD exp prog ()
-  ReadOK    :: VarPred exp Bool
-            => Chan Closeable a -> ChanCMD exp prog (exp Bool)
+data ChanCMD fs a where
+  NewChan   :: pred a => exp ChanBound -> ChanCMD (Param3 prog exp pred) (Chan t a)
+  ReadChan  :: pred a => Chan t a -> ChanCMD (Param3 prog exp pred) (Val a)
+  WriteChan :: pred a
+            => Chan t a -> exp a -> ChanCMD (Param3 prog exp pred) (Val Bool)
+  CloseChan :: Chan Closeable a -> ChanCMD (Param3 prog exp pred) ()
+  ReadOK    :: Chan Closeable a -> ChanCMD (Param3 prog exp pred) (Val Bool)
 
 instance HFunctor ThreadCMD where
   hfmap f (ForkWithId p) = ForkWithId $ f . p
   hfmap _ (Kill tid)     = Kill tid
   hfmap _ (Wait tid)     = Wait tid
 
-instance HFunctor (ChanCMD exp) where
+instance HBifunctor ThreadCMD where
+  hbimap f _ (ForkWithId p) = ForkWithId $ f . p
+  hbimap _ _ (Kill tid)     = Kill tid
+  hbimap _ _ (Wait tid)     = Wait tid
+
+instance (ThreadCMD :<: instr) => Reexpressible ThreadCMD instr where
+  reexpressInstrEnv reexp (ForkWithId p) = ReaderT $ \env ->
+      singleInj $ ForkWithId (flip runReaderT env . p)
+  reexpressInstrEnv reexp (Kill tid) = lift $ singleInj $ Kill tid
+  reexpressInstrEnv reexp (Wait tid) = lift $ singleInj $ Wait tid
+
+instance HFunctor ChanCMD where
   hfmap _ (NewChan sz)    = NewChan sz
   hfmap _ (ReadChan c)    = ReadChan c
   hfmap _ (WriteChan c x) = WriteChan c x
   hfmap _ (CloseChan c)   = CloseChan c
   hfmap _ (ReadOK c)      = ReadOK c
 
-type instance IExp (ThreadCMD :+: i) = IExp i
+instance HBifunctor ChanCMD where
+  hbimap _ f (NewChan sz)    = NewChan (f sz)
+  hbimap _ _ (ReadChan c)    = ReadChan c
+  hbimap _ f (WriteChan c x) = WriteChan c (f x)
+  hbimap _ _ (CloseChan c)   = CloseChan c
+  hbimap _ _ (ReadOK c)      = ReadOK c
 
-type instance IExp (ChanCMD e)       = e
-type instance IExp (ChanCMD e :+: i) = e
+instance (ChanCMD :<: instr) => Reexpressible ChanCMD instr where
+  reexpressInstrEnv reexp (NewChan sz)    = lift . singleInj . NewChan =<< reexp sz
+  reexpressInstrEnv reexp (ReadChan c)    = lift $ singleInj $ ReadChan c
+  reexpressInstrEnv reexp (WriteChan c x) = lift . singleInj . WriteChan c =<< reexp x
+  reexpressInstrEnv reexp (CloseChan c)   = lift $ singleInj $ CloseChan c
+  reexpressInstrEnv reexp (ReadOK c)      = lift $ singleInj $ ReadOK c
 
-runThreadCMD :: ThreadCMD IO a
+runThreadCMD :: ThreadCMD (Param3 IO exp pred) a
              -> IO a
 runThreadCMD (ForkWithId p) = do
   f <- newFlag
@@ -118,10 +138,10 @@
 runThreadCMD (Wait (TIDEval _ f)) = do
   waitFlag f
 
-runChanCMD :: forall exp a. EvalExp exp
-           => ChanCMD exp IO a -> IO a
-runChanCMD (NewChan sz) =
-  ChanEval <$> Bounded.newBoundedChan (fromIntegral $ evalExp sz)
+runChanCMD :: ChanCMD (Param3 IO IO pred) a -> IO a
+runChanCMD (NewChan sz) = do
+  sz' <- sz
+  ChanEval <$> Bounded.newBoundedChan (fromIntegral sz')
            <*> newIORef False
            <*> newIORef True
 runChanCMD (ReadChan (ChanEval c closedref lastread)) = do
@@ -129,25 +149,26 @@
   mval <- Bounded.tryReadChan c
   case mval of
     Just x -> do
-        return $ litExp x
+        return $ ValEval x
     Nothing
       | closed -> do
         writeIORef lastread False
         return undefined
       | otherwise -> do
-        litExp <$> Bounded.readChan c
+        ValEval <$> Bounded.readChan c
 runChanCMD (WriteChan (ChanEval c closedref _) x) = do
   closed <- readIORef closedref
+  x' <- x
   if closed
-    then return (litExp False)
-    else Bounded.writeChan c (evalExp x) >> return (litExp True)
+    then return (ValEval False)
+    else Bounded.writeChan c x' >> return (ValEval True)
 runChanCMD (CloseChan (ChanEval _ closedref _)) = do
   writeIORef closedref True
 runChanCMD (ReadOK (ChanEval _ _ lastread)) = do
-  litExp <$> readIORef lastread
+  ValEval <$> readIORef lastread
 
-instance Interp ThreadCMD IO where
-  interp = runThreadCMD
-instance EvalExp exp => Interp (ChanCMD exp) IO where
-  interp = runChanCMD
+instance InterpBi ThreadCMD IO (Param1 pred) where
+  interpBi = runThreadCMD
+instance InterpBi ChanCMD IO (Param1 pred) where
+  interpBi = runChanCMD
 
diff --git a/src/Language/Embedded/Expression.hs b/src/Language/Embedded/Expression.hs
--- a/src/Language/Embedded/Expression.hs
+++ b/src/Language/Embedded/Expression.hs
@@ -1,93 +1,53 @@
-{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE CPP #-}
 
--- | Interface for evaluation and compilation of pure expressions
-module Language.Embedded.Expression
-  ( VarId
-  , VarPred
-  , EvalExp(..)
-  , CompExp(..)
-  , freshVar
-  , freshVar_
-  )
-  where
+-- | Interface to pure expressions
 
-import Data.Proxy
-import Data.Constraint
-import Language.C.Monad
-import Language.C.Quote.C
-import Language.C.Syntax (Exp,Type)
-import qualified Language.C.Syntax as C
+module Language.Embedded.Expression where
 
 
 
--- | Constraint on the types of variables in a given expression language
-type family VarPred (exp :: * -> *) :: * -> Constraint
+import Data.Typeable
 
--- | General interface for evaluating expressions
-class EvalExp exp
-  where
-    -- | Literal expressions
-    litExp  :: VarPred exp a => a -> exp a
+import GHC.Prim (Constraint)
 
-    -- | Evaluation of (closed) expressions
-    evalExp :: exp a -> a
+import Language.C.Quote.C (ToIdent (..))
 
--- | General interface for compiling expressions
-class CompExp exp where
-    -- | Variable expressions
-    varExp  :: VarPred exp a => VarId -> exp a
 
-    -- | Compilation of expressions
-    --
-    -- /NOTE: It is assumed that free variables in the expression are rendered as @vIII@, where/
-    -- /      @III@ is the variable identifier./
-    compExp :: (MonadC m) => exp a -> m Exp
 
-    -- | Extract expression type
-    compType :: forall m a
-             .  (MonadC m, VarPred exp a)
-             => exp a -> m Type
-    compType _ = compTypeP (Proxy :: Proxy (exp a))
-    {-# INLINE compType #-}
+-- | Variable identifier
+type VarId = String
 
-    -- | Extract expression type
-    compTypeP :: forall proxy m a
-              .  (MonadC m, VarPred exp a)
-              => proxy (exp a) -> m Type
-    compTypeP _ = compTypePP (Proxy :: Proxy exp) (Proxy :: Proxy a)
-    {-# INLINE compTypeP #-}
+-- | Expressions that support injection of values and named variables
+class FreeExp exp
+  where
+    -- | Constraint on the types of values and variables in an expression
+    -- language
+    type VarPred exp :: * -> Constraint
 
-    -- | Extract expression type
-    compTypePP :: forall proxy1 proxy2 m a
-               .  (MonadC m, VarPred exp a)
-               => proxy1 exp -> proxy2 a -> m Type
-    compTypePP _ _ = compTypePP2 (Proxy :: Proxy exp) (Proxy :: Proxy (Proxy a))
-    {-# INLINE compTypePP #-}
+    -- | Construct a value expression
+    valExp :: VarPred exp a => a -> exp a
 
-    -- | Extract expression type
-    compTypePP2 :: forall proxy proxy1 proxy2 m a
-                .  (MonadC m, VarPred exp a)
-                => proxy exp -> proxy1 (proxy2 a) -> m Type
-    compTypePP2 _ _ = compType (undefined :: exp a)
-    {-# INLINE compTypePP2 #-}
+    -- | Construct a named variable expression
+    varExp :: VarPred exp a => VarId -> exp a
 
-    {-# MINIMAL varExp , compExp , (compType | compTypeP | compTypePP | compTypePP2 ) #-}
+-- | Value
+data Val a
+    = ValComp VarId  -- ^ Symbolic value
+    | ValEval a      -- ^ Concrete value
+  deriving Typeable
 
--- | Variable identifier
-type VarId = Integer
+instance ToIdent (Val a) where toIdent (ValComp r) = toIdent r
 
--- | Create and declare a fresh variable and return its name
-freshVar :: forall exp m a. (CompExp exp, VarPred exp a, MonadC m) => m (exp a, C.Id)
-freshVar = do
-    v <- fmap varExp freshId
-    t <- compTypeP (Proxy :: Proxy (exp a))
-    C.Var n _ <- compExp v
-    touchVar n
-    case t of
-      C.Type _ C.Ptr{} _ -> addLocal [cdecl| $ty:t $id:n = NULL; |]
-      _                  -> addLocal [cdecl| $ty:t $id:n; |]
-    return (v,n)
+-- | Convert a value to an expression
+valToExp :: (VarPred exp a, FreeExp exp) => Val a -> exp a
+valToExp (ValComp v) = varExp v
+valToExp (ValEval a) = valExp a
 
--- | Create and declare a fresh variable
-freshVar_ :: forall exp m a. (CompExp exp, VarPred exp a, MonadC m) => m (exp a)
-freshVar_ = fst `fmap` freshVar
+-- | Expressions that support evaluation
+class FreeExp exp => EvalExp exp
+    -- The super class is motivated by the fact that evaluation of functions
+    -- `exp a -> exp b` can be done by constructing an argument using `valExp`.
+  where
+    -- | Evaluation of a closed expression
+    evalExp :: exp a -> a
+
diff --git a/src/Language/Embedded/Imperative.hs b/src/Language/Embedded/Imperative.hs
--- a/src/Language/Embedded/Imperative.hs
+++ b/src/Language/Embedded/Imperative.hs
@@ -8,38 +8,40 @@
 -- type MyProg exp a = `Program` (`RefCMD` exp `:+:` `FileCMD` exp) a
 -- @
 --
--- Also, instructions are parameterized on the expression language. In the above
--- example, @exp@ can be any type (of kind @* -> *@) that implements the
--- 'EvalExp' and 'CompExp' classes.
+-- Also, instructions are parameterized on the expression language.
 --
 -- Some examples of using the library are found in the @examples@ directory.
 
 module Language.Embedded.Imperative
-  ( module Control.Monad
-  , module Data.Int
-  , module Data.Word
-    -- * Program monad
+  ( -- * Program monad
+    module Control.Monad
   , ProgramT
   , Program
   , interpretT
   , interpret
+  , interpretBiT
+  , interpretBi
+  , Param1
+  , Param2
+  , Param3
     -- * Imperative instructions
   , RefCMD
   , ArrCMD
   , ControlCMD
+  , PtrCMD
   , FileCMD
-  , CallCMD
-    -- * Types of Printf arguments
-  , PrintfArg
+  , C_CMD
     -- * Composing instruction sets
   , (:+:)
   , (:<:)
-  , IExp
-    -- * Interpreting expressions
+    -- * Interface for expression types
+  , FreeExp
   , VarPred
   , EvalExp
   , CompExp
     -- * Front end
+  , module Data.Int
+  , module Data.Word
   , module Language.Embedded.Imperative.Frontend.General
   , module Language.Embedded.Imperative.Frontend
   ) where
@@ -56,5 +58,6 @@
 import Language.Embedded.Imperative.CMD
 import Language.Embedded.Imperative.Frontend.General
 import Language.Embedded.Imperative.Frontend
+import Language.Embedded.Backend.C.Expression
 import Language.Embedded.Imperative.Backend.C ()
 
diff --git a/src/Language/Embedded/Imperative/Args.hs b/src/Language/Embedded/Imperative/Args.hs
--- a/src/Language/Embedded/Imperative/Args.hs
+++ b/src/Language/Embedded/Imperative/Args.hs
@@ -1,100 +1,75 @@
 {-# LANGUAGE QuasiQuotes #-}
-{-# LANGUAGE PolyKinds   #-}
 
 -- | Various types of function arguments
 
 module Language.Embedded.Imperative.Args where
 
-import Control.Monad
 import Data.Proxy
+
 import Language.C.Quote.C
-import Language.C.Syntax
-import Language.Embedded.Expression
+import Language.C.Syntax hiding (Deref)
+
+import Language.C.Monad
 import Language.Embedded.Imperative.CMD
 import Language.Embedded.Backend.C
 
--- | Value argument
-data ValArg exp where
-  ValArg :: VarPred exp a => exp a -> ValArg exp
-
-instance Arg ValArg where
-  mkArg   (ValArg a) = compExp a
-  mkParam (ValArg a) = do
-    t <- compType a
-    return [cparam| $ty:t |]
-
-  mapArg predCast f (ValArg (a :: exp a)) =
-    predCast (Proxy :: Proxy a) $ ValArg (f a)
-
-  mapMArg predCast f (ValArg (a :: exp a)) =
-    predCast (Proxy :: Proxy a) $ liftM ValArg (f a)
-
 -- | Reference argument
-data RefArg exp where
-  RefArg :: VarPred exp a => Ref a -> RefArg exp
+data RefArg pred where
+  RefArg :: pred a => Ref a -> RefArg pred
 
-instance Arg RefArg where
-  mkArg   (RefArg r) = return [cexp| &$id:r |]
-  mkParam (RefArg (r :: Ref a) :: RefArg exp) = do
-    t <- compTypeP (Proxy :: Proxy (exp a))
+instance Arg RefArg CType where
+  mkArg   (RefArg r) = touchVar r >> return [cexp| &$id:r |]
+  mkParam (RefArg (r :: Ref a)) = do
+    t <- cType (Proxy :: Proxy a)
     return [cparam| $ty:t* |]
 
-  mapArg predCast _ (RefArg (r :: Ref a)) =
-    predCast (Proxy :: Proxy a) $ RefArg r
+-- | Mutable array argument
+data ArrArg pred where
+  ArrArg :: pred a => Arr i a -> ArrArg pred
 
-  mapMArg predCast _ (RefArg (r :: Ref a)) =
-    predCast (Proxy :: Proxy a) $ return $ RefArg r
+instance Arg ArrArg CType where
+  mkArg   (ArrArg a) = touchVar a >> return [cexp| $id:a |]
+  mkParam (ArrArg (_ :: Arr i a)) = do
+    t <- cType (Proxy :: Proxy a)
+    return [cparam| $ty:t* |]
 
--- | Array argument
-data ArrArg exp where
-  ArrArg :: VarPred exp a => Arr n a -> ArrArg exp
+-- | Immutable array argument
+data IArrArg pred where
+  IArrArg :: pred a => IArr i a -> IArrArg pred
 
-instance Arg ArrArg where
-  mkArg   (ArrArg a) = return [cexp| $id:a |]
-  mkParam (ArrArg (a :: Arr n a) :: ArrArg exp) = do
-    t <- compTypeP (Proxy :: Proxy (exp a))
+instance Arg IArrArg CType where
+  mkArg   (IArrArg a) = touchVar a >> return [cexp| $id:a |]
+  mkParam (IArrArg (_ :: IArr i a)) = do
+    t <- cType (Proxy :: Proxy a)
     return [cparam| $ty:t* |]
 
-  mapArg predCast _ (ArrArg (a :: Arr n a)) =
-    predCast (Proxy :: Proxy a) $ ArrArg a
+-- | Pointer argument
+data PtrArg pred where
+  PtrArg :: pred a => Ptr a -> PtrArg pred
 
-  mapMArg predCast _ (ArrArg (a :: Arr n a)) =
-    predCast (Proxy :: Proxy a) $ return $ ArrArg a
+instance Arg PtrArg CType where
+  mkArg   (PtrArg p) = touchVar p >> return [cexp| $id:p |]
+  mkParam (PtrArg (_ :: Ptr a)) = do
+    t <- cType (Proxy :: Proxy a)
+    return [cparam| $ty:t* |]
 
 -- | Abstract object argument
-data ObjArg exp where
-  ObjArg :: Object -> ObjArg exp
-
-instance Arg ObjArg where
-  mkArg   (ObjArg o) = return [cexp| $id:o |]
-  mkParam (ObjArg (Object True t _))  = let t' = namedType t in return [cparam| $ty:t'* |]
-  mkParam (ObjArg (Object False t _)) = let t' = namedType t in return [cparam| $ty:t' |]
-  mapArg  _ _ (ObjArg o) = ObjArg o
-  mapMArg _ _ (ObjArg o) = return $ ObjArg o
+data ObjArg pred where
+  ObjArg :: Object -> ObjArg pred
 
+instance Arg ObjArg pred where
+  mkArg   (ObjArg o) = touchVar o >> return [cexp| $id:o |]
+  mkParam (ObjArg (Object pointed t _))
+      | pointed   = return [cparam| $ty:t'* |]
+      | otherwise = return [cparam| $ty:t'  |]
+    where
+      t' = namedType t
 
 -- | Constant string argument
-data StrArg exp where
-  StrArg :: String -> StrArg exp
+data StrArg pred where
+  StrArg :: String -> StrArg pred
 
-instance Arg StrArg where
+instance Arg StrArg pred where
   mkArg   (StrArg s) = return [cexp| $string:s |]
   mkParam (StrArg s) = return [cparam| const char* |]
-  mapArg  _ _ (StrArg s) = StrArg s
-  mapMArg _ _ (StrArg s) = return $ StrArg s
-
--- | Modifier that takes the address of another argument
-newtype Addr arg exp = Addr (arg exp)
-
-instance Arg arg => Arg (Addr arg) where
-  mkArg (Addr arg) = do
-    e <- mkArg arg
-    return [cexp| &$e |]
-  mkParam (Addr arg) = do
-    p <- mkParam arg
-    case p of
-       Param mid spec decl loc -> return $ Param mid spec (Ptr [] decl loc) loc
-       _ -> error "Cannot deal with antiquotes"
-  mapArg  predCast f (Addr arg) = Addr (mapArg predCast f arg)
-  mapMArg predCast f (Addr arg) = liftM Addr (mapMArg predCast f arg)
 
diff --git a/src/Language/Embedded/Imperative/Backend/C.hs b/src/Language/Embedded/Imperative/Backend/C.hs
--- a/src/Language/Embedded/Imperative/Backend/C.hs
+++ b/src/Language/Embedded/Imperative/Backend/C.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 -- | C code generation for imperative commands
 
@@ -23,62 +24,108 @@
 import Language.Embedded.Imperative.Frontend.General
 import Language.Embedded.Backend.C
 
+
+
 -- | Compile `RefCMD`
-compRefCMD :: forall exp prog a. CompExp exp
-           => RefCMD exp prog a -> CGen a
-compRefCMD cmd@NewRef = do
-    t <- compTypePP2 (Proxy :: Proxy exp) cmd
-    r <- RefComp <$> freshId
-    case t of
-      C.Type _ C.Ptr{} _ -> addLocal [cdecl| $ty:t $id:r = NULL; |]
-      _                  -> addLocal [cdecl| $ty:t $id:r; |]
+compRefCMD :: CompExp exp => RefCMD (Param3 prog exp CType) a -> CGen a
+compRefCMD cmd@(NewRef base) = do
+    t <- cType (proxyArg cmd)
+    r <- RefComp <$> gensym base
+    addLocal $ case t of
+      C.Type _ C.Ptr{} _ -> [cdecl| $ty:t $id:r = NULL; |]
+      _                  -> [cdecl| $ty:t $id:r; |]
     return r
-compRefCMD (InitRef exp) = do
-    t <- compType exp
-    r <- RefComp <$> freshId
-    v <- compExp exp
+compRefCMD (InitRef base exp) = do
+    t <- cType exp
+    r <- RefComp <$> gensym base
+    e <- compExp exp
     addLocal [cdecl| $ty:t $id:r; |]
-    addStm   [cstm| $id:r = $v; |]
+    addStm   [cstm| $id:r = $e; |]
     return r
 compRefCMD (GetRef ref) = do
-    (v,_) <- freshVar
-    e <- compExp v
+    v <- freshVar
     touchVar ref
-    addStm [cstm| $e = $id:ref; |]
+    addStm [cstm| $id:v = $id:ref; |]
     return v
 compRefCMD (SetRef ref exp) = do
     v <- compExp exp
     touchVar ref
     addStm [cstm| $id:ref = $v; |]
+compRefCMD (UnsafeFreezeRef (RefComp v)) = return $ ValComp v
 
+-- The `IsPointer` instance for `Arr` demands that arrays are represented as
+-- pointers in C (because `IsPointer` enables use of `SwapPtr`). As explained
+-- [here](http://stackoverflow.com/questions/3393518/swap-arrays-by-using-pointers-in-c),
+-- arrays in C are *not* pointers in the sense that they can be redirected. Here
+-- "arrays" means variables declared as e.g. `int arr[10];`. This is why we
+-- declare a supplementary pointer for such arrays; e.g:
+--
+--     int _a[] = {0,1,2,3,4,5,6,7,8,9};
+--     int * a = _a;
+--
+-- This extra pointer is not needed when using `alloca` since then the array is
+-- a pointer anyway. One option might be to use `alloca` for all arrays, but
+-- that doesn't permit defining constant arrays using a literal as above.
+--
+-- Pointers that are used between multiple functions will be lifted to shared globals.
+-- To ensure the correctness of the resulting program the underlying arrays must also
+-- be lifted, hence the extra `touchVar` application on their symbols.
+
 -- | Compile `ArrCMD`
-compArrCMD :: forall exp prog a. CompExp exp
-           => ArrCMD exp prog a -> CGen a
-compArrCMD cmd@(NewArr size) = do
-    sym <- gensym "a"
-    v   <- compExp size
-    t   <- compTypePP2 (Proxy :: Proxy exp) cmd
-    addLocal [cdecl| $ty:t $id:sym[ $v ]; |]
+compArrCMD :: CompExp exp => ArrCMD (Param3 prog exp CType) a -> CGen a
+compArrCMD cmd@(NewArr base size) = do
+    sym <- gensym base
+    let sym' = '_':sym
+    n <- compExp size
+    t <- cType (proxyArg cmd)
+    case n of
+      C.Const _ _ -> do
+        addLocal [cdecl| $ty:t $id:sym'[ $n ]; |]
+        addLocal [cdecl| $ty:t * $id:sym = $id:sym'; |]  -- explanation above
+      _ -> do
+        addInclude "<alloca.h>"
+        addLocal [cdecl| $ty:t * $id:sym; |]
+        addStm [cstm| $id:sym = alloca($n * sizeof($ty:t)); |]
     return $ ArrComp sym
-compArrCMD cmd@(NewArr_) = do
-    sym <- gensym "a"
-    t   <- compTypePP2 (Proxy :: Proxy exp) cmd
-    addLocal [cdecl| $ty:t * $id:sym; |]
+compArrCMD cmd@(InitArr base as) = do
+    sym <- gensym base
+    let sym' = '_':sym
+    t   <- cType (proxyArg cmd)
+    as' <- mapM cLit as
+    addLocal [cdecl| $ty:t $id:sym'[] = $init:(arrayInit as');|]
+    addLocal [cdecl| $ty:t * $id:sym = $id:sym'; |]  -- explanation above
     return $ ArrComp sym
 compArrCMD (GetArr expi arr) = do
-    (v,n) <- freshVar
-    i     <- compExp expi
+    v <- freshVar
+    i <- compExp expi
+    touchVar $ BaseArrOf arr  -- explanation above
     touchVar arr
-    addStm [cstm| $id:n = $id:arr[ $i ]; |]
+    addStm [cstm| $id:v = $id:arr[ $i ]; |]
     return v
 compArrCMD (SetArr expi expv arr) = do
     v <- compExp expv
     i <- compExp expi
+    touchVar $ BaseArrOf arr  -- explanation above
     touchVar arr
     addStm [cstm| $id:arr[ $i ] = $v; |]
+compArrCMD cmd@(CopyArr arr1 arr2 expl) = do
+    addInclude "<string.h>"
+    mapM_ touchVar [BaseArrOf arr1,BaseArrOf arr2]  -- explanation above
+    mapM_ touchVar [arr1,arr2]
+    l <- compExp expl
+    t <- cType arr1
+    addStm [cstm| memcpy($id:arr1, $id:arr2, $l * sizeof($ty:t)); |]
+compArrCMD (UnsafeFreezeArr (ArrComp arr)) = return $ IArrComp arr
+compArrCMD (UnsafeThawArr (IArrComp arr))  = return $ ArrComp arr
 
+-- | Generates the symbol name as an identifier for a given array.
+newtype BaseArrOf i a = BaseArrOf (Arr i a)
+instance ToIdent (BaseArrOf i a)
+    where toIdent (BaseArrOf (ArrComp sym)) = toIdent $ '_':sym
+
+
 -- | Compile `ControlCMD`
-compControlCMD :: CompExp exp => ControlCMD exp CGen a -> CGen a
+compControlCMD :: CompExp exp => ControlCMD (Param3 CGen exp CType) a -> CGen a
 compControlCMD (If c t f) = do
     cc <- compExp c
     ct <- inNewBlock_ t
@@ -107,14 +154,38 @@
               _      -> addStm [cstm| if (! $contc) {break;} |]
         body
     when (not noop) $ addStm [cstm| while (1) {$items:bodyc} |]
-compControlCMD (For lo hi body) = do
-    loe   <- compExp lo
-    hie   <- compExp hi
-    (i,n) <- freshVar
+compControlCMD (For (lo,step,hi) body) = do
+    loe <- compExp lo
+    hie <- compExp $ borderVal hi
+    i   <- freshVar
     bodyc <- inNewBlock_ (body i)
-    addStm [cstm| for ($id:n=$loe; $id:n<=$hie; $id:n++) {$items:bodyc} |]
+    let incl = borderIncl hi
+    let conte
+          | incl && (step>=0) = [cexp| $id:i<=$hie |]
+          | incl && (step<0)  = [cexp| $id:i>=$hie |]
+          | step >= 0         = [cexp| $id:i< $hie |]
+          | step < 0          = [cexp| $id:i> $hie |]
+    let stepe
+          | step == 1    = [cexp| $id:i++ |]
+          | step == (-1) = [cexp| $id:i-- |]
+          | step == 0    = [cexp| 0 |]
+          | step >  0    = [cexp| $id:i = $id:i + $step |]
+          | step <  0    = [cexp| $id:i = $id:i - $(negate step) |]
+    addStm [cstm| for ($id:i=$loe; $conte; $stepe) {$items:bodyc} |]
 compControlCMD Break = addStm [cstm| break; |]
+compControlCMD (Assert cond msg) = do
+    addInclude "<assert.h>"
+    c <- compExp cond
+    addStm [cstm| assert($c && $msg); |]
 
+compPtrCMD :: PtrCMD (Param3 prog exp pred) a -> CGen a
+compPtrCMD (SwapPtr a b) = do
+    sym <- gensym "tmp"
+    addLocal [cdecl| void * $id:sym; |]
+    addStm   [cstm| $id:sym = $id:a; |]
+    addStm   [cstm| $id:a = $id:b; |]
+    addStm   [cstm| $id:b = $id:sym; |]
+
 compIOMode :: IOMode -> String
 compIOMode ReadMode      = "r"
 compIOMode WriteMode     = "w"
@@ -122,11 +193,11 @@
 compIOMode ReadWriteMode = "r+"
 
 -- | Compile `FileCMD`
-compFileCMD :: CompExp exp => FileCMD exp CGen a -> CGen a
+compFileCMD :: CompExp exp => FileCMD (Param3 prog exp CType) a -> CGen a
 compFileCMD (FOpen path mode) = do
     addInclude "<stdio.h>"
     addInclude "<stdlib.h>"
-    sym <- gensym "v"
+    sym <- gensym "f"
     addLocal [cdecl| typename FILE * $id:sym; |]
     addStm   [cstm| $id:sym = fopen($id:path',$string:mode'); |]
     return $ HandleComp sym
@@ -134,6 +205,7 @@
     path' = show path
     mode' = compIOMode mode
 compFileCMD (FClose h) = do
+    addInclude "<stdio.h>"
     touchVar h
     addStm [cstm| fclose($id:h); |]
 compFileCMD (FPrintf h form as) = do
@@ -145,56 +217,61 @@
     as' <- fmap ([h',form'']++) $ sequence [compExp a | PrintfArg a <- as]
     addStm [cstm| fprintf($args:as'); |]
 compFileCMD cmd@(FGet h) = do
-    (v,n) <- freshVar
+    addInclude "<stdio.h>"
+    v <- freshVar
     touchVar h
-    let mkProxy = (\_ -> Proxy) :: FileCMD exp prog (exp a) -> Proxy a
+    let mkProxy = (\_ -> Proxy) :: FileCMD (Param3 prog exp pred) (Val a) -> Proxy a
         form    = formatSpecifier (mkProxy cmd)
-    addStm [cstm| fscanf($id:h, $string:form, &$id:n); |]
+    addStm [cstm| fscanf($id:h, $string:form, &$id:v); |]
     return v
 compFileCMD (FEof h) = do
     addInclude "<stdbool.h>"
-    (v,n) <- freshVar
+    addInclude "<stdio.h>"
+    v <- freshVar
     touchVar h
-    addStm [cstm| $id:n = feof($id:h); |]
+    addStm [cstm| $id:v = feof($id:h); |]
     return v
 
-compObjectCMD :: CompExp exp => ObjectCMD exp CGen a -> CGen a
-compObjectCMD (NewObject t) = do
-    sym <- gensym "obj"
-    let t' = namedType t
-    addLocal [cdecl| $ty:t' * $id:sym; |]
-    return $ Object True t sym
-compObjectCMD (InitObject fun pnt t args) = do
-    sym <- gensym "obj"
+compC_CMD :: CompExp exp => C_CMD (Param3 CGen exp CType) a -> CGen a
+compC_CMD cmd@(NewPtr base) = do
+    addInclude "<stddef.h>"
+    p <- PtrComp <$> gensym base
+    t <- cType (proxyArg cmd)
+    addLocal [cdecl| $ty:t * $id:p = NULL; |]
+    return p
+compC_CMD (PtrToArr (PtrComp p)) = return $ ArrComp p
+compC_CMD (NewObject base t pointed) = do
+    o <- Object pointed t <$> gensym base
     let t' = namedType t
-    as  <- mapM mkArg args
-    addLocal [cdecl| $ty:t' * $id:sym; |]
-    addStm   [cstm|  $id:sym = $id:fun($args:as); |]
-    return $ Object pnt t sym
-
-compCallCMD :: CompExp exp => CallCMD exp CGen a -> CGen a
-compCallCMD (AddInclude inc)    = addInclude inc
-compCallCMD (AddDefinition def) = addGlobal def
-compCallCMD (AddExternFun fun res args) = do
-    tres  <- compTypeP res
+    if pointed
+      then addLocal [cdecl| $ty:t' * $id:o; |]
+      else addLocal [cdecl| $ty:t' $id:o; |]
+    return o
+compC_CMD (AddInclude inc)    = addInclude inc
+compC_CMD (AddDefinition def) = addGlobal def
+compC_CMD (AddExternFun fun res args) = do
+    tres  <- cType res
     targs <- mapM mkParam args
     addGlobal [cedecl| extern $ty:tres $id:fun($params:targs); |]
-compCallCMD (AddExternProc proc args) = do
+compC_CMD (AddExternProc proc args) = do
     targs <- mapM mkParam args
     addGlobal [cedecl| extern void $id:proc($params:targs); |]
-compCallCMD (CallFun fun as) = do
-    as'   <- mapM mkArg as
-    (v,n) <- freshVar
-    addStm [cstm| $id:n = $id:fun($args:as'); |]
+compC_CMD (CallFun fun as) = do
+    as' <- mapM mkArg as
+    v   <- freshVar
+    addStm [cstm| $id:v = $id:fun($args:as'); |]
     return v
-compCallCMD (CallProc fun as) = do
+compC_CMD (CallProc obj fun as) = do
     as' <- mapM mkArg as
-    addStm [cstm| $id:fun($args:as'); |]
+    case obj of
+      Nothing -> addStm [cstm| $id:fun($args:as'); |]
+      Just o  -> addStm [cstm| $id:o = $id:fun($args:as'); |]
+compC_CMD (InModule mod prog) = inModule mod prog
 
-instance CompExp exp => Interp (RefCMD exp)     CGen where interp = compRefCMD
-instance CompExp exp => Interp (ArrCMD exp)     CGen where interp = compArrCMD
-instance CompExp exp => Interp (ControlCMD exp) CGen where interp = compControlCMD
-instance CompExp exp => Interp (FileCMD exp)    CGen where interp = compFileCMD
-instance CompExp exp => Interp (ObjectCMD exp)  CGen where interp = compObjectCMD
-instance CompExp exp => Interp (CallCMD exp)    CGen where interp = compCallCMD
+instance CompExp exp => Interp RefCMD     CGen (Param2 exp CType) where interp = compRefCMD
+instance CompExp exp => Interp ArrCMD     CGen (Param2 exp CType) where interp = compArrCMD
+instance CompExp exp => Interp ControlCMD CGen (Param2 exp CType) where interp = compControlCMD
+instance                Interp PtrCMD     CGen (Param2 exp pred)  where interp = compPtrCMD
+instance CompExp exp => Interp FileCMD    CGen (Param2 exp CType) where interp = compFileCMD
+instance CompExp exp => Interp C_CMD      CGen (Param2 exp CType) where interp = compC_CMD
 
diff --git a/src/Language/Embedded/Imperative/CMD.hs b/src/Language/Embedded/Imperative/CMD.hs
--- a/src/Language/Embedded/Imperative/CMD.hs
+++ b/src/Language/Embedded/Imperative/CMD.hs
@@ -1,10 +1,12 @@
 {-# LANGUAGE CPP #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 -- | Imperative commands. These commands can be used with the 'Program' monad,
 -- and different command types can be combined using (':+:').
 --
 -- These commands are general imperative constructs independent of the back end,
--- except for 'CallCMD' which is C-specific.
+-- except for 'C_CMD' which is C-specific.
 
 module Language.Embedded.Imperative.CMD
   ( -- * References
@@ -12,40 +14,56 @@
   , RefCMD (..)
     -- * Arrays
   , Arr (..)
+  , IArr (..)
   , ArrCMD (..)
     -- * Control flow
+  , Border (..)
+  , borderVal
+  , borderIncl
+  , IxRange
   , ControlCMD (..)
+    -- * Pointers
+  , IsPointer (..)
+  , PtrCMD (..)
     -- * File handling
   , Handle (..)
   , stdin
   , stdout
+  , PrintfArg (..)
+  , mapPrintfArg
+  , mapPrintfArgM
   , Formattable (..)
   , FileCMD (..)
-  , PrintfArg (..)
-    -- * Abstract objects
+    -- * C-specific commands
+  , Ptr (..)
   , Object (..)
-  , ObjectCMD (..)
-    -- * External function calls (C-specific)
-  , FunArg (..)
-  , VarPredCast
   , Arg (..)
-  , CallCMD (..)
+  , FunArg (..)
+  , mapFunArg
+  , mapFunArgM
+  , Assignable
+  , C_CMD (..)
   ) where
 
 
 
+import Control.Monad.Reader
+import Data.Array
 import Data.Array.IO
 import Data.Char (isSpace)
 import Data.Int
 import Data.IORef
+import Data.List
 import Data.Typeable
 import Data.Word
 import System.IO (IOMode (..))
 import qualified System.IO as IO
 import qualified Text.Printf as Printf
 
-#if __GLASGOW_HASKELL__ < 708
-import Data.Proxy
+#if __GLASGOW_HASKELL__ < 710
+import Control.Applicative
+import Data.Foldable hiding (sequence_)
+import Data.Traversable (Traversable, traverse)
 #endif
 
 import Control.Monad.Operational.Higher
@@ -53,11 +71,15 @@
 import Control.Monads
 import Language.Embedded.Expression
 import Language.Embedded.Traversal
+
+-- C-specific imports:
 import qualified Language.C.Syntax as C
-import Language.C.Quote.C (ToIdent (..))
-import Language.C.Monad
+import Language.C.Quote.C
+import Language.C.Monad (CGen)
+import Language.Embedded.Backend.C.Expression
 
 
+
 --------------------------------------------------------------------------------
 -- * References
 --------------------------------------------------------------------------------
@@ -68,134 +90,287 @@
     | RefEval (IORef a)
   deriving Typeable
 
--- | Identifiers from references
-instance ToIdent (Ref a)
-  where
-    toIdent (RefComp r) = C.Id ('v' : show r)
+instance ToIdent (Ref a) where toIdent (RefComp r) = C.Id r
 
 -- | Commands for mutable references
-data RefCMD exp (prog :: * -> *) a
+data RefCMD fs a
   where
-    NewRef  :: VarPred exp a => RefCMD exp prog (Ref a)
-    InitRef :: VarPred exp a => exp a -> RefCMD exp prog (Ref a)
-    GetRef  :: VarPred exp a => Ref a -> RefCMD exp prog (exp a)
-    SetRef  :: VarPred exp a => Ref a -> exp a -> RefCMD exp prog ()
-      -- `VarPred` for `SetRef` is not needed for code generation, but it can be useful when
-      -- interpreting with a dynamically typed store. `VarPred` can then be used to supply a
-      -- `Typeable` dictionary for casting.
+    NewRef  :: pred a => String -> RefCMD (Param3 prog exp pred) (Ref a)
+    InitRef :: pred a => String -> exp a -> RefCMD (Param3 prog exp pred) (Ref a)
+    GetRef  :: pred a => Ref a -> RefCMD (Param3 prog exp pred) (Val a)
+    SetRef  :: pred a => Ref a -> exp a -> RefCMD (Param3 prog exp pred) ()
+      -- `pred a` for `SetRef` is not needed for code generation, but it can be
+      -- useful when interpreting with a dynamically typed store. It can then be
+      -- used e.g. to supply a `Typeable` constraint for casting.
+    UnsafeFreezeRef :: pred a => Ref a -> RefCMD (Param3 prog exp pred) (Val a)
+      -- Like `GetRef` but without using a fresh variable for the result. This
+      -- is only safe if the reference is never written to after the freezing.
 #if  __GLASGOW_HASKELL__>=708
   deriving Typeable
 #endif
 
-instance HFunctor (RefCMD exp)
+instance HFunctor RefCMD
   where
-    hfmap _ NewRef       = NewRef
-    hfmap _ (InitRef a)  = InitRef a
-    hfmap _ (GetRef r)   = GetRef r
-    hfmap _ (SetRef r a) = SetRef r a
+    hfmap _ (NewRef base)       = NewRef base
+    hfmap _ (InitRef base a)    = InitRef base a
+    hfmap _ (GetRef r)          = GetRef r
+    hfmap _ (SetRef r a)        = SetRef r a
+    hfmap _ (UnsafeFreezeRef r) = UnsafeFreezeRef r
 
-instance CompExp exp => DryInterp (RefCMD exp)
+instance HBifunctor RefCMD
   where
-    dryInterp NewRef       = liftM RefComp fresh
-    dryInterp (InitRef _)  = liftM RefComp fresh
-    dryInterp (GetRef _)   = liftM varExp fresh
-    dryInterp (SetRef _ _) = return ()
+    hbimap _ _ (NewRef base)       = NewRef base
+    hbimap _ f (InitRef base a)    = InitRef base (f a)
+    hbimap _ _ (GetRef r)          = GetRef r
+    hbimap _ f (SetRef r a)        = SetRef r (f a)
+    hbimap _ _ (UnsafeFreezeRef r) = UnsafeFreezeRef r
 
-type instance IExp (RefCMD e)       = e
-type instance IExp (RefCMD e :+: i) = e
+instance (RefCMD :<: instr) => Reexpressible RefCMD instr
+  where
+    reexpressInstrEnv reexp (NewRef base)       = lift $ singleInj $ NewRef base
+    reexpressInstrEnv reexp (InitRef base a)    = lift . singleInj . InitRef base =<< reexp a
+    reexpressInstrEnv reexp (GetRef r)          = lift $ singleInj $ GetRef r
+    reexpressInstrEnv reexp (SetRef r a)        = lift . singleInj . SetRef r =<< reexp a
+    reexpressInstrEnv reexp (UnsafeFreezeRef r) = lift $ singleInj $ UnsafeFreezeRef r
 
+instance DryInterp RefCMD
+  where
+    dryInterp (NewRef base)    = liftM RefComp $ freshStr base
+    dryInterp (InitRef base _) = liftM RefComp $ freshStr base
+    dryInterp (GetRef _)       = liftM ValComp $ freshStr "v"
+    dryInterp (SetRef _ _)     = return ()
+    dryInterp (UnsafeFreezeRef (RefComp v)) = return $ ValComp v
 
 
+
 --------------------------------------------------------------------------------
 -- * Arrays
 --------------------------------------------------------------------------------
 
 -- | Mutable array
-data Arr n a
-    = ArrComp String
-    | ArrEval (IOArray n a)
+data Arr i a
+    = ArrComp VarId
+    | ArrEval (IORef (IOArray i a))
+        -- The `IORef` is needed in order to make the `IsPointer` instance
   deriving Typeable
 
--- | Identifiers from arrays
-instance ToIdent (Arr i a)
-  where
-    toIdent (ArrComp arr) = C.Id arr
+-- | Immutable array
+data IArr i a
+    = IArrComp VarId
+    | IArrEval (Array i a)
+        -- The `IORef` is needed in order to make the `IsPointer` instance
+  deriving Typeable
 
+-- In a way, it's not terribly useful to have `Arr` parameterized on the index
+-- type, since it's required to be an integer type, and it doesn't really matter
+-- which integer type is used since we can always cast between them.
+--
+-- Another option would be to remove the parameter and allow any integer type
+-- when indexing (and use e.g. `IOArray Word32` for evaluation). However this
+-- has the big downside of losing type inference. E.g. the statement
+-- `getArr arr 0` would be ambiguously typed.
+--
+-- Yet another option is to hard-code a specific index type. But this would
+-- limit the use of arrays to specific platforms.
+--
+-- So in the end, the above representation seems like a good trade-off. A client
+-- of `imperative-edsl` may always chose to make a wrapper interface that uses
+-- a specific index type.
+
+instance ToIdent (Arr i a)  where toIdent (ArrComp arr)  = C.Id arr
+instance ToIdent (IArr i a) where toIdent (IArrComp arr) = C.Id arr
+
 -- | Commands for mutable arrays
-data ArrCMD exp (prog :: * -> *) a
+data ArrCMD fs a
   where
-    NewArr :: (VarPred exp a, VarPred exp n, Integral n, Ix n) => exp n -> ArrCMD exp prog (Arr n a)
-    NewArr_ :: (VarPred exp a, VarPred exp n, Integral n, Ix n) => ArrCMD exp prog (Arr n a)
-    GetArr :: (VarPred exp a, Integral n, Ix n)                => exp n -> Arr n a -> ArrCMD exp prog (exp a)
-    SetArr :: (Integral n, Ix n)                               => exp n -> exp a -> Arr n a -> ArrCMD exp prog ()
+    NewArr  :: (pred a, Integral i, Ix i) => String -> exp i -> ArrCMD (Param3 prog exp pred) (Arr i a)
+    InitArr :: (pred a, Integral i, Ix i) => String -> [a] -> ArrCMD (Param3 prog exp pred) (Arr i a)
+    GetArr  :: (pred a, Integral i, Ix i) => exp i -> Arr i a -> ArrCMD (Param3 prog exp pred) (Val a)
+    SetArr  :: (pred a, Integral i, Ix i) => exp i -> exp a -> Arr i a -> ArrCMD (Param3 prog exp pred) ()
+    CopyArr :: (pred a, Integral i, Ix i) => Arr i a -> Arr i a -> exp i -> ArrCMD (Param3 prog exp pred) ()
+    UnsafeFreezeArr :: (pred a, Integral i, Ix i) => Arr i a -> ArrCMD (Param3 prog exp pred) (IArr i a)
+    UnsafeThawArr   :: (pred a, Integral i, Ix i) => IArr i a -> ArrCMD (Param3 prog exp pred) (Arr i a)
 #if  __GLASGOW_HASKELL__>=708
   deriving Typeable
 #endif
+  -- Not all `pred` constraints are needed by the back ends in imperative-edsl,
+  -- but they may still be useful for other back ends.
 
-instance HFunctor (ArrCMD exp)
+instance HFunctor ArrCMD
   where
-    hfmap _ (NewArr n)       = NewArr n
-    hfmap _ (NewArr_)        = NewArr_
-    hfmap _ (GetArr i arr)   = GetArr i arr
-    hfmap _ (SetArr i a arr) = SetArr i a arr
+    hfmap _ (NewArr base n)       = NewArr base n
+    hfmap _ (InitArr base as)     = InitArr base as
+    hfmap _ (GetArr i arr)        = GetArr i arr
+    hfmap _ (SetArr i a arr)      = SetArr i a arr
+    hfmap _ (CopyArr a1 a2 l)     = CopyArr a1 a2 l
+    hfmap _ (UnsafeFreezeArr arr) = UnsafeFreezeArr arr
+    hfmap _ (UnsafeThawArr arr)   = UnsafeThawArr arr
 
-instance CompExp exp => DryInterp (ArrCMD exp)
+instance HBifunctor ArrCMD
   where
-    dryInterp (NewArr _)   = liftM ArrComp $ freshStr "a"
-    dryInterp (NewArr_)      = liftM ArrComp $ freshStr "a"
-    dryInterp (GetArr _ _)   = liftM varExp fresh
-    dryInterp (SetArr _ _ _) = return ()
+    hbimap _ f (NewArr base n)       = NewArr base (f n)
+    hbimap _ _ (InitArr base as)     = InitArr base as
+    hbimap _ f (GetArr i arr)        = GetArr (f i) arr
+    hbimap _ f (SetArr i a arr)      = SetArr (f i) (f a) arr
+    hbimap _ f (CopyArr a1 a2 l)     = CopyArr a1 a2 (f l)
+    hbimap _ _ (UnsafeFreezeArr arr) = UnsafeFreezeArr arr
+    hbimap _ _ (UnsafeThawArr arr)   = UnsafeThawArr arr
 
-type instance IExp (ArrCMD e)       = e
-type instance IExp (ArrCMD e :+: i) = e
+instance (ArrCMD :<: instr) => Reexpressible ArrCMD instr
+  where
+    reexpressInstrEnv reexp (NewArr base n)       = lift . singleInj . NewArr base =<< reexp n
+    reexpressInstrEnv reexp (InitArr base as)     = lift $ singleInj $ InitArr base as
+    reexpressInstrEnv reexp (GetArr i arr)        = lift . singleInj . flip GetArr arr =<< reexp i
+    reexpressInstrEnv reexp (SetArr i a arr)      = do i' <- reexp i; a' <- reexp a; lift $ singleInj $ SetArr i' a' arr
+    reexpressInstrEnv reexp (CopyArr a1 a2 l)     = lift . singleInj . CopyArr a1 a2 =<< reexp l
+    reexpressInstrEnv reexp (UnsafeFreezeArr arr) = lift $ singleInj $ UnsafeFreezeArr arr
+    reexpressInstrEnv reexp (UnsafeThawArr arr)   = lift $ singleInj $ UnsafeThawArr arr
 
+instance DryInterp ArrCMD
+  where
+    dryInterp (NewArr base _)  = liftM ArrComp $ freshStr base
+    dryInterp (InitArr base _) = liftM ArrComp $ freshStr base
+    dryInterp (GetArr _ _)     = liftM ValComp $ freshStr "v"
+    dryInterp (SetArr _ _ _)   = return ()
+    dryInterp (CopyArr _ _ _)  = return ()
+    dryInterp (UnsafeFreezeArr (ArrComp arr)) = return (IArrComp arr)
+    dryInterp (UnsafeThawArr (IArrComp arr))  = return (ArrComp arr)
 
 
+
 --------------------------------------------------------------------------------
 -- * Control flow
 --------------------------------------------------------------------------------
 
-data ControlCMD exp prog a
+data Border i = Incl i | Excl i
+  deriving (Eq, Show, Functor, Foldable, Traversable)
+
+-- | 'fromInteger' gives an inclusive border. No other methods defined.
+instance Num i => Num (Border i)
   where
-    If    :: exp Bool -> prog () -> prog () -> ControlCMD exp prog ()
-    While :: prog (exp Bool) -> prog () -> ControlCMD exp prog ()
-    For   :: (VarPred exp n, Integral n) =>
-             exp n -> exp n -> (exp n -> prog ()) -> ControlCMD exp prog ()
-    Break :: ControlCMD exp prog ()
+    fromInteger = Incl . fromInteger
+    (+) = error "(+) not defined for Border"
+    (-) = error "(-) not defined for Border"
+    (*) = error "(*) not defined for Border"
+    abs    = error "abs not defined for Border"
+    signum = error "signum not defined for Border"
 
-instance HFunctor (ControlCMD exp)
+borderVal :: Border i -> i
+borderVal (Incl i) = i
+borderVal (Excl i) = i
+
+borderIncl :: Border i -> Bool
+borderIncl (Incl _) = True
+borderIncl _        = False
+
+-- | Index range
+--
+-- @(lo,step,hi)@
+--
+-- @lo@ gives the start index; @step@ gives the step length; @hi@ gives the stop
+-- index which may be inclusive or exclusive.
+type IxRange i = (i, Int, Border i)
+
+data ControlCMD fs a
   where
-    hfmap g (If c t f)        = If c (g t) (g f)
-    hfmap g (While cont body) = While (g cont) (g body)
-    hfmap g (For lo hi body)  = For lo hi (g . body)
+    If     :: exp Bool -> prog () -> prog () -> ControlCMD (Param3 prog exp pred) ()
+    While  :: prog (exp Bool) -> prog () -> ControlCMD (Param3 prog exp pred) ()
+    For    :: (pred i, Integral i) => IxRange (exp i) -> (Val i -> prog ()) -> ControlCMD (Param3 prog exp pred) ()
+    Break  :: ControlCMD (Param3 prog exp pred) ()
+    Assert :: exp Bool -> String -> ControlCMD (Param3 prog exp pred) ()
+
+instance HFunctor ControlCMD
+  where
+    hfmap f (If c thn els)    = If c (f thn) (f els)
+    hfmap f (While cont body) = While (f cont) (f body)
+    hfmap f (For rng body)    = For rng (f . body)
     hfmap _ Break             = Break
+    hfmap _ (Assert cond msg) = Assert cond msg
 
-instance DryInterp (ControlCMD exp)
+instance HBifunctor ControlCMD
   where
-    dryInterp (If _ _ _)  = return ()
-    dryInterp (While _ _) = return ()
-    dryInterp (For _ _ _) = return ()
-    dryInterp Break       = return ()
+    hbimap f g (If c thn els)          = If (g c) (f thn) (f els)
+    hbimap f g (While cont body)       = While (f $ fmap g cont) (f body)
+    hbimap f g (For (lo,step,hi) body) = For (g lo, step, fmap g hi) (f . body)
+    hbimap _ _ Break                   = Break
+    hbimap _ g (Assert cond msg)       = Assert (g cond) msg
 
-type instance IExp (ControlCMD e)       = e
-type instance IExp (ControlCMD e :+: i) = e
+instance (ControlCMD :<: instr) => Reexpressible ControlCMD instr
+  where
+    reexpressInstrEnv reexp (If c thn els) = do
+        c' <- reexp c
+        ReaderT $ \env ->
+          singleInj $ If c' (runReaderT thn env) (runReaderT els env)
+    reexpressInstrEnv reexp (While cont body) = ReaderT $ \env ->
+        singleInj $ While
+            (runReaderT (cont >>= reexp) env)
+            (runReaderT body env)
+    reexpressInstrEnv reexp (For (lo,step,hi) body) = do
+        lo' <- reexp lo
+        hi' <- traverse reexp hi
+        ReaderT $ \env -> singleInj $
+            For (lo',step,hi') (flip runReaderT env . body)
+    reexpressInstrEnv reexp Break             = lift $ singleInj Break
+    reexpressInstrEnv reexp (Assert cond msg) = lift . singleInj . flip Assert msg =<< reexp cond
 
+instance DryInterp ControlCMD
+  where
+    dryInterp (If _ _ _)   = return ()
+    dryInterp (While _ _)  = return ()
+    dryInterp (For _ _)    = return ()
+    dryInterp Break        = return ()
+    dryInterp (Assert _ _) = return ()
 
 
+
 --------------------------------------------------------------------------------
+-- * Pointers
+--------------------------------------------------------------------------------
+
+-- The reason for not implementing `SwapPtr` using the `Ptr` type is that it's
+-- (currently) not possible to interpret `Ptr` in `IO`.
+
+-- | Types that are represented as a pointers in C
+class ToIdent a => IsPointer a
+  where
+    runSwapPtr :: a -> a -> IO ()
+
+instance IsPointer (Arr i a)
+  where
+    runSwapPtr (ArrEval arr1) (ArrEval arr2) = do
+        arr1' <- readIORef arr1
+        arr2' <- readIORef arr2
+        writeIORef arr1 arr2'
+        writeIORef arr2 arr1'
+
+data PtrCMD fs a
+  where
+    SwapPtr :: IsPointer a => a -> a -> PtrCMD (Param3 prog exp pred) ()
+
+instance HFunctor   PtrCMD where hfmap _    (SwapPtr a b) = SwapPtr a b
+instance HBifunctor PtrCMD where hbimap _ _ (SwapPtr a b) = SwapPtr a b
+
+instance (PtrCMD :<: instr) => Reexpressible PtrCMD instr
+  where
+    reexpressInstrEnv reexp (SwapPtr a b) = lift $ singleInj (SwapPtr a b)
+
+instance DryInterp PtrCMD
+  where
+    dryInterp (SwapPtr _ _) = return ()
+
+
+
+--------------------------------------------------------------------------------
 -- * File handling
 --------------------------------------------------------------------------------
 
 -- | File handle
 data Handle
-    = HandleComp String
+    = HandleComp VarId
     | HandleEval IO.Handle
   deriving Typeable
 
--- | Identifiers from handles
-instance ToIdent Handle
-  where
-    toIdent (HandleComp h) = C.Id h
+instance ToIdent Handle where toIdent (HandleComp h) = C.Id h
 
 -- | Handle to stdin
 stdin :: Handle
@@ -205,6 +380,20 @@
 stdout :: Handle
 stdout = HandleComp "stdout"
 
+data PrintfArg exp
+  where
+    PrintfArg :: Printf.PrintfArg a => exp a -> PrintfArg exp
+
+mapPrintfArg
+    :: (forall a . exp1 a -> exp2 a)
+    -> PrintfArg exp1 -> PrintfArg exp2
+mapPrintfArg f (PrintfArg exp) = PrintfArg (f exp)
+
+mapPrintfArgM :: Monad m
+    => (forall a . exp1 a -> m (exp2 a))
+    -> PrintfArg exp1 -> m (PrintfArg exp2)
+mapPrintfArgM f (PrintfArg exp) = liftM PrintfArg (f exp)
+
 -- | Values that can be printed\/scanned using @printf@\/@scanf@
 class (Typeable a, Read a, Printf.PrintfArg a) => Formattable a
   where
@@ -223,18 +412,15 @@
 instance Formattable Float  where formatSpecifier _ = "%f"
 instance Formattable Double where formatSpecifier _ = "%f"
 
-data FileCMD exp (prog :: * -> *) a
+data FileCMD fs a
   where
-    FOpen   :: FilePath -> IOMode                       -> FileCMD exp prog Handle
-    FClose  :: Handle                                   -> FileCMD exp prog ()
-    FEof    :: VarPred exp Bool => Handle               -> FileCMD exp prog (exp Bool)
-    FPrintf :: Handle -> String -> [PrintfArg exp]      -> FileCMD exp prog ()
-    FGet    :: (Formattable a, VarPred exp a) => Handle -> FileCMD exp prog (exp a)
-
-data PrintfArg exp where
-  PrintfArg :: (Printf.PrintfArg a, VarPred exp a) => exp a -> PrintfArg exp
+    FOpen   :: FilePath -> IOMode                  -> FileCMD (Param3 prog exp pred) Handle
+    FClose  :: Handle                              -> FileCMD (Param3 prog exp pred) ()
+    FEof    :: Handle                              -> FileCMD (Param3 prog exp pred) (Val Bool)
+    FPrintf :: Handle -> String -> [PrintfArg exp] -> FileCMD (Param3 prog exp pred) ()
+    FGet    :: (pred a, Formattable a) => Handle   -> FileCMD (Param3 prog exp pred) (Val a)
 
-instance HFunctor (FileCMD exp)
+instance HFunctor FileCMD
   where
     hfmap _ (FOpen file mode)     = FOpen file mode
     hfmap _ (FClose hdl)          = FClose hdl
@@ -242,129 +428,183 @@
     hfmap _ (FGet hdl)            = FGet hdl
     hfmap _ (FEof hdl)            = FEof hdl
 
-instance CompExp exp => DryInterp (FileCMD exp)
+instance HBifunctor FileCMD
   where
+    hbimap _ _ (FOpen file mode)     = FOpen file mode
+    hbimap _ _ (FClose hdl)          = FClose hdl
+    hbimap _ f (FPrintf hdl form as) = FPrintf hdl form (map (mapPrintfArg f) as)
+    hbimap _ _ (FGet hdl)            = FGet hdl
+    hbimap _ _ (FEof hdl)            = FEof hdl
+
+instance (FileCMD :<: instr) => Reexpressible FileCMD instr
+  where
+    reexpressInstrEnv reexp (FOpen file mode)   = lift $ singleInj $ FOpen file mode
+    reexpressInstrEnv reexp (FClose h)          = lift $ singleInj $ FClose h
+    reexpressInstrEnv reexp (FEof h)            = lift $ singleInj $ FEof h
+    reexpressInstrEnv reexp (FPrintf h form as) = lift . singleInj . FPrintf h form =<< mapM (mapPrintfArgM reexp) as
+    reexpressInstrEnv reexp (FGet h)            = lift $ singleInj $ FGet h
+
+instance DryInterp FileCMD
+  where
     dryInterp (FOpen _ _)     = liftM HandleComp $ freshStr "h"
     dryInterp (FClose _)      = return ()
     dryInterp (FPrintf _ _ _) = return ()
-    dryInterp (FGet _)        = liftM varExp fresh
-    dryInterp (FEof _)        = liftM varExp fresh
-
-type instance IExp (FileCMD e)       = e
-type instance IExp (FileCMD e :+: i) = e
+    dryInterp (FGet _)        = liftM ValComp $ freshStr "v"
+    dryInterp (FEof _)        = liftM ValComp $ freshStr "v"
 
 
 
 --------------------------------------------------------------------------------
--- * Abstract objects
+-- * C-specific commands
 --------------------------------------------------------------------------------
 
+-- | Pointer
+newtype Ptr (a :: *) = PtrComp {ptrId :: VarId}
+  deriving Typeable
+
+instance ToIdent (Ptr a) where toIdent = C.Id . ptrId
+
+-- | Abstract object
 data Object = Object
     { pointed    :: Bool
     , objectType :: String
-    , objectId   :: String
+    , objectId   :: VarId
     }
   deriving (Eq, Show, Ord, Typeable)
 
--- | Identifiers from objects
-instance ToIdent Object
-  where
-    toIdent (Object _ _ o) = C.Id o
+instance ToIdent Object where toIdent (Object _ _ o) = C.Id o
 
-data ObjectCMD exp (prog :: * -> *) a
+class Arg arg pred
   where
-    NewObject
-        :: String  -- Type
-        -> ObjectCMD exp prog Object
-    InitObject
-        :: String -- Function name
-        -> Bool   -- Pointed object?
-        -> String -- Object Type
-        -> [FunArg exp]
-        -> ObjectCMD exp prog Object
+    mkArg   :: arg pred -> CGen C.Exp
+    mkParam :: arg pred -> CGen C.Param
 
-instance HFunctor (ObjectCMD exp)
+data FunArg exp pred
   where
-    hfmap _ (NewObject t)        = NewObject t
-    hfmap _ (InitObject s p t a) = InitObject s p t a
+    ValArg   :: pred a => exp a -> FunArg exp pred
+    AddrArg  :: FunArg exp pred -> FunArg exp pred
+    DerefArg :: FunArg exp pred -> FunArg exp pred
+    FunArg   :: Arg arg pred => arg pred -> FunArg exp pred
 
-instance DryInterp (ObjectCMD exp)
+instance CompExp exp => Arg (FunArg exp) CType
   where
-    dryInterp (NewObject t)        = liftM (Object True t) $ freshStr "obj"
-    dryInterp (InitObject _ _ t _) = liftM (Object True t) $ freshStr "obj"
-
-type instance IExp (ObjectCMD e)       = e
-type instance IExp (ObjectCMD e :+: i) = e
-
-
-
---------------------------------------------------------------------------------
--- * External function calls (C-specific)
---------------------------------------------------------------------------------
+    mkArg (ValArg a) = compExp a
+    mkArg (AddrArg arg) = do
+        e <- mkArg arg
+        return [cexp| &$e |]
+    mkArg (DerefArg arg) = do
+        e <- mkArg arg
+        return [cexp| *$e |]
+    mkArg (FunArg a) = mkArg a
 
-data FunArg exp where
-  FunArg :: Arg arg => arg exp -> FunArg exp
+    mkParam (ValArg (a :: exp a)) = do
+        t <- cType (Proxy :: Proxy a)
+        return [cparam| $ty:t |]
+    mkParam (AddrArg arg) = do
+      p <- mkParam arg
+      case p of
+         C.Param mid spec decl loc -> return $ C.Param mid spec (C.Ptr [] decl loc) loc
+         _ -> error "mkParam for Addr: cannot deal with antiquotes"
+    mkParam (DerefArg arg) = do
+      p <- mkParam arg
+      case p of
+         C.Param mid spec (C.Ptr [] decl _) loc -> return $ C.Param mid spec decl loc
+         C.Param _ _ _ _ -> error "mkParam for Deref: cannot dereference non-pointer parameter"
+         _ -> error "mkParam for Deref: cannot deal with antiquotes"
+    mkParam (FunArg a) = mkParam a
 
--- | Evidence that @`VarPred` exp1@ implies @`VarPred` exp2@
-type VarPredCast exp1 exp2 = forall a b .
-    VarPred exp1 a => Proxy a -> (VarPred exp2 a => b) -> b
+mapFunArg ::
+    (forall a . exp1 a -> exp2 a) -> FunArg exp1 pred -> FunArg exp2 pred
+mapFunArg f (ValArg a)   = ValArg (f a)
+mapFunArg f (AddrArg a)  = AddrArg $ mapFunArg f a
+mapFunArg f (DerefArg a) = DerefArg $ mapFunArg f a
+mapFunArg f (FunArg a)   = FunArg a
 
-class Arg arg where
-  mkArg   :: CompExp exp => arg exp -> CGen C.Exp
-  mkParam :: CompExp exp => arg exp -> CGen C.Param
+mapFunArgM :: Monad m
+    => (forall a . exp1 a -> m (exp2 a))
+    -> FunArg exp1 pred
+    -> m (FunArg exp2 pred)
+mapFunArgM f (ValArg a)   = liftM ValArg (f a)
+mapFunArgM f (AddrArg a)  = liftM AddrArg $ mapFunArgM f a
+mapFunArgM f (DerefArg a) = liftM DerefArg $ mapFunArgM f a
+mapFunArgM f (FunArg a)   = return (FunArg a)
 
-  -- | Map over the expression(s) in an argument
-  mapArg  :: VarPredCast exp1 exp2
-          -> (forall a . VarPred exp1 a => exp1 a -> exp2 a)
-          -> arg exp1
-          -> arg exp2
+class ToIdent obj => Assignable obj
 
-  -- | Monadic map over the expression(s) in an argument
-  mapMArg :: Monad m
-          => VarPredCast exp1 exp2
-          -> (forall a . VarPred exp1 a => exp1 a -> m (exp2 a))
-          -> arg exp1
-          -> m (arg exp2)
+instance Assignable (Ref a)
+instance Assignable (Arr i a)
+instance Assignable (IArr i a)
+instance Assignable (Ptr a)
+instance Assignable Object
 
-instance Arg FunArg where
-  mkArg   (FunArg arg) = mkArg arg
-  mkParam (FunArg arg) = mkParam arg
-  mapArg  predCast f (FunArg arg) = FunArg (mapArg predCast f arg)
-  mapMArg predCast f (FunArg arg) = liftM FunArg (mapMArg predCast f arg)
+data C_CMD fs a
+  where
+    NewPtr   :: pred a => String -> C_CMD (Param3 prog exp pred) (Ptr a)
+    PtrToArr :: Ptr a -> C_CMD (Param3 prog exp pred) (Arr i a)
+    NewObject
+        :: String  -- Base name
+        -> String  -- Type
+        -> Bool    -- Pointed?
+        -> C_CMD (Param3 prog exp pred) Object
+    AddInclude    :: String       -> C_CMD (Param3 prog exp pred) ()
+    AddDefinition :: C.Definition -> C_CMD (Param3 prog exp pred) ()
+    AddExternFun  :: pred res => String -> proxy res -> [FunArg exp pred] -> C_CMD (Param3 prog exp pred) ()
+    AddExternProc :: String -> [FunArg exp pred] -> C_CMD (Param3 prog exp pred) ()
+    CallFun       :: pred a => String -> [FunArg exp pred] -> C_CMD (Param3 prog exp pred) (Val a)
+    CallProc      :: Assignable obj => Maybe obj -> String -> [FunArg exp pred] -> C_CMD (Param3 prog exp pred) ()
+    InModule      :: String -> prog () -> C_CMD (Param3 prog exp pred) ()
 
-data CallCMD exp (prog :: * -> *) a
+instance HFunctor C_CMD
   where
-    AddInclude    :: String       -> CallCMD exp prog ()
-    AddDefinition :: C.Definition -> CallCMD exp prog ()
-    AddExternFun  :: VarPred exp res
-                  => String
-                  -> proxy (exp res)
-                  -> [FunArg exp]
-                  -> CallCMD exp prog ()
-    AddExternProc :: String -> [FunArg exp] -> CallCMD exp prog ()
-    CallFun       :: VarPred exp a => String -> [FunArg exp] -> CallCMD exp prog (exp a)
-    CallProc      ::                  String -> [FunArg exp] -> CallCMD exp prog ()
+    hfmap _ (NewPtr base)             = NewPtr base
+    hfmap _ (PtrToArr p)              = PtrToArr p
+    hfmap _ (NewObject base p t)      = NewObject base p t
+    hfmap _ (AddInclude incl)         = AddInclude incl
+    hfmap _ (AddDefinition def)       = AddDefinition def
+    hfmap _ (AddExternFun fun p args) = AddExternFun fun p args
+    hfmap _ (AddExternProc proc args) = AddExternProc proc args
+    hfmap _ (CallFun fun args)        = CallFun fun args
+    hfmap _ (CallProc obj proc args)  = CallProc obj proc args
+    hfmap f (InModule mod prog)       = InModule mod (f prog)
 
-instance HFunctor (CallCMD exp)
+instance HBifunctor C_CMD
   where
-    hfmap _ (AddInclude incl)           = AddInclude incl
-    hfmap _ (AddDefinition def)         = AddDefinition def
-    hfmap _ (AddExternFun fun res args) = AddExternFun fun res args
-    hfmap _ (AddExternProc proc args)   = AddExternProc proc args
-    hfmap _ (CallFun fun args)          = CallFun fun args
-    hfmap _ (CallProc proc args)        = CallProc proc args
+    hbimap _ _ (NewPtr base)             = NewPtr base
+    hbimap _ _ (PtrToArr p)              = PtrToArr p
+    hbimap _ _ (NewObject base p t)      = NewObject base p t
+    hbimap _ _ (AddInclude incl)         = AddInclude incl
+    hbimap _ _ (AddDefinition def)       = AddDefinition def
+    hbimap _ f (AddExternFun fun p args) = AddExternFun fun p (map (mapFunArg f) args)
+    hbimap _ f (AddExternProc proc args) = AddExternProc proc (map (mapFunArg f) args)
+    hbimap _ f (CallFun fun args)        = CallFun fun (map (mapFunArg f) args)
+    hbimap _ f (CallProc obj proc args)  = CallProc obj proc (map (mapFunArg f) args)
+    hbimap f _ (InModule mod prog)       = InModule mod (f prog)
 
-instance CompExp exp => DryInterp (CallCMD exp)
+instance (C_CMD :<: instr) => Reexpressible C_CMD instr
   where
-    dryInterp (AddInclude _)       = return ()
-    dryInterp (AddDefinition _)    = return ()
-    dryInterp (AddExternFun _ _ _) = return ()
-    dryInterp (AddExternProc _ _)  = return ()
-    dryInterp (CallFun _ _)        = liftM varExp fresh
-    dryInterp (CallProc _ _)       = return ()
+    reexpressInstrEnv reexp (NewPtr base)             = lift $ singleInj $ NewPtr base
+    reexpressInstrEnv reexp (PtrToArr p)              = lift $ singleInj $ PtrToArr p
+    reexpressInstrEnv reexp (NewObject base p t)      = lift $ singleInj $ NewObject base p t
+    reexpressInstrEnv reexp (AddInclude incl)         = lift $ singleInj $ AddInclude incl
+    reexpressInstrEnv reexp (AddDefinition def)       = lift $ singleInj $ AddDefinition def
+    reexpressInstrEnv reexp (AddExternFun fun p args) = lift . singleInj . AddExternFun fun p =<< mapM (mapFunArgM reexp) args
+    reexpressInstrEnv reexp (AddExternProc proc args) = lift . singleInj . AddExternProc proc =<< mapM (mapFunArgM reexp) args
+    reexpressInstrEnv reexp (CallFun fun args)        = lift . singleInj . CallFun fun =<< mapM (mapFunArgM reexp) args
+    reexpressInstrEnv reexp (CallProc obj proc args)  = lift . singleInj . CallProc obj proc =<< mapM (mapFunArgM reexp) args
+    reexpressInstrEnv reexp (InModule mod prog)       = ReaderT $ \env -> singleInj $ InModule mod (runReaderT prog env)
 
-type instance IExp (CallCMD e)       = e
-type instance IExp (CallCMD e :+: i) = e
+instance DryInterp C_CMD
+  where
+    dryInterp (NewPtr base)          = liftM PtrComp $ freshStr base
+    dryInterp (PtrToArr (PtrComp p)) = return $ ArrComp p
+    dryInterp (NewObject base t p)   = liftM (Object p t) $ freshStr base
+    dryInterp (AddInclude _)         = return ()
+    dryInterp (AddDefinition _)      = return ()
+    dryInterp (AddExternFun _ _ _)   = return ()
+    dryInterp (AddExternProc _ _)    = return ()
+    dryInterp (CallFun _ _)          = liftM ValComp $ freshStr "v"
+    dryInterp (CallProc _ _ _)       = return ()
+    dryInterp (InModule _ _)         = return ()
 
 
 
@@ -372,34 +612,93 @@
 -- * Running commands
 --------------------------------------------------------------------------------
 
-runRefCMD :: forall exp prog a . EvalExp exp => RefCMD exp prog a -> IO a
-runRefCMD (InitRef a)                       = fmap RefEval $ newIORef $ evalExp a
-runRefCMD NewRef                            = fmap RefEval $ newIORef $ error "reading uninitialized reference"
-runRefCMD (SetRef (RefEval r) a)            = writeIORef r $ evalExp a
-runRefCMD (GetRef (RefEval (r :: IORef b))) = fmap litExp $ readIORef r
+runRefCMD :: RefCMD (Param3 IO IO pred) a -> IO a
+runRefCMD (NewRef _)              = fmap RefEval $ newIORef $ error "reading uninitialized reference"
+runRefCMD (InitRef _ a)           = fmap RefEval . newIORef =<< a
+runRefCMD (SetRef (RefEval r) a)  = writeIORef r =<< a
+runRefCMD (GetRef (RefEval r))    = ValEval <$> readIORef r
+runRefCMD cmd@(UnsafeFreezeRef r) = runRefCMD (GetRef r `asTypeOf` cmd)
 
-runArrCMD :: EvalExp exp => ArrCMD exp prog a -> IO a
-runArrCMD (NewArr n) = fmap ArrEval $ newArray_ (0, fromIntegral (evalExp n)-1)
-runArrCMD (NewArr_) = error "NewArr_ not allowed in interpreted mode"
-runArrCMD (SetArr i a (ArrEval arr)) =
-    writeArray arr (fromIntegral (evalExp i)) (evalExp a)
-runArrCMD (GetArr i (ArrEval arr)) =
-    fmap litExp $ readArray arr (fromIntegral (evalExp i))
+runArrCMD :: ArrCMD (Param3 IO IO pred) a -> IO a
+runArrCMD (NewArr _ n) = do
+    n'  <- n
+    arr <- newArray_ (0, fromIntegral n'-1)
+    ArrEval <$> newIORef arr
+runArrCMD (InitArr _ as) = fmap ArrEval . newIORef =<< newListArray (0, genericLength as - 1) as
+runArrCMD (GetArr i (ArrEval arr)) = do
+    arr'  <- readIORef arr
+    i'    <- i
+    (l,h) <- getBounds arr'
+    if i'<l || i'>h
+      then error $ "getArr: index "
+                ++ show (toInteger i')
+                ++ " out of bounds "
+                ++ show (toInteger l, toInteger h)
+      else ValEval <$> readArray arr' i'
+runArrCMD (SetArr i a (ArrEval arr)) = do
+    arr'  <- readIORef arr
+    i'    <- i
+    a'    <- a
+    (l,h) <- getBounds arr'
+    if i'<l || i'>h
+      then error $ "setArr: index "
+                ++ show (toInteger i')
+                ++ " out of bounds "
+                ++ show (toInteger l, toInteger h)
+      else writeArray arr' (fromIntegral i') a'
+runArrCMD (CopyArr (ArrEval arr1) (ArrEval arr2) l) = do
+    arr1'  <- readIORef arr1
+    arr2'  <- readIORef arr2
+    l'     <- l
+    (0,h1) <- getBounds arr1'
+    (0,h2) <- getBounds arr2'
+    if l'>h2+1
+    then error $ "copyArr: cannot copy "
+              ++ show (toInteger l')
+              ++ " elements from array with "
+              ++ show (toInteger (h2+1))
+              ++ " allocated elements"
+    else if l'>h1+1
+    then error $ "copyArr: cannot copy "
+              ++ show (toInteger l')
+              ++ " elements to array with "
+              ++ show (toInteger (h1+1))
+              ++ " allocated elements"
+    else sequence_
+      [ readArray arr2' i >>= writeArray arr1' i | i <- genericTake l' [0..] ]
+runArrCMD (UnsafeFreezeArr (ArrEval arr)) =
+    fmap IArrEval . freeze =<< readIORef arr
+runArrCMD (UnsafeThawArr (IArrEval arr)) =
+    fmap ArrEval . newIORef =<< thaw arr
 
-runControlCMD :: EvalExp exp => ControlCMD exp IO a -> IO a
-runControlCMD (If c t f)        = if evalExp c then t else f
+runControlCMD :: ControlCMD (Param3 IO IO pred) a -> IO a
+runControlCMD (If c t f)        = c >>= \c' -> if c' then t else f
 runControlCMD (While cont body) = loop
   where loop = do
-          c <- cont
-          when (evalExp c) $ body >> loop
-runControlCMD (For lo hi body) = loop (evalExp lo)
+          c <- join cont
+          when c (body >> loop)
+runControlCMD (For (lo,step,hi) body) = do
+    lo' <- lo
+    hi' <- borderVal hi
+    loop lo' hi'
   where
-    hi' = evalExp hi
-    loop i
-      | i <= hi'  = body (litExp i) >> loop (i+1)
+    incl = borderIncl hi
+    cont i h
+      | incl && (step>=0) = i <= h
+      | incl && (step<0)  = i >= h
+      | step >= 0         = i <  h
+      | step < 0          = i >  h
+    loop i h
+      | cont i h  = body (ValEval i) >> loop (i + fromIntegral step) h
       | otherwise = return ()
 runControlCMD Break = error "cannot run programs involving break"
+runControlCMD (Assert cond msg) = do
+    cond' <- cond
+    unless cond' $ error $ "Assertion failed: " ++ msg
 
+runPtrCMD :: PtrCMD (Param3 IO IO pred) a -> IO a
+runPtrCMD (SwapPtr a b) = runSwapPtr a b
+
 evalHandle :: Handle -> IO.Handle
 evalHandle (HandleEval h)        = h
 evalHandle (HandleComp "stdin")  = IO.stdin
@@ -418,40 +717,39 @@
         cs <- readWord h
         return (c:cs)
 
-evalFPrintf :: EvalExp exp =>
-    [PrintfArg exp] -> (forall r . Printf.HPrintfType r => r) -> IO ()
-evalFPrintf []            pf = pf
-evalFPrintf (PrintfArg a:as) pf = evalFPrintf as (pf $ evalExp a)
+runFPrintf :: [PrintfArg IO] -> (forall r . Printf.HPrintfType r => r) -> IO ()
+runFPrintf []               pf = pf
+runFPrintf (PrintfArg a:as) pf = a >>= \a' -> runFPrintf as (pf a')
 
-runFileCMD :: EvalExp exp => FileCMD exp IO a -> IO a
-runFileCMD (FOpen file mode)              = fmap HandleEval $ IO.openFile file mode
+runFileCMD :: FileCMD (Param3 IO IO pred) a -> IO a
+runFileCMD (FOpen file mode)              = HandleEval <$> IO.openFile file mode
 runFileCMD (FClose (HandleEval h))        = IO.hClose h
 runFileCMD (FClose (HandleComp "stdin"))  = return ()
 runFileCMD (FClose (HandleComp "stdout")) = return ()
-runFileCMD (FPrintf h format as)          = evalFPrintf as (Printf.hPrintf (evalHandle h) format)
+runFileCMD (FPrintf h format as)          = runFPrintf as (Printf.hPrintf (evalHandle h) format)
 runFileCMD (FGet h)   = do
     w <- readWord $ evalHandle h
     case reads w of
-        [(f,"")] -> return $ litExp f
+        [(f,"")] -> return $ ValEval f
         _        -> error $ "fget: no parse (input " ++ show w ++ ")"
-runFileCMD (FEof h) = fmap litExp $ IO.hIsEOF $ evalHandle h
-
-runObjectCMD :: ObjectCMD exp IO a -> IO a
-runObjectCMD (NewObject _) = error "cannot run programs involving newObject"
-runObjectCMD (InitObject _ _ _ _) = error "cannot run programs involving initObject"
+runFileCMD (FEof h) = fmap ValEval $ IO.hIsEOF $ evalHandle h
 
-runCallCMD :: EvalExp exp => CallCMD exp IO a -> IO a
-runCallCMD (AddInclude _)       = return ()
-runCallCMD (AddDefinition _)    = return ()
-runCallCMD (AddExternFun _ _ _) = return ()
-runCallCMD (AddExternProc _ _)  = return ()
-runCallCMD (CallFun _ _)        = error "cannot run programs involving callFun"
-runCallCMD (CallProc _ _)       = error "cannot run programs involving callProc"
+runC_CMD :: C_CMD (Param3 IO IO pred) a -> IO a
+runC_CMD (NewPtr base)        = error $ "cannot run programs involving newPtr (base name " ++ base ++ ")"
+runC_CMD (PtrToArr p)         = error "cannot run programs involving ptrToArr"
+runC_CMD (NewObject base _ _) = error $ "cannot run programs involving newObject (base name " ++ base ++ ")"
+runC_CMD (AddInclude _)       = return ()
+runC_CMD (AddDefinition _)    = return ()
+runC_CMD (AddExternFun _ _ _) = return ()
+runC_CMD (AddExternProc _ _)  = return ()
+runC_CMD (CallFun _ _)        = error "cannot run programs involving callFun"
+runC_CMD (CallProc _ _ _)     = error "cannot run programs involving callProc"
+runC_CMD (InModule _ prog)    = prog
 
-instance EvalExp exp => Interp (RefCMD exp)     IO where interp = runRefCMD
-instance EvalExp exp => Interp (ArrCMD exp)     IO where interp = runArrCMD
-instance EvalExp exp => Interp (ControlCMD exp) IO where interp = runControlCMD
-instance EvalExp exp => Interp (FileCMD exp)    IO where interp = runFileCMD
-instance                Interp (ObjectCMD exp)  IO where interp = runObjectCMD
-instance EvalExp exp => Interp (CallCMD exp)    IO where interp = runCallCMD
+instance InterpBi RefCMD     IO (Param1 pred) where interpBi = runRefCMD
+instance InterpBi ArrCMD     IO (Param1 pred) where interpBi = runArrCMD
+instance InterpBi ControlCMD IO (Param1 pred) where interpBi = runControlCMD
+instance InterpBi PtrCMD     IO (Param1 pred) where interpBi = runPtrCMD
+instance InterpBi FileCMD    IO (Param1 pred) where interpBi = runFileCMD
+instance InterpBi C_CMD      IO (Param1 pred) where interpBi = runC_CMD
 
diff --git a/src/Language/Embedded/Imperative/Frontend.hs b/src/Language/Embedded/Imperative/Frontend.hs
--- a/src/Language/Embedded/Imperative/Frontend.hs
+++ b/src/Language/Embedded/Imperative/Frontend.hs
@@ -2,11 +2,7 @@
 {-# LANGUAGE QuasiQuotes #-}
 {-# LANGUAGE UndecidableInstances #-}
 
--- Front end for imperative instructions
---
--- These instructions are general imperative constructs independent of the back
--- end, except for the stuff under \"External function calls\" which is
--- C-specific.
+-- Front end for imperative programs
 
 module Language.Embedded.Imperative.Frontend where
 
@@ -19,16 +15,12 @@
 import Data.Typeable
 import System.IO.Unsafe
 
-#if __GLASGOW_HASKELL__ < 708
-import Data.Proxy
-#endif
-import Language.C.Quote.C
-
 import Control.Monad.Operational.Higher
+import System.IO.Fake
 import Language.Embedded.Expression
 import Language.Embedded.Imperative.CMD
-import Language.Embedded.Imperative.Frontend.General
 import Language.Embedded.Imperative.Args
+import Language.Embedded.Imperative.Frontend.General
 
 
 
@@ -37,35 +29,57 @@
 --------------------------------------------------------------------------------
 
 -- | Create an uninitialized reference
-newRef :: (VarPred (IExp instr) a, RefCMD (IExp instr) :<: instr) => ProgramT instr m (Ref a)
-newRef = singleE NewRef
+newRef :: (pred a, RefCMD :<: instr) =>
+    ProgramT instr (Param2 exp pred) m (Ref a)
+newRef = newNamedRef "r"
 
+-- | Create an uninitialized named reference
+--
+-- The provided base name may be appended with a unique identifier to avoid name
+-- collisions.
+newNamedRef :: (pred a, RefCMD :<: instr)
+    => String  -- ^ Base name
+    -> ProgramT instr (Param2 exp pred) m (Ref a)
+newNamedRef = singleInj . NewRef
+
 -- | Create an initialized reference
-initRef :: (VarPred (IExp instr) a, RefCMD (IExp instr) :<: instr) =>
-    IExp instr a -> ProgramT instr m (Ref a)
-initRef = singleE . InitRef
+initRef :: (pred a, RefCMD :<: instr)
+    => exp a  -- ^ Initial value
+    -> ProgramT instr (Param2 exp pred) m (Ref a)
+initRef = initNamedRef "r"
 
+-- | Create an initialized named reference
+--
+-- The provided base name may be appended with a unique identifier to avoid name
+-- collisions.
+initNamedRef :: (pred a, RefCMD :<: instr)
+    => String  -- ^ Base name
+    -> exp a   -- ^ Initial value
+    -> ProgramT instr (Param2 exp pred) m (Ref a)
+initNamedRef base a = singleInj (InitRef base a)
+
 -- | Get the contents of a reference
-getRef :: (VarPred (IExp instr) a, RefCMD (IExp instr) :<: instr) =>
-    Ref a -> ProgramT instr m (IExp instr a)
-getRef = singleE . GetRef
+getRef :: (pred a, FreeExp exp, VarPred exp a, RefCMD :<: instr, Monad m) =>
+    Ref a -> ProgramT instr (Param2 exp pred) m (exp a)
+getRef = fmap valToExp . singleInj . GetRef
 
 -- | Set the contents of a reference
-setRef :: (VarPred (IExp instr) a, RefCMD (IExp instr) :<: instr) =>
-    Ref a -> IExp instr a -> ProgramT instr m ()
-setRef r = singleE . SetRef r
+setRef :: (pred a, RefCMD :<: instr) =>
+    Ref a -> exp a -> ProgramT instr (Param2 exp pred) m ()
+setRef r = singleInj . SetRef r
 
 -- | Modify the contents of reference
-modifyRef
-    :: ( VarPred (IExp instr) a
-       , EvalExp (IExp instr)
-       , CompExp (IExp instr)
-       , RefCMD (IExp instr) :<: instr
-       , Monad m
-       )
-    => Ref a -> (IExp instr a -> IExp instr a) -> ProgramT instr m ()
+modifyRef :: (pred a, FreeExp exp, VarPred exp a, RefCMD :<: instr, Monad m) =>
+    Ref a -> (exp a -> exp a) -> ProgramT instr (Param2 exp pred) m ()
 modifyRef r f = setRef r . f =<< unsafeFreezeRef r
 
+-- | Freeze the contents of reference (only safe if the reference is not updated
+-- as long as the resulting value is alive)
+unsafeFreezeRef
+    :: (pred a, FreeExp exp, VarPred exp a, RefCMD :<: instr, Monad m)
+    => Ref a -> ProgramT instr (Param2 exp pred) m (exp a)
+unsafeFreezeRef = fmap valToExp . singleInj . UnsafeFreezeRef
+
 -- | Read the value of a reference without returning in the monad
 --
 -- WARNING: Don't use this function unless you really know what you are doing.
@@ -75,189 +89,233 @@
 -- can give strange results when evaluating in 'IO', as explained here:
 --
 -- <http://fun-discoveries.blogspot.se/2015/09/strictness-can-fix-non-termination.html>
-veryUnsafeFreezeRef :: (VarPred exp a, EvalExp exp, CompExp exp) =>
-    Ref a -> exp a
-veryUnsafeFreezeRef (RefEval r) = litExp $! unsafePerformIO $! readIORef r
+veryUnsafeFreezeRef :: (FreeExp exp, VarPred exp a) => Ref a -> exp a
+veryUnsafeFreezeRef (RefEval r) = valExp $! unsafePerformIO $! readIORef r
 veryUnsafeFreezeRef (RefComp v) = varExp v
 
--- | Freeze the contents of reference (only safe if the reference is never
--- written to after the freezing)
-unsafeFreezeRef :: (VarPred exp a, EvalExp exp, CompExp exp, Monad m) =>
-    Ref a -> ProgramT instr m (exp a)
-unsafeFreezeRef r = return $! veryUnsafeFreezeRef r
-  -- Strict applications (here and in `veryUnsafeFreezeRef`) are needed when
-  -- evaluating in `IO` to force `readIORef` to be performed before the next
-  -- action.
-  --
-  -- The `modifyRef` test case fails if the strict applications are removed, so
-  -- this seems to work. If there's a problem, another possibility would be to
-  -- make `unsafeFreezeRef` an instruction in `RefCMD`. This would avoid the
-  -- need for `unsafePerformIO`.
 
 
-
 --------------------------------------------------------------------------------
 -- * Arrays
 --------------------------------------------------------------------------------
 
--- | Create an uninitialized an array
-newArr
-    :: ( pred a
-       , pred i
-       , Integral i
-       , Ix i
-       , ArrCMD (IExp instr) :<: instr
-       , pred ~ VarPred (IExp instr)
-       )
-    => IExp instr i -> ProgramT instr m (Arr i a)
-newArr n = singleE $ NewArr n
+-- | Create an uninitialized array
+newArr :: (pred a, Integral i, Ix i, ArrCMD :<: instr)
+    => exp i  -- ^ Length
+    -> ProgramT instr (Param2 exp pred) m (Arr i a)
+newArr = newNamedArr "a"
 
-newArr_
-    :: ( pred a
-       , pred i
-       , Integral i
-       , Ix i
-       , ArrCMD (IExp instr) :<: instr
-       , pred ~ VarPred (IExp instr)
-       )
-    => ProgramT instr m (Arr i a)
-newArr_ = singleE $ NewArr_
+-- | Create an uninitialized named array
+--
+-- The provided base name may be appended with a unique identifier to avoid name
+-- collisions.
+newNamedArr :: (pred a, Integral i, Ix i, ArrCMD :<: instr)
+    => String -- ^ Base name
+    -> exp i  -- ^ Length
+    -> ProgramT instr (Param2 exp pred) m (Arr i a)
+newNamedArr base len = singleInj (NewArr base len)
 
--- | Set the contents of an array
+-- | Create and initialize an array
+initArr :: (pred a, Integral i, Ix i, ArrCMD :<: instr)
+    => [a]  -- ^ Initial contents
+    -> ProgramT instr (Param2 exp pred) m (Arr i a)
+initArr = initNamedArr "a"
+
+-- | Create and initialize a named array
+--
+-- The provided base name may be appended with a unique identifier to avoid name
+-- collisions.
+initNamedArr :: (pred a, Integral i, Ix i, ArrCMD :<: instr)
+    => String  -- ^ Base name
+    -> [a]     -- ^ Initial contents
+    -> ProgramT instr (Param2 exp pred) m (Arr i a)
+initNamedArr base init = singleInj (InitArr base init)
+
+-- | Get an element of an array
 getArr
-    :: ( VarPred (IExp instr) a
-       , ArrCMD (IExp instr) :<: instr
+    :: ( pred a
+       , FreeExp exp
+       , VarPred exp a
        , Integral i
        , Ix i
+       , ArrCMD :<: instr
+       , Monad m
        )
-    => IExp instr i -> Arr i a -> ProgramT instr m (IExp instr a)
-getArr i arr = singleE $ GetArr i arr
+    => exp i -> Arr i a -> ProgramT instr (Param2 exp pred) m (exp a)
+getArr i arr = fmap valToExp $ singleInj $ GetArr i arr
 
--- | Set the contents of an array
-setArr
-    :: ( VarPred (IExp instr) a
-       , ArrCMD (IExp instr) :<: instr
-       , Integral i
-       , Ix i
-       )
-    => IExp instr i -> IExp instr a -> Arr i a -> ProgramT instr m ()
-setArr i a arr = singleE (SetArr i a arr)
+-- | Set an element of an array
+setArr :: (pred a, Integral i, Ix i, ArrCMD :<: instr) =>
+    exp i -> exp a -> Arr i a -> ProgramT instr (Param2 exp pred) m ()
+setArr i a arr = singleInj (SetArr i a arr)
 
+-- | Copy the contents of an array to another array. The number of elements to
+-- copy must not be greater than the number of allocated elements in either
+-- array.
+copyArr :: (pred a, Integral i, Ix i, ArrCMD :<: instr)
+    => Arr i a  -- ^ Destination
+    -> Arr i a  -- ^ Source
+    -> exp i    -- ^ Number of elements
+    -> ProgramT instr (Param2 exp pred) m ()
+copyArr arr1 arr2 len = singleInj $ CopyArr arr1 arr2 len
 
+-- | Freeze a mutable array to an immutable one. This involves copying the array
+-- to a newly allocated one.
+freezeArr :: (pred a, Integral i, Ix i, ArrCMD :<: instr, Monad m)
+    => Arr i a
+    -> exp i  -- ^ Length of new array
+    -> ProgramT instr (Param2 exp pred) m (IArr i a)
+freezeArr arr n = do
+    arr2 <- newArr n
+    copyArr arr2 arr n
+    unsafeFreezeArr arr2
 
+-- | Freeze a mutable array to an immutable one without making a copy. This is
+-- generally only safe if the the mutable array is not updated as long as the
+-- immutable array is alive.
+unsafeFreezeArr :: (pred a, Integral i, Ix i, ArrCMD :<: instr) =>
+    Arr i a -> ProgramT instr (Param2 exp pred) m (IArr i a)
+unsafeFreezeArr arr = singleInj $ UnsafeFreezeArr arr
+
+-- | Thaw an immutable array to a mutable one. This involves copying the array
+-- to a newly allocated one.
+thawArr :: (pred a, Integral i, Ix i, ArrCMD :<: instr, Monad m)
+    => IArr i a
+    -> exp i  -- ^ Number of elements to copy
+    -> ProgramT instr (Param2 exp pred) m (Arr i a)
+thawArr arr n = do
+    arr2 <- unsafeThawArr arr
+    arr3 <- newArr n
+    copyArr arr3 arr2 n
+    return arr3
+
+-- | Thaw an immutable array to a mutable one without making a copy. This is
+-- generally only safe if the the mutable array is not updated as long as the
+-- immutable array is alive.
+unsafeThawArr :: (pred a, Integral i, Ix i, ArrCMD :<: instr) =>
+    IArr i a -> ProgramT instr (Param2 exp pred) m (Arr i a)
+unsafeThawArr arr = singleInj $ UnsafeThawArr arr
+
+-- | Create and initialize an immutable array
+initIArr :: (pred a, Integral i, Ix i, ArrCMD :<: instr, Monad m) =>
+    [a] -> ProgramT instr (Param2 exp pred) m (IArr i a)
+initIArr = unsafeFreezeArr <=< initArr
+
+
+
 --------------------------------------------------------------------------------
 -- * Control flow
 --------------------------------------------------------------------------------
 
 -- | Conditional statement
-iff :: (ControlCMD (IExp instr) :<: instr)
-    => IExp instr Bool      -- ^ Condition
-    -> ProgramT instr m ()  -- ^ True branch
-    -> ProgramT instr m ()  -- ^ False branch
-    -> ProgramT instr m ()
-iff b t f = singleE $ If b t f
+iff :: (ControlCMD :<: instr)
+    => exp Bool      -- ^ Condition
+    -> ProgramT instr (Param2 exp pred) m ()  -- ^ True branch
+    -> ProgramT instr (Param2 exp pred) m ()  -- ^ False branch
+    -> ProgramT instr (Param2 exp pred) m ()
+iff b t f = singleInj $ If b t f
 
 -- | Conditional statement that returns an expression
 ifE
-    :: ( VarPred (IExp instr) a
-       , ControlCMD (IExp instr) :<: instr
-       , RefCMD (IExp instr)     :<: instr
+    :: ( pred a
+       , FreeExp exp
+       , VarPred exp a
+       , ControlCMD :<: instr
+       , RefCMD     :<: instr
        , Monad m
        )
-    => IExp instr Bool                  -- ^ Condition
-    -> ProgramT instr m (IExp instr a)  -- ^ True branch
-    -> ProgramT instr m (IExp instr a)  -- ^ False branch
-    -> ProgramT instr m (IExp instr a)
+    => exp Bool                                    -- ^ Condition
+    -> ProgramT instr (Param2 exp pred) m (exp a)  -- ^ True branch
+    -> ProgramT instr (Param2 exp pred) m (exp a)  -- ^ False branch
+    -> ProgramT instr (Param2 exp pred) m (exp a)
 ifE b t f = do
     r <- newRef
     iff b (t >>= setRef r) (f >>= setRef r)
     getRef r
 
 -- | While loop
-while :: (ControlCMD (IExp instr) :<: instr)
-    => ProgramT instr m (IExp instr Bool)  -- ^ Continue condition
-    -> ProgramT instr m ()                 -- ^ Loop body
-    -> ProgramT instr m ()
-while b t = singleE $ While b t
-
--- | While loop that returns an expression
-whileE
-    :: ( VarPred (IExp instr) a
-       , ControlCMD (IExp instr) :<: instr
-       , RefCMD (IExp instr)     :<: instr
-       , Monad m
-       )
-    => ProgramT instr m (IExp instr Bool)  -- ^ Continue condition
-    -> ProgramT instr m (IExp instr a)     -- ^ Loop body
-    -> ProgramT instr m (IExp instr a)
-whileE b t = do
-    r <- newRef
-    while b (t >>= setRef r)
-    getRef r
-
--- | For loop
-for :: (ControlCMD (IExp instr) :<: instr, Integral n, VarPred (IExp instr) n)
-    => IExp instr n                           -- ^ Start index
-    -> IExp instr n                           -- ^ Stop index
-    -> (IExp instr n -> ProgramT instr m ())  -- ^ Loop body
-    -> ProgramT instr m ()
-for lo hi body = singleE $ For lo hi body
+while :: (ControlCMD :<: instr)
+    => ProgramT instr (Param2 exp pred) m (exp Bool)  -- ^ Continue condition
+    -> ProgramT instr (Param2 exp pred) m ()          -- ^ Loop body
+    -> ProgramT instr (Param2 exp pred) m ()
+while b t = singleInj $ While b t
 
 -- | For loop
-forE
-    :: ( Integral n
-       , VarPred (IExp instr) n
-       , VarPred (IExp instr) a
-       , ControlCMD (IExp instr) :<: instr
-       , RefCMD (IExp instr)     :<: instr
-       , Monad m
+for
+    :: ( FreeExp exp
+       , ControlCMD :<: instr
+       , Integral n
+       , pred n
+       , VarPred exp n
        )
-    => IExp instr n                                       -- ^ Start index
-    -> IExp instr n                                       -- ^ Stop index
-    -> (IExp instr n -> ProgramT instr m (IExp instr a))  -- ^ Loop body
-    -> ProgramT instr m (IExp instr a)
-forE lo hi body = do
-    r <- newRef
-    for lo hi (body >=> setRef r)
-    getRef r
+    => IxRange (exp n)                                   -- ^ Index range
+    -> (exp n -> ProgramT instr (Param2 exp pred) m ())  -- ^ Loop body
+    -> ProgramT instr (Param2 exp pred) m ()
+for range body = singleInj $ For range (body . valToExp)
 
 -- | Break out from a loop
-break :: (ControlCMD (IExp instr) :<: instr) => ProgramT instr m ()
-break = singleE Break
+break :: (ControlCMD :<: instr) => ProgramT instr (Param2 exp pred) m ()
+break = singleInj Break
 
+-- | Assertion
+assert :: (ControlCMD :<: instr)
+    => exp Bool  -- ^ Expression that should be true
+    -> String    -- ^ Message in case of failure
+    -> ProgramT instr (Param2 exp pred) m ()
+assert cond msg = singleInj $ Assert cond msg
 
 
+
 --------------------------------------------------------------------------------
+-- * Pointer operations
+--------------------------------------------------------------------------------
+
+-- | Swap two pointers
+--
+-- This is generally an unsafe operation. E.g. it can be used to make a
+-- reference to a data structure escape the scope of the data.
+--
+-- The 'IsPointer' class ensures that the operation is only possible for types
+-- that are represented as pointers in C.
+unsafeSwap :: (IsPointer a, PtrCMD :<: instr) =>
+    a -> a -> ProgramT instr (Param2 exp pred) m ()
+unsafeSwap a b = singleInj $ SwapPtr a b
+
+
+
+--------------------------------------------------------------------------------
 -- * File handling
 --------------------------------------------------------------------------------
 
 -- | Open a file
-fopen :: (FileCMD (IExp instr) :<: instr) => FilePath -> IOMode -> ProgramT instr m Handle
-fopen file = singleE . FOpen file
+fopen :: (FileCMD :<: instr) =>
+    FilePath -> IOMode -> ProgramT instr (Param2 exp pred) m Handle
+fopen file = singleInj . FOpen file
 
 -- | Close a file
-fclose :: (FileCMD (IExp instr) :<: instr) => Handle -> ProgramT instr m ()
-fclose = singleE . FClose
+fclose :: (FileCMD :<: instr) => Handle -> ProgramT instr (Param2 exp pred) m ()
+fclose = singleInj . FClose
 
 -- | Check for end of file
-feof :: (VarPred (IExp instr) Bool, FileCMD (IExp instr) :<: instr) =>
-    Handle -> ProgramT instr m (IExp instr Bool)
-feof = singleE . FEof
+feof :: (FreeExp exp, VarPred exp Bool, FileCMD :<: instr, Monad m) =>
+    Handle -> ProgramT instr (Param2 exp pred) m (exp Bool)
+feof = fmap valToExp . singleInj . FEof
 
 class PrintfType r
   where
     type PrintfExp r :: * -> *
     fprf :: Handle -> String -> [PrintfArg (PrintfExp r)] -> r
 
-instance (FileCMD (IExp instr) :<: instr, a ~ ()) => PrintfType (ProgramT instr m a)
+instance (FileCMD :<: instr, a ~ ()) =>
+    PrintfType (ProgramT instr (Param2 exp pred) m a)
   where
-    type PrintfExp (ProgramT instr m a) = IExp instr
-    fprf h form as = singleE $ FPrintf h form (reverse as)
+    type PrintfExp (ProgramT instr (Param2 exp pred) m a) = exp
+    fprf h form as = singleInj $ FPrintf h form (reverse as)
 
-instance (Formattable a, VarPred exp a, PrintfType r, exp ~ PrintfExp r) =>
+instance (Formattable a, PrintfType r, exp ~ PrintfExp r) =>
     PrintfType (exp a -> r)
   where
-    type PrintfExp (exp a -> r) = exp
+    type PrintfExp  (exp a -> r) = exp
     fprf h form as = \a -> fprf h form (PrintfArg a : as)
 
 -- | Print to a handle. Accepts a variable number of arguments.
@@ -265,24 +323,27 @@
 fprintf h format = fprf h format []
 
 -- | Put a single value to a handle
-fput :: forall instr a m
-    .  (Formattable a, VarPred (IExp instr) a, FileCMD (IExp instr) :<: instr)
+fput :: forall instr exp pred a m
+    .  (Formattable a, VarPred exp a, FileCMD :<: instr)
     => Handle
-    -> String        -- ^ Prefix
-    -> IExp instr a  -- ^ Expression to print
-    -> String        -- ^ Suffix
-    -> ProgramT instr m ()
+    -> String  -- ^ Prefix
+    -> exp a   -- ^ Expression to print
+    -> String  -- ^ Suffix
+    -> ProgramT instr (Param2 exp pred) m ()
 fput hdl prefix a suffix =
     fprintf hdl (prefix ++ formatSpecifier (Proxy :: Proxy a) ++ suffix) a
 
 -- | Get a single value from a handle
 fget
     :: ( Formattable a
-       , VarPred (IExp instr) a
-       , FileCMD (IExp instr) :<: instr
+       , pred a
+       , FreeExp exp
+       , VarPred exp a
+       , FileCMD :<: instr
+       , Monad m
        )
-    => Handle -> ProgramT instr m (IExp instr a)
-fget = singleE . FGet
+    => Handle -> ProgramT instr (Param2 exp pred) m (exp a)
+fget = fmap valToExp . singleInj . FGet
 
 -- | Print to @stdout@. Accepts a variable number of arguments.
 printf :: PrintfType r => String -> r
@@ -291,41 +352,56 @@
 
 
 --------------------------------------------------------------------------------
--- * Abstract objects
+-- * C-specific commands
 --------------------------------------------------------------------------------
 
--- | Create a pointer to an abstract object. The only thing one can do with such
--- objects is to pass them to 'callFun' or 'callProc'.
-newObject :: (ObjectCMD (IExp instr) :<: instr)
-    => String  -- ^ Object type
-    -> ProgramT instr m Object
-newObject = singleE . NewObject
+-- | Create a null pointer
+newPtr :: (pred a, C_CMD :<: instr) => ProgramT instr (Param2 exp pred) m (Ptr a)
+newPtr = newNamedPtr "p"
 
--- | Call a function to create a pointed object
-initObject :: (ObjectCMD (IExp instr) :<: instr)
-    => String                 -- ^ Function name
-    -> String                 -- ^ Object type
-    -> [FunArg (IExp instr)]  -- ^ Arguments
-    -> ProgramT instr m Object
-initObject fun ty args = singleE $ InitObject fun True ty args
+-- | Create a named null pointer
+--
+-- The provided base name may be appended with a unique identifier to avoid name
+-- collisions.
+newNamedPtr :: (pred a, C_CMD :<: instr)
+    => String  -- ^ Base name
+    -> ProgramT instr (Param2 exp pred) m (Ptr a)
+newNamedPtr = singleInj . NewPtr
 
--- | Call a function to create an object
-initUObject :: (ObjectCMD (IExp instr) :<: instr)
-    => String                 -- ^ Function name
-    -> String                 -- ^ Object type
-    -> [FunArg (IExp instr)]  -- ^ Arguments
-    -> ProgramT instr m Object
-initUObject fun ty args = singleE $ InitObject fun False ty args
+-- | Cast a pointer to an array
+ptrToArr :: (C_CMD :<: instr) => Ptr a -> ProgramT instr (Param2 exp pred) m (Arr i a)
+ptrToArr = singleInj . PtrToArr
 
+-- | Create a pointer to an abstract object. The only thing one can do with such
+-- objects is to pass them to 'callFun' or 'callProc'.
+newObject :: (C_CMD :<: instr)
+    => String  -- ^ Object type
+    -> Bool    -- ^ Pointed?
+    -> ProgramT instr (Param2 exp pred) m Object
+newObject t p = newNamedObject "obj" t p
 
+-- | Create a pointer to a named abstract object. The only thing one can do with
+-- such objects is to pass them to 'callFun' or 'callProc'.
+--
+-- The provided base name may be appended with a unique identifier to avoid name
+-- collisions.
+newNamedObject :: (C_CMD :<: instr)
+    => String  -- ^ Base name
+    -> String  -- ^ Object type
+    -> Bool    -- ^ Pointed?
+    -> ProgramT instr (Param2 exp pred) m Object
+newNamedObject base t p = singleInj $ NewObject base t p
 
---------------------------------------------------------------------------------
--- * External function calls (C-specific)
---------------------------------------------------------------------------------
+-- | Generate code into another translation unit
+inModule :: (C_CMD :<: instr)
+    => String
+    -> ProgramT instr (Param2 exp pred) m ()
+    -> ProgramT instr (Param2 exp pred) m ()
+inModule mod prog = singleInj $ InModule mod prog
 
 -- | Add an @#include@ statement to the generated code
-addInclude :: (CallCMD (IExp instr) :<: instr) => String -> ProgramT instr m ()
-addInclude = singleE . AddInclude
+addInclude :: (C_CMD :<: instr) => String -> ProgramT instr (Param2 exp pred) m ()
+addInclude = singleInj . AddInclude
 
 -- | Add a global definition to the generated code
 --
@@ -348,60 +424,72 @@
 -- >           // goes here
 -- >       }
 -- >       |]
-addDefinition :: (CallCMD (IExp instr) :<: instr) => Definition -> ProgramT instr m ()
-addDefinition = singleE . AddDefinition
+addDefinition :: (C_CMD :<: instr) => Definition -> ProgramT instr (Param2 exp pred) m ()
+addDefinition = singleInj . AddDefinition
 
 -- | Declare an external function
-addExternFun :: (VarPred exp res, CallCMD exp :<: instr, exp ~ IExp instr)
-    => String           -- ^ Function name
-    -> proxy (exp res)  -- ^ Proxy for expression and result type
-    -> [FunArg exp]     -- ^ Arguments (only used to determine types)
-    -> ProgramT instr m ()
-addExternFun fun res args = singleE $ AddExternFun fun res args
+addExternFun :: (pred res, C_CMD :<: instr)
+    => String             -- ^ Function name
+    -> proxy res          -- ^ Proxy for result type
+    -> [FunArg exp pred]  -- ^ Arguments (only used to determine types)
+    -> ProgramT instr (Param2 exp pred) m ()
+addExternFun fun res args = singleInj $ AddExternFun fun res args
 
 -- | Declare an external procedure
-addExternProc :: (CallCMD exp :<: instr, exp ~ IExp instr)
-    => String        -- ^ Procedure name
-    -> [FunArg exp]  -- ^ Arguments (only used to determine types)
-    -> ProgramT instr m ()
-addExternProc proc args = singleE $ AddExternProc proc args
+addExternProc :: (C_CMD :<: instr)
+    => String             -- ^ Procedure name
+    -> [FunArg exp pred]  -- ^ Arguments (only used to determine types)
+    -> ProgramT instr (Param2 exp pred) m ()
+addExternProc proc args = singleInj $ AddExternProc proc args
 
 -- | Call a function
-callFun :: (VarPred (IExp instr) a, CallCMD (IExp instr) :<: instr)
-    => String                 -- ^ Function name
-    -> [FunArg (IExp instr)]  -- ^ Arguments
-    -> ProgramT instr m (IExp instr a)
-callFun fun as = singleE $ CallFun fun as
+callFun :: (pred a, FreeExp exp, VarPred exp a, C_CMD :<: instr, Monad m)
+    => String             -- ^ Function name
+    -> [FunArg exp pred]  -- ^ Arguments
+    -> ProgramT instr (Param2 exp pred) m (exp a)
+callFun fun as = fmap valToExp $ singleInj $ CallFun fun as
 
 -- | Call a procedure
-callProc :: (CallCMD (IExp instr) :<: instr)
-    => String                 -- ^ Procedure name
-    -> [FunArg (IExp instr)]  -- ^ Arguments
-    -> ProgramT instr m ()
-callProc fun as = singleE $ CallProc fun as
+callProc :: (C_CMD :<: instr)
+    => String             -- ^ Procedure name
+    -> [FunArg exp pred]  -- ^ Arguments
+    -> ProgramT instr (Param2 exp pred) m ()
+callProc fun as = singleInj $ CallProc (Nothing :: Maybe Object) fun as
 
+-- | Call a procedure and assign its result
+callProcAssign :: (Assignable obj, C_CMD :<: instr)
+    => obj                -- ^ Object to which the result should be assigned
+    -> String             -- ^ Procedure name
+    -> [FunArg exp pred]  -- ^ Arguments
+    -> ProgramT instr (Param2 exp pred) m ()
+callProcAssign obj fun as = singleInj $ CallProc (Just obj) fun as
+  -- The reason for having both `callProc` and `callProcAssign` instead of a
+  -- single one with a `Maybe obj` is that the caller would have to resolve the
+  -- overloading when passing `Nothing` (as currently done in `callProc`).
+
 -- | Declare and call an external function
-externFun :: forall instr m exp res
-    .  (VarPred exp res, CallCMD exp :<: instr, exp ~ IExp instr, Monad m)
-    => String        -- ^ Function name
-    -> [FunArg exp]  -- ^ Arguments
-    -> ProgramT instr m (exp res)
+externFun :: forall instr m exp pred res
+    .  (pred res, FreeExp exp, VarPred exp res, C_CMD :<: instr, Monad m)
+    => String             -- ^ Function name
+    -> [FunArg exp pred]  -- ^ Arguments
+    -> ProgramT instr (Param2 exp pred) m (exp res)
 externFun fun args = do
-    addExternFun fun (Proxy :: Proxy (exp res)) args
+    addExternFun fun (Proxy :: Proxy res) args
     callFun fun args
 
 -- | Declare and call an external procedure
-externProc :: (CallCMD exp :<: instr, exp ~ IExp instr, Monad m)
+externProc :: (C_CMD :<: instr, Monad m)
     => String        -- ^ Procedure name
-    -> [FunArg exp]  -- ^ Arguments
-    -> ProgramT instr m ()
+    -> [FunArg exp pred]  -- ^ Arguments
+    -> ProgramT instr (Param2 exp pred) m ()
 externProc proc args = do
     addExternProc proc args
     callProc proc args
 
 -- | Get current time as number of seconds passed today
-getTime :: (VarPred (IExp instr) Double, CallCMD (IExp instr) :<: instr, Monad m) =>
-    ProgramT instr m (IExp instr Double)
+getTime
+    :: (pred Double, FreeExp exp, VarPred exp Double, C_CMD :<: instr, Monad m)
+    => ProgramT instr (Param2 exp pred) m (exp Double)
 getTime = do
     addInclude "<sys/time.h>"
     addInclude "<sys/resource.h>"
@@ -421,32 +509,44 @@
 
 -- Arguments
 
--- | Constant string argument
-strArg :: String -> FunArg exp
-strArg = FunArg . StrArg
-
 -- | Value argument
-valArg :: VarPred exp a => exp a -> FunArg exp
-valArg = FunArg . ValArg
+valArg :: pred a => exp a -> FunArg exp pred
+valArg = ValArg
 
 -- | Reference argument
-refArg :: VarPred exp a => Ref a -> FunArg exp
+refArg :: (pred a, Arg RefArg pred) => Ref a -> FunArg exp pred
 refArg = FunArg . RefArg
 
--- | Array argument
-arrArg :: VarPred exp a => Arr n a -> FunArg exp
+-- | Mutable array argument
+arrArg :: (pred a, Arg ArrArg pred) => Arr i a -> FunArg exp pred
 arrArg = FunArg . ArrArg
 
+-- | Immutable array argument
+iarrArg :: (pred a, Arg IArrArg pred) => IArr i a -> FunArg exp pred
+iarrArg = FunArg . IArrArg
+
+-- | Pointer argument
+ptrArg :: (pred a, Arg PtrArg pred) => Ptr a -> FunArg exp pred
+ptrArg = FunArg . PtrArg
+
 -- | Abstract object argument
-objArg :: Object -> FunArg exp
+objArg :: Object -> FunArg exp pred
 objArg = FunArg . ObjArg
 
+-- | Constant string argument
+strArg :: String -> FunArg exp pred
+strArg = FunArg . StrArg
+
 -- | Modifier that takes the address of another argument
-addr :: FunArg exp -> FunArg exp
-addr = FunArg . Addr
+addr :: FunArg exp pred -> FunArg exp pred
+addr = AddrArg
 
+-- | Modifier that dereferences another argument
+deref :: FunArg exp pred -> FunArg exp pred
+deref = DerefArg
 
 
+
 --------------------------------------------------------------------------------
 -- * Running programs
 --------------------------------------------------------------------------------
@@ -454,6 +554,14 @@
 -- | Run a program in 'IO'. Note that not all instructions are supported for
 -- running in 'IO'. For example, calls to external C functions are not
 -- supported.
-runIO :: (Interp instr IO, HFunctor instr) => Program instr a -> IO a
-runIO = interpret
+runIO :: (EvalExp exp, InterpBi instr IO (Param1 pred), HBifunctor instr) =>
+    Program instr (Param2 exp pred) a -> IO a
+runIO = interpretBi (return . evalExp)
+
+-- | Like 'runIO' but with explicit input/output connected to @stdin@/@stdout@
+captureIO :: (EvalExp exp, InterpBi instr IO (Param1 pred), HBifunctor instr)
+    => Program instr (Param2 exp pred) a  -- ^ Program to run
+    -> String                             -- ^ Input to send to @stdin@
+    -> IO String                          -- ^ Result from @stdout@
+captureIO = fakeIO . runIO
 
diff --git a/src/Language/Embedded/Imperative/Frontend/General.hs b/src/Language/Embedded/Imperative/Frontend/General.hs
--- a/src/Language/Embedded/Imperative/Frontend/General.hs
+++ b/src/Language/Embedded/Imperative/Frontend/General.hs
@@ -7,18 +7,25 @@
 module Language.Embedded.Imperative.Frontend.General
   ( Ref
   , Arr
+  , IArr
+  , Border (..)
+  , IxRange
+  , IsPointer
   , IO.IOMode (..)
   , Handle
   , stdin
   , stdout
+  , PrintfArg
   , Formattable
+  , Ptr
   , Object
   , FunArg (..)
+  , Assignable
   , Definition
   , cedecl
   ) where
-  -- Note: Important not to export the constructors of `Ref`, `Arr` or `Handle`,
-  -- since the user is not supposed to inspect such values.
+  -- Note: Important not to export the constructors of `Ref`, `Arr`, etc. since
+  -- the user is not supposed to inspect such values.
 
 import qualified System.IO as IO
 
diff --git a/src/Language/Embedded/Signature.hs b/src/Language/Embedded/Signature.hs
--- a/src/Language/Embedded/Signature.hs
+++ b/src/Language/Embedded/Signature.hs
@@ -9,9 +9,9 @@
 
 import Language.C.Monad
 import Language.Embedded.Expression
+import Language.Embedded.Backend.C.Expression
 
 import Language.C.Quote.C
-import Language.C.Syntax (Id(..),Exp(..),Type)
 
 
 -- * Language
@@ -23,31 +23,34 @@
   Named  :: String -> Ann exp a
 
 -- | Signatures
-data Signature exp a where
-  Ret    :: (VarPred exp a) => String -> exp a -> Signature exp a
-  Ptr    :: (VarPred exp a) => String -> exp a -> Signature exp a
-  Lam    :: (VarPred exp a) => Ann exp a -> (exp a -> Signature exp b)
-         -> Signature exp (a -> b)
+data Signature exp pred a where
+  Ret    :: pred a => String -> exp a -> Signature exp pred a
+  Ptr    :: pred a => String -> exp a -> Signature exp pred a
+  Lam    :: pred a => Ann exp a -> (Val a -> Signature exp pred b)
+         -> Signature exp pred (a -> b)
 
 
 -- * Combinators
 
-lam :: (VarPred exp a)
-    => (exp a -> Signature exp b) -> Signature exp (a -> b)
-lam f = Lam Empty $ \x -> f x
+lam :: (pred a, FreeExp exp, VarPred exp a)
+    => (exp a -> Signature exp pred b) -> Signature exp pred (a -> b)
+lam f = Lam Empty $ \x -> f (valToExp x)
 
-name :: (VarPred exp a)
-     => String -> (exp a -> Signature exp b) -> Signature exp (a -> b)
-name s f = Lam (Named s) $ \x -> f x
+name :: (pred a, FreeExp exp, VarPred exp a)
+     => String -> (exp a -> Signature exp pred b) -> Signature exp pred (a -> b)
+name s f = Lam (Named s) $ \x -> f (valToExp x)
 
-ret,ptr :: (VarPred exp a)
-        => String -> exp a -> Signature exp a
+ret,ptr :: (pred a)
+        => String -> exp a -> Signature exp pred a
 ret = Ret
 ptr = Ptr
 
-arg :: (VarPred exp a)
-    => Ann exp a -> (exp a -> exp b) -> (exp b -> Signature exp c) -> Signature exp (a -> c)
-arg s g f = Lam s $ \x -> f (g x)
+arg :: (pred a, FreeExp exp, VarPred exp a)
+    => Ann exp a
+    -> (exp a -> exp b)
+    -> (exp b -> Signature exp pred c)
+    -> Signature exp pred (a -> c)
+arg s g f = Lam s $ \x -> f $ g $ valToExp x
 
 
 
@@ -55,51 +58,48 @@
 
 -- | Compile a function @Signature@ to C code
 translateFunction :: forall m exp a. (MonadC m, CompExp exp)
-                  => Signature exp a -> m ()
+                  => Signature exp CType a -> m ()
 translateFunction sig = go sig (return ())
   where
-    go :: forall d. Signature exp d -> m () -> m ()
+    go :: Signature exp CType d -> m () -> m ()
     go (Ret n a) prelude = do
-      t <- compType a
+      t <- cType a
       inFunctionTy t n $ do
         prelude
         e <- compExp a
         addStm [cstm| return $e; |]
     go (Ptr n a) prelude = do
-      t <- compType a
+      t <- cType a
       inFunction n $ do
         prelude
         e <- compExp a
         addParam [cparam| $ty:t *out |]
         addStm [cstm| *out = $e; |]
     go fun@(Lam Empty f) prelude = do
-      t <- compTypePP (Proxy :: Proxy exp) (argProxy fun)
-      v <- fmap varExp freshId
-      Var n _ <- compExp v
-      go (f v) $ prelude >> addParam [cparam| $ty:t $id:n |]
+      t <- cType (argProxy fun)
+      v <- freshVar
+      go (f v) $ prelude >> addParam [cparam| $ty:t $id:v |]
     go fun@(Lam n@(Native l) f) prelude = do
-      t <- compTypePP (Proxy :: Proxy exp) (elemProxy n fun)
+      t <- cType n
       i <- freshId
-      let w = varExp i
-      Var (Id m _) _ <- compExp w
-      let n = m ++ "_buf"
-      withAlias i ('&':m) $ go (f w) $ do
+      let vi = 'v' : show i
+      let w = ValComp vi
+      let n = vi ++ "_buf"
+      withAlias i ('&':vi) $ go (f w) $ do
         prelude
         len <- compExp l
-        addLocal [cdecl| struct array $id:m = { .buffer = $id:n
-                                              , .length=$len
-                                              , .elemSize=sizeof($ty:t)
-                                              , .bytes=sizeof($ty:t)*$len
-                                              }; |]
+        addLocal [cdecl| struct array $id:vi = { .buffer = $id:n
+                                               , .length=$len
+                                               , .elemSize=sizeof($ty:t)
+                                               , .bytes=sizeof($ty:t)*$len
+                                               }; |]
         addParam [cparam| $ty:t * $id:n |]
     go fun@(Lam (Named s) f) prelude = do
-      t <- compTypePP (Proxy :: Proxy exp) (argProxy fun)
+      t <- cType (argProxy fun)
       i <- freshId
-      withAlias i s $ go (f $ varExp i) $ prelude >> addParam [cparam| $ty:t $id:s |]
-
-    argProxy :: Signature exp (b -> c) -> Proxy b
-    argProxy _ = Proxy
+      let w = ValComp ('v' : show i)
+      withAlias i s $ go (f w) $ prelude >> addParam [cparam| $ty:t $id:s |]
 
-    elemProxy :: Ann exp [b] -> Signature exp ([b] -> c) -> Proxy b
-    elemProxy _ _ = Proxy
+argProxy :: Signature exp pred (b -> c) -> Proxy b
+argProxy _ = Proxy
 
diff --git a/src/Language/Embedded/Traversal.hs b/src/Language/Embedded/Traversal.hs
--- a/src/Language/Embedded/Traversal.hs
+++ b/src/Language/Embedded/Traversal.hs
@@ -19,13 +19,13 @@
   where
     -- | Dry interpretation of an instruction. This function is like 'interp'
     -- except that it interprets in any monad that can supply fresh variables.
-    dryInterp :: MonadSupply m => instr m a -> m a
+    dryInterp :: MonadSupply m => instr '(m,fs) a -> m a
 
 -- | Interpretation of a program as a combination of dry interpretation and
 -- effectful observation
 observe_ :: (DryInterp instr, HFunctor instr, MonadSupply m)
-    => (forall a . instr m a -> a -> m ())  -- ^ Function for observing instructions
-    -> Program instr a
+    => (forall a . instr '(m,fs) a -> a -> m ())  -- ^ Function for observing instructions
+    -> Program instr fs a
     -> m a
 observe_ obs = interpretWithMonad $ \i -> do
     a <- dryInterp i
@@ -35,8 +35,8 @@
 -- | Interpretation of a program as a combination of dry interpretation and
 -- effectful observation
 observe :: (DryInterp instr, HFunctor instr, MonadSupply m)
-    => (forall a . instr m a -> a -> m a)  -- ^ Function for observing instructions
-    -> Program instr a
+    => (forall a . instr '(m,fs) a -> a -> m a)  -- ^ Function for observing instructions
+    -> Program instr fs a
     -> m a
 observe obs = interpretWithMonad $ \i -> do
     a <- dryInterp i
diff --git a/src/System/IO/Fake.hs b/src/System/IO/Fake.hs
new file mode 100644
--- /dev/null
+++ b/src/System/IO/Fake.hs
@@ -0,0 +1,68 @@
+-- | Running actions with explicit input\/output connected to
+-- @`stdin`@\/@`stdout`@.
+--
+-- This module is inspired by the package <http://hackage.haskell.org/package/silently>.
+
+module System.IO.Fake where
+
+
+
+import Control.DeepSeq
+import Control.Exception
+import GHC.IO.Handle
+import System.Directory
+import System.IO
+
+
+
+-- | Perform an action that with access to a temporary file. The file is removed
+-- after the action is completed.
+withTempFile
+    :: FilePath                     -- ^ Path to directory for temporary file
+    -> String                       -- ^ Base name for temporary file
+    -> ((FilePath,Handle) -> IO a)  -- ^ Action
+    -> IO a
+withTempFile tmpDir base k = bracket
+    (openTempFile tmpDir base)
+    (\(file,h) -> hClose h >> removeFile file)
+    k
+
+-- | Perform an action with a redirected handle
+withRedirect
+    :: Handle  -- ^ Shadowing handle
+    -> Handle  -- ^ Shadowed handle
+    -> IO a    -- ^ Action in which the redirect takes place
+    -> IO a
+withRedirect new old act = bracket
+    (do buffering <- hGetBuffering old
+        dupH      <- hDuplicate old
+        hDuplicateTo new old
+        return (dupH,buffering)
+    )
+    (\(dupH,buffering) -> do
+        hDuplicateTo dupH old
+        hSetBuffering old buffering
+        hClose dupH
+    )
+    (\_ -> act)
+
+-- | Perform an action with explicit input\/output connected to
+-- @`stdin`@\/@`stdout`@
+fakeIO
+    :: IO a       -- ^ Action
+    -> String     -- ^ Input to send to @stdin@
+    -> IO String  -- ^ Result from @stdout@
+fakeIO act inp = do
+    tmpDir <- getTemporaryDirectory
+    withTempFile tmpDir "fakeInput" $ \(inpFile,inpH) ->
+      withTempFile tmpDir "fakeOutput" $ \(outFile,outH) -> do
+        withRedirect outH stdout $
+          withRedirect inpH stdin $ do
+            hPutStr inpH inp
+            hSeek inpH AbsoluteSeek 0
+            act
+            hFlush stdout
+            hSeek outH AbsoluteSeek 0
+            str <- hGetContents outH
+            str `deepseq` return str
+
diff --git a/tests/CExp.hs b/tests/CExp.hs
new file mode 100644
--- /dev/null
+++ b/tests/CExp.hs
@@ -0,0 +1,111 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+module CExp where
+
+
+
+import Data.Int
+
+import Test.Tasty.QuickCheck
+import Test.Tasty.TH
+
+import Language.Syntactic (AST (..), DenResult)
+#if MIN_VERSION_syntactic(3,0,0)
+import Language.Syntactic.Functional (Denotation)
+#else
+import Language.Syntactic (Denotation)
+#endif
+
+import Language.Embedded.Imperative
+import Language.Embedded.Backend.C
+import Language.Embedded.CExp
+
+
+
+data NumExp
+    = VAR Int
+    | INT Int
+    | ADD NumExp NumExp
+    | SUB NumExp NumExp
+    | MUL NumExp NumExp
+    | NEG NumExp
+  deriving (Eq, Show)
+
+evalNumExp :: Num a => (Int -> a) -> NumExp -> a
+evalNumExp env (VAR v)   = env v
+evalNumExp env (INT i)   = fromIntegral i
+evalNumExp env (ADD a b) = evalNumExp env a + evalNumExp env b
+evalNumExp env (SUB a b) = evalNumExp env a - evalNumExp env b
+evalNumExp env (MUL a b) = evalNumExp env a * evalNumExp env b
+evalNumExp env (NEG a)   = negate (evalNumExp env a)
+
+num2CExp :: (Num a, Ord a, CType a) => NumExp -> CExp a
+num2CExp = evalNumExp (\v -> variable ('v' : show v))
+
+-- | Partial function for evaluating 'CExp' produced by 'num2CExp'
+evalNumCExp :: forall a
+    .  (String -> a)  -- ^ Mapping from variable names to values
+    -> CExp a
+    -> a
+evalNumCExp env = go . unCExp
+  where
+    go :: (a ~ DenResult sig) => AST T sig -> Denotation sig
+    go (Sym (T (Var v)))                = env v
+    go (Sym (T s))                      = evalSym s
+    go (Sym (T s@(UOp UnNeg)) :$ a)     = evalSym s $ go a
+    go (Sym (T s@(Op BiAdd)) :$ a :$ b) = evalSym s (go a) (go b)
+    go (Sym (T s@(Op BiSub)) :$ a :$ b) = evalSym s (go a) (go b)
+    go (Sym (T s@(Op BiMul)) :$ a :$ b) = evalSym s (go a) (go b)
+
+genNumExp :: Gen NumExp
+genNumExp = sized go
+  where
+    go s = frequency
+        [ -- Variable
+          (1, do v <- choose (0,4)
+                 return $ VAR v
+          )
+          -- Literal
+        , (1, fmap INT $ elements [-100 .. 100])
+        , (s, binOp ADD)
+        , (s, binOp SUB)
+        , (s, binOp MUL)
+        , (s, unOp NEG)
+        ]
+      where
+        binOp op = liftM2 op (go (s `div` 2)) (go (s `div` 2))
+        unOp op  = liftM op (go (s-1))
+
+instance Arbitrary NumExp
+  where
+    arbitrary = genNumExp
+
+    shrink (ADD a b) = a : b : [ADD a' b | a' <- shrink a] ++ [ADD a b' | b' <- shrink b]
+    shrink (SUB a b) = a : b : [SUB a' b | a' <- shrink a] ++ [SUB a b' | b' <- shrink b]
+    shrink (MUL a b) = a : b : [MUL a' b | a' <- shrink a] ++ [MUL a b' | b' <- shrink b]
+    shrink (NEG a)   = a : [NEG a' | a' <- shrink a]
+    shrink _         = []
+
+-- Test that numeric expressions are simplified correctly
+prop_numExp :: (a ~ Int32) => (a,a,a,a,a) -> NumExp -> Bool
+prop_numExp (a,b,c,d,e) numExp =
+    evalNumExp env1 numExp == evalNumCExp env2 (num2CExp numExp)
+  where
+    env1 v       = [a,b,c,d,e] !! v
+    env2 ('v':v) = [a,b,c,d,e] !! read v
+
+-- Test that inexact numeric expressions are handled correctly
+--
+-- This property fails if one changes `isExact` to `const True`
+prop_numExp_inexact :: (a ~ Float) => (a,a,a,a,a) -> NumExp -> Bool
+prop_numExp_inexact (a,b,c,d,e) numExp =
+    evalNumExp env1 numExp == evalNumCExp env2 (num2CExp numExp)
+  where
+    env1 v       = [a,b,c,d,e] !! v
+    env2 ('v':v) = [a,b,c,d,e] !! read v
+
+main = $defaultMainGenerator
+
diff --git a/tests/Examples.hs b/tests/Examples.hs
deleted file mode 100644
--- a/tests/Examples.hs
+++ /dev/null
@@ -1,22 +0,0 @@
-import Imperative ()
-import Concurrent ()
-import Language.Embedded.CExp
-import Language.Embedded.Imperative
-import Language.Embedded.Backend.C
-import System.IO
-import System.Process
-import System.Directory
-import System.Exit
-
-main = do let c = compile $
-                 do addInclude "<stdio.h>" :: Program (CallCMD CExp) ()
-                    callProc "printf" [strArg "Hello World!\n"]
-          (fp,h) <- openTempFile "" "temp.c"
-          hPutStrLn h c
-          hClose h
-          system $ "gcc " ++ fp
-          e <- system "./a.out"
-          removeFile fp
-          removeFile "a.out"
-          exitWith e
-
diff --git a/tests/Imperative.hs b/tests/Imperative.hs
new file mode 100644
--- /dev/null
+++ b/tests/Imperative.hs
@@ -0,0 +1,319 @@
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+
+-- | Tests for various constructs
+
+module Imperative where
+
+
+
+import Data.Int
+import Data.Word
+
+import Language.Embedded.Imperative
+import Language.Embedded.Backend.C
+import Language.Embedded.CExp
+
+
+
+type CMD
+    =   RefCMD
+    :+: ArrCMD
+    :+: ControlCMD
+    :+: PtrCMD
+    :+: FileCMD
+    :+: C_CMD
+
+type Prog = Program CMD (Param2 CExp CType)
+
+prog :: Prog ()
+prog = do
+    r <- initRef (10 :: CExp Int32)
+    a <- getRef r
+    modifyRef r (*a)
+    printf "%d\n" a
+
+
+
+-- | Test primitive types
+testTypes :: Prog ()
+testTypes = do
+    inp :: CExp Int32 <- fget stdin
+    a <- unsafeFreezeRef =<< initRef (i2n inp + 0x88               :: CExp Int8)
+    b <- unsafeFreezeRef =<< initRef (i2n inp + 0x8888             :: CExp Int16)
+    c <- unsafeFreezeRef =<< initRef (i2n inp + 0x88888888         :: CExp Int32)
+    d <- unsafeFreezeRef =<< initRef (i2n inp + 0x8888888888888888 :: CExp Int64)
+    e <- unsafeFreezeRef =<< initRef (i2n inp + 0xEE               :: CExp Word8)
+    f <- unsafeFreezeRef =<< initRef (i2n inp + 0xEEEE             :: CExp Word16)
+    g <- unsafeFreezeRef =<< initRef (i2n inp + 0xEEEEEEEE         :: CExp Word32)
+    h <- unsafeFreezeRef =<< initRef (i2n inp + 0xEEEEEEEEEEEEEEEE :: CExp Word64)
+    i <- unsafeFreezeRef =<< initRef (i2n inp - 9                  :: CExp Float)
+    j <- unsafeFreezeRef =<< initRef (i2n inp - 10                 :: CExp Double)
+    printf "%d %d %d %ld %u %u %u %lu %.3f %.3f\n" a b c d e f g h i j
+    k1 <- unsafeFreezeRef =<< initRef true
+    k2 <- unsafeFreezeRef =<< initRef true
+    iff ((k1 #&& k2) #|| not_ k1) (printf "true") (printf "false")
+
+testCExp :: Prog ()
+testCExp = do
+    a :: CExp Int32 <- fget stdin
+    let b = a#==10 ? a*3 $ a-5+8
+    let c = sin (i2n a) :: CExp Double
+    let d = c/23
+    printf "%d " b
+    printf "%d " (not_ (a#==10) ? a*3 $ a-5+8)
+    printf "%d " (a `quot_` b)
+    printf "%d " (a #% b)
+    printf "%d " (cond (i2b a) a b)
+    printf "%d " (b2i (not_ (a#==10)) * a)
+    printf "%.3f " c
+    printf "%.3f " d
+    printf "%.3f " (i2n a :: CExp Float)
+    printf "%ld "  (round_ (c*1000)              :: CExp Int32)
+    printf "%d "   (round_ (11.5 :: CExp Float)  :: CExp Int32)
+    printf "%d "   (round_ (-11.5 :: CExp Float) :: CExp Int32)
+    printf "%.3f " (c**d)
+
+testRef :: Prog ()
+testRef = do
+    r1 <- newRef
+    r2 <- initRef (3 :: CExp Int32)
+    modifyRef r2 (*2)
+    setRef r1 =<< getRef r2
+    a <- unsafeFreezeRef r1
+    b <- unsafeFreezeRef r2
+    printf "%d %d\n" a b
+
+testArr1 :: Prog ()
+testArr1 = do
+    arr1 :: Arr Word32 Int32 <- newArr (10 :: CExp Word32)
+    arr2 :: Arr Word32 Int32 <- newArr (10 :: CExp Word32)
+    sequence_ [setArr i (i2n i+10) arr1 | i' <- [0..9], let i = fromInteger i']
+    copyArr arr2 arr1 10
+    sequence_ [getArr i arr2 >>= printf "%d " . (*3) | i' <- [0..9], let i = fromInteger i']
+    printf "\n"
+
+testArr2 :: Prog ()
+testArr2 = do
+    n <- fget stdin
+    arr :: Arr Word32 Int32 <- newArr n  -- Array of dynamic length
+    sequence_ [setArr (i2n i) i arr | i' <- [0..3], let i = fromInteger i']
+    sequence_ [getArr i arr >>= printf "%d " . (*3) | i' <- [0..3], let i = fromInteger i']
+    printf "\n"
+    return ()
+
+testArr3 :: Prog ()
+testArr3 = do
+    arr :: Arr Word32 Int32 <- initArr [8,7,6,5]
+    sequence_ [getArr i arr >>= printf "%d " . (*3) | i' <- [0..3], let i = fromInteger i']
+    printf "\n"
+    return ()
+
+testArr4 :: Prog ()
+testArr4 = do
+    arr :: Arr Word32 Int32 <- initArr [8,7,6,5]
+    iarr <- freezeArr arr 4
+    sequence_ [printf "%d " $ iarr #! i | i' <- [0..3], let i = fromInteger i']
+    printf "\n"
+
+testArr5 :: Prog ()
+testArr5 = do
+    arr :: Arr Word32 Int32 <- initArr [8,7,6,5]
+    iarr <- unsafeFreezeArr arr
+    sequence_ [printf "%d " $ iarr #! i | i' <- [0..3], let i = fromInteger i']
+    printf "\n"
+
+testArr6 :: Prog ()
+testArr6 = do
+    arr :: Arr Word32 Int32 <- initArr [8,7,6,5]
+    iarr <- unsafeFreezeArr arr
+    arr2 <- unsafeThawArr iarr
+    sequence_ [getArr i arr2 >>= printf "%d " | i <- map fromInteger [0..3]]
+    printf "\n"
+
+testArr7 :: Prog ()
+testArr7 = do
+    arr :: Arr Word32 Int32 <- initArr [8,7,6,5]
+    iarr <- freezeArr arr 4
+    arr2 <- thawArr iarr 4
+    sequence_ [getArr i arr2 >>= printf "%d " | i <- map fromInteger [0..3]]
+    printf "\n"
+
+testSwap1 :: Prog ()
+testSwap1 = do
+    arr1 :: Arr Word32 Int32 <- initArr [1,2,3,4]
+    arr2 :: Arr Word32 Int32 <- initArr [11,12,13,14]
+    unsafeSwap arr1 arr2
+    sequence_ [getArr i arr1 >>= printf "%d " | i <- map fromInteger [0..3]]
+    printf "\n"
+
+testSwap2 :: Prog ()
+testSwap2 = do
+    arr1 :: Arr Word32 Int32 <- initArr [1,2,3,4]
+    n <- fget stdin
+    arr2 :: Arr Word32 Int32 <- newArr n
+    copyArr arr2 arr1 4
+    setArr 2 22 arr2
+    unsafeSwap arr1 arr2
+    sequence_ [getArr i arr1 >>= printf "%d " | i <- map fromInteger [0..3]]
+    printf "\n"
+    sequence_ [getArr i arr2 >>= printf "%d " | i <- map fromInteger [0..3]]
+    printf "\n"
+
+testIf1 :: Prog ()
+testIf1 = do
+    inp :: CExp Int32 <- fget stdin
+    a <- ifE (inp #== 10)        (return (inp+1)) (return (inp*3))
+    b <- ifE (not_ (inp #== 10)) (return (a+1))   (return (a*3))
+    printf "%d %d\n" a b
+
+testIf2 :: Prog ()
+testIf2 = do
+    inp :: CExp Int32 <- fget stdin
+    iff (inp #== 11)        (printf "== 11\n") (printf "/= 11\n")
+    iff (not_ (inp #== 11)) (printf "/= 11\n") (printf "== 11\n")
+    iff (inp #== 12)        (printf "== 12\n") (return ())
+    iff (not_ (inp #== 12)) (return ())        (printf "== 12\n")
+    iff (inp #== 13)        (printf "== 13\n") (return ())
+    iff (not_ (inp #== 13)) (return ())        (printf "== 13\n")
+    iff (inp #== 14)        (return ())        (return ())
+
+-- Loop from 0 to 9 in steps of 1
+testFor1 :: Prog ()
+testFor1 = for (0,1,9) $ \i ->
+    printf "%d\n" (i :: CExp Int8)
+
+-- Loop from 9 to 0 in steps of 2
+testFor2 :: Prog ()
+testFor2 = for (9,-2,0) $ \i ->
+    printf "%d\n" (i :: CExp Int8)
+
+-- Loop from 0 to but excluding 10 in steps of 2
+testFor3 :: Prog ()
+testFor3 = for (0, 2, Excl 10) $ \i ->
+    printf "%d\n" (i :: CExp Int8)
+
+-- While loop tested in `sumInput` in Demo.hs.
+
+testAssert :: Prog ()
+testAssert = do
+    inp :: CExp Int32 <- fget stdin
+    assert (inp #> 0) "input too small"
+    printf "past assertion\n"
+
+testPtr :: Prog ()
+testPtr = do
+    addInclude "<stdlib.h>"
+    addInclude "<string.h>"
+    addInclude "<stdio.h>"
+    p :: Ptr Int32 <- newPtr
+    callProcAssign p "malloc" [valArg (100 :: CExp Word32)]
+    arr :: Arr Word32 Int32 <- initArr [34,45,56,67,78]
+    callProc "memcpy" [ptrArg p, arrArg arr, valArg (5*4 :: CExp Word32)]  -- sizeof(int32_t) = 4
+    callProc "printf" [strArg "%d\n", deref $ ptrArg p]
+    iarr :: IArr Word32 Int32 <- unsafeFreezeArr =<< ptrToArr p
+    printf "sum: %d\n" (iarr#!0 + iarr#!1 + iarr#!2 + iarr#!3 + iarr#!4)
+    callProc "free" [ptrArg p]
+
+testArgs :: Prog ()
+testArgs = do
+    addInclude "<stdio.h>"
+    addDefinition setPtr_def
+    addDefinition ret_def
+    let v = 55 :: CExp Int32
+    r <- initRef (66 :: CExp Int32)
+    a :: Arr Int32 Int32 <- initArr [234..300]
+    ia <- freezeArr a 10
+    p :: Ptr Int32 <- newPtr
+    o <- newObject "int" False
+    op <- newObject "int" True
+    callProcAssign p "setPtr" [refArg r]
+    callProcAssign o "ret" [valArg v]
+    callProcAssign op "setPtr" [refArg r]
+    callProc "printf"
+        [ strArg "%d %d %d %d %d %d %d\n"
+        , valArg v
+        , deref (refArg r)
+        , deref (arrArg a)
+        , deref (iarrArg ia)
+        , deref (ptrArg p)
+        , objArg o
+        , deref (objArg op)
+        ]
+  where
+    setPtr_def = [cedecl|
+        int * setPtr (int *a) {
+            return a;
+        }
+        |]
+    ret_def = [cedecl|
+        int ret (int a) {
+            return a;
+        }
+        |]
+
+testExternArgs :: Prog ()
+testExternArgs = do
+    let v = 55 :: CExp Int32
+    externProc "val_proc" [valArg v]
+    r <- initRef v
+    externProc "ref_proc1" [refArg r]
+    externProc "ref_proc2" [deref $ refArg r]  -- TODO Simplify
+    a :: Arr Int32 Int32 <- newArr 10
+    externProc "arr_proc1" [arrArg a]
+    externProc "arr_proc2" [addr $ arrArg a]
+    externProc "arr_proc3" [deref $ arrArg a]
+    p :: Ptr Int32 <- newPtr
+    externProc "ptr_proc1" [ptrArg p]
+    externProc "ptr_proc2" [addr $ ptrArg p]
+    externProc "ptr_proc3" [deref $ ptrArg p]
+    o <- newObject "int" False
+    externProc "obj_proc1" [objArg o]
+    externProc "obj_proc2" [addr $ objArg o]
+    op <- newObject "int" True
+    externProc "obj_proc3" [objArg op]
+    externProc "obj_proc4" [addr $ objArg op]
+    externProc "obj_proc5" [deref $ objArg op]
+    let s = "apa"
+    externProc "str_proc1"  [strArg s]
+    externProc "str_proc2"  [deref $ strArg s]
+    return ()
+
+
+
+----------------------------------------
+
+-- It would be nice to be able to run these tests using Tests.Tasty.HUnit, but
+-- I wasn't able to make that work, probably due to the use of `fakeIO` in the
+-- tests. First, Tasty wasn't able to silence the output of the tests, and
+-- secondly, the tests would always fail when running a second time.
+
+testAll = do
+    tag "testTypes"  >> compareCompiled  testTypes  (runIO testTypes)                      "0\n"
+    tag "testCExp"   >> compareCompiledM testCExp   (runIO testCExp)                       "44\n"
+    tag "testRef"    >> compareCompiled  testRef    (runIO testRef)                        ""
+    tag "testArr1"   >> compareCompiled  testArr1   (runIO testArr1)                       ""
+    tag "testArr2"   >> compareCompiled  testArr2   (runIO testArr2)                       "20\n"
+    tag "testArr3"   >> compareCompiled  testArr3   (runIO testArr3)                       ""
+    tag "testArr4"   >> compareCompiled  testArr4   (runIO testArr4)                       ""
+    tag "testArr5"   >> compareCompiled  testArr5   (runIO testArr5)                       ""
+    tag "testArr6"   >> compareCompiled  testArr6   (runIO testArr6)                       ""
+    tag "testArr7"   >> compareCompiled  testArr7   (runIO testArr6)                       ""
+    tag "testArr7"   >> compareCompiled  testArr7   (runIO testArr7)                       ""
+    tag "testSwap1"  >> compareCompiled  testSwap1  (runIO testSwap1)                      ""
+    tag "testSwap2"  >> compareCompiled  testSwap2  (runIO testSwap2)                      "45\n"
+    tag "testIf1"    >> compareCompiled  testIf1    (runIO testIf1)                        "12\n"
+    tag "testIf2"    >> compareCompiled  testIf2    (runIO testIf2)                        "12\n"
+    tag "testFor1"   >> compareCompiled  testFor1   (runIO testFor1)                       ""
+    tag "testFor2"   >> compareCompiled  testFor2   (runIO testFor2)                       ""
+    tag "testFor3"   >> compareCompiled  testFor3   (runIO testFor3)                       ""
+    tag "testAssert" >> compareCompiled  testAssert (runIO testAssert)                     "45"
+    tag "testPtr"    >> compareCompiled  testPtr    (putStrLn "34" >> putStrLn "sum: 280") ""
+    tag "testArgs"   >> compareCompiled  testArgs   (putStrLn "55 66 234 234 66 55 66")    ""
+    tag "testExternArgs" >> compileAndCheck  testExternArgs
+  where
+    tag str = putStrLn $ "---------------- tests/Imperative.hs/" ++ str ++ "\n"
+    compareCompiledM = compareCompiled'
+        defaultExtCompilerOpts {externalFlagsPost = ["-lm"]}
+
diff --git a/tests/Semantics.hs b/tests/Semantics.hs
deleted file mode 100644
--- a/tests/Semantics.hs
+++ /dev/null
@@ -1,22 +0,0 @@
-import Language.Embedded.Expression (evalExp)
-import Language.Embedded.Imperative
-import Language.Embedded.CExp
-
-
-
--- Test that `modifyRef` doesn't loop. It will loop if evaluation of `setRef` is
--- too lazy so that the `unsafeFreezeRef` happens before `setRef` in
--- `modifyRef`.
-modifyRefProg :: Program (RefCMD CExp) (CExp Int32)
-modifyRefProg = do
-    r <- initRef 0
-    modifyRef r (+1)
-    getRef r
-
-testModifyRef = do
-    1 <- fmap evalExp $ runIO modifyRefProg
-    return ()
-
-main = do
-    testModifyRef
-
diff --git a/tests/Tests.hs b/tests/Tests.hs
new file mode 100644
--- /dev/null
+++ b/tests/Tests.hs
@@ -0,0 +1,11 @@
+import qualified Imperative
+import qualified Concurrent
+import qualified Demo
+import qualified CExp
+
+main = do
+    Imperative.testAll
+    Concurrent.testAll
+    Demo.testAll
+    CExp.main
+