b4a00883f358625923365ca1560c96edec172a52sf{- |

b4a00883f358625923365ca1560c96edec172a52sfModule : $Header$

b4a00883f358625923365ca1560c96edec172a52sfDescription : A parser for the TPTP Input Syntax

b4a00883f358625923365ca1560c96edec172a52sfCopyright : (c) C.Maeder, DFKI Lab Bremen 2008

b4a00883f358625923365ca1560c96edec172a52sfLicense : GPLv2 or higher, see LICENSE.txt

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfMaintainer : Christian.Maeder@dfki.de

b4a00883f358625923365ca1560c96edec172a52sfStability : provisional

b4a00883f358625923365ca1560c96edec172a52sfPortability : portable

b4a00883f358625923365ca1560c96edec172a52sf

0662ed52e814f8f08ef0e09956413a792584eddffuankgA parser for the TPTP Input Syntax v3.4.0.1 taken from

b4a00883f358625923365ca1560c96edec172a52sf<http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html>

b4a00883f358625923365ca1560c96edec172a52sf-}

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfmodule SoftFOL.ParseTPTP

b4a00883f358625923365ca1560c96edec172a52sf ( tptp

b4a00883f358625923365ca1560c96edec172a52sf , singleQuoted

b4a00883f358625923365ca1560c96edec172a52sf , form

b4a00883f358625923365ca1560c96edec172a52sf , genList

b4a00883f358625923365ca1560c96edec172a52sf , genTerm

44f575c8cb19a7a5cd61664a7848be6bc197df02fuankg , GenTerm (..)

b4a00883f358625923365ca1560c96edec172a52sf , GenData (..)

b4a00883f358625923365ca1560c96edec172a52sf , AWord (..)

b4a00883f358625923365ca1560c96edec172a52sf , prTPTPs

b4a00883f358625923365ca1560c96edec172a52sf , tptpModel

b4a00883f358625923365ca1560c96edec172a52sf , ppGenTerm

b4a00883f358625923365ca1560c96edec172a52sf ) where

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfimport Text.ParserCombinators.Parsec

b4a00883f358625923365ca1560c96edec172a52sfimport SoftFOL.Sign

b4a00883f358625923365ca1560c96edec172a52sfimport SoftFOL.PrintTPTP

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfimport qualified Common.Doc as Doc

b4a00883f358625923365ca1560c96edec172a52sfimport Common.Id

b4a00883f358625923365ca1560c96edec172a52sfimport Common.Lexer (getPos)

b4a00883f358625923365ca1560c96edec172a52sfimport Common.Parsec

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfimport Control.Monad

b4a00883f358625923365ca1560c96edec172a52sfimport Data.Char (ord, toLower, isAlphaNum)

b4a00883f358625923365ca1560c96edec172a52sfimport Data.Maybe

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfshowRole :: Role -> String

b4a00883f358625923365ca1560c96edec172a52sfshowRole = map toLower . show

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfallRoles :: [Role]

b4a00883f358625923365ca1560c96edec172a52sfallRoles =

b4a00883f358625923365ca1560c96edec172a52sf [ Axiom

b4a00883f358625923365ca1560c96edec172a52sf , Hypothesis

b4a00883f358625923365ca1560c96edec172a52sf , Definition

b4a00883f358625923365ca1560c96edec172a52sf , Assumption

b4a00883f358625923365ca1560c96edec172a52sf , Lemma

b4a00883f358625923365ca1560c96edec172a52sf , Theorem

b4a00883f358625923365ca1560c96edec172a52sf , Conjecture

b4a00883f358625923365ca1560c96edec172a52sf , Negated_conjecture

b4a00883f358625923365ca1560c96edec172a52sf , Plain

b4a00883f358625923365ca1560c96edec172a52sf , Fi_domain

b4a00883f358625923365ca1560c96edec172a52sf , Fi_functors

b4a00883f358625923365ca1560c96edec172a52sf , Fi_predicates

b4a00883f358625923365ca1560c96edec172a52sf , Type

b4a00883f358625923365ca1560c96edec172a52sf , Unknown ]

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sftptp :: Parser [TPTP]

b4a00883f358625923365ca1560c96edec172a52sftptp = skip >> many (headerLine <|> include <|> formAnno

b4a00883f358625923365ca1560c96edec172a52sf <|> (newline >> skip >> return EmptyLine)) << eof

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfblank :: Parser p -> Parser ()

