module CC.Term.Pretty

import CC.Name
import CC.Term

import Text.PrettyPrint.Prettyprinter

--------------------------------------------------------------------------------

startPrec, leftAppPrec, appPrec : Prec
startPrec = Open
leftAppPrec = Backtick
appPrec = App

prettyVar : (ctx : Context) -> (k : Nat) -> (0 _ : IsVar k n ctx) -> Doc ann
prettyVar (_ :< n) 0 (Here eq) = pretty n
prettyVar (ctx :< _) (S k) (There prf) = prettyVar ctx k prf

prettyTerm : {ctx : Context} -> Prec -> Term ctx -> Doc ann
prettyTerm d (Var k _ prf) = prettyVar ctx k prf
prettyTerm d (Abs n t) =
  let (names, body) = mapFst (pretty n ::) $ getNames t in
  parenthesise (d > startPrec) $ group $
    backslash <+> concatWith (\x, y => x <+> comma <+> line <+> y) names <++>
    pretty "=>" <+> softline <+> body
  where
  getNames : {ctx : Context} -> Term ctx -> (List (Doc ann), Doc ann)
  getNames (Abs n t) = mapFst (pretty n ::) (getNames t)
  getNames t = ([], prettyTerm startPrec t)
prettyTerm d (App t u) =
  parenthesise (d >= appPrec) $ group $
  prettyTerm leftAppPrec t <++> prettyTerm appPrec u
prettyTerm d (Let n t u) =
  parenthesise (d > startPrec) $ group $ align $
    pretty "let" <++>
    (group $ align $ hang 2 $ pretty n <++> pretty "=" <+> line <+> prettyTerm startPrec t) <+>
    pretty ";" <+> line <+>
    prettyTerm startPrec u

export
{ctx : Context} -> Pretty (Term ctx) where
  prettyPrec = prettyTerm