Make everything relevant.

Too few proofs were relevant. Now they are.

1 files changed, 90 insertions, 0 deletions

diff --git a/src/Inky/Data/SnocList/Var.idr b/src/Inky/Data/SnocList/Var.idr
new file mode 100644
index 0000000..cc7c088
--- /dev/null
+++ b/src/Inky/Data/SnocList/Var.idr
@@ -0,0 +1,90 @@
+module Inky.Data.SnocList.Var
+
+import public Inky.Data.SnocList.Elem
+
+import Data.Singleton
+import Inky.Data.SnocList
+import Inky.Decidable
+
+export
+prefix 2 %%
+
+public export
+record Var (sx : SnocList a) where
+  constructor (%%)
+  0 name : a
+  {auto pos : Elem name sx}
+
+%name Var i, j, k
+
+public export
+toVar : Elem x sx -> Var sx
+toVar pos = (%%) x {pos}
+
+public export
+ThereVar : Var sx -> Var (sx :< x)
+ThereVar i = toVar (There i.pos)
+
+export
+Show (Var sx) where
+  show i = show (elemToNat i.pos)
+
+-- Basic Properties ---------------------------------------------------------
+
+export
+toVarCong : {0 i : Elem x sx} -> {0 j : Elem y sx} -> i = j -> toVar i = toVar j
+toVarCong Refl = Refl
+
+export
+posCong : {0 i, j : Var sx} -> i = j -> i.pos ~=~ j.pos
+posCong Refl = Refl
+
+export
+toVarInjective : {i : Elem x sx} -> {j : Elem y sx} -> (0 _ : toVar i = toVar j) -> i = j
+toVarInjective prf = toNatInjective $ toNatCong $ posCong prf
+
+export
+posInjective : {i : Var sx} -> {j : Var sx} -> (0 _ : i.pos ~=~ j.pos) -> i = j
+posInjective {i = %% x} {j = %% y} prf = irrelevantEq $ toVarCong prf
+
+-- Decidable Equality ----------------------------------------------------------
+
+public export
+DecEq' (Var {a} sx) where
+  does i j = (decEq i.pos j.pos).does
+  reason i j =
+    mapWhen (\prf => irrelevantEq $ posInjective prf) posCong $
+    (decEq i.pos j.pos).reason
+
+-- Weakening -------------------------------------------------------------------
+
+public export
+wknL : (len : LengthOf sy) => Var sx -> Var (sx ++ sy)
+wknL i = toVar $ wknL i.pos len
+
+public export
+wknR : Var sx -> Var (sy ++ sx)
+wknR i = toVar $ wknR i.pos
+
+public export
+split : {auto len : LengthOf sy} -> Var (sx ++ sy) -> Either (Var sx) (Var sy)
+split i = bimap toVar toVar $ split len i.pos
+
+public export
+lift1 :
+  (Var sx -> Var sy) ->
+  Var (sx :< x) -> Var (sy :< y)
+lift1 f ((%%) x {pos = Here}) = %% y
+lift1 f ((%%) name {pos = There i}) = ThereVar (f $ %% name)
+
+-- Names -----------------------------------------------------------------------
+
+export
+nameOf : {sx : SnocList a} -> (i : Var sx) -> Singleton i.name
+nameOf i = nameOf i.pos
+
+-- Search ----------------------------------------------------------------------
+
+export
+lookup : DecEq' a => (x : a) -> (sx : SnocList a) -> Maybe (Var sx)
+lookup x sx = toVar <$> lookup x sx