b4a00883f358625923365ca1560c96edec172a52sfblank = (>> skipMany1 whiteSpace)

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfszsOutput :: Parser ()

b4a00883f358625923365ca1560c96edec172a52sfszsOutput = blank (string "SZS") >> blank (string "output")

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfiproverSzsEnd :: Parser ()

b4a00883f358625923365ca1560c96edec172a52sfiproverSzsEnd = try $ char '%' >> skipMany whiteSpace >> szsOutput

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfotherCommentLine :: Parser ()

b4a00883f358625923365ca1560c96edec172a52sfotherCommentLine = (lookAhead iproverSzsEnd >> forget (char '%'))

b4a00883f358625923365ca1560c96edec172a52sf <|> forget commentLine

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfskipAllButEnd :: Parser ()

b4a00883f358625923365ca1560c96edec172a52sfskipAllButEnd = skipMany $ whiteSpace <|> commentBlock <|> otherCommentLine

b4a00883f358625923365ca1560c96edec172a52sf <|> forget newline

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sftptpModel :: Parser [(String, SPTerm)]

b4a00883f358625923365ca1560c96edec172a52sftptpModel = do

b4a00883f358625923365ca1560c96edec172a52sf _ <- manyTill anyChar

b4a00883f358625923365ca1560c96edec172a52sf (try (szsOutput >> blank (string "start"))

b4a00883f358625923365ca1560c96edec172a52sf <|> try (blank $ string "START OF MODEL"))

b4a00883f358625923365ca1560c96edec172a52sf _ <- manyTill anyChar newline

b4a00883f358625923365ca1560c96edec172a52sf skipAllButEnd

b4a00883f358625923365ca1560c96edec172a52sf ts <- many1 (formAnno << skipAllButEnd)

b4a00883f358625923365ca1560c96edec172a52sf (szsOutput >> blank (string "end"))

b4a00883f358625923365ca1560c96edec172a52sf <|> forget (string "END OF MODEL")

b4a00883f358625923365ca1560c96edec172a52sf return $ foldr (\ t l -> case t of

b4a00883f358625923365ca1560c96edec172a52sf FormAnno _ (Name n) _ e _ -> (n, e) : l

b4a00883f358625923365ca1560c96edec172a52sf _ -> l) [] ts

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfprintable :: Char -> Bool

b4a00883f358625923365ca1560c96edec172a52sfprintable c = let i = ord c in i >= 32 && i <= 126

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfcommentLine :: Parser String

b4a00883f358625923365ca1560c96edec172a52sfcommentLine = (char '%' <|> char '#') >> manyTill (satisfy printable) newline

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfheaderLine :: Parser TPTP

b4a00883f358625923365ca1560c96edec172a52sfheaderLine = fmap CommentLine $ commentLine << skip

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfcommentBlock :: Parser ()

b4a00883f358625923365ca1560c96edec172a52sfcommentBlock = forget $ plainBlock "/*" "*/"

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfwhiteSpace :: Parser ()

0662ed52e814f8f08ef0e09956413a792584eddffuankgwhiteSpace = forget $ oneOf "\r\t\v\f "

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfskip :: Parser ()

b4a00883f358625923365ca1560c96edec172a52sfskip = skipMany $ whiteSpace <|> commentBlock

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfskipAll :: Parser ()

b4a00883f358625923365ca1560c96edec172a52sfskipAll = skipMany $ whiteSpace <|> commentBlock <|> forget commentLine

b4a00883f358625923365ca1560c96edec172a52sf <|> forget newline

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sflexeme :: Parser a -> Parser a

b4a00883f358625923365ca1560c96edec172a52sflexeme = (<< skipAll)

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfkey :: Parser a -> Parser ()

0662ed52e814f8f08ef0e09956413a792584eddffuankgkey = (>> skipAll)

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfkeyChar :: Char -> Parser ()

b4a00883f358625923365ca1560c96edec172a52sfkeyChar = key . char

b4a00883f358625923365ca1560c96edec172a52sf

0662ed52e814f8f08ef0e09956413a792584eddffuankgcomma :: Parser ()

b4a00883f358625923365ca1560c96edec172a52sfcomma = keyChar ','

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfoParen :: Parser ()

b4a00883f358625923365ca1560c96edec172a52sfoParen = keyChar '('

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfcDotParen :: Parser ()

