diff --git a/Gensym.hs b/Gensym.hs
new file mode 100644
--- /dev/null
+++ b/Gensym.hs
@@ -0,0 +1,30 @@
+module Gensym (
+    Gensym(..), gensym, runGensym
+  ) where
+
+import Control.Applicative
+
+-- Gensym monad
+
+data Gensym a = G (Int -> (Int, a))
+
+instance Monad Gensym where
+    return v = G(\x -> (x,v))
+    m >>= k = G(\x -> let G f = m in
+                      let (x', v) = f x in 
+                      let G f' = k v in f' x')
+
+instance Functor Gensym where
+    fmap f x = x >>= (return . f)
+
+instance Control.Applicative.Applicative Gensym where
+    pure = return
+    f <*> x = do f' <- f ; x' <- x ; return (f' x')
+
+gensym :: Gensym Int
+gensym = G(\x -> (x+1, x))
+
+runGensym (G f) = snd $ f 0
+
+instance Show a => Show (Gensym a) where
+    show x = show $ runGensym x
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,26 @@
+Copyright (c) 2008-2011, Ezra e. k. Cooper
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Narc.hs b/Narc.hs
new file mode 100644
--- /dev/null
+++ b/Narc.hs
@@ -0,0 +1,200 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+
+-- | Query SQL databases using Nested Relational Calculus embedded in
+-- Haskell.
+-- 
+-- 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")])
+
+module Narc (
+  -- * The type of the embedded terms
+  NarcTerm,
+  -- * Translation to an SQL representation
+  narcTermToSQL,
+  -- * The language itself
+  unit, Const, primApp, abs, app, ifthenelse, singleton,
+  nil, union, record, project, foreach, having
+) where
+
+import Prelude hiding (abs, catch)
+import Control.Exception (catch, throwIO, evaluate, SomeException)
+import Control.Monad.State hiding (when, join)
+import Control.Monad.Error (throwError, runErrorT, Error(..))
+import Data.List (nub, (\\), sort, sortBy, groupBy, intersperse)
+import Data.Maybe (fromJust, isJust, fromMaybe)
+
+import Control.Applicative ((<$>), (<*>))
+import Foreign (unsafePerformIO)            -- FIXME
+
+import Test.QuickCheck hiding (promote, Failure)
+import QCUtils
+import Test.HUnit hiding (State, assert)
+
+import Debug.Trace
+
+import Gensym
+
+import Narc.AST
+import Narc.Common
+import Narc.Compile
+import Narc.Debug
+import Narc.Eval
+import Narc.Failure
+import Narc.Pretty
+import Narc.AST.Pretty
+import Narc.SQL.Pretty
+import qualified Narc.SQL as SQL
+import Narc.Type as Type
+import Narc.TypeInfer
+import Narc.Util
+
+import Narc.HDBC
+
+-- THE AWESOME FULL COMPILATION FUNCTION -------------------------------
+
+typeCheckAndCompile :: Term a -> SQL.Query
+typeCheckAndCompile = compile [] . runTyCheck []
+
+-- The Narc embedded langauge-------------------------------------------
+
+-- Example query
+
+example_dull = (Comp "x" (Table "foo" [("a", TBool)], ())
+                (If (Project (Var "x", ()) "a", ())
+                 (Singleton (Var "x", ()), ())
+                 (Nil, ()), ()), ())
+
+-- HOAS-ish embedded language.
+
+type NarcTerm = Gensym (Term ()) -- ^ Bleck. Rename.
+
+-- | Translate a Narc term to an SQL query string--perhaps the central
+-- | function of the interface.
+narcTermToSQLString :: NarcTerm -> String
+narcTermToSQLString = SQL.serialize . narcTermToSQL
+
+-- | Translate a Narc term to an SQL query.
+narcTermToSQL :: NarcTerm -> SQL.Query
+narcTermToSQL = typeCheckAndCompile . realize
+
+-- | Turn a HOAS representation of a Narc term into a concrete,
+-- | named-binder representation.
+realize :: NarcTerm -> Term ()
+realize = runGensym
+
+-- | A dummy value, or zero-width record.
+unit :: NarcTerm
+unit = return $ (!) Unit
+
+-- | A polymorphic way of embedding constants into a term.
+class Const' a where cnst' :: a -> NarcTerm
+instance Const' Bool where cnst' b = return ((!)(Bool b))
+instance Const' Integer where cnst' n = return ((!)(Num n))
+
+-- | Apply some primitive function, such as @(+)@ or @avg@, to a list
+-- of arguments.
+primApp :: String -> [NarcTerm] -> NarcTerm
+primApp f args =  (!) . PrimApp f <$> sequence args
+
+-- | Create a functional abstraction.
+abs :: (String -> NarcTerm) -> NarcTerm
+abs fn = do
+  n <- gensym
+  let x = '_' : show n
+  body <- fn x
+  return $ (!) $ Abs x body
+
+-- | Apply a functional term to an argument.
+app :: NarcTerm -> NarcTerm -> NarcTerm
+app l m = (!) <$> (App <$> l <*> m)
+
+-- | A reference to a named database table; second argument is its
+-- schema type.
+table :: Tabname -> [(Field, Type)] -> NarcTerm
+table tbl ty = return $ (!) $ Table tbl ty
+
+-- | A condition between two terms, as determined by the boolean value
+-- of the first term.
+ifthenelse :: NarcTerm -> NarcTerm -> NarcTerm -> NarcTerm
+ifthenelse c t f = (!) <$> (If <$> c <*> t <*> f)
+
+-- | A singleton collection of one item.
+singleton :: NarcTerm -> NarcTerm
+singleton x = (!) . Singleton <$> x
+
+-- | An empty collection.
+nil :: NarcTerm
+nil = return $ (!) $ Nil
+
+-- | The union of two collections
+union :: NarcTerm -> NarcTerm -> NarcTerm
+union l r = (!) <$> (Union <$> l <*> r)
+
+-- | Construct a record (name-value pairs) out of other terms; usually
+-- used, with base values for the record elements, as the final
+-- result of a query, corresponding to the @select@ clause of a SQL
+-- query, but can also be used with nested results internally in a
+-- query.
+record :: [(String, NarcTerm)] -> NarcTerm
+record fields = (!) <$> (Record <$> sequence [do expr' <- expr ; return (lbl, expr') | (lbl, expr) <- fields])
+
+-- | Project a field out of a record value.
+project :: NarcTerm -> String -> NarcTerm
+project expr field = (!) <$> (Project <$> expr <*> return field)
+
+-- | For each item in the collection resulting from the first
+-- argument, give it to the function which is the second argument
+-- and evaluate--this corresponds to a loop, or two one part of a
+-- cross in traditional SQL queries.
+foreach :: NarcTerm -> (NarcTerm -> NarcTerm) -> NarcTerm
+foreach src k = do
+  src' <- src
+  n <- gensym
+  let x = '_' : show n
+  body' <- k (return (var_ x))
+  return $ (!)(Comp x src' body')
+
+-- | Filter the current iteration as per the condition in the first
+-- argument. Corresponds to a @where@ clause in a SQL query.
+having :: NarcTerm -> NarcTerm -> NarcTerm
+having cond body = ifthenelse cond body nil
+
+-- Example query
+
+example' = let t = (table "foo" [("a", TBool)]) in
+           foreach t $ \x -> 
+           (having (project x "a")
+             (singleton x))
+
+example2' = let t = (table "foo" [("a", TNum)]) in
+            let s = (table "bar" [("a", TNum)]) in
+            foreach t $ \x -> 
+            foreach s $ \y -> 
+            ifthenelse (primApp "<" [project x "a", project y "a"])
+             (singleton x)
+             (singleton y)
+
+example3' =
+    let t = table "employees" [("name", TString), ("salary", TNum)] in
+    foreach t $ \emp ->
+    having (primApp "<" [cnst' (20000::Integer), project emp "salary"]) $
+      singleton (record [("nom", project emp "name")])
+
+-- Unit tests ----------------------------------------------------------
+
+test_example =
+    TestList [
+        SQL.serialize (typeCheckAndCompile (realize example'))
+        ~?= "select _0.a as a from foo as _0 where _0.a"
+        ,
+        SQL.serialize (typeCheckAndCompile (realize example2'))
+        ~?= "(select _0.a as a from foo as _0, bar as _1 where _0.a < _1.a) union (select _1.a as a from foo as _0, bar as _1 where not(_0.a < _1.a))"
+        ,
+        SQL.serialize (typeCheckAndCompile (realize example3'))
+        ~?= "select _0.name as nom from employees as _0 where 20000 < _0.salary"
+    ]
diff --git a/Narc/AST.hs b/Narc/AST.hs
new file mode 100644
--- /dev/null
+++ b/Narc/AST.hs
@@ -0,0 +1,298 @@
+{-# LANGUAGE FlexibleInstances #-}
+
+module Narc.AST (
+  Term'(..),
+  Term,
+  Var,
+  PlainTerm,
+  TypedTerm,
+  fvs,
+  substTerm,
+  strip,
+  retagulate,
+  rename,
+  variables,
+  (!),
+  unit_, Const, cnst_, primApp_, var_, abs_, app_, table_, ifthenelse_,
+  singleton_, nil_, union_, record_, project_, foreach_ 
+) where
+
+import Data.List as List ((\\), nub)
+
+import Prelude hiding (abs)
+
+import Narc.Common
+import Narc.Type
+import Narc.Util (alistmap, u)
+import Narc.Var
+
+-- | Terms in the nested relational calculus (represented concretely
+-- | 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)
+             | 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)
+--           | IsEmpty (Term a)
+    deriving (Eq,Show)
+
+-- | Terms whose every subexpression is annotated with a value of some
+-- | particular type.
+type Term a = (Term' a, a)
+
+-- TBD: use term ::: type or similar instead of (term, type).
+
+type PlainTerm = Term ()
+
+type TypedTerm = Term Type
+
+-- Operations on terms -------------------------------------------------
+
+fvs (Unit, _) = []
+fvs (Bool _, _) = []
+fvs (Num _, _) = []
+fvs (String _, _) = []
+fvs (PrimApp prim args, _) = nub $ concat $ map fvs args
+fvs (Var x, _) = [x]
+fvs (Abs x n, _) = fvs n \\ [x]
+fvs (App l m, _) = fvs l `u` fvs m
+fvs (Table _ _, _) = []
+fvs (If c a b, _) = fvs c `u` fvs a `u` fvs b
+fvs (Nil, _) = []
+fvs (Singleton elem, _) = fvs elem
+fvs (Union m n, _) = fvs m `u` fvs n
+fvs (Record fields, _) = nub $ concat $ map (fvs . snd) fields
+fvs (Project targ _, _) = fvs targ
+fvs (Comp x src body, _) = fvs src `u` (fvs body \\ [x])
+
+variables = map ('y':) $ map show [0..]
+
+rename x y (Var z, q) | x == z    = (Var y, q)
+                      | otherwise = (Var z, q)
+rename x y (l@(Abs z n, q)) | x == z    = l
+                            | otherwise = (Abs z (rename x y n), q)
+rename x y (App l m, q) = (App (rename x y l) (rename x y m), q)
+rename x y (PrimApp prim args, q) = (PrimApp prim (map (rename x y) args), q)
+rename x y (Singleton elem, q) = (Singleton (rename x y elem), q)
+rename x y (Project targ label, q) = (Project (rename x y targ) label, q)
+rename x y (Record fields, q) = (Record (alistmap (rename x y) fields), q)
+rename x y (Comp z src body, q) 
+    | x == z = (Comp z src body, q)
+    | y == z = let y' = head $ variables \\ [y] in
+               let body' = rename y y' body in
+                 (Comp z (rename x y src) (rename x y body'), q)
+    | 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 (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)
+rename x y (Nil, q) = (Nil, q)
+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
+substTerm x v (m@(Unit, _))       = m
+substTerm x v (m@(Bool b, _))     = m
+substTerm x v (m@(Num n, _))      = m
+substTerm x v (m@(String s, _))   = m
+substTerm x v (m@(Table s t, _))  = m
+substTerm x v (m@(Nil, _))        = m
+substTerm x v (Singleton elem, q) = (Singleton (substTerm x v elem), q)
+substTerm x v (Union m n, q) = (Union (substTerm x v m) (substTerm x v n), q)
+substTerm x v (m@(Var y, _)) | y == x    = v
+                             | otherwise = m
+substTerm x v (l @ (Abs y n, q))
+    | x == y            = l
+    | y `notElem` fvs v = (Abs y (substTerm x v n), q) 
+    | otherwise = 
+        let y' = head $ variables \\ fvs v in
+        let n' = rename y y' n in
+        (Abs y' (substTerm x v n'), q)
+substTerm x v (App l m, q) = (App (substTerm x v l) (substTerm x v m), q)
+substTerm x v (PrimApp prim args,q)= (PrimApp prim (map (substTerm x v) args),q)
+substTerm x v (Project targ label, q) = (Project (substTerm x v targ) label, q)
+substTerm x v (Record fields, q) = (Record (alistmap (substTerm x v) fields), q)
+substTerm x v (Comp y src body, q) 
+    | x == y    =
+        (Comp y src' body, q)
+    | y `notElem` fvs v =
+        (Comp y src' (substTerm x v body), q)
+    | otherwise = 
+        let y' = head $ variables \\ fvs v in
+        let body' = rename y y' body in
+        (Comp y' src' (substTerm x v body'), q)
+    where src' = (substTerm x v src)
+substTerm x v (If c a b, q) = 
+    (If (substTerm x v c) (substTerm x v a) (substTerm x v b), q)
+
+-- | lazyDepth: calculate a list (poss. inf.) whose sum is the depth
+-- of the term. (unused)
+lazyDepth :: Term a -> [Int]
+lazyDepth (Abs _ n, _) = 1 : lazyDepth n
+lazyDepth (App l m, _) = 1 : zipWith max (lazyDepth l) (lazyDepth m)
+lazyDepth (Project m _, _) = 1 : lazyDepth m
+lazyDepth (Singleton m, _) = 1 : lazyDepth m
+lazyDepth (PrimApp prim args, _) =
+    1 : foldr1 (zipWith max) (map lazyDepth args)
+lazyDepth (Record fields, _) =
+    1 : foldr1 (zipWith max) (map (lazyDepth . snd) fields)
+lazyDepth (Comp _ src body, _) =
+    1 : zipWith max (lazyDepth src) (lazyDepth body)
+lazyDepth _ = 1 : []
+
+-- Generic term-recursion functions ------------------------------------
+
+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) =
+    (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) =
+    (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))
+
+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 (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))
+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 (Comp x src body, d) = 
+    (Comp x (retagulate f src) (retagulate f body),
+     f (Comp x (retagulate f src) (retagulate f body), d))
+
+strip = entagulate (const ())
+
+-- | numComps: 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
+numComps (App l m, _) = numComps l + numComps m
+numComps (Singleton body, _) = numComps body
+numComps (Record fields, _) = sum $ map (numComps . snd) fields
+numComps (Project m _, _) = numComps m
+numComps (Union a b, _) = numComps a + numComps b
+numComps (Unit, _) = 0
+numComps (Bool _, _) = 0
+numComps (Num _, _) = 0
+numComps (String _, _) = 0
+numComps (Var _, _) = 0
+numComps (Table _ _, _) = 0
+numComps (If c a b, _) = numComps c + numComps a + numComps b
+numComps (Nil, _) = 0
+
+-- | An interface for semanticizing the Narc concrete language as
+-- | desired (as per "Unembedding domain specific languages" by Atkey,
+-- | Lindley and Yallop).
+class NarcSem result where
+    unit :: result
+    bool :: Bool -> result
+    num :: Integer -> result
+    string :: String -> result
+    primApp :: String -> [result] -> result
+    var :: Var -> result
+    abs :: Var -> result -> result
+    app :: result -> result -> result
+    table :: Tabname -> [(Field, Type)] -> result
+    ifthenelse :: result -> result -> result -> result
+    singleton :: result -> result
+    nil :: result
+    union :: result -> result -> result
+    record :: [(String, result)] -> result
+    project :: result -> String -> result
+    foreach :: result -> Var -> result -> result
+--    cnst :: Constable t => t -> result
+class Constable t where cnst :: NarcSem result => t -> result
+instance Constable Bool where cnst b = bool b
+instance Constable Integer where cnst n = num n
+
+-- Explicit-named builders
+
+(!) x = (x, ())
+
+instance NarcSem (Term'(),()) where
+  unit = (!)Unit
+  bool b = (!)(Bool b)
+  num n = (!)(Num n)
+  string n = (!)(String n)
+  primApp f args = (!)(PrimApp f args)
+  var x = (!)(Var x)
+  abs x body = (!)(Abs x body)
+  app l m = (!)(App l m)
+  table tbl ty = (!)(Table tbl ty)
+  ifthenelse c t f = (!)(If c t f)
+  singleton x = (!)(Singleton x)
+  nil = (!)Nil
+  union a b = (!)(Union a b)
+  record fields = (!)(Record fields)
+  project body field = (!)(Project body field)
+  foreach src x body = (!)(Comp x src body)
+-- class Const a where cnst_ :: a -> Term ()
+
+unit_ = (!)Unit
+class Const a where cnst_ :: a -> Term ()
+instance Const Bool where cnst_ b = (!)(Bool b)
+instance Const Integer where cnst_ n = (!)(Num n)
+primApp_ f args = (!)(PrimApp f args)
+var_ x = (!)(Var x)
+abs_ x body = (!)(Abs x body)
+app_ l m = (!)(App l m)
+table_ tbl ty = (!)(Table tbl ty)
+ifthenelse_ c t f = (!)(If c t f)
+singleton_ x = (!)(Singleton x)
+nil_ = (!)Nil
+union_ a b = (!)(Union a b)
+record_ fields = (!)(Record fields)
+project_ body field = (!)(Project body field)
+foreach_ src x body = (!)(Comp x src body)
diff --git a/Narc/AST/Pretty.hs b/Narc/AST/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/Narc/AST/Pretty.hs
@@ -0,0 +1,33 @@
+{-# LANGUAGE TypeSynonymInstances #-}
+
+module Narc.AST.Pretty where
+
+import Narc.AST
+import Narc.Pretty
+import Narc.Util (mapstrcat)
+
+-- Pretty-printing ------------------------------------------------=====
+
+instance Pretty (Term' a) where
+  pretty (Unit) = "()"
+  pretty (Bool b) = show b
+  pretty (Num n) = show n
+  pretty (PrimApp f args) = f ++ "(" ++ mapstrcat "," pretty args ++ ")"
+  pretty (Var x) = x
+  pretty (Abs x n) = "(fun " ++ x ++ " -> " ++ pretty n ++ ")"
+  pretty (App l m) = pretty l ++ " " ++ pretty m
+  pretty (Table tbl t) = "(table " ++ tbl ++ " : " ++ show t ++ ")"
+  pretty (If c a b) =
+      "(if " ++ pretty c ++ " then " ++ pretty a ++ 
+      " else " ++ pretty b ++ " )"
+  pretty (Singleton m) = "[" ++ pretty m ++ "]" 
+  pretty (Nil) = "[]"
+  pretty (Union m n) = "(" ++ pretty n ++ " ++ " ++ pretty n ++ ")"
+  pretty (Record fields) = 
+      "{" ++ mapstrcat "," (\(l,m) -> l ++ "=" ++ pretty m) fields ++ "}"
+  pretty (Project m l) = "(" ++ pretty m ++ "." ++ l ++ ")"
+  pretty (Comp x m n) =
+      "(for (" ++ x ++ " <- " ++ pretty m ++ ") " ++ pretty n ++ ")"
+
+instance Pretty (Term a) where
+  pretty (m, t) = pretty m
diff --git a/Narc/Common.hs b/Narc/Common.hs
new file mode 100644
--- /dev/null
+++ b/Narc/Common.hs
@@ -0,0 +1,6 @@
+module Narc.Common where
+
+type Tabname = String
+
+type Field = String
+
diff --git a/Narc/Compile.hs b/Narc/Compile.hs
new file mode 100644
--- /dev/null
+++ b/Narc/Compile.hs
@@ -0,0 +1,226 @@
+{-# OPTIONS_GHC -Wall #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Narc.Compile (compile) where
+
+import Data.List ((\\))
+
+import Narc.AST
+import Narc.AST.Pretty ()
+import Narc.Contract
+import Narc.Debug (forceAndReport)
+import Narc.Pretty
+import Narc.SQL
+import Narc.Type as Type
+import Narc.TypeInfer
+import Narc.Util (image, maps, alistmap)
+
+-- -- Testing-related imports
+-- import Test.QuickCheck (Property, forAll, sized)
+-- import Narc.TermGen
+-- import Narc.Eval
+-- import Narc.Failure
+
+-- { Compilation } -----------------------------------------------------
+
+etaExpand :: TypedTerm -> [(String, Type)] -> TypedTerm
+etaExpand expr fieldTys =
+    let exprTy = TRecord fieldTys in
+    (Record [(field, ((Project expr field), fTy))
+             | (field, fTy) <- fieldTys], 
+     exprTy)
+
+-- | Normalize DB terms in a nearly call-by-value way.
+normTerm :: [(String, QType)] -- ^ An environment, typing all free vars.
+         -> TypedTerm         -- ^ The term to normalize.
+         -> TypedTerm
+normTerm _env (m@(Unit, _ty))   = m
+normTerm _env (m@(Bool _, _))   = m
+normTerm _env (m@(Num _, _))    = m
+normTerm _env (m@(String _, _)) = m
+normTerm env (PrimApp fun args, t) = (PrimApp fun (map (normTerm env) args), t)
+normTerm env (expr@(Var x, t)) = 
+    -- Eta-expand at record type.
+    if (maps x) env then 
+        case t of
+          TRecord t' -> etaExpand expr t'
+          _ -> (Var x, t) 
+    else
+      error $ "Free variable "++ x ++ " in normTerm"
+normTerm _env (Abs x n, t) =
+    (Abs x n, t)
+normTerm env (App l m, t) = 
+    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)
+      (If b l1 l2, _) ->
+          (normTerm env (If b (App l1 w, t) (App l2 w, t), t))
+      v@(Var _, _) -> (App v w, t)
+      v -> error $ "unexpected normal form in appl posn in normTerm " ++ show v
+normTerm _env (Table s t, t') = (Table s t, t')
+normTerm env (If b m (Nil, _), t@(TList _)) =
+    let b' = normTerm env b in
+    case normTerm env m of
+      (Nil, _)           -> (Nil, t)
+      (Singleton m', _)  -> (If b' (Singleton m', t) (Nil, t), t)
+      (Table s fTys, _)  -> (If b' (Table s fTys, t) (Nil, t), t)
+      (Comp x l m', _)   -> normTerm env (Comp x l (If b' m' (Nil, t), t), t)
+      (m1 `Union` m2, _) -> ((normTerm env (If b' m1 (Nil, t), t)) `Union`
+                             (normTerm env (If b' m2 (Nil, t), t)), t)
+      v@(If _ _ _, _)    -> (If b' v (Nil, t), t)
+      v -> error $ "Unexpected normal form in conditional body in normTerm: " ++
+                    show v
+normTerm env (If b@(_,bTy) m n, t@(TList _)) = -- The case where n /= Nil
+    ((normTerm env (If b m (Nil, t), t)) `Union` 
+     (normTerm env (If (PrimApp "not" [b], bTy) n (Nil, t), t)), t)
+normTerm env (If b m n, t@(TRecord fTys)) =
+    let b' = normTerm env b in
+    let (Record mFields, _) = normTerm env m
+        (Record nFields, _) = normTerm env n in
+    (Record [(l, (If b' (image l mFields) (image l nFields), (image l fTys)))
+             | (l, _) <- mFields],
+     t)
+normTerm env (If b m n, t) = 
+    (If (normTerm env b) (normTerm env m) (normTerm env n), t)
+normTerm env (Singleton m, t) = (Singleton (normTerm env m), t)
+normTerm _env (Nil, t) = (Nil, t)
+normTerm env (m `Union` n, t) = ((normTerm env m) `Union` (normTerm env n), t)
+normTerm env (Record fields, t) =
+    (Record [(a, normTerm env m) | (a, m) <- fields], t)
+normTerm env (Project argTerm label, t) = 
+    case normTerm env argTerm of
+      (Record fields, _) -> case (lookup label fields) of 
+                              Just x -> x 
+                              Nothing -> error $ "no field " ++ label
+      -- Ah, the following not necessary because If pushes into records.
+      (If condn v1 v2,_) ->
+          normTerm env (If condn
+                        (Project v1 label, t)
+                        (Project v2 label, t), t)
+      v@(Var _x, _) -> (Project v label, t)
+      v -> error $ "Unexpected normal form in body of Project in normTerm: " ++ 
+                    show v
+normTerm env (Comp x src body, t) =
+    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)
+      (Comp y src2 body2, _) ->
+          -- Freshen @y@ over @src@ with respect to @body@ (that of
+          -- the outer comprehension), because we're widening the
+          -- scope of @y@ to include @body@.
+          let (y', body') = if y `elem` fvs body then
+                              let newY = minFreeFor body in
+                              (newY, rename y newY body)
+                         else (y, body)
+          in
+            (normTerm env (Comp y' src2 (Comp x body2 body', t), t))
+      (srcL `Union` srcR, _) ->
+          ((normTerm env (Comp x srcL body, t)) `Union` 
+           (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 
+                 normTerm env' body
+      (If cond' src' (Nil, _), _) ->
+          assert (x `notElem` fvs cond') $
+          let v = normTerm env (Comp x src' body, t) in
+          insertFurther (\(v',t') -> (If cond' (v',t') (Nil, t'), t')) v
+      v -> error $
+             "unexpected normal form in source part of comprehension: " ++
+             show v
+
+-- Insertion functions for rebuilding a term, dropping a
+-- reconstructor k down through unions and compr'ns (there must be
+-- a better way!).
+insert :: (TypedTerm -> TypedTerm) -> TypedTerm -> TypedTerm
+insert k ((v,t) :: TypedTerm) =
+    case v of
+      Nil -> (Nil, t)
+      n1 `Union` n2 -> ((insert k n1) `Union` (insert k n2), t)
+      _ -> k (v,t)
+
+insertFurther :: (TypedTerm -> TypedTerm) -> TypedTerm -> TypedTerm
+insertFurther k ((v,t) :: TypedTerm) =
+    case v of
+      Nil -> (Nil, t)
+      n1 `Union` n2 -> 
+          ((insertFurther k n1) `Union` (insertFurther k n2), t)
+      Comp x m n -> (Comp x m (insertFurther k n), t)
+      _ -> k (v,t)
+
+-- See (Bird 2010) for a better algorithm here.
+minFreeFor :: Term a -> Var
+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 (Nil, _)         = Narc.SQL.emptyQuery
+translateTerm (f@(Comp _ (Table _ _, _) _, _))                  = translateF f
+translateTerm (f@(If _ _ (Nil, _), _))                          = translateF f
+translateTerm (f@(Singleton (Record _, _), _))                  = translateF f
+translateTerm (f@(Table _ _, _))                                = translateF f
+translateTerm x = 
+    error $ "translateTerm got unexpected term: " ++ (pretty.fst) x
+
+-- translateF, translateZ and translateB are named after the syntactic
+-- 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 (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}
+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 (If b z (Nil, _), _) =
+    let q@(Select _ _ _) = translateZ z in
+    Select {rslt=rslt q, tabs = tabs q, cond = translateB b : cond q}
+translateZ (Singleton (Record fields, _), _) = 
+    Select {rslt = QRecord(alistmap translateB fields), tabs = [], cond = []}
+translateZ (Table tabname fTys, _) =
+    Select {rslt = QRecord[(l,QField tabname l)| (l,_ty) <- fTys],
+            tabs = [(tabname, tabname, TRecord fTys)], cond = []}
+translateZ z = error$ "translateZ got unexpected term: " ++ (pretty.fst) z
+
+translateB :: Term b -> Query
+translateB (If b b' b'', _)            = QIf (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 b = error$ "translateB got unexpected term: " ++ (pretty.fst) b
+
+compile :: TyEnv -> TypedTerm -> Query
+compile env = translateTerm . normTerm env
+
+-- -- Tests
+
+-- -- FIXME: where does this belong? It tests a function internal to this
+-- -- module (normTerm) but uses testing apparatus that is defined at a
+-- -- "higher" layer (Narc.Test) and uses an otherwise unrelated module
+-- -- (Narc.Eval).
+-- prop_norm_sound :: TyEnv -> Env -> Property
+-- prop_norm_sound tyEnv env =
+--   forAll (sized (typeGen [])) $ \t ->
+--   forAll (sized (typedTermGen tyEnv t)) $ \m ->
+--       isErrorMSuccess $ tryErrorGensym $ 
+--       do m' <- infer m
+--          return (eval env (normTerm tyEnv m') == eval env m')
diff --git a/Narc/Contract.hs b/Narc/Contract.hs
new file mode 100644
--- /dev/null
+++ b/Narc/Contract.hs
@@ -0,0 +1,7 @@
+module Narc.Contract where
+
+-- Contractual assertions ----------------------------------------------
+
+contract p x = if p x then x else error "Contract broken"
+
+assert x e = if x then e else error "assertion failed"
diff --git a/Narc/Debug.hs b/Narc/Debug.hs
new file mode 100644
--- /dev/null
+++ b/Narc/Debug.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Narc.Debug where
+
+import Prelude hiding (catch)
+import Control.Exception (catch, evaluate, throwIO, SomeException)
+import Debug.Trace (trace)
+import Foreign (unsafePerformIO)
+
+-- | Enable/disable debugging messages
+debugFlag :: Bool
+debugFlag = False
+
+-- | Trace the given string if debugging is on, or do nothing if not.
+debug :: String -> a -> a
+debug str = if debugFlag then trace str else id
+
+breakFlag x = x     -- a hook for a breakpoint in GHCi debugger
+
+-- | Force an arbitrary expression, tracing the @String@ arg if
+-- forcing produces an exception.
+forceAndReport :: a -> String -> a
+forceAndReport expr msg = 
+          unsafePerformIO $
+          catch (evaluate $
+                 expr `seq` expr
+          ) (\(exc::SomeException) ->
+            breakFlag $ 
+            debug msg $ 
+             Control.Exception.throwIO exc
+          )
diff --git a/Narc/Eval.hs b/Narc/Eval.hs
new file mode 100644
--- /dev/null
+++ b/Narc/Eval.hs
@@ -0,0 +1,119 @@
+module Narc.Eval where
+
+import Narc.AST
+import Narc.Debug (debug)
+import Narc.Util (alistmap)
+
+--
+-- Evaluation ----------------------------------------------------------
+--
+
+-- { Values and value environments } -----------------------------------
+
+bind x v env = (x,v):env
+
+-- type RuntimeTerm = Term (Maybe Query)
+
+type Env = [(Var, Value)]
+
+data Value = VUnit | VBool Bool | VNum Integer
+            | VList [Value]
+            | VRecord [(String, Value)]
+            | VAbs Var TypedTerm Env
+        deriving (Eq, Show)
+
+fromValue :: Value -> TypedTerm
+fromValue VUnit = (Unit, undefined)
+fromValue (VBool b) = (Bool b, undefined)
+fromValue (VNum n) = (Num n, undefined)
+fromValue (VList xs) = foldr1 union (map singleton $ map fromValue xs)
+    where union x y = (x `Union` y, undefined)
+          singleton x = (Singleton x, undefined)
+fromValue (VRecord fields) = (Record (alistmap fromValue fields), undefined)
+fromValue (VAbs x n env) = foldr (\(y,v) -> substTerm y (fromValue v))
+                           (Abs x n, undefined) env
+
+concatVLists xs = VList $ concat [x | (VList x)<-xs]
+
+initialEnv :: Env
+initialEnv =
+    []
+--     [("+",
+--       ((VAbs "x" (Abs "y"
+--                   (PrimApp "+" [(Var "x", (TNum, openEpe), (Var "y", TNum)],
+--                    Just (QOp (QVar "x") Plus (QVar "y"))), TNum) []),
+--        Just (QAbs "x" (QAbs "y" (QOp (QVar "x") Plus (QVar "y"))))))]
+
+-- | appPrim: apply a primitive function to a list of value arguments.
+appPrim :: String -> [Value] -> Value
+appPrim "+" [VNum a, VNum b] = VNum (a+b)
+appPrim p _ = error("Unknown primitive" ++ p)
+
+-- | eval: Evaluate a typed term in a closing environment. Captures the
+-- effects performed by the term. (NB: type info is not actually used;
+-- should eliminate this.)
+eval :: Env -> TypedTerm -> Value
+eval env (Unit, _) = (VUnit)
+eval env (Bool b, q) = (VBool b)
+eval env (Num n, q) = (VNum n)
+eval env (PrimApp prim args, q) = 
+    let (vArgs) = map (eval env) args in
+    (appPrim prim vArgs)
+eval env (Var x, q) =
+    case lookup x env of
+      Nothing -> error
+                 ("Variable " ++ x ++ " not found in env " ++ show env ++ 
+                  " while evaluating term.")
+      Just v -> v
+eval env (Abs x n, q) = (VAbs x n env')
+    where env' = filter (\(a,b) -> a `elem` fvs n) env
+eval env (App l m, q) = 
+    let (v) = eval env l in
+    let (w) = eval env m in
+    case v of
+      (VAbs x n env') -> 
+          let env'' = bind x w env' in
+          let (r) = eval env'' n in
+          (r)
+      _ -> error "non-function applied"
+eval env (Table name fields, q) = 
+    (VList [])
+eval env (If c a b, _) =
+    let (VBool t) = eval env c in
+    let (result) = if t then eval env a else eval env b in
+    (result)
+eval env (Nil, _) =
+    (VList [])
+eval env (Singleton body, q) =
+    let (v) = eval env body in
+    (VList [v])
+eval env (Union m n, _) =
+    let (VList v) = eval env m in
+    let (VList w) = eval env n in
+    (VList $ v ++ w)
+eval env (Record fields, q) =
+    let (vFields) = [let (value) = eval env term in
+                     ((name, value))
+                     | (name, term) <- fields] in
+    (VRecord vFields)
+eval env (Project m f, q) =
+    let (v) = eval env m in
+    case v of
+      VRecord fields -> 
+          case lookup f fields of {
+            Nothing -> error $ "No field " ++ f ++ " in " ++ 
+                               show v ++ "(" ++ show m ++ ")" ;
+            Just vField -> vField
+          }
+      _ -> error("Non-record value " ++ show v ++ " target of projection " ++ 
+                 show(Project m f))
+eval env (Comp x src body, q) =
+    let (vSrc) = eval env src in
+    case vSrc of
+      (VList elems) -> 
+          let (results) = [eval (bind x v env) body
+                           | v <- elems] in
+          (concatVLists results)
+      _ -> error("Comprehension source was not a list.")
+
+run = eval initialEnv
diff --git a/Narc/Failure.hs b/Narc/Failure.hs
new file mode 100644
--- /dev/null
+++ b/Narc/Failure.hs
@@ -0,0 +1,46 @@
+module Narc.Failure where
+
+import Narc.Debug
+import Control.Monad.Error hiding (when, join)
+import Gensym
+
+-- Failure and ErrorGensym monads --------------------------------------
+-- (TBD: this is more general than Narc; factor it out.)
+
+type Failure a = Either String a
+
+fayl = Left -- TBD: would be better to make Failure a newtype & use
+            -- fail from Monad.
+
+-- instance Monad Failure where
+--     return = Failure . Right
+--     fail = Failure . Left
+--     x >>= k = case x of Failure(Left err) -> Failure(Left err)
+--                         Failure(Right x') -> k x'
+
+runError :: Either String t -> t
+runError (Left e) = breakFlag $ error e
+runError (Right x) = x
+
+isError (Left x) = True
+isError (Right _) = False
+
+isSuccess (Left _) = False
+isSuccess (Right _) = True
+
+type ErrorGensym a = ErrorT String Gensym a
+
+-- | Run an ErrorGensym action, raising errors with `error'.
+runErrorGensym = runError . runGensym . runErrorT
+
+-- | Try running an ErrorGensym action, packaging result in an Either
+-- | with Left as failure, Right as success.
+tryErrorGensym = runGensym . runErrorT
+
+under x = either throwError return x
+
+isErrorMSuccess = either (const False) (const True) 
+
+instance Error () where
+    noMsg = ()
+    strMsg _ = ()
diff --git a/Narc/Failure/QuickCheck.hs b/Narc/Failure/QuickCheck.hs
new file mode 100644
--- /dev/null
+++ b/Narc/Failure/QuickCheck.hs
@@ -0,0 +1,17 @@
+module Narc.Failure.QuickCheck where
+
+import Test.QuickCheck
+
+import QCUtils
+import Narc.Failure
+
+-- QuickCheck property utilities ---------------------------------------
+
+failureToProperty :: Test.QuickCheck.Testable a => Failure a -> Property
+failureToProperty (Left _) = failProp
+failureToProperty (Right x) = property x
+
+failureToPropertyIgnoreFailure :: Test.QuickCheck.Testable a => 
+                                  Failure a -> Property
+failureToPropertyIgnoreFailure (Left _) = ignore
+failureToPropertyIgnoreFailure (Right x) = property x
diff --git a/Narc/HDBC.hs b/Narc/HDBC.hs
new file mode 100644
--- /dev/null
+++ b/Narc/HDBC.hs
@@ -0,0 +1,13 @@
+module Narc.HDBC where
+
+import Database.HDBC
+
+import Narc.AST
+import Narc.SQL
+import Narc.Compile
+import Narc.TypeInfer
+
+run :: IConnection conn => Term a -> conn -> IO [[SqlValue]]
+run t conn =
+    let sql = serialize (compile [] (runTyCheck [] t)) in
+    quickQuery conn sql []
diff --git a/Narc/Pretty.hs b/Narc/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/Narc/Pretty.hs
@@ -0,0 +1,8 @@
+module Narc.Pretty where
+
+import Narc.Common
+
+-- Pretty-printing ------------------------------------------------=====
+
+class Pretty t where
+  pretty :: t -> String
diff --git a/Narc/Rewrite.hs b/Narc/Rewrite.hs
new file mode 100644
--- /dev/null
+++ b/Narc/Rewrite.hs
@@ -0,0 +1,67 @@
+module Narc.Rewrite where
+
+import Data.Maybe (fromMaybe)
+
+import Narc.AST
+import Narc.Type
+import Narc.Util (alistmap)
+
+-- Rewrite -------------------------------------------------------------
+--
+-- Small-step version of compilation: local rewrite rules applied
+-- willy-nilly.
+
+perhaps :: (a -> Maybe a) -> a -> a
+perhaps f x = fromMaybe x (f x)
+
+bu :: (Term a -> Maybe (Term a)) -> Term a -> Term a
+bu f (Unit, d) = perhaps f (Unit, d)
+bu f (Bool b, d) = perhaps f (Bool b, d)
+bu f (Num n, d) = perhaps f (Num n, d)
+bu f (Var x, d) = perhaps f (Var x, d)
+bu f (Abs x n, d) = perhaps f (Abs x (bu f n), d)
+bu f (App l m, d) = perhaps f (App (bu f l) (bu f m), d)
+bu f (If c a b, d) =
+    perhaps f (If (bu f c)
+          (bu f a)
+          (bu f b), d)
+bu f (Table tab fields, d) = perhaps f (Table tab fields, d)
+bu f (Singleton m, d) = perhaps f (Singleton (bu f m), d)
+bu f (Record fields, d) = perhaps f (Record (alistmap (bu f) fields), d)
+bu f (Project m a, d) = perhaps f (Project (bu f m) a, d)
+bu f (Comp x src body, d) = perhaps f (Comp x (bu f src) (bu f body), d)
+bu f (PrimApp fun args, d) = perhaps f (PrimApp fun args, d)
+bu f (Nil, d) = perhaps f (Nil, d)
+bu f (Union a b, d) = perhaps f (Union a b, d)
+
+rw (Comp x (Singleton m, _) n, t) = Just (substTerm x m n)
+rw (App (Abs x n, st) m, t) = Just (substTerm x m n)
+rw (Project (Record fields, rect) fld, t) = lookup fld fields
+rw (Singleton (Var x, xT), t) = Nothing -- for now
+rw (Comp x (Nil, _) n, t) = Just (Nil, t)
+rw (Comp x m (Nil, _), t) = Just (Nil, t)
+rw (Comp x (Comp y l m, s) n, t) = 
+    if y `notElem` fvs n then
+        Just (Comp y l (Comp x m n, t), t)
+    else Nothing
+rw (Comp x (m1 `Union` m2, s) n, t) =
+    Just ((Comp x m1 n, t) `Union` (Comp x m2 n, t), t)
+rw (Comp x m (n1 `Union` n2, _), t) =
+    Just ((Comp x m n1, t) `Union` (Comp x m n2, t), t)
+rw (Comp x (If b m (Nil, _), _) n, t) =
+    Just (Comp x m (If b n (Nil, t), t), t)
+rw (If (b, bTy) m n, t@(TList _, _)) | fst n /= Nil =
+                      Just((If (b,bTy) m (Nil, t), t) `Union`
+                           (If (PrimApp "not" [(b, bTy)], bTy) n (Nil, t), t), t)
+rw (If b (Nil, _) (Nil, _), t) = Just (Nil, t)
+rw (If b (Comp x m n, _) (Nil, _), t) = Just (Comp x m (If b n (Nil, t), t), t) 
+rw (If b (m1 `Union` m2, _) (Nil, _), t) =
+    Just ((If b m1 (Nil, t), t) `Union` (If b m2 (Nil, t), t), t)
+-- push App inside If
+-- push Project inside If
+-- push If inside Record
+-- rw (IsEmpty m, t) 
+--     | lorob t   = Nothing
+--     | otherwise = 
+--         IsEmpty (Comp "x" m (Singleton (Unit, TUnit), TList Tunit), TList TUnit)
+rw _ = Nothing
diff --git a/Narc/SQL.hs b/Narc/SQL.hs
new file mode 100644
--- /dev/null
+++ b/Narc/SQL.hs
@@ -0,0 +1,155 @@
+module Narc.SQL where
+
+import Data.List (nub, intercalate)
+
+import Narc.Common
+import Narc.Type
+import Narc.Util (u, mapstrcat)
+
+--
+-- SQL Queries ---------------------------------------------------------
+--
+
+data Op = Eq | Less
+        | Plus | Minus | Times | Divide
+        deriving(Eq, Show)
+
+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
+
+      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
+
+      limit = 100
+
+-- Basic functions on query expressions --------------------------------
+
+freevarsQuery (q@(Select _ _ _)) = 
+    (freevarsQuery (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
+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]
+
+serialize :: Query -> String
+serialize q@(Select _ _ _) =
+    "select " ++ serializeRow (rslt q) ++
+    " from " ++ mapstrcat ", " (\(a, b, _) -> a ++ " as " ++ b) (tabs q) ++
+    " where " ++ if null (cond q) then
+                     "true"
+                 else mapstrcat " and " serializeAtom (cond q)
+serialize (QUnion l r) =
+    "(" ++ serialize l ++ ") union (" ++ serialize r ++ ")"
+
+serializeRow (QRecord 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 l ++ " " ++ serializeOp op ++ " " ++ serializeAtom r
+serializeAtom (QField rec fld) = rec ++ "." ++ fld
+serializeAtom (QIf cond l r) = 
+    "case when " ++ serializeAtom cond ++
+    " then " ++ serializeAtom l ++
+    " else " ++ serializeAtom r ++
+    " end)"
+serializeAtom (QExists q) =
+    "exists (" ++ serialize q ++ ")"
+
+serializeOp Eq = "="
+serializeOp Less = "<"
+serializeOp Plus = "<"
+serializeOp Minus = "<"
+serializeOp Times = "<"
+serializeOp Divide = "<"
diff --git a/Narc/SQL/Pretty.hs b/Narc/SQL/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/Narc/SQL/Pretty.hs
@@ -0,0 +1,39 @@
+module Narc.SQL.Pretty where
+
+import Narc.Pretty
+import Narc.SQL
+import Narc.Util (mapstrcat)
+
+instance Pretty Query where
+  pretty (Select{rslt=QRecord flds, tabs=tabs, cond=cond}) = 
+         "select " ++ mapstrcat ", " (\(alias, expr) -> 
+                                          pretty expr ++ " as " ++ alias)
+                      flds ++ 
+         (if null tabs then "" else
+         " from " ++ mapstrcat ", " (\(name, al, ty) -> name ++ " as " ++ al) 
+                         tabs) ++ 
+         " 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 (QField a b) = a ++ "." ++ b
+
+  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
+                       ++ " else " ++ pretty f
+
+-- Pretty-printing for Op, common to both AST and SQL languages.
+
+instance Pretty Op where
+  pretty Plus = " + "
+  pretty Eq = " = "
+  pretty Less = " < "
diff --git a/Narc/TermGen.hs b/Narc/TermGen.hs
new file mode 100644
--- /dev/null
+++ b/Narc/TermGen.hs
@@ -0,0 +1,196 @@
+module Narc.TermGen where
+
+import Control.Monad hiding (when)
+
+import Test.QuickCheck hiding (promote, Failure)
+
+import Gensym
+import QCUtils
+
+import Narc.AST
+import Narc.SQL
+import Narc.Type as Type
+import Narc.Util
+
+--
+-- QuickCheck term generators ------------------------------------------
+--
+
+smallIntGen :: Gen Int
+smallIntGen = elements [0..5]
+
+typeGen :: [TyVar] -> Int -> Gen Type
+typeGen tyEnv size =
+    oneof $ [return TBool,
+             return TNum
+            ] ++
+    [do x <- elements tyEnv; return $ TVar x | length tyEnv > 0] ++
+    whens (size > 0)
+        [
+         do s <- typeGen tyEnv (size-1)
+            t <- typeGen tyEnv (size-1)
+            return $ TArr s t,
+         do t <- typeGen tyEnv (size-1)
+            return $ TList t,
+         do n <- smallIntGen :: Gen Int
+            fields <- sequence [do t <- typeGen tyEnv (size-1)
+                                   return ('f':show i, t) | i <- [0..n]]
+            return $ TRecord fields
+        ]
+
+-- | Generate a random term, unlikely to be well-typed.
+termGen :: [Var] -> Int -> Gen (Term ())
+termGen fvs size = frequency $
+    [(1,                    return (Unit, ())),
+     (1, do b <- arbitrary; return (Bool b, ())),
+     (1, do n <- arbitrary; return (Num n, ()))
+    ]
+    ++
+    (whens (not (null fvs)) [(3, do x <- elements fvs;
+                                    return (Var x, ()))])
+    ++
+    whens (size > 0) [
+     (3, do x <- varGen
+            n <- termGen (x:fvs) (size-1)
+            return (Abs x n, ())),
+     (6, do m <- termGen fvs (size-1)
+            n <- termGen fvs (size-1)
+            return $ (App m n, ())),
+     (6, do m <- termGen fvs (size-1)
+            f <- identGen
+            return $ (Project m f, ())),
+     (6, do m <- termGen fvs (size-1)
+            return $ (Singleton m, ())),
+     (18, do n <- smallIntGen
+             tableName <- identGen
+             fields <- sequence $ replicate n $
+                       do name <- identGen
+                          ty <- elements [TBool, TNum]
+                          return (name, ty)
+             return $ (Table tableName fields, ())),
+     (9, do n <- smallIntGen
+            fields <- sequence $ replicate n $
+                      do name <- identGen
+                         term <- termGen fvs (size-1)
+                         return (name, term)
+            return $ (Record fields, ())),
+     (72, do x <- varGen  -- Overwhelmingly favor comprehensions when
+                          -- we have enough size remaining, since
+                          -- we'll be favoring other stuff when we run
+                          -- out of size.
+             l <- termGen fvs (size-1)
+             m <- termGen (x:fvs) (size-1)
+             return $ (Comp x l m, ()))
+    ]
+
+closedTermGen :: Int -> Gen (Term' (), ())
+closedTermGen size = 
+    termGen [] size
+
+oneofMaybe :: [Gen(Maybe a)] -> Gen (Maybe a)
+oneofMaybe [] = return Nothing
+oneofMaybe (x:xs) = do x' <- x
+                       xs' <- oneofMaybe xs
+                       case (x', xs') of
+                         (Nothing, Nothing) -> return Nothing
+                         _ -> oneof (map (return . Just) $ 
+                                         asList x' ++ asList xs')
+
+-- Why isn't this bloody thing generating deconstructors??
+typedTermGen :: TyEnv -> Type -> Int -> Gen (Term ())
+typedTermGen env ty sz = 
+--    debug ("generating term (type " ++ show ty ++ ") at size " ++ show sz) $
+    frequency (
+    -- variables
+    -- (NOTE: presently only gens vars that have ground type, sans quant'rs)
+    [(2, return $ (Var x, ())) | (x, (xQs, xTy)) <- env,
+                                 xQs == [] && xTy == ty] ++
+    -- constructors
+    (case ty of
+      TNum  -> [(1, do n <- arbitrary; return (Num n, ()))]
+      TBool -> [(1, do b <- arbitrary; return (Bool b, ()))]
+      TArr s t -> 
+          [(2, do x <- varGen 
+                  n <- typedTermGen ((x, ([], s)):(unassoc x env)) t decSz
+                  return $ (Abs x n, ()))]
+      TRecord fTys -> 
+          [(2, do fields <- forM fTys $ \(lbl, ty) ->
+                              do m <- typedTermGen env ty decSz
+                                 return (lbl, m)
+                  return $ (Record fields, ()))]
+      TList ty ->
+          [(2, do m <- typedTermGen env ty decSz 
+                  return $ (Singleton m, ()))]
+          ++ case ty of 
+                TRecord fTys ->
+                  if not (and [isBaseTy ty | (_, ty) <- fTys]) then [] else
+                  [(2, do tab <- identGen
+                          return $ (Table ('T':tab) fTys, ()))]
+                _ -> []
+      _ -> error("Strange type while generating term: " ++ 
+                 show ty ++ " (size " ++ show sz ++ ")")
+    ) ++
+    -- deconstructors
+    if (sz <= 0) then [] else (
+     [
+      (10, do s <- typeGen [] (intSqrt sz)
+              m <- typedTermGen env (TArr s ty) decSz
+              n <- typedTermGen env s decSz
+              return $ (App m n, ())),
+      (10, do c <- typedTermGen env TBool decSz
+              a <- typedTermGen env ty decSz
+              b <- typedTermGen env ty decSz
+              return $ (If c a b, ()))
+     ] ++
+     -- Comprehension: a constructor and a destructor
+     case ty of
+      (TList _) ->
+          [(20, do x <- varGen
+                   s <- typeGen [] (intSqrt sz)
+                   src <- typedTermGen env (TList s) decSz
+                   let env' = Type.bind x ([], s) env
+                   body <- typedTermGen env' ty decSz
+                   return (Comp x src body, ()))
+          ]
+      _ -> []
+    )
+  )
+  where decSz = max (sz-1) 0
+
+closedTypedTermGen :: Type -> Int -> Gen (Term ())
+closedTypedTermGen ty size = 
+--    let tyEnv = runErrorGensym makeInitialTyEnv in
+    let tyEnv = [] in
+    typedTermGen tyEnv ty size
+
+dbTableTypeGen :: Gen Type
+dbTableTypeGen = 
+    do n <- nonNegInt :: Gen Int
+       ty <- elements [TBool, TNum]
+       return $ TList (TRecord [('t': show i, ty) | i <- [0..n-1]])
+
+
+-- Generators
+
+instance Arbitrary Op where
+    arbitrary = oneof [return Eq, return Less]
+
+listGen :: Int -> Gen a -> Gen [a]
+listGen 0 gen = oneof [ return [], do x <- gen
+                                      xs <- listGen 0 gen
+                                      return (x : xs)]
+listGen n gen = do x <- gen
+                   xs <- listGen (n-1) gen
+                   return (x : xs)
+
+identCharGen :: Gen Char
+identCharGen = oneof $ map return (['a'..'z'] ++ ['A'..'Z'] ++ ['_'])
+
+identGen :: Gen String
+identGen = listGen 1 identCharGen
+
+varGen :: Gen String
+varGen = (return ('x':)) `ap` identGen
+
+pairGen :: Gen a -> Gen b -> Gen (a, b)
+pairGen aGen bGen = do a <- aGen; b <- bGen; return (a, b)
diff --git a/Narc/Test.hs b/Narc/Test.hs
new file mode 100644
--- /dev/null
+++ b/Narc/Test.hs
@@ -0,0 +1,82 @@
+{-# OPTIONS_GHC -Wall -fno-warn-name-shadowing #-}
+
+module 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 Gensym
+import QCUtils
+
+import Narc.AST
+import Narc.Compile
+import Narc.Failure
+import Narc.SQL
+import Narc.Type as Type
+import Narc.TypeInfer
+import 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
+                  groundQuery $ compile initialTyEnv $ tyTerm
+                 ]
+
+unitTests :: ErrorGensym Test
+unitTests = do normalizerTests <- makeNormalizerTests 
+               return $ TestList [tyCheckTests, normalizerTests, typingTest]
+
+runUnitTests :: IO Counts
+runUnitTests = runErrorGensym $ liftM runTestTT unitTests
+
+--
+-- Big QuickCheck properties
+--
+
+-- | Assertion that well-typed terms evaluate without throwing.
+prop_eval_safe :: Property
+prop_eval_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 ==>
+            let q = (compile [] $! m') in
+            collect (sizeQuery q) $  -- NB: Counts sizes only up to ~100.
+                    excAsFalse (q == q) -- Self-comparison forces the
+                                        -- value (?) thus surfacing
+                                        -- any @error@s that might be
+                                        -- raised.
+
+prop_typedTermGen_tyCheck :: Property
+prop_typedTermGen_tyCheck =
+  forAll (sized $ typeGen []) $ \ty ->
+  forAll (sized $ typedTermGen (runErrorGensym makeInitialTyEnv) ty) $ \m ->
+  case runGensym $ runErrorT $ infer m of
+    Left _ -> False
+    Right (_m', ty') -> isErrorMSuccess $ unify ty ty'
+
+-- Main ----------------------------------------------------------------
+
+main :: IO ()
+main = do
+  quickCheckWith tinyArgs prop_eval_safe
+  _ <- runUnitTests
+  return ()
diff --git a/Narc/Type.hs b/Narc/Type.hs
new file mode 100644
--- /dev/null
+++ b/Narc/Type.hs
@@ -0,0 +1,245 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Narc.Type where
+
+import Test.QuickCheck
+
+import Gensym
+import QCUtils
+
+import Data.List ((\\))
+import Control.Monad.State (State(..), get, put, evalState) -- TBD: use Gensym monad instead
+import Control.Applicative ((<$>))
+import Narc.Failure (Failure, fayl)
+import Narc.Failure.QuickCheck
+import Narc.Util (dom, rng, image, alistmap, sortAlist, onCorresponding,
+                     disjointAlist, validEnv, eqUpTo)
+import Narc.Var
+
+type TyVar = Int
+
+data Type = TBool | TNum | TString | TUnit | TList Type
+          | TArr Type Type
+          | TRecord [(String, Type)]
+          | TVar TyVar
+    deriving (Eq, Show)
+
+type QType = ([TyVar], Type)
+
+type TySubst = [(Int, Type)]
+
+type TyEnv = [(Var, QType)]
+
+-- Operations on types, rows and substitutions ------------------------
+
+isBaseTy TBool = True
+isBaseTy TNum  = True
+isBaseTy TString  = True
+isBaseTy _     = False
+
+isTyVar (TVar _) = True
+isTyVar _        = False
+
+isDBRecordTy (TRecord fields) = all (isBaseTy . snd) fields
+isDBRecordTy _                = False
+
+isRecordTy (TRecord fields) = True
+isRecordTy _                = False
+
+isDBTableTy (TList ty) = isDBRecordTy ty
+isDBTableTy _          = False
+
+emptyTySubst :: (TySubst)
+emptyTySubst = ([])
+
+-- | ftvs: free type variables
+ftvs TBool = []
+ftvs TNum = []
+ftvs TString = []
+ftvs TUnit = []
+ftvs (TList t) = ftvs t
+ftvs (TArr s t) = ftvs s ++ ftvs t
+ftvs (TRecord fields) = concat [ftvs t | (lbl, t) <- fields]
+ftvs (TVar a) = [a]
+
+numFtvs = length . ftvs
+
+-- | ftvsSubst: the free type variables of a type substitution--that is,
+-- the type variables free in the types in the range of the substitution.
+ftvsSubst a = concatMap ftvs $ rng a
+
+-- | occurs x ty: does variable x appear in type ty? (Note there are no
+-- type-variable binders).
+occurs x (TVar y) | x == y    = True
+                  | otherwise = False
+occurs x (TArr s t) = x `occurs` s || x `occurs` t
+occurs x (TList t) = x `occurs` t
+occurs x (TRecord t) = any (occurs x) (map snd t)
+occurs x (TUnit) = False
+occurs x (TBool) = False
+occurs x (TNum) = False
+occurs x (TString) = False
+
+applyTySubst :: TySubst -> Type -> Type
+applyTySubst subst (TUnit) = TUnit
+applyTySubst subst (TBool) = TBool
+applyTySubst subst (TNum) = TNum
+applyTySubst subst (TString) = TString
+applyTySubst subst (TVar a) = case lookup a subst of
+                              Nothing -> TVar a
+                              Just ty -> ty
+applyTySubst subst (TArr a b) =
+    TArr (applyTySubst subst a) (applyTySubst subst b)
+applyTySubst subst (TList a) = TList (applyTySubst subst a)
+applyTySubst subst (TRecord a) = TRecord (alistmap (applyTySubst subst) a)
+
+
+-- Type operations -----------------------------------------------------
+
+instantiate (qs, ty) =
+    do subst <- sequence [do y <- gensym ; return (q, TVar y) | q <- qs]
+       return $ applyTySubst subst ty
+
+{- | normalizeType:
+   Renumber all the type variables in a normal way to allow
+   comparing types.
+-}
+normalizeType :: Type -> State (Int, [(Int, Int)]) Type
+normalizeType TBool = return TBool
+normalizeType TNum = return TNum
+normalizeType TString = return TString
+normalizeType TUnit = return TUnit
+normalizeType (TList ty) = TList <$> normalizeType ty
+normalizeType (TRecord recTy) = undefined
+normalizeType (TVar a) = do (ctr, env) <- Control.Monad.State.get
+                            case lookup a env of
+                              Nothing -> do put (ctr+1, (a, ctr):env)
+                                            return $ TVar ctr
+                              Just b -> return $ TVar b
+normalizeType (TArr s t) =
+    do s' <- normalizeType s
+       t' <- normalizeType t
+       return $ TArr s' t'
+
+runNormalizeType ty = evalState (normalizeType ty) (0, [])
+
+-- instanceOf: is there a substitution that turns ty2 into ty1? Useful in tests
+instanceOf :: Type -> Type -> Failure ()
+instanceOf ty1 (TVar x) = return ()
+instanceOf TBool TBool = return ()
+instanceOf TNum TNum = return ()
+instanceOf TString TString = return ()
+instanceOf (TArr s t) (TArr u v) = 
+    instanceOf t v >>
+    instanceOf s u
+instanceOf (TList a) (TList b) = instanceOf a b
+instanceOf (TRecord a) (TRecord b) = 
+    let a' = sortAlist a 
+        b' = sortAlist b
+    in
+      do result <- sequence [if ax == bx then instanceOf ay by else fayl "Record mismatch"
+                             | ((ax, ay), (bx, by)) <- zip a' b']
+         return ()
+instanceOf a b = fayl ""
+
+unify :: Type -> Type -> Failure (TySubst)
+unify s t | s == t = return ([])
+unify (TVar x) t | not (x `occurs` t) = return ([(x, t)])
+                 | otherwise = fayl("Occurs check failed on " ++ 
+                                    show (TVar x) ++ " and " ++ show t)
+unify t (TVar x) | not (x `occurs` t) = return ([(x, t)])
+                 | otherwise = fayl("Occurs check failed on " ++ 
+                                    show t ++ " and " ++ show (TVar x))
+unify TBool TBool = return ([])
+unify TNum TNum = return ([])
+unify TString TString = return ([])
+unify (TArr s t) (TArr u v) = 
+    do substSU <- unify s u
+       substTV <- unify (applyTySubst substSU t)
+                        (applyTySubst substSU v)
+       composeTySubst [substTV, substSU]
+unify (TList a) (TList b) = unify a b
+unify (TRecord a) (TRecord b) = 
+    let a' = sortAlist a 
+        b' = sortAlist b
+    in
+      do substs <- sequence
+                [if ax == bx then unify ay by else
+                     fayl ("Record types " ++ show a' ++ 
+                           " and " ++ show b' ++ 
+                           " mismatched.")
+                 | ((ax, ay), (bx, by)) <- zip a' b']
+         let (tySubsts) = substs
+         subst <- composeTySubst tySubsts
+         return (subst)
+unify a b = fayl("Type mismatch between " ++ 
+                 show a ++ " and " ++ show b)
+
+unifyAll :: [Type] -> Failure TySubst
+unifyAll [] = return ([])
+unifyAll [x] = return ([])
+unifyAll (x1:x2:xs) = do (tySubst) <- x1 `unify` x2
+                         unifyAll (map (applyTySubst tySubst)
+                                   (x2:xs))
+
+composeTySubst :: [TySubst] -> Failure TySubst
+composeTySubst [] = return $ ([])
+composeTySubst subst =
+    let (tySubsts) = subst in
+    do addlSubsts <- sequence $
+                         onCorresponding unifyAll $ concat tySubsts
+       let (addlTySubsts) = addlSubsts
+       let substs' = tySubsts ++ addlTySubsts
+       let tySubst = flip foldr1 substs'
+                 (\s1 s2 -> s1 ++ alistmap (applyTySubst s1) s2)
+       if any (\(a,b) -> occurs a b) tySubst then 
+          fayl "Circular type substitution in composeTySubst" 
+        else 
+            return (tySubst)
+
+prop_composeTySubst = 
+    forAll (genEnv 0) $ \a ->
+    forAll (genEnv (length a)) $ \b ->
+    forAll arbitrary $ \ty ->
+    disjointAlist a b && validEnv a && validEnv b ==>
+    (do ab <- composeTySubst[a, b]
+        return $ applyTySubst ab ty)
+    == (return $ (applyTySubst a $ applyTySubst b ty) :: Failure Type)
+
+-- unused
+disjoinSubst :: TySubst -> TySubst -> TySubst
+disjoinSubst a b =
+  [(image bx mapping, applyTySubst subst by) | (bx, by) <- b]
+    where mapping = (dom b ++ ftvsSubst b) `zip`
+                      ([0..] \\ (dom a ++ ftvsSubst a))
+          subst = alistmap TVar mapping
+
+instance Arbitrary Type where
+    arbitrary = 
+        oneof
+          [ return TBool
+          , return TNum
+          , return TString
+          , do s <- arbitrary
+               t <- arbitrary
+               return (TArr s t)
+          , do x <- posInt
+               return (TVar x)
+          ]
+
+-- Check that unification produces a substitution which actually
+-- unifies the two types. (Currently fails; something wrong with the way
+-- substitutions are composed or not.)
+prop_unify_apply_subst = 
+  forAll arbitrary $ \(a :: Type) ->
+  forAll arbitrary $ \(b :: Type) -> 
+    collect (numFtvs a, numFtvs b) $
+    failureToPropertyIgnoreFailure $
+    do (subst) <- a `unify` b
+       let e = applyTySubst subst a
+       let f = applyTySubst subst b
+       return $ eqUpTo runNormalizeType e f
+
+-- { Typing environments } ---------------------------------------------
+
+bind x v env = (x,v):env
diff --git a/Narc/TypeInfer.hs b/Narc/TypeInfer.hs
new file mode 100644
--- /dev/null
+++ b/Narc/TypeInfer.hs
@@ -0,0 +1,233 @@
+module Narc.TypeInfer where
+
+import Data.Maybe (fromMaybe)
+import Data.Either
+
+import Control.Monad.State (lift)
+
+import Test.HUnit
+
+import Gensym
+import Narc.AST
+import Narc.Type
+import Narc.Failure
+import Narc.Debug (debug)
+
+--
+-- Type inference ------------------------------------------------------
+--
+
+tyCheckTerms env terms = 
+    do results <- sequence [tyCheck env term | term <- terms]
+       let (tySubsts, terms') = unzip results
+       let (terms'', termTys) = unzip terms'
+       tySubst <- under $ composeTySubst tySubsts
+       return (tySubst, terms')
+
+-- | tyCheck env term infers a type for term in environment env.
+-- The environment has type [(Var, QType)];
+-- 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)
+tyCheck env (Unit, _) = 
+    do let ty = (TUnit)
+       return (emptyTySubst, (Unit, ty))
+tyCheck env (Bool b, _) = 
+    do let ty = (TBool)
+       return (emptyTySubst, (Bool b, ty))
+tyCheck env (Num n, _) = 
+    do let ty = (TNum)
+       return (emptyTySubst, (Num n, ty))
+tyCheck env (String s, _) = 
+    do let ty = (TString)
+       return (emptyTySubst, (String s, ty))
+tyCheck env (Table t tys, _) =
+    do let ty = (TList (TRecord tys))
+       return (emptyTySubst, (Table t tys, ty))
+tyCheck env (Var x, _) =
+    do let qTy = fromMaybe (error("Type error: no var " ++ x))
+                 $ lookup x env
+       ty <- lift $ instantiate qTy
+       debug ("*** instantiated " ++ show qTy ++ " to " ++ show ty) $
+        return (emptyTySubst, (Var x, (ty)))
+tyCheck env (PrimApp fun args, _) = 
+    do (tySubst, args) <- tyCheckTerms env args
+       return(tySubst, (PrimApp fun args, (TBool))) -- TBD
+tyCheck env (Abs x n, _) = 
+    do argTyVar <- lift gensym
+       (tySubst, n'@(_, (nTy))) <- 
+           tyCheck ((x, ([], TVar argTyVar)) : env) n
+       let argTy = applyTySubst tySubst $ TVar argTyVar
+       return(tySubst,
+              (Abs x n', (TArr argTy nTy)))
+tyCheck env (If c a b, _) =
+    do (cTySubst, c'@(_, (cTy))) <- tyCheck env c
+       (aTySubst, a'@(_, (aTy))) <- tyCheck env a
+       (bTySubst, b'@(_, (bTy))) <- tyCheck env b
+       cBaseTySubst <- under (unify cTy TBool)
+       abTySubst <- under $ unify aTy bTy
+       tySubst <- under $ composeTySubst
+                             [aTySubst, bTySubst, cTySubst,
+                              cBaseTySubst, abTySubst]
+       let ty = applyTySubst tySubst bTy
+       return (tySubst,
+               (If c' a' b', (ty)))
+tyCheck env (Nil, _) = 
+    do t <- lift gensym
+       return (emptyTySubst, (Nil, (TList (TVar t))))
+tyCheck env (Singleton m, _) =
+    do (tySubst, m'@(_, (mTy))) <- tyCheck env m
+       return (tySubst,
+               (Singleton m', (TList mTy)))
+tyCheck env (Union a b, _) =
+    do (aTySubst, a'@(_, (aTy))) <- tyCheck env a
+       (bTySubst, b'@(_, (bTy))) <- tyCheck env b
+       abTySubst <- under $ unify aTy bTy
+       tySubst <- under $ composeTySubst
+                             [aTySubst, bTySubst, abTySubst]
+       let ty = applyTySubst tySubst bTy
+       return (tySubst,
+               (Union a' b', (ty)))
+tyCheck env (Record fields, _) =
+    let (fieldNames, terms) = unzip fields in
+    do (tySubst, terms) <- tyCheckTerms env terms
+       let fieldTys = map snd terms
+       return (tySubst,
+               (Record (zip fieldNames terms),
+                (TRecord [(name,ty)| (ty, name) <- zip fieldTys fieldNames])))
+tyCheck env (Project m f, _) =
+    do rowVar <- lift gensym; a <- lift gensym
+       (tySubst, m'@(_, mTy)) <- tyCheck env m
+       case mTy of
+         TVar x ->     -- Note: bogus
+                return (((x, TRecord [(f, TVar a)]):tySubst),
+                        (Project m' f, (TVar a)))
+         TRecord fieldTys ->
+                case lookup f fieldTys of
+                  Nothing -> fail("no field " ++ f ++ " in record " ++ 
+                                  show (strip m))
+                  Just fieldTy ->
+                      return (tySubst,
+                              (Project m' f, fieldTy))
+         _ -> fail("Project from non-record type.")
+tyCheck env (App m n, _) = 
+    do a <- lift gensym; b <- lift gensym;
+       (mTySubst, m'@(_, (mTy))) <- tyCheck env m
+       (nTySubst, n'@(_, (nTy))) <- tyCheck env n
+       let nTy' = applyTySubst mTySubst $ nTy
+       let mTy' = applyTySubst nTySubst $ mTy
+       subExprTySubst <- under $ composeTySubst [mTySubst, nTySubst]
+       
+       let mArrTy = TArr (nTy') (TVar b)
+       mArrTySubst <- under $ unify mArrTy mTy'
+       
+       let resultTy = applyTySubst mArrTySubst $ TVar b
+       
+       tySubst <- under $ composeTySubst [mArrTySubst,
+                                          subExprTySubst]
+       
+       return (tySubst,
+               (App m' n', (resultTy)))
+
+tyCheck env term@(Comp x src body, d) =
+    do (substSrc, src') <- tyCheck env src
+       let srcTy = typeAnno 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'
+       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 []
+
+infer :: Term a -> ErrorGensym TypedTerm -- FIXME broken, discards subst'n
+infer term =
+    do initialTyEnv <- makeInitialTyEnv
+       (_, term') <-
+        --    runErrorGensym $ 
+               tyCheck initialTyEnv term
+       return term'
+
+infer' :: Term' a -> ErrorGensym TypedTerm
+infer' term = infer (term, undefined)
+
+runInfer = runErrorGensym . infer
+
+runTyCheck env m = runErrorGensym $ 
+    do initialTyEnv <- makeInitialTyEnv
+       (subst, m') <- tyCheck (initialTyEnv++env) m
+       return $ retagulate (applyTySubst subst . snd) m'
+
+inferTys :: Term () -> ErrorGensym Type
+inferTys m = 
+    do (_, (ty)) <- infer m
+       return (ty)
+
+inferType :: Term () -> ErrorGensym Type
+inferType m = infer m >>= (return . snd)
+
+runInferType = runErrorGensym . inferType
+
+inferType' :: Term' () -> ErrorGensym Type
+inferType' m = infer' m >>= (return . snd)
+
+-- UNIT TESTS ----------------------------------------------------------
+
+unitAssert b = assertEqual "." b True
+
+tyCheckTests =
+    TestList ["Simple application of id to table" ~:
+                     (runErrorGensym $ 
+                       inferTys (App (Abs "x" (Var "x", ()), ())
+                              (Table "wine" [], ()), ()))
+                       ~?= (TList (TRecord [])),
+              "Curried application of id to table" ~:
+                     (runErrorGensym . inferTys)
+                     (App (App
+                              (Abs "x" (Abs "y" (App (Var "x", ())
+                                                     (Var "y", ()), ()), ()), ())
+                                 (Abs "x" (Var "x", ()), ()), ())
+                                 (Table "wine" [], ()), ())
+                       ~?= (TList (TRecord [])),
+              "Curried application, de/reconstructing record" ~:
+                     (runErrorGensym . inferTys) 
+                     (App (App
+                      (Abs "f" (Abs "x" (App (Var "f",()) (Var "x",()),()),()),())
+                      (Abs "x"
+                       (Record[("baz", (Project(Var "x",()) "foo", ()))],
+                        ()),
+                       ()), ())
+                      (Record [("foo", (Num 47, ()))], ()), ())
+                      ~?= (TRecord[("baz", TNum)]),
+              "omega" ~:
+                    unitAssert $ isError $
+                      (tryErrorGensym . inferType)
+                      (Abs "x" (App (Var "x", ()) (Var "x", ()), ()), ())
+                  ]
+
+typingTest1 = 
+  let idTy = (TArr (TVar 9) (TVar 9)) in
+  let concatMapTy = (TArr (TArr (TVar 2) (TList (TVar 3)))
+                     (TArr (TList (TVar 2))
+                               (TList (TVar 3)))) in
+  let Right mArrSubst = unify concatMapTy  (TArr (TVar 4) (TVar 5)) in
+  let argTy = applyTySubst mArrSubst (TVar 4) in
+             -- TArr (TVar 2) ([],Just 0) (TList (TVar 3))
+  let Right funcArgSubst = unify argTy idTy in
+  let resultTy = (applyTySubst funcArgSubst $ applyTySubst mArrSubst (TVar 5)) 
+  in
+  (resultTy, funcArgSubst,
+   case resultTy of
+   TArr (TList (TList (TVar a))) (TList (TVar b)) -> a == b)
+
+typingTest = let (_,_,x) = typingTest1 in 
+             TestCase (unitAssert x)
diff --git a/Narc/Util.hs b/Narc/Util.hs
new file mode 100644
--- /dev/null
+++ b/Narc/Util.hs
@@ -0,0 +1,111 @@
+module Narc.Util where
+
+import Data.Maybe (fromJust, isJust)
+import Data.List as List ((\\), nub, intersperse, groupBy, sortBy, sort)
+
+--
+-- List Utilities
+--
+
+dom alist = map fst alist
+rng alist = map snd alist
+
+collate proj = groupBy (\x y -> proj x == proj y) . 
+               sortBy (\x y -> proj x `compare` proj y)
+
+sortAlist :: [(String, b)] -> [(String, b)]
+sortAlist = sortBy (\a b -> fst a `compare` fst b)
+
+cross f g (x,y) = (f x, g y)
+
+onRight f = cross id f
+onLeft f = cross f id
+
+-- | shadow: given two alists, return the elements of the first that
+-- are NOT mapped by the second
+shadow as bs = [(a,x) | (a,x) <- as, a `notElem` domBs]
+    where domBs = map fst bs
+
+-- | Tests that an alist or environment is well-formed: that its first
+-- | components are all unique.
+validEnv xs = length (nub $ map fst xs) == length xs
+
+mr agg xs = map reduceGroup (collate fst xs)
+    where reduceGroup xs = let (as, bs) = unzip xs in
+                             (the as, agg bs)
+          the xs | allEq xs = head xs
+
+onCorresponding :: Ord a => ([b]->c) -> [(a,b)] -> [c]
+onCorresponding agg xs = map reduceGroup (collate fst xs)
+    where reduceGroup xs = agg $ map snd xs
+
+($>) x f = f x
+
+image x = fromJust . lookup x
+
+maps x = isJust . lookup x
+
+intSqrt :: Integral a => a -> a
+intSqrt = floor . sqrt . fromIntegral
+
+unassoc a = filter ((/= a) . fst)
+
+nubassoc [] = []
+nubassoc ((x,y):xys) = (x,y) : (nubassoc $ unassoc x xys)
+
+graph f xs = [(x, f x) | x <- xs]
+alistmap f = map (\(a, b) -> (a, f b))
+
+bagEq a b = a \\ b == [] && b \\ a == []
+
+setEq a b = (nub a) `bagEq` (nub b)
+
+u a b = nub (a ++ b)
+
+contains a b = null(b \\ a)
+
+setMinus xs ys = nub $ sort $ xs \\ ys
+
+(\\\) xs ys = setMinus xs ys
+
+allEq [] = True
+allEq (x:xs) = all (== x) xs
+
+disjoint :: Eq a => [a] -> [a] -> Bool
+disjoint xs ys = not (any (\x-> any (==x) ys) xs)
+
+disjointAlist xs ys = disjoint (map fst xs) (map fst ys)
+-- disjointAlist [] _ = True
+-- disjointAlist _ [] = True
+-- disjointAlist xs ((a,b):ys) =
+--     (not $ any ((== a) . fst) xs) && disjointAlist xs ys
+
+-- | Convert a maybe to a zero-or-one-element list.
+asList :: Maybe a -> [a]
+asList Nothing = []
+asList (Just x) = [x]
+
+isRight :: Either a b -> Bool
+isRight (Right _) = True
+isRight (Left _ ) = False
+
+isLeft :: Either a b -> Bool
+isLeft (Left _) = True
+isLeft (Right _ ) = False
+
+-- | zipAlist: given two alists with the same domain,
+-- returns an alist mapping each of those domain values to
+-- the pair of the two corresponding values from the given lists.
+zipAlist xs ys = 
+    let xsys = zip (sortAlist xs) (sortAlist ys) in
+    if not $ and [x == y | ((x, a), (y, b)) <- xsys] then 
+        error "alist mismatch in zipAlist"
+    else [(x, (a, b)) | ((x, a), (y, b)) <- xsys]
+
+-- | mapstrcat: transform a list to one of strings, with a given
+-- | function, and join these together with some `glue' string.
+mapstrcat :: String -> (a -> String) -> [a] -> String
+mapstrcat glue f xs = concat $ List.intersperse glue (map f xs)
+
+-- Functional utilities
+eqUpTo f x y = f x == f y
diff --git a/Narc/Var.hs b/Narc/Var.hs
new file mode 100644
--- /dev/null
+++ b/Narc/Var.hs
@@ -0,0 +1,4 @@
+module Narc.Var where
+
+type Var = String
+
diff --git a/QCUtils.hs b/QCUtils.hs
new file mode 100644
--- /dev/null
+++ b/QCUtils.hs
@@ -0,0 +1,192 @@
+{-# LANGUAGE BangPatterns, ScopedTypeVariables #-}
+
+module QCUtils where
+
+import Prelude hiding (catch)
+import Test.QuickCheck
+import Control.Exception
+import Foreign (unsafePerformIO)
+
+import System.Random
+
+{- Wrappers for detecting exceptions -}
+
+-- | @propertyDefined x@ is a property asserting that @x@ can be
+-- | forced without error.
+propertyDefined :: a -> Property
+propertyDefined exp = unsafePerformIO $ 
+                      catch (do x <- evaluate exp
+                                return $ property True)
+                            (\(exc::SomeException) -> return $ property False)
+
+-- | @excAsFalse x@ is a property that acts like @x@, except that it
+-- | is @False@ when @x@ would throw an exception (and never throws an
+-- | exception itself).
+excAsFalse :: Testable a => a -> Property
+excAsFalse exp = unsafePerformIO $ 
+                     catch (do x <- evaluate exp
+                               return $ property x)
+                           (\(exc::SomeException) -> return $ property False)
+
+-- | Convert an arbitrary value into a @Maybe@ by forcing it,
+-- | catching errors and treating them as @Nothing@.
+excAsNothing :: a -> Maybe a
+excAsNothing exp = unsafePerformIO $ 
+                     catch (do x <- evaluate exp
+                               return $ Just x)
+                           (\(exc::SomeException) -> return Nothing)
+
+-- | A predicate asserting that forcing a thunk produces an error
+-- | (useful for tests that want to ensure error is thrown).
+throws :: a -> Bool
+throws exp = unsafePerformIO $ 
+             catch (do !x <- evaluate exp
+                       return $ False)
+                   (\(exc::SomeException) -> return True)
+
+-- | Compare two functions at a particular input, incl. error
+-- behavior.
+f_equal x f g = (excAsNothing $ f x) == (excAsNothing $ g x)
+
+{- Some simple generators -}
+
+arbChar :: Gen Char
+arbChar = elements $ ['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['_', ' ', '!']
+
+arbLetter :: Gen Char
+arbLetter = elements $ ['a'..'z'] ++ ['A'..'Z'] 
+
+arbWordChar :: Gen Char
+arbWordChar = frequency [(1, elements $ ['a'..'z'] ++ ['A'..'Z']),
+                         (1, elements ['_'])]
+
+
+arbStringLen :: Gen Char -> Int -> Gen String
+arbStringLen charGen 0 = return ""
+arbStringLen charGen n = do str <- arbStringLen charGen (n-1)
+                            ch <- charGen
+                            return $ ch : str
+
+-- | arbString: Generate a string of some length between 0 and 6, each length 
+-- with equal probability
+arbString charGen = frequency [(1, arbStringLen charGen len)| len <- [0..6]]
+
+arbStringSized charGen = sized (\n -> arbStringLen charGen n)
+
+genIntLt n = elements [0..n-1]
+
+vecTor :: Int -> Gen a -> Gen [a]
+vecTor n _ | n < 0 = error "vector with negative # of elements"
+vecTor 0 gen = return []
+vecTor n gen = do x <- gen; xs <- vecTor (n-1) gen; return $ x : xs
+
+posInt :: (Num a, Arbitrary a) => Gen a
+posInt = fmap ((+1) . abs) arbitrary
+
+nonNegInt :: (Num a, Arbitrary a) => Gen a
+nonNegInt = fmap abs arbitrary
+
+expIntGen n = frequency [(1, return n), (1, expIntGen (n+1))]
+
+-- Combinators for writing conditional generators
+
+whens p e = if p then e else []
+
+{- Configurations for small, big, and huge test runs -}
+
+small = stdArgs
+
+big = Args {
+    maxSuccess = 1000,
+    maxDiscard = 1000,
+    maxSize = 12,
+    replay = Nothing,
+    chatty = False
+  }
+
+huge = Args {
+    maxSuccess = 10000,
+    maxDiscard =  5000,
+    maxSize = 20,
+    replay = Nothing,
+    chatty = False
+  }
+
+{- General list functions -}
+
+histogram [] result = result
+histogram (x : xs) result =
+    histogram xs (incLookup x result)  
+    where incLookup x [] = [(x, 1)]
+          incLookup x ((y, yN):ys) | x == y    = (y,yN+1) : ys
+                                   | otherwise = (y,yN)   : (incLookup x ys)
+
+subsets [] = [[]]
+subsets (x:xs) = 
+    let xsSubsets = subsets xs in
+    map (x:) xsSubsets ++ xsSubsets
+
+chooseSubset [] n = []
+chooseSubset (x:xs) 0 = []
+chooseSubset (x:xs) n = if n `mod` 2 == 1 then x : chooseSubset xs (n `div` 2)
+                        else chooseSubset xs (n `div` 2)
+
+arbSubset xs = do n <- posInt :: Gen Int
+                  return $ chooseSubset xs n
+
+genEnv :: (Arbitrary a, Num a, Enum a, Arbitrary b) => a -> Gen [(a, b)]
+genEnv min = 
+    do n <- arbitrary
+       sequence [do ty <- arbitrary; return (i, ty)
+                 | i <- [min..min+pred(abs n)]]
+
+failProp = property False
+
+ignore = False ==> (undefined::Bool)
+
+-- QuickCheck settings -------------------------------------------------
+
+tinyArgs :: Args
+tinyArgs = Args {
+    maxSuccess = 100,
+    maxDiscard = 100,
+    maxSize = 8,
+    replay = Nothing,
+    chatty = False
+  }
+
+verySmallArgs :: Args
+verySmallArgs = Args {
+    maxSuccess = 1000,
+    maxDiscard = 1000,
+    maxSize = 12,
+    replay = Nothing,
+    chatty = False
+  }
+
+smallArgs :: Args
+smallArgs = Args {
+    maxSuccess = 10000,
+    maxDiscard = 10000,
+    maxSize = 16,
+    replay = Nothing,
+    chatty = False
+  }
+
+mediumArgs :: Args
+mediumArgs = Args {
+    maxSuccess = 100,
+    maxDiscard = 100,
+    maxSize = 100,
+    replay = Nothing,
+    chatty = False
+  }
+
+bigArgs :: Args
+bigArgs = Args {
+    maxSuccess = 1000,
+    maxDiscard = 1000,
+    maxSize = 500,
+    replay = Nothing,
+    chatty = False
+  }
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/narc.cabal b/narc.cabal
new file mode 100644
--- /dev/null
+++ b/narc.cabal
@@ -0,0 +1,61 @@
+-- narc.cabal auto-generated by cabal init. For additional options,
+-- see
+-- http://www.haskell.org/cabal/release/cabal-latest/doc/users-guide/authors.html#pkg-descr.
+-- The name of the package.
+Name:                narc
+
+-- 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
+
+-- 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:         
+
+-- URL for the project homepage or repository.
+Homepage:            http://ezrakilty.net/projects/narc
+
+-- The license under which the package is released.
+License:             BSD3
+
+-- The file containing the license text.
+License-file:        LICENSE
+
+-- The package author(s).
+Author:              Ezra e. k. Cooper
+
+-- An email address to which users can send suggestions, bug reports,
+-- and patches.
+Maintainer:          ezra@ezrakilty.net
+
+-- A copyright notice.
+-- Copyright:           
+
+Category:            Database
+
+Build-type:          Simple
+
+-- Extra files to be distributed with the package, such as examples or
+-- a README.
+-- Extra-source-files:  
+
+-- Constraint on the version of Cabal needed to build this package.
+Cabal-version:       >=1.2
+
+
+Library
+  -- Modules exported by the library.
+  Exposed-modules:     Narc, Narc.AST, Narc.Common, Narc.Compile, Narc.Eval, Narc.Failure, Narc.Pretty, Narc.Rewrite, Narc.SQL, Narc.Test, Narc.Type, Narc.TypeInfer, Narc.Util, Narc.AST.Pretty, Narc.Failure.QuickCheck, Narc.SQL.Pretty, 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, Narc.TermGen, Narc.Var, Narc.Contract, Narc.Debug
+  
+  -- Extra tools (e.g. alex, hsc2hs, ...) needed to build the source.
+  -- Build-tools:         
+