From af7c222cc3e487cd3ca8b5dd8749b7e258da7c7c Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Fri, 16 Jun 2023 18:01:33 +0100
Subject: Define semantics and encode types up to pairs.

---
 src/Term/Syntax.idr | 47 +++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 47 insertions(+)
 create mode 100644 src/Term/Syntax.idr

(limited to 'src/Term/Syntax.idr')

diff --git a/src/Term/Syntax.idr b/src/Term/Syntax.idr
new file mode 100644
index 0000000..a990600
--- /dev/null
+++ b/src/Term/Syntax.idr
@@ -0,0 +1,47 @@
+module Term.Syntax
+
+import public Data.SnocList
+import public Term
+
+-- Combinators
+
+export
+Id : Term (ty ~> ty) ctx
+Id = Abs (Var Here)
+
+export
+Arb : {ty : Ty} -> Term ty ctx
+Arb {ty = N} = Zero
+Arb {ty = ty ~> ty'} = Const Arb
+
+export
+Lit : Nat -> Term N ctx
+Lit 0 = Zero
+Lit (S k) = Suc (Lit k)
+
+-- HOAS
+
+infix 4 ~>*
+
+public export
+(~>*) : SnocList Ty -> Ty -> Ty
+sty ~>* ty = foldr (~>) ty sty
+
+export
+Abs' : (Term ty (ctx :< ty) -> Term ty' (ctx :< ty)) -> Term (ty ~> ty') ctx
+Abs' f = Abs (f $ Var Here)
+
+export
+App' : {ty : Ty} -> Term (ty ~> ty') ctx -> Term ty ctx -> Term ty' ctx
+App' (Const t `Over` thin) u = t `Over` thin
+App' (Abs t `Over` thin) u = subst (t `Over` Keep thin) (Base Id :< u)
+App' t u = App t u
+
+export
+App : {sty : SnocList Ty} -> Term (sty ~>* ty) ctx -> All (flip Term ctx) sty -> Term ty ctx
+App t [<] = t
+App t (us :< u) = App' (App t us) u
+
+export
+(.) : {ty, ty' : Ty} -> Term (ty' ~> ty'') ctx -> Term (ty ~> ty') ctx -> Term (ty ~> ty'') ctx
+t . u = Abs (App (shift t) [<App (shift u) [<Var Here]])
-- 
cgit v1.2.3