PrintTHF.hs revision fc09e0a6af734edbd944dd8082bb51985c233b43
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias{- |
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasModule : $Header$
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasDescription : A printer for the TPTP-THF Syntax
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis TsogiasCopyright : (c) A. Tsogias, DFKI Bremen 2011
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasLicense : GPLv2 or higher, see LICENSE.txt
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
fc09e0a6af734edbd944dd8082bb51985c233b43Alexis TsogiasMaintainer : Alexis.Tsogias@dfki.de
fc09e0a6af734edbd944dd8082bb51985c233b43Alexis TsogiasStability : provisional
fc09e0a6af734edbd944dd8082bb51985c233b43Alexis TsogiasPortability : portable
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis TsogiasA printer for the TPTP-THF Input Syntax v5.1.0.2 taken from
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias<http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html>
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias-}
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasmodule THF.PrintTHF where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasimport THF.As
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasimport Data.Char
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasimport Common.Doc
1e622ddf5a057555db1924ddc88475c695c6f7f2Alexis Tsogias--import Common.DocUtils
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintTPTPTHF :: [TPTP_THF] -> Doc
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintTPTPTHF [] = empty
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintTPTPTHF (t : rt) = case t of
1e622ddf5a057555db1924ddc88475c695c6f7f2Alexis Tsogias TPTP_THF_Annotated_Formula _ _ _ _ -> printTHF t $++$ printTPTPTHF rt
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias _ -> printTHF t $+$ printTPTPTHF rt
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasclass PrintTHF a where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF :: a -> Doc
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF TPTP_THF where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF t = case t of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TPTP_THF_Annotated_Formula n fr f a ->
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias text "thf" <> parens (printTHF n <> comma
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias <+> printTHF fr <> comma
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias <+> printTHF f <> printTHF a)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias <> text "."
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TPTP_Include i -> printTHF i
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TPTP_Comment c -> printTHF c
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TPTP_Defined_Comment dc -> printTHF dc
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TPTP_System_Comment sc -> printTHF sc
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF Comment where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF c = case c of
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias Comment_Line s -> text "%" <> text s
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias Comment_Block sl -> text "/*"
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias $+$ printCommentBlock sl
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias $+$ text "*/"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF DefinedComment where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF dc = case dc of
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias Defined_Comment_Line s -> text "%$" <> text s
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias Defined_Comment_Block sl -> text "/*$"
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias $+$ printCommentBlock sl
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias $+$ text "*/"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF SystemComment where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF sc = case sc of
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias System_Comment_Line s -> text "%$$" <> text s
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias System_Comment_Block sl -> text "/*$$"
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias $+$ printCommentBlock sl
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias $+$ text "*/"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintCommentBlock :: [String] -> Doc
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis TsogiasprintCommentBlock [] = empty
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis TsogiasprintCommentBlock (s : rt) = text s $+$ printCommentBlock rt
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF Include where
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias printTHF (I_Include fn nl) = text "include" <> parens (printFileName fn
4cea468e955597a7069faba3f43f27e913f2b651Alexis Tsogias <> maybe empty (\c -> comma <+> printNameList c) nl) <> text "."
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF Annotations where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF a = case a of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias Annotations s o -> comma <+> printTHF s <> printOptionalInfo o
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias Null -> empty
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF FormulaRole where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF fr = text $ map toLower (show fr)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF THFFormula where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF f = case f of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TF_THF_Logic_Formula lf -> printTHF lf
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TF_THF_Sequent s -> printTHF s
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF THFLogicFormula where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF lf = case lf of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TLF_THF_Binary_Formula bf -> printTHF bf
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TLF_THF_Unitary_Formula uf -> printTHF uf
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TLF_THF_Type_Formula tf -> printTHF tf
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TLF_THF_Sub_Type st -> printTHF st
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF THFBinaryFormula where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF bf = case bf of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TBF_THF_Binary_Tuple bt -> printTHF bt
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TBF_THF_Binary_Type bt -> printTHF bt
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TBF_THF_Binary_Pair uf1 pc uf2 ->
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF uf1 <+> printTHF pc <+> printTHF uf2
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF THFBinaryTuple where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF bt = case bt of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TBT_THF_Or_Formula uf ufl ->
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias sepBy (map printTHF (uf : ufl)) orSign
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TBT_THF_And_Formula uf ufl ->
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias sepBy (map printTHF (uf : ufl)) andSign
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TBT_THF_Apply_Formula uf ufl ->
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias sepBy (map printTHF (uf : ufl)) applySign
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF THFUnitaryFormula where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF uf = case uf of
1e622ddf5a057555db1924ddc88475c695c6f7f2Alexis Tsogias TUF_THF_Quantified_Formula q vl uf1 ->
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF q <+> brackets (sepByCommas (map printTHF vl))
1e622ddf5a057555db1924ddc88475c695c6f7f2Alexis Tsogias <+> text ":" <+> printTHF uf1
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TUF_THF_Unary_Formula uc lf ->
4cea468e955597a7069faba3f43f27e913f2b651Alexis Tsogias printTHF uc <+> parens (printTHF lf)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TUF_THF_Atom a -> printTHF a
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TUF_THF_Tuple t -> printTHFTuple t
1e622ddf5a057555db1924ddc88475c695c6f7f2Alexis Tsogias TUF_THF_Let dvl uf2 ->
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias text ":=" <+> brackets (sepByCommas (map printTHF dvl))
1e622ddf5a057555db1924ddc88475c695c6f7f2Alexis Tsogias <+> text ":" <+> printTHF uf2
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TUF_THF_Conditional lf1 lf2 lf3 ->
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias text "$itef" <> parens (printTHF lf1
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias <> comma <+> printTHF lf2
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias <> comma <+> printTHF lf3)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TUF_THF_Logic_Formula_Par l -> parens (printTHF l)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF THFVariable where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF v = case v of
1e622ddf5a057555db1924ddc88475c695c6f7f2Alexis Tsogias TV_THF_Typed_Variable va tlt -> printVariable va
e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias <+> text ":" <+> printTHF tlt
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TV_Variable var -> printVariable var
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF THFTypeFormula where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF tf = case tf of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TTF_THF_Type_Formula tbf tlt ->
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF tbf <+> text ":" <+> printTHF tlt
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TTF_THF_Role_Type c tlt ->
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF c <+> text ":" <+> printTHF tlt
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF THFTypeableFormula where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF tbf = case tbf of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TTyF_THF_Atom a -> printTHF a
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TTyF_THF_Tuple t -> printTHFTuple t
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TTyF_THF_Logic_Formula lf -> parens $ printTHF lf
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF THFSubType where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF (TST_THF_Sub_Type c1 c2) =
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF c1 <+> text "<<" <+> printTHF c2
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintTHFTopLevelType :: THFTopLevelType -> Doc
4cea468e955597a7069faba3f43f27e913f2b651Alexis TsogiasprintTHFTopLevelType = printTHF
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintTHFUnitaryType :: THFUnitaryType -> Doc
4cea468e955597a7069faba3f43f27e913f2b651Alexis TsogiasprintTHFUnitaryType = printTHF
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF THFBinaryType where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF bt = case bt of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TBT_THF_Mapping_Type ut utl -> sepBy (map printTHF (ut : utl)) arrowSign
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TBT_THF_Xprod_Type ut utl -> sepBy (map printTHF (ut : utl)) starSign
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TBT_THF_Union_Type ut utl -> sepBy (map printTHF (ut : utl)) plusSign
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF THFAtom where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF a = case a of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TA_Term t -> printTHF t
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TA_THF_Conn_Term ct -> printTHF ct
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TA_Defined_Type dt -> printTHF dt
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TA_Defined_Plain_Formula dp -> printTHF dp
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TA_System_Type asw -> printAtomicSystemWord asw
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TA_System_Atomic_Formula st -> printTHF st
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintTHFTuple :: THFTuple -> Doc
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintTHFTuple ufl = brackets $ sepByCommas (map printTHF ufl)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF THFDefinedVar where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF dv = case dv of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TDV_THF_Defined_Var v lf ->
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF v <+> text ":=" <+> printTHF lf
4cea468e955597a7069faba3f43f27e913f2b651Alexis Tsogias TDV_THF_Defined_Var_Par d -> parens (printTHF d)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF THFSequent where
4cea468e955597a7069faba3f43f27e913f2b651Alexis Tsogias printTHF (TS_THF_Sequent_Par s) = parens $ printTHF s
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF (TS_THF_Sequent t1 t2) =
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHFTuple t1 <+> text "-->" <+> printTHFTuple t2
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF THFConnTerm where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF ct = case ct of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TCT_THF_Pair_Connective pc -> printTHF pc
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TCT_Assoc_Connective ac -> printTHF ac
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias TCT_THF_Unary_Connective uc -> printTHF uc
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF THFQuantifier where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF q = case q of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias ForAll -> text "!"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias Exists -> text "?"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias Lambda_Binder -> text "^"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias Dependent_Product -> text "!>"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias Dependent_Sum -> text "?*"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias Indefinite_Description -> text "@+"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias Definite_Description -> text "@-"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF THFPairConnective where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF pc = case pc of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias Infix_Equality -> text "="
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias Infix_Inequality -> text "!="
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias Equivalent -> text "<=>"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias Implication -> text "=>"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias IF -> text "<="
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias XOR -> text "<~>"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias NOR -> text "~|"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias NAND -> text "~&"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF THFUnaryConnective where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF uc = case uc of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias Negation -> text "~"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias PiForAll -> text "!!"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias SigmaExists -> text "??"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF AssocConnective where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF AND = text "&"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF OR = text "|"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF DefinedType where
4cea468e955597a7069faba3f43f27e913f2b651Alexis Tsogias printTHF dt = text $ "$" ++ drop 3 (show dt)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF DefinedPlainFormula where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF dpf = case dpf of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias DPF_Defined_Prop dp -> printTHF dp
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias DPF_Defined_Formula dp a -> printTHF dp <> parens (printArguments a)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF DefinedProp where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF DP_True = text "$true"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF DP_False = text "$false"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF DefinedPred where
4cea468e955597a7069faba3f43f27e913f2b651Alexis Tsogias printTHF dp = text $ "$" ++ map toLower (show dp)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF Term where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF t = case t of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias T_Function_Term ft -> printTHF ft
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias T_Variable v -> printVariable v
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF FunctionTerm where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF ft = case ft of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias FT_Plain_Term pt -> printTHF pt
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias FT_Defined_Term dt -> printTHF dt
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias FT_System_Term st ->printTHF st
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF PlainTerm where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF pt = case pt of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias PT_Constant c -> printConstant c
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias PT_Plain_Term f a -> printTPTPFunctor f <> parens (printArguments a)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintConstant :: Constant -> Doc
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintConstant = printTPTPFunctor
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintTPTPFunctor :: TPTPFunctor -> Doc
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintTPTPFunctor = printTHF
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF DefinedTerm where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF dt = case dt of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias DT_Defined_Atom da -> printTHF da
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias DT_Defined_Atomic_Term dpt -> printTHF dpt
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF DefinedAtom where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF da = case da of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias DA_Number n -> printTHF n
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias DA_Distinct_Object dio -> printDistinctObject dio
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF DefinedPlainTerm where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF dpt = case dpt of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias DPT_Defined_Constant df -> printTHF df
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias DPT_Defined_Function df a -> printTHF df <> parens (printArguments a)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF DefinedFunctor where
4cea468e955597a7069faba3f43f27e913f2b651Alexis Tsogias printTHF df = text $ "$" ++ map toLower (show df)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF SystemTerm where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF st = case st of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias ST_System_Constant sf -> printSystemFunctor sf
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias ST_System_Term sf a -> printSystemFunctor sf
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias <> parens (printArguments a)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintSystemFunctor :: SystemFunctor -> Doc
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintSystemFunctor = printAtomicSystemWord
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintVariable :: Variable -> Doc
4cea468e955597a7069faba3f43f27e913f2b651Alexis TsogiasprintVariable = text
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintArguments :: Arguments -> Doc
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintArguments = sepByCommas . map printTHF
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF PrincipalSymbol where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF ps = case ps of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias PS_Functor f -> printTPTPFunctor f
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias PS_Variable v -> printVariable v
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF Source where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF s = case s of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias S_Dag_Source ds -> printTHF ds
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias S_Internal_Source it oi -> text "introduced" <> parens (
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF it <> printOptionalInfo oi)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias S_External_Source es -> printTHF es
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias S_Sources ss -> sepByCommas (map printTHF ss)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias S_Unknown -> text "unknown"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF DagSource where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF ds = case ds of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias DS_Name n -> printTHF n
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias DS_Inference_Record aw ui pl -> text "inference"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias <> parens (printTHF aw <> comma <+> printUsefulInfo ui
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias <> comma <+> brackets (sepByCommas (map printTHF pl)))
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF ParentInfo where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF (PI_Parent_Info s mgl) =
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias let gl = maybe empty (\c -> text ":" <> printGeneralList c) mgl
4cea468e955597a7069faba3f43f27e913f2b651Alexis Tsogias in printTHF s <> gl
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF IntroType where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF it = text (drop 3 (show it))
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF ExternalSource where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF es = case es of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias ES_File_Source fs -> printTHF fs
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias ES_Theory tn oi -> text "theory" <> parens (
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF tn <> printOptionalInfo oi)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias ES_Creator_Source aw oi -> text "creator" <> parens (
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF aw <> printOptionalInfo oi)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF FileSource where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF (FS_File fn mn) =
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias let n = maybe empty (\c -> comma <+> printTHF c) mn
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias in text "file" <> parens (printFileName fn <> n)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF TheoryName where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF tn = text $ map toLower (show tn)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintOptionalInfo :: OptionalInfo -> Doc
4cea468e955597a7069faba3f43f27e913f2b651Alexis TsogiasprintOptionalInfo = maybe empty (\ui -> comma <+> printUsefulInfo ui)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintUsefulInfo :: UsefulInfo -> Doc
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintUsefulInfo = brackets . sepByCommas . map printTHF
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF InfoItem where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF ii = case ii of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias II_Formula_Item fi -> printTHF fi
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias II_Inference_Item infi -> printTHF infi
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias II_General_Function gf -> printTHF gf
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF FormulaItem where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF fi = case fi of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias FI_Description_Item aw -> text "description" <> parens (printTHF aw)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias FI_Iquote_Item aw -> text "iquote" <> parens (printTHF aw)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF InferenceItem where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF ii = case ii of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias II_Inference_Status is -> printTHF is
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias II_Assumptions_Record nl -> text "assumptions"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias <> parens (brackets (printNameList nl))
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias II_New_Symbol_Record aw psl -> text "new_symbols" <> parens (printTHF aw
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias <> comma <+> brackets (sepByCommas (map printTHF psl)))
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias II_Refutation fs -> text "refutation" <> parens (printTHF fs)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF InferenceStatus where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF is = case is of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias IS_Status s -> text "status" <> parens (printTHF s)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias IS_Inference_Info aw1 aw2 gl -> printTHF aw1 <> parens (printTHF aw2
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias <> comma <+> printGeneralList gl)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF StatusValue where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF sv = text $ map toLower (show sv)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintNameList :: NameList -> Doc
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintNameList = sepByCommas . map printTHF
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF GeneralTerm where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF gt = case gt of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias GT_General_Data gd -> printTHF gd
1e622ddf5a057555db1924ddc88475c695c6f7f2Alexis Tsogias GT_General_Data_Term gd gt1 -> printTHF gd <+> text ":" <+> printTHF gt1
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias GT_General_List gl -> printGeneralList gl
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF GeneralData where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF gd = case gd of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias GD_Atomic_Word aw -> printTHF aw
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias GD_General_Function gf -> printTHF gf
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias GD_Variable v -> printVariable v
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias GD_Number n -> printTHF n
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias GD_Distinct_Object dio -> printDistinctObject dio
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias GD_Formula_Data fd -> printTHF fd
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias GD_Bind v fd -> text "bind" <> parens (
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printVariable v <> comma <+> printTHF fd)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF GeneralFunction where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF (GF_General_Function aw gts) =
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF aw <> parens (printGeneralTerms gts)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF FormulaData where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF (THF_Formula thff) = text "$thf" <> parens (printTHF thff)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintGeneralList :: GeneralList -> Doc
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintGeneralList = brackets . printGeneralTerms
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintGeneralTerms :: GeneralTerms -> Doc
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintGeneralTerms = sepByCommas . map printTHF
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF Name where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF n = case n of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias N_Atomic_Word a -> printTHF a
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias N_Integer s -> text s
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF AtomicWord where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF a = case a of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias A_Single_Quoted s -> printSingleQuoted s
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias A_Lower_Word l -> text l
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintAtomicSystemWord :: AtomicSystemWord -> Doc
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintAtomicSystemWord asw = text ("$$" ++ asw)
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogiasinstance PrintTHF Number where
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias printTHF n = case n of
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias Num_Integer i -> text i
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias Num_Rational ra -> text ra
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias Num_Real re -> text re
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintFileName :: FileName -> Doc
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintFileName = printSingleQuoted
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintSingleQuoted :: SingleQuoted -> Doc
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintSingleQuoted s = text "\'" <> text s <> text "\'"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintDistinctObject :: DistinctObject -> Doc
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasprintDistinctObject s = text "\"" <> text s <> text "\""
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasorSign :: Doc
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasorSign = text "|"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasandSign :: Doc
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasandSign = text "&"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasapplySign :: Doc
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasapplySign = text "@"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasarrowSign :: Doc
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasarrowSign = text ">"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasstarSign :: Doc
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasstarSign = text "*"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasplusSign :: Doc
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiasplusSign = text "+"
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis Tsogias
12f6880fc0909e8dc2bdebc5f299a6a8bfa8afa7Alexis TsogiassepBy :: [Doc] -> Doc -> Doc
1e622ddf5a057555db1924ddc88475c695c6f7f2Alexis TsogiassepBy ls s = case ls of
1e622ddf5a057555db1924ddc88475c695c6f7f2Alexis Tsogias (c : []) -> c
1e622ddf5a057555db1924ddc88475c695c6f7f2Alexis Tsogias (c : d) -> c <+> s <+> sepBy d s
1e622ddf5a057555db1924ddc88475c695c6f7f2Alexis Tsogias [] -> empty