From 9e702dd03d9ef0d2eefcddc0dc22aba67eee7a40 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 5 Jun 2023 16:40:55 +0200
Subject: [PATCH] switch syntax to codb

---
 lib/Quox/Syntax/Term/Base.idr | 619 +++++++++++++++-------------------
 1 file changed, 272 insertions(+), 347 deletions(-)

diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr
index 5682c73..0ff7b3b 100644
--- a/lib/Quox/Syntax/Term/Base.idr
+++ b/lib/Quox/Syntax/Term/Base.idr
@@ -1,5 +1,6 @@
 module Quox.Syntax.Term.Base
 
+import public Quox.Thin
 import public Quox.Syntax.Var
 import public Quox.Syntax.Shift
 import public Quox.Syntax.Subst
@@ -18,9 +19,6 @@ import Data.Maybe
 import Data.Nat
 import public Data.So
 import Data.String
-import public Data.SortedMap
-import public Data.SortedMap.Dependent
-import public Data.SortedSet
 import Derive.Prelude
 
 %default total
@@ -46,345 +44,301 @@ TagVal : Type
 TagVal = String
 
 
+||| type-checkable terms, which consists of types and constructor forms.
+|||
+||| first argument `d` is dimension scope size; second `n` is term scope size
 public export
-data ScopedBody : Nat -> (Nat -> Type) -> Nat -> Type where
-  Y : (body : f (s + n)) -> ScopedBody s f n
-  N : (body : f n)       -> ScopedBody s f n
-%name ScopedBody body
+data Term : (d, n : Nat) -> Type
+%name Term s, t, r
 
-export %inline %hint
-EqScopedBody : (forall n. Eq (f n)) => Eq (ScopedBody s f n)
-EqScopedBody = deriveEq
-
-export %inline %hint
-ShowScopedBody : (forall n. Show (f n)) => Show (ScopedBody s f n)
-ShowScopedBody = deriveShow
-
-||| a scoped term with names
+||| inferrable terms, which consists of elimination forms like application and
+||| `case` (as well as other terms with an annotation)
+|||
+||| first argument `d` is dimension scope size; second `n` is term scope size
 public export
-record Scoped (s : Nat) (f : Nat -> Type) (n : Nat) where
-  constructor S
-  names : BContext s
-  body  : ScopedBody s f n
-%name Scoped body
-
-export %inline
-(forall n. Eq (f n)) => Eq (Scoped s f n) where
-  s == t = s.body == t.body
-
-export %inline %hint
-ShowScoped : (forall n. Show (f n)) => Show (Scoped s f n)
-ShowScoped = deriveShow
+data Elim : (d, n : Nat) -> Type
+%name Elim e, f
 
 
-infixl 8 :#
-infixl 9 :@, :%
-mutual
-  public export
-  TSubst : TSubstLike
-  TSubst d = Subst $ \n => Elim d n
+public export
+ScopeTermN : Nat -> TermLike
+ScopeTermN s d n = ScopedN s (\n => Term d n) 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) -> (loc : Loc) -> Term d n
+public export
+DScopeTermN : Nat -> TermLike
+DScopeTermN s d n = ScopedN s (\d => Term d n) d
 
-    ||| function type
-    Pi  : (qty : Qty) -> (arg : Term d n) ->
-          (res : ScopeTerm d n) -> (loc : Loc) -> Term d n
-    ||| function term
-    Lam : (body : ScopeTerm d n) -> (loc : Loc) -> Term d n
+public export
+ScopeTerm : TermLike
+ScopeTerm = ScopeTermN 1
 
