diff --git a/Dedukti.hs b/Dedukti.hs
--- a/Dedukti.hs
+++ b/Dedukti.hs
@@ -6,6 +6,7 @@
 -- arguments the appropriate driver is invoked. Everything is coordinated by
 -- the driver. This module is also the place where global configuration data
 -- is initialized.
+
 module Main where
 
 import System.Environment
@@ -15,28 +16,66 @@
 import Dedukti.Driver.Batch
 import Dedukti.Driver.Compile
 import Text.PrettyPrint.Leijen
-import Control.Monad (unless, when)
-import System.Console.GetOpt
+import Data.List (partition, isPrefixOf)
+import Data.Either (partitionEithers)
 import System.Exit
 import System.IO
-import qualified Data.Text.Lazy.Encoding as T
-import qualified Data.Text.Lazy as T
-import qualified Data.ByteString.Lazy as B
+import qualified Data.ByteString.Lazy.Char8 as B
+import qualified Paths_dedukti as Cabal (version)
+import Data.Version
 
 
-data Flag = FlagMake | FlagHelp | FlagVersion | FlagVerbose | FlagVeryVerbose
+data Flag = FlagMake
+          | FlagJobs Int
+          | FlagFormat Config.Format
+          | FlagHelp | FlagVersion
+          | FlagVerbose | FlagVeryVerbose
             deriving (Eq, Ord, Show)
 
-options = [ Option [] ["make"] (NoArg FlagMake)
-                       "Build MODULE and all its dependencies in one go."
-          , Option ['v'] [] (OptArg verb "v")
-                       "Be verbose. -vv to be even more verbose."
-          , Option ['h'] ["help"] (NoArg FlagHelp) "This usage information."
-          , Option [] ["version"] (NoArg FlagVersion) "Output version information then exit." ]
-    where verb Nothing = FlagVerbose
-          verb (Just "v") = FlagVeryVerbose
-          verb _ = error "Unrecognized verbosity level."
+data FlagArity a = Nullary String Flag
+                 | Unary String (String -> Flag)
 
+flagDescriptions =
+  [ ([Nullary "--make" FlagMake],
+     "Build MODULE and all its dependencies in one go.")
+  , ([Unary "-jN" (FlagJobs . read)],
+     "Perform N jobs at once.")
+  , ([Nullary "-fexternal" (FlagFormat Config.External)],
+     "Force recognizing input as (human-readable) external format.")
+  , ([Nullary "-fprefix-notation" (FlagFormat Config.Prefix)],
+     "Force recognizing input as (fast) prefix format.")
+  , ([Unary "-v[v]" $ \arg -> if null arg then FlagVerbose else FlagVeryVerbose],
+     "Be verbose, -vv to be even more verbose.")
+  , (zipWith ($) [Nullary "-h", Nullary "--help"] (repeat FlagHelp),
+     "This usage information.")
+  , ([Nullary "--version" FlagVersion],
+     "Output version information then exit.") ]
+
+-- Flag descriptions obey the following conventions:
+--
+-- - double hyphen flags don't have arguments.
+--
+-- - Everything after the first letter of a hyphen flag is part of the
+--   argument.
+parseCmdline args =
+  let (hyphened, rest) = partition (\arg -> "-" `isPrefixOf` arg) args
+      (errors, flags) = partitionEithers $ map toFlag hyphened
+  in (flags, rest, errors)
+    where flagmap = concatMap fst flagDescriptions
+          unpack ('-':'-':name) = (name, "")
+          unpack ('-':name:arg) = ([name], arg)
+          unpack x = error $ "Malformed argument: " ++ x
+          lookupFlag name arg (Nullary n f : desc)
+              | fst (unpack n) == name =
+                  if null arg
+                  then Right f
+                  else Left $ "No argument expected for flag " ++ n
+          lookupFlag name arg (Unary n f : desc)
+              | fst (unpack n) == name = Right (f arg)
+          lookupFlag name _ [] = Left $ "Flag not found: " ++ name
+          lookupFlag name arg (_:desc) = lookupFlag name arg desc
+          toFlag x | (name, arg) <- unpack x = lookupFlag name arg flagmap
+
 printUsage = do
   self <- parameter Config.imageName
   let header = show $ text "Usage:" <+>
@@ -45,18 +84,22 @@
 
 printHelp = do
   self <- parameter Config.imageName
-  let header = show $ text "Usage:" <+>
+  let header = text "Usage:" <+>
                (text self <+> text "[OPTION]..." <+> text "MODULE")
                <$> text "Options:"
-  io $ putStrLn (usageInfo header options)
+      flags = vsep (map pflag flagDescriptions)
+  io $ putStrLn $ show $ header <$> indent 4 flags
+    where pflag (flags, desc) = fillBreak 14 (hcat $ punctuate (text ", ") $
+                                   map (text . name) flags) <+> text desc
+          name (Nullary n _) = n
+          name (Unary n _) = n
 
 bailout = printUsage >> io exitFailure
 
 printVersion = do
   self <- parameter Config.imageName
-  version <- parameter Config.version
-  io $ B.putStrLn $ T.encodeUtf8 $ T.pack $ flip displayS "" $ renderPretty 0.70 100 $
-     text "Dedukti" <+> text version <> line <> line <>
+  io $ B.putStrLn $ B.pack $ flip displayS "" $ renderPretty 0.70 100 $
+     text "Dedukti" <+> text (showVersion Cabal.version) <> line <> line <>
      text "Copyright (c) 2009 CNRS - École Polytechnique - INRIA." <> line <> line <>
      fillText "You may redistribute copies of Dedukti under the terms of \
               \the GNU General Public License. For more information about \
@@ -65,15 +108,17 @@
 initializeConfiguration = foldr aux Config.defaultConfig
     where aux FlagVerbose c     = c { Config.verbosity = Verbose }
           aux FlagVeryVerbose c = c { Config.verbosity = Debug }
+          aux (FlagFormat f) c  = c { Config.format = Just f }
+          aux (FlagJobs n) c    = c { Config.jobs = n }
           aux _ c               = c
 
 main = do
   args <- getArgs
-  let (opts, files, errs) = getOpt RequireOrder options args
+  let (opts, files, errs) = parseCmdline args
   when (not (null errs)) $ do
-         hPutDoc stderr (vsep (map text errs))
+         hPutDoc stderr (vcat (map text errs) <> line)
          exitFailure
-  runDkM (initializeConfiguration opts) $
+  (`runDkM` initializeConfiguration opts) $
          case undefined of
            _ | FlagHelp `elem` opts -> printHelp
              | FlagVersion `elem` opts -> printVersion
diff --git a/Dedukti/Analysis/Rule.hs b/Dedukti/Analysis/Rule.hs
--- a/Dedukti/Analysis/Rule.hs
+++ b/Dedukti/Analysis/Rule.hs
@@ -1,3 +1,9 @@
+-- |
+-- Copyright : © 2009 CNRS - École Polytechnique - INRIA
+-- License   : GPL
+--
+-- Various checks on rules.
+
 module Dedukti.Analysis.Rule where
 
 import Dedukti.Core
@@ -20,6 +26,7 @@
 
 checkOrdering :: [TyRule Qid a] -> DkM ()
 checkOrdering rules = do
+  say Verbose $ text "Checking rule contiguity ..."
   mapM_ (\x -> when (length x > 1) (throw $ NonContiguousRules (head x))) $
         group $ sort $ map head $ group $ map Rule.headConstant rules
 
diff --git a/Dedukti/Analysis/Scope.hs b/Dedukti/Analysis/Scope.hs
--- a/Dedukti/Analysis/Scope.hs
+++ b/Dedukti/Analysis/Scope.hs
@@ -4,8 +4,7 @@
 --
 -- Check that all occurrences of variables are in scope of their definitions.
 -- Other well-formedness checks can also be found here, such as rejecting
--- duplicate top-level definitions and enforcing contiguity of rule
--- defnitions.
+-- duplicate top-level definitions.
 
 module Dedukti.Analysis.Scope where
 
@@ -15,7 +14,8 @@
 import Dedukti.Pretty ()
 import Dedukti.DkM
 import Data.List (sort, group)
-import qualified Data.Set as Set
+import qualified Data.Map as Map
+import qualified StringTable.AtomSet as AtomSet
 
 
 newtype DuplicateDefinition = DuplicateDefinition Qid
@@ -45,32 +45,46 @@
 
 checkUniqueness :: Module Qid a -> DkM ()
 checkUniqueness (decls, rules) = do
+  say Verbose $ text "Checking that variables only appear once in rule environments ..."
   chk decls
   mapM_ (\(env :@ _) -> chk (env_bindings env)) rules
     where chk bs = mapM_ (\x -> when (length x > 1)
                                 (throw $ DuplicateDefinition (head x))) $
                    group $ sort $ map bind_name bs
 
-checkScopes :: forall a. Show a => Set.Set Qid -> Module Qid a -> DkM ()
+type Context = Map.Map MName AtomSet.AtomSet
+
+-- | Initial environment to pass to 'checkScopes'.
+initContext :: [Qid]                -- ^ declarations from other modules.
+            -> Context
+initContext qids =
+  Map.fromListWith AtomSet.union $ map (\qid -> (qid_qualifier qid, AtomSet.singleton (qid_stem qid))) qids
+
+checkScopes :: forall a. Show a => Context -> Module Qid a -> DkM ()
 checkScopes env (decls, rules) = do
+  say Verbose $ text "Checking that all declarations are well scoped ..."
   topenv <- foldM chkBinding env decls
   mapM_ (chkRule topenv) rules
-    where chkBinding env (x ::: ty) = do
+    where ins qid env = Map.insertWith' AtomSet.union (qid_qualifier qid)
+                        (AtomSet.singleton (qid_stem qid)) env
+          mem qid env = maybe False (AtomSet.notMember (qid_stem qid))
+                        (Map.lookup (qid_qualifier qid) env)
+          chkBinding env (x ::: ty) = do
             chkExpr env ty
-            return $ Set.insert x env
+            return $ ins x env
           chkRule topenv r@(env :@ rule) = do
