content: {- |
  Module      :  ./SoftFOL/CreateDFGDoc.hs
  Description :  Generating DFG Doc out of SPASS theories.
  Copyright   :  (c) Klaus Luettich, Uni Bremen 2005
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  luecke@informatik.uni-bremen.de
  Stability   :  provisional
  Portability :  non-protable(Logic)
  
  Printing a (G_theory CASL _) into a DFG Doc.
  
  -}
  
  module SoftFOL.CreateDFGDoc (printTheoryAsSoftFOL) where
  
  import Logic.Prover
  import Logic.Grothendieck
  import Logic.Comorphism
  import Logic.Coerce
  
  import Static.GTheory
  
  import Common.AS_Annotation as AS_Anno
  import Common.Doc
  import Common.DocUtils
  import Common.ExtSign
  import Common.IRI (IRI)
  import Common.ProofUtils
  import Common.Result
  
  import CASL.Logic_CASL
  import CASL.Sublogic
  
  import Comorphisms.CASL2SubCFOL
  import Comorphisms.CASL2PCFOL
  import Comorphisms.SuleCFOL2SoftFOL
  
  import SoftFOL.Logic_SoftFOL
  import SoftFOL.Conversions
  import SoftFOL.Translate
  import SoftFOL.Sign
  
  import SoftFOL.PrintTPTP
  
  spassConsTimeLimit :: Int
  spassConsTimeLimit = 500
  
  printTheoryAsSoftFOL :: IRI
           -> Int -- ^ 0 = DFG, 1 = TPTP
           -> Bool
              {- ^ if True a conjecture false is added otherwise
                   its a theory without its own conjectures. -}
           -> G_theory -> IO (Maybe Doc)
  printTheoryAsSoftFOL sn lang checkConsistency
    gth@(G_theory lid _ (ExtSign sign _) _ thSens _) =
      maybe (return Nothing)
            (\ (sign1, sens1) ->
                 do prob <- genSoftFOLProblem
                                thName
                                (spLogicalPart sign1 sens1)
                                (if checkConsistency
                                 then Just falseConj
                                 else Nothing)
                    return $ Just $ printOut
                           prob {settings = [SPSettings
                                              {settingName = SPASS,
                                               settingBody = flags}]})
                           -- (prob {settings = flags}))
  
        (resultToMaybe (if lessSublogicComor (sublogicOfTh gth) $
            Comorphism suleCFOL2SoftFOL
         then coerceBasicTheory lid CASL "" (sign, sens)
                >>= wrapMapTheory suleCFOL2SoftFOL
         else (if lessSublogicComor (sublogicOfTh gth) $ Comorphism idCASL
          then coerceBasicTheory lid CASL "" (sign, sens)
                >>= wrapMapTheory idCASL
                >>= wrapMapTheory defaultCASL2SubCFOL
                >>= wrapMapTheory suleCFOL2SoftFOL
          else if lessSublogicComor (sublogicOfTh gth) $
                  Comorphism idCASL_nosub
               then coerceBasicTheory lid CASL "" (sign, sens)
                        >>= wrapMapTheory idCASL_nosub
                        >>= wrapMapTheory CASL2PCFOL
                        >>= wrapMapTheory defaultCASL2SubCFOL
                        >>= wrapMapTheory suleCFOL2SoftFOL
               else coerceBasicTheory lid SoftFOL "" (sign, sens))))
    where
          printOut = case lang of
                       0 -> pretty
                       1 -> printTPTP
                       _ -> pretty
          sens = toNamedList thSens
          thName = show sn
  
          spLogicalPart sig sen =
                              foldl insertSentence
                                    (signToSPLogicalPart sig)
                                    (reverse $
                                     prepareSenNames transSenName sen)
  
          flags = if checkConsistency
                  then [SPFlag "set_flag" ["TimeLimit", show spassConsTimeLimit]
                       , SPFlag "set_flag" ["DocProof", "1"]]
                  else []
  
          falseConj = (makeNamed "inconsistent" falseSen)
                      { isAxiom = False }
          falseSen = simpTerm SPFalse
  
          max_nosub_SPASS = caslTop { cons_features = emptyMapConsFeature }
          max_sub_SPASS = caslTop { sub_features = LocFilSub }
          idCASL = mkIdComorphism CASL max_sub_SPASS
          idCASL_nosub = mkIdComorphism CASL max_nosub_SPASS
  