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



  Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
  What is a Logic?.
  In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-133. Birkhaeuser.


module QBF.Logic_QBF where

import Logic.Logic

import Propositional.Sign

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
         parse_basic_spec QBF = Just basicSpec
         parse_symb_items QBF = Just symbItems
         parse_symb_map_items QBF = Just 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
      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
          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