{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
{-# LANGUAGE NoImplicitPrelude #-}

{-# OPTIONS_GHC -fno-warn-missing-signatures #-}

module PrettyTCM where

import Prelude hiding (sequence, mapM, (<>))

import Abstract
import {-# SOURCE #-} Eval
import {-# SOURCE #-} TCM
import qualified Util
import Value

#if !MIN_VERSION_base(4,8,0)
import Control.Applicative ((<$>), (<*>))
#endif
import Control.Monad ((<=<))
import Data.Traversable

import qualified Text.PrettyPrint as P


-- from Agda.TypeChecking.Pretty

type Doc = P.Doc

empty, comma, colon :: Monad m => m Doc

empty :: forall (m :: * -> *). Monad m => m Doc
empty      = Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
P.empty
comma :: forall (m :: * -> *). Monad m => m Doc
comma      = Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
P.comma
colon :: forall (m :: * -> *). Monad m => m Doc
colon      = String -> m Doc
forall {m :: * -> *}. Monad m => String -> m Doc
text String
":"
pretty :: a -> m Doc
pretty a
x   = Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> m Doc) -> Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ a -> Doc
forall a. Pretty a => a -> Doc
Util.pretty a
x
-- prettyA x  = P.prettyA x
text :: String -> m Doc
text String
s     = Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> m Doc) -> Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
P.text String
s
pwords :: String -> [m Doc]
pwords String
s   = (Doc -> m Doc) -> [Doc] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Doc] -> [m Doc]) -> [Doc] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ String -> [Doc]
Util.pwords String
s
fwords :: String -> m Doc
fwords String
s   = Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> m Doc) -> Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
Util.fwords String
s
sep :: [f Doc] -> f Doc
sep [f Doc]
ds     = [Doc] -> Doc
P.sep ([Doc] -> Doc) -> f [Doc] -> f Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [f Doc] -> f [Doc]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [f Doc]
ds
fsep :: [f Doc] -> f Doc
fsep [f Doc]
ds    = [Doc] -> Doc
P.fsep ([Doc] -> Doc) -> f [Doc] -> f Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [f Doc] -> f [Doc]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [f Doc]
ds
hsep :: [f Doc] -> f Doc
hsep [f Doc]
ds    = [Doc] -> Doc
P.hsep ([Doc] -> Doc) -> f [Doc] -> f Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [f Doc] -> f [Doc]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [f Doc]
ds
vcat :: [f Doc] -> f Doc
vcat [f Doc]
ds    = [Doc] -> Doc
P.vcat ([Doc] -> Doc) -> f [Doc] -> f Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [f Doc] -> f [Doc]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [f Doc]
ds
f Doc
d1 $$ :: f Doc -> f Doc -> f Doc
$$ f Doc
d2   = Doc -> Doc -> Doc
(P.$$) (Doc -> Doc -> Doc) -> f Doc -> f (Doc -> Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f Doc
d1 f (Doc -> Doc) -> f Doc -> f Doc
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f Doc
d2
f Doc
d1 <> :: f Doc -> f Doc -> f Doc
<> f Doc
d2   = Doc -> Doc -> Doc
(P.<>) (Doc -> Doc -> Doc) -> f Doc -> f (Doc -> Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f Doc
d1 f (Doc -> Doc) -> f Doc -> f Doc
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f Doc
d2
f Doc
d1 <+> :: f Doc -> f Doc -> f Doc
<+> f Doc
d2  = Doc -> Doc -> Doc
(P.<+>) (Doc -> Doc -> Doc) -> f Doc -> f (Doc -> Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f Doc
d1 f (Doc -> Doc) -> f Doc -> f Doc
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f Doc
d2
nest :: Int -> f Doc -> f Doc
nest Int
n f Doc
d   = Int -> Doc -> Doc
P.nest Int
n (Doc -> Doc) -> f Doc -> f Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f Doc
d
braces :: f Doc -> f Doc
braces f Doc
d   = Doc -> Doc
P.braces (Doc -> Doc) -> f Doc -> f Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f Doc
d
brackets :: f Doc -> f Doc
brackets f Doc
d = Doc -> Doc
P.brackets (Doc -> Doc) -> f Doc -> f Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f Doc
d
parens :: f Doc -> f Doc
parens f Doc
d   = Doc -> Doc
P.parens (Doc -> Doc) -> f Doc -> f Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f Doc
d

prettyList :: [f Doc] -> f Doc
prettyList [f Doc]
ds = f Doc -> f Doc
forall {f :: * -> *}. Functor f => f Doc -> f Doc
brackets (f Doc -> f Doc) -> f Doc -> f Doc
forall a b. (a -> b) -> a -> b
$ [f Doc] -> f Doc
forall {f :: * -> *}. Monad f => [f Doc] -> f Doc
fsep ([f Doc] -> f Doc) -> [f Doc] -> f Doc
forall a b. (a -> b) -> a -> b
$ f Doc -> [f Doc] -> [f Doc]
forall {f :: * -> *}. Monad f => f Doc -> [f Doc] -> [f Doc]
punctuate f Doc
forall (m :: * -> *). Monad m => m Doc
comma [f Doc]
ds

punctuate :: f Doc -> [f Doc] -> [f Doc]
punctuate f Doc
_ [] = []
punctuate f Doc
d [f Doc]
ds = (f Doc -> f Doc -> f Doc) -> [f Doc] -> [f Doc] -> [f Doc]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith f Doc -> f Doc -> f Doc
forall {f :: * -> *}. Applicative f => f Doc -> f Doc -> f Doc
(<>) [f Doc]
ds (Int -> f Doc -> [f Doc]
forall a. Int -> a -> [a]
replicate Int
n f Doc
d [f Doc] -> [f Doc] -> [f Doc]
forall a. [a] -> [a] -> [a]
++ [f Doc
forall (m :: * -> *). Monad m => m Doc
empty])
    where
        n :: Int
n = [f Doc] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [f Doc]
ds Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1

-- monadic pretty printing

class ToExpr a where
  toExpression :: a -> TypeCheck Expr

instance ToExpr Expr where
  toExpression :: Expr -> TypeCheck Expr
toExpression = Expr -> TypeCheck Expr
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return

instance ToExpr Val where
  toExpression :: Val -> TypeCheck Expr
toExpression = Val -> TypeCheck Expr
toExpr


class PrettyTCM a where
  prettyTCM :: a -> TypeCheck Doc

instance PrettyTCM Name where
  prettyTCM :: Name -> TypeCheck Doc
prettyTCM = Name -> TypeCheck Doc
forall {m :: * -> *} {a}. (Monad m, Pretty a) => a -> m Doc
pretty

instance PrettyTCM Pattern where
  prettyTCM :: Pattern -> TypeCheck Doc
prettyTCM = Pattern -> TypeCheck Doc
forall {m :: * -> *} {a}. (Monad m, Pretty a) => a -> m Doc
pretty

instance PrettyTCM [Pattern] where
  prettyTCM :: [Pattern] -> TypeCheck Doc
prettyTCM = [TypeCheck Doc] -> TypeCheck Doc
forall {f :: * -> *}. Monad f => [f Doc] -> f Doc
sep ([TypeCheck Doc] -> TypeCheck Doc)
-> ([Pattern] -> [TypeCheck Doc]) -> [Pattern] -> TypeCheck Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pattern -> TypeCheck Doc) -> [Pattern] -> [TypeCheck Doc]
forall a b. (a -> b) -> [a] -> [b]
map Pattern -> TypeCheck Doc
forall {m :: * -> *} {a}. (Monad m, Pretty a) => a -> m Doc
pretty

instance PrettyTCM Expr where
  prettyTCM :: Expr -> TypeCheck Doc
prettyTCM = Expr -> TypeCheck Doc
forall {m :: * -> *} {a}. (Monad m, Pretty a) => a -> m Doc
pretty

instance PrettyTCM (Sort Expr) where
  prettyTCM :: Sort Expr -> TypeCheck Doc
prettyTCM = Sort Expr -> TypeCheck Doc
forall {m :: * -> *} {a}. (Monad m, Pretty a) => a -> m Doc
pretty

instance PrettyTCM Val where
  prettyTCM :: Val -> TypeCheck Doc
prettyTCM = Expr -> TypeCheck Doc
forall {m :: * -> *} {a}. (Monad m, Pretty a) => a -> m Doc
pretty (Expr -> TypeCheck Doc)
-> (Val -> TypeCheck Expr) -> Val -> TypeCheck Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Val -> TypeCheck Expr
toExpr

instance PrettyTCM [Val] where
  prettyTCM :: [Val] -> TypeCheck Doc
prettyTCM = [TypeCheck Doc] -> TypeCheck Doc
forall {f :: * -> *}. Monad f => [f Doc] -> f Doc
sep ([TypeCheck Doc] -> TypeCheck Doc)
-> ([Val] -> [TypeCheck Doc]) -> [Val] -> TypeCheck Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Val -> TypeCheck Doc) -> [Val] -> [TypeCheck Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Expr -> TypeCheck Doc
forall {m :: * -> *} {a}. (Monad m, Pretty a) => a -> m Doc
pretty (Expr -> TypeCheck Doc)
-> (Val -> TypeCheck Expr) -> Val -> TypeCheck Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Val -> TypeCheck Expr
toExpr)

instance PrettyTCM (Sort Val) where
  prettyTCM :: Sort Val -> TypeCheck Doc
prettyTCM = Sort Expr -> TypeCheck Doc
forall {m :: * -> *} {a}. (Monad m, Pretty a) => a -> m Doc
pretty (Sort Expr -> TypeCheck Doc)
-> (Sort Val
    -> StateT
         TCState (ReaderT TCContext (ExceptT TraceError IO)) (Sort Expr))
-> Sort Val
-> TypeCheck Doc
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< (Val -> TypeCheck Expr)
-> Sort Val
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) (Sort Expr)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Sort a -> m (Sort b)
mapM Val -> TypeCheck Expr
toExpr

instance PrettyTCM a => PrettyTCM (OneOrTwo a) where
  prettyTCM :: OneOrTwo a -> TypeCheck Doc
prettyTCM (One a
a)     = a -> TypeCheck Doc
forall a. PrettyTCM a => a -> TypeCheck Doc
prettyTCM a
a
  prettyTCM (Two a
a1 a
a2) = a -> TypeCheck Doc
forall a. PrettyTCM a => a -> TypeCheck Doc
prettyTCM a
a1 TypeCheck Doc -> TypeCheck Doc -> TypeCheck Doc
forall {f :: * -> *}. Applicative f => f Doc -> f Doc -> f Doc
<+> String -> TypeCheck Doc
forall {m :: * -> *}. Monad m => String -> m Doc
text String
"||" TypeCheck Doc -> TypeCheck Doc -> TypeCheck Doc
forall {f :: * -> *}. Applicative f => f Doc -> f Doc -> f Doc
<+> a -> TypeCheck Doc
forall a. PrettyTCM a => a -> TypeCheck Doc
prettyTCM a
a2

instance (ToExpr a) => PrettyTCM (Measure a) where
  prettyTCM :: Measure a -> TypeCheck Doc
prettyTCM Measure a
mu = Measure Expr -> TypeCheck Doc
forall {m :: * -> *} {a}. (Monad m, Pretty a) => a -> m Doc
pretty (Measure Expr -> TypeCheck Doc)
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) (Measure Expr)
-> TypeCheck Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (a -> TypeCheck Expr)
-> Measure a
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) (Measure Expr)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Measure a -> m (Measure b)
mapM a -> TypeCheck Expr
forall a. ToExpr a => a -> TypeCheck Expr
toExpression Measure a
mu

