{-# 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 -> [[Char]]
pFresh :: [String]
                 , PEnv -> [[Char]]
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 :: forall a. Int -> ([[Char]] -> P a) -> P a
withNames Int
n [[Char]] -> P a
k = do
  ([[Char]]
xs, [[Char]]
ys) <- (PEnv -> ([[Char]], [[Char]]))
-> ReaderT PEnv Identity ([[Char]], [[Char]])
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((PEnv -> ([[Char]], [[Char]]))
 -> ReaderT PEnv Identity ([[Char]], [[Char]]))
-> (PEnv -> ([[Char]], [[Char]]))
-> ReaderT PEnv Identity ([[Char]], [[Char]])
forall a b. (a -> b) -> a -> b
$ Int -> [[Char]] -> ([[Char]], [[Char]])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n ([[Char]] -> ([[Char]], [[Char]]))
-> (PEnv -> [[Char]]) -> PEnv -> ([[Char]], [[Char]])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PEnv -> [[Char]]
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 :: [[Char]]
pFresh = [[Char]]
ys }) ([[Char]] -> P a
k [[Char]]
xs)

-- | Don't generate fresh names for unused variables.
withNames' :: HasFree a => Int -> a -> ([String] -> P b) -> P b
withNames' :: forall a b. HasFree a => Int -> a -> ([[Char]] -> P b) -> P b
withNames' Int
n a
tm [[Char]] -> P b
k = Int -> ([[Char]] -> P b) -> P b
forall a. Int -> ([[Char]] -> P a) -> P a
withNames Int
n' (([[Char]] -> P b) -> P b) -> ([[Char]] -> P b) -> P b
forall a b. (a -> b) -> a -> b
$ [[Char]] -> P b
k ([[Char]] -> P b) -> ([[Char]] -> [[Char]]) -> [[Char]] -> P b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Char]] -> [[Char]]
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 :: [[Char]] -> [[Char]]
insBlanks = Int -> [[Char]] -> [[Char]]
go Int
n
      where
        go :: Int -> [[Char]] -> [[Char]]
go Int
0 [[Char]]
_ = []
        go Int