b4a00883f358625923365ca1560c96edec172a52sfcDotParen = string ")." >> skip >> option () (newline >> skip)

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfinclude :: Parser TPTP

0662ed52e814f8f08ef0e09956413a792584eddffuankginclude = do

b4a00883f358625923365ca1560c96edec172a52sf key $ tryString "include"

b4a00883f358625923365ca1560c96edec172a52sf oParen

b4a00883f358625923365ca1560c96edec172a52sf a <- atomicWord

b4a00883f358625923365ca1560c96edec172a52sf m <- optionL $ do

b4a00883f358625923365ca1560c96edec172a52sf comma

b4a00883f358625923365ca1560c96edec172a52sf sepBy1 aname comma

b4a00883f358625923365ca1560c96edec172a52sf cDotParen

b4a00883f358625923365ca1560c96edec172a52sf return $ Include (FileName a) m

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sf-- | does not allow leading zeros

b4a00883f358625923365ca1560c96edec172a52sfnatural :: Parser String

b4a00883f358625923365ca1560c96edec172a52sfnatural = string "0" <|> many1 digit

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfaname :: Parser Name

b4a00883f358625923365ca1560c96edec172a52sfaname = fmap Name (atomicWord <|> lexeme natural)

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfatomicWord :: Parser String

b4a00883f358625923365ca1560c96edec172a52sfatomicWord = lexeme $ lowerWord <|> singleQuoted

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfisUAlphaNum :: Char -> Bool

b4a00883f358625923365ca1560c96edec172a52sfisUAlphaNum c = isAlphaNum c || elem c "_$"

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfluWord :: Parser Char -> Parser String

b4a00883f358625923365ca1560c96edec172a52sfluWord p = do

b4a00883f358625923365ca1560c96edec172a52sf c <- p

b4a00883f358625923365ca1560c96edec172a52sf r <- many $ satisfy isUAlphaNum

b4a00883f358625923365ca1560c96edec172a52sf return $ c : r

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sflowerWord :: Parser String

b4a00883f358625923365ca1560c96edec172a52sflowerWord = luWord lower

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfupperWord :: Parser String

b4a00883f358625923365ca1560c96edec172a52sfupperWord = luWord upper

b4a00883f358625923365ca1560c96edec172a52sf

cf7ca2f9eaa6523fefcccba4287b91637391fb51fuankgsingleQuoted :: Parser String

b4a00883f358625923365ca1560c96edec172a52sfsingleQuoted =

b4a00883f358625923365ca1560c96edec172a52sf let quote = '\'' in fmap concat $

b4a00883f358625923365ca1560c96edec172a52sf char quote

b4a00883f358625923365ca1560c96edec172a52sf >> many (tryString "\\'" <|> single

b4a00883f358625923365ca1560c96edec172a52sf (satisfy $ \ c -> printable c && c /= quote))

b4a00883f358625923365ca1560c96edec172a52sf << char quote

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfformKind :: Parser FormKind

b4a00883f358625923365ca1560c96edec172a52sfformKind = choice $ map (\ k -> key (tryString $ show k) >> return k)

b4a00883f358625923365ca1560c96edec172a52sf [FofKind, CnfKind, FotKind]

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfrole :: Parser Role

b4a00883f358625923365ca1560c96edec172a52sfrole = choice $ map (\ r -> key (tryString $ showRole r)

b4a00883f358625923365ca1560c96edec172a52sf >> return r) allRoles

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfformAnno :: Parser TPTP

b4a00883f358625923365ca1560c96edec172a52sfformAnno = do

b4a00883f358625923365ca1560c96edec172a52sf k <- formKind

b4a00883f358625923365ca1560c96edec172a52sf oParen

b4a00883f358625923365ca1560c96edec172a52sf n <- aname

b4a00883f358625923365ca1560c96edec172a52sf comma

b4a00883f358625923365ca1560c96edec172a52sf r <- role

b4a00883f358625923365ca1560c96edec172a52sf comma

b4a00883f358625923365ca1560c96edec172a52sf f <- form

b4a00883f358625923365ca1560c96edec172a52sf m <- optionMaybe $ do

b4a00883f358625923365ca1560c96edec172a52sf comma

b4a00883f358625923365ca1560c96edec172a52sf gt <- fmap Source genTerm

b4a00883f358625923365ca1560c96edec172a52sf i <- optionMaybe $ do

