From e1c22b664c7d5a3652c0dd5b095327aff7568994 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Tue, 20 Jul 2021 22:05:19 +0200
Subject: [PATCH] some syntax stuff

---
 quox.ipkg                    |   2 +-
 src/Quox.idr                 |  19 +-
 src/Quox/Ctx.idr             |  98 ++++++++++
 src/Quox/Name.idr            |  52 ++++++
 src/Quox/Pretty.idr          | 200 +++++++++++++++++++++
 src/Quox/Syntax/Dim.idr      |  50 ++++++
 src/Quox/Syntax/Qty.idr      |  54 ++++++
 src/Quox/Syntax/Shift.idr    | 174 ++++++++++++++++++
 src/Quox/Syntax/Subst.idr    | 121 +++++++++++++
 src/Quox/Syntax/Term.idr     | 340 +++++++++++++++++++++++++++++++++++
 src/Quox/Syntax/Universe.idr |  28 +++
 src/Quox/Syntax/Var.idr      | 142 +++++++++++++++
 12 files changed, 1278 insertions(+), 2 deletions(-)
 create mode 100644 src/Quox/Ctx.idr
 create mode 100644 src/Quox/Name.idr
 create mode 100644 src/Quox/Pretty.idr
 create mode 100644 src/Quox/Syntax/Dim.idr
 create mode 100644 src/Quox/Syntax/Qty.idr
 create mode 100644 src/Quox/Syntax/Shift.idr
 create mode 100644 src/Quox/Syntax/Subst.idr
 create mode 100644 src/Quox/Syntax/Term.idr
 create mode 100644 src/Quox/Syntax/Universe.idr
 create mode 100644 src/Quox/Syntax/Var.idr

diff --git a/quox.ipkg b/quox.ipkg
index e9db42b..b604c48 100644
--- a/quox.ipkg
+++ b/quox.ipkg
@@ -9,4 +9,4 @@ executable = quox
 main = Quox
 sourcedir = "src"
 
-depends = base
+depends = base, contrib
diff --git a/src/Quox.idr b/src/Quox.idr
index 39512b5..cd617fa 100644
--- a/src/Quox.idr
+++ b/src/Quox.idr
@@ -1,4 +1,21 @@
 module Quox
 
