{- |

Module : ./THF/PrintTHF.hs

Description : A printer for the TPTP-THF Syntax

Copyright : (c) A. Tsogias, DFKI Bremen 2011

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Alexis.Tsogias@dfki.de

Stability : provisional

Portability : portable

A printer for the TPTP-THF Input Syntax v5.1.0.2 taken from

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

-}

module THF.PrintTHF where

import THF.As

import Data.Char

import Common.Doc

import Common.DocUtils

import Common.Id (Token)

{- -----------------------------------------------------------------------------

Pretty Instances for the THF and THF0 Syntax.

Most methods match those of As.hs

----------------------------------------------------------------------------- -}

printTPTPTHF :: [TPTP_THF] -> Doc

printTPTPTHF [] = empty

printTPTPTHF (t : rt) = case t of

TPTP_THF_Annotated_Formula {} -> pretty t $++$ printTPTPTHF rt

_ -> pretty t $+$ printTPTPTHF rt

instance Pretty TPTP_THF where

pretty t = case t of

TPTP_THF_Annotated_Formula n fr f a ->

text "thf" <> parens (pretty n <> comma

<+> pretty fr <> comma

<+> pretty f <> pretty a)

<> text "."

TPTP_Include i -> pretty i

TPTP_Comment c -> pretty c

TPTP_Defined_Comment dc -> pretty dc

TPTP_System_Comment sc -> pretty sc

TPTP_Header h -> prettyHeader h

prettyHeader :: [Comment] -> Doc

prettyHeader = foldr (($+$) . pretty) empty

instance Pretty Comment where

pretty c = case c of

Comment_Line s -> text "%" <> (text . show) s

Comment_Block sl -> text "/*"

$+$ prettyCommentBlock (lines $ show sl)

$+$ text "*/"

instance Pretty DefinedComment where

pretty dc = case dc of

Defined_Comment_Line s -> text "%$" <> (text . show) s

Defined_Comment_Block sl -> text "/*$"

$+$ prettyCommentBlock (lines $ show sl)

$+$ text "*/"

instance Pretty SystemComment where

pretty sc = case sc of

System_Comment_Line s -> text "%$$" <> (text . show) s

System_Comment_Block sl -> text "/*$$"

$+$ prettyCommentBlock (lines $ show sl)

$+$ text "*/"

prettyCommentBlock :: [String] -> Doc

prettyCommentBlock = foldr (($+$) . text) empty

instance Pretty Include where

pretty (I_Include fn nl) = text "include" <> parens (prettySingleQuoted fn

<> maybe empty (\ c -> comma <+> prettyNameList c) nl) <> text "."

instance Pretty Annotations where

pretty a = case a of

Annotations s o -> comma <+> pretty s <> prettyOptionalInfo o

Null -> empty

instance Pretty FormulaRole where

pretty fr = text $ map toLower (show fr)

instance Pretty THFFormula where

pretty f = case f of

TF_THF_Logic_Formula lf -> pretty lf

TF_THF_Sequent s -> pretty s

T0F_THF_Typed_Const tc -> pretty tc

instance Pretty THFLogicFormula where

pretty lf = case lf of

TLF_THF_Binary_Formula bf -> pretty bf

TLF_THF_Unitary_Formula uf -> pretty uf

TLF_THF_Type_Formula tf -> pretty tf

TLF_THF_Sub_Type st -> pretty st

instance Pretty THFBinaryFormula where

pretty bf = case bf of

TBF_THF_Binary_Tuple bt -> pretty bt

TBF_THF_Binary_Type bt -> pretty bt

TBF_THF_Binary_Pair uf1 pc uf2 ->

pretty uf1 <+> pretty pc <+> pretty uf2

instance Pretty THFBinaryTuple where

pretty bt = case bt of

TBT_THF_Or_Formula ufl -> sepBy (map pretty ufl) orSign

TBT_THF_And_Formula ufl -> sepBy (map pretty ufl) andSign

TBT_THF_Apply_Formula ufl -> sepBy (map pretty ufl) applySign

instance Pretty THFUnitaryFormula where

pretty tuf = case tuf of

TUF_THF_Quantified_Formula qf -> pretty qf

TUF_THF_Unary_Formula uc lf -> pretty uc <+> parens (pretty lf)

TUF_THF_Atom a -> pretty a

TUF_THF_Tuple t -> prettyTuple t

TUF_THF_Conditional lf1 lf2 lf3 ->

text "$itef" <> parens (pretty lf1

<> comma <+> pretty lf2

<> comma <+> pretty lf3)

TUF_THF_Logic_Formula_Par l -> parens (pretty l)

