Split monolithic file into modules.

Prove metatheory for generic initial algebras, instead of a clunky
concrete one.

1 files changed, 85 insertions, 0 deletions

diff --git a/src/Example.idr b/src/Example.idr
new file mode 100644
index 0000000..83d6acc
--- /dev/null
+++ b/src/Example.idr
@@ -0,0 +1,85 @@
+module Example
+
+import Data.Singleton
+import SOAS
+
+infixr 3 -:>
+
+-- Writing the descriptions directly is fine
+-- 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 $ extend p (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)
+  }
+
+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
+
+%hint
+TermMetaAlg : STLC .MetaAlg meta (Term meta)
+TermMetaAlg = MkMetaAlg
+  { alg = Op
+  , var = Va
+  , mvar = Me
+  }
+
+%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))
+
+Ex1 : Term Var (B -:> (B -:> B) -:> B) [<]
+Ex1 = Op $ Lam "x" $ Op $ Lam "f" $ Op $ App (Va $ %% "f") (Va $ %% "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