{-# OPTIONS_GHC -fno-warn-orphans #-}

module Agda.Compiler.Treeless.Pretty () where

import Prelude hiding ((!!)) -- don't use partial functions!

import Control.Arrow (first)
import Control.Monad.Reader
import Data.Maybe
import qualified Data.Map as Map

import Agda.Syntax.Treeless
import Agda.Compiler.Treeless.Subst
import Agda.Utils.Pretty
import Agda.Utils.List

import Agda.Utils.Impossible

data PEnv = PEnv { PEnv -> Int
pPrec :: Int
                 , PEnv -> [String]
pFresh :: [String]
                 , PEnv -> [String]
pBound :: [String] }

type P = Reader PEnv

--UNUSED Liang-Ting Chen 2019-07-16
--withName :: (String -> P a) -> P a
--withName k = withNames 1 $ \[x] -> k x

withNames :: Int -> ([String] -> P a) -> P a
withNames :: Int -> ([String] -> P a) -> P a
withNames Int
n [String] -> P a
k = do
  ([String]
xs, [String]
ys) <- (PEnv -> ([String], [String]))
-> ReaderT PEnv Identity ([String], [String])
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((PEnv -> ([String], [String]))
 -> ReaderT PEnv Identity ([String], [String]))
-> (PEnv -> ([String], [String]))
-> ReaderT PEnv Identity ([String], [String])
forall a b. (a -> b) -> a -> b
$ Int -> [String] -> ([String], [String])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n ([String] -> ([String], [String]))
-> (PEnv -> [String]) -> PEnv -> ([String], [String])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PEnv -> [String]
pFresh
  (PEnv -> PEnv) -> P a -> P a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\ PEnv
e -> PEnv
e { pFresh :: [String]
pFresh = [String]
ys }) ([String] -> P a
k [String]
xs)

-- | Don't generate fresh names for unused variables.
withNames' :: HasFree a => Int -> a -> ([String] -> P b) -> P b
withNames' :: Int -> a -> ([String] -> P b) -> P b
withNames' Int
n a
tm [String] -> P b
k = Int -> ([String] -> P b) -> P b
forall a. Int -> ([String] -> P a) -> P a
withNames Int
n' (([String] -> P b) -> P b) -> ([String] -> P b) -> P b
forall a b. (a -> b) -> a -> b
$ [String] -> P b
k ([String] -> P b) -> ([String] -> [String]) -> [String] -> P b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> [String]
insBlanks
  where
    fv :: Map Int Occurs
fv = a -> Map Int Occurs
forall a. HasFree a => a -> Map Int Occurs
freeVars a
tm
    n' :: Int
n'  = [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n) ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ Map Int Occurs -> [Int]
forall k a. Map k a -> [k]
Map.keys Map Int Occurs
fv
    insBlanks :: [String] -> [String]
insBlanks = Int -> [String] -> [String]
go Int
n
      where
        go :: Int -> [String] -> [String]
go Int
0 [String]
_ = []
        go Int
i xs0 :: [String]
xs0@(~(String
x : [String]
xs))
          | Int -> Map Int Occurs -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Map Int Occurs
fv = String
x   String -> [String] -> [String]
forall a. a -> [a] -> [a]
: Int -> [String] -> [String]
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [String]
xs
          | Bool
otherwise             = String
"_" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: Int -> [String] -> [String]
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [String]
xs0

bindName :: String -> P a -> P a
bindName :: String -> P a -> P a
bindName String
x = (PEnv -> PEnv) -> P a -> P a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((PEnv -> PEnv) -> P a -> P a) -> (PEnv -> PEnv) -> P a -> P a
forall a b. (a -> b) -> a -> b
$ \ PEnv
e -> PEnv
e { pBound :: [String]
pBound = String
x String -> [String] -> [String]
forall a. a -> [a] -> [a]
: PEnv -> [String]
pBound PEnv
e }

