{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./QBF/Sublogic.hs
Description :  Sublogics for propositional logic
Copyright   :  (c) Jonathan von Schroeder, DFKI GmbH 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  <jonathan.von_schroeder@dfki.de>
Stability   :  experimental
Portability :  non-portable (imports Logic.Logic)

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 QBF.Sublogic
    (
     slBasicSpec                  -- determine sublogic for basic spec
    , QBFFormulae (..)             -- types of propositional formulae
    , QBFSL (..)                   -- sublogics for propositional logic
    , sublogicsMax                 -- join of sublogics
    , top                           -- Propositional
    , bottom                        -- Horn
    , sublogicsAll                 -- all sublogics
    , sublogicsName                -- name of sublogics
    , slSig                        -- sublogic for a signature
    , slForm                       -- sublogic for a formula
    , slSym                        -- sublogic for symbols
    , slSymit                      -- sublogic for symbol items
    , slMor                        -- sublogic for morphisms
    , slSymmap                     -- 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 SYMBITEMS
    , prFormulaM                    -- projections of formulae
    , prBasicSpec                   -- projections of basic specs
    , isProp
    , isHC
    )
    where

import qualified QBF.Tools as Tools
import qualified QBF.AS_BASIC_QBF as AS_BASIC
import qualified QBF.Symbol as Symbol
import qualified QBF.Morphism as Morphism

import qualified Propositional.Sign as Sign

import qualified Common.Lib.State as State
import qualified Common.AS_Annotation as AS_Anno

import Data.Data

-- | types of propositional formulae
data QBFFormulae = PlainFormula      -- Formula without structural constraints
                  | HornClause        -- Horn Clause Formulae
                  deriving (Int -> QBFFormulae -> ShowS
[QBFFormulae] -> ShowS
QBFFormulae -> String
(Int -> QBFFormulae -> ShowS)
-> (QBFFormulae -> String)
-> ([QBFFormulae] -> ShowS)
-> Show QBFFormulae
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [QBFFormulae] -> ShowS
$cshowList :: [QBFFormulae] -> ShowS
show :: QBFFormulae -> String
$cshow :: QBFFormulae -> String
showsPrec :: Int -> QBFFormulae -> ShowS
$cshowsPrec :: Int -> QBFFormulae -> ShowS
Show, QBFFormulae -> QBFFormulae -> Bool
(QBFFormulae -> QBFFormulae -> Bool)
-> (QBFFormulae -> QBFFormulae -> Bool) -> Eq QBFFormulae
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: QBFFormulae -> QBFFormulae -> Bool
$c/= :: QBFFormulae -> QBFFormulae -> Bool
== :: QBFFormulae -> QBFFormulae -> Bool
$c== :: QBFFormulae -> QBFFormulae -> Bool
Eq, Eq QBFFormulae
Eq QBFFormulae =>
(QBFFormulae -> QBFFormulae -> Ordering)
-> (QBFFormulae -> QBFFormulae -> Bool)
-> (QBFFormulae -> QBFFormulae -> Bool)
-> (QBFFormulae -> QBFFormulae -> Bool)
-> (QBFFormulae -> QBFFormulae -> Bool)
-> (QBFFormulae -> QBFFormulae -> QBFFormulae)
-> (QBFFormulae -> QBFFormulae -> QBFFormulae)
-> Ord QBFFormulae
QBFFormulae -> QBFFormulae -> Bool
QBFFormulae -> QBFFormulae -> Ordering
QBFFormulae -> QBFFormulae -> QBFFormulae
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 :: QBFFormulae -> QBFFormulae -> QBFFormulae
$cmin :: QBFFormulae -> QBFFormulae -> QBFFormulae
max :: QBFFormulae -> QBFFormulae -> QBFFormulae
$cmax :: QBFFormulae -> QBFFormulae -> QBFFormulae
>= :: QBFFormulae -> QBFFormulae -> Bool
$c>= :: QBFFormulae -> QBFFormulae -> Bool
> :: QBFFormulae -> QBFFormulae -> Bool
$c> :: QBFFormulae -> QBFFormulae -> Bool
<= :: QBFFormulae -> QBFFormulae -> Bool
$c<= :: QBFFormulae -> QBFFormulae -> Bool
< :: QBFFormulae -> QBFFormulae -> Bool
$c< :: QBFFormulae -> QBFFormulae -> Bool
compare :: QBFFormulae -> QBFFormulae -> Ordering
$ccompare :: QBFFormulae -> QBFFormulae -> Ordering
$cp1Ord :: Eq QBFFormulae
Ord, Typeable, Typeable QBFFormulae
Constr
DataType
Typeable QBFFormulae =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> QBFFormulae -> c QBFFormulae)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c QBFFormulae)
-> (QBFFormulae -> Constr)
-> (QBFFormulae -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c QBFFormulae))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c QBFFormulae))
-> ((forall b. Data b => b -> b) -> QBFFormulae -> QBFFormulae)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> QBFFormulae -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> QBFFormulae -> r)
-> (forall u. (forall d. Data d => d -> u) -> QBFFormulae -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> QBFFormulae -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> QBFFormulae -> m QBFFormulae)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> QBFFormulae -> m QBFFormulae)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> QBFFormulae -> m QBFFormulae)
-> Data QBFFormulae
QBFFormulae -> Constr
QBFFormulae -> DataType
(forall b. Data b => b -> b) -> QBFFormulae -> QBFFormulae
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QBFFormulae -> c QBFFormulae
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QBFFormulae
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) -> QBFFormulae -> u
forall u. (forall d. Data d => d -> u) -> QBFFormulae -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QBFFormulae -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QBFFormulae -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QBFFormulae -> m QBFFormulae
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QBFFormulae -> m QBFFormulae
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QBFFormulae
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QBFFormulae -> c QBFFormulae
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QBFFormulae)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c QBFFormulae)
$cHornClause :: Constr
$cPlainFormula :: Constr
$tQBFFormulae :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> QBFFormulae -> m QBFFormulae
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QBFFormulae -> m QBFFormulae
gmapMp :: (forall d. Data d => d -> m d) -> QBFFormulae -> m QBFFormulae
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QBFFormulae -> m QBFFormulae
gmapM :: (forall d. Data d => d -> m d) -> QBFFormulae -> m QBFFormulae
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QBFFormulae -> m QBFFormulae
gmapQi :: Int -> (forall d. Data d => d -> u) -> QBFFormulae -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> QBFFormulae -> u
gmapQ :: (forall d. Data d => d -> u) -> QBFFormulae -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> QBFFormulae -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QBFFormulae -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QBFFormulae -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QBFFormulae -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QBFFormulae -> r
gmapT :: (forall b. Data b => b -> b) -> QBFFormulae -> QBFFormulae
$cgmapT :: (forall b. Data b => b -> b) -> QBFFormulae -> QBFFormulae
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c QBFFormulae)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c QBFFormulae)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c QBFFormulae)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QBFFormulae)
dataTypeOf :: QBFFormulae -> DataType
$cdataTypeOf :: QBFFormulae -> DataType
toConstr :: QBFFormulae -> Constr
$ctoConstr :: QBFFormulae -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QBFFormulae
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QBFFormulae
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QBFFormulae -> c QBFFormulae
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QBFFormulae -> c QBFFormulae
$cp1Data :: Typeable QBFFormulae
Data)

