{-# 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