{-# 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 Int -> QBF -> ShowS
[QBF] -> ShowS
QBF -> String
(Int -> QBF -> ShowS)
-> (QBF -> String) -> ([QBF] -> ShowS) -> Show QBF
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [QBF] -> ShowS
$cshowList :: [QBF] -> ShowS
show :: QBF -> String
$cshow :: QBF -> String
showsPrec :: Int -> QBF -> ShowS
$cshowsPrec :: Int -> QBF -> ShowS
Show

instance Language QBF where
    description :: QBF -> String
description _ = "Propositional Logic extended with quantified boolean formulas\n"
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ "for more information please refer to\n"
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ "http://en.wikipedia.org/wiki/Propositional_logic"
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ "http://www.voronkov.com/lics.cgi"

-- | Instance of Category for propositional logic
instance Category Sign Morphism where
    -- Identity morhpism
    ide :: Sign -> Morphism
ide = Sign -> Morphism
idMor
    -- Returns the domain of a morphism
    dom :: Morphism -> Sign
dom = Morphism -> Sign
source
    -- Returns the codomain of a morphism
    cod :: Morphism -> Sign
cod = Morphism -> Sign
target
    -- check if morphism is inclusion
    isInclusion :: Morphism -> Bool
isInclusion = Map Id Id -> Bool
forall k a. Map k a -> Bool
Map.null (Map Id Id -> Bool) -> (Morphism -> Map Id Id) -> Morphism -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism -> Map Id Id
propMap
    -- tests if the morphism is ok
    legal_mor :: Morphism -> Result ()
legal_mor = Morphism -> Result ()
isLegalMorphism
    -- composition of morphisms
    composeMorphisms :: Morphism -> Morphism -> Result Morphism
composeMorphisms = Morphism -> Morphism -> Result Morphism
composeMor

-- | Instance of Sentences for propositional logic
instance Sentences QBF FORMULA
    Sign Morphism Symbol where
    negation :: QBF -> FORMULA -> Maybe FORMULA
negation QBF = FORMULA -> Maybe FORMULA
forall a. a -> Maybe a
Just (FORMULA -> Maybe FORMULA)
-> (FORMULA -> FORMULA) -> FORMULA -> Maybe FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> FORMULA
negateFormula
    -- returns the set of symbols
    sym_of :: QBF -> Sign -> [Set Symbol]
sym_of QBF = Set Symbol -> [Set Symbol]
forall a. a -> [a]
singletonList (Set Symbol -> [Set Symbol])
-> (Sign -> Set Symbol) -> Sign -> [Set Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Set Symbol
symOf
    -- kind of symbols is always prop
    symKind :: QBF -> Symbol -> String
symKind QBF _ = "prop"
    -- returns the symbol map
    symmap_of :: QBF -> Morphism -> EndoMap Symbol
symmap_of QBF = Morphism -> EndoMap Symbol
getSymbolMap
    -- returns the name of a symbol
    sym_name :: QBF -> Symbol -> Id
sym_name QBF = Symbol -> Id
getSymbolName
    -- translation of sentences along signature morphism
    map_sen :: QBF -> Morphism -> FORMULA -> Result FORMULA
map_sen QBF = Morphism -> FORMULA -> Result FORMULA
mapSentence
    -- there is nothing to leave out
    simplify_sen :: QBF -> Sign -> FORMULA -> FORMULA
simplify_sen QBF _ = FORMULA -> FORMULA
simplify

instance Semigroup BASICSPEC where
    (BasicSpec l1 :: [Annoted BASICITEMS]
l1) <> :: BASICSPEC -> BASICSPEC -> BASICSPEC
<> (BasicSpec l2 :: [Annoted BASICITEMS]
l2) = [Annoted BASICITEMS] -> BASICSPEC
BasicSpec ([Annoted BASICITEMS] -> BASICSPEC)
-> [Annoted BASICITEMS] -> BASICSPEC
forall a b. (a -> b) -> a -> b
$ [Annoted BASICITEMS]
l1 [Annoted BASICITEMS]
-> [Annoted BASICITEMS] -> [Annoted BASICITEMS]
forall a. [a] -> [a] -> [a]
++ [Annoted BASICITEMS]
l2
instance Monoid BASICSPEC where
    mempty :: BASICSPEC
mempty = [Annoted BASICITEMS] -> BASICSPEC
BasicSpec []

-- | Syntax of Propositional logic
instance Syntax QBF BASICSPEC Symbol
    SYMBITEMS SYMBMAPITEMS where
         parse_basic_spec :: QBF -> Maybe (PrefixMap -> AParser st BASICSPEC)
parse_basic_spec QBF = (PrefixMap -> AParser st BASICSPEC)
-> Maybe (PrefixMap -> AParser st BASICSPEC)
forall a. a -> Maybe a
Just PrefixMap -> AParser st BASICSPEC
forall st. PrefixMap -> AParser st BASICSPEC
basicSpec
         parse_symb_items :: QBF -> Maybe (PrefixMap -> AParser st SYMBITEMS)
parse_symb_items QBF = (PrefixMap -> AParser st SYMBITEMS)
-> Maybe (PrefixMap -> AParser st SYMBITEMS)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st SYMBITEMS)
 -> Maybe (PrefixMap -> AParser st SYMBITEMS))
