```{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE LambdaCase #-}
{- |
Module      :  ./Propositional/Sublogic.hs
Description :  Sublogics for propositional logic
Copyright   :  (c) Dominik Luecke, Uni Bremen 2007

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

Sublogics for Propositional Logic
-}

{-
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.Sublogic
(
sl_basic_spec                  -- determine sublogic for basic spec
, PropFormulae (..)             -- types of propositional formulae
, PropSL (..)                   -- sublogics for propositional logic
, sublogics_max                 -- join of sublogics
, top                           -- Propositional
, bottom                        -- Horn
, sublogics_all                 -- all sublogics
, sublogics_name                -- name of sublogics
, compareLE
, sl_sig                        -- sublogic for a signature
, sl_form                       -- sublogic for a formula
, sl_sym                        -- sublogic for symbols
, sl_symit                      -- sublogic for symbol items
, sl_mor                        -- sublogic for morphisms
, sl_symmap                     -- sublogic for symbol map items
, prSymbolM                     -- projection of symbols
, prSig                         -- projections of signatures
, prMor                         -- projections of morphisms
, prSymMapM                     -- projections of symbol maps
, prSymM                        -- projections of SYMB_ITEMS
, prFormulaM                    -- projections of formulae
, prBasicSpec                   -- projections of basic specs
, isNNF
, isCNF
, isDNF
, isHC
, isHF
)
where

import Data.Data
import Data.Set
import qualified Data.List as DL

import qualified Propositional.AS_BASIC_Propositional as AS_BASIC

import qualified Propositional.Sign as Sign
import qualified Propositional.Symbol as Symbol
import qualified Propositional.Morphism as Morphism

import qualified Common.AS_Annotation as AS_Anno

{- -----------------------------------------------------------------------------
datatypes                                                                 --
----------------------------------------------------------------------------- -}

-- | types of propositional formulae
data PropFormulae = HornFormula             -- Formual that after conversion to CNF yields a Horn Clause
| NegationNormalForm      -- Formula in Negation Normal Form
| DisjunctiveNormalForm   -- Formula in Disjunctive Normal Form
| ConjunctiveNormalForm   -- Formula in Conjunctive Normal Form
| HornClause              -- Horn Clauses, i.e., a Horn Formula that is also in CNF
deriving (Int -> PropFormulae -> ShowS
[PropFormulae] -> ShowS
PropFormulae -> String
(Int -> PropFormulae -> ShowS)
-> (PropFormulae -> String)
-> ([PropFormulae] -> ShowS)
-> Show PropFormulae
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PropFormulae] -> ShowS
\$cshowList :: [PropFormulae] -> ShowS
show :: PropFormulae -> String
\$cshow :: PropFormulae -> String
showsPrec :: Int -> PropFormulae -> ShowS
\$cshowsPrec :: Int -> PropFormulae -> ShowS
Show, PropFormulae -> PropFormulae -> Bool
(PropFormulae -> PropFormulae -> Bool)
-> (PropFormulae -> PropFormulae -> Bool) -> Eq PropFormulae
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PropFormulae -> PropFormulae -> Bool
\$c/= :: PropFormulae -> PropFormulae -> Bool
== :: PropFormulae -> PropFormulae -> Bool
\$c== :: PropFormulae -> PropFormulae -> Bool
Eq, Eq PropFormulae
Eq PropFormulae =>
(PropFormulae -> PropFormulae -> Ordering)
-> (PropFormulae -> PropFormulae -> Bool)
-> (PropFormulae -> PropFormulae -> Bool)
-> (PropFormulae -> PropFormulae -> Bool)
-> (PropFormulae -> PropFormulae -> Bool)
-> (PropFormulae -> PropFormulae -> PropFormulae)
-> (PropFormulae -> PropFormulae -> PropFormulae)
-> Ord PropFormulae
PropFormulae -> PropFormulae -> Bool
PropFormulae -> PropFormulae -> Ordering
PropFormulae -> PropFormulae -> PropFormulae
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: PropFormulae -> PropFormulae -> PropFormulae
\$cmin :: PropFormulae -> PropFormulae -> PropFormulae
max :: PropFormulae -> PropFormulae -> PropFormulae
\$cmax :: PropFormulae -> PropFormulae -> PropFormulae
>= :: PropFormulae -> PropFormulae -> Bool
\$c>= :: PropFormulae -> PropFormulae -> Bool
> :: PropFormulae -> PropFormulae -> Bool
\$c> :: PropFormulae -> PropFormulae -> Bool
<= :: PropFormulae -> PropFormulae -> Bool
\$c<= :: PropFormulae -> PropFormulae -> Bool
< :: PropFormulae -> PropFormulae -> Bool
\$c< :: PropFormulae -> PropFormulae -> Bool
compare :: PropFormulae -> PropFormulae -> Ordering
\$ccompare :: PropFormulae -> PropFormulae -> Ordering
\$cp1Ord :: Eq PropFormulae
Ord, Typeable, Typeable PropFormulae
Constr
DataType
Typeable PropFormulae =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PropFormulae -> c PropFormulae)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PropFormulae)
-> (PropFormulae -> Constr)
-> (PropFormulae -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PropFormulae))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PropFormulae))
-> ((forall b. Data b => b -> b) -> PropFormulae -> PropFormulae)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PropFormulae -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PropFormulae -> r)
-> (forall u. (forall d. Data d => d -> u) -> PropFormulae -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> PropFormulae -> u)
-> (forall (m :: * -> *).
(forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulae)
-> (forall (m :: * -> *).
(forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulae)
-> (forall (m :: * -> *).
(forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulae)
-> Data PropFormulae
PropFormulae -> Constr
PropFormulae -> DataType
(forall b. Data b => b -> b) -> PropFormulae -> PropFormulae
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PropFormulae -> c PropFormulae
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PropFormulae
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> PropFormulae -> u
forall u. (forall d. Data d => d -> u) -> PropFormulae -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PropFormulae -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PropFormulae -> r
forall (m :: * -> *).
(forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulae
forall (m :: * -> *).
(forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulae
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PropFormulae
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PropFormulae -> c PropFormulae
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PropFormulae)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PropFormulae)
\$cHornClause :: Constr
\$cConjunctiveNormalForm :: Constr
\$cDisjunctiveNormalForm :: Constr
\$cNegationNormalForm :: Constr
\$cHornFormula :: Constr
\$tPropFormulae :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulae
\$cgmapMo :: forall (m :: * -> *).
(forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulae
gmapMp :: (forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulae
\$cgmapMp :: forall (m :: * -> *).
(forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulae
gmapM :: (forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulae
\$cgmapM :: forall (m :: * -> *).
(forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulae
gmapQi :: Int -> (forall d. Data d => d -> u) -> PropFormulae -> u
\$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PropFormulae -> u
gmapQ :: (forall d. Data d => d -> u) -> PropFormulae -> [u]
\$cgmapQ :: forall u. (forall d. Data d => d -> u) -> PropFormulae -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PropFormulae -> r
\$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PropFormulae -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PropFormulae -> r
\$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PropFormulae -> r
gmapT :: (forall b. Data b => b -> b) -> PropFormulae -> PropFormulae
\$cgmapT :: (forall b. Data b => b -> b) -> PropFormulae -> PropFormulae
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PropFormulae)
\$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PropFormulae)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c PropFormulae)
\$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PropFormulae)
dataTypeOf :: PropFormulae -> DataType
\$cdataTypeOf :: PropFormulae -> DataType
toConstr :: PropFormulae -> Constr
\$ctoConstr :: PropFormulae -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PropFormulae
\$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PropFormulae
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PropFormulae -> c PropFormulae
\$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PropFormulae -> c PropFormulae
\$cp1Data :: Typeable PropFormulae
Data)

-- | sublogics for propositional logic
data PropSL = PropSL
{
PropSL -> Set PropFormulae
format :: Set PropFormulae     -- Structural restrictions
{-
- Each restriction should be an element of the set.
- Obviously `PlainFormula` can be part of every format because
- it does not add any requirements. By convention, the set should
- contain all restrictions that are applicable. E.g., instead of
- {CNF} it should only be {CNF, NNF}. A Formula without any restrictions
- is represented as an empty set, i.e., {}.
-}
} deriving (Int -> PropSL -> ShowS
[PropSL] -> ShowS
PropSL -> String
(Int -> PropSL -> ShowS)
-> (PropSL -> String) -> ([PropSL] -> ShowS) -> Show PropSL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PropSL] -> ShowS
\$cshowList :: [PropSL] -> ShowS
show :: PropSL -> String
\$cshow :: PropSL -> String
showsPrec :: Int -> PropSL -> ShowS
\$cshowsPrec :: Int -> PropSL -> ShowS
Show, PropSL -> PropSL -> Bool
(PropSL -> PropSL -> Bool)
-> (PropSL -> PropSL -> Bool) -> Eq PropSL
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PropSL -> PropSL -> Bool
\$c/= :: PropSL -> PropSL -> Bool
== :: PropSL -> PropSL -> Bool
\$c== :: PropSL -> PropSL -> Bool
Eq, Eq PropSL
Eq PropSL =>
(PropSL -> PropSL -> Ordering)
-> (PropSL -> PropSL -> Bool)
-> (PropSL -> PropSL -> Bool)
-> (PropSL -> PropSL -> Bool)
-> (PropSL -> PropSL -> Bool)
-> (PropSL -> PropSL -> PropSL)
-> (PropSL -> PropSL -> PropSL)
-> Ord PropSL
PropSL -> PropSL -> Bool
PropSL -> PropSL -> Ordering
PropSL -> PropSL -> PropSL
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: PropSL -> PropSL -> PropSL
\$cmin :: PropSL -> PropSL -> PropSL
max :: PropSL -> PropSL -> PropSL
\$cmax :: PropSL -> PropSL -> PropSL
>= :: PropSL -> PropSL -> Bool
\$c>= :: PropSL -> PropSL -> Bool
> :: PropSL -> PropSL -> Bool
\$c> :: PropSL -> PropSL -> Bool
<= :: PropSL -> PropSL -> Bool
\$c<= :: PropSL -> PropSL -> Bool
< :: PropSL -> PropSL -> Bool
\$c< :: PropSL -> PropSL -> Bool
compare :: PropSL -> PropSL -> Ordering
\$ccompare :: PropSL -> PropSL -> Ordering
\$cp1Ord :: Eq PropSL
Ord, Typeable, Typeable PropSL
Constr
DataType
Typeable PropSL =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PropSL -> c PropSL)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PropSL)
-> (PropSL -> Constr)
-> (PropSL -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PropSL))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PropSL))
-> ((forall b. Data b => b -> b) -> PropSL -> PropSL)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PropSL -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PropSL -> r)
-> (forall u. (forall d. Data d => d -> u) -> PropSL -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> PropSL -> u)
-> (forall (m :: * -> *).
(forall d. Data d => d -> m d) -> PropSL -> m PropSL)
-> (forall (m :: * -> *).
(forall d. Data d => d -> m d) -> PropSL -> m PropSL)
-> (forall (m :: * -> *).
(forall d. Data d => d -> m d) -> PropSL -> m PropSL)
-> Data PropSL
PropSL -> Constr
PropSL -> DataType
(forall b. Data b => b -> b) -> PropSL -> PropSL
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PropSL -> c PropSL
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PropSL
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> PropSL -> u
forall u. (forall d. Data d => d -> u) -> PropSL -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PropSL -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PropSL -> r
forall (m :: * -> *).
(forall d. Data d => d -> m d) -> PropSL -> m PropSL
forall (m :: * -> *).
(forall d. Data d => d -> m d) -> PropSL -> m PropSL
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PropSL
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PropSL -> c PropSL
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PropSL)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PropSL)
\$cPropSL :: Constr
\$tPropSL :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> PropSL -> m PropSL
\$cgmapMo :: forall (m :: * -> *).
(forall d. Data d => d -> m d) -> PropSL -> m PropSL
gmapMp :: (forall d. Data d => d -> m d) -> PropSL -> m PropSL
\$cgmapMp :: forall (m :: * -> *).
(forall d. Data d => d -> m d) -> PropSL -> m PropSL
gmapM :: (forall d. Data d => d -> m d) -> PropSL -> m PropSL
\$cgmapM :: forall (m :: * -> *).
(forall d. Data d => d -> m d) -> PropSL -> m PropSL
gmapQi :: Int -> (forall d. Data d => d -> u) -> PropSL -> u
\$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PropSL -> u
gmapQ :: (forall d. Data d => d -> u) -> PropSL -> [u]
\$cgmapQ :: forall u. (forall d. Data d => d -> u) -> PropSL -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PropSL -> r
\$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PropSL -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PropSL -> r
\$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PropSL -> r
gmapT :: (forall b. Data b => b -> b) -> PropSL -> PropSL
\$cgmapT :: (forall b. Data b => b -> b) -> PropSL -> PropSL
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PropSL)
\$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PropSL)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c PropSL)
\$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PropSL)
dataTypeOf :: PropSL -> DataType
\$cdataTypeOf :: PropSL -> DataType
toConstr :: PropSL -> Constr
\$ctoConstr :: PropSL -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PropSL
\$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PropSL
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PropSL -> c PropSL
\$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PropSL -> c PropSL
\$cp1Data :: Typeable PropSL
Data)

isNNF :: PropSL -> Bool
isNNF :: PropSL -> Bool
isNNF sl :: PropSL
sl = PropFormulae
NegationNormalForm PropFormulae -> Set PropFormulae -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` PropSL -> Set PropFormulae
format PropSL
sl

isDNF :: PropSL -> Bool
isDNF :: PropSL -> Bool
isDNF sl :: PropSL
sl = PropFormulae
DisjunctiveNormalForm PropFormulae -> Set PropFormulae -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` PropSL -> Set PropFormulae
format PropSL
sl

isCNF :: PropSL -> Bool
isCNF :: PropSL -> Bool
isCNF sl :: PropSL
sl = PropFormulae
ConjunctiveNormalForm PropFormulae -> Set PropFormulae -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` PropSL -> Set PropFormulae
format PropSL
sl

isHC :: PropSL -> Bool
isHC :: PropSL -> Bool
isHC sl :: PropSL
sl = PropFormulae
HornClause PropFormulae -> Set PropFormulae -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` PropSL -> Set PropFormulae
format PropSL
sl

isHF :: PropSL -> Bool
isHF :: PropSL -> Bool
isHF sl :: PropSL
sl = PropFormulae
HornFormula PropFormulae -> Set PropFormulae -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` PropSL -> Set PropFormulae
format PropSL
sl

-- | comparison of sublogics
compareLE :: PropSL -> PropSL -> Bool
compareLE :: PropSL -> PropSL -> Bool
compareLE p1 :: PropSL
p1 p2 :: PropSL
p2 =
let f1 :: Set PropFormulae
f1 = PropSL -> Set PropFormulae
format PropSL
p1
f2 :: Set PropFormulae
f2 = PropSL -> Set PropFormulae
format PropSL
p2
in
Set PropFormulae
f2 Set PropFormulae -> Set PropFormulae -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`isSubsetOf` Set PropFormulae
f1

