Print.hs

{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances    #-}
module PiSigma.Print where

import Control.Monad

import Text.PrettyPrint.ANSI.Leijen

import PiSigma.Syntax
import PiSigma.Evaluation
import PiSigma.Nf

-- * Print class for various types

class Print a where
    prt :: Env e => a -> Eval e String

instance Print Val where
    prt a = quote [] a >>= prt

instance Print (Clos Term) where
    prt a = quote [] a >>= prt

instance Print Ne where
    prt a = quote [] a >>= prt

instance Print Term where
    prt a = return (displayS (renderPretty 0.8 75 (pretty a)) "")


data Msg = V Val | C (Clos Term) | T Term | S String

instance Print Msg where
    prt (V v) = prt v
    prt (C c) = prt c
    prt (T t) = prt t
    prt (S s) = return s

failp :: (Print a, Env e) => [a] -> Eval e b
failp ps = do msg <- foldM (\ msg p -> do s <- prt p
                                          return (msg++s)) "" ps
              fail msg

-- * Pretty printer for terms

-- | Context for printing. Determines whether parentheses are
-- required.
type PrintContext = Int

prettyTerm :: PrintContext -> Term -> Doc
prettyTerm _ (Var x)        = text x
prettyTerm _ (Let p t)      = pretty p <> pretty t
prettyTerm _ Type           = text "Type"
prettyTerm c (Q Pi (t1,(n,t2))) =
  contextParens c 1 $
  group (binding 2 n t1 <$> text "->" <+> prettyTerm 1 t2)
prettyTerm c (Q Sigma (t1,(n,t2))) =
  contextParens c 2 $
  binding 2 n t1 <+> text "*" <+> prettyTerm 3 t2
prettyTerm _ (Lam (n,t))    =
  text "\\" <+> text n <+> text "->" <+> prettyTerm 0 t
prettyTerm c (t1 :. t2)     =
  group (hang 2 (contextParens c 3 (prettyTerm 3 t1 <$> prettyTerm 4 t2)))
prettyTerm c (Pair (t1,t2)) =
  tupled (map (prettyTerm 0) [t1,t2])
prettyTerm _ (Split t1 (n1,(n2,t2))) =
  hang 2 (text "split" <+> prettyTerm 0 t1 <+> text "with"
            <+> parens (text n1 <> comma <> text n2)
            <+> text "->" <$> prettyTerm 0 t2)
prettyTerm _ (Enum ls)      = braces (sep (map text ls))
prettyTerm _ (Label l)      = text ('\'' : l)
prettyTerm _ (Case t bs)    =
  hang 2 (text "case" <+> prettyTerm 0 t <+> text "of" <$> branches bs)
prettyTerm c (Lift t)       =
  contextParens c 5 $
  text "^" <> prettyTerm 5 t
prettyTerm _ (Box t)        =
  brackets (prettyTerm 0 t)
prettyTerm c (Force t)      =
  contextParens c 3 $
  text "!" <> prettyTerm 4 t

prettyEntry :: Entry -> Doc
prettyEntry (Defn n t)      =
  hang 2 (text n <+> text "=" <$> prettyTerm 0 t <> text ";")
prettyEntry (Decl n t)      =
  hang 2 (text n <+> text ":" <$> prettyTerm 0 t <> text ";")

binding :: PrintContext -> String -> Term -> Doc
binding c "" t = prettyTerm c t
binding _ n  t = parens (text n <+> colon <+> prettyTerm 0 t)

branches :: [(Label,Term)] -> Doc
branches bs = encloseSep lbrace rbrace (text "|") (map branch bs)
  where branch (n,t) = text n <+> text "->" <+> prettyTerm 0 t

-- | Prints parens if the current context is higher
-- than a certain limit.
contextParens :: PrintContext -> PrintContext -> Doc -> Doc
contextParens c d p | c > d     = parens p
                    | otherwise = p

instance Pretty Term where
  pretty = prettyTerm 0

instance Pretty Entry where
  pretty = prettyEntry