diff --git a/DDC/Driver/Command/Ast.hs b/DDC/Driver/Command/Ast.hs
deleted file mode 100644
--- a/DDC/Driver/Command/Ast.hs
+++ /dev/null
@@ -1,61 +0,0 @@
-
-module DDC.Driver.Command.Ast
-        ( cmdAstModule
-        , cmdAstExp)
-where
-import DDC.Driver.Command.Check
-import DDC.Interface.Source
-import DDC.Build.Language
-import Control.Monad.Trans.Error
-import qualified Language.Haskell.Exts.Parser as H
-import qualified Language.Haskell.Exts.Pretty as H
-
-
--- | Parse, check, and pretty print a module's internal representation.
-cmdAstModule :: Language -> Source -> String -> IO ()
-cmdAstModule language source str
- | Language bundle      <- language
- , fragment             <- bundleFragment bundle
- = do   mModule <- runErrorT 
-                $ cmdCheckModuleFromString fragment source str
-        goShow mModule
- where
-        -- Expression had a parse or type error.
-        goShow (Left err)
-         = do   putStrLn err
-                return ()
-
-        -- Expression is well-typed.
-        goShow (Right x)
-         = let p = pretty x in
-           putStrLn p
-         
-        pretty x
-         = case H.parseExp (show x) of
-                H.ParseOk parsed -> H.prettyPrint parsed
-                err -> show err
-
-
--- | Parse, check, and pretty print an expression's internal representation.
-cmdAstExp :: Language -> Source -> String -> IO ()
-cmdAstExp language source str
- | Language bundle      <- language
- , fragment             <- bundleFragment bundle
- , modules              <- bundleModules  bundle
- =   cmdParseCheckExp fragment modules True source str 
- >>= goShow
- where
-        -- Expression had a parse or type error.
-        goShow Nothing
-         = return ()
-
-        -- Expression is well-typed.
-        goShow (Just x)
-         = let p = pretty x in
-	   putStrLn p
-	 
-	pretty x
-	 = case H.parseExp (show x) of
-		H.ParseOk parsed -> H.prettyPrint parsed
-		err -> show err
-
diff --git a/DDC/Driver/Command/BaseBuild.hs b/DDC/Driver/Command/BaseBuild.hs
--- a/DDC/Driver/Command/BaseBuild.hs
+++ b/DDC/Driver/Command/BaseBuild.hs
@@ -37,7 +37,7 @@
 cmdBaseBuild config
  = do   let builder     = configBuilder config
         let target      = buildTarget builder
-
+        
         -- Ensure the lib dir exists.
         exists   <- liftIO $ doesDirectoryExist $ buildBaseLibDir builder
         when (not exists)
@@ -49,9 +49,10 @@
         mapM_ (cmdCompile config) srcLiteFiles
 
         -- Build all the .dcs files.
+        let config'      = config { configInferTypes = True }
         let srcSaltFiles = map (buildBaseSrcDir builder </>) (baseSaltFiles builder)
         let objSaltFiles = map (flip replaceExtension "o")   srcSaltFiles
-        mapM_ (cmdCompile config) srcSaltFiles
+        mapM_ (cmdCompile config') srcSaltFiles
 
         -- Build all the .c files.
         let srcSeaFiles  = map (buildBaseSrcDir builder </>) (baseSeaFiles builder)
diff --git a/DDC/Driver/Command/Check.hs b/DDC/Driver/Command/Check.hs
--- a/DDC/Driver/Command/Check.hs
+++ b/DDC/Driver/Command/Check.hs
@@ -1,22 +1,32 @@
 module DDC.Driver.Command.Check
-        ( cmdUniverse
-        , cmdUniverse1
-        , cmdUniverse2
-        , cmdUniverse3
-        , cmdShowKind
-        , cmdTypeEquiv
-        , cmdShowWType
+        ( -- * Checking modules. 
+          cmdCheckFromFile
+        , cmdCheckSourceTetraFromFile
+        , cmdCheckSourceTetraFromString
+        , cmdCheckCoreFromFile
+        , cmdCheckCoreFromString
+
+          -- * Checking types.
         , cmdShowType
-        , cmdExpRecon
-        , ShowTypeMode(..)
-        , cmdCheckModuleFromFile
-        , cmdCheckModuleFromString
+        , cmdTypeEquiv
         , cmdParseCheckType
-        , cmdParseCheckExp)
+
+          -- * Checking expressions.
+        , Mode(..)
+        , ShowSpecMode(..)
+        , cmdShowSpec
+        , cmdExpRecon
+        , cmdParseCheckExp
+
+          -- * Checking witnesses.
+        , cmdShowWType)
 where
+import DDC.Driver.Stage
 import DDC.Driver.Output
+import DDC.Driver.Config
 import DDC.Interface.Source
 import DDC.Build.Language
+import DDC.Build.Pipeline
 import DDC.Core.Fragment
 import DDC.Core.Load
 import DDC.Core.Parser
@@ -32,101 +42,165 @@
 import Control.Monad.IO.Class
 import qualified DDC.Base.Parser        as BP
 import qualified DDC.Type.Check         as T
+import qualified DDC.Core.Check         as C
 import Control.Monad
+import System.FilePath
+import System.Directory
 
 
--- universe -------------------------------------------------------------------
--- | Show the universe of some type.
-cmdUniverse :: Language -> Source -> String -> IO ()
-cmdUniverse language source str
- | Language bundle      <- language
- , fragment             <- bundleFragment bundle
- , profile              <- fragmentProfile fragment
- = do   result          <- cmdParseCheckType source fragment str
-        case result of
-         Just (t, _)
-          | Just u      <- universeOfType (profilePrimKinds profile) t
-          ->    outDocLn $ ppr u
+-- Module -----------------------------------------------------------------------------------------
+-- | Parse and type-check a core module from a file, 
+--   printing any errors to @stdout@.
+--
+--   This function handle fragments of Disciple Core, as well as Source Tetra
+--   modules. The language to use is determined by inspecting the file name
+--   extension.
+--
+cmdCheckFromFile
+        :: Config               -- ^ Driver config.
+        -> FilePath             -- ^ Module file path.
+        -> ErrorT String IO ()
 
-         _ ->   outDocLn $ text "no universe"
+cmdCheckFromFile config filePath
+ 
+ -- Check a Disciple Source Tetra module.
+ | ".dst"       <- takeExtension filePath
+ =      cmdCheckSourceTetraFromFile config filePath
 
+ -- Check a module in some fragment of Disciple Core.
+ | Just language <- languageOfExtension (takeExtension filePath)
+ =      cmdCheckCoreFromFile config language filePath
 
--- | Given the type of some thing (up one level)
---   show the universe of the thing.
-cmdUniverse1 :: Language -> Source -> String -> IO ()
-cmdUniverse1 language source str
- | Language bundle      <- language
- , fragment             <- bundleFragment bundle
- , profile              <- fragmentProfile fragment
- = do   result          <- cmdParseCheckType source fragment str
-        case result of
-         Just (t, _)
-          | Just u      <- universeFromType1 (profilePrimKinds profile) t
-          ->    outDocLn $ ppr u
+ -- Don't know how to check this file.
+ | otherwise
+ = let  ext     = takeExtension filePath
+   in   throwError $ "Cannot check '" ++ ext ++ "'files."
 
-         _ ->   outDocLn $ text "no universe"
 
+---------------------------------------------------------------------------------------------------
+-- | Check a Disciple Source Tetra module from a file.
+cmdCheckSourceTetraFromFile
+        :: Config               -- ^ Driver config.
+        -> FilePath             -- ^ Module file path.
+        -> ErrorT String IO ()
 
--- | Given the kind of some thing (up two levels)
---   show the universe of the thing.
-cmdUniverse2 :: Language -> Source -> String -> IO ()
-cmdUniverse2 language source str
+cmdCheckSourceTetraFromFile config filePath
+ = do
+        -- Check that the file exists.
+        exists <- liftIO $ doesFileExist filePath
+        when (not exists)
+         $ throwError $ "No such file " ++ show filePath
+
+        -- Read in the source file.
+        src     <- liftIO $ readFile filePath
+
+        cmdCheckSourceTetraFromString config (SourceFile filePath) src
+
+
+---------------------------------------------------------------------------------------------------
+-- | Check a Disciple Source Tetra module from a string.
+--   Any errors are thrown in the `ErrorT` monad.
+cmdCheckSourceTetraFromString
+        :: Config               -- ^ Driver config.
+        -> Source               -- ^ Source of the code.
+        -> String               -- ^ Program module text.
+        -> ErrorT String IO ()
+
+cmdCheckSourceTetraFromString config source str
+ = let
+        pmode   = prettyModeOfConfig $ configPretty config
+
+        pipeLoad
+         = pipeText     (nameOfSource source) (lineStartOfSource source) str
+         $ stageSourceTetraLoad config source
+         [ PipeCoreOutput pmode SinkDiscard ]
+   in do
+        errs    <- liftIO pipeLoad
+        case errs of
+         [] -> return ()
+         es -> throwError $ renderIndent $ vcat $ map ppr es
+ 
+
+---------------------------------------------------------------------------------------------------
+-- | Check some fragment of Disciple core from a file.
+cmdCheckCoreFromFile
+        :: Config               -- ^ Driver config.
+        -> Language             -- ^ Core language definition.
+        -> FilePath             -- ^ Module file path.
+        -> ErrorT String IO ()
+
+cmdCheckCoreFromFile config language filePath
  | Language bundle      <- language
  , fragment             <- bundleFragment bundle
- = do   result          <- cmdParseCheckType source fragment str
-        case result of
-         Just (t, _)
-          | Just u      <- universeFromType2 t
-          ->    outDocLn $ ppr u
+ = do
+        mModule <- liftIO 
+                $ loadModuleFromFile fragment filePath 
+                $ (if configInferTypes config then C.Synth else C.Recon)
+        
+        case mModule of
+                (Left  err, _ct) -> throwError (renderIndent $ ppr err)
+                (Right _,   _ct) -> return ()
 
-         _ ->   outDocLn $ text "no universe"
 
+-- | Parse and type-check a core module from a string.
+cmdCheckCoreFromString
+        :: (Ord n, Show n, Pretty n, Pretty (err (AnTEC BP.SourcePos n)))
+        => Fragment n err       -- ^ Language fragment.
+        -> Source               -- ^ Source of the program text.
+        -> String               -- ^ Program text.
+        -> C.Mode n             -- ^ Type checker mode.
+        -> ErrorT String IO (Module (AnTEC BP.SourcePos n) n)
 
--- | Given the sort of some thing (up three levels)
---   show the universe of the thing.
---   We can't type check naked sorts, so just parse them.
-cmdUniverse3 :: Language -> Source -> String -> IO ()
-cmdUniverse3 language source str
- | Language bundle      <- language
- , fragment             <- bundleFragment  bundle
- , profile              <- fragmentProfile fragment
- = let  srcName = nameOfSource source
-        srcLine = lineStartOfSource source
-        kenv    = profilePrimKinds profile
+cmdCheckCoreFromString fragment source str mode
+ = do   
+        let mModule = loadModuleFromString fragment
+                        (nameOfSource source) (lineStartOfSource source)
+                        mode str
 
-        -- Parse the tokens.
-        goParse toks                
-         = case BP.runTokenParser describeTok srcName 
-                        (pType (contextOfProfile profile))
-                        toks of
-            Left err    -> outDocLn $ ppr err
-            Right t     -> goUniverse3 (spreadT kenv t)
+        case mModule of
+                (Left err, _ct) -> throwError (renderIndent $ ppr err)
+                (Right mm, _ct) -> return mm
 
-        goUniverse3 tt
-         = case universeFromType3 tt of
-            Just u      -> outDocLn $ ppr u
-            Nothing     -> outDocLn $ text "no universe"
 
-   in   goParse (fragmentLexExp fragment srcName srcLine str)
+-- Type -------------------------------------------------------------------------------------------
+-- | Parse a core spec, and return its kind.
+cmdParseCheckType 
+        :: (Ord n, Show n, Pretty n, Pretty (err (AnTEC BP.SourcePos n)))
+        => Fragment n err       -- ^ Language fragment.
+        -> Universe             -- ^ Universe this type is supposed to be in.
+        -> Source               -- ^ Source of the program text.
+        -> String               -- ^ Program text.
+        -> IO (Maybe (Type n, Kind n))
 
+cmdParseCheckType fragment uni source str
+ = let  srcName = nameOfSource source
+        srcLine = lineStartOfSource source
+        toks    = fragmentLexExp fragment srcName srcLine str
+        eTK     = loadTypeFromTokens fragment uni srcName toks
+   in   case eTK of
+         Left err       
+          -> do outDocLn $ ppr err
+                return Nothing
 
--- kind ------------------------------------------------------------------------
--- | Show the kind of a type.
-cmdShowKind :: Language -> Source -> String -> IO ()
-cmdShowKind language source str
+         Right (t, k)
+          ->    return $ Just (t, k)
+
+
+-- | Show the type of a type in the given universe.
+cmdShowType :: Language -> Universe -> Source -> String -> IO ()
+cmdShowType language uni source str
  | Language bundle      <- language
  , fragment             <- bundleFragment  bundle
- , profile              <- fragmentProfile fragment
  = let  srcName = nameOfSource source
         srcLine = lineStartOfSource source
         toks    = fragmentLexExp fragment srcName srcLine str
-        eTK     = loadType profile srcName toks
+        eTK     = loadTypeFromTokens fragment uni srcName toks
    in   case eTK of
          Left err       -> outDocLn $ ppr err
          Right (t, k)   -> outDocLn $ ppr t <+> text "::" <+> ppr k
 
 
--- tequiv ---------------------------------------------------------------------
+-- tequiv -----------------------------------------------------------------------------------------
 -- | Check if two types are equivlant.
 cmdTypeEquiv :: Language -> Source -> String -> IO ()
 cmdTypeEquiv language source ss
@@ -157,7 +231,7 @@
         kenv    = profilePrimKinds    profile
 
         checkT t
-         = case T.checkType config kenv (spreadT kenv t) of
+         = case T.checkSpec config kenv (spreadT kenv t) of
                 Left err 
                  -> do  outDocLn $ ppr err
                         return False
@@ -168,221 +242,166 @@
    in goParse (fragmentLexExp fragment srcName srcLine ss)
 
 
--- wtype ----------------------------------------------------------------------
--- | Show the type of a witness.
-cmdShowWType :: Language -> Source -> String -> IO ()
-cmdShowWType language source str
- | Language bundle      <- language
- , fragment             <- bundleFragment  bundle
- , profile              <- fragmentProfile fragment
- = let  srcName = nameOfSource source
-        srcLine = lineStartOfSource source
-        toks    = fragmentLexExp fragment srcName srcLine str
-        eTK     = loadWitness profile srcName toks
-   in   case eTK of
-         Left err       -> outDocLn $ ppr err
-         Right (t, k)   -> outDocLn $ ppr t <+> text "::" <+> ppr k
+-- Exp --------------------------------------------------------------------------------------------
+-- | Parse the given core expression, 
+--   and return it, along with its type, effect and closure.
+--
+--   If the expression had a parse error, undefined vars, or type error
+--   then print this to the console.
+--
+--   We include a flag to override the language profile to allow partially
+--   applied primitives. Although a paticular evaluator (or backend) may not
+--   support partially applied primitives, we want to accept them if we are
+--   only loading an expression to check its type.
+--
+cmdParseCheckExp 
+        :: (Ord n, Show n, Pretty n, Pretty (err (AnTEC BP.SourcePos n)))
+        => Fragment n err       -- ^ The current language fragment.
+        -> ModuleMap (AnTEC () n) n -- ^ Current modules
+        -> Mode n               -- ^ Type checker mode.
+        -> Bool                 -- ^ Print type checker trace.
+        -> Bool                 -- ^ Allow partial application of primitives.
+        -> Source               -- ^ Where this expression was sourced from.
+        -> String               -- ^ Text to parse.
+        -> IO ( Maybe (Exp (AnTEC BP.SourcePos n) n)
+              , Maybe CheckTrace)
 
+cmdParseCheckExp 
+        fragment modules 
+        mode printTrace permitPartialPrims 
+        source str
+ = goLex
+ where
+        -- Override profile to allow partially applied primitives if we were
+        -- told to do so.
+        profile   = fragmentProfile fragment
+        features  = profileFeatures profile
+        features' = features { featuresPartialPrims 
+                             = featuresPartialPrims features || permitPartialPrims}
+        profile'  = profile  { profileFeatures  = features' }
+        fragment' = fragment     { fragmentProfile  = profile'  }
 
--- check / type / effect / closure --------------------------------------------
+        goLex 
+         = goLoad (fragmentLexExp fragment'
+                        (nameOfSource source) 
+                        (lineStartOfSource source) 
+                        str)
+
+        -- Parse and type check the expression.
+        goLoad toks
+         = case loadExpFromTokens fragment' modules 
+                        (nameOfSource source) mode toks of
+              (Left err, mct)
+               -> do    outDocLn $ ppr err
+                        
+                        case mct of
+                         Just ct 
+                          | printTrace  -> outDocLn $ ppr ct
+                         _              -> return ()
+                        
+                        return (Nothing, mct)
+
+              (Right result, mct)
+               -> return (Just result, mct)
+
+
+---------------------------------------------------------------------------------------------------
 -- | What components of the checked type to display.
-data ShowTypeMode
-        = ShowTypeAll
-        | ShowTypeValue
-        | ShowTypeEffect
-        | ShowTypeClosure
+data ShowSpecMode
+        = ShowSpecAll
+        | ShowSpecData
+        | ShowSpecEffect
+        | ShowSpecClosure
         deriving (Eq, Show)
 
 
--- | Show the type of an expression.
-cmdShowType :: Language -> ShowTypeMode -> Source -> String -> IO ()
-cmdShowType language mode source ss
+-- | Show the spec of an expression.
+cmdShowSpec
+        :: Language     -- ^ Language fragment.
+        -> ShowSpecMode -- ^ What part of the type to show.
+        -> Bool         -- ^ Type checker mode, Synth(True) or Recon(False)
+        -> Bool         -- ^ Whether to display type checker trace.
+        -> Source       -- ^ Source of the program text.
+        -> String       -- ^ Program text.
+        -> IO ()
+
+cmdShowSpec language showMode checkMode shouldPrintTrace source ss
  | Language bundle      <- language
  , fragment             <- bundleFragment  bundle
  , modules              <- bundleModules   bundle
- = cmdParseCheckExp fragment modules True source ss >>= goResult fragment
+ =   cmdParseCheckExp fragment modules mode shouldPrintTrace True source ss 
+ >>= goResult fragment
  where
