Define generic syntax construction.main

Whilst it works (see `Example`), a generated data type would probably
work better.

1 files changed, 25 insertions, 1 deletions

diff --git a/src/SOAS/Context.idr b/src/SOAS/Context.idr
index ef657ae..e2f3c03 100644
--- a/src/SOAS/Context.idr
+++ b/src/SOAS/Context.idr
@@ -16,7 +16,7 @@ data (.Ctx) : (type : Type) -> Type where
 public export
 data (.Erased) : type.Ctx -> Type where
   Z : [<].Erased
-  S : ctx.Erased -> (ctx :< x).Erased
+  S : ctx.Erased -> (ctx :< (n :- ty)).Erased
 
 public export
 (.toNat) : ctx.Erased -> Nat
@@ -27,3 +27,27 @@ public export
 (++) : (ctx1,ctx2 : type.Ctx) -> type.Ctx
 ctx1 ++ [<] = ctx1
 ctx1 ++ (ctx2 :< ty) = (ctx1 ++ ctx2) :< ty
+
+namespace All
+  public export
+  data (.All) : type.Ctx -> (p : (0 n : String) -> type -> Type) -> Type where
+    Lin : [<].All p
+    (:<) : ctx.All p -> p n ty -> (ctx :< (n :- ty)).All p
+
+  public export
+  head : (ctx :< (n :- ty)).All p -> p n ty
+  head (sx :< px) = px
+
+  public export
+  tail : (ctx :< (n :- ty)).All p -> ctx.All p
+  tail (sx :< px) = sx
+
+public export
+(.rename) : (ctx : type.Ctx) -> (0 names : ctx.All (\_,_ => String)) -> type.Ctx
+[<].rename names = [<]
+(ctx :< (_ :- ty)).rename names = ctx.rename (tail names) :< (head names :- ty)
+
+export
+erasedRename : ctx.Erased -> (ctx.rename names).Erased
+erasedRename Z = Z
+erasedRename (S length) = S (erasedRename length)