diff --git a/lib/Quox/Context.idr b/lib/Quox/Context.idr
index d481a1d..a2cd868 100644
--- a/lib/Quox/Context.idr
+++ b/lib/Quox/Context.idr
@@ -6,6 +6,7 @@ import Quox.Pretty
 import Data.DPair
 import Data.Nat
 import Data.SnocList
+import Data.Vect
 import Control.Monad.Identity
 
 %default total
@@ -64,6 +65,13 @@ public export
 tel1 . [<]         = tel1
 tel1 . (tel2 :< s) = (tel1 . tel2) :< s
 
+export
+(<><) : Telescope' a from to -> Vect n a -> Telescope' a from (n + to)
+(<><) tel [] = tel
+(<><) tel (x :: xs) {n = S n} =
+  rewrite plusSuccRightSucc n to in
+  (tel :< x) <>< xs
+
 
 public export
 getShiftWith : (forall from, to. tm from -> Shift from to -> tm to) ->
diff --git a/lib/Quox/Name.idr b/lib/Quox/Name.idr
index 372c9f1..20d16d8 100644
--- a/lib/Quox/Name.idr
+++ b/lib/Quox/Name.idr
@@ -13,50 +13,85 @@ import Derive.Prelude
 public export
 data BaseName
 = UN String -- user-given name
+| Unused    -- "_"
 %runElab derive "BaseName" [Eq, Ord]
 
-export
-Show BaseName where
-  show (UN x) = x
-
-
 export
 baseStr : BaseName -> String
 baseStr (UN x) = x
+baseStr Unused = "_"
 
-export
-FromString BaseName where
-  fromString = UN
+export Show BaseName where show = baseStr
+export FromString BaseName where fromString = UN
+
+
+public export
+Mods : Type
+Mods = SnocList String
 
 
 public export
 record Name where
   constructor MakeName
-  mods : SnocList String
+  mods : Mods
   base : BaseName
 %runElab derive "Name" [Eq, Ord]
 
-export
-Show Name where
-  show (MakeName mods base) =
-    concat $ intersperse "." $ toList $ mods :< show base
-
-export
-FromString Name where
-  fromString x = MakeName [<] (fromString x)
-
 public export %inline
 unq : BaseName -> Name
 unq = MakeName [<]
 
+||| add some namespaces to the beginning of a name
+public export %inline
+addMods : Mods -> Name -> Name
+addMods ms = {mods $= (ms <+>)}
+
+
+public export
+PBaseName : Type
+PBaseName = String
+
+public export
+record PName where
+  constructor MakePName
+  mods : Mods
+  base : String
+%runElab derive "PName" [Eq, Ord]
+
+export %inline
+fromPName : PName -> Name
+fromPName p = MakeName p.mods $ UN p.base
+
+export %inline
+toPName : Name -> PName
+toPName p = MakePName p.mods $ baseStr p.base
+
+export
+Show PName where
+  show (MakePName mods base) = concat $ intersperse "." $ toList $ mods :< base
+
+export Show Name where show = show . toPName
+
+export FromString PName where fromString = MakePName [<]
+
+export FromString Name where fromString = fromPName . fromString
+
+
+export
+toDotsP : PName -> String
+toDotsP x = fastConcat $ cast $ map (<+> ".") x.mods :< x.base
 
 export
 toDots : Name -> String
 toDots x = fastConcat $ cast $ map (<+> ".") x.mods :< baseStr x.base
 
 export
-fromList : List1 String -> Name
-fromList (x ::: xs) = go [<] x xs where
-  go : SnocList String -> String -> List String -> Name
-  go mods x []        = MakeName mods (UN x)
+fromListP : List1 String -> PName
+fromListP (x ::: xs) = go [<] x xs where
+  go : SnocList String -> String -> List String -> PName
+  go mods x []        = MakePName mods x
   go mods x (y :: ys) = go (mods :< x) y ys
+
+export %inline
+fromList : List1 String -> Name
+fromList = fromPName . fromListP
diff --git a/lib/Quox/Parser.idr b/lib/Quox/Parser.idr
index 9276178..b9806fa 100644
--- a/lib/Quox/Parser.idr
+++ b/lib/Quox/Parser.idr
@@ -1,280 +1,6 @@
 module Quox.Parser
 
-import public Quox.Lexer
 import public Quox.Parser.Syntax
