add Tighten Term etc

src/Quox/Syntax/Term.idr

@@ -7,6 +7,7 @@ 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
 
@@ -476,6 +477,48 @@ 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 (_ :# _)