module CC.Term.Pretty

import CC.Name
import CC.Term

import Text.PrettyPrint.Prettyprinter

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

startPrec, leftArrowPrec, leftAppPrec, appPrec : Prec
startPrec = Open
leftArrowPrec = Backtick
leftAppPrec = Open
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

export
{ctx : Context} -> Pretty (Term ctx) where
  prettyPrec d (Var k n prf) = prettyVar ctx k prf
  prettyPrec d (Let n Nothing val t) =
    parenthesise (d > startPrec) $ group $ align $
      pretty "let" <++>
      (group $ align $ hang 2 $ pretty n <++> equals <+> line <+> pretty val) <+>
      pretty ";" <+> line <+> pretty t
  prettyPrec d (Let n (Just ty) val t) =
    parenthesise (d > startPrec) $ group $ align $
      pretty "let" <++>
      (group $ align $ hang 2 $
        pretty n <++> colon <++> pretty ty <++> equals <+> line <+> pretty val) <+>
      pretty ";" <+> line <+> pretty t
  prettyPrec d Set = pretty "Set"
  prettyPrec d (Pi Nothing dom cod) =
    parenthesise (d > startPrec) $ group $
      prettyPrec leftArrowPrec dom <++> pretty "->" <++> pretty cod
  prettyPrec d (Pi (Just n) dom cod) =
    parenthesise (d > startPrec) $ group $
      parens (pretty n <++> colon <++> pretty dom) <++> pretty "->" <+> softline <+> pretty cod
  prettyPrec 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 = ([], pretty t)
  prettyPrec d (App t u) =
    parenthesise (d >= appPrec) $ group $
    prettyPrec leftAppPrec t <++> prettyPrec appPrec u