-- | sublogics for propositional logic
data QBFSL = QBFSL
    {
      QBFSL -> QBFFormulae
format :: QBFFormulae     -- Structural restrictions
    } deriving (Int -> QBFSL -> ShowS
[QBFSL] -> ShowS
QBFSL -> String
(Int -> QBFSL -> ShowS)
-> (QBFSL -> String) -> ([QBFSL] -> ShowS) -> Show QBFSL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [QBFSL] -> ShowS
$cshowList :: [QBFSL] -> ShowS
show :: QBFSL -> String
$cshow :: QBFSL -> String
showsPrec :: Int -> QBFSL -> ShowS
$cshowsPrec :: Int -> QBFSL -> ShowS
Show, QBFSL -> QBFSL -> Bool
(QBFSL -> QBFSL -> Bool) -> (QBFSL -> QBFSL -> Bool) -> Eq QBFSL
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: QBFSL -> QBFSL -> Bool
$c/= :: QBFSL -> QBFSL -> Bool
== :: QBFSL -> QBFSL -> Bool
$c== :: QBFSL -> QBFSL -> Bool
Eq, Eq QBFSL
Eq QBFSL =>
(QBFSL -> QBFSL -> Ordering)
-> (QBFSL -> QBFSL -> Bool)
-> (QBFSL -> QBFSL -> Bool)
-> (QBFSL -> QBFSL -> Bool)
-> (QBFSL -> QBFSL -> Bool)
-> (QBFSL -> QBFSL -> QBFSL)
-> (QBFSL -> QBFSL -> QBFSL)
-> Ord QBFSL
QBFSL -> QBFSL -> Bool
QBFSL -> QBFSL -> Ordering
QBFSL -> QBFSL -> QBFSL
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 :: QBFSL -> QBFSL -> QBFSL
$cmin :: QBFSL -> QBFSL -> QBFSL
max :: QBFSL -> QBFSL -> QBFSL
$cmax :: QBFSL -> QBFSL -> QBFSL
>= :: QBFSL -> QBFSL -> Bool
$c>= :: QBFSL -> QBFSL -> Bool
> :: QBFSL -> QBFSL -> Bool
$c> :: QBFSL -> QBFSL -> Bool
<= :: QBFSL -> QBFSL -> Bool
$c<= :: QBFSL -> QBFSL -> Bool
< :: QBFSL -> QBFSL -> Bool
$c< :: QBFSL -> QBFSL -> Bool
compare :: QBFSL -> QBFSL -> Ordering
$ccompare :: QBFSL -> QBFSL -> Ordering
$cp1Ord :: Eq QBFSL
Ord, Typeable, Typeable QBFSL
Constr
DataType
Typeable QBFSL =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> QBFSL -> c QBFSL)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c QBFSL)
-> (QBFSL -> Constr)
-> (QBFSL -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c QBFSL))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QBFSL))
-> ((forall b. Data b => b -> b) -> QBFSL -> QBFSL)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QBFSL -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QBFSL -> r)
-> (forall u. (forall d. Data d => d -> u) -> QBFSL -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> QBFSL -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> QBFSL -> m QBFSL)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> QBFSL -> m QBFSL)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> QBFSL -> m QBFSL)
-> Data QBFSL
QBFSL -> Constr
QBFSL -> DataType
(forall b. Data b => b -> b) -> QBFSL -> QBFSL
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QBFSL -> c QBFSL
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QBFSL
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) -> QBFSL -> u
forall u. (forall d. Data d => d -> u) -> QBFSL -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QBFSL -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QBFSL -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QBFSL -> m QBFSL
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QBFSL -> m QBFSL
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QBFSL
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QBFSL -> c QBFSL
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QBFSL)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QBFSL)
$cQBFSL :: Constr
$tQBFSL :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> QBFSL -> m QBFSL
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QBFSL -> m QBFSL
gmapMp :: (forall d. Data d => d -> m d) -> QBFSL -> m QBFSL
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QBFSL -> m QBFSL
gmapM :: (forall d. Data d => d -> m d) -> QBFSL -> m QBFSL
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QBFSL -> m QBFSL
gmapQi :: Int -> (forall d. Data d => d -> u) -> QBFSL -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> QBFSL -> u
gmapQ :: (forall d. Data d => d -> u) -> QBFSL -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> QBFSL -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QBFSL -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QBFSL -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QBFSL -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QBFSL -> r
gmapT :: (forall b. Data b => b -> b) -> QBFSL -> QBFSL
$cgmapT :: (forall b. Data b => b -> b) -> QBFSL -> QBFSL
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QBFSL)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QBFSL)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c QBFSL)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QBFSL)
dataTypeOf :: QBFSL -> DataType
$cdataTypeOf :: QBFSL -> DataType
toConstr :: QBFSL -> Constr
$ctoConstr :: QBFSL -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QBFSL
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QBFSL
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QBFSL -> c QBFSL
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QBFSL -> c QBFSL
$cp1Data :: Typeable QBFSL
Data)