-> (AParser st SYMBITEMS -> PrefixMap -> AParser st SYMBITEMS)
-> AParser st SYMBITEMS
-> Maybe (PrefixMap -> AParser st SYMBITEMS)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SYMBITEMS -> PrefixMap -> AParser st SYMBITEMS
forall a b. a -> b -> a
const (AParser st SYMBITEMS -> Maybe (PrefixMap -> AParser st SYMBITEMS))
-> AParser st SYMBITEMS
-> Maybe (PrefixMap -> AParser st SYMBITEMS)
forall a b. (a -> b) -> a -> b
$ AParser st SYMBITEMS
forall st. GenParser Char st SYMBITEMS
symbItems
         parse_symb_map_items :: QBF -> Maybe (PrefixMap -> AParser st SYMBMAPITEMS)
parse_symb_map_items QBF = (PrefixMap -> AParser st SYMBMAPITEMS)
-> Maybe (PrefixMap -> AParser st SYMBMAPITEMS)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st SYMBMAPITEMS)
 -> Maybe (PrefixMap -> AParser st SYMBMAPITEMS))
-> (AParser st SYMBMAPITEMS
    -> PrefixMap -> AParser st SYMBMAPITEMS)
-> AParser st SYMBMAPITEMS
-> Maybe (PrefixMap -> AParser st SYMBMAPITEMS)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SYMBMAPITEMS -> PrefixMap -> AParser st SYMBMAPITEMS
forall a b. a -> b -> a
const (AParser st SYMBMAPITEMS
 -> Maybe (PrefixMap -> AParser st SYMBMAPITEMS))
-> AParser st SYMBMAPITEMS
-> Maybe (PrefixMap -> AParser st SYMBMAPITEMS)
forall a b. (a -> b) -> a -> b
$ AParser st SYMBMAPITEMS
forall st. GenParser Char st SYMBMAPITEMS
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 -> Stability
stability QBF = Stability
Stable
      top_sublogic :: QBF -> QBFSL
top_sublogic QBF = QBFSL
Sublogic.top
      all_sublogics :: QBF -> [QBFSL]
all_sublogics QBF = [QBFSL]
sublogicsAll
      empty_proof_tree :: QBF -> ProofTree
empty_proof_tree QBF = ProofTree
emptyProofTree
    -- supplied provers
      provers :: QBF -> [Prover Sign FORMULA Morphism QBFSL ProofTree]
provers QBF = [Prover Sign FORMULA Morphism QBFSL ProofTree
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
-> Maybe
     ((BASICSPEC, Sign, GlobalAnnos)
      -> Result (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA]))
basic_analysis QBF =
              ((BASICSPEC, Sign, GlobalAnnos)
 -> Result (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA]))
-> Maybe
     ((BASICSPEC, Sign, GlobalAnnos)
      -> Result (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA]))
forall a. a -> Maybe a
Just (BASICSPEC, Sign, GlobalAnnos)
-> Result (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA])
basicPropositionalAnalysis
          empty_signature :: QBF -> Sign
empty_signature QBF = Sign
emptySig
          is_subsig :: QBF -> Sign -> Sign -> Bool
is_subsig QBF = Sign -> Sign -> Bool
isSubSigOf
          subsig_inclusion :: QBF -> Sign -> Sign -> Result Morphism
subsig_inclusion QBF s :: Sign
s = Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism -> Result Morphism)
-> (Sign -> Morphism) -> Sign -> Result Morphism
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Sign -> Morphism
inclusionMap Sign
s
          signature_union :: QBF -> Sign -> Sign -> Result Sign
signature_union QBF = Sign -> Sign -> Result Sign
sigUnion
          symbol_to_raw :: QBF -> Symbol -> Symbol
symbol_to_raw QBF = Symbol -> Symbol
symbolToRaw
          id_to_raw :: QBF -> Id -> Symbol
id_to_raw QBF = Id -> Symbol
idToRaw
          matches :: QBF -> Symbol -> Symbol -> Bool
matches QBF = Symbol -> Symbol -> Bool
Symbol.matches
          stat_symb_items :: QBF -> Sign -> [SYMBITEMS] -> Result [Symbol]
