diff --git a/ivory-backend-c.cabal b/ivory-backend-c.cabal
--- a/ivory-backend-c.cabal
+++ b/ivory-backend-c.cabal
@@ -2,7 +2,7 @@
 --  see http://haskell.org/cabal/users-guide/
 
 name:                ivory-backend-c
-version:             0.1.0.1
+version:             0.1.0.3
 author:              Galois, Inc.
 maintainer:          leepike@galois.com
 category:            Language
@@ -12,13 +12,14 @@
 build-type:          Simple
 cabal-version:       >= 1.10
 data-files:             runtime/ivory.h,
+                        runtime/ivory_templates.h,
                         runtime/ivory_asserts.h
 license:             BSD3
 license-file:        LICENSE
 source-repository    this
   type:     git
   location: https://github.com/GaloisInc/ivory
-  tag:      hackage-backend-0101
+  tag:      hackage-backend-0103
 
 library
   exposed-modules:      Ivory.Compile.C,
@@ -27,25 +28,24 @@
                         Ivory.Compile.C.Prop,
                         Ivory.Compile.C.Types,
                         Ivory.Compile.C.CmdlineFrontend,
-                        Ivory.Compile.C.CmdlineFrontend.Options,
-                        Ivory.Compile.C.SourceDeps
+                        Ivory.Compile.C.CmdlineFrontend.Options
   other-modules:        Paths_ivory_backend_c
 
-  build-depends:        base >= 4.6 && < 4.7,
-                        language-c-quote >= 0.7.1,
-                        -- XXX remove when inits quasi-quote escape is added
+  build-depends:        base >= 4.6 && < 5,
+                        base-compat,
+                        language-c-quote >= 0.10.0,
                         srcloc,
                         mainland-pretty >= 0.2.5,
                         monadLib >= 3.7,
                         template-haskell >= 2.8,
                         bytestring >= 0.10,
-                        ivory,
-                        ivory-opts,
                         directory,
                         filepath,
                         process,
-                        cmdlib >= 0.3.5,
-                        containers
+                        containers,
+                        ivory,
+                        ivory-opts,
+                        ivory-artifact
   hs-source-dirs:       src
   default-language:     Haskell2010
 
diff --git a/runtime/ivory.h b/runtime/ivory.h
--- a/runtime/ivory.h
+++ b/runtime/ivory.h
@@ -1,124 +1,185 @@
 #ifndef IVORY_H
 #define IVORY_H
 
-#include<stdint.h>
-#include<math.h>
-#include<stdbool.h>
-#include<string.h>
-#include<limits.h>
+#include <stdint.h>
+#include <math.h>
+#include <string.h>
+#include <limits.h>
 
 #include "ivory_asserts.h"
+#include "ivory_templates.h"
 
 #define FOREVER true
 #define FOREVER_INC
 
-/* abs implementations */
+// ----------------------------------------
 
+#define TYPE char
+#define EXT  char
+#define M    CHAR
+
 #if (CHAR_MIN < 0)
-static inline char abs_char(char i) {
-  COMPILER_ASSERTS(i != CHAR_MIN);
-  return i >= 0 ? i : -i;
-}
+ABS_I
+SIGNUM_I
+ADD_OVF_I
+SUB_OVF_I
+MUL_OVF_I
+DIV_OVF_I
 #else
 static inline char abs_char(char i) {
   return i;
 }
+SIGNUM_U
+ADD_OVF_U
+SUB_OVF_U
+MUL_OVF_U
+
 #endif
 
-static inline int8_t abs_i8(int8_t i) {
-  COMPILER_ASSERTS(i != INT8_MIN);
-  return i >= 0 ? i : -i;
-}
+#undef TYPE
+#undef EXT
+#undef M
 
-static inline int16_t abs_i16(int16_t i) {
-  COMPILER_ASSERTS(i != INT16_MIN);
-  return i >= 0 ? i : -i;
-}
+// ----------------------------------------
 
-static inline int32_t abs_i32(int32_t i) {
-  COMPILER_ASSERTS(i != INT32_MIN);
-  return i >= 0 ? i : -i;
-}
+#define TYPE int8_t
+#define EXT  i8
+#define M    INT8
+ABS_I
+SIGNUM_I
+ADD_OVF_I
+SUB_OVF_I
+MUL_OVF_I
+DIV_OVF_I
+#undef TYPE
+#undef EXT
+#undef M
 
-static inline int64_t abs_i64(int64_t i) {
-  COMPILER_ASSERTS(i != INT64_MIN);
-  return i >= 0 ? i : -i;
-}
+// ----------------------------------------
 
-/* signum implementations */
 
-#if (CHAR_MIN < 0)
-static inline char signum_char(char i) {
-  if (i > 0) return 1;
-  if (i < 0) return (-1);
-  return 0;
-}
-#else
-static inline char signum_char(char i) {
-  if (i > 0) return 1;
-  return 0;
-}
-#endif
+#define TYPE int16_t
+#define EXT  i16
+#define M    INT16
+ABS_I
+SIGNUM_I
+ADD_OVF_I
+SUB_OVF_I
+MUL_OVF_I
+DIV_OVF_I
+#undef TYPE
+#undef EXT
+#undef M
 
-static inline int8_t signum_i8(int8_t i) {
-  if (i > 0) return 1;
-  if (i < 0) return (-1);
-  return 0;
-}
+// ----------------------------------------
 
-static inline int16_t signum_i16(int16_t i) {
-  if (i > 0) return 1;
-  if (i < 0) return (-1);
-  return 0;
-}
+#define TYPE int32_t
+#define EXT  i32
+#define M    INT32
+ABS_I
+SIGNUM_I
+ADD_OVF_I
+SUB_OVF_I
+MUL_OVF_I
+DIV_OVF_I
+#undef TYPE
+#undef EXT
+#undef M
 
-static inline int32_t signum_i32(int32_t i) {
-  if (i > 0) return 1;
-  if (i < 0) return (-1);
-  return 0;
-}
+// ----------------------------------------
 
-static inline int64_t signum_i64(int64_t i) {
-  if (i > 0) return 1;
-  if (i < 0) return (-1);
-  return 0;
-}
+#define TYPE int64_t
+#define EXT  i64
+#define M    INT64
+ABS_I
+SIGNUM_I
+ADD_OVF_I
+SUB_OVF_I
+MUL_OVF_I
+DIV_OVF_I
+#undef TYPE
+#undef EXT
+#undef M
 
-static inline float signum_float(float i) {
-  if (i > 0) return 1;
-  if (i < 0) return (-1);
-  return 0;
-}
+// ----------------------------------------
+// The types below don't need an abs implementation
+// ----------------------------------------
 
-static inline double signum_double(double i) {
-  if (i > 0) return 1;
-  if (i < 0) return (-1);
-  return 0;
-}
+// ----------------------------------------
 
-static inline uint8_t signum_u8(uint8_t i) {
-  if (i > 0) return 1;
-  return 0;
-}
+#define TYPE float
+#define EXT  float
+SIGNUM_I
+#undef TYPE
+#undef EXT
 
-static inline uint16_t signum_u16(uint16_t i) {
-  if (i > 0) return 1;
-  return 0;
-}
+// ----------------------------------------
 
-static inline uint32_t signum_u32(uint32_t i) {
-  if (i > 0) return 1;
-  return 0;
-}
+#define TYPE double
+#define EXT  double
+SIGNUM_I
+#undef TYPE
+#undef EXT
 
-static inline uint64_t signum_u64(uint64_t i) {
-  if (i > 0) return 1;
-  return 0;
-}
+// ----------------------------------------
 
-/* index type */
+#define TYPE uint8_t
+#define EXT  u8
+#define M    UINT8
+SIGNUM_U
+ADD_OVF_U
+SUB_OVF_U
+MUL_OVF_U
+DIV_OVF_U
+#undef TYPE
+#undef EXT
+#undef M
 
-/* machine-depdentent size */
+// ----------------------------------------
+
+#define TYPE uint16_t
+#define EXT  u16
+#define M    UINT16
+SIGNUM_U
+ADD_OVF_U
+SUB_OVF_U
+MUL_OVF_U
+DIV_OVF_U
+#undef TYPE
+#undef EXT
+#undef M
+
+// ----------------------------------------
+
+#define TYPE uint32_t
+#define EXT  u32
+#define M    UINT32
+SIGNUM_U
+ADD_OVF_U
+SUB_OVF_U
+MUL_OVF_U
+DIV_OVF_U
+#undef TYPE
+#undef EXT
+#undef M
+
+// ----------------------------------------
+
+#define TYPE uint64_t
+#define EXT  u64
+#define M    UINT64
+SIGNUM_U
+ADD_OVF_U
+SUB_OVF_U
+MUL_OVF_U
+DIV_OVF_U
+#undef TYPE
+#undef EXT
+#undef M
+
+// ----------------------------------------
+
+// Index type: machine-depdentent size
 typedef int idx;
 
 #endif // IVORY_H
diff --git a/runtime/ivory_asserts.h b/runtime/ivory_asserts.h
--- a/runtime/ivory_asserts.h
+++ b/runtime/ivory_asserts.h
@@ -5,15 +5,14 @@
 
 #ifdef IVORY_TEST
 
-#ifdef __arm__
+#if defined(IVORY_USER_ASSERT_HOOK)
 
