{-# OPTIONS_GHC -fno-warn-orphans #-}
module Agda.Compiler.Treeless.Pretty () where
import Prelude hiding ((!!))
import Control.Arrow (first)
import Control.Monad.Reader
import Data.Maybe
import qualified Data.Map as Map
import Agda.Syntax.Treeless
import Agda.Compiler.Treeless.Subst
import Agda.Utils.Pretty
import Agda.Utils.List
import Agda.Utils.Impossible
data PEnv = PEnv { PEnv -> Int
pPrec :: Int
, PEnv -> [String]
pFresh :: [String]
, PEnv -> [String]
pBound :: [String] }
type P = Reader PEnv
withNames :: Int -> ([String] -> P a) -> P a
withNames :: Int -> ([String] -> P a) -> P a
withNames n :: Int
n k :: [String] -> P a
k = do
(xs :: [String]
xs, ys :: [String]
ys) <- (PEnv -> ([String], [String]))
-> ReaderT PEnv Identity ([String], [String])
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((PEnv -> ([String], [String]))
-> ReaderT PEnv Identity ([String], [String]))
-> (PEnv -> ([String], [String]))
-> ReaderT PEnv Identity ([String], [String])
forall a b. (a -> b) -> a -> b
$ Int -> [String] -> ([String], [String])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n ([String] -> ([String], [String]))
-> (PEnv -> [String]) -> PEnv -> ([String], [String])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PEnv -> [String]
pFresh
(PEnv -> PEnv) -> P a -> P a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\ e :: PEnv
e -> PEnv
e { pFresh :: [String]
pFresh = [String]
ys }) ([String] -> P a
k [String]
xs)
withNames' :: HasFree a => Int -> a -> ([String] -> P b) -> P b
withNames' :: Int -> a -> ([String] -> P b) -> P b
withNames' n :: Int
n tm :: a
tm k :: [String] -> P b
k = Int -> ([String] -> P b) -> P b
forall a. Int -> ([String] -> P a) -> P a
withNames Int
n' (([String] -> P b) -> P b) -> ([String] -> P b) -> P b
forall a b. (a -> b) -> a -> b
$ [String] -> P b
k ([String] -> P b) -> ([String] -> [String]) -> [String] -> P b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> [String]
insBlanks
where
fv :: Map Int Occurs
fv = a -> Map Int Occurs
forall a. HasFree a => a -> Map Int Occurs
freeVars a
tm
n' :: Int
n' = [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n) ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ Map Int Occurs -> [Int]
forall k a. Map k a -> [k]
Map.keys Map Int Occurs
fv
insBlanks :: [String] -> [String]
insBlanks = Int -> [String] -> [String]
forall a. IsString a => Int -> [a] -> [a]
go Int
n
where
go :: Int -> [a] -> [a]
go 0 _ = []
go i :: Int
i xs0 :: [a]
xs0@(~(x :: a
x : xs :: [a]
xs))
| Int -> Map Int Occurs -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) Map Int Occurs
fv = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: Int -> [a] -> [a]
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) [a]
xs
| Bool
otherwise = "_" a -> [a] -> [a]
forall a. a -> [a] -> [a]
: Int -> [a] -> [a]
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) [a]
xs0
bindName :: String -> P a -> P a
bindName :: String -> P a -> P a
bindName x :: String
x = (PEnv -> PEnv) -> P a -> P a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((PEnv -> PEnv) -> P a -> P a) -> (PEnv -> PEnv) -> P a -> P a
forall a b. (a -> b) -> a -> b
$ \ e :: PEnv
e -> PEnv
e { pBound :: [String]
pBound = String
x String -> [String] -> [String]
forall a. a -> [a] -> [a]
: PEnv -> [String]
pBound PEnv
e }
bindNames :: [String] -> P a -> P a
bindNames :: [String] -> P a -> P a
bindNames xs :: [String]
xs p :: P a
p = (String -> P a -> P a) -> P a -> [String] -> P a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr String -> P a -> P a
forall a. String -> P a -> P a
bindName P a
p [String]
xs
paren :: Int -> P Doc -> P Doc
paren :: Int -> P Doc -> P Doc
paren p :: Int
p doc :: P Doc
doc = do
Int
n <- (PEnv -> Int) -> ReaderT PEnv Identity Int
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks PEnv -> Int
pPrec
(if Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n then Doc -> Doc
parens else Doc -> Doc
forall a. a -> a
id) (Doc -> Doc) -> P Doc -> P Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> P Doc
doc
prec :: Int -> P a -> P a
prec :: Int -> P a -> P a
prec p :: Int
p = (PEnv -> PEnv) -> P a -> P a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((PEnv -> PEnv) -> P a -> P a) -> (PEnv -> PEnv) -> P a -> P a
forall a b. (a -> b) -> a -> b
$ \ e :: PEnv
e -> PEnv
e { pPrec :: Int
pPrec = Int
p }
name :: Int -> P String
name :: Int -> P String
name x :: Int
x = (PEnv -> String) -> P String
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks
((PEnv -> String) -> P String) -> (PEnv -> String) -> P String
forall a b. (a -> b) -> a -> b
$ (\ xs :: [String]
xs -> String -> [String] -> Int -> String
forall a. a -> [a] -> Int -> a
indexWithDefault String
forall a. HasCallStack => a
__IMPOSSIBLE__ [String]
xs Int
x)
([String] -> String) -> (PEnv -> [String]) -> PEnv -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (Integer -> String) -> [Integer] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (("^" String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (Integer -> String) -> Integer -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> String
forall a. Show a => a -> String
show) [1..])
([String] -> [String]) -> (PEnv -> [String]) -> PEnv -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PEnv -> [String]
pBound
runP :: P a -> a
runP :: P a -> a
runP p :: P a
p = P a -> PEnv -> a
forall r a. Reader r a -> r -> a
runReader P a
p PEnv :: Int -> [String] -> [String] -> PEnv
PEnv{ pPrec :: Int
pPrec = 0, pFresh :: [String]
pFresh = [String]
names, pBound :: [String]
pBound = [] }
where
names :: [String]
names = [ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
i | String
i <- "" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (Integer -> String) -> [Integer] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> String
forall a. Show a => a -> String
show [1..], String
x <- (Char -> String) -> String -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Char -> String -> String
forall a. a -> [a] -> [a]
:[]) ['a'..'z'] ]
instance Pretty TTerm where
prettyPrec :: Int -> TTerm -> Doc
prettyPrec p :: Int
p t :: TTerm
t = P Doc -> Doc
forall a. P a -> a
runP (P Doc -> Doc) -> P Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> P Doc -> P Doc
forall a. Int -> P a -> P a
prec Int
p (TTerm -> P Doc
pTerm TTerm
t)
opName :: TPrim -> String
opName :: TPrim -> String
opName PAdd = "+"
opName PSub = "-"
opName PMul = "*"
opName PQuot = "quot"
opName PRem = "rem"
opName PGeq = ">="
opName PLt = "<"
opName PEqI = "==I"
opName PAdd64 = "+64"
opName PSub64 = "-64"
opName PMul64 = "*64"
opName PQuot64 = "quot64"
opName PRem64 = "rem64"
opName PLt64 = "<64"
opName PEq64 = "==64"
opName PEqF = "==F"
opName PEqS = "==S"
opName PEqC = "==C"
opName PEqQ = "==Q"
opName PIf = "if_then_else_"
opName PSeq = "seq"
opName PITo64 = "toWord64"
opName P64ToI = "fromWord64"
isInfix :: TPrim -> Maybe (Int, Int, Int)
isInfix :: TPrim -> Maybe (Int, Int, Int)
isInfix op :: TPrim
op =
case TPrim
op of
PMul -> Int -> Maybe (Int, Int, Int)
forall c. Num c => c -> Maybe (c, c, c)
l 7
PAdd -> Int -> Maybe (Int, Int, Int)
forall c. Num c => c -> Maybe (c, c, c)
l 6
PSub -> Int -> Maybe (Int, Int, Int)
forall c. Num c => c -> Maybe (c, c, c)
l 6
PGeq -> Int -> Maybe (Int, Int, Int)
forall c. Num c => c -> Maybe (c, c, c)
non 4
PLt -> Int -> Maybe (Int, Int, Int)
forall c. Num c => c -> Maybe (c, c, c)
non 4
PMul64 -> Int -> Maybe (Int, Int, Int)
forall c. Num c => c -> Maybe (c, c, c)
l 7
PAdd64 -> Int -> Maybe (Int, Int, Int)
forall c. Num c => c -> Maybe (c, c, c)
l 6
PSub64 -> Int -> Maybe (Int, Int, Int)
forall c. Num c => c -> Maybe (c, c, c)
l 6
PLt64 -> Int -> Maybe (Int, Int, Int)
forall c. Num c => c -> Maybe (c, c, c)
non 4
p :: TPrim
p | TPrim -> Bool
isPrimEq TPrim
p -> Int -> Maybe (Int, Int, Int)
forall c. Num c => c -> Maybe (c, c, c)
non 4
_ -> Maybe (Int, Int, Int)
forall a. Maybe a
Nothing
where
l :: c -> Maybe (c, c, c)
l n :: c
n = (c, c, c) -> Maybe (c, c, c)
forall a. a -> Maybe a
Just (c
n, c
n, c
n c -> c -> c
forall a. Num a => a -> a -> a
+ 1)
r :: c -> Maybe (c, c, c)
r n :: c
n = (c, c, c) -> Maybe (c, c, c)
forall a. a -> Maybe a
Just (c
n, c
n c -> c -> c
forall a. Num a => a -> a -> a
+ 1, c
n)
non :: c -> Maybe (c, c, c)
non n :: c
n = (c, c, c) -> Maybe (c, c, c)
forall a. a -> Maybe a
Just (c
n, c
n c -> c -> c
forall a. Num a => a -> a -> a
+ 1, c
n c -> c -> c
forall a. Num a => a -> a -> a
+ 1)
pTerm' :: Int -> TTerm -> P Doc
pTerm' :: Int -> TTerm -> P Doc
pTerm' p :: Int
p = Int -> P Doc -> P Doc
forall a. Int -> P a -> P a
prec Int
p (P Doc -> P Doc) -> (TTerm -> P Doc) -> TTerm -> P Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TTerm -> P Doc
pTerm
pTerm :: TTerm -> P Doc
pTerm :: TTerm -> P Doc
pTerm t :: TTerm
t = case TTerm
t of
TVar x :: Int
x -> String -> Doc
text (String -> Doc) -> P String -> P Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> P String
name Int
x
TApp (TPrim op :: TPrim
op) [a :: TTerm
a, b :: TTerm
b] | Just (c :: Int
c, l :: Int
l, r :: Int
r) <- TPrim -> Maybe (Int, Int, Int)
isInfix TPrim
op ->
Int -> P Doc -> P Doc
paren Int
c (P Doc -> P Doc) -> P Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep ([Doc] -> Doc) -> ReaderT PEnv Identity [Doc] -> P Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [P Doc] -> ReaderT PEnv Identity [Doc]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ Int -> TTerm -> P Doc
pTerm' Int
l TTerm
a
, Doc -> P Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> P Doc) -> Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ TPrim -> String
opName TPrim
op
, Int -> TTerm -> P Doc
pTerm' Int
r TTerm
b ]
TApp (TPrim PIf) [a :: TTerm
a, b :: TTerm
b, c :: TTerm
c] ->
Int -> P Doc -> P Doc
paren 0 (P Doc -> P Doc) -> P Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ (\ a :: Doc
a b :: Doc
b c :: Doc
c -> [Doc] -> Doc
sep [ "if" Doc -> Doc -> Doc
<+> Doc
a
, Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ "then" Doc -> Doc -> Doc
<+> Doc
b
, Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ "else" Doc -> Doc -> Doc
<+> Doc
c ])
(Doc -> Doc -> Doc -> Doc)
-> P Doc -> ReaderT PEnv Identity (Doc -> Doc -> Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TTerm -> P Doc
pTerm' 0 TTerm
a
ReaderT PEnv Identity (Doc -> Doc -> Doc)
-> P Doc -> ReaderT PEnv Identity (Doc -> Doc)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> TTerm -> P Doc
pTerm' 0 TTerm
b
ReaderT PEnv Identity (Doc -> Doc) -> P Doc -> P Doc
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TTerm -> P Doc
pTerm TTerm
c
TDef f :: QName
f -> Doc -> P Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> P Doc) -> Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
f
TCon c :: QName
c -> Doc -> P Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> P Doc) -> Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
c
TLit l :: Literal
l -> Doc -> P Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> P Doc) -> Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ Literal -> Doc
forall a. Pretty a => a -> Doc
pretty Literal
l
TPrim op :: TPrim
op | Maybe (Int, Int, Int) -> Bool
forall a. Maybe a -> Bool
isJust (TPrim -> Maybe (Int, Int, Int)
isInfix TPrim
op) -> Doc -> P Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> P Doc) -> Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text ("_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ TPrim -> String
opName TPrim
op String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_")
| Bool
otherwise -> Doc -> P Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> P Doc) -> Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text (TPrim -> String
opName TPrim
op)
TApp f :: TTerm
f es :: [TTerm]
es ->
Int -> P Doc -> P Doc
paren 9 (P Doc -> P Doc) -> P Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ (\a :: Doc
a bs :: [Doc]
bs -> [Doc] -> Doc
sep [Doc
a, Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep [Doc]
bs])
(Doc -> [Doc] -> Doc)
-> P Doc -> ReaderT PEnv Identity ([Doc] -> Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TTerm -> P Doc
pTerm' 9 TTerm
f
ReaderT PEnv Identity ([Doc] -> Doc)
-> ReaderT PEnv Identity [Doc] -> P Doc
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (TTerm -> P Doc) -> [TTerm] -> ReaderT PEnv Identity [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Int -> TTerm -> P Doc
pTerm' 10) [TTerm]
es
TLam _ -> Int -> P Doc -> P Doc
paren 0 (P Doc -> P Doc) -> P Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ Int -> TTerm -> ([String] -> P Doc) -> P Doc
forall a b. HasFree a => Int -> a -> ([String] -> P b) -> P b
withNames' Int
n TTerm
b (([String] -> P Doc) -> P Doc) -> ([String] -> P Doc) -> P Doc
forall a b. (a -> b) -> a -> b
$ \ xs :: [String]
xs -> [String] -> P Doc -> P Doc
forall a. [String] -> P a -> P a
bindNames [String]
xs (P Doc -> P Doc) -> P Doc -> P Doc
forall a b. (a -> b) -> a -> b
$
(\b :: Doc
b -> [Doc] -> Doc
sep [ String -> Doc
text ("λ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
xs String -> String -> String
forall a. [a] -> [a] -> [a]
++ " →")
, Int -> Doc -> Doc
nest 2 Doc
b ]) (Doc -> Doc) -> P Doc -> P Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TTerm -> P Doc
pTerm' 0 TTerm
b
where
(n :: Int
n, b :: TTerm
b) = TTerm -> (Int, TTerm)
tLamView TTerm
t
TLet{} -> Int -> P Doc -> P Doc
paren 0 (P Doc -> P Doc) -> P Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ Int -> ([String] -> P Doc) -> P Doc
forall a. Int -> ([String] -> P a) -> P a
withNames ([TTerm] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TTerm]
es) (([String] -> P Doc) -> P Doc) -> ([String] -> P Doc) -> P Doc
forall a b. (a -> b) -> a -> b
$ \ xs :: [String]
xs ->
(\ (binds :: [(String, Doc)]
binds, b :: Doc
b) -> [Doc] -> Doc
sep [ "let" Doc -> Doc -> Doc
<+> [Doc] -> Doc
vcat [ [Doc] -> Doc
sep [ String -> Doc
text String
x Doc -> Doc -> Doc
<+> "="
, Int -> Doc -> Doc
nest 2 Doc
e ] | (x :: String
x, e :: Doc
e) <- [(String, Doc)]
binds ]
Doc -> Doc -> Doc
<+> "in", Doc
b ])
(([(String, Doc)], Doc) -> Doc)
-> ReaderT PEnv Identity ([(String, Doc)], Doc) -> P Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(String, TTerm)]
-> TTerm -> ReaderT PEnv Identity ([(String, Doc)], Doc)
pLets ([String] -> [TTerm] -> [(String, TTerm)]
forall a b. [a] -> [b] -> [(a, b)]
zip [String]
xs [TTerm]
es) TTerm
b
where
(es :: [TTerm]
es, b :: TTerm
b) = TTerm -> ([TTerm], TTerm)
tLetView TTerm
t
pLets :: [(String, TTerm)]
-> TTerm -> ReaderT PEnv Identity ([(String, Doc)], Doc)
pLets [] b :: TTerm
b = ([],) (Doc -> ([(String, Doc)], Doc))
-> P Doc -> ReaderT PEnv Identity ([(String, Doc)], Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TTerm -> P Doc
pTerm' 0 TTerm
b
pLets ((x :: String
x, e :: TTerm
e) : bs :: [(String, TTerm)]
bs) b :: TTerm
b = do
Doc
e <- Int -> TTerm -> P Doc
pTerm' 0 TTerm
e
([(String, Doc)] -> [(String, Doc)])
-> ([(String, Doc)], Doc) -> ([(String, Doc)], Doc)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ((String
x, Doc
e) (String, Doc) -> [(String, Doc)] -> [(String, Doc)]
forall a. a -> [a] -> [a]
:) (([(String, Doc)], Doc) -> ([(String, Doc)], Doc))
-> ReaderT PEnv Identity ([(String, Doc)], Doc)
-> ReaderT PEnv Identity ([(String, Doc)], Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String
-> ReaderT PEnv Identity ([(String, Doc)], Doc)
-> ReaderT PEnv Identity ([(String, Doc)], Doc)
forall a. String -> P a -> P a
bindName String
x ([(String, TTerm)]
-> TTerm -> ReaderT PEnv Identity ([(String, Doc)], Doc)
pLets [(String, TTerm)]
bs TTerm
b)
TCase x :: Int
x _ def :: TTerm
def alts :: [TAlt]
alts -> Int -> P Doc -> P Doc
paren 0 (P Doc -> P Doc) -> P Doc -> P Doc
forall a b. (a -> b) -> a -> b
$
(\ sc :: Doc
sc alts :: [Doc]
alts defd :: Doc
defd ->
[Doc] -> Doc
sep [ "case" Doc -> Doc -> Doc
<+> Doc
sc Doc -> Doc -> Doc
<+> "of"
, Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat ([Doc]
alts [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [ "_ →" Doc -> Doc -> Doc
<+> Doc
defd | [Doc] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc]
alts Bool -> Bool -> Bool
|| TTerm
def TTerm -> TTerm -> Bool
forall a. Eq a => a -> a -> Bool
/= TError -> TTerm
TError TError
TUnreachable ]) ]
) (Doc -> [Doc] -> Doc -> Doc)
-> P Doc -> ReaderT PEnv Identity ([Doc] -> Doc -> Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TTerm -> P Doc
pTerm' 0 (Int -> TTerm
TVar Int
x)
ReaderT PEnv Identity ([Doc] -> Doc -> Doc)
-> ReaderT PEnv Identity [Doc]
-> ReaderT PEnv Identity (Doc -> Doc)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (TAlt -> P Doc) -> [TAlt] -> ReaderT PEnv Identity [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TAlt -> P Doc
pAlt [TAlt]
alts
ReaderT PEnv Identity (Doc -> Doc) -> P Doc -> P Doc
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> TTerm -> P Doc
pTerm' 0 TTerm
def
where
pAlt :: TAlt -> P Doc
pAlt (TALit l :: Literal
l b :: TTerm
b) = Doc -> Doc -> Doc
pAlt' (Doc -> Doc -> Doc) -> P Doc -> ReaderT PEnv Identity (Doc -> Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TTerm -> P Doc
pTerm' 0 (Literal -> TTerm
TLit Literal
l) ReaderT PEnv Identity (Doc -> Doc) -> P Doc -> P Doc
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> TTerm -> P Doc
pTerm' 0 TTerm
b
pAlt (TAGuard g :: TTerm
g b :: TTerm
b) =
Doc -> Doc -> Doc
pAlt' (Doc -> Doc -> Doc) -> P Doc -> ReaderT PEnv Identity (Doc -> Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (("_" Doc -> Doc -> Doc
<+> "|" Doc -> Doc -> Doc
<+>) (Doc -> Doc) -> P Doc -> P Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TTerm -> P Doc
pTerm' 0 TTerm
g)
ReaderT PEnv Identity (Doc -> Doc) -> P Doc -> P Doc
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Int -> TTerm -> P Doc
pTerm' 0 TTerm
b)
pAlt (TACon c :: QName
c a :: Int
a b :: TTerm
b) =
Int -> TTerm -> ([String] -> P Doc) -> P Doc
forall a b. HasFree a => Int -> a -> ([String] -> P b) -> P b
withNames' Int
a TTerm
b (([String] -> P Doc) -> P Doc) -> ([String] -> P Doc) -> P Doc
forall a b. (a -> b) -> a -> b
$ \ xs :: [String]
xs -> [String] -> P Doc -> P Doc
forall a. [String] -> P a -> P a
bindNames [String]
xs (P Doc -> P Doc) -> P Doc -> P Doc
forall a b. (a -> b) -> a -> b
$
Doc -> Doc -> Doc
pAlt' (Doc -> Doc -> Doc) -> P Doc -> ReaderT PEnv Identity (Doc -> Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TTerm -> P Doc
pTerm' 0 (TTerm -> [TTerm] -> TTerm
TApp (QName -> TTerm
TCon QName
c) [Int -> TTerm
TVar Int
i | Int
i <- [Int] -> [Int]
forall a. [a] -> [a]
reverse [0..Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1]])
ReaderT PEnv Identity (Doc -> Doc) -> P Doc -> P Doc
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> TTerm -> P Doc
pTerm' 0 TTerm
b
pAlt' :: Doc -> Doc -> Doc
pAlt' p :: Doc
p b :: Doc
b = [Doc] -> Doc
sep [Doc
p Doc -> Doc -> Doc
<+> "→", Int -> Doc -> Doc
nest 2 Doc
b]
TUnit -> Doc -> P Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure "()"
TSort -> Doc -> P Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure "Set"
TErased -> Doc -> P Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure "_"
TError err :: TError
err -> Int -> P Doc -> P Doc
paren 9 (P Doc -> P Doc) -> P Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ Doc -> P Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> P Doc) -> Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ "error" Doc -> Doc -> Doc
<+> String -> Doc
text (String -> String
forall a. Show a => a -> String
show (TError -> String
forall a. Show a => a -> String
show TError
err))
TCoerce t :: TTerm
t -> Int -> P Doc -> P Doc
paren 9 (P Doc -> P Doc) -> P Doc -> P Doc
forall a b. (a -> b) -> a -> b
$ ("coe" Doc -> Doc -> Doc
<+>) (Doc -> Doc) -> P Doc -> P Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TTerm -> P Doc
pTerm' 10 TTerm
t