diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,24 @@
+Copyright (c) 2016, The Charles Stark Draper Laboratory, Inc.
+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.
+    * Neither the name of the <organization> nor the
+      names of its contributors may be used to endorse or promote products
+      derived from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "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 CHARLES STARK DRAPER LABORATORY, INC 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/Language/CSPM/Pretty.hs b/Language/CSPM/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/Language/CSPM/Pretty.hs
@@ -0,0 +1,688 @@
+{- |
+   Module      :  Language.CSP.Pretty
+   Description :  Pretty printing for the CSP abstract syntax
+   Copyright   :  Draper Laboratories
+   
+   The two functions in the module are used for pretty-printing the abstract CSP
+   syntax.  The output is intended to be readable by FDR3.
+-}
+
+module Language.CSPM.Pretty (emitMod, emitMods) where
+
+import Language.CSPM.Syntax
+import Text.PrettyPrint
+import Data.List
+import Control.Monad
+import qualified Data.Map as M
+import qualified Data.Set as S
+
+-- We need to keep track of which identifiers are in scope, so that we can use
+-- simple names where possible.  We use a state monad (note: not a reader
+-- monad, since there are globals, though we do provide reader like
+-- functionality).  The state consists of three parts: 
+--
+-- - A map of identifiers to Doc, which says how to print anything currently
+--   in scope.
+--
+-- - A Set, which just contains the range of the map.  When we see a new
+--   identifier, we need to check that the way we want to print it doesn't
+--   conflict with things already in scope.  Keeping a around is much more
+--   efficient than getting the range of the map as a list and searching that.
+--
+-- - A list of "warnings".  If we encounter an identifier that's not in scope,
+--   we have to guess about how to print it.  This may not be safe, so we note
+--   the problem in the warnings.
+--
+-- Additionally, because CSP declarations may be mutually recursive, we do a
+-- first pass to add all the global variables to the monad.  This first pass
+-- also shows up where a block of local definitions may be mutually recursive,
+-- as in let-within clauses.
+
+data PPState = PPState {ppIdMap    :: !(M.Map Id String),
+                        ppUsedDocs :: !(S.Set String),
+                        ppWarnings :: ![String]}
+
+emptyPPState :: PPState
+emptyPPState = PPState {ppIdMap    = M.empty,
+                        ppUsedDocs = S.empty,
+                        ppWarnings = []}
+
+newtype PP a = PP (PPState -> (PPState,a))
+
+unPP :: PP a -> PPState -> (PPState,a)
+unPP (PP f) = f
+
+instance Functor PP where
+  fmap f (PP g) = PP (\st -> fmap f (g st))
+
+instance Monad PP where
+  return x  = PP $ \pps -> (pps,x)
+  m >>= k   = PP $ \pps -> let (pps',res) = unPP m pps in unPP (k res) pps'
+
+instance Applicative PP where
+  pure = return
+  (<*>) = ap
+
+
+runPP :: PPState -> PP a -> (a,[String])
+runPP st (PP f) = let (st',res) = f st in (res, ppWarnings st')
+
+getIdMap :: PP (M.Map Id String)
+getIdMap = PP $ \pps -> (pps,ppIdMap pps)
+
+warn :: String -> PP ()
+warn warning = PP $ \pps -> (pps {ppWarnings = warning : ppWarnings pps},())
+
+addGlobal :: Id -> PP Doc
+addGlobal var = PP $ \pps -> 
+  let ppvar = if S.member niceVersion (ppUsedDocs pps)
+                then uglyVersion
+                else niceVersion
+  in
+    (pps {ppIdMap = M.insert var ppvar (ppIdMap pps),
+          ppUsedDocs = S.insert ppvar (ppUsedDocs pps)},
+     text ppvar)
+  where
+    niceVersion :: String
+    niceVersion = namePart var
+
+    uglyVersion :: String
+    uglyVersion =
+      case var of
+        Id (s,i) -> s ++ show i
+        Fixed s  -> s
+
+addLocal :: Id -> (Doc -> PP a) -> PP a
+addLocal var action = PP $ \pps ->
+  case M.lookup var (ppIdMap pps) of
+    Just d -> unPP (action $ text d) pps
+    Nothing -> 
+      let ppvar = if S.member niceVersion (ppUsedDocs pps)
+                    then uglyVersion
+                    else niceVersion 
+          
+          (pps',result) = 
+             unPP (action $ text ppvar) $
+               pps {ppIdMap = M.insert var ppvar (ppIdMap pps),
+                    ppUsedDocs = S.insert ppvar (ppUsedDocs pps)}
+      in 
+        (pps' {ppIdMap = M.delete var (ppIdMap pps'),
+               ppUsedDocs = S.delete ppvar (ppUsedDocs pps')},
+         result)
+      where
+        niceVersion :: String
+        niceVersion = namePart var
+    
+        uglyVersion :: String
+        uglyVersion =
+          case var of
+            Id (s,i) -> s ++ show i
+            Fixed s  -> s
+
+addLocals :: [Id] -> ([Doc] -> PP a) -> PP a
+addLocals vars action =  addLocalsRec vars []
+  where
+    addLocalsRec []     ds = action $ reverse ds
+    addLocalsRec (v:vs) ds = 
+      addLocal v $ \d -> addLocalsRec vs (d:ds)
+
+---
+
+ppId :: Id -> PP Doc
+ppId var = do 
+  idmap <- getIdMap
+  case M.lookup var idmap of
+    Just d -> return $ text d
+    Nothing -> do
+      pp <- 
+        case var of
+          Fixed s  -> return s
+          Id (s,i) -> do 
+            warn $ "Identifier " ++ show var ++ " not found."
+            return $ s ++ show i
+      return $ text pp
+
+-------------------------------
+
+commas :: [Doc] -> Doc
+commas es = hsep $ punctuate comma es
+
+dots :: [Doc] -> Doc
+dots es = hcat $ punctuate (char '.') es
+
+ppFDRMod :: FDRMod -> PP Doc
+ppFDRMod tops = do
+  addTLGlobals tops
+  ttops <- mapM ppDefinition $ topLevels tops
+  return $ vcat $ punctuate (text "\n") ttops
+
+-- This takes a pattern and does two things: tells you how it should be
+-- displayed, and extends the local scope with the relevant identifiers for
+-- the duration of the pretty printing.
+ppPattern :: Pat -> (Doc -> PP a) -> PP a
+ppPattern (PId var)         f = addLocal var f
+ppPattern (PConcat p1 p2)   f = ppBinaryPattern p1 p2 (char '^') f
+ppPattern (PDot p1 ps)      f = ppPatList (p1:ps) (char '.') f
+ppPattern (PDouble p1 p2)   f = ppBinaryPattern p1 p2 (text "@@") f
+ppPattern (PList pats)      f = 
+  ppPatList pats comma $ \ppats -> f $ char '<' <> ppats <> char '>'
+ppPattern (PConst c)        f = f $ ppConst c
+ppPattern PEmptySet         f = f $ text "{}"
+ppPattern (PSingletonSet p) f = ppPattern p $ \pp -> f $ braces pp
+ppPattern (PTuple pats)     f =
+  ppPatList pats comma $ \ppats -> f $ parens ppats
+ppPattern PWildCard         f = f $ char '_'
+
+-- abstract out the common case of printing a binary pattern
+ppBinaryPattern :: Pat -> Pat -> Doc -> (Doc -> PP a) -> PP a
+ppBinaryPattern p1 p2 pnct f = do
+  ppPatParens p1 $ \pp1 -> 
+    ppPatParens p2 $ \pp2 ->
+      f $ pp1 <> pnct <> pp2
+
+-- abstract out the common case of printing a list of patterns
+ppPatList :: [Pat] -> Doc -> (Doc -> PP a) -> PP a
+ppPatList pats pnct f = patList pats []
+  where
+--    patList :: [Exp] -> [Doc] -> PP a
+    patList []     ds = f $ hcat $ punctuate pnct $ reverse ds
+    patList (p:ps) ds = ppPatParens p $ \d -> patList ps (d:ds)
+
+
+-- prints the pattern with an extra set of parens if it's not a var
+ppPatParens :: Pat -> (Doc -> PP a) -> PP a
+ppPatParens p@(PId _) f = ppPattern p f
+ppPatParens p f = ppPattern p (\d -> f $ parens d)
+
+-- print a datatype constructor declaration
+ppConstructor :: (Id,[Exp]) -> PP Doc
+ppConstructor (c,tys) = do
+  tc  <- ppId c
+  ttys <- mapM ppExp tys
+  return $ dots (tc : map parens ttys)
+
+ppDefinition :: Definition -> PP Doc
+ppDefinition (DVar p e) = do
+  -- Note that this may "double add" the variables in the pattern to the map,
+  -- since they were probably added when we entered the scope of this definition
+  -- as part of handling mutually recursive definitions.  This is fine, because
+  -- ppPattern calls addLocal, which handles existing variables declarations
+  -- gracefully.
+  ppPattern p $ \pp -> do
+    pe <- ppExp e
+    return $ pp <+> char '=' <+> pe
+ppDefinition (DFun funName funClauses) = do
+  tname <- ppId funName
+  vcat <$> mapM (ppFunClause tname) funClauses
+  where
+    ppFunClause :: Doc -> ([Pat],Exp) -> PP Doc
+    ppFunClause fnm (pats,body) = ppPatList pats (char ',') $ \ppats -> do
+      pbody <- ppExp body
+      return $ fnm <+> parens ppats <+> char '=' $+$ (nest 2 $ pbody)
+ppDefinition (DAnnot x t) = do
+  px <- ppId x
+  pt <- ppType t
+  return $ px <+> text "::" <+> pt
+ppDefinition (DDataType nm cnstrs) = do
+  tnm <- ppId nm
+  tcnstrs <- mapM ppConstructor cnstrs
+  return $ 
+    text "datatype" <+> tnm <+> char '=' 
+       <+> (hcat $ punctuate (text " | ") tcnstrs)
+ppDefinition (DSubType nm cnstrs) = do
+  tnm <- ppId nm
+  tcnstrs <- mapM ppConstructor cnstrs
+  return $ 
+    text "subtype" <+> tnm <+> char '=' 
+       <+> (hcat $ punctuate (text " | ") tcnstrs)
+ppDefinition (DChan xs []) = do 
+  pxs <- commas <$> mapM ppId xs
+  return $ text "channel" <+> pxs
+ppDefinition (DChan xs tys) = do
+  pxs <- commas <$> mapM ppId xs
+  ptys <- mapM ppType tys
+  return $ text "channel" <+> pxs <+> colon <+> dots ptys
+ppDefinition (DInclude str) = 
+  return $ text "include" <+> text (show str) --- XXXX hack for escape chars
+ppDefinition (DExternal x) = do
+  px <- ppId x
+  return $ text "external" <+> px
+ppDefinition (DTransparent x) = do
+  px <- ppId x
+  return $ text "transparent" <+> px
+ppDefinition (DAssert a m) = do
+  pa <- ppAssertion a m
+  return $ text "assert" <+> pa
+
+--just the letter part, not the brackets or [T=
+modelLetter :: Model -> String
+modelLetter MT  = "T"
+modelLetter MF  = "F"
+modelLetter MFD = "FD"
+
+--This is [T] or [FD], etc.
+ppModel :: Model -> Doc
+ppModel = brackets . text . modelLetter
+
+ppAssertion :: Assertion -> Model -> PP Doc
+ppAssertion (ARefines p q) m = do
+  pp <- ppExp p
+  pq <- ppExp q
+  return $ pp <+> text ('[' : pm ++ "=") <+> pq
+  where
+    pm = modelLetter m
+ppAssertion (ADeadlockFree p) m = do
+  pp <- ppExp p
+  let pm = ppModel m
+  return $ pp <+> text ":[deadlock free" <+> pm <> char ']'
+ppAssertion (ADivergenceFree p) m = do
+  pp <- ppExp p
+  let pm = ppModel m
+  return $ pp <+> text ":[divergence free" <+> pm <> char ']'
+ppAssertion (ADeterministic p) m = do
+  pp <- ppExp p
+  let pm = ppModel m
+  return $ pp <+> text ":[deterministic" <+> pm <> char ']'
+ppAssertion (AHasTrace p t) m = do
+  pp <- ppExp p
+  pe <- ppExp t
+  let pm = ppModel m
+  return $ pp <+> text ":[has trace" <+> pm <> text "]:" <+> pe
+
+
+ppType :: Type -> PP Doc
+ppType TEvent        = return $ text "Event"
+ppType TChar         = return $ text "Char"
+ppType TBool         = return $ text "Bool"
+ppType TInt          = return $ text "Int"
+ppType TUnit         = return $ text "Unit"
+ppType (TList t)     = do
+  pt <- ppType t
+  return $ char '<' <+> pt <+> char '>'
+ppType (TSet t)      = do
+  pt <- ppType t
+  return $ braces pt
+ppType (TMap t1 t2)  = do
+  pt1 <- ppType t1
+  pt2 <- ppType t2
+  return $ text "(|" <+> pt1 <+> text "=>" <+> pt2 <+> text "|)"
+ppType (TData x)     = ppId x
+ppType (TRange a b)  = do 
+  pa <- ppExpParens a
+  pb <- ppExpParens b
+  return $ braces $ (parens pa) <> text ".." <> (parens pb)
+ppType TProc         = return $ text "Proc"
+
+-- Printing comprehension/set statements.  Three notes:
+--
+-- 1) We take in a list of comprehension statements rather than each
+--    individually for reasons of scope.  In particular, you can write
+--    comprehensions like:
+--    
+--       < x+1 | x <- xs, isOdd(x) >
+-- 
+--    Here, the later comprehension statement "isOdd(x)" needs "x" to be in
+--    scope.
+-- 
+-- 2) For the same reason, ppCompStmts takes in an argument indicating the
+--    monadic scope of the local variables declared in the patterns (much like
+--    addLocal and ppPattern).
+--
+-- 3) FDR3 appears to support both the "x <- a" syntax that is natural in
+--    comprehensions, as in:
+--
+--      < x+1 | x <- xs >
+-- 
+--    and the "x : a" syntax that is natural in replicated operations, as in:
+--
+--     [] x : {0..5} @ P(x)
+--
+--    These mean the same thing, and it appears you can use either syntax in
+--    either place.  For uniformity, we use only the "<-" syntax, since it is
+--    the one mentioned on the relevant fdr page:
+--
+--      https://www.cs.ox.ac.uk/projects/fdr/manual/cspm/syntax.html#csp-statements
+ppCompStmt :: [CompStmt] -> (Doc -> PP a) -> PP a
+ppCompStmt cs f = ppCS cs []
+  where
+    -- ppCS :: [CompStmt] -> [Doc] -> PP a
+    ppCS []                ds = 
+      f $ commas $ reverse ds
+    ppCS (CSGen p e : css) ds = do
+      pe <- ppExp e
+      ppPattern p $ \pp -> ppCS css (pp <+> text "<-" <+> pe : ds)
+    ppCS (CSPred e : css)  ds = do
+      pe <- ppExp e
+      ppCS css (pe : ds)
+
+-- Printing expressions
+ppExp :: Exp -> PP Doc
+ppExp (EId x) = ppId x
+ppExp (ELambda pats e) = 
+  ppPatList pats comma $ \ppats -> do
+    te <- ppExp e
+    return $ char '\\' <+> ppats <+> char '@' <+> te
+ppExp (EApp fun es) = do
+  tfun <- ppExpParens fun
+  tes <- mapM ppExp es
+  return $ tfun <> (parens $ commas tes)
+ppExp (ELet defs e) = do
+  addTLLocals (FDRMod defs) $ do
+    pdefs <- mapM ppDefinition defs
+    pe <- ppExp e
+    return $ text "let" $$ nest 2 (vcat $ punctuate (text "\n") pdefs)
+                        $$ text "within" $$ (nest 2 pe)
+ppExp (EIfThenElse c e1 e2) = do
+  tc <- ppExp c
+  te1 <- ppExp e1
+  te2 <- ppExp e2
+  return $ 
+     text "if" <+> tc <+> text "then" $+$ (nest 2 te1)
+                       $$ text "else" $+$ (nest 2 te2)
+ppExp (EUOp op e) = do
+  te <- ppExpParens e
+  return $ ppUOp op <+> te
+ppExp (EBinOp e1 op e2) = ppBOpExp e1 (ppBinOp op) e2
+ppExp (EConst c) = return $ ppConst c
+ppExp (EError s) = return $ text "error" <> (parens $ text $ show s)
+ppExp (EDot e es) = do 
+  te <- ppExpParens e
+  tes <- mapM ppExpParens es
+  return $ dots (te:tes)
+ppExp (EExtChoice e1 e2) = ppBOpExp e1 (text "[]") e2
+ppExp (EGuarded e1 e2)   = ppBOpExp e1 (char '&') e2
+ppExp (EHide e1 e2)      = ppBOpExp e1 (char '\\') e2
+ppExp (EIntChoice e1 e2) = ppBOpExp e1 (text "|~|") e2
+ppExp (EPrefix e1 ces e2) = do
+  te1 <- ppExpParens e1
+  tces_te2 <- ppCommsPrefix ces []
+  return $ te1 <> tces_te2
+  where
+    ppCommsPrefix :: [(CommField)] -> [Doc] -> PP Doc
+    ppCommsPrefix [] ds = do 
+      te2 <- ppExpParens e2
+      return $ hcat $ reverse $ te2 : (text " -> ") : ds
+    ppCommsPrefix (comm:comms) ds =
+      case ppComm comm of
+        (d,Left e) -> do 
+          pe <- ppExpParens e
+          ppCommsPrefix comms ((d <> pe) : ds)
+        (d,Right p) ->
+          ppPattern p $ \pp -> 
+            ppCommsPrefix comms ((d <> pp) : ds)
+      where
+        -- How to display the comm, and whether the thing that comes after it
+        -- is a binder (as in the case of "c?x -> ...") or not (as in the case
+        -- of "c!x -> ..."
+        ppComm :: CommField -> (Doc,Either Exp Pat)
+        ppComm (CFPlain e)   = (char '.', Left e)
+        ppComm (CFInput p)   = (char '?', Right p)
+        ppComm (CFOutput e)  = (char '!', Left e)
+        ppComm (CFNDInput p) = (char '$', Right p)
+ppExp (EProject e1 e2) = ppBOpExp e1 (text "|\\") e2
+ppExp (ERename e1 nms) = do
+  pe1 <- ppExpParens e1
+  pnms <- mapM (\(n1,n2) -> (,) <$> ppExpParens n1 <*> ppExpParens n2) nms
+  let prnms = map (\(pn1,pn2) -> pn1 <+> text "<-" <+> pn2) pnms
+  return $ pe1 <+> text "[[" <+> commas prnms <+> text "]]"
+ppExp (EAlphaParallel p a b q) = do
+  pa <- ppExpParens a
+  pb <- ppExpParens b
+  ppBOpExp p (brackets $ pa <+> text "||" <+> pb) q
+ppExp (EGenParallel p a q) = do
+  pa <- ppExp a
+  ppBOpExp p (text "[|" <+> pa <+> text "|]") q
+ppExp (EInterleave e1 e2) = ppBOpExp e1 (text "|||") e2
+ppExp (EException p a q)  = do
+  pa <- ppExp a
+  ppBOpExp p (text "[|" <+> pa <+> text "|>") q
+ppExp (EInterrupt e1 e2)  = ppBOpExp e1 (text "/\\") e2
+ppExp (ESeq e1 e2)        = ppBOpExp e1 (char ';') e2
+ppExp (ELinkedParallel p nms q) = do
+  pnms <- mapM (\(c,d) -> (,) <$> ppExpParens c <*> ppExpParens d) nms
+  let ppnms = commas $ map (\(pc,pd) -> pc <+> text "<->" <+> pd) pnms
+  ppBOpExp p ppnms q
+ppExp (ETimeout e1 e2)    = ppBOpExp e1 (text "[>") e2
+ppExp (ESyncExtChoice p a q) = do
+  pa <- ppExp a
+  ppBOpExp p (text "[+" <+> pa <+> text "+]") q
+ppExp (ESyncInterrupt p a q) = do
+  pa <- ppExp a
+  ppBOpExp p (text "/+" <+> pa <+> text "+\\") q
+ppExp (ERepAlphaParallel cs a p) =
+  ppCompStmt cs $ \pstmts -> do
+    pa <- ppExp a
+    pp <- ppExpParens p
+    return $ text "||" <+> pstmts <+> char '@' <+> brackets pa <+> pp
+ppExp (ERepExtChoice cs p)     = ppRepExp (text "[]") cs p
+ppExp (ERepGenParallel a cs p) = do
+  pa <- ppExp a
+  ppRepExp (text "[|" <+> pa <+> text "|]") cs p
+ppExp (ERepInterleave cs p)    = ppRepExp (text "|||") cs p
+ppExp (ERepIntChoice cs p)     = ppRepExp (text "|~|") cs p
+ppExp (ERepLinkedParallel links cs p) = do
+  plinks <- mapM (\(l,r) -> (,) <$> ppExpParens l <*> ppExpParens r) links
+  let linkedLinks = map (\(pl,pr) -> pl <+> text "<->" <+> pr) plinks
+  ppRepExp (brackets $ commas linkedLinks) cs p
+ppExp (ERepSeq cs p)           = ppRepExp (char ';') cs p
+ppExp (ERepSyncExtChoice a cs p) = do
+  pa <- ppExp a
+  ppRepExp (text "[+" <+> pa <+> text "+]") cs p
+ppExp (EList es)          = do
+  tes <- mapM ppExpParens es
+  return $ char '<' <+> commas tes <+> char '>'
+ppExp (EListComp es cs)   =
+  ppCompStmt cs $ \pcs -> do
+    pes <- mapM ppExpParens es
+    return $ char '<' <+> commas pes <+> char '|' <+> pcs <+> char '>'
+ppExp (EListFrom e)       = do
+  pe <- ppExpParens e
+  return $ char '<' <+> pe <+> text "..>"
+ppExp (EListFromComp e cs) =
+  ppCompStmt cs $ \pcs -> do
+    pe <- ppExpParens e
+    return $ char '<' <+> pe <+> text ".. |" <+> pcs <+> char '>'
+ppExp (EListFromTo e1 e2) = do
+  pe1 <- ppExpParens e1
+  pe2 <- ppExpParens e2
+  return $ char '<' <+> pe1 <+> text ".." <+> pe2 <+> char '>'
+ppExp (EListFromToComp e1 e2 cs) =
+  ppCompStmt cs $ \pcs -> do
+    pe1 <- ppExpParens e1
+    pe2 <- ppExpParens e2
+    return $ char '<' <+> pe1 <+> text ".." <+> pe2
+                      <+> char '|' <+> pcs <+> char '>'
+ppExp (EListConcat e1 e2) = ppBOpExp e1 (char '^') e2
+ppExp (EListLength e)     = do
+  pe <- ppExp e
+  return $ char '#' <+> pe
+ppExp (ETuple es)         = parens . commas <$> mapM ppExp es
+ppExp (ESet es)           = braces . commas <$> mapM ppExp es
+ppExp (ESetComp es cs)    = 
+  ppCompStmt cs $ \pcs -> do
+    pes <- mapM ppExp es
+    return $ braces $ commas pes <+> char '|' <+> pcs
+ppExp (ESetFrom e)        = do
+  pe <- ppExp e
+  return $ braces $ pe <+> text ".."
+ppExp (ESetFromComp e cs) =
+  ppCompStmt cs $ \pcs -> do
+    pe <- ppExp e
+    return $ braces $ pe <+> text ".. |" <+> pcs
+ppExp (ESetFromTo e1 e2)  = do
+  pe1 <- ppExp e1
+  pe2 <- ppExp e2
+  return $ braces $ pe1 <+> text ".." <+> pe2
+ppExp (ESetFromToComp e1 e2 cs) =
+  ppCompStmt cs $ \pcs -> do
+    pe1 <- ppExp e1
+    pe2 <- ppExp e2
+    return $ braces $ pe1 <+> text ".." <+> pe2 <+> char '|' <+> pcs
+ppExp ESetInt  = return $ text "Int"
+ppExp ESetBool = return $ text "Bool"
+ppExp (EEnumSet es)       = do
+  pes <- commas <$> mapM ppExp es
+  return $ text "{|" <+> pes <+> text "|}"
+ppExp (EEnumSetComp es cs) =
+  ppCompStmt cs $ \pcs -> do
+    pes <- commas <$> mapM ppExp es
+    return $ text "{|" <+> pes <+> char '|' <+> pcs <+> text "|}"
+ppExp (EMap es) = do
+  tes <- mapM ppMapPair es
+  return $ text "(|" <+> commas tes <+> text "|)"
+  where 
+    ppMapPair (e1, e2) = do te1 <- ppExpParens e1 
+                            te2 <- ppExpParens e2
+                            return $ te1 <+> text "=>" <+> te2
+
+
+-- parens around compound things only
+ppExpParens :: Exp -> PP Doc
+ppExpParens e@(EId _)                 = ppExp e
+ppExpParens e@(EConst _)              = ppExp e
+ppExpParens e@(EList _)               = ppExp e
+ppExpParens e@(EListComp _ _)         = ppExp e
+ppExpParens e@(EListFrom _)           = ppExp e
+ppExpParens e@(EListFromComp _ _)     = ppExp e
+ppExpParens e@(EListFromTo _ _)       = ppExp e
+ppExpParens e@(EListFromToComp _ _ _) = ppExp e
+ppExpParens e@(ETuple _)              = ppExp e
+ppExpParens e@(ESet _)                = ppExp e
+ppExpParens e@(ESetComp _ _)          = ppExp e
+ppExpParens e@(ESetFrom _)            = ppExp e
+ppExpParens e@(ESetFromComp _ _)      = ppExp e
+ppExpParens e@(ESetFromTo _ _)        = ppExp e
+ppExpParens e@(ESetFromToComp _ _ _)  = ppExp e
+ppExpParens e@(ESetInt)               = ppExp e
+ppExpParens e@(ESetBool)              = ppExp e
+ppExpParens e@(EEnumSet _)            = ppExp e
+ppExpParens e@(EEnumSetComp _ _)      = ppExp e
+ppExpParens e@(EMap _)                = ppExp e
+ppExpParens e = parens <$> ppExp e
+
+-- Abstract the common case of "binary" operators, which actually comes up much
+-- more than just the arithmetic ones.
+ppBOpExp :: Exp -> Doc -> Exp -> PP Doc
+ppBOpExp e1 pop e2 = do
+  pe1 <- ppExpParens e1
+  pe2 <- ppExpParens e2
+  return $ pe1 <+> pop <+> pe2
+
+-- Abstract the common case of "replicated" operators
+ppRepExp :: Doc -> [CompStmt] -> Exp -> PP Doc
+ppRepExp op stmts e = do
+  ppCompStmt stmts $ \pstmts -> do
+    pe <- ppExp e
+    return $ op <+> pstmts <+> char '@' <+> pe
+
+ppConst :: Const -> Doc
+ppConst CStop = text "STOP"
+ppConst CSkip = text "SKIP"
+ppConst (CInt n) = integer n
+ppConst (CChar c) = char '\'' <> char c <> char '\''
+ppConst (CBool b) = if b then text "True" else text "False"
+ppConst (CString s) = text $ show s -- XXX hack.  I think this escapes things that matter?
+ppConst CUnit = text "UnitVal"
+
+ppUOp :: UOp -> Doc
+ppUOp UNeg      = char '-'
+ppUOp UNot      = text "not"
+--ppUOp (Hide _) = error "Internal error: ppUOpApp called on hide"
+
+ppBinOp :: BinOp -> Doc
+ppBinOp BEq         = text "=="
+ppBinOp BLeq        = text "<="
+ppBinOp BLt         = char '<'
+ppBinOp BGeq        = text ">="
+ppBinOp BGt         = char '>'
+ppBinOp BAnd        = text "and"
+ppBinOp BOr         = text "or"
+ppBinOp BNeq        = text "!="
+ppBinOp BPlus       = char '+'
+ppBinOp BMinus      = char '-'
+ppBinOp BTimes      = char '*'
+ppBinOp BDiv        = char '\\'
+ppBinOp BMod        = char '%'
+
+------------------
+------------------ Top-level identifiers
+------------------
+
+topLevelIDs :: FDRMod -> [Id]
+topLevelIDs m = concatMap tlIDs $ topLevels m
+  where
+   tlIDs :: Definition -> [Id]
+   tlIDs (DFun nm _)      = [nm]
+   tlIDs (DVar pat _)     = patIDs pat
+   tlIDs (DAnnot _ _)     = []
+   tlIDs (DDataType nm cnstrs) = nm : map fst cnstrs
+   tlIDs (DSubType nm _)  = [nm]
+   tlIDs (DChan x _)      = x
+   tlIDs (DInclude _)     = []
+   tlIDs (DExternal f)    = [f]
+   tlIDs (DTransparent f) = [f]
+   tlIDs (DAssert _ _)    = []
+
+-- The IDs inside a pattern
+patIDs :: Pat -> [Id]
+patIDs (PId x)           = [x]
+patIDs (PConcat p1 p2)   = patIDs p1 ++ patIDs p2
+patIDs (PDot p1 p2)      = concatMap patIDs (p1:p2)
+patIDs (PDouble p1 p2)   = patIDs p1 ++ patIDs p2
+patIDs (PList ps)        = concatMap patIDs ps
+patIDs (PConst _)        = []
+patIDs PEmptySet         = []
+patIDs (PSingletonSet p) = patIDs p
+patIDs (PTuple ps)       = concatMap patIDs ps
+patIDs PWildCard         = []
+
+---- This scans a module and adds any top-level names to the monad, since they
+---- may be used mutually recursively.
+addTLGlobals :: FDRMod -> PP ()
+addTLGlobals m = mapM_ addGlobal $ topLevelIDs m
+
+-- The `PP a` arg here is the scope of these locals
+addTLLocals :: FDRMod -> PP a -> PP a
+addTLLocals m a = addLocals (topLevelIDs m) $ \_ -> a
+--------------
+--------------
+--------------
+
+genStyle :: Style
+genStyle = Style {mode = LeftMode, lineLength = 0, ribbonsPerLine = 0}
+
+preludeNames :: [Id]
+preludeNames = []
+
+prelude :: PPState
+prelude = foldl' addName emptyPPState preludeNames
+  where
+    addName :: PPState -> Id -> PPState
+    addName pps nm@(Fixed s) =
+      pps {ppIdMap    = M.insert nm s (ppIdMap pps),
+           ppUsedDocs = S.insert s (ppUsedDocs pps)}
+    addName pps nm@(Id (s,_)) =
+      pps {ppIdMap    = M.insert nm s (ppIdMap pps),
+           ppUsedDocs = S.insert s (ppUsedDocs pps),
+           ppWarnings = w : (ppWarnings pps)}
+      where
+        w = "Non-fixed id " ++ show nm ++ " in prelude,"
+
+-- | Pretty-prints an FDR3 module.
+-- Returns the pretty-printed module as a string, and a list of warnings.  The
+-- module string should be valid FDR3 input.  The warnings will mention any
+-- non-fixed identifiers that are used out of their scope.
+emitMod :: FDRMod -> (String,[String])
+emitMod m = let (d,ws) = runPP prelude $ ppFDRMod m in
+               (renderStyle genStyle d, ws)
+
+-- | Pretty-prints an FDR3 module.
+-- Returns two lists of strings.  The strings in the first list are the
+-- pretty-printed input modules, and should be valid input for FDR3.  The
+-- strings in the second list are warnings, and will mention any non-fixed
+-- identifiers used out of scope.  Globals with non-fixed identifiers in each
+-- input module are considered in scope for subsequent modules in the list.
+emitMods :: [FDRMod] -> ([String],[String])
+emitMods mds =
+  let (ds,ws) = runPP prelude $ mapM ppFDRMod mds in
+    (map (renderStyle genStyle) ds, ws)
diff --git a/Language/CSPM/Syntax.hs b/Language/CSPM/Syntax.hs
new file mode 100644
--- /dev/null
+++ b/Language/CSPM/Syntax.hs
@@ -0,0 +1,249 @@
+{- |
+   Module      :  Language.CSP.Syntax
+   Description :  Abstract syntax for CSP
+   Copyright   :  Draper Laboratories
+   
+   Abstract syntax of machine-reable CSP.  This is intended to correspond
+   with the input language of FDR3, though some features are likely missing.
+
+-}
+
+module Language.CSPM.Syntax where
+
+
+
+
+{- | 'Id' is our type for names. -}
+data Id  =
+  -- | the 'Id' constructor should be used for most identifiers, like variable
+  -- names.  It has two fields - a 'String' and an 'Int'.  Only the 'Int' is
+  -- used to check equality of names, the 'String' is just a hint for pretty
+  -- printing.  The pretty printer doesn't guarantee to use exactly this
+  -- name in the case where different 'Id's use the same string part.
+    Id    (String,Int)
+  -- | 'Fixed' is for identifiers where the name matters outside the scope of
+  -- what is currently being pretty printed (for example, to refer to the
+  -- standard library).  The pretty printer will always use exactly this
+  -- name, and the programmer must avoid conflicts to get sane CSPm.
+  | Fixed String        
+  deriving (Show)
+
+instance Eq Id where
+  (Id (_,i1)) == (Id (_,i2)) = i1 == i2
+  (Fixed s1)  == (Fixed s2)  = s1 == s2
+  _ == _                     = False
+  
+instance Ord Id where
+  compare (Id (_,i1)) (Id (_,i2)) = compare i1 i2
+  compare (Id _) (Fixed _)        = LT
+  compare (Fixed s1) (Fixed s2)   = compare s1 s2
+  compare (Fixed _)  (Id _)       = GT
+
+-- | A helper function which gets the string part of an identifier, useful
+-- for error messages
+namePart :: Id -> String
+namePart (Id (s,_)) = s
+namePart (Fixed s)  = s
+
+-- | Base types in FDR
+data Type = TEvent | TProc
+          | TChar | TBool | TInt | TUnit
+          | TList Type | TSet Type | TMap Type Type
+          | TData Id
+          | TRange Exp Exp
+            deriving (Eq, Show)
+
+-- | Toplevel FDR modules (this corresponds to a .csp file)
+data FDRMod = FDRMod { topLevels :: [Definition] }
+              deriving (Eq, Show)
+
+-- | Toplevel declarations in FDR
+data Definition = 
+    DVar Pat Exp
+  | DFun Id [([Pat],Exp)]
+  | DAnnot Id Type
+
+   -- | Somewhat unusually, the arguments to data constructors in CSPm datatype
+   -- declarations are actually expressions, not types.  In particular, the
+   -- arguments must always be a set, as in:
+   -- 
+   -- >   datatype Foo = F.{0..5}.{True,False}
+   -- 
+   -- FDR provides a little syntax sugar to help with common cases, in that
+   -- there are actually /expressions/ called @Int@ and @Bool@:
+   --
+   -- >     Int :: {Int}      Bool :: {Bool}
+   -- >     Int = {0..}       Bool = {True,False}
+  | DDataType Id [(Id,[Exp])]
+
+  | DSubType Id [(Id,[Exp])]
+  | DChan [Id] [Type]
+  | DInclude String
+  | DExternal Id
+  | DTransparent Id
+  | DAssert Assertion Model
+    deriving (Eq, Show)
+
+-- | The models that can be used in assertions.
+data Model
+  -- | Traces
+  = MT
+  -- | Failures
+  | MF
+  -- | Failures-divergences
+  | MFD
+  deriving (Eq,Show)
+
+-- | FDR assertions
+data Assertion = ARefines Exp Exp
+               | ADeadlockFree Exp
+               | ADivergenceFree Exp
+               | ADeterministic Exp
+               | AHasTrace Exp Exp
+  deriving (Eq,Show)
+
+-- | The types of fields one can use in a prefix.
+data CommField =
+  -- | .
+    CFPlain Exp
+  -- | ?
+  | CFInput Pat
+  -- | !
+  | CFOutput Exp
+  -- | $
+  | CFNDInput Pat 
+    deriving (Eq,Show)
+
+-- | Constants
+data Const = CStop | CSkip | CInt Integer | CChar Char | CUnit
+           | CBool Bool | CString String
+             deriving (Eq, Show)
+
+-- | Comprehension Statements
+data CompStmt =
+    CSGen Pat Exp  -- CSGen p e  ==   p <- e     (or    p : e)
+  | CSPred Exp
+  deriving (Eq,Show)
+
+-- | Patterns
+data Pat =
+    PId Id
+  | PConcat Pat Pat
+  | PDot Pat [Pat]
+  | PDouble Pat Pat
+  | PList [Pat]
+  | PConst Const
+  | PEmptySet
+  | PSingletonSet Pat
+  | PTuple [Pat]
+  | PWildCard
+  deriving (Eq,Show)
+
+-- | Expressions
+data Exp =
+  -- FP basics
+    EId Id
+  | ELambda [Pat] Exp
+  | EApp Exp [Exp]
+  | ELet [Definition] Exp
+  | EIfThenElse Exp Exp Exp
+  | EUOp UOp Exp
+  | EBinOp Exp BinOp Exp
+  | EConst Const
+  | EError String
+    
+  -- CSP-specific
+  | EDot Exp [Exp]
+
+  | EExtChoice Exp Exp
+  | EGuarded Exp Exp
+  | EHide Exp Exp
+  | EIntChoice Exp Exp
+  -- | In prefix we deviate a little from the strict grammar by taking an exp
+  -- and its dotted arguments rather than an arbitrary expression.  This
+  -- helps with pretty printing (and conceptually).
+  | EPrefix Exp [CommField] Exp  
+  | EProject Exp Exp  
+  | ERename Exp [(Exp,Exp)]
+
+  | EAlphaParallel Exp Exp Exp Exp
+  | EGenParallel Exp Exp Exp
+  | EInterleave Exp Exp
+
+  | EException Exp Exp Exp
+  | EInterrupt Exp Exp
+  | ESeq Exp Exp
+  | ELinkedParallel Exp [(Exp,Exp)] Exp 
+  | ETimeout Exp Exp
+  | ESyncExtChoice Exp Exp Exp
+  | ESyncInterrupt Exp Exp Exp
+
+  | ERepAlphaParallel [CompStmt] Exp Exp
+  | ERepExtChoice [CompStmt] Exp
+  | ERepGenParallel Exp [CompStmt] Exp
+  | ERepInterleave [CompStmt] Exp
+  | ERepIntChoice [CompStmt] Exp
+  | ERepLinkedParallel [(Exp,Exp)] [CompStmt] Exp
+  | ERepSeq [CompStmt] Exp
+  | ERepSyncExtChoice Exp [CompStmt] Exp
+
+  -- Lists
+  | EList [Exp]
+  | EListComp [Exp] [CompStmt]
+  | EListFrom Exp
+  | EListFromComp Exp [CompStmt]
+  | EListFromTo Exp Exp
+  | EListFromToComp Exp Exp [CompStmt]
+  | EListConcat Exp Exp
+  | EListLength Exp
+
+  -- Tuples
+  | ETuple [Exp]
+         
+  -- Sets
+  | ESet [Exp]
+  | ESetComp [Exp] [CompStmt]
+  | ESetFrom Exp
+  | ESetFromComp Exp [CompStmt]
+  | ESetFromTo Exp Exp
+  | ESetFromToComp Exp Exp [CompStmt]
+
+  -- Built-in sets.  In the official CSPm syntax, these are just IDs provided by
+  -- the standard library.  But for sanity, I'm making them explicit parts of
+  -- the syntax.
+  | ESetInt
+  | ESetBool
+
+  -- Enumerated Set
+  | EEnumSet [Exp]
+  | EEnumSetComp [Exp] [CompStmt]
+
+  --maps
+  | EMap [(Exp, Exp)]
+    deriving (Eq, Show)
+
+-- | Unary boolean and arithmetic operators
+data UOp = 
+    UNeg 
+  | UNot
+  deriving (Eq, Show)
+
+-- | Binary boolean and arithmetic operators
+data BinOp =
+
+    BEq
+  | BNeq
+  | BLeq
+  | BLt
+  | BGeq
+  | BGt
+
+  | BPlus
+  | BMinus
+  | BTimes
+  | BDiv
+  | BMod
+
+  | BAnd
+  | BOr
+  deriving (Eq, Show)
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/cspretty.cabal b/cspretty.cabal
new file mode 100644
--- /dev/null
+++ b/cspretty.cabal
@@ -0,0 +1,19 @@
+name:                cspretty
+version:             1.0
+synopsis:            AST and pretty printer for CSPm
+license:             BSD3
+license-file:        LICENSE
+author:              Draper Labs
+maintainer:          ccasinghino@draper.com
+category:            Language
+build-type:          Simple
+cabal-version:       >=1.10
+
+library
+  exposed-modules:     Language.CSPM.Syntax
+                       Language.CSPM.Pretty
+  build-depends:       base       >= 4.8 && < 4.9,
+                       pretty     >= 1.1,
+                       containers >= 0.5
+  default-language:    Haskell2010
+  ghc-options:         -Wall -O2