-    ||| pair type
-    Sig : (fst : Term d n) -> (snd : ScopeTerm d n) -> (loc : Loc) -> Term d n
-    ||| pair value
-    Pair : (fst, snd : Term d n) -> (loc : Loc) -> Term d n
-
-    ||| enumeration type
-    Enum : (cases : SortedSet TagVal) -> (loc : Loc) -> Term d n
-    ||| enumeration value
-    Tag : (tag : TagVal) -> (loc : Loc) -> Term d n
-
-    ||| equality type
-    Eq : (ty : DScopeTerm d n) -> (l, r : Term d n) -> (loc : Loc) -> Term d n
-    ||| equality term
-    DLam : (body : DScopeTerm d n) -> (loc : Loc) -> Term d n
-
-    ||| natural numbers (temporary until 𝐖 gets added)
-    Nat  : (loc : Loc) -> Term d n
-    -- [todo] can these be elims?
-    Zero : (loc : Loc) -> Term d n
-    Succ : (p : Term d n) -> (loc : Loc) -> Term d n
-
-    ||| "box" (package a value up with a certain quantity)
-    BOX : (qty : Qty) -> (ty : Term d n) -> (loc : Loc) -> Term d n
-    Box : (val : Term d n) -> (loc : Loc) -> Term d n
-
-    ||| elimination
-    E : (e : Elim d n) -> Term d n
-
-    ||| term closure/suspended substitution
-    CloT  : WithSubst (Term d) (Elim d) n -> Term d n
-    ||| dimension closure/suspended substitution
-    DCloT : WithSubst (\d => Term d n) Dim d -> Term d n
-  %name Term s, t, r
-
-  ||| first argument `d` is dimension scope size, second `n` is term scope size
-  public export
-  data Elim : (d, n : Nat) -> Type where
-    ||| free variable, possibly with a displacement (see @crude, or @mugen for a
-    ||| more abstract and formalised take)
-    |||
-    ||| e.g. if f : ★₀ → ★₁, then f¹ : ★₁ → ★₂
-    F : (x : Name) -> (u : Universe) -> (loc : Loc) -> Elim d n
-    ||| bound variable
-    B : (i : Var n) -> (loc : Loc) -> Elim d n
-
-    ||| term application
-    App : (fun : Elim d n) -> (arg : Term d n) -> (loc : Loc) -> Elim d n
-
-    ||| pair destruction
-    |||
-    ||| `CasePair 𝜋 𝑒 ([𝑟], 𝐴) ([𝑥, 𝑦], 𝑡)` is
-    ||| `𝐜𝐚𝐬𝐞 𝜋 · 𝑒 𝐫𝐞𝐭𝐮𝐫𝐧 𝑟 ⇒ 𝐴 𝐨𝐟 { (𝑥, 𝑦) ⇒ 𝑡 }`
-    CasePair : (qty : Qty) -> (pair : Elim d n) ->
-               (ret : ScopeTerm d n) ->
-               (body : ScopeTermN 2 d n) ->
-               (loc : Loc) ->
-               Elim d n
-
-    ||| enum matching
-    CaseEnum : (qty : Qty) -> (tag : Elim d n) ->
-               (ret : ScopeTerm d n) ->
-               (arms : CaseEnumArms d n) ->
-               (loc : Loc) ->
-               Elim d n
-
-    ||| nat matching
-    CaseNat : (qty, qtyIH : Qty) -> (nat : Elim d n) ->
-              (ret : ScopeTerm d n) ->
-              (zero : Term d n) ->
-              (succ : ScopeTermN 2 d n) ->
-              (loc : Loc) ->
-              Elim d n
-
-    ||| unboxing
-    CaseBox : (qty : Qty) -> (box : Elim d n) ->
-              (ret : ScopeTerm d n) ->
-              (body : ScopeTerm d n) ->
-              (loc : Loc) ->
-              Elim d n
-
-    ||| dim application
-    DApp : (fun : Elim d n) -> (arg : Dim d) -> (loc : Loc) -> Elim d n
-
-    ||| type-annotated term
-    Ann : (tm, ty : Term d n) -> (loc : Loc) -> Elim d n
-
-    ||| coerce a value along a type equality, or show its coherence
-    ||| [@xtt; §2.1.1]
-    Coe : (ty : DScopeTerm d n) -> (p, q : Dim d) ->
-          (val : Term d n) -> (loc : Loc) -> Elim d n
-
-    ||| "generalised composition" [@xtt; §2.1.2]
-    Comp : (ty : Term d n) -> (p, q : Dim d) ->
-           (val : Term d n) -> (r : Dim d) ->
-           (zero, one : DScopeTerm d n) -> (loc : Loc) -> Elim d n
-
-    ||| match on types. needed for b.s. of coercions [@xtt; §2.2]
-    TypeCase : (ty : Elim d n) -> (ret : Term d n) ->
-               (arms : TypeCaseArms d n) -> (def : Term d n) ->
-               (loc : Loc) ->
-               Elim d n
-
-    ||| term closure/suspended substitution
-    CloE  : WithSubst (Elim d) (Elim d) n -> Elim d n
-    ||| dimension closure/suspended substitution
-    DCloE : WithSubst (\d => Elim d n) Dim d -> Elim d n
-  %name Elim e, f
-
-  public export
-  CaseEnumArms : TermLike
-  CaseEnumArms d n = SortedMap TagVal (Term d n)
-
-  public export
-  TypeCaseArms : TermLike
-  TypeCaseArms d n = SortedDMap TyConKind (\k => TypeCaseArmBody k d n)
-
-  public export
-  TypeCaseArm : TermLike
-  TypeCaseArm d n = (k ** TypeCaseArmBody k d n)
-
-  public export
-  TypeCaseArmBody : TyConKind -> TermLike
-  TypeCaseArmBody k = ScopeTermN (arity k)
+public export
+DScopeTerm : TermLike
+DScopeTerm = DScopeTermN 1
 
 
-  public export
-  ScopeTermN, DScopeTermN : Nat -> TermLike
-  ScopeTermN  s d n = Scoped s (Term d) n
-  DScopeTermN s d n = Scoped s (\d => Term d n) d
+public export
+TermT : TermLike
+TermT = Thinned2 (\d, n => Term d n)
 
