diff --git a/Database/Narc.hs b/Database/Narc.hs
--- a/Database/Narc.hs
+++ b/Database/Narc.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE ScopedTypeVariables, TypeSynonymInstances #-}
 {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
 
 -- | Query SQL databases using Nested Relational Calculus embedded in
@@ -7,18 +7,19 @@
 -- The primed functions in this module are in fact the syntactic 
 -- forms of the embedded language. Use them as, for example:
 -- 
--- >  foreach (table "employees" []) $ \emp ->
--- >    having (primApp "<" [cnst 20000, project emp "salary"]) $
--- >    singleton (record [(project emp "name")])
+-- > let employeesSchema = [("name", TString), ("salary", TNum)] in
+-- > let employeesTable = table "employees" employeesSchema in
+-- > foreach employeesTable $ \emp -> 
+-- >   having (primApp "<" [cnst 20000, project emp "salary"]) $
+-- >   singleton (record [("name", project emp "name")])
 
 module Database.Narc (
-  -- * The type of the embedded terms
-  NarcTerm,
   -- * Translation to an SQL representation
   narcToSQL, narcToSQLString,
+  SQL.serialize,
   -- * The language itself
-  unit, table, cnst, Constable, primApp, abs, app, ifthenelse, singleton,
-  nil, union, record, project, foreach, having,
+  unit, table, cnst, primApp, abs, app, ifthenelse, singleton,
+  nil, union, record, project, foreach, having, result,
   Type(..)
 ) where
 
@@ -95,9 +96,11 @@
 -- | A polymorphic way of embedding constants into a term.
 class Constable a where
     -- | Lift a constant value into a query.
+    -- @Constable@ types currently include @Bool@ and @Integer@.
     cnst :: a -> NarcTerm
-instance Constable Bool where cnst b = return ((!)(Bool b))
+instance Constable Bool    where cnst b = return ((!)(Bool b))
 instance Constable Integer where cnst n = return ((!)(Num n))
+instance Constable String  where cnst s = return ((!)(String s))
 
 -- | Apply some primitive function, such as @(+)@ or @avg@, to a list
 -- of arguments.
@@ -166,3 +169,12 @@
 -- argument. Corresponds to a @where@ clause in a SQL query.
 having :: NarcTerm -> NarcTerm -> NarcTerm
 having cond body = ifthenelse cond body nil
+
+-- | A shortcut for giving the typical bottom of a ``FLWOR-style''
+-- comprehension:
+--
+-- > foreach t $ \row ->
+-- > having (project x "a" > 2) $ 
+-- > result [("result", project x "b")]
+result :: [(String, NarcTerm)] -> NarcTerm
+result x = singleton $ record x
diff --git a/Database/Narc/AST.hs b/Database/Narc/AST.hs
--- a/Database/Narc/AST.hs
+++ b/Database/Narc/AST.hs
@@ -1,9 +1,9 @@
-{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}
 
 module Database.Narc.AST (
   Term'(..),
   Term,
-  Var,
+  VarName,
   PlainTerm,
   TypedTerm,
   fvs,
@@ -30,13 +30,13 @@
 -- | with named variables)
 data Term' a = Unit | Bool Bool | Num Integer | String String
              | PrimApp String [Term a]
-             | Var Var | Abs Var (Term a) | App (Term a) (Term a)
+             | Var VarName | Abs VarName (Term a) | App (Term a) (Term a)
              | Table Tabname [(Field, Type)]
              | If (Term a) (Term a) (Term a)
              | Singleton (Term a) | Nil | Union (Term a) (Term a)
              | Record [(String, Term a)]
              | Project (Term a) String
-             | Comp Var (Term a) (Term a)
+             | Comp VarName (Term a) (Term a)
 --           | IsEmpty (Term a)
     deriving (Eq,Show)
 
@@ -88,6 +88,7 @@
     | otherwise= (Comp z (rename x y src) (rename x y body), q)
 rename x y (String n, q) = (String n, q)
 rename x y (Bool b, q) = (Bool b, q)
+rename x y (Num n, q) = (Num n, q)
 rename x y (Table s t, q) = (Table s t, q)
 rename x y (If c a b, q) = (If (rename x y c) (rename x y a) (rename x y b), q)
 rename x y (Unit, q) = (Unit, q)
@@ -95,8 +96,9 @@
 rename x y (Union a b, q) = (Union (rename x y a) (rename x y b), q)
 
 -- | substTerm x v m: substite v for x in term m
--- (Actually incorrect because it does not make substitutions in the q.)
-substTerm :: Var -> Term t -> Term t -> Term t
+-- (Actually incorrect because it does not make substitutions in the
+-- annotation.)
+substTerm :: VarName -> Term t -> Term t -> Term t
 substTerm x v (m@(Unit, _))       = m
 substTerm x v (m@(Bool b, _))     = m
 substTerm x v (m@(Num n, _))      = m
@@ -148,73 +150,91 @@
 
 -- Generic term-recursion functions ------------------------------------
 
+-- | Apply a function to each term while traversing down, and use its
+-- | result as the annotation of that node.
 entagulate :: (Term a -> b) -> Term a -> Term b
-entagulate f (Bool b, d) = (Bool b, f (Bool b, d))
-entagulate f (Num n, d) = (Num n, f (Num n, d))
-entagulate f (String s, d) = (String s, f (String s, d))
-entagulate f (Var x, d) = (Var x, f (Var x, d))
-entagulate f (Abs x n, d) = (Abs x (entagulate f n), f (Abs x n, d))
-entagulate f (App l m, d) = (App (entagulate f l) (entagulate f m),
-                          f (App l m, d))
-entagulate f (If c a b, d) =
+entagulate f m@(Unit, d) = (Unit, f m)
+entagulate f m@(PrimApp fn xs, d) = (PrimApp fn (map (entagulate f) xs), f m)
+entagulate f m@(Bool b, d) = (Bool b, f m)
+entagulate f m@(Num n, d) = (Num n, f m)
+entagulate f m@(String s, d) = (String s, f m)
+entagulate f m@(Var x, d) = (Var x, f m)
+entagulate f m@(Abs x n, d) = (Abs x (entagulate f n), f m)
+entagulate f m@(App l' m', d) = (App (entagulate f l') (entagulate f m'),
+                          f m)
+entagulate f m@(If c a b, d) =
     (If (entagulate f c)
      (entagulate f a)
      (entagulate f b),
-     f (If c a b, d))
-entagulate f (Table tab fields, d) = (Table tab fields, f (Table tab fields, d))
-entagulate f (Nil, d) = (Nil, f (Nil,d))
-entagulate f (Singleton m, d) = (Singleton (entagulate f m),
-                              f (Singleton m, d))
-entagulate f (Union a b, d) =
+     f m)
+entagulate f m@(Table tab fields, d) = (Table tab fields, f m)
+entagulate f m@(Nil, d) = (Nil, f m)
+entagulate f m@(Singleton m', d) = (Singleton (entagulate f m'),
+                              f m)
+entagulate f m@(Union a b, d) =
     (Union
      (entagulate f a)
      (entagulate f b),
-     f (Union a b, d))
-entagulate f (Record fields, d) = (Record (alistmap (entagulate f) fields), 
-                                f (Record fields, d))
-entagulate f (Project m a, d) = (Project (entagulate f m) a,
-                              f (Project m a, d))
-entagulate f (Comp x src body, d) = 
-    (Comp x (entagulate f src) (entagulate f body),
-     f (Comp x src body, d))
+     f m)
+entagulate f m@(Record fields, d) =
+    (Record (alistmap (entagulate f) fields), f m)
+entagulate f m@(Project m' a, d) = (Project (entagulate f m') a, f m)
+entagulate f m@(Comp x src body, d) = 
+    (Comp x (entagulate f src) (entagulate f body), f m)
 
