Define generic syntax construction.main

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

1 files changed, 36 insertions, 68 deletions

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