From 02cb45707da07d5e6faca92158d10a6e454a6bac Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Thu, 22 Dec 2022 00:02:23 +0000
Subject: Add Container types.

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

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

diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index 9f64c38..d21569a 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -28,6 +28,13 @@ data Syntax : Type where
   Left   : WithBounds Syntax -> Syntax
   Right  : WithBounds Syntax -> Syntax
   Case   : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
+  -- Containers
+  Container : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
+  MkContainer : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
+  Tag : WithBounds Syntax -> Syntax
+  Position : WithBounds Syntax -> Syntax
+  Next : WithBounds Syntax -> Syntax
+  Sem : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
   -- True
   Top    : Syntax
   Point  : Syntax
@@ -105,6 +112,34 @@ 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 (Container a s s') =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "Container", prettyPrecBounds App a, prettyPrecBounds App s, prettyPrecBounds App s']
+prettyPrec d (MkContainer t p f) =
+  parenthesise (d >= User 0) $
+  group $
+  fillSep
+    [ prettyPrecBounds (User 0) t <++> pretty "<|"
+    , prettyPrecBounds (User 0) p <++> pretty "/"
+    , prettyPrecBounds (User 0) f
+    ]
+prettyPrec d (Tag t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "tag", prettyPrecBounds App t]
+prettyPrec d (Position t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "position", prettyPrecBounds App t]
+prettyPrec d (Next t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "next", prettyPrecBounds App t]
+prettyPrec d (Sem s a t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "sem", prettyPrecBounds App s, prettyPrecBounds App a, prettyPrecBounds App t]
 prettyPrec d Top = pretty "()"
 prettyPrec d Point = pretty "tt"
 prettyPrec d Bottom = pretty "Void"
-- 
cgit v1.2.3