b4a00883f358625923365ca1560c96edec172a52sf comma

b4a00883f358625923365ca1560c96edec172a52sf fmap Info genList

8ffac2c334103c0336602aaede650cb578611151fuankg return $ Annos gt i

8ffac2c334103c0336602aaede650cb578611151fuankg cDotParen

b4a00883f358625923365ca1560c96edec172a52sf return $ FormAnno k n r f m

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfcolon :: Parser ()

b4a00883f358625923365ca1560c96edec172a52sfcolon = keyChar ':'

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfgenTerm :: Parser GenTerm

b4a00883f358625923365ca1560c96edec172a52sfgenTerm = fmap GenTermList genList <|> do

b4a00883f358625923365ca1560c96edec172a52sf gd <- genData

b4a00883f358625923365ca1560c96edec172a52sf m <- optionMaybe $ do

b4a00883f358625923365ca1560c96edec172a52sf keyChar ':'

b4a00883f358625923365ca1560c96edec172a52sf genTerm

b4a00883f358625923365ca1560c96edec172a52sf return $ GenTerm gd m

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfgenData :: Parser GenData

b4a00883f358625923365ca1560c96edec172a52sfgenData = formData <|> otherData <|> do

b4a00883f358625923365ca1560c96edec172a52sf a <- fmap AWord atomicWord

b4a00883f358625923365ca1560c96edec172a52sf l <- optionL $ parens $ sepBy1 genTerm comma

b4a00883f358625923365ca1560c96edec172a52sf return $ GenData a l

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfotherData :: Parser GenData

b4a00883f358625923365ca1560c96edec172a52sfotherData = fmap OtherGenData $ (upperWord <|> real <|> distinct) << skipAll

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfdistinct :: Parser String

b4a00883f358625923365ca1560c96edec172a52sfdistinct =

b4a00883f358625923365ca1560c96edec172a52sf let dquot = '"' in

b4a00883f358625923365ca1560c96edec172a52sf enclosedBy (flat $ many1 $ tryString "\\\"" <|> single (satisfy (/= dquot)))

b4a00883f358625923365ca1560c96edec172a52sf $ char dquot

0662ed52e814f8f08ef0e09956413a792584eddffuankg

b4a00883f358625923365ca1560c96edec172a52sfdecimal :: Parser String

b4a00883f358625923365ca1560c96edec172a52sfdecimal = optionL (single $ oneOf "-+") <++> natural

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfreal :: Parser String

b4a00883f358625923365ca1560c96edec172a52sfreal = do

b4a00883f358625923365ca1560c96edec172a52sf d <- decimal

b4a00883f358625923365ca1560c96edec172a52sf f <- optionL $ char '.' <:> many1 digit

b4a00883f358625923365ca1560c96edec172a52sf e <- optionL $ oneOf "eE" <:> decimal

b4a00883f358625923365ca1560c96edec172a52sf return $ d ++ f ++ e

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sfformData :: Parser GenData

b4a00883f358625923365ca1560c96edec172a52sfformData =

0662ed52e814f8f08ef0e09956413a792584eddffuankg liftM GenFormData $ liftM2 FormData (char '$' >> formKind) $ parens form

b4a00883f358625923365ca1560c96edec172a52sf

b4a00883f358625923365ca1560c96edec172a52sforOp :: Parser ()

orOp = keyChar '|'

andOp :: Parser ()

andOp = keyChar '&'

pToken :: Parser String -> Parser Token

pToken = liftM2 (\ p s -> Token s (Range [p])) getPos . (<< skipAll)

form :: Parser SPTerm

form = do

u <- unitary

do orOp

us <- sepBy1 unitary orOp

return $ compTerm SPOr $ u : us

<|> do

andOp

us <- sepBy1 unitary andOp

return $ compTerm SPAnd $ u : us

<|> do

o <- choice $ map (pToken . tryString)

["<=>", "=>", "<=", "<~>", "~|", "~&"]

u2 <- unitary

let s = tokStr o

a = [u, u2]

return $ case lookup s $ zip ["<=>", "=>", "<="]

[SPEquiv, SPImplies, SPImplied] of

Just ks -> compTerm ks a

Nothing -> case lookup s $ zip ["<~>", "~|", "~&"]

[SPEquiv, SPOr, SPAnd] of

Just ks -> compTerm SPNot [compTerm ks a]

Nothing -> compTerm (SPCustomSymbol o) a