stat_symb_items QBF _ = [SYMBITEMS] -> Result [Symbol]
mkStatSymbItems
          stat_symb_map_items :: QBF
-> Sign -> Maybe Sign -> [SYMBMAPITEMS] -> Result (EndoMap Symbol)
stat_symb_map_items QBF _ _ = [SYMBMAPITEMS] -> Result (EndoMap Symbol)
mkStatSymbMapItem
          morphism_union :: QBF -> Morphism -> Morphism -> Result Morphism
morphism_union QBF = Morphism -> Morphism -> Result Morphism
morphismUnion
          induced_from_morphism :: QBF -> EndoMap Symbol -> Sign -> Result Morphism
induced_from_morphism QBF = EndoMap Symbol -> Sign -> Result Morphism
inducedFromMorphism
          induced_from_to_morphism :: QBF
-> EndoMap Symbol
-> ExtSign Sign Symbol
-> ExtSign Sign Symbol
-> Result Morphism
induced_from_to_morphism QBF = EndoMap Symbol
-> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism
inducedFromToMorphism
          signature_colimit :: QBF -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism)
signature_colimit QBF = Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism)
signatureColimit

-- | Sublogics
instance SemiLatticeWithTop QBFSL where
    lub :: QBFSL -> QBFSL -> QBFSL
lub = QBFSL -> QBFSL -> QBFSL
sublogicsMax
    top :: QBFSL
top = QBFSL
Sublogic.top

instance MinSublogic QBFSL BASICSPEC where
     minSublogic :: BASICSPEC -> QBFSL
minSublogic = QBFSL -> BASICSPEC -> QBFSL
slBasicSpec QBFSL
bottom

instance MinSublogic QBFSL Sign where
    minSublogic :: Sign -> QBFSL
minSublogic = QBFSL -> Sign -> QBFSL
slSig QBFSL
bottom

instance SublogicName QBFSL where
    sublogicName :: QBFSL -> String
sublogicName = QBFSL -> String
sublogicsName

instance MinSublogic QBFSL FORMULA where
    minSublogic :: FORMULA -> QBFSL
minSublogic = QBFSL -> FORMULA -> QBFSL
slForm QBFSL
bottom

instance MinSublogic QBFSL Symbol where
    minSublogic :: Symbol -> QBFSL
minSublogic = QBFSL -> Symbol -> QBFSL
slSym QBFSL
bottom

instance MinSublogic QBFSL SYMBITEMS where
    minSublogic :: SYMBITEMS -> QBFSL
minSublogic = QBFSL -> SYMBITEMS -> QBFSL
slSymit QBFSL
bottom

instance MinSublogic QBFSL Morphism where
    minSublogic :: Morphism -> QBFSL
minSublogic = QBFSL -> Morphism -> QBFSL
slMor QBFSL
bottom

instance MinSublogic QBFSL SYMBMAPITEMS where
    minSublogic :: SYMBMAPITEMS -> QBFSL
minSublogic = QBFSL -> SYMBMAPITEMS -> QBFSL
slSymmap QBFSL
bottom

instance ProjectSublogicM QBFSL Symbol where
    projectSublogicM :: QBFSL -> Symbol -> Maybe Symbol
projectSublogicM = QBFSL -> Symbol -> Maybe Symbol
prSymbolM

instance ProjectSublogic QBFSL Sign where
    projectSublogic :: QBFSL -> Sign -> Sign
projectSublogic = QBFSL -> Sign -> Sign
prSig

instance ProjectSublogic QBFSL Morphism where
    projectSublogic :: QBFSL -> Morphism -> Morphism
projectSublogic = QBFSL -> Morphism -> Morphism
prMor

instance ProjectSublogicM QBFSL SYMBMAPITEMS where
    projectSublogicM :: QBFSL -> SYMBMAPITEMS -> Maybe SYMBMAPITEMS
projectSublogicM = QBFSL -> SYMBMAPITEMS -> Maybe SYMBMAPITEMS
prSymMapM

instance ProjectSublogicM QBFSL SYMBITEMS where
    projectSublogicM :: QBFSL -> SYMBITEMS -> Maybe SYMBITEMS
projectSublogicM = QBFSL -> SYMBITEMS -> Maybe SYMBITEMS
prSymM

instance ProjectSublogic QBFSL BASICSPEC where
    projectSublogic :: QBFSL -> BASICSPEC -> BASICSPEC
projectSublogic = QBFSL -> BASICSPEC -> BASICSPEC
prBasicSpec

instance ProjectSublogicM QBFSL FORMULA where
    projectSublogicM :: QBFSL -> FORMULA -> Maybe FORMULA
projectSublogicM = QBFSL -> FORMULA -> Maybe FORMULA
prFormulaM