+-- | Apply a function to each node while traversing *up*, using its
+-- | result as the new annotation for that node.
+
+-- (FIXME: I think all this can be refactored to a nice BU/TD
+-- combinator that doesn't know about annotations.
 retagulate :: (Term a -> a) -> Term a -> Term a
 retagulate f (Unit, d) = (Unit, f (Unit, d))
 retagulate f (Bool b, d) = (Bool b, f (Bool b, d))
 retagulate f (Num n, d) = (Num n, f (Num n, d))
 retagulate f (String s, d) = (String s, f (String s, d))
 retagulate f (Var x, d) = (Var x, f (Var x, d))
-retagulate f (Abs x n, d) = (Abs x (retagulate f n),
-                             f (Abs x (retagulate f n), d))
-retagulate f (App l m, d) = (App (retagulate f l) (retagulate f m),
-                          f (App (retagulate f l) (retagulate f m), d))
-retagulate f (PrimApp fn ar, d) = (PrimApp fn (map (retagulate f) ar),
-                                   f (PrimApp fn (map (retagulate f) ar), d))
+retagulate f (Abs x n, d) =
+    let n' = (retagulate f n) in
+    let result = Abs x n' in
+    (result, f (Abs x n', d))
+retagulate f (App l m, d) = 
+    let l' = retagulate f l in
+    let m' = retagulate f m in
+    let result = App l' m' in
+    (result, f (result, d))
+retagulate f (PrimApp fn args, d) =
+    let result = PrimApp fn (map (retagulate f) args) in
+    (result, f (result, d))
 retagulate f (If c a b, d) =
-    (If (retagulate f c)
-     (retagulate f a)
-     (retagulate f b),
-     f (If (retagulate f c)
-        (retagulate f a)
-        (retagulate f b), d))
-retagulate f (Table tab fields, d) = (Table tab fields, f (Table tab fields, d))
+    let result = If (retagulate f c)
+                    (retagulate f a)
+                    (retagulate f b)
+    in
+      (result, f (result, d))
+retagulate f (Table tab fields, d) =
+    let result = Table tab fields in
+    (result, f (result, d))
 retagulate f (Nil, d) = (Nil, f (Nil, d))
-retagulate f (Singleton m, d) = (Singleton (retagulate f m),
-                              f (Singleton (retagulate f m), d))
-retagulate f (Union l m, d) = (Union (retagulate f l) (retagulate f m),
-                               f (Union (retagulate f l) (retagulate f m), d))
-retagulate f (Record fields, d) = (Record (alistmap (retagulate f) fields), 
-                                f (Record (alistmap (retagulate f) fields), d))
-retagulate f (Project m a, d) = (Project (retagulate f m) a,
-                              f (Project (retagulate f m) a, d))
+retagulate f (Singleton m, d) =
+    let result = Singleton (retagulate f m) in
+    (result, f (result, d))
+retagulate f (Union l m, d) =
+    let result = Union (retagulate f l) (retagulate f m) in
+    (result, f (result, d))
+retagulate f (Record fields, d) =
+    let result = Record (alistmap (retagulate f) fields) in
+    (result, f (result, d))
+retagulate f (Project m a, d) =
+    let result = Project (retagulate f m) a in
+    (result, f (result, d))
 retagulate f (Comp x src body, d) = 
-    (Comp x (retagulate f src) (retagulate f body),
-     f (Comp x (retagulate f src) (retagulate f body), d))
+    let result = Comp x (retagulate f src) (retagulate f body) in
+    (result, f (result, d))
 
 strip = entagulate (const ())
 
--- | numComps: Number of comprehensions in an expression, a measure of
--- the complexity of the query.
+-- | The number of comprehensions in an expression, a measure of the
+-- complexity of the query.
 numComps (Comp x src body, _) = 1 + numComps src + numComps body
 numComps (PrimApp _ args, _) = sum $ map numComps args
 numComps (Abs _ n, _) = numComps n
@@ -241,8 +261,8 @@
     num :: Integer -> result
     string :: String -> result
     primApp :: String -> [result] -> result
-    var :: Var -> result
-    abs :: Var -> result -> result
+    var :: VarName -> result
+    abs :: VarName -> result -> result
     app :: result -> result -> result
     table :: Tabname -> [(Field, Type)] -> result
     ifthenelse :: result -> result -> result -> result
@@ -251,7 +271,7 @@
     union :: result -> result -> result
     record :: [(String, result)] -> result
     project :: result -> String -> result
-    foreach :: result -> Var -> result -> result
+    foreach :: result -> VarName -> result -> result
 --    cnst :: Constable t => t -> result
 class Constable t where cnst :: NarcSem result => t -> result
 instance Constable Bool where cnst b = bool b
@@ -284,6 +304,7 @@
 class Const a where cnst_ :: a -> Term ()
 instance Const Bool where cnst_ b = (!)(Bool b)
 instance Const Integer where cnst_ n = (!)(Num n)
+instance Const String where cnst_ s = (!)(String s)
 primApp_ f args = (!)(PrimApp f args)
 var_ x = (!)(Var x)
 abs_ x body = (!)(Abs x body)
diff --git a/Database/Narc/AST/Pretty.hs b/Database/Narc/AST/Pretty.hs
--- a/Database/Narc/AST/Pretty.hs
+++ b/Database/Narc/AST/Pretty.hs
@@ -12,6 +12,7 @@
   pretty (Unit) = "()"
   pretty (Bool b) = show b
   pretty (Num n) = show n
+  pretty (String s) = show s
   pretty (PrimApp f args) = f ++ "(" ++ mapstrcat "," pretty args ++ ")"
   pretty (Var x) = x
   pretty (Abs x n) = "(fun " ++ x ++ " -> " ++ pretty n ++ ")"
diff --git a/Database/Narc/Compile.hs b/Database/Narc/Compile.hs
--- a/Database/Narc/Compile.hs
+++ b/Database/Narc/Compile.hs
@@ -8,9 +8,8 @@
 import Database.Narc.AST
 import Database.Narc.AST.Pretty ()
 import Database.Narc.Contract
-import Database.Narc.Debug (forceAndReport)
 import Database.Narc.Pretty
-import Database.Narc.SQL as SQL
+import qualified Database.Narc.SQL as SQL
 import Database.Narc.Type as Type
 import Database.Narc.TypeInfer
 import Database.Narc.Util (image, maps, alistmap)
@@ -23,8 +22,8 @@
 
 -- { Compilation } -----------------------------------------------------
 
-etaExpand :: TypedTerm -> [(String, Type)] -> TypedTerm
-etaExpand expr fieldTys =
+etaExpandRecord :: TypedTerm -> [(String, Type)] -> TypedTerm
+etaExpandRecord expr fieldTys =
     let exprTy = TRecord fieldTys in
     (Record [(field, ((Project expr field), fTy))
              | (field, fTy) <- fieldTys], 
@@ -43,7 +42,7 @@
     -- Eta-expand at record type.
     if (maps x) env then 
         case t of
-          TRecord t' -> etaExpand expr t'
+          TRecord t' -> etaExpandRecord expr t'
           _ -> (Var x, t) 
     else
       error $ "Free variable "++ x ++ " in normTerm"
@@ -53,10 +52,13 @@
     let w = normTerm env m in
     case normTerm env l of 
       (Abs x n, _) -> 
-          forceAndReport (
-            let !n' = substTerm x w n in
-            normTerm env (runTyCheck env $ n')
-          ) ("susbtituting "++show w++" for "++x++" in "++show n)
+          let n' = substTerm x w n in
+          case tryTyCheck env $ n' of
+            Right term' -> normTerm env (term')
+            Left msg -> error ("Error " ++ msg ++
+                               " substituting " ++ pretty w ++ 
+                               " for " ++ x ++ " in " ++ pretty n)
+
       (If b l1 l2, _) ->
           (normTerm env (If b (App l1 w, t) (App l2 w, t), t))
       v@(Var _, _) -> (App v w, t)
@@ -108,10 +110,12 @@
     case normTerm env src of
       (Nil, _) -> (Nil, t)
       (Singleton src', _) -> 
-          forceAndReport (
-            let !n' = substTerm x src' body in
-            normTerm env (runTyCheck env n')
-          ) ("Substituting " ++ show src' ++ " for " ++ x ++ " in " ++ show body)
+          let body' = substTerm x src' body in
+          case tryTyCheck env body' of
+            Right body'' -> normTerm env body''
+            Left msg -> error ("Error " ++ msg ++
+                               "\nWhile substituting " ++ pretty src' ++ 
+                               "\nfor " ++ x ++ "\nin " ++ pretty body)
       (Comp y src2 body2, _) ->
           -- Freshen @y@ over @src@ with respect to @body@ (that of
           -- the outer comprehension), because we're widening the
@@ -127,7 +131,7 @@
            (normTerm env (Comp x srcR body, t)), t)
       (tbl @ (Table _tableName fieldTys, _)) ->
           insert (\(v',t') -> (Comp x tbl (v',t'), t')) $
-                 let env' = Type.bind x ([],TList(TRecord fieldTys)) env in 
+                 let env' = Type.bind x ([],TRecord fieldTys) env in 
                  normTerm env' body
       (If cond' src' (Nil, _), _) ->
           assert (x `notElem` fvs cond') $
@@ -157,13 +161,13 @@
       _ -> k (v,t)
 
 -- See (Bird 2010) for a better algorithm here.
-minFreeFor :: Term a -> Var
+minFreeFor :: Term a -> VarName
 minFreeFor n = head $ variables \\ fvs n 
 
 -- | @translateTerm@ homomorphically translates a normal-form Term to an
 -- | SQL Query.
-translateTerm :: TypedTerm -> Query
-translateTerm (v `Union` u, _) = (translateTerm v) `QUnion` (translateTerm u)
+translateTerm :: TypedTerm -> SQL.Query
+translateTerm (v `Union` u, _) = (translateTerm v) `SQL.Union` (translateTerm u)
 translateTerm (Nil, _)         = SQL.emptyQuery
 translateTerm (f@(Comp _ (Table _ _, _) _, _))                  = translateF f
 translateTerm (f@(If _ _ (Nil, _), _))                          = translateF f
@@ -176,39 +180,50 @@
 -- classes (in the grammar of the normalized form) which they handle.
 -- (F for "for comprehension", Z for "final bit of a nest of
 -- comprehensions", and B for "base type"
-translateF :: Term b -> Query
+translateF :: Term b -> SQL.Query
 translateF (Comp x (Table tabname fTys, _) n, _) =
-    let q@(Select _ _ _) = translateF n in
-    Select {rslt = rslt q,
-            tabs = (tabname, x, TRecord fTys):tabs q,
-            cond = cond q}
+    let q@(SQL.Select _ _ _) = translateF n in
+    SQL.Select {SQL.rslt = SQL.rslt q,
+               SQL.tabs = (tabname, x, TRecord fTys):SQL.tabs q,
+               SQL.cond = SQL.cond q}
 translateF (z@(If _ _ (Nil, _), _))                             = translateZ z
 translateF (z@(Singleton (Record _, _), _))                     = translateZ z
 translateF (z@(Table _ _, _))                                   = translateZ z
 translateF m = error $ "translateF for unexpected term: " ++ pretty (fst m)
 
-translateZ :: Term b -> Query
+translateZ :: Term b -> SQL.Query
 translateZ (If b z (Nil, _), _) =
-    let q@(Select _ _ _) = translateZ z in
-    Select {rslt=rslt q, tabs = tabs q, cond = translateB b : cond q}
+    let q@(SQL.Select _ _ _) = translateZ z in
+    SQL.Select {SQL.rslt=SQL.rslt q,
+                   SQL.tabs = SQL.tabs q,
+                SQL.cond = translateB b : SQL.cond q}
 translateZ (Singleton (Record fields, _), _) = 
-    Select {rslt = QRecord(alistmap translateB fields), tabs = [], cond = []}
+    SQL.Select {SQL.rslt = alistmap translateB fields,
+                SQL.tabs = [],
+                SQL.cond = []}
 translateZ (Table tabname fTys, _) =
-    Select {rslt = QRecord[(l,QField tabname l)| (l,_ty) <- fTys],
-            tabs = [(tabname, tabname, TRecord fTys)], cond = []}
+    SQL.Select {SQL.rslt = [(l,SQL.Field tabname l) | (l,_ty) <- fTys],
+                SQL.tabs = [(tabname, tabname, TRecord fTys)],
+                SQL.cond = []}
 translateZ z = error$ "translateZ got unexpected term: " ++ (pretty.fst) z
 
-translateB :: Term b -> Query
-translateB (If b b' b'', _)            = QIf (translateB b)
+translateB :: Term b -> SQL.QBase
+translateB (If b b' b'', _)            = SQL.If (translateB b)
                                            (translateB b') (translateB b'') 
-translateB (Bool n, _)                 = (QBool n)
-translateB (Num n, _)                  = (QNum n)
-translateB (Project (Var x, _) l, _)   = QField x l
-translateB (PrimApp "not" [arg], _)    = QNot (translateB arg)
-translateB (PrimApp "<" [l, r], _)     = QOp (translateB l) Less (translateB r)
+translateB (Bool n, _)                 = (SQL.Lit (SQL.Bool n))
+translateB (Num n, _)                  = (SQL.Lit (SQL.Num n))
+translateB (String s, _)               = (SQL.Lit (SQL.String s))
+translateB (Project (Var x, _) l, _)   = SQL.Field x l
+translateB (PrimApp "not" [arg], _)    = SQL.Not (translateB arg)
+translateB (PrimApp "<" [l, r], _)   = SQL.Op (translateB l) SQL.Less (translateB r)
+translateB (PrimApp "=" [l, r], _)   = SQL.Op (translateB l) SQL.Eq (translateB r)
+translateB (PrimApp "+" [l, r], _)   = SQL.Op (translateB l) SQL.Plus (translateB r)
+translateB (PrimApp "-" [l, r], _)   = SQL.Op (translateB l) SQL.Minus (translateB r)
+translateB (PrimApp "*" [l, r], _)   = SQL.Op (translateB l) SQL.Times (translateB r)
+translateB (PrimApp "/" [l, r], _)   = SQL.Op (translateB l) SQL.Divide (translateB r)
 translateB b = error$ "translateB got unexpected term: " ++ (pretty.fst) b
 
-compile :: TyEnv -> TypedTerm -> Query
+compile :: TyEnv -> TypedTerm -> SQL.Query
 compile env = translateTerm . normTerm env
 
 -- -- Tests
diff --git a/Database/Narc/Eval.hs b/Database/Narc/Eval.hs
--- a/Database/Narc/Eval.hs
+++ b/Database/Narc/Eval.hs
@@ -14,18 +14,20 @@
 
 -- type RuntimeTerm = Term (Maybe Query)
 
-type Env = [(Var, Value)]
+type Env = [(VarName, Value)]
 
-data Value = VUnit | VBool Bool | VNum Integer
+data Value = VUnit | VBool Bool | VNum Integer | VString String
             | VList [Value]
             | VRecord [(String, Value)]
-            | VAbs Var TypedTerm Env
+            | VAbs VarName TypedTerm Env
         deriving (Eq, Show)
 
+-- | Inject a data value back into a literal term that denotes it.
 fromValue :: Value -> TypedTerm
 fromValue VUnit = (Unit, undefined)
 fromValue (VBool b) = (Bool b, undefined)
 fromValue (VNum n) = (Num n, undefined)
+fromValue (VString s) = (String s, undefined)
 fromValue (VList xs) = foldr1 union (map singleton $ map fromValue xs)
     where union x y = (x `Union` y, undefined)
           singleton x = (Singleton x, undefined)
@@ -56,6 +58,7 @@
 eval env (Unit, _) = (VUnit)
 eval env (Bool b, q) = (VBool b)
 eval env (Num n, q) = (VNum n)
+eval env (String s, q) = (VString s)
 eval env (PrimApp prim args, q) = 
     let (vArgs) = map (eval env) args in
     (appPrim prim vArgs)
diff --git a/Database/Narc/Failure.hs b/Database/Narc/Failure.hs
--- a/Database/Narc/Failure.hs
+++ b/Database/Narc/Failure.hs
@@ -31,10 +31,12 @@
 type ErrorGensym a = ErrorT String Gensym a
 
 -- | Run an ErrorGensym action, raising errors with `error'.
+runErrorGensym :: ErrorT String Gensym a -> a
 runErrorGensym = runError . runGensym . runErrorT
 
 -- | Try running an ErrorGensym action, packaging result in an Either
 -- | with Left as failure, Right as success.
+tryErrorGensym :: ErrorT e Gensym a -> Either e a
 tryErrorGensym = runGensym . runErrorT
 
 under x = either throwError return x
diff --git a/Database/Narc/SQL.hs b/Database/Narc/SQL.hs
--- a/Database/Narc/SQL.hs
+++ b/Database/Narc/SQL.hs
@@ -1,3 +1,5 @@
+-- | A direct representation of SQL queries.
+
 module Database.Narc.SQL where
 
 import Data.List (nub, intercalate)
@@ -6,120 +8,84 @@
 import Database.Narc.Type
 import Database.Narc.Util (u, mapstrcat)
 
---
--- SQL Queries ---------------------------------------------------------
---
+import Unary
 
+-- | The representation of SQL queries (e.g. @select R from Ts where B@)
+
+-- (This is unpleasant; it should probably be organized into various
+-- syntactic classes.)
+data Query =
+    Select {
+      rslt :: Row,
+      tabs :: [(Tabname, Tabname, Type)],
+      cond :: [QBase]
+    }
+    | Union Query Query
+      deriving(Eq, Show)
+
+type Row = [(Field, QBase)]
+
+-- | Atomic-typed query fragments.
+data QBase =
+      Lit DataItem
+    | Not QBase
+    | Op QBase Op QBase
+    | Field String String
+    | If QBase QBase QBase
+    | Exists Query
+      deriving (Eq, Show)
+
+data DataItem = Num Integer
+              | Bool Bool
+              | String String
+  deriving (Eq, Show)
+
+-- | Binary operators used in queries.
 data Op = Eq | Less
         | Plus | Minus | Times | Divide
         deriving(Eq, Show)
 
+-- | Unary operators used in queries.
 data UnOp = Min | Max | Count | Sum | Average
         deriving (Eq, Show)
 
--- | Query: the type of SQL queries ("select R from Ts where B")
--- (This is unpleasant; it should probably be organized into various
--- syntactic classes.)
-data Query = Select {rslt :: Query,                  -- make this a list
-                     tabs :: [(Field, Field, Type)], -- use [(Field,Type)]
-                     cond :: [Query]
-                    }
-           | QNum Integer
-           | QBool Bool
-           | QNot Query
-           | QOp Query Op Query
-           | QField String String
-           | QRecord [(Field, Query)]
-           | QUnion Query Query
-           | QIf Query Query Query
-           | QExists Query
-        deriving(Eq, Show)
-
-emptyQuery = Select {rslt = QRecord [], tabs = [], cond = [QBool False]}
-
--- | @sizeQuery@ approximates the size of a query by calling giving up
--- | its node count past a certain limit (currently limit = 100, below).
-sizeQueryExact :: Query -> Integer
-sizeQueryExact (q@(Select _ _ _)) =
-    sizeQueryExact (rslt q) + (sum $ map sizeQueryExact (cond q))
-sizeQueryExact (QNum n) = 1
-sizeQueryExact (QBool b) = 1
-sizeQueryExact (QNot q) = 1 + sizeQueryExact q
-sizeQueryExact (QOp a op b) = 1 + sizeQueryExact a + sizeQueryExact b
-sizeQueryExact (QField t f) = 1
-sizeQueryExact (QRecord fields) = sum [sizeQueryExact n | (a, n) <- fields]
-sizeQueryExact (QUnion m n) = sizeQueryExact m + sizeQueryExact n
-sizeQueryExact (QIf c a b) = sizeQueryExact c + sizeQueryExact a + sizeQueryExact b
-sizeQueryExact (QExists q) = 1 + sizeQueryExact q
-
--- | @sizeQuery@ approximates the size of a query by calling giving up
--- | its node count past a certain limit (currently limit = 100, below).
-sizeQuery :: Query -> Integer
-sizeQuery qy = loop 0 qy
-    where
-      loop' :: Integer -> Query -> Integer
-      loop' n qy = if n > limit then n else loop n qy
+-- | The trivial query, returning no rows.
+emptyQuery = Select {rslt = [], tabs = [], cond = [Lit (Bool False)]}
 
-      loop :: Integer -> Query -> Integer
-      loop n (q@(Select _ _ _)) = 
-          let n' = foldr (\r n -> loop' n r) n (cond q) in
-          loop' n' (rslt q)
-      loop n (QNum i) = n + 1
-      loop n (QBool b) = n + 1
-      loop n (QNot q) = loop' (n+1) q
-      loop n (QOp a op b) = let n' = loop' (n+1) a in loop' n' b
-      loop n (QField t f) = n + 1
-      loop n (QRecord fields) = foldr (\r n -> loop' n r) n (map snd fields)
-      loop n (QUnion a b) = let n' = loop' (n+1) a in loop' n' b
-      loop n (QIf c a b) = 
-          let n' = loop' (n+1) c in
-          let n'' = loop' n' a in
-          loop' n'' b
-      loop n (QExists q) = loop' (n+1) q
+-- | @sizeQuery@ returns the number of nodes in a query. It's
+-- | abstracted to Num to allow using Unary, and then ``lazily''
+-- | counting up to a certain amount. This helps if you only want to
+-- | know whether a (potentially-enormous) query is larger than some
+-- | modest cutoff.
+sizeQuery :: Num a => Query -> a
+sizeQuery  (q@(Select _ _ _)) =
+    1 + (sum (map sizeQueryB (cond q)) +
+       sum (map sizeQueryB (map snd (rslt q))))
+sizeQuery (Union a b) = 1 + (sizeQuery a + sizeQuery b)
 
-      limit = 100
+sizeQueryB :: Num a => QBase -> a
+sizeQueryB (Lit _)     = 1
+sizeQueryB (Not q)     = 1 + (sizeQueryB q)
+sizeQueryB (Op a op b) = 1 + (sizeQueryB a + sizeQueryB b)
+sizeQueryB (If c a b)  = 1 + (sizeQueryB c + sizeQueryB a + sizeQueryB b)
+sizeQueryB (Field t f) = 1
+sizeQueryB (Exists q)  = 1 + (sizeQuery q)
 
 -- Basic functions on query expressions --------------------------------
 
 freevarsQuery (q@(Select _ _ _)) = 
-    (freevarsQuery (rslt q))
+    (concatMap (freevarsQueryB . snd)  (rslt q))
     `u`
-    (nub $ concat $ map freevarsQuery (cond q))
-freevarsQuery (QOp lhs op rhs) = nub (freevarsQuery lhs ++ freevarsQuery rhs)
-freevarsQuery (QRecord fields) = concatMap (freevarsQuery . snd) fields
+    (nub $ concat $ map freevarsQueryB (cond q))
 freevarsQuery _ = []
 
-isQRecord (QRecord _) = True
-isQRecord _ = False
-
--- | a groundQuery is a *real* SQL query--one without variables or appl'ns.
-groundQuery :: Query -> Bool
-groundQuery (qry@(Select _ _ _)) =
-    all groundQueryExpr (cond qry) &&
-    groundQueryExpr (rslt qry) &&
-    isQRecord (rslt qry)
-groundQuery (QUnion a b) = groundQuery a && groundQuery b
-groundQuery (QExists qry) = groundQuery qry
-groundQuery (QRecord fields) = all (groundQuery . snd) fields
-groundQuery (QOp b1 _ b2) = groundQuery b1 && groundQuery b2
-groundQuery (QNum _) = True
-groundQuery (QBool _) = True
-groundQuery (QField _ _) = True
-groundQuery (QNot a) = groundQuery a
-
--- | a groundQueryExpr is an atomic-type expression.
-groundQueryExpr :: Query -> Bool
-groundQueryExpr (qry@(Select _ _ _)) = False
-groundQueryExpr (QUnion a b) = False
-groundQueryExpr (QExists qry) = groundQuery qry
-groundQueryExpr (QRecord fields) = all (groundQueryExpr . snd) fields
-groundQueryExpr (QOp b1 _ b2) = groundQueryExpr b1 && groundQueryExpr b2
-groundQueryExpr (QNot a) = groundQueryExpr a
-groundQueryExpr (QNum _) = True
-groundQueryExpr (QBool _) = True
-groundQueryExpr (QField _ _) = True
-groundQueryExpr (QIf c a b) = all groundQueryExpr [c,a,b]
+freevarsQueryB (Op lhs op rhs) =
+    nub (freevarsQueryB lhs ++ freevarsQueryB rhs)
+freevarsQueryB (Not arg) = freevarsQueryB arg
+freevarsQueryB _ = []
 
+-- | Serialize a @Query@ to its ASCII SQL serialization.
+-- Dies on those @Query@s that don't represent valid SQL queries.
 serialize :: Query -> String
 serialize q@(Select _ _ _) =
     "select " ++ serializeRow (rslt q) ++
@@ -127,29 +93,32 @@
     " where " ++ if null (cond q) then
                      "true"
                  else mapstrcat " and " serializeAtom (cond q)
-serialize (QUnion l r) =
+serialize (Union l r) =
     "(" ++ serialize l ++ ") union (" ++ serialize r ++ ")"
 
-serializeRow (QRecord flds) =
+serializeRow (flds) =
     mapstrcat ", " (\(x, expr) -> serializeAtom expr ++ " as " ++ x) flds
 
-serializeAtom (QNum i) = show i
-serializeAtom (QBool b) = show b
-serializeAtom (QNot expr) = "not(" ++ serializeAtom expr ++ ")"
-serializeAtom (QOp l op r) = 
+serializeAtom (Lit lit) = serializeLit lit
+serializeAtom (Not expr) = "not(" ++ serializeAtom expr ++ ")"
+serializeAtom (Op l op r) = 
     serializeAtom l ++ " " ++ serializeOp op ++ " " ++ serializeAtom r
-serializeAtom (QField rec fld) = rec ++ "." ++ fld
-serializeAtom (QIf cond l r) = 
+serializeAtom (Field rec fld) = rec ++ "." ++ fld
+serializeAtom (If cond l r) = 
     "case when " ++ serializeAtom cond ++
     " then " ++ serializeAtom l ++
     " else " ++ serializeAtom r ++
     " end)"
-serializeAtom (QExists q) =
+serializeAtom (Exists q) =
     "exists (" ++ serialize q ++ ")"
 
+serializeLit (Num i) = show i
+serializeLit (Bool b) = show b
+serializeLit (String s) = show s
+
 serializeOp Eq = "="
 serializeOp Less = "<"
-serializeOp Plus = "<"
-serializeOp Minus = "<"
-serializeOp Times = "<"
-serializeOp Divide = "<"
+serializeOp Plus = "+"
+serializeOp Minus = "-"
+serializeOp Times = "*"
+serializeOp Divide = "/"
diff --git a/Database/Narc/SQL/Pretty.hs b/Database/Narc/SQL/Pretty.hs
--- a/Database/Narc/SQL/Pretty.hs
+++ b/Database/Narc/SQL/Pretty.hs
@@ -5,7 +5,7 @@
 import Database.Narc.Util (mapstrcat)
 
 instance Pretty Query where
-  pretty (Select{rslt=QRecord flds, tabs=tabs, cond=cond}) = 
+  pretty (Select{rslt=flds, tabs=tabs, cond=cond}) = 
          "select " ++ mapstrcat ", " (\(alias, expr) -> 
                                           pretty expr ++ " as " ++ alias)
                       flds ++ 
@@ -15,25 +15,33 @@
          " where " ++ pretty_cond cond
                    where pretty_cond [] = "true"
                          pretty_cond cond = mapstrcat " and " pretty cond
-  pretty (QOp lhs op rhs) = pretty lhs ++ pretty op ++ pretty rhs
-  pretty (QRecord fields) = "{"++ mapstrcat ", "
-                               (\(lbl,expr) -> 
-                                    lbl ++ "=" ++ show expr) fields
-                          ++ "}"
-  pretty (QNum n) = show n
-  pretty (QBool True) = "true"
-  pretty (QBool False) = "false"
+
+  pretty (Union a b) = pretty a ++ " union all " ++ pretty b
+
+instance Pretty QBase where
+  pretty (Lit lit) = pretty lit
    
-  pretty (QField a b) = a ++ "." ++ b
+  pretty (Field a b) = a ++ "." ++ b
+  pretty (Not b) = "not " ++ pretty b
+  pretty (Op lhs op rhs) = pretty lhs ++ pretty op ++ pretty rhs
 
-  pretty (QUnion a b) = pretty a ++ " union all " ++ pretty b
-  pretty (QNot b) = "not " ++ pretty b
-  pretty (QIf c t f) = "if " ++ pretty c ++ " then " ++ pretty t
+  pretty (If c t f) = "if " ++ pretty c ++ " then " ++ pretty t
                        ++ " else " ++ pretty f
 
+  pretty (Exists q) = "exists (" ++ pretty q ++ ")"
+
+instance Pretty DataItem where
+  pretty (Num n) = show n
+  pretty (String s) = show s -- FIXME use SQL-style quoting.
+  pretty (Bool True) = "true"
+  pretty (Bool False) = "false"
+
 -- Pretty-printing for Op, common to both AST and SQL languages.
 
 instance Pretty Op where
-  pretty Plus = " + "
-  pretty Eq = " = "
-  pretty Less = " < "
+  pretty Plus   = " + "
+  pretty Minus  = " - "
+  pretty Times  = " * "
+  pretty Divide = " / "
+  pretty Eq     = " = "
+  pretty Less   = " < "
diff --git a/Database/Narc/TermGen.hs b/Database/Narc/TermGen.hs
--- a/Database/Narc/TermGen.hs
+++ b/Database/Narc/TermGen.hs
@@ -39,7 +39,7 @@
         ]
 
 -- | Generate a random term, unlikely to be well-typed.
-termGen :: [Var] -> Int -> Gen (Term ())
+termGen :: [VarName] -> Int -> Gen (Term ())
 termGen fvs size = frequency $
     [(1,                    return (Unit, ())),
      (1, do b <- arbitrary; return (Bool b, ())),
diff --git a/Database/Narc/Test.hs b/Database/Narc/Test.hs
--- a/Database/Narc/Test.hs
+++ b/Database/Narc/Test.hs
@@ -3,12 +3,12 @@
 module Database.Narc.Test where
 
 import Prelude hiding (catch)
-import Control.Monad.State hiding (when, join)
 import Control.Monad.Error ({- Error(..), throwError, -} runErrorT)
 
 import Test.QuickCheck hiding (promote, Failure)
 import Test.HUnit hiding (State, assert)
 
+import Unary
 import Gensym
 import QCUtils
 
@@ -20,46 +20,45 @@
 import Database.Narc.TypeInfer
 import Database.Narc.TermGen
 
-makeNormalizerTests :: ErrorGensym Test
-makeNormalizerTests = 
-    do initialTyEnv <- makeInitialTyEnv 
-       return$ TestList 
-                 [TestCase $ unitAssert $ 
-                  let term = (Comp "x" (Table "foo" [("fop", TNum)], ())
-                              (If (Bool True,())
-                               (Singleton (Record
-                                           [("f0", (Project (Var "x", ())
-                                                    "fop",()))],()),())
-                               (Singleton (Record 
-                                           [("f0", (Num 3, ()))], ()), ()), 
-                               ()), ()) in
-                  let tyTerm = runErrorGensym $ infer $ term in
-                  SQL.groundQuery $ compile initialTyEnv $ tyTerm
-                 ]
+normalizerTests :: Test
+normalizerTests = 
+    TestList [
+        TestCase $ unitAssert $ 
+        -- TBD: use builders here.
+        let term = (Comp "x" (Table "foo" [("fop", TNum)], ())
+                    (If (Bool True,())
+                     (Singleton (Record
+                                 [("f0", (Project (Var "x", ())
+                                          "fop",()))],()),())
+                     (Singleton (Record 
+                                 [("f0", (Num 3, ()))], ()), ()), 
+                     ()), ()) in
+        let typedTerm = runErrorGensym $ infer $ term in
+        (1::Integer) < (SQL.sizeQuery $ compile [] $ typedTerm)
+    ]
 
-unitTests :: ErrorGensym Test
-unitTests = do normalizerTests <- makeNormalizerTests 
-               return $ TestList [tyCheckTests, normalizerTests, typingTest]
+unitTests :: Test
+unitTests = TestList [tyCheckTests, normalizerTests, typingTest]
 
 runUnitTests :: IO Counts
-runUnitTests = runErrorGensym $ liftM runTestTT unitTests
+runUnitTests = runTestTT $ unitTests
 
 --
 -- Big QuickCheck properties
 --
 
--- | Assertion that well-typed terms evaluate without throwing.
-prop_eval_safe :: Property
-prop_eval_safe = 
+-- | Assertion that well-typed terms compile without throwing.
+prop_compile_safe :: Property
+prop_compile_safe = 
     forAll dbTableTypeGen $ \ty ->
     forAll (sized (closedTypedTermGen ty)) $ \m ->
     case tryErrorGensym (infer m) of
       Left _ -> label "ill-typed" $ property True -- ignore ill-typed terms
                                                   -- but report their occurence.
       Right (m'@(_, ty)) -> 
-          isDBTableTy ty ==>
+          classify (isDBTableTy ty) "Flat relation type" $
             let q = (compile [] $! m') in
-            collect (SQL.sizeQuery q) $  -- NB: Counts sizes only up to ~100.
+            collect (min 100 (SQL.sizeQuery q::Unary)) $  -- NB: Counts sizes only up to ~100.
                     excAsFalse (q == q)  -- Self-comparison forces the
                                          -- value (?) thus surfacing
                                          -- any @error@s that might be
@@ -68,7 +67,7 @@
 prop_typedTermGen_tyCheck :: Property
 prop_typedTermGen_tyCheck =
   forAll (sized $ typeGen []) $ \ty ->
-  forAll (sized $ typedTermGen (runErrorGensym makeInitialTyEnv) ty) $ \m ->
+  forAll (sized $ typedTermGen [] ty) $ \m ->
   case runGensym $ runErrorT $ infer m of
     Left _ -> False
     Right (_m', ty') -> isErrorMSuccess $ unify ty ty'
@@ -77,6 +76,7 @@
 
 main :: IO ()
 main = do
-  quickCheckWith tinyArgs prop_eval_safe
+  quickCheckWith tinyArgs prop_typedTermGen_tyCheck
+  quickCheckWith tinyArgs prop_compile_safe
   _ <- runUnitTests
   return ()
diff --git a/Database/Narc/Type.hs b/Database/Narc/Type.hs
--- a/Database/Narc/Type.hs
+++ b/Database/Narc/Type.hs
@@ -28,7 +28,7 @@
 
 type TySubst = [(Int, Type)]
 
-type TyEnv = [(Var, QType)]
+type TyEnv = [(VarName, QType)]
 
 -- Operations on types, rows and substitutions ------------------------
 
diff --git a/Database/Narc/TypeInfer.hs b/Database/Narc/TypeInfer.hs
--- a/Database/Narc/TypeInfer.hs
+++ b/Database/Narc/TypeInfer.hs
@@ -12,6 +12,8 @@
 import Database.Narc.Type
 import Database.Narc.Failure
 import Database.Narc.Debug (debug)
+import Database.Narc.Pretty
+import Database.Narc.AST.Pretty
 
 --
 -- Type inference ------------------------------------------------------
@@ -29,7 +31,7 @@
 -- an entry (x, qty) indicates that variable x has the quantified type qty;
 -- a QType (ys, ty) indicates the type "forall ys, ty".
 tyCheck :: TyEnv -> Term a
-        -> ErrorGensym (TySubst, Term Type)
+        -> ErrorGensym (TySubst, TypedTerm)
 tyCheck env (Unit, _) = 
     do let ty = (TUnit)
        return (emptyTySubst, (Unit, ty))
@@ -110,7 +112,7 @@
                   Just fieldTy ->
                       return (tySubst,
                               (Project m' f, fieldTy))
-         _ -> fail("Project from non-record type.")
+         _ -> fail ("Project from non-record type: " ++ pretty (Project m f))
 tyCheck env (App m n, _) = 
     do a <- lift gensym; b <- lift gensym;
        (mTySubst, m'@(_, (mTy))) <- tyCheck env m
@@ -132,29 +134,25 @@
 
 tyCheck env term@(Comp x src body, d) =
     do (substSrc, src') <- tyCheck env src
-       let srcTy = typeAnno src'
+       let srcTy = annotation src'
        a <- lift gensym
        srcTySubst <- under $ unify (TList (TVar a)) srcTy
        let srcTy' = applyTySubst srcTySubst (TVar a)
        (substBody, body') <- tyCheck ((x, unquantType srcTy') : env) body
-       let bodyTy = typeAnno body'
+       let bodyTy = annotation body'
        resultSubst <- under $ composeTySubst [substSrc, substBody]
        return (resultSubst, (Comp x src' body', bodyTy))
 
 unquantType ty = ([], ty)
 
-typeAnno :: Term Type -> Type
-typeAnno (_, ty) = ty
-
-makeInitialTyEnv :: ErrorGensym [(String, QType)]
-makeInitialTyEnv = return []
+annotation :: TypedTerm -> Type
+annotation (_, ty) = ty
 
 infer :: Term a -> ErrorGensym TypedTerm -- FIXME broken, discards subst'n
 infer term =
-    do initialTyEnv <- makeInitialTyEnv
-       (_, term') <-
+    do (_, term') <-
         --    runErrorGensym $ 
-               tyCheck initialTyEnv term
+               tyCheck [] term
        return term'
 
 infer' :: Term' a -> ErrorGensym TypedTerm
@@ -162,11 +160,16 @@
 
 runInfer = runErrorGensym . infer
 
-runTyCheck env m = runErrorGensym $ 
-    do initialTyEnv <- makeInitialTyEnv
-       (subst, m') <- tyCheck (initialTyEnv++env) m
+typeAnnotate env m =
+    do (subst, m') <- tyCheck env m
        return $ retagulate (applyTySubst subst . snd) m'
 
+runTyCheck :: [(VarName, QType)] -> Term a -> TypedTerm
+runTyCheck env m = runErrorGensym $ typeAnnotate env m
+
+tryTyCheck :: [(VarName, QType)] -> Term a -> Either String TypedTerm
+tryTyCheck env m = tryErrorGensym $ typeAnnotate env m
+
 inferTys :: Term () -> ErrorGensym Type
 inferTys m = 
     do (_, (ty)) <- infer m
@@ -227,7 +230,9 @@
   in
   (resultTy, funcArgSubst,
    case resultTy of
-   TArr (TList (TList (TVar a))) (TList (TVar b)) -> a == b)
+   TArr (TList (TList (TVar a))) (TList (TVar b)) -> a == b
+   _ -> False    -- unexpected form of result!
+  )
 
 typingTest = let (_,_,x) = typingTest1 in 
              TestCase (unitAssert x)
diff --git a/Database/Narc/Util.hs b/Database/Narc/Util.hs
--- a/Database/Narc/Util.hs
+++ b/Database/Narc/Util.hs
@@ -34,6 +34,7 @@
     where reduceGroup xs = let (as, bs) = unzip xs in
                              (the as, agg bs)
           the xs | allEq xs = head xs
+          the _ = error "Argument to 'the' non-unique"
 
 onCorresponding :: Ord a => ([b]->c) -> [(a,b)] -> [c]
 onCorresponding agg xs = map reduceGroup (collate fst xs)
diff --git a/Database/Narc/Var.hs b/Database/Narc/Var.hs
--- a/Database/Narc/Var.hs
+++ b/Database/Narc/Var.hs
@@ -1,4 +1,4 @@
 module Database.Narc.Var where
 
-type Var = String
+type VarName = String
 
diff --git a/Unary.hs b/Unary.hs
new file mode 100644
--- /dev/null
+++ b/Unary.hs
@@ -0,0 +1,58 @@
+module Unary where
+
+data Unary = Z | S Unary
+    deriving (Eq)
+
+instance Num Unary where
+    Z     + y = y
+    x     + Z = x
+    (S x) + y = S (x `rightPlus` y)
+
+    abs x = x
+    signum Z = Z
+    signum (S x) = S Z
+    fromInteger x | 0 == x = Z
+                  | 0 <= x = S (fromInteger (x-1))
+                  | otherwise = unaryUnderflow
+
+    -- | Multiplication. Discouraged because slow.
+    Z * y = Z
+    x * Z = Z
+    (S x) * y = y + (x * y)
+
+unaryUnderflow = error "unary represents positive integers only"
+
+instance Ord Unary where
+    min Z y = Z
+    min x Z = Z
+    min (S x) (S y) = S (min x y)
+    x < Z = False
+    Z < S y = True
+    S x < S y = x < y
+
+instance Show Unary where
+    show x = show (toInteger x)
+
+instance Enum Unary where
+    succ x = S x
+    pred (S x) = x
+    pred Z = error "No pred of Z"
+    toEnum x | 0 <= x = foldr (const S) Z [1..x]
+             | x < 0 = unaryUnderflow
+    fromEnum Z = 0
+    fromEnum (S x) = 1 + fromEnum x
+
+instance Real Unary where
+    toRational x = error "toRational undefined"
+
+instance Integral Unary where
+    toInteger Z = 0
+    toInteger (S x) = 1 + toInteger x
+    quotRem x y = let (q,r) = (quotRem (toInteger x) (toInteger y)) in
+                  (fromInteger q, fromInteger r)
+
+-- | Right-recursive version of (+), to balance the recursion.
+rightPlus :: Unary -> Unary -> Unary
+rightPlus Z     y = y
+rightPlus x     Z = x
+rightPlus x (S y) = S (x + y)
diff --git a/narc.cabal b/narc.cabal
--- a/narc.cabal
+++ b/narc.cabal
@@ -7,14 +7,14 @@
 -- The package version. See the Haskell package versioning policy
 -- (http://www.haskell.org/haskellwiki/Package_versioning_policy) for
 -- standards guiding when and how versions should be incremented.
-Version:             0.1.2
+Version:             0.1.3
 
 -- A short (one-line) description of the package.
 Synopsis:            Query SQL databases using Nested Relational Calculus embedded in Haskell.
 
 -- A longer description of the package.
 Description:         Narc is an embedded language for querying SQL databases, 
-		     which permits using the "nested relational" model, a more
+		     which permits using the ``nested relational'' model, a more
 		     flexible model than the traditional relational model of SQL
 		     databases. In spite of this richer data model, queries are
 		     transformed into SQL to run against standard databases.
@@ -63,13 +63,13 @@
 
 Library
   -- Modules exported by the library.
-  Exposed-modules:     Database.Narc, Database.Narc.SQL, Database.Narc.Test, Database.Narc.Type, Database.Narc.HDBC
+  Exposed-modules:     Database.Narc, Database.Narc.Test, Database.Narc.Type, Database.Narc.HDBC
   
   -- Packages needed in order to build this package.
   Build-depends: base >=4 && < 5, HUnit, QuickCheck, mtl, random, HDBC
   
   -- Modules not exported by this package.
-  Other-modules:       Gensym, QCUtils, Database.Narc.TermGen, Database.Narc.Var, Database.Narc.Contract, Database.Narc.Debug, Database.Narc.TypeInfer, Database.Narc.Util, Database.Narc.AST.Pretty, Database.Narc.Failure.QuickCheck, Database.Narc.Rewrite, Database.Narc.AST, Database.Narc.Common, Database.Narc.Compile, Database.Narc.Eval, Database.Narc.Failure, Database.Narc.Pretty, Database.Narc.SQL.Pretty
+  Other-modules:       Gensym, QCUtils, Unary, Database.Narc.TermGen, Database.Narc.Var, Database.Narc.Contract, Database.Narc.Debug, Database.Narc.TypeInfer, Database.Narc.Util, Database.Narc.AST.Pretty, Database.Narc.Failure.QuickCheck, Database.Narc.Rewrite, Database.Narc.AST, Database.Narc.Common, Database.Narc.Compile, Database.Narc.Eval, Database.Narc.Failure, Database.Narc.Pretty, Database.Narc.SQL.Pretty, Database.Narc.SQL
   
   -- Extra tools (e.g. alex, hsc2hs, ...) needed to build the source.
   -- Build-tools: