{-# LANGUAGE MultiParamTypeClasses #-}
{- |
Module      :  ./Propositional/Logic_Propositional.hs
Description :  Instance of class Logic for propositional logic
Copyright   :  (c) Dominik Luecke, Uni Bremen 2007
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  experimental
Portability :  non-portable (imports Logic.Logic)

Instance of class Logic for the propositional logic
   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.
-}

module Propositional.Logic_Propositional where

import ATC.ProofTree ()

import Logic.Logic

import Propositional.Sign
import Propositional.Morphism
import Propositional.AS_BASIC_Propositional
import Propositional.ATC_Propositional ()
import Propositional.Fold
import Propositional.Symbol as Symbol
import Propositional.Parse_AS_Basic
import Propositional.Analysis
import Propositional.Sublogic as Sublogic
import Propositional.ProveWithTruthTable
import Propositional.Prove
import Propositional.Conservativity
import Propositional.ProveMinisat

import Common.ProverTools
import Common.Consistency
import Common.ProofTree
import Common.Id

import qualified Data.Map as Map
import Data.Monoid ()

-- | Lid for propositional logic
data Propositional = Propositional deriving Int -> Propositional -> ShowS
[Propositional] -> ShowS
Propositional -> String
(Int -> Propositional -> ShowS)
-> (Propositional -> String)
-> ([Propositional] -> ShowS)
-> Show Propositional
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Propositional] -> ShowS
$cshowList :: [Propositional] -> ShowS
show :: Propositional -> String
$cshow :: Propositional -> String
showsPrec :: Int -> Propositional -> ShowS
$cshowsPrec :: Int -> Propositional -> ShowS
Show

instance Language Propositional where
    description :: Propositional -> String
description _ = "Propositional Logic\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"

-- | 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 Propositional FORMULA
    Sign Morphism Symbol where
    negation :: Propositional -> FORMULA -> Maybe FORMULA
negation Propositional = 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
. Range -> FORMULA -> FORMULA
negForm Range
nullRange
    -- returns the set of symbols
    sym_of :: Propositional -> Sign -> [Set Symbol]
sym_of Propositional = 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
    -- returns the symbol map
    symmap_of :: Propositional -> Morphism -> EndoMap Symbol
symmap_of Propositional = Morphism -> EndoMap Symbol
getSymbolMap
    -- returns the name of a symbol
    sym_name :: Propositional -> Symbol -> Id
sym_name Propositional = Symbol -> Id
getSymbolName
    symKind :: Propositional -> Symbol -> String
symKind Propositional _ = "prop"
    -- translation of sentences along signature morphism
    map_sen :: Propositional -> Morphism -> FORMULA -> Result FORMULA
map_sen Propositional = Morphism -> FORMULA -> Result FORMULA
mapSentence
    -- there is nothing to leave out
    simplify_sen :: Propositional -> Sign -> FORMULA -> FORMULA
simplify_sen Propositional _ = FORMULA -> FORMULA
simplify

instance Semigroup BASIC_SPEC where
    (Basic_spec l1 :: [Annoted BASIC_ITEMS]
l1) <> :: BASIC_SPEC -> BASIC_SPEC -> BASIC_SPEC
<> (Basic_spec l2 :: [Annoted BASIC_ITEMS]
l2) = [Annoted BASIC_ITEMS] -> BASIC_SPEC
Basic_spec ([Annoted BASIC_ITEMS] -> BASIC_SPEC)
-> [Annoted BASIC_ITEMS] -> BASIC_SPEC
forall a b. (a -> b) -> a -> b
$ [Annoted BASIC_ITEMS]
l1 [Annoted BASIC_ITEMS]
-> [Annoted BASIC_ITEMS] -> [Annoted BASIC_ITEMS]
forall a. [a] -> [a] -> [a]
++ [Annoted BASIC_ITEMS]
l2
instance Monoid BASIC_SPEC where
    mempty :: BASIC_SPEC
mempty = [Annoted BASIC_ITEMS] -> BASIC_SPEC
Basic_spec []

-- - | Syntax of Propositional logic
instance Syntax Propositional BASIC_SPEC
    Symbol SYMB_ITEMS SYMB_MAP_ITEMS where
         parsersAndPrinters :: Propositional
-> Map
     String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
parsersAndPrinters Propositional =
           String
