From 67d8c59cd18886cf62ed636a5cec18264cb8d0ae Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 11 Apr 2022 23:36:01 +0200
Subject: [PATCH] make tighten into an interface

---
 src/Quox/OPE.idr        | 18 ++++++++++++++++++
 src/Quox/Syntax/Var.idr | 17 ++---------------
 2 files changed, 20 insertions(+), 15 deletions(-)

diff --git a/src/Quox/OPE.idr b/src/Quox/OPE.idr
index c57cac0..9b6de26 100644
--- a/src/Quox/OPE.idr
+++ b/src/Quox/OPE.idr
@@ -52,6 +52,24 @@ dropInnerN 0     = Id
 dropInnerN (S m) = Drop $ dropInnerN m
 
 
+public export
+interface Tighten t where
+  tighten : Alternative f => OPE m n -> t n -> f (t m)
+
+parameters {auto _ : Tighten t} {auto _ : Alternative f}
+  export
+  tightenInner : {n : Nat} -> m `LTE` n -> t n -> f (t m)
+  tightenInner = tighten . dropInner
+
+  export
+  tightenN : (m : Nat) -> t (m + n) -> f (t n)
+  tightenN m = tighten $ dropInnerN m
+
+  export
+  tighten1 : t (S n) -> f (t n)
+  tighten1 = tightenN 1
+
+
 
 -- [todo] can this be done with fancy nats too?
 -- with bitmasks sure but that might not be worth the effort
diff --git a/src/Quox/Syntax/Var.idr b/src/Quox/Syntax/Var.idr
index 07834d5..a937fec 100644
--- a/src/Quox/Syntax/Var.idr
+++ b/src/Quox/Syntax/Var.idr
@@ -264,23 +264,10 @@ decEqFromBool i j =
 
 public export %inline DecEq (Var n) where decEq = varDecEq
 
-parameters {auto _ : Alternative f}
-  export
-  tighten : OPE m n -> Var n -> f (Var m)
+export
+Tighten Var where
   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