Add more program structure to abstract terms.

Add more program structure to type inference and checking.

1 files changed, 42 insertions, 0 deletions

diff --git a/src/Obs/Pretty.idr b/src/Obs/Pretty.idr
new file mode 100644
index 0000000..52a358c
--- /dev/null
+++ b/src/Obs/Pretty.idr
@@ -0,0 +1,42 @@
+module Obs.Pretty
+
+import public Text.PrettyPrint.Prettyprinter
+
+-- ty is rendered Open
+export
+prettyDecl : (name : String) -> (ty : Doc ann) -> Doc ann
+prettyDecl name ty = parens $ group (pretty name <++> colon <+> line <+> align ty)
+
+-- ty and tail are rendered Open
+export
+prettyDeclForm : (prec : Prec) ->
+  (name : String) ->
+  (ty : Doc ann) ->
+  (sep : String) ->
+  (tail : Doc ann) ->
+  Doc ann
+prettyDeclForm d name ty sep tail =
+  parenthesise (d > Open) $ group $ vsep $ [prettyDecl name ty <++> pretty sep, align tail]
+
+-- body is rendered Open
+export
+prettyLambda : (prec : Prec) -> (name : String) -> (body : Doc ann) -> Doc ann
+prettyLambda d name body =
+  parenthesise (d >= App) $ group $ vsep [backslash <+> pretty name <++> pretty "=>", align body]
+
+-- head is rendered Open, tail are rendered App
+export
+prettyApp : (prec : Prec) -> (head : Doc ann) -> (tail : List (Doc ann)) -> Doc ann
+prettyApp d head tail = parenthesise (d >= App) $ group $ vsep (align head :: map (hang 2) tail)
+
+-- first and second are rendered Open
+export
+prettyPair : (first, second : Doc ann) -> Doc ann
+prettyPair first second =
+  angles $ group (neutral <++> align first <+> comma <+> line <+> align second <++> neutral)
+
+-- left and right are rendered Equal
+export
+prettyEqual : (prec : Prec) -> (left, right : Doc ann) -> Doc ann
+prettyEqual d left right =
+  parenthesise (d >= Equal) $ group $ vsep [align left <++> pretty "~", align right]