From 5ea7880e387eb9f22f3ca8ab4944dd195e6d952d Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 24 Apr 2022 00:21:30 +0200
Subject: [PATCH] typechecker stuff

---
 src/Quox.idr                    |   2 +-
 src/Quox/Context.idr            |  17 +-
 src/Quox/Equal.idr              | 182 +++++----
 src/Quox/Error.idr              |   5 +
 src/Quox/NatExtra.idr           |   6 +-
 src/Quox/OPE.idr                |   2 +-
 src/Quox/Reduce.idr             | 121 ++++++
 src/Quox/Syntax/DimEq.idr       |  16 +-
 src/Quox/Syntax/Shift.idr       |  17 +
 src/Quox/Syntax/Term.idr        | 669 +-------------------------------
 src/Quox/Syntax/Term/Base.idr   | 106 +++++
 src/Quox/Syntax/Term/Pretty.idr |  85 ++++
 src/Quox/Syntax/Term/Reduce.idr | 163 ++++++++
 src/Quox/Syntax/Term/Split.idr  |  82 ++++
 src/Quox/Syntax/Term/Subst.idr  | 133 +++++++
 src/Quox/Typechecker.idr        | 142 +++++++
 src/Quox/Typing.idr             |  23 +-
 17 files changed, 1021 insertions(+), 750 deletions(-)
 create mode 100644 src/Quox/Reduce.idr
 create mode 100644 src/Quox/Syntax/Term/Base.idr
 create mode 100644 src/Quox/Syntax/Term/Pretty.idr
 create mode 100644 src/Quox/Syntax/Term/Reduce.idr
 create mode 100644 src/Quox/Syntax/Term/Split.idr
 create mode 100644 src/Quox/Syntax/Term/Subst.idr
 create mode 100644 src/Quox/Typechecker.idr

diff --git a/src/Quox.idr b/src/Quox.idr
index 56cfbc3..8d1354e 100644
--- a/src/Quox.idr
+++ b/src/Quox.idr
@@ -5,7 +5,7 @@ import public Quox.Syntax
 import public Quox.Equal
 import public Quox.Error
 import public Quox.Pretty
--- import public Quox.Typechecker
+import public Quox.Typechecker
 
 import Data.Nat
 import Data.Vect
diff --git a/src/Quox/Context.idr b/src/Quox/Context.idr
index 639fc36..7bd96eb 100644
--- a/src/Quox/Context.idr
+++ b/src/Quox/Context.idr
@@ -2,7 +2,7 @@ module Quox.Context
 
 import Quox.Syntax.Shift
 import Quox.Pretty
-import Quox.NatExtra
+import public Quox.NatExtra
 
 import Data.DPair
 import Data.Nat
@@ -36,6 +36,10 @@ Context' : (a : Type) -> (len : Nat) -> Type
 Context' a = Context (\_ => a)
 
 
+public export
+tail : Context tm (S n) -> Context tm n
+tail (tel :< _) = tel
+
 export
 toSnocList : Telescope tm _ _ -> SnocList (Exists tm)
 toSnocList [<]        = [<]
@@ -158,6 +162,17 @@ teleLte' [<]        = LTERefl
 teleLte' (tel :< _) = LTESuccR (teleLte' tel)
 
 
+export
+tabulate : ((n : Nat) -> tm n) ->
+           (from, to : Nat) -> from `LTE'` to => Telescope tm from to
+tabulate f from from   @{LTERefl}    = [<]
+tabulate f from (S to) @{LTESuccR _} = tabulate f from to :< f to
+
+export
+tabulate0 : ((n : Nat) -> tm n) -> (n : Nat) -> Context tm n
+tabulate0 f n = tabulate f 0 n
+
+
 export
 pure : from `LTE'` to => a -> Telescope' a from to
 pure @{LTERefl}    x = [<]
diff --git a/src/Quox/Equal.idr b/src/Quox/Equal.idr
index 7888262..943993a 100644
--- a/src/Quox/Equal.idr
+++ b/src/Quox/Equal.idr
@@ -1,121 +1,161 @@
 module Quox.Equal
 
 import public Quox.Syntax
+import public Quox.Reduce
 import Quox.Error
 
 %default total
 
 
+public export
+data Mode = Equal | Sub
+
 public export
 data Error
-= Clash  SomeTerm SomeTerm
-| ClashU Universe Universe
-| ClashQ Qty      Qty
+= ClashT Mode (Term d n) (Term d n)
+| ClashU Mode Universe Universe
+| ClashQ      Qty      Qty
 
 private %inline
-clashT' : Term d n -> Term d n -> Error
-clashT' = Clash `on` some2
-
-private %inline
-clashE' : Elim d n -> Elim d n -> Error
-clashE' = clashT' `on` E
+ClashE : Mode -> Elim d n -> Elim d n -> Error
+ClashE mode = ClashT mode `on` E
 
 parameters {auto _ : MonadThrow Error m}
   private %inline
-  clashT : Term d n -> Term d n -> m a
-  clashT = throw .: clashT'
+  clashT : Mode -> Term d n -> Term d n -> m a
+  clashT mode = throw .: ClashT mode
 
   private %inline
-  clashE : Elim d n -> Elim d n -> m a
-  clashE = clashT `on` E
-
-  private %inline
-  eq : Eq a => (a -> a -> Error) -> a -> a -> m ()
-  eq err a b = unless (a == b) $ throw $ err a b
+  clashE : Mode -> Elim d n -> Elim d n -> m a
+  clashE mode = throw .: ClashE mode
 
   mutual
     private covering
-    equalTN' : (s, t : Term 0 n) ->
-               (0 _ : NotRedexT s) -> (0 _ : NotRedexT t) -> m ()
+    compareTN' : Mode ->
+                 (s, t : Term 0 n) ->
+                 (0 _ : NotRedexT s) -> (0 _ : NotRedexT t) -> m ()
 
-    equalTN' (TYPE k) (TYPE l) _ _ =
-      eq ClashU k l
-    equalTN' s@(TYPE _) t _ _ = clashT s t
+    compareTN' mode (TYPE k) (TYPE l) _ _ =
+      case mode of
+           Equal => unless (k == l) $ throw $ ClashU Equal k l
+           Sub   => unless (k <= l) $ throw $ ClashU Sub   k l
+    compareTN' mode s@(TYPE _) t _ _ = clashT mode s t
 
-    equalTN' (Pi qtm1 qty1 _ arg1 res1) (Pi qtm2 qty2 _ arg2 res2) _ _ = do
-      eq ClashQ qtm1 qtm2
-      eq ClashQ qty1 qty2
-      equalT0 arg1 arg2
-      equalTS0 res1 res2
-    equalTN' s@(Pi {}) t _ _ = clashT s t
+    compareTN' mode (Pi qtm1 qty1 _ arg1 res1)
+                    (Pi qtm2 qty2 _ arg2 res2) _ _ = do
+      -- [todo] these should probably always be ==, right..?
+      unless (qtm1 == qtm2) $ throw $ ClashQ qtm1 qtm2
+      unless (qty1 == qty2) $ throw $ ClashQ qty1 qty2
+      compareT0  mode arg2 arg1 -- reversed for contravariant Sub
+      compareTS0 mode res1 res2
+    compareTN' mode s@(Pi {}) t _ _ = clashT mode s t
 
     -- [todo] eta
-    equalTN' (Lam _ body1) (Lam _ body2) _ _ =
-      equalTS0 body1 body2
-    equalTN' s@(Lam {}) t _ _ = clashT s t
+    compareTN' _ (Lam _ body1) (Lam _ body2) _ _ =
+      compareTS0 Equal body1 body2
+    compareTN' mode s@(Lam {}) t _ _ = clashT mode s t
 
-    equalTN' (E e) (E f) ps pt = equalE0 e f
-    equalTN' s@(E _) t _ _ = clashT s t
+    compareTN' mode (E e) (E f) ps pt = compareE0 mode e f
+    compareTN' mode s@(E _) t _ _ = clashT mode s t
 
-    equalTN' (CloT  {}) _ ps _ = void $ ps IsCloT
-    equalTN' (DCloT {}) _ ps _ = void $ ps IsDCloT
+    compareTN' _ (CloT  {}) _ ps _ = void $ ps IsCloT
+    compareTN' _ (DCloT {}) _ ps _ = void $ ps IsDCloT
 
     private covering
-    equalEN' : (e, f : Elim 0 n) ->
-               (0 _ : NotRedexE e) -> (0 _ : NotRedexE f) -> m ()
+    compareEN' : Mode ->
+                 (e, f : Elim 0 n) ->
+                 (0 _ : NotRedexE e) -> (0 _ : NotRedexE f) -> m ()
 
