Define generic syntax construction.main

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

10 files changed, 210 insertions, 103 deletions

diff --git a/soas.ipkg b/soas.ipkg
index 5255261..88c49db 100644
--- a/soas.ipkg
+++ b/soas.ipkg
@@ -22,6 +22,7 @@ modules = SOAS
     , SOAS.Family
     , SOAS.Strength
     , SOAS.Structure
+    , SOAS.Syntax
     , SOAS.Theory
     , SOAS.Var
 
diff --git a/src/Example.idr b/src/Example.idr
index 3676d5e..ed7d891 100644
--- a/src/Example.idr
+++ b/src/Example.idr
@@ -9,77 +9,45 @@ infixr 3 -:>
 -- but deriving their functoriality and strength is annoying
 -- and not needed with enough metaprogramming
 
-data TypeSTLC = B | (-:>) TypeSTLC TypeSTLC
-
-data STLC : TypeSTLC .SortedFunctor  where
-  App : (f : a (ty1 -:> ty2) ctx) ->
-        (x : a ty1 ctx) -> STLC a ty2 ctx
-  Lam : (x : String) ->
-        (body : a ty2 (ctx :< (x :- ty1))) ->
-        STLC a (ty1 -:> ty2) ctx
-
-%hint
-strSTLC : Strength STLC
-strSTLC = MkStrength
-  { strength = \p,x,mon => \case
-    (App f x) => \theta => App (f theta) (x theta)
-    (Lam str {ty1} body) => \theta =>
-        Lam str $ body $ p.extend (mon.var (%% str))
-      $ \v => mon.ren (theta v)
-                      (\u => ThereVar u) -- Bug: can't eta-reduce
-  }
-
-%hint
-functorialitySTLC : STLC .Map
-functorialitySTLC = MkMap
-  { map = \h => \case
-    (App f x) => App (h f) (h x)
-    (Lam str body) => Lam str (h body)
-  }
+%hide Syntax.PreorderReasoning.prefix.(|~)
+%hide Syntax.PreorderReasoning.Generic.prefix.(|~)
 
-data Term : (meta : type.SortedFamily) -> type.SortedFamily where
-  Va : Var -|> Term meta
-  Me : meta -|> Term meta ^ Term meta
-  Op : STLC (Term meta) -|> Term meta
---   -- La : (x : String) -> bind [< x :- ty1 ] (Term meta) ty2 -||> Term meta (ty1 -:> ty2)
---   -- bug: unification error in Ex1
---   La : (x : String) -> Term meta ty2 (ctx :< (x :- ty1)) -> Term meta (ty1 -:> ty2) ctx
---   -- Ap : Term meta (ty1 -:> ty2) -||> Term meta ty1 =||> Term meta ty2
---   Ap : Term meta (ty1 -:> ty2) ctx -> Term meta ty1 ctx -> Term meta ty2 ctx
+data TypeSTLC = B | (-:>) TypeSTLC TypeSTLC
 
-%hint
-TermMetaAlg : STLC .MetaAlg meta (Term meta)
-TermMetaAlg = MkMetaAlg
-  { alg = Op
-  , var = Va
-  , mvar = Me
-  }
+data OpSTLC : TypeSTLC -> (TypeSTLC .Ctx, TypeSTLC).Ctx -> Type where
+  App : OpSTLC ty2 [<"f" :- ([<], ty1 -:> ty2), "x" :- ([<], ty1)]
+  Lam : OpSTLC (ty1 -:> ty2) [<"body" :- ([<"x" :- ty1], ty2)]
 
