{- |
Module      :  $Header$
Description :  Provers for propositional logic
Copyright   :  (c) Till Mossakowski, Uni Bremen 2008
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  till@informatik.uni-bremen.de
Stability   :  experimental
Portability :  portable

A truth table prover for propositional logic.
Inefficient, but useful for learning purposes.
-}

module Propositional.ProveWithTruthTable
  ( ttProver
  , ttConsistencyChecker
  , ttConservativityChecker
  , allModels
  ) where

import Common.Lib.Tabular

import Propositional.AS_BASIC_Propositional
import Propositional.Sign
import qualified Propositional.Morphism as PMorphism
import qualified Propositional.ProverState as PState
import qualified Propositional.Sign as Sig
import Propositional.Sublogic (PropSL, top)

import qualified Logic.Prover as LP

import qualified Interfaces.GenericATPState as ATPState
import GUI.GenericATP
import GUI.Utils (infoDialog, createTextSaveDisplay)

import Common.ProofTree
import qualified Common.AS_Annotation as AS_Anno
import qualified Common.Id as Id

import qualified Data.Set as Set
import qualified Common.OrderedMap as OMap

import Common.Consistency
import qualified Common.Result as Result

import Data.Time (midnight)

-- * Prover implementation

-- | the name of the prover
ttS :: String
ttS = "truth tables"

-- maximal size of the signature
maxSigSize :: Int
maxSigSize = 17

-- display error message when signature is too large
sigTooLarge :: Int -> String
sigTooLarge sigSize = unlines
  [ "Signature is too large."
  , "It should contain < " ++ show maxSigSize ++ " symbols,"
  , "but it contains " ++ show sigSize ++ " symbols." ]

ttHelpText :: String
ttHelpText = "An implementation of the truth table method.\n"
             ++ "Very inefficient, but useful for learning and teaching\n"
             ++ "Works well for signatures with less than " ++ show maxSigSize
             ++ " symbols."

{- |
  Models and evaluation of sentences
-}

type Model = Set.Set Id.Id -- a model specifies which propositions are true

-- | show Bools in truth table
showBool :: Bool -> String
showBool True = "T"
showBool False = "F"

-- | evaluation of sentences in a model
eval :: Model -> FORMULA -> Bool
eval m (Negation phi _) = not $ eval m phi
eval m (Conjunction phis _) = all (eval m) phis
eval m (Disjunction phis _) = any (eval m) phis
eval m (Implication phi1 phi2 _) = not (eval m phi1) || eval m phi2
eval m (Equivalence phi1 phi2 _) = eval m phi1 == eval m phi2
eval _ (True_atom _) = True
eval _ (False_atom _) = False
eval m (Predication ident) = Id.simpleIdToId ident `Set.member` m

evalNamed :: Model -> AS_Anno.Named FORMULA -> Bool
evalNamed m = eval m . AS_Anno.sentence

{- |
  Evaluation of (co)freeness constraints
-}

-- | amalgamation of models
amalg :: Model -> Model -> Model
amalg = Set.union

data FormulaOrFree =
     Formula FORMULA
   | FreeConstraint (LP.FreeDefMorphism FORMULA PMorphism.Morphism)

evalNamedFormulaOrFree :: Model -> AS_Anno.Named FormulaOrFree -> Bool
evalNamedFormulaOrFree m = evalFormulaOrFree m . AS_Anno.sentence

evalFormulaOrFree :: Model -> FormulaOrFree -> Bool
evalFormulaOrFree m (Formula phi) = eval m phi
evalFormulaOrFree m (FreeConstraint freedef) = evalFree m freedef

reduceModel :: Sig.Sign -> Model -> Model
reduceModel sig m = Set.intersection m (items sig)

leq :: Model -> Model -> Bool
leq = Set.isSubsetOf