bindNames :: [String] -> P a -> P a
bindNames :: [String] -> P a -> P a
bindNames [String]
xs P a
p = (String -> P a -> P a) -> P a -> [String] -> P a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr String -> P a -> P a
forall a. String -> P a -> P a
bindName P a
p [String]
xs

paren :: Int -> P Doc -> P Doc
paren :: Int -> P Doc -> P Doc
paren Int
p P Doc
doc = do
  Int
n <- (PEnv -> Int) -> ReaderT PEnv Identity Int
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks PEnv -> Int
pPrec
  (if Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n then Doc -> Doc
parens else Doc -> Doc
forall a. a -> a
id) (Doc -> Doc) -> P Doc -> P Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> P Doc
doc

prec :: Int -> P a -> P a
prec :: Int -> P a -> P a
prec Int
p = (PEnv -> PEnv) -> P a -> P a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((PEnv -> PEnv) -> P a -> P a) -> (PEnv -> PEnv) -> P a -> P a
forall a b. (a -> b) -> a -> b
$ \ PEnv
e -> PEnv
e { pPrec :: Int
pPrec = Int
p }

name :: Int -> P String
name :: Int -> P String
name Int
x = (PEnv -> String) -> P String
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks
  ((PEnv -> String) -> P String) -> (PEnv -> String) -> P String
forall a b. (a -> b) -> a -> b
$ (\ [String]
xs -> String -> [String] -> Int -> String
forall a. a -> [a] -> Int -> a
indexWithDefault String
forall a. HasCallStack => a
__IMPOSSIBLE__ [String]
xs Int
x)
  ([String] -> String) -> (PEnv -> [String]) -> PEnv -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (Integer -> String) -> [Integer] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((String
"^" String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (Integer -> String) -> Integer -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> String
forall a. Show a => a -> String
show) [Integer
1..])
  ([String] -> [String]) -> (PEnv -> [String]) -> PEnv -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PEnv -> [String]
pBound

runP :: P a -> a
runP :: P a -> a
runP P a
p = P a -> PEnv -> a
forall r a. Reader r a -> r -> a
runReader P a
p PEnv :: Int -> [String] -> [String] -> PEnv
PEnv{ pPrec :: Int
pPrec = Int
0, pFresh :: [String]
pFresh = [String]
names, pBound :: [String]
pBound = [] }
  where
    names :: [String]
names = [ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
i | String
i <- String
"" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (Integer -> String) -> [Integer] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> String
forall a. Show a => a -> String
show [Integer
1..], String
x <- (Char -> String) -> String -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Char -> String -> String
forall a. a -> [a] -> [a]
:[]) [Char
'a'..Char
'z'] ]

instance Pretty TTerm where
  prettyPrec :: Int -> TTerm -> Doc
prettyPrec Int
p TTerm
t = P Doc -> Doc
forall a. P a -> a
runP (P Doc -> Doc) -> P Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> P Doc -> P Doc
forall a. Int -> P a -> P a
prec Int
p (TTerm -> P Doc
pTerm TTerm
t)

opName :: TPrim -> String
opName :: TPrim -> String
opName TPrim
PAdd = String
"+"
opName TPrim
PSub = String
"-"
opName TPrim
PMul = String
"*"
opName TPrim
PQuot = String
"quot"
opName TPrim
PRem = String
"rem"
opName TPrim
PGeq = String
">="
opName TPrim
PLt  = String
"<"
opName TPrim
PEqI = String
"==I"
opName TPrim
PAdd64 = String
"+64"
opName TPrim
PSub64 = String
"-64"
opName TPrim
PMul64 = String
"*64"
opName TPrim
PQuot64 = String
"quot64"
opName TPrim
PRem64 = String
"rem64"
opName TPrim
PLt64  = String
"<64"
opName TPrim
PEq64 = String
"==64"
opName TPrim
PEqF = String
"==F"
opName TPrim
PEqS = String
"==S"
opName TPrim
PEqC = String
"==C"
opName TPrim
PEqQ = String
"==Q"
opName TPrim
PIf  = String
"if_then_else_"
opName TPrim
PSeq = String
"seq"
opName TPrim
PITo64 = String
"toWord64"
opName TPrim
P64ToI = String
"fromWord64"


