    {-# 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 :: Int -> [[Char]] -> [[Char]] -> PEnv
    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