-> (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
-> Map
     String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
-> Map
     String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
forall b. String -> b -> Map String b -> Map String b
addSyntax "Hets" (PrefixMap -> AParser st BASIC_SPEC
forall st. PrefixMap -> AParser st BASIC_SPEC
basicSpec, BASIC_SPEC -> Doc
forall a. Pretty a => a -> Doc
pretty)
           (Map String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
 -> Map
      String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc))
-> Map
     String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
-> Map
     String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
forall a b. (a -> b) -> a -> b
$ (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
-> Map
     String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc)
forall b. b -> Map String b
makeDefault (PrefixMap -> AParser st BASIC_SPEC
forall st. PrefixMap -> AParser st BASIC_SPEC
basicSpec, BASIC_SPEC -> Doc
forall a. Pretty a => a -> Doc
pretty)
         parse_symb_items :: Propositional -> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
parse_symb_items Propositional = (PrefixMap -> AParser st SYMB_ITEMS)
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st SYMB_ITEMS)
 -> Maybe (PrefixMap -> AParser st SYMB_ITEMS))
-> (AParser st SYMB_ITEMS -> PrefixMap -> AParser st SYMB_ITEMS)
-> AParser st SYMB_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SYMB_ITEMS -> PrefixMap -> AParser st SYMB_ITEMS
forall a b. a -> b -> a
const (AParser st SYMB_ITEMS
 -> Maybe (PrefixMap -> AParser st SYMB_ITEMS))
-> AParser st SYMB_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall a b. (a -> b) -> a -> b
$ AParser st SYMB_ITEMS
forall st. GenParser Char st SYMB_ITEMS
symbItems
         parse_symb_map_items :: Propositional -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
parse_symb_map_items Propositional = (PrefixMap -> AParser st SYMB_MAP_ITEMS)
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st SYMB_MAP_ITEMS)
 -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS))
-> (AParser st SYMB_MAP_ITEMS
    -> PrefixMap -> AParser st SYMB_MAP_ITEMS)
-> AParser st SYMB_MAP_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SYMB_MAP_ITEMS -> PrefixMap -> AParser st SYMB_MAP_ITEMS
forall a b. a -> b -> a
const (AParser st SYMB_MAP_ITEMS
 -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS))
-> AParser st SYMB_MAP_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall a b. (a -> b) -> a -> b
$ AParser st SYMB_MAP_ITEMS
forall st. GenParser Char st SYMB_MAP_ITEMS
symbMapItems

-- | Instance of Logic for propositional logc
instance Logic Propositional
    PropSL                    -- Sublogics
    BASIC_SPEC                -- basic_spec
    FORMULA                   -- sentence
    SYMB_ITEMS                -- symb_items
    SYMB_MAP_ITEMS            -- symb_map_items
    Sign                          -- sign
    Morphism                  -- morphism
    Symbol                      -- symbol
    Symbol                      -- raw_symbol
    ProofTree                      -- proof_tree
    where
        -- hybridization
      parse_basic_sen :: Propositional -> Maybe (BASIC_SPEC -> AParser st FORMULA)
parse_basic_sen Propositional = (BASIC_SPEC -> AParser st FORMULA)
-> Maybe (BASIC_SPEC -> AParser st FORMULA)
forall a. a -> Maybe a
Just ((BASIC_SPEC -> AParser st FORMULA)
 -> Maybe (BASIC_SPEC -> AParser st FORMULA))
-> (BASIC_SPEC -> AParser st FORMULA)
-> Maybe (BASIC_SPEC -> AParser st FORMULA)
forall a b. (a -> b) -> a -> b
$ AParser st FORMULA -> BASIC_SPEC -> AParser st FORMULA
forall a b. a -> b -> a
const AParser st FORMULA
forall st. AParser st FORMULA
impFormula
      stability :: Propositional -> Stability
stability Propositional = Stability
Stable
      top_sublogic :: Propositional -> PropSL
top_sublogic Propositional = PropSL
Sublogic.top
      all_sublogics :: Propositional -> [PropSL]
all_sublogics Propositional = [PropSL]
sublogics_all
      empty_proof_tree :: Propositional -> ProofTree
empty_proof_tree Propositional = ProofTree
emptyProofTree
    -- supplied provers
      provers :: Propositional -> [Prover Sign FORMULA Morphism PropSL ProofTree]