isInfix :: TPrim -> Maybe (Int, Int, Int)
isInfix :: TPrim -> Maybe (Int, Int, Int)
isInfix TPrim
op =
  case TPrim
op of
    TPrim
PMul -> Int -> Maybe (Int, Int, Int)
forall c. Num c => c -> Maybe (c, c, c)
l Int
7
    TPrim
PAdd -> Int -> Maybe (Int, Int, Int)
forall c. Num c => c -> Maybe (c, c, c)
l Int
6
    TPrim
PSub -> Int -> Maybe (Int, Int, Int)
forall c. Num c => c -> Maybe (c, c, c)
l Int
6
    TPrim
PGeq -> Int -> Maybe (Int, Int, Int)
forall c. Num c => c -> Maybe (c, c, c)
non Int
4
    TPrim
PLt  -> Int -> Maybe (Int, Int, Int)
forall c. Num c => c -> Maybe (c, c, c)
non Int
4
    TPrim
PMul64 -> Int -> Maybe (Int, Int, Int)
forall c. Num c => c -> Maybe (c, c, c)
l Int
7
    TPrim
PAdd64 -> Int -> Maybe (Int, Int, Int)
forall c. Num c => c -> Maybe (c, c, c)
l Int
6
    TPrim
PSub64 -> Int -> Maybe (Int, Int, Int)
forall c. Num c => c -> Maybe (c, c, c)
l Int
6
    TPrim
PLt64  -> Int -> Maybe (Int, Int, Int)
forall c. Num c => c -> Maybe (c, c, c)
non Int
4
    TPrim
p | TPrim -> Bool
isPrimEq TPrim
p -> Int -> Maybe (Int, Int, Int)
forall c. Num c => c -> Maybe (c, c, c)
non Int
4
    TPrim
_    -> Maybe (Int, Int, Int)
forall a. Maybe a
Nothing
  where
    l :: c -> Maybe (c, c, c)
l c
n   = (c, c, c) -> Maybe (c, c, c)
forall a. a -> Maybe a
Just (c
n, c
n, c
n c -> c -> c
forall a. Num a => a -> a -> a
+ c
1)
    r :: c -> Maybe (c, c, c)
r c
n   = (c, c, c) -> Maybe (c, c, c)
forall a. a -> Maybe a
Just (c
n, c
n c -> c -> c
forall a. Num a => a -> a -> a
+ c
1, c
n) -- NB:: Defined but not used
    non :: c -> Maybe (c, c, c)
non c
n = (c, c, c) -> Maybe (c, c, c)
forall a. a -> Maybe a
Just (c
n, c
n c -> c -> c
forall a. Num a => a -> a -> a
+ c
1, c
n c -> c -> c
forall a. Num a => a -> a -> a
+ c
1)

pTerm' :: Int -> TTerm -> P Doc
pTerm' :: Int -> TTerm -> P Doc
pTerm' Int
p = Int -> P Doc -> P Doc
forall a. Int -> P a -> P a
prec Int
p (P Doc -> P Doc) -> (TTerm -> P Doc) -> TTerm -> P Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TTerm -> P Doc
pTerm

pTerm :: TTerm -> P Doc
pTerm :: TTerm -> P Doc
pTerm = \case
  TVar Int
x -> String -> Doc
text (String -> Doc) -> P String -> P Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> P String
name Int
x
  TApp (TPrim TPrim
op) [TTerm
a, TTerm
b] | Just (Int
c, Int
l, Int
r) <- TPrim -> Maybe (Int, Int, Int)
isInfix TPrim
op ->
    Int -> P Doc -> P Doc
paren Int
c (P Doc -> P Doc) -> P Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep ([Doc] -> Doc) -> ReaderT PEnv Identity [Doc] -> P Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [P Doc] -> ReaderT PEnv Identity [Doc]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ Int -> TTerm -> P Doc
pTerm' Int
l TTerm
a
                               , Doc -> P Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> P Doc) -> Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ TPrim -> String