instance (ToExpr a) => PrettyTCM (Bound a) where
  prettyTCM :: Bound a -> TypeCheck Doc
prettyTCM Bound a
beta = Bound Expr -> TypeCheck Doc
forall {m :: * -> *} {a}. (Monad m, Pretty a) => a -> m Doc
pretty (Bound Expr -> TypeCheck Doc)
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) (Bound Expr)
-> TypeCheck Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (a -> TypeCheck Expr)
-> Bound a
-> StateT
     TCState (ReaderT TCContext (ExceptT TraceError IO)) (Bound Expr)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Bound a -> m (Bound b)
mapM a -> TypeCheck Expr
forall a. ToExpr a => a -> TypeCheck Expr
toExpression Bound a
beta

instance (PrettyTCM a, PrettyTCM b) => PrettyTCM (a,b) where
  prettyTCM :: (a, b) -> TypeCheck Doc
prettyTCM (a
a,b
b) = TypeCheck Doc -> TypeCheck Doc
forall {f :: * -> *}. Functor f => f Doc -> f Doc
parens (TypeCheck Doc -> TypeCheck Doc) -> TypeCheck Doc -> TypeCheck Doc
forall a b. (a -> b) -> a -> b
$ a -> TypeCheck Doc
forall a. PrettyTCM a => a -> TypeCheck Doc
prettyTCM a
a TypeCheck Doc -> TypeCheck Doc -> TypeCheck Doc
forall {f :: * -> *}. Applicative f => f Doc -> f Doc -> f Doc
<> TypeCheck Doc
forall (m :: * -> *). Monad m => m Doc
comma TypeCheck Doc -> TypeCheck Doc -> TypeCheck Doc
forall {f :: * -> *}. Applicative f => f Doc -> f Doc -> f Doc
<+> b -> TypeCheck Doc
forall a. PrettyTCM a => a -> TypeCheck Doc
prettyTCM b
b