-/* TODO: We could write a better "assert" that suspends all RTOS
- * tasks and tries to write a debug string somewhere, but this is at
- * least somewhat useful while running under GDB. */
+extern void ivory_user_assert_hook(void);
+
 #define ivory_assert(arg)         \
   do {                            \
     if (!(arg)) {                 \
-      asm volatile("bkpt");       \
+       ivory_user_assert_hook();  \
     }                             \
   } while (0)
 
@@ -23,8 +22,26 @@
 #define ASSERTS(arg)          ivory_assert(arg)
 #define COMPILER_ASSERTS(arg) ivory_assert(arg)
 
-#else /* ! __arm__ */
+#elif defined(IVORY_USER_VERBOSE_ASSERT_HOOK)
 
+extern void ivory_user_verbose_assert_hook(const char *asserttype,
+		const char *expr, const char *file, int line);
+
+#define ivory_assert(atype, arg)  \
+  do {                            \
+    if (!(arg)) {                 \
+       ivory_user_verbose_assert_hook(atype, #arg, __FILE__, __LINE__); \
+    }                             \
+  } while (0)
+
+#define REQUIRES(arg)         ivory_assert("REQUIRES",arg)
+#define ENSURES(arg)          ivory_assert("ENSURES",arg)
+#define ASSUMES(arg)          ivory_assert("ASSUMES",arg)
+#define ASSERTS(arg)          ivory_assert("ASSERTS",arg)
+#define COMPILER_ASSERTS(arg) ivory_assert("COMPILER_ASSERTS",arg)
+
+#else
+
 #include <assert.h>
 
 #define REQUIRES(arg)         assert(arg)
@@ -33,11 +50,9 @@
 #define ASSERTS(arg)          assert(arg)
 #define COMPILER_ASSERTS(arg) assert(arg)
 
-#endif /* __arm__ */
-
-#endif /* IVORY_TEST */
+#endif /* assert hooks */
 
-#ifdef IVORY_DEPLOY
+#else /* IVORY_TEST */
 
 #define REQUIRES(arg)
 #define ENSURES(arg)
@@ -45,6 +60,6 @@
 #define ASSERTS(arg)
 #define COMPILER_ASSERTS(arg)
 
-#endif /* IVORY_DEPLOY */
+#endif /* IVORY_TEST */
 
 #endif /* IVORY_ASSERTS_H */
diff --git a/runtime/ivory_templates.h b/runtime/ivory_templates.h
new file mode 100644
--- /dev/null
+++ b/runtime/ivory_templates.h
@@ -0,0 +1,96 @@
+#ifndef IVORY_TEMPLATES_H
+#define IVORY_TEMPLATES_H
+
+#include<stdbool.h>
+#include<limits.h>
+
+#define CAT(X,Y) X##_##Y
+// Indirection in case X,Y defined
+#define C(X,Y) CAT(X,Y)
+
+#define MKMAX(X) C(X,MAX)
+#define MKMIN(X) C(X,MIN)
+
+// abs implementations for signed types
+// note: -MIN may not equal MAX
+#define ABS_I                                       \
+static inline TYPE C(abs,EXT)(TYPE i) {             \
+  if(i == MKMIN(M)) { return MKMAX(M); }            \
+  else { return i >= 0 ? i : -i; }                  \
+}
+
+// Unsigned signnum
+#define SIGNUM_U                                    \
+static inline TYPE C(signum,EXT)(TYPE i) {          \
+  if (i > 0) return 1;                              \
+  return 0;                                         \
+}
+
+// Signed signum
+#define SIGNUM_I                                    \
+static inline TYPE C(signum,EXT)(TYPE i) {          \
+  if (i > 0) return 1;                              \
+  if (i < 0) return (-1);                           \
+  return 0;                                         \
+}
+
+// Addition overflow check for signed types
+#define ADD_OVF_I                                   \
+static inline bool C(add_ovf,EXT)(TYPE x, TYPE y) { \
+  return (x >= 0 && y >= 0 && MKMAX(M) - x >= y)    \
+      || (x <= 0 && y <= 0 && MKMIN(M) - x <= y)    \
+      || (C(signum,EXT)(x) != C(signum,EXT)(y));    \
+}
+
+// Addition overflow check for unsigned types
+#define ADD_OVF_U                                   \
+static inline bool C(add_ovf,EXT)(TYPE x, TYPE y) { \
+  return MKMAX(M) - x >= y;                         \
+}
+
+// Subtraction overflow check for signed types
+#define SUB_OVF_I                                   \
+static inline bool C(sub_ovf,EXT)(TYPE x, TYPE y) { \
+  return (x >= 0 && y <= 0 && MKMAX(M) + y >= x)    \
+      || (x <= 0 && y >= 0 && MKMIN(M) + y <= x)    \
+      || (C(signum,EXT)(x) == C(signum,EXT)(y));    \
+}
+
+// Subtraction overflow check for unsigned types
+#define SUB_OVF_U                                   \
+static inline bool C(sub_ovf,EXT)(TYPE x, TYPE y) { \
+  return x >= y;                                    \
+}
+
+// Multiplication overflow check for signed types.  Note use of our safe abs
+// function here.
+#define MUL_OVF_I                                          \
+static inline bool C(mul_ovf,EXT)(TYPE x, TYPE y) {        \
+  return (x != MKMIN(M) || y != (-1))                      \
+      && (y != MKMIN(M) || x != (-1))                      \
+      && (   x == 0                                        \
+          || y == 0                                        \
+          || (   MKMAX(M) / C(abs,EXT)(x) >= C(abs,EXT)(y) \
+              && MKMIN(M) / C(abs,EXT)(x) <= C(abs,EXT)(y) \
+         ));                                               \
+}
+
+// Multiplication overflow check for unsigned types.
+#define MUL_OVF_U                                    \
+static inline bool C(mul_ovf,EXT)(TYPE x, TYPE y) {  \
+  return x == 0 || MKMAX(M) / x >= y;                \
+}
+
+// Division overflow check for signed types.
+#define DIV_OVF_I                                    \
+static inline bool C(div_ovf,EXT)(TYPE x, TYPE y) {  \
+  return y != 0 && (x != MKMIN(M) || y != (-1));     \
+}
+
+// Division overflow check for unsigned types.
+#define DIV_OVF_U                                                             \
+  static inline bool C(div_ovf,EXT)(__attribute__((unused)) TYPE x, TYPE y) { \
+  return y != 0;                                                              \
+}
+
+#endif // IVORY_TEMPLATES_H
diff --git a/src/Ivory/Compile/C.hs b/src/Ivory/Compile/C.hs
--- a/src/Ivory/Compile/C.hs
+++ b/src/Ivory/Compile/C.hs
@@ -3,8 +3,6 @@
   , compileModule
   , runOpt
   , showModule
-  , writeHdr
-  , writeSrc
   , renderHdr
   , renderSrc
   , CompileUnits(..)
diff --git a/src/Ivory/Compile/C/CmdlineFrontend.hs b/src/Ivory/Compile/C/CmdlineFrontend.hs
--- a/src/Ivory/Compile/C/CmdlineFrontend.hs
+++ b/src/Ivory/Compile/C/CmdlineFrontend.hs
@@ -6,196 +6,249 @@
   , runCompilerWith
   , Opts(..), parseOpts, printUsage
   , initialOpts
+  , compileUnits
+  , outputCompiler
   ) where
 
-import qualified Paths_ivory_backend_c
-import qualified Ivory.Compile.C as C
-import qualified Ivory.Compile.C.SourceDeps as C
+import           Data.List                  (nub, (\\), intercalate)
+import qualified Paths_ivory_backend_c      as P
+import qualified Ivory.Compile.C            as C
 
 import           Ivory.Compile.C.CmdlineFrontend.Options
 
 import           Ivory.Language
-import qualified Ivory.Opts.ConstFold as O
-import qualified Ivory.Opts.Overflow as O
-import qualified Ivory.Opts.DivZero as O
-import qualified Ivory.Opts.Index as O
-import qualified Ivory.Opts.FP as O
-import qualified Ivory.Opts.CFG as G
+import           Ivory.Artifact
+import           Ivory.Language.Syntax.AST  as I
+import qualified Ivory.Opts.BitShift        as O
+import qualified Ivory.Opts.ConstFold       as O
+import qualified Ivory.Opts.CSE             as O
+import qualified Ivory.Opts.Overflow        as O
+import qualified Ivory.Opts.DivZero         as O
+import qualified Ivory.Opts.Index           as O
+import qualified Ivory.Opts.FP              as O
+import qualified Ivory.Opts.SanityCheck     as S
+import qualified Ivory.Opts.TypeCheck       as T
 
-import qualified Data.ByteString.Char8 as B
 