-  public export
-  ScopeTerm, DScopeTerm : TermLike
-  ScopeTerm  = ScopeTermN 1
-  DScopeTerm = DScopeTermN 1
+public export
+ElimT : TermLike
+ElimT = Thinned2 (\d, n => Elim d n)
 
-mutual
-  export %hint
-  EqTerm : Eq (Term d n)
-  EqTerm = assert_total {a = Eq (Term d n)} deriveEq
 
-  export %hint
-  EqElim : Eq (Elim d n)
-  EqElim = assert_total {a = Eq (Elim d n)} deriveEq
+public export
+DimArg : TermLike
+DimArg d n = Dim d
 
-mutual
-  export %hint
-  ShowTerm : Show (Term d n)
-  ShowTerm = assert_total {a = Show (Term d n)} deriveShow
 
-  export %hint
-  ShowElim : Show (Elim d n)
-  ShowElim = assert_total {a = Show (Elim d n)} deriveShow
+data Term where
+  ||| type of types
+  TYPE : (l : Universe) -> (loc : Loc) -> Term 0 0
 
-||| scope which ignores all its binders
-public export %inline
-SN : {s : Nat} -> f n -> Scoped s f n
-SN = S (replicate s $ BN Unused noLoc) . N
+  ||| function type
+  Pi : Qty -> Subterms [Term, ScopeTerm] d n -> Loc -> Term d n
+  ||| function value
+  Lam : ScopeTerm d n -> Loc -> Term d n
 
-||| scope which uses its binders
-public export %inline
-SY : BContext s -> f (s + n) -> Scoped s f n
-SY ns = S ns . Y
+  ||| pair type
+  Sig : Subterms [Term, ScopeTerm] d n -> Loc -> Term d n
+  ||| pair value
+  Pair : Subterms [Term, Term] d n -> Loc -> Term d n
 
-public export %inline
-name : Scoped 1 f n -> BindName
-name (S [< x] _) = x
+  ||| enum type
+  Enum : List TagVal -> Loc -> Term 0 0
+  ||| enum value
+  Tag : TagVal -> Loc -> Term 0 0
 