isProp :: QBFSL -> Bool
isProp :: QBFSL -> Bool
isProp sl :: QBFSL
sl = QBFSL -> QBFFormulae
format QBFSL
sl QBFFormulae -> QBFFormulae -> Bool
forall a. Eq a => a -> a -> Bool
== QBFFormulae
PlainFormula

isHC :: QBFSL -> Bool
isHC :: QBFSL -> Bool
isHC sl :: QBFSL
sl = QBFSL -> QBFFormulae
format QBFSL
sl QBFFormulae -> QBFFormulae -> Bool
forall a. Eq a => a -> a -> Bool
== QBFFormulae
HornClause

-- | comparison of sublogics
compareLE :: QBFSL -> QBFSL -> Bool
compareLE :: QBFSL -> QBFSL -> Bool
compareLE p1 :: QBFSL
p1 p2 :: QBFSL
p2 =
    let f1 :: QBFFormulae
f1 = QBFSL -> QBFFormulae
format QBFSL
p1
        f2 :: QBFFormulae
f2 = QBFSL -> QBFFormulae
format QBFSL
p2
    in
      case (QBFFormulae
f1, QBFFormulae
f2) of
        (_, PlainFormula) -> Bool
True
        (HornClause, HornClause) -> Bool
True
        (_, HornClause) -> Bool
