    {-# OPTIONS_GHC -Wunused-imports #-}

    {-# 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.IntMap as IntMap

    import Agda.Syntax.Treeless
    import Agda.Syntax.Common.Pretty

    import Agda.Compiler.Treeless.Subst

    import Agda.Utils.Impossible
    import Agda.Utils.Function
    import Agda.Utils.List

    instance Pretty Compiled where
      pretty :: Compiled -> Doc Aspects
    pretty Compiled {TTerm
    cTreeless :: TTerm
    cTreeless :: Compiled -> TTerm
    cTreeless, Maybe [ArgUsage]
    cArgUsage :: Maybe [ArgUsage]
    cArgUsage :: Compiled -> Maybe [ArgUsage]
    cArgUsage} =
        Doc Aspects
    "Compiled {" Doc Aspects -> Doc Aspects -> Doc Aspects
    <?> [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    vcat
          [ Doc Aspects
    "cTreeless   =" Doc Aspects -> Doc Aspects -> Doc Aspects
    <?> TTerm -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty TTerm
    cTreeless
          , Doc Aspects
    "funCompiled =" Doc Aspects -> Doc Aspects -> Doc Aspects
    <?> Maybe [ArgUsage] -> Doc Aspects
    forall a. Show a => a -> Doc Aspects
    pshow Maybe [ArgUsage]
    cArgUsage
          ] Doc Aspects -> Doc Aspects -> Doc Aspects
    <?> Doc Aspects
    "}"

    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
      (xs, 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
      local (\ PEnv
    e -> PEnv
    e { pFresh = ys }) (k 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 :: IntMap Occurs
    fv = a -> IntMap Occurs
    forall a. HasFree a => a -> IntMap Occurs
    freeVars a
    tm
        n' :: Int
    n'  = [Int] -> Int
    forall a. [a] -> 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
    $ IntMap Occurs -> [Int]
    forall a. IntMap a -> [Int]
    IntMap.keys IntMap 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 -> IntMap Occurs -> Bool
    forall a. Int -> IntMap a -> Bool
    IntMap.member (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) IntMap 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 a.
    (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 = x : pBound 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 a b. (a -> b -> b) -> b -> [a] -> b
    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 Aspects) -> P (Doc Aspects)
    paren Int
    p P (Doc Aspects)
    doc = do
      n <- (PEnv -> Int) -> ReaderT PEnv Identity Int
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks PEnv -> Int
    pPrec
      applyWhen (p < n) parens <$> 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 a.
    (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 = 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 Aspects
    prettyPrec Int
    p TTerm
    t = P (Doc Aspects) -> Doc Aspects
    forall a. P a -> a
    runP (P (Doc Aspects) -> Doc Aspects) -> P (Doc Aspects) -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ Int -> P (Doc Aspects) -> P (Doc Aspects)
    forall a. Int -> P a -> P a
    prec Int
    p (TTerm -> P (Doc Aspects)
    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 Aspects)
    pTerm' Int
    p = Int -> P (Doc Aspects) -> P (Doc Aspects)
    forall a. Int -> P a -> P a
    prec Int
    p (P (Doc Aspects) -> P (Doc Aspects))
    -> (TTerm -> P (Doc Aspects)) -> TTerm -> P (Doc Aspects)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TTerm -> P (Doc Aspects)
    pTerm

    pTerm :: TTerm -> P Doc
    pTerm :: TTerm -> P (Doc Aspects)
    pTerm = \case
      TVar Int
    x -> [Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text ([Char] -> Doc Aspects) -> P [Char] -> P (Doc Aspects)
    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 Aspects) -> P (Doc Aspects)
    paren Int
    c (P (Doc Aspects) -> P (Doc Aspects))
    -> P (Doc Aspects) -> P (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    sep ([Doc Aspects] -> Doc Aspects)
    -> ReaderT PEnv Identity [Doc Aspects] -> P (Doc Aspects)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [P (Doc Aspects)] -> ReaderT PEnv Identity [Doc Aspects]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a. Monad m => [m a] -> m [a]
    sequence [ Int -> TTerm -> P (Doc Aspects)
    pTerm' Int
    l TTerm
    a
                                   , Doc Aspects -> P (Doc Aspects)
    forall a. a -> ReaderT PEnv Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Doc Aspects -> P (Doc Aspects)) -> Doc Aspects -> P (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text ([Char] -> Doc Aspects) -> [Char] -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ TPrim -> [Char]
    opName TPrim
    op
                                   , Int -> TTerm -> P (Doc Aspects)
    pTerm' Int
    r TTerm
    b ]
      TApp (TPrim TPrim
    PIf) [TTerm
    a, TTerm
    b, TTerm
    c] ->
        Int -> P (Doc Aspects) -> P (Doc Aspects)
    paren Int
    0 (P (Doc Aspects) -> P (Doc Aspects))
    -> P (Doc Aspects) -> P (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ (\ Doc Aspects
    a Doc Aspects
    b Doc Aspects
    c -> [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    sep [ Doc Aspects
    "if" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    a
                                  , Int -> Doc Aspects -> Doc Aspects
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ Doc Aspects
    "then" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    b
                                  , Int -> Doc Aspects -> Doc Aspects
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ Doc Aspects
    "else" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    c ])
                  (Doc Aspects -> Doc Aspects -> Doc Aspects -> Doc Aspects)
    -> P (Doc Aspects)
    -> ReaderT
         PEnv Identity (Doc Aspects -> Doc Aspects -> Doc Aspects)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> TTerm -> P (Doc Aspects)
    pTerm' Int
    0 TTerm
    a
                  ReaderT PEnv Identity (Doc Aspects -> Doc Aspects -> Doc Aspects)
    -> P (Doc Aspects)
    -> ReaderT PEnv Identity (Doc Aspects -> Doc Aspects)
    forall a b.
    ReaderT PEnv Identity (a -> b)
    -> ReaderT PEnv Identity a -> ReaderT PEnv Identity b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Int -> TTerm -> P (Doc Aspects)
    pTerm' Int
    0 TTerm
    b
                  ReaderT PEnv Identity (Doc Aspects -> Doc Aspects)
    -> P (Doc Aspects) -> P (Doc Aspects)
    forall a b.
    ReaderT PEnv Identity (a -> b)
    -> ReaderT PEnv Identity a -> ReaderT PEnv Identity b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> TTerm -> P (Doc Aspects)
    pTerm TTerm
    c
      TDef QName
    f -> Doc Aspects -> P (Doc Aspects)
    forall a. a -> ReaderT PEnv Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Doc Aspects -> P (Doc Aspects)) -> Doc Aspects -> P (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ QName -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty QName
    f
      TCon QName
    c -> Doc Aspects -> P (Doc Aspects)
    forall a. a -> ReaderT PEnv Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Doc Aspects -> P (Doc Aspects)) -> Doc Aspects -> P (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ QName -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    pretty QName
    c
      TLit Literal
    l -> Doc Aspects -> P (Doc Aspects)
    forall a. a -> ReaderT PEnv Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Doc Aspects -> P (Doc Aspects)) -> Doc Aspects -> P (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ Literal -> Doc Aspects
    forall a. Pretty a => a -> Doc Aspects
    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 Aspects -> P (Doc Aspects)
    forall a. a -> ReaderT PEnv Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Doc Aspects -> P (Doc Aspects)) -> Doc Aspects -> P (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    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 Aspects -> P (Doc Aspects)
    forall a. a -> ReaderT PEnv Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Doc Aspects -> P (Doc Aspects)) -> Doc Aspects -> P (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text (TPrim -> [Char]
    opName TPrim
    op)
      TApp TTerm
    f [TTerm]
    es ->
        Int -> P (Doc Aspects) -> P (Doc Aspects)
    paren Int
    9 (P (Doc Aspects) -> P (Doc Aspects))
    -> P (Doc Aspects) -> P (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ (\Doc Aspects
    a [Doc Aspects]
    bs -> [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    sep [Doc Aspects
    a, Int -> Doc Aspects -> Doc Aspects
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
    forall a b. (a -> b) -> a -> b
    $ [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    fsep [Doc Aspects]
    bs])
                  (Doc Aspects -> [Doc Aspects] -> Doc Aspects)
    -> P (Doc Aspects)
    -> ReaderT PEnv Identity ([Doc Aspects] -> Doc Aspects)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> TTerm -> P (Doc Aspects)
    pTerm' Int
    9 TTerm
    f
                  ReaderT PEnv Identity ([Doc Aspects] -> Doc Aspects)
    -> ReaderT PEnv Identity [Doc Aspects] -> P (Doc Aspects)
    forall a b.
    ReaderT PEnv Identity (a -> b)
    -> ReaderT PEnv Identity a -> ReaderT PEnv Identity b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (TTerm -> P (Doc Aspects))
    -> [TTerm] -> ReaderT PEnv Identity [Doc Aspects]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (Int -> TTerm -> P (Doc Aspects)
    pTerm' Int
    10) [TTerm]
    es
      t :: TTerm
    t@TLam{} -> Int -> P (Doc Aspects) -> P (Doc Aspects)
    paren Int
    0 (P (Doc Aspects) -> P (Doc Aspects))
    -> P (Doc Aspects) -> P (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ Int -> TTerm -> ([[Char]] -> P (Doc Aspects)) -> P (Doc Aspects)
    forall a b. HasFree a => Int -> a -> ([[Char]] -> P b) -> P b
    withNames' Int
    n TTerm
    b (([[Char]] -> P (Doc Aspects)) -> P (Doc Aspects))
    -> ([[Char]] -> P (Doc Aspects)) -> P (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ \ [[Char]]
    xs -> [[Char]] -> P (Doc Aspects) -> P (Doc Aspects)
    forall a. [[Char]] -> P a -> P a
    bindNames [[Char]]
    xs (P (Doc Aspects) -> P (Doc Aspects))
    -> P (Doc Aspects) -> P (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $
        (\Doc Aspects
    b -> [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    sep [ [Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    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 Aspects -> Doc Aspects
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 Doc Aspects
    b ]) (Doc Aspects -> Doc Aspects) -> P (Doc Aspects) -> P (Doc Aspects)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> TTerm -> P (Doc Aspects)
    pTerm' Int
    0 TTerm
    b
        where
          (Int
    n, TTerm
    b) = TTerm -> (Int, TTerm)
    tLamView TTerm
    t
      t :: TTerm
    t@TLet{} -> Int -> P (Doc Aspects) -> P (Doc Aspects)
    paren Int
    0 (P (Doc Aspects) -> P (Doc Aspects))
    -> P (Doc Aspects) -> P (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ Int -> ([[Char]] -> P (Doc Aspects)) -> P (Doc Aspects)
    forall a. Int -> ([[Char]] -> P a) -> P a
    withNames ([TTerm] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [TTerm]
    es) (([[Char]] -> P (Doc Aspects)) -> P (Doc Aspects))
    -> ([[Char]] -> P (Doc Aspects)) -> P (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ \ [[Char]]
    xs ->
        (\ ([([Char], Doc Aspects)]
    binds, Doc Aspects
    b) -> [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    sep [ Doc Aspects
    "let" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    vcat [ [Doc Aspects] -> Doc Aspects
    forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
    sep [ [Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    text [Char]
    x Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    "="
                                                    , Int -> Doc Aspects -> Doc Aspects
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 Doc Aspects
    e ] | ([Char]
    x, Doc Aspects
    e) <- [([Char], Doc Aspects)]
    binds ]
                                  Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc Aspects
    "in", Doc Aspects
    b ])
          (([([Char], Doc Aspects)], Doc Aspects) -> Doc Aspects)
    -> ReaderT PEnv Identity ([([Char], Doc Aspects)], Doc Aspects)
    -> P (Doc Aspects)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [([Char], TTerm)]
    -> TTerm
    -> ReaderT PEnv Identity ([([Char], Doc Aspects)], Doc Aspects)
    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 Aspects)], Doc Aspects)
    pLets [] TTerm
    b = ([],) (Doc Aspects -> ([([Char], Doc Aspects)], Doc Aspects))
    -> P (Doc Aspects)
    -> ReaderT PEnv Identity ([([Char], Doc Aspects)], Doc Aspects)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> TTerm -> P (Doc Aspects)
    pTerm' Int
    0 TTerm
    b
          pLets (([Char]
    x, TTerm
    e) : [([Char], TTerm)]
    bs) TTerm
    b = do
            e <- Int -> TTerm -> P (Doc Aspects)
    pTerm' Int
    0 TTerm
    e
            first ((x, e) :) <$> bindName x (pLets bs b)

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

      TTerm
    TUnit -> Doc Aspects -> P (Doc Aspects)
    forall a. a -> ReaderT PEnv Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Doc Aspects
    "()"
      TTerm
    TSort -> Doc Aspects -> P (Doc Aspects)
    forall a. a -> ReaderT PEnv Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Doc Aspects
    "Set"
      TTerm
    TErased -> Doc Aspects -> P (Doc Aspects)
    forall a. a -> ReaderT PEnv Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Doc Aspects
    "_"
      TError TError
    err -> Int -> P (Doc Aspects) -> P (Doc Aspects)
    paren Int
    9 (P (Doc Aspects) -> P (Doc Aspects))
    -> P (Doc Aspects) -> P (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ Doc Aspects -> P (Doc Aspects)
    forall a. a -> ReaderT PEnv Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Doc Aspects -> P (Doc Aspects)) -> Doc Aspects -> P (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ Doc Aspects
    "error" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+> [Char] -> Doc Aspects
    forall a. [Char] -> Doc a
    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 Aspects) -> P (Doc Aspects)
    paren Int
    9 (P (Doc Aspects) -> P (Doc Aspects))
    -> P (Doc Aspects) -> P (Doc Aspects)
    forall a b. (a -> b) -> a -> b
    $ (Doc Aspects
    "coe" Doc Aspects -> Doc Aspects -> Doc Aspects
    forall a. Doc a -> Doc a -> Doc a
    <+>) (Doc Aspects -> Doc Aspects) -> P (Doc Aspects) -> P (Doc Aspects)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> TTerm -> P (Doc Aspects)
    pTerm' Int
    10 TTerm
    t