diff options
Diffstat (limited to 'src/Obs/Syntax.idr')
| -rw-r--r-- | src/Obs/Syntax.idr | 153 |
1 files changed, 63 insertions, 90 deletions
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr index d21569a..7bf4b61 100644 --- a/src/Obs/Syntax.idr +++ b/src/Obs/Syntax.idr @@ -2,6 +2,7 @@ module Obs.Syntax import Obs.Sort + import Text.Bounded import Text.PrettyPrint.Prettyprinter @@ -11,41 +12,34 @@ import Text.PrettyPrint.Prettyprinter public export data Syntax : Type where - Var : String -> Syntax + Var : String -> Syntax -- Sorts - Sort : Sort -> Syntax + Sort : Sort -> Syntax -- Dependent Products - Pi : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> Syntax + Pi : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> Syntax Lambda : WithBounds String -> WithBounds Syntax -> Syntax - App : WithBounds Syntax -> WithBounds Syntax -> Syntax + App : WithBounds Syntax -> WithBounds Syntax -> Syntax -- Dependent Sums - Sigma : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> Syntax - Pair : WithBounds Syntax -> WithBounds Syntax -> Syntax - Fst : WithBounds Syntax -> Syntax - Snd : WithBounds Syntax -> Syntax - -- Disjoint Coproducts - Sum : WithBounds Syntax -> WithBounds Syntax -> Syntax - Left : WithBounds Syntax -> Syntax - Right : WithBounds Syntax -> Syntax - Case : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax - -- Containers - Container : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax - MkContainer : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax - Tag : WithBounds Syntax -> Syntax - Position : WithBounds Syntax -> Syntax - Next : WithBounds Syntax -> Syntax - Sem : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax + Sigma : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> Syntax + Pair : WithBounds Syntax -> WithBounds Syntax -> Syntax + Fst : WithBounds Syntax -> Syntax + Snd : WithBounds Syntax -> Syntax + -- Booleans + Bool : Syntax + True : Syntax + False : Syntax + If : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax -- True - Top : Syntax - Point : Syntax + Top : Syntax + Point : Syntax -- False Bottom : Syntax - Absurd : WithBounds Syntax -> WithBounds Syntax -> Syntax + Absurd : WithBounds Syntax -> Syntax -- Equality - Equal : WithBounds Syntax -> WithBounds Syntax -> Syntax - Refl : WithBounds Syntax -> Syntax + Equal : WithBounds Syntax -> WithBounds Syntax -> Syntax + Refl : WithBounds Syntax -> Syntax Transp : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax - Cast : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax + Cast : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax CastId : WithBounds Syntax -> Syntax public export @@ -65,115 +59,94 @@ prettyPrec d (Sort s) = prettyPrec d s prettyPrec d (Pi var a b) = parenthesise (d > Open) $ group $ - parens (pretty var.val <++> colon <+> softline <+> prettyPrecBounds Open a) <++> - pretty "->" <+> softline <+> - prettyPrecBounds Open b + parens (pretty var.val <++> colon <+> softline <+> align (prettyPrecBounds Open a)) <++> + pretty "->" <+> line <+> + align (prettyPrecBounds Open b) prettyPrec d (Lambda var t) = parenthesise (d > Open) $ group $ backslash <+> pretty var.val <++> - pretty "=>" <+> softline <+> - prettyPrecBounds Open t + pretty "=>" <+> line <+> + align (prettyPrecBounds Open t) prettyPrec d (App t u) = parenthesise (d >= App) $ group $ - fillSep [prettyPrecBounds Open t, prettyPrecBounds App u] + vsep [prettyPrecBounds Open t, prettyPrecBounds App u] prettyPrec d (Sigma var a b) = parenthesise (d >= App) $ group $ - parens (pretty var.val <++> colon <+> softline <+> prettyPrecBounds Open a) <++> - pretty "**" <+> softline <+> - prettyPrecBounds Open b + parens (pretty var.val <++> colon <+> softline <+> align (prettyPrecBounds Open a)) <++> + pretty "**" <+> line <+> + align (prettyPrecBounds Open b) prettyPrec d (Pair t u) = angles $ group $ - neutral <++> prettyPrecBounds Open t <+> comma <+> softline <+> prettyPrecBounds Open u <++> neutral + neutral <++> prettyPrecBounds Open t <+> comma <+> line <+> prettyPrecBounds Open u <++> neutral prettyPrec d (Fst t) = parenthesise (d >= App) $ group $ - fillSep [pretty "fst", prettyPrecBounds App t] + vsep [pretty "fst", prettyPrecBounds App t] prettyPrec d (Snd t) = parenthesise (d >= App) $ group $ - fillSep [pretty "snd", prettyPrecBounds App t] -prettyPrec d (Sum a b) = - parenthesise (d >= App) $ - group $ - fillSep [pretty "Either", prettyPrecBounds App a, prettyPrecBounds App b] -prettyPrec d (Left t) = - parenthesise (d >= App) $ - group $ - fillSep [pretty "Left", prettyPrecBounds App t] -prettyPrec d (Right t) = - parenthesise (d >= App) $ - group $ - fillSep [pretty "Right", prettyPrecBounds App t] -prettyPrec d (Case t s b f g) = + vsep [pretty "snd", prettyPrecBounds App t] +prettyPrec d Bool = pretty "Bool" +prettyPrec d True = pretty "True" +prettyPrec d False = pretty "False" +prettyPrec d (If var a t f g) = parenthesise (d >= App) $ group $ - fillSep [pretty "case", prettyPrecBounds App t, prettyPrecBounds App s, prettyPrecBounds App b, prettyPrecBounds App f, prettyPrecBounds App g] -prettyPrec d (Container a s s') = - parenthesise (d >= App) $ - group $ - fillSep [pretty "Container", prettyPrecBounds App a, prettyPrecBounds App s, prettyPrecBounds App s'] -prettyPrec d (MkContainer t p f) = - parenthesise (d >= User 0) $ - group $ - fillSep - [ prettyPrecBounds (User 0) t <++> pretty "<|" - , prettyPrecBounds (User 0) p <++> pretty "/" - , prettyPrecBounds (User 0) f - ] -prettyPrec d (Tag t) = - parenthesise (d >= App) $ - group $ - fillSep [pretty "tag", prettyPrecBounds App t] -prettyPrec d (Position t) = - parenthesise (d >= App) $ - group $ - fillSep [pretty "position", prettyPrecBounds App t] -prettyPrec d (Next t) = - parenthesise (d >= App) $ - group $ - fillSep [pretty "next", prettyPrecBounds App t] -prettyPrec d (Sem s a t) = - parenthesise (d >= App) $ - group $ - fillSep [pretty "sem", prettyPrecBounds App s, prettyPrecBounds App a, prettyPrecBounds App t] + vsep $ + [ pretty "if" + , parens $ + group $ + backslash <+> pretty var.val <++> + pretty "=>" <+> line <+> + align (prettyPrecBounds Open a) + , prettyPrecBounds App t + , prettyPrecBounds App f + , prettyPrecBounds App g + ] prettyPrec d Top = pretty "()" prettyPrec d Point = pretty "tt" prettyPrec d Bottom = pretty "Void" -prettyPrec d (Absurd a t) = +prettyPrec d (Absurd t) = parenthesise (d >= App) $ group $ - fillSep [pretty "absurd", prettyPrecBounds App a, prettyPrecBounds App t] + vsep [pretty "absurd", prettyPrecBounds App t] prettyPrec d (Equal t u) = parenthesise (d >= Equal) $ group $ - prettyPrecBounds Equal t <++> pretty "~" <+> softline <+> prettyPrecBounds Equal u + prettyPrecBounds Equal t <++> pretty "~" <+> line <+> prettyPrecBounds Equal u prettyPrec d (Refl t) = parenthesise (d >= App) $ group $ - fillSep [pretty "refl", prettyPrecBounds App t] -prettyPrec d (Transp t b u t' e) = + vsep [pretty "refl", prettyPrecBounds App t] +prettyPrec d (Transp a t u t' e) = parenthesise (d >= App) $ group $ - fillSep $ + vsep $ [ pretty "transp" + , prettyPrecBounds App a , prettyPrecBounds App t - , prettyPrecBounds App b , prettyPrecBounds App u , prettyPrecBounds App t' , prettyPrecBounds App e ] -prettyPrec d (Cast b e t) = +prettyPrec d (Cast a b e t) = parenthesise (d >= App) $ group $ - fillSep [pretty "cast", prettyPrecBounds App b, prettyPrecBounds App e, prettyPrecBounds App t] + vsep $ + [ pretty "cast" + , prettyPrecBounds App a + , prettyPrecBounds App b + , prettyPrecBounds App e + , prettyPrecBounds App t + ] prettyPrec d (CastId t) = parenthesise (d >= App) $ group $ - fillSep [pretty "castRefl", prettyPrecBounds App t] + vsep [pretty "castRefl", prettyPrecBounds App t] prettyPrecBounds d (MkBounded val _ _) = prettyPrec d val |