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/Term.idr | 29 ++++++++++++++++++++++++++++-
 1 file changed, 28 insertions(+), 1 deletion(-)

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

diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index 366a4b7..9221dbd 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -19,6 +19,11 @@ data Term : Nat -> Type where
   Pi     : Bounds -> String -> Term n -> Term (S n) -> Term n
   Lambda : Bounds -> String -> Term (S n) -> Term n
   App    : Term n -> Term n -> Term n
+  -- Dependent Sums
+  Sigma  : Bounds -> String -> Term n -> Term (S n) -> Term n
+  Pair   : Bounds -> Term n -> Term n -> Term n
+  Fst    : Bounds -> Term n -> Term n
+  Snd    : Bounds -> Term n -> Term n
   -- True
   Top    : Bounds -> Term n
   Point  : Bounds -> Term n
@@ -48,6 +53,10 @@ fullBounds tm@(Sort x s) = MkBounded tm False x
 fullBounds tm@(Pi x var a b) = mergeBounds (mergeBounds (fullBounds a) (fullBounds b)) (MkBounded tm False x)
 fullBounds tm@(Lambda x var t) = mergeBounds (fullBounds t) (MkBounded tm False x)
 fullBounds tm@(App t u) = map (\_ => tm) (mergeBounds (fullBounds t) (fullBounds u))
+fullBounds tm@(Sigma x var a b) = mergeBounds (mergeBounds (fullBounds a) (fullBounds b)) (MkBounded tm False x)
+fullBounds tm@(Pair x t u) = mergeBounds (mergeBounds (fullBounds t) (fullBounds u)) (MkBounded tm False x)
+fullBounds tm@(Fst x t) = mergeBounds (fullBounds t) (MkBounded tm False x)
+fullBounds tm@(Snd x t) = mergeBounds (fullBounds t) (MkBounded tm False x)
 fullBounds tm@(Top x) = MkBounded tm False x
 fullBounds tm@(Point x) = MkBounded tm False x
 fullBounds tm@(Bottom x) = MkBounded tm False x
@@ -75,8 +84,26 @@ Pretty (Term n) 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 <++> 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 > Open) $
-- 
cgit v1.2.3