module Obs.Pretty

import public Text.PrettyPrint.Prettyprinter

-- ty is rendered Open
export
prettyDecl : (name : Maybe String) -> (ty : Doc ann) -> Doc ann
prettyDecl Nothing ty = parens $ group $ align ty
prettyDecl (Just name) ty = parens $ group (pretty name <++> colon <+> line <+> align ty)

-- names are rendered Open
export
prettyDeclForm : (prec : Prec) ->
  (decls : List (Doc ann)) ->
  (sep : String) ->
  (tail : Doc ann) ->
  Doc ann
prettyDeclForm d decls sep tail =
  parenthesise (d > Open) $
  group $
  concatWith (\x, y => x <++> pretty sep <+> line <+> y) $
  decls ++ [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]