{- ----------------------------------------------------------------------------
Special elements in the Lattice of logics                                --
---------------------------------------------------------------------------- -}

top :: PropSL
top :: PropSL
top = Set PropFormulae -> PropSL
PropSL Set PropFormulae
forall a. Set a
empty

bottom :: PropSL
bottom :: PropSL
bottom = Set PropFormulae -> PropSL
PropSL (Set PropFormulae -> PropSL) -> Set PropFormulae -> PropSL
forall a b. (a -> b) -> a -> b
\$ [PropFormulae] -> Set PropFormulae
forall a. Ord a => [a] -> Set a
fromList [PropFormulae
HornClause, PropFormulae
ConjunctiveNormalForm, PropFormulae
DisjunctiveNormalForm, PropFormulae
NegationNormalForm, PropFormulae
HornFormula]

need_PF :: PropSL
need_PF :: PropSL
need_PF = PropSL
bottom { format :: Set PropFormulae
format = Set PropFormulae
forall a. Set a
empty }

{- -----------------------------------------------------------------------------
join and max                                                              --
----------------------------------------------------------------------------- -}

sublogics_join :: PropSL -> PropSL -> PropSL
sublogics_join :: PropSL -> PropSL -> PropSL
sublogics_join a :: PropSL
a b :: PropSL
b = PropSL :: Set PropFormulae -> PropSL
PropSL
{
format :: Set PropFormulae
format = Set PropFormulae -> Set PropFormulae -> Set PropFormulae
forall a. Ord a => Set a -> Set a -> Set a
intersection (PropSL -> Set PropFormulae
format PropSL
a) (PropSL -> Set PropFormulae
format PropSL
b)
}

sublogics_max :: PropSL -> PropSL -> PropSL
sublogics_max :: PropSL -> PropSL -> PropSL
sublogics_max = PropSL -> PropSL -> PropSL
sublogics_join

{- -----------------------------------------------------------------------------
Helpers                                                                   --
----------------------------------------------------------------------------- -}

-- compute sublogics from a list of sublogics
--
comp_list :: [PropSL] -> PropSL
comp_list :: [PropSL] -> PropSL
comp_list = (PropSL -> PropSL -> PropSL) -> PropSL -> [PropSL] -> PropSL
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Prelude.foldl PropSL -> PropSL -> PropSL
sublogics_max PropSL
bottom

{- ----------------------------------------------------------------------------
Functions to compute minimal sublogic for a given element, these work    --
by recursing into all subelements                                        --
---------------------------------------------------------------------------- -}

-- | determines the sublogic for symbol map items
sl_symmap :: PropSL -> AS_BASIC.SYMB_MAP_ITEMS -> PropSL
sl_symmap :: PropSL -> SYMB_MAP_ITEMS -> PropSL
sl_symmap ps :: PropSL
ps _ = PropSL
ps

-- | determines the sublogic for a morphism
sl_mor :: PropSL -> Morphism.Morphism -> PropSL
sl_mor :: PropSL -> Morphism -> PropSL
sl_mor ps :: PropSL
ps _ = PropSL
ps

-- | determines the sublogic for a Signature
sl_sig :: PropSL -> Sign.Sign -> PropSL
sl_sig :: PropSL -> Sign -> PropSL
sl_sig ps :: PropSL
ps _ = PropSL
ps

-- | determines the sublogic for Symbol items
sl_symit :: PropSL -> AS_BASIC.SYMB_ITEMS -> PropSL
sl_symit :: PropSL -> SYMB_ITEMS -> PropSL
sl_symit ps :: PropSL
ps _ = PropSL
ps

-- | determines the sublogic for symbols
sl_sym :: PropSL -> Symbol.Symbol -> PropSL
sl_sym :: PropSL -> Symbol -> PropSL
sl_sym ps :: PropSL
ps _ = PropSL
ps

-- | determines sublogic for formula
sl_form :: PropSL -> AS_BASIC.FORMULA -> PropSL
sl_form :: PropSL -> FORMULA -> PropSL
sl_form ps :: PropSL
ps f :: FORMULA
f = PropSL -> PropSL -> PropSL
sublogics_max PropSL
ps (PropSL -> PropSL) -> PropSL -> PropSL
forall a b. (a -> b) -> a -> b
\$ FORMULA -> PropSL
analyzeFormula FORMULA
f

moreThanNLit :: [AS_BASIC.FORMULA] -> Int -> Bool
moreThanNLit :: [FORMULA] -> Int -> Bool
moreThanNLit form :: [FORMULA]
form n :: Int
n = (Int -> Bool -> Int) -> Int -> [Bool] -> Int
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Prelude.foldl (\ y :: Int
y x :: Bool
x -> if Bool
x then Int
y Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 else Int
y) 0
((FORMULA -> Bool) -> [FORMULA] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
Prelude.map FORMULA -> Bool
isPosLiteral [FORMULA]
form) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
n

-- determines wheter a Formula is a literal
isLiteral :: AS_BASIC.FORMULA -> Bool
isLiteral :: FORMULA -> Bool
isLiteral (AS_BASIC.Predication _) = Bool
True
isLiteral (AS_BASIC.Negation (AS_BASIC.Predication _) _ ) = Bool
True
isLiteral (AS_BASIC.Negation _ _) = Bool
False
isLiteral (AS_BASIC.Conjunction _ _) = Bool
False
isLiteral (AS_BASIC.Implication {}) = Bool
False
isLiteral (AS_BASIC.Equivalence {}) = Bool
False
isLiteral (AS_BASIC.Disjunction _ _) = Bool
False
isLiteral (AS_BASIC.True_atom _ ) = Bool
True
isLiteral (AS_BASIC.False_atom _) = Bool
True

-- determines wheter a Formula is a positive literal
isPosLiteral :: AS_BASIC.FORMULA -> Bool
isPosLiteral :: FORMULA -> Bool
isPosLiteral (AS_BASIC.Predication _) = Bool
True
isPosLiteral (AS_BASIC.Negation _ _) = Bool
False
isPosLiteral (AS_BASIC.Conjunction _ _) = Bool
False
isPosLiteral (AS_BASIC.Implication {}) = Bool
False
isPosLiteral (AS_BASIC.Equivalence {}) = Bool
False
isPosLiteral (AS_BASIC.Disjunction _ _) = Bool
False
isPosLiteral (AS_BASIC.True_atom _ ) = Bool
True
isPosLiteral (AS_BASIC.False_atom _) = Bool
True

