{-# LANGUAGE FlexibleInstances,TypeSynonymInstances #-}

module MProver.PPrint where

import MProver.Syntax
import MProver.Monad
import MProver.Eval (unnestApp)

import Unbound.LocallyNameless

import Text.PrettyPrint.HughesPJ

import Data.Char

class Ppr p where
  ppr :: (Monad m) => p -> MPT m Doc
  
isidentifier :: String -> Bool
isidentifier (c:cs) = isAlphaNum c && all (\c -> isAlphaNum c || c == '\'' || c == '_') cs

instance Ppr Expr where
  ppr (Lambda b) = do
                     (x,e) <- unbind b
                     e_    <- ppr e
                     return $ parens $ text "\\" <+> text (name2String x) <+> text "->" <+> e_
  ppr (Var x)    = if isidentifier (name2String x) then return $ text $ name2String x else return $ parens $ text $ name2String x
  ppr (Ctor c)   = return $ text c
  ppr (Literal l) = ppr l
  ppr (Let b)     = do
                      (r,e)  <- unbind b
                      let ds =  unrec r
                      ds_    <- mapM ppr ds
                      e_     <- ppr e
                      return $ parens $ text "let" $+$ (nest 2 $ braces $ vcat $ punctuate semi ds_) $+$ text "in" $+$ (nest 2 e_)
  ppr (Case e as) = do
                      e_  <- ppr e
                      as_ <- mapM ppr as
                      return $ parens $ text "case" <+> e_ <+> text "of" $+$ (nest 2 $ braces $ vcat $ punctuate semi as_)
  ppr (App e1 e2) = do
                      let (f,args) = unnestApp (App e1 e2)
                      args_ <- mapM ppr args
                      case (f,args_) of
                        (Var x,[a1_,a2_]) | not (isidentifier (name2String x)) && length args == 2 -> do
                           return $ parens $ a1_ <+> text (name2String x) <+> a2_
                        _ -> do
                           f_    <- ppr f
                           return $ parens $ f_ <+> hsep args_
  ppr Bottom      = return $ text "_|_"

instance Ppr (Name Expr,Embed Expr) where
  ppr (n,em) = do
                 e_ <- ppr (unembed em)
                 return $ text (name2String n) <+> equals <+> e_

instance Ppr Alt where
  ppr b = do
            (p,e) <- unbind b
            p_    <- ppr p
            e_    <- ppr e
            return $ p_ <+> text "->" <+> e_

instance Ppr Pat where
  ppr (PatVar x)     = return $ text $ name2String x
  ppr (PatCtor c)    = return $ text c
  ppr (PatLiteral l) = ppr l
  ppr PatWildcard    = return $ text "_"
  ppr (PatApp c ps)  = do
                         ps_ <- mapM ppr ps
                         return $ parens $ text c <+> hsep ps_
  ppr PatBottom      = return $ text "_|_"

instance Ppr Lit where
  ppr (LitInteger i) = return $ int (fromIntegral i)
  ppr (LitChar c)    = return $ text $ show c
  ppr (LitFrac d)    = return $ double d

instance Ppr Formula where
  -- FIXME: ty
  ppr (ForallExpr _ b) = do
                           (x,fo) <- unbind b
                           fo_    <- ppr fo
                           return $ text "Forall" <+> text (name2String x) <> comma <+> fo_
  ppr (ForallProof fo1 fo2) = do
                                fo1_ <- ppr fo1
                                fo2_ <- ppr fo2
                                return $ text "Assuming" <+> fo1_ <> comma <+> fo2_
  ppr (FormulaEq e1 e2) = do
                            e1_ <- ppr e1
                            e2_ <- ppr e2
                            return $ lbrace <+> e1_ <+> equals <+> e2_ <+> rbrace