From 29a05f990dd945be30995c4f46b91b5f7c83abd9 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 4 Jul 2023 13:20:46 +0100
Subject: Make unions a pseudo-built-in type.

---
 src/Term/Semantics.idr | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

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

diff --git a/src/Term/Semantics.idr b/src/Term/Semantics.idr
index 62e2be7..c31a9e6 100644
--- a/src/Term/Semantics.idr
+++ b/src/Term/Semantics.idr
@@ -33,6 +33,29 @@ restrict (Keep thin) = [| mapInit (restrict thin) |]
 indexVar : All p [<x] -> p x
 indexVar [<px] = px
 
+arb : (ty : Ty) -> TypeOf ty
+arb N = 0
+arb (ty ~> ty') = const (arb ty')
+
+swap : (ty1, ty2 : Ty) -> TypeOf (ty1 <+> ty2) -> TypeOf (ty2 <+> ty1)
+swap N N = id
+swap N (ty2 ~> ty2') = (swap N ty2' .)
+swap (ty1 ~> ty1') N = (swap ty1' N .)
+swap (ty1 ~> ty1') (ty2 ~> ty2') = (swap ty1' ty2' .) . (. swap ty2 ty1)
+
+inl : (ty1, ty2 : Ty) -> TypeOf ty1 -> TypeOf (ty1 <+> ty2)
+prl : (ty1, ty2 : Ty) -> TypeOf (ty1 <+> ty2) -> TypeOf ty1
+
+inl N N = id
+inl N (ty2 ~> ty2') = const . inl N ty2'
+inl (ty1 ~> ty1') N = (inl ty1' N .)
+inl (ty1 ~> ty1') (ty2 ~> ty2') = (inl ty1' ty2' .) . (. prl ty1 ty2)
+
+prl N N = id
+prl N (ty2 ~> ty2') = prl N ty2' . ($ arb ty2)
+prl (ty1 ~> ty1') N = (prl ty1' N .)
+prl (ty1 ~> ty1') (ty2 ~> ty2') = (prl ty1' ty2' .) . (. inl ty1 ty2)
+
 %inline
 opSem : Operator tys ty -> TypeOf (foldr (~>) ty tys)
 opSem (Lit n) = n
@@ -43,6 +66,11 @@ opSem Pred = pred
 opSem Minus = minus
 opSem Div = div
 opSem Mod = mod
+opSem (Inl ty1 ty2) = inl ty1 ty2
+opSem (Inr ty1 ty2) = swap ty2 ty1 . inl ty2 ty1
+opSem (Prl ty1 ty2) = prl ty1 ty2
+opSem (Prr ty1 ty2) = prl ty2 ty1 . swap ty1 ty2
+opSem (Arb ty) = arb ty
 
 %inline
 sem' : Monad m => Term ty ctx -> m (All TypeOf ctx -> TypeOf ty)
-- 
cgit v1.2.3