Improve runtime behaviour of variables.

Operations like `weakl`, `weakr` and `copair` now treat variables as
integers at runtime, instead of treating them as unary naturals.

Reimplent `lift` in terms of `copair`.

4 files changed, 88 insertions, 51 deletions

diff --git a/src/Example.idr b/src/Example.idr
index 83d6acc..3676d5e 100644
--- a/src/Example.idr
+++ b/src/Example.idr
@@ -24,7 +24,7 @@ strSTLC = MkStrength
   { strength = \p,x,mon => \case
     (App f x) => \theta => App (f theta) (x theta)
     (Lam str {ty1} body) => \theta =>
-        Lam str $ body $ extend p (mon.var (%% str))
+        Lam str $ body $ p.extend (mon.var (%% str))
       $ \v => mon.ren (theta v)
                       (\u => ThereVar u) -- Bug: can't eta-reduce
   }
diff --git a/src/SOAS/Context.idr b/src/SOAS/Context.idr
index 25d2308..ef657ae 100644
--- a/src/SOAS/Context.idr
+++ b/src/SOAS/Context.idr
@@ -19,6 +19,11 @@ data (.Erased) : type.Ctx -> Type where
   S : ctx.Erased -> (ctx :< x).Erased
 
 public export
+(.toNat) : ctx.Erased -> Nat
+(Z).toNat = 0
+(S length).toNat = S length.toNat
+
+public export
 (++) : (ctx1,ctx2 : type.Ctx) -> type.Ctx
 ctx1 ++ [<] = ctx1
 ctx1 ++ (ctx2 :< ty) = (ctx1 ++ ctx2) :< ty
diff --git a/src/SOAS/Structure.idr b/src/SOAS/Structure.idr
index 854725f..5f9e1c9 100644
--- a/src/SOAS/Structure.idr
+++ b/src/SOAS/Structure.idr
@@ -19,18 +19,11 @@ type.VarPointedCoalgStruct = MkPointedCoalgStruct
   , var = id
   }
 
-liftPos :
-  (length : ctx.Erased) -> (mon : type.PointedCoalgStruct p) =>
-  (p.subst ctx1 ctx2) -> p.substNamed (ctx1 ++ ctx) (ctx2 ++ ctx)
-liftPos Z     f x = f x.toVar
-liftPos (S l) f Here        = mon.var (Here .toVar)
-liftPos (S l) f (There pos) = mon.ren (liftPos l f pos) ThereVar
-
 export
 lift :
   (length : ctx.Erased) -> (mon : type.PointedCoalgStruct p) =>
   (p.subst ctx1 ctx2) -> p.subst (ctx1 ++ ctx) (ctx2 ++ ctx)
-lift ctx f v = liftPos ctx f v.pos
+lift length f = p.copair length (\v => mon.ren (f v) weakl) (mon.var . weakr)
 
 -- Substitution Monoid
 
@@ -44,11 +37,11 @@ export
 (.sub) :
   (mon : type.MonStruct m) ->
   m sy (ctx :< (n :- ty)) -> m ty ctx -> m sy ctx
-mon.sub t s = mon.mult t (extend m s mon.var)
+mon.sub t s = mon.mult t (m.extend s mon.var)
 
 export
 (.sub2) :
   (mon : type.MonStruct m) ->
   m sy (ctx :< (x :- ty1) :< (x :- ty2)) ->
   m ty1 ctx ->  m ty2 ctx -> m sy ctx
-mon.sub2 t s1 s2 = mon.mult t (extend m s2 (extend m s1 mon.var))
+mon.sub2 t s1 s2 = mon.mult t (m.extend s2 (m.extend s1 mon.var))
diff --git a/src/SOAS/Var.idr b/src/SOAS/Var.idr
index f3129f9..22e8028 100644
--- a/src/SOAS/Var.idr
+++ b/src/SOAS/Var.idr
@@ -1,48 +1,53 @@
 module SOAS.Var
 
+import Data.Nat
+import Data.So
+
 import SOAS.Context
 import SOAS.Family
 
 prefix 4 %%
 infixr 3 ~> , ~:>
 