-public export %inline
-(.name) : Scoped 1 f n -> BindName
-s.name = name s
+  ||| equality type
+  Eq : Subterms [DScopeTerm, Term, Term] d n -> Loc -> Term d n
+  ||| equality value
+  DLam : DScopeTerm d n -> Loc -> Term d n
 
-||| more convenient Pi
-public export %inline
-PiY : (qty : Qty) -> (x : BindName) ->
-      (arg : Term d n) -> (res : Term d (S n)) -> (loc : Loc) -> Term d n
-PiY {qty, x, arg, res, loc} = Pi {qty, arg, res = SY [< x] res, loc}
+  ||| natural numbers (temporary until 𝐖 gets added)
+  Nat  : Loc -> Term 0 0
+  Zero : Loc -> Term 0 0
+  Succ : Term d n -> Loc -> Term 0 0
 
-||| more convenient Lam
-public export %inline
-LamY : (x : BindName) -> (body : Term d (S n)) -> (loc : Loc) -> Term d n
-LamY {x, body, loc} = Lam {body = SY [< x] body, loc}
+  ||| package a value with a quantity
+  ||| e.g. a value of [ω. A], when unpacked, can be used ω times,
+  ||| even if the box itself is linear
+  BOX : Qty -> Term d n -> Loc -> Term d n
+  Box : Term d n -> Loc -> Term d n
 
-public export %inline
-LamN : (body : Term d n) -> (loc : Loc) -> Term d n
-LamN {body, loc} = Lam {body = SN body, loc}
+  E : Elim d n -> Term d n
 
-||| non dependent function type
-public export %inline
-Arr : (qty : Qty) -> (arg, res : Term d n) -> (loc : Loc) -> Term d n
-Arr {qty, arg, res, loc} = Pi {qty, arg, res = SN res, loc}
+  ||| term closure/suspended substitution
+  CloT  : WithSubst (Term d) (Elim d) n -> Term d n
+  ||| dimension closure/suspended substitution
+  DCloT : WithSubst (\d => Term d n) Dim d -> Term d n
 
-||| more convenient Sig
-public export %inline
-SigY : (x : BindName) -> (fst : Term d n) ->
-       (snd : Term d (S n)) -> (loc : Loc) -> Term d n
-SigY {x, fst, snd, loc} = Sig {fst, snd = SY [< x] snd, loc}
+||| first argument `d` is dimension scope size, second `n` is term scope size
+public export
+data Elim where
+  ||| free variable, possibly with a displacement (see @crude, or @mugen for a
+  ||| more abstract and formalised take)
+  |||
+  ||| e.g. if f : ★₀ → ★₁, then f¹ : ★₁ → ★₂
+  F : Name -> Universe -> Loc -> Elim 0 0
+  ||| bound variable
+  B : Loc -> Elim 0 1
 
-||| non dependent pair type
-public export %inline
-And : (fst, snd : Term d n) -> (loc : Loc) -> Term d n
-And {fst, snd, loc} = Sig {fst, snd = SN snd, loc}
+  ||| term application
+  App : Subterms [Elim, Term] d n -> Loc -> Elim d n
 
-||| more convenient Eq
-public export %inline
-EqY : (i : BindName) -> (ty : Term (S d) n) ->
-      (l, r : Term d n) -> (loc : Loc) -> Term d n
-EqY {i, ty, l, r, loc} = Eq {ty = SY [< i] ty, l, r, loc}
+  ||| pair match
+  ||| - the subterms are, in order: [head, return type, body]
+  ||| - the quantity is that of the head, and since pairs only have one
+  |||   constructor, can be 0
+  CasePair : Qty -> Subterms [Elim, ScopeTerm, ScopeTermN 2] d n ->
+             Loc -> Elim d n
 
