{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE LambdaCase #-}
{- |
Module      :  ./Propositional/Sublogic.hs
Description :  Sublogics 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)

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 :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulae)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulae)
-> (forall (m :: * -> *).
    MonadPlus 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 :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus 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 :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PropFormulae -> m PropFormulae
forall (m :: * -> *).
MonadPlus 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 :: * -> *).
MonadPlus 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 :: * -> *).
MonadPlus 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 :: * -> *).
Monad 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 :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> PropSL -> m PropSL)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PropSL -> m PropSL)
-> (forall (m :: * -> *).
    MonadPlus 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 :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus 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 :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PropSL -> m PropSL
forall (m :: * -> *).
MonadPlus 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 :: * -> *).
MonadPlus 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 :: * -> *).
MonadPlus 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 :: * -> *).
Monad 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