1 files changed, 38 insertions, 0 deletions
diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index 9221dbd..578bf83 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -30,6 +30,12 @@ data Term : Nat -> Type where
   -- False
   Bottom : Bounds -> Term n
   Absurd : Bounds -> Term n -> Term n -> Term n
+  -- Equality
+  Equal  : Bounds -> Term n -> Term n -> Term n
+  Refl   : Bounds -> Term n -> Term n
+  Transp : Bounds -> Term n -> Term n -> Term n -> Term n -> Term n -> Term n
+  Cast   : Bounds -> Term n -> Term n -> Term n -> Term n
+  CastId : Bounds -> Term n -> Term n
 
 public export
 record Definition (n : Nat) where
@@ -61,6 +67,11 @@ fullBounds tm@(Top x) = MkBounded tm False x
 fullBounds tm@(Point x) = MkBounded tm False x
 fullBounds tm@(Bottom x) = MkBounded tm False x
 fullBounds tm@(Absurd x a t) = mergeBounds (mergeBounds (fullBounds a) (fullBounds t)) (MkBounded tm False x)
+fullBounds tm@(Equal x t u) = mergeBounds (mergeBounds (fullBounds t) (fullBounds u)) (MkBounded tm False x)
+fullBounds tm@(Refl x t) = mergeBounds (fullBounds t) (MkBounded tm False x)
+fullBounds tm@(Transp x t b u t' e) = mergeBounds (mergeBounds (mergeBounds (fullBounds t) (fullBounds b)) (mergeBounds (fullBounds u) (fullBounds t'))) (mergeBounds (fullBounds e) (MkBounded tm False x))
+fullBounds tm@(Cast x b e t) = mergeBounds (mergeBounds (fullBounds b) (fullBounds e)) (mergeBounds (fullBounds t) (MkBounded tm False x))
+fullBounds tm@(CastId x t) = mergeBounds (fullBounds t) (MkBounded tm False x)
 
 -- Pretty Print ----------------------------------------------------------------
 
@@ -109,6 +120,33 @@ Pretty (Term n) where
     parenthesise (d > Open) $
     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 n) where