-||| more convenient DLam
-public export %inline
-DLamY : (i : BindName) -> (body : Term (S d) n) -> (loc : Loc) -> Term d n
-DLamY {i, body, loc} = DLam {body = SY [< i] body, loc}
+  ||| enum match
+  CaseEnum : Qty -> (arms : List TagVal) ->
+             Subterms (Elim :: ScopeTerm :: (Term <$ arms)) d n ->
+             Loc -> Elim d n
 
-public export %inline
-DLamN : (body : Term d n) -> (loc : Loc) -> Term d n
-DLamN {body, loc} = DLam {body = SN body, loc}
+  ||| nat match
+  CaseNat : Qty -> Qty ->
+            Subterms [Elim, ScopeTerm, Term, ScopeTermN 2] d n ->
+            Loc -> Elim d n
+
+  ||| box match
+  CaseBox : Qty -> Subterms [Elim, ScopeTerm, ScopeTerm] d n -> Loc -> Elim d n
+
+  ||| dim application
+  DApp : Subterms [Elim, DimArg] d n -> Loc -> Elim d n
+
+  ||| type-annotated term
+  Ann : Subterms [Term, Term] d n -> Loc -> Elim d n
+
+  ||| coerce a value along a type equality, or show its coherence
+  ||| [@xtt; §2.1.1]
+  Coe : Subterms [DScopeTerm, DimArg, DimArg, Term] d n ->
+        Loc -> Elim d n
+
+  ||| "generalised composition" [@xtt; §2.1.2]
+  Comp : Subterms [Term, DimArg, DimArg, Term,
+                   DimArg, DScopeTerm, DScopeTerm] d n ->
+         Loc -> Elim d n
+
+  ||| match on types. needed for b.s. of coercions [@xtt; §2.2]
+  TypeCase : Subterms [Elim, Term,   -- head, type
+                       Term,         -- ★
+                       ScopeTermN 2, -- pi
+                       ScopeTermN 2, -- sig
+                       Term,         -- enum
+                       ScopeTermN 5, -- eq
+                       Term,         -- nat
+                       ScopeTerm     -- box
+                      ] d n -> Loc -> Elim d n
+
+  ||| term closure/suspended substitution
+  CloE  : WithSubst (Elim d) (Elim d) n -> Elim d n
+  ||| dimension closure/suspended substitution
+  DCloE : WithSubst (\d => Elim d n) Dim d -> Elim d n
+
+
+-- this kills the idris ☹
+-- export %hint
+-- EqTerm : Eq (Term d n)
+
+-- export %hint
+-- EqElim : Eq (Elim d n)
+
+-- EqTerm = deriveEq
+-- EqElim = deriveEq
+
+
+-- mutual
+--   export %hint
+--   ShowTerm : Show (Term d n)
+--   ShowTerm = assert_total {a = Show (Term d n)} deriveShow
+
+--   export %hint
+--   ShowElim : Show (Elim d n)
+--   ShowElim = assert_total {a = Show (Elim d n)} deriveShow
+
+-- ||| scope which ignores all its binders
+-- public export %inline
+-- SN : {s : Nat} -> f n -> Scoped s f n
+-- SN = S (replicate s $ BN Unused noLoc) . N
+
+-- ||| scope which uses its binders
+-- public export %inline
+-- SY : BContext s -> f (s + n) -> Scoped s f n
+-- SY ns = S ns . Y
+
+-- public export %inline
+-- name : Scoped 1 f n -> BindName
+-- name (S [< x] _) = x
+
+-- public export %inline
+-- (.name) : Scoped 1 f n -> BindName
+-- s.name = name s
+
+-- ||| more convenient Pi
+-- public export %inline
+-- PiY : (qty : Qty) -> (x : BindName) ->
+--       (arg : Term d n) -> (res : Term d (S n)) -> (loc : Loc) -> Term d n
+-- PiY {qty, x, arg, res, loc} = Pi {qty, arg, res = SY [< x] res, loc}
+
+-- ||| more convenient Lam
+-- public export %inline
+-- LamY : (x : BindName) -> (body : Term d (S n)) -> (loc : Loc) -> Term d n
+-- LamY {x, body, loc} = Lam {body = SY [< x] body, loc}
+
+-- public export %inline
+-- LamN : (body : Term d n) -> (loc : Loc) -> Term d n
+-- LamN {body, loc} = Lam {body = SN body, loc}
+
+-- ||| non dependent function type
+-- public export %inline
+-- Arr : (qty : Qty) -> (arg, res : Term d n) -> (loc : Loc) -> Term d n
+-- Arr {qty, arg, res, loc} = Pi {qty, arg, res = SN res, loc}
+
+-- ||| more convenient Sig
+-- public export %inline
+-- SigY : (x : BindName) -> (fst : Term d n) ->
+--        (snd : Term d (S n)) -> (loc : Loc) -> Term d n
+-- SigY {x, fst, snd, loc} = Sig {fst, snd = SY [< x] snd, loc}
+
+-- ||| non dependent pair type
+-- public export %inline
+-- And : (fst, snd : Term d n) -> (loc : Loc) -> Term d n
+-- And {fst, snd, loc} = Sig {fst, snd = SN snd, loc}
+
+-- ||| more convenient Eq
+-- public export %inline
+-- EqY : (i : BindName) -> (ty : Term (S d) n) ->
+--       (l, r : Term d n) -> (loc : Loc) -> Term d n
+-- EqY {i, ty, l, r, loc} = Eq {ty = SY [< i] ty, l, r, loc}
+
+-- ||| more convenient DLam
+-- public export %inline
+-- DLamY : (i : BindName) -> (body : Term (S d) n) -> (loc : Loc) -> Term d n
+-- DLamY {i, body, loc} = DLam {body = SY [< i] body, loc}
+
+-- public export %inline
+-- DLamN : (body : Term d n) -> (loc : Loc) -> Term d n
+-- DLamN {body, loc} = DLam {body = SN body, loc}
+
+-- ||| non dependent equality type
+-- public export %inline
+-- Eq0 : (ty, l, r : Term d n) -> (loc : Loc) -> Term d n
+-- Eq0 {ty, l, r, loc} = Eq {ty = SN ty, l, r, loc}
 