-- | determines subloig for basic items
sl_basic_items :: PropSL -> AS_BASIC.BASIC_ITEMS -> PropSL
sl_basic_items :: PropSL -> BASIC_ITEMS -> PropSL
sl_basic_items ps :: PropSL
ps bi :: BASIC_ITEMS
bi =
case BASIC_ITEMS
bi of
AS_BASIC.Pred_decl _ -> PropSL
ps
AS_BASIC.Axiom_items xs :: [Annoted FORMULA]
xs -> [PropSL] -> PropSL
comp_list ([PropSL] -> PropSL) -> [PropSL] -> PropSL
forall a b. (a -> b) -> a -> b
\$ (Annoted FORMULA -> PropSL) -> [Annoted FORMULA] -> [PropSL]
forall a b. (a -> b) -> [a] -> [b]
Prelude.map (PropSL -> FORMULA -> PropSL
sl_form PropSL
ps (FORMULA -> PropSL)
-> (Annoted FORMULA -> FORMULA) -> Annoted FORMULA -> PropSL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted FORMULA -> FORMULA
forall a. Annoted a -> a
AS_Anno.item) [Annoted FORMULA]
xs

-- | determines sublogic for basic spec
sl_basic_spec :: PropSL -> AS_BASIC.BASIC_SPEC -> PropSL
sl_basic_spec :: PropSL -> BASIC_SPEC -> PropSL
sl_basic_spec ps :: PropSL
ps (AS_BASIC.Basic_spec spec :: [Annoted BASIC_ITEMS]
spec) =
[PropSL] -> PropSL
comp_list ([PropSL] -> PropSL) -> [PropSL] -> PropSL
forall a b. (a -> b) -> a -> b
\$ (Annoted BASIC_ITEMS -> PropSL)
-> [Annoted BASIC_ITEMS] -> [PropSL]
forall a b. (a -> b) -> [a] -> [b]
Prelude.map (PropSL -> BASIC_ITEMS -> PropSL
sl_basic_items PropSL
ps (BASIC_ITEMS -> PropSL)
-> (Annoted BASIC_ITEMS -> BASIC_ITEMS)
-> Annoted BASIC_ITEMS
-> PropSL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted BASIC_ITEMS -> BASIC_ITEMS
forall a. Annoted a -> a
AS_Anno.item) [Annoted BASIC_ITEMS]
spec

-- | all sublogics
sublogics_all :: [PropSL]
sublogics_all :: [PropSL]
sublogics_all =
(Set PropFormulae -> PropSL) -> [Set PropFormulae] -> [PropSL]
forall a b. (a -> b) -> [a] -> [b]
Prelude.map (\x :: Set PropFormulae
x -> PropSL :: Set PropFormulae -> PropSL
PropSL{ format :: Set PropFormulae
format = Set PropFormulae
x }) ([Set PropFormulae] -> [PropSL]) -> [Set PropFormulae] -> [PropSL]
forall a b. (a -> b) -> a -> b
\$
(Set PropFormulae -> Bool)
-> [Set PropFormulae] -> [Set PropFormulae]
forall a. (a -> Bool) -> [a] -> [a]
Prelude.filter Set PropFormulae -> Bool
isIllegalConfig ([Set PropFormulae] -> [Set PropFormulae])
-> [Set PropFormulae] -> [Set PropFormulae]
forall a b. (a -> b) -> a -> b
\$
Set (Set PropFormulae) -> [Set PropFormulae]
forall a. Set a -> [a]
toList (Set (Set PropFormulae) -> [Set PropFormulae])
-> Set (Set PropFormulae) -> [Set PropFormulae]
forall a b. (a -> b) -> a -> b
\$ Set PropFormulae -> Set (Set PropFormulae)
forall a. Set a -> Set (Set a)
powerSet (Set PropFormulae -> Set (Set PropFormulae))
-> Set PropFormulae -> Set (Set PropFormulae)
forall a b. (a -> b) -> a -> b
\$ [PropFormulae] -> Set PropFormulae
forall a. Ord a => [a] -> Set a
fromList [PropFormulae
NegationNormalForm, PropFormulae
DisjunctiveNormalForm, PropFormulae
ConjunctiveNormalForm, PropFormulae
HornClause]
where
isIllegalConfig :: Set PropFormulae -> Bool
isIllegalConfig :: Set PropFormulae -> Bool
isIllegalConfig restr :: Set PropFormulae
restr | PropFormulae
HornClause PropFormulae -> Set PropFormulae -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Set PropFormulae
restr Bool -> Bool -> Bool
&& PropFormulae
ConjunctiveNormalForm PropFormulae -> Set PropFormulae -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Set PropFormulae
restr = Bool
False
| PropFormulae
ConjunctiveNormalForm PropFormulae -> Set PropFormulae -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Set PropFormulae
restr Bool -> Bool -> Bool
&& PropFormulae
NegationNormalForm PropFormulae -> Set PropFormulae -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Set PropFormulae
restr = Bool
False
| PropFormulae
DisjunctiveNormalForm PropFormulae -> Set PropFormulae -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Set PropFormulae
restr Bool -> Bool -> Bool
&& PropFormulae
NegationNormalForm PropFormulae -> Set PropFormulae -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Set PropFormulae
restr = Bool
False
| Bool
otherwise = Bool
True

{- -----------------------------------------------------------------------------
Conversion functions to String                                            --
----------------------------------------------------------------------------- -}

