Define semantics and encode types up to pairs.

3 files changed, 87 insertions, 0 deletions

diff --git a/src/Encoded/Bool.idr b/src/Encoded/Bool.idr
new file mode 100644
index 0000000..d185856
--- /dev/null
+++ b/src/Encoded/Bool.idr
@@ -0,0 +1,22 @@
+module Encoded.Bool
+
+import Term.Syntax
+
+export
+B : Ty
+B = N
+
+export
+True : Term B ctx
+True = Lit 0
+  
+export
+False : Term B ctx
+False = Lit 1
+
+export
+if' : Term (B ~> ty ~> ty ~> ty) ctx
+if' = Abs' (\b =>
+  Rec b
+    (Abs $ Const $ Var Here)
+    (Const $ Const $ Abs $ Var Here))
diff --git a/src/Encoded/Pair.idr b/src/Encoded/Pair.idr
new file mode 100644
index 0000000..b2a95ab
--- /dev/null
+++ b/src/Encoded/Pair.idr
@@ -0,0 +1,25 @@
+module Encoded.Pair
+
+import Encoded.Bool
+import Encoded.Union
+import Term.Syntax
+
+export
+(*) : Ty -> Ty -> Ty
+ty1 * ty2 = B ~> (ty1 <+> ty2)
+
+export
+pair : {ty1, ty2 : Ty} -> Term (ty1 ~> ty2 ~> (ty1 * ty2)) ctx
+pair = Abs $ Abs $ Abs $
+  let t = Var (There $ There Here) in
+  let u = Var (There Here) in
+  let b = Var Here in
+  App if' [<b, App inL [<t], App inR [<u]]
+
+export
+fst : {ty1, ty2 : Ty} -> Term ((ty1 * ty2) ~> ty1) ctx
+fst = Abs $ App (prL . Var Here) [<True]
+
+export
+snd : {ty1, ty2 : Ty} -> Term ((ty1 * ty2) ~> ty2) ctx
+snd = Abs $ App (prR . Var Here) [<False]
diff --git a/src/Encoded/Union.idr b/src/Encoded/Union.idr
new file mode 100644
index 0000000..5c3b95c
--- /dev/null
+++ b/src/Encoded/Union.idr
@@ -0,0 +1,40 @@
+module Encoded.Union
+
+import Term.Syntax
+
+export
+(<+>) : Ty -> Ty -> Ty
+N <+> N = N
+N <+> (ty2 ~> ty2') = ty2 ~> (N <+> ty2')
+(ty1 ~> ty1') <+> N = ty1 ~> (ty1' <+> N)
+(ty1 ~> ty1') <+> (ty2 ~> ty2') = (ty1 <+> ty2) ~> (ty1' <+> ty2')
+
+export
+swap : {ty1, ty2 : Ty} -> Term ((ty1 <+> ty2) ~> (ty2 <+> ty1)) ctx
+swap {ty1 = N, ty2 = N} = Id
+swap {ty1 = N, ty2 = ty2 ~> ty2'} = Abs' (\f => swap . f)
+swap {ty1 = ty1 ~> ty1', ty2 = N} = Abs' (\f => swap . f)
+swap {ty1 = ty1 ~> ty1', ty2 = ty2 ~> ty2'} = Abs' (\f => swap . f . swap)
+
+export
+inL : {ty1, ty2 : Ty} -> Term (ty1 ~> (ty1 <+> ty2)) ctx
+export
+prL : {ty1, ty2 : Ty} -> Term ((ty1 <+> ty2) ~> ty1) ctx
+
+inL {ty1 = N, ty2 = N} = Id
+inL {ty1 = N, ty2 = ty2 ~> ty2'} = Abs' (\n => Const (App inL [<n]))
+inL {ty1 = ty1 ~> ty1', ty2 = N} = Abs' (\f => inL . f)
+inL {ty1 = ty1 ~> ty1', ty2 = ty2 ~> ty2'} = Abs' (\f => inL . f . prL)
+
+prL {ty1 = N, ty2 = N} = Id
+prL {ty1 = N, ty2 = ty2 ~> ty2'} = Abs' (\t => App prL [<App t [<Arb]])
+prL {ty1 = ty1 ~> ty1', ty2 = N} = Abs' (\t => prL . t)
+prL {ty1 = ty1 ~> ty1', ty2 = ty2 ~> ty2'} = Abs' (\t => prL . t . inL)
+
+export
+inR : {ty1, ty2 : Ty} -> Term (ty2 ~> (ty1 <+> ty2)) ctx
+inR = swap . inL
+
+export
+prR : {ty1, ty2 : Ty} -> Term ((ty1 <+> ty2) ~> ty2) ctx
+prR = prL . swap