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

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"
++ "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 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
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
```