7 files changed, 172 insertions, 31 deletions
diff --git a/src/SOAS/Algebra.idr b/src/SOAS/Algebra.idr
index 7dff735..db701d3 100644
--- a/src/SOAS/Algebra.idr
+++ b/src/SOAS/Algebra.idr
@@ -27,7 +27,6 @@ record (.MetaAlg)
 export
 traverse : {0 p,a : type.SortedFamily} ->
       {0 signature : type.SortedFunctor} ->
-      (functoriality : signature.Map) =>
       (str : Strength signature) =>
       (coalg : type.PointedCoalgStruct p) =>
       (alg : signature a -|> a) ->
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)
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
diff --git a/src/SOAS/Structure.idr b/src/SOAS/Structure.idr
index 5f9e1c9..8c5bb5d 100644
--- a/src/SOAS/Structure.idr
+++ b/src/SOAS/Structure.idr
@@ -34,14 +34,20 @@ record (.MonStruct) (type : Type) (m : type.SortedFamily) where
   mult : m -|> (m ^ m)
 
 export
+(.wkn) :
+  (0 m : type.SortedFamily) -> (mon : type.PointedCoalgStruct m) =>
+  m sy ctx -> m sy (ctx :< (n :- ty))
+m.wkn t = mon.ren t (weakl {length = S Z})
+
+export
 (.sub) :
-  (mon : type.MonStruct m) ->
+  (0 m : type.SortedFamily) -> (mon : type.MonStruct m) =>
   m sy (ctx :< (n :- ty)) -> m ty ctx -> m sy ctx
-mon.sub t s = mon.mult t (m.extend s mon.var)
+m.sub t s = mon.mult t (m.extend s mon.var)
 
 export
 (.sub2) :