-%hint
-TermInitial : STLC .Initial meta (Term meta)
-TermInitial = MkInitial
-  { metalg = TermMetaAlg
-  , bang = bang
-  }
-  where
-    bang : (0 b : TypeSTLC .SortedFamily) -> (metalg : STLC .MetaAlg meta b) -> Term meta -|> b
-    bang b metalg (Va v) = metalg.var v
-    bang b metalg (Me m theta) = metalg.mvar m (\v => bang b metalg (theta v))
-    bang b metalg (Op (Lam str body)) = metalg.alg (Lam str (bang b metalg body))
-    bang b metalg (Op (App f x)) = metalg.alg (App (bang b metalg f) (bang b metalg x))
+STLC : TypeSTLC .Signature
+STLC = MkSig OpSTLC $ \case
+  App => [<Z, Z]
+  Lam => [<S Z]
 
-Ex1 : Term Var (B -:> (B -:> B) -:> B) [<]
-Ex1 = Op $ Lam "x" $ Op $ Lam "f" $ Op $ App (Va $ %% "f") (Va $ %% "x")
+Ex1 : STLC .Term Var (B -:> (B -:> B) -:> B) [<]
+Ex1 =
+  Alg $ Op Lam [<Bind [<"x"] $
+  Alg $ Op Lam [<Bind [<"f"] $
+    Alg $ Op App [<[] (Var (%% "f")), [] (Var (%% "x"))]]]
 
 beta :
-  {0 body : Term Var ty2 (ctx :< (x :- ty1))} ->
-  Singleton (Op $ App (Op $ Lam x body) t) -> Term Var ty2 ctx
-beta (Val (Op $ App (Op $ Lam x body) t)) = TermInitial .monStruct.sub body t
-
-Ex2 : Term Var (B -:> B) [<]
-Ex2 = Op $ App
-        (Op $ Lam "f" $ Op $ Lam "x" $ Op $ App (Va $ %% "f") (Va $ (%% "x") {pos = Here}))
-        (Op $ Lam "x" $ Va $ %% "x")
-
-Ex3 : Term Var (B -:> B) [<]
-Ex3 = beta $ Val Ex2
+  {0 body : STLC .Term Var ty2 (ctx :< (x :- ty1))} ->
+  Singleton (Alg $ Op App [<[] (Alg $ Op Lam [<Bind [<x] body]), [] t]) ->
+  STLC .Term Var ty2 ctx
+beta (Val $ Alg $ Op App [<Bind [<] $ Alg $ Op Lam [<Bind [<x] body], Bind [<] t]) =
+  (STLC .Term Var).sub body t
+
+eta : STLC .Term Var (ty1 -:> ty2) ctx -> STLC .Term Var (ty1 -:> ty2) ctx
+eta t =
+  Alg $ Op Lam [<Bind [<"x"] $
+    Alg $ Op App [<[] ((STLC .Term Var).wkn t), [] (Var $ %% "x")]]
+
+Ex2 : STLC .Term Var (B -:> B) [<]
+Ex2 =
+  Alg $ Op App
+    [<[] (Alg $ Op Lam [<Bind [<"f"] $
+          Alg $ Op Lam [<Bind [<"x"] $
+          Alg $ Op App [<[] (Var $ (%% "f") {pos = There Here}), [] (Var $ %% "x")]]])
+    , [] (Alg $ Op Lam [<Bind [<"x"] $ Var $ %% "x"])]
+
+Ex3 : STLC .Term Var (B -:> B) [<]
+Ex3 = eta $ beta $ Val Ex2
diff --git a/src/SOAS.idr b/src/SOAS.idr
index 892f039..9eb7c4c 100644
--- a/src/SOAS.idr
+++ b/src/SOAS.idr
@@ -5,6 +5,7 @@ import public SOAS.Context
 import public SOAS.Family
 import public SOAS.Strength
 import public SOAS.Structure
+import public SOAS.Syntax
 import public SOAS.Theory
 import public SOAS.Var
 
@@ -88,7 +89,3 @@ import public SOAS.Var
 -- prod : (signatures : List $ type.SortedFunctor) ->
 --   type.SortedFunctor
 -- (prod signatures) x ty ctx = All (\sig => sig x ty ctx) signatures
-
-public export
-bind : (tys : type.Ctx) -> type.SortedFunctor
-bind tys = (<<< tys)
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