-||| non dependent equality type
-public export %inline
-Eq0 : (ty, l, r : Term d n) -> (loc : Loc) -> Term d n
-Eq0 {ty, l, r, loc} = Eq {ty = SN ty, l, r, loc}
 
 ||| same as `F` but as a term
 public export %inline
-FT : Name -> Universe -> Loc -> Term d n
+FT : Name -> Universe -> Loc -> Term 0 0
 FT x u loc = E $ F x u loc
 
 ||| 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) => (loc : Loc) -> Elim d n
-BV i loc = B (V i) loc
+BV : (i : Fin n) -> (loc : Loc) -> ElimT d n
+BV i loc = Th2 zero (one' i) $ B loc
 
 ||| same as `BV` but as a term
 public export %inline
-BVT : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Term d n
-BVT i loc = E $ BV i loc
+BVT : (i : Fin n) -> (loc : Loc) -> TermT d n
+BVT i loc = Th2 zero (one' i) $ E $ B loc
 
 public export
-makeNat : Nat -> Loc -> Term d n
-makeNat 0 loc = Zero loc
+makeNat : Nat -> Loc -> Term 0 0
+makeNat 0     loc = Zero loc
 makeNat (S k) loc = Succ (makeNat k loc) loc
 
-public export %inline
-enum : List TagVal -> Loc -> Term d n
-enum ts loc = Enum (SortedSet.fromList ts) loc
-
-public export %inline
-typeCase : Elim d n -> Term d n ->
-           List (TypeCaseArm d n) -> Term d n -> Loc -> Elim d n
-typeCase ty ret arms def loc = TypeCase ty ret (fromList arms) def loc
-
-public export %inline
-typeCase1Y : Elim d n -> Term d n ->
-             (k : TyConKind) -> BContext (arity k) -> Term d (arity k + n) ->
-             (loc : Loc) ->
-             {default (Nat loc) def : Term d n} ->
-             Elim d n
-typeCase1Y ty ret k ns body loc = typeCase ty ret [(k ** SY ns body)] def loc
-
 
 export
 Located (Elim d n) where
-  (F _ _ loc).loc               = loc
-  (B _ loc).loc                 = loc
-  (App _ _ loc).loc             = loc
-  (CasePair _ _ _ _ loc).loc    = loc
-  (CaseEnum _ _ _ _ loc).loc    = loc
-  (CaseNat _ _ _ _ _ _ loc).loc = loc
-  (CaseBox _ _ _ _ loc).loc     = loc
-  (DApp _ _ loc).loc            = loc
-  (Ann _ _ loc).loc             = loc
-  (Coe _ _ _ _ loc).loc         = loc
-  (Comp _ _ _ _ _ _ _ loc).loc  = loc
-  (TypeCase _ _ _ _ loc).loc    = loc
-  (CloE (Sub e _)).loc          = e.loc
-  (DCloE (Sub e _)).loc         = e.loc
+  (F _ _ loc).loc          = loc
+  (B loc).loc              = loc
+  (App _ loc).loc          = loc
+  (CasePair _ _ loc).loc   = loc
+  (CaseEnum _ _ _ loc).loc = loc
+  (CaseNat _ _ _ loc).loc  = loc
+  (CaseBox _ _ loc).loc    = loc
+  (DApp _ loc).loc         = loc
+  (Ann _ loc).loc          = loc
+  (Coe _ loc).loc          = loc
+  (Comp _ loc).loc         = loc
+  (TypeCase _ loc).loc     = loc
+  (CloE (Sub e _)).loc     = e.loc
+  (DCloE (Sub e _)).loc    = e.loc
 
 export
 Located (Term d n) where
   (TYPE _ loc).loc      = loc
-  (Pi _ _ _ loc).loc    = loc
+  (Pi _ _ loc).loc      = loc
   (Lam _ loc).loc       = loc
-  (Sig _ _ loc).loc     = loc
-  (Pair _ _ loc).loc    = loc
+  (Sig _ loc).loc       = loc
+  (Pair _ loc).loc      = loc
   (Enum _ loc).loc      = loc
   (Tag _ loc).loc       = loc
-  (Eq _ _ _ loc).loc    = loc
+  (Eq _ loc).loc        = loc
   (DLam _ loc).loc      = loc
   (Nat loc).loc         = loc
   (Zero loc).loc        = loc
@@ -395,69 +349,40 @@ Located (Term d n) where
   (CloT (Sub t _)).loc  = t.loc
   (DCloT (Sub t _)).loc = t.loc
 
-export
-Located1 f => Located (ScopedBody s f n) where
-  (Y t).loc = t.loc
-  (N t).loc = t.loc
-
-export
-Located1 f => Located (Scoped s f n) where
-  t.loc = t.body.loc
-
 
 export
 Relocatable (Elim d n) where
-  setLoc loc (F x u _) = F x u loc
-  setLoc loc (B i _) = B i loc
-  setLoc loc (App fun arg _) = App fun arg loc
-  setLoc loc (CasePair qty pair ret body _) =
-    CasePair qty pair ret body loc
-  setLoc loc (CaseEnum qty tag ret arms _) =
-    CaseEnum qty tag ret arms loc
-  setLoc loc (CaseNat qty qtyIH nat ret zero succ _) =
-    CaseNat qty qtyIH nat ret zero succ loc
-  setLoc loc (CaseBox qty box ret body _) =
-    CaseBox qty box ret body loc
-  setLoc loc (DApp fun arg _) =
-    DApp fun arg loc
-  setLoc loc (Ann tm ty _) =
-    Ann tm ty loc
-  setLoc loc (Coe ty p q val _) =
-    Coe ty p q val loc
-  setLoc loc (Comp ty p q val r zero one _) =
-    Comp ty p q val r zero one loc
-  setLoc loc (TypeCase ty ret arms def _) =
-    TypeCase ty ret arms def loc
-  setLoc loc (CloE (Sub term subst)) =
-    CloE $ Sub (setLoc loc term) subst
-  setLoc loc (DCloE (Sub term subst)) =
-    DCloE $ Sub (setLoc loc term) subst
+  setLoc loc (F x u _)                = F x u loc
+  setLoc loc (B _)                    = B loc
+  setLoc loc (App ts _)               = App ts loc
+  setLoc loc (CasePair qty ts _)      = CasePair qty ts loc
+  setLoc loc (CaseEnum qty arms ts _) = CaseEnum qty arms ts loc
+  setLoc loc (CaseNat qty qtyIH ts _) = CaseNat qty qtyIH ts loc
+  setLoc loc (CaseBox qty ts _)       = CaseBox qty ts loc
+  setLoc loc (DApp ts _)              = DApp ts loc
+  setLoc loc (Ann ts _)               = Ann ts loc
+  setLoc loc (Coe ts _)               = Coe ts loc
+  setLoc loc (Comp ts _)              = Comp ts loc
+  setLoc loc (TypeCase ts _)          = TypeCase ts loc
+  setLoc loc (CloE (Sub term subst))  = CloE $ Sub (setLoc loc term) subst
+  setLoc loc (DCloE (Sub term subst)) = DCloE $ Sub (setLoc loc term) subst
 
 export
 Relocatable (Term d n) where
-  setLoc loc (TYPE l _) = TYPE l loc
-  setLoc loc (Pi qty arg res _) = Pi qty arg res loc
-  setLoc loc (Lam body _) = Lam body loc
-  setLoc loc (Sig fst snd _) = Sig fst snd loc
-  setLoc loc (Pair fst snd _) = Pair fst snd loc
-  setLoc loc (Enum cases _) = Enum cases loc
-  setLoc loc (Tag tag _) = Tag tag loc
-  setLoc loc (Eq ty l r _) = Eq ty l r loc
-  setLoc loc (DLam body _) = DLam body loc
-  setLoc loc (Nat _) = Nat loc
-  setLoc loc (Zero _) = Zero loc
-  setLoc loc (Succ p _) = Succ p loc
-  setLoc loc (BOX qty ty _) = BOX qty ty loc
-  setLoc loc (Box val _) = Box val loc
-  setLoc loc (E e) = E $ setLoc loc e
-  setLoc loc (CloT (Sub term subst)) = CloT $ Sub (setLoc loc term) subst
+  setLoc loc (TYPE l _)               = TYPE l loc
+  setLoc loc (Pi qty ts _)            = Pi qty ts loc
+  setLoc loc (Lam body _)             = Lam body loc
+  setLoc loc (Sig ts _)               = Sig ts loc
+  setLoc loc (Pair ts _)              = Pair ts loc
+  setLoc loc (Enum cases _)           = Enum cases loc
+  setLoc loc (Tag tag _)              = Tag tag loc
+  setLoc loc (Eq ts _)                = Eq ts loc
+  setLoc loc (DLam body _)            = DLam body loc
+  setLoc loc (Nat _)                  = Nat loc
+  setLoc loc (Zero _)                 = Zero loc
+  setLoc loc (Succ p _)               = Succ p loc
+  setLoc loc (BOX qty ty _)           = BOX qty ty loc
+  setLoc loc (Box val _)              = Box val loc
+  setLoc loc (E e)                    = E $ setLoc loc e
+  setLoc loc (CloT (Sub term subst))  = CloT $ Sub (setLoc loc term) subst
   setLoc loc (DCloT (Sub term subst)) = DCloT $ Sub (setLoc loc term) subst
-
-export
-Relocatable1 f => Relocatable (ScopedBody s f n) where
-  setLoc loc (Y body) = Y $ setLoc loc body
-  setLoc loc (N body) = N $ setLoc loc body
-
-export
-Relocatable1 f => Relocatable (Scoped s f n) where
-  setLoc loc (S names body) = S (setLoc loc <$> names) (setLoc loc body)