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/Syntax.idr | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

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

diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index 36b1b9f..9f64c38 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -23,6 +23,11 @@ data Syntax : Type where
   Pair   : WithBounds Syntax -> WithBounds Syntax -> Syntax
   Fst    : WithBounds Syntax -> Syntax
   Snd    : WithBounds Syntax -> Syntax
+  -- Disjoint Coproducts
+  Sum    : WithBounds Syntax -> WithBounds Syntax -> Syntax
+  Left   : WithBounds Syntax -> Syntax
+  Right  : WithBounds Syntax -> Syntax
+  Case   : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
   -- True
   Top    : Syntax
   Point  : Syntax
@@ -84,6 +89,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