sublogics_name :: PropSL -> String
sublogics_name :: PropSL -> String
sublogics_name f :: PropSL
f = if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Prelude.null [String]
listOfSLs then "PlainFormula" else String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
DL.intercalate "_" [String]
listOfSLs
where
listOfSLs :: [String]
listOfSLs = (PropFormulae -> String) -> [PropFormulae] -> [String]
forall a b. (a -> b) -> [a] -> [b]
Prelude.map (\case
HornFormula -> "HornFormula"
HornClause -> "HornClause"
ConjunctiveNormalForm -> "CNF"
DisjunctiveNormalForm -> "DNF"
NegationNormalForm -> "NNF") ([PropFormulae] -> [String]) -> [PropFormulae] -> [String]
forall a b. (a -> b) -> a -> b
\$ Set PropFormulae -> [PropFormulae]
forall a. Set a -> [a]
toList (Set PropFormulae -> [PropFormulae])
-> Set PropFormulae -> [PropFormulae]
forall a b. (a -> b) -> a -> b
\$ PropSL -> Set PropFormulae
format PropSL
f

{- -----------------------------------------------------------------------------
Projections to sublogics                                                  --
----------------------------------------------------------------------------- -}

prSymbolM :: PropSL -> Symbol.Symbol -> Maybe Symbol.Symbol
prSymbolM :: PropSL -> Symbol -> Maybe Symbol
prSymbolM _ = Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just

prSig :: PropSL -> Sign.Sign -> Sign.Sign
prSig :: PropSL -> Sign -> Sign
prSig _ sig :: Sign
sig = Sign
sig

prMor :: PropSL -> Morphism.Morphism -> Morphism.Morphism
prMor :: PropSL -> Morphism -> Morphism
prMor _ mor :: Morphism
mor = Morphism
mor

prSymMapM :: PropSL
-> AS_BASIC.SYMB_MAP_ITEMS
-> Maybe AS_BASIC.SYMB_MAP_ITEMS
prSymMapM :: PropSL -> SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS
prSymMapM _ = SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS
forall a. a -> Maybe a
Just

prSymM :: PropSL -> AS_BASIC.SYMB_ITEMS -> Maybe AS_BASIC.SYMB_ITEMS
prSymM :: PropSL -> SYMB_ITEMS -> Maybe SYMB_ITEMS
prSymM _ = SYMB_ITEMS -> Maybe SYMB_ITEMS
forall a. a -> Maybe a
Just

-- keep an element if its computed sublogic is in the given sublogic
--

prFormulaM :: PropSL -> AS_BASIC.FORMULA -> Maybe AS_BASIC.FORMULA
prFormulaM :: PropSL -> FORMULA -> Maybe FORMULA
prFormulaM sl :: PropSL
sl form :: FORMULA
form
| PropSL -> PropSL -> Bool
compareLE (PropSL -> FORMULA -> PropSL
sl_form PropSL
bottom FORMULA
form) PropSL
sl = FORMULA -> Maybe FORMULA
forall a. a -> Maybe a
Just FORMULA
form
| Bool
otherwise = Maybe FORMULA
forall a. Maybe a
Nothing

prPredItem :: PropSL -> AS_BASIC.PRED_ITEM -> AS_BASIC.PRED_ITEM
prPredItem :: PropSL -> PRED_ITEM -> PRED_ITEM
prPredItem _ prI :: PRED_ITEM
prI = PRED_ITEM
prI

prBASIC_items :: PropSL -> AS_BASIC.BASIC_ITEMS -> AS_BASIC.BASIC_ITEMS
prBASIC_items :: PropSL -> BASIC_ITEMS -> BASIC_ITEMS
prBASIC_items pSL :: PropSL
pSL bI :: BASIC_ITEMS
bI =
case BASIC_ITEMS
bI of
AS_BASIC.Pred_decl pI :: PRED_ITEM
pI -> PRED_ITEM -> BASIC_ITEMS
AS_BASIC.Pred_decl (PRED_ITEM -> BASIC_ITEMS) -> PRED_ITEM -> BASIC_ITEMS
forall a b. (a -> b) -> a -> b
\$ PropSL -> PRED_ITEM -> PRED_ITEM
prPredItem PropSL
pSL PRED_ITEM
pI
AS_BASIC.Axiom_items aIS :: [Annoted FORMULA]
aIS -> [Annoted FORMULA] -> BASIC_ITEMS
AS_BASIC.Axiom_items ([Annoted FORMULA] -> BASIC_ITEMS)
-> [Annoted FORMULA] -> BASIC_ITEMS
forall a b. (a -> b) -> a -> b
\$ (Annoted FORMULA -> [Annoted FORMULA])
-> [Annoted FORMULA] -> [Annoted FORMULA]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Annoted FORMULA -> [Annoted FORMULA]
mapH [Annoted FORMULA]
aIS
where
mapH :: AS_Anno.Annoted AS_BASIC.FORMULA
-> [AS_Anno.Annoted AS_BASIC.FORMULA]
mapH :: Annoted FORMULA -> [Annoted FORMULA]
mapH annoForm :: Annoted FORMULA
annoForm = let formP :: Maybe FORMULA
formP = PropSL -> FORMULA -> Maybe FORMULA
prFormulaM PropSL
pSL (FORMULA -> Maybe FORMULA) -> FORMULA -> Maybe FORMULA
forall a b. (a -> b) -> a -> b
\$ Annoted FORMULA -> FORMULA
forall a. Annoted a -> a
AS_Anno.item Annoted FORMULA
annoForm in
case Maybe FORMULA
formP of
Nothing -> []
Just f :: FORMULA
f -> [ Annoted :: forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
AS_Anno.Annoted
{
item :: FORMULA
AS_Anno.item = FORMULA
f
, opt_pos :: Range
AS_Anno.opt_pos = Annoted FORMULA -> Range
forall a. Annoted a -> Range
AS_Anno.opt_pos Annoted FORMULA
annoForm
, l_annos :: [Annotation]
AS_Anno.l_annos = Annoted FORMULA -> [Annotation]
forall a. Annoted a -> [Annotation]
AS_Anno.l_annos Annoted FORMULA
annoForm
, r_annos :: [Annotation]
AS_Anno.r_annos = Annoted FORMULA -> [Annotation]
forall a. Annoted a -> [Annotation]
AS_Anno.r_annos Annoted FORMULA
annoForm
}
]

