From 3efff3e96d34abbd1665d3b9e6c1d4c088307229 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 27 Feb 2022 01:22:02 +0100
Subject: [PATCH] rewrite Context.(!!)

---
 src/Quox/Context.idr | 25 +++++++++++++++++--------
 1 file changed, 17 insertions(+), 8 deletions(-)

diff --git a/src/Quox/Context.idr b/src/Quox/Context.idr
index 07c2f45..3575d5b 100644
--- a/src/Quox/Context.idr
+++ b/src/Quox/Context.idr
@@ -66,19 +66,28 @@ tel1 . (tel2 :< s) = (tel1 . tel2) :< s
 
 
 public export
-getShift : CanShift tm => Context tm len -> Var len -> Shift len out -> tm out
-getShift (ctx :< t) VZ     by = t // drop1 by
-getShift (ctx :< t) (VS i) by = getShift ctx i (drop1 by)
+getShiftWith : (forall from, to. tm from -> Shift from to -> tm to) ->
+               Shift len out -> Context tm len -> Var len -> tm out
+getShiftWith shft by (ctx :< t) VZ     = t `shft` drop1 by
+getShiftWith shft by (ctx :< t) (VS i) = getShiftWith shft (drop1 by) ctx i
+
+public export %inline
+getShift : CanShift tm => Shift len out -> Context tm len -> Var len -> tm out
+getShift = getShiftWith (//)
+
+public export %inline
+getWith : (forall from, to. tm from -> Shift from to -> tm to) ->
+          Context tm len -> Var len -> tm len
+getWith shft = getShiftWith shft SZ
 
 infixl 8 !!
-public export %inline
 (!!) : CanShift tm => Context tm len -> Var len -> tm len
-ctx !! i = getShift ctx i SZ
+(!!) = getWith (//)
 
-infixl 8 !?
+infixl 8 !!!
 public export %inline
-(!?) : Context' tm len -> Var len -> tm
-ctx !? i = (ctx !! i) @{Const}
+(!!!) : Context' tm len -> Var len -> tm
+(!!!) = getWith const
 
 
 ||| a triangle of bindings. each type binding in a context counts the ues of