-            let lhsvars = Set.fromList [ x | Var x _ <- everyone (Rule.head r) ]
-            mapM_ (\x -> when (x `Set.notMember` lhsvars) $
+            let lhsvars = AtomSet.fromList [ qid_stem x | Var x _ <- everyone (Rule.head r) ]
+            mapM_ (\x -> when (qid_stem x `AtomSet.notMember` lhsvars) $
                          throw (IllegalEnvironment x)) (map bind_name $ env_bindings env)
             ruleenv <- foldM chkBinding topenv $ env_bindings env
-            descendM (chkExpr (topenv `Set.union` ruleenv)) rule
+            descendM (chkExpr (Map.unionWith AtomSet.union topenv ruleenv)) rule
           chkExpr env t@(Var x _) = do
-            when (x `Set.notMember` env) (throw $ ScopeError x)
+            when (x `mem` env) (throw $ ScopeError x)
             return (t :: Expr Qid a)
           chkExpr env (Lam (x ::: ty) t _) = do
             chkExpr env ty
-            chkExpr (Set.insert x env) t
+            chkExpr (ins x env) t
           chkExpr env (Pi (x ::: ty) t _)  = do
             chkExpr env ty
-            chkExpr (Set.insert x env) t
+            chkExpr (ins x env) t
           chkExpr env t = descendM (chkExpr env) t
diff --git a/Dedukti/CodeGen.hs b/Dedukti/CodeGen.hs
--- a/Dedukti/CodeGen.hs
+++ b/Dedukti/CodeGen.hs
@@ -3,11 +3,12 @@
 -- License   : GPL
 --
 -- Interface for all code generators.
-module Dedukti.CodeGen (CodeGen(..)) where
 
+module Dedukti.CodeGen where
+
 import Dedukti.Core
 import Dedukti.Module
-import qualified Data.Text.Lazy as T
+import Data.ByteString.Lazy.Char8 (ByteString)
 
 
 class CodeGen o where
@@ -23,4 +24,4 @@
     serialize :: MName   -- ^ The module name
               -> [MName] -- ^ Dependencies
               -> Bundle o -- ^ Code
-              -> T.Text
+              -> ByteString
diff --git a/Dedukti/CodeGen/Exts.hs b/Dedukti/CodeGen/Exts.hs
--- a/Dedukti/CodeGen/Exts.hs
+++ b/Dedukti/CodeGen/Exts.hs
@@ -13,13 +13,19 @@
 import Dedukti.Pretty
 import qualified Dedukti.Rule as Rule
 import qualified Language.Haskell.Exts.Syntax as Hs
+import qualified Language.Haskell.Exts.Build as Hs
 import Language.Haskell.Exts.Pretty
-import qualified Data.Text.Lazy as T
+import Language.Haskell.Exts.QQ
+import qualified Data.ByteString.Lazy.Char8 as B
 import Data.Char (toUpper)
+import Data.List (foldl')
 import qualified Data.Stream as Stream
 import Prelude hiding ((*))
 
 
+(*) :: Hs.SrcLoc                -- dummy source location.
+(*) = Hs.SrcLoc "" 0 0
+
 type Em a = a (Id Record) (A Record)
 
 type instance Id Record = Qid
@@ -38,73 +44,68 @@
 
     emit rs@(RS x ty rules) =
         Rec x (length rules) (function rs : def_ty : def_box : zipWith defs_rule [0..] rules)
-        where def_ty  = value (x .$ "ty") (code ty)
-              def_box = value (x .$ "box")
-                                     (primbbox (term ty) (var (x .$ "ty")) (var x))
+        where (tyname, boxname) = (varName (x .$ "ty"), varName (x .$ "box"))
+              def_ty  = [dec| ((tyname)) = $(code ty) |]
+              def_box = [dec| ((boxname)) = bbox $(term ty) $(Hs.var tyname) $(var x) |]
               -- Checking rules involves much of the same work as checking all
               -- declarations at top-level, so let's just call the code
               -- generation functions recursively.
               defs_rule n (env :@ lhs :--> rhs) =
-                  let rec (x ::: ty) rs = (emit (RS x ty []) :: Record) : rs
-                      Bundle decls = coalesce $ foldr rec [ruleCheck] (env_bindings env)
-                  in  Hs.FunBind [Hs.Match (*) (varName (x .$ "rule" .$ T.pack (show n)))
-                                  []
-                                  Nothing
-                                  (Hs.UnGuardedRhs (primitiveVar "main" []))
-                                  (Hs.BDecls decls)]
-                      where ruleCheck = Rec (qid "rule") 0
-                                            [value (qid "rule" .$ "box")
-                                             (primitiveVar "checkRule" [term lhs, term rhs])]
+                  let f (x ::: ty) rs = (emit (RS x ty []) :: Record) : rs
+                      ruleCheck = let rule_box = varName (qid "rule" .$ "box")
+                                  in Rec (qid "rule") 0 [[dec| ((rule_box)) = checkRule $(term lhs) $(term rhs) |]]
+                      Bundle decls = coalesce $ foldr f [ruleCheck] (env_bindings env)
+                      rule = varName (x .$ "rule" .$ B.pack (show n))
+                      body = Hs.letE decls [hs| main |]
+                  in [dec| ((rule)) = $body |]
 
     coalesce records = Bundle $ concatMap rec_code records ++ [main]
-        where main = Hs.FunBind [Hs.Match (*) (Hs.Ident "main") []
-                                       Nothing (Hs.UnGuardedRhs checks) (Hs.BDecls [])]
+        where main = [dec| main = $checks |]
               checks = Hs.Do (concatMap rules records ++ map declaration records)
-              declaration rec = Hs.Qualifier (primitiveVar "checkDeclaration"
-                                              [ Hs.Lit $ Hs.String $ show $ pretty $ unqualify $ rec_name rec
-                                              , var (rec_name rec .$ "box") ])
+              declaration r = let desc = Hs.strE $ show $ pretty $ unqualify $ rec_name r
+                                in Hs.qualStmt [hs| checkDeclaration $desc $(var (rec_name r .$ "box")) |]
               rules (Rec _ 0 _) = []
               rules (Rec x nr _) =
-                  [Hs.Qualifier $ primitiveVar "putStrLn" [Hs.Lit $ Hs.String ("Starting rule " ++ show (pretty (unqualify x)))]] ++
-                  map (\n -> Hs.Qualifier $ var (x .$ "rule" .$ T.pack (show n))) [0..nr-1] ++
-                  [Hs.Qualifier $ primitiveVar "putStrLn" [Hs.Lit $ Hs.String ("Finished rule " ++ show (pretty (unqualify x)))]]
+                let startmsg = Hs.strE $ "Starting rule " ++ show (pretty (unqualify x)) ++ "."
+                    finishmsg = Hs.strE $ "Finished rule " ++ show (pretty (unqualify x)) ++ "."
+                in [Hs.qualStmt [hs| putStrLn $startmsg |]]
+                    ++ map (\n -> Hs.qualStmt $ var (x .$ "rule" .$ B.pack (show n))) [0..nr-1]
+                    ++ [Hs.qualStmt [hs| putStrLn $finishmsg |]]
 
     serialize mod deps (Bundle decls) =
-        T.pack $ prettyPrintWithMode defaultMode {layout = PPInLine} $
+        B.pack $ prettyPrintWithMode defaultMode {layout = PPInLine} $
         Hs.Module (*) (modname mod) [] Nothing Nothing imports decls
         where imports = runtime : map (\m -> Hs.ImportDecl (*) (modname m) True False Nothing Nothing Nothing) deps
               runtime = Hs.ImportDecl (*) (Hs.ModuleName "Dedukti.Runtime") False False Nothing Nothing Nothing
-              modname m = Hs.ModuleName $ T.unpack $ T.intercalate "." $ map capitalize $ toList m
+              modname m = Hs.ModuleName $ B.unpack $ B.intercalate "." $ map capitalize $ toList m
 
 -- | A similar encoding of names as the z-encoding of GHC. Non-letter
 -- characters are escaped with an x.
 xencode :: Qid -> String
 xencode qid =
-    T.unpack $
-     joinQ (qid_qualifier qid) `T.append`
+    B.unpack $
+     joinQ (qid_qualifier qid) `B.append`
      -- Prepend all idents with an x to avoid clash with runtime functions.
-     T.cons 'x' (enc (qid_stem qid)) `T.append`
+     B.cons 'x' (enc $ fromAtom $ qid_stem qid) `B.append`
      joinS (qid_suffix qid)
         where joinQ Root = ""
-              joinQ (h :. x) = joinQ h `T.append` capitalize x `T.append` "."
+              joinQ (h :. x) = joinQ h `B.append` capitalize (fromAtom x) `B.append` "."
               joinS Root = ""
-              joinS (h :. x) = joinS h `T.append` "_" `T.append` x
-              enc = T.concatMap f where
+              joinS (h :. x) = joinS h `B.append` "_" `B.append` fromAtom x
+              enc = B.concatMap f where
                   f 'x'  = "xx"
                   f '\'' = "xq"
                   f '_'  = "xu"
-                  f x | x >= '0', x <= '9' = 'x' `T.cons` T.singleton x
-                      | otherwise = T.singleton x
+                  f x | x >= '0', x <= '9' = 'x' `B.cons` B.singleton x
+                      | otherwise = B.singleton x
 
 function :: Em RuleSet -> Hs.Decl
-function (RS x _ []) =
-    Hs.FunBind [Hs.Match (*) (varName x) [] Nothing (Hs.UnGuardedRhs (primCon x)) (Hs.BDecls [])]
-function (RS x _ rs) =
-    Hs.FunBind [Hs.Match (*) (varName x) [] Nothing (Hs.UnGuardedRhs rhs) (Hs.BDecls [f])]
+function (RS x _ []) = Hs.nameBind (*) (varName x) (constant x)
+function (RS x _ rs) = Hs.sfun (*) (varName x) [] (Hs.UnGuardedRhs rhs) (Hs.binds [f])
     where n = Rule.arity (head rs)
-          rhs = foldr primLam
-                (application (Hs.Var (Hs.UnQual (Hs.Ident "__")) : Stream.take n variables))
-                (Stream.take n pvariables)
+          occs = Stream.take n (Stream.map Hs.var variables)
+          pats = Stream.take n variables
+          rhs = foldr (\x y -> [hs| Lam (\((x)) -> $y) |]) (Hs.metaFunction "__" occs) pats
           f | n > 0     = Hs.FunBind (map clause rs ++ [defaultClause x n])
             | otherwise = Hs.FunBind (map clause rs)
 
@@ -112,120 +113,71 @@
 clause rule =
     let (lrule@(env :@ _ :--> rhs), constraints) = Rule.linearize qids rule
     in if null constraints
-       then Hs.Match (*) (Hs.Ident "__") (map (pattern env) (Rule.patterns lrule))
-            Nothing (Hs.UnGuardedRhs (code rhs)) (Hs.BDecls [])
-       else Hs.Match (*) (Hs.Ident "__") (map (pattern env) (Rule.patterns lrule))
-            Nothing (Hs.GuardedRhss [Hs.GuardedRhs (*) (guards constraints) (code rhs)]) (Hs.BDecls [])
-    where guards constraints =
-              map (\(x, x') -> Hs.Qualifier $
-                   primitiveVar "convertible" [Hs.Lit (Hs.Int 0), var x, var x']) constraints
-          qids = Stream.unfold (\i -> ((qid $ T.pack $ show i) .$ "fresh", i + 1)) 0
+       then Hs.Match (*) (Hs.name "__") (map (pattern env) (Rule.patterns lrule))
+            Nothing (Hs.UnGuardedRhs (code rhs)) Hs.noBinds
+       else Hs.Match (*) (Hs.name "__") (map (pattern env) (Rule.patterns lrule))
+            Nothing (Hs.GuardedRhss [Hs.GuardedRhs (*) (guards constraints) (code rhs)]) Hs.noBinds
+    where guards = map (\(x, x') -> Hs.qualStmt $
+                                    [hs| convertible 0 $(var x) $(var x') |])
+          qids = Stream.unfold (\i -> ((qid $ B.pack $ show i) .$ "fresh", i + 1)) 0
 
 defaultClause :: Id Record -> Int -> Hs.Match
 defaultClause x n =
-    Hs.Match (*) (Hs.Ident "__") (Stream.take n pvariables) Nothing
-          (Hs.UnGuardedRhs (primApps x (Stream.take n variables))) (Hs.BDecls [])
-
-value :: Id Record -> Hs.Exp -> Hs.Decl
-value x rhs =
-    Hs.FunBind [Hs.Match (*) (varName x) [] Nothing (Hs.UnGuardedRhs rhs) (Hs.BDecls [])]
+    Hs.Match (*) (Hs.name "__") (Stream.take n (Stream.map Hs.pvar variables)) Nothing
+          (Hs.UnGuardedRhs (foldl' (\e x -> [hs| App $e $x |]) (constant x) (Stream.take n (Stream.map Hs.var variables)))) Hs.noBinds
 
+constant c = [hs| Con $(Hs.strE $ show $ pretty c) |]
 
 pattern :: Em Env -> Em Expr -> Hs.Pat
-pattern env (Var x _) | x `isin` env = pvar x
+pattern env (Var x _) | x `isin` env = Hs.pvar (varName x)
 pattern env expr = case unapply expr of
                      Var x _ : xs -> primAppsP x (map (pattern env) xs)
 
+-- | Build a pattern matching constant.
+primConP c = Hs.PParen (Hs.pApp (Hs.name "Con") [Hs.strP (show (pretty c))])
+primAppP t1 t2 = Hs.PParen (Hs.pApp (Hs.name "App") [t1, t2])
+primAppsP c = foldl' primAppP (primConP c)
+
 -- | Turn an expression into object code with types erased.
 code :: Em Expr -> Hs.Exp
 code (Var x _)            = var x
-code (Lam (x ::: ty) t _) = primLam (pvar x) (code t)
-code (Lam (Hole ty) t _)  = primLam Hs.PWildCard (code t)
-code (Pi (x ::: ty) t _)  = primPi (code ty) (pvar x) (code t)
-code (Pi (Hole ty) t _)   = primPi (code ty) Hs.PWildCard (code t)
-code (App t1 t2 _)        = primap (code t1) (code t2)
-code Type                 = primType
+code (Lam (x ::: ty) t _) | n <- varName x = [hs| Lam (\((n)) -> $(code t)) |]
+code (Lam (Hole ty) t _)  = [hs| Lam (\_ -> $(code t)) |]
+code (Pi (x ::: ty) t _)  | n <- varName x = [hs| Pi $(code ty) (\((n)) -> $(code t)) |]
+code (Pi (Hole ty) t _)   = [hs| Pi $(code ty) (\_ -> $(code t)) |]
+code (App t1 t2 _)        = [hs| ap $(code t1) $(code t2) |]
+code Type                 = [hs| Type |]
 
 -- | Turn a term into its Haskell representation, including all types.
 term :: Em Expr -> Hs.Exp
 term (Var x _)     = var (x .$ "box")
-term (Lam b t _)   = primTLam b (term t)
-term (Pi b t _)    = primTPi  b (term t)
-term (App t1 t2 _) = primTApp (term t1) (primUBox (term t2) (code t2))
-term Type          = primTType
-term Kind          = primTKind
+term (Lam b t _)   = typedAbstraction [hs| TLam |] b (term t)
+term (Pi b t _)    = typedAbstraction [hs| TPi |] b (term t)
+term (App t1 t2 _) = [hs| TApp $(term t1) (UBox $(term t2) $(code t2)) |]
+term Type          = [hs| TType |]
 
-(*) :: Hs.SrcLoc
-(*) = Hs.SrcLoc "" 0 0
+typedAbstraction c b t =
+    case b of
+      x ::: ty -> [hs| $c $(dom ty) (\((box)) -> $ran) |]
+          where box = varName (x .$ "box")
+                ran = let n = varName x
+                      in [hs| let ((n)) = obj $(Hs.var box) in $t |]
+      Hole ty  -> [hs| $c $(dom ty) (\_ -> $t) |]
+    where dom ty = if isVariable ty
+                   then term ty else [hs| sbox $(term ty) Type $(code ty) |]
 
 varName :: Id Record -> Hs.Name
-varName = Hs.Ident . xencode . unqualify
+varName = Hs.name . xencode . unqualify
 
 -- | Smart variable constructor.
 var :: Id Record -> Hs.Exp
-var = Hs.Var . Hs.UnQual . Hs.Ident . xencode
-
-pvar :: Id Record -> Hs.Pat
-pvar = Hs.PVar . varName
+var = Hs.var . Hs.name . xencode
 
 -- | Produce a set of variables y1, ..., yn
-variables =
-    Stream.unfold (\i -> (Hs.Var $ Hs.UnQual $ Hs.Ident $ ('y':) $ show i, i + 1)) 0
-
-pvariables =
-    Stream.unfold (\i -> (Hs.PVar $ Hs.Ident $ ('y':) $ show i, i + 1)) 0
-
-application :: [Hs.Exp] -> Hs.Exp
-application = foldl1 Hs.App
-
--- Primitives
-
-primitiveVar s [] = Hs.Var $ Hs.UnQual $ Hs.Ident s
-primitiveVar s xs = Hs.Paren $ application $ (Hs.Var $ Hs.UnQual $ Hs.Ident s) : xs
-
-primitiveCon s [] = Hs.Con $ Hs.UnQual $ Hs.Ident s
-primitiveCon s xs = Hs.Paren $ application $ (Hs.Con $ Hs.UnQual $ Hs.Ident s) : xs
-
-primap  t1 t2 = primitiveVar "ap"  [t1, t2]
-primApp t1 t2 = primitiveCon "App" [t1, t2]
-primCon c     = primitiveCon "Con" [Hs.Lit (Hs.String (show (pretty c)))]
-primType      = primitiveCon "Type" []
-
-primLam pat t = primitiveCon "Lam" [Hs.Paren (Hs.Lambda (*) [pat] t)]
-primPi  dom pat range = primitiveCon "Pi" [dom, Hs.Paren (Hs.Lambda (*) [pat] range)]
-
-primApps c = foldl primApp (primCon c)
-
-typedAbstraction c b t =
-    let (pat, ty, ran) =
-            case b of
-              x ::: ty -> ( pvar (x .$ "box")
-                          , ty
-                          , Hs.Let (Hs.BDecls [value x (primobj (var (x .$ "box")))]) t )
-              Hole ty  -> (Hs.PWildCard, ty, t)
-        dom = if isVariable ty
-              then term ty else primsbox (term ty) primType (code ty)
-    in primitiveCon c [dom, Hs.Paren (Hs.Lambda (*) [pat] ran)]
-
-primTLam       = typedAbstraction "TLam"
-primTPi        = typedAbstraction "TPi"
-primTApp t1 t2 = primitiveCon "TApp" [t1, t2]
-primTType      = primitiveCon "TType" []
-primTKind      = primitiveCon "TKind" []
-
-primUBox ty obj_code         = primitiveCon "UBox" [ty, obj_code]
-primbbox ty ty_code obj_code = primitiveVar "bbox" [ty, ty_code, obj_code]
-primsbox ty ty_code obj_code = primitiveVar "sbox" [ty, ty_code, obj_code]
-
-primobj t = primitiveVar "obj" [t]
-
--- | Build a pattern matching a constant.
-primConP c = Hs.PParen $ Hs.PApp (Hs.UnQual $ Hs.Ident "Con") [Hs.PLit (Hs.String (show (pretty c)))]
-primAppP t1 t2 = Hs.PParen $ Hs.PApp (Hs.UnQual $ Hs.Ident "App") [t1, t2]
-primAppsP c = foldl primAppP (primConP c)
+variables = Stream.unfold (\i -> (Hs.name $ ('y':) $ show i, i + 1)) 0
 
 -- | Capitalize a word.
-capitalize :: T.Text -> T.Text
-capitalize s = case T.uncons s of
-             Nothing -> T.empty
-             Just (x, xs) -> toUpper x `T.cons` xs
+capitalize :: B.ByteString -> B.ByteString
+capitalize s = case B.uncons s of
+             Nothing -> B.empty
+             Just (x, xs) -> toUpper x `B.cons` xs
diff --git a/Dedukti/Config.hs b/Dedukti/Config.hs
--- a/Dedukti/Config.hs
+++ b/Dedukti/Config.hs
@@ -6,22 +6,28 @@
 
 module Dedukti.Config where
 
+import System.Environment (getProgName)
+import System.IO.Unsafe (unsafePerformIO)
 
+
 data Verbosity = Quiet | Verbose | Debug
                  deriving (Eq, Ord, Show)
 
+data Format = External | Prefix
+              deriving (Eq, Ord, Show)
+
 data Config = Config
-    { homeDir :: FilePath
-    , imageName :: FilePath
-    , version :: String
+    { imageName :: FilePath
     , hsCompiler :: FilePath
     , verbosity :: Verbosity
+    , format :: Maybe Format    -- ^ @Just format@ if input format is forced.
+    , jobs :: Int               -- ^ Number of simultaneous jobs to run.
     }
 
 defaultConfig =
-    Config { homeDir = "."
-           , imageName = "dedukti"
+    Config { imageName = unsafePerformIO $ getProgName
            , hsCompiler = "ghc"
-           , version = "0.1"
-           , verbosity = Quiet }
+           , verbosity = Quiet
+           , format = Nothing
+           , jobs = 1 }
 
diff --git a/Dedukti/Core.hs b/Dedukti/Core.hs
--- a/Dedukti/Core.hs
+++ b/Dedukti/Core.hs
@@ -16,7 +16,8 @@
     , bind_name, bind_type
     , isAbstraction, isApplication, isVariable, isAtomic, isApplicative
     -- * Environments
-    , emptyEnv, env_bindings, env_domain, env_codomain, (&), (!), isin
+    , emptyEnv, env_bindings, env_domain, env_codomain, (&), (!)
+    , isin, fromBindings
     -- * Annotations
     , Unannot, nann, (%%), (%%%), (<%%>), (<%%%>)
     -- * Smart constructors
@@ -45,8 +46,8 @@
 
 -- | A type decorating a variable, or a type on its own.
 data Binding id a = id ::: Expr id a
-               | Hole (Expr id a)
-                 deriving (Eq, Ord, Show)
+                  | Hole (Expr id a)
+                    deriving (Eq, Ord, Show)
 
 -- | A rewrite rule.
 data Rule id a = Expr id a :--> Expr id a
@@ -186,10 +187,10 @@
 
 class Ord (Id t) => Transform t where
     -- | Effectful bottom-up transformation on terms.
-    transformM :: (Monad m, Ord (Id t)) => (Expr (Id t) (A t) -> m (Expr (Id t) (A t))) -> t -> m t
+    transformM :: Monad m => (Expr (Id t) (A t) -> m (Expr (Id t) (A t))) -> t -> m t
 
     -- | Helper function for top-down transformations.
-    descendM :: (Monad m, Ord (Id t)) => (Expr (Id t) (A t) -> m (Expr (Id t) (A t))) -> t -> m t
+    descendM :: Monad m => (Expr (Id t) (A t) -> m (Expr (Id t) (A t))) -> t -> m t
 
 instance Ord id => Transform (Module id a) where
     transformM f (decls, rules) =
diff --git a/Dedukti/DkM.hs b/Dedukti/DkM.hs
--- a/Dedukti/DkM.hs
+++ b/Dedukti/DkM.hs
@@ -7,15 +7,16 @@
 -- facilities and an interface to the system are also provided.
 
 module Dedukti.DkM ( module Control.Monad
-                  , DkM, runDkM, warn, warnings, say
-                  , Verbosity(..)
-                  , configuration, parameter
-                  , command
-                  -- pretty-printing combinators.
-                  , Pretty(..), text, (<+>), (<>), int
-                  , fillText
-                  , E.Exception(..), Typeable, E.throw, io
-                  , onException) where
+                   , DkM, runDkM, warn, warnings, say
+                   , Verbosity(..)
+                   , configuration, parameter
+                   , command
+                   -- * pretty-printing combinators.
+                   , Pretty(..), text, (<+>), (<>), int
+                   , fillText
+                   , E.Exception(..), Typeable, E.throw, io
+                   -- * Wrappers around IO primitives.
+                   , onException) where
 
 import Dedukti.Config as Config
 import Control.Monad
@@ -36,8 +37,8 @@
 newtype DkM a = DkM (ReaderT Config IO a)
     deriving (Monad, MonadIO, Functor, Applicative, MonadReader Config)
 
-runDkM :: Config -> DkM a -> IO a
-runDkM conf (DkM m) = runReaderT m conf
+runDkM :: DkM a -> Config -> IO a
+runDkM (DkM m) = runReaderT m
 
 -- | Get all global parameters.
 configuration :: DkM Config
@@ -78,4 +79,4 @@
 onException :: DkM a -> DkM b -> DkM a
 onException x y = do
   conf <- configuration
-  io $ runDkM conf x `E.onException` runDkM conf y
+  io $ runDkM x conf `E.onException` runDkM y conf
diff --git a/Dedukti/Driver/Batch.hs b/Dedukti/Driver/Batch.hs
--- a/Dedukti/Driver/Batch.hs
+++ b/Dedukti/Driver/Batch.hs
@@ -4,6 +4,7 @@
 --
 -- The batch driver. It compiles all given targets and all their dependencies,
 -- also invoking the Haskell compiler on the generated source code.
+
 module Dedukti.Driver.Batch (make) where
 
 import Dedukti.Driver.Compile
@@ -14,12 +15,10 @@
 import qualified Dedukti.Config as Config
 import qualified Control.Hmk.IO as IO
 import Control.Hmk
-import qualified Data.Text.Lazy.Encoding as T
-import qualified Data.ByteString.Lazy as B
+import qualified Data.ByteString.Lazy.Char8 as B
 import qualified Data.Map as Map
 import Control.Monad.State
 import Control.Applicative
-import Data.Typeable (Typeable)
 import System.Directory (copyFile)
 import Data.Char (toUpper)
 
@@ -47,7 +46,8 @@
         Nothing -> do
           lift $ say Verbose $ text "Parsing" <+> text (show mod) <+> text "..."
           let path = srcPathFromModule mod
-          src <- lift (parse path <$> io (liftM T.decodeUtf8 (B.readFile path)))
+          config <- lift configuration
+          src <- lift (parse config path <$> io (B.readFile path))
           let dependencies = collectDependencies src
               rs = g mod dependencies (task_compile mod src)
           -- Recursively construct rules for dependent modules.
@@ -72,23 +72,23 @@
                           , Rule hi (dko:dki:dephis) (Just $ task_hscomp dko) cmp
                           , Rule o (dko:dki:dephis) (Just $ task_hscomp dko) cmp
                           , Rule chi [hi] (Just $ task_himv hi chi) cmp ]
-    task_hscomp dko _ = do
+    task_hscomp dko _ = abortOnError $ do
       hscomp <- parameter Config.hsCompiler
       io . IO.testExitCode =<< command hscomp [ "-c", "-w", "-x", "hs", dko
                                               , "-XOverloadedStrings"
                                               , "-XPatternGuards" ]
     -- GHC won't find the interface files if their names don't start with a
     -- capital letter. So alias the interface file with a capitalized name.
-    task_himv hi chi _ = do
+    task_himv hi chi _ = abortOnError $ do
       io $ copyFile hi chi
       return TaskSuccess
-    task_compile mod src _ = do
+    task_compile mod src _ = abortOnError $ do
       compileAST mod src `onException`
           (say Quiet $ text "In module" <+> pretty mod <> text ":")
       return TaskSuccess
 
 data CommandError = CommandError
-    deriving Typeable
+                    deriving Typeable
 
 instance Show CommandError where
     show CommandError = "Command returned non-zero exit status."
@@ -97,19 +97,30 @@
 
 -- | Perform each system action, aborting if an action returns
 -- non-zero exit code.
-abortOnError :: [DkM Result] -> DkM ()
-abortOnError = mapM_ f where
-    f cmd = do code <- cmd
-               case code of
-                 TaskSuccess -> return ()
-                 TaskFailure -> throw CommandError
+abortOnError :: DkM Result -> DkM Result
+abortOnError cmd = do
+  code <- cmd
+  case code of
+    TaskFailure -> throw CommandError
+    x -> return x
 
 -- | Compile each of the modules given as input and all of their
 -- dependencies, if necessary.
 make :: [MName] -> DkM ()
 make modules = do
+  config <- configuration
   let targets = map (pathFromModule ".o") modules
+      run :: Rule DkM a -> Rule IO a
+      run Rule{..} = Rule{ recipe = fmap (\f x -> runDkM (f x) config) recipe
+                         , isStale = \x y -> runDkM (isStale x y) config
+                         , .. }
   rs <- process cmp <$> rules modules
-  schedule <- mk rs targets
-  say Debug $ text "Tasks to execute:" <+> int (length schedule)
-  abortOnError schedule
+  -- Depending on whether we have several cores or not, we either call
+  -- mkConcurrent to perform all the tasks concurrently, or call mk to create
+  -- a schedule and execute that.
+  n <- parameter Config.jobs
+  if n > 1 then
+      do io $ mkConcurrent n (map run rs) targets else
+      do schedule <- mk rs targets
+         say Verbose $ text "Tasks to execute:" <+> int (length schedule)
+         sequence_ schedule
diff --git a/Dedukti/Driver/Compile.hs b/Dedukti/Driver/Compile.hs
--- a/Dedukti/Driver/Compile.hs
+++ b/Dedukti/Driver/Compile.hs
@@ -8,29 +8,26 @@
 
 import Dedukti.Module
 import Dedukti.Parser
+import qualified Dedukti.Parser.Interface as Interface
 import Dedukti.DkM
 import Dedukti.Core
 import Dedukti.Analysis.Dependency
 import Dedukti.Analysis.Scope
+import Control.Applicative
 import qualified Dedukti.CodeGen.Exts as CG
 import qualified Dedukti.Rule as Rule
 import qualified Dedukti.Analysis.Rule as Rule
-import qualified Data.Text.Lazy as T
-import qualified Data.Text.Lazy.Encoding as T
-import qualified Data.ByteString.Lazy as B
+import qualified Data.ByteString.Lazy.Char8 as B
 import qualified Data.Set as Set
 
 
-readT = io . liftM T.decodeUtf8 . B.readFile
-writeT path = io . B.writeFile path . T.encodeUtf8
-
 -- | Qualify all occurrences of identifiers defined in current module.
 selfQualify :: MName -> [Pa RuleSet] -> [Pa RuleSet]
 selfQualify mod rsets = let defs = Set.fromList (map rs_name rsets)
                         in map (descend (f defs))
-                               (map (\RS{..} -> RS{rs_name = rs_name{qid_qualifier = mod}, ..}) rsets)
+                               (map (\RS{..} -> RS{rs_name = qualify mod rs_name, ..}) rsets)
     where f defs (Var x a) | Nothing <- provenance x
-                           , x `Set.member` defs = Var x{qid_qualifier = mod} a
+                           , x `Set.member` defs = Var (qualify mod x) a
           f defs (Lam (x ::: ty) t a) =
               Lam (x ::: f defs ty) (f (Set.delete x defs) t) a
           f defs (Pi (x ::: ty) t a) =
@@ -39,24 +36,24 @@
 
 -- | Read the interface file of each module name to collect the declarations
 -- exported by the module.
-populateInitialEnvironment :: [MName] -> DkM (Set.Set Qid)
-populateInitialEnvironment =
-    liftM Set.unions .
+populateInitialEnvironment :: [MName] -> DkM Context
+populateInitialEnvironment deps =
+    initContext . concat <$>
     mapM (\dep -> let path = ifacePathFromModule dep
-                  in liftM (Set.fromList . map (qual dep) . parseIface path) $
-                     readT path)
-        where qual mod qid = qid{qid_qualifier = mod}
+                  in map (qualify dep) . Interface.parse path <$>
+                     io (B.readFile path)) deps
 
 -- | Generate the content of an interface file.
-interface :: Pa Module -> T.Text
-interface (decls, _) = T.unlines (map (qid_stem . bind_name) decls)
+interface :: Pa Module -> B.ByteString
+interface (decls, _) = B.unlines (map (fromAtom . qid_stem . bind_name) decls)
 
 -- | Emit Haskell code for one module.
 compile :: MName -> DkM ()
 compile mod = do
   say Verbose $ text "Parsing" <+> text (show mod) <+> text "..."
   let path = srcPathFromModule mod
-  compileAST mod =<< return (parse path) `ap` readT path
+  config <- configuration
+  compileAST mod =<< return (parse config path) `ap` io (B.readFile path)
 
 -- | Emit Haskell code for one module, starting from the AST.
 compileAST :: MName -> Pa Module -> DkM ()
@@ -72,9 +69,10 @@
   checkUniqueness src
   checkScopes extdecls src
   Rule.checkOrdering rules
+  say Verbose $ text "Checking well formation of rule heads ..."
   mapM_ Rule.checkHead rules
-  say Debug $ pretty (concatMap rs_rules (Rule.ruleSets decls rules))
+  say Debug $ pretty $ Rule.ruleSets decls rules
   say Verbose $ text "Compiling" <+> text (show mod) <+> text "..."
   let code = map CG.emit (selfQualify mod (Rule.ruleSets decls rules)) :: [CG.Code]
-  writeT (objPathFromModule mod) $ CG.serialize mod deps $ CG.coalesce code
-  writeT (ifacePathFromModule mod) $ interface src
+  io $ B.writeFile (objPathFromModule mod) $ CG.serialize mod deps $ CG.coalesce code
+  io $ B.writeFile (ifacePathFromModule mod) $ interface src
diff --git a/Dedukti/Module.hs b/Dedukti/Module.hs
--- a/Dedukti/Module.hs
+++ b/Dedukti/Module.hs
@@ -5,6 +5,8 @@
 -- A representation of module names and associated functions to map module
 -- names to source files and vice-versa. Qualified names, as required in the
 -- presence of modules, are also defined here.
+
+{-# OPTIONS_GHC -funbox-strict-fields #-}
 module Dedukti.Module
     ( -- * Data types
       Hierarchy(..), MName
@@ -14,18 +16,25 @@
     , hierarchy, toList
     , pathFromModule, moduleFromPath
     , srcPathFromModule, objPathFromModule, ifacePathFromModule
-    -- * Qualified names.
-    , Qid(..), qid, (.$), provenance, unqualify
+    -- * Qualified names
+    , Qid, qid_qualifier, qid_stem, qid_suffix
+    , qid, (.$), provenance, qualify, unqualify
+    -- * Atoms
+    , Atom
+    , fromAtom, toAtom
     ) where
 
 import Dedukti.DkM
 import System.FilePath
 import Data.Char (isAlpha, isAlphaNum)
-import qualified Data.Text.Lazy as T
+import qualified Data.ByteString.Lazy.Char8 as B
+import qualified Data.ByteString as BS (concat)
 import Text.PrettyPrint.Leijen
+import qualified StringTable.Atom as Atom
+import StringTable.Atom (Atom)
 
 
-data Hierarchy = !Hierarchy :. !T.Text | Root
+data Hierarchy = !Hierarchy :. !Atom | Root
                  deriving (Eq, Ord, Show)
 
 type MName = Hierarchy
@@ -39,31 +48,37 @@
 instance Exception InvalidModuleName
 
 instance Pretty MName where
-    pretty (Root :. x) = text (T.unpack x)
-    pretty (xs :. x) = pretty xs <> char '.' <> text (T.unpack x)
+    pretty (Root :. x) = text (B.unpack (fromAtom x))
+    pretty (xs :. x) = pretty xs <> char '.' <> text (B.unpack (fromAtom x))
 
-hierarchy :: [T.Text] -> Hierarchy
+fromAtom :: Atom -> B.ByteString
+fromAtom = B.fromChunks . return . Atom.fromAtom
+
+toAtom :: B.ByteString -> Atom
+toAtom = Atom.toAtom . BS.concat . B.toChunks
+
+hierarchy :: [B.ByteString] -> Hierarchy
 hierarchy =  f . reverse where
     f [] = Root
-    f (x:xs) = f xs :. x
+    f (x:xs) = f xs :. toAtom x
 
-toList :: Hierarchy -> [T.Text]
+toList :: Hierarchy -> [B.ByteString]
 toList = reverse . f where
     f Root = []
-    f (xs :. x) = x : f xs
+    f (xs :. x) = fromAtom x : f xs
 
 -- | Raise an exception if module name component is a valid identifier.
 check :: String -> String
-check cmpt@(x:xs) | isAlpha x, and (map isAlphaNum xs) = cmpt
+check cmpt@(x:xs) | isAlpha x, and (map (\x -> isAlphaNum x || elem x "_-+~") xs) = cmpt
                   | otherwise = throw $ InvalidModuleName cmpt
 
 pathFromModule :: String -> MName -> FilePath
 pathFromModule ext mod =
-    addExtension (joinPath $ map T.unpack $ toList mod) ext
+    addExtension (joinPath $ map B.unpack $ toList mod) ext
 
 moduleFromPath :: FilePath -> MName
 moduleFromPath =
-    hierarchy . map (T.pack . check) . splitDirectories . dropExtension
+    hierarchy . map (B.pack . check) . splitDirectories . dropExtension
 
 srcPathFromModule :: MName -> FilePath
 srcPathFromModule = pathFromModule ".dk"
@@ -75,24 +90,30 @@
 ifacePathFromModule = pathFromModule ".dki"
 
 -- | The datatype of qualified names.
-data Qid = Qid { qid_qualifier :: !Hierarchy
-               , qid_stem      :: !T.Text
-               , qid_suffix    :: !Hierarchy }
-           deriving (Eq, Ord, Show)
+data Qid = Qid !Hierarchy !Atom !Hierarchy
+           deriving (Eq, Show, Ord)
 
+qid_qualifier (Qid qual _ _) = qual
+qid_stem (Qid _ stem _) = stem
+qid_suffix (Qid _ _ suf) = suf
+
 -- | Shorthand qid introduction.
-qid :: T.Text -> Qid
-qid x = Qid Root x Root
+qid :: B.ByteString -> Qid
+qid x = Qid Root (toAtom x) Root
 
 -- | Append suffix.
-(.$) :: Qid -> T.Text -> Qid
-(Qid qual x sufs) .$ suf = Qid qual x (sufs :. suf)
+(.$) :: Qid -> B.ByteString -> Qid
+(Qid qual x sufs) .$ suf = Qid qual x (sufs :. (toAtom suf))
 
 -- | Get the module where the qid is defined, based on its qualifier.
 provenance :: Qid -> Maybe MName
 provenance (Qid Root _ _) = Nothing
 provenance (Qid qual _ _) = Just qual
 
+-- | Set the qualifier.
+qualify :: Hierarchy -> Qid -> Qid
+qualify qual (Qid _ stem suf) = Qid qual stem suf
+
 -- | Remove any qualifier.
 unqualify :: Qid -> Qid
-unqualify qid = qid{qid_qualifier = Root}
+unqualify (Qid _ stem suf) = Qid Root stem suf
diff --git a/Dedukti/Parser.hs b/Dedukti/Parser.hs
--- a/Dedukti/Parser.hs
+++ b/Dedukti/Parser.hs
@@ -1,181 +1,31 @@
 -- |
 -- Copyright : © 2009 CNRS - École Polytechnique - INRIA
 -- License   : GPL
+--
+-- Frontend to all the different parsers available. This module abstracts over
+-- that fact that input can come in different formats, providing a single
+-- point of entry to parsing instead.
 
-{-# OPTIONS_GHC -fno-warn-unused-binds #-}
-module Dedukti.Parser (Pa, Dedukti.Parser.parse, parseIface) where
+module Dedukti.Parser where
 
+import qualified Dedukti.Config as Config
+import qualified Dedukti.Parser.External as External
+import qualified Dedukti.Parser.Prefix as Prefix
 import Dedukti.Core
 import Dedukti.Module
-import Text.Parsec hiding (ParseError, parse)
-import qualified Text.Parsec.Token as Token
-import Control.Applicative hiding ((<|>), many)
-import Control.Monad.Identity
-import qualified Control.Exception as Exception
-import qualified Data.Text.Lazy as T
-import Data.Typeable (Typeable)
+import qualified Data.ByteString.Lazy.Char8 as B
 
 
+type SourceName = String
+
 -- The AST type as returned by the Parser.
 type Pa t = t Qid Unannot
 
--- The parsing monad.
-type P = Parsec String [Pa TyRule]
-
-newtype ParseError = ParseError String
-    deriving Typeable
-
-instance Show ParseError where
-    show (ParseError e) = e
-
-instance Exception.Exception ParseError
-
-newtype IfaceError = IfaceError String
-    deriving Typeable
-
-instance Show IfaceError where
-    show (IfaceError f) = "Broken interface file " ++ f ++ "."
-
-instance Exception.Exception IfaceError
-
-parse :: SourceName -> T.Text -> Pa Module
-parse name input =
-    -- At the toplevel, a source file is a list of declarations and rule
-    -- definitions. Here rules are accumulated by side-effect, added to the
-    -- parser state as we encounter them.
-    case runParser ((,) <$> toplevel <*> allRules) [] name (T.unpack input) of
-      Left e -> Exception.throw (ParseError (show e))
-      Right x -> x
-
--- | Parser for interface files.
-parseIface :: SourceName -> T.Text -> [Qid]
-parseIface _ = map qid . T.lines
-
-addRule :: Pa TyRule -> P ()
-addRule rule = modifyState (rule:)
-
--- | Retrieve all rules encountered so far from the parser state.
-allRules :: P [Pa TyRule]
-allRules = liftM reverse getState
-
-lexDef = Token.LanguageDef
-         { Token.commentStart = "(;"
-         , Token.commentEnd = ";)"
-         , Token.commentLine = ";"
-         , Token.nestedComments = False
-         , Token.identStart = alphaNum <|> char '_' <|> char '\''
-         , Token.identLetter = alphaNum <|> char '_' <|> char '\''
-         , Token.opStart = parserFail "No user defined operators yet."
-         , Token.opLetter = parserFail "No user defined operators yet."
-         , Token.reservedNames = ["Type", "Kind"]
-         , Token.reservedOpNames = [":", "=>", "->", "-->"]
-         , Token.caseSensitive = True
-         }
-
-Token.LanguageDef{..} = lexDef
-Token.TokenParser{..} = Token.makeTokenParser lexDef
-
--- | Qualified or unqualified name.
---
--- > qid ::= id.id | id
-qident = ident <?> "qid" where
-    ident = do
-      c <- identStart
-      cs <- many identLetter
-      x <- (do let qualifier = T.pack (c:cs)
-               c <- try $ do char '.'; identStart
-               cs <- many identLetter
-               let name = T.pack (c:cs)
-               return $ Qid (Root :. qualifier) name Root)
-           <|> return (qid (T.pack (c:cs)))
-      whiteSpace
-      return (Var x nann)
-
--- | Unqualified name.
-ident = qid . T.pack <$> identifier
-
--- | Root production rule of the grammar.
---
--- > toplevel ::= declaration toplevel
--- >            | rule toplevel
--- >            | eof
-toplevel =
-    whiteSpace *>
-    (    (rule *> toplevel) -- Rules are accumulated by side-effect.
-     <|> ((:) <$> declaration <*> toplevel)
-     <|> (eof *> return []))
-
--- | Binding construct.
---
--- > binding ::= id : term
-binding = ((:::) <$> ident <* reservedOp ":" <*> term)
-          <?> "binding"
-
--- | Top-level declarations.
---
--- > declaration ::= id ":" term "."
-declaration = (binding <* dot)
-              <?> "declaration"
-
--- | Left hand side of an abstraction or a product.
---
--- > domain ::= id ":" applicative
--- >          | applicative
-domain = (    ((:::) <$> try (ident <* reservedOp ":") <*> applicative)
-          <|> (Hole <$> applicative))
-         <?> "domain"
-
--- |
--- > sort ::= Type
-sort = Type <$ reserved "Type"
-
--- | Terms and types.
---
--- We first try to parse as the domain of a lambda or pi. If we
--- later find out there was no arrow after the domain, then we take
--- the domain to be an expression, and return that.
---
--- > term ::= domain "->" term
--- >        | domain "=>" term
--- >        | applicative
-term = do
-  d <- domain
-  choice [ pi d <?> "pi"
-         , lambda d <?> "lambda"
-         , return (bind_type d)]
-    where pi d = Pi <$> pure d <* reservedOp "->" <*> term <%%> nann
-          lambda d = Lam <$> pure d <* reservedOp "=>" <*> term <%%> nann
-
--- | Constituents of an applicative form.
---
--- > simple ::= sort
--- >          | qid
--- >          | "(" term ")"
-simple = sort <|> qident <|> parens term
-
--- | Expressions that are either a name or an application of a
--- expression to one or more arguments.
---
--- > applicative ::= simple
--- >               | applicative simple
--- >
-applicative = (\xs -> case xs of
-                        [t] -> t
-                        (f:ts) -> apply f ts (repeat nann))
-              <$> many1 simple
-              <?> "applicative"
-
--- | A rule.
---
--- > rule ::= env term "-->" term
--- > env ::= "[]"
--- >       | "[" env2 "]"
--- > env2 ::= binding
--- >        | binding "," env2
-rule = ((\env lhs rhs -> foldr (&) emptyEnv env :@ lhs :--> rhs)
-        <$> brackets (sepBy binding comma)
-        <*> term
-        <*  reservedOp "-->"
-        <*> term
-        <*  dot) >>= addRule
-       <?> "rule"
+parse :: Config.Config -> SourceName -> B.ByteString -> Pa Module
+parse config name input =
+  let magic = "(; # FORMAT prefix # ;)\n" in
+  case (magic `B.isPrefixOf` input, Config.format config) of
+    (True, _) -> Prefix.parse name (B.drop (B.length magic) input)
+    (False, Just Config.Prefix) -> Prefix.parse name input
+    (False, Just Config.External) -> External.parse name input
+    (False, Nothing) -> External.parse name input
diff --git a/Dedukti/Parser.hs-boot b/Dedukti/Parser.hs-boot
new file mode 100644
--- /dev/null
+++ b/Dedukti/Parser.hs-boot
@@ -0,0 +1,9 @@
+module Dedukti.Parser where
+
+import Dedukti.Core
+import Dedukti.Module
+
+
+type SourceName = String
+type Pa t = t Qid Unannot
+
diff --git a/Dedukti/Parser/External.hs b/Dedukti/Parser/External.hs
new file mode 100644
--- /dev/null
+++ b/Dedukti/Parser/External.hs
@@ -0,0 +1,175 @@
+-- |
+-- Copyright : © 2009 CNRS - École Polytechnique - INRIA
+-- License   : GPL
+
+{-# OPTIONS_GHC -fno-warn-unused-binds #-}
+module Dedukti.Parser.External (Pa, parse) where
+
+import {-# SOURCE #-} Dedukti.Parser
+import Dedukti.Core
+import Dedukti.Module
+import Text.Parsec hiding (SourceName, ParseError, parse)
+import qualified Text.Parsec.Token as Token
+import Control.Applicative hiding ((<|>), many)
+import Control.Monad.Identity
+import qualified Data.ByteString.Lazy.Char8 as B
+import qualified Control.Exception as Exception
+import Data.Typeable (Typeable)
+
+
+-- The parsing monad.
+type P = Parsec B.ByteString [Pa TyRule]
+
+newtype ParseError = ParseError String
+    deriving Typeable
+
+instance Show ParseError where
+    show (ParseError e) = e
+
+instance Exception.Exception ParseError
+
+newtype IfaceError = IfaceError String
+    deriving Typeable
+
+instance Show IfaceError where
+    show (IfaceError f) = "Broken interface file " ++ f ++ "."
+
+instance Exception.Exception IfaceError
+
+parse :: SourceName -> B.ByteString -> Pa Module
+parse name input =
+    -- At the toplevel, a source file is a list of declarations and rule
+    -- definitions. Here rules are accumulated by side-effect, added to the
+    -- parser state as we encounter them.
+    case runParser ((,) <$> toplevel <*> allRules) [] name input of
+      Left e -> Exception.throw (ParseError (show e))
+      Right x -> x
+
+addRule :: Pa TyRule -> P ()
+addRule rule = modifyState (rule:)
+
+-- | Retrieve all rules encountered so far from the parser state.
+allRules :: P [Pa TyRule]
+allRules = liftM reverse getState
+
+lexDef = Token.LanguageDef
+         { Token.commentStart = "(;"
+         , Token.commentEnd = ";)"
+         , Token.commentLine = ";"
+         , Token.nestedComments = False
+         , Token.identStart = alphaNum <|> char '_' <|> char '\''
+         , Token.identLetter = alphaNum <|> char '_' <|> char '\''
+         , Token.opStart = parserFail "No user defined operators yet."
+         , Token.opLetter = parserFail "No user defined operators yet."
+         , Token.reservedNames = ["Type", "Kind"]
+         , Token.reservedOpNames = [":", "=>", "->", "-->"]
+         , Token.caseSensitive = True
+         }
+
+Token.LanguageDef{..} = lexDef
+Token.TokenParser{..} = Token.makeTokenParser lexDef
+
+-- | Qualified or unqualified name.
+--
+-- > qid ::= id.id | id
+qident = ident <?> "qid" where
+    ident = do
+      c <- identStart
+      cs <- many identLetter
+      x <- (do let qualifier = B.pack (c:cs)
+               c <- try $ do char '.'; identStart
+               cs <- many identLetter
+               let name = B.pack (c:cs)
+               return $ qualify (hierarchy [qualifier]) (qid name))
+           <|> return (qid (B.pack (c:cs)))
+      whiteSpace
+      return (Var x nann)
+
+-- | Unqualified name.
+ident = qid . B.pack <$> identifier
+
+-- | Root production rule of the grammar.
+--
+-- > toplevel ::= declaration toplevel
+-- >            | rule toplevel
+-- >            | eof
+toplevel =
+    whiteSpace *>
+    (    (rule *> toplevel) -- Rules are accumulated by side-effect.
+     <|> ((:) <$> declaration <*> toplevel)
+     <|> (eof *> return []))
+
+-- | Binding construct.
+--
+-- > binding ::= id ":" term
+binding = ((:::) <$> ident <* reservedOp ":" <*> term)
+          <?> "binding"
+
+-- | Top-level declarations.
+--
+-- > declaration ::= binding "."
+declaration = (binding <* dot)
+              <?> "declaration"
+
+-- | Left hand side of an abstraction or a product.
+--
+-- > domain ::= id ":" applicative
+-- >          | applicative
+domain = (    ((:::) <$> try (ident <* reservedOp ":") <*> applicative)
+          <|> (Hole <$> applicative))
+         <?> "domain"
+
+-- |
+-- > sort ::= "Type"
+sort = Type <$ reserved "Type"
+
+-- | Terms and types.
+--
+-- We first try to parse as the domain of a lambda or pi. If we
+-- later find out there was no arrow after the domain, then we take
+-- the domain to be an expression, and return that.
+--
+-- > term ::= domain "->" term
+-- >        | domain "=>" term
+-- >        | applicative
+term = do
+  d <- domain
+  choice [ pi d <?> "pi"
+         , lambda d <?> "lambda"
+         , return (bind_type d)]
+    where pi d = Pi <$> pure d <* reservedOp "->" <*> term <%%> nann
+          lambda d = Lam <$> pure d <* reservedOp "=>" <*> term <%%> nann
+
+-- | Constituents of an applicative form.
+--
+-- > simple ::= sort
+-- >          | qid
+-- >          | "(" term ")"
+simple = sort <|> qident <|> parens term
+
+-- | Expressions that are either a name or an application of a
+-- expression to one or more arguments.
+--
+-- > applicative ::= simple
+-- >               | applicative simple
+-- >
+applicative = (\xs -> case xs of
+                        [t] -> t
+                        (f:ts) -> apply f ts (repeat nann))
+              <$> many1 simple
+              <?> "applicative"
+
+-- | A rule.
+--
+-- > rule ::= env term "-->" term "."
+-- > env ::= "[]"
+-- >       | "[" env2 "]"
+-- > env2 ::= binding
+-- >        | binding "," env2
+rule = ((\env lhs rhs -> foldr (&) emptyEnv env :@ lhs :--> rhs)
+        <$> brackets (sepBy binding comma)
+        <*> term
+        <*  reservedOp "-->"
+        <*> term
+        <*  dot) >>= addRule
+       <?> "rule"
diff --git a/Dedukti/Parser/Prefix.hs b/Dedukti/Parser/Prefix.hs
new file mode 100644
--- /dev/null
+++ b/Dedukti/Parser/Prefix.hs
@@ -0,0 +1,57 @@
+-- |
+-- Copyright : © 2009 CNRS - École Polytechnique - INRIA
+-- License   : GPL
+--
+-- Parser for an alternative format for Dedukti source files using reverse
+-- polish notation. This format has the advantage of being very easy to parse
+-- efficiently.
+
+{-# OPTIONS_GHC -funbox-strict-fields #-}
+module Dedukti.Parser.Prefix (Pa, parse) where
+
+import {-# SOURCE #-} Dedukti.Parser
+import Dedukti.Core
+import Dedukti.Module
+import qualified Data.ByteString.Lazy.Char8 as B
+import Data.Either (partitionEithers)
+import Data.Char (isSpace)
+
+
+type Token = B.ByteString
+data Frame = Expr !(Pa Expr)
+           | Binding !(Pa Binding)
+           | Env [Pa Binding]
+           | TyRule !(Pa TyRule)
+
+type Stack = [Frame]
+
+
+parse :: SourceName -> B.ByteString -> Pa Module
+parse name = partitionEithers . map classify . foldr step [] . tokens
+  where classify (Binding x) = Left x
+        classify (TyRule x) = Right x
+        classify _ = error $ "Parse error in " ++ name
+
+tokens :: B.ByteString -> [Token]
+tokens = filter (not . B.null) . B.splitWith isSpace
+
+step :: Token -> Stack -> Stack
+
+-- bindings
+step ":" (Expr (Var x _) : Expr y : xs) = Binding (x ::: y) : xs
+
+-- rules
+step "-->" (Env x : Expr y : Expr z : xs) = TyRule (fromBindings x :@ y :--> z) : xs
+
+-- environments
+step "," (Binding x : Env y : xs) = Env (x:y) : xs
+step "[]" xs = Env [] : xs
+
+-- expressions
+step "=>"   (Binding x : Expr y : xs) = Expr (Lam x y %% nann) : xs
+step "->"   (Binding x : Expr y : xs) = Expr (Pi x y %% nann) : xs
+step "@"    (Expr x : Expr y : xs)    = Expr (App x y %% nann) : xs
+step "Type" xs                        = Expr Type : xs
+step v xs = case reverse (B.split '.' v) of
+  var : quals -> let mod = hierarchy (reverse quals)
+                 in Expr (Var (qualify mod (qid var)) %% nann) : xs
diff --git a/Dedukti/Pretty.hs b/Dedukti/Pretty.hs
--- a/Dedukti/Pretty.hs
+++ b/Dedukti/Pretty.hs
@@ -12,15 +12,33 @@
 import Dedukti.Core
 import Dedukti.Module
 import Text.PrettyPrint.Leijen
-import qualified Data.Text.Lazy as T
+import qualified Data.ByteString.Lazy.Char8 as B
 
 
-textT = text . T.unpack
+textB = text . B.unpack
 
+-- | For purposes of pretty-printing, need to distinguish a top-level binding
+-- from a binding representing the domain of a dependent product or
+-- abstraction.
+newtype Domain id a = Domain (Binding id a)
+
+instance Pretty id => Pretty (Binding id a) where
+    pretty (x ::: ty) = pretty x <+> char ':' <+> pretty ty
+    pretty (Hole ty) =  pretty ty
+
+    prettyList = vcat . map (\x -> pretty x <> dot)
+
+instance Pretty id => Pretty (Domain id a) where
+    pretty (Domain dom) =
+        let pty | Pi _ _ _ <- bind_type dom = parens (pretty (bind_type dom))
+                | otherwise = pretty (bind_type dom)
+        in case dom of
+             x ::: _ -> pretty x <+> char ':' <+> pty
+             Hole _ -> pty
+
 instance Pretty id => Pretty (Expr id a) where
-    pretty (Lam x t _) = pretty x <+> text "=>" <+> pretty t
-    pretty (Pi x t _) | Pi _ _ _ <- bind_type x = parens (pretty x) <+> text "->" <+> pretty t
-                      | otherwise = pretty x <+> text "->" <+> pretty t
+    pretty (Lam dom ran _) = pretty dom <+> text "=>" <+> pretty ran
+    pretty (Pi dom ran _) = pretty (Domain dom) <+> text "->" <+> pretty ran
     pretty (App t1 t2 _) =
         let f = if isApplicative t1 then id else parens
             g = if isAtomic t2 then id else parens
@@ -29,12 +47,6 @@
     pretty Type = text "Type"
     pretty Kind = text "Kind"
 
-instance Pretty id => Pretty (Binding id a) where
-    pretty (x ::: ty) = pretty x <+> char ':' <+> pretty ty
-    pretty (Hole ty) =  pretty ty
-
-    prettyList = vcat . map (\x -> pretty x <> dot)
-
 instance Pretty id => Pretty (Rule id a) where
     pretty (lhs :--> rhs) = pretty lhs <+> text "-->" <+> pretty rhs
 
@@ -48,11 +60,15 @@
 
     prettyList = vcat . map (\x -> pretty x <> dot)
 
+instance (Eq a, Ord id, Pretty id) => Pretty (RuleSet id a) where
+    pretty RS{..} = vcat (pretty (rs_name ::: rs_type) : map pretty rs_rules)
+    prettyList = vcat . punctuate line . map pretty
+
 instance Pretty Qid where
     pretty qid = joinQ (qid_qualifier qid) <>
-                 textT (qid_stem qid) <>
+                 textB (fromAtom (qid_stem qid)) <>
                  joinS (qid_suffix qid)
         where joinQ Root = empty
-              joinQ (h :. x) = joinQ h <> textT x <> dot
+              joinQ (h :. x) = joinQ h <> textB (fromAtom x) <> dot
               joinS Root = empty
-              joinS (h :. x) = joinS h <> char '_' <> textT x
+              joinS (h :. x) = joinS h <> char '_' <> textB (fromAtom x)
diff --git a/Dedukti/Rule.hs b/Dedukti/Rule.hs
--- a/Dedukti/Rule.hs
+++ b/Dedukti/Rule.hs
@@ -36,9 +36,9 @@
 
 -- | Combine declarations with their associated rules, if any.
 ruleSets :: (Show id, Show a, Ord id) => [Binding id a] -> [TyRule id a] -> [RuleSet id a]
-ruleSets ds rs = snd $ foldl aux (sortBy cmp (group rs), []) ds where
-    aux ([],       rsets) (x ::: ty)          = ([], RS x ty [] : rsets)
-    aux (rs : rss, rsets) (x ::: ty)
+ruleSets ds rs = snd $ foldr aux (sortBy cmp (group rs), []) ds where
+    aux (x ::: ty) ([],       rsets)          = ([], RS x ty [] : rsets)
+    aux (x ::: ty) (rs : rss, rsets)
         | x == headConstant (Prelude.head rs) = (rss, RS x ty rs : rsets)
         | otherwise                           = (rs : rss, RS x ty [] : rsets)
     -- We cannot change the order of the declarations, but we need rules to be
@@ -46,7 +46,7 @@
     ordering = Map.fromList (zip (map bind_name ds) [0..])
     cmp x y = let xi = ordering Map.! headConstant (Prelude.head x)
                   yi = ordering Map.! headConstant (Prelude.head y)
-              in compare xi yi
+              in compare yi xi
 
 -- | Make the rule left-linear and return collected unification constraints.
 -- This function must be provided with an infinite supply of fresh variable
@@ -62,7 +62,7 @@
             (xs, seen, constraints) <- get
             if x `Set.member` seen then
                 do let Stream.Cons x' xs' = xs
-                   put (xs', Set.insert x seen, (x, x'):constraints)
+                   put (xs', Set.insert x' seen, (x, x'):constraints)
                    return $ Var x' a else
                 do put (xs, Set.insert x seen, constraints)
                    return t
diff --git a/Dedukti/Runtime.hs b/Dedukti/Runtime.hs
--- a/Dedukti/Runtime.hs
+++ b/Dedukti/Runtime.hs
@@ -29,8 +29,8 @@
 import Text.Show.Functions ()
 import Data.Typeable hiding (typeOf)
 import Prelude hiding (pi, catch)
-import System.IO
 import Data.Time.Clock
+import Text.PrettyPrint.Leijen
 
 
 -- Exceptions
@@ -41,7 +41,7 @@
 data TypeError = TypeError
     deriving (Show, Typeable)
 
-data RuleError = RuleError
+data RuleError = RuleError Doc Doc
     deriving (Show, Typeable)
 
 instance Exception SortError
@@ -106,25 +106,25 @@
 
 typeOf :: Int -> Term -> Code
 typeOf n (Box ty _) = ty
-typeOf n (TLam bx@(Box Type a) f) = Pi a (\x -> typeOf n (f (Box a x)))
-typeOf n (TPi bx@(Box Type a) f) = typeOf (n + 1) (f (Box a (Var n)))
-typeOf n (TApp t1 bx@(Box ty2 t2))
+typeOf n (TLam (Box Type a) f) = Pi a (\x -> typeOf n (f (Box a x)))
+typeOf n (TPi (Box Type a) f) = typeOf (n + 1) (f (Box a (Var n)))
+typeOf n (TApp t1 (Box ty2 t2))
     | Pi tya f <- typeOf n t1, convertible n tya ty2 = f t2
-typeOf n (TApp t1 bx@(UBox tty2 t2))
+typeOf n (TApp t1 (UBox tty2 t2))
     | Pi tya f <- typeOf n t1, ty2 <- typeOf n tty2,
       convertible n tya ty2 = f t2
 typeOf n TType = Kind
 typeOf n t = throw TypeError
 
 checkDeclaration :: String -> Term -> IO ()
-checkDeclaration x t = catch (evaluate t >> putStrLn "Check") handler
+checkDeclaration x t = catch (evaluate t >> putStrLn ("Checked " ++ x ++ ".")) handler
     where handler (SomeException e) = do
-            putStrLn $ "Error during checking of " ++ x
+            putStrLn $ "Error during checking of " ++ x ++ "."
             throw e
 
 checkRule :: Term -> Term -> Term
 checkRule lhs rhs | convertible 0 (typeOf 0 lhs) (typeOf 0 rhs) = emptyBox
-                  | otherwise = throw RuleError
+                  | otherwise = throw $ RuleError (pretty (typeOf 0 lhs)) (pretty (typeOf 0 rhs))
 
 start :: IO UTCTime
 start = do
@@ -137,3 +137,15 @@
   t' <- getCurrentTime
   let total = diffUTCTime t' t
   putStrLn $ "Stop. Runtime: " ++ show total
+
+-- Pretty printing.
+
+instance Pretty Code where
+  pretty = p 0 where
+    p n (Var x) = text (show x)
+    p n (Con c) = text (show c)
+    p n (Lam f) = parens (int n <+> text "=>" <+> p (n + 1) (f (Var n)))
+    p n (Pi ty1 ty2) = parens (int n <+> colon <+> p n ty1 <+> text "->" <+> p (n + 1) (ty2 (Var n)))
+    p n (App t1 t2) = parens (p n t1 <+> p n t2)
+    p n Type = text "Type"
+    p n Kind = text "Kind"
diff --git a/Setup.lhs b/Setup.lhs
--- a/Setup.lhs
+++ b/Setup.lhs
@@ -1,3 +1,14 @@
 #!/usr/bin/env runhaskell
-> import Distribution.Simple
-> main = defaultMain
+
+> import Distribution.Simple as Simple
+> import Distribution.Simple.LocalBuildInfo
+> import Distribution.PackageDescription
+> import System.FilePath
+> import System.Process
+>
+> main = defaultMainWithHooks hooks
+>   where hooks = simpleUserHooks { Simple.runTests = Main.runTests }
+>
+> runTests :: Args -> Bool -> PackageDescription -> LocalBuildInfo -> IO ()
+> runTests _ _ _ lbi = system testprog >> return ()
+>   where testprog = (buildDir lbi) </> "dedukti-tests" </> "dedukti-tests"
diff --git a/Test.hs b/Test.hs
new file mode 100644
--- /dev/null
+++ b/Test.hs
@@ -0,0 +1,90 @@
+module Main where
+
+import Test.Framework (defaultMain)
+import Test.Framework.Providers.API
+import System.FilePath
+import System.Directory
+import System.Process
+import System.Exit
+import Control.Exception
+import Data.Typeable
+import Prelude hiding (catch)
+
+data CheckResult = CheckOk
+                   -- ^ The property is true as far as we could check it
+                 | CheckFailed String
+                   -- ^ The property was not true. The string is the reason.
+                 | CheckNoExpectedFailure
+                   -- ^ We expected that a property would fail but it didn't
+                 | CheckTimedOut
+                   -- ^ The property timed out during execution
+                 | CheckException String
+                   -- ^ The property raised an exception during execution
+                   deriving Typeable
+
+instance Show CheckResult where
+  show CheckOk = "Ok, passed."
+  show (CheckFailed err) = "Failed: " ++ err
+  show CheckNoExpectedFailure = "No expected failure."
+  show CheckTimedOut = "Timed out."
+  show (CheckException err) = "Exception: " ++ err
+
+instance Exception CheckResult
+
+data CheckRunning = CheckRunning
+                    deriving Show
+
+instance TestResultlike CheckRunning CheckResult where
+    testSucceeded CheckOk = True
+    testSucceeded _ = False
+
+data Expectation = ExpectSuccess | ExpectFailure
+
+data Check = Check { chk_test :: String
+                   , chk_deps :: [String]
+                   , chk_expect :: Expectation }
+
+instance Testlike CheckRunning CheckResult Check where
+    runTest topts Check{..} = runImprovingIO $ do
+      yieldImprovement CheckRunning
+      result <- maybeTimeoutImprovingIO (unK $ topt_timeout topts) $
+                liftIO (dkrun chk_test chk_deps chk_expect)
+      return (result `orElse` CheckTimedOut)
+
+    testTypeName _ = "Type Checking Runs"
+
+dkrun :: FilePath -> [FilePath] -> Expectation -> IO CheckResult
+dkrun dk deps exp = do
+  cwd <- getCurrentDirectory
+  setCurrentDirectory $ cwd </> "t"
+  result <- catch (do
+    let compile = rawSystem "../dist/build/dedukti/dedukti" [dk <.> "dk"]
+        run = rawSystem "../scripts/dkrun" $ (dk <.> "dko") : map (<.> "dko") deps
+    test (return ()) fail compile
+    case exp of
+      ExpectSuccess -> test (return CheckOk) fail run
+      ExpectFailure -> test (return CheckNoExpectedFailure) (const $ return CheckOk) run)
+            (\e -> return (e :: CheckResult))
+  setCurrentDirectory cwd
+  return result
+    where test s f m = m >>= \code -> case code of
+            ExitSuccess -> s
+            ExitFailure x -> f x
+          fail x = throw $ CheckFailed $ "exit status " ++ show x
+
+check :: TestName -> [String] -> Test
+check name deps = Test name (Check name deps ExpectSuccess)
+
+checkFailure :: TestName -> [String] -> Test
+checkFailure name deps = Test name (Check name deps ExpectFailure)
+
+-- * Actual tests.
+
+main = defaultMain tests
+
+tests = [ testGroup "Smoke tests"
+          [ check "nat" []
+          , check "logic" []
+          , check "coc" []
+          , check "peano" ["logic", "coc"]
+          , checkFailure "bug" [] ] ]
diff --git a/dedukti.cabal b/dedukti.cabal
--- a/dedukti.cabal
+++ b/dedukti.cabal
@@ -1,9 +1,9 @@
 name:           dedukti
-version:        1.0.3
+version:        1.1.0
 author:         Mathieu Boespflug
 maintainer:     Mathieu Boespflug <mboes@lix.polytechnique.fr>
 copyright:      © 2009 CNRS - École Polytechnique - INRIA
-homepage:       http://www.lix.polytechnique.fr/~mboes/src/dedukti.git
+homepage:       http://www.lix.polytechnique.fr/dedukti
 synopsis:       A type-checker for the λΠ-modulo calculus.
 description:
     Dedukti is a proof checker for the λΠ-modulo calculus, a
@@ -16,7 +16,7 @@
 license:        GPL
 license-file:   COPYING
 cabal-version:  >= 1.6.0
-build-type:     Simple
+build-type:     Custom
 tested-with:    GHC ==6.10
 data-files:     t/bug.dk
                 t/coc.dk
@@ -36,11 +36,22 @@
                       doc/fdl.texi
                       doc/references.texi
 
+flag test
+  description: Compile test harness (requires test-framework).
+  default:     False
 
+library
+  exposed-modules:     Dedukti.Runtime
+  build-depends:       time >= 1.1
+  extensions:          DeriveDataTypeable, PatternGuards, FlexibleInstances
+  ghc-options:         -fwarn-unused-binds -fwarn-unused-imports
+
 executable dedukti
   main-is:             Dedukti.hs
   other-modules:       Dedukti.Core,
                        Dedukti.Parser,
+                       Dedukti.Parser.External,
+                       Dedukti.Parser.Prefix,
                        Dedukti.Pretty,
                        Dedukti.Driver.Interactive,
                        Dedukti.Driver.Batch,
@@ -57,18 +68,32 @@
 
   build-depends:       base >= 4 && < 5, mtl >= 1.1, containers >= 0.2,
                        directory, filepath, process,
-                       parsec >= 3.0.0, wl-pprint >= 1.0, bytestring >= 0.9.1.0,
-                       haskell-src-exts >= 1.1.0, Stream >= 0.3, text >= 0.3,
-                       hmk >= 0.9
-  extensions:          EmptyDataDecls, PatternGuards, GeneralizedNewtypeDeriving
-                       DeriveDataTypeable, TypeFamilies, LiberalTypeSynonyms,
+                       bytestring >= 0.9.1.0,
+                       parsec >= 3.1.0,
+                       wl-pprint >= 1.0,
+                       haskell-src-exts >= 1.1.0,
+                       haskell-src-exts-qq >= 0.1,
+                       Stream >= 0.3 && < 0.3.2,
+                       hmk >= 0.9.7,
+                       stringtable-atom >= 0.0.6
+  extensions:          EmptyDataDecls, PatternGuards,
+                       GeneralizedNewtypeDeriving, DeriveDataTypeable,
+                       TypeFamilies, LiberalTypeSynonyms,
                        FlexibleInstances, FlexibleContexts, OverloadedStrings,
                        RecordWildCards, TypeSynonymInstances, ScopedTypeVariables
-                       MultiParamTypeClasses
+                       MultiParamTypeClasses,
+                       TemplateHaskell, QuasiQuotes
   ghc-options:         -fwarn-unused-binds -fwarn-unused-imports
 
-library
-  exposed-modules:     Dedukti.Runtime
-  build-depends:       time >= 1.1
-  extensions:          DeriveDataTypeable, PatternGuards, FlexibleInstances
-  ghc-options:         -fwarn-unused-binds -fwarn-unused-imports
+
+executable dedukti-tests
+  main-is:             Test.hs
+  if !flag(test)
+    buildable: False
+  else
+    buildable: True
+    build-depends:       directory, filepath, process,
+                         test-framework >= 0.2 && < 0.3
+    extensions:          DeriveDataTypeable, MultiParamTypeClasses,
+                         RecordWildCards
+    ghc-options:         -fwarn-unused-binds -fwarn-unused-imports
diff --git a/doc/manual.texi.in b/doc/manual.texi.in
--- a/doc/manual.texi.in
+++ b/doc/manual.texi.in
@@ -66,8 +66,8 @@
 @menu
 * Overview::            The general architecture.
 * Installation::        How to install the Dedukti system.
-* Dedukti syntax::       The input language for Dedukti.
-* Invoking dedukti::     The compiler.
+* Dedukti syntax::      The input language for Dedukti.
+* Invoking dedukti::    The compiler.
 * Invoking dkrun::      Executing the proof checks.
 * References::          Bibliographic references.
 * Copying this manual:: How you can copy and share this manual.
@@ -113,14 +113,32 @@
 @cindex Cabal
 @cindex Hackage
 Dedukti uses the Cabal architecture for building and packaging
-applications and libraries.
+applications and libraries. Regardless of the method of installation
+chosen, one needs to satisfy manually dependency on system libraries,
+such as the PCRE library. It might also be necessary to install
+development version of these packages, depending on your distribution.
 
 @menu
+* Requirements::        Required versions for compiler and libraries.
 * Local install::       Installing in your home directory.
 * Global install::      Installing in the system directories.
 * Building the documentation::     How to build the documentation.
 @end menu
 
+@node Requirements
+@section Requirements
+@cindex system libaries
+@cindex Haskell compiler
+
+Dedukti requires the Glorious Haskell Compiler (GHC) versions 6.10 and
+above to compile. Note that GHC 6.12.1 has a bug preventing a dependency
+of Dedukti to compile properly, so ulterior revisions in the 6.12 series
+are recommended.
+
+The PCRE library 7.0 or above, including the header files, must be
+present on the system before proceeding to @ref{Local install} or
+@ref{Global install}.
+
 @node Local install
 @section Installing Dedukti locally
 
@@ -208,9 +226,11 @@
 @chapter Dedukti syntax
 
 @menu
-* Syntax overview::     An informal description of input files.
-* Scoping rules::       The scope of declarations and rules.
-* Grammar::             A formal specification of the syntax.
+* Syntax overview::         An informal description of input files.
+* Pragmas::                 Use source pragmas for compiler hints.
+* Scoping rules::           The scope of declarations and rules.
+* Grammar::                 A formal specification of the syntax.
+* Prefix notation grammar:: A formal specification of an alternative syntax.
 @end menu
 
 @node Syntax overview
@@ -349,6 +369,30 @@
 @end example
 @end quotation
 
+@node Pragmas
+@section Pragmas
+@cindex pragmas
+
+Multi-line comments whose first non-blank character following the
+comment delimiter is a hash ``@verb{.#.}'' symbol are treated specially
+by Dedukti. These comments are considered @dfn{pragmas}, providing hints
+to the compilation process. The syntax of pragmas is as follows.
+Following the hash sign is the name of the pragma, in upper case. All
+remaining tokens until the closing comment delimiter are arguments to
+the pragma.
+
+Currently, the only supported pragma is the @code{FORMAT} pragma,
+expliciting the syntax of the source file in which it occurs. This
+pragma may only appear on the first line of the source file, as in the
+following:
+
+@example
+(; # FORMAT prefix ;)
+@end example
+
+This line says that the source file is in prefix notation (@pxref{Prefix
+syntax}).
+
 @node Scoping rules
 @section Scoping rules
 @cindex scoping
@@ -379,11 +423,11 @@
 toplevel ::= declaration toplevel
            | rule toplevel
            | eof
-binding ::= id : term
-declaration ::= id ":" term "."
+binding ::= id ":" term
+declaration ::= binding "."
 domain ::= id ":" applicative
          | applicative
-sort ::= Type
+sort ::= "Type"
 term ::= domain "->" term
        | domain "=>" term
        | applicative
@@ -392,19 +436,54 @@
          | "(" term ")"
 applicative ::= simple
               | applicative simple
-rule ::= env term "-->" term
+rule ::= env term "-->" term "."
 env ::= "[]"
       | "[" env2 "]"
 env2 ::= binding
        | binding "," env2
 @end example
 
+@node Prefix notation grammar
+@section Axioms and rules in prefix notation
+@cindex grammar
+@cindex syntax
+@cindex prefix notation
+@cindex polish notation
+
+For the rationale behind prefix notation, see @ref{Prefix syntax}
+
+Source files in prefix notation consist in a string of whitespace
+delimited tokens, as is the case for the human-readable format defined
+above. Unlike that format, however, there is no syntax for comments,
+though a @code{FORMAT} pragma may appear on the first line. Any token
+that is not one of the literals appearing in the grammar below is
+considered an identifier. Identifiers are period separated lists of
+characters, everything before the last period specifying the module
+qualifier for an identifier.
+
+@example
+qid ::= id.id | id
+toplevel ::= binding toplevel
+           | rule toplevel
+           | eof
+binding ::= ":" id term
+sort ::= "Type"
+term ::= "->" binding term
+       | "=>" binding term
+       | "@@" term term
+       | qid
+rule ::= "-->" env term term
+env ::= "[]"
+      | "," binding env
+@end example
+
 @node Invoking dedukti
 @chapter Invoking @command{dedukti}
 
 @menu
 * One-shot mode::       Compiling one source file at a time.
 * Batch mode::          Let Dedukti figure out what needs to be compiled.
+* Prefix syntax::       Input source files to Dedukti in alternative syntax.
 @end menu
 
 @node One-shot mode
@@ -441,7 +520,7 @@
 @node Batch mode
 @section Batch mode
 
-Compile in batch mode by passing the @code{--make} flag to
+Compile in batch mode by passing the @code{--make} option to
 @command{dedukti}. In this mode, dependencies of the file given in
 argument will be compiled first, though after the dependencies of the
 dependencies have been compiled, etc. Those dependencies that do not
@@ -453,6 +532,45 @@
 for the module given as argument and its dependencies. Compiling to
 native code often yields much better performance during checking.
 @xref{Invoking dkrun}.
+
+@node Prefix syntax
+@section Prefix syntax
+@cindex prefix notation
+@cindex polish notation
+@cindex syntax
+@cindex source files
+@cindex parsing
+
+Because Dedukti may be used as the backend proof checker for a number of
+frontend mechanized translators, proof assistants and other interactive
+environments, in many cases the input to Dedukti is not human crafted
+but mechanically generated. Dedukti therefore accepts source files in an
+alternative syntax that can be parsed much more efficiently, inspired by
+Jan Łukasiewicz' polish notation for sentential
+logic@footnote{@uref{http://en.wikipedia.org/wiki/Polish_notation}}. The
+syntax uses prefix notation for operators, much like Lisp, but unlike
+Lisp, arities for all the operators are fixed and known in advance,
+therefore no parentheses are need around subterms.
+
+This syntax for Dedukti axioms and rules is the preferred target syntax
+for automated tools that produce Dedukti code. Parsing time is at least
+an order of magnitude smaller for source files in prefix notation.
+Dedukti can automatically recognize the syntax of the source file if the
+first line of the source file is a @code{FORMAT} pragma
+(@pxref{Pragmas}). It is also possible to force a particular format
+using the following command line options:
+
+@table @option
+@item -fexternal
+Force recognizing input as (human-readable) external format.
+
+@item -fprefix-notation
+Force recognizing input as (fast) prefix format.
+
+@end table
+
+See @ref{Prefix notation grammar} for the lexical and grammatical
+structure of this syntax.
 
 @node Invoking dkrun
 @chapter Invoking @command{dkrun}
diff --git a/doc/mkfile b/doc/mkfile
--- a/doc/mkfile
+++ b/doc/mkfile
@@ -9,7 +9,7 @@
 	m4 $prereq | makeinfo -
 
 default:QV:
-	echo 'Please specify one of "html" or "pdf" as targets.'
+	echo 'Please specify one of "html", "pdf" or "info" as targets.'
 	exit 1
 
 pdf:V: manual.pdf
diff --git a/scripts/dkrun b/scripts/dkrun
--- a/scripts/dkrun
+++ b/scripts/dkrun
@@ -2,7 +2,7 @@
 
 if [ -z $* ]
 then
-    echo "Usage: dkrun module.euo [DEPENDENCY]..." 1>&2
+    echo "Usage: dkrun module.dko [DEPENDENCY]..." 1>&2
     echo "    Where all dependent modules must be listed explicitly," 1>&2
     echo "    after the module to typecheck." 1>&2
     exit 1