-  (mon : type.MonStruct m) ->
+  (0 m : type.SortedFamily) -> (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 (m.extend s2 (m.extend s1 mon.var))
+m.sub2 t s1 s2 = mon.mult t (m.extend s2 (m.extend s1 mon.var))
diff --git a/src/SOAS/Syntax.idr b/src/SOAS/Syntax.idr
new file mode 100644
index 0000000..7f0e3be
--- /dev/null
+++ b/src/SOAS/Syntax.idr
@@ -0,0 +1,103 @@
+module SOAS.Syntax
+
+import SOAS.Algebra
+import SOAS.Context
+import SOAS.Family
+import SOAS.Strength
+import SOAS.Structure
+import SOAS.Theory
+import SOAS.Var
+
+--------------------------------------------------------------------------------
+-- Signatures
+
+public export
+(.ParamsErased) : (type.Ctx, type).Ctx -> Type
+params.ParamsErased = params.All (\_, extty => (fst extty).Erased)
+
+public export
+record (.Signature) (type : Type) where
+  constructor MkSig
+  0 ops : (ty : type) -> (params : (type.Ctx, type).Ctx) -> Type
+  erased :
+    {0 ty : type} -> {0 params : (type.Ctx, type).Ctx} ->
+    (op : ops ty params) -> params.ParamsErased
+
+--------------------------------------------------------------------------------
+-- Functor
+
+public export
+data (.Args) : (type.Ctx, type).Ctx -> type.SortedFamily -> type.Family where
+  Lin  : [<].Args a ctx
+  (:<) :
+    params.Args a ctx ->
+    BindRename ext a ty ctx ->
+    (params :< (n :- (ext, ty))).Args a ctx
+
+public export
+data (.functor) : type.Signature -> type.SortedFunctor where
+  Op : (op : sig.ops ty params) -> (args : params.Args a ctx) -> sig.functor a ty ctx
+
+--------------------------------------------------------------------------------
+-- Functoriality
+
+argsMap : (a -|> b) -> params.Args a -||> params.Args b
+argsMap f [<] = [<]
+argsMap f (sx :< (Bind names x)) = argsMap f sx :< (Bind names $ f x)
+
+export
+%hint
+(.functorMap) : (0 sig : type.Signature) -> sig.functor.Map
+sig.functorMap = MkMap $ \f => \(Op op args) => Op op (argsMap f args)
+
+--------------------------------------------------------------------------------
+-- Strength
+
+argsStr :
+  (erased : params.ParamsErased) -> (mon : type.PointedCoalgStruct p) =>
+  params.Args (x ^ p) -||> params.Args x ^^ p
+argsStr [<] [<] {ctx} theta = [<]
+argsStr (erased :< length) (sx :< (Bind names x)) {ctx} theta =
+  argsStr erased sx theta :< (Bind names $ x $ lift (erasedRename length) theta)
+
+export
+%hint
+(.functorStrength) :
+  (sig : type.Signature) -> Strength sig.functor
+sig.functorStrength = MkStrength $
+  \(Op op args), theta => Op op (argsStr (sig.erased op) args theta)
+
+--------------------------------------------------------------------------------
+-- Terms
+
+public export
+data (.Term) : (sig : type.Signature) -> type.SortedFunctor where
+  Var : Var -|> sig.Term a
+  Alg : sig.functor (sig.Term a) -|> sig.Term a
+  MVar : a -|> sig.Term a ^ sig.Term a
+
+%hint
+export
+(.TermMetalg) : (sig : type.Signature) -> sig.functor.MetaAlg meta (sig.Term meta)
+sig.TermMetalg = MkMetaAlg { alg = Alg, var = Var, mvar = MVar }
+
+%hint
+export
+(.TermInitial) : (sig : type.Signature) -> sig.functor.Initial meta (sig.Term meta)
+sig.TermInitial = MkInitial
+  { metalg = sig.TermMetalg
+  , sem = sem
+  }
+  where
+  sem : (0 b : type.SortedFamily) -> (metalg : sig.functor.MetaAlg meta b) => sig.Term meta -|> b
+  semArgs :
+    (0 b : type.SortedFamily) -> (metalg : sig.functor.MetaAlg meta b) =>
+    {0 params : (type.Ctx, type).Ctx} ->
+    params.Args (sig.Term meta) -||> params.Args b
+
+  sem b (Var v) = metalg.var v
+  sem b (Alg (Op op args)) = metalg.alg $ Op op $ semArgs b args
+  sem b (MVar m f) = metalg.mvar m $ \v => sem b (f v)
+
+  semArgs b [<] = [<]
+  semArgs b (sx :< (Bind names x)) = semArgs b sx :< (Bind names $ sem b x)
diff --git a/src/SOAS/Theory.idr b/src/SOAS/Theory.idr
index f36e7a1..43bb024 100644
--- a/src/SOAS/Theory.idr
+++ b/src/SOAS/Theory.idr
@@ -14,22 +14,14 @@ record (.Initial)
          (a : type.SortedFamily) where
   constructor MkInitial
   metalg : signature.MetaAlg meta a
-  bang :
+  sem :
     (0 b : type.SortedFamily) ->
-    (metalg : signature.MetaAlg meta b) ->
+    (metalg : signature.MetaAlg meta b) =>
     a -|> b
 
-public export
-(.sem) :
-  signature .Initial meta a ->
-  (0 b : type.SortedFamily) -> (metalg : signature.MetaAlg meta b) =>
-  a -|> b
-init.sem b = init.bang b metalg
-
 %hint
 public export
 (.pointedCoalgStruct) :
-  (functoriality : signature.Map) =>
   (str : Strength signature) =>
   signature.Initial meta a -> type.PointedCoalgStruct a
 init.pointedCoalgStruct = MkPointedCoalgStruct
@@ -41,7 +33,6 @@ init.pointedCoalgStruct = MkPointedCoalgStruct
 %hint
 public export
 (.monStruct) :
-  (functoriality : signature.Map) =>
   (str : Strength signature) =>
   signature.Initial meta a -> type.MonStruct a
 init.monStruct = MkSubstMonoidStruct
@@ -52,7 +43,6 @@ init.monStruct = MkSubstMonoidStruct
 %hint
 public export
 (.monoidStruct) :
-  (functoriality : signature.Map) =>
   (str : Strength signature) =>
   signature.Initial meta a -> signature.MonoidStruct a
 init.monoidStruct = MkSignatureMonoid { mon = init.monStruct , alg = init.metalg.alg }
diff --git a/src/SOAS/Var.idr b/src/SOAS/Var.idr
index 22e8028..8362126 100644
--- a/src/SOAS/Var.idr
+++ b/src/SOAS/Var.idr
@@ -7,7 +7,7 @@ import SOAS.Context
 import SOAS.Family
 
 prefix 4 %%
-infixr 3 ~> , ~:>
+infixr 3 ~> , ~:>, ^, ^^
 
 --------------------------------------------------------------------------------
 -- Variables
@@ -127,8 +127,12 @@ x.extend {ty} u theta = x.copair (S Z) theta (x.singleton u)
 -- Families
 
 public export 0
+(^^) : (tgt : type.Family) -> (src : type.SortedFamily) -> type.Family
+(tgt ^^ src) ctx = src.subst ctx -||> tgt
+
+public export 0
 (^) : (tgt, src : type.SortedFamily) -> type.SortedFamily
-(tgt ^ src) ty ctx = src.subst ctx -||> tgt ty
+(tgt ^ src) ty = tgt ty ^^ src
 
 public export 0
 Nil : type.SortedFamily -> type.SortedFamily
@@ -138,3 +142,11 @@ Nil f = f ^ Var
 (*) : (derivative, tangent : type.SortedFamily) -> type.SortedFamily
 (derivative * tangent) ty ctx =
   (ctx' : type.Ctx ** (derivative ty ctx' , tangent.subst ctx' ctx))
+
+--------------------------------------------------------------------------------
+-- Utilities
+
+export
+lookup : ctx.All p -> {k : Nat} -> (0 pos : ctx.varAt n k ty) -> p n ty
+lookup (sx :< px) Here = px
+lookup (sx :< px) (There v) = lookup sx v