i xs0 :: [[Char]]
xs0@(~([Char]
x : [[Char]]
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 = [Char]
x   [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: Int -> [[Char]] -> [[Char]]
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [[Char]]
xs
          | Bool
otherwise             = [Char]
"_" [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: Int -> [[Char]] -> [[Char]]
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [[Char]]
xs0

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

bindNames :: [String] -> P a -> P a
bindNames :: forall a. [[Char]] -> P a -> P a
bindNames [[Char]]
xs P a
p = ([Char] -> P a -> P a) -> P a -> [[Char]] -> P a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr [Char] -> P a -> P a
forall a. [Char] -> P a -> P a
bindName P a
p [[Char]]
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 :: forall a. Int -> P a -> P a
prec Int
p = (PEnv -> PEnv)
-> ReaderT PEnv Identity a -> ReaderT PEnv Identity a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((PEnv -> PEnv)
 -> ReaderT PEnv Identity a -> ReaderT PEnv Identity a)
-> (PEnv -> PEnv)
-> ReaderT PEnv Identity a
-> ReaderT PEnv Identity a
forall a b. (a -> b) -> a -> b
$ \ PEnv
e -> PEnv
e { pPrec :: Int
pPrec = Int
p }

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

runP :: P a -> a
runP :: forall a. P a -> a
runP P a
p = P a -> PEnv -> a
forall r a. Reader r a -> r -> a
runReader P a
p PEnv{ pPrec :: Int
pPrec = Int
0, pFresh :: [[Char]]
pFresh = [[Char]]
names, pBound :: [[Char]]
pBound = [] }
  where
    names :: [[Char]]
names = [ [Char]
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
i | [Char]
i <- [Char]
"" [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: (Integer -> [Char]) -> [Integer] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> [Char]
forall a. Show a => a -> [Char]
show [Integer
1..], [Char]
x <- (Char -> [Char]) -> [Char] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (Char -> [Char] -> [Char]
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 -> [Char]
opName TPrim
PAdd = [Char]
"+"
opName TPrim
PSub = [Char]
"-"
opName TPrim
PMul = [Char]
"*"
opName TPrim
PQuot = [Char]
"quot"
opName TPrim
PRem = [Char]
"rem"
opName TPrim
PGeq = [Char]
">="
opName TPrim
PLt  = [Char]
"<"
opName TPrim
PEqI = [Char]
"==I"
opName TPrim
PAdd64 = [Char]
"+64"
opName TPrim
PSub64 = [Char]
"-64"
opName TPrim
PMul64 = [Char]
"*64"
opName TPrim
PQuot64 = [Char]
"quot64"
opName TPrim
PRem64 = [Char]
"rem64"
opName TPrim
PLt64  = [Char]
"<64"
opName TPrim
PEq64 = [Char]
"==64"
opName TPrim
PEqF = [Char]
"==F"
opName TPrim
PEqS = [Char]
"==S"
opName TPrim
PEqC = [Char]
"==C"
opName TPrim
PEqQ = [Char]
"==Q"
opName TPrim
PIf  = [Char]
"if_then_else_"
opName TPrim
PSeq = [Char]
"seq"
opName TPrim
PITo64 = [Char]
"toWord64"
opName TPrim
P64ToI = [Char]
"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 -> [Char] -> Doc
text ([Char] -> Doc) -> P [Char] -> P Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> P [Char]
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
$ [Char] -> Doc
text ([Char] -> Doc) -> [Char] -> Doc
forall a b. (a -> b) -> a -> b
$ TPrim -> [Char]
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
$ [Char] -> Doc
text ([Char]
"_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TPrim -> [Char]
opName TPrim
op [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"_")
           | 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
$ [Char] -> Doc
text (TPrim -> [Char]
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 -> ([[Char]] -> P Doc) -> P Doc
forall a b. HasFree a => Int -> a -> ([[Char]] -> P b) -> P b
withNames' Int
n TTerm
b (([[Char]] -> P Doc) -> P Doc) -> ([[Char]] -> P Doc) -> P Doc
forall a b. (a -> b) -> a -> b
$ \ [[Char]]
xs -> [[Char]] -> P Doc -> P Doc
forall a. [[Char]] -> P a -> P a
bindNames [[Char]]
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 [ [Char] -> Doc
text ([Char]
"λ " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [[Char]] -> [Char]
unwords [[Char]]
xs [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" →")
               , 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 -> ([[Char]] -> P Doc) -> P Doc
forall a. Int -> ([[Char]] -> P a) -> P a
withNames ([TTerm] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TTerm]
es) (([[Char]] -> P Doc) -> P Doc) -> ([[Char]] -> P Doc) -> P Doc
forall a b. (a -> b) -> a -> b
$ \ [[Char]]
xs ->
    (\ ([([Char], 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 [ [Char] -> Doc
text [Char]
x Doc -> Doc -> Doc
<+> Doc
"="
                                                , Int -> Doc -> Doc
nest Int
2 Doc
e ] | ([Char]
x, Doc
e) <- [([Char], Doc)]
binds ]
                              Doc -> Doc -> Doc
<+> Doc
"in", Doc
b ])
      (([([Char], Doc)], Doc) -> Doc)
-> ReaderT PEnv Identity ([([Char], Doc)], Doc) -> P Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [([Char], TTerm)]
-> TTerm -> ReaderT PEnv Identity ([([Char], Doc)], Doc)
pLets ([[Char]] -> [TTerm] -> [([Char], TTerm)]
forall a b. [a] -> [b] -> [(a, b)]
zip [[Char]]
xs [TTerm]
es) TTerm
b
    where
      ([TTerm]
es, TTerm
b) = TTerm -> ([TTerm], TTerm)
tLetView TTerm
t

      pLets :: [([Char], TTerm)]
-> TTerm -> ReaderT PEnv Identity ([([Char], Doc)], Doc)
pLets [] TTerm
b = ([],) (Doc -> ([([Char], Doc)], Doc))
-> P Doc -> ReaderT PEnv Identity ([([Char], Doc)], Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TTerm -> P Doc
pTerm' Int
0 TTerm
b
      pLets (([Char]
x, TTerm
e) : [([Char], TTerm)]
bs) TTerm
b = do
        Doc
e <- Int -> TTerm -> P Doc
pTerm' Int
0 TTerm
e
        ([([Char], Doc)] -> [([Char], Doc)])
-> ([([Char], Doc)], Doc) -> ([([Char], Doc)], Doc)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (([Char]
x, Doc
e) ([Char], Doc) -> [([Char], Doc)] -> [([Char], Doc)]
forall a. a -> [a] -> [a]
:) (([([Char], Doc)], Doc) -> ([([Char], Doc)], Doc))
-> ReaderT PEnv Identity ([([Char], Doc)], Doc)
-> ReaderT PEnv Identity ([([Char], Doc)], Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char]
-> ReaderT PEnv Identity ([([Char], Doc)], Doc)
-> ReaderT PEnv Identity ([([Char], Doc)], Doc)
forall a. [Char] -> P a -> P a
bindName [Char]
x ([([Char], TTerm)]
-> TTerm -> ReaderT PEnv Identity ([([Char], Doc)], Doc)
pLets [([Char], 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 -> ([[Char]] -> P Doc) -> P Doc
forall a b. HasFree a => Int -> a -> ([[Char]] -> P b) -> P b
withNames' Int
a TTerm
b (([[Char]] -> P Doc) -> P Doc) -> ([[Char]] -> P Doc) -> P Doc
forall a b. (a -> b) -> a -> b
$ \ [[Char]]
xs -> [[Char]] -> P Doc -> P Doc
forall a. [[Char]] -> P a -> P a
bindNames [[Char]]
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
<+> [Char] -> Doc
text ([Char] -> [Char]
forall a. Show a => a -> [Char]
show (TError -> [Char]
forall a. Show a => a -> [Char]
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