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

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

diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index 71b554c..cf5bb61 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -26,6 +26,8 @@ data Constructor : Nat -> Type where
   Sum    : Sort -> Sort -> NormalForm n -> NormalForm n -> Constructor n
   Left   : NormalForm n -> Constructor n
   Right  : NormalForm n -> Constructor n
+  Container : Sort -> NormalForm n -> Sort -> Sort -> Constructor n
+  MkContainer : NormalForm n -> NormalForm n -> NormalForm n -> Constructor n
   Top    : Constructor n
   Bottom : Constructor n
 
@@ -36,6 +38,9 @@ data Neutral : Nat -> Type where
   Fst    : Neutral n -> Neutral n
   Snd    : Neutral n -> Neutral n
   Case   : Neutral n -> NormalForm n -> NormalForm n -> Neutral n
+  Tag    : Neutral n -> Neutral n
+  Position : Neutral n -> Neutral n
+  Next   : Neutral n -> Neutral n
   Absurd : Neutral n
   Equal  : Neutral n -> NormalForm n -> NormalForm n -> Neutral n
   EqualL : Nat -> Neutral n -> NormalForm n -> Neutral n
@@ -79,6 +84,8 @@ eqCnstr (Pair t u) (Pair t' u') = eqWhnf t t' && eqWhnf u u'
 eqCnstr (Sum s s' a b) (Sum l l' a' b') = s == l && s' == l' && eqWhnf a a' && eqWhnf b b'
 eqCnstr (Left t) (Left t') = eqWhnf t t'
 eqCnstr (Right t) (Right t') = eqWhnf t t'
+eqCnstr (Container s a s' s'') (Container l a' l' l'') = s == l && eqWhnf a a' && s' == l' && s'' == l''
+eqCnstr (MkContainer t p f) (MkContainer t' p' f') = eqWhnf t t' && eqWhnf p p' && eqWhnf f f'
 eqCnstr Top Top = True
 eqCnstr Bottom Bottom = True
 eqCnstr _ _ = False
@@ -88,6 +95,9 @@ eqNtrl (App t u) (App t' u') = eqNtrl t t' && eqWhnf u u'
 eqNtrl (Fst t) (Fst t') = eqNtrl t t'
 eqNtrl (Snd t) (Snd t') = eqNtrl t t'
 eqNtrl (Case t f g) (Case t' f' g') = eqNtrl t t' && eqWhnf f f' && eqWhnf g g'
+eqNtrl (Tag t) (Tag t') = eqNtrl t t'
+eqNtrl (Position t) (Position t') = eqNtrl t t'
+eqNtrl (Next t) (Next t') = eqNtrl t t'
 eqNtrl Absurd Absurd = True
 eqNtrl (Equal a t u) (Equal a' t' u') = eqNtrl a a' && eqWhnf t t' && eqWhnf u u'
 eqNtrl (EqualL i t u) (EqualL j t' u') = i == j && eqNtrl t t' && eqWhnf u u'
@@ -164,6 +174,18 @@ prettyPrecCnstr d (Right t) =
   parenthesise (d >= App) $
   group $
   fillSep [pretty "Right", prettyPrecWhnf App t]
+prettyPrecCnstr d (Container s a s' s'') =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "Container", prettyPrecWhnf App a, prettyPrec App s', prettyPrec App s'']
+prettyPrecCnstr d (MkContainer t p f) =
+  parenthesise (d >= User 0) $
+  group $
+  fillSep
+    [ prettyPrecWhnf (User 0) t <++> pretty "<|"
+    , prettyPrecWhnf (User 0) p <++> pretty "/"
+    , prettyPrecWhnf (User 0) f
+    ]
 prettyPrecCnstr d Top = pretty "()"
 prettyPrecCnstr d Bottom = pretty "Void"
 
@@ -184,6 +206,18 @@ prettyPrecNtrl d (Case t f g) =
   parenthesise (d >= App) $
   group $
   fillSep [pretty "case", prettyPrecNtrl App t, prettyPrecWhnf App f, prettyPrecWhnf App g]
+prettyPrecNtrl d (Tag t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "tag", prettyPrecNtrl App t]
+prettyPrecNtrl d (Position t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "position", prettyPrecNtrl App t]
+prettyPrecNtrl d (Next t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "next", prettyPrecNtrl App t]
 prettyPrecNtrl d Absurd = pretty "absurd"
 prettyPrecNtrl d (Equal _ t u) =
   parenthesise (d >= Equal) $
@@ -258,6 +292,8 @@ renameCnstr (Pair t u) f = Pair (renameWhnf t f) (renameWhnf u f)
 renameCnstr (Sum s s' a b) f = Sum s s' (renameWhnf a f) (renameWhnf b f)
 renameCnstr (Left t) f = Left (renameWhnf t f)
 renameCnstr (Right t) f = Right (renameWhnf t f)
+renameCnstr (Container s a s' s'') f = Container s (renameWhnf a f) s' s''
+renameCnstr (MkContainer t p u) f = MkContainer (renameWhnf t f) (renameWhnf p f) (renameWhnf u f)
 renameCnstr Top f = Top
 renameCnstr Bottom f = Bottom
 
@@ -266,6 +302,9 @@ renameNtrl (App t u) f = App (renameNtrl t f) (renameWhnf u f)
 renameNtrl (Fst t) f = Fst (renameNtrl t f)
 renameNtrl (Snd t) f = Snd (renameNtrl t f)
 renameNtrl (Case t u t') f = Case (renameNtrl t f) (renameWhnf u f) (renameWhnf t' f)
+renameNtrl (Tag t) f = Tag (renameNtrl t f)
+renameNtrl (Position t) f = Position (renameNtrl t f)
+renameNtrl (Next t) f = Next (renameNtrl t f)
 renameNtrl Absurd f = Absurd
 renameNtrl (Equal a t u) f = Equal (renameNtrl a f) (renameWhnf t f) (renameWhnf u f)
 renameNtrl (EqualL i t u) f = EqualL i (renameNtrl t f) (renameWhnf u f)
-- 
cgit v1.2.3