From a8a4ef9933a1a07b6fbf2d257df2a5fb40b1e87d Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Wed, 21 Dec 2022 20:32:56 +0000
Subject: Add sum types.

---
 src/Obs/Term.idr | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

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

diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index 446fdcb..be3721f 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -24,6 +24,11 @@ data Term : Nat -> Type where
   Pair   : WithBounds (Term n) -> WithBounds (Term n) -> Term n
   Fst    : WithBounds (Term n) -> Term n
   Snd    : WithBounds (Term n) -> Term n
+  -- Disjoint Coproducts
+  Sum    : WithBounds (Term n) -> WithBounds (Term n) -> Term n
+  Left   : WithBounds (Term n) -> Term n
+  Right  : WithBounds (Term n) -> Term n
+  Case   : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n
   -- True
   Top    : Term n
   Point  : Term n
@@ -90,6 +95,22 @@ prettyPrec d (Snd t) =
   parenthesise (d >= App) $
   group $
   fillSep [pretty "snd", prettyPrecBounds App t]
+prettyPrec d (Sum a b) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "Either", prettyPrecBounds App a, prettyPrecBounds App b]
+prettyPrec d (Left t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "Left", prettyPrecBounds App t]
+prettyPrec d (Right t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "Right", prettyPrecBounds App t]
+prettyPrec d (Case t s b f g) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "case", prettyPrecBounds App t, prettyPrecBounds App s, prettyPrecBounds App b, prettyPrecBounds App f, prettyPrecBounds App g]
 prettyPrec d Top = pretty "()"
 prettyPrec d Point = pretty "tt"
 prettyPrec d Bottom = pretty "Void"
-- 
cgit v1.2.3