<|> return u

unitary :: Parser SPTerm

unitary = parens form <|> quantForm <|> unaryForm <|> atomicForm

quantForm :: Parser SPTerm

quantForm = do

q <- lexeme $ (char '!' >> return SPForall)

<|> (char '?' >> return SPExists)

vs <- brackets $ sepBy1 variable comma

colon

u <- unitary

return SPQuantTerm

{ quantSym = q

, variableList = vs

, qFormula = u }

unaryForm :: Parser SPTerm

unaryForm = do

keyChar '~'

u <- unitary

return $ compTerm SPNot [u]

atomicForm :: Parser SPTerm

atomicForm = do

t <- term

do key $ try $ char '=' << notFollowedBy (char '>' )

t2 <- term

return $ mkEq t t2

<|> do

key $ tryString "!="

t2 <- term

return $ compTerm SPNot [mkEq t t2]

<|> return t

variable :: Parser SPTerm

variable = fmap (simpTerm . SPCustomSymbol) $ pToken upperWord

definedAtom :: Parser SPTerm

definedAtom = fmap (simpTerm . SPCustomSymbol) $ pToken $ real <|> distinct

functor :: Parser SPSymbol

functor = fmap (\ t -> fromMaybe (SPCustomSymbol t)

$ lookup (tokStr t)

$ zip ["$true", "$false", "$equal"] [SPTrue, SPFalse, SPEqual])

$ pToken

$ lowerWord <|> singleQuoted <|> dollarWord

-- system and defined words

dollarWord :: Parser String

dollarWord = do

d <- tryString "$$" <|> string "$"

w <- lowerWord

return $ d ++ w

-- mixed plain, defined and system terms

term :: Parser SPTerm

term = variable <|> definedAtom <|> do

f <- functor

as <- optionL $ parens $ sepBy1 term comma

return $ compTerm f as

brackets :: Parser a -> Parser a

brackets p = do

keyChar '['

a <- p

keyChar ']'

return a

parens :: Parser a -> Parser a

parens p = do

oParen

a <- p

keyChar ')'

return a

genList :: Parser [GenTerm]

genList = brackets $ sepBy genTerm comma

prTPTPs :: [TPTP] -> Doc.Doc

prTPTPs = Doc.vcat . map prTPTP

prTPTP :: TPTP -> Doc.Doc

prTPTP p = case p of

FormAnno k (Name n) r t m ->

Doc.text (show k)

Doc.<> Doc.parens

(Doc.sepByCommas $

[ Doc.text n

, Doc.text $ showRole r

, printTPTP t]

++ maybe [] ppAnnos m)

Doc.<> Doc.dot

Include (FileName f) ns ->

Doc.text "include"

Doc.<> Doc.parens

(Doc.sepByCommas $

ppName f : if null ns then [] else

[Doc.brackets $ Doc.sepByCommas $ map ppAName ns])

Doc.<> Doc.dot

CommentLine l -> Doc.text $ '%' : l

EmptyLine -> Doc.text ""

ppName :: String -> Doc.Doc

ppName s = (if all isUAlphaNum s then id else Doc.quotes) $ Doc.text s

ppAName :: Name -> Doc.Doc

ppAName (Name n) = ppName n

ppAnnos :: Annos -> [Doc.Doc]

ppAnnos (Annos (Source gt) m) = ppGenTerm gt : maybe [] ppInfo m

ppInfo :: Info -> [Doc.Doc]

ppInfo (Info l) = [ppGenList l]

ppList :: [GenTerm] -> Doc.Doc

ppList = Doc.sepByCommas . map ppGenTerm

ppGenList :: [GenTerm] -> Doc.Doc

ppGenList = Doc.brackets . ppList

ppGenTerm :: GenTerm -> Doc.Doc

ppGenTerm gt = case gt of

GenTerm gd m -> let d = ppGenData gd in case m of

Just t -> Doc.fsep [d Doc.<> Doc.colon, ppGenTerm t]

Nothing -> d

GenTermList l -> ppGenList l

ppGenData :: GenData -> Doc.Doc

ppGenData gd = case gd of

GenData (AWord aw) l -> ppName aw Doc.<>

if null l then Doc.empty else Doc.parens $ ppList l

OtherGenData s -> Doc.text s

GenFormData (FormData k t) ->

Doc.text ('$' : show k)

Doc.<> Doc.parens (printTPTP t)