From 49e4b61cd6b8150e516997606e803bfeec75d1f0 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Sun, 18 Dec 2022 22:56:48 +0000
Subject: Add dependent sums.

---
 src/Obs/Syntax.idr | 25 ++++++++++++++++++++++++-
 1 file changed, 24 insertions(+), 1 deletion(-)

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

diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index 4a7ee0c..f1a552f 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -18,6 +18,11 @@ data Syntax : Type where
   Pi     : Bounds -> WithBounds String -> Syntax -> Syntax -> Syntax
   Lambda : Bounds -> WithBounds String -> Syntax -> Syntax
   App    : Syntax -> Syntax -> Syntax
+  -- Dependent Sums
+  Sigma  : Bounds -> WithBounds String -> Syntax -> Syntax -> Syntax
+  Pair   : Bounds -> Syntax -> Syntax -> Syntax
+  Fst    : Bounds -> Syntax -> Syntax
+  Snd    : Bounds -> Syntax -> Syntax
   -- True
   Top    : Bounds -> Syntax
   Point  : Bounds -> Syntax
@@ -55,8 +60,26 @@ Pretty Syntax where
     parenthesise (d >= App) $
     group $
     fillSep [prettyPrec Open t, prettyPrec App u]
+  prettyPrec d (Sigma _ var a b) =
+    parenthesise (d >= App) $
+    group $
+    parens (pretty var.val <++> colon <+> softline <+> prettyPrec Open a) <++>
+    pretty "**" <+> softline <+>
+    prettyPrec Open b
+  prettyPrec d (Pair _ t u) =
+    angles $
+    group $
+    neutral <++> prettyPrec Open t <+> comma <+> softline <+> prettyPrec Open u <++> neutral
+  prettyPrec d (Fst _ t) =
+    parenthesise (d >= App) $
+    group $
+    fillSep [pretty "fst", prettyPrec App t]
+  prettyPrec d (Snd _ t) =
+    parenthesise (d >= App) $
+    group $
+    fillSep [pretty "snd", prettyPrec App t]
   prettyPrec d (Top _) = pretty "()"
-  prettyPrec d (Point _) = pretty "*"
+  prettyPrec d (Point _) = pretty "tt"
   prettyPrec d (Bottom _) = pretty "Void"
   prettyPrec d (Absurd _ a t) =
     parenthesise (d >= App) $
-- 
cgit v1.2.3