Define semantics and encode types up to pairs.

1 files changed, 40 insertions, 0 deletions

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