+import Data.Maybe (mapMaybe, catMaybes)
 import Control.Monad (when)
 import Data.List (foldl')
-import System.Directory (doesFileExist,createDirectoryIfMissing)
+import System.Directory (createDirectoryIfMissing)
 import System.Environment (getArgs)
-import System.FilePath (takeDirectory,takeExtension,addExtension,(</>))
-import Text.PrettyPrint.Mainland
-    ((<+>),(<>),line,text,stack,punctuate,render,empty,indent,displayS)
-import qualified System.FilePath.Posix as PFP
-
+import System.FilePath (addExtension,(</>))
 
 -- Code Generation Front End ---------------------------------------------------
 
-compile :: [Module] -> IO ()
-compile = compileWith Nothing Nothing
+compile :: [Module] -> [Located Artifact] -> IO ()
+compile = compileWith
 
-compileWith :: Maybe G.SizeMap -> Maybe [IO FilePath] -> [Module] -> IO ()
-compileWith sm sp ms = runCompilerWith sm sp ms =<< parseOpts =<< getArgs
+compileWith :: [Module] -> [Located Artifact] -> IO ()
+compileWith ms as = do
+  args <- getArgs
+  opts <- parseOpts args
+  runCompilerWith ms as opts
 
-runCompilerWith :: Maybe G.SizeMap -> Maybe [IO FilePath] -> [Module] -> Opts -> IO ()
-runCompilerWith sm sp =
-  rc (maybe G.defaultSizeMap id sm) (maybe [] id sp)
+runCompiler :: [Module] -> [Located Artifact] -> Opts -> IO ()
+runCompiler ms as os = runCompilerWith ms as os
 
-runCompiler :: [Module] -> Opts -> IO ()
-runCompiler = runCompilerWith Nothing Nothing
+-- | Main compile function plus domain-specific type-checking that can't be
+-- embedded in the Haskell type-system.  Type-checker also emits warnings.
+runCompilerWith ::[Module] -> [Located Artifact] -> Opts -> IO ()
+runCompilerWith modules artifacts opts = do
+  cmodules <- compileUnits modules opts
+  if outProcSyms opts
+    then C.outputProcSyms modules
+    else outputCompiler cmodules artifacts opts
 
-rc :: G.SizeMap -> [IO FilePath] -> [Module] -> Opts -> IO ()
-rc sm userSearchPath modules opts
-  | outProcSyms opts = C.outputProcSyms modules
-  | printDeps        = runDeps
-  | otherwise        = do
-    if stdOut opts then mapM_ showM_ cmodules else run
-    -- CFG stuff
-    when (cfg opts) $ do
-      cfs <- mapM (\p -> G.callGraphDot p (cfgDotDir opts) optModules) cfgps
-      let maxstacks = map ms (zip cfgps cfs)
-      mapM_ maxStackMsg (zip cfgps maxstacks)
+outputCompiler :: [C.CompileUnits] -> [Located Artifact] -> Opts -> IO ()
+outputCompiler cmodules artifacts opts
+  | Nothing <- outDir opts
+  = stdoutmodules cmodules
+  | otherwise
+  = outputmodules opts cmodules artifacts
+
+stdoutmodules :: [C.CompileUnits] -> IO ()
+stdoutmodules cmodules =
+  mapM_ (putStrLn . C.showModule) cmodules
+
+outputmodules :: Opts -> [C.CompileUnits] -> [Located Artifact] -> IO ()
+outputmodules opts cmodules user_artifacts = do
+  -- Irrrefutable pattern checked above
+  let Just srcdir = outDir opts
+  let incldir = hdrDir srcdir
+  let rootdir = rootDir srcdir
+  createDirectoryIfMissing True rootdir
+  createDirectoryIfMissing True srcdir
+  createDirectoryIfMissing True incldir
+  let artifacts = runtimeHeaders ++ user_artifacts
+  warnCollisions cmodules artifacts rootdir srcdir incldir
+  mapM_ (output srcdir ".c" renderSource) cmodules
+  mapM_ (output incldir  ".h" renderHeader) cmodules
+  runArtifactCompiler artifacts rootdir srcdir incldir
+
   where
-  ivoryHeaders = ["ivory.h", "ivory_asserts.h"]
+  hdrDir dir =
+    case outHdrDir opts of
+      Nothing -> dir
+      Just d  -> d
 
-  run = do
-    searchPath <- mkSearchPath opts userSearchPath
-    createDirectoryIfMissing True (includeDir opts)
-    createDirectoryIfMissing True (srcDir opts)
-    outputHeaders (includeDir opts) cmodules
-    outputSources (srcDir opts) cmodules
-    C.outputSourceDeps (includeDir opts) (srcDir opts)
-       (map ("runtime/" ++) ivoryHeaders ++ (C.collectSourceDeps modules)) searchPath
+  rootDir dir =
+    case outArtDir opts of -- XXX TODO: fix outArtDir naming, should be outRootDir or somethign
+      Nothing -> dir
+      Just d  -> d
 
-  runDeps =
-    outputDeps (deps opts) (depPrefix opts) (genHs ++ cpyHs) (genSs ++ cpySs)
+  output :: FilePath -> FilePath -> (C.CompileUnits -> String)
+         -> C.CompileUnits
+         -> IO ()
+  output dir ext render m = outputHelper fout (render m)
+    where fout = addExtension (dir </> (C.unitName m)) ext
+
+  renderHeader cu = C.renderHdr (C.headers cu) (C.unitName cu)
+  renderSource cu = C.renderSrc (C.sources cu)
+
+  outputHelper :: FilePath -> String -> IO ()
+  outputHelper fname contents = case verbose opts of
+    False -> out
+    True -> do
+      putStr ("Writing to file " ++ fname ++ "...")
+      out
+      putStrLn " Done"
     where
-    sdeps = C.collectSourceDeps modules
-    genHs = map (mkDep (includeDir opts) ".h") cmodules
-    genSs = map (mkDep (srcDir opts) ".c")     cmodules
-    cpyHs = map (mkDepSourceDep (includeDir opts)) $
-              filter (\p -> takeExtension p == ".h") sdeps
-    cpySs = map (mkDepSourceDep (srcDir opts)) $
-              filter (\p -> takeExtension p == ".c") sdeps
+    out = writeFile fname contents
 
-  optModules = map (C.runOpt passes) modules
+-- | Compile, type-check, and optimize modules, but don't generate C files.
+compileUnits ::[Module] -> Opts -> IO [C.CompileUnits]
+compileUnits modules opts = do
+  let (bs, msgs) = concatRes (map tcMod modules)
+  putStrLn msgs
+  when (scErrors opts) $ do
+    let (bs', msgs') = concatRes (map scMod modules)
+    when bs' $ do
+      putStrLn msgs'
+      error "Sanity-check failed!"
+  when (tcErrors opts && bs) (error "There were type-checking errors.")
+  return (mkCUnits modules opts)
+  where
+  concatRes :: [(Bool, String)] -> (Bool, String)
+  concatRes r = let (bs, strs) = unzip r in
+                (or bs, concat strs)
 
-  cfgps = cfgProc opts
+  scMod :: I.Module -> (Bool, String)
+  scMod m = (S.existErrors res, S.render msg)
+    where
+    res = S.sanityCheck modules m
+    msg = S.showErrors (I.modName m) res
 
-  ms (p, cf) = G.maxStack p cf sm
-  maxStackMsg :: (String, G.WithTop Integer) -> IO ()
-  maxStackMsg (p,res) =
-    putStrLn $ "Maximum stack usage from function " ++ p ++ ": " ++ show res
+  tcMod :: I.Module -> (Bool, String)
+  tcMod m = concatRes reses
 
-  cmodules   = map C.compileModule optModules
+    where
+    showWarnings = tcWarnings opts
 
-  printDeps = not (null (deps opts))
+    allProcs vs = I.public vs ++ I.private vs
 
-  showM_ mods = do
-    mapM_ (mapM_ putStrLn) (C.showModule mods)
+    reses :: [(Bool, String)]
+    reses = map tcProc (allProcs (I.modProcs m))
 
-  cfPass = mkPass constFold O.constFold
+    tcProc :: I.Proc -> (Bool, String)
+    tcProc p = ( T.existErrors tc
+               , errs ++ if showWarnings then warnings else []
+               )
+      where
+      tc       = T.typeCheck p
+      res f    = unlines $ f (I.procSym p) tc
+      warnings = res T.showWarnings
+      errs     = res T.showErrors
 
+mkCUnits :: [Module] -> Opts -> [C.CompileUnits]
+mkCUnits modules opts = cmodules
+  where
+  cmodules            = map C.compileModule optModules
+  optModules          = map (C.runOpt passes) modules
+
+  cfPass              = mkPass constFold O.constFold
   -- Put new assertion passes here and add them to passes below.
-  ofPass = mkPass overflow O.overflowFold
-  dzPass = mkPass divZero O.divZeroFold
-  fpPass = mkPass fpCheck O.fpFold
-  ixPass = mkPass ixCheck O.ixFold
+  ofPass              = mkPass overflow O.overflowFold
+  dzPass              = mkPass divZero O.divZeroFold
+  fpPass              = mkPass fpCheck O.fpFold
+  ixPass              = mkPass ixCheck O.ixFold
+  bsPass              = mkPass bitShiftCheck O.bitShiftFold
+  locPass             = mkPass (not . srcLocs) dropSrcLocs
 
   mkPass passOpt pass = if passOpt opts then pass else id
 
-  -- Constant folding before and after all other passes.
+  -- CSE first, because it uses observable sharing for efficiency, which will
+  -- be lost if any other re-writes happen before it.
+  --
+  -- Next, prune any source locations we don't need.
+  --
+  -- Finally, constant folding before and after all assertion passes.
+  --
+  -- XXX This should be made more efficient at some point, since each pass
+  --traverses the AST.  It's not obvious how to do that cleanly, though.
   passes e = foldl' (flip ($)) e
-    [ cfPass
-    , ofPass, dzPass, fpPass, ixPass
+    [ O.cseFold
+    , locPass
     , cfPass
+    , ofPass, dzPass, fpPass, ixPass, bsPass
+    , cfPass
     ]
 
-  -- Output headers in a directory
-  outputHeaders :: FilePath -> [C.CompileUnits] -> IO ()
-  outputHeaders fp cus = mapM_ (process outputHeader fp) cus
-  -- Output sources in a directory
-  outputSources :: FilePath -> [C.CompileUnits] -> IO ()
-  outputSources fp cus = mapM_ (process outputSrc fp) cus
-
-  process outputter dir m = outputter (dir </> (C.unitName m)) m
-
-  -- Transform a compiled unit into a header, and write to a .h file
-  outputHeader :: FilePath -> C.CompileUnits -> IO ()
-  outputHeader basename cm = do
-    let headerfname = addExtension basename ".h"
-        header = C.renderHdr (C.headers cm) (C.unitName cm)
-    outputHelper headerfname header
-
-  -- Transform a compiled unit into a c src, and write to a .c file
-  outputSrc :: FilePath -> C.CompileUnits -> IO ()
-  outputSrc basename cm = do
-    let srcfname = addExtension basename ".c"
-        src = C.renderSrc (C.sources cm)
-    outputHelper srcfname src
+--------------------------------------------------------------------------------
 
-  outputHelper :: FilePath -> String -> IO ()
-  outputHelper fname contents = case verbose opts of
-    False -> out
-    True -> do
-      putStr ("Writing to file " ++ fname ++ "...")
-      out
-      putStrLn " Done"
-    where
-    out = writeFile fname contents
+runArtifactCompiler :: [Located Artifact] -> FilePath -> FilePath -> FilePath
+                    -> IO ()
+runArtifactCompiler las root_dir src_dir incl_dir = do
+  mes <- sequence
+    [ case la of
+       Root a -> putArtifact root_dir a
+       Src a  -> putArtifact src_dir a
+       Incl a -> putArtifact incl_dir a
+    | la <- las ]
+  case catMaybes mes of
+    [] -> return ()
+    errs -> error (unlines errs)
 
 --------------------------------------------------------------------------------
 
-mkDep :: FilePath -> String -> C.CompileUnits -> String
-mkDep basepath extension unit = basepath PFP.</> (C.unitName unit) PFP.<.> extension
-
-mkDepSourceDep :: FilePath -> FilePath -> String
-mkDepSourceDep basepath sdep = basepath PFP.</> sdep
+runtimeHeaders :: [Located Artifact]
+runtimeHeaders = map a [ "ivory.h", "ivory_asserts.h", "ivory_templates.h" ]
+  where a f = Incl $ artifactCabalFile P.getDataDir ("runtime/" ++ f)
 
-outputDeps :: FilePath -> String -> [String] -> [String] -> IO ()
-outputDeps path prefix headers sources = do
-  createDirectoryIfMissing True (takeDirectory path)
-  outputIfChanged path docstring
+--------------------------------------------------------------------------------
+warnCollisions :: [C.CompileUnits] -- All Ivory Modules
+               -> [Located Artifact] -- All artifacts
+               -> FilePath  -- Root path
+               -> FilePath  -- Source path
+               -> FilePath  -- Incl path
+               -> IO ()
+warnCollisions ms as rootpath spath ipath = case dupes of
+  [] -> return ()
+  _ -> putStrLn $ intercalate "\n\t" $
+    ["**** Warning: the following files will be written multiple times during codegen! ****"]
+    ++ dupes
   where
-  docstring = displayS (render w d) ""
-  w = 10000000 -- don't ever wrap lines - invalid make syntax
-  d = stack $
-    [ text "# dep file autogenerated by ivory compiler"
-    , empty
-    , listof (prefix ++ "_HEADERS") headers
-    , empty
-    , listof (prefix ++ "_SOURCES") sources
-    ]
-  declaration n = text n <+> text ":= \\" <> line
-  listof name values = declaration name <>
-    (indent 4 $ stack $ punctuate (text " \\") (map text values))
+  cnames = [ spath </> (C.unitName m ++ ".c") | m <- ms ]
+  hnames = [ ipath </> (C.unitName m ++ ".h") | m <- ms ]
+  anames = [ case la of
+              Root a -> rootpath </> artifactFileName a
+              Src a  -> spath </>  artifactFileName a
+              Incl a -> ipath </>  artifactFileName a
+           | la <- as ]
+  allnames = cnames ++ hnames ++ anames
+  dupes = allnames \\ (nub allnames)
 
-outputIfChanged :: FilePath -> String -> IO ()
-outputIfChanged path string_contents = do
-  let contents = B.pack string_contents
-  exists <- doesFileExist path
-  case exists of
-    False -> B.writeFile path contents
-    True -> do
-      existing <- B.readFile path
-      case existing == contents of
-          True -> return ()
-          False -> B.writeFile path contents
 
+--------------------------------------------------------------------------------
 
-mkSearchPath :: Opts -> [IO FilePath] -> IO [FilePath]
-mkSearchPath opts userSearchPaths = do
-  rtPath <- getRtPath
-  users <- sequence userSearchPaths
-  return $ rtPath:users
+dropSrcLocs :: I.Proc -> I.Proc
+dropSrcLocs p = p { I.procBody = dropSrcLocsBlock (I.procBody p) }
   where
-  getRtPath :: IO FilePath
-  getRtPath  = case rtIncludeDir opts of
-    Just path -> return path
-    Nothing   -> Paths_ivory_backend_c.getDataDir
-
+  dropSrcLocsBlock = mapMaybe go
+  go stmt = case stmt of
+    I.IfTE b t f              -> Just $ I.IfTE b (dropSrcLocsBlock t)
+                                                 (dropSrcLocsBlock f)
+    I.Loop m v e i b          -> Just $ I.Loop m v e i (dropSrcLocsBlock b)
+    I.Forever b               -> Just $ I.Forever (dropSrcLocsBlock b)
+    I.Comment (I.SourcePos _) -> Nothing
+    _                         -> Just stmt
diff --git a/src/Ivory/Compile/C/CmdlineFrontend/Options.hs b/src/Ivory/Compile/C/CmdlineFrontend/Options.hs
--- a/src/Ivory/Compile/C/CmdlineFrontend/Options.hs
+++ b/src/Ivory/Compile/C/CmdlineFrontend/Options.hs
@@ -1,9 +1,8 @@
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE GADTs #-}
-
 module Ivory.Compile.C.CmdlineFrontend.Options where
 
-import Data.Monoid (Monoid(..),mconcat)
+import Prelude ()
+import Prelude.Compat
+
 import System.Console.GetOpt
     (ArgOrder(Permute),OptDescr(..),ArgDescr(..),getOpt,usageInfo)
 
@@ -12,23 +11,17 @@
 
 -- Option Parsing --------------------------------------------------------------
 
-data OptParser opt
-  = Success (opt -> opt)
-  | Error [String]
+data OptParser opt = OptParser [String] (opt -> opt)
 
 instance Monoid (OptParser opt) where
-  mempty                        = Success id
-
+  mempty = OptParser [] id
   -- left-to-right composition makes the last option parsed take precedence
-  Success f `mappend` Success g = Success (f . g)
-  Error as  `mappend` Error bs  = Error (as ++ bs)
-  Error as  `mappend` _         = Error as
-  _         `mappend` Error bs  = Error bs
+  OptParser as f `mappend` OptParser bs g = OptParser (as ++ bs) (f . g)
 
 -- | Option parser succeeded, use this function to transform the default
 -- options.
 success :: (opt -> opt) -> OptParser opt
-success  = Success
+success  = OptParser []
 
 -- | Option parser failed, emit this message.
 --
@@ -43,8 +36,8 @@
              -> (Either [String] (opt -> opt))
 parseOptions opts args = case getOpt Permute opts args of
   (fs,[],[]) -> case mconcat fs of
-    Success f -> Right f
-    Error es  -> Left es
+    OptParser [] f -> Right f
+    OptParser es _ -> Left es
   (_,_,es)  -> Left es
 
 
@@ -52,13 +45,13 @@
 -- Command Line Options --------------------------------------------------------
 
 data Opts = Opts
-  { stdOut      :: Bool
-  , includeDir  :: FilePath
-  , srcDir      :: FilePath
-  -- dependencies
-  , deps        :: FilePath
-  , depPrefix   :: String
-  , rtIncludeDir:: Maybe FilePath
+  { outDir      :: Maybe FilePath
+  -- ^ output directory for all files (or standard out).
+  , outHdrDir   :: Maybe FilePath
+  -- ^ if set, output directory for headers. Otherwise, use @outDir@.
+  , outArtDir   :: Maybe FilePath
+  -- ^ if set, output directory for artifacts. Otherwise, use @outDir@.
+
   -- optimization passes
   , constFold   :: Bool
   , overflow    :: Bool
@@ -66,34 +59,36 @@
   , ixCheck     :: Bool
   , fpCheck     :: Bool
   , outProcSyms :: Bool
+  , bitShiftCheck :: Bool
   -- CFG stuff
   , cfg         :: Bool
   , cfgDotDir   :: FilePath
   , cfgProc     :: [String]
   -- debugging
   , verbose     :: Bool
+  , srcLocs     :: Bool
+  -- Typechecking
+  , tcWarnings  :: Bool
+  , tcErrors    :: Bool
+  , scErrors    :: Bool
 
   , help        :: Bool
   } deriving (Show)
 
 initialOpts :: Opts
 initialOpts  = Opts
-  { stdOut       = False
-  , includeDir   = ""
-  , srcDir       = ""
-
-  -- dependencies
-  , deps         = ""
-  , depPrefix    = ""
-  , rtIncludeDir = Nothing
+  { outDir       = Nothing
+  , outHdrDir    = Nothing
+  , outArtDir    = Nothing
 
-  -- optimization passes
+  -- optimization/safety passes
   , constFold    = False
   , overflow     = False
   , divZero      = False
   , ixCheck      = False
   , fpCheck      = False
   , outProcSyms  = False
+  , bitShiftCheck = False
 
   -- CFG stuff
   , cfg          = False
@@ -101,27 +96,24 @@
   , cfgProc      = []
   -- debugging
   , verbose      = False
-
+  , srcLocs      = False
+  , tcWarnings   = False
+  , tcErrors     = True
+  , scErrors     = True
   , help         = False
   }
 
 setStdOut :: OptParser Opts
-setStdOut  = success (\opts -> opts { stdOut = True } )
-
-setIncludeDir :: String -> OptParser Opts
-setIncludeDir str = success (\opts -> opts { includeDir = str })
-
-setSrcDir :: String -> OptParser Opts
-setSrcDir str = success (\opts -> opts { srcDir = str })
+setStdOut  = success (\opts -> opts { outDir = Nothing } )
 
-setDeps :: String -> OptParser Opts
-setDeps str = success (\opts -> opts { deps = str })
+setOutDir :: String -> OptParser Opts
+setOutDir str = success (\opts -> opts { outDir = Just str })
 
-setDepPrefix :: String -> OptParser Opts
-setDepPrefix str = success (\opts -> opts { depPrefix = str })
+setHdrDir :: String -> OptParser Opts
+setHdrDir str = success (\opts -> opts { outHdrDir = Just str })
 
-setRtIncludeDir :: String -> OptParser Opts
-setRtIncludeDir str = success (\opts -> opts { rtIncludeDir = Just str })
+setArtDir :: String -> OptParser Opts
+setArtDir str = success (\opts -> opts { outArtDir = Just str })
 
 setConstFold :: OptParser Opts
 setConstFold  = success (\opts -> opts { constFold = True })
@@ -141,6 +133,9 @@
 setProcSyms :: OptParser Opts
 setProcSyms  = success (\opts -> opts { outProcSyms = True })
 
+setBitShiftCheck :: OptParser Opts
+setBitShiftCheck  = success (\opts -> opts { bitShiftCheck = True })
+
 setCfg :: OptParser Opts
 setCfg  = success (\opts -> opts { cfg = True })
 
@@ -153,6 +148,18 @@
 setVerbose :: OptParser Opts
 setVerbose  = success (\opts -> opts { verbose = True })
 
+setSrcLocs :: OptParser Opts
+setSrcLocs  = success (\opts -> opts { srcLocs = True })
+
+setWarnings :: OptParser Opts
+setWarnings = success (\opts -> opts { tcWarnings = True })
+
+setErrors :: Bool -> OptParser Opts
+setErrors b = success (\opts -> opts { tcErrors = b })
+
+setSanityCheck :: Bool -> OptParser Opts
+setSanityCheck b = success (\opts -> opts { scErrors = b })
+
 setHelp :: OptParser Opts
 setHelp  = success (\opts -> opts { help = True })
 
@@ -160,17 +167,9 @@
 options  =
   [ Option "" ["std-out"] (NoArg setStdOut)
     "print to stdout only"
-  , Option "" ["include-dir"] (ReqArg setIncludeDir "PATH")
-    "output directory for header files"
-  , Option "" ["src-dir"] (ReqArg setSrcDir "PATH")
-    "output directory for source files"
 
-  , Option "" ["dep-file"] (ReqArg setDeps "FILE")
-    "makefile dependency output"
-  , Option "" ["dep-prefix"] (ReqArg setDepPrefix "STRING")
-    "makefile dependency prefix"
-  , Option "" ["rt-include-dir"] (ReqArg setRtIncludeDir "PATH")
-    "path to ivory runtime includes"
+  , Option "" ["src-dir"] (ReqArg setOutDir "PATH")
+    "output directory for source files"
 
   , Option "" ["const-fold"] (NoArg setConstFold)
     "enable the constant folding pass"
@@ -182,6 +181,8 @@
     "generate assertions checking for back indexes (e.g., negative)"
   , Option "" ["fp-check"] (NoArg setFpCheck)
     "generate assertions checking for NaN and Infinitiy."
+  , Option "" ["bitshift-check"] (NoArg setBitShiftCheck)
+    "generate assertions checking for bit-shift overflow."
 
   , Option "" ["out-proc-syms"] (NoArg setProcSyms)
     "dump out the modules' function symbols"
@@ -196,6 +197,24 @@
 
   , Option "" ["verbose"] (NoArg setVerbose)
     "verbose debugging output"
+
+  , Option "" ["srclocs"] (NoArg setSrcLocs)
+    "output source locations from the Ivory code"
+
+  , Option "" ["tc-warnings"] (NoArg setWarnings)
+    "show type-check warnings"
+
+  , Option "" ["tc-errors"] (NoArg $ setErrors True)
+    "Abort on type-check errors (default)"
+
+  , Option "" ["no-tc-errors"] (NoArg $ setErrors False)
+    "Treat type-check errors as warnings"
+
+  , Option "" ["sanity-check"] (NoArg $ setSanityCheck True)
+    "Enable sanity-check"
+
+  , Option "" ["no-sanity-check"] (NoArg $ setSanityCheck False)
+    "Disable sanity-check"
 
   , Option "h" ["help"] (NoArg setHelp)
     "display this message"
diff --git a/src/Ivory/Compile/C/Gen.hs b/src/Ivory/Compile/C/Gen.hs
--- a/src/Ivory/Compile/C/Gen.hs
+++ b/src/Ivory/Compile/C/Gen.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE PackageImports #-}
 {-# LANGUAGE QuasiQuotes #-}
-{-# LANGUAGE CPP#-}
+{-# LANGUAGE CPP #-}
 
 -- | Ivory backend targeting language-c-quote.
 
@@ -9,14 +9,15 @@
 import qualified "language-c-quote" Language.C.Syntax as C
 import Language.C.Quote.GCC
 
+import qualified Ivory.Language.Array  as I
 import qualified Ivory.Language.Syntax as I
+import Ivory.Language.Syntax.Concrete.Pretty
 import qualified Ivory.Language.Proc as P
 
 import Ivory.Compile.C.Types
 import Ivory.Compile.C.Prop
 
 import Prelude hiding (exp, abs, signum)
-import qualified Prelude as P
 import Data.List (foldl')
 
 import Data.Loc (noLoc)
@@ -27,34 +28,20 @@
 -- | Compile a top-level element.
 compile :: P.Def a -> Compile
 compile (P.DefProc fun) = compileUnit fun
-compile (P.DefExtern e) = compileExtern e
 compile (P.DefImport _) = error "Can't compile an import!"
 
 --------------------------------------------------------------------------------
--- | Compile an extern declaration
-compileExtern :: I.Extern -> Compile
-compileExtern I.Extern
-  { I.externSym     = sym
-  , I.externRetType = ret
-  , I.externArgs    = args
-  }
-  = putExt [cedecl| extern $ty:(toType ret) $id:(sym)
-                      ($params:(map mkParam args)) ; |]
-  where
-  mkParam ty = [cparam| $ty:(toType ty) |]
-
---------------------------------------------------------------------------------
 -- | Compile a struct.
 compileStruct :: Visibility -> I.Struct -> Compile
 compileStruct visibility def = case def of
-  I.Struct n fs    ->
-    (if visibility == Public then putHdrSrc else putSrc)
-    [cedecl| struct $id:n { $sdecls:(map mkFieldGroup fs)
-                          } __attribute__ ((__packed__)) ;
-           |]
-  I.Abstract _ file ->
-    putHdrInc (SysInclude file)
+  I.Struct n fs
+    -> (if visibility == Public then putHdrSrc else putSrc)
+         [cedecl| typedef struct $id:n { $sdecls:(map mkFieldGroup fs) } $id:n ;
+                |]
 
+  I.Abstract _ file
+    -> putHdrInc (SysInclude file)
+
 mkFieldGroup :: I.Typed String -> C.FieldGroup
 mkFieldGroup field =
   [csdecl| $ty:(toType (I.tType field)) $id:(I.tValue field) ; |]
@@ -62,7 +49,7 @@
 --------------------------------------------------------------------------------
 -- | Compile an external memory area reference.
 compileAreaImport :: I.AreaImport -> Compile
-compileAreaImport ai = putSrcInc (SysInclude (I.aiFile ai))
+compileAreaImport ai = putHdrInc (SysInclude (I.aiFile ai))
 
 --------------------------------------------------------------------------------
 -- | Get prototypes for memory areas.
@@ -102,13 +89,20 @@
                    , I.procEnsures  = ensures
                    }
   = do let ens  = map I.getEnsure ensures
-       let bd   = concatMap (toBody ens) body
+       let bd   = foldr collapseComment [] $ concatMap (toBody ens) body
        let reqs = map (toRequire . I.getRequire) requires
        putSrc [cedecl| $ty:(toType ret) ($id:sym) ($params:(toArgs args))
                          { $items:reqs
                            $items:bd
                          } |]
 
+collapseComment :: C.BlockItem -> [C.BlockItem] -> [C.BlockItem]
+collapseComment (C.BlockStm (C.Comment c (C.Exp Nothing _) src))
+                (C.BlockStm stm : items)
+  = C.BlockStm (C.Comment c stm src) : items
+collapseComment stm items
+  = stm : items
+
 --------------------------------------------------------------------------------
 -- | Get the prototypes.
 extractProto :: Visibility -> I.Proc -> Compile
@@ -126,7 +120,8 @@
 
 -- | Argument conversion.
 toArgs :: [I.Typed I.Var] -> [C.Param]
-toArgs = foldl' go [] . reverse
+toArgs [] = [[cparam| void |]]
+toArgs ls = foldl' go [] (reverse ls)
   where
   go acc I.Typed { I.tType  = t
                  , I.tValue = v }
@@ -137,24 +132,35 @@
   C.Type spec decl loc -> C.Param Nothing spec decl loc
   _                    -> error "toParam: unexpected anti-quote"
 
--- | Type conversion outside of an assignment context.  This converts arrays to
+--------------------------------------------------------------------------------
+-- Types
+
+-- | Type conversion outside of an casting context. This converts arrays to
 -- arrays, and carrays to pointers.
 toType :: I.Type -> C.Type
-toType  = toTypeCxt $ \ t -> case t of
-  I.TyCArray t'  -> [cty| $ty:(toType t') *          |]
-  I.TyArr len t' -> [cty| $ty:(toType t')[$uint:len] |]
-  _              -> [cty| $ty:(toType t) *           |]
-
+toType = toTypeCxt arrIxTy
+  where
+  -- Invariant: ty is wrapped in a Ref, ConstRef, or Ptr.
+  arrIxTy t = case t of
+    I.TyArr    len t'
+      -> [cty| $ty:(toTypeCxt arrIxTy t')[$uint:len] |]
+    I.TyCArray t'
+      -> [cty| $ty:(toTypeCxt arrIxTy t') *          |]
+    _ -> [cty| $ty:(toTypeCxt arrIxTy t ) *          |]
 
--- | Type conversion in the context of an assignment.
--- This converts all arrays/carrays to pointers.
-toTypeAssign :: I.Type -> C.Type
-toTypeAssign  = toTypeCxt $ \ t -> case t of
-  I.TyCArray t'  -> [cty| $ty:(toTypeAssign t') * |]
-  I.TyArr _   t' -> [cty| $ty:(toTypeAssign t') * |]
-  _              -> [cty| $ty:(toTypeAssign t)  * |]
+-- | Type conversion in the context of a cast, converting all arrays/carrays to
+-- pointers.
+toTypeCast :: I.Type -> C.Type
+toTypeCast = toTypeCxt arrIxTy
+  where
+  -- Invariant: ty is wrapped in a Ref, ConstRef, or Ptr.
+  arrIxTy t = case t of
+   I.TyArr    _len t'
+     -> [cty| $ty:(toTypeCxt arrIxTy t') * |]
+   I.TyCArray t'
+     -> [cty| $ty:(toTypeCxt arrIxTy t') * |]
+   _ -> [cty| $ty:(toTypeCxt arrIxTy t ) * |]
 
---------------------------------------------------------------------------------
 -- | C type conversion, with a special case for references and pointers.
 toTypeCxt :: (I.Type -> C.Type) -> I.Type -> C.Type
 toTypeCxt arrCase = convert
@@ -164,16 +170,16 @@
     I.TyChar              -> [cty| char |]
     I.TyInt i             -> intSize i
     I.TyWord w            -> wordSize w
+    I.TyIndex _           -> convert I.ixRep
     I.TyBool              -> [cty| typename bool |]
     I.TyFloat             -> [cty| float |]
     I.TyDouble            -> [cty| double |]
     I.TyStruct nm         -> [cty| struct $id:nm |]
     I.TyConstRef t        -> [cty| const $ty:(arrCase t) |]
-    -- Reference is a guaranted non-NULL pointer.
     I.TyRef t             -> arrCase t
     I.TyPtr t             -> arrCase t
-    I.TyArr len t         -> [cty| $ty:(convert t)[$uint:len] |]
     I.TyCArray t          -> [cty| $ty:(convert t) * |]
+    I.TyArr len t         -> [cty| $ty:(convert t)[$uint:len] |]
     I.TyProc retTy argTys ->
       [cty| $ty:(convert retTy) (*)
             ($params:(map (toParam . convert) argTys)) |]
@@ -212,8 +218,9 @@
 toBody ens stmt =
   let toBody' = toBody ens in
   case stmt of
+    -- t is the ref type.
     I.Assign t v exp       ->
-      [C.BlockDecl [cdecl| $ty:(toTypeAssign t) $id:(toVar v)
+      [C.BlockDecl [cdecl| $ty:(toTypeCast t) $id:(toVar v)
                          = $exp:(toExpr t exp); |]]
     I.IfTE exp blk0 blk1   ->
       let ifBd   = concatMap toBody' blk0 in
@@ -234,27 +241,21 @@
     -- optimize away *& constructions on dereferncing structs and indexes into
     -- arrays.
     I.Deref t var exp      -> [C.BlockDecl
-      [cdecl| $ty:(toType t) $id:(toVar var) = $exp:deref; |]]
-      where
-      deref = case t of
-                I.TyArr _ _  -> [cexp| * $exp:e |]
-                I.TyCArray _ -> [cexp| * $exp:e |]
-                _            -> [cexp|   $exp:e |]
-      e = case exp of
-            I.ExpLabel t' e' field ->
-              [cexp| $exp:(toExpr (I.TyRef t') e') -> $id:field |]
-            I.ExpIndex t' e' ti i  ->
-              [cexp| $exp:(toExpr (I.TyRef t') e') [$exp:(toExpr ti i)] |]
-            _                      -> [cexp| * $exp:(toExpr (I.TyRef t) exp) |]
+      [cdecl| $ty:(toType t) $id:(toVar var) = $exp:(derefExp (toExpr (I.TyRef t) exp)); |]]
 
     I.Local t var inits    -> [C.BlockDecl
-      [cdecl| $ty:(toType t) $id:(toVar var) = $init:(toInit inits); |]]
+      [cdecl| $ty:(toType t) $id:(toVar var)
+                = $init:(toInit inits); |]]
     -- Can't do a static check since we have local let bindings.
     I.RefCopy t vto vfrom  ->
-      [C.BlockStm [cstm| if( $exp:toRef != $exp:fromRef) {
-         memcpy( $exp:toRef, $exp:fromRef, sizeof($ty:(toType t)) ); }
-                           else { COMPILER_ASSERTS(false); }
-      |]]
+      [C.BlockStm $ case t of
+        I.TyArr{} ->
+          [cstm| if( $exp:toRef != $exp:fromRef) {
+             memcpy( $exp:toRef, $exp:fromRef, sizeof($ty:(toType t)) ); }
+                               else { COMPILER_ASSERTS(false); }
+          |]
+        _ -> [cstm| $exp:(derefExp toRef) = $exp:(derefExp fromRef); |]
+      ]
       where
       toRef   = toExpr (I.TyRef t) vto
       fromRef = toExpr (I.TyRef t) vfrom
@@ -287,7 +288,7 @@
                    , I.tValue = v }
           = toExpr t' v
     -- Assume that ty is a signed and sufficiently big (int).
-    I.Loop var start incr blk ->
+    I.Loop _ var start incr blk ->
       let loopBd =  concatMap toBody' blk in
       [C.BlockStm [cstm| for( $ty:(toType ty) $id:(toVar var)
                                 = $exp:(toExpr ty start);
@@ -295,7 +296,7 @@
                               $exp:incExp ) {
                        $items:loopBd } |]]
       where
-      ty = I.TyInt I.Int32
+      ty = I.ixRep
       (test,incExp)  = toIncr incr
       ix = toVar var
       toIncr (I.IncrTo to) =
@@ -317,8 +318,12 @@
 
     I.Break                       -> [C.BlockStm [cstm| break; |]]
     I.Store t ptr exp             -> [C.BlockStm
-      [cstm| * $exp:(toExpr (I.TyRef t) ptr) = $exp:(toExpr t exp); |]]
+      [cstm| $exp:(derefExp (toExpr (I.TyRef t) ptr)) = $exp:(toExpr t exp); |]]
 
+    I.Comment (I.UserComment c)   -> [C.BlockStm
+      [cstm| $comment:("/* " ++ c ++ " */"); |]]
+    I.Comment (I.SourcePos src)   -> [C.BlockStm
+      [cstm| $comment:("/* " ++ prettyPrint (pretty src) ++ " */"); |]]
 -- | Return statement.
 typedRet :: I.Typed I.Expr -> C.Exp
 typedRet I.Typed { I.tType  = t
@@ -340,6 +345,14 @@
 
 --------------------------------------------------------------------------------
 
+derefExp :: C.Exp -> C.Exp
+derefExp (C.UnOp C.AddrOf rhs _) = rhs
+derefExp e = [cexp| * $exp:e |]
+
+labelExp :: C.Exp -> String -> C.Exp
+labelExp (C.UnOp C.AddrOf lhs _) field = [cexp| $exp:lhs . $id:field |]
+labelExp lhs field = [cexp| $exp:lhs -> $id:field |]
+
 -- | Translate an expression.
 toExpr :: I.Type -> I.Expr -> C.Exp
 ----------------------------------------
@@ -348,10 +361,11 @@
 toExpr t (I.ExpLit lit)  =
   case lit of
     -- XXX hack: should make type-correct literals.
-    I.LitInteger i -> [cexp| ($ty:(toType t))$id:fromInt |]
+    I.LitInteger i -> [cexp| ($ty:(toTypeCast t))$id:fromInt |]
       where fromInt = case t of
                         I.TyWord _  -> show i ++ "U"
                         I.TyInt  _  -> show i
+                        I.TyIndex _ -> show i
                         I.TyFloat   -> show (fromIntegral i :: Float) ++ "F"
                         I.TyDouble  -> show (fromIntegral i :: Double)
                         _           -> error ("Nonint type " ++ (show t) ++
@@ -363,18 +377,21 @@
     I.LitFloat f   -> [cexp| $id:(show f ++ "f") |]
     I.LitDouble d  -> [cexp| $id:(show d) |]
 ----------------------------------------
-toExpr t (I.ExpOp op args) = [cexp| ($ty:(toType t)) $exp:(toExpOp t op args) |]
+toExpr t (I.ExpOp op args) =
+  [cexp| ($ty:(toTypeCast t)) $exp:(toExpOp t op args) |]
 ----------------------------------------
 toExpr _ (I.ExpSym sym) = [cexp| $id:sym |]
 ----------------------------------------
+toExpr _ (I.ExpExtern (I.Extern sym _ _)) = [cexp| $id:sym |]
+----------------------------------------
 toExpr t (I.ExpLabel t' e field) = case t of
   I.TyRef (I.TyArr _ _)       -> getField
   I.TyRef (I.TyCArray _)      -> getField
   I.TyConstRef (I.TyArr _ _)  -> getField
   I.TyConstRef (I.TyCArray _) -> getField
   _                           ->
-    [cexp| &($exp:(toExpr (I.TyRef t') e) -> $id:field) |]
-  where getField = [cexp| ($exp:(toExpr  t' e) -> $id:field) |]
+    [cexp| &($exp:(labelExp (toExpr (I.TyRef t') e) field)) |]
+  where getField = labelExp (toExpr t' e) field
 ----------------------------------------
 toExpr t (I.ExpIndex at a ti i) = case t of
   I.TyRef (I.TyArr _ _)       -> expIdx I.TyRef
@@ -388,10 +405,10 @@
     [cexp| ($exp:(toExpr (constr at) a) [$exp:(toExpr ti i)]) |]
 ----------------------------------------
 toExpr tTo (I.ExpSafeCast tFrom e) =
-  [cexp| ($ty:(toType tTo))$exp:(toExpr tFrom e) |]
+  [cexp| ($ty:(toTypeCast tTo))$exp:(toExpr tFrom e) |]
 ----------------------------------------
-toExpr tTo (I.ExpToIx e maxSz) =
-  [cexp| $exp:(toExpr tTo e ) % $exp:maxSz |]
+toExpr _ (I.ExpToIx e maxSz) =
+  [cexp| $exp:(toExpr I.ixRep e ) % $exp:maxSz |]
 ----------------------------------------
 toExpr tTo (I.ExpAddrOfGlobal sym) = case tTo of
   I.TyRef (I.TyArr _ _)       -> [cexp| $id:sym |]
@@ -414,6 +431,7 @@
         I.Word16    -> "UINT16_MAX"
         I.Word32    -> "UINT32_MAX"
         I.Word64    -> "UINT64_MAX"
+      I.TyIndex n -> show n
       _           -> err
     False -> case ty of
       I.TyInt sz -> case sz of
@@ -421,10 +439,17 @@
         I.Int16    -> "INT16_MIN"
         I.Int32    -> "INT32_MIN"
         I.Int64    -> "INT64_MIN"
-      _          -> err
+      I.TyWord sz -> show $ case sz of
+        I.Word8     -> 0 :: Integer
+        I.Word16    -> 0
+        I.Word32    -> 0
+        I.Word64    -> 0
+      I.TyIndex _ -> "0"
+      _           -> err
   err = error $ "unexpected type " ++ show ty ++ " in ExpMaxMin."
 ----------------------------------------
-
+toExpr ty (I.ExpSizeOf ty') = [cexp| ($ty:(toTypeCast ty)) sizeof($ty:(toType ty')) |]
+----------------------------------------
 
 exp0 :: [C.Exp] -> C.Exp
 exp0 = flip (!!) 0
@@ -500,6 +525,7 @@
   I.ExpFAsin      -> floatingUnary ty "asin"  args
   I.ExpFAcos      -> floatingUnary ty "acos"  args
   I.ExpFAtan      -> floatingUnary ty "atan"  args
+  I.ExpFAtan2     -> floatingBinary ty "atan2" args
   I.ExpFSinh      -> floatingUnary ty "sinh"  args
   I.ExpFCosh      -> floatingUnary ty "cosh"  args
   I.ExpFTanh      -> floatingUnary ty "tanh"  args
@@ -510,19 +536,13 @@
   -- float operations
   -- XXX this needs to add a dependency on <math.h>
   I.ExpIsNan ety -> let xs = mkArgs ety args in
-                    [cexp| ($ty:(toType I.TyBool)) (isnan($exp:(exp0 xs))) |]
+                    [cexp| ($ty:(toTypeCast I.TyBool)) (isnan($exp:(exp0 xs))) |]
   -- isinf returns -1 for negative infinity and 1 for positive infinity.
   I.ExpIsInf ety -> let xs = mkArgs ety args in
-                    [cexp| ($ty:(toType I.TyBool)) (isinf($exp:(exp0 xs))) |]
-  I.ExpRoundF    -> floatingBinary ty "round" args
-  I.ExpCeilF     -> floatingBinary ty "ceil" args
-  I.ExpFloorF    -> floatingBinary ty "floor" args
-
-  -- float casting
-  I.ExpToFloat ety   -> let xs = mkArgs ety args in
-                        [cexp| ($ty:(toType ty))($exp:(exp0 xs)) |]
-  I.ExpFromFloat ety ->
-    [cexp| ($ty:(toType ty))($exp:(floatingUnary ety "trunc" args)) |]
+                    [cexp| ($ty:(toTypeCast I.TyBool)) (isinf($exp:(exp0 xs))) |]
+  I.ExpRoundF    -> floatingUnary ty "round" args
+  I.ExpCeilF     -> floatingUnary ty "ceil"  args
+  I.ExpFloorF    -> floatingUnary ty "floor" args
 
   -- bit operations
   I.ExpBitAnd        -> let xs = mkArgs ty args in
@@ -594,7 +614,7 @@
   I.TyFloat  -> "signum_float"
   I.TyDouble -> "signum_double"
   I.TyInt i  -> "signum_i" ++ showInt i
-  I.TyWord w -> "signum_w" ++ showWord w
+  I.TyWord w -> "signum_u" ++ showWord w
   I.TyChar   -> "signum_char"
   _          -> error ("signum " ++ "unimplemented for type " ++ show ty)
 ----------------------------------------
diff --git a/src/Ivory/Compile/C/Modules.hs b/src/Ivory/Compile/C/Modules.hs
--- a/src/Ivory/Compile/C/Modules.hs
+++ b/src/Ivory/Compile/C/Modules.hs
@@ -1,10 +1,13 @@
 {-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE CPP #-}
 
 module Ivory.Compile.C.Modules where
 
 import Paths_ivory_backend_c (version)
 
-import qualified Text.PrettyPrint.Mainland as PP
+import Prelude ()
+import Prelude.Compat
+
 import Text.PrettyPrint.Mainland
 
 import qualified Ivory.Language.Syntax.AST as I
@@ -14,24 +17,23 @@
 
 import Data.Char (toUpper)
 import Data.Version (showVersion)
-import Control.Applicative ((<$>))
 import qualified Data.Set as S
-import Control.Monad
+import Control.Monad (unless)
 import System.FilePath.Posix ((<.>)) -- Always use posix convention in C code
 import MonadLib (put,runM)
 
 --------------------------------------------------------------------------------
 
-showModule :: CompileUnits -> [[String]]
-showModule m =
-  [ mk "// Sources:\n" (sources m)
-  , mk "// Header:\n"  (headers m)
-  , mk "// Externs:\n" (S.empty, externs m)
+showModule :: CompileUnits -> String
+showModule m = unlines $ map unlines $
+  [ mk (lbl "Source") (sources m)
+  , mk (lbl "Header") (headers m)
   ]
   where
+  lbl l = "// module " ++ unitName m ++ " " ++ l ++ ":\n"
   mk _   (_,[])         = []
   mk str (incls,units)  = str : pp (map includeDef (S.toList incls) ++ units)
-  pp = map (show . ppr)
+  pp = map (pretty maxWidth . ppr)
 
 --------------------------------------------------------------------------------
 
@@ -44,19 +46,9 @@
                text " * Compiler version " <+> text compilerVersion </>
                text " */"
 
--- | Output header file for a module.
-writeHdr :: Bool                -- ^ Verbosity
-         -> FilePath            -- ^ Output file name
-         -> (Includes, Sources) -- ^ Source to translate
-         -> String              -- ^ Unit name
-         -> IO ()
-writeHdr True  f s unitname = toFile f $ renderHdr s unitname
-writeHdr False f s unitname = toFileQuiet f $ renderHdr s unitname
-
 renderHdr :: (Includes, Sources) -> String -> String
-renderHdr s unitname = PP.displayS (PP.render width guardedHeader) ""
+renderHdr s unitname = displayS (render maxWidth guardedHeader) ""
   where
-  width = 80
   guardedHeader = stack [ topComments
                         , topGuard
                         , topExternC
@@ -64,7 +56,7 @@
                         , botExternC
                         , botGuard
                         ]
-  topGuard        = text "#ifndef" <+> guardName PP.</> text "#define"
+  topGuard        = text "#ifndef" <+> guardName </> text "#define"
                       <+> guardName
   botGuard        = text "#endif" <+> text "/*" <+> guardName <+> text "*/"
   unitname'       = map (\c -> if c == '-' then '_' else c) unitname
@@ -77,34 +69,13 @@
                                      , "#endif"]
   defs (incls,us) = map includeDef (S.toList incls) ++ us
 
-
--- | Output source file for a module.
-writeSrc :: Bool                 -- ^ Be verbose
-         -> FilePath             -- ^ Output source name
-         -> (Includes, Sources)  -- ^ Module to translate
-         -> IO ()
-writeSrc verbose f s = vToFile f (renderSrc s)
-  where
-  vToFile = if verbose then toFile else toFileQuiet
-
 renderSrc :: (Includes, Sources) -> String
-renderSrc s = PP.displayS (PP.render width srcdoc) ""
+renderSrc s = displayS (render maxWidth srcdoc) ""
   where
-  width = 80
   srcdoc = topComments </> out
   defs (incls,us) = map includeDef (S.toList incls) ++ us
   out = stack $ punctuate line $ map ppr $ defs s
 
--- Utility
-toFileQuiet :: FilePath -> String -> IO ()
-toFileQuiet f v = writeFile f v
-
-toFile :: FilePath -> String -> IO ()
-toFile f v = do
-  putStr $ "Writing to file " ++ f ++ "..."
-  toFileQuiet f v
-  putStrLn " Done."
-
 --------------------------------------------------------------------------------
 
 runOpt :: (I.Proc -> I.Proc) -> I.Module -> I.Module
@@ -122,8 +93,8 @@
 compileModule I.Module { I.modName        = nm
                        , I.modDepends     = deps
                        , I.modHeaders     = hdrs
-                       , I.modExterns     = exts
                        , I.modImports     = imports
+                       , I.modExterns     = externs
                        , I.modProcs       = procs
                        , I.modStructs     = structs
                        , I.modAreas       = areas
@@ -133,7 +104,6 @@
   { unitName = nm
   , sources  = sources res
   , headers  = headers res
-  , externs  = externs res
   }
   where
   res     = compRes comp
@@ -151,11 +121,11 @@
     putHdrInc (LocalInclude "ivory.h")
     -- module names don't have a .h on the end
     mapM_ (putHdrInc . LocalInclude . ((<.> "h"))) (S.toList deps)
-    mapM_ (putHdrInc . SysInclude)   (S.toList hdrs)
+    mapM_ (putHdrInc . LocalInclude) (S.toList hdrs)
     mapM_ (compileStruct Public) (I.public structs)
     mapM_ (compileStruct Private) (I.private structs)
-    mapM_ compileExtern exts
     mapM_ fromImport imports
+    mapM_ fromExtern externs
     mapM_ (extractAreaProto Public) (I.public areas)
     mapM_ (extractAreaProto Private) (I.private areas)
     mapM_ (compileArea Public) (I.public areas)
@@ -168,10 +138,15 @@
 --------------------------------------------------------------------------------
 
 fromImport :: I.Import -> Compile
-fromImport p = putSrcInc (SysInclude (I.importFile p))
+fromImport p = putHdrInc (SysInclude (I.importFile p))
 
 --------------------------------------------------------------------------------
 
+fromExtern :: I.Extern -> Compile
+fromExtern p = putHdrInc (SysInclude (I.externFile p))
+
+--------------------------------------------------------------------------------
+
 outputProcSyms :: [I.Module] -> IO ()
 outputProcSyms mods = putStrLn $ unwords $ concatMap go mods
   where
@@ -180,3 +155,10 @@
     where I.Visible pub priv = I.modProcs m
 
 --------------------------------------------------------------------------------
+
+-- This is generated code, and sometimes, we have large expressions. In
+-- practice, this means that once the width is reached, one token is placed per
+-- line(!). So we'll make a high limit for width, somewhat ironically making
+-- generated C more readable.
+maxWidth :: Int
+maxWidth = 400
diff --git a/src/Ivory/Compile/C/Prop.hs b/src/Ivory/Compile/C/Prop.hs
--- a/src/Ivory/Compile/C/Prop.hs
+++ b/src/Ivory/Compile/C/Prop.hs
@@ -12,6 +12,7 @@
   where
   loop e = case e of
     I.ExpSym{}             -> e
+    I.ExpExtern{}          -> e
     I.ExpVar v             -> if v == I.retval then retE else e
     I.ExpLit{}             -> e
     I.ExpOp op args        -> I.ExpOp op (map loop args)
@@ -21,5 +22,6 @@
     I.ExpToIx e0 maxSz     -> I.ExpToIx (loop e0) maxSz
     I.ExpAddrOfGlobal{}    -> e
     I.ExpMaxMin{}          -> e
+    I.ExpSizeOf{}          -> e
 
 --------------------------------------------------------------------------------
diff --git a/src/Ivory/Compile/C/SourceDeps.hs b/src/Ivory/Compile/C/SourceDeps.hs
deleted file mode 100644
--- a/src/Ivory/Compile/C/SourceDeps.hs
+++ /dev/null
@@ -1,45 +0,0 @@
-
-module Ivory.Compile.C.SourceDeps where
-
-import Control.Monad
-import System.FilePath
-import System.Directory
-
-import Data.Either
-import qualified Data.Set as Set
-
-import Ivory.Language
-import qualified Ivory.Language.Syntax.AST as AST
-
--- At some point we may want to restrict this to .c and .h files only
--- but for now we'll leave it alone.
-collectSourceDeps :: [Module] -> [FilePath]
-collectSourceDeps ms = Set.toList $ foldl aux Set.empty ms
-  where aux acc m = Set.union acc (AST.modSourceDeps m)
-
-outputSourceDeps :: FilePath -> FilePath -- Output dirs: include dir, source dir
-                 -> [FilePath]           -- SourceDeps: list if filenames to output
-                 -> [FilePath]           -- Search Path: list of directories
-                 -> IO ()                --  where SourceDeps may be
-outputSourceDeps inclDir srcDir srcDeps searchPath = do
-    validSearchPath <- filterM doesDirectoryExist searchPath
-    discovered <- mapM (findSource validSearchPath) srcDeps
-    mapM_ output (rights discovered)
-    case lefts discovered of
-      [] -> return ()
-      es -> error $ "failure to output source dependencies:\n" ++ (unlines es) ++
-                    "in search path:\n" ++ (unlines searchPath)
-  where
-  findSource :: [FilePath] -> FilePath -> IO (Either String FilePath)
-  findSource searchpath f = do
-    v <- filterM doesFileExist $ map (\p -> p </> f) searchpath
-    case v of
-      []   -> return $ Left ("not found: " ++ f)
-      a:_ -> return $ Right a
-  output :: FilePath -> IO ()
-  output fp = case takeExtension fp of
-    ".h" -> copyFile fp (inclDir </> (takeFileName fp))
-    _    -> copyFile fp (srcDir  </> (takeFileName fp))
-
-
-
diff --git a/src/Ivory/Compile/C/Types.hs b/src/Ivory/Compile/C/Types.hs
--- a/src/Ivory/Compile/C/Types.hs
+++ b/src/Ivory/Compile/C/Types.hs
@@ -4,11 +4,13 @@
 
 module Ivory.Compile.C.Types where
 
+import Prelude ()
+import Prelude.Compat
+
 import Language.C.Quote.GCC
 import qualified "language-c-quote" Language.C.Syntax as C
 
 import MonadLib (WriterT,Id,put)
-import Data.Monoid
 import qualified Data.Set as S
 
 --------------------------------------------------------------------------------
@@ -30,22 +32,20 @@
   { unitName :: String
   , sources  :: (Includes, Sources)
   , headers  :: (Includes, Sources)
-  , externs  :: Sources
   } deriving Show
 
 instance Monoid CompileUnits where
-  mempty = CompileUnits mempty mempty mempty mempty
-  (CompileUnits n0 s0 h0 e0) `mappend` (CompileUnits n1 s1 h1 e1) =
+  mempty = CompileUnits mempty mempty mempty
+  (CompileUnits n0 s0 h0) `mappend` (CompileUnits n1 s1 h1) =
     CompileUnits (n0 `mappend` n1)
                  (s0 `mappend` s1)
                  (h0 `mappend` h1)
-                 (e0 `mappend` e1)
 
 --------------------------------------------------------------------------------
 
 newtype CompileM a = Compile
   { unCompile :: WriterT CompileUnits Id a }
-  deriving (Functor, Monad)
+  deriving (Functor, Monad, Applicative)
 
 type Compile = CompileM ()
 
@@ -62,8 +62,5 @@
 
 putHdrInc :: Include -> Compile
 putHdrInc inc = Compile (put mempty { headers = (S.fromList [inc],[]) })
-
-putExt :: C.Definition -> Compile
-putExt ext = Compile (put mempty { externs = [ext] })
 
 --------------------------------------------------------------------------------