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

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 :: 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 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
$ 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 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