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

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

diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index be3721f..10f2129 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -29,6 +29,13 @@ data Term : Nat -> Type where
   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
+  -- Containers
+  Container : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n
+  MkContainer : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n
+  Tag : WithBounds (Term n) -> Term n
+  Position : WithBounds (Term n) -> Term n
+  Next : WithBounds (Term n) -> Term n
+  Sem : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n
   -- True
   Top    : Term n
   Point  : Term n
@@ -111,6 +118,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