-        goResult _ Nothing
-         = return ()
-
-        goResult fragment (Just x)
-         = let  -- This will always succeed because a well typed expression
-                -- is never a naked type or witness, and only those don't
-                -- have annotations.
-                Just annot      = takeAnnotOfExp x
+        -- Determine the checker mode based on the flag we're given.
+        -- We don't pass the mode directly because the Mode type is
+        -- also parameterised over the type of names.
+        mode    = case checkMode of
+                        True    -> Synth
+                        False   -> Recon
 
-                t               = annotType annot
-                eff             = annotEffect annot
-                clo             = annotClosure annot
+        goResult fragment (Just x, Just ct)
+         = let  annot    = annotOfExp x
+                t        = annotType annot
+                eff      = annotEffect annot
+                clo      = annotClosure annot
+                features = profileFeatures $ fragmentProfile fragment
 
-           in case mode of
-                ShowTypeAll
+           in case showMode of
+                ShowSpecAll
                  -> do  outDocLn $ ppr x
                         outDocLn $ text ":*:" <+> ppr t
                         
-                        let features    = profileFeatures $ fragmentProfile fragment
                         when (featuresTrackedEffects  features)
                          $ outDocLn $ text ":!:" <+> ppr eff
 
                         when (featuresTrackedClosures features)
                          $ outDocLn $ text ":$:" <+> ppr clo
-        
-                ShowTypeValue
+
+                        when shouldPrintTrace 
+                         $ do   outDocLn $ checkTraceDoc ct
+                                outDoc (text "\n")
+
+                ShowSpecData
                  ->     outDocLn $ ppr x <+> text "::" <+> ppr t
         
-                ShowTypeEffect
+                ShowSpecEffect
                  ->     outDocLn $ ppr x <+> text ":!:" <+> ppr eff
 
-                ShowTypeClosure
+                ShowSpecClosure
                  ->     outDocLn $ ppr x <+> text ":$:" <+> ppr clo
 
+        goResult _ _
+         = return ()
 
--- Recon ----------------------------------------------------------------------
+
+-- Recon ------------------------------------------------------------------------------------------
 -- | Check expression and reconstruct type annotations on binders.
 cmdExpRecon :: Language -> Source -> String -> IO ()
 cmdExpRecon language source ss
  | Language bundle      <- language
  , fragment             <- bundleFragment  bundle
  , modules              <- bundleModules   bundle
- =   cmdParseCheckExp fragment modules True source ss 
+ =   cmdParseCheckExp fragment modules Recon False True source ss 
  >>= goResult
  where
-        goResult Nothing
+        goResult (Nothing, _ct)
          = return ()
 
-        goResult (Just x)
+        goResult (Just x,  _ct)
          = outDocLn $ ppr x
 
 
--- Check ----------------------------------------------------------------------
--- | Parse and type-check a core module from a file.
-cmdCheckModuleFromFile
-        :: (Ord n, Show n, Pretty n, Pretty (err (AnTEC BP.SourcePos n)))
-        => Fragment n err
-        -> FilePath
-        -> ErrorT String IO (Module (AnTEC BP.SourcePos n) n)
-
-cmdCheckModuleFromFile fragment filePath
- = goLoad 
- where  lexModule =  fragmentLexModule fragment filePath 1
-
-        -- Load and type-check the module.
-        goLoad 
-         = do   mModule <- liftIO 
-                        $ loadModuleFromFile 
-                                (fragmentProfile fragment) lexModule filePath
-                case mModule of
-                 Left  err      -> throwError (renderIndent $ ppr err)
-                 Right mm       -> goCheckFragment mm
-
-        -- Do fragment specific checks.
-        goCheckFragment mm
-         = case fragmentCheckModule fragment mm of
-                Just err        -> throwError (renderIndent $ ppr err)
-                Nothing         -> return mm
-
-
--- | Parse and type-check a core module from a string.
-cmdCheckModuleFromString
-        :: (Ord n, Show n, Pretty n, Pretty (err (AnTEC BP.SourcePos n)))
-        => Fragment n err
-        -> Source
-        -> String
-        -> ErrorT String IO (Module (AnTEC BP.SourcePos n) n)
-
-cmdCheckModuleFromString fragment source str
- = goLoad
- where  lexModule = fragmentLexModule fragment 
-                        (nameOfSource source) 
-                        (lineStartOfSource source)
-
-        -- Load and type-check the module.
-        goLoad
-         = let  mModule = loadModuleFromString
-                                (fragmentProfile fragment) lexModule
-                                (nameOfSource source)
-                                str
-
-            in  case mModule of
-                  Left err       -> throwError (renderIndent $ ppr err)
-                  Right mm       -> goCheckFragment mm
-
-        goCheckFragment mm
-         = case fragmentCheckModule fragment mm of
-                Just err        -> throwError  (renderIndent $ ppr err)
-                Nothing         -> return mm
-
-
--- | Parse a core type, and check its kind.
-cmdParseCheckType 
-        :: (Ord n, Show n, Pretty n)
-        => Source
-        -> Fragment n err
-        -> String 
-        -> IO (Maybe (Type n, Kind n))
-
-cmdParseCheckType source frag str
+-- wtype ------------------------------------------------------------------------------------------
+-- | Show the type of a witness.
+cmdShowWType :: Language -> Source -> String -> IO ()
+cmdShowWType language source str
+ | Language bundle      <- language
+ , fragment             <- bundleFragment  bundle
  = let  srcName = nameOfSource source
         srcLine = lineStartOfSource source
-        toks    = fragmentLexExp frag srcName srcLine str
-        eTK     = loadType (fragmentProfile frag) srcName toks
+        toks    = fragmentLexExp fragment srcName srcLine str
+        eTK     = loadWitnessFromTokens fragment srcName toks
    in   case eTK of