opName TPrim
op
                               , Int -> TTerm -> P Doc
pTerm' Int
r TTerm
b ]
  TApp (TPrim TPrim
PIf) [TTerm
a, TTerm
b, TTerm
c] ->
    Int -> P Doc -> P Doc
paren Int
0 (P Doc -> P Doc) -> P Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ (\ Doc
a Doc
b Doc
c -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Doc
"if" Doc -> Doc -> Doc
<+> Doc
a
                              , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"then" Doc -> Doc -> Doc
<+> Doc
b
                              , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"else" Doc -> Doc -> Doc
<+> Doc
c ])
              (Doc -> Doc -> Doc -> Doc)
-> P Doc -> ReaderT PEnv Identity (Doc -> Doc -> Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TTerm -> P Doc
pTerm' Int
0 TTerm
a
              ReaderT PEnv Identity (Doc -> Doc -> Doc)
-> P Doc -> ReaderT PEnv Identity (Doc -> Doc)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> TTerm -> P Doc
pTerm' Int
0 TTerm
b
              ReaderT PEnv Identity (Doc -> Doc) -> P Doc -> P Doc
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TTerm -> P Doc
pTerm TTerm
c
  TDef QName
f -> Doc -> P Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> P Doc) -> Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
f
  TCon QName
c -> Doc -> P Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> P Doc) -> Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
c
  TLit Literal
l -> Doc -> P Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> P Doc) -> Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ Literal -> Doc
forall a. Pretty a => a -> Doc
pretty Literal
l
  TPrim TPrim
op | Maybe (Int, Int, Int) -> Bool
forall a. Maybe a -> Bool
isJust (TPrim -> Maybe (Int, Int, Int)
isInfix TPrim
op) -> Doc -> P Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> P Doc) -> Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text (String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ TPrim -> String
opName TPrim
op String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_")
           | Bool
otherwise -> Doc -> P Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> P Doc) -> Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text (TPrim -> String
opName TPrim
op)
  TApp TTerm
f [TTerm]
es ->
    Int -> P Doc -> P Doc
paren Int
9 (P Doc -> P Doc) -> P Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ (\Doc
a [Doc]
bs -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [Doc
a, Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep [Doc]
bs])
              (Doc -> [Doc] -> Doc)
-> P Doc -> ReaderT PEnv Identity ([Doc] -> Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TTerm -> P Doc
pTerm' Int
9 TTerm
f
              ReaderT PEnv Identity ([Doc] -> Doc)
-> ReaderT PEnv Identity [Doc] -> P Doc
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (TTerm -> P Doc) -> [TTerm] -> ReaderT PEnv Identity [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Int -> TTerm -> P Doc
pTerm' Int
10) [TTerm]
es
  t :: TTerm
t@TLam{} -> Int -> P Doc -> P Doc
paren Int
0 (P Doc -> P Doc) -> P Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ Int -> TTerm -> ([String] -> P Doc) -> P Doc
forall a b. HasFree a => Int -> a -> ([String] -> P b) -> P b
withNames' Int
n TTerm
b (([String] -> P Doc) -> P Doc) -> ([String] -> P Doc) -> P Doc
forall a b. (a -> b) -> a -> b
$ \ [String]
xs -> [String] -> P Doc -> P Doc
forall a. [String] -> P a -> P a
bindNames [String]
xs (P Doc -> P Doc) -> P Doc -> P Doc
forall a b. (a -> b) -> a -> b
$
    (\Doc
b -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ String -> Doc
text (String
"λ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
xs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" →")
               , Int -> Doc -> Doc
nest Int
2 Doc
b ]) (Doc -> Doc) -> P Doc -> P Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TTerm -> P Doc
pTerm' Int
0 TTerm
b
    where
      (Int
n, TTerm
b) = TTerm -> (Int, TTerm)
tLamView TTerm
t
  t :: TTerm