-public export
-data (.varPos) : (ctx : type.Ctx) -> (0 x : String) -> type -> Type
-    where [search x]
-  Here  : (ctx :< (x :- ty)).varPos x ty
-  There : ctx.varPos x ty -> (ctx :< sy).varPos x ty
+--------------------------------------------------------------------------------
+-- Variables
 
 public export
-data (.var) : type.Ctx -> type -> Type where
-  (%%) : (0 name : String) -> {auto pos : ctx.varPos name ty} -> ctx.var ty
-
-0
-(.name) : ctx.var ty -> String
-(%% name).name = name
+data (.varAt) : (ctx : type.Ctx) -> (0 x : String) -> (n : Nat) -> type -> Type
+  where [search x]
+  Here  : (ctx :< (x :- ty)).varAt x 0 ty
+  There : ctx.varAt x n ty -> (ctx :< sy).varAt x (S n) ty
 
-export
-(.pos) : (v : ctx.var ty) -> ctx.varPos v.name ty
-((%% name) {pos}).pos = pos
+public export
+record (.var) (ctx : type.Ctx) (ty : type)  where
+  constructor (%%)
+  0 name : String
+  {idx : Nat}
+  {auto 0 pos : ctx.varAt name idx ty}
 
 export
-(.toVar) : (v : ctx.varPos x ty) -> ctx.var ty
-pos.toVar {x} = (%% x) {pos}
+(.toVar) : {n : Nat} -> (0 v : ctx.varAt x n ty) -> ctx.var ty
+pos.toVar = %% x
 
 export
 ThereVar : (v : ctx.var ty) -> (ctx :< ex).var ty
-ThereVar v = (%% v.name) {pos = There v.pos}
+ThereVar v = (%% v.name) {idx = S v.idx, pos = There v.pos}
 
 public export
 Var : type.SortedFamily
 Var = flip (.var)
 
+--------------------------------------------------------------------------------
+-- Substitutions
+
 public export 0
 (.subst) : {type : Type} -> type.SortedFamily -> type.Ctx -> type.Ctx -> Type
 f.subst ctx1 ctx2 = type.gensubst Var f ctx1 ctx2
 
 public export 0
 (.substNamed) : {type : Type} -> type.SortedFamily -> type.Ctx -> type.Ctx -> Type
-f.substNamed ctx1 ctx2 = {0 x : String} -> {0 ty : type} -> ctx1.varPos x ty -> f ty ctx2
+f.substNamed ctx1 ctx2 =
+  {k : Nat} -> {0 x : String} -> {0 ty : type} -> (0 pos : ctx1.varAt x k ty) -> f ty ctx2
 
 public export 0
 (~>) : {type : Type} -> (src, tgt : type.Ctx) -> Type
@@ -52,40 +57,74 @@ public export 0
 (~:>) : {type : Type} -> (src, tgt : type.Ctx) -> Type
 (~:>) = (Var).substNamed
 
-weakl : (ctx1, ctx2 : type.Ctx) -> ctx1 ~> (ctx1 ++ ctx2)
-weakl ctx1 [<] x = x
-weakl ctx1 (ctx2 :< z) x = ThereVar (weakl ctx1 ctx2 x)
+weaklPos :
+  (length : ctx2.Erased) -> ctx1.varAt x n ty ->
+  (ctx1 ++ ctx2).varAt x (length.toNat + n) ty
+weaklPos Z          pos = pos
+weaklPos (S length) pos = There (weaklPos length pos)
 
-weakrNamed : (ctx1, ctx2 : type.Ctx) -> ctx2 ~:> (ctx1 ++ ctx2)
-weakrNamed ctx1 (ctx :< (x :- ty)) Here = (%% x) {pos = Here}
-weakrNamed ctx1 (ctx :< sy) (There pos) =
-  ThereVar $ weakrNamed ctx1 ctx pos
+%inline
+weaklNamed : {auto length : ctx2.Erased} -> ctx1 ~:> (ctx1 ++ ctx2)
+weaklNamed pos = (weaklPos length pos).toVar
 
