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`.

1 files changed, 3 insertions, 10 deletions

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))