-- File generated by the BNF Converter (bnfc 2.9.4.1).

{-# LANGUAGE CPP                  #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE LambdaCase           #-}
#if __GLASGOW_HASKELL__ <= 708
{-# LANGUAGE OverlappingInstances #-}
#endif

-- | Pretty-printer for Language.

module Language.Rzk.Syntax.Print where

import           Data.Char               (Char, isSpace)
import qualified Language.Rzk.Syntax.Abs
import           Prelude                 (Bool (..), Double, Int, Integer,
                                          ShowS, String, all, elem, foldr, id,
                                          map, null, replicate, showChar,
                                          showString, shows, span, ($), (*),
                                          (+), (++), (-), (.), (<), (==))

-- | The top-level printing method.

printTree :: Print a => a -> String
printTree :: forall a. Print a => a -> String
printTree = Doc -> String
render forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a -> b) -> a -> b
$ String
"") forall a b. (a -> b) -> a -> b
$ Doc
d []) String
""
  where
  rend
    :: Int        -- ^ Indentation level.
    -> Bool       -- ^ Pending indentation to be output before next character?
    -> [String]
    -> ShowS
  rend :: Int -> Bool -> [String] -> ShowS
rend Int
i Bool
p = \case
      String
"["      :[String]
ts -> Char -> ShowS
char Char
'[' 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
'(' forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Bool -> [String] -> ShowS
rend Int
i Bool
False [String]
ts
--      "{"      :ts -> onNewLine i     p . showChar   '{'  . new (i+1) ts
--      "}" : ";":ts -> onNewLine (i-1) p . showString "};" . new (i-1) ts
--      "}"      :ts -> onNewLine (i-1) p . showChar   '}'  . new (i-1) ts
      [String
";"]        -> Char -> ShowS
char Char
';'
      String
";"      :[String]
ts -> Char -> ShowS
char Char
';' 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
t 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
space String
t      forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Bool -> [String] -> ShowS
rend Int
i Bool
False [String]
ts
      []           -> forall a. a -> a
id
    where
    -- Output character after pending indentation.
    char :: Char -> ShowS
    char :: Char -> ShowS
char Char
c = ShowS
pending forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
c

    -- Output pending indentation.
    pending :: ShowS
    pending :: ShowS
pending = if Bool
p then Int -> ShowS
indent Int
i else forall a. a -> a
id

  -- Indentation (spaces) for given indentation level.
  indent :: Int -> ShowS
  indent :: Int -> ShowS
indent Int
i = Int -> ShowS -> ShowS
replicateS (Int
2forall a. Num a => a -> a -> a
*Int
i) (Char -> ShowS
showChar Char
' ')

  -- Continue rendering in new line with new indentation.
  new :: Int -> [String] -> ShowS
  new :: Int -> [String] -> ShowS
new Int
j [String]
ts = Char -> ShowS
showChar Char
'\n' forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Bool -> [String] -> ShowS
rend Int
j Bool
True [String]
ts

  -- Make sure we are on a fresh line.
  onNewLine :: Int -> Bool -> ShowS
  onNewLine :: Int -> Bool -> ShowS
onNewLine Int
i Bool
p = (if Bool
p then forall a. a -> a
id else Char -> ShowS
showChar Char
'\n') forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ShowS
indent Int
i

  -- Separate given string from following text by a space (if needed).
  space :: String -> ShowS
  space :: String -> ShowS
space String
t String
s =
    case (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace String
t', forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
spc, forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
rest) of
      (Bool
True , Bool
_   , Bool
True ) -> []              -- remove trailing space
      (Bool
False, Bool
_   , Bool
True ) -> String
t'              -- remove trailing space
      (Bool
False, Bool
True, Bool
False) -> String
t' forall a. [a] -> [a] -> [a]
++ Char
' ' forall a. a -> [a] -> [a]
: String
s   -- add space if none
      (Bool, Bool, Bool)
_                    -> String
t' forall a. [a] -> [a] -> [a]
++ String
s
    where
      t' :: String
t'          = String -> ShowS
showString String
t []
      (String
spc, String
rest) = forall a. (a -> Bool) -> [a] -> ([a], [a])
span Char -> Bool
isSpace String
s

  closingOrPunctuation :: String -> Bool
  closingOrPunctuation :: String -> Bool
closingOrPunctuation [Char
c] = Char
c 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
'(') forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc
ss forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS -> Doc
doc (Char -> ShowS
showChar Char
')')

concatS :: [ShowS] -> ShowS
concatS :: [ShowS] -> ShowS
concatS = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) forall a. a -> a
id

concatD :: [Doc] -> Doc
concatD :: [Doc] -> Doc
concatD = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) forall a. a -> a
id

replicateS :: Int -> ShowS -> ShowS
replicateS :: Int -> ShowS -> ShowS
replicateS Int
n ShowS
f = [ShowS] -> ShowS
concatS (forall a. Int -> a -> [a]
replicate Int
n ShowS
f)