False

-- Special elements in the Lattice of logics

top :: QBFSL
top :: QBFSL
top = QBFFormulae -> QBFSL
QBFSL QBFFormulae
PlainFormula

bottom :: QBFSL
bottom :: QBFSL
bottom = QBFFormulae -> QBFSL
QBFSL QBFFormulae
HornClause

needPF :: QBFSL
needPF :: QBFSL
needPF = QBFSL
bottom { format :: QBFFormulae
format = QBFFormulae
PlainFormula }

-- join and max

sublogicsJoin :: (QBFFormulae -> QBFFormulae -> QBFFormulae)
                  -> QBFSL -> QBFSL -> QBFSL
sublogicsJoin :: (QBFFormulae -> QBFFormulae -> QBFFormulae)
-> QBFSL -> QBFSL -> QBFSL
sublogicsJoin pfF :: QBFFormulae -> QBFFormulae -> QBFFormulae
pfF a :: QBFSL
a b :: QBFSL
b = QBFSL :: QBFFormulae -> QBFSL
QBFSL
                         {
                           format :: QBFFormulae
format = QBFFormulae -> QBFFormulae -> QBFFormulae
pfF (QBFSL -> QBFFormulae
format QBFSL
a) (QBFSL -> QBFFormulae
format QBFSL
b)
                         }

joinType :: QBFFormulae -> QBFFormulae -> QBFFormulae
joinType :: QBFFormulae -> QBFFormulae -> QBFFormulae
joinType HornClause HornClause = QBFFormulae
HornClause
joinType _ _ = QBFFormulae
PlainFormula

sublogicsMax :: QBFSL -> QBFSL -> QBFSL
sublogicsMax :: QBFSL -> QBFSL -> QBFSL
sublogicsMax = (QBFFormulae -> QBFFormulae -> QBFFormulae)
-> QBFSL -> QBFSL -> QBFSL
sublogicsJoin QBFFormulae -> QBFFormulae -> QBFFormulae
joinType

-- Helpers

-- compute sublogics from a list of sublogics

compList :: [QBFSL] -> QBFSL
compList :: [QBFSL] -> QBFSL
compList = (QBFSL -> QBFSL -> QBFSL) -> QBFSL -> [QBFSL] -> QBFSL
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl QBFSL -> QBFSL -> QBFSL
sublogicsMax QBFSL
bottom

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

-- | determines the sublogic for symbol map items
slSymmap :: QBFSL -> AS_BASIC.SYMBMAPITEMS -> QBFSL
slSymmap :: QBFSL -> SYMBMAPITEMS -> QBFSL
slSymmap ps :: QBFSL
ps _ = QBFSL
ps

-- | determines the sublogic for a morphism
slMor :: QBFSL -> Morphism.Morphism -> QBFSL
slMor :: QBFSL -> Morphism -> QBFSL
slMor ps :: QBFSL
ps _ = QBFSL
ps

-- | determines the sublogic for a Signature
slSig :: QBFSL -> Sign.Sign -> QBFSL
slSig :: QBFSL -> Sign -> QBFSL
slSig ps :: QBFSL
ps _ = QBFSL
ps

-- | determines the sublogic for Symbol items
slSymit :: QBFSL -> AS_BASIC.SYMBITEMS -> QBFSL
slSymit :: QBFSL -> SYMBITEMS -> QBFSL
slSymit ps :: QBFSL
ps _ = QBFSL
ps

-- | determines the sublogic for symbols
slSym :: QBFSL -> Symbol.Symbol -> QBFSL
slSym :: QBFSL -> Symbol -> QBFSL
slSym ps :: QBFSL
ps _ = QBFSL
ps

-- | determines sublogic for formula
slForm :: QBFSL -> AS_BASIC.FORMULA -> QBFSL
slForm :: QBFSL -> FORMULA -> QBFSL
slForm ps :: QBFSL
ps = QBFSL -> [FORMULA] -> QBFSL
slFlForm QBFSL
ps ([FORMULA] -> QBFSL) -> (FORMULA -> [FORMULA]) -> FORMULA -> QBFSL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> [FORMULA]
Tools.flatten

-- | determines sublogic for flattened formula
slFlForm :: QBFSL -> [AS_BASIC.FORMULA] -> QBFSL
slFlForm :: QBFSL -> [FORMULA] -> QBFSL
slFlForm ps :: QBFSL
ps = (QBFSL -> QBFSL -> QBFSL) -> QBFSL -> [QBFSL] -> QBFSL
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl QBFSL -> QBFSL -> QBFSL
sublogicsMax QBFSL
ps
  ([QBFSL] -> QBFSL) -> ([FORMULA] -> [QBFSL]) -> [FORMULA] -> QBFSL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FORMULA -> QBFSL) -> [FORMULA] -> [QBFSL]
