diff options
Diffstat (limited to 'src/Obs/Syntax.idr')
| -rw-r--r-- | src/Obs/Syntax.idr | 33 |
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 |