



{-# LANGUAGE TypeSynonymInstances #-}

-- {-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances #-}
-- {-# LANGUAGE UndecidableInstances #-}
-- {-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
-- {-# LANGUAGE ViewPatterns #-}
-- {-# LANGUAGE DefaultSignatures #-}

{-# LANGUAGE OverloadedStrings #-}

{-# LANGUAGE CPP #-}





-- ghc options

{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_GHC -fno-warn-unused-matches #-}
-- {-# OPTIONS_GHC -fno-warn-name-shadowing #-}


{-# OPTIONS_GHC -fno-warn-orphans #-}
-- {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
-- {-# OPTIONS_GHC -fno-warn-unused-do-bind #-}
-- {-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
-- {-# OPTIONS_GHC -fno-warn-incomplete-uni-patterns #-}
-- {-# OPTIONS_GHC -fno-warn-name-shadowing #-}




-- |
-- Copyright :  (c) Andreas Reuleaux 2015
-- License   :  BSD2
-- Maintainer:  Andreas Reuleaux <rx@a-rx.info>
-- Stability :  experimental
-- Portability: non-portable
--
-- This module provides pretty printing functionality for Pire's
-- abstract and concrete syntax




{-
  exmpls

  nopos <$> parsingFileS moduleDef_ "test/Nat.pi"

  pp <$> parsingFileS moduleDef_ "test/Nat.pi"


  (runExceptT $ getModules  ["test"] "Nat") >>= return . pp . last . fromRight'


 -}



-- A Pretty Printer.




module Pire.Pretty.PP where




import Pire.Syntax.Eps
-- import Pire.Syntax.Binder
import Pire.Syntax.Expr


import Pire.Pretty.Common
import Pire.Pretty.Wrap

import Pire.Pretty.Expr
import Pire.Pretty.Decl ()



import Control.Monad.Reader
import Text.PrettyPrint as TPP


#ifdef MIN_VERSION_GLASGOW_HASKELL
#if MIN_VERSION_GLASGOW_HASKELL(7,10,3,0)
-- ghc >= 7.10.3
#else
-- older ghc versions, but MIN_VERSION_GLASGOW_HASKELL defined
#endif
#else
-- MIN_VERSION_GLASGOW_HASKELL not even defined yet (ghc <= 7.8.x)
import Control.Applicative
#endif




import qualified Data.Text as T


-- -- disp
-- -- dispArg' :: Arg Exp String -> Doc
-- -- dispArg' (Arg ep t) =
-- --     bindParens ep $ dispExp' t


dispArg :: Arg T.Text T.Text -> M Doc


dispArg arg@(Arg ep t) = do
    st <- ask
    let annotParens = if showAnnots st
                      then mandatoryBindParens
                      else bindParens
    let wraparg' (Arg p x) = case x of
              V _       -> bindParens p
              TCon _ []   -> bindParens p
              Type        -> bindParens p
              TyUnit      -> bindParens p
              LitUnit     -> bindParens p
              TyBool      -> bindParens p
              LitBool b   -> bindParens p
              -- Sigma _     -> bindParens p

              Position _ a     -> wraparg' (Arg p a)

              DCon _ [] _ -> annotParens p
              -- Prod _ _ _  -> annotParens p
              TrustMe _   -> annotParens p
              Refl _      -> annotParens p

              _           -> mandatoryBindParens p
    wraparg' arg <$> dispExpr t



-- dispArg arg@(Arg ep t) = do

--     bindParens ep <$> disp t




-- hm, we do have this in Pretty/Binder.hs - right ?

-- -- dispBinder :: Disp s => Binder s -> M Doc

-- -- dispBinder (Binder v ws) = (<>) <$> (disp v) <*> disp ws

-- -- dispBinder (BinderInBrackets bo bnd bc) = return $ text "error: dispBinder(BinderInBrackets ...)"
-- -- -- dispBinder (BinderInBrackets bo (Binder v ws) bc) = (<>) <$> (disp v) <*> disp ws









-- --  > runIdentity (runReaderT (gatherBinders  $ lama "x" $ V "b") initDI)
-- -- ([x],b)
-- --  > runIdentity (runReaderT (gatherBinders  $ lama "x" $ V "x") initDI)
-- -- ([x],x)
-- --  >
-- -- > runIdentity (runReaderT (gatherBinders  $ lama "a" $ lama "x" $ V "x") initDI)
-- -- ([a,x],x)
-- -- >
-- -- > runIdentity (runReaderT (gatherBinders  $ lam "a" $ lam "x" $ V "x" :@ V "z") initDI)
-- -- ([a,x],x z)
-- -- >

-- -- dito for lams
-- -- > runIdentity (runReaderT (gatherBinders  $ lams ["a", "x"] $ V "x" :@ V "z") initDI)
-- -- ([a,x],x z)
-- -- >



-- gatherBinders :: Exp String -> M ([Doc], Doc)


-- gatherBinders (Lam n s) =
--   do
--     let db = text n
--     let body = instantiate1 (V n) s
--     (rest, body) <- gatherBinders body
--     return $ (db : rest, body)



-- gatherBinders (LamA n annot s) =
--   do
--     let dn = text n
--     dt <- dispAnnot annot
--     let db = if isEmpty dt then dn else (parens (dn <+> dt))
--     let body = instantiate1 (V n) s
--     (rest, body) <- gatherBinders body
--     return $ (db : rest, body)





-- gatherBinders (ErasedLamA n annot s) =
--   do
--     let dn = text n
--     dt <- dispAnnot annot
--     let body = instantiate1 (V n) s
--     (rest, body) <- gatherBinders body
--     return $ ( brackets (dn <+> dt) : rest, body)


-- -- maybe somehow gather them recursivley for Lams
-- -- (analogous to the other defs) ?
-- -- this is just the n:[] case, though

-- -- gatherBinders (Lams (n:[]) s) =
-- --   do
-- --     let db = text n
-- --     let body = instantiate1 (V n) s
-- --     (rest, body) <- gatherBinders body
-- --     return $ (db : rest, body)


-- gatherBinders (Lams ns s) =
--   do
--     let dbs = [text b | b <- ns]
--     body <- dispExp $ instantiate (\(Name b ()) -> V b) s
--     return $ (dbs, body)





-- gatherBinders body = do
--   db <- dispExp body
--   return ([], db)




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


  



dispEps :: Eps -> M Doc

dispEps ErasedP = return $ text "ErasedP"
dispEps RuntimeP = return $ text "RuntimeP"

-- dispEps VarP = return $ text "VarP"
-- dispEps WildP = return $ text "WildP"

instance Disp Eps where
  disp = dispEps