T0UF_THF_Abstraction vl uf -> text "^" <+>

brackets (prettyVariableList vl) <+> text ":" <+> pretty uf

instance Pretty THFQuantifiedFormula where

pretty qf = case qf of

TQF_THF_Quantified_Formula tq vl uf -> pretty tq <+>

brackets (prettyVariableList vl) <+> text ":" <+> pretty uf

T0QF_THF_Quantified_Var q vl uf -> pretty q <+>

brackets (prettyVariableList vl) <+> text ":" <+> pretty uf

T0QF_THF_Quantified_Novar tq uf ->

pretty tq <+> parens (pretty uf)

prettyVariableList :: THFVariableList -> Doc

prettyVariableList vl = sepByCommas (map pretty vl)

instance Pretty THFVariable where

pretty v = case v of

TV_THF_Typed_Variable va tlt -> prettyUpperWord va

<+> text ":" <+> pretty tlt

TV_Variable var -> prettyUpperWord var

instance Pretty THFTypedConst where

pretty ttc = case ttc of

T0TC_Typed_Const c tlt -> prettyConstant c <+> text ":"

<+> pretty tlt

T0TC_THF_TypedConst_Par tc -> parens (pretty tc)

instance Pretty THFTypeFormula where

pretty ttf = case ttf of

TTF_THF_Type_Formula tf tlt -> pretty tf <+> text ":" <+> pretty tlt

TTF_THF_Typed_Const c tlt -> prettyConstant c <+> text ":"

<+> pretty tlt

instance Pretty THFTypeableFormula where

pretty tbf = case tbf of

TTyF_THF_Atom a -> pretty a

TTyF_THF_Tuple t -> prettyTuple t

TTyF_THF_Logic_Formula lf -> parens $ pretty lf

instance Pretty THFSubType where

pretty (TST_THF_Sub_Type c1 c2) =

prettyConstant c1 <+> text "<<" <+> prettyConstant c2

instance Pretty THFTopLevelType where

pretty tlt = case tlt of

TTLT_THF_Logic_Formula lf -> pretty lf

T0TLT_Constant c -> prettyConstant c

T0TLT_Variable v -> prettyUpperWord v

T0TLT_Defined_Type dt -> pretty dt

T0TLT_System_Type st -> prettyAtomicSystemWord st

T0TLT_THF_Binary_Type bt -> pretty bt

instance Pretty THFUnitaryType where

pretty ut = case ut of

TUT_THF_Unitary_Formula uf -> pretty uf

T0UT_Constant c -> prettyConstant c

T0UT_Variable v -> prettyUpperWord v

T0UT_Defined_Type dt -> pretty dt

T0UT_System_Type st -> prettyAtomicSystemWord st

T0UT_THF_Binary_Type_Par bt -> parens (pretty bt)

instance Pretty THFBinaryType where

pretty tbt = case tbt of

TBT_THF_Mapping_Type utl -> sepBy (map pretty utl) arrowSign

TBT_THF_Xprod_Type utl -> sepBy (map pretty utl) starSign

TBT_THF_Union_Type utl -> sepBy (map pretty utl) plusSign

T0BT_THF_Binary_Type_Par bt -> parens (pretty bt)

instance Pretty THFAtom where

pretty a = case a of

TA_Term t -> pretty t

TA_THF_Conn_Term ct -> pretty ct

TA_Defined_Type dt -> pretty dt

TA_Defined_Plain_Formula dp -> pretty dp

TA_System_Type st -> prettyAtomicSystemWord st

TA_System_Atomic_Formula st -> pretty st

T0A_Constant c -> prettyConstant c

T0A_Defined_Constant dc -> prettyAtomicDefinedWord dc

T0A_System_Constant sc -> prettyAtomicSystemWord sc

T0A_Variable v -> prettyUpperWord v

prettyTuple :: THFTuple -> Doc

prettyTuple ufl = brackets $ sepByCommas (map pretty ufl)

instance Pretty THFSequent where

pretty (TS_THF_Sequent_Par s) = parens $ pretty s

pretty (TS_THF_Sequent t1 t2) =

prettyTuple t1 <+> text "-->" <+> prettyTuple t2

instance Pretty THFConnTerm where

pretty ct = case ct of

TCT_THF_Pair_Connective pc -> pretty pc

TCT_Assoc_Connective ac -> pretty ac

TCT_THF_Unary_Connective uc -> pretty uc

T0CT_THF_Quantifier q -> pretty q

instance Pretty THFQuantifier where

pretty q = case q of

TQ_ForAll -> text "!"

TQ_Exists -> text "?"

TQ_Lambda_Binder -> text "^"

TQ_Dependent_Product -> text "!>"