prBasicSpec :: PropSL -> AS_BASIC.BASIC_SPEC -> AS_BASIC.BASIC_SPEC
prBasicSpec :: PropSL -> BASIC_SPEC -> BASIC_SPEC
prBasicSpec pSL :: PropSL
pSL (AS_BASIC.Basic_spec bS :: [Annoted BASIC_ITEMS]
bS) =
[Annoted BASIC_ITEMS] -> BASIC_SPEC
AS_BASIC.Basic_spec ([Annoted BASIC_ITEMS] -> BASIC_SPEC)
-> [Annoted BASIC_ITEMS] -> BASIC_SPEC
forall a b. (a -> b) -> a -> b
\$ (Annoted BASIC_ITEMS -> Annoted BASIC_ITEMS)
-> [Annoted BASIC_ITEMS] -> [Annoted BASIC_ITEMS]
forall a b. (a -> b) -> [a] -> [b]
Prelude.map Annoted BASIC_ITEMS -> Annoted BASIC_ITEMS
mapH [Annoted BASIC_ITEMS]
bS
where
mapH :: AS_Anno.Annoted AS_BASIC.BASIC_ITEMS
-> AS_Anno.Annoted AS_BASIC.BASIC_ITEMS
mapH :: Annoted BASIC_ITEMS -> Annoted BASIC_ITEMS
mapH aBI :: Annoted BASIC_ITEMS
aBI = Annoted :: forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
AS_Anno.Annoted
{
item :: BASIC_ITEMS
AS_Anno.item = PropSL -> BASIC_ITEMS -> BASIC_ITEMS
prBASIC_items PropSL
pSL (BASIC_ITEMS -> BASIC_ITEMS) -> BASIC_ITEMS -> BASIC_ITEMS
forall a b. (a -> b) -> a -> b
\$ Annoted BASIC_ITEMS -> BASIC_ITEMS
forall a. Annoted a -> a
AS_Anno.item Annoted BASIC_ITEMS
aBI
, opt_pos :: Range
AS_Anno.opt_pos = Annoted BASIC_ITEMS -> Range
forall a. Annoted a -> Range
AS_Anno.opt_pos Annoted BASIC_ITEMS
aBI
, l_annos :: [Annotation]
AS_Anno.l_annos = Annoted BASIC_ITEMS -> [Annotation]
forall a. Annoted a -> [Annotation]
AS_Anno.l_annos Annoted BASIC_ITEMS
aBI
, r_annos :: [Annotation]
AS_Anno.r_annos = Annoted BASIC_ITEMS -> [Annotation]
forall a. Annoted a -> [Annotation]
AS_Anno.r_annos Annoted BASIC_ITEMS
aBI
}

-- check if a formula is in a certain sublogic

analyzeFormula :: AS_BASIC.FORMULA -> PropSL
analyzeFormula :: FORMULA -> PropSL
analyzeFormula formula :: FORMULA
formula = PropSL :: Set PropFormulae -> PropSL
PropSL {
format :: Set PropFormulae
format = [PropFormulae] -> Set PropFormulae
forall a. Ord a => [a] -> Set a
fromList
([PropFormulae] -> Set PropFormulae)
-> [PropFormulae] -> Set PropFormulae
forall a b. (a -> b) -> a -> b
\$ ((FORMULA -> Bool, String) -> PropFormulae)
-> [(FORMULA -> Bool, String)] -> [PropFormulae]
forall a b. (a -> b) -> [a] -> [b]
Prelude.map ((\case
"checkNNF" -> PropFormulae
NegationNormalForm
"checkDNF" -> PropFormulae
DisjunctiveNormalForm
"checkCNF" -> PropFormulae
ConjunctiveNormalForm
"checkHornC" -> PropFormulae
HornClause
"checkHornF" -> PropFormulae
HornFormula
_ -> String -> PropFormulae
forall a. HasCallStack => String -> a
error "Unexhaustive Pattern Match") (String -> PropFormulae)
-> ((FORMULA -> Bool, String) -> String)
-> (FORMULA -> Bool, String)
-> PropFormulae
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FORMULA -> Bool, String) -> String
forall a b. (a, b) -> b
snd)
([(FORMULA -> Bool, String)] -> [PropFormulae])
-> [(FORMULA -> Bool, String)] -> [PropFormulae]
forall a b. (a -> b) -> a -> b
\$ ((FORMULA -> Bool, String) -> Bool)
-> [(FORMULA -> Bool, String)] -> [(FORMULA -> Bool, String)]
forall a. (a -> Bool) -> [a] -> [a]
Prelude.filter ((FORMULA -> Bool, String) -> FORMULA -> Bool
forall t t b. (t -> t, b) -> t -> t
`apply` FORMULA
formula)
[(FORMULA -> Bool
checkNNF, "checkNNF"), (FORMULA -> Bool
checkCNF, "checkCNF"), (FORMULA -> Bool
checkDNF, "checkDNF"), (FORMULA -> Bool
checkHC, "checkHornC"), (FORMULA -> Bool
checkHF, "checkHornF")]
}
where
apply :: (t -> t, b) -> t -> t
apply f :: (t -> t, b)
f x :: t
x = (t -> t, b) -> t -> t
forall a b. (a, b) -> a
fst (t -> t, b)
f t
x