-         Left err       
-          -> do outDocLn $ ppr err
-                return Nothing
-
-         Right (t, k)
-          ->    return $ Just (t, k)
-
-
--- | Parse the given core expression, 
---   and return it, along with its type, effect and closure.
---
---   If the expression had a parse error, undefined vars, or type error
---   then print this to the console.
---
---   We include a flag to override the language profile to allow partially
---   applied primitives. Although a paticular evaluator (or backend) may not
---   support partially applied primitives, we want to accept them if we are
---   only loading an expression to check its type.
---
-cmdParseCheckExp 
-        :: (Ord n, Show n, Pretty n, Pretty (err (AnTEC BP.SourcePos n)))
-        => Fragment n err       -- ^ The current language fragment.
-        -> ModuleMap (AnTEC () n) n -- ^ Current modules
-        -> Bool                 -- ^ Allow partial application of primitives.
-        -> Source               -- ^ Where this expression was sourced from.
-        -> String               -- ^ Text to parse.
-        -> IO (Maybe ( Exp (AnTEC BP.SourcePos n) n))
-
-cmdParseCheckExp frag modules permitPartialPrims source str
- = goLoad (fragmentLexExp frag (nameOfSource source) (lineStartOfSource source) str)
- where
-        -- Override profile to allow partially applied primitives if we were
-        -- told to do so.
-        profile   = fragmentProfile frag
-        features  = profileFeatures profile
-        features' = features { featuresPartialPrims 
-                             = featuresPartialPrims features || permitPartialPrims}
-        profile'  = profile  { profileFeatures  = features' }
-        frag'     = frag     { fragmentProfile  = profile'  }
-
-        -- Parse and type check the expression.
-        goLoad toks
-         = case loadExp (fragmentProfile frag') modules (nameOfSource source) toks of
-              Left err
-               -> do    putStrLn $ renderIndent $ ppr err
-                        return Nothing
-
-              Right result
-               -> goCheckFragment result
-
-        -- Do fragment specific checks.
-        goCheckFragment x
-         = case fragmentCheckExp frag' x of
-             Just err 
-              -> do     putStrLn $ renderIndent $ ppr err
-                        return Nothing
+         Left err       -> outDocLn $ ppr err
+         Right (t, k)   -> outDocLn $ ppr t <+> text "::" <+> ppr k
 
-             Nothing  
-              -> do     return (Just x)
diff --git a/DDC/Driver/Command/Compile.hs b/DDC/Driver/Command/Compile.hs
--- a/DDC/Driver/Command/Compile.hs
+++ b/DDC/Driver/Command/Compile.hs
@@ -5,17 +5,15 @@
 import DDC.Driver.Stage
 import DDC.Interface.Source
 import DDC.Build.Pipeline
-import DDC.Build.Language.Salt          as Salt
+import System.FilePath
 import System.Directory
 import Control.Monad
 import Control.Monad.Trans.Error
 import Control.Monad.IO.Class
-import Data.List
 import qualified DDC.Core.Pretty        as P
 
 
 -- | Compile a source module into a @.o@ file.
--- 
 cmdCompile :: Config -> FilePath -> ErrorT String IO ()
 cmdCompile config filePath
  = do   
@@ -25,27 +23,43 @@
          $ throwError $ "No such file " ++ show filePath
 
         src             <- liftIO $ readFile filePath
+        let ext         = takeExtension filePath
         let source      = SourceFile filePath
 
         -- Decide what to do based on file extension.
         let make
-                -- Make a Core Lite module.
-                | isSuffixOf ".dcl" filePath
+                -- Compile a Source Tetra module.
+                | ext == ".dst"
+                = liftIO
+                $ pipeText (nameOfSource source) (lineStartOfSource source) src
+                $ stageSourceTetraLoad config source
+                [ PipeCoreReannotate  (const ())
+                [ stageTetraToSalt     config source pipesSalt ]]
+
+                -- Compile a Core Tetra module.
+                | ext == ".dct"
+                = liftIO
+                $ pipeText (nameOfSource source) (lineStartOfSource source) src
+                $ stageTetraLoad    config source
+                [ stageTetraToSalt  config source pipesSalt ]
+
+                -- Compile a Core Lite module.
+                | ext == ".dcl"
                 = liftIO 
                 $ pipeText (nameOfSource source) (lineStartOfSource source) src
                 $ stageLiteLoad     config source
                 [ stageLiteOpt      config source  
                 [ stageLiteToSalt   config source pipesSalt ]]
 
-                -- Make a Core Salt module.
-                | isSuffixOf ".dcs" filePath
+                -- Compile a Core Salt module.
+                | ext == ".dcs"
                 = liftIO 
                 $ pipeText (nameOfSource source) (lineStartOfSource source) src
-                $ PipeTextLoadCore  Salt.fragment pipesSalt
+                $ stageSaltLoad     config source pipesSalt
 
                 -- Unrecognised.
                 | otherwise
-                = throwError $ "Don't know how to compile " ++ filePath
+                = throwError $ "Cannot compile '" ++ ext ++ "' files."
 
             pipesSalt
              = case configViaBackend config of
diff --git a/DDC/Driver/Command/Flow/Concretize.hs b/DDC/Driver/Command/Flow/Concretize.hs
--- a/DDC/Driver/Command/Flow/Concretize.hs
+++ b/DDC/Driver/Command/Flow/Concretize.hs
@@ -5,11 +5,13 @@
 import DDC.Build.Pipeline
 import DDC.Build.Language.Flow
 import DDC.Driver.Stage
+import DDC.Driver.Config
 import DDC.Interface.Source
 import DDC.Data.Canned
 import Control.Monad.Trans.Error
 import Control.Monad.IO.Class
 import qualified DDC.Core.Flow.Transform.Concretize     as Concretize
+import qualified DDC.Core.Check                         as C
 import qualified DDC.Base.Pretty                        as P
 
 
@@ -20,19 +22,21 @@
         -> String       -- ^ Program module text.
         -> ErrorT String IO ()
 
-cmdFlowConcretize _config source sourceText
- = do   
-        errs    <- liftIO
-                $  pipeText (nameOfSource source)
-                            (lineStartOfSource source)
-                            sourceText
-                $  PipeTextLoadCore fragment
-                [  PipeCoreReannotate (const ())
-                [  PipeCoreHacks 
-                   (Canned $ \m -> return 
-                           $  Concretize.concretizeModule m)
-                [  PipeCoreOutput SinkStdout ]]]
+cmdFlowConcretize config source sourceText
+ = let  pmode   = prettyModeOfConfig $ configPretty config
 
+        pipeConcretize
+         = pipeText (nameOfSource source)
+                    (lineStartOfSource source)
+                    sourceText
+         $ PipeTextLoadCore fragment C.Recon SinkDiscard
+         [ PipeCoreReannotate (const ())
+         [ PipeCoreHacks 
+                (Canned $ \m -> return 
+                        $  Concretize.concretizeModule m)
+         [ PipeCoreOutput pmode SinkStdout ]]]
+   in do
+        errs    <- liftIO pipeConcretize
         case errs of
          []     -> return ()
          es     -> throwError $ P.renderIndent $ P.vcat $ map P.ppr es
diff --git a/DDC/Driver/Command/Flow/Lower.hs b/DDC/Driver/Command/Flow/Lower.hs
--- a/DDC/Driver/Command/Flow/Lower.hs
+++ b/DDC/Driver/Command/Flow/Lower.hs
@@ -2,43 +2,52 @@
 module DDC.Driver.Command.Flow.Lower
         (cmdFlowLower)
 where
-import DDC.Driver.Stage
+import DDC.Driver.Stage                         as Driver
+import DDC.Driver.Config
 import DDC.Interface.Source
 import DDC.Build.Pipeline
 import Control.Monad.Trans.Error
 import Control.Monad.IO.Class
 import qualified DDC.Base.Pretty                as P
+import qualified DDC.Core.Check                 as C
 import qualified DDC.Build.Language.Flow        as Flow
+import qualified DDC.Core.Flow                  as Flow
 
 
 -- | Lower a flow program to loop code.
 cmdFlowLower
-        :: Config
-        -> Source       -- ^ Source of the code.
-        -> String       -- ^ Program module text.
+        :: Driver.Config        -- ^ Driver config.
+        -> Flow.Config          -- ^ Config for the lowering transform.
+        -> Source               -- ^ Source of the code.
+        -> String               -- ^ Program module text.
         -> ErrorT String IO ()
 
-cmdFlowLower config source sourceText
+cmdFlowLower
+        configDriver configLower
+        source sourceText
  = let  
+        pmode   = prettyModeOfConfig $ configPretty configDriver
+
         pipeLower
          = pipeText (nameOfSource source)
                     (lineStartOfSource source)
                     sourceText
-         $  stageFlowLoad  config source
-         [  stageFlowPrep  config source
-         [  PipeCoreCheck  Flow.fragment
-         [  stageFlowLower config source [ pipeFinal ]]]]
+         $  stageFlowLoad  configDriver source 
+         [  stageFlowPrep  configDriver source
+         [  PipeCoreCheck  Flow.fragment C.Recon SinkDiscard
+         [  stageFlowLower configDriver configLower source [ pipeFinal ]]]]
 
         pipeFinal
-         | configTaintAvoidTypeChecks config
-         = PipeCoreOutput SinkStdout
+         | configTaintAvoidTypeChecks configDriver
+         = PipeCoreOutput   pmode SinkStdout 
 
          | otherwise
-         = PipeCoreCheck Flow.fragment
-         [ PipeCoreOutput SinkStdout ]
+         = PipeCoreCheck    Flow.fragment C.Recon SinkDiscard
+         [ PipeCoreOutput   pmode SinkStdout ]
 
    in do        
         errs    <- liftIO pipeLower
         case errs of
          []     -> return ()
          es     -> throwError $ P.renderIndent $ P.vcat $ map P.ppr es
+
diff --git a/DDC/Driver/Command/Flow/Melt.hs b/DDC/Driver/Command/Flow/Melt.hs
new file mode 100644
--- /dev/null
+++ b/DDC/Driver/Command/Flow/Melt.hs
@@ -0,0 +1,47 @@
+
+module DDC.Driver.Command.Flow.Melt
+        (cmdFlowMelt)
+where
+import DDC.Interface.Source
+import DDC.Driver.Stage
+import DDC.Driver.Config
+import DDC.Build.Pipeline
+import DDC.Build.Language.Flow
+import Control.Monad.Trans.Error
+import Control.Monad.IO.Class
+import qualified DDC.Core.Check         as C
+import qualified DDC.Base.Pretty        as P
+
+
+-- | Thread a state token through the given flow program.
+--     This can't be generic in the language fragment because we
+--     need to provide a specific type to use for the world token,
+--     and new types for the effectful combinators.
+cmdFlowMelt
+        :: Config               -- ^ Driver config.
+        -> Source               -- ^ Source of the code.
+        -> String               -- ^ Program module text.
+        -> ErrorT String IO ()
+
+cmdFlowMelt config source sourceText
+ = let  pmode   = prettyModeOfConfig $ configPretty config
+        
+        pipeMelt
+         = pipeText (nameOfSource source)
+                    (lineStartOfSource source)
+                    sourceText
+         $ stageFlowLoad  config source 
+         [ PipeCoreCheck  fragment C.Recon SinkDiscard
+         [ PipeCoreAsFlow 
+         [ PipeFlowMelt
+         [ PipeCoreCheck  fragment C.Recon SinkDiscard
+         [ PipeCoreOutput pmode SinkStdout ]]]]]
+
+   in do
+        errs    <- liftIO pipeMelt
+        case errs of
+         []     -> return ()
+         es     -> throwError $ P.renderIndent $ P.vcat $ map P.ppr es
+
+
+
diff --git a/DDC/Driver/Command/Flow/Prep.hs b/DDC/Driver/Command/Flow/Prep.hs
--- a/DDC/Driver/Command/Flow/Prep.hs
+++ b/DDC/Driver/Command/Flow/Prep.hs
@@ -3,32 +3,36 @@
         (cmdFlowPrep)
 where
 import DDC.Driver.Stage
+import DDC.Driver.Config
 import DDC.Interface.Source
 import DDC.Build.Pipeline
 import Control.Monad.Trans.Error
 import Control.Monad.IO.Class
+import qualified DDC.Core.Check                 as C
 import qualified DDC.Base.Pretty                as P
 import qualified DDC.Build.Language.Flow        as Flow
 
 
 -- | Prepare a Disciple Core Flow module for lowering.
 cmdFlowPrep
-        :: Config
-        -> Source       -- ^ Source of the code.
-        -> String       -- ^ Program module text.
+        :: Config               -- ^ Driver config.
+        -> Source               -- ^ Source of the code.
+        -> String               -- ^ Program module text.
         -> ErrorT String IO ()
 
 cmdFlowPrep config source sourceText
- = do   
-        errs    <- liftIO
-                $  pipeText (nameOfSource source)
-                            (lineStartOfSource source)
-                            sourceText
-                $  stageFlowLoad  config source
-                [  stageFlowPrep  config source
-                [  PipeCoreCheck Flow.fragment
-                [  PipeCoreOutput SinkStdout ]]]
-
+ = let  pmode   = prettyModeOfConfig $ configPretty config
+        
+        pipePrep
+         = pipeText (nameOfSource source)
+                     (lineStartOfSource source)
+                     sourceText
+         $ stageFlowLoad  config source 
+         [ stageFlowPrep  config source
+         [ PipeCoreCheck  Flow.fragment C.Recon SinkDiscard
+         [ PipeCoreOutput pmode SinkStdout ]]]
+   in do
+        errs    <- liftIO pipePrep
         case errs of
          []     -> return ()
          es     -> throwError $ P.renderIndent $ P.vcat $ map P.ppr es
diff --git a/DDC/Driver/Command/Flow/Rate.hs b/DDC/Driver/Command/Flow/Rate.hs
new file mode 100644
--- /dev/null
+++ b/DDC/Driver/Command/Flow/Rate.hs
@@ -0,0 +1,40 @@
+
+module DDC.Driver.Command.Flow.Rate
+        (cmdFlowRate)
+where
+import DDC.Driver.Stage
+import DDC.Driver.Config
+import DDC.Interface.Source
+import DDC.Build.Pipeline
+import Control.Monad.Trans.Error
+import Control.Monad.IO.Class
+import qualified DDC.Base.Pretty                as P
+import qualified DDC.Core.Check                 as C
+import qualified DDC.Build.Language.Flow        as Flow
+
+
+-- | Perform rate inference to transform vector operations to series
+cmdFlowRate
+        :: Config               -- ^ Driver config.
+        -> Source               -- ^ Source of the code.
+        -> String               -- ^ Program module text.
+        -> ErrorT String IO ()
+
+cmdFlowRate config source sourceText
+ = let  pmode   = prettyModeOfConfig $ configPretty config
+        
+        pipeRate
+         = pipeText (nameOfSource source)
+                    (lineStartOfSource source)
+                    sourceText
+         $ stageFlowLoad  config source 
+         [ stageFlowRate  config source 
+         [ PipeCoreCheck  Flow.fragment C.Recon SinkDiscard
+         [ PipeCoreOutput pmode SinkStdout ]]]
+   
+   in do
+        errs    <- liftIO pipeRate
+        case errs of
+         []     -> return ()
+         es     -> throwError $ P.renderIndent $ P.vcat $ map P.ppr es
+
diff --git a/DDC/Driver/Command/Flow/Thread.hs b/DDC/Driver/Command/Flow/Thread.hs
--- a/DDC/Driver/Command/Flow/Thread.hs
+++ b/DDC/Driver/Command/Flow/Thread.hs
@@ -2,16 +2,18 @@
 module DDC.Driver.Command.Flow.Thread
         (cmdFlowThread)
 where
+import DDC.Interface.Source
 import DDC.Build.Pipeline
 import DDC.Build.Language.Flow
-import DDC.Core.Fragment
 import DDC.Driver.Stage
-import DDC.Interface.Source
+import DDC.Driver.Config
+import DDC.Core.Fragment
 import DDC.Data.Canned
 import Control.Monad.Trans.Error
 import Control.Monad.IO.Class
 import qualified DDC.Core.Transform.Thread      as Thread
 import qualified DDC.Core.Flow.Transform.Thread as Flow
+import qualified DDC.Core.Check                 as C
 import qualified DDC.Base.Pretty                as P
 
 
@@ -20,30 +22,31 @@
 --     need to provide a specific type to use for the world token,
 --     and new types for the effectful combinators.
 cmdFlowThread
-        :: Config
-        -> Source       -- ^ Source of the code.
-        -> String       -- ^ Program module text.
+        :: Config               -- ^ Driver config.
+        -> Source               -- ^ Source of the code.
+        -> String               -- ^ Program module text.
         -> ErrorT String IO ()
 
-cmdFlowThread _config source sourceText
- = do   
-        errs    <- liftIO
-                $  pipeText (nameOfSource source)
-                            (lineStartOfSource source)
-                            sourceText
-                $  PipeTextLoadCore fragment
-                [  PipeCoreReannotate (const ())
-                [  PipeCoreCheck    fragment
-                [  PipeCoreHacks 
-                   (Canned $ \m -> return 
-                           $  Thread.thread Flow.threadConfig 
-                                (profilePrimKinds (fragmentProfile fragment))
-                                (profilePrimTypes (fragmentProfile fragment)) m)
-                [  PipeCoreOutput SinkStdout ]]]]
+cmdFlowThread config source sourceText
+ = let  pmode   = prettyModeOfConfig $ configPretty config
+        
+        pipeThread
+         = pipeText (nameOfSource source)
+                    (lineStartOfSource source)
+                    sourceText
+         $  PipeTextLoadCore fragment C.Recon SinkDiscard
+         [  PipeCoreReannotate (const ())
+         [  PipeCoreCheck    fragment C.Recon SinkDiscard
+         [  PipeCoreHacks 
+            (Canned $ \m -> return 
+                    $  Thread.thread Flow.threadConfig 
+                        (profilePrimKinds (fragmentProfile fragment))
+                        (profilePrimTypes (fragmentProfile fragment)) m)
+         [  PipeCoreOutput pmode SinkStdout ]]]]
 
+   in do
+        errs    <- liftIO pipeThread
         case errs of
          []     -> return ()
          es     -> throwError $ P.renderIndent $ P.vcat $ map P.ppr es
-
-
 
diff --git a/DDC/Driver/Command/Flow/Wind.hs b/DDC/Driver/Command/Flow/Wind.hs
--- a/DDC/Driver/Command/Flow/Wind.hs
+++ b/DDC/Driver/Command/Flow/Wind.hs
@@ -3,11 +3,13 @@
         (cmdFlowWind)
 where
 import DDC.Driver.Stage
+import DDC.Driver.Config
 import DDC.Interface.Source
 import DDC.Build.Pipeline
 import Control.Monad.Trans.Error
 import Control.Monad.IO.Class
 import qualified DDC.Base.Pretty                as P
+import qualified DDC.Core.Check                 as C
 import qualified DDC.Build.Language.Flow        as Flow
 
 
@@ -19,22 +21,23 @@
         -> ErrorT String IO ()
 
 cmdFlowWind config source sourceText
- = let  
+ = let  pmode   = prettyModeOfConfig $ configPretty config
+
         pipeLower
          = pipeText (nameOfSource source)
                     (lineStartOfSource source)
                     sourceText
-         $  stageFlowLoad  config source
-         [  PipeCoreCheck  Flow.fragment
-         [  stageFlowWind config source [ pipeFinal ]]]
+         $  stageFlowLoad  config source 
+         [  PipeCoreCheck  Flow.fragment C.Recon SinkDiscard
+         [  stageFlowWind  config source [ pipeFinal ]]]
 
         pipeFinal
          | configTaintAvoidTypeChecks config
-         = PipeCoreOutput SinkStdout
+         = PipeCoreOutput pmode SinkStdout
 
          | otherwise
-         = PipeCoreCheck Flow.fragment
-         [ PipeCoreOutput SinkStdout ]
+         = PipeCoreCheck Flow.fragment C.Recon SinkDiscard
+         [ PipeCoreOutput pmode SinkStdout ]
 
    in do        
         errs    <- liftIO pipeLower
diff --git a/DDC/Driver/Command/Load.hs b/DDC/Driver/Command/Load.hs
--- a/DDC/Driver/Command/Load.hs
+++ b/DDC/Driver/Command/Load.hs
@@ -1,177 +1,235 @@
 
 module DDC.Driver.Command.Load
-        ( cmdReadModule
-        , cmdReadModule'
-        , cmdLoadFromFile
-        , cmdLoadFromString)
+        ( cmdLoadFromFile
+        , cmdLoadSourceTetraFromFile
+        , cmdLoadSourceTetraFromString
+        , cmdLoadCoreFromFile
+        , cmdLoadCoreFromString
+        , cmdLoadSimplifier)
 where
 import DDC.Interface.Source
 import DDC.Build.Pipeline
 import DDC.Build.Language
 import DDC.Core.Simplifier.Parser
 import DDC.Core.Transform.Reannotate
-import DDC.Core.Module
-import DDC.Core.Load
+import DDC.Driver.Command.Read
+import DDC.Driver.Stage
+import DDC.Driver.Config
+import DDC.Core.Annot.AnTEC
 import DDC.Core.Pretty
-import DDC.Data.Canned
-import Control.DeepSeq
 import Control.Monad
 import Control.Monad.Trans.Error
 import Control.Monad.IO.Class
-import Data.IORef
-import System.Directory
 import System.FilePath
-import System.IO
-import qualified Data.Map               as Map
-import qualified DDC.Base.Parser        as BP
+import System.Directory
+import qualified Data.Map                       as Map
+import qualified DDC.Core.Check                 as C
 
 
--- Read -----------------------------------------------------------------------
--- | Load and typecheck a module.
-cmdReadModule 
-        :: (Ord n, Show n, Pretty n, NFData n)
-        => Fragment n err       -- ^ Language fragment.
-        -> FilePath             -- ^ Path to the module.
-        -> IO (Maybe (Module (AnTEC BP.SourcePos n) n))
-cmdReadModule = cmdReadModule' True
+-------------------------------------------------------------------------------
+-- | Load and transform a module.
+--   The result is printed to @stdout@.
+--   Any errors are thrown in the `ErrorT` monad.
+--
+--   This function handle fragments of Disciple Core, as well as Source Tetra
+--   modules. The language to use is determined by inspecting the file name
+--   extension.
+--      
+--   We also take the specification of a simplifier to apply to the module.
+--
+cmdLoadFromFile
+        :: Config               -- ^ Driver config.
+        -> Maybe String         -- ^ Simplifier specification.
+        -> [FilePath]           -- ^ More modules to use as inliner templates.
+        -> FilePath             -- ^ Module file name.
+        -> ErrorT String IO ()
 
+cmdLoadFromFile config mStrSimpl fsTemplates filePath
 
-cmdReadModule'
-        :: (Ord n, Show n, Pretty n, NFData n)
-        => Bool                 -- ^ If true, print errors out
-        -> Fragment n err       -- ^ Language fragment.
-        -> FilePath             -- ^ Path to the module.
-        -> IO (Maybe (Module (AnTEC BP.SourcePos n) n))
+ -- Load a Disciple Source Tetra module.
+ | ".dst"        <- takeExtension filePath
+ =      cmdLoadSourceTetraFromFile config filePath
 
-cmdReadModule' printErrors frag filePath
- = do
-        -- Read in the source file.
-        exists  <- doesFileExist filePath
+ -- Load a module in some fragment of Disciple Core.
+ | Just language <- languageOfExtension (takeExtension filePath)
+ = case mStrSimpl of
+        Nothing 
+         ->     cmdLoadCoreFromFile config language filePath
+        
+        Just strSimpl
+         -> do  language' <- cmdLoadSimplifier config language strSimpl fsTemplates
+                cmdLoadCoreFromFile config language' filePath
+
+ -- Don't know how to load this file.
+ | otherwise
+ = let  ext     = takeExtension filePath
+   in   throwError $ "Cannot load '" ++ ext ++ "' files."
+
+
+-------------------------------------------------------------------------------
+-- | Load a Disciple Source Tetra module from a file.
+--   The result is printed to @stdout@.
+--   Any errors are thrown in the `ErrorT` monad.
+cmdLoadSourceTetraFromFile
+        :: Config               -- ^ Driver config.
+        -> FilePath             -- ^ Module file path.
+        -> ErrorT String IO ()
+
+cmdLoadSourceTetraFromFile config filePath
+ = do   
+        -- Check that the file exists.
+        exists  <- liftIO $ doesFileExist filePath
         when (not exists)
-         $      error $ "No such file " ++ show filePath
+         $ throwError $ "No such file " ++ show filePath
 
-        src     <- readFile filePath
-        let source   = SourceFile filePath
+        -- Read in the source file.
+        src     <- liftIO $ readFile filePath
 
-        cmdReadModule_parse printErrors filePath frag source src
+        cmdLoadSourceTetraFromString config (SourceFile filePath) src
 
 
-cmdReadModule_parse printErrors filePath frag source src
- = do   ref     <- newIORef Nothing
-        errs    <- pipeText (nameOfSource source) (lineStartOfSource source) src
-                $  PipeTextLoadCore frag
-                   [ PipeCoreHacks (Canned (\m -> writeIORef ref (Just m) >> return m)) 
-                     [PipeCoreOutput SinkDiscard] ]
+-------------------------------------------------------------------------------
+-- | Load a Disciple Source Tetra module from a string.
+--   The result is printed to @stdout@.
+--   Any errors are thrown in the `ErrorT` monad.
+cmdLoadSourceTetraFromString
+        :: Config               -- ^ Driver config.
+        -> Source               -- ^ Source of the code.
+        -> String               -- ^ Program module text.
+        -> ErrorT String IO ()
 
+cmdLoadSourceTetraFromString config source str
+ = let
+        pmode   = prettyModeOfConfig $ configPretty config
+
+        pipeLoad
+         = pipeText     (nameOfSource source) (lineStartOfSource source) str
+         $ stageSourceTetraLoad config source
+         [ PipeCoreOutput pmode SinkStdout ]
+   in do
+        errs    <- liftIO pipeLoad
         case errs of
-         [] -> do
-                readIORef ref
+         [] -> return ()
+         es -> throwError $ renderIndent $ vcat $ map ppr es
+ 
 
-         _ -> do
-                when printErrors
-                 $ do putStrLn $ "When reading " ++ filePath
-                      mapM_ (hPutStrLn stderr . renderIndent . ppr) errs
-                return Nothing
+-------------------------------------------------------------------------------
+-- | Load a Disciple Core module from a file.
+--   The result is printed to @stdout@.
+cmdLoadCoreFromFile
+        :: Config               -- ^ Driver config.
+        -> Language             -- ^ Core language definition.
+        -> FilePath             -- ^ Module file path
+        -> ErrorT String IO ()
 
+cmdLoadCoreFromFile config language filePath
+ = do
+        -- Check that the file exists.
+        exists  <- liftIO $ doesFileExist filePath
+        when (not exists)
+         $ throwError $ "No such file " ++ show filePath
 
+        -- Read in the source file.
+        src     <- liftIO $ readFile filePath
+
+        cmdLoadCoreFromString config language (SourceFile filePath) src
+
+
 -------------------------------------------------------------------------------
--- | Load and transform a module, printing the result to stdout.
---   The current transform is set with the given string.
-cmdLoadFromFile
-        :: Maybe String         -- ^ Simplifier specification.
-        -> [FilePath]           -- ^ More modules to use as inliner templates.
-        -> FilePath             -- ^ Module file name.
+-- | Load a Disciple Core module from a string.
+--   The result it printed to @stdout@.
+cmdLoadCoreFromString
+        :: Config               -- ^ Driver config.
+        -> Language             -- ^ Language definition
+        -> Source               -- ^ Source of the code.
+        -> String               -- ^ Program module text.
         -> ErrorT String IO ()
 
-cmdLoadFromFile strSimpl fsTemplates filePath
- = case languageOfExtension (takeExtension filePath) of
-        Nothing       -> throwError $ "Unknown file extension."
-        Just language -> cmdLoad_language strSimpl fsTemplates filePath language
+cmdLoadCoreFromString config language source str
+ | Language bundle      <- language
+ , fragment             <- bundleFragment   bundle
+ = let  
+        pmode           = prettyModeOfConfig $ configPretty config
 
-cmdLoad_language Nothing _ filePath language
- = configLoad_simpl language filePath
+        -- The type inferencer doesn't work with the Lite fragment.
+        config'         = if fragmentExtension fragment == "dcl"
+                                then config { configInferTypes = False}
+                                else config
 
-cmdLoad_language (Just strSimpl) fsTemplates filePath language
+        pipeLoad
+         = pipeText     (nameOfSource source) (lineStartOfSource source) str
+         $ PipeTextLoadCore  fragment 
+                        (if configInferTypes config' then C.Synth else C.Recon) 
+                        SinkDiscard
+         [ PipeCoreReannotate (\a -> a { annotTail = () })
+         [ PipeCoreSimplify  fragment (bundleStateInit bundle)
+                                      (bundleSimplifier bundle)
+         [ PipeCoreOutput    pmode SinkStdout ]]]
+
+   in do
+        errs    <- liftIO pipeLoad
+        case errs of
+         [] -> return ()
+         es -> throwError $ renderIndent $ vcat $ map ppr es
+
+
+-------------------------------------------------------------------------------
+-- | Parse the simplifier defined in this string, 
+--   and load it and all the inliner templates into the language bundle.
+cmdLoadSimplifier 
+        :: Config               -- ^ Driver config.
+        -> Language             -- ^ Language definition.
+        -> String               -- ^ Simplifier specification.
+        -> [FilePath]           -- ^ Modules to use as inliner templates.
+        -> ErrorT String IO Language
+
+cmdLoadSimplifier config language strSimpl fsTemplates
  | Language bundle      <- language
- , modules              <- bundleModules       bundle
- , rules                <- bundleRewriteRules  bundle
+ , modules_bundle       <- bundleModules bundle
  , mkNamT               <- bundleMakeNamifierT bundle
  , mkNamX               <- bundleMakeNamifierX bundle
+ , rules                <- bundleRewriteRules bundle
  , fragment             <- bundleFragment      bundle
  , readName             <- fragmentReadName    fragment
  = do
-        let rules'          = Map.assocs rules
-
         -- Load all the modues that we're using for inliner templates.
         --  If any of these don't load then the 'cmdReadModule' function 
         --  will display the errors.
-        mMoreModules
+        mModules
          <- liftM sequence
-         $  mapM (liftIO . cmdReadModule fragment)
+         $  mapM (liftIO . cmdReadModule config fragment)
                  fsTemplates
 
+        modules_annot
+         <- case mModules of
+                 Nothing -> throwError $ "Cannot load inlined module."
+                 Just ms -> return     $ ms
+
+        -- Zap annotations on the loaded modules.
+        -- Any type errors will already have been displayed, so we don't need 
+        -- the source position info any more.
         let zapAnnot annot
                 = annot { annotTail = () }
 
-        moreModules
-         <- case mMoreModules of
-                 Nothing -> throwError $ "Imported modules do not parse."
-                 Just ms -> return     $ map (reannotate zapAnnot) ms
+        let modules_new 
+                = map (reannotate zapAnnot) modules_annot
 
         -- Collect all definitions from modules
-        let templateModules
-                = moreModules ++ (Map.elems modules)
+        let modules_all
+                = Map.elems modules_bundle ++ modules_new
 
-        -- Simplifier details for the parser.
+        -- Wrap up the inliner templates and current rules into
+        -- a SimplifierDetails, which we give to the Simplifier parser.
         let details
                 = SimplifierDetails mkNamT mkNamX 
-                        [(n, reannotate zapAnnot rule) | (n, rule) <- rules']
-                        templateModules
+                    [(n, reannotate zapAnnot rule) | (n, rule) <- Map.assocs rules]
+                    modules_all
 
+        -- Parse the simplifer string.
         case parseSimplifier readName details strSimpl of
          Left err
           -> throwError $ renderIndent $ ppr err
 
          Right simpl
-          -> let bundle' = bundle { bundleSimplifier = simpl }
-             in  configLoad_simpl (Language bundle') filePath
-
-configLoad_simpl language filePath
- = do   
-        -- Check that the file exists.
-        exists  <- liftIO $ doesFileExist filePath
-        when (not exists)
-         $ throwError $ "No such file " ++ show filePath
-
-        -- Read in the source file.
-        src     <- liftIO $ readFile filePath
-
-        cmdLoadFromString language (SourceFile filePath) src
-
-
--------------------------------------------------------------------------------
--- | Load and transform a module, 
---   then print the result to @stdout@.
-cmdLoadFromString
-        :: Language             -- ^ Language definition
-        -> Source               -- ^ Source of the code.
-        -> String               -- ^ Program module text.
-        -> ErrorT String IO ()
-
-cmdLoadFromString language source str
- | Language bundle      <- language
- , fragment             <- bundleFragment   bundle
- , simpl                <- bundleSimplifier bundle
- , zero                 <- bundleStateInit  bundle
- = do   errs    <- liftIO
-                $  pipeText (nameOfSource source) (lineStartOfSource source) str
-                $  PipeTextLoadCore  fragment
-                [  PipeCoreReannotate (\a -> a { annotTail = ()})
-                [  PipeCoreSimplify  fragment zero simpl
-                [  PipeCoreCheck     fragment
-                [  PipeCoreOutput    SinkStdout ]]]]
-
-        case errs of
-         [] -> return ()
-         es -> throwError $ renderIndent $ vcat $ map ppr es
+          -> return $ Language $ bundle { bundleSimplifier = simpl }
 
diff --git a/DDC/Driver/Command/Make.hs b/DDC/Driver/Command/Make.hs
--- a/DDC/Driver/Command/Make.hs
+++ b/DDC/Driver/Command/Make.hs
@@ -5,12 +5,11 @@
 import DDC.Driver.Stage
 import DDC.Interface.Source
 import DDC.Build.Pipeline
-import DDC.Build.Language.Salt          as Salt
+import System.FilePath
 import System.Directory
 import Control.Monad.Trans.Error
 import Control.Monad.IO.Class
 import Control.Monad
-import Data.List
 import qualified DDC.Core.Pretty        as P
 
 
@@ -24,12 +23,28 @@
          $ throwError $ "No such file " ++ show filePath
 
         src             <- liftIO $ readFile filePath
+        let ext         = takeExtension filePath
         let source      = SourceFile filePath
 
         -- Decide what to do based on file extension.
         let make
+                -- Make a Source Tetra module.
+                | ext == ".dst"
+                = liftIO
+                $ pipeText (nameOfSource source) (lineStartOfSource source) src
+                $ stageSourceTetraLoad config source
+                [ PipeCoreReannotate  (const ())
+                [ stageTetraToSalt     config source pipesSalt ]]
+
+                -- Make a Core Tetra module.
+                | ext == ".dct"
+                = liftIO
+                $ pipeText (nameOfSource source) (lineStartOfSource source) src
+                $ stageTetraLoad    config source
+                [ stageTetraToSalt  config source pipesSalt ]
+
                 -- Make a Core Lite module.
-                | isSuffixOf ".dcl" filePath
+                | ext == ".dcl"
                 = liftIO
                 $ pipeText (nameOfSource source) (lineStartOfSource source) src
                 $ stageLiteLoad     config source
@@ -37,14 +52,14 @@
                 [ stageLiteToSalt   config source pipesSalt ]]
 
                 -- Make a Core Salt module.
-                | isSuffixOf ".dcs" filePath
+                | ext == ".dcs"
                 = liftIO
                 $ pipeText (nameOfSource source) (lineStartOfSource source) src
-                $ PipeTextLoadCore  Salt.fragment pipesSalt
+                $ stageSaltLoad     config source pipesSalt 
 
                 -- Unrecognised.
                 | otherwise
-                = throwError $ "Don't know how to make " ++ filePath
+                = throwError $ "Cannot make '" ++ filePath ++ "' files."
 
             pipesSalt
              = case configViaBackend config of
diff --git a/DDC/Driver/Command/Parse.hs b/DDC/Driver/Command/Parse.hs
--- a/DDC/Driver/Command/Parse.hs
+++ b/DDC/Driver/Command/Parse.hs
@@ -1,27 +1,133 @@
 
 module DDC.Driver.Command.Parse
-        (cmdParseModule)
+        ( cmdParseFromFile
+        , cmdParseSourceTetraFromFile
+        , cmdParseCoreFromFile)
 where
-import DDC.Interface.Source
 import DDC.Driver.Stage
+import DDC.Build.Language
+import DDC.Source.Tetra.Pretty
+import DDC.Source.Tetra.Lexer           as ST
+import DDC.Source.Tetra.Parser          as ST
+import DDC.Core.Fragment                as C
+import DDC.Core.Parser                  as C
+import DDC.Core.Lexer                   as C
+import DDC.Base.Parser                  as BP
+import DDC.Data.Token                   as Token
 import Control.Monad.Trans.Error
 import Control.Monad.IO.Class
 import System.FilePath
-import qualified DDC.Core.Lexer as C
+import System.Directory
+import Control.Monad
 
 
-cmdParseModule :: Config -> Source -> String -> ErrorT String IO ()
-cmdParseModule config source str
- | SourceFile filePath  <- source
- = case takeExtension filePath of
-        ".dst"  -> cmdParseModule_tetra config filePath str
-        _       -> throwError "Unknown file extension."
+-------------------------------------------------------------------------------
+-- | Parse a module.
+--   The result AST is printed to @stdout@.
+--   Any errors are thrown in the `ErrorT` monad.
+--
+--   This function handle fragments of Disciple Core, as well as Source Tetra
+--   modules. The language to use is determined by inspecting the file name
+--   extension.
+--
+cmdParseFromFile 
+        :: Config               -- ^ Driver config.
+        -> FilePath             -- ^ Module file name.
+        -> ErrorT String IO ()
 
+cmdParseFromFile config filePath
+ 
+ -- Parse a Disciple Source Tetra module.
+ | ".dst"        <- takeExtension filePath
+ =  cmdParseSourceTetraFromFile config filePath
+
+ -- Parse a module in some fragment of Disciple Core.
+ | Just language <- languageOfExtension (takeExtension filePath)
+ = cmdParseCoreFromFile config language filePath
+
+ -- Don't know how to parse this file.
  | otherwise
- = throwError "Cannot detect language."
+ = let  ext     = takeExtension filePath
+   in   throwError $ "Cannot parse '" ++ ext ++ "' files."
 
 
-cmdParseModule_tetra _config sourcePathName str
- = do   let tokens = C.lexModuleWithOffside sourcePathName 1 str
-        liftIO $ putStrLn $ show tokens
-        return ()
+-------------------------------------------------------------------------------
+-- | Parse a Disciple Source Tetra module from a file.
+--   The result AST is printed to @stdout@.
+--   Any errors are thrown in the `ErrorT` monad.
+cmdParseSourceTetraFromFile
+        :: Config               -- ^ Driver config.
+        -> FilePath             -- ^ Module file path.
+        -> ErrorT String IO ()
+
+cmdParseSourceTetraFromFile config filePath
+ = do   
+        -- Check that the file exists.
+        exists  <- liftIO $ doesFileExist filePath
+        when (not exists)
+         $ throwError $ "No such file " ++ show filePath
+
+        -- Read in the source file.
+        src     <- liftIO $ readFile filePath
+
+        -- Lex the source string.
+        let toks    = ST.lexModuleString filePath 1 src
+
+        when (configDump config)
+         $ liftIO $ writeFile "dump.tetra-parse.tokens-sp" 
+                  $ unlines $ map show toks
+
+        when (configDump config)
+         $ liftIO $ writeFile "dump.tetra-parse.tokens" 
+                  $ unlines $ map show $ map Token.tokenTok toks
+
+        let context = ST.Context
+                    { ST.contextTrackedEffects          = True
+                    , ST.contextTrackedClosures         = True
+                    , ST.contextFunctionalEffects       = False
+                    , ST.contextFunctionalClosures      = False }
+                    
+        case BP.runTokenParser
+                C.describeTok filePath 
+                (ST.pModule context) toks of
+         Left err 
+          ->    throwError (renderIndent $ ppr err)
+         
+         Right mm
+          ->    liftIO $ putStrLn (renderIndent $ ppr mm)
+
+
+-------------------------------------------------------------------------------
+-- | Parse a Disciple Core module from a file.
+--   The AST is printed to @stdout@.
+--   Any errors are thrown in the `ErrorT` monad.
+cmdParseCoreFromFile
+        :: Config               -- ^ Driver config
+        -> Language             -- ^ Core language definition.
+        -> FilePath             -- ^ Module file path.
+        -> ErrorT String IO ()
+
+cmdParseCoreFromFile _config language filePath
+ | Language bundle      <- language
+ , fragment             <- bundleFragment  bundle
+ , profile              <- fragmentProfile fragment
+ = do   
+        -- Check that the file exists.
+        exists  <- liftIO $ doesFileExist filePath
+        when (not exists)
+         $ throwError $ "No such file " ++ show filePath
+
+        -- Read in the source file.
+        src     <- liftIO $ readFile filePath
+
+        -- Lex the source string.
+        let toks = (C.fragmentLexModule fragment) filePath 1 src
+
+        case BP.runTokenParser
+                C.describeTok filePath 
+                (C.pModule (C.contextOfProfile profile)) toks of
+         Left err
+          ->    throwError (renderIndent $ ppr err)
+
+         Right mm
+          ->    liftIO $ putStrLn (renderIndent $ ppr mm)
diff --git a/DDC/Driver/Command/Read.hs b/DDC/Driver/Command/Read.hs
new file mode 100644
--- /dev/null
+++ b/DDC/Driver/Command/Read.hs
@@ -0,0 +1,78 @@
+
+module DDC.Driver.Command.Read
+        ( cmdReadModule
+        , cmdReadModule')
+where
+import DDC.Interface.Source
+import DDC.Driver.Config
+import DDC.Build.Pipeline
+import DDC.Build.Language
+import DDC.Core.Module
+import DDC.Core.Load
+import DDC.Core.Pretty
+import DDC.Data.Canned
+import Control.DeepSeq
+import Control.Monad
+import Data.IORef
+import System.Directory
+import System.IO
+import qualified DDC.Base.Parser                as BP
+import qualified DDC.Core.Check                 as C
+
+
+-- Read -----------------------------------------------------------------------
+-- | Load and typecheck a module.
+cmdReadModule 
+        :: (Ord n, Show n, Pretty n, Pretty (err (AnTEC BP.SourcePos n)), NFData n)
+        => Config               -- ^ Driver config.
+        -> Fragment n err       -- ^ Language fragment.
+        -> FilePath             -- ^ Path to the module.
+        -> IO (Maybe (Module (AnTEC BP.SourcePos n) n))
+cmdReadModule = cmdReadModule' True
+
+
+cmdReadModule'
+        :: (Ord n, Show n, Pretty n, Pretty (err (AnTEC BP.SourcePos n)), NFData n)
+        => Bool                 -- ^ If true, print errors out
+        -> Config               -- ^ Driver config
+        -> Fragment n err       -- ^ Language fragment.
+        -> FilePath             -- ^ Path to the module.
+        -> IO (Maybe (Module (AnTEC BP.SourcePos n) n))
+
+cmdReadModule' printErrors config fragment filePath
+ = do
+        -- The inferencer doesn't work with the Lite fragment.
+        let config'     = if fragmentExtension fragment == "dcl"
+                                then config { configInferTypes = False }
+                                else config
+
+        -- Read in the source file.
+        exists  <- doesFileExist filePath
+        when (not exists)
+         $      error $ "No such file " ++ show filePath
+
+        src     <- readFile filePath
+        let source   = SourceFile filePath
+
+        cmdReadModule_parse printErrors config' filePath fragment source src
+
+
+cmdReadModule_parse printErrors config filePath fragment source src
+ = do   ref     <- newIORef Nothing
+        errs    <- pipeText (nameOfSource source) (lineStartOfSource source) src
+                $  PipeTextLoadCore fragment
+                        (if configInferTypes config then C.Synth else C.Recon)
+                        SinkDiscard
+                   [ PipeCoreHacks (Canned (\m -> writeIORef ref (Just m) >> return m)) 
+                     [PipeCoreOutput pprDefaultMode SinkDiscard] ]
+
+        case errs of
+         [] -> do
+                readIORef ref
+
+         _ -> do
+                when printErrors
+                 $ do putStrLn $ "When reading " ++ filePath
+                      mapM_ (hPutStrLn stderr . renderIndent . ppr) errs
+                return Nothing
+
diff --git a/DDC/Driver/Command/RewriteRules.hs b/DDC/Driver/Command/RewriteRules.hs
--- a/DDC/Driver/Command/RewriteRules.hs
+++ b/DDC/Driver/Command/RewriteRules.hs
@@ -9,6 +9,7 @@
 import DDC.Core.Module
 import DDC.Core.Lexer
 import DDC.Core.Pretty
+import DDC.Core.Exp
 import DDC.Core.Transform.Reannotate
 import DDC.Core.Transform.Rewrite.Rule  hiding (Error)
 import DDC.Core.Transform.Rewrite.Parser
@@ -69,18 +70,27 @@
      = do r' <- checkRewriteRule config kinds' types' r
           return (show n, reannotate (const ()) r')
 
-    config   = C.configOfProfile (fragmentProfile fragment)
-    kinds    = profilePrimKinds  (fragmentProfile fragment)
-    types    = profilePrimTypes  (fragmentProfile fragment)
+    config      = C.configOfProfile (fragmentProfile fragment)
+    kinds       = profilePrimKinds  (fragmentProfile fragment)
+    types       = profilePrimTypes  (fragmentProfile fragment)
 
-    kindsImp = moduleKindEnv modu
-    typesImp = moduleTypeEnv modu
+    kindsImp    = moduleKindEnv modu
+    typesImp    = moduleTypeEnv modu
 
-    kindsExp = modulesGetBinds $ moduleExportKinds modu
-    typesExp = modulesGetBinds $ moduleExportTypes modu
+    kindsExp    = Env.fromList 
+                $ [BName n t | (n, Just t) <- map (liftSnd takeTypeOfExportSource)
+                                           $  moduleExportTypes  modu ]
+    
+    typesExp    = Env.fromList
+                $ [BName n t | (n, Just t) <- map (liftSnd takeTypeOfExportSource)
+                                           $  moduleExportValues modu ]
 
+    liftSnd f (x, y) = (x, f y)
+
     -- Final kind and type environments
-    kinds'	 = kinds `Env.union` kindsImp `Env.union` kindsExp
-    types'	 = types `Env.union` typesImp `Env.union` typesExp
+    kinds'	= kinds `Env.union` kindsImp `Env.union` kindsExp
+    types'	= types `Env.union` typesImp `Env.union` typesExp
 
     source'  = nameOfSource source
+
+
diff --git a/DDC/Driver/Command/Tetra/Boxing.hs b/DDC/Driver/Command/Tetra/Boxing.hs
new file mode 100644
--- /dev/null
+++ b/DDC/Driver/Command/Tetra/Boxing.hs
@@ -0,0 +1,40 @@
+
+module DDC.Driver.Command.Tetra.Boxing
+        (cmdTetraBoxing)
+where
+import DDC.Driver.Stage
+import DDC.Driver.Config
+import DDC.Interface.Source
+import DDC.Build.Pipeline
+import Control.Monad.Trans.Error
+import Control.Monad.IO.Class
+import qualified DDC.Core.Check                 as C
+import qualified DDC.Base.Pretty                as P
+import qualified DDC.Build.Language.Tetra       as Tetra
+
+
+-- | Prepare a Disciple Core Tetra module for lowering.
+cmdTetraBoxing
+        :: Config               -- ^ Driver config.
+        -> Source               -- ^ Source of the code.
+        -> String               -- ^ Program module text.
+        -> ErrorT String IO ()
+
+cmdTetraBoxing config source sourceText
+ = let  pmode   = prettyModeOfConfig $ configPretty config
+        
+        pipeBoxing
+         = pipeText     (nameOfSource source) 
+                        (lineStartOfSource source) sourceText
+         $ PipeTextLoadCore Tetra.fragment C.Recon SinkDiscard
+         [ PipeCoreAsTetra
+         [ PipeTetraBoxing
+         [ PipeCoreCheck  Tetra.fragment C.Recon SinkDiscard
+         [ PipeCoreOutput pmode SinkStdout ]]]]
+   in do
+        errs    <- liftIO pipeBoxing
+        case errs of
+         []     -> return ()
+         es     -> throwError $ P.renderIndent $ P.vcat $ map P.ppr es
+
+
diff --git a/DDC/Driver/Command/ToC.hs b/DDC/Driver/Command/ToC.hs
--- a/DDC/Driver/Command/ToC.hs
+++ b/DDC/Driver/Command/ToC.hs
@@ -1,70 +1,181 @@
 
 module DDC.Driver.Command.ToC
-        (cmdToC)
+        ( cmdToSeaFromFile
+        , cmdToSeaSourceTetraFromFile
+        , cmdToSeaSourceTetraFromString
+        , cmdToSeaCoreFromFile
+        , cmdToSeaCoreFromString)
 where
 import DDC.Driver.Stage
 import DDC.Interface.Source
 import DDC.Build.Pipeline
 import DDC.Build.Language
 import DDC.Core.Fragment
+import DDC.Base.Pretty
 import System.FilePath
+import System.Directory
 import Control.Monad.Trans.Error
 import Control.Monad.IO.Class
-import qualified DDC.Build.Language.Salt        as Salt
-import qualified DDC.Build.Language.Lite        as Lite
-import qualified DDC.Base.Pretty                as P
 
+import Control.Monad
 
--- | Parse, check, and convert a module to C.
+
+-------------------------------------------------------------------------------
+-- | Convert a module to C.
+--   The output is printed to @stdout@.
+--   Any errors are thrown in the `ErrorT` monad.
 --
+cmdToSeaFromFile
+        :: Config               -- ^ Driver config.
+        -> FilePath             -- ^ Core language definition.
+        -> ErrorT String IO ()
+
+cmdToSeaFromFile config filePath
+ 
+ -- Convert a Disciple Source Tetra module.
+ | ".dst"         <- takeExtension filePath
+ =      cmdToSeaSourceTetraFromFile config filePath
+
+ -- Convert a module in some fragment of Disciple Core.
+ | Just language  <- languageOfExtension (takeExtension filePath)
+ =      cmdToSeaCoreFromFile config language filePath
+
+ -- Don't know how to convert this file.
+ | otherwise
+ = let  ext     = takeExtension filePath
+   in   throwError $ "Cannot convert '" ++ ext ++ "' files to C."
+
+
+-------------------------------------------------------------------------------
+-- | Convert Disciple Source Tetra to C.
+--   The result is printed to @stdout@.
+--   Any errors are thrown in the `ErrorT` monad.
+cmdToSeaSourceTetraFromFile
+        :: Config               -- ^ Driver config.
+        -> FilePath             -- ^ Module file path.
+        -> ErrorT String IO ()
+
+cmdToSeaSourceTetraFromFile config filePath
+ = do
+        -- Check that the file exists.
+        exists  <- liftIO $ doesFileExist filePath
+        when (not exists)
+         $ throwError $ "No such file " ++ show filePath
+
+        -- Read in the source file.
+        src     <- liftIO $ readFile filePath
+
+        cmdToSeaSourceTetraFromString config (SourceFile filePath) src
+
+
+-------------------------------------------------------------------------------
+-- | Convert Disciple Source Tetra to C.
+--   The result is printed to @stdout@.
+--   Any errors are thrown in the `ErrorT` monad.
+cmdToSeaSourceTetraFromString
+        :: Config               -- ^ Driver config.
+        -> Source               -- ^ Source of the code.
+        -> String               -- ^ Program module text.
+        -> ErrorT String IO ()
+
+cmdToSeaSourceTetraFromString config source str
+ = let  
+        pipeLoad
+         = pipeText (nameOfSource source) (lineStartOfSource source) str
+         $ stageSourceTetraLoad config source
+         [ PipeCoreReannotate (const ())
+         [ stageTetraToSalt   config source 
+         [ stageSaltOpt       config source
+         [ stageSaltToC       config source SinkStdout]]]]
+         
+   in do
+        errs    <- liftIO pipeLoad
+        case errs of
+         []     -> return ()
+         es     -> throwError $ renderIndent $ vcat $ map ppr es
+
+
+-------------------------------------------------------------------------------
+-- | Parse, check and convert a Core module to Sea.
+--   Works for the 'Tetra', 'Lite' and 'Salt' fragments.
+--   The result is printed to @stdout@.
+--   Any errors are thrown in the `ErrorT` monad.
+--
+cmdToSeaCoreFromFile
+        :: Config               -- ^ Driver config.
+        -> Language             -- ^ Core language definition.
+        -> FilePath             -- ^ Module file path.
+        -> ErrorT String IO ()
+
+cmdToSeaCoreFromFile config language filePath
+ = do
+        -- Check that the file exists.
+        exists  <- liftIO $ doesFileExist filePath
+        when (not exists)
+         $ throwError $ "No such file " ++ show filePath
+
+        -- Read in the source file.
+        src     <- liftIO $ readFile filePath
+
+        cmdToSeaCoreFromString config language (SourceFile filePath) src
+
+
+-------------------------------------------------------------------------------
+-- | Parse, check, and convert a module to C.
 --   The output is printed to @stdout@. 
+--   Any errors are thrown in the `ErrorT` monad.
 --
-cmdToC  :: Config       -- ^ Compiler configuration.
+cmdToSeaCoreFromString  
+        :: Config       -- ^ Compiler configuration.
         -> Language     -- ^ Language definition.
         -> Source       -- ^ Source of the code.
         -> String       -- ^ Program module text.
         -> ErrorT String IO ()
 
-cmdToC config language source sourceText
+cmdToSeaCoreFromString config language source str
  | Language bundle      <- language
  , fragment             <- bundleFragment  bundle
  , profile              <- fragmentProfile fragment
  = do   
         let fragName = profileName profile
-        let mSuffix  = case source of 
-                        SourceFile filePath     -> Just $ takeExtension filePath
-                        _                       -> Nothing
-
+        
         -- Decide what to do based on file extension and current fragment.
         let compile
-                -- Compile a Core Lite module.
-                | fragName == "Lite" || mSuffix == Just ".dcl"
+                -- Convert a Core Tetra module to C.
+                | fragName == "Tetra"
                 = liftIO
-                $ pipeText (nameOfSource source) (lineStartOfSource source) sourceText
-                $ PipeTextLoadCore Lite.fragment
-                [ PipeCoreReannotate (const ())
-                [ stageLiteOpt     config source 
-                [ stageLiteToSalt  config source 
-                [ stageSaltOpt     config source
-                [ stageSaltToC     config source SinkStdout]]]]]
+                $ pipeText (nameOfSource source) (lineStartOfSource source) str
+                $ stageTetraLoad     config source
+                [ stageTetraToSalt   config source
+                [ stageSaltOpt       config source
+                [ stageSaltToC       config source SinkStdout]]]
+                
+                -- Convert a Core Lite module to C.
+                | fragName == "Lite"
+                = liftIO
+                $ pipeText (nameOfSource source) (lineStartOfSource source) str
+                $ stageLiteLoad      config source
+                [ stageLiteOpt       config source 
+                [ stageLiteToSalt    config source 
+                [ stageSaltOpt       config source
+                [ stageSaltToC       config source SinkStdout]]]]
 
-                -- Compile a Core Salt module.
-                | fragName == "Salt" || mSuffix == Just ".dcs"
+                -- Convert a Core Lite module to Salt.
+                | fragName == "Salt"
                 = liftIO
-                $ pipeText (nameOfSource source) (lineStartOfSource source) sourceText
-                $ PipeTextLoadCore Salt.fragment
-                [ PipeCoreReannotate (const ())
-                [ stageSaltOpt     config source
-                [ stageSaltToC     config source SinkStdout]]]
+                $ pipeText (nameOfSource source) (lineStartOfSource source) str
+                $ stageSaltLoad      config source
+                [ stageSaltOpt       config source
+                [ stageSaltToC       config source SinkStdout]]
 
                 -- Unrecognised.
                 | otherwise
-                = throwError "Don't know how to convert this to C"
+                = throwError $ "Cannot convert '" ++ fragName ++ "'modules to C."
 
 
         -- Throw any errors that arose during compilation
         errs <- compile
         case errs of
          []     -> return ()
-         es     -> throwError $ P.renderIndent $ P.vcat $ map P.ppr es
+         es     -> throwError $ renderIndent $ vcat $ map ppr es
 
diff --git a/DDC/Driver/Command/ToLlvm.hs b/DDC/Driver/Command/ToLlvm.hs
--- a/DDC/Driver/Command/ToLlvm.hs
+++ b/DDC/Driver/Command/ToLlvm.hs
@@ -1,70 +1,184 @@
 
 module DDC.Driver.Command.ToLlvm
-        (cmdToLlvm)
+        ( cmdToLlvmFromFile
+        , cmdToLlvmSourceTetraFromFile
+        , cmdToLlvmSourceTetraFromString
+        , cmdToLlvmCoreFromFile
+        , cmdToLlvmCoreFromString)
 where
 import DDC.Driver.Stage
 import DDC.Interface.Source
 import DDC.Build.Pipeline
 import DDC.Build.Language
 import DDC.Core.Fragment
+import DDC.Base.Pretty
+import System.Directory
 import System.FilePath
 import Control.Monad.Trans.Error
 import Control.Monad.IO.Class
-import qualified DDC.Build.Language.Salt        as Salt
-import qualified DDC.Build.Language.Lite        as Lite
-import qualified DDC.Base.Pretty                as P
+import Control.Monad
 
 
--- | Parse, check and convert a  module to LLVM.
+-------------------------------------------------------------------------------
+-- | Convert a module to LLVM.
+--   The output is printed to @stdout@.
+--   Any errors are thrown in the `ErrorT` monad.
 --
---   The output is printed to @stdout@. 
+cmdToLlvmFromFile
+        :: Config               -- ^ Driver config.
+        -> FilePath             -- ^ Core language definition.
+        -> ErrorT String IO ()
+
+cmdToLlvmFromFile config filePath
+ 
+ -- Convert a Disciple Source Tetra module.
+ | ".dst"         <- takeExtension filePath
+ =      cmdToLlvmSourceTetraFromFile config filePath
+
+ -- Convert a module in some fragment of Disciple Core.
+ | Just language  <- languageOfExtension (takeExtension filePath)
+ =      cmdToLlvmCoreFromFile config language filePath
+
+ -- Don't know how to convert this file.
+ | otherwise
+ = let  ext     = takeExtension filePath
+   in   throwError $ "Cannot convert '" ++ ext ++ "' files to LLVM."
+
+
+-------------------------------------------------------------------------------
+-- | Convert Disciple Source Tetra to LLVM.
+--   The result is printed to @stdout@.
+--   Any errors are thrown in the `ErrorT` monad.
+cmdToLlvmSourceTetraFromFile
+        :: Config               -- ^ Driver config.
+        -> FilePath             -- ^ Module file path.
+        -> ErrorT String IO ()
+
+cmdToLlvmSourceTetraFromFile config filePath
+ = do
+        -- Check that the file exists.
+        exists  <- liftIO $ doesFileExist filePath
+        when (not exists)
+         $ throwError $ "No such file " ++ show filePath
+
+        -- Read in the source file.
+        src     <- liftIO $ readFile filePath
+
+        cmdToLlvmSourceTetraFromString config (SourceFile filePath) src
+
+
+-------------------------------------------------------------------------------
+-- | Convert Disciple Source Tetra to LLVM.
+--   The result is printed to @stdout@.
+--   Any errors are thrown in the `ErrorT` monad.
+cmdToLlvmSourceTetraFromString
+        :: Config               -- ^ Driver config.
+        -> Source               -- ^ Source of the code.
+        -> String               -- ^ Program module text.
+        -> ErrorT String IO ()
+
+cmdToLlvmSourceTetraFromString config source str
+ = let  
+        pipeLoad
+         = pipeText (nameOfSource source) (lineStartOfSource source) str
+         $ stageSourceTetraLoad config source
+         [ PipeCoreReannotate (const ())
+         [ stageTetraToSalt     config source 
+         [ stageSaltOpt         config source
+         [ stageSaltToLLVM      config source
+         [ PipeLlvmPrint SinkStdout]]]]]
+   
+   in do
+        errs    <- liftIO pipeLoad
+        case errs of
+         []     -> return ()
+         es     -> throwError $ renderIndent $ vcat $ map ppr es
+
+
+-------------------------------------------------------------------------------
+-- | Parse, check and convert a Core module to LLVM.
+--   Works for the 'Tetra', 'Lite' and 'Salt' fragments.
+--   The result is printed to @stdout@.
+--   Any errors are thrown in the `ErrorT` monad.
 --
-cmdToLlvm 
-        :: Config       -- ^ Compiler configuration.
-        -> Language     -- ^ Language definition.
-        -> Source       -- ^ Source of the code.
-        -> String       -- ^ Program module text.
+cmdToLlvmCoreFromFile
+        :: Config               -- ^ Driver config.
+        -> Language             -- ^ Core language definition.
+        -> FilePath             -- ^ Module file path.
         -> ErrorT String IO ()
 
-cmdToLlvm config language source sourceText
+cmdToLlvmCoreFromFile config language filePath
+ = do
+        -- Check that the file exists.
+        exists  <- liftIO $ doesFileExist filePath
+        when (not exists)
+         $ throwError $ "No such file " ++ show filePath
+
+        -- Read in the source file.
+        src     <- liftIO $ readFile filePath
+
+        cmdToLlvmCoreFromString config language (SourceFile filePath) src
+
+
+-------------------------------------------------------------------------------
+-- | Parse, check and convert a Core module to LLVM.
+--   Works for the 'Tetra', 'Lite' and 'Salt' fragments.
+--   The result is printed to @stdout@.
+--   Any errors are thrown in the `ErrorT` monad.
+--
+cmdToLlvmCoreFromString
+        :: Config               -- ^ Driver config.
+        -> Language             -- ^ Language definition.
+        -> Source               -- ^ Source of the code.
+        -> String               -- ^ Program module text.
+        -> ErrorT String IO ()
+
+cmdToLlvmCoreFromString config language source str
  | Language bundle      <- language
  , fragment             <- bundleFragment  bundle
  , profile              <- fragmentProfile fragment
- = do   let fragName = profileName profile
-        let mSuffix  = case source of 
-                        SourceFile filePath     -> Just $ takeExtension filePath
-                        _                       -> Nothing
-
+ = do   
+        -- Language fragment name.
+        let fragName = profileName profile
+        
         -- Decide what to do based on file extension and current fragment.
         let compile
-                -- Compile a Core Lite module.
-                | fragName == "Lite" || mSuffix == Just ".dcl"
+                -- Convert a Core Tetra module to LLVM.
+                | fragName == "Tetra"
                 = liftIO
-                $ pipeText (nameOfSource source) (lineStartOfSource source) sourceText
-                $ PipeTextLoadCore Lite.fragment
-                [ PipeCoreReannotate (const ())
-                [ stageLiteOpt     config source
-                [ stageLiteToSalt  config source
-                [ stageSaltOpt     config source
-                [ stageSaltToLLVM  config source 
-                [ PipeLlvmPrint SinkStdout]]]]]]
+                $ pipeText (nameOfSource source) (lineStartOfSource source) str
+                $ stageTetraLoad     config source
+                [ stageTetraToSalt   config source
+                [ stageSaltOpt       config source
+                [ stageSaltToLLVM    config source
+                [ PipeLlvmPrint      SinkStdout]]]]
 
-                -- Compile a Core Salt module.
-                | fragName == "Salt" || mSuffix == Just ".dcs"
+                -- Convert a Core Lite module to LLVM.
+                | fragName == "Lite"
                 = liftIO
-                $ pipeText (nameOfSource source) (lineStartOfSource source) sourceText
-                $ PipeTextLoadCore Salt.fragment
-                [ PipeCoreReannotate (const ())
-                [ stageSaltOpt     config source
-                [ stageSaltToLLVM  config source
-                [ PipeLlvmPrint SinkStdout]]]]
+                $ pipeText (nameOfSource source) (lineStartOfSource source) str
+                $ stageLiteLoad      config source
+                [ stageLiteOpt       config source
+                [ stageLiteToSalt    config source
+                [ stageSaltOpt       config source
+                [ stageSaltToLLVM    config source 
+                [ PipeLlvmPrint SinkStdout]]]]]
 
+                -- Convert a Core Salt module to LLVM.
+                | fragName == "Salt"
+                = liftIO
+                $ pipeText (nameOfSource source) (lineStartOfSource source) str
+                $ stageSaltLoad      config source
+                [ stageSaltOpt       config source
+                [ stageSaltToLLVM    config source
+                [ PipeLlvmPrint      SinkStdout]]]
+
                 -- Unrecognised.
                 | otherwise
-                = throwError $ "Don't know how to convert this to LLVM"
+                = throwError $ "Cannot convert '" ++ fragName ++ "' modules to LLVM."
 
         -- Throw any errors that arose during compilation
         errs <- compile
         case errs of
          []     -> return ()
-         es     -> throwError $ P.renderIndent $ P.vcat $ map P.ppr es
+         es     -> throwError $ renderIndent $ vcat $ map ppr es
diff --git a/DDC/Driver/Command/ToSalt.hs b/DDC/Driver/Command/ToSalt.hs
--- a/DDC/Driver/Command/ToSalt.hs
+++ b/DDC/Driver/Command/ToSalt.hs
@@ -1,76 +1,186 @@
 
 module DDC.Driver.Command.ToSalt
-        (cmdToSalt)
+        ( cmdToSaltFromFile
+        , cmdToSaltSourceTetraFromFile
+        , cmdToSaltSourceTetraFromString
+        , cmdToSaltCoreFromFile
+        , cmdToSaltCoreFromString)
 where
 import DDC.Driver.Stage
+import DDC.Driver.Config
 import DDC.Interface.Source
 import DDC.Build.Pipeline
 import DDC.Build.Language
 import DDC.Core.Fragment
-import DDC.Core.Module
-import DDC.Data.Canned
+import DDC.Base.Pretty
 import System.FilePath
+import System.Directory
 import Control.Monad.Trans.Error
 import Control.Monad.IO.Class
+import Control.Monad
 import qualified DDC.Build.Language.Salt        as Salt
-import qualified DDC.Build.Language.Lite        as Lite
-import qualified DDC.Base.Pretty                as P
-import qualified Data.Map                       as Map
+import qualified DDC.Core.Check                 as C
 
 
--- | Parse, check, and fully evaluate an expression.
---
+-------------------------------------------------------------------------------
+-- | Convert a module to Core Salt.
 --   The output is printed to @stdout@.
----
---   The Core -> Salt conversion only accepts A-normalised programs,
---   so we normalize it along the way.
+--   Any errors are thrown in the `ErrorT` monad.
 --
-cmdToSalt 
-        :: Config       -- ^ Compiler configuration.
-        -> Language     -- ^ Language definition.
-        -> Source       -- ^ Source of the code.
-        -> String       -- ^ Program module text.
+cmdToSaltFromFile
+        :: Config               -- ^ Driver config.
+        -> FilePath             -- ^ Module file path.
         -> ErrorT String IO ()
 
-cmdToSalt config language source sourceText
+cmdToSaltFromFile config filePath
+
+ -- Convert a Disciple Source Tetra module.
+ | ".dst"        <- takeExtension filePath
+ =      cmdToSaltSourceTetraFromFile config filePath
+ 
+ -- Convert a module in some fragment of Disciple Core.
+ | Just language <- languageOfExtension (takeExtension filePath)
+ =      cmdToSaltCoreFromFile config language filePath
+
+ -- Don't know how to convert this file.
+ | otherwise
+ = let  ext     = takeExtension filePath
+   in   throwError $ "Cannot convert '" ++ ext ++ "' files to Salt."
+
+
+-------------------------------------------------------------------------------
+-- | Convert Disciple Core Tetra to Disciple Core Salt.
+--   The result is printed to @stdout@.
+--   Any errors are thrown in the `ErrorT` monad.
+cmdToSaltSourceTetraFromFile
+        :: Config               -- ^ Driver config.
+        -> FilePath             -- ^ Module file path.
+        -> ErrorT String IO ()
+
+cmdToSaltSourceTetraFromFile config filePath
+ = do
+        -- Check that the file exists.
+        exists  <- liftIO $ doesFileExist filePath
+        when (not exists)
+         $ throwError $ "No such file " ++ show filePath
+
+        -- Read in the source file.
+        src     <- liftIO $ readFile filePath
+
+        cmdToSaltSourceTetraFromString config (SourceFile filePath) src
+
+
+-------------------------------------------------------------------------------
+-- | Convert Disciple Source Tetra to Disciple Core Salt.
+--   The result is printed to @stdout@.
+--   Any errors are thrown in the `ErrorT` monad.
+cmdToSaltSourceTetraFromString
+        :: Config               -- ^ Driver config.
+        -> Source               -- ^ Source of the code.
+        -> String               -- ^ Program module text.
+        -> ErrorT String IO ()
+
+cmdToSaltSourceTetraFromString config source str
+ = let  
+        pmode   = prettyModeOfConfig $ configPretty config
+
+        pipeLoad
+         = pipeText (nameOfSource source)
+                    (lineStartOfSource source) str
+         $ stageSourceTetraLoad config source
+         [ PipeCoreReannotate (const ())
+         [ stageTetraToSalt     config source 
+         [ stageSaltOpt         config source
+         [ PipeCoreCheck        Salt.fragment C.Recon SinkDiscard
+         [ PipeCoreOutput pmode SinkStdout ]]]]]
+
+   in do
+        errs    <- liftIO pipeLoad
+        case errs of
+         []     -> return ()
+         es     -> throwError $ renderIndent $ vcat $ map ppr es
+
+
+-------------------------------------------------------------------------------
+-- | Convert some fragment of Disciple Core to Core Salt.
+--   Works for the 'Lite' and 'Tetra' fragments.
+--   The result is printed to @stdout@.
+--   Any errors are thrown in the `ErrorT` monad.
+--
+cmdToSaltCoreFromFile
+        :: Config               -- ^ Driver config.
+        -> Language             -- ^ Core language definition.
+        -> FilePath             -- ^ Module file path.
+        -> ErrorT String IO ()  
+
+cmdToSaltCoreFromFile config language filePath
+ = do   
+        -- Check that the file exists.
+        exists  <- liftIO $ doesFileExist filePath
+        when (not exists)
+         $ throwError $ "No such file " ++ show filePath
+
+        -- Read in the source file.
+        src     <- liftIO $ readFile filePath
+
+        cmdToSaltCoreFromString config language (SourceFile filePath) src
+
+
+-------------------------------------------------------------------------------
+-- | Convert some fragment of Disciple Core to Core Salt.
+--   Works for the 'Lite' and 'Tetra' fragments.
+--   The result is printed to @stdout@.
+--   Any errors are thrown in the `ErrorT` monad.
+--
+cmdToSaltCoreFromString
+        :: Config               -- ^ Driver config.
+        -> Language             -- ^ Language definition.
+        -> Source               -- ^ Source of the code.
+        -> String               -- ^ Program module text.
+        -> ErrorT String IO ()
+
+cmdToSaltCoreFromString config language source str
  | Language bundle      <- language
- , fragment             <- bundleFragment  bundle
+ , fragment             <- bundleFragment bundle
  , profile              <- fragmentProfile fragment
- = do   let fragName = profileName profile
-        let mSuffix  = case source of 
-                        SourceFile filePath     -> Just $ takeExtension filePath
-                        _                       -> Nothing
+ = do   
+        -- Language fragment name.
+        let fragName    = profileName profile
 
-        -- Decide what to do based on file extension and current fragment.
+        -- Pretty printer mode.
+        let pmode       = prettyModeOfConfig $ configPretty config
+
+        -- Decide what to do based on the fragment name.
         let compile
-                -- Compile a Core Lite module.
-                | fragName == "Lite" || mSuffix == Just ".dcl"
+                -- Compile a Core Tetra module to Salt.
+                | fragName == "Tetra"
                 = liftIO
-                $ pipeText (nameOfSource source) (lineStartOfSource source) sourceText
-                $ PipeTextLoadCore Lite.fragment
-                [ PipeCoreReannotate (const ())
+                $ pipeText (nameOfSource source) (lineStartOfSource source) str
+                $ stageTetraLoad   config source
+                [ stageTetraToSalt config source
+                [ stageSaltOpt     config source
+                [ PipeCoreCheck    Salt.fragment C.Recon SinkDiscard
+                [ PipeCoreOutput   pmode SinkStdout]]]]
+                
+                -- Convert a Core Lite module to Salt.
+                | fragName == "Lite" 
+                = liftIO
+                $ pipeText (nameOfSource source) (lineStartOfSource source) str
+                $ stageLiteLoad    config source
                 [ stageLiteOpt     config source
                 [ stageLiteToSalt  config source
                 [ stageSaltOpt     config source
-                [ PipeCoreCheck    Salt.fragment
-                [ (if configSuppressCoreImports config
-                        then PipeCoreHacks    (Canned (\x -> return $ eraseImports x))
-                        else PipeCoreId)
-                [ PipeCoreOutput   SinkStdout]]]]]]]
+                [ PipeCoreCheck    Salt.fragment C.Recon SinkDiscard
+                [ PipeCoreOutput   pmode SinkStdout]]]]]
 
-                -- Unrecognised.
+                -- Unrecognised fragment name or file extension.
                 | otherwise
-                = throwError $ "Don't know how to convert this to Salt"
+                = throwError 
+                $ "Cannot convert '" ++ fragName ++ "' modules to Salt."
 
         -- Throw any errors that arose during compilation
         errs <- compile
         case errs of
          []     -> return ()
-         es     -> throwError $ P.renderIndent $ P.vcat $ map P.ppr es
-
+         es     -> throwError $ renderIndent $ vcat $ map ppr es
 
--- | Erase the import list of a module.
-eraseImports :: Module a n -> Module a n
-eraseImports mm
- = mm   { moduleImportKinds     = Map.empty
-        , moduleImportTypes     = Map.empty }
diff --git a/DDC/Driver/Command/Trans.hs b/DDC/Driver/Command/Trans.hs
new file mode 100644
--- /dev/null
+++ b/DDC/Driver/Command/Trans.hs
@@ -0,0 +1,217 @@
+{-# OPTIONS -Werror #-}
+
+module DDC.Driver.Command.Trans
+        ( cmdTransDetect
+        , cmdTransModule
+        , cmdTransExp
+        , cmdTransExpCont
+	, transExp)
+where
+import DDC.Driver.Config
+import DDC.Driver.Output
+import DDC.Driver.Command.Check
+import DDC.Build.Language
+import DDC.Build.Pipeline
+import DDC.Interface.Source
+import DDC.Core.Transform.Reannotate
+import DDC.Core.Load
+import DDC.Core.Fragment
+import DDC.Core.Simplifier
+import DDC.Core.Exp
+import DDC.Core.Compounds
+import DDC.Type.Equiv
+import DDC.Type.Subsumes
+import DDC.Base.Pretty
+import DDC.Core.Module
+import Data.Typeable
+import Control.Monad
+import Control.Monad.Trans.Error
+import Control.Monad.IO.Class
+import DDC.Type.Env                             as Env
+import qualified DDC.Core.Check                 as C
+import qualified Control.Monad.State.Strict     as S
+
+
+-- Detect -----------------------------------------------------------------------------------------
+-- | Load and transform a module or expression, and print the result to @stdout@.
+--  
+--   If the source starts with the 'module' keyword then treat it as one,
+--   otherwise treat it as an expression.
+--
+cmdTransDetect 
+        :: Config               -- ^ Driver config.
+        -> Language             -- ^ Language definition.
+        -> Bool                 -- ^ Print transform info.
+        -> Source               -- ^ Source of the code.
+        -> String               -- ^ Input text.
+        -> ErrorT String IO ()
+
+cmdTransDetect    config language shouldPrintInfo
+        source str
+
+ | "module" : _ <- words str
+ = cmdTransModule config language shouldPrintInfo
+        source str
+
+ | otherwise
+ = cmdTransExp    config language shouldPrintInfo
+        source str
+
+
+-- Module -----------------------------------------------------------------------------------------
+-- | Load and transform a module, and print the result to @stdout@.
+cmdTransModule
+        :: Config               -- ^ Driver config.
+        -> Language             -- ^ Language definition.
+        -> Bool                 -- ^ Print transform info.
+        -> Source               -- ^ Source of the code.
+        -> String               -- ^ Input text.
+        -> ErrorT String IO ()
+
+cmdTransModule config language _shouldPrintInfo source str
+ | Language bundle      <- language
+ , fragment             <- bundleFragment   bundle
+ , simpl                <- bundleSimplifier bundle
+ , zero                 <- bundleStateInit  bundle
+ = let
+        pmode   = prettyModeOfConfig $ configPretty config
+
+        pipeTrans
+         = pipeText (nameOfSource source) (lineStartOfSource source) str
+         $ PipeTextLoadCore fragment 
+                (if configInferTypes config then C.Synth else C.Recon) 
+                SinkDiscard
+         [  PipeCoreReannotate (\a -> a { annotTail = ()})
+         [  PipeCoreSimplify  fragment zero simpl
+         [  PipeCoreCheck     fragment C.Recon SinkDiscard
+         [  PipeCoreOutput    pmode SinkStdout ]]]]
+ 
+    in do
+        errs    <- liftIO pipeTrans 
+        case errs of
+         [] -> return ()
+         es -> throwError $ renderIndent $ vcat $ map ppr es
+
+
+-- Exp --------------------------------------------------------------------------------------------
+-- | Load and transfrom an expression
+--   and print the result to @stdout@.
+cmdTransExp
+        :: Config               -- ^ Driver config.
+        -> Language             -- ^ Source language.
+        -> Bool                 -- ^ Print transform info.
+        -> Source               -- ^ Source of input text.
+        -> String               -- ^ Input text.
+        -> ErrorT String IO ()
+
+cmdTransExp config language traceTrans
+        source str
+ 
+ = liftIO 
+ $ cmdTransExpCont config traceTrans language 
+        (\_ -> return ()) 
+        source str
+
+
+-- Cont -------------------------------------------------------------------------------------------
+-- | Load an expression and apply the current transformation.
+cmdTransExpCont
+        :: Config       -- ^ Driver config.
+        -> Bool 
+        -> Language 
+        -> (forall n. Typeable n
+              => Exp (AnTEC () n) n -> IO ())
+        -> Source 
+        -> String 
+        -> IO ()
+
+cmdTransExpCont _config traceTrans language eatExp source str
+ | Language bundle      <- language
+ , fragment             <- bundleFragment   bundle
+ , modules              <- bundleModules    bundle
+ , simpl                <- bundleSimplifier bundle
+ , zero                 <- bundleStateInit  bundle
+ , profile              <- fragmentProfile  fragment
+ =   cmdParseCheckExp fragment modules Recon False False source str 
+ >>= goStore profile modules zero simpl
+ where
+        -- Expression is well-typed.
+        goStore profile modules zero simpl (Just x, _)
+         = do   let kenv    = modulesExportTypes  modules (profilePrimKinds profile)
+                let tenv    = modulesExportValues modules (profilePrimTypes profile)
+
+                tr      <- transExp traceTrans profile kenv tenv zero simpl 
+                        $  reannotate (\a -> a { annotTail = ()}) x
+		
+                case tr of
+		  Nothing -> return ()
+		  Just x' 
+                   -> do outDocLn $ ppr x'
+                         eatExp x'
+
+        -- Expression had a parse or type error.
+        goStore _ _ _ _ _
+         = do   return ()
+
+
+-- Trans ------------------------------------------------------------------------------------------
+-- | Transform an expression, or display errors
+transExp
+        :: (Eq n, Ord n, Pretty n, Show n)
+        => Bool                         -- ^ Trace transform information.
+        -> Profile n                    -- ^ Language profile.
+        -> KindEnv n                    -- ^ Kind Environment.
+        -> TypeEnv n                    -- ^ Type Environment.
+        -> s
+        -> Simplifier s (AnTEC () n) n
+        -> Exp (AnTEC () n) n
+        -> IO (Maybe (Exp (AnTEC () n) n))
+
+transExp traceTrans profile kenv tenv zero simpl xx
+ = do
+        let annot  = annotOfExp xx
+        let t1     = annotType    annot
+        let eff1   = annotEffect  annot
+        let clo1   = annotClosure annot
+
+         -- Apply the simplifier.
+        let tx          = flip S.evalState zero
+                        $ applySimplifierX profile kenv tenv simpl xx
+        
+        let x'          = reannotate (const ()) $ result tx
+
+        when (traceTrans)
+         $ case (resultInfo tx) of
+           TransformInfo inf
+            -> outDocLn  
+            $  text "* TRANSFORM INFORMATION: " <$> indent 4 (ppr inf) <$> text ""
+
+        -- Check that the simplifier perserved the type of the expression.
+        case fst $ C.checkExp (C.configOfProfile profile) kenv tenv x' Recon of
+          Right (x2, t2, eff2, clo2)
+           |  equivT t1 t2
+           ,  subsumesT kEffect  eff1 eff2
+           ,  subsumesT kClosure clo1 clo2
+           -> do return (Just x2)
+
+           | otherwise
+           -> do outDocLn $ vcat
+                    [ text "* CRASH AND BURN: Transform is not type preserving."
+                    , ppr x'
+                    , text ":: 1 " <+> ppr t1
+                    , text ":: 2 " <+> ppr t2
+                    , text ":!:1 " <+> ppr eff1
+                    , text ":!:2 " <+> ppr eff2
+                    , text ":$:1 " <+> ppr clo1
+                    , text ":$:2 " <+> ppr clo2 ]
+                 return Nothing
+
+          Left err
+           -> do outDocLn $ vcat
+                    [ text "* CRASH AND BURN: Type error in transformed program."
+                    , ppr err
+                    , text "" ]
+
+                 outDocLn $ text "Transformed expression:"
+                 outDocLn $ ppr x'
+                 return Nothing
diff --git a/DDC/Driver/Config.hs b/DDC/Driver/Config.hs
new file mode 100644
--- /dev/null
+++ b/DDC/Driver/Config.hs
@@ -0,0 +1,139 @@
+
+module DDC.Driver.Config
+        ( Config        (..)
+        
+        , ConfigPretty  (..)
+        , defaultConfigPretty
+        , prettyModeOfConfig
+        
+        , ViaBackend    (..))
+where
+import DDC.Build.Builder                        
+import DDC.Core.Simplifier                      (Simplifier)
+import DDC.Core.Pretty
+import DDC.Core.Module
+
+import qualified DDC.Core.Salt.Runtime          as Salt
+import qualified DDC.Core.Salt                  as Salt
+
+import qualified DDC.Core.Lite                  as Lite
+
+
+-- | Configuration for main compiler stages.
+data Config
+        = Config
+        { -- | Dump intermediate code.
+          configDump                    :: Bool
+
+          -- | Use bidirectional type inference on the input code.
+        , configInferTypes              :: Bool
+
+          -- | Simplifiers to apply to intermediate code
+        , configSimplLite               :: Simplifier Int () Lite.Name
+        , configSimplSalt               :: Simplifier Int () Salt.Name
+
+          -- | Backend code generator to use
+        , configViaBackend              :: ViaBackend
+
+          -- | Runtime system configuration
+        , configRuntime                 :: Salt.Config
+
+          -- | The builder to use for the target architecture
+        , configBuilder                 :: Builder
+
+          -- | Core langauge pretty printer configuration.
+        , configPretty                  :: ConfigPretty
+
+          -- | Suppress the #import prelude in C modules
+        , configSuppressHashImports     :: Bool 
+
+          -- | Override output file
+        , configOutputFile              :: Maybe FilePath
+
+          -- | Override directory for build products
+        , configOutputDir               :: Maybe FilePath
+
+          -- | Keep intermediate .ddc.ll files
+        , configKeepLlvmFiles           :: Bool
+
+          -- | Keep intermediate .ddc.c files
+        , configKeepSeaFiles            :: Bool
+
+          -- | Keep intermediate .ddc.s files
+        , configKeepAsmFiles            :: Bool
+
+          -- | Avoid running the type checker where possible.
+          --   When debugging program transformations, use this to get
+          --   the invalid code rather than just the type error message.
+        , configTaintAvoidTypeChecks    :: Bool
+        }
+
+
+-- ConfigPretty ---------------------------------------------------------------
+-- | Core language pretty printer configuration.
+data ConfigPretty
+        = ConfigPretty
+        { configPrettyUseLetCase        :: Bool 
+        , configPrettyVarTypes          :: Bool
+        , configPrettyConTypes          :: Bool
+        , configPrettySuppressImports   :: Bool
+        , configPrettySuppressExports   :: Bool 
+        , configPrettySuppressLetTypes  :: Bool }
+
+
+-- | Default pretty printer configuration.
+defaultConfigPretty :: ConfigPretty
+defaultConfigPretty
+        = ConfigPretty
+        { configPrettyUseLetCase        = False
+        , configPrettyVarTypes          = False
+        , configPrettyConTypes          = False 
+        , configPrettySuppressImports   = False
+        , configPrettySuppressExports   = False
+        , configPrettySuppressLetTypes  = False }
+
+
+-- | Convert a the pretty configuration into the mode to use to print a module.
+--   We keep the 'ConfigPretty' type separate from PrettyMode because the 
+--   former can be non-recursive with other types, and does not need to be
+--   parameterised by the annotation or name types.
+prettyModeOfConfig
+        :: (Eq n, Pretty n) 
+        => ConfigPretty -> PrettyMode (Module a n)
+
+prettyModeOfConfig config
+ = modeModule
+ where
+        modeModule      
+         = PrettyModeModule
+         { modeModuleLets               = modeLets
+         , modeModuleSuppressImports    = configPrettySuppressImports config
+         , modeModuleSuppressExports    = configPrettySuppressExports config }
+
+        modeExp         
+         = PrettyModeExp
+         { modeExpLets                  = modeLets
+         , modeExpAlt                   = modeAlt
+         , modeExpConTypes              = configPrettyConTypes config
+         , modeExpVarTypes              = configPrettyVarTypes config
+         , modeExpUseLetCase            = configPrettyUseLetCase config }
+
+        modeLets        
+         = PrettyModeLets
+         { modeLetsExp                  = modeExp 
+         , modeLetsSuppressTypes        = configPrettySuppressLetTypes config }
+
+        modeAlt
+         = PrettyModeAlt
+         { modeAltExp                   = modeExp }
+        
+
+-- ViaBackend -----------------------------------------------------------------
+data ViaBackend
+        -- | Compile via the C backend.
+        = ViaC
+
+        -- | Compile via the LLVM backend.
+        | ViaLLVM
+        deriving Show
+
diff --git a/DDC/Driver/Dump.hs b/DDC/Driver/Dump.hs
new file mode 100644
--- /dev/null
+++ b/DDC/Driver/Dump.hs
@@ -0,0 +1,30 @@
+
+module DDC.Driver.Dump
+        (dump)
+where
+import DDC.Driver.Config
+import DDC.Interface.Source
+import DDC.Build.Pipeline
+import System.FilePath
+import Data.Maybe
+
+
+-- | If the Dump mode is set 
+--    then produce a SinkFile to write a module to a file, 
+--    otherwise produce SinkDiscard to drop it on the floor.
+dump :: Config -> Source -> String -> Sink
+dump config source dumpFile 
+        | configDump config
+        = let   outputDir
+                 | SourceFile filePath  <- source
+                 = fromMaybe (takeDirectory filePath) 
+                             (configOutputDir config)
+
+                 | otherwise
+                 = fromMaybe "."
+                             (configOutputDir config)
+
+          in    SinkFile $ outputDir </> dumpFile
+
+        | otherwise
+        = SinkDiscard
diff --git a/DDC/Driver/Stage.hs b/DDC/Driver/Stage.hs
--- a/DDC/Driver/Stage.hs
+++ b/DDC/Driver/Stage.hs
@@ -10,9 +10,15 @@
         ( Config        (..)
         , ViaBackend    (..)
 
+          -- * Tetra stages
+        , stageSourceTetraLoad
+        , stageTetraLoad
+        , stageTetraToSalt
+
           -- * Flow stages
         , stageFlowLoad
         , stageFlowPrep
+        , stageFlowRate
         , stageFlowLower
         , stageFlowWind
 
@@ -22,6 +28,7 @@
         , stageLiteToSalt
 
           -- * Salt stages
+        , stageSaltLoad
         , stageSaltOpt
         , stageSaltToC
         , stageSaltToLLVM
@@ -30,368 +37,8 @@
           -- * LLVM stages
         , stageCompileLLVM)
 where
-import DDC.Interface.Source
-import DDC.Build.Builder
-import DDC.Build.Pipeline
-import DDC.Core.Transform.Namify
-import DDC.Core.Simplifier                      (Simplifier)
-import System.FilePath
-import Data.Monoid
-import Data.Maybe
-
-import qualified DDC.Core.Flow                  as Flow
-import qualified DDC.Core.Flow.Profile          as Flow
-import qualified DDC.Build.Language.Flow        as Flow
-
-import qualified DDC.Build.Language.Salt        as Salt
-import qualified DDC.Core.Salt.Runtime          as Salt
-import qualified DDC.Core.Salt.Name             as Salt
-
-import qualified DDC.Build.Language.Lite        as Lite
-import qualified DDC.Core.Lite                  as Lite
-
-import qualified DDC.Core.Check                 as C
-import qualified DDC.Core.Simplifier            as S
-import qualified DDC.Core.Simplifier.Recipe     as S
-import qualified DDC.Core.Transform.Namify      as S
-import qualified DDC.Core.Transform.Snip        as Snip
-
-
--- | Configuration for main compiler stages.
-data Config
-        = Config
-        { -- | Dump intermediate code.
-          configDump                    :: Bool
-
-          -- | Simplifiers to apply to intermediate code
-        , configSimplLite               :: Simplifier Int () Lite.Name
-        , configSimplSalt               :: Simplifier Int () Salt.Name
-
-          -- | Backend code generator to use
-        , configViaBackend              :: ViaBackend
-
-          -- | Runtime system configuration
-        , configRuntime                 :: Salt.Config
-
-          -- | The builder to use for the target architecture
-        , configBuilder                 :: Builder
-
-          -- | Suppress imports in Core modules
-        , configSuppressCoreImports     :: Bool
-
-          -- | Suppress the #import prelude in C modules
-        , configSuppressHashImports     :: Bool 
-
-          -- | Override output file
-        , configOutputFile              :: Maybe FilePath
-
-          -- | Override directory for build products
-        , configOutputDir               :: Maybe FilePath
-
-          -- | Keep intermediate .ddc.ll files
-        , configKeepLlvmFiles           :: Bool
-
-          -- | Keep intermediate .ddc.c files
-        , configKeepSeaFiles            :: Bool
-
-          -- | Keep intermediate .ddc.s files
-        , configKeepAsmFiles            :: Bool
-
-          -- | Avoid running the type checker where possible.
-          --   When debugging program transformations, use this to get
-          --   the invalid code rather than just the type error message.
-        , configTaintAvoidTypeChecks    :: Bool
-        }
-
-
-data ViaBackend
-        -- | Compile via the C backend.
-        = ViaC
-
-        -- | Compile via the LLVM backend.
-        | ViaLLVM
-        deriving Show
-
-
--------------------------------------------------------------------------------
--- | Type check Core Flow.
-stageFlowLoad
-        :: Config -> Source
-        -> [PipeCore () Flow.Name]
-        -> PipeText Flow.Name Flow.Error
-
-stageFlowLoad config source pipesFlow
- = PipeTextLoadCore Flow.fragment
- [ PipeCoreReannotate (const ())
-        ( PipeCoreOutput (dump config source "dump.flow-load.dcf")
-        : pipesFlow ) ]
-
-
--------------------------------------------------------------------------------
--- | Prepare a Core Flow module for lowering.
-stageFlowPrep
-        :: Config -> Source
-        -> [PipeCore () Flow.Name]
-        ->  PipeCore () Flow.Name
-
-stageFlowPrep config source pipesFlow
- = PipeCoreReannotate   (const ())
- [ PipeCoreSimplify     Flow.fragment (0 :: Int) simplNorm
-   [ PipeCoreOutput     (dump config source "dump.flow-prep-norm.dcf")
-   , PipeCoreAsFlow
-     [ PipeFlowPrep
-       ( PipeCoreOutput (dump config source "dump.flow-prep-done.dcf")
-         : pipesFlow)]]]
- 
- where  simplNamify
-         =  S.Trans (S.Namify namifierT namifierX)
-
-        simplNorm
-         =  S.Trans (S.Snip $ Snip.configZero { Snip.configSnipLetBody = True })
-         <> S.flatten 
-         <> simplNamify
-
-        namifierT       = S.makeNamifier Flow.freshT
-        namifierX       = S.makeNamifier Flow.freshX
-
-
--------------------------------------------------------------------------------
--- | Lower a Core Flow module.
---   Is needs to already be prepped,
---   and have full type annotations.
-stageFlowLower
-        :: Config -> Source
-        -> [PipeCore () Flow.Name]
-        ->  PipeCore (C.AnTEC () Flow.Name) Flow.Name
-
-stageFlowLower config source pipesFlow
- = PipeCoreAsFlow
-     [ PipeFlowLower
-       ( PipeCoreOutput    (dump config source "dump.flow-lower.dcf")
-       : pipesFlow ) ]
-
-
--------------------------------------------------------------------------------
--- | Wind loop primops into tail recursive loops in a Core Flow module.
-stageFlowWind
-        :: Config -> Source
-        -> [PipeCore () Flow.Name]
-        ->  PipeCore (C.AnTEC () Flow.Name) Flow.Name
-
-stageFlowWind config source pipesFlow
- = PipeCoreAsFlow
-     [ PipeFlowWind
-       ( PipeCoreOutput    (dump config source "dump.flow-wind.dcf")
-       : pipesFlow ) ]
-
-
--------------------------------------------------------------------------------
--- | Type check Core Lite.
-stageLiteLoad
-        :: Config -> Source
-        -> [PipeCore () Lite.Name]
-        -> PipeText Lite.Name Lite.Error
-
-stageLiteLoad config source pipesLite
- = PipeTextLoadCore Lite.fragment
- [ PipeCoreReannotate (const ())
-        ( PipeCoreOutput (dump config source "dump.lite.dcl")
-        : pipesLite ) ]
-
-
--------------------------------------------------------------------------------
--- | Optimise Core Lite.
-stageLiteOpt 
-        :: Config -> Source
-        -> [PipeCore () Lite.Name]
-        ->  PipeCore () Lite.Name
-
-stageLiteOpt config source pipes
- = PipeCoreSimplify 
-        Lite.fragment
-        (0 :: Int) 
-        (configSimplLite config)
-        ( PipeCoreOutput (dump config source "dump.lite-opt.dcl") 
-        : pipes)
-
-
--------------------------------------------------------------------------------
--- | Optimise Core Salt.
-stageSaltOpt
-        :: Config -> Source
-        -> [PipeCore () Salt.Name]
-        -> PipeCore  () Salt.Name
-
-stageSaltOpt config source pipes
- = PipeCoreSimplify 
-        Salt.fragment
-        (0 :: Int) 
-        (configSimplSalt config)        
-        ( PipeCoreOutput  (dump config source "dump.salt-opt.dcl")
-        : pipes )
-
-
--------------------------------------------------------------------------------
--- | Convert Core Lite to Core Salt.
----
---   The Lite to Salt transform requires the program to be normalised,
---   and have type annotations.
-stageLiteToSalt 
-        :: Config -> Source
-        -> [PipeCore () Salt.Name] 
-        -> PipeCore  () Lite.Name
-
-stageLiteToSalt config source pipesSalt
- = PipeCoreSimplify       Lite.fragment 0 normalizeLite
-   [ PipeCoreCheck        Lite.fragment
-     [ PipeCoreOutput     (dump config source "dump.lite-normalized.dcl")
-     , PipeCoreAsLite
-       [ PipeLiteToSalt   (buildSpec $ configBuilder config) 
-                          (configRuntime config)
-         ( PipeCoreOutput (dump config source "dump.salt.dcs")
-         : pipesSalt)]]]
-           
- where  normalizeLite
-         = S.anormalize
-                (makeNamifier Lite.freshT)      
-                (makeNamifier Lite.freshX)
-
-
--------------------------------------------------------------------------------
--- | Convert Core Salt to C code.
-stageSaltToC
-        :: Config -> Source
-        -> Sink
-        -> PipeCore () Salt.Name
-
-stageSaltToC config source sink
- = PipeCoreSimplify       Salt.fragment 0 normalizeSalt
-   [ PipeCoreCheck        Salt.fragment
-     [ PipeCoreOutput     (dump config source "dump.salt-normalized.dcs")
-     , PipeCoreAsSalt
-       [ PipeSaltTransfer
-         [ PipeSaltOutput (dump config source "dump.salt-transfer.dcs")
-         , PipeSaltPrint
-                (not $ configSuppressHashImports config)
-                (buildSpec $ configBuilder config)
-                sink ]]]]
-
- where  normalizeSalt
-         = S.anormalize (makeNamifier Salt.freshT) 
-                        (makeNamifier Salt.freshX)
-
-
--------------------------------------------------------------------------------
--- | Compile Core Salt via C code.
-stageCompileSalt
-        :: Config -> Source
-        -> FilePath             -- ^ Path of original source file.
-                                --   Build products are placed into the same dir.
-        -> Bool                 -- ^ Should we link this into an executable
-        -> PipeCore () Salt.Name
-
-stageCompileSalt config source filePath shouldLinkExe
- = let  -- Decide where to place the build products.
-        outputDir      = fromMaybe (takeDirectory filePath) (configOutputDir config)
-        outputDirBase  = dropExtension (replaceDirectory filePath outputDir)
-        cPath          = outputDirBase ++ ".ddc.c"
-        oPath          = outputDirBase ++ ".o"
-        exePathDefault = outputDirBase
-        exePath        = fromMaybe exePathDefault (configOutputFile config)
-   in
-        PipeCoreSimplify        Salt.fragment 0 normalizeSalt
-         [ PipeCoreCheck        Salt.fragment
-           [ PipeCoreOutput     (dump config source "dump.salt-normalized.dcs")
-           , PipeCoreAsSalt
-             [ PipeSaltTransfer
-               [ PipeSaltOutput (dump config source "dump.salt-transfer.dcs")
-               , PipeSaltCompile
-                        (buildSpec $ configBuilder config)
-                        (configBuilder config)
-                        cPath
-                        oPath
-                        (if shouldLinkExe 
-                                then Just exePath 
-                                else Nothing) 
-                        (configKeepSeaFiles config)
-                        ]]]]
-
- where  normalizeSalt
-         = S.anormalize (makeNamifier Salt.freshT) 
-                        (makeNamifier Salt.freshX)
-
-
--------------------------------------------------------------------------------
--- | Convert Core Salt to LLVM.
-stageSaltToLLVM
-        :: Config -> Source
-        -> [PipeLlvm]
-        -> PipeCore () Salt.Name
-
-stageSaltToLLVM config source pipesLLVM
- = PipeCoreSimplify Salt.fragment 0 normalizeSalt
-   [ PipeCoreCheck          Salt.fragment
-     [ PipeCoreOutput       (dump config source "dump.salt-normalized.dcs")
-     , PipeCoreAsSalt
-       [ PipeSaltTransfer
-         [ PipeSaltOutput   (dump config source "dump.salt-transfer.dcs")
-         , PipeSaltToLlvm   (buildSpec $ configBuilder config) 
-                            pipesLLVM ]]]]
-
- where  normalizeSalt
-         = S.anormalize (makeNamifier Salt.freshT) 
-                        (makeNamifier Salt.freshX)
-
-
--------------------------------------------------------------------------------
--- | Compile LLVM code.
-stageCompileLLVM 
-        :: Config -> Source
-        -> FilePath             -- ^ Path of original source file.
-                                --   Build products are placed into the same dir.
-        -> Bool                 -- ^ Should we link this into an executable
-        -> PipeLlvm
-
-stageCompileLLVM config _source filePath shouldLinkExe
- = let  -- Decide where to place the build products.
-        outputDir      = fromMaybe (takeDirectory filePath) (configOutputDir config)
-        outputDirBase  = dropExtension (replaceDirectory filePath outputDir)
-        llPath         = outputDirBase ++ ".ddc.ll"
-        sPath          = outputDirBase ++ ".ddc.s"
-        oPath          = outputDirBase ++ ".o"
-        exePathDefault = outputDirBase
-        exePath        = fromMaybe exePathDefault (configOutputFile config)
-   in   -- Make the pipeline for the final compilation.
-        PipeLlvmCompile
-          { pipeBuilder           = configBuilder config
-          , pipeFileLlvm          = llPath
-          , pipeFileAsm           = sPath
-          , pipeFileObject        = oPath
-          , pipeFileExe           = if shouldLinkExe 
-                                        then Just exePath 
-                                        else Nothing 
-          , pipeKeepLlvmFiles     = configKeepLlvmFiles config
-          , pipeKeepAsmFiles      = configKeepAsmFiles  config }
-
-
-------------------------------------------------------------------------------
--- | If the Dump mode is set 
---    then produce a SinkFile to write a module to a file, 
---    otherwise produce SinkDiscard to drop it on the floor.
-dump :: Config -> Source -> String -> Sink
-dump config source dumpFile 
-        | configDump config
-        = let   outputDir
-                 | SourceFile filePath  <- source
-                 = fromMaybe (takeDirectory filePath) 
-                             (configOutputDir config)
-
-                 | otherwise
-                 = fromMaybe "."
-                             (configOutputDir config)
-
-          in    SinkFile $ outputDir </> dumpFile
-
-        | otherwise
-        = SinkDiscard
-
+import DDC.Driver.Config
+import DDC.Driver.Stage.Tetra
+import DDC.Driver.Stage.Flow
+import DDC.Driver.Stage.Lite
+import DDC.Driver.Stage.Salt
diff --git a/DDC/Driver/Stage/Flow.hs b/DDC/Driver/Stage/Flow.hs
new file mode 100644
--- /dev/null
+++ b/DDC/Driver/Stage/Flow.hs
@@ -0,0 +1,98 @@
+
+module DDC.Driver.Stage.Flow
+        ( stageFlowLoad
+        , stageFlowPrep
+        , stageFlowRate
+        , stageFlowLower
+        , stageFlowWind)
+where
+import DDC.Driver.Dump
+import DDC.Driver.Config
+import DDC.Interface.Source
+import DDC.Build.Pipeline
+import DDC.Base.Pretty
+import qualified DDC.Core.Check                 as C
+import qualified DDC.Core.Flow                  as Flow
+import qualified DDC.Build.Language.Flow        as Flow
+
+
+---------------------------------------------------------------------------------------------------
+-- | Type check Core Flow.
+stageFlowLoad
+        :: Config -> Source
+        -> [PipeCore () Flow.Name]
+        -> PipeText Flow.Name Flow.Error
+
+stageFlowLoad config source pipesFlow
+ = PipeTextLoadCore Flow.fragment 
+        (if configInferTypes config then C.Synth else C.Recon)
+                         (dump config source "dump.flow-check.txt")
+   [ PipeCoreReannotate  (const ()) 
+        ( PipeCoreOutput pprDefaultMode
+                         (dump config source "dump.flow-load.dcf")
+        : pipesFlow ) ]
+
+
+---------------------------------------------------------------------------------------------------
+-- | Prepare a Core Flow module for lowering.
+stageFlowPrep
+        :: Config -> Source
+        -> [PipeCore () Flow.Name]
+        ->  PipeCore () Flow.Name
+
+stageFlowPrep config source pipesFlow
+ = PipeCoreReannotate   (const ())
+ [ PipeCoreAsFlow
+   [ PipeFlowPrep
+     ( PipeCoreOutput   pprDefaultMode
+                        (dump config source "dump.flow-prep.dcf")
+     : pipesFlow)]]
+
+
+---------------------------------------------------------------------------------------------------
+-- | Perform rate inference to transform vector operations to series
+stageFlowRate
+        :: Config -> Source
+        -> [PipeCore () Flow.Name]
+        ->  PipeCore () Flow.Name
+
+stageFlowRate config source pipesFlow
+ = PipeCoreReannotate   (const ())
+ [ PipeCoreAsFlow
+   [ PipeFlowRate
+     ( PipeCoreOutput   pprDefaultMode
+                        (dump config source "dump.flow-rate.dcf")
+     : pipesFlow)]]
+ 
+
+---------------------------------------------------------------------------------------------------
+-- | Lower a Core Flow module.
+--   Is needs to already be prepped,
+--   and have full type annotations.
+stageFlowLower
+        :: Config -> Flow.Config -> Source
+        -> [PipeCore () Flow.Name]
+        ->  PipeCore (C.AnTEC () Flow.Name) Flow.Name
+
+stageFlowLower config lowerConfig source pipesFlow 
+ = PipeCoreAsFlow
+     [ PipeFlowLower lowerConfig
+       ( PipeCoreOutput pprDefaultMode
+                        (dump config source "dump.flow-lower.dcf")
+       : pipesFlow ) ]
+
+
+---------------------------------------------------------------------------------------------------
+-- | Wind loop primops into tail recursive loops in a Core Flow module.
+stageFlowWind
+        :: Config -> Source
+        -> [PipeCore () Flow.Name]
+        ->  PipeCore (C.AnTEC () Flow.Name) Flow.Name
+
+stageFlowWind config source pipesFlow
+ = PipeCoreAsFlow
+     [ PipeFlowWind
+       ( PipeCoreOutput pprDefaultMode
+                        (dump config source "dump.flow-wind.dcf")
+       : pipesFlow ) ]
+
diff --git a/DDC/Driver/Stage/Lite.hs b/DDC/Driver/Stage/Lite.hs
new file mode 100644
--- /dev/null
+++ b/DDC/Driver/Stage/Lite.hs
@@ -0,0 +1,79 @@
+
+module DDC.Driver.Stage.Lite
+        ( stageLiteLoad
+        , stageLiteOpt
+        , stageLiteToSalt)
+where
+import DDC.Driver.Dump
+import DDC.Driver.Config
+import DDC.Interface.Source
+import DDC.Build.Builder
+import DDC.Build.Pipeline
+import DDC.Core.Transform.Namify
+import DDC.Base.Pretty
+import qualified DDC.Core.Salt.Name             as Salt
+import qualified DDC.Build.Language.Lite        as Lite
+import qualified DDC.Core.Lite                  as Lite
+import qualified DDC.Core.Check                 as C
+import qualified DDC.Core.Simplifier.Recipe     as S
+
+
+---------------------------------------------------------------------------------------------------
+-- | Load and type check Core Lite.
+stageLiteLoad
+        :: Config -> Source
+        -> [PipeCore () Lite.Name]
+        -> PipeText Lite.Name Lite.Error
+
+stageLiteLoad config source pipesLite
+ = PipeTextLoadCore Lite.fragment
+        C.Recon          (dump config source "dump.lite-check.txt")
+ [ PipeCoreReannotate (const ())
+        ( PipeCoreOutput pprDefaultMode
+                         (dump config source "dump.lite-load.dcl")
+        : pipesLite ) ]
+
+
+---------------------------------------------------------------------------------------------------
+-- | Optimise Core Lite.
+stageLiteOpt 
+        :: Config -> Source
+        -> [PipeCore () Lite.Name]
+        ->  PipeCore () Lite.Name
+
+stageLiteOpt config source pipes
+ = PipeCoreSimplify 
+        Lite.fragment
+        (0 :: Int) 
+        (configSimplLite config)
+        ( PipeCoreOutput pprDefaultMode
+                         (dump config source "dump.lite-opt.dcl") 
+        : pipes)
+
+
+---------------------------------------------------------------------------------------------------
+-- | Convert Core Lite to Core Salt.
+---
+--   The Lite to Salt transform requires the program to be normalised,
+--   and have type annotations.
+stageLiteToSalt 
+        :: Config -> Source
+        -> [PipeCore () Salt.Name] 
+        -> PipeCore  () Lite.Name
+
+stageLiteToSalt config source pipesSalt
+ = PipeCoreSimplify       Lite.fragment 0 normalizeLite
+   [ PipeCoreCheck        Lite.fragment C.Recon SinkDiscard
+     [ PipeCoreOutput     pprDefaultMode
+                          (dump config source "dump.lite-normalized.dcl")
+     , PipeCoreAsLite
+       [ PipeLiteToSalt   (buildSpec $ configBuilder config) 
+                          (configRuntime config)
+         ( PipeCoreOutput pprDefaultMode
+                          (dump config source "dump.salt.dcs")
+         : pipesSalt)]]]
+           
+ where  normalizeLite
+         = S.anormalize
+                (makeNamifier Lite.freshT)      
+                (makeNamifier Lite.freshX)
diff --git a/DDC/Driver/Stage/Salt.hs b/DDC/Driver/Stage/Salt.hs
new file mode 100644
--- /dev/null
+++ b/DDC/Driver/Stage/Salt.hs
@@ -0,0 +1,178 @@
+
+module DDC.Driver.Stage.Salt
+        ( stageSaltLoad
+        , stageSaltOpt
+        , stageSaltToC
+        , stageSaltToLLVM
+        , stageCompileSalt
+        , stageCompileLLVM)
+where
+import DDC.Driver.Dump
+import DDC.Driver.Config
+import DDC.Interface.Source
+import DDC.Build.Builder
+import DDC.Build.Pipeline
+import DDC.Core.Transform.Namify
+import DDC.Base.Pretty
+import System.FilePath
+import Data.Maybe
+import qualified DDC.Build.Language.Salt        as Salt
+import qualified DDC.Core.Salt.Name             as Salt
+import qualified DDC.Core.Salt.Convert          as Salt
+import qualified DDC.Core.Check                 as C
+import qualified DDC.Core.Simplifier.Recipe     as S
+
+
+---------------------------------------------------------------------------------------------------
+-- | Load and type check a Core Salt module.
+stageSaltLoad
+        :: Config -> Source
+        -> [PipeCore () Salt.Name]
+        -> PipeText Salt.Name Salt.Error
+
+stageSaltLoad config source pipesSalt
+ = PipeTextLoadCore Salt.fragment 
+        (if configInferTypes config then C.Synth else C.Recon)
+        SinkDiscard
+ [ PipeCoreReannotate (const ())
+        ( PipeCoreOutput pprDefaultMode
+                         (dump config source "dump.salt-load.dcl")
+        : pipesSalt ) ]
+
+
+---------------------------------------------------------------------------------------------------
+-- | Optimise Core Salt.
+stageSaltOpt
+        :: Config -> Source
+        -> [PipeCore () Salt.Name]
+        -> PipeCore  () Salt.Name
+
+stageSaltOpt config source pipes
+ = PipeCoreSimplify 
+        Salt.fragment
+        (0 :: Int) 
+        (configSimplSalt config)        
+        ( PipeCoreOutput  pprDefaultMode 
+                          (dump config source "dump.salt-opt.dcl")
+        : pipes )
+
+
+---------------------------------------------------------------------------------------------------
+-- | Convert Core Salt to C code.
+stageSaltToC
+        :: Config -> Source
+        -> Sink
+        -> PipeCore () Salt.Name
+
+stageSaltToC config source sink
+ = PipeCoreSimplify       Salt.fragment 0 normalizeSalt
+   [ PipeCoreCheck        Salt.fragment C.Recon SinkDiscard
+     [ PipeCoreOutput     pprDefaultMode
+                          (dump config source "dump.salt-normalized.dcs")
+     , PipeCoreAsSalt
+       [ PipeSaltTransfer
+         [ PipeSaltOutput (dump config source "dump.salt-transfer.dcs")
+         , PipeSaltPrint
+                (not $ configSuppressHashImports config)
+                (buildSpec $ configBuilder config)
+                sink ]]]]
+
+ where  normalizeSalt
+         = S.anormalize (makeNamifier Salt.freshT) 
+                        (makeNamifier Salt.freshX)
+
+
+---------------------------------------------------------------------------------------------------
+-- | Convert Core Salt to LLVM.
+stageSaltToLLVM
+        :: Config -> Source
+        -> [PipeLlvm]
+        -> PipeCore () Salt.Name
+
+stageSaltToLLVM config source pipesLLVM
+ = PipeCoreSimplify Salt.fragment 0 normalizeSalt
+   [ PipeCoreCheck          Salt.fragment C.Recon SinkDiscard
+     [ PipeCoreOutput       pprDefaultMode
+                            (dump config source "dump.salt-normalized.dcs")
+     , PipeCoreAsSalt
+       [ PipeSaltTransfer
+         [ PipeSaltOutput   (dump config source "dump.salt-transfer.dcs")
+         , PipeSaltToLlvm   (buildSpec $ configBuilder config) 
+                            pipesLLVM ]]]]
+
+ where  normalizeSalt
+         = S.anormalize (makeNamifier Salt.freshT) 
+                        (makeNamifier Salt.freshX)
+
+
+---------------------------------------------------------------------------------------------------
+-- | Compile Core Salt via C code.
+stageCompileSalt
+        :: Config -> Source
+        -> FilePath             -- ^ Path of original source file.
+                                --   Build products are placed into the same dir.
+        -> Bool                 -- ^ Should we link this into an executable
+        -> PipeCore () Salt.Name
+
+stageCompileSalt config source filePath shouldLinkExe
+ = let  -- Decide where to place the build products.
+        outputDir      = fromMaybe (takeDirectory filePath) (configOutputDir config)
+        outputDirBase  = dropExtension (replaceDirectory filePath outputDir)
+        cPath          = outputDirBase ++ ".ddc.c"
+        oPath          = outputDirBase ++ ".o"
+        exePathDefault = outputDirBase
+        exePath        = fromMaybe exePathDefault (configOutputFile config)
+   in
+        PipeCoreSimplify        Salt.fragment 0 normalizeSalt
+         [ PipeCoreCheck        Salt.fragment C.Recon SinkDiscard
+           [ PipeCoreOutput     pprDefaultMode
+                                (dump config source "dump.salt-normalized.dcs")
+           , PipeCoreAsSalt
+             [ PipeSaltTransfer
+               [ PipeSaltOutput (dump config source "dump.salt-transfer.dcs")
+               , PipeSaltCompile
+                        (buildSpec $ configBuilder config)
+                        (configBuilder config)
+                        cPath
+                        oPath
+                        (if shouldLinkExe 
+                                then Just exePath 
+                                else Nothing) 
+                        (configKeepSeaFiles config)
+                        ]]]]
+
+ where  normalizeSalt
+         = S.anormalize (makeNamifier Salt.freshT) 
+                        (makeNamifier Salt.freshX)
+
+
+---------------------------------------------------------------------------------------------------
+-- | Compile LLVM code.
+stageCompileLLVM 
+        :: Config -> Source
+        -> FilePath             -- ^ Path of original source file.
+                                --   Build products are placed into the same dir.
+        -> Bool                 -- ^ Should we link this into an executable
+        -> PipeLlvm
+
+stageCompileLLVM config _source filePath shouldLinkExe
+ = let  -- Decide where to place the build products.
+        outputDir      = fromMaybe (takeDirectory filePath) (configOutputDir config)
+        outputDirBase  = dropExtension (replaceDirectory filePath outputDir)
+        llPath         = outputDirBase ++ ".ddc.ll"
+        sPath          = outputDirBase ++ ".ddc.s"
+        oPath          = outputDirBase ++ ".o"
+        exePathDefault = outputDirBase
+        exePath        = fromMaybe exePathDefault (configOutputFile config)
+   in   -- Make the pipeline for the final compilation.
+        PipeLlvmCompile
+          { pipeBuilder           = configBuilder config
+          , pipeFileLlvm          = llPath
+          , pipeFileAsm           = sPath
+          , pipeFileObject        = oPath
+          , pipeFileExe           = if shouldLinkExe 
+                                        then Just exePath 
+                                        else Nothing 
+          , pipeKeepLlvmFiles     = configKeepLlvmFiles config
+          , pipeKeepAsmFiles      = configKeepAsmFiles  config }
+
diff --git a/DDC/Driver/Stage/Tetra.hs b/DDC/Driver/Stage/Tetra.hs
new file mode 100644
--- /dev/null
+++ b/DDC/Driver/Stage/Tetra.hs
@@ -0,0 +1,103 @@
+
+module DDC.Driver.Stage.Tetra
+        ( stageSourceTetraLoad
+        , stageTetraLoad
+        , stageTetraToSalt)
+where
+import DDC.Driver.Dump
+import DDC.Driver.Config
+import DDC.Interface.Source
+import DDC.Build.Pipeline
+import DDC.Base.Pretty
+import qualified DDC.Build.Language.Tetra       as BE
+import qualified DDC.Build.Builder              as B
+import qualified DDC.Core.Tetra                 as CE
+import qualified DDC.Core.Salt                  as CS
+import qualified DDC.Core.Check                 as C
+import qualified DDC.Core.Simplifier.Recipe     as C
+import qualified DDC.Core.Transform.Namify      as C
+import qualified DDC.Base.Parser                as BP
+
+
+---------------------------------------------------------------------------------------------------
+-- | Load and type check a Source Tetra module.
+stageSourceTetraLoad
+        :: Config -> Source
+        -> [PipeCore (C.AnTEC BP.SourcePos CE.Name) CE.Name]
+        -> PipeText CE.Name CE.Error
+
+stageSourceTetraLoad config source pipesTetra
+ = PipeTextLoadSourceTetra
+                    (dump config source "dump.tetra-load-tokens.txt")
+                    (dump config source "dump.tetra-load-raw.dct")
+                    (dump config source "dump.tetra-load-trace.txt")
+   ( PipeCoreOutput pprDefaultMode
+                    (dump config source "dump.tetra-load.dct")
+   : pipesTetra ) 
+
+
+---------------------------------------------------------------------------------------------------
+-- | Load and type check a Core Tetra module.
+stageTetraLoad
+        :: Config -> Source
+        -> [PipeCore () CE.Name]
+        -> PipeText CE.Name CE.Error
+
+stageTetraLoad config source pipesTetra
+ = PipeTextLoadCore BE.fragment 
+        (if configInferTypes config then C.Synth else C.Recon)
+                         (dump config source "dump.tetra-check.dct")
+ [ PipeCoreReannotate (const ())
+        ( PipeCoreOutput pprDefaultMode
+                         (dump config source "dump.tetra-load.dct")
+        : pipesTetra ) ]
+ 
+
+---------------------------------------------------------------------------------------------------
+-- | Convert a Core Tetra module to Core Salt.
+--
+--   This includes performing the Boxing transform.
+---
+--   The Tetra to Salt transform requires the program to be normalised,
+--   and have type annotations.
+stageTetraToSalt 
+        :: Config -> Source
+        -> [PipeCore () CS.Name] 
+        -> PipeCore  () CE.Name
+
+stageTetraToSalt config source pipesSalt
+ = pipe_norm
+ where
+        pipe_norm
+         = PipeCoreSimplify     BE.fragment 0 normalize
+           [ PipeCoreCheck      BE.fragment C.Recon SinkDiscard
+           [ PipeCoreOutput     pprDefaultMode
+                                (dump config source "dump.tetra-normalized.dct")
+           , pipe_boxing ]]
+
+        normalize
+         = C.anormalize
+                (C.makeNamifier CE.freshT)      
+                (C.makeNamifier CE.freshX)
+
+        pipe_boxing
+         = PipeCoreAsTetra      
+           [ PipeTetraBoxing
+             [ PipeCoreOutput     pprDefaultMode
+                                  (dump config source "dump.tetra-boxing-raw.dct")
+             , PipeCoreSimplify   BE.fragment 0 normalize
+               [ PipeCoreOutput   pprDefaultMode
+                                  (dump config source "dump.tetra-boxing-simp.dct")
+               , PipeCoreCheck    BE.fragment C.Recon SinkDiscard
+                 [ PipeCoreOutput pprDefaultMode
+                                  (dump config source "dump.tetra-boxing.dct")
+             , pipe_toSalt]]]]
+
+        pipe_toSalt
+         = PipeCoreAsTetra
+           [ PipeTetraToSalt    (B.buildSpec $ configBuilder config) 
+                                (configRuntime config)
+           ( PipeCoreOutput     pprDefaultMode
+                                (dump config source "dump.salt.dcs")
+           : pipesSalt)]
+           
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,7 +1,7 @@
 --------------------------------------------------------------------------------
 The Disciplined Disciple Compiler License (MIT style)
 
-Copyrite (K) 2007-2013 The Disciplined Disciple Compiler Strike Force
+Copyrite (K) 2007-2014 The Disciplined Disciple Compiler Strike Force
 All rights reversed.
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
@@ -13,18 +13,4 @@
 
 The above copyright notice and this permission notice shall be included in
 all copies or substantial portions of the Software.
-
--------------------------------------------------------------------------------
-Under Australian law copyright is free and automatic.
-By contributing to DDC authors grant all rights they have regarding their
-contributions to the other members of the Disciplined Disciple Compiler Strike
-Force, past, present and future, as well as placing their contributions under
-the above license.
-
-Use "darcs show authors" to get a list of Strike Force members.
-
 --------------------------------------------------------------------------------
-Redistributions of libraries in ./external are governed by their own licenses:
-
-  - TinyPTC   GNU Lesser General Public License
-  
diff --git a/ddc-driver.cabal b/ddc-driver.cabal
--- a/ddc-driver.cabal
+++ b/ddc-driver.cabal
@@ -1,5 +1,5 @@
 Name:           ddc-driver
-Version:        0.3.2.1
+Version:        0.4.1.1
 License:        MIT
 License-file:   LICENSE
 Author:         The Disciplined Disciple Compiler Strike Force
@@ -17,54 +17,67 @@
 
 Library
   Build-depends:
-        base            == 4.6.*,
-        deepseq         == 1.3.*,
-        containers      == 0.5.*,
-        filepath        == 1.3.*,
-        process         == 1.1.*,
-        mtl             == 2.1.*,
-        haskell-src-exts == 1.13.*,
-        directory       == 1.2.*,
-        transformers    == 0.3.*,
-        ddc-base        == 0.3.2.*,
-        ddc-core        == 0.3.2.*,
-        ddc-core-eval   == 0.3.2.*,
-        ddc-core-simpl  == 0.3.2.*,
-        ddc-core-salt   == 0.3.2.*,
-        ddc-core-llvm   == 0.3.2.*,
-        ddc-core-flow   == 0.3.2.*,
-        ddc-build       == 0.3.2.*,
-        ddc-interface   == 0.3.2.*
+        base             >= 4.6 && < 4.8,
+        process          >= 1.1 && < 1.3,
+        deepseq          == 1.3.*,
+        containers       == 0.5.*,
+        filepath         == 1.3.*,
+        mtl              == 2.1.*,
+        directory        == 1.2.*,
+        transformers     == 0.3.*,
+        ddc-base         == 0.4.1.*,
+        ddc-core         == 0.4.1.*,
+        ddc-core-eval    == 0.4.1.*,
+        ddc-core-simpl   == 0.4.1.*,
+        ddc-core-salt    == 0.4.1.*,
+        ddc-core-llvm    == 0.4.1.*,
+        ddc-core-flow    == 0.4.1.*,
+        ddc-core-tetra   == 0.4.1.*,
+        ddc-source-tetra == 0.4.1.*,
+        ddc-build        == 0.4.1.*,
+        ddc-interface    == 0.4.1.*
   
   Exposed-modules:
         DDC.Driver.Command.Flow.Concretize
         DDC.Driver.Command.Flow.Lower
+        DDC.Driver.Command.Flow.Melt
         DDC.Driver.Command.Flow.Prep
+        DDC.Driver.Command.Flow.Rate
         DDC.Driver.Command.Flow.Thread
         DDC.Driver.Command.Flow.Wind
 
-        DDC.Driver.Command.Ast
+        DDC.Driver.Command.Tetra.Boxing
+
         DDC.Driver.Command.BaseBuild
         DDC.Driver.Command.Check
         DDC.Driver.Command.Compile
         DDC.Driver.Command.Load
         DDC.Driver.Command.Make
         DDC.Driver.Command.Parse
+        DDC.Driver.Command.Read
         DDC.Driver.Command.RewriteRules
         DDC.Driver.Command.ToC
         DDC.Driver.Command.ToLlvm
         DDC.Driver.Command.ToSalt
+        DDC.Driver.Command.Trans
 
-        DDC.Driver.Stage
+        DDC.Driver.Stage.Flow
+        DDC.Driver.Stage.Lite
+        DDC.Driver.Stage.Salt
+        DDC.Driver.Stage.Tetra
 
-  Other-modules:
+        DDC.Driver.Config
+        DDC.Driver.Dump
         DDC.Driver.Output
-
+        DDC.Driver.Stage
+      
   Extensions:
         ExistentialQuantification
+        RankNTypes
         PatternGuards
 
   ghc-options:
         -Wall
         -fno-warn-missing-signatures
+        -fno-warn-missing-methods
         -fno-warn-unused-do-bind