Define generic syntax construction.main

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

1 files changed, 103 insertions, 0 deletions

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)