+import public Quox.Syntax.Term
+import public Quox.Pretty
+
+import Data.Nat
+import Data.Vect
+
+
+export
+tm : Term 1 2
+tm =
+  (Pi Zero One "a" (BVT 0) (E (F "F" :@@ [BVT 0, FT "w"]))
+    `DCloT` (DOne ::: id))
+    `CloT`  (F "y" ::: TYPE (U 1) :# TYPE (U 2) ::: id)
+
 main : IO Unit
-main = putStrLn ":qtuwu:"
+main = do
+  prettyTerm tm
+  prettyTerm $ pushSubstsT tm
+  putStrLn ":qtuwu:"
diff --git a/src/Quox/Ctx.idr b/src/Quox/Ctx.idr
new file mode 100644
index 0000000..56a2991
--- /dev/null
+++ b/src/Quox/Ctx.idr
@@ -0,0 +1,98 @@
+module Quox.Ctx
+
+import Data.Nat
+import Data.Fin
+import Data.SnocList
+import Data.DPair
+
+
+%default total
+
+public export
+data Ctx : Nat -> (Nat -> Type) -> Type where
+  Lin  : Ctx 0 f
+  (:<) : Ctx n f -> f n -> Ctx (S n) f
+
+%name Ctx ctx
+
+
+public export
+0 Ctx' : Nat -> Type -> Type
+Ctx' n a = Ctx n (\_ => a)
+
+
+public export
+toSList : Ctx n f -> SnocList (Exists f)
+toSList [<]        = [<]
+toSList (ctx :< x) = toSList ctx :< Evidence _ x
+
+public export
+toSList' : Ctx' n a -> SnocList a
+toSList' ctx = map (.snd) $ toSList ctx
+
+public export
+fromSList' : (xs : SnocList a) -> Ctx' (length xs) a
+fromSList' [<]       = [<]
+fromSList' (sx :< x) = fromSList' sx :< x
+
+
+public export
+0 Weaken : (Nat -> Type) -> Type
+Weaken f = forall n. (by : Nat) -> (1 x : f n) -> f (by + n)
+
+public export
+interface Weak f where weakN : Weaken f
+
+public export
+weak : Weak f => (1 x : f n) -> f (S n)
+weak = weakN 1
+
+
+public export
+lookBy : Weaken f -> Ctx n f -> (1 _ : Fin n) -> f n
+lookBy w = go 0 where
+  go : forall n. (by : Nat) -> Ctx n f -> (1 _ : Fin n) -> f (by + n)
+  go by (ctx :< x) (FZ {k})   =
+    rewrite sym $ plusSuccRightSucc by k in w (S by) x
+  go by (ctx :< x) (FS {k} i) =
+    rewrite sym $ plusSuccRightSucc by k in go (S by) ctx i
+
+public export
+look : Weak f => Ctx n f -> (1 _ : Fin n) -> f n
+look = lookBy weakN
+
+infixl 9 !!
+public export
+(!!) : Ctx' n a -> (1 _ : Fin n) -> a
+(!!) = lookBy (\_, x => x)
+
+
+public export
+map : (forall n. f n -> g n) -> (1 _ : Ctx n f) -> Ctx n g
+map f [<]        = [<]
+map f (ctx :< x) = map f ctx :< f x
+
+
+public export
+(forall n. Eq (f n)) => Eq (Ctx n f) where
+  [<]         == [<]         = True
+  (ctx1 :< x) == (ctx2 :< y) = ctx1 == ctx2 && x == y
+
+public export
+(forall n. Ord (f n)) => Ord (Ctx n f) where
+  compare [<]         [<]         = EQ
+  compare (ctx1 :< x) (ctx2 :< y) = compare ctx1 ctx2 <+> compare x y
+
+
+||| like `Exists` but only shows the second part
+private
+data ShowWrapper : (Nat -> Type) -> Type where
+  SW : f n -> ShowWrapper f
+
+private
+(forall n. Show (f n)) => Show (ShowWrapper f) where
+  showPrec d (SW x) = showPrec d x
+
+export
+(forall n. Show (f n)) => Show (Ctx n f) where
+  show = show . map (\x => SW {f} x.snd) . toSList
diff --git a/src/Quox/Name.idr b/src/Quox/Name.idr
new file mode 100644
index 0000000..c432667
--- /dev/null
+++ b/src/Quox/Name.idr
@@ -0,0 +1,52 @@
+module Quox.Name
+
+import public Data.SnocList
+
+%default total
+
+
+public export
+data BaseName =
+    UN String -- user-given name
+
+private 0 BRepr : Type
+BRepr = String
+
+private %inline brepr : BaseName -> BRepr
+brepr (UN x) = x
+
+export Eq  BaseName where (==) = (==) `on` brepr
+export Ord BaseName where compare = compare `on` brepr
+
+export
+baseStr : BaseName -> String
+baseStr (UN x) = x
+
+export
+FromString BaseName where
+  fromString = UN
+
+
+public export
+record Name where
+  constructor MakeName
+  mods : SnocList String
+  base : BaseName
+
+private 0 Repr : Type
+Repr = (SnocList String, BRepr)
+
+private %inline repr : Name -> Repr
+repr x = (x.mods, brepr x.base)
+
+export Eq  Name where (==) = (==) `on` repr
+export Ord Name where compare = compare `on` repr
+
+export
+FromString Name where
+  fromString x = MakeName [<] (fromString x)
+
+
+export
+toDots : Name -> String
+toDots x = fastConcat $ cast $ map (<+> ".") x.mods :< baseStr x.base
diff --git a/src/Quox/Pretty.idr b/src/Quox/Pretty.idr
new file mode 100644
index 0000000..9393b36
--- /dev/null
+++ b/src/Quox/Pretty.idr
@@ -0,0 +1,200 @@
+module Quox.Pretty
+
+import Quox.Name
+
+import public Text.PrettyPrint.Prettyprinter.Doc
+import Text.PrettyPrint.Prettyprinter.Render.String
+import Text.PrettyPrint.Prettyprinter.Render.Terminal
+import public Data.String
+import Data.DPair
+
+import public Control.Monad.Identity
+import public Control.Monad.Reader
+
+%default total
+
+
+public export
+data HL
+  = Delim
+  | TVar
+  | TVarErr
+  | Dim
+  | DVar
+  | DVarErr
+  | Qty
+  | Free
+  | Syntax
+
+private 0 HLRepr : Type
+HLRepr = Nat
+
+private %inline hlRepr : HL -> Nat
+hlRepr Delim   = 0
+hlRepr TVar    = 1
+hlRepr TVarErr = 2
+hlRepr Dim     = 3
+hlRepr DVar    = 4
+hlRepr DVarErr = 5
+hlRepr Qty     = 6
+hlRepr Free    = 7
+hlRepr Syntax  = 8
+
+export Eq  HL where (==) = (==) `on` hlRepr
+export Ord HL where compare = compare `on` hlRepr
+
+
+public export
+data PPrec
+  = Outer
+  | Ann  -- right of "::"
+  | AnnL -- left  of "::"
+  -- ...
+  | App  -- term/dimension application
+  | SApp -- substitution application
+  | Arg
+
+private 0 PrecRepr : Type
+PrecRepr = Nat
+
+private %inline precRepr : PPrec -> PrecRepr
+precRepr Outer = 0
+precRepr Ann   = 1
+precRepr AnnL  = 2
+-- ...
+precRepr App   = 98
+precRepr SApp  = 99
+precRepr Arg   = 100
+
+export Eq  PPrec where (==) = (==) `on` precRepr
+export Ord PPrec where compare = compare `on` precRepr
+
+
+export %inline
+hl : HL -> Doc HL -> Doc HL
+hl = annotate
+
+export %inline
+hl' : HL -> Doc HL -> Doc HL
+hl' h = hl h . unAnnotate
+
+export %inline
+hlF : Functor f => HL -> f (Doc HL) -> f (Doc HL)
+hlF = map . hl
+
+export %inline
+hlF' : Functor f => HL -> f (Doc HL) -> f (Doc HL)
+hlF' = map . hl'
+
+
+export
+parens : Doc HL -> Doc HL
+parens doc = hl Delim "(" <+> doc <+> hl Delim ")"
+
+export
+parensIf : Bool -> Doc HL -> Doc HL
+parensIf True  = parens
+parensIf False = id
+
+
+public export
+record PrettyEnv where
+  constructor MakePrettyEnv
+  ||| names of bound dimension variables
+  dnames  : List Name
+  ||| names of bound term variables
+  tnames  : List Name
+  ||| use non-ascii characters for syntax
+  unicode : Bool
+  ||| surrounding precedence level
+  prec    : PPrec
+
+public export
+0 M : Type -> Type
+M = Reader PrettyEnv
+
+export
+ifUnicode : (uni, asc : Lazy a) -> M a
+ifUnicode uni asc = if unicode !ask then [|uni|] else [|asc|]
+
+export
+parensIfM : PPrec -> Doc HL -> M (Doc HL)
+parensIfM d doc = pure $ parensIf (prec !ask > d) doc
+
+export
+withPrec : PPrec -> M a -> M a
+withPrec d = local {prec := d}
+
+public export data BinderSort = T | D
+
+export
+under : BinderSort -> Name -> M a -> M a
+under s x = local $
+  {prec := Outer} .
+  (case s of T => {tnames $= (x ::)}; D => {dnames $= (x ::)})
+
+
+public export
+interface PrettyHL a where
+  prettyM : a -> M (Doc HL)
+
+public export %inline
+pretty0M : PrettyHL a => a -> M (Doc HL)
+pretty0M = local {prec := Outer} . prettyM
+
+public export %inline
+pretty0 : PrettyHL a => {default True unicode : Bool} -> a -> Doc HL
+pretty0 x {unicode} =
+  let env = MakePrettyEnv {dnames = [], tnames = [], unicode, prec = Outer} in
+  runReader env $ prettyM x
+
+
+export
+(forall a. PrettyHL (f a)) => PrettyHL (Exists f) where
+  prettyM x = prettyM x.snd
+
+export
+PrettyHL a => PrettyHL (Subset a b) where
+  prettyM x = prettyM x.fst
+
+
+export PrettyHL BaseName where prettyM = pure . pretty . baseStr
+export PrettyHL Name     where prettyM = pure . pretty . toDots
+
+
+export
+prettyStr : PrettyHL a => {default True unicode : Bool} -> a -> String
+prettyStr {unicode} =
+  renderString .
+  layoutSmart (MkLayoutOptions (AvailablePerLine 80 0.8)) .
+  pretty0 {unicode}
+
+
+export
+termHL : HL -> AnsiStyle
+termHL Delim   = color BrightBlack
+termHL TVar    = color BrightYellow
+termHL TVarErr = color BrightYellow  <+> underline
+termHL Dim     = color BrightGreen   <+> bold
+termHL DVar    = color BrightGreen
+termHL DVarErr = color BrightGreen   <+> underline
+termHL Qty     = color BrightMagenta <+> bold
+termHL Free    = color BrightWhite
+termHL Syntax  = color BrightBlue
+
+export
+prettyTerm : {default True color, unicode : Bool} -> PrettyHL a => a -> IO Unit
+prettyTerm x {color, unicode} =
+  let reann = if color then map termHL else unAnnotate in
+  Terminal.putDoc $ reann $ pretty0 x {unicode}
+
+
+infixr 6 <//>
+export %inline
+(<//>) : Doc a -> Doc a -> Doc a
+a <//> b = sep [a, b]
+
+infixr 6 </>
+export %inline
+(</>) : Doc a -> Doc a -> Doc a
+a </> b = cat [a, b]
diff --git a/src/Quox/Syntax/Dim.idr b/src/Quox/Syntax/Dim.idr
new file mode 100644
index 0000000..81ce290
--- /dev/null
+++ b/src/Quox/Syntax/Dim.idr
@@ -0,0 +1,50 @@
+module Quox.Syntax.Dim
+
+import Quox.Syntax.Var
+import Quox.Syntax.Subst
+import Quox.Pretty
+
+%default total
+
+
+public export
+data Dim : Nat -> Type where
+  DZero, DOne : Dim d
+  DBound : Var d -> Dim d
+%name Dim.Dim p, q
+
+private DRepr : Type
+DRepr = Nat
+
+private %inline drepr : Dim n -> DRepr
+drepr d = case d of DZero => 0; DOne => 1; DBound i => 2 + i.nat
+
+export Eq  (Dim n) where (==) = (==) `on` drepr
+export Ord (Dim n) where compare = compare `on` drepr
+
+export
+PrettyHL (Dim n) where
+  prettyM DZero      = hl Dim <$> ifUnicode "𝟬" "0"
+  prettyM DOne       = hl Dim <$> ifUnicode "𝟭" "1"
+  prettyM (DBound i) = prettyVar DVar DVarErr (!ask).dnames i
+
+
+public export
+0 DSubst : Nat -> Nat -> Type
+DSubst = Subst Dim
+
+
+export %inline
+prettyDSubst : DSubst from to -> Pretty.M (Doc HL)
+prettyDSubst th =
+  prettySubstM prettyM (dnames !ask) DVar
+    !(ifUnicode "⟨" "<") !(ifUnicode "⟩" ">") th
+
+
+export FromVar Dim where fromVar = DBound
+
+export
+CanSubst Dim Dim where
+  DZero    // _  = DZero
+  DOne     // _  = DOne
+  DBound i // th = th !! i
diff --git a/src/Quox/Syntax/Qty.idr b/src/Quox/Syntax/Qty.idr
new file mode 100644
index 0000000..632198a
--- /dev/null
+++ b/src/Quox/Syntax/Qty.idr
@@ -0,0 +1,54 @@
+module Quox.Syntax.Qty
+
+import Quox.Pretty
+
+import Data.Fin
+
+
+public export
+data Qty = Zero | One | Many
+%name Qty.Qty pi, rh
+
+private Repr : Type
+Repr = Fin 3
+
+private %inline repr : Qty -> Repr
+repr pi = case pi of Zero => 0; One => 1; Many => 2
+
+export Eq  Qty where (==) = (==) `on` repr
+export Ord Qty where compare = compare `on` repr
+
+
+export
+PrettyHL Qty where
+  prettyM pi = hl Qty <$>
+    case pi of
+      Zero => ifUnicode "𝟬" "0"
+      One  => ifUnicode "𝟭" "1"
+      Many => ifUnicode "𝛚" "*"
+
+export %inline
+prettyQtyBinds : List Qty -> M (Doc HL)
+prettyQtyBinds =
+  map (align . sep) .
+  traverse (\pi => [|pretty0M pi <++> pure (hl Delim "|")|])
+
+
+public export
+(+) : Qty -> Qty -> Qty
+Zero + rh   = rh
+pi   + Zero = pi
+_    + _    = Many
+
+public export
+(*) : Qty -> Qty -> Qty
+Zero * _    = Zero
+_    * Zero = Zero
+One  * rh   = rh
+pi   * One  = pi
+Many * Many = Many
+
+infix 6 <=.
+public export
+(<=.) : Qty -> Qty -> Bool
+pi <=. rh = rh == Many || pi == rh
diff --git a/src/Quox/Syntax/Shift.idr b/src/Quox/Syntax/Shift.idr
new file mode 100644
index 0000000..eea3d69
--- /dev/null
+++ b/src/Quox/Syntax/Shift.idr
@@ -0,0 +1,174 @@
+module Quox.Syntax.Shift
+
+import public Quox.Syntax.Var
+import Quox.Pretty
+
+import Data.Nat
+import Data.So
+
+%default total
+
+
+||| represents the difference between a smaller scope and a larger one.
+public export
+data Shift : (0 from, to : Nat) -> Type where
+  SZ : Shift from from
+  SS : Shift from to -> Shift from (S to)
+%name Shift by, bz
+%builtin Natural Shift
+
+public export
+(.nat) : Shift from to -> Nat
+(SZ).nat    = Z
+(SS by).nat = S by.nat
+%transform "Shift.(.nat)" Shift.(.nat) = believe_me
+
+public export Cast (Shift from to) Nat where cast = (.nat)
+
+export Eq  (Shift from to) where (==) = (==) `on` (.nat)
+export Ord (Shift from to) where compare = compare `on` (.nat)
+
+
+||| shift equivalence, ignoring indices
+public export
+data Eqv : Shift from1 to1 -> Shift from2 to2 -> Type where
+  EqSZ : SZ `Eqv` SZ
+  EqSS : by `Eqv` bz -> SS by `Eqv` SS bz
+%name Eqv e
+
+||| two equivalent shifts are equal if they have the same indices.
+export
+0 fromEqv : by `Eqv` bz -> by = bz
+fromEqv EqSZ     = Refl
+fromEqv (EqSS e) = cong SS $ fromEqv e
+
+||| two equal shifts are equivalent.
+export
+0 toEqv : by = bz -> by `Eqv` bz
+toEqv Refl {by = SZ}      = EqSZ
+toEqv Refl {by = (SS by)} = EqSS $ toEqv Refl {by}
+
+
+public export
+0 shiftDiff : (by : Shift from to) -> to = by.nat + from
+shiftDiff SZ      = Refl
+shiftDiff (SS by) = cong S $ shiftDiff by
+
+export
+0 shiftVarLT : (by : Shift from to) -> (i : Var from) ->
+               by.nat + i.nat `LT` to
+shiftVarLT by i =
+  rewrite plusSuccRightSucc by.nat i.nat in
+  transitive {rel=LTE}
+    (plusLteMonotoneLeft by.nat (S i.nat) from (toNatLT i))
+    (replace {p=(\n => LTE n to)} (shiftDiff by) $ reflexive {rel=LTE})
+
+
+public export
+fromNat : (by : Nat) -> Shift from (by + from)
+fromNat Z      = SZ
+fromNat (S by) = SS $ fromNat by
+%transform "Shift.fromNat" Shift.fromNat x = believe_me x
+
+export
+0 fromToNat : (by : Shift from to) -> by `Eqv` fromNat by.nat {from}
+fromToNat SZ      = EqSZ
+fromToNat (SS by) = EqSS $ fromToNat by
+
+export
+0 toFromNat : (from, by : Nat) -> by = (fromNat by {from}).nat
+toFromNat from 0     = Refl
+toFromNat from (S k) = cong S $ toFromNat from k
+
+export
+0 toNatInj' : (by : Shift from1 to1) -> (bz : Shift from2 to2) ->
+              by.nat = bz.nat -> by `Eqv` bz
+toNatInj' SZ      SZ      prf = EqSZ
+toNatInj' (SS by) (SS bz) prf = EqSS $ toNatInj' by bz $ succInjective _ _ prf
+toNatInj' (SS by) SZ      Refl impossible
+
+export
+0 toNatInj : (by, bz : Shift from to) -> by.nat = bz.nat -> by = bz
+toNatInj by bz e = fromEqv $ toNatInj' by bz e
+
+
+public export
+shift : Shift from to -> Var from -> Var to
+shift SZ      i = i
+shift (SS by) i = VS $ shift by i
+
+private
+shiftViaNat' : (by : Shift from to) -> (i : Var from) ->
+               (0 p : by.nat + i.nat `LT` to) -> Var to
+shiftViaNat' by i p = V $ by.nat + i.nat
+
+private
+shiftViaNat : Shift from to -> Var from -> Var to
+shiftViaNat by i = shiftViaNat' by i $ shiftVarLT by i
+
+private
+0 shiftViaNatCorrect : (by : Shift from to) -> (i : Var from) ->
+                       (0 p : by.nat + i.nat `LT` to) ->
+                       shiftViaNat' by i p = shift by i
+shiftViaNatCorrect SZ      i (LTESucc p) = fromToNat i _
+shiftViaNatCorrect (SS by) i (LTESucc p) = cong VS $ shiftViaNatCorrect by i p
+
+%transform "Shift.shift" shift = shiftViaNat
+
+
+infixl 9 .
+public export
+(.) : Shift from mid -> Shift mid to -> Shift from to
+by . SZ    = by
+by . SS bz = SS $ by . bz
+
+private
+0 compNatProof : (by : Shift from mid) -> (bz : Shift mid to) ->
+                 to = by.nat + bz.nat + from
+compNatProof by bz =
+  shiftDiff bz                       >>>
+  cong (bz.nat +) (shiftDiff by)     >>>
+  plusAssociative bz.nat by.nat from >>>
+  cong (+ from) (plusCommutative bz.nat by.nat)
+ where
+  infixr 0 >>>
+  0 (>>>) : a = b -> b = c -> a = c
+  x >>> y = trans x y
+
+private
+compViaNat' : (by : Shift from mid) -> (bz : Shift mid to) ->
+              Shift from (by.nat + bz.nat + from)
+compViaNat' by bz = fromNat $ by.nat + bz.nat
+
+private
+compViaNat : (by : Shift from mid) -> (bz : Shift mid to) -> Shift from to
+compViaNat by bz = rewrite compNatProof by bz in compViaNat' by bz
+
+private
+0 compViaNatCorrect : (by : Shift from mid) -> (bz : Shift mid to) ->
+                      by . bz `Eqv` compViaNat' by bz
+compViaNatCorrect by SZ =
+  rewrite plusZeroRightNeutral by.nat in fromToNat by
+compViaNatCorrect by (SS bz) =
+  rewrite sym $ plusSuccRightSucc by.nat bz.nat in
+  EqSS $ compViaNatCorrect by bz
+
+%transform "Shift.(.)" Shift.(.) = compViaNat
+
+
+||| `prettyShift bnd unicode prec by` pretty-prints the shift `by`, with the
+||| following arguments:
+|||
+||| * `by : Shift from to`
+||| * `bnd : HL` is the highlight used for bound variables of this kind
+||| * `unicode : Bool` is whether to use unicode characters in the output
+||| * `prec : PPrec` is the surrounding precedence level
+export
+prettyShift : (bnd : HL) -> Shift from to -> Pretty.M (Doc HL)
+prettyShift bnd by =
+  parensIfM Outer $ hsep $
+    [hl bnd   !(ifUnicode "𝑖"  "i"), hl Delim !(ifUnicode "≔" ":="),
+     hl bnd $ !(ifUnicode "𝑖+" "i+") <+> pretty by.nat]
+
+||| prints using the `TVar` highlight for variables
+export PrettyHL (Shift from to) where prettyM = prettyShift TVar
diff --git a/src/Quox/Syntax/Subst.idr b/src/Quox/Syntax/Subst.idr
new file mode 100644
index 0000000..a25155d
--- /dev/null
+++ b/src/Quox/Syntax/Subst.idr
@@ -0,0 +1,121 @@
+module Quox.Syntax.Subst
+
+import Quox.Syntax.Shift
+import Quox.Syntax.Var
+import Quox.Name
+import Quox.Pretty
+
+import Data.List
+
+%default total
+
+
+infixr 5 :::
+public export
+data Subst : (Nat -> Type) -> Nat -> Nat -> Type where
+  Shift : Shift from to -> Subst env from to
+  (:::) : (t : Lazy (env to)) -> Subst env from to -> Subst env (S from) to
+%name Subst th, ph, ps
+
+
+private
+Repr : (Nat -> Type) -> Nat -> Type
+Repr f to = (List (f to), Nat)
+
+private
+repr : Subst f from to -> Repr f to
+repr (Shift by) = ([], by.nat)
+repr (t ::: th) = let (ts, i) = repr th in (t::ts, i)
+
+
+export Eq  (f to) => Eq  (Subst f from to) where (==) = (==) `on` repr
+export Ord (f to) => Ord (Subst f from to) where compare = compare `on` repr
+
+
+infixl 8 //
+public export
+interface FromVar env => CanSubst env term where
+  (//) : term from -> Subst env from to -> term to
+
+public export
+0 CanSubst1 : (Nat -> Type) -> Type
+CanSubst1 f = CanSubst f f
+
+
+infixl 8 !!
+public export
+(!!) : FromVar term => Subst term from to -> Var from -> term to
+(Shift by) !! i      = fromVar $ shift by i
+(t ::: th) !! VZ     = t
+(t ::: th) !! (VS i) = th !! i
+
+
+public export
+CanSubst Var Var where
+  i    // Shift by     = shift by i
+  VZ   // (t ::: th) = t
+  VS i // (t ::: th) = i // th
+
+
+public export %inline
+shift : (by : Nat) -> Subst env from (by + from)
+shift by = Shift $ fromNat by
+
+
+infixl 9 .
+public export
+(.) : CanSubst1 f => Subst f from mid -> Subst f mid to -> Subst f from to
+Shift SZ      . ph         = ph
+Shift (SS by) . Shift bz   = Shift $ SS by . bz
+Shift (SS by) . (t ::: th) = Shift by . th
+(t ::: th)    . ph         = (t // ph) ::: (th . ph)
+
+public export %inline
+id : Subst f n n
+id = shift 0
+
+public export
+map : (f to -> g to) -> Subst f from to -> Subst g from to
+map f (Shift by) = Shift by
+map f (t ::: th) = f t ::: map f th
+
+
+public export %inline
+push : CanSubst1 f => Subst f from to -> Subst f (S from) (S to)
+push th = fromVar VZ ::: (th . shift 1)
+
+
+||| `prettySubst pr bnd op cl unicode th` pretty-prints the substitution `th`,
+||| with the following arguments:
+|||
+||| * `th : Subst f from to`
+||| * `pr : (unicode : Bool) -> f to -> m (Doc HL)` prints a single element
+||| * `names : List Name` is a list of known bound var names
+||| * `bnd : HL` is the highlight to use for bound variables being subsituted
+||| * `op, cl : Doc HL` are the opening and closing brackets
+||| * `unicode : Bool` is whether to use unicode characters in the output
+|||   (also passed into `pr`)
+export
+prettySubstM : (pr : f to -> Pretty.M (Doc HL)) ->
+               (names : List Name) ->
+               (bnd : HL) -> (op, cl : Doc HL) ->
+               Subst f from to -> Pretty.M (Doc HL)
+prettySubstM pr names bnd op cl th =
+  encloseSep (hl Delim op) (hl Delim cl) (hl Delim "; ") <$>
+    withPrec Outer (go 0 th)
+ where
+  go1 : Nat -> f to -> Pretty.M (Doc HL)
+  go1 i t = pure $ hang 2 $ sep
+    [hsep [!(prettyVar' bnd bnd names i),
+           hl Delim !(ifUnicode "≔" ":=")],
+     !(pr t)]
+
+  go : forall from. Nat -> Subst f from to -> Pretty.M (List (Doc HL))
+  go _ (Shift SZ) = pure []
+  go _ (Shift by) = [|pure (prettyShift bnd by)|]
+  go i (t ::: th) = [|go1 i t :: go (S i) th|]
+
+||| prints with [square brackets] and the `TVar` highlight for variables
+export
+PrettyHL (f to) => PrettyHL (Subst f from to) where
+  prettyM th = prettySubstM prettyM (tnames !ask) TVar "[" "]" th
diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr
new file mode 100644
index 0000000..50d8e8d
--- /dev/null
+++ b/src/Quox/Syntax/Term.idr
@@ -0,0 +1,340 @@
+module Quox.Syntax.Term
+
+import public Quox.Ctx
+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 Quox.Pretty
+
+import public Data.DPair
+import Data.List
+import Data.Maybe
+import Data.Nat
+import public Data.So
+import Data.String
+
+%default total
+
+
+infixl 8 :#
+infixl 9 :@
+mutual
+  public export
+  0 TSubst : Nat -> Nat -> Nat -> Type
+  TSubst d = Subst (Elim d)
+
+  ||| 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  : (qty, qtm : Qty) -> (x : Name) ->
+          (a : Term d n) -> (b : Term d (S n)) -> Term d n
+    ||| function term
+    Lam : (x : Name) -> (t : Term d (S n)) -> Term d n
+
+    ||| elimination
+    E : (e : Elim d n) -> Term d n
+
+    ||| term closure/suspended substitution
+    CloT  : (s : Term d from)  -> (th : Lazy (TSubst d from to)) -> Term d to
+    ||| dimension closure/suspended substitution
+    DCloT : (s : 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
+    (:@) : (f : Elim d n) -> (s : Term d n) -> Elim d n
+
+    ||| type-annotated term
+    (:#) : (s, a : Term d n) -> Elim d n
+
+    ||| term closure/suspended substitution
+    CloE  : (e : Elim d from)  -> (th : Lazy (TSubst d from to)) -> Elim d to
+    ||| dimension closure/suspended substitution
+    DCloE : (e : Elim dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Elim dto n
+
+%name Term s, t, r
+%name Elim e, f
+
+
+||| 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) -> {auto 0 p : LT i n} -> Elim d n
+BV i = B $ V i
+
+||| same as `BV` but as a term
+public export %inline
+BVT : (i : Nat) -> {auto 0 p : LT i n} -> Term d n
+BVT i = E $ BV i
+
+
+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
+
+private
+getArgs' : Elim d n -> List (Term d n) -> (Elim d n, List (Term d n))
+getArgs' (f :@ s) args = getArgs' f (s :: args)
+getArgs' f        args = (f, args)
+
+||| 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 -> (Elim d n, List (Term d n))
+getArgs e = getArgs' e []
+
+
+private %inline typeD : Doc HL
+typeD = hl Syntax "Type"
+
+private %inline arrowD : Pretty.M (Doc HL)
+arrowD = hlF Syntax $ ifUnicode "→" "->"
+
+private %inline lamD : Pretty.M (Doc HL)
+lamD = hlF Syntax $ ifUnicode "λ" "fun"
+
+private %inline annD : Pretty.M (Doc HL)
+annD = hlF Syntax $ ifUnicode "⦂" "::"
+
+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 qty qtm x s t) =
+      parensIfM Outer $ hang 2 $
+        !(prettyBinder [qty, qtm] 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 (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
+  prettyTSubst : TSubst d from to -> Pretty.M (Doc HL)
+  prettyTSubst s = prettySubstM prettyM (tnames !ask) TVar "[" "]" s
+
+  export covering
+  prettyBinder : List Qty -> Name -> Term d n -> Pretty.M (Doc HL)
+  prettyBinder pis x a =
+    pure $ parens $ hang 2 $
+      !(prettyQtyBinds pis) <//>
+      hsep [hl TVar !(prettyM x), 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       = CloE e $ assert_total $ ph . th
+  e         // Shift SZ = e
+  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         // Shift SZ = s
+  s         // th       = CloT s th
+
+
+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
+
+
+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
+
+
+||| true if an elimination has a closure or dimension closure at the top level
+public export %inline
+isCloE : Elim d n -> Bool
+isCloE (CloE  _ _) = True
+isCloE (DCloE _ _) = True
+isCloE _           = False
+
+||| 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
+isCloT : Term d n -> Bool
+isCloT (CloT  _ _) = True
+isCloT (DCloT _ _) = True
+isCloT (E e)       = isCloE e
+isCloT _           = False
+
+||| an elimination which is not a top level closure
+public export 0 NotCloElim : Nat -> Nat -> Type
+NotCloElim d n = Subset (Elim d n) $ So . not . isCloE
+
+||| a term which is not a top level closure
+public export 0 NotCloTerm : Nat -> Nat -> Type
+NotCloTerm d n = Subset (Term d n) $ So . not . isCloT
+
+
+mutual
+  export
+  pushSubstsT : Term d n -> NotCloTerm d n
+  pushSubstsT s = pushSubstsT' id id s
+
+  export
+  pushSubstsE : Elim d n -> NotCloElim d n
+  pushSubstsE e = pushSubstsE' id id e
+
+  private
+  pushSubstsT' : DSubst dfrom dto -> TSubst dto from to ->
+                 Term dfrom from -> NotCloTerm dto to
+  pushSubstsT' th ph (TYPE l) =
+    Element (TYPE l) Oh
+  pushSubstsT' th ph (Pi qty qtm x a b) =
+    Element (Pi qty qtm x (subs a th ph) (subs b th (push ph))) Oh
+  pushSubstsT' th ph (Lam x t) =
+    Element (Lam x $ subs t th $ push ph) Oh
+  pushSubstsT' th ph (E e) =
+    case pushSubstsE' th ph e of Element e' prf => Element (E e') prf
+  pushSubstsT' th ph (CloT  s ps) =
+    pushSubstsT' th (comp' th ps ph) s
+  pushSubstsT' th ph (DCloT s ps) =
+    pushSubstsT' (ps . th) ph s
+
+  private
+  pushSubstsE' : DSubst dfrom dto -> TSubst dto from to ->
+                 Elim dfrom from -> NotCloElim dto to
+  pushSubstsE' th ph (F x) =
+    Element (F x) Oh
+  pushSubstsE' th ph (B i) =
+    assert_total pushSubstsE $ ph !! i
+  pushSubstsE' th ph (f :@ s) =
+    Element (subs f th ph :@ subs s th ph) Oh
+  pushSubstsE' th ph (s :# a) =
+    Element (subs s th ph :# subs a th ph) Oh
+  pushSubstsE' th ph (CloE  e ps) =
+    pushSubstsE' th (comp' th ps ph) e
+  pushSubstsE' th ph (DCloE e ps) =
+    pushSubstsE' (ps . th) ph e
+
+
+||| `(λx. t ⦂ (x: A) → B) s >>> (t ⦂ B)[x ≔ (s ⦂ A)`
+export
+betaLam1 : Alternative f => Elim d n -> f (Elim d n)
+betaLam1 ((Lam {t, _} :# Pi {a, b, _}) :@ s) =
+  pure $ (t :# b) // (s :# a ::: id)
+betaLam1 _ = empty
+
+||| `(e ⦂ A) >>> e`    [if `e` is an elim]
+export
+upsilon1 : Alternative f => Elim d n -> f (Elim d n)
+upsilon1 (E e :# _) = pure e
+upsilon1 _          = empty
+
+public export
+step : Alternative f => Elim d n -> f (Elim d n)
+step e = betaLam1 e <|> upsilon1 e
+
+public export
+step' : Elim d n -> Elim d n
+step' e = fromMaybe e $ step e
diff --git a/src/Quox/Syntax/Universe.idr b/src/Quox/Syntax/Universe.idr
new file mode 100644
index 0000000..9b3ba1e
--- /dev/null
+++ b/src/Quox/Syntax/Universe.idr
@@ -0,0 +1,28 @@
+module Quox.Syntax.Universe
+
+import Quox.Pretty
+
+import Data.Fin
+
+%default total
+
+
+||| `UAny` doesn't show up in programs, but when checking something is
+||| just some type (e.g. in a signature) it's checked against `Star UAny`
+public export
+data Universe = U Nat | UAny
+%name Universe l
+
+private Repr : Type
+Repr = (Fin 2, Nat)
+
+private %inline repr : Universe -> Repr
+repr u = case u of U i => (0, i); UAny => (1, 0)
+
+export Eq  Universe where (==) = (==) `on` repr
+export Ord Universe where compare = compare `on` repr
+
+export
+PrettyHL Universe where
+  prettyM UAny  = pure $ hl Delim "_"
+  prettyM (U l) = pure $ hl Free $ pretty l
diff --git a/src/Quox/Syntax/Var.idr b/src/Quox/Syntax/Var.idr
new file mode 100644
index 0000000..9e4ee97
--- /dev/null
+++ b/src/Quox/Syntax/Var.idr
@@ -0,0 +1,142 @@
+module Quox.Syntax.Var
+
+import Quox.Name
+
+import Data.Nat
+import Data.Maybe
+import Data.List
+import Quox.Pretty
+
+%default total
+
+
+public export
+data Var : Nat -> Type where
+  VZ : Var (S n)
+  VS : Var n -> Var (S n)
+%name Var i, j
+%builtin Natural Var
+
+public export
+(.nat) : Var n -> Nat
+(VZ).nat   = 0
+(VS i).nat = S i.nat
+%transform "Var.(.nat)" Var.(.nat) i = believe_me i
+
+public export Cast (Var n) Nat where cast n = n.nat
+
+export Eq   (Var n) where i == j = i.nat == j.nat
+export Ord  (Var n) where compare i j = compare i.nat j.nat
+export Show (Var n) where showPrec d i = showCon d "V" $ showArg i.nat
+
+
+private
+prettyIndex : Nat -> Pretty.M (Doc a)
+prettyIndex i =
+  ifUnicode (pretty $ pack $ map sup $ unpack $ show i) (":" <+> pretty i)
+ where
+  sup : Char -> Char
+  sup c = case c of
+    '0' => '⁰'; '1' => '¹'; '2' => '²'; '3' => '³'; '4' => '⁴'
+    '5' => '⁵'; '6' => '⁶'; '7' => '⁷'; '8' => '⁸'; '9' => '⁹'; _ => c
+
+||| `prettyVar hlok hlerr names i` pretty prints the de Bruijn index `i`.
+|||
+||| If it is within the bounds of `names`, then it uses the name at that index,
+||| highlighted as `hlok`. Otherwise it is just printed as a number highlighted
+||| as `hlerr`.
+export
+prettyVar' : HL -> HL -> List Name -> Nat -> Pretty.M (Doc HL)
+prettyVar' hlok hlerr names i =
+  case inBounds i names of
+       Yes _ => hlF' hlok [|prettyM (index i names) <+> prettyIndex i|]
+       No  _ => pure $ hl hlerr $ pretty i
+
+export %inline
+prettyVar : HL -> HL -> List Name -> Var n -> Pretty.M (Doc HL)
+prettyVar hlok hlerr names i = prettyVar' hlok hlerr names i.nat
+
+
+public export
+fromNatWith : (i : Nat) -> (0 p : i `LT` n) -> Var n
+fromNatWith Z     (LTESucc _) = VZ
+fromNatWith (S i) (LTESucc p) = VS $ fromNatWith i p
+%transform "Var.fromNatWith" fromNatWith i p = believe_me i
+
+public export %inline
+V : (i : Nat) -> {auto 0 p : i `LT` n} -> Var n
+V i {p} = fromNatWith i p
+
+public export %inline
+tryFromNat : Alternative f => (n : Nat) -> Nat -> f (Var n)
+tryFromNat n i =
+  case i `isLT` n of
+       Yes p => pure $ fromNatWith i p
+       No  _ => empty
+
+export
+0 toNatLT : (i : Var n) -> i.nat `LT` n
+toNatLT VZ     = LTESucc LTEZero
+toNatLT (VS i) = LTESucc $ toNatLT i
+
+export
+0 toNatInj : {i, j : Var n} -> i.nat = j.nat -> i = j
+toNatInj {i = VZ}     {j = VZ}     Refl = Refl
+toNatInj {i = VZ}     {j = (VS i)} Refl impossible
+toNatInj {i = (VS i)} {j = VZ}     Refl impossible
+toNatInj {i = (VS i)} {j = (VS j)} prf  =
+  cong VS $ toNatInj $ succInjective _ _ prf
+
+export
+0 fromToNat : (i : Var n) -> (p : i.nat `LT` n) -> fromNatWith i.nat p = i
+fromToNat VZ     (LTESucc p) = Refl
+fromToNat (VS i) (LTESucc p) = rewrite fromToNat i p in Refl
+
+export
+0 toFromNat : (i : Nat) -> (p : i `LT` n) -> (fromNatWith i p).nat = i
+toFromNat 0     (LTESucc x) = Refl
+toFromNat (S k) (LTESucc x) = cong S $ toFromNat k x
+
+
+public export
+(.int) : Var n -> Integer
+i.int = natToInteger i.nat
+%builtin NaturalToInteger Var.(.int)
+
+public export Cast (Var n) Integer where cast i = i.int
+
+
+-- not using %transform like other things because weakSpec requires the proof
+-- to be relevant. but since only `LTESucc` is ever possible that seems
+-- to be a bug?
+export
+weak : (0 p : m `LTE` n) -> Var m -> Var n
+weak p i = fromNatWith i.nat $ transitive (toNatLT i) p {rel=LTE}
+
+public export
+0 weakSpec : m `LTE` n -> Var m -> Var n
+weakSpec LTEZero     _      impossible
+weakSpec (LTESucc p) VZ     = VZ
+weakSpec (LTESucc p) (VS i) = VS $ weakSpec p i
+
+export
+0 weakSpecCorrect : (p : m `LTE` n) -> (i : Var m) -> (weakSpec p i).nat = i.nat
+weakSpecCorrect LTEZero     _      impossible
+weakSpecCorrect (LTESucc x) VZ     = Refl
+weakSpecCorrect (LTESucc x) (VS i) = cong S $ weakSpecCorrect x i
+
+export
+0 weakCorrect : (p : m `LTE` n) -> (i : Var m) -> (weak p i).nat = i.nat
+weakCorrect LTEZero     _ impossible
+weakCorrect (LTESucc p) VZ     = Refl
+weakCorrect (LTESucc p) (VS i) = cong S $ weakCorrect p i
+
+export
+0 weakIsSpec : (p : m `LTE` n) -> (i : Var m) -> weak p i = weakSpec p i
+weakIsSpec p i = toNatInj $ trans (weakCorrect p i) (sym $ weakSpecCorrect p i)
+
+
+public export
+interface FromVar f where %inline fromVar : Var n -> f n
+
+public export FromVar Var where fromVar = id