PrintTHF.hs revision e9458b1a7a19a63aa4c179f9ab20f4d50681c168
{- |
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