checkNNF :: AS_BASIC.FORMULA -> Bool
checkNNF :: FORMULA -> Bool
checkNNF formula :: FORMULA
formula =
case FORMULA
formula of
AS_BASIC.Conjunction conjs :: [FORMULA]
conjs _ -> (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\case
AS_BASIC.Disjunction form :: [FORMULA]
form _ -> (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all FORMULA -> Bool
checkNNF [FORMULA]
form
AS_BASIC.Conjunction form :: [FORMULA]
form _ -> (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all FORMULA -> Bool
checkNNF [FORMULA]
form
conj :: FORMULA
conj -> FORMULA -> Bool
isLiteral FORMULA
conj) [FORMULA]
conjs
AS_BASIC.Disjunction disjs :: [FORMULA]
disjs _ -> (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\case
AS_BASIC.Disjunction form :: [FORMULA]
form _ -> (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all FORMULA -> Bool
checkNNF [FORMULA]
form
AS_BASIC.Conjunction form :: [FORMULA]
form _ -> (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all FORMULA -> Bool
checkNNF [FORMULA]
form
disj :: FORMULA
disj -> FORMULA -> Bool
isLiteral FORMULA
disj) [FORMULA]
disjs
form :: FORMULA
form -> FORMULA -> Bool
isLiteral FORMULA
form

checkDNF :: AS_BASIC.FORMULA -> Bool
checkDNF :: FORMULA -> Bool
checkDNF formula :: FORMULA
formula =
case FORMULA
formula of
AS_BASIC.Disjunction disjs :: [FORMULA]
disjs _ -> (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\case
AS_BASIC.Conjunction form :: [FORMULA]
form _ -> (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all FORMULA -> Bool
isLiteral [FORMULA]
form
disj :: FORMULA
disj -> FORMULA -> Bool
isLiteral FORMULA
disj) [FORMULA]
disjs
AS_BASIC.Conjunction form :: [FORMULA]
form _ -> (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all FORMULA -> Bool
isLiteral [FORMULA]
form
form :: FORMULA
form -> FORMULA -> Bool
isLiteral FORMULA
form

checkCNF :: AS_BASIC.FORMULA -> Bool
checkCNF :: FORMULA -> Bool
checkCNF formula :: FORMULA
formula =
case FORMULA
formula of
AS_BASIC.Conjunction conjs :: [FORMULA]
conjs _ -> (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\case
AS_BASIC.Disjunction form :: [FORMULA]
form _ -> (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all FORMULA -> Bool
isLiteral [FORMULA]
form
conj :: FORMULA
conj -> FORMULA -> Bool
isLiteral FORMULA
conj) [FORMULA]
conjs
AS_BASIC.Disjunction form :: [FORMULA]
form _ -> (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all FORMULA -> Bool
isLiteral [FORMULA]
form
form :: FORMULA
form -> FORMULA -> Bool
isLiteral FORMULA
form

checkHC :: AS_BASIC.FORMULA -> Bool
checkHC :: FORMULA -> Bool
checkHC formula :: FORMULA
formula = FORMULA -> Bool
checkHF FORMULA
formula Bool -> Bool -> Bool
&& FORMULA -> Bool
checkCNF FORMULA
formula

checkHF :: AS_BASIC.FORMULA -> Bool
checkHF :: FORMULA -> Bool
checkHF formula :: FORMULA
formula =
let
flatCNF :: FORMULA -> Bool
flatCNF (AS_BASIC.Conjunction conjs :: [FORMULA]
conjs _) = (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all FORMULA -> Bool
isPosLiteral [FORMULA]
conjs
flatCNF f :: FORMULA
f = FORMULA -> Bool
isPosLiteral FORMULA
f
in
case FORMULA
formula of
AS_BASIC.Conjunction conjs :: [FORMULA]
conjs _ -> (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\case
AS_BASIC.Disjunction disjs :: [FORMULA]
disjs _ -> [FORMULA] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((FORMULA -> Bool) -> [FORMULA] -> [FORMULA]
forall a. (a -> Bool) -> [a] -> [a]
Prelude.filter FORMULA -> Bool
isPosLiteral [FORMULA]
disjs) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 1
AS_BASIC.Implication lhs :: FORMULA
lhs rhs :: FORMULA
rhs _ -> FORMULA -> Bool
flatCNF FORMULA
lhs Bool -> Bool -> Bool
&& FORMULA -> Bool
isPosLiteral FORMULA
rhs
conj :: FORMULA
conj -> FORMULA -> Bool
isLiteral FORMULA
conj) [FORMULA]
conjs
AS_BASIC.Disjunction disjs :: [FORMULA]
disjs _ -> (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all FORMULA -> Bool
isLiteral [FORMULA]
disjs Bool -> Bool -> Bool
&& [FORMULA] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((FORMULA -> Bool) -> [FORMULA] -> [FORMULA]
forall a. (a -> Bool) -> [a] -> [a]
Prelude.filter FORMULA -> Bool
isPosLiteral [FORMULA]
disjs) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 1
AS_BASIC.Implication lhs :: FORMULA
lhs rhs :: FORMULA
rhs _ -> FORMULA -> Bool
flatCNF FORMULA
lhs Bool -> Bool -> Bool
&& FORMULA -> Bool
isPosLiteral FORMULA
rhs
form :: FORMULA
form -> FORMULA -> Bool
isLiteral FORMULA
form
```