t@TLet{} -> Int -> P Doc -> P Doc
paren Int
0 (P Doc -> P Doc) -> P Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ Int -> ([String] -> P Doc) -> P Doc
forall a. Int -> ([String] -> P a) -> P a
withNames ([TTerm] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TTerm]
es) (([String] -> P Doc) -> P Doc) -> ([String] -> P Doc) -> P Doc
forall a b. (a -> b) -> a -> b
$ \ [String]
xs ->
    (\ ([(String, Doc)]
binds, Doc
b) -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Doc
"let" Doc -> Doc -> Doc
<+> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat [ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ String -> Doc
text String
x Doc -> Doc -> Doc
<+> Doc
"="
                                                , Int -> Doc -> Doc
nest Int
2 Doc
e ] | (String
x, Doc
e) <- [(String, Doc)]
binds ]
                              Doc -> Doc -> Doc
<+> Doc
"in", Doc
b ])
      (([(String, Doc)], Doc) -> Doc)
-> ReaderT PEnv Identity ([(String, Doc)], Doc) -> P Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(String, TTerm)]
-> TTerm -> ReaderT PEnv Identity ([(String, Doc)], Doc)
pLets ([String] -> [TTerm] -> [(String, TTerm)]
forall a b. [a] -> [b] -> [(a, b)]
zip [String]
xs [TTerm]
es) TTerm
b
    where
      ([TTerm]
es, TTerm
b) = TTerm -> ([TTerm], TTerm)
tLetView TTerm
t

      pLets :: [(String, TTerm)]
-> TTerm -> ReaderT PEnv Identity ([(String, Doc)], Doc)
pLets [] TTerm
b = ([],) (Doc -> ([(String, Doc)], Doc))
-> P Doc -> ReaderT PEnv Identity ([(String, Doc)], Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TTerm -> P Doc
pTerm' Int
0 TTerm
b
      pLets ((String
x, TTerm
e) : [(String, TTerm)]
bs) TTerm
b = do
        Doc
e <- Int -> TTerm -> P Doc
pTerm' Int
0 TTerm
e
        ([(String, Doc)] -> [(String, Doc)])
-> ([(String, Doc)], Doc) -> ([(String, Doc)], Doc)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ((String
x, Doc
e) (String, Doc) -> [(String, Doc)] -> [(String, Doc)]
forall a. a -> [a] -> [a]
:) (([(String, Doc)], Doc) -> ([(String, Doc)], Doc))
-> ReaderT PEnv Identity ([(String, Doc)], Doc)
-> ReaderT PEnv Identity ([(String, Doc)], Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String
-> ReaderT PEnv Identity ([(String, Doc)], Doc)
-> ReaderT PEnv Identity ([(String, Doc)], Doc)
forall a. String -> P a -> P a
bindName String
x ([(String, TTerm)]
-> TTerm -> ReaderT PEnv Identity ([(String, Doc)], Doc)
pLets [(String, TTerm)]
bs TTerm
b)

  TCase Int
x CaseInfo
_ TTerm
def [TAlt]
alts -> Int -> P Doc -> P Doc
paren Int
0 (P Doc -> P Doc) -> P Doc -> P Doc
forall a b. (a -> b) -> a -> b
$
    (\ Doc
sc [Doc]
alts Doc
defd ->
      [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Doc
"case" Doc -> Doc -> Doc
<+> Doc
sc Doc -> Doc -> Doc
<+> Doc
"of"
          , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc]
alts [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [ Doc
"_ →" Doc -> Doc -> Doc
<+> Doc
defd | [Doc] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc]
alts Bool -> Bool -> Bool
|| TTerm
def TTerm -> TTerm -> Bool
forall a. Eq a => a -> a -> Bool
/= TError -> TTerm
TError TError
TUnreachable ]) ]
    ) (Doc -> [Doc] -> Doc -> Doc)
