Improve parsing.

6 files changed, 593 insertions, 598 deletions

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index 9215dda..b8fca7b 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -18,74 +18,77 @@ Context n = List (String, Fin n)
 bind : Context n -> String -> Context (S n)
 bind ctx str = (str, 0) :: map (mapSnd FS) ctx
 
-export
 abstractSyntax : Context n -> Syntax -> Logging ann (Term n)
+abstractSyntaxBounds : Context n -> WithBounds Syntax -> Logging ann (WithBounds (Term n))
+
 abstractSyntax ctx (Var var) = do
-  let Just i = lookup var.val ctx
+  let Just i = lookup var ctx
     | Nothing => inScope "unbound variable" $ fatal var
   pure (Var var i)
-abstractSyntax ctx (Sort bounds s) = pure (Sort bounds s)
-abstractSyntax ctx (Pi bounds var a b) = do
-  a <- abstractSyntax ctx a
-  b <- abstractSyntax (bind ctx var.val) b
-  pure (Pi bounds var.val a b)
-abstractSyntax ctx (Lambda bounds var t) = do
-  t <- abstractSyntax (bind ctx var.val) t
-  pure (Lambda bounds var.val t)
+abstractSyntax ctx (Sort s) = pure (Sort s)
+abstractSyntax ctx (Pi var a b) = do
+  a <- abstractSyntaxBounds ctx a
+  b <- abstractSyntaxBounds (bind ctx var.val) b
+  pure (Pi var a b)
+abstractSyntax ctx (Lambda var t) = do
+  t <- abstractSyntaxBounds (bind ctx var.val) t
+  pure (Lambda var t)
 abstractSyntax ctx (App t u) = do
-  t <- abstractSyntax ctx t
-  u <- abstractSyntax ctx u
+  t <- abstractSyntaxBounds ctx t
+  u <- abstractSyntaxBounds ctx u
   pure (App t u)
