diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,11 @@
+Copyright Vanessa McHale (c) 2018
+
+Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
+
+1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
+
+2. 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.
+
+3. Neither the name of the copyright holder 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 COPYRIGHT HOLDER 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/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,5 @@
+# language-ats
+
+## Installation
+
+## Configuration
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/bench/Bench.hs b/bench/Bench.hs
new file mode 100644
--- /dev/null
+++ b/bench/Bench.hs
@@ -0,0 +1,20 @@
+module Main where
+
+import           Criterion.Main
+import           Language.ATS
+
+main :: IO ()
+main =
+    defaultMain [ env envFiles $ \ ~(l, m) ->
+                  bgroup "format"
+                      [ bench "lexATS (large)" $ nf lexATS l
+                      , bench "parseATS . lexATS (large)" $ nf (parseATS . lexATS) l
+                      , bench "printATS . parseATS . lexATS (large)" $ nf (fmap printATS . parseATS . lexATS) l
+                      , bench "lexATS (medium)" $ nf lexATS m
+                      , bench "parseATS . lexATS (medium)" $ nf (parseATS . lexATS) m
+                      , bench "printATS . parseATS . lexATS (medium)" $ nf (fmap printATS . parseATS . lexATS) m
+                      ]
+                ]
+    where large = readFile "test/data/polyglot.dats"
+          medium = readFile "test/data/toml-parse.dats"
+          envFiles = (,) <$> large <*> medium
diff --git a/cabal.project.local b/cabal.project.local
new file mode 100644
--- /dev/null
+++ b/cabal.project.local
@@ -0,0 +1,12 @@
+constraints: language-ats +development
+with-compiler: ghc-8.2.2
+optimization: 2
+tests: True
+benchmarks: True
+documentation: True
+haddock-hoogle: True
+haddock-internal: True
+
+program-options
+  happy-options: -gcsa
+  alex-options: -g
diff --git a/language-ats.cabal b/language-ats.cabal
new file mode 100644
--- /dev/null
+++ b/language-ats.cabal
@@ -0,0 +1,81 @@
+name:                language-ats
+version:             0.1.0.0
+synopsis:            Parser and pretty-printer for ATS.
+description:         Parser and pretty-printer for [ATS](http://www.ats-lang.org/), written with Happy and Alex.
+homepage:            https://github.com/vmchale/language-ats#readme
+license:             BSD3
+license-file:        LICENSE
+author:              Vanessa McHale
+maintainer:          vamchale@gmail.com
+copyright:           Copyright: (c) 2018 Vanessa McHale
+category:            Language, Lexer, Parser, Pretty Printer
+build-type:          Simple
+extra-doc-files:     README.md
+extra-source-files:  stack.yaml
+                   , cabal.project.local
+cabal-version:       1.18
+
+Flag development {
+  Description: Enable `-Werror`
+  manual: True
+  default: False
+}
+
+library
+  hs-source-dirs:      src
+  exposed-modules:     Language.ATS
+  other-modules:       Language.ATS.Lexer
+                     , Language.ATS.Parser
+                     , Language.ATS.Types
+                     , Language.ATS.PrettyPrint
+  build-depends:       base >= 4.10 && < 5
+                     , array
+                     , lens
+                     , deepseq
+                     , ansi-wl-pprint >= 0.6.8
+                     , recursion-schemes
+                     , ansi-terminal
+                     , unordered-containers
+                     , composition-prelude
+  default-language:    Haskell2010
+  build-tools:         happy
+                     , alex
+  if flag(development)
+    ghc-options:       -Werror
+  if impl(ghc >= 8.0)
+    ghc-options:       -Wincomplete-uni-patterns -Wincomplete-record-updates -Wcompat
+  ghc-options:         -Wall
+
+test-suite language-ats-test
+  type:                exitcode-stdio-1.0
+  hs-source-dirs:      test
+  main-is:             Spec.hs
+  build-depends:       base
+                     , language-ats
+                     , hspec
+                     , hspec-dirstream
+                     , system-filepath
+  if flag(development)
+    ghc-options:       -Werror
+  if impl(ghc >= 8.0)
+    ghc-options:       -Wincomplete-uni-patterns -Wincomplete-record-updates -Wcompat
+  ghc-options:         -threaded -rtsopts -with-rtsopts=-N -Wall
+  default-language:    Haskell2010
+
+benchmark language-ats-bench
+  type:                exitcode-stdio-1.0
+  hs-source-dirs:      bench
+  main-is:             Bench.hs
+  build-depends:       base
+                     , language-ats
+                     , criterion
+  if flag(development)
+    ghc-options:       -Werror
+  if impl(ghc >= 8.0)
+    ghc-options:       -Wincomplete-uni-patterns -Wincomplete-record-updates -Wcompat
+  ghc-options:         -threaded -rtsopts -with-rtsopts=-N -O3 -Wall
+  default-language:    Haskell2010
+
+source-repository head
+  type:     git
+  location: https://github.com/vmchale/language-ats
diff --git a/src/Language/ATS.hs b/src/Language/ATS.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/ATS.hs
@@ -0,0 +1,53 @@
+-- | Main module for the library
+module Language.ATS ( -- * Functions for working with syntax
+                      lexATS
+                    , parseATS
+                    , printATS
+                    , printATSCustom
+                    , printATSFast
+                    -- * Library functions
+                    , getDependencies
+                    -- * Syntax Tree
+                    , ATS (..)
+                    , Declaration (..)
+                    , Expression (..)
+                    , Type (..)
+                    , Function (..)
+                    , Implementation (..)
+                    , Pattern (..)
+                    , Name (..)
+                    , UnOp (..)
+                    , BinOp (..)
+                    , DataPropLeaf (..)
+                    , Leaf (..)
+                    , Arg (..)
+                    , Addendum (..)
+                    , LambdaType (..)
+                    , Universal (..)
+                    , Existential (..)
+                    , PreFunction (..)
+                    , StaticExpression (..)
+                    , Paired (..)
+                    , Fixity (..)
+                    -- * Lexical types
+                    , Token (..)
+                    , AlexPosn (..)
+                    , Keyword (..)
+                    -- * Error types
+                    , ATSError
+                    -- * Lenses
+                    , leaves
+                    , constructorUniversals
+                    ) where
+
+import           Data.Maybe               (catMaybes)
+import           Language.ATS.Lexer
+import           Language.ATS.Parser
+import           Language.ATS.PrettyPrint
+import           Language.ATS.Types
+
+getDependencies :: ATS -> [FilePath]
+getDependencies (ATS ds) = catMaybes (g <$> ds)
+    where g (Staload _ s) = Just s
+          g (Include s)   = Just s
+          g _             = Nothing
diff --git a/src/Language/ATS/Lexer.x b/src/Language/ATS/Lexer.x
new file mode 100644
--- /dev/null
+++ b/src/Language/ATS/Lexer.x
@@ -0,0 +1,491 @@
+{
+
+    {-# OPTIONS_GHC -fno-warn-unused-matches -fno-warn-incomplete-uni-patterns #-}
+    {-# LANGUAGE DeriveGeneric #-}
+    {-# LANGUAGE DeriveAnyClass #-}
+    {-# LANGUAGE DeriveDataTypeable #-}
+    {-# LANGUAGE StandaloneDeriving #-}
+    {-# LANGUAGE OverloadedStrings #-}
+
+    -- | Module exporting the lexer itself as well as several data types for
+    -- working with tokens.
+    module Language.ATS.Lexer ( AlexPosn (..)
+                              , Token (..)
+                              , Keyword (..)
+                              , Addendum (..)
+                              , lexATS
+                              , token_posn
+                              , to_string
+                              , get_addendum
+                              ) where
+
+import Data.Data (Typeable, Data)
+import Data.Char (toUpper, toLower)
+import Control.Lens (over, _head)
+import Control.DeepSeq (NFData)
+import GHC.Generics (Generic)
+import Text.PrettyPrint.ANSI.Leijen hiding (line, column, (<$>))
+
+}
+
+%wrapper "posn"
+
+-- Digits
+$digit = 0-9
+$octal = 0-7
+
+-- Characters
+$special = [\+\-\&\|\[\]\{\}\(\)\_\=\!\%\^\$\@\;\~\,\.\\\#]
+$alpha = [a-zA-Z]
+$terminal = $printable # $white
+$esc_char = \27
+@escape_ch = \\ ([nt\'\\] | $octal+)
+@escape_str = \\ ([nt\"\\] | $octal+)
+@char = ($terminal # [\\\']) | " " | @escape_ch | $esc_char
+@char_lit = \' @char \'
+
+$br = [\<\>]
+
+-- Boolean literals
+@bool = (true | false)
+
+-- Integer
+@integer = $digit+
+@time_lit = $digit+ u
+
+-- Floats
+@decimals = $digit+
+@float = @decimals \. @decimals
+
+-- Strings
+@string = \" ($printable # [\"\\] | @escape_str | $esc_char | \n)* \"
+
+-- Identifiers
+@identifier = ($alpha | _) ($alpha | $digit | _ | ! | ' | \$)*
+
+-- Multi-line comments
+@not_close_paren = (\*+ [^\)] | [^\*] \))
+@paren_comment = \(\* ([^\)\*] | @not_close_paren | \n)* \*\)
+@not_close_slash = (\*+ [^\/] | [^\*] \/)
+@slash_comment = \/\* ([^\/\*] | @not_close_slash | \n)* \*\/
+@block_comment = @paren_comment | @slash_comment
+
+@if_block = "#if" ([^\#] | "#then" | "#print" | \n)+ "#endif" .*
+
+-- FIXME this is a disaster lol
+@ref_call = ($alpha | $digit | "(" | ")" | _ | (","))+ ">"
+
+@not_close_c = \% [^\}]
+@c_block = \%\{ ("#" | "$" | "^" | "") ([^\%] | @not_close_c | \n)* \%\}
+
+@inner_signature = ("!wrt" | "!exn" | "!exnwrt" | "0" | "1" | "!all" | "!laz" | "lin" | "fun" | "clo" | "cloptr" | "cloref" | "!ntm" | "!ref" | "prf" | "fe" | @block_comment)
+@inner_signature_mult = (@inner_signature (("," | "") @inner_signature)*) | ""
+
+@lambda = "=>" | "=>>" | "=<" @inner_signature_mult ">"
+@signature = ":<" @inner_signature_mult ">" | ":"
+@func_type = "->" | "-<" @inner_signature_mult ">"
+
+@at_brace = \@ ($white | @block_comment)* \{
+
+@operator = "**" | "+" | "-" | "*" | "/" | ".." | "!=" | ">=" | "<=" | "==" | "=" | "~" | "%" | "&&" | "||" | ":=" | ".<" | ">." | "<" | ">" | ">>" | "?" | "?!" | "#[" -- TODO context so tilde doesn't follow
+
+@double_parens = "(" @block_comment ")" | "()"
+@double_braces = "{" @block_comment "}" | "{}"
+@double_brackets = "<" @block_comment ">" | "<>"
+
+@view = v | view
+
+@fixity_decl = "infixr" | "infixl" | "prefix" | "postfix"
+
+tokens :-
+
+    $white+                  ;
+    ^ @block_comment         { tok (\p s -> CommentLex p s) }
+    ^ "//".*                 { tok (\p s -> CommentLex p s) }
+    "//".*                   ;
+    @block_comment           ;
+    "#define".*              { tok (\p s -> MacroBlock p s) }      
+    @if_block                { tok (\p s -> MacroBlock p s) }      
+    @c_block                 { tok (\p s -> CBlockLex p s) }
+    fun                      { tok (\p s -> Keyword p KwFun) }
+    fn                       { tok (\p s -> Keyword p KwFn) }
+    fnx                      { tok (\p s -> Keyword p KwFnx) }
+    and                      { tok (\p s -> Keyword p KwAnd) }
+    prval                    { tok (\p s -> Keyword p KwPrval) }
+    prfn                     { tok (\p s -> Keyword p KwPrfn) }
+    prfun                    { tok (\p s -> Keyword p KwPrfun) }
+    datatype                 { tok (\p s -> Keyword p KwDatatype) }
+    data @view type          { tok (\p s -> Keyword p KwDatavtype) }
+    dataview                 { tok (\p s -> Keyword p KwDataview) }
+    dataprop                 { tok (\p s -> Keyword p KwDataprop) }
+    assume                   { tok (\p s -> Keyword p KwAssume) }
+    typedef                  { tok (\p s -> Keyword p KwTypedef) }
+    @view typedef            { tok (\p s -> Keyword p KwVtypedef) }
+    absprop                  { tok (\p s -> Keyword p KwAbsprop) }
+    llam                     { tok (\p s -> Keyword p KwLinearLambda) }
+    lam                      { tok (\p s -> Keyword p KwLambda) }
+    staload                  { tok (\p s -> Keyword p KwStaload) }
+    let                      { tok (\p s -> Keyword p KwLet) }
+    in                       { tok (\p s -> Keyword p KwIn) }
+    end                      { tok (\p s -> Keyword p KwEnd) }
+    case"+"                  { tok (\p s -> Keyword p (KwCase Plus)) }
+    case"-"                  { tok (\p s -> Keyword p (KwCase Minus)) }
+    case                     { tok (\p s -> Keyword p (KwCase None)) }
+    castfn                   { tok (\p s -> Keyword p KwCastfn) }
+    val"+"                   { tok (\p s -> Keyword p (KwVal Plus)) } -- TODO also val@ ?
+    val"-"                   { tok (\p s -> Keyword p (KwVal Minus)) } 
+    val                      { tok (\p s -> Keyword p (KwVal None)) }
+    var                      { tok (\p s -> Keyword p KwVar) }
+    int                      { tok (\p s -> Keyword p KwInt) }
+    if                       { tok (\p s -> Keyword p KwIf) }
+    sif                      { tok (\p s -> Keyword p KwSif) }
+    then                     { tok (\p s -> Keyword p KwThen) }
+    else                     { tok (\p s -> Keyword p KwElse) }
+    string                   { tok (\p s -> Keyword p KwString) }
+    bool                     { tok (\p s -> Keyword p KwBool) }
+    void                     { tok (\p s -> Keyword p KwVoid) }
+    nat                      { tok (\p s -> Keyword p KwNat) }
+    implement                { tok (\p s -> Keyword p KwImplement) }
+    implmnt                  { tok (\p s -> Keyword p KwImplement) }
+    primplmnt                { tok (\p s -> Keyword p KwProofImplement) }
+    primplement              { tok (\p s -> Keyword p KwProofImplement) }
+    abst"@"ype               { tok (\p s -> Keyword p (KwAbst0p None)) }
+    abst"@ype+"              { tok (\p s -> Keyword p (KwAbst0p Plus)) }
+    abst"@type-"             { tok (\p s -> Keyword p (KwAbst0p Minus)) }
+    abs@view"t@ype"          { tok (\p s -> Keyword p (KwAbsvt0p None)) }
+    t"@"ype"+"               { tok (\p s -> Keyword p (KwT0p Plus)) }
+    t"@"ype"-"               { tok (\p s -> Keyword p (KwT0p Minus)) }
+    t"@"ype                  { tok (\p s -> Keyword p (KwT0p None)) }
+    @view"t@ype+"            { tok (\p s -> Keyword p (KwVt0p Plus)) }
+    @view"t@ype-"            { tok (\p s -> Keyword p (KwVt0p Minus)) }
+    @view"t@ype"             { tok (\p s -> Keyword p (KwVt0p None)) }
+    abstype                  { tok (\p s -> Keyword p KwAbstype) }
+    abs @view type           { tok (\p s -> Keyword p KwAbsvtype) }
+    absview                  { tok (\p s -> Keyword p KwAbsview) }
+    view                     { tok (\p s -> Keyword p (KwView None)) }
+    view"+"                  { tok (\p s -> Keyword p (KwView Plus)) }
+    view"-"                  { tok (\p s -> Keyword p (KwView Minus)) }
+    viewdef                  { tok (\p s -> Keyword p KwViewdef) }
+    "#"include               { tok (\p s -> Keyword p KwInclude) }
+    when                     { tok (\p s -> Keyword p KwWhen) }
+    of                       { tok (\p s -> Keyword p KwOf) }
+    stadef                   { tok (\p s -> Keyword p KwStadef) }
+    stacst                   { tok (\p s -> Keyword p KwStacst) }
+    local                    { tok (\p s -> Keyword p KwLocal) }
+    praxi                    { tok (\p s -> Keyword p KwPraxi) }
+    while                    { tok (\p s -> Keyword p KwWhile) }
+    where                    { tok (\p s -> Keyword p KwWhere) }
+    begin                    { tok (\p s -> Keyword p KwBegin) }
+    overload                 { tok (\p s -> Keyword p KwOverload) }
+    with                     { tok (\p s -> Keyword p KwWith) }
+    char                     { tok (\p s -> Keyword p KwChar) }
+    extern                   { tok (\p s -> Keyword p KwExtern) }
+    sortdef                  { tok (\p s -> Keyword p KwSortdef) }
+    propdef                  { tok (\p s -> Keyword p KwPropdef) }
+    tkindef                  { tok (\p s -> Keyword p KwTKind) }
+    typekindef               { tok (\p s -> Keyword p KwTKind) }
+    "$raise"                 { tok (\p s -> Keyword p KwRaise) }
+    mod                      { tok (\p s -> Keyword p KwMod) }
+    "println!"               { tok (\p s -> Identifier p s) }
+    "prerrln!"               { tok (\p s -> Identifier p s) }
+    "fix@"                   { tok (\p s -> Keyword p KwFixAt) }
+    "lam@"                   { tok (\p s -> Keyword p KwLambdaAt) }
+    "addr"                   { tok (\p s -> Keyword p KwAddr) }
+    "addr@"                  { tok (\p s -> Keyword p KwAddrAt) }
+    "view@"                  { tok (\p s -> Keyword p KwViewAt) }
+    sta                      { tok (\p s -> Keyword p KwSta) }
+    symintr                  { tok (\p s -> Keyword p KwSymintr) }
+    absview                  { tok (\p s -> Keyword p KwAbsview) }
+    "$list"                  { tok (\p s -> Keyword p (KwListLit "")) }
+    "$list_vt"               { tok (\p s -> Keyword p (KwListLit "_vt")) }
+    "fold@"                  { tok (\p s -> IdentifierSpace p s) }
+    "free@"                  { tok (\p s -> Identifier p s) }
+    @fixity_decl             { tok (\p s -> FixityTok p s) }
+    @double_parens           { tok (\p s -> DoubleParenTok p) }
+    @double_braces           { tok (\p s -> DoubleBracesTok p) }
+    @double_brackets         { tok (\p s -> DoubleBracketTok p) }
+    @char_lit                { tok (\p s -> CharTok p (toChar s)) }
+    @lambda                  { tok (\p s -> Arrow p s) }
+    @func_type               { tok (\p s -> FuncType p s) }
+    @bool                    { tok (\p s -> BoolTok p (read (over _head toUpper s)))}
+    @time_lit                { tok (\p s -> TimeTok p s) }
+    @integer                 { tok (\p s -> IntTok p (read s)) } -- FIXME shouldn't fail silenty on overflow
+    @float                   { tok (\p s -> FloatTok p (read s)) }
+    $br / @ref_call          { tok (\p s -> SpecialBracket p) }
+    @at_brace                { tok (\p s -> Operator p "@{") } -- FIXME this is kinda sloppy
+    @operator                { tok (\p s -> Operator p s) }
+    @signature               { tok (\p s -> SignatureTok p (tail s)) }
+    $special                 { tok (\p s -> Special p s) }
+    "effmask_all"            { tok (\p s -> Identifier p s) }
+    "effmask_wrt"            { tok (\p s -> Identifier p s) }
+    "extype"                 { tok (\p s -> Identifier p s) }
+    @identifier / " "        { tok (\p s -> IdentifierSpace p s) }
+    @identifier              { tok (\p s -> Identifier p s) }
+    @string                  { tok (\p s -> StringTok p s) }
+
+{
+
+deriving instance Generic AlexPosn
+deriving instance NFData AlexPosn
+deriving instance Data AlexPosn
+deriving instance Typeable AlexPosn
+
+tok f p s = f p s
+
+-- | Determines the default behavior for incomplete pattern matches
+data Addendum = None
+              | Plus
+              | Minus
+              deriving (Eq, Show, Generic, NFData, Data, Typeable)
+
+get_addendum (Keyword _ (KwVal a)) = a
+get_addendum _ = None
+
+data Keyword = KwFun
+             | KwFnx
+             | KwAnd
+             | KwDatatype
+             | KwDatavtype
+             | KwAssume
+             | KwTypedef
+             | KwVtypedef
+             | KwStaload
+             | KwLet
+             | KwIn
+             | KwLocal
+             | KwEnd
+             | KwImplement
+             | KwCase Addendum
+             | KwIf
+             | KwSif
+             | KwThen
+             | KwElse
+             | KwString
+             | KwBool
+             | KwInt
+             | KwVoid
+             | KwNat
+             | KwVal Addendum
+             | KwVar
+             | KwLambda
+             | KwLinearLambda
+             | KwInclude
+             | KwWhen
+             | KwOf
+             | KwAbsprop
+             | KwPrval
+             | KwStadef
+             | KwPraxi
+             | KwWhile
+             | KwWhere
+             | KwBegin
+             | KwOverload
+             | KwWith
+             | KwChar
+             | KwDataview
+             | KwDataprop
+             | KwView Addendum
+             | KwAbstype
+             | KwType
+             | KwAbst0p Addendum
+             | KwAbsvt0p Addendum
+             | KwT0p Addendum
+             | KwVt0p Addendum
+             | KwPrfun
+             | KwPrfn
+             | KwCastfn
+             | KwExtern
+             | KwAbsvtype
+             | KwProofImplement
+             | KwSortdef
+             | KwPropdef
+             | KwRaise
+             | KwTKind
+             | KwMod
+             | KwFixAt
+             | KwLambdaAt
+             | KwAddrAt
+             | KwAddr
+             | KwSta
+             | KwViewAt
+             | KwViewdef
+             | KwSymintr
+             | KwAbsview
+             | KwFn
+             | KwInfix
+             | KwInfixr
+             | KwInfixl
+             | KwStacst
+             | KwListLit String
+             deriving (Eq, Show, Generic, NFData)
+
+data Token = Identifier AlexPosn String
+           | Keyword AlexPosn Keyword
+           | BoolTok AlexPosn Bool
+           | IntTok AlexPosn Int
+           | FloatTok AlexPosn Float
+           | CharTok AlexPosn Char
+           | StringTok AlexPosn String
+           | Special AlexPosn String
+           | CBlockLex AlexPosn String
+           | IdentifierSpace AlexPosn String
+           | Operator AlexPosn String
+           | Arrow AlexPosn String
+           | FuncType AlexPosn String
+           | CommentLex AlexPosn String
+           | MacroBlock AlexPosn String
+           | TimeTok AlexPosn String
+           | SignatureTok AlexPosn String
+           | DoubleParenTok AlexPosn
+           | DoubleBracesTok AlexPosn
+           | DoubleBracketTok AlexPosn
+           | SpecialBracket AlexPosn
+           | FixityTok AlexPosn String
+           deriving (Eq, Show, Generic, NFData)
+
+instance Pretty Addendum where
+    pretty Plus = "+"
+    pretty Minus = "-"
+    pretty None = ""
+
+instance Pretty Keyword where
+    pretty KwFun = "fun"
+    pretty KwAnd = "and"
+    pretty KwDatatype = "datatype"
+    pretty KwDatavtype = "datavtype" -- FIXME this wrongly squashes dataviewtype
+    pretty KwFnx = "fnx"
+    pretty KwAssume = "assume"
+    pretty KwTypedef = "typedef"
+    pretty KwVtypedef = "vtypedef"
+    pretty KwStaload = "stload"
+    pretty KwLet = "let"
+    pretty KwWhere = "where"
+    pretty KwLocal = "local"
+    pretty KwEnd = "end"
+    pretty KwBegin = "begin"
+    pretty KwIn = "in"
+    pretty KwImplement = "implement"
+    pretty (KwCase c) = "case" <> pretty c
+    pretty KwIf = "if"
+    pretty KwSif = "sif"
+    pretty KwThen = "then"
+    pretty KwElse = "else"
+    pretty KwString = "string"
+    pretty KwBool = "bool"
+    pretty KwInt = "int"
+    pretty KwVoid = "void"
+    pretty KwNat = "nat"
+    pretty (KwVal c) = "val" <> pretty c
+    pretty KwVar = "var"
+    pretty KwLambda = "lam"
+    pretty KwLinearLambda = "llam"
+    pretty KwInclude = "include"
+    pretty KwWhen = "when"
+    pretty KwOf = "of"
+    pretty KwAbsprop = "absprop"
+    pretty KwPrval = "prval"
+    pretty KwStadef = "stadef"
+    pretty KwPraxi = "praxi"
+    pretty KwWhile = "while"
+    pretty KwOverload = "overload"
+    pretty KwWith = "with"
+    pretty KwChar = "char"
+    pretty KwDataview = "dataview"
+    pretty KwDataprop = "dataprop"
+    pretty (KwView c) = "view" <> pretty c
+    pretty KwAbstype = "abstype"
+    pretty KwAbsvtype = "absvtype"
+    pretty KwType = "type"
+    pretty (KwAbst0p c) = "abst@ype" <> pretty c
+    pretty (KwAbsvt0p c) = "absvt@ype" <> pretty c
+    pretty (KwT0p c) = "t@ype" <> pretty c
+    pretty (KwVt0p c) = "vt@ype" <> pretty c
+    pretty KwPrfun = "prfun"
+    pretty KwPrfn = "prfn"
+    pretty KwCastfn = "castfn"
+    pretty KwExtern = "extern"
+    pretty KwRaise = "$raise"
+    pretty KwProofImplement = "primplmnt"
+    pretty KwSortdef = "sortdef"
+    pretty KwPropdef = "propdef"
+    pretty KwTKind = "tkind"
+    pretty KwMod = "mod"
+    pretty KwFixAt = "fix@"
+    pretty KwLambdaAt = "lam@"
+    pretty KwAddrAt = "addr@"
+    pretty KwAddr = "addr"
+    pretty KwSta = "sta"
+    pretty KwStacst = "stacst"
+    pretty KwViewAt = "view@"
+    pretty KwViewdef = "viewdef"
+    pretty KwSymintr = "symintr"
+    pretty KwAbsview = "absview"
+    pretty KwFn = "fn"
+    pretty KwInfix = "infix"
+    pretty KwInfixr = "infixr"
+    pretty KwInfixl = "infixl"
+    pretty (KwListLit s) = "list" <> string s
+
+instance Pretty Token where
+    pretty (Identifier _ s) = text s
+    pretty (IdentifierSpace _ s) = text s
+    pretty (Keyword _ kw) = pretty kw
+    pretty (BoolTok _ b) = text $ over _head toLower (show b)
+    pretty (IntTok _ i) = pretty i
+    pretty (FloatTok _ x) = pretty x
+    pretty (CharTok _ c) = squotes (pretty c)
+    pretty (StringTok _ s) = dquotes (text s)
+    pretty (Special _ s) = text s
+    pretty CBlockLex{} = "%{"
+    pretty (Arrow _ s) = text s
+    pretty (CommentLex _ s) = text $ take 2 s
+    pretty (FuncType _ s) = text s
+    pretty (TimeTok _ s) = text s
+    pretty (SignatureTok _ s) = ":" <> text s
+    pretty (Operator _ s) = text s
+    pretty (MacroBlock _ s) = "#"
+    pretty DoubleParenTok{} = "()"
+    pretty DoubleBracesTok{} = "{}"
+    pretty DoubleBracketTok{} = "<>"
+    pretty SpecialBracket{} = "<"
+    pretty (FixityTok _ s) = text s
+
+to_string (CommentLex _ s) = s
+to_string (Identifier _ s) = s
+to_string (IdentifierSpace _ s) = s
+to_string _ = mempty
+
+token_posn (Identifier p _) = p
+token_posn (IdentifierSpace p _) = p
+token_posn (Keyword p _) = p
+token_posn (BoolTok p _) = p
+token_posn (IntTok p _) = p
+token_posn (FloatTok p _) = p
+token_posn (StringTok p _) = p
+token_posn (Special p _) = p
+token_posn (CBlockLex p _) = p
+token_posn (Operator p _) = p
+token_posn (Arrow p _) = p
+token_posn (FuncType p _) = p
+token_posn (CharTok p _) = p
+token_posn (CommentLex p _) = p
+token_posn (MacroBlock p _) = p
+token_posn (TimeTok p _) = p
+token_posn (SignatureTok p _) = p
+token_posn (DoubleParenTok p) = p
+token_posn (DoubleBracesTok p) = p
+token_posn (DoubleBracketTok p) = p
+token_posn (SpecialBracket p) = p
+token_posn (FixityTok p _) = p
+
+toChar :: String -> Char
+toChar "'\\n'" = '\n'
+toChar "'\\t'" = '\t'
+toChar "'\\\\'" = '\\'
+toChar x = x !! 1
+
+-- | This function turns a string into a stream of tokens for the parser.
+lexATS :: String -> [Token]
+lexATS = alexScanTokens
+
+}
diff --git a/src/Language/ATS/Parser.y b/src/Language/ATS/Parser.y
new file mode 100644
--- /dev/null
+++ b/src/Language/ATS/Parser.y
@@ -0,0 +1,697 @@
+{
+    {-# LANGUAGE OverloadedStrings #-}
+    {-# LANGUAGE DeriveGeneric     #-}
+    {-# LANGUAGE DeriveAnyClass    #-}
+    {-# LANGUAGE FlexibleContexts  #-}
+
+    -- | This module contains the parser.
+    module Language.ATS.Parser ( parseATS
+                               , ATSError
+                               ) where
+
+import Language.ATS.Types
+import Language.ATS.Lexer ( Token (..)
+                          , AlexPosn (..)
+                          , Keyword (..)
+                          , Addendum (..)
+                          , token_posn
+                          , to_string
+                          , get_addendum
+                          )
+
+import Data.Char (toLower)
+import Control.DeepSeq (NFData)
+import Control.Lens (over, _head)
+import GHC.Generics (Generic)
+import Prelude
+import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
+
+}
+
+%name parseATS
+%tokentype { Token }
+%error { parseError }
+%monad { Either (ATSError String) } { (>>=) } { pure }
+
+%token
+    fun { Keyword $$ KwFun }
+    fn { Keyword $$ KwFn }
+    castfn { Keyword $$ KwCastfn }
+    prfun { Keyword $$ KwPrfun }
+    prfn { Keyword $$ KwPrfn }
+    fnx { Keyword $$ KwFnx }
+    and { Keyword $$ KwAnd }
+    lambda { Keyword $$ KwLambda }
+    llambda { Keyword $$ KwLinearLambda }
+    if { Keyword $$ KwIf }
+    sif { Keyword $$ KwSif }
+    stadef { Keyword $$ KwStadef }
+    val { $$@(Keyword _ (KwVal _)) }
+    prval { Keyword $$ KwPrval }
+    var { Keyword $$ KwVar }
+    then { Keyword $$ KwThen }
+    let { Keyword $$ KwLet }
+    typedef { Keyword $$ KwTypedef }
+    vtypedef { Keyword $$ KwVtypedef }
+    absview { Keyword $$ KwAbsview }
+    absvtype { Keyword $$ KwAbsvtype }
+    abstype { Keyword $$ KwAbstype }
+    abst0p { Keyword $$ (KwAbst0p None) }
+    absvt0p { Keyword $$ (KwAbsvt0p None) }
+    viewdef { Keyword $$ KwViewdef }
+    in { Keyword $$ KwIn }
+    end { Keyword $$ KwEnd }
+    stringType { Keyword $$ KwString }
+    charType { Keyword $$ KwChar }
+    voidType { Keyword $$ KwVoid }
+    implement { Keyword $$ KwImplement }
+    primplmnt { Keyword $$ KwProofImplement }
+    else { Keyword $$ KwElse }
+    bool { Keyword $$ KwBool }
+    int { Keyword $$ KwInt }
+    nat { Keyword $$ KwNat }
+    addr { Keyword $$ KwAddr }
+    when { Keyword $$ KwWhen }
+    begin { Keyword $$ KwBegin }
+    case { Keyword _ (KwCase $$) }
+    datatype { Keyword $$ KwDatatype }
+    datavtype { Keyword $$ KwDatavtype }
+    while { Keyword $$ KwWhile }
+    of { Keyword $$ KwOf }
+    include { Keyword $$ KwInclude }
+    staload { Keyword $$ KwStaload }
+    overload { Keyword $$ KwOverload }
+    with { Keyword $$ KwWith }
+    dataprop { Keyword $$ KwDataprop }
+    praxi { Keyword $$ KwPraxi }
+    extern { Keyword $$ KwExtern }
+    t0pPlain { Keyword $$ (KwT0p None) }
+    t0pCo { Keyword $$ (KwT0p Plus) }
+    vt0pCo { Keyword $$ (KwVt0p Plus) }
+    vt0pPlain { Keyword $$ (KwVt0p None) }
+    where { Keyword $$ KwWhere }
+    absprop { Keyword $$ KwAbsprop }
+    sortdef { Keyword $$ KwSortdef }
+    local { Keyword $$ KwLocal }
+    view { Keyword $$ (KwView None) }
+    viewPlusMinus { Keyword _ (KwView $$) }
+    raise { Keyword $$ KwRaise }
+    tkindef { Keyword $$ KwTKind }
+    assume { Keyword $$ KwAssume }
+    addrAt { Keyword $$ KwAddrAt }
+    viewAt { Keyword $$ KwViewAt }
+    symintr { Keyword $$ KwSymintr }
+    stacst { Keyword $$ KwStacst }
+    propdef { Keyword $$ KwPropdef }
+    list { Keyword $$ (KwListLit "") }
+    list_vt { Keyword $$ (KwListLit "_vt") }
+    boolLit { BoolTok _ $$ }
+    timeLit { TimeTok _ $$ }
+    intLit { IntTok _ $$ }
+    floatLit { FloatTok _ $$ }
+    effmaskWrt { Identifier $$ "effmask_wrt" }
+    effmaskAll { Identifier $$ "effmask_all" }
+    extype { Identifier $$ "extype" }
+    extfcall { Identifier $$ "extfcall" }
+    ldelay { Identifier $$ "ldelay" }
+    listVT { Identifier $$ "list_vt" }
+    foldAt { Identifier $$ "fold@" }
+    identifier { $$@Identifier{} }
+    identifierSpace { $$@IdentifierSpace{} }
+    closeParen { Special $$ ")" }
+    openParen { Special $$ "(" }
+    colon { SignatureTok $$ "" }
+    signature { SignatureTok _ $$ }
+    comma { Special $$ "," }
+    percent { Operator $$ "%" }
+    geq { Operator $$ ">=" }
+    leq { Operator $$ "<=" }
+    neq { Operator $$ "!=" }
+    openTermetric { Operator $$ ".<" }
+    closeTermetric { Operator $$ ">." }
+    mutateArrow { FuncType $$ "->" }
+    mutateEq { Operator $$ ":=" }
+    lbracket { Operator $$ "<" }
+    rbracket { Operator $$ ">" }
+    eq { Operator $$ "=" }
+    or { Operator $$ "||" }
+    vbar { Special $$ "|" }
+    lbrace { Special $$ "{" }
+    rbrace { Special $$ "}" }
+    funcArrow { FuncType _ $$ }
+    plainArrow { Arrow $$ "=>" }
+    cloref1Arrow { Arrow $$ "=<cloref1>" }
+    cloptr1Arrow { Arrow $$ "=<cloptr1>" }
+    lincloptr1Arrow { Arrow $$ "=<lincloptr1>" }
+    spear { Arrow $$ "=>>" }
+    lsqbracket { Special $$ "[" }
+    rsqbracket { Special $$ "]" }
+    string { StringTok _ $$ }
+    charLit { CharTok _ $$ }
+    underscore { Special $$ "_" }
+    minus { Operator $$ "-" }
+    plus { Operator $$ "+" }
+    div { Operator $$ "/" }
+    mult { Operator $$ "*" }
+    exclamation { Special $$ "!" }
+    dot { Special $$ "." }
+    at { Special $$ "@" }
+    tilde { Operator $$ "~" }
+    dollar { Special $$ "$" }
+    semicolon { Special $$ ";" }
+    andOp { Operator $$ "&&" }
+    doubleEq { Operator $$ "==" }
+    doubleDot { Operator $$ ".." }
+    doubleParens { DoubleParenTok $$ }
+    doubleBraces { DoubleBracesTok $$ }
+    doubleBrackets { DoubleBracketTok $$ }
+    prfTransform { Operator $$ ">>" } -- For types like &a >> a?!
+    refType { Special $$ "&" } -- For types like &a
+    maybeProof { Operator $$ "?" } -- For types like a?
+    fromVT { Operator $$ "?!" } -- For types like a?!
+    openExistential { Operator $$ "#[" } -- Same as `[` in ATS2
+    cblock { CBlockLex _ $$ }
+    define { MacroBlock _ $$ }
+    lineComment { $$@CommentLex{} }
+    lspecial { SpecialBracket $$ }
+    atbrace { Operator $$ "@{" }
+    exp { Operator $$ "**" }
+    mod { Keyword $$ KwMod }
+    fixAt { Keyword $$ KwFixAt }
+    lamAt { Keyword $$ KwLambdaAt }
+    infixr { FixityTok $$ "infixr" }
+    infixl { FixityTok $$ "infixr" }
+    prefix { FixityTok $$ "prefix" }
+    postfix { FixityTok $$ "postfix" }
+
+%%
+
+ATS : Declarations { ATS $1 }
+
+-- | Parse declarations in a list
+Declarations : { [] } 
+             | Declarations Declaration { $2 : $1 }
+             | Declarations FunDecl { $2 ++ $1 }
+             | Declarations local ATS in ATS end { Local $2 $3 $5 : $1 }
+
+-- | Several comma-separated types
+TypeIn : Type { [$1] }
+       | TypeIn comma Type { $3 : $1 }
+
+-- | Several comma-separated types or static expressions
+TypeInExpr : TypeIn { $1 }
+           | StaticExpression { [ConcreteType $1] }
+           | TypeInExpr comma Type { $3 : $1 }
+           | TypeInExpr comma StaticExpression { ConcreteType $3 : $1 }
+
+-- | Parse a type
+Type : Name openParen TypeInExpr closeParen { Dependent $1 $3 }
+     | identifierSpace openParen TypeInExpr closeParen { Dependent (Unqualified $ to_string $1) $3 }
+     | bool { Bool }
+     | int { Int }
+     | nat { Nat }
+     | addr { Addr }
+     | stringType { String }
+     | charType { Char }
+     | voidType { Void }
+     | t0pPlain { T0p None }
+     | t0pCo { T0p Plus }
+     | vt0pPlain { Vt0p None }
+     | vt0pCo { Vt0p Plus }
+     | stringType openParen StaticExpression closeParen { DepString $3 }
+     | stringType StaticExpression { DepString $2 }
+     | int openParen StaticExpression closeParen { DependentInt $3 }
+     | bool openParen StaticExpression closeParen { DependentBool $3 }
+     | identifierSpace { Named (Unqualified $ to_string $1) }
+     | Name { Named $1 }
+     | exclamation Type { Unconsumed $2 }
+     | Type mutateArrow Type { FunctionType "->" $1 $3 }
+     | Type funcArrow Type { FunctionType $2 $1 $3 }
+     | refType Type { RefType $2 }
+     | Type maybeProof { MaybeVal $1 } 
+     | Type fromVT { FromVT $1 }
+     | Type prfTransform Type { AsProof $1 (Just $3) }
+     | Type prfTransform underscore { AsProof $1 Nothing }
+     | view at Type { ViewType $1 $3 }
+     | viewPlusMinus { ViewLiteral $1 }
+     | view { ViewLiteral None }
+     | Existential Type { Ex $1 $2 }
+     | Universal Type { ForA $1 $2 }
+     | Type at Type { At $2 (Just $1) $3 }
+     | at Type { At $1 Nothing $2 }
+     | atbrace Records rbrace { AnonymousRecord $1 $2 }
+     | openParen Type vbar Type closeParen { ProofType $1 $2 $4 }
+     | identifierSpace identifier { Dependent (Unqualified $ to_string $1) [Named (Unqualified $ to_string $2)] }
+     | openParen TypeIn closeParen { Tuple $1 $2 }
+     | openParen Type closeParen { $2 }
+     | int StaticExpression { DependentInt $2 }
+     | doubleParens { NoneType $1 }
+     | minus {% Left $ Expected $1 "Type" "-" }
+     | dollar {% Left $ Expected $1 "Type" "$" }
+     | int identifier openParen {% Left $ Expected (token_posn $2) "Static integer expression" (to_string $2) }
+
+FullArgs : Args { $1 }
+
+-- | A comma-separated list of arguments
+Args : Arg { [$1] }
+     | FullArgs comma Arg vbar Arg { PrfArg $3 $5 : $1 }
+     | Args comma Arg { $3 : $1 }
+     | Arg vbar Arg { [ PrfArg $1 $3 ] }
+
+TypeArg : identifier { Arg (First $ to_string $1) }
+        | IdentifierOr colon Type { Arg (Both $1 $3) }
+        | Type { Arg (Second $1) }
+
+Arg : TypeArg { $1 }
+    | StaticExpression { Arg (Second (ConcreteType $1)) }
+
+-- | Parse a literal
+Literal : boolLit { BoolLit $1 }
+        | timeLit { TimeLit $1 }
+        | intLit { IntLit $1 }
+        | floatLit { FloatLit $1 }
+        | string { StringLit $1 }
+        | charLit { CharLit $1 }
+        | doubleParens { VoidLiteral $1 }
+
+-- | Parse a list of comma-separated patterns
+PatternIn : Pattern { [$1] }
+          | PatternIn comma Pattern { $3 : $1 }
+
+-- | Parse a pattern match
+Pattern : identifier { PName (to_string $1) [] }
+        | identifierSpace { PName (to_string $1) [] }
+        | underscore { Wildcard $1 }
+        | identifier doubleParens { PName (to_string $1 ++ "()") [] }
+        | tilde Pattern { Free $2 }
+        | identifier openParen PatternIn closeParen { PName (to_string $1) $3 }
+        | identifier Pattern { PSum (to_string $1) $2 }
+        | identifierSpace Pattern { PSum (to_string $1) $2 }
+        | openParen PatternIn vbar PatternIn closeParen { Proof $1 $2 $4 }
+        | openParen PatternIn closeParen { TuplePattern $2 }
+        | Literal { PLiteral $1 }
+        | Pattern when Expression { Guarded $2 $3 $1 }
+        | at Pattern { AtPattern $1 $2 }
+        | identifier Universals Pattern { UniversalPattern (token_posn $1) (to_string $1) $2 $3 }
+        | identifierSpace Universals Pattern { UniversalPattern (token_posn $1) (to_string $1) $2 $3 }
+        | Existential Pattern { ExistentialPattern $1 $2 }
+        | minus {% Left $ Expected $1 "Pattern" "-" }
+        | plus {% Left $ Expected $1 "Pattern" "+" }
+
+-- | Parse a case expression
+Case : vbar Pattern CaseArrow Expression { [($2, $3, $4)] }
+     | Pattern CaseArrow Expression { [($1, $2, $3)] }
+     | Case vbar Pattern CaseArrow Expression { ($3, $4, $5) : $1 }
+
+ExpressionPrf : ExpressionIn { (Nothing, $1) }
+              | Expression vbar ExpressionIn { (Just $1, $3) } -- FIXME only passes one proof?
+
+-- | A list of comma-separated expressions
+ExpressionIn : Expression { [$1] }
+             | ExpressionIn comma Expression { $3 : $1 }
+
+Tuple : PreExpression comma PreExpression { [$3, $1] }
+      | Tuple comma PreExpression { $3 : $1 }
+
+-- | Parse an arrow in a case statement
+CaseArrow : plainArrow { Plain $1 }
+          | spear { Spear $1 }
+          | minus {% Left $ Expected $1 "Arrow" "-" }
+          | eq {% Left $ Expected $1 "Arrow" "=" }
+          | minus {% Left $ Expected $1 "Arrow" "-" }
+
+LambdaArrow : plainArrow { Plain $1 }
+            | cloref1Arrow { Full $1 "cloref1" } -- TODO do this more efficiently.
+            | cloptr1Arrow { Full $1 "cloptr1" }
+            | lincloptr1Arrow { Full $1 "lincloptr1" }
+            | minus {% Left $ Expected $1 "Arrow" "-" }
+            | openParen {% Left $ Expected $1 "Arrow" "(" }
+            | closeParen {% Left $ Expected $1 "Arrow" ")" }
+
+-- | Expression or named call to an expression
+Expression : identifierSpace PreExpression { Call (Unqualified $ to_string $1) [] [] Nothing [$2] }
+           | PreExpression { $1 }
+           | openParen Tuple closeParen { TupleEx $1 $2 }
+           | Expression semicolon Expression { Precede $1 $3 }
+           | Expression semicolon { $1 }
+           | openParen Expression closeParen { $2 }
+           | Expression colon Type { TypeSignature $1 $3 } -- TODO is a more general expression sensible?
+           | openParen Expression vbar Expression closeParen { ProofExpr $1 $2 $4 }
+           | list_vt lbrace Type rbrace openParen ExpressionIn closeParen { ListLiteral $1 "vt" $3 $6 }
+           | list lbrace Type rbrace openParen ExpressionIn closeParen { ListLiteral $1 "" $3 $6 }
+           | begin Expression extern {% Left $ Expected $3 "end" "extern" }
+           | Expression prfTransform underscore {% Left $ Expected $2 "Rest of expression or declaration" ">>" }
+
+TypeArgs : lbrace Type rbrace { [$2] }
+         | lbrace TypeIn rbrace { $2 }
+         | TypeArgs lbrace Type rbrace { $3 : $1 }
+         | lbrace doubleDot rbrace { [ ImplicitType $2 ] } -- FIXME only valid on function calls
+         | TypeArgs lbrace TypeIn rbrace { $3 ++ $1 }
+
+BracketedArgs : lbracket Type rbracket { [$2] }
+              | lbracket TypeIn rbrace { $2 }
+
+Call : Name doubleParens { Call $1 [] [] Nothing [] }
+     | identifierSpace openParen ExpressionPrf closeParen { Call (Unqualified $ to_string $1) [] [] (fst $3) (snd $3) }
+     | Name openParen ExpressionPrf closeParen { Call $1 [] [] (fst $3) (snd $3) }
+     | Name TypeArgs openParen ExpressionPrf closeParen { Call $1 [] $2 (fst $4) (snd $4) }
+     | Name TypeArgs { Call $1 [] $2 Nothing [] }
+     | Name lspecial TypeIn rbracket doubleParens { Call $1 $3 [] Nothing [VoidLiteral $5] }
+     | Name lspecial TypeIn rbracket openParen ExpressionPrf closeParen { Call $1 $3 [] (fst $6) (snd $6) }
+     | Name lspecial TypeIn rbracket { Call $1 $3 [] Nothing [] }
+     | raise PreExpression { Call (SpecialName $1 "raise") [] [] Nothing [$2] } -- $raise can have at most one argument
+     | Name openParen ExpressionPrf end {% Left $ Expected $4 ")" "end"}
+     | Name openParen ExpressionPrf else {% Left $ Expected $4 ")" "else"}
+
+StaticArgs : StaticExpression { [$1] }
+           | StaticArgs comma StaticExpression { $3 : $1 }
+
+StaticExpression : Name { StaticVal $1 }
+                 | StaticExpression BinOp StaticExpression { StaticBinary $2 $1 $3 }
+                 | intLit { StaticInt $1 }
+                 | doubleParens { StaticVoid $1 }
+                 | boolLit { StaticBool $1 }
+                 | sif StaticExpression then StaticExpression else StaticExpression { Sif $2 $4 $6 } -- TODO separate type for static expressions
+                 | identifierSpace { StaticVal (Unqualified $ to_string $1) }
+                 | Name openParen StaticArgs closeParen { SCall $1 $3 }
+                 | identifierSpace openParen StaticArgs closeParen { SCall (Unqualified $ to_string $1) $3 }
+                 | StaticExpression semicolon StaticExpression { SPrecede $1 $3 }
+    
+-- | Parse an expression that can be called without parentheses
+PreExpression : identifier lsqbracket PreExpression rsqbracket { Index $2 (Unqualified $ to_string $1) $3 }
+              | Literal { $1 }
+              | Call { $1 }
+              | case Expression of Case { Case $3 $1 $2 $4 }
+              | openParen Expression closeParen { ParenExpr $1 $2 }
+              | PreExpression BinOp PreExpression { Binary $2 $1 $3 }
+              | UnOp PreExpression { Unary $1 $2 } -- FIXME throw error when we try to negate a string literal/time
+              | PreExpression dot Name { Access $2 $1 $3 }
+              | PreExpression dot intLit { Access $2 $1 (Unqualified $ show $3) }
+              | PreExpression dot identifierSpace { Access $2 $1 (Unqualified $ to_string $3) }
+              | if Expression then Expression { If $2 $4 Nothing}
+              | if Expression then Expression else Expression { If $2 $4 (Just $6) }
+              | let ATS in end { Let $1 $2 Nothing }
+              | let ATS in Expression end { Let $1 $2 (Just $4) }
+              | let ATS in Expression vbar {% Left $ Expected $5 "end" "|" }
+              | lambda Pattern LambdaArrow Expression { Lambda $1 $3 $2 $4 }
+              | llambda Pattern LambdaArrow Expression { LinearLambda $1 $3 $2 $4 }
+              | addrAt PreExpression { AddrAt $1 $2 }
+              | viewAt PreExpression { ViewAt $1 $2 }
+              | PreExpression at PreExpression { AtExpr $1 $3 }
+              | atbrace RecordVal rbrace { RecordValue $1 $2 Nothing }
+              | atbrace RecordVal rbrace colon Type { RecordValue $1 $2 (Just $5) }
+              | exclamation PreExpression { Deref $1 $2 }
+              | PreExpression mutateArrow identifierSpace mutateEq PreExpression { FieldMutate $2 $1 (to_string $3) $5 }
+              | PreExpression mutateArrow identifier mutateEq PreExpression { FieldMutate $2 $1 (to_string $3) $5 }
+              | PreExpression mutateEq PreExpression { Mutate $1 $3 }
+              | PreExpression where lbrace Declarations rbrace { WhereExp $1 $4 }
+              | identifierSpace { NamedVal (Unqualified $ to_string $1) }
+              | begin Expression end { Begin $1 $2 }
+              | Name { NamedVal $1 }
+              | lbrace ATS rbrace { Actions $2 }
+              | while openParen PreExpression closeParen PreExpression { While $1 $3 $5 }
+              | include {% Left $ Expected $1 "Expression" "include" }
+              | staload {% Left $ Expected $1 "Expression" "staload" }
+              | overload {% Left $ Expected $1 "Expression" "overload" }
+              | var {% Left $ Expected $1 "Expression" "var" }
+              | Termetric {% Left $ Expected (fst $1) "Expression" "termetric" }
+              | fromVT {% Left $ Expected $1 "Expression" "?!" }
+              | prfTransform {% Left $ Expected $1 "Expression" ">>" }
+              | maybeProof {% Left $ Expected $1 "Expression" "?" }
+              | let openParen {% Left $ Expected $1 "Expression" "let (" }
+              | let ATS in Expression lineComment {% Left $ Expected (token_posn $5) "end" (take 2 $ to_string $5) }
+              | let ATS in Expression extern {% Left $ Expected $5 "end" "extern" }
+              | let ATS in Expression fun {% Left $ Expected $5 "end" "fun" }
+              | let ATS in Expression vtypedef {% Left $ Expected $5 "end" "vtypedef" }
+              | if Expression then Expression else else {% Left $ Expected $6 "Expression" "else" }
+
+-- | Parse a termetric
+Termetric : openTermetric StaticExpression closeTermetric { ($1, $2) }
+          | underscore {% Left $ Expected $1 "_" "Termination metric" }
+          | dollar {% Left $ Expected $1 "$" "Termination metric" }
+
+-- | Parse an existential quantier on a type
+Existential : lsqbracket Args vbar StaticExpression rsqbracket { Existential $2 False Nothing (Just $4) }
+            | lsqbracket Args rsqbracket { Existential $2 False Nothing Nothing }
+            | openExistential Args rsqbracket { Existential $2 True Nothing Nothing }
+            | openExistential Args vbar StaticExpression rsqbracket { Existential $2 True Nothing (Just $4) }
+            | lsqbracket Args colon Type rsqbracket { Existential $2 False (Just $4) Nothing } -- FIXME arguments should include more than just ':'
+            | lsqbracket StaticExpression rsqbracket { Existential [] False Nothing (Just $2) }
+            
+-- | Parse a universal quantifier on a type
+Universal : lbrace Args rbrace { Universal $2 Nothing Nothing }
+          | lbrace Args vbar StaticExpression rbrace { Universal $2 Nothing (Just $4) }
+
+-- | Parse the details of an implementation
+Implementation : FunName doubleParens eq Expression { Implement $2 [] [] $1 [] $4 }
+               | FunName openParen FullArgs closeParen eq Expression { Implement $2 [] [] $1 $3 $6 }
+               | FunName Universals openParen FullArgs closeParen eq Expression { Implement $3 [] $2 $1 $4 $7 }
+               | Universals FunName openParen FullArgs closeParen eq Expression { Implement $3 $1 [] $2 $4 $7 }
+               | Universals FunName Universals openParen FullArgs closeParen eq Expression { Implement $4 $1 $3 $2 $5 $8 }
+
+-- | Parse a function name
+FunName : IdentifierOr { Unqualified $1 }
+        | identifier dollar identifier { Functorial (to_string $1) (to_string $3) }
+
+-- | Parse a general name
+Name : identifier { Unqualified (to_string $1) }
+     | underscore { Unqualified "_" }
+     | listVT { Unqualified "list_vt" }
+     | foldAt { Unqualified "fold@" }
+     | dollar identifier dot identifier { Qualified $1 (to_string $4) (to_string $2) }
+     | dollar identifier dot identifierSpace { Qualified $1 (to_string $4) (to_string $2) }
+     | dollar effmaskWrt { SpecialName $1 "effmask_wrt" }
+     | dollar effmaskAll { SpecialName $1 "effmask_all" }
+     | dollar extype { SpecialName $1 "effmask_all" }
+     | dollar listVT { SpecialName $1 "list_vt" }
+     | dollar ldelay { SpecialName $1 "ldelay" } -- FIXME there is probably a better/more efficient way of doing this
+     | dollar {% Left $ Expected $1 "Name" "$" }
+
+-- | Parse a list of values in a record
+RecordVal : IdentifierOr eq Expression { [($1, $3)] }
+          | RecordVal comma IdentifierOr eq Expression { ($3, $5) : $1 }
+
+-- | Parse a list of types in a record
+Records : IdentifierOr eq Type { [($1, $3)] }
+        | Records comma IdentifierOr eq Type { ($3, $5) : $1 }
+
+IdentifiersIn : IdentifierOr { [$1] }
+              | IdentifiersIn comma IdentifierOr { $3 : $1 }
+
+OfType : { Nothing }
+       | of Type { Just $2 }
+
+-- | Parse a constructor for a sum type
+SumLeaf : vbar Universals identifier { Leaf $2 (to_string $3) [] Nothing }
+        | vbar Universals identifierSpace of Type { Leaf $2 (to_string $3) [] (Just $5) }
+        | vbar Universals IdentifierOr openParen IdentifiersIn closeParen OfType { Leaf $2 $3 $5 $7 }
+
+-- | Parse all constructors of a sum type
+Leaves : SumLeaf { [$1] }
+       | Leaves SumLeaf { $2 : $1 }
+       | Universals identifierSpace of Type { [Leaf $1 (to_string $2) [] (Just $4)] }
+       | Universals identifier { [Leaf $1 (to_string $2) [] Nothing] }
+       | Universals identifier openParen IdentifiersIn closeParen OfType { [Leaf $1 (to_string $2) $4 $6] } -- FIXME should take any static expression.
+       | dollar {% Left $ Expected $1 "|" "$" }
+
+Universals : { [] }
+           | doubleBraces { [] }
+           | Universals Universal { $2 : $1 }
+
+-- | Optionally parse a termetric
+OptTermetric : { Nothing }
+             | Termetric { Just (snd $1) }
+
+-- | Parse a unary operator
+UnOp : tilde { Negate }
+
+-- | Parse a binary operator
+BinOp : plus { Add }
+      | minus { Sub }
+      | div { Div }
+      | mult { Mult }
+      | geq { GreaterThanEq }
+      | leq { LessThanEq }
+      | lbracket { LessThan }
+      | rbracket { GreaterThan }
+      | neq { NotEqual }
+      | andOp { LogicalAnd }
+      | or { LogicalOr }
+      | doubleEq { StaticEq }
+      | eq { Equal }
+      | mod { Mod }
+      | percent { Mod }
+
+-- | Optionally parse a function body
+OptExpression : { Nothing }
+              | eq Expression { Just $2 } -- FIXME only let this happen for external declarations
+
+-- | Parse a constructor for a 'dataprop'
+DataPropLeaf : vbar Universals Expression { DataPropLeaf $2 $3 Nothing }
+             | Universals Expression { DataPropLeaf $1 $2 Nothing }
+             | vbar Universals Expression of Expression { DataPropLeaf $2 $3 (Just $5) }
+             | Universals Expression of Expression { DataPropLeaf $1 $2 (Just $4) }
+
+-- | Parse several constructors for a 'dataprop'
+DataPropLeaves : DataPropLeaf { [$1] }
+               | DataPropLeaves DataPropLeaf { $2 : $1 }
+               | prval {% Left $ Expected $1 "Constructor" "prval" }
+               | var {% Left $ Expected $1 "Constructor" "var" }
+               | val {% Left $ Expected (token_posn $1) "Constructor" "val" }
+               | lambda {% Left $ Expected $1 "Constructor" "lam" }
+               | llambda {% Left $ Expected $1 "Constructor" "llam" }
+               | minus {% Left $ Expected $1 "Constructor" "-" }
+               | dollar {% Left $ Expected $1 "Constructor" "$" }
+               | fromVT {% Left $ Expected $1 "Constructor" "?!" }
+               | prfTransform {% Left $ Expected $1 "Constructor" ">>" }
+               | maybeProof {% Left $ Expected $1 "Constructor" "?" }
+
+Signature : signature { $1 }
+          | colon { "" }
+
+OptType : Type { Just $1 }
+        | { Nothing }
+
+-- | Parse a type signature and optional function body
+PreFunction : FunName openParen FullArgs closeParen Signature OptType OptExpression { (PreF $1 $5 [] [] $3 $6 Nothing $7) }
+            | FunName Universals OptTermetric Signature OptType OptExpression { PreF $1 $4 [] $2 [NoArgs] $5 $3 $6 }
+            | FunName Universals OptTermetric doubleParens Signature OptType OptExpression { PreF $1 $5 [] $2 [] $6 $3 $7 }
+            | FunName Universals OptTermetric openParen FullArgs closeParen Signature OptType OptExpression { PreF $1 $7 [] $2 $5 $8 $3 $9 }
+            | Universals FunName Universals OptTermetric openParen FullArgs closeParen Signature OptType OptExpression { PreF $2 $8 $1 $3 $6 $9 $4 $10 }
+            | Universals FunName Universals OptTermetric Signature OptType OptExpression { PreF $2 $5 $1 $3 [] $6 $4 $7 }
+            | prval {% Left $ Expected $1 "Function signature" "prval" }
+            | var {% Left $ Expected $1 "Function signature" "var" }
+            | val {% Left $ Expected (token_posn $1) "Function signature" "val" }
+            | lambda {% Left $ Expected $1 "Function signature" "lam" }
+            | llambda {% Left $ Expected $1 "Function signature" "llam" }
+            | lsqbracket {% Left $ Expected $1 "Function signature" "[" }
+
+-- | Parse affiliated `sortdef`s
+AndSort : AndSort and IdentifierOr eq Type { AndD $1 (SortDef $2 $3 $5) } -- TODO figure out if this is building up the slow way
+        | sortdef IdentifierOr eq Type { SortDef $1 $2 $4 }
+
+-- | Function declaration
+FunDecl : fun PreFunction { [ Func $1 (Fun $2) ] }
+        | prfun PreFunction { [ Func $1 (PrFun $2) ] }
+        | prfn PreFunction { [ Func $1 (PrFn $2) ] }
+        | fnx PreFunction { [ Func $1 (Fnx $2) ] }
+        | castfn PreFunction { [ Func $1 (CastFn $2) ] }
+        | fn PreFunction identifier {% Left $ Expected (token_posn $3) "=" (to_string $3) }
+        | fn PreFunction { [ Func $1 (Fn $2) ] }
+        | FunDecl and PreFunction { Func $2 (And $3) : $1 }
+        | extern FunDecl { over _head (Extern $1) $2 }
+        | extern fun PreFunction eq {% Left $ Expected $1 "Declaration" "Function body" }
+        | extern fnx PreFunction eq {% Left $ Expected $1 "Declaration" "Function body" }
+        | extern praxi PreFunction eq {% Left $ Expected $1 "Declaration" "Function body" }
+        | extern prfun PreFunction eq {% Left $ Expected $1 "Declaration" "Function body" }
+        | extern prfn PreFunction eq {% Left $ Expected $1 "Declaration" "Function body" }
+        | lambda {% Left $ Expected $1 "Function declaration" "lam" }
+        | llambda {% Left $ Expected $1 "Function declaration" "llam" }
+        | fun fn {% Left $ Expected $2 "Function name" "fn" }
+        | fn fun {% Left $ Expected $2 "Function name" "fun" }
+        | extern FunDecl identifier openParen {% Left $ Expected (token_posn $3) "Static integer expression" (to_string $3) }
+
+IdentifierOr : identifier { to_string $1 }
+             | identifierSpace { to_string $1 }
+
+MaybeType : eq Type { Just $2 }
+          | { Nothing }
+
+-- | Parse a declaration defining a type
+TypeDecl : typedef IdentifierOr eq Type { TypeDef $1 $2 [] $4 }
+         | typedef IdentifierOr openParen FullArgs closeParen eq Type { TypeDef $1 $2 $4 $7 }
+         | vtypedef IdentifierOr eq Type { ViewTypeDef $1 $2 [] $4 }
+         | vtypedef IdentifierOr openParen FullArgs closeParen eq Type { ViewTypeDef $1 $2 $4 $7 }
+         | datatype IdentifierOr eq Leaves { SumType $2 [] $4 }
+         | datatype IdentifierOr openParen Args closeParen eq Leaves { SumType $2 $4 $7 }
+         | datavtype IdentifierOr eq Leaves { SumViewType $2 [] $4 }
+         | datavtype IdentifierOr openParen Args closeParen eq Leaves { SumViewType $2 $4 $7 }
+         | abst0p IdentifierOr eq Type { AbsT0p $1 $2 $4 }
+         | viewdef IdentifierOr openParen FullArgs closeParen eq Type { ViewDef $1 $2 $4 $7 }
+         | absvt0p IdentifierOr openParen FullArgs closeParen MaybeType { AbsVT0p $1 $2 $4 $6 }
+         | absvt0p IdentifierOr eq Type { AbsVT0p $1 $2 [] (Just $4) }
+         | absview IdentifierOr openParen FullArgs closeParen MaybeType { AbsView $1 $2 $4 $6 }
+         | abstype IdentifierOr openParen FullArgs closeParen MaybeType { AbsType $1 $2 $4 $6 }
+         | absvtype IdentifierOr openParen FullArgs closeParen MaybeType { AbsViewType $1 $2 $4 $6 }
+         | dataprop IdentifierOr openParen FullArgs closeParen eq DataPropLeaves { DataProp $1 $2 $4 $7 }
+         | absprop IdentifierOr openParen FullArgs closeParen { AbsProp $1 $2 $4 }
+         | stadef IdentifierOr eq Name { Stadef $2 $4 [] }
+         | stadef IdentifierOr eq Name openParen TypeIn closeParen { Stadef $2 $4 $6 }
+         | stadef boolLit eq Name { Stadef (over _head toLower (show $2)) $4 [] } -- TODO identifierSpace
+         | sortdef IdentifierOr eq Type { SortDef $1 $2 $4 }
+         | AndSort { $1 }
+
+Fixity : infixr { RightFix $1 }
+       | infixl { LeftFix $1 }
+       | prefix { Pre $1 }
+       | postfix { Post $1 }
+
+Operator : identifierSpace { to_string $1 }
+         | exp { "**" }
+
+Operators : Operator { [$1] }
+          | Operators Operator { $2 : $1 }
+          | Operators identifier { to_string $2 : $1 }
+
+StackFunction : openParen Args closeParen Signature Type plainArrow Expression { StackF $4 $2 $5 $7 }
+
+-- | Parse a declaration
+Declaration : include string { Include $2 }
+            | define { Define $1 }
+            | define identifierSpace string { Define ($1 ++ " " ++ to_string $2 ++ $3) } -- FIXME better approach?
+            | define identifierSpace intLit { Define ($1 ++ " " ++ to_string $2 ++ " " ++ show $3) }
+            | cblock { CBlock $1 }
+            | lineComment { Comment (to_string $1) }
+            | staload underscore eq string { Staload (Just "_") $4 }
+            | staload string { Staload Nothing $2 }
+            | staload IdentifierOr eq string { Staload (Just $2) $4 }
+            | extern Declaration { Extern $1 $2 }
+            | var Pattern colon Type with PreExpression { Var (Just $4) $2 Nothing (Just $6) } -- FIXME signature is too general.
+            | var Pattern colon Type eq PreExpression { Var (Just $4) $2 (Just $6) Nothing }
+            | val Pattern colon Type eq PreExpression { Val (get_addendum $1) (Just $4) $2 $6 }
+            | val Pattern eq Expression { Val (get_addendum $1) Nothing $2 $4 }
+            | var Pattern eq Expression { Var Nothing $2 (Just $4) Nothing }
+            | var Pattern colon Type { Var (Just $4) $2 Nothing Nothing }
+            | var Pattern eq fixAt IdentifierOr StackFunction { Var Nothing $2 (Just $ FixAt $5 $6) Nothing }
+            | var Pattern eq lamAt StackFunction { Var Nothing $2 (Just $ LambdaAt $5) Nothing }
+            | prval Pattern eq Expression { PrVal $2 $4 }
+            | praxi PreFunction { Func $1 (Praxi $2) }
+            | primplmnt Implementation { ProofImpl $2 }
+            | implement Implementation { Impl [] $2 }
+            | implement openParen Args closeParen Implementation { Impl $3 $5 }
+            | overload BinOp with Name { OverloadOp $1 $2 $4 }
+            | overload identifierSpace with Name { OverloadIdent $1 (to_string $2) $4 Nothing }
+            | overload tilde with identifierSpace of intLit { OverloadIdent $1 "~" (Unqualified $ to_string $4) (Just $6) } -- FIXME figure out a general solution.
+            | assume Name openParen Args closeParen eq Expression { Assume $2 $4 $7 }
+            | tkindef IdentifierOr eq string { TKind $1 (Unqualified $2) $4 }
+            | TypeDecl { $1 }
+            | symintr Name { SymIntr $1 $2 }
+            | stacst IdentifierOr colon Type OptExpression { Stacst $1 (Unqualified $2) $4 $5 }
+            | propdef IdentifierOr openParen Args closeParen eq Type { PropDef $1 $2 $4 $7 }
+            | Fixity intLit Operators { FixityDecl $1 (Just $2) $3 }
+            | val Universals IdentifierOr colon Type { StaVal $2 $3 $5 }
+            | lambda {% Left $ Expected $1 "Declaration" "lam" }
+            | llambda {% Left $ Expected $1 "Declaration" "llam" }
+            | minus {% Left $ Expected $1 "Declaration" "-" }
+            | dollar {% Left $ Expected $1 "Declaration" "$" }
+            | fromVT {% Left $ Expected $1 "Declaration" "?!" }
+            | prfTransform {% Left $ Expected $1 "Declaration" ">>" }
+            | maybeProof {% Left $ Expected $1 "Declaration" "?" }
+            | identifier {% Left $ Expected (token_posn $1) "Declaration" (to_string $1) }
+
+{
+
+data ATSError a = Expected AlexPosn a a
+                | Unknown Token -- FIXME error type for expression when a static expression was expected (?)
+                deriving (Eq, Show, Generic, NFData)
+
+instance Pretty AlexPosn where
+    pretty (AlexPn _ line col) = pretty line <> ":" <> pretty col
+
+instance Pretty (ATSError String) where
+    pretty (Expected p s1 s2) = red "Error: " <> pretty p <> linebreak <> (indent 2 $ "Unexpected" <+> squotes (string s2) <> ", expected:" <+> squotes (string s1)) <> linebreak
+    pretty (Unknown t) = red "Error:" <+> "unexpected token" <+> squotes (pretty t) <+> "at" <+> pretty (token_posn t) <> linebreak
+
+parseError :: [Token] -> Either (ATSError String) a
+parseError = Left . Unknown . head 
+}
diff --git a/src/Language/ATS/PrettyPrint.hs b/src/Language/ATS/PrettyPrint.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/ATS/PrettyPrint.hs
@@ -0,0 +1,525 @@
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+{-# LANGUAGE CPP                  #-}
+{-# LANGUAGE DeriveAnyClass       #-}
+{-# LANGUAGE DeriveGeneric        #-}
+{-# LANGUAGE FlexibleContexts     #-}
+{-# LANGUAGE FlexibleInstances    #-}
+{-# LANGUAGE OverloadedStrings    #-}
+{-# LANGUAGE PatternSynonyms      #-}
+{-# LANGUAGE StandaloneDeriving   #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+
+module Language.ATS.PrettyPrint ( printATS
+                                , printATSCustom
+                                , printATSFast
+                                ) where
+
+import           Control.Composition                   hiding ((&))
+import           Control.DeepSeq                       (NFData)
+import           Control.Lens                          hiding (op, pre)
+#if __GLASGOW_HASKELL__ >= 801
+import           Data.Function                         (on)
+#endif
+import           Data.Functor.Foldable                 (cata)
+import           GHC.Generics                          (Generic)
+import           Language.ATS.Types
+import           Prelude                               hiding ((<$>))
+import           System.Console.ANSI.Types
+import           Text.PrettyPrint.ANSI.Leijen
+import           Text.PrettyPrint.ANSI.Leijen.Internal
+
+infixr 5 $$
+
+deriving instance Generic Underlining
+deriving instance NFData Underlining
+deriving instance Generic ConsoleIntensity
+deriving instance NFData ConsoleIntensity
+deriving instance Generic Color
+deriving instance NFData Color
+deriving instance Generic ColorIntensity
+deriving instance NFData ColorIntensity
+deriving instance Generic ConsoleLayer
+deriving instance NFData ConsoleLayer
+deriving instance Generic Doc
+deriving instance NFData Doc
+
+instance Eq Doc where
+    (==) = on (==) show
+
+-- | Pretty-print with sensible defaults.
+printATS :: ATS -> String
+printATS = (<> "\n") . printATSCustom 0.6 120
+
+printATSCustom :: Float -- ^ Ribbon fraction
+               -> Int -- ^ Ribbon width
+               -> ATS -> String
+printATSCustom r i (ATS x) = g mempty
+    where g = (displayS . renderSmart r i . pretty) (ATS $ reverse x)
+
+-- | Fast pretty-printer without indendation. Useful for generating code.
+printATSFast :: ATS -> String
+printATSFast (ATS x) = g mempty
+    where g = (displayS . renderCompact . (<> "\n") . pretty) (ATS $ reverse x)
+
+instance Pretty Name where
+    pretty (Unqualified n)   = text n
+    pretty (Qualified _ i n) = "$" <> text n <> "." <> text i
+    pretty (SpecialName _ s) = "$" <> text s
+    pretty (Functorial s s') = text s <> "$" <> text s'
+    pretty Unnamed{}         = mempty
+
+instance Pretty LambdaType where
+    pretty Plain{}    = "=>"
+    pretty Spear{}    = "=>>"
+    pretty (Full _ v) = "=<" <> text v <> ">"
+
+instance Pretty BinOp where
+    pretty Mult          = "*"
+    pretty Add           = "+"
+    pretty Div           = "/"
+    pretty Sub           = "-"
+    pretty GreaterThan   = ">"
+    pretty LessThan      = "<"
+    pretty Equal         = "="
+    pretty NotEqual      = "!="
+    pretty LogicalAnd    = "&&"
+    pretty LogicalOr     = "||"
+    pretty LessThanEq    = "<="
+    pretty GreaterThanEq = ">="
+    pretty StaticEq      = "=="
+    pretty Mod           = "%"
+
+splits :: BinOp -> Bool
+splits Mult       = True
+splits Add        = True
+splits Div        = True
+splits Sub        = True
+splits LogicalAnd = True
+splits LogicalOr  = True
+splits _          = False
+
+startsParens :: Doc -> Bool
+startsParens d = f (show d) where
+    f ('(':_) = True
+    f _       = False
+
+prettySmall :: Doc -> [Doc] -> Doc
+prettySmall op es = mconcat (punctuate (" " <> op <> " ") es)
+
+prettyBinary :: Doc -> [Doc] -> Doc
+prettyBinary op es
+    | length (showFast $ mconcat es) < 80 = prettySmall op es
+    | otherwise = prettyLarge op es
+
+prettyLarge :: Doc -> [Doc] -> Doc
+prettyLarge _ []      = mempty
+prettyLarge op (e:es) = e <$> vsep (fmap (op <+>) es)
+
+-- FIXME we really need a monadic pretty printer lol.
+lengthAlt :: Doc -> Doc -> Doc
+lengthAlt d1 d2
+    | length (showFast d2) >= 30 = d1 <$> indent 4 d2
+    | otherwise = d1 <+> d2
+
+instance Pretty Expression where
+    pretty = cata a . rewriteATS where
+        a (IfF e e' (Just e''))         = "if" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e''
+        a (IfF e e' Nothing)            = "if" <+> e <+> "then" <$> indent 2 e'
+        a (LetF _ e (Just e'))          = flatAlt
+            ("let" <$> indent 2 (pretty ((\(ATS x) -> ATS $ reverse x) e)) <$> "in" <$> indent 2 e' <$> "end")
+            ("let" <+> pretty ((\(ATS x) -> ATS $ reverse x) e) <$> "in" <+> e' <$> "end")
+        a (LetF _ e Nothing)            = flatAlt
+            ("let" <$> indent 2 (pretty ((\(ATS x) -> ATS $ reverse x) e)) <$> "in end")
+            ("let" <+> pretty ((\(ATS x) -> ATS $ reverse x) e) <$> "in end")
+        a (BoolLitF True)               = "true"
+        a (BoolLitF False)              = "false"
+        a (TimeLitF s)                  = text s
+        a (IntLitF i)                   = pretty i
+        a (LambdaF _ lt p e)            = let pre = "lam" <+> pretty p <+> pretty lt in flatAlt (lengthAlt pre e) (pre <+> e)
+        a (LinearLambdaF _ lt p e)      = let pre = "llam" <+> pretty p <+> pretty lt in flatAlt (lengthAlt pre e) (pre <+> e)
+        a (FloatLitF f)                 = pretty f
+        a (StringLitF s)                = text s -- FIXME escape indentation in multi-line strings.
+        a (ParenExprF _ e)              = parens e
+        a (BinListF op@Add es)          = prettyBinary (pretty op) es
+        a (BinaryF op e e')
+            | splits op = e </> pretty op <+> e'
+            | otherwise = e <+> pretty op <+> e'
+        a (IndexF _ n e)                = pretty n <> "[" <> e <> "]"
+        a (UnaryF Negate e)             = "~" <> e
+        a (NamedValF nam)              = pretty nam
+        a (CallF nam [] [] Nothing []) = pretty nam <> "()"
+        a (CallF nam [] [] (Just e) xs) = pretty nam <> prettyArgsG ("(" <> pretty e <+> "| ") ")" xs -- FIXME split eagerly on "|"
+        a (CallF nam [] [] Nothing xs) = pretty nam <> prettyArgs xs
+        a (CallF nam [] us Nothing []) = pretty nam <> prettyArgsU "{" "}" us
+        a (CallF nam [] us Nothing xs) = pretty nam <> prettyArgsU "{" "}" us <> prettyArgsG "(" ")" xs
+        a (CallF nam is [] Nothing []) = pretty nam <> prettyArgsU "<" ">" is
+        a (CallF nam is [] Nothing [x])
+            | startsParens x = pretty nam <> prettyArgsU "<" ">" is <> pretty x
+        a (CallF nam is [] Nothing xs) = pretty nam <> prettyArgsU "<" ">" is <> prettyArgs xs
+        a (CaseF _ add e cs)            = "case" <> pretty add <+> e <+> "of" <$> indent 2 (prettyCases cs)
+        a (VoidLiteralF _)              = "()"
+        a (RecordValueF _ es Nothing)   = prettyRecord es
+        a (RecordValueF _ es (Just x))  = prettyRecord es <+> ":" <+> pretty x
+        a (PrecedeF e e')               = parens (e <+> ";" </> e')
+        a (PrecedeListF es)             = lineAlt (prettyArgsList "; " "(" ")" es) ("(" <> mconcat (punctuate " ; " es) <> ")")
+        a (FieldMutateF _ o f v)        = pretty o <> "->" <> string f <+> ":=" <+> v
+        a (MutateF e e')                = e <+> ":=" <+> e'
+        a (DerefF _ e)                  = "!" <> e
+        a (AccessF _ e n)
+            | noParens e = e <> "." <> pretty n
+            | otherwise = parens e <> "." <> pretty n
+        a (CharLitF '\\')              = "'\\\\'"
+        a (CharLitF '\n')              = "'\\n'"
+        a (CharLitF '\t')              = "'\\t'"
+        a (CharLitF c)                 = "'" <> char c <> "'"
+        a (ProofExprF _ e e')          = "(" <> e <+> "|" <+> e' <> ")"
+        a (TypeSignatureF e t)         = e <+> ":" <+> pretty t
+        a (WhereExpF e d)              = e <+> "where" <$> braces (" " <> nest 2 (pretty (ATS $ reverse d)) <> " ")
+        a (TupleExF _ es)              = parens (mconcat $ punctuate ", " (reverse es))
+        a (WhileF _ e e')              = "while" <> parens e <> e'
+        a (ActionsF as)                = "{" <$> indent 2 (pretty ((\(ATS x) -> ATS $ reverse x) as)) <$> "}"
+        a UnderscoreLitF{}             = "_"
+        a (AtExprF e e')               = e <> "@" <> e'
+        a (BeginF _ e)
+            | not (startsParens e) = linebreak <> indent 2 ("begin" <$> indent 2 e <$> "end")
+            | otherwise = e
+        a (FixAtF n (StackF s as t e)) = "fix@" <+> text n <+> prettyArgs as <+> ":" <> pretty s <+> pretty t <+> "=>" <$> indent 2 (pretty e)
+        a (LambdaAtF (StackF s as t e)) = "lam@" <+> prettyArgs as <+> ":" <> pretty s <+> pretty t <+> "=>" <$> indent 2 (pretty e)
+        a (AddrAtF _ e)                = "addr@" <> e
+        a (ViewAtF _ e)                = "view@" <> e
+        a (ListLiteralF _ s t es)      = "list" <> string s <> "{" <> pretty t <> "}" <> prettyArgs es
+        a BinListF{} = undefined
+        a CallF{} = undefined
+        prettyCases []              = mempty
+        prettyCases [(s, l, t)]     = "|" <+> pretty s <+> pretty l <+> t
+        prettyCases ((s, l, t): xs) = prettyCases xs $$ "|" <+> pretty s <+> pretty l <+> t -- FIXME can leave space with e.g. => \n begin ...
+
+noParens :: Doc -> Bool
+noParens = all (`notElem` ("()" :: String)) . show
+
+patternHelper :: [Doc] -> Doc
+patternHelper ps = mconcat (punctuate ", " (reverse ps))
+
+instance Pretty Pattern where
+    pretty = cata a where
+        a (WildcardF _)                = "_"
+        a (PSumF s x)                  = string s <+> x
+        a (PLiteralF e)                = pretty e
+        a (PNameF s [])                = string s
+        a (PNameF s [x])               = string s <> parens x
+        a (PNameF s ps)                = string s <> parens (patternHelper ps)
+        a (FreeF p)                    = "~" <> p
+        a (GuardedF _ e p)             = p <+> "when" <+> pretty e
+        a (ProofF _ p p')              = parens (patternHelper p <+> "|" <+> patternHelper p')
+        a (TuplePatternF ps)           = parens (patternHelper ps)
+        a (AtPatternF _ p)             = "@" <> p
+        a (UniversalPatternF _ n us p) = text n <> prettyArgsU "" "" us <> p
+        a (ExistentialPatternF e p)    = pretty e <> p
+
+singleArg :: Arg -> Doc
+singleArg x@Arg{} = argHelper (<>) x
+singleArg x       = pretty x
+
+argHelper :: (Doc -> Doc -> Doc) -> Arg -> Doc
+argHelper _ (Arg (First s))   = pretty s
+argHelper _ (Arg (Second t))  = pretty t
+argHelper op (Arg (Both s t)) = pretty s `op` colon `op` pretty t
+argHelper op (PrfArg a a')    = pretty a `op` "|" `op` pretty a'
+argHelper _ NoArgs            = undefined -- in theory we handle this elsewhere.
+
+instance Pretty Arg where
+    pretty = argHelper (<+>)
+
+squish :: BinOp -> Bool
+squish Add  = True
+squish Sub  = True
+squish Mult = True
+squish _    = False
+
+instance Pretty StaticExpression where
+    pretty = cata a where
+        a (StaticValF n)            = pretty n
+        a (StaticBinaryF op se se')
+            | squish op = se <> pretty op <> se'
+            | otherwise = se <+> pretty op <+> se'
+        a (StaticIntF i)            = pretty i
+        a StaticVoidF{}             = "()"
+        a (SifF e e' e'')           = "sif" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e''
+        a (StaticBoolF True)        = "true"
+        a (StaticBoolF False)       = "false"
+        a (SCallF n cs)             = pretty n <> parens (mconcat (punctuate "," . reverse . fmap pretty $ cs))
+        a (SPrecedeF e e')          = e <> ";" <+> e'
+
+instance Pretty Type where
+    pretty = cata a where
+        a IntF                    = "int"
+        a StringF                 = "string"
+        a BoolF                   = "bool"
+        a VoidF                   = "void"
+        a NatF                    = "nat"
+        a AddrF                   = "addr"
+        a CharF                   = "char"
+        a (NamedF n)              = pretty n
+        a (ExF e t)               = pretty e <+> t
+        a (DependentIntF e)       = "int(" <> pretty e <> ")"
+        a (DependentBoolF e)      = "bool(" <> pretty e <> ")"
+        a (DepStringF e)          = "string(" <> pretty e <> ")"
+        a (DependentF n ts)       = pretty n <> parens (mconcat (punctuate ", " (fmap pretty (reverse ts))))
+        a DoubleF                 = "double"
+        a FloatF                  = "float"
+        a (ForAF u t)             = pretty u <+> t
+        a (UnconsumedF t)         = "!" <> t
+        a (AsProofF t (Just t'))  = t <+> ">>" <+> t'
+        a (AsProofF t Nothing)    = t <+> ">> _"
+        a (FromVTF t)             = t <> "?!"
+        a (MaybeValF t)           = t <> "?"
+        a (T0pF ad)               = "t@ype" <> pretty ad
+        a (Vt0pF ad)              = "vt@ype" <> pretty ad
+        a (AtF _ (Just t) t')     = t <+> "@" <+> t'
+        a (AtF _ Nothing t)       = "@" <> t
+        a (ProofTypeF _ t t')     = parens (t <+> "|" <+> t')
+        a (ConcreteTypeF e)       = pretty e
+        a (TupleF _ ts)           = parens (mconcat (punctuate ", " (fmap pretty (reverse ts))))
+        a (RefTypeF t)            = "&" <> t
+        a (ViewTypeF _ t)         = "view@" <> parens t
+        a (FunctionTypeF s t t')  = t <+> string s <+> t'
+        a (ViewLiteralF c)        = "view" <> pretty c
+        a NoneTypeF{}             = "()"
+        a ImplicitTypeF{}         = ".."
+        a (AnonymousRecordF _ rs) = prettyRecord rs
+
+gan :: Maybe Type -> Doc
+gan (Just t) = " : " <> pretty t <> " "
+gan Nothing  = ""
+
+withHashtag :: Bool -> Doc
+withHashtag True = "#["
+withHashtag _    = lbracket
+
+instance Pretty Existential where
+    pretty (Existential [] b Nothing (Just e)) = withHashtag b <+> pretty e <+> rbracket
+    pretty (Existential [x@Arg{}] b Nothing Nothing) = withHashtag b <> singleArg x <> rbracket
+    pretty (Existential bs b ty Nothing)  = withHashtag b <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <> gan ty <+> rbracket
+    pretty (Existential bs b ty (Just e)) = withHashtag b <+> mconcat (punctuate ", " (fmap go (reverse bs))) <> gan ty <+> "|" <+> pretty e <+> rbracket
+        where go (Arg (First s))  = pretty s
+              go (Arg (Both s t)) = pretty s <+> colon <+> pretty t
+              go (Arg (Second t)) = pretty t
+              go _                = undefined
+
+instance Pretty Universal where
+    pretty (Universal [x@PrfArg{}] Nothing Nothing) = lbrace <+> pretty x <+> rbrace -- FIXME universals can now be length-one arguments
+    pretty (Universal [x] Nothing Nothing) = lbrace <> singleArg x <> rbrace -- FIXME universals can now be length-one arguments
+    pretty (Universal bs ty Nothing) = lbrace <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <> gan ty <+> rbrace
+    pretty (Universal bs ty (Just e)) = lbrace <+> mconcat (punctuate ", " (fmap go (reverse bs))) <> gan ty <+> "|" <+> pretty e <+> rbrace
+        where go (Arg (First s))  = pretty s
+              go (Arg (Both s t)) = pretty s <+> colon <+> pretty t
+              go (Arg (Second t)) = pretty t
+              go _                = undefined
+
+instance Pretty ATS where
+    pretty (ATS xs) = concatSame (fmap rewriteDecl xs)
+
+instance Pretty Implementation where
+    pretty (Implement _ [] [] n [] e)  = "implement" <+> pretty n <+> "() =" <$> indent 2 (pretty e)
+    pretty (Implement _ [] [] n ias e) = "implement" <+> pretty n <+> prettyArgs ias <+> "=" <$> indent 2 (pretty e)
+    pretty (Implement _ [] us n ias e) = "implement" <+> pretty n <+> foldMap pretty us </> prettyArgs ias <+> "=" <$> indent 2 (pretty e)
+    pretty (Implement _ ps [] n ias e) = "implement" <+> foldMap pretty ps </> pretty n <+> prettyArgs ias <+> "=" <$> indent 2 (pretty e)
+    pretty (Implement _ ps us n ias e) = "implement" <+> foldMap pretty ps </> pretty n </> foldMap pretty us <+> prettyArgs ias <+> "=" <$> indent 2 (pretty e)
+
+isVal :: Declaration -> Bool
+isVal Val{}   = True
+isVal Var{}   = True
+isVal PrVal{} = True
+isVal _       = False
+
+glue :: Declaration -> Declaration -> Bool
+glue x y
+    | isVal x && isVal y = True
+glue Staload{} Staload{}           = True
+glue Include{} Include{}           = True
+glue ViewTypeDef{} ViewTypeDef{}   = True
+glue TypeDef{} TypeDef{}           = True
+glue Comment{} _                   = True
+glue (Func _ Fnx{}) (Func _ And{}) = True
+glue _ _                           = False
+
+{-# INLINE glue #-}
+
+concatSame :: [Declaration] -> Doc
+concatSame []  = mempty
+concatSame [x] = pretty x
+concatSame (x:x':xs)
+    | glue x x' = pretty x <$> concatSame (x':xs)
+    | otherwise = pretty x <> line <$> concatSame (x':xs)
+
+-- TODO - soft break
+($$) :: Doc -> Doc -> Doc
+x $$ y = align (x <$> y)
+
+lineAlt :: Doc -> Doc -> Doc
+lineAlt = group .* flatAlt
+
+showFast :: Doc -> String
+showFast d = displayS (renderCompact d) mempty
+
+prettyRecord :: (Pretty a) => [(String, a)] -> Doc
+prettyRecord es
+    | any ((>40) . length . showFast . pretty) es = prettyRecordF True es
+    | otherwise = lineAlt (prettyRecordF True es) (prettyRecordS True es)
+
+prettyRecordS :: (Pretty a) => Bool -> [(String, a)] -> Doc
+prettyRecordS _ []             = mempty
+prettyRecordS True [(s, t)]    = "@{" <+> text s <+> "=" <+> pretty t <+> "}"
+prettyRecordS _ [(s, t)]       = "@{" <+> text s <+> "=" <+> pretty t
+prettyRecordS True ((s, t):xs) = prettyRecordS False xs <> "," <+> text s <+> ("=" <+> pretty t) <+> "}"
+prettyRecordS x ((s, t):xs)    = prettyRecordS x xs <> "," <+> text s <+> ("=" <+> pretty t)
+
+prettyRecordF :: (Pretty a) => Bool -> [(String, a)] -> Doc
+prettyRecordF _ []             = mempty
+prettyRecordF True [(s, t)]    = "@{" <+> text s <+> align ("=" <+> pretty t) <+> "}"
+prettyRecordF _ [(s, t)]       = "@{" <+> text s <+> align ("=" <+> pretty t)
+prettyRecordF True ((s, t):xs) = prettyRecordF False xs $$ indent 1 ("," <+> text s <+> align ("=" <+> pretty t) <$> "}")
+prettyRecordF x ((s, t):xs)    = prettyRecordF x xs $$ indent 1 ("," <+> text s <+> align ("=" <+> pretty t))
+
+prettyDL :: [DataPropLeaf] -> Doc
+prettyDL []                               = mempty
+prettyDL [DataPropLeaf [] e Nothing]      = indent 2 ("|" <+> pretty e)
+prettyDL [DataPropLeaf [] e (Just e')]    = indent 2 ("|" <+> pretty e <+> "of" <+> pretty e')
+prettyDL (DataPropLeaf [] e Nothing:xs)   = prettyDL xs $$ indent 2 ("|" <+> pretty e)
+prettyDL (DataPropLeaf [] e (Just e'):xs) = prettyDL xs $$ indent 2 ("|" <+> pretty e <+> "of" <+> pretty e')
+prettyDL [DataPropLeaf us e Nothing]      = indent 2 ("|" <+> foldMap pretty us <+> pretty e)
+prettyDL [DataPropLeaf us e (Just e')]    = indent 2 ("|" <+> foldMap pretty us <+> pretty e <+> "of" <+> pretty e')
+prettyDL (DataPropLeaf us e Nothing:xs)   = prettyDL xs $$ indent 2 ("|" <+> foldMap pretty us <+> pretty e)
+prettyDL (DataPropLeaf us e (Just e'):xs) = prettyDL xs $$ indent 2 ("|" <+> foldMap pretty us <+> pretty e <+> "of" <+> pretty e')
+
+universalHelper :: [Universal] -> Doc
+universalHelper = mconcat . fmap pretty . reverse
+
+prettyLeaf :: [Leaf] -> Doc
+prettyLeaf []                         = mempty
+prettyLeaf [Leaf [] s [] Nothing]     = indent 2 ("|" <+> text s)
+prettyLeaf [Leaf [] s [] (Just e)]    = indent 2 ("|" <+> text s <+> "of" <+> pretty e)
+prettyLeaf (Leaf [] s [] Nothing:xs)  = prettyLeaf xs $$ indent 2 ("|" <+> text s)
+prettyLeaf (Leaf [] s [] (Just e):xs) = prettyLeaf xs $$ indent 2 ("|" <+> text s <+> "of" <+> pretty e)
+prettyLeaf [Leaf [] s as Nothing]     = indent 2 ("|" <+> text s <> prettyArgs as)
+prettyLeaf [Leaf [] s as (Just e)]    = indent 2 ("|" <+> text s <> prettyArgs as <+> "of" <+> pretty e)
+prettyLeaf (Leaf [] s as Nothing:xs)  = prettyLeaf xs $$ indent 2 ("|" <+> text s <> prettyArgs as)
+prettyLeaf (Leaf [] s as (Just e):xs) = prettyLeaf xs $$ indent 2 ("|" <+> text s <> prettyArgs as <+> "of" <+> pretty e)
+prettyLeaf [Leaf us s [] Nothing]     = indent 2 ("|" <+> universalHelper us <+> text s)
+prettyLeaf [Leaf us s [] (Just e)]    = indent 2 ("|" <+> universalHelper us <+> text s <+> "of" <+> pretty e)
+prettyLeaf (Leaf us s [] Nothing:xs)  = prettyLeaf xs $$ indent 2 ("|" <+> universalHelper us <+> text s)
+prettyLeaf (Leaf us s [] (Just e):xs) = prettyLeaf xs $$ indent 2 ("|" <+> universalHelper us <+> text s <+> "of" <+> pretty e)
+prettyLeaf [Leaf us s as Nothing]     = indent 2 ("|" <+> universalHelper us <+> text s <> prettyArgs as)
+prettyLeaf [Leaf us s as (Just e)]    = indent 2 ("|" <+> universalHelper us <+> text s <> prettyArgs as <+> "of" <+> pretty e)
+prettyLeaf (Leaf us s as Nothing:xs)  = prettyLeaf xs $$ indent 2 ("|" <+> universalHelper us <+> text s <> prettyArgs as)
+prettyLeaf (Leaf us s as (Just e):xs) = prettyLeaf xs $$ indent 2 ("|" <+> universalHelper us <+> text s <> prettyArgs as <+> "of" <+> pretty e)
+
+prettyHelper :: Doc -> [Doc] -> [Doc]
+prettyHelper _ [x]    = [x]
+prettyHelper c (x:xs) = flatAlt (" " <> x) x : fmap (c <>) xs
+prettyHelper _ x      = x
+
+prettyBody :: Doc -> Doc -> [Doc] -> Doc
+prettyBody c1 c2 [d] = c1 <> d <> c2
+prettyBody c1 c2 ds  = (c1 <>) . align . indent (-1) . cat . (<> pure c2) $ ds
+
+prettyArgsG' :: Doc -> Doc -> Doc -> [Doc] -> Doc
+prettyArgsG' c3 c1 c2 = prettyBody c1 c2 . prettyHelper c3 . reverse
+
+prettyArgsList :: Doc -> Doc -> Doc -> [Doc] -> Doc
+prettyArgsList c3 c1 c2 = prettyBody c1 c2 . va . prettyHelper c3
+
+va :: [Doc] -> [Doc]
+va = (& _tail.traverse %~ group)
+
+prettyArgsG :: Doc -> Doc -> [Doc] -> Doc
+prettyArgsG = prettyArgsG' ", "
+
+prettyArgsU :: (Pretty a) => Doc -> Doc -> [a] -> Doc
+prettyArgsU = prettyArgs' ","
+
+prettyArgs' :: (Pretty a) => Doc -> Doc -> Doc -> [a] -> Doc
+prettyArgs' = fmap pretty -.*** prettyArgsG'
+
+prettyArgs :: (Pretty a) => [a] -> Doc
+prettyArgs = prettyArgs' ", " "(" ")"
+
+fancyU :: [Universal] -> Doc
+fancyU = foldMap pretty . reverse
+
+(<#>) :: Doc -> Doc -> Doc
+(<#>) a b = lineAlt (a <$> indent 2 b) (a <+> b)
+
+-- FIXME figure out a nicer algorithm for when/how to split lines.
+-- aka don't use '</>' in places.
+instance Pretty PreFunction where
+    pretty (PreF i si [] [] [NoArgs] (Just rt) Nothing (Just e)) = pretty i <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e) -- FIXME this is an awful hack
+    pretty (PreF i si [] [] as (Just rt) Nothing (Just e)) = pretty i <> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
+    pretty (PreF i si [] [] as (Just rt) (Just t) (Just e)) = pretty i </> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
+    pretty (PreF i si [] us as (Just rt) (Just t) (Just e)) = pretty i </> fancyU us </> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
+    pretty (PreF i si [] us [NoArgs] (Just rt) Nothing (Just e)) = pretty i </> fancyU us <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
+    pretty (PreF i si [] us as (Just rt) Nothing (Just e)) = pretty i </> fancyU us </> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
+    pretty (PreF i si pus [] as (Just rt) Nothing (Just e)) = fancyU pus </> pretty i <> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
+    pretty (PreF i si pus [] as (Just rt) (Just t) (Just e)) = fancyU pus </> pretty i <+> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
+    pretty (PreF i si pus us as (Just rt) (Just t) (Just e)) = fancyU pus </> pretty i </> fancyU us </> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
+    pretty (PreF i si pus us as (Just rt) Nothing (Just e)) = fancyU pus </> pretty i </> fancyU us </> prettyArgs as <+> ":" <> text si <#> pretty rt <+> "=" <$> indent 2 (pretty e)
+    pretty (PreF i si [] [] as (Just rt) Nothing Nothing) = pretty i <> prettyArgs as <+> ":" <> text si <#> pretty rt
+    pretty (PreF i si [] us [] (Just rt) Nothing Nothing) = pretty i </> fancyU us <+> ":" <> text si <#> pretty rt
+    pretty (PreF i si [] us as (Just rt) Nothing Nothing) = pretty i </> fancyU us </> prettyArgs as <+> ":" <> text si <#> pretty rt
+    pretty (PreF i si pus us as (Just rt) Nothing Nothing) = fancyU pus </> pretty i </> fancyU us </> prettyArgs as <+> ":" <> text si <#> pretty rt
+    pretty _ = undefined
+
+instance Pretty DataPropLeaf where
+    pretty (DataPropLeaf us e Nothing)   = "|" <+> foldMap pretty (reverse us) <+> pretty e
+    pretty (DataPropLeaf us e (Just e')) = "|" <+> foldMap pretty (reverse us) <+> pretty e <+> "of" <+> pretty e'
+
+instance Pretty Declaration where
+    pretty (AbsType _ s as Nothing)        = "abstype" <+> text s <> prettyArgs as
+    pretty (AbsViewType _ s as Nothing)    = "absvtype" <+> text s <> prettyArgs as
+    pretty (AbsViewType _ s as (Just t))   = "absvtype" <+> text s <> prettyArgs as <+> "=" <+> pretty t
+    pretty (SumViewType s [] ls)           = "datavtype" <+> text s <+> "=" <$> prettyLeaf ls
+    pretty (SumViewType s as ls)           = "datavtype" <+> text s <> prettyArgs as <+> "=" <$> prettyLeaf ls
+    pretty (SumType s [] ls)               = "datatype" <+> text s <+> "=" <$> prettyLeaf ls
+    pretty (SumType s as ls)               = "datatype" <+> text s <> prettyArgs as <+> "=" <$> prettyLeaf ls
+    pretty (Impl [] i)                     = pretty i
+    pretty (PrVal p e)                     = "prval" <+> pretty p <+> "=" <+> pretty e
+    pretty (Val a Nothing p e)             = "val" <> pretty a <+> pretty p <+> "=" <+> pretty e
+    pretty (Val a (Just t) p e)            = "val" <> pretty a <+> pretty p <> ":" <+> pretty t <+> "=" <+> pretty e
+    pretty (Var (Just t) p Nothing e)      = "var" <+> pretty p <> ":" <+> pretty t <+> "with" <+> pretty e
+    pretty (Var Nothing p e Nothing)       = "var" <+> pretty p <+> "=" <+> pretty e
+    pretty (Var (Just t) p e Nothing)      = "var" <+> pretty p <> ":" <+> pretty t <+> "=" <+> pretty e
+    pretty (Include s)                     = "#include" <+> pretty s
+    pretty (Staload Nothing s)             = "staload" <+> pretty s
+    pretty (Staload (Just q) s)            = "staload" <+> pretty q <+> "=" <+> pretty s
+    pretty (CBlock s)                      = string s
+    pretty (Comment s)                     = string s
+    pretty (OverloadOp _ o n)              = "overload" <+> pretty o <+> "with" <+> pretty n
+    pretty (OverloadIdent _ i n Nothing)   = "overload" <+> text i <+> "with" <+> pretty n
+    pretty (OverloadIdent _ i n (Just n')) = "overload" <+> text i <+> "with" <+> pretty n <+> "of" <+> pretty n'
+    -- We use 'text' here, which means indentation might get fucked up for
+    -- C preprocessor macros, but you absolutely deserve it if you indent your
+    -- macros.
+    pretty (Define s)                      = text s
+    pretty (Func _ (Fn pref))              = "fn" </> pretty pref
+    pretty (Func _ (Fun pref))             = "fun" </> pretty pref
+    pretty (Func _ (CastFn pref))          = "castfn" </> pretty pref
+    pretty (Func _ (Fnx pref))             = "fnx" </> pretty pref
+    pretty (Func _ (And pref))             = "and" </> pretty pref
+    pretty (Func _ (Praxi pref))           = "praxi" </> pretty pref
+    pretty (Func _ (PrFun pref))           = "prfun" </> pretty pref
+    pretty (Func _ (PrFn pref))            = "prfn" </> pretty pref
+    pretty (Extern _ d)                    = "extern" <$> pretty d
+    pretty (DataProp _ s as ls)            = "dataprop" <+> text s <> prettyArgs as <+> "=" <$> prettyDL ls
+    pretty (ViewTypeDef _ s [] t)          = "vtypedef" <+> text s <+> "=" <#> pretty t
+    pretty (ViewTypeDef _ s as t)          = "vtypedef" <+> text s <> prettyArgs as <+> "=" <#> pretty t
+    pretty (TypeDef _ s [] t)              = "typedef" <+> text s <+> "=" <+> pretty t
+    pretty (TypeDef _ s as t)              = "typedef" <+> text s <> prettyArgs as <+> "=" <+> pretty t
+    pretty (AbsProp _ n as)                = "absprop" <+> text n <+> prettyArgs as
+    pretty (Assume n as e)                 = "assume" </> pretty n <> prettyArgs as <+> "=" </> pretty e
+    pretty (SymIntr _ n)                   = "symintr" <+> pretty n
+    pretty (Stacst _ n t Nothing)          = "stacst" </> pretty n <+> ":" </> pretty t
+    pretty (Stacst _ n t (Just e))         = "stacst" </> pretty n <+> ":" </> pretty t <+> "=" </> pretty e
+    pretty (PropDef _ s as t)              = "propdef" </> text s <+> prettyArgs as <+> "=" </> pretty t
+    pretty (Local _ d d')                  = "local" <$> indent 2 (pretty d) <$> "in" <$> indent 2 (pretty d') <$> "end"
+    pretty _                               = undefined
diff --git a/src/Language/ATS/Types.hs b/src/Language/ATS/Types.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/ATS/Types.hs
@@ -0,0 +1,361 @@
+{-# LANGUAGE DeriveAnyClass             #-}
+{-# LANGUAGE DeriveDataTypeable         #-}
+{-# LANGUAGE DeriveFoldable             #-}
+{-# LANGUAGE DeriveFunctor              #-}
+{-# LANGUAGE DeriveGeneric              #-}
+{-# LANGUAGE DeriveTraversable          #-}
+{-# LANGUAGE DerivingStrategies         #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE LambdaCase                 #-}
+{-# LANGUAGE TemplateHaskell            #-}
+{-# LANGUAGE TypeFamilies               #-}
+
+-- | This is a module containing types to model the ATS syntax tree. As it is
+-- collapsed by the pretty printer, you may see that in some places it is
+-- focused on the lexical side of things.
+module Language.ATS.Types
+    ( ATS (..)
+    , Declaration (..)
+    , Type (..)
+    , Name (..)
+    , Pattern (..)
+    , PatternF (..)
+    , Arg (..)
+    , Universal (..)
+    , Function (..)
+    , Expression (..)
+    , ExpressionF (..)
+    , Implementation (..)
+    , BinOp (..)
+    , UnOp (..)
+    , TypeF (..)
+    , Existential (..)
+    , LambdaType (..)
+    , Addendum (..)
+    , DataPropLeaf (..)
+    , PreFunction (..)
+    , Paired (..)
+    , Leaf (..)
+    , StaticExpression (..)
+    , StaticExpressionF (..)
+    , Fixity (..)
+    , StackFunction (..)
+    , rewriteATS
+    , rewriteDecl
+    -- * Lenses
+    , leaves
+    , constructorUniversals
+    ) where
+
+import           Control.DeepSeq          (NFData)
+import           Control.Lens
+import           Data.Functor.Foldable    (ListF (Cons), ana, cata, embed, project)
+import           Data.Functor.Foldable.TH (makeBaseFunctor)
+import           Data.Maybe               (isJust)
+import           Data.Semigroup           (Semigroup)
+import           GHC.Generics             (Generic)
+import           Language.ATS.Lexer       (Addendum (..), AlexPosn)
+
+data Fixity = RightFix AlexPosn
+            | LeftFix AlexPosn
+            | Pre AlexPosn
+            | Post AlexPosn
+            deriving (Show, Eq, Generic, NFData)
+
+-- | Newtype wrapper containing a list of declarations
+newtype ATS = ATS { unATS :: [Declaration] }
+    deriving (Show, Eq, Generic)
+    deriving newtype (NFData, Semigroup, Monoid)
+
+data Leaf = Leaf { _constructorUniversals :: [Universal], name :: String, constructorArgs :: [String], maybeType :: Maybe Type }
+    deriving (Show, Eq, Generic, NFData)
+
+-- | Declare something in a scope (a function, value, action, etc.)
+data Declaration = Func AlexPosn Function
+                 | Impl [Arg] Implementation
+                 | ProofImpl Implementation -- primplmnt -- TODO add args
+                 | Val Addendum (Maybe Type) Pattern Expression
+                 | StaVal [Universal] String Type
+                 | PrVal Pattern Expression
+                 | Var (Maybe Type) Pattern (Maybe Expression) (Maybe Expression) -- TODO AlexPosn
+                 | AndDecl (Maybe Type) Pattern Expression
+                 | Include String
+                 | Staload (Maybe String) String
+                 | Stadef String Name [Type]
+                 | CBlock String
+                 | TypeDef AlexPosn String [Arg] Type
+                 | ViewTypeDef AlexPosn String [Arg] Type
+                 | SumType { typeName :: String, typeArgs :: [Arg], _leaves :: [Leaf] }
+                 | SumViewType { typeName :: String, typeArgs :: [Arg], _leaves :: [Leaf] }
+                 | AbsType AlexPosn String [Arg] (Maybe Type)
+                 | AbsViewType AlexPosn String [Arg] (Maybe Type)
+                 | AbsView AlexPosn String [Arg] (Maybe Type)
+                 | AbsVT0p AlexPosn String [Arg] (Maybe Type)
+                 | AbsT0p AlexPosn String Type
+                 | ViewDef AlexPosn String [Arg] Type
+                 | OverloadOp AlexPosn BinOp Name
+                 | OverloadIdent AlexPosn String Name (Maybe Int)
+                 | Comment String
+                 | DataProp AlexPosn String [Arg] [DataPropLeaf]
+                 | Extern AlexPosn Declaration
+                 | Define String
+                 | SortDef AlexPosn String Type
+                 | AndD Declaration Declaration
+                 | Local AlexPosn ATS ATS
+                 | AbsProp AlexPosn String [Arg]
+                 | Assume Name [Arg] Expression
+                 | TKind AlexPosn Name String
+                 | SymIntr AlexPosn Name
+                 | Stacst AlexPosn Name Type (Maybe Expression)
+                 | PropDef AlexPosn String [Arg] Type
+                 -- uses an 'Int' because you fully deserve what you get if your
+                 -- fixity declarations overflow.
+                 | FixityDecl Fixity (Maybe Int) [String]
+                 deriving (Show, Eq, Generic, NFData)
+
+data DataPropLeaf = DataPropLeaf [Universal] Expression (Maybe Expression)
+                  deriving (Show, Eq, Generic, NFData)
+
+-- | A type for parsed ATS types
+data Type = Bool
+          | Void
+          | String
+          | Char
+          | Int
+          | Nat
+          | Addr
+          | DependentInt StaticExpression
+          | DependentBool StaticExpression
+          | DepString StaticExpression
+          | Double
+          | Float
+          | Tuple AlexPosn [Type]
+          | Named Name
+          | Ex Existential Type
+          | ForA Universal Type
+          | Dependent Name [Type]
+          | Unconsumed Type -- !a
+          | AsProof Type (Maybe Type) -- a >> b
+          | FromVT Type -- For a viewtype VT, we can prove there exist a view V and type T such that `VT` is equivalent to `(V | T)` - that T is `VT?!`
+          | MaybeVal Type -- This is just `a?` or the like
+          | T0p Addendum -- t@ype
+          | Vt0p Addendum -- vt@ype
+          | At AlexPosn (Maybe Type) Type
+          | ProofType AlexPosn Type Type -- Aka (prf | val)
+          | ConcreteType StaticExpression
+          | RefType Type
+          | ViewType AlexPosn Type
+          | FunctionType String Type Type
+          | NoneType AlexPosn
+          | ImplicitType AlexPosn
+          | ViewLiteral Addendum
+          | AnonymousRecord AlexPosn [(String, Type)]
+          deriving (Show, Eq, Generic, NFData)
+
+-- | A type for the various lambda arrows (@=>@, @=\<cloref1>@, etc.)
+data LambdaType = Plain AlexPosn
+                | Full AlexPosn String
+                | Spear AlexPosn
+                deriving (Show, Eq, Generic, NFData)
+
+-- | A name can be qualified (@$UN.unsafefn@) or not
+data Name = Unqualified String
+          | Qualified AlexPosn String String
+          | SpecialName AlexPosn String
+          | Functorial String String
+          | Unnamed AlexPosn
+          deriving (Show, Eq, Generic, NFData)
+
+-- | A data type for patterns.
+data Pattern = Wildcard AlexPosn
+             | PName String [Pattern]
+             | PSum String Pattern
+             | PLiteral Expression
+             | Guarded AlexPosn Expression Pattern
+             | Free Pattern
+             | Proof AlexPosn [Pattern] [Pattern]
+             | TuplePattern [Pattern]
+             | AtPattern AlexPosn Pattern
+             | UniversalPattern AlexPosn String [Universal] Pattern
+             | ExistentialPattern Existential Pattern
+             deriving (Show, Eq, Generic, NFData)
+
+data Paired a b = Both a b
+                | First a
+                | Second b
+                deriving (Show, Eq, Generic, NFData)
+
+-- | An argument to a function.
+data Arg = Arg (Paired String Type)
+         | PrfArg Arg Arg
+         | NoArgs
+    deriving (Show, Eq, Generic, NFData)
+
+-- | Wrapper for universal quantifiers (refinement types)
+data Universal = Universal { bound :: [Arg], typeU :: Maybe Type, prop :: Maybe StaticExpression } -- TODO NonEmpty type?
+    deriving (Show, Eq, Generic, NFData)
+
+-- | Wrapper for existential quantifiers/types
+data Existential = Existential { boundE :: [Arg], isOpen :: Bool, typeE :: Maybe Type, propE :: Maybe StaticExpression }
+    deriving (Show, Eq, Generic, NFData)
+
+-- | @~@ is used to negate numbers in ATS
+data UnOp = Negate
+    deriving (Show, Eq, Generic, NFData)
+
+-- | Binary operators on expressions
+data BinOp = Add
+           | Mult
+           | Div
+           | Sub
+           | GreaterThan
+           | GreaterThanEq
+           | LessThan
+           | LessThanEq
+           | Equal
+           | NotEqual
+           | LogicalAnd
+           | LogicalOr
+           | StaticEq
+           | Mod
+           deriving (Show, Eq, Generic, NFData)
+
+-- FIXME add position information?
+data StaticExpression = StaticVal Name
+                      | StaticBinary BinOp StaticExpression StaticExpression
+                      | StaticInt Int
+                      | SPrecede StaticExpression StaticExpression
+                      | StaticBool Bool
+                      | StaticVoid AlexPosn
+                      | Sif { scond :: StaticExpression, wwhenTrue :: StaticExpression, selseExpr :: StaticExpression } -- Static if (for proofs)
+                      | SCall Name [StaticExpression]
+                      deriving (Show, Eq, Generic, NFData)
+
+-- | A (possibly effectful) expression.
+data Expression = Let AlexPosn ATS (Maybe Expression)
+                | VoidLiteral -- The '()' literal representing inaction.
+                    AlexPosn
+                -- function call: <a>, then {n}
+                | Call Name [Type] [Type] (Maybe Expression) [Expression]
+                | NamedVal Name
+                | ListLiteral AlexPosn String Type [Expression]
+                | If { cond     :: Expression -- ^ Expression evaluating to a boolean value
+                     , whenTrue :: Expression -- ^ Expression to be returned when true
+                     , elseExpr :: Maybe Expression -- ^ Expression to be returned when false
+                     }
+                | BoolLit Bool
+                | TimeLit String
+                | FloatLit Float
+                | IntLit Int
+                | UnderscoreLit AlexPosn
+                | Lambda AlexPosn LambdaType Pattern Expression
+                | LinearLambda AlexPosn LambdaType Pattern Expression
+                | Index AlexPosn Name Expression
+                | Access AlexPosn Expression Name
+                | StringLit String
+                | CharLit Char
+                | AtExpr Expression Expression
+                | AddrAt AlexPosn Expression
+                | ViewAt AlexPosn Expression
+                | Binary BinOp Expression Expression
+                | Unary UnOp Expression
+                | Case { posE :: AlexPosn
+                       , kind :: Addendum
+                       , val  :: Expression
+                       , arms :: [(Pattern, LambdaType, Expression)] -- ^ Each @(Pattern, Expression)@ pair corresponds to a branch of the 'case' statement
+                       }
+                | RecordValue AlexPosn [(String, Expression)] (Maybe Type)
+                | Precede Expression Expression
+                | FieldMutate { posE  :: AlexPosn
+                              , old   :: Expression -- ^ Record to modify
+                              , field :: String -- ^ Field being modified
+                              , new   :: Expression -- ^ New value of the field
+                              }
+                | Mutate Expression Expression
+                | Deref AlexPosn Expression
+                | ProofExpr AlexPosn Expression Expression
+                | TypeSignature Expression Type
+                | WhereExp Expression [Declaration]
+                | TupleEx AlexPosn [Expression]
+                | While AlexPosn Expression Expression
+                | Actions ATS
+                | Begin AlexPosn Expression
+                | BinList { _op :: BinOp, _exprs :: [Expression] }
+                | PrecedeList { _exprs :: [Expression] }
+                | FixAt String StackFunction
+                | LambdaAt StackFunction
+                | ParenExpr AlexPosn Expression
+                deriving (Show, Eq, Generic, NFData)
+
+-- | An 'implement' declaration
+data Implementation = Implement { pos            :: AlexPosn
+                                , preUniversalsI :: [Universal]
+                                , universalsI    :: [Universal] -- ^ Universal quantifiers
+                                , nameI          :: Name -- ^ Name of the template being implemented
+                                , iArgs          :: [Arg] -- ^ Arguments
+                                , iExpression    :: Expression -- ^ Expression holding the function body.
+                                }
+    deriving (Show, Eq, Generic, NFData)
+
+-- | A function declaration accounting for all three keywords (???) ATS uses to
+-- define them.
+data Function = Fun PreFunction
+              | Fn PreFunction
+              | Fnx PreFunction
+              | And PreFunction
+              | PrFun PreFunction
+              | PrFn PreFunction
+              | Praxi PreFunction
+              | CastFn PreFunction
+              deriving (Show, Eq, Generic, NFData)
+
+data StackFunction = StackF { stSig        :: String
+                            , stArgs       :: [Arg]
+                            , stReturnType :: Type
+                            , stExpression :: Expression
+                            }
+                            deriving (Show, Eq, Generic, NFData)
+
+data PreFunction = PreF { fname         :: Name -- ^ Function name
+                        , sig           :: String -- ^ e.g. <> or \<!wrt>
+                        , preUniversals :: [Universal] -- ^ Universal quantifiers making a function generic
+                        , universals    :: [Universal] -- ^ Universal quantifiers/refinement type
+                        , args          :: [Arg] -- ^ Actual function arguments
+                        , returnType    :: Maybe Type -- ^ Return type
+                        , termetric     :: Maybe StaticExpression -- ^ Optional termination metric
+                        , expression    :: Maybe Expression -- ^ Expression holding the actual function body (not present in static templates)
+                        }
+                        deriving (Show, Eq, Generic, NFData)
+
+makeBaseFunctor ''Pattern
+makeBaseFunctor ''Expression
+makeBaseFunctor ''StaticExpression
+makeBaseFunctor ''Type
+makeLenses ''Leaf
+makeLenses ''Declaration
+
+rewriteDecl :: Declaration -> Declaration
+rewriteDecl x@SumViewType{} = g x
+    where g = over (leaves.mapped.constructorUniversals) h
+          h :: [Universal] -> [Universal]
+          h = ana c where
+            c (y:y':ys)
+                | typeU y == typeU y' && isJust (typeU y) =
+                    Cons (Universal (bound y ++ bound y') (typeU y) (StaticBinary LogicalAnd <$> prop y <*> prop y')) ys
+            c y = project y
+rewriteDecl x = x
+
+-- precedence: rewrite n + 2 * x to n + (2 * x)
+-- TODO: rewrite multiple universals when it's the right context?
+rewriteATS :: Expression -> Expression
+rewriteATS = cata a where
+    a (CallF n ts ts' me [ParenExpr _ e@NamedVal{}]) = Call n ts ts' me [e]
+    a (CallF n ts ts' me [ParenExpr _ e@Call{}])     = Call n ts ts' me [e]
+    a (PrecedeF e e'@PrecedeList{})                  = PrecedeList (e : _exprs e')
+    a (PrecedeF e e')                                = PrecedeList [e, e']
+    a (BinaryF Mult (Binary Add e e') e'')           = Binary Add e (Binary Mult e' e'')
+    a (BinaryF Add e (BinList Add es))               = BinList Add (e : es)
+    a (BinaryF Add e e')                             = BinList Add [e, e']
+    a (ParenExprF _ e@Precede{})                     = e
+    a (ParenExprF _ e@PrecedeList{})                 = e
+    a x                                              = embed x
diff --git a/stack.yaml b/stack.yaml
new file mode 100644
--- /dev/null
+++ b/stack.yaml
@@ -0,0 +1,9 @@
+---
+resolver: lts-10.3
+packages:
+  - '.'
+extra-deps: []
+flags:
+  language-ats:
+    development: false
+extra-package-dbs: []
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+import qualified Filesystem.Path.CurrentOS as F
+import           Language.ATS
+import           Test.Hspec
+import           Test.Hspec.Dirstream
+
+isATS :: F.FilePath -> Bool
+isATS x = (extension x `elem`) (pure <$> ["ats", "dats", "sats", "hats", "cats"])
+
+main :: IO ()
+main = hspec $
+    describe "pretty-print" $ parallel $
+        testFiles "test/data" isATS (fmap printATS . parseATS . lexATS)