hets/THF/PrintTHF.hs

	PrintTHF.hs revision 8fb127028cb7dd361e348a3252e33487f73428bc
{- |
Module      :  $Header$
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 = 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