TQ_Dependent_Sum -> text "?*"

TQ_Indefinite_Description -> text "@+"

TQ_Definite_Description -> text "@-"

T0Q_PiForAll -> text "!!"

T0Q_SigmaExists -> text "??"

instance Pretty Quantifier where

pretty q = case q of

T0Q_ForAll -> text "!"

T0Q_Exists -> text "?"

instance Pretty THFPairConnective where

pretty pc = case pc of

Infix_Equality -> text "="

Infix_Inequality -> text "!="

Equivalent -> text "<=>"

Implication -> text "=>"

IF -> text "<="

XOR -> text "<~>"

NOR -> text "~|"

NAND -> text "~&"

instance Pretty THFUnaryConnective where

pretty uc = case uc of

Negation -> text "~"

PiForAll -> text "!!"

SigmaExists -> text "??"

instance Pretty AssocConnective where

pretty AND = text "&"

pretty OR = text "|"

instance Pretty DefinedType where

pretty DT_oType = text "$o"

pretty dt = text $ '$' : drop 3 (show dt)

instance Pretty DefinedPlainFormula where

pretty dpf = case dpf of

DPF_Defined_Prop dp -> pretty dp

DPF_Defined_Formula dp a -> pretty dp <> parens (prettyArguments a)

instance Pretty DefinedProp where

pretty DP_True = text "$true"

pretty DP_False = text "$false"

instance Pretty DefinedPred where

pretty dp = text $ '$' : map toLower (show dp)

instance Pretty Term where

pretty t = case t of

T_Function_Term ft -> pretty ft

T_Variable v -> prettyUpperWord v

instance Pretty FunctionTerm where

pretty ft = case ft of

FT_Plain_Term pt -> pretty pt

FT_Defined_Term dt -> pretty dt

FT_System_Term st -> pretty st

instance Pretty PlainTerm where

pretty pt = case pt of

PT_Constant c -> prettyConstant c

PT_Plain_Term f a -> pretty f <> parens (prettyArguments a)

prettyConstant :: Constant -> Doc

prettyConstant = pretty

instance Pretty DefinedTerm where

pretty dt = case dt of

DT_Defined_Atom da -> pretty da

DT_Defined_Atomic_Term dpt -> pretty dpt

instance Pretty DefinedAtom where

pretty da = case da of

DA_Number n -> pretty n

DA_Distinct_Object dio -> prettyDistinctObject dio

instance Pretty DefinedPlainTerm where

pretty dpt = case dpt of

DPT_Defined_Constant df -> pretty df

DPT_Defined_Function df a -> pretty df <> parens (prettyArguments a)

instance Pretty DefinedFunctor where

pretty df = text $ '$' : map toLower (show df)

instance Pretty SystemTerm where

pretty st = case st of

ST_System_Constant sf -> prettyAtomicSystemWord sf

ST_System_Term sf a -> prettyAtomicSystemWord sf

<> parens (prettyArguments a)

prettyArguments :: Arguments -> Doc

prettyArguments = sepByCommas . map pretty

instance Pretty PrincipalSymbol where

pretty ps = case ps of

PS_Functor f -> pretty f

PS_Variable v -> prettyUpperWord v

instance Pretty Source where

pretty s = case s of

S_Dag_Source ds -> pretty ds

S_Internal_Source it oi -> text "introduced" <> parens (

pretty it <> prettyOptionalInfo oi)

S_External_Source es -> pretty es

S_Sources ss -> sepByCommas (map pretty ss)

S_Unknown -> text "unknown"

instance Pretty DagSource where

pretty ds = case ds of

DS_Name n -> pretty n

DS_Inference_Record aw ui pl -> text "inference"

<> parens (pretty aw <> comma <+> prettyUsefulInfo ui

<> comma <+> brackets (sepByCommas (map pretty pl)))

instance Pretty ParentInfo where

pretty (PI_Parent_Info s mgl) =

let gl = maybe empty (\ c -> text ":" <> prettyGeneralList c) mgl

in pretty s <> gl

instance Pretty IntroType where

pretty it = text (drop 3 (show it))

instance Pretty ExternalSource where

pretty es = case es of

ES_File_Source fs -> pretty fs

ES_Theory tn oi -> text "theory" <> parens (

pretty tn <> prettyOptionalInfo oi)

ES_Creator_Source aw oi -> text "creator" <> parens (

pretty aw <> prettyOptionalInfo oi)

instance Pretty FileSource where

pretty (FS_File fn mn) =

let n = maybe empty (\ c -> comma <+> pretty c) mn

in text "file" <> parens (prettySingleQuoted fn <> n)