-abstractSyntax ctx (Sigma bounds var a b) = do
-  a <- abstractSyntax ctx a
-  b <- abstractSyntax (bind ctx var.val) b
-  pure (Sigma bounds var.val a b)
-abstractSyntax ctx (Pair b t u) = do
-  t <- abstractSyntax ctx t
-  u <- abstractSyntax ctx u
-  pure (Pair b t u)
-abstractSyntax ctx (Fst b t) = do
-  t <- abstractSyntax ctx t
-  pure (Fst b t)
-abstractSyntax ctx (Snd b t) = do
-  t <- abstractSyntax ctx t
-  pure (Snd b t)
-abstractSyntax ctx (Top b) = pure (Top b)
-abstractSyntax ctx (Point b) = pure (Point b)
-abstractSyntax ctx (Bottom b) = pure (Bottom b)
-abstractSyntax ctx (Absurd bounds a t) = do
-  a <- abstractSyntax ctx a
-  t <- abstractSyntax ctx t
-  pure (Absurd bounds a t)
-abstractSyntax ctx (Equal bounds t u) = do
-  t <- abstractSyntax ctx t
-  u <- abstractSyntax ctx u
-  pure (Equal bounds t u)
-abstractSyntax ctx (Refl bounds t) = do
-  t <- abstractSyntax ctx t
-  pure (Refl bounds t)
-abstractSyntax ctx (Transp bounds t b u t' e) = do
-  t <- abstractSyntax ctx t
-  b <- abstractSyntax ctx b
-  u <- abstractSyntax ctx u
-  t' <- abstractSyntax ctx t'
-  e <- abstractSyntax ctx e
-  pure (Transp bounds t b u t' e)
-abstractSyntax ctx (Cast bounds b e t) = do
-  b <- abstractSyntax ctx b
-  e <- abstractSyntax ctx e
-  t <- abstractSyntax ctx t
-  pure (Cast bounds b e t)
-abstractSyntax ctx (CastId bounds t) = do
-  t <- abstractSyntax ctx t
-  pure (CastId bounds t)
+abstractSyntax ctx (Sigma var a b) = do
+  a <- abstractSyntaxBounds ctx a
+  b <- abstractSyntaxBounds (bind ctx var.val) b
+  pure (Sigma var a b)
+abstractSyntax ctx (Pair t u) = do
+  t <- abstractSyntaxBounds ctx t
+  u <- abstractSyntaxBounds ctx u
+  pure (Pair t u)
+abstractSyntax ctx (Fst t) = do
+  t <- abstractSyntaxBounds ctx t
+  pure (Fst t)
+abstractSyntax ctx (Snd t) = do
+  t <- abstractSyntaxBounds ctx t
+  pure (Snd t)
+abstractSyntax ctx Top = pure Top
+abstractSyntax ctx Point = pure Point
+abstractSyntax ctx Bottom = pure Bottom
+abstractSyntax ctx (Absurd a t) = do
+  a <- abstractSyntaxBounds ctx a
+  t <- abstractSyntaxBounds ctx t
+  pure (Absurd a t)
+abstractSyntax ctx (Equal t u) = do
+  t <- abstractSyntaxBounds ctx t
+  u <- abstractSyntaxBounds ctx u
+  pure (Equal t u)
+abstractSyntax ctx (Refl t) = do
+  t <- abstractSyntaxBounds ctx t
+  pure (Refl t)
+abstractSyntax ctx (Transp t b u t' e) = do
+  t <- abstractSyntaxBounds ctx t
+  b <- abstractSyntaxBounds ctx b
+  u <- abstractSyntaxBounds ctx u
+  t' <- abstractSyntaxBounds ctx t'
+  e <- abstractSyntaxBounds ctx e
+  pure (Transp t b u t' e)
+abstractSyntax ctx (Cast b e t) = do
+  b <- abstractSyntaxBounds ctx b
+  e <- abstractSyntaxBounds ctx e
+  t <- abstractSyntaxBounds ctx t
+  pure (Cast b e t)
+abstractSyntax ctx (CastId t) = do
+  t <- abstractSyntaxBounds ctx t
+  pure (CastId t)
+
+abstractSyntaxBounds ctx (MkBounded v irrel bnds) =
+  pure $ MkBounded !(abstractSyntax ctx v) irrel bnds
 
 abstractDefinition : Context n -> Definition -> Logging ann (Definition n)
 abstractDefinition ctx def = pure $ MkDefinition
   { name = def.name
-  , bounds = def.bounds
-  , ty = !(abstractSyntax ctx def.ty)
-  , tm = !(abstractSyntax ctx def.tm)
+  , ty = !(abstractSyntaxBounds ctx def.ty)
+  , tm = !(abstractSyntaxBounds ctx def.tm)
   }
 
 export
@@ -93,7 +96,7 @@ abstractBlock : (defs : List Definition) -> Logging ann (Block (length defs))
 abstractBlock defs =
   let asContext : Block n -> Context n
       asContext []            = []
-      asContext (defs :< def) = bind (asContext defs) def.name
+      asContext (defs :< def) = bind (asContext defs) def.name.val
   in let helper : Block n -> (defs : List Definition) -> Logging ann (Block (length defs + n))
          helper blk []            = pure blk
          helper blk (def :: defs) = do
diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index 2caf733..fd3a814 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -5,6 +5,7 @@ import Data.Fin
 import Obs.Sort
 import Obs.Substitution
 
+import Text.Bounded
 import Text.PrettyPrint.Prettyprinter
 
 %default total
@@ -49,7 +50,7 @@ data NormalForm : Nat -> Type where
 public export
 record Definition (n : Nat) where
   constructor MkDefinition
-  name   : String
+  name   : WithBounds String
   sort   : Sort
   ty     : NormalForm n
   tm     : NormalForm n
@@ -208,8 +209,8 @@ Pretty (NormalForm n) where
 export
 Pretty (Definition n) where
   pretty def = group $
-    pretty def.name <++> colon <+> softline <+> pretty def.ty <+> softline <+> colon <++> pretty def.sort <+> hardline <+>
-    pretty def.name <++> equals <+> softline <+> pretty def.tm
+    pretty def.name.val <++> colon <+> softline <+> pretty def.ty <+> softline <+> colon <++> pretty def.sort <+> hardline <+>
+    pretty def.name.val <++> equals <+> softline <+> pretty def.tm
 
 export
 Pretty (Context n) where
diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index 95d8e96..0ccba86 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -1,6 +1,7 @@
 module Obs.Parser
 
 import Data.String
+import Data.Vect
 
 import Obs.Logging
 import Obs.Sort
@@ -15,8 +16,8 @@ import Text.Parser
 %default total
 
 data ObsTokenKind
-  = OTNewline
-  | OTIgnore
+  = OTNewlines
+  | OTSpaces
   | OTIdent
   -- Keywords
   | OTProp
@@ -49,8 +50,8 @@ data ObsTokenKind
   | OTColon
 
 Eq ObsTokenKind where
-  OTNewline == OTNewline = True
-  OTIgnore == OTIgnore = True
+  OTNewlines == OTNewlines = True
+  OTSpaces == OTSpaces = True
   OTIdent == OTIdent = True
   OTProp == OTProp = True
   OTSet == OTSet = True
@@ -84,8 +85,8 @@ TokenKind ObsTokenKind where
   TokType OTNat   = Nat
   TokType _     = ()
 
-  tokValue OTNewline s = ()
-  tokValue OTIgnore s = ()
+  tokValue OTNewlines s = ()
+  tokValue OTSpaces s = ()
   tokValue OTIdent s = s
   tokValue OTProp s = ()
   tokValue OTSet s = ()
@@ -116,9 +117,35 @@ TokenKind ObsTokenKind where
 ObsToken : Type
 ObsToken = Token ObsTokenKind
 
-ignored : WithBounds ObsToken -> Bool
-ignored (MkBounded (Tok OTIgnore _) _ _) = True
-ignored _ = False
+Show ObsToken where
+  show (Tok OTNewlines s) = "\\n"
+  show (Tok OTSpaces s) = " "
+  show (Tok OTIdent s) = s
+  show (Tok OTProp s) = "Prop"
+  show (Tok OTSet s) = "Set"
+  show (Tok OTNat s) = s
+  show (Tok OTFst s) = "fst"
+  show (Tok OTSnd s) = "snd"
+  show (Tok OTPoint s) = "tt"
+  show (Tok OTVoid s) = "Void"
+  show (Tok OTAbsurd s) = "absurd"
+  show (Tok OTRefl s) = "refl"
+  show (Tok OTTransp s) = "transp"
+  show (Tok OTCast s) = "cast"
+  show (Tok OTCastRefl s) = "castRefl"
+  show (Tok OTUnit s) = "()"
+  show (Tok OTPOpen s) = "("
+  show (Tok OTPClose s) = ")"
+  show (Tok OTAOpen s) = "<"
+  show (Tok OTAClose s) = ">"
+  show (Tok OTBackslash s) = "\\"
+  show (Tok OTThinArrow s) = "->"
+  show (Tok OTFatArrow s) = "=>"
+  show (Tok OTProduct s) = "**"
+  show (Tok OTComma s) = ","
+  show (Tok OTTilde s) = "~"
+  show (Tok OTEqual s) = "="
+  show (Tok OTColon s) = ":"
 
 identifier : Lexer
 identifier = alpha <+> many alphaNum
@@ -139,7 +166,7 @@ keywords =
   ]
 
 obsTokenMap : TokenMap ObsToken
-obsTokenMap = toTokenMap [(newline, OTNewline), (spaces, OTIgnore)] ++
+obsTokenMap = toTokenMap [(newlines, OTNewlines), (spaces, OTSpaces)] ++
   [ (identifier, \s =>
         case lookup s keywords of
           (Just kind) => Tok kind s
@@ -160,175 +187,154 @@ obsTokenMap = toTokenMap [(newline, OTNewline), (spaces, OTIgnore)] ++
   , (exact ":", OTColon)
   ]
 
-newlines : Grammar state ObsToken False ()
-newlines = map (\_ => ()) $ many (match OTNewline)
+op : Type -> Type -> Nat -> Type
+op a b 0 = b
+op a b (S n) = a -> op a b n
+
+uncurry : (n : _) -> op a b n -> Vect n a -> b
+uncurry 0     f []        = f
+uncurry (S n) f (x :: xs) = uncurry n (f x) xs
+
+headForms : List (ObsTokenKind, (n ** (Vect n (WithBounds Syntax) -> Syntax)))
+headForms =
+  [ (OTFst, (1 ** uncurry 1 Fst))
+  , (OTSnd, (1 ** uncurry 1 Snd))
+  , (OTPoint, (0 ** uncurry 0 Point))
+  , (OTVoid, (0 ** uncurry 0 Bottom))
+  , (OTAbsurd, (2 ** uncurry 2 Absurd))
+  , (OTRefl, (1 ** uncurry 1 Refl))
+  , (OTTransp, (5 ** uncurry 5 Transp))
+  , (OTCast, (3 ** uncurry 3 Cast))
+  , (OTCastRefl, (1 ** uncurry 1 CastId))
+  , (OTUnit, (0 ** uncurry 0 Top))
+  ]
+
+declForms : List (ObsTokenKind, (WithBounds String -> op (WithBounds Syntax) Syntax 2))
+declForms = [(OTThinArrow, Pi), (OTProduct, Sigma)]
 
-parens : {c : _} -> Grammar state ObsToken c a -> Grammar state ObsToken True a
-parens g =
-  match OTPOpen *>
-  newlines *>
-  g <*
-  newlines <*
-  match OTPClose
+count : (n : _) -> Grammar state tok True a -> Grammar state tok (isSucc n) (Vect n a)
+count 0     p = pure []
+count (S n) p = [| p :: count n p |]
 
 ident : Grammar state ObsToken True (WithBounds String)
 ident = bounds $ match OTIdent
 
-var : Grammar state ObsToken True Syntax
-var = [| Var (ident <* commit) |]
-
-prop : Grammar state ObsToken True Syntax
-prop = do
-  prop <- bounds $ match OTProp <* commit
-  pure (Sort prop.bounds Prop)
-
-set0 : Grammar state ObsToken True Syntax
-set0 = do
-  set <- bounds $ match OTSet <* commit
-  pure (Sort set.bounds (Set 0))
-
-top : Grammar state ObsToken True Syntax
-top = do
-  unit <- bounds $ match OTUnit <* commit
-  pure (Top unit.bounds)
-
-point : Grammar state ObsToken True Syntax
-point = do
-  point <- bounds $ match OTPoint <* commit
-  pure (Point point.bounds)
-
-bottom : Grammar state ObsToken True Syntax
-bottom = do
-  void <- bounds $ match OTVoid <* commit
-  pure (Bottom void.bounds)
-
-atomicNoSet : Grammar state ObsToken True Syntax
-atomicNoSet = (var <|> prop <|> top <|> point <|> bottom) <* commit
-
-atomic : Grammar state ObsToken True Syntax
-atomic = (atomicNoSet <|> set0) <* commit
-
-set : Grammar state ObsToken True Syntax
-set = do
-  i <- [| mergeBounds (bounds $ match OTSet) (bounds $ map Set $ option 0 $ match OTNat) |] <* commit
-  pure (Sort i.bounds i.val)
-
-lambda : Grammar state ObsToken True (Syntax -> Syntax)
-lambda = do
-  name <- bounds $ match OTBackslash *> commit *> ident <* newlines <* match OTFatArrow <* newlines
-  pure (Lambda name.bounds name.val)
-
-projFst : Grammar state ObsToken True (Syntax -> Syntax)
-projFst = do
-  fst <- bounds $ match OTFst <* commit
-  pure (Fst fst.bounds)
-
-projSnd : Grammar state ObsToken True (Syntax -> Syntax)
-projSnd = do
-  snd <- bounds $ match OTSnd <* commit
-  pure (Snd snd.bounds)
-
-botElim : Grammar state ObsToken True (Syntax -> Syntax -> Syntax)
-botElim = do
-  absurd <- bounds $ match OTAbsurd <* commit
-  pure (Absurd absurd.bounds)
-
-refl : Grammar state ObsToken True (Syntax -> Syntax)
-refl = do
-  refl <- bounds $ match OTRefl <* commit
-  pure (Refl refl.bounds)
-
-transp : Grammar state ObsToken True (Syntax -> Syntax -> Syntax -> Syntax -> Syntax -> Syntax)
-transp = do
-  transp <- bounds $ match OTTransp <* commit
-  pure (Transp transp.bounds)
-
-cast : Grammar state ObsToken True (Syntax -> Syntax -> Syntax -> Syntax)
-cast = do
-  cast <- bounds $ match OTCast <* commit
-  pure (Cast cast.bounds)
-
-castRefl : Grammar state ObsToken True (Syntax -> Syntax)
-castRefl = do
-  castRefl <- bounds $ match OTCastRefl <* commit
-  pure (CastId castRefl.bounds)
-
--- NOTE: these functions are all total.
-partial
-pi : WithBounds (WithBounds String, Syntax) -> Grammar state ObsToken True (Syntax -> Syntax)
-partial
-sigma : WithBounds (WithBounds String, Syntax) -> Grammar state ObsToken True (Syntax -> Syntax)
-partial
-pair : Grammar state ObsToken True Syntax -> Grammar state ObsToken True Syntax -> Grammar state ObsToken True Syntax
+whitespace : Grammar state ObsToken True ()
+whitespace = map (\_ => ()) $ some (optional (match OTNewlines) *> match OTSpaces)
+
+parens : Lazy (Grammar state ObsToken True a) -> Grammar state ObsToken True a
+parens p = match OTPOpen *> optional whitespace *> p <* optional whitespace <* match OTPClose
+
+var : Grammar state ObsToken True (WithBounds Syntax)
+var = map (map Var) ident
+
+noArgSort : Grammar state ObsToken True (WithBounds Sort)
+noArgSort = bounds $
+  map (const Prop) (match OTProp <* commit) <|>
+  map (const (Set 0)) (match OTSet <* commit)
+
+sort : Grammar state ObsToken True (WithBounds Sort)
+sort = bounds $
+  map (const Prop) (match OTProp <* commit) <|>
+  map Set (match OTSet *> commit *> option 0 (match OTNat <* commit))
+
+decl : Lazy (Grammar state ObsToken True a) -> Grammar state ObsToken True (WithBounds String, a)
+decl p = [| MkPair (ident <* whitespace <* match OTColon <* whitespace) p |]
+
+pair : Lazy (Grammar state ObsToken True a) -> Grammar state ObsToken True (a, a)
+pair p =
+  match OTAOpen *> commit *>
+  [| MkPair
+      (optional whitespace *> p <* optional whitespace <* match OTComma <* commit)
+      (optional whitespace *> p <* optional whitespace) |]
+  <* match OTAClose <* commit
+
 partial
-term : Grammar state ObsToken True Syntax
+noSortsTerm : Grammar state ObsToken True (WithBounds Syntax)
 partial
-precGteApp : Grammar state ObsToken True Syntax
+term : Grammar state ObsToken True (WithBounds Syntax)
 partial
-precGteEqual : Grammar state ObsToken True Syntax
+head : Grammar state ObsToken True (WithBounds Syntax)
 partial
-exp' : Grammar state ObsToken True Syntax
+spine : Grammar state ObsToken True (WithBounds Syntax)
 partial
-exp : Grammar state ObsToken True Syntax
+equals : Grammar state ObsToken True (WithBounds Syntax)
 partial
-decl : Grammar state ObsToken True (WithBounds String, Syntax)
-
-pi decl = do
-  _ <- match OTThinArrow <* commit <* newlines
-  Parser.Core.pure (uncurry (Pi decl.bounds) decl.val)
-
-sigma decl = do
-  _ <- match OTProduct <* commit <* newlines
-  Parser.Core.pure (uncurry (Sigma decl.bounds) decl.val)
-
-pair fst snd = do
-  pair <- bounds $ [| MkPair (match OTAOpen *> fst <* newlines <* match OTComma <* newlines) (snd <* newlines <* match OTAClose) |]
-  pure (uncurry (Pair pair.bounds) pair.val)
-
-term = atomic <|> pair exp exp <|> parens exp
-precGteApp = atomicNoSet <|> set <|> pair exp exp <|> parens exp
-precGteEqual =
-  map (\ty => let (t, t') = ty.val in maybe t (Equal ty.bounds t) t') $
-  bounds [| MkPair precGteApp (optional (newlines *> match OTTilde *> commit *> newlines *> precGteApp)) |]
-exp' =
-  precGteEqual <|>
-  (projFst <*> term) <|>
-  (projSnd <*> term) <|>
-  (botElim <*> term <*> term) <|>
-  (refl <*> term) <|>
-  (transp <*> term <*> term <*> term <*> term <*> term) <|>
-  (Parser.cast <*> term <*> term <*> term) <|>
-  (castRefl <*> term)
+exp : Grammar state ObsToken True (WithBounds Syntax)
+
+noSortsTerm =
+  parens exp <|>
+  var <|>
+  bounds (map (uncurry Pair) (pair exp))
+
+term = noSortsTerm <|> map (map Sort) noArgSort
+
+head =
+  noSortsTerm <|>
+  map (map Sort) sort <|>
+  bounds
+    (choiceMap
+      (\(hd, (n ** f)) => match hd *> commit *> [| f (count n (whitespace *> term)) |])
+      headForms)
+
+spine = map (uncurry $ foldl (\t, u => joinBounds (map (\_ => map (\_ => App t u) u) t))) $
+  [| MkPair head (many (whitespace *> term)) |]
+
+equals = map (\(t, u) => maybe t (\u => joinBounds (map (\_ => map (\_ => Equal t u) u) t)) u) $
+  [| MkPair spine (optional (whitespace *> match OTTilde *> commit *> whitespace *> spine)) |]
+
 exp =
-  (bounds (parens decl) <* many (match OTNewline) >>= (\decl => (pi decl <|> sigma decl) <*> exp)) <|>
-  (lambda <*> exp) <|>
-  (map (\(t, ts) => foldl1 App (t :: ts)) [| MkPair exp' (many term) |])
-decl = [| MkPair ident (match OTColon *> commit *> exp) |]
+  equals <|>
+  bounds
+    (map (\((var, a), (b, f)) => f var a b) $
+     [| MkPair
+          (parens (decl exp) <* whitespace)
+          (choiceMap
+            (\(op, f) => match op *> commit *> whitespace *> [| MkPair exp (pure f) |])
+            declForms)
+     |]) <|>
+  bounds
+    (map (uncurry Lambda) $
+     match OTBackslash *> commit *>
+     [| MkPair (ident <* whitespace <* match OTFatArrow <* whitespace) exp |])
 
 partial
-def : Grammar state ObsToken True (WithBounds String, Syntax)
-def = [| MkPair ident (match OTEqual *> exp) |]
+def : Grammar state ObsToken True (WithBounds String, WithBounds Syntax)
+def = [| MkPair (ident <* whitespace <* match OTEqual <* whitespace) exp |]
 
 partial
 fullDef : Grammar state ObsToken True Definition
 fullDef =
   seq
-    [| MkPair decl (match OTNewline *> def) |]
+    [| MkPair (decl exp) (optional whitespace *> match OTNewlines *> def) |]
     (\((name, ty), (name', tm)) =>
       if name.val == name'.val
-        then pure (MkDefinition {bounds = name.bounds, name = name.val, ty, tm})
+        then pure (MkDefinition {name = name, ty, tm})
         else fatalLoc name.bounds "name mismatch for declaration and definition")
 
 partial
 file : Grammar state ObsToken False (List Definition)
-file = many (match OTNewline) *> sepBy (some (match OTNewline)) fullDef <* many (match OTNewline) <* eof
-
-postprocess : List (WithBounds ObsToken) -> List (WithBounds ObsToken)
-postprocess [] = []
-postprocess [tok] = if ignored tok then [] else [tok]
-postprocess (tok :: tail@(tok' :: toks)) = case (tok.val.kind, tok'.val.kind) of
-  (OTPOpen, OTPClose) => map (\_ => Tok OTUnit "()") (mergeBounds tok tok') :: postprocess toks
-  _ => if ignored tok then postprocess tail else tok :: postprocess tail
+file =
+  optional (whitespace *> match OTNewlines) *>
+  sepEndBy (optional whitespace *> match OTNewlines) fullDef <*
+  eof
+
+whitespaceIrrelevant : WithBounds ObsToken -> WithBounds ObsToken
+whitespaceIrrelevant a = case (a.val.kind) of
+  OTSpaces => removeIrrelevance a
+  OTNewlines => removeIrrelevance a
+  _ => a
+
+-- Combines tokens for nicer parsing
+mergeToks : List (WithBounds ObsToken) -> List (WithBounds ObsToken)
+mergeToks (a :: tail@(b :: rest)) = case (a.val.kind, b.val.kind) of
+  (OTSpaces, OTNat) => mergeBounds a b :: mergeToks rest
+  (OTPOpen, OTPClose) => map (\_ => (Tok OTUnit "")) (mergeBounds a b) :: mergeToks rest
+  _ => a :: mergeToks tail
+mergeToks toks = toks
+
+preprocess : List (WithBounds ObsToken) -> List (WithBounds ObsToken)
+preprocess = mergeToks . map whitespaceIrrelevant
 
 castErr : Either (List1 (ParsingError tok)) a -> Logging ann a
 castErr (Right x) = pure x
@@ -348,6 +354,7 @@ parse : String -> Logging ann (List Definition)
 parse str = do
   let (toks, _, _, "") = lex obsTokenMap str
     | (_, l, c, rem) => inScope "lex" $ fatal "failed to lex input"
-  (defs, []) <- inScope "parse" $ castErr $ parse file $ postprocess toks
-    | (_, (t :: _)) => inScope "parse" $ fatal "unparsed tokens"
+  let toks = preprocess toks
+  (defs, []) <- inScope "parse" $ castErr $ parse file $ toks
+    | (_, ts) => inScope "parse" $ fatal "unparsed tokens"
   pure defs
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index bcc0cb4..36b1b9f 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -11,116 +11,122 @@ import Text.PrettyPrint.Prettyprinter
 
 public export
 data Syntax : Type where
-  Var    : WithBounds String -> Syntax
+  Var    : String -> Syntax
   -- Sorts
-  Sort   : Bounds -> Sort -> Syntax
+  Sort   : Sort -> Syntax
   -- Dependent Products
-  Pi     : Bounds -> WithBounds String -> Syntax -> Syntax -> Syntax
-  Lambda : Bounds -> WithBounds String -> Syntax -> Syntax
-  App    : Syntax -> Syntax -> Syntax
+  Pi     : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> Syntax
+  Lambda : WithBounds String -> WithBounds Syntax -> Syntax
+  App    : WithBounds Syntax -> WithBounds Syntax -> Syntax
   -- Dependent Sums
-  Sigma  : Bounds -> WithBounds String -> Syntax -> Syntax -> Syntax
-  Pair   : Bounds -> Syntax -> Syntax -> Syntax
-  Fst    : Bounds -> Syntax -> Syntax
-  Snd    : Bounds -> Syntax -> Syntax
+  Sigma  : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> Syntax
+  Pair   : WithBounds Syntax -> WithBounds Syntax -> Syntax
+  Fst    : WithBounds Syntax -> Syntax
+  Snd    : WithBounds Syntax -> Syntax
   -- True
-  Top    : Bounds -> Syntax
-  Point  : Bounds -> Syntax
+  Top    : Syntax
+  Point  : Syntax
   -- False
-  Bottom : Bounds -> Syntax
-  Absurd : Bounds -> Syntax -> Syntax -> Syntax
+  Bottom : Syntax
+  Absurd : WithBounds Syntax -> WithBounds Syntax -> Syntax
   -- Equality
-  Equal  : Bounds -> Syntax -> Syntax -> Syntax
-  Refl   : Bounds -> Syntax -> Syntax
-  Transp : Bounds -> Syntax -> Syntax -> Syntax -> Syntax -> Syntax -> Syntax
-  Cast   : Bounds -> Syntax -> Syntax -> Syntax -> Syntax
-  CastId : Bounds -> Syntax -> Syntax
+  Equal  : WithBounds Syntax -> WithBounds Syntax -> Syntax
+  Refl   : WithBounds Syntax -> Syntax
+  Transp : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
+  Cast   : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
+  CastId : WithBounds Syntax -> Syntax
 
 public export
 record Definition where
   constructor MkDefinition
-  bounds : Bounds -- of the name
-  name   : String
-  ty     : Syntax
-  tm     : Syntax
+  name   : WithBounds String
+  ty     : WithBounds Syntax
+  tm     : WithBounds Syntax
 
 -- Pretty Print ----------------------------------------------------------------
 
+prettyPrec : Prec -> Syntax -> Doc ann
+prettyPrecBounds : Prec -> WithBounds Syntax -> Doc ann
+
+prettyPrec d (Var var) = pretty var
+prettyPrec d (Sort s) = prettyPrec d s
+prettyPrec d (Pi var a b) =
+  parenthesise (d > Open) $
+  group $
+  parens (pretty var.val <++> colon <+> softline <+> prettyPrecBounds Open a) <++>
+  pretty "->" <+> softline <+>
+  prettyPrecBounds Open b
+prettyPrec d (Lambda var t) =
+  parenthesise (d > Open) $
+  group $
+  backslash <+> pretty var.val <++>
+  pretty "=>" <+> softline <+>
+  prettyPrecBounds Open t
+prettyPrec d (App t u) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [prettyPrecBounds Open t, prettyPrecBounds App u]
+prettyPrec d (Sigma var a b) =
+  parenthesise (d >= App) $
+  group $
+  parens (pretty var.val <++> colon <+> softline <+> prettyPrecBounds Open a) <++>
+  pretty "**" <+> softline <+>
+  prettyPrecBounds Open b
+prettyPrec d (Pair t u) =
+  angles $
+  group $
+  neutral <++> prettyPrecBounds Open t <+> comma <+> softline <+> prettyPrecBounds Open u <++> neutral
+prettyPrec d (Fst t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "fst", prettyPrecBounds App t]
+prettyPrec d (Snd t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "snd", prettyPrecBounds App t]
+prettyPrec d Top = pretty "()"
+prettyPrec d Point = pretty "tt"
+prettyPrec d Bottom = pretty "Void"
+prettyPrec d (Absurd a t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "absurd", prettyPrecBounds App a, prettyPrecBounds App t]
+prettyPrec d (Equal t u) =
+  parenthesise (d >= Equal) $
+  group $
+  prettyPrecBounds Equal t <++> pretty "~" <+> softline <+> prettyPrecBounds Equal u
+prettyPrec d (Refl t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "refl", prettyPrecBounds App t]
+prettyPrec d (Transp t b u t' e) =
+  parenthesise (d >= App) $
+  group $
+  fillSep $
+  [ pretty "transp"
+  , prettyPrecBounds App t
+  , prettyPrecBounds App b
+  , prettyPrecBounds App u
+  , prettyPrecBounds App t'
+  , prettyPrecBounds App e
+  ]
+prettyPrec d (Cast b e t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "cast", prettyPrecBounds App b, prettyPrecBounds App e, prettyPrecBounds App t]
+prettyPrec d (CastId t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "castRefl", prettyPrecBounds App t]
+
+prettyPrecBounds d (MkBounded val _ _) = prettyPrec d val
+
 export
 Pretty Syntax where
-  prettyPrec d (Var var) = pretty var.val
-  prettyPrec d (Sort _ s) = prettyPrec d s
-  prettyPrec d (Pi _ var a b) =
-    parenthesise (d > Open) $
-    group $
-    parens (pretty var.val <++> colon <+> softline <+> prettyPrec Open a) <++>
-    pretty "->" <+> softline <+>
-    prettyPrec Open b
-  prettyPrec d (Lambda _ var t) =
-    parenthesise (d > Open) $
-    group $
-    backslash <+> pretty var.val <++>
-    pretty "=>" <+> softline <+>
-    prettyPrec Open t
-  prettyPrec d (App t u) =
-    parenthesise (d >= App) $
-    group $
-    fillSep [prettyPrec Open t, prettyPrec App u]
-  prettyPrec d (Sigma _ var a b) =
-    parenthesise (d >= App) $
-    group $
-    parens (pretty var.val <++> colon <+> softline <+> prettyPrec Open a) <++>
-    pretty "**" <+> softline <+>
-    prettyPrec Open b
-  prettyPrec d (Pair _ t u) =
-    angles $
-    group $
-    neutral <++> prettyPrec Open t <+> comma <+> softline <+> prettyPrec Open u <++> neutral
-  prettyPrec d (Fst _ t) =
-    parenthesise (d >= App) $
-    group $
-    fillSep [pretty "fst", prettyPrec App t]
-  prettyPrec d (Snd _ t) =
-    parenthesise (d >= App) $
-    group $
-    fillSep [pretty "snd", prettyPrec App t]
-  prettyPrec d (Top _) = pretty "()"
-  prettyPrec d (Point _) = pretty "tt"
-  prettyPrec d (Bottom _) = pretty "Void"
-  prettyPrec d (Absurd _ a t) =
-    parenthesise (d >= App) $
-    group $
-    fillSep [pretty "absurd", prettyPrec App a, prettyPrec App t]
-  prettyPrec d (Equal _ t u) =
-    parenthesise (d >= Equal) $
-    group $
-    prettyPrec Equal t <++> pretty "~" <+> softline <+> prettyPrec Equal u
-  prettyPrec d (Refl _ t) =
-    parenthesise (d >= App) $
-    group $
-    fillSep [pretty "refl", prettyPrec App t]
-  prettyPrec d (Transp _ t b u t' e) =
-    parenthesise (d >= App) $
-    group $
-    fillSep $
-    [ pretty "transp"
-    , prettyPrec App t
-    , prettyPrec App b
-    , prettyPrec App u
-    , prettyPrec App t'
-    , prettyPrec App e
-    ]
-  prettyPrec d (Cast _ b e t) =
-    parenthesise (d >= App) $
-    group $
-    fillSep [pretty "cast", prettyPrec App b, prettyPrec App e, prettyPrec App t]
-  prettyPrec d (CastId _ t) =
-    parenthesise (d >= App) $
-    group $
-    fillSep [pretty "castRefl", prettyPrec App t]
+  prettyPrec = Syntax.prettyPrec
 
 export
 Pretty Definition where
   pretty def = group $
-    pretty def.name <++> colon <+> softline <+> pretty def.ty <+> hardline <+>
-    pretty def.name <++> equals <+> softline <+> pretty def.tm
+    pretty def.name.val <++> colon <+> softline <+> pretty def.ty.val <+> hardline <+>
+    pretty def.name.val <++> equals <+> softline <+> pretty def.tm.val
diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index 578bf83..446fdcb 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -12,147 +12,130 @@ import Text.PrettyPrint.Prettyprinter
 
 public export
 data Term : Nat -> Type where
-  Var    : WithBounds String -> Fin n -> Term n
+  Var    : String -> Fin n -> Term n
   -- Sorts
-  Sort   : Bounds -> Sort -> Term n
+  Sort   : Sort -> Term n
   -- Dependent Product
-  Pi     : Bounds -> String -> Term n -> Term (S n) -> Term n
-  Lambda : Bounds -> String -> Term (S n) -> Term n
-  App    : Term n -> Term n -> Term n
+  Pi     : WithBounds String -> WithBounds (Term n) -> WithBounds (Term (S n)) -> Term n
+  Lambda : WithBounds String -> WithBounds (Term (S n)) -> Term n
+  App    : WithBounds (Term n) -> WithBounds (Term n) -> Term n
   -- Dependent Sums
-  Sigma  : Bounds -> String -> Term n -> Term (S n) -> Term n
-  Pair   : Bounds -> Term n -> Term n -> Term n
-  Fst    : Bounds -> Term n -> Term n
-  Snd    : Bounds -> Term n -> Term n
+  Sigma  : WithBounds String -> WithBounds (Term n) -> WithBounds (Term (S n)) -> Term n
+  Pair   : WithBounds (Term n) -> WithBounds (Term n) -> Term n
+  Fst    : WithBounds (Term n) -> Term n
+  Snd    : WithBounds (Term n) -> Term n
   -- True
-  Top    : Bounds -> Term n
-  Point  : Bounds -> Term n
+  Top    : Term n
+  Point  : Term n
   -- False
-  Bottom : Bounds -> Term n
-  Absurd : Bounds -> Term n -> Term n -> Term n
+  Bottom : Term n
+  Absurd : WithBounds (Term n) -> WithBounds (Term n) -> Term n
   -- Equality
-  Equal  : Bounds -> Term n -> Term n -> Term n
-  Refl   : Bounds -> Term n -> Term n
-  Transp : Bounds -> Term n -> Term n -> Term n -> Term n -> Term n -> Term n
-  Cast   : Bounds -> Term n -> Term n -> Term n -> Term n
-  CastId : Bounds -> Term n -> Term n
+  Equal  : WithBounds (Term n) -> WithBounds (Term n) -> Term n
+  Refl   : WithBounds (Term n) -> Term n
+  Transp : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n
+  Cast   : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n
+  CastId : WithBounds (Term n) -> Term n
 
 public export
 record Definition (n : Nat) where
   constructor MkDefinition
-  bounds : Bounds -- of the name
-  name   : String
-  ty     : Term n
-  tm     : Term n
+  name   : WithBounds String
+  ty     : WithBounds (Term n)
+  tm     : WithBounds (Term n)
 
 public export
 data Block : Nat -> Type where
   Nil  : Block 0
   (:<) : Block n -> Definition n -> Block (S n)
 
--- Operations ------------------------------------------------------------------
+-- Pretty Print ----------------------------------------------------------------
 
-export
-fullBounds : Term n -> WithBounds (Term n)
-fullBounds tm@(Var var i) = map (\_ => tm) var
-fullBounds tm@(Sort x s) = MkBounded tm False x
-fullBounds tm@(Pi x var a b) = mergeBounds (mergeBounds (fullBounds a) (fullBounds b)) (MkBounded tm False x)
-fullBounds tm@(Lambda x var t) = mergeBounds (fullBounds t) (MkBounded tm False x)
-fullBounds tm@(App t u) = map (\_ => tm) (mergeBounds (fullBounds t) (fullBounds u))
-fullBounds tm@(Sigma x var a b) = mergeBounds (mergeBounds (fullBounds a) (fullBounds b)) (MkBounded tm False x)
-fullBounds tm@(Pair x t u) = mergeBounds (mergeBounds (fullBounds t) (fullBounds u)) (MkBounded tm False x)
-fullBounds tm@(Fst x t) = mergeBounds (fullBounds t) (MkBounded tm False x)
-fullBounds tm@(Snd x t) = mergeBounds (fullBounds t) (MkBounded tm False x)
-fullBounds tm@(Top x) = MkBounded tm False x
-fullBounds tm@(Point x) = MkBounded tm False x
-fullBounds tm@(Bottom x) = MkBounded tm False x
-fullBounds tm@(Absurd x a t) = mergeBounds (mergeBounds (fullBounds a) (fullBounds t)) (MkBounded tm False x)
-fullBounds tm@(Equal x t u) = mergeBounds (mergeBounds (fullBounds t) (fullBounds u)) (MkBounded tm False x)
-fullBounds tm@(Refl x t) = mergeBounds (fullBounds t) (MkBounded tm False x)
-fullBounds tm@(Transp x t b u t' e) = mergeBounds (mergeBounds (mergeBounds (fullBounds t) (fullBounds b)) (mergeBounds (fullBounds u) (fullBounds t'))) (mergeBounds (fullBounds e) (MkBounded tm False x))
-fullBounds tm@(Cast x b e t) = mergeBounds (mergeBounds (fullBounds b) (fullBounds e)) (mergeBounds (fullBounds t) (MkBounded tm False x))
-fullBounds tm@(CastId x t) = mergeBounds (fullBounds t) (MkBounded tm False x)
+prettyPrec : Prec -> Term n -> Doc ann
+prettyPrecBounds : Prec -> WithBounds (Term n) -> Doc ann
 
--- Pretty Print ----------------------------------------------------------------
+prettyPrec d (Var var _) = pretty var
+prettyPrec d (Sort s) = prettyPrec d s
+prettyPrec d (Pi var a b) =
+  parenthesise (d > Open) $
+  group $
+  parens (pretty var.val <++> colon <+> softline <+> prettyPrecBounds Open a) <++>
+  pretty "->" <+> softline <+>
+  prettyPrecBounds Open b
+prettyPrec d (Lambda var t) =
+  parenthesise (d > Open) $
+  group $
+  backslash <+> pretty var.val <++>
+  pretty "=>" <+> softline <+>
+  prettyPrecBounds Open t
+prettyPrec d (App t u) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [prettyPrecBounds Open t, prettyPrecBounds App u]
+prettyPrec d (Sigma var a b) =
+  parenthesise (d >= App) $
+  group $
+  parens (pretty var.val <++> colon <+> softline <+> prettyPrecBounds Open a) <++>
+  pretty "**" <+> softline <+>
+  prettyPrecBounds Open b
+prettyPrec d (Pair t u) =
+  angles $
+  group $
+  neutral <++> prettyPrecBounds Open t <+> comma <+> softline <+> prettyPrecBounds Open u <++> neutral
+prettyPrec d (Fst t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "fst", prettyPrecBounds App t]
+prettyPrec d (Snd t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "snd", prettyPrecBounds App t]
+prettyPrec d Top = pretty "()"
+prettyPrec d Point = pretty "tt"
+prettyPrec d Bottom = pretty "Void"
+prettyPrec d (Absurd a t) =
+  parenthesise (d > Open) $
+  group $
+  fillSep [pretty "absurd", prettyPrecBounds App a, prettyPrecBounds App t]
+prettyPrec d (Equal t u) =
+  parenthesise (d >= Equal) $
+  group $
+  prettyPrecBounds Equal t <++> pretty "~" <+> softline <+> prettyPrecBounds Equal u
+prettyPrec d (Refl t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "refl", prettyPrecBounds App t]
+prettyPrec d (Transp t b u t' e) =
+  parenthesise (d >= App) $
+  group $
+  fillSep $
+  [ pretty "transp"
+  , prettyPrecBounds App t
+  , prettyPrecBounds App b
+  , prettyPrecBounds App u
+  , prettyPrecBounds App t'
+  , prettyPrecBounds App e
+  ]
+prettyPrec d (Cast b e t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "cast", prettyPrecBounds App b, prettyPrecBounds App e, prettyPrecBounds App t]
+prettyPrec d (CastId t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "castRefl", prettyPrecBounds App t]
+
+prettyPrecBounds d (MkBounded v _ _) = prettyPrec d v
 
 export
 Pretty (Term n) where
-  prettyPrec d (Var var _) = pretty var.val
-  prettyPrec d (Sort _ s) = prettyPrec d s
-  prettyPrec d (Pi _ var a b) =
-    parenthesise (d > Open) $
-    group $
-    parens (pretty var <++> colon <+> softline <+> prettyPrec Open a) <++>
-    pretty "->" <+> softline <+>
-    prettyPrec Open b
-  prettyPrec d (Lambda _ var t) =
-    parenthesise (d > Open) $
-    group $
-    backslash <+> pretty var <++>
-    pretty "=>" <+> softline <+>
-    prettyPrec Open t
-  prettyPrec d (App t u) =
-    parenthesise (d >= App) $
-    group $
-    fillSep [prettyPrec Open t, prettyPrec App u]
-  prettyPrec d (Sigma _ var a b) =
-    parenthesise (d >= App) $
-    group $
-    parens (pretty var <++> colon <+> softline <+> prettyPrec Open a) <++>
-    pretty "**" <+> softline <+>
-    prettyPrec Open b
-  prettyPrec d (Pair _ t u) =
-    angles $
-    group $
-    neutral <++> prettyPrec Open t <+> comma <+> softline <+> prettyPrec Open u <++> neutral
-  prettyPrec d (Fst _ t) =
-    parenthesise (d >= App) $
-    group $
-    fillSep [pretty "fst", prettyPrec App t]
-  prettyPrec d (Snd _ t) =
-    parenthesise (d >= App) $
-    group $
-    fillSep [pretty "snd", prettyPrec App t]
-  prettyPrec d (Top _) = pretty "()"
-  prettyPrec d (Point _) = pretty "tt"
-  prettyPrec d (Bottom _) = pretty "Void"
-  prettyPrec d (Absurd _ a t) =
-    parenthesise (d > Open) $
-    group $
-    fillSep [pretty "absurd", prettyPrec App a, prettyPrec App t]
-  prettyPrec d (Equal _ t u) =
-    parenthesise (d >= Equal) $
-    group $
-    prettyPrec Equal t <++> pretty "~" <+> softline <+> prettyPrec Equal u
-  prettyPrec d (Refl _ t) =
-    parenthesise (d >= App) $
-    group $
-    fillSep [pretty "refl", prettyPrec App t]
-  prettyPrec d (Transp _ t b u t' e) =
-    parenthesise (d >= App) $
-    group $
-    fillSep $
-    [ pretty "transp"
-    , prettyPrec App t
-    , prettyPrec App b
-    , prettyPrec App u
-    , prettyPrec App t'
-    , prettyPrec App e
-    ]
-  prettyPrec d (Cast _ b e t) =
-    parenthesise (d >= App) $
-    group $
-    fillSep [pretty "cast", prettyPrec App b, prettyPrec App e, prettyPrec App t]
-  prettyPrec d (CastId _ t) =
-    parenthesise (d >= App) $
-    group $
-    fillSep [pretty "castRefl", prettyPrec App t]
+  prettyPrec = Term.prettyPrec
 
 export
 Pretty (Definition n) where
   pretty def = group $
-    pretty def.name <++> colon <+> softline <+> pretty def.ty <+> hardline <+>
-    pretty def.name <++> equals <+> softline <+> pretty def.tm
+    pretty def.name.val <++> colon <+> softline <+> pretty def.ty.val <+> hardline <+>
+    pretty def.name.val <++> equals <+> softline <+> pretty def.tm.val
 
 export
 Pretty (Block n) where
diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr
index 834dbb7..3ec91f7 100644
--- a/src/Obs/Typing.idr
+++ b/src/Obs/Typing.idr
@@ -335,178 +335,175 @@ asSubst (ctx ::< _)              (FS i) = map (weaken 1) (asSubst ctx i)
 -- Checking and Inference ------------------------------------------------------
 
 covering partial
-check : TyContext m n -> Term n -> NormalForm n -> Sort -> Logging ann (NormalForm n)
+check : TyContext m n -> WithBounds (Term n) -> NormalForm n -> Sort -> Logging ann (NormalForm n)
 covering partial
-infer : TyContext m n -> Term n -> Logging ann (NormalForm n, NormalForm n, Sort)
+infer : TyContext m n -> WithBounds (Term n) -> Logging ann (NormalForm n, NormalForm n, Sort)
 covering partial
 inferType : {default typeMismatch tag : forall a . Bounds -> Doc ann -> Doc ann -> Logging ann a}
-  -> TyContext m n -> Term n -> Logging ann (NormalForm n, Sort)
-
-check ctx tm@(Lambda _ _ t) (Cnstr (Pi s s' var a b)) _ = do
-  inScope "check" $ trace $ map (\_ => pretty {ann} "checking under lambda with type" <++> pretty a) (fullBounds tm)
-  inScope "check" $ trace $ map (\_ => "binding new variable to \{var}") (fullBounds tm)
-  inScope "check" $ trace $ map (\_ => pretty {ann} "checking for type" <++> pretty b) (fullBounds tm)
-  t <- check (ctx ::< (var, a, s)) t b s'
-  case s' of
-    Prop => pure Irrel
-    _ => pure (Cnstr $ Lambda var t)
-check ctx tm@(Lambda _ _ _) ty _ = typeMismatch (fullBounds tm).bounds (pretty "pi") (pretty ty)
-check ctx tm@(Pair _ t u) (Cnstr (Sigma s s' var a b)) _ = do
-  inScope "check" $ trace $ map (\_ => "checking pair") (fullBounds tm)
-  inScope "check" $ trace $ map (\_ => pretty {ann} "checking first for type" <++> pretty a) (fullBounds tm)
-  t <- check ctx t a s
-  b <- subst1 t b
-  inScope "check" $ trace $ map (\_ => pretty {ann} "checking second for type" <++> pretty b) (fullBounds tm)
-  u <- check ctx u b s'
-  inScope "check" $ trace $ map (\_ => pretty {ann} "pair is well typed") (fullBounds tm)
-  case (s, s') of
-    (Prop, Prop) => pure Irrel
-    _ => pure (Cnstr $ Pair t u)
-check ctx tm@(Pair _ _ _) ty _ = typeMismatch (fullBounds tm).bounds (pretty "sigma") (pretty ty)
-check ctx tm ty s = do
-  let bounded = fullBounds tm
-  inScope "check" $ trace $ map (\_ => "checking has fallen through") bounded
-  (tm, ty', s') <- infer ctx tm
-  inScope "check" $ trace $ map (\_ => pretty {ann} "inferred type is" <++> pretty ty') bounded
-  let True = s == s'
-    | False => sortMismatch bounded.bounds (pretty s) (pretty s')
-  True <- convert !(subst ty $ asSubst ctx) !(subst ty' $ asSubst ctx) (cast s) (suc s)
-    | False => typeMismatch bounded.bounds (pretty ty) (pretty ty')
-  inScope "check" $ trace $ map (\_ => pretty {ann} "converted" <++> pretty ty' <+> softline <+> pretty "to" <++> pretty ty) bounded
-  pure tm
-
-infer ctx tm@(Var b i) = do
-  inScope "infer" $ trace $ map (\_ => "encountered variable \{b.val}@\{show i}") (fullBounds tm)
-  let (t, a, s) = index ctx i
-  inScope "infer" $ trace $ map (\_ => pretty {ann} "variable has type" <++> pretty a) (fullBounds tm)
-  pure (t, a, s)
-infer ctx (Sort b s) = pure (cast s, cast (suc s), suc (suc s))
-infer ctx tm@(Pi _ var a b) = do
-  inScope "infer" $ trace $ map (\_ => "encountered Pi type") (fullBounds tm)
-  (a, s) <- inferType ctx a
-  inScope "infer" $ trace $ map (\_ => pretty {ann} "argument has type" <++> pretty a) (fullBounds tm)
-  (b, s') <- inferType (ctx ::< (var, a, s)) b
-  inScope "infer" $ trace $ map (\_ => pretty {ann} "result has type" <++> pretty b <+> comma <+> softline <+> pretty "so Pi type has type" <++> pretty (s ~> s')) (fullBounds tm)
-  pure (Cnstr (Pi s s' var a b), cast (s ~> s'), suc (s ~> s'))
-infer ctx tm@(Lambda _ _ _) = inScope "cannot infer type" $ fatal (fullBounds tm)
-infer ctx tm@(App t u) = do
-  inScope "infer" $ trace $ map (\_ => "encountered application") (fullBounds tm)
-  let bounded = fullBounds t
-  (t, ty@(Cnstr (Pi s s' _ a b)), _) <- infer ctx t
-    | (_, t, _) => inScope "wrong type to apply" $ fatal (map (\_ => t) bounded)
-  inScope "infer" $ trace $ map (\_ => pretty {ann} "function has type" <++> pretty ty) (fullBounds tm)
-  inScope "infer" $ trace $ map (\_ => pretty {ann} "checking argument has type" <++> pretty a) (fullBounds tm)
-  u <- check ctx u a s
-  inScope "infer" $ trace $ map (\_ => "argument is well typed") (fullBounds tm)
-  res <- doApp t u
-  ty <- subst1 u b
-  inScope "infer" $ trace $ map (\_ => pretty {ann} "final result is" <++> pretty res <+> softline <+> pretty "of type" <++> pretty ty) (fullBounds tm)
-  pure (res, ty, s')
-infer ctx tm@(Sigma _ var a b) = do
-  inScope "infer" $ trace $ map (\_ => "encountered Sigma type") (fullBounds tm)
-  (a, s) <- inferType ctx a
-  inScope "infer" $ trace $ map (\_ => pretty {ann} "first has type" <++> pretty a) (fullBounds tm)
-  (b, s') <- inferType (ctx ::< (var, a, s)) b
-  inScope "infer" $ trace $ map (\_ => pretty {ann} "second has type" <++> pretty b <+> comma <+> softline <+> pretty "so Sigma type has type" <++> pretty (lub s s')) (fullBounds tm)
-  pure (Cnstr (Sigma s s' var a b), cast (lub s s'), suc (lub s s'))
-infer ctx tm@(Pair _ _ _) = inScope "cannot infer type" $ fatal (fullBounds tm)
-infer ctx tm@(Fst _ t) = do
-  inScope "infer" $ trace $ map (\_ => "encountered first projection") (fullBounds tm)
-  let bounded = fullBounds t
-  (t, ty@(Cnstr (Sigma s s' _ a b)), _) <- infer ctx t
-    | (_, t, _) => inScope "wrong type to fst" $ fatal (map (\_ => t) bounded)
-  inScope "infer" $ trace $ map (\_ => pretty {ann} "pair has type" <++> pretty ty) (fullBounds tm)
-  res <- doFst t
-  inScope "infer" $ trace $ map (\_ => pretty {ann} "final result is" <++> pretty res <+> softline <+> pretty "of type" <++> pretty a) (fullBounds tm)
-  pure (res, a, s)
-infer ctx tm@(Snd _ t) = do
-  inScope "infer" $ trace $ map (\_ => "encountered first projection") (fullBounds tm)
-  let bounded = fullBounds t
-  (t, ty@(Cnstr (Sigma s s' _ a b)), _) <- infer ctx t
-    | (_, t, _) => inScope "wrong type to fst" $ fatal (map (\_ => t) bounded)
-  inScope "infer" $ trace $ map (\_ => pretty {ann} "pair has type" <++> pretty ty) (fullBounds tm)
-  t1 <- doFst t
-  res <- doSnd t
-  b <- subst1 t1 b
-  inScope "infer" $ trace $ map (\_ => pretty {ann} "final result is" <++> pretty res <+> softline <+> pretty "of type" <++> pretty b) (fullBounds tm)
-  pure (res, b, s')
-infer ctx (Top b) = pure $ (Cnstr Top, cast Prop, Set 0)
-infer ctx (Point b) = pure $ (Irrel, Cnstr Top, Prop)
-infer ctx (Bottom b) = pure $ (Cnstr Bottom, cast Prop, Set 0)
-infer ctx tm@(Absurd b a t) = do
-  inScope "infer" $ trace $ map (\_ => "encountered absurd") (fullBounds tm)
-  (a, s) <- inferType ctx a
-  inScope "infer" $ trace $ map (\_ => pretty {ann} "will fudge to type" <++> pretty a) (fullBounds tm)
-  inScope "infer" $ trace $ map (\_ => pretty {ann} "checking for proof of false") (fullBounds tm)
-  _ <- check ctx t (Cnstr Bottom) Prop
-  inScope "infer" $ trace $ map (\_ => "proof of false is well typed") (fullBounds tm)
-  pure (Ntrl Absurd, a, s)
-infer ctx tm@(Equal b t u) = do
-  inScope "infer" $ trace $ map (\_ => "encountered equal") (fullBounds tm)
-  (t, a, s) <- infer ctx t
-  inScope "infer" $ trace $ map (\_ => pretty {ann} "lhs has type" <++> pretty a) (fullBounds tm)
-  inScope "infer" $ trace $ map (\_ => "checking rhs has same type") (fullBounds tm)
-  u <- check ctx u a s
-  inScope "infer" $ trace $ map (\_ => "rhs is well typed") (fullBounds tm)
-  res <- doEqual a t u
-  inScope "infer" $ trace $ map (\_ => pretty {ann} "equality computes to" <++> pretty res) (fullBounds tm)
-  pure (res, cast Prop, Set 0)
-infer ctx tm@(Refl b t) = do
-  inScope "infer" $ trace $ map (\_ => "encountered refl") (fullBounds tm)
-  (t, a, s) <- infer ctx t
-  inScope "infer" $ trace $ map (\_ => pretty {ann} "term has type" <++> pretty a) (fullBounds tm)
-  ty <- doEqual a t t
-  inScope "infer" $ trace $ map (\_ => pretty {ann} "equality computes to" <++> pretty ty) (fullBounds tm)
-  pure (Irrel, ty, Prop)
-infer ctx tm@(Transp _ t b u t' e) = do
-  inScope "infer" $ trace $ map (\_ => "encountered transp") (fullBounds tm)
-  (t, a, s) <- infer ctx t
-  inScope "infer" $ trace $ map (\_ => pretty {ann} "start index has type" <++> pretty a) (fullBounds tm)
-  inScope "infer" $ trace $ map (\_ => "checking end index has same type") (fullBounds tm)
-  t' <- check ctx t' a s
-  inScope "infer" $ trace $ map (\_ => "end index is well typed") (fullBounds tm)
-  let bounded = fullBounds b
-  let ty = Cnstr (Pi s (Set 0) "_" a (cast Prop))
-  inScope "infer" $ trace $ map (\_ => pretty {ann} "checkout output is in" <++> pretty ty) (fullBounds tm)
-  b <- check ctx b ty s
-  inScope "infer" $ trace $ map (\_ => pretty {ann} "output is well typed") (fullBounds tm)
-  inScope "infer" $ trace $ map (\_ => "checking equality type") (fullBounds tm)
-  eq <- doEqual a t t'
-  _ <- check ctx e eq Prop
-  inScope "infer" $ trace $ map (\_ => "equality is well typed") (fullBounds tm)
-  inScope "infer" $ trace $ map (\_ => "checking transformed value") (fullBounds tm)
-  inTy <- doApp b t
-  _ <- check ctx u inTy Prop
-  inScope "infer" $ trace $ map (\_ => "transformed value is well typed") (fullBounds tm)
-  outTy <- doApp b t'
-  inScope "infer" $ trace $ map (\_ => pretty {ann} "producing value of type" <++> pretty outTy) (fullBounds tm)
-  pure (Irrel, outTy, Prop)
-infer ctx tm@(Cast _ b e t) = do
-  inScope "infer" $ trace $ map (\_ => "encountered cast") (fullBounds tm)
-  (t, a, s) <- infer ctx t
-  inScope "infer" $ trace $ map (\_ => pretty {ann} "input has type" <++> pretty a) (fullBounds tm)
-  inScope "infer" $ trace $ map (\_ => "checking output has same sort") (fullBounds tm)
-  b <- check ctx b (cast s) (suc s)
-  inScope "infer" $ trace $ map (\_ => "output is well sorted") (fullBounds tm)
-  inScope "infer" $ trace $ map (\_ => "checking equality type") (fullBounds tm)
-  eq <- doEqual (cast s) a b
-  _ <- check ctx e eq Prop
-  inScope "infer" $ trace $ map (\_ => "equality is well typed") (fullBounds tm)
-  inScope "infer" $ trace $ map (\_ => pretty {ann} "producing value of type" <++> pretty b) (fullBounds tm)
-  res <- doCastL a b t
-  pure (res, b, s)
-infer ctx tm@(CastId _ t) = do
-  inScope "infer" $ trace $ map (\_ => "encountered cast identity proof") (fullBounds tm)
-  (t, a, s) <- infer ctx t
-  inScope "infer" $ trace $ map (\_ => pretty {ann} "term has type" <++> pretty a) (fullBounds tm)
-  cast <- doCastL a a t
-  eq <- doEqual a cast t
-  inScope "infer" $ trace $ map (\_ => pretty {ann} "producing equality type" <++> pretty eq) (fullBounds tm)
-  pure (Irrel, eq, Prop)
+  -> TyContext m n -> WithBounds (Term n) -> Logging ann (NormalForm n, Sort)
+
+check ctx tm ty s = case (tm.val, ty) of
+  (Lambda _ t, Cnstr (Pi s s' var a b)) => do
+    inScope "check" $ trace $ map (\_ => pretty {ann} "checking under lambda with type" <++> pretty a) tm
+    inScope "check" $ trace $ map (\_ => "binding new variable to \{var}") tm
+    inScope "check" $ trace $ map (\_ => pretty {ann} "checking for type" <++> pretty b) tm
+    t <- check (ctx ::< (var, a, s)) t b s'
+    case s' of
+      Prop => pure Irrel
+      _ => pure (Cnstr $ Lambda var t)
+  (Lambda _ _, ty) => typeMismatch tm.bounds (pretty "pi") (pretty ty)
+  (Pair t u, Cnstr (Sigma s s' var a b)) => do
+    inScope "check" $ trace $ map (\_ => "checking pair") tm
+    inScope "check" $ trace $ map (\_ => pretty {ann} "checking first for type" <++> pretty a) tm
+    t <- check ctx t a s
+    b <- subst1 t b
+    inScope "check" $ trace $ map (\_ => pretty {ann} "checking second for type" <++> pretty b) tm
+    u <- check ctx u b s'
+    inScope "check" $ trace $ map (\_ => pretty {ann} "pair is well typed") tm
+    case (s, s') of
+      (Prop, Prop) => pure Irrel
+      _ => pure (Cnstr $ Pair t u)
+  (Pair _ _, ty) => typeMismatch tm.bounds (pretty "sigma") (pretty ty)
+  (_, _) => do
+    inScope "check" $ trace $ map (\_ => "checking has fallen through") tm
+    (v, a, s') <- infer ctx tm
+    inScope "check" $ trace $ map (\_ => pretty {ann} "inferred type is" <++> pretty a) tm
+    let True = s == s'
+      | False => sortMismatch tm.bounds (pretty s) (pretty s')
+    True <- convert !(subst ty $ asSubst ctx) !(subst a $ asSubst ctx) (cast s) (suc s)
+      | False => typeMismatch tm.bounds (pretty ty) (pretty a)
+    inScope "check" $ trace $ map (\_ => pretty {ann} "converted" <++> pretty a <+> softline <+> pretty "to" <++> pretty ty) tm
+    pure v
+
+infer ctx tm = case tm.val of
+  (Var var i) => do
+    inScope "infer" $ trace $ map (\_ => "encountered variable \{var}@\{show i}") tm
+    let (t, a, s) = index ctx i
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "variable has type" <++> pretty a) tm
+    pure (t, a, s)
+  (Sort s) => pure (cast s, cast (suc s), suc (suc s))
+  (Pi var a b) => do
+    inScope "infer" $ trace $ map (\_ => "encountered Pi type") tm
+    (a, s) <- inferType ctx a
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "argument has type" <++> pretty a) tm
+    (b, s') <- inferType (ctx ::< (var.val, a, s)) b
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "result has type" <++> pretty b <+> comma <+> softline <+> pretty "so Pi type has type" <++> pretty (s ~> s')) tm
+    pure (Cnstr (Pi s s' var.val a b), cast (s ~> s'), suc (s ~> s'))
+  (Lambda _ _) => inScope "cannot infer type" $ fatal tm
+  (App t u) => do
+    inScope "infer" $ trace $ map (\_ => "encountered application") tm
+    (t, ty@(Cnstr (Pi s s' _ a b)), _) <- infer ctx t
+      | (_, ty, _) => inScope "wrong type to apply" $ fatal (map (\_ => ty) tm)
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "function has type" <++> pretty ty) tm
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "checking argument has type" <++> pretty a) tm
+    u <- check ctx u a s
+    inScope "infer" $ trace $ map (\_ => "argument is well typed") tm
+    res <- doApp t u
+    ty <- subst1 u b
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "final result is" <++> pretty res <+> softline <+> pretty "of type" <++> pretty ty) tm
+    pure (res, ty, s')
+  (Sigma var a b) => do
+    inScope "infer" $ trace $ map (\_ => "encountered Sigma type") tm
+    (a, s) <- inferType ctx a
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "first has type" <++> pretty a) tm
+    (b, s') <- inferType (ctx ::< (var.val, a, s)) b
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "second has type" <++> pretty b <+> comma <+> softline <+> pretty "so Sigma type has type" <++> pretty (lub s s')) tm
+    pure (Cnstr (Sigma s s' var.val a b), cast (lub s s'), suc (lub s s'))
+  (Pair _ _) => inScope "cannot infer type" $ fatal tm
+  (Fst t) => do
+    inScope "infer" $ trace $ map (\_ => "encountered first projection") tm
+    (t, ty@(Cnstr (Sigma s s' _ a b)), _) <- infer ctx t
+      | (_, ty, _) => inScope "wrong type to fst" $ fatal (map (\_ => ty) tm)
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "pair has type" <++> pretty ty) tm
+    res <- doFst t
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "final result is" <++> pretty res <+> softline <+> pretty "of type" <++> pretty a) tm
+    pure (res, a, s)
+  (Snd t) => do
+    inScope "infer" $ trace $ map (\_ => "encountered first projection") tm
+    (t, ty@(Cnstr (Sigma s s' _ a b)), _) <- infer ctx t
+      | (_, ty, _) => inScope "wrong type to fst" $ fatal (map (\_ => ty) tm)
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "pair has type" <++> pretty ty) tm
+    t1 <- doFst t
+    res <- doSnd t
+    b <- subst1 t1 b
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "final result is" <++> pretty res <+> softline <+> pretty "of type" <++> pretty b) tm
+    pure (res, b, s')
+  Top => pure $ (Cnstr Top, cast Prop, Set 0)
+  Point => pure $ (Irrel, Cnstr Top, Prop)
+  Bottom  => pure $ (Cnstr Bottom, cast Prop, Set 0)
+  (Absurd a t) => do
+    inScope "infer" $ trace $ map (\_ => "encountered absurd") tm
+    (a, s) <- inferType ctx a
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "will fudge to type" <++> pretty a) tm
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "checking for proof of false") tm
+    _ <- check ctx t (Cnstr Bottom) Prop
+    inScope "infer" $ trace $ map (\_ => "proof of false is well typed") tm
+    pure (Ntrl Absurd, a, s)
+  (Equal t u) => do
+    inScope "infer" $ trace $ map (\_ => "encountered equal") tm
+    (t, a, s) <- infer ctx t
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "lhs has type" <++> pretty a) tm
+    inScope "infer" $ trace $ map (\_ => "checking rhs has same type") tm
+    u <- check ctx u a s
+    inScope "infer" $ trace $ map (\_ => "rhs is well typed") tm
+    res <- doEqual a t u
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "equality computes to" <++> pretty res) tm
+    pure (res, cast Prop, Set 0)
+  (Refl t) => do
+    inScope "infer" $ trace $ map (\_ => "encountered refl") tm
+    (t, a, s) <- infer ctx t
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "term has type" <++> pretty a) tm
+    ty <- doEqual a t t
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "equality computes to" <++> pretty ty) tm
+    pure (Irrel, ty, Prop)
+  (Transp t b u t' e) => do
+    inScope "infer" $ trace $ map (\_ => "encountered transp") tm
+    (t, a, s) <- infer ctx t
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "start index has type" <++> pretty a) tm
+    inScope "infer" $ trace $ map (\_ => "checking end index has same type") tm
+    t' <- check ctx t' a s
+    inScope "infer" $ trace $ map (\_ => "end index is well typed") tm
+    let ty = Cnstr (Pi s (Set 0) "_" a (cast Prop))
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "checkout output is in" <++> pretty ty) tm
+    b <- check ctx b ty s
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "output is well typed") tm
+    inScope "infer" $ trace $ map (\_ => "checking equality type") tm
+    eq <- doEqual a t t'
+    _ <- check ctx e eq Prop
+    inScope "infer" $ trace $ map (\_ => "equality is well typed") tm
+    inScope "infer" $ trace $ map (\_ => "checking transformed value") tm
+    inTy <- doApp b t
+    _ <- check ctx u inTy Prop
+    inScope "infer" $ trace $ map (\_ => "transformed value is well typed") tm
+    outTy <- doApp b t'
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "producing value of type" <++> pretty outTy) tm
+    pure (Irrel, outTy, Prop)
+  (Cast b e t) => do
+    inScope "infer" $ trace $ map (\_ => "encountered cast") tm
+    (t, a, s) <- infer ctx t
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "input has type" <++> pretty a) tm
+    inScope "infer" $ trace $ map (\_ => "checking output has same sort") tm
+    b <- check ctx b (cast s) (suc s)
+    inScope "infer" $ trace $ map (\_ => "output is well sorted") tm
+    inScope "infer" $ trace $ map (\_ => "checking equality type") tm
+    eq <- doEqual (cast s) a b
+    _ <- check ctx e eq Prop
+    inScope "infer" $ trace $ map (\_ => "equality is well typed") tm
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "producing value of type" <++> pretty b) tm
+    res <- doCastL a b t
+    pure (res, b, s)
+  (CastId t) => do
+    inScope "infer" $ trace $ map (\_ => "encountered cast identity proof") tm
+    (t, a, s) <- infer ctx t
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "term has type" <++> pretty a) tm
+    cast <- doCastL a a t
+    eq <- doEqual a cast t
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "producing equality type" <++> pretty eq) tm
+    pure (Irrel, eq, Prop)
 
 inferType ctx a = do
   (a, Cnstr (Sort s), _) <- infer ctx a
-    | (_, ty, _) => tag (fullBounds a).bounds (pretty "sort") (pretty ty)
+    | (_, ty, _) => tag a.bounds (pretty "sort") (pretty ty)
   pure (a, s)
 
 -- Checking Definitions and Blocks ---------------------------------------------
@@ -514,14 +511,12 @@ inferType ctx a = do
 covering partial
 checkDef : Context n -> Term.Definition n -> Logging ann (NormalForm.Definition n)
 checkDef ctx def = do
-  let tyBounds = (fullBounds def.ty).bounds
-  let tmBounds = (fullBounds def.tm).bounds
   (ty, sort) <-
     inferType {tag = \bounds, lhs, rhs => inScope "invalid declaration" $ mismatch bounds lhs rhs}
       (fromContext ctx) def.ty
-  inScope "check" $ debug (pretty {ann} "\{def.name} has type" <++> pretty ty)
+  inScope "check" $ debug $ map (\name => pretty {ann} "\{name} has type" <++> pretty ty) def.name
   tm <- check (fromContext ctx) def.tm ty sort
-  inScope "check" $ debug (pretty {ann} "\{def.name} is well typed with value" <++> pretty tm)
+  inScope "check" $ debug $ map (\name => pretty {ann} "\{name} is well typed with value" <++> pretty tm) def.name
   pure $ MkDefinition {name = def.name, ty, tm, sort}
 
 covering partial