diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -5,5 +5,5 @@
 [haskell-src-exts](http://hackage.haskell.org/package/haskell-src-exts) that
 provides a parser and pretty-printer for [ATS](http://ats-lang.org/).
 
-The parser is slightly buggy but it can handle most of the language; see
+The parser is slightly buggy but it can handle almost all of the language; see
 the `test/data` directory for examples of what it can handle.
diff --git a/language-ats.cabal b/language-ats.cabal
--- a/language-ats.cabal
+++ b/language-ats.cabal
@@ -1,5 +1,5 @@
 name:                language-ats
-version:             1.0.0.0
+version:             1.0.1.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.
 license:             BSD3
@@ -36,6 +36,9 @@
                      , recursion-schemes
                      , composition-prelude
                      , ansi-terminal
+                     , containers
+                     , mtl
+                     , transformers
   default-language:    Haskell2010
   build-tools:         happy
                      , alex
diff --git a/src/Language/ATS.hs b/src/Language/ATS.hs
--- a/src/Language/ATS.hs
+++ b/src/Language/ATS.hs
@@ -4,6 +4,7 @@
 module Language.ATS ( -- * Functions for working with syntax
                       lexATS
                     , parse
+                    , parseWithCtx
                     , printATS
                     , printATSCustom
                     , printATSFast
@@ -36,6 +37,8 @@
                     , SortArg (..)
                     , Sort (..)
                     , SortArgs
+                    -- * Parser State
+                    , FixityState
                     -- * Lexical types
                     , Token (..)
                     , AlexPosn (..)
@@ -55,7 +58,7 @@
 import           Control.Lens
 import           Control.Monad
 import           Control.Monad.IO.Class
-import           Data.Maybe                   (catMaybes)
+import           Control.Monad.Trans.State
 import           GHC.IO.Handle.FD             (stderr)
 import           Language.ATS.Lexer
 import           Language.ATS.Parser
@@ -63,8 +66,8 @@
 import           Language.ATS.Types
 import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
 
-rewriteATS' :: Eq a => ATS a -> ATS a
-rewriteATS' (ATS ds) = ATS (rewriteDecl <$> ds)
+rewriteATS' :: Eq a => (ATS a, FixityState a) -> ATS a
+rewriteATS' (ATS ds, st) = ATS (rewriteDecl st <$> ds)
 
 -- | Print an error message to standard error.
 printErr :: MonadIO m => ATSError -> m ()
@@ -72,12 +75,19 @@
 
 -- | Parse a string containing ATS source.
 parse :: String -> Either ATSError (ATS AlexPosn)
-parse = fmap rewriteATS' . (parseATS <=< (over _Left LexError . lexATS))
+parse = parseWithCtx mempty
 
+-- | Parse with some fixity declarations already in scope.
+parseWithCtx :: FixityState AlexPosn -> String -> Either ATSError (ATS AlexPosn)
+parseWithCtx st = stateParse <=< lexErr
+    where withSt = flip runStateT st
+          lexErr = over _Left LexError . lexATS
+          stateParse = fmap rewriteATS' . withSt . parseATS
+
 -- | Extract a list of files that some code depends on.
 getDependencies :: ATS a -> [FilePath]
-getDependencies (ATS ds) = join $ catMaybes (g <$> ds)
-    where g (Staload _ _ s)  = Just [s]
-          g (Include s)      = Just [s]
-          g (Local _ as as') = Just $ getDependencies as <> getDependencies as'
-          g _                = Nothing
+getDependencies (ATS ds) = g =<< ds
+    where g (Staload _ _ s)  = [s]
+          g (Include s)      = [s]
+          g (Local _ as as') = foldMap getDependencies [as, as']
+          g _                = mempty
diff --git a/src/Language/ATS/Lexer.x b/src/Language/ATS/Lexer.x
--- a/src/Language/ATS/Lexer.x
+++ b/src/Language/ATS/Lexer.x
@@ -121,7 +121,7 @@
     <two> @comment_in+ / [^\)]   { tok (\p s -> alex $ CommentContents p s) }
     <two> @comment_general       { tok (\p s -> alex $ CommentContents p s) }
     <three> @block_comment_end   { tok (\p s -> alex $ CommentContents p s) `andBegin` two }
-    <three> @block_comment_start { tok (\_ _ -> alexError "Nested comments of depth >3 are not supported.") }
+    <three> @block_comment_start { tok (\_ _ -> alexError "Nested comments of depth > 3 are not supported.") }
     <three> [^\*\(\)\/]+         { tok (\p s -> alex $ CommentContents p s) }
     <three> @comment_in+ / [^\)] { tok (\p s -> alex $ CommentContents p s) }
     <three> @comment_general     { tok (\p s -> alex $ CommentContents p s) }
diff --git a/src/Language/ATS/Parser.y b/src/Language/ATS/Parser.y
--- a/src/Language/ATS/Parser.y
+++ b/src/Language/ATS/Parser.y
@@ -20,6 +20,10 @@
                           , get_staload
                           )
 
+import qualified Data.Map as M
+import Control.Monad.Trans.Class
+import Control.Monad.Trans.State
+import Control.Composition
 import Data.Char (toLower)
 import Control.DeepSeq (NFData)
 import Control.Lens (over, _head)
@@ -32,8 +36,28 @@
 %name parseATS
 %tokentype { Token }
 %error { parseError }
-%monad { Either ATSError } { (>>=) } { pure }
+%monad { ParseSt } { (>>=) } { pure }
 
+%left plus
+%left minus
+%left mult
+%left div
+%left mod
+%left percent
+%left andOp
+%left or
+%right at
+%right in
+%right mutateArrow
+%nonassoc lbracket
+%nonassoc rbrakcet
+%nonassoc neq
+%nonassoc doubleEq
+%nonassoc doubleBrackets
+%nonassoc leq
+%nonassoc geq
+%nonassoc mutateEq
+
 %token
     fun { Keyword $$ KwFun }
     fn { Keyword $$ KwFn }
@@ -231,13 +255,14 @@
      | openParen TypeIn vbar Type closeParen { ProofType $1 $2 $4 } -- FIXME can have multiple first parts
      | identifierSpace identifier { Dependent (Unqualified $ to_string $1) [Named (Unqualified $ to_string $2)] }
      | openParen TypeIn closeParen { Tuple $1 $2 }
-     | openParen TypeIn rbrace {% Left $ Expected $3 ")" "}" }
+     | openParen TypeIn rbrace {% left $ Expected $3 ")" "}" }
      | openParen Type closeParen { ParenType $1 $2 }
      | doubleParens { NoneType $1 }
-     | minus {% Left $ Expected $1 "Type" "-" }
-     | dollar {% Left $ Expected $1 "Type" "$" }
-     | identifierSpace identifier openParen {% Left $ Expected (token_posn $2) "Static integer expression" (to_string $2) }
-     | Type identifierSpace {% Left $ Expected (token_posn $2) "," (to_string $2) }
+     | Type where PreFunction { WhereType $2 $1 $3 }
+     | minus {% left $ Expected $1 "Type" "-" }
+     | dollar {% left $ Expected $1 "Type" "$" }
+     | identifierSpace identifier openParen {% left $ Expected (token_posn $2) "Static integer expression" (to_string $2) }
+     | Type identifierSpace {% left $ Expected (token_posn $2) "," (to_string $2) }
 
 FullArgs : Args { $1 }
 
@@ -287,8 +312,8 @@
         | 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" "+" }
+        | minus {% left $ Expected $1 "Pattern" "-" }
+        | plus {% left $ Expected $1 "Pattern" "+" }
 
 -- | Parse a case expression
 Case : vbar Pattern CaseArrow Expression { [($2, $3, $4)] }
@@ -312,17 +337,17 @@
 -- | 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" "-" }
+          | 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" ")" }
+            | 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] }
@@ -335,8 +360,8 @@
            | 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 } -- TODO is this legal??