forall a b. (a -> b) -> [a] -> [b]
map (\ x :: FORMULA
x -> State Int QBFSL -> Int -> QBFSL
forall s a. State s a -> s -> a
State.evalState (QBFSL -> FORMULA -> State Int QBFSL
anaForm QBFSL
ps FORMULA
x) 0)

-- analysis of single "clauses"
anaForm :: QBFSL -> AS_BASIC.FORMULA -> State.State Int QBFSL
anaForm :: QBFSL -> FORMULA -> State Int QBFSL
anaForm ps :: QBFSL
ps f :: FORMULA
f =
    case FORMULA
f of
      AS_BASIC.Conjunction l :: [FORMULA]
l _ ->
          do
            Int
st <- State Int Int
forall s. State s s
State.get
            QBFSL -> State Int QBFSL
forall (m :: * -> *) a. Monad m => a -> m a
return (QBFSL -> State Int QBFSL) -> QBFSL -> State Int QBFSL
forall a b. (a -> b) -> a -> b
$ QBFSL -> QBFSL -> QBFSL
sublogicsMax QBFSL
needPF (QBFSL -> QBFSL) -> QBFSL -> QBFSL
forall a b. (a -> b) -> a -> b
$ [QBFSL] -> QBFSL
compList ([QBFSL] -> QBFSL) -> [QBFSL] -> QBFSL
forall a b. (a -> b) -> a -> b
$ (FORMULA -> QBFSL) -> [FORMULA] -> [QBFSL]
forall a b. (a -> b) -> [a] -> [b]
map
              (\ x :: FORMULA
x -> State Int QBFSL -> Int -> QBFSL
forall s a. State s a -> s -> a
State.evalState (QBFSL -> FORMULA -> State Int QBFSL
anaForm QBFSL
ps FORMULA
x) (Int
st Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)) [FORMULA]
l
      AS_BASIC.Implication l :: FORMULA
l m :: FORMULA
m _ ->
          do
             Int
st <- State Int Int
forall s. State s s
State.get
             let analyze :: QBFSL
analyze = QBFSL -> QBFSL -> QBFSL
sublogicsMax QBFSL
needPF (QBFSL -> QBFSL) -> QBFSL -> QBFSL
forall a b. (a -> b) -> a -> b
$ QBFSL -> QBFSL -> QBFSL
sublogicsMax
                   ((\ x :: FORMULA
x -> State Int QBFSL -> Int -> QBFSL
forall s a. State s a -> s -> a
State.evalState (QBFSL -> FORMULA -> State Int QBFSL
anaForm QBFSL
ps FORMULA
x) (Int
st Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)) FORMULA
l)
                   ((\ x :: FORMULA
x -> State Int QBFSL -> Int -> QBFSL
forall s a. State s a -> s -> a
State.evalState (QBFSL -> FORMULA -> State Int QBFSL
anaForm QBFSL
ps FORMULA
x) (Int
st Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)) FORMULA
m)
             QBFSL -> State Int QBFSL
forall (m :: * -> *) a. Monad m => a -> m a
return (QBFSL -> State Int QBFSL) -> QBFSL -> State Int QBFSL
forall a b. (a -> b) -> a -> b
$
                    if Int
st Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 1 Bool -> Bool -> Bool
&& QBFSL -> QBFFormulae
format QBFSL
ps QBFFormulae -> QBFFormulae -> Bool
forall a. Eq a => a -> a -> Bool
== QBFFormulae
HornClause Bool -> Bool -> Bool
&& FORMULA -> FORMULA -> Bool
checkHornPos FORMULA
l FORMULA
m
                    then
                        QBFSL
ps
                    else
                        QBFSL
analyze
      AS_BASIC.Equivalence l :: FORMULA
l m :: FORMULA
m _ ->
           do
             Int
st <- State Int Int
forall s. State s s
State.get
             QBFSL -> State Int QBFSL
