From 362c9354cf45f5f845f7df474aacc9f2b81e8cb9 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 27 Feb 2022 02:17:51 +0100
Subject: [PATCH] add Var.tighten*

---
 src/Quox/Syntax/Var.idr | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/src/Quox/Syntax/Var.idr b/src/Quox/Syntax/Var.idr
index a6290c3..07834d5 100644
--- a/src/Quox/Syntax/Var.idr
+++ b/src/Quox/Syntax/Var.idr
@@ -263,3 +263,24 @@ decEqFromBool i j =
 %transform "Var.decEq" varDecEq = decEqFromBool
 
 public export %inline DecEq (Var n) where decEq = varDecEq
+
+parameters {auto _ : Alternative f}
+  export
+  tighten : OPE m n -> Var n -> f (Var m)
+  tighten Id       i      = pure i
+  tighten (Drop q) VZ     = empty
+  tighten (Drop q) (VS i) = tighten q i
+  tighten (Keep q) VZ     = pure VZ
+  tighten (Keep q) (VS i) = VS <$> tighten q i
+
+  export
+  tightenInner : {n : Nat} -> m `LTE` n -> Var n -> f (Var m)
+  tightenInner = tighten . dropInner
+
+  export
+  tightenN : (m : Nat) -> Var (m + n) -> f (Var n)
+  tightenN m = tighten $ dropInnerN m
+
+  export
+  tighten1 : Var (S n) -> f (Var n)
+  tighten1 = tightenN 1