-> P Doc -> ReaderT PEnv Identity ([Doc] -> Doc -> Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TTerm -> P Doc
pTerm' Int
0 (Int -> TTerm
TVar Int
x)
      ReaderT PEnv Identity ([Doc] -> Doc -> Doc)
-> ReaderT PEnv Identity [Doc]
-> ReaderT PEnv Identity (Doc -> Doc)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (TAlt -> P Doc) -> [TAlt] -> ReaderT PEnv Identity [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TAlt -> P Doc
pAlt [TAlt]
alts
      ReaderT PEnv Identity (Doc -> Doc) -> P Doc -> P Doc
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> TTerm -> P Doc
pTerm' Int
0 TTerm
def
    where
      pAlt :: TAlt -> P Doc
pAlt (TALit Literal
l TTerm
b) = Doc -> Doc -> Doc
pAlt' (Doc -> Doc -> Doc) -> P Doc -> ReaderT PEnv Identity (Doc -> Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TTerm -> P Doc
pTerm' Int
0 (Literal -> TTerm
TLit Literal
l) ReaderT PEnv Identity (Doc -> Doc) -> P Doc -> P Doc
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> TTerm -> P Doc
pTerm' Int
0 TTerm
b
      pAlt (TAGuard TTerm
g TTerm
b) =
        Doc -> Doc -> Doc
pAlt' (Doc -> Doc -> Doc) -> P Doc -> ReaderT PEnv Identity (Doc -> Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Doc
"_" Doc -> Doc -> Doc
<+> Doc
"|" Doc -> Doc -> Doc
<+>) (Doc -> Doc) -> P Doc -> P Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TTerm -> P Doc
pTerm' Int
0 TTerm
g)
              ReaderT PEnv Identity (Doc -> Doc) -> P Doc -> P Doc
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Int -> TTerm -> P Doc
pTerm' Int
0 TTerm
b)
      pAlt (TACon QName
c Int
a TTerm
b) =
        Int -> TTerm -> ([String] -> P Doc) -> P Doc
forall a b. HasFree a => Int -> a -> ([String] -> P b) -> P b
withNames' Int
a TTerm
b (([String] -> P Doc) -> P Doc) -> ([String] -> P Doc) -> P Doc
forall a b. (a -> b) -> a -> b
$ \ [String]
xs -> [String] -> P Doc -> P Doc
forall a. [String] -> P a -> P a
bindNames [String]
xs (P Doc -> P Doc) -> P Doc -> P Doc
forall a b. (a -> b) -> a -> b
$
        Doc -> Doc -> Doc
pAlt' (Doc -> Doc -> Doc) -> P Doc -> ReaderT PEnv Identity (Doc -> Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TTerm -> P Doc
pTerm' Int
0 (TTerm -> [TTerm] -> TTerm
TApp (QName -> TTerm
TCon QName
c) [Int -> TTerm
TVar Int
i | Int
i <- [Int] -> [Int]
forall a. [a] -> [a]
reverse [Int
0..Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]])
              ReaderT PEnv Identity (Doc -> Doc) -> P Doc -> P Doc
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> TTerm -> P Doc
pTerm' Int
0 TTerm
b
      pAlt' :: Doc -> Doc -> Doc
pAlt' Doc
p Doc
b = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [Doc
p Doc -> Doc -> Doc
<+> Doc
"→", Int -> Doc -> Doc
nest Int
2 Doc
b]

  TTerm
TUnit -> Doc -> P Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
"()"
  TTerm
TSort -> Doc -> P Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
"Set"
  TTerm
TErased -> Doc -> P Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
"_"
  TError TError
err -> Int -> P Doc -> P Doc
paren Int
9 (P Doc -> P Doc) -> P Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ Doc -> P Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> P Doc) -> Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ Doc
"error" Doc -> Doc -> Doc
<+> String -> Doc
text (String -> String
forall a. Show a => a -> String
show (TError -> String
forall a. Show a => a -> String
show TError
err))
  TCoerce TTerm
t -> Int -> P Doc -> P Doc
paren Int
9 (P Doc -> P Doc) -> P Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ (Doc
"coe" Doc -> Doc -> Doc
<+>) (Doc -> Doc) -> P Doc -> P Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TTerm -> P Doc
pTerm' Int
10 TTerm
t