Copyright	(c) Rene Wagner, Rainer Grabbe, Uni Bremen 2005-2006
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	unknown
Safe Haskell	None

SoftFOL.PrintTPTP

Description

Pretty printing for SoftFOL signatures in TPTP syntax. Refer to http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html for the TPTP syntax documentation.

Synopsis

Documentation

class PrintTPTP a where

This type class allows pretty printing in TPTP syntax of instantiated data types

Methods

printTPTP :: a -> Doc

Instances

PrintTPTP SPSettingBody
PrintTPTP SPSetting
PrintTPTP SPLogState	Creates a Doc from an `SPLogState`.
PrintTPTP SPDescription	Creates a Doc from a SoftFOL description.
PrintTPTP SPSymbol	Creates a Doc from a SoftFOL Symbol.
PrintTPTP SPQuantSym	Creates a Doc from a SoftFOL Quantifier Symbol.
PrintTPTP SPTerm	Creates a Doc from a SoftFOL Term.
PrintTPTP SPOriginType	Creates a Doc from a SoftFOL Origin Type.
PrintTPTP SPFormulaList	Creates a Doc from a SoftFOL Formula List.
PrintTPTP SPDeclaration	Creates a Doc from a SoftFOL Declaration. A subsort declaration will be rewritten as a special SPQuantTerm.
PrintTPTP SPLogicalPart	Creates a Doc from a SoftFOL Logical Part.
PrintTPTP SPProblem	Creates a Doc from a SoftFOL Problem.
PrintTPTP Sign

separator :: String

Helper function. Generates a separating comment line.

printFormula :: SPOriginType -> SPFormula -> Doc

Creates a Doc from a SoftFOL Formula. Needed since SPFormula is just a 'type SPFormula = Named SPTerm' and thus instanciating PrintTPTP is not possible.

printTermList :: SPSymbol -> [SPTerm] -> Doc

Creates a Doc from a list of SoftFOL Terms connected by a SoftFOL Symbol.

printCommaSeparated :: [SPTerm] -> Doc

Helper function. Generates a comma separated list of SoftFOL Terms as a Doc.

parPrintTPTP :: SPTerm -> Doc

isUnitary :: SPTerm -> Bool

binLogOps :: [SPSymbol]

spCommentText :: String -> String -> Doc

Helper function. Creates a formatted comment output for a description field. On left side will be displayed the field's name, on right side its content.