-           | begin Expression extern {% Left $ Expected $3 "end" "extern" }
-           | Expression prfTransform underscore {% Left $ Expected $2 "Rest of expression or declaration" ">>" }
+           | 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 }
@@ -355,8 +380,8 @@
      | Name Implicits openParen ExpressionPrf closeParen { Call $1 $2 [] (fst $4) (snd $4) }
      | Name Implicits { Call $1 $2 [] 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"}
+     | Name openParen ExpressionPrf end {% left $ Expected $4 ")" "end"}
+     | Name openParen ExpressionPrf else {% left $ Expected $4 ")" "else"}
 
 StaticArgs : StaticExpression { [$1] }
            | StaticArgs comma StaticExpression { $3 : $1 }
@@ -397,7 +422,7 @@
               | 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" "|" }
+              | 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 }
@@ -412,29 +437,29 @@
               | lineComment PreExpression { CommentExpr (to_string $1) $2 }
               | comma openParen identifier closeParen { MacroVar $1 (to_string $3) }
               | PreExpression where lbrace ATS rbrace { WhereExp $1 $4 }
-              | include {% Left $ Expected $1 "Expression" "include" }
-              | staload {% Left $ Expected (token_posn $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 else {% Left $ Expected $5 "end" "else" }
-              | let ATS in Expression fun {% Left $ Expected $5 "end" "fun" }
-              | let ATS in Expression vtypedef {% Left $ Expected $5 "end" "vtypedef" }
-              | let ATS in Expression implement {% Left $ Expected $5 "end" "implement" }
-              | let ATS in Expression semicolon {% Left $ Expected $5 "end" ";" }
-              | let ATS if {% Left $ Expected $3 "in" "if" }
-              | if Expression then Expression else else {% Left $ Expected $6 "Expression" "else" }
+              | include {% left $ Expected $1 "Expression" "include" }
+              | staload {% left $ Expected (token_posn $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 else {% left $ Expected $5 "end" "else" }
+              | let ATS in Expression fun {% left $ Expected $5 "end" "fun" }
+              | let ATS in Expression vtypedef {% left $ Expected $5 "end" "vtypedef" }
+              | let ATS in Expression implement {% left $ Expected $5 "end" "implement" }
+              | let ATS in Expression semicolon {% left $ Expected $5 "end" ";" }
+              | let ATS if {% left $ Expected $3 "in" "if" }
+              | 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" }
+          | underscore {% left $ Expected $1 "_" "Termination metric" }
+          | dollar {% left $ Expected $1 "$" "Termination metric" }
 
 
 Sort : t0pPlain { T0p None }
@@ -504,7 +529,7 @@
      | dollar identifier dot identifierSpace { Qualified $1 (to_string $4) (to_string $2) }
      | dollar identifier dot identifier dollar IdentifierOr { Qualified $1 (to_string $4 ++ ('$' : $6)) (to_string $2) }
      | specialIdentifier { SpecialName (token_posn $1) (to_string $1) }
-     | dollar {% Left $ Expected $1 "Name" "$" }
+     | dollar {% left $ Expected $1 "Name" "$" }
 
 -- | Parse a list of values in a record
 RecordVal : IdentifierOr eq Expression { [($1, $3)] }
@@ -534,7 +559,7 @@
        | Universals identifierSpace of Type { [Leaf $1 (to_string $2) [] (Just $4)] }
        | Universals identifier { [Leaf $1 (to_string $2) [] Nothing] }
        | Universals identifier openParen StaticExpressionsIn closeParen OfType { [Leaf $1 (to_string $2) $4 $6] } -- FIXME should take any static expression.
-       | dollar {% Left $ Expected $1 "|" "$" }
+       | dollar {% left $ Expected $1 "|" "$" }
 
 Universals : { [] }
            | doubleBraces { [] }
@@ -547,6 +572,7 @@
 -- | Parse a unary operator
 UnOp : tilde { Negate }
      | exclamation { Deref }
+     | customOperator { SpecialOp (token_posn $1) (to_string $1) }
 
 -- | Parse a binary operator
 BinOp : plus { Add }
@@ -557,7 +583,7 @@
       | leq { LessThanEq }
       | lbracket { LessThan }
       | rbracket { GreaterThan }
-      | neq { NotEqual }
+      | neq { NotEq }
       | andOp { LogicalAnd }
       | or { LogicalOr }
       | doubleEq { StaticEq }
@@ -573,11 +599,11 @@
 -- | Optionally parse a function body
 OptExpression : { Nothing }
               | eq Expression { Just $2 } -- FIXME only let this happen for external declarations (?)
-              | let {% Left $ Expected $1 "=" "let" } -- TODO is this actually a good idea?
-              | ifcase {% Left $ Expected $1 "=" "ifcase" }
-              | eq fun {% Left $ Expected $2 "Expression" "=" }
-              | eq lineComment fun {% Left $ Expected $3 "Expression" "=" }
-              | lbrace {% Left $ Expected $1 "Expression" "{" }
+              | let {% left $ Expected $1 "=" "let" } -- TODO is this actually a good idea?
+              | ifcase {% left $ Expected $1 "=" "ifcase" }
+              | eq fun {% left $ Expected $2 "Expression" "=" }
+              | eq lineComment fun {% left $ Expected $3 "Expression" "=" }
+              | lbrace {% left $ Expected $1 "Expression" "{" }
 
 -- | Parse a constructor for a 'dataprop'
 DataPropLeaf : vbar Universals Expression { DataPropLeaf $2 $3 Nothing }
@@ -590,44 +616,43 @@
                | DataPropLeaves DataPropLeaf { $2 : $1 }
                | lineComment { [] }
                | DataPropLeaves lineComment { $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" "?" }
+               | 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 }
+OptType : Signature Type { Just ($1, $2) }
         | { 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 doubleParens Signature OptType OptExpression { PreF $2 $6 $1 $3 [] $7 $4 $8 }
-            | 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" "[" }
+PreFunction : FunName openParen FullArgs closeParen OptType OptExpression { (PreF $1 (fmap fst $5) [] [] $3 (fmap snd $5) Nothing $6) }
+            | FunName Universals OptTermetric OptType OptExpression { PreF $1 (fmap fst $4) [] $2 [NoArgs] (fmap snd $4) $3 $5 }
+            | FunName Universals OptTermetric doubleParens OptType OptExpression { PreF $1 (fmap fst $5) [] $2 [] (fmap snd $5) $3 $6 }
+            | FunName Universals OptTermetric openParen FullArgs closeParen OptType OptExpression { PreF $1 (fmap fst $7) [] $2 $5 (fmap snd $7) $3 $8 }
+            | Universals FunName Universals OptTermetric openParen FullArgs closeParen OptType OptExpression { PreF $2 (fmap fst $8) $1 $3 $6 (fmap snd $8) $4 $9 }
+            | Universals FunName Universals OptTermetric doubleParens OptType OptExpression { PreF $2 (fmap fst $6) $1 $3 [] (fmap snd $6) $4 $7 }
+            | Universals FunName Universals OptTermetric OptType OptExpression { PreF $2 (fmap fst $5) $1 $3 [] (fmap snd $5) $4 $6 }
+            | 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 Sort { AndD $1 (SortDef $2 $3 (Left $5)) } -- TODO figure out if this is building up the slow way
         | sortdef IdentifierOr eq Sort { SortDef $1 $2 (Left $4) }
         | sortdef IdentifierOr eq Universal { SortDef $1 $2 (Right $4) }
 
--- Feb. 15th 2pm
 AndStadef : stadef IdentifierOr SortArgs eq Type { Stadef $2 $3 $5 }
           | AndStadef and IdentifierOr SortArgs eq Type { AndD $1 (Stadef $3 $4 $6) }
 
@@ -638,22 +663,22 @@
 FunDecl : fun PreFunction { [ Func $1 (Fun $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 identifier {% left $ Expected (token_posn $3) "=" (to_string $3) }
         | fn PreFunction { [ Func $1 (Fn $2) ] }
         | FunDecl and PreFunction { Func $2 (And $3) : $1 }
         | StafunDecl { [$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) }
-        | extern identifier {% Left $ Expected (token_posn $2) "Declaration" (to_string $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) }
+        | extern identifier {% left $ Expected (token_posn $2) "Declaration" (to_string $2) }
 
 IdentifierOr : identifier { to_string $1 }
              | identifierSpace { to_string $1 }
@@ -697,13 +722,13 @@
          | absprop IdentifierOr openParen FullArgs closeParen { AbsProp $1 $2 $4 }
          | AndSort { $1 }
          | AndStadef { $1 }
-         | extern typedef {% Left $ Expected $2 "external declaration" "typedef" }
-         | vtypedef IdentifierOr SortArgs eq vbar {% Left $ Expected $5 "Viewtype" "|" }
-         | typedef IdentifierOr SortArgs eq vbar {% Left $ Expected $5 "Type" "|" }
-         | datavtype IdentifierOr SortArgs vbar {% Left $ Expected $4 "=" "|" }
-         | datatype IdentifierOr SortArgs vbar {% Left $ Expected $4 "=" "|" }
-         | dataview IdentifierOr SortArgs vbar {% Left $ Expected $4 "=" "|" }
-         | dataprop IdentifierOr SortArgs vbar {% Left $ Expected $4 "=" "|" }
+         | extern typedef {% left $ Expected $2 "external declaration" "typedef" }
+         | vtypedef IdentifierOr SortArgs eq vbar {% left $ Expected $5 "Viewtype" "|" }
+         | typedef IdentifierOr SortArgs eq vbar {% left $ Expected $5 "Type" "|" }
+         | datavtype IdentifierOr SortArgs vbar {% left $ Expected $4 "=" "|" }
+         | datatype IdentifierOr SortArgs vbar {% left $ Expected $4 "=" "|" }
+         | dataview IdentifierOr SortArgs vbar {% left $ Expected $4 "=" "|" }
+         | dataprop IdentifierOr SortArgs vbar {% left $ Expected $4 "=" "|" }
 
 Fixity : infixr intLit { RightFix $1 $2 }
        | infixl intLit { LeftFix $1 $2 }
@@ -726,7 +751,7 @@
         | val Pattern eq Expression { [ Val (get_addendum $1) Nothing $2 $4 ] }
         | ValDecl and Pattern eq Expression { Val None Nothing $3 $5 : $1 }
         | extern ValDecl { over _head (Extern $1) $2 }
-        | val Pattern eq colon {% Left $ Expected $4 "Expression" ":" }
+        | val Pattern eq colon {% left $ Expected $4 "Expression" ":" }
 
 StaticDeclaration : prval Pattern eq Expression { PrVal $2 $4 }
                   | praxi PreFunction { Func $1 (Praxi $2) }
@@ -768,8 +793,8 @@
             | var Pattern colon Type eq PreExpression { Var (Just $4) $2 (Just $6) Nothing }
             | 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 }
+            | var Pattern eq fixAt IdentifierOr StackFunction { Var Nothing $2 (Just $ FixAt $4 $5 $6) Nothing }
+            | var Pattern eq lamAt StackFunction { Var Nothing $2 (Just $ LambdaAt $4 $5) Nothing }
             | implement FunArgs Implementation { Impl $2 $3 }
             | StaticDeclaration { $1 }
             | overload BinOp with Name { OverloadOp $1 $2 $4 Nothing }
@@ -792,20 +817,27 @@
             | propdef IdentifierOr openParen Args closeParen eq Type { PropDef $1 $2 $4 $7 }
             | exception identifierSpace of doubleParens { Exception (to_string $2) (Tuple $4 mempty) }
             | exception identifierSpace of openParen Type closeParen { Exception (to_string $2) (Tuple $4 [$5]) }
-            | Fixity Operators { FixityDecl $1 $2 }
+            | Fixity Operators {% addSt $1 $2 }
             | 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) }
-            | identifierSpace {% Left $ Expected (token_posn $1) "Declaration" (to_string $1) }
+            | 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) }
+            | identifierSpace {% left $ Expected (token_posn $1) "Declaration" (to_string $1) }
+            | where {% left $ Expected $1 "Declaration" "where" }
 
 {
 
+type ParseSt a = StateT (FixityState AlexPosn) (Either ATSError) a
+
+addSt :: Fixity AlexPosn -> [String] -> ParseSt (Declaration AlexPosn)
+addSt x keys = modify (thread inserts) >> pure (FixityDecl x keys)
+    where inserts = flip M.insert x <$> keys
+
 data ATSError = Expected AlexPosn String String
               | Unknown Token
               | LexError String
@@ -814,13 +846,21 @@
 instance Pretty AlexPosn where
     pretty (AlexPn _ line col) = pretty line <> ":" <> pretty col
 
+unmatched :: AlexPosn -> String -> Doc
+unmatched l chr = red "Error:" <+> "unmatched" <+> squotes (text chr) <+> "at" <+> pretty l <> linebreak 
+
 instance Pretty ATSError where
     pretty (Expected p s1 s2) = red "Error: " <> pretty p <> linebreak <> (indent 2 $ "Unexpected" <+> squotes (text s2) <> ", expected:" <+> squotes (text s1)) <> linebreak
-    pretty (Unknown (Special l ")")) = red "Error:" <+> "unmatched ')' at" <+> pretty l <> linebreak 
+    pretty (Unknown (Special l ")")) = unmatched l ")" 
+    pretty (Unknown (Special l "}")) = unmatched l "}"
+    pretty (Unknown (Special l ">")) = unmatched l ">"
     pretty (Unknown t) = red "Error:" <+> "unexpected token" <+> squotes (pretty t) <+> "at" <+> pretty (token_posn t) <> linebreak
     pretty (LexError s) = red "Lexical error:" <+> text s
 
-parseError :: [Token] -> Either ATSError a
-parseError = Left . Unknown . head 
+left :: ATSError -> ParseSt b
+left = lift . Left
+
+parseError :: [Token] -> ParseSt a
+parseError = left . Unknown . head 
 
 }
diff --git a/src/Language/ATS/PrettyPrint.hs b/src/Language/ATS/PrettyPrint.hs
--- a/src/Language/ATS/PrettyPrint.hs
+++ b/src/Language/ATS/PrettyPrint.hs
@@ -82,14 +82,13 @@
     pretty GreaterThan        = ">"
     pretty LessThan           = "<"
     pretty Equal              = "="
-    pretty NotEqual           = "!="
+    pretty NotEq              = "!="
     pretty LogicalAnd         = "&&"
     pretty LogicalOr          = "||"
     pretty LessThanEq         = "<="
     pretty GreaterThanEq      = ">="
     pretty StaticEq           = "=="
     pretty Mod                = "%"
-    pretty NotEq              = "<>"
     pretty Mutate             = ":="
     pretty SpearOp            = "->"
     pretty At                 = "@"
@@ -132,12 +131,12 @@
 prettyArgsProof Nothing  = prettyArgs
 
 instance Pretty (UnOp a) where
-    pretty Negate        = "~"
-    pretty Deref         = "!"
-    pretty (SpecialOp s) = text s
+    pretty Negate          = "~"
+    pretty Deref           = "!"
+    pretty (SpecialOp _ s) = text s
 
 instance Eq a => Pretty (Expression a) where
-    pretty = cata a . rewriteATS where
+    pretty = cata a 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 e')          = flatAlt
@@ -166,7 +165,7 @@
             | startsParens x = pretty nam <> prettyImplicits is <> pretty x
         a (CallF nam is [] e xs) = pretty nam <> prettyImplicits is <> prettyArgsProof e xs
         a (CallF nam is us e xs) = pretty nam <> prettyImplicits is <> prettyArgsU "{" "}" us <> prettyArgsProof e xs
-        a (CaseF _ add e cs)            = "case" <> pretty add <+> e <+> "of" <$> indent 2 (prettyCases cs)
+        a (CaseF _ add' e cs)           = "case" <> pretty add' <+> e <+> "of" <$> indent 2 (prettyCases cs)
         a (IfCaseF _ cs)                = "ifcase" <$> indent 2 (prettyIfCase cs)
         a (VoidLiteralF _)              = "()"
         a (RecordValueF _ es Nothing)   = prettyRecord es
@@ -190,11 +189,11 @@
         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 (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 (CommentExprF c e) = text c <$> e
         a (MacroVarF _ s) = ",(" <> text s <> ")"
         a BinListF{} = undefined -- Shouldn't happen
@@ -302,6 +301,7 @@
         a ImplicitTypeF{}                  = ".."
         a (AnonymousRecordF _ rs)          = prettyRecord rs
         a (ParenTypeF _ t)                 = parens t
+        a (WhereTypeF _ t pref)            = t <#> indent 2 ("where" </> pretty pref)
 
 gan :: Eq a => Maybe (Sort a) -> Doc
 gan (Just t) = " : " <> pretty t <> " "
@@ -485,13 +485,16 @@
 (<#>) :: Doc -> Doc -> Doc
 (<#>) a b = lineAlt (a <$> indent 2 b) (a <+> b)
 
-prettySigG :: (Pretty a) => Doc -> String -> Maybe a -> Doc
-prettySigG d si (Just rt) = d <> ":" <> text si <#> pretty rt <> d
-prettySigG _ _ _          = mempty
+prettySigG :: (Pretty a) => Doc -> Doc -> Maybe String -> Maybe a -> Doc
+prettySigG d d' (Just si) (Just rt) = d <> ":" <> text si <#> pretty rt <> d'
+prettySigG _ _ _ _                  = mempty
 
-prettySig :: (Pretty a) => String -> Maybe a -> Doc
-prettySig = prettySigG space
+prettySigNull :: (Pretty a) => Maybe String -> Maybe a -> Doc
+prettySigNull = prettySigG space mempty
 
+prettySig :: (Pretty a) => Maybe String -> Maybe a -> Doc
+prettySig = prettySigG space space
+
 prettyTermetric :: Pretty a => Maybe a -> Doc
 prettyTermetric (Just t) = softline <> ".<" <> pretty t <> ">." <> softline
 prettyTermetric Nothing  = mempty
@@ -502,11 +505,11 @@
     pretty (PreF i si [] us as rt t (Just e)) = pretty i </> fancyU us <> prettyTermetric t <> prettyArgsNil as <> prettySig si rt <> "=" <$> indent 2 (pretty e)
     pretty (PreF i si pus [] as rt Nothing (Just e)) = fancyU pus </> pretty i <> prettyArgsNil as <> prettySig si rt <> "=" <$> indent 2 (pretty e)
     pretty (PreF i si pus us as rt t (Just e)) = fancyU pus </> pretty i </> fancyU us <> prettyTermetric t <> prettyArgsNil as <> prettySig si rt <> "=" <$> indent 2 (pretty e)
-    pretty (PreF i si [] [] as rt Nothing Nothing) = pretty i <> prettyArgsNil as <+> ":" <> text si <#> pretty rt
-    pretty (PreF i si [] us [] rt Nothing Nothing) = pretty i </> fancyU us <+> ":" <> text si <#> pretty rt
-    pretty (PreF i si [] us as rt Nothing Nothing) = pretty i </> fancyU us </> prettyArgsNil as <+> ":" <> text si <#> pretty rt
-    pretty (PreF i si pus [] as rt t Nothing) = fancyU pus </> pretty i <> prettyTermetric t </> prettyArgsNil as <+> ":" <> text si <#> pretty rt
-    pretty (PreF i si pus us as rt t Nothing) = fancyU pus </> pretty i <> prettyTermetric t </> fancyU us </> prettyArgsNil as <+> ":" <> text si <#> pretty rt
+    pretty (PreF i si [] [] as rt Nothing Nothing) = pretty i <> prettyArgsNil as <> prettySigNull si rt
+    pretty (PreF i si [] us [] rt Nothing Nothing) = pretty i </> fancyU us <> prettySigNull si rt
+    pretty (PreF i si [] us as rt Nothing Nothing) = pretty i </> fancyU us </> prettyArgsNil as <> prettySigNull si rt
+    pretty (PreF i si pus [] as rt t Nothing) = fancyU pus </> pretty i <> prettyTermetric t </> prettyArgsNil as <> prettySigNull si rt
+    pretty (PreF i si pus us as rt t Nothing) = fancyU pus </> pretty i <> prettyTermetric t </> fancyU us </> prettyArgsNil as <> prettySigNull si rt
 
 instance Eq a => Pretty (DataPropLeaf a) where
     pretty (DataPropLeaf us e Nothing)   = "|" <+> foldMap pretty (reverse us) <+> pretty e
@@ -524,7 +527,7 @@
 prettyMaybeType _        = mempty
 
 valSig :: (Pretty a) => Maybe a -> Doc
-valSig = prettySigG mempty mempty
+valSig = prettySigG mempty mempty (Just mempty)
 
 prettySortArgs :: (Pretty a) => Maybe [a] -> Doc
 prettySortArgs Nothing   = mempty
diff --git a/src/Language/ATS/Types.hs b/src/Language/ATS/Types.hs
--- a/src/Language/ATS/Types.hs
+++ b/src/Language/ATS/Types.hs
@@ -46,6 +46,8 @@
     , SortArg (..)
     , SortArgs
     , DataSortLeaf (..)
+    , FixityState
+    -- * Rewrites
     , rewriteATS
     , rewriteDecl
     -- * Lenses
@@ -59,11 +61,13 @@
     , comment
     ) where
 
+import           Control.Composition
 import           Control.DeepSeq          (NFData)
 import           Control.Lens
 import           Data.Function            (on)
 import           Data.Functor.Foldable    (ListF (Cons), ana, cata, embed, project)
 import           Data.Functor.Foldable.TH (makeBaseFunctor)
+import qualified Data.Map                 as M
 import           Data.Maybe               (isJust)
 import           Data.Semigroup           (Semigroup)
 import           GHC.Generics             (Generic)
@@ -88,13 +92,13 @@
 
 -- | Declare something in a scope (a function, value, action, etc.)
 data Declaration a = Func { pos :: a, _fun :: Function a }
-                   | Impl [Arg a] (Implementation a) -- TODO do something better for implicit universals
-                   | ProofImpl [Arg a] (Implementation a)
-                   | Val Addendum (Maybe (Type a)) (Pattern a) (Expression a)
+                   | Impl { implArgs :: [Arg a], _impl :: Implementation a } -- TODO do something better for implicit universals
+                   | ProofImpl { implArgs :: [Arg a], _impl :: Implementation a }
+                   | Val { add :: Addendum, valT :: Maybe (Type a), valPat :: Pattern a, _valExpression :: Expression a }
                    | StaVal [Universal a] String (Type a)
-                   | PrVal (Pattern a) (Expression a)
-                   | Var (Maybe (Type a)) (Pattern a) (Maybe (Expression a)) (Maybe (Expression a)) -- TODO a
-                   | AndDecl (Maybe (Type a)) (Pattern a) (Expression a)
+                   | PrVal { prvalPat :: Pattern a, _prValExpr :: Expression a }
+                   | Var { varT :: Maybe (Type a), varPat :: Pattern a, _varExpr1 :: Maybe (Expression a), _varExpr2 :: Maybe (Expression a) }
+                   | AndDecl { andT :: Maybe (Type a), andPat :: Pattern a, _andExpr :: Expression a }
                    | Include String
                    | Staload Bool (Maybe String) String
                    | Stadef String (SortArgs a) (Type a) -- [Type] -- FIXME stadef array(a:vt@ype, n:int) = @[a][n]
@@ -112,7 +116,7 @@
                    | OverloadOp a (BinOp a) (Name a) (Maybe Int)
                    | OverloadIdent a String (Name a) (Maybe Int)
                    | Comment { _comment :: String }
-                   | DataProp a String (SortArgs a) [DataPropLeaf a]
+                   | DataProp { pos :: a, propName :: String, propArgs :: SortArgs a, _propLeaves :: [DataPropLeaf a] }
                    | DataView a String (SortArgs a) [Leaf a]
                    | Extern a (Declaration a)
                    | Define String
@@ -135,7 +139,7 @@
 data DataSortLeaf a = DataSortLeaf [Universal a] (Sort a) (Maybe (Sort a))
                     deriving (Show, Eq, Generic, NFData)
 
-data DataPropLeaf a = DataPropLeaf [Universal a] (Expression a) (Maybe (Expression a))
+data DataPropLeaf a = DataPropLeaf { propU :: [Universal a], _propExpr1 :: Expression a, _propExpr2 :: Maybe (Expression a) }
                     deriving (Show, Eq, Generic, NFData)
 
 -- | A type for parsed ATS types
@@ -160,6 +164,7 @@
             | ViewLiteral Addendum
             | AnonymousRecord a [(String, Type a)]
             | ParenType a (Type a)
+            | WhereType a (Type a) (PreFunction a)
             deriving (Show, Eq, Generic, NFData)
 
 -- | A type for @=>@, @=\<cloref1>@, etc.
@@ -225,7 +230,7 @@
 -- | @~@ is used to negate numbers in ATS
 data UnOp a = Negate
             | Deref
-            | SpecialOp String
+            | SpecialOp a String
     deriving (Show, Eq, Generic, NFData)
 
 -- | Binary operators on expressions
@@ -238,7 +243,6 @@
              | LessThan
              | LessThanEq
              | Equal
-             | NotEqual
              | LogicalAnd
              | LogicalOr
              | StaticEq
@@ -289,10 +293,10 @@
                   | IfCase { posE   :: a
                            , ifArms :: [(Expression a, LambdaType a, Expression a)]
                            }
-                  | Case { posE :: a
-                         , kind :: Addendum
-                         , val  :: Expression a
-                         , arms :: [(Pattern a, LambdaType a, Expression a)] -- ^ Each @((Pattern a), (Expression a))@ pair corresponds to a branch of the 'case' statement
+                  | Case { posE  :: a
+                         , kind  :: Addendum
+                         , val   :: Expression a
+                         , _arms :: [(Pattern a, LambdaType a, Expression a)] -- ^ Each @((Pattern a), (Expression a))@ pair corresponds to a branch of the 'case' statement
                          }
                   | RecordValue a [(String, Expression a)] (Maybe (Type a))
                   | Precede (Expression a) (Expression a)
@@ -305,8 +309,8 @@
                   | Begin a (Expression a)
                   | BinList { _op :: BinOp a, _exprs :: [Expression a] }
                   | PrecedeList { _exprs :: [Expression a] }
-                  | FixAt String (StackFunction a)
-                  | LambdaAt (StackFunction a)
+                  | FixAt a String (StackFunction a)
+                  | LambdaAt a (StackFunction a)
                   | ParenExpr a (Expression a)
                   | CommentExpr String (Expression a)
                   | MacroVar a String
@@ -319,7 +323,7 @@
                                   , universalsI    :: [Universal a] -- ^ Universal quantifiers
                                   , nameI          :: Name a -- ^ (Name a) of the template being implemented
                                   , iArgs          :: [Arg a] -- ^ Arguments
-                                  , iExpression    :: Either (StaticExpression a) (Expression a) -- ^ Expression (or static expression) holding the function body.
+                                  , _iExpression   :: Either (StaticExpression a) (Expression a) -- ^ Expression (or static expression) holding the function body.
                                   }
     deriving (Show, Eq, Generic, NFData)
 
@@ -335,6 +339,9 @@
                 | CastFn { _preF :: PreFunction a }
                 deriving (Show, Eq, Generic, NFData)
 
+-- | A type for stack-allocated functions. See
+-- [here](http://ats-lang.sourceforge.net/DOCUMENT/ATS2TUTORIAL/HTML/c1267.html)
+-- for more.
 data StackFunction a = StackF { stSig        :: String
                               , stArgs       :: [Arg a]
                               , stReturnType :: Type a
@@ -343,7 +350,7 @@
                               deriving (Show, Eq, Generic, NFData)
 
 data PreFunction a = PreF { fname         :: Name a -- ^ Function name
-                          , sig           :: String -- ^ e.g. <> or \<!wrt>
+                          , sig           :: Maybe String -- ^ e.g. <> or \<!wrt>
                           , preUniversals :: [Universal a] -- ^ Universal quantifiers making a function generic
                           , universals    :: [Universal a] -- ^ (Universal a) quantifiers/refinement type
                           , args          :: [Arg a] -- ^ Actual function arguments
@@ -360,11 +367,27 @@
 makeLenses ''Leaf
 makeLenses ''Declaration
 makeLenses ''PreFunction
+makeLenses ''Implementation
+makeLenses ''DataPropLeaf
 makeLenses ''Function
 makeLenses ''Type
 
-rewriteDecl :: Eq a => Declaration a -> Declaration a
-rewriteDecl x@SumViewType{} = g x
+exprLens :: Eq a => FixityState a -> ASetter s t (Expression a) (Expression a) -> s -> t
+exprLens st = flip over (rewriteATS st)
+
+exprLenses :: Eq a => FixityState a -> [ASetter b b (Expression a) (Expression a)] -> b -> b
+exprLenses st = thread . fmap (exprLens st)
+
+rewriteDecl :: Eq a => FixityState a -> Declaration a -> Declaration a
+rewriteDecl st (Extern l d) = Extern l (rewriteDecl st d)
+rewriteDecl st x@Val{} = exprLens st valExpression x
+rewriteDecl st x@Var{} = exprLenses st [varExpr1._Just, varExpr2._Just] x
+rewriteDecl st x@Func{} = exprLens st (fun.preF.expression._Just) x
+rewriteDecl st x@Impl{} = exprLens st (impl.iExpression._Right) x
+rewriteDecl st x@PrVal{} = exprLens st prValExpr x
+rewriteDecl st x@AndDecl{} = exprLens st andExpr x
+rewriteDecl st x@DataProp{} = exprLenses st (fmap ((propLeaves.each).) [propExpr1, propExpr2._Just]) x
+rewriteDecl _ x@SumViewType{} = g x
     where g = over (leaves.mapped.constructorUniversals) h
           h :: Eq a => [Universal a] -> [Universal a]
           h = ana c where
@@ -372,7 +395,7 @@
                 | 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
+rewriteDecl _ x = x
 
 -- FIXME left vs. right shouldn't be treated the same
 instance (Eq a) => Ord (Fixity a) where
@@ -387,39 +410,50 @@
 infix_ :: Int -> Fixity a
 infix_ = Infix undefined
 
+type FixityState a = M.Map String (Fixity a)
+
 -- | Default fixities from @fixity.ats@
-getFixity :: BinOp a -> Fixity a
-getFixity Add           = leftFix 50
-getFixity Sub           = leftFix 50
-getFixity Mutate        = infix_ 0
-getFixity Mult          = leftFix 60
-getFixity Div           = leftFix 60
-getFixity SpearOp       = rightFix 10
-getFixity LogicalAnd    = leftFix 21
-getFixity LogicalOr     = leftFix 20
-getFixity At            = rightFix 40
-getFixity GreaterThan   = infix_ 40
-getFixity GreaterThanEq = infix_ 40
-getFixity LessThanEq    = infix_ 40
-getFixity Equal         = infix_ 30
-getFixity NotEqual      = infix_ 30
-getFixity StaticEq      = infix_ 30
-getFixity Mod           = leftFix 60
-getFixity _             = leftFix 100
+getFixity :: FixityState a -> BinOp a -> Fixity a
+getFixity _ Add                  = leftFix 50
+getFixity _ Sub                  = leftFix 50
+getFixity _ Mutate               = infix_ 0
+getFixity _ Mult                 = leftFix 60
+getFixity _ Div                  = leftFix 60
+getFixity _ SpearOp              = rightFix 10
+getFixity _ LogicalAnd           = leftFix 21
+getFixity _ LogicalOr            = leftFix 20
+getFixity _ At                   = rightFix 40
+getFixity _ GreaterThan          = infix_ 40
+getFixity _ GreaterThanEq        = infix_ 40
+getFixity _ LessThanEq           = infix_ 40
+getFixity _ Equal                = infix_ 30
+getFixity _ NotEq                = infix_ 30
+getFixity _ StaticEq             = infix_ 30
+getFixity _ Mod                  = leftFix 60
+getFixity _ LessThan             = infix_ 40
+getFixity st (SpecialInfix _ op') =
+    case M.lookup op' st of
+        (Just f) -> f
+        Nothing  -> infix_ 100
 
-instance (Eq a) => Ord (BinOp a) where
-    compare = on compare getFixity
+compareFixity :: Eq a => FixityState a -> BinOp a -> BinOp a -> Bool
+compareFixity st = (== GT) .* on compare (getFixity st)
 
-rewriteATS :: Eq a => Expression a -> Expression a
-rewriteATS = cata a where
+-- | Among other things, this rewrites expressions so that operator precedence
+-- is respected; this ensures @1 + 2 * 3@ will be parsed as the correct
+-- expression.
+rewriteATS :: Eq a => FixityState a -> Expression a -> Expression a
+rewriteATS st = cata a where
+    a (LetF loc (ATS ds) e')                         = Let loc (ATS (rewriteDecl st <$> ds)) e'
     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 op' (Binary op'' e e') e'')
-        | op' > op'' = Binary op'' e (Binary op' e' e'')
+        | compareFixity st op' op'' = Binary op'' e (Binary op' 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 (WhereExpF e (ATS ds))                         = WhereExp e (ATS (rewriteDecl st <$> ds))
     a x                                              = embed x