-weakr : (ctx1, ctx2 : type.Ctx) -> ctx2 ~> (ctx1 ++ ctx2)
-weakr ctx1 ctx2 ((%% name) {pos}) = weakrNamed ctx1 ctx2 pos
+export
+weakl : {auto length : ctx2.Erased} -> ctx1 ~> (ctx1 ++ ctx2)
+weakl v = weaklNamed v.pos
 
-(.copairPos) :
-  (0 x : type.SortedFamily) -> {auto length : ctx2.Erased} ->
+weakrPos : ctx2.varAt x n ty -> (ctx1 ++ ctx2).varAt x n ty
+weakrPos Here        = Here
+weakrPos (There pos) = There (weakrPos pos)
+
+weakrNamed : ctx2 ~:> (ctx1 ++ ctx2)
+weakrNamed pos = (weakrPos pos).toVar
+
+export
+weakr : ctx2 ~> (ctx1 ++ ctx2)
+weakr v = weakrNamed v.pos
+
+splitPosL :
+  (length : ctx2.Erased) -> (0 lt : So (n < length.toNat)) ->
+  (ctx1 ++ ctx2).varAt x n ty -> ctx2.varAt x n ty
+splitPosL Z lt Here impossible
+splitPosL (S length) lt Here = Here
+splitPosL (S length) lt (There pos) = There (splitPosL length lt pos)
+
+splitPosR :
+  (length : ctx2.Erased) -> (0 gte : So (not (n < length.toNat))) ->
+  (ctx1 ++ ctx2).varAt x n ty -> ctx1.varAt x (minus n length.toNat) ty
+splitPosR Z gte pos = rewrite minusZeroRight n in pos
+splitPosR (S z) gte (There pos) = splitPosR z gte pos
+
+(.copairNamed) :
+  (0 x : type.SortedFamily) -> (length : ctx2.Erased) ->
   x.subst ctx1 ctx -> x.subst ctx2 ctx -> x.substNamed (ctx1 ++ ctx2) ctx
-x.copairPos {length = Z} g1 g2 pos = g1 $ pos.toVar
-x.copairPos {length = S l} g1 g2 Here = g2 (Here .toVar)
-x.copairPos {length = S l} g1 g2 (There pos) =
-  x.copairPos g1 (g2 . ThereVar) pos
+x.copairNamed length g1 g2 {k} pos =
+  case choose (k < length.toNat) of
+    Left lt => g2 (splitPosL length lt pos).toVar
+    Right gte => g1 (splitPosR length gte pos).toVar
 
+export
 (.copair) :
-  (0 x : type.SortedFamily) -> {auto length : ctx2.Erased} ->
+  (0 x : type.SortedFamily) -> (length : ctx2.Erased) ->
   x.subst ctx1 ctx -> x.subst ctx2 ctx -> x.subst (ctx1 ++ ctx2) ctx
-x.copair g1 g2 v = x.copairPos g1 g2 v.pos
+x.copair length g1 g2 v = x.copairNamed length g1 g2 v.pos
+
+(.singletonNamed) : (0 x : type.SortedFamily) -> x ty ctx -> x.substNamed [<(n :- ty)] ctx
+x.singletonNamed {ty} u Here = u
+x.singletonNamed {ty} u (There v) impossible -- workaround
+
+(.singleton) : (0 x : type.SortedFamily) -> x ty ctx -> x.subst [<(n :- ty)] ctx
+x.singleton {ty} u v = x.singletonNamed u v.pos
 
 export
-extend :
+(.extend) :
   (0 x : type.SortedFamily) ->
   x ty ctx2 -> x.subst ctx1 ctx2 ->
   x.subst (ctx1 :< (n :- ty)) ctx2
-extend x {ctx2, ty} u theta = x.copair {length = S Z} theta workaround -- (\case {Here => x})
-    where
-      workaround : x.subst [< (n :- ty)] ctx2
-      workaround ((%% _) {pos = Here}) = u
+x.extend {ty} u theta = x.copair (S Z) theta (x.singleton u)
+
+--------------------------------------------------------------------------------
+-- Families
 
 public export 0
 (^) : (tgt, src : type.SortedFamily) -> type.SortedFamily