-- | The printer class does the job.

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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (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
'\'' forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Char -> ShowS
mkEsc Char
'\'' Char
c 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
'"' forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ShowS] -> ShowS
concatS (forall a b. (a -> b) -> [a] -> [b]
map (Char -> Char -> ShowS
mkEsc Char
'"') String
s) 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 forall a. Eq a => a -> a -> Bool
== Char
q -> Char -> ShowS
showChar Char
'\\' 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 forall a. Ord a => a -> a -> Bool
< Int
i then Doc -> Doc
parenth else forall a. a -> a
id

instance Print Integer where
  prt :: Int -> Integer -> Doc
prt Int
_ Integer
x = ShowS -> Doc
doc (forall a. Show a => a -> ShowS
shows Integer
x)

instance Print Double where
  prt :: Int -> Double -> Doc
prt Int
_ Double
x = ShowS -> Doc
doc (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 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 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 [forall a. Print a => Int -> a -> Doc
prt Int
0 LanguageDecl' a
languagedecl, 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 [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 [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 [forall a. Print a => Int -> a -> Doc
prt Int
0 VarIdent' a
x]
  prt Int
_ (VarIdent' a
x:[VarIdent' a]
xs) = [Doc] -> Doc
concatD [forall a. Print a => Int -> a -> Doc
prt Int
0 VarIdent' a
x, 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"), 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"), forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
":"), 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"), 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"), 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"), 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"), forall a. Print a => Int -> a -> Doc
prt Int
0 VarIdent' a
varident, forall a. Print a => Int -> a -> Doc
prt Int
0 DeclUsedVars' a
declusedvars, forall a. Print a => Int -> a -> Doc
prt Int
0 [Param' a]
params, ShowS -> Doc
doc (String -> ShowS
showString String
":"), 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"), forall a. Print a => Int -> a -> Doc
prt Int
0 [VarIdent' a]
varidents, ShowS -> Doc
doc (String -> ShowS
showString String
":"), forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term])
    Language.Rzk.Syntax.Abs.CommandSection a
_ SectionName' a
sectionname1 [Command' a]
commands SectionName' a
sectionname2 -> Int -> Int -> Doc -> Doc
prPrec Int
i Int
0 ([Doc] -> Doc
concatD [ShowS -> Doc
doc (String -> ShowS
showString String
"#section"), forall a. Print a => Int -> a -> Doc
prt Int
0 SectionName' a
sectionname1, ShowS -> Doc
doc (String -> ShowS
showString String
";"), forall a. Print a => Int -> a -> Doc
prt Int
0 [Command' a]
commands, ShowS -> Doc
doc (String -> ShowS
showString String
"#end"), forall a. Print a => Int -> a -> Doc
prt Int
0 SectionName' a
sectionname2])
    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"), forall a. Print a => Int -> a -> Doc
prt Int
0 VarIdent' a
varident, forall a. Print a => Int -> a -> Doc
prt Int
0 DeclUsedVars' a
declusedvars, forall a. Print a => Int -> a -> Doc
prt Int
0 [Param' a]
params, ShowS -> Doc
doc (String -> ShowS
showString String
":"), forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
":="), 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 [forall a. Print a => Int -> a -> Doc
prt Int
0 Command' a
x, ShowS -> Doc
doc (String -> ShowS
showString String
";"), 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
"("), 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 [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 [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
"("), forall a. Print a => Int -> a -> Doc
prt Int
0 Pattern' a
pattern_1, ShowS -> Doc
doc (String -> ShowS
showString String
","), forall a. Print a => Int -> a -> Doc
prt Int
0 Pattern' a
pattern_2, 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
_ [Pattern' a
x]    = [Doc] -> Doc
concatD [forall a. Print a => Int -> a -> Doc
prt Int
0 Pattern' a
x]
  prt Int
_ (Pattern' a
x:[Pattern' a]
xs) = [Doc] -> Doc
concatD [forall a. Print a => Int -> a -> Doc
prt Int
0 Pattern' a
x, 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 [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
"("), forall a. Print a => Int -> a -> Doc
prt Int
0 [Pattern' a]
patterns, ShowS -> Doc
doc (String -> ShowS
showString String
":"), 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
"("), forall a. Print a => Int -> a -> Doc
prt Int
0 [Pattern' a]
patterns, ShowS -> Doc
doc (String -> ShowS
showString String
":"), forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"|"), 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
"{"), forall a. Print a => Int -> a -> Doc
prt Int
0 Pattern' a
pattern_, ShowS -> Doc
doc (String -> ShowS
showString String
":"), forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"|"), 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 [forall a. Print a => Int -> a -> Doc
prt Int
0 Param' a
x]
  prt Int
_ (Param' a
x:[Param' a]
xs) = [Doc] -> Doc
concatD [forall a. Print a => Int -> a -> Doc
prt Int
0 Param' a
x, 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 [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
"("), forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
":"), 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
"("), forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
":"), forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term2, ShowS -> Doc
doc (String -> ShowS
showString String
"|"), 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
"{"), forall a. Print a => Int -> a -> Doc
prt Int
0 Pattern' a
pattern_, ShowS -> Doc
doc (String -> ShowS
showString String
":"), 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
"("), forall a. Print a => Int -> a -> Doc
prt Int
0 Pattern' a
pattern_, ShowS -> Doc
doc (String -> ShowS
showString String
":"), 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
"|"), 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.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 [forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"\8614"), 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 [forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"|->"), 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 [forall a. Print a => Int -> a -> Doc
prt Int
0 Restriction' a
x]
  prt Int
_ (Restriction' a
x:[Restriction' a]
xs) = [Doc] -> Doc
concatD [forall a. Print a => Int -> a -> Doc
prt Int
0 Restriction' a
x, ShowS -> Doc
doc (String -> ShowS
showString String
","), 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 [forall a. Print a => Int -> a -> Doc
prt Int
5 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"\215"), 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 [forall a. Print a => Int -> a -> Doc
prt Int
5 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"\8801"), 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 [forall a. Print a => Int -> a -> Doc
prt Int
5 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"\8804"), 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 [forall a. Print a => Int -> a -> Doc
prt Int
4 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"\8743"), 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 [forall a. Print a => Int -> a -> Doc
prt Int
3 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"\8744"), 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
"("), 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
"("), forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
","), forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term2, ShowS -> Doc
doc (String -> ShowS
showString String
","), forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term3, ShowS -> Doc
doc (String -> ShowS
showString String
","), 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 [forall a. Print a => Int -> a -> Doc
prt Int
0 ParamDecl' a
paramdecl, ShowS -> Doc
doc (String -> ShowS
showString String
"\8594"), 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
"("), forall a. Print a => Int -> a -> Doc
prt Int
0 Pattern' a
pattern_, ShowS -> Doc
doc (String -> ShowS
showString String
":"), 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
","), forall a. Print a => Int -> a -> Doc
prt Int
1 Term' a
term2])
    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 [forall a. Print a => Int -> a -> Doc
prt Int
2 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"=_{"), forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term2, ShowS -> Doc
doc (String -> ShowS
showString String
"}"), 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 [forall a. Print a => Int -> a -> Doc
prt Int
2 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"="), 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 [forall a. Print a => Int -> a -> Doc
prt Int
6 Term' a
term, ShowS -> Doc
doc (String -> ShowS
showString String
"["), 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
"<"), forall a. Print a => Int -> a -> Doc
prt Int
0 ParamDecl' a
paramdecl, ShowS -> Doc
doc (String -> ShowS
showString String
"\8594"), 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 [forall a. Print a => Int -> a -> Doc
prt Int
6 Term' a
term1, 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
"\\"), forall a. Print a => Int -> a -> Doc
prt Int
0 [Param' a]
params, ShowS -> Doc
doc (String -> ShowS
showString String
"\8594"), 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
"("), forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
","), forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term2, 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"), 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"), 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_{"), 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_{"), forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
":"), 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
"("), forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
","), forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term2, ShowS -> Doc
doc (String -> ShowS
showString String
","), forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term3, ShowS -> Doc
doc (String -> ShowS
showString String
","), forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term4, ShowS -> Doc
doc (String -> ShowS
showString String
","), forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
term5, ShowS -> Doc
doc (String -> ShowS
showString String
","), 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 [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 [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 [forall a. Print a => Int -> a -> Doc
prt Int
2 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"as"), 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 [forall a. Print a => Int -> a -> Doc
prt Int
5 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"==="), 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 [forall a. Print a => Int -> a -> Doc
prt Int
5 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"<="), 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 [forall a. Print a => Int -> a -> Doc
prt Int
4 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"/\\"), 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 [forall a. Print a => Int -> a -> Doc
prt Int
3 Term' a
term1, ShowS -> Doc
doc (String -> ShowS
showString String
"\\/"), 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 [forall a. Print a => Int -> a -> Doc
prt Int
0 ParamDecl' a
paramdecl, ShowS -> Doc
doc (String -> ShowS
showString String
"->"), 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
"("), forall a. Print a => Int -> a -> Doc
prt Int
0 Pattern' a
pattern_, ShowS -> Doc
doc (String -> ShowS
showString String
":"), 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
","), forall a. Print a => Int -> a -> Doc
prt Int
1 Term' a
term2])
    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
"\\"), forall a. Print a => Int -> a -> Doc
prt Int
0 [Param' a]
params, ShowS -> Doc
doc (String -> ShowS
showString String
"->"), 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
"<"), forall a. Print a => Int -> a -> Doc
prt Int
0 ParamDecl' a
paramdecl, ShowS -> Doc
doc (String -> ShowS
showString String
"->"), 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"), 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"), 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 [forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
x]
  prt Int
_ (Term' a
x:[Term' a]
xs) = [Doc] -> Doc
concatD [forall a. Print a => Int -> a -> Doc
prt Int
0 Term' a
x, ShowS -> Doc
doc (String -> ShowS
showString String
","), forall a. Print a => Int -> a -> Doc
prt Int
0 [Term' a]
xs]