forall (m :: * -> *) a. Monad m => a -> m a
return (QBFSL -> State Int QBFSL) -> QBFSL -> State Int QBFSL
forall a b. (a -> b) -> a -> b
$ QBFSL -> QBFSL -> QBFSL
sublogicsMax QBFSL
needPF (QBFSL -> QBFSL) -> QBFSL -> QBFSL
forall a b. (a -> b) -> a -> b
$ QBFSL -> QBFSL -> QBFSL
sublogicsMax
               ((\ x :: FORMULA
x -> State Int QBFSL -> Int -> QBFSL
forall s a. State s a -> s -> a
State.evalState (QBFSL -> FORMULA -> State Int QBFSL
anaForm QBFSL
ps FORMULA
x) (Int
st Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)) FORMULA
l)
               ((\ x :: FORMULA
x -> State Int QBFSL -> Int -> QBFSL
forall s a. State s a -> s -> a
State.evalState (QBFSL -> FORMULA -> State Int QBFSL
anaForm QBFSL
ps FORMULA
x) (Int
st Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)) FORMULA
m)
      AS_BASIC.Negation l :: FORMULA
l _ ->
          if FORMULA -> Bool
isLiteral FORMULA
l
          then
                QBFSL -> State Int QBFSL
forall (m :: * -> *) a. Monad m => a -> m a
return QBFSL
ps
          else
              do
                Int
st <- State Int Int
forall s. State s s
State.get
                QBFSL -> State Int QBFSL
forall (m :: * -> *) a. Monad m => a -> m a
return (QBFSL -> State Int QBFSL) -> QBFSL -> State Int QBFSL
forall a b. (a -> b) -> a -> b
$ (\ x :: FORMULA
x -> State Int QBFSL -> Int -> QBFSL
forall s a. State s a -> s -> a
State.evalState (QBFSL -> FORMULA -> State Int QBFSL
anaForm QBFSL
ps FORMULA
x) (Int
st Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)) FORMULA
l
      AS_BASIC.Disjunction l :: [FORMULA]
l _ ->
                    let lprime :: [FORMULA]
lprime = (FORMULA -> [FORMULA]) -> [FORMULA] -> [FORMULA]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap FORMULA -> [FORMULA]
Tools.flattenDis [FORMULA]
l in
                    if (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all FORMULA -> Bool
isLiteral [FORMULA]
lprime
                    then QBFSL -> State Int QBFSL
forall (m :: * -> *) a. Monad m => a -> m a
return (QBFSL -> State Int QBFSL) -> QBFSL -> State Int QBFSL
forall a b. (a -> b) -> a -> b
$
                        if [FORMULA] -> Int -> Bool
moreThanNLit [FORMULA]
lprime 1
                          then QBFSL -> QBFSL -> QBFSL
sublogicsMax QBFSL
needPF QBFSL
ps
                          else QBFSL
ps
                    else
                        do
                          Int
st <- State Int Int
forall s. State s s
State.get
                          QBFSL -> State Int QBFSL
forall (m :: * -> *) a. Monad m => a -> m a
return (QBFSL -> State Int QBFSL) -> QBFSL -> State Int QBFSL
forall a b. (a -> b) -> a -> b
$ QBFSL -> QBFSL -> QBFSL
sublogicsMax QBFSL
needPF (QBFSL -> QBFSL) -> QBFSL -> QBFSL
forall a b. (a -> b) -> a -> b
$ [QBFSL] -> QBFSL
compList ([QBFSL] -> QBFSL) -> [QBFSL] -> QBFSL
forall a b. (a -> b) -> a -> b
$ (FORMULA -> QBFSL) -> [FORMULA] -> [QBFSL]
forall a b. (a -> b) -> [a] -> [b]
map
                            (\ x :: FORMULA
x -> State Int QBFSL -> Int -> QBFSL
forall s a. State s a -> s -> a
State.evalState (QBFSL -> FORMULA -> State Int QBFSL
anaForm QBFSL
ps FORMULA
x) (Int
st Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1))
                                      [FORMULA]
lprime
      AS_BASIC.TrueAtom _ -> QBFSL -> State Int QBFSL
forall (m :: * -> *) a. Monad m => a -> m a
return QBFSL
ps
      AS_BASIC.FalseAtom _ -> QBFSL -> State Int QBFSL
forall (m :: * -> *) a. Monad m => a -> m a
return QBFSL
ps
      AS_BASIC.Predication _ -> QBFSL -> State Int QBFSL
forall (m :: * -> *) a. Monad m => a -> m a
return QBFSL
ps
      AS_BASIC.ForAll {} -> QBFSL -> State Int QBFSL
forall (m :: * -> *) a. Monad m => a -> m a
return QBFSL
needPF
      AS_BASIC.Exists {} -> QBFSL -> State Int QBFSL
forall (m :: * -> *) a. Monad m => a -> m a
return QBFSL
needPF

moreThanNLit :: [AS_BASIC.FORMULA] -> Int -> Bool
moreThanNLit :: [FORMULA] -> Int -> Bool
moreThanNLit = Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
(>) (Int -> Int -> Bool)
-> ([FORMULA] -> Int) -> [FORMULA] -> Int -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Bool -> Int) -> Int -> [Bool] -> Int
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
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
  ([Bool] -> Int) -> ([FORMULA] -> [Bool]) -> [FORMULA] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FORMULA -> Bool) -> [FORMULA] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> Bool