provers Propositional =
        [Prover Sign FORMULA Morphism PropSL ProofTree
zchaffProver, MiniSatVer -> Prover Sign FORMULA Morphism PropSL ProofTree
minisatProver MiniSatVer
Minisat, MiniSatVer -> Prover Sign FORMULA Morphism PropSL ProofTree
minisatProver MiniSatVer
Minisat2, Prover Sign FORMULA Morphism PropSL ProofTree
ttProver]
      cons_checkers :: Propositional
-> [ConsChecker Sign FORMULA PropSL Morphism ProofTree]
cons_checkers Propositional =
        [ ConsChecker Sign FORMULA PropSL Morphism ProofTree
propConsChecker, MiniSatVer -> ConsChecker Sign FORMULA PropSL Morphism ProofTree
minisatConsChecker MiniSatVer
Minisat
        , MiniSatVer -> ConsChecker Sign FORMULA PropSL Morphism ProofTree
minisatConsChecker MiniSatVer
Minisat2, ConsChecker Sign FORMULA PropSL Morphism ProofTree
ttConsistencyChecker]
      conservativityCheck :: Propositional -> [ConservativityChecker Sign FORMULA Morphism]
conservativityCheck Propositional =
          [ String
-> IO (Maybe String)
-> ((Sign, [Named FORMULA])
    -> Morphism
    -> [Named FORMULA]
    -> IO (Result (Conservativity, [FORMULA])))
-> ConservativityChecker Sign FORMULA Morphism
forall sign sentence morphism.
String
-> IO (Maybe String)
-> ((sign, [Named sentence])
    -> morphism
    -> [Named sentence]
    -> IO (Result (Conservativity, [sentence])))
-> ConservativityChecker sign sentence morphism
ConservativityChecker "sKizzo" (String -> IO (Maybe String)
checkBinary "sKizzo") (Sign, [Named FORMULA])
-> Morphism
-> [Named FORMULA]
-> IO (Result (Conservativity, [FORMULA]))
conserCheck
          , String
-> IO (Maybe String)
-> ((Sign, [Named FORMULA])
    -> Morphism
    -> [Named FORMULA]
    -> IO (Result (Conservativity, [FORMULA])))
-> ConservativityChecker Sign FORMULA Morphism
forall sign sentence morphism.
String
-> IO (Maybe String)
-> ((sign, [Named sentence])
    -> morphism
    -> [Named sentence]
    -> IO (Result (Conservativity, [sentence])))
-> ConservativityChecker sign sentence morphism
ConservativityChecker "Truth Tables" (Maybe String -> IO (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe String
forall a. Maybe a
Nothing)
              (Sign, [Named FORMULA])
-> Morphism
-> [Named FORMULA]
-> IO (Result (Conservativity, [FORMULA]))
ttConservativityChecker]

-- | Static Analysis for propositional logic
instance StaticAnalysis Propositional
    BASIC_SPEC                -- basic_spec
    FORMULA                   -- sentence
    SYMB_ITEMS                -- symb_items
    SYMB_MAP_ITEMS            -- symb_map_items
    Sign                          -- sign
    Morphism                  -- morphism
    Symbol                      -- symbol
    Symbol                      -- raw_symbol
        where
          basic_analysis :: Propositional
-> Maybe
     ((BASIC_SPEC, Sign, GlobalAnnos)
      -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA]))
basic_analysis Propositional =
              ((BASIC_SPEC, Sign, GlobalAnnos)
 -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA]))
-> Maybe
     ((BASIC_SPEC, Sign, GlobalAnnos)
      -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA]))
forall a. a -> Maybe a
Just (BASIC_SPEC, Sign, GlobalAnnos)
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])
basicPropositionalAnalysis
          sen_analysis :: Propositional
-> Maybe ((BASIC_SPEC, Sign, FORMULA) -> Result FORMULA)
sen_analysis Propositional = ((BASIC_SPEC, Sign, FORMULA) -> Result FORMULA)
-> Maybe ((BASIC_SPEC, Sign, FORMULA) -> Result FORMULA)
forall a. a -> Maybe a
Just (BASIC_SPEC, Sign, FORMULA) -> Result FORMULA
pROPsen_analysis
          empty_signature :: Propositional -> Sign
empty_signature Propositional = Sign
emptySig
          is_subsig :: Propositional -> Sign -> Sign -> Bool
is_subsig Propositional = Sign -> Sign -> Bool
isSubSigOf
          subsig_inclusion :: Propositional -> Sign -> Sign -> Result Morphism
