Define generic syntax construction.main

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

1 files changed, 18 insertions, 11 deletions

diff --git a/src/SOAS/Strength.idr b/src/SOAS/Strength.idr
index f902ad4..2174baf 100644
--- a/src/SOAS/Strength.idr
+++ b/src/SOAS/Strength.idr
@@ -1,5 +1,6 @@
 module SOAS.Strength
 
+import SOAS.Context
 import SOAS.Family
 import SOAS.Structure
 import SOAS.Var
@@ -12,22 +13,28 @@ type.SortedFunctor = type.SortedFamily -> type.SortedFamily
 public export
 record Strength (f : type.SortedFunctor) where
   constructor MkStrength
-  strength :
-    (0 p,x : type.SortedFamily) ->
-    (mon : type.PointedCoalgStruct p) ->
+  str :
+    {0 p,x : type.SortedFamily} ->
+    (mon : type.PointedCoalgStruct p) =>
     (f (x ^ p)) -|> ((f x) ^ p)
 
-export
-(.str) :
-  Strength f ->
-  {0 p,x : type.SortedFamily} ->
-  (mon : type.PointedCoalgStruct p) =>
-  (f (x ^ p)) -|> ((f x) ^ p)
-strength.str {p,x,mon} = strength.strength p x mon
-
 public export
 record (.Map) (signature : type.SortedFunctor) where
   constructor MkMap
   map :
     {0 a,b : type.SortedFamily} -> (a -|> b) ->
     signature a -|> signature b
+
+public export
+bind : (tys : type.Ctx) -> type.SortedFunctor
+bind tys = (<<< tys)
+
+public export
+record BindRename (tys : type.Ctx) (a : type.SortedFamily) (ty : type) (ctx : type.Ctx) where
+  constructor Bind
+  0 names : tys.All (\_,_ => String)
+  body : a ty (ctx ++ tys.rename names)
+
+public export
+Nil : a -|> BindRename [<] a
+[] x = Bind [<] x