isMin :: Bool -> Model -> [Model] -> Bool
isMin isCo m = all (\m' -> if isCo then leq m' m else leq m m')

evalFree :: Model
         -> LP.FreeDefMorphism FORMULA PMorphism.Morphism
         -> Bool
evalFree m freedef =
  let diffsig = Sign (items freetar `Set.difference` items freesrc)
      mred = reduceModel freesrc m
      modelsOverMred = map (mred `amalg`) (allModels diffsig)
      modelClass = foldr (filter . flip eval) modelsOverMred freeth
  in all (eval m) freeth        -- the model satisfies the axioms ...
     && isMin isCo m modelClass -- ... and is the minimal one that does so
  where freemor = LP.freeDefMorphism freedef
        freesrc = PMorphism.source freemor
        freetar = PMorphism.target freemor
        freeth = map AS_Anno.sentence $ LP.freeTheory freedef
        isCo = LP.isCofree freedef

-- | generate all models for a signature
allModels :: Sign -> [Model]
allModels sig = allModels1 $ Set.toList $ items sig
  where allModels1 [] = [Set.empty]
        allModels1 (p:rest) =
          let models = allModels1 rest
           in models ++ map (Set.insert p) models

data TTExtRow =
     TTExtRow { rextprops, rextaxioms :: [Bool]
              , rextIsModel :: Bool
              }

data TTRow =
     TTRow { rprops, raxioms :: [Bool]
           , rgoal :: Maybe Bool
           , rextrows :: [TTExtRow]
           , rIsModel :: Bool
           , rIsOK :: Bool
           }

data TTHead =
     TTHead { hprops, haxioms, hextprops, hextaxioms :: [String]
            , hgoal :: Maybe String
            }

data TruthTable =
     TruthTable { thead :: TTHead
                , trows :: [TTRow]
                }

renderTT :: TruthTable -> Table String String String
renderTT tt = Table rowHeaders header table
  where
  hextpropsTT = hextprops (thead tt)
  hextaxiomsTT = hextaxioms (thead tt)
  rowsTT = trows tt
  header = Group DoubleLine
           ( [ Group SingleLine (map Header (hprops (thead tt)))
             , Group SingleLine (map Header (haxioms (thead tt)))]
             ++ (if null hextpropsTT && null hextaxiomsTT then []
                 else [ Header ""
                      , Group SingleLine (map Header hextpropsTT)
                      , Group SingleLine (map Header hextaxiomsTT)])
             ++ case hgoal (thead tt) of
                 Nothing -> []
                 Just g -> [Group DoubleLine [Header g]])
  rowtype r = (if rIsModel r then "M" else " ")
              ++(if rIsOK r then (if rIsModel r then "+" else "o")
                            else "-")
  rowHeader r = Group NoLine
    $ Header (rowtype r) : map (const (Header "")) [2..length (rextrows r)]
  rowHeaders = if all (null . rextrows) rowsTT
    then Group NoLine (map (Header . rowtype) rowsTT)
    else Group SingleLine (map rowHeader rowsTT)
  makeExtRow e = (if rextIsModel e then "M" else "") :
    map showBool (rextprops e) ++ map showBool (rextaxioms e)
  makeRow r =
    let common = map showBool (rprops r) ++ map showBool (raxioms r) ++
                 case (rgoal r) of
                   Nothing -> []
                   Just g -> [showBool g]
        emptyPrefix = map (const "") [1..length common]
    in case map makeExtRow (rextrows r) of
       [] -> [common]
       e : extrows -> (common ++ e) : map (emptyPrefix ++) extrows
  table = concatMap makeRow rowsTT

{- |
  The Prover implementation.

  Implemented are: a prover GUI.
-}
ttProver :: LP.Prover Sig.Sign FORMULA PMorphism.Morphism PropSL ProofTree
ttProver = LP.mkProverTemplate ttS top ttProveGUI

{- |
   The Consistency Cheker.
-}
ttConsistencyChecker :: LP.ConsChecker Sig.Sign FORMULA PropSL
                                  PMorphism.Morphism ProofTree
ttConsistencyChecker = LP.mkConsChecker ttS top consCheck

consCheck :: String -> LP.TacticScript
          -> LP.TheoryMorphism Sig.Sign FORMULA PMorphism.Morphism ProofTree
          -> [LP.FreeDefMorphism FORMULA PMorphism.Morphism]
          -- ^ free definitions
          -> IO (LP.CCStatus ProofTree)
consCheck _ _ tm _freedefs = case LP.tTarget tm of
  LP.Theory sig nSens ->
    let sigSize = Set.size (items sig) in
    if sigSize >= maxSigSize then
      return $ LP.CCStatus (ProofTree $ sigTooLarge sigSize) midnight Nothing
    else do
      let axs = filter (AS_Anno.isAxiom . snd) $ OMap.toList nSens
          models = allModels sig
          sigList = Set.toList $ items sig
          heading = TTHead { hprops = map show sigList
                           , haxioms = map fst axs
                           , hextprops = [], hextaxioms = []
                           , hgoal = Nothing
                           }
          mkRow m =
            let evalAx = map (eval m . AS_Anno.sentence . snd) axs
                isModel = and evalAx
            in TTRow { rprops = map (`Set.member` m) sigList
                     , raxioms = evalAx
                     , rextrows = []
                     , rgoal = Nothing
                     , rIsModel = isModel
                     , rIsOK = isModel
                     }
          rows = map mkRow models
          isOK = any rIsOK rows
          table = TruthTable { thead = heading
                             , trows = rows
                             }
          legend = "Legend:\nM+ = model of the axioms\n"
                   ++ " - = not a model of the axioms\n"
          body = legend ++ "\n" ++ render id id id (renderTT table)
      return $ LP.CCStatus (ProofTree body) midnight $ Just isOK

-- ** prover GUI

{- |
  Invokes the generic prover GUI.
-}
ttProveGUI :: String -- ^ theory name
          -> LP.Theory Sig.Sign FORMULA ProofTree
          -> [LP.FreeDefMorphism FORMULA PMorphism.Morphism]
          -- ^ free definitions
          -> IO([LP.ProofStatus ProofTree]) -- ^ proof status for each goal
ttProveGUI thName th freedefs =
  genericATPgui (atpFun thName) True (LP.proverName ttProver) thName th
                freedefs emptyProofTree

{- |
  Record for prover specific functions. This is used by both GUI and command
  line interface.
-}
atpFun :: String -- ^ Theory name
  -> ATPState.ATPFunctions Sig.Sign FORMULA PMorphism.Morphism ProofTree
     PState.PropProverState
atpFun thName = ATPState.ATPFunctions
                { ATPState.initialProverState = PState.propProverState
                , ATPState.goalOutput         = goalProblem thName
                , ATPState.atpTransSenName    = PState.transSenName
                , ATPState.atpInsertSentence  = PState.insertSentence
                , ATPState.proverHelpText     = ttHelpText
                , ATPState.runProver          = runTt
                , ATPState.batchTimeEnv       = ""
                , ATPState.fileExtensions     = ATPState.FileExtensions
                    { ATPState.problemOutput = ".tt"
                    , ATPState.proverOutput = ".tt"
                    , ATPState.theoryConfiguration = ".tt"}
                , ATPState.createProverOptions = createTtOptions
                }

defaultProofStatus :: AS_Anno.Named FORMULA -> LP.ProofStatus ProofTree
defaultProofStatus nGoal =
  LP.openProofStatus (AS_Anno.senAttr nGoal) (LP.proverName ttProver)
                     emptyProofTree

{- |
  Runs tt.
-}

runTt :: PState.PropProverState
      -- ^ logical part containing the input Sign and
      -- axioms and possibly goals that have been proved
      -- earlier as additional axioms
      -> ATPState.GenericConfig ProofTree
      -- ^ configuration to use
      -> Bool
      -- ^ True means save DIMACS file
      -> String
      -- ^ Name of the theory
      -> AS_Anno.Named FORMULA
      -- ^ Goal to prove
      -> IO (ATPState.ATPRetval, ATPState.GenericConfig ProofTree)
      -- ^ (retval, configuration with proof status and complete output)
runTt pState cfg _ _thName nGoal =
  let sig = PState.initialSignature pState
      sigSize = Set.size $ items sig
   in if sigSize >= maxSigSize then do
        infoDialog "Signature too large" $ sigTooLarge sigSize
        return (ATPState.ATPTLimitExceeded,
                cfg { ATPState.proofStatus = defaultProofStatus nGoal })
      else do
       let axs = PState.initialAxioms pState
           freedefs = PState.freeDefs pState
           nameFree fd =
              AS_Anno.makeNamed (if LP.isCofree fd then "cofree" else "free")
                                (FreeConstraint fd)
           sens = map (AS_Anno.mapNamed Formula) axs ++ map nameFree freedefs
           models = allModels sig
           sigList = Set.toList $ items sig
           heading =
             TTHead { hprops = map show sigList
                    , haxioms = map AS_Anno.senAttr sens
                    , hextprops = [], hextaxioms = []
                    , hgoal = Just $ AS_Anno.senAttr nGoal
                    }
           mkRow m =
             let evalAx = map (evalNamedFormulaOrFree m) sens
                 evalGoal = evalNamed m nGoal
                 isModel = and evalAx
             in TTRow { rprops = map (`Set.member` m) sigList
                      , raxioms = evalAx
                      , rextrows = []
                      , rgoal = Just evalGoal
                      , rIsModel = isModel
                      , rIsOK = not isModel || evalGoal
                      }
           rows = map mkRow models
           isOK = all rIsOK rows
           consistent = any rIsModel rows
           table = TruthTable { thead = heading
                              , trows = rows
                              }
           legend = "Legend:\nM = model of the premises\n"++
             "+ = OK, model fulfills conclusion\n"++
             "- = not OK, counterexample for logical consequence\n"++
             "o = OK, premises are not fulfilled, hence conclusion is "
             ++ "irrelevant\n"
           body = legend++"\n"++render id id id (renderTT table)
       let status = (defaultProofStatus nGoal)
                     { LP.goalStatus = if isOK then LP.Proved consistent
                                               else LP.Disproved
                     ,LP.usedAxioms = map AS_Anno.senAttr sens
                     }
       return (ATPState.ATPSuccess,
               cfg { ATPState.proofStatus = status
                   , ATPState.resultOutput = [body] })

{- |
  Creates a list of all options the truth table prover runs with.
  Only Option is the timelimit
-}
createTtOptions :: ATPState.GenericConfig ProofTree -> [String]
createTtOptions _cfg = [] -- [(show $ configTimeLimit cfg)]

goalProblem :: String -- ^ name of the theory
            -> PState.PropProverState -- ^ initial Prover state
            -> AS_Anno.Named FORMULA -- ^ goal to prove
            -> [String] -- ^ Options (ignored)
            -> IO String
goalProblem _ _ _ _ = return ""

{- |
  Conservativity check
-}

-- | Conservativity Check via truth table

-- TODO: check for injectivity!

ttConservativityChecker ::
              (Sign, [AS_Anno.Named FORMULA]) -- ^ Initial sign and formulas
           -> PMorphism.Morphism              -- ^ morhpism between specs
           -> [AS_Anno.Named FORMULA]         -- ^ Formulas of extended spec
           -> IO (Result.Result (Maybe (Conservativity, [FORMULA])))
ttConservativityChecker (_, srcSens) mor tarSens =
  let srcAxs        = filter AS_Anno.isAxiom srcSens
      tarAxs        = filter AS_Anno.isAxiom tarSens
      srcSig        = items $ PMorphism.source mor
      imageSig      = Set.map (PMorphism.applyMorphism mor) srcSig
      imageSigList  = Set.toList imageSig
      tarSig        = items $ PMorphism.target mor
      newSig        = Set.difference tarSig imageSig
      sigSize       = Set.size tarSig
  in if sigSize >= maxSigSize then return $ return Nothing
    else do
      let imageAxs = map (AS_Anno.mapNamed (PMorphism.mapSentenceH mor)) srcAxs
          models = allModels (Sign imageSig)
          newSigList = Set.toList newSig
          heading =
            TTHead { hprops = map show imageSigList,
                     haxioms = map AS_Anno.senAttr srcAxs,
                     hextprops =  map show newSigList,
                     hextaxioms = map AS_Anno.senAttr tarAxs,
                     hgoal = Nothing
                   }
          mkRow m =
            let evalAx = map (evalNamed m) imageAxs
                isModel = and evalAx
                extmodels = allModels (Sign newSig)
                extrow m' =
                  let evalExtAx = map (evalNamed (m `amalg` m')) tarAxs
                      isExtModel = and evalExtAx
                   in TTExtRow { rextprops = map (`Set.member` m') newSigList,
                                rextaxioms = evalExtAx,
                                rextIsModel = isExtModel
                              }
                extrows = map extrow extmodels
            in TTRow { rprops = map (`Set.member` m) imageSigList,
                       raxioms = evalAx,
                       rgoal = Nothing,
                       rextrows = if isModel then extrows else [],
                       rIsModel = isModel,
                       rIsOK = not isModel || any rextIsModel extrows
                     }
          rows = map mkRow models
          isOK = all rIsOK rows
          table = TruthTable { thead = heading,
                               trows = rows
                             }
          title = "The extension is "++ (if isOK then "" else "not ")
                  ++ "conservative"
          legend = "Legend:\n"
            ++ "M = model of the axioms\n"
            ++ "+ = OK, has expansion\n"
            ++ "- = not OK, has no expansion, hence conservativity fails\n"
            ++ "o = OK, not a model of the axioms, hence no expansion needed\n"
          body = legend++"\n"++render id id id (renderTT table)
          res = if isOK then Cons else Inconsistent
      createTextSaveDisplay title "unnamed" body
      return $ return $ Just (res, [])
