content: {-# LANGUAGE MultiParamTypeClasses #-}
  {- |
  Module      :  ./QBF/Logic_QBF.hs
  Description :  Instance of class Logic for propositional logic
                 extended with QBFs
  
  Copyright   :  (c) Jonathan von Schroeder, DFKI GmbH 2010
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  jonathan.von_schroeder@dfki.de
  Stability   :  experimental
  Portability :  non-portable (imports Logic.Logic)
  
  Instance of class Logic for the propositional logic extended with QBFs
     Also the instances for Syntax and Category.
  
    Ref.
  
    <http://en.wikipedia.org/wiki/Propositional_logic>
  
    Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
    What is a Logic?.
    In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-133. Birkhaeuser.
    2005.
  
    <http://www.voronkov.com/lics.cgi>
  -}
  
  module QBF.Logic_QBF where
  
  import Logic.Logic
  
  import Propositional.Sign
  
  import QBF.AS_BASIC_QBF
  import QBF.ATC_QBF ()
  import QBF.Analysis
  import QBF.Morphism
  import QBF.Parse_AS_Basic
  import QBF.ProveDepQBF
  import QBF.Sublogic as Sublogic
  import QBF.Symbol as Symbol
  import QBF.Tools
  
  import ATC.ProofTree ()
  
  import Common.ProofTree
  
  import qualified Data.Map as Map
  import Data.Monoid ()
  
  -- | Lid for propositional logic
  data QBF = QBF deriving Show
  
  instance Language QBF where
      description _ = "Propositional Logic extended with quantified boolean formulas\n"
          ++ "for more information please refer to\n"
          ++ "http://en.wikipedia.org/wiki/Propositional_logic"
          ++ "http://www.voronkov.com/lics.cgi"
  
  -- | Instance of Category for propositional logic
  instance Category Sign Morphism where
      -- Identity morhpism
      ide = idMor
      -- Returns the domain of a morphism
      dom = source
      -- Returns the codomain of a morphism
      cod = target
      -- check if morphism is inclusion
      isInclusion = Map.null . propMap
      -- tests if the morphism is ok
      legal_mor = isLegalMorphism
      -- composition of morphisms
      composeMorphisms = composeMor
  
  -- | Instance of Sentences for propositional logic
  instance Sentences QBF FORMULA
      Sign Morphism Symbol where
      negation QBF = Just . negateFormula
      -- returns the set of symbols
      sym_of QBF = singletonList . symOf
      -- kind of symbols is always prop
      symKind QBF _ = "prop"
      -- returns the symbol map
      symmap_of QBF = getSymbolMap
      -- returns the name of a symbol
      sym_name QBF = getSymbolName
      -- translation of sentences along signature morphism
      map_sen QBF = mapSentence
      -- there is nothing to leave out
      simplify_sen QBF _ = simplify
  
  instance Semigroup BASICSPEC where
      (BasicSpec l1) <> (BasicSpec l2) = BasicSpec $ l1 ++ l2
  instance Monoid BASICSPEC where
      mempty = BasicSpec []
  
  -- | Syntax of Propositional logic
  instance Syntax QBF BASICSPEC Symbol
      SYMBITEMS SYMBMAPITEMS where
           parse_basic_spec QBF = Just basicSpec
           parse_symb_items QBF = Just . const $ symbItems
           parse_symb_map_items QBF = Just . const $ symbMapItems
  
  -- | Instance of Logic for propositional logc
  instance Logic QBF
      QBFSL                     -- Sublogics
      BASICSPEC                 -- basic_spec
      FORMULA                   -- sentence
      SYMBITEMS                 -- symb_items
      SYMBMAPITEMS              -- symb_map_items
      Sign                      -- sign
      Morphism                  -- morphism
      Symbol                    -- symbol
      Symbol                    -- raw_symbol
      ProofTree                 -- proof_tree
      where
        stability QBF = Stable
        top_sublogic QBF = Sublogic.top
        all_sublogics QBF = sublogicsAll
        empty_proof_tree QBF = emptyProofTree
      -- supplied provers
        provers QBF = [depQBFProver]
  
  -- | Static Analysis for propositional logic
  instance StaticAnalysis QBF
      BASICSPEC                 -- basic_spec
      FORMULA                   -- sentence
      SYMBITEMS                 -- symb_items
      SYMBMAPITEMS              -- symb_map_items
      Sign                      -- sign
      Morphism                  -- morphism
      Symbol                    -- symbol
      Symbol                    -- raw_symbol
          where
            basic_analysis QBF =
                Just basicPropositionalAnalysis
            empty_signature QBF = emptySig
            is_subsig QBF = isSubSigOf
            subsig_inclusion QBF s = return . inclusionMap s
            signature_union QBF = sigUnion
            symbol_to_raw QBF = symbolToRaw
            id_to_raw QBF = idToRaw
            matches QBF = Symbol.matches
            stat_symb_items QBF _ = mkStatSymbItems
            stat_symb_map_items QBF _ _ = mkStatSymbMapItem
            morphism_union QBF = morphismUnion
            induced_from_morphism QBF = inducedFromMorphism
            induced_from_to_morphism QBF = inducedFromToMorphism
            signature_colimit QBF = signatureColimit
  
  -- | Sublogics
  instance SemiLatticeWithTop QBFSL where
      lub = sublogicsMax
      top = Sublogic.top
  
  instance MinSublogic QBFSL BASICSPEC where
       minSublogic = slBasicSpec bottom
  
  instance MinSublogic QBFSL Sign where
      minSublogic = slSig bottom
  
  instance SublogicName QBFSL where
      sublogicName = sublogicsName
  
  instance MinSublogic QBFSL FORMULA where
      minSublogic = slForm bottom
  
  instance MinSublogic QBFSL Symbol where
      minSublogic = slSym bottom
  
  instance MinSublogic QBFSL SYMBITEMS where
      minSublogic = slSymit bottom
  
  instance MinSublogic QBFSL Morphism where
      minSublogic = slMor bottom
  
  instance MinSublogic QBFSL SYMBMAPITEMS where
      minSublogic = slSymmap bottom
  
  instance ProjectSublogicM QBFSL Symbol where
      projectSublogicM = prSymbolM
  
  instance ProjectSublogic QBFSL Sign where
      projectSublogic = prSig
  
  instance ProjectSublogic QBFSL Morphism where
      projectSublogic = prMor
  
  instance ProjectSublogicM QBFSL SYMBMAPITEMS where
      projectSublogicM = prSymMapM
  
  instance ProjectSublogicM QBFSL SYMBITEMS where
      projectSublogicM = prSymM
  
  instance ProjectSublogic QBFSL BASICSPEC where
      projectSublogic = prBasicSpec
  
  instance ProjectSublogicM QBFSL FORMULA where
      projectSublogicM = prFormulaM
  