{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
#if __GLASGOW_HASKELL__ <= 708
{-# LANGUAGE OverlappingInstances #-}
#endif
module Language.Rzk.Syntax.Print where
import Prelude
( ($), (.)
, Bool(..), (==), (<)
, Int, Integer, Double, (+), (-), (*)
, String, (++)
, ShowS, showChar, showString
, all, elem, foldr, id, map, null, replicate, shows, span
)
import Data.Char ( Char, isSpace )
import qualified Language.Rzk.Syntax.Abs
printTree :: Print a => a -> String
printTree :: forall a. Print a => a -> String
printTree = Doc -> String
render (Doc -> String) -> (a -> Doc) -> a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0
type Doc = [ShowS] -> [ShowS]
doc :: ShowS -> Doc
doc :: ShowS -> Doc
doc = (:)
render :: Doc -> String
render :: Doc -> String
render Doc
d = Int -> Bool -> [String] -> ShowS
rend Int
0 Bool
False ((ShowS -> String) -> [ShowS] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
"") ([ShowS] -> [String]) -> [ShowS] -> [String]
forall a b. (a -> b) -> a -> b
$ Doc
d []) String
""
where
rend
:: Int
-> Bool
-> [String]
-> ShowS
rend :: Int -> Bool -> [String] -> ShowS
rend Int
i Bool
p = \case
String
"[" :[String]
ts -> Char -> ShowS
char Char
'[' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Bool -> [String] -> ShowS
rend Int
i Bool
False [String]
ts
String
"(" :[String]
ts -> Char -> ShowS
char Char
'(' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Bool -> [String] -> ShowS
rend Int
i Bool
False [String]
ts
String
"{" :[String]
ts -> Int -> Bool -> ShowS
onNewLine Int
i Bool
p ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
'{' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [String] -> ShowS
new (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [String]
ts
String
"}" : String
";":[String]
ts -> Int -> Bool -> ShowS
onNewLine (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Bool
p ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
"};" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [String] -> ShowS
new (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [String]
ts
String
"}" :[String]
ts -> Int -> Bool -> ShowS
onNewLine (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Bool
p ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
'}' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [String] -> ShowS
new (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [String]
ts
[String
";"] -> Char -> ShowS
char Char
';'
String
";" :[String]
ts -> Char -> ShowS
char Char
';' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [String] -> ShowS
new Int
i [String]
ts
String
t : ts :: [String]
ts@(String
s:[String]
_) | String -> Bool
closingOrPunctuation String
s
-> ShowS
pending ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
t ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Bool -> [String] -> ShowS
rend Int
i Bool
False [String]
ts
String
t :[String]
ts -> ShowS
pending ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
space String
t ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Bool -> [String] -> ShowS
rend Int
i Bool
False [String]
ts
[] -> ShowS
forall a. a -> a
id
where
char :: Char -> ShowS
char :: Char -> ShowS
char Char
c = ShowS
pending ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
c
pending :: ShowS
pending :: ShowS
pending = if Bool
p then Int -> ShowS
indent Int
i else ShowS
forall a. a -> a
id
indent :: Int -> ShowS
indent :: Int -> ShowS
indent Int
i = Int -> ShowS -> ShowS
replicateS (Int
2Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
i) (Char -> ShowS
showChar Char
' ')
new :: Int -> [String] -> ShowS
new :: Int -> [String] -> ShowS
new Int
j [String]
ts = Char -> ShowS
showChar Char
'\n' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Bool -> [String] -> ShowS
rend Int
j Bool
True [String]
ts
onNewLine :: Int -> Bool -> ShowS
onNewLine :: Int -> Bool -> ShowS
onNewLine Int
i Bool
p = (if Bool
p then ShowS
forall a. a -> a
id else Char -> ShowS
showChar Char
'\n') ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ShowS
indent Int
i
space :: String -> ShowS
space :: String -> ShowS
space String
t String
s =
case ((Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace String
t, String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
spc, String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
rest) of
(Bool
True , Bool
_ , Bool
True ) -> []
(Bool
False, Bool
_ , Bool
True ) -> String
t
(Bool
False, Bool
True, Bool
False) -> String
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ Char
' ' Char -> ShowS
forall a. a -> [a] -> [a]
: String
s
(Bool, Bool, Bool)
_ -> String
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
where
(String
spc, String
rest) = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span Char -> Bool
isSpace String
s
closingOrPunctuation :: String -> Bool
closingOrPunctuation :: String -> Bool
closingOrPunctuation [Char
c] = Char
c Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
closerOrPunct
closingOrPunctuation String
_ = Bool
False
closerOrPunct :: String
closerOrPunct :: String
closerOrPunct = String
")],;"
parenth :: Doc -> Doc
parenth :: Doc -> Doc
parenth Doc
ss = ShowS -> Doc
doc (Char -> ShowS
showChar Char
'(') Doc -> Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc
ss Doc -> Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS -> Doc
doc (Char -> ShowS
showChar Char
')')
concatS :: [ShowS] -> ShowS
concatS :: [ShowS] -> ShowS
concatS = (ShowS -> ShowS -> ShowS) -> ShowS -> [ShowS] -> ShowS
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) ShowS
forall a. a -> a
id
concatD :: [Doc] -> Doc
concatD :: [Doc] -> Doc
concatD = (Doc -> Doc -> Doc) -> Doc -> [Doc] -> Doc
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Doc -> Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) Doc
forall a. a -> a
id
replicateS :: Int -> ShowS -> ShowS
replicateS :: Int -> ShowS -> ShowS
replicateS Int
n ShowS
f = [ShowS] -> ShowS
concatS (Int -> ShowS -> [ShowS]
forall a. Int -> a -> [a]
replicate Int
n ShowS
f)
class Print a where
prt :: Int -> a -> Doc
instance {-# OVERLAPPABLE #-} Print a => Print [a] where
prt :: Int -> [a] -> Doc
prt Int
i = [Doc] -> Doc
concatD ([Doc] -> Doc) -> ([a] -> [Doc]) -> [a] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
i)
instance Print Char where
prt :: Int -> Char -> Doc
prt Int
_ Char
c = ShowS -> Doc
doc (Char -> ShowS
showChar Char
'\'' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Char -> ShowS
mkEsc Char
'\'' Char
c ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
'\'')
instance Print String where
prt :: Int -> String -> Doc
prt Int
_ = String -> Doc
printString
printString :: String -> Doc
printString :: String -> Doc
printString String
s = ShowS -> Doc
doc (Char -> ShowS
showChar Char
'"' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ShowS] -> ShowS
concatS ((Char -> ShowS) -> String -> [ShowS]
forall a b. (a -> b) -> [a] -> [b]
map (Char -> Char -> ShowS
mkEsc Char
'"') String
s) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
'"')
mkEsc :: Char -> Char -> ShowS
mkEsc :: Char -> Char -> ShowS
mkEsc Char
q = \case
Char
s | Char
s Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
q -> Char -> ShowS
showChar Char
'\\' ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
s
Char
'\\' -> String -> ShowS
showString String
"\\\\"
Char
'\n' -> String -> ShowS
showString String
"\\n"
Char
'\t' -> String -> ShowS
showString String
"\\t"
Char
s -> Char -> ShowS
showChar Char
s
prPrec :: Int -> Int -> Doc -> Doc
prPrec :: Int -> Int -> Doc -> Doc
prPrec Int
i Int
j = if Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
i then Doc -> Doc
parenth else Doc -> Doc
forall a. a -> a
id
instance Print Integer where
prt :: Int -> Integer -> Doc
prt Int
_ Integer
x = ShowS -> Doc
doc (Integer -> ShowS
forall a. Show a => a -> ShowS
shows Integer
x)
instance Print Double where
prt :: Int -> Double -> Doc
prt Int
_ Double
x = ShowS -> Doc
doc (Double -> ShowS
forall a. Show a => a -> ShowS
shows Double
x)
instance Print Language.Rzk.Syntax.Abs.VarIdentToken where
prt :: Int -> VarIdentToken -> Doc
prt Int
_ (Language.Rzk.Syntax.Abs.VarIdentToken String
i) = ShowS -> Doc
doc (ShowS -> Doc) -> ShowS -> Doc
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
i
instance Print Language.Rzk.Syntax.Abs.HoleIdentToken where
prt :: Int -> HoleIdentToken -> Doc
prt Int
_ (Language.Rzk.Syntax.Abs.HoleIdentToken String
i) = ShowS -> Doc
doc (ShowS -> Doc) -> ShowS -> Doc
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
i
instance Print (Language.Rzk.Syntax.Abs.Module' a) where
prt :: Int -> Module' a -> Doc
prt Int
i = \case
Language.Rzk.Syntax.Abs.Module a
_ LanguageDecl' a
languagedecl [Command' a]
commands -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [Int -> LanguageDecl' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 LanguageDecl' a
languagedecl, Int -> [Command' a] -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 [Command' a]
commands])
instance Print (Language.Rzk.Syntax.Abs.HoleIdent' a) where
prt :: Int -> HoleIdent' a -> Doc
prt Int
i = \case
Language.Rzk.Syntax.Abs.HoleIdent a
_ HoleIdentToken
holeidenttoken -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [Int -> HoleIdentToken -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 HoleIdentToken
holeidenttoken])
instance Print (Language.Rzk.Syntax.Abs.VarIdent' a) where
prt :: Int -> VarIdent' a -> Doc
prt Int
i = \case
Language.Rzk.Syntax.Abs.VarIdent a
_ VarIdentToken
varidenttoken -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [Int -> VarIdentToken -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 VarIdentToken
varidenttoken])
instance Print [Language.Rzk.Syntax.Abs.VarIdent' a] where
prt :: Int -> [VarIdent' a] -> Doc
prt Int
_ [] = [Doc] -> Doc
concatD []
prt Int
_ [VarIdent' a
x] = [Doc] -> Doc
concatD [Int -> VarIdent' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 VarIdent' a
x]
prt Int
_ (VarIdent' a
x:[VarIdent' a]
xs) = [Doc] -> Doc
concatD [Int -> VarIdent' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 VarIdent' a
x, Int -> [VarIdent' a] -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 [VarIdent' a]
xs]
instance Print (Language.Rzk.Syntax.Abs.LanguageDecl' a) where
prt :: Int -> LanguageDecl' a -> Doc
prt Int
i = \case
Language.Rzk.Syntax.Abs.LanguageDecl a
_ Language' a
language -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"#lang"), Int -> Language' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Language' a
language, ShowS -> Doc
doc (String -> ShowS
showString String
";")])
instance Print (Language.Rzk.Syntax.Abs.Language' a) where
prt :: Int -> Language' a -> Doc
prt Int
i = \case
Language.Rzk.Syntax.Abs.Rzk1 a
_ -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"rzk-1")])
instance Print (Language.Rzk.Syntax.Abs.Command' a) where
prt :: Int -> Command' a -> Doc
prt Int
i = \case
Language.Rzk.Syntax.Abs.CommandSetOption a
_ String
str1 String
str2 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"#set-option"), String -> Doc
printString String
str1, ShowS -> Doc
doc (String -> ShowS
showString String
"="), String -> Doc
printString String
str2])
Language.Rzk.Syntax.Abs.CommandUnsetOption a
_ String
str -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"#unset-option"), String -> Doc
printString String
str])
Language.Rzk.Syntax.Abs.CommandCheck a
_ Term' a
term1 Term' a
term2 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"#check"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
":"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term2])
Language.Rzk.Syntax.Abs.CommandCompute a
_ Term' a
term -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"#compute"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term])
Language.Rzk.Syntax.Abs.CommandComputeWHNF a
_ Term' a
term -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"#compute-whnf"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term])
Language.Rzk.Syntax.Abs.CommandComputeNF a
_ Term' a
term -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"#compute-nf"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term])
Language.Rzk.Syntax.Abs.CommandPostulate a
_ VarIdent' a
varident DeclUsedVars' a
declusedvars [Param' a]
params Term' a
term -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"#postulate"), Int -> VarIdent' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 VarIdent' a
varident, Int -> DeclUsedVars' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 DeclUsedVars' a
declusedvars, Int -> [Param' a] -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 [Param' a]
params, ShowS -> Doc
doc (String -> ShowS
showString String
":"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term])
Language.Rzk.Syntax.Abs.CommandAssume a
_ [VarIdent' a]
varidents Term' a
term -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"#assume"), Int -> [VarIdent' a] -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 [VarIdent' a]
varidents, ShowS -> Doc
doc (String -> ShowS
showString String
":"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term])
Language.Rzk.Syntax.Abs.CommandSection a
_ SectionName' a
sectionname -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"#section"), Int -> SectionName' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 SectionName' a
sectionname])
Language.Rzk.Syntax.Abs.CommandSectionEnd a
_ SectionName' a
sectionname -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"#end"), Int -> SectionName' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 SectionName' a
sectionname])
Language.Rzk.Syntax.Abs.CommandDefine a
_ VarIdent' a
varident DeclUsedVars' a
declusedvars [Param' a]
params Term' a
term1 Term' a
term2 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"#define"), Int -> VarIdent' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 VarIdent' a
varident, Int -> DeclUsedVars' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 DeclUsedVars' a
declusedvars, Int -> [Param' a] -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 [Param' a]
params, ShowS -> Doc
doc (String -> ShowS
showString String
":"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
":="), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term2])
instance Print [Language.Rzk.Syntax.Abs.Command' a] where
prt :: Int -> [Command' a] -> Doc
prt Int
_ [] = [Doc] -> Doc
concatD []
prt Int
_ (Command' a
x:[Command' a]
xs) = [Doc] -> Doc
concatD [Int -> Command' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Command' a
x, ShowS -> Doc
doc (String -> ShowS
showString String
";"), Int -> [Command' a] -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 [Command' a]
xs]
instance Print (Language.Rzk.Syntax.Abs.DeclUsedVars' a) where
prt :: Int -> DeclUsedVars' a -> Doc
prt Int
i = \case
Language.Rzk.Syntax.Abs.DeclUsedVars a
_ [VarIdent' a]
varidents -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"uses"), ShowS -> Doc
doc (String -> ShowS
showString String
"("), Int -> [VarIdent' a] -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 [VarIdent' a]
varidents, ShowS -> Doc
doc (String -> ShowS
showString String
")")])
instance Print (Language.Rzk.Syntax.Abs.SectionName' a) where
prt :: Int -> SectionName' a -> Doc
prt Int
i = \case
Language.Rzk.Syntax.Abs.NoSectionName a
_ -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [])
Language.Rzk.Syntax.Abs.SomeSectionName a
_ VarIdent' a
varident -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [Int -> VarIdent' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 VarIdent' a
varident])
instance Print (Language.Rzk.Syntax.Abs.Pattern' a) where
prt :: Int -> Pattern' a -> Doc
prt Int
i = \case
Language.Rzk.Syntax.Abs.PatternUnit a
_ -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"unit")])
Language.Rzk.Syntax.Abs.PatternVar a
_ VarIdent' a
varident -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [Int -> VarIdent' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 VarIdent' a
varident])
Language.Rzk.Syntax.Abs.PatternPair a
_ Pattern' a
pattern_1 Pattern' a
pattern_2 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"("), Int -> Pattern' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Pattern' a
pattern_1, ShowS -> Doc
doc (String -> ShowS
showString String
","), Int -> Pattern' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Pattern' a
pattern_2, ShowS -> Doc
doc (String -> ShowS
showString String
")")])
Language.Rzk.Syntax.Abs.PatternTuple a
_ Pattern' a
pattern_1 Pattern' a
pattern_2 [Pattern' a]
patterns -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"("), Int -> Pattern' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Pattern' a
pattern_1, ShowS -> Doc
doc (String -> ShowS
showString String
","), Int -> Pattern' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Pattern' a
pattern_2, ShowS -> Doc
doc (String -> ShowS
showString String
","), Int -> [Pattern' a] -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
1 [Pattern' a]
patterns, ShowS -> Doc
doc (String -> ShowS
showString String
")")])
instance Print [Language.Rzk.Syntax.Abs.Pattern' a] where
prt :: Int -> [Pattern' a] -> Doc
prt Int
_ [] = [Doc] -> Doc
concatD []
prt Int
1 [Pattern' a
x] = [Doc] -> Doc
concatD [Int -> Pattern' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
1 Pattern' a
x]
prt Int
1 (Pattern' a
x:[Pattern' a]
xs) = [Doc] -> Doc
concatD [Int -> Pattern' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
1 Pattern' a
x, ShowS -> Doc
doc (String -> ShowS
showString String
","), Int -> [Pattern' a] -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
1 [Pattern' a]
xs]
prt Int
_ [Pattern' a
x] = [Doc] -> Doc
concatD [Int -> Pattern' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Pattern' a
x]
prt Int
_ (Pattern' a
x:[Pattern' a]
xs) = [Doc] -> Doc
concatD [Int -> Pattern' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Pattern' a
x, Int -> [Pattern' a] -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 [Pattern' a]
xs]
instance Print (Language.Rzk.Syntax.Abs.Param' a) where
prt :: Int -> Param' a -> Doc
prt Int
i = \case
Language.Rzk.Syntax.Abs.ParamPattern a
_ Pattern' a
pattern_ -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [Int -> Pattern' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Pattern' a
pattern_])
Language.Rzk.Syntax.Abs.ParamPatternType a
_ [Pattern' a]
patterns Term' a
term -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"("), Int -> [Pattern' a] -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 [Pattern' a]
patterns, ShowS -> Doc
doc (String -> ShowS
showString String
":"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term, ShowS -> Doc
doc (String -> ShowS
showString String
")")])
Language.Rzk.Syntax.Abs.ParamPatternShape a
_ [Pattern' a]
patterns Term' a
term1 Term' a
term2 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"("), Int -> [Pattern' a] -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 [Pattern' a]
patterns, ShowS -> Doc
doc (String -> ShowS
showString String
":"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"|"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term2, ShowS -> Doc
doc (String -> ShowS
showString String
")")])
Language.Rzk.Syntax.Abs.ParamPatternShapeDeprecated a
_ Pattern' a
pattern_ Term' a
term1 Term' a
term2 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"{"), Int -> Pattern' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Pattern' a
pattern_, ShowS -> Doc
doc (String -> ShowS
showString String
":"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"|"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term2, ShowS -> Doc
doc (String -> ShowS
showString String
"}")])
instance Print [Language.Rzk.Syntax.Abs.Param' a] where
prt :: Int -> [Param' a] -> Doc
prt Int
_ [] = [Doc] -> Doc
concatD []
prt Int
_ [Param' a
x] = [Doc] -> Doc
concatD [Int -> Param' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Param' a
x]
prt Int
_ (Param' a
x:[Param' a]
xs) = [Doc] -> Doc
concatD [Int -> Param' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Param' a
x, Int -> [Param' a] -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 [Param' a]
xs]
instance Print (Language.Rzk.Syntax.Abs.ParamDecl' a) where
prt :: Int -> ParamDecl' a -> Doc
prt Int
i = \case
Language.Rzk.Syntax.Abs.ParamType a
_ Term' a
term -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
6 Term' a
term])
Language.Rzk.Syntax.Abs.ParamTermType a
_ Term' a
term1 Term' a
term2 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"("), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
":"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term2, ShowS -> Doc
doc (String -> ShowS
showString String
")")])
Language.Rzk.Syntax.Abs.ParamTermShape a
_ Term' a
term1 Term' a
term2 Term' a
term3 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"("), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
":"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term2, ShowS -> Doc
doc (String -> ShowS
showString String
"|"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term3, ShowS -> Doc
doc (String -> ShowS
showString String
")")])
Language.Rzk.Syntax.Abs.ParamTermTypeDeprecated a
_ Pattern' a
pattern_ Term' a
term -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"{"), Int -> Pattern' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Pattern' a
pattern_, ShowS -> Doc
doc (String -> ShowS
showString String
":"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term, ShowS -> Doc
doc (String -> ShowS
showString String
"}")])
Language.Rzk.Syntax.Abs.ParamVarShapeDeprecated a
_ Pattern' a
pattern_ Term' a
term1 Term' a
term2 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"{"), ShowS -> Doc
doc (String -> ShowS
showString String
"("), Int -> Pattern' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Pattern' a
pattern_, ShowS -> Doc
doc (String -> ShowS
showString String
":"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
")"), ShowS -> Doc
doc (String -> ShowS
showString String
"|"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term2, ShowS -> Doc
doc (String -> ShowS
showString String
"}")])
instance Print (Language.Rzk.Syntax.Abs.SigmaParam' a) where
prt :: Int -> SigmaParam' a -> Doc
prt Int
i = \case
Language.Rzk.Syntax.Abs.SigmaParam a
_ Pattern' a
pattern_ Term' a
term -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [Int -> Pattern' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Pattern' a
pattern_, ShowS -> Doc
doc (String -> ShowS
showString String
":"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term])
instance Print [Language.Rzk.Syntax.Abs.SigmaParam' a] where
prt :: Int -> [SigmaParam' a] -> Doc
prt Int
_ [] = [Doc] -> Doc
concatD []
prt Int
_ [SigmaParam' a
x] = [Doc] -> Doc
concatD [Int -> SigmaParam' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 SigmaParam' a
x]
prt Int
_ (SigmaParam' a
x:[SigmaParam' a]
xs) = [Doc] -> Doc
concatD [Int -> SigmaParam' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 SigmaParam' a
x, ShowS -> Doc
doc (String -> ShowS
showString String
","), Int -> [SigmaParam' a] -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 [SigmaParam' a]
xs]
instance Print (Language.Rzk.Syntax.Abs.Restriction' a) where
prt :: Int -> Restriction' a -> Doc
prt Int
i = \case
Language.Rzk.Syntax.Abs.Restriction a
_ Term' a
term1 Term' a
term2 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"\8614"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term2])
Language.Rzk.Syntax.Abs.ASCII_Restriction a
_ Term' a
term1 Term' a
term2 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"|->"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term2])
instance Print [Language.Rzk.Syntax.Abs.Restriction' a] where
prt :: Int -> [Restriction' a] -> Doc
prt Int
_ [] = [Doc] -> Doc
concatD []
prt Int
_ [Restriction' a
x] = [Doc] -> Doc
concatD [Int -> Restriction' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Restriction' a
x]
prt Int
_ (Restriction' a
x:[Restriction' a]
xs) = [Doc] -> Doc
concatD [Int -> Restriction' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Restriction' a
x, ShowS -> Doc
doc (String -> ShowS
showString String
","), Int -> [Restriction' a] -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 [Restriction' a]
xs]
instance Print (Language.Rzk.Syntax.Abs.Term' a) where
prt :: Int -> Term' a -> Doc
prt Int
i = \case
Language.Rzk.Syntax.Abs.Universe a
_ -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"U")])
Language.Rzk.Syntax.Abs.UniverseCube a
_ -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"CUBE")])
Language.Rzk.Syntax.Abs.UniverseTope a
_ -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"TOPE")])
Language.Rzk.Syntax.Abs.CubeUnit a
_ -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"1")])
Language.Rzk.Syntax.Abs.CubeUnitStar a
_ -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"*\8321")])
Language.Rzk.Syntax.Abs.Cube2 a
_ -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"2")])
Language.Rzk.Syntax.Abs.Cube2_0 a
_ -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"0\8322")])
Language.Rzk.Syntax.Abs.Cube2_1 a
_ -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"1\8322")])
Language.Rzk.Syntax.Abs.CubeProduct a
_ Term' a
term1 Term' a
term2 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
5 ([Doc] -> Doc
concatD [Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
5 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"\215"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
6 Term' a
term2])
Language.Rzk.Syntax.Abs.TopeTop a
_ -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"\8868")])
Language.Rzk.Syntax.Abs.TopeBottom a
_ -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"\8869")])
Language.Rzk.Syntax.Abs.TopeEQ a
_ Term' a
term1 Term' a
term2 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
4 ([Doc] -> Doc
concatD [Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
5 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"\8801"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
5 Term' a
term2])
Language.Rzk.Syntax.Abs.TopeLEQ a
_ Term' a
term1 Term' a
term2 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
4 ([Doc] -> Doc
concatD [Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
5 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"\8804"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
5 Term' a
term2])
Language.Rzk.Syntax.Abs.TopeAnd a
_ Term' a
term1 Term' a
term2 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
3 ([Doc] -> Doc
concatD [Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
4 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"\8743"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
3 Term' a
term2])
Language.Rzk.Syntax.Abs.TopeOr a
_ Term' a
term1 Term' a
term2 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
2 ([Doc] -> Doc
concatD [Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
3 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"\8744"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
2 Term' a
term2])
Language.Rzk.Syntax.Abs.RecBottom a
_ -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"recBOT")])
Language.Rzk.Syntax.Abs.RecOr a
_ [Restriction' a]
restrictions -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"recOR"), ShowS -> Doc
doc (String -> ShowS
showString String
"("), Int -> [Restriction' a] -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 [Restriction' a]
restrictions, ShowS -> Doc
doc (String -> ShowS
showString String
")")])
Language.Rzk.Syntax.Abs.RecOrDeprecated a
_ Term' a
term1 Term' a
term2 Term' a
term3 Term' a
term4 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"recOR"), ShowS -> Doc
doc (String -> ShowS
showString String
"("), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
","), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term2, ShowS -> Doc
doc (String -> ShowS
showString String
","), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term3, ShowS -> Doc
doc (String -> ShowS
showString String
","), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term4, ShowS -> Doc
doc (String -> ShowS
showString String
")")])
Language.Rzk.Syntax.Abs.TypeFun a
_ ParamDecl' a
paramdecl Term' a
term -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
1 ([Doc] -> Doc
concatD [Int -> ParamDecl' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 ParamDecl' a
paramdecl, ShowS -> Doc
doc (String -> ShowS
showString String
"\8594"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
1 Term' a
term])
Language.Rzk.Syntax.Abs.TypeSigma a
_ Pattern' a
pattern_ Term' a
term1 Term' a
term2 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
1 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"\931"), ShowS -> Doc
doc (String -> ShowS
showString String
"("), Int -> Pattern' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Pattern' a
pattern_, ShowS -> Doc
doc (String -> ShowS
showString String
":"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
")"), ShowS -> Doc
doc (String -> ShowS
showString String
","), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
1 Term' a
term2])
Language.Rzk.Syntax.Abs.TypeSigmaTuple a
_ SigmaParam' a
sigmaparam [SigmaParam' a]
sigmaparams Term' a
term -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
1 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"\931"), ShowS -> Doc
doc (String -> ShowS
showString String
"("), Int -> SigmaParam' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 SigmaParam' a
sigmaparam, ShowS -> Doc
doc (String -> ShowS
showString String
","), Int -> [SigmaParam' a] -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 [SigmaParam' a]
sigmaparams, ShowS -> Doc
doc (String -> ShowS
showString String
")"), ShowS -> Doc
doc (String -> ShowS
showString String
","), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
1 Term' a
term])
Language.Rzk.Syntax.Abs.TypeUnit a
_ -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"Unit")])
Language.Rzk.Syntax.Abs.TypeId a
_ Term' a
term1 Term' a
term2 Term' a
term3 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
1 ([Doc] -> Doc
concatD [Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
2 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"=_{"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term2, ShowS -> Doc
doc (String -> ShowS
showString String
"}"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
2 Term' a
term3])
Language.Rzk.Syntax.Abs.TypeIdSimple a
_ Term' a
term1 Term' a
term2 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
1 ([Doc] -> Doc
concatD [Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
2 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"="), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
2 Term' a
term2])
Language.Rzk.Syntax.Abs.TypeRestricted a
_ Term' a
term [Restriction' a]
restrictions -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
6 ([Doc] -> Doc
concatD [Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
6 Term' a
term, ShowS -> Doc
doc (String -> ShowS
showString String
"["), Int -> [Restriction' a] -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 [Restriction' a]
restrictions, ShowS -> Doc
doc (String -> ShowS
showString String
"]")])
Language.Rzk.Syntax.Abs.TypeExtensionDeprecated a
_ ParamDecl' a
paramdecl Term' a
term -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"<"), Int -> ParamDecl' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 ParamDecl' a
paramdecl, ShowS -> Doc
doc (String -> ShowS
showString String
"\8594"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term, ShowS -> Doc
doc (String -> ShowS
showString String
">")])
Language.Rzk.Syntax.Abs.App a
_ Term' a
term1 Term' a
term2 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
6 ([Doc] -> Doc
concatD [Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
6 Term' a
term1, Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
7 Term' a
term2])
Language.Rzk.Syntax.Abs.Lambda a
_ [Param' a]
params Term' a
term -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
1 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"\\"), Int -> [Param' a] -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 [Param' a]
params, ShowS -> Doc
doc (String -> ShowS
showString String
"\8594"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
1 Term' a
term])
Language.Rzk.Syntax.Abs.Pair a
_ Term' a
term1 Term' a
term2 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"("), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
","), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term2, ShowS -> Doc
doc (String -> ShowS
showString String
")")])
Language.Rzk.Syntax.Abs.Tuple a
_ Term' a
term1 Term' a
term2 [Term' a]
terms -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"("), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
","), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term2, ShowS -> Doc
doc (String -> ShowS
showString String
","), Int -> [Term' a] -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 [Term' a]
terms, ShowS -> Doc
doc (String -> ShowS
showString String
")")])
Language.Rzk.Syntax.Abs.First a
_ Term' a
term -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
6 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"\960\8321"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
7 Term' a
term])
Language.Rzk.Syntax.Abs.Second a
_ Term' a
term -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
6 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"\960\8322"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
7 Term' a
term])
Language.Rzk.Syntax.Abs.Unit a
_ -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"unit")])
Language.Rzk.Syntax.Abs.Refl a
_ -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"refl")])
Language.Rzk.Syntax.Abs.ReflTerm a
_ Term' a
term -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"refl_{"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term, ShowS -> Doc
doc (String -> ShowS
showString String
"}")])
Language.Rzk.Syntax.Abs.ReflTermType a
_ Term' a
term1 Term' a
term2 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"refl_{"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
":"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term2, ShowS -> Doc
doc (String -> ShowS
showString String
"}")])
Language.Rzk.Syntax.Abs.IdJ a
_ Term' a
term1 Term' a
term2 Term' a
term3 Term' a
term4 Term' a
term5 Term' a
term6 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"idJ"), ShowS -> Doc
doc (String -> ShowS
showString String
"("), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
","), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term2, ShowS -> Doc
doc (String -> ShowS
showString String
","), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term3, ShowS -> Doc
doc (String -> ShowS
showString String
","), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term4, ShowS -> Doc
doc (String -> ShowS
showString String
","), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term5, ShowS -> Doc
doc (String -> ShowS
showString String
","), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term6, ShowS -> Doc
doc (String -> ShowS
showString String
")")])
Language.Rzk.Syntax.Abs.Hole a
_ HoleIdent' a
holeident -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [Int -> HoleIdent' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 HoleIdent' a
holeident])
Language.Rzk.Syntax.Abs.Var a
_ VarIdent' a
varident -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [Int -> VarIdent' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 VarIdent' a
varident])
Language.Rzk.Syntax.Abs.TypeAsc a
_ Term' a
term1 Term' a
term2 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
2 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"as"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
1 Term' a
term2])
Language.Rzk.Syntax.Abs.ASCII_CubeUnitStar a
_ -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"*_1")])
Language.Rzk.Syntax.Abs.ASCII_Cube2_0 a
_ -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"0_2")])
Language.Rzk.Syntax.Abs.ASCII_Cube2_1 a
_ -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"1_2")])
Language.Rzk.Syntax.Abs.ASCII_TopeTop a
_ -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"TOP")])
Language.Rzk.Syntax.Abs.ASCII_TopeBottom a
_ -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"BOT")])
Language.Rzk.Syntax.Abs.ASCII_TopeEQ a
_ Term' a
term1 Term' a
term2 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
4 ([Doc] -> Doc
concatD [Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
5 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"==="), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
5 Term' a
term2])
Language.Rzk.Syntax.Abs.ASCII_TopeLEQ a
_ Term' a
term1 Term' a
term2 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
4 ([Doc] -> Doc
concatD [Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
5 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"<="), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
5 Term' a
term2])
Language.Rzk.Syntax.Abs.ASCII_TopeAnd a
_ Term' a
term1 Term' a
term2 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
3 ([Doc] -> Doc
concatD [Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
4 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"/\\"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
3 Term' a
term2])
Language.Rzk.Syntax.Abs.ASCII_TopeOr a
_ Term' a
term1 Term' a
term2 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
2 ([Doc] -> Doc
concatD [Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
3 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"\\/"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
2 Term' a
term2])
Language.Rzk.Syntax.Abs.ASCII_TypeFun a
_ ParamDecl' a
paramdecl Term' a
term -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
1 ([Doc] -> Doc
concatD [Int -> ParamDecl' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 ParamDecl' a
paramdecl, ShowS -> Doc
doc (String -> ShowS
showString String
"->"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
1 Term' a
term])
Language.Rzk.Syntax.Abs.ASCII_TypeSigma a
_ Pattern' a
pattern_ Term' a
term1 Term' a
term2 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
1 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"Sigma"), ShowS -> Doc
doc (String -> ShowS
showString String
"("), Int -> Pattern' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Pattern' a
pattern_, ShowS -> Doc
doc (String -> ShowS
showString String
":"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
")"), ShowS -> Doc
doc (String -> ShowS
showString String
","), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
1 Term' a
term2])
Language.Rzk.Syntax.Abs.ASCII_TypeSigmaTuple a
_ SigmaParam' a
sigmaparam [SigmaParam' a]
sigmaparams Term' a
term -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
1 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"Sigma"), ShowS -> Doc
doc (String -> ShowS
showString String
"("), Int -> SigmaParam' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 SigmaParam' a
sigmaparam, ShowS -> Doc
doc (String -> ShowS
showString String
","), Int -> [SigmaParam' a] -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 [SigmaParam' a]
sigmaparams, ShowS -> Doc
doc (String -> ShowS
showString String
")"), ShowS -> Doc
doc (String -> ShowS
showString String
","), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
1 Term' a
term])
Language.Rzk.Syntax.Abs.ASCII_Lambda a
_ [Param' a]
params Term' a
term -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
1 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"\\"), Int -> [Param' a] -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 [Param' a]
params, ShowS -> Doc
doc (String -> ShowS
showString String
"->"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
1 Term' a
term])
Language.Rzk.Syntax.Abs.ASCII_TypeExtensionDeprecated a
_ ParamDecl' a
paramdecl Term' a
term -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
7 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"<"), Int -> ParamDecl' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 ParamDecl' a
paramdecl, ShowS -> Doc
doc (String -> ShowS
showString String
"->"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term, ShowS -> Doc
doc (String -> ShowS
showString String
">")])
Language.Rzk.Syntax.Abs.ASCII_First a
_ Term' a
term -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
6 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"first"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
7 Term' a
term])
Language.Rzk.Syntax.Abs.ASCII_Second a
_ Term' a
term -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
6 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"second"), Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
7 Term' a
term])
instance Print [Language.Rzk.Syntax.Abs.Term' a] where
prt :: Int -> [Term' a] -> Doc
prt Int
_ [] = [Doc] -> Doc
concatD []
prt Int
_ [Term' a
x] = [Doc] -> Doc
concatD [Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
x]
prt Int
_ (Term' a
x:[Term' a]
xs) = [Doc] -> Doc
concatD [Int -> Term' a -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
x, ShowS -> Doc
doc (String -> ShowS
showString String
","), Int -> [Term' a] -> Doc
forall a. Print a => Int -> a -> Doc
prt Int
0 [Term' a]
xs]