Add equality types and casts.

1 files changed, 33 insertions, 0 deletions

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