-
-import Data.Fin
-import Data.Vect
-import public Text.Parser
-
-%default total
-
-
-public export
-0 Grammar : Bool -> Type -> Type
-Grammar = Core.Grammar () Token
-%hide Core.Grammar
-
-
-export
-res : (str : String) -> (0 _ : IsReserved str) => Grammar True ()
-res str = terminal "expecting \"\{str}\"" $
-  \x => guard $ x == Reserved str
-
-export
-resC : (str : String) -> (0 _ : IsReserved str) => Grammar True ()
-resC str = do res str; commit
-
-
-parameters {default True commit : Bool}
-  private
-  maybeCommit : Grammar False ()
-  maybeCommit = when commit Core.commit
-
-  export
-  betweenR : {c : Bool} -> (op, cl : String) ->
-             (0 _ : IsReserved op) => (0 _ : IsReserved cl) =>
-             Grammar c a -> Grammar True a
-  betweenR o c p = res o *> maybeCommit *> p <* res c <* maybeCommit
-
-  export
-  parens, bracks, braces : {c : Bool} -> Grammar c a -> Grammar True a
-  parens = betweenR "(" ")"
-  bracks = betweenR "[" "]"
-  braces = betweenR "{" "}"
-
-
-export
-commaSep : {c : Bool} -> Grammar c a -> Grammar False (List a)
-commaSep = sepEndBy (res ",")
-  -- don't commit because of the possible terminating ","
-
-export
-semiSep : {c : Bool} -> Grammar c a -> Grammar False (List a)
-semiSep = sepEndBy (res ";")
-
-export
-commaSep1 : {c : Bool} -> Grammar c a -> Grammar c (List1 a)
-commaSep1 = sepEndBy1 (res ",")
-
-export
-darr : Grammar True ()
-darr = resC "⇒"
-
-
-export
-name : Grammar True Name
-name = terminal "expecting name" $
-  \case Name i => Just i; _ => Nothing
-
-export
-baseName : Grammar True BaseName
-baseName = terminal "expecting unqualified name" $
-  \case Name i => guard (null i.mods) $> i.base
-        _      => Nothing
-
-export
-nat : Grammar True Nat
-nat = terminal "expecting natural number" $
-  \case Nat n => pure n; _ => Nothing
-
-export
-string : Grammar True String
-string = terminal "expecting string literal" $
-  \case Str s => pure s; _ => Nothing
-
-export
-tag : Grammar True String
-tag = terminal "expecting tag constructor" $
-  \case Tag t => pure t; _ => Nothing
-
-export
-bareTag : Grammar True String
-bareTag = string <|> [|toDots name|]
-
-export
-universe : Grammar True PUniverse
-universe = terminal "expecting type universe" $
-  \case TYPE u => Just u; _ => Nothing
-
-export
-bname : Grammar True BName
-bname = Nothing <$ res "_"
-    <|> [|Just baseName|]
-
-export
-zeroOne : (zero, one : a) -> Grammar True a
-zeroOne zero one = terminal "expecting zero or one" $
-  \case Nat 0 => Just zero; Nat 1 => Just one; _ => Nothing
-
-
-export covering
-qty : Grammar True PQty
-qty = zeroOne Zero One
-  <|> Any <$ res "ω"
-  <|> parens qty
-
-private covering
-qtys : Grammar False (List PQty)
-qtys = option [] [|toList $ some qty <* res "·"|]
-
-export
-dimConst : Grammar True DimConst
-dimConst = zeroOne Zero One
-
-export covering
-dim : Grammar True PDim
-dim = [|V baseName|]
-  <|> [|K dimConst|]
-  <|> parens dim
-
-private
-0 PBinderHead : Nat -> Type
-PBinderHead n = (Vect n PQty, BName, PTerm)
-
-private
-toVect : List a -> (n ** Vect n a)
-toVect []        = (_ ** [])
-toVect (x :: xs) = (_ ** x :: snd (toVect xs))
-
-private
-0 MakeBinder : Nat -> Type
-MakeBinder n = (String, PBinderHead n -> PTerm -> PTerm)
-
-private
-makePi : MakeBinder 1
-makePi = ("→", \([pi], x, s) => Pi pi x s)
-
-private
-makeSig : MakeBinder 0
-makeSig = ("×", \([], x, s) => Sig x s)
-
-private
-makeBinder : {m, n : Nat} -> MakeBinder m -> PBinderHead n -> PTerm ->
-             Grammar False PTerm
-makeBinder (str, f) h t =
-  case decEq m n of
-    Yes Refl => pure $ f h t
-    No  _    =>
-      let q = if m == 1 then "quantity" else "quantities" in
-      fatalError "'\{str}' expects \{show m} \{q}, got \{show n}"
-
-private
-binderInfix : Grammar True (n ** MakeBinder n)
-binderInfix = res "→" $> (1 ** makePi)
-          <|> res "×" $> (0 ** makeSig)
-
-private
-lamIntro : Grammar True (BName -> PTerm -> PTerm)
-lamIntro = Lam  <$ resC "λ"
-       <|> DLam <$ resC "δ"
-
-private covering
-caseIntro : Grammar True PQty
-caseIntro = resC "case1" $> One
-        <|> resC "caseω" $> Any
-        <|> resC "case" *> qty <* resC "·"
-
-private
-optNameBinder : Grammar False BName
-optNameBinder = [|join $ optional $ bname <* darr|]
-
-mutual
-  export covering
-  term : Grammar True PTerm
-  term = lamTerm
-     <|> caseTerm
-     <|> bindTerm
-     <|> [|annotate infixEqTerm (optional $ resC "∷" *> term)|]
-  where
-    annotate : PTerm -> Maybe PTerm -> PTerm
-    annotate s a = maybe s (s :#) a
-
-  private covering
-  lamTerm : Grammar True PTerm
-  lamTerm = flip . foldr <$> lamIntro <*> some bname <* darr <*> term
-
-  private covering
-  caseTerm : Grammar True PTerm
-  caseTerm =
-    [|Case caseIntro term
-           (resC "return" *> optBinderTerm)
-           (resC "of"     *> braces caseBody)|]
-
-  private covering
-  caseBody : Grammar False PCaseBody
-  caseBody = [|CasePair (pairPat <* darr) (term <* optSemi)|]
-         <|> [|CaseEnum $ semiSep [|MkPair tag (darr *> term)|]|]
-  where
-    optSemi = ignore $ optional $ res ";"
-    pairPat = parens [|MkPair bname (resC "," *> bname)|]
-
-  private covering
-  bindTerm : Grammar True PTerm
-  bindTerm = do
-    bnd <- binderHead
-    inf <- binderInfix
-    body <- term
-    makeBinder (snd inf) (snd bnd) body
-
-  private covering
-  infixEqTerm : Grammar True PTerm
-  infixEqTerm = do
-    l <- appTerm
-    rty <- optional [|MkPair (resC "≡" *> term) (resC ":" *> appTerm)|]
-    pure $ maybe l (\rty => Eq (Nothing, snd rty) l (fst rty)) rty
-
-  private covering
-  appTerm : Grammar True PTerm
-  appTerm = resC "★"  *> [|TYPE nat|]
-        <|> resC "Eq" *> [|Eq (bracks optBinderTerm) aTerm aTerm|]
-        <|> [|apply aTerm (many appArg)|]
-  where
-    data PArg = TermArg PTerm | DimArg PDim
-
-    appArg : Grammar True PArg
-    appArg = [|DimArg $ resC "@" *> dim|]
-         <|> [|TermArg aTerm|]
-
-    apply : PTerm -> List PArg -> PTerm
-    apply = foldl apply1 where
-      apply1 : PTerm -> PArg -> PTerm
-      apply1 f (TermArg x) = f :@ x
-      apply1 f (DimArg  p) = f :% p
-
-  private covering
-  aTerm : Grammar True PTerm
-  aTerm = [|Enum $ braces $ commaSep bareTag|]
-      <|> [|TYPE universe|]
-      <|> [|V name|]
-      <|> [|Tag tag|]
-      <|> foldr1 Pair <$> parens (commaSep1 term)
-
-  private covering
-  binderHead : Grammar True (n ** PBinderHead n)
-  binderHead = parens {commit = False} $ do
-    qs <- [|toVect qtys|]
-    name <- bname
-    resC ":"
-    ty <- term
-    pure (qs.fst ** (qs.snd, name, ty))
-
-  private covering
-  optBinderTerm : Grammar True (BName, PTerm)
-  optBinderTerm = [|MkPair optNameBinder term|]
-
-
-export covering
-defIntro : Grammar True PQty
-defIntro = Zero <$ resC "def0"
-       <|> Any  <$ resC "defω"
-       <|> resC "def" *> option Any (qty <* resC "·")
-
-export covering
-definition : Grammar True PDefinition
-definition =
-  [|MkPDef defIntro name (resC ":" *> term) (resC "≔" *> term)|] <* resC ";"
-
-export covering
-input : Grammar False (List PDefinition)
-input = many definition
+import public Quox.Parser.Lexer
+import public Quox.Parser.Parser
+import public Quox.Parser.FromParser
diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr
new file mode 100644
index 0000000..136c0ca
--- /dev/null
+++ b/lib/Quox/Parser/FromParser.idr
@@ -0,0 +1,212 @@
+||| take freshly-parsed input, translate it to core, and check it
+module Quox.Parser.FromParser
+
+import Quox.Parser.Syntax
+import Quox.Typechecker
+import Data.List
+
+import public Control.Monad.Either
+import public Control.Monad.State
+import public Control.Monad.Reader
+
+
+public export
+data FromParserError =
+    AnnotationNeeded PTerm
+  | DuplicatesInEnum (List TagVal)
+  | DimNotInScope PBaseName
+  | QtyNotGlobal PQty
+  | DimNameInTerm PBaseName
+
+public export
+interface LoadFile m where
+  loadFile : (file : String) -> m PTopLevel
+
+public export
+0 CanError : (Type -> Type) -> Type
+CanError = MonadError FromParserError
+
+public export
+0 HasNamespace : (Type -> Type) -> Type
+HasNamespace = MonadReader Mods
+
+public export
+0 HasSeenFiles : (Type -> Type) -> Type
+HasSeenFiles = MonadState (SortedSet String)
+
+public export
+0 FromParser : (Type -> Type) -> Type
+FromParser m = (CanError m, HasNamespace m, HasSeenFiles m)
+
+
+
+parameters {auto _ : Functor m} (b : Var n -> m a) (f : PName -> m a)
+           (xs : Context' BName n)
+  private
+  fromBaseName : PBaseName -> m a
+  fromBaseName x = maybe (f $ MakePName [<] x) b $ Context.find (== Just x) xs
+
+  private
+  fromName : PName -> m a
+  fromName x = if null x.mods then fromBaseName x.base else f x
+
+export
+fromPDimWith : CanError m =>
+               Context' BName d -> PDim -> m (Dim d)
+fromPDimWith ds (K e) = pure $ K e
+fromPDimWith ds (V i) =
+  fromBaseName (pure . B) (const $ throwError $ DimNotInScope i) ds i
+
+private
+avoidDim : CanError m => Context' BName d -> PName -> m (Term q d n)
+avoidDim ds x =
+  fromName (const $ throwError $ DimNameInTerm x.base)
+           (pure . FT . fromPName) ds x
+
+
+mutual
+  export
+  fromPTermWith : CanError m =>
+                  Context' BName d -> Context' BName n ->
+                  PTerm -> m (Term Three d n)
+  fromPTermWith ds ns t0 = case t0 of
+    TYPE k =>
+      pure $ TYPE $ k
+
+    Pi pi x s t =>
+      Pi pi <$> fromPTermWith ds ns s
+            <*> fromPTermTScope ds ns [x] t
+
+    Lam x s =>
+      Lam <$> fromPTermTScope ds ns [x] s
+
+    s :@ t =>
+      map E $ (:@) <$> fromPTermElim ds ns s <*> fromPTermWith ds ns t
+
+    Sig x s t =>
+      Sig <$> fromPTermWith ds ns s <*> fromPTermTScope ds ns [x] t
+
+    Pair s t =>
+      Pair <$> fromPTermWith ds ns s <*> fromPTermWith ds ns t
+
+    Case pi pair (r, ret) (CasePair (x, y) body) =>
+      map E $ Base.CasePair pi
+        <$> fromPTermElim ds ns pair
+        <*> fromPTermTScope ds ns [r] ret
+        <*> fromPTermTScope ds ns [x, y] body
+
+    Case pi tag (r, ret) (CaseEnum arms) =>
+      map E $ Base.CaseEnum pi
+        <$> fromPTermElim ds ns tag
+        <*> fromPTermTScope ds ns [r] ret
+        <*> assert_total fromPTermEnumArms ds ns arms
+
+    Enum strs =>
+      let set = SortedSet.fromList strs in
+      if length strs == length (SortedSet.toList set) then
+        pure $ Enum set
+      else
+        throwError $ DuplicatesInEnum strs
+
+    Tag str => pure $ Tag str
+
+    Eq (i, ty) s t =>
+      Eq <$> fromPTermDScope ds ns [i] ty
+         <*> fromPTermWith ds ns s
+         <*> fromPTermWith ds ns t
+
+    DLam i s =>
+      DLam <$> fromPTermDScope ds ns [i] s
+
+    s :% p =>
+      map E $ (:%) <$> fromPTermElim ds ns s <*> fromPDimWith ds p
+
+    V x =>
+      fromName (pure . E . B) (avoidDim ds) ns x
+
+    s :# a =>
+      map E $ (:#) <$> fromPTermWith ds ns s <*> fromPTermWith ds ns a
+
+  private
+  fromPTermEnumArms : CanError m =>
+                      Context' BName d -> Context' BName n ->
+                      List (TagVal, PTerm) -> m (CaseEnumArms Three d n)
+  fromPTermEnumArms ds ns =
+    map SortedMap.fromList . traverse (traverse $ fromPTermWith ds ns)
+
+  private
+  fromPTermElim : CanError m =>
+                  Context' BName d -> Context' BName n ->
+                  PTerm -> m (Elim Three d n)
+  fromPTermElim ds ns e =
+    case !(fromPTermWith ds ns e) of
+      E e => pure e
+      _   => throwError $ AnnotationNeeded e
+
+  -- [todo] use SN if the var is named but still unused
+  private
+  fromPTermTScope : {s : Nat} -> CanError m =>
+                    Context' BName d -> Context' BName n ->
+                    Vect s BName ->
+                    PTerm -> m (ScopeTermN s Three d n)
+  fromPTermTScope ds ns xs t =
+    if all isNothing xs then
+      SN <$> fromPTermWith ds ns t
+    else
+      SY (map (maybe Unused UN) xs) <$> fromPTermWith ds (ns <>< xs) t
+
+  private
+  fromPTermDScope : {s : Nat} -> CanError m =>
+                    Context' BName d -> Context' BName n ->
+                    Vect s BName ->
+                    PTerm -> m (DScopeTermN s Three d n)
+  fromPTermDScope ds ns xs t =
+    if all isNothing xs then
+      SN <$> fromPTermWith ds ns t
+    else
+      SY (map (maybe Unused UN) xs) <$> fromPTermWith (ds <>< xs) ns t
+
+
+export %inline
+fromPTerm : CanError m => PTerm -> m (Term Three 0 0)
+fromPTerm = fromPTermWith [<] [<]
+
+
+export
+globalPQty : CanError m => (q : PQty) -> m (IsGlobal q)
+globalPQty pi = case isGlobal pi of
+  Yes y => pure y
+  No  n => throwError $ QtyNotGlobal pi
+
+
+
+-- -- [todo] extend substitutions so they can do this injection. that's the sort of
+-- -- thing they are for.
+-- export
+-- fromPDefinition : FromParser m => PDefinition -> m (Name, Definition Three)
+-- fromPDefinition (MkPDef {name, qty, type, term}) =
+--   pure (addMods !ask $ fromPName name, MkDef' {
+--     qty, qtyGlobal = !(globalPQty qty),
+--     type = T $ inject !(fromPTerm type),
+--     term = Just $ T $ inject !(fromPTerm term)
+--   })
+
+
+-- export
+-- fromPDecl : FromParser m => PDecl -> m (List (Name, Definition Three))
+-- fromPDecl (PDef def) = singleton <$> fromPDefinition def
+-- fromPDecl (PNs  ns)  = local (<+> ns.name) $
+--   concat <$> assert_total traverse fromPDecl ns.decls
+
+
+-- export covering
+-- fromPTopLevel : (FromParser m, LoadFile m) =>
+--                 PTopLevel -> m (List (Name, Definition Three))
+-- fromPTopLevel (PD decl)    = fromPDecl decl
+-- fromPTopLevel (PLoad file) =
+--   if contains file !get then
+--     pure []
+--   else do
+--     modify $ insert file
+--     t <- loadFile file
+--     fromPTopLevel t
diff --git a/lib/Quox/Lexer.idr b/lib/Quox/Parser/Lexer.idr
similarity index 97%
rename from lib/Quox/Lexer.idr
rename to lib/Quox/Parser/Lexer.idr
index 8144571..9c38a00 100644
--- a/lib/Quox/Lexer.idr
+++ b/lib/Quox/Parser/Lexer.idr
@@ -1,4 +1,4 @@
-module Quox.Lexer
+module Quox.Parser.Lexer
 
 import Quox.CharExtra
 import Quox.Name
@@ -25,7 +25,7 @@ import Derive.Prelude
 public export
 data Token =
     Reserved String
-  | Name Name
+  | Name PName
   | Nat Nat
   | Str String
   | Tag String
@@ -91,7 +91,7 @@ nameL = baseNameL <+> many (is '.' <+> baseNameL)
 
 private
 name : Tokenizer TokenW
-name = match nameL $ Name . fromList . split (== '.') . normalizeNfc
+name = match nameL $ Name . fromListP . split (== '.') . normalizeNfc
 
 ||| [todo] escapes other than `\"` and (accidentally) `\\`
 export
@@ -228,7 +228,9 @@ reserved =
    Word1 "def",
    Word1 "def0",
    Word "defω" `Or` Word "def#",
-   Sym "≔" `Or` Sym ":="]
+   Sym "≔" `Or` Sym ":=",
+   Word1 "load",
+   Word1 "namespace"]
 
 ||| `IsReserved str` is true if `Reserved str` might actually show up in
 ||| the token stream
diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr
new file mode 100644
index 0000000..cc61f64
--- /dev/null
+++ b/lib/Quox/Parser/Parser.idr
@@ -0,0 +1,328 @@
+module Quox.Parser.Parser
+
+import public Quox.Parser.Lexer
+import public Quox.Parser.Syntax
+
+import Data.Fin
+import Data.Vect
+import public Text.Parser
+
+%default total
+
+
+public export
+0 Grammar : Bool -> Type -> Type
+Grammar = Core.Grammar () Token
+%hide Core.Grammar
+
+
+export
+res : (str : String) -> (0 _ : IsReserved str) => Grammar True ()
+res str = terminal "expecting \"\{str}\"" $
+  \x => guard $ x == Reserved str
+
+export
+resC : (str : String) -> (0 _ : IsReserved str) => Grammar True ()
+resC str = do res str; commit
+
+
+parameters {default True commit : Bool}
+  private
+  maybeCommit : Grammar False ()
+  maybeCommit = when commit Core.commit
+
+  export
+  betweenR : {c : Bool} -> (op, cl : String) ->
+             (0 _ : IsReserved op) => (0 _ : IsReserved cl) =>
+             Grammar c a -> Grammar True a
+  betweenR o c p = res o *> maybeCommit *> p <* res c <* maybeCommit
+
+  export
+  parens, bracks, braces : {c : Bool} -> Grammar c a -> Grammar True a
+  parens = betweenR "(" ")"
+  bracks = betweenR "[" "]"
+  braces = betweenR "{" "}"
+
+
+export
+commaSep : {c : Bool} -> Grammar c a -> Grammar False (List a)
+commaSep = sepEndBy (res ",")
+  -- don't commit because of the possible terminating ","
+
+export
+semiSep : {c : Bool} -> Grammar c a -> Grammar False (List a)
+semiSep = sepEndBy (res ";")
+
+export
+commaSep1 : {c : Bool} -> Grammar c a -> Grammar c (List1 a)
+commaSep1 = sepEndBy1 (res ",")
+
+export
+darr : Grammar True ()
+darr = resC "⇒"
+
+
+export
+name : Grammar True PName
+name = terminal "expecting name" $
+  \case Name i => Just i; _ => Nothing
+
+export
+mods : Grammar True Mods
+mods = name <&> \n => n.mods :< n.base
+
+export
+baseName : Grammar True String
+baseName = terminal "expecting unqualified name" $
+  \case Name i => guard (null i.mods) $> i.base
+        _      => Nothing
+
+export
+nat : Grammar True Nat
+nat = terminal "expecting natural number" $
+  \case Nat n => pure n; _ => Nothing
+
+export
+string : Grammar True String
+string = terminal "expecting string literal" $
+  \case Str s => pure s; _ => Nothing
+
+export
+tag : Grammar True String
+tag = terminal "expecting tag constructor" $
+  \case Tag t => pure t; _ => Nothing
+
+export
+bareTag : Grammar True String
+bareTag = string <|> [|toDotsP name|]
+
+export
+universe : Grammar True PUniverse
+universe = terminal "expecting type universe" $
+  \case TYPE u => Just u; _ => Nothing
+
+export
+bname : Grammar True BName
+bname = Nothing <$ res "_"
+    <|> [|Just baseName|]
+
+export
+zeroOne : (zero, one : a) -> Grammar True a
+zeroOne zero one = terminal "expecting zero or one" $
+  \case Nat 0 => Just zero; Nat 1 => Just one; _ => Nothing
+
+
+export covering
+qty : Grammar True PQty
+qty = zeroOne Zero One
+  <|> Any <$ res "ω"
+  <|> parens qty
+
+private covering
+qtys : Grammar False (List PQty)
+qtys = option [] [|toList $ some qty <* res "·"|]
+
+export
+dimConst : Grammar True DimConst
+dimConst = zeroOne Zero One
+
+export covering
+dim : Grammar True PDim
+dim = [|V baseName|]
+  <|> [|K dimConst|]
+  <|> parens dim
+
+private
+0 PBinderHead : Nat -> Type
+PBinderHead n = (Vect n PQty, BName, PTerm)
+
+private
+toVect : List a -> (n ** Vect n a)
+toVect []        = (_ ** [])
+toVect (x :: xs) = (_ ** x :: snd (toVect xs))
+
+private
+0 MakeBinder : Nat -> Type
+MakeBinder n = (String, PBinderHead n -> PTerm -> PTerm)
+
+private
+makePi : MakeBinder 1
+makePi = ("→", \([pi], x, s) => Pi pi x s)
+
+private
+makeSig : MakeBinder 0
+makeSig = ("×", \([], x, s) => Sig x s)
+
+private
+makeBinder : {m, n : Nat} -> MakeBinder m -> PBinderHead n -> PTerm ->
+             Grammar False PTerm
+makeBinder (str, f) h t =
+  case decEq m n of
+    Yes Refl => pure $ f h t
+    No  _    =>
+      let q = if m == 1 then "quantity" else "quantities" in
+      fatalError "'\{str}' expects \{show m} \{q}, got \{show n}"
+
+private
+binderInfix : Grammar True (n ** MakeBinder n)
+binderInfix = res "→" $> (1 ** makePi)
+          <|> res "×" $> (0 ** makeSig)
+
+private
+lamIntro : Grammar True (BName -> PTerm -> PTerm)
+lamIntro = Lam  <$ resC "λ"
+       <|> DLam <$ resC "δ"
+
+private covering
+caseIntro : Grammar True PQty
+caseIntro = resC "case1" $> One
+        <|> resC "caseω" $> Any
+        <|> resC "case" *> qty <* resC "·"
+
+private
+optNameBinder : Grammar False BName
+optNameBinder = [|join $ optional $ bname <* darr|]
+
+mutual
+  export covering
+  term : Grammar True PTerm
+  term = lamTerm
+     <|> caseTerm
+     <|> bindTerm
+     <|> [|annotate infixEqTerm (optional $ resC "∷" *> term)|]
+  where
+    annotate : PTerm -> Maybe PTerm -> PTerm
+    annotate s a = maybe s (s :#) a
+
+  private covering
+  lamTerm : Grammar True PTerm
+  lamTerm = flip . foldr <$> lamIntro <*> some bname <* darr <*> term
+
+  private covering
+  caseTerm : Grammar True PTerm
+  caseTerm =
+    [|Case caseIntro term
+           (resC "return" *> optBinderTerm)
+           (resC "of"     *> braces caseBody)|]
+
+  private covering
+  caseBody : Grammar False PCaseBody
+  caseBody = [|CasePair (pairPat <* darr) (term <* optSemi)|]
+         <|> [|CaseEnum $ semiSep [|MkPair tag (darr *> term)|]|]
+  where
+    optSemi = ignore $ optional $ res ";"
+    pairPat = parens [|MkPair bname (resC "," *> bname)|]
+
+  private covering
+  bindTerm : Grammar True PTerm
+  bindTerm = do
+    bnd <- binderHead
+    inf <- binderInfix
+    body <- term
+    makeBinder (snd inf) (snd bnd) body
+
+  private covering
+  infixEqTerm : Grammar True PTerm
+  infixEqTerm = do
+    l <- appTerm
+    rty <- optional [|MkPair (resC "≡" *> term) (resC ":" *> appTerm)|]
+    pure $ maybe l (\rty => Eq (Nothing, snd rty) l (fst rty)) rty
+
+  private covering
+  appTerm : Grammar True PTerm
+  appTerm = resC "★"  *> [|TYPE nat|]
+        <|> resC "Eq" *> [|Eq (bracks optBinderTerm) aTerm aTerm|]
+        <|> [|apply aTerm (many appArg)|]
+  where
+    data PArg = TermArg PTerm | DimArg PDim
+
+    appArg : Grammar True PArg
+    appArg = [|DimArg $ resC "@" *> dim|]
+         <|> [|TermArg aTerm|]
+
+    apply : PTerm -> List PArg -> PTerm
+    apply = foldl apply1 where
+      apply1 : PTerm -> PArg -> PTerm
+      apply1 f (TermArg x) = f :@ x
+      apply1 f (DimArg  p) = f :% p
+
+  private covering
+  aTerm : Grammar True PTerm
+  aTerm = [|Enum $ braces $ commaSep bareTag|]
+      <|> [|TYPE universe|]
+      <|> [|V name|]
+      <|> [|Tag tag|]
+      <|> foldr1 Pair <$> parens (commaSep1 term)
+
+  private covering
+  binderHead : Grammar True (n ** PBinderHead n)
+  binderHead = parens {commit = False} $ do
+    qs <- [|toVect qtys|]
+    name <- bname
+    resC ":"
+    ty <- term
+    pure (qs.fst ** (qs.snd, name, ty))
+
+  private covering
+  optBinderTerm : Grammar True (BName, PTerm)
+  optBinderTerm = [|MkPair optNameBinder term|]
+
+
+export covering
+defIntro : Grammar True PQty
+defIntro = Zero <$ resC "def0"
+       <|> Any  <$ resC "defω"
+       <|> resC "def" *> option Any (qty <* resC "·")
+
+export covering
+definition : Grammar True PDefinition
+definition =
+  [|MkPDef defIntro name
+      (optional (resC ":" *> term))
+      (resC "≔" *> term)|]
+
+export
+load : Grammar True String
+load = resC "load" *> string
+
+mutual
+  export covering
+  namespace_ : Grammar True PNamespace
+  namespace_ =
+    [|MkPNamespace (resC "namespace" *> mods) (braces $ many decl)|]
+
+  export covering
+  decl : Grammar True PDecl
+  decl = [|PDef definition|]
+     <|> [|PNs  namespace_|]
+
+export covering
+topLevel : Grammar True PTopLevel
+topLevel = [|PLoad load|]
+       <|> [|PD    decl|]
+
+export covering
+input : Grammar False (List PTopLevel)
+input = skipSemis *> many (topLevel <* skipSemis)
+  where skipSemis = ignore $ many $ resC ";"
+
+
+public export
+data Error =
+    LexError   Lexer.Error
+  | ParseError (List1 (ParsingError Token))
+%hide Lexer.Error
+
+export
+lexParseWith : {c : Bool} -> Grammar c a -> String -> Either Error a
+lexParseWith grm input = do
+  toks <- mapFst LexError $ lex input
+  bimap ParseError fst $ parse (grm <* eof) toks
+
+export covering %inline
+lexParseInput : String -> Either Error (List PTopLevel)
+lexParseInput = lexParseWith input
+
+export covering %inline
+lexParseTerm : String -> Either Error PTerm
+lexParseTerm = lexParseWith term
diff --git a/lib/Quox/Parser/Syntax.idr b/lib/Quox/Parser/Syntax.idr
index c3cee48..aaf13dd 100644
--- a/lib/Quox/Parser/Syntax.idr
+++ b/lib/Quox/Parser/Syntax.idr
@@ -4,8 +4,6 @@ import public Quox.Syntax
 import public Quox.Syntax.Qty.Three
 import public Quox.Definition
 
-import public Control.Monad.Either
-
 import Derive.Prelude
 %hide TT.Name
 
@@ -15,7 +13,7 @@ import Derive.Prelude
 
 public export
 0 BName : Type
-BName = Maybe BaseName
+BName = Maybe String
 
 public export
 0 PUniverse : Type
@@ -27,7 +25,7 @@ PQty = Three
 
 namespace PDim
   public export
-  data PDim = K DimConst | V BaseName
+  data PDim = K DimConst | V PBaseName
   %name PDim p, q
   %runElab derive "PDim" [Eq, Ord, Show]
 
@@ -53,7 +51,7 @@ namespace PTerm
       | DLam BName PTerm
       | (:%) PTerm PDim
 
-      | V Name
+      | V PName
       | (:#) PTerm PTerm
     %name PTerm s, t
 
@@ -70,15 +68,35 @@ public export
 record PDefinition where
   constructor MkPDef
   qty  : PQty
-  name : Name
-  type : PTerm
+  name : PName
+  type : Maybe PTerm
   term : PTerm
 %name PDefinition def
 %runElab derive "PDefinition" [Eq, Ord, Show]
 
+mutual
+  public export
+  record PNamespace where
+    constructor MkPNamespace
+    name  : Mods
+    decls : List PDecl
+  %name PNamespace ns
+
+  public export
+  data PDecl =
+      PDef PDefinition
+    | PNs  PNamespace
+  %name PDecl decl
+%runElab deriveMutual ["PNamespace", "PDecl"] [Eq, Ord, Show]
+
+public export
+data PTopLevel = PD PDecl | PLoad String
+%name PTopLevel t
+%runElab derive "PTopLevel" [Eq, Ord, Show]
+
 
 export
-toPDimWith : Context' BaseName d -> Dim d -> PDim
+toPDimWith : Context' PBaseName d -> Dim d -> PDim
 toPDimWith ds (K e) = K e
 toPDimWith ds (B i) = V $ ds !!! i
 
@@ -90,27 +108,30 @@ toPDim = toPDimWith [<]
 mutual
   namespace Term
     export
-    toPTermWith : Context' BaseName d -> Context' BaseName n ->
+    toPTermWith : Context' PBaseName d -> Context' PBaseName n ->
                   Term Three d n -> PTerm
     toPTermWith ds ns t =
       let Element t _ = pushSubsts t in
       toPTermWith' ds ns t
 
     private
-    toPTermWith' : Context' BaseName d -> Context' BaseName n ->
+    toPTermWith' : Context' PBaseName d -> Context' PBaseName n ->
                    (t : Term Three d n) -> (0 _ : NotClo t) =>
                    PTerm
     toPTermWith' ds ns s = case s of
       TYPE l =>
         TYPE l
       Pi qty arg (S [x] res) =>
-        Pi qty (Just x) (toPTermWith ds ns arg)
-                        (toPTermWith ds (ns :< x) res.term)
+        Pi qty (Just $ show x)
+          (toPTermWith ds ns arg)
+          (toPTermWith ds (ns :< baseStr x) res.term)
       Lam (S [x] body) =>
-        Lam (Just x) $ toPTermWith ds (ns :< x) body.term
+        Lam (Just $ show x) $
+          toPTermWith ds (ns :< baseStr x) body.term
       Sig fst (S [x] snd) =>
-        Sig (Just x) (toPTermWith ds ns fst)
-                     (toPTermWith ds (ns :< x) snd.term)
+        Sig (Just $ show x)
+          (toPTermWith ds ns fst)
+          (toPTermWith ds (ns :< baseStr x) snd.term)
       Pair fst snd =>
         Pair (toPTermWith ds ns fst) (toPTermWith ds ns snd)
       Enum cases =>
@@ -118,40 +139,40 @@ mutual
       Tag tag =>
         Tag tag
       Eq (S [i] ty) l r =>
-        Eq (Just i, toPTermWith (ds :< i) ns ty.term)
+        Eq (Just $ show i, toPTermWith (ds :< baseStr i) ns ty.term)
            (toPTermWith ds ns l) (toPTermWith ds ns r)
       DLam (S [i] body) =>
-        DLam (Just i) $ toPTermWith (ds :< i) ns body.term
+        DLam (Just $ show i) $ toPTermWith (ds :< baseStr i) ns body.term
       E e =>
         toPTermWith ds ns e
 
   namespace Elim
     export
-    toPTermWith : Context' BaseName d -> Context' BaseName n ->
+    toPTermWith : Context' PBaseName d -> Context' PBaseName n ->
                   Elim Three d n -> PTerm
     toPTermWith ds ns e =
       let Element e _ = pushSubsts e in
       toPTermWith' ds ns e
 
     private
-    toPTermWith' : Context' BaseName d -> Context' BaseName n ->
+    toPTermWith' : Context' PBaseName d -> Context' PBaseName n ->
                    (e : Elim Three d n) -> (0 _ : NotClo e) =>
                    PTerm
     toPTermWith' ds ns e = case e of
       F x =>
-        V x
+        V $ toPName x
       B i =>
-        V $ unq $ ns !!! i
+        V $ MakePName [<] $ ns !!! i
       fun :@ arg =>
         toPTermWith ds ns fun :@ toPTermWith ds ns arg
       CasePair qty pair (S [r] ret) (S [x, y] body) =>
         Case qty (toPTermWith ds ns pair)
-             (Just r, toPTermWith ds (ns :< r) ret.term)
-             (CasePair (Just x, Just y) $
-                toPTermWith ds (ns :< x :< y) body.term)
+             (Just $ show r, toPTermWith ds (ns :< baseStr r) ret.term)
+             (CasePair (Just $ show x, Just $ show y) $
+                toPTermWith ds (ns :< baseStr x :< baseStr y) body.term)
       CaseEnum qty tag (S [r] ret) arms =>
         Case qty (toPTermWith ds ns tag)
-             (Just r, toPTermWith ds (ns :< r) ret.term)
+             (Just $ show r, toPTermWith ds (ns :< baseStr r) ret.term)
              (CaseEnum $ mapSnd (toPTermWith ds ns) <$> SortedMap.toList arms)
       fun :% arg =>
         toPTermWith ds ns fun :% toPDimWith ds arg
@@ -167,172 +188,3 @@ namespace Elim
   export
   toPTerm : Elim Three 0 0 -> PTerm
   toPTerm = toPTermWith [<] [<]
-
-
-
-public export
-data FromPTermError =
-    AnnotationNeeded PTerm
-  | DuplicatesInEnum (List TagVal)
-  | DimNotInScope Name
-  | QtyNotGlobal PQty
-  | DimNameInTerm Name
-
-public export
-FromPTerm : (Type -> Type) -> Type
-FromPTerm m = MonadError FromPTermError m
-
-private
-extendVect : Telescope' a from to -> Vect n a -> Telescope' a from (n + to)
-extendVect tel [] = tel
-extendVect tel (x :: xs) {n = S n} =
-  rewrite plusSuccRightSucc n to in
-  extendVect (tel :< x) xs
-
-
-parameters {auto _ : FromPTerm m} (b : Var n -> m a) (f : Name -> m a)
-           (xs : Context' BName n)
-  private
-  fromBaseName : BaseName -> m a
-  fromBaseName x = maybe (f $ unq x) b $ Context.find (== Just x) xs
-
-  fromName : Name -> m a
-  fromName x = if null x.mods then fromBaseName x.base else f x
-
-export
-fromPDimWith : FromPTerm m =>
-               Context' BName d -> PDim -> m (Dim d)
-fromPDimWith ds (K e) = pure $ K e
-fromPDimWith ds (V i) = fromBaseName (pure . B) (throwError . DimNotInScope) ds i
-
-private
-avoidDim : FromPTerm m => Context' BName d -> Name -> m (Term q d n)
-avoidDim ds x =
-  fromName (const $ throwError $ DimNameInTerm x) (pure . FT) ds x
-
-
-mutual
-  export
-  fromPTermWith : FromPTerm m =>
-                  Context' BName d -> Context' BName n ->
-                  PTerm -> m (Term Three d n)
-  fromPTermWith ds ns t0 = case t0 of
-    TYPE k =>
-      pure $ TYPE $ k
-
-    Pi pi x s t =>
-      Pi pi <$> fromPTermWith ds ns s
-            <*> fromPTermTScope ds ns [x] t
-
-    Lam x s =>
-      Lam <$> fromPTermTScope ds ns [x] s
-
-    s :@ t =>
-      map E $ (:@) <$> fromPTermElim ds ns s <*> fromPTermWith ds ns t
-
-    Sig x s t =>
-      Sig <$> fromPTermWith ds ns s <*> fromPTermTScope ds ns [x] t
-
-    Pair s t =>
-      Pair <$> fromPTermWith ds ns s <*> fromPTermWith ds ns t
-
-    Case pi pair (r, ret) (CasePair (x, y) body) =>
-      map E $ Base.CasePair pi
-        <$> fromPTermElim ds ns pair
-        <*> fromPTermTScope ds ns [r] ret
-        <*> fromPTermTScope ds ns [x, y] body
-
-    Case pi tag (r, ret) (CaseEnum arms) =>
-      map E $ Base.CaseEnum pi
-        <$> fromPTermElim ds ns tag
-        <*> fromPTermTScope ds ns [r] ret
-        <*> assert_total fromPTermEnumArms ds ns arms
-
-    Enum strs =>
-      let set = SortedSet.fromList strs in
-      if length strs == length (SortedSet.toList set) then
-        pure $ Enum set
-      else
-        throwError $ DuplicatesInEnum strs
-
-    Tag str => pure $ Tag str
-
-    Eq (i, ty) s t =>
-      Eq <$> fromPTermDScope ds ns [i] ty
-         <*> fromPTermWith ds ns s
-         <*> fromPTermWith ds ns t
-
-    DLam i s =>
-      DLam <$> fromPTermDScope ds ns [i] s
-
-    s :% p =>
-      map E $ (:%) <$> fromPTermElim ds ns s <*> fromPDimWith ds p
-
-    V x =>
-      fromName (pure . E . B) (avoidDim ds) ns x
-
-    s :# a =>
-      map E $ (:#) <$> fromPTermWith ds ns s <*> fromPTermWith ds ns a
-
-  private
-  fromPTermEnumArms : FromPTerm m =>
-                      Context' BName d -> Context' BName n ->
-                      List (TagVal, PTerm) -> m (CaseEnumArms Three d n)
-  fromPTermEnumArms ds ns =
-    map SortedMap.fromList . traverse (traverse $ fromPTermWith ds ns)
-
-  private
-  fromPTermElim : FromPTerm m =>
-                  Context' BName d -> Context' BName n ->
-                  PTerm -> m (Elim Three d n)
-  fromPTermElim ds ns e =
-    case !(fromPTermWith ds ns e) of
-      E e => pure e
-      _   => throwError $ AnnotationNeeded e
-
-  -- [todo] use SN if the var is named but still unused
-  private
-  fromPTermTScope : {s : Nat} -> FromPTerm m =>
-                    Context' BName d -> Context' BName n ->
-                    Vect s BName ->
-                    PTerm -> m (ScopeTermN s Three d n)
-  fromPTermTScope ds ns xs t =
-    if all isNothing xs then
-      SN <$> fromPTermWith ds ns t
-    else
-      SY (map (fromMaybe "_") xs) <$> fromPTermWith ds (extendVect ns xs) t
-
-  private
-  fromPTermDScope : {s : Nat} -> FromPTerm m =>
-                    Context' BName d -> Context' BName n ->
-                    Vect s BName ->
-                    PTerm -> m (DScopeTermN s Three d n)
-  fromPTermDScope ds ns xs t =
-    if all isNothing xs then
-      SN <$> fromPTermWith ds ns t
-    else
-      SY (map (fromMaybe "_") xs) <$> fromPTermWith (extendVect ds xs) ns t
-
-
-export %inline
-fromPTerm : FromPTerm m => PTerm -> m (Term Three 0 0)
-fromPTerm = fromPTermWith [<] [<]
-
-
-export
-globalPQty : FromPTerm m => (q : PQty) -> m (IsGlobal q)
-globalPQty pi = case isGlobal pi of
-  Yes y => pure y
-  No  n => throwError $ QtyNotGlobal pi
-
-
--- [todo] extend substitutions so they can do this injection. that's the sort of
--- thing they are for.
-export
-fromPDefinition : FromPTerm m => PDefinition -> m (Name, Definition Three)
-fromPDefinition (MkPDef {name, qty, type, term}) =
-  pure (name, MkDef' {
-    qty, qtyGlobal = !(globalPQty qty),
-    type = T $ inject !(fromPTerm type),
-    term = Just $ T $ inject !(fromPTerm term)
-  })
diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg
index 2134fa4..c5e851b 100644
--- a/lib/quox-lib.ipkg
+++ b/lib/quox-lib.ipkg
@@ -33,6 +33,8 @@ modules =
   Quox.Name,
   Quox.Typing,
   Quox.Typechecker,
-  Quox.Lexer,
+  Quox.Parser.Lexer,
   Quox.Parser.Syntax,
+  Quox.Parser.Parser,
+  Quox.Parser.FromParser,
   Quox.Parser
diff --git a/tests/Tests/FromPTerm.idr b/tests/Tests/FromPTerm.idr
index 01d62b0..3991f7c 100644
--- a/tests/Tests/FromPTerm.idr
+++ b/tests/Tests/FromPTerm.idr
@@ -3,30 +3,29 @@ module Tests.FromPTerm
 import Quox.Parser.Syntax
 import Quox.Parser
 import TermImpls
+import Tests.Parser as TParser
 import TAP
 
 import Derive.Prelude
 %language ElabReflection
 
+%hide TParser.Failure
+%hide TParser.ExpectedFail
+
 public export
 data Failure =
-    LexError Lexer.Error
-  | ParseError (List1 (ParsingError Token))
-  | FromPTermError FromPTermError
+    ParseError (Parser.Error)
+  | FromParserError FromParserError
   | WrongResult String
   | ExpectedFail String
 
-%runElab derive "Syntax.FromPTermError" [Show]
+%runElab derive "FromParser.FromParserError" [Show]
 
 export
 ToInfo Failure where
-  toInfo (LexError err) =
-    [("type", "LexError"), ("info", show err)]
-  toInfo (ParseError errs) =
-    ("type", "ParseError") ::
-    map (bimap show show) ([1 .. length errs] `zip` toList errs)
-  toInfo (FromPTermError err) =
-    [("type", "FromPTermError"),
+  toInfo (ParseError err) = toInfo err
+  toInfo (FromParserError err) =
+    [("type", "FromParserError"),
      ("got", show err)]
   toInfo (WrongResult got) =
     [("type", "WrongResult"), ("got", got)]
@@ -35,14 +34,13 @@ ToInfo Failure where
 
 
 parameters {c : Bool} {auto _ : Show b}
-           (grm : Grammar c a) (fromP : a -> Either FromPTermError b)
+           (grm : Grammar c a) (fromP : a -> Either FromParserError b)
            (inp : String)
   parameters {default (ltrim inp) label : String}
     parsesWith : (b -> Bool) -> Test
     parsesWith p = test label $ do
-      toks      <- mapFst LexError $ lex inp
-      (pres, _) <- mapFst ParseError $ parse (grm <* eof) toks
-      res       <- mapFst FromPTermError $ fromP pres
+      pres <- mapFst ParseError $ lexParseWith grm inp
+      res  <- mapFst FromParserError $ fromP pres
       unless (p res) $ Left $ WrongResult $ show res
 
     parses : Test
@@ -54,8 +52,7 @@ parameters {c : Bool} {auto _ : Show b}
   parameters {default "\{ltrim inp}  # fails" label : String}
     parseFails : Test
     parseFails = test label $ do
-      toks      <- mapFst LexError $ lex inp
-      (pres, _) <- mapFst ParseError $ parse (grm <* eof) toks
+      pres <- mapFst ParseError $ lexParseWith grm inp
       either (const $ Right ()) (Left . ExpectedFail . show) $ fromP pres
 
 
diff --git a/tests/Tests/Parser.idr b/tests/Tests/Parser.idr
index f1c71d3..0aac535 100644
--- a/tests/Tests/Parser.idr
+++ b/tests/Tests/Parser.idr
@@ -7,18 +7,22 @@ import TAP
 
 public export
 data Failure =
-    LexError Lexer.Error
-  | ParseError (List1 (ParsingError Token))
+    ParseError Parser.Error
   | WrongResult String
   | ExpectedFail String
 
 export
-ToInfo Failure where
+ToInfo Parser.Error where
   toInfo (LexError err) =
     [("type", "LexError"), ("info", show err)]
   toInfo (ParseError errs) =
     ("type", "ParseError") ::
     map (bimap show show) ([1 .. length errs] `zip` toList errs)
+
+export
+ToInfo Failure where
+  toInfo (ParseError err) =
+    toInfo err
   toInfo (WrongResult got) =
     [("type", "WrongResult"), ("got", got)]
   toInfo (ExpectedFail got) =
@@ -30,8 +34,7 @@ parameters {c : Bool} {auto _ : Show a} (grm : Grammar c a)
   parameters {default (ltrim inp) label : String}
     parsesWith : (a -> Bool) -> Test
     parsesWith p = test label $ do
-      toks     <- mapFst LexError $ lex inp
-      (res, _) <- mapFst ParseError $ parse (grm <* eof) toks
+      res <- mapFst ParseError $ lexParseWith grm inp
       unless (p res) $ Left $ WrongResult $ show res
 
     parses : Test
@@ -43,9 +46,8 @@ parameters {c : Bool} {auto _ : Show a} (grm : Grammar c a)
   parameters {default "\{ltrim inp}  # fails" label : String}
     parseFails : Test
     parseFails = test label $ do
-      toks <- mapFst LexError $ lex inp
-      either (const $ Right ()) (Left . ExpectedFail . show . fst) $
-        parse (grm <* eof) toks
+      either (const $ Right ()) (Left . ExpectedFail . show) $
+        lexParseWith grm inp
 
 
 export
@@ -59,9 +61,9 @@ tests = "parser" :- [
 
   "names" :- [
     parsesAs name "x"
-      (MakeName [<] $ UN "x"),
+      (MakePName [<] "x"),
     parsesAs name "Data.String.length"
-      (MakeName [< "Data", "String"] $ UN "length"),
+      (MakePName [< "Data", "String"] "length"),
     parseFails name "_"
   ],
 
@@ -119,7 +121,7 @@ tests = "parser" :- [
 
   "applications" :- [
     parsesAs term "f" (V "f"),
-    parsesAs term "f.x.y" (V $ MakeName [< "f", "x"] $ UN "y"),
+    parsesAs term "f.x.y" (V $ MakePName [< "f", "x"] "y"),
     parsesAs term "f x" (V "f" :@ V "x"),
     parsesAs term "f x y" (V "f" :@ V "x" :@ V "y"),
     parsesAs term "(f x) y" (V "f" :@ V "x" :@ V "y"),
@@ -240,22 +242,36 @@ tests = "parser" :- [
   ],
 
   "definitions" :- [
-    parsesAs definition "defω x : (_: {a}) × {b} ≔ ('a, 'b);" $
-      MkPDef Any "x" (Sig Nothing (Enum ["a"]) (Enum ["b"]))
+    parsesAs definition "defω x : (_: {a}) × {b} ≔ ('a, 'b)" $
+      MkPDef Any "x" (Just $ Sig Nothing (Enum ["a"]) (Enum ["b"]))
         (Pair (Tag "a") (Tag "b")),
-    parsesAs definition "def# x : (_: {a}) ** {b} ≔ ('a, 'b);" $
-      MkPDef Any "x" (Sig Nothing (Enum ["a"]) (Enum ["b"]))
+    parsesAs definition "defω x : (_: {a}) × {b} ≔ ('a, 'b)" $
+      MkPDef Any "x" (Just $ Sig Nothing (Enum ["a"]) (Enum ["b"]))
         (Pair (Tag "a") (Tag "b")),
-    parsesAs definition "def ω·x : (_: {a}) × {b} ≔ ('a, 'b);" $
-      MkPDef Any "x" (Sig Nothing (Enum ["a"]) (Enum ["b"]))
+    parsesAs definition "def# x : (_: {a}) ** {b} ≔ ('a, 'b)" $
+      MkPDef Any "x" (Just $ Sig Nothing (Enum ["a"]) (Enum ["b"]))
         (Pair (Tag "a") (Tag "b")),
-    parsesAs definition "def x : (_: {a}) × {b} ≔ ('a, 'b);" $
-      MkPDef Any "x" (Sig Nothing (Enum ["a"]) (Enum ["b"]))
+    parsesAs definition "def ω·x : (_: {a}) × {b} ≔ ('a, 'b)" $
+      MkPDef Any "x" (Just $ Sig Nothing (Enum ["a"]) (Enum ["b"]))
         (Pair (Tag "a") (Tag "b")),
-    parsesAs definition "def0 A : ★₀ ≔ {a, b, c};" $
-      MkPDef Zero "A" (TYPE 0) (Enum ["a", "b", "c"]),
+    parsesAs definition "def x : (_: {a}) × {b} ≔ ('a, 'b)" $
+      MkPDef Any "x" (Just $ Sig Nothing (Enum ["a"]) (Enum ["b"]))
+        (Pair (Tag "a") (Tag "b")),
+    parsesAs definition "def0 A : ★₀ ≔ {a, b, c}" $
+      MkPDef Zero "A" (Just $ TYPE 0) (Enum ["a", "b", "c"])
+  ],
+
+  "top level" :- [
     parsesAs input "def0 A : ★₀ ≔ {}; def0 B : ★₁ ≔ A;" $
-      [MkPDef Zero "A" (TYPE 0) (Enum []),
-       MkPDef Zero "B" (TYPE 1) (V "A")]
+      [PD $ PDef $ MkPDef Zero "A" (Just $ TYPE 0) (Enum []),
+       PD $ PDef $ MkPDef Zero "B" (Just $ TYPE 1) (V "A")],
+    parsesAs input "def0 A : ★₀ ≔ {} def0 B : ★₁ ≔ A" $
+      [PD $ PDef $ MkPDef Zero "A" (Just $ TYPE 0) (Enum []),
+       PD $ PDef $ MkPDef Zero "B" (Just $ TYPE 1) (V "A")],
+    parsesAs input "def0 A : ★₀ ≔ {};;; def0 B : ★₁ ≔ A" $
+      [PD $ PDef $ MkPDef Zero "A" (Just $ TYPE 0) (Enum []),
+       PD $ PDef $ MkPDef Zero "B" (Just $ TYPE 1) (V "A")],
+    parsesAs input "" [] {label = "[empty input]"},
+    parsesAs input ";;;;;;;;;;;;;;;;;;;;;;;;;;" []
   ]
 ]