diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2012, Galois, 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 Jason Dagit nor the names of other
+      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 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/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/aterm-utils.cabal b/aterm-utils.cabal
new file mode 100644
--- /dev/null
+++ b/aterm-utils.cabal
@@ -0,0 +1,49 @@
+name:                aterm-utils
+version:             0.1.0.0
+synopsis:            Utility functions for working with aterms as generated by Minitermite
+-- description:         
+license:             BSD3
+license-file:        LICENSE
+author:              Jason Dagit
+maintainer:          dagit@galois.com
+copyright:           (c) 2012 Galois, Inc 
+category:            Language
+build-type:          Simple
+cabal-version:       >=1.8
+homepage:            https://github.com/GaloisInc/aterm-utils
+
+executable ppaterm
+  hs-source-dirs:    src
+  Main-is:           PPATerm.hs
+
+  Build-depends:       base < 5
+                     , aterm
+                     , aterm-utils
+                     , transformers
+                     , wl-pprint
+
+  ghc-options: -O2 -Wall
+  if impl(ghc >= 7.0.1)
+    ghc-prof-options: -rtsopts
+  ghc-prof-options: -prof -auto-all -caf-all
+
+library
+
+  exposed-modules:   ATerm.Utilities
+                   , ATerm.Matching
+                   , ATerm.Pretty
+
+  Build-depends:       base < 5
+                     , aterm
+                     , transformers
+                     , wl-pprint
+
+  hs-source-dirs:      src
+  ghc-options: -O2 -Wall
+  if impl(ghc >= 7.0.1)
+    ghc-prof-options: -rtsopts
+  ghc-prof-options: -prof -auto-all -caf-all
+
+source-repository head
+  type:     git
+  location: git://github.com/GaloisInc/aterm-utils.git
diff --git a/src/ATerm/Matching.hs b/src/ATerm/Matching.hs
new file mode 100644
--- /dev/null
+++ b/src/ATerm/Matching.hs
@@ -0,0 +1,153 @@
+{-# LANGUAGE PatternGuards #-}
+module ATerm.Matching
+( -- * Types
+  Binding(..)
+-- * Combinators
+, exactlyS
+, exactlyI
+, exactlyL
+, exactlyA
+, exactlyNamed
+, contains
+, containsL
+, containsA
+, containsChildren
+, bindT
+, bindL
+, bindI
+, bindS
+, bindA
+) where
+
+import ATerm.AbstractSyntax
+import qualified ATerm.Utilities as U
+import Control.Monad -- For MonadPlus
+
+-- | Binding type gives you back the parts of the ATerm that
+-- that match.
+data Binding = BoundTerm Int     -- ^ The index into the ATermTable of the matching ATerm
+             | BoundList [Int]   -- ^ The list of indexes into the ATermTable that match
+             | BoundInt  Integer -- ^ The matching Integer
+             | BoundStr  String  -- ^ The matching String
+             | BoundAppl Int     -- ^ The index into the ATermTable for the ShAAppl term
+  deriving (Eq, Read, Show, Ord)
+
+-- | Turns anything with an Eq instance into a
+-- matcher by using (==). No binding is generated.
+exactly :: (MonadPlus m, Eq a) => a -> a -> m ()
+exactly a b = guard (a == b) >> return ()
+
+-- * ATermMatcher Combinators
+
+---------------------------------------------------------------------
+-- ** Exact matchers, no binding generated when they match
+---------------------------------------------------------------------
+
+-- | Matches exactly the string 's' within the ATerm
+exactlyS :: MonadPlus m => String -> ATermTable -> m ()
+exactlyS s t = case getATerm t of
+  ShAAppl s' [] _ -> exactly s s'
+  _               -> mzero
+
+-- | Matches exactly the integer 'i' within the ATerm
+exactlyI :: MonadPlus m => Integer -> ATermTable -> m ()
+exactlyI i t = case getATerm t of
+  ShAInt i' _ -> exactly i i'
+  _           -> mzero
+
+-- | Matches exactly the list 'xs' within the ATerm
+exactlyL :: MonadPlus m => [ATermTable -> m a] -> ATermTable -> m [a]
+exactlyL ms t = case getATerm t of
+  ShAList ls _ -> do
+    _ <- guard (length ms == length ls)
+    sequence (zipWith (\m i -> m (getATermByIndex1 i t)) ms ls)
+  _ -> mzero
+
+-- | Matches the string exactly
+exactlyA :: MonadPlus m => String -> [ATermTable -> m a] -> ATermTable -> m [a]
+exactlyA s ms t = case getATerm t of
+  ShAAppl s' ls _ -> do
+    _ <- exactly s s'
+    _ <- guard (length ms == length ls)
+    sequence (zipWith (\m i -> U.app m t i) ms ls)
+  _ -> mzero
+
+-- | Looks for an Appl with name 's' and any children
+exactlyNamed :: MonadPlus m => String -> ATermTable -> m ()
+exactlyNamed s t = case getATerm t of
+  ShAAppl s' _ _ -> do
+    _ <- exactly s s'
+    return ()
+  _ -> mzero
+
+---------------------------------------------------------------------
+-- ** Partial matchers, ie., they just specify part of the structure
+---------------------------------------------------------------------
+
+containsChildren :: Monad m
+                 => m (ATermTable -> b) -> m Int -> ATermTable -> m b
+containsChildren ms is t = do
+  i <- is
+  m <- ms
+  return (m (getATermByIndex1 i t))
+
+-- | Matches a partial specification against the children. The
+-- matching is maximised so that if the pattern occurs more than
+-- once it is matched each time it appears.
+contains :: [ATermTable -> a] -> ATermTable -> [a]
+contains ms t = case getATerm t of
+  ShAAppl _ ls _ -> containsChildren ms ls t
+  ShAList   ls _ -> containsChildren ms ls t
+  _              -> mzero
+
+-- | Matches a partial specification of a sub aterm List. The
+-- matching is maximised so that if the pattern occurs more than
+-- once it is matched each time it appears.
+containsL :: [ATermTable -> a] -> ATermTable -> [a]
+containsL ms t = case getATerm t of
+  ShAList ls _ -> containsChildren ms ls t
+  _            -> mzero
+
+-- | Matches a partial specification of an Appl. The matching is
+-- maximised so that if the pattern occurs more than once it is match
+-- each time it appears.
+containsA :: String -> [ATermTable -> a] -> ATermTable -> [a]
+containsA s ams t = case getATerm t of
+  ShAAppl s' ls _ -> do
+    _ <- exactly s s'
+    containsChildren ams ls t
+  _               -> mzero
+
+---------------------------------------------------------------------
+-- ** Wildcard matchers, these create bindings when they match
+---------------------------------------------------------------------
+
+-- | Matches any ATerm and generates a binding to that term
+bindT :: MonadPlus m => ATermTable -> m Binding
+bindT t = return (BoundTerm (getTopIndex t))
+  
+-- | Matches any list and generates a binding to that list
+bindL :: MonadPlus m => ATermTable -> m Binding
+bindL t = case getATerm t of
+  ShAList ls _ -> return (BoundList ls)
+  _            -> mzero
+
+-- | Matches any integer and generates a binding to that integer
+bindI :: MonadPlus m => ATermTable -> m Binding
+bindI t = case getATerm t of
+  ShAInt i _ -> return (BoundInt i)
+  _          -> mzero
+
+-- | Matches any string and generates a binding to that string
+-- Strings have the form (Appl somestring [] []).
+-- Not to be confused with matching the the string part of an Appl.
+bindS :: MonadPlus m => ATermTable -> m Binding
+bindS t = case getATerm t of
+  ShAAppl s [] [] -> return (BoundStr s)
+  _               -> mzero
+
+-- | Matches any Appl and generates a binding to that Appl
+bindA :: MonadPlus m => ATermTable -> m Binding
+bindA t = case getATerm t of
+  ShAAppl _ _ _ -> return (BoundAppl (getTopIndex t))
+  _             -> mzero
diff --git a/src/ATerm/Pretty.hs b/src/ATerm/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/src/ATerm/Pretty.hs
@@ -0,0 +1,41 @@
+module ATerm.Pretty
+(
+  ppATerm
+)
+where
+
+import Text.PrettyPrint.Leijen
+import ATerm.AbstractSyntax
+
+ppATerm :: ATermTable -> Doc
+ppATerm t = case getATerm t of
+  ShAAppl s [] [] -> text s -- this will already have double quotes in this case
+  ShAAppl s is _  -> nestAppl t s is
+  ShAList   is _  -> nestList t is
+  ShAInt  i    _  -> integer i
+
+ppAList :: ATermTable -> [Int] -> [Doc]
+ppAList t is = map (\i -> ppATerm (getATermByIndex1 i t)) is
+
+nestList :: ATermTable -> [Int] -> Doc
+nestList t is = children ds
+  where
+  children []  = lbracket <> rbracket
+  children [d] = lbracket <> d <> rbracket
+  children _   =
+    lbracket                                                          <$>
+      indent 2 (align (cat (zipWith (<>) (empty : repeat comma) ds))) <$>
+    rbracket
+  ds = ppAList t is
+
+
+nestAppl :: ATermTable -> String -> [Int] -> Doc
+nestAppl t s is = children ds
+  where
+  children []  = text s <> lparen <> rparen
+  children [d] = text s <> lparen <> d <> rparen
+  children _   = text s <>
+    lparen                                                               <$>
+      indent 2 (align (cat (zipWith (<>) (text " " : repeat comma) ds))) <$>
+    (indent 1 rparen)
+  ds = ppAList t is
diff --git a/src/ATerm/Utilities.hs b/src/ATerm/Utilities.hs
new file mode 100644
--- /dev/null
+++ b/src/ATerm/Utilities.hs
@@ -0,0 +1,240 @@
+{-# LANGUAGE PatternGuards #-}
+-- | Functions for working with the ATerms that ROSE produces.
+module ATerm.Utilities
+( -- * Utility functions
+  app             -- (ATermTable -> a) -> ATermTable -> Int -> a
+, foldr           -- (ATermTable -> a -> a) -> a -> ATermTable -> a
+, foldl           -- (a -> ATermTable -> a) -> a -> ATermTable -> a
+, foldl'          -- (a -> ATermTable -> a) -> a -> ATermTable -> a
+, foldM           -- (a -> ATermTable -> m a) -> a -> ATermTable -> m a
+, mapM            -- (ATermTable -> m b) -> ATermTable -> m [b]
+, mapM_           -- (ATermTable -> m b) -> ATermTable -> m ()
+, map             -- (ATermTable -> a) -> ATermTable -> [a]
+, concatMap       -- (ATermTable -> [a]) -> ATermTable -> [a]
+-- * Check Monad
+, CheckM
+, appM            -- (ATermTable -> a) -> Int -> CheckM log state m a
+, currentTerm     -- CheckM log state m ATermTable
+, withCurrentTerm -- ATermTable -> CheckM log state m a -> CheckM log state m a
+, childrenM       -- CheckM log state m [Int]
+, satisfy         -- (ATermTable -> Bool) -> CheckM log st m a -> CheckM log st m (Maybe a)
+, inSubtree       -- CheckM log state m a -> CheckM log state m [[a]]
+, inSubtree_      -- CheckM log state m a -> CheckM log state m ()
+, everywhere      -- CheckM log state m a -> CheckM log state m [a]
+, everywhere_     -- CheckM log state m a -> CheckM log state m ()
+-- * Extractions
+, extractString   -- ATermTable -> Maybe String
+, extractInteger  -- ATermTable -> Maybe Integer
+, extractFileInfo -- ATermTable -> Maybe (String, Integer, Integer)
+, isNamed         -- String -> ATermTable -> Bool
+, showATerm       -- ATermTable -> String
+, children        -- ATermTable -> [Int]
+-- * Read and write
+, readATerm
+, writeSharedATerm
+-- * Misc
+, getATermFromTable
+) where
+
+import ATerm.ReadWrite
+import ATerm.SimpPretty
+import ATerm.AbstractSyntax
+
+import Control.Monad.Trans.RWS.Strict
+import Control.Monad ( liftM )
+import qualified Control.Monad as M
+import Data.Monoid
+
+import qualified Data.List as L ( foldl' )
+import Prelude hiding (foldr, foldl, map, mapM_, mapM, concatMap)
+import qualified Prelude as P
+
+---------------------------------------------------------------------
+-- Working with ATerms (eg., ATermTable)
+---------------------------------------------------------------------
+
+-- | Turns a normal function of ATermTable into a function that
+-- works on the hash value instead.
+app :: (ATermTable -> a) -> ATermTable -> Int -> a
+app f t i = f (getATermByIndex1 i t)
+
+-- | Standard foldr, but for ATermTables
+foldr :: (ATermTable -> a -> a) -> a -> ATermTable -> a
+foldr k z at = go at
+  where
+  go t = t `k` P.foldr k' z (children t)
+  k' i acc = app (foldr k acc) at i
+
+-- | Standard foldl, but for ATermTables
+foldl :: (a -> ATermTable -> a) -> a -> ATermTable -> a
+foldl k z at = go at
+  where
+  go t = k (P.foldl k' z (children t)) t
+  k' acc i = app (foldl k acc) at i
+
+-- | Standard foldl', but for ATermTables
+foldl' :: (a -> ATermTable -> a) -> a -> ATermTable -> a
+foldl' k z at = go at
+  where
+  go t = let z' = L.foldl' k' z (children t) in z' `seq` k z' t
+  k' acc i = app (foldl' k acc) at i
+
+-- | Standard foldM, but for ATermTables
+foldM :: (Monad m) => (a -> ATermTable -> m a) -> a -> ATermTable -> m a
+foldM k z at = go at
+  where
+  go t = k z t >>= \a -> M.foldM k' a (children t)
+  k' acc i = app (foldM k acc) at i
+
+-- | Standard mapM, but for ATermTables
+mapM :: (Monad m) => (ATermTable -> m b) -> ATermTable -> m [b]
+mapM f = foldM action []
+  where
+  action acc x = do
+    x' <- f x
+    return (x' : acc)
+
+-- | Standard mapM_, but for ATermTables
+mapM_ :: (Monad m) => (ATermTable -> m b) -> ATermTable -> m ()
+mapM_ f = foldM action ()
+  where
+  action _ x = do
+    _ <- f x
+    return ()
+
+-- | Standard map, but for ATermTables
+map :: (ATermTable -> a) -> ATermTable -> [a]
+map f at = foldr ((:) . f) [] at
+
+-- | Standard concatMap, but for ATermTables
+concatMap :: (ATermTable -> [a]) -> ATermTable -> [a]
+concatMap f at = foldr ((++) . f) [] at
+
+---------------------------------------------------------------------
+-- Checker Monad
+---------------------------------------------------------------------
+
+-- | The checker monad. For now the environment is the current ATerm, in the
+-- future we may also store the path from the root to the current ATerm, so use
+-- 'currentTerm' instead of ask to get the current ATerm
+type CheckM log state m a = RWST ATermTable log state m a
+
+-- | Like 'app' but lifts the result into the CheckM monad
+appM :: (Monoid log, Monad m) => (ATermTable -> a) -> Int -> CheckM log state m a
+appM f i = do
+  t <- currentTerm
+  return (f (getATermByIndex1 i t))
+
+-- | Use this instead of 'ask' so that we can refactor
+-- the environment later without impacting existing code.
+currentTerm :: (Monoid log, Monad m) => CheckM log state m ATermTable
+currentTerm = ask
+
+-- | Use this instead of 'local' so that we can refactor
+-- the environment later without impacting existing code.
+withCurrentTerm :: (Monoid log, Monad m)
+                => ATermTable -> CheckM log state m a -> CheckM log state m a
+withCurrentTerm t = local (const t)
+
+-- | Return the hashes of the current term's children into the monad
+childrenM :: (Monad m, Monoid log) => CheckM log state m [Int]
+childrenM = children `liftM` currentTerm
+
+-- | Use this when the current node must satisfy a specific property.
+-- Note: Using Maybe here is a bit of a hack. Refactor to support MonadPlus style guards?
+satisfy :: (Monad m, Monoid log)
+        => (ATermTable -> Bool) -> CheckM log st m a -> CheckM log st m (Maybe a)
+satisfy p m = do
+  t <- currentTerm
+  case p t of
+    True  -> Just `liftM` m
+    False -> return Nothing
+
+-- | Applies a traversal in a subtree of the current ATerm. Differs from 'everywhere'
+-- in that it does not apply the traversal to the current term (only its children and
+-- their children).
+inSubtree :: (Monad m, Monoid log) => CheckM log state m a -> CheckM log state m [[a]]
+inSubtree c = do
+  ks <- childrenM
+  at <- currentTerm
+  let kids = P.map (`getATermByIndex1` at) ks
+  P.mapM (`withCurrentTerm` (everywhere c)) kids
+
+-- Like 'inSubtree_' but throws away the result.
+inSubtree_ :: (Monad m, Monoid log) => CheckM log state m a -> CheckM log state m ()
+inSubtree_ c = do
+  ks <- childrenM
+  at <- currentTerm
+  let kids = P.map (`getATermByIndex1` at) ks
+  P.mapM_ (`withCurrentTerm` (everywhere c)) kids
+
+-- | Applies a traversal over the tree defined by the current node (including root node).
+everywhere :: (Monad m, Monoid log) => CheckM log state m a -> CheckM log state m [a]
+everywhere c = currentTerm >>= mapM (\at -> withCurrentTerm at c)
+
+-- | Like 'everywhere' but throws away the result.
+everywhere_ :: (Monad m, Monoid log) => CheckM log state m a -> CheckM log state m ()
+everywhere_ c = currentTerm >>= mapM_ (\at -> withCurrentTerm at c)
+
+{-
+-- Left here as a lesson: This doesn't seem to do the intended thing
+everywhere' :: (Monad m, Monoid log) => CheckM log state m a -> CheckM log state m [a]
+everywhere' c = currentTerm >>= mapM (const c)
+-}
+
+---------------------------------------------------------------------
+-- Turn ATerms into normal values, we make assumptions
+-- about the format that ROSE emits ATerms in.
+---------------------------------------------------------------------
+
+-- | Extracts the label of Application nodes
+extractString :: ATermTable -> Maybe String
+extractString at =
+  case getATerm at of
+  ShAAppl s _ _ -> Just s
+  _             -> Nothing
+
+-- | Extract the integer of Int nodes
+extractInteger :: ATermTable -> Maybe Integer
+extractInteger at =
+  case getATerm at of
+  ShAInt i _ -> Just i
+  _          -> Nothing
+
+-- | Extracts the filename, line number, and colunm number from
+-- file_info nodes.
+extractFileInfo :: ATermTable -> Maybe (String, Integer, Integer)
+extractFileInfo at =
+  case getATerm at of
+  ShAAppl s [fp,line,col] _
+    | s == "file_info"
+    , Just f <- extractString  (getATermByIndex1 fp   at)
+    , Just l <- extractInteger (getATermByIndex1 line at)
+    , Just c <- extractInteger (getATermByIndex1 col  at) -> Just (f,l,c)
+  _                                                       -> Nothing
+
+-- | Equality test on the label of an Application node
+isNamed :: String -> ATermTable -> Bool
+isNamed name t =
+  case getATerm t of
+  ShAAppl s _ _ -> s == name
+  _             -> False 
+
+-- | It's not acually pretty, but that's not our fault.
+showATerm :: ATermTable -> String
+showATerm = render . writeSharedATermSDoc
+
+-- | This pattern comes up in most traversals.  Simply return the stable names
+-- so we don't break sharing.
+children :: ATermTable -> [Int]
+children t =
+  case getATerm t of
+  ShAAppl _ l _ -> l
+  ShAList   l _ -> l
+  ShAInt  _   _ -> []
+
+---------------------------------------------------------------------
+-- Misc
+---------------------------------------------------------------------
+getATermFromTable :: ATermTable -> Int -> ATermTable
+getATermFromTable = flip getATermByIndex1
diff --git a/src/PPATerm.hs b/src/PPATerm.hs
new file mode 100644
--- /dev/null
+++ b/src/PPATerm.hs
@@ -0,0 +1,54 @@
+module Main where
+
+import System.Console.GetOpt
+import System.Environment ( getArgs )
+
+import Control.Applicative
+import Control.Monad ( when )
+import Data.List ( foldl', isSuffixOf )
+
+-- Project specific imports
+import ATerm.Pretty ( ppATerm )
+import qualified ATerm.Utilities as U
+
+---------------------------------------------------------------------
+-- Command Line options
+---------------------------------------------------------------------
+data Options = Options
+  { optSource :: Maybe FilePath -- ^ Nothing means read from stdin
+                                --   otherwise read this file
+  }
+  deriving (Read, Show, Eq)
+
+options :: [ OptDescr (Options -> Options) ]
+options =
+  [ Option "s" ["source"]
+      (ReqArg (\arg opt -> opt { optSource = Just arg }) "FILE")
+      "ATerm file to pretty print"
+  ]
+
+defaultOptions :: Options
+defaultOptions = Options { optSource = Nothing }
+
+header :: String
+header = unlines
+  [ "usage: [-s FILE]"
+  , "  If no file is given, input is taken from stdin"
+  ]
+
+---------------------------------------------------------------------
+-- Main program
+---------------------------------------------------------------------
+main :: IO ()
+main = do
+  args <- getArgs
+  let (flags, _, errors) = getOpt RequireOrder options args
+      opts = foldl' (.) id flags defaultOptions
+  when (not (null errors)) $ error (concat errors ++ usageInfo header options)
+  cs <- removeTrailingDot <$> maybe getContents readFile (optSource opts)
+  let aterms = U.readATerm cs
+  print (ppATerm aterms)
+  where
+  removeTrailingDot s
+    | length s >= 2 && ".\n" `isSuffixOf` s = init (init s)
+    | otherwise = s