content: {- |
  Module      :  ./SoftFOL/PrintTPTP.hs
  Description :  Pretty printing for SPASS signatures in TPTP syntax.
  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
  
  Pretty printing for SoftFOL signatures in TPTP syntax.
     Refer to <http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html>
     for the TPTP syntax documentation.
  
  -}
  
  module SoftFOL.PrintTPTP where
  
  import Common.AS_Annotation
  import Common.Doc
  import Common.DocUtils
  
  import SoftFOL.Sign
  import SoftFOL.Conversions
  
  import Data.Maybe
  
  {- | This type class allows pretty printing in TPTP syntax of instantiated data
  types -}
  class PrintTPTP a where
      printTPTP :: a -> Doc
  
  instance Pretty TPTP where
      pretty (FormAnno _ _ _ t _) = printTPTP t
      pretty _ = empty
  
  {- |
    Helper function. Generates a separating comment line.
  -}
  separator :: String
  separator = '%' : replicate 75 '-'
  
  instance PrintTPTP Sign where
      printTPTP = printTPTP . signToSPLogicalPart
  
  {- |
    Creates a Doc from a SoftFOL Problem.
  -}
  instance PrintTPTP SPProblem where
      printTPTP p = text separator
        $+$ text "% Problem" <+> colon <+> text (identifier p)
        $+$ printTPTP (description p)
        $+$ vcat (map printTPTP $ settings p)
        $+$ text separator
        $+$ printTPTP (logicalPart p)
  
  {- |
    Creates a Doc from a SoftFOL Logical Part.
  -}
  instance PrintTPTP SPLogicalPart where
      printTPTP lp =
        let decls = declarationList lp
            validDeclarations = filter (\ decl -> case decl of
                SPSubsortDecl {} -> True
                SPTermDecl {} -> True
                SPSimpleTermDecl _ -> True
                _ -> False)
                       $ fromMaybe [] decls
            fs = formulaLists lp
        in if null validDeclarations && null fs then
              text "fof" <> parens
                (text "empty" <> comma <> printTPTP SPOriginAxioms
                 <> comma <> printTPTP SPTrue) <> dot
           else vcat (map (\ (decl, i) ->
                      text "fof" <>
                      parens (text ("declaration" ++ show i) <> comma <>
                      printTPTP SPOriginAxioms <> comma
                      $+$ printTPTP decl) <> dot)
                  $ zip validDeclarations [(0 :: Int) ..])
           $+$ vcat (map printTPTP fs)
  
  {- |
   Creates a Doc from a SoftFOL Declaration.
   A subsort declaration will be rewritten as a special SPQuantTerm.
  -}
  instance PrintTPTP SPDeclaration where
      printTPTP decl = case decl of
        SPSubsortDecl {sortSymA = sortA, sortSymB = sortB}
          -> let subsortVar = spTerms $ genVarList sortA [sortB]
             in printTPTP SPQuantTerm
               { quantSym = SPForall,
                 variableList = subsortVar,
                 qFormula = compTerm SPImplies
                   [ compTerm (spSym sortA) subsortVar
                   , compTerm (spSym sortB) subsortVar] }
        SPTermDecl {termDeclTermList = tlist, termDeclTerm = tt}
          -> printTPTP SPQuantTerm {
                         quantSym = SPForall,
                         variableList = tlist,
                         qFormula = tt}
        SPSimpleTermDecl stsym -> printTPTP stsym
        pd@(SPPredDecl {}) -> maybe empty printTPTP $ predDecl2Term pd
        _ -> empty
  
  {- |
    Creates a Doc from a SoftFOL Formula List.
  -}
  instance PrintTPTP SPFormulaList where
      printTPTP l = vcat $ map (printFormula $ originType l) $ formulae l
  
  {- |
    Creates a Doc from a SoftFOL Origin Type.
  -}
  instance PrintTPTP SPOriginType where
      printTPTP t = text $ case t of
          SPOriginAxioms -> "axiom"
          SPOriginConjectures -> "conjecture"
  
  {- |
    Creates a Doc from a SoftFOL Formula. Needed since SPFormula is just a
    'type SPFormula = Named SPTerm' and thus instanciating PrintTPTP is not
    possible.
  -}
  printFormula :: SPOriginType -> SPFormula -> Doc
  -- printFormula ot f = printFormulaText ot (senAttr f) (sentence f)
  printFormula ot f =
      text "fof" <> parens (text (senAttr f) <> comma <> printTPTP ot <> comma
                            $+$ printTPTP (sentence f)) <> dot
  
  {- |
    Creates a Doc from a SoftFOL Term.
  -}
  instance PrintTPTP SPTerm where
      printTPTP t = case t of
        SPQuantTerm {quantSym = qsym, variableList = tlist, qFormula = tt} -> let
          isComplexTerm tm = case tm of
              SPComplexTerm _ [] -> False
              _ -> True
          getVars tm = case tm of
              SPComplexTerm _ args ->
                if null args then [tm] else concatMap getVars args
              _ -> []
          cl = filter isComplexTerm tlist
          conj = case qsym of
                   SPExists -> compTerm SPAnd $ cl ++ [tt]
                   _ -> compTerm SPImplies $ (case cl of
                     [hd] -> hd
                     _ -> compTerm SPAnd cl) : [tt]
          in printTPTP qsym
             <+> brackets (printCommaSeparated $ concatMap getVars tlist)
             <+> colon
             -- either all variables are simple terms
             <+> if null cl then parPrintTPTP tt
                 -- or there are none simple terms
                 else
            {- construct premiss for implication out of variableList (Forall)
            construct conjunction out of variableList (Exists) -}
                 parens $ printTPTP conj
        SPComplexTerm {symbol = ctsym, arguments = args}
          -> printTermList ctsym args
  
  {- |
    Creates a Doc from a list of SoftFOL Terms connected by a SoftFOL Symbol.
  -}
  printTermList :: SPSymbol -> [SPTerm] -> Doc
  printTermList symb terms = let
    sbd = printTPTP symb
    d = if null terms then sbd else sbd <> parens (printCommaSeparated terms)
    in case symb of
    SPNot -> case terms of
          [t] -> sbd <+> parPrintTPTP t
          _ -> d
    _ -> if elem symb $ SPEqual : binLogOps then
       fsep $ prepPunctuate (sbd <> space) $ map parPrintTPTP terms
       else d
  
  {- |
    Helper function. Generates a comma separated list of SoftFOL Terms as a Doc.
  -}
  printCommaSeparated :: [SPTerm] -> Doc
  printCommaSeparated = sepByCommas . map printTPTP
  
  parPrintTPTP :: SPTerm -> Doc
  parPrintTPTP t = (if isUnitary t then id else parens) $ printTPTP t
  
  isUnitary :: SPTerm -> Bool
  isUnitary t = case t of
      SPComplexTerm {symbol = ctsym, arguments = _ : _ : _} ->
         notElem ctsym binLogOps
      _ -> True
  
  binLogOps :: [SPSymbol]
  binLogOps = [SPOr, SPAnd, SPImplies, SPImplied, SPEquiv]
  
  {- |
    Creates a Doc from a SoftFOL Quantifier Symbol.
  -}
  instance PrintTPTP SPQuantSym where
      printTPTP qs = text $ case qs of
          SPForall -> "!"
          SPExists -> "?"
          SPCustomQuantSym cst -> show cst
  
  {- |
    Creates a Doc from a SoftFOL Symbol.
  -}
  instance PrintTPTP SPSymbol where
      printTPTP s = text $ case s of
          SPEqual -> "="
          SPTrue -> "$true"
          SPFalse -> "$false"
          SPOr -> "|"
          SPAnd -> "&"
          SPNot -> "~"
          SPImplies -> "=>"
          SPImplied -> "<="
          SPEquiv -> "<=>"
          SPCustomSymbol cst -> show cst
          _ -> showSPSymbol s
  
  {- |
    Creates a Doc from a SoftFOL description.
  -}
  instance PrintTPTP SPDescription where
      printTPTP d = spCommentText "Name   " (name d)
        $+$ spCommentText "Author " (author d)
        $+$ maybe empty (spCommentText "Version") (version d)
        $+$ maybe empty (spCommentText "Logic  ") (logic d)
        $+$ text "% Status " <+> colon <+> printTPTP (status d)
        $+$ spCommentText "Desc   " (desc d)
        $+$ maybe empty (spCommentText "Date   ") (date d)
  
  {- |
    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.
  -}
  spCommentText :: String -> String -> Doc
  spCommentText fieldName fieldDesc =
      hsep [text "%", text fieldName, colon, text fieldDesc]
  
  {- |
    Creates a Doc from an 'SPLogState'.
  -}
  instance PrintTPTP SPLogState where
      printTPTP s = text $ case s of
        SPStateSatisfiable -> "satisfiable"
        SPStateUnsatisfiable -> "unsatisfiable"
        SPStateUnknown -> "unknown"
  
  instance PrintTPTP SPSetting where
      printTPTP s = spCommentText "Option " "" <+> case s of
        SPGeneralSettings e -> text $ show e
        SPSettings _ settingText -> hsep $ map printTPTP settingText
  
  instance PrintTPTP SPSettingBody where
      printTPTP s = case s of
        SPFlag sw v -> hcat
          [text sw, if null v then empty else
                        parens $ hsep $ punctuate comma $ map text v]
        _ -> empty
  