{- |
Module      :  $Header$
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

{- |
  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