instance Pretty TheoryName where

pretty tn = text $ map toLower (show tn)

prettyOptionalInfo :: OptionalInfo -> Doc

prettyOptionalInfo = maybe empty (\ ui -> comma <+> prettyUsefulInfo ui)

prettyUsefulInfo :: UsefulInfo -> Doc

prettyUsefulInfo = brackets . sepByCommas . map pretty

instance Pretty InfoItem where

pretty ii = case ii of

II_Formula_Item fi -> pretty fi

II_Inference_Item infi -> pretty infi

II_General_Function gf -> pretty gf

instance Pretty FormulaItem where

pretty fi = case fi of

FI_Description_Item aw -> text "description" <> parens (pretty aw)

FI_Iquote_Item aw -> text "iquote" <> parens (pretty aw)

instance Pretty InferenceItem where

pretty ii = case ii of

II_Inference_Status is -> pretty is

II_Assumptions_Record nl -> text "assumptions"

<> parens (brackets (prettyNameList nl))

II_New_Symbol_Record aw psl -> text "new_symbols" <> parens (pretty aw

<> comma <+> brackets (sepByCommas (map pretty psl)))

II_Refutation fs -> text "refutation" <> parens (pretty fs)

instance Pretty InferenceStatus where

pretty is = case is of

IS_Status s -> text "status" <> parens (pretty s)

IS_Inference_Info aw1 aw2 gl -> pretty aw1 <> parens (pretty aw2

<> comma <+> prettyGeneralList gl)

instance Pretty StatusValue where

pretty sv = text $ map toLower (show sv)

prettyNameList :: NameList -> Doc

prettyNameList = sepByCommas . map pretty

instance Pretty GeneralTerm where

pretty gt = case gt of

GT_General_Data gd -> pretty gd

GT_General_Data_Term gd gt1 -> pretty gd <+> text ":" <+> pretty gt1

GT_General_List gl -> prettyGeneralList gl

instance Pretty GeneralData where

pretty gd = case gd of

GD_Atomic_Word aw -> pretty aw

GD_General_Function gf -> pretty gf

GD_Variable v -> prettyUpperWord v

GD_Number n -> pretty n

GD_Distinct_Object dio -> prettyDistinctObject dio

GD_Formula_Data fd -> pretty fd

GD_Bind v fd -> text "bind" <> parens (

prettyUpperWord v <> comma <+> pretty fd)

instance Pretty GeneralFunction where

pretty (GF_General_Function aw gts) =

pretty aw <> parens (prettyGeneralTerms gts)

instance Pretty FormulaData where

pretty (THF_Formula thff) = text "$thf" <> parens (pretty thff)

prettyGeneralList :: GeneralList -> Doc

prettyGeneralList = brackets . prettyGeneralTerms

prettyGeneralTerms :: GeneralTerms -> Doc

prettyGeneralTerms = sepByCommas . map pretty

instance Pretty Name where

pretty n = case n of

N_Atomic_Word a -> pretty a

N_Integer s -> text $ show s

T0N_Unsigned_Integer s -> text $ show s

instance Pretty AtomicWord where

pretty a = case a of

A_Single_Quoted s -> prettySingleQuoted s

A_Lower_Word l -> prettyLowerWord l

prettyAtomicSystemWord :: Token -> Doc

prettyAtomicSystemWord asw = text ("$$" ++ show asw)

prettyAtomicDefinedWord :: Token -> Doc

prettyAtomicDefinedWord adw = text ('$' : show adw)

instance Pretty Number where

pretty n = case n of

Num_Integer i -> text $ show i

Num_Rational ra -> text $ show ra

Num_Real re -> text $ show re

prettySingleQuoted :: Token -> Doc

prettySingleQuoted s = text "\'" <> (text . show) s <> text "\'"

prettyDistinctObject :: Token -> Doc

prettyDistinctObject s = text "\"" <> (text . show) s <> text "\""

prettyLowerWord :: Token -> Doc

prettyLowerWord uw' = let uw = show uw' in text (toLower (head uw) : tail uw)

prettyUpperWord :: Token -> Doc

prettyUpperWord uw' = let uw = show uw' in text (toUpper (head uw) : tail uw)

orSign :: Doc

orSign = text "|"

andSign :: Doc

andSign = text "&"

applySign :: Doc

applySign = text "@"

arrowSign :: Doc

arrowSign = text ">"

starSign :: Doc

starSign = text "*"

plusSign :: Doc

plusSign = text "+"

sepBy :: [Doc] -> Doc -> Doc

sepBy ls s = case ls of

(c : []) -> c

(c : d) -> c <+> s <+> sepBy d s

[] -> empty