-    equalEN' (F x) (F y) _ _ = do
-      eq (clashE' `on` F {d = 0, n = 0}) x y
-    equalEN' e@(F _) f _ _ = clashE e f
+    compareEN' mode e@(F x) f@(F y) _ _ =
+      unless (x == y) $ clashE mode e f
+    compareEN' mode e@(F _) f _ _ = clashE mode e f
 
-    equalEN' (B i) (B j) _ _ = do
-      eq (clashE' `on` B {d = 0}) i j
-    equalEN' e@(B _) f _ _ = clashE e f
+    compareEN' mode e@(B i) f@(B j) _ _ =
+      unless (i == j) $ clashE mode e f
+    compareEN' mode e@(B _) f _ _ = clashE mode e f
 
-    equalEN' (fun1 :@ arg1) (fun2 :@ arg2) _ _ = do
-      equalE0 fun1 fun2
-      equalT0 arg1 arg2
-    equalEN' e@(_ :@ _) f _ _ = clashE e f
+    -- [todo] tracking variance of functions? maybe???
+    -- probably not
+    compareEN' _ (fun1 :@ arg1) (fun2 :@ arg2) _ _ = do
+      compareE0 Equal fun1 fun2
+      compareT0 Equal arg1 arg2
+    compareEN' mode e@(_ :@ _) f _ _ = clashE mode e f
 
-    equalEN' (tm1 :# ty1) (tm2 :# ty2) _ _ = do
-      equalT0 tm1 tm2
-      equalT0 ty1 ty2
-    equalEN' e@(_ :# _) f _ _ = clashE e f
+    -- [todo] is always checking the types are equal correct?
+    compareEN' mode (tm1 :# ty1) (tm2 :# ty2) _ _ = do
+      compareT0 mode tm1 tm2
+      compareT0 Equal ty1 ty2
+    compareEN' mode e@(_ :# _) f _ _ = clashE mode e f
 
-    equalEN' (CloE  {}) _ pe _ = void $ pe IsCloE
-    equalEN' (DCloE {}) _ pe _ = void $ pe IsDCloE
+    compareEN' _ (CloE  {}) _ pe _ = void $ pe IsCloE
+    compareEN' _ (DCloE {}) _ pe _ = void $ pe IsDCloE
 
 
     private covering %inline
-    equalTN : NonRedexTerm 0 n -> NonRedexTerm 0 n -> m ()
-    equalTN s t = equalTN' s.fst t.fst s.snd t.snd
+    compareTN : Mode -> NonRedexTerm 0 n -> NonRedexTerm 0 n -> m ()
+    compareTN mode s t = compareTN' mode s.fst t.fst s.snd t.snd
 
     private covering %inline
-    equalEN : NonRedexElim 0 n -> NonRedexElim 0 n -> m ()
-    equalEN e f = equalEN' e.fst f.fst e.snd f.snd
+    compareEN : Mode -> NonRedexElim 0 n -> NonRedexElim 0 n -> m ()
+    compareEN mode e f = compareEN' mode e.fst f.fst e.snd f.snd
 
 
     export covering %inline
-    equalT : DimEq d -> Term d n -> Term d n -> m ()
-    equalT eqs s t =
-      for_ (splits eqs) $ \th => (s /// th) `equalT0` (t /// th)
+    compareT : Mode -> DimEq d -> Term d n -> Term d n -> m ()
+    compareT mode eqs s t =
+      for_ (splits eqs) $ \th => compareT0 mode (s /// th) (t /// th)
 
     export covering %inline
-    equalE : DimEq d -> Elim d n -> Elim d n -> m ()
-    equalE eqs e f =
-      for_ (splits eqs) $ \th => (e /// th) `equalE0` (f /// th)
+    compareE : Mode -> DimEq d -> Elim d n -> Elim d n -> m ()
+    compareE mode eqs e f =
+      for_ (splits eqs) $ \th => compareE0 mode (e /// th) (f /// th)
 
 
     export covering %inline
-    equalT0 : Term 0 n -> Term 0 n -> m ()
-    equalT0 s t = whnfT s `equalTN` whnfT t
+    compareT0 : Mode -> Term 0 n -> Term 0 n -> m ()
+    compareT0 mode s t = compareTN mode (whnfT s) (whnfT t)
 
     export covering %inline
-    equalE0 : Elim 0 n -> Elim 0 n -> m ()
-    equalE0 e f = whnfE e `equalEN` whnfE f
+    compareE0 : Mode -> Elim 0 n -> Elim 0 n -> m ()
+    compareE0 mode e f = compareEN mode (whnfE e) (whnfE f)
 
     export covering %inline
-    equalTS0 : ScopeTerm 0 n -> ScopeTerm 0 n -> m ()
-    equalTS0 (TUnused body1) (TUnused body2) = equalT0 body1 body2
-    equalTS0 body1 body2 =
-      fromScopeTerm body1 `equalT0` fromScopeTerm body2
+    compareTS0 : Mode -> ScopeTerm 0 n -> ScopeTerm 0 n -> m ()
+    compareTS0 mode (TUnused body1) (TUnused body2) =
+      compareT0 mode body1 body2
+    compareTS0 mode body1 body2 =
+      compareT0 mode (fromScopeTerm body1) (fromScopeTerm body2)
+
+
+    export covering %inline
+    equalTWith : DimEq d -> Term d n -> Term d n -> m ()
+    equalTWith = compareT Equal
+
+    export covering %inline
+    equalEWith : DimEq d -> Elim d n -> Elim d n -> m ()
+    equalEWith = compareE Equal
+
+    export covering %inline
+    subTWith : DimEq d -> Term d n -> Term d n -> m ()
+    subTWith = compareT Sub
+
+    export covering %inline
+    subEWith : DimEq d -> Elim d n -> Elim d n -> m ()
+    subEWith = compareE Sub
+
+
+    export covering %inline
+    equalT : {d : Nat} -> Term d n -> Term d n -> m ()
+    equalT = equalTWith DimEq.new
+
+    export covering %inline
+    equalE : {d : Nat} -> Elim d n -> Elim d n -> m ()
+    equalE = equalEWith DimEq.new
+
+    export covering %inline
+    subT : {d : Nat} -> Term d n -> Term d n -> m ()
+    subT = subTWith DimEq.new
+
+    export covering %inline
+    subE : {d : Nat} -> Elim d n -> Elim d n -> m ()
+    subE = subEWith DimEq.new
diff --git a/src/Quox/Error.idr b/src/Quox/Error.idr
index 1c17878..b83ee7c 100644
--- a/src/Quox/Error.idr
+++ b/src/Quox/Error.idr
@@ -183,6 +183,11 @@ interface MonadThrow err m1 => MonadCatch err m1 m2 | err, m1 where
 public export
 interface (Monad m1, Monad m2) => MonadEmbed m1 m2 where embed : m1 a -> m2 a
 
+public export
+MonadThrows : (errs : List Type) -> (m : Type -> Type) -> Type
+MonadThrows []          m = Monad m
+MonadThrows (ty :: tys) m = (MonadThrow ty m, MonadThrows tys m)
+
 
 export %inline
 implementation
diff --git a/src/Quox/NatExtra.idr b/src/Quox/NatExtra.idr
index 28e2cba..f17179f 100644
--- a/src/Quox/NatExtra.idr
+++ b/src/Quox/NatExtra.idr
@@ -20,9 +20,9 @@ lteSucc' LTERefl      = LTERefl
 lteSucc' (LTESuccR p) = LTESuccR $ lteSucc' p
 
 public export
-fromLTE : {n : Nat} -> LTE m n -> LTE' m n
-fromLTE LTEZero     = lteZero'
-fromLTE (LTESucc p) = lteSucc' $ fromLTE p
+fromLte : {n : Nat} -> LTE m n -> LTE' m n
+fromLte LTEZero     = lteZero'
+fromLte (LTESucc p) = lteSucc' $ fromLte p
 
 public export
 toLte : {n : Nat} -> m `LTE'` n -> m `LTE` n
diff --git a/src/Quox/OPE.idr b/src/Quox/OPE.idr
index 9b6de26..b3a381d 100644
--- a/src/Quox/OPE.idr
+++ b/src/Quox/OPE.idr
@@ -44,7 +44,7 @@ dropInner' (LTESuccR p) = Drop $ dropInner' $ force p
 
 public export
 dropInner : {n : Nat} -> LTE m n -> OPE m n
-dropInner = dropInner' . fromLTE
+dropInner = dropInner' . fromLte
 
 public export
 dropInnerN : (m : Nat) -> OPE n (m + n)
diff --git a/src/Quox/Reduce.idr b/src/Quox/Reduce.idr
new file mode 100644
index 0000000..19fbd2b
--- /dev/null
+++ b/src/Quox/Reduce.idr
@@ -0,0 +1,121 @@
+module Quox.Reduce
+
+import public Quox.Syntax
+
+
+public export
+data IsRedexT : Term d n -> Type where
+  IsUpsilon : IsRedexT $ E (_ :# _)
+  IsCloT    : IsRedexT $ CloT {}
+  IsDCloT   : IsRedexT $ DCloT {}
+
+public export %inline
+NotRedexT : Term d n -> Type
+NotRedexT = Not . IsRedexT
+
+public export
+data IsRedexE : Elim d n -> Type where
+  IsBetaLam : IsRedexE $ (Lam {} :# Pi {}) :@ _
+  IsCloE    : IsRedexE $ CloE {}
+  IsDCloE   : IsRedexE $ DCloE {}
+
+public export %inline
+NotRedexE : Elim d n -> Type
+NotRedexE = Not . IsRedexE
+
+
+export %inline
+isRedexT : (t : Term d n) -> Dec (IsRedexT t)
+isRedexT (E (_ :# _))   = Yes IsUpsilon
+isRedexT (CloT {})      = Yes IsCloT
+isRedexT (DCloT {})     = Yes IsDCloT
+isRedexT (TYPE _)       = No $ \x => case x of {}
+isRedexT (Pi {})        = No $ \x => case x of {}
+isRedexT (Lam {})       = No $ \x => case x of {}
+isRedexT (E (F _))      = No $ \x => case x of {}
+isRedexT (E (B _))      = No $ \x => case x of {}
+isRedexT (E (_ :@ _))   = No $ \x => case x of {}
+isRedexT (E (CloE {}))  = No $ \x => case x of {}
+isRedexT (E (DCloE {})) = No $ \x => case x of {}
+
+export %inline
+isRedexE : (e : Elim d n) -> Dec (IsRedexE e)
+isRedexE ((Lam {} :# Pi {}) :@ _)      = Yes IsBetaLam
+isRedexE (CloE {})                     = Yes IsCloE
+isRedexE (DCloE {})                    = Yes IsDCloE
+isRedexE (F x)                         = No $ \x => case x of {}
+isRedexE (B i)                         = No $ \x => case x of {}
+isRedexE (F _                    :@ _) = No $ \x => case x of {}
+isRedexE (B _                    :@ _) = No $ \x => case x of {}
+isRedexE (_ :@ _                 :@ _) = No $ \x => case x of {}
+isRedexE ((TYPE _   :# _)        :@ _) = No $ \x => case x of {}
+isRedexE ((Pi {}    :# _)        :@ _) = No $ \x => case x of {}
+isRedexE ((Lam {}   :# TYPE _)   :@ _) = No $ \x => case x of {}
+isRedexE ((Lam {}   :# Lam {})   :@ _) = No $ \x => case x of {}
+isRedexE ((Lam {}   :# E _)      :@ _) = No $ \x => case x of {}
+isRedexE ((Lam {}   :# CloT {})  :@ _) = No $ \x => case x of {}
+isRedexE ((Lam {}   :# DCloT {}) :@ _) = No $ \x => case x of {}
+isRedexE ((E _      :# _)        :@ _) = No $ \x => case x of {}
+isRedexE ((CloT {}  :# _)        :@ _) = No $ \x => case x of {}
+isRedexE ((DCloT {} :# _)        :@ _) = No $ \x => case x of {}
+isRedexE (CloE {}                :@ _) = No $ \x => case x of {}
+isRedexE (DCloE {}               :@ _) = No $ \x => case x of {}
+isRedexE (_ :# _)                      = No $ \x => case x of {}
+
+
+public export %inline
+RedexTerm : Nat -> Nat -> Type
+RedexTerm d n = Subset (Term d n) IsRedexT
+
+public export %inline
+NonRedexTerm : Nat -> Nat -> Type
+NonRedexTerm d n = Subset (Term d n) NotRedexT
+
+
+public export %inline
+RedexElim : Nat -> Nat -> Type
+RedexElim d n = Subset (Elim d n) IsRedexE
+
+public export %inline
+NonRedexElim : Nat -> Nat -> Type
+NonRedexElim d n = Subset (Elim d n) NotRedexE
+
+
+||| substitute a term with annotation for the bound variable of a `ScopeTerm`
+export %inline
+substScope : (arg, argTy : Term d n) -> (body : ScopeTerm d n) -> Term d n
+substScope arg argTy (TUsed   body) = body // one (arg :# argTy)
+substScope arg argTy (TUnused body) = body
+
+export %inline
+stepT' : (s : Term d n) -> IsRedexT s -> Term d n
+stepT' (E (s :# _)) IsUpsilon = s
+stepT' (CloT  s th) IsCloT    = pushSubstsTWith' id th s
+stepT' (DCloT s th) IsDCloT   = pushSubstsTWith' th id s
+
+export %inline
+stepT : (s : Term d n) -> Either (NotRedexT s) (Term d n)
+stepT s = case isRedexT s of Yes y => Right $ stepT' s y; No n => Left n
+
+export %inline
+stepE' : (e : Elim d n) -> IsRedexE e -> Elim d n
+stepE' ((Lam {body, _} :# Pi {arg, res, _}) :@ s) IsBetaLam =
+  substScope s arg body :# substScope s arg res
+stepE' (CloE  e th) IsCloE  = pushSubstsEWith' id th e
+stepE' (DCloE e th) IsDCloE = pushSubstsEWith' th id e
+
+export %inline
+stepE : (e : Elim d n) -> Either (NotRedexE e) (Elim d n)
+stepE e = case isRedexE e of Yes y => Right $ stepE' e y; No n => Left n
+
+export covering
+whnfT : Term d n -> NonRedexTerm d n
+whnfT s = case stepT s of
+               Right s'   => whnfT s'
+               Left  done => Element s done
+
+export covering
+whnfE : Elim d n -> NonRedexElim d n
+whnfE e = case stepE e of
+               Right e'   => whnfE e'
+               Left  done => Element e done
diff --git a/src/Quox/Syntax/DimEq.idr b/src/Quox/Syntax/DimEq.idr
index 7d0680e..3ac70ac 100644
--- a/src/Quox/Syntax/DimEq.idr
+++ b/src/Quox/Syntax/DimEq.idr
@@ -33,13 +33,13 @@ zeroEq : DimEq 0
 zeroEq = C [<]
 
 export
-new' : (d : Nat) -> DimEq' d
-new' 0     = [<]
-new' (S d) = new' d :< Nothing
+new' : {d : Nat} -> DimEq' d
+new' {d = 0}   = [<]
+new' {d = S d} = new' :< Nothing
 
 export %inline
-new : (d : Nat) -> DimEq d
-new d = C (new' d)
+new : {d : Nat} -> DimEq d
+new = C new'
 
 
 private %inline
@@ -147,16 +147,16 @@ splits (C eqs)   = splits' eqs
 
 private
 0 newGetShift : (d : Nat) -> (i : Var d) -> (by : Shift d d') ->
-                getShift' by (new' d) i = Nothing
+                getShift' by (new' {d}) i = Nothing
 newGetShift (S d) VZ     by = Refl
 newGetShift (S d) (VS i) by = newGetShift d i (drop1 by)
 
 export
-0 newGet' : (d : Nat) -> (i : Var d) -> get' (new' d) i = Nothing
+0 newGet' : (d : Nat) -> (i : Var d) -> get' (new' {d}) i = Nothing
 newGet' d i = newGetShift d i SZ
 
 export
-0 newGet : (d : Nat) -> (p : Dim d) -> get (new' d) p = p
+0 newGet : (d : Nat) -> (p : Dim d) -> get (new' {d}) p = p
 newGet d (K e) = Refl
 newGet d (B i) = rewrite newGet' d i in Refl
 
diff --git a/src/Quox/Syntax/Shift.idr b/src/Quox/Syntax/Shift.idr
index d11e69e..18dfb99 100644
--- a/src/Quox/Syntax/Shift.idr
+++ b/src/Quox/Syntax/Shift.idr
@@ -71,6 +71,10 @@ fromNat Z      = SZ
 fromNat (S by) = SS $ fromNat by
 %transform "Shift.fromNat" Shift.fromNat x = believe_me x
 
+public export
+fromNat0 : (by : Nat) -> Shift 0 by
+fromNat0 by = rewrite sym $ plusZeroRightNeutral by in fromNat by
+
 export
 0 fromToNat : (by : Shift from to) -> by `Eqv` fromNat by.nat {from}
 fromToNat SZ      = EqSZ
@@ -96,6 +100,19 @@ export %inline
 Injective Shift.(.nat) where injective eq = irrelevantEq $ toNatInj eq
 
 
+public export
+ssDown : Shift (S from) to -> Shift from to
+ssDown SZ      = SS SZ
+ssDown (SS by) = SS (ssDown by)
+
+export
+0 ssDownEqv : (by : Shift (S from) to) -> ssDown by `Eqv` SS by
+ssDownEqv SZ      = EqSS EqSZ
+ssDownEqv (SS by) = EqSS $ ssDownEqv by
+
+%transform "Shift.ssDown" ssDown by = believe_me (SS by)
+
+
 public export
 shift : Shift from to -> Var from -> Var to
 shift SZ      i = i
diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr
index 6427fda..f9acfe6 100644
--- a/src/Quox/Syntax/Term.idr
+++ b/src/Quox/Syntax/Term.idr
@@ -1,666 +1,7 @@
 module Quox.Syntax.Term
 
-import public Quox.Syntax.Var
-import public Quox.Syntax.Shift
-import public Quox.Syntax.Subst
-import public Quox.Syntax.Universe
-import public Quox.Syntax.Qty
-import public Quox.Syntax.Dim
-import public Quox.Name
-import public Quox.OPE
-
-import Quox.Pretty
-
-import public Data.DPair
-import Data.List
-import Data.Maybe
-import Data.Nat
-import public Data.So
-import Data.String
-import Data.Vect
-
-%default total
-
-
-infixl 8 :#
-infixl 9 :@
-mutual
-  public export
-  TSubst : Nat -> Nat -> Nat -> Type
-  TSubst d = Subst (\n => Elim d n)
-
-  ||| first argument `d` is dimension scope size, second `n` is term scope size
-  public export
-  data Term : (d, n : Nat) -> Type where
-    ||| type of types
-    TYPE : (l : Universe) -> Term d n
-
-    ||| function type
-    Pi  : (qtm, qty : Qty) -> (x : Name) ->
-          (arg : Term d n) -> (res : ScopeTerm d n) -> Term d n
-    ||| function term
-    Lam : (x : Name) -> (body : ScopeTerm d n) -> Term d n
-
-    ||| elimination
-    E : (e : Elim d n) -> Term d n
-
-    ||| term closure/suspended substitution
-    CloT  : (tm : Term d from)  -> (th : Lazy (TSubst d from to)) -> Term d to
-    ||| dimension closure/suspended substitution
-    DCloT : (tm : Term dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Term dto n
-
-  ||| first argument `d` is dimension scope size, second `n` is term scope size
-  public export
-  data Elim : (d, n : Nat) -> Type where
-    ||| free variable
-    F : (x : Name) -> Elim d n
-    ||| bound variable
-    B : (i : Var n) -> Elim d n
-
-    ||| term application
-    (:@) : (fun : Elim d n) -> (arg : Term d n) -> Elim d n
-
-    ||| type-annotated term
-    (:#) : (tm, ty : Term d n) -> Elim d n
-
-    ||| term closure/suspended substitution
-    CloE  : (el : Elim d from)  -> (th : Lazy (TSubst d from to)) -> Elim d to
-    ||| dimension closure/suspended substitution
-    DCloE : (el : Elim dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Elim dto n
-
-  ||| a scope with one more bound variable
-  public export
-  data ScopeTerm : (d, n : Nat) -> Type where
-    ||| variable is used
-    TUsed : (body : Term d (S n)) -> ScopeTerm d n
-    ||| variable is unused
-    TUnused : (body : Term d n) -> ScopeTerm d n
-
-  ||| a scope with one more bound dimension variable
-  public export
-  data DScopeTerm : (d, n : Nat) -> Type where
-    ||| variable is used
-    DUsed : (body : Term (S d) n) -> DScopeTerm d n
-    ||| variable is unused
-    DUnused : (body : Term d n) -> DScopeTerm d n
-
-%name Term s, t, r
-%name Elim e, f
-%name ScopeTerm body
-%name DScopeTerm body
-
-export
-fromDScopeTerm : DScopeTerm d n -> Term (S d) n
-fromDScopeTerm (DUsed   body) = body
-fromDScopeTerm (DUnused body) = body `DCloT` shift 1
-
-export
-fromScopeTerm : ScopeTerm d n -> Term d (S n)
-fromScopeTerm (TUsed   body) = body
-fromScopeTerm (TUnused body) = body `CloT` shift 1
-
-
-||| same as `F` but as a term
-public export %inline
-FT : Name -> Term d n
-FT = E . F
-
-||| abbreviation for a bound variable like `BV 4` instead of
-||| `B (VS (VS (VS (VS VZ))))`
-public export %inline
-BV : (i : Nat) -> (0 _ : LT i n) => Elim d n
-BV i = B $ V i
-
-||| same as `BV` but as a term
-public export %inline
-BVT : (i : Nat) -> (0 _ : LT i n) => Term d n
-BVT i = E $ BV i
-
-
-public export %inline
-isLam : Term d n -> Bool
-isLam (Lam {}) = True
-isLam _        = False
-
-public export
-NotLam : Term d n -> Type
-NotLam = So . not . isLam
-
-
-public export %inline
-isApp : Elim d n -> Bool
-isApp ((:@) {}) = True
-isApp _         = False
-
-public export
-NotApp : Elim d n -> Type
-NotApp = So . not . isApp
-
-
-infixl 9 :@@
-||| apply multiple arguments at once
-public export %inline
-(:@@) : Elim d n -> List (Term d n) -> Elim d n
-f :@@ ss = foldl (:@) f ss
-
-public export
-record GetArgs (d, n : Nat) where
-  constructor GotArgs
-  fun      : Elim d n
-  args     : List (Term d n)
-  0 notApp : NotApp fun
-
-private
-getArgs' : Elim d n -> List (Term d n) -> GetArgs d n
-getArgs' fun args with (choose $ isApp fun)
-  getArgs' (f :@ a) args | Left yes = getArgs' f (a :: args)
-  _ | Right no = GotArgs {fun, args, notApp = no}
-
-||| splits an application into its head and arguments. if it's not an
-||| application then the list is just empty
-export %inline
-getArgs : Elim d n -> GetArgs d n
-getArgs e = getArgs' e []
-
-
-infixr 1 :\\
-public export
-(:\\) : Vect m Name -> Term d (m + n) -> Term d n
-[]      :\\ t = t
-x :: xs :\\ t = let t' = replace {p = Term _} (plusSuccRightSucc {}) t in
-                Lam x $ TUsed $ xs :\\ t'
-
-public export
-record GetLams (d, n : Nat) where
-  constructor GotLams
-  names    : Vect lams Name
-  body     : Term d rest
-  0 eq     : lams + n = rest
-  0 notLam : NotLam body
-
-public export
-getLams : Term d n -> GetLams d n
-getLams s with (choose $ isLam s)
-  getLams s@(Lam x body) | Left yes =
-    let inner = getLams $ assert_smaller s $ fromScopeTerm body in
-    GotLams {names  = x :: inner.names,
-             body   = inner.body,
-             eq     = plusSuccRightSucc {} `trans` inner.eq,
-             notLam = inner.notLam}
-  _ | Right no = GotLams {names = [], body = s, eq = Refl, notLam = no}
-
-
-parameters {auto _ : Pretty.HasEnv m}
-  private %inline arrowD : m (Doc HL)
-  arrowD = hlF Syntax $ ifUnicode "→" "->"
-
-  private %inline lamD : m (Doc HL)
-  lamD = hlF Syntax $ ifUnicode "λ" "fun"
-
-  private %inline annD : m (Doc HL)
-  annD = hlF Syntax $ ifUnicode "⦂" "::"
-
-private %inline typeD : Doc HL
-typeD = hl Syntax "Type"
-
-private %inline colonD : Doc HL
-colonD = hl Syntax ":"
-
-mutual
-  export covering
-  PrettyHL (Term d n) where
-    prettyM (TYPE l) =
-      parensIfM App $ typeD <//> !(withPrec Arg $ prettyM l)
-    prettyM (Pi qtm qty x s t) =
-      parensIfM Outer $ hang 2 $
-        !(prettyBinder [qtm, qty] x s) <++> !arrowD
-          <//> !(under T x $ prettyM t)
-    prettyM (Lam x t) =
-      parensIfM Outer $
-        sep [!lamD, hl TVar !(prettyM x), !arrowD]
-          <//> !(under T x $ prettyM t)
-    prettyM (E e) =
-      prettyM e
-    prettyM (CloT s th) =
-      parensIfM SApp . hang 2 =<<
-        [|withPrec SApp (prettyM s) </> prettyTSubst th|]
-    prettyM (DCloT s th) =
-      parensIfM SApp . hang 2 =<<
-        [|withPrec SApp (prettyM s) </> prettyDSubst th|]
-
-  export covering
-  PrettyHL (Elim d n) where
-    prettyM (F x) =
-      hl' Free <$> prettyM x
-    prettyM (B i) =
-      prettyVar TVar TVarErr (!ask).tnames i
-    prettyM (e :@ s) =
-      let GotArgs f args _ = getArgs' e [s] in
-      parensIfM App =<< withPrec Arg
-        [|prettyM f <//> (align . sep <$> traverse prettyM args)|]
-    prettyM (s :# a) =
-      parensIfM Ann $ hang 2 $
-        !(withPrec AnnL $ prettyM s) <++> !annD
-          <//> !(withPrec Ann $ prettyM a)
-    prettyM (CloE e th)  =
-      parensIfM SApp . hang 2 =<<
-        [|withPrec SApp (prettyM e) </> prettyTSubst th|]
-    prettyM (DCloE e th) =
-      parensIfM SApp . hang 2 =<<
-        [|withPrec SApp (prettyM e) </> prettyDSubst th|]
-
-  export covering
-  PrettyHL (ScopeTerm d n) where
-    prettyM body = prettyM $ fromScopeTerm body
-
-  export covering
-  prettyTSubst : Pretty.HasEnv m => TSubst d from to -> m (Doc HL)
-  prettyTSubst s = prettySubstM prettyM (!ask).tnames TVar "[" "]" s
-
-  export covering
-  prettyBinder : Pretty.HasEnv m => List Qty -> Name -> Term d n -> m (Doc HL)
-  prettyBinder pis x a =
-    pure $ parens $ hang 2 $
-      hsep [hl TVar !(prettyM x),
-            sep [!(prettyQtyBinds pis),
-                 hsep [colonD, !(withPrec Outer $ prettyM a)]]]
-
-
-export FromVar (Elim d) where fromVar = B
-export FromVar (Term d) where fromVar = E . fromVar
-
-||| does the minimal reasonable work:
-||| - deletes the closure around a free name since it doesn't do anything
-||| - deletes an identity substitution
-||| - composes (lazily) with an existing top-level closure
-||| - immediately looks up a bound variable
-||| - otherwise, wraps in a new closure
-export
-CanSubst (Elim d) (Elim d) where
-  F x       // _  = F x
-  B i       // th = th !! i
-  CloE e ph // th = assert_total CloE e $ ph . th
-  e         // th = case force th of
-                         Shift SZ => e
-                         th       => CloE e th
-
-||| does the minimal reasonable work:
-||| - deletes the closure around an atomic constant like `TYPE`
-||| - deletes an identity substitution
-||| - composes (lazily) with an existing top-level closure
-||| - goes inside `E` in case it is a simple variable or something
-||| - otherwise, wraps in a new closure
-export
-CanSubst (Elim d) (Term d) where
-  TYPE l    // _  = TYPE l
-  E e       // th = E $ e // th
-  CloT s ph // th = CloT s $ ph . th
-  s         // th = case force th of
-                         Shift SZ => s
-                         th       => CloT s th
-
-export
-CanSubst (Elim d) (ScopeTerm d) where
-  TUsed   body // th = TUsed   $ body // push th
-  TUnused body // th = TUnused $ body // th
-
-export CanSubst Var (Term      d) where s // th = s // map (B {d}) th
-export CanSubst Var (Elim      d) where e // th = e // map (B {d}) th
-export CanSubst Var (ScopeTerm d) where s // th = s // map (B {d}) th
-
-export CanShift (Term      d) where s // by = s // Shift by {env = Elim d}
-export CanShift (Elim      d) where e // by = e // Shift by {env = Elim d}
-export CanShift (ScopeTerm d) where s // by = s // Shift by {env = Elim d}
-
-
-infixl 8 ///
-mutual
-  namespace Term
-    ||| applies a dimension substitution with the same behaviour as `(//)`
-    ||| above
-    export
-    (///) : Term dfrom n -> DSubst dfrom dto -> Term dto n
-    TYPE l     /// _        = TYPE l
-    E e        /// th       = E $ e /// th
-    DCloT s ph /// th       = DCloT s $ ph . th
-    s          /// Shift SZ = s
-    s          /// th       = DCloT s th
-
-    ||| applies a term and dimension substitution
-    public export %inline
-    subs : Term dfrom from -> DSubst dfrom dto -> TSubst dto from to ->
-           Term dto to
-    subs s th ph = s /// th // ph
-
-  namespace Elim
-    ||| applies a dimension substitution with the same behaviour as `(//)`
-    ||| above
-    export
-    (///) : Elim dfrom n -> DSubst dfrom dto -> Elim dto n
-    F x        /// _        = F x
-    B i        /// _        = B i
-    DCloE e ph /// th       = DCloE e $ ph . th
-    e          /// Shift SZ = e
-    e          /// th       = DCloE e th
-
-    ||| applies a term and dimension substitution
-    public export %inline
-    subs : Elim dfrom from -> DSubst dfrom dto -> TSubst dto from to ->
-           Elim dto to
-    subs e th ph = e /// th // ph
-
-  namespace ScopeTerm
-    ||| applies a dimension substitution with the same behaviour as `(//)`
-    ||| above
-    export
-    (///) : ScopeTerm dfrom n -> DSubst dfrom dto -> ScopeTerm dto n
-    TUsed   body /// th = TUsed   $ body /// th
-    TUnused body /// th = TUnused $ body /// th
-
-    ||| applies a term and dimension substitution
-    public export %inline
-    subs : ScopeTerm dfrom from -> DSubst dfrom dto -> TSubst dto from to ->
-           ScopeTerm dto to
-    subs body th ph = body /// th // ph
-
-
-private %inline
-comp' : DSubst dfrom dto -> TSubst dfrom from mid -> TSubst dto mid to ->
-        TSubst dto from to
-comp' th ps ph = map (/// th) ps . ph
-
-
-mutual
-  ||| true if a term has a closure or dimension closure at the top level,
-  ||| or is `E` applied to such an elimination
-  public export %inline
-  topCloT : Term d n -> Bool
-  topCloT (CloT  _ _) = True
-  topCloT (DCloT _ _) = True
-  topCloT (E e)       = topCloE e
-  topCloT _           = False
-
-  ||| true if an elimination has a closure or dimension closure at the top level
-  public export %inline
-  topCloE : Elim d n -> Bool
-  topCloE (CloE  _ _) = True
-  topCloE (DCloE _ _) = True
-  topCloE _           = False
-
-
-public export IsNotCloT : Term d n -> Type
-IsNotCloT = So . not . topCloT
-
-||| a term which is not a top level closure
-public export NotCloTerm : Nat -> Nat -> Type
-NotCloTerm d n = Subset (Term d n) IsNotCloT
-
-public export IsNotCloE : Elim d n -> Type
-IsNotCloE = So . not . topCloE
-
-||| an elimination which is not a top level closure
-public export NotCloElim : Nat -> Nat -> Type
-NotCloElim d n = Subset (Elim d n) IsNotCloE
-
-public export %inline
-ncloT : (t : Term d n) -> (0 _ : IsNotCloT t) => NotCloTerm d n
-ncloT t @{p} = Element t p
-
-public export %inline
-ncloE : (t : Elim d n) -> (0 _ : IsNotCloE t) => NotCloElim d n
-ncloE e @{p} = Element e p
-
-
-
-mutual
-  ||| if the input term has any top-level closures, push them under one layer of
-  ||| syntax
-  export %inline
-  pushSubstsT : Term d n -> NotCloTerm d n
-  pushSubstsT s = pushSubstsTWith id id s
-
-  ||| if the input elimination has any top-level closures, push them under one
-  ||| layer of syntax
-  export %inline
-  pushSubstsE : Elim d n -> NotCloElim d n
-  pushSubstsE e = pushSubstsEWith id id e
-
-  export
-  pushSubstsTWith : DSubst dfrom dto -> TSubst dto from to ->
-                    Term dfrom from -> NotCloTerm dto to
-  pushSubstsTWith th ph (TYPE l) =
-    ncloT $ TYPE l
-  pushSubstsTWith th ph (Pi qtm qty x a body) =
-    ncloT $ Pi qtm qty x (subs a th ph) (subs body th ph)
-  pushSubstsTWith th ph (Lam x body) =
-    ncloT $ Lam x $ subs body th ph
-  pushSubstsTWith th ph (E e) =
-    let Element e _ = pushSubstsEWith th ph e in ncloT $ E e
-  pushSubstsTWith th ph (CloT  s ps) =
-    pushSubstsTWith th (comp' th ps ph) s
-  pushSubstsTWith th ph (DCloT s ps) =
-    pushSubstsTWith (ps . th) ph s
-
-  export
-  pushSubstsEWith : DSubst dfrom dto -> TSubst dto from to ->
-                    Elim dfrom from -> NotCloElim dto to
-  pushSubstsEWith th ph (F x) =
-    ncloE $ F x
-  pushSubstsEWith th ph (B i) =
-    assert_total pushSubstsE $ ph !! i
-  pushSubstsEWith th ph (f :@ s) =
-    ncloE $ subs f th ph :@ subs s th ph
-  pushSubstsEWith th ph (s :# a) =
-    ncloE $ subs s th ph :# subs a th ph
-  pushSubstsEWith th ph (CloE  e ps) =
-    pushSubstsEWith th (comp' th ps ph) e
-  pushSubstsEWith th ph (DCloE e ps) =
-    pushSubstsEWith (ps . th) ph e
-
-
-parameters (th : DSubst dfrom dto) (ph : TSubst dto from to)
-  public export %inline
-  pushSubstsTWith' : Term dfrom from -> Term dto to
-  pushSubstsTWith' s = (pushSubstsTWith th ph s).fst
-
-  public export %inline
-  pushSubstsEWith' : Elim dfrom from -> Elim dto to
-  pushSubstsEWith' e = (pushSubstsEWith th ph e).fst
-
-
-public export %inline
-pushSubstsT' : Term d n -> Term d n
-pushSubstsT' s = (pushSubstsT s).fst
-
-public export %inline
-pushSubstsE' : Elim d n -> Elim d n
-pushSubstsE' e = (pushSubstsE e).fst
-
-
-mutual
-  -- tightening a term/elim also causes substitutions to be pushed through.
-  -- this is because otherwise a variable in an unused part of the subst
-  -- would cause it to incorrectly fail
-
-  export covering
-  Tighten (Term d) where
-    tighten p (TYPE l) =
-      pure $ TYPE l
-    tighten p (Pi qtm qty x arg res) =
-      Pi qtm qty x <$> tighten p arg
-                   <*> tighten p res
-    tighten p (Lam x body) =
-      Lam x <$> tighten p body
-    tighten p (E e) =
-      E <$> tighten p e
-    tighten p (CloT tm th) =
-      tighten p $ pushSubstsTWith' id th tm
-    tighten p (DCloT tm th) =
-      tighten p $ pushSubstsTWith' th id tm
-
-  export covering
-  Tighten (Elim d) where
-    tighten p (F x) =
-      pure $ F x
-    tighten p (B i) =
-      B <$> tighten p i
-    tighten p (fun :@ arg) =
-      [|tighten p fun :@ tighten p arg|]
-    tighten p (tm :# ty) =
-      [|tighten p tm :# tighten p ty|]
-    tighten p (CloE el th) =
-      tighten p $ pushSubstsEWith' id th el
-    tighten p (DCloE el th) =
-      tighten p $ pushSubstsEWith' th id el
-
-  export covering
-  Tighten (ScopeTerm d) where
-    tighten p (TUsed   body) = TUsed   <$> tighten (Keep p) body
-    tighten p (TUnused body) = TUnused <$> tighten p body
-
-
-public export
-data IsRedexT : Term d n -> Type where
-  IsUpsilon : IsRedexT $ E (_ :# _)
-  IsCloT    : IsRedexT $ CloT {}
-  IsDCloT   : IsRedexT $ DCloT {}
-
-public export %inline
-NotRedexT : Term d n -> Type
-NotRedexT = Not . IsRedexT
-
-public export
-data IsRedexE : Elim d n -> Type where
-  IsBetaLam : IsRedexE $ (Lam {} :# Pi {}) :@ _
-  IsCloE    : IsRedexE $ CloE {}
-  IsDCloE   : IsRedexE $ DCloE {}
-
-public export %inline
-NotRedexE : Elim d n -> Type
-NotRedexE = Not . IsRedexE
-
-
-export %inline
-isRedexT : (t : Term d n) -> Dec (IsRedexT t)
-isRedexT (E (_ :# _))   = Yes IsUpsilon
-isRedexT (CloT {})      = Yes IsCloT
-isRedexT (DCloT {})     = Yes IsDCloT
-isRedexT (TYPE _)       = No $ \x => case x of {}
-isRedexT (Pi {})        = No $ \x => case x of {}
-isRedexT (Lam {})       = No $ \x => case x of {}
-isRedexT (E (F _))      = No $ \x => case x of {}
-isRedexT (E (B _))      = No $ \x => case x of {}
-isRedexT (E (_ :@ _))   = No $ \x => case x of {}
-isRedexT (E (CloE {}))  = No $ \x => case x of {}
-isRedexT (E (DCloE {})) = No $ \x => case x of {}
-
-export %inline
-isRedexE : (e : Elim d n) -> Dec (IsRedexE e)
-isRedexE ((Lam {} :# Pi {}) :@ _)      = Yes IsBetaLam
-isRedexE (CloE {})                     = Yes IsCloE
-isRedexE (DCloE {})                    = Yes IsDCloE
-isRedexE (F x)                         = No $ \x => case x of {}
-isRedexE (B i)                         = No $ \x => case x of {}
-isRedexE (F _                    :@ _) = No $ \x => case x of {}
-isRedexE (B _                    :@ _) = No $ \x => case x of {}
-isRedexE (_ :@ _                 :@ _) = No $ \x => case x of {}
-isRedexE ((TYPE _   :# _)        :@ _) = No $ \x => case x of {}
-isRedexE ((Pi {}    :# _)        :@ _) = No $ \x => case x of {}
-isRedexE ((Lam {}   :# TYPE _)   :@ _) = No $ \x => case x of {}
-isRedexE ((Lam {}   :# Lam {})   :@ _) = No $ \x => case x of {}
-isRedexE ((Lam {}   :# E _)      :@ _) = No $ \x => case x of {}
-isRedexE ((Lam {}   :# CloT {})  :@ _) = No $ \x => case x of {}
-isRedexE ((Lam {}   :# DCloT {}) :@ _) = No $ \x => case x of {}
-isRedexE ((E _      :# _)        :@ _) = No $ \x => case x of {}
-isRedexE ((CloT {}  :# _)        :@ _) = No $ \x => case x of {}
-isRedexE ((DCloT {} :# _)        :@ _) = No $ \x => case x of {}
-isRedexE (CloE {}                :@ _) = No $ \x => case x of {}
-isRedexE (DCloE {}               :@ _) = No $ \x => case x of {}
-isRedexE (_ :# _)                      = No $ \x => case x of {}
-
-
-public export %inline
-RedexTerm : Nat -> Nat -> Type
-RedexTerm d n = Subset (Term d n) IsRedexT
-
-public export %inline
-NonRedexTerm : Nat -> Nat -> Type
-NonRedexTerm d n = Subset (Term d n) NotRedexT
-
-
-public export %inline
-RedexElim : Nat -> Nat -> Type
-RedexElim d n = Subset (Elim d n) IsRedexE
-
-public export %inline
-NonRedexElim : Nat -> Nat -> Type
-NonRedexElim d n = Subset (Elim d n) NotRedexE
-
-
-||| substitute a term with annotation for the bound variable of a `ScopeTerm`
-public export %inline
-substScope : (arg, argTy : Term d n) -> (body : ScopeTerm d n) -> Term d n
-substScope arg argTy (TUsed   body) = body // one (arg :# argTy)
-substScope arg argTy (TUnused body) = body
-
-public export %inline
-stepT' : (s : Term d n) -> IsRedexT s -> Term d n
-stepT' (E (s :# _)) IsUpsilon = s
-stepT' (CloT  s th) IsCloT    = pushSubstsTWith' id th s
-stepT' (DCloT s th) IsDCloT   = pushSubstsTWith' th id s
-
-public export %inline
-stepT : (s : Term d n) -> Either (NotRedexT s) (Term d n)
-stepT s = case isRedexT s of Yes y => Right $ stepT' s y; No n => Left n
-
-public export %inline
-stepE' : (e : Elim d n) -> IsRedexE e -> Elim d n
-stepE' ((Lam {body, _} :# Pi {arg, res, _}) :@ s) IsBetaLam =
-  substScope s arg body :# substScope s arg res
-stepE' (CloE  e th) IsCloE  = pushSubstsEWith' id th e
-stepE' (DCloE e th) IsDCloE = pushSubstsEWith' th id e
-
-public export %inline
-stepE : (e : Elim d n) -> Either (NotRedexE e) (Elim d n)
-stepE e = case isRedexE e of Yes y => Right $ stepE' e y; No n => Left n
-
-public export
-whnfT : Term d n -> NonRedexTerm d n
-whnfT s = case stepT s of
-               Right s'   => whnfT $ assert_smaller s s'
-               Left  done => Element s done
-
-public export
-whnfE : Elim d n -> NonRedexElim d n
-whnfE e = case stepE e of
-               Right e'   => whnfE $ assert_smaller e e'
-               Left  done => Element e done
-
-
-public export
-Exists2 : (ty1 -> ty2 -> Type) -> Type
-Exists2 t = Exists $ Exists . t
-
-public export %inline
-some : {0 f : a -> Type} -> f x -> Exists f
-some p = Evidence _ p
-
-public export %inline
-some2 : {0 f : a -> b -> Type} -> f x y -> Exists2 f
-some2 p = some $ some p
-
-
-||| A term of some unknown scope sizes.
-public export
-SomeTerm : Type
-SomeTerm = Exists2 Term
-
-||| An elimination of some unknown scope sizes.
-public export
-SomeElim : Type
-SomeElim = Exists2 Elim
-
-||| A dimension of some unknown scope size.
-public export
-SomeDim : Type
-SomeDim = Exists Dim
+import public Quox.Syntax.Term.Base
+import public Quox.Syntax.Term.Split
+import public Quox.Syntax.Term.Subst
+import public Quox.Syntax.Term.Reduce
+import public Quox.Syntax.Term.Pretty
diff --git a/src/Quox/Syntax/Term/Base.idr b/src/Quox/Syntax/Term/Base.idr
new file mode 100644
index 0000000..22552f6
--- /dev/null
+++ b/src/Quox/Syntax/Term/Base.idr
@@ -0,0 +1,106 @@
+module Quox.Syntax.Term.Base
+
+import public Quox.Syntax.Var
+import public Quox.Syntax.Shift
+import public Quox.Syntax.Subst
+import public Quox.Syntax.Universe
+import public Quox.Syntax.Qty
+import public Quox.Syntax.Dim
+import public Quox.Name
+import public Quox.OPE
+
+import Quox.Pretty
+
+import public Data.DPair
+import Data.List
+import Data.Maybe
+import Data.Nat
+import public Data.So
+import Data.String
+import Data.Vect
+
+%default total
+
+
+infixl 8 :#
+infixl 9 :@
+mutual
+  public export
+  TSubst : Nat -> Nat -> Nat -> Type
+  TSubst d = Subst (\n => Elim d n)
+
+  ||| first argument `d` is dimension scope size, second `n` is term scope size
+  public export
+  data Term : (d, n : Nat) -> Type where
+    ||| type of types
+    TYPE : (l : Universe) -> Term d n
+
+    ||| function type
+    Pi  : (qtm, qty : Qty) -> (x : Name) ->
+          (arg : Term d n) -> (res : ScopeTerm d n) -> Term d n
+    ||| function term
+    Lam : (x : Name) -> (body : ScopeTerm d n) -> Term d n
+
+    ||| elimination
+    E : (e : Elim d n) -> Term d n
+
+    ||| term closure/suspended substitution
+    CloT  : (tm : Term d from)  -> (th : Lazy (TSubst d from to)) -> Term d to
+    ||| dimension closure/suspended substitution
+    DCloT : (tm : Term dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Term dto n
+
+  ||| first argument `d` is dimension scope size, second `n` is term scope size
+  public export
+  data Elim : (d, n : Nat) -> Type where
+    ||| free variable
+    F : (x : Name) -> Elim d n
+    ||| bound variable
+    B : (i : Var n) -> Elim d n
+
+    ||| term application
+    (:@) : (fun : Elim d n) -> (arg : Term d n) -> Elim d n
+
+    ||| type-annotated term
+    (:#) : (tm, ty : Term d n) -> Elim d n
+
+    ||| term closure/suspended substitution
+    CloE  : (el : Elim d from)  -> (th : Lazy (TSubst d from to)) -> Elim d to
+    ||| dimension closure/suspended substitution
+    DCloE : (el : Elim dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Elim dto n
+
+  ||| a scope with one more bound variable
+  public export
+  data ScopeTerm : (d, n : Nat) -> Type where
+    ||| variable is used
+    TUsed : (body : Term d (S n)) -> ScopeTerm d n
+    ||| variable is unused
+    TUnused : (body : Term d n) -> ScopeTerm d n
+
+  ||| a scope with one more bound dimension variable
+  public export
+  data DScopeTerm : (d, n : Nat) -> Type where
+    ||| variable is used
+    DUsed : (body : Term (S d) n) -> DScopeTerm d n
+    ||| variable is unused
+    DUnused : (body : Term d n) -> DScopeTerm d n
+
+%name Term s, t, r
+%name Elim e, f
+%name ScopeTerm body
+%name DScopeTerm body
+
+||| same as `F` but as a term
+public export %inline
+FT : Name -> Term d n
+FT = E . F
+
+||| abbreviation for a bound variable like `BV 4` instead of
+||| `B (VS (VS (VS (VS VZ))))`
+public export %inline
+BV : (i : Nat) -> (0 _ : LT i n) => Elim d n
+BV i = B $ V i
+
+||| same as `BV` but as a term
+public export %inline
+BVT : (i : Nat) -> (0 _ : LT i n) => Term d n
+BVT i = E $ BV i
diff --git a/src/Quox/Syntax/Term/Pretty.idr b/src/Quox/Syntax/Term/Pretty.idr
new file mode 100644
index 0000000..ae78f7e
--- /dev/null
+++ b/src/Quox/Syntax/Term/Pretty.idr
@@ -0,0 +1,85 @@
+module Quox.Syntax.Term.Pretty
+
+import Quox.Syntax.Term.Base
+import Quox.Syntax.Term.Split
+import Quox.Syntax.Term.Subst
+import Quox.Pretty
+
+import Data.Vect
+
+
+
+parameters {auto _ : Pretty.HasEnv m}
+  private %inline arrowD : m (Doc HL)
+  arrowD = hlF Syntax $ ifUnicode "→" "->"
+
+  private %inline lamD : m (Doc HL)
+  lamD = hlF Syntax $ ifUnicode "λ" "fun"
+
+  private %inline annD : m (Doc HL)
+  annD = hlF Syntax $ ifUnicode "⦂" "::"
+
+private %inline typeD : Doc HL
+typeD = hl Syntax "Type"
+
+private %inline colonD : Doc HL
+colonD = hl Syntax ":"
+
+mutual
+  export covering
+  PrettyHL (Term d n) where
+    prettyM (TYPE l) =
+      parensIfM App $ typeD <//> !(withPrec Arg $ prettyM l)
+    prettyM (Pi qtm qty x s t) =
+      parensIfM Outer $ hang 2 $
+        !(prettyBinder [qtm, qty] x s) <++> !arrowD
+          <//> !(under T x $ prettyM t)
+    prettyM (Lam x t) =
+      parensIfM Outer $
+        sep [!lamD, hl TVar !(prettyM x), !arrowD]
+          <//> !(under T x $ prettyM t)
+    prettyM (E e) =
+      prettyM e
+    prettyM (CloT s th) =
+      parensIfM SApp . hang 2 =<<
+        [|withPrec SApp (prettyM s) </> prettyTSubst th|]
+    prettyM (DCloT s th) =
+      parensIfM SApp . hang 2 =<<
+        [|withPrec SApp (prettyM s) </> prettyDSubst th|]
+
+  export covering
+  PrettyHL (Elim d n) where
+    prettyM (F x) =
+      hl' Free <$> prettyM x
+    prettyM (B i) =
+      prettyVar TVar TVarErr (!ask).tnames i
+    prettyM (e :@ s) =
+      let GotArgs f args _ = getArgs' e [s] in
+      parensIfM App =<< withPrec Arg
+        [|prettyM f <//> (align . sep <$> traverse prettyM args)|]
+    prettyM (s :# a) =
+      parensIfM Ann $ hang 2 $
+        !(withPrec AnnL $ prettyM s) <++> !annD
+          <//> !(withPrec Ann $ prettyM a)
+    prettyM (CloE e th)  =
+      parensIfM SApp . hang 2 =<<
+        [|withPrec SApp (prettyM e) </> prettyTSubst th|]
+    prettyM (DCloE e th) =
+      parensIfM SApp . hang 2 =<<
+        [|withPrec SApp (prettyM e) </> prettyDSubst th|]
+
+  export covering
+  PrettyHL (ScopeTerm d n) where
+    prettyM body = prettyM $ fromScopeTerm body
+
+  export covering
+  prettyTSubst : Pretty.HasEnv m => TSubst d from to -> m (Doc HL)
+  prettyTSubst s = prettySubstM prettyM (!ask).tnames TVar "[" "]" s
+
+  export covering
+  prettyBinder : Pretty.HasEnv m => List Qty -> Name -> Term d n -> m (Doc HL)
+  prettyBinder pis x a =
+    pure $ parens $ hang 2 $
+      hsep [hl TVar !(prettyM x),
+            sep [!(prettyQtyBinds pis),
+                 hsep [colonD, !(withPrec Outer $ prettyM a)]]]
diff --git a/src/Quox/Syntax/Term/Reduce.idr b/src/Quox/Syntax/Term/Reduce.idr
new file mode 100644
index 0000000..611fba0
--- /dev/null
+++ b/src/Quox/Syntax/Term/Reduce.idr
@@ -0,0 +1,163 @@
+module Quox.Syntax.Term.Reduce
+
+import Quox.Syntax.Term.Base
+import Quox.Syntax.Term.Subst
+
+
+mutual
+  ||| true if a term has a closure or dimension closure at the top level,
+  ||| or is `E` applied to such an elimination
+  public export %inline
+  topCloT : Term d n -> Bool
+  topCloT (CloT  _ _) = True
+  topCloT (DCloT _ _) = True
+  topCloT (E e)       = topCloE e
+  topCloT _           = False
+
+  ||| true if an elimination has a closure or dimension closure at the top level
+  public export %inline
+  topCloE : Elim d n -> Bool
+  topCloE (CloE  _ _) = True
+  topCloE (DCloE _ _) = True
+  topCloE _           = False
+
+
+public export IsNotCloT : Term d n -> Type
+IsNotCloT = So . not . topCloT
+
+||| a term which is not a top level closure
+public export NotCloTerm : Nat -> Nat -> Type
+NotCloTerm d n = Subset (Term d n) IsNotCloT
+
+public export IsNotCloE : Elim d n -> Type
+IsNotCloE = So . not . topCloE
+
+||| an elimination which is not a top level closure
+public export NotCloElim : Nat -> Nat -> Type
+NotCloElim d n = Subset (Elim d n) IsNotCloE
+
+public export %inline
+ncloT : (t : Term d n) -> (0 _ : IsNotCloT t) => NotCloTerm d n
+ncloT t @{p} = Element t p
+
+public export %inline
+ncloE : (t : Elim d n) -> (0 _ : IsNotCloE t) => NotCloElim d n
+ncloE e @{p} = Element e p
+
+
+
+mutual
+  ||| if the input term has any top-level closures, push them under one layer of
+  ||| syntax
+  export %inline
+  pushSubstsT : Term d n -> NotCloTerm d n
+  pushSubstsT s = pushSubstsTWith id id s
+
+  ||| if the input elimination has any top-level closures, push them under one
+  ||| layer of syntax
+  export %inline
+  pushSubstsE : Elim d n -> NotCloElim d n
+  pushSubstsE e = pushSubstsEWith id id e
+
+  export
+  pushSubstsTWith : DSubst dfrom dto -> TSubst dto from to ->
+                    Term dfrom from -> NotCloTerm dto to
+  pushSubstsTWith th ph (TYPE l) =
+    ncloT $ TYPE l
+  pushSubstsTWith th ph (Pi qtm qty x a body) =
+    ncloT $ Pi qtm qty x (subs a th ph) (subs body th ph)
+  pushSubstsTWith th ph (Lam x body) =
+    ncloT $ Lam x $ subs body th ph
+  pushSubstsTWith th ph (E e) =
+    let Element e _ = pushSubstsEWith th ph e in ncloT $ E e
+  pushSubstsTWith th ph (CloT  s ps) =
+    pushSubstsTWith th (comp' th ps ph) s
+  pushSubstsTWith th ph (DCloT s ps) =
+    pushSubstsTWith (ps . th) ph s
+
+  export
+  pushSubstsEWith : DSubst dfrom dto -> TSubst dto from to ->
+                    Elim dfrom from -> NotCloElim dto to
+  pushSubstsEWith th ph (F x) =
+    ncloE $ F x
+  pushSubstsEWith th ph (B i) =
+    assert_total pushSubstsE $ ph !! i
+  pushSubstsEWith th ph (f :@ s) =
+    ncloE $ subs f th ph :@ subs s th ph
+  pushSubstsEWith th ph (s :# a) =
+    ncloE $ subs s th ph :# subs a th ph
+  pushSubstsEWith th ph (CloE  e ps) =
+    pushSubstsEWith th (comp' th ps ph) e
+  pushSubstsEWith th ph (DCloE e ps) =
+    pushSubstsEWith (ps . th) ph e
+
+
+parameters (th : DSubst dfrom dto) (ph : TSubst dto from to)
+  public export %inline
+  pushSubstsTWith' : Term dfrom from -> Term dto to
+  pushSubstsTWith' s = (pushSubstsTWith th ph s).fst
+
+  public export %inline
+  pushSubstsEWith' : Elim dfrom from -> Elim dto to
+  pushSubstsEWith' e = (pushSubstsEWith th ph e).fst
+
+
+public export %inline
+pushSubstsT' : Term d n -> Term d n
+pushSubstsT' s = (pushSubstsT s).fst
+
+public export %inline
+pushSubstsE' : Elim d n -> Elim d n
+pushSubstsE' e = (pushSubstsE e).fst
+
+
+mutual
+  -- tightening a term/elim also causes substitutions to be pushed through.
+  -- this is because otherwise a variable in an unused part of the subst
+  -- would cause it to incorrectly fail
+
+  export covering
+  Tighten (Term d) where
+    tighten p (TYPE l) =
+      pure $ TYPE l
+    tighten p (Pi qtm qty x arg res) =
+      Pi qtm qty x <$> tighten p arg
+                   <*> tighten p res
+    tighten p (Lam x body) =
+      Lam x <$> tighten p body
+    tighten p (E e) =
+      E <$> tighten p e
+    tighten p (CloT tm th) =
+      tighten p $ pushSubstsTWith' id th tm
+    tighten p (DCloT tm th) =
+      tighten p $ pushSubstsTWith' th id tm
+
+  export covering
+  Tighten (Elim d) where
+    tighten p (F x) =
+      pure $ F x
+    tighten p (B i) =
+      B <$> tighten p i
+    tighten p (fun :@ arg) =
+      [|tighten p fun :@ tighten p arg|]
+    tighten p (tm :# ty) =
+      [|tighten p tm :# tighten p ty|]
+    tighten p (CloE el th) =
+      tighten p $ pushSubstsEWith' id th el
+    tighten p (DCloE el th) =
+      tighten p $ pushSubstsEWith' th id el
+
+  export covering
+  Tighten (ScopeTerm d) where
+    tighten p (TUsed   body) = TUsed   <$> tighten (Keep p) body
+    tighten p (TUnused body) = TUnused <$> tighten p body
+
+
+public export %inline
+weakT : Term d n -> Term d (S n)
+weakT t = t //. shift 1
+
+public export %inline
+weakE : Elim d n -> Elim d (S n)
+weakE t = t //. shift 1
+
diff --git a/src/Quox/Syntax/Term/Split.idr b/src/Quox/Syntax/Term/Split.idr
new file mode 100644
index 0000000..2977ed1
--- /dev/null
+++ b/src/Quox/Syntax/Term/Split.idr
@@ -0,0 +1,82 @@
+module Quox.Syntax.Term.Split
+
+import Quox.Syntax.Term.Base
+import Quox.Syntax.Term.Subst
+
+import Data.So
+import Data.Vect
+
+%default total
+
+
+public export %inline
+isLam : Term d n -> Bool
+isLam (Lam {}) = True
+isLam _        = False
+
+public export
+NotLam : Term d n -> Type
+NotLam = So . not . isLam
+
+
+public export %inline
+isApp : Elim d n -> Bool
+isApp ((:@) {}) = True
+isApp _         = False
+
+public export
+NotApp : Elim d n -> Type
+NotApp = So . not . isApp
+
+
+infixl 9 :@@
+||| apply multiple arguments at once
+public export %inline
+(:@@) : Elim d n -> List (Term d n) -> Elim d n
+f :@@ ss = foldl (:@) f ss
+
+public export
+record GetArgs (d, n : Nat) where
+  constructor GotArgs
+  fun      : Elim d n
+  args     : List (Term d n)
+  0 notApp : NotApp fun
+
+export
+getArgs' : Elim d n -> List (Term d n) -> GetArgs d n
+getArgs' fun args with (choose $ isApp fun)
+  getArgs' (f :@ a) args | Left yes = getArgs' f (a :: args)
+  _ | Right no = GotArgs {fun, args, notApp = no}
+
+||| splits an application into its head and arguments. if it's not an
+||| application then the list is just empty
+export %inline
+getArgs : Elim d n -> GetArgs d n
+getArgs e = getArgs' e []
+
+
+infixr 1 :\\
+public export
+(:\\) : Vect m Name -> Term d (m + n) -> Term d n
+[]      :\\ t = t
+x :: xs :\\ t = let t' = replace {p = Term _} (plusSuccRightSucc {}) t in
+                Lam x $ TUsed $ xs :\\ t'
+
+public export
+record GetLams (d, n : Nat) where
+  constructor GotLams
+  names    : Vect lams Name
+  body     : Term d rest
+  0 eq     : lams + n = rest
+  0 notLam : NotLam body
+
+public export
+getLams : Term d n -> GetLams d n
+getLams s with (choose $ isLam s)
+  getLams s@(Lam x body) | Left yes =
+    let inner = getLams $ assert_smaller s $ fromScopeTerm body in
+    GotLams {names  = x :: inner.names,
+             body   = inner.body,
+             eq     = plusSuccRightSucc {} `trans` inner.eq,
+             notLam = inner.notLam}
+  _ | Right no = GotLams {names = [], body = s, eq = Refl, notLam = no}
diff --git a/src/Quox/Syntax/Term/Subst.idr b/src/Quox/Syntax/Term/Subst.idr
new file mode 100644
index 0000000..1b76225
--- /dev/null
+++ b/src/Quox/Syntax/Term/Subst.idr
@@ -0,0 +1,133 @@
+module Quox.Syntax.Term.Subst
+
+import Quox.Syntax.Term.Base
+
+
+export FromVar (Elim d) where fromVar = B
+export FromVar (Term d) where fromVar = E . fromVar
+
+||| does the minimal reasonable work:
+||| - deletes the closure around a free name since it doesn't do anything
+||| - deletes an identity substitution
+||| - composes (lazily) with an existing top-level closure
+||| - immediately looks up a bound variable
+||| - otherwise, wraps in a new closure
+export
+CanSubst (Elim d) (Elim d) where
+  F x       // _  = F x
+  B i       // th = th !! i
+  CloE e ph // th = assert_total CloE e $ ph . th
+  e         // th = case force th of
+                         Shift SZ => e
+                         th       => CloE e th
+
+||| does the minimal reasonable work:
+||| - deletes the closure around an atomic constant like `TYPE`
+||| - deletes an identity substitution
+||| - composes (lazily) with an existing top-level closure
+||| - goes inside `E` in case it is a simple variable or something
+||| - otherwise, wraps in a new closure
+export
+CanSubst (Elim d) (Term d) where
+  TYPE l    // _  = TYPE l
+  E e       // th = E $ e // th
+  CloT s ph // th = CloT s $ ph . th
+  s         // th = case force th of
+                         Shift SZ => s
+                         th       => CloT s th
+
+export
+CanSubst (Elim d) (ScopeTerm d) where
+  TUsed   body // th = TUsed   $ body // push th
+  TUnused body // th = TUnused $ body // th
+
+export CanSubst Var (Term      d) where s // th = s // map (B {d}) th
+export CanSubst Var (Elim      d) where e // th = e // map (B {d}) th
+export CanSubst Var (ScopeTerm d) where s // th = s // map (B {d}) th
+
+
+infixl 8 //., ///
+mutual
+  namespace Term
+    ||| applies a term substitution with a less ambiguous type
+    export
+    (//.) : Term d from -> TSubst d from to -> Term d to
+    t //. th = t // th
+
+    ||| applies a dimension substitution with the same behaviour as `(//)`
+    ||| above
+    export
+    (///) : Term dfrom n -> DSubst dfrom dto -> Term dto n
+    TYPE l     /// _        = TYPE l
+    E e        /// th       = E $ e /// th
+    DCloT s ph /// th       = DCloT s $ ph . th
+    s          /// Shift SZ = s
+    s          /// th       = DCloT s th
+
+    ||| applies a term and dimension substitution
+    public export %inline
+    subs : Term dfrom from -> DSubst dfrom dto -> TSubst dto from to ->
+           Term dto to
+    subs s th ph = s /// th // ph
+
+  namespace Elim
+    ||| applies a term substitution with a less ambiguous type
+    export
+    (//.) : Elim d from -> TSubst d from to -> Elim d to
+    e //. th = e // th
+
+    ||| applies a dimension substitution with the same behaviour as `(//)`
+    ||| above
+    export
+    (///) : Elim dfrom n -> DSubst dfrom dto -> Elim dto n
+    F x        /// _        = F x
+    B i        /// _        = B i
+    DCloE e ph /// th       = DCloE e $ ph . th
+    e          /// Shift SZ = e
+    e          /// th       = DCloE e th
+
+    ||| applies a term and dimension substitution
+    public export %inline
+    subs : Elim dfrom from -> DSubst dfrom dto -> TSubst dto from to ->
+           Elim dto to
+    subs e th ph = e /// th // ph
+
+  namespace ScopeTerm
+    ||| applies a term substitution with a less ambiguous type
+    export
+    (//.) : ScopeTerm d from -> TSubst d from to -> ScopeTerm d to
+    body //. th = body // th
+
+    ||| applies a dimension substitution with the same behaviour as `(//)`
+    ||| above
+    export
+    (///) : ScopeTerm dfrom n -> DSubst dfrom dto -> ScopeTerm dto n
+    TUsed   body /// th = TUsed   $ body /// th
+    TUnused body /// th = TUnused $ body /// th
+
+    ||| applies a term and dimension substitution
+    public export %inline
+    subs : ScopeTerm dfrom from -> DSubst dfrom dto -> TSubst dto from to ->
+           ScopeTerm dto to
+    subs body th ph = body /// th // ph
+
+export CanShift (Term      d) where s // by = s //. Shift by
+export CanShift (Elim      d) where e // by = e //. Shift by
+export CanShift (ScopeTerm d) where s // by = s //. Shift by
+
+
+export %inline
+comp' : DSubst dfrom dto -> TSubst dfrom from mid -> TSubst dto mid to ->
+        TSubst dto from to
+comp' th ps ph = map (/// th) ps . ph
+
+
+export
+fromDScopeTerm : DScopeTerm d n -> Term (S d) n
+fromDScopeTerm (DUsed   body) = body
+fromDScopeTerm (DUnused body) = body /// shift 1
+
+export
+fromScopeTerm : ScopeTerm d n -> Term d (S n)
+fromScopeTerm (TUsed   body) = body
+fromScopeTerm (TUnused body) = body //. shift 1
diff --git a/src/Quox/Typechecker.idr b/src/Quox/Typechecker.idr
new file mode 100644
index 0000000..973ed89
--- /dev/null
+++ b/src/Quox/Typechecker.idr
@@ -0,0 +1,142 @@
+module Quox.Typechecker
+
+import public Quox.Syntax
+import public Quox.Typing
+import Quox.Error
+
+%default total
+
+
+private covering %inline
+expectTYPE : MonadThrow Typing.Error m => Term d n -> m Universe
+expectTYPE s =
+  case (whnfT s).fst of
+       TYPE l => pure l
+       _      => throw $ ExpectedTYPE s
+
+private covering %inline
+expectPi : MonadThrow Typing.Error m => Term d n ->
+           m (Qty, Qty, Term d n, ScopeTerm d n)
+expectPi ty =
+  case (whnfT ty).fst of
+       Pi qtm qty _ arg res => pure (qtm, qty, arg, res)
+       _                    => throw $ ExpectedPi ty
+
+private %inline
+expectEqualQ : MonadThrow Equal.Error m =>
+               (expect, actual : Qty) -> m ()
+expectEqualQ pi rh = unless (pi == rh) $ throw $ ClashQ pi rh
+
+
+private %inline
+popQ : MonadThrow Equal.Error m => Qty -> QOutput (S n) -> m (QOutput n)
+popQ pi (qctx :< rh) = expectEqualQ pi rh $> qctx
+
+
+private %inline
+tail : TyContext d (S n) -> TyContext d n
+tail = {tctx $= tail, qctx $= tail}
+
+
+private %inline
+weakI : InferResult d n -> InferResult d (S n)
+weakI = {type $= weakT, tmout $= (:< zero), tyout $= (:< zero)}
+
+private
+lookupBound : {n : Nat} -> Var n -> TyContext d n -> InferResult d n
+lookupBound VZ (MkTyContext {tctx = _ :< ty, qctx = _ :< tyout, _}) =
+  InfRes {type = weakT ty, tmout = zero :< one, tyout = tyout :< zero}
+lookupBound (VS i) ctx =
+  weakI $ lookupBound i (tail ctx)
+
+
+mutual
+  -- [todo] it seems like the options here for dealing with substitutions are
+  -- to either push them or parametrise the whole typechecker over ambient
+  -- substitutions. both of them seem like the same amount of work for the
+  -- computer but pushing is less work for the me
+
+  export covering %inline
+  check : MonadThrows [Typing.Error, Equal.Error] m => {d, n : Nat} ->
+          (ctx : TyContext d n) -> (subj : Term d n) -> (ty : Term d n) ->
+          m (CheckResult n)
+  check ctx subj ty = check' ctx (pushSubstsT subj) ty
+
+  export covering %inline
+  infer : MonadThrows [Typing.Error, Equal.Error] m => {d, n : Nat} ->
+          (ctx : TyContext d n) -> (subj : Elim d n) ->
+          m (InferResult d n)
+  infer ctx subj = infer' ctx (pushSubstsE subj)
+
+
+  export covering
+  check' : MonadThrows [Typing.Error, Equal.Error] m => {d, n : Nat} ->
+           (ctx : TyContext d n) ->
+           (subj : NotCloTerm d n) -> (ty : Term d n) ->
+           m (CheckResult n)
+
+  check' ctx (Element (TYPE l) _) ty = do
+    l' <- expectTYPE ty
+    unless (l < l') $ throw $ BadUniverse l l'
+    pure $ ChkRes {tmout = zero, tyout = zero}
+
+  -- [todo] factor this stuff out
+  check' ctx (Element (Pi qtm qty x arg (TUsed res)) _) ty = do
+    l <- expectTYPE ty
+    argty <- check ctx arg (TYPE l)
+    resty <- check (extendTy arg argty.tmout ctx) res (TYPE l)
+    res'tmout <- popQ qty resty.tmout
+    pure $ ChkRes {tmout = argty.tmout + res'tmout, tyout = zero}
+  check' ctx (Element (Pi qtm qty x arg (TUnused res)) _) ty = do
+    ignore $ expectTYPE ty
+    argty <- check ctx arg ty
+    resty <- check ctx res ty
+    expectEqualQ qty zero
+    pure $ ChkRes {tmout = argty.tmout + resty.tmout, tyout = zero}
+
+  check' ctx (Element (Lam x body) _) ty = do
+    (qtm, qty, arg, res) <- expectPi ty
+    -- [todo] do this properly?
+    let body = fromScopeTerm body; res = fromScopeTerm res
+    argres <- check ctx arg (TYPE UAny)
+    let ctx' = extendTy arg argres.tmout ctx
+    bodyres <- check ctx' body res
+    tmout <- popQ qtm bodyres.tmout
+    tyout <- popQ qty bodyres.tyout
+    pure $ ChkRes {tmout, tyout = argres.tmout + tyout}
+
+  check' ctx (Element (E e) _) ty = do
+    infres <- infer ctx e
+    tyres  <- check ctx ty (TYPE UAny)
+    infres.type `subT` ty
+    pure $ ChkRes {tmout = infres.tmout, tyout = tyres.tmout}
+
+  export covering
+  infer' : MonadThrows [Typing.Error, Equal.Error] m => {d, n : Nat} ->
+           (ctx : TyContext d n) -> (subj : NotCloElim d n) ->
+           m (InferResult d n)
+
+  infer' ctx (Element (F x) _) =
+    case lookup x ctx.globals of
+         Just g  => pure $ InfRes {type = g.type, tmout = zero, tyout = zero}
+         Nothing => throw $ NotInScope x
+
+  infer' ctx (Element (B i) _) = pure $ lookupBound i ctx
+
+  infer' ctx (Element (fun :@ arg) _) = do
+    funres <- infer ctx fun
+    (qtm, qty, argty, resty) <- expectPi funres.type
+    let resty = fromScopeTerm resty
+    argres <- check ctx arg argty
+    let ctx' = extendTy argty argres.tyout ctx
+    resres <- check ctx' resty (TYPE UAny)
+    res'tyout <- popQ qty resres.tmout
+    let type = resty //. (arg :# argty ::: id)
+    pure $ InfRes {type,
+                   tmout = funres.tmout + qtm * argres.tmout,
+                   tyout = res'tyout    + qty * argres.tmout}
+
+  infer' ctx (Element (tm :# ty) _) = do
+    ignore $ check ctx ty (TYPE UAny)
+    res <- check ctx tm ty
+    pure $ InfRes {type = ty, tmout = res.tmout, tyout = res.tyout}
diff --git a/src/Quox/Typing.idr b/src/Quox/Typing.idr
index f3e1406..a3174f9 100644
--- a/src/Quox/Typing.idr
+++ b/src/Quox/Typing.idr
@@ -2,9 +2,10 @@ module Quox.Typing
 
 import public Quox.Syntax
 import public Quox.Context
+import public Quox.Equal
 
 import Data.Nat
-import Data.SortedMap
+import public Data.SortedMap
 import Control.Monad.Reader
 import Control.Monad.State
 
@@ -83,3 +84,23 @@ namespace QOutput
   export
   zero : {n : Nat} -> QOutput n
   zero = pure Zero
+
+
+public export
+record CheckResult n where
+  constructor ChkRes
+  tmout, tyout : QOutput n
+
+public export
+record InferResult d n where
+  constructor InfRes
+  type : Term d n
+  tmout, tyout : QOutput n
+
+
+public export
+data Error
+= NotInScope Name
+| ExpectedTYPE (Term d n)
+| ExpectedPi   (Term d n)
+| BadUniverse Universe Universe