subsig_inclusion Propositional 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 :: Propositional -> Sign -> Sign -> Result Sign
signature_union Propositional = Sign -> Sign -> Result Sign
sigUnion
          symbol_to_raw :: Propositional -> Symbol -> Symbol
symbol_to_raw Propositional = Symbol -> Symbol
symbolToRaw
          id_to_raw :: Propositional -> Id -> Symbol
id_to_raw Propositional = Id -> Symbol
idToRaw
          matches :: Propositional -> Symbol -> Symbol -> Bool
matches Propositional = Symbol -> Symbol -> Bool
Symbol.matches
          stat_symb_items :: Propositional -> Sign -> [SYMB_ITEMS] -> Result [Symbol]
stat_symb_items Propositional _ = [SYMB_ITEMS] -> Result [Symbol]
mkStatSymbItems
          stat_symb_map_items :: Propositional
-> Sign
-> Maybe Sign
-> [SYMB_MAP_ITEMS]
-> Result (EndoMap Symbol)
stat_symb_map_items Propositional _ _ = [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol)
mkStatSymbMapItem
          morphism_union :: Propositional -> Morphism -> Morphism -> Result Morphism
morphism_union Propositional = Morphism -> Morphism -> Result Morphism
morphismUnion
          induced_from_morphism :: Propositional -> EndoMap Symbol -> Sign -> Result Morphism
induced_from_morphism Propositional = EndoMap Symbol -> Sign -> Result Morphism
inducedFromMorphism
          induced_from_to_morphism :: Propositional
-> EndoMap Symbol
-> ExtSign Sign Symbol
-> ExtSign Sign Symbol
-> Result Morphism
induced_from_to_morphism Propositional = EndoMap Symbol
-> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism
inducedFromToMorphism
          signature_colimit :: Propositional
-> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism)
signature_colimit Propositional = Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism)
signatureColimit

-- | Sublogics
instance SemiLatticeWithTop PropSL where
    lub :: PropSL -> PropSL -> PropSL
lub = PropSL -> PropSL -> PropSL
sublogics_max
    top :: PropSL
top = PropSL
Sublogic.top

instance MinSublogic PropSL BASIC_SPEC where
     minSublogic :: BASIC_SPEC -> PropSL
minSublogic = PropSL -> BASIC_SPEC -> PropSL
sl_basic_spec PropSL
bottom

instance MinSublogic PropSL Sign where
    minSublogic :: Sign -> PropSL
minSublogic = PropSL -> Sign -> PropSL
sl_sig PropSL
bottom

instance SublogicName PropSL where
    sublogicName :: PropSL -> String
sublogicName = PropSL -> String
sublogics_name

instance MinSublogic PropSL FORMULA where
    minSublogic :: FORMULA -> PropSL
minSublogic = PropSL -> FORMULA -> PropSL
sl_form PropSL
bottom

instance MinSublogic PropSL Symbol where
    minSublogic :: Symbol -> PropSL
minSublogic = PropSL -> Symbol -> PropSL
sl_sym PropSL
bottom

instance MinSublogic PropSL SYMB_ITEMS where
    minSublogic :: SYMB_ITEMS -> PropSL
minSublogic = PropSL -> SYMB_ITEMS -> PropSL
sl_symit PropSL
bottom

instance MinSublogic PropSL Morphism where
    minSublogic :: Morphism -> PropSL
minSublogic = PropSL -> Morphism -> PropSL
sl_mor PropSL
bottom

instance MinSublogic PropSL SYMB_MAP_ITEMS where
    minSublogic :: SYMB_MAP_ITEMS -> PropSL
minSublogic = PropSL -> SYMB_MAP_ITEMS -> PropSL
sl_symmap PropSL
bottom

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

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

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

instance ProjectSublogicM PropSL SYMB_MAP_ITEMS where
    projectSublogicM :: PropSL -> SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS
projectSublogicM = PropSL -> SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS
prSymMapM

instance ProjectSublogicM PropSL SYMB_ITEMS where
    projectSublogicM :: PropSL -> SYMB_ITEMS -> Maybe SYMB_ITEMS
projectSublogicM = PropSL -> SYMB_ITEMS -> Maybe SYMB_ITEMS
prSymM

instance ProjectSublogic PropSL BASIC_SPEC where
    projectSublogic :: PropSL -> BASIC_SPEC -> BASIC_SPEC
projectSublogic = PropSL -> BASIC_SPEC -> BASIC_SPEC
prBasicSpec

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