From cb4ec1e7c1551c1d28f00ba11b062daa78e8c4e3 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 20 Dec 2022 11:07:04 +0000
Subject: Add equality types and casts.

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

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

diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index f1a552f..bcc0cb4 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -29,6 +29,12 @@ data Syntax : Type where
   -- False
   Bottom : Bounds -> Syntax
   Absurd : Bounds -> Syntax -> Syntax -> Syntax
+  -- Equality
+  Equal  : Bounds -> Syntax -> Syntax -> Syntax
+  Refl   : Bounds -> Syntax -> Syntax
+  Transp : Bounds -> Syntax -> Syntax -> Syntax -> Syntax -> Syntax -> Syntax
+  Cast   : Bounds -> Syntax -> Syntax -> Syntax -> Syntax
+  CastId : Bounds -> Syntax -> Syntax
 
 public export
 record Definition where
@@ -85,6 +91,33 @@ Pretty Syntax where
     parenthesise (d >= App) $
     group $
     fillSep [pretty "absurd", prettyPrec App a, prettyPrec App t]
+  prettyPrec d (Equal _ t u) =
+    parenthesise (d >= Equal) $
+    group $
+    prettyPrec Equal t <++> pretty "~" <+> softline <+> prettyPrec Equal u
+  prettyPrec d (Refl _ t) =
+    parenthesise (d >= App) $
+    group $
+    fillSep [pretty "refl", prettyPrec App t]
+  prettyPrec d (Transp _ t b u t' e) =
+    parenthesise (d >= App) $
+    group $
+    fillSep $
+    [ pretty "transp"
+    , prettyPrec App t
+    , prettyPrec App b
+    , prettyPrec App u
+    , prettyPrec App t'
+    , prettyPrec App e
+    ]
+  prettyPrec d (Cast _ b e t) =
+    parenthesise (d >= App) $
+    group $
+    fillSep [pretty "cast", prettyPrec App b, prettyPrec App e, prettyPrec App t]
+  prettyPrec d (CastId _ t) =
+    parenthesise (d >= App) $
+    group $
+    fillSep [pretty "castRefl", prettyPrec App t]
 
 export
 Pretty Definition where
-- 
cgit v1.2.3