{-# 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 n :: Int
n k :: [String] -> P a
k = do
  (xs :: [String]
xs, ys :: [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 (\ e :: 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' n :: Int
n tm :: a
tm k :: [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]
forall a. IsString a => Int -> [a] -> [a]
go Int
n
      where
        go :: Int -> [a] -> [a]
go 0 _ = []
        go i :: Int
i xs0 :: [a]
xs0@(~(x :: a
x : xs :: [a]
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
- 1) Map Int Occurs
fv = a
x   a -> [a] -> [a]
forall a. a -> [a] -> [a]
: Int -> [a] -> [a]
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) [a]
xs
          | Bool
otherwise             = "_" a -> [a] -> [a]
forall a. a -> [a] -> [a]
: Int -> [a] -> [a]
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) [a]
xs0

bindName :: String -> P a -> P a
bindName :: String -> P a -> P a
bindName x :: 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
$ \ e :: 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 xs :: [String]
xs p :: 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 p :: Int
p doc :: 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 p :: 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
$ \ e :: PEnv
e -> PEnv
e { pPrec :: Int
pPrec = Int
p }

name :: Int -> P String
name :: Int -> P String
name x :: 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
$ (\ xs :: [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
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) [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 :: 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 = 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]
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 [1..], String
x <- (Char -> String) -> String -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Char -> String -> String
forall a. a -> [a] -> [a]
:[]) ['a'..'z'] ]

instance Pretty TTerm where
  prettyPrec :: Int -> TTerm -> Doc
prettyPrec p :: Int
p t :: 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 PAdd = "+"
opName PSub = "-"
opName PMul = "*"
opName PQuot = "quot"
opName PRem = "rem"
opName PGeq = ">="
opName PLt  = "<"
opName PEqI = "==I"
opName PAdd64 = "+64"
opName PSub64 = "-64"
opName PMul64 = "*64"
opName PQuot64 = "quot64"
opName PRem64 = "rem64"
opName PLt64  = "<64"
opName PEq64 = "==64"
opName PEqF = "==F"
opName PEqS = "==S"
opName PEqC = "==C"
opName PEqQ = "==Q"
opName PIf  = "if_then_else_"
opName PSeq = "seq"
opName PITo64 = "toWord64"
opName P64ToI = "fromWord64"


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

pTerm' :: Int -> TTerm -> P Doc
pTerm' :: Int -> TTerm -> P Doc
pTerm' p :: 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 t :: TTerm
t = case TTerm
t of
  TVar x :: 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 op :: TPrim
op) [a :: TTerm
a, b :: TTerm
b] | Just (c :: Int
c, l :: Int
l, r :: 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
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 PIf) [a :: TTerm
a, b :: TTerm
b, c :: TTerm
c] ->
    Int -> P Doc -> P Doc
paren 0 (P Doc -> P Doc) -> P Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ (\ a :: Doc
a b :: Doc
b c :: Doc
c -> [Doc] -> Doc
sep [ "if" Doc -> Doc -> Doc
<+> Doc
a
                              , Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ "then" Doc -> Doc -> Doc
<+> Doc
b
                              , Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ "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' 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' 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 f :: 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 c :: 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 l :: 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 op :: 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
forall a. [a] -> [a] -> [a]
++ TPrim -> String
opName TPrim
op String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_")
           | 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 f :: TTerm
f es :: [TTerm]
es ->
    Int -> P Doc -> P Doc
paren 9 (P Doc -> P Doc) -> P Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ (\a :: Doc
a bs :: [Doc]
bs -> [Doc] -> Doc
sep [Doc
a, Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [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' 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' 10) [TTerm]
es
  TLam _ -> Int -> P Doc -> P Doc
paren 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
$ \ xs :: [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
$
    (\b :: Doc
b -> [Doc] -> Doc
sep [ String -> Doc
text ("λ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
xs String -> String -> String
forall a. [a] -> [a] -> [a]
++ " →")
               , Int -> Doc -> Doc
nest 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' 0 TTerm
b
    where
      (n :: Int
n, b :: TTerm
b) = TTerm -> (Int, TTerm)
tLamView TTerm
t
  TLet{} -> Int -> P Doc -> P Doc
paren 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
$ \ xs :: [String]
xs ->
    (\ (binds :: [(String, Doc)]
binds, b :: Doc
b) -> [Doc] -> Doc
sep [ "let" Doc -> Doc -> Doc
<+> [Doc] -> Doc
vcat [ [Doc] -> Doc
sep [ String -> Doc
text String
x Doc -> Doc -> Doc
<+> "="
                                                , Int -> Doc -> Doc
nest 2 Doc
e ] | (x :: String
x, e :: Doc
e) <- [(String, Doc)]
binds ]
                              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
      (es :: [TTerm]
es, b :: TTerm
b) = TTerm -> ([TTerm], TTerm)
tLetView TTerm
t

      pLets :: [(String, TTerm)]
-> TTerm -> ReaderT PEnv Identity ([(String, Doc)], Doc)
pLets [] b :: 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' 0 TTerm
b
      pLets ((x :: String
x, e :: TTerm
e) : bs :: [(String, TTerm)]
bs) b :: TTerm
b = do
        Doc
e <- Int -> TTerm -> P Doc
pTerm' 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 x :: Int
x _ def :: TTerm
def alts :: [TAlt]
alts -> Int -> P Doc -> P Doc
paren 0 (P Doc -> P Doc) -> P Doc -> P Doc
forall a b. (a -> b) -> a -> b
$
    (\ sc :: Doc
sc alts :: [Doc]
alts defd :: Doc
defd ->
      [Doc] -> Doc
sep [ "case" Doc -> Doc -> Doc
<+> Doc
sc Doc -> Doc -> Doc
<+> "of"
          , Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat ([Doc]
alts [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [ "_ →" 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' 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' 0 TTerm
def
    where
      pAlt :: TAlt -> P Doc
pAlt (TALit l :: Literal
l b :: 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' 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' 0 TTerm
b
      pAlt (TAGuard g :: TTerm
g b :: 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) -> P Doc -> P Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TTerm -> P Doc
pTerm' 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' 0 TTerm
b)
      pAlt (TACon c :: QName
c a :: Int
a b :: 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
$ \ xs :: [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' 0 (TTerm -> [TTerm] -> TTerm
TApp (QName -> TTerm
TCon QName
c) [Int -> TTerm
TVar Int
i | Int
i <- [Int] -> [Int]
forall a. [a] -> [a]
reverse [0..Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
- 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' 0 TTerm
b
      pAlt' :: Doc -> Doc -> Doc
pAlt' p :: Doc
p b :: Doc
b = [Doc] -> Doc
sep [Doc
p Doc -> Doc -> Doc
<+> "→", Int -> Doc -> Doc
nest 2 Doc
b]

  TUnit -> Doc -> P Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure "()"
  TSort -> Doc -> P Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure "Set"
  TErased -> Doc -> P Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure "_"
  TError err :: TError
err -> Int -> P Doc -> P Doc
paren 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
$ "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 t :: TTerm
t -> Int -> P Doc -> P Doc
paren 9 (P Doc -> P Doc) -> P Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ ("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' 10 TTerm
t