isPosLiteral

-- 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.ForAll {}) = Bool
False
isLiteral (AS_BASIC.Exists {}) = Bool
False
isLiteral (AS_BASIC.TrueAtom _) = Bool
True
isLiteral (AS_BASIC.FalseAtom _) = 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.ForAll {}) = Bool
False
isPosLiteral (AS_BASIC.Exists {}) = Bool
False
isPosLiteral (AS_BASIC.TrueAtom _ ) = Bool
True
isPosLiteral (AS_BASIC.FalseAtom _) = Bool
True

-- | determines subloig for basic items
slBasicItems :: QBFSL -> AS_BASIC.BASICITEMS -> QBFSL
slBasicItems :: QBFSL -> BASICITEMS -> QBFSL
slBasicItems ps :: QBFSL
ps bi :: BASICITEMS
bi =
    case BASICITEMS
bi of
      AS_BASIC.PredDecl _ -> QBFSL
ps
      AS_BASIC.AxiomItems xs :: [Annoted FORMULA]
xs -> [QBFSL] -> QBFSL
compList ([QBFSL] -> QBFSL) -> [QBFSL] -> QBFSL
forall a b. (a -> b) -> a -> b
$ (Annoted FORMULA -> QBFSL) -> [Annoted FORMULA] -> [QBFSL]
forall a b. (a -> b) -> [a] -> [b]
map (QBFSL -> FORMULA -> QBFSL
slForm QBFSL
ps (FORMULA -> QBFSL)
-> (Annoted FORMULA -> FORMULA) -> Annoted FORMULA -> QBFSL
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
slBasicSpec :: QBFSL -> AS_BASIC.BASICSPEC -> QBFSL
slBasicSpec :: QBFSL -> BASICSPEC -> QBFSL
slBasicSpec ps :: QBFSL
ps (AS_BASIC.BasicSpec spec :: [Annoted BASICITEMS]
spec) =
    [QBFSL] -> QBFSL
compList ([QBFSL] -> QBFSL) -> [QBFSL] -> QBFSL
forall a b. (a -> b) -> a -> b
$ (Annoted BASICITEMS -> QBFSL) -> [Annoted BASICITEMS] -> [QBFSL]
forall a b. (a -> b) -> [a] -> [b]
map (QBFSL -> BASICITEMS -> QBFSL
slBasicItems QBFSL
ps (BASICITEMS -> QBFSL)
-> (Annoted BASICITEMS -> BASICITEMS)
-> Annoted BASICITEMS
-> QBFSL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted BASICITEMS -> BASICITEMS
forall a. Annoted a -> a
AS_Anno.item) [Annoted BASICITEMS]
spec

-- | all sublogics
sublogicsAll :: [QBFSL]
sublogicsAll :: [QBFSL]
sublogicsAll =
    [QBFSL :: QBFFormulae -> QBFSL
QBFSL
     {
       format :: QBFFormulae
format = QBFFormulae
HornClause
     }
    , QBFSL :: QBFFormulae -> QBFSL
QBFSL
     {
       format :: QBFFormulae
format = QBFFormulae
PlainFormula
     }
    ]

-- Conversion functions to String

sublogicsName :: QBFSL -> String
sublogicsName :: QBFSL -> String
sublogicsName f :: QBFSL
f = case QBFSL -> QBFFormulae
format QBFSL
f of
      HornClause -> "HornClause"
      PlainFormula -> "Prop"

-- Projections to sublogics

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

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

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

prSymMapM :: QBFSL
          -> AS_BASIC.SYMBMAPITEMS
          -> Maybe AS_BASIC.SYMBMAPITEMS
prSymMapM :: QBFSL -> SYMBMAPITEMS -> Maybe SYMBMAPITEMS
prSymMapM _ = SYMBMAPITEMS -> Maybe SYMBMAPITEMS
forall a. a -> Maybe a
Just

prSymM :: QBFSL -> AS_BASIC.SYMBITEMS -> Maybe AS_BASIC.SYMBITEMS
prSymM :: QBFSL -> SYMBITEMS -> Maybe SYMBITEMS
prSymM _ = SYMBITEMS -> Maybe SYMBITEMS
forall a. a -> Maybe a
Just

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

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

prPredItem :: QBFSL -> AS_BASIC.PREDITEM -> AS_BASIC.PREDITEM
prPredItem :: QBFSL -> PREDITEM -> PREDITEM
prPredItem _ prI :: PREDITEM
prI = PREDITEM
prI

prBASICItems :: QBFSL -> AS_BASIC.BASICITEMS -> AS_BASIC.BASICITEMS
prBASICItems :: QBFSL -> BASICITEMS -> BASICITEMS
prBASICItems pSL :: QBFSL
pSL bI :: BASICITEMS
bI =
    case BASICITEMS
bI of
      AS_BASIC.PredDecl pI :: PREDITEM
pI -> PREDITEM -> BASICITEMS
AS_BASIC.PredDecl (PREDITEM -> BASICITEMS) -> PREDITEM -> BASICITEMS
forall a b. (a -> b) -> a -> b
$ QBFSL -> PREDITEM -> PREDITEM
prPredItem QBFSL
pSL PREDITEM
pI
      AS_BASIC.AxiomItems aIS :: [Annoted FORMULA]
aIS -> [Annoted FORMULA] -> BASICITEMS
AS_BASIC.AxiomItems ([Annoted FORMULA] -> BASICITEMS)
-> [Annoted FORMULA] -> BASICITEMS
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 = QBFSL -> FORMULA -> Maybe FORMULA
prFormulaM QBFSL
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 :: QBFSL -> AS_BASIC.BASICSPEC -> AS_BASIC.BASICSPEC
prBasicSpec :: QBFSL -> BASICSPEC -> BASICSPEC
prBasicSpec pSL :: QBFSL
pSL (AS_BASIC.BasicSpec bS :: [Annoted BASICITEMS]
bS) =
    [Annoted BASICITEMS] -> BASICSPEC
AS_BASIC.BasicSpec ([Annoted BASICITEMS] -> BASICSPEC)
-> [Annoted BASICITEMS] -> BASICSPEC
forall a b. (a -> b) -> a -> b
$ (Annoted BASICITEMS -> Annoted BASICITEMS)
-> [Annoted BASICITEMS] -> [Annoted BASICITEMS]
forall a b. (a -> b) -> [a] -> [b]
map Annoted BASICITEMS -> Annoted BASICITEMS
mapH [Annoted BASICITEMS]
bS
    where
      mapH :: AS_Anno.Annoted AS_BASIC.BASICITEMS
           -> AS_Anno.Annoted AS_BASIC.BASICITEMS
      mapH :: Annoted BASICITEMS -> Annoted BASICITEMS
mapH aBI :: Annoted BASICITEMS
aBI = Annoted :: forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
AS_Anno.Annoted
                 {
                   item :: BASICITEMS
AS_Anno.item = QBFSL -> BASICITEMS -> BASICITEMS
prBASICItems QBFSL
pSL (BASICITEMS -> BASICITEMS) -> BASICITEMS -> BASICITEMS
forall a b. (a -> b) -> a -> b
$ Annoted BASICITEMS -> BASICITEMS
forall a. Annoted a -> a
AS_Anno.item Annoted BASICITEMS
aBI
                 , opt_pos :: Range
AS_Anno.opt_pos = Annoted BASICITEMS -> Range
forall a. Annoted a -> Range
AS_Anno.opt_pos Annoted BASICITEMS
aBI
                 , l_annos :: [Annotation]
AS_Anno.l_annos = Annoted BASICITEMS -> [Annotation]
forall a. Annoted a -> [Annotation]
AS_Anno.l_annos Annoted BASICITEMS
aBI
                 , r_annos :: [Annotation]
AS_Anno.r_annos = Annoted BASICITEMS -> [Annotation]
forall a. Annoted a -> [Annotation]
AS_Anno.r_annos Annoted BASICITEMS
aBI
                 }

checkHornPos :: AS_BASIC.FORMULA -> AS_BASIC.FORMULA -> Bool
checkHornPos :: FORMULA -> FORMULA -> Bool
checkHornPos fc :: FORMULA
fc fl :: FORMULA
fl =
    case FORMULA
fc of
      AS_BASIC.Conjunction _ _ -> (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all FORMULA -> Bool
isPosLiteral ([FORMULA] -> Bool) -> [FORMULA] -> Bool
forall a b. (a -> b) -> a -> b
$ FORMULA -> [FORMULA]
Tools.flatten FORMULA
fc
      _ -> Bool
False
    Bool -> Bool -> Bool